Module Operator.Sig

This 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).

type access_type =

1. | Read
   (*

   Loading from memory.

   *)
2. | Write
   (*

   Storing into memory.

   *)

type arith_type =

1. | Plus
   (*

   Addition operation

   *)
2. | Minus
   (*

   Substraction operation

   *)

module type ARITY = sig ... end

Arity of function symbols. 'r represents the result type and 'a, 'b, 'c the arguments.

module Forward_Arity : sig ... end

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).

module Backward_Arity : sig ... end

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.

Boolean transfer functions

Transfer functions for boolean values: not, and (&&), or (||), as well as contants true_ and false_.

module type BOOLEAN_BACKWARD = sig ... end

module type BOOLEAN_FORWARD = sig ... end

Integer transfer functions

Transfer functions for unbounded integers:

• addition (iadd); subtraction (isub);
• multiplication (imul, in general, itimes when multiplying by a constant);
• division (idiv), remainder (imod);
• comparisons (ieq for ==, ile for <=);
• shifts (left ishl and right ishr)
• bitwise operations (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.

module type INTEGER_BACKWARD = sig ... end

module type INTEGER_FORWARD_MIN = sig ... end

module type INTEGER_FORWARD = sig ... end

Bitvector transfer functions

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.

module type BITVECTOR_BACKWARD = sig ... end

module type BITVECTOR_FORWARD = sig ... end

module type BITVECTOR_FORWARD_WITH_BIMUL_ADD = sig ... end

Binary transfer functions

Binary is the name of values handled by C or machine-level programs, i.e. either numeric bitvectors or pointers.

module type BINARY_BACKWARD = sig ... end

module type BINARY_FORWARD = sig ... end

module type OFFSET_BACKWARD = sig ... end

module type OFFSET_FORWARD = sig ... end

module type BLOCK_BACKWARD = sig ... end

module type BLOCK_FORWARD = sig ... end

Enum transfer functions

Transfer function for enum values. Enums are types with a fixed (small) number of possible cases.

module type ENUM_BACKWARD = sig ... end

module type ENUM_FORWARD = sig ... end

Memory transfer functions

module type MEMORY_BACKWARD = sig ... end

module type MEMORY_FORWARD = sig ... end