claripy.backends.Backend

class documentation

class Backend: (source)

Known subclasses: claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_smtlib.BackendSMTLibBase, claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

View In Hierarchy

Backends are Claripy's workhorses. Claripy exposes ASTs (claripy.ast.Base objects) to the world, but when actual computation has to be done, it pushes those ASTs into objects that can be handled by the backends themselves. This provides a unified interface to the outside world while allowing Claripy to support different types of computation. For example, BackendConcrete provides computation support for concrete bitvectors and booleans, BackendVSA introduces VSA constructs such as StridedIntervals (and details what happens when operations are performed on them), and BackendZ3 provides support for symbolic variables and constraint solving. There are a set of functions that a backend is expected to implement. For all of these functions, the "public" version is expected to be able to deal with claripy.ast.Base objects, while the "private" version should only deal with objects specific to the backend itself. This is distinguished with Python idioms: a public function will be named func() while a private function will be _func(). All functions should return objects that are usable by the backend in its private methods. If this can't be done (i.e., some functionality is being attempted that the backend can't handle), the backend should raise a BackendError. In this case, Claripy will move on to the next backend in its list. All backends must implement a convert() function. This function receives a claripy.ast.Base and should return an object that the backend can handle in its private methods. Backends should also implement a _convert() method, which will receive anything that is *not* a claripy.ast.Base object (i.e., an integer or an object from a different backend). If convert() or _convert() receives something that the backend can't translate to a format that is usable internally, the backend should raise BackendError, and thus won't be used for that object. Claripy contract with its backends is as follows: backends should be able to can handle, in their private functions, any object that they return from their private *or* public functions. Likewise, Claripy will never pass an object to any backend private function that did not originate as a return value from a private or public function of that backend. One exception to this is _convert(), as Claripy can try to stuff anything it feels like into _convert() to see if the backend can handle that type of object.

Method __init__ Undocumented
Method add This function adds constraints to the backend solver.
Method apply_annotation This should apply the annotation on the backend object, and return a new backend object.
Method batch_eval Evaluate one or multiple expressions.
Method call Calls operation `op` on args `args` with this backend.
Method cardinality This should return the maximum number of values that an expression can take on. This should be a strict *over* approximation.
Method check_satisfiability This function does a constraint check and returns the solvers state
Method convert Resolves a claripy.ast.Base into something usable by the backend.
Method convert_list Undocumented
Method default_op Undocumented
Method downsize Clears all caches associated with this backend.
Method eval This function returns up to `n` possible solutions for expression `expr`.
Method handles Checks whether this backend can handle the expression.
Method has_false Should return False if `e` can possibly be False.
Method has_true Should return True if `e` can possible be True.
Method identical This should return whether `a` is identical to `b`. Of course, this isn't always clear. True should mean that it is definitely identical. False eans that, conservatively, it might not be.
Method is_false Should return True if e can be easily found to be False.
Method is_true Should return True if `e` can be easily found to be True.
Method max Return the maximum value of expr.
Method min Return the minimum value of `expr`.
Method multivalued Undocumented
Method name This should return the name of an expression.
Method satisfiable This function does a constraint check and checks if the solver is in a sat state.
Method simplify Undocumented
Method singlevalued Undocumented
Method solution Return True if `v` is a solution of `expr` with the extra constraints, False otherwise.
Method solver This function should return an instance of whatever object handles solving for this backend. For example, in Z3, this would be z3.Solver().
Method unsat_core This function returns the unsat core from the backend solver.
Class Variable __slots__ Undocumented
Property is_smt_backend Undocumented
Method _abstract Abstracts the BackendObject e to an AST.
Method _add This function adds constraints to the backend solver.
Method _batch_eval Evaluate one or multiple expressions.
Method _call _call
Method _cardinality This should return the maximum number of values that an expression can take on. This should be a strict *over* approximation.
Method _check_satisfiability This function does a constraint check and returns the solvers state
Method _convert Converts `r` to something usable by this backend.
Method _eval This function returns up to `n` possible solutions for expression `expr`.
Method _has_false The native version of :func:`has_false`.
Method _has_true The native version of :func:`has_true`.
Method _identical This should return whether `a` is identical to `b`. This is the native version of ``identical()``.
Method _is_false The native version of is_false.
Method _is_true The native version of is_true.
Method _make_expr_ops Fill up `self._op_expr` dict.
Method _make_raw_ops Undocumented
Method _max Return the maximum value of expr.
Method _min Return the minimum value of expr.
Method _name This should return the name of an object.
Method _satisfiable This function does a constraint check and returns a model for a solver.
Method _simplify Undocumented
Method _solution Return True if v is a solution of expr with the extra constraints, False otherwise.
Method _unsat_core This function returns the unsat core from the backend solver.
Instance Variable _cache_objects Undocumented
Instance Variable _false_cache Undocumented
Instance Variable _op_expr Undocumented
Instance Variable _op_raw Undocumented
Instance Variable _solver_required Undocumented
Instance Variable _tls Undocumented
Instance Variable _true_cache Undocumented
Property _object_cache Undocumented
def __init__(self, solver_required=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_smtlib.BackendSMTLibBase, claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

Undocumented

def add(self, s, c, track=False): (source)
overridden in claripy.backends.backend_z3.BackendZ3

This function adds constraints to the backend solver. :param c: A sequence of ASTs :param s: A backend solver object :param bool track: True to enable constraint tracking, which is used in unsat_core()

def apply_annotation(self, o, a): (source)
overridden in claripy.backends.backend_vsa.BackendVSA

This should apply the annotation on the backend object, and return a new backend object. :param o: A backend object. :param a: An Annotation object. :return: A backend object.

def batch_eval(self, exprs, n, extra_constraints=(), solver=None, model_callback=None): (source)

Evaluate one or multiple expressions. :param exprs: A list of expressions to evaluate. :param n: Number of different solutions to return. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver object, native to the backend, to assist in the evaluation. :param model_callback: a function that will be executed with recovered models (if any) :return: A list of up to n tuples, where each tuple is a solution for all expressions.

def call(self, op, args): (source)
overridden in claripy.backends.backend_z3.BackendZ3

Calls operation `op` on args `args` with this backend. :return: A backend object representing the result.

def cardinality(self, a): (source)

This should return the maximum number of values that an expression can take on. This should be a strict *over* approximation. :param a: The AST to evaluate :return: An integer

def check_satisfiability(self, extra_constraints=(), solver=None, model_callback=None): (source)

This function does a constraint check and returns the solvers state :param solver: The backend solver object. :param extra_constraints: Extra constraints (as ASTs) to add to s for this solve :param model_callback: a function that will be executed with recovered models (if any) :return: 'SAT', 'UNSAT', or 'UNKNOWN'

def convert(self, expr): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_vsa.BackendVSA

Resolves a claripy.ast.Base into something usable by the backend. :param expr: The expression. :param save: Save the result in the expression's object cache :return: A backend object.

def convert_list(self, args): (source)

Undocumented

def default_op(self, expr): (source)

Undocumented

def downsize(self): (source)
overridden in claripy.backends.backend_z3.BackendZ3

Clears all caches associated with this backend.

def eval(self, expr, n, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend

This function returns up to `n` possible solutions for expression `expr`. :param expr: expression (an AST) to evaluate :param n: number of results to return :param solver: a solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver) :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :param model_callback: a function that will be executed with recovered models (if any) :return: A sequence of up to n results (backend objects)

def handles(self, expr): (source)

Checks whether this backend can handle the expression. :param expr: The expression. :return: True if the backend can handle this expression, False if not.

def has_false(self, e, extra_constraints=(), solver=None, model_callback=None): (source)

Should return False if `e` can possibly be False. :param e: The AST. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver, for backends that require it. :param model_callback: a function that will be executed with recovered models (if any) :return: A boolean.

def has_true(self, e, extra_constraints=(), solver=None, model_callback=None): (source)

Should return True if `e` can possible be True. :param e: The AST. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver, for backends that require it. :param model_callback: a function that will be executed with recovered models (if any) :return: A boolean

def identical(self, a, b): (source)

This should return whether `a` is identical to `b`. Of course, this isn't always clear. True should mean that it is definitely identical. False eans that, conservatively, it might not be. :param a: an AST :param b: another AST

def is_false(self, e, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete

Should return True if e can be easily found to be False. :param e: The AST :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver, for backends that require it :param model_callback: a function that will be executed with recovered models (if any) :return: A boolean.

def is_true(self, e, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete

Should return True if `e` can be easily found to be True. :param e: The AST. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver, for backends that require it. :param model_callback: a function that will be executed with recovered models (if any) :returns: A boolean.

def max(self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None): (source)

Return the maximum value of expr. :param expr: expression (an AST) to evaluate :param solver: a solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver) :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :param signed: Whether to solve for the maximum signed integer instead of the unsigned max :param model_callback: a function that will be executed with recovered models (if any) :return: the maximum possible value of expr (backend object)

def min(self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None): (source)

Return the minimum value of `expr`. :param expr: expression (an AST) to evaluate :param solver: a solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver) :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :param signed: Whether to solve for the minimum signed integer instead of the unsigned min :param model_callback: a function that will be executed with recovered models (if any) :return: the minimum possible value of expr (backend object)

def multivalued(self, a): (source)

Undocumented

def name(self, a): (source)
overridden in claripy.backends.backend_vsa.BackendVSA

This should return the name of an expression. :param a: the AST to evaluate

def satisfiable(self, extra_constraints=(), solver=None, model_callback=None): (source)

This function does a constraint check and checks if the solver is in a sat state. :param solver: The backend solver object. :param extra_constraints: Extra constraints (as ASTs) to add to s for this solve :param model_callback: a function that will be executed with recovered models (if any) :return: True if sat, otherwise false

def simplify(self, e): (source)
overridden in claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

Undocumented

def singlevalued(self, a): (source)

Undocumented

def solution(self, expr, v, extra_constraints=(), solver=None, model_callback=None): (source)

Return True if `v` is a solution of `expr` with the extra constraints, False otherwise. :param expr: An expression (an AST) to evaluate :param v: The proposed solution (an AST) :param solver: A solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver). :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param model_callback: a function that will be executed with recovered models (if any) :return: True if `v` is a solution of `expr`, False otherwise

def solver(self, timeout=None): (source)
overridden in claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend, claripy.backends.backend_z3.BackendZ3

This function should return an instance of whatever object handles solving for this backend. For example, in Z3, this would be z3.Solver().

def unsat_core(self, s): (source)

This function returns the unsat core from the backend solver. :param s: A backend solver object. :return: The unsat core.

__slots__: tuple[str, ...] = (source)
overridden in claripy.backends.backend_concrete.BackendConcrete

Undocumented

@property
is_smt_backend = (source)
overridden in claripy.backends.backend_smtlib.BackendSMTLibBase

Undocumented

def _abstract(self, e): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_z3.BackendZ3

Abstracts the BackendObject e to an AST. :param e: The backend object. :return: An AST.

def _add(self, s, c, track=False): (source)
overridden in claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend, claripy.backends.backend_z3.BackendZ3

This function adds constraints to the backend solver. :param c: sequence of converted backend objects :param s: backend solver object :param bool track: True to enable constraint tracking, which is used in unsat_core().

def _batch_eval(self, exprs, n, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend, claripy.backends.backend_z3.BackendZ3

Evaluate one or multiple expressions. :param exprs: A list of expressions to evaluate. :param n: Number of different solutions to return. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver object, native to the backend, to assist in the evaluation. :param model_callback: a function that will be executed with recovered models (if any) :return: A list of up to n tuples, where each tuple is a solution for all expressions.

def _call(self, op, args): (source)

_call :param op: :param args: :return:

def _cardinality(self, b): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_vsa.BackendVSA

This should return the maximum number of values that an expression can take on. This should be a strict *over* approximation. :param a: The AST to evalute :return: An integer

def _check_satisfiability(self, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_smtlib.BackendSMTLibBase

This function does a constraint check and returns the solvers state :param solver: The backend solver object. :param extra_constraints: Extra constraints (as ASTs) to add to s for this solve :param model_callback: a function that will be executed with recovered models (if any) :return: 'SAT', 'UNSAT', or 'UNKNOWN'

def _convert(self, r): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

Converts `r` to something usable by this backend.

def _eval(self, expr, n, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend, claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

This function returns up to `n` possible solutions for expression `expr`. :param expr: An expression (backend object) to evaluate. :param n: A number of results to return. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver). :param model_callback: a function that will be executed with recovered models (if any) :return: A sequence of up to n results (backend objects).

def _has_false(self, e, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_vsa.BackendVSA

The native version of :func:`has_false`. :param e: The backend object. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver, for backends that require it. :param model_callback: a function that will be executed with recovered models (if any) :return: A boolean.

def _has_true(self, e, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_vsa.BackendVSA

The native version of :func:`has_true`. :param e: The backend object. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver, for backends that require it. :param model_callback: a function that will be executed with recovered models (if any) :return: A boolean.

def _identical(self, a, b): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

This should return whether `a` is identical to `b`. This is the native version of ``identical()``. :param a: the (backend-native) object :param b: the (backend-native) object

def _is_false(self, e, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend, claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

The native version of is_false. :param e: The backend object. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver, for backends that require it. :param model_callback: a function that will be executed with recovered models (if any) :return: A boolean.

def _is_true(self, e, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend, claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

The native version of is_true. :param e: The backend object. :param extra_constraints: Extra constraints (as ASTs) to add to the solver for this solve. :param solver: A solver, for backends that require it. :param model_callback: a function that will be executed with recovered models (if any) :return: A boolean.

def _make_expr_ops(self, op_list, op_dict=None, op_class=None): (source)

Fill up `self._op_expr` dict. :param op_list: A list of operation names. :param op_dict: A dictionary of operation methods. :param op_class: Where the operation method comes from. :return:

def _make_raw_ops(self, op_list, op_dict=None, op_module=None): (source)

Undocumented

def _max(self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

Return the maximum value of expr. :param expr: expression (backend object) to evaluate :param solver: a solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver) :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :param signed: Whether to solve for the maximum signed integer instead of the unsigned max :param model_callback: a function that will be executed with recovered models (if any) :return: the maximum possible value of expr (backend object)

def _min(self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

Return the minimum value of expr. :param expr: expression (backend object) to evaluate :param solver: a solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver) :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :param signed: Whether to solve for the minimum signed integer instead of the unsigned min :param model_callback: a function that will be executed with recovered models (if any) :return: the minimum possible value of expr (backend object)

def _name(self, o): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_z3.BackendZ3

This should return the name of an object. :param o: the (backend-native) object

def _satisfiable(self, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_smtlib.BackendSMTLibBase, claripy.backends.backend_z3.BackendZ3

This function does a constraint check and returns a model for a solver. :param solver: The backend solver object :param extra_constraints: Extra constraints (backend objects) to add to s for this solve :param model_callback: a function that will be executed with recovered models (if any) :return: True if sat, otherwise false

def _simplify(self, e): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_smtlib_solvers.SMTLibSolverBackend, claripy.backends.backend_z3.BackendZ3

Undocumented

def _solution(self, expr, v, extra_constraints=(), solver=None, model_callback=None): (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_vsa.BackendVSA, claripy.backends.backend_z3.BackendZ3

Return True if v is a solution of expr with the extra constraints, False otherwise. :param expr: expression (backend object) to evaluate :param v: the proposed solution (backend object) :param solver: a solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver) :param extra_constraints: extra constraints (as ASTs) to add to the solver for this solve :return: True if v is a solution of expr, False otherwise

def _unsat_core(self, s): (source)
overridden in claripy.backends.backend_z3.BackendZ3

This function returns the unsat core from the backend solver. :param s: A backend solver object. :return: The unsat core.

_cache_objects: bool = (source)
overridden in claripy.backends.backend_concrete.BackendConcrete, claripy.backends.backend_z3_parallel.BackendZ3Parallel

Undocumented

_false_cache = (source)

Undocumented

_op_expr: dict = (source)

Undocumented

_op_raw: dict = (source)

Undocumented

_solver_required = (source)

Undocumented

_tls = (source)

Undocumented

_true_cache = (source)

Undocumented

@property
_object_cache = (source)

Undocumented