API Reference

This API is under active development, and should be considered unstable.



Helper to determine whether an object is symbolic (e.g checking if data read from memory is symbolic)

Parameters:value (object) – object to check
Returns:whether value is symbolic
Return type:bool

A decorator used to mark a function model as variadic. This function should take two parameters: a State object, and a generator object for the arguments.

Parameters:func (callable) – Function model


class manticore.Manticore(path_or_state, args=None, disasm='capstone')

The central analysis object.

  • path_or_state (str or State) – Path to a binary to analyze or State object
  • args (list[str]) – Arguments to provide to binary

context (dict) – Global context for arbitrary data storage

add_hook(pc, callback)

Add a callback to be invoked on executing a program counter. Pass None for pc to invoke callback on every instruction. callback should be a callable that takes one State argument.

  • pc (int or None) – Address of instruction to hook
  • callback (callable) – Hook function

A decorator used to register a hook function for a given instruction address. Equivalent to calling add_hook().

Parameters:pc (int or None) – Address of instruction to hook
locked_context(*args, **kwds)

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:
    visited = context['visited']
    context['visited'] = visited

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:
  • key (object) – Storage key
  • value_type (list or dict or set) – type of value associated with key
run(procs=1, timeout=0)

Runs analysis.

  • procs (int) – Number of parallel worker processes
  • timeout – Analysis timeout, in seconds

Gracefully terminate the currently-executing run. Typically called from within a hook().


Convenience interface for setting logging verbosity to one of several predefined logging presets. Valid values: 0-5.


class manticore.core.state.State(constraints, platform, **kwargs)

Representation of a unique program state/path.

  • constraints (ConstraintSet) – Initial constraints
  • platform (Platform) – Initial operating system state

context (dict) – Local context for arbitrary data storage


Abandon the currently-active state.

Note: This must be called from the Executor loop, or a hook().


Constrain state.

Parameters:constraint (manticore.core.smtlib.Bool) – Constraint to add
generate_testcase(name, message='State generated testcase')

Generate a testcase for this state and place in the analysis workspace.

  • name (str) – Short string identifying this testcase used to prefix workspace entries.
  • message (str) – Longer description

Invoke a model. A model is a callable whose first argument is a State. If the model models a normal (non-variadic) function, the following arguments correspond to the arguments of the C function being modeled. If the model models a variadic function, the following argument is a generator object, which can be used to access function arguments dynamically. The model callable should simply return the value that should be returned by the native function being modeled.

Parameters:model (callable) – Model to invoke
new_symbolic_buffer(nbytes, **options)

Create and return a symbolic buffer of length nbytes. The buffer is not written into State’s memory; write it to the state’s memory to introduce it into the program state.

  • nbytes (int) – Length of the new buffer
  • name (str) – (keyword arg only) The name to assign to the buffer
  • cstring (bool) – (keyword arg only) Whether or not to enforce that the buffer is a cstring (i.e. no bytes, except for the last byte). (bool)
  • taint (tuple or frozenset) – Taint identifier of the new buffer

Expression representing the buffer.

new_symbolic_value(nbits, label='val', taint=frozenset([]))

Create and return a symbolic value that is nbits bits wide. Assign the value to a register or write it into the address space to introduce it into the program state.

  • nbits (int) – The bitwidth of the value returned
  • label (str) – The label to assign to the value
  • taint (tuple or frozenset) – Taint identifier of this value

Expression representing the value

solve_buffer(addr, nbytes)

Reads nbytes of symbolic data from a buffer in memory at addr and attempts to concretize it

  • address (int) – Address of buffer to concretize
  • nbytes (int) – Size of buffer to concretize

Concrete contents of buffer

Return type:


solve_n(expr, nsolves, policy='minmax')

Concretize a symbolic Expression into nsolves solutions.

Parameters:expr (manticore.core.smtlib.Expression) – Symbolic value to concretize
Returns:Concrete value
Return type:list[int]

Concretize a symbolic Expression into one solution.

Parameters:expr (manticore.core.smtlib.Expression) – Symbolic value to concretize
Returns:Concrete value
Return type:int
symbolicate_buffer(data, label='INPUT', wildcard='+', string=False, taint=frozenset([]))

Mark parts of a buffer as symbolic (demarked by the wildcard byte)

  • data (str) – The string to symbolicate. If no wildcard bytes are provided, this is the identity function on the first argument.
  • label (str) – The label to assign to the value
  • wildcard (str) – The byte that is considered a wildcard
  • string (bool) – Ensure bytes returned can not be
  • taint (tuple or frozenset) – Taint identifier of the symbolicated data

If data does not contain any wildcard bytes, data itself. Otherwise, a list of values derived from data. Non-wildcard bytes are kept as is, wildcard bytes are replaced by Expression objects.


class manticore.core.cpu.abstractcpu.Cpu(regfile, memory, **kwargs)

Base class for all Cpu architectures. Functionality common to all architectures (and expected from users of a Cpu) should be here. Commonly used by platforms and py:class:manticore.core.Executor

The following attributes need to be defined in any derived class

  • arch
  • mode
  • max_instr_width
  • address_bit_size
  • pc_alias
  • stack_alias

Returns all register names for this CPU. Any register returned can be accessed via a cpu.REG convenience interface (e.g. cpu.EAX) for both reading and writing.

Returns:valid register names
Return type:tuple[str]
read_bytes(where, size)

Read from memory.

  • where (int) – address to read data from
  • size (int) – number of bytes


Return type:

list[int or Expression]

read_int(where, size=None)

Reads int from memory

  • where (int) – address to read from
  • size – number of bits to read

the value read

Return type:

int or BitVec


Dynamic interface for reading cpu registers

Parameters:register (str) – register name (as listed in self.all_registers)
Returns:register value
Return type:int or long or Expression
write_bytes(where, data)

Write a concrete or symbolic (or mixed) buffer to memory

  • where (int) – address to write to
  • data (str or list) – data to write
write_int(where, expression, size=None)

Writes int to memory

  • where (int) – address to write to
  • expr (int or BitVec) – value to write
  • size – bit size of expr
write_register(register, value)

Dynamic interface for writing cpu registers

  • register (str) – register name (as listed in self.all_registers)
  • value (int or long or Expression) – register value


Models here are intended to be passed to invoke_model(), not invoked directly.