injector.ml 28.2 KB
Newer Older
Julien Signoles's avatar
Julien Signoles committed
1
2
3
4
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
(*                                                                        *)
5
(*  Copyright (C) 2012-2019                                               *)
Julien Signoles's avatar
Julien Signoles committed
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         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                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

23
module E_acsl_label = Label (* [Label] is hidden when opening [Cil_datatype *)
24
25
26
27
28
29
open Cil_types
open Cil_datatype

let dkey = Options.dkey_translation

(* ************************************************************************** *)
30
(* Expressions *)
31
32
(* ************************************************************************** *)

Julien Signoles's avatar
Julien Signoles committed
33
let replace_literal_string_in_exp env kf_opt (* None for globals *) e =
34
35
  (* do not touch global initializers because they accept only constants;
     replace literal strings elsewhere *)
Julien Signoles's avatar
Julien Signoles committed
36
37
  match kf_opt with
  | None -> e, env
38
  | Some kf -> Literal_observer.subst_all_literals_in_exp env kf e
Julien Signoles's avatar
Julien Signoles committed
39
40
41
42
43
44

let rec inject_in_init env kf_opt vi off = function
  | SingleInit e as init ->
    if vi.vglob then Global_observer.add_initializer vi off init;
    let e, env = replace_literal_string_in_exp env kf_opt e in
    SingleInit e, env
45
  | CompoundInit(typ, l) ->
46
47
    (* inject in all single initializers that can be built from the compound
       version *)
Julien Signoles's avatar
Julien Signoles committed
48
49
    let l, env =
      List.fold_left
50
51
52
53
        (fun (l, env) (off', i) ->
           let new_off = Cil.addOffset off' off in
           let i, env = inject_in_init env kf_opt vi new_off i in
           (off', i) :: l, env)
Julien Signoles's avatar
Julien Signoles committed
54
55
56
57
        ([], env)
        l
    in
    CompoundInit(typ, List.rev l), env
58

Julien Signoles's avatar
Julien Signoles committed
59
let inject_in_local_init loc env kf vi = function
60
  | ConsInit (fvi, sz :: _, _) as init
Julien Signoles's avatar
Julien Signoles committed
61
62
63
64
65
66
67
68
69
70
71
72
    when Functions.Libc.is_vla_alloc_name fvi.vname ->
    (* handle variable-length array allocation via [__fc_vla_alloc].  Here each
       instance of [__fc_vla_alloc] is rewritten to [alloca] (that is used to
       implement VLA) and further a custom call to [store_block] tracking VLA
       allocation is issued. *)
    (* KV: do not add handling [alloca] allocation here (or anywhere else for
       that matter). Handling of [alloca] should be implemented in Frama-C
       (eventually). This is such that each call to [alloca] becomes
       [__fc_vla_alloc]. It is already handled using the code below. *)
    fvi.vname <- Functions.Libc.actual_alloca;
    (* Since we need to pass [vi] by value, cannot use [Misc.mk_store_stmt]
       here. Do it manually. *)
73
    let store = Constructor.mk_store_stmt ~str_size:sz vi in
Julien Signoles's avatar
Julien Signoles committed
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
    let env = Env.add_stmt ~post:true env kf store in
    init, env

  | ConsInit (fvi, args, kind)
    when Options.Validate_format_strings.get ()
      && Functions.Libc.is_printf_name fvi.vname
    ->
    (* rewrite format functions (e.g., [printf]). *)
    let name = Functions.RTL.get_rtl_replacement_name fvi.vname in
    let new_vi = Misc.get_lib_fun_vi name in
    let fmt = Functions.Libc.get_printf_argument_str ~loc fvi.vname args in
    ConsInit(new_vi, fmt :: args, kind), env

  | ConsInit (fvi, _, _) as init
    when Options.Replace_libc_functions.get ()
      && Functions.RTL.has_rtl_replacement fvi.vname
    ->
    (* rewrite names of functions for which we have alternative definitions in
       the RTL. *)
    fvi.vname <- Functions.RTL.get_rtl_replacement_name fvi.vname;
    init, env

Julien Signoles's avatar
Julien Signoles committed
96
97
98
99
  | AssignInit init ->
    let init, env = inject_in_init env (Some kf) vi NoOffset init in
    AssignInit init, env

100
  | ConsInit(vi, l, ck) ->
Julien Signoles's avatar
Julien Signoles committed
101
    let l, env =
102
103
      List.fold_right
        (fun e (l, env) ->
Julien Signoles's avatar
Julien Signoles committed
104
105
106
           let e, env = replace_literal_string_in_exp env (Some kf) e in
           e :: l, env)
        l
107
        ([], env)
Julien Signoles's avatar
Julien Signoles committed
108
109
    in
    ConsInit(vi, l, ck), env
Julien Signoles's avatar
Julien Signoles committed
110

111
112
113
114
(* ************************************************************************** *)
(* Instructions and statements *)
(* ************************************************************************** *)

Julien Signoles's avatar
Julien Signoles committed
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
(* rewrite names of functions for which we have alternative definitions in the
   RTL. *)
let rename_caller loc args exp = match exp.enode with
  | Lval(Var vi, _)
    when Options.Replace_libc_functions.get ()
      && Functions.RTL.has_rtl_replacement vi.vname
    ->
    vi.vname <- Functions.RTL.get_rtl_replacement_name vi.vname;
    exp, args

  | Lval(Var vi , _) when Functions.Libc.is_vla_free_name vi.vname ->
    (* handle variable-length array allocation via [__fc_vla_free]. Rewrite its
       name to [delete_block]. The rest is in place. *)
    vi.vname <- Functions.RTL.mk_api_name "delete_block";
    exp, args

  | Lval(Var vi, _)
    when Options.Validate_format_strings.get ()
      && Functions.Libc.is_printf_name vi.vname
    ->
    (* rewrite names of format functions (such as printf). This case differs
       from the above because argument list of format functions is extended with
       an argument describing actual variadic arguments *)
    (* replacement name, e.g., [printf] -> [__e_acsl_builtin_printf] *)
    let name = Functions.RTL.get_rtl_replacement_name vi.vname in
    (* variadic arguments descriptor *)
    let fmt = Functions.Libc.get_printf_argument_str ~loc vi.vname args in
    (* get the name of the library function we need. Cannot just rewrite the
       name as AST check will then fail *)
    let vi = Misc.get_lib_fun_vi name in
    Cil.evar vi, fmt :: args

  | _ ->
    exp, args

(* TODO: should be better documented *)
let add_initializer loc ?vi lv ?(post=false) stmt env kf =
  if Functions.instrument kf then
    let may_safely_ignore = function
      | Var vi, NoOffset -> vi.vglob || vi.vformal
      | _ -> false
    in
    let must_model = Mmodel_analysis.must_model_lval ~stmt ~kf lv in
    if not (may_safely_ignore lv) && must_model then
159
      let before = Cil.mkStmt ~valid_sid:true stmt.skind in
Julien Signoles's avatar
Julien Signoles committed
160
161
162
      let new_stmt =
        (* bitfields are not yet supported ==> no initializer.
           a [not_yet] will be raised in [Translate]. *)
163
164
        if Cil.isBitfield lv then Cil.mkEmptyStmt ()
        else Constructor.mk_initialize ~loc lv
165
      in
Julien Signoles's avatar
Julien Signoles committed
166
167
168
169
      let env = Env.add_stmt ~post ~before env kf new_stmt in
      let env = match vi with
        | None -> env
        | Some vi ->
170
          let new_stmt = Constructor.mk_store_stmt vi in
Julien Signoles's avatar
Julien Signoles committed
171
172
173
          Env.add_stmt ~post ~before env kf new_stmt
      in
      env
174
175
    else
      env
Julien Signoles's avatar
Julien Signoles committed
176
177
178
  else
    env

Julien Signoles's avatar
Julien Signoles committed
179
let inject_in_instr env kf stmt = function
Julien Signoles's avatar
Julien Signoles committed
180
  | Set(lv, e, loc) ->
Julien Signoles's avatar
Julien Signoles committed
181
    let e, env = replace_literal_string_in_exp env (Some kf) e in
Julien Signoles's avatar
Julien Signoles committed
182
183
184
185
186
187
188
    let env = add_initializer loc lv stmt env kf in
    Set(lv, e, loc), env

  | Call(result, caller, args, loc) ->
    let args, env =
      List.fold_right
        (fun a (args, env) ->
Julien Signoles's avatar
Julien Signoles committed
189
           let a, env = replace_literal_string_in_exp env (Some kf) a in
Julien Signoles's avatar
Julien Signoles committed
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
           a :: args, env)
        args
        ([], env)
    in
    let caller, args = rename_caller loc args caller in
    (* add statement tracking initialization of return values *)
    let env =
      match result with
      | Some lv when not (Functions.RTL.is_generated_kf kf) ->
        add_initializer loc lv ~post:false stmt env kf
      | _ ->
        env
    in
    Call(result, caller, args, loc), env

  | Local_init(vi, linit, loc) ->
    let lv = Var vi, NoOffset in
207
    let env = add_initializer loc ~vi lv ~post:true stmt env kf in
Julien Signoles's avatar
Julien Signoles committed
208
209
210
211
212
213
    let linit, env = inject_in_local_init loc env kf vi linit in
    Local_init(vi, linit, loc), env

  (* nothing to do: *)
  | Asm _
  | Skip _
Julien Signoles's avatar
Julien Signoles committed
214
  | Code_annot _ as instr ->
Julien Signoles's avatar
Julien Signoles committed
215
    instr, env
216

Julien Signoles's avatar
Julien Signoles committed
217
218
219
let add_new_block_in_stmt env kf stmt =
  (* Add temporal analysis instrumentations *)
  let env = Temporal.handle_stmt stmt env kf in
220
  let new_stmt, env =
Julien Signoles's avatar
Julien Signoles committed
221
222
223
224
225
226
227
228
229
230
231
232
    if Functions.check kf then
      let env =
        (* handle ghost statement *)
        if stmt.ghost then begin
          stmt.ghost <- false;
          (* translate potential RTEs of ghost code *)
          let rtes = Rte.stmt ~warn:false kf stmt in
          Translate.translate_rte_annots Printer.pp_stmt stmt kf env rtes
        end else
          env
      in
      (* handle loop invariants *)
233
234
      let new_stmt, env = Loops.preserve_invariant env kf stmt in
      new_stmt, env
Julien Signoles's avatar
Julien Signoles committed
235
    else
236
      stmt, env
Julien Signoles's avatar
Julien Signoles committed
237
238
239
240
241
242
243
244
245
246
247
  in
  let mk_post_env env stmt =
    Annotations.fold_code_annot
      (fun _ a env -> Translate.translate_post_code_annotation kf env a)
      stmt
      env
  in
  let new_stmt, env =
    (* Remove local variables which scopes ended via goto/break/continue. *)
    let del_vars = Exit_points.delete_vars stmt in
    let env = Memory_observer.delete_from_set ~before:stmt env kf del_vars in
248
    if Kernel_function.is_return_stmt kf stmt then
Julien Signoles's avatar
Julien Signoles committed
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
      let env =
        if Functions.check kf then
          (* must generate the post_block before including [stmt] (the
             'return') since no code is executed after it. However, since
             this statement is pure (Cil invariant), that is semantically
             correct. *)
          (* [JS 2019/2/19] TODO: what about the other ways of early exiting
             a block? *)
          let env = mk_post_env env stmt in
          (* also handle the postcondition of the function and clear the
             env *)
          Translate.translate_post_spec kf env (Annotations.funspec kf)
        else
          env
      in
      (* de-allocating memory previously allocating by the kf *)
      (* remove recorded function arguments *)
      let fargs = Kernel_function.get_formals kf in
      let env = Memory_observer.delete_from_list env kf fargs in
      let b, env =
        Env.pop_and_get env new_stmt ~global_clear:true Env.After
      in
271
      if Kernel_function.is_main kf && Mmodel_analysis.use_model () then begin
Julien Signoles's avatar
Julien Signoles committed
272
273
274
275
276
277
278
        let stmts = b.bstmts in
        let l = List.rev stmts in
        match l with
        | [] -> assert false (* at least the 'return' stmt *)
        | ret :: l ->
          let loc = Stmt.loc stmt in
          let delete_stmts =
279
280
            Global_observer.mk_delete_stmts
              [ Constructor.mk_rtl_call ~loc "memory_clean" []; ret ]
Julien Signoles's avatar
Julien Signoles committed
281
282
283
          in
          b.bstmts <- List.rev l @ delete_stmts
      end;
284
      let new_stmt = Constructor.mk_block stmt b in
Julien Signoles's avatar
Julien Signoles committed
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
      if not (Cil_datatype.Stmt.equal stmt new_stmt) then begin
        (* move the labels of the return to the new block in order to
           evaluate the postcondition when jumping to them. *)
        E_acsl_label.move kf stmt new_stmt
      end;
      new_stmt, env
    else (* i.e. not (is_return stmt) *)
      (* must generate [pre_block] which includes [stmt] before generating
         [post_block] *)
      let pre_block, env =
        Env.pop_and_get
          ~split:true
          env
          new_stmt
          ~global_clear:false
          Env.After
      in
      let env =
        (* if [kf] is not monitored, do not translate any postcondition,
           but still push an empty environment consumed by
           [Env.pop_and_get] below. This [Env.pop_and_get] call is always
           required in order to generate the code not directly related to
           the annotations of the current stmt in anycase. *)
        if Functions.check kf then mk_post_env (Env.push env) stmt
        else Env.push env
      in
      let post_block, env =
        Env.pop_and_get
          env
314
          (Constructor.mk_block new_stmt pre_block)
Julien Signoles's avatar
Julien Signoles committed
315
316
317
318
319
320
321
322
          ~global_clear:false
          Env.Before
      in
      let post_block =
        if post_block.blocals = [] && new_stmt.labels = []
        then Cil.transient_block post_block
        else post_block
      in
323
      let res = Constructor.mk_block new_stmt post_block in
Julien Signoles's avatar
Julien Signoles committed
324
325
326
327
328
329
330
331
      if not (Cil_datatype.Stmt.equal new_stmt res) then
        E_acsl_label.move kf new_stmt res;
      res, env
  in
  Options.debug ~level:4
    "@[new stmt (from sid %d):@ %a@]" stmt.sid Printer.pp_stmt new_stmt;
  new_stmt, env

332
333
(* visit the substmts and build the new skind *)
let rec inject_in_substmt env kf stmt = match stmt.skind with
Julien Signoles's avatar
Julien Signoles committed
334
335
336
  | Instr instr ->
    let instr, env = inject_in_instr env kf stmt instr in
    Instr instr, env
337
338

  | Return(Some e, loc)  ->
Julien Signoles's avatar
Julien Signoles committed
339
    let e, env = replace_literal_string_in_exp env (Some kf) e in
340
341
342
343
344
    Return(Some e, loc), env

  | If(e, blk1, blk2, loc) ->
    let env = inject_in_block env kf blk1 in
    let env = inject_in_block env kf blk2 in
Julien Signoles's avatar
Julien Signoles committed
345
    let e, env = replace_literal_string_in_exp env (Some kf) e in
346
347
348
    If(e, blk1, blk2, loc), env

  | Switch(e, blk, stmts, loc) ->
349
    (* [blk] and [stmts] are visited at the same time *)
350
    let env = inject_in_block env kf blk in
Julien Signoles's avatar
Julien Signoles committed
351
    let e, env = replace_literal_string_in_exp env (Some kf) e in
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
    Switch(e, blk, stmts, loc), env

  | Loop(_ (* ignore AST annotations *), blk, loc, stmt_opt1, stmt_opt2) ->
    let env = inject_in_block env kf blk in
    let do_opt env = function
      | None -> None, env
      | Some stmt ->
        let stmt, env = inject_in_stmt env kf stmt in
        Some stmt, env
    in
    let stmt_opt1, env = do_opt env stmt_opt1 in
    let stmt_opt2, env = do_opt env stmt_opt2 in
    Loop([], blk, loc, stmt_opt1, stmt_opt2), env

  | Block blk as skind ->
    skind, inject_in_block env kf blk

  | UnspecifiedSequence l ->
    let l, env =
      List.fold_left
        (fun (l, env) (stmt, l1, l2, l3, srefs) ->
           let stmt, env = inject_in_stmt env kf stmt in
           (stmt, l1, l2, l3, srefs) :: l, env)
        ([], env)
        l
    in
378
    UnspecifiedSequence (List.rev l), env
379
380

  | Throw(Some(e, ty), loc) ->
Julien Signoles's avatar
Julien Signoles committed
381
    let e, env = replace_literal_string_in_exp env (Some kf) e in
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
    Throw(Some(e, ty), loc), env

  | TryCatch(blk, l, _loc) as skind ->
    let env = inject_in_block env kf blk in
    let env =
      List.fold_left
        (fun env (cb, blk) ->
           let env = inject_in_catch_binder env kf cb in
           inject_in_block env kf blk)
        env
        l
    in
    skind, env

  | TryFinally(blk1, blk2, _loc) as skind ->
    let env = inject_in_block env kf blk1 in
    let env = inject_in_block env kf blk2 in
    skind, env

Julien Signoles's avatar
Julien Signoles committed
401
402
  | TryExcept(_blk1, (_instrs, _e), _blk2, _loc) ->
    Error.not_yet "try ... except ..."
403
404
405
406
407
408
409
410
411
412

  (* nothing to do: *)
  | Throw(None, _)
  | Return(None, _)
  | Goto _ (* do not visit the internal stmt since it has already been handle *)
  | Break _
  | Continue _ as skind ->
    skind, env

and inject_in_stmt env kf stmt =
Julien Signoles's avatar
Julien Signoles committed
413
414
415
416
417
418
419
420
421
422
423
  Options.debug ~level:4
    "proceeding stmt (sid %d) %a@."
    stmt.sid Stmt.pretty stmt;
  (* pushing a new context *)
  let env = Env.push env in
  let env = match stmt.skind with
    | Loop _ -> Env.push_loop env
    | _ -> env
  in
  (* initial environment *)
  let env =
424
    if Kernel_function.is_first_stmt kf stmt then
Julien Signoles's avatar
Julien Signoles committed
425
      let env =
426
        if Kernel_function.is_main kf then
Julien Signoles's avatar
Julien Signoles committed
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
          env
        else
          let env =
            Memory_observer.store env kf (Kernel_function.get_formals kf)
          in
          Temporal.handle_function_parameters kf env
      in
      (* translate the precondition of the function *)
      if Functions.check kf then
        let funspec = Annotations.funspec kf in
        Translate.translate_pre_spec kf env funspec
      else env
    else
      env
  in
  (* translate code annotations *)
  let env =
    if Functions.check kf then
      Annotations.fold_code_annot
        (fun _ a env -> Translate.translate_pre_code_annotation kf env a)
        stmt
        env
    else
      env
  in
  (* add [__e_acsl_store_duplicate] calls for local variables which declarations
     are bypassed by gotos. Note: should be done before visiting instructions
     (which adds initializers), otherwise init calls appear before store
     calls. *)
  let duplicates = Exit_points.store_vars stmt in
  let env = Memory_observer.duplicate_store ~before:stmt env kf duplicates in
458
459
  let skind, env = inject_in_substmt env kf stmt in
  stmt.skind <- skind;
Julien Signoles's avatar
Julien Signoles committed
460
461
462
  (* building the new block of code *)
  add_new_block_in_stmt env kf stmt

463
and inject_in_block (env: Env.t) kf blk =
Julien Signoles's avatar
Julien Signoles committed
464
  let stmts, env =
465
466
    List.fold_left
      (fun (stmts, env) stmt ->
Julien Signoles's avatar
Julien Signoles committed
467
468
469
         let stmt, env = inject_in_stmt env kf stmt in
         stmt :: stmts, env)
      ([], env)
470
      blk.bstmts
Julien Signoles's avatar
Julien Signoles committed
471
  in
472
  blk.bstmts <- List.rev stmts;
473
  (* now inject code that de-allocates the necessary observation variables and
474
475
     blocks of the runtime memory that have been previously allocated *)
  (* calls to [free] for de-allocating variables observing \at(_,_) *)
476
477
478
  let free_stmts = At_with_lscope.Free.find_all kf in
  match blk.blocals, free_stmts with
  | [], [] ->
Julien Signoles's avatar
Julien Signoles committed
479
    env
480
  | [], _ :: _ | _ :: _, [] | _ :: _, _ :: _ ->
481
482
    (* [TODO] this piece of code could be improved *)
    (* de-allocate the memory blocks observing locals *)
483
484
485
486
    let add_locals stmts =
      if Functions.instrument kf then
        List.fold_left
          (fun acc vi ->
487
488
489
             if Mmodel_analysis.must_model_vi ~kf vi
             then Constructor.mk_delete_stmt vi :: acc
             else acc)
490
491
492
493
494
          stmts
          blk.blocals
      else
        stmts
    in
495
    (* select the precise location to inject these pieces of code *)
496
497
498
499
500
    let rec insert_in_innermost_last_block blk = function
      | { skind = Return _ } as ret :: ((potential_clean :: tl) as l) ->
        (* keep the return (enclosed in a generated block) at the end;
           preceded by clean if any *)
        let init, tl =
501
          if Kernel_function.is_main kf && Mmodel_analysis.use_model () then
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
            free_stmts @ [ potential_clean; ret ], tl
          else
            free_stmts @ [ ret ], l
        in
        (* now that [free] stmts for [kf] have been inserted,
           there is no more need to keep the corresponding entries in the
           table managing them. *)
        At_with_lscope.Free.remove_all kf;
        blk.bstmts <-
          List.fold_left (fun acc v -> v :: acc) (add_locals init) tl
      | { skind = Block b } :: _ ->
        insert_in_innermost_last_block b (List.rev b.bstmts)
      | l ->
        blk.bstmts <- List.fold_left (fun acc v -> v :: acc) (add_locals []) l
    in
    insert_in_innermost_last_block blk (List.rev blk.bstmts);
    if Functions.instrument kf then
      blk.bstmts <-
        List.fold_left
          (fun acc vi ->
             if Mmodel_analysis.must_model_vi vi && not vi.vdefined
523
             then Constructor.mk_store_stmt vi :: acc
524
525
             else acc)
          blk.bstmts
Julien Signoles's avatar
Julien Signoles committed
526
527
          blk.blocals;
    env
528

529
530
531
532
533
534
and inject_in_catch_binder env kf = function
  | Catch_exn(_, l) ->
    List.fold_left (fun env (_, blk) -> inject_in_block env kf blk) env l
  | Catch_all ->
    env

535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
(* ************************************************************************** *)
(* Function definition *)
(* ************************************************************************** *)

let add_generated_variables_in_function env fundec =
  let vars = Env.get_generated_variables env in
  let locals, blocks =
    List.fold_left
      (fun (local_vars, block_vars as acc) (v, scope) -> match scope with
         (* TODO: [kf] assumed to be consistent. Should be asserted. *)
         (* TODO: actually, is the kf as constructor parameter useful? *)
         | Env.LFunction _kf -> v :: local_vars, v :: block_vars
         | Env.LLocal_block _kf -> v :: local_vars, block_vars
         | _ -> acc)
      (fundec.slocals, fundec.sbody.blocals)
      vars
  in
  fundec.slocals <- locals;
  fundec.sbody.blocals <- blocks

(* Memory management for \at on purely logic variables: put [malloc] stmts at
   proper locations *)
let add_malloc_and_free_stmts kf fundec =
  let malloc_stmts = At_with_lscope.Malloc.find_all kf in
  let fstmts = malloc_stmts @ fundec.sbody.bstmts in
  fundec.sbody.bstmts <- fstmts;
  (* now that [malloc] stmts for [kf] have been inserted, there is no more need
     to keep the corresponding entries in the table managing them. *)
  At_with_lscope.Malloc.remove_all kf

565
let inject_in_fundec main fundec =
566
567
568
569
570
  let vi = fundec.svar in
  let kf = try Globals.Functions.get vi with Not_found -> assert false in
  (* convert ghost variables *)
  vi.vghost <- false;
  List.iter (fun vi -> vi.vghost <- false) fundec.slocals;
571
572
573
574
575
  let unghost_formal vi =
    vi.vghost <- false ;
    vi.vattr <- Cil.dropAttribute Cil.frama_c_ghost_formal vi.vattr
  in
  List.iter unghost_formal fundec.sformals;
576
577
  (* update environments *)
  Builtins.update vi.vname vi;
578
579
  (* track function addresses but the main function that is tracked internally
     via RTL *)
580
  if not (Kernel_function.is_main kf) then Global_observer.add vi;
581
582
  (* exit point computations *)
  if Functions.instrument kf then Exit_points.generate fundec;
583
  (* recursive visit *)
584
585
  Options.feedback ~dkey ~level:2 "entering in function %a."
    Kernel_function.pretty kf;
586
  let env = inject_in_block Env.empty kf fundec.sbody in
587
588
589
590
  Exit_points.clear ();
  add_generated_variables_in_function env fundec;
  add_malloc_and_free_stmts kf fundec;
  (* setting main if necessary *)
591
  let main = if Kernel_function.is_main kf then Some fundec else main in
592
593
594
595
596
597
598
599
  Options.feedback ~dkey ~level:2 "function %a done."
    Kernel_function.pretty kf;
  env, main

(* ************************************************************************** *)
(* The whole AST *)
(* ************************************************************************** *)

600
601
602
603
604
605
606
607
608
609
610
611
let unghost_vi vi =
  (* do not convert extern ghost variables, because they can't be linked,
     see bts #1392 *)
  if vi.vstorage <> Extern then vi.vghost <- false;
  match Cil.unrollType vi.vtype with
  | TFun(res, Some l, va, attr) ->
    (* unghostify function's parameters *)
    let retype (n, t, a) = n, t, Cil.dropAttribute Cil.frama_c_ghost_formal a in
    vi.vtype <- TFun(res, Some (List.map retype l), va, attr)
  | _ ->
    ()

612
613
614
615
616
617
618
619
620
621
622
let inject_in_global (env, main) = function
  (* library functions and built-ins *)
  | GVarDecl(vi, _) | GVar(vi, _, _)
  | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
    when Misc.is_library_loc vi.vdecl || Builtins.mem vi.vname ->
    Misc.register_library_function vi;
    if Builtins.mem vi.vname then Builtins.update vi.vname vi;
    env, main

  (* Cil built-ins and other library globals: nothing to do *)
  | GVarDecl(vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _)
623
    when Misc.is_fc_or_compiler_builtin vi ->
624
625
626
627
    env, main
  | g when Misc.is_library_loc (Global.loc g) ->
    env, main

628
  (* variable declarations *)
629
  | GVarDecl(vi, _) | GFunDecl(_, vi, _) ->
630
    unghost_vi vi;
631
    Global_observer.add vi;
632
633
634
    env, main

  (* variable definition *)
Julien Signoles's avatar
Julien Signoles committed
635
636
  | GVar(vi, { init = None }, _) ->
    Global_observer.add vi;
637
    unghost_vi vi;
Julien Signoles's avatar
Julien Signoles committed
638
639
640
641
    env, main

  | GVar(vi, { init = Some init }, _) ->
    Global_observer.add vi;
642
    unghost_vi vi;
Julien Signoles's avatar
Julien Signoles committed
643
644
645
646
    let _init, env = inject_in_init env None vi NoOffset init in
    (* ignore the new initializer that handles literal strings since they are
       not substituted in global initializers (see
       [replace_literal_string_in_exp]) *)
647
648
649
    env, main

  (* function definition *)
650
651
  | GFun({ svar = vi } as fundec, _) ->
    unghost_vi vi;
652
    inject_in_fundec main fundec
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667

  (* other globals: nothing to do *)
  | GType _
  | GCompTag _
  | GCompTagDecl _
  | GEnumTag _
  | GEnumTagDecl _
  | GAsm _
  | GPragma _
  | GText _
  | GAnnot _ (* do never read annotation from sources *)
    ->
    env, main

(* TODO: what about using [file.globalinit]? *)
668
let inject_global_initializer file main =
669
  Options.feedback ~dkey ~level:2 "building global initializer.";
670
  let vi, fundec = Global_observer.mk_init_function () in
671
672
673
674
675
676
677
678
679
680
681
  let cil_fct = GFun(fundec, Location.unknown) in
  if Mmodel_analysis.use_model () then begin
    match main with
    | Some main ->
      let exp = Cil.evar ~loc:Location.unknown vi in
      (* Create [__e_acsl_globals_init();] call *)
      let stmt =
        Cil.mkStmtOneInstr ~valid_sid:true
          (Call(None, exp, [], Location.unknown))
      in
      vi.vreferenced <- true;
682
      (* insert [__e_acsl_globals_init ();] as first statement of [main] *)
683
684
      main.sbody.bstmts <- stmt :: main.sbody.bstmts;
      let new_globals =
685
686
        List.fold_left
          (fun acc g -> match g with
687
             | GFun({ svar = vi }, _) when Varinfo.equal vi main.svar -> acc
688
             | _ -> g :: acc)
689
          []
690
          file.globals
691
      in
692
693
694
695
696
697
698
699
700
      let new_globals =
        let rec rev_and_extend acc = function
          | [] -> acc
          | f :: l -> rev_and_extend (f :: acc) l
        in
        (* [__e_acsl_globals_init] and [main] at the end *)
        rev_and_extend [ cil_fct; GFun(main, Location.unknown) ] new_globals
      in
      (* add the literal string varinfos as the very first globals *)
701
702
      let new_globals =
        Literal_strings.fold
703
          (fun _ vi l -> GVar(vi, { init = None }, Location.unknown) :: l)
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
          new_globals
      in
      file.globals <- new_globals
    | None ->
      Kernel.warning "@[no entry point specified:@ \
                      you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
        Global_observer.function_name;
      file.globals <- file.globals @ [ cil_fct ]
  end

(* Add a call to [__e_acsl_memory_init] that initializes memory storage and
   potentially records program arguments. Parameters to [__e_acsl_memory_init]
   are addresses of program arguments or NULLs if [main] is declared without
   arguments. *)
let inject_mmodel_initializer main =
  let loc = Location.unknown in
  let nulls = [ Cil.zero loc ; Cil.zero loc ] in
  let handle_main main =
    let args =
723
      (* record arguments only if the second has a pointer type, so argument
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
         strings can be recorded. This is sufficient to capture C99 compliant
         arguments and GCC extensions with environ. *)
      match main.sformals with
      | [] ->
        (* no arguments to main given *)
        nulls
      | _argc :: argv :: _ when Cil.isPointerType argv.vtype ->
        (* grab addresses of arguments for a call to the main initialization
           function, i.e., [__e_acsl_memory_init] *)
        List.map Cil.mkAddrOfVi main.sformals;
      | _ :: _ ->
        (* some non-standard arguments. *)
        nulls
    in
    let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
    let args = args @ [ ptr_size ] in
740
    let init = Constructor.mk_rtl_call loc "memory_init" args in
741
742
743
744
745
    main.sbody.bstmts <- init :: main.sbody.bstmts
  in
  Extlib.may handle_main main

let inject_in_file file =
746
  let _env, main =
747
748
749
750
751
    List.fold_left inject_in_global (Env.empty, None) file.globals
  in
  (* post-treatment *)
  (* extend [main] with forward initialization and put it at end *)
  if not (Global_observer.is_empty () && Literal_strings.is_empty ()) then
752
    inject_global_initializer file main;
753
754
755
  file.globals <- Logic_functions.add_generated_functions file.globals;
  inject_mmodel_initializer main

756
let reset_all ast =
757
  (* by default, do not run E-ACSL on the generated code *)
758
  Options.Run.off ();
759
  (* reset all the E-ACSL environments to their original states *)
760
  Mmodel_analysis.reset ();
761
762
763
764
  Misc.reset ();
  Logic_functions.reset ();
  Literal_strings.reset ();
  Global_observer.reset ();
765
  Typing.clear ();
766
767
  (* reset some kernel states: *)
  (* reset the CFG that has been heavily modified by the code generation step *)
768
769
  Cfg.clearFileCFG ~clear_id:false ast;
  Cfg.computeFileCFG ast;
770
771
  (* notify the kernel that new code has been generated (but we have kept the
     old one) *)
772
  Ast.mark_as_grown ()
773
774
775
776
777

let inject () =
  Options.feedback ~level:2
    "injecting annotations as code in project %a"
    Project.pretty (Project.current ());
778
  Keep_status.before_translation ();
779
  Misc.reorder_ast ();
780
  Gmp_types.init ();
781
782
  let ast = Ast.get () in
  inject_in_file ast;
783
  reset_all ast;
784

Julien Signoles's avatar
Julien Signoles committed
785
786
(*
Local Variables:
787
compile-command: "make -C ../../../../.."
Julien Signoles's avatar
Julien Signoles committed
788
789
End:
*)