angr.state_plugins.solver

angr.state_plugins.solver.timed_function(f)
angr.state_plugins.solver.enable_timing()
angr.state_plugins.solver.disable_timing()
angr.state_plugins.solver.error_converter(f)
angr.state_plugins.solver.concrete_path_bool(f)
angr.state_plugins.solver.concrete_path_not_bool(f)
angr.state_plugins.solver.concrete_path_scalar(f)
angr.state_plugins.solver.concrete_path_tuple(f)
angr.state_plugins.solver.concrete_path_list(f)
class angr.state_plugins.solver.SimSolver

Bases: SimStatePlugin

This is the plugin you’ll use to interact with symbolic variables, creating them and evaluating them. It should be available on a state as state.solver.

Any top-level variable of the claripy module can be accessed as a property of this object.

__init__(solver=None, all_variables=None, temporal_tracked_variables=None, eternal_tracked_variables=None)
reload_solver(constraints=None)

Reloads the solver. Useful when changing solver options.

Parameters:

constraints (list) – A new list of constraints to use in the reloaded solver instead of the current one

get_variables(*keys)

Iterate over all variables for which their tracking key is a prefix of the values provided.

Elements are a tuple, the first element is the full tracking key, the second is the symbol.

>>> list(s.solver.get_variables('mem'))
[(('mem', 0x1000), <BV64 mem_1000_4_64>), (('mem', 0x1008), <BV64 mem_1008_5_64>)]

>>> list(s.solver.get_variables('file'))
[(('file', 1, 0), <BV8 file_1_0_6_8>), (('file', 1, 1), <BV8 file_1_1_7_8>),
    (('file', 2, 0), <BV8 file_2_0_8_8>)]

>>> list(s.solver.get_variables('file', 2))
[(('file', 2, 0), <BV8 file_2_0_8_8>)]

>>> list(s.solver.get_variables())
[(('mem', 0x1000), <BV64 mem_1000_4_64>), (('mem', 0x1008), <BV64 mem_1008_5_64>),
    (('file', 1, 0), <BV8 file_1_0_6_8>), (('file', 1, 1), <BV8 file_1_1_7_8>),
    (('file', 2, 0), <BV8 file_2_0_8_8>)]
register_variable(v, key, eternal=True)

Register a value with the variable tracking system

Parameters:

  • v – The BVS to register

  • key – A tuple to register the variable under

Parma eternal:

Whether this is an eternal variable, default True. If False, an incrementing counter will be appended to the key.

describe_variables(v)

Given an AST, iterate over all the keys of all the BVS leaves in the tree which are registered.

Unconstrained(name, bits, uninitialized=True, inspect=True, events=True, key=None, eternal=False, uc_alloc_depth=None, **kwargs)

Creates an unconstrained symbol or a default concrete value (0), based on the state options.

Parameters:

  • name – The name of the symbol.

  • bits – The size (in bits) of the symbol.

  • uninitialized – Whether this value should be counted as an “uninitialized” value in the course of an analysis.

  • inspect – Set to False to avoid firing SimInspect breakpoints

  • events – Set to False to avoid generating a SimEvent for the occasion

  • key – Set this to a tuple of increasingly specific identifiers (for example, ('mem', 0xffbeff00) or ('file', 4, 0x20) to cause it to be tracked, i.e. accessible through solver.get_variables.

  • eternal – Set to True in conjunction with setting a key to cause all states with the same ancestry to retrieve the same symbol when trying to create the value. If False, a counter will be appended to the key.

Returns:

an unconstrained symbol (or a concrete value of 0).

BVS(name, size, min=None, max=None, stride=None, uninitialized=False, explicit_name=False, key=None, eternal=False, inspect=True, events=True, **kwargs)

Creates a bit-vector symbol (i.e., a variable). Other keyword parameters are passed directly on to the constructor of claripy.ast.BV.

Parameters:

  • name – The name of the symbol.

  • size – The size (in bits) of the bit-vector.

  • min – The minimum value of the symbol. Note that this only work when using VSA.

  • max – The maximum value of the symbol. Note that this only work when using VSA.

  • stride – The stride of the symbol. Note that this only work when using VSA.

  • uninitialized – Whether this value should be counted as an “uninitialized” value in the course of an analysis.

  • explicit_name – Set to True to prevent an identifier from appended to the name to ensure uniqueness.

  • key – Set this to a tuple of increasingly specific identifiers (for example, ('mem', 0xffbeff00) or ('file', 4, 0x20) to cause it to be tracked, i.e. accessible through solver.get_variables.

  • eternal – Set to True in conjunction with setting a key to cause all states with the same ancestry to retrieve the same symbol when trying to create the value. If False, a counter will be appended to the key.

  • inspect – Set to False to avoid firing SimInspect breakpoints

  • events – Set to False to avoid generating a SimEvent for the occasion

Returns:

A BV object representing this symbol.

downsize()

Frees memory associated with the constraint solver by clearing all of its internal caches.

property constraints

Returns the constraints of the state stored by the solver.

eval_to_ast(e, n, extra_constraints=(), exact=None)

Evaluate an expression, using the solver if necessary. Returns AST objects.

Parameters:

  • e – the expression

  • n – the number of desired solutions

  • extra_constraints – extra constraints to apply to the solver

  • exact – if False, returns approximate solutions

Returns:

a tuple of the solutions, in the form of claripy AST nodes

Return type:

tuple

max(e, extra_constraints=(), exact=None, signed=False)

Return the maximum value of expression e.

:param e : expression (an AST) to evaluate :type extra_constraints: :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :param exact : if False, return approximate solutions. :param signed : Whether the expression should be treated as a signed value. :return: the maximum possible value of e (backend object)

min(e, extra_constraints=(), exact=None, signed=False)

Return the minimum value of expression e.

:param e : expression (an AST) to evaluate :type extra_constraints: :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :param exact : if False, return approximate solutions. :param signed : Whether the expression should be treated as a signed value. :return: the minimum possible value of e (backend object)

solution(e, v, extra_constraints=(), exact=None)

Return True if v is a solution of expr with the extra constraints, False otherwise.

Parameters:

  • e – An expression (an AST) to evaluate

  • v – The proposed solution (an AST)

  • extra_constraints – Extra constraints (as ASTs) to add to the solver for this solve.

  • exact – If False, return approximate solutions.

Returns:

True if v is a solution of expr, False otherwise

is_true(e, extra_constraints=(), exact=None)

If the expression provided is absolutely, definitely a true boolean, return True. Note that returning False doesn’t necessarily mean that the expression can be false, just that we couldn’t figure that out easily.

Parameters:

  • e – An expression (an AST) to evaluate

  • extra_constraints – Extra constraints (as ASTs) to add to the solver for this solve.

  • exact – If False, return approximate solutions.

Returns:

True if v is definitely true, False otherwise

is_false(e, extra_constraints=(), exact=None)

If the expression provided is absolutely, definitely a false boolean, return True. Note that returning False doesn’t necessarily mean that the expression can be true, just that we couldn’t figure that out easily.

Parameters:

  • e – An expression (an AST) to evaluate

  • extra_constraints – Extra constraints (as ASTs) to add to the solver for this solve.

  • exact – If False, return approximate solutions.

Returns:

True if v is definitely false, False otherwise

unsat_core(extra_constraints=())

This function returns the unsat core from the backend solver.

Parameters:

extra_constraints – Extra constraints (as ASTs) to add to the solver for this solve.

Returns:

The unsat core.

satisfiable(extra_constraints=(), exact=None)

This function does a constraint check and checks if the solver is in a sat state.

Parameters:

  • extra_constraints – Extra constraints (as ASTs) to add to s for this solve

  • exact – If False, return approximate solutions.

Returns:

True if sat, otherwise false

add(*constraints)

Add some constraints to the solver.

Parameters:

constraints – Pass any constraints that you want to add (ASTs) as varargs.

CastType = ~CastType
eval_upto(e, n, cast_to=None, **kwargs)
Overloads:

  • self, e (claripy.ast.BV), n (int), cast_to (None), kwargs → list[int]

  • self, e (claripy.ast.BV), n (int), cast_to (type[CastType]), kwargs → list[CastType]

  • self, e (claripy.ast.Bool), n (int), cast_to (None), kwargs → list[bool]

  • self, e (claripy.ast.Bool), n (int), cast_to (type[CastType]), kwargs → list[CastType]

  • self, e (claripy.ast.FP), n (int), cast_to (None), kwargs → list[float]

  • self, e (claripy.ast.FP), n (int), cast_to (type[CastType]), kwargs → list[CastType]

Evaluate an expression, using the solver if necessary. Returns primitives as specified by the cast_to parameter. Only certain primitives are supported, check the implementation of _cast_to to see which ones.

Parameters:

  • e – the expression

  • n – the number of desired solutions

  • extra_constraints – extra constraints to apply to the solver

  • exact – if False, returns approximate solutions

  • cast_to – desired type of resulting values

Returns:

a tuple of the solutions, in the form of Python primitives

Return type:

tuple

eval(e, cast_to=None, **kwargs)
Overloads:

  • self, e (claripy.ast.BV), cast_to (None), kwargs → int

  • self, e (claripy.ast.BV), cast_to (type[CastType]), kwargs → CastType

  • self, e (claripy.ast.Bool), cast_to (None), kwargs → bool

  • self, e (claripy.ast.Bool), cast_to (type[CastType]), kwargs → CastType

  • self, e (claripy.ast.FP), cast_to (None), kwargs → float

  • self, e (claripy.ast.FP), cast_to (type[CastType]), kwargs → CastType

Evaluate an expression to get any possible solution. The desired output types can be specified using the cast_to parameter. extra_constraints can be used to specify additional constraints the returned values must satisfy.

Parameters:

  • e – the expression to get a solution for

  • kwargs – Any additional kwargs will be passed down to eval_upto

  • cast_to – desired type of resulting values

Raises:

SimUnsatError – if no solution could be found satisfying the given constraints

Returns:

eval_one(e, cast_to=None, **kwargs)
Overloads:

  • self, e (claripy.ast.BV), cast_to (None), kwargs → int

  • self, e (claripy.ast.BV), cast_to (type[CastType]), kwargs → CastType

  • self, e (claripy.ast.Bool), cast_to (None), kwargs → bool

  • self, e (claripy.ast.Bool), cast_to (type[CastType]), kwargs → CastType

  • self, e (claripy.ast.FP), cast_to (None), kwargs → float

  • self, e (claripy.ast.FP), cast_to (type[CastType]), kwargs → CastType

Evaluate an expression to get the only possible solution. Errors if either no or more than one solution is returned. A kwarg parameter default can be specified to be returned instead of failure!

Parameters:

  • e – the expression to get a solution for

  • cast_to – desired type of resulting values

  • default – A value can be passed as a kwarg here. It will be returned in case of failure.

  • kwargs – Any additional kwargs will be passed down to eval_upto

Raises:

  • SimUnsatError – if no solution could be found satisfying the given constraints

  • SimValueError – if more than one solution was found to satisfy the given constraints

Returns:

The value for e

eval_atmost(e, n, cast_to=None, **kwargs)
Overloads:

  • self, e (claripy.ast.BV), n (int), cast_to (None), kwargs → list[int]

  • self, e (claripy.ast.BV), n (int), cast_to (type[CastType]), kwargs → list[CastType]

  • self, e (claripy.ast.Bool), n (int), cast_to (None), kwargs → list[bool]

  • self, e (claripy.ast.Bool), n (int), cast_to (type[CastType]), kwargs → list[CastType]

  • self, e (claripy.ast.FP), n (int), cast_to (None), kwargs → list[float]

  • self, e (claripy.ast.FP), n (int), cast_to (type[CastType]), kwargs → list[CastType]

Evaluate an expression to get at most n possible solutions. Errors if either none or more than n solutions are returned.

Parameters:

  • e – the expression to get a solution for

  • n – the inclusive upper limit on the number of solutions

  • cast_to – desired type of resulting values

  • kwargs – Any additional kwargs will be passed down to eval_upto

Raises:

  • SimUnsatError – if no solution could be found satisfying the given constraints

  • SimValueError – if more than n solutions were found to satisfy the given constraints

Returns:

The solutions for e

eval_atleast(e, n, cast_to=None, **kwargs)
Overloads:

  • self, e (claripy.ast.BV), n (int), cast_to (None), kwargs → list[int]

  • self, e (claripy.ast.BV), n (int), cast_to (type[CastType]), kwargs → list[CastType]

  • self, e (claripy.ast.Bool), n (int), cast_to (None), kwargs → list[bool]

  • self, e (claripy.ast.Bool), n (int), cast_to (type[CastType]), kwargs → list[CastType]

  • self, e (claripy.ast.FP), n (int), cast_to (None), kwargs → list[float]

  • self, e (claripy.ast.FP), n (int), cast_to (type[CastType]), kwargs → list[CastType]

Evaluate an expression to get at least n possible solutions. Errors if less than n solutions were found.

Parameters:

  • e – the expression to get a solution for

  • n – the inclusive lower limit on the number of solutions

  • cast_to – desired type of resulting values

  • kwargs – Any additional kwargs will be passed down to eval_upto

Raises:

  • SimUnsatError – if no solution could be found satisfying the given constraints

  • SimValueError – if less than n solutions were found to satisfy the given constraints

Returns:

The solutions for e

eval_exact(e, n, cast_to=None, **kwargs)
Overloads:

  • self, e (claripy.ast.BV), n (int), cast_to (None), kwargs → list[int]

  • self, e (claripy.ast.BV), n (int), cast_to (type[CastType]), kwargs → list[CastType]

  • self, e (claripy.ast.Bool), n (int), cast_to (None), kwargs → list[bool]

  • self, e (claripy.ast.Bool), n (int), cast_to (type[CastType]), kwargs → list[CastType]

  • self, e (claripy.ast.FP), n (int), cast_to (None), kwargs → list[float]

  • self, e (claripy.ast.FP), n (int), cast_to (type[CastType]), kwargs → list[CastType]

Evaluate an expression to get exactly the n possible solutions. Errors if any number of solutions other than n was found to exist.

Parameters:

  • e – the expression to get a solution for

  • n – the inclusive lower limit on the number of solutions

  • cast_to – desired type of resulting values

  • kwargs – Any additional kwargs will be passed down to eval_upto

Raises:

  • SimUnsatError – if no solution could be found satisfying the given constraints

  • SimValueError – if any number of solutions other than n were found to satisfy the given constraints

Returns:

The solutions for e

min_int(e, extra_constraints=(), exact=None, signed=False)

Return the minimum value of expression e.

:param e : expression (an AST) to evaluate :type extra_constraints: :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :param exact : if False, return approximate solutions. :param signed : Whether the expression should be treated as a signed value. :return: the minimum possible value of e (backend object)

max_int(e, extra_constraints=(), exact=None, signed=False)

Return the maximum value of expression e.

:param e : expression (an AST) to evaluate :type extra_constraints: :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :param exact : if False, return approximate solutions. :param signed : Whether the expression should be treated as a signed value. :return: the maximum possible value of e (backend object)

unique(e, **kwargs)

Returns True if the expression e has only one solution by querying the constraint solver. It does also add that unique solution to the solver’s constraints.

symbolic(e)

Returns True if the expression e is symbolic.

single_valued(e)

Returns True whether e is a concrete value or is a value set with only 1 possible value. This differs from unique in that this does not query the constraint solver.

simplify(e=None)

Simplifies e. If e is None, simplifies the constraints of this state.

variables(e)

Returns the symbolic variables present in the AST of e.