dup_functions.ml 15.8 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
(*                                                                        *)
5
(*  Copyright (C) 2012-2019                                               *)
Virgile Prevosto's avatar
Virgile Prevosto committed
6
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
7
8
9
10
11
12
13
14
15
16
17
18
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
Virgile Prevosto's avatar
Virgile Prevosto committed
19
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
20
21
22
23
24
(*                                                                        *)
(**************************************************************************)

open Cil_types

25
26
let dkey = Options.dkey_dup

27
28
29
30
31
32
(* ********************************************************************** *)
(* Environment *)
(* ********************************************************************** *)

let fct_tbl: unit Kernel_function.Hashtbl.t = Kernel_function.Hashtbl.create 7

33
34
let actions = Queue.create ()

35
36
37
38
39
40
41
42
43
44
45
46
47
module Global: sig
  val add_logic_info: logic_info -> unit
  val mem_logic_info: logic_info -> bool
  val reset: unit -> unit
end = struct

  let tbl = Cil_datatype.Logic_info.Hashtbl.create 7
  let add_logic_info x = Cil_datatype.Logic_info.Hashtbl.add tbl x ()
  let mem_logic_info x = Cil_datatype.Logic_info.Hashtbl.mem tbl x
  let reset () = Cil_datatype.Logic_info.Hashtbl.clear tbl

end

48
let reset () =
49
  Kernel_function.Hashtbl.clear fct_tbl;
50
51
52
  Global.reset ();
  Queue.clear actions

53
54
55
56
57
58
59
(* ********************************************************************** *)
(* Duplicating functions *)
(* ********************************************************************** *)

let dup_funspec tbl bhv spec =
  (*  Options.feedback "DUP SPEC %a" Cil.d_funspec spec;*)
  let o = object
60
    inherit Cil.genericCilVisitor bhv
61
62
63

    val already_visited = Cil_datatype.Logic_var.Hashtbl.create 7

64
    method !vlogic_info_use li =
65
      if Global.mem_logic_info li then
66
67
68
        Cil.ChangeDoChildrenPost
          ({ li with l_var_info = li.l_var_info } (* force a copy *),
           Visitor_behavior.Get.logic_info bhv)
69
      else
70
        Cil.JustCopy
71

72
    method !vterm_offset _ =
73
      Cil.DoChildrenPost
74
75
76
77
78
79
80
        (function (* no way to directly visit fieldinfo and model_info uses *)
          | TField(fi, off) ->
            TField(Visitor_behavior.Get.fieldinfo bhv fi, off)
          | TModel(mi, off) ->
            TModel(Visitor_behavior.Get.model_info bhv mi, off)
          | off ->
            off)
81

82
    method !vlogic_var_use orig_lvi =
83
      match orig_lvi.lv_origin with
84
85
      | None ->
        Cil.JustCopy
86
      | Some vi ->
87
88
89
90
91
92
93
94
95
        try
          let new_lvi =
            Cil_datatype.Logic_var.Hashtbl.find already_visited orig_lvi
          in
          Cil.ChangeTo new_lvi
        with Not_found ->
          Cil.ChangeDoChildrenPost
            ({ orig_lvi with lv_id = orig_lvi.lv_id } (* force a copy *),
             fun lvi ->
96
97
98
               (* using [Visitor_behavior.Get.logic_var bhv lvi] is correct only
                  because the lv_id used to compare the lvi does not change
                  between the original one and this copy *)
99
100
101
102
103
104
105
106
107
108
109
110
111
112
               try
                 let new_vi = Cil_datatype.Varinfo.Hashtbl.find tbl vi in
                 Cil_datatype.Logic_var.Hashtbl.add
                   already_visited orig_lvi lvi;
                 lvi.lv_id <- new_vi.vid;
                 lvi.lv_name <- new_vi.vname;
                 lvi.lv_origin <- Some new_vi;
                 new_vi.vlogic_var_assoc <- Some lvi;
                 lvi
               with Not_found ->
                 assert vi.vglob;
                 Visitor_behavior.Get.logic_var bhv lvi)

    method !videntified_term _ =
113
114
      Cil.DoChildrenPost Logic_const.refresh_identified_term

115
    method !videntified_predicate _ =
116
117
118
119
      Cil.DoChildrenPost Logic_const.refresh_predicate
  end in
  Cil.visitCilFunspec o spec

120
let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
121
122
  new_vi.vdefined <- true;
  let formals = Kernel_function.get_formals kf in
123
124
125
  let mk_formal vi =
    let name =
      if vi.vname = "" then
Andre Maroneze's avatar
Andre Maroneze committed
126
        (* unnamed formal parameter: must generate a fresh name since a fundec
Julien Signoles's avatar
Julien Signoles committed
127
           cannot have unnamed formals (see bts #2303). *)
128
129
        Varname.get
          ~scope:Varname.Function
130
          (Functions.RTL.mk_gen_name "unamed_formal")
131
132
133
134
135
136
      else
        vi.vname
    in
    Cil.copyVarinfo vi name
  in
  let new_formals = List.map mk_formal formals in
137
138
139
  let res =
    let ty = Kernel_function.get_return_type kf in
    if Cil.isVoidType ty then None
140
    else Some (Cil.makeVarinfo false false ~referenced:true "__retres" ty)
141
142
143
144
145
  in
  let return =
    Cil.mkStmt ~valid_sid:true
      (Return(Extlib.opt_map (Cil.evar ~loc) res, loc))
  in
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
  let stmts =
    let l =
      [ Cil.mkStmtOneInstr ~valid_sid:true
          (Call(Extlib.opt_map Cil.var res,
                Cil.evar ~loc vi,
                List.map (Cil.evar ~loc) new_formals,
                loc));
        return ]
    in
    if Functions.instrument kf then
      l
    else
      (* set the 'unsound_verdict' variable to 'false' whenever required *)
      let unsound =
        Cil.mkStmtOneInstr ~valid_sid:true
          (Set((Var sound_verdict_vi, NoOffset), Cil.zero ~loc, loc))
      in
      unsound :: l
164
165
166
167
168
169
170
  in
  let locals = match res with None -> [] | Some r -> [ r ] in
  let body = Cil.mkBlock stmts in
  body.blocals <- locals;
  let tbl = Cil_datatype.Varinfo.Hashtbl.create 7 in
  List.iter2 (Cil_datatype.Varinfo.Hashtbl.add tbl) formals new_formals;
  let new_spec = dup_funspec tbl bhv spec in
171
172
173
174
175
176
177
178
179
180
181
182
183
184
  let fundec =
    { svar = new_vi;
      sformals = new_formals;
      slocals = locals;
      smaxid = List.length new_formals;
      sbody = body;
      smaxstmtid = None;
      sallstmts = [];
      sspec = new_spec }
  in
  (* compute the CFG of the new [fundec] *)
  Cfg.clearCFGinfo ~clear_id:false fundec;
  Cfg.cfgFun fundec;
  fundec
185

186
let dup_global loc actions spec bhv sound_verdict_vi kf vi new_vi =
187
188
  let name = vi.vname in
  Options.feedback ~dkey ~level:2 "entering in function %s" name;
189
  let fundec = dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi  in
190
  let fct = Definition(fundec, loc) in
191
  let new_spec = fundec.sspec in
192
  let new_kf = { fundec = fct; spec = new_spec } in
193
194
195
196
  Queue.add (fun () ->
      Kernel_function.Hashtbl.add fct_tbl new_kf ();
      Globals.Functions.register new_kf;
      Globals.Functions.replace_by_definition new_spec fundec loc;
197
198
199
200
201
202
203
      Annotations.register_funspec new_kf;
      if new_vi.vname = "main" then begin
        (* recompute the info about the old main since its name has changed;
           see the corresponding part in the main visitor *)
        Globals.Functions.remove vi;
        Globals.Functions.register kf
      end)
204
    actions;
205
  Options.feedback ~dkey ~level:2 "function %s" name;
206
207
208
  (* remove the specs attached to the previous kf iff it is a definition:
     it is necessary to keep stable the number of annotations in order to get
     [Keep_status] working fine. *)
209
  let kf = Visitor_behavior.Get.kernel_function bhv kf in
210
211
212
  if Kernel_function.is_definition kf then begin
    Queue.add
      (fun () ->
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
         let bhvs =
           Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
         in
         List.iter
           (fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
           bhvs;
         Annotations.iter_decreases
           (fun e _ -> Annotations.remove_decreases e kf)
           kf;
         Annotations.iter_terminates
           (fun e _ -> Annotations.remove_terminates e kf)
           kf;
         Annotations.iter_complete
           (fun e l -> Annotations.remove_complete e kf l)
           kf;
         Annotations.iter_disjoint
           (fun e l -> Annotations.remove_disjoint e kf l)
           kf)
231
232
      actions
  end;
233
  GFun(fundec, loc), GFunDecl(new_spec, new_vi, loc)
234
235
236
237
238

(* ********************************************************************** *)
(* Visitor *)
(* ********************************************************************** *)

239
type position = Before_gmp | Gmpz | After_gmp | Memory_model | Code
240

241
242
class dup_functions_visitor = object (self)
  inherit Visitor.frama_c_inplace
243

244
245
246
247
248
249
250
251
252
253
254
255
  val unduplicable_functions =
    let white_list =
      [ "__builtin_va_arg";
        "__builtin_va_end";
        "__builtin_va_start";
        "__builtin_va_copy" ]
    in
    List.fold_left
      (fun acc s -> Datatype.String.Set.add s acc)
      Datatype.String.Set.empty
      white_list

256
  val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
257
  val mutable before_memory_model = Before_gmp
258
259
  val mutable new_definitions: global list = []
  (* new definitions of the annotated functions which will contain the
Andre Maroneze's avatar
Andre Maroneze committed
260
     translation of the E-ACSL contract *)
261

262
263
  val mutable sound_verdict_vi =
    let name = Functions.RTL.mk_api_name "sound_verdict" in
264
    let vi = Cil.makeGlobalVar name Cil.intType in
265
266
267
268
    vi.vstorage <- Extern;
    vi.vreferenced <- true;
    vi

269
  method private before_memory_model = match before_memory_model with
270
271
    | Before_gmp | Gmpz | After_gmp -> true
    | Memory_model | Code -> false
272
273
274
275

  method private next () =
    match before_memory_model with
    | Before_gmp -> ()
276
    | Gmpz -> before_memory_model <- After_gmp
277
278
279
280
    | After_gmp -> ()
    | Memory_model -> before_memory_model <- Code
    | Code -> ()

281
  method !vlogic_info_decl li =
282
    Global.add_logic_info li;
283
    Cil.SkipChildren
284

285
  method !vvrbl vi =
286
287
288
289
    try
      let new_vi = Cil_datatype.Varinfo.Hashtbl.find fct_tbl vi in
      Cil.ChangeTo new_vi
    with Not_found ->
290
      Cil.SkipChildren
291

292
  method private is_variadic_function vi =
293
    match Cil.unrollType vi.vtype with
294
295
    | TFun(_, _, variadic, _) -> variadic
    | _ -> true
296

297
  method !vglob_aux = function
298
    | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
299
300
      when (* duplicate a function iff: *)
        not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
301
302
303
        (* it is not already duplicated *)
        && not (Datatype.String.Set.mem vi.vname unduplicable_functions)
        (* it is duplicable *)
304
305
        && not (self#is_variadic_function vi)
        (* it is not a variadic function *)
306
        && not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
307
        && not (Misc.is_fc_or_compiler_builtin vi) (* it is not a built-in *)
308
309
310
311
312
        &&
        (let kf =
           try Globals.Functions.get vi with Not_found -> assert false
         in
         not (Functions.instrument kf)
313
314
315
         (* either explicitely listed as to be not instrumented *)
         ||
         (* or: *)
316
317
318
         (not (Cil.is_empty_funspec
                 (Annotations.funspec ~populate:false
                    (Extlib.the self#current_kf)))
319
320
321
          (* it has a function contract *)
          && Functions.check kf
          (* its annotations must be monitored *)))
322
      ->
323
324
      self#next ();
      let name = Functions.RTL.mk_gen_name vi.vname in
325
      let new_vi = Cil.makeGlobalVar name vi.vtype in
326
327
328
      Cil_datatype.Varinfo.Hashtbl.add fct_tbl vi new_vi;
      Cil.DoChildrenPost
        (fun l -> match l with
329
330
           | [ GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
               as g ]
331
332
333
             ->
             (match g with
              | GFunDecl _ ->
334
335
                let kf = Extlib.the self#current_kf in
                if not (Kernel_function.is_definition kf)
336
337
338
                && vi.vname <> "malloc" && vi.vname <> "free"
                then
                  Options.warning "@[annotating undefined function `%a':@ \
339
340
341
                                   the generated program may miss memory \
                                   instrumentation@ if there are \
                                   memory-related annotations.@]"
342
343
344
345
                    Printer.pp_varinfo vi
              | GFun _ -> ()
              | _ -> assert false);
             let tmp = vi.vname in
346
347
348
             if tmp = "main" then begin
               (* the new function becomes the new main: *)
               (* 1. swap the name of both functions *)
349
               vi.vname <- new_vi.vname;
350
351
352
353
354
355
356
357
358
359
               new_vi.vname <- tmp;
               (* 2. force recomputation of the entry point if necessary *)
               if Kernel.MainFunction.get () = tmp then begin
                 let selection =
                   State_selection.with_dependencies Kernel.MainFunction.self
                 in
                 Project.clear ~selection ()
               end
               (* 3. recompute what is necessary in [Globals.Functions]:
                  done in [dup_global] *)
360
361
362
             end;
             let kf =
               try
363
                 Globals.Functions.get vi
364
365
366
367
368
369
370
371
372
373
374
375
376
377
               with Not_found ->
                 Options.fatal
                   "unknown function `%s' while trying to duplicate it"
                   vi.vname
             in
             let spec = Annotations.funspec ~populate:false kf in
             let new_g, new_decl =
               dup_global
                 loc
                 self#get_filling_actions
                 spec
                 self#behavior
                 sound_verdict_vi
                 kf
378
                 vi
379
380
381
382
383
                 new_vi
             in
             (* postpone the introduction of the new function definition to the
                end *)
             new_definitions <- new_g :: new_definitions;
384
385
             (* put the declaration before the original function in order to
                solve issue with recursive functions *)
386
387
388
389
390
391
392
393
394
395
             [ new_decl; g ]
           | _ -> assert false)
    | GVarDecl(_, loc) | GFunDecl(_, _, loc) | GFun(_, loc)
      when Misc.is_library_loc loc ->
      (match before_memory_model with
       | Before_gmp -> before_memory_model <- Gmpz
       | Gmpz | Memory_model -> ()
       | After_gmp -> before_memory_model <- Memory_model
       | Code -> () (* still processing the GMP and memory model headers,
                       but reading some libc code *));
396
      Cil.DoChildren
397
    | GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
398
      when Misc.is_fc_or_compiler_builtin vi ->
399
      self#next ();
400
      Cil.DoChildren
401
402
403
    | _ ->
      self#next ();
      Cil.DoChildren
404

405
  method !vfile f =
406
    Cil.DoChildrenPost
407
      (fun _ ->
408
409
410
         match new_definitions with
         | [] -> f
         | _ :: _ ->
411
412
413
414
415
416
417
418
419
420
           (* add the generated definitions of libc at the end of [l]. This way,
              we are sure that they have access to all of it (in particular, the
              memory model, GMP and the soundness variable). Also add the
              [__e_acsl_sound_verdict] variable at the beginning *)
           let new_globals =
             GVarDecl(sound_verdict_vi, Cil_datatype.Location.unknown)
             :: f.globals
             @ new_definitions
           in
           f.globals <- new_globals;
421
           f)
422

Julien Signoles's avatar
Julien Signoles committed
423
424
  initializer
    reset ()
425
426
427

end

428
let dup () =
429
  Options.feedback ~level:2 "duplicating annotated functions";
430
  Visitor.visitFramacFile (new dup_functions_visitor) (Ast.get ());
431
  Queue.iter (fun f -> f ()) actions;
432
  Ast.mark_as_grown ()
433
434
435

(*
Local Variables:
436
compile-command: "make -C ../../../../.."
437
438
End:
*)