From 0f8e9144a64d22dac51757d20b7282df5cfb8a17 Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Tue, 16 Oct 2018 16:55:58 +0800 Subject: [PATCH 1/4] analysis/transaction_order_dependence: import missing `copy` module in transaction_order_dependence.py copy.deepcopy() is used in transaction_order_dependence.py, but the `copy` module is not imported. --- mythril/analysis/modules/transaction_order_dependence.py | 1 + 1 file changed, 1 insertion(+) diff --git a/mythril/analysis/modules/transaction_order_dependence.py b/mythril/analysis/modules/transaction_order_dependence.py index 4528459c..9db7c104 100644 --- a/mythril/analysis/modules/transaction_order_dependence.py +++ b/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 * From ce4075b8df3e8d6bcfdd309b91b3a3fad2177f3d Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Tue, 9 Oct 2018 13:52:12 +0800 Subject: [PATCH 2/4] laser/instruction: remove unused solver in sstore_() --- mythril/laser/ethereum/instructions.py | 5 ----- 1 file changed, 5 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index c31d5f46..cabdaba1 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/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 From 725bfec464594070d568f6a24880abd16afb05a4 Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Tue, 30 Oct 2018 20:53:30 +0800 Subject: [PATCH 3/4] laser/instruction: simplify before checking by Z3 is_true() Z3 is_true() does not automatically consider `expr == expr` to be true, so `is_true(key_argument == index_argument)` in `sstore_()` will miss lots of positive conditions and then generate lots of unnecessary subsequent paths. Take the following contract for example ``` contract Foo { mapping(address => uint) public balances; function bar(address _to, uint256 _value) public { require(balances[_to] + _value >= balances[_to]); balances[_to] += _value; balances[_to] += _value; } ``` Before this commit, - 772 nodes/771 edges/8288 states are generated. After this commit, - only 237 nodes/236 edges/3204 states are generated. --- mythril/laser/ethereum/instructions.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index cabdaba1..edefece9 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -929,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, From 91015e63baae514393e0cb6a7ea64e80a3b93d67 Mon Sep 17 00:00:00 2001 From: Haozhong Zhang Date: Tue, 30 Oct 2018 21:17:06 +0800 Subject: [PATCH 4/4] analysis/integer: remove unnecessary deepcopy of constraints `solver.get_model()` has no way to mutate constraints passed to it, so the expensive deepcopy of constraints before calling `solver.get_model()`is unnecessary. --- mythril/analysis/modules/integer.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py index b5c952f8..4e6f9b25 100644 --- a/mythril/analysis/modules/integer.py +++ b/mythril/analysis/modules/integer.py @@ -127,11 +127,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