translate.ml 39.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
type strnum_ty = (* TYpe of a STRing that represents a NUMber *)
  | StrZ
  | StrR
  | Not_a_strnum (* C numbers (integers AND floats) included *)

68
(* convert [e] in a way that it is compatible with the given typing context. *)
69
let add_cast ~loc ?name env ctx sty t_opt e =
70
  let mk_mpz e =
71
72
73
74
75
    let _, e, env = Env.new_var
      ~loc
      ?name
      env
      t_opt
76
      (Gmp.Z.t ())
77
      (fun lv v -> [ Gmp.init_set ~loc (Cil.var lv) v e ])
78
79
80
    in
    e, env
  in
81
82
  let e, env = match sty with
    | StrZ -> mk_mpz e
83
    | StrR -> Real.mk_real ~loc ?name e env t_opt
84
85
    | Not_a_strnum -> e, env
  in
86
  match ctx with
87
88
  | None ->
    e, env
89
90
  | Some ctx ->
    let ty = Cil.typeOf e in
91
92
    if Gmp.Z.is_t ctx then
      if Gmp.Z.is_t ty then
93
        e, env
94
95
      else if Real.is_t ty then
        Real.cast_to_z ~loc ?name e env
96
97
98
99
      else
        (* Convert the C integer into a mpz.
           Remember: very long integer constants have been temporary converted
           into strings;
100
           also possible to get a non integralType (or Gmp.z_t) with a non-one in
101
102
           the case of \null *)
        let e =
103
104
105
106
107
108
          if Cil.isIntegralType ty || sty = StrZ then
            e
          else if not (Cil.isIntegralType ty) && sty = Not_a_strnum then
            Cil.mkCast e Cil.longType (* \null *)
          else (* Remaining: not (Cil.isIntegralType ty) && sty = StrR *)
            assert false
109
110
        in
        mk_mpz e
111
112
113
    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
114
115
    else
      (* handle a C-integer context *)
116
      if Gmp.Z.is_t ty || sty = StrZ then
117
118
        (* we get an mpz, but it fits into a C integer: convert it *)
        let fname, new_ty =
119
          if Cil.isSignedInteger ctx then
120
121
122
123
124
125
126
127
128
129
130
131
132
133
            "__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
134
135
      else if Real.is_t ty || sty = StrR then
        Real.add_cast ~loc ?name e env ctx
136
      else
137
        Cil.mkCastT ~force:false ~e ~oldt:ty ~newt:ctx, env
138

139
140
let constant_to_exp ~loc t c =
  let mk_real s =
141
    let s = Real.normalize_str s in
142
143
144
    Cil.mkString ~loc s, StrR
  in
  match c with
145
  | Integer(n, _repr) ->
146
    (try
147
       let ity = Typing.get_number_ty t in
148
       match ity with
149
150
       | Typing.Nan ->
         assert false
151
       | Typing.Real ->
152
153
154
         mk_real (Integer.to_string n)
       | Typing.Gmpz ->
         raise Cil.Not_representable
155
156
       | Typing.C_type kind ->
         let cast = Typing.get_cast t in
157
         match cast, kind with
158
         | Some ty, (ILongLong | IULongLong) when Gmp.Z.is_t ty ->
159
           raise Cil.Not_representable
160
         | Some ty, (ILongLong | IULongLong) when Real.is_t ty ->
161
           mk_real (Integer.to_string n)
162
163
164
165
166
167
168
         | (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. *)
169
           Cil.kinteger64 ~loc ~kind n, Not_a_strnum
170
     with Cil.Not_representable ->
171
       (* too big integer *)
172
173
174
175
176
177
178
       Cil.mkString ~loc (Integer.to_string n), StrZ)
  | LStr s -> Cil.new_exp ~loc (Const (CStr s)), Not_a_strnum
  | LWStr s -> Cil.new_exp ~loc (Const (CWStr s)), Not_a_strnum
  | LChr c -> Cil.new_exp ~loc (Const (CChr c)), Not_a_strnum
  | LReal {r_literal=s; r_nearest=_; r_lower=_; r_upper=_} ->
    mk_real s
  | LEnum e -> Cil.new_exp ~loc (Const (CEnum e)), Not_a_strnum
179

180
let conditional_to_exp ?(name="if") loc t_opt e1 (e2, env2) (e3, env3) =
181
  let env = Env.pop (Env.pop env3) in
182
183
184
185
186
187
  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
  | _ ->
188
189
    let ty = match t_opt with
      | None (* predicate *) -> Cil.intType
190
      | Some t -> Typing.get_typ t
191
    in
192
193
    let _, e, env =
      Env.new_var
194
195
196
197
198
199
200
        ~loc
        ~name
        env
        t_opt
        ty
        (fun v ev ->
          let lv = Cil.var v in
201
202
          let ty = Cil.typeOf ev in
          let init_set =
203
            if Real.is_t ty then Real.init_set else Gmp.init_set
204
205
          in
          let affect e = init_set ~loc lv ev e in
206
207
208
209
210
211
212
213
214
          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)) ])
215
216
    in
    e, env
217

218
let rec thost_to_host kf env th = match th with
219
  | TVar { lv_origin = Some v } ->
220
    Var (Visitor_behavior.Get.varinfo (Env.get_behavior env) v), env, v.vname
221
  | TVar ({ lv_origin = None } as logic_v) ->
222
    Var (Env.Logic_binding.get env logic_v), env, logic_v.lv_name
223
  | TResult _typ ->
224
225
226
227
    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
228
    | Var v -> Var (Visitor_behavior.Get.varinfo (Env.get_behavior env) v), env, "result"
229
230
    | _ -> assert false)
  | TMem t ->
231
    let e, env = term_to_exp kf env t in
232
233
    Mem e, env, ""

234
and toffset_to_offset ?loc kf env = function
235
  | TNoOffset -> NoOffset, env
236
  | TField(f, offset) ->
237
    let offset, env = toffset_to_offset ?loc kf env offset in
238
    Field(f, offset), env
239
  | TIndex(t, offset) ->
240
241
    let e, env = term_to_exp kf env t in
    let offset, env = toffset_to_offset kf env offset in
242
    Index(e, offset), env
243
  | TModel _ -> not_yet env "model"
244

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

(* 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. *)
563
and term_to_exp kf env t =
564
  let generate_rte = Env.generate_rte env in
565
  Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)"
566
567
    Printer.pp_term t generate_rte;
  let env = Env.rte env false in
568
  let t = match t.term_node with TLogic_coerce(_, t) -> t | _ -> t in
569
  let e, env, sty, name = context_insensitive_term_to_exp kf env t in
570
  let env = if generate_rte then translate_rte kf env e else env in
571
  let cast = Typing.get_cast t in
572
573
574
575
576
577
  let name = if name = "" then None else Some name in
  add_cast
    ~loc:t.term_loc
    ?name
    env
    cast
578
    sty
579
580
    (Some t)
    e
581
582
583

(* generate the C code equivalent to [t1 bop t2]. *)
and comparison_to_exp
584
    ~loc ?e1 kf env ity bop ?(name=Misc.name_of_binop bop) t1 t2 t_opt =
585
586
  let e1, env = match e1 with
    | None ->
587
      let e1, env = term_to_exp kf env t1 in
588
589
590
      e1, env
    | Some e1 ->
      e1, env
591
  in
592
  let e2, env = term_to_exp kf env t2 in
593
  match ity with
594
595
596
597
598
599
600
601
602
603
604
  | Typing.C_type _ | Typing.Nan ->
    Cil.mkBinOp ~loc bop e1 e2, env
  | Typing.Gmpz ->
    let _, e, env = Env.new_var
      ~loc
      env
      t_opt
      ~name
      Cil.intType
      (fun v _ ->
        [ Misc.mk_call ~loc ~result:(Cil.var v) "__gmpz_cmp" [ e1; e2 ] ])
605
    in
606
    Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
607
608
  | Typing.Real ->
    Real.cmp ~loc bop e1 e2 env t_opt
609

610
and at_to_exp_no_lscope env t_opt label e =
611
  let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
612
  (* generate a new variable denoting [\at(t',label)].
613
     That is this variable which is the resulting expression.
614
615
     ACSL typing rule ensures that the type of this variable is the same as
     the one of [e]. *)
616
  let loc = Stmt.loc stmt in
617
618
  let res_v, res, new_env =
    Env.new_var
619
      ~loc
620
      ~name:"at"
621
      ~scope:Env.Function
622
623
      env
      t_opt
624
      (Cil.typeOf e)
625
      (fun _ _ -> [])
626
627
628
  in
  let env_ref = ref new_env in
  (* visitor modifying in place the labeled statement in order to store [e]
629
630
     in the resulting variable at this location (which is the only correct
     one). *)
631
  let o = object
632
    inherit Visitor.frama_c_inplace
633
    method !vstmt_aux stmt =
634
      (* either a standard C affectation or something else according to type of
635
        [e] *)
636
      let ty = Cil.typeOf e in
637
      let init_set = if Real.is_t ty then Real.init_set else Gmp.init_set in
638
      let new_stmt = init_set ~loc (Cil.var res_v) res e in
639
640
      assert (!env_ref == new_env);
      (* generate the new block of code for the labeled statement and the
641
        corresponding environment *)
642
      let block, new_env =
643
       Env.pop_and_get new_env new_stmt ~global_clear:false Env.Middle
644
      in
645
      env_ref := Env.extend_stmt_in_place new_env stmt ~label block;
646
647
648
649
      Cil.ChangeTo stmt
  end
  in
  let bhv = Env.get_behavior new_env in
650
651
652
653
654
  let new_stmt =
    Visitor.visitFramacStmt o (Visitor_behavior.Get.stmt bhv stmt)
  in
  Visitor_behavior.Set.stmt bhv stmt new_stmt;
  res, !env_ref, Not_a_strnum
655

656
and env_of_li li kf env loc =
657
658
  let t = Misc.term_of_li li in
  let ty = Typing.get_typ t in
659
  let vi, vi_e, env = Env.Logic_binding.add ~ty env li.l_var_info in
660
661
662
663
664
665
  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
666
667
    | Typing.Real ->
      Real.init_set ~loc (Cil.var vi) vi_e e
668
669
670
  in
  Env.add_stmt env stmt

671
672
673
(* 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. *)
674
and named_predicate_content_to_exp ?name kf env p =
675
676
  let loc = p.pred_loc in
  match p.pred_content with
677
678
  | Pfalse -> Cil.zero ~loc, env
  | Ptrue -> Cil.one ~loc, env
679
680
681
682
  | Papp(li, labels, args) ->
    (* Simply use the implementation of Tapp(li, labels, args).
      To achieve this, we create a clone of [li] for which the type is
      transformed from [None] (type of predicates) to
683
      [Some int] (type as a term). *)
684
685
686
687
688
689
690
691
692
    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
693
  | Pseparated _ -> not_yet env "\\separated"
694
  | Pdangling _ -> not_yet env "\\dangling"
695
  | Pvalid_function _ -> not_yet env "\\valid_function"
696
  | Prel(rel, t1, t2) ->
697
    let ity = Typing.get_integer_op_of_predicate p in
698
    comparison_to_exp ~loc kf env ity (relation_to_binop rel) t1 t2 None
699
700
  | Pand(p1, p2) ->
    (* p1 && p2 <==> if p1 then p2 else false *)
701
    let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 in
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
702
    let _, env2 as res2 =
703
      named_predicate_to_exp kf (Env.push env1) p2 in
704
705
    let env3 = Env.push env2 in
    let name = match name with None -> "and" | Some n -> n in
706
    conditional_to_exp ~name loc None e1 res2 (Cil.zero loc, env3)
707
  | Por(p1, p2) ->
708
    (* p1 || p2 <==> if p1 then true else p2 *)
709
    let e1, env1 = named_predicate_to_exp kf (Env.rte env true) p1 in
710
    let env' = Env.push env1 in
711
    let res2 = named_predicate_to_exp kf (Env.push env') p2 in
712
    let name = match name with None -> "or" | Some n -> n in
713
    conditional_to_exp ~name loc None e1 (Cil.one loc, env') res2
714
  | Pxor _ -> not_yet env "xor"
715
  | Pimplies(p1, p2) ->
716
    (* (p1 ==> p2) <==> !p1 || p2 *)
717
    named_predicate_to_exp
718
      ~name:"implies"
719
      kf
720
721
      env
      (Logic_const.por ~loc ((Logic_const.pnot ~loc p1), p2))
722
  | Piff(p1, p2) ->
723
    (* (p1 <==> p2) <==> (p1 ==> p2 && p2 ==> p1) *)
724
    named_predicate_to_exp
725
      ~name:"equiv"
726
      kf
727
728
      env
      (Logic_const.pand ~loc
729
	 (Logic_const.pimplies ~loc (p1, p2),
730
731
	  Logic_const.pimplies ~loc (p2, p1)))
  | Pnot p ->
732
    let e, env = named_predicate_to_exp kf env p in
733
734
    Cil.new_exp ~loc (UnOp(LNot, e, Cil.intType)), env
  | Pif(t, p2, p3) ->
735
    let e1, env1 = term_to_exp kf (Env.rte env true) t in
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
736
    let (_, env2 as res2) =
737
738
      named_predicate_to_exp kf (Env.push env1) p2 in
    let res3 = named_predicate_to_exp kf (Env.push env2) p3 in
739
    conditional_to_exp loc None e1 res2 res3
740
  | Plet(li, p) ->
741
    let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
742
    let env = Env.Logic_scope.extend env lvs in
743
744
    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
745
746
    Interval.Env.remove li.l_var_info;
    e, env
747
  | Pforall _ | Pexists _ -> Quantif.quantif_to_exp kf env p
748
  | Pat(p, BuiltinLabel Here) ->
749
    named_predicate_to_exp kf env p
750
  | Pat(p', label) ->
751
752
    let lscope = Env.Logic_scope.get env in
    let pot = Misc.PoT_pred p' in
753
754
755
    if Lscope.is_used lscope pot then
      At_with_lscope.to_exp ~loc kf env pot label
    else begin
756
757
      (* convert [t'] to [e] in a separated local env *)
      let e, env = named_predicate_to_exp kf (Env.push env) p' in
758
759
      let e, env, sty = at_to_exp_no_lscope env None label e in
      assert (sty = Not_a_strnum);
760
      e, env
761
    end
762
763
  | Pvalid_read(BuiltinLabel Here as llabel, t) as pc
  | (Pvalid(BuiltinLabel Here as llabel, t) as pc) ->
764
    let call_valid t =
765
      let name = match pc with
766
767
768
        | Pvalid _ -> "valid"
        | Pvalid_read _ -> "valid_read"
        | _ -> assert false
769
      in
770
      Mmodel_translate.call_valid ~loc kf name Cil.intType env t
771
    in
Julien Signoles's avatar
Julien Signoles committed
772
    if !is_visiting_valid then begin
773
      (* we already transformed \valid(t) into \initialized(&t) && \valid(t):
774
         now convert this right-most valid. *)
Julien Signoles's avatar
Julien Signoles committed
775
      is_visiting_valid := false;
776
      call_valid t p
777
778
779
    end else begin
      match t.term_node, t.term_type with
      | TLval tlv, Ctype ty ->
780
781
782
783
784
785
        let init =
          Logic_const.pinitialized ~loc (llabel, Misc.term_addr_of ~loc tlv ty)
        in
        Typing.type_named_predicate ~must_clear:false init;
        let p = Logic_const.pand ~loc (init, p) in
        is_visiting_valid := true;
786
        named_predicate_to_exp kf env p
787
      | _ ->
788
        call_valid t p
789
    end
790
791
  | Pvalid _ -> not_yet env "labeled \\valid"
  | Pvalid_read _ -> not_yet env "labeled \\valid_read"
792
  | Pinitialized(BuiltinLabel Here, t) ->
793
    (match t.term_node with
794
795
    (* optimisation when we know that the initialisation is ok *)
    | TAddrOf (TResult _, TNoOffset) -> Cil.one ~loc, env
796
    | TAddrOf (TVar { lv_origin = Some vi }, TNoOffset)
797
798
      when
        vi.vformal || vi.vglob || Functions.RTL.is_generated_name vi.vname ->
799
      Cil.one ~loc, env
Fonenantsoa Maurica 's avatar
Fonenantsoa Maurica committed
800
    | _ ->
801
802
803
804
805
806
      Mmodel_translate.call_with_size
        ~loc
        kf
        "initialized"
        Cil.intType
        env
807
808
        t
        p)