Expressions
Abstract syntax tree (AST) expressions
Expressions are the nodes of the AST where input and state variables being the leaf nodes. ILAng provides the interface to define and construct the AST expressions based on the set of operators supported in SMT LIB2. Basic type checks are performed at run time.
Constant
To declare a constant Boolean and bit-vector expression is easy:
Besides key and element bit-width, a constant memory consists of a default value and a set of key-element pairs. The below example creates a constant memory where all elements have value 0xFF
except for key 2
being mapped to 0x4
. The memory address and data are 32
and 8
bit wide, respectively.
Logical operation
Logic operations such as AND, OR, and NOT can be applied to Boolean and bit-vector type expressions (need to have the same type). Note that the operations on bit-vectors are bit-wise.
Arithmetic operation
ILAng also supports arithmetic operations for bit-vector type expressions. Note that arithmetic operations are signed by default.
For bit-vectors, there are also several bit-wise operations available:
Binary comparison
With two expressions of the same type, you can compare logically or arithmetically:
Note that, by default, comparison are singed for bit-vectors. There is always an unsigned correspondent.
Memory operations
To load and store memory values:
If-then-else
To represent conditional expressions, the if-then-else operator takes as inputs one Boolean expression (condition) and two branch expressions of the same type.
Last updated