Fix issue with cache during summaries (#1619)

* Check versions before using integer module

* Use IssueAnnotations

* Fix misc issues with summaries

* Fix cache issue

* Fix safe functions

mythril/analysis/issue_annotation.py

@@ -3,6 +3,7 @@ from typing import List
 from mythril.analysis.report import Issue
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.smt import Bool
+from copy import deepcopy
 
 
 class IssueAnnotation(StateAnnotation):
@@ -24,3 +25,10 @@ class IssueAnnotation(StateAnnotation):
     @property
     def persist_over_calls(self) -> bool:
         return True
+
+    def __copy__(self):
+        return IssueAnnotation(
+            conditions=deepcopy(self.conditions),
+            issue=self.issue,
+            detector=self.detector,
+        )

mythril/analysis/module/base.py

@@ -64,7 +64,7 @@ class DetectionModule(ABC):
         - issues: The issues used to update the cache
         """
         issues = issues or self.issues
-        for issue in self.issues:
+        for issue in issues:
             self.cache.add((issue.address, issue.bytecode_hash))
 
     def execute(self, target: GlobalState) -> Optional[List[Issue]]:

mythril/analysis/potential_issues.py

@@ -98,7 +98,6 @@ def check_potential_issues(state: GlobalState) -> None:
             unsat_potential_issues.append(potential_issue)
             continue
 
-        potential_issue.detector.cache.add(potential_issue.address)
         issue = Issue(
             contract=potential_issue.contract,
             function_name=potential_issue.function_name,
@@ -123,5 +122,5 @@ def check_potential_issues(state: GlobalState) -> None:
         )
         if args.use_issue_annotations is False:
             potential_issue.detector.issues.append(issue)
-            potential_issue.detector.update_cache()
+            potential_issue.detector.update_cache([issue])
     annotation.potential_issues = unsat_potential_issues

mythril/analysis/solver.py

@@ -63,6 +63,7 @@ def get_transaction_sequence(
     tx_constraints, minimize = _set_minimisation_constraints(
         transaction_sequence, constraints.copy(), [], 5000, global_state.world_state
     )
+
     try:
         model = get_model(tx_constraints, minimize=minimize)
     except UnsatError:

mythril/laser/ethereum/state/constraints.py

@@ -28,7 +28,6 @@ class Constraints(list):
         """
         :return: True/False based on the existence of solution of constraints
         """
-
         try:
             get_model(self)
         except UnsatError:

tests/integration_tests/test_safe_functions.py

@@ -23,7 +23,7 @@ test_data = (
 )
 
 bytes_test_data = (
-    ("safe_funcs.sol.o", ["change_val()"]),
+    ("safe_funcs.sol.o", ["change_val()", "assert1()"]),
     ("suicide.sol.o", []),
     ("overflow.sol.o", ["balanceOf(address)", "totalSupply()"]),
     (