Addign computation of minimal encoding length to use for memory initalization when symbolically executing the constructor.

mythril/analysis/modules/build_traces.py

@@ -1,8 +1,13 @@
 from mythril.analysis.report import Issue
 from mythril.solidnotary.transactiontrace import TransactionTrace
-from mythril.solidnotary.solidnotary import get_transaction_traces
+from mythril.disassembler.disassembly import Disassembly
+from laser.ethereum.svm import GlobalState, Account, Environment, MachineState, CalldataType
+from z3 import BitVec
+from mythril.analysis.symbolic import SymExecWrapper
+from mythril.solidnotary.solidnotary import get_transaction_traces, get_construction_traces
 from mythril.solidnotary.z3utility import  are_satisfiable
 import logging
+from mythril.solidnotary.calldata import get_minimal_constructor_param_encoding_len, abi_json_to_abi
 
 
 '''
@@ -19,23 +24,62 @@ def print_obj(obj):
     print(obj.children())
     print()
 
+def get_constr_glbstate(contract, address):
+
+    mstate = MachineState(gas=10000000)
+
+    minimal_const_byte_len = get_minimal_constructor_param_encoding_len(abi_json_to_abi(contract.abi))
+
+    # better would be to append symbolic params to the bytecode such that the codecopy instruction that copies the
+    # params into memory takes care of placing them onto the memory with the respective size.
+    for i in range(int(minimal_const_byte_len / 32)):
+        mstate.mem_extend(128 + 32 * i, 32)
+        mstate.memory.insert(128 + 32 * i, BitVec('calldata_' + contract.name + '_' + str(i * 32), 256))
+
+    # Todo Replace pure placement of enough symbolic 32 Byte-words with placement of symbolic variables that contain
+    # the name of the solidity variables
+
+    accounts = {address: Account(address, contract.disassembly, contract_name=contract.name)}
+
+    environment = Environment(
+        accounts[address],
+        BitVec("caller", 256),
+        [],
+        BitVec("gasprice", 256),
+        BitVec("callvalue", 256),
+        BitVec("origin", 256),
+        calldata_type=CalldataType.SYMBOLIC,
+    )
+
+    # Todo find source for account info, maybe the std statespace?
+
+    return GlobalState(accounts, environment, mstate)
+
 
 def execute(statespace):
 
     logging.debug("Executing module: Transaction End")
 
-    traces = []
+    constructor_trace = {}
+
+    if hasattr(statespace, "sym_constr"):
+        sym_exe_tuple = statespace.sym_constr
+        glbstate = get_constr_glbstate(sym_exe_tuple[0], sym_exe_tuple[1])
+        sym_exe_tuple = statespace.sym_constr + (glbstate,)
+        constr_statespace = SymExecWrapper(*sym_exe_tuple)
+        constructor_trace = get_construction_traces(constr_statespace) # Todo the traces here should not contain references to storages anymore
+        for t in constructor_trace:
+            t.pp_trace()
 
     traces = get_transaction_traces(statespace)
-    for trace in traces:
+    for trace in constructor_trace:
         comp_trace_lvls = trace.apply_up_to_trace_levels(traces, 3)
         for trace_lvl in comp_trace_lvls:
             for t in trace_lvl:
-                if t.lvl == 4:
                     t.pp_trace()
 
-#    for trace in traces:
-#        trace.pp_trace()
+    # for trace in traces:
+    #    trace.pp_trace()
 
     #print("==== Second level traces ====")
     #for trace in traces:

mythril/solidnotary/calldata.py

@@ -0,0 +1,150 @@
+from re import search
+from mythril.exceptions import CompilerError
+from subprocess import Popen, PIPE
+import json
+import sys
+
+class CalldataMap:
+
+    def __init__(self, abi, solc_v):
+        pass
+
+    def __init__(self, solidity_file, solc_v):
+        pass
+
+def get_minimal_param_encoding_len(abi_inputs):
+    len = 0
+    return len
+
+def get_minimal_byte_enc_len(abi_obj):
+    if type(abi_obj) == list:
+        return sum([head_byte_length_min(t) for t in abi_obj]) + sum([tail_byte_length_min(t) for t in abi_obj])
+    if type(abi_obj) == str:
+        stype = abi_obj
+    else:
+        stype = abi_obj['type']
+    if stype == 'tuple':
+        return get_minimal_byte_enc_len(abi_obj['components'])
+    try:
+        match = search(r'(?P<pre>.*)\[(?P<post>[0-9]+)\]', stype)
+        pre = match['pre']
+        post = match['post']
+        return int(post) * get_minimal_byte_enc_len(pre)
+    except (KeyError, TypeError) as e:
+        pass
+    if stype.endswith("[]"):
+        return 32
+
+    if stype == "string":
+        return 32
+    elif stype == "bytes":
+        return 32 # 2 was the smallest observed value, remix did not allow specification of zero size bytes
+    elif [stype.startswith(prefix_type) for prefix_type in ["int", "uint", "address", "bool", "fixed", "ufixed", "bytes"]]:
+        return 32
+
+def head_byte_length_min(abi_obj):
+    if is_dynamic(abi_obj):
+        return 32
+    else:
+        return get_minimal_byte_enc_len(abi_obj)
+
+
+def tail_byte_length_min(abi_obj):
+    if is_dynamic(abi_obj):
+        return get_minimal_byte_enc_len(abi_obj)
+    else:
+        return 0
+
+def get_minimal_wsize(abi_obj):
+    stype = abi_obj['type']
+    if type(stype) == list:
+        return sum(list(map(lambda a: get_minimal_wsize(a), stype)))
+    if stype in ["bytes", "string"] or stype.endswith("[]"):
+        return True
+    if stype == 'tuple':
+        return True in [is_dynamic(elem) for elem in abi_obj['components']]
+    try:
+        match = search(r'(?P<pre>.*)(?P<post>\[[0-9]+\])', stype)
+        pre = match['pre']
+        # post = match['post']
+        return is_dynamic(pre)
+    except (KeyError | TypeError):
+        pass
+    return False
+
+
+def get_minimal_constructor_param_encoding_len(abi):
+    for spec in abi:
+        try:
+            if spec['type'] == 'constructor':
+                con_inputs = spec['inputs']
+                return get_minimal_byte_enc_len(con_inputs)
+        except KeyError:
+            print("ABI does not contain inputs for constructor")
+    return -1
+
+def get_minimal_constr_param_byte_length(filename, contract_name=None):
+    abi_decoded = get_solc_abi_json(filename)
+    return get_minimal_constructor_param_encoding_len(abi_decoded)
+
+def is_dynamic(abi_obj):
+    if type(abi_obj) == list:
+        return True in list(map(lambda a: is_dynamic(a), abi_obj))
+    if type(abi_obj) == str:
+        stype = abi_obj
+    else:
+        stype = abi_obj['type']
+    if stype in ["bytes", "string"] or stype.endswith("[]"):
+        return True
+    if stype == 'tuple':
+        return True in [is_dynamic(elem) for elem in abi_obj['components']]
+    try:
+        match = search(r'(?P<pre>.*)(?P<post>\[[0-9]+\])', stype)
+        pre = match['pre']
+        # post = match['post']
+        return is_dynamic(pre)
+    except (KeyError, TypeError) as e:
+        pass
+    return False
+
+def get_solc_abi_json(file, solc_binary="solc", solc_args=None):
+
+    cmd = [solc_binary, "--abi", '--allow-paths', "."]
+
+    if solc_args:
+        cmd.extend(solc_args.split(" "))
+
+    cmd.append(file)
+
+    try:
+        p = Popen(cmd, stdout=PIPE, stderr=PIPE)
+
+        stdout, stderr = p.communicate()
+        ret = p.returncode
+
+        if ret != 0:
+            raise CompilerError("Solc experienced a fatal error (code %d).\n\n%s" % (ret, stderr.decode('UTF-8')))
+    except FileNotFoundError:
+        raise CompilerError("Compiler not found. Make sure that solc is installed and in PATH, or set the SOLC environment variable.")
+
+    out = stdout.decode("UTF-8")
+
+    if not len(out):
+        raise CompilerError("Compilation failed.")
+
+    out = out[out.index("["):]
+
+    print(out)
+
+    return json.loads(out)
+
+def abi_json_to_abi(abi_json):
+    return json.loads(abi_json)
+
+
+if __name__ == "__main__":
+    if len(sys.argv) > 1:
+        print("Size:")
+        print(get_minimal_constr_param_byte_length(sys.argv[1]))
+    else:
+        print("Error: No file specified")