From 12ca4426d6974231fbd25a6452c6a31c3f630a21 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Wed, 12 Dec 2018 12:36:24 +0100
Subject: [PATCH] Refactor analysis to work with smt abstraction

---
 mythril/analysis/callgraph.py    |  7 ++++---
 mythril/analysis/ops.py          |  2 +-
 mythril/analysis/solver.py       | 11 ++++++-----
 mythril/analysis/traceexplore.py |  3 ++-
 4 files changed, 13 insertions(+), 10 deletions(-)

diff --git a/mythril/analysis/callgraph.py b/mythril/analysis/callgraph.py
index b5dd1ee3..e8ff62b9 100644
--- a/mythril/analysis/callgraph.py
+++ b/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", "")
-            except z3.Z3Exception:
+                label = str(simplify(edge.condition)).replace("\n", "")
+            except Z3Exception:
                 label = str(edge.condition).replace("\n", "")
 
         label = re.sub(
diff --git a/mythril/analysis/ops.py b/mythril/analysis/ops.py
index 6c3cfea1..1eb5a080 100644
--- a/mythril/analysis/ops.py
+++ b/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
 
diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 8666931d..a202beb4 100644
--- a/mythril/analysis/solver.py
+++ b/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
diff --git a/mythril/analysis/traceexplore.py b/mythril/analysis/traceexplore.py
index 6fd476aa..ef2020ad 100644
--- a/mythril/analysis/traceexplore.py
+++ b/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