typing.ml 26.7 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
23
24
25
(*                                                                        *)
(**************************************************************************)

open Cil_types

(* Implement Figure 4 of J. Signoles' JFLA'15 paper "Rester statique pour
26
   devenir plus rapide, plus précis et plus mince". *)
27
28
29
30

let dkey = Options.dkey_typing

let compute_quantif_guards_ref
Julien Signoles's avatar
Julien Signoles committed
31
32
33
  : (predicate -> logic_var list -> predicate ->
     (term * relation * logic_var * relation * term) list) ref
  = Extlib.mk_fun "compute_quantif_guards_ref"
34
35

(******************************************************************************)
36
(** Datatype and constructor *)
37
38
(******************************************************************************)

39
type number_ty =
40
41
  | C_integer of ikind
  | C_float of fkind
42
  | Gmpz
43
  | Rational
44
  | Real
45
  | Nan
46

47
48
let ikind ik = C_integer ik
let c_int = ikind IInt
49
let gmpz = Gmpz
50
51
let fkind fk = C_float fk
let rational = Rational
52
let nan = Nan
53

54
55
56
module D =
  Datatype.Make_with_collections
    (struct
57
      type t = number_ty
58
      let name = "E_ACSL.Typing.t"
59
      let reprs = [ Gmpz; Real; Nan; c_int ]
60
61
      include Datatype.Undefined

Julien Signoles's avatar
Julien Signoles committed
62
63
64
65
      let compare ty1 ty2 =
        if ty1 == ty2 then 0
        else
          match ty1, ty2 with
66
          | C_integer i1, C_integer i2 ->
Julien Signoles's avatar
Julien Signoles committed
67
68
            if i1 = i2 then 0
            else if Cil.intTypeIncluded i1 i2 then -1 else 1
69
          | C_float f1, C_float f2 ->
Julien Signoles's avatar
Julien Signoles committed
70
            Transitioning.Stdlib.compare f1 f2
71
72
73
74
75
          | (C_integer _ | C_float _ | Gmpz | Rational | Real), Nan
          | (C_integer _ | C_float _ | Gmpz | Rational ), Real
          | (C_integer _ | C_float _ | Gmpz), Rational
          | (C_integer _ | C_float _), Gmpz
          | C_integer _, C_float _ ->
Julien Signoles's avatar
Julien Signoles committed
76
            -1
77
78
79
80
          | (C_float _ | Gmpz | Rational | Real | Nan), C_integer _
          | (Gmpz | Rational | Real | Nan), C_float _
          | (Rational | Real | Nan), Gmpz
          | (Real | Nan), Rational
Julien Signoles's avatar
Julien Signoles committed
81
82
          | Nan, Real ->
            1
83
84
85
86
87
          | Gmpz, Gmpz
          | Rational, Rational
          | Real, Real
          | Nan, Nan ->
            assert false
88
89
90
91

      let equal = Datatype.from_compare

      let hash = function
92
93
        | C_integer ik -> 7 * Hashtbl.hash ik
        | C_float fk -> 97 * Hashtbl.hash fk
94
        | Gmpz -> 787
95
        | Rational -> 907
96
97
        | Real -> 1011
        | Nan -> 1277
98
99

      let pretty fmt = function
100
101
        | C_integer k -> Printer.pp_ikind fmt k
        | C_float k -> Printer.pp_fkind fmt k
102
        | Gmpz -> Format.pp_print_string fmt "Gmpz"
103
        | Rational -> Format.pp_print_string fmt "Rational"
104
105
        | Real -> Format.pp_print_string fmt "Real"
        | Nan -> Format.pp_print_string fmt "Nan"
106
    end)
107

108
109
110
111
(******************************************************************************)
(** Basic operations *)
(******************************************************************************)

112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
let join_cty ty1 ty2 =
  let ty = Cil.arithmeticConversion ty1 ty2 in
  match ty with
  | TInt(i, _) -> C_integer i
  | TFloat(f, _) -> C_float f
  | _ ->
    Options.fatal "[typing] join failure: unexpected result %a"
      Printer.pp_typ ty

let join ty1 ty2 =
  if ty1 == ty2 then ty1
  else
    match ty1, ty2 with
    | Nan, Nan | Real, Real | Rational, Rational | Gmpz, Gmpz ->
      assert false
    | Nan, (C_integer _ | C_float _ | Gmpz | Rational | Real as ty)
    | (C_integer _ | C_float _ | Gmpz | Rational | Real as ty), Nan ->
      Options.fatal "[typing] join failure: number %a and nan" D.pretty ty
    | Real, (C_integer _ | C_float _ | Gmpz | Rational)
    | (C_integer _ | C_float _ | Rational | Gmpz), Real ->
      Real
    | Rational, (C_integer _ | C_float _ | Gmpz)
    | (C_integer _ | C_float _ | Gmpz), Rational
    | C_float _, Gmpz
    | Gmpz, C_float _ ->
      Rational
    | Gmpz, C_integer _
    | C_integer _, Gmpz ->
      Gmpz
    | C_float f1, C_float f2 ->
      join_cty (TFloat(f1, [])) (TFloat(f2, []))
    | C_float f, C_integer n
    | C_integer n, C_float f ->
      join_cty (TFloat(f, [])) (TInt(n, []))
    | C_integer i1, C_integer i2 ->
      if Options.Gmp_only.get () then Gmpz
      else join_cty (TInt(i1, [])) (TInt(i2, []))
149

150
151
exception Not_a_number
let typ_of_number_ty = function
152
153
  | C_integer ik -> TInt(ik, [])
  | C_float fk -> TFloat(fk, [])
154
  | Gmpz -> Gmp_types.Z.t ()
155
  (* for the time being, no reals but rationals instead *)
156
  | Rational -> Gmp_types.Q.t ()
157
  | Real -> Error.not_yet "real number type"
158
  | Nan -> raise Not_a_number
159

160
161
let typ_of_lty = function
  | Ctype cty -> cty
162
  | Linteger -> Gmp_types.Z.t ()
163
  | Lreal -> Error.not_yet "real type"
164
165
  | Ltype _ | Lvar _ | Larrow _ -> Options.fatal "unexpected logic type"

166
167
168
169
(******************************************************************************)
(** Memoization *)
(******************************************************************************)

170
type computed_info =
Julien Signoles's avatar
Julien Signoles committed
171
172
173
  { ty: D.t;  (* type required for the term *)
    op: D.t; (* type required for the operation *)
    cast: D.t option; (* if not [None], type of the context which the term
174
                         must be casted to. If [None], no cast needed. *)
Julien Signoles's avatar
Julien Signoles committed
175
  }
176

177
178
(* Memoization module which retrieves the computed info of some terms. If the
   info is already computed for a term, it is never recomputed *)
179
180
181
182
183
184
module Memo: sig
  val memo: (term -> computed_info) -> term -> computed_info
  val get: term -> computed_info
  val clear: unit -> unit
end = struct

185
186
187
188
189
190
191
192
193
  (* The comparison over terms is the physical equality. It cannot be the
     structural one (given by [Cil_datatype.Term.equal]) because the very same
     term can be used in 2 different contexts which lead to different casts.

     By construction (see prepare_ast.ml), there are no physically equal terms
     in the E-ACSL's generated AST. Consequently the memoisation should be fully
     useless. However:
     - type info of many terms are accessed several times
     - the translation of E-ACSL guarded quantifications generates
Julien Signoles's avatar
Julien Signoles committed
194
195
196
197
198
       new terms (see module {!Quantif}) which must be typed. The term
       corresponding to the bound variable [x] is actually used twice: once in the
       guard and once for encoding [x+1] when incrementing it. The memoization is
       only useful here and indeed prevent the generation of one extra variable in
       some cases. *)
199
  let tbl = Misc.Id_term.Hashtbl.create 97
200
201

  let get t =
202
    try Misc.Id_term.Hashtbl.find tbl t
203
    with Not_found ->
204
205
206
      Options.fatal
        "[typing] type of term '%a' was never computed."
        Printer.pp_term t
207
208

  let memo f t =
209
    try Misc.Id_term.Hashtbl.find tbl t
210
211
    with Not_found ->
      let x = f t in
212
      Misc.Id_term.Hashtbl.add tbl t x;
213
214
      x

215
  let clear () = Misc.Id_term.Hashtbl.clear tbl
216
217
218
219
220
221
222
223
224

end

(******************************************************************************)
(** {2 Coercion rules} *)
(******************************************************************************)

(* Compute the smallest type (bigger than [int]) which can contain the whole
   interval. It is the \theta operator of the JFLA's paper. *)
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
let ty_of_interv ?ctx = function
  | Interval.Float(fk, _) -> C_float fk
  | Interval.Rational -> Rational
  | Interval.Real -> Real
  | Interval.Nan -> Nan
  | Interval.Ival iv ->
    try
      let kind = Interval.ikind_of_ival iv in
      (match ctx with
       | None
       | Some (Gmpz | Nan) ->
         C_integer kind
       | Some (C_integer ik as ctx) ->
         (* return [ctx] type for types smaller than int to prevent superfluous
            casts in the generated code *)
         if Cil.intTypeIncluded kind ik then ctx else C_integer kind
241
242
       | Some (C_float _ | Rational | Real as ty) ->
         ty)
243
    with Cil.Not_representable ->
Julien Signoles's avatar
Julien Signoles committed
244
245
246
247
    match ctx with
    | None | Some(C_integer _ | Gmpz | Nan) -> Gmpz
    | Some (C_float _ | Rational) -> Rational
    | Some Real -> Real
248

249
250
(* compute a new {!computed_info} by coercing the given type [ty] to the given
   context [ctx]. [op] is the type for the operator. *)
251
let coerce ~arith_operand ~ctx ~op ty =
252
  if D.compare ty ctx = 1 then
253
254
    (* type larger than the expected context,
       so we must introduce an explicit cast *)
255
    { ty; op; cast = Some ctx }
256
  else
257
258
    (* only add an explicit cast if the context is [Gmp] and [ty] is not;
       or if the term corresponding to [ty] is an operand of an arithmetic
Andre Maroneze's avatar
Andre Maroneze committed
259
       operation which must be explicitly coerced in order to force the
260
       operation to be of the expected type. *)
Julien Signoles's avatar
Julien Signoles committed
261
262
263
  if (ctx = Gmpz && ty <> Gmpz) || arith_operand
  then { ty; op; cast = Some ctx }
  else { ty; op; cast = None }
264

Julien Signoles's avatar
Julien Signoles committed
265
let number_ty_of_typ ty = match Cil.unrollType ty with
266
267
  | TInt(ik, _) | TEnum({ ekind = ik }, _) -> C_integer ik
  | TFloat(fk, _) -> C_float fk
Julien Signoles's avatar
Julien Signoles committed
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
  | TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
  | TNamed _ -> assert false

let ty_of_logic_ty ?term lty =
  let get_ty = function
    | Linteger -> Gmpz
    | Ctype ty -> number_ty_of_typ ty
    | Lreal -> Real
    | Larrow _ -> Nan
    | Ltype _ -> Error.not_yet "user-defined logic type"
    | Lvar _ -> Error.not_yet "type variable"
  in
  match term with
  | None -> get_ty lty
  | Some t ->
    if Options.Gmp_only.get () && lty = Linteger then Gmpz
    else
285
286
      let i = Interval.infer t in
      ty_of_interv i
Julien Signoles's avatar
Julien Signoles committed
287
288
289
290
291
292
293
294

(******************************************************************************)
(** {2 Type system} *)
(******************************************************************************)

(* generate a context [c]. Take --e-acsl-gmp-only into account iff [use_gmp_opt]
   is true. *)
let mk_ctx ~use_gmp_opt = function
295
296
297
298
  | C_integer _ as c ->
    if use_gmp_opt && Options.Gmp_only.get () then Gmpz
    else c
  | C_float _ | Gmpz | Rational | Real | Nan as c -> c
Julien Signoles's avatar
Julien Signoles committed
299

300
(* the number_ty corresponding to [t] whenever use as an offset.
301
302
   In that case, it cannot be a GMP, so it must be coerced to an integral type
   in that case *)
Julien Signoles's avatar
Julien Signoles committed
303
let type_offset t =
304
305
306
307
308
309
310
311
  let i = Interval.infer t in
  match ty_of_interv i with
  | Gmpz -> C_integer ILongLong (* largest possible type *)
  | ty -> ty

let type_letin li li_t =
  let i = Interval.infer li_t in
  Interval.Env.add li.l_var_info i
312

313
314
(* type the term [t] in a context [ctx] by taking --e-acsl-gmp-only into account
   iff [use_gmp_opt] is true. *)
315
316
let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
  let ctx = Extlib.opt_map (mk_ctx ~use_gmp_opt) ctx in
317
  let dup ty = ty, ty in
318
319
320
321
322
323
324
  let compute_ctx ?ctx i =
    (* in order to get a minimal amount of generated casts for operators, the
       result is typed in the given context [ctx], but not the operands.
       This function returns a tuple (ctx_of_result, ctx_of_operands) *)
    match ctx with
    | None ->
      (* no context: factorize *)
325
      dup (mk_ctx ~use_gmp_opt:true (ty_of_interv i))
326
    | Some ctx ->
327
328
      mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx i),
      mk_ctx ~use_gmp_opt:true (ty_of_interv i)
329
  in
330
331
  let infer t =
    Cil.CurrentLoc.set t.term_loc;
332
333
334
    (* this pattern matching implements the formal rules of the JFLA's paper
       (and of course also covers the missing cases). Also enforce the invariant
       that every subterm is typed, even if it is not an integer. *)
335
    match t.term_node with
336
    | TConst (Integer _ | LChr _ | LEnum _ | LReal _)
337
338
339
    | TSizeOf _
    | TSizeOfStr _
    | TAlignOf _ ->
340
341
      let i = Interval.infer t in
      let ty = ty_of_interv ?ctx i in
342
      dup ty
343

344
    | TLval tlv ->
345
346
      let i = Interval.infer t in
      let ty = ty_of_interv ?ctx i in
347
348
349
350
351
352
353
      type_term_lval tlv;
      dup ty

    | Toffset(_, t')
    | Tblock_length(_, t')
    | TSizeOfE t'
    | TAlignOfE t' ->
354
355
356
357
      let i = Interval.infer t in
      (* [t'] must be typed, but it is a pointer *)
      ignore (type_term ~use_gmp_opt:true ~ctx:Nan t');
      let ty = ty_of_interv ?ctx i in
358
      dup ty
359

360
    | TBinOp (MinusPP, t1, t2) ->
361
362
363
364
365
      let i = Interval.infer t in
      (* [t1] and [t2] must be typed, but they are pointers *)
      ignore (type_term ~use_gmp_opt:true ~ctx:Nan t1);
      ignore (type_term ~use_gmp_opt:true ~ctx:Nan t2);
      let ty = ty_of_interv ?ctx i in
366
367
368
      dup ty

    | TUnOp (unop, t') ->
369
370
371
      let i = Interval.infer t in
      let i' = Interval.infer t' in
      let ctx_res, ctx = compute_ctx ?ctx (Interval.join i i') in
372
373
374
375
376
377
378
      ignore (type_term ~use_gmp_opt:true ~arith_operand:true ~ctx t');
      (match unop with
       | LNot -> c_int, ctx_res (* converted into [t == 0] in case of GMP *)
       | Neg | BNot -> dup ctx_res)

    | TBinOp ((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt), t1, t2)
      ->
379
380
381
      let i = Interval.infer t in
      let i1 = Interval.infer t1 in
      let i2 = Interval.infer t2 in
382
      let ctx_res, ctx =
383
        compute_ctx ?ctx (Interval.join i (Interval.join i1 i2))
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
      in
      (* it is enough to explicitly coerce when required one operand to [ctx]
         (through [arith_operand]) in order to force the type of the
         operation.  Heuristic: coerce the operand which is not a lval in
         order to lower the number of explicit casts *)
      let rec cast_first t1 t2 = match t1.term_node with
        | TLval _ -> false
        | TLogic_coerce(_, t) -> cast_first t t2
        | _ -> true
      in
      let cast_first = cast_first t1 t2 in
      ignore (type_term ~use_gmp_opt:true ~arith_operand:cast_first ~ctx t1);
      ignore
        (type_term ~use_gmp_opt:true ~arith_operand:(not cast_first) ~ctx t2);
      dup ctx_res

    | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
      assert (match ctx with None -> true | Some c -> D.compare c c_int >= 0);
402
403
      let i1 = Interval.infer t1 in
      let i2 = Interval.infer t2 in
404
      let ctx =
405
        mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Interval.join i1 i2))
406
407
408
409
410
      in
      ignore (type_term ~use_gmp_opt:true ~ctx t1);
      ignore (type_term ~use_gmp_opt:true ~ctx t2);
      let ty = match ctx with
        | Nan -> c_int
411
        | Real | Rational | Gmpz | C_float _ | C_integer _ -> ctx
412
413
414
415
      in
      c_int, ty

    | TBinOp ((LAnd | LOr), t1, t2) ->
416
417
418
      let i1 = Interval.infer t1 in
      let i2 = Interval.infer t2 in
      let ty = ty_of_interv ?ctx (Interval.join i1 i2) in
419
420
421
422
423
424
425
426
427
428
      (* both operands fit in an int. *)
      ignore (type_term ~use_gmp_opt:true ~ctx:c_int t1);
      ignore (type_term ~use_gmp_opt:true ~ctx:c_int t2);
      dup ty

    | TBinOp (BAnd, _, _) -> Error.not_yet "bitwise and"
    | TBinOp (BXor, _, _) -> Error.not_yet "bitwise xor"
    | TBinOp (BOr, _, _) -> Error.not_yet "bitwise or"

    | TCastE(_, t') ->
429
430
431
432
433
      (* compute the smallest interval from the whole term [t] *)
      let i = Interval.infer t in
      (* nothing more to do: [i] is already more precise than what we could
         infer from the arguments of the cast. *)
      let ctx = ty_of_interv ?ctx i in
434
435
436
437
438
439
440
441
442
      ignore (type_term ~use_gmp_opt:true ~ctx t');
      dup ctx

    | Tif (t1, t2, t3) ->
      let ctx1 =
        mk_ctx ~use_gmp_opt:false c_int (* an int must be generated *)
      in
      ignore (type_term ~use_gmp_opt:false ~ctx:ctx1 t1);
      let i = Interval.infer t in
443
444
445
446
      let i2 = Interval.infer t2 in
      let i3 = Interval.infer t3 in
      let ctx = ty_of_interv ?ctx (Interval.join i (Interval.join i2 i3)) in
      let ctx = mk_ctx ~use_gmp_opt:true ctx in
447
448
449
450
451
452
453
454
455
456
457
458
      ignore (type_term ~use_gmp_opt:true ~ctx t2);
      ignore (type_term ~use_gmp_opt:true ~ctx t3);
      dup ctx

    | Tat (t, _)
    | TLogic_coerce (_, t) ->
      dup (type_term ~use_gmp_opt ~arith_operand ?ctx t).ty

    | TAddrOf tlv
    | TStartOf tlv ->
      (* it is a pointer, but subterms must be typed. *)
      type_term_lval tlv;
459
      dup Nan
460
461
462

    | Tbase_addr (_, t) ->
      (* it is a pointer, but subterms must be typed. *)
463
464
      ignore (type_term ~use_gmp_opt:true ~ctx:Nan t);
      dup Nan
465
466
467

    | TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
      (* both [t1] and [t2] must be typed. *)
468
      ignore (type_term ~use_gmp_opt:true ~ctx:Nan t1);
469
470
      let ctx = type_offset t2 in
      ignore (type_term ~use_gmp_opt:false ~ctx t2);
471
      dup Nan
472
473
474
475
476
477
478
479

    | Tapp(li, _, args) ->
      if Builtins.mem li.l_var_info.lv_name then
        let typ_arg lvi arg =
          (* a built-in is a C function, so the context is necessarily a C
             type. *)
          let ctx = ty_of_logic_ty lvi.lv_type in
          ignore (type_term ~use_gmp_opt:false ~ctx arg)
480
        in
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
        List.iter2 typ_arg li.l_profile args;
        (* [li.l_type is [None] for predicate only: not possible here.
           Thus using [Extlib.the] is fine *)
        dup (ty_of_logic_ty (Extlib.the li.l_type))
      else begin
        (* TODO: what if the type of the parameter is smaller than the infered
           type of the argument? For now, it is silently ignored (both
           statically and at runtime)... *)
        List.iter (fun arg -> ignore (type_term ~use_gmp_opt:true arg)) args;
        (* TODO: recursive call in arguments of function call *)
        match li.l_body with
        | LBpred _ ->
          (* possible to have an [LBpred] here because we transformed
             [Papp] into [Tapp] *)
          dup c_int
        | LBterm _ ->
          begin match li.l_type with
            | None ->
              assert false
            | Some lty ->
501
              (* TODO: what if the function returns a real? *)
502
503
504
505
506
507
508
509
510
511
512
513
514
515
              let ty = ty_of_logic_ty ~term:t lty in
              dup ty
          end
        | LBnone ->
          Error.not_yet "logic functions with no definition nor reads clause"
        | LBreads _ ->
          Error.not_yet "logic functions performing read accesses"
        | LBinductive _ ->
          Error.not_yet "logic functions inductively defined"
      end

    | Tunion _ -> Error.not_yet "tset union"
    | Tinter _ -> Error.not_yet "tset intersection"
    | Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
516
517
518

    | Trange(None, _) | Trange(_, None) ->
      Options.abort "unbounded ranges are not part of E-ACSl"
519
520
521
    | Trange(Some n1, Some n2) ->
      ignore (type_term ~use_gmp_opt n1);
      ignore (type_term ~use_gmp_opt n2);
522
523
524
      let i = Interval.infer t in
      let ty = ty_of_interv ?ctx i in
      dup ty
525
526
527

    | Tlet(li, t) ->
      let li_t = Misc.term_of_li li in
528
      type_letin li li_t;
529
530
      ignore (type_term ~use_gmp_opt:true li_t);
      dup (type_term ~use_gmp_opt:true ?ctx t).ty
531

532
533
534
535
536
537
538
539
    | Tlambda (_,_) -> Error.not_yet "lambda"
    | TDataCons (_,_) -> Error.not_yet "datacons"
    | TUpdate (_,_,_) -> Error.not_yet "update"

    | Tnull
    | TConst (LStr _ | LWStr _)
    | Ttypeof _
    | Ttype _
540
    | Tempty_set  -> dup Nan
541
  in
542
543
  Memo.memo
    (fun t ->
544
545
546
547
       let ty, op = infer t in
       match ctx with
       | None -> { ty; op; cast = None }
       | Some ctx -> coerce ~arith_operand ~ctx ~op ty)
548
    t
549

550
551
552
and type_term_lval (host, offset) =
  type_term_lhost host;
  type_term_offset offset
553

554
and type_term_lhost = function
555
556
  | TVar _
  | TResult _ -> ()
557
  | TMem t -> ignore (type_term ~use_gmp_opt:false ~ctx:Nan t)
558

559
and type_term_offset = function
560
561
  | TNoOffset -> ()
  | TField(_, toff)
562
  | TModel(_, toff) -> type_term_offset toff
563
  | TIndex(t, toff) ->
Julien Signoles's avatar
Julien Signoles committed
564
    let ctx = type_offset t in
565
    ignore (type_term ~use_gmp_opt:false ~ctx t);
566
    type_term_offset toff
567

568
569
let rec type_predicate p =
  Cil.CurrentLoc.set p.pred_loc;
570
  (* this pattern matching also follows the formal rules of the JFLA's paper *)
571
572
  let op =
    match p.pred_content with
573
    | Pfalse | Ptrue -> c_int
574
575
    | Papp(li, _, _) ->
      begin match li.l_body with
576
577
578
579
580
581
        | LBpred _ ->
          (* No need to type subpredicates
             since Papp will be transformed into Tapp in Translate:
             a retyping is done there *)
          c_int
        | LBnone -> (* Eg: \is_finite *)
582
          Error.not_yet "predicate with no definition nor reads clause"
583
584
        | LBreads _ | LBterm _ | LBinductive _ ->
          Options.fatal "unexpected logic definition"
585
      end
586
587
588
    | Pseparated _ -> Error.not_yet "\\separated"
    | Pdangling _ -> Error.not_yet "\\dangling"
    | Prel(_, t1, t2) ->
589
590
591
592
      let i1 = Interval.infer t1 in
      let i2 = Interval.infer t2 in
      let i = Interval.join i1 i2 in
      let ctx = mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i) in
593
594
      ignore (type_term ~use_gmp_opt:true ~ctx t1);
      ignore (type_term ~use_gmp_opt:true ~ctx t2);
595
      (match ctx with
596
       | Nan -> c_int
597
       | Real | Rational | Gmpz | C_float _ | C_integer _ -> ctx)
598
599
600
601
602
    | Pand(p1, p2)
    | Por(p1, p2)
    | Pxor(p1, p2)
    | Pimplies(p1, p2)
    | Piff(p1, p2) ->
603
604
      ignore (type_predicate p1);
      ignore (type_predicate p2);
605
606
      c_int
    | Pnot p ->
607
      ignore (type_predicate p);
608
609
      c_int
    | Pif(t, p1, p2) ->
610
611
      let ctx = mk_ctx ~use_gmp_opt:false c_int in
      ignore (type_term ~use_gmp_opt:false ~ctx t);
612
613
      ignore (type_predicate p1);
      ignore (type_predicate p2);
614
      c_int
615
616
    | Plet(li, p) ->
      let li_t = Misc.term_of_li li in
617
      type_letin li li_t;
618
619
      ignore (type_term ~use_gmp_opt:true li_t);
      (type_predicate p).ty
620

621
622
    | Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) })
    | Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
623
      let guards = !compute_quantif_guards_ref p bounded_vars hyps in
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
      let iv_plus_one iv =
        Interval.Ival (Ival.add_singleton_int Integer.one iv)
      in
      List.iter
        (fun (t1, r1, x, r2, t2) ->
           let i1 = Interval.infer t1 in
           let i1 = match r1, i1 with
             | Rlt, Interval.Ival iv -> iv_plus_one iv
             | Rle, _ -> i1
             | _ -> assert false
           in
           let i2 = Interval.infer t2 in
           (* add one to [i2], since we increment the loop counter one more
              time before going outside the loop. *)
           let i2 = match r2, i2 with
             | Rlt, _ -> i2
             | Rle, Interval.Ival iv -> iv_plus_one iv
             | _ -> assert false
           in
           let i = Interval.join i1 i2 in
           let ctx = match x.lv_type with
             | Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i)
             | Ctype ty ->
               (match Cil.unrollType ty with
                | TInt(ik, _) -> mk_ctx ~use_gmp_opt:true (C_integer ik)
                | ty ->
650
                  Options.fatal "unexpected type %a for quantified variable %a"
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
                    Printer.pp_typ ty
                    Printer.pp_logic_var x)
             | lty ->
               Options.fatal "unexpected type %a for quantified variable %a"
                 Printer.pp_logic_type lty
                 Printer.pp_logic_var x
           in
           (* forcing when typing bounds prevents to generate an extra useless
              GMP variable when --e-acsl-gmp-only *)
           ignore (type_term ~use_gmp_opt:false ~ctx t1);
           ignore (type_term ~use_gmp_opt:false ~ctx t2);
           (* if we must generate GMP code, degrade the interval in order to
              guarantee that [x] will be a GMP when typing the goal *)
           let i = match ctx with
             | C_integer _ -> i
             | Gmpz -> Interval.top_ival (* [ -\infty; +\infty ] *)
             | C_float _ | Rational | Real | Nan ->
               Options.fatal "unexpected quantification over %a" D.pretty ctx
           in
           Interval.Env.add x i)
        guards;
      (type_predicate goal).ty
673
674
675
676
677
678
679

    | Pinitialized(_, t)
    | Pfreeable(_, t)
    | Pallocable(_, t)
    | Pvalid(_, t)
    | Pvalid_read(_, t)
    | Pvalid_function t ->
680
      ignore (type_term ~use_gmp_opt:false ~ctx:Nan t);
681
      c_int
682
683
684

    | Pforall _ -> Error.not_yet "unguarded \\forall quantification"
    | Pexists _ -> Error.not_yet "unguarded \\exists quantification"
685
    | Pat(p, _) -> (type_predicate p).ty
686
687
    | Pfresh _ -> Error.not_yet "\\fresh"
  in
688
  coerce ~arith_operand:false ~ctx:c_int ~op c_int
689

690
let type_term ~use_gmp_opt ?ctx t =
691
  Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
692
    Printer.pp_term t (Pretty_utils.pp_opt D.pretty) ctx;
693
  ignore (type_term ~use_gmp_opt ?ctx t)
694

695
let type_named_predicate ?(must_clear=true) p =
696
  Options.feedback ~dkey ~level:3 "typing predicate '%a'."
697
    Printer.pp_predicate p;
698
699
700
701
  if must_clear then begin
    Interval.Env.clear ();
    Memo.clear ()
  end;
702
  ignore (type_predicate p)
703

704
705
706
707
708
let unsafe_set t ?ctx ty =
  let ctx = match ctx with None -> ty | Some ctx -> ctx in
  let mk _ = coerce ~arith_operand:false ~ctx ~op:ty ty in
  ignore (Memo.memo mk t)

709
(******************************************************************************)
710
(** {2 Getters} *)
711
712
(******************************************************************************)

713
let get_number_ty t = (Memo.get t).ty
714
let get_integer_op t = (Memo.get t).op
715
let get_integer_op_of_predicate p = (type_predicate p).op
716

717
(* {!typ_of_integer}, but handle the not-integer cases. *)
718
let extract_typ t ty =
719
720
  try typ_of_number_ty ty
  with Not_a_number ->
Julien Signoles's avatar
Julien Signoles committed
721
722
723
724
725
726
727
  match t.term_type with
  | Ctype _ as lty -> Logic_utils.logicCType lty
  | Linteger | Lreal ->
    Options.fatal "unexpected context NaN for term %a" Printer.pp_term t
  | Ltype _ -> Error.not_yet "unsupported logic type: user-defined type"
  | Lvar _ -> Error.not_yet "unsupported logic type: type variable"
  | Larrow _ -> Error.not_yet "unsupported logic type: type arrow"
728

729
730
let get_typ t =
  let info = Memo.get t in
731
  extract_typ t info.ty
732

733
734
let get_op t =
  let info = Memo.get t in
735
  extract_typ t info.op
736

737
738
let get_cast t =
  let info = Memo.get t in
739
740
  try Extlib.opt_map typ_of_number_ty info.cast
  with Not_a_number -> None
741
742

let get_cast_of_predicate p =
743
  let info = type_predicate p in
744
745
  try Extlib.opt_map typ_of_number_ty info.cast
  with Not_a_number -> assert false
746
747

let clear = Memo.clear
748

749
750
module Datatype = D

751
752
(*
Local Variables:
753
compile-command: "make -C ../../../../.."
754
755
End:
*)