diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py index 78956cba..fe593e8d 100644 --- a/mythril/analysis/modules/exceptions.py +++ b/mythril/analysis/modules/exceptions.py @@ -43,7 +43,6 @@ class ReachableExceptionsModule(DetectionModule): :param state: :return: """ - print("SHIT ASSERT") log.debug("ASSERT_FAIL in function " + state.environment.active_function_name) try: @@ -74,7 +73,6 @@ class ReachableExceptionsModule(DetectionModule): transaction_sequence=transaction_sequence, gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) - print(state.mstate.constraints) return [issue] except UnsatError: diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 3e29cddc..e0e60796 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -152,7 +152,6 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction): address = "" input_ = transaction.code.bytecode else: - print(transaction.call_data._calldata.raw) input_ = "".join( [ hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:] diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 3a4aca0b..b179b452 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1368,10 +1368,7 @@ class Instruction: state = global_state.mstate index = state.stack.pop() - state.stack.append(global_state.environment.active_account.storage[index]) - if global_state.get_current_instruction()['address'] == 357: - print(state.stack[-1]) return [global_state] @StateTransition() diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index bdf7d715..cc873b02 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -122,7 +122,6 @@ class ArrayStorageRegion(StorageRegion): storage, is_keccak_storage = self._get_corresponding_storage(key) if is_keccak_storage: key = self._sanitize(key.input_) - storage[key] = value def __deepcopy__(self, memodict=dict()): @@ -180,7 +179,6 @@ class Storage: @staticmethod def _array_condition(key: BitVec): - return ( not isinstance(key, BitVecFunc) or ( @@ -193,7 +191,6 @@ class Storage: def __getitem__(self, key: BitVec) -> BitVec: ite_get = self._ite_region[cast(BitVecFunc, key)] array_get = self._array_region[key] - print(If(ite_get, ite_get, array_get)) return If(ite_get, ite_get, array_get) def __setitem__(self, key: BitVec, value: Any) -> None: diff --git a/mythril/laser/ethereum/state/environment.py b/mythril/laser/ethereum/state/environment.py index a3300f9a..3112c2b4 100644 --- a/mythril/laser/ethereum/state/environment.py +++ b/mythril/laser/ethereum/state/environment.py @@ -5,6 +5,7 @@ from typing import Dict from z3 import ExprRef from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.state.constraints import Constraints from mythril.laser.ethereum.state.calldata import BaseCalldata from mythril.laser.smt import symbol_factory @@ -22,6 +23,7 @@ class Environment: callvalue: ExprRef, origin: ExprRef, code=None, + constraints=None, ) -> None: """ diff --git a/mythril/laser/smt/bitvecfunc.py b/mythril/laser/smt/bitvecfunc.py index db57809f..902bee25 100644 --- a/mythril/laser/smt/bitvecfunc.py +++ b/mythril/laser/smt/bitvecfunc.py @@ -67,12 +67,13 @@ def _comparison_helper( if operation == z3.ULT: operation = operator.lt return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union) - #if not isinstance(b, BitVecFunc) and a.potential_value: - # condition = False - # for value, cond in a.potential_value: - # if value is not None: - # condition = Or(condition, And(b == value, cond)) - # return And(condition, operation(a.raw, b.raw)) + + if not isinstance(b, BitVecFunc) and a.potential_value: + condition = False + for value, cond in a.potential_value: + if value is not None: + condition = Or(condition, And(b == value, cond)) + return And(condition, operation(a.raw, b.raw)) if ( not isinstance(b, BitVecFunc) or not a.func_name