Add more precompile tests (#1576)

* Add tests for natives

* Black updates

* Update black
pull/1577/head
Nikhil Parasaram 3 years ago committed by GitHub
parent 4003ff1e80
commit c72ac81de1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 2
      .circleci/config.yml
  2. 2
      .pre-commit-config.yaml
  3. 1
      mypy-stubs/z3/__init__.pyi
  4. 4
      mythril/analysis/module/base.py
  5. 2
      mythril/analysis/module/loader.py
  6. 2
      mythril/analysis/module/modules/exceptions.py
  7. 4
      mythril/analysis/module/modules/integer.py
  8. 4
      mythril/analysis/module/modules/user_assertions.py
  9. 2
      mythril/analysis/module/util.py
  10. 8
      mythril/analysis/report.py
  11. 4
      mythril/analysis/security.py
  12. 8
      mythril/analysis/solver.py
  13. 6
      mythril/interfaces/cli.py
  14. 9
      mythril/laser/ethereum/function_managers/exponent_function_manager.py
  15. 2
      mythril/laser/ethereum/function_managers/keccak_function_manager.py
  16. 4
      mythril/laser/ethereum/instructions.py
  17. 3
      mythril/laser/ethereum/iprof.py
  18. 7
      mythril/laser/ethereum/natives.py
  19. 2
      mythril/laser/ethereum/state/world_state.py
  20. 2
      mythril/laser/ethereum/strategy/extensions/bounded_loops.py
  21. 8
      mythril/laser/ethereum/svm.py
  22. 2
      mythril/laser/plugin/builder.py
  23. 4
      mythril/laser/plugin/interface.py
  24. 8
      mythril/laser/plugin/loader.py
  25. 2
      mythril/laser/plugin/plugins/coverage/coverage_strategy.py
  26. 4
      mythril/laser/plugin/plugins/dependency_pruner.py
  27. 3
      mythril/laser/plugin/plugins/instruction_profiler.py
  28. 4
      mythril/laser/plugin/signals.py
  29. 2
      mythril/laser/smt/__init__.py
  30. 6
      mythril/laser/smt/model.py
  31. 15
      mythril/laser/smt/solver/independence_solver.py
  32. 2
      mythril/laser/smt/solver/solver_statistics.py
  33. 2
      mythril/mythril/mythril_disassembler.py
  34. 2
      mythril/plugin/discovery.py
  35. 2
      mythril/plugin/interface.py
  36. 67
      tests/laser/Precompiles/test_ecrecover.py
  37. 13
      tests/laser/Precompiles/test_identity.py
  38. 95
      tests/laser/Precompiles/test_ripemd.py
  39. 95
      tests/laser/Precompiles/test_sha256.py

@ -40,7 +40,7 @@ jobs:
- run: - run:
name: Black style check name: Black style check
command: | command: |
pip3 install --user black==19.10b0 pip3 install --user black==21.12b0
python3 -m black --check /home/mythril/ python3 -m black --check /home/mythril/
- run: - run:

@ -2,6 +2,6 @@
# See https://pre-commit.com/hooks.html for more hooks # See https://pre-commit.com/hooks.html for more hooks
repos: repos:
- repo: https://github.com/psf/black - repo: https://github.com/psf/black
rev: 19.3b0 rev: 21.12b0
hooks: hooks:
- id: black - id: black

@ -168,6 +168,7 @@ class Optimize(Z3PPObject):
sat: CheckSatResult = ... sat: CheckSatResult = ...
unsat: CheckSatResult = ... unsat: CheckSatResult = ...
@overload @overload
def Int(name: str) -> ArithRef: ... def Int(name: str) -> ArithRef: ...
@overload @overload

@ -17,7 +17,7 @@ log = logging.getLogger(__name__)
class EntryPoint(Enum): class EntryPoint(Enum):
""" EntryPoint Enum """EntryPoint Enum
This enum is used to signify the entry_point of detection modules. This enum is used to signify the entry_point of detection modules.
See also the class documentation of DetectionModule 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]]]] self.cache = set() # type: Set[Optional[Union[int, Tuple[int, str]]]]
def reset_module(self): def reset_module(self):
""" Resets the storage of this module """ """Resets the storage of this module"""
self.issues = [] self.issues = []
def execute(self, target: GlobalState) -> Optional[List[Issue]]: def execute(self, target: GlobalState) -> Optional[List[Issue]]:

@ -51,7 +51,7 @@ class ModuleLoader(object, metaclass=Singleton):
entry_point: Optional[EntryPoint] = None, entry_point: Optional[EntryPoint] = None,
white_list: Optional[List[str]] = None, white_list: Optional[List[str]] = None,
) -> List[DetectionModule]: ) -> List[DetectionModule]:
""" Gets registered detection modules """Gets registered detection modules
:param entry_point: If specified: only return detection modules with this entry point :param entry_point: If specified: only return detection modules with this entry point
:param white_list: If specified: only return whitelisted detection modules :param white_list: If specified: only return whitelisted detection modules

@ -18,7 +18,7 @@ PANIC_SIGNATURE = [78, 72, 123, 113]
class LastJumpAnnotation(StateAnnotation): 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: def __init__(self, last_jump: int = None) -> None:
self.last_jump: int = last_jump self.last_jump: int = last_jump

@ -31,7 +31,7 @@ log = logging.getLogger(__name__)
class OverUnderflowAnnotation: class OverUnderflowAnnotation:
""" Symbol Annotation used if a BitVector can overflow""" """Symbol Annotation used if a BitVector can overflow"""
def __init__( def __init__(
self, overflowing_state: GlobalState, operator: str, constraint: Bool self, overflowing_state: GlobalState, operator: str, constraint: Bool
@ -46,7 +46,7 @@ class OverUnderflowAnnotation:
class OverUnderflowStateAnnotation(StateAnnotation): 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: def __init__(self) -> None:
self.overflowing_state_annotations = set() # type: Set[OverUnderflowAnnotation] self.overflowing_state_annotations = set() # type: Set[OverUnderflowAnnotation]

@ -87,9 +87,11 @@ class UserAssertions(DetectionModule):
) )
if message: if message:
description_tail = "A user-provided assertion failed with the message '{}'".format( description_tail = (
"A user-provided assertion failed with the message '{}'".format(
message message
) )
)
else: else:
description_tail = "A user-provided assertion failed." description_tail = "A user-provided assertion failed."

@ -13,7 +13,7 @@ OP_CODE_LIST = OPCODES.keys()
def get_detection_module_hooks( def get_detection_module_hooks(
modules: List[DetectionModule], hook_type="pre" modules: List[DetectionModule], hook_type="pre"
) -> Dict[str, List[Callable]]: ) -> 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 modules: The modules for which to retrieve hooks
:param hook_type: The type of hooks to retrieve (default: "pre") :param hook_type: The type of hooks to retrieve (default: "pre")

@ -71,12 +71,12 @@ class Issue:
@property @property
def transaction_sequence_users(self): 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 return self.transaction_sequence
@property @property
def transaction_sequence_jsonv2(self): 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 ( return (
self.add_block_data(self.transaction_sequence) self.add_block_data(self.transaction_sequence)
if self.transaction_sequence if self.transaction_sequence
@ -85,7 +85,7 @@ class Issue:
@staticmethod @staticmethod
def add_block_data(transaction_sequence: Dict): 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"]: for step in transaction_sequence["steps"]:
step["gasLimit"] = "0x7d000" step["gasLimit"] = "0x7d000"
step["gasPrice"] = "0x773594000" step["gasPrice"] = "0x773594000"
@ -167,7 +167,7 @@ class Issue:
self.source_mapping = self.address self.source_mapping = self.address
def resolve_function_names(self): def resolve_function_names(self):
""" Resolves function names for each step """ """Resolves function names for each step"""
if ( if (
self.transaction_sequence is None self.transaction_sequence is None

@ -12,7 +12,7 @@ log = logging.getLogger(__name__)
def retrieve_callback_issues(white_list: Optional[List[str]] = None) -> List[Issue]: 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] issues = [] # type: List[Issue]
for module in ModuleLoader().get_detection_modules( for module in ModuleLoader().get_detection_modules(
entry_point=EntryPoint.CALLBACK, white_list=white_list 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]: 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 statespace: Symbolic statespace to analyze
:param white_list: Optionally whitelist modules to use for the analysis :param white_list: Optionally whitelist modules to use for the analysis

@ -24,7 +24,7 @@ log = logging.getLogger(__name__)
def pretty_print_model(model): def pretty_print_model(model):
""" Pretty prints a z3 model """Pretty prints a z3 model
:param model: :param model:
:return: :return:
@ -161,7 +161,7 @@ def _replace_with_actual_sha(
def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]): def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]):
""" Gets a concrete state """ """Gets a concrete state"""
accounts = {} accounts = {}
for address, account in initial_accounts.items(): for address, account in initial_accounts.items():
# Skip empty default account # 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): 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 # Get concrete values from transaction
address = hex(transaction.callee_account.address.value) address = hex(transaction.callee_account.address.value)
value = model.eval(transaction.call_value.raw, model_completion=True).as_long() 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( def _set_minimisation_constraints(
transaction_sequence, constraints, minimize, max_size, world_state transaction_sequence, constraints, minimize, max_size, world_state
) -> Tuple[Constraints, tuple]: ) -> Tuple[Constraints, tuple]:
""" Set constraints that minimise key transaction values """Set constraints that minimise key transaction values
Constraints generated: Constraints generated:
- Upper bound on calldata size - Upper bound on calldata size

@ -23,11 +23,7 @@ from mythril.exceptions import (
) )
from mythril.laser.ethereum.transaction.symbolic import ACTORS from mythril.laser.ethereum.transaction.symbolic import ACTORS
from mythril.plugin.loader import MythrilPluginLoader from mythril.plugin.loader import MythrilPluginLoader
from mythril.mythril import ( from mythril.mythril import MythrilAnalyzer, MythrilDisassembler, MythrilConfig
MythrilAnalyzer,
MythrilDisassembler,
MythrilConfig,
)
from mythril.analysis.module import ModuleLoader from mythril.analysis.module import ModuleLoader
from mythril.analysis.report import Report from mythril.analysis.report import Report

@ -2,14 +2,7 @@ import logging
from typing import Dict, List, Optional, Tuple from typing import Dict, List, Optional, Tuple
from mythril.laser.smt import ( from mythril.laser.smt import And, BitVec, Bool, Function, URem, symbol_factory
And,
BitVec,
Bool,
Function,
URem,
symbol_factory,
)
log = logging.getLogger(__name__) log = logging.getLogger(__name__)

@ -62,7 +62,7 @@ class KeccakFunctionManager:
""" """
keccak = symbol_factory.BitVecVal( keccak = symbol_factory.BitVecVal(
int.from_bytes( 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, 256,
) )

@ -656,9 +656,7 @@ class Instruction:
If( If(
s0 <= 31, s0 <= 31,
If( If(
sign_bit_set, sign_bit_set, s1 | (TT256 - set_testbit), s1 & (set_testbit - 1)
s1 | (TT256 - set_testbit),
s1 & (set_testbit - 1),
), ),
s1, s1,
) )

@ -24,8 +24,7 @@ _InstrExecStatistics = Dict[str, _InstrExecStatistic]
class InstructionProfiler: class InstructionProfiler:
"""Performance profile for the execution of each instruction. """Performance profile for the execution of each instruction."""
"""
def __init__(self): def __init__(self):
self.records = dict() self.records = dict()

@ -134,11 +134,6 @@ def identity(data: List[int]) -> List[int]:
:param data: :param data:
:return: :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 return data
@ -279,7 +274,7 @@ def native_contracts(address: int, data: BaseCalldata) -> List[int]:
""" """
if not isinstance(data, ConcreteCalldata): if not isinstance(data, ConcreteCalldata):
raise NativeContractException() raise NativeContractException
concrete_data = data.concrete(None) concrete_data = data.concrete(None)
try: try:
return PRECOMPILE_FUNCTIONS[address - 1](concrete_data) return PRECOMPILE_FUNCTIONS[address - 1](concrete_data)

@ -115,7 +115,7 @@ class WorldState:
except ValueError: except ValueError:
code = None code = None
return self.create_account( 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( def create_account(

@ -102,7 +102,7 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
return count return count
def get_strategic_global_state(self) -> GlobalState: def get_strategic_global_state(self) -> GlobalState:
""" Returns the next state """Returns the next state
:return: Global state :return: Global state
""" """

@ -125,7 +125,7 @@ class LaserEVM:
creation_code: str = None, creation_code: str = None,
contract_name: str = None, contract_name: str = None,
) -> None: ) -> None:
""" Starts symbolic execution """Starts symbolic execution
There are two modes of execution. There are two modes of execution.
Either we analyze a preconfigured configuration, in which case the world_state and target_address variables Either we analyze a preconfigured configuration, in which case the world_state and target_address variables
must be supplied. must be supplied.
@ -274,7 +274,7 @@ class LaserEVM:
return final_states if track_gas else None return final_states if track_gas else None
def _add_world_state(self, global_state: GlobalState): 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: for hook in self._add_world_state_hooks:
try: try:
@ -612,7 +612,7 @@ class LaserEVM:
""" """
def hook_decorator(func: Callable): def hook_decorator(func: Callable):
""" Hook decorator generated by laser_hook """Hook decorator generated by laser_hook
:param func: Decorated function :param func: Decorated function
""" """
@ -628,7 +628,7 @@ class LaserEVM:
""" """
def hook_decorator(func: Callable): def hook_decorator(func: Callable):
""" Hook decorator generated by laser_hook """Hook decorator generated by laser_hook
:param func: Decorated function :param func: Decorated function
""" """

@ -5,7 +5,7 @@ from typing import Optional
class PluginBuilder(ABC): class PluginBuilder(ABC):
""" PluginBuilder """PluginBuilder
The plugin builder interface enables construction of Laser plugins The plugin builder interface enables construction of Laser plugins
""" """

@ -2,7 +2,7 @@ from mythril.laser.ethereum.svm import LaserEVM
class LaserPlugin: 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 Functionality in laser that the symbolic execution process does not need to depend on
can be implemented in the form of a laser plugin. can be implemented in the form of a laser plugin.
@ -16,7 +16,7 @@ class LaserPlugin:
""" """
def initialize(self, symbolic_vm: LaserEVM) -> None: 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 :param symbolic_vm: symbolic virtual machine to initialize the laser plugin on
""" """

@ -15,7 +15,7 @@ class LaserPluginLoader(object, metaclass=Singleton):
""" """
def __init__(self) -> None: def __init__(self) -> None:
""" Initializes the plugin loader """ """Initializes the plugin loader"""
self.laser_plugin_builders = {} # type: Dict[str, PluginBuilder] self.laser_plugin_builders = {} # type: Dict[str, PluginBuilder]
self.plugin_args = {} # type: Dict[str, Dict] self.plugin_args = {} # type: Dict[str, Dict]
@ -23,7 +23,7 @@ class LaserPluginLoader(object, metaclass=Singleton):
self.plugin_args[plugin_name] = kwargs self.plugin_args[plugin_name] = kwargs
def load(self, plugin_builder: PluginBuilder) -> None: def load(self, plugin_builder: PluginBuilder) -> None:
""" Enables a Laser Plugin """Enables a Laser Plugin
:param plugin_builder: Builder that constructs the 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 self.laser_plugin_builders[plugin_builder.name] = plugin_builder
def is_enabled(self, plugin_name: str) -> bool: 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 :param plugin_name: Name of the plugin to check
""" """
@ -53,7 +53,7 @@ class LaserPluginLoader(object, metaclass=Singleton):
def instrument_virtual_machine( def instrument_virtual_machine(
self, symbolic_vm: LaserEVM, with_plugins: Optional[List[str]] 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 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 :param with_plugins: Override the globally enabled/disabled builders and load all plugins in the list
""" """

@ -35,7 +35,7 @@ class CoverageStrategy(BasicSearchStrategy):
return self.super_strategy.get_strategic_global_state() return self.super_strategy.get_strategic_global_state()
def _is_covered(self, global_state: GlobalState) -> bool: 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 bytecode = global_state.environment.code.bytecode
index = global_state.mstate.pc index = global_state.mstate.pc
return self.instruction_coverage_plugin.is_instruction_covered(bytecode, index) return self.instruction_coverage_plugin.is_instruction_covered(bytecode, index)

@ -20,7 +20,7 @@ log = logging.getLogger(__name__)
def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation: def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation:
""" Returns a dependency annotation """Returns a dependency annotation
:param state: A global state object :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: def get_ws_dependency_annotation(state: GlobalState) -> WSDependencyAnnotation:
""" Returns the world state annotation """Returns the world state annotation
:param state: A global state object :param state: A global state object
""" """

@ -39,8 +39,7 @@ class InstructionProfilerBuilder(PluginBuilder):
class InstructionProfiler(LaserPlugin): class InstructionProfiler(LaserPlugin):
"""Performance profile for the execution of each instruction. """Performance profile for the execution of each instruction."""
"""
def __init__(self): def __init__(self):
self._reset() self._reset()

@ -8,7 +8,7 @@ class PluginSignal(Exception):
class PluginSkipWorldState(PluginSignal): 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 Plugins that raise this signal while the add_world_state hook is being executed
will force laser to abandon that world state. will force laser to abandon that world state.
@ -18,7 +18,7 @@ class PluginSkipWorldState(PluginSignal):
class PluginSkipState(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 Plugins that raise this signal while the add_world_state hook is being executed
will force laser to abandon that world state. will force laser to abandon that world state.

@ -129,7 +129,7 @@ class _Z3SymbolFactory(SymbolFactory[z3.BoolRef, z3.BitVecRef]):
@staticmethod @staticmethod
def Bool(value: "__builtins__.bool", annotations: Annotations = None) -> z3.BoolRef: 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) return z3.BoolVal(value)
@staticmethod @staticmethod

@ -4,7 +4,7 @@ from typing import Union, List
class Model: 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 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. which has models for multiple queries which need an uniform output.
@ -25,7 +25,7 @@ class Model:
return result return result
def __getitem__(self, item) -> Union[None, z3.ExprRef]: def __getitem__(self, item) -> Union[None, z3.ExprRef]:
""" Get declaration from model """Get declaration from model
If item is an int, then the declaration at offset item is returned If item is an int, then the declaration at offset item is returned
If item is a declaration, then the interpretation is returned If item is a declaration, then the interpretation is returned
""" """
@ -45,7 +45,7 @@ class Model:
def eval( def eval(
self, expression: z3.ExprRef, model_completion: bool = False self, expression: z3.ExprRef, model_completion: bool = False
) -> Union[None, z3.ExprRef]: ) -> Union[None, z3.ExprRef]:
""" Evaluate the expression using this model """Evaluate the expression using this model
:param expression: The expression to evaluate :param expression: The expression to evaluate
:param model_completion: Use the default value if the model has no interpretation of the given expression :param model_completion: Use the default value if the model has no interpretation of the given expression

@ -23,7 +23,7 @@ def _get_expr_variables(expression: z3.ExprRef) -> List[z3.ExprRef]:
class DependenceBucket: 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): def __init__(self, variables=None, conditions=None):
""" """
@ -36,10 +36,10 @@ class DependenceBucket:
class DependenceMap: 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): def __init__(self):
""" Initializes a DependenceMap object """ """Initializes a DependenceMap object"""
self.buckets = [] # type: List[DependenceBucket] self.buckets = [] # type: List[DependenceBucket]
self.variable_map = {} # type: Dict[str, DependenceBucket] self.variable_map = {} # type: Dict[str, DependenceBucket]
@ -69,7 +69,7 @@ class DependenceMap:
self.variable_map[str(variable)] = new_bucket self.variable_map[str(variable)] = new_bucket
def _merge_buckets(self, bucket_list: Set[DependenceBucket]) -> DependenceBucket: 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] variables = [] # type: List[str]
conditions = [] # type: List[z3.BoolRef] conditions = [] # type: List[z3.BoolRef]
for bucket in bucket_list: for bucket in bucket_list:
@ -122,7 +122,7 @@ class IndependenceSolver:
@stat_smt_query @stat_smt_query
def check(self) -> z3.CheckSatResult: def check(self) -> z3.CheckSatResult:
"""Returns z3 smt check result. """ """Returns z3 smt check result."""
dependence_map = DependenceMap() dependence_map = DependenceMap()
for constraint in self.constraints: for constraint in self.constraints:
dependence_map.add_condition(constraint) dependence_map.add_condition(constraint)
@ -140,7 +140,7 @@ class IndependenceSolver:
return z3.sat return z3.sat
def model(self) -> Model: def model(self) -> Model:
"""Returns z3 model for a solution. """ """Returns z3 model for a solution."""
return Model(self.models) return Model(self.models)
def reset(self) -> None: def reset(self) -> None:
@ -148,6 +148,5 @@ class IndependenceSolver:
self.constraints = [] self.constraints = []
def pop(self, num) -> None: def pop(self, num) -> None:
"""Pop num constraints from this solver. """Pop num constraints from this solver."""
"""
self.constraints.pop(num) self.constraints.pop(num)

@ -27,7 +27,7 @@ def stat_smt_query(func: Callable):
class SolverStatistics(object, metaclass=Singleton): class SolverStatistics(object, metaclass=Singleton):
""" Solver Statistics Class """Solver Statistics Class
Keeps track of the important statistics around smt queries Keeps track of the important statistics around smt queries
""" """

@ -267,7 +267,7 @@ class MythrilDisassembler:
key_formatted = rzpad(key, 32) key_formatted = rzpad(key, 32)
mappings.append( mappings.append(
int.from_bytes( int.from_bytes(
sha3(key_formatted + position_formatted), byteorder="big", sha3(key_formatted + position_formatted), byteorder="big"
) )
) )

@ -43,7 +43,7 @@ class PluginDiscovery(object, metaclass=Singleton):
return plugin(**plugin_args) return plugin(**plugin_args)
def get_plugins(self, default_enabled=None) -> List[str]: 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 :param default_enabled: Select plugins that are enabled by default
:return: List of plugin names :return: List of plugin names

@ -37,7 +37,7 @@ class MythrilCLIPlugin(MythrilPlugin):
class MythrilLaserPlugin(MythrilPlugin, LaserPluginBuilder, ABC): class MythrilLaserPlugin(MythrilPlugin, LaserPluginBuilder, ABC):
""" Mythril Laser Plugin interface """Mythril Laser Plugin interface
Plugins of this type are used to instrument the laser EVM Plugins of this type are used to instrument the laser EVM
""" """

@ -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)

@ -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

@ -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)

@ -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)
Loading…
Cancel
Save