Add debugging code

mythril/analysis/modules/call_to_dynamic_with_gas.py

@@ -13,6 +13,8 @@ Check for call.value()() to an untrusted address
 
 def execute(statespace):
 
+    logging.debug("Executing module: CALL_TO_DYNAMIC_WITH_GAS")
+
     issues = []
 
     for call in statespace.calls:

mythril/analysis/modules/delegatecall_forward.py

@@ -2,6 +2,7 @@ from z3 import *
 import re
 from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
+import logging
 
 
 '''
@@ -12,6 +13,8 @@ Check for invocations of delegatecall(msg.data) in the fallback function.
 
 def execute(statespace):
 
+    logging.debug("Executing module: DELEGATECALL_FORWARD")
+
     issues = []
     visited = []
 

mythril/analysis/modules/delegatecall_to_dynamic.py

@@ -13,6 +13,8 @@ Check for invocations of delegatecall/callcode to a user-supplied address
 
 def execute(statespace):
 
+    logging.debug("Executing module: DELEGATECALL_TO_DYNAMIC")
+
     issues = []
 
     for call in statespace.calls:

mythril/analysis/modules/ether_send.py

@@ -17,6 +17,8 @@ to that index).
 
 def execute(statespace):
 
+    logging.debug("Executing module: ETHER_SEND")
+
     issues = []
 
     for call in statespace.calls:

mythril/analysis/modules/integer_overflow.py

@@ -15,11 +15,12 @@ UINT_MAX = BitVecVal(2 ** 256 - 1, 256)
 MODULE DESCRIPTION:
 
 Check for integer overflows.
-Checks ADD instruction, MUL still todo
 '''
 
 def execute(statespace):
 
+    logging.debug("Executing module: INTEGER_OVERFLOW")
+
     issues = []
 
     for k in statespace.nodes:

mythril/analysis/modules/integer_underflow.py

@@ -16,6 +16,8 @@ For every SUB instruction, check if there's a possible state where op1 > op0.
 
 def execute(statespace):
 
+    logging.debug("Executing module: INTEGER_UNDERFLOW")
+
     issues = []
 
     for k in statespace.nodes:

mythril/analysis/modules/tx_origin.py

@@ -1,5 +1,6 @@
 from mythril.analysis.report import Issue
 import re
+import logging
 
 
 '''
@@ -10,6 +11,8 @@ Check for constraints on tx.origin (i.e., access to some functionality is restri
 
 def execute(statespace):
 
+    logging.debug("Executing module: TX_ORIGIN")
+
     issues = []
 
     for k in statespace.nodes:

mythril/analysis/modules/unchecked_retval.py

@@ -26,6 +26,8 @@ For low-level-calls this check is omitted. E.g.:
 
 def execute(statespace):
 
+    logging.debug("Executing module: UNCHECKED_RETVAL")
+
     issues = []
     visited = []
 

mythril/analysis/modules/unchecked_suicide.py

@@ -17,6 +17,8 @@ Check for SUICIDE instructions that either can be reached by anyone, or where ms
 
 def execute(statespace):
 
+    logging.debug("Executing module: UNCHECKED_SUICIDE")
+
     issues = []
 
     for k in statespace.nodes:

mythril/analysis/modules/weak_random.py

@@ -20,6 +20,9 @@ TODO:
 
 
 def execute(statespace):
+
+    logging.debug("Executing module: WEAK_RANDOM")
+
     issues = []
 
     for call in statespace.calls:

mythril/analysis/symbolic.py

@@ -92,6 +92,8 @@ class StateSpace:
                         break
 
                 if taint:
+                    s.tainted = True
+
                     try:
                         solver.get_model(s.node.constraints)
                         s.tainted = True

requirements.txt

@@ -2,6 +2,6 @@ ethereum>=2.0.4
 ZODB>=5.3.0
 z3-solver>=4.5
 web3
-laser-ethereum==0.2.21
+laser-ethereum==0.3.0
 requests
 BTrees

setup.py

@@ -254,7 +254,7 @@ Credit
 setup(
     name='mythril',
 
-    version='0.8.25',
+    version='0.8.26',
 
     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.2.21',
+        'laser-ethereum==0.3.0',
         'requests',
         'BTrees'
     ],