Bugfix calls (#1288)

* Fix bugs

* Change tests

* black

* Fix the string

* Change the name and add a docstring

* Change max-depth to 128

* refactor with black

* Rename function name and remove constraints append code

mythril/analysis/modules/external_calls.py

@@ -94,14 +94,10 @@ class ExternalCalls(DetectionModule):
             # Check whether we can also set the callee address
 
             try:
-                constraints += [to == ACTORS.attacker]
-
-                for tx in state.world_state.transaction_sequence:
-                    if not isinstance(tx, ContractCreationTransaction):
-                        constraints.append(tx.caller == ACTORS.attacker)
+                new_constraints = constraints + [to == ACTORS.attacker]
 
                 solver.get_transaction_sequence(
-                    state, constraints + state.world_state.constraints
+                    state, new_constraints + state.world_state.constraints
                 )
 
                 description_head = "A call to a user-supplied address is executed."
@@ -122,7 +118,7 @@ class ExternalCalls(DetectionModule):
                     severity="Medium",
                     description_head=description_head,
                     description_tail=description_tail,
-                    constraints=constraints,
+                    constraints=new_constraints,
                     detector=self,
                 )
 

mythril/interfaces/cli.py

@@ -384,7 +384,7 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
     options.add_argument(
         "--max-depth",
         type=int,
-        default=50,
+        default=128,
         help="Maximum recursion depth for symbolic execution",
     )
     options.add_argument(

mythril/laser/ethereum/instructions.py

@@ -732,7 +732,6 @@ class Instruction:
         :return:
         """
         state = global_state.mstate
-
         val = state.stack.pop()
         exp = Not(val) if isinstance(val, Bool) else val == 0
 
@@ -1395,7 +1394,6 @@ class Instruction:
 
         state.mem_extend(offset, 32)
         data = state.memory.get_word_at(offset)
-
         state.stack.append(data)
         return [global_state]
 
@@ -1518,7 +1516,6 @@ class Instruction:
         states = []
 
         op0, condition = state.stack.pop(), state.stack.pop()
-
         try:
             jump_addr = util.get_concrete_int(op0)
         except TypeError:
@@ -1712,7 +1709,6 @@ class Instruction:
         :return:
         """
         call_value, mem_offset, mem_size = global_state.mstate.pop(3)
-
         return self._create_transaction_helper(
             global_state, call_value, mem_offset, mem_size
         )
@@ -1837,6 +1833,27 @@ class Instruction:
         """
         global_state.current_transaction.end(global_state)
 
+    @staticmethod
+    def _write_symbolic_returndata(
+        global_state: GlobalState, memory_out_offset: BitVec, memory_out_size: BitVec
+    ):
+        """
+        Writes symbolic return-data into memory, The memory offset and size should be concrete
+        :param global_state:
+        :param memory_out_offset:
+        :param memory_out_size:
+        :return:
+        """
+        if memory_out_offset.symbolic is True or memory_out_size.symbolic is True:
+            return
+        for i in range(memory_out_size.value):
+            global_state.mstate.memory[memory_out_offset + i] = global_state.new_bitvec(
+                "call_output_var({})_{}".format(
+                    simplify(memory_out_offset + i), global_state.mstate.pc,
+                ),
+                8,
+            )
+
     @StateTransition()
     def call_(self, global_state: GlobalState) -> List[GlobalState]:
         """
@@ -1847,6 +1864,7 @@ class Instruction:
         instr = global_state.get_current_instruction()
         environment = global_state.environment
 
+        memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5]
         try:
             (
                 callee_address,
@@ -1875,6 +1893,9 @@ class Instruction:
                     e
                 )
             )
+            self._write_symbolic_returndata(
+                global_state, memory_out_offset, memory_out_size
+            )
             # TODO: decide what to do in this case
             global_state.mstate.stack.append(
                 global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1933,7 +1954,7 @@ class Instruction:
         """
         instr = global_state.get_current_instruction()
         environment = global_state.environment
-
+        memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5]
         try:
             (
                 callee_address,
@@ -1944,6 +1965,7 @@ class Instruction:
                 _,
                 _,
             ) = get_call_parameters(global_state, self.dynamic_loader, True)
+
             if callee_account is not None and callee_account.code.bytecode == "":
                 log.debug("The call is related to ether transfer between accounts")
                 sender = global_state.environment.active_account.address
@@ -1961,6 +1983,9 @@ class Instruction:
                     e
                 )
             )
+            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)
             )
@@ -1988,7 +2013,7 @@ class Instruction:
         :return:
         """
         instr = global_state.get_current_instruction()
-
+        memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5]
         try:
             (
                 callee_address,
@@ -2005,6 +2030,9 @@ class Instruction:
                     e
                 )
             )
+            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)
             )
@@ -2016,6 +2044,9 @@ class Instruction:
                 "retval_" + str(instr["address"]), 256
             )
             global_state.mstate.stack.append(return_value)
+            self._write_symbolic_returndata(
+                global_state, memory_out_offset, memory_out_size
+            )
             global_state.world_state.constraints.append(return_value == 0)
             return [global_state]
 
@@ -2060,6 +2091,7 @@ class Instruction:
         """
         instr = global_state.get_current_instruction()
         environment = global_state.environment
+        memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4]
 
         try:
             (
@@ -2089,6 +2121,9 @@ class Instruction:
                     e
                 )
             )
+            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)
             )
@@ -2116,6 +2151,7 @@ class Instruction:
         :return:
         """
         instr = global_state.get_current_instruction()
+        memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4]
 
         try:
             (
@@ -2136,6 +2172,9 @@ class Instruction:
             global_state.mstate.stack.append(
                 global_state.new_bitvec("retval_" + str(instr["address"]), 256)
             )
+            self._write_symbolic_returndata(
+                global_state, memory_out_offset, memory_out_size
+            )
             return [global_state]
 
         if global_state.last_return_data is None:
@@ -2188,6 +2227,7 @@ class Instruction:
         """
         instr = global_state.get_current_instruction()
         environment = global_state.environment
+        memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4]
         try:
             (
                 callee_address,
@@ -2216,6 +2256,9 @@ class Instruction:
                     e
                 )
             )
+            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)
             )
@@ -2248,6 +2291,10 @@ class Instruction:
 
     def post_handler(self, global_state, function_name: str):
         instr = global_state.get_current_instruction()
+        if function_name in ("staticcall", "delegatecall"):
+            memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4]
+        else:
+            memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5]
 
         try:
             with_value = function_name is not "staticcall"
@@ -2266,6 +2313,9 @@ class Instruction:
                     function_name, e
                 )
             )
+            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)
             )

tests/instructions/static_call_test.py

@@ -90,7 +90,7 @@ def test_staticness_call_concrete(f1, input, success):
     # Arrange
     state = get_global_state()
     state.environment.static = True
-    state.mstate.stack = []
+    state.mstate.stack = [10] * 100
     code = Disassembly(code="616263")
     f1.return_value = ("0", Account(code=code, address="0x19"), 0, input, 0, 0, 0)
     instruction = Instruction("call", dynamic_loader=None)
@@ -110,7 +110,7 @@ def test_staticness_call_symbolic(f1):
     # Arrange
     state = get_global_state()
     state.environment.static = True
-    state.mstate.stack = []
+    state.mstate.stack = [10] * 100
     call_value = symbol_factory.BitVecSym("x", 256)
     code = Disassembly(code="616263")
     f1.return_value = ("0", Account(code=code, address="0x19"), 0, call_value, 0, 0, 0)