Operator.SigSourceThis defines the syntax for the operators usable in the internal languages of Codex, expressed as signatures as in the Tagless final approach.
The signatures are grouped by type of values manipulated (boolean, integer, bitvector, binary, memory, enum). We define two set of functions: the forward are the normal operations, and the backward exclude the functions of arity 0 (for which a backward operation is meaningless).
Arity of function symbols. 'r represents the result type and 'a, 'b, 'c the arguments.
Standard arities for forward transfer functions: given the arguments, return the results. These match the arities of the concrete functions they represent (but with concrete types substituted for their abstract counterparts).
Standard arities for backward transfer functions (used to refined the arguments from information on the result values). These take the result value 'r as argument and return a new-improved value for each argument. They return None when no improvement is possible for that argument.
Note: in the following, we distinguish between backward and forward because there is no need to implement backward transfer functions for symbols with arity 0.
Transfer functions for boolean values: not, and (&&), or (||), as well as contants true_ and false_.
Transfer functions for unbounded integers:
iadd); subtraction (isub);imul, in general, itimes when multiplying by a constant);idiv), remainder (imod);ieq for ==, ile for <=);ishl and right ishr)ior, iand, ixor).For the bitwise operation, we assume an infinite two-complement representation: i.e. -1 is represented by an infinite sequence of 1, and 0 by an infinite sequence of 0.
Purely numerical operations on fixed-size bitvectors. Includes bitwise operations and arithmetic, but not pointer arithmetic.
Note: the size argument is generally the size of both arguments and the result.
Binary is the name of values handled by C or machine-level programs, i.e. either numeric bitvectors or pointers.
Transfer function for enum values. Enums are types with a fixed (small) number of possible cases.