claripy.backends.backend_concrete.BackendConcrete

class documentation

class BackendConcrete(Backend): (source)

View In Hierarchy

Undocumented

Static Method BVV Undocumented
Static Method FPV Undocumented
Static Method StringV Undocumented
Method __init__ Undocumented
Method convert Override Backend.convert() to add fast paths for BVVs and BoolVs.
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.
Class Variable __slots__ Undocumented
Static Method _op_add Undocumented
Static Method _op_and Undocumented
Static Method _op_boolnot Undocumented
Static Method _op_fpSqrt Undocumented
Static Method _op_mul Undocumented
Static Method _op_neg Undocumented
Static Method _op_not Undocumented
Static Method _op_or Undocumented
Static Method _op_sub Undocumented
Static Method _op_xor Undocumented
Static Method _to_primitive Undocumented
Method _abstract Abstracts the BackendObject e to an AST.
Method _batch_eval Evaluate one or multiple expressions.
Method _cardinality This should return the maximum number of values that an expression can take on. This should be a strict *over* approximation.
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 _If Undocumented
Method _is_false The native version of is_false.
Method _is_true The native version of is_true.
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 _simplify Undocumented
Method _solution Return True if v is a solution of expr with the extra constraints, False otherwise.
Instance Variable _cache_objects Undocumented

Inherited from Backend:

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_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 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.
Property is_smt_backend Undocumented
Method _add This function adds constraints to the backend solver.
Method _call _call
Method _check_satisfiability This function does a constraint check and returns the solvers state
Method _make_expr_ops Fill up `self._op_expr` dict.
Method _make_raw_ops Undocumented
Method _satisfiable This function does a constraint check and returns a model for a solver.
Method _unsat_core This function returns the unsat core from the backend solver.
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
@staticmethod
def BVV(value, size): (source)

Undocumented

@staticmethod
def FPV(op, sort): (source)

Undocumented

@staticmethod
def StringV(value, size): (source)

Undocumented

def __init__(self): (source)
overrides claripy.backends.Backend.__init__

Undocumented

def convert(self, expr): (source)
overrides claripy.backends.Backend.convert

Override Backend.convert() to add fast paths for BVVs and BoolVs.

def is_false(self, e, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend.is_false

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)
overrides claripy.backends.Backend.is_true

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.

__slots__: tuple = (source)
overrides claripy.backends.Backend.__slots__

Undocumented

@staticmethod
def _op_add(*args): (source)

Undocumented

@staticmethod
def _op_and(*args): (source)

Undocumented

@staticmethod
def _op_boolnot(arg): (source)

Undocumented

@staticmethod
def _op_fpSqrt(rm, a): (source)

Undocumented

@staticmethod
def _op_mul(*args): (source)

Undocumented

@staticmethod
def _op_neg(arg): (source)

Undocumented

@staticmethod
def _op_not(arg): (source)

Undocumented

@staticmethod
def _op_or(*args): (source)

Undocumented

@staticmethod
def _op_sub(*args): (source)

Undocumented

@staticmethod
def _op_xor(*args): (source)

Undocumented

@staticmethod
def _to_primitive(expr): (source)

Undocumented

def _abstract(self, e): (source)
overrides claripy.backends.Backend._abstract

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

def _batch_eval(self, exprs, n, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._batch_eval

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 _cardinality(self, b): (source)
overrides claripy.backends.Backend._cardinality

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 _convert(self, a): (source)
overrides claripy.backends.Backend._convert

Converts `r` to something usable by this backend.

def _eval(self, expr, n, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._eval

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)
overrides claripy.backends.Backend._has_false

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)
overrides claripy.backends.Backend._has_true

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)
overrides claripy.backends.Backend._identical

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 _If(self, b, t, f): (source)

Undocumented

def _is_false(self, e, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._is_false

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)
overrides claripy.backends.Backend._is_true

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 _max(self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._max

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)
overrides claripy.backends.Backend._min

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, e): (source)
overrides claripy.backends.Backend._name

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

def _simplify(self, e): (source)
overrides claripy.backends.Backend._simplify

Undocumented

def _solution(self, expr, v, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._solution

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

_cache_objects: bool = (source)
overrides claripy.backends.Backend._cache_objects

Undocumented