States

Accessing

class manticore.core.manticore.ManticoreBase(initial_state, workspace_url=None, outputspace_url=None, introspection_plugin_type: type = <class 'manticore.core.plugin.IntrospectionAPIPlugin'>, **kwargs)

all_states

Iterates over the all states (ready and terminated) It holds a lock so no changes state lists are allowed

Notably the cancelled states are not included here.

See also ready_states.

count_busy_states()

Busy states count

count_killed_states()

Cancelled states count

count_ready_states()

Ready states count

count_terminated_states()

Terminated states count

killed_states

Iterates over the cancelled/killed states.

See also ready_states.

ready_states

Iterator over ready states. It supports state changes. State changes will be saved back at each iteration.

The state data change must be done in a loop, e.g. for state in ready_states: … as we re-save the state when the generator comes back to the function.

This means it is not possible to change the state used by Manticore with states = list(m.ready_states).

terminated_states

Iterates over the terminated states.

See also ready_states.

Operations

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

Representation of a unique program state/path.

Parameters:

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

Variables:

context (dict) – Local context for arbitrary data storage

abandon()

Abandon the currently-active state.

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

can_be_false(expr)

can_be_true(expr)

concretize(symbolic, policy, maxcount=7)

This finds a set of solutions for symbolic using policy.

This limits the number of solutions returned to maxcount to avoid a blowup in the state space. This means that if there are more than `maxcount` feasible solutions, some states will be silently ignored.

constrain(constraint)

Constrain state.

Parameters:constraint (manticore.core.smtlib.Bool) – Constraint to add

constraints

context

execute()

id

input_symbols

is_feasible()

migrate_expression(expression)

must_be_true(expr)

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.

Parameters:

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

Returns:

Expression representing the buffer.

new_symbolic_value(nbits, label=None, 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.

Parameters:

• 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

Returns:

Expression representing the value

platform

solve_buffer(addr, nbytes, constrain=False)

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

Parameters:

• address (int) – Address of buffer to concretize
• nbytes (int) – Size of buffer to concretize
• constrain (bool) – If True, constrain the buffer to the concretized value

Returns:

Concrete contents of buffer

Return type:

list[int]

solve_max(expr)

Solves a symbolic Expression into its maximum solution

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

solve_min(expr)

Solves a symbolic Expression into its minimum solution

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

solve_minmax(expr)

Solves a symbolic Expression into its minimum and maximun solution. Only defined for bitvects.

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

solve_n(expr, nsolves)

Concretize a symbolic Expression into nsolves solutions.

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

solve_one(expr, constrain=False)

A version of solver_one_n for a single expression. See solve_one_n.

solve_one_n(*exprs, constrain=False)

Concretize a symbolic Expression into one solution.

Parameters:

• exprs – An iterable of manticore.core.smtlib.Expression
• constrain (bool) – If True, constrain expr to solved solution value

Returns:

Concrete value or a tuple of concrete values

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)

Parameters:

• 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 NULL
• taint (tuple or frozenset) – Taint identifier of the symbolicated data

Returns:

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.

Inspecting

class manticore.core.plugin.StateDescriptor(state_id: int, state_list: Optional[manticore.utils.enums.StateLists] = None, children: set = <factory>, last_update: datetime.datetime = <factory>, last_intermittent_update: Optional[datetime.datetime] = None, created_at: datetime.datetime = <factory>, status: manticore.utils.enums.StateStatus = <StateStatus.waiting_for_worker: 'waiting_for_worker'>, _old_status: Optional[manticore.utils.enums.StateStatus] = None, total_execs: Optional[int] = None, own_execs: Optional[int] = None, pc: Optional[Any] = None, field_updated_at: Dict[str, datetime.datetime] = <factory>, termination_msg: Optional[str] = None)

Dataclass that tracks information about a State.

children = None

State IDs of any states that forked from this one

created_at = None

The time at which this state was created (or first detected, if the did_enque callback didn’t fire for some reason)

field_updated_at = None

Dict mapping field names to the time that field was last updated

last_intermittent_update = None

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_update = None

The time that any field of this Descriptor was last updated

own_execs = None

Number of executions that took place in this state alone, excluding its parents

pc = None

Last program counter (if set)

state_id = None

State ID Number

state_list = None

Which State List the state currently resides in (or None if it’s been removed entirely)

status = 'waiting_for_worker'

What the state is currently doing (ie waiting for a worker, running, solving, etc.) See enums.StateStatus

termination_msg = None

Message attached to the TerminateState exception that ended this state

total_execs = None

Total number of instruction executions in this state, including those in its parents