Merge branch 'develop' into features/plugin_loader_sym

# Conflicts:
#	mythril/laser/ethereum/plugins/plugin_factory.py

mythril/analysis/modules/delegatecall.py

@@ -50,7 +50,7 @@ def _analyze_states(state: GlobalState) -> List[Issue]:
 
     if call.type is not "DELEGATECALL":
         return []
-    if call.node.function_name is not "fallback":
+    if state.environment.active_function_name is not "fallback":
         return []
 
     state = call.state
@@ -77,8 +77,8 @@ def _concrete_call(
         return []
 
     issue = Issue(
-        contract=call.node.contract_name,
+        contract=state.environment.active_account.contract_name,
-        function_name=call.node.function_name,
+        function_name=state.environment.active_function_name,
         address=address,
         swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT,
         bytecode=state.environment.code.bytecode,

mythril/analysis/modules/dependence_on_predictable_vars.py

@@ -71,13 +71,13 @@ def _analyze_states(state: GlobalState) -> list:
         "The contract sends Ether depending on the values of the following variables:\n"
     )
 
-    # First check: look for predictable state variables in node & call recipient constraints
+    # First check: look for predictable state variables in state & call recipient constraints
 
     vars = ["coinbase", "gaslimit", "timestamp", "number"]
     found = []
 
     for var in vars:
-        for constraint in call.node.constraints[:] + [call.to]:
+        for constraint in call.state.mstate.constraints[:] + [call.to]:
             if var in str(constraint):
                 found.append(var)
 
@@ -94,8 +94,8 @@ def _analyze_states(state: GlobalState) -> list:
             )
 
             issue = Issue(
-                contract=call.node.contract_name,
+                contract=state.environment.active_account.contract_name,
-                function_name=call.node.function_name,
+                function_name=state.environment.active_function_name,
                 address=address,
                 swc_id=swc_id,
                 bytecode=call.state.environment.code.bytecode,
@@ -112,7 +112,7 @@ def _analyze_states(state: GlobalState) -> list:
 
     # Second check: blockhash
 
-    for constraint in call.node.constraints[:] + [call.to]:
+    for constraint in call.state.mstate.constraints[:] + [call.to]:
         if "blockhash" in str(constraint):
             if "number" in str(constraint):
                 m = re.search(r"blockhash\w+(\s-\s(\d+))*", str(constraint))
@@ -145,8 +145,8 @@ def _analyze_states(state: GlobalState) -> list:
                         description += ", this expression will always be equal to zero."
 
                     issue = Issue(
-                        contract=call.node.contract_name,
+                        contract=state.environment.active_account.contract_name,
-                        function_name=call.node.function_name,
+                        function_name=state.environment.active_function_name,
                         address=address,
                         bytecode=call.state.environment.code.bytecode,
                         title="Dependence on Predictable Variable",
@@ -186,8 +186,8 @@ def _analyze_states(state: GlobalState) -> list:
                             )
                         )
                         issue = Issue(
-                            contract=call.node.contract_name,
+                            contract=state.environment.active_account.contract_name,
-                            function_name=call.node.function_name,
+                            function_name=state.environment.active_function_name,
                             address=address,
                             bytecode=call.state.environment.code.bytecode,
                             title="Dependence on Predictable Variable",
@@ -212,7 +212,7 @@ def solve(call: Call) -> bool:
     :return:
     """
     try:
-        model = solver.get_model(call.node.constraints)
+        model = solver.get_model(call.state.mstate.constraints)
         log.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] MODEL: " + str(model))
         pretty_model = solver.pretty_print_model(model)
 

mythril/analysis/modules/deprecated_ops.py

@@ -30,13 +30,13 @@ def _analyze_state(state):
             "Use of msg.origin is deprecated and the instruction may be removed in the  future. "
             "Use msg.sender instead.\nSee also: "
             "https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin".format(
-                node.function_name
+                state.environment.active_function_name
             )
         )
         swc_id = DEPRECATED_FUNCTIONS_USAGE
 
     elif instruction["opcode"] == "CALLCODE":
-        log.debug("CALLCODE in function " + node.function_name)
+        log.debug("CALLCODE in function " + state.environment.active_function_name)
         title = "Use of callcode"
         description_head = "Use of callcode is deprecated."
         description_tail = (
@@ -45,10 +45,12 @@ def _analyze_state(state):
             "therefore deprecated and may be removed in the future. Use the delegatecall method instead."
         )
         swc_id = DEPRECATED_FUNCTIONS_USAGE
+    else:
+        return
 
     issue = Issue(
-        contract=node.contract_name,
+        contract=state.environment.active_account.contract_name,
-        function_name=node.function_name,
+        function_name=state.environment.active_function_name,
         address=instruction["address"],
         title=title,
         bytecode=state.environment.code.bytecode,

mythril/analysis/modules/ether_thief.py

@@ -67,7 +67,6 @@ class EtherThief(DetectionModule):
         :return:
         """
         instruction = state.get_current_instruction()
-        node = state.node
 
         if instruction["opcode"] != "CALL":
             return []
@@ -80,7 +79,7 @@ class EtherThief(DetectionModule):
 
         eth_sent_total = symbol_factory.BitVecVal(0, 256)
 
-        constraints = copy(node.constraints)
+        constraints = copy(state.mstate.constraints)
 
         for tx in state.world_state.transaction_sequence:
             if tx.caller == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF:
@@ -101,8 +100,8 @@ class EtherThief(DetectionModule):
             debug = json.dumps(transaction_sequence, indent=4)
 
             issue = Issue(
-                contract=node.contract_name,
+                contract=state.environment.active_account.contract_name,
-                function_name=node.function_name,
+                function_name=state.environment.active_function_name,
                 address=instruction["address"],
                 swc_id=UNPROTECTED_ETHER_WITHDRAWAL,
                 title="Unprotected Ether Withdrawal",

mythril/analysis/modules/exceptions.py

@@ -19,9 +19,8 @@ def _analyze_state(state) -> list:
     :return:
     """
     log.info("Exceptions module: found ASSERT_FAIL instruction")
-    node = state.node
 
-    log.debug("ASSERT_FAIL in function " + node.function_name)
+    log.debug("ASSERT_FAIL in function " + state.environment.active_function_name)
 
     try:
         address = state.get_current_instruction()["address"]
@@ -34,12 +33,14 @@ def _analyze_state(state) -> list:
             "Use `require()` for regular input checking."
         )
 
-        transaction_sequence = solver.get_transaction_sequence(state, node.constraints)
+        transaction_sequence = solver.get_transaction_sequence(
+            state, state.mstate.constraints
+        )
         debug = json.dumps(transaction_sequence, indent=4)
 
         issue = Issue(
-            contract=node.contract_name,
+            contract=state.environment.active_account.contract_name,
-            function_name=node.function_name,
+            function_name=state.environment.active_function_name,
             address=address,
             swc_id=ASSERT_VIOLATION,
             title="Exception State",

mythril/analysis/modules/external_calls.py

@@ -8,6 +8,7 @@ from mythril.analysis.report import Issue
 from mythril.laser.smt import UGT, symbol_factory
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.exceptions import UnsatError
+from copy import copy
 import logging
 import json
 
@@ -28,14 +29,13 @@ def _analyze_state(state):
     :param state:
     :return:
     """
-    node = state.node
     gas = state.mstate.stack[-1]
     to = state.mstate.stack[-2]
 
     address = state.get_current_instruction()["address"]
 
     try:
-        constraints = node.constraints
+        constraints = copy(state.mstate.constraints)
         transaction_sequence = solver.get_transaction_sequence(
             state, constraints + [UGT(gas, symbol_factory.BitVecVal(2300, 256))]
         )
@@ -56,8 +56,8 @@ def _analyze_state(state):
             )
 
             issue = Issue(
-                contract=node.contract_name,
+                contract=state.environment.active_account.contract_name,
-                function_name=node.function_name,
+                function_name=state.environment.active_function_name,
                 address=address,
                 swc_id=REENTRANCY,
                 title="External Call To User-Supplied Address",
@@ -83,8 +83,8 @@ def _analyze_state(state):
             )
 
             issue = Issue(
-                contract=node.contract_name,
+                contract=state.environment.active_account.contract_name,
-                function_name=state.node.function_name,
+                function_name=state.environment.active_function_name,
                 address=address,
                 swc_id=REENTRANCY,
                 title="External Call To Fixed Address",

mythril/analysis/modules/integer.py

@@ -120,7 +120,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         c = Not(BVAddNoOverflow(op0, op1, False))
 
         # Check satisfiable
-        model = self._try_constraints(state.node.constraints, [c])
+        model = self._try_constraints(state.mstate.constraints, [c])
         if model is None:
             return
 
@@ -132,7 +132,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         c = Not(BVMulNoOverflow(op0, op1, False))
 
         # Check satisfiable
-        model = self._try_constraints(state.node.constraints, [c])
+        model = self._try_constraints(state.mstate.constraints, [c])
         if model is None:
             return
 
@@ -144,7 +144,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         c = Not(BVSubNoUnderflow(op0, op1, False))
 
         # Check satisfiable
-        model = self._try_constraints(state.node.constraints, [c])
+        model = self._try_constraints(state.mstate.constraints, [c])
         if model is None:
             return
 
@@ -172,7 +172,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
             )
         else:
             constraint = op0.value ** op1.value >= 2 ** 256
-        model = self._try_constraints(state.node.constraints, [constraint])
+        model = self._try_constraints(state.mstate.constraints, [constraint])
         if model is None:
             return
         annotation = OverUnderflowAnnotation(state, "exponentiation", constraint)
@@ -286,7 +286,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
             ):
                 continue
 
-            node = ostate.node
             try:
 
                 transaction_sequence = solver.get_transaction_sequence(
@@ -297,8 +296,8 @@ class IntegerOverflowUnderflowModule(DetectionModule):
 
             _type = "Underflow" if annotation.operator == "subtraction" else "Overflow"
             issue = Issue(
-                contract=node.contract_name,
+                contract=ostate.environment.active_account.contract_name,
-                function_name=node.function_name,
+                function_name=ostate.environment.active_function_name,
                 address=ostate.get_current_instruction()["address"],
                 swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW,
                 bytecode=ostate.environment.code.bytecode,
@@ -319,8 +318,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
 
     @staticmethod
     def _try_constraints(constraints, new_constraints):
-        """
+        """        Tries new constraints
-        Tries new constraints
         :return Model if satisfiable otherwise None
         """
         try:

mythril/analysis/modules/multiple_sends.py

@@ -55,7 +55,6 @@ def _analyze_state(state: GlobalState):
     :param state: the current state
     :return: returns the issues for that corresponding state
     """
-    node = state.node
     instruction = state.get_current_instruction()
 
     annotations = cast(
@@ -95,8 +94,8 @@ def _analyze_state(state: GlobalState):
             )
 
             issue = Issue(
-                contract=node.contract_name,
+                contract=state.environment.active_account.contract_name,
-                function_name=node.function_name,
+                function_name=state.environment.active_function_name,
                 address=instruction["address"],
                 swc_id=MULTIPLE_SENDS,
                 bytecode=state.environment.code.bytecode,

mythril/analysis/modules/suicide.py

@@ -48,13 +48,14 @@ class SuicideModule(DetectionModule):
 
     def _analyze_state(self, state):
         log.info("Suicide module: Analyzing suicide instruction")
-        node = state.node
         instruction = state.get_current_instruction()
         if self._cache_address.get(instruction["address"], False):
             return []
         to = state.mstate.stack[-1]
 
-        log.debug("[SUICIDE] SUICIDE in function " + node.function_name)
+        log.debug(
+            "[SUICIDE] SUICIDE in function " + state.environment.active_function_name
+        )
 
         description_head = "The contract can be killed by anyone."
 
@@ -62,7 +63,7 @@ class SuicideModule(DetectionModule):
             try:
                 transaction_sequence = solver.get_transaction_sequence(
                     state,
-                    node.constraints
+                    state.mstate.constraints
                     + [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF],
                 )
                 description_tail = (
@@ -71,7 +72,7 @@ class SuicideModule(DetectionModule):
                 )
             except UnsatError:
                 transaction_sequence = solver.get_transaction_sequence(
-                    state, node.constraints
+                    state, state.mstate.constraints
                 )
                 description_tail = "Arbitrary senders can kill this contract."
 
@@ -79,8 +80,8 @@ class SuicideModule(DetectionModule):
             self._cache_address[instruction["address"]] = True
 
             issue = Issue(
-                contract=node.contract_name,
+                contract=state.environment.active_account.contract_name,
-                function_name=node.function_name,
+                function_name=state.environment.active_function_name,
                 address=instruction["address"],
                 swc_id=UNPROTECTED_SELFDESTRUCT,
                 bytecode=state.environment.code.bytecode,

mythril/analysis/modules/unchecked_retval.py

@@ -61,7 +61,6 @@ class UncheckedRetvalModule(DetectionModule):
 
 def _analyze_state(state: GlobalState) -> list:
     instruction = state.get_current_instruction()
-    node = state.node
 
     annotations = cast(
         List[UncheckedRetvalAnnotation],
@@ -80,7 +79,7 @@ def _analyze_state(state: GlobalState) -> list:
         issues = []
         for retval in retvals:
             try:
-                solver.get_model(node.constraints + [retval["retval"] == 0])
+                solver.get_model(state.mstate.constraints + [retval["retval"] == 0])
             except UnsatError:
                 continue
 
@@ -91,8 +90,8 @@ def _analyze_state(state: GlobalState) -> list:
             )
 
             issue = Issue(
-                contract=node.contract_name,
+                contract=state.environment.active_account.contract_name,
-                function_name=node.function_name,
+                function_name=state.environment.active_function_name,
                 address=retval["address"],
                 bytecode=state.environment.code.bytecode,
                 title="Unchecked Call Return Value",

mythril/laser/ethereum/call.py

@@ -136,7 +136,7 @@ def get_callee_account(
     log.debug("Attempting to load dependency")
 
     try:
-        code = dynamic_loader.dynld(environment.active_account.address, callee_address)
+        code = dynamic_loader.dynld(callee_address)
     except ValueError as error:
         log.debug("Unable to execute dynamic loader because: {}".format(str(error)))
         raise error

mythril/laser/ethereum/instructions.py

@@ -1097,7 +1097,7 @@ class Instruction:
             return [global_state]
 
         try:
-            code = self.dynamic_loader.dynld(environment.active_account.address, addr)
+            code = self.dynamic_loader.dynld(addr)
         except (ValueError, AttributeError) as e:
             log.debug("error accessing contract storage due to: " + str(e))
             state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))

mythril/laser/ethereum/plugins/implementations/coverage.py

@@ -0,0 +1,59 @@
+from mythril.laser.ethereum.svm import LaserEVM
+from mythril.laser.ethereum.plugins.plugin import LaserPlugin
+from mythril.laser.ethereum.state.global_state import GlobalState
+
+from typing import Dict, Tuple, List
+
+import logging
+
+log = logging.getLogger(__name__)
+
+
+class InstructionCoveragePlugin(LaserPlugin):
+    """InstructionCoveragePlugin
+
+    This plugin measures the instruction coverage of mythril.
+    The instruction coverage is the ratio between the instructions that have been executed
+    and the total amount of instructions.
+
+    Note that with lazy constraint solving enabled that this metric will be "unsound" as
+    reachability will not be considered for the calculation of instruction coverage.
+
+    """
+
+    def initialize(self, symbolic_vm: LaserEVM):
+        """Initializes the instruction coverage plugin
+
+        Introduces hooks for each instruction
+        :param symbolic_vm:
+        :return:
+        """
+        coverage = {}  # type: Dict[str, Tuple[int, List[bool]]]
+
+        @symbolic_vm.laser_hook("stop_sym_exec")
+        def stop_sym_exec_hook():
+            # Print results
+            for code, code_cov in coverage.items():
+                cov_percentage = sum(code_cov[1]) / float(code_cov[0]) * 100
+
+                log.info(
+                    "Achieved {:.2f}% coverage for code: {}".format(
+                        cov_percentage, code
+                    )
+                )
+
+        @symbolic_vm.laser_hook("execute_state")
+        def execute_state_hook(global_state: GlobalState):
+            # Record coverage
+            code = global_state.environment.code.bytecode
+
+            if code not in coverage.keys():
+                number_of_instructions = len(
+                    global_state.environment.code.instruction_list
+                )
+                coverage[code] = (
+                    number_of_instructions,
+                    [False] * number_of_instructions,
+                )
+
+            coverage[code][1][global_state.mstate.pc] = True

mythril/laser/ethereum/plugins/plugin_factory.py

@@ -21,3 +21,12 @@ class PluginFactory:
         )
 
         return MutationPruner()
+
+    @staticmethod
+    def build_instruction_coverage_plugin() -> LaserPlugin:
+        """ Creates an instance of the instruction coverage plugin"""
+        from mythril.laser.ethereum.plugins.implementations.coverage import (
+            InstructionCoveragePlugin,
+        )
+
+        return InstructionCoveragePlugin()

mythril/support/loader.py

@@ -58,17 +58,15 @@ class DynLoader:
 
         return data
 
-    def dynld(self, contract_address, dependency_address):
+    def dynld(self, dependency_address):
         """
-
-        :param contract_address:
         :param dependency_address:
         :return:
         """
         if not self.contract_loading:
             raise ValueError("Cannot load contract when contract_loading flag is false")
 
-        log.debug("Dynld at contract " + contract_address + ": " + dependency_address)
+        log.debug("Dynld at contract " + dependency_address)
 
         # Ensure that dependency_address is the correct length, with 0s prepended as needed.
         dependency_address = (