States¶
Accessing¶
-
class
manticore.core.manticore.
ManticoreBase
(initial_state, workspace_url=None, policy='random', **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 raises TooManySolutions if more solutions than maxcount
-
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 solutionParameters: 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 solutionParameters: 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.