From c72ac81de18e1981c00aec7e3d2414912eb1e5b6 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 31 Dec 2021 18:21:49 +0000 Subject: [PATCH] Add more precompile tests (#1576) * Add tests for natives * Black updates * Update black --- .circleci/config.yml | 2 +- .pre-commit-config.yaml | 2 +- mypy-stubs/z3/__init__.pyi | 1 + mythril/analysis/module/base.py | 4 +- mythril/analysis/module/loader.py | 2 +- mythril/analysis/module/modules/exceptions.py | 2 +- mythril/analysis/module/modules/integer.py | 4 +- .../module/modules/user_assertions.py | 6 +- mythril/analysis/module/util.py | 2 +- mythril/analysis/report.py | 8 +- mythril/analysis/security.py | 4 +- mythril/analysis/solver.py | 8 +- mythril/interfaces/cli.py | 6 +- .../exponent_function_manager.py | 11 +-- .../keccak_function_manager.py | 2 +- mythril/laser/ethereum/instructions.py | 4 +- mythril/laser/ethereum/iprof.py | 3 +- mythril/laser/ethereum/natives.py | 7 +- mythril/laser/ethereum/state/machine_state.py | 2 +- mythril/laser/ethereum/state/world_state.py | 2 +- .../strategy/extensions/bounded_loops.py | 2 +- mythril/laser/ethereum/svm.py | 8 +- mythril/laser/plugin/builder.py | 2 +- mythril/laser/plugin/interface.py | 4 +- mythril/laser/plugin/loader.py | 8 +- .../plugins/coverage/coverage_strategy.py | 2 +- .../laser/plugin/plugins/dependency_pruner.py | 24 ++--- .../plugin/plugins/instruction_profiler.py | 3 +- mythril/laser/plugin/signals.py | 4 +- mythril/laser/smt/__init__.py | 2 +- mythril/laser/smt/expression.py | 4 +- mythril/laser/smt/model.py | 12 +-- .../laser/smt/solver/independence_solver.py | 15 ++- mythril/laser/smt/solver/solver_statistics.py | 2 +- mythril/mythril/mythril_disassembler.py | 2 +- mythril/plugin/discovery.py | 4 +- mythril/plugin/interface.py | 2 +- mythril/support/support_utils.py | 4 +- tests/laser/Precompiles/test_ecrecover.py | 67 +++++++++++++ tests/laser/Precompiles/test_identity.py | 13 +++ tests/laser/Precompiles/test_ripemd.py | 95 +++++++++++++++++++ tests/laser/Precompiles/test_sha256.py | 95 +++++++++++++++++++ 42 files changed, 354 insertions(+), 102 deletions(-) create mode 100644 tests/laser/Precompiles/test_ecrecover.py create mode 100644 tests/laser/Precompiles/test_identity.py create mode 100644 tests/laser/Precompiles/test_ripemd.py create mode 100644 tests/laser/Precompiles/test_sha256.py diff --git a/.circleci/config.yml b/.circleci/config.yml index 1981c40d..a45004ac 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -40,7 +40,7 @@ jobs: - run: name: Black style check command: | - pip3 install --user black==19.10b0 + pip3 install --user black==21.12b0 python3 -m black --check /home/mythril/ - run: diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index f0b82b07..0807b4df 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -2,6 +2,6 @@ # See https://pre-commit.com/hooks.html for more hooks repos: - repo: https://github.com/psf/black - rev: 19.3b0 + rev: 21.12b0 hooks: - id: black diff --git a/mypy-stubs/z3/__init__.pyi b/mypy-stubs/z3/__init__.pyi index 9668d7c0..08e6456d 100644 --- a/mypy-stubs/z3/__init__.pyi +++ b/mypy-stubs/z3/__init__.pyi @@ -168,6 +168,7 @@ class Optimize(Z3PPObject): sat: CheckSatResult = ... unsat: CheckSatResult = ... + @overload def Int(name: str) -> ArithRef: ... @overload diff --git a/mythril/analysis/module/base.py b/mythril/analysis/module/base.py index 4c8c7561..0459cf2a 100644 --- a/mythril/analysis/module/base.py +++ b/mythril/analysis/module/base.py @@ -17,7 +17,7 @@ log = logging.getLogger(__name__) class EntryPoint(Enum): - """ EntryPoint Enum + """EntryPoint Enum This enum is used to signify the entry_point of detection modules. See also the class documentation of DetectionModule @@ -54,7 +54,7 @@ class DetectionModule(ABC): self.cache = set() # type: Set[Optional[Union[int, Tuple[int, str]]]] def reset_module(self): - """ Resets the storage of this module """ + """Resets the storage of this module""" self.issues = [] def execute(self, target: GlobalState) -> Optional[List[Issue]]: diff --git a/mythril/analysis/module/loader.py b/mythril/analysis/module/loader.py index 05c3b74c..35c35730 100644 --- a/mythril/analysis/module/loader.py +++ b/mythril/analysis/module/loader.py @@ -51,7 +51,7 @@ class ModuleLoader(object, metaclass=Singleton): entry_point: Optional[EntryPoint] = None, white_list: Optional[List[str]] = None, ) -> List[DetectionModule]: - """ Gets registered detection modules + """Gets registered detection modules :param entry_point: If specified: only return detection modules with this entry point :param white_list: If specified: only return whitelisted detection modules diff --git a/mythril/analysis/module/modules/exceptions.py b/mythril/analysis/module/modules/exceptions.py index 0c1d523b..4fab643b 100644 --- a/mythril/analysis/module/modules/exceptions.py +++ b/mythril/analysis/module/modules/exceptions.py @@ -18,7 +18,7 @@ PANIC_SIGNATURE = [78, 72, 123, 113] class LastJumpAnnotation(StateAnnotation): - """ State Annotation used if an overflow is both possible and used in the annotated path""" + """State Annotation used if an overflow is both possible and used in the annotated path""" def __init__(self, last_jump: int = None) -> None: self.last_jump: int = last_jump diff --git a/mythril/analysis/module/modules/integer.py b/mythril/analysis/module/modules/integer.py index adc2e2fb..c5f994c7 100644 --- a/mythril/analysis/module/modules/integer.py +++ b/mythril/analysis/module/modules/integer.py @@ -31,7 +31,7 @@ log = logging.getLogger(__name__) class OverUnderflowAnnotation: - """ Symbol Annotation used if a BitVector can overflow""" + """Symbol Annotation used if a BitVector can overflow""" def __init__( self, overflowing_state: GlobalState, operator: str, constraint: Bool @@ -46,7 +46,7 @@ class OverUnderflowAnnotation: class OverUnderflowStateAnnotation(StateAnnotation): - """ State Annotation used if an overflow is both possible and used in the annotated path""" + """State Annotation used if an overflow is both possible and used in the annotated path""" def __init__(self) -> None: self.overflowing_state_annotations = set() # type: Set[OverUnderflowAnnotation] diff --git a/mythril/analysis/module/modules/user_assertions.py b/mythril/analysis/module/modules/user_assertions.py index c6b8b2d2..62c042d6 100644 --- a/mythril/analysis/module/modules/user_assertions.py +++ b/mythril/analysis/module/modules/user_assertions.py @@ -87,8 +87,10 @@ class UserAssertions(DetectionModule): ) if message: - description_tail = "A user-provided assertion failed with the message '{}'".format( - message + description_tail = ( + "A user-provided assertion failed with the message '{}'".format( + message + ) ) else: diff --git a/mythril/analysis/module/util.py b/mythril/analysis/module/util.py index cffae14a..1c9b3b97 100644 --- a/mythril/analysis/module/util.py +++ b/mythril/analysis/module/util.py @@ -13,7 +13,7 @@ OP_CODE_LIST = OPCODES.keys() def get_detection_module_hooks( modules: List[DetectionModule], hook_type="pre" ) -> Dict[str, List[Callable]]: - """ Gets a dictionary with the hooks for the passed detection modules + """Gets a dictionary with the hooks for the passed detection modules :param modules: The modules for which to retrieve hooks :param hook_type: The type of hooks to retrieve (default: "pre") diff --git a/mythril/analysis/report.py b/mythril/analysis/report.py index ea31a10e..ac714dfd 100644 --- a/mythril/analysis/report.py +++ b/mythril/analysis/report.py @@ -71,12 +71,12 @@ class Issue: @property def transaction_sequence_users(self): - """ Returns the transaction sequence without pre-generated block data""" + """Returns the transaction sequence without pre-generated block data""" return self.transaction_sequence @property def transaction_sequence_jsonv2(self): - """ Returns the transaction sequence as a json string with pre-generated block data""" + """Returns the transaction sequence as a json string with pre-generated block data""" return ( self.add_block_data(self.transaction_sequence) if self.transaction_sequence @@ -85,7 +85,7 @@ class Issue: @staticmethod def add_block_data(transaction_sequence: Dict): - """ Adds sane block data to a transaction_sequence """ + """Adds sane block data to a transaction_sequence""" for step in transaction_sequence["steps"]: step["gasLimit"] = "0x7d000" step["gasPrice"] = "0x773594000" @@ -167,7 +167,7 @@ class Issue: self.source_mapping = self.address def resolve_function_names(self): - """ Resolves function names for each step """ + """Resolves function names for each step""" if ( self.transaction_sequence is None diff --git a/mythril/analysis/security.py b/mythril/analysis/security.py index 2fd0a63e..e53da210 100644 --- a/mythril/analysis/security.py +++ b/mythril/analysis/security.py @@ -12,7 +12,7 @@ log = logging.getLogger(__name__) def retrieve_callback_issues(white_list: Optional[List[str]] = None) -> List[Issue]: - """ Get the issues discovered by callback type detection modules""" + """Get the issues discovered by callback type detection modules""" issues = [] # type: List[Issue] for module in ModuleLoader().get_detection_modules( entry_point=EntryPoint.CALLBACK, white_list=white_list @@ -26,7 +26,7 @@ def retrieve_callback_issues(white_list: Optional[List[str]] = None) -> List[Iss def fire_lasers(statespace, white_list: Optional[List[str]] = None) -> List[Issue]: - """ Fire lasers at analysed statespace object + """Fire lasers at analysed statespace object :param statespace: Symbolic statespace to analyze :param white_list: Optionally whitelist modules to use for the analysis diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index 760c8c2a..83f2deee 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -24,7 +24,7 @@ log = logging.getLogger(__name__) def pretty_print_model(model): - """ Pretty prints a z3 model + """Pretty prints a z3 model :param model: :return: @@ -161,7 +161,7 @@ def _replace_with_actual_sha( def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]): - """ Gets a concrete state """ + """Gets a concrete state""" accounts = {} for address, account in initial_accounts.items(): # Skip empty default account @@ -176,7 +176,7 @@ def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]): def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction): - """ Gets a concrete transaction from a transaction and z3 model""" + """Gets a concrete transaction from a transaction and z3 model""" # Get concrete values from transaction address = hex(transaction.callee_account.address.value) value = model.eval(transaction.call_value.raw, model_completion=True).as_long() @@ -210,7 +210,7 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction): def _set_minimisation_constraints( transaction_sequence, constraints, minimize, max_size, world_state ) -> Tuple[Constraints, tuple]: - """ Set constraints that minimise key transaction values + """Set constraints that minimise key transaction values Constraints generated: - Upper bound on calldata size diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index 129315d9..c16ff23b 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -23,11 +23,7 @@ from mythril.exceptions import ( ) from mythril.laser.ethereum.transaction.symbolic import ACTORS from mythril.plugin.loader import MythrilPluginLoader -from mythril.mythril import ( - MythrilAnalyzer, - MythrilDisassembler, - MythrilConfig, -) +from mythril.mythril import MythrilAnalyzer, MythrilDisassembler, MythrilConfig from mythril.analysis.module import ModuleLoader from mythril.analysis.report import Report diff --git a/mythril/laser/ethereum/function_managers/exponent_function_manager.py b/mythril/laser/ethereum/function_managers/exponent_function_manager.py index 4c280eb8..40742e28 100644 --- a/mythril/laser/ethereum/function_managers/exponent_function_manager.py +++ b/mythril/laser/ethereum/function_managers/exponent_function_manager.py @@ -2,14 +2,7 @@ import logging from typing import Dict, List, Optional, Tuple -from mythril.laser.smt import ( - And, - BitVec, - Bool, - Function, - URem, - symbol_factory, -) +from mythril.laser.smt import And, BitVec, Bool, Function, URem, symbol_factory log = logging.getLogger(__name__) @@ -19,7 +12,7 @@ class ExponentFunctionManager: Uses an uninterpreted function for exponentiation with the following properties: 1) power(a, b) > 0 2) if a = 256 => forall i if b = i then power(a, b) = (256 ^ i) % (2^256) - + Only these two properties are added as to handle indexing of boolean arrays. Caution should be exercised when increasing the conditions since it severely affects the solving time. diff --git a/mythril/laser/ethereum/function_managers/keccak_function_manager.py b/mythril/laser/ethereum/function_managers/keccak_function_manager.py index 4df4980b..7e640a5a 100644 --- a/mythril/laser/ethereum/function_managers/keccak_function_manager.py +++ b/mythril/laser/ethereum/function_managers/keccak_function_manager.py @@ -62,7 +62,7 @@ class KeccakFunctionManager: """ keccak = symbol_factory.BitVecVal( int.from_bytes( - sha3(data.value.to_bytes(data.size() // 8, byteorder="big")), "big", + sha3(data.value.to_bytes(data.size() // 8, byteorder="big")), "big" ), 256, ) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index a92036c3..ea031e73 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -656,9 +656,7 @@ class Instruction: If( s0 <= 31, If( - sign_bit_set, - s1 | (TT256 - set_testbit), - s1 & (set_testbit - 1), + sign_bit_set, s1 | (TT256 - set_testbit), s1 & (set_testbit - 1) ), s1, ) diff --git a/mythril/laser/ethereum/iprof.py b/mythril/laser/ethereum/iprof.py index a81c6b3b..83a49416 100644 --- a/mythril/laser/ethereum/iprof.py +++ b/mythril/laser/ethereum/iprof.py @@ -24,8 +24,7 @@ _InstrExecStatistics = Dict[str, _InstrExecStatistic] class InstructionProfiler: - """Performance profile for the execution of each instruction. - """ + """Performance profile for the execution of each instruction.""" def __init__(self): self.records = dict() diff --git a/mythril/laser/ethereum/natives.py b/mythril/laser/ethereum/natives.py index ba3952eb..8f920e99 100644 --- a/mythril/laser/ethereum/natives.py +++ b/mythril/laser/ethereum/natives.py @@ -134,11 +134,6 @@ def identity(data: List[int]) -> List[int]: :param data: :return: """ - # Group up into an array of 32 byte words instead - # of an array of bytes. If saved to memory, 32 byte - # words are currently needed, but a correct memory - # implementation would be byte indexed for the most - # part. return data @@ -279,7 +274,7 @@ def native_contracts(address: int, data: BaseCalldata) -> List[int]: """ if not isinstance(data, ConcreteCalldata): - raise NativeContractException() + raise NativeContractException concrete_data = data.concrete(None) try: return PRECOMPILE_FUNCTIONS[address - 1](concrete_data) diff --git a/mythril/laser/ethereum/state/machine_state.py b/mythril/laser/ethereum/state/machine_state.py index a0070911..ac87eaf2 100644 --- a/mythril/laser/ethereum/state/machine_state.py +++ b/mythril/laser/ethereum/state/machine_state.py @@ -93,7 +93,7 @@ class MachineStack(list): class MachineState: """ - MachineState represents current machine state also referenced to as \mu. + MachineState represents current machine state also referenced to as \mu. """ def __init__( diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py index 763cbe6c..55bd84b9 100644 --- a/mythril/laser/ethereum/state/world_state.py +++ b/mythril/laser/ethereum/state/world_state.py @@ -115,7 +115,7 @@ class WorldState: except ValueError: code = None return self.create_account( - address=addr_bitvec.value, dynamic_loader=dynamic_loader, code=code, + address=addr_bitvec.value, dynamic_loader=dynamic_loader, code=code ) def create_account( diff --git a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py index d4a7639d..85c6eb25 100644 --- a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py +++ b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py @@ -102,7 +102,7 @@ class BoundedLoopsStrategy(BasicSearchStrategy): return count def get_strategic_global_state(self) -> GlobalState: - """ Returns the next state + """Returns the next state :return: Global state """ diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 66cb040b..e5876423 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -125,7 +125,7 @@ class LaserEVM: creation_code: str = None, contract_name: str = None, ) -> None: - """ Starts symbolic execution + """Starts symbolic execution There are two modes of execution. Either we analyze a preconfigured configuration, in which case the world_state and target_address variables must be supplied. @@ -274,7 +274,7 @@ class LaserEVM: return final_states if track_gas else None def _add_world_state(self, global_state: GlobalState): - """ Stores the world_state of the passed global state in the open states""" + """Stores the world_state of the passed global state in the open states""" for hook in self._add_world_state_hooks: try: @@ -612,7 +612,7 @@ class LaserEVM: """ def hook_decorator(func: Callable): - """ Hook decorator generated by laser_hook + """Hook decorator generated by laser_hook :param func: Decorated function """ @@ -628,7 +628,7 @@ class LaserEVM: """ def hook_decorator(func: Callable): - """ Hook decorator generated by laser_hook + """Hook decorator generated by laser_hook :param func: Decorated function """ diff --git a/mythril/laser/plugin/builder.py b/mythril/laser/plugin/builder.py index c4f08211..51f8d546 100644 --- a/mythril/laser/plugin/builder.py +++ b/mythril/laser/plugin/builder.py @@ -5,7 +5,7 @@ from typing import Optional class PluginBuilder(ABC): - """ PluginBuilder + """PluginBuilder The plugin builder interface enables construction of Laser plugins """ diff --git a/mythril/laser/plugin/interface.py b/mythril/laser/plugin/interface.py index 55fbdb72..02eb29c2 100644 --- a/mythril/laser/plugin/interface.py +++ b/mythril/laser/plugin/interface.py @@ -2,7 +2,7 @@ from mythril.laser.ethereum.svm import LaserEVM class LaserPlugin: - """ Base class for laser plugins + """Base class for laser plugins Functionality in laser that the symbolic execution process does not need to depend on can be implemented in the form of a laser plugin. @@ -16,7 +16,7 @@ class LaserPlugin: """ def initialize(self, symbolic_vm: LaserEVM) -> None: - """ Initializes this plugin on the symbolic virtual machine + """Initializes this plugin on the symbolic virtual machine :param symbolic_vm: symbolic virtual machine to initialize the laser plugin on """ diff --git a/mythril/laser/plugin/loader.py b/mythril/laser/plugin/loader.py index 19f793a1..01b03fbc 100644 --- a/mythril/laser/plugin/loader.py +++ b/mythril/laser/plugin/loader.py @@ -15,7 +15,7 @@ class LaserPluginLoader(object, metaclass=Singleton): """ def __init__(self) -> None: - """ Initializes the plugin loader """ + """Initializes the plugin loader""" self.laser_plugin_builders = {} # type: Dict[str, PluginBuilder] self.plugin_args = {} # type: Dict[str, Dict] @@ -23,7 +23,7 @@ class LaserPluginLoader(object, metaclass=Singleton): self.plugin_args[plugin_name] = kwargs def load(self, plugin_builder: PluginBuilder) -> None: - """ Enables a Laser Plugin + """Enables a Laser Plugin :param plugin_builder: Builder that constructs the plugin """ @@ -36,7 +36,7 @@ class LaserPluginLoader(object, metaclass=Singleton): self.laser_plugin_builders[plugin_builder.name] = plugin_builder def is_enabled(self, plugin_name: str) -> bool: - """ Returns whether the plugin is loaded in the symbolic_vm + """Returns whether the plugin is loaded in the symbolic_vm :param plugin_name: Name of the plugin to check """ @@ -53,7 +53,7 @@ class LaserPluginLoader(object, metaclass=Singleton): def instrument_virtual_machine( self, symbolic_vm: LaserEVM, with_plugins: Optional[List[str]] ): - """ Load enabled plugins into the passed symbolic virtual machine + """Load enabled plugins into the passed symbolic virtual machine :param symbolic_vm: The virtual machine to instrument the plugins with :param with_plugins: Override the globally enabled/disabled builders and load all plugins in the list """ diff --git a/mythril/laser/plugin/plugins/coverage/coverage_strategy.py b/mythril/laser/plugin/plugins/coverage/coverage_strategy.py index 94ca65b3..a8b7809d 100644 --- a/mythril/laser/plugin/plugins/coverage/coverage_strategy.py +++ b/mythril/laser/plugin/plugins/coverage/coverage_strategy.py @@ -35,7 +35,7 @@ class CoverageStrategy(BasicSearchStrategy): return self.super_strategy.get_strategic_global_state() def _is_covered(self, global_state: GlobalState) -> bool: - """ Checks if the instruction for the given global state is already covered""" + """Checks if the instruction for the given global state is already covered""" bytecode = global_state.environment.code.bytecode index = global_state.mstate.pc return self.instruction_coverage_plugin.is_instruction_covered(bytecode, index) diff --git a/mythril/laser/plugin/plugins/dependency_pruner.py b/mythril/laser/plugin/plugins/dependency_pruner.py index bcc5e9c1..863ead99 100644 --- a/mythril/laser/plugin/plugins/dependency_pruner.py +++ b/mythril/laser/plugin/plugins/dependency_pruner.py @@ -20,7 +20,7 @@ log = logging.getLogger(__name__) def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation: - """ Returns a dependency annotation + """Returns a dependency annotation :param state: A global state object """ @@ -51,7 +51,7 @@ def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation: def get_ws_dependency_annotation(state: GlobalState) -> WSDependencyAnnotation: - """ Returns the world state annotation + """Returns the world state annotation :param state: A global state object """ @@ -80,14 +80,14 @@ class DependencyPrunerBuilder(PluginBuilder): class DependencyPruner(LaserPlugin): """Dependency Pruner Plugin - For every basic block, this plugin keeps a list of storage locations that - are accessed (read) in the execution path containing that block. This map - is built up over the whole symbolic execution run. + For every basic block, this plugin keeps a list of storage locations that + are accessed (read) in the execution path containing that block. This map + is built up over the whole symbolic execution run. - After the initial build up of the map in the first transaction, blocks are - executed only if any of the storage locations written to in the previous - transaction can have an effect on that block or any of its successors. - """ + After the initial build up of the map in the first transaction, blocks are + executed only if any of the storage locations written to in the previous + transaction can have an effect on that block or any of its successors. + """ def __init__(self): """Creates DependencyPruner""" @@ -293,9 +293,9 @@ class DependencyPruner(LaserPlugin): def _check_basic_block(address: int, annotation: DependencyAnnotation): """This method is where the actual pruning happens. - :param address: Start address (bytecode offset) of the block - :param annotation: - """ + :param address: Start address (bytecode offset) of the block + :param annotation: + """ # Don't skip any blocks in the contract creation transaction if self.iteration < 2: diff --git a/mythril/laser/plugin/plugins/instruction_profiler.py b/mythril/laser/plugin/plugins/instruction_profiler.py index c79564ac..d5034fda 100644 --- a/mythril/laser/plugin/plugins/instruction_profiler.py +++ b/mythril/laser/plugin/plugins/instruction_profiler.py @@ -39,8 +39,7 @@ class InstructionProfilerBuilder(PluginBuilder): class InstructionProfiler(LaserPlugin): - """Performance profile for the execution of each instruction. - """ + """Performance profile for the execution of each instruction.""" def __init__(self): self._reset() diff --git a/mythril/laser/plugin/signals.py b/mythril/laser/plugin/signals.py index b59614ca..cb4aab06 100644 --- a/mythril/laser/plugin/signals.py +++ b/mythril/laser/plugin/signals.py @@ -8,7 +8,7 @@ class PluginSignal(Exception): class PluginSkipWorldState(PluginSignal): - """ Plugin to skip world state + """Plugin to skip world state Plugins that raise this signal while the add_world_state hook is being executed will force laser to abandon that world state. @@ -18,7 +18,7 @@ class PluginSkipWorldState(PluginSignal): class PluginSkipState(PluginSignal): - """ Plugin to skip world state + """Plugin to skip world state Plugins that raise this signal while the add_world_state hook is being executed will force laser to abandon that world state. diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index 4dba9e6f..09e5b243 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -129,7 +129,7 @@ class _Z3SymbolFactory(SymbolFactory[z3.BoolRef, z3.BitVecRef]): @staticmethod def Bool(value: "__builtins__.bool", annotations: Annotations = None) -> z3.BoolRef: - """ Creates a new bit vector with a concrete value """ + """Creates a new bit vector with a concrete value""" return z3.BoolVal(value) @staticmethod diff --git a/mythril/laser/smt/expression.py b/mythril/laser/smt/expression.py index c549f818..ea1bdad5 100644 --- a/mythril/laser/smt/expression.py +++ b/mythril/laser/smt/expression.py @@ -14,8 +14,8 @@ class Expression(Generic[T]): def __init__(self, raw: T, annotations: Optional[Annotations] = None): """ - :param raw: - :param annotations: + :param raw: + :param annotations: """ self.raw = raw diff --git a/mythril/laser/smt/model.py b/mythril/laser/smt/model.py index 524683e9..b5e2646d 100644 --- a/mythril/laser/smt/model.py +++ b/mythril/laser/smt/model.py @@ -4,7 +4,7 @@ from typing import Union, List class Model: - """ The model class wraps a z3 model + """The model class wraps a z3 model This implementation allows for multiple internal models, this is required for the use of an independence solver which has models for multiple queries which need an uniform output. @@ -25,10 +25,10 @@ class Model: return result def __getitem__(self, item) -> Union[None, z3.ExprRef]: - """ Get declaration from model - If item is an int, then the declaration at offset item is returned - If item is a declaration, then the interpretation is returned - """ + """Get declaration from model + If item is an int, then the declaration at offset item is returned + If item is a declaration, then the interpretation is returned + """ for internal_model in self.raw: is_last_model = self.raw.index(internal_model) == len(self.raw) - 1 @@ -45,7 +45,7 @@ class Model: def eval( self, expression: z3.ExprRef, model_completion: bool = False ) -> Union[None, z3.ExprRef]: - """ Evaluate the expression using this model + """Evaluate the expression using this model :param expression: The expression to evaluate :param model_completion: Use the default value if the model has no interpretation of the given expression diff --git a/mythril/laser/smt/solver/independence_solver.py b/mythril/laser/smt/solver/independence_solver.py index 8f64de46..a8ce59dd 100644 --- a/mythril/laser/smt/solver/independence_solver.py +++ b/mythril/laser/smt/solver/independence_solver.py @@ -23,7 +23,7 @@ def _get_expr_variables(expression: z3.ExprRef) -> List[z3.ExprRef]: class DependenceBucket: - """ Bucket object to contain a set of conditions that are dependent on each other """ + """Bucket object to contain a set of conditions that are dependent on each other""" def __init__(self, variables=None, conditions=None): """ @@ -36,10 +36,10 @@ class DependenceBucket: class DependenceMap: - """ DependenceMap object that maintains a set of dependence buckets, used to separate independent smt queries """ + """DependenceMap object that maintains a set of dependence buckets, used to separate independent smt queries""" def __init__(self): - """ Initializes a DependenceMap object """ + """Initializes a DependenceMap object""" self.buckets = [] # type: List[DependenceBucket] self.variable_map = {} # type: Dict[str, DependenceBucket] @@ -69,7 +69,7 @@ class DependenceMap: self.variable_map[str(variable)] = new_bucket def _merge_buckets(self, bucket_list: Set[DependenceBucket]) -> DependenceBucket: - """ Merges the buckets in bucket list """ + """Merges the buckets in bucket list""" variables = [] # type: List[str] conditions = [] # type: List[z3.BoolRef] for bucket in bucket_list: @@ -122,7 +122,7 @@ class IndependenceSolver: @stat_smt_query def check(self) -> z3.CheckSatResult: - """Returns z3 smt check result. """ + """Returns z3 smt check result.""" dependence_map = DependenceMap() for constraint in self.constraints: dependence_map.add_condition(constraint) @@ -140,7 +140,7 @@ class IndependenceSolver: return z3.sat def model(self) -> Model: - """Returns z3 model for a solution. """ + """Returns z3 model for a solution.""" return Model(self.models) def reset(self) -> None: @@ -148,6 +148,5 @@ class IndependenceSolver: self.constraints = [] def pop(self, num) -> None: - """Pop num constraints from this solver. - """ + """Pop num constraints from this solver.""" self.constraints.pop(num) diff --git a/mythril/laser/smt/solver/solver_statistics.py b/mythril/laser/smt/solver/solver_statistics.py index 603caf69..e87dfbb4 100644 --- a/mythril/laser/smt/solver/solver_statistics.py +++ b/mythril/laser/smt/solver/solver_statistics.py @@ -27,7 +27,7 @@ def stat_smt_query(func: Callable): class SolverStatistics(object, metaclass=Singleton): - """ Solver Statistics Class + """Solver Statistics Class Keeps track of the important statistics around smt queries """ diff --git a/mythril/mythril/mythril_disassembler.py b/mythril/mythril/mythril_disassembler.py index 006c4469..4adcc779 100644 --- a/mythril/mythril/mythril_disassembler.py +++ b/mythril/mythril/mythril_disassembler.py @@ -267,7 +267,7 @@ class MythrilDisassembler: key_formatted = rzpad(key, 32) mappings.append( int.from_bytes( - sha3(key_formatted + position_formatted), byteorder="big", + sha3(key_formatted + position_formatted), byteorder="big" ) ) diff --git a/mythril/plugin/discovery.py b/mythril/plugin/discovery.py index 173f9ae9..96eff676 100644 --- a/mythril/plugin/discovery.py +++ b/mythril/plugin/discovery.py @@ -8,7 +8,7 @@ from typing import List, Dict, Any, Optional class PluginDiscovery(object, metaclass=Singleton): """PluginDiscovery class - This plugin implements the logic to discover and build plugins in installed python packages + This plugin implements the logic to discover and build plugins in installed python packages """ # Installed plugins structure. Retrieves all modules that have an entry point for mythril.plugins @@ -43,7 +43,7 @@ class PluginDiscovery(object, metaclass=Singleton): return plugin(**plugin_args) def get_plugins(self, default_enabled=None) -> List[str]: - """ Gets a list of installed mythril plugins + """Gets a list of installed mythril plugins :param default_enabled: Select plugins that are enabled by default :return: List of plugin names diff --git a/mythril/plugin/interface.py b/mythril/plugin/interface.py index 2d08b6c2..0184bff3 100644 --- a/mythril/plugin/interface.py +++ b/mythril/plugin/interface.py @@ -37,7 +37,7 @@ class MythrilCLIPlugin(MythrilPlugin): class MythrilLaserPlugin(MythrilPlugin, LaserPluginBuilder, ABC): - """ Mythril Laser Plugin interface + """Mythril Laser Plugin interface Plugins of this type are used to instrument the laser EVM """ diff --git a/mythril/support/support_utils.py b/mythril/support/support_utils.py index 9956de6d..6ca94184 100644 --- a/mythril/support/support_utils.py +++ b/mythril/support/support_utils.py @@ -58,14 +58,14 @@ def sha3(value): def zpad(x, l): - """ + """ Left zero pad value `x` at least to length `l`. """ return b"\x00" * max(0, l - len(x)) + x def rzpad(value, total_length): - """ + """ Right zero pad value `x` at least to length `l`. """ return value + b"\x00" * max(0, total_length - len(value)) diff --git a/tests/laser/Precompiles/test_ecrecover.py b/tests/laser/Precompiles/test_ecrecover.py new file mode 100644 index 00000000..1fa79911 --- /dev/null +++ b/tests/laser/Precompiles/test_ecrecover.py @@ -0,0 +1,67 @@ +import pytest + +from mock import patch +from eth_utils import decode_hex +from mythril.laser.ethereum.natives import ecrecover, NativeContractException +from mythril.laser.smt import symbol_factory + +msg = b"\x6b\x8d\x2c\x81\xb1\x1b\x2d\x69\x95\x28\xdd\xe4\x88\xdb\xdf\x2f\x94\x29\x3d\x0d\x33\xc3\x2e\x34\x7f\x25\x5f\xa4\xa6\xc1\xf0\xa9" +v = b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x1c" +r = b"\x53\x56\x92\x27\x4f\x15\x24\x34\x00\x2a\x7c\x4c\x7d\x7c\xd0\x16\xea\x3e\x2d\x70\x2f\x2d\x2f\xd5\xb3\x32\x64\x6a\x9e\x40\x9a\x6b" +s = b"\x1f\x59\x24\xf5\x9c\x6d\x77\x66\xa6\x93\x17\xa3\xdf\x72\x9d\x8b\x61\x3c\x67\xaa\xf2\xfe\x06\x13\x39\x8b\x9f\x94\x4b\x98\x8e\xbd" + +GOOD_DATA = list(msg + v + r + s) + + +@pytest.mark.parametrize( + "input_list, expected_result", + ( + ([], []), + ([10, 20], []), + ( + GOOD_DATA, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 131, + 23, + 8, + 48, + 142, + 77, + 185, + 107, + 254, + 47, + 229, + 79, + 224, + 43, + 181, + 99, + 36, + 171, + 166, + 119, + ], + ), + ), +) +def test_ecrecover(input_list, expected_result): + assert ecrecover(input_list) == expected_result + + +def test_ecrecover_symbol(): + input_list = ["bab", symbol_factory.BitVecSym("name", 256)] + with pytest.raises(NativeContractException): + ecrecover(input_list) diff --git a/tests/laser/Precompiles/test_identity.py b/tests/laser/Precompiles/test_identity.py new file mode 100644 index 00000000..ded2b5c8 --- /dev/null +++ b/tests/laser/Precompiles/test_identity.py @@ -0,0 +1,13 @@ +import pytest + +from mock import patch +from eth_utils import decode_hex +from mythril.laser.ethereum.natives import identity, NativeContractException +from mythril.laser.smt import symbol_factory + + +@pytest.mark.parametrize( + "input_list, expected_result", (([], []), ([10, 20], [10, 20])) +) +def test_identity(input_list, expected_result): + assert identity(input_list) == expected_result diff --git a/tests/laser/Precompiles/test_ripemd.py b/tests/laser/Precompiles/test_ripemd.py new file mode 100644 index 00000000..7f18ff5f --- /dev/null +++ b/tests/laser/Precompiles/test_ripemd.py @@ -0,0 +1,95 @@ +import pytest + +from mock import patch +from eth_utils import decode_hex +from mythril.laser.ethereum.natives import ripemd160, NativeContractException +from mythril.laser.smt import symbol_factory + + +@pytest.mark.parametrize( + "input_list, expected_result", + ( + ( + [], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 156, + 17, + 133, + 165, + 197, + 233, + 252, + 84, + 97, + 40, + 8, + 151, + 126, + 232, + 245, + 72, + 178, + 37, + 141, + 49, + ], + ), + ( + [10, 20], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 92, + 161, + 226, + 233, + 76, + 11, + 228, + 69, + 224, + 14, + 89, + 120, + 246, + 184, + 197, + 182, + 35, + 215, + 51, + 130, + ], + ), + ), +) +def test_ripemd160(input_list, expected_result): + assert ripemd160(input_list) == expected_result + + +def test_ripemd160_symbol(): + input_list = ["bab", symbol_factory.BitVecSym("name", 256)] + with pytest.raises(NativeContractException): + ripemd160(input_list) diff --git a/tests/laser/Precompiles/test_sha256.py b/tests/laser/Precompiles/test_sha256.py new file mode 100644 index 00000000..f03e98c6 --- /dev/null +++ b/tests/laser/Precompiles/test_sha256.py @@ -0,0 +1,95 @@ +import pytest + +from mock import patch +from eth_utils import decode_hex +from mythril.laser.ethereum.natives import sha256, NativeContractException +from mythril.laser.smt import symbol_factory + + +@pytest.mark.parametrize( + "input_list, expected_result", + ( + ( + [], + [ + 227, + 176, + 196, + 66, + 152, + 252, + 28, + 20, + 154, + 251, + 244, + 200, + 153, + 111, + 185, + 36, + 39, + 174, + 65, + 228, + 100, + 155, + 147, + 76, + 164, + 149, + 153, + 27, + 120, + 82, + 184, + 85, + ], + ), + ( + [10, 20], + [ + 195, + 48, + 250, + 117, + 58, + 197, + 190, + 59, + 143, + 203, + 82, + 116, + 80, + 98, + 247, + 129, + 204, + 158, + 15, + 79, + 169, + 129, + 162, + 189, + 6, + 252, + 185, + 105, + 53, + 91, + 148, + 105, + ], + ), + ), +) +def test_sha256(input_list, expected_result): + assert sha256(input_list) == expected_result + + +def test_sha_symbol(): + input_list = ["bab", symbol_factory.BitVecSym("name", 256)] + with pytest.raises(NativeContractException): + sha256(input_list)