Merge pull request #657 from ConsenSys/develop

Merge develop

mythril/analysis/modules/dependence_on_predictable_vars.py

@@ -66,7 +66,7 @@ def execute(statespace):
                     function_name=call.node.function_name,
                     address=address,
                     swc_id=swc_type,
-                    bytecode=state.environment.code.bytecode,
+                    bytecode=call.state.environment.code.bytecode,
                     title="Dependence on predictable environment variable",
                     _type="Warning",
                     description=description,
@@ -144,7 +144,7 @@ def execute(statespace):
                                 contract=call.node.contract_name,
                                 function_name=call.node.function_name,
                                 address=address,
-                                bytecode=state.environment.code.bytecode,
+                                bytecode=call.state.environment.code.bytecode,
                                 title="Dependence on predictable variable",
                                 _type="Informational",
                                 description=description,

mythril/analysis/modules/integer.py

@@ -72,11 +72,13 @@ def _check_integer_overflow(statespace, state, node):
     # Formulate expression
     if instruction["opcode"] == "ADD":
         expr = op0 + op1
+        # constraint = Not(BVAddNoOverflow(op0, op1, signed=False))
     else:
         expr = op1 * op0
+        # constraint = Not(BVMulNoOverflow(op0, op1, signed=False))
 
-    # Check satisfiable
     constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0))
+    # Check satisfiable
     model = _try_constraints(node.constraints, [constraint])
 
     if model is None:
@@ -130,11 +132,8 @@ def _try_constraints(constraints, new_constraints):
     Tries new constraints
     :return Model if satisfiable otherwise None
     """
-    _constraints = copy.deepcopy(constraints)
-    for constraint in new_constraints:
-        _constraints.append(copy.deepcopy(constraint))
     try:
-        model = solver.get_model(_constraints)
+        model = solver.get_model(constraints + new_constraints)
         return model
     except UnsatError:
         return None
@@ -210,7 +209,7 @@ def _check_integer_underflow(statespace, state, node):
                 )
 
                 issue.description = (
-                    "The substraction can result in an integer underflow.\n"
+                    "The subtraction can result in an integer underflow.\n"
                 )
 
                 issue.debug = "Transaction Sequence: " + str(

mythril/analysis/modules/transaction_order_dependence.py

@@ -1,5 +1,6 @@
 import logging
 import re
+import copy
 
 from mythril.analysis import solver
 from mythril.analysis.ops import *

mythril/laser/ethereum/instructions.py

@@ -18,7 +18,6 @@ from z3 import (
     URem,
     SRem,
     BitVec,
-    Solver,
     is_true,
     BitVecVal,
     If,
@@ -43,7 +42,6 @@ from mythril.laser.ethereum.transaction import (
     TransactionStartSignal,
     ContractCreationTransaction,
 )
-from mythril.analysis.solver import get_model
 
 TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
@@ -924,9 +922,6 @@ class Instruction:
             storage_keys = global_state.environment.active_account.storage.keys()
             keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys)
 
-            solver = Solver()
-            solver.set(timeout=1000)
-
             results = []
             new = False
 
@@ -934,7 +929,7 @@ class Instruction:
                 key_argument = keccak_function_manager.get_argument(keccak_key)
                 index_argument = keccak_function_manager.get_argument(index)
 
-                if is_true(key_argument == index_argument):
+                if is_true(simplify(key_argument == index_argument)):
                     return self._sstore_helper(
                         copy(global_state),
                         keccak_key,

mythril/version.py

@@ -1,3 +1,3 @@
 # This file is suitable for sourcing inside POSIX shell, e.g. bash as
 # well as for importing into Python
-VERSION = "v0.19.0"  # NOQA
+VERSION = "v0.19.1"  # NOQA

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

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The substraction 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 substraction 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": "The arithmetic 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

@@ -9,7 +9,7 @@
 
 ### Description
 
-The substraction can result in an integer underflow.
+The subtraction can result in an integer underflow.
 
 ## Integer Underflow
 - SWC ID: 101
@@ -20,7 +20,7 @@ The substraction can result in an integer underflow.
 
 ### Description
 
-The substraction can result in an integer underflow.
+The subtraction can result in an integer underflow.
 
 ## Integer Overflow
 - SWC ID: 101

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

@@ -4,7 +4,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 567
-The substraction can result in an integer underflow.
+The subtraction can result in an integer underflow.
 
 --------------------
 
@@ -14,7 +14,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 649
-The substraction can result in an integer underflow.
+The subtraction can result in an integer underflow.
 
 --------------------
 

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

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The substraction 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 substraction 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": "The arithmetic 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

@@ -9,7 +9,7 @@
 
 ### Description
 
-The substraction can result in an integer underflow.
+The subtraction can result in an integer underflow.
 
 ## Integer Underflow
 - SWC ID: 101
@@ -20,7 +20,7 @@ The substraction can result in an integer underflow.
 
 ### Description
 
-The substraction can result in an integer underflow.
+The subtraction can result in an integer underflow.
 
 ## Integer Overflow
 - SWC ID: 101

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

@@ -4,7 +4,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 567
-The substraction can result in an integer underflow.
+The subtraction can result in an integer underflow.
 
 --------------------
 
@@ -14,7 +14,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 649
-The substraction can result in an integer underflow.
+The subtraction can result in an integer underflow.
 
 --------------------