Module Types.TypedC

TypedC: Grammar for describing the types for the type-based domain, and operations on concrete types.

type value_symbol = string
type value =
  1. | Sym of value_symbol
type array_length =
  1. | Fixed_length of Z.t
  2. | Variable_length of value_symbol
val pp_value : Stdlib.Format.formatter -> value -> unit
val pp_array_length : Stdlib.Format.formatter -> array_length -> unit
module Pred : sig ... end
type basic = Units.In_bytes.t * string
type structure = {
  1. st_byte_size : Units.In_bytes.t;
  2. st_members : (Units.In_bytes.t * string * typ) list;
}
and union = {
  1. un_byte_size : Units.In_bytes.t option;
  2. un_types : (string * typ) list;
}
and descr =
  1. | Void
  2. | Base of basic
    (*

    Base types. Note that even if they have a name, they are not a definition (e.g., you cannot have pointers to byte.

    *)
  3. | Structure of structure
  4. | StructureFAM of {
    1. structure : typ;
    2. array : typ;
    }
    (*

    Structure with flexible array member, decomposed as fix prefix * array.

    *)
  5. | Ptr of pointer
    (*

    Todo: we should always have a size (possibly an existentially-qualified variable).

    *)
  6. | Array of typ * array_length
    (*

    Arguments: element type, and the number of elements, if statically known.

    *)
  7. | Function of funtyp
  8. | Application of name
  9. | Existential of typ * string * typ
  10. | Union of union
  11. | Weak of typ
and pointer = {
  1. pointed : typ;
}
and name = {
  1. constr : constr;
  2. args : Pred.expr list;
}
and constr_name =
  1. | ConstrName of string
  2. | ConstrNameFunc of string
  3. | ConstrNameUnion of string
  4. | ConstrNameStruct of string
  5. | ConstrNameEnum of string
  6. | ConstrNameArray of constr_name

Called type name in OOPSLA, but is the name of a family of region names when there are arguments.

and constr = private {
  1. id : int;
  2. name : constr_name;
  3. arity : int;
}

Each constr_name is associated to a unique id and arity to give a constr.

and funtyp = {
  1. ret : typ;
  2. args : typ list;
  3. pure : bool;
}
and typ = {
  1. mutable descr : descr;
  2. mutable pred : Pred.t;
}
type fundef = {
  1. funtyp : typ;
  2. inline : bool;
}
val pp : Stdlib.Format.formatter -> typ -> unit
val pp_constr : Stdlib.Format.formatter -> constr -> unit
val compare : typ -> typ -> int
val equal : typ -> typ -> bool
val equiv : typ -> typ -> bool

equiv a b returns true if it can show that a is a subtype of b and b is a subtype a.

module Constr : sig ... end
module Build : sig ... end
val is_flexible_array : typ -> bool
val is_function_pure : typ -> bool
val contains : typ -> typ -> bool

contains t u determines whether t contains u. (Definition: t contains u iff t = u or a component of t (e.g. a structure member) contains u.

exception Unsizeable_type
val sizeof : typ -> Units.In_bytes.t

Returns the size of the type (in bytes), if possible

exception Undefined_type_constructor of string

These functions allow to update or query the binding from type names to types.

val get_type_definitions : unit -> string list
val inlined : typ -> typ

Unroll the definitions of a type (i.e. replace a name with the corresponding type)

val substitute_in_type : typ -> (value_symbol * Pred.expr) list -> typ

Substitutes the symbolic variables in the type typ by the corresponding expressions in bindings

val substitute_symbol : typ -> string -> string -> typ
val word : byte_size:Units.In_bytes.t -> typ
val tuple : typ list -> typ

Additionnal functions used for type domains

type constr_def = typ * string list
val add_constr_definition : constr -> constr_def -> unit

Maps a name to a type constructor.

val constr_of_name : constr -> constr_def option

find the constr_def associated to a constr, or None if none.

val print_constr_map : Stdlib.Format.formatter -> unit -> unit

print the constructor map, for debug purposes.

val print_spec : Stdlib.Format.formatter -> unit -> unit

print all the stored maps, for debug purposes

val add_function_name_definition : string -> typ -> bool -> unit
val function_of_name : string -> typ option

Retrieve the type associated to a function name, or None if there is none.

val function_definition_of_name : string -> fundef option

Retrieve the type associated to a function name, and whether it was declared inline; or None if not found.

val print_function_map : Stdlib.Format.formatter -> unit -> unit

print the function map, for debug purposes.

val get_function_names : unit -> string list
val add_global_name_definition : string -> typ -> unit
val global_of_name : string -> typ option

Retrieve the type associated to a function name, or None if not found.

val print_global_map : Stdlib.Format.formatter -> unit -> unit

print the function map, for debug purposes.