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
31
    : (predicate -> logic_var list -> predicate ->
32
33
34
35
       (term * relation * logic_var * relation * term) list) ref
    = Extlib.mk_fun "compute_quantif_guards_ref"

(******************************************************************************)
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 =
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
175
176
                         must be casted to. If [None], no cast needed. *)
    }

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
185
186
module Memo: sig
  val memo: (term -> computed_info) -> term -> computed_info
  val get: term -> computed_info
  val clear: unit -> unit
end = struct

  module H = Hashtbl.Make(struct
    type t = term
187
188
189
190
191
192
193
194
195
196
197
198
199
    (* 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, there are no physically equal terms in the AST
       built by Cil. Consequently the memoisation should be fully
       useless. However the translation of E-ACSL guarded quantification
       generates 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. *)
200
201
202
203
204
205
206
207
208
    let equal (t1:term) t2 = t1 == t2
    let hash = Cil_datatype.Term.hash
  end)

  let tbl = H.create 97

  let get t =
    try H.find tbl t
    with Not_found ->
209
210
211
      Options.fatal
        "[typing] type of term '%a' was never computed."
        Printer.pp_term t
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229

  let memo f t =
    try H.find tbl t
    with Not_found ->
      let x = f t in
      H.add tbl t x;
      x

  let clear () = H.clear tbl

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. *)
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
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
246
247
       | Some (C_float _ | Rational | Real as ty) ->
         ty)
248
249
250
251
252
    with Cil.Not_representable ->
      match ctx with
      | None | Some(C_integer _ | Gmpz | Nan) -> Gmpz
      | Some (C_float _ | Rational) -> Rational
      | Some Real -> Real
253

254
255
(* compute a new {!computed_info} by coercing the given type [ty] to the given
   context [ctx]. [op] is the type for the operator. *)
256
let coerce ~arith_operand ~ctx ~op ty =
257
  if D.compare ty ctx = 1 then
258
259
    (* type larger than the expected context,
       so we must introduce an explicit cast *)
260
    { ty; op; cast = Some ctx }
261
  else
262
263
    (* 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
264
       operation which must be explicitly coerced in order to force the
265
       operation to be of the expected type. *)
266
    if (ctx = Gmpz && ty <> Gmpz) || arith_operand
267
    then { ty; op; cast = Some ctx }
268
    else { ty; op; cast = None }
269

Julien Signoles's avatar
Julien Signoles committed
270
let number_ty_of_typ ty = match Cil.unrollType ty with
271
272
  | TInt(ik, _) | TEnum({ ekind = ik }, _) -> C_integer ik
  | TFloat(fk, _) -> C_float fk
Julien Signoles's avatar
Julien Signoles committed
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
  | 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
290
291
      let i = Interval.infer t in
      ty_of_interv i
Julien Signoles's avatar
Julien Signoles committed
292
293
294
295
296
297
298
299

(******************************************************************************)
(** {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
300
301
302
303
  | 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
304

305
(* the number_ty corresponding to [t] whenever use as an offset.
306
307
   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
308
let type_offset t =
309
310
311
312
313
314
315
316
  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
317

318
319
(* type the term [t] in a context [ctx] by taking --e-acsl-gmp-only into account
   iff [use_gmp_opt] is true. *)
320
321
let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
  let ctx = Extlib.opt_map (mk_ctx ~use_gmp_opt) ctx in
322
  let dup ty = ty, ty in
323
324
325
326
327
328
329
  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 *)
330
      dup (mk_ctx ~use_gmp_opt:true (ty_of_interv i))
331
    | Some ctx ->
332
333
      mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx i),
      mk_ctx ~use_gmp_opt:true (ty_of_interv i)
334
  in
335
336
  let infer t =
    Cil.CurrentLoc.set t.term_loc;
337
338
339
    (* 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. *)
340
    match t.term_node with
341
    | TConst (Integer _ | LChr _ | LEnum _ | LReal _)
342
343
344
    | TSizeOf _
    | TSizeOfStr _
    | TAlignOf _ ->
345
346
      let i = Interval.infer t in
      let ty = ty_of_interv ?ctx i in
347
      dup ty
348

349
    | TLval tlv ->
350
351
      let i = Interval.infer t in
      let ty = ty_of_interv ?ctx i in
352
353
354
355
356
357
358
      type_term_lval tlv;
      dup ty

    | Toffset(_, t')
    | Tblock_length(_, t')
    | TSizeOfE t'
    | TAlignOfE t' ->
359
360
361
362
      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
363
      dup ty
364

365
    | TBinOp (MinusPP, t1, t2) ->
366
367
368
369
370
      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
371
372
373
      dup ty

    | TUnOp (unop, t') ->
374
375
376
      let i = Interval.infer t in
      let i' = Interval.infer t' in
      let ctx_res, ctx = compute_ctx ?ctx (Interval.join i i') in
377
378
379
380
381
382
383
      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)
      ->
384
385
386
      let i = Interval.infer t in
      let i1 = Interval.infer t1 in
      let i2 = Interval.infer t2 in
387
      let ctx_res, ctx =
388
        compute_ctx ?ctx (Interval.join i (Interval.join i1 i2))
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
      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);
407
408
      let i1 = Interval.infer t1 in
      let i2 = Interval.infer t2 in
409
      let ctx =
410
        mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Interval.join i1 i2))
411
412
413
414
415
      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
416
        | Real | Rational | Gmpz | C_float _ | C_integer _ -> ctx
417
418
419
420
      in
      c_int, ty

    | TBinOp ((LAnd | LOr), t1, t2) ->
421
422
423
      let i1 = Interval.infer t1 in
      let i2 = Interval.infer t2 in
      let ty = ty_of_interv ?ctx (Interval.join i1 i2) in
424
425
426
427
428
429
430
431
432
433
      (* 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') ->
434
435
436
437
438
      (* 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
439
440
441
442
443
444
445
446
447
      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
448
449
450
451
      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
452
453
454
455
456
457
458
459
460
461
462
463
      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;
464
      dup Nan
465
466
467

    | Tbase_addr (_, t) ->
      (* it is a pointer, but subterms must be typed. *)
468
469
      ignore (type_term ~use_gmp_opt:true ~ctx:Nan t);
      dup Nan
470
471
472

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

    | 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)
485
        in
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
        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 ->
506
              (* TODO: what if the function returns a real? *)
507
508
509
510
511
512
513
514
515
516
517
518
519
520
              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"
521
522
523

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

    | Tlet(li, t) ->
      let li_t = Misc.term_of_li li in
533
      type_letin li li_t;
534
535
      ignore (type_term ~use_gmp_opt:true li_t);
      dup (type_term ~use_gmp_opt:true ?ctx t).ty
536

537
538
539
540
541
542
543
544
    | Tlambda (_,_) -> Error.not_yet "lambda"
    | TDataCons (_,_) -> Error.not_yet "datacons"
    | TUpdate (_,_,_) -> Error.not_yet "update"

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

555
556
557
and type_term_lval (host, offset) =
  type_term_lhost host;
  type_term_offset offset
558

559
and type_term_lhost = function
560
561
  | TVar _
  | TResult _ -> ()
562
  | TMem t -> ignore (type_term ~use_gmp_opt:false ~ctx:Nan t)
563

564
and type_term_offset = function
565
566
  | TNoOffset -> ()
  | TField(_, toff)
567
  | TModel(_, toff) -> type_term_offset toff
568
  | TIndex(t, toff) ->
Julien Signoles's avatar
Julien Signoles committed
569
    let ctx = type_offset t in
570
    ignore (type_term ~use_gmp_opt:false ~ctx t);
571
    type_term_offset toff
572

573
574
let rec type_predicate p =
  Cil.CurrentLoc.set p.pred_loc;
575
  (* this pattern matching also follows the formal rules of the JFLA's paper *)
576
577
  let op =
    match p.pred_content with
578
    | Pfalse | Ptrue -> c_int
579
580
    | Papp(li, _, _) ->
      begin match li.l_body with
581
582
583
584
585
586
        | 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 *)
587
          Error.not_yet "predicate with no definition nor reads clause"
588
589
        | LBreads _ | LBterm _ | LBinductive _ ->
          Options.fatal "unexpected logic definition"
590
      end
591
592
593
    | Pseparated _ -> Error.not_yet "\\separated"
    | Pdangling _ -> Error.not_yet "\\dangling"
    | Prel(_, t1, t2) ->
594
595
596
597
      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
598
599
      ignore (type_term ~use_gmp_opt:true ~ctx t1);
      ignore (type_term ~use_gmp_opt:true ~ctx t2);
600
      (match ctx with
601
       | Nan -> c_int
602
       | Real | Rational | Gmpz | C_float _ | C_integer _ -> ctx)
603
604
605
606
607
    | Pand(p1, p2)
    | Por(p1, p2)
    | Pxor(p1, p2)
    | Pimplies(p1, p2)
    | Piff(p1, p2) ->
608
609
      ignore (type_predicate p1);
      ignore (type_predicate p2);
610
611
      c_int
    | Pnot p ->
612
      ignore (type_predicate p);
613
614
      c_int
    | Pif(t, p1, p2) ->
615
616
      let ctx = mk_ctx ~use_gmp_opt:false c_int in
      ignore (type_term ~use_gmp_opt:false ~ctx t);
617
618
      ignore (type_predicate p1);
      ignore (type_predicate p2);
619
      c_int
620
621
    | Plet(li, p) ->
      let li_t = Misc.term_of_li li in
622
      type_letin li li_t;
623
624
      ignore (type_term ~use_gmp_opt:true li_t);
      (type_predicate p).ty
625

626
627
    | Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) })
    | Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
628
      let guards = !compute_quantif_guards_ref p bounded_vars hyps in
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
      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 ->
655
                  Options.fatal "unexpected type %a for quantified variable %a"
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
                    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
678
679
680
681
682
683
684

    | Pinitialized(_, t)
    | Pfreeable(_, t)
    | Pallocable(_, t)
    | Pvalid(_, t)
    | Pvalid_read(_, t)
    | Pvalid_function t ->
685
      ignore (type_term ~use_gmp_opt:false ~ctx:Nan t);
686
      c_int
687
688
689

    | Pforall _ -> Error.not_yet "unguarded \\forall quantification"
    | Pexists _ -> Error.not_yet "unguarded \\exists quantification"
690
    | Pat(p, _) -> (type_predicate p).ty
691
692
    | Pfresh _ -> Error.not_yet "\\fresh"
  in
693
  coerce ~arith_operand:false ~ctx:c_int ~op c_int
694

695
let type_term ~use_gmp_opt ?ctx t =
696
  Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
697
    Printer.pp_term t (Pretty_utils.pp_opt D.pretty) ctx;
698
  ignore (type_term ~use_gmp_opt ?ctx t)
699

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

709
710
711
712
713
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)

714
(******************************************************************************)
715
(** {2 Getters} *)
716
717
(******************************************************************************)

718
let get_number_ty t = (Memo.get t).ty
719
let get_integer_op t = (Memo.get t).op
720
let get_integer_op_of_predicate p = (type_predicate p).op
721

722
(* {!typ_of_integer}, but handle the not-integer cases. *)
723
let extract_typ t ty =
724
725
  try typ_of_number_ty ty
  with Not_a_number ->
726
727
    match t.term_type with
    | Ctype _ as lty -> Logic_utils.logicCType lty
728
729
    | Linteger | Lreal ->
      Options.fatal "unexpected context NaN for term %a" Printer.pp_term t
730
731
732
    | 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"
733

734
735
let get_typ t =
  let info = Memo.get t in
736
  extract_typ t info.ty
737

738
739
let get_op t =
  let info = Memo.get t in
740
  extract_typ t info.op
741

742
743
let get_cast t =
  let info = Memo.get t in
744
745
  try Extlib.opt_map typ_of_number_ty info.cast
  with Not_a_number -> None
746
747

let get_cast_of_predicate p =
748
  let info = type_predicate p in
749
750
  try Extlib.opt_map typ_of_number_ty info.cast
  with Not_a_number -> assert false
751
752

let clear = Memo.clear
753

754
755
module Datatype = D

756
757
(*
Local Variables:
758
compile-command: "make -C ../.."
759
760
End:
*)