refactor analysis modules to work with smt abstraction

mythril/analysis/modules/delegatecall.py

@@ -3,7 +3,6 @@ from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT
 from mythril.analysis.ops import get_variable, VarType
 from mythril.analysis.report import Issue
 from mythril.analysis.modules.base import DetectionModule
-import logging
 
 
 class DelegateCallModule(DetectionModule):

mythril/analysis/modules/dependence_on_predictable_vars.py

@@ -1,5 +1,4 @@
 import re
-from z3 import *
 from mythril.analysis.ops import VarType
 from mythril.analysis import solver
 from mythril.analysis.report import Issue

mythril/analysis/modules/ether_thief.py

@@ -5,7 +5,7 @@ from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.analysis.modules.base import DetectionModule
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.exceptions import UnsatError
-from z3 import BitVecVal, UGT, Sum
+from mythril.laser.smt import symbol_factory, UGT, Sum, BVAddNoOverflow
 import logging
 from copy import copy
 
@@ -33,7 +33,7 @@ def _analyze_state(state):
     call_value = state.mstate.stack[-3]
     target = state.mstate.stack[-2]
 
-    eth_sent_total = BitVecVal(0, 256)
+    eth_sent_total = symbol_factory.BitVecVal(0, 256)
 
     constraints = copy(node.constraints)
 

mythril/analysis/modules/external_calls.py

@@ -1,8 +1,8 @@
-from z3 import *
 from mythril.analysis.report import Issue
 from mythril.analysis import solver
 from mythril.analysis.swc_data import REENTRANCY
 from mythril.analysis.modules.base import DetectionModule
+from mythril.laser.smt import UGT, symbol_factory
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.exceptions import UnsatError
 import logging
@@ -27,7 +27,7 @@ def _analyze_state(state):
     try:
         constraints = node.constraints
         transaction_sequence = solver.get_transaction_sequence(
-            state, constraints + [UGT(gas, BitVecVal(2300, 256))]
+            state, constraints + [UGT(gas, symbol_factory.BitVecVal(2300, 256))]
         )
 
         # Check whether we can also set the callee address

mythril/analysis/modules/integer.py

@@ -1,12 +1,12 @@
-from z3 import *
 from mythril.analysis import solver
-from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.taint_analysis import TaintRunner
 from mythril.analysis.modules.base import DetectionModule
-import re
+
+from mythril.laser.smt import BVAddNoOverflow, BVSubNoUnderflow, BVMulNoOverflow, BitVec, symbol_factory, Not
+
 import copy
 import logging
 
@@ -64,15 +64,15 @@ class IntegerOverflowUnderflowModule(DetectionModule):
 
         # An integer overflow is possible if op0 + op1 or op0 * op1 > MAX_UINT
         # Do a type check
-        allowed_types = [int, BitVecRef, BitVecNumRef]
+        allowed_types = [int, BitVec]
         if not (type(op0) in allowed_types and type(op1) in allowed_types):
             return issues
 
         # Change ints to BitVec
         if type(op0) is int:
-            op0 = BitVecVal(op0, 256)
+            op0 = symbol_factory.BitVecVal(op0, 256)
         if type(op1) is int:
-            op1 = BitVecVal(op1, 256)
+            op1 = symbol_factory.BitVecVal(op1, 256)
 
         # Formulate expression
         # FIXME: handle exponentiation
@@ -176,7 +176,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 )
             )
 
-            allowed_types = [int, BitVecRef, BitVecNumRef]
+            allowed_types = [int, BitVec]
 
             if type(op0) in allowed_types and type(op1) in allowed_types:
                 constraints.append(Not(BVSubNoUnderflow(op0, op1, signed=False)))

mythril/analysis/modules/suicide.py

@@ -1,5 +1,4 @@
 from mythril.analysis import solver
-from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT
 from mythril.exceptions import UnsatError

tests/testdata/input_contracts/suicide.sol

@@ -1,4 +1,3 @@
-pragma solidity 0.5.0;
 
 
 contract Suicide {
@@ -7,4 +6,4 @@ contract Suicide {
     selfdestruct(addr);
   }
 
-}
+}