package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Operator.SigSource

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

Sourcetype access_type =
  1. | Read
    (*

    Loading from memory.

    *)
  2. | Write
    (*

    Storing into memory.

    *)
Sourcetype arith_type =
  1. | Plus
    (*

    Addition operation

    *)
  2. | Minus
    (*

    Substraction operation

    *)
Sourcemodule type ARITY = sig ... end

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

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

Sourcemodule 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_.

Sourcemodule type BOOLEAN_BACKWARD = sig ... end
Sourcemodule 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.

Sourcemodule type INTEGER_BACKWARD = sig ... end
Sourcemodule type INTEGER_FORWARD_MIN = sig ... end
Sourcemodule 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.

Sourcemodule type BITVECTOR_BACKWARD = sig ... end
Sourcemodule type BITVECTOR_FORWARD = sig ... end
Sourcemodule 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.

Sourcemodule type BINARY_BACKWARD = sig ... end
Sourcemodule type BINARY_FORWARD = sig ... end
Sourcemodule type OFFSET_BACKWARD = sig ... end
Sourcemodule type OFFSET_FORWARD = sig ... end
Sourcemodule type BLOCK_BACKWARD = sig ... end
Sourcemodule type BLOCK_FORWARD = sig ... end

Enum transfer functions

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

Sourcemodule type ENUM_BACKWARD = sig ... end
Sourcemodule type ENUM_FORWARD = sig ... end

Memory transfer functions

Sourcemodule type MEMORY_BACKWARD = sig ... end
Sourcemodule type MEMORY_FORWARD = sig ... end