translate.ml 40.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
(*                                                                        *)
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).            *)
Julien Signoles's avatar
Julien Signoles committed
20
(*                                                                        *)
21
22
(**************************************************************************)

23
module E_acsl_label = Label
24
25
26
open Cil_types
open Cil_datatype

27
28
let dkey = Options.dkey_translation

29
30
31
32
33
34
35
36
let not_yet env s =
  Env.Context.save env;
  Error.not_yet s

let handle_error f env =
  let env = Error.handle f env in
  Env.Context.restore env

37
(* internal to [named_predicate_to_exp] but put it outside in order to not add
38
   extra tedious parameter.
39
40
41
   It is [true] iff we are currently visiting \valid. *)
let is_visiting_valid = ref false

42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
(* ************************************************************************** *)
(* Transforming terms and predicates into C expressions (if any) *)
(* ************************************************************************** *)

let relation_to_binop = function
  | Rlt -> Lt
  | Rgt -> Gt
  | Rle -> Le
  | Rge -> Ge
  | Req -> Eq
  | Rneq -> Ne

let name_of_mpz_arith_bop = function
  | PlusA -> "__gmpz_add"
  | MinusA -> "__gmpz_sub"
  | Mult -> "__gmpz_mul"
  | Div -> "__gmpz_tdiv_q"
  | Mod -> "__gmpz_tdiv_r"
  | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
  | Shiftlt | Shiftrt | PlusPI | IndexPI | MinusPI | MinusPP -> assert false

63
64
65
66
67
68
69
(* Type of a string that represents a number.
   Used when a string is required to encode a constant number because it is not
   representable in any C type  *)
type strnum =
  | Str_Z         (* integers *)
  | Str_R         (* reals *)
  | C_number      (* integers AND floats) included *)
70

71
(* convert [e] in a way that it is compatible with the given typing context. *)
72
let add_cast ~loc ?name env ctx strnum t_opt e =
73
  let mk_mpz e =
Julien Signoles's avatar
Julien Signoles committed
74
75
76
77
78
79
80
81
    let _, e, env =
      Env.new_var
        ~loc
        ?name
        env
        t_opt
        (Gmp.Z.t ())
        (fun lv v -> [ Gmp.init_set ~loc (Cil.var lv) v e ])
82
83
84
    in
    e, env
  in
85
  let e, env = match strnum with
Julien Signoles's avatar
Julien Signoles committed
86
    (* TODO RATIONAL: make this matching consistent *)
87
88
89
    | Str_Z -> mk_mpz e
    | Str_R -> Real.mk_real ~loc ?name e env t_opt
    | C_number -> e, env
90
  in
91
  match ctx with
92
93
  | None ->
    e, env
94
95
  | Some ctx ->
    let ty = Cil.typeOf e in
Julien Signoles's avatar
Julien Signoles committed
96
97
98
    (* TODO RATIONAL:
       spaghetti code below. Would be nice to be improved (or at least
       more commented) ==> boolean pattern matching? *)
99
100
    if Gmp.Z.is_t ctx then
      if Gmp.Z.is_t ty then
101
        e, env
102
103
      else if Real.is_t ty then
        Real.cast_to_z ~loc ?name e env
104
105
      else
        (* Convert the C integer into a mpz.
Julien Signoles's avatar
Julien Signoles committed
106
107
108
           Remember:
           - very long constants have been temporary converted into strings;
           - possible to get a non integral type (or Gmp.z_t) with a non-one in
109
110
           the case of \null *)
        let e =
111
          if Cil.isIntegralType ty || strnum = Str_Z then
112
            e
113
          else if not (Cil.isIntegralType ty) && strnum = C_number then
114
            Cil.mkCast e Cil.longType (* \null *)
Julien Signoles's avatar
Julien Signoles committed
115
          else begin
Julien Signoles's avatar
Julien Signoles committed
116
117
118
            (* TODO RATIONAL: this case seems to be possible:
               getting a very long rational constants (so a string) to be casted
               to an integer *)
Julien Signoles's avatar
Julien Signoles committed
119
120
121
            assert (not (Cil.isIntegralType ty) && strnum = Str_R);
            assert false
          end
122
123
        in
        mk_mpz e
124
125
126
    else if Real.is_t ctx then
      if Real.is_t (Cil.typeOf e) then e, env
      else Real.mk_real ~loc ?name e env t_opt
127
128
    else
      (* handle a C-integer context *)
129
      if Gmp.Z.is_t ty || strnum = Str_Z then
130
131
        (* we get an mpz, but it fits into a C integer: convert it *)
        let fname, new_ty =
132
          if Cil.isSignedInteger ctx then
133
134
135
136
137
138
139
140
141
142
143
144
145
146
            "__gmpz_get_si", Cil.longType
          else
            "__gmpz_get_ui", Cil.ulongType
        in
        let _, e, env =
          Env.new_var
            ~loc
            ?name
            env
            None
            new_ty
            (fun v _ -> [ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e ] ])
        in
        e, env
147
      else if Real.is_t ty || strnum = Str_R then
148
        Real.add_cast ~loc ?name e env ctx
149
      else
150
        Cil.mkCastT ~force:false ~e ~oldt:ty ~newt:ctx, env
151

152
153
let constant_to_exp ~loc t c =
  let mk_real s =
154
    let s = Real.normalize_str s in
155
    Cil.mkString ~loc s, Str_R
156
157
  in
  match c with
158
  | Integer(n, _repr) ->
159
    (try
160
       let ity = Typing.get_number_ty t in
161
       match ity with
162
163
       | Typing.Nan ->
         assert false
164
       | Typing.Real ->
Julien Signoles's avatar
Julien Signoles committed
165
166
167
         (* TODO RATIONAL:
            - is it possible?
            - why converting the integer to a string? *)
168
169
170
         mk_real (Integer.to_string n)
       | Typing.Gmpz ->
         raise Cil.Not_representable
171
172
       | Typing.C_type kind ->
         let cast = Typing.get_cast t in
173
         match cast, kind with
Julien Signoles's avatar
Julien Signoles committed
174
175
         (* TODO RATIONAL: why are the two first cases not the same?
            (exception vs builder) *)
176
         | Some ty, (ILongLong | IULongLong) when Gmp.Z.is_t ty ->
177
           raise Cil.Not_representable
178
         | Some ty, (ILongLong | IULongLong) when Real.is_t ty ->
179
           mk_real (Integer.to_string n)
180
181
182
183
184
185
186
         | (None | Some _), _ ->
           (* do not keep the initial string representation because the
              generated constant must reflect its type computed by the type
              system. For instance, when translating [INT_MAX+1], we must
              generate a [long long] addition and so [1LL]. If we keep the
              initial string representation, the kind would be ignored in the
              generated code and so [1] would be generated. *)
187
           Cil.kinteger64 ~loc ~kind n, C_number
188
     with Cil.Not_representable ->
189
       (* too big integer *)
190
191
192
193
194
195
       Cil.mkString ~loc (Integer.to_string n), Str_Z)
  | LStr s -> Cil.new_exp ~loc (Const (CStr s)), C_number
  | LWStr s -> Cil.new_exp ~loc (Const (CWStr s)), C_number
  | LChr c -> Cil.new_exp ~loc (Const (CChr c)), C_number
  | LReal {r_literal=s; r_nearest=_; r_lower=_; r_upper=_} -> mk_real s
  | LEnum e -> Cil.new_exp ~loc (Const (CEnum e)), C_number
196

197
let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
198
  let env = Env.pop (Env.pop env3) in
199
200
201
202
203
204
  match e1.enode with
  | Const(CInt64(n, _, _)) when Integer.is_zero n ->
    e3, Env.transfer ~from:env3 env
  | Const(CInt64(n, _, _)) when Integer.is_one n ->
    e2, Env.transfer ~from:env2 env
  | _ ->
205
206
    let ty = match t_opt with
      | None (* predicate *) -> Cil.intType
207
      | Some t -> Typing.get_typ t
208
    in
209
210
    let _, e, env =
      Env.new_var
211
212
213
214
215
216
217
        ~loc
        ~name
        env
        t_opt
        ty
        (fun v ev ->
          let lv = Cil.var v in
218
219
          let ty = Cil.typeOf ev in
          let init_set =
Julien Signoles's avatar
Julien Signoles committed
220
            (* TODO RATIONAL: how is it possible to get a real here? *)
221
            if Real.is_t ty then Real.init_set else Gmp.init_set
222
223
          in
          let affect e = init_set ~loc lv ev e in
224
225
226
227
228
229
230
231
232
          let then_block, _ =
            let s = affect e2 in
            Env.pop_and_get env2 s ~global_clear:false Env.Middle
          in
          let else_block, _ =
            let s = affect e3 in
            Env.pop_and_get env3 s ~global_clear:false Env.Middle
          in
          [ Cil.mkStmt ~valid_sid:true (If(e1, then_block, else_block, loc)) ])
233
234
    in
    e, env
235

236
let rec thost_to_host kf env th = match th with
237
  | TVar { lv_origin = Some v } ->
238
    Var (Visitor_behavior.Get.varinfo (Env.get_behavior env) v), env, v.vname
239
  | TVar ({ lv_origin = None } as logic_v) ->
240
    Var (Env.Logic_binding.get env logic_v), env, logic_v.lv_name
241
  | TResult _typ ->
242
243
244
245
    let vis = Env.get_visitor env in
    let kf = Extlib.the vis#current_kf in
    let lhost = Misc.result_lhost kf in
    (match lhost with
246
247
     | Var v -> Var (Visitor_behavior.Get.varinfo (Env.get_behavior env) v), env, "result"
     | _ -> assert false)
248
  | TMem t ->
249
    let e, env = term_to_exp kf env t in
250
251
    Mem e, env, ""

252
and toffset_to_offset ?loc kf env = function
253
  | TNoOffset -> NoOffset, env
254
  | TField(f, offset) ->
255
    let offset, env = toffset_to_offset ?loc kf env offset in
256
    Field(f, offset), env
257
  | TIndex(t, offset) ->
258
259
    let e, env = term_to_exp kf env t in
    let offset, env = toffset_to_offset kf env offset in
260
    Index(e, offset), env
261
  | TModel _ -> not_yet env "model"
262

263
264
265
and tlval_to_lval kf env (host, offset) =
  let host, env, name = thost_to_host kf env host in
  let offset, env = toffset_to_offset kf env offset in
266
267
268
269
270
271
  let name = match offset with NoOffset -> name | Field _ | Index _ -> "" in
  (host, offset), env, name

(* the returned boolean says that the expression is an mpz_string;
   the returned string is the name of the generated variable corresponding to
   the term. *)
272
and context_insensitive_term_to_exp kf env t =
273
274
  let loc = t.term_loc in
  match t.term_node with
275
  | TConst c ->
276
277
    let c, strnum = constant_to_exp ~loc t c in
    c, env, strnum, ""
278
  | TLval lv ->
279
    let lv, env, name = tlval_to_lval kf env lv in
280
281
    Cil.new_exp ~loc (Lval lv), env, C_number, name
  | TSizeOf ty -> Cil.sizeOf ~loc ty, env, C_number, "sizeof"
282
  | TSizeOfE t ->
283
    let e, env = term_to_exp kf env t in
284
    Cil.sizeOf ~loc (Cil.typeOf e), env, C_number, "sizeof"
285
  | TSizeOfStr s ->
286
287
    Cil.new_exp ~loc (SizeOfStr s), env, C_number, "sizeofstr"
  | TAlignOf ty -> Cil.new_exp ~loc (AlignOf ty), env, C_number, "alignof"
288
  | TAlignOfE t ->
289
    let e, env = term_to_exp kf env t in
290
    Cil.new_exp ~loc (AlignOfE e), env, C_number, "alignof"
291
  | TUnOp(Neg | BNot as op, t') ->
292
    let ty = Typing.get_typ t in
293
    let e, env = term_to_exp kf env t' in
294
    if Gmp.Z.is_t ty then
295
      let name, vname = match op with
296
297
298
        | Neg -> "__gmpz_neg", "neg"
        | BNot -> "__gmpz_com", "bnot"
        | LNot -> assert false
299
      in
300
      let _, e, env =
301
302
303
304
305
306
        Env.new_var_and_mpz_init
          ~loc
          env
          ~name:vname
          (Some t)
          (fun _ ev -> [ Misc.mk_call ~loc name [ ev; e ] ])
307
      in
308
      e, env, C_number, ""
309
    else if Real.is_t ty then
310
      not_yet env "reals: Neg | BNot"
311
    else
312
      Cil.new_exp ~loc (UnOp(op, e, ty)), env, C_number, ""
313
  | TUnOp(LNot, t) ->
314
    let ty = Typing.get_op t in
315
    if Gmp.Z.is_t ty then
316
317
      (* [!t] is converted into [t == 0] *)
      let zero = Logic_const.tinteger 0 in
318
      let ctx = Typing.get_number_ty t in
319
      Typing.type_term ~use_gmp_opt:true ~ctx zero;
Julien Signoles's avatar
Julien Signoles committed
320
321
      let e, env =
        comparison_to_exp kf ~loc ~name:"not" env Typing.gmpz Eq t zero (Some t)
322
      in
323
      e, env, C_number, ""
324
    else if Real.is_t ty then
325
      not_yet env "reals: LNot"
326
327
    else begin
      assert (Cil.isIntegralType ty);
328
      let e, env = term_to_exp kf env t in
329
      Cil.new_exp ~loc (UnOp(LNot, e, Cil.intType)), env, C_number, ""
330
331
    end
  | TBinOp(PlusA | MinusA | Mult as bop, t1, t2) ->
332
    let ty = Typing.get_typ t in
333
334
    let e1, env = term_to_exp kf env t1 in
    let e2, env = term_to_exp kf env t2 in
335
    if Gmp.Z.is_t ty then
336
337
      let name = name_of_mpz_arith_bop bop in
      let mk_stmts _ e = [ Misc.mk_call ~loc name [ e; e1; e2 ] ] in
338
      let name = Misc.name_of_binop bop in
339
340
      let _, e, env =
	Env.new_var_and_mpz_init ~loc ~name env (Some t) mk_stmts
341
      in
342
      e, env, C_number, ""
343
344
    else if Real.is_t ty then
      let e, env = Real.binop ~loc bop e1 e2 env (Some t) in
345
      e, env, C_number, ""
346
    else
347
348
349
    if Logic_typing.is_integral_type t.term_type then
      Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
    else
Julien Signoles's avatar
Julien Signoles committed
350
      (* TODO RATIONAL: why question mark? *)
351
      not_yet env "floating-point context (?)"
352
  | TBinOp(Div | Mod as bop, t1, t2) ->
353
    let ty = Typing.get_typ t in
354
355
    let e1, env = term_to_exp kf env t1 in
    let e2, env = term_to_exp kf env t2 in
356
    if Gmp.Z.is_t ty then
357
      (* TODO: preventing division by zero should not be required anymore.
358
         RTE should do this automatically. *)
359
      let ctx = Typing.get_number_ty t in
360
      let t = Some t in
361
      let name = name_of_mpz_arith_bop bop in
362
      (* [TODO] can now do better since the type system got some info about
363
         possible values of [t2] *)
364
365
      (* guarding divisions and modulos *)
      let zero = Logic_const.tinteger 0 in
366
      Typing.type_term ~use_gmp_opt:true ~ctx zero;
367
      (* do not generate [e2] from [t2] twice *)
368
      let guard, env =
369
        let name = Misc.name_of_binop bop ^ "_guard" in
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
370
        comparison_to_exp
371
          ~loc kf env Typing.gmpz ~e1:e2 ~name Eq t2 zero t
372
      in
373
      let mk_stmts _v e =
374
	assert (Gmp.Z.is_t ty);
375
376
	let vis = Env.get_visitor env in
	let kf = Extlib.the vis#current_kf in
377
378
379
	let cond =
	  Misc.mk_e_acsl_guard
	    (Env.annotation_kind env)
380
	    kf
381
	    guard
382
	    (Logic_const.prel ~loc (Req, t2, zero))
383
384
385
386
	in
	Env.add_assert env cond (Logic_const.prel (Rneq, t2, zero));
	let instr = Misc.mk_call ~loc name [ e; e1; e2 ] in
	[ cond; instr ]
387
      in
388
      let name = Misc.name_of_binop bop in
389
      let _, e, env = Env.new_var_and_mpz_init ~loc ~name env t mk_stmts in
390
      e, env, C_number, ""
391
392
    else if Real.is_t ty then
      let e, env = Real.binop ~loc bop e1 e2 env (Some t) in
393
      e, env, C_number, ""
394
    else
395
      (* no guard required since RTEs are generated separately *)
396
397
398
    if Logic_typing.is_integral_type t.term_type then
      Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
    else
Julien Signoles's avatar
Julien Signoles committed
399
      (* TODO RATIONAL: why question mark? *)
400
      not_yet env "floating-point context (?)"
401
402
  | TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
    (* comparison operators *)
403
    let ity = Typing.get_integer_op t in
404
    let e, env = comparison_to_exp ~loc kf env ity bop t1 t2 (Some t) in
405
    e, env, C_number, ""
406
407
  | TBinOp((Shiftlt | Shiftrt), _, _) ->
    (* left/right shift *)
408
    not_yet env "left/right shift"
409
410
  | TBinOp(LOr, t1, t2) ->
    (* t1 || t2 <==> if t1 then true else t2 *)
411
    let e1, env1 = term_to_exp kf (Env.rte env true) t1 in
412
    let env' = Env.push env1 in
413
    let res2 = term_to_exp kf (Env.push env') t2 in
414
    let e, env =
415
      conditional_to_exp ~name:"or" loc (Some t) e1 (Cil.one loc, env') res2
416
    in
417
    e, env, C_number, ""
418
419
  | TBinOp(LAnd, t1, t2) ->
    (* t1 && t2 <==> if t1 then t2 else false *)
420
421
    let e1, env1 = term_to_exp kf (Env.rte env true) t1 in
    let _, env2 as res2 = term_to_exp kf (Env.push env1) t2 in
422
    let env3 = Env.push env2 in
423
424
    let e, env =
      conditional_to_exp ~name:"and" loc (Some t) e1 res2 (Cil.zero loc, env3)
425
    in
426
    e, env, C_number, ""
427
428
  | TBinOp((BOr | BXor | BAnd), _, _) ->
    (* other logic/arith operators  *)
429
    not_yet env "missing binary bitwise operator"
430
  | TBinOp(PlusPI | IndexPI | MinusPI as bop, t1, t2) ->
431
    if Misc.is_set_of_ptr_or_array t1.term_type ||
432
433
434
435
       Misc.is_set_of_ptr_or_array t2.term_type then
      (* case of arithmetic over set of pointers (due to use of ranges)
         should have already been handled in [mmodel_call_with_ranges] *)
      assert false;
436
    (* binary operation over pointers *)
437
438
439
    let ty = match t1.term_type with
      | Ctype ty -> ty
      | _ -> assert false
440
    in
441
442
    let e1, env = term_to_exp kf env t1 in
    let e2, env = term_to_exp kf env t2 in
443
    Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
444
  | TBinOp(MinusPP, t1, t2) ->
445
    begin match Typing.get_number_ty t with
446
447
448
449
      | Typing.C_type _ ->
        let e1, env = term_to_exp kf env t1 in
        let e2, env = term_to_exp kf env t2 in
        let ty = Typing.get_typ t in
450
        Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)), env, C_number, ""
451
      | Typing.Gmpz ->
452
        not_yet env "pointer subtraction resulting in gmp"
453
      | Typing.Real | Typing.Nan ->
454
455
        assert false
    end
456
  | TCastE(ty, t') ->
457
    let e, env = term_to_exp kf env t' in
458
    let e, env =
459
      add_cast ~loc ~name:"cast" env (Some ty) C_number (Some t) e
460
    in
461
    e, env, C_number, ""
462
  | TLogic_coerce _ -> assert false (* handle in [term_to_exp] *)
463
  | TAddrOf lv ->
464
    let lv, env, _ = tlval_to_lval kf env lv in
465
    Cil.mkAddrOf ~loc lv, env, C_number, "addrof"
466
  | TStartOf lv ->
467
    let lv, env, _ = tlval_to_lval kf env lv in
468
    Cil.mkAddrOrStartOf ~loc lv, env, C_number, "startof"
469
  | Tapp(li, [], targs) ->
Julien Signoles's avatar
Julien Signoles committed
470
471
472
473
    let fname = li.l_var_info.lv_name in
    (* build the varinfo (as an expression) which stores the result of the
       function call. *)
    let _, e, env =
474
475
      if Builtins.mem li.l_var_info.lv_name then
        (* E-ACSL built-in function call *)
476
477
478
479
480
481
482
483
484
485
486
487
488
        let args, env =
          try
            List.fold_right
              (fun targ (l, env) ->
                 let e, env = term_to_exp kf env targ in
                 e :: l, env)
              targs
              ([], env)
          with Invalid_argument _ ->
            Options.fatal
              "[Tapp] unexpected number of arguments when calling %s"
              fname
        in
489
490
491
492
493
494
        Env.new_var
          ~loc
          ~name:(fname ^ "_app")
          env
          (Some t)
          (Misc.cty (Extlib.the li.l_type))
495
496
          (fun vi _ ->
             [ Misc.mk_call ~loc ~result:(Cil.var vi) fname args ])
497
      else
498
499
500
501
502
        (* build the arguments and compute the integer_ty of the parameters *)
        let params_ty, args, env =
          List.fold_right
            (fun targ (params_ty, args, env) ->
               let e, env = term_to_exp kf env targ in
503
               let param_ty = Typing.get_number_ty targ in
504
505
               let e, env =
                 try
506
507
                   let ty = Typing.typ_of_number_ty param_ty in
                   (* TODO RATIONAL: check [Not_a_strnum] *)
508
                   add_cast loc env (Some ty) C_number (Some targ) e
509
                 with Typing.Not_a_number ->
510
511
512
                   e, env
               in
               param_ty :: params_ty, e :: args, env)
513
            targs
514
            ([], [], env)
515
        in
516
517
518
519
        let gen_fname =
          Env.Varname.get ~scope:Env.Global (Functions.RTL.mk_gen_name fname)
        in
        Logic_functions.tapp_to_exp ~loc gen_fname env t li params_ty args
Julien Signoles's avatar
Julien Signoles committed
520
    in
521
    e, env, C_number, "app"
522
523
  | Tapp(_, _ :: _, _) ->
    not_yet env "logic functions with labels"
524
525
  | Tlambda _ -> not_yet env "functional"
  | TDataCons _ -> not_yet env "constructor"
526
  | Tif(t1, t2, t3) ->
527
528
529
    let e1, env1 = term_to_exp kf (Env.rte env true) t1 in
    let (_, env2 as res2) = term_to_exp kf (Env.push env1) t2 in
    let res3 = term_to_exp kf (Env.push env2) t3 in
530
    let e, env = conditional_to_exp loc (Some t) e1 res2 res3 in
531
    e, env, C_number, ""
532
  | Tat(t, BuiltinLabel Here) ->
533
    let e, env = term_to_exp kf env t in
534
    e, env, C_number, ""
535
  | Tat(t', label) ->
536
537
    let lscope = Env.Logic_scope.get env in
    let pot = Misc.PoT_term t' in
538
539
    if Lscope.is_used lscope pot then
      let e, env = At_with_lscope.to_exp ~loc kf env pot label in
540
      e, env, C_number, ""
541
    else
542
      let e, env = term_to_exp kf (Env.push env) t' in
543
544
      let e, env, sty = at_to_exp_no_lscope env (Some t) label e in
      e, env, sty, ""
545
  | Tbase_addr(BuiltinLabel Here, t) ->
546
547
    let name = "base_addr" in
    let e, env = Mmodel_translate.call ~loc kf name Cil.voidPtrType env t in
548
    e, env, C_number, name
549
  | Tbase_addr _ -> not_yet env "labeled \\base_addr"
550
  | Toffset(BuiltinLabel Here, t) ->
551
    let size_t = Cil.theMachine.Cil.typeOfSizeOf in
552
553
    let name = "offset" in
    let e, env = Mmodel_translate.call ~loc kf name size_t env t in
554
    e, env, C_number, name
555
  | Toffset _ -> not_yet env "labeled \\offset"
556
  | Tblock_length(BuiltinLabel Here, t) ->
557
    let size_t = Cil.theMachine.Cil.typeOfSizeOf in
558
559
    let name = "block_length" in
    let e, env = Mmodel_translate.call ~loc kf name size_t env t in
560
    e, env, C_number, name
561
  | Tblock_length _ -> not_yet env "labeled \\block_length"
562
  | Tnull ->
563
    Cil.mkCast (Cil.zero ~loc) (TPtr(TVoid [], [])), env, C_number, "null"
564
565
566
567
568
569
570
571
  | TUpdate _ -> not_yet env "functional update"
  | Ttypeof _ -> not_yet env "typeof"
  | Ttype _ -> not_yet env "C type"
  | Tempty_set -> not_yet env "empty tset"
  | Tunion _ -> not_yet env "union of tsets"
  | Tinter _ -> not_yet env "intersection of tsets"
  | Tcomprehension _ -> not_yet env "tset comprehension"
  | Trange _ -> not_yet env "range"
572
  | Tlet(li, t) ->
573
    let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
574
    let env = Env.Logic_scope.extend env lvs in
575
576
    let env = env_of_li li kf env loc in
    let e, env = term_to_exp kf env t in
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
577
    Interval.Env.remove li.l_var_info;
578
    e, env, C_number, ""
579
580
581
582

(* Convert an ACSL term into a corresponding C expression (if any) in the given
   environment. Also extend this environment in order to include the generating
   constructs. *)
583
and term_to_exp kf env t =
584
  let generate_rte = Env.generate_rte env in
585
  Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)"
586
587
    Printer.pp_term t generate_rte;
  let env = Env.rte env false in
588
  let t = match t.term_node with TLogic_coerce(_, t) -> t | _ -> t in
589
  let e, env, sty, name = context_insensitive_term_to_exp kf env t in
590
  let env = if generate_rte then translate_rte kf env e else env in
591
  let cast = Typing.get_cast t in
592
593
594
595
596
597
  let name = if name = "" then None else Some name in
  add_cast
    ~loc:t.term_loc
    ?name
    env
    cast
598
    sty
599
600
    (Some t)
    e
601
602
603

(* generate the C code equivalent to [t1 bop t2]. *)
and comparison_to_exp
604
    ~loc ?e1 kf env ity bop ?(name=Misc.name_of_binop bop) t1 t2 t_opt =
605
606
  let e1, env = match e1 with
    | None ->
607
      let e1, env = term_to_exp kf env t1 in
608
609
610
      e1, env
    | Some e1 ->
      e1, env
611
  in
612
  let e2, env = term_to_exp kf env t2 in
613
  match ity with
614
615
616
617
  | Typing.C_type _ | Typing.Nan ->
    Cil.mkBinOp ~loc bop e1 e2, env
  | Typing.Gmpz ->
    let _, e, env = Env.new_var
618
619
620
621
622
623
624
        ~loc
        env
        t_opt
        ~name
        Cil.intType
        (fun v _ ->
           [ Misc.mk_call ~loc ~result:(Cil.var v) "__gmpz_cmp" [ e1; e2 ] ])
625
    in
626
    Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
627
628
  | Typing.Real ->
    Real.cmp ~loc bop e1 e2 env t_opt
629

630
and at_to_exp_no_lscope env t_opt label e =
631
  let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
632
  (* generate a new variable denoting [\at(t',label)].
633
     That is this variable which is the resulting expression.
634
635
     ACSL typing rule ensures that the type of this variable is the same as
     the one of [e]. *)
636
  let loc = Stmt.loc stmt in
637
638
  let res_v, res, new_env =
    Env.new_var
639
      ~loc
640
      ~name:"at"
641
      ~scope:Env.Function
642
643
      env
      t_opt
644
      (Cil.typeOf e)
645
      (fun _ _ -> [])
646
647
648
  in
  let env_ref = ref new_env in
  (* visitor modifying in place the labeled statement in order to store [e]
649
650
     in the resulting variable at this location (which is the only correct
     one). *)
651
  let o = object
652
    inherit Visitor.frama_c_inplace
653
    method !vstmt_aux stmt =
Julien Signoles's avatar
Julien Signoles committed
654
655
      (* either a standard C affectation or a call to an initializer according
         to the type of [e] *)
656
      let ty = Cil.typeOf e in
657
      let init_set = if Real.is_t ty then Real.init_set else Gmp.init_set in
658
      let new_stmt = init_set ~loc (Cil.var res_v) res e in
659
660
      assert (!env_ref == new_env);
      (* generate the new block of code for the labeled statement and the
661
         corresponding environment *)
662
      let block, new_env =
663
        Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
664
      in
665
      env_ref := Env.extend_stmt_in_place new_env stmt ~label block;
666
667
668
669
      Cil.ChangeTo stmt
  end
  in
  let bhv = Env.get_behavior new_env in
670
671
672
673
  let new_stmt =
    Visitor.visitFramacStmt o (Visitor_behavior.Get.stmt bhv stmt)
  in
  Visitor_behavior.Set.stmt bhv stmt new_stmt;
674
  res, !env_ref, C_number
675

676
and env_of_li li kf env loc =
677
678
  let t = Misc.term_of_li li in
  let ty = Typing.get_typ t in
679
  let vi, vi_e, env = Env.Logic_binding.add ~ty env li.l_var_info in
680
681
682
683
684
685
  let e, env = term_to_exp kf env t in
  let stmt = match Typing.get_number_ty t with
    | Typing.C_type _ | Typing.Nan ->
      Cil.mkStmtOneInstr (Set (Cil.var vi, e, loc))
    | Typing.Gmpz ->
      Gmp.init_set ~loc (Cil.var vi) vi_e e
686
687
    | Typing.Real ->
      Real.init_set ~loc (Cil.var vi) vi_e e
688
689
690
  in
  Env.add_stmt env stmt

691
692
693
(* Convert an ACSL named predicate into a corresponding C expression (if
   any) in the given environment. Also extend this environment which includes
   the generating constructs. *)
694
and named_predicate_content_to_exp ?name kf env p =
695
696
  let loc = p.pred_loc in
  match p.pred_content with
697
698
  | Pfalse -> Cil.zero ~loc, env
  | Ptrue -> Cil.one ~loc, env
699
700
  | Papp(li, labels, args) ->
    (* Simply use the implementation of Tapp(li, labels, args).
701
702
703
       To achieve this, we create a clone of [li] for which the type is
       transformed from [None] (type of predicates) to
       [Some int] (type as a term). *)
704
705
706
707
708
709
710
711
712
    let prj = Project.current () in
    let o = object inherit Visitor.frama_c_copy prj end in
    let li = Visitor.visitFramacLogicInfo o li in
    let lty = Ctype Cil.intType in
    li.l_type <- Some lty;
    let tapp = Logic_const.term ~loc (Tapp(li, labels, args)) lty in
    Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int tapp;
    let e, env = term_to_exp kf env tapp in
    e, env
713
  | Pseparated _ -> not_yet env "\\separated"
714
  | Pdangling _ -> not_yet env "\\dangling"
715
  | Pvalid_function _ -> not_yet env "\\valid_function"
716
  | Prel(rel, t1, t2) ->
717
    let ity = Typing.get_integer_op_of_predicate p in
718
    comparison_to_exp ~loc kf env ity (relation_to_binop rel) t1 t2 None
719
720
  | Pand(p1, p2) ->
    (* p1 && p2 <==> if p1 then p2 else false *)
721
    let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 in
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
722
    let _, env2 as res2 =
723
      named_predicate_to_exp kf (Env.push env1) p2 in
724
725
    let env3 = Env.push env2 in
    let name = match name with None -> "and" | Some n -> n in
726
    conditional_to_exp ~name loc None e1 res2 (Cil.zero loc, env3)
727
  | Por(p1, p2) ->
728
    (* p1 || p2 <==> if p1 then true else p2 *)
729
    let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 in
730
    let env' = Env.push env1 in
731
    let res2 = named_predicate_to_exp kf (Env.push env') p2 in
732
    let name = match name with None -> "or" | Some n -> n in
733
    conditional_to_exp ~name loc None e1 (Cil.one loc, env') res2
734
  | Pxor _ -> not_yet env "xor"
735
  | Pimplies(p1, p2) ->
736
    (* (p1 ==> p2) <==> !p1 || p2 *)
737
    named_predicate_to_exp
738
      ~name:"implies"
739
      kf
740
741
      env
      (Logic_const.por ~loc ((Logic_const.pnot ~loc p1), p2))
742
  | Piff(p1, p2) ->
743
    (* (p1 <==> p2) <==> (p1 ==> p2 && p2 ==> p1) *)
744
    named_predicate_to_exp
745
      ~name:"equiv"
746
      kf
747
748
      env
      (Logic_const.pand ~loc
749
	 (Logic_const.pimplies ~loc (p1, p2),
750
751
	  Logic_const.pimplies ~loc (p2, p1)))
  | Pnot p ->
752
    let e, env = named_predicate_to_exp kf env p in
753
754
    Cil.new_exp ~loc (UnOp(LNot, e, Cil.intType)), env
  | Pif(t, p2, p3) ->
755
    let e1, env1 = term_to_exp kf (Env.rte env true) t in
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
756
    let (_, env2 as res2) =
757
758
      named_predicate_to_exp kf (Env.push env1) p2 in
    let res3 = named_predicate_to_exp kf (Env.push env2) p3 in
759
    conditional_to_exp loc None e1 res2 res3
760
  | Plet(li, p) ->
761
    let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
762
    let env = Env.Logic_scope.extend env lvs in
763
764
    let env = env_of_li li kf env loc in
    let e, env = named_predicate_to_exp kf env p in
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
765
766
    Interval.Env.remove li.l_var_info;
    e, env
767
  | Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
768
  | Pat(p, BuiltinLabel Here) ->
769
    named_predicate_to_exp kf env p
770
  | Pat(p', label) ->
771
772
    let lscope = Env.Logic_scope.get env in
    let pot = Misc.PoT_pred p' in
773
774
775
    if Lscope.is_used lscope pot then
      At_with_lscope.to_exp ~loc kf env pot label
    else begin