Module Typing

module Typing: sig .. end

Type system which computes the smallest C type that may contain all the possible values of a given integer term or predicate. Also compute the required casts. It is based on interval inference of module Interval.

It implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour devenir plus rapide, plus précis et plus mince".

Example: consider a variable x of type int and a variable y of type char on a (strange) architecture in which values of type int belongs to the interval [-128;127] and values of type char belongs to the interval [-32;31], while there are no other integral types. Then here are some information computed from the term 1+(x+1)/(y-64) by the type system: 1. x+1 must be a GMP (because of the potential overflow) 2. consequently x, which is an int, must be coerced into a GMP and the same for the number 1 in this addition. 3. y-64 can be computed in an int (because the result belongs to the interval [-96;-33]). 4. (x+1)/(y-64) must be a GMP operation because the numerator is a GMP (see 1.). Consequently y-64 must be coerced into a GMP too. However, the result belongs to the interval [-3;3] and thus can be safely coerced to an int. 5. Consequently the addition of the toplevel term 1+(x+1)/(y-64) can safely be computed in int: its result belongs to [-2;4].


Datatypes

type integer_ty = private 
| Gmp
| C_type of Cil_types.ikind
| Other (*

Any non-integral type

*)

Possible types inferred by the system.

module Datatype: Datatype.S_with_collections  with type t = integer_ty

Smart constructors

val gmp : integer_ty
val c_int : integer_ty
val ikind : Cil_types.ikind -> integer_ty
val other : integer_ty

Useful operations over Typing.integer_ty

exception Not_an_integer
val typ_of_integer_ty : integer_ty -> Cil_types.typ
val integer_ty_of_typ : Cil_types.typ -> integer_ty

Reverse of typ_of_integer_ty

val ty_of_logic_ty : Cil_types.logic_type -> integer_ty
val join : integer_ty -> integer_ty -> integer_ty

Typing.integer_ty is a join-semi-lattice if you do not consider Other. If there is no Other in argument, this function computes the join of this semi-lattice. If one of the argument is Other, the function assumes that the other argument is also Other. In this case, the result is Other.

Typing

val type_term : use_gmp_opt:bool -> ?ctx:integer_ty -> Cil_types.term -> unit

Compute the type of each subterm of the given term in the given context. If use_gmp_opt is false, then the conversion to the given context is done even if -e-acsl-gmp-only is set.

val type_named_predicate : ?must_clear:bool -> Cil_types.predicate -> unit

Compute the type of each term of the given predicate. Set must_clear to false in order to not reset the environment.

val clear : unit -> unit

Remove all the previously computed types.

Getters

Below, the functions assume that either Typing.type_term or Typing.type_named_predicate has been previously computed for the given term or predicate.

val get_integer_ty : Cil_types.term -> integer_ty
val get_integer_op : Cil_types.term -> integer_ty
val get_integer_op_of_predicate : Cil_types.predicate -> integer_ty
val get_typ : Cil_types.term -> Cil_types.typ

Get the type which the given term must be generated to.

val get_op : Cil_types.term -> Cil_types.typ

Get the type which the operation on top of the given term must be generated to.

val get_cast : Cil_types.term -> Cil_types.typ option

Get the type which the given term must be converted to (if any).

val get_cast_of_predicate : Cil_types.predicate -> Cil_types.typ option

Like Typing.get_cast, but for predicates.

val unsafe_set : Cil_types.term -> ?ctx:integer_ty -> integer_ty -> unit

Register that the given term has the given type in the given context (if any). No verification is done.

Typing/types-related utils

val ty_of_interv : ?ctx:integer_ty -> Ival.t -> integer_ty
val typ_of_lty : Cil_types.logic_type -> Cil_types.typ

Internal stuff

val compute_quantif_guards_ref : (Cil_types.predicate ->
Cil_types.logic_var list ->
Cil_types.predicate ->
(Cil_types.term * Cil_types.relation * Cil_types.logic_var *
Cil_types.relation * Cil_types.term)
list)
Stdlib.ref

Forward reference.