Name | Description | Example |
LShR | Logically shifts an expression to the right. (the default shifts are arithmetic) |
|
RotateLeft | Rotates an expression left |
|
RotateRight | Rotates an expression right |
|
And | Logical And (on boolean expressions) |
|
Or | Logical Or (on boolean expressions) |
|
Not | Logical Not (on a boolean expression) |
|
If | An If-then-else | Choose the maximum of two expressions: |
ULE | Unsigned less than or equal to | Check if x is less than or equal to y: |
ULT | Unsigned less than | Check if x is less than y: |
UGE | Unsigned greater than or equal to | Check if x is greater than or equal to y: |
UGT | Unsigned greater than | Check if x is greater than y: |
SLE | Signed less than or equal to | Check if x is less than or equal to y: |
SLT | Signed less than | Check if x is less than y: |
SGE | Signed greater than or equal to | Check if x is greater than or equal to y: |
SGT | Signed greater than | Check if x is greater than y: |
TODO: Add the floating point ops
Name | Description | Example |
SignExt | Pad a bitvector on the left with |
|
ZeroExt | Pad a bitvector on the left with |
|
Extract | Extracts the given bits (zero-indexed from the right, inclusive) from an expression. | Extract the least significant byte of x: |
Concat | Concatenates any number of expressions together into a new expression. |
|
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