Refactor analysis to work with smt abstraction

mythril/analysis/callgraph.py

@@ -2,7 +2,8 @@ import re
 
 from jinja2 import Environment, PackageLoader, select_autoescape
 from mythril.laser.ethereum.svm import NodeFlags
-import z3
+from z3 import Z3Exception
+from mythril.laser.smt import simplify
 
 default_opts = {
     "autoResize": True,
@@ -174,8 +175,8 @@ def extract_edges(statespace):
             label = ""
         else:
             try:
-                label = str(z3.simplify(edge.condition)).replace("\n", "")
+                label = str(simplify(edge.condition)).replace("\n", "")
-            except z3.Z3Exception:
+            except Z3Exception:
                 label = str(edge.condition).replace("\n", "")
 
         label = re.sub(

mythril/analysis/ops.py

@@ -1,4 +1,4 @@
-from z3 import *
+from mythril.laser.smt import simplify
 from enum import Enum
 from mythril.laser.ethereum import util
 

mythril/analysis/solver.py

@@ -1,4 +1,5 @@
-from z3 import Solver, simplify, sat, unknown, FuncInterp, UGE, Optimize
+from z3 import sat, unknown, FuncInterp
+from mythril.laser.smt import simplify, UGE, Optimize, symbol_factory
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
@@ -8,7 +9,7 @@ import logging
 
 def get_model(constraints, minimize=(), maximize=()):
     s = Optimize()
-    s.set("timeout", 100000)
+    s.set_timeout(100000)
 
     for constraint in constraints:
         if type(constraint) == bool and not constraint:
@@ -82,7 +83,7 @@ def get_transaction_sequence(global_state, constraints):
         if not isinstance(transaction, ContractCreationTransaction):
             transactions.append(transaction)
             # Constrain calldatasize
-            max_calldatasize = 5000
+            max_calldatasize = symbol_factory.BitVecVal(5000, 256)
             tx_constraints.append(
                 UGE(max_calldatasize, transaction.call_data.calldatasize)
             )
@@ -114,10 +115,10 @@ def get_transaction_sequence(global_state, constraints):
         )
 
         concrete_transactions[tx_id]["call_value"] = (
-            "0x%x" % model.eval(transaction.call_value, model_completion=True).as_long()
+            "0x%x" % model.eval(transaction.call_value.raw, model_completion=True).as_long()
         )
         concrete_transactions[tx_id]["caller"] = "0x" + (
-            "%x" % model.eval(transaction.caller, model_completion=True).as_long()
+            "%x" % model.eval(transaction.caller.raw, model_completion=True).as_long()
         ).zfill(40)
 
     return concrete_transactions

mythril/analysis/traceexplore.py

@@ -1,4 +1,5 @@
-from z3 import Z3Exception, simplify
+from z3 import Z3Exception
+from mythril.laser.smt import simplify
 from mythril.laser.ethereum.svm import NodeFlags
 import re