`claripy` — Solver Engine¶

Realistically, you should never have to work with in-depth claripy APIs unless you’re doing some hard-core 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.BV(op: str, args: Iterable[ArgType], add_variables: Iterable[str] | None = None, hash: int | None = None, symbolic: bool | None = None, variables: frozenset[str] | None = None, errored: set[Backend] | None = None, annotations: tuple[Annotation, ...] = (), skip_child_annotations: bool = False, length: int | None = None, encoded_name: bytes | None = None)[source]¶

Bases: Bits

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 sub-bits and bit-ranges can be extracted from a bitvector using index and slice notation. Bits are indexed weirdly. For a 32-bit AST:

a[31] is the LEFT most bit, so it’d be the 0 in

01111111111111111111111111111111

a[0] is the RIGHT most bit, so it’d be the 0 in

11111111111111111111111111111110

a[31:30] are the two leftmost bits, so they’d be the 0s in:

00111111111111111111111111111111

a[1:0] are the two rightmost bits, so they’d be the 0s in:

11111111111111111111111111111100

Parameters:

op (str)
args (Iterable[ArgType])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool | None)
variables (frozenset[str] | None)
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

chop(bits=1)[source]¶

Chops a BV into consecutive sub-slices. 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 left-most (i.e. most significant) bits.

get_byte(index)[source]¶

Extracts a byte from a BV, where the index refers to the byte in a big-endian order

Parameters:: index – the byte to extract
Returns:: An 8-bit BV

get_bytes(index, size)[source]¶

Extracts several bytes from a bitvector, where the index refers to the byte in a big-endian order

Parameters:

index – the byte index at which to start extracting
size – the number of bytes to extract

Returns:

A BV of size size * 8

zero_extend(n)[source]¶: Zero-extends the bitvector by n bits. So:

a = BVV(0b1111, 4) b = a.zero_extend(4) b is BVV(0b00001111)

sign_extend(n)[source]¶: Sign-extends the bitvector by n bits. So:

a = BVV(0b1111, 4) b = a.sign_extend(4) b is BVV(0b11111111)

concat(*args)[source]¶: Concatenates this bitvector with the bitvectors provided. This bitvector will be on the far-left, i.e. the most significant bits.

val_to_fp(sort, signed=True, rm=None)[source]¶

Interpret this bitvector as an integer, and return the floating-point 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()[source]¶

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 bit-pattern is the same as this BV

raw_to_bv()[source]¶: A counterpart to FP.raw_to_bv - does nothing and returns itself.

to_bv()[source]¶

identical(other)[source]¶

Check if two ASTs are identical. If strict is False, the comparison will be lenient on the names of the ASTs.

Return type:: bool
Parameters:: other (Self)

static Concat(*args)¶

static Extract(*args)¶

LShR()¶

SDiv()¶

SGE()¶

SGT()¶

SLE()¶

SLT()¶

SMod()¶

UGE()¶

UGT()¶

ULE()¶

ULT()¶

intersection()¶

property reversed¶

union()¶

widen()¶

Bases: Bits

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

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

to_fp(sort, rm=None)[source]¶

Convert this float to a different sort

Parameters:

sort – The sort to convert to
rm – Optional: The rounding mode to use

Return type:

FP

Returns:

An FP AST

raw_to_fp()[source]¶

A counterpart to BV.raw_to_fp - does nothing and returns itself.

Return type:: FP

raw_to_bv()[source]¶

Interpret the bit-pattern of this IEEE754 floating point number as a bitvector. The inverse of this function is to_bv.

Return type:: BV
Returns:: A BV AST whose bit-pattern is the same as this FP

to_bv()[source]¶

Return type:: BV

val_to_bv(size, signed=True, rm=None)[source]¶

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

Return type:

BV

Returns:

A bitvector whose value is the rounded version of this FP’s value

property sort: FSort¶

Sqrt()¶

fpAbs()¶

fpAdd()¶

fpDiv()¶

fpEQ()¶

fpGEQ()¶

fpGT()¶

fpLEQ()¶

fpLT()¶

fpMul()¶

fpNEQ()¶

fpNeg()¶

fpSqrt()¶

fpSub()¶

fpToFP()¶

fpToFPUnsigned()¶

fpToIEEEBV()¶

isInf()¶

isNaN()¶

Bases: object

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

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

op: str¶

args: tuple[Union[Base, bool, int, float, str, FSort, tuple[ArgType], None], ...]¶

length: int | None¶

variables: frozenset[str]¶

symbolic: bool¶

annotations: tuple[Annotation, ...]¶

depth: int¶

make_like(op, args, simplify=False, annotations=None, variables=None, symbolic=None, skip_child_annotations=False, length=None)[source]¶

Return type:

Self

Parameters:

op (str)
args (Iterable[Base | bool | int | float | str | FSort | tuple[ArgType] | None])
simplify (bool)
annotations (tuple[Annotation, ...] | None)
variables (frozenset[str] | None)
symbolic (bool | None)
skip_child_annotations (bool)
length (int | None)

__init__(*args, **kwargs)[source]¶

hash()[source]¶

Python’s built in hash function is not collision resistant, so we use our own. When you call hash(ast), the value is derived from the claripy hash, but it gets passed through python’s non-resistent hash function first. This skips that step, allowing the claripy hash to be used directly, eg as a cache key.

Return type:: int

identical(other)[source]¶

Check if two ASTs are identical. If strict is False, the comparison will be lenient on the names of the ASTs.

Return type:: bool
Parameters:: other (Self)

has_annotation_type(annotation_type)[source]¶

Check if this AST has an annotation of a given type.

Parameters:: annotation_type (type[Annotation]) – The type of the annotation.
Return type:: bool
Returns:: True if the AST has an annotation of the given type.

get_annotations_by_type(annotation_type)[source]¶

Get all annotations of a given type.

Parameters:: annotation_type (type[TypeVar(A, bound= Annotation)]) – The type of the annotation.
Return type:: tuple[TypeVar(A, bound= Annotation), ...]
Returns:: A tuple of annotations of the given type.

get_annotation(annotation_type)[source]¶

Get the first annotation of a given type.

Parameters:: annotation_type (type[TypeVar(A, bound= Annotation)]) – The type of the annotation.
Return type:: Optional[TypeVar(A, bound= Annotation)]
Returns:: The annotation of the given type, or None if not found.

append_annotation(a)[source]¶

Appends an annotation to this AST.

Parameters:: a (Annotation) – the annotation to append
Return type:: Self
Returns:: a new AST, with the annotation added

append_annotations(new_tuple)[source]¶

Appends several annotations to this AST.

Parameters:: new_tuple (tuple[Annotation, ...]) – the tuple of annotations to append
Return type:: Self
Returns:: a new AST, with the annotations added

annotate(*args, remove_annotations=None)[source]¶

Appends annotations to this AST.

Parameters:

args (Annotation) – the tuple of annotations to append (variadic positional args)
remove_annotations (Optional[Iterable[Annotation]]) – annotations to remove

Return type:

Self

Returns:

a new AST, with the annotations added

insert_annotation(a)[source]¶

Inserts an annotation to this AST.

Parameters:: a (Annotation) – the annotation to insert
Return type:: Self
Returns:: a new AST, with the annotation added

insert_annotations(new_tuple)[source]¶

Inserts several annotations to this AST.

Parameters:: new_tuple (tuple[Annotation, ...]) – the tuple of annotations to insert
Return type:: Self
Returns:: a new AST, with the annotations added

replace_annotations(new_tuple)[source]¶

Replaces annotations on this AST.

Parameters:: new_tuple (tuple[Annotation, ...]) – the tuple of annotations to replace the old annotations with
Return type:: Self
Returns:: a new AST, with the annotations added

remove_annotation(a)[source]¶

Removes an annotation from this AST.

Parameters:: a (Annotation) – the annotation to remove
Return type:: Self
Returns:: a new AST, with the annotation removed

remove_annotations(remove_sequence)[source]¶

Removes several annotations from this AST.

Parameters:: remove_sequence (Iterable[Annotation]) – a sequence/set of the annotations to remove
Return type:: Self
Returns:: a new AST, with the annotations removed

clear_annotations()[source]¶

Removes all annotations from this AST.

Return type:: Self
Returns:: a new AST, with all annotations removed

clear_annotation_type(annotation_type)[source]¶

Removes all annotations of a given type from this AST.

Parameters:: annotation_type (type[Annotation]) – the type of annotations to remove
Return type:: Self
Returns:: a new AST, with the annotations removed

dbg_repr(prefix=None)[source]¶

Returns a debug representation of this AST.

Return type:: str

shallow_repr(max_depth=8, explicit_length=False, details=ReprLevel.LITE_REPR, inner=False, parent_prec=15, left=True)[source]¶

Returns a string representation of this AST, but with a maximum depth to prevent floods of text being printed.

Parameters:

max_depth (int) – The maximum depth to print.
explicit_length (bool) – Print lengths of BVV arguments.
details (ReprLevel) – An integer value specifying how detailed the output should be: LITE_REPR - print short repr for both operations and BVs, MID_REPR - print full repr for operations and short for BVs, FULL_REPR - print full repr of both operations and BVs.
inner (bool) – whether or not it is an inner AST
parent_prec (int) – parent operation precedence level
left (bool) – whether or not it is a left AST

Return type:

str

Returns:

A string representing the AST

children_asts()[source]¶

Return an iterator over the nested children ASTs.

Return type:: Iterator[Base]

leaf_asts()[source]¶

Return an iterator over the leaf ASTs.

Return type:: Iterator[Base]

is_leaf()[source]¶

Check if this AST is a leaf node.

Return type:: bool

dbg_is_looped()[source]¶

Return type:: Base | bool

structurally_match(o)[source]¶

Structurally compares two A objects, and check if their corresponding leaves are definitely the same A object (name-wise or hash-identity wise).

Parameters:: o (Base) – the other claripy A object
Return type:: bool
Returns:: True/False

canonicalize(var_map=None, counter=None)[source]¶

Return type:: Self

property concrete_value¶

property singlevalued: bool¶

property multivalued: bool¶

property cardinality: int¶

property concrete: bool¶

Bases: Base

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.

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

make_like(op, args, **kwargs)[source]¶

size()[source]¶

Return type:: int
Returns:: The bit length of this AST

raw_to_bv()[source]¶: Converts this data’s bit-pattern to a bitvector.

raw_to_fp()[source]¶: Converts this data’s bit-pattern to an IEEE float.

Bases: Base

Bool is the AST class for a boolean value.

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

is_true()[source]¶: 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()[source]¶: 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.

size()[source]¶: Returns the size of the AST in bits. A boolean is 1 bit.

intersection()¶

Bases: Base

Base class that represent the AST of a String object and implements all the operation useful to create and modify the AST.

Do not instantiate this class directly, instead use StringS or StringV to construct a symbol or value, and then use operations to construct more complicated expressions.

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

strReplace(str_to_replace, replacement)[source]¶

Replace the first occurence of str_to_replace with replacement

Parameters:

str_to_replace (claripy.ast.String) – pattern that has to be replaced
replacement (claripy.ast.String) – replacement pattern

toInt()[source]¶: Convert the string to a bitvector holding the integer representation of the string

indexOf(pattern, start_idx)[source]¶: Return the start index of the pattern inside the input string in a Bitvector representation, otherwise it returns -1 (always using a BitVector)

static IntToStr(*args)¶

static StrConcat(*args)¶

static StrContains(*args)¶

static StrIndexOf(*args)¶

static StrIsDigit(*args)¶

static StrLen(*args)¶

static StrPrefixOf(*args)¶

static StrReplace(*args)¶

static StrSubstr(*args)¶

static StrSuffixOf(*args)¶

static StrToInt(*args)¶

claripy.ast.false()[source]¶

claripy.ast.true()[source]¶

class claripy.ast.base.ReprLevel(value)[source]¶

Bases: IntEnum

Representation levels for ASTs.

LITE_REPR = 0¶

MID_REPR = 1¶

FULL_REPR = 2¶

Bases: object

This is the base class of all claripy ASTs. An AST tracks a tree of operations on arguments.

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

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

op: str¶

args: tuple[Union[Base, bool, int, float, str, FSort, tuple[ArgType], None], ...]¶

length: int | None¶

variables: frozenset[str]¶

symbolic: bool¶

annotations: tuple[Annotation, ...]¶

depth: int¶

make_like(op, args, simplify=False, annotations=None, variables=None, symbolic=None, skip_child_annotations=False, length=None)[source]¶

Return type:

Self

Parameters:

op (str)
args (Iterable[Base | bool | int | float | str | FSort | tuple[ArgType] | None])
simplify (bool)
annotations (tuple[Annotation, ...] | None)
variables (frozenset[str] | None)
symbolic (bool | None)
skip_child_annotations (bool)
length (int | None)

__init__(*args, **kwargs)[source]¶

hash()[source]¶

Return type:: int

identical(other)[source]¶

Check if two ASTs are identical. If strict is False, the comparison will be lenient on the names of the ASTs.

Return type:: bool
Parameters:: other (Self)

has_annotation_type(annotation_type)[source]¶

Check if this AST has an annotation of a given type.

Parameters:: annotation_type (type[Annotation]) – The type of the annotation.
Return type:: bool
Returns:: True if the AST has an annotation of the given type.

get_annotations_by_type(annotation_type)[source]¶

Get all annotations of a given type.

Parameters:: annotation_type (type[TypeVar(A, bound= Annotation)]) – The type of the annotation.
Return type:: tuple[TypeVar(A, bound= Annotation), ...]
Returns:: A tuple of annotations of the given type.

get_annotation(annotation_type)[source]¶

Get the first annotation of a given type.

Parameters:: annotation_type (type[TypeVar(A, bound= Annotation)]) – The type of the annotation.
Return type:: Optional[TypeVar(A, bound= Annotation)]
Returns:: The annotation of the given type, or None if not found.

append_annotation(a)[source]¶

Appends an annotation to this AST.

Parameters:: a (Annotation) – the annotation to append
Return type:: Self
Returns:: a new AST, with the annotation added

append_annotations(new_tuple)[source]¶

Appends several annotations to this AST.

Parameters:: new_tuple (tuple[Annotation, ...]) – the tuple of annotations to append
Return type:: Self
Returns:: a new AST, with the annotations added

annotate(*args, remove_annotations=None)[source]¶

Appends annotations to this AST.

Parameters:

args (Annotation) – the tuple of annotations to append (variadic positional args)
remove_annotations (Optional[Iterable[Annotation]]) – annotations to remove

Return type:

Self

Returns:

a new AST, with the annotations added

insert_annotation(a)[source]¶

Inserts an annotation to this AST.

Parameters:: a (Annotation) – the annotation to insert
Return type:: Self
Returns:: a new AST, with the annotation added

insert_annotations(new_tuple)[source]¶

Inserts several annotations to this AST.

Parameters:: new_tuple (tuple[Annotation, ...]) – the tuple of annotations to insert
Return type:: Self
Returns:: a new AST, with the annotations added

replace_annotations(new_tuple)[source]¶

Replaces annotations on this AST.

Parameters:: new_tuple (tuple[Annotation, ...]) – the tuple of annotations to replace the old annotations with
Return type:: Self
Returns:: a new AST, with the annotations added

remove_annotation(a)[source]¶

Removes an annotation from this AST.

Parameters:: a (Annotation) – the annotation to remove
Return type:: Self
Returns:: a new AST, with the annotation removed

remove_annotations(remove_sequence)[source]¶

Removes several annotations from this AST.

Parameters:: remove_sequence (Iterable[Annotation]) – a sequence/set of the annotations to remove
Return type:: Self
Returns:: a new AST, with the annotations removed

clear_annotations()[source]¶

Removes all annotations from this AST.

Return type:: Self
Returns:: a new AST, with all annotations removed

clear_annotation_type(annotation_type)[source]¶

Removes all annotations of a given type from this AST.

Parameters:: annotation_type (type[Annotation]) – the type of annotations to remove
Return type:: Self
Returns:: a new AST, with the annotations removed

dbg_repr(prefix=None)[source]¶

Returns a debug representation of this AST.

Return type:: str

shallow_repr(max_depth=8, explicit_length=False, details=ReprLevel.LITE_REPR, inner=False, parent_prec=15, left=True)[source]¶

Returns a string representation of this AST, but with a maximum depth to prevent floods of text being printed.

Parameters:

max_depth (int) – The maximum depth to print.
explicit_length (bool) – Print lengths of BVV arguments.
details (ReprLevel) – An integer value specifying how detailed the output should be: LITE_REPR - print short repr for both operations and BVs, MID_REPR - print full repr for operations and short for BVs, FULL_REPR - print full repr of both operations and BVs.
inner (bool) – whether or not it is an inner AST
parent_prec (int) – parent operation precedence level
left (bool) – whether or not it is a left AST

Return type:

str

Returns:

A string representing the AST

children_asts()[source]¶

Return an iterator over the nested children ASTs.

Return type:: Iterator[Base]

leaf_asts()[source]¶

Return an iterator over the leaf ASTs.

Return type:: Iterator[Base]

is_leaf()[source]¶

Check if this AST is a leaf node.

Return type:: bool

dbg_is_looped()[source]¶

Return type:: Base | bool

structurally_match(o)[source]¶

Structurally compares two A objects, and check if their corresponding leaves are definitely the same A object (name-wise or hash-identity wise).

Parameters:: o (Base) – the other claripy A object
Return type:: bool
Returns:: True/False

canonicalize(var_map=None, counter=None)[source]¶

Return type:: Self

property concrete_value¶

property singlevalued: bool¶

property multivalued: bool¶

property cardinality: int¶

property concrete: bool¶

Bases: Base

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.

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

make_like(op, args, **kwargs)[source]¶

size()[source]¶

Return type:: int
Returns:: The bit length of this AST

raw_to_bv()[source]¶: Converts this data’s bit-pattern to a bitvector.

raw_to_fp()[source]¶: Converts this data’s bit-pattern to an IEEE float.

Bases: Base

Bool is the AST class for a boolean value.

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

is_true()[source]¶: 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()[source]¶: 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.

size()[source]¶: Returns the size of the AST in bits. A boolean is 1 bit.

intersection()¶

claripy.ast.bool.BoolS(name, explicit_name=None)[source]¶

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.

Return type:

Bool

Returns:

A Bool object representing this symbol.

claripy.ast.bool.BoolV(val)[source]¶

Return type:: Bool

claripy.ast.bool.true()[source]¶

claripy.ast.bool.false()[source]¶

claripy.ast.bool.If(cond, true_value, false_value)[source]¶

claripy.ast.bool.ite_dict(i, d, default)[source]¶: Return an expression of if-then-else trees which expresses a switch tree :type i: :param i: The variable which may take on multiple values affecting the final result :type d: :param d: A dict mapping possible values for i to values which the result could be :type default: :param default: A default value that the expression should take on if i matches none of the keys of d :return: An expression encoding the result of the above

claripy.ast.bool.ite_cases(cases, default)[source]¶

Return an expression of if-then-else trees which expresses a series of alternatives

Parameters:

cases – A list of tuples (c, v). c is the condition under which v should be the result of the expression
default – A default value that the expression should take on if none of the c conditions are satisfied

Returns:

An expression encoding the result of the above

claripy.ast.bool.reverse_ite_cases(ast)[source]¶: Given an expression created by ite_cases, produce the cases that generated it :type ast: :param ast: :return:

claripy.ast.bool.constraint_to_si(expr)[source]¶

Convert a constraint to SI if possible.

Parameters:: expr
Returns:

Bases: Bits

Individual sub-bits and bit-ranges can be extracted from a bitvector using index and slice notation. Bits are indexed weirdly. For a 32-bit AST:

a[31] is the LEFT most bit, so it’d be the 0 in

01111111111111111111111111111111

a[0] is the RIGHT most bit, so it’d be the 0 in

11111111111111111111111111111110

a[31:30] are the two leftmost bits, so they’d be the 0s in:

00111111111111111111111111111111

a[1:0] are the two rightmost bits, so they’d be the 0s in:

11111111111111111111111111111100

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

chop(bits=1)[source]¶

Chops a BV into consecutive sub-slices. 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 left-most (i.e. most significant) bits.

get_byte(index)[source]¶

Extracts a byte from a BV, where the index refers to the byte in a big-endian order

Parameters:: index – the byte to extract
Returns:: An 8-bit BV

get_bytes(index, size)[source]¶

Extracts several bytes from a bitvector, where the index refers to the byte in a big-endian order

Parameters:

index – the byte index at which to start extracting
size – the number of bytes to extract

Returns:

A BV of size size * 8

zero_extend(n)[source]¶: Zero-extends the bitvector by n bits. So:

a = BVV(0b1111, 4) b = a.zero_extend(4) b is BVV(0b00001111)

sign_extend(n)[source]¶: Sign-extends the bitvector by n bits. So:

a = BVV(0b1111, 4) b = a.sign_extend(4) b is BVV(0b11111111)

concat(*args)[source]¶: Concatenates this bitvector with the bitvectors provided. This bitvector will be on the far-left, i.e. the most significant bits.

val_to_fp(sort, signed=True, rm=None)[source]¶

Interpret this bitvector as an integer, and return the floating-point 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()[source]¶

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 bit-pattern is the same as this BV

raw_to_bv()[source]¶: A counterpart to FP.raw_to_bv - does nothing and returns itself.

to_bv()[source]¶

identical(other)[source]¶

Check if two ASTs are identical. If strict is False, the comparison will be lenient on the names of the ASTs.

Return type:: bool
Parameters:: other (Self)

static Concat(*args)¶

static Extract(*args)¶

LShR()¶

SDiv()¶

SGE()¶

SGT()¶

SLE()¶

SLT()¶

SMod()¶

UGE()¶

UGT()¶

ULE()¶

ULT()¶

intersection()¶

property reversed¶

union()¶

widen()¶

claripy.ast.bv.BVS(name, size, explicit_name=None, **kwargs)[source]¶

Creates a bit-vector symbol (i.e., a variable).

If you want to specify the maximum or minimum value of a normal symbol that is not part of value-set 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 bit-vector.
explicit_name (bool) – If False, an identifier is appended to the name to ensure uniqueness.

Return type:

BV

Returns:

a BV object representing this symbol.

claripy.ast.bv.BVV(value, size=None, **kwargs)[source]¶

Creates a bit-vector value (i.e., a concrete value).

Parameters:

value – The value. Either an integer or a bytestring. If it’s the latter, it will be interpreted as the bytes of a big-endian constant.
size – The size (in bits) of the bit-vector. Optional if you provide a string, required for an integer.

Return type:

BV

Returns:

A BV object representing this value.

claripy.ast.bv.SI(name='unnamed', bits=0, lower_bound=None, upper_bound=None, stride=None, explicit_name=None)[source]¶

claripy.ast.bv.TSI(bits, name=None, explicit_name=None)[source]¶

claripy.ast.bv.ESI(bits, **kwargs)[source]¶

claripy.ast.bv.ValueSet(bits, region, region_base_addr, value)[source]¶

Parameters:

bits (int)
region (str)
region_base_addr (int)
value (BV | int)

claripy.ast.bv.VS(bits, region, region_base_addr, value)¶

Parameters:

bits (int)
region (str)
region_base_addr (int)
value (BV | int)

Bases: Bits

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

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

to_fp(sort, rm=None)[source]¶

Convert this float to a different sort

Parameters:

sort – The sort to convert to
rm – Optional: The rounding mode to use

Return type:

FP

Returns:

An FP AST

raw_to_fp()[source]¶

A counterpart to BV.raw_to_fp - does nothing and returns itself.

Return type:: FP

raw_to_bv()[source]¶

Interpret the bit-pattern of this IEEE754 floating point number as a bitvector. The inverse of this function is to_bv.

Return type:: BV
Returns:: A BV AST whose bit-pattern is the same as this FP

to_bv()[source]¶

Return type:: BV

val_to_bv(size, signed=True, rm=None)[source]¶

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

Return type:

BV

Returns:

A bitvector whose value is the rounded version of this FP’s value

property sort: FSort¶

Sqrt()¶

fpAbs()¶

fpAdd()¶

fpDiv()¶

fpEQ()¶

fpGEQ()¶

fpGT()¶

fpLEQ()¶

fpLT()¶

fpMul()¶

fpNEQ()¶

fpNeg()¶

fpSqrt()¶

fpSub()¶

fpToFP()¶

fpToFPUnsigned()¶

fpToIEEEBV()¶

isInf()¶

isNaN()¶

claripy.ast.fp.FPS(name, sort, explicit_name=None)[source]¶

Creates a floating-point 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.

Return type:

FP

Returns:

An FP AST.

claripy.ast.fp.FPV(value, sort)[source]¶

Creates a concrete floating-point value.

Parameters:

value – The value of the floating point.
sort – The sort of the floating point.

Return type:

FP

Returns:

An FP AST.

Bases: Base

Base class that represent the AST of a String object and implements all the operation useful to create and modify the AST.

Do not instantiate this class directly, instead use StringS or StringV to construct a symbol or value, and then use operations to construct more complicated expressions.

Parameters:

op (str)
args (tuple[Base | bool | int | float | str | FSort | tuple[ArgType] | None, ...])
add_variables (Iterable[str] | None)
hash (int | None)
symbolic (bool)
variables (frozenset[str])
errored (set[Backend] | None)
annotations (tuple[Annotation, ...])
skip_child_annotations (bool)
length (int | None)
encoded_name (bytes | None)

strReplace(str_to_replace, replacement)[source]¶

Replace the first occurence of str_to_replace with replacement

Parameters:

str_to_replace (claripy.ast.String) – pattern that has to be replaced
replacement (claripy.ast.String) – replacement pattern

toInt()[source]¶: Convert the string to a bitvector holding the integer representation of the string

indexOf(pattern, start_idx)[source]¶: Return the start index of the pattern inside the input string in a Bitvector representation, otherwise it returns -1 (always using a BitVector)

static IntToStr(*args)¶

static StrConcat(*args)¶

static StrContains(*args)¶

static StrIndexOf(*args)¶

static StrIsDigit(*args)¶

static StrLen(*args)¶

static StrPrefixOf(*args)¶

static StrReplace(*args)¶

static StrSubstr(*args)¶

static StrSuffixOf(*args)¶

static StrToInt(*args)¶

claripy.ast.strings.StringS(name, explicit_name=False, **kwargs)[source]¶

Create a new symbolic string (analogous to z3.String())

Parameters:

name – The name of the symbolic string (i. e. the name of the variable)
explicit_name (bool) – If False, an identifier is appended to the name to ensure uniqueness.

Returns:

The String object representing the symbolic string

claripy.ast.strings.StringV(value, **kwargs)[source]¶

Create a new Concrete string (analogous to z3.StringVal())

Parameters:: value – The constant value of the concrete string
Returns:: The String object representing the concrete string

Backends¶

class claripy.backends.Backend(solver_required=None)[source]¶

Bases: object

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.

__init__(solver_required=None)[source]¶

downsize()[source]¶: Clears all caches associated with this backend.

handles(expr)[source]¶

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)[source]¶

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.

convert_list(args)[source]¶

call(op, args)[source]¶

Calls operation op on args args with this backend.

Returns:: A backend object representing the result.

simplify(expr)[source]¶

is_true(e, extra_constraints=(), solver=None, model_callback=None)[source]¶

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)[source]¶

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)[source]¶

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)[source]¶

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)[source]¶: 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)[source]¶

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)[source]¶

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)[source]¶

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)[source]¶

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=(), signed=False, solver=None, model_callback=None)[source]¶

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
signed – Whether to solve for the minimum signed integer instead of the unsigned min
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=(), signed=False, solver=None, model_callback=None)[source]¶

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
signed – Whether to solve for the maximum signed integer instead of the unsigned max
model_callback – a function that will be executed with recovered models (if any)

Returns:

the maximum possible value of expr (backend object)

check_satisfiability(extra_constraints=(), solver=None, model_callback=None)[source]¶

This function does a constraint check and returns the solvers 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:

‘SAT’, ‘UNSAT’, or ‘UNKNOWN’

satisfiable(extra_constraints=(), solver=None, model_callback=None)[source]¶

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)[source]¶

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

name(a)[source]¶

This should return the name of an expression.

Parameters:: a – the AST to evaluate

identical(a, b)[source]¶

This should return whether a is identical to b. Of course, this isn’t always clear. True should mean that it is definitely identical. False eans that, conservatively, it might not be.

Parameters:

a – an AST
b – another AST

Return type:

bool

cardinality(a)[source]¶

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

singlevalued(a)[source]¶

multivalued(a)[source]¶

apply_annotation(o, a)[source]¶

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.

default_op(expr)[source]¶

class claripy.backends.BackendConcrete[source]¶

Bases: Backend

__init__()[source]¶

static BVV(value, size)[source]¶

static StringV(value)[source]¶

static FPV(op, sort)[source]¶

convert(expr)[source]¶: Override Backend.convert() to add fast paths for BVVs and BoolVs.

is_true(e, extra_constraints=(), solver=None, model_callback=None)[source]¶

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)[source]¶

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.

class claripy.backends.BackendVSA[source]¶

Bases: Backend

BackendVSA is a backend that uses VSA (Value Set Analysis) to represent and reason about values.

__init__()[source]¶

convert(expr)[source]¶

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)[source]¶

This should return the name of an expression.

Parameters:: a – the AST to evaluate

apply_annotation(o, a)[source]¶

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:

BackendObject

static BVV(ast)[source]¶

static BoolV(ast)[source]¶

static And(a, *args)[source]¶

static Not(a)[source]¶

static ULT(a, b)[source]¶

static ULE(a, b)[source]¶

static UGT(a, b)[source]¶

static UGE(a, b)[source]¶

static SLT(a, b)[source]¶

static SLE(a, b)[source]¶

static SGT(a, b)[source]¶

static SGE(a, b)[source]¶

static BVS(ast)[source]¶

Parameters:: ast (BV)

If(cond, t, f)[source]¶

static Or(*args)[source]¶

static LShR(expr, shift_amount)[source]¶

static Concat(*args)[source]¶

static Extract(*args)[source]¶

static SignExt(*args)[source]¶

static ZeroExt(*args)[source]¶

static Reverse(arg)[source]¶

union(ast)[source]¶

intersection(ast)[source]¶

widen(ast)[source]¶

static CreateTopStridedInterval(bits, name=None)[source]¶

static constraint_to_si(expr)[source]¶

class claripy.backends.BackendZ3(reuse_z3_solver=None, ast_cache_size=10000)[source]¶

Bases: Backend

__init__(reuse_z3_solver=None, ast_cache_size=10000)[source]¶

property bvs_annotations: dict[bytes, tuple[Annotation, ...]]¶

downsize()[source]¶: Clears all caches associated with this backend.

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

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

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

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

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

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

StringV(**kwargs)[source]¶: The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.

StringS(**kwargs)[source]¶: The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.

call(*args, **kwargs)[source]¶

Calls operation op on args args with this backend.

Returns:: A backend object representing the result.

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

clone_solver(s)[source]¶

add(s, c, track=False)[source]¶

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

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

class claripy.backends.backend_concrete.BVV(value, bits)[source]¶

Bases: BackendObject

A concrete bitvector value. Used in the concrete backend for calculations. Any use outside of claripy should use claripy.BVV instead.

__init__(value, bits)[source]¶

bits¶

mod¶

property value¶

property signed¶

size()[source]¶

class claripy.backends.backend_concrete.FPV(value, sort)[source]¶

Bases: BackendObject

A concrete floating point value. Used in the concrete backend for calculations. Any use outside of claripy should use claripy.FPV instead.

__init__(value, sort)[source]¶

value¶

sort¶

fpSqrt()[source]¶

class claripy.backends.backend_concrete.BackendConcrete[source]¶

Bases: Backend

__init__()[source]¶

static BVV(value, size)[source]¶

static StringV(value)[source]¶

static FPV(op, sort)[source]¶

convert(expr)[source]¶: Override Backend.convert() to add fast paths for BVVs and BoolVs.

is_true(e, extra_constraints=(), solver=None, model_callback=None)[source]¶

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)[source]¶

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.

class claripy.backends.backend_concrete.StringV(value)[source]¶

Bases: BackendObject

A concrete string value. Used in the concrete backend for calculations. Any use outside of claripy should use claripy.StringV instead.

__init__(value)[source]¶

claripy.backends.backend_z3.handle_sigint(signals, frametype)[source]¶

Return type:

Any

Parameters:

signals (int)
frametype (FrameType | None)

claripy.backends.backend_z3.z3_expr_to_smt2(f, status='unknown', name='benchmark', logic='')[source]¶

claripy.backends.backend_z3.claripy_solver_to_smt2(s)[source]¶

claripy.backends.backend_z3.int_to_str_unlimited(v)[source]¶

Convert an integer to a decimal string, without any size limit.

Parameters:: v (int) – The integer to convert.
Return type:: str
Returns:: The string.

claripy.backends.backend_z3.Z3_to_int_str(val)[source]¶

claripy.backends.backend_z3.str_to_int_unlimited(s)[source]¶

Convert a decimal string to an integer, without any size limit.

Parameters:: s (str) – The string to convert.
Return type:: int
Returns:: The integer.

claripy.backends.backend_z3.condom(f)[source]¶

claripy.backends.backend_z3.z3_solver_sat(solver, extra_constraints, occasion)[source]¶

class claripy.backends.backend_z3.SmartLRUCache(maxsize, getsizeof=None, evict=None)[source]¶

Bases: LRUCache

__init__(maxsize, getsizeof=None, evict=None)[source]¶

popitem()[source]¶: Remove and return the (key, value) pair least recently used.

class claripy.backends.backend_z3.BackendZ3(reuse_z3_solver=None, ast_cache_size=10000)[source]¶

Bases: Backend

__init__(reuse_z3_solver=None, ast_cache_size=10000)[source]¶

property bvs_annotations: dict[bytes, tuple[Annotation, ...]]¶

downsize()[source]¶: Clears all caches associated with this backend.

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

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

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

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

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

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

StringV(**kwargs)[source]¶: The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.

StringS(**kwargs)[source]¶: The Z3 condom intercepts Z3Exceptions and throws a ClaripyZ3Error instead.

call(*args, **kwargs)[source]¶

Calls operation op on args args with this backend.

Returns:: A backend object representing the result.

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

clone_solver(s)[source]¶

add(s, c, track=False)[source]¶

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

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

class claripy.backends.backend_vsa.BackendVSA[source]¶

Bases: Backend

BackendVSA is a backend that uses VSA (Value Set Analysis) to represent and reason about values.

__init__()[source]¶

convert(expr)[source]¶

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)[source]¶

This should return the name of an expression.

Parameters:: a – the AST to evaluate

apply_annotation(o, a)[source]¶

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:

BackendObject

static BVV(ast)[source]¶

static BoolV(ast)[source]¶

static And(a, *args)[source]¶

static Not(a)[source]¶

static ULT(a, b)[source]¶

static ULE(a, b)[source]¶

static UGT(a, b)[source]¶

static UGE(a, b)[source]¶

static SLT(a, b)[source]¶

static SLE(a, b)[source]¶

static SGT(a, b)[source]¶

static SGE(a, b)[source]¶

static BVS(ast)[source]¶

Parameters:: ast (BV)

If(cond, t, f)[source]¶

static Or(*args)[source]¶

static LShR(expr, shift_amount)[source]¶

static Concat(*args)[source]¶

static Extract(*args)[source]¶

static SignExt(*args)[source]¶

static ZeroExt(*args)[source]¶

static Reverse(arg)[source]¶

union(ast)[source]¶

intersection(ast)[source]¶

widen(ast)[source]¶

static CreateTopStridedInterval(bits, name=None)[source]¶

static constraint_to_si(expr)[source]¶

class claripy.backends.backend_vsa.Balancer(c)[source]¶

Bases: object

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.

__init__(c)[source]¶

property compat_ret¶

property replacements¶

comparison_info = {'SGE': (False, True, False), 'SGT': (False, False, False), 'SLE': (True, True, False), 'SLT': (True, False, False), 'UGE': (False, True, True), 'UGT': (False, False, True), 'ULE': (True, True, True), 'ULT': (True, False, True), '__ge__': (False, True, False), '__gt__': (False, False, False), '__le__': (True, True, False), '__lt__': (True, False, False)}¶

class claripy.backends.backend_vsa.BoolResult(value)[source]¶

Bases: BackendObject

A class representing the result of a boolean operation. Values can be True, False, or Maybe.

Parameters:: value (tuple[bool, ...])

__init__(value)[source]¶

Parameters:: value (tuple[bool, ...])

value: tuple[bool, ...]¶

identical(other)[source]¶

union(other)[source]¶

property cardinality¶

static is_maybe(o)[source]¶

static has_true(o)[source]¶

static has_false(o)[source]¶

static is_true(o)[source]¶

static is_false(o)[source]¶

claripy.backends.backend_vsa.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)[source]¶

Parameters:

name
bits
stride
lower_bound
upper_bound
to_conv
discrete_set (bool)
discrete_set_max_cardinality (int)

Returns:

class claripy.backends.backend_vsa.DiscreteStridedIntervalSet(name=None, bits=0, si_set=None, max_cardinality=None)[source]¶

Bases: StridedInterval

A DiscreteStridedIntervalSet represents one or more discrete StridedInterval instances.

__init__(name=None, bits=0, si_set=None, max_cardinality=None)[source]¶

property cardinality¶

This is an over-approximation of the cardinality of this DSIS.

Returns:

property number_of_values¶

property stride¶

should_collapse()[source]¶

collapse()[source]¶

Collapse into a StridedInterval instance.

Returns:: A new StridedInterval instance.

normalize()[source]¶

Return the collapsed object if should_collapse() is True, otherwise return self.

Returns:: A DiscreteStridedIntervalSet object.

copy()[source]¶

concat(b)[source]¶

Operation concat

Parameters:: b – The other operand to concatenate with.
Returns:: The concatenated value.

extract(high_bit, low_bit)[source]¶

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)[source]¶

Parameters:

n
signed

Returns:

union(b)[source]¶

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.

intersection(b)[source]¶

reverse()[source]¶

Operation Reverse

Returns:: None

sign_extend(new_length)[source]¶

Operation SignExt

Parameters:: new_length – The length to extend to.
Returns:: SignExtended value.

zero_extend(new_length)[source]¶

Operation ZeroExt

Parameters:: new_length – The length to extend to.
Returns:: ZeroExtended value.

widen(b)[source]¶

Widening operator.

Parameters:: b – The other operand.
Returns:: The widened result.

claripy.backends.backend_vsa.FalseResult()[source]¶

Return a BoolResult representing the value False.

Return type:: BoolResult

claripy.backends.backend_vsa.MaybeResult()[source]¶

Return a BoolResult representing the value Maybe.

Return type:: BoolResult

class claripy.backends.backend_vsa.StridedInterval(name=None, bits=0, stride=None, lower_bound=None, upper_bound=None, uninitialized=False, bottom=False)[source]¶

Bases: BackendObject

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 signedness-agostic, please refer to [1] Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level 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 1-to-1 reproduction of [1].

Thanks all corresponding authors for their outstanding works.

__init__(name=None, bits=0, stride=None, lower_bound=None, upper_bound=None, uninitialized=False, bottom=False)[source]¶

copy()[source]¶

nameless_copy()[source]¶

normalize()[source]¶

eval(n, signed=False)[source]¶

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)[source]¶: Checks whether an integer is solution of the current strided Interval :type b: :param b: integer to check :return: True if b belongs to the current Strided Interval, False otherwhise

identical(o)[source]¶

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)[source]¶

Signed less than

Parameters:: o – The other operand
Returns:: TrueResult(), FalseResult(), or MaybeResult()

SLE(o)[source]¶

Signed less than or equal to.

Parameters:: o – The other operand.
Returns:: TrueResult(), FalseResult(), or MaybeResult()

SGT(o)[source]¶

Signed greater than.

Parameters:: o – The other operand
Returns:: TrueResult(), FalseResult(), or MaybeResult()

SGE(o)[source]¶

Signed greater than or equal to.

Parameters:: o – The other operand
Returns:: TrueResult(), FalseResult(), or MaybeResult()

ULT(o)[source]¶

Unsigned less than.

Parameters:: o – The other operand
Returns:: TrueResult(), FalseResult(), or MaybeResult()

ULE(o)[source]¶

Unsigned less than or equal to.

Parameters:: o – The other operand
Returns:: TrueResult(), FalseResult(), or MaybeResult()

UGT(o)[source]¶

Signed greater than.

Parameters:: o – The other operand
Returns:: TrueResult(), FalseResult(), or MaybeResult()

UGE(o)[source]¶

Unsigned greater than or equal to.

Parameters:: o – The other operand
Returns:: TrueResult(), FalseResult(), or MaybeResult()

eq(o)[source]¶

Equal

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

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

property name¶

property reversed¶

property cardinality¶

property complement¶

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

Returns:

property lower_bound¶

property upper_bound¶

property bits¶

property stride¶

property max¶

property min¶

property unique¶

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

property is_top¶

If this is a TOP value.

Returns:: True if this is a TOP

property is_bottom¶

Whether this StridedInterval is a BOTTOM, in other words, describes an empty set of integers.

Returns:: True/False

property is_integer¶

If this is an integer, i.e. self.lower_bound == self.upper_bound.

Returns:: True if this is an integer, False otherwise

property is_interval¶

property n_values¶

static lcm(a, b)[source]¶

Get the least common multiple.

Parameters:

a – The first operand (integer)
b – The second operand (integer)

Returns:

Their LCM

static gcd(a, b)[source]¶

Get the greatest common divisor.

Parameters:

a – The first operand (integer)
b – The second operand (integer)

Returns:

Their GCD

static highbit(k)[source]¶

static min_bits(val, max_bits=None)[source]¶

static max_int(k)[source]¶

static min_int(k)[source]¶

static signed_max_int(k)[source]¶

static signed_min_int(k)[source]¶

static upper(bits, i, stride)[source]¶

Returns:

static lower(bits, i, stride)[source]¶

Returns:

static top(bits, name=None, uninitialized=False)[source]¶

Get a TOP StridedInterval.

Returns:

static empty(bits)[source]¶

neg(*args, **kwargs)[source]¶

add(b)[source]¶

Binary operation: add

Parameters:: b – The other operand
Returns:: self + b

sub(b)[source]¶

Binary operation: sub

Parameters:: b – The other operand
Returns:: self - b

mul(o)[source]¶

Binary operation: multiplication

Parameters:: o – The other operand
Returns:: self * o

sdiv(o)[source]¶

Binary operation: signed division

Parameters:: o – The divisor
Returns:: (self / o) in signed arithmetic

udiv(o)[source]¶

Binary operation: unsigned division

Parameters:: o – The divisor
Returns:: (self / o) in unsigned arithmetic

bitwise_not(*args, **kwargs)[source]¶

bitwise_or(t)[source]¶

Binary operation: logical or

Parameters:: b – The other operand
Returns:: self | b

This implementation combines the approaches used by ‘WYSINWYX: what you see is not what you execute’ paper and ‘Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code’. The first paper provides an sound way to approximate the stride, whereas the second provides a way to calculate the or operation using wrapping intervals. Note that, even though according Warren’s work ‘Hacker’s delight’, one should follow different approaches to calculate the minimun/maximum values of an or operations according on the type of the operands (signed/unsigned). On the other other hand, by splitting the wrapping-intervals at the south pole, we can safely and soundly only use the Warren’s functions for unsigned integers.

bitwise_and(t)[source]¶

Binary operation: logical and

Parameters:: b – The other operand
Returns:

The following code implements the and operations as presented in the paper ‘Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code’

bitwise_xor(t)[source]¶

Operation xor

Parameters:: t – The other operand.

rshift_logical(*args, **kwargs)[source]¶

rshift_arithmetic(*args, **kwargs)[source]¶

lshift(*args, **kwargs)[source]¶

cast_low(*args, **kwargs)[source]¶

concat(b)[source]¶

extract(*args, **kwargs)[source]¶

agnostic_extend(*args, **kwargs)[source]¶

zero_extend(*args, **kwargs)[source]¶

sign_extend(*args, **kwargs)[source]¶

union(b)[source]¶

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(*intervals_to_join)[source]¶

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). :type intervals_to_join: :param intervals_to_join: Intervals to join :return: Interval that contains all intervals

static pseudo_join(s, b, smart_join=True)[source]¶

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 pseudo-join operation is not associative in wrapping intervals (please refer to section 3.1 paper ‘Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level 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(a, b)[source]¶

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 sign(a)[source]¶

static igcd(a, b)[source]¶

Parameters:

a – First integer
b – Second integer

Returns:

the integer GCD between a and b

static diop_natural_solution_linear(c, a, b)[source]¶

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

intersection(b)[source]¶

widen(b)[source]¶

reverse()[source]¶

This is a delayed reversing function. All it really does is to invert the _reversed property of this StridedInterval object.

Returns:: None

claripy.backends.backend_vsa.TrueResult()[source]¶

Return a BoolResult representing the value True.

Return type:: BoolResult

class claripy.backends.backend_vsa.ValueSet(name=None, region=None, region_base_addr=None, bits=None, val=None)[source]¶

Bases: BackendObject

ValueSet is a mapping between memory regions and corresponding offsets.

__init__(name=None, region=None, region_base_addr=None, bits=None, val=None)[source]¶

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

property name¶

property bits¶

property regions¶

property reversed¶

property unique¶

property cardinality¶

property is_empty¶

property valueset¶

static empty(bits)[source]¶

items()[source]¶

size()[source]¶

copy()[source]¶

Make a copy of self and return.

Returns:: A new ValueSet object.
Return type:: ValueSet

get_si(region)[source]¶

stridedinterval()[source]¶

LShR(other)[source]¶

SLT(other)[source]¶

SGT(other)[source]¶

SLE(other)[source]¶

SGE(other)[source]¶

eval(n, signed=False)[source]¶

property min¶

The minimum integer value of a value-set. It is only defined when there is exactly one region.

Returns:: A integer that represents the minimum integer value of this value-set.
Return type:: int

property max¶

The maximum integer value of a value-set. It is only defined when there is exactly one region.

Returns:: A integer that represents the maximum integer value of this value-set.
Return type:: int

reverse()[source]¶

extract(high_bit, low_bit)[source]¶

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

concat(b)[source]¶

union(b)[source]¶

widen(b)[source]¶

intersection(b)[source]¶

identical(o)[source]¶

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.

Frontends¶

class claripy.frontend.CompositeFrontend(template_frontend, track=False, **kwargs)[source]¶

Bases: ConstrainedFrontend

Composite Solver splits constraints into independent sets, allowing caching to be done on a per-set basis. Additionally, by allowing constraints to be solved independently, the solver can be more efficient in some cases (“divide and conquer”).

For example, the constraints (a==b, b==1, c==4) would be split into two sets: one containing a==b and b==1, and the other containing c==4.

__init__(template_frontend, track=False, **kwargs)[source]¶

downsize()[source]¶

property variables¶

check_satisfiability(extra_constraints=(), exact=None)[source]¶

Checks the satisfiability of stored constraints conjunction.

Parameters:

extra_constraints – extra constraints to consider when checking satisfiability
exact – whether or not to perform exact checking. Ignored by non-approximating backends.

Returns:

‘SAT’ if the conjunction is satisfiable otherwise ‘UNSAT’

satisfiable(extra_constraints=(), exact=None)[source]¶

Checks if stored constraints conjunction is satisfiable.

Parameters:

extra_constraints – extra constraints to consider when checking satisfiability
exact – whether or not to perform exact checking. Ignored by non-approximating backends.

Returns:

True if the conjunction is satisfiable otherwise False

eval(e, n, extra_constraints=(), exact=None)[source]¶

Evaluates expression e, returning a tuple of n solutions.

Parameters:

e – the expression
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

tuple of python primitives representing results

batch_eval(exprs, n, extra_constraints=(), exact=None)[source]¶

Evaluates exprs, returning a list of tuples (one tuple of n solutions for expression).

Parameters:

exprs – expressions
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

list of tuples of python primitives representing results

max(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its max possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

max possible value

min(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its min possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

min possible value

solution(e, v, extra_constraints=(), exact=None)[source]¶

Checks if v is a possible solution to e.

Parameters:

e – the expression
v – the value
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it is a possible solution otherwise False

is_true(e, extra_constraints=(), exact=None)[source]¶

Checks if e can only (and TRIVIALLY) evaluate to True. If this function returns True, then the expression cannot ever be False, regardless of constraints or anything else. If the expression returns False, then the expression might STILL not ever be False; it’s just that we can’t trivially prove it. In other words, a return value of False gives you no information whatsoever.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it can only evaluate to True otherwise False

is_false(e, extra_constraints=(), exact=None)[source]¶

Checks if e can only (and TRIVIALLY) evaluate to False. If this function returns True, then the expression cannot ever be True, regardless of constraints or anything else. If the expression returns False, then the expression might STILL not ever be True; it’s just that we can’t trivially prove it. In other words, a return value of False gives you no information whatsoever.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it can only evaluate to False otherwise False

unsat_core(extra_constraints=())[source]¶

simplify()[source]¶: Simplifies the stored constraints conjunction.

finalize()[source]¶

property timeout¶

property max_memory¶

merge(others, merge_conditions, common_ancestor=None)[source]¶

split()[source]¶

class claripy.frontend.Frontend[source]¶

Bases: object

Frontend is the base class for all claripy Solvers, which are the interfaces to the backend constraint solvers.

__init__()[source]¶

branch()[source]¶

blank_copy()[source]¶

eval_to_ast(e, n, extra_constraints=(), exact=None)[source]¶

Evaluates expression e, returning a list of n concrete ASTs.

Parameters:

e – the expression
n – the number of ASTs to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

list of concrete ASTs

finalize()[source]¶

merge(others, merge_conditions, common_ancestor=None)[source]¶

combine(others)[source]¶

split()[source]¶

add(constraints, invalidate_cache=True)[source]¶

Adds constraint(s) to constraints list.

Parameters:: constraints – constraint(s) to add
Returns:

simplify()[source]¶: Simplifies the stored constraints conjunction.

check_satisfiability(extra_constraints=(), exact=None)[source]¶

Checks the satisfiability of stored constraints conjunction.

Parameters:

extra_constraints – extra constraints to consider when checking satisfiability
exact – whether or not to perform exact checking. Ignored by non-approximating backends.

Returns:

‘SAT’ if the conjunction is satisfiable otherwise ‘UNSAT’

satisfiable(extra_constraints=(), exact=None)[source]¶

Checks if stored constraints conjunction is satisfiable.

Parameters:

extra_constraints – extra constraints to consider when checking satisfiability
exact – whether or not to perform exact checking. Ignored by non-approximating backends.

Returns:

True if the conjunction is satisfiable otherwise False

eval(e, n, extra_constraints=(), exact=None)[source]¶

Evaluates expression e, returning a tuple of n solutions.

Parameters:

e – the expression
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

tuple of python primitives representing results

batch_eval(exprs, n, extra_constraints=(), exact=None)[source]¶

Evaluates exprs, returning a list of tuples (one tuple of n solutions for expression).

Parameters:

exprs – expressions
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

list of tuples of python primitives representing results

max(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its max possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

max possible value

min(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its min possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

min possible value

solution(e, v, extra_constraints=(), exact=None)[source]¶

Checks if v is a possible solution to e.

Parameters:

e – the expression
v – the value
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it is a possible solution otherwise False

is_true(e, extra_constraints=(), exact=None)[source]¶

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it can only evaluate to True otherwise False

is_false(e, extra_constraints=(), exact=None)[source]¶

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it can only evaluate to False otherwise False

downsize()[source]¶

class claripy.frontend.FullFrontend(solver_backend, timeout=None, max_memory=None, track=False, **kwargs)[source]¶

Bases: ConstrainedFrontend

FullFrontend is a frontend that supports all claripy operations and is backed by a full solver backend.

__init__(solver_backend, timeout=None, max_memory=None, track=False, **kwargs)[source]¶

simplify()[source]¶: Simplifies the stored constraints conjunction.

check_satisfiability(extra_constraints=(), exact=None)[source]¶

Checks the satisfiability of stored constraints conjunction.

Parameters:

extra_constraints – extra constraints to consider when checking satisfiability
exact – whether or not to perform exact checking. Ignored by non-approximating backends.

Return type:

bool

Returns:

‘SAT’ if the conjunction is satisfiable otherwise ‘UNSAT’

satisfiable(extra_constraints=(), exact=None)[source]¶

Checks if stored constraints conjunction is satisfiable.

Parameters:

extra_constraints (Iterable[Bool]) – extra constraints to consider when checking satisfiability
exact (Optional[bool]) – whether or not to perform exact checking. Ignored by non-approximating backends.

Return type:

bool

Returns:

True if the conjunction is satisfiable otherwise False

eval(e, n, extra_constraints=(), exact=None)[source]¶

Evaluates expression e, returning a tuple of n solutions.

Parameters:

e – the expression
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Return type:

tuple[Any, ...]

Returns:

tuple of python primitives representing results

batch_eval(exprs, n, extra_constraints=(), exact=None)[source]¶

Evaluates exprs, returning a list of tuples (one tuple of n solutions for expression).

Parameters:

exprs – expressions
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

list of tuples of python primitives representing results

max(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its max possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

max possible value

min(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its min possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

min possible value

solution(e, v, extra_constraints=(), exact=None)[source]¶

Checks if v is a possible solution to e.

Parameters:

e – the expression
v – the value
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it is a possible solution otherwise False

is_true(e, extra_constraints=(), exact=None)[source]¶

Parameters:

e (Bool) – the expression
extra_constraints (tuple[Bool, ...]) – extra constraints to consider when performing the evaluation
exact (Optional[bool]) – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Return type:

bool

Returns:

True if it can only evaluate to True otherwise False

is_false(e, extra_constraints=(), exact=None)[source]¶

Parameters:

e (Bool) – the expression
extra_constraints (tuple[Bool, ...]) – extra constraints to consider when performing the evaluation
exact (Optional[bool]) – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Return type:

bool

Returns:

True if it can only evaluate to False otherwise False

unsat_core(extra_constraints=())[source]¶

Return type:: Iterable[Bool]
Parameters:: extra_constraints (tuple[Bool, ...])

downsize()[source]¶

Return type:: None

merge(others, merge_conditions, common_ancestor=None)[source]¶

Return type:: tuple[bool, Self]

class claripy.frontend.HybridFrontend(exact_frontend, approximate_frontend, approximate_first=False, **kwargs)[source]¶

Bases: Frontend

HybridFrontend is a frontend that uses two backends, one exact and one approximate, to solve constraints.

In practice this allows there to be a solver that can use the VSA backend or the Z3 backend depending on the constraints.

__init__(exact_frontend, approximate_frontend, approximate_first=False, **kwargs)[source]¶

property constraints¶

property variables¶

satisfiable(extra_constraints=(), exact=None)[source]¶

Checks if stored constraints conjunction is satisfiable.

Parameters:

extra_constraints – extra constraints to consider when checking satisfiability
exact – whether or not to perform exact checking. Ignored by non-approximating backends.

Returns:

True if the conjunction is satisfiable otherwise False

eval_to_ast(e, n, extra_constraints=(), exact=None)[source]¶

Evaluates expression e, returning a list of n concrete ASTs.

Parameters:

e – the expression
n – the number of ASTs to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

list of concrete ASTs

eval(e, n, extra_constraints=(), exact=None)[source]¶

Evaluates expression e, returning a tuple of n solutions.

Parameters:

e – the expression
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

tuple of python primitives representing results

batch_eval(exprs, n, extra_constraints=(), exact=None)[source]¶

Evaluates exprs, returning a list of tuples (one tuple of n solutions for expression).

Parameters:

exprs – expressions
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

list of tuples of python primitives representing results

max(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its max possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

max possible value

min(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its min possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

min possible value

solution(e, v, extra_constraints=(), exact=None)[source]¶

Checks if v is a possible solution to e.

Parameters:

e – the expression
v – the value
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it is a possible solution otherwise False

is_true(e, extra_constraints=(), exact=None)[source]¶

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it can only evaluate to True otherwise False

is_false(e, extra_constraints=(), exact=None)[source]¶

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it can only evaluate to False otherwise False

unsat_core(extra_constraints=())[source]¶

combine(others)[source]¶

merge(others, merge_conditions, common_ancestor=None)[source]¶

simplify()[source]¶: Simplifies the stored constraints conjunction.

downsize()[source]¶

finalize()[source]¶

split()[source]¶

class claripy.frontend.LightFrontend(solver_backend, **kwargs)[source]¶

Bases: ConstrainedFrontend

LightFrontend is an extremely simple frontend that is used primarily for the purpose of quickly evaluating expressions using the concrete and VSA backends.

__init__(solver_backend, **kwargs)[source]¶

eval(e, n, extra_constraints=(), exact=None)[source]¶

Evaluates expression e, returning a tuple of n solutions.

Parameters:

e – the expression
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

tuple of python primitives representing results

batch_eval(exprs, n, extra_constraints=(), exact=None)[source]¶

Evaluates exprs, returning a list of tuples (one tuple of n solutions for expression).

Parameters:

exprs – expressions
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

list of tuples of python primitives representing results

max(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its max possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

max possible value

min(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its min possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

min possible value

solution(e, v, extra_constraints=(), exact=None)[source]¶

Checks if v is a possible solution to e.

Parameters:

e – the expression
v – the value
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it is a possible solution otherwise False

is_true(e, extra_constraints=(), exact=None)[source]¶

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it can only evaluate to True otherwise False

is_false(e, extra_constraints=(), exact=None)[source]¶

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it can only evaluate to False otherwise False

satisfiable(extra_constraints=(), exact=None)[source]¶

Checks if stored constraints conjunction is satisfiable.

Parameters:

extra_constraints – extra constraints to consider when checking satisfiability
exact – whether or not to perform exact checking. Ignored by non-approximating backends.

Returns:

True if the conjunction is satisfiable otherwise False

merge(others, merge_conditions, common_ancestor=None)[source]¶

class claripy.frontend.ReplacementFrontend(actual_frontend, allow_symbolic=None, replacements=None, replacement_cache=None, unsafe_replacement=None, complex_auto_replace=None, auto_replace=None, replace_constraints=None, **kwargs)[source]¶

Bases: ConstrainedFrontend

ReplacementFrontend is a frontend that allows for the replacement symbolic constraints with concrete solutions. This is useful for simplifying constraints and speeding up solving time.

__init__(actual_frontend, allow_symbolic=None, replacements=None, replacement_cache=None, unsafe_replacement=None, complex_auto_replace=None, auto_replace=None, replace_constraints=None, **kwargs)[source]¶

add_replacement(old, new, invalidate_cache=True, replace=True, promote=True)[source]¶

remove_replacements(old_entries)[source]¶

clear_replacements()[source]¶

downsize()[source]¶

eval(e, n, extra_constraints=(), exact=None)[source]¶

Evaluates expression e, returning a tuple of n solutions.

Parameters:

e – the expression
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

tuple of python primitives representing results

batch_eval(exprs, n, extra_constraints=(), exact=None)[source]¶

Evaluates exprs, returning a list of tuples (one tuple of n solutions for expression).

Parameters:

exprs – expressions
n – the number of solutions to return
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

list of tuples of python primitives representing results

max(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its max possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

max possible value

min(e, extra_constraints=(), signed=False, exact=None)[source]¶

Evaluates e, returning its min possible value.

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
signed – whether the value should be treated as a signed integer
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

min possible value

solution(e, v, extra_constraints=(), exact=None)[source]¶

Checks if v is a possible solution to e.

Parameters:

e – the expression
v – the value
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it is a possible solution otherwise False

is_true(e, extra_constraints=(), exact=None)[source]¶

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it can only evaluate to True otherwise False

is_false(e, extra_constraints=(), exact=None)[source]¶

Parameters:

e – the expression
extra_constraints – extra constraints to consider when performing the evaluation
exact – whether or not to perform an exact evaluation. Ignored by non-approximating backends.

Returns:

True if it can only evaluate to False otherwise False

satisfiable(extra_constraints=(), exact=None)[source]¶

Checks if stored constraints conjunction is satisfiable.

Parameters:

extra_constraints – extra constraints to consider when checking satisfiability
exact – whether or not to perform exact checking. Ignored by non-approximating backends.

Returns:

True if the conjunction is satisfiable otherwise False

class claripy.solvers.Solver(backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

Bases: ConcreteHandlerMixin, EagerResolutionMixin, ConstraintFilterMixin, ConstraintDeduplicatorMixin, SimplifySkipperMixin, SatCacheMixin, ModelCacheMixin, ConstraintExpansionMixin, SimplifyHelperMixin, FullFrontend

Solver is the default Claripy frontend. It uses Z3 as the backend solver by default.

__init__(backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

class claripy.solvers.SolverCacheless(backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

Bases: ConcreteHandlerMixin, EagerResolutionMixin, ConstraintFilterMixin, ConstraintDeduplicatorMixin, SimplifySkipperMixin, FullFrontend

SolverCacheless is a Solver without caching. It uses Z3 as the backend solver by default.

__init__(backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

class claripy.solvers.SolverReplacement(actual_frontend=None, **kwargs)[source]¶

Bases: ConcreteHandlerMixin, ConstraintDeduplicatorMixin, ReplacementFrontend

SolverReplacement is a frontend wrapper that replaces constraints with their solutions.

__init__(actual_frontend=None, **kwargs)[source]¶

class claripy.solvers.SolverHybrid(exact_frontend=None, approximate_frontend=None, complex_auto_replace=True, replace_constraints=True, track=False, approximate_first=False, **kwargs)[source]¶

Bases: ConcreteHandlerMixin, EagerResolutionMixin, ConstraintFilterMixin, ConstraintDeduplicatorMixin, SimplifySkipperMixin, HybridFrontend

SolverHybrid is a frontend that uses an exact solver and an approximate solver.

__init__(exact_frontend=None, approximate_frontend=None, complex_auto_replace=True, replace_constraints=True, track=False, approximate_first=False, **kwargs)[source]¶

class claripy.solvers.SolverVSA(**kwargs)[source]¶

Bases: ConcreteHandlerMixin, ConstraintFilterMixin, LightFrontend

SolverVSA is a thin frontend to the VSA backend solver.

__init__(**kwargs)[source]¶

class claripy.solvers.SolverConcrete(**kwargs)[source]¶

Bases: ConcreteHandlerMixin, ConstraintFilterMixin, LightFrontend

SolverConcrete is a thin frontend to the Concrete backend solver.

__init__(**kwargs)[source]¶

class claripy.solvers.SolverStrings(*args, backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

Bases: ConcreteHandlerMixin, ConstraintFilterMixin, ConstraintDeduplicatorMixin, EagerResolutionMixin, FullFrontend

SolverStrings is a frontend that uses Z3 to solve string constraints.

__init__(*args, backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

class claripy.solvers.SolverCompositeChild(backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

Bases: ConstraintDeduplicatorMixin, SatCacheMixin, SimplifySkipperMixin, ModelCacheMixin, FullFrontend

SolverCompositeChild is a frontend that is used as a child in a SolverComposite.

__init__(backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

class claripy.solvers.SolverComposite(template_solver=None, track=False, **kwargs)[source]¶

Bases: ConcreteHandlerMixin, EagerResolutionMixin, ConstraintFilterMixin, ConstraintDeduplicatorMixin, SatCacheMixin, SimplifySkipperMixin, SimplifyHelperMixin, ConstraintExpansionMixin, CompositedCacheMixin, CompositeFrontend

SolverComposite is a frontend that composes multiple templated frontends.

__init__(template_solver=None, track=False, **kwargs)[source]¶

Frontend Mixins¶

Annotations¶

class claripy.annotation.Annotation[source]¶

Bases: object

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.

property eliminatable: bool¶

Returns whether this annotation can be eliminated in a simplification.

Returns:: True if eliminatable, False otherwise

property relocatable: bool¶

Returns whether this annotation can be relocated in a simplification.

Returns:: True if it can be relocated, false otherwise.

relocate(src, dst)[source]¶

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 + zero

Here, 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 (Base) – the old AST that was eliminated in the simplification
dst (Base) – the new AST (the result of a simplification)

Returns:

the annotation that will be applied to dst

class claripy.annotation.SimplificationAvoidanceAnnotation[source]¶

Bases: Annotation

SimplificationAvoidanceAnnotation is an annotation that prevents simplification of an AST.

property eliminatable¶

Returns whether this annotation can be eliminated in a simplification.

Returns:: True if eliminatable, False otherwise

property relocatable¶

Returns whether this annotation can be relocated in a simplification.

Returns:: True if it can be relocated, false otherwise.

class claripy.annotation.StridedIntervalAnnotation(stride, lower_bound, upper_bound)[source]¶

Bases: SimplificationAvoidanceAnnotation

StridedIntervalAnnotation allows annotating a BVS to represent a strided interval.

Parameters:

stride (int)
lower_bound (int)
upper_bound (int)

__init__(stride, lower_bound, upper_bound)[source]¶

Parameters:

stride (int)
lower_bound (int)
upper_bound (int)

stride: int¶

lower_bound: int¶

upper_bound: int¶

class claripy.annotation.RegionAnnotation(region_id, region_base_addr)[source]¶

Bases: SimplificationAvoidanceAnnotation

Use RegionAnnotation to annotate ASTs. Normally, an AST annotated by RegionAnnotations is treated as a ValueSet.

__init__(region_id, region_base_addr)[source]¶

class claripy.annotation.UninitializedAnnotation[source]¶

Bases: Annotation

Use UninitializedAnnotation to annotate ASTs that are uninitialized.

eliminatable = False¶

relocatable = True¶

VSA¶

Misc. Things¶

claripy.BVS(name, size, explicit_name=None, **kwargs)[source]¶

Creates a bit-vector symbol (i.e., a variable).

Parameters:

name – The name of the symbol.
size – The size (in bits) of the bit-vector.
explicit_name (bool) – If False, an identifier is appended to the name to ensure uniqueness.

Return type:

BV

Returns:

a BV object representing this symbol.

claripy.BVV(value, size=None, **kwargs)[source]¶

Creates a bit-vector value (i.e., a concrete value).

Parameters:

value – The value. Either an integer or a bytestring. If it’s the latter, it will be interpreted as the bytes of a big-endian constant.
size – The size (in bits) of the bit-vector. Optional if you provide a string, required for an integer.

Return type:

BV

Returns:

A BV object representing this value.

claripy.ESI(bits, **kwargs)[source]¶

claripy.FPS(name, sort, explicit_name=None)[source]¶

Creates a floating-point 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.

Return type:

FP

Returns:

An FP AST.

claripy.FPV(value, sort)[source]¶

Creates a concrete floating-point value.

Parameters:

value – The value of the floating point.
sort – The sort of the floating point.

Return type:

FP

Returns:

An FP AST.

class claripy.RM(value)[source]¶

Bases: Enum

Rounding modes for floating point operations.

See https://en.wikipedia.org/wiki/IEEE_754#Rounding_rules for more information.

RM_NearestTiesEven = 'RM_RNE'¶

RM_NearestTiesAwayFromZero = 'RM_RNA'¶

RM_TowardsZero = 'RM_RTZ'¶

RM_TowardsPositiveInf = 'RM_RTP'¶

RM_TowardsNegativeInf = 'RM_RTN'¶

static default()[source]¶

pydecimal_equivalent_rounding_mode()[source]¶

claripy.SGE(*args)¶

claripy.SGT(*args)¶

claripy.SI(name='unnamed', bits=0, lower_bound=None, upper_bound=None, stride=None, explicit_name=None)[source]¶

claripy.SLE(*args)¶

claripy.SLT(*args)¶

claripy.TSI(bits, name=None, explicit_name=None)[source]¶

claripy.UGE(*args)¶

claripy.UGT(*args)¶

claripy.ULE(*args)¶

claripy.ULT(*args)¶

claripy.VS(bits, region, region_base_addr, value)¶

Parameters:

bits (int)
region (str)
region_base_addr (int)
value (BV | int)

claripy.And(*args)¶

class claripy.Annotation[source]¶

Bases: object

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.

property eliminatable: bool¶

Returns whether this annotation can be eliminated in a simplification.

Returns:: True if eliminatable, False otherwise

property relocatable: bool¶

Returns whether this annotation can be relocated in a simplification.

Returns:: True if it can be relocated, false otherwise.

relocate(src, dst)[source]¶

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 + zero

Here, 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 (Base) – the old AST that was eliminated in the simplification
dst (Base) – the new AST (the result of a simplification)

Returns:

the annotation that will be applied to dst

claripy.BoolS(name, explicit_name=None)[source]¶

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.

Return type:

Bool

Returns:

A Bool object representing this symbol.

claripy.BoolV(val)[source]¶

Return type:: Bool

exception claripy.ClaripyError[source]¶: Bases: Exception

exception claripy.ClaripyFrontendError[source]¶: Bases: ClaripyError

exception claripy.ClaripyOperationError[source]¶: Bases: ClaripyASTError

exception claripy.ClaripySolverInterruptError[source]¶: Bases: ClaripyError

exception claripy.ClaripyZeroDivisionError[source]¶: Bases: ClaripyOperationError, ZeroDivisionError

claripy.Concat(*args)¶

claripy.Extract(*args)¶

claripy.If(cond, true_value, false_value)[source]¶

claripy.IntToStr(*args)¶

claripy.LShR(*args)¶

claripy.Not(*args)¶

claripy.Or(*args)¶

class claripy.RegionAnnotation(region_id, region_base_addr)[source]¶

Bases: SimplificationAvoidanceAnnotation

Use RegionAnnotation to annotate ASTs. Normally, an AST annotated by RegionAnnotations is treated as a ValueSet.

__init__(region_id, region_base_addr)[source]¶

claripy.Reverse(*args)¶

claripy.RotateLeft(*args)¶

claripy.RotateRight(*args)¶

claripy.SDiv(*args)¶

claripy.SMod(*args)¶

claripy.SignExt(*args)¶

class claripy.SimplificationAvoidanceAnnotation[source]¶

Bases: Annotation

SimplificationAvoidanceAnnotation is an annotation that prevents simplification of an AST.

property eliminatable¶

Returns whether this annotation can be eliminated in a simplification.

Returns:: True if eliminatable, False otherwise

property relocatable¶

Returns whether this annotation can be relocated in a simplification.

Returns:: True if it can be relocated, false otherwise.

class claripy.Solver(backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

Solver is the default Claripy frontend. It uses Z3 as the backend solver by default.

__init__(backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

class claripy.SolverCacheless(backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

Bases: ConcreteHandlerMixin, EagerResolutionMixin, ConstraintFilterMixin, ConstraintDeduplicatorMixin, SimplifySkipperMixin, FullFrontend

SolverCacheless is a Solver without caching. It uses Z3 as the backend solver by default.

__init__(backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

class claripy.SolverComposite(template_solver=None, track=False, **kwargs)[source]¶

SolverComposite is a frontend that composes multiple templated frontends.

__init__(template_solver=None, track=False, **kwargs)[source]¶

class claripy.SolverConcrete(**kwargs)[source]¶

Bases: ConcreteHandlerMixin, ConstraintFilterMixin, LightFrontend

SolverConcrete is a thin frontend to the Concrete backend solver.

__init__(**kwargs)[source]¶

class claripy.SolverHybrid(exact_frontend=None, approximate_frontend=None, complex_auto_replace=True, replace_constraints=True, track=False, approximate_first=False, **kwargs)[source]¶

Bases: ConcreteHandlerMixin, EagerResolutionMixin, ConstraintFilterMixin, ConstraintDeduplicatorMixin, SimplifySkipperMixin, HybridFrontend

SolverHybrid is a frontend that uses an exact solver and an approximate solver.

__init__(exact_frontend=None, approximate_frontend=None, complex_auto_replace=True, replace_constraints=True, track=False, approximate_first=False, **kwargs)[source]¶

class claripy.SolverReplacement(actual_frontend=None, **kwargs)[source]¶

Bases: ConcreteHandlerMixin, ConstraintDeduplicatorMixin, ReplacementFrontend

SolverReplacement is a frontend wrapper that replaces constraints with their solutions.

__init__(actual_frontend=None, **kwargs)[source]¶

class claripy.SolverStrings(*args, backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

Bases: ConcreteHandlerMixin, ConstraintFilterMixin, ConstraintDeduplicatorMixin, EagerResolutionMixin, FullFrontend

SolverStrings is a frontend that uses Z3 to solve string constraints.

__init__(*args, backend=<claripy.backends.backend_z3.BackendZ3 object>, **kwargs)[source]¶

class claripy.SolverVSA(**kwargs)[source]¶

Bases: ConcreteHandlerMixin, ConstraintFilterMixin, LightFrontend

SolverVSA is a thin frontend to the VSA backend solver.

__init__(**kwargs)[source]¶

claripy.StrConcat(*args)¶

claripy.StrContains(*args)¶

claripy.StrIndexOf(*args)¶

claripy.StrIsDigit(*args)¶

claripy.StrLen(*args)¶

claripy.StrPrefixOf(*args)¶

claripy.StrReplace(*args)¶

claripy.StrSubstr(*args)¶

claripy.StrSuffixOf(*args)¶

claripy.StrToInt(*args)¶

claripy.StringS(name, explicit_name=False, **kwargs)[source]¶

Create a new symbolic string (analogous to z3.String())

Parameters:

name – The name of the symbolic string (i. e. the name of the variable)
explicit_name (bool) – If False, an identifier is appended to the name to ensure uniqueness.

Returns:

The String object representing the symbolic string

claripy.StringV(value, **kwargs)[source]¶

Create a new Concrete string (analogous to z3.StringVal())

Parameters:: value – The constant value of the concrete string
Returns:: The String object representing the concrete string

class claripy.UninitializedAnnotation[source]¶

Bases: Annotation

Use UninitializedAnnotation to annotate ASTs that are uninitialized.

eliminatable = False¶

relocatable = True¶

exception claripy.UnsatError[source]¶: Bases: ClaripyError

claripy.ValueSet(bits, region, region_base_addr, value)[source]¶

Parameters:

bits (int)
region (str)
region_base_addr (int)
value (BV | int)

claripy.ZeroExt(*args)¶

claripy.burrow_ite(expr)[source]¶

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

Return type:: TypeVar(T, bound= Base)
Parameters:: expr (T)

claripy.constraint_to_si(expr)[source]¶

Convert a constraint to SI if possible.

Parameters:: expr
Returns:

claripy.excavate_ite(expr)[source]¶

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.

Return type:: TypeVar(T, bound= Base)
Parameters:: expr (T)

claripy.false()[source]¶

claripy.fpAbs(*args)¶

claripy.fpAdd(*args)¶

claripy.fpDiv(*args)¶

claripy.fpEQ(*args)¶

claripy.fpFP(*args)¶

claripy.fpGEQ(*args)¶

claripy.fpGT(*args)¶

claripy.fpIsInf(*args)¶

claripy.fpIsNaN(*args)¶

claripy.fpLEQ(*args)¶

claripy.fpLT(*args)¶

claripy.fpMul(*args)¶

claripy.fpNEQ(*args)¶

claripy.fpNeg(*args)¶

claripy.fpSqrt(*args)¶

claripy.fpSub(*args)¶

claripy.fpToFP(*args)¶

claripy.fpToFPUnsigned(*args)¶

claripy.fpToIEEEBV(*args)¶

claripy.fpToSBV(*args)¶

claripy.fpToUBV(*args)¶

claripy.intersection(*args)¶

claripy.is_false(expr)[source]¶

Checks if a boolean expression is trivially False.

A false result does not necessarily mean that the expression is False, but rather that it is not trivially False.

Return type:: bool
Parameters:: expr (Bool)

claripy.is_true(expr)[source]¶

Checks if a boolean expression is trivially True.

A false result does not necessarily mean that the expression is False, but rather that it is not trivially True.

Return type:: bool
Parameters:: expr (Bool)

claripy.ite_cases(cases, default)[source]¶

Return an expression of if-then-else trees which expresses a series of alternatives

Parameters:

cases – A list of tuples (c, v). c is the condition under which v should be the result of the expression
default – A default value that the expression should take on if none of the c conditions are satisfied

Returns:

An expression encoding the result of the above

claripy.ite_dict(i, d, default)[source]¶: Return an expression of if-then-else trees which expresses a switch tree :type i: :param i: The variable which may take on multiple values affecting the final result :type d: :param d: A dict mapping possible values for i to values which the result could be :type default: :param default: A default value that the expression should take on if i matches none of the keys of d :return: An expression encoding the result of the above

claripy.replace(expr, old, new)[source]¶

Returns this AST but with the AST ‘old’ replaced with AST ‘new’ in its subexpressions.

Return type:

Base

Parameters:

expr (Base)
old (T)
new (T)

claripy.replace_dict(expr, replacements, variable_set=None, leaf_operation=<function <lambda>>)[source]¶

Returns this AST with subexpressions replaced by those that can be found in replacements dict.

Parameters:

variable_set (Optional[set[str]]) – For optimization, ast’s without these variables are not checked for replacing.
replacements (dict[int, Base]) – A dictionary of hashes to their replacements.
leaf_operation (Callable[[Base], Base]) – An operation that should be applied to the leaf nodes.
expr (Base)

Return type:

Base

Returns:

An AST with all instances of ast’s in replacements.

claripy.reverse_ite_cases(ast)[source]¶: Given an expression created by ite_cases, produce the cases that generated it :type ast: :param ast: :return:

claripy.set_debug(enabled)[source]¶: Enable or disable the debug mode. In debug mode, a bunch of extra checks in claripy will be executed. You’ll want to disable debug mode if you are running performance critical code.

claripy.simplify(expr)[source]¶

Simplify an expression.

Return type:: TypeVar(T, bound= Base)
Parameters:: expr (T)

claripy.true()[source]¶

claripy.union(*args)¶

claripy.widen(*args)¶

exception claripy.errors.ClaripyError[source]¶: Bases: Exception

exception claripy.errors.UnsatError[source]¶: Bases: ClaripyError

exception claripy.errors.ClaripyFrontendError[source]¶: Bases: ClaripyError

exception claripy.errors.ClaripySerializationError[source]¶: Bases: ClaripyError

exception claripy.errors.BackendError[source]¶: Bases: ClaripyError

exception claripy.errors.BackendUnsupportedError[source]¶: Bases: BackendError

exception claripy.errors.ClaripyZ3Error[source]¶: Bases: ClaripyError

exception claripy.errors.ClaripyBackendVSAError[source]¶: Bases: BackendError

exception claripy.errors.MissingSolverError[source]¶: Bases: ClaripyError

exception claripy.errors.ClaripySolverInterruptError[source]¶: Bases: ClaripyError

exception claripy.errors.ClaripyASTError[source]¶: Bases: ClaripyError

exception claripy.errors.ClaripyBalancerError[source]¶: Bases: ClaripyASTError

exception claripy.errors.ClaripyBalancerUnsatError[source]¶: Bases: ClaripyBalancerError

exception claripy.errors.ClaripyTypeError[source]¶: Bases: ClaripyASTError

exception claripy.errors.ClaripyValueError[source]¶: Bases: ClaripyASTError

exception claripy.errors.ClaripySizeError[source]¶: Bases: ClaripyASTError

exception claripy.errors.ClaripyOperationError[source]¶: Bases: ClaripyASTError

exception claripy.errors.ClaripyReplacementError[source]¶: Bases: ClaripyASTError

exception claripy.errors.ClaripyRecursionError[source]¶: Bases: ClaripyOperationError

exception claripy.errors.ClaripyZeroDivisionError[source]¶: Bases: ClaripyOperationError, ZeroDivisionError

class claripy.fp.RM(value)[source]¶

Bases: Enum

Rounding modes for floating point operations.

See https://en.wikipedia.org/wiki/IEEE_754#Rounding_rules for more information.

RM_NearestTiesEven = 'RM_RNE'¶

RM_NearestTiesAwayFromZero = 'RM_RNA'¶

RM_TowardsZero = 'RM_RTZ'¶

RM_TowardsPositiveInf = 'RM_RTP'¶

RM_TowardsNegativeInf = 'RM_RTN'¶

static default()[source]¶

pydecimal_equivalent_rounding_mode()[source]¶

class claripy.fp.FSort(name, exp, mantissa)[source]¶

Bases: object

A class representing a floating point sort.

__init__(name, exp, mantissa)[source]¶

property length¶

static from_size(n)[source]¶

static from_params(exp, mantissa)[source]¶

claripy.operations.op(name, arg_types, return_type, extra_check=None, calc_length=None)[source]¶

Return type:: Callable[..., TypeVar(T, bound= Base)]
Parameters:: return_type (type[T])

claripy.operations.reversed_op(op_func)[source]¶

claripy.operations.length_same_check(*args)[source]¶

claripy.operations.basic_length_calc(*args)[source]¶

claripy.operations.extract_check(high, low, bv)[source]¶

claripy.operations.extend_check(amount, _)[source]¶

claripy.operations.concat_length_calc(*args)[source]¶

claripy.operations.extract_length_calc(high, low, _)[source]¶

claripy.operations.ext_length_calc(ext, orig)[source]¶

claripy.simplifications.if_simplifier(cond, if_true, if_false)[source]¶

claripy.simplifications.concat_simplifier(*args)[source]¶

claripy.simplifications.rshift_simplifier(val, shift)[source]¶

claripy.simplifications.lshr_simplifier(val, shift)[source]¶

claripy.simplifications.lshift_simplifier(val, shift)[source]¶

claripy.simplifications.eq_simplifier(a, b)[source]¶

claripy.simplifications.ne_simplifier(a, b)[source]¶

claripy.simplifications.ge_simplifier(a, b)[source]¶

claripy.simplifications.bv_reverse_simplifier(body)[source]¶

claripy.simplifications.boolean_and_simplifier(*args)[source]¶

claripy.simplifications.boolean_or_simplifier(*args)[source]¶

claripy.simplifications.bitwise_add_simplifier(*args)[source]¶

claripy.simplifications.bitwise_mul_simplifier(*args)[source]¶

claripy.simplifications.bitwise_sub_simplifier(a, b)[source]¶

claripy.simplifications.bitwise_xor_simplifier_minmax(a, b)[source]¶

claripy.simplifications.bitwise_xor_simplifier(a, b, *args)[source]¶

claripy.simplifications.bitwise_or_simplifier(a, b, *args)[source]¶

claripy.simplifications.bitwise_and_simplifier(a, b, *args)[source]¶

claripy.simplifications.boolean_not_simplifier(body)[source]¶

claripy.simplifications.zeroext_simplifier(n, e)[source]¶

claripy.simplifications.signext_simplifier(n, e)[source]¶

claripy.simplifications.extract_simplifier(high, low, val)[source]¶

claripy.simplifications.fptobv_simplifier(the_fp)[source]¶

claripy.simplifications.fptofp_simplifier(*args)[source]¶

claripy.simplifications.rotate_shift_mask_simplifier(a, b)[source]¶

Handles the following case:

((A << a) | (A >> (_N - a))) & mask, where: A being a BVS, a being a integer that is less than _N, _N is either 32 or 64, and mask can be evaluated to 0xffffffff (64-bit) or 0xffff (32-bit) after reversing the rotate-shift operation.

It will be simplified to:

(A & (mask >>> a)) <<< a

claripy.simplifications.str_reverse_simplifier(arg)[source]¶

claripy.simplifications.invert_simplifier(expr)[source]¶

claripy.simplifications.and_mask_comparing_against_constant_simplifier(op, a, b)[source]¶

This simplifier handles the following case:

A & mask == b, and A & mask != b

If the high bits of A are 0, & mask can be eliminated.

claripy.simplifications.zeroext_extract_comparing_against_constant_simplifier(op, a, b)[source]¶

This simplifier handles the following cases:

Extract(hi, 0, Concat(0, A)) op b, and Extract(hi, 0, ZeroExt(n, A)) op b

Extract can be eliminated if the high bits of Concat(0, A) or ZeroExt(n, A) are all zeros.

claripy.simplifications.zeroext_comparing_against_simplifier(op, a, b)[source]¶

This simplifier handles the following cases:

ZeroExt(n, A) == b, ZeroExt(n, A) != b, and ZeroExt(n, A) >= b

If the high bits of b are all zeros (in case of ==, !=, and >=) or have at leclaripy one ones (in case of !=), ZeroExt can be eliminated.

claripy.simplifications.simplify(op, args)[source]¶

Simplifies the given operation with the given arguments. Returns the simplified result if possible, along with a boolean representing whether annotations were handled by the simplifier.

Return type:: tuple[Base | None, bool]

claripy.debug.set_debug(enabled)[source]¶: Enable or disable the debug mode. In debug mode, a bunch of extra checks in claripy will be executed. You’ll want to disable debug mode if you are running performance critical code.

claripy — Solver Engine¶

AST¶

Backends¶

Frontends¶

Frontend Mixins¶

Annotations¶

VSA¶

Misc. Things¶

`claripy` — Solver Engine¶