typing.mli 7.06 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
Patrick Baudin's avatar
Patrick Baudin committed
3
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
4
(*                                                                        *)
5
(*  Copyright (C) 2012-2019                                               *)
Virgile Prevosto's avatar
Virgile Prevosto committed
6
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
7
8
9
10
11
12
13
14
15
16
17
18
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
Virgile Prevosto's avatar
Virgile Prevosto committed
19
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
20
21
22
(*                                                                        *)
(**************************************************************************)

Julien Signoles's avatar
Julien Signoles committed
23
(** Type system which computes the smallest C type that may contain all the
24
    possible values of a given integer term or predicate. Also compute the
25
26
27
    required casts. It is based on interval inference of module {!Interval}.

    It implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour
28
    devenir plus rapide, plus précis et plus mince".
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

    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]]. *)
46

47
48
49
open Cil_types

(******************************************************************************)
50
(** {2 Datatypes} *)
51
52
(******************************************************************************)

53
54
55
(** Possible types infered by the system. *)

type number_ty = private
56
57
  | C_integer of ikind
  | C_float of fkind
58
  | Gmpz
59
  | Rational
60
  | Real
61
  | Nan
Julien Signoles's avatar
Julien Signoles committed
62

63
module Datatype: Datatype.S_with_collections with type t = number_ty
64

Julien Signoles's avatar
Julien Signoles committed
65
(** {3 Smart constructors} *)
66

67
68
val c_int: number_ty
val ikind: ikind -> number_ty
69
val fkind: fkind -> number_ty
70
val gmpz: number_ty
71
val rational: number_ty
72
val nan: number_ty
73

74
(** {3 Useful operations over {!number_ty}} *)
Julien Signoles's avatar
Julien Signoles committed
75

76
77
78
exception Not_a_number
val typ_of_number_ty: number_ty -> typ
(** @return the C type corresponding to an {!number_ty}. That is [Gmp.z_t ()]
79
    for [Gmpz], [Real.t ()] for [Real] and [TInt(ik, [[]])] for [Ctype ik].
80
    @raise Not_a_number in case of [Nan]. *)
81

82
83
val number_ty_of_typ: typ -> number_ty
(** Reverse of [typ_of_number_ty] *)
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
84

85
86
val join: number_ty -> number_ty -> number_ty
(** {!number_ty} is a join-semi-lattice if you do not consider [Other]. If
87
88
    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
Julien Signoles's avatar
Julien Signoles committed
89
    the other argument is also {!Other}. In this case, the result is [Other]. *)
90
91
92
93
94

(******************************************************************************)
(** {2 Typing} *)
(******************************************************************************)

95
val type_term: use_gmp_opt:bool -> ?ctx:number_ty -> term -> unit
96
(** Compute the type of each subterm of the given term in the given context. If
97
98
    [use_gmp_opt] is false, then the conversion to the given context is done
    even if -e-acsl-gmp-only is set. *)
99

100
val type_named_predicate: ?must_clear:bool -> predicate -> unit
Julien Signoles's avatar
Julien Signoles committed
101
102
103
104
105
106
107
108
109
110
111
(** 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. *)

(** {3 Getters}

    Below, the functions assume that either {!type_term} or
    {!type_named_predicate} has been previously computed for the given term or
    predicate. *)
112

113
114
val get_number_ty: term -> number_ty
(** @return the infered type for the given term. *)
Julien Signoles's avatar
Julien Signoles committed
115

116
117
val get_integer_op: term -> number_ty
(** @return the infered type for the top operation of the given term.
Julien Signoles's avatar
Julien Signoles committed
118
119
120
    It is meaningless to call this function over a non-arithmetical/logical
    operator. *)

121
122
val get_integer_op_of_predicate: predicate -> number_ty
(** @return the infered type for the top operation of the given predicate. *)
123
124

val get_typ: term -> typ
Julien Signoles's avatar
Julien Signoles committed
125
(** Get the type which the given term must be generated to. *)
126

127
val get_op: term -> typ
Julien Signoles's avatar
Julien Signoles committed
128
129
(** Get the type which the operation on top of the given term must be generated
    to. *)
130

131
val get_cast: term -> typ option
Julien Signoles's avatar
Julien Signoles committed
132
(** Get the type which the given term must be converted to (if any). *)
133

134
val get_cast_of_predicate: predicate -> typ option
Julien Signoles's avatar
Julien Signoles committed
135
(** Like {!get_cast}, but for predicates. *)
136

137
val unsafe_set: term -> ?ctx:number_ty -> number_ty -> unit
138
139
140
(** Register that the given term has the given type in the given context (if
    any). No verification is done. *)

141
(*****************************************************************************)
142
(** {2 Typing/types-related utils} *)
143
144
(*****************************************************************************)

145
val ty_of_interv: ?ctx:number_ty -> Interval.t -> number_ty
146
147
(* Compute the smallest type (bigger than [int]) which can contain the whole
   interval. It is the \theta operator of the JFLA's paper. *)
148

149
150
151
val typ_of_lty: logic_type -> typ
(** @return the C type that correponds to the given logic type. *)

152
153
154
155
156
(******************************************************************************)
(** {2 Internal stuff} *)
(******************************************************************************)

val compute_quantif_guards_ref
Julien Signoles's avatar
Julien Signoles committed
157
158
  : (predicate -> logic_var list -> predicate ->
     (term * relation * logic_var * relation * term) list) ref
159
160
161
162
(** Forward reference. *)

(*
Local Variables:
163
compile-command: "make -C ../../../../.."
164
165
End:
*)