import sys
import collections
from antlr4 import *
from CLexer import CLexer
from CParser import CParser
from CListener import CListener


def main():
    get_file()

    file = FileStream("program.c")
    lexer = CLexer(file)
    stream = CommonTokenStream(lexer)
    parser = CParser(stream)
    tree = parser.compilationUnit()

    listener = myCListener()
    walker = ParseTreeWalker()
    walker.walk(listener, tree)

    listener.show()


def get_file():
    try:
        f1 = open(sys.argv[1], "rt")
        x = f1.readline()
        while x.startswith("#include"):
            x = f1.readline()
        f2 = open("program.c", "wt")
        f2.write(f1.read())
        f1.close()
        f2.close()
    except IndexError:
        print("Error - You forgot to enter a file")
        sys.exit(1)
    except FileNotFoundError:
        print("Error - Please enter a valid file")
        sys.exit(1)


class myCListener(CListener):

    def __init__(self):
        self.is_main = True
        self.variable = {}
        self.variable_if = {}
        self.variable_for = {}
        self.parameter = []
        self.function_name = ""
        self.in_if = False
        self.if_condition = ""

    def enterFunctionDefinition(self, ctx: CParser.FunctionDefinitionContext):
        # function_name = ctx.children.get(1).getChild(0).getChild(0).getText()
        function_name = ctx.children[1].getChild(0).getChild(0).getText()
        if function_name == "main":
            self.is_main = False
            return
        self.function_name = function_name

    def enterParameterDeclaration(self, ctx: CParser.ParameterDeclarationContext):
        if self.is_main:
            self.parameter.append(ctx.declarator().getText())

    def enterInitDeclarator(self, ctx: CParser.InitDeclaratorContext):
        if self.is_main:
            variable_name = ctx.declarator().getText()
            variable_value = ctx.initializer().getText()
            self.variable[variable_name] = variable_value

    def enterExpressionStatement(self, ctx: CParser.ExpressionStatementContext):
        expr = ctx.getText()
        if self.is_main:
            if not self.in_if:
                self.resolve(expr)
        else:
            # expr = expr[17:]  OR:
            # expr = re.sub("^printf\(\"%d\"," + "KjZC\(", "", expr) OR:
            expr = expr[expr.index(self.function_name) + len(self.function_name) + 1: -3]
            expr = expr.split(",")
            for i in range(len(expr)):
                self.parameter[i] = {self.parameter[i]: expr[i]}

    # if:
    def enterSelectionStatement(self, ctx: CParser.SelectionStatementContext):
        self.variable_if = self.variable.copy()
        self.in_if = True
        self.if_condition = ctx.children[2].getText()

        a = str(ctx.children[4].getText()[1:-2])
        a = a.split(";")
        for k in a:
            # self.resolve(k)
            k = k.replace(";", "")
            k = k.split("=")
            for i,j in self.variable_if.items():
                if i in k[1]:
                    # k[1] = k[1].replace(i, j)
                    k[1] = k[1].replace(i, "(" + j + ")")
            self.variable_if[k[0]] = k[1]

    def exitSelectionStatement(self, ctx: CParser.SelectionStatementContext):
        self.in_if = False

    # for:
    def enterIterationStatement(self, ctx: CParser.IterationStatementContext):
        self.variable_for = self.variable.copy()
        for_condition = ctx.children[2].getText().split(";")
        # eg. i=0
        a = str(for_condition[0]).split("=")
        a = str(ctx.children[4].getText())[1:-2]
        a = a.split(";")
        for k in a:
            # self.resolve(k)
            k = k.replace(";", "")
            k = k.split("=")
            for i, j in self.variable_for.items():
                if i in k[1]:
                    # k[1] = k[1].replace(i, j)
                    k[1] = k[1].replace(i, "(" + j + ")")
            self.variable_for[k[0]] = k[1]

    def resolve(self, expr):
        expr = expr.replace(";", "")
        expr = expr.split("=")
        for i, j in self.variable.items():
            if i in expr[1]:
                # expr[1] = expr[1].replace(i, j)
                expr[1] = expr[1].replace(i, "(" + j + ")")
        self.variable[expr[0]] = expr[1]

    def show(self):
        f = open("output.txt", "wt")
        a = self.variable_if.copy()
        b = self.variable_for.copy()

        for i, j in self.variable.items():
            for k in list(a.values()):
                if j == k:
                    a.pop(i)
            for k in list(b.values()):
                if j == k:
                    b.pop(i)

        f.write("***********************************\n")
        f.write("Symbolic formula:\n")
        f.write("***********************************\n")

        # x = collections.OrderedDict(sorted(self.variable.items(), key=lambda t: t[1]))
        f.write("\nPath that leads to if:\n\n")
        # for i,j in x.items():
        #     f.write(i + ": " + j + "\n")
        for i, j in self.variable_if.items():
            f.write(i + ": " + j + "\n")
        # for i, j in sorted(self.variable_if.items()):
        #     f.write(i + ": " + j + "\n")
        # for i in sorted(self.variable_if.keys()):
        #     f.write(i + ": " + self.variable_if[i] + "\n")

        f.write("\n\nPath that leads to for:\n\n")
        for i, j in self.variable_for.items():
            if i != "i":
                f.write(i + ": " + j + "\n")

        for i in self.parameter:
            for x,y in i.items():
                for n,m in self.variable_if.items():
                    if x in m:
                        m = m.replace(x, y)
                        self.variable_if[n]=m

                for n,m in self.variable_for.items():
                    if x in m:
                        m = m.replace(x, y)
                        self.variable_for[n]=m
                if x in self.if_condition:
                    self.if_condition = self.if_condition.replace(x, y)

        f.write("\n------------------------------------------------------------------------------------------------------------------\n")
        f.write("\n***********************************\n")
        f.write("Real values:\n")
        f.write("***********************************\n")

        number_of_integer_overflow = 0
        number_of_division_by_zero = 0

        if eval(self.if_condition):
            f.write("\nPath leads to if:\n")
            for i, j in self.variable_if.items():
                answer = 0
                try:
                    answer = eval(j)
                    if answer > 2147483647 or answer < -2147483648:
                        number_of_integer_overflow += 1
                        f.write("Found Interger Overflow: " + i + " = " + str(answer) + "\n")
                    else:
                        f.write(i + ": " + str(answer) + "\n")
                except ZeroDivisionError:
                    number_of_division_by_zero += 1
                    f.write("Found By Division Error in " + i + "\n")

        else:
            f.write("\nPath leads to for:\n")
            for i, j in self.variable_for.items():
                answer = 0
                try:
                    answer = eval(j)
                    if answer > 2147483647 or answer < -2147483648:
                        number_of_integer_overflow += 1
                        f.write("Found Interger Overflow: " + i + " = " + str(answer) + "\n")
                    else:
                        f.write(i + ": " + str(answer) + "\n")
                except ZeroDivisionError:
                    number_of_division_by_zero += 1
                    f.write("Found By Division Error in " + i + "\n")

        f.write("\n***********************************\n")
        f.write("Number of Integer Overflow: " + str(number_of_integer_overflow) + "\n")
        f.write("Number of Division By Zero: " + str(number_of_division_by_zero) + "\n")
        f.write("***********************************\n")


if __name__ == '__main__':
    main()
