Cleaned up some logic. Fixed issue with VMException and freezing on staticcall.

mythril/analysis/call_helpers.py

@@ -18,7 +18,7 @@ def get_call_from_state(state: GlobalState) -> Union[Call, None]:
     op = instruction["opcode"]
     stack = state.mstate.stack
 
-    if op in ("CALL", "CALLCODE", "STATICCALL"):
+    if op in ("CALL", "CALLCODE"):
         gas, to, value, meminstart, meminsz, memoutstart, memoutsz = (
             get_variable(stack[-1]),
             get_variable(stack[-2]),

mythril/laser/ethereum/instructions.py

@@ -1789,7 +1789,6 @@ class Instruction:
         :param global_state:
         :return:
         """
-
         call_value, mem_offset, mem_size = global_state.mstate.pop(3)
 
         return self._create_transaction_helper(
@@ -1801,12 +1800,10 @@ class Instruction:
         call_value, mem_offset, mem_size = global_state.mstate.pop(3)
         call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size)
         if global_state.last_return_data:
-            global_state.mstate.stack.append(
-                symbol_factory.BitVecVal(int(global_state.last_return_data, 16), 256)
-            )
+            return_val = symbol_factory.BitVecVal(int(global_state.last_return_data, 16), 256)
         else:
-            global_state.mstate.stack.append(symbol_factory.BitVecVal(0, 256))
-
+            return_val = symbol_factory.BitVecVal(0, 256)
+        global_state.mstate.stack.append(return_val)
         return [global_state]
 
     @StateTransition(is_state_mutation_instruction=True)
@@ -1827,11 +1824,10 @@ class Instruction:
         call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4)
         call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size)
         if global_state.last_return_data:
-            global_state.mstate.stack.append(
-                symbol_factory.BitVecVal(int(global_state.last_return_data), 256)
-            )
+            return_val = symbol_factory.BitVecVal(int(global_state.last_return_data), 256)
         else:
-            global_state.mstate.stack.append(symbol_factory.BitVecVal(0, 256))
+            return_val = symbol_factory.BitVecVal(0, 256)
+        global_state.mstate.stack.append(return_val)
         return [global_state]
 
     @StateTransition()
@@ -2287,6 +2283,7 @@ class Instruction:
         )
         raise TransactionStartSignal(transaction, self.op_code, global_state)
 
+    @StateTransition()
     def staticcall_post(self, global_state: GlobalState) -> List[GlobalState]:
         return self.post_handler(global_state, function_name="staticcall")
 
@@ -2294,8 +2291,9 @@ class Instruction:
         instr = global_state.get_current_instruction()
 
         try:
+            with_value = function_name is not "staticcall"
             callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters(
-                global_state, self.dynamic_loader, True
+                global_state, self.dynamic_loader, with_value
             )
         except ValueError as e:
             log.debug(

mythril/laser/ethereum/transaction/transaction_models.py

@@ -201,7 +201,7 @@ class ContractCreationTransaction(BaseTransaction):
         callee_account = world_state.create_account(
             0, concrete_storage=True, creator=caller.value, address=contract_address
         )
-        callee_account.contract_name = contract_name
+        callee_account.contract_name = contract_name or callee_account.contract_name
         # init_call_data "should" be false, but it is easier to model the calldata symbolically
         # and add logic in codecopy/codesize/calldatacopy/calldatasize than to model code "correctly"
         super().__init__(