claripy
— Solver Engine¶
Realistically, you should never have to work with indepth claripy APIs unless you’re doing some hardcore analysis. Most of the time, you’ll be using claripy as a simple frontend to z3:
import claripy
a = claripy.BVS("sym_val", 32)
b = claripy.RotateLeft(a, 8)
c = b + 4
s = claripy.Solver()
s.add(c == 0x41424344)
assert s.eval(c, 1)[0] == 0x41424344
assert s.eval(a, 1)[0] == 0x40414243
Or using its components in angr:
import angr, claripy
b = angr.Project('/bin/true')
path = b.factory.path()
rax_start = claripy.BVS('rax_start', 64)
path.state.regs.rax = rax_start
path_new = path.step()[0]
rax_new = path_new.state.regs.rax
path_new.state.se.add(rax_new == 1337)
print path_new.state.se.eval(rax_start, 1)[0]
AST¶

class
claripy.ast.base.
Base
(*args, **kwargs)¶ This is the base class of all claripy ASTs. An AST tracks a tree of operations on arguments.
This class should not be instanciated directly  instead, use one of the constructor functions (BVS, BVV, FPS, FPV…) to construct a leaf node and then build more complicated expressions using operations.
AST objects have hash identity. This means that an AST that has the same hash as another AST will be the same object. This is critical for efficient memory usage. As an example, the following is true:
a, b = two different ASTs c = b + a d = b + a assert c is d
Variables:  op – The operation that is being done on the arguments
 args – The arguments that are being used
This is called when you create a new Base object, whether directly or through an operation. It finalizes the arguments (see the _finalize function, above) and then computes a hash. If an AST of this hash already exists, it returns that AST. Otherwise, it creates, initializes, and returns the AST.
Parameters:  op – The AST operation (‘__add__’, ‘Or’, etc)
 args – The arguments to the AST operation (i.e., the objects to add)
 variables – The symbolic variables present in the AST (default: empty set)
 symbolic – A flag saying whether or not the AST is symbolic (default: False)
 length – An integer specifying the length of this AST (default: None)
 collapsible – A flag of whether or not Claripy can feel free to collapse this AST. This is mostly used to keep Claripy from collapsing Reverse operations, so that they can be undone with another Reverse.
 simplified – A measure of how simplified this AST is. 0 means unsimplified, 1 means fastsimplified (basically, just undoing the Reverse op), and 2 means simplified through z3.
 errored – A set of backends that are known to be unable to handle this AST.
 eager_backends – A list of backends with which to attempt eager evaluation
 annotations – A frozenset of annotations applied onto this AST.

make_uuid
(uuid=None)¶ This overrides the default ANA uuid with the hash of the AST. UUID is slow, and we’ll soon replace it from ANA itself, and this will go away.
Returns: a string representation of the AST hash.

cache_key
¶ A key that refers to this AST  this value is appropriate for usage as a key in dictionaries.

append_annotation
(a)¶ Appends an annotation to this AST.
Parameters: a – the annotation to append Returns: a new AST, with the annotation added

append_annotations
(new_tuple)¶ Appends several annotations to this AST.
Parameters: new_tuple – the tuple of annotations to append Returns: a new AST, with the annotations added

annotate
(*args)¶ Appends annotations to this AST.
Parameters: args – the tuple of annotations to append (variadic positional args) Returns: a new AST, with the annotations added

insert_annotation
(a)¶ Inserts an annotation to this AST.
Parameters: a – the annotation to insert Returns: a new AST, with the annotation added

insert_annotations
(new_tuple)¶ Inserts several annotations to this AST.
Parameters: new_tuple – the tuple of annotations to insert Returns: a new AST, with the annotations added

replace_annotations
(new_tuple)¶ Replaces annotations on this AST.
Parameters: new_tuple – the tuple of annotations to replace the old annotations with Returns: a new AST, with the annotations added

remove_annotation
(a)¶ Removes an annotation from this AST.
Parameters: a – the annotation to remove Returns: a new AST, with the annotation removed

remove_annotations
(remove_sequence)¶ Removes several annotations from this AST.
Parameters: remove_sequence – a sequence/set of the annotations to remove Returns: a new AST, with the annotations removed

dbg_repr
(prefix=None)¶ Returns a debug representation of this AST.

shallow_repr
(max_depth=8)¶ Returns a string representation of this AST, but with a maximum depth to prevent floods of text being printed.
Parameters: max_depth – The maximum depth to print Returns: A string representing the AST

depth
¶ The depth of this AST. For example, an AST representing (a+(b+c)) would have a depth of 2.

swap_args
(new_args, new_length=None)¶ This returns the same AST, with the arguments swapped out for new_args.

split
(split_on)¶ Splits the AST if its operation is split_on (i.e., return all the arguments). Otherwise, return a list with just the AST.

structurally_match
(o)¶ Structurally compares two A objects, and check if their corresponding leaves are definitely the same A object (namewise or hashidentity wise).
Parameters: o – the other claripy A object Returns: True/False

replace
(old, new)¶ Returns this AST but with the AST ‘old’ replaced with AST ‘new’ in its subexpressions.

replace_dict
(replacements)¶ Parameters: replacements – A dictionary of asts to replace and their replacements. Returns: An AST with all instances of ast’s in replacements.

ite_burrowed
¶ Returns an equivalent AST that “burrows” the ITE expressions as deep as possible into the ast, for simpler printing.

ite_excavated
¶ Returns an equivalent AST that “excavates” the ITE expressions out as far as possible toward the root of the AST, for processing in static analyses.

uninitialized
¶ Whether this AST comes from an uninitialized dereference or not. It’s only used in underconstrained symbolic execution mode.
Returns: True/False/None (unspecified).

uc_alloc_depth
¶ The depth of allocation by lazyinitialization. It’s only used in underconstrained symbolic execution mode.
Returns: An integer indicating the allocation depth, or None if it’s not from lazyinitialization.

class
claripy.ast.bits.
Bits
(*args, **kwargs)¶ A base class for AST types that can be stored as a series of bits. Currently, this is bitvectors and IEEE floats.
Variables: length – The length of this value in bits. This is called when you create a new Base object, whether directly or through an operation. It finalizes the arguments (see the _finalize function, above) and then computes a hash. If an AST of this hash already exists, it returns that AST. Otherwise, it creates, initializes, and returns the AST.
Parameters:  op – The AST operation (‘__add__’, ‘Or’, etc)
 args – The arguments to the AST operation (i.e., the objects to add)
 variables – The symbolic variables present in the AST (default: empty set)
 symbolic – A flag saying whether or not the AST is symbolic (default: False)
 length – An integer specifying the length of this AST (default: None)
 collapsible – A flag of whether or not Claripy can feel free to collapse this AST. This is mostly used to keep Claripy from collapsing Reverse operations, so that they can be undone with another Reverse.
 simplified – A measure of how simplified this AST is. 0 means unsimplified, 1 means fastsimplified (basically, just undoing the Reverse op), and 2 means simplified through z3.
 errored – A set of backends that are known to be unable to handle this AST.
 eager_backends – A list of backends with which to attempt eager evaluation
 annotations – A frozenset of annotations applied onto this AST.

raw_to_bv
()¶ Converts this data’s bitpattern to a bitvector.

raw_to_fp
()¶ Converts this data’s bitpattern to an IEEE float.

class
claripy.ast.bool.
Bool
(*args, **kwargs)¶ This is called when you create a new Base object, whether directly or through an operation. It finalizes the arguments (see the _finalize function, above) and then computes a hash. If an AST of this hash already exists, it returns that AST. Otherwise, it creates, initializes, and returns the AST.
Parameters:  op – The AST operation (‘__add__’, ‘Or’, etc)
 args – The arguments to the AST operation (i.e., the objects to add)
 variables – The symbolic variables present in the AST (default: empty set)
 symbolic – A flag saying whether or not the AST is symbolic (default: False)
 length – An integer specifying the length of this AST (default: None)
 collapsible – A flag of whether or not Claripy can feel free to collapse this AST. This is mostly used to keep Claripy from collapsing Reverse operations, so that they can be undone with another Reverse.
 simplified – A measure of how simplified this AST is. 0 means unsimplified, 1 means fastsimplified (basically, just undoing the Reverse op), and 2 means simplified through z3.
 errored – A set of backends that are known to be unable to handle this AST.
 eager_backends – A list of backends with which to attempt eager evaluation
 annotations – A frozenset of annotations applied onto this AST.

is_true
()¶ Returns True if ‘self’ can be easily determined to be True. Otherwise, return False. Note that the AST might still be True (i.e., if it were simplified via Z3), but it’s hard to quickly tell that.

is_false
()¶ Returns True if ‘self’ can be easily determined to be False. Otherwise, return False. Note that the AST might still be False (i.e., if it were simplified via Z3), but it’s hard to quickly tell that.

claripy.ast.bool.
BoolS
(name, explicit_name=None)¶ Creates a boolean symbol (i.e., a variable).
Parameters:  name – The name of the symbol
 explicit_name – If False, an identifier is appended to the name to ensure uniqueness.
Returns: A Bool object representing this symbol.

claripy.ast.bool.
constraint_to_si
(expr)¶ Convert a constraint to SI if possible.
Parameters: expr – Returns:

class
claripy.ast.bv.
BV
(*args, **kwargs)¶ A class representing an AST of operations culminating in a bitvector. Do not instantiate this class directly, instead use BVS or BVV to construct a symbol or value, and then use operations to construct more complicated expressions.
Individual subbits and bitranges can be extracted from a bitvector using index and slice notation. Bits are indexed weirdly. For a 32bit AST:
a[31] is the LEFT most bit, so it’d be the 0 in
01111111111111111111111111111111a[0] is the RIGHT most bit, so it’d be the 0 in
11111111111111111111111111111110a[31:30] are the two leftmost bits, so they’d be the 0s in:
00111111111111111111111111111111a[1:0] are the two rightmost bits, so they’d be the 0s in:
11111111111111111111111111111100This is called when you create a new Base object, whether directly or through an operation. It finalizes the arguments (see the _finalize function, above) and then computes a hash. If an AST of this hash already exists, it returns that AST. Otherwise, it creates, initializes, and returns the AST.
Parameters:  op – The AST operation (‘__add__’, ‘Or’, etc)
 args – The arguments to the AST operation (i.e., the objects to add)
 variables – The symbolic variables present in the AST (default: empty set)
 symbolic – A flag saying whether or not the AST is symbolic (default: False)
 length – An integer specifying the length of this AST (default: None)
 collapsible – A flag of whether or not Claripy can feel free to collapse this AST. This is mostly used to keep Claripy from collapsing Reverse operations, so that they can be undone with another Reverse.
 simplified – A measure of how simplified this AST is. 0 means unsimplified, 1 means fastsimplified (basically, just undoing the Reverse op), and 2 means simplified through z3.
 errored – A set of backends that are known to be unable to handle this AST.
 eager_backends – A list of backends with which to attempt eager evaluation
 annotations – A frozenset of annotations applied onto this AST.

chop
(bits=1)¶ Chops a BV into consecutive subslices. Obviously, the length of this BV must be a multiple of bits.
Returns: A list of smaller bitvectors, each bits
in length. The first one will be the leftmost (i.e. most significant) bits.

get_byte
(index)¶ Extracts a byte from a BV, where the index refers to the byte in a bigendian order
Parameters: index – the byte to extract Returns: An 8bit BV

get_bytes
(index, size)¶ Extracts several bytes from a bitvector, where the index refers to the byte in a bigendian order
Parameters: index – the byte to extract Returns: A BV of size size * 8

zero_extend
(n)¶ Zeroextends the bitvector by n bits. So:
a = BVV(0b1111, 4) b = a.zero_extend(4) b is BVV(0b00001111)

sign_extend
(n)¶ Signextends the bitvector by n bits. So:
a = BVV(0b1111, 4) b = a.sign_extend(4) b is BVV(0b11111111)

concat
(*args)¶ Concatenates this bitvector with the bitvectors provided. This bitvector will be on the farleft, i.e. the most significant bits.

val_to_fp
(sort, signed=True, rm=None)¶ Interpret this bitvector as an integer, and return the floatingpoint representation of that integer.
Parameters:  sort – The sort of floating point value to return
 signed – Optional: whether this value is a signed integer
 rm – Optional: the rounding mode to use
Returns: An FP AST whose value is the same as this BV

raw_to_fp
()¶ Interpret the bits of this bitvector as an IEEE754 floating point number. The inverse of this function is raw_to_bv.
Returns: An FP AST whose bitpattern is the same as this BV

raw_to_bv
()¶ A counterpart to FP.raw_to_bv  does nothing and returns itself.

claripy.ast.bv.
BVS
(name, size, min=None, max=None, stride=None, uninitialized=False, explicit_name=None, discrete_set=False, discrete_set_max_card=None, **kwargs)¶ Creates a bitvector symbol (i.e., a variable).
If you want to specify the maximum or minimum value of a normal symbol that is not part of valueset analysis, you should manually add constraints to that effect. Do not use ``min`` and ``max`` for symbolic execution.
Parameters:  name – The name of the symbol.
 size – The size (in bits) of the bitvector.
 min – The minimum value of the symbol, used only for valueset analysis
 max – The maximum value of the symbol, used only for valueset analysis
 stride – The stride of the symbol, used only for valueset analysis
 uninitialized – Whether this value should be counted as an “uninitialized” value in the course of an analysis.
 explicit_name (bool) – If False, an identifier is appended to the name to ensure uniqueness.
 discrete_set (bool) – If True, a DiscreteStridedIntervalSet will be used instead of a normal StridedInterval.
 discrete_set_max_card (int) – The maximum cardinality of the discrete set. It is ignored if discrete_set is set to False or None.
Returns: a BV object representing this symbol.

claripy.ast.bv.
BVV
(value, size=None, **kwargs)¶ Creates a bitvector value (i.e., a concrete value).
Parameters:  value – The value. Either an integer or a string. If it’s a string, it will be interpreted as the bytes of a bigendian constant.
 size – The size (in bits) of the bitvector. Optional if you provide a string, required for an integer.
Returns: A BV object representing this value.

class
claripy.ast.fp.
FP
(*args, **kwargs)¶ An AST representing a set of operations culminating in an IEEE754 floating point number.
Do not instantiate this class directly, instead use FPV or FPS to construct a value or symbol, and then use operations to construct more complicated expressions.
Variables:  length – The length of this value
 sort – The sort of this value, usually either FSORT_FLOAT or FSORT_DOUBLE
This is called when you create a new Base object, whether directly or through an operation. It finalizes the arguments (see the _finalize function, above) and then computes a hash. If an AST of this hash already exists, it returns that AST. Otherwise, it creates, initializes, and returns the AST.
Parameters:  op – The AST operation (‘__add__’, ‘Or’, etc)
 args – The arguments to the AST operation (i.e., the objects to add)
 variables – The symbolic variables present in the AST (default: empty set)
 symbolic – A flag saying whether or not the AST is symbolic (default: False)
 length – An integer specifying the length of this AST (default: None)
 collapsible – A flag of whether or not Claripy can feel free to collapse this AST. This is mostly used to keep Claripy from collapsing Reverse operations, so that they can be undone with another Reverse.
 simplified – A measure of how simplified this AST is. 0 means unsimplified, 1 means fastsimplified (basically, just undoing the Reverse op), and 2 means simplified through z3.
 errored – A set of backends that are known to be unable to handle this AST.
 eager_backends – A list of backends with which to attempt eager evaluation
 annotations – A frozenset of annotations applied onto this AST.

to_fp
(sort, rm=None)¶ Convert this float to a different sort
Parameters:  sort – The sort to convert to
 rm – Optional: The rounding mode to use
Returns: An FP AST

raw_to_fp
()¶ A counterpart to BV.raw_to_fp  does nothing and returns itself.

raw_to_bv
()¶ Interpret the bitpattern of this IEEE754 floating point number as a bitvector. The inverse of this function is to_bv.
Returns: A BV AST whose bitpattern is the same as this FP

val_to_bv
(size, signed=True, rm=None)¶ Convert this floating point value to an integer.
Parameters:  size – The size of the bitvector to return
 signed – Optional: Whether the target integer is signed
 rm – Optional: The rounding mode to use
Returns: A bitvector whose value is the rounded version of this FP’s value

claripy.ast.fp.
FPS
(name, sort, explicit_name=None)¶ Creates a floatingpoint symbol.
Parameters:  name – The name of the symbol
 sort – The sort of the floating point
 explicit_name – If False, an identifier is appended to the name to ensure uniqueness.
Returns: An FP AST.

claripy.ast.fp.
FPV
(value, sort)¶ Creates a concrete floatingpoint value.
Parameters:  value – The value of the floating point.
 sort – The sort of the floating point.
Returns: An FP AST.

class
claripy.ast.int.
Int
(*args, **kwargs)¶ This is called when you create a new Base object, whether directly or through an operation. It finalizes the arguments (see the _finalize function, above) and then computes a hash. If an AST of this hash already exists, it returns that AST. Otherwise, it creates, initializes, and returns the AST.
Parameters:  op – The AST operation (‘__add__’, ‘Or’, etc)
 args – The arguments to the AST operation (i.e., the objects to add)
 variables – The symbolic variables present in the AST (default: empty set)
 symbolic – A flag saying whether or not the AST is symbolic (default: False)
 length – An integer specifying the length of this AST (default: None)
 collapsible – A flag of whether or not Claripy can feel free to collapse this AST. This is mostly used to keep Claripy from collapsing Reverse operations, so that they can be undone with another Reverse.
 simplified – A measure of how simplified this AST is. 0 means unsimplified, 1 means fastsimplified (basically, just undoing the Reverse op), and 2 means simplified through z3.
 errored – A set of backends that are known to be unable to handle this AST.
 eager_backends – A list of backends with which to attempt eager evaluation
 annotations – A frozenset of annotations applied onto this AST.

class
claripy.ast.vs.
VS
(*args, **kwargs)¶ This is called when you create a new Base object, whether directly or through an operation. It finalizes the arguments (see the _finalize function, above) and then computes a hash. If an AST of this hash already exists, it returns that AST. Otherwise, it creates, initializes, and returns the AST.
Parameters:  op – The AST operation (‘__add__’, ‘Or’, etc)
 args – The arguments to the AST operation (i.e., the objects to add)
 variables – The symbolic variables present in the AST (default: empty set)
 symbolic – A flag saying whether or not the AST is symbolic (default: False)
 length – An integer specifying the length of this AST (default: None)
 collapsible – A flag of whether or not Claripy can feel free to collapse this AST. This is mostly used to keep Claripy from collapsing Reverse operations, so that they can be undone with another Reverse.
 simplified – A measure of how simplified this AST is. 0 means unsimplified, 1 means fastsimplified (basically, just undoing the Reverse op), and 2 means simplified through z3.
 errored – A set of backends that are known to be unable to handle this AST.
 eager_backends – A list of backends with which to attempt eager evaluation
 annotations – A frozenset of annotations applied onto this AST.
Backends¶

class
claripy.backends.
Backend
(solver_required=None)¶ 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.

downsize
()¶ Clears all caches associated with this backend.

handles
(expr)¶ Checks whether this backend can handle the expression.
Parameters: expr – The expression. Returns: True if the backend can handle this expression, False if not.

convert
(expr)¶ Resolves a claripy.ast.Base into something usable by the backend.
Parameters:  expr – The expression.
 save – Save the result in the expression’s object cache
Returns: A backend object.

call
(op, args)¶ Calls operation op on args args with this backend.
Returns: A backend object representing the result.

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

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

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

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

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

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

unsat_core
(s)¶ This function returns the unsat core from the backend solver.
Parameters: s – A backend solver object. Returns: The unsat core.

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

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

min
(expr, extra_constraints=(), solver=None, model_callback=None)¶ Return the minimum value of expr.
Parameters:  expr – expression (an AST) to evaluate
 solver – a solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver)
 extra_constraints – extra constraints (as ASTs) to add to the solver for this solve
 model_callback – a function that will be executed with recovered models (if any)
Returns: the minimum possible value of expr (backend object)

max
(expr, extra_constraints=(), solver=None, model_callback=None)¶ Return the maximum value of expr.
Parameters:  expr – expression (an AST) to evaluate
 solver – a solver object, native to the backend, to assist in the evaluation (for example, a z3.Solver)
 extra_constraints – extra constraints (as ASTs) to add to the solver for this solve
 model_callback – a function that will be executed with recovered models (if any)
Returns: the maximum possible value of expr (backend object)

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

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

size
(a)¶ This should return the size of an expression.
Parameters: a – the AST to evaluate

name
(a)¶ This should return the name of an expression.
Parameters: a – the AST to evaluate

identical
(a, b)¶ 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.
Parameters:  a – an AST
 b – another AST

cardinality
(a)¶ This should return the maximum number of values that an expression can take on. This should be a strict over approximation.
Parameters: a – The AST to evaluate Returns: An integer

apply_annotation
(o, a)¶ This should apply the annotation on the backend object, and return a new backend object.
Parameters:  o – A backend object.
 a – An Annotation object.
Returns: A backend object.


class
claripy.backend_object.
BackendObject
¶ This is a base class for custom backend objects to implement.
It lets Claripy know that how to deal with those objects, in case they’re directly used in operations.
Backend objects that don’t derive from this class need to be wrapped in a typeI claripy.ast.Base.

to_claripy
()¶ Claripy calls this to retrieve something that it can directly reason about.


class
claripy.backends.backend_concrete.
BackendConcrete
¶

class
claripy.backends.backend_z3.
BackendZ3
¶ 
downsize
()¶ Clears all caches associated with this backend.

BVS
(**kwargs)¶ The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.

BVV
(**kwargs)¶ The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.

FPS
(**kwargs)¶ The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.

FPV
(**kwargs)¶ The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.

BoolS
(**kwargs)¶ The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.

BoolV
(**kwargs)¶ The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.

call
(*args, **kwargs)¶ Calls operation op on args args with this backend.
Returns: A backend object representing the result.

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

simplify
(**kwargs)¶ The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.


class
claripy.backends.backend_z3_parallel.
BackendZ3Parallel
¶ 
solver
(*args, **kwargs)¶ This function should return an instance of whatever object handles solving for this backend. For example, in Z3, this would be z3.Solver().

call
(*args, **kwargs)¶ Calls operation op on args args with this backend.
Returns: A backend object representing the result.

simplify
(*args, **kwargs)¶ The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.


class
claripy.backends.backend_vsa.
BackendVSA
¶ 
convert
(expr)¶ Resolves a claripy.ast.Base into something usable by the backend.
Parameters:  expr – The expression.
 save – Save the result in the expression’s object cache
Returns: A backend object.

name
(a)¶ This should return the name of an expression.
Parameters: a – the AST to evaluate

apply_annotation
(bo, annotation)¶ Apply an annotation on the backend object.
Parameters:  bo (BackendObject) – The backend object.
 annotation (Annotation) – The annotation to be applied
Returns: A new BackendObject
Return type:

static
CreateStridedInterval
(bits=0, stride=None, lower_bound=None, upper_bound=None, uninitialized=False, to_conv=None, discrete_set=False, discrete_set_max_cardinality=None)¶ Parameters:  name –
 bits –
 stride –
 lower_bound –
 upper_bound –
 to_conv –
 discrete_set (bool) –
 discrete_set_max_cardinality (int) –
Returns:

Frontends¶
Frontend Mixins¶
Annotations¶

class
claripy.annotation.
Annotation
¶ Annotations are used to achieve claripy’s goal of being an arithmetic instrumentation engine. They provide a means to pass extra information to the claripy backends.

eliminatable
¶ Returns whether this annotation can be eliminated in a simplification.
Returns: True if eliminatable, False otherwise

relocatable
¶ Returns whether this annotation can be relocated in a simplification.
Returns: True if it can be relocated, false otherwise.

relocate
(src, dst)¶ This is called when an annotation has to be relocated because of simplifications.
Consider the following case:
x = claripy.BVS(‘x’, 32) zero = claripy.BVV(0, 32).add_annotation(your_annotation) y = x + zeroHere, one of three things can happen:
 if your_annotation.eliminatable is True, the simplifiers will simply eliminate your_annotation along with zero and y is x will hold
 elif your_annotation.relocatable is False, the simplifier will abort and y will never be simplified
 elif your_annotation.relocatable is True, the simplifier will run, determine that the simplified result of x + zero will be x. It will then call your_annotation.relocate(zero, x) to move the annotation away from the AST that is about to be eliminated.
Parameters:  src – the old AST that was eliminated in the simplification
 dst – the new AST (the result of a simplification)
Returns: the annotation that will be applied to dst


class
claripy.annotation.
SimplificationAvoidanceAnnotation
¶
VSA¶

class
claripy.vsa.abstract_location.
AbstractLocation
(bbl_key, stmt_id, region_id, segment_list=None, region_offset=None, size=None)¶

class
claripy.vsa.bool_result.
BoolResult
(op=None, args=None)¶

class
claripy.vsa.bool_result.
TrueResult
(op=None, args=None)¶

class
claripy.vsa.bool_result.
FalseResult
(op=None, args=None)¶

class
claripy.vsa.bool_result.
MaybeResult
(op=None, args=None)¶

class
claripy.vsa.discrete_strided_interval_set.
DiscreteStridedIntervalSet
(name=None, bits=0, si_set=None, max_cardinality=None)¶ A DiscreteStridedIntervalSet represents one or more discrete StridedInterval instances.

cardinality
¶ This is an overapproximation of the cardinality of this DSIS.
Returns:

collapse
()¶ Collapse into a StridedInterval instance.
Returns: A new StridedInterval instance.

normalize
()¶ Return the collapsed object if
should_collapse()
is True, otherwise return self.Returns: A DiscreteStridedIntervalSet object.

concat
(o)¶ Operation concat
Parameters: b – The other operand to concatenate with. Returns: The concatenated value.

extract
(high_bit, low_bit)¶ Operation extract
Parameters:  high_bit – The highest bit to begin extraction.
 low_bit – The lowest bit to end extraction.
Returns: Extracted bits.

eval
(n, signed=False)¶ Parameters:  n –
 signed –
Returns:

union
(b)¶ The union operation. It might return a DiscreteStridedIntervalSet to allow for better precision in analysis.
Parameters: b – Operand Returns: A new DiscreteStridedIntervalSet, or a new StridedInterval.

sign_extend
(o)¶ Operation SignExt
Parameters: new_length – The length to extend to. Returns: SignExtended value.

zero_extend
(o)¶ Operation ZeroExt
Parameters: new_length – The length to extend to. Returns: ZeroExtended value.

widen
(o)¶ Widening operator.
Parameters: b – The other operand. Returns: The widened result.


exception
claripy.vsa.errors.
ClaripyVSAError
¶

exception
claripy.vsa.errors.
ClaripyVSAOperationError
¶

class
claripy.vsa.strided_interval.
WarrenMethods
¶ Methods as suggested in book. Hackers Delight.

static
min_or
(b, c, d, w)¶ Lower bound of result of ORing 2intervals.
Parameters:  a – Lower bound of first interval
 b – Upper bound of first interval
 c – Lower bound of second interval
 d – Upper bound of second interval
 w – bit width
Returns: Lower bound of ORing 2intervals

static
max_or
(b, c, d, w)¶ Upper bound of result of ORing 2intervals.
Parameters:  a – Lower bound of first interval
 b – Upper bound of first interval
 c – Lower bound of second interval
 d – Upper bound of second interval
 w – bit width
Returns: Upper bound of ORing 2intervals

static
min_and
(b, c, d, w)¶ Lower bound of result of ANDing 2intervals.
Parameters:  a – Lower bound of first interval
 b – Upper bound of first interval
 c – Lower bound of second interval
 d – Upper bound of second interval
 w – bit width
Returns: Lower bound of ANDing 2intervals

static
max_and
(b, c, d, w)¶ Upper bound of result of ANDing 2intervals.
Parameters:  a – Lower bound of first interval
 b – Upper bound of first interval
 c – Lower bound of second interval
 d – Upper bound of second interval
 w – bit width
Returns: Upper bound of ANDing 2intervals

static
min_xor
(b, c, d, w)¶ Lower bound of result of XORing 2intervals.
Parameters:  a – Lower bound of first interval
 b – Upper bound of first interval
 c – Lower bound of second interval
 d – Upper bound of second interval
 w – bit width
Returns: Lower bound of XORing 2intervals

static
max_xor
(b, c, d, w)¶ Upper bound of result of XORing 2intervals.
Parameters:  a – Lower bound of first interval
 b – Upper bound of first interval
 c – Lower bound of second interval
 d – Upper bound of second interval
 w – bit width
Returns: Upper bound of XORing 2intervals

static

class
claripy.vsa.strided_interval.
StridedInterval
(name=None, bits=0, stride=None, lower_bound=None, upper_bound=None, uninitialized=False, bottom=False)¶ A Strided Interval is represented in the following form:
<bits> stride[lower_bound, upper_bound]
For more details, please refer to relevant papers like TIE and WYSINWYE.
This implementation is signednessagostic, please refer to [1] SignednessAgnostic Program Analysis: Precise Integer Bounds for LowLevel Code by Jorge A. Navas, etc. for more details. Note that this implementation only takes hint from [1]. Such a work has been improved to be more precise (and still sound) when dealing with strided intervals. DO NOT expect to see a 1to1 reproduction of [1].
Thanks all corresponding authors for their outstanding works.

eval
(n, signed=False)¶ Evaluate this StridedInterval to obtain a list of concrete integers.
Parameters:  n – Upper bound for the number of concrete integers
 signed – Treat this StridedInterval as signed or unsigned
Returns: A list of at most n concrete integers

solution
(b)¶ Checks whether an integer is solution of the current strided Interval :param b: integer to check :return: True if b belongs to the current Strided Interval, False otherwhise

identical
(o)¶ Used to make exact comparisons between two StridedIntervals. Usually it is only used in test cases.
Parameters: o – The other StridedInterval to compare with. Returns: True if they are exactly same, False otherwise.

SLT
(o)¶ Signed less than
Parameters: o – The other operand Returns: TrueResult(), FalseResult(), or MaybeResult()

SLE
(o)¶ Signed less than or equal to.
Parameters: o – The other operand. Returns: TrueResult(), FalseResult(), or MaybeResult()

SGT
(o)¶ Signed greater than.
Parameters: o – The other operand Returns: TrueResult(), FalseResult(), or MaybeResult()

SGE
(o)¶ Signed greater than or equal to.
Parameters: o – The other operand Returns: TrueResult(), FalseResult(), or MaybeResult()

ULT
(o)¶ Unsigned less than.
Parameters: o – The other operand Returns: TrueResult(), FalseResult(), or MaybeResult()

ULE
(o)¶ Unsigned less than or equal to.
Parameters: o – The other operand Returns: TrueResult(), FalseResult(), or MaybeResult()

UGT
(o)¶ Signed greater than.
Parameters: o – The other operand Returns: TrueResult(), FalseResult(), or MaybeResult()

UGE
(o)¶ Unsigned greater than or equal to.
Parameters: o – The other operand Returns: TrueResult(), FalseResult(), or MaybeResult()

eq
(o)¶ Equal
Parameters: o – The ohter operand Returns: TrueResult(), FalseResult(), or MaybeResult()

LShR
(shift_amount)¶ Logical shift right. :param StridedInterval shift_amount: The amount of shifting :return: The shifted StridedInterval object :rtype: StridedInterval

complement
¶ Return the complement of the interval Refer section 3.1 augmented for managing strides
Returns:

is_empty
¶ The same as is_bottom :return: True/False

is_top
¶ If this is a TOP value.
Returns: True if this is a TOP

is_bottom
¶ Whether this StridedInterval is a BOTTOM, in other words, describes an empty set of integers.
Returns: True/False

is_integer
¶ If this is an integer, i.e. self.lower_bound == self.upper_bound.
Returns: True if this is an integer, False otherwise

static
lcm
(b)¶ Get the least common multiple.
Parameters:  a – The first operand (integer)
 b – The second operand (integer)
Returns: Their LCM

static
gcd
(b)¶ Get the greatest common divisor.
Parameters:  a – The first operand (integer)
 b – The second operand (integer)
Returns: Their GCD

static
upper
(i, stride)¶ Returns:

static
lower
(i, stride)¶ Returns:

static
top
(name=None, uninitialized=False)¶ Get a TOP StridedInterval.
Returns:

add
(o)¶ Binary operation: add
Parameters: b – The other operand Returns: self + b

sub
(o)¶ Binary operation: sub
Parameters: b – The other operand Returns: self  b

mul
(o)¶ Binary operation: multiplication
Parameters: o – The other operand Returns: self * o

sdiv
(o)¶ Binary operation: signed division
Parameters: o – The divisor Returns: (self / o) in signed arithmetic

udiv
(o)¶ Binary operation: unsigned division
Parameters: o – The divisor Returns: (self / o) in unsigned arithmetic

bitwise_or
(o)¶ Binary operation: logical or
Parameters: b – The other operand Returns: self  b

bitwise_and
(o)¶ Binary operation: logical and
Parameters: b – The other operand Returns:

bitwise_xor
(o)¶ Operation xor
Parameters: t – The other operand.

union
(o)¶ The union operation. It might return a DiscreteStridedIntervalSet to allow for better precision in analysis.
Parameters: b – Operand Returns: A new DiscreteStridedIntervalSet, or a new StridedInterval.

static
least_upper_bound
()¶ Pseudo least upper bound. Join the given set of intervals into a big interval. The resulting strided interval is the one which in all the possible joins of the presented SI, presented the least number of values.
The number of joins to compute is linear with the number of intervals to join.
Draft of proof: Considering three generic SI (a,b, and c) ordered from their lower bounds, such that a.lower_bund <= b.lower_bound <= c.lower_bound, where <= is the lexicographic less or equal. The only joins which have sense to compute are: * a U b U c * b U c U a * c U a U b
All the other combinations fall in either one of these cases. For example: b U a U c does not make make sense to be calculated. In fact, if one draws this union, the result is exactly either (b U c U a) or (a U b U c) or (c U a U b). :param intervals_to_join: Intervals to join :return: Interval that contains all intervals

static
pseudo_join
(b, smart_join=True)¶ It two intervals in a way that the resulting SI is the one that has the least SI cardinality (i.e., which represents the least number of elements) possible if the smart_join flag is enabled, otherwise it just joins the SI according the order they are passed to the function.
The pseudojoin operation is not associative in wrapping intervals (please refer to section 3.1 paper ‘SignednessAgnostic Program Analysis: Precise Integer Bounds for LowLevel Code’), Therefore the join of three WI may give us different results according on the order we join them. All of the results will be sound, though.
Please use the function least_upper_bound as a stub.
Parameters:  s – The first SI
 b – The other SI.
 smart_join – Enable the smart join behavior. If this flag is set, this function joins the two SI in a way that the resulting Si has least number of elements (more precise). If it is unset, this function will join the two SI according on the order they are passed to the function.
Returns: A new StridedInterval

static
extended_euclid
(b)¶ It calculates the GCD of a and b, and two values x and y such that: a*x + b*y = GCD(a,b). This code has been taken from the project sympy.
Parameters:  a – first integer
 b – second integer
Returns: x,y and the GCD of a and b

static
igcd
(b)¶ Parameters:  a – First integer
 b – Second integer
Returns: the integer GCD between a and b

static
diop_natural_solution_linear
(a, b)¶ It finds the fist natural solution of the diophantine equation a*x + b*y = c. Some lines of this code are taken from the project sympy.
Parameters:  c – constant
 a – quotient of x
 b – quotient of y
Returns: the first natural solution of the diophatine equation

reverse
()¶ This is a delayed reversing function. All it really does is to invert the _reversed property of this StridedInterval object.
Returns: None


claripy.vsa.strided_interval.
CreateStridedInterval
(name=None, bits=0, stride=None, lower_bound=None, upper_bound=None, uninitialized=False, to_conv=None, discrete_set=False, discrete_set_max_cardinality=None)¶ Parameters:  name –
 bits –
 stride –
 lower_bound –
 upper_bound –
 to_conv –
 discrete_set (bool) –
 discrete_set_max_cardinality (int) –
Returns:

class
claripy.vsa.valueset.
RegionAnnotation
(region_id, region_base_addr, offset)¶ Use RegionAnnotation to annotate ASTs. Normally, an AST annotated by RegionAnnotations is treated as a ValueSet.
Note that Annotation objects are immutable. Do not change properties of an Annotation object without creating a new one.

eliminatable
¶ A Region annotation is not eliminatable in simplifications.
Returns: False Return type: bool

relocatable
¶ A Region annotation is not relocatable in simplifications.
Returns: False Return type: bool

relocate
(src, dst)¶ Override Annotation.relocate().
Parameters:  src – The old AST
 dst – The new AST, as the result of a simplification
Returns: The new annotation that should be applied on the new AST


class
claripy.vsa.valueset.
ValueSet
(name=None, region=None, region_base_addr=None, bits=None, val=None)¶ ValueSet is a mapping between memory regions and corresponding offsets.
Constructor.
Parameters:  name (str) – Name of this ValueSet object. Only for debugging purposes.
 region (str) – Region ID.
 region_base_addr (int) – Base address of the region.
 bits (int) – Size of the ValueSet.
 val – an initial offset

apply_annotation
(annotation)¶ Apply a new annotation onto self, and return a new ValueSet object.
Parameters: annotation (RegionAnnotation) – The annotation to apply. Returns: A new ValueSet object Return type: ValueSet

min
¶ The minimum integer value of a valueset. It is only defined when there is exactly one region.
Returns: A integer that represents the minimum integer value of this valueset. Return type: int

max
¶ The maximum integer value of a valueset. It is only defined when there is exactly one region.
Returns: A integer that represents the maximum integer value of this valueset. Return type: int

extract
(high_bit, low_bit)¶ Operation extract
 A cheap hack is implemented: a copy of self is returned if (high_bit  low_bit + 1 == self.bits), which is a
 ValueSet instance. Otherwise a StridedInterval is returned.
Parameters:  high_bit –
 low_bit –
Returns: A ValueSet or a StridedInterval

identical
(o)¶ Used to make exact comparisons between two ValueSets.
Parameters: o – The other ValueSet to compare with. Returns: True if they are exactly same, False otherwise.
Misc. Things¶

class
claripy.balancer.
Balancer
(helper, c, validation_frontend=None)¶ The Balancer is an equation redistributor. The idea is to take an AST and rebalance it to, for example, isolate unknown terms on one side of an inequality.

class
claripy.bv.
BVV
(value, bits)¶

exception
claripy.errors.
ClaripyError
¶

exception
claripy.errors.
UnsatError
¶

exception
claripy.errors.
ClaripyFrontendError
¶

exception
claripy.errors.
ClaripySerializationError
¶

exception
claripy.errors.
BackendError
¶

exception
claripy.errors.
BackendUnsupportedError
¶

exception
claripy.errors.
ClaripyZ3Error
¶

exception
claripy.errors.
ClaripyBackendVSAError
¶

exception
claripy.errors.
ClaripyASTError
¶

exception
claripy.errors.
ClaripyBalancerError
¶

exception
claripy.errors.
ClaripyBalancerUnsatError
¶

exception
claripy.errors.
ClaripyTypeError
¶

exception
claripy.errors.
ClaripyValueError
¶

exception
claripy.errors.
ClaripySizeError
¶

exception
claripy.errors.
ClaripyOperationError
¶

exception
claripy.errors.
ClaripyReplacementError
¶

exception
claripy.errors.
ClaripyRecursionError
¶

exception
claripy.errors.
ClaripyZeroDivisionError
¶

class
claripy.fp.
RM
¶

class
claripy.fp.
FPV
(value, sort)¶