typing.ml 27.4 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
(*                                                                        *)
Patrick Baudin's avatar
Patrick Baudin committed
5
(*  Copyright (C) 2012-2018                                               *)
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
  | C_type of ikind
41
  | Gmpz
42
  | Real
43
  | Nan
44

45
46
let c_int = C_type IInt
let ikind ik = C_type ik
47
let gmpz = Gmpz
48
let real = Real
49
let nan = Nan
50

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

      let compare ty1 ty2 = match ty1, ty2 with
        | C_type i1, C_type i2 ->
          if i1 = i2 then 0
          else if Cil.intTypeIncluded i1 i2 then -1 else 1
63
64
65
66
67
68
69
70
71
        | (C_type _ | Gmpz | Real), Nan
        | (C_type _ | Gmpz), Real
        | C_type _, Gmpz ->
          -1
        | (Gmpz | Real | Nan), C_type _
        | (Real | Nan), Gmpz
        | Nan, Real ->
          1
        | Gmpz, Gmpz | Real, Real | Nan, Nan -> 0
72
73
74
75

      let equal = Datatype.from_compare

      let hash = function
76
77
78
79
        | C_type ik -> 7 * Hashtbl.hash ik
        | Gmpz -> 787
        | Real -> 1011
        | Nan -> 1277
80
81
82

      let pretty fmt = function
        | C_type k -> Printer.pp_ikind fmt k
83
84
85
        | Gmpz -> Format.pp_print_string fmt "Gmpz"
        | Real -> Format.pp_print_string fmt "Real"
        | Nan -> Format.pp_print_string fmt "Nan"
86
    end)
87

88
89
90
91
(******************************************************************************)
(** Basic operations *)
(******************************************************************************)

92
let join ty1 ty2 = match ty1, ty2 with
93
94
  | Nan, Nan ->
    Nan
95
  | Nan, Real | Real, Nan ->
96
    Options.fatal "[typing] join failure: real and nan"
97
98
99
  | Real, Real -> Real
  | Real, (Gmpz | C_type _) | (Gmpz | C_type _), Real ->
    Real
100
101
102
  | Nan, (Gmpz | C_type _) | (Gmpz | C_type _), Nan ->
    Options.fatal "[typing] join failure: integer and nan"
  | Gmpz, _ | _, Gmpz -> Gmpz
103
  | C_type i1, C_type i2 ->
104
    if Options.Gmp_only.get () then Gmpz
105
    else
106
107
108
109
110
111
112
      let ty = Cil.arithmeticConversion (TInt(i1, [])) (TInt(i2, [])) in
      match ty with
      | TInt(i, _) -> C_type i
      | _ ->
        Options.fatal "[typing] join failure: unexpected result %a"
          Printer.pp_typ ty

113
114
exception Not_a_number
let typ_of_number_ty = function
115
  | C_type ik -> TInt(ik, [])
116
  | Gmpz -> Gmp.Z.t ()
117
  | Real -> Real.t ()
118
  | Nan -> raise Not_a_number
119

120
121
let typ_of_lty = function
  | Ctype cty -> cty
122
  | Linteger -> Gmp.Z.t ()
123
124
125
  | Lreal ->
    (* TODO RATIONAL: implement this case *)
    assert false
126
127
  | Ltype _ | Lvar _ | Larrow _ -> Options.fatal "unexpected logic type"

128
129
130
131
(******************************************************************************)
(** Memoization *)
(******************************************************************************)

132
type computed_info =
133
134
135
    { 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
136
137
138
                         must be casted to. If [None], no cast needed. *)
    }

139
140
(* Memoization module which retrieves the computed info of some terms. If the
   info is already computed for a term, it is never recomputed *)
141
142
143
144
145
146
147
148
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
149
150
151
152
153
154
155
156
157
158
159
160
161
    (* 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. *)
162
163
164
165
166
167
168
169
170
    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 ->
171
172
173
      Options.fatal
        "[typing] type of term '%a' was never computed."
        Printer.pp_term t
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189

  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} *)
(******************************************************************************)

Julien Signoles's avatar
Julien Signoles committed
190
let ty_of_logic_ty = function
191
  | Linteger -> Gmpz
Julien Signoles's avatar
Julien Signoles committed
192
193
  | Ctype ty -> (match Cil.unrollType ty with
    | TInt(ik, _) -> C_type ik
194
    | TFloat _ -> Real
195
    | _ -> Nan)
196
  | Lreal -> Real
197
  | Larrow _ -> Nan
Julien Signoles's avatar
Julien Signoles committed
198
199
200
  | Ltype _ -> Error.not_yet "user-defined logic type"
  | Lvar _ -> Error.not_yet "type variable"

201
let number_ty_of_typ ty = ty_of_logic_ty (Ctype ty)
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
202

203
204
(* Compute the smallest type (bigger than [int]) which can contain the whole
   interval. It is the \theta operator of the JFLA's paper. *)
205
let ty_of_interv ?ctx i =
206
  try
Julien Signoles's avatar
Julien Signoles committed
207
    let kind = Interval.ikind_of_interv i in
208
    (* ctx type whenever possible to prevent superfluous casts in the generated
209
       code *)
210
    (match ctx with
211
     | None | Some (Gmpz | Nan) -> C_type kind
212
     | Some (C_type ik as ctx) ->
213
       if Cil.intTypeIncluded kind ik then ctx else C_type kind
214
     | Some Real -> Real)
215
  with Cil.Not_representable ->
216
    match ctx with
217
    | Some Real -> Real
218
    | None | Some _ -> Gmpz
219

220
221
(* compute a new {!computed_info} by coercing the given type [ty] to the given
   context [ctx]. [op] is the type for the operator. *)
222
let coerce ~arith_operand ~ctx ~op ty =
223
  if D.compare ty ctx = 1 then
224
225
    (* type larger than the expected context,
       so we must introduce an explicit cast *)
226
    { ty; op; cast = Some ctx }
227
  else
228
229
    (* 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
230
       operation which must be explicitly coerced in order to force the
231
       operation to be of the expected type. *)
232
    if (ctx = Gmpz && ty <> Gmpz) || arith_operand
233
    then { ty; op; cast = Some ctx }
234
    else { ty; op; cast = None }
235

236
(* the number_ty corresponding to [t] whenever use as an offset.
237
238
239
240
241
242
   In that case, it cannot be a GMP, so it must be coerced to an integral type
   in that case *)
let offset_ty t =
  try
    let i = Interval.infer t in
    match ty_of_interv i with
243
    | Gmpz -> C_type ILongLong (* largest possible type *)
244
    | ty -> ty
245
  with
246
247
248
249
250
  | Interval.Is_a_real ->
    (* TODO RATIONAL: shouldn't it be 'assert false' because of typing? *)
    C_type ILongLong
  | Interval.Not_a_number ->
    Options.fatal "expected an integral type for %a" Printer.pp_term t
251

252
(******************************************************************************)
253
(** {2 Type system} *)
254
255
(******************************************************************************)

256
257
258
(* generate a context [c]. Take --e-acsl-gmp-only into account iff [use_gmp_opt]
   is true. *)
let mk_ctx ~use_gmp_opt = function
259
  | C_type _ as c -> if use_gmp_opt && Options.Gmp_only.get () then Gmpz else c
260
  | Gmpz | Real | Nan as c -> c
261

262
263
264
let infer_if_integer li =
  let li_t = Misc.term_of_li li in
  match ty_of_logic_ty li_t.term_type with
265
  | C_type _ | Gmpz ->
266
267
    let i = Interval.infer li_t in
    Interval.Env.add li.l_var_info i
268
  | Real | Nan ->
269
270
    ()

271
272
(* type the term [t] in a context [ctx] by taking --e-acsl-gmp-only into account
   iff [use_gmp_opt] is true. *)
273
274
let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
  let ctx = Extlib.opt_map (mk_ctx ~use_gmp_opt) ctx in
275
  let dup ty = ty, ty in
276
277
278
279
280
281
282
  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 *)
283
      dup (mk_ctx ~use_gmp_opt:true (ty_of_interv i))
284
    | Some ctx ->
285
286
      mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx i),
      mk_ctx ~use_gmp_opt:true (ty_of_interv i)
287
  in
288
289
  let infer t =
    Cil.CurrentLoc.set t.term_loc;
290
291
292
    (* 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. *)
293
    try
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
      match t.term_node with
      | TConst (LReal _) ->
        (* TODO: real: irrationals raise not_yet *)
        dup real
      | TConst (Integer _ | LChr _ | LEnum _)
      | TSizeOf _
      | TSizeOfStr _
      | TAlignOf _ ->
        let ty =
          try
            let i = Interval.infer t in
            ty_of_interv ?ctx i
          with Interval.Not_a_number ->
            nan
        in
        dup ty
      | TLval tlv ->
        let ty =
          try
            let i = Interval.infer t in
            ty_of_interv ?ctx i
          with
316
          | Interval.Not_a_number -> nan
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
          | Interval.Is_a_real -> real
        in
        type_term_lval tlv;
        dup ty

      | Toffset(_, t')
      | Tblock_length(_, t')
      | TSizeOfE t'
      | TAlignOfE t' ->
        let ty =
          try
            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');
            ty_of_interv ?ctx i
          with Interval.Not_a_number ->
            assert false (* this term is an integer *)
        in
        dup ty

      | TBinOp (MinusPP, t1, t2) ->
        let ty =
          try
            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);
            ty_of_interv ?ctx i
          with Interval.Not_a_number ->
            assert false (* this term is an integer *)
        in
        dup ty

      | TUnOp (unop, t') ->
        let ctx_res, ctx =
          try
            let i = Interval.infer t in
            let i' = Interval.infer t' in
            compute_ctx ?ctx (Ival.join i i')
          with
357
358
359
          | Interval.Not_a_number ->
            assert false (* only Is_a_real could be raised *)
          | Interval.Is_a_real ->
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
            real, real
        in
        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)
        ->
        let ctx_res, ctx =
          try
            let i = Interval.infer t in
            let i1 = Interval.infer t1 in
            let i2 = Interval.infer t2 in
            compute_ctx ?ctx (Ival.join i (Ival.join i1 i2))
          with
376
          | Interval.Is_a_real ->
377
            dup real
378
379
          | Interval.Not_a_number ->
            assert false (* only Is_a_real could be raised *)
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
        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);
        let ctx =
          try
            let i1 = Interval.infer t1 in
            let i2 = Interval.infer t2 in
            mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Ival.join i1 i2))
          with
404
          | Interval.Is_a_real ->
405
            real
406
407
          | Interval.Not_a_number ->
            nan
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
        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
          | Real | Gmpz | C_type _ -> ctx
        in
        c_int, ty

      | TBinOp ((LAnd | LOr), t1, t2) ->
        let ty =
          try
            let i1 = Interval.infer t1 in
            let i2 = Interval.infer t2 in
            ty_of_interv ?ctx (Ival.join i1 i2)
          with Interval.Not_a_number ->
            nan
        in
        (* 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') ->
        let ctx =
          try
            (* 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. *)
            ty_of_interv ?ctx i
          with
444
          | Interval.Not_a_number -> nan
445
446
447
448
          | Interval.Is_a_real -> real
        in
        ignore (type_term ~use_gmp_opt:true ~ctx t');
        dup ctx
449

450
451
452
      | Tif (t1, t2, t3) ->
        let ctx1 =
          mk_ctx ~use_gmp_opt:false c_int (* an int must be generated *)
453
        in
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
        ignore (type_term ~use_gmp_opt:false ~ctx:ctx1 t1);
        let i = Interval.infer t in
        let ctx =
          try
            let i2 = Interval.infer t2 in
            let i3 = Interval.infer t3 in
            let ctx = ty_of_interv ?ctx (Ival.join i (Ival.join i2 i3)) in
            mk_ctx ~use_gmp_opt:true ctx
          with Interval.Not_a_number ->
            nan
        in
        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;
        dup nan

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

      | TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
        (* both [t1] and [t2] must be typed. *)
        ignore (type_term ~use_gmp_opt:true ~ctx:nan t1);
        let ctx = offset_ty t2 in
        ignore (type_term ~use_gmp_opt:false ~ctx t2);
        dup nan

      | 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)
          in
          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 ->
                match lty with
                | Linteger ->
                  let i = Interval.infer t in
                  if Options.Gmp_only.get () then dup Gmpz
                  else dup (ty_of_interv i)
                | Ctype TInt(ik, _ ) ->
                  dup (C_type ik)
                | Ctype TFloat _ -> (* TODO: handle in MR !226 *)
                  (* TODO RATIONAL: re-implement this case *)
                  assert false (* dup Other *)
                | Lreal ->
                  (* TODO RATIONAL: implement this case *)
                  Error.not_yet "real numbers"
                | Ctype _ ->
                  (* TODO RATIONAL: re-implement this case *)
                  assert false (* dup Other *)
                | Ltype _ | Lvar _ | Larrow _ ->
                  Options.fatal "unexpected type"
            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"
      | Trange(Some n1, Some n2) ->
        ignore (type_term ~use_gmp_opt n1);
        ignore (type_term ~use_gmp_opt n2);
        let i = Interval.infer t in
        let ty = ty_of_interv ?ctx i in
        dup ty
      | Trange(None, _) | Trange(_, None) ->
        Options.abort "unbounded ranges are not part of E-ACSl"
      | Tlet(li, t) ->
        infer_if_integer li;
        let li_t = Misc.term_of_li li in
        ignore (type_term ~use_gmp_opt:true li_t);
        dup (type_term ~use_gmp_opt:true ?ctx t).ty
      | Tlambda (_,_) -> Error.not_yet "lambda"
      | TDataCons (_,_) -> Error.not_yet "datacons"
      | TUpdate (_,_,_) -> Error.not_yet "update"

      | Tnull
      | TConst (LStr _ | LWStr _)
      | Ttypeof _
      | Ttype _
      | Tempty_set  -> dup nan
Julien Signoles's avatar
Julien Signoles committed
571

572
    with Interval.Is_a_real ->
573
      (* TODO RATIONAL: I do not like such a try with *)
574
      Error.not_yet "reals: typing: term using unsupported construct"
575
  in
576
577
  Memo.memo
    (fun t ->
578
579
580
581
       let ty, op = infer t in
       match ctx with
       | None -> { ty; op; cast = None }
       | Some ctx -> coerce ~arith_operand ~ctx ~op ty)
582
    t
583

584
585
586
and type_term_lval (host, offset) =
  type_term_lhost host;
  type_term_offset offset
587

588
and type_term_lhost = function
589
590
  | TVar _
  | TResult _ -> ()
591
  | TMem t -> ignore (type_term ~use_gmp_opt:false ~ctx:nan t)
592

593
and type_term_offset = function
594
595
  | TNoOffset -> ()
  | TField(_, toff)
596
  | TModel(_, toff) -> type_term_offset toff
597
  | TIndex(t, toff) ->
598
    let ctx = offset_ty t in
599
    ignore (type_term ~use_gmp_opt:false ~ctx t);
600
    type_term_offset toff
601

602
603
let rec type_predicate p =
  Cil.CurrentLoc.set p.pred_loc;
604
  (* this pattern matching also follows the formal rules of the JFLA's paper *)
605
606
  let op =
    match p.pred_content with
607
    | Pfalse | Ptrue -> c_int
608
609
610
611
612
613
614
615
616
617
618
619
    | Papp(li, _, _) ->
      begin match li.l_body with
      | 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 *)
        Error.not_yet "logic functions with no definition nor reads clause"
      | LBreads _ | LBterm _ | LBinductive _ ->
        Options.fatal "unexpected logic definition"
      end
620
621
622
    | Pseparated _ -> Error.not_yet "\\separated"
    | Pdangling _ -> Error.not_yet "\\dangling"
    | Prel(_, t1, t2) ->
623
624
      let ctx =
        try
625
626
          let i1 = Interval.infer t1 in
          let i2 = Interval.infer t2 in
627
          let i = Ival.join i1 i2 in
628
          mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i)
629
630
        with
          | Interval.Not_a_number -> nan
631
          | Interval.Is_a_real -> real
632
      in
633
634
      ignore (type_term ~use_gmp_opt:true ~ctx t1);
      ignore (type_term ~use_gmp_opt:true ~ctx t2);
635
      (match ctx with
636
      | Nan -> c_int
637
      | Real | Gmpz | C_type _ -> ctx)
638
639
640
641
642
    | Pand(p1, p2)
    | Por(p1, p2)
    | Pxor(p1, p2)
    | Pimplies(p1, p2)
    | Piff(p1, p2) ->
643
644
      ignore (type_predicate p1);
      ignore (type_predicate p2);
645
646
      c_int
    | Pnot p ->
647
      ignore (type_predicate p);
648
649
      c_int
    | Pif(t, p1, p2) ->
650
651
      let ctx = mk_ctx ~use_gmp_opt:false c_int in
      ignore (type_term ~use_gmp_opt:false ~ctx t);
652
653
      ignore (type_predicate p1);
      ignore (type_predicate p2);
654
      c_int
655
656
657
658
659
    | Plet(li, p) ->
      infer_if_integer li;
      let li_t = Misc.term_of_li li in
      ignore (type_term ~use_gmp_opt:true li_t);
      (type_predicate p).ty
660

661
662
    | Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) })
    | Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
663
      let guards = !compute_quantif_guards_ref p bounded_vars hyps in
664
665
666
667
      List.iter
        (fun (t1, r1, x, r2, t2) ->
          let i1 = Interval.infer t1 in
          let i1 = match r1 with
668
            | Rlt -> Ival.add_singleton_int Integer.one i1
669
670
671
672
            | Rle -> i1
            | _ -> assert false
          in
          let i2 = Interval.infer t2 in
673
674
          (* add one to [i2], since we increment the loop counter one more
             time before going outside the loop. *)
675
676
          let i2 = match r2 with
            | Rlt -> i2
677
            | Rle -> Ival.add_singleton_int Integer.one i2
678
679
            | _ -> assert false
          in
680
          let i = Ival.join i1 i2 in
681
          let ctx = match x.lv_type with
682
            | Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i)
683
684
            | Ctype ty ->
              (match Cil.unrollType ty with
685
              | TInt(ik, _) -> mk_ctx ~use_gmp_opt:true (C_type ik)
686
              | ty ->
687
                Options.fatal "unexpected type %a for quantified variable %a"
688
689
690
691
692
693
694
                  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
695
696
          (* forcing when typing bounds prevents to generate an extra useless
             GMP variable when --e-acsl-gmp-only *)
697
698
          ignore (type_term ~use_gmp_opt:false ~ctx t1);
          ignore (type_term ~use_gmp_opt:false ~ctx t2);
699
700
701
702
          (* 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_type _ -> i
703
704
            | Gmpz -> Ival.inject_range None None (* [ -\infty; +\infty ] *)
            | Nan -> assert false
705
            | Real -> Error.not_yet "reals: quantification"
706
          in
707
708
          Interval.Env.add x i)
        guards;
709
      (type_predicate goal).ty
710
711
712
713
714
715
716

    | Pinitialized(_, t)
    | Pfreeable(_, t)
    | Pallocable(_, t)
    | Pvalid(_, t)
    | Pvalid_read(_, t)
    | Pvalid_function t ->
717
      ignore (type_term ~use_gmp_opt:false ~ctx:nan t);
718
      c_int
719
720
721

    | Pforall _ -> Error.not_yet "unguarded \\forall quantification"
    | Pexists _ -> Error.not_yet "unguarded \\exists quantification"
722
    | Pat(p, _) -> (type_predicate p).ty
723
724
    | Pfresh _ -> Error.not_yet "\\fresh"
  in
725
  coerce ~arith_operand:false ~ctx:c_int ~op c_int
726

727
let type_term ~use_gmp_opt ?ctx t =
728
  Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
729
    Printer.pp_term t (Pretty_utils.pp_opt D.pretty) ctx;
730
  ignore (type_term ~use_gmp_opt ?ctx t)
731

732
let type_named_predicate ?(must_clear=true) p =
733
  Options.feedback ~dkey ~level:3 "typing predicate '%a'."
734
    Printer.pp_predicate p;
735
736
737
738
  if must_clear then begin
    Interval.Env.clear ();
    Memo.clear ()
  end;
739
  ignore (type_predicate p)
740

741
742
743
744
745
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)

746
(******************************************************************************)
747
(** {2 Getters} *)
748
749
(******************************************************************************)

750
let get_number_ty t = (Memo.get t).ty
751
let get_integer_op t = (Memo.get t).op
752
let get_integer_op_of_predicate p = (type_predicate p).op
753

754
(* {!typ_of_integer}, but handle the not-integer cases. *)
755
let extract_typ t ty =
756
757
  try typ_of_number_ty ty
  with Not_a_number ->
758
    let lty = t.term_type in
759
    match lty with
760
761
762
    | Ctype _ ->
      Logic_utils.logicCType lty
    | Lreal ->
763
      Real.t ()
764
    | Ltype _ | Lvar _ | Linteger | Larrow _ ->
765
766
767
      if Cil.isLogicRealType lty then TFloat(FLongDouble, [])
      else if Cil.isLogicFloatType lty then  Logic_utils.logicCType lty
      else Error.not_yet "unsupported logic type"
768

769
770
let get_typ t =
  let info = Memo.get t in
771
  extract_typ t info.ty
772

773
774
let get_op t =
  let info = Memo.get t in
775
  extract_typ t info.op
776

777
778
let get_cast t =
  let info = Memo.get t in
779
780
  try Extlib.opt_map typ_of_number_ty info.cast
  with Not_a_number -> None
781
782

let get_cast_of_predicate p =
783
  let info = type_predicate p in
784
785
  try Extlib.opt_map typ_of_number_ty info.cast
  with Not_a_number -> assert false
786
787

let clear = Memo.clear
788

789
790
module Datatype = D

791
792
793
794
795
(*
Local Variables:
compile-command: "make"
End:
*)