Add changeability check to caller constraint and add docstring

mythril/analysis/modules/suicide.py

@@ -4,6 +4,7 @@ from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction import ContractCreationTransaction
+import re
 import logging
 
 
@@ -55,25 +56,25 @@ def _analyze_state(state, node):
         description += "The remaining Ether is sent to: " + str(to) + "\n"
 
     not_creator_constraints = []
-    if len(state.world_state.transaction_sequence) >= 1:
-        creator = None
-        if isinstance(
-            state.world_state.transaction_sequence[0], ContractCreationTransaction
-        ):
-            creator = state.world_state.transaction_sequence[0].caller
-        if creator is not None:
-            for transaction in state.world_state.transaction_sequence[1:]:
-                not_creator_constraints.append(
-                    Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator))
-                )
-                not_creator_constraints.append(
-                    Not(Extract(159, 0, transaction.caller) == 0)
-                )
-        else:
-            for transaction in state.world_state.transaction_sequence:
-                not_creator_constraints.append(
-                    Not(Extract(159, 0, transaction.caller) == 0)
-                )
+    creator = None
+    if isinstance(
+        state.world_state.transaction_sequence[0], ContractCreationTransaction
+    ):
+        creator = state.world_state.transaction_sequence[0].caller
+    if creator is not None:
+        for transaction in state.world_state.transaction_sequence[1:]:
+            not_creator_constraints.append(
+                Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator))
+            )
+            not_creator_constraints.append(
+                Not(Extract(159, 0, transaction.caller) == 0)
+            )
+    else:
+        for transaction in state.world_state.transaction_sequence:
+            not_creator_constraints.append(
+                Not(Extract(159, 0, transaction.caller) == 0)
+            )
+        not_creator_constraints.append(check_changeable_constraints(node.constraints))
 
     try:
         model = solver.get_model(node.constraints + not_creator_constraints)
@@ -100,3 +101,12 @@ def _analyze_state(state, node):
         logging.debug("[UNCHECKED_SUICIDE] no model found")
 
     return issues
+
+
+def check_changeable_constraints(constraints):
+    for constraint in constraints:
+        if re.search(r"caller", str(constraint)) and re.search(
+            r"[0-9]{20}", str(constraint)
+        ):
+            return False
+    return True

mythril/laser/ethereum/svm.py

@@ -120,6 +120,11 @@ class LaserEVM:
             logging.info("Achieved {} coverage for code: {}".format(cov, code))
 
     def _execute_transactions(self, address):
+        """
+        This function executes multiple transactions on the address based on the coverage
+        :param address: Address of the contract
+        :return:
+        """
         self.coverage = {}
         for i in range(self.max_transaction_count):
             initial_coverage = self._get_covered_instructions()