Previous  Up  Next

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


type integer_ty = private
| Gmp
| C_type of Cil_types.ikind
| Other (*
Any non-integral type
*)
Possible types infered by the system.
val pretty : Format.formatter -> integer_ty -> unit

Smart constructors


val gmp : integer_ty
val c_int : integer_ty
val ikind : Cil_types.ikind -> integer_ty
val other : integer_ty

Useful operations over Typing.integer_ty


exception Not_an_integer
val typ_of_integer_ty : integer_ty -> Cil_types.typ
Raises Not_an_integer in case of Other.
Returns the C type corresponding to an 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.

Typing


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.

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_integer_ty : Cil_types.term -> integer_ty
Returns the infered type for the given term.
val get_integer_op : Cil_types.term -> integer_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 -> integer_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:integer_ty -> integer_ty -> unit
Register that the given term has the given type in the given context (if any). No verification is done.

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.