claripy.backends.backend_z3.BackendZ3

class documentation

class BackendZ3(Backend): (source)

Known subclasses: claripy.backends.backend_z3_parallel.BackendZ3Parallel

View In Hierarchy

Undocumented

Method __init__ Undocumented
Method add This function adds constraints to the backend solver.
Method BoolS Undocumented
Method BoolV Undocumented
Method BVS Undocumented
Method BVV Undocumented
Method call Calls operation `op` on args `args` with this backend.
Method clone_solver Undocumented
Method downsize Clears all caches associated with this backend.
Method FPS Undocumented
Method FPV Undocumented
Method simplify Undocumented
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 StringS Undocumented
Method StringV Undocumented
Instance Variable reuse_z3_solver Undocumented
Property extra_bvs_data Undocumented
Static Method _abstract_fp_encoded_val Undocumented
Static Method _abstract_fp_val Undocumented
Static Method _op_add Undocumented
Static Method _op_and Undocumented
Static Method _op_div Undocumented
Static Method _op_mod Undocumented
Static Method _op_mul Undocumented
Static Method _op_or Undocumented
Static Method _op_raw_Concat Undocumented
Static Method _op_raw_Extract Undocumented
Static Method _op_raw_IntToStr Undocumented
Static Method _op_raw_LShR Undocumented
Static Method _op_raw_Reverse Undocumented
Static Method _op_raw_RotateLeft Undocumented
Static Method _op_raw_RotateRight Undocumented
Static Method _op_raw_SDiv Undocumented
Static Method _op_raw_SGE Undocumented
Static Method _op_raw_SGT Undocumented
Static Method _op_raw_SignExt Undocumented
Static Method _op_raw_SLE Undocumented
Static Method _op_raw_SLT Undocumented
Static Method _op_raw_SMod Undocumented
Static Method _op_raw_StrConcat Undocumented
Static Method _op_raw_StrContains Undocumented
Static Method _op_raw_StrIndexOf Undocumented
Static Method _op_raw_StrLen Undocumented
Static Method _op_raw_StrPrefixOf Undocumented
Static Method _op_raw_StrReplace Undocumented
Static Method _op_raw_StrSubstr Undocumented
Static Method _op_raw_StrSuffixOf Undocumented
Static Method _op_raw_StrToInt Undocumented
Static Method _op_raw_UGE Undocumented
Static Method _op_raw_UGT Undocumented
Static Method _op_raw_ULE Undocumented
Static Method _op_raw_ULT Undocumented
Static Method _op_raw_ZeroExt Undocumented
Static Method _op_sub Undocumented
Static Method _op_xor Undocumented
Static Method _z3_ast_hash This is a better hashing function for z3 Ast objects. Z3_get_ast_hash() creates too many hash collisions.
Method _abstract Abstracts the BackendObject e to an AST.
Method _abstract_bv_val Undocumented
Method _abstract_internal Undocumented
Method _abstract_to_primitive Undocumented
Method _add This function adds constraints to the backend solver.
Method _batch_eval Evaluate one or multiple expressions.
Method _convert Converts `r` to something usable by this backend.
Method _eval This function returns up to `n` possible solutions for expression `expr`.
Method _extrema _max if is_max else _min
Method _generic_model Converts a Z3 model to a name->primitive dict.
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 _name This should return the name of an object.
Method _op_raw_And Undocumented
Method _op_raw_fpAbs Undocumented
Method _op_raw_fpAdd Undocumented
Method _op_raw_fpDiv Undocumented
Method _op_raw_fpEQ Undocumented
Method _op_raw_fpFP Undocumented
Method _op_raw_fpGEQ Undocumented
Method _op_raw_fpGT Undocumented
Method _op_raw_fpIsInf Undocumented
Method _op_raw_fpIsNaN Undocumented
Method _op_raw_fpLEQ Undocumented
Method _op_raw_fpLT Undocumented
Method _op_raw_fpMul Undocumented
Method _op_raw_fpNeg Undocumented
Method _op_raw_fpSqrt Undocumented
Method _op_raw_fpSub Undocumented
Method _op_raw_fpToFP Undocumented
Method _op_raw_fpToFPUnsigned Undocumented
Method _op_raw_fpToIEEEBV Undocumented
Method _op_raw_fpToSBV Undocumented
Method _op_raw_fpToUBV Undocumented
Method _op_raw_If Undocumented
Method _op_raw_Not Undocumented
Method _op_raw_Or Undocumented
Method _op_raw_Xor Undocumented
Method _pop_from_ast_cache Undocumented
Method _primitive_from_model Undocumented
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.
Class Variable _split_on Undocumented
Instance Variable _ast_cache_size Undocumented
Property _ast_cache Undocumented
Property _boolref_tactics Undocumented
Property _c_uint64_p Undocumented
Property _context Undocumented
Property _sym_cache Undocumented
Property _var_cache Undocumented

Inherited from Backend:

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 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 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 singlevalued 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.
Class Variable __slots__ Undocumented
Property is_smt_backend Undocumented
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 _has_false The native version of :func:`has_false`.
Method _has_true The native version of :func:`has_true`.
Method _make_expr_ops Fill up `self._op_expr` dict.
Method _make_raw_ops Undocumented
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, reuse_z3_solver=None, ast_cache_size=10000): (source)
overrides claripy.backends.Backend.__init__
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

Undocumented

def add(self, s, c, track=False): (source)
overrides claripy.backends.Backend.add

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()

@condom
def BoolS(self, ast): (source)

Undocumented

@condom
def BoolV(self, ast): (source)

Undocumented

@condom
def BVS(self, ast): (source)

Undocumented

@condom
def BVV(self, ast): (source)

Undocumented

def call(self, *args, **kwargs): (source)
overrides claripy.backends.Backend.call
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

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

def clone_solver(self, s): (source)

Undocumented

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

Clears all caches associated with this backend.

@condom
def FPS(self, ast): (source)

Undocumented

@condom
def FPV(self, ast): (source)

Undocumented

@condom
def simplify(self, expr): (source)
overrides claripy.backends.Backend.simplify
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

Undocumented

def solver(self, timeout=None, max_memory=None): (source)
overrides claripy.backends.Backend.solver
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

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

@condom
def StringS(self, ast): (source)

Undocumented

@condom
def StringV(self, ast): (source)

Undocumented

reuse_z3_solver = (source)

Undocumented

@property
extra_bvs_data = (source)

Undocumented

@staticmethod
def _abstract_fp_encoded_val(ctx, ast): (source)

Undocumented

@staticmethod
def _abstract_fp_val(ctx, ast, op_name): (source)

Undocumented

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

Undocumented

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

Undocumented

@staticmethod
def _op_div(a, b): (source)

Undocumented

@staticmethod
def _op_mod(a, b): (source)

Undocumented

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

Undocumented

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

Undocumented

@staticmethod
@condom
def _op_raw_Concat(*args): (source)

Undocumented

@staticmethod
@condom
def _op_raw_Extract(high, low, a): (source)

Undocumented

@staticmethod
@condom
def _op_raw_IntToStr(input_bv): (source)

Undocumented

@staticmethod
@condom
def _op_raw_LShR(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_Reverse(a): (source)

Undocumented

@staticmethod
@condom
def _op_raw_RotateLeft(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_RotateRight(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_SDiv(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_SGE(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_SGT(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_SignExt(n, a): (source)

Undocumented

@staticmethod
@condom
def _op_raw_SLE(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_SLT(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_SMod(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_StrConcat(*args): (source)

Undocumented

@staticmethod
@condom
def _op_raw_StrContains(input_string, substring): (source)

Undocumented

@staticmethod
@condom
def _op_raw_StrIndexOf(string, pattern, start_idx, bitlength): (source)

Undocumented

@staticmethod
@condom
def _op_raw_StrLen(input_string, bitlength): (source)

Undocumented

@staticmethod
@condom
def _op_raw_StrPrefixOf(prefix, input_string): (source)

Undocumented

@staticmethod
@condom
def _op_raw_StrReplace(input_string, target, replacement): (source)

Undocumented

@staticmethod
@condom
def _op_raw_StrSubstr(start_idx, count, initial_string): (source)

Undocumented

@staticmethod
@condom
def _op_raw_StrSuffixOf(suffix, input_string): (source)

Undocumented

@staticmethod
@condom
def _op_raw_StrToInt(input_string, bitlength): (source)

Undocumented

@staticmethod
@condom
def _op_raw_UGE(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_UGT(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_ULE(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_ULT(a, b): (source)

Undocumented

@staticmethod
@condom
def _op_raw_ZeroExt(n, a): (source)

Undocumented

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

Undocumented

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

Undocumented

@staticmethod
def _z3_ast_hash(ast): (source)

This is a better hashing function for z3 Ast objects. Z3_get_ast_hash() creates too many hash collisions. :param ast: A z3 Ast object. :return: An integer - the hash.

@condom
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 _abstract_bv_val(self, ctx, ast): (source)

Undocumented

def _abstract_internal(self, ctx, ast, split_on=None): (source)

Undocumented

def _abstract_to_primitive(self, ctx, ast): (source)

Undocumented

def _add(self, s, c, track=False): (source)
overrides claripy.backends.Backend._add
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

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().

@condom
def _batch_eval(self, exprs, n, extra_constraints=(), solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._batch_eval
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

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.

@condom
def _convert(self, obj): (source)
overrides claripy.backends.Backend._convert
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

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
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

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 _extrema(self, is_max: bool, expr, extra_constraints, signed, solver, model_callback): (source)

_max if is_max else _min

def _generic_model(self, z3_model): (source)

Converts a Z3 model to a name->primitive dict.

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, 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.

@condom
def _max(self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._max
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

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)

@condom
def _min(self, expr, extra_constraints=(), signed=False, solver=None, model_callback=None): (source)
overrides claripy.backends.Backend._min
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

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

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

def _op_raw_And(self, *args): (source)

Undocumented

@condom
def _op_raw_fpAbs(self, a): (source)

Undocumented

@condom
def _op_raw_fpAdd(self, rm, a, b): (source)

Undocumented

@condom
def _op_raw_fpDiv(self, rm, a, b): (source)

Undocumented

@condom
def _op_raw_fpEQ(self, a, b): (source)

Undocumented

@condom
def _op_raw_fpFP(self, sgn, exp, sig): (source)

Undocumented

@condom
def _op_raw_fpGEQ(self, a, b): (source)

Undocumented

@condom
def _op_raw_fpGT(self, a, b): (source)

Undocumented

@condom
def _op_raw_fpIsInf(self, a): (source)

Undocumented

@condom
def _op_raw_fpIsNaN(self, a): (source)

Undocumented

@condom
def _op_raw_fpLEQ(self, a, b): (source)

Undocumented

@condom
def _op_raw_fpLT(self, a, b): (source)

Undocumented

@condom
def _op_raw_fpMul(self, rm, a, b): (source)

Undocumented

@condom
def _op_raw_fpNeg(self, a): (source)

Undocumented

@condom
def _op_raw_fpSqrt(self, rm, a): (source)

Undocumented

@condom
def _op_raw_fpSub(self, rm, a, b): (source)

Undocumented

@condom
def _op_raw_fpToFP(self, a1, a2=None, a3=None): (source)

Undocumented

@condom
def _op_raw_fpToFPUnsigned(self, a1, a2, a3): (source)

Undocumented

@condom
def _op_raw_fpToIEEEBV(self, x): (source)

Undocumented

@condom
def _op_raw_fpToSBV(self, rm, fp, bv_len): (source)

Undocumented

@condom
def _op_raw_fpToUBV(self, rm, fp, bv_len): (source)

Undocumented

def _op_raw_If(self, i, t, e): (source)

Undocumented

def _op_raw_Not(self, a): (source)

Undocumented

def _op_raw_Or(self, *args): (source)

Undocumented

def _op_raw_Xor(self, *args): (source)

Undocumented

def _pop_from_ast_cache(self, _, tpl): (source)

Undocumented

@condom
def _primitive_from_model(self, model, expr): (source)

Undocumented

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

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)
overrides claripy.backends.Backend._simplify
overridden in claripy.backends.backend_z3_parallel.BackendZ3Parallel

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

def _unsat_core(self, s): (source)
overrides claripy.backends.Backend._unsat_core

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

_split_on: set[str] = (source)

Undocumented

_ast_cache_size = (source)

Undocumented

@property
_ast_cache = (source)

Undocumented

@property
_boolref_tactics = (source)

Undocumented

@property
_c_uint64_p = (source)

Undocumented

@property
_context = (source)

Undocumented

@property
_sym_cache = (source)

Undocumented

@property
_var_cache = (source)

Undocumented