Merge branch 'develop' into workshop-fixes

mythril/analysis/modules/suicide.py

@@ -60,9 +60,7 @@ class SuicideModule(DetectionModule):
 
         to = state.mstate.stack[-1]
 
-        log.debug(
-            "[SUICIDE] SUICIDE in function " + state.environment.active_function_name
-        )
+        log.debug("SUICIDE in function %s", state.environment.active_function_name)
 
         description_head = "The contract can be killed by anyone."
 
@@ -103,7 +101,7 @@ class SuicideModule(DetectionModule):
             )
             return [issue]
         except UnsatError:
-            log.info("[UNCHECKED_SUICIDE] no model found")
+            log.debug("No model found")
 
         return []
 

mythril/laser/ethereum/instructions.py

@@ -198,6 +198,7 @@ class Instruction:
         """
         # Generalize some ops
         log.debug("Evaluating %s at %i", self.op_code, global_state.mstate.pc)
+
         op = self.op_code.lower()
         if self.op_code.startswith("PUSH"):
             op = "push"
@@ -783,15 +784,10 @@ class Instruction:
             log.debug("Unsupported symbolic calldata offset in CALLDATACOPY")
             dstart = simplify(op1)
 
-        size_sym = False
         try:
             size = util.get_concrete_int(op2)  # type: Union[int, BitVec]
         except TypeError:
             log.debug("Unsupported symbolic size in CALLDATACOPY")
-            size = simplify(op2)
-            size_sym = True
-
-        if size_sym:
             size = 320  # The excess size will get overwritten
 
         size = cast(int, size)
@@ -1397,7 +1393,6 @@ class Instruction:
 
         state = global_state.mstate
         index = state.stack.pop()
-
         state.stack.append(global_state.environment.active_account.storage[index])
         return [global_state]
 
@@ -1410,7 +1405,6 @@ class Instruction:
         """
         state = global_state.mstate
         index, value = state.stack.pop(), state.stack.pop()
-
         global_state.environment.active_account.storage[index] = value
         return [global_state]
 

mythril/laser/ethereum/state/account.py

@@ -75,7 +75,9 @@ class Storage:
     def __getitem__(self, item: BitVec) -> BitVec:
         storage, is_keccak_storage = self._get_corresponding_storage(item)
         if is_keccak_storage:
-            item = self._sanitize(cast(BitVecFunc, item).input_)
+            sanitized_item = self._sanitize(cast(BitVecFunc, item).input_)
+        else:
+            sanitized_item = item
         if (
             self.address
             and self.address.value != 0
@@ -84,7 +86,7 @@ class Storage:
             and (self.dynld and self.dynld.storage_loading)
         ):
             try:
-                storage[item] = symbol_factory.BitVecVal(
+                storage[sanitized_item] = symbol_factory.BitVecVal(
                     int(
                         self.dynld.read_storage(
                             contract_address="0x{:040X}".format(self.address.value),
@@ -95,11 +97,11 @@ class Storage:
                     256,
                 )
                 self.storage_keys_loaded.add(int(item.value))
-                self.printable_storage[item] = storage[item]
+                self.printable_storage[item] = storage[sanitized_item]
             except ValueError as e:
                 log.debug("Couldn't read storage at %s: %s", item, e)
 
-        return simplify(storage[item])
+        return simplify(storage[sanitized_item])
 
     @staticmethod
     def get_map_index(key: BitVec) -> BitVec:

mythril/laser/ethereum/svm.py

@@ -257,6 +257,7 @@ class LaserEVM:
 
     def _add_world_state(self, global_state: GlobalState):
         """ Stores the world_state of the passed global state in the open states"""
+
         for hook in self._add_world_state_hooks:
             try:
                 hook(global_state)
@@ -325,6 +326,8 @@ class LaserEVM:
             new_global_state.node = global_state.node
             new_global_state.mstate.constraints = global_state.mstate.constraints
 
+            log.debug("Starting new transaction %s", start_signal.transaction)
+
             return [new_global_state], op_code
 
         except TransactionEndSignal as end_signal:
@@ -332,6 +335,8 @@ class LaserEVM:
                 -1
             ]
 
+            log.debug("Ending transaction %s.", transaction)
+
             if return_global_state is None:
                 if (
                     not isinstance(transaction, ContractCreationTransaction)

mythril/laser/ethereum/transaction/transaction_models.py

@@ -134,6 +134,14 @@ class BaseTransaction:
     def initial_global_state(self) -> GlobalState:
         raise NotImplementedError
 
+    def __str__(self) -> str:
+        return "{} {} from {} to {:#42x}".format(
+            self.__class__.__name__,
+            self.id,
+            self.caller,
+            int(str(self.callee_account.address)) if self.callee_account else -1,
+        )
+
 
 class MessageCallTransaction(BaseTransaction):
     """Transaction object models an transaction."""