List of Claripy Operations#

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