Merge with master

Dockerfile

@@ -5,6 +5,7 @@ COPY . /opt/mythril
 RUN apt-get update \
   && apt-get install -y \
      build-essential \
+     locales \
      python-pip-whl=9.0.1-2 \
      python3-pip=9.0.1-2 \
      python3-setuptools \
@@ -22,4 +23,9 @@ RUN apt-get update \
   && pip3 install -r requirements.txt \
   && python setup.py install
 
+RUN locale-gen en_US.UTF-8
+ENV LANG en_US.UTF-8
+ENV LANGUAGE en_US.en
+ENV LC_ALL en_US.UTF-8
+
 ENTRYPOINT ["/usr/local/bin/myth"]

README.md

@@ -1,5 +1,5 @@
 # Mythril OSS [![Tweet](https://img.shields.io/twitter/url/http/shields.io.svg?style=social)](https://twitter.com/intent/tweet?text=Mythril%20-%20Security%20Analyzer%20for%20Ethereum%20Smart%20Contracts&url=https://www.github.com/ConsenSys/mythril)
-[![Discord](https://img.shields.io/discord/481002907366588416.svg)](https://discord.gg/vwX58mr)
+[![Discord](https://img.shields.io/discord/481002907366588416.svg)](https://discord.gg/E3YrVtG)
 [![PyPI](https://badge.fury.io/py/mythril.svg)](https://pypi.python.org/pypi/mythril)
 ![Master Build Status](https://img.shields.io/circleci/project/github/ConsenSys/mythril/master.svg)
 [![Waffle.io - Columns and their card count](https://badge.waffle.io/ConsenSys/mythril.svg?columns=all)](https://waffle.io/ConsenSys/mythril)
@@ -9,7 +9,7 @@
 
 Mythril OSS is the classic security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. 
 
-Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/dFHQGrE) will serve your needs!
+Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/E3YrVtG) will serve your needs!
 
 Oh and by the way, we're now building a whole security tools ecosystem with [Mythril Platform API](https://mythril.ai). You should definitely check that out as well.
 
@@ -33,7 +33,7 @@ See the [Wiki](https://github.com/ConsenSys/mythril/wiki/Installation-and-Setup)
 
 Instructions for using the 'myth' tool are found on the [Wiki](https://github.com/ConsenSys/mythril/wiki). 
 
-For support or general discussions please join the Mythril community on [Discord](https://discord.gg/dFHQGrE).
+For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
 
 ## Presentations, papers and videos
 

mythril/analysis/modules/multiple_sends.py

@@ -1,4 +1,5 @@
 from mythril.analysis.report import Issue
+from mythril.laser.ethereum.cfg import JumpType
 """
 MODULE DESCRIPTION:
 
@@ -21,7 +22,7 @@ def execute(statespace):
             instruction = call.state.get_current_instruction()
             issue = Issue(node.contract_name, node.function_name, instruction['address'],
                           "Multiple Calls",
-                          "Information")
+                          "Informational")
 
             issue.description = \
                 "Multiple sends exist in one transaction, try to isolate each external call into its own transaction." \
@@ -50,7 +51,8 @@ def _explore_states(call, statespace):
 
 def _child_nodes(statespace, node):
     result = []
-    children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid]
+    children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid
+                and edge.type != JumpType.Transaction]
 
     for child in children:
         result.append(child)

mythril/laser/ethereum/evm_exceptions.py

@@ -10,4 +10,5 @@ class StackOverflowException(VmException):
     pass
 
 
-
+class InvalidJumpDestination(VmException):
+    pass

mythril/laser/ethereum/instructions.py

@@ -13,7 +13,7 @@ from mythril.laser.ethereum.state import GlobalState, CalldataType
 import mythril.laser.ethereum.natives as natives
 from mythril.laser.ethereum.transaction import MessageCallTransaction, TransactionStartSignal, \
     ContractCreationTransaction
-from mythril.laser.ethereum.evm_exceptions import VmException, StackUnderflowException
+from mythril.laser.ethereum.evm_exceptions import VmException, StackUnderflowException, InvalidJumpDestination
 from mythril.laser.ethereum.keccak import KeccakFunctionManager
 
 TT256 = 2 ** 256
@@ -22,16 +22,37 @@ TT256M1 = 2 ** 256 - 1
 keccak_function_manager = KeccakFunctionManager()
 
 
-def instruction(func):
-    """ Wrapper that handles copy and original return """
+class StateTransition(object):
+    """Decorator that handles global state copy and original return.
 
-    def wrapper(self, global_state):
-        global_state_copy = copy(global_state)
-        new_global_states = func(self, global_state_copy)
-        for state in new_global_states:
-            state.mstate.pc += 1
-        return new_global_states
-    return wrapper
+    This decorator calls the decorated instruction mutator function on a copy of the state that
+    is passed to it. After the call, the resulting new states' program counter is automatically
+    incremented if `increment_pc=True`.
+    """
+
+    def __init__(self, increment_pc=True):
+        self.increment_pc = increment_pc
+
+    @staticmethod
+    def call_on_state_copy(func, func_obj, state):
+        global_state_copy = copy(state)
+        return func(func_obj, global_state_copy)
+
+    def increment_states_pc(self, states):
+        if self.increment_pc:
+            for state in states:
+                state.mstate.pc += 1
+        return states
+
+    def __call__(self, func):
+        def wrapper(func_obj, global_state):
+            new_global_states = self.call_on_state_copy(
+                func,
+                func_obj,
+                global_state
+            )
+            return self.increment_states_pc(new_global_states)
+        return wrapper
 
 
 class Instruction:
@@ -64,11 +85,11 @@ class Instruction:
 
         return instruction_mutator(global_state)
 
-    @instruction
+    @StateTransition()
     def jumpdest_(self, global_state):
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def push_(self, global_state):
         push_instruction = global_state.get_current_instruction()
         push_value = push_instruction['argument'][2:]
@@ -82,25 +103,25 @@ class Instruction:
         global_state.mstate.stack.append(BitVecVal(int(push_value, 16), 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def dup_(self, global_state):
         value = int(global_state.get_current_instruction()['opcode'][3:], 10)
         global_state.mstate.stack.append(global_state.mstate.stack[-value])
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def swap_(self, global_state):
         depth = int(self.op_code[4:])
         stack = global_state.mstate.stack
         stack[-depth - 1], stack[-1] = stack[-1], stack[-depth - 1]
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def pop_(self, global_state):
         global_state.mstate.stack.pop()
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def and_(self, global_state):
         stack = global_state.mstate.stack
         op1, op2 = stack.pop(), stack.pop()
@@ -113,7 +134,7 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def or_(self, global_state):
         stack = global_state.mstate.stack
         op1, op2 = stack.pop(), stack.pop()
@@ -128,19 +149,19 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def xor_(self, global_state):
         mstate = global_state.mstate
         mstate.stack.append(mstate.stack.pop() ^ mstate.stack.pop())
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def not_(self, global_state: GlobalState):
         mstate = global_state.mstate
         mstate.stack.append(TT256M1 - mstate.stack.pop())
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def byte_(self, global_state):
         mstate = global_state.mstate
         op0, op1 = mstate.stack.pop(), mstate.stack.pop()
@@ -161,25 +182,25 @@ class Instruction:
         return [global_state]
 
     # Arithmetic
-    @instruction
+    @StateTransition()
     def add_(self, global_state):
         global_state.mstate.stack.append(
             (helper.pop_bitvec(global_state.mstate) + helper.pop_bitvec(global_state.mstate)))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def sub_(self, global_state):
         global_state.mstate.stack.append(
             (helper.pop_bitvec(global_state.mstate) - helper.pop_bitvec(global_state.mstate)))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def mul_(self, global_state):
         global_state.mstate.stack.append(
             (helper.pop_bitvec(global_state.mstate) * helper.pop_bitvec(global_state.mstate)))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def div_(self, global_state):
         op0, op1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate)
         if op1 == 0:
@@ -188,7 +209,7 @@ class Instruction:
             global_state.mstate.stack.append(UDiv(op0, op1))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def sdiv_(self, global_state):
         s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate)
         if s1 == 0:
@@ -197,33 +218,33 @@ class Instruction:
             global_state.mstate.stack.append(s0 / s1)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def mod_(self, global_state):
         s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate)
         global_state.mstate.stack.append(0 if s1 == 0 else URem(s0, s1))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def smod_(self, global_state):
         s0, s1 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate)
         global_state.mstate.stack.append(0 if s1 == 0 else SRem(s0, s1))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def addmod_(self, global_state):
         s0, s1, s2 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate), util.pop_bitvec(
             global_state.mstate)
         global_state.mstate.stack.append(URem(URem(s0, s2) + URem(s1, s2), s2))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def mulmod_(self, global_state):
         s0, s1, s2 = util.pop_bitvec(global_state.mstate), util.pop_bitvec(global_state.mstate), util.pop_bitvec(
             global_state.mstate)
         global_state.mstate.stack.append(URem(URem(s0, s2) * URem(s1, s2), s2))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def exp_(self, global_state):
         state = global_state.mstate
 
@@ -235,7 +256,7 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def signextend_(self, global_state):
         state = global_state.mstate
         s0, s1 = state.stack.pop(), state.stack.pop()
@@ -259,28 +280,28 @@ class Instruction:
         return [global_state]
 
     # Comparisons
-    @instruction
+    @StateTransition()
     def lt_(self, global_state):
         state = global_state.mstate
         exp = ULT(util.pop_bitvec(state), util.pop_bitvec(state))
         state.stack.append(exp)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def gt_(self, global_state):
         state = global_state.mstate
         exp = UGT(util.pop_bitvec(state), util.pop_bitvec(state))
         state.stack.append(exp)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def slt_(self, global_state):
         state = global_state.mstate
         exp = util.pop_bitvec(state) < util.pop_bitvec(state)
         state.stack.append(exp)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def sgt_(self, global_state):
         state = global_state.mstate
 
@@ -288,7 +309,7 @@ class Instruction:
         state.stack.append(exp)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def eq_(self, global_state):
         state = global_state.mstate
 
@@ -306,7 +327,7 @@ class Instruction:
         state.stack.append(exp)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def iszero_(self, global_state):
         state = global_state.mstate
 
@@ -317,7 +338,7 @@ class Instruction:
         return [global_state]
 
     # Call data
-    @instruction
+    @StateTransition()
     def callvalue_(self, global_state):
         state = global_state.mstate
         environment = global_state.environment
@@ -325,7 +346,7 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def calldataload_(self, global_state):
         state = global_state.mstate
         environment = global_state.environment
@@ -365,7 +386,7 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def calldatasize_(self, global_state):
         state = global_state.mstate
         environment = global_state.environment
@@ -375,7 +396,7 @@ class Instruction:
             state.stack.append(BitVecVal(len(environment.calldata), 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def calldatacopy_(self, global_state):
         state = global_state.mstate
         environment = global_state.environment
@@ -440,35 +461,35 @@ class Instruction:
         return [global_state]
 
     # Environment
-    @instruction
+    @StateTransition()
     def address_(self, global_state):
         state = global_state.mstate
         environment = global_state.environment
         state.stack.append(environment.address)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def balance_(self, global_state):
         state = global_state.mstate
         address = state.stack.pop()
         state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def origin_(self, global_state):
         state = global_state.mstate
         environment = global_state.environment
         state.stack.append(environment.origin)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def caller_(self, global_state):
         state = global_state.mstate
         environment = global_state.environment
         state.stack.append(environment.sender)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def codesize_(self, global_state):
         state = global_state.mstate
         environment = global_state.environment
@@ -476,7 +497,7 @@ class Instruction:
         state.stack.append(len(disassembly.bytecode) // 2)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def sha3_(self, global_state):
         global keccak_function_manager
 
@@ -513,12 +534,12 @@ class Instruction:
         state.stack.append(BitVecVal(util.concrete_int_from_bytes(keccak, 0), 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def gasprice_(self, global_state):
         global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def codecopy_(self, global_state):
         memory_offset, code_offset, size = global_state.mstate.stack.pop(), global_state.mstate.stack.pop(), global_state.mstate.stack.pop()
 
@@ -567,7 +588,7 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def extcodesize_(self, global_state):
         state = global_state.mstate
         addr = state.stack.pop()
@@ -593,7 +614,7 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def extcodecopy_(self, global_state):
         # FIXME: not implemented
         state = global_state.mstate
@@ -601,45 +622,45 @@ class Instruction:
         start, s2, size = state.stack.pop(), state.stack.pop(), state.stack.pop()
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def returndatasize_(self, global_state):
         global_state.mstate.stack.append(global_state.new_bitvec("returndatasize", 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def blockhash_(self, global_state):
         state = global_state.mstate
         blocknumber = state.stack.pop()
         state.stack.append(global_state.new_bitvec("blockhash_block_" + str(blocknumber), 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def coinbase_(self, global_state):
         global_state.mstate.stack.append(global_state.new_bitvec("coinbase", 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def timestamp_(self, global_state):
         global_state.mstate.stack.append(global_state.new_bitvec("timestamp", 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def number_(self, global_state):
         global_state.mstate.stack.append(global_state.new_bitvec("block_number", 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def difficulty_(self, global_state):
         global_state.mstate.stack.append(global_state.new_bitvec("block_difficulty", 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def gaslimit_(self, global_state):
         global_state.mstate.stack.append(global_state.new_bitvec("block_gaslimit", 256))
         return [global_state]
 
     # Memory operations
-    @instruction
+    @StateTransition()
     def mload_(self, global_state):
         state = global_state.mstate
         op0 = state.stack.pop()
@@ -666,7 +687,7 @@ class Instruction:
         state.stack.append(data)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def mstore_(self, global_state):
         state = global_state.mstate
         op0, value = state.stack.pop(), state.stack.pop()
@@ -701,7 +722,7 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def mstore8_(self, global_state):
         state = global_state.mstate
         op0, value = state.stack.pop(), state.stack.pop()
@@ -717,7 +738,7 @@ class Instruction:
         state.memory[offset] = value % 256
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def sload_(self, global_state):
         global keccak_function_manager
         
@@ -770,6 +791,7 @@ class Instruction:
         global_state.mstate.stack.append(data)
         return [global_state]
 
+
     def _get_constraints(self, keccak_keys, this_key, argument):
         global keccak_function_manager
         for keccak_key in keccak_keys:
@@ -778,7 +800,7 @@ class Instruction:
             keccak_argument = keccak_function_manager.get_argument(keccak_key)
             yield keccak_argument != argument
 
-    @instruction
+    @StateTransition()
     def sstore_(self, global_state):
         global keccak_function_manager
         state = global_state.mstate
@@ -836,28 +858,25 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition(increment_pc=False)
     def jump_(self, global_state):
         state = global_state.mstate
         disassembly = global_state.environment.code
         try:
             jump_addr = util.get_concrete_int(state.stack.pop())
         except AttributeError:
-            logging.debug("Invalid jump argument (symbolic address)")
-            return []
-        except StackUnderflowException:
-            return []
+            raise InvalidJumpDestination("Invalid jump argument (symbolic address)")
+        except IndexError:
+            raise StackUnderflowException()
 
         index = util.get_instruction_index(disassembly.instruction_list, jump_addr)
         if index is None:
-            logging.debug("JUMP to invalid address")
-            return []
+            raise InvalidJumpDestination("JUMP to invalid address")
 
         op_code = disassembly.instruction_list[index]['opcode']
 
         if op_code != "JUMPDEST":
-            logging.debug("Skipping JUMP to invalid destination (not JUMPDEST): " + str(jump_addr))
-            return []
+            raise InvalidJumpDestination("Skipping JUMP to invalid destination (not JUMPDEST): " + str(jump_addr))
 
         new_state = copy(global_state)
         new_state.mstate.pc = index
@@ -865,7 +884,7 @@ class Instruction:
 
         return [new_state]
 
-    @instruction
+    @StateTransition(increment_pc=False)
     def jumpi_(self, global_state):
         state = global_state.mstate
         disassembly = global_state.environment.code
@@ -878,6 +897,7 @@ class Instruction:
             # FIXME: to broad exception handler
         except:
             logging.debug("Skipping JUMPI to invalid destination.")
+            global_state.mstate.pc += 1
             return [global_state]
 
         # False case
@@ -886,6 +906,7 @@ class Instruction:
         if (type(negated) == bool and negated) or (type(negated) == BoolRef and not is_false(negated)):
             new_state = copy(global_state)
             new_state.mstate.depth += 1
+            new_state.mstate.pc += 1
             new_state.mstate.constraints.append(negated)
             states.append(new_state)
         else:
@@ -908,29 +929,27 @@ class Instruction:
                 new_state.mstate.pc = index
                 new_state.mstate.depth += 1
                 new_state.mstate.constraints.append(condi)
-
                 states.append(new_state)
             else:
                 logging.debug("Pruned unreachable states.")
-
         return states
 
-    @instruction
+    @StateTransition()
     def pc_(self, global_state):
         global_state.mstate.stack.append(global_state.mstate.pc - 1)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def msize_(self, global_state):
         global_state.mstate.stack.append(global_state.new_bitvec("msize", 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def gas_(self, global_state):
         global_state.mstate.stack.append(global_state.new_bitvec("gas", 256))
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def log_(self, global_state):
         # TODO: implement me
         state = global_state.mstate
@@ -940,7 +959,7 @@ class Instruction:
         # Not supported
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def create_(self, global_state):
         # TODO: implement me
         state = global_state.mstate
@@ -949,7 +968,7 @@ class Instruction:
         state.stack.append(0)
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def return_(self, global_state):
         state = global_state.mstate
         offset, length = state.stack.pop(), state.stack.pop()
@@ -960,27 +979,42 @@ class Instruction:
             logging.debug("Return with symbolic length or offset. Not supported")
         global_state.current_transaction.end(global_state, return_data)
 
-    @instruction
+    @StateTransition()
     def suicide_(self, global_state):
-        return []
+        target = global_state.mstate.stack.pop()
+
+        # Often the target of the suicide instruction will be symbolic
+        # If it isn't then well transfer the balance to the indicated contract
+        if isinstance(target, BitVecNumRef):
+            target = '0x' + hex(target.as_long())[-40:]
+        if isinstance(target, str):
+            try:
+                global_state.world_state[target].balance += global_state.environment.active_account.balance
+            except KeyError:
+                global_state.world_state.create_account(address=target, balance=global_state.environment.active_account.balance)
+
+        global_state.environment.active_account.balance = 0
+        global_state.environment.active_account.deleted = True
+
+        global_state.current_transaction.end(global_state)
 
-    @instruction
+    @StateTransition()
     def revert_(self, global_state):
         return []
 
-    @instruction
+    @StateTransition()
     def assert_fail_(self, global_state):
         return []
 
-    @instruction
+    @StateTransition()
     def invalid_(self, global_state):
         return []
 
-    @instruction
+    @StateTransition()
     def stop_(self, global_state):
         global_state.current_transaction.end(global_state)
 
-    @instruction
+    @StateTransition()
     def call_(self, global_state):
 
         instr = global_state.get_current_instruction()
@@ -1039,7 +1073,7 @@ class Instruction:
                                              call_data_type=call_data_type)
         raise TransactionStartSignal(transaction, self.op_code)
 
-    @instruction
+    @StateTransition()
     def call_post(self, global_state):
         instr = global_state.get_current_instruction()
 
@@ -1080,7 +1114,7 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def callcode_(self, global_state):
         instr = global_state.get_current_instruction()
         environment = global_state.environment
@@ -1107,7 +1141,7 @@ class Instruction:
                                              )
         raise TransactionStartSignal(transaction, self.op_code)
 
-    @instruction
+    @StateTransition()
     def callcode_post(self, global_state):
         instr = global_state.get_current_instruction()
 
@@ -1149,7 +1183,7 @@ class Instruction:
         return [global_state]
 
 
-    @instruction
+    @StateTransition()
     def delegatecall_(self, global_state):
         instr = global_state.get_current_instruction()
         environment = global_state.environment
@@ -1177,7 +1211,7 @@ class Instruction:
         raise TransactionStartSignal(transaction, self.op_code)
 
 
-    @instruction
+    @StateTransition()
     def delegatecall_post(self, global_state):
         instr = global_state.get_current_instruction()
 
@@ -1221,7 +1255,7 @@ class Instruction:
 
         return [global_state]
 
-    @instruction
+    @StateTransition()
     def staticcall_(self, global_state):
         # TODO: implement me
         instr = global_state.get_current_instruction()

mythril/laser/ethereum/state.py

@@ -1,4 +1,5 @@
 from z3 import BitVec, BitVecVal, Solver, ExprRef, sat
+from mythril.disassembler.disassembly import Disassembly
 from copy import copy, deepcopy
 from enum import Enum
 from random import randint
@@ -61,7 +62,7 @@ class Account:
         :param concrete_storage: Interpret storage as concrete
         """
         self.nonce = 0
-        self.code = code
+        self.code = code or Disassembly("")
         self.balance = balance if balance else BitVec("balance", 256)
         self.storage = Storage(concrete_storage, address=address, dynamic_loader=dynamic_loader)
 
@@ -69,6 +70,8 @@ class Account:
         self.address = address
         self.contract_name = contract_name
 
+        self.deleted = False
+
     def __str__(self):
         return str(self.as_dict)
 

mythril/laser/ethereum/svm.py

@@ -10,6 +10,7 @@ from datetime import datetime, timedelta
 from copy import copy
 from mythril.laser.ethereum.transaction import execute_contract_creation, execute_message_call
 from functools import reduce
+from mythril.laser.ethereum.evm_exceptions import VmException
 
 
 class SVMError(Exception):
@@ -122,6 +123,10 @@ class LaserEVM:
             self._measure_coverage(global_state)
             new_global_states = Instruction(op_code, self.dynamic_loader).evaluate(global_state)
 
+        except VmException as e:
+            logging.debug("Encountered a VmException, ending path: `{}`".format(str(e)))
+            new_global_states = []
+
         except TransactionStartSignal as e:
             # Setup new global state
             new_global_state = e.transaction.initial_global_state()
@@ -219,7 +224,7 @@ class LaserEVM:
                     new_node.flags |= NodeFlags.FUNC_ENTRY
             except StackUnderflowException:
                 new_node.flags |= NodeFlags.FUNC_ENTRY
-        address = state.environment.code.instruction_list[state.mstate.pc - 1]['address']
+        address = state.environment.code.instruction_list[state.mstate.pc]['address']
 
         environment = state.environment
         disassembly = environment.code

mythril/laser/ethereum/transaction/symbolic.py

@@ -1,4 +1,5 @@
 from z3 import BitVec, Extract, Not
+from logging import debug
 
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
@@ -6,13 +7,16 @@ from mythril.laser.ethereum.state import CalldataType
 from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction,\
     get_next_transaction_id
 
-
 def execute_message_call(laser_evm, callee_address):
     """ Executes a message call transaction from all open states """
     open_states = laser_evm.open_states[:]
     del laser_evm.open_states[:]
 
     for open_world_state in open_states:
+        if open_world_state[callee_address].deleted:
+            debug("Can not execute dead contract, skipping.")
+            continue
+
         next_transaction_id = get_next_transaction_id()
         transaction = MessageCallTransaction(
             world_state=open_world_state,

requirements.txt

@@ -8,6 +8,7 @@ eth-keyfile>=0.5.1
 eth-keys>=0.2.0b3
 eth-rlp>=0.1.0
 eth-tester>=0.1.0b21
+eth-typing<2.0.0,>=1.3.0
 eth-utils>=1.0.1
 jinja2>=2.9
 mock

setup.py

@@ -95,6 +95,7 @@ setup(
         'eth-keys>=0.2.0b3',
         'eth-rlp>=0.1.0',
         'eth-tester>=0.1.0b21',
+        'eth-typing>=1.3.0,<2.0.0',
         'coverage',
         'jinja2>=2.9',
         'rlp>=1.0.1',

tests/laser/evm_testsuite/evm_test.py

@@ -52,29 +52,23 @@ def test_vmtest(test_name: str, pre_condition: dict, action: dict, post_conditio
 
     # Act
     laser_evm.time = datetime.now()
-    try:
-        execute_message_call(
-            laser_evm,
-            callee_address=action['address'],
-            caller_address=action['caller'],
-            origin_address=action['origin'],
-            code=action['code'][2:],
-            gas=action['gas'],
-            data=binascii.a2b_hex(action['data'][2:]),
-            gas_price=int(action['gasPrice'], 16),
-            value=int(action['value'], 16)
-        )
-    except VmException as e:
-        if post_condition == {}:
-            return
-        else:
-            raise e
+    execute_message_call(
+        laser_evm,
+        callee_address=action['address'],
+        caller_address=action['caller'],
+        origin_address=action['origin'],
+        code=action['code'][2:],
+        gas=action['gas'],
+        data=binascii.a2b_hex(action['data'][2:]),
+        gas_price=int(action['gasPrice'], 16),
+        value=int(action['value'], 16)
+    )
 
     # Assert
-    if 'Suicide' not in test_name:
+
+    if post_condition != {}:
         assert len(laser_evm.open_states) == 1
     else:
-        assert len(laser_evm.open_states) == 0
         return
 
     world_state = laser_evm.open_states[0]

tests/laser/transaction/symbolic_test.py

@@ -1,7 +1,7 @@
 from mythril.laser.ethereum.transaction.symbolic import execute_message_call, execute_contract_creation
 from mythril.laser.ethereum.transaction import MessageCallTransaction, ContractCreationTransaction
 from mythril.laser.ethereum.svm import LaserEVM
-from mythril.laser.ethereum.state import WorldState
+from mythril.laser.ethereum.state import WorldState, Account
 import unittest.mock as mock
 from unittest.mock import MagicMock
 
@@ -20,7 +20,7 @@ def test_execute_message_call(mocked_setup: MagicMock):
     laser_evm = LaserEVM({})
 
     world_state = WorldState()
-    world_state.accounts["address"] = "something"
+    world_state.accounts["address"] = Account("address")
 
     laser_evm.open_states = [world_state]
     laser_evm.exec = MagicMock()