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)
- property 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
- property killed_states
Iterates over the cancelled/killed states.
See also ready_states.
- property 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).
- property 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, explicit_values: Optional[List[Any]] = None)¶
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
- property constraints¶
- property context¶
- execute()¶
- property id¶
- property 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
- property 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: manticore.core.smtlib.expression.Expression, constrain: bool = False) List[int] ¶
Concretize a list of symbolic
Expression
into a list of solutions.- Parameters
exprs – An iterable of manticore.core.smtlib.Expression
constrain (bool) – If True, constrain expr to solved solution value
- Returns
List of concrete value or a tuple of concrete values
- solve_one_n_batched(exprs: Sequence[manticore.core.smtlib.expression.Expression], constrain: bool = False) List[int] ¶
Concretize a list of symbolic
Expression
into a list of solutions. :param exprs: An iterable of manticore.core.smtlib.Expression :param bool constrain: If True, constrain expr to solved solution value :return: List of concrete value or a tuple of concrete values
- 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>, parent: Optional[int] = None, 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, _old_status: Optional[manticore.utils.enums.StateStatus] = None, total_execs: Optional[int] = None, own_execs: Optional[int] = None, pc: Optional[Any] = None, last_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: set¶
State IDs of any states that forked from this one
- created_at: datetime.datetime¶
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: Dict[str, datetime.datetime]¶
Dict mapping field names to the time that field was last updated
- last_intermittent_update: Optional[datetime.datetime] = 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_pc: Optional[Any] = None¶
Last concrete program counter, useful when a state forks and the program counter becomes symbolic
- last_update: datetime.datetime¶
The time that any field of this Descriptor was last updated
- own_execs: Optional[int] = None¶
Number of executions that took place in this state alone, excluding its parents
- parent: Optional[int] = None¶
State ID of zero or one forked state that created this one
- pc: Optional[Any] = None¶
Last program counter (if set)
- state_id: int¶
State ID Number
- state_list: Optional[manticore.utils.enums.StateLists] = None¶
Which State List the state currently resides in (or None if it’s been removed entirely)
- status: manticore.utils.enums.StateStatus = 'waiting_for_worker'¶
What the state is currently doing (ie waiting for a worker, running, solving, etc.) See enums.StateStatus
- termination_msg: Optional[str] = None¶
Message attached to the TerminateState exception that ended this state
- total_execs: Optional[int] = None¶
Total number of instruction executions in this state, including those in its parents