Merge branch 'develop' into bugfix/665

mythril/analysis/solver.py

@@ -1,4 +1,4 @@
-from z3 import Solver, simplify, sat, unknown, FuncInterp, UGE
+from z3 import Solver, simplify, sat, unknown, FuncInterp, UGE, Optimize
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
@@ -6,12 +6,17 @@ from mythril.laser.ethereum.transaction.transaction_models import (
 import logging
 
 
-def get_model(constraints):
+def get_model(constraints, minimize=(), maximize=()):
-    s = Solver()
+    s = Optimize()
     s.set("timeout", 100000)
 
     for constraint in constraints:
         s.add(constraint)
+    for e in minimize:
+        s.minimize(e)
+    for e in maximize:
+        s.maximize(e)
+
     result = s.check()
     if result == sat:
         return s.model()
@@ -62,6 +67,7 @@ def get_transaction_sequence(global_state, constraints):
     txs = {}
     creation_tx_ids = []
     tx_constraints = constraints.copy()
+    minimize = []
 
     for transaction in transaction_sequence:
         tx_id = str(transaction.id)
@@ -74,12 +80,14 @@ def get_transaction_sequence(global_state, constraints):
                     UGE(max_calldatasize, transaction.call_data.calldatasize)
                 )
 
+            minimize.append(transaction.call_data.calldatasize)
+
             txs[tx_id] = tx_template.copy()
 
         else:
             creation_tx_ids.append(tx_id)
 
-    model = get_model(tx_constraints)
+    model = get_model(tx_constraints, minimize=minimize)
 
     for transaction in transaction_sequence:
         if not isinstance(transaction, ContractCreationTransaction):
@@ -105,7 +113,7 @@ def get_transaction_sequence(global_state, constraints):
         if "caller" in name:
             # caller is 'creator' for creation transactions
             tx_id = name.replace("caller", "")
-            caller = "0x" + ("%x" % model[d].as_long()).zfill(64)
+            caller = "0x" + ("%x" % model[d].as_long()).zfill(40)
 
             txs[tx_id]["caller"] = caller
 

mythril/laser/ethereum/instructions.py

@@ -417,7 +417,11 @@ class Instruction:
         environment = global_state.environment
         op0 = state.stack.pop()
 
-        state.stack.append(environment.calldata.get_word_at(op0))
+        value, constraints = environment.calldata.get_word_at(op0)
+
+        state.stack.append(value)
+        state.constraints.extend(constraints)
+
         return [global_state]
 
     @StateTransition()
@@ -497,7 +501,10 @@ class Instruction:
 
                 new_memory = []
                 for i in range(size):
-                    new_memory.append(environment.calldata[i_data])
+                    value, constraints = environment.calldata[i_data]
+                    new_memory.append(value)
+                    state.constraints.extend(constraints)
+
                     i_data = (
                         i_data + 1 if isinstance(i_data, int) else simplify(i_data + 1)
                     )

mythril/laser/ethereum/natives.py

@@ -1,6 +1,5 @@
 # -*- coding: utf8 -*-
 
-import copy
 import hashlib
 import logging
 
@@ -8,7 +7,8 @@ from ethereum.utils import ecrecover_to_pub
 from py_ecc.secp256k1 import N as secp256k1n
 from rlp.utils import ALL_BYTES
 
-from mythril.laser.ethereum.util import bytearray_to_int, sha3
+from mythril.laser.ethereum.util import bytearray_to_int, sha3, get_concrete_int
+from z3 import Concat, simplify
 
 
 class NativeContractException(Exception):
@@ -70,7 +70,16 @@ def ripemd160(data):
 
 
 def identity(data):
-    return copy.copy(data)
+    # Group up into an array of 32 byte words instead
+    # of an array of bytes. If saved to memory, 32 byte
+    # words are currently needed, but a correct memory
+    # implementation would be byte indexed for the most
+    # part.
+    return data
+    result = []
+    for i in range(0, len(data), 32):
+        result.append(simplify(Concat(data[i : i + 32])))
+    return result
 
 
 def native_contracts(address, data):
@@ -79,4 +88,11 @@ def native_contracts(address, data):
     """
 
     functions = (ecrecover, sha256, ripemd160, identity)
-    return functions[address - 1](data.starting_calldata)
+
+    try:
+        data = [get_concrete_int(e) for e in data._calldata]
+    except TypeError:
+        # Symbolic calldata
+        data = data._calldata
+
+    return functions[address - 1](data)

mythril/laser/ethereum/state.py

@@ -4,16 +4,15 @@ from z3 import (
     BitVecRef,
     BitVecNumRef,
     BitVecSort,
-    Solver,
     ExprRef,
     Concat,
     sat,
     simplify,
     Array,
     ForAll,
-    Solver,
-    UGT,
     Implies,
+    UGE,
+    UGT,
 )
 from z3.z3types import Z3Exception
 from mythril.disassembler.disassembly import Disassembly
@@ -45,7 +44,7 @@ class Calldata:
         :param starting_calldata: byte array representing the concrete calldata of a transaction
         """
         self.tx_id = tx_id
-        if starting_calldata:
+        if not starting_calldata is None:
             self._calldata = []
             self.calldatasize = BitVecVal(len(starting_calldata), 256)
             self.concrete = True
@@ -56,32 +55,21 @@ class Calldata:
             self.calldatasize = BitVec("{}_calldatasize".format(self.tx_id), 256)
             self.concrete = False
 
-        self.starting_calldata = starting_calldata or []
-
-    @property
-    def constraints(self):
-        constraints = []
         if self.concrete:
-            for calldata_byte in self.starting_calldata:
+            for calldata_byte in starting_calldata:
                 if type(calldata_byte) == int:
                     self._calldata.append(BitVecVal(calldata_byte, 8))
                 else:
                     self._calldata.append(calldata_byte)
-            constraints.append(self.calldatasize == len(self.starting_calldata))
-        else:
-            x = BitVec("x", 256)
-            constraints.append(
-                ForAll(x, Implies(self[x] != 0, UGT(self.calldatasize, x)))
-            )
-        return constraints
 
     def concretized(self, model):
         result = []
-
         for i in range(
             get_concrete_int(model.eval(self.calldatasize, model_completion=True))
         ):
-            result.append(get_concrete_int(model.eval(self[i], model_completion=True)))
+            result.append(
+                get_concrete_int(model.eval(self._calldata[i], model_completion=True))
+            )
 
         return result
 
@@ -103,15 +91,23 @@ class Calldata:
             except Z3Exception:
                 raise IndexError("Invalid Calldata Slice")
 
-            return simplify(Concat(dataparts))
+            values, constraints = zip(*dataparts)
+            result_constraints = []
+            for c in constraints:
+                result_constraints.extend(c)
+            return (simplify(Concat(values)), result_constraints)
 
         if self.concrete:
             try:
-                return self._calldata[get_concrete_int(item)]
+                return (self._calldata[get_concrete_int(item)], ())
             except IndexError:
-                return BitVecVal(0, 8)
+                return (BitVecVal(0, 8), ())
         else:
-            return self._calldata[item]
+            constraints = [
+                Implies(self._calldata[item] != 0, UGT(self.calldatasize, item))
+            ]
+
+            return (self._calldata[item], constraints)
 
 
 class Storage:

mythril/laser/ethereum/transaction/transaction_models.py

@@ -91,9 +91,6 @@ class MessageCallTransaction:
 
         global_state = GlobalState(self.world_state, environment, None)
         global_state.environment.active_function_name = "fallback"
-        global_state.mstate.constraints.extend(
-            global_state.environment.calldata.constraints
-        )
 
         return global_state
 
@@ -173,9 +170,6 @@ class ContractCreationTransaction:
 
         global_state = GlobalState(self.world_state, environment, None)
         global_state.environment.active_function_name = "constructor"
-        global_state.mstate.constraints.extend(
-            global_state.environment.calldata.constraints
-        )
 
         return global_state
 

tests/laser/state/calldata_test.py

@@ -2,7 +2,7 @@ import pytest
 from mythril.laser.ethereum.state import Calldata
 from z3 import Solver, simplify
 from z3.z3types import Z3Exception
-
+from mock import MagicMock
 
 uninitialized_test_data = [
     ([]),  # Empty concrete calldata
@@ -17,10 +17,12 @@ def test_concrete_calldata_uninitialized_index(starting_calldata):
     solver = Solver()
 
     # Act
-    value = calldata[100]
+    value, constraint1 = calldata[100]
-    value2 = calldata.get_word_at(200)
+    value2, constraint2 = calldata.get_word_at(200)
+
+    solver.add(constraint1)
+    solver.add(constraint2)
 
-    solver.add(calldata.constraints)
     solver.check()
     model = solver.model()
 
@@ -38,7 +40,6 @@ def test_concrete_calldata_calldatasize():
     solver = Solver()
 
     # Act
-    solver.add(calldata.constraints)
     solver.check()
     model = solver.model()
 
@@ -54,11 +55,11 @@ def test_symbolic_calldata_constrain_index():
     solver = Solver()
 
     # Act
-    constraint = calldata[100] == 50
+    value, calldata_constraints = calldata[100]
+    constraint = value == 50
 
-    value = calldata[100]
+    solver.add([constraint] + calldata_constraints)
 
-    solver.add(calldata.constraints + [constraint])
     solver.check()
     model = solver.model()
 
@@ -76,9 +77,10 @@ def test_concrete_calldata_constrain_index():
     solver = Solver()
 
     # Act
-    constraint = calldata[2] == 3
+    value, calldata_constraints = calldata[2]
+    constraint = value == 3
 
-    solver.add(calldata.constraints + [constraint])
+    solver.add([constraint] + calldata_constraints)
     result = solver.check()
 
     # Assert
@@ -88,14 +90,18 @@ def test_concrete_calldata_constrain_index():
 def test_concrete_calldata_constrain_index():
     # Arrange
     calldata = Calldata(0)
+    mstate = MagicMock()
+    mstate.constraints = []
     solver = Solver()
 
     # Act
     constraints = []
-    constraints.append(calldata[51] == 1)
+    value, calldata_constraints = calldata[51]
+    constraints.append(value == 1)
     constraints.append(calldata.calldatasize == 50)
 
-    solver.add(calldata.constraints + constraints)
+    solver.add(constraints + calldata_constraints)
+
     result = solver.check()
 
     # Assert

tests/laser/transaction/symbolic_test.py

@@ -10,9 +10,6 @@ from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.state import WorldState, Account
 import unittest.mock as mock
 from unittest.mock import MagicMock
-from mythril.laser.ethereum.transaction.symbolic import (
-    _setup_global_state_for_execution,
-)
 
 
 def _is_message_call(_, transaction):
@@ -70,25 +67,3 @@ def test_execute_contract_creation(mocked_setup: MagicMock):
     # laser_evm.exec.assert_called_once()
     assert laser_evm.exec.call_count == 1
     assert len(laser_evm.open_states) == 0
-
-
-def test_calldata_constraints_in_transaction():
-    # Arrange
-    laser_evm = LaserEVM({})
-    world_state = WorldState()
-
-    correct_constraints = [MagicMock(), MagicMock(), MagicMock()]
-
-    transaction = MessageCallTransaction(
-        world_state, Account("ca11ee"), Account("ca114")
-    )
-    transaction.call_data = MagicMock()
-    transaction.call_data.constraints = correct_constraints
-
-    # Act
-    _setup_global_state_for_execution(laser_evm, transaction)
-
-    # Assert
-    state = laser_evm.work_list[0]
-    for constraint in correct_constraints:
-        assert constraint in state.environment.calldata.constraints