Concolic tool (#1445)

* Mythril v0.22.14

* Add trace plugin and find trace

* Add finding trace

* Add some changes

* change help text

* Add some comments

* Add support for concolic strategy

* Fix issues

* Add concolic exec tool

* Add a few fixes

* Fix a few errors

* Add tests

* Fix test interface

* Add muti flip test

* Add multi contract test

* Fix cases with multicontract calls

* Add more tests and fixes

* Fix tests

* Fix mypy

* Change tests and other small fixes

* Add more documentation

* Add some changes

* Update mythril/concolic/find_trace.py

Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>

* Remove space

Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>

* Fix typing

* Fix Review issues

* Change test type

* Remove deepcopy

* Use 3.8 for typing

* Use typing_extensions

* Fix prev_state

* Add changes to tests and fix some bugs

* Fix address assignment

* Fix issues and format

* Remove set_option

* Split plugins

* Refactor

Co-authored-by: JoranHonig <JoranHonig@users.noreply.github.com>

mythril/analysis/solver.py

@@ -1,8 +1,10 @@
 """This module contains analysis module helpers to solve path constraints."""
-import logging
+
-from typing import Dict, List, Tuple, Union
+from typing import Dict, List, Tuple, Union, Any
 
 import z3
+import logging
+
 from z3 import FuncInterp
 
 from mythril.exceptions import UnsatError
@@ -48,8 +50,10 @@ def pretty_print_model(model):
 
 def get_transaction_sequence(
     global_state: GlobalState, constraints: Constraints
-) -> Dict:
+) -> Dict[str, Any]:
     """Generate concrete transaction sequence.
+    Note: This function only considers the constraints in constraint argument,
+    which in some cases is expected to differ from global_state's constraints
 
     :param global_state: GlobalState to generate transaction sequence for
     :param constraints: list of constraints used to generate transaction sequence
@@ -66,16 +70,19 @@ def get_transaction_sequence(
         model = get_model(tx_constraints, minimize=minimize)
     except UnsatError:
         raise UnsatError
-    # Include creation account in initial state
+
-    # Note: This contains the code, which should not exist until after the first tx
+    if isinstance(transaction_sequence[0], ContractCreationTransaction):
-    initial_world_state = transaction_sequence[0].world_state
+        initial_world_state = transaction_sequence[0].prev_world_state
+    else:
+        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)
 
-    min_price_dict = {}  # type: Dict[str, int]
+    min_price_dict: Dict[str, int] = {}
     for address in initial_accounts.keys():
         min_price_dict[address] = model.eval(
             initial_world_state.starting_balances[
@@ -159,13 +166,15 @@ def _replace_with_actual_sha(
             )
 
 
-def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]):
+def _get_concrete_state(
+    initial_accounts: Dict, min_price_dict: Dict[str, int]
+) -> Dict[str, Dict]:
     """Gets a concrete state"""
     accounts = {}
     for address, account in initial_accounts.items():
         # Skip empty default account
 
-        data = dict()  # type: Dict[str, Union[int, str]]
+        data: Dict[str, Union[int, str]] = {}
         data["nonce"] = account.nonce
         data["code"] = account.serialised_code()
         data["storage"] = str(account.storage)

mythril/concolic/__init__.py

@@ -0,0 +1,2 @@
+from mythril.concolic.concolic_execution import concolic_execution
+from mythril.concolic.find_trace import concrete_execution

mythril/concolic/concolic_execution.py

@@ -0,0 +1,85 @@
+import json
+import binascii
+
+from datetime import datetime, timedelta
+from typing import Dict, List, Any
+from copy import deepcopy
+
+from mythril.concolic.concrete_data import ConcreteData
+from mythril.concolic.find_trace import concrete_execution
+from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.ethereum.strategy.concolic import ConcolicStrategy
+from mythril.laser.ethereum.svm import LaserEVM
+from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.transaction.symbolic import execute_transaction
+from mythril.laser.ethereum.transaction.transaction_models import tx_id_manager
+from mythril.laser.smt import Expression, BitVec, symbol_factory
+from mythril.laser.ethereum.time_handler import time_handler
+from mythril.support.support_args import args
+
+
+def flip_branches(
+    init_state: WorldState,
+    concrete_data: ConcreteData,
+    jump_addresses: List[str],
+    trace: List,
+) -> List[Dict[str, Dict[str, Any]]]:
+    """
+    Flips branches and prints the input required for branch flip
+
+    :param concrete_data: Concrete data
+    :param jump_addresses: Jump addresses to flip
+    :param trace: trace to follow
+    """
+    tx_id_manager.restart_counter()
+    output_list = []
+    laser_evm = LaserEVM(
+        execution_timeout=600, use_reachability_check=False, transaction_count=10
+    )
+    laser_evm.open_states = [deepcopy(init_state)]
+    laser_evm.strategy = ConcolicStrategy(
+        work_list=laser_evm.work_list,
+        max_depth=100,
+        trace=trace,
+        flip_branch_addresses=jump_addresses,
+    )
+
+    time_handler.start_execution(laser_evm.execution_timeout)
+    laser_evm.time = datetime.now()
+
+    for transaction in concrete_data["steps"]:
+        execute_transaction(
+            laser_evm,
+            callee_address=transaction["address"],
+            caller_address=symbol_factory.BitVecVal(
+                int(transaction["origin"], 16), 256
+            ),
+            data=transaction["input"][2:],
+        )
+
+    if laser_evm.strategy.results:
+        for addr in jump_addresses:
+            output_list.append(laser_evm.strategy.results[addr])
+    return output_list
+
+
+def concolic_execution(
+    concrete_data: ConcreteData, jump_addresses: List, solver_timeout=100000
+) -> List[Dict[str, Dict[str, Any]]]:
+    """
+    Executes codes and prints input required to cover the branch flips
+    :param input_file: Input file
+    :param jump_addresses: Jump addresses to flip
+    :param solver_timeout: Solver timeout
+
+    """
+    init_state, trace = concrete_execution(concrete_data)
+    args.solver_timeout = solver_timeout
+    output_list = flip_branches(
+        init_state=init_state,
+        concrete_data=concrete_data,
+        jump_addresses=jump_addresses,
+        trace=trace,
+    )
+    return output_list

mythril/concolic/concrete_data.py

@@ -0,0 +1,34 @@
+from typing import Dict, List
+from typing_extensions import TypedDict
+
+
+class AccountData(TypedDict):
+    balance: str
+    code: str
+    nonce: int
+    storage: dict
+
+
+class InitialState(TypedDict):
+    accounts: Dict[str, AccountData]
+
+
+class TransactionData(TypedDict):
+    address: str
+    blockCoinbase: str
+    blockDifficulty: str
+    blockGasLimit: str
+    blockNumber: str
+    blockTime: str
+    calldata: str
+    gasLimit: str
+    gasPrice: str
+    input: str
+    name: str
+    origin: str
+    value: str
+
+
+class ConcreteData(TypedDict):
+    initialState: InitialState
+    steps: List[TransactionData]

mythril/concolic/find_trace.py

@@ -0,0 +1,78 @@
+import json
+import binascii
+
+from copy import deepcopy
+from datetime import datetime
+from typing import Dict, List, Tuple
+
+from mythril.concolic.concrete_data import ConcreteData
+
+from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.ethereum.svm import LaserEVM
+from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.transaction.concolic import execute_transaction
+from mythril.laser.plugin.loader import LaserPluginLoader
+from mythril.laser.smt import Expression, BitVec, symbol_factory
+from mythril.laser.ethereum.transaction.transaction_models import tx_id_manager
+from mythril.plugin.discovery import PluginDiscovery
+
+
+def setup_concrete_initial_state(concrete_data: ConcreteData) -> WorldState:
+    """
+    Sets up concrete initial state
+    :param concrete_data: Concrete data
+    :return: initialised world state
+    """
+    world_state = WorldState()
+    for address, details in concrete_data["initialState"]["accounts"].items():
+        account = Account(address, concrete_storage=True)
+        account.code = Disassembly(details["code"][2:])
+        account.nonce = details["nonce"]
+        if type(details["storage"]) == str:
+            details["storage"] = eval(details["storage"])  # type: ignore
+        for key, value in details["storage"].items():
+            key_bitvec = symbol_factory.BitVecVal(int(key, 16), 256)
+            account.storage[key_bitvec] = symbol_factory.BitVecVal(int(value, 16), 256)
+
+        world_state.put_account(account)
+        account.set_balance(int(details["balance"], 16))
+    return world_state
+
+
+def concrete_execution(concrete_data: ConcreteData) -> Tuple[WorldState, List]:
+    """
+    Executes code concretely to find the path to be followed by concolic executor
+    :param concrete_data: Concrete data
+    :return: path trace
+    """
+    tx_id_manager.restart_counter()
+    init_state = setup_concrete_initial_state(concrete_data)
+    laser_evm = LaserEVM(execution_timeout=1000)
+    laser_evm.open_states = [deepcopy(init_state)]
+    plugin_loader = LaserPluginLoader()
+    assert PluginDiscovery().is_installed("myth_concolic_execution")
+    trace_plugin = PluginDiscovery().installed_plugins["myth_concolic_execution"]()
+
+    plugin_loader.load(trace_plugin)
+    laser_evm.time = datetime.now()
+    plugin_loader.instrument_virtual_machine(laser_evm, None)
+    for transaction in concrete_data["steps"]:
+        execute_transaction(
+            laser_evm,
+            callee_address=transaction["address"],
+            caller_address=symbol_factory.BitVecVal(
+                int(transaction["origin"], 16), 256
+            ),
+            origin_address=symbol_factory.BitVecVal(
+                int(transaction["origin"], 16), 256
+            ),
+            gas_limit=int(transaction.get("gasLimit", "0x9999999999999999999999"), 16),
+            data=binascii.a2b_hex(transaction["input"][2:]),
+            gas_price=int(transaction.get("gasPrice", "0x773594000"), 16),
+            value=int(transaction["value"], 16),
+            track_gas=False,
+        )
+
+    tx_id_manager.restart_counter()
+    return init_state, plugin_loader.plugin_list["MythX Trace Finder"].tx_trace  # type: ignore

mythril/disassembler/disassembly.py

@@ -23,8 +23,10 @@ class Disassembly(object):
         :param enable_online_lookup:
         """
         self.bytecode = code
-        self.instruction_list = asm.disassemble(util.safe_decode(code))
+        if type(code) == str:
-
+            self.instruction_list = asm.disassemble(util.safe_decode(code))
+        else:
+            self.instruction_list = asm.disassemble(code)
         self.func_hashes = []  # type: List[str]
         self.function_name_to_address = {}  # type: Dict[str, int]
         self.address_to_function_name = {}  # type: Dict[int, str]

mythril/exceptions.py

@@ -39,3 +39,9 @@ class DetectorNotFoundError(MythrilBaseException):
     detection module."""
 
     pass
+
+
+class IllegalArgumentError(ValueError):
+    """The argument used does not exist"""
+
+    pass

mythril/interfaces/cli.py

@@ -16,12 +16,15 @@ import traceback
 
 import mythril.support.signatures as sigs
 from argparse import ArgumentParser, Namespace, RawTextHelpFormatter
+from mythril.concolic import concolic_execution
 from mythril.exceptions import (
     DetectorNotFoundError,
     CriticalError,
 )
 from mythril.laser.ethereum.transaction.symbolic import ACTORS
+from mythril.plugin.discovery import PluginDiscovery
 from mythril.plugin.loader import MythrilPluginLoader
+
 from mythril.mythril import MythrilAnalyzer, MythrilDisassembler, MythrilConfig
 
 from mythril.analysis.module import ModuleLoader
@@ -34,6 +37,8 @@ _ = MythrilPluginLoader()
 
 ANALYZE_LIST = ("analyze", "a")
 DISASSEMBLE_LIST = ("disassemble", "d")
+
+CONCOLIC_LIST = ("concolic", "c")
 SAFE_FUNCTIONS_COMMAND = "safe-functions"
 READ_STORAGE_COMNAND = "read-storage"
 FUNCTION_TO_HASH_COMMAND = "function-to-hash"
@@ -47,6 +52,7 @@ log = logging.getLogger(__name__)
 COMMAND_LIST = (
     ANALYZE_LIST
     + DISASSEMBLE_LIST
+    + CONCOLIC_LIST
     + (
         READ_STORAGE_COMNAND,
         SAFE_FUNCTIONS_COMMAND,
@@ -203,6 +209,29 @@ def get_utilities_parser() -> ArgumentParser:
     return parser
 
 
+def create_concolic_parser(parser: ArgumentParser) -> ArgumentParser:
+    """
+    Get parser which handles arguments for concolic branch flipping
+    """
+    parser.add_argument(
+        "input",
+        help="The input jsonv2 file with concrete data",
+    )
+    parser.add_argument(
+        "--branches",
+        help="branch addresses to be flipped. usage: --branches 34,6f8,16a",
+        required=True,
+        metavar="BRANCH",
+    )
+    parser.add_argument(
+        "--solver-timeout",
+        type=int,
+        default=100000,
+        help="The maximum amount of time(in milli seconds) the solver spends for queries from analysis modules",
+    )
+    return parser
+
+
 def main() -> None:
     """The main CLI interface entry point."""
 
@@ -211,6 +240,7 @@ def main() -> None:
     runtime_input_parser = get_runtime_input_parser()
     creation_input_parser = get_creation_input_parser()
     output_parser = get_output_parser()
+
     parser = argparse.ArgumentParser(
         description="Security analysis of Ethereum smart contracts"
     )
@@ -262,6 +292,16 @@ def main() -> None:
     )
     create_disassemble_parser(disassemble_parser)
 
+    if PluginDiscovery().is_installed("myth_concolic_execution"):
+        concolic_parser = subparsers.add_parser(
+            CONCOLIC_LIST[0],
+            help="Runs concolic execution to flip the desired branches",
+            aliases=CONCOLIC_LIST[1:],
+            parents=[],
+            formatter_class=RawTextHelpFormatter,
+        )
+        create_concolic_parser(concolic_parser)
+
     subparsers.add_parser(
         LIST_DETECTORS_COMMAND,
         parents=[output_parser],
@@ -936,6 +976,15 @@ def parse_args_and_execute(parser: ArgumentParser, args: Namespace) -> None:
         parser.print_help()
         sys.exit()
 
+    if args.command in CONCOLIC_LIST:
+        with open(args.input) as f:
+            concrete_data = json.load(f)
+        output_list = concolic_execution(
+            concrete_data, args.branches.split(","), args.solver_timeout
+        )
+        json.dump(output_list, sys.stdout, indent=4)
+        sys.exit()
+
     # Parse cmdline args
     validate_args(args)
     try:

mythril/laser/ethereum/instructions.py

@@ -56,7 +56,7 @@ from mythril.laser.ethereum.transaction import (
     MessageCallTransaction,
     TransactionStartSignal,
     ContractCreationTransaction,
-    get_next_transaction_id,
+    tx_id_manager,
 )
 
 from mythril.support.support_utils import get_code_hash
@@ -194,6 +194,7 @@ class StateTransition(object):
             new_global_states = [
                 self.accumulate_gas(state) for state in new_global_states
             ]
+
             return self.increment_states_pc(new_global_states)
 
         return wrapper
@@ -726,7 +727,6 @@ class Instruction:
 
         op1 = state.stack.pop()
         op2 = state.stack.pop()
-
         if isinstance(op1, Bool):
             op1 = If(
                 op1, symbol_factory.BitVecVal(1, 256), symbol_factory.BitVecVal(0, 256)
@@ -1599,6 +1599,7 @@ class Instruction:
             new_state.mstate.max_gas_used += max_gas
 
             # manually increment PC
+
             new_state.mstate.depth += 1
             new_state.mstate.pc += 1
             new_state.world_state.constraints.append(negated)
@@ -1606,8 +1607,6 @@ class Instruction:
         else:
             log.debug("Pruned unreachable states.")
 
-        # True case
-
         # Get jump destination
         index = util.get_instruction_index(disassembly.instruction_list, jump_addr)
 
@@ -1750,7 +1749,7 @@ class Instruction:
 
         code_str = bytes.hex(bytes(code_raw))
 
-        next_transaction_id = get_next_transaction_id()
+        next_transaction_id = tx_id_manager.get_next_tx_id()
         constructor_arguments = ConcreteCalldata(
             next_transaction_id, call_data[code_end:]
         )

mythril/laser/ethereum/state/account.py

@@ -109,17 +109,18 @@ class Account:
         balances: Array = None,
         concrete_storage=False,
         dynamic_loader=None,
+        nonce=0,
     ) -> None:
         """Constructor for account.
 
         :param address: Address of the account
         :param code: The contract code of the account
         :param contract_name: The name associated with the account
-        :param balance: The balance for the account
+        :param balances: The balance for the account
         :param concrete_storage: Interpret storage as concrete
         """
         self.concrete_storage = concrete_storage
-        self.nonce = 0
+        self.nonce = nonce
         self.code = code or Disassembly("")
         self.address = (
             address
@@ -162,6 +163,16 @@ class Account:
         assert self._balances is not None
         self._balances[self.address] = balance
 
+    def set_storage(self, storage: Dict):
+        """
+        Sets concrete storage
+        """
+        for key, value in storage.items():
+            concrete_key, concrete_value = int(key, 16), int(value, 16)
+            self.storage[
+                symbol_factory.BitVecVal(concrete_key, 256)
+            ] = symbol_factory.BitVecVal(concrete_value, 256)
+
     def add_balance(self, balance: Union[int, BitVec]) -> None:
         """
 
@@ -205,6 +216,7 @@ class Account:
             contract_name=self.contract_name,
             balances=self._balances,
             concrete_storage=self.concrete_storage,
+            nonce=self.nonce,
         )
         new_account.storage = deepcopy(self.storage)
         new_account.code = self.code

mythril/laser/ethereum/state/constraints.py

@@ -47,13 +47,6 @@ class Constraints(list):
         )
         super(Constraints, self).append(constraint)
 
-    def pop(self, index: int = -1) -> None:
-        """
-
-        :param index: Index to be popped from the list
-        """
-        raise NotImplementedError
-
     @property
     def as_list(self) -> List[Bool]:
         """

mythril/laser/ethereum/state/machine_state.py

@@ -107,7 +107,6 @@ class MachineState:
         depth=0,
         max_gas_used=0,
         min_gas_used=0,
-        prev_pc=-1,
     ) -> None:
         """Constructor for machineState.
 
@@ -119,9 +118,8 @@ class MachineState:
         :param depth:
         :param max_gas_used:
         :param min_gas_used:
-        :param prev_pc:
         """
-        self._pc = pc
+        self.pc = pc
         self.stack = MachineStack(stack)
         self.subroutine_stack = MachineStack(subroutine_stack)
         self.memory = memory or Memory()
@@ -129,7 +127,6 @@ class MachineState:
         self.min_gas_used = min_gas_used  # lower gas usage bound
         self.max_gas_used = max_gas_used  # upper gas usage bound
         self.depth = depth
-        self.prev_pc = prev_pc  # holds context of current pc
 
     def calculate_extension_size(self, start: int, size: int) -> int:
         """
@@ -225,11 +222,10 @@ class MachineState:
             gas_limit=self.gas_limit,
             max_gas_used=self.max_gas_used,
             min_gas_used=self.min_gas_used,
-            pc=self._pc,
+            pc=self.pc,
             stack=copy(self.stack),
             memory=copy(self.memory),
             depth=self.depth,
-            prev_pc=self.prev_pc,
             subroutine_stack=copy(self.subroutine_stack),
         )
 
@@ -240,19 +236,6 @@ class MachineState:
         """
         return str(self.as_dict)
 
-    @property
-    def pc(self) -> int:
-        """
-
-        :return:
-        """
-        return self._pc
-
-    @pc.setter
-    def pc(self, value):
-        self.prev_pc = self._pc
-        self._pc = value
-
     @property
     def memory_size(self) -> int:
         """
@@ -268,7 +251,7 @@ class MachineState:
         :return:
         """
         return dict(
-            pc=self._pc,
+            pc=self.pc,
             stack=self.stack,
             subroutine_stack=self.subroutine_stack,
             memory=self.memory,
@@ -276,5 +259,4 @@ class MachineState:
             gas=self.gas_limit,
             max_gas_used=self.max_gas_used,
             min_gas_used=self.min_gas_used,
-            prev_pc=self.prev_pc,
         )

mythril/laser/ethereum/state/world_state.py

@@ -125,6 +125,7 @@ class WorldState:
         dynamic_loader=None,
         creator=None,
         code=None,
+        nonce=0,
     ) -> Account:
         """Create non-contract account.
 
@@ -134,14 +135,21 @@ class WorldState:
         :param dynamic_loader: used for dynamically loading storage from the block chain
         :param creator: The address of the creator of the contract if it's a contract
         :param code: The code of the contract, if it's a contract
+        :param nonce: Nonce of the account
         :return: The new account
         """
+        if creator in self.accounts:
+            nonce = self.accounts[creator].nonce
+        elif creator:
+            self.create_account(address=creator)
+
         address = (
             symbol_factory.BitVecVal(address, 256)
-            if address
+            if address is not None
-            else self._generate_new_address(creator)
+            else self._generate_new_address(creator, nonce=self.accounts[creator].nonce)
         )
-
+        if creator:
+            self.accounts[creator].nonce += 1
         new_account = Account(
             address=address,
             balances=self.balances,
@@ -150,7 +158,7 @@ class WorldState:
         )
         if code:
             new_account.code = code
-
+        new_account.nonce = nonce
         new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
 
         self.put_account(new_account)
@@ -197,14 +205,14 @@ class WorldState:
         """
         return filter(lambda x: isinstance(x, annotation_type), self.annotations)
 
-    def _generate_new_address(self, creator=None) -> BitVec:
+    def _generate_new_address(self, creator=None, nonce=0) -> BitVec:
         """Generates a new address for the global state.
 
         :return:
         """
         if creator:
             # TODO: Use nounce
-            address = "0x" + str(generate_contract_address(creator, 0).hex())
+            address = "0x" + str(generate_contract_address(creator, nonce).hex())
             return symbol_factory.BitVecVal(int(address, 16), 256)
         while True:
             address = "0x" + "".join([str(hex(randint(0, 16)))[-1] for _ in range(40)])

mythril/laser/ethereum/strategy/__init__.py

@@ -4,9 +4,9 @@ from mythril.laser.ethereum.state.global_state import GlobalState
 
 
 class BasicSearchStrategy(ABC):
-    """"""
+    """
-
+    A basic search strategy which halts based on depth
-    __slots__ = "work_list", "max_depth"
+    """
 
     def __init__(self, work_list, max_depth):
         self.work_list = work_list  # type: List[GlobalState]
@@ -26,5 +26,26 @@ class BasicSearchStrategy(ABC):
             if global_state.mstate.depth >= self.max_depth:
                 return self.__next__()
             return global_state
-        except IndexError:
+        except (IndexError, StopIteration):
+            raise StopIteration
+
+
+class CriterionSearchStrategy(BasicSearchStrategy):
+    """
+    If a criterion is satisfied, the search halts
+    """
+
+    def __init__(self, work_list, max_depth):
+        super().__init__(work_list, max_depth)
+        self._satisfied_criterion = False
+
+    def get_strategic_global_state(self):
+        if self._satisfied_criterion:
+            raise StopIteration
+        try:
+            global_state = self.get_strategic_global_state()
+        except StopIteration:
             raise StopIteration
+
+    def set_criterion_satisfied(self):
+        self._satisfied_criterion = True

mythril/laser/ethereum/strategy/basic.py

@@ -4,33 +4,7 @@ from typing import List
 
 from mythril.laser.ethereum.state.global_state import GlobalState
 from . import BasicSearchStrategy
-
+from random import choices
-try:
-    from random import choices
-except ImportError:
-
-    # This is for supporting python versions < 3.6
-    from itertools import accumulate
-    from random import random
-    from bisect import bisect
-
-    # TODO: Remove ignore after this has been fixed: https://github.com/python/mypy/issues/1297
-    def choices(  # type: ignore
-        population: List, weights: List[int] = None
-    ) -> List[int]:
-        """Returns a random element out of the population based on weight.
-
-        If the relative weights or cumulative weights are not specified,
-        the selections are made with equal probability.
-        """
-        if weights is None:
-            return [population[int(random() * len(population))]]
-        cum_weights = list(accumulate(weights))
-        return [
-            population[
-                bisect(cum_weights, random() * cum_weights[-1], 0, len(population) - 1)
-            ]
-        ]
 
 
 class DepthFirstSearchStrategy(BasicSearchStrategy):

mythril/laser/ethereum/strategy/concolic.py

@@ -0,0 +1,133 @@
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.constraints import Constraints
+from mythril.laser.ethereum.strategy.basic import BasicSearchStrategy
+from mythril.laser.ethereum.state.annotation import StateAnnotation
+from mythril.laser.ethereum.transaction import ContractCreationTransaction
+from mythril.laser.ethereum.util import get_instruction_index
+from mythril.analysis.solver import get_transaction_sequence
+from mythril.laser.smt import Not
+from mythril.exceptions import UnsatError
+
+from functools import reduce
+from typing import Dict, cast, List, Any, Tuple
+from copy import copy
+from . import CriterionSearchStrategy
+import logging
+import operator
+
+log = logging.getLogger(__name__)
+
+
+class TraceAnnotation(StateAnnotation):
+    """
+    This is the annotation used by the ConcolicStrategy to store concolic traces.
+    """
+
+    def __init__(self, trace=None):
+        self.trace = trace or []
+
+    @property
+    def persist_over_calls(self) -> bool:
+        return True
+
+    def __copy__(self):
+        return TraceAnnotation(copy(self.trace))
+
+
+class ConcolicStrategy(CriterionSearchStrategy):
+    """
+    Executes program concolically using the input trace till a specific branch
+    """
+
+    def __init__(
+        self,
+        work_list: List[GlobalState],
+        max_depth: int,
+        trace: List[List[Tuple[int, str]]],
+        flip_branch_addresses: List[str],
+    ):
+        """
+
+        work_list: The work-list of states
+        max_depth: The maximum depth for the strategy to go through
+        trace: This is the trace to be followed, each element is of the type Tuple(program counter, tx_id)
+        flip_branch_addresses: Branch addresses to be flipped.
+        """
+        super().__init__(work_list, max_depth)
+        self.trace: List[Tuple[int, str]] = reduce(operator.iconcat, trace, [])
+        self.last_tx_count: int = len(trace)
+        self.flip_branch_addresses: List[str] = flip_branch_addresses
+        self.results: Dict[str, Dict[str, Any]] = {}
+
+    def check_completion_criterion(self):
+        if len(self.flip_branch_addresses) == len(self.results):
+            self.set_criterion_satisfied()
+
+    def get_strategic_global_state(self) -> GlobalState:
+        """
+        This function does the following:-
+        1) Choose the states by following the concolic trace.
+        2) In case we have an executed JUMPI that is in flip_branch_addresses, flip that branch.
+        :return:
+        """
+        while len(self.work_list) > 0:
+            state = self.work_list.pop()
+            seq_id = len(state.world_state.transaction_sequence)
+
+            trace_annotations = cast(
+                List[TraceAnnotation],
+                list(state.world_state.get_annotations(TraceAnnotation)),
+            )
+
+            if len(trace_annotations) == 0:
+                annotation = TraceAnnotation()
+                state.world_state.annotate(annotation)
+            else:
+                annotation = trace_annotations[0]
+
+            # Appends trace
+            annotation.trace.append((state.mstate.pc, state.current_transaction.id))
+
+            # If length of trace is 1 then it is not a JUMPI
+            if len(annotation.trace) < 2:
+                # If trace does not follow the specified path, ignore the state
+                if annotation.trace != self.trace[: len(annotation.trace)]:
+                    continue
+                return state
+
+            # Get the address of the previous pc
+            addr: str = str(
+                state.environment.code.instruction_list[annotation.trace[-2][0]][
+                    "address"
+                ]
+            )
+            if (
+                annotation.trace == self.trace[: len(annotation.trace)]
+                and seq_id == self.last_tx_count
+                and addr in self.flip_branch_addresses
+                and addr not in self.results
+            ):
+                if (
+                    state.environment.code.instruction_list[annotation.trace[-2][0]][
+                        "opcode"
+                    ]
+                    != "JUMPI"
+                ):
+                    log.error(
+                        f"The branch {addr} does not lead "
+                        "to a jump address, skipping this branch"
+                    )
+                    continue
+
+                constraints = Constraints(state.world_state.constraints[:-1])
+                constraints.append(Not(state.world_state.constraints[-1]))
+
+                try:
+                    self.results[addr] = get_transaction_sequence(state, constraints)
+                except UnsatError:
+                    self.results[addr] = None
+            elif annotation.trace != self.trace[: len(annotation.trace)]:
+                continue
+            self.check_completion_criterion()
+            return state
+        raise StopIteration

mythril/laser/ethereum/svm.py

@@ -60,6 +60,7 @@ class LaserEVM:
         transaction_count=2,
         requires_statespace=True,
         iprof=None,
+        use_reachability_check=True,
     ) -> None:
         """
         Initializes the laser evm object
@@ -73,14 +74,15 @@ class LaserEVM:
         :param requires_statespace: Variable indicating whether the statespace should be recorded
         :param iprof: Instruction Profiler
         """
-        self.execution_info = []  # type: List[ExecutionInfo]
+        self.execution_info: List[ExecutionInfo] = []
 
-        self.open_states = []  # type: List[WorldState]
+        self.open_states: List[WorldState] = []
         self.total_states = 0
         self.dynamic_loader = dynamic_loader
+        self.use_reachability_check = use_reachability_check
 
         # TODO: What about using a deque here?
-        self.work_list = []  # type: List[GlobalState]
+        self.work_list: List[GlobalState] = []
         self.strategy = strategy(self.work_list, max_depth)
         self.max_depth = max_depth
         self.transaction_count = transaction_count
@@ -90,30 +92,45 @@ class LaserEVM:
 
         self.requires_statespace = requires_statespace
         if self.requires_statespace:
-            self.nodes = {}  # type: Dict[int, Node]
+            self.nodes: Dict[int, Node] = {}
-            self.edges = []  # type: List[Edge]
+            self.edges: List[Edge] = []
 
-        self.time = None  # type: datetime
+        self.time: datetime = None
 
-        self.pre_hooks = defaultdict(list)  # type: DefaultDict[str, List[Callable]]
+        self.pre_hooks: DefaultDict[str, List[Callable]] = defaultdict(list)
-        self.post_hooks = defaultdict(list)  # type: DefaultDict[str, List[Callable]]
+        self.post_hooks: DefaultDict[str, List[Callable]] = defaultdict(list)
 
-        self._add_world_state_hooks = []  # type: List[Callable]
+        self._add_world_state_hooks: List[Callable] = []
-        self._execute_state_hooks = []  # type: List[Callable]
+        self._execute_state_hooks: List[Callable] = []
 
-        self._start_sym_trans_hooks = []  # type: List[Callable]
+        self._start_sym_trans_hooks: List[Callable] = []
-        self._stop_sym_trans_hooks = []  # type: List[Callable]
+        self._stop_sym_trans_hooks: List[Callable] = []
 
-        self._start_sym_exec_hooks = []  # type: List[Callable]
+        self._start_sym_exec_hooks: List[Callable] = []
-        self._stop_sym_exec_hooks = []  # type: List[Callable]
+        self._stop_sym_exec_hooks: List[Callable] = []
+
+        self._start_exec_hooks: List[Callable] = []
+        self._stop_exec_hooks: List[Callable] = []
 
         self._transaction_end_hooks: List[Callable] = []
+
         self.iprof = iprof
-        self.instr_pre_hook = {}  # type: Dict[str, List[Callable]]
+        self.instr_pre_hook: Dict[str, List[Callable]] = {}
-        self.instr_post_hook = {}  # type: Dict[str, List[Callable]]
+        self.instr_post_hook: Dict[str, List[Callable]] = {}
         for op in OPCODES:
             self.instr_pre_hook[op] = []
             self.instr_post_hook[op] = []
+        self.hook_type_map = {
+            "add_world_state": self._add_world_state_hooks,
+            "execute_state": self._execute_state_hooks,
+            "start_sym_exec": self._start_sym_exec_hooks,
+            "stop_sym_exec": self._stop_sym_exec_hooks,
+            "start_sym_trans": self._start_sym_trans_hooks,
+            "stop_sym_trans": self._stop_sym_trans_hooks,
+            "start_exec": self._start_exec_hooks,
+            "stop_exec": self._stop_exec_hooks,
+            "transaction_end": self._transaction_end_hooks,
+        }
         log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
 
     def extend_strategy(self, extension: ABCMeta, *args) -> None:
@@ -200,12 +217,13 @@ class LaserEVM:
             if len(self.open_states) == 0:
                 break
             old_states_count = len(self.open_states)
-            self.open_states = [
+            if self.use_reachability_check:
-                state for state in self.open_states if state.constraints.is_possible
+                self.open_states = [
-            ]
+                    state for state in self.open_states if state.constraints.is_possible
-            prune_count = old_states_count - len(self.open_states)
+                ]
-            if prune_count:
+                prune_count = old_states_count - len(self.open_states)
-                log.info("Pruned {} unreachable states".format(prune_count))
+                if prune_count:
+                    log.info("Pruned {} unreachable states".format(prune_count))
             log.info(
                 "Starting message call transaction, iteration: {}, {} initial states".format(
                     i, len(self.open_states)
@@ -242,6 +260,8 @@ class LaserEVM:
         :return:
         """
         final_states = []  # type: List[GlobalState]
+        for hook in self._start_exec_hooks:
+            hook()
 
         for global_state in self.strategy:
             if create and self._check_create_termination():
@@ -272,6 +292,9 @@ class LaserEVM:
                 final_states.append(global_state)
             self.total_states += len(new_states)
 
+        for hook in self._stop_exec_hooks:
+            hook()
+
         return final_states if track_gas else None
 
     def _add_world_state(self, global_state: GlobalState):
@@ -581,20 +604,9 @@ class LaserEVM:
 
     def register_laser_hooks(self, hook_type: str, hook: Callable):
         """registers the hook with this Laser VM"""
-        if hook_type == "add_world_state":
+
-            self._add_world_state_hooks.append(hook)
+        if hook_type in self.hook_type_map:
-        elif hook_type == "execute_state":
+            self.hook_type_map[hook_type].append(hook)
-            self._execute_state_hooks.append(hook)
-        elif hook_type == "start_sym_exec":
-            self._start_sym_exec_hooks.append(hook)
-        elif hook_type == "stop_sym_exec":
-            self._stop_sym_exec_hooks.append(hook)
-        elif hook_type == "start_sym_trans":
-            self._start_sym_trans_hooks.append(hook)
-        elif hook_type == "stop_sym_trans":
-            self._stop_sym_trans_hooks.append(hook)
-        elif hook_type == "transaction_end":
-            self._transaction_end_hooks.append(hook)
         else:
             raise ValueError(f"Invalid hook type {hook_type}")
 

mythril/laser/ethereum/transaction/concolic.py

@@ -1,27 +1,87 @@
 """This module contains functions to set up and execute concolic message
 calls."""
+import binascii
+
 from typing import List, Union
+from copy import deepcopy
 
+from mythril.exceptions import IllegalArgumentError
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
+from mythril.laser.smt import symbol_factory
+from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.calldata import ConcreteCalldata
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.transaction.transaction_models import (
     MessageCallTransaction,
-    get_next_transaction_id,
+    ContractCreationTransaction,
+    tx_id_manager,
 )
 
 
+def execute_contract_creation(
+    laser_evm,
+    callee_address,
+    caller_address,
+    origin_address,
+    data,
+    gas_limit,
+    gas_price,
+    value,
+    code=None,
+    track_gas=False,
+    contract_name=None,
+):
+    """Executes a contract creation transaction concretely.
+
+    :param laser_evm:
+    :param callee_address:
+    :param caller_address:
+    :param origin_address:
+    :param code:
+    :param data:
+    :param gas_limit:
+    :param gas_price:
+    :param value:
+    :param track_gas:
+    :return:
+    """
+
+    open_states: List[WorldState] = laser_evm.open_states[:]
+    del laser_evm.open_states[:]
+
+    data = binascii.b2a_hex(data).decode("utf-8")
+
+    for open_world_state in open_states:
+        next_transaction_id = tx_id_manager.get_next_tx_id()
+        transaction = ContractCreationTransaction(
+            world_state=open_world_state,
+            identifier=next_transaction_id,
+            gas_price=gas_price,
+            gas_limit=gas_limit,  # block gas limit
+            origin=origin_address,
+            code=Disassembly(data),
+            caller=caller_address,
+            contract_name=contract_name,
+            call_data=None,
+            call_value=value,
+        )
+        _setup_global_state_for_execution(laser_evm, transaction)
+
+    return laser_evm.exec(True, track_gas=track_gas)
+
+
 def execute_message_call(
     laser_evm,
     callee_address,
     caller_address,
     origin_address,
-    code,
     data,
     gas_limit,
     gas_price,
     value,
+    code=None,
     track_gas=False,
 ) -> Union[None, List[GlobalState]]:
     """Execute a message call transaction from all open states.
@@ -38,12 +98,12 @@ def execute_message_call(
     :param track_gas:
     :return:
     """
-    # TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
-    open_states = laser_evm.open_states[:]
-    del laser_evm.open_states[:]
 
+    open_states: List[WorldState] = laser_evm.open_states[:]
+    del laser_evm.open_states[:]
     for open_world_state in open_states:
-        next_transaction_id = get_next_transaction_id()
+        next_transaction_id = tx_id_manager.get_next_tx_id()
+        code = code or open_world_state[callee_address].code.bytecode
         transaction = MessageCallTransaction(
             world_state=open_world_state,
             identifier=next_transaction_id,
@@ -94,3 +154,21 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
     global_state.node = new_node
     new_node.states.append(global_state)
     laser_evm.work_list.append(global_state)
+
+
+def execute_transaction(*args, **kwargs) -> Union[None, List[GlobalState]]:
+    """
+    Chooses the transaction type based on callee address and
+    executes the transaction
+    """
+    try:
+        if kwargs["callee_address"] == "":
+            if kwargs["caller_address"] == "":
+                kwargs["caller_address"] = kwargs["origin"]
+            return execute_contract_creation(*args, **kwargs)
+        kwargs["callee_address"] = symbol_factory.BitVecVal(
+            int(kwargs["callee_address"], 16), 256
+        )
+    except KeyError as k:
+        raise IllegalArgumentError(f"Argument not found: {k}")
+    return execute_message_call(*args, **kwargs)

mythril/laser/ethereum/transaction/symbolic.py

@@ -2,6 +2,7 @@
 symbolic values."""
 import logging
 from typing import Optional
+from copy import deepcopy
 
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
@@ -11,9 +12,10 @@ from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.transaction.transaction_models import (
     MessageCallTransaction,
     ContractCreationTransaction,
-    get_next_transaction_id,
+    tx_id_manager,
     BaseTransaction,
 )
+from typing import List, Union
 from mythril.laser.smt import symbol_factory, Or, BitVec
 
 log = logging.getLogger(__name__)
@@ -82,7 +84,7 @@ def execute_message_call(laser_evm, callee_address: BitVec) -> None:
             log.debug("Can not execute dead contract, skipping.")
             continue
 
-        next_transaction_id = get_next_transaction_id()
+        next_transaction_id = tx_id_manager.get_next_tx_id()
 
         external_sender = symbol_factory.BitVecSym(
             "sender_{}".format(next_transaction_id), 256
@@ -109,7 +111,12 @@ def execute_message_call(laser_evm, callee_address: BitVec) -> None:
 
 
 def execute_contract_creation(
-    laser_evm, contract_initialization_code, contract_name=None, world_state=None
+    laser_evm,
+    contract_initialization_code,
+    contract_name=None,
+    world_state=None,
+    origin=ACTORS["CREATOR"],
+    caller=ACTORS["CREATOR"],
 ) -> Account:
     """Executes a contract creation transaction from all open states.
 
@@ -118,14 +125,13 @@ def execute_contract_creation(
     :param contract_name:
     :return:
     """
-    # TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
-    del laser_evm.open_states[:]
 
     world_state = world_state or WorldState()
     open_states = [world_state]
+    del laser_evm.open_states[:]
     new_account = None
     for open_world_state in open_states:
-        next_transaction_id = get_next_transaction_id()
+        next_transaction_id = tx_id_manager.get_next_tx_id()
         # call_data "should" be '[]', but it is easier to model the calldata symbolically
         # and add logic in codecopy/codesize/calldatacopy/calldatasize than to model code "correctly"
         transaction = ContractCreationTransaction(
@@ -135,9 +141,9 @@ def execute_contract_creation(
                 "gas_price{}".format(next_transaction_id), 256
             ),
             gas_limit=8000000,  # block gas limit
-            origin=ACTORS["CREATOR"],
+            origin=origin,
             code=Disassembly(contract_initialization_code),
-            caller=ACTORS["CREATOR"],
+            caller=caller,
             contract_name=contract_name,
             call_data=None,
             call_value=symbol_factory.BitVecSym(
@@ -189,3 +195,24 @@ def _setup_global_state_for_execution(laser_evm, transaction: BaseTransaction) -
     global_state.node = new_node
     new_node.states.append(global_state)
     laser_evm.work_list.append(global_state)
+
+
+def execute_transaction(*args, **kwargs):
+    """
+    Chooses the transaction type based on callee address and
+    executes the transaction
+    """
+    laser_evm = args[0]
+    if kwargs["callee_address"] == "":
+        for ws in laser_evm.open_states[:]:
+            execute_contract_creation(
+                laser_evm=laser_evm,
+                contract_initialization_code=kwargs["data"],
+                world_state=ws,
+            )
+        return
+
+    execute_message_call(
+        laser_evm=laser_evm,
+        callee_address=symbol_factory.BitVecVal(int(kwargs["callee_address"], 16), 256),
+    )

mythril/laser/ethereum/transaction/transaction_models.py

@@ -4,7 +4,7 @@ execution."""
 from copy import deepcopy
 from z3 import ExprRef
 from typing import Union, Optional
-
+from mythril.support.support_utils import Singleton
 from mythril.laser.ethereum.state.calldata import ConcreteCalldata
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata
@@ -16,17 +16,20 @@ import logging
 
 log = logging.getLogger(__name__)
 
-_next_transaction_id = 0
 
+class TxIdManager(object, metaclass=Singleton):
+    def __init__(self):
+        self._next_transaction_id = 0
+
+    def get_next_tx_id(self):
+        self._next_transaction_id += 1
+        return str(self._next_transaction_id)
+
+    def restart_counter(self):
+        self._next_transaction_id = 0
 
-def get_next_transaction_id() -> str:
-    """
 
-    :return:
+tx_id_manager = TxIdManager()
-    """
-    global _next_transaction_id
-    _next_transaction_id += 1
-    return str(_next_transaction_id)
 
 
 class TransactionEndSignal(Exception):
@@ -72,7 +75,7 @@ class BaseTransaction:
     ) -> None:
         assert isinstance(world_state, WorldState)
         self.world_state = world_state
-        self.id = identifier or get_next_transaction_id()
+        self.id = identifier or tx_id_manager.get_next_tx_id()
 
         self.gas_price = (
             gas_price

mythril/laser/plugin/loader.py

@@ -2,6 +2,7 @@ import logging
 from typing import Dict, List, Optional
 
 from mythril.laser.ethereum.svm import LaserEVM
+from mythril.laser.plugin.interface import LaserPlugin
 from mythril.laser.plugin.builder import PluginBuilder
 from mythril.support.support_utils import Singleton
 
@@ -18,6 +19,7 @@ class LaserPluginLoader(object, metaclass=Singleton):
         """Initializes the plugin loader"""
         self.laser_plugin_builders = {}  # type: Dict[str, PluginBuilder]
         self.plugin_args = {}  # type: Dict[str, Dict]
+        self.plugin_list = {}  # type: Dict[str, LaserPlugin]
 
     def add_args(self, plugin_name, **kwargs):
         self.plugin_args[plugin_name] = kwargs
@@ -70,3 +72,4 @@ class LaserPluginLoader(object, metaclass=Singleton):
             log.info(f"Instrumenting symbolic vm with plugin: {plugin_name}")
             plugin = plugin_builder(**self.plugin_args.get(plugin_name, {}))
             plugin.initialize(symbolic_vm)
+            self.plugin_list[plugin_name] = plugin

mythril/mythril/mythril_disassembler.py

@@ -89,6 +89,7 @@ class MythrilDisassembler:
         """
         if address is None:
             address = util.get_indexed_address(0)
+
         if bin_runtime:
             self.contracts.append(
                 EVMContract(

mythril/plugin/discovery.py

@@ -36,7 +36,6 @@ class PluginDiscovery(object, metaclass=Singleton):
             raise ValueError(f"Plugin with name: `{plugin_name}` is not installed")
 
         plugin = self.installed_plugins.get(plugin_name)
-
         if plugin is None or not issubclass(plugin, MythrilPlugin):
             raise ValueError(f"No valid plugin was found for {plugin_name}")
 

mythril/plugin/loader.py

@@ -46,7 +46,6 @@ class MythrilPluginLoader(object, metaclass=Singleton):
         logging.info(f"Loading plugin: {plugin.name}")
 
         log.info(f"Loading plugin: {str(plugin)}")
-
         if isinstance(plugin, DetectionModule):
             self._load_detection_module(plugin)
         elif isinstance(plugin, MythrilLaserPlugin):