Fix misc issues related to summaries (#1617)

* Check versions before using integer module

* Use IssueAnnotations

* Fix misc issues with summaries

mythril/analysis/module/modules/arbitrary_jump.py

@@ -56,6 +56,7 @@ class ArbitraryJump(DetectionModule):
             )
         except UnsatError:
             return []
+        log.info("Detected arbitrary jump dest")
         issue = Issue(
             contract=state.environment.active_account.contract_name,
             function_name=state.environment.active_function_name,

mythril/analysis/module/modules/suicide.py

@@ -11,6 +11,7 @@ from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
 )
 import logging
+from mythril.laser.ethereum.function_managers import keccak_function_manager
 
 
 log = logging.getLogger(__name__)

mythril/analysis/solver.py

@@ -58,11 +58,8 @@ def get_transaction_sequence(
     :param global_state: GlobalState to generate transaction sequence for
     :param constraints: list of constraints used to generate transaction sequence
     """
-
     transaction_sequence = global_state.world_state.transaction_sequence
-
     concrete_transactions = []
-
     tx_constraints, minimize = _set_minimisation_constraints(
         transaction_sequence, constraints.copy(), [], 5000, global_state.world_state
     )

mythril/ethereum/util.py

@@ -90,7 +90,7 @@ def get_solc_json(file, solc_binary="solc", solc_settings_json=None):
     try:
         result = json.loads(out)
     except JSONDecodeError as e:
-        log.error(f"Encountered a decode error, stdout:{out}, stderr: {stderr}")
+        log.error(f"Encountered a decode error.\n stdout:{out}\n stderr: {stderr}")
         raise e
 
     for error in result.get("errors", []):

mythril/laser/ethereum/function_managers/__init__.py

@@ -1,2 +1,2 @@
 from .exponent_function_manager import exponent_function_manager
-from .keccak_function_manager import keccak_function_manager
+from .keccak_function_manager import keccak_function_manager, KeccakFunctionManager

mythril/laser/ethereum/function_managers/keccak_function_manager.py

@@ -127,7 +127,6 @@ class KeccakFunctionManager:
                 func(concrete_input) == concrete_hash,
                 inverse(func(concrete_input)) == concrete_input,
             )
-
         return condition
 
     def get_concrete_hash_data(self, model) -> Dict[int, List[Optional[int]]]:

mythril/laser/ethereum/state/constraints.py

@@ -52,7 +52,7 @@ class Constraints(list):
         """
         :return: returns the list of constraints
         """
-        return self[:]
+        return self[:] + [keccak_function_manager.create_conditions()]
 
     def __copy__(self) -> "Constraints":
         """

mythril/laser/ethereum/svm.py

@@ -410,7 +410,12 @@ class LaserEVM:
             log.debug("Ending transaction %s.", transaction)
 
             for hook in self._transaction_end_hooks:
-                hook(global_state, transaction, return_global_state, end_signal.revert)
+                hook(
+                    end_signal.global_state,
+                    transaction,
+                    return_global_state,
+                    end_signal.revert,
+                )
 
             if return_global_state is None:
                 if (

mythril/laser/smt/array.py

@@ -29,7 +29,7 @@ class BaseArray:
         """Sets an item in the array, key can be symbolic."""
         self.raw = z3.Store(self.raw, key.raw, value.raw)
 
-    def substitute(self, original_expression: "BaseArray", new_expression: "BaseArray"):
+    def substitute(self, original_expression, new_expression):
         """
 
         :param original_expression: