Use last jump as source for yul mapping (#1518)

mythril/analysis/module/modules/exceptions.py

@@ -1,13 +1,14 @@
 """This module contains the detection code for reachable exceptions."""
 import logging
 
-from typing import List
+from typing import List, cast
 from mythril.analysis import solver
 from mythril.analysis.module.base import DetectionModule, EntryPoint
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import ASSERT_VIOLATION
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum import util
 
 log = logging.getLogger(__name__)
@@ -16,6 +17,17 @@ log = logging.getLogger(__name__)
 PANIC_SIGNATURE = [78, 72, 123, 113]
 
 
+class LastJumpAnnotation(StateAnnotation):
+    """ 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
+
+    def __copy__(self):
+        new_annotation = LastJumpAnnotation(self.last_jump)
+        return new_annotation
+
+
 class Exceptions(DetectionModule):
     """"""
 
@@ -23,7 +35,7 @@ class Exceptions(DetectionModule):
     swc_id = ASSERT_VIOLATION
     description = "Checks whether any exception states are reachable."
     entry_point = EntryPoint.CALLBACK
-    pre_hooks = ["ASSERT_FAIL", "REVERT"]
+    pre_hooks = ["ASSERT_FAIL", "JUMP", "REVERT"]
 
     def _execute(self, state: GlobalState) -> None:
         """
@@ -49,6 +61,23 @@ class Exceptions(DetectionModule):
         :return:
         """
         opcode = state.get_current_instruction()["opcode"]
+        address = state.get_current_instruction()["address"]
+
+        annotations = cast(
+            List[LastJumpAnnotation],
+            [a for a in state.get_annotations(LastJumpAnnotation)],
+        )
+        if len(annotations) == 0:
+            state.annotate(LastJumpAnnotation())
+            annotations = cast(
+                List[LastJumpAnnotation],
+                [a for a in state.get_annotations(LastJumpAnnotation)],
+            )
+
+        if opcode == "JUMP":
+            annotations[0].last_jump = address
+            return []
+
         if opcode == "REVERT" and not is_assertion_failure(state):
             return []
 
@@ -57,7 +86,6 @@ class Exceptions(DetectionModule):
         )
 
         try:
-            address = state.get_current_instruction()["address"]
             description_tail = (
                 "It is possible to trigger an assertion violation. Note that Solidity assert() statements should "
                 "only be used to check invariants. Review the transaction trace generated for this issue and "
@@ -68,6 +96,7 @@ class Exceptions(DetectionModule):
             transaction_sequence = solver.get_transaction_sequence(
                 state, state.world_state.constraints
             )
+
             issue = Issue(
                 contract=state.environment.active_account.contract_name,
                 function_name=state.environment.active_function_name,
@@ -80,6 +109,7 @@ class Exceptions(DetectionModule):
                 bytecode=state.environment.code.bytecode,
                 transaction_sequence=transaction_sequence,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                source_location=annotations[0].last_jump,
             )
             return [issue]
 

mythril/analysis/report.py

@@ -34,6 +34,7 @@ class Issue:
         description_head="",
         description_tail="",
         transaction_sequence=None,
+        source_location=None,
     ):
         """
 
@@ -66,6 +67,7 @@ class Issue:
         self.discovery_time = time() - StartTime().global_start_time
         self.bytecode_hash = get_code_hash(bytecode)
         self.transaction_sequence = transaction_sequence
+        self.source_location = source_location
 
     @property
     def transaction_sequence_users(self):
@@ -141,6 +143,11 @@ class Issue:
         :param contract:
         """
         if self.address and isinstance(contract, SolidityContract):
+            if self.source_location:
+                codeinfo = contract.get_source_info(
+                    self.source_location, constructor=(self.function == "constructor")
+                )
+            else:
                 codeinfo = contract.get_source_info(
                     self.address, constructor=(self.function == "constructor")
                 )

mythril/solidity/soliditycontract.py

@@ -90,7 +90,6 @@ class SolidityContract(EVMContract):
         self.solc_indices = self.get_solc_indices(data)
         self.solc_json = data
         self.input_file = input_file
-
         has_contract = False
 
         # If a contract name has been specified, find the bytecode of that specific contract
@@ -195,6 +194,7 @@ class SolidityContract(EVMContract):
         mappings = self.constructor_mappings if constructor else self.mappings
         index = helper.get_instruction_index(disassembly.instruction_list, address)
         file_index = mappings[index].solidity_file_idx
+
         if file_index == -1:
             # If issue is detected in an internal file
             return None