Use a more precise modeling of return data (#1630)

* remove depth for jump

* Use a more precise modeling of return data

* Fix issues with lists

* Fix issues

mythril/laser/ethereum/instructions.py

@@ -52,6 +52,8 @@ from mythril.laser.ethereum.evm_exceptions import (
 )
 from mythril.laser.ethereum.instruction_data import get_opcode_gas, calculate_sha3_gas
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.return_data import ReturnData
+
 from mythril.laser.ethereum.transaction import (
     MessageCallTransaction,
     TransactionStartSignal,
@@ -1340,7 +1342,7 @@ class Instruction:
         for i in range(concrete_size):
             global_state.mstate.memory[concrete_memory_offset + i] = (
                 global_state.last_return_data[concrete_return_offset + i]
-                if i < len(global_state.last_return_data)
+                if i < global_state.last_return_data.size
                 else 0
             )
 
@@ -1353,16 +1355,10 @@ class Instruction:
         :param global_state:
         :return:
         """
-        if global_state.last_return_data is None:
+        if global_state.last_return_data:
-            log.debug(
+            global_state.mstate.stack.append(global_state.last_return_data.size)
-                "No last_return_data found, adding an unconstrained bitvec to the stack"
-            )
-            global_state.mstate.stack.append(
-                global_state.new_bitvec("returndatasize", 256)
-            )
         else:
-            global_state.mstate.stack.append(len(global_state.last_return_data))
+            global_state.mstate.stack.append(0)
-
         return [global_state]
 
     @StateTransition()
@@ -1865,7 +1861,9 @@ class Instruction:
             state.mem_extend(offset, length)
             StateTransition.check_gas_usage_limit(global_state)
             return_data = state.memory[offset : offset + length]
-        global_state.current_transaction.end(global_state, return_data)
+        global_state.current_transaction.end(
+            global_state, ReturnData(return_data, length)
+        )
 
     @StateTransition(is_state_mutation_instruction=True)
     def selfdestruct_(self, global_state: GlobalState):
@@ -1898,7 +1896,25 @@ class Instruction:
         """
         state = global_state.mstate
         offset, length = state.stack.pop(), state.stack.pop()
-        return_data = [global_state.new_bitvec("return_data", 8)]
+        if length.symbolic is False:
+            return_data = [
+                global_state.new_bitvec(
+                    f"{global_state.current_transaction.id}_return_data_{i}", 8
+                )
+                for i in range(length.value)
+            ]
+        else:
+            return_data = [
+                If(
+                    i < length,
+                    global_state.new_bitvec(
+                        f"{global_state.current_transaction.id}_return_data_{i}", 8
+                    ),
+                    0,
+                )
+                for i in range(300)
+            ]
+
         try:
             return_data = state.memory[
                 util.get_concrete_int(offset) : util.get_concrete_int(offset + length)
@@ -1906,7 +1922,7 @@ class Instruction:
         except TypeError:
             log.debug("Return with symbolic length or offset. Not supported")
         global_state.current_transaction.end(
-            global_state, return_data=return_data, revert=True
+            global_state, return_data=ReturnData(return_data, length), revert=True
         )
 
     @StateTransition()
@@ -1947,13 +1963,27 @@ class Instruction:
         """
         if memory_out_offset.symbolic is True or memory_out_size.symbolic is True:
             return
+        return_data = []
+        return_data_size = global_state.new_bitvec("returndatasize", 256)
+
         for i in range(memory_out_size.value):
-            global_state.mstate.memory[memory_out_offset + i] = global_state.new_bitvec(
+            data = global_state.new_bitvec(
                 "call_output_var({})_{}".format(
                     simplify(memory_out_offset + i), global_state.mstate.pc
                 ),
                 8,
             )
+            return_data.append(data)
+        for i in range(memory_out_size.value):
+            global_state.mstate.memory[memory_out_offset + i] = If(
+                i <= return_data_size,
+                return_data[i],
+                global_state.mstate.memory[memory_out_offset + i],
+            )
+
+        global_state.last_return_data = ReturnData(
+            return_data=return_data, return_data_size=return_data_size
+        )
 
     @StateTransition()
     def call_(self, global_state: GlobalState) -> List[GlobalState]:
@@ -1982,6 +2012,9 @@ class Instruction:
                 sender = environment.active_account.address
                 receiver = callee_account.address
                 transfer_ether(global_state, sender, receiver, value)
+                self._write_symbolic_returndata(
+                    global_state, memory_out_offset, memory_out_size
+                )
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -2072,6 +2105,9 @@ class Instruction:
                 sender = global_state.environment.active_account.address
                 receiver = callee_account.address
                 transfer_ether(global_state, sender, receiver, value)
+                self._write_symbolic_returndata(
+                    global_state, memory_out_offset, memory_out_size
+                )
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -2176,9 +2212,9 @@ class Instruction:
 
         # Copy memory
         global_state.mstate.mem_extend(
-            memory_out_offset, min(memory_out_size, len(global_state.last_return_data))
+            memory_out_offset, min(memory_out_size, global_state.last_return_data.size)
         )
-        for i in range(min(memory_out_size, len(global_state.last_return_data))):
+        for i in range(min(memory_out_size, global_state.last_return_data.size)):
             global_state.mstate.memory[
                 i + memory_out_offset
             ] = global_state.last_return_data[i]
@@ -2216,6 +2252,9 @@ class Instruction:
                 sender = global_state.environment.active_account.address
                 receiver = callee_account.address
                 transfer_ether(global_state, sender, receiver, value)
+                self._write_symbolic_returndata(
+                    global_state, memory_out_offset, memory_out_size
+                )
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -2317,9 +2356,9 @@ class Instruction:
 
             # Copy memory
         global_state.mstate.mem_extend(
-            memory_out_offset, min(memory_out_size, len(global_state.last_return_data))
+            memory_out_offset, min(memory_out_size, global_state.last_return_data.size)
         )
-        for i in range(min(memory_out_size, len(global_state.last_return_data))):
+        for i in range(min(memory_out_size, global_state.last_return_data.size)):
             global_state.mstate.memory[
                 i + memory_out_offset
             ] = global_state.last_return_data[i]
@@ -2356,10 +2395,13 @@ class Instruction:
                 sender = environment.active_account.address
                 receiver = callee_account.address
                 transfer_ether(global_state, sender, receiver, value)
-
+                self._write_symbolic_returndata(
+                    global_state, memory_out_offset, memory_out_size
+                )
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
                 )
+
                 return [global_state]
 
         except ValueError as e:
@@ -2458,17 +2500,19 @@ class Instruction:
             )
             return [global_state]
 
-        # Copy memory
         global_state.mstate.mem_extend(
-            memory_out_offset, min(memory_out_size, len(global_state.last_return_data))
+            memory_out_offset, min(memory_out_size, global_state.last_return_data.size)
         )
-        for i in range(min(memory_out_size, len(global_state.last_return_data))):
+
+        for i in range(min(memory_out_size, global_state.last_return_data.size)):
             global_state.mstate.memory[
                 i + memory_out_offset
             ] = global_state.last_return_data[i]
 
         # Put return value on stack
-        return_value = global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+        return_value = global_state.new_bitvec(
+            "retval_" + str(global_state.get_current_instruction()["address"]), 256
+        )
         global_state.mstate.stack.append(return_value)
         global_state.world_state.constraints.append(return_value == 1)
 

mythril/laser/ethereum/state/return_data.py

@@ -0,0 +1,32 @@
+"""This module declares classes to represent call data."""
+from typing import List
+
+from mythril.laser.smt import (
+    BitVec,
+)
+
+
+class ReturnData:
+    """Base returndata class."""
+
+    def __init__(self, return_data: List[BitVec], return_data_size: BitVec) -> None:
+        """
+
+        :param tx_id:
+        """
+        self.return_data = return_data
+        self.return_data_size = return_data_size
+
+    @property
+    def size(self) -> BitVec:
+        """
+
+        :return: Calldata size for this calldata object
+        """
+        return self.return_data_size
+
+    def __getitem__(self, index):
+        if index < self.size:
+            return self.return_data[index]
+        else:
+            return 0

mythril/laser/ethereum/svm.py

@@ -270,6 +270,7 @@ class LaserEVM:
             hook()
 
         for global_state in self.strategy:
+
             if create and self._check_create_termination():
                 log.debug("Hit create timeout, returning.")
                 return final_states + [global_state] if track_gas else None
@@ -277,13 +278,11 @@ class LaserEVM:
             if not create and self._check_execution_termination():
                 log.debug("Hit execution timeout, returning.")
                 return final_states + [global_state] if track_gas else None
-
             try:
                 new_states, op_code = self.execute_state(global_state)
             except NotImplementedError:
                 log.debug("Encountered unimplemented instruction")
                 continue
-
             if args.sparse_pruning is False:
                 new_states = [
                     state

mythril/laser/ethereum/transaction/transaction_models.py

@@ -148,12 +148,20 @@ class BaseTransaction:
         raise NotImplementedError
 
     def __str__(self) -> str:
+        if self.callee_account is None or self.callee_account.address.symbolic is False:
             return "{} {} from {} to {:#42x}".format(
                 self.__class__.__name__,
                 self.id,
                 self.caller,
                 int(str(self.callee_account.address)) if self.callee_account else -1,
             )
+        else:
+            return "{} {} from {} to {}".format(
+                self.__class__.__name__,
+                self.id,
+                self.caller,
+                str(self.callee_account.address),
+            )
 
 
 class MessageCallTransaction(BaseTransaction):
@@ -258,11 +266,13 @@ class ContractCreationTransaction(BaseTransaction):
         :param revert:
         """
 
-        if return_data is None or len(return_data) == 0:
+        if return_data is None or return_data.size == 0:
             self.return_data = None
             raise TransactionEndSignal(global_state, revert=revert)
 
-        global_state.environment.active_account.code.assign_bytecode(tuple(return_data))
+        global_state.environment.active_account.code.assign_bytecode(
+            tuple(return_data.return_data)
+        )
         self.return_data = str(
             hex(global_state.environment.active_account.address.value)
         )

mythril/laser/smt/bitvec_helper.py

@@ -59,11 +59,15 @@ def If(
     if isinstance(b, BaseArray) and isinstance(c, BaseArray):
         array = z3.If(a.raw, b.raw, c.raw)
         return _z3_array_converter(array)
-
+    default_sort_size = 256
+    if isinstance(b, BitVec):
+        default_sort_size = b.size()
+    if isinstance(c, BitVec):
+        default_sort_size = c.size()
     if not isinstance(b, BitVec):
-        b = BitVec(z3.BitVecVal(b, 256))
+        b = BitVec(z3.BitVecVal(b, default_sort_size))
     if not isinstance(c, BitVec):
-        c = BitVec(z3.BitVecVal(c, 256))
+        c = BitVec(z3.BitVecVal(c, default_sort_size))
     union = a.annotations.union(b.annotations).union(c.annotations)
     return BitVec(z3.If(a.raw, b.raw, c.raw), union)