From dfaa9382ecbf6387e12e121c6368a95a6f3342ed Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Thu, 14 Apr 2022 13:59:21 +0100 Subject: [PATCH] Fix misc issues related to summaries (#1617) * Check versions before using integer module * Use IssueAnnotations * Fix misc issues with summaries --- mythril/analysis/module/modules/arbitrary_jump.py | 1 + mythril/analysis/module/modules/suicide.py | 1 + mythril/analysis/solver.py | 3 --- mythril/ethereum/util.py | 2 +- mythril/laser/ethereum/function_managers/__init__.py | 2 +- .../ethereum/function_managers/keccak_function_manager.py | 1 - mythril/laser/ethereum/state/constraints.py | 2 +- mythril/laser/ethereum/svm.py | 7 ++++++- mythril/laser/smt/array.py | 2 +- 9 files changed, 12 insertions(+), 9 deletions(-) diff --git a/mythril/analysis/module/modules/arbitrary_jump.py b/mythril/analysis/module/modules/arbitrary_jump.py index a113d471..bb4da658 100644 --- a/mythril/analysis/module/modules/arbitrary_jump.py +++ b/mythril/analysis/module/modules/arbitrary_jump.py @@ -56,6 +56,7 @@ class ArbitraryJump(DetectionModule): ) except UnsatError: return [] + log.info("Detected arbitrary jump dest") issue = Issue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, diff --git a/mythril/analysis/module/modules/suicide.py b/mythril/analysis/module/modules/suicide.py index 7dae7f53..9f61164f 100644 --- a/mythril/analysis/module/modules/suicide.py +++ b/mythril/analysis/module/modules/suicide.py @@ -11,6 +11,7 @@ from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) import logging +from mythril.laser.ethereum.function_managers import keccak_function_manager log = logging.getLogger(__name__) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 93e60106..3661cb2b 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -58,11 +58,8 @@ def get_transaction_sequence( :param global_state: GlobalState to generate transaction sequence for :param constraints: list of constraints used to generate transaction sequence """ - transaction_sequence = global_state.world_state.transaction_sequence - concrete_transactions = [] - tx_constraints, minimize = _set_minimisation_constraints( transaction_sequence, constraints.copy(), [], 5000, global_state.world_state ) diff --git a/mythril/ethereum/util.py b/mythril/ethereum/util.py index 85cc20f4..30ae79f8 100644 --- a/mythril/ethereum/util.py +++ b/mythril/ethereum/util.py @@ -90,7 +90,7 @@ def get_solc_json(file, solc_binary="solc", solc_settings_json=None): try: result = json.loads(out) except JSONDecodeError as e: - log.error(f"Encountered a decode error, stdout:{out}, stderr: {stderr}") + log.error(f"Encountered a decode error.\n stdout:{out}\n stderr: {stderr}") raise e for error in result.get("errors", []): diff --git a/mythril/laser/ethereum/function_managers/__init__.py b/mythril/laser/ethereum/function_managers/__init__.py index 3fa564a3..056b4cf3 100644 --- a/mythril/laser/ethereum/function_managers/__init__.py +++ b/mythril/laser/ethereum/function_managers/__init__.py @@ -1,2 +1,2 @@ from .exponent_function_manager import exponent_function_manager -from .keccak_function_manager import keccak_function_manager +from .keccak_function_manager import keccak_function_manager, KeccakFunctionManager diff --git a/mythril/laser/ethereum/function_managers/keccak_function_manager.py b/mythril/laser/ethereum/function_managers/keccak_function_manager.py index 8122b4c9..9518bbec 100644 --- a/mythril/laser/ethereum/function_managers/keccak_function_manager.py +++ b/mythril/laser/ethereum/function_managers/keccak_function_manager.py @@ -127,7 +127,6 @@ class KeccakFunctionManager: func(concrete_input) == concrete_hash, inverse(func(concrete_input)) == concrete_input, ) - return condition def get_concrete_hash_data(self, model) -> Dict[int, List[Optional[int]]]: diff --git a/mythril/laser/ethereum/state/constraints.py b/mythril/laser/ethereum/state/constraints.py index 1c6a61ec..ec6414ba 100644 --- a/mythril/laser/ethereum/state/constraints.py +++ b/mythril/laser/ethereum/state/constraints.py @@ -52,7 +52,7 @@ class Constraints(list): """ :return: returns the list of constraints """ - return self[:] + return self[:] + [keccak_function_manager.create_conditions()] def __copy__(self) -> "Constraints": """ diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 66c4aef9..f7b81f1a 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -410,7 +410,12 @@ class LaserEVM: log.debug("Ending transaction %s.", transaction) for hook in self._transaction_end_hooks: - hook(global_state, transaction, return_global_state, end_signal.revert) + hook( + end_signal.global_state, + transaction, + return_global_state, + end_signal.revert, + ) if return_global_state is None: if ( diff --git a/mythril/laser/smt/array.py b/mythril/laser/smt/array.py index 732b292e..66bccd6c 100644 --- a/mythril/laser/smt/array.py +++ b/mythril/laser/smt/array.py @@ -29,7 +29,7 @@ class BaseArray: """Sets an item in the array, key can be symbolic.""" self.raw = z3.Store(self.raw, key.raw, value.raw) - def substitute(self, original_expression: "BaseArray", new_expression: "BaseArray"): + def substitute(self, original_expression, new_expression): """ :param original_expression: