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
number_ty = private
| |
C_integer of |
| |
C_float of |
| |
Gmpz |
| |
Rational |
| |
Real |
| |
Nan |
module Function_params_ty:Datatype.S_with_collections
with 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_ty
Typing.number_ty
exception Not_a_number
val typ_of_number_ty : number_ty -> Cil_types.typ
Not_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_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
.
val type_term : use_gmp_opt:bool ->
?ctx:number_ty ->
lenv:Function_params_ty.t -> 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 : lenv:Function_params_ty.t -> Cil_types.predicate -> unit
Compute the type of each term of the given predicate.
val clear : unit -> unit
Remove 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_ty
val get_integer_op : lenv:Function_params_ty.t -> Cil_types.term -> number_ty
val get_integer_op_of_predicate : lenv:Function_params_ty.t -> Cil_types.predicate -> number_ty
val get_typ : lenv:Function_params_ty.t -> Cil_types.term -> Cil_types.typ
Get the type which the given term must be generated to.
val get_op : lenv:Function_params_ty.t -> 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 : lenv:Function_params_ty.t -> 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 : lenv:Function_params_ty.t ->
Cil_types.predicate -> Cil_types.typ option
Like Typing.get_cast
, but for predicates.
val unsafe_set : Cil_types.term ->
?ctx:number_ty ->
lenv:Function_params_ty.t -> number_ty -> unit
Register that the given term has the given type in the given context (if any). No verification is done.
val ty_of_interv : ?ctx:number_ty -> ?use_gmp_opt:bool -> Interval.t -> number_ty
val typ_of_lty : Cil_types.logic_type -> Cil_types.typ
val type_program : Cil_types.file -> unit
compute 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 -> unit
compute and store the types of all the terms in a given predicate
val preprocess_rte : lenv:Function_params_ty.t -> Cil_types.code_annotation -> unit
compute and store the type of all the terms in a code annotation