claripy.backends.backend_vsa.BackendVSA

class documentation

class BackendVSA(Backend): (source)

View In Hierarchy

Undocumented

Static Method __rshift__ Undocumented
Static Method And Undocumented
Static Method BoolV Undocumented
Static Method BVS Undocumented
Static Method Concat Undocumented
Static Method CreateTopStridedInterval Undocumented
Static Method Extract Undocumented
Static Method LShR Undocumented
Static Method Not Undocumented
Static Method Or Undocumented
Static Method Reverse Undocumented
Static Method SGE Undocumented
Static Method SGT Undocumented
Static Method SignExt Undocumented
Static Method SLE Undocumented
Static Method SLT Undocumented
Static Method UGE Undocumented
Static Method UGT Undocumented
Static Method ULE Undocumented
Static Method ULT Undocumented
Static Method ZeroExt Undocumented
Method __init__ Undocumented
Method apply_annotation Apply an annotation on the backend object.
Method BVV Undocumented
Method constraint_to_si Undocumented
Method convert Resolves a claripy.ast.Base into something usable by the backend.
Method If Undocumented
Method intersection Undocumented
Method name This should return the name of an expression.
Method simplify Undocumented
Method union Undocumented
Method widen Undocumented
Static Method _op_add Undocumented
Static Method _op_and Undocumented
Static Method _op_mod Undocumented
Static Method _op_mul Undocumented
Static Method _op_or Undocumented
Static Method _op_sub Undocumented
Static Method _op_xor Undocumented
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 _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 _solution Return True if v is a solution of expr with the extra constraints, False otherwise.
Method _unique Undocumented

Inherited from Backend:

Method add This function adds constraints to the backend solver.
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 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 satisfiable This function does a constraint check and checks if the solver is in a sat state.
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 _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 _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 _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
@staticmethod
def __rshift__(expr, shift_amount): (source)

Undocumented

@staticmethod
def And(a, *args): (source)

Undocumented

@staticmethod
def BoolV(ast): (source)

Undocumented

@staticmethod
def BVS(ast): (source)

Undocumented

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

Undocumented

@staticmethod
def CreateTopStridedInterval(bits, name=None, uninitialized=False): (source)

Undocumented

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

Undocumented

@staticmethod
def LShR(expr, shift_amount): (source)

Undocumented

@staticmethod
def Not(a): (source)

Undocumented

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

Undocumented

@staticmethod
def Reverse(arg): (source)

Undocumented

@staticmethod
@normalize_arg_order
def SGE(a, b): (source)

Undocumented

@staticmethod
@normalize_arg_order
def SGT(a, b): (source)

Undocumented

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

Undocumented

@staticmethod
@normalize_arg_order
def SLE(a, b): (source)

Undocumented

@staticmethod
@normalize_arg_order
def SLT(a, b): (source)

Undocumented

@staticmethod
@normalize_arg_order
def UGE(a, b): (source)

Undocumented

@staticmethod
@normalize_arg_order
def UGT(a, b): (source)

Undocumented

@staticmethod
@normalize_arg_order
def ULE(a, b): (source)

Undocumented

@staticmethod
@normalize_arg_order
def ULT(a, b): (source)

Undocumented

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

Undocumented

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

Undocumented

def apply_annotation(self, bo, annotation): (source)
overrides claripy.backends.Backend.apply_annotation

Apply an annotation on the backend object. :param BackendObject bo: The backend object. :param Annotation annotation: The annotation to be applied :return: A new BackendObject :rtype: BackendObject

def BVV(self, ast): (source)

Undocumented

def constraint_to_si(self, expr): (source)

Undocumented

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

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

Undocumented

@convert_args
def intersection(self, ast): (source)

Undocumented

def name(self, a): (source)
overrides claripy.backends.Backend.name

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

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

Undocumented

@convert_args
def union(self, ast): (source)

Undocumented

@convert_args
def widen(self, ast): (source)

Undocumented

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

Undocumented

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

Undocumented

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

Undocumented

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

Undocumented

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

Undocumented

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

Undocumented

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

Undocumented

def _cardinality(self, a): (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, o, 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, o, 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 _is_false(self, o, 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, o, 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 _solution(self, obj, 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

def _unique(self, obj): (source)

Undocumented