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]
.
type
integer_ty = private
| |
Gmp |
|||
| |
C_type of |
|||
| |
Other |
(* | Any non-integral type | *) |
Possible types infered by the system.
val pretty : Format.formatter -> integer_ty -> unit
val gmp : integer_ty
val c_int : integer_ty
val ikind : Cil_types.ikind -> integer_ty
val other : integer_ty
Typing.integer_ty
exception Not_an_integer
val typ_of_integer_ty : integer_ty -> Cil_types.typ
Not_an_integer
in case of Other
.Typing.integer_ty
. That is Gmpz.t ()
for Gmp
and TInt(ik, [[]])
for Ctype ik
.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
.
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.
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.
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.