Merge latest develop branch into 'feature/type-hints-develop'

mythril/analysis/modules/dependence_on_predictable_vars.py

@@ -48,7 +48,7 @@ def execute(statespace):
 
         found = []
         for var in vars:
-            for constraint in call.node.constraints + [call.to]:
+            for constraint in call.node.constraints[:] + [call.to]:
                 if var in str(constraint):
                     found.append(var)
 
@@ -75,7 +75,7 @@ def execute(statespace):
 
         # Second check: blockhash
 
-        for constraint in call.node.constraints + [call.to]:
+        for constraint in call.node.constraints[:] + [call.to]:
             if "blockhash" in str(constraint):
                 description = "In the function `" + call.node.function_name + "` "
                 if "number" in str(constraint):

mythril/analysis/modules/integer.py

@@ -70,10 +70,13 @@ def _check_integer_overflow(statespace, state, node):
         op1 = BitVecVal(op1, 256)
 
     # Formulate expression
+    # FIXME: handle exponentiation
     if instruction["opcode"] == "ADD":
+        operator = "add"
         expr = op0 + op1
         # constraint = Not(BVAddNoOverflow(op0, op1, signed=False))
     else:
+        operator = "multiply"
         expr = op1 * op0
         # constraint = Not(BVMulNoOverflow(op0, op1, signed=False))
 
@@ -101,7 +104,9 @@ def _check_integer_overflow(statespace, state, node):
         _type="Warning",
     )
 
-    issue.description = "The arithmetic operation can result in integer overflow.\n"
+    issue.description = "This binary {} operation can result in integer overflow.\n".format(
+        operator
+    )
     issue.debug = "Transaction Sequence: " + str(
         solver.get_transaction_sequence(state, node.constraints)
     )

mythril/laser/ethereum/instructions.py

@@ -1070,6 +1070,7 @@ class Instruction:
                 states.append(new_state)
             else:
                 logging.debug("Pruned unreachable states.")
+        del global_state
         return states
 
     @StateTransition()

mythril/laser/ethereum/state.py

@@ -266,6 +266,43 @@ class Environment:
         )
 
 
+class Constraints(list):
+    """
+    This class should maintain a solver and it's constraints, This class tries to make the Constraints() object
+    as a simple list of constraints with some background processing.
+    TODO: add the solver to this class after callback refactor
+    """
+
+    def __init__(self, constraint_list=None, solver=None, possibility=None):
+        super(Constraints, self).__init__(constraint_list or [])
+        self.solver = solver
+        self.__possibility = possibility
+
+    def check_possibility(self):
+        return True
+
+    def append(self, constraint):
+        super(Constraints, self).append(constraint)
+
+    def pop(self, index=-1):
+        raise NotImplementedError
+
+    def __copy__(self):
+        constraint_list = super(Constraints, self).copy()
+        return Constraints(constraint_list)
+
+    def __deepcopy__(self, memodict=None):
+        return self.__copy__()
+
+    def __add__(self, constraints):
+        constraints_list = super(Constraints, self).__add__(constraints)
+        return Constraints(constraint_list=constraints_list)
+
+    def __iadd__(self, constraints):
+        super(Constraints, self).__iadd__(constraints)
+        return self
+
+
 class MachineStack(list):
     """
     Defines EVM stack, overrides the default list to handle overflows
@@ -328,14 +365,14 @@ class MachineState:
     MachineState represents current machine state also referenced to as \mu
     """
 
-    def __init__(self, gas: int):
+    def __init__(self, gas: int, pc=0, stack=None, memory=None, constraints=None, depth=0):
         """ Constructor for machineState """
-        self.pc = 0
-        self.stack = MachineStack()
-        self.memory = []
+        self.pc = pc
+        self.stack = MachineStack(stack)
+        self.memory = memory or []
         self.gas = gas
-        self.constraints = []
-        self.depth = 0
+        self.constraints = constraints or Constraints()
+        self.depth = depth
 
     def mem_extend(self, start: int, size: int) -> None:
         """
@@ -362,7 +399,18 @@ class MachineState:
 
         return values[0] if amount == 1 else values
 
-    def __str__(self) -> str:
+    def __deepcopy__(self, memodict=None):
+        memodict = {} if memodict is None else memodict
+        return MachineState(
+            gas=self.gas,
+            pc=self.pc,
+            stack=copy(self.stack),
+            memory=copy(self.memory),
+            constraints=copy(self.constraints),
+            depth=self.depth,
+        )
+
+    def __str__(self):
         return str(self.as_dict)
 
     @property

mythril/laser/ethereum/svm.py

@@ -171,7 +171,6 @@ class LaserEVM:
             except NotImplementedError:
                 logging.info("Encountered unimplemented instruction")
                 continue
-
             self.manage_cfg(op_code, new_states)
 
             self.work_list += new_states

tests/testdata/outputs_expected/ether_send.sol.o.json

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 722, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.", "function": "withdrawfunds()", "swc_id": "105", "title": "Ether send", "type": "Warning"}, {"address": 883, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The arithmetic operation can result in integer overflow.\n", "function": "invest()", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}
+{"error": null, "issues": [{"address": 722, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.", "function": "withdrawfunds()", "swc_id": "105", "title": "Ether send", "type": "Warning"}, {"address": 883, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This binary add operation can result in integer overflow.\n", "function": "invest()", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}

tests/testdata/outputs_expected/ether_send.sol.o.markdown

@@ -20,4 +20,4 @@ It seems that an attacker is able to execute an call instruction, this can mean
 
 ### Description
 
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.

tests/testdata/outputs_expected/ether_send.sol.o.text

@@ -13,7 +13,7 @@ Type: Warning
 Contract: Unknown
 Function name: invest()
 PC address: 883
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.
 
 --------------------
 

tests/testdata/outputs_expected/overflow.sol.o.json

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The arithmetic operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}
+{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This binary add operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}

tests/testdata/outputs_expected/overflow.sol.o.markdown

@@ -31,4 +31,4 @@ The subtraction can result in an integer underflow.
 
 ### Description
 
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.

tests/testdata/outputs_expected/overflow.sol.o.text

@@ -24,7 +24,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 725
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.
 
 --------------------
 

tests/testdata/outputs_expected/underflow.sol.o.json

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The arithmetic operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}
+{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This binary add operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}

tests/testdata/outputs_expected/underflow.sol.o.markdown

@@ -31,4 +31,4 @@ The subtraction can result in an integer underflow.
 
 ### Description
 
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.

tests/testdata/outputs_expected/underflow.sol.o.text

@@ -24,7 +24,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 725
-The arithmetic operation can result in integer overflow.
+This binary add operation can result in integer overflow.
 
 --------------------