diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ef4a0acef6..0887c6b412 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -103,5 +103,3 @@ jobs: uses: pypa/gh-action-pypi-publish@v1.2.2 with: password: ${{ secrets.PYPI_UPLOAD }} - - diff --git a/docs/states.rst b/docs/states.rst index 7f40dcb5a7..291129ae4b 100644 --- a/docs/states.rst +++ b/docs/states.rst @@ -16,3 +16,11 @@ Operations :members: :undoc-members: :exclude-members: all_states, ready_states, count_ready_states, count_busy_states, killed_states, count_killed_states, terminated_states, count_terminated_states + + +Inspecting +---------- + +.. autoclass:: manticore.core.plugin.StateDescriptor + :members: + :undoc-members: diff --git a/examples/evm/mappingchallenge.py b/examples/evm/mappingchallenge.py index 1f8bf7c95f..3de1fc7853 100644 --- a/examples/evm/mappingchallenge.py +++ b/examples/evm/mappingchallenge.py @@ -29,7 +29,7 @@ class StopAtDepth(Detector): """ This just aborts explorations that are too deep """ - def will_start_run_callback(self, *args): + def will_run_callback(self, *args): with self.manticore.locked_context("seen_rep", dict) as reps: reps.clear() diff --git a/examples/linux/introspect_state.py b/examples/linux/introspect_state.py new file mode 100644 index 0000000000..be4304e429 --- /dev/null +++ b/examples/linux/introspect_state.py @@ -0,0 +1,74 @@ +from manticore.native import Manticore +from manticore.core.plugin import StateDescriptor +from manticore.utils.enums import StateStatus +from time import sleep +import typing +import argparse + +parser = argparse.ArgumentParser( + description="Explore a binary with Manticore and print the tree of states" +) +parser.add_argument( + "binary", type=str, nargs="?", default="binaries/multiple-styles", help="The program to run", +) +args = parser.parse_args() + + +def print_fork_tree(states: typing.Dict[int, StateDescriptor]): + """ + Performs a depth-first traversal of the state tree, where each branch is a different fork + """ + + def df_print(state_id, depth=0): + state = states[state_id] + + # Prepare a debug message about the state based on its current status + msg = "" + if state.status == StateStatus.running: + msg = "(Exec {} ins)".format(state.own_execs if state.own_execs is not None else 0) + elif state.status == StateStatus.waiting_for_solver: + msg = "(Solving)" + elif state.status == StateStatus.waiting_for_worker: + msg = "(Waiting)" + elif state.status == StateStatus.stopped: + msg = "({})".format(state.termination_msg) + + # Print nice pretty arrows showing parenthood + if depth == 0: + print(state_id, msg) + else: + print(" " * (depth - 1) + "└-->", state_id, msg) + + # Prioritize states with fewer (or no) children since it gives us a nicer tree in the common case + for c_st in sorted(state.children, key=lambda k: len(states[k].children)): + df_print(c_st, depth + 1) + + # Only works if all states fork from the initial state + df_print(0) + print() + + +def run_every(callee: typing.Callable, duration: int = 3) -> typing.Callable: + """ + Returns a function that calls every seconds + """ + + def inner(thread): # Takes `thread` as argument, which is provided by the daemon thread API + while True: + # Pass Manticore's state descriptor dict to the callee + callee(thread.manticore.introspect()) + sleep(duration) + + return inner + + +m = Manticore(args.binary) + +# Tell Manticore to run `print_fork_tree` every second +m.register_daemon(run_every(print_fork_tree, 1)) + +m.run() + +sleep(1) +print("Final fork tree:") +print_fork_tree(m.introspect()) diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py index 321071c161..b94feef826 100644 --- a/manticore/core/manticore.py +++ b/manticore/core/manticore.py @@ -2,7 +2,7 @@ import itertools import logging import sys -import time +import typing import random import weakref from typing import Callable @@ -12,44 +12,25 @@ import functools import shlex -from ..core.plugin import Plugin +from ..core.plugin import Plugin, IntrospectionAPIPlugin, StateDescriptor from ..core.smtlib import Expression from ..core.state import StateBase from ..core.workspace import ManticoreOutput from ..exceptions import ManticoreError from ..utils import config from ..utils.deprecated import deprecated +from ..utils.enums import StateLists, MProcessingType from ..utils.event import Eventful -from ..utils.helpers import PickleSerializer +from ..utils.helpers import PickleSerializer, pretty_print_state_descriptors from ..utils.log import set_verbosity from ..utils.nointerrupt import WithKeyboardInterruptAs from .workspace import Workspace, Testcase -from .worker import WorkerSingle, WorkerThread, WorkerProcess +from .worker import WorkerSingle, WorkerThread, WorkerProcess, DaemonThread from multiprocessing.managers import SyncManager import threading import ctypes import signal -from enum import Enum - - -class MProcessingType(Enum): - """Used as configuration constant for choosing multiprocessing flavor""" - - multiprocessing = "multiprocessing" - single = "single" - threading = "threading" - - def title(self): - return self._name_.title() - - @classmethod - def from_string(cls, name): - return cls.__members__[name] - - def to_class(self): - return globals()[f"Manticore{self.title()}"] - logger = logging.getLogger(__name__) @@ -80,6 +61,8 @@ def to_class(self): class ManticoreBase(Eventful): + _published_events = {"solve"} + def _manticore_single(self): self._worker_type = WorkerSingle @@ -195,16 +178,26 @@ def newFunction(self, *args, **kw): "run", "start_worker", "terminate_worker", + "transition_state", "enqueue_state", "fork_state", "load_state", + "save_state", + "remove_state", "terminate_state", "kill_state", "execute_instruction", "terminate_execution", } - def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kwargs): + def __init__( + self, + initial_state, + workspace_url=None, + outputspace_url=None, + introspection_plugin_type: type = IntrospectionAPIPlugin, + **kwargs, + ): """ Manticore symbolically explores program states. @@ -364,7 +357,12 @@ def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kw # the different type of events occur over an exploration. # Note that each callback will run in a worker process and that some # careful use of the shared context is needed. - self.plugins = set() + self.plugins: typing.Set[Plugin] = set() + assert issubclass( + introspection_plugin_type, IntrospectionAPIPlugin + ), "Introspection plugin must be a subclass of IntrospectionAPIPlugin" + self._introspector = introspection_plugin_type() + self.register_plugin(self._introspector) # Set initial root state if not isinstance(initial_state, StateBase): @@ -373,6 +371,11 @@ def __init__(self, initial_state, workspace_url=None, outputspace_url=None, **kw # Workers will use manticore __dict__ So lets spawn them last self._workers = [self._worker_type(id=i, manticore=self) for i in range(consts.procs)] + + # We won't create the daemons until .run() is called + self._daemon_threads: typing.List[DaemonThread] = [] + self._daemon_callbacks: typing.List[typing.Callable] = [] + self._snapshot = None self._main_id = os.getpid(), threading.current_thread().ident @@ -405,7 +408,9 @@ def goto_snapshot(self): raise ManticoreError("No snapshot to go to") self.clear_ready_states() for state_id in self._snapshot: + self._publish("will_enqueue_state", None, can_raise=False) self._ready_states.append(state_id) + self._publish("did_enqueue_state", state_id, can_raise=False) self._snapshot = None @sync @@ -514,16 +519,15 @@ def setstate(x, y): # maintain a list of children for logging purpose children.append(new_state_id) + self._publish("did_fork_state", state, expression, solutions, policy, children) + logger.debug("Forking current state %r into states %r", state.id, children) + with self._lock: self._busy_states.remove(state.id) self._remove(state.id) state._id = None self._lock.notify_all() - self._publish("did_fork_state", new_state, expression, new_value, policy) - - logger.debug("Forking current state %r into states %r", state.id, children) - @staticmethod @deprecated("Use utils.log.set_verbosity instead.") def verbosity(level): @@ -535,7 +539,7 @@ def verbosity(level): # State storage @Eventful.will_did("save_state", can_raise=False) - def _save(self, state, state_id=None): + def _save(self, state, state_id=None) -> int: """ Store or update a state in secondary storage under state_id. Use a fresh id is None is provided. @@ -548,15 +552,14 @@ def _save(self, state, state_id=None): return state.id @Eventful.will_did("load_state", can_raise=False) - def _load(self, state_id): + def _load(self, state_id: int) -> StateBase: """ Load the state from the secondary storage - :param state_id: a estate id - :type state_id: int - :returns: the state id used + :param state_id: a state id + :returns: the loaded state """ if not hasattr(self, "stcache"): - self.stcache = weakref.WeakValueDictionary() + self.stcache: weakref.WeakValueDictionary = weakref.WeakValueDictionary() if state_id in self.stcache: return self.stcache[state_id] state = self._workspace.load_state(state_id, delete=False) @@ -567,11 +570,10 @@ def _load(self, state_id): return state @Eventful.will_did("remove_state", can_raise=False) - def _remove(self, state_id): + def _remove(self, state_id: int) -> int: """ Remove a state from secondary storage - :param state_id: a estate id - :type state_id: int + :param state_id: a state id """ if not hasattr(self, "stcache"): self.stcache = weakref.WeakValueDictionary() @@ -579,9 +581,10 @@ def _remove(self, state_id): del self.stcache[state_id] self._workspace.rm_state(state_id) + return state_id # Internal support for state lists - def _put_state(self, state): + def _put_state(self, state) -> int: """ This enqueues the state for exploration. Serialize and store the state with a fresh state_id. Then add it to @@ -592,14 +595,18 @@ def _put_state(self, state): +-------+ """ + self._publish("will_enqueue_state", state, can_raise=False) state_id = self._save(state, state_id=state.id) with self._lock: # Enqueue it in the ready state list for processing self._ready_states.append(state_id) self._lock.notify_all() + # The problem with using will_did here is that the lock is released before the event is fired, so typically + # a worker has moved the state from READY to BUSY *before* `did_enqueue_state` is published. + self._publish("did_enqueue_state", state_id, can_raise=False) return state_id - def _get_state(self, wait=False): + def _get_state(self, wait=False) -> typing.Optional[StateBase]: """ Dequeue a state form the READY list and add it to the BUSY list """ with self._lock: # If wait is true do the conditional wait for states @@ -630,28 +637,39 @@ def _get_state(self, wait=False): state_id = random.choice(list(self._ready_states)) # Move from READY to BUSY + self._publish("will_transition_state", state_id, StateLists.ready, StateLists.busy) self._ready_states.remove(state_id) self._busy_states.append(state_id) + self._publish("did_transition_state", state_id, StateLists.ready, StateLists.busy) self._lock.notify_all() return self._load(state_id) @sync - def _revive_state(self, state_id): - """ Send a BUSY state back to READY list + def _revive_state(self, state_id: int): + """ Send a state back to READY list - +--------+ +------+ - | READY +<-------+ BUSY | - +---+----+ +------+ + +--------+ +------------------+ + | READY +<-------+ BUSY/TERMINATED | + +---+----+ +----------------+ """ - # Move from BUSY to READY - self._busy_states.remove(state_id) + # Move from BUSY or TERMINATED to READY + src = None + if state_id in self._busy_states: + src = StateLists.busy + self._publish("will_transition_state", state_id, src, StateLists.ready) + self._busy_states.remove(state_id) + if state_id in self._terminated_states: + src = StateLists.terminated + self._publish("will_transition_state", state_id, src, StateLists.ready) + self._terminated_states.remove(state_id) self._ready_states.append(state_id) + self._publish("did_transition_state", state_id, src, StateLists.ready) self._lock.notify_all() @sync - def _terminate_state(self, state_id, delete=False): + def _terminate_state(self, state_id: int, delete=False): """ Send a BUSY state to the TERMINATED list or trash it if delete is True +------+ +------------+ @@ -672,13 +690,15 @@ def _terminate_state(self, state_id, delete=False): self._remove(state_id) else: # add the state_id to the terminated list + self._publish("will_transition_state", state_id, StateLists.busy, StateLists.terminated) self._terminated_states.append(state_id) + self._publish("did_transition_state", state_id, StateLists.busy, StateLists.terminated) # wake up everyone waiting for a change in the state lists self._lock.notify_all() @sync - def _kill_state(self, state_id, delete=False): + def _kill_state(self, state_id: int, delete=False): """ Send a BUSY state to the KILLED list or trash it if delete is True +------+ +--------+ @@ -699,35 +719,42 @@ def _kill_state(self, state_id, delete=False): self._remove(state_id) else: # add the state_id to the terminated list + self._publish("will_transition_state", state_id, StateLists.busy, StateLists.killed) self._killed_states.append(state_id) + self._publish("did_transition_state", state_id, StateLists.busy, StateLists.killed) # wake up everyone waiting for a change in the state lists self._lock.notify_all() @sync - def kill_state(self, state, delete=False): + def kill_state(self, state: typing.Union[StateBase, int], delete: bool = False): """ Kill a state. A state is moved from any list to the kill list or fully removed from secondary storage - :param state_id: a estate id - :type state_id: int + :param state: a state :param delete: if true remove the state from the secondary storage - :type delete: bool + """ - state_id = state.id + state_id = getattr(state, "id", state) + src = None if state_id in self._busy_states: + src = StateLists.busy self._busy_states.remove(state_id) if state_id in self._terminated_states: + src = StateLists.terminated self._terminated_states.remove(state_id) if state_id in self._ready_states: + src = StateLists.ready self._ready_states.remove(state_id) if delete: self._remove(state_id) else: # add the state_id to the terminated list + self._publish("will_transition_state", state_id, src, StateLists.killed) self._killed_states.append(state_id) + self._publish("did_transition_state", state_id, src, StateLists.killed) @property # type: ignore @sync @@ -1071,12 +1098,23 @@ def run(self): # User subscription to events is disabled from now on self.subscribe = None + # Passing generators to callbacks is a bit hairy because the first callback would drain it if we didn't + # clone the iterator in event.py. We're preserving the old API here, but it's something to avoid in the future. self._publish("will_run", self.ready_states) self._running.value = True # start all the workers! for w in self._workers: w.start() + # Create each daemon thread and pass it `self` + if not self._daemon_threads: # Don't recreate the threads if we call run multiple times + for i, cb in enumerate(self._daemon_callbacks): + dt = DaemonThread( + id=i, manticore=self + ) # Potentially duplicated ids with workers. Don't mix! + self._daemon_threads.append(dt) + dt.start(cb) + # Main process. Lets just wait and capture CTRL+C at main with WithKeyboardInterruptAs(self.kill): with self._lock: @@ -1094,7 +1132,14 @@ def run(self): logger.debug("Killed. Moving all remaining ready states to killed list") # move all READY to KILLED: while self._ready_states: + state_id = self._ready_states[-1] + self._publish( + "will_transition_state", state_id, StateLists.ready, StateLists.killed + ) self._killed_states.append(self._ready_states.pop()) + self._publish( + "did_transition_state", state_id, StateLists.ready, StateLists.killed + ) self._running.value = False self._publish("did_run") @@ -1139,3 +1184,28 @@ def save_run_data(self): config.save(f) logger.info("Results in %s", self._output.store.uri) + + def introspect(self) -> typing.Dict[int, StateDescriptor]: + """ + Allows callers to view descriptors for each state + + :return: the latest copy of the State Descriptor dict + """ + if self._introspector is not None: + return self._introspector.get_state_descriptors() + return {} + + @at_not_running + def register_daemon(self, callback: typing.Callable): + """ + Allows the user to register a function that will be called at `ManticoreBase.run()` and can run + in the background. Infinite loops are acceptable as it will be killed when Manticore exits. The provided + function is passed a thread as an argument, with the current Manticore object available as thread.manticore. + + :param callback: function to be called + """ + self._daemon_callbacks.append(callback) + + def pretty_print_states(self, *_args): + """ Calls pretty_print_state_descriptors on the current set of state descriptors """ + pretty_print_state_descriptors(self.introspect()) diff --git a/manticore/core/plugin.py b/manticore/core/plugin.py index 6d1a1c4b23..5abf69737e 100644 --- a/manticore/core/plugin.py +++ b/manticore/core/plugin.py @@ -3,7 +3,11 @@ import cProfile import pstats import threading +import typing from functools import wraps +from dataclasses import dataclass, field +from ..utils.enums import StateLists, StateStatus +from datetime import datetime from .smtlib import issymbolic @@ -352,11 +356,11 @@ def will_execute_instruction_callback(self, state, pc, instruction): def did_execute_instruction_callback(self, state, pc, target_pc, instruction): logger.info("did_execute_instruction %r %r %r %r", state, pc, target_pc, instruction) - def will_start_run_callback(self, state): + def will_run_callback(self, state): """ Called once at the beginning of the run. state is the initial root state """ - logger.info("will_start_run") + logger.info("will_run") def did_run_callback(self): logger.info("did_run") @@ -364,8 +368,10 @@ def did_run_callback(self): def will_fork_state_callback(self, parent_state, expression, solutions, policy): logger.info("will_fork_state %r %r %r %r", parent_state, expression, solutions, policy) - def did_fork_state_callback(self, child_state, expression, new_value, policy): - logger.info("did_fork_state %r %r %r %r", child_state, expression, new_value, policy) + def did_fork_state_callback(self, child_state, expression, new_value, policy, children): + logger.info( + "did_fork_state %r %r %r %r %r", child_state, expression, new_value, policy, children + ) def did_load_state_callback(self, state, state_id): logger.info("did_load_state %r %r", state, state_id) @@ -402,3 +408,256 @@ def will_write_register_callback(self, state, register, value): def did_write_register_callback(self, state, register, value): logger.info("did_write_register %r %r %r", state, register, value) + + +@dataclass +class StateDescriptor: + """ + Dataclass that tracks information about a State. + """ + + #: State ID Number + state_id: int + #: Which State List the state currently resides in (or None if it's been removed entirely) + state_list: typing.Optional[StateLists] = None + #: State IDs of any states that forked from this one + children: set = field(default_factory=set) + #: The time that any field of this Descriptor was last updated + last_update: datetime = field(default_factory=datetime.now) + #: The time at which the on_execution_intermittent callback was last applied to this state. This is when the PC and exec count get updated. + last_intermittent_update: typing.Optional[datetime] = None + #: The time at which this state was created (or first detected, if the did_enque callback didn't fire for some reason) + created_at: datetime = field(default_factory=datetime.now) + #: What the state is currently doing (ie waiting for a worker, running, solving, etc.) See enums.StateStatus + status: StateStatus = StateStatus.waiting_for_worker + #: The last thing a state was doing. Allows us to swap back to this once it finishes solving. + _old_status: typing.Optional[StateStatus] = None + #: Total number of instruction executions in this state, including those in its parents + total_execs: typing.Optional[int] = None + #: Number of executions that took place in this state alone, excluding its parents + own_execs: typing.Optional[int] = None + #: Last program counter (if set) + pc: typing.Optional[typing.Any] = None + #: Dict mapping field names to the time that field was last updated + field_updated_at: typing.Dict[str, datetime] = field(default_factory=dict) + #: Message attached to the TerminateState exception that ended this state + termination_msg: typing.Optional[str] = None + + def __setattr__(self, key, value): + """ + Force updates the last_updated item any time a field is written to + """ + if key != "last_update": + super().__setattr__(key, value) + now = datetime.now() + # This calls setattr on the _dict_, so it doesn't cause an infinite loop + getattr(self, "field_updated_at", {})[key] = now + super().__setattr__("last_update", now) + + +class IntrospectionAPIPlugin(Plugin): + """ + Plugin that tracks the movements of States throughout the State lifecycle. Creates a StateDescriptor for each state + and stores them in its context, and keeps them up to date whenever a callback registers a change in the State. + """ + + def create_state(self, state_id: int): + """ + Adds a StateDescriptor to the context in the READY state list + + :param state_id: ID of the state + """ + assert state_id is not None + with self.locked_context("manticore_state", dict) as context: + context[state_id] = StateDescriptor(state_id=state_id, state_list=StateLists.ready) + + def will_run_callback(self, ready_states: typing.Generator): + """ + Called at the beginning of ManticoreBase.run(). Creates a state descriptor for each of the ready states. + + :param ready_states: Generator that allows us to iterate over the ready states (and modify them if necessary) + """ + for state in ready_states: + self.create_state(state.id) + + def did_enqueue_state_callback(self, state_id: int): + """ + Called whenever a state is added to the ready_states list. Creates a state descriptor. + + :param state_id: State ID of the new State + """ + logger.debug("did_enqueue_state: %s", state_id) + self.create_state(state_id) + + def did_transition_state_callback( + self, state_id: int, from_list: StateLists, to_list: StateLists + ): + """ + Called whenever a state moves from one state list to another. Updates the status based on which list the state + has been moved to. + + :param state_id: The ID of the state that was moved + :param from_list: The list the state used to be in + :param to_list: The list it's currently in + """ + logger.debug("did_transition_state %s: %s --> %s", state_id, from_list, to_list) + with self.locked_context("manticore_state", dict) as context: + if state_id not in context: + logger.warning( + "Got a state transition event for %s, but failed to capture its initialization", + state_id, + ) + state = context.setdefault( + state_id, StateDescriptor(state_id=state_id, state_list=from_list) + ) + if state.state_list != from_list: + logger.warning( + "Callbacks failed to capture state %s transitioning from %s to %s", + state_id, + state.state_list, + from_list, + ) + state.state_list = to_list + if to_list == StateLists.ready: + state.status = StateStatus.waiting_for_worker + elif to_list == StateLists.busy: + state.status = StateStatus.running + elif to_list in {StateLists.terminated, StateLists.killed}: + state.status = StateStatus.stopped + + def did_remove_state_callback(self, state_id: int): + """ + Called whenever a state was removed. As in, not terminated, not killed, but removed. This happens when we fork - + the parent state is removed and the children are enqueued. It can also be triggered manually if we really don't + like a state for some reason. Doesn't destroy the state descriptor, but updates its status and list accordingly. + + :param state_id: ID of the state that was removed + """ + logger.debug("did_remove_state: %s", state_id) + with self.locked_context("manticore_state", dict) as context: + if state_id not in context: + logger.warning( + "Removing state %s, but failed to capture its initialization", state_id + ) + else: + # Wipe the state list to indicate it's been deleted, but keep it around for record-keeping + desc = context[state_id] + desc.state_list = None + desc.status = StateStatus.destroyed + + def did_fork_state_callback( + self, state, expression, solutions, policy, children: typing.List[int] + ): + """ + Called upon each fork. Sets the children for each state. + + :param state: The parent state + :param expression: The expression we forked on + :param solutions: Possible values of the expression + :param policy: The policy used for finding solutions + :param children: the state IDs of the children + """ + state_id = state.id + logger.debug("did_fork_state: %s --> %s", state_id, children) + with self.locked_context("manticore_state", dict) as context: + if state_id not in context: + logger.warning( + "Forked state %s, but failed to capture its initialization", state_id + ) + context.setdefault(state_id, StateDescriptor(state_id=state_id)).children.update( + children + ) + + def will_solve_callback(self, state, constraints, expr, solv_func: str): + """ + Called when we're about to ask the solver for something. Updates the status of the state accordingly. + + :param state: State asking for the solve + :param constraints: Current constraint set used for solving + :param expr: Expression to be solved + :param solv_func: Which solver function is being used to find a solution + """ + if state is None: + logger.debug("Solve callback fired outside of a state, dropping...") + return + with self.locked_context("manticore_state", dict) as context: + if state.id not in context: + logger.warning( + "Caught will_solve in state %s, but failed to capture its initialization", + state.id, + ) + desc = context.setdefault(state.id, StateDescriptor(state_id=state.id)) + desc._old_status = desc.status + desc.status = StateStatus.waiting_for_solver + + def did_solve_callback(self, state, constraints, expr, solv_func: str, solutions): + """ + Called when we've finished solving. Sets the status of the state back to whatever it was. + + :param state: State asking for the solve + :param constraints: Current constraint set used for solving + :param expr: Expression to be solved + :param solv_func: Which solver function is being used to find a solution + :param solutions: the solved values for expr + """ + if state is None: + logger.debug("Solve callback fired outside of a state, dropping...") + return + with self.locked_context("manticore_state", dict) as context: + if state.id not in context: + logger.warning( + "Caught did_solve in state %s, but failed to capture its initialization", + state.id, + ) + desc = context[state.id] + desc.status = desc._old_status + + def on_execution_intermittent_callback( + self, state, update_cb: typing.Callable, *args, **kwargs + ): + """ + Called every n instructions, where n is config.core.execs_per_intermittent_cb. Calls the provided callback + to update platform-specific information on the descriptor. + + :param state: The state that raised the intermittent event + :param update_cb: Callback provided by the caller that will set some platform-specific fields on the state + descriptor. This could be PC for native, or something else for EVM + :param args: Optional args to pass to the callback + :param kwargs: Optional kwargs to pass to the callback + """ + with self.locked_context("manticore_state", dict) as context: + if state.id not in context: + logger.warning( + "Caught intermittent callback in state %s, but failed to capture its initialization", + state.id, + ) + update_cb( + context.setdefault(state.id, StateDescriptor(state_id=state.id)), *args, **kwargs, + ) + context[state.id].last_intermittent_update = datetime.now() + + def did_terminate_state_callback(self, state, ex: Exception): + """ + Capture TerminateState exceptions so we can get the messages attached + + :param state: State that was terminated + :param ex: The TerminateState exception w/ the termination message + """ + state_id = state.id + with self.locked_context("manticore_state", dict) as context: + if state_id not in context: + logger.warning( + "Caught termination of state %s, but failed to capture its initialization", + state_id, + ) + context.setdefault(state_id, StateDescriptor(state_id=state_id)).termination_msg = str( + ex + ) + + def get_state_descriptors(self) -> typing.Dict[int, StateDescriptor]: + """ + :return: the most up-to-date copy of the state descriptor dict available + """ + with self.locked_context("manticore_state", dict) as context: + out = context.copy() # TODO: is this necessary to break out of the lock? + return out diff --git a/manticore/core/state.py b/manticore/core/state.py index 93067d7723..96ae8cb9a4 100644 --- a/manticore/core/state.py +++ b/manticore/core/state.py @@ -4,7 +4,15 @@ from .smtlib import solver, Bool, issymbolic, BitVecConstant from ..utils.event import Eventful from ..utils.helpers import PickleSerializer +from ..utils import config +from .plugin import StateDescriptor +consts = config.get_group("core") +consts.add( + "execs_per_intermittent_cb", + default=1000, + description="How often to fire the `exec_intermittent` event", +) logger = logging.getLogger(__name__) @@ -90,6 +98,71 @@ def __init__(self, message, expression: Bool, **kwargs): super().__init__(message, expression, policy="ALL", **kwargs) +class EventSolver(Eventful): + """ + Wrapper around the solver that raises `will_solve` and `did_solve` around every call. Each call expands to: + ``` + def method_name(self, constraints, expression, *args, **kwargs): + self._publish("will_solve", constraints, expression, "method_name") + solved = SelectedSolver.instance().method_name(constraints, expression, *args, **kwargs) + self._publish("did_solve", constraints, expression, "method_name", solved) + return solved + ``` + """ + + _published_events = {"solve"} + + @property + def _solver(self): + from .smtlib import SelectedSolver + + return SelectedSolver.instance() # solver + + def can_be_true(self, constraints, expression, *args, **kwargs): + self._publish("will_solve", constraints, expression, "can_be_true") + solved = self._solver.can_be_true(constraints, expression, *args, **kwargs) + self._publish("did_solve", constraints, expression, "can_be_true", solved) + return solved + + def get_all_values(self, constraints, expression, *args, **kwargs): + self._publish("will_solve", constraints, expression, "get_all_values") + solved = self._solver.get_all_values(constraints, expression, *args, **kwargs) + self._publish("did_solve", constraints, expression, "get_all_values", solved) + return solved + + def get_value(self, constraints, expression, *args, **kwargs): + self._publish("will_solve", constraints, expression, "get_value") + solved = self._solver.get_value(constraints, expression, *args, **kwargs) + self._publish("did_solve", constraints, expression, "get_value", solved) + return solved + + def max(self, constraints, expression, *args, **kwargs): + self._publish("will_solve", constraints, expression, "max") + solved = self._solver.max(constraints, expression, *args, **kwargs) + self._publish("did_solve", constraints, expression, "max", solved) + return solved + + def min(self, constraints, expression, *args, **kwargs): + self._publish("will_solve", constraints, expression, "min") + solved = self._solver.min(constraints, expression, *args, **kwargs) + self._publish("did_solve", constraints, expression, "min", solved) + return solved + + def minmax(self, constraints, expression, *args, **kwargs): + self._publish("will_solve", constraints, expression, "minmax") + solved = self._solver.minmax(constraints, expression, *args, **kwargs) + self._publish("did_solve", constraints, expression, "minmax", solved) + return solved + + def __getattr__(self, item: str): + """ + Pass through any undefined attribute lookups to the underlying solver + :param item: The name of the field to get + :return: The item, if present on self._solver + """ + return getattr(self._solver, item) + + class StateBase(Eventful): """ Representation of a unique program state/path. @@ -99,6 +172,8 @@ class StateBase(Eventful): :ivar dict context: Local context for arbitrary data storage """ + _published_events = {"execution_intermittent"} + def __init__(self, constraints, platform, **kwargs): super().__init__(**kwargs) self._platform = platform @@ -108,8 +183,12 @@ def __init__(self, constraints, platform, **kwargs): self._child = None self._context = dict() self._terminated_by = None + self._solver = EventSolver() + self._total_exec = 0 + self._own_exec = 0 # 33 # Events are lost in serialization and fork !! + self.forward_events_from(self._solver) self.forward_events_from(platform) def __getstate__(self): @@ -120,6 +199,7 @@ def __getstate__(self): state["child"] = self._child state["context"] = self._context state["terminated_by"] = self._terminated_by + state["exec_counter"] = self._total_exec return state def __setstate__(self, state): @@ -130,8 +210,12 @@ def __setstate__(self, state): self._child = state["child"] self._context = state["context"] self._terminated_by = state["terminated_by"] + self._total_exec = state["exec_counter"] + self._own_exec = 0 + self._solver = EventSolver() # 33 # Events are lost in serialization and fork !! + self.forward_events_from(self._solver) self.forward_events_from(self._platform) @property @@ -151,6 +235,7 @@ def __enter__(self): new_state._input_symbols = list(self._input_symbols) new_state._context = copy.copy(self._context) new_state._id = None + new_state._total_exec = self._total_exec self.copy_eventful_state(new_state) self._child = new_state @@ -184,8 +269,23 @@ def constraints(self, constraints): self._constraints = constraints self.platform.constraints = constraints + def _update_state_descriptor(self, descriptor: StateDescriptor, *args, **kwargs): + """ + Called on execution_intermittent to update the descriptor for this state. This is intended for information + like the PC or instruction count, where updating after each instruction would be a waste of cycles. + This one updates the execution counts + + :param descriptor: StateDescriptor for this state + """ + descriptor.total_execs = self._total_exec + descriptor.own_execs = self._own_exec + def execute(self): - raise NotImplementedError + self._total_exec += 1 + self._own_exec += 1 + + if self._total_exec % consts.execs_per_intermittent_cb == 0: + self._publish("on_execution_intermittent", self._update_state_descriptor) def constrain(self, constraint): """Constrain state. @@ -318,12 +418,6 @@ def concretize(self, symbolic, policy, maxcount=7): return tuple(set(vals)) - @property - def _solver(self): - from .smtlib import SelectedSolver - - return SelectedSolver.instance() # solver - def migrate_expression(self, expression): if not issymbolic(expression): return expression diff --git a/manticore/core/worker.py b/manticore/core/worker.py index 2b6fe5e9bd..31270bdbcd 100644 --- a/manticore/core/worker.py +++ b/manticore/core/worker.py @@ -4,6 +4,7 @@ import multiprocessing import threading import os +import typing logger = logging.getLogger(__name__) @@ -229,3 +230,25 @@ def start(self): def join(self): self._p.join() self._p = None + + +class DaemonThread(WorkerThread): + """ + Special case of WorkerThread that will exit whenever the main Manticore process exits. + """ + + def start(self, target: typing.Optional[typing.Callable] = None): + """ + Function that starts the thread. Can take an optional callable to be invoked at the start, or can be subclassed, + in which case `target` should be None and the the `run` method will be invoked at the start. + + :param target: an optional callable that will be invoked to start the thread. The callable should accept this + thread as an argument. + """ + logger.debug( + "Starting Daemon %d. (Pid %d Tid %d).", self.id, os.getpid(), threading.get_ident(), + ) + + self._t = threading.Thread(target=self.run if target is None else target, args=(self,)) + self._t.daemon = True + self._t.start() diff --git a/manticore/core/workspace.py b/manticore/core/workspace.py index 2160f2e165..a4a711ae30 100644 --- a/manticore/core/workspace.py +++ b/manticore/core/workspace.py @@ -561,6 +561,7 @@ def _increment_id(self) -> int: @property def _last_id(self): + filename = ".testcase_id" try: with self._store.stream(filename, "r") as f: last_id = int(f.read()) @@ -658,5 +659,6 @@ def save_constraints(testcase, state: StateBase): def save_input_symbols(testcase, state: StateBase): with testcase.open_stream("input") as f: for symbol in state.input_symbols: - buf = SelectedSolver.instance().get_value(state.constraints, symbol) + # TODO - constrain=False here, so the extra migration shouldn't cause problems, right? + buf = state.solve_one(symbol) f.write(f"{symbol.name}: {buf!r}\n") diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index 388fe7b306..5fb64c6769 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -11,9 +11,9 @@ DetectExternalCallAndLeak, DetectEnvInstruction, DetectRaceCondition, - DetectorClassification, DetectManipulableBalance, ) +from ..utils.enums import DetectorClassification from ..core.plugin import Profiler from .manticore import ManticoreEVM from .plugins import ( diff --git a/manticore/ethereum/detectors.py b/manticore/ethereum/detectors.py index 78340966db..fd90e0ba24 100644 --- a/manticore/ethereum/detectors.py +++ b/manticore/ethereum/detectors.py @@ -1,6 +1,4 @@ -from manticore.core.smtlib.visitors import simplify import hashlib -from enum import Enum from typing import Optional import logging from contextlib import contextmanager @@ -15,23 +13,11 @@ taint_with, ) from ..core.plugin import Plugin - +from ..utils.enums import DetectorClassification logger = logging.getLogger(__name__) -class DetectorClassification(Enum): - """ - Shall be consistent with - https://github.com/trailofbits/slither/blob/563d5118298e4cae7f0ea5f2a531f0dcdcebd64d/slither/detectors/abstract_detector.py#L11-L15 - """ - - HIGH = 0 - MEDIUM = 1 - LOW = 2 - INFORMATIONAL = 3 - - class Detector(Plugin): # argument that needs to be passed to --detect to use given detector ARGUMENT: Optional[str] = None diff --git a/manticore/ethereum/manticore.py b/manticore/ethereum/manticore.py index 1ef66a3f88..b8fcb4bfe0 100644 --- a/manticore/ethereum/manticore.py +++ b/manticore/ethereum/manticore.py @@ -4,7 +4,6 @@ from multiprocessing import Queue, Process from queue import Empty as EmptyQueue from typing import Dict, Optional, Union -from enum import Enum import io import pyevmasm as EVMAsm import random @@ -13,7 +12,7 @@ from crytic_compile import CryticCompile, InvalidCompilation, is_supported -from ..core.manticore import ManticoreBase, Testcase, ManticoreError +from ..core.manticore import ManticoreBase, ManticoreError from ..core.smtlib import ( ConstraintSet, @@ -22,42 +21,25 @@ BitVec, Operators, BoolConstant, - BoolOperation, Expression, issymbolic, - simplify, SelectedSolver, ) -from ..core.state import TerminateState, AbandonState +from ..core.state import AbandonState from .account import EVMContract, EVMAccount, ABI from .detectors import Detector from .solidity import SolidityMetadata from .state import State from ..exceptions import EthereumError, DependencyError, NoAliveStates from ..platforms import evm -from ..utils import config, log +from ..utils import config from ..utils.deprecated import deprecated +from ..utils.enums import Sha3Type from ..utils.helpers import PickleSerializer, printable_bytes logger = logging.getLogger(__name__) logging.getLogger("CryticCompile").setLevel(logging.ERROR) - -class Sha3Type(Enum): - """Used as configuration constant for choosing sha3 flavor""" - - concretize = "concretize" - symbolicate = "symbolicate" - fake = "fake" - - def title(self): - return self._name_.title() - - @classmethod - def from_string(cls, name): - return cls.__members__[name] - - consts = config.get_group("evm") consts.add("defaultgas", 3000000, "Default gas value for ethereum transactions.") consts.add( @@ -135,6 +117,8 @@ class ManticoreEVM(ManticoreBase): m.finalize() """ + _published_events = {"solve"} + def make_symbolic_buffer(self, size, name=None, avoid_collisions=False): """ Creates a symbolic buffer of size bytes to be used in transactions. You can operate on it normally and add constraints to manticore.constraints @@ -586,7 +570,22 @@ def solidity_create_contract( constructor_data = b"" # Balance could be symbolic, lets ask the solver # Option 1: balance can not be 0 and the function is marked as not payable - if not SelectedSolver.instance().can_be_true(self.constraints, balance == 0): + maybe_balance = balance == 0 + self._publish( + "will_solve", None, self.constraints, maybe_balance, "can_be_true" + ) + must_have_balance = SelectedSolver.instance().can_be_true( + self.constraints, maybe_balance + ) + self._publish( + "did_solve", + None, + self.constraints, + maybe_balance, + "can_be_true", + must_have_balance, + ) + if not must_have_balance: # balance always != 0 if not md.constructor_abi["payable"]: raise EthereumError( @@ -597,10 +596,14 @@ def solidity_create_contract( for state in self.ready_states: world = state.platform - if not SelectedSolver.instance().can_be_true( - self.constraints, - Operators.UGE(world.get_balance(owner.address), balance), - ): + expr = Operators.UGE(world.get_balance(owner.address), balance) + self._publish("will_solve", None, self.constraints, expr, "can_be_true") + sufficient = SelectedSolver.instance().can_be_true(self.constraints, expr,) + self._publish( + "did_solve", None, self.constraints, expr, "can_be_true", sufficient + ) + + if not sufficient: raise EthereumError( f"Can't create solidity contract with balance ({balance}) " f"because the owner account ({owner}) has insufficient balance." @@ -1165,8 +1168,7 @@ def run(self, **kwargs): while saved_states: state_id = saved_states.pop() if state_id in self._terminated_states: - self._terminated_states.remove(state_id) - self._ready_states.append(state_id) + self._revive_state(state_id) # Callbacks def _on_concretize(self, state, func, data, result): @@ -1800,7 +1802,7 @@ def worker_finalize(q): for i in EVMAsm.disassemble_all(runtime_bytecode): if (address, i.pc) in seen: count += 1 - globalmanticore / ethereum / manticore.py_runtime_asm.write("*") + global_runtime_asm.write("*") else: global_runtime_asm.write(" ") @@ -1897,7 +1899,7 @@ def all_sound_states(self): """ self.fix_unsound_all() _ready_states = self._ready_states - for state_id in _all_states: + for state_id in _ready_states: state = self._load(state_id) if self.fix_unsound_symbolication(state): yield state diff --git a/manticore/ethereum/plugins.py b/manticore/ethereum/plugins.py index 83365dc22b..ee3a2fb409 100644 --- a/manticore/ethereum/plugins.py +++ b/manticore/ethereum/plugins.py @@ -6,6 +6,7 @@ from ..core.plugin import Plugin from ..core.smtlib import Operators, to_constant +from ..utils.enums import StateLists import pyevmasm as EVMAsm logger = logging.getLogger(__name__) @@ -105,7 +106,7 @@ def __init__(self, loop_count_threshold=5, **kwargs): super().__init__(**kwargs) self.loop_count_threshold = loop_count_threshold - def will_start_run_callback(self, *args): + def will_run_callback(self, *args): with self.manticore.locked_context("seen_rep", dict) as reps: reps.clear() @@ -217,8 +218,20 @@ def did_run_callback(self): st = self.manticore._load(state_id) if not st.context["written"][-1]: if st.id in self.manticore._ready_states: + self._publish( + "will_transition_state", + state_id, + StateLists.ready, + StateLists.terminated, + ) self.manticore._ready_states.remove(st.id) self.manticore._terminated_states.append(st.id) + self._publish( + "did_transition_state", + state_id, + StateLists.ready, + StateLists.terminated, + ) saved_states.remove(st.id) def generate_testcase(self, state, testcase, message): diff --git a/manticore/ethereum/state.py b/manticore/ethereum/state.py index 0c2a44a838..723b6def6d 100644 --- a/manticore/ethereum/state.py +++ b/manticore/ethereum/state.py @@ -1,6 +1,18 @@ from ..core.state import StateBase +from ..core.plugin import StateDescriptor class State(StateBase): def execute(self): + super().execute() return self._platform.execute() + + def _update_state_descriptor(self, descriptor: StateDescriptor, *args, **kwargs): + """ + Called on execution_intermittent to update the descriptor for this state. + This one should apply any EVM-specific information to the descriptor. + + :param descriptor: StateDescriptor for this state + """ + super()._update_state_descriptor(descriptor, *args, **kwargs) + descriptor.pc = None # TODO - Grab whatever notion of a PC EVM has diff --git a/manticore/native/cpu/abstractcpu.py b/manticore/native/cpu/abstractcpu.py index 57489de5cd..0ffeb2e4c5 100644 --- a/manticore/native/cpu/abstractcpu.py +++ b/manticore/native/cpu/abstractcpu.py @@ -496,6 +496,7 @@ class Cpu(Eventful): "protect_memory", "unmap_memory", "execute_syscall", + "solve", } def __init__(self, regfile: RegisterFile, memory: Memory, **kwargs): @@ -907,9 +908,10 @@ def decode_instruction(self, pc: int): vals = visitors.simplify_array_select(c) c = bytes([vals[0]]) except visitors.ArraySelectSimplifier.ExpressionNotSimple: - c = struct.pack( - "B", SelectedSolver.instance().get_value(self.memory.constraints, c) - ) + self._publish("will_solve", self.memory.constraints, c, "get_value") + solved = SelectedSolver.instance().get_value(self.memory.constraints, c) + self._publish("did_solve", self.memory.constraints, c, "get_value", solved) + c = struct.pack("B", solved) elif isinstance(c, Constant): c = bytes([c.value]) else: diff --git a/manticore/native/manticore.py b/manticore/native/manticore.py index 95827b7067..2e55f97ba5 100644 --- a/manticore/native/manticore.py +++ b/manticore/native/manticore.py @@ -9,7 +9,7 @@ from elftools.elf.elffile import ELFFile from elftools.elf.sections import SymbolTableSection -from .state import State +from .state import State, TerminateState from ..core.manticore import ManticoreBase from ..core.smtlib import ConstraintSet from ..core.smtlib.solver import SelectedSolver, issymbolic @@ -190,7 +190,7 @@ def _assertions_callback(self, state, pc, instruction): # This will interpret the buffer specification written in INTEL ASM. # (It may dereference pointers) assertion = parse(program, state.cpu.read_int, state.cpu.read_register) - if not SelectedSolver.instance().can_be_true(state.constraints, assertion): + if not state.can_be_true(assertion): logger.info(str(state.cpu)) logger.info( "Assertion %x -> {%s} does not hold. Aborting state.", state.cpu.pc, program @@ -384,6 +384,8 @@ def _make_linux( concrete_start="", pure_symbolic=False, stdin_size=None, + *args, + **kwargs, ) -> State: from ..platforms import linux diff --git a/manticore/native/memory.py b/manticore/native/memory.py index 6afea1a857..5f8ca25c4c 100644 --- a/manticore/native/memory.py +++ b/manticore/native/memory.py @@ -31,6 +31,7 @@ description="If True, throws a memory safety error if ANY concretization of a pointer is" " out of bounds. Otherwise, forks into valid and invalid memory access states.", ) +solver = SelectedSolver.instance() class MemoryException(Exception): @@ -1194,8 +1195,9 @@ def read(self, address, size, force=False): solutions = self._try_get_solutions(address, size, "r", force=force) assert len(solutions) > 0 except TooManySolutions as e: - solver = SelectedSolver.instance() + self.cpu._publish("will_solve", self.constraints, address, "minmax") m, M = solver.minmax(self.constraints, address) + self.cpu._publish("did_solve", self.constraints, address, "minmax", (m, M)) logger.debug( f"Got TooManySolutions on a symbolic read. Range [{m:x}, {M:x}]. Not crashing!" ) @@ -1210,7 +1212,12 @@ def read(self, address, size, force=False): crashing_condition, ) - if solver.can_be_true(self.constraints, crashing_condition): + self.cpu._publish("will_solve", self.constraints, crashing_condition, "can_be_true") + can_crash = solver.can_be_true(self.constraints, crashing_condition) + self.cpu._publish( + "did_solve", self.constraints, crashing_condition, "can_be_true", can_crash + ) + if can_crash: raise InvalidSymbolicMemoryAccess(address, "r", size, crashing_condition) # INCOMPLETE Result! We could also fork once for every map @@ -1327,17 +1334,22 @@ def _try_get_solutions(self, address, size, access, max_solutions=0x1000, force= :rtype: list """ assert issymbolic(address) - solver = SelectedSolver.instance() + self.cpu._publish("will_solve", self.constraints, address, "get_all_values") solutions = solver.get_all_values( self.constraints, address, maxcnt=max_solutions, silent=True ) + self.cpu._publish("did_solve", self.constraints, address, "get_all_values", solutions) crashing_condition = False for base in solutions: if not self.access_ok(slice(base, base + size), access, force): crashing_condition = Operators.OR(address == base, crashing_condition) + self.cpu._publish("will_solve", self.constraints, crashing_condition, "get_all_values") crash_or_not = solver.get_all_values(self.constraints, crashing_condition, maxcnt=3) + self.cpu._publish( + "did_solve", self.constraints, crashing_condition, "get_all_values", crash_or_not + ) if not consts.fast_crash and len(crash_or_not) == 2: from ..core.state import Concretize @@ -1437,9 +1449,13 @@ def _deref_can_succeed(self, mapping, address, size): if not issymbolic(address): return address >= mapping.start and address + size < mapping.end else: - solver = SelectedSolver.instance() constraint = Operators.AND(address >= mapping.start, address + size < mapping.end) - return solver.can_be_true(self.constraints, constraint) + self.cpu._publish("will_solve", self.constraints, constraint, "can_be_true") + deref_can_succeed = solver.can_be_true(self.constraints, constraint) + self.cpu._publish( + "did_solve", self.constraints, constraint, "can_be_true", deref_can_succeed + ) + return deref_can_succeed def _import_concrete_memory(self, from_addr, to_addr): """ @@ -1475,8 +1491,11 @@ def _map_deref_expr(self, map, address): return Operators.AND(Operators.UGE(address, map.start), Operators.ULT(address, map.end)) def _reachable_range(self, sym_address, size): - solver = SelectedSolver.instance() + self.cpu._publish("will_solve", self.constraints, sym_address, "minmax") addr_min, addr_max = solver.minmax(self.constraints, sym_address) + self.cpu._publish( + "did_solve", self.constraints, sym_address, "minmax", (addr_min, addr_max) + ) return addr_min, addr_max + size - 1 def valid_ptr(self, address): diff --git a/manticore/native/models.py b/manticore/native/models.py index cc9c76dcbd..8c9b7e2c92 100644 --- a/manticore/native/models.py +++ b/manticore/native/models.py @@ -5,7 +5,6 @@ from .cpu.abstractcpu import Cpu, ConcretizeArgument from .state import State from ..core.smtlib import issymbolic, BitVec -from ..core.smtlib.solver import SelectedSolver from ..core.smtlib.operators import ITEBV, ZEXTEND from ..core.state import Concretize from typing import Union @@ -34,7 +33,7 @@ def variadic(func): return func -def is_definitely_NULL(byte, constrs) -> bool: +def must_be_NULL(state, byte) -> bool: """ Checks if a given byte read from memory is NULL. This supports both concrete & symbolic byte values. @@ -44,12 +43,12 @@ def is_definitely_NULL(byte, constrs) -> bool: :return: whether a given byte is NULL or constrained to NULL """ if issymbolic(byte): - return SelectedSolver.instance().must_be_true(constrs, byte == 0) + return state.must_be_true(byte == 0) else: return byte == 0 -def cannot_be_NULL(byte, constrs) -> bool: +def cannot_be_NULL(state, byte) -> bool: """ Checks if a given byte read from memory is not NULL or cannot be NULL @@ -58,12 +57,12 @@ def cannot_be_NULL(byte, constrs) -> bool: :return: whether a given byte is not NULL or cannot be NULL """ if issymbolic(byte): - return SelectedSolver.instance().must_be_true(constrs, byte != 0) + return state.must_be_true(byte != 0) else: return byte != 0 -def can_be_NULL(byte, constrs) -> bool: +def can_be_NULL(state, byte) -> bool: """ Checks if a given byte read from memory can be NULL @@ -72,12 +71,12 @@ def can_be_NULL(byte, constrs) -> bool: :return: whether a given byte is NULL or can be NULL """ if issymbolic(byte): - return SelectedSolver.instance().can_be_true(constrs, byte == 0) + return state.can_be_true(byte == 0) else: return byte == 0 -def _find_zero(cpu, constrs, ptr: Union[int, BitVec]) -> int: +def _find_zero(cpu, state, ptr: Union[int, BitVec]) -> int: """ Helper for finding the closest NULL or, effectively NULL byte from a starting address. @@ -90,7 +89,7 @@ def _find_zero(cpu, constrs, ptr: Union[int, BitVec]) -> int: offset = 0 while True: byte = cpu.read_int(ptr + offset, 8) - if is_definitely_NULL(byte, constrs): + if must_be_NULL(state, byte): break offset += 1 @@ -129,8 +128,8 @@ def strcmp(state: State, s1: Union[int, BitVec], s2: Union[int, BitVec]): if issymbolic(s2): raise ConcretizeArgument(state.cpu, 2) - s1_zero_idx = _find_zero(cpu, state.constraints, s1) - s2_zero_idx = _find_zero(cpu, state.constraints, s2) + s1_zero_idx = _find_zero(cpu, state, s1) + s2_zero_idx = _find_zero(cpu, state, s2) min_zero_idx = min(s1_zero_idx, s2_zero_idx) ret = None @@ -171,7 +170,6 @@ def strlen_exact(state: State, s: Union[int, BitVec]) -> Union[int, BitVec]: raise ConcretizeArgument(state.cpu, 1) cpu = state.cpu - constrs = state.constraints # Initialize offset based on whether state has been forked in strlen if "strlen" not in state.context: @@ -180,9 +178,9 @@ def strlen_exact(state: State, s: Union[int, BitVec]) -> Union[int, BitVec]: offset = state.context["strlen"] c = cpu.read_int(s + offset, 8) - while not is_definitely_NULL(c, constrs): + while not must_be_NULL(state, c): # If the byte can be NULL concretize and fork states - if can_be_NULL(c, constrs): + if can_be_NULL(state, c): state.context["strlen"] = offset raise Concretize("Forking on possible NULL strlen", expression=(c == 0), policy="ALL") @@ -209,7 +207,7 @@ def strlen_approx(state: State, s: Union[int, BitVec]) -> Union[int, BitVec]: raise ConcretizeArgument(state.cpu, 1) cpu = state.cpu - zero_idx = _find_zero(cpu, state.constraints, s) + zero_idx = _find_zero(cpu, state, s) ret = zero_idx @@ -241,7 +239,6 @@ def strcpy(state: State, dst: Union[int, BitVec], src: Union[int, BitVec]) -> Un raise ConcretizeArgument(state.cpu, 1) cpu = state.cpu - constrs = state.constraints ret = dst # Initialize offset based on whether state has been forked in strcpy @@ -252,11 +249,11 @@ def strcpy(state: State, dst: Union[int, BitVec], src: Union[int, BitVec]) -> Un # Copy until a src_byte is symbolic and constrained to '\000', or is concrete and '\000' src_val = cpu.read_int(src + offset, 8) - while not is_definitely_NULL(src_val, constrs): + while not must_be_NULL(state, src_val): cpu.write_int(dst + offset, src_val, 8) # If a src byte can be NULL concretize and fork states - if can_be_NULL(src_val, constrs): + if can_be_NULL(state, src_val): state.context["strcpy"] = offset raise Concretize("Forking on NULL strcpy", expression=(src_val == 0), policy="ALL") offset += 1 @@ -295,7 +292,6 @@ def strncpy( raise ConcretizeArgument(state.cpu, 3) cpu = state.cpu - constrs = state.constraints ret = dst # Initialize offset based on whether state has been forked in strncpy @@ -306,11 +302,11 @@ def strncpy( # Copy until a src_byte is symbolic and constrained to '\000', or is concrete and '\000' src_val = cpu.read_int(src + offset, 8) - while offset < n and not is_definitely_NULL(src_val, constrs): + while offset < n and not must_be_NULL(state, src_val): cpu.write_int(dst + offset, src_val, 8) # If a src byte can be NULL concretize and fork states - if can_be_NULL(src_val, constrs): + if can_be_NULL(state, src_val): state.context["strncpy"] = offset raise Concretize("Forking on NULL strncpy", expression=(src_val == 0), policy="ALL") offset += 1 diff --git a/manticore/native/plugins.py b/manticore/native/plugins.py index d28454efbf..939f5cb973 100644 --- a/manticore/native/plugins.py +++ b/manticore/native/plugins.py @@ -10,7 +10,7 @@ def on_register(self): p = self.manticore._publish self.manticore._publish = lambda *args, **kwargs: None for state in self.manticore.ready_states: - self.did_fork_state_callback(state, None, None, None) + self.did_fork_state_callback(state, None, None, None, None) self.manticore._publish = p @@ -30,9 +30,7 @@ def delete_state(self, state_id): :param state_id: state-id for state that is being deleted :return: None """ - with self.manticore._lock: - self.manticore._ready_states.remove(state_id) - self.manticore._remove(state_id) + self.manticore.kill_state(state_id, delete=True) def replace_state(self, state_id, state): """ @@ -43,7 +41,7 @@ def replace_state(self, state_id, state): """ return self.manticore._save(state, state_id=state_id) - def did_fork_state_callback(self, state, expression, new_value, policy): + def did_fork_state_callback(self, state, expression, new_value, policy, children): state_id = state.id """That means no one else has to offer one Message Input diff --git a/manticore/native/state.py b/manticore/native/state.py index da0f6930be..cb470f3093 100644 --- a/manticore/native/state.py +++ b/manticore/native/state.py @@ -37,6 +37,7 @@ def execute(self): """ Perform a single step on the current state """ + super().execute() from .cpu.abstractcpu import ( ConcretizeRegister, ) # must be here, otherwise we get circular imports @@ -96,3 +97,13 @@ def invoke_model(self, model): :param model: callable, model to invoke """ self._platform.invoke_model(model, prefix_args=(self,)) + + def _update_state_descriptor(self, descriptor, *args, **kwargs): + """ + Called on execution_intermittent to update the descriptor for this state. + This one should apply any native-specific information to the descriptor. Right now, that's just the PC + + :param descriptor: StateDescriptor for this state + """ + super()._update_state_descriptor(descriptor, *args, **kwargs) + descriptor.pc = self.cpu.PC diff --git a/manticore/platforms/evm.py b/manticore/platforms/evm.py index f65c1cac53..7b43ddbbf8 100644 --- a/manticore/platforms/evm.py +++ b/manticore/platforms/evm.py @@ -647,6 +647,7 @@ class EVM(Eventful): "evm_write_code", "decode_instruction", "on_unsound_symbolication", + "solve", } class transact: @@ -1239,9 +1240,17 @@ def _check_jmpdest(self): if isinstance(should_check_jumpdest, Constant): should_check_jumpdest = should_check_jumpdest.value elif issymbolic(should_check_jumpdest): + self._publish("will_solve", self.constraints, should_check_jumpdest, "get_all_values") should_check_jumpdest_solutions = SelectedSolver.instance().get_all_values( self.constraints, should_check_jumpdest ) + self._publish( + "did_solve", + self.constraints, + should_check_jumpdest, + "get_all_values", + should_check_jumpdest_solutions, + ) if len(should_check_jumpdest_solutions) != 1: raise EthereumError("Conditional not concretized at JMPDEST check") should_check_jumpdest = should_check_jumpdest_solutions[0] @@ -1727,7 +1736,10 @@ def CALLDATACOPY(self, mem_offset, data_offset, size): if consts.oog == "complete": # gas reduced #?? cond = Operators.ULT(self.gas, self._checkpoint_data[1]) - if not SelectedSolver.instance().can_be_true(self.constraints, cond): + self._publish("will_solve", self.constraints, cond, "can_be_true") + enough_gas = SelectedSolver.instance().can_be_true(self.constraints, cond) + self._publish("did_solve", self.constraints, cond, "can_be_true", enough_gas) + if not enough_gas: raise NotEnoughGas() self.constraints.add(cond) @@ -1736,7 +1748,9 @@ def CALLDATACOPY(self, mem_offset, data_offset, size): max_size = size if issymbolic(max_size): + self._publish("will_solve", self.constraints, size, "max") max_size = SelectedSolver.instance().max(self.constraints, size) + self._publish("did_solve", self.constraints, size, "max", max_size) if calldata_overflow is not None: cap = len(self.data) + calldata_overflow @@ -1784,7 +1798,9 @@ def CODECOPY(self, mem_offset, code_offset, size): self._consume(copyfee) if issymbolic(size): + self._publish("will_solve", self.constraints, size, "max") max_size = SelectedSolver.instance().max(self.constraints, size) + self._publish("did_solve", self.constraints, size, "max", max_size) else: max_size = size @@ -2393,6 +2409,7 @@ class EVMWorld(Platform): "open_transaction", "close_transaction", "symbolic_function", + "solve", } def __init__(self, constraints, fork=DEFAULT_FORK, **kwargs): @@ -2450,9 +2467,13 @@ def try_simplify_to_constant(self, data): concrete_data.append(simplified.value) else: # simplify by solving. probably means that we need to improve simplification + self._publish("will_solve", self.constraints, simplified, "get_all_values") solutions = SelectedSolver.instance().get_all_values( self.constraints, simplified, 2, silent=True ) + self._publish( + "did_solve", self.constraints, simplified, "get_all_values", solutions + ) if len(solutions) != 1: break concrete_data.append(solutions[0]) @@ -2475,7 +2496,9 @@ def symbolic_function(self, func, data): return result[0] except Exception as e: logger.info("Error! %r", e) + self._publish("will_solve", self.constraints, data, "get_value") data_c = SelectedSolver.instance().get_value(self.constraints, data) + self._publish("did_solve", self.constraints, data, "get_value", data_c) return int(sha3.keccak_256(data_c).hexdigest(), 16) @property @@ -3419,7 +3442,9 @@ def dump(self, stream, state, mevm, message): # temp_cs.add(storage.get(index) != 0) temp_cs.add(storage.is_known(index)) # Query the solver to get all storage indexes with used slots + self._publish("will_solve", temp_cs, index, "get_all_values") all_used_indexes = SelectedSolver.instance().get_all_values(temp_cs, index) + self._publish("did_solve", temp_cs, index, "get_all_values", all_used_indexes) if all_used_indexes: stream.write("Storage:\n") diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index bc2e88f016..153c414e58 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -2299,7 +2299,9 @@ def sys_writev(self, fd, iov, count): size = cpu.read_int(iov + i * sizeof_iovec + (sizeof_iovec // 2), ptrsize) if issymbolic(size): + self._publish("will_solve", self.constraints, size, "get_value") size = SelectedSolver.instance().get_value(self.constraints, size) + self._publish("did_solve", self.constraints, size, "get_value", size) data = [Operators.CHR(cpu.read_int(buf + i, 8)) for i in range(size)] data = self._transform_write_data(data) @@ -3247,7 +3249,9 @@ def _transform_write_data(self, data: MixedSymbolicBuffer) -> bytes: for c in data: if issymbolic(c): bytes_concretized += 1 + self._publish("will_solve", self.constraints, c, "get_value") c = bytes([SelectedSolver.instance().get_value(self.constraints, c)]) + self._publish("did_solve", self.constraints, c, "get_value", c) concrete_data += cast(bytes, c) if bytes_concretized > 0: @@ -3259,7 +3263,9 @@ def _transform_write_data(self, data: MixedSymbolicBuffer) -> bytes: def sys_exit_group(self, error_code): if issymbolic(error_code): + self._publish("will_solve", self.constraints, error_code, "get_value") error_code = SelectedSolver.instance().get_value(self.constraints, error_code) + self._publish("did_solve", self.constraints, error_code, "get_value", error_code) return self._exit( f"Program finished with exit status: {ctypes.c_int32(error_code).value} (*)" ) @@ -3455,7 +3461,9 @@ def make_chr(c): try: for c in data: if issymbolic(c): + self._publish("will_solve", self.constraints, c, "get_value") c = SelectedSolver.instance().get_value(self.constraints, c) + self._publish("did_solve", self.constraints, c, "get_value", c) fd.write(make_chr(c)) except SolverError: fd.write("{SolverError}") diff --git a/manticore/platforms/platform.py b/manticore/platforms/platform.py index d54ca4d30a..9be3edcb3f 100644 --- a/manticore/platforms/platform.py +++ b/manticore/platforms/platform.py @@ -48,6 +48,8 @@ class Platform(Eventful): Base class for all platforms e.g. operating systems or virtual machines. """ + _published_events = {"solve"} + def __init__(self, path, **kwargs): super().__init__(**kwargs) diff --git a/manticore/utils/command_line.py b/manticore/utils/command_line.py index d139d8bd08..570fa42536 100644 --- a/manticore/utils/command_line.py +++ b/manticore/utils/command_line.py @@ -4,7 +4,7 @@ """ from prettytable import PrettyTable -from ..ethereum.detectors import DetectorClassification +from .enums import DetectorClassification classification_txt = { DetectorClassification.INFORMATIONAL: "Informational", diff --git a/manticore/utils/emulate.py b/manticore/utils/emulate.py index 47a294cf87..9a77b8b84b 100644 --- a/manticore/utils/emulate.py +++ b/manticore/utils/emulate.py @@ -55,7 +55,7 @@ class ConcreteUnicornEmulator: implementations in Manticore. This Emulator is instead intended to completely replace Manticore's executor when operating on purely concrete data. - To use the emulator, register a callback for the will_start_run event that calls `state.cpu.emulate_until` with an + To use the emulator, register a callback for the will_run event that calls `state.cpu.emulate_until` with an address at which it should switch back from Unicorn to Manticore. Passing 0 will result in the entire target being executed concretely. diff --git a/manticore/utils/enums.py b/manticore/utils/enums.py new file mode 100644 index 0000000000..ee994d1b6f --- /dev/null +++ b/manticore/utils/enums.py @@ -0,0 +1,71 @@ +from enum import Enum + + +class StateLists(Enum): + """ + The set of StateLists tracked in ManticoreBase + """ + + ready = "READY" + busy = "BUSY" + terminated = "TERMINATED" + killed = "KILLED" + + +class StateStatus(Enum): + """ + Statuses that a StateDescriptor can have + """ + + waiting_for_worker = "waiting_for_worker" + waiting_for_solver = "waiting_for_solver" + running = "running" + #: Killed OR Terminated + stopped = "stopped" + #: Removed + destroyed = "destroyed" + + +class MProcessingType(Enum): + """Used as configuration constant for choosing multiprocessing flavor""" + + multiprocessing = "multiprocessing" + single = "single" + threading = "threading" + + def title(self): + return self._name_.title() + + @classmethod + def from_string(cls, name): + return cls.__members__[name] + + def to_class(self): + return globals()[f"Manticore{self.title()}"] + + +class Sha3Type(Enum): + """Used as configuration constant for choosing sha3 flavor""" + + concretize = "concretize" + symbolicate = "symbolicate" + fake = "fake" + + def title(self): + return self._name_.title() + + @classmethod + def from_string(cls, name): + return cls.__members__[name] + + +class DetectorClassification(Enum): + """ + Shall be consistent with + https://github.com/trailofbits/slither/blob/563d5118298e4cae7f0ea5f2a531f0dcdcebd64d/slither/detectors/abstract_detector.py#L11-L15 + """ + + HIGH = 0 + MEDIUM = 1 + LOW = 2 + INFORMATIONAL = 3 diff --git a/manticore/utils/event.py b/manticore/utils/event.py index 2e7e035173..e486205234 100644 --- a/manticore/utils/event.py +++ b/manticore/utils/event.py @@ -5,6 +5,7 @@ from typing import Dict, Set from itertools import takewhile from weakref import WeakKeyDictionary, ref +from inspect import isgenerator logger = logging.getLogger(__name__) @@ -146,10 +147,9 @@ def _publish(self, _name, *args, can_raise=True, **kwargs): self._check_event(_name) self._publish_impl(_name, *args, **kwargs) except Exception as e: + logger.warning("Exception raised in callback: %s", e) if can_raise: raise - else: - logger.info("Exception raised at a callback %r", e) # Separate from _publish since the recursive method call to forward an event # shouldn't check the event. @@ -157,7 +157,13 @@ def _publish_impl(self, _name, *args, **kwargs): bucket = self._get_signal_bucket(_name) for robj, methods in bucket.items(): for callback in methods: - callback(robj(), *args, **kwargs) + # Need to clone any iterable args, otherwise the first usage will drain it. + # If the generator isn't available on `self`, give up and return it anyway. + new_args = ( + (arg if not isgenerator(arg) else getattr(self, arg.__name__, arg)) + for arg in args + ) + callback(robj(), *new_args, **kwargs) # The include_source flag indicates to prepend the source of the event in # the callback signature. This is set on forward_events_from/to diff --git a/manticore/utils/helpers.py b/manticore/utils/helpers.py index b3982839b2..5c918b3ec2 100644 --- a/manticore/utils/helpers.py +++ b/manticore/utils/helpers.py @@ -5,10 +5,13 @@ from collections import OrderedDict from gzip import GzipFile from io import BytesIO +from prettytable import PrettyTable +from datetime import datetime -from typing import Any, IO +from typing import Any, IO, Dict from .config import get_group +from .enums import StateLists logger = logging.getLogger(__name__) @@ -145,3 +148,55 @@ def pickle_dump(obj: Any, fp: IO[bytes]) -> None: Serializes an object as a gzipped pickle to the given file. """ return pickle.dump(obj, fp, protocol=pickle.HIGHEST_PROTOCOL) + + +def pretty_print_state_descriptors(desc: Dict): + """ + Given a dict of state descriptors, nicely formats and prints it to stdout. + :param desc: Dict mapping state IDs to State Descriptors, like the one returned from MantioreBase.introspect + """ + + descriptors = desc.values() + nready, nbusy, nkill, nterm = 0, 0, 0, 0 + for st in descriptors: + nready += 1 if (st.state_list == StateLists.ready) else 0 + nbusy += 1 if (st.state_list == StateLists.busy) else 0 + nkill += 1 if (st.state_list == StateLists.busy) else 0 + nterm += 1 if (st.state_list == StateLists.terminated) else 0 + + print( + "Ready States:", + nready, + " | ", + "Busy States:", + nbusy, + " | ", + "Terminated States:", + nterm, + " | ", + "Killed States:", + nkill, + ) + + tab = PrettyTable() + tab.field_names = ["ID", "Status", "Duration", "Execs", "Execs/Sec"] + if nbusy: + now = datetime.now() + for st in descriptors: + if st.state_list == StateLists.busy: + duration = ( + now - st.field_updated_at["state_list"] + ) # Time since this state became Busy + execs = st.own_execs if st.own_execs is not None else 0 + tab.add_row( + [ + st.state_id, + st.status.value, + str(duration)[:-4], + execs, + "{:.2f}".format(execs / (now - st.created_at).total_seconds()), + ] + ) + + print(tab) + print() diff --git a/manticore/wasm/executor.py b/manticore/wasm/executor.py index dd6eeede7a..4bab43dffb 100644 --- a/manticore/wasm/executor.py +++ b/manticore/wasm/executor.py @@ -43,7 +43,7 @@ class Executor(Eventful): _published_events = {"set_global", "get_global", "set_local", "get_local"} - def __init__(self, constraints, *args, **kwargs): + def __init__(self, *args, **kwargs): self._mapping = { 0x00: self.unreachable, @@ -220,9 +220,6 @@ def __init__(self, constraints, *args, **kwargs): 0xBF: self.f64_reinterpret_i64, } - #: Constraint set to use for checking overflows and boundary conditions - self.constraints = constraints - self.zero_div = False self.overflow = False @@ -231,14 +228,12 @@ def __init__(self, constraints, *args, **kwargs): def __getstate__(self): state = super().__getstate__() state["mapping"] = self._mapping - state["constraints"] = self.constraints state["zero_div"] = self.zero_div state["overflow"] = self.overflow return state def __setstate__(self, state): self._mapping = state["mapping"] - self.constraints = state["constraints"] self.zero_div = state["zero_div"] self.overflow = state["overflow"] super().__setstate__(state) diff --git a/manticore/wasm/manticore.py b/manticore/wasm/manticore.py index 8826c8e4c0..a90f894639 100644 --- a/manticore/wasm/manticore.py +++ b/manticore/wasm/manticore.py @@ -87,8 +87,7 @@ def f(argv_generator=None): with self.locked_context("wasm.saved_states", list) as saved_states: while saved_states: state_id = saved_states.pop() - self._terminated_states.remove(state_id) - self._ready_states.append(state_id) + self._revive_state(state_id) if argv_generator is not None: self.invoke(item, argv_generator) @@ -156,27 +155,13 @@ def collect_returns(self, n=1): ret = None if not p.stack.empty(): ret = p.stack.pop() + # TODO - eventually we'll need to support floats as well. + # That'll probably require us to subclass bitvecs into IxxBV and FxxBV if issymbolic(ret): if ret.size == 32: - inner.append( - list( - I32(a) # TODO - eventually we'll need to support floats as well. - for a in SelectedSolver.instance().get_all_values( - state.constraints, ret - ) - ) - ) + inner.append(list(I32(a) for a in state.solve_n(ret, n))) elif ret.size == 64: - inner.append( - list( - I64( - a - ) # TODO - that'll probably require us to subclass bitvecs into IxxBV and FxxBV - for a in SelectedSolver.instance().get_all_values( - state.constraints, ret - ) - ) - ) + inner.append(list(I64(a) for a in state.solve_n(ret, n))) else: inner.append([ret]) outer.append(inner) @@ -205,8 +190,7 @@ def _reinit(self): with self.locked_context("wasm.saved_states", list) as saved_states: while saved_states: state_id = saved_states.pop() - self._terminated_states.remove(state_id) - self._ready_states.append(state_id) + self._revive_state(state_id) def generate_testcase(self, state, message="test", name="test"): testcase = super().generate_testcase(state, message) diff --git a/manticore/wasm/state.py b/manticore/wasm/state.py index 2173c9e537..9a462364ab 100644 --- a/manticore/wasm/state.py +++ b/manticore/wasm/state.py @@ -42,4 +42,5 @@ def locals(self): return frame.locals def execute(self): + super().execute() return self._platform.execute(self) diff --git a/manticore/wasm/structure.py b/manticore/wasm/structure.py index 667b052f2b..129d0eebd5 100644 --- a/manticore/wasm/structure.py +++ b/manticore/wasm/structure.py @@ -729,10 +729,9 @@ def __setstate__(self, state): self.globals = state["globals"] -def _eval_maybe_symbolic(constraints, expression) -> bool: +def _eval_maybe_symbolic(state, expression) -> bool: if issymbolic(expression): - solver = SelectedSolver.instance() - return solver.must_be_true(constraints, expression) + return state.must_be_true(expression) return True if expression else False @@ -806,7 +805,7 @@ def __init__(self, constraints=None): self.globaladdrs = [] self.exports = [] self.export_map = {} - self.executor = Executor(constraints) + self.executor = Executor() self.function_names = {} self.local_names = {} self._instruction_queue = deque() @@ -1274,12 +1273,12 @@ def exec_instruction( self._publish("will_execute_instruction", inst) if 0x2 <= inst.opcode <= 0x11: # This is a control-flow instruction self.executor.zero_div = _eval_maybe_symbolic( - self.executor.constraints, self.executor.zero_div + self._state, self.executor.zero_div ) if self.executor.zero_div: raise ZeroDivisionTrap() self.executor.overflow = _eval_maybe_symbolic( - self.executor.constraints, self.executor.overflow + self._state, self.executor.overflow ) if self.executor.overflow: raise OverflowDivisionTrap() diff --git a/tests/native/test_models.py b/tests/native/test_models.py index a3e5f498c8..2b41cafbf9 100644 --- a/tests/native/test_models.py +++ b/tests/native/test_models.py @@ -24,7 +24,7 @@ strlen_approx, strcpy, strncpy, - is_definitely_NULL, + must_be_NULL, cannot_be_NULL, ) @@ -296,14 +296,14 @@ def _assert_concrete(self, s, d): src = cpu.read_int(s, 8) dst = cpu.read_int(d, 8) offset = 0 - while cannot_be_NULL(src, self.state.constraints): + while cannot_be_NULL(self.state, src): self.assertEqual(src, dst) offset += 1 src = cpu.read_int(s + offset, 8) dst = cpu.read_int(d + offset, 8) # Assert final NULL byte - self.assertTrue(is_definitely_NULL(src, self.state.constraints)) + self.assertTrue(must_be_NULL(self.state, src)) self.assertEqual(0, dst) def _test_strcpy(self, string, dst_len=None): @@ -421,7 +421,7 @@ def _assert_concrete(self, s, d, n): offset = 0 # Check that min(n, length of src) characters are copied from src to dst - while not is_definitely_NULL(src, self.state.constraints) and offset < n: + while not must_be_NULL(self.state, src) and offset < n: self.assertEqual(src, dst) offset += 1 src = cpu.read_int(s + offset, 8) diff --git a/tests/native/test_unicorn_concrete.py b/tests/native/test_unicorn_concrete.py index f0fe1d41aa..ec8971ec6e 100644 --- a/tests/native/test_unicorn_concrete.py +++ b/tests/native/test_unicorn_concrete.py @@ -6,8 +6,8 @@ class ConcretePlugin(Plugin): - def will_run_callback(self, *_args): - for state in self.manticore.ready_states: + def will_run_callback(self, ready_states): + for state in ready_states: state.cpu.emulate_until(0) @@ -85,11 +85,15 @@ def test_register_comparison(self): concrete_regs = {} normal_regs = {} - for st in self.m.all_states: + self.assertEqual( + len(list(self.m.terminated_states)), len(list(self.concrete_instance.terminated_states)) + ) + self.assertGreater(len(list(self.m.terminated_states)), 0) + for st in self.m.terminated_states: for reg in should_match: normal_regs[reg] = getattr(st.platform.current, reg) - for st in self.concrete_instance.all_states: + for st in self.concrete_instance.terminated_states: for reg in should_match: concrete_regs[reg] = getattr(st.platform.current, reg) diff --git a/tests/other/test_state_introspection.py b/tests/other/test_state_introspection.py new file mode 100644 index 0000000000..dacbbce4d7 --- /dev/null +++ b/tests/other/test_state_introspection.py @@ -0,0 +1,89 @@ +import unittest +from manticore.native import Manticore +from manticore.core.plugin import IntrospectionAPIPlugin, StateDescriptor +from pathlib import Path +from time import sleep +from manticore.utils.enums import StateLists +import io +import contextlib + +ms_file = str( + Path(__file__).parent.parent.parent.joinpath("examples", "linux", "binaries", "multiple-styles") +) + + +class TestDaemonThread(unittest.TestCase): + def daemon(self, _thread): + while True: + self.fired = True + sleep(1) + + def test_daemon(self): + self.fired = False + m = Manticore(ms_file, stdin_size=17) + m.register_daemon(self.daemon) + m.run() + + self.assertTrue(self.fired) + + +class TestIntrospect(unittest.TestCase): + def introspect_loop(self, thread): + while True: + self.history.append(thread.manticore.introspect()) + sleep(0.5) + + def test_introspect_daemon(self): + self.history = [] + m = Manticore(ms_file, stdin_size=17) + m.register_daemon(self.introspect_loop) + m.run() + + sleep(1) # Leave time for the callback to fire after we've finished + self.assertGreater(len(self.history), 0) + progression = [] + for hist in self.history: + hist = hist.values() + progression.append( + ( + sum(1 if (st.state_list == StateLists.ready) else 0 for st in hist), + sum(1 if (st.state_list == StateLists.busy) else 0 for st in hist), + sum(1 if (st.state_list == StateLists.terminated) else 0 for st in hist), + ) + ) + self.assertEqual(progression[-1][0], 0) # Once finished, we have no ready states + self.assertEqual(progression[-1][1], 0) # Once finished, we have no busy states + # Once finished, we have only terminated states. + self.assertGreater(progression[-1][2], 0) + + f = io.StringIO() + with contextlib.redirect_stdout(f): + m.pretty_print_states() + self.assertIn("Terminated States: {}".format(progression[-1][2]), f.getvalue()) + + +class MyIntrospector(IntrospectionAPIPlugin): + def on_execution_intermittent_callback(self, state, update_cb, *args, **kwargs): + super().on_execution_intermittent_callback(state, update_cb, *args, **kwargs) + with self.locked_context("manticore_state", dict) as context: + context[state.id].i_am_custom = True + + +class TestCustomIntrospector(unittest.TestCase): + def introspect_loop(self, thread): + while True: + self.history.append(thread.manticore.introspect()) + sleep(0.5) + + def test_custom_introspector(self): + self.history = [] + m = Manticore(ms_file, introspection_plugin_type=MyIntrospector, stdin_size=17) + m.register_daemon(self.introspect_loop) + m.run() + + self.assertGreater(len(self.history), 0) + self.assertTrue(any(getattr(st, "i_am_custom", False) for st in self.history[-1].values())) + + +if __name__ == "__main__": + unittest.main()