Make calldata compatible with partial abstraction, and add missing features to smt

mythril/analysis/modules/integer.py

@@ -5,7 +5,14 @@ from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.taint_analysis import TaintRunner
 from mythril.analysis.modules.base import DetectionModule
 
-from mythril.laser.smt import BVAddNoOverflow, BVSubNoUnderflow, BVMulNoOverflow, BitVec, symbol_factory, Not
+from mythril.laser.smt import (
+    BVAddNoOverflow,
+    BVSubNoUnderflow,
+    BVMulNoOverflow,
+    BitVec,
+    symbol_factory,
+    Not,
+)
 
 import copy
 import logging

mythril/analysis/solver.py

@@ -115,7 +115,8 @@ def get_transaction_sequence(global_state, constraints):
         )
 
         concrete_transactions[tx_id]["call_value"] = (
-            "0x%x" % model.eval(transaction.call_value.raw, 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.raw, model_completion=True).as_long()

mythril/laser/ethereum/call.py

@@ -60,7 +60,9 @@ def get_call_parameters(
 
 
 def get_callee_address(
-    global_state: GlobalState, dynamic_loader: DynLoader, symbolic_to_address: Expression
+    global_state: GlobalState,
+    dynamic_loader: DynLoader,
+    symbolic_to_address: Expression,
 ):
     """
     Gets the address of the callee

mythril/laser/ethereum/instructions.py

@@ -86,9 +86,7 @@ class StateTransition(object):
             value = global_state.current_transaction.gas_limit.value
             if value is None:
                 return
-            global_state.current_transaction.gas_limit = (
+            global_state.current_transaction.gas_limit = value
-                value
-            )
         if (
             global_state.mstate.min_gas_used
             >= global_state.current_transaction.gas_limit
@@ -139,7 +137,6 @@ class Instruction:
             op = "swap"
         elif self.op_code.startswith("LOG"):
             op = "log"
-        print(global_state.get_current_instruction())
         instruction_mutator = (
             getattr(self, op + "_", None)
             if not post

mythril/laser/ethereum/keccak.py

@@ -1,5 +1,6 @@
 from mythril.laser.smt import Expression
 
+
 class KeccakFunctionManager:
     def __init__(self):
         self.keccak_expression_mapping = {}

mythril/laser/ethereum/state/calldata.py

@@ -9,6 +9,7 @@ from mythril.laser.ethereum.util import get_concrete_int
 from z3 import Model
 from z3.z3types import Z3Exception
 
+
 class CalldataType(Enum):
     CONCRETE = 1
     SYMBOLIC = 2
@@ -142,22 +143,26 @@ class SymbolicCalldata(BaseCalldata):
         Initializes the SymbolicCalldata object
         :param tx_id: Id of the transaction that the calldata is for.
         """
-        self._size = BitVec(str(tx_id) + "_calldatasize", 256)
+        self._size = symbol_factory.BitVecSym(str(tx_id) + "_calldatasize", 256)
-        self._calldata = Array(
+        self._calldata = Array("{}_calldata".format(tx_id), 256, 8)
-            "{}_calldata".format(tx_id), 256, 8
-        )
         super().__init__(tx_id)
 
     def _load(self, item: Union[int, Expression]) -> Any:
         item = symbol_factory.BitVecVal(item, 256) if isinstance(item, int) else item
-        return simplify(If(item < self._size, simplify(self._calldata[item]), 0))
+        return simplify(
+            If(
+                item < self._size,
+                simplify(self._calldata[item]),
+                symbol_factory.BitVecVal(0, 8),
+            )
+        )
 
     def concrete(self, model: Model) -> list:
-        concrete_length = get_concrete_int(model.eval(self.size, model_completion=True))
+        concrete_length = model.eval(self.size.raw, model_completion=True).as_long()
         result = []
         for i in range(concrete_length):
             value = self._load(i)
-            c_value = get_concrete_int(model.eval(value, model_completion=True))
+            c_value = model.eval(value.raw, model_completion=True).as_long()
             result.append(c_value)
 
         return result

mythril/laser/ethereum/state/memory.py

@@ -1,6 +1,14 @@
 from typing import Union
 from z3 import Z3Exception
-from mythril.laser.smt import BitVec, symbol_factory, If, Concat, simplify, Bool, Extract
+from mythril.laser.smt import (
+    BitVec,
+    symbol_factory,
+    If,
+    Concat,
+    simplify,
+    Bool,
+    Extract,
+)
 from mythril.laser.ethereum import util
 
 
@@ -36,9 +44,7 @@ class Memory:
             assert result.size() == 256
             return result
 
-    def write_word_at(
+    def write_word_at(self, index: int, value: Union[int, BitVec, bool, Bool]) -> None:
-        self, index: int, value: Union[int, BitVec, bool, Bool]
-    ) -> None:
         """
         Writes a 32 byte word to memory at the specified index`
         :param index: index to write to
@@ -58,7 +64,11 @@ class Memory:
             self[index : index + 32] = _bytes
         except (Z3Exception, AttributeError):  # BitVector or BoolRef
             if isinstance(value, Bool):
-                value_to_write = If(value, symbol_factory.BitVecVal(1, 256), symbol_factory.BitVecVal(0, 256))
+                value_to_write = If(
+                    value,
+                    symbol_factory.BitVecVal(1, 256),
+                    symbol_factory.BitVecVal(0, 256),
+                )
             else:
                 value_to_write = value
             assert value_to_write.size() == 256

mythril/laser/ethereum/taint_analysis.py

@@ -8,6 +8,7 @@ from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.analysis.symbolic import SymExecWrapper
 from mythril.laser.smt import Expression
 
+
 class TaintRecord:
     """
     TaintRecord contains tainting information for a specific (state, node)

mythril/laser/smt/__init__.py

@@ -8,11 +8,16 @@ from mythril.laser.smt.bitvec import (
     URem,
     SRem,
     UDiv,
+    UGE,
+    Sum,
+    BVAddNoOverflow,
+    BVMulNoOverflow,
+    BVSubNoUnderflow,
 )
 from mythril.laser.smt.expression import Expression, simplify
 from mythril.laser.smt.bool import Bool, is_true, is_false, Or, Not
 from mythril.laser.smt.array import K, Array, BaseArray
-from mythril.laser.smt.solver import Solver
+from mythril.laser.smt.solver import Solver, Optimize
 
 import z3
 

mythril/laser/smt/bitvec.py

@@ -57,6 +57,8 @@ class BitVec(Expression):
 
     def __and__(self, other: "BV") -> "BV":
         """ Create an and expression """
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, 256))
         union = self.annotations + other.annotations
         return BitVec(self.raw & other.raw, annotations=union)
 
@@ -99,6 +101,12 @@ class BitVec(Expression):
 
 def If(a: Bool, b: BitVec, c: BitVec):
     """ Create an if-then-else expression """
+    if not isinstance(a, Expression):
+        a = Bool(z3.BoolVal(a))
+    if not isinstance(b, Expression):
+        b = BitVec(z3.BitVecVal(b, 256))
+    if not isinstance(c, Expression):
+        c = BitVec(z3.BitVecVal(c, 256))
     union = a.annotations + b.annotations + c.annotations
     return BitVec(z3.If(a.raw, b.raw, c.raw), union)
 
@@ -109,6 +117,11 @@ def UGT(a: BitVec, b: BitVec) -> Bool:
     return Bool(z3.UGT(a.raw, b.raw), annotations)
 
 
+def UGE(a: BitVec, b:BitVec) -> Bool:
+    annotations = a.annotations + b.annotations
+    return Bool(z3.UGE(a.raw, b.raw), annotations)
+
+
 def ULT(a: BitVec, b: BitVec) -> Bool:
     """ Create an unsigned less than expression """
     annotations = a.annotations + b.annotations
@@ -159,3 +172,20 @@ def Sum(*args) -> BitVec:
     for bv in args:
         annotations += bv.annotations
     return BitVec(nraw, annotations)
+
+
+def BVAddNoOverflow(a: BitVec, b: BitVec, signed: bool) -> Bool:
+    return Bool(z3.BVAddNoOverflow(a.raw, b.raw, signed))
+
+
+def BVMulNoOverflow(a: BitVec, b: BitVec, signed: bool) -> Bool:
+    return Bool(z3.BVMulNoOverflow(a.raw, b.raw, signed))
+
+
+def BVSubNoUnderflow(a: BitVec, b: BitVec, signed: bool) -> Bool:
+    if not isinstance(a, Expression):
+        a = BitVec(z3.BitVecVal(a, 256))
+    if not isinstance(b, Expression):
+        b = BitVec(z3.BitVecVal(b, 256))
+
+    return Bool(z3.BVSubNoUnderflow(a.raw, b.raw, signed))

mythril/laser/smt/bool.py

@@ -48,6 +48,7 @@ class Bool(Expression):
         if self.value is not None:
             return self.value
         else:
+            return False
             raise AttributeError("Can not evalutate symbolic bool value")
 
 def Or(a: Bool, b: Bool):

mythril/laser/smt/expression.py

@@ -26,6 +26,9 @@ class Expression:
         """ Simplifies this expression """
         self.raw = z3.simplify(self.raw)
 
+    def __repr__(self):
+        return self.raw.__repr__()
+
 
 def simplify(expression: Expression):
     """ Simplifies the expression """

mythril/laser/smt/solver.py

@@ -1,5 +1,6 @@
 import z3
 from mythril.laser.smt.bool import Bool
+from mythril.laser.smt.expression import Expression
 
 
 class Solver:
@@ -16,11 +17,17 @@ class Solver:
 
     def add(self, constraints: list) -> None:
         """ Adds the constraints to this solver """
+        if not isinstance(constraints, list):
+            self.raw.add(constraints.raw)
+            return
         constraints = [c.raw for c in constraints]
         self.raw.add(constraints)
 
     def append(self, constraints: list) -> None:
         """ Adds the constraints to this solver """
+        if not isinstance(constraints, list):
+            self.raw.append(constraints.raw)
+            return
         constraints = [c.raw for c in constraints]
         self.raw.add(constraints)
 
@@ -35,3 +42,15 @@ class Solver:
 
     def pop(self, num) -> None:
         self.raw.pop(num)
+
+
+class Optimize(Solver):
+    def __init__(self):
+        super().__init__()
+        self.raw = z3.Optimize()
+
+    def minimize(self, element: Expression):
+        self.raw.minimize(element.raw)
+
+    def maximize(self, element: Expression):
+        self.raw.maximize(element.raw)