Use better issue annotations for search (#1615)

* Check versions before using integer module

* Use IssueAnnotations

mythril/analysis/issue_annotation.py

@@ -0,0 +1,26 @@
+from typing import List
+
+from mythril.analysis.report import Issue
+from mythril.laser.ethereum.state.annotation import StateAnnotation
+from mythril.laser.smt import Bool
+
+
+class IssueAnnotation(StateAnnotation):
+    def __init__(self, conditions: List[Bool], issue: Issue, detector):
+        """
+        Issue Annotation to propogate issues
+        - conditions: A list of independent conditions [a, b, c, ...]
+                      Each of these have to be independently be satisfied
+        - issue: The issue of the annotation
+        - detector: The detection module
+        """
+        self.conditions = conditions
+        self.issue = issue
+        self.detector = detector
+
+    def persist_to_world_state(self) -> bool:
+        return True
+
+    @property
+    def persist_over_calls(self) -> bool:
+        return True

mythril/analysis/module/base.py

@@ -4,10 +4,11 @@ This module includes an definition of the DetectionModule interface.
 DetectionModules implement different analysis rules to find weaknesses and vulnerabilities.
 """
 import logging
-from typing import List, Set, Optional, Tuple, Union
+from typing import List, Set, Optional, Tuple
 
 from mythril.analysis.report import Issue
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.support.support_args import args
 from mythril.support.support_utils import get_code_hash
 from abc import ABC, abstractmethod
 from enum import Enum
@@ -86,7 +87,8 @@ class DetectionModule(ABC):
 
         result = self._execute(target)
         log.debug("Exiting analysis module: {}".format(self.__class__.__name__))
-        if result:
+
+        if result and not args.use_issue_annotations:
             self.update_cache(result)
             self.issues += result
 

mythril/analysis/module/modules/arbitrary_jump.py

@@ -1,9 +1,11 @@
 """This module contains the detection code for Arbitrary jumps."""
 import logging
 from mythril.analysis.solver import get_transaction_sequence, UnsatError
+from mythril.analysis.issue_annotation import IssueAnnotation
 from mythril.analysis.module.base import DetectionModule, Issue, EntryPoint
 from mythril.analysis.swc_data import ARBITRARY_JUMP
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.smt import And
 
 log = logging.getLogger(__name__)
 
@@ -37,8 +39,7 @@ class ArbitraryJump(DetectionModule):
         """
         return self._analyze_state(state)
 
-    @staticmethod
-    def _analyze_state(state):
+    def _analyze_state(self, state):
         """
 
         :param state:
@@ -70,6 +71,14 @@ class ArbitraryJump(DetectionModule):
             gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             transaction_sequence=transaction_sequence,
         )
+        state.annotate(
+            IssueAnnotation(
+                conditions=[And(*state.world_state.constraints)],
+                issue=issue,
+                detector=self,
+            )
+        )
+
         return [issue]
 
 

mythril/analysis/module/modules/delegatecall.py

@@ -14,7 +14,7 @@ from mythril.laser.ethereum.transaction.transaction_models import (
 from mythril.analysis.module.base import DetectionModule, EntryPoint
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import symbol_factory, UGT
+from mythril.laser.smt import symbol_factory, UGT, Bool
 
 log = logging.getLogger(__name__)
 

mythril/analysis/module/modules/dependence_on_origin.py

@@ -2,13 +2,14 @@
 dependence."""
 import logging
 from copy import copy
-
+from mythril.analysis.issue_annotation import IssueAnnotation
 from mythril.analysis.module.base import DetectionModule, EntryPoint
 from mythril.analysis.report import Issue
 from mythril.exceptions import UnsatError
 from mythril.analysis import solver
 from mythril.analysis.swc_data import TX_ORIGIN_USAGE
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.smt import And
 from typing import List
 
 log = logging.getLogger(__name__)
@@ -40,8 +41,7 @@ class TxOrigin(DetectionModule):
         """
         return self._analyze_state(state)
 
-    @staticmethod
-    def _analyze_state(state: GlobalState) -> List[Issue]:
+    def _analyze_state(self, state: GlobalState) -> List[Issue]:
         """
 
         :param state:
@@ -92,6 +92,11 @@ class TxOrigin(DetectionModule):
                         gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
                         transaction_sequence=transaction_sequence,
                     )
+                    state.annotate(
+                        IssueAnnotation(
+                            conditions=[And(*constraints)], issue=issue, detector=self
+                        )
+                    )
 
                     issues.append(issue)
 

mythril/analysis/module/modules/dependence_on_predictable_vars.py

@@ -2,11 +2,12 @@
 dependence."""
 import logging
 
+from mythril.analysis.issue_annotation import IssueAnnotation
 from mythril.analysis.module.base import DetectionModule, EntryPoint
 from mythril.analysis.report import Issue
 from mythril.exceptions import UnsatError
 from mythril.analysis import solver
-from mythril.laser.smt import ULT, symbol_factory
+from mythril.laser.smt import And, ULT, symbol_factory
 from mythril.analysis.swc_data import TIMESTAMP_DEPENDENCE, WEAK_RANDOMNESS
 from mythril.analysis.module.module_helpers import is_prehook
 from mythril.laser.ethereum.state.global_state import GlobalState
@@ -54,8 +55,7 @@ class PredictableVariables(DetectionModule):
         """
         return self._analyze_state(state)
 
-    @staticmethod
-    def _analyze_state(state: GlobalState) -> List[Issue]:
+    def _analyze_state(self, state: GlobalState) -> List[Issue]:
         """
 
         :param state:
@@ -126,7 +126,13 @@ class PredictableVariables(DetectionModule):
                             ),
                             transaction_sequence=transaction_sequence,
                         )
-
+                        state.annotate(
+                            IssueAnnotation(
+                                conditions=[And(*constraints)],
+                                issue=issue,
+                                detector=self,
+                            )
+                        )
                         issues.append(issue)
 
             elif opcode == "BLOCKHASH":

mythril/analysis/module/modules/exceptions.py

@@ -3,6 +3,7 @@ import logging
 
 from typing import List, cast
 from mythril.analysis import solver
+from mythril.analysis.issue_annotation import IssueAnnotation
 from mythril.analysis.module.base import DetectionModule, EntryPoint
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import ASSERT_VIOLATION
@@ -10,6 +11,7 @@ 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
+from mythril.laser.smt import And
 
 log = logging.getLogger(__name__)
 
@@ -45,8 +47,7 @@ class Exceptions(DetectionModule):
         """
         return self._analyze_state(state)
 
-    @staticmethod
-    def _analyze_state(state) -> List[Issue]:
+    def _analyze_state(self, state) -> List[Issue]:
         """
 
         :param state:
@@ -103,6 +104,14 @@ class Exceptions(DetectionModule):
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
                 source_location=annotations[0].last_jump,
             )
+            state.annotate(
+                IssueAnnotation(
+                    conditions=[And(*state.world_state.constraints)],
+                    issue=issue,
+                    detector=self,
+                )
+            )
+
             return [issue]
 
         except UnsatError:

mythril/analysis/module/modules/integer.py

@@ -4,6 +4,7 @@ underflows."""
 from math import log2, ceil
 from typing import cast, List, Set
 from mythril.analysis import solver
+from mythril.analysis.issue_annotation import IssueAnnotation
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW
 from mythril.exceptions import UnsatError
@@ -102,7 +103,7 @@ class IntegerArithmetics(DetectionModule):
         self._ostates_satisfiable = set()
         self._ostates_unsatisfiable = set()
 
-    def _execute(self, state: GlobalState) -> None:
+    def _execute(self, state: GlobalState) -> List[Issue]:
         """Executes analysis module for integer underflow and integer overflow.
 
         :param state: Statespace to analyse
@@ -122,8 +123,12 @@ class IntegerArithmetics(DetectionModule):
             "STOP": [self._handle_transaction_end],
             "EXP": [self._handle_exp],
         }
+        results = []
         for func in funcs[opcode]:
-            func(state)
+            result = func(state)
+            if result and len(result) > 0:
+                results += result
+        return results
 
     def _get_args(self, state):
         stack = state.mstate.stack
@@ -253,10 +258,10 @@ class IntegerArithmetics(DetectionModule):
                 if isinstance(annotation, OverUnderflowAnnotation):
                     state_annotation.overflowing_state_annotations.add(annotation)
 
-    def _handle_transaction_end(self, state: GlobalState) -> None:
+    def _handle_transaction_end(self, state: GlobalState) -> List[Issue]:
 
         state_annotation = _get_overflowunderflow_state_annotation(state)
-
+        issues = []
         for annotation in state_annotation.overflowing_state_annotations:
 
             ostate = annotation.overflowing_state
@@ -313,10 +318,13 @@ class IntegerArithmetics(DetectionModule):
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
                 transaction_sequence=transaction_sequence,
             )
-
-            address = _get_address_from_state(ostate)
-            self.cache.add(address)
-            self.issues.append(issue)
+            state.annotate(
+                IssueAnnotation(
+                    issue=issue, detector=self, conditions=[And(*constraints)]
+                )
+            )
+            issues.append(issue)
+        return issues
 
 
 detector = IntegerArithmetics()

mythril/analysis/module/modules/multiple_sends.py

@@ -2,13 +2,14 @@
 a single transaction."""
 from copy import copy
 from typing import cast, List
-
+from mythril.analysis.issue_annotation import IssueAnnotation
 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.module.base import DetectionModule, EntryPoint
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.smt import And
 import logging
 
 log = logging.getLogger(__name__)
@@ -36,8 +37,7 @@ class MultipleSends(DetectionModule):
     def _execute(self, state: GlobalState) -> None:
         return self._analyze_state(state)
 
-    @staticmethod
-    def _analyze_state(state: GlobalState):
+    def _analyze_state(self, state: GlobalState):
         """
         :param state: the current state
         :return: returns the issues for that corresponding state
@@ -90,7 +90,13 @@ class MultipleSends(DetectionModule):
                     gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
                     transaction_sequence=transaction_sequence,
                 )
-
+                state.annotate(
+                    IssueAnnotation(
+                        conditions=[And(*state.world_state.constraints)],
+                        issue=issue,
+                        detector=self,
+                    )
+                )
                 return [issue]
 
         return []

mythril/analysis/module/modules/suicide.py

@@ -2,6 +2,7 @@ from mythril.analysis import solver
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT
 from mythril.exceptions import UnsatError
+from mythril.analysis.issue_annotation import IssueAnnotation
 from mythril.analysis.module.base import DetectionModule, EntryPoint
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction.symbolic import ACTORS
@@ -49,8 +50,7 @@ class AccidentallyKillable(DetectionModule):
         """
         return self._analyze_state(state)
 
-    @staticmethod
-    def _analyze_state(state):
+    def _analyze_state(self, state):
         log.info("Suicide module: Analyzing suicide instruction")
         instruction = state.get_current_instruction()
 
@@ -60,20 +60,22 @@ class AccidentallyKillable(DetectionModule):
 
         description_head = "Any sender can cause the contract to self-destruct."
 
-        constraints = []
+        attacker_constraints = []
 
         for tx in state.world_state.transaction_sequence:
             if not isinstance(tx, ContractCreationTransaction):
-                constraints.append(
+                attacker_constraints.append(
                     And(tx.caller == ACTORS.attacker, tx.caller == tx.origin)
                 )
         try:
             try:
-                transaction_sequence = solver.get_transaction_sequence(
-                    state,
+                constraints = (
                     state.world_state.constraints
-                    + constraints
-                    + [to == ACTORS.attacker],
+                    + [to == ACTORS.attacker]
+                    + attacker_constraints
+                )
+                transaction_sequence = solver.get_transaction_sequence(
+                    state, constraints
                 )
 
                 description_tail = (
@@ -84,8 +86,9 @@ class AccidentallyKillable(DetectionModule):
                 )
 
             except UnsatError:
+                constraints = state.world_state.constraints + attacker_constraints
                 transaction_sequence = solver.get_transaction_sequence(
-                    state, state.world_state.constraints + constraints
+                    state, constraints
                 )
                 description_tail = (
                     "Any sender can trigger execution of the SELFDESTRUCT instruction to destroy this "
@@ -106,6 +109,12 @@ class AccidentallyKillable(DetectionModule):
                 transaction_sequence=transaction_sequence,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
+            state.annotate(
+                IssueAnnotation(
+                    conditions=[And(*constraints)], issue=issue, detector=self
+                )
+            )
+
             return [issue]
         except UnsatError:
             log.debug("No model found")

mythril/analysis/module/modules/unchecked_retval.py

@@ -4,12 +4,13 @@ from copy import copy
 from typing import cast, List
 
 from mythril.analysis import solver
+from mythril.analysis.issue_annotation import IssueAnnotation
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import UNCHECKED_RET_VAL
 from mythril.analysis.module.base import DetectionModule, EntryPoint
 from mythril.exceptions import UnsatError
+from mythril.laser.smt import And
 from mythril.laser.smt.bitvec import BitVec
-
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum.state.global_state import GlobalState
 
@@ -112,6 +113,14 @@ class UncheckedRetval(DetectionModule):
                     gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
                     transaction_sequence=transaction_sequence,
                 )
+                conditions = [
+                    And(*(state.world_state.constraints + [retval["retval"] == 1])),
+                    And(*(state.world_state.constraints + [retval["retval"] == 1])),
+                ]
+
+                state.annotate(
+                    IssueAnnotation(conditions=conditions, issue=issue, detector=self)
+                )
 
                 issues.append(issue)
 

mythril/analysis/module/modules/user_assertions.py

@@ -2,11 +2,12 @@
 calls."""
 
 from mythril.analysis import solver
+from mythril.analysis.issue_annotation import IssueAnnotation
 from mythril.analysis.potential_issues import Issue
 from mythril.analysis.swc_data import ASSERT_VIOLATION
 from mythril.analysis.module.base import DetectionModule, EntryPoint
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import Extract
+from mythril.laser.smt import Extract, And
 from mythril.exceptions import UnsatError
 import logging
 import eth_abi
@@ -110,6 +111,13 @@ class UserAssertions(DetectionModule):
                 transaction_sequence=transaction_sequence,
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
+            state.annotate(
+                IssueAnnotation(
+                    detector=self,
+                    issue=issue,
+                    conditions=[And(*state.world_state.constraints)],
+                )
+            )
             return [issue]
 
         except UnsatError:

mythril/analysis/potential_issues.py

@@ -1,8 +1,11 @@
 from mythril.analysis.report import Issue
+from mythril.analysis.issue_annotation import IssueAnnotation
 from mythril.analysis.solver import get_transaction_sequence
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.smt import And
+from mythril.support.support_args import args
 
 
 class PotentialIssue:
@@ -96,8 +99,7 @@ def check_potential_issues(state: GlobalState) -> None:
             continue
 
         potential_issue.detector.cache.add(potential_issue.address)
-        potential_issue.detector.issues.append(
-            Issue(
+        issue = Issue(
             contract=potential_issue.contract,
             function_name=potential_issue.function_name,
             address=potential_issue.address,
@@ -110,6 +112,16 @@ def check_potential_issues(state: GlobalState) -> None:
             description_tail=potential_issue.description_tail,
             transaction_sequence=transaction_sequence,
         )
+        state.annotate(
+            IssueAnnotation(
+                detector=potential_issue.detector,
+                issue=issue,
+                conditions=[
+                    And(*(state.world_state.constraints + potential_issue.constraints))
+                ],
             )
+        )
+        if args.use_issue_annotations is False:
+            potential_issue.detector.issues.append(issue)
             potential_issue.detector.update_cache()
     annotation.potential_issues = unsat_potential_issues

mythril/support/support_args.py

@@ -1,4 +1,8 @@
-class Args:
+from typing import List
+from mythril.support.support_utils import Singleton
+
+
+class Args(object, metaclass=Singleton):
     """
     This module helps in preventing args being sent through multiple of classes to reach
     any analysis/laser module
@@ -14,6 +18,7 @@ class Args:
         self.solver_log = None
         self.transaction_sequences: List[List[str]] = None
         self.use_integer_module = True
+        self.use_issue_annotations = False
 
 
 args = Args()