LASER v2 compatibility fixes & code formatting

myth

@@ -368,7 +368,7 @@ elif (args.graph) or (args.fire_lasers):
         else:
             states = StateSpace(contracts, max_depth=args.max_depth)
         # except:
-        #    exitWithError(args.outform, "Symbolic exection error: " + str(e))
+        #    exitWithError(args.outform, "Symbolic execution error: " + str(e))
 
         if args.enable_physics is not None:
             physics = True
@@ -388,13 +388,13 @@ elif (args.graph) or (args.fire_lasers):
 
         for contract in contracts:
 
-            try:
+            #try:
             if (args.dynld):
                 states = StateSpace([contract], dynloader=DynLoader(eth), max_depth=args.max_depth)
             else:
                 states = StateSpace([contract], max_depth=args.max_depth)
-            except Exception as e:
-                exitWithError(args.outform, "Symbolic exection error: " + str(e))        
+            #except Exception as e:
+            #    exitWithError(args.outform, "Symbolic exection error: " + str(e))        
 
             issues = fire_lasers(states)
 

mythril/analysis/modules/delegatecall_forward.py

@@ -11,6 +11,7 @@ MODULE DESCRIPTION:
 Check for invocations of delegatecall(msg.data) in the fallback function.
 '''
 
+
 def execute(statespace):
 
     logging.debug("Executing module: DELEGATECALL_FORWARD")
@@ -29,15 +30,15 @@ def execute(statespace):
 
         if (call.type == "DELEGATECALL") and (call.node.function_name == "fallback"):
 
-            stack = call.state.stack
+            stack = call.state.mstate.stack
 
             meminstart = get_variable(stack[-3])
 
             if meminstart.type == VarType.CONCRETE:
 
-                if (re.search(r'calldata.*_0', str(call.state.memory[meminstart.val]))):
+                if (re.search(r'calldata.*_0', str(call.state.mstate.memory[meminstart.val]))):
 
-                    issue = Issue(call.node.module_name, call.node.function_name, call.addr, "CALLDATA forwarded with delegatecall()", "Informational")
+                    issue = Issue(call.node.contract_name, call.node.function_name, call.addr, "CALLDATA forwarded with delegatecall()", "Informational")
 
                     issue.description = \
                         "This contract forwards its calldata via DELEGATECALL in its fallback function. " \

mythril/analysis/modules/delegatecall_to_dynamic.py

@@ -45,7 +45,7 @@ def execute(statespace):
                                 if s.tainted:
                                     issue = Issue(call.type + " to dynamic address in storage", "Warning")
                                     issue.description = \
-                                        "The function " + call.node.function_name + " in contract '" + call.node.module_name + " delegates execution to a contract address stored in a state variable. " \
+                                        "The function " + call.node.function_name + " in contract '" + call.node.contract_name + " delegates execution to a contract address stored in a state variable. " \
                                         "There is a check on storage index " + str(index) + ". This storage index can be written to by calling the function '" + s.node.function_name + "'.\n" \
                                         "Make sure that the contract address cannot be set by untrusted users."
                                     issues.append(issue)
@@ -56,10 +56,10 @@ def execute(statespace):
 
                     else:
 
-                        issue = Issue(call.node.module_name, call.node.function_name, call.addr, "DELEGATECALL to dynamic address", "Informational")
+                        issue = Issue(call.node.contract_name, call.node.function_name, call.addr, "DELEGATECALL to dynamic address", "Informational")
 
                         issue.description = \
-                            "The function " + call.node.function_name + " in contract '" + call.node.module_name + " delegates execution to a contract with a dynamic address." \
+                            "The function " + call.node.function_name + " in contract '" + call.node.contract_name + " delegates execution to a contract with a dynamic address." \
                             "To address:" + str(call.to)
 
                         issues.append(issue)

mythril/analysis/modules/depreciated_ops.py

@@ -9,6 +9,7 @@ MODULE DESCRIPTION:
 Check for constraints on tx.origin (i.e., access to some functionality is restricted to a specific origin).
 '''
 
+
 def execute(statespace):
 
     logging.debug("Executing module: DEPRECIATED OPCODES")
@@ -24,7 +25,7 @@ def execute(statespace):
 
             if(instruction['opcode'] == "ORIGIN"):
 
-                issue = Issue(node.contract_name, node.function_name, instruction['address'],  "Use of tx.origin", "Warning", \
+                issue = Issue(node.contract_name, node.function_name, instruction['address'], "Use of tx.origin", "Warning",
                     "Function " + node.function_name + " retrieves the transaction origin (tx.origin) using the ORIGIN opcode. Use tx.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin"
                 )
 

mythril/analysis/modules/suicide.py

@@ -7,7 +7,6 @@ import re
 import logging
 
 
-
 '''
 MODULE DESCRIPTION:
 
@@ -15,6 +14,7 @@ Check for SUICIDE instructions that either can be reached by anyone, or where ms
 (i.e. there's a write to that index is unconstrained by msg.sender).
 '''
 
+
 def execute(statespace):
 
     logging.debug("Executing module: UNCHECKED_SUICIDE")
@@ -34,8 +34,8 @@ def execute(statespace):
 
                 description = "The function " + node.function_name + " executes the SUICIDE instruction."
 
-                state = node.states[instruction['address']]
-                to = state.stack.pop()
+                stack = copy.deepcopy(state.mstate.stack)
+                to = stack.pop()
 
                 if ("caller" in str(to)):
                     description += "\nThe remaining Ether is sent to the caller's address.\n"

mythril/analysis/ops.py

@@ -20,33 +20,29 @@ class Variable:
 
 class Op:
 
-    def __init__(self, node, addr):
+    def __init__(self, node, state, addr):
         self.node = node
+        self.state = state
         self.addr = addr
 
+
 class Call(Op):
 
-    def __init__(self, node, addr, _type, to, gas, value = Variable(0, VarType.CONCRETE), data = None):
+    def __init__(self, node, state, addr, _type, to, gas, value=Variable(0, VarType.CONCRETE), data=None):
 
-        super().__init__(node, addr)
+        super().__init__(node, state, addr)
         self.to = to
         self.gas = gas
         self.type = _type
         self.value = value
         self.data = data
 
-class Suicide(Op):
-
-    def __init__(self, node, addr, call_type, to, value):
-        super().__init__(node, addr)
-        self.to = to
 
 class SStore(Op):
 
-    def __init__(self, node, addr, value):
-        super().__init__(node, addr)
+    def __init__(self, node, state, addr, value):
+        super().__init__(node, state, addr)
         self.value = value
-        self.tainted = False
 
 
 def get_variable(i):
@@ -54,6 +50,3 @@ def get_variable(i):
         return Variable(helper.get_concrete_int(i), VarType.CONCRETE)
     except AttributeError:
         return Variable(simplify(i), VarType.SYMBOLIC)
-
-
-

mythril/analysis/symbolic.py

@@ -54,14 +54,14 @@ class StateSpace:
                                 continue
 
                         if (meminstart.type == VarType.CONCRETE and meminsz.type == VarType.CONCRETE):
-                            self.calls.append(Call(self.nodes[key], instruction['address'], op, to, gas, value, state.mstate.memory[meminstart.val:meminsz.val*4]))
+                            self.calls.append(Call(self.nodes[key], state, instruction['address'], op, to, gas, value, state.mstate.memory[meminstart.val:meminsz.val*4]))
                         else:
-                            self.calls.append(Call(self.nodes[key], instruction['address'], op, to, gas, value))                     
+                            self.calls.append(Call(self.nodes[key], state, instruction['address'], op, to, gas, value))                     
                     else:
                         gas, to, meminstart, meminsz, memoutstart, memoutsz = \
                             get_variable(stack.pop()), get_variable(stack.pop()), get_variable(stack.pop()), get_variable(stack.pop()), get_variable(stack.pop()), get_variable(stack.pop())
 
-                        self.calls.append(Call(self.nodes[key], instruction['address'], op, to, gas))
+                        self.calls.append(Call(self.nodes[key], state, instruction['address'], op, to, gas))
 
                 '''
                 elif op == 'SSTORE':

requirements.txt

@@ -2,7 +2,7 @@ ethereum>=2.0.4
 ZODB>=5.3.0
 z3-solver>=4.5
 web3
-laser-ethereum==0.5.0
+laser-ethereum==0.5.1
 requests
 BTrees
 py-solc

setup.py

@@ -254,7 +254,7 @@ Credit
 setup(
     name='mythril',
 
-    version='0.13.0',
+    version='0.13.1',
 
     description='Security analysis tool for Ethereum smart contracts',
     long_description=long_description,
@@ -291,7 +291,7 @@ setup(
         'web3',
         'ZODB>=5.3.0',
         'z3-solver>=4.5',
-        'laser-ethereum==0.5.0',
+        'laser-ethereum==0.5.1',
         'requests',
         'BTrees',
         'py-solc'