import rbr_rule
import os
from timeit import default_timer as dtimer
import traceback

'''
This module translate the RBR generated by EthIR to SACO RBR.
It receives a list with rbr_rule instances.
'''

costabs_path = "/tmp/costabs/"
tmp_path = "/tmp/"

global pattern
pattern = ["PUSH1",
                   "DUP2",
                   "PUSH1",
                   "AND",
                   "ISZERO",
                   "PUSH2",
                   "MUL",
                   "SUB",
                   "AND",
                   "PUSH1",
                   "SWAP1",
                   "DIV"]

global st_vars

def rbr2saco(rbr,execution,cname):
    global st_vars

    begin = dtimer()

    st_vars = rbr[0][0].get_all_state_vars()
    new_rules = []
    try:
        for rules in rbr:
            for rule in rules:
                new_rule = process_rule_saco(rule)
                new_rules.append(new_rule)

        write(new_rules,execution,cname)
        end = dtimer()
        print("SACO RBR: "+str(end-begin)+"s")

    except:
        #print traceback.print_exc()
        raise Exception("Error in SACO translation",5)
    
def build_head(rule):
    head = rule.get_rule_name()

    input_vars = rule.vars_to_string("input")

    local_vars = rule.build_local_vars() 
    local_vars_string = ", ".join(local_vars)
    
    gv_aux = get_field_vars(rule)
    if(len(gv_aux)> 0 ):
        gv = ", ".join(gv_aux)
    else:
        gv = ""
    
    cv_aux = get_contract_vars(rule)
    if(len(cv_aux)>0):
        cv = ", ".join(cv_aux)
    else:
        cv = ""

    if (input_vars == ""):
            if(gv == ""):
                d_vars = ""
            else:
                d_vars = gv
    else:
        d_vars = input_vars
        if(gv != ""):
            d_vars = d_vars+", "+gv

    if d_vars == "" and local_vars_string != "":
        d_vars = local_vars_string
    elif d_vars != "" and local_vars_string != "":
        d_vars = d_vars+", "+local_vars_string
    
    if d_vars != "" and cv != "":
        d_vars = d_vars+", "+cv
    elif d_vars == "" and cv != "":
        d_vars = cv
    
    return head+"("+d_vars+")=>"



def process_rule_saco(rule):
    new_rule = ""
    head = build_head(rule)
    new_rule = new_rule+head+"\n"
    if rule.get_guard()!="":
        new_rule = new_rule+"\t"+rule.get_guard()+"\n"

    instr_aux = process_instructions(rule)
    instr = filter(lambda x: x !="",instr_aux)
    for ins in instr:
        new_rule = new_rule+"\t"+ins+"\n"

    return new_rule
    

def get_contract_vars(rule):
    bc = rule.get_bc()
    new = map(lambda x: "l("+x+")",bc)
    return new

def get_field_vars(rule):
    names, numeric = rule.get_global_arg()

    if numeric != []:
        new_numeric = map(lambda x: "field(g"+x+")",numeric)
    else:
        new_numeric = []
        
    if names != []:
        new_names = map(lambda x: "field("+x+")",names)
    else:
        new_names = []
        
    new = new_names+new_numeric 

    return new

def transform_vars(var):
    
    if var.find("s(")!=-1: #stack variable
        new_var = var
    elif var.find("g(")!=-1: #field variable
        posEnd = var.find(")")
        if st_vars ==[]:
            new_var = "field(g"+var[2:posEnd]+")"
        else:
            new_var = "field("+var[2:posEnd]+")"
    elif var.find("l(")!=-1: #local variable
        new_var = var
    elif var != "": #contract variable
        new_var = "l("+var+")"
    else:
        new_var = ""
    return new_var

def call_instruction(instr):

    pos_head = instr.find("(",5) #It is a call. It starts with call(__(
    end = len(instr)-2
    variables = instr[pos_head+1:end].split(",")
    new_vars = map(lambda x: transform_vars(x.strip()),variables)
    new_vars_string = ", ".join(new_vars)

    new_instr = instr[:pos_head+1]+new_vars_string+"))"
    return new_instr
    
def process_instructions(rule):
    cont = rule.get_fresh_index()+1
    contract_vars = rule.get_bc()
    instructions = rule.get_instructions()
    new_instructions = []
    has_string_pattern = rule.get_string_getter()
    idx_loop = 0
    len_ins = len(instructions)
    
    while(idx_loop<len_ins):
        instr = instructions[idx_loop]

        if idx_loop == 8 and has_string_pattern:
            new_instructions = compute_string_pattern(new_instructions)
            idx_loop = idx_loop+26
        elif instr.find("/")!=-1:
            idx_loop = check_mul_div_pattern(new_instructions,instructions,idx_loop)
        else:
            cont = process_single_instruction(instr,new_instructions,contract_vars,cont)
            idx_loop = idx_loop+1
            
    return new_instructions

            
def process_single_instruction(instr,new_instructions,contract_vars,cont):        
    if instr.find("call(",0)!=-1:
        new = call_instruction(instr)
    elif instr.find("and(",0)!=-1:
        # nop_top = new_instructions[-1]
        # top = new_instructions[-2]
        # number = top.split("=")[1].strip()
        
        # try:
        #     number = int(number)
        #     bin_num = bin(number)
        #     l = filter(lambda x: x!="1",bin_num)
        #     if l == "0b":
        #         number = "1"
        #     elif l == "0b0":
        #         number = "0"
        #     else:
        #         number = "none"
        # except:
        #     number = "none"
        # finally:
        #     one = False
        #     if number == "1":
        #         one = True
        #     elif number == "0":
        #         var = " 0"
        #     else:
        #         var = " s("+str(cont)+")"
        #         cont+=1
        #     if one:
        #         new = ""
        #     else:
        #         pos = instr.find("=")
        #         new = instr[:pos+1]+var
            
        pos = instr.find("=")
        var = " s("+str(cont)+")"
        new = instr[:pos+1]+var
        cont+=1
    elif instr.find("or(",0)!=-1:
        pos = instr.find("=")
        new = instr[:pos+1]+" s("+str(cont)+")"
        cont+=1
    elif instr.find("not(",0)!=-1:
        # nop_top = new_instructions[-1]
        # top = new_instructions[-2]
        # if nop_top.startswith("nop(PUSH"):
        #     number = top.split("=")[1].strip()
        #     if number == " 1":
        #         var = "0"
        #     elif number == "0":
        #         var = " 1"
        #     else:
        #         var = " s("+str(cont)+")"
        #         cont+=1
        # else:
        #     var = " s("+str(cont)+")"
        #     cont+=1
        
        pos = instr.find("=")
        #new = instr[:pos+1]+var
        new = instr[:pos+1]+" s("+str(cont)+")"
        cont+=1
    elif instr.find("xor(",0)!=-1:
        pos = instr.find("=")
        new = instr[:pos+1]+" s("+str(cont)+")"
        cont+=1
    elif instr.find("gs(",0)!=-1:
        pos = instr.find("=")
        new = "l("+instr[:pos].strip()+") "+instr[pos:]
    elif instr.find("gl =",0)!=-1:
        pos = instr.find("=")
        new = "l("+instr[:pos].strip()+") "+instr[pos:]
    elif instr.find("ls(",0)!=-1:
        pos = instr.find("=")
        new = "l("+instr[:pos].strip()+") "+instr[pos:]
    elif instr.find("ll =",0)!=-1:
        pos = instr.find("=")
        new = "l("+instr[:pos].strip()+") "+instr[pos:]        
    elif instr.find("fresh",0)!=-1:
        pos = instr.find("=")
        new = instr[:pos+1]+" s("+str(cont)+")"
        cont+=1
    elif instr.find("= eq",0)!=-1:
        pos = instr.find("=")
        new = instr[:pos+1]+" s("+str(cont)+")"
        cont+=1
    elif instr.find("= lt",0)!=-1:
        pos = instr.find("=")
        new = instr[:pos+1]+" s("+str(cont)+")"
        cont+=1
    elif instr.find("= gt",0)!=-1:
        pos = instr.find("=")
        new = instr[:pos+1]+" s("+str(cont)+")"
        cont+=1
    elif instr.find("g(",0)!=-1:
        pos = instr.find("=",0)
        posI = instr.find("g(",0)
        if posI <pos: #field var in the left
            if st_vars ==[]:
                new = "field(g"+instr[posI+2:]
            else:
                new = "field("+instr[posI+2:]
        else:
            if st_vars ==[]:
                new = instr[:pos+1]+" field(g"+instr[posI+2:]
            else:
                new = instr[:pos+1]+" field("+instr[posI+2:]
    elif instr.find("^",0)!=-1:
        pos = instr.find("=",0)
        new = instr[:pos+1]+" s("+str(cont)+")"
        cont+=1
    elif instr.find("byte",0)!=-1: # upper bound-> 255
        pos = instr.find("=",0)
        new = instr[:pos+1]+" 255"
    elif instr.find("sha3",0)!=-1:
        pos = instr.find("=",0)
        new = instr[:pos+1]+" s("+str(cont)+")"
        cont+=1
    elif instr.find("*")!=-1:
        nop = new_instructions[-1].strip(")")
        idx = nop.find("nop(PUSH")
        if(idx !=-1 and int(nop[idx+8:])<10):
            posEq = instr.find("=")
            var = instr[:posEq].strip()
            limit = int(new_instructions[-2].split("=")[1].strip())
            if limit < 1000:
                s_list = [var for i in range(limit)]
                new_aux = "+".join(s_list)
                new = var+" = "+new_aux
            else:
                new = instr
        else:
            new = instr

    elif instr.find("shl")!=-1:
        pos = instr.find("=")
        var = " s("+str(cont)+")"
        new = instr[:pos+1]+var
        cont+=1

    elif instr.find("shr")!=-1:
        pos = instr.find("=")
        var = " s("+str(cont)+")"
        new = instr[:pos+1]+var
        cont+=1

    elif instr.find("sar")!=-1:
        pos = instr.find("=")
        var = " s("+str(cont)+")"
        new = instr[:pos+1]+var
        cont+=1

    elif instr.find("extcodehash",0)!=-1:
        pos = instr.find("=",0)
        new = instr[:pos+1]+" s("+str(cont)+")"
        cont+=1
        
    elif instr.find("nop(MLOAD)")!=-1:
        top = new_instructions.pop()
        val = top.split("=")[0].strip()
        if val.startswith("s("):
            new = "'$acquire'(noncu,("+val+"+32)/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new_instructions.append(top)
            new = instr
    elif instr.find("nop(MSTORE)")!=-1:
        top = new_instructions.pop()
        val = top.split("=")
        val_1 = val[0].strip()
        val_2 = val[1].strip()
        if val_1.startswith("l(ls") and val_2.startswith("s("):
            new = "'$acquire'(noncu,("+val_2+"+32)/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new_instructions.append(top)
            new = instr
        elif not val_1.startswith("l(ls"):
            index = new_instructions[-2]
            val = index.split("=")[0].strip()
            new = "'$acquire'(noncu,("+val+"+32)/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new_instructions.append(top)
            new = instr
    elif instr.find("nop(MSTORE8)")!=-1:
        top = new_instructions.pop()
        val = top.split("=")
        val_1 = val[0].strip()
        val_2 = val[1].strip()
        if val_1.startswith("l(ls") and val_2.startswith("s("):
            new = "'$acquire'(noncu,("+val_2+"+1)/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new_instructions.append(top)
            new = instr
        elif not val_1.startswith("l(ls"):
            index = new_instructions[-2]
            val = index.split("=")[0].strip()
            new = "'$acquire'(noncu,("+val+"+1)/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new_instructions.append(top)
            new = instr
    elif instr.find("nop(SHA3)")!=-1:
        top = new_instructions.pop()
        val = top.split("=")[0].strip()
        if val.startswith("s("):
            num = val.split("(")[1].strip(")")
            num_var = int(num)
            exp = "s("+str(num_var+1)+")+"+val
            new = "'$acquire'(noncu,("+exp+")/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new_instructions.append(top)
            new = instr
    elif instr.find("nop(CALLDATACOPY)")!=-1 or instr.find("nop(CODECOPY)")!=-1 or instr.find("nop(RETURNDATACOPY)")!=-1:
        top = new_instructions[-3]
        val = top.split("=")[0].strip()
        if val.startswith("s("):
            num = val.split("(")[1].strip(")")
            num_var = int(num)
            exp = "s("+str(num_var-2)+")+"+val
            new = "'$acquire'(noncu,("+exp+")/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new = instr
    elif instr.find("nop(EXTCODECOPY)")!=-1:
        top = new_instructions[-3]
        val = top.split("=")[0].strip()
        if val.startswith("s("):
            num = val.split("(")[1].strip(")")
            num_var = int(num)
            exp = "s("+str(num_var-1)+")+"+"s("+str(num_var-3)+")"
            new = "'$acquire'(noncu,("+exp+")/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new = instr
    elif instr.find("nop(LOG1)")!=-1 or instr.find("nop(LOG2)")!=-1 or instr.find("nop(LOG3)")!=-1 or instr.find("nop(LOG4)")!=-1:
        top = new_instructions[-3]
        val = top.split("=")[0].strip()
        if val.startswith("s("):
            num = val.split("(")[1].strip(")")
            num_var = int(num)
            exp = "s("+str(num_var-1)+")+"+val
            new = "'$acquire'(noncu,("+exp+")/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new = instr
    elif instr.find("nop(RETURN)")!=-1 or instr.find("nop(REVERT)")!=-1:
        top = new_instructions[-3]
        val = top.split("=")[0].strip()
        if val.startswith("s("):
            num = val.split("(")[1].strip(")")
            num_var = int(num)
            exp = "s("+str(num_var-1)+")+"+val
            new = "'$acquire'(noncu,("+exp+")/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new = instr
    elif instr.find("nop(CALL)")!=-1:
        top = new_instructions[-3]
        last = new_instructions.pop()
        val = top.split("=")[0].strip()
        if val.startswith("s("):
            num = val.split("(")[1].strip(")")
            num_var = int(num)
            exp = "s("+str(num_var-3)+")+"+"s("+str(num_var-4)+")"
            new = "'$acquire'(noncu,("+exp+")/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            exp = "s("+str(num_var-5)+")+"+"s("+str(num_var-6)+")"
            new = "'$acquire'(noncu,("+exp+")/32)"
            new_instructions.append(new)
            new = "'$release'(noncu)"
            new_instructions.append(new)
            new_instructions.append(last)
            new = instr

                
    elif len(instr.split("=")) > 1:
        slices = instr.split("=")
        name = slices[1].strip()
        if not name.startswith("s("):
            if(name in contract_vars or name[:name.find("(")] in contract_vars):
                new = slices[0]+"= l("+name+")"
            else:
                new = instr
        else:
            new = instr
            
    elif instr.find("skip")!=-1:
        new = ""
            
    else:
        new = instr
            
    new_instructions.append(new)
        
    return cont

def compute_string_pattern(new_instructions):
    nop_inst = map(lambda x: "nop("+x+")",pattern)
    new_instructions = new_instructions+nop_inst
    return new_instructions

#pattern PUSH1 DUP1 SWAP2 DIV MUL
def check_mul_div_pattern(new_instructions,instructions,idx):
    if len(new_instructions)>=7:
        swap2 = new_instructions[-1]
        dup1 = new_instructions[-5]
        push1 = new_instructions[-7]
        mul = instructions[idx+3]
        if swap2 == "nop(SWAP2)" and dup1 == "nop(DUP1)" and push1 == "nop(PUSH1)" and mul == "nop(MUL)":
            div_ins = instructions[idx].split("/")[0].strip()
            mul_ins = instructions[idx+2].split("*")[0].strip()
            new_instructions.append(div_ins)
            new_instructions.append(instructions[idx+1])
            new_instructions.append(mul_ins)
            new_instructions.append(mul)
            idx = idx+4
        else:
            new_instructions.append(instructions[idx])
            idx = idx+1
    else:
        new_instructions.append(instructions[idx])
        idx = idx+1
    return idx

def write(rules,execution,cname):
    
    # if "costabs" not in os.listdir("/tmp/"):
    #     os.mkdir("/tmp/costabs/")

    if execution == None:
        name = costabs_path+"rbr_saco.rbr"
    elif cname == None:
        name = costabs_path+"rbr"+str(execution)+"_saco.rbr"
    else:
        name = costabs_path+cname+"_saco.rbr"
    with open(name,"w") as f:
        for rule in rules:
            f.write(rule+"\n")

    f.close()
