List of Claripy Operations

Last updated 9 months ago

Arithmetic and Logic
Name
Description
Example
LShR
Logically shifts an expression to the right. (the default shifts are arithmetic)
x.LShR(10)
RotateLeft
Rotates an expression left
x.RotateLeft(8)
RotateRight
Rotates an expression right
x.RotateRight(8)
And
Logical And (on boolean expressions)
solver.And(x == y, x > 0)
Or
Logical Or (on boolean expressions)
solver.Or(x == y, y < 10)
Not
Logical Not (on a boolean expression)
solver.Not(x == y) is the same as x != y
If
An If-then-else
Choose the maximum of two expressions: solver.If(x > y, x, y)
ULE
Unsigned less than or equal to
Check if x is less than or equal to y: x.ULE(y)
ULT
Unsigned less than
Check if x is less than y: x.ULT(y)
UGE
Unsigned greater than or equal to
Check if x is greater than or equal to y: x.UGE(y)
UGT
Unsigned greater than
Check if x is greater than y: x.UGT(y)
SLE
Signed less than or equal to
Check if x is less than or equal to y: x.SLE(y)
SLT
Signed less than
Check if x is less than y: x.SLT(y)
SGE
Signed greater than or equal to
Check if x is greater than or equal to y: x.SGE(y)
SGT
Signed greater than
Check if x is greater than y: x.SGT(y)
TODO: Add the floating point ops
Bitvector Manipulation
Name
Description
Example
SignExt
Pad a bitvector on the left with n sign bits
x.sign_extend(n)
ZeroExt
Pad a bitvector on the left with n zero bits
x.zero_extend(n)
Extract
Extracts the given bits (zero-indexed from the right, inclusive) from an expression.
Extract the least significant byte of x: x[7:0]
Concat
Concatenates any number of expressions together into a new expression.
x.concat(y, ...)
Extra Functionality
There's a bunch of prepackaged behavior that you could implement by analyzing the ASTs and composing sets of operations, but here's an easier way to do it:
You can chop a bitvector into a list of chunks of n bits with val.chop(n)
You can endian-reverse a bitvector with x.reversed
You can get the width of a bitvector in bits with val.length
You can test if an AST has any symbolic components with val.symbolic
You can get a set of the names of all the symbolic variables implicated in the construction of an AST with val.variables

Appendix

List of State Options

Name	Description	Example
LShR	Logically shifts an expression to the right. (the default shifts are arithmetic)	`x.LShR(10)`
RotateLeft	Rotates an expression left	`x.RotateLeft(8)`
RotateRight	Rotates an expression right	`x.RotateRight(8)`
And	Logical And (on boolean expressions)	`solver.And(x == y, x > 0)`
Or	Logical Or (on boolean expressions)	`solver.Or(x == y, y < 10)`
Not	Logical Not (on a boolean expression)	`solver.Not(x == y)` is the same as `x != y`
If	An If-then-else	Choose the maximum of two expressions: `solver.If(x > y, x, y)`
ULE	Unsigned less than or equal to	Check if x is less than or equal to y: `x.ULE(y)`
ULT	Unsigned less than	Check if x is less than y: `x.ULT(y)`
UGE	Unsigned greater than or equal to	Check if x is greater than or equal to y: `x.UGE(y)`
UGT	Unsigned greater than	Check if x is greater than y: `x.UGT(y)`
SLE	Signed less than or equal to	Check if x is less than or equal to y: `x.SLE(y)`
SLT	Signed less than	Check if x is less than y: `x.SLT(y)`
SGE	Signed greater than or equal to	Check if x is greater than or equal to y: `x.SGE(y)`
SGT	Signed greater than	Check if x is greater than y: `x.SGT(y)`