From 074d5a74be2c022d3c2bf419e729621d2696eb1b Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Mon, 22 Jul 2019 09:33:52 -0700
Subject: [PATCH 01/30] WIP uselsess commit

---
 mythril/analysis/modules/ether_thief.py        | 12 +++++++++---
 .../analysis/templates/report_as_text.jinja2   |  2 ++
 mythril/laser/ethereum/call.py                 | 18 ++++++++++++++++--
 mythril/laser/ethereum/instructions.py         | 17 ++++++++++++++---
 mythril/laser/ethereum/state/account.py        |  2 ++
 mythril/laser/ethereum/state/world_state.py    |  5 ++++-
 .../ethereum/transaction/transaction_models.py |  5 +++--
 7 files changed, 50 insertions(+), 11 deletions(-)

diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py
index 76952a54..b5dc8c02 100644
--- a/mythril/analysis/modules/ether_thief.py
+++ b/mythril/analysis/modules/ether_thief.py
@@ -114,15 +114,21 @@ class EtherThief(DetectionModule):
         Require that the current transaction is sent by the attacker and
         that the Ether is sent to the attacker's address.
         """
-
+        attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256)
+        eth_recieved_by_attacker = (
+            value
+            + state.world_state.balances[attacker_address_bitvec]
+            - state.world_state.starting_balances[attacker_address_bitvec]
+        )
+        eth_recieved_by_attacker.simplify()
+        print(eth_recieved_by_attacker)
         constraints += [
-            UGT(value, eth_sent_by_attacker),
+            UGT(eth_recieved_by_attacker, eth_sent_by_attacker),
             target == ATTACKER_ADDRESS,
             state.current_transaction.caller == ATTACKER_ADDRESS,
         ]
 
         try:
-
             transaction_sequence = solver.get_transaction_sequence(state, constraints)
 
             issue = Issue(
diff --git a/mythril/analysis/templates/report_as_text.jinja2 b/mythril/analysis/templates/report_as_text.jinja2
index dd70bb45..776b661d 100644
--- a/mythril/analysis/templates/report_as_text.jinja2
+++ b/mythril/analysis/templates/report_as_text.jinja2
@@ -21,6 +21,8 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
 {% if issue.tx_sequence %}
 Transaction Sequence:
 
+{{ issue.tx_sequence.initialState }}
+
 {% for step in issue.tx_sequence.steps %}
 {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
 Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }}
diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py
index 918c1d3f..7cb084b0 100644
--- a/mythril/laser/ethereum/call.py
+++ b/mythril/laser/ethereum/call.py
@@ -49,7 +49,11 @@ def get_call_parameters(
 
     callee_account = None
     call_data = get_call_data(global_state, memory_input_offset, memory_input_size)
-    if int(callee_address, 16) >= 5 or int(callee_address, 16) == 0:
+    if (
+        isinstance(callee_address, BitVec)
+        or int(callee_address, 16) >= 5
+        or int(callee_address, 16) == 0
+    ):
         callee_account = get_callee_account(
             global_state, callee_address, dynamic_loader
         )
@@ -88,6 +92,8 @@ def get_callee_address(
         log.debug("CALL to: " + str(simplify(symbolic_to_address)))
 
         if match is None or dynamic_loader is None:
+            # TODO: Fix types
+            return symbolic_to_address
             raise ValueError()
 
         index = int(match.group(1))
@@ -111,7 +117,9 @@ def get_callee_address(
 
 
 def get_callee_account(
-    global_state: GlobalState, callee_address: str, dynamic_loader: DynLoader
+    global_state: GlobalState,
+    callee_address: Union[str, BitVec],
+    dynamic_loader: DynLoader,
 ):
     """Gets the callees account from the global_state.
 
@@ -123,6 +131,12 @@ def get_callee_account(
     environment = global_state.environment
     accounts = global_state.accounts
 
+    if isinstance(callee_address, BitVec):
+        if callee_address.symbolic:
+            return Account(callee_address, balances=global_state.world_state.balances)
+        else:
+            callee_address = callee_address.value
+
     try:
         return global_state.accounts[int(callee_address, 16)]
     except KeyError:
diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index b3e3eaa6..79c00945 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -25,7 +25,7 @@ from mythril.laser.smt import (
     Bool,
     Not,
     LShR,
-)
+    BVSubNoUnderflow, UGE)
 from mythril.laser.smt import symbol_factory
 
 import mythril.laser.ethereum.util as helper
@@ -840,7 +840,11 @@ class Instruction:
         """
         state = global_state.mstate
         address = state.stack.pop()
-        state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256))
+
+        balance = global_state.world_state.balances[
+            global_state.environment.active_account.address
+        ]
+        state.stack.append(balance)
         return [global_state]
 
     @StateTransition()
@@ -1688,7 +1692,14 @@ class Instruction:
             )
 
             if callee_account is not None and callee_account.code.bytecode == "":
-                log.debug("The call is related to ether transfer between accounts")
+                log.warning(
+                    "The call is related to ether transfer between accounts"
+                )  # TODO: was debug
+
+                global_state.mstate.constraints.append(UGE(global_state.world_state.balances[environment.active_account.address], value))
+                #global_state.world_state.balances[environment.active_account.address] -= value
+                global_state.world_state.balances[callee_account.address] += value
+
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
                 )
diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py
index f5196287..9e83f63a 100644
--- a/mythril/laser/ethereum/state/account.py
+++ b/mythril/laser/ethereum/state/account.py
@@ -169,6 +169,8 @@ class Account:
         self._balances = balances
         self.balance = lambda: self._balances[self.address]
 
+        # TODO: Add initial balance
+
     def __str__(self) -> str:
         return str(self.as_dict)
 
diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py
index 236da526..d5851533 100644
--- a/mythril/laser/ethereum/state/world_state.py
+++ b/mythril/laser/ethereum/state/world_state.py
@@ -27,6 +27,7 @@ class WorldState:
         """
         self._accounts = {}  # type: Dict[int, Account]
         self.balances = Array("balance", 256, 256)
+        self.starting_balances = copy(self.balances)
 
         self.node = None  # type: Optional['Node']
         self.transaction_sequence = transaction_sequence or []
@@ -60,6 +61,7 @@ class WorldState:
             annotations=new_annotations,
         )
         new_world_state.balances = copy(self.balances)
+        new_world_state.starting_balances = copy(self.starting_balances)
         for account in self._accounts.values():
             new_world_state.put_account(copy(account))
         new_world_state.node = self.node
@@ -115,7 +117,7 @@ class WorldState:
             concrete_storage=concrete_storage,
         )
         if balance:
-            new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
+            new_account.add_balance(symbol_factory.BitVecVal(balance, 256))
 
         self.put_account(new_account)
         return new_account
@@ -180,5 +182,6 @@ class WorldState:
 
         :param account:
         """
+        assert not account.address.symbolic # ???
         self._accounts[account.address.value] = account
         account._balances = self.balances
diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py
index 93cc7e3b..2f5c34cf 100644
--- a/mythril/laser/ethereum/transaction/transaction_models.py
+++ b/mythril/laser/ethereum/transaction/transaction_models.py
@@ -13,7 +13,7 @@ from mythril.laser.ethereum.state.environment import Environment
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.smt import symbol_factory
+from mythril.laser.smt import symbol_factory, BVSubNoUnderflow, UGE
 
 _next_transaction_id = 0
 
@@ -117,7 +117,8 @@ class BaseTransaction:
         receiver = environment.active_account.address
         value = environment.callvalue
 
-        global_state.world_state.balances[sender] -= value
+        global_state.mstate.constraints.append(UGE(global_state.world_state.balances[sender], value))
+        #global_state.world_state.balances[sender] -= value
         global_state.world_state.balances[receiver] += value
 
         return global_state

From 584bdf13d68b4ebf674168ce150ae5b8127b9d31 Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Wed, 24 Jul 2019 15:51:38 -0700
Subject: [PATCH 02/30] First draft of ether balance modeling

---
 mythril/analysis/modules/ether_thief.py       | 64 ++++++-------
 mythril/analysis/solver.py                    | 37 +++++---
 .../analysis/templates/report_as_text.jinja2  |  2 -
 mythril/laser/ethereum/call.py                | 12 +--
 mythril/laser/ethereum/instructions.py        | 91 +++++++++++++++++--
 mythril/laser/ethereum/state/account.py       |  2 -
 mythril/laser/ethereum/state/world_state.py   |  2 +-
 .../transaction/transaction_models.py         | 20 ++--
 tests/laser/evm_testsuite/evm_test.py         |  4 +-
 9 files changed, 156 insertions(+), 78 deletions(-)

diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py
index 95fbe2fb..cf668b25 100644
--- a/mythril/analysis/modules/ether_thief.py
+++ b/mythril/analysis/modules/ether_thief.py
@@ -15,7 +15,15 @@ from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction import ContractCreationTransaction
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import UGT, Sum, symbol_factory, BVAddNoOverflow, If
+from mythril.laser.smt import (
+    UGT,
+    Sum,
+    symbol_factory,
+    BVAddNoOverflow,
+    If,
+    simplify,
+    UGE,
+)
 
 log = logging.getLogger(__name__)
 
@@ -74,55 +82,35 @@ class EtherThief(DetectionModule):
         :param state:
         :return:
         """
+        state = copy(state)
         instruction = state.get_current_instruction()
 
-        if instruction["opcode"] != "CALL":
-            return []
-
-        address = instruction["address"]
-
         value = state.mstate.stack[-3]
         target = state.mstate.stack[-2]
 
-        eth_sent_by_attacker = symbol_factory.BitVecVal(0, 256)
-
         constraints = copy(state.mstate.constraints)
 
-        for tx in state.world_state.transaction_sequence:
-            """
-            Constraint: The call value must be greater than the sum of Ether sent by the attacker over all
-            transactions. This prevents false positives caused by legitimate refund functions.
-            Also constrain the addition from overflowing (otherwise the solver produces solutions with 
-            ridiculously high call values).
-            """
-            constraints += [BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, False)]
-            eth_sent_by_attacker = Sum(
-                eth_sent_by_attacker,
-                tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0),
-            )
-
-            """
-            Constraint: All transactions must originate from regular users (not the creator/owner).
-            This prevents false positives where the owner willingly transfers ownership to another address.
-            """
-
-            if not isinstance(tx, ContractCreationTransaction):
-                constraints += [tx.caller != CREATOR_ADDRESS]
-
         """
         Require that the current transaction is sent by the attacker and
-        that the Ether is sent to the attacker's address.
+        that the Ether sent to the attacker's address is greater than the
+        amount of Ether the attacker sent.
         """
         attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256)
-        eth_recieved_by_attacker = (
-            value
-            + state.world_state.balances[attacker_address_bitvec]
-            - state.world_state.starting_balances[attacker_address_bitvec]
-        )
-        eth_recieved_by_attacker.simplify()
-        print(eth_recieved_by_attacker)
+
+        constraints += [
+            UGE(
+                state.world_state.balances[state.environment.active_account.address],
+                value,
+            )
+        ]
+        state.world_state.balances[attacker_address_bitvec] += value
+        state.world_state.balances[state.environment.active_account.address] -= value
+
         constraints += [
-            UGT(eth_recieved_by_attacker, eth_sent_by_attacker),
+            UGT(
+                state.world_state.balances[attacker_address_bitvec],
+                state.world_state.starting_balances[attacker_address_bitvec],
+            ),
             target == ATTACKER_ADDRESS,
             state.current_transaction.caller == ATTACKER_ADDRESS,
         ]
diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 6a14fb68..547e5d11 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -95,7 +95,7 @@ def get_transaction_sequence(
     concrete_transactions = []
 
     tx_constraints, minimize = _set_minimisation_constraints(
-        transaction_sequence, constraints.copy(), [], 5000
+        transaction_sequence, constraints.copy(), [], 5000, global_state.world_state
     )
 
     try:
@@ -103,19 +103,23 @@ def get_transaction_sequence(
     except UnsatError:
         raise UnsatError
 
-    min_price_dict = {}  # type: Dict[str, int]
+    # Include creation account in initial state
+    # Note: This contains the code, which should not exist until after the first tx
+    initial_world_state = transaction_sequence[0].world_state
+    initial_accounts = initial_world_state.accounts
+
     for transaction in transaction_sequence:
         concrete_transaction = _get_concrete_transaction(model, transaction)
         concrete_transactions.append(concrete_transaction)
 
-        caller = concrete_transaction["origin"]
-        value = int(concrete_transaction["value"], 16)
-        min_price_dict[caller] = min_price_dict.get(caller, 0) + value
-
-    if isinstance(transaction_sequence[0], ContractCreationTransaction):
-        initial_accounts = transaction_sequence[0].prev_world_state.accounts
-    else:
-        initial_accounts = transaction_sequence[0].world_state.accounts
+    min_price_dict = {}  # type: Dict[str, int]
+    for address in initial_accounts.keys():
+        min_price_dict[address] = model.eval(
+            initial_world_state.starting_balances[
+                symbol_factory.BitVecVal(address, 256)
+            ].raw,
+            model_completion=True,
+        ).as_long()
 
     concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict)
 
@@ -171,7 +175,7 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
 
 
 def _set_minimisation_constraints(
-    transaction_sequence, constraints, minimize, max_size
+    transaction_sequence, constraints, minimize, max_size, world_state
 ) -> Tuple[Constraints, tuple]:
     """ Set constraints that minimise key transaction values
 
@@ -192,6 +196,15 @@ def _set_minimisation_constraints(
 
         # Minimize
         minimize.append(transaction.call_data.calldatasize)
-        minimize.append(transaction.call_value)
+
+    for account in world_state.accounts.values():
+        # Lazy way to prevent overflows and to ensure "reasonable" balances
+        # Each account starts with less than 100 ETH
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(100000000000000000000, 256),
+                world_state.starting_balances[account.address],
+            )
+        )
 
     return constraints, tuple(minimize)
diff --git a/mythril/analysis/templates/report_as_text.jinja2 b/mythril/analysis/templates/report_as_text.jinja2
index 8fa2454a..d7b84355 100644
--- a/mythril/analysis/templates/report_as_text.jinja2
+++ b/mythril/analysis/templates/report_as_text.jinja2
@@ -21,8 +21,6 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
 {% if issue.tx_sequence %}
 Transaction Sequence:
 
-{{ issue.tx_sequence.initialState }}
-
 {% for step in issue.tx_sequence.steps %}
 {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
 Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }}
diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py
index 7cb084b0..f29c34bf 100644
--- a/mythril/laser/ethereum/call.py
+++ b/mythril/laser/ethereum/call.py
@@ -88,13 +88,12 @@ def get_callee_address(
     except TypeError:
         log.debug("Symbolic call encountered")
 
-        match = re.search(r"storage_(\d+)", str(simplify(symbolic_to_address)))
+        match = re.search(r"Storage\[(\d+)\]", str(simplify(symbolic_to_address)))
         log.debug("CALL to: " + str(simplify(symbolic_to_address)))
 
         if match is None or dynamic_loader is None:
             # TODO: Fix types
             return symbolic_to_address
-            raise ValueError()
 
         index = int(match.group(1))
         log.debug("Dynamic contract address at storage index {}".format(index))
@@ -106,8 +105,7 @@ def get_callee_address(
             )
         # TODO: verify whether this happens or not
         except:
-            log.debug("Error accessing contract storage.")
-            raise ValueError
+            return symbolic_to_address
 
         # testrpc simply returns the address, geth response is more elaborate.
         if not re.match(r"^0x[0-9a-f]{40}$", callee_address):
@@ -135,7 +133,7 @@ def get_callee_account(
         if callee_address.symbolic:
             return Account(callee_address, balances=global_state.world_state.balances)
         else:
-            callee_address = callee_address.value
+            callee_address = hex(callee_address.value)[2:]
 
     try:
         return global_state.accounts[int(callee_address, 16)]
@@ -223,12 +221,12 @@ def get_call_data(
 
 def native_call(
     global_state: GlobalState,
-    callee_address: str,
+    callee_address: Union[str, BitVec],
     call_data: BaseCalldata,
     memory_out_offset: Union[int, Expression],
     memory_out_size: Union[int, Expression],
 ) -> Union[List[GlobalState], None]:
-    if not 0 < int(callee_address, 16) < 5:
+    if isinstance(callee_address, BitVec) or not 0 < int(callee_address, 16) < 5:
         return None
 
     log.debug("Native contract called: " + callee_address)
diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 79c00945..eda8a037 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -25,7 +25,9 @@ from mythril.laser.smt import (
     Bool,
     Not,
     LShR,
-    BVSubNoUnderflow, UGE)
+    BVSubNoUnderflow,
+    UGE,
+)
 from mythril.laser.smt import symbol_factory
 
 import mythril.laser.ethereum.util as helper
@@ -1619,7 +1621,7 @@ class Instruction:
         transfer_amount = global_state.environment.active_account.balance()
         # Often the target of the suicide instruction will be symbolic
         # If it isn't then we'll transfer the balance to the indicated contract
-        global_state.world_state[target].add_balance(transfer_amount)
+        global_state.world_state.balances[target] += transfer_amount
 
         global_state.environment.active_account = deepcopy(
             global_state.environment.active_account
@@ -1692,13 +1694,20 @@ class Instruction:
             )
 
             if callee_account is not None and callee_account.code.bytecode == "":
-                log.warning(
-                    "The call is related to ether transfer between accounts"
-                )  # TODO: was debug
+                log.debug("The call is related to ether transfer between accounts")
+                sender = environment.active_account.address
+                receiver = callee_account.address
+                value = (
+                    value
+                    if isinstance(value, BitVec)
+                    else symbol_factory.BitVecVal(value, 256)
+                )
 
-                global_state.mstate.constraints.append(UGE(global_state.world_state.balances[environment.active_account.address], value))
-                #global_state.world_state.balances[environment.active_account.address] -= value
-                global_state.world_state.balances[callee_account.address] += value
+                global_state.mstate.constraints.append(
+                    UGE(global_state.world_state.balances[sender], value)
+                )
+                global_state.world_state.balances[receiver] += value
+                global_state.world_state.balances[sender] -= value
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1815,6 +1824,28 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters(
                 global_state, self.dynamic_loader, True
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = global_state.environment.active_account.address
+                receiver = callee_account.address
+                value = (
+                    value
+                    if isinstance(value, BitVec)
+                    else symbol_factory.BitVecVal(value, 256)
+                )
+
+                global_state.mstate.constraints.append(
+                    UGE(global_state.world_state.balances[sender], value)
+                )
+                global_state.world_state.balances[receiver] += value
+                global_state.world_state.balances[sender] -= value
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
@@ -1918,6 +1949,28 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters(
                 global_state, self.dynamic_loader
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = environment.active_account.address
+                receiver = callee_account.address
+                value = (
+                    value
+                    if isinstance(value, BitVec)
+                    else symbol_factory.BitVecVal(value, 256)
+                )
+
+                global_state.mstate.constraints.append(
+                    UGE(global_state.world_state.balances[sender], value)
+                )
+                global_state.world_state.balances[receiver] += value
+                global_state.world_state.balances[sender] -= value
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
@@ -2019,6 +2072,28 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters(
                 global_state, self.dynamic_loader
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = global_state.environment.active_account.address
+                receiver = callee_account.address
+                value = (
+                    value
+                    if isinstance(value, BitVec)
+                    else symbol_factory.BitVecVal(value, 256)
+                )
+
+                global_state.mstate.constraints.append(
+                    UGE(global_state.world_state.balances[sender], value)
+                )
+                global_state.world_state.balances[receiver] += value
+                global_state.world_state.balances[sender] -= value
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py
index 51d61d27..1a32ad37 100644
--- a/mythril/laser/ethereum/state/account.py
+++ b/mythril/laser/ethereum/state/account.py
@@ -189,8 +189,6 @@ class Account:
         self._balances = balances
         self.balance = lambda: self._balances[self.address]
 
-        # TODO: Add initial balance
-
     def __str__(self) -> str:
         return str(self.as_dict)
 
diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py
index d5851533..5227099e 100644
--- a/mythril/laser/ethereum/state/world_state.py
+++ b/mythril/laser/ethereum/state/world_state.py
@@ -182,6 +182,6 @@ class WorldState:
 
         :param account:
         """
-        assert not account.address.symbolic # ???
+        assert not account.address.symbolic  # ???
         self._accounts[account.address.value] = account
         account._balances = self.balances
diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py
index 2f5c34cf..f29e9236 100644
--- a/mythril/laser/ethereum/transaction/transaction_models.py
+++ b/mythril/laser/ethereum/transaction/transaction_models.py
@@ -4,7 +4,7 @@ execution."""
 import array
 from copy import deepcopy
 from z3 import ExprRef
-from typing import Union, Optional, cast
+from typing import Union, Optional
 
 from mythril.laser.ethereum.state.calldata import ConcreteCalldata
 from mythril.laser.ethereum.state.account import Account
@@ -12,8 +12,10 @@ from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata
 from mythril.laser.ethereum.state.environment import Environment
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.world_state import WorldState
-from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.smt import symbol_factory, BVSubNoUnderflow, UGE
+from mythril.laser.smt import symbol_factory, UGE, BitVec
+import logging
+
+log = logging.getLogger(__name__)
 
 _next_transaction_id = 0
 
@@ -115,11 +117,17 @@ class BaseTransaction:
 
         sender = environment.sender
         receiver = environment.active_account.address
-        value = environment.callvalue
+        value = (
+            environment.callvalue
+            if isinstance(environment.callvalue, BitVec)
+            else symbol_factory.BitVecVal(environment.callvalue, 256)
+        )
 
-        global_state.mstate.constraints.append(UGE(global_state.world_state.balances[sender], value))
-        #global_state.world_state.balances[sender] -= value
+        global_state.mstate.constraints.append(
+            UGE(global_state.world_state.balances[sender], value)
+        )
         global_state.world_state.balances[receiver] += value
+        global_state.world_state.balances[sender] -= value
 
         return global_state
 
diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py
index 244b5844..e5d1727d 100644
--- a/tests/laser/evm_testsuite/evm_test.py
+++ b/tests/laser/evm_testsuite/evm_test.py
@@ -165,8 +165,8 @@ def test_vmtest(
         # no more work to do if error happens or out of gas
         assert len(laser_evm.open_states) == 0
     else:
-        assert len(laser_evm.open_states) == 1
-        world_state = laser_evm.open_states[0]
+        assert len(final_states) == 1
+        world_state = final_states[0].world_state
 
         for address, details in post_condition.items():
             account = world_state[symbol_factory.BitVecVal(int(address, 16), 256)]

From a288da7bb5c42a3e443eccb82a73ea48a03b6dda Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Wed, 24 Jul 2019 16:28:03 -0700
Subject: [PATCH 03/30] Clean up leftover code

---
 mythril/analysis/modules/ether_thief.py     | 17 +----
 mythril/laser/ethereum/call.py              |  1 -
 mythril/laser/ethereum/instructions.py      | 73 ++++++++-------------
 mythril/laser/ethereum/state/world_state.py |  1 -
 4 files changed, 30 insertions(+), 62 deletions(-)

diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py
index cf668b25..948e9c89 100644
--- a/mythril/analysis/modules/ether_thief.py
+++ b/mythril/analysis/modules/ether_thief.py
@@ -1,29 +1,16 @@
 """This module contains the detection code for unauthorized ether
 withdrawal."""
 import logging
-import json
 from copy import copy
 
 from mythril.analysis import solver
 from mythril.analysis.modules.base import DetectionModule
 from mythril.analysis.report import Issue
-from mythril.laser.ethereum.transaction.symbolic import (
-    ATTACKER_ADDRESS,
-    CREATOR_ADDRESS,
-)
+from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
 from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.exceptions import UnsatError
-from mythril.laser.ethereum.transaction import ContractCreationTransaction
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import (
-    UGT,
-    Sum,
-    symbol_factory,
-    BVAddNoOverflow,
-    If,
-    simplify,
-    UGE,
-)
+from mythril.laser.smt import UGT, symbol_factory, UGE
 
 log = logging.getLogger(__name__)
 
diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py
index f29c34bf..e31f0474 100644
--- a/mythril/laser/ethereum/call.py
+++ b/mythril/laser/ethereum/call.py
@@ -92,7 +92,6 @@ def get_callee_address(
         log.debug("CALL to: " + str(simplify(symbolic_to_address)))
 
         if match is None or dynamic_loader is None:
-            # TODO: Fix types
             return symbolic_to_address
 
         index = int(match.group(1))
diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index eda8a037..80dcd840 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -25,7 +25,6 @@ from mythril.laser.smt import (
     Bool,
     Not,
     LShR,
-    BVSubNoUnderflow,
     UGE,
 )
 from mythril.laser.smt import symbol_factory
@@ -56,6 +55,30 @@ TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
 
 
+def transfer_ether(
+    global_state: GlobalState,
+    sender: BitVec,
+    receiver: BitVec,
+    value: Union[int, BitVec],
+):
+    """
+    Perform an Ether transfer between two accounts
+
+    :param global_state: The global state in which the Ether transfer occurs
+    :param sender: The sender of the Ether
+    :param receiver: The recipient of the Ether
+    :param value: The amount of Ether to send
+    :return:
+    """
+    value = value if isinstance(value, BitVec) else symbol_factory.BitVecVal(value, 256)
+
+    global_state.mstate.constraints.append(
+        UGE(global_state.world_state.balances[sender], value)
+    )
+    global_state.world_state.balances[receiver] += value
+    global_state.world_state.balances[sender] -= value
+
+
 class StateTransition(object):
     """Decorator that handles global state copy and original return.
 
@@ -1697,17 +1720,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = environment.active_account.address
                 receiver = callee_account.address
-                value = (
-                    value
-                    if isinstance(value, BitVec)
-                    else symbol_factory.BitVecVal(value, 256)
-                )
-
-                global_state.mstate.constraints.append(
-                    UGE(global_state.world_state.balances[sender], value)
-                )
-                global_state.world_state.balances[receiver] += value
-                global_state.world_state.balances[sender] -= value
+                transfer_ether(sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1829,17 +1842,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = global_state.environment.active_account.address
                 receiver = callee_account.address
-                value = (
-                    value
-                    if isinstance(value, BitVec)
-                    else symbol_factory.BitVecVal(value, 256)
-                )
-
-                global_state.mstate.constraints.append(
-                    UGE(global_state.world_state.balances[sender], value)
-                )
-                global_state.world_state.balances[receiver] += value
-                global_state.world_state.balances[sender] -= value
+                transfer_ether(sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1954,17 +1957,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = environment.active_account.address
                 receiver = callee_account.address
-                value = (
-                    value
-                    if isinstance(value, BitVec)
-                    else symbol_factory.BitVecVal(value, 256)
-                )
-
-                global_state.mstate.constraints.append(
-                    UGE(global_state.world_state.balances[sender], value)
-                )
-                global_state.world_state.balances[receiver] += value
-                global_state.world_state.balances[sender] -= value
+                transfer_ether(sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -2077,17 +2070,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = global_state.environment.active_account.address
                 receiver = callee_account.address
-                value = (
-                    value
-                    if isinstance(value, BitVec)
-                    else symbol_factory.BitVecVal(value, 256)
-                )
-
-                global_state.mstate.constraints.append(
-                    UGE(global_state.world_state.balances[sender], value)
-                )
-                global_state.world_state.balances[receiver] += value
-                global_state.world_state.balances[sender] -= value
+                transfer_ether(sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py
index 5227099e..20628877 100644
--- a/mythril/laser/ethereum/state/world_state.py
+++ b/mythril/laser/ethereum/state/world_state.py
@@ -182,6 +182,5 @@ class WorldState:
 
         :param account:
         """
-        assert not account.address.symbolic  # ???
         self._accounts[account.address.value] = account
         account._balances = self.balances

From 267fbf06ebf05105777d3c02127de558cc154863 Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Wed, 24 Jul 2019 22:44:04 -0700
Subject: [PATCH 04/30] Fix missing argument to function

---
 mythril/laser/ethereum/instructions.py | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 80dcd840..e5347f2f 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -1720,7 +1720,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = environment.active_account.address
                 receiver = callee_account.address
-                transfer_ether(sender, receiver, value)
+                transfer_ether(global_state, sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1842,7 +1842,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = global_state.environment.active_account.address
                 receiver = callee_account.address
-                transfer_ether(sender, receiver, value)
+                transfer_ether(global_state, sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1957,7 +1957,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = environment.active_account.address
                 receiver = callee_account.address
-                transfer_ether(sender, receiver, value)
+                transfer_ether(global_state, sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -2070,7 +2070,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = global_state.environment.active_account.address
                 receiver = callee_account.address
-                transfer_ether(sender, receiver, value)
+                transfer_ether(global_state, sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)

From 2aa0d39646f767c32d28772645911c91c9377ceb Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Thu, 25 Jul 2019 12:03:06 -0700
Subject: [PATCH 05/30] Only add constraint to symbolic Ether balances

---
 mythril/analysis/solver.py                            | 11 ++++++-----
 .../laser/ethereum/transaction/transaction_models.py  |  1 -
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 547e5d11..82e3f2ee 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -200,11 +200,12 @@ def _set_minimisation_constraints(
     for account in world_state.accounts.values():
         # Lazy way to prevent overflows and to ensure "reasonable" balances
         # Each account starts with less than 100 ETH
-        constraints.append(
-            UGE(
-                symbol_factory.BitVecVal(100000000000000000000, 256),
-                world_state.starting_balances[account.address],
+        if account.address.symbolic:
+            constraints.append(
+                UGE(
+                    symbol_factory.BitVecVal(100000000000000000000, 256),
+                    world_state.starting_balances[account.address],
+                )
             )
-        )
 
     return constraints, tuple(minimize)
diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py
index f29e9236..bccdf7aa 100644
--- a/mythril/laser/ethereum/transaction/transaction_models.py
+++ b/mythril/laser/ethereum/transaction/transaction_models.py
@@ -189,7 +189,6 @@ class ContractCreationTransaction(BaseTransaction):
             0, concrete_storage=True, creator=caller.value
         )
         callee_account.contract_name = contract_name
-        # TODO: set correct balance for new account
         super().__init__(
             world_state=world_state,
             callee_account=callee_account,

From 518e33b45b1de974e94eb0779c9c91d8d1f2f6ee Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Mon, 29 Jul 2019 09:25:04 -0700
Subject: [PATCH 06/30] Fix incorrect values in some suicide evm tests

---
 .../evm_testsuite/VMTests/vmSystemOperations/suicide0.json    | 4 ++--
 .../VMTests/vmSystemOperations/suicideNotExistingAccount.json | 4 ++--
 .../VMTests/vmSystemOperations/suicideSendEtherToMe.json      | 4 ++--
 tests/laser/evm_testsuite/evm_test.py                         | 4 ++--
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json
index ae80e8f6..456a7c16 100644
--- a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json
+++ b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json
@@ -47,7 +47,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {
@@ -55,4 +55,4 @@
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json
index ecf5d3bc..b72d6bcc 100644
--- a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json
+++ b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json
@@ -54,7 +54,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {
@@ -62,4 +62,4 @@
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json
index 7a8f19b8..f27557ed 100644
--- a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json
+++ b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json
@@ -47,7 +47,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {
@@ -55,4 +55,4 @@
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py
index e5d1727d..244b5844 100644
--- a/tests/laser/evm_testsuite/evm_test.py
+++ b/tests/laser/evm_testsuite/evm_test.py
@@ -165,8 +165,8 @@ def test_vmtest(
         # no more work to do if error happens or out of gas
         assert len(laser_evm.open_states) == 0
     else:
-        assert len(final_states) == 1
-        world_state = final_states[0].world_state
+        assert len(laser_evm.open_states) == 1
+        world_state = laser_evm.open_states[0]
 
         for address, details in post_condition.items():
             account = world_state[symbol_factory.BitVecVal(int(address, 16), 256)]

From 73d11a6405284e5db3666959d7b4a5aa56315c4b Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Tue, 6 Aug 2019 09:08:02 -0700
Subject: [PATCH 07/30] Update wiki links to Read the Docs links

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 4eee32a3..df3ad81c 100644
--- a/README.md
+++ b/README.md
@@ -32,7 +32,7 @@ Install from Pypi:
 $ pip3 install mythril
 ```
 
-See the [Wiki](https://github.com/ConsenSys/mythril/wiki/Installation-and-Setup) for more detailed instructions. 
+See the [docs](https://mythril-classic.readthedocs.io/en/master/installation.html) for more detailed instructions. 
 
 ## Usage
 
@@ -75,7 +75,7 @@ Caller: [ATTACKER], function: commencekilling(), txdata: 0x7c11da20, value: 0x0
 ```
 
 
-Instructions for using Mythril are found on the [Wiki](https://github.com/ConsenSys/mythril/wiki). 
+Instructions for using Mythril are found on the [docs](https://mythril-classic.readthedocs.io/en/master/). 
 
 For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
 

From b08a9d9d84d8159dd3a3665498bb4ec098a12db4 Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Wed, 7 Aug 2019 12:00:18 -0700
Subject: [PATCH 08/30] Constrain all transaction callers to have <= 1000 ETH

---
 mythril/analysis/solver.py | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 82e3f2ee..8755c6c5 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -8,7 +8,7 @@ from mythril.analysis.analysis_args import analysis_args
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.constraints import Constraints
 from mythril.laser.ethereum.transaction import BaseTransaction
-from mythril.laser.smt import UGE, Optimize, symbol_factory
+from mythril.laser.smt import UGE, Optimize, symbol_factory, simplify
 from mythril.laser.ethereum.time_handler import time_handler
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction.transaction_models import (
@@ -197,15 +197,21 @@ def _set_minimisation_constraints(
         # Minimize
         minimize.append(transaction.call_data.calldatasize)
 
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(1000000000000000000000, 256),
+                world_state.starting_balances[transaction.caller],
+            )
+        )
+
     for account in world_state.accounts.values():
         # Lazy way to prevent overflows and to ensure "reasonable" balances
         # Each account starts with less than 100 ETH
-        if account.address.symbolic:
-            constraints.append(
-                UGE(
-                    symbol_factory.BitVecVal(100000000000000000000, 256),
-                    world_state.starting_balances[account.address],
-                )
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(100000000000000000000, 256),
+                world_state.starting_balances[account.address],
             )
+        )
 
     return constraints, tuple(minimize)

From 4bfaadea98bed96a7b4b9385614c99eb74f66261 Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Wed, 7 Aug 2019 12:03:17 -0700
Subject: [PATCH 09/30] Remove unneeded import

---
 mythril/analysis/solver.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 8755c6c5..3358d537 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -8,7 +8,7 @@ from mythril.analysis.analysis_args import analysis_args
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.constraints import Constraints
 from mythril.laser.ethereum.transaction import BaseTransaction
-from mythril.laser.smt import UGE, Optimize, symbol_factory, simplify
+from mythril.laser.smt import UGE, Optimize, symbol_factory
 from mythril.laser.ethereum.time_handler import time_handler
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction.transaction_models import (

From 5f3a84107eeed5f5ff4a0454a6e262ff6bb9019c Mon Sep 17 00:00:00 2001
From: e-ngo <52668908+e-ngo@users.noreply.github.com>
Date: Wed, 7 Aug 2019 18:15:45 -0700
Subject: [PATCH 10/30] "true" to True (#1188)

---
 mythril/analysis/report.py    | 2 +-
 mythril/interfaces/cli.py     | 4 +---
 mythril/interfaces/old_cli.py | 4 +---
 3 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/mythril/analysis/report.py b/mythril/analysis/report.py
index 1a39c0ff..d40c466b 100644
--- a/mythril/analysis/report.py
+++ b/mythril/analysis/report.py
@@ -238,7 +238,7 @@ class Report:
             return {}
         logs = []  # type: List[Dict]
         for exception in self.exceptions:
-            logs += [{"level": "error", "hidden": "true", "msg": exception}]
+            logs += [{"level": "error", "hidden": True, "msg": exception}]
         return {"logs": logs}
 
     def as_swc_standard_format(self):
diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py
index 8962fa16..2cbf3f4c 100644
--- a/mythril/interfaces/cli.py
+++ b/mythril/interfaces/cli.py
@@ -63,9 +63,7 @@ def exit_with_error(format_, message):
                 "sourceType": "",
                 "sourceFormat": "",
                 "sourceList": [],
-                "meta": {
-                    "logs": [{"level": "error", "hidden": "true", "msg": message}]
-                },
+                "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]},
             }
         ]
         print(json.dumps(result))
diff --git a/mythril/interfaces/old_cli.py b/mythril/interfaces/old_cli.py
index 0deedc85..211d1c8e 100644
--- a/mythril/interfaces/old_cli.py
+++ b/mythril/interfaces/old_cli.py
@@ -44,9 +44,7 @@ def exit_with_error(format_, message):
                 "sourceType": "",
                 "sourceFormat": "",
                 "sourceList": [],
-                "meta": {
-                    "logs": [{"level": "error", "hidden": "true", "msg": message}]
-                },
+                "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]},
             }
         ]
         print(json.dumps(result))

From 4b1bcbeb3e86df0f0fb22eb80b10bcf2c1c6d71f Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Thu, 8 Aug 2019 06:46:14 +0530
Subject: [PATCH 11/30] Version update

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

diff --git a/mythril/__version__.py b/mythril/__version__.py
index a9b138d9..b7808215 100644
--- a/mythril/__version__.py
+++ b/mythril/__version__.py
@@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
 as for importing into Python.
 """
 
-__version__ = "v0.21.13"
+__version__ = "v0.21.14"

From 4f539f6bf069f277f1e4d009fd86449fd2d810f6 Mon Sep 17 00:00:00 2001
From: palkeo <contact@palkeo.com>
Date: Thu, 8 Aug 2019 20:35:34 +0200
Subject: [PATCH 12/30] Fix a bug: correctly copy printable storage over
 (#1191)

* Fix a bug: the key for the accounts is an integer.

* Fix a bug: correctly copy printable storage.

Also fix another serialization bug that appears now that the printable
storage is not empty.

* Revert "Fix a bug: the key for the accounts is an integer."

Should not have been included in that PR.
---
 mythril/analysis/solver.py              | 2 +-
 mythril/laser/ethereum/state/account.py | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 3358d537..d949dd57 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -137,7 +137,7 @@ def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]):
         data = dict()  # type: Dict[str, Union[int, str]]
         data["nonce"] = account.nonce
         data["code"] = account.code.bytecode
-        data["storage"] = account.storage.printable_storage
+        data["storage"] = str(account.storage)
         data["balance"] = hex(min_price_dict.get(address, 0))
         accounts[hex(address)] = data
     return {"accounts": accounts}
diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py
index 4c47516a..0b9aec62 100644
--- a/mythril/laser/ethereum/state/account.py
+++ b/mythril/laser/ethereum/state/account.py
@@ -144,7 +144,7 @@ class Storage:
         )
         storage._standard_storage = deepcopy(self._standard_storage)
         storage._map_storage = deepcopy(self._map_storage)
-        storage.print_storage = copy(self.printable_storage)
+        storage.printable_storage = copy(self.printable_storage)
         return storage
 
     def __str__(self) -> str:

From 8397ca89ad0ec5ff3f2a6fd1e3cce996d6e86bbc Mon Sep 17 00:00:00 2001
From: palkeo <contact@palkeo.com>
Date: Thu, 8 Aug 2019 20:52:16 +0200
Subject: [PATCH 13/30] Fix a bug: the key for the accounts is an integer.
 (#1190)

---
 mythril/laser/ethereum/call.py | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py
index 753d97d4..2e471037 100644
--- a/mythril/laser/ethereum/call.py
+++ b/mythril/laser/ethereum/call.py
@@ -125,8 +125,6 @@ def get_callee_account(
     :param dynamic_loader: dynamic loader to use
     :return: Account belonging to callee
     """
-    accounts = global_state.accounts
-
     if isinstance(callee_address, BitVec):
         if callee_address.symbolic:
             return Account(callee_address, balances=global_state.world_state.balances)
@@ -161,7 +159,7 @@ def get_callee_account(
         dynamic_loader=dynamic_loader,
         balances=global_state.world_state.balances,
     )
-    accounts[callee_address] = callee_account
+    global_state.accounts[int(callee_address, 16)] = callee_account
 
     return callee_account
 

From 04d295b329f74b133c2cbfe27a54268815cc28f9 Mon Sep 17 00:00:00 2001
From: palkeo <contact@palkeo.com>
Date: Thu, 8 Aug 2019 19:26:03 +0200
Subject: [PATCH 14/30] Track what storage has been initialized, and load
 non-initialized storage.

---
 mythril/laser/ethereum/state/account.py | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py
index 0b9aec62..98ca205c 100644
--- a/mythril/laser/ethereum/state/account.py
+++ b/mythril/laser/ethereum/state/account.py
@@ -60,6 +60,7 @@ class Storage:
         self.printable_storage = {}  # type: Dict[BitVec, BitVec]
 
         self.dynld = dynamic_loader
+        self.storage_keys_loaded = set()
         self.address = address
 
     @staticmethod
@@ -75,12 +76,11 @@ class Storage:
         storage, is_keccak_storage = self._get_corresponding_storage(item)
         if is_keccak_storage:
             item = self._sanitize(cast(BitVecFunc, item).input_)
-        value = storage[item]
         if (
-            (value.value == 0 or value.value is None)  # 0 for Array, None for K
-            and self.address
-            and item.symbolic is False
+            self.address
             and self.address.value != 0
+            and int(item.value) not in self.storage_keys_loaded
+            and item.symbolic is False
             and (self.dynld and self.dynld.storage_loading)
         ):
             try:
@@ -94,8 +94,8 @@ class Storage:
                     ),
                     256,
                 )
+                self.storage_keys_loaded.add(int(item.value))
                 self.printable_storage[item] = storage[item]
-                return storage[item]
             except ValueError as e:
                 log.debug("Couldn't read storage at %s: %s", item, e)
 
@@ -136,6 +136,7 @@ class Storage:
         if is_keccak_storage:
             key = self._sanitize(key.input_)
         storage[key] = value
+        self.storage_keys_loaded.add(int(key.value))
 
     def __deepcopy__(self, memodict=dict()):
         concrete = isinstance(self._standard_storage, K)
@@ -145,6 +146,7 @@ class Storage:
         storage._standard_storage = deepcopy(self._standard_storage)
         storage._map_storage = deepcopy(self._map_storage)
         storage.printable_storage = copy(self.printable_storage)
+        storage.storage_keys_loaded = copy(self.storage_keys_loaded)
         return storage
 
     def __str__(self) -> str:

From a9fd342baf0b5317935778a8cb66cc92783afea9 Mon Sep 17 00:00:00 2001
From: palkeo <contact@palkeo.com>
Date: Thu, 8 Aug 2019 19:50:05 +0200
Subject: [PATCH 15/30] Check if item is symbolic first.

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

diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py
index 98ca205c..2c1d8887 100644
--- a/mythril/laser/ethereum/state/account.py
+++ b/mythril/laser/ethereum/state/account.py
@@ -79,8 +79,8 @@ class Storage:
         if (
             self.address
             and self.address.value != 0
-            and int(item.value) not in self.storage_keys_loaded
             and item.symbolic is False
+            and int(item.value) not in self.storage_keys_loaded
             and (self.dynld and self.dynld.storage_loading)
         ):
             try:

From b46f2a4001b2193a75d4e5af1053df85753350ea Mon Sep 17 00:00:00 2001
From: palkeo <contact@palkeo.com>
Date: Thu, 8 Aug 2019 20:04:15 +0200
Subject: [PATCH 16/30] Check that key is not symbolic in __setitem__

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

diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py
index 2c1d8887..fc3204cf 100644
--- a/mythril/laser/ethereum/state/account.py
+++ b/mythril/laser/ethereum/state/account.py
@@ -136,7 +136,8 @@ class Storage:
         if is_keccak_storage:
             key = self._sanitize(key.input_)
         storage[key] = value
-        self.storage_keys_loaded.add(int(key.value))
+        if key.symbolic is False:
+            self.storage_keys_loaded.add(int(key.value))
 
     def __deepcopy__(self, memodict=dict()):
         concrete = isinstance(self._standard_storage, K)

From ef1cbc405229a3ac66477d1d119b5fa76feec670 Mon Sep 17 00:00:00 2001
From: palkeo <contact@palkeo.com>
Date: Fri, 9 Aug 2019 00:03:56 +0200
Subject: [PATCH 17/30] Add type annotation.

---
 mythril/laser/ethereum/state/account.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py
index fc3204cf..53649221 100644
--- a/mythril/laser/ethereum/state/account.py
+++ b/mythril/laser/ethereum/state/account.py
@@ -4,7 +4,7 @@ This includes classes representing accounts and their storage.
 """
 import logging
 from copy import copy, deepcopy
-from typing import Any, Dict, Union, Tuple, cast
+from typing import Any, Dict, Union, Tuple, Set, cast
 
 
 from mythril.laser.smt import (
@@ -60,7 +60,7 @@ class Storage:
         self.printable_storage = {}  # type: Dict[BitVec, BitVec]
 
         self.dynld = dynamic_loader
-        self.storage_keys_loaded = set()
+        self.storage_keys_loaded = set()  # type: Set[int]
         self.address = address
 
     @staticmethod

From bcf528e13968a5189e6974db93c88d00c6c5502c Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Thu, 8 Aug 2019 17:42:32 -0700
Subject: [PATCH 18/30] Fix pruning of calls

---
 mythril/analysis/solver.py                    |  8 ++++
 .../implementations/dependency_pruner.py      | 39 +++++++++++++------
 .../implementations/mutation_pruner.py        |  4 ++
 3 files changed, 40 insertions(+), 11 deletions(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index d949dd57..9504c71a 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -204,6 +204,14 @@ def _set_minimisation_constraints(
             )
         )
 
+        # FIXME: This shouldn't be needed.
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(1000000000000000000000, 256),
+                transaction.call_value,
+            )
+        )
+
     for account in world_state.accounts.values():
         # Lazy way to prevent overflows and to ensure "reasonable" balances
         # Each account starts with less than 100 ETH
diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py
index bb78fdd8..b2b1ee16 100644
--- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py
+++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py
@@ -25,6 +25,7 @@ class DependencyAnnotation(StateAnnotation):
     def __init__(self):
         self.storage_loaded = []  # type: List
         self.storage_written = {}  # type: Dict[int, List]
+        self.has_call = False  # type: bool
         self.path = [0]  # type: List
         self.blocks_seen = set()  # type: Set[int]
 
@@ -32,6 +33,7 @@ class DependencyAnnotation(StateAnnotation):
         result = DependencyAnnotation()
         result.storage_loaded = copy(self.storage_loaded)
         result.storage_written = copy(self.storage_written)
+        result.has_call = self.has_call
         result.path = copy(self.path)
         result.blocks_seen = copy(self.blocks_seen)
         return result
@@ -134,6 +136,7 @@ class DependencyPruner(LaserPlugin):
 
     def _reset(self):
         self.iteration = 0
+        self.calls_on_path = {}  # type: Dict[int, bool]
         self.sloads_on_path = {}  # type: Dict[int, List[object]]
         self.sstores_on_path = {}  # type: Dict[int, List[object]]
         self.storage_accessed_global = set()  # type: Set
@@ -166,6 +169,17 @@ class DependencyPruner(LaserPlugin):
             else:
                 self.sstores_on_path[address] = [target_location]
 
+    def update_calls(self, path: List[int]) -> None:
+        """Update the dependency map for the block offsets on the given path.
+
+        :param path
+        :param target_location
+        """
+
+        for address in path:
+            if address in self.sstores_on_path:
+                self.calls_on_path[address] = True
+
     def wanna_execute(self, address: int, annotation: DependencyAnnotation) -> bool:
         """Decide whether the basic block starting at 'address' should be executed.
 
@@ -175,6 +189,9 @@ class DependencyPruner(LaserPlugin):
 
         storage_write_cache = annotation.get_storage_write_cache(self.iteration - 1)
 
+        if address in self.calls_on_path:
+            return True
+
         # Skip "pure" paths that don't have any dependencies.
 
         if address not in self.sloads_on_path:
@@ -270,6 +287,13 @@ class DependencyPruner(LaserPlugin):
             self.update_sloads(annotation.path, location)
             self.storage_accessed_global.add(location)
 
+        @symbolic_vm.pre_hook("CALL")
+        def stop_hook(state: GlobalState):
+            annotation = get_dependency_annotation(state)
+
+            self.update_calls(annotation.path)
+            annotation.has_call = True
+
         @symbolic_vm.pre_hook("STOP")
         def stop_hook(state: GlobalState):
             _transaction_end(state)
@@ -293,11 +317,14 @@ class DependencyPruner(LaserPlugin):
             for index in annotation.storage_written:
                 self.update_sstores(annotation.path, index)
 
+            if annotation.has_call:
+                self.update_calls(annotation.path)
+
         def _check_basic_block(address: int, annotation: DependencyAnnotation):
             """This method is where the actual pruning happens.
 
              :param address: Start address (bytecode offset) of the block
-             :param annotation
+             :param annotation:
              """
 
             # Don't skip any blocks in the contract creation transaction
@@ -338,13 +365,3 @@ class DependencyPruner(LaserPlugin):
             annotation.storage_loaded = []
 
             world_state_annotation.annotations_stack.append(annotation)
-
-            log.debug(
-                "Iteration {}: Adding world state at address {}, end of function {}.\nDependency map: {}\nStorage written: {}".format(
-                    self.iteration,
-                    state.get_current_instruction()["address"],
-                    state.node.function_name,
-                    self.sloads_on_path,
-                    annotation.storage_written[self.iteration],
-                )
-            )
diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py
index 8a6fc9d6..8b19b292 100644
--- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py
+++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py
@@ -45,6 +45,10 @@ class MutationPruner(LaserPlugin):
         def mutator_hook(global_state: GlobalState):
             global_state.annotate(MutationAnnotation())
 
+        @symbolic_vm.pre_hook("CALL")
+        def mutator_hook(global_state: GlobalState):
+            global_state.annotate(MutationAnnotation())
+
         @symbolic_vm.laser_hook("add_world_state")
         def world_state_filter_hook(global_state: GlobalState):
             if And(

From 66c604b72c98799e7abb35aa82c0c37b429f3cb7 Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Thu, 8 Aug 2019 18:11:15 -0700
Subject: [PATCH 19/30] Fix invalid function names

---
 .../ethereum/plugins/implementations/dependency_pruner.py     | 2 +-
 .../laser/ethereum/plugins/implementations/mutation_pruner.py | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py
index b2b1ee16..bfff2c4d 100644
--- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py
+++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py
@@ -288,7 +288,7 @@ class DependencyPruner(LaserPlugin):
             self.storage_accessed_global.add(location)
 
         @symbolic_vm.pre_hook("CALL")
-        def stop_hook(state: GlobalState):
+        def call_hook(state: GlobalState):
             annotation = get_dependency_annotation(state)
 
             self.update_calls(annotation.path)
diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py
index 8b19b292..86755610 100644
--- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py
+++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py
@@ -42,11 +42,11 @@ class MutationPruner(LaserPlugin):
         """
 
         @symbolic_vm.pre_hook("SSTORE")
-        def mutator_hook(global_state: GlobalState):
+        def sstore_mutator_hook(global_state: GlobalState):
             global_state.annotate(MutationAnnotation())
 
         @symbolic_vm.pre_hook("CALL")
-        def mutator_hook(global_state: GlobalState):
+        def call_mutator_hook(global_state: GlobalState):
             global_state.annotate(MutationAnnotation())
 
         @symbolic_vm.laser_hook("add_world_state")

From 2eb94f3043b1348e27dc40ed57423515251f6be2 Mon Sep 17 00:00:00 2001
From: palkeo <contact@palkeo.com>
Date: Fri, 9 Aug 2019 17:38:52 +0200
Subject: [PATCH 20/30] Small cleanups (no semantic changes) (#1196)

* Small cleanups.

* Run black.
---
 mythril/analysis/modules/suicide.py                      | 6 ++----
 mythril/laser/ethereum/instructions.py                   | 8 +-------
 mythril/laser/ethereum/svm.py                            | 5 +++++
 mythril/laser/ethereum/transaction/transaction_models.py | 8 ++++++++
 4 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py
index 509b3137..b5a9b988 100644
--- a/mythril/analysis/modules/suicide.py
+++ b/mythril/analysis/modules/suicide.py
@@ -60,9 +60,7 @@ class SuicideModule(DetectionModule):
 
         to = state.mstate.stack[-1]
 
-        log.debug(
-            "[SUICIDE] SUICIDE in function " + state.environment.active_function_name
-        )
+        log.debug("SUICIDE in function %s", state.environment.active_function_name)
 
         description_head = "The contract can be killed by anyone."
 
@@ -103,7 +101,7 @@ class SuicideModule(DetectionModule):
             )
             return [issue]
         except UnsatError:
-            log.info("[UNCHECKED_SUICIDE] no model found")
+            log.debug("No model found")
 
         return []
 
diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 9020babc..5d2b9e93 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -198,6 +198,7 @@ class Instruction:
         """
         # Generalize some ops
         log.debug("Evaluating %s at %i", self.op_code, global_state.mstate.pc)
+
         op = self.op_code.lower()
         if self.op_code.startswith("PUSH"):
             op = "push"
@@ -783,15 +784,10 @@ class Instruction:
             log.debug("Unsupported symbolic calldata offset in CALLDATACOPY")
             dstart = simplify(op1)
 
-        size_sym = False
         try:
             size = util.get_concrete_int(op2)  # type: Union[int, BitVec]
         except TypeError:
             log.debug("Unsupported symbolic size in CALLDATACOPY")
-            size = simplify(op2)
-            size_sym = True
-
-        if size_sym:
             size = 320  # The excess size will get overwritten
 
         size = cast(int, size)
@@ -1397,7 +1393,6 @@ class Instruction:
 
         state = global_state.mstate
         index = state.stack.pop()
-
         state.stack.append(global_state.environment.active_account.storage[index])
         return [global_state]
 
@@ -1410,7 +1405,6 @@ class Instruction:
         """
         state = global_state.mstate
         index, value = state.stack.pop(), state.stack.pop()
-
         global_state.environment.active_account.storage[index] = value
         return [global_state]
 
diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py
index c9fc393c..88b362c8 100644
--- a/mythril/laser/ethereum/svm.py
+++ b/mythril/laser/ethereum/svm.py
@@ -257,6 +257,7 @@ class LaserEVM:
 
     def _add_world_state(self, global_state: GlobalState):
         """ Stores the world_state of the passed global state in the open states"""
+
         for hook in self._add_world_state_hooks:
             try:
                 hook(global_state)
@@ -325,6 +326,8 @@ class LaserEVM:
             new_global_state.node = global_state.node
             new_global_state.mstate.constraints = global_state.mstate.constraints
 
+            log.debug("Starting new transaction %s", start_signal.transaction)
+
             return [new_global_state], op_code
 
         except TransactionEndSignal as end_signal:
@@ -332,6 +335,8 @@ class LaserEVM:
                 -1
             ]
 
+            log.debug("Ending transaction %s.", transaction)
+
             if return_global_state is None:
                 if (
                     not isinstance(transaction, ContractCreationTransaction)
diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py
index bccdf7aa..c2b18b9c 100644
--- a/mythril/laser/ethereum/transaction/transaction_models.py
+++ b/mythril/laser/ethereum/transaction/transaction_models.py
@@ -134,6 +134,14 @@ class BaseTransaction:
     def initial_global_state(self) -> GlobalState:
         raise NotImplementedError
 
+    def __str__(self) -> str:
+        return "{} {} from {} to {:#42x}".format(
+            self.__class__.__name__,
+            self.id,
+            self.caller,
+            int(str(self.callee_account.address)) if self.callee_account else -1,
+        )
+
 
 class MessageCallTransaction(BaseTransaction):
     """Transaction object models an transaction."""

From 0281be777b278c99630b88dc85cb81cec36c63cd Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Fri, 9 Aug 2019 09:58:31 -0700
Subject: [PATCH 21/30] Fix onsite storage by using proper variables (#1194)

---
 mythril/laser/ethereum/state/account.py | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

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

From fa29f9b67ff1a02950625929097507d840a4bd4d Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Fri, 9 Aug 2019 18:39:14 -0700
Subject: [PATCH 22/30] Fix some ether problems and fix minimise (#1198)

---
 mythril/analysis/modules/ether_thief.py | 15 ++++++++++++++-
 mythril/analysis/solver.py              | 10 +---------
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py
index 87dd5be0..65e5c8e8 100644
--- a/mythril/analysis/modules/ether_thief.py
+++ b/mythril/analysis/modules/ether_thief.py
@@ -6,10 +6,15 @@ from copy import copy
 from mythril.analysis import solver
 from mythril.analysis.modules.base import DetectionModule
 from mythril.analysis.report import Issue
-from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
+from mythril.laser.ethereum.transaction.symbolic import (
+    ATTACKER_ADDRESS,
+    CREATOR_ADDRESS,
+)
 from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.transaction import ContractCreationTransaction
+
 from mythril.laser.smt import UGT, symbol_factory, UGE
 
 log = logging.getLogger(__name__)
@@ -82,6 +87,14 @@ class EtherThief(DetectionModule):
         that the Ether sent to the attacker's address is greater than the
         amount of Ether the attacker sent.
         """
+        for tx in state.world_state.transaction_sequence:
+            """
+            Constraint: All transactions must originate from regular users (not the creator/owner).
+            This prevents false positives where the owner willingly transfers ownership to another address.
+            """
+            if not isinstance(tx, ContractCreationTransaction):
+                constraints += [tx.caller != CREATOR_ADDRESS]
+
         attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256)
 
         constraints += [
diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 9504c71a..b6959a82 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -196,7 +196,7 @@ def _set_minimisation_constraints(
 
         # Minimize
         minimize.append(transaction.call_data.calldatasize)
-
+        minimize.append(transaction.call_value)
         constraints.append(
             UGE(
                 symbol_factory.BitVecVal(1000000000000000000000, 256),
@@ -204,14 +204,6 @@ def _set_minimisation_constraints(
             )
         )
 
-        # FIXME: This shouldn't be needed.
-        constraints.append(
-            UGE(
-                symbol_factory.BitVecVal(1000000000000000000000, 256),
-                transaction.call_value,
-            )
-        )
-
     for account in world_state.accounts.values():
         # Lazy way to prevent overflows and to ensure "reasonable" balances
         # Each account starts with less than 100 ETH

From b3d20d22a53278be4809023f374a456c06d0185d Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Fri, 9 Aug 2019 20:30:11 -0700
Subject: [PATCH 23/30] Version update

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

diff --git a/mythril/__version__.py b/mythril/__version__.py
index b7808215..8cb19bb6 100644
--- a/mythril/__version__.py
+++ b/mythril/__version__.py
@@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
 as for importing into Python.
 """
 
-__version__ = "v0.21.14"
+__version__ = "v0.21.15"

From 7a025fadeefb5538b6f2b6a87051dc04fc7f8a04 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Sun, 11 Aug 2019 18:22:42 -0700
Subject: [PATCH 24/30] Update the execution timeout for calls.sol test

---
 tests/laser/transaction/create_transaction_test.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/laser/transaction/create_transaction_test.py b/tests/laser/transaction/create_transaction_test.py
index 5c4e93ad..574dcc06 100644
--- a/tests/laser/transaction/create_transaction_test.py
+++ b/tests/laser/transaction/create_transaction_test.py
@@ -44,7 +44,7 @@ def test_sym_exec():
         contract,
         address=(util.get_indexed_address(0)),
         strategy="dfs",
-        execution_timeout=10,
+        execution_timeout=25,
     )
     issues = fire_lasers(sym)
 

From dcdceefd5d0f6976236f6a77056e10186b9e6e56 Mon Sep 17 00:00:00 2001
From: palkeo <contact@palkeo.com>
Date: Mon, 12 Aug 2019 23:17:50 +0200
Subject: [PATCH 25/30] Fix support for calls forwarding the entire calldata.
 (#1195)

* Fix support for calls forwarding the entire calldata.

* Reformat with black.

* uses_entire_calldata is always a Bool

* Revert "uses_entire_calldata is always a Bool"

This reverts commit 629cb531722cb73661353ccc2a1eb64af0c857d7.

* Revert "Revert "uses_entire_calldata is always a Bool""

Didn't help, it passed before. Strange. Will need to find a way to
investigate locally.
---
 mythril/laser/ethereum/call.py | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py
index 2e471037..bc1c360c 100644
--- a/mythril/laser/ethereum/call.py
+++ b/mythril/laser/ethereum/call.py
@@ -16,7 +16,7 @@ from mythril.laser.ethereum.state.calldata import (
     ConcreteCalldata,
 )
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import BitVec
+from mythril.laser.smt import BitVec, Bool, is_true
 from mythril.laser.smt import simplify, Expression, symbol_factory
 from mythril.support.loader import DynLoader
 
@@ -197,10 +197,10 @@ def get_call_data(
     )
 
     uses_entire_calldata = simplify(
-        memory_size - global_state.environment.calldata.calldatasize == 0
+        memory_size == global_state.environment.calldata.calldatasize
     )
 
-    if uses_entire_calldata is True:
+    if is_true(uses_entire_calldata):
         return global_state.environment.calldata
 
     try:
@@ -211,7 +211,9 @@ def get_call_data(
         ]
         return ConcreteCalldata(transaction_id, calldata_from_mem)
     except TypeError:
-        log.debug("Unsupported symbolic calldata offset")
+        log.debug(
+            "Unsupported symbolic calldata offset %s size %s", memory_start, memory_size
+        )
         return SymbolicCalldata(transaction_id)
 
 

From 42fec0c77095202987da11fa117ad211c93d67b5 Mon Sep 17 00:00:00 2001
From: Bernhard Mueller <bernhard.mueller11@gmail.com>
Date: Wed, 14 Aug 2019 09:49:31 +0200
Subject: [PATCH 26/30] Change actor addresses in line with MythX test case
 conventions

---
 mythril/laser/ethereum/transaction/symbolic.py | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py
index 1a895048..16e0d54f 100644
--- a/mythril/laser/ethereum/transaction/symbolic.py
+++ b/mythril/laser/ethereum/transaction/symbolic.py
@@ -21,9 +21,10 @@ CREATOR_ADDRESS = 0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE
 ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
 
 ACTOR_ADDRESSES = [
-    symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256),
-    symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256),
-    symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEE, 256),
+    symbol_factory.BitVecVal(0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, 256),
+    symbol_factory.BitVecVal(0xBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBB, 256),
+    symbol_factory.BitVecVal(0xCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCC, 256),
+    symbol_factory.BitVecVal(0xDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDD, 256),
 ]
 
 

From 106bf49fda9dce41a6c5283792b5d65544e8b424 Mon Sep 17 00:00:00 2001
From: Bernhard Mueller <bernhard.mueller11@gmail.com>
Date: Wed, 14 Aug 2019 19:52:44 +0200
Subject: [PATCH 27/30] Reduce number of actors

---
 mythril/laser/ethereum/transaction/symbolic.py | 1 -
 1 file changed, 1 deletion(-)

diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py
index 16e0d54f..99bb7252 100644
--- a/mythril/laser/ethereum/transaction/symbolic.py
+++ b/mythril/laser/ethereum/transaction/symbolic.py
@@ -24,7 +24,6 @@ ACTOR_ADDRESSES = [
     symbol_factory.BitVecVal(0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, 256),
     symbol_factory.BitVecVal(0xBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBB, 256),
     symbol_factory.BitVecVal(0xCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCC, 256),
-    symbol_factory.BitVecVal(0xDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDD, 256),
 ]
 
 

From 48216680872db5cfff8c30ba0840b82cf35be735 Mon Sep 17 00:00:00 2001
From: Bernhard Mueller <bernhard.mueller11@gmail.com>
Date: Thu, 15 Aug 2019 12:14:16 +0200
Subject: [PATCH 28/30] Fix standard actors list

---
 mythril/laser/ethereum/transaction/symbolic.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py
index 99bb7252..2212e805 100644
--- a/mythril/laser/ethereum/transaction/symbolic.py
+++ b/mythril/laser/ethereum/transaction/symbolic.py
@@ -21,9 +21,9 @@ CREATOR_ADDRESS = 0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE
 ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
 
 ACTOR_ADDRESSES = [
+    symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256),
+    symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256),
     symbol_factory.BitVecVal(0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, 256),
-    symbol_factory.BitVecVal(0xBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBBB, 256),
-    symbol_factory.BitVecVal(0xCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCC, 256),
 ]
 
 

From c8d91b6f417e1db94269f651defba8cad5c25a72 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Wed, 21 Aug 2019 17:45:19 +0530
Subject: [PATCH 29/30] Add the rest of the precompiles (#990)

* Support modular exponentiation for concrete data

* Add elliptic curve operations

* Fix type hints and refactor code

* Support usage of the rest of the native contracts

* Remove unused imports

* Add tests for elliptic curve functions

* Use a constant for native functions count

* Update py_ecc version

* Use PRECOMPILE_COUNT over hardcoded value

* Use shortened list comprehensives

* Clean up imports

* Use precompile count in checking precompile calls

* Refactor code
---
 mythril/analysis/call_helpers.py              |   3 +-
 mythril/analysis/modules/external_calls.py    |   3 +-
 mythril/analysis/symbolic.py                  |   6 +-
 mythril/laser/ethereum/call.py                |  13 +-
 mythril/laser/ethereum/natives.py             | 168 +++++++++++++-----
 mythril/laser/ethereum/util.py                |  24 +++
 requirements.txt                              |   2 +-
 setup.py                                      |   2 +-
 tests/laser/Precompiles/test_ec_add.py        |  27 +++
 .../laser/Precompiles/test_elliptic_curves.py |  35 ++++
 tests/laser/Precompiles/test_elliptic_mul.py  |  27 +++
 tests/laser/Precompiles/test_mod_exp.py       |  61 +++++++
 12 files changed, 321 insertions(+), 50 deletions(-)
 create mode 100644 tests/laser/Precompiles/test_ec_add.py
 create mode 100644 tests/laser/Precompiles/test_elliptic_curves.py
 create mode 100644 tests/laser/Precompiles/test_elliptic_mul.py
 create mode 100644 tests/laser/Precompiles/test_mod_exp.py

diff --git a/mythril/analysis/call_helpers.py b/mythril/analysis/call_helpers.py
index 6cb796df..270ff5af 100644
--- a/mythril/analysis/call_helpers.py
+++ b/mythril/analysis/call_helpers.py
@@ -4,6 +4,7 @@ from typing import Union
 
 from mythril.analysis.ops import VarType, Call, get_variable
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 
 
 def get_call_from_state(state: GlobalState) -> Union[Call, None]:
@@ -28,7 +29,7 @@ def get_call_from_state(state: GlobalState) -> Union[Call, None]:
             get_variable(stack[-7]),
         )
 
-        if to.type == VarType.CONCRETE and 0 < to.val < 5:
+        if to.type == VarType.CONCRETE and 0 < to.val <= PRECOMPILE_COUNT:
             return None
 
         if meminstart.type == VarType.CONCRETE and meminsz.type == VarType.CONCRETE:
diff --git a/mythril/analysis/modules/external_calls.py b/mythril/analysis/modules/external_calls.py
index e80c8802..81cd6bd2 100644
--- a/mythril/analysis/modules/external_calls.py
+++ b/mythril/analysis/modules/external_calls.py
@@ -10,6 +10,7 @@ from mythril.laser.ethereum.transaction.transaction_models import (
 from mythril.analysis.modules.base import DetectionModule
 from mythril.analysis.report import Issue
 from mythril.laser.smt import UGT, symbol_factory, Or, BitVec
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.exceptions import UnsatError
 from copy import copy
@@ -33,7 +34,7 @@ def _is_precompile_call(global_state: GlobalState):
     constraints += [
         Or(
             to < symbol_factory.BitVecVal(1, 256),
-            to > symbol_factory.BitVecVal(16, 256),
+            to > symbol_factory.BitVecVal(PRECOMPILE_COUNT, 256),
         )
     ]
 
diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py
index 02b5c8ca..ce98b0ce 100644
--- a/mythril/analysis/symbolic.py
+++ b/mythril/analysis/symbolic.py
@@ -14,6 +14,7 @@ from mythril.laser.ethereum.strategy.basic import (
     BasicSearchStrategy,
 )
 
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 from mythril.laser.ethereum.transaction.symbolic import (
     ATTACKER_ADDRESS,
     CREATOR_ADDRESS,
@@ -212,7 +213,10 @@ class SymExecWrapper:
                             get_variable(stack[-7]),
                         )
 
-                        if to.type == VarType.CONCRETE and to.val < 5:
+                        if (
+                            to.type == VarType.CONCRETE
+                            and 0 < to.val <= PRECOMPILE_COUNT
+                        ):
                             # ignore prebuilts
                             continue
 
diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py
index bc1c360c..24a8e2f3 100644
--- a/mythril/laser/ethereum/call.py
+++ b/mythril/laser/ethereum/call.py
@@ -10,13 +10,14 @@ import mythril.laser.ethereum.util as util
 from mythril.laser.ethereum import natives
 from mythril.laser.ethereum.gas import OPCODE_GAS
 from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 from mythril.laser.ethereum.state.calldata import (
     BaseCalldata,
     SymbolicCalldata,
     ConcreteCalldata,
 )
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import BitVec, Bool, is_true
+from mythril.laser.smt import BitVec, is_true
 from mythril.laser.smt import simplify, Expression, symbol_factory
 from mythril.support.loader import DynLoader
 
@@ -51,7 +52,7 @@ def get_call_parameters(
     call_data = get_call_data(global_state, memory_input_offset, memory_input_size)
     if (
         isinstance(callee_address, BitVec)
-        or int(callee_address, 16) >= 5
+        or int(callee_address, 16) > PRECOMPILE_COUNT
         or int(callee_address, 16) == 0
     ):
         callee_account = get_callee_account(
@@ -223,8 +224,12 @@ def native_call(
     call_data: BaseCalldata,
     memory_out_offset: Union[int, Expression],
     memory_out_size: Union[int, Expression],
-) -> Union[List[GlobalState], None]:
-    if isinstance(callee_address, BitVec) or not 0 < int(callee_address, 16) < 5:
+) -> Optional[List[GlobalState]]:
+
+    if (
+        isinstance(callee_address, BitVec)
+        or not 0 < int(callee_address, 16) <= PRECOMPILE_COUNT
+    ):
         return None
 
     log.debug("Native contract called: " + callee_address)
diff --git a/mythril/laser/ethereum/natives.py b/mythril/laser/ethereum/natives.py
index ef38d8c9..991a172c 100644
--- a/mythril/laser/ethereum/natives.py
+++ b/mythril/laser/ethereum/natives.py
@@ -6,12 +6,20 @@ from typing import List, Union
 
 from ethereum.utils import ecrecover_to_pub
 from py_ecc.secp256k1 import N as secp256k1n
+import py_ecc.optimized_bn128 as bn128
 from rlp.utils import ALL_BYTES
 
 from mythril.laser.ethereum.state.calldata import BaseCalldata, ConcreteCalldata
-from mythril.laser.ethereum.util import bytearray_to_int
-from ethereum.utils import sha3
-from mythril.laser.smt import Concat, simplify
+from mythril.laser.ethereum.util import extract_copy, extract32
+from ethereum.utils import (
+    sha3,
+    big_endian_to_int,
+    safe_ord,
+    zpad,
+    int_to_big_endian,
+    encode_int32,
+)
+from ethereum.specials import validate_point
 
 log = logging.getLogger(__name__)
 
@@ -22,35 +30,6 @@ class NativeContractException(Exception):
     pass
 
 
-def int_to_32bytes(
-    i: int
-) -> bytes:  # used because int can't fit as bytes function's input
-    """
-
-    :param i:
-    :return:
-    """
-    o = [0] * 32
-    for x in range(32):
-        o[31 - x] = i & 0xFF
-        i >>= 8
-    return bytes(o)
-
-
-def extract32(data: bytearray, i: int) -> int:
-    """
-
-    :param data:
-    :param i:
-    :return:
-    """
-    if i >= len(data):
-        return 0
-    o = data[i : min(i + 32, len(data))]
-    o.extend(bytearray(32 - len(o)))
-    return bytearray_to_int(o)
-
-
 def ecrecover(data: List[int]) -> List[int]:
     """
 
@@ -59,14 +38,14 @@ def ecrecover(data: List[int]) -> List[int]:
     """
     # TODO: Add type hints
     try:
-        byte_data = bytearray(data)
-        v = extract32(byte_data, 32)
-        r = extract32(byte_data, 64)
-        s = extract32(byte_data, 96)
+        bytes_data = bytearray(data)
+        v = extract32(bytes_data, 32)
+        r = extract32(bytes_data, 64)
+        s = extract32(bytes_data, 96)
     except TypeError:
         raise NativeContractException
 
-    message = b"".join([ALL_BYTES[x] for x in byte_data[0:32]])
+    message = b"".join([ALL_BYTES[x] for x in bytes_data[0:32]])
     if r >= secp256k1n or s >= secp256k1n or v < 27 or v > 28:
         return []
     try:
@@ -85,10 +64,10 @@ def sha256(data: List[int]) -> List[int]:
     :return:
     """
     try:
-        byte_data = bytes(data)
+        bytes_data = bytes(data)
     except TypeError:
         raise NativeContractException
-    return list(bytearray(hashlib.sha256(byte_data).digest()))
+    return list(bytearray(hashlib.sha256(bytes_data).digest()))
 
 
 def ripemd160(data: List[int]) -> List[int]:
@@ -120,6 +99,114 @@ def identity(data: List[int]) -> List[int]:
     return data
 
 
+def mod_exp(data: List[int]) -> List[int]:
+    """
+    TODO: Some symbolic parts can be handled here
+    Modular Exponentiation
+    :param data: Data with <length_of_BASE> <length_of_EXPONENT> <length_of_MODULUS> <BASE> <EXPONENT> <MODULUS>
+    :return: modular exponentiation
+    """
+    bytes_data = bytearray(data)
+    baselen = extract32(bytes_data, 0)
+    explen = extract32(bytes_data, 32)
+    modlen = extract32(bytes_data, 64)
+    if baselen == 0:
+        return [0] * modlen
+    if modlen == 0:
+        return []
+
+    first_exp_bytes = extract32(bytes_data, 96 + baselen) >> (8 * max(32 - explen, 0))
+    bitlength = -1
+    while first_exp_bytes:
+        bitlength += 1
+        first_exp_bytes >>= 1
+
+    base = bytearray(baselen)
+    extract_copy(bytes_data, base, 0, 96, baselen)
+    exp = bytearray(explen)
+    extract_copy(bytes_data, exp, 0, 96 + baselen, explen)
+    mod = bytearray(modlen)
+    extract_copy(bytes_data, mod, 0, 96 + baselen + explen, modlen)
+    if big_endian_to_int(mod) == 0:
+        return [0] * modlen
+    o = pow(big_endian_to_int(base), big_endian_to_int(exp), big_endian_to_int(mod))
+    return [safe_ord(x) for x in zpad(int_to_big_endian(o), modlen)]
+
+
+def ec_add(data: List[int]) -> List[int]:
+    bytes_data = bytearray(data)
+    x1 = extract32(bytes_data, 0)
+    y1 = extract32(bytes_data, 32)
+    x2 = extract32(bytes_data, 64)
+    y2 = extract32(bytes_data, 96)
+    p1 = validate_point(x1, y1)
+    p2 = validate_point(x2, y2)
+    if p1 is False or p2 is False:
+        return []
+    o = bn128.normalize(bn128.add(p1, p2))
+    return [safe_ord(x) for x in (encode_int32(o[0].n) + encode_int32(o[1].n))]
+
+
+def ec_mul(data: List[int]) -> List[int]:
+    bytes_data = bytearray(data)
+    x = extract32(bytes_data, 0)
+    y = extract32(bytes_data, 32)
+    m = extract32(bytes_data, 64)
+    p = validate_point(x, y)
+    if p is False:
+        return []
+    o = bn128.normalize(bn128.multiply(p, m))
+    return [safe_ord(c) for c in (encode_int32(o[0].n) + encode_int32(o[1].n))]
+
+
+def ec_pair(data: List[int]) -> List[int]:
+    if len(data) % 192:
+        return []
+
+    zero = (bn128.FQ2.one(), bn128.FQ2.one(), bn128.FQ2.zero())
+    exponent = bn128.FQ12.one()
+    bytes_data = bytearray(data)
+    for i in range(0, len(bytes_data), 192):
+        x1 = extract32(bytes_data, i)
+        y1 = extract32(bytes_data, i + 32)
+        x2_i = extract32(bytes_data, i + 64)
+        x2_r = extract32(bytes_data, i + 96)
+        y2_i = extract32(bytes_data, i + 128)
+        y2_r = extract32(bytes_data, i + 160)
+        p1 = validate_point(x1, y1)
+        if p1 is False:
+            return []
+        for v in (x2_i, x2_r, y2_i, y2_r):
+            if v >= bn128.field_modulus:
+                return []
+        fq2_x = bn128.FQ2([x2_r, x2_i])
+        fq2_y = bn128.FQ2([y2_r, y2_i])
+        if (fq2_x, fq2_y) != (bn128.FQ2.zero(), bn128.FQ2.zero()):
+            p2 = (fq2_x, fq2_y, bn128.FQ2.one())
+            if not bn128.is_on_curve(p2, bn128.b2):
+                return []
+        else:
+            p2 = zero
+        if bn128.multiply(p2, bn128.curve_order)[-1] != bn128.FQ2.zero():
+            return []
+        exponent *= bn128.pairing(p2, p1, final_exponentiate=False)
+    result = bn128.final_exponentiate(exponent) == bn128.FQ12.one()
+    return [0] * 31 + [1 if result else 0]
+
+
+PRECOMPILE_FUNCTIONS = (
+    ecrecover,
+    sha256,
+    ripemd160,
+    identity,
+    mod_exp,
+    ec_add,
+    ec_mul,
+    ec_pair,
+)
+PRECOMPILE_COUNT = len(PRECOMPILE_FUNCTIONS)
+
+
 def native_contracts(address: int, data: BaseCalldata) -> List[int]:
     """Takes integer address 1, 2, 3, 4.
 
@@ -127,11 +214,10 @@ def native_contracts(address: int, data: BaseCalldata) -> List[int]:
     :param data:
     :return:
     """
-    functions = (ecrecover, sha256, ripemd160, identity)
 
     if isinstance(data, ConcreteCalldata):
         concrete_data = data.concrete(None)
     else:
         raise NativeContractException()
 
-    return functions[address - 1](concrete_data)
+    return PRECOMPILE_FUNCTIONS[address - 1](concrete_data)
diff --git a/mythril/laser/ethereum/util.py b/mythril/laser/ethereum/util.py
index 9cb5d950..4191173d 100644
--- a/mythril/laser/ethereum/util.py
+++ b/mythril/laser/ethereum/util.py
@@ -150,3 +150,27 @@ def bytearray_to_int(arr):
     for a in arr:
         o = (o << 8) + a
     return o
+
+
+def extract_copy(
+    data: bytearray, mem: bytearray, memstart: int, datastart: int, size: int
+):
+    for i in range(size):
+        if datastart + i < len(data):
+            mem[memstart + i] = data[datastart + i]
+        else:
+            mem[memstart + i] = 0
+
+
+def extract32(data: bytearray, i: int) -> int:
+    """
+
+    :param data:
+    :param i:
+    :return:
+    """
+    if i >= len(data):
+        return 0
+    o = data[i : min(i + 32, len(data))]
+    o.extend(bytearray(32 - len(o)))
+    return bytearray_to_int(o)
diff --git a/requirements.txt b/requirements.txt
index 11382df3..6901873e 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -1,7 +1,7 @@
 coloredlogs>=10.0
 configparser>=3.5.0
 coverage
-py_ecc==1.4.2
+py_ecc==1.6.0
 eth_abi==1.3.0
 eth-account>=0.1.0a2,<=0.3.0
 ethereum>=2.3.2
diff --git a/setup.py b/setup.py
index ce115193..bee87da0 100755
--- a/setup.py
+++ b/setup.py
@@ -25,7 +25,7 @@ REQUIRES_PYTHON = ">=3.5.0"
 # What packages are required for this module to be executed?
 REQUIRED = [
     "coloredlogs>=10.0",
-    "py_ecc==1.4.2",
+    "py_ecc==1.6.0",
     "ethereum>=2.3.2",
     "z3-solver>=4.8.5.0",
     "requests",
diff --git a/tests/laser/Precompiles/test_ec_add.py b/tests/laser/Precompiles/test_ec_add.py
new file mode 100644
index 00000000..4ede2cf0
--- /dev/null
+++ b/tests/laser/Precompiles/test_ec_add.py
@@ -0,0 +1,27 @@
+from mock import patch
+from eth_utils import decode_hex
+from mythril.laser.ethereum.natives import ec_add
+from py_ecc.optimized_bn128 import FQ
+
+VECTOR_A = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+
+def test_ec_add_sanity():
+    assert ec_add(VECTOR_A) == []
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.add", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.normalize")
+def test_ec_add(f1, f2, f3):
+    FQ.fielf_modulus = 128
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    assert ec_add(VECTOR_A) == ([0] * 31 + [1]) * 2
diff --git a/tests/laser/Precompiles/test_elliptic_curves.py b/tests/laser/Precompiles/test_elliptic_curves.py
new file mode 100644
index 00000000..28908f58
--- /dev/null
+++ b/tests/laser/Precompiles/test_elliptic_curves.py
@@ -0,0 +1,35 @@
+from mock import patch
+from mythril.laser.ethereum.natives import ec_pair
+from py_ecc.optimized_bn128 import FQ
+
+
+def test_ec_pair_192_check():
+    vec_c = [0] * 100
+    assert ec_pair(vec_c) == []
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.is_on_curve", return_value=True)
+@patch("mythril.laser.ethereum.natives.bn128.pairing", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.normalize")
+def test_ec_pair(f1, f2, f3, f4):
+    FQ.fielf_modulus = 100
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    vec_c = [0] * 192
+    assert ec_pair(vec_c) == [0] * 31 + [1]
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=False)
+def test_ec_pair_point_validation_failure(f1):
+    vec_c = [0] * 192
+    assert ec_pair(vec_c) == []
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+def test_ec_pair_field_exceed_mod(f1):
+    FQ.fielf_modulus = 100
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    vec_c = [10] * 192
+    assert ec_pair(vec_c) == []
diff --git a/tests/laser/Precompiles/test_elliptic_mul.py b/tests/laser/Precompiles/test_elliptic_mul.py
new file mode 100644
index 00000000..c3b3be9d
--- /dev/null
+++ b/tests/laser/Precompiles/test_elliptic_mul.py
@@ -0,0 +1,27 @@
+from mock import patch
+from eth_utils import decode_hex
+from mythril.laser.ethereum.natives import ec_mul
+from py_ecc.optimized_bn128 import FQ
+
+VECTOR_A = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.multiply", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.normalize")
+def test_ec_mul(f1, f2, f3):
+    FQ.fielf_modulus = 128
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    assert ec_mul(VECTOR_A) == ([0] * 31 + [1]) * 2
+
+
+def test_ec_mul_validation_failure():
+    assert ec_mul(VECTOR_A) == []
diff --git a/tests/laser/Precompiles/test_mod_exp.py b/tests/laser/Precompiles/test_mod_exp.py
new file mode 100644
index 00000000..d050c929
--- /dev/null
+++ b/tests/laser/Precompiles/test_mod_exp.py
@@ -0,0 +1,61 @@
+import pytest
+from eth_utils import decode_hex
+from mythril.laser.ethereum.natives import mod_exp
+from ethereum.utils import big_endian_to_int
+
+
+EIP198_VECTOR_A = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+EIP198_VECTOR_B = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000000"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+EIP198_VECTOR_C = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000002"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "ffff"
+    "8000000000000000000000000000000000000000000000000000000000000000"
+    "07"
+)
+
+EIP198_VECTOR_D = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000002"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "ffff"
+    "80"
+)
+
+
+@pytest.mark.parametrize(
+    "data,expected",
+    (
+        (EIP198_VECTOR_A, 1),
+        (EIP198_VECTOR_B, 0),
+        (
+            EIP198_VECTOR_C,
+            26689440342447178617115869845918039756797228267049433585260346420242739014315,
+        ),
+        (
+            EIP198_VECTOR_D,
+            26689440342447178617115869845918039756797228267049433585260346420242739014315,
+        ),
+    ),
+)
+def test_modexp_result(data, expected):
+    actual = mod_exp(data)
+    assert big_endian_to_int(actual) == expected

From 00dc912f2c12d0bdb4cb66292bda715bcaec5fa2 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Mon, 26 Aug 2019 12:16:48 +0530
Subject: [PATCH 30/30] Refactor the cli and add help for the contract
 selection (#1203)

---
 mythril/interfaces/cli.py | 27 +++++++++++++++++++++------
 1 file changed, 21 insertions(+), 6 deletions(-)

diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py
index 2cbf3f4c..5b78ba38 100644
--- a/mythril/interfaces/cli.py
+++ b/mythril/interfaces/cli.py
@@ -15,7 +15,7 @@ import coloredlogs
 import traceback
 
 import mythril.support.signatures as sigs
-from argparse import ArgumentParser, Namespace
+from argparse import ArgumentParser, Namespace, RawTextHelpFormatter
 from mythril.exceptions import AddressNotFoundError, CriticalError
 from mythril.mythril import (
     MythrilAnalyzer,
@@ -174,6 +174,7 @@ def main() -> None:
         help="Triggers the analysis of the smart contract",
         parents=[rpc_parser, utilities_parser, input_parser, output_parser],
         aliases=ANALYZE_LIST[1:],
+        formatter_class=RawTextHelpFormatter,
     )
     create_analyzer_parser(analyzer_parser)
 
@@ -182,6 +183,7 @@ def main() -> None:
         help="Disassembles the smart contract",
         aliases=DISASSEMBLE_LIST[1:],
         parents=[rpc_parser, utilities_parser, input_parser],
+        formatter_class=RawTextHelpFormatter,
     )
     create_disassemble_parser(disassemble_parser)
 
@@ -223,7 +225,13 @@ def create_disassemble_parser(parser: ArgumentParser):
     :param parser:
     :return:
     """
-    parser.add_argument("solidity_file", nargs="*")
+    # Using nargs=* would the implementation below for getting code for both disassemble and analyze
+    parser.add_argument(
+        "solidity_files",
+        nargs="*",
+        help="Inputs file name and contract name. Currently supports a single contract\n"
+        "usage: file1.sol:OptionalContractName",
+    )
 
 
 def create_read_storage_parser(read_storage_parser: ArgumentParser):
@@ -290,7 +298,12 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
     :param analyzer_parser:
     :return:
     """
-    analyzer_parser.add_argument("solidity_file", nargs="*")
+    analyzer_parser.add_argument(
+        "solidity_files",
+        nargs="*",
+        help="Inputs file name and contract name. \n"
+        "usage: file1.sol:OptionalContractName file2.sol file3.sol:OptionalContractName",
+    )
     commands = analyzer_parser.add_argument_group("commands")
     commands.add_argument("-g", "--graph", help="generate a control flow graph")
     commands.add_argument(
@@ -425,6 +438,8 @@ def validate_args(args: Namespace):
             exit_with_error(
                 args.outform, "Invalid -v value, you can find valid values in usage"
             )
+    if args.command in DISASSEMBLE_LIST and len(args.solidity_files) > 1:
+        exit_with_error("text", "Only a single arg is supported for using disassemble")
 
     if args.command in ANALYZE_LIST:
         if args.query_signature and sigs.ethereum_input_decoder is None:
@@ -509,15 +524,15 @@ def load_code(disassembler: MythrilDisassembler, args: Namespace):
     elif args.__dict__.get("address", False):
         # Get bytecode from a contract address
         address, _ = disassembler.load_from_address(args.address)
-    elif args.__dict__.get("solidity_file", False):
+    elif args.__dict__.get("solidity_files", False):
         # Compile Solidity source file(s)
-        if args.command in ANALYZE_LIST and args.graph and len(args.solidity_file) > 1:
+        if args.command in ANALYZE_LIST and args.graph and len(args.solidity_files) > 1:
             exit_with_error(
                 args.outform,
                 "Cannot generate call graphs from multiple input files. Please do it one at a time.",
             )
         address, _ = disassembler.load_from_solidity(
-            args.solidity_file
+            args.solidity_files
         )  # list of files
     else:
         exit_with_error(