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].
Possible types infered by the system.
type
| |
C_integer of |
| |
C_float of |
| |
Gmpz |
| |
Rational |
| |
Real |
| |
Nan |
module Function_params_ty:Datatype.S_with_collectionswith type t = number_ty list
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_tyTyping.number_tyexception Not_a_number
val typ_of_number_ty : number_ty -> Cil_types.typNot_a_number in case of Nan.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 : post:bool -> Cil_types.typ -> number_tyReverse 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_tyTyping.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.
val type_term : use_gmp_opt:bool ->
?ctx:number_ty ->
lenv:Function_params_ty.t -> Cil_types.term -> unitCompute 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 : lenv:Function_params_ty.t -> Cil_types.predicate -> unitCompute the type of each term of the given predicate.
val clear : unit -> unitRemove all the previously computed types.
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 : lenv:Function_params_ty.t -> Cil_types.term -> number_tyval get_integer_op : lenv:Function_params_ty.t -> Cil_types.term -> number_tyval get_integer_op_of_predicate : lenv:Function_params_ty.t -> Cil_types.predicate -> number_tyval get_typ : lenv:Function_params_ty.t -> Cil_types.term -> Cil_types.typGet the type which the given term must be generated to.
val get_op : lenv:Function_params_ty.t -> Cil_types.term -> Cil_types.typGet the type which the operation on top of the given term must be generated to.
val get_cast : lenv:Function_params_ty.t -> Cil_types.term -> Cil_types.typ optionGet the type which the given term must be converted to (if any).
val get_cast_of_predicate : lenv:Function_params_ty.t ->
Cil_types.predicate -> Cil_types.typ optionLike Typing.get_cast, but for predicates.
val unsafe_set : Cil_types.term ->
?ctx:number_ty ->
lenv:Function_params_ty.t -> number_ty -> unitRegister that the given term has the given type in the given context (if any). No verification is done.
val typ_of_lty : Cil_types.logic_type -> Cil_types.typval type_program : Cil_types.file -> unitcompute and store the type of all the terms that will be translated in a program
val preprocess_predicate : Function_params_ty.t -> Cil_types.predicate -> unitcompute and store the types of all the terms in a given predicate
val preprocess_rte : lenv:Function_params_ty.t -> Cil_types.code_annotation -> unitcompute and store the type of all the terms in a code annotation