Symbolic tests rf (#1431)

* Add assertions to auto test gen

* Add symbolic tests

* Make calldata symbolic

* EVM: Support exp aka pow (#1361)

* EVM: Add support for EXP with concrete/solvable exponent

Adds support for EXP aka POW, with concrete or solvable exponent, fixing #1005 effectively.

Not sure if we can do it any better - it seems z3 doesn't have exp/pow for bitvectors.

* Update operators.py

* Update evm.py

* Use concretized_args

* Move Operators.POW to EVM._exp

* Extend travis wait for output to 30m

* Extend travis build to 60m...

* Fix Operators.ITE -> Operators.ITEBV

* Split ethereum travis job to two jobs

* EVM.EXP: concretize base=SAMPLED

* Fix concrete tests: use to_constant

* Fix set storage in concrete tests

* Split ethereum_vm tests into concrete and symbolic

* Fix travis tests

* Split symbolic tests into two jobs

* Split VMTests even more

* More tests split

* [WIP][WIP][WIP] Moving executor functionality to ManticoreBase and refactor concurrency shared data

* Workspace locks

* Concurrency flavor configurable from commandline

* Asserts and refactorrrrrrrs

* Remove unused callback

* Some CC

* Some CC

* Some CC

* Fix solver vs Z3Solver

* Make solver a singleton based on tid/pid. REfactor m._save. Fix some tests

* typo and evm bugfix

* Fix some tests referecing global solver

* Fix concolic tests and more global solver refs

* Fix tests

* CC fixes

* Fix tests. Fix testcase id generation

* Move profiling to a plugin and fix tests

* Add solver intance ref to mem test

* Fix mem workspace tests

* Fix output checking tests

* Fix z3solver ref

* Relax verbosity/log tests

* Moved Workers to its own file

* Relax output tests

* Relax output tests

* Fix profiling test

* Fix more tests

* Default multiprocessing

* Try to clean mcore __del__

* Change Worker life span

* Fix Single mode

* CC

* revert verbosity travis

* CC and solver ref fix

* Relax ouput checking tests and some bugfixes

* running -> ready

* Fixing teeests

* add weak cache to _load

* del debug prints

* Adding config.py support for Enums

* Try/Remove generate_testcase event as it never occurs online. Fix tests

* Fix CC

* Kill the cache when start/stop run. Remove debugprints. clean tests

* Fix travis test _other_

* Fix native tests and timeout

* Fix state.must_be_true

* fix CC

* Changing fstat tets...:
~'

* LLLLLLLLinux tests

* Skip unicorn concrete test for now

* Try fix CodeClimate

* Try fix CodeClimate

* Update evm examples to newest solidity

* Complete transformation of consts.mprocessing to enum

* Add blank line (codeclimate)

* Using the enum instead of the string

* Using the enum instead of the string

* Merge and fix

* CC and debug print

* Move fee consumption to checkpoint so it is not done twice. Fix frontier test generator

* Fix Job Count (and force travis rebuild)

```
0.02s$ ./cc-test-reporter sum-coverage --output - --parts $JOB_COUNT coverage/codeclimate.*.json | ./cc-test-reporter upload-coverage --input -
Error: expected 3 parts, received 4 parts
```

* Add tx number to testcase log

* Del test verbosity

.travis.yml

@@ -14,11 +14,12 @@ stages:
 env:
   global:
     - CC_TEST_REPORTER_ID=db72f1ed59628c16eb0c00cbcd629c4c71f68aa1892ef42d18c7c2b8326f460a
-    - JOB_COUNT=3 # Three jobs generate test coverage: ethereum, native, and other
+    - JOB_COUNT=4 # Three jobs generate test coverage: ethereum, ethereum_vm, native, and other
     - PYTHONWARNINGS="default::ResourceWarning" # Enable ResourceWarnings
   matrix:
     - TEST_TYPE=examples
     - TEST_TYPE=ethereum
+    - TEST_TYPE=ethereum_vm
     - TEST_TYPE=native
     - TEST_TYPE=other
 
@@ -52,7 +53,7 @@ install:
   - scripts/travis_install.sh $TEST_TYPE
 
 script:
-  - scripts/travis_test.sh $TEST_TYPE
+  - travis_wait 60 scripts/travis_test.sh $TEST_TYPE
 
 after_success:
   - ./cc-test-reporter format-coverage -t coverage.py -o "coverage/codeclimate.$TEST_TYPE.json"

manticore/core/smtlib/visitors.py

@@ -476,6 +476,11 @@ def visit_BitVecSub(self, expression, *operands):
                 return left.operands[1]
             elif self._same_constant(left.operands[1], right):
                 return left.operands[0]
+        elif isinstance(left, BitVecSub) and isinstance(right, Constant):
+            subleft = left.operands[0]
+            subright = left.operands[1]
+            if isinstance(subright, Constant):
+                return BitVecSub(subleft, BitVecConstant(subleft.size, subright.value + right.value, taint=subright.taint | right.taint))
 
     def visit_BitVecOr(self, expression, *operands):
         """ a | 0 => a

manticore/ethereum/manticore.py

@@ -1022,7 +1022,6 @@ def multi_tx_analysis(self, solidity_filename, working_dir=None, contract_name=N
         if contract_account is None:
             logger.info("Failed to create contract: exception in constructor")
             return
-
         prev_coverage = 0
         current_coverage = 0
         tx_no = 0
@@ -1323,13 +1322,14 @@ def generate_testcase(self, state, message='', only_if=None, name='user'):
                 else:
                     return False
 
+        blockchain = state.platform
+
         # FIXME. workspace should not be responsible for formating the output
         # each object knows its secrets, and each class should be able to report
         # its final state
-        testcase = super().generate_testcase(state, message, name=name)
+        testcase = super().generate_testcase(state, message + f'({len(blockchain.human_transactions)} txs)', name=name)
         # TODO(mark): Refactor ManticoreOutput to let the platform be more in control
         #  so this function can be fully ported to EVMWorld.generate_workspace_files.
-        blockchain = state.platform
 
         local_findings = set()
         for detector in self.detectors.values():

manticore/platforms/evm.py

@@ -37,7 +37,7 @@
 # ignore: Ignore gas. Do not account for it. Do not OOG.
 consts = config.get_group('evm')
 
-consts.add('oog', default='concrete', description=(
+consts.add('oog', default='pedantic', description=(
     'Default behavior for symbolic gas.'
     'pedantic: Fully faithful. Test at every instruction. Forks.'
     'complete: Mostly faithful. Test at BB limit. Forks.'
@@ -436,10 +436,18 @@ def wrapper(*args, **kwargs):
                 if policy == "ACCOUNTS":
                     value = args[index]
                     world = args[0].world
-                    #special handler for EVM only policy
+                    # special handler for EVM only policy
                     cond = world._constraint_to_accounts(value, ty='both', include_zero=True)
                     world.constraints.add(cond)
                     policy = 'ALL'
+
+                if args[index].taint:
+                    # TODO / FIXME: The taint should persist!
+                    logger.warning(
+                        f"Concretizing {func.__name__}'s {index} argument and dropping its taints: "
+                        "the value might not be tracked properly (in case of using detectors)"
+                    )
+                logger.info(f"Concretizing instruction argument {arg} by {policy}")
                 raise ConcretizeArgument(index, policy=policy)
             return func(*args, **kwargs)
         wrapper.__signature__ = inspect.signature(func)
@@ -779,7 +787,7 @@ def _top(self, n=0):
 
     def _pop(self):
         """Pop a value from the stack"""
-        if len(self.stack) == 0:
+        if not self.stack:
             raise StackUnderflow()
         return self.stack.pop()
 
@@ -791,7 +799,6 @@ def _consume(self, fee):
         elif isinstance(fee, BitVec):
             if fee.size != 512:
                 raise ValueError("Fees should be 512 bit long")
-
         # This configuration variable allows the user to control and perhaps relax the gas calculation
         # pedantic: gas is faithfully accounted and checked at instruction level. State may get forked in OOG/NoOOG
         # complete: gas is faithfully accounted and checked at basic blocks limits. State may get forked in OOG/NoOOG
@@ -800,6 +807,19 @@ def _consume(self, fee):
         # pesimistic: OOG soon. If it may NOT be enough gas we ignore the normal case. A constraint is added to assert the gas is NOT enough and the other state is ignored.
         # ignore: Ignore gas. Do not account for it. Do not OOG.
 
+        # optimization that speed up concrete fees sometimes
+        if not issymbolic(fee) and issymbolic(self._gas):
+            reps, m = getattr(self, '_mgas', (0, None))
+            reps += 1
+            if m is None and reps > 10:
+                m = Z3Solver.instance().min(self.constraints, self._gas)
+            self._mgas = reps, m
+
+            if m is not None and fee < m:
+                self._gas -= fee
+                self._mgas = reps, m - fee
+                return
+
         if consts.oog in ('pedantic', 'complete'):
             # gas is faithfully accounted and ogg checked at instruction/BB level.
             if consts.oog == 'pedantic' or self.instruction.is_terminator:
@@ -837,7 +857,7 @@ def _consume(self, fee):
             # Try not to OOG. If it may be enough gas we ignore the OOG case.
             # A constraint is added to assert the gas is enough and the OOG state is ignored.
             # explore only when there is enough gas if possible
-            if Z3Solver().can_be_true(self.constraints, Operators.UGT(self.gas, fee)):
+            if Z3Solver.instance().can_be_true(self.constraints, Operators.UGT(self.gas, fee)):
                 self.constraints.add(Operators.UGT(self.gas, fee))
             else:
                 logger.debug(f"Not enough gas for instruction {self.instruction.name} at 0x{self.pc:x}")
@@ -846,15 +866,15 @@ def _consume(self, fee):
             # OOG soon. If it may NOT be enough gas we ignore the normal case.
             # A constraint is added to assert the gas is NOT enough and the other state is ignored.
             # explore only when there is enough gas if possible
-            if Z3Solver().can_be_true(self.constraints, Operators.ULE(self.gas, fee)):
+            if Z3Solver.instance().can_be_true(self.constraints, Operators.ULE(self.gas, fee)):
                 self.constraints.add(Operators.ULE(self.gas, fee))
                 raise NotEnoughGas()
         else:
             if consts.oog != 'ignore':
                 raise Exception("Wrong oog config variable")
             # do nothing. gas is not even changed
             return
-        self._gas -= fee
+        self._gas = simplify(self._gas - fee)
 
         # If everything is concrete lets just check at every instruction
         if not issymbolic(self._gas) and self._gas < 0:
@@ -872,9 +892,9 @@ def _pop_arguments(self):
         for _ in range(current.pops):
             arguments.append(self._pop())
         # simplify stack arguments
-        for i in range(len(arguments)):
-            if isinstance(arguments[i], Constant) and not arguments[i].taint:
-                arguments[i] = arguments[i].value
+        for i, arg in enumerate(arguments):
+            if isinstance(arg, Constant) and not arg.taint:
+                arguments[i] = arg.value
         return arguments
 
     def _top_arguments(self):
@@ -937,7 +957,10 @@ def _checkpoint(self):
             # this could raise an insufficient stack exception
             arguments = self._pop_arguments()
             fee = self._calculate_gas(*arguments)
+
             self._checkpoint_data = (pc, old_gas, instruction, arguments, fee, allocated)
+            self._consume(fee)
+
         return self._checkpoint_data
 
     def _rollback(self):
@@ -1030,21 +1053,21 @@ def setstate(state, value):
                              policy='ALL')
         #print (self)
         try:
+            #import time
             #limbo = 0.0
             #a = time.time()
             self._check_jmpdest()
             #b = time.time()
             last_pc, last_gas, instruction, arguments, fee, allocated = self._checkpoint()
             #c = time.time()
-            self._consume(fee)
             #d = time.time()
             result = self._handler(*arguments)
             #e = time.time()
             self._advance(result)
             #f = time.time()
             #if hasattr(self, 'F'):
             #    limbo = (a-self.F)*100
-            #print("%02.2f %02.2f %02.2f %02.2f %02.2f %02.2f"%((b-a)*100, (c-b)*100, (d-c)*100, (e-d)*100, (f-e)*100, limbo))
+            #print(f"{instruction}\t\t %02.4f %02.4f %02.4f %02.4f %02.4f %02.4f"%((b-a)*100, (c-b)*100, (d-c)*100, (e-d)*100, (f-e)*100, limbo))
             #self.F = time.time()
 
         except ConcretizeGas as ex:
@@ -1224,12 +1247,22 @@ def nbytes(e):
             return result
         return EXP_SUPPLEMENTAL_GAS * nbytes(exponent)
 
+    @concretized_args(base='SAMPLED', exponent='SAMPLED')
     def EXP(self, base, exponent):
         """
-            Exponential operation
-            The zero-th power of zero 0^0 is defined to be one
+        Exponential operation
+        The zero-th power of zero 0^0 is defined to be one.
+
+        :param base: exponential base, concretized with sampled values
+        :param exponent: exponent value, concretized with sampled values
+        :return: BitVec* EXP result
         """
-        # fixme integer bitvec
+        if exponent == 0:
+            return 1
+
+        if base == 0:
+            return 0
+
         return pow(base, exponent, TT256)
 
     def SIGNEXTEND(self, size, value):
@@ -1299,8 +1332,8 @@ def try_simplify_to_constant(self, data):
             if isinstance(simplified, Constant):
                 concrete_data.append(simplified.value)
             else:
-                #simplify by solving. probably means that we need to improve simplification
-                solutions = Z3Solver().get_all_values(self.constraints, simplified, 2, silent=True)
+                # simplify by solving. probably means that we need to improve simplification
+                solutions = Z3Solver.instance().get_all_values(self.constraints, simplified, 2, silent=True)
                 if len(solutions) != 1:
                     break
                 concrete_data.append(solutions[0])
@@ -1405,7 +1438,6 @@ def CALLDATACOPY_gas(self, mem_offset, data_offset, size):
 
     def CALLDATACOPY(self, mem_offset, data_offset, size):
         """Copy input data in current environment to memory"""
-
         if issymbolic(size):
             if Z3Solver().can_be_true(self._constraints, size <= len(self.data) + 32):
                 self.constraints.add(size <= len(self.data) + 32)

scripts/compare_traces.py

@@ -0,0 +1,51 @@
+import sys
+
+import os
+
+
+def compare_traces(dir1: str, dir2: str):
+    """
+    Compare state traces from two mcore_* directories.
+
+    For now assumes to use `test_xxxxxxx.trace` only.
+    """
+    get_traces = lambda dir: [f for f in os.listdir(dir) if f.startswith('test_') and f.endswith('.trace')]
+
+    traces1 = get_traces(dir1)
+    traces2 = get_traces(dir2)
+
+    traces1.sort()
+    traces2.sort()
+
+    print("### Comparing traces: ")
+    print(f"dir1 - {dir1} :")
+    print(', '.join(traces1))
+    print()
+    print(f"dir2 - {dir2} :")
+    print(', '.join(traces2))
+
+    for t1, t2 in zip(traces1, traces2):
+        path1 = os.path.join(dir1, t1)
+        path2 = os.path.join(dir2, t2)
+
+        with open(path1) as fp1, open(path2) as fp2:
+            if fp1.read() != fp2.read():
+                print(f'Files {t1} and {t2} differs.')
+            else:
+                print(f'Files {t1} and {t2} matches.')
+
+
+if __name__ == '__main__':
+    if len(sys.argv) != 3:
+        print(f'Usage: {sys.argv[0]} MCORE_DIR_1 MCORE_DIR_2')
+        sys.exit()
+
+    dir1, dir2 = sys.argv[1:]
+
+    not_dir = lambda d: not os.path.isdir(d)
+
+    if not_dir(dir1) or not_dir(dir2):
+        print('One of passed args is not a directory!')
+        sys.exit(-1)
+
+    compare_traces(dir1, dir2)

scripts/travis_test.sh

@@ -93,8 +93,9 @@ run_examples() {
 
 # Test type
 case $1 in
-    native)     ;&  # Fallthrough
-    ethereum)   ;&  # Fallthrough
+    native)                 ;&  # Fallthrough
+    ethereum)               ;&  # Fallthrough
+    ethereum_vm)       ;&  # Fallthrough
     other)
         echo "Running only the tests from 'tests/$1' directory"
         run_tests_from_dir $1
@@ -106,22 +107,24 @@ case $1 in
         ;;
 
     all)
-        echo "Running all tests registered in travis_test.sh: examples, native, ethereum, other";
+        echo "Running all tests registered in travis_test.sh: examples, native, ethereum, ethereum_vm, other";
 
         # Functions should return 0 on success and 1 on failure
         RV=0
         run_tests_from_dir native
         RV=$(($RV + $?))
         run_tests_from_dir ethereum
         RV=$(($RV + $?))
+	run_tests_from_dir ethereum_vm
+        RV=$(($RV + $?))
         run_tests_from_dir other
         RV=$(($RV + $?))
         run_examples
         RV=$(($RV + $?))
         ;;
 
     *)
-        echo "Usage: $0 [examples|native|ethereum|other|all]"
+        echo "Usage: $0 [examples|native|ethereum|ethereum_vm|other|all]"
         exit 3;
         ;;
 esac

tests/ethereum_vm/VMTests_concrete/__init__.py

@@ -0,0 +1 @@
+# DO NOT DELETE

tests/ethereum_vm/VMTests_concrete/test_vmTests.py

@@ -0,0 +1,145 @@
+"""DO NOT MODIFY: Tests generated from `VMTests/vmTests` with make_VMTests.py"""
+import unittest
+from binascii import unhexlify
+
+import rlp
+import sha3
+from rlp.sedes import (
+    CountableList,
+    BigEndianInt,
+    Binary,
+)
+
+from manticore.core.smtlib import ConstraintSet, Z3Solver  # Ignore unused import in non-symbolic tests!
+from manticore.core.smtlib.visitors import to_constant
+from manticore.platforms import evm
+from manticore.utils import config
+from manticore.core.state import Concretize
+
+
+
+class Log(rlp.Serializable):
+    fields = [
+        ('address', Binary.fixed_length(20, allow_empty=True)),
+        ('topics', CountableList(BigEndianInt(32))),
+        ('data', Binary())
+    ]
+
+
+class EVMTest_vmTests(unittest.TestCase):
+    # https://nose.readthedocs.io/en/latest/doc_tests/test_multiprocess/multiprocess.html#controlling-distribution
+    _multiprocess_can_split_ = True
+    # https://docs.python.org/3.7/library/unittest.html#unittest.TestCase.maxDiff
+    maxDiff = None
+
+    SAVED_DEFAULT_FORK = evm.DEFAULT_FORK
+
+    @classmethod
+    def setUpClass(cls):
+        consts = config.get_group('evm')
+        consts.oog = 'pedantic'
+        evm.DEFAULT_FORK = 'frontier'
+
+    @classmethod
+    def tearDownClass(cls):
+        evm.DEFAULT_FORK = cls.SAVED_DEFAULT_FORK
+
+    def _test_run(self, world):
+        result = None
+        returndata = b''
+        try:
+            while True:
+                try:
+                    world.current_vm.execute()
+                except Concretize as e:
+                    value = self._solve(world.constraints, e.expression)
+                    class fake_state:pass
+                    fake_state = fake_state()
+                    fake_state.platform = world
+                    e.setstate(fake_state, value)
+        except evm.EndTx as e:
+            result = e.result
+            if result in ('RETURN', 'REVERT'):
+                returndata = self._solve(world.constraints, e.data)
+        except evm.StartTx as e:
+            self.fail('This tests should not initiate an internal tx (no CALLs allowed)')
+        return result, returndata
+
+    def _solve(self, constraints, val):
+        results = Z3Solver.instance().get_all_values(constraints, val, maxcnt=3)
+        # We constrain all values to single values!
+        self.assertEqual(len(results), 1)
+        return results[0]
+
+
+    def test_suicide(self):
+        """
+        Testcase taken from https://github.com/ethereum/tests
+        File: suicide.json
+        sha256sum: 1aa0a61de3c9576faf6ac4f002626210a5315d3132d032162b2934d304a60c1f
+        Code:     CALLER
+                  SELFDESTRUCT
+        """    
+
+        def solve(val):
+            """
+            Those tests are **auto-generated** and `solve` is used in symbolic tests.
+            So yes, this returns just val; it makes it easier to generate tests like this.
+            """
+            return to_constant(val)
+
+        constraints = ConstraintSet()
+
+        blocknumber = 0
+        timestamp = 1
+        difficulty = 256
+        coinbase = 244687034288125203496486448490407391986876152250
+        gaslimit = 1000000
+        world = evm.EVMWorld(constraints, blocknumber=blocknumber, timestamp=timestamp, difficulty=difficulty,
+                             coinbase=coinbase, gaslimit=gaslimit)
+
+        acc_addr = 0xf572e5295c57f15886f9b263e2f6d2d6c7b5ec6
+        acc_code = unhexlify('33ff')
+        acc_balance = 100000000000000000000000
+        acc_nonce = 0
+
+        world.create_account(address=acc_addr, balance=acc_balance, code=acc_code, nonce=acc_nonce)
+
+        address = 0xf572e5295c57f15886f9b263e2f6d2d6c7b5ec6
+        caller = 0xcd1722f3947def4cf144679da39c4c32bdc35681
+        price = 0x5af3107a4000
+        value = 1000000000000000000
+        gas = 100000
+        data = ''
+        # open a fake tx, no funds send
+        world._open_transaction('CALL', address, price, data, caller, value, gas=gas)
+
+        # This variable might seem redundant in some tests - don't forget it is auto generated
+        # and there are cases in which we need it ;)
+        result, returndata = self._test_run(world)
+
+        # World sanity checks - those should not change, right?
+        self.assertEqual(solve(world.block_number()), 0)
+        self.assertEqual(solve(world.block_gaslimit()), 1000000)
+        self.assertEqual(solve(world.block_timestamp()), 1)
+        self.assertEqual(solve(world.block_difficulty()), 256)
+        self.assertEqual(solve(world.block_coinbase()), 0x2adc25665018aa1fe0e6bc666dac8fc2697ff9ba)
+
+        # Add post checks for account 0xcd1722f3947def4cf144679da39c4c32bdc35681
+        # check nonce, balance, code
+        self.assertEqual(solve(world.get_nonce(0xcd1722f3947def4cf144679da39c4c32bdc35681)), 0)
+        self.assertEqual(solve(world.get_balance(0xcd1722f3947def4cf144679da39c4c32bdc35681)), 100000000000000000000000)
+        self.assertEqual(world.get_code(0xcd1722f3947def4cf144679da39c4c32bdc35681), unhexlify(''))
+        # check outs
+        self.assertEqual(returndata, unhexlify(''))
+        # check logs
+        logs = [Log(unhexlify('{:040x}'.format(l.address)), l.topics, solve(l.memlog)) for l in world.logs]
+        data = rlp.encode(logs)
+        self.assertEqual(sha3.keccak_256(data).hexdigest(), '1dcc4de8dec75d7aab85b567b6ccd41ad312451b948a7413f0a142fd40d49347')
+
+        # test used gas
+        self.assertEqual(solve(world.current_vm.gas), 99998)
+
+
+if __name__ == '__main__':
+    unittest.main()

tests/ethereum_vm/VMTests_symbolic/__init__.py

@@ -0,0 +1 @@
+# DO NOT DELETE

tests/ethereum_vm/VMTests_symbolic/test_vmTests.py

@@ -0,0 +1,161 @@
+"""DO NOT MODIFY: Tests generated from `VMTests/vmTests` with make_VMTests.py"""
+import unittest
+from binascii import unhexlify
+
+import rlp
+import sha3
+from rlp.sedes import (
+    CountableList,
+    BigEndianInt,
+    Binary,
+)
+
+from manticore.core.smtlib import ConstraintSet, Z3Solver  # Ignore unused import in non-symbolic tests!
+from manticore.core.smtlib.visitors import to_constant
+from manticore.platforms import evm
+from manticore.utils import config
+from manticore.core.state import Concretize
+
+
+
+class Log(rlp.Serializable):
+    fields = [
+        ('address', Binary.fixed_length(20, allow_empty=True)),
+        ('topics', CountableList(BigEndianInt(32))),
+        ('data', Binary())
+    ]
+
+
+class EVMTest_vmTests(unittest.TestCase):
+    # https://nose.readthedocs.io/en/latest/doc_tests/test_multiprocess/multiprocess.html#controlling-distribution
+    _multiprocess_can_split_ = True
+    # https://docs.python.org/3.7/library/unittest.html#unittest.TestCase.maxDiff
+    maxDiff = None
+
+    SAVED_DEFAULT_FORK = evm.DEFAULT_FORK
+
+    @classmethod
+    def setUpClass(cls):
+        consts = config.get_group('evm')
+        consts.oog = 'pedantic'
+        evm.DEFAULT_FORK = 'frontier'
+
+    @classmethod
+    def tearDownClass(cls):
+        evm.DEFAULT_FORK = cls.SAVED_DEFAULT_FORK
+
+    def _test_run(self, world):
+        result = None
+        returndata = b''
+        try:
+            while True:
+                try:
+                    world.current_vm.execute()
+                except Concretize as e:
+                    value = self._solve(world.constraints, e.expression)
+                    class fake_state:pass
+                    fake_state = fake_state()
+                    fake_state.platform = world
+                    e.setstate(fake_state, value)
+        except evm.EndTx as e:
+            result = e.result
+            if result in ('RETURN', 'REVERT'):
+                returndata = self._solve(world.constraints, e.data)
+        except evm.StartTx as e:
+            self.fail('This tests should not initiate an internal tx (no CALLs allowed)')
+        return result, returndata
+
+    def _solve(self, constraints, val):
+        results = Z3Solver.instance().get_all_values(constraints, val, maxcnt=3)
+        # We constrain all values to single values!
+        self.assertEqual(len(results), 1)
+        return results[0]
+
+
+    def test_suicide(self):
+        """
+        Testcase taken from https://github.com/ethereum/tests
+        File: suicide.json
+        sha256sum: 1aa0a61de3c9576faf6ac4f002626210a5315d3132d032162b2934d304a60c1f
+        Code:     CALLER
+                  SELFDESTRUCT
+        """    
+
+        def solve(val):
+            return self._solve(constraints, val)
+
+        constraints = ConstraintSet()
+
+        blocknumber = constraints.new_bitvec(256, name='blocknumber')
+        constraints.add(blocknumber == 0)
+
+        timestamp = constraints.new_bitvec(256, name='timestamp')
+        constraints.add(timestamp == 1)
+
+        difficulty = constraints.new_bitvec(256, name='difficulty')
+        constraints.add(difficulty == 256)
+
+        coinbase = constraints.new_bitvec(256, name='coinbase')
+        constraints.add(coinbase == 244687034288125203496486448490407391986876152250)
+
+        gaslimit = constraints.new_bitvec(256, name='gaslimit')
+        constraints.add(gaslimit == 1000000)
+
+        world = evm.EVMWorld(constraints, blocknumber=blocknumber, timestamp=timestamp, difficulty=difficulty,
+                             coinbase=coinbase, gaslimit=gaslimit)
+
+        acc_addr = 0xf572e5295c57f15886f9b263e2f6d2d6c7b5ec6
+        acc_code = unhexlify('33ff')
+
+        acc_balance = constraints.new_bitvec(256, name='balance_0xf572e5295c57f15886f9b263e2f6d2d6c7b5ec6')
+        constraints.add(acc_balance == 100000000000000000000000)
+
+        acc_nonce = constraints.new_bitvec(256, name='nonce_0xf572e5295c57f15886f9b263e2f6d2d6c7b5ec6')
+        constraints.add(acc_nonce == 0)
+
+        world.create_account(address=acc_addr, balance=acc_balance, code=acc_code, nonce=acc_nonce)
+
+        address = 0xf572e5295c57f15886f9b263e2f6d2d6c7b5ec6
+        caller = 0xcd1722f3947def4cf144679da39c4c32bdc35681
+        price = constraints.new_bitvec(256, name='price')
+        constraints.add(price == 100000000000000)
+
+        value = constraints.new_bitvec(256, name='value')
+        constraints.add(value == 1000000000000000000)
+
+        gas = constraints.new_bitvec(256, name='gas')
+        constraints.add(gas == 100000)
+
+        data = ''
+        # open a fake tx, no funds send
+        world._open_transaction('CALL', address, price, data, caller, value, gas=gas)
+
+        # This variable might seem redundant in some tests - don't forget it is auto generated
+        # and there are cases in which we need it ;)
+        result, returndata = self._test_run(world)
+
+        # World sanity checks - those should not change, right?
+        self.assertEqual(solve(world.block_number()), 0)
+        self.assertEqual(solve(world.block_gaslimit()), 1000000)
+        self.assertEqual(solve(world.block_timestamp()), 1)
+        self.assertEqual(solve(world.block_difficulty()), 256)
+        self.assertEqual(solve(world.block_coinbase()), 0x2adc25665018aa1fe0e6bc666dac8fc2697ff9ba)
+
+        # Add post checks for account 0xcd1722f3947def4cf144679da39c4c32bdc35681
+        # check nonce, balance, code
+        self.assertEqual(solve(world.get_nonce(0xcd1722f3947def4cf144679da39c4c32bdc35681)), 0)
+        self.assertEqual(solve(world.get_balance(0xcd1722f3947def4cf144679da39c4c32bdc35681)), 100000000000000000000000)
+        self.assertEqual(world.get_code(0xcd1722f3947def4cf144679da39c4c32bdc35681), unhexlify(''))
+        # check outs
+        self.assertEqual(returndata, unhexlify(''))
+        # check logs
+        logs = [Log(unhexlify('{:040x}'.format(l.address)), l.topics, solve(l.memlog)) for l in world.logs]
+        data = rlp.encode(logs)
+        self.assertEqual(sha3.keccak_256(data).hexdigest(), '1dcc4de8dec75d7aab85b567b6ccd41ad312451b948a7413f0a142fd40d49347')
+
+        # test used gas
+        self.assertEqual(solve(world.current_vm.gas), 99998)
+
+
+if __name__ == '__main__':
+    unittest.main()