From 8a5b34c2ec1fee085cf7c279258262d43ab460e2 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 27 Aug 2020 16:44:55 -0300 Subject: [PATCH 1/3] New exploration stopping condition --- manticore/__main__.py | 3 --- manticore/ethereum/cli.py | 23 ++++++++++++++++++++++- manticore/ethereum/manticore.py | 33 ++++++++++++++++++++++++++++++--- 3 files changed, 52 insertions(+), 7 deletions(-) diff --git a/manticore/__main__.py b/manticore/__main__.py index 12d553465..e0e78d2e1 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -154,9 +154,6 @@ def positive(value): help="Maximum number of symbolic transactions to run (positive integer)", ) - eth_flags.add_argument( - "--txnocoverage", action="store_true", help="Do not use coverage as stopping criteria" - ) eth_flags.add_argument( "--txnoether", action="store_true", help="Do not attempt to send ether to contract" diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index fe90f870c..850aab6eb 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -40,6 +40,27 @@ description="Simply avoid exploring basic blocks that end in a REVERT", ) +from enum import Enum +class TermCondCovType(Enum): + """Used as configuration constant for choosing the coverage based termination + condition""" + + no = "no" + local = "local" + wide = "wide" + + def title(self): + return self._name_.title() + + @classmethod + def from_string(cls, name): + return cls.__members__[name] + +consts.add( + "txcoverage", default=TermCondCovType.local, + description="Set coverage stopping criteria" +) + def get_detectors_classes(): return [ @@ -134,7 +155,7 @@ def ethereum_main(args, logger): args.argv[0], contract_name=args.contract, tx_limit=args.txlimit, - tx_use_coverage=not args.txnocoverage, + tx_use_coverage=consts.txcoverage, tx_send_ether=not args.txnoether, tx_account=args.txaccount, tx_preconstrain=args.txpreconstrain, diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index b55f10c5b..80c1bb831 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -1032,6 +1032,18 @@ def preconstraint_for_call_transaction( return constraint + def local_coverage_progress(self) -> bool: + for state in self.ready_states: + new_local_coverage = len(set(state.context['evm.trace'])) + if 'evm.localcoverage' in state.context: + old_local_coverage = state.context['evm.localcoverage'] + else: + old_local_coverage = 0 + state.context['evm.localcoverage'] = new_local_coverage + if new_local_coverage != old_local_coverage: + return True + return False + def multi_tx_analysis( self, solidity_filename, @@ -1082,8 +1094,9 @@ def multi_tx_analysis( prev_coverage = 0 current_coverage = 0 tx_no = 0 - while (current_coverage < 100 or not tx_use_coverage) and not self.is_killed(): + while (current_coverage < 100 or tx_use_coverage is tx_use_coverage.no) and not self.is_killed(): try: + logger.info("Starting symbolic transaction: %d", tx_no) # run_symbolic_tx @@ -1104,7 +1117,7 @@ def multi_tx_analysis( address=contract_account, data=symbolic_data, value=value, - gas=230000, + gas=2300000, ) logger.info( @@ -1118,17 +1131,31 @@ def multi_tx_analysis( # Check if the maximum number of tx was reached if tx_limit is not None and tx_no + 1 == tx_limit: + print("Maximun tx limit reached") + logger.info("Maximun tx limit reached") break # Check if coverage has improved or not - if tx_use_coverage: + if tx_use_coverage is tx_use_coverage.wide: prev_coverage = current_coverage current_coverage = self.global_coverage(contract_account) found_new_coverage = prev_coverage < current_coverage if not found_new_coverage: + print("No coverage progresss!") + logger.info("No coverage progresss!") break + elif tx_use_coverage is tx_use_coverage.local: + try: + if not self.local_coverage_progress(): + print("No state made any progress") + logger.info("No state made any progress") + break + except Exception as e: + print (e) + + tx_no += 1 def run(self, **kwargs): From 41d9f502d7c85c16a63d4cd0c5b82f7a95a64b91 Mon Sep 17 00:00:00 2001 From: feliam Date: Thu, 27 Aug 2020 17:59:33 -0300 Subject: [PATCH 2/3] blkn --- manticore/__main__.py | 5 +- manticore/ethereum/cli.py | 8 +- manticore/ethereum/manticore.py | 298 ++++++++++++++++---------------- 3 files changed, 159 insertions(+), 152 deletions(-) diff --git a/manticore/__main__.py b/manticore/__main__.py index e0e78d2e1..8f3623b1f 100644 --- a/manticore/__main__.py +++ b/manticore/__main__.py @@ -154,7 +154,6 @@ def positive(value): help="Maximum number of symbolic transactions to run (positive integer)", ) - eth_flags.add_argument( "--txnoether", action="store_true", help="Do not attempt to send ether to contract" ) @@ -206,7 +205,9 @@ def positive(value): ) eth_flags.add_argument( - "--limit-loops", action="store_true", help="Limit loops depth", + "--limit-loops", + action="store_true", + help="Limit loops depth", ) eth_flags.add_argument( diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index 850aab6eb..322d5ee95 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -41,9 +41,11 @@ ) from enum import Enum + + class TermCondCovType(Enum): """Used as configuration constant for choosing the coverage based termination - condition""" + condition""" no = "no" local = "local" @@ -56,9 +58,9 @@ def title(self): def from_string(cls, name): return cls.__members__[name] + consts.add( - "txcoverage", default=TermCondCovType.local, - description="Set coverage stopping criteria" + "txcoverage", default=TermCondCovType.local, description="Set coverage stopping criteria" ) diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 80c1bb831..7a1440ce6 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -111,43 +111,43 @@ def calculate_coverage(runtime_bytecode, seen): class ManticoreEVM(ManticoreBase): - """ Manticore EVM manager - - Usage Ex:: - - from manticore.ethereum import ManticoreEVM, ABI - m = ManticoreEVM() - #And now make the contract account to analyze - source_code = ''' - pragma solidity ^0.4.15; - contract AnInt { - uint private i=0; - function set(uint value){ - i=value - } + """Manticore EVM manager + + Usage Ex:: + + from manticore.ethereum import ManticoreEVM, ABI + m = ManticoreEVM() + #And now make the contract account to analyze + source_code = ''' + pragma solidity ^0.4.15; + contract AnInt { + uint private i=0; + function set(uint value){ + i=value } - ''' - #Initialize user and contracts - user_account = m.create_account(balance=1000) - contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0) - contract_account.set(12345, value=100) - - m.finalize() + } + ''' + #Initialize user and contracts + user_account = m.create_account(balance=1000) + contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0) + contract_account.set(12345, value=100) + + m.finalize() """ def make_symbolic_buffer(self, size, name=None, avoid_collisions=False): - """ Creates a symbolic buffer of size bytes to be used in transactions. - You can operate on it normally and add constraints to manticore.constraints - via manticore.constrain(constraint_expression) - - Example use:: - - symbolic_data = m.make_symbolic_buffer(320) - m.constrain(symbolic_data[0] == 0x65) - m.transaction(caller=attacker_account, - address=contract_account, - data=symbolic_data, - value=100000 ) + """Creates a symbolic buffer of size bytes to be used in transactions. + You can operate on it normally and add constraints to manticore.constraints + via manticore.constrain(constraint_expression) + + Example use:: + + symbolic_data = m.make_symbolic_buffer(320) + m.constrain(symbolic_data[0] == 0x65) + m.transaction(caller=attacker_account, + address=contract_account, + data=symbolic_data, + value=100000 ) """ if name is None: name = "TXBUFFER" @@ -163,19 +163,19 @@ def make_symbolic_buffer(self, size, name=None, avoid_collisions=False): ) def make_symbolic_value(self, nbits=256, name=None): - """ Creates a symbolic value, normally a uint256, to be used in transactions. - You can operate on it normally and add constraints to manticore.constraints - via manticore.constrain(constraint_expression) + """Creates a symbolic value, normally a uint256, to be used in transactions. + You can operate on it normally and add constraints to manticore.constraints + via manticore.constrain(constraint_expression) - Example use:: + Example use:: - symbolic_value = m.make_symbolic_value() - m.constrain(symbolic_value > 100) - m.constrain(symbolic_value < 1000) - m.transaction(caller=attacker_account, - address=contract_account, - data=data, - value=symbolic_value ) + symbolic_value = m.make_symbolic_value() + m.constrain(symbolic_value > 100) + m.constrain(symbolic_value < 1000) + m.transaction(caller=attacker_account, + address=contract_account, + data=data, + value=symbolic_value ) """ avoid_collisions = False @@ -319,16 +319,16 @@ def _compile_through_crytic_compile(filename, contract_name, libraries, crytic_c @staticmethod def _compile(source_code, contract_name, libraries=None, crytic_compile_args=None): - """ Compile a Solidity contract, used internally - - :param source_code: solidity source - :type source_code: string (filename, directory, etherscan address) or a file handle - :param contract_name: a string with the name of the contract to analyze - :param libraries: an itemizable of pairs (library_name, address) - :param crytic_compile_args: crytic compile options (https://github.com/crytic/crytic-compile/wiki/Configuration) - :type crytic_compile_args: dict - :return: name, source_code, bytecode, srcmap, srcmap_runtime, hashes - :return: name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi, warnings + """Compile a Solidity contract, used internally + + :param source_code: solidity source + :type source_code: string (filename, directory, etherscan address) or a file handle + :param contract_name: a string with the name of the contract to analyze + :param libraries: an itemizable of pairs (library_name, address) + :param crytic_compile_args: crytic compile options (https://github.com/crytic/crytic-compile/wiki/Configuration) + :type crytic_compile_args: dict + :return: name, source_code, bytecode, srcmap, srcmap_runtime, hashes + :return: name, source_code, bytecode, runtime, srcmap, srcmap_runtime, hashes, abi, warnings """ crytic_compile_args = dict() if crytic_compile_args is None else crytic_compile_args @@ -336,10 +336,13 @@ def _compile(source_code, contract_name, libraries=None, crytic_compile_args=Non if isinstance(source_code, io.IOBase): source_code = source_code.name - if (isinstance(source_code, str) and - not is_supported(source_code) and - # Until https://github.com/crytic/crytic-compile/issues/103 is implemented - "ignore_compile" not in crytic_compile_args): + if ( + isinstance(source_code, str) + and not is_supported(source_code) + and + # Until https://github.com/crytic/crytic-compile/issues/103 is implemented + "ignore_compile" not in crytic_compile_args + ): with tempfile.NamedTemporaryFile("w+", suffix=".sol") as temp: temp.write(source_code) temp.flush() @@ -489,7 +492,7 @@ def human_transactions(self, state_id=None): def make_symbolic_arguments(self, types): """ - Build a reasonable set of symbolic arguments matching the types list + Build a reasonable set of symbolic arguments matching the types list """ from . import abitypes @@ -542,24 +545,24 @@ def solidity_create_contract( gas=None, compile_args=None, ): - """ Creates a solidity contract and library dependencies - - :param source_code: solidity source code - :type source_code: string (filename, directory, etherscan address) or a file handle - :param owner: owner account (will be default caller in any transactions) - :type owner: int or EVMAccount - :param contract_name: Name of the contract to analyze (optional if there is a single one in the source code) - :type contract_name: str - :param balance: balance to be transferred on creation - :type balance: int or BitVecVariable - :param address: the address for the new contract (optional) - :type address: int or EVMAccount - :param tuple args: constructor arguments - :param compile_args: crytic compile options #FIXME(https://github.com/crytic/crytic-compile/wiki/Configuration) - :type compile_args: dict - :param gas: gas budget for each contract creation needed (may be more than one if several related contracts defined in the solidity source) - :type gas: int - :rtype: EVMAccount + """Creates a solidity contract and library dependencies + + :param source_code: solidity source code + :type source_code: string (filename, directory, etherscan address) or a file handle + :param owner: owner account (will be default caller in any transactions) + :type owner: int or EVMAccount + :param contract_name: Name of the contract to analyze (optional if there is a single one in the source code) + :type contract_name: str + :param balance: balance to be transferred on creation + :type balance: int or BitVecVariable + :param address: the address for the new contract (optional) + :type address: int or EVMAccount + :param tuple args: constructor arguments + :param compile_args: crytic compile options #FIXME(https://github.com/crytic/crytic-compile/wiki/Configuration) + :type compile_args: dict + :param gas: gas budget for each contract creation needed (may be more than one if several related contracts defined in the solidity source) + :type gas: int + :rtype: EVMAccount """ if compile_args is None: compile_args = dict() @@ -665,17 +668,17 @@ def get_nonce(self, address): return next(iter(nonces)) def create_contract(self, owner, balance=0, address=None, init=None, name=None, gas=None): - """ Creates a contract - - :param owner: owner account (will be default caller in any transactions) - :type owner: int or EVMAccount - :param balance: balance to be transferred on creation - :type balance: int or BitVecVariable - :param int address: the address for the new contract (optional) - :param str init: initializing evm bytecode and arguments - :param str name: a unique name for reference - :param gas: gas budget for the creation/initialization of the contract - :rtype: EVMAccount + """Creates a contract + + :param owner: owner account (will be default caller in any transactions) + :type owner: int or EVMAccount + :param balance: balance to be transferred on creation + :type balance: int or BitVecVariable + :param int address: the address for the new contract (optional) + :param str init: initializing evm bytecode and arguments + :param str name: a unique name for reference + :param gas: gas budget for the creation/initialization of the contract + :rtype: EVMAccount """ if not self.count_ready_states(): raise NoAliveStates @@ -751,34 +754,34 @@ def end_block(self): world.end_block() def transaction(self, caller, address, value, data, gas=None, price=1): - """ Issue a symbolic transaction in all running states - - :param caller: the address of the account sending the transaction - :type caller: int or EVMAccount - :param address: the address of the contract to call - :type address: int or EVMAccount - :param value: balance to be transfered on creation - :type value: int or BitVecVariable - :param data: initial data - :param gas: gas budget - :param price: gas unit price - :raises NoAliveStates: if there are no alive states to execute + """Issue a symbolic transaction in all running states + + :param caller: the address of the account sending the transaction + :type caller: int or EVMAccount + :param address: the address of the contract to call + :type address: int or EVMAccount + :param value: balance to be transfered on creation + :type value: int or BitVecVariable + :param data: initial data + :param gas: gas budget + :param price: gas unit price + :raises NoAliveStates: if there are no alive states to execute """ self._transaction( "CALL", caller, value=value, address=address, data=data, gas=gas, price=price ) def create_account(self, balance=0, address=None, code=None, name=None, nonce=None): - """ Low level creates an account. This won't generate a transaction. - - :param balance: balance to be set on creation (optional) - :type balance: int or BitVecVariable - :param address: the address for the new account (optional) - :type address: int - :param code: the runtime code for the new account (None means normal account), str or bytes (optional) - :param nonce: force a specific nonce - :param name: a global account name eg. for use as reference in the reports (optional) - :return: an EVMAccount + """Low level creates an account. This won't generate a transaction. + + :param balance: balance to be set on creation (optional) + :type balance: int or BitVecVariable + :param address: the address for the new account (optional) + :type address: int + :param code: the runtime code for the new account (None means normal account), str or bytes (optional) + :param nonce: force a specific nonce + :param name: a global account name eg. for use as reference in the reports (optional) + :return: an EVMAccount """ # Need at least one state where to apply this if not self.count_ready_states(): @@ -874,17 +877,17 @@ def _migrate_tx_expressions(self, state, caller, address, value, data, gas, pric return caller, address, value, data, gas, price def _transaction(self, sort, caller, value=0, address=None, data=None, gas=None, price=1): - """ Initiates a transaction - - :param caller: caller account - :type caller: int or EVMAccount - :param int address: the address for the transaction (optional) - :param value: value to be transferred - :param price: the price of gas for this transaction. - :type value: int or BitVecVariable - :param str data: initializing evm bytecode and arguments or transaction call data - :param gas: gas budget for current transaction - :rtype: EVMAccount + """Initiates a transaction + + :param caller: caller account + :type caller: int or EVMAccount + :param int address: the address for the transaction (optional) + :param value: value to be transferred + :param price: the price of gas for this transaction. + :type value: int or BitVecVariable + :param str data: initializing evm bytecode and arguments or transaction call data + :param gas: gas budget for current transaction + :rtype: EVMAccount """ if gas is None: gas = consts.defaultgas @@ -991,13 +994,13 @@ def preconstraint_for_call_transaction( value: Optional[Union[int, Expression]] = None, contract_metadata: Optional[SolidityMetadata] = None, ): - """ Returns a constraint that excludes combinations of value and data that would cause an exception in the EVM - contract dispatcher. + """Returns a constraint that excludes combinations of value and data that would cause an exception in the EVM + contract dispatcher. - :param address: address of the contract to call - :param value: balance to be transferred (optional) - :param data: symbolic transaction data - :param contract_metadata: SolidityMetadata for the contract (optional) + :param address: address of the contract to call + :param value: balance to be transferred (optional) + :param data: symbolic transaction data + :param contract_metadata: SolidityMetadata for the contract (optional) """ if isinstance(address, EVMAccount): address = int(address) @@ -1034,12 +1037,12 @@ def preconstraint_for_call_transaction( def local_coverage_progress(self) -> bool: for state in self.ready_states: - new_local_coverage = len(set(state.context['evm.trace'])) - if 'evm.localcoverage' in state.context: - old_local_coverage = state.context['evm.localcoverage'] + new_local_coverage = len(set(state.context["evm.trace"])) + if "evm.localcoverage" in state.context: + old_local_coverage = state.context["evm.localcoverage"] else: old_local_coverage = 0 - state.context['evm.localcoverage'] = new_local_coverage + state.context["evm.localcoverage"] = new_local_coverage if new_local_coverage != old_local_coverage: return True return False @@ -1094,7 +1097,9 @@ def multi_tx_analysis( prev_coverage = 0 current_coverage = 0 tx_no = 0 - while (current_coverage < 100 or tx_use_coverage is tx_use_coverage.no) and not self.is_killed(): + while ( + current_coverage < 100 or tx_use_coverage is tx_use_coverage.no + ) and not self.is_killed(): try: logger.info("Starting symbolic transaction: %d", tx_no) @@ -1153,8 +1158,7 @@ def multi_tx_analysis( logger.info("No state made any progress") break except Exception as e: - print (e) - + print(e) tx_no += 1 @@ -1292,8 +1296,8 @@ def _on_unsound_symbolication(self, state, func, data, result): result.append(value) def fix_unsound_symbolication_fake(self, state): - """ This method goes through all the applied symbolic functions and tries - to find a concrete matching set of pairs + """This method goes through all the applied symbolic functions and tries + to find a concrete matching set of pairs """ def make_cond(state, table): @@ -1311,8 +1315,8 @@ def make_cond(state, table): return state.can_be_true(True) def fix_unsound_symbolication_sound(self, state): - """ This method goes through all the applied symbolic functions and tries - to find a concrete matching set of pairs + """This method goes through all the applied symbolic functions and tries + to find a concrete matching set of pairs """ def concretize_known_pairs(state, symbolic_pairs, known_pairs): @@ -1329,7 +1333,7 @@ def concretize_known_pairs(state, symbolic_pairs, known_pairs): return def match(state, func, symbolic_pairs, concrete_pairs, start=None): - """ Tries to find a concrete match for the symbolic pairs. It uses + """Tries to find a concrete match for the symbolic pairs. It uses concrete_pairs (and potentially extends it with solved pairs) until a matching set of concrete pairs is found, or fail. @@ -1446,9 +1450,9 @@ def fix_unsound_symbolication(self, state): return state.context["soundcheck"] def _terminate_state_callback(self, state, e): - """ INTERNAL USE - Every time a state finishes executing the last transaction, we save it in - our private list + """INTERNAL USE + Every time a state finishes executing the last transaction, we save it in + our private list """ if isinstance(e, AbandonState): # do nothing @@ -1505,8 +1509,8 @@ def _did_evm_execute_instruction_callback(self, state, instruction, arguments, r ) def get_metadata(self, address) -> Optional[SolidityMetadata]: - """ Gets the solidity metadata for address. - This is available only if address is a contract created from solidity + """Gets the solidity metadata for address. + This is available only if address is a contract created from solidity """ return self.metadata.get(address) @@ -1871,9 +1875,9 @@ def worker_finalize(q): self.remove_all() def global_coverage(self, account): - """ Returns code coverage for the contract on `account_address`. - This sums up all the visited code lines from any of the explored - states. + """Returns code coverage for the contract on `account_address`. + This sums up all the visited code lines from any of the explored + states. """ account_address = int(account) runtime_bytecode = None From 70b1fddd91533c84ee9c582db5a81c426b653b38 Mon Sep 17 00:00:00 2001 From: feliam Date: Wed, 2 Sep 2020 12:43:28 -0300 Subject: [PATCH 3/3] Add/fix tests --- manticore/__init__.py | 3 ++- manticore/ethereum/__init__.py | 2 +- manticore/ethereum/cli.py | 22 --------------- manticore/ethereum/manticore.py | 28 ++++++++++++++++--- manticore/utils/log.py | 3 +-- tests/ethereum/test_general.py | 43 ++++++++++++++++++++++++++++-- tests/ethereum/test_regressions.py | 2 +- 7 files changed, 71 insertions(+), 32 deletions(-) diff --git a/manticore/__init__.py b/manticore/__init__.py index 753996dbb..b1e308103 100644 --- a/manticore/__init__.py +++ b/manticore/__init__.py @@ -7,7 +7,7 @@ from .utils import config, log from .utils.log import set_verbosity from .core.smtlib import issymbolic, istainted -from .ethereum.manticore import ManticoreEVM +from .ethereum.manticore import ManticoreEVM, TermCondCovType from .core.plugin import Plugin from .exceptions import ManticoreError @@ -17,4 +17,5 @@ ManticoreEVM.__name__, set_verbosity.__name__, ManticoreError.__name__, + TermCondCovType.__name__ ] diff --git a/manticore/ethereum/__init__.py b/manticore/ethereum/__init__.py index 068a7c8be..56ba3c9d6 100644 --- a/manticore/ethereum/__init__.py +++ b/manticore/ethereum/__init__.py @@ -1,6 +1,6 @@ # Exports (for `from manticore.ethereum import ...`) from .abi import ABI -from .manticore import ManticoreEVM, config +from .manticore import ManticoreEVM, config, TermCondCovType from .state import State from .detectors import ( Detector, diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index 322d5ee95..ec4e073ed 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -42,28 +42,6 @@ from enum import Enum - -class TermCondCovType(Enum): - """Used as configuration constant for choosing the coverage based termination - condition""" - - no = "no" - local = "local" - wide = "wide" - - def title(self): - return self._name_.title() - - @classmethod - def from_string(cls, name): - return cls.__members__[name] - - -consts.add( - "txcoverage", default=TermCondCovType.local, description="Set coverage stopping criteria" -) - - def get_detectors_classes(): return [ DetectInvalid, diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 7a1440ce6..a8433f950 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -71,6 +71,25 @@ def from_string(cls, name): "Default timeout for matching sha3 for unsound states (see unsound symbolication).", ) +class TermCondCovType(Enum): + """Used as configuration constant for choosing the coverage based termination + condition""" + + no = "no" + local = "local" + wide = "wide" + + def title(self): + return self._name_.title() + + @classmethod + def from_string(cls, name): + return cls.__members__[name] + + +consts.add( + "txcoverage", default=TermCondCovType.local, description="Set coverage stopping criteria" +) def flagged(flag): """ @@ -1035,6 +1054,7 @@ def preconstraint_for_call_transaction( return constraint + @ManticoreBase.sync def local_coverage_progress(self) -> bool: for state in self.ready_states: new_local_coverage = len(set(state.context["evm.trace"])) @@ -1044,15 +1064,17 @@ def local_coverage_progress(self) -> bool: old_local_coverage = 0 state.context["evm.localcoverage"] = new_local_coverage if new_local_coverage != old_local_coverage: - return True - return False + continue + self._ready_states.remove(state.id) + self._terminated_states.append(state.id) + return self.count_ready_states() > 0 def multi_tx_analysis( self, solidity_filename, contract_name=None, tx_limit=None, - tx_use_coverage=True, + tx_use_coverage=TermCondCovType.local, tx_send_ether=True, tx_account="attacker", tx_preconstrain=False, diff --git a/manticore/utils/log.py b/manticore/utils/log.py index f49595f0a..f54155dcc 100644 --- a/manticore/utils/log.py +++ b/manticore/utils/log.py @@ -61,8 +61,7 @@ def filter(self, record) -> bool: ctxfilter = ContextFilter() - -class CustomLogger(logging.Logger): +class CustomLogger(logging.getLoggerClass()): """ Custom Logger class that can grab the correct verbosity level from this module """ diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index dc408c9da..e910688da 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -21,7 +21,6 @@ from manticore.core.state import TerminateState from manticore.ethereum import ( ManticoreEVM, - State, DetectExternalCallAndLeak, DetectIntegerOverflow, Detector, @@ -30,11 +29,12 @@ EthereumError, EVMContract, verifier, + TermCondCovType ) from manticore.ethereum.plugins import FilterFunctions from manticore.ethereum.solidity import SolidityMetadata from manticore.platforms import evm -from manticore.platforms.evm import EVMWorld, ConcretizeArgument, concretized_args, Return, Stop +from manticore.platforms.evm import ConcretizeArgument, concretized_args, Return, Stop from manticore.utils.deprecated import ManticoreDeprecationWarning from manticore.utils import config import io @@ -68,6 +68,45 @@ def test_int_ovf(self): self.assertIn("Unsigned integer overflow at ADD instruction", all_findings) self.assertIn("Unsigned integer overflow at MUL instruction", all_findings) + def test_multitx_term_cond_wide(self): + + mevm = ManticoreEVM() + source_code = """ + contract MotivatingExample { + event Log(string); + int private stateA = 0; + int private stateB = 0; + function f(int input) public { + stateA=input; + } + function g() public { + stateB = stateA; + } + function h() payable public { + if(stateB == 61){ + emit Log("Bug found"); + } + } +}""" + #This will stop before the bug is found + mevm.multi_tx_analysis(source_code, tx_use_coverage=TermCondCovType.wide ) + found_log = 0 + for state in mevm.all_states: + if state.platform.logs: + found_log += 1 + self.assertEqual(found_log,0) + + + #This will never stop :joy: + mevm = ManticoreEVM() + with mevm.kill_timeout(timeout=600): + mevm.multi_tx_analysis(source_code, tx_limit=4, tx_use_coverage=TermCondCovType.local ) + found_log = 0 + for state in mevm.all_states: + if state.platform.logs: + found_log += 1 + self.assertGreater(found_log,0) + class EthVerifierIntegrationTest(unittest.TestCase): def test_propverif(self): diff --git a/tests/ethereum/test_regressions.py b/tests/ethereum/test_regressions.py index f55ff457a..738922e63 100644 --- a/tests/ethereum/test_regressions.py +++ b/tests/ethereum/test_regressions.py @@ -118,7 +118,7 @@ def test_solidity_timeout(self): def test_regressions_676(self): issue = {"number": 676, "contract": None, "txlimit": 1} - self._simple_cli_run( + self. _simple_cli_run( f'{issue["number"]}.sol', contract=issue["contract"], tx_limit=issue["txlimit"],