From 44d25e48e761a5b63cec2c6bb82a87ca9c1fe724 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Tue, 17 Jul 2018 15:22:20 +0200
Subject: [PATCH 01/21] Check for length bin runtime

---
 mythril/laser/ethereum/state.py | 60 ++++++++++++++++++++++++++++++++-
 mythril/laser/ethereum/svm.py   |  9 ++---
 2 files changed, 64 insertions(+), 5 deletions(-)

diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py
index 932eae65..19394ffa 100644
--- a/mythril/laser/ethereum/state.py
+++ b/mythril/laser/ethereum/state.py
@@ -1,12 +1,13 @@
 from z3 import BitVec, BitVecVal
 from copy import copy, deepcopy
 from enum import Enum
-
+from random import random
 
 class CalldataType(Enum):
     CONCRETE = 1
     SYMBOLIC = 2
 
+
 class Account:
     """
     Account class representing ethereum accounts
@@ -31,6 +32,12 @@ class Account:
     def __str__(self):
         return str(self.as_dict)
 
+    def set_balance(self, balance):
+        self.balance = balance
+
+    def add_balance(self, balance):
+        self.balance += balance
+
     def get_storage(self, index):
         return self.storage[index] if index in self.storage.keys() else BitVec("storage_" + str(index), 256)
 
@@ -149,3 +156,54 @@ class GlobalState:
         """ Gets the current instruction for this GlobalState"""
         instructions = self.environment.code.instruction_list
         return instructions[self.mstate.pc]
+
+
+class WorldState:
+    """
+    The WorldState class represents the world state as described in the yellowpaper
+    """
+    def __init__(self):
+        """
+        Constructor for the world state. Initializes the accounts record
+        """
+        self.accounts = {}
+
+    def __getitem__(self, item):
+        """
+        Gets an account from the worldstate using item as key
+        :param item: Address of the account to get
+        :return: Account associated with the address
+        """
+        return self.accounts[item]
+
+    def create_account(self, balance=0):
+        """
+        Create non-contract account
+        :param balance: Initial balance for the account
+        :return: The new account
+        """
+        new_account = Account(self._generate_new_address(), balance=balance)
+        self._put_account(new_account)
+        return new_account
+
+    def create_initialized_contract_account(self, contract_code, storage):
+        """
+        Creates a new contract account, based on the contract code and storage provided
+        The contract code only includes the runtime contract bytecode
+        :param contract_code: Runtime bytecode for the contract
+        :param storage: Initial storage for the contract
+        :return: The new account
+        """
+        new_account = Account(self._generate_new_address(), code=contract_code, balance=0)
+        new_account.storage = storage
+        self._put_account(new_account)
+
+    def _generate_new_address(self):
+        """ Generates a new address for the global state"""
+        while True:
+            address = '0x' + ''.join([str(hex(random(0, 16)))[-1] for _ in range(20)])
+            if address not in self.accounts.keys():
+                return address
+
+    def _put_account(self, account):
+        self.accounts[account.address] = account
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index c7dc2927..6177c4ad 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -1,6 +1,6 @@
 from z3 import BitVec
 import logging
-from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account
+from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState
 from mythril.laser.ethereum.instructions import Instruction
 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
 from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
@@ -25,7 +25,8 @@ class LaserEVM:
     """
     def __init__(self, accounts, dynamic_loader=None, max_depth=22):
         self.instructions_covered = []
-        self.accounts = accounts
+        self.world_state = WorldState()
+        self.world_state.accounts = accounts
 
         self.nodes = {}
         self.edges = []
@@ -47,7 +48,7 @@ class LaserEVM:
 
         # Initialize the execution environment
         environment = Environment(
-            self.accounts[main_address],
+            self.world_state[main_address],
             BitVec("caller", 256),
             [],
             BitVec("gasprice", 256),
@@ -61,7 +62,7 @@ class LaserEVM:
         initial_node = Node(environment.active_account.contract_name)
         self.nodes[initial_node.uid] = initial_node
 
-        global_state = GlobalState(self.accounts, environment, initial_node)
+        global_state = GlobalState(self.world_state, environment, initial_node)
         initial_node.states.append(global_state)
 
         # Empty the work_list before starting an execution

From 105053365f644bd94f24f6ff1efd8e7cda96710e Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 19 Jul 2018 15:01:24 +0200
Subject: [PATCH 02/21] Adds Transaction JumpType

---
 mythril/laser/ethereum/cfg.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/mythril/laser/ethereum/cfg.py b/mythril/laser/ethereum/cfg.py
index f462f5cf..a8a4fe82 100644
--- a/mythril/laser/ethereum/cfg.py
+++ b/mythril/laser/ethereum/cfg.py
@@ -8,6 +8,7 @@ class JumpType(Enum):
     UNCONDITIONAL = 2
     CALL = 3
     RETURN = 4
+    Transaction = 5
 
 
 class NodeFlags(Flags):

From cb74e187a428bb116504fb5789a1c02f6151cae6 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 19 Jul 2018 15:02:05 +0200
Subject: [PATCH 03/21] Add node reference to world state, this will in the
 future be used to link multiple transactions

---
 mythril/laser/ethereum/state.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py
index 19394ffa..b29a0680 100644
--- a/mythril/laser/ethereum/state.py
+++ b/mythril/laser/ethereum/state.py
@@ -160,13 +160,14 @@ class GlobalState:
 
 class WorldState:
     """
-    The WorldState class represents the world state as described in the yellowpaper
+    The WorldState class represents the world state as described in the yellow paper
     """
     def __init__(self):
         """
         Constructor for the world state. Initializes the accounts record
         """
         self.accounts = {}
+        self.node = None
 
     def __getitem__(self, item):
         """

From f31343096ffa4196438aebdfcc09dcd1fe20746a Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 19 Jul 2018 15:02:41 +0200
Subject: [PATCH 04/21] Initial CallTransactionImplementation

---
 mythril/laser/ethereum/transaction.py | 44 +++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 mythril/laser/ethereum/transaction.py

diff --git a/mythril/laser/ethereum/transaction.py b/mythril/laser/ethereum/transaction.py
new file mode 100644
index 00000000..28f0f852
--- /dev/null
+++ b/mythril/laser/ethereum/transaction.py
@@ -0,0 +1,44 @@
+import logging
+from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType
+from mythril.laser.ethereum.cfg import Node, Edge, JumpType
+from z3 import BitVec
+
+
+class CallTransaction:
+    def __init__(self, callee_address):
+        self.callee_address = callee_address
+        self.caller = BitVec("caller", 256)
+        self.gas_price = BitVec("gasprice", 256)
+        self.call_value = BitVec("callvalue", 256)
+        self.origin = BitVec("origin", 256)
+        pass
+
+    def run(self, open_world_states, evm):
+        for open_world_state in open_world_states:
+
+            # Initialize the execution environment
+            environment = Environment(
+                open_world_state[self.callee_address],
+                self.caller,
+                [],
+                self.gas_price,
+                self.call_value,
+                self.origin,
+                calldata_type=CalldataType.SYMBOLIC,
+            )
+
+            new_node = Node(environment.active_account.contract_name)
+            evm.instructions_covered = [False for _ in environment.code.instruction_list]
+
+            evm.nodes[new_node.uid] = new_node
+            if open_world_state.node:
+                evm.edges.append(Edge(open_world_state.node.uid, new_node.uid, edge_type=JumpType.Transaction, condition=None))
+
+            global_state = GlobalState(open_world_state, environment, new_node)
+            new_node.states.append(global_state)
+
+            evm.work_list.append(global_state)
+
+        evm.exec()
+        logging.info("Execution complete")
+        logging.info("Achieved {0:.3g}% coverage".format(evm.coverage))

From 55be6a88834e23b9bb5de19fcd6a023262b48159 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 19 Jul 2018 15:03:28 +0200
Subject: [PATCH 05/21] Use CallTransaction versus constructing environments in
 LaserEVM

---
 mythril/laser/ethereum/svm.py | 30 ++++--------------------------
 1 file changed, 4 insertions(+), 26 deletions(-)

diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 6177c4ad..83dd6d3e 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -1,6 +1,7 @@
 from z3 import BitVec
 import logging
 from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState
+from mythril.laser.ethereum.transaction import CallTransaction
 from mythril.laser.ethereum.instructions import Instruction
 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
 from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
@@ -45,35 +46,12 @@ class LaserEVM:
 
     def sym_exec(self, main_address):
         logging.debug("Starting LASER execution")
+        transaction = CallTransaction(main_address)
+        transaction.run([self.world_state], self)
 
-        # Initialize the execution environment
-        environment = Environment(
-            self.world_state[main_address],
-            BitVec("caller", 256),
-            [],
-            BitVec("gasprice", 256),
-            BitVec("callvalue", 256),
-            BitVec("origin", 256),
-            calldata_type=CalldataType.SYMBOLIC,
-        )
-
-        self.instructions_covered = [False for _ in environment.code.instruction_list]
-
-        initial_node = Node(environment.active_account.contract_name)
-        self.nodes[initial_node.uid] = initial_node
-
-        global_state = GlobalState(self.world_state, environment, initial_node)
-        initial_node.states.append(global_state)
-
-        # Empty the work_list before starting an execution
-        self.work_list.append(global_state)
-        self._sym_exec()
-
-        logging.info("Execution complete")
-        logging.info("Achieved {0:.3g}% coverage".format(self.coverage))
         logging.info("%d nodes, %d edges, %d total states", len(self.nodes), len(self.edges), self.total_states)
 
-    def _sym_exec(self):
+    def exec(self):
         for global_state in self.strategy:
             try:
                 new_states, op_code = self.execute_state(global_state)

From 4fccaeefd67c3c736861870a8fe711a934c96e6d Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 19 Jul 2018 15:25:21 +0200
Subject: [PATCH 06/21] Add some documentation

---
 mythril/laser/ethereum/transaction.py | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/mythril/laser/ethereum/transaction.py b/mythril/laser/ethereum/transaction.py
index 28f0f852..9249d515 100644
--- a/mythril/laser/ethereum/transaction.py
+++ b/mythril/laser/ethereum/transaction.py
@@ -5,7 +5,12 @@ from z3 import BitVec
 
 
 class CallTransaction:
+    """ Represents a call value transaction """
     def __init__(self, callee_address):
+        """
+        Constructor for Call transaction, sets up all symbolic parameters
+        :param callee_address: Address of the contract that will be called
+        """
         self.callee_address = callee_address
         self.caller = BitVec("caller", 256)
         self.gas_price = BitVec("gasprice", 256)
@@ -14,6 +19,7 @@ class CallTransaction:
         pass
 
     def run(self, open_world_states, evm):
+        """ Runs this transaction on the evm starting from the open world states"""
         for open_world_state in open_world_states:
 
             # Initialize the execution environment

From de949dc7e7936fc32c792c00ccbeac08f32cd9f1 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Thu, 19 Jul 2018 15:25:21 +0200
Subject: [PATCH 07/21] adds space

---
 mythril/laser/ethereum/transaction.py | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/mythril/laser/ethereum/transaction.py b/mythril/laser/ethereum/transaction.py
index 28f0f852..e28f91c0 100644
--- a/mythril/laser/ethereum/transaction.py
+++ b/mythril/laser/ethereum/transaction.py
@@ -5,7 +5,12 @@ from z3 import BitVec
 
 
 class CallTransaction:
+    """ Represents a call value transaction """
     def __init__(self, callee_address):
+        """
+        Constructor for Call transaction, sets up all symbolic parameters
+        :param callee_address: Address of the contract that will be called
+        """
         self.callee_address = callee_address
         self.caller = BitVec("caller", 256)
         self.gas_price = BitVec("gasprice", 256)
@@ -14,6 +19,7 @@ class CallTransaction:
         pass
 
     def run(self, open_world_states, evm):
+        """ Runs this transaction on the evm starting from the open world states """
         for open_world_state in open_world_states:
 
             # Initialize the execution environment

From fdfbc0cc6cf5ca7013471b1c75a23e9ee1cc411d Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sat, 21 Jul 2018 14:47:18 +0200
Subject: [PATCH 08/21] Support multiple transactions

---
 mythril/laser/ethereum/svm.py         | 15 ++++++++++++---
 mythril/laser/ethereum/transaction.py | 15 ++++++++++++---
 2 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 83dd6d3e..a9e65759 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -26,8 +26,10 @@ class LaserEVM:
     """
     def __init__(self, accounts, dynamic_loader=None, max_depth=22):
         self.instructions_covered = []
-        self.world_state = WorldState()
-        self.world_state.accounts = accounts
+
+        world_state = WorldState()
+        world_state.accounts = accounts
+        self.open_states = [world_state]
 
         self.nodes = {}
         self.edges = []
@@ -47,7 +49,7 @@ class LaserEVM:
     def sym_exec(self, main_address):
         logging.debug("Starting LASER execution")
         transaction = CallTransaction(main_address)
-        transaction.run([self.world_state], self)
+        transaction.run(self.open_states, self)
 
         logging.info("%d nodes, %d edges, %d total states", len(self.nodes), len(self.edges), self.total_states)
 
@@ -59,6 +61,13 @@ class LaserEVM:
                 logging.debug("Encountered unimplemented instruction")
                 continue
 
+            if len(new_states) == 0:
+                # TODO: let global state use worldstate
+                open_world_state = WorldState()
+                open_world_state.accounts = global_state.accounts
+                open_world_state.node = global_state.node
+                self.open_states.append(open_world_state)
+
             self.manage_cfg(op_code, new_states)
 
             self.work_list += new_states
diff --git a/mythril/laser/ethereum/transaction.py b/mythril/laser/ethereum/transaction.py
index e28f91c0..ffaa6b76 100644
--- a/mythril/laser/ethereum/transaction.py
+++ b/mythril/laser/ethereum/transaction.py
@@ -16,11 +16,20 @@ class CallTransaction:
         self.gas_price = BitVec("gasprice", 256)
         self.call_value = BitVec("callvalue", 256)
         self.origin = BitVec("origin", 256)
-        pass
 
-    def run(self, open_world_states, evm):
+        self.open_states = None
+
+    @property
+    def has_ran(self):
+        return self.open_states is None
+
+    def run(self, open_world_states: list, evm):
         """ Runs this transaction on the evm starting from the open world states """
-        for open_world_state in open_world_states:
+        # Consume the open states
+        open_states = open_world_states[:]
+        del open_world_states[:]
+
+        for open_world_state in open_states:
 
             # Initialize the execution environment
             environment = Environment(

From 23bf26299bcffb8b38bfe2961ba5aac0185a2b97 Mon Sep 17 00:00:00 2001
From: Bernhard Mueller <bernhard.mueller11@gmail.com>
Date: Sat, 21 Jul 2018 22:02:40 +0200
Subject: [PATCH 09/21] Formatting, remove unused imports & function

---
 mythril/disassembler/disassembly.py |  4 ++--
 mythril/ether/ethcontract.py        | 13 -------------
 mythril/leveldb/client.py           | 11 ++++++-----
 3 files changed, 8 insertions(+), 20 deletions(-)

diff --git a/mythril/disassembler/disassembly.py b/mythril/disassembler/disassembly.py
index a20d4ffe..9f8aff89 100644
--- a/mythril/disassembler/disassembly.py
+++ b/mythril/disassembler/disassembly.py
@@ -1,4 +1,4 @@
-from mythril.ether import asm,util
+from mythril.ether import asm, util
 from mythril.support.signatures import SignatureDb
 import logging
 
@@ -38,7 +38,7 @@ class Disassembly(object):
                 func_name = "_function_" + func_hash
 
             try:
-                offset = self.instruction_list[i+2]['argument']
+                offset = self.instruction_list[i + 2]['argument']
                 jump_target = int(offset, 16)
 
                 self.func_to_addr[func_name] = jump_target
diff --git a/mythril/ether/ethcontract.py b/mythril/ether/ethcontract.py
index 197376b0..7c012f25 100644
--- a/mythril/ether/ethcontract.py
+++ b/mythril/ether/ethcontract.py
@@ -70,16 +70,3 @@ class ETHContract(persistent.Persistent):
                 continue
 
         return eval(str_eval.strip())
-
-
-class InstanceList(persistent.Persistent):
-
-    def __init__(self):
-        self.addresses = []
-        self.balances = []
-        pass
-
-    def add(self, address, balance=0):
-        self.addresses.append(address)
-        self.balances.append(balance)
-        self._p_changed = True
diff --git a/mythril/leveldb/client.py b/mythril/leveldb/client.py
index 5f1e4221..bbed33a4 100644
--- a/mythril/leveldb/client.py
+++ b/mythril/leveldb/client.py
@@ -1,13 +1,11 @@
-import plyvel
 import binascii
 import rlp
-import hashlib
 import logging
 from ethereum import utils
 from ethereum.block import BlockHeader, Block
-from mythril.leveldb.state import State, Account
+from mythril.leveldb.state import State
 from mythril.leveldb.eth_db import ETH_DB
-from mythril.ether.ethcontract import ETHContract, InstanceList
+from mythril.ether.ethcontract import ETHContract
 
 # Per https://github.com/ethereum/go-ethereum/blob/master/core/database_util.go
 # prefixes and suffixes for keys in geth
@@ -16,7 +14,8 @@ bodyPrefix = b'b'       # bodyPrefix + num (uint64 big endian) + hash -> block b
 numSuffix = b'n'        # headerPrefix + num (uint64 big endian) + numSuffix -> hash
 blockHashPrefix = b'H'  # blockHashPrefix + hash -> num (uint64 big endian)
 # known geth keys
-headHeaderKey = b'LastBlock' # head (latest) header hash
+headHeaderKey = b'LastBlock'  # head (latest) header hash
+
 
 def _formatBlockNumber(number):
     '''
@@ -24,12 +23,14 @@ def _formatBlockNumber(number):
     '''
     return utils.zpad(utils.int_to_big_endian(number), 8)
 
+
 def _encode_hex(v):
     '''
     encodes hash as hex
     '''
     return '0x' + utils.encode_hex(v)
 
+
 class EthLevelDB(object):
     '''
     Go-Ethereum LevelDB client class

From 3e868427b25db2d267a7f2777bb24ece3536f68c Mon Sep 17 00:00:00 2001
From: Ubuntu <ubuntu@ip-10-0-150-254.ec2.internal>
Date: Sat, 21 Jul 2018 20:36:14 +0000
Subject: [PATCH 10/21] Optimize search

---
 mythril/disassembler/disassembly.py | 3 ++-
 mythril/ether/ethcontract.py        | 9 ++++++---
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/mythril/disassembler/disassembly.py b/mythril/disassembler/disassembly.py
index 9f8aff89..2f7aec4c 100644
--- a/mythril/disassembler/disassembly.py
+++ b/mythril/disassembler/disassembly.py
@@ -7,7 +7,7 @@ class Disassembly(object):
 
     def __init__(self, code):
         self.instruction_list = asm.disassemble(util.safe_decode(code))
-        self.xrefs = []
+        self.func_hashes = []
         self.func_to_addr = {}
         self.addr_to_func = {}
         self.bytecode = code
@@ -24,6 +24,7 @@ class Disassembly(object):
 
         for i in jmptable_indices:
             func_hash = self.instruction_list[i]['argument']
+            self.func_hashes.append(func_hash)
             try:
                 # tries local cache, file and optional online lookup
                 # may return more than one function signature. since we cannot probe for the correct one we'll use the first
diff --git a/mythril/ether/ethcontract.py b/mythril/ether/ethcontract.py
index 7c012f25..8e19c746 100644
--- a/mythril/ether/ethcontract.py
+++ b/mythril/ether/ethcontract.py
@@ -31,12 +31,12 @@ class ETHContract(persistent.Persistent):
 
     def get_easm(self):
 
-        return Disassembly(self.code).get_easm()
+        return self.disassembly.get_easm()
 
     def matches_expression(self, expression):
 
-        easm_code = self.get_easm()
         str_eval = ''
+        easm_code = None
 
         matches = re.findall(r'func#([a-zA-Z0-9\s_,(\\)\[\]]+)#', expression)
 
@@ -58,6 +58,9 @@ class ETHContract(persistent.Persistent):
             m = re.match(r'^code#([a-zA-Z0-9\s,\[\]]+)#', token)
 
             if (m):
+                if easm_code is None:
+                    easm_code = self.get_easm()
+
                 code = m.group(1).replace(",", "\\n")
                 str_eval += "\"" + code + "\" in easm_code"
                 continue
@@ -65,7 +68,7 @@ class ETHContract(persistent.Persistent):
             m = re.match(r'^func#([a-fA-F0-9]+)#$', token)
 
             if (m):
-                str_eval += "\"" + m.group(1) + "\" in easm_code"
+                str_eval += "\"" + m.group(1) + "\" in self.disassembly.func_hashes"
 
                 continue
 

From 5955abc1e12c1cf39b9fcfd305f9b10c62769ca0 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sun, 22 Jul 2018 14:37:06 +0200
Subject: [PATCH 11/21] Rename to message call and fix comparison

---
 mythril/laser/ethereum/svm.py         | 5 +++--
 mythril/laser/ethereum/transaction.py | 5 +++--
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index a9e65759..62f790f1 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -1,7 +1,7 @@
 from z3 import BitVec
 import logging
 from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState
-from mythril.laser.ethereum.transaction import CallTransaction
+from mythril.laser.ethereum.transaction import MessageCall
 from mythril.laser.ethereum.instructions import Instruction
 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
 from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
@@ -48,7 +48,8 @@ class LaserEVM:
 
     def sym_exec(self, main_address):
         logging.debug("Starting LASER execution")
-        transaction = CallTransaction(main_address)
+
+        transaction = MessageCall(main_address)
         transaction.run(self.open_states, self)
 
         logging.info("%d nodes, %d edges, %d total states", len(self.nodes), len(self.edges), self.total_states)
diff --git a/mythril/laser/ethereum/transaction.py b/mythril/laser/ethereum/transaction.py
index ffaa6b76..66028ec1 100644
--- a/mythril/laser/ethereum/transaction.py
+++ b/mythril/laser/ethereum/transaction.py
@@ -4,7 +4,8 @@ from mythril.laser.ethereum.cfg import Node, Edge, JumpType
 from z3 import BitVec
 
 
-class CallTransaction:
+class MessageCall:
+
     """ Represents a call value transaction """
     def __init__(self, callee_address):
         """
@@ -21,7 +22,7 @@ class CallTransaction:
 
     @property
     def has_ran(self):
-        return self.open_states is None
+        return self.open_states is not None
 
     def run(self, open_world_states: list, evm):
         """ Runs this transaction on the evm starting from the open world states """

From d9de7114dd352d23e2c9c400c5ea961048f12d9b Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sun, 22 Jul 2018 14:39:21 +0200
Subject: [PATCH 12/21] Store world state

---
 mythril/laser/ethereum/svm.py | 2 ++
 tests/svm_test.py             | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 62f790f1..47d95bf2 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -29,6 +29,8 @@ class LaserEVM:
 
         world_state = WorldState()
         world_state.accounts = accounts
+        # this sets the initial world state
+        self.world_state = world_state
         self.open_states = [world_state]
 
         self.nodes = {}
diff --git a/tests/svm_test.py b/tests/svm_test.py
index 4742b89e..b79edd2d 100644
--- a/tests/svm_test.py
+++ b/tests/svm_test.py
@@ -18,7 +18,7 @@ class LaserEncoder(json.JSONEncoder):
 
 def _all_info(laser):
     accounts = {}
-    for address, _account in laser.accounts.items():
+    for address, _account in laser.world_state.accounts.items():
         account = _account.as_dict
         account["code"] = account["code"].instruction_list
         account['balance'] = str(account['balance'])

From 0fdc27339b79dc9a9ba7a944e66d7d4e102865ff Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <tommycjniko@gmail.com>
Date: Sun, 22 Jul 2018 18:17:13 +0530
Subject: [PATCH 13/21] mythril/analysis/modules/ether_send.py

---
 mythril/analysis/modules/ether_send.py | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/mythril/analysis/modules/ether_send.py b/mythril/analysis/modules/ether_send.py
index d6bf850c..b7a4dce0 100644
--- a/mythril/analysis/modules/ether_send.py
+++ b/mythril/analysis/modules/ether_send.py
@@ -27,15 +27,14 @@ def execute(statespace):
         state = call.state
         address = state.get_current_instruction()['address']
 
-        if ("callvalue" in str(call.value)):
+        if "callvalue" in str(call.value):
             logging.debug("[ETHER_SEND] Skipping refund function")
             continue
 
         # We're only interested in calls that send Ether
 
-        if call.value.type == VarType.CONCRETE:
-            if call.value.val == 0:
-                continue
+        if call.value.type == VarType.CONCRETE and call.value.val == 0:
+            continue
 
         interesting = False
 
@@ -52,14 +51,14 @@ def execute(statespace):
         else:
             m = re.search(r'storage_([a-z0-9_&^]+)', str(call.to))
 
-            if (m):
+            if m:
                 idx = m.group(1)
 
                 description += "a non-zero amount of Ether is sent to an address taken from storage slot " + str(idx) + ".\n"
 
                 func = statespace.find_storage_write(state.environment.active_account.address, idx)
 
-                if (func):
+                if func:
                     description += "There is a check on storage index " + str(idx) + ". This storage slot can be written to by calling the function `" + func + "`.\n"
                     interesting = True
                 else:
@@ -74,7 +73,7 @@ def execute(statespace):
 
             index = 0
 
-            while(can_solve and index < len(node.constraints)):
+            while can_solve and index < len(node.constraints):
 
                 constraint = node.constraints[index]
                 index += 1
@@ -82,14 +81,14 @@ def execute(statespace):
 
                 m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint))
 
-                if (m):
+                if m:
 
                     constrained = True
                     idx = m.group(1)
 
                     func = statespace.find_storage_write(state.environment.active_account.address, idx)
 
-                    if (func):
+                    if func:
                         description += "\nThere is a check on storage index " + str(idx) + ". This storage slot can be written to by calling the function `" + func + "`."
                     else:
                         logging.debug("[ETHER_SEND] No storage writes to index " + str(idx))
@@ -98,7 +97,7 @@ def execute(statespace):
 
                 # CALLER may also be constrained to hardcoded address. I.e. 'caller' and some integer
 
-                elif (re.search(r"caller", str(constraint)) and re.search(r'[0-9]{20}', str(constraint))):
+                elif re.search(r"caller", str(constraint)) and re.search(r'[0-9]{20}', str(constraint)):
                     constrained = True
                     can_solve = False
                     break
@@ -116,7 +115,8 @@ def execute(statespace):
 
                     debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model)
 
-                    issue = Issue(call.node.contract_name, call.node.function_name, address, "Ether send", "Warning", description, debug)
+                    issue = Issue(call.node.contract_name, call.node.function_name, address, "Ether send", "Warning",
+                                  description, debug)
                     issues.append(issue)
 
                 except UnsatError:

From 71d48dd7585508b23ce2c650e7123741294c5371 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Sun, 22 Jul 2018 14:54:33 +0200
Subject: [PATCH 14/21] Use correct variable

---
 mythril/laser/ethereum/transaction.py | 2 +-
 tests/native_test.py                  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/mythril/laser/ethereum/transaction.py b/mythril/laser/ethereum/transaction.py
index 66028ec1..a1416b5e 100644
--- a/mythril/laser/ethereum/transaction.py
+++ b/mythril/laser/ethereum/transaction.py
@@ -50,7 +50,7 @@ class MessageCall:
             if open_world_state.node:
                 evm.edges.append(Edge(open_world_state.node.uid, new_node.uid, edge_type=JumpType.Transaction, condition=None))
 
-            global_state = GlobalState(open_world_state, environment, new_node)
+            global_state = GlobalState(open_world_state.accounts, environment, new_node)
             new_node.states.append(global_state)
 
             evm.work_list.append(global_state)
diff --git a/tests/native_test.py b/tests/native_test.py
index 8deb4d39..374c8cbf 100644
--- a/tests/native_test.py
+++ b/tests/native_test.py
@@ -47,7 +47,7 @@ IDENTITY_TEST[3] = (83269476937987, False)
 
 def _all_info(laser):
     accounts = {}
-    for address, _account in laser.accounts.items():
+    for address, _account in laser.world_state.accounts.items():
         account = _account.as_dict
         account["code"] = account["code"].instruction_list
         account['balance'] = str(account['balance'])

From c1db9485047441321334760603743c61ff7fc1f3 Mon Sep 17 00:00:00 2001
From: "Dr. Sergey Pogodin" <dr.pogodin@gmail.com>
Date: Sun, 22 Jul 2018 15:00:50 +0200
Subject: [PATCH 15/21] Adds sonar-scanner to the build flow

---
 .circleci/config.yml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 13e9d790..0a295470 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -57,6 +57,10 @@ jobs:
           command: python3 setup.py install
           working_directory: /home/mythril
 
+      - run:
+          name: Sonar analysis
+          command: if [ -z "CIRCLE_PR_NUMBER" ]; then sonar-scanner -Dsonar.projectKey=$SONAR_PROJECT_KEY -Dsonar.organization=$SONAR_ORGANIZATION -Dsonar.sources=/home/mythril -Dsonar.host.url=$SONAR_HOST_URL -Dsonar.login=$(SONAR_LOGIN); fi
+
       - run:
           name: Integration tests
           command: if [ -z "$CIRCLE_PR_NUMBER" ]; then ./run-integration-tests.sh; fi

From 9485ee458798703409126a150f4d66410dee008e Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Mon, 23 Jul 2018 18:38:49 +0200
Subject: [PATCH 16/21] save

---
 mythril/analysis/modules/exceptions.py | 2 --
 mythril/analysis/modules/integer.py    | 4 +++-
 mythril/analysis/solver.py             | 4 ++--
 mythril/laser/ethereum/instructions.py | 7 +++----
 mythril/laser/ethereum/state.py        | 7 ++++++-
 mythril/laser/ethereum/svm.py          | 2 +-
 6 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/mythril/analysis/modules/exceptions.py b/mythril/analysis/modules/exceptions.py
index 507bbd49..fc287948 100644
--- a/mythril/analysis/modules/exceptions.py
+++ b/mythril/analysis/modules/exceptions.py
@@ -24,9 +24,7 @@ def execute(statespace):
         for state in node.states:
 
             instruction = state.get_current_instruction()
-
             if(instruction['opcode'] == "ASSERT_FAIL"):
-
                 try:
                     model = solver.get_model(node.constraints)
                     address = state.get_current_instruction()['address']
diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py
index e21dbb58..25282e2c 100644
--- a/mythril/analysis/modules/integer.py
+++ b/mythril/analysis/modules/integer.py
@@ -30,6 +30,7 @@ def execute(statespace):
         node = statespace.nodes[k]
 
         for state in node.states:
+            # pass
             issues += _check_integer_underflow(statespace, state, node)
             issues += _check_integer_overflow(statespace, state, node)
 
@@ -50,6 +51,8 @@ def _check_integer_overflow(statespace, state, node):
     instruction = state.get_current_instruction()
     if instruction['opcode'] not in ("ADD", "MUL"):
         return issues
+    if instruction['address'] != 755:
+        return issues
 
     # Formulate overflow constraints
     stack = state.mstate.stack
@@ -108,7 +111,6 @@ def _verify_integer_overflow(statespace, node, expr, state, model, constraint, o
 
     return _try_constraints(node.constraints, [Not(constraint)]) is not None
 
-
 def _try_constraints(constraints, new_constraints):
     """
     Tries new constraints
diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 0f6703e6..01633956 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -4,7 +4,7 @@ import logging
 
 def get_model(constraints):
     s = Solver()
-    s.set("timeout", 10000)
+    s.set("timeout", 100000)
 
     for constraint in constraints:
         s.add(constraint)
@@ -12,7 +12,7 @@ def get_model(constraints):
     if result == sat:
         return s.model()
     elif result == unknown:
-        logging.info("Timeout encountered while solving expression using z3")
+        logging.error("Timeout encountered while solving expression using z3")
     raise UnsatError
 
 
diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 2db3adf7..c97a5ebd 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -778,7 +778,7 @@ class Instruction:
                 new_state = copy(global_state)
                 new_state.mstate.pc = index
                 new_state.mstate.depth += 1
-                new_state.mstate.constraints.append(condi)
+                new_state.mstate.constraints.append(simplify(condi))
 
                 states.append(new_state)
             else:
@@ -786,12 +786,11 @@ class Instruction:
 
         # False case
         negated = Not(condition) if type(condition) == BoolRef else condition == 0
-        sat = not is_false(simplify(negated)) if type(condi) == BoolRef else not negated
 
-        if sat:
+        if (type(negated) == bool and negated) or (type(negated) == BoolRef and not is_false(simplify(negated))):
             new_state = copy(global_state)
             new_state.mstate.depth += 1
-            new_state.mstate.constraints.append(negated)
+            new_state.mstate.constraints.append(simplify(negated))
             states.append(new_state)
         else:
             logging.debug("Pruned unreachable states.")
diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py
index 7cb865b6..07951f6a 100644
--- a/mythril/laser/ethereum/state.py
+++ b/mythril/laser/ethereum/state.py
@@ -39,7 +39,12 @@ class Account:
         self.balance += balance
 
     def get_storage(self, index):
-        return self.storage[index] if index in self.storage.keys() else BitVec("storage_" + str(index), 256)
+        if index in self.storage.keys():
+            return self.storage[index]
+        else:
+            symbol = BitVec("storage_" + str(index), 256)
+            self.storage[index] = symbol
+            return symbol
 
     @property
     def as_dict(self):
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 1f54e6f2..98a0ba9d 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -70,7 +70,7 @@ class LaserEVM:
             try:
                 new_states, op_code = self.execute_state(global_state)
             except NotImplementedError:
-                logging.debug("Encountered unimplemented instruction")
+                logging.error("Encountered unimplemented instruction: {}".format(op_code))
                 continue
 
             if len(new_states) == 0:

From 2c052cb40e4fcb6b24c6481c9f3bd6a4b003d56c Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Tue, 24 Jul 2018 13:25:05 +0200
Subject: [PATCH 17/21] Clean up integer

---
 mythril/analysis/modules/integer.py | 2 --
 1 file changed, 2 deletions(-)

diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py
index 25282e2c..1c990e60 100644
--- a/mythril/analysis/modules/integer.py
+++ b/mythril/analysis/modules/integer.py
@@ -51,8 +51,6 @@ def _check_integer_overflow(statespace, state, node):
     instruction = state.get_current_instruction()
     if instruction['opcode'] not in ("ADD", "MUL"):
         return issues
-    if instruction['address'] != 755:
-        return issues
 
     # Formulate overflow constraints
     stack = state.mstate.stack

From 7c839b9825fa8cd22ce56b9be7329ba60e52bd8c Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Tue, 24 Jul 2018 13:25:38 +0200
Subject: [PATCH 18/21] Check on active account vs environment (which is
 shallow copied)

---
 mythril/laser/ethereum/taint_analysis.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mythril/laser/ethereum/taint_analysis.py b/mythril/laser/ethereum/taint_analysis.py
index bd53b08c..37f546a0 100644
--- a/mythril/laser/ethereum/taint_analysis.py
+++ b/mythril/laser/ethereum/taint_analysis.py
@@ -118,7 +118,7 @@ class TaintRunner:
         direct_children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid]
         children = []
         for child in direct_children:
-            if child.states[0].environment == environment:
+            if child.states[0].environment.active_account == environment.active_account:
                 children.append(child)
             else:
                 children += TaintRunner.children(child, statespace, environment)

From b7c67962d8bb12983a5f3361fab17719363e02d7 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Wed, 25 Jul 2018 13:48:35 +0200
Subject: [PATCH 19/21] And use address for comparison in taint analysis

---
 mythril/laser/ethereum/state.py          | 18 ++++++++++--------
 mythril/laser/ethereum/taint_analysis.py |  2 +-
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py
index 07951f6a..032cf66e 100644
--- a/mythril/laser/ethereum/state.py
+++ b/mythril/laser/ethereum/state.py
@@ -38,13 +38,14 @@ class Account:
     def add_balance(self, balance):
         self.balance += balance
 
-    def get_storage(self, index):
-        if index in self.storage.keys():
-            return self.storage[index]
-        else:
-            symbol = BitVec("storage_" + str(index), 256)
-            self.storage[index] = symbol
-            return symbol
+    # def get_storage(self, index):
+    #     return BitVec("storage_" + str(index), 256)
+    #     if index in self.storage.keys():
+    #         return self.storage[index]
+    #     else:
+    #         symbol = BitVec("storage_" + str(index), 256)
+    #         self.storage[index] = symbol
+    #         return symbol
 
     @property
     def as_dict(self):
@@ -83,6 +84,7 @@ class Environment:
     def __str__(self):
         return str(self.as_dict)
 
+
     @property
     def as_dict(self):
         return dict(active_account=self.active_account, sender=self.sender, calldata=self.calldata,
@@ -150,7 +152,7 @@ class GlobalState:
 
 
     def __copy__(self):
-        accounts = self.accounts
+        accounts = copy(self.accounts)
         environment = copy(self.environment)
         mstate = deepcopy(self.mstate)
         call_stack = copy(self.call_stack)
diff --git a/mythril/laser/ethereum/taint_analysis.py b/mythril/laser/ethereum/taint_analysis.py
index 37f546a0..441d9e23 100644
--- a/mythril/laser/ethereum/taint_analysis.py
+++ b/mythril/laser/ethereum/taint_analysis.py
@@ -118,7 +118,7 @@ class TaintRunner:
         direct_children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid]
         children = []
         for child in direct_children:
-            if child.states[0].environment.active_account == environment.active_account:
+            if child.states[0].environment.active_account.address == environment.active_account.address:
                 children.append(child)
             else:
                 children += TaintRunner.children(child, statespace, environment)

From ab4c49e78c70b10ce363e17c29d18436e0e50b78 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Wed, 25 Jul 2018 13:51:01 +0200
Subject: [PATCH 20/21] Do account copy

---
 mythril/laser/ethereum/instructions.py | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index c97a5ebd..ae7ef8fe 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -707,13 +707,8 @@ class Instruction:
             index = str(index)
 
         try:
-            # Create a fresh copy of the account object before modifying storage
-
-            for k in global_state.accounts:
-                if global_state.accounts[k] == global_state.environment.active_account:
-                    global_state.accounts[k] = deepcopy(global_state.accounts[k])
-                    global_state.environment.active_account = global_state.accounts[k]
-                    break
+            global_state.environment.active_account = deepcopy(global_state.environment.active_account)
+            global_state.accounts[global_state.environment.active_account.address] = global_state.environment.active_account
 
             global_state.environment.active_account.storage[index] = value
         except KeyError:

From e0e92630b9dd6d6b46df112733ade7fd23ef2c00 Mon Sep 17 00:00:00 2001
From: Joran Honig <joran.honig@gmail.com>
Date: Wed, 25 Jul 2018 13:58:05 +0200
Subject: [PATCH 21/21] cleanup

---
 mythril/analysis/modules/integer.py | 1 -
 mythril/analysis/solver.py          | 2 +-
 mythril/laser/ethereum/svm.py       | 2 +-
 3 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/mythril/analysis/modules/integer.py b/mythril/analysis/modules/integer.py
index 1c990e60..f89c0781 100644
--- a/mythril/analysis/modules/integer.py
+++ b/mythril/analysis/modules/integer.py
@@ -30,7 +30,6 @@ def execute(statespace):
         node = statespace.nodes[k]
 
         for state in node.states:
-            # pass
             issues += _check_integer_underflow(statespace, state, node)
             issues += _check_integer_overflow(statespace, state, node)
 
diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 01633956..9c5a2dd0 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -12,7 +12,7 @@ def get_model(constraints):
     if result == sat:
         return s.model()
     elif result == unknown:
-        logging.error("Timeout encountered while solving expression using z3")
+        logging.info("Timeout encountered while solving expression using z3")
     raise UnsatError
 
 
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index 98a0ba9d..61899681 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -70,7 +70,7 @@ class LaserEVM:
             try:
                 new_states, op_code = self.execute_state(global_state)
             except NotImplementedError:
-                logging.error("Encountered unimplemented instruction: {}".format(op_code))
+                logging.info("Encountered unimplemented instruction: {}".format(op_code))
                 continue
 
             if len(new_states) == 0: