class manticore.core.manticore.ManticoreBase(initial_state, workspace_url=None, policy='random', **kwargs)
__init__(initial_state, workspace_url=None, policy='random', **kwargs)

State to start from.

Manticore symbolically explores program states.

Manticore phases

Manticore has multiprocessing capabilities. Several worker processes could be registered to do concurrent exploration of the READY states. Manticore can be itself at different phases: STANDBY, RUNNING.

      +---------+               +---------+
----->| STANDBY +<------------->+ RUNNING |
      +---------+               +----+----+


Manticore starts at STANDBY with a single initial state. Here the user can inspect, modify and generate testcases for the different states. The workers are paused and not doing any work. Actions: run()


At RUNNING the workers consume states from the READY state list and potentially fork new states or terminate states. A RUNNING manticore can be stopped back to STANDBY. Actions: stop()

States and state lists

A state contains all the information of the running program at a given moment. State snapshots are saved to the workspace often. Internally Manticore associates a fresh id with each saved state. The memory copy of the state is then changed by the emulation of the specific arch. Stored snapshots are periodically updated using: _save() and _load().

          _save     +-------------+  _load
State  +----------> |  WORKSPACE  +----------> State

During exploration Manticore spawns a number of temporary states that are maintained in different lists:

  |   +-+---{fork}-----+
  |   | |              |
  V   V V              |
+---------+        +---+----+      +------------+
|  READY  +------->|  BUSY  +----->| TERMINATED |
+---------+        +---+----+      +------------+
     |                             +--------+
     +---------------------------->| KILLED |

At any given time a state must be at the READY, BUSY, TERMINATED or KILLED list.

State list: READY

The READY list holds all the runnable states. Internally a state is added to the READY list via method _put_state(state). Workers take states from the READY list via the _get_state(wait=True|False) method. A worker mainloop will consume states from the READY list and mark them as BUSYwhile working on them. States in the READY list can go to BUSY or KILLED

State list: BUSY

When a state is selected for exploration from the READY list it is marked as busy and put in the BUSY list. States being explored will be constantly modified and only saved back to storage when moved out of the BUSY list. Hence, when at BUSY the stored copy of the state will be potentially outdated. States in the BUSY list can go to TERMINATED, KILLED or they can be {forked} back to READY. The forking process could involve generating new child states and removing the parent from all the lists.

State list: TERMINATED

TERMINATED contains states that have reached a final condition and raised TerminateState. Worker’s mainloop simply moves the states that requested termination to the TERMINATED list. This is a final list.

`An inherited Manticore class like ManticoreEVM could internally revive the states in TERMINATED that pass some condition and move them back to READY so the user can apply a following transaction.`

State list: KILLED

KILLED contains all the READY and BUSY states found at a cancel event. Manticore supports interactive analysis and has a prominetnt event system A useror ui can stop or cancel the exploration at any time. The unfinnished states cought at this situation are simply moved to its own list for further user action. This is a final list.

  • initial_state – the initial root State object
  • workspace_url – workspace folder name
  • policy – scheduling policy
  • kwargs – other kwargs, e.g.

Allows the decorated method to run only when manticore is NOT exploring states


Allows the decorated method to run only when manticore is actively exploring states


Convenient access to shared context. We maintain a local copy of the share context during the time manticore is not running. This local context is copied to the shared context when a run starts and copied back when a run finishes


Total states count


Generate a report testcase for every state in the system and remove all temporary files/streams from the workspace


True if workers are killed. It is safe to join them


True if workers are exploring BUSY states or waiting for READY states


Attempt to cancel and kill all the workers. Workers must terminate RUNNING, STANDBY -> KILLED


A convenient context manager that will kill a manticore run after timeout seconds

locked_context(key=None, value_type=<class 'list'>)

A context manager that provides safe parallel access to the global Manticore context. This should be used to access the global Manticore context when parallel analysis is activated. Code within the with block is executed atomically, so access of shared variables should occur within.

Example use:

with m.locked_context() as context:

Optionally, parameters can specify a key and type for the object paired to this key.:

with m.locked_context('feature_list', list) as feature_list:

Note: If standard (non-proxy) list or dict objects are contained in a referent, modifications to those mutable values will not be propagated through the manager because the proxy has no way of knowing when the values contained within are modified. However, storing a value in a container proxy (which triggers a __setitem__ on the proxy object) does propagate through the manager and so to effectively modify such an item, one could re-assign the modified value to the container proxy:

  • key (object) – Storage key
  • value_type (list or dict or set) – type of value associated with key

Deletes all streams from storage and clean state lists


Runs analysis.

Parameters:timeout – Analysis timeout, in seconds
subscribe(name, callback)

Register a callback to an event


Synchronization decorator


Removes a plugin from manticore. No events should be sent to it after

static verbosity(level)

Sets global vervosity level. This will activate different logging profiles globally depending on the provided numeric value


Waits for the condition callable to return True