Add tx data to all modules

mythril/analysis/modules/dependence_on_predictable_vars.py

@@ -27,22 +27,25 @@ def is_prehook() -> bool:
 class PredictableValueAnnotation:
     """Symbol annotation used if a variable is initialized from a predictable environment variable."""
 
-    def __init__(self, operation: str) -> None:
+    def __init__(self, operation: str, add_constraints=None) -> None:
         self.operation = operation
+        self.add_constraints = add_constraints
 
 
 class PredictablePathAnnotation(StateAnnotation):
     """State annotation used when a path is chosen based on a predictable variable."""
 
-    def __init__(self, operation: str, location: int) -> None:
+    def __init__(self, operation: str, location: int, add_constraints=None) -> None:
         self.operation = operation
         self.location = location
+        self.add_constraints = add_constraints
 
 
 class OldBlockNumberUsedAnnotation(StateAnnotation):
     """State annotation set in blockhash prehook if the input value is lower than the current block number."""
 
-    def __init__(self) -> None:
+    def __init__(self, constraints) -> None:
+        self.block_constraints = constraints
         pass
 
 
@@ -92,6 +95,13 @@ def _analyze_states(state: GlobalState) -> list:
             for annotation in state.annotations:
 
                 if isinstance(annotation, PredictablePathAnnotation):
+                    constraints = state.mstate.constraints + annotation.add_constraints
+                    try:
+                        transaction_sequence = solver.get_transaction_sequence(
+                            state, constraints
+                        )
+                    except UnsatError:
+                        continue
                     description = (
                         "The "
                         + annotation.operation
@@ -133,6 +143,7 @@ def _analyze_states(state: GlobalState) -> list:
                         description_head="A control flow decision is made based on a predictable variable.",
                         description_tail=description,
                         gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                        transaction_sequence=transaction_sequence,
                     )
                     issues.append(issue)
 
@@ -147,6 +158,7 @@ def _analyze_states(state: GlobalState) -> list:
                         PredictablePathAnnotation(
                             annotation.operation,
                             state.get_current_instruction()["address"],
+                            add_constraints=annotation.add_constraints,
                         )
                     )
                     break
@@ -166,8 +178,8 @@ def _analyze_states(state: GlobalState) -> list:
 
                 # Why the second constraint? Because without it Z3 returns a solution where param overflows.
 
-                solver.get_model(constraint)
-                state.annotate(OldBlockNumberUsedAnnotation())
+                solver.get_model(state.mstate.constraints + constraint)
+                state.annotate(OldBlockNumberUsedAnnotation(constraint))
 
             except UnsatError:
                 pass
@@ -186,8 +198,12 @@ def _analyze_states(state: GlobalState) -> list:
             )
 
             if len(annotations):
+                # We can append any block constraint here
                 state.mstate.stack[-1].annotate(
-                    PredictableValueAnnotation("block hash of a previous block")
+                    PredictableValueAnnotation(
+                        "block hash of a previous block",
+                        add_constraints=annotations[0].block_constraints,
+                    )
                 )
         else:
             # Always create an annotation when COINBASE, GASLIMIT, TIMESTAMP or NUMBER is executed.

mythril/analysis/modules/deprecated_ops.py

@@ -1,5 +1,6 @@
 """This module contains the detection code for deprecated op codes."""
 from mythril.analysis.report import Issue
+from mythril.analysis.solver import get_transaction_sequence, UnsatError
 from mythril.analysis.swc_data import DEPRECATED_FUNCTIONS_USAGE
 from mythril.analysis.modules.base import DetectionModule
 from mythril.laser.ethereum.state.global_state import GlobalState
@@ -47,7 +48,10 @@ def _analyze_state(state):
         swc_id = DEPRECATED_FUNCTIONS_USAGE
     else:
         return
-
+    try:
+        transaction_sequence = get_transaction_sequence(state, state.mstate.constraints)
+    except UnsatError:
+        return
     issue = Issue(
         contract=state.environment.active_account.contract_name,
         function_name=state.environment.active_function_name,
@@ -59,6 +63,7 @@ def _analyze_state(state):
         description_head=description_head,
         description_tail=description_tail,
         gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+        transaction_sequence=transaction_sequence,
     )
     return [issue]
 

mythril/analysis/modules/dos.py

@@ -6,6 +6,7 @@ from typing import Dict, cast, List
 from mythril.analysis.swc_data import DOS_WITH_BLOCK_GAS_LIMIT
 from mythril.analysis.report import Issue
 from mythril.analysis.modules.base import DetectionModule
+from mythril.analysis.solver import get_transaction_sequence, UnsatError
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum import util
@@ -103,7 +104,12 @@ class DOS(DetectionModule):
             description_tail = "{} is executed in a loop. Be aware that the transaction may fail to execute if the loop is unbounded and the necessary gas exceeds the block gas limit.".format(
                 operation
             )
-
+            try:
+                transaction_sequence = get_transaction_sequence(
+                    state, state.mstate.constraints
+                )
+            except UnsatError:
+                return []
             issue = Issue(
                 contract=state.environment.active_account.contract_name,
                 function_name=state.environment.active_function_name,
@@ -115,6 +121,7 @@ class DOS(DetectionModule):
                 description_head=description_head,
                 description_tail=description_tail,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                transaction_sequence=transaction_sequence,
             )
 
             return [issue]

mythril/analysis/modules/multiple_sends.py

@@ -4,6 +4,7 @@ from copy import copy
 from typing import cast, List
 
 from mythril.analysis.report import Issue
+from mythril.analysis.solver import get_transaction_sequence, UnsatError
 from mythril.analysis.swc_data import MULTIPLE_SENDS
 from mythril.analysis.modules.base import DetectionModule
 from mythril.laser.ethereum.state.annotation import StateAnnotation
@@ -73,7 +74,12 @@ def _analyze_state(state: GlobalState):
     else:  # RETURN or STOP
 
         for offset in call_offsets[1:]:
-
+            try:
+                transaction_sequence = get_transaction_sequence(
+                    state, state.mstate.constraints
+                )
+            except UnsatError:
+                continue
             description_tail = (
                 "This call is executed after a previous call in the same transaction. "
                 "Try to isolate each call, transfer or send into its own transaction."
@@ -90,6 +96,7 @@ def _analyze_state(state: GlobalState):
                 description_head="Multiple calls are executed in the same transaction.",
                 description_tail=description_tail,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                transaction_sequence=transaction_sequence,
             )
 
             return [issue]

mythril/analysis/modules/state_change_external_calls.py

@@ -35,7 +35,25 @@ class StateChangeCallsAnnotation(StateAnnotation):
     def get_issue(self, global_state: GlobalState) -> Optional[Issue]:
         if not self.state_change_states:
             return None
+        constraints = copy(global_state.mstate.constraints)
+        gas = self.call_state.mstate.stack[-1]
+        to = self.call_state.mstate.stack[-2]
+        constraints += [
+            UGT(gas, symbol_factory.BitVecVal(2300, 256)),
+            Or(
+                to > symbol_factory.BitVecVal(16, 256),
+                to == symbol_factory.BitVecVal(0, 256),
+            ),
+        ]
+        if self.user_defined_address:
+            constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF]
 
+        try:
+            transaction_sequence = solver.get_transaction_sequence(
+                global_state, constraints
+            )
+        except UnsatError:
+            return None
         severity = "Medium" if self.user_defined_address else "Low"
         address = global_state.get_current_instruction()["address"]
         logging.debug(
@@ -59,6 +77,7 @@ class StateChangeCallsAnnotation(StateAnnotation):
             description_tail=description_tail,
             swc_id=REENTRANCY,
             bytecode=global_state.environment.code.bytecode,
+            transaction_sequence=transaction_sequence,
         )
 
 

mythril/analysis/modules/unchecked_retval.py

@@ -78,7 +78,9 @@ def _analyze_state(state: GlobalState) -> list:
         issues = []
         for retval in retvals:
             try:
-                solver.get_model(state.mstate.constraints + [retval["retval"] == 0])
+                transaction_sequence = solver.get_transaction_sequence(
+                    state, state.mstate.constraints + [retval["retval"] == 0]
+                )
             except UnsatError:
                 continue
 
@@ -99,6 +101,7 @@ def _analyze_state(state: GlobalState) -> list:
                 description_head="The return value of a message call is not checked.",
                 description_tail=description_tail,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                transaction_sequence=transaction_sequence,
             )
 
             issues.append(issue)