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

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
val number_ty_of_typ : post:bool -> Cil_types.typ -> number_ty

Reverse of typ_of_number_ty number_ty_of_typ ~post ty return the Typing.number_ty corresponding to a C type. post indicates if the type is before or after the typing phase. The GMP types will be recognized only in a post-typing phase.

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.

If must_clear is true, the typing environment is reset before translating the predicate. The environment should be reset when translating a new assertion, and kept otherwise.

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
val get_integer_op : Cil_types.term -> number_ty
val get_integer_op_of_predicate : Cil_types.predicate -> number_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: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

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.