typing.ml 23.3 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
Virgile Prevosto's avatar
Virgile Prevosto committed
3
(*  This file is part of Frama-C.                                         *)
4
(*                                                                        *)
Virgile Prevosto's avatar
Virgile Prevosto committed
5
6
(*  Copyright (C) 2007-2017                                               *)
(*    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
40
41
(******************************************************************************)

type integer_ty =
  | Gmp
  | C_type of ikind
42
43
  | Other

44
45
46
let gmp = Gmp
let c_int = C_type IInt
let ikind ik = C_type ik
47
let other = Other
48

49
50
51
include Datatype.Make
(struct
  type t = integer_ty
52
  let name = "E_ACSL.New_typing.t"
53
54
55
56
57
58
59
  let reprs = [ Gmp; c_int ]
  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
60
61
62
    | (Other | C_type _), Gmp | Other, C_type _ -> -1
    | Gmp, (C_type _ | Other) | C_type _, Other -> 1
    | Gmp, Gmp | Other, Other -> 0
63
64
65
66

  let equal = Datatype.from_compare

  let pretty fmt = function
67
    | Gmp -> Format.pp_print_string fmt "GMP"
68
    | C_type k -> Printer.pp_ikind fmt k
69
    | Other -> Format.pp_print_string fmt "OTHER"
70
71
 end)

72
73
74
75
(******************************************************************************)
(** Basic operations *)
(******************************************************************************)

76
77
78
79
80
81
82
83
let join ty1 ty2 = match ty1, ty2 with
  | Other, Other -> Other
  | Other, (Gmp | C_type _) | (Gmp | C_type _), Other ->
    Options.fatal "[typing] join failure: integer and non integer type"
  | Gmp, _ | _, Gmp -> Gmp
  | C_type i1, C_type i2 ->
    if Options.Gmp_only.get () then Gmp
    else
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
      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

exception Not_an_integer
let typ_of_integer_ty = function
  | Gmp -> Gmpz.t ()
  | C_type ik -> TInt(ik, [])
  | Other -> raise Not_an_integer

(******************************************************************************)
(** Memoization *)
(******************************************************************************)

101
102
type computed_info =
    { ty: t;  (* type required for the term *)
103
      op: t; (* type required for the operation *)
104
105
106
107
      cast: t option; (* if not [None], type of the context which the term
                         must be casted to. If [None], no cast needed. *)
    }

108
109
(* Memoization module which retrieves the computed info of some terms. If the
   info is already computed for a term, it is never recomputed *)
110
111
112
113
114
115
116
117
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
118
119
120
121
122
123
124
125
126
127
128
129
130
    (* 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. *)
131
132
133
134
135
136
137
138
139
    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 ->
140
141
142
      Options.fatal
        "[typing] type of term '%a' was never computed."
        Printer.pp_term t
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158

  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
159
160
161
162
163
164
165
166
167
let ty_of_logic_ty = function
  | Linteger -> Gmp
  | Ctype ty -> (match Cil.unrollType ty with
    | TInt(ik, _) -> C_type ik
    | _ -> Other)
  | Lreal | Larrow _ -> Other
  | Ltype _ -> Error.not_yet "user-defined logic type"
  | Lvar _ -> Error.not_yet "type variable"

168
169
(* Compute the smallest type (bigger than [int]) which can contain the whole
   interval. It is the \theta operator of the JFLA's paper. *)
170
let ty_of_interv ?ctx i =
171
  try
172
173
174
175
176
177
178
179
180
    let itv_kind =
      if Ival.is_bottom i then IInt
      else match Ival.min_and_max i with
        | Some l, Some u ->
          let is_pos = Integer.ge l Integer.zero in
          let lkind = Cil.intKindForValue l is_pos in
          let ukind = Cil.intKindForValue u is_pos in
          (* kind corresponding to the interval *)
          if Cil.intTypeIncluded lkind ukind then ukind else lkind
181
182
183
        | None, None -> raise Cil.Not_representable (* GMP *)
        | None, Some _ | Some _, None ->
          Kernel.fatal ~current:true "ival: %a" Ival.pretty i
184
    in
185
186
    (* convert the kind to [IInt] whenever smaller. *)
    let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
187
    (* ctx type whenever possible to prevent superfluous casts in the generated
188
       code *)
189
    (match ctx with
190
191
192
     | None | Some (Gmp | Other) -> C_type kind
     | Some (C_type ik as ctx) ->
       if Cil.intTypeIncluded itv_kind ik then ctx else C_type kind)
193
194
195
  with Cil.Not_representable ->
    Gmp

196
197
(* compute a new {!computed_info} by coercing the given type [ty] to the given
   context [ctx]. [op] is the type for the operator. *)
198
let coerce ~arith_operand ~ctx ~op ty =
199
200
201
  if compare ty ctx = 1 then begin
    (* type larger than the expected context,
       so we must introduce an explicit cast *)
202
    { ty; op; cast = Some ctx }
203
  end else
204
205
206
207
208
209
    (* 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
       operation which must be explicitely coerced in order to force the
       operation to be of the expected type. *)
    if (ctx = Gmp && ty <> Gmp) || arith_operand
    then { ty; op; cast = Some ctx }
210
    else { ty; op; cast = None }
211

212
213
214
215
216
217
218
219
220
221
222
223
(* the integer_ty corresponding to [t] whenever use as an offset.
   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
    | Gmp -> C_type ILongLong (* largest possible type *)
    | ty -> ty
  with Interval.Not_an_integer ->
    Options.fatal "expected an integral type for %a" Printer.pp_term t

224
(******************************************************************************)
225
(** {2 Type system} *)
226
227
(******************************************************************************)

228
229
230
231
232
(* generate a context [c]. Take --e-acsl-gmp-only into account iff [use_gmp_opt]
   is true. *)
let mk_ctx ~use_gmp_opt = function
  | Other | Gmp as c -> c
  | C_type _ as c -> if use_gmp_opt && Options.Gmp_only.get () then Gmp else c
233

234
235
(* type the term [t] in a context [ctx] by taking --e-acsl-gmp-only into account
   iff [use_gmp_opt] is true. *)
236
237
let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
  let ctx = Extlib.opt_map (mk_ctx ~use_gmp_opt) ctx in
238
  let dup ty = ty, ty in
239
240
241
242
243
244
245
  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 *)
246
      dup (mk_ctx ~use_gmp_opt:true (ty_of_interv i))
247
    | Some ctx ->
248
249
      mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx i),
      mk_ctx ~use_gmp_opt:true (ty_of_interv i)
250
  in
251
252
  let infer t =
    Cil.CurrentLoc.set t.term_loc;
253
254
255
    (* 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. *)
256
    match t.term_node with
257
    | TConst (Integer _ | LChr _ | LEnum _)
258
259
    | TSizeOf _
    | TSizeOfStr _
260
    | TAlignOf _ ->
261
262
      let ty =
        try
263
          let i = Interval.infer t in
264
          ty_of_interv ?ctx i
265
266
267
268
        with Interval.Not_an_integer ->
          Other
      in
      dup ty
269
    | TLval tlv ->
270
271
      let ty =
        try
272
          let i = Interval.infer t in
273
          ty_of_interv ?ctx i
274
275
276
        with Interval.Not_an_integer ->
          Other
      in
277
      type_term_lval tlv;
278
      dup ty
279

280
    | Toffset(_, t')
281
282
283
    | Tblock_length(_, t')
    | TSizeOfE t'
    | TAlignOfE t' ->
284
285
      let ty =
        try
286
          let i = Interval.infer t in
287
          (* [t'] must be typed, but it is a pointer *)
288
          ignore (type_term ~use_gmp_opt:true ~ctx:Other t');
289
          ty_of_interv ?ctx i
290
        with Interval.Not_an_integer ->
291
          assert false (* this term is an integer *)
292
293
      in
      dup ty
294
295

    | TBinOp (MinusPP, t1, t2) ->
296
297
      let ty =
        try
298
          let i = Interval.infer t in
299
          (* [t1] and [t2] must be typed, but they are pointers *)
300
301
          ignore (type_term ~use_gmp_opt:true ~ctx:Other t1);
          ignore (type_term ~use_gmp_opt:true ~ctx:Other t2);
302
          ty_of_interv ?ctx i
303
        with Interval.Not_an_integer ->
304
          assert false (* this term is an integer *)
305
306
307
308
      in
      dup ty

    | TUnOp (unop, t') ->
309
      let ctx_res, ctx =
310
        try
311
312
          let i = Interval.infer t in
          let i' = Interval.infer t' in
313
          compute_ctx ?ctx (Ival.join i i')
314
        with Interval.Not_an_integer ->
315
          dup Other (* real *)
316
      in
317
      ignore (type_term ~use_gmp_opt:true ~arith_operand:true ~ctx t');
318
      (match unop with
319
320
      | LNot -> c_int, ctx_res (* converted into [t == 0] in case of GMP *)
      | Neg | BNot -> dup ctx_res)
321
322

    | TBinOp((PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt), t1, t2) ->
323
      let ctx_res, ctx =
324
        try
325
326
327
          let i = Interval.infer t in
          let i1 = Interval.infer t1 in
          let i2 = Interval.infer t2 in
328
          compute_ctx ?ctx (Ival.join i (Ival.join i1 i2))
329
        with Interval.Not_an_integer ->
330
          dup Other (* real *)
331
      in
332
333
334
335
336
337
338
339
340
341
      (* it is enough to explicitely 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
342
343
344
      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);
345
      dup ctx_res
346

347
    | TBinOp ((Lt | Gt | Le | Ge | Eq | Ne), t1, t2) ->
348
      assert (match ctx with None -> true | Some c -> compare c c_int >= 0);
349
350
      let ctx =
        try
351
352
          let i1 = Interval.infer t1 in
          let i2 = Interval.infer t2 in
353
          mk_ctx ~use_gmp_opt:true (ty_of_interv ?ctx (Ival.join i1 i2))
354
355
356
        with Interval.Not_an_integer ->
          Other
      in
357
358
      ignore (type_term ~use_gmp_opt:true ~ctx t1);
      ignore (type_term ~use_gmp_opt:true ~ctx t2);
359
      let ty = match ctx with
360
361
        | Other -> c_int
        | Gmp | C_type _ -> ctx
362
      in
363
364
      c_int, ty

365
    | TBinOp ((LAnd | LOr), t1, t2) ->
366
      let ty =
367
        try
368
369
          let i1 = Interval.infer t1 in
          let i2 = Interval.infer t2 in
370
          ty_of_interv ?ctx (Ival.join i1 i2)
371
372
        with Interval.Not_an_integer ->
          Other
373
      in
374
      (* both operands fit in an int. *)
375
376
      ignore (type_term ~use_gmp_opt:true ~ctx:c_int t1);
      ignore (type_term ~use_gmp_opt:true ~ctx:c_int t2);
377
      dup ty
378
379
380
381
382

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

383
384
    | TCastE(_, t')
    | TCoerce(t', _) ->
385
      let ctx =
386
        try
387
388
          (* compute the smallest interval from the whole term [t] *)
          let i = Interval.infer t in
389
          (* nothing more to do: [i] is already more precise than what we
390
             could infer from the arguments of the cast. *)
391
          ty_of_interv ?ctx i
392
393
394
        with Interval.Not_an_integer ->
          Other
      in
395
      ignore (type_term ~use_gmp_opt:true ~ctx t');
396
      dup ctx
397
398

    | Tif (t1, t2, t3) ->
399
400
401
402
      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);
403
      let i = Interval.infer t in
404
405
      let ctx =
        try
406
407
          let i2 = Interval.infer t2 in
          let i3 = Interval.infer t3 in
408
          let ctx = ty_of_interv ?ctx (Ival.join i (Ival.join i2 i3)) in
409
          mk_ctx ~use_gmp_opt:true ctx
410
411
        with Interval.Not_an_integer ->
          Other
412
      in
413
414
      ignore (type_term ~use_gmp_opt:true ~ctx t2);
      ignore (type_term ~use_gmp_opt:true ~ctx t3);
415
      dup ctx
416
417

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

421
    | TCoerceE (t1, t2) ->
422
423
      let ctx =
        try
424
425
426
          let i = Interval.infer t in
          let i1 = Interval.infer t1 in
          let i2 = Interval.infer t2 in
427
          ty_of_interv ?ctx (Ival.join i (Ival.join i1 i2))
428
429
        with Interval.Not_an_integer ->
          Other
430
      in
431
432
      ignore (type_term ~use_gmp_opt:true ~ctx t1);
      ignore (type_term ~use_gmp_opt:true ~ctx t2);
433
      dup ctx
434

435
436
    | TAddrOf tlv
    | TStartOf tlv ->
437
      (* it is a pointer, but subterms must be typed. *)
438
      type_term_lval tlv;
439
      dup Other
440
441

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

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

Julien Signoles's avatar
Julien Signoles committed
453
454
455
    | Tapp(li, _, args) ->
      let typ_arg lvi arg =
        let ctx = ty_of_logic_ty lvi.lv_type in
456
        ignore (type_term ~use_gmp_opt:false ~ctx arg)
Julien Signoles's avatar
Julien Signoles committed
457
458
459
460
461
462
      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))

463
464
465
466
467
    | Tunion _ -> Error.not_yet "tset union"
    | Tinter _ -> Error.not_yet "tset intersection"
    | Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
    | Trange (_,_) -> Error.not_yet "trange"
    | Tlet (_,_) -> Error.not_yet "let binding"
468
469
470
    | Tlambda (_,_) -> Error.not_yet "lambda"
    | TDataCons (_,_) -> Error.not_yet "datacons"
    | TUpdate (_,_,_) -> Error.not_yet "update"
471

472
473
    | Tnull
    | TConst (LStr _ | LWStr _ | LReal _)
474
475
    | Ttypeof _
    | Ttype _
476
    | Tempty_set  -> dup Other
477
  in
478
479
480
481
482
  Memo.memo
    (fun t ->
      let ty, op = infer t in
      match ctx with
      | None -> { ty; op; cast = None }
483
      | Some ctx -> coerce ~arith_operand ~ctx ~op ty)
484
    t
485

486
487
488
and type_term_lval (host, offset) =
  type_term_lhost host;
  type_term_offset offset
489

490
and type_term_lhost = function
491
492
  | TVar _
  | TResult _ -> ()
493
  | TMem t -> ignore (type_term ~use_gmp_opt:false ~ctx:Other t)
494

495
and type_term_offset = function
496
497
  | TNoOffset -> ()
  | TField(_, toff)
498
  | TModel(_, toff) -> type_term_offset toff
499
  | TIndex(t, toff) ->
500
    let ctx = offset_ty t in
501
    ignore (type_term ~use_gmp_opt:false ~ctx t);
502
    type_term_offset toff
503

504
505
let rec type_predicate p =
  Cil.CurrentLoc.set p.pred_loc;
506
  (* this pattern matching also follows the formal rules of the JFLA's paper *)
507
  let op = match p.pred_content with
508
509
510
511
512
    | Pfalse | Ptrue -> c_int
    | Papp _ -> Error.not_yet "logic function application"
    | Pseparated _ -> Error.not_yet "\\separated"
    | Pdangling _ -> Error.not_yet "\\dangling"
    | Prel(_, t1, t2) ->
513
514
      let ctx =
        try
515
516
          let i1 = Interval.infer t1 in
          let i2 = Interval.infer t2 in
517
          let i = Ival.join i1 i2 in
518
          mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:c_int i)
519
520
521
        with Interval.Not_an_integer ->
          Other
      in
522
523
      ignore (type_term ~use_gmp_opt:true ~ctx t1);
      ignore (type_term ~use_gmp_opt:true ~ctx t2);
524
525
526
      (match ctx with
      | Other -> c_int
      | Gmp | C_type _ -> ctx)
527
528
529
530
531
    | Pand(p1, p2)
    | Por(p1, p2)
    | Pxor(p1, p2)
    | Pimplies(p1, p2)
    | Piff(p1, p2) ->
532
533
      ignore (type_predicate p1);
      ignore (type_predicate p2);
534
535
      c_int
    | Pnot p ->
536
      ignore (type_predicate p);
537
538
      c_int
    | Pif(t, p1, p2) ->
539
540
      let ctx = mk_ctx ~use_gmp_opt:false c_int in
      ignore (type_term ~use_gmp_opt:false ~ctx t);
541
542
      ignore (type_predicate p1);
      ignore (type_predicate p2);
543
544
      c_int
    | Plet _ -> Error.not_yet "let _ = _ in _"
545

546
547
    | Pforall(bounded_vars, { pred_content = Pimplies(hyps, goal) })
    | Pexists(bounded_vars, { pred_content = Pand(hyps, goal) }) ->
548
      let guards = !compute_quantif_guards_ref p bounded_vars hyps in
549
550
551
552
      List.iter
        (fun (t1, r1, x, r2, t2) ->
          let i1 = Interval.infer t1 in
          let i1 = match r1 with
553
            | Rlt -> Ival.add_singleton_int Integer.one i1
554
555
556
557
            | Rle -> i1
            | _ -> assert false
          in
          let i2 = Interval.infer t2 in
558
559
          (* add one to [i2], since we increment the loop counter one more
             time before going outside the loop. *)
560
561
          let i2 = match r2 with
            | Rlt -> i2
562
            | Rle -> Ival.add_singleton_int Integer.one i2
563
564
            | _ -> assert false
          in
565
          let i = Ival.join i1 i2 in
566
          let ctx = match x.lv_type with
567
            | Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmp i)
568
569
            | Ctype ty ->
              (match Cil.unrollType ty with
570
              | TInt(ik, _) -> mk_ctx ~use_gmp_opt:true (C_type ik)
571
              | ty ->
572
                Options.fatal "unexpected type %a for quantified variable %a"
573
574
575
576
577
578
579
                  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
580
581
          (* forcing when typing bounds prevents to generate an extra useless
             GMP variable when --e-acsl-gmp-only *)
582
583
          ignore (type_term ~use_gmp_opt:false ~ctx t1);
          ignore (type_term ~use_gmp_opt:false ~ctx t2);
584
585
586
587
588
589
590
          (* 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
            | Gmp -> Ival.inject_range None None (* [ -\infty; +\infty ] *)
            | Other -> assert false
          in
591
592
          Interval.Env.add x i)
        guards;
593
      (type_predicate goal).ty
594
595
596
597
598
599
600

    | Pinitialized(_, t)
    | Pfreeable(_, t)
    | Pallocable(_, t)
    | Pvalid(_, t)
    | Pvalid_read(_, t)
    | Pvalid_function t ->
601
      ignore (type_term ~use_gmp_opt:false ~ctx:Other t);
602
      c_int
603
604
605

    | Pforall _ -> Error.not_yet "unguarded \\forall quantification"
    | Pexists _ -> Error.not_yet "unguarded \\exists quantification"
606
    | Pat(p, _) -> (type_predicate p).ty
607
608
609
    | Pfresh _ -> Error.not_yet "\\fresh"
    | Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
  in
610
  coerce ~arith_operand:false ~ctx:c_int ~op c_int
611

612
let type_term ~use_gmp_opt ?ctx t =
613
  Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
614
    Printer.pp_term t (Pretty_utils.pp_opt pretty) ctx;
615
  ignore (type_term ~use_gmp_opt ?ctx t)
616

617
let type_named_predicate ?(must_clear=true) p =
618
  Options.feedback ~dkey ~level:3 "typing predicate '%a'."
619
    Printer.pp_predicate p;
620
621
622
623
  if must_clear then begin
    Interval.Env.clear ();
    Memo.clear ()
  end;
624
  ignore (type_predicate p)
625

626
627
628
629
630
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)

631
(******************************************************************************)
632
(** {2 Getters} *)
633
634
(******************************************************************************)

635
636
let get_integer_ty t = (Memo.get t).ty
let get_integer_op t = (Memo.get t).op
637
let get_integer_op_of_predicate p = (type_predicate p).op
638

639
(* {!typ_of_integer}, but handle the not-integer cases. *)
640
641
642
let extract_typ t ty =
  try typ_of_integer_ty ty
  with Not_an_integer ->
643
644
645
646
647
648
649
650
    let lty = t.term_type in
    if Cil.isLogicRealType lty then TFloat(FLongDouble, [])
    else if Cil.isLogicFloatType lty then Logic_utils.logicCType lty
    else
      Kernel.fatal "unexpected types %a and %a for term %a"
        Printer.pp_logic_type lty
        pretty ty
        Printer.pp_term t
651

652
653
let get_typ t =
  let info = Memo.get t in
654
  extract_typ t info.ty
655

656
657
let get_op t =
  let info = Memo.get t in
658
  extract_typ t info.op
659

660
661
let get_cast t =
  let info = Memo.get t in
662
663
  try Extlib.opt_map typ_of_integer_ty info.cast
  with Not_an_integer -> None
664
665

let get_cast_of_predicate p =
666
  let info = type_predicate p in
667
668
  try Extlib.opt_map typ_of_integer_ty info.cast
  with Not_an_integer -> assert false
669
670

let clear = Memo.clear
671
672
673
674
675
676

(*
Local Variables:
compile-command: "make"
End:
*)