Module Operator.Function_symbol

Function symbol: Reusable tags that allow a building a term, i.e. a tagged representation of an expressions that composes transfer functions.

type case = int

Some aliases for legibility

The case number of an enum

Phantom type parameters

These types are never instanciated as values. They are used as phantom parameters in GADTs to distinguish terms and function symboles based on the concrete value they represent.

type boolean = private

1. | TypeBoolean

A boolean value, e.g. true or false

type integer = private

1. | TypeInteger

An unbounded integer value, often represented by Z.t in the concrete

type enum = private

1. | TypeEnum

An enum value: can take a fixed number of values depending on the enum type being considered.

type bitvector = private

1. | TypeBitvector

A bitvector of size size We generally do not store the size; instead, most operation have a ~size parameter specifying the number of bits of the underlying operation.

type binary = bitvector

type memory = private

1. | TypeMemory

Arities

type ar0 = private

1. | Ar0

A term of arity 0 is just a constant

type 'a ar1 = private

1. | Ar1

A term of arity 1 is a unary operation (ex: boolean not). The 'a parameter represents the type of the argument.

type ('a, 'b) ar2 = private

1. | Ar2

A term of arity 2 is a binary operation (ex: addition) The 'a parameter represents the type of the arguments.

Types

type 'a typ =

1. | Boolean : boolean typ
2. | Integer : integer typ
3. | Enum : enum typ
4. | Binary : Units.In_bits.t -> binary typ
5. | Memory : memory typ

A GADT regrouping all our phantom type parameters

type any_type =

1. | Any_type : 'a typ -> any_type

Existential wrapper for typ.

Function symbols

The type of function symbols takes two parameters:

• 'arg is the arity, i.e. the type of arguments needed to build this term. The arity should be either ar0, 'a ar1 or ('a, 'b) ar2.

• 'ret it the return type of the function symbol, i.e. the type of the term whose head is this function symbol.

type ('arg, 'ret) function_symbol =

1. | True : (ar0, boolean) function_symbol
2. | False : (ar0, boolean) function_symbol
3. | And : ((boolean, boolean) ar2, boolean) function_symbol
4. | Or : ((boolean, boolean) ar2, boolean) function_symbol
5. | Not : (boolean ar1, boolean) function_symbol
6. | BoolUnion : ((boolean, boolean) ar2, boolean) function_symbol
7. | Biconst : Units.In_bits.t * Z.t -> (ar0, binary) function_symbol
   (*

   Bitvector constant with the given size and value.

   *)
8. | Biadd : {
   1. size : Units.In_bits.t;
   2. flags : Flags.Biadd.t;
   } -> ((binary, binary) ar2, binary) function_symbol
   (*

   Addition on bitvectors of size size. See biadd for the flag meanings.

   *)
9. | Bisub : {
   1. size : Units.In_bits.t;
   2. flags : Flags.Biadd.t;
   } -> ((binary, binary) ar2, binary) function_symbol
   (*

   Bitvector subtraction See biadd for the flag meanings.

   *)
10. | Bimul : {
    1. size : Units.In_bits.t;
    2. flags : Flags.Bimul.t;
    } -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector multiplication, See biadd for the flag meanings.

    *)
11. | Biudiv : Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector unsigned division.

    *)
12. | Bisdiv : Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector signed division. This is truncated (C99-like) integer division.

    *)
13. | Biumod : Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector unsigned modulo.

    *)
14. | Bismod : Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector signed modulo.

    *)
15. | Bshl : {
    1. size : Units.In_bits.t;
    2. flags : Flags.Bshl.t;
    } -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector left-shift

    *)
16. | Bashr : Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector arithmetic right shift (pad with top-bit)

    *)
17. | Blshr : Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector logical right shift (pad with zeros)

    *)
18. | Band : Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector bitwise and

    *)
19. | Bor : Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector bitwise or

    *)
20. | Bxor : Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector bitwise xor

    *)
21. | Beq : Units.In_bits.t -> ((binary, binary) ar2, boolean) function_symbol
    (*

    Bitvector equality

    *)
22. | Bisle : Units.In_bits.t -> ((binary, binary) ar2, boolean) function_symbol
    (*

    Signed comparison between two bitvectors (using less-or-equal <=). Bitvectors are interpreted as integers in [-2^{size-1}..-2^{size-1}-1] using two's complement.

    *)
23. | Biule : Units.In_bits.t -> ((binary, binary) ar2, boolean) function_symbol
    (*

    Unsigned comparison between two bitvectors (using less-or-equal <=). Bitvectors are interpreted as positive integers in [0..-2^{size}-1].

    *)
24. | Bconcat : Units.In_bits.t * Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
    (*

    Bitvector concatenation: the new bitvector's size is the sum of the sizes of the arguments. The first argument becomes the most significant bits.

    *)
25. | Bextract : {
    1. size : Units.In_bits.t;
    2. index : Units.In_bits.t;
    3. oldsize : Units.In_bits.t;
    } -> (binary ar1, binary) function_symbol
    (*

    Extract a size of a bitvector of total size oldsize, starting at index. Should satisfy index + size <= oldsize.

    *)
26. | Bsext : Units.In_bits.t -> (binary ar1, binary) function_symbol
    (*

    Sign-extend (pad left with topbit) the argument bitvector until it reaches the specified size.

    *)
27. | Buext : Units.In_bits.t -> (binary ar1, binary) function_symbol
    (*

    Unsngned-extend (pad left with zero) the argument bitvector until it reaches the specified size.

    *)
28. | Bofbool : Units.In_bits.t -> (boolean ar1, binary) function_symbol
    (*

    Turn a boolean into a bitvector: false is 0 and true is 1.

    *)
29. | Bunion : int * Units.In_bits.t -> ((binary, binary) ar2, binary) function_symbol
30. | Bchoose : int * Units.In_bits.t -> (binary ar1, binary) function_symbol
31. | Iconst : Z.t -> (ar0, integer) function_symbol
    (*

    Integer constant

    *)
32. | Iadd : ((integer, integer) ar2, integer) function_symbol
33. | Isub : ((integer, integer) ar2, integer) function_symbol
34. | Imul : ((integer, integer) ar2, integer) function_symbol
35. | Idiv : ((integer, integer) ar2, integer) function_symbol
    (*

    This is truncated (C99-like) integer division

    *)
36. | Imod : ((integer, integer) ar2, integer) function_symbol
37. | Ishl : ((integer, integer) ar2, integer) function_symbol
38. | Ishr : ((integer, integer) ar2, integer) function_symbol
39. | Ior : ((integer, integer) ar2, integer) function_symbol
    (*

    Bitwise or, where negative integers are seen as prefixed by infinite ones

    *)
40. | Ixor : ((integer, integer) ar2, integer) function_symbol
41. | Iand : ((integer, integer) ar2, integer) function_symbol
    (*

    Bitwise and, where negative integers are seen as prefixed by infinite ones

    *)
42. | Ieq : ((integer, integer) ar2, boolean) function_symbol
43. | Ile : ((integer, integer) ar2, boolean) function_symbol
44. | Itimes : Z.t -> (integer ar1, integer) function_symbol
    (*

    Multiply an integer by a constant

    *)
45. | EnumConst : case -> (ar0, enum) function_symbol
    (*

    An enum case with the given value

    *)
46. | CaseOf : case -> (enum ar1, boolean) function_symbol
    (*

    true if the argument matches the given case, false otherwise.

    *)

module Build : sig ... end

Builder for these terms. Note that we do not perform any hash-consing here.

val type_of : ('a, 'b) function_symbol -> 'b typ

val hash : ('a, 'b) function_symbol -> int

val equal : ('a, 'b) function_symbol -> ('c, 'd) function_symbol -> bool

module type PRETTY_ARG = sig ... end

Helper to build pretty-printers. We can pretty print a term if we have access to the tag (representing the operation) and we know how to pretty-print the arguments.

module type PRETTY_RESULT = sig ... end

module Pretty (M : PRETTY_ARG) : PRETTY_RESULT with type 'a t = 'a M.t and type 'a pack = 'a M.pack