Module Operator.Function_symbolSource

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

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

Sourcetype boolean = private
  1. | TypeBoolean

A boolean value, e.g. true or false

Sourcetype integer = private
  1. | TypeInteger

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

Sourcetype enum = private
  1. | TypeEnum

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

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

Sourcetype binary = bitvector
Sourcetype memory = private
  1. | TypeMemory

Arities

Sourcetype ar0 = private
  1. | Ar0

A term of arity 0 is just a constant

Sourcetype '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.

Sourcetype ('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

Sourcetype '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

Sourcetype any_type =
  1. | Any_type : 'a typ -> any_type

Existential wrapper for typ.

Function symbols

The type of function symbols takes two parameters:

Sourcetype ('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.

    *)
Sourcemodule Build : sig ... end

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

Sourceval type_of : ('a, 'b) function_symbol -> 'b typ
Sourceval hash : ('a, 'b) function_symbol -> int
Sourceval equal : ('a, 'b) function_symbol -> ('c, 'd) function_symbol -> bool
Sourcemodule 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.

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