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

Datatype and constructor



Datatypes



Possible types infered by the system.
type number_ty = private 
| C_integer of Cil_types.ikind
| C_float of Cil_types.fkind
| Gmpz
| Rational
| Real
| Nan
module Datatype: Datatype.S_with_collections  with type t = number_ty

Smart constructors


val c_int : number_ty
val ikind : Cil_types.ikind -> number_ty
val fkind : Cil_types.fkind -> number_ty
val gmpz : number_ty
val rational : number_ty
val nan : number_ty

Useful operations over Typing.number_ty


exception Not_a_number
val typ_of_number_ty : number_ty -> Cil_types.typ
Raises Not_a_number in case of Nan.
Returns the C type corresponding to an Typing.number_ty. That is Gmp.z_t () for Gmpz, Real.t () for Real and TInt(ik, [[]]) for Ctype ik.
val number_ty_of_typ : Cil_types.typ -> number_ty
Reverse of typ_of_number_ty
val join : number_ty -> number_ty -> number_ty
Typing.number_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:number_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_number_ty : Cil_types.term -> number_ty
Returns the infered type for the given term.
val get_integer_op : Cil_types.term -> number_ty
Returns the infered type for the top operation of the given term. It is meaningless to call this function over a non-arithmetical/logical operator.
val get_integer_op_of_predicate : Cil_types.predicate -> number_ty
Returns the infered type for the top operation of the given predicate.
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:number_ty -> number_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:number_ty -> Interval.t -> number_ty

Coercion rules


val typ_of_lty : Cil_types.logic_type -> Cil_types.typ
Returns the C type that correponds to the given logic type.

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)
Pervasives.ref
Forward reference.