dup_functions.ml 15.3 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
        (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)
79

80
    method !vlogic_var_use orig_lvi =
81
      match orig_lvi.lv_origin with
82
83
      | None ->
        Cil.JustCopy
84
      | Some vi ->
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
        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 ->
               (* 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 *)
               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 _ =
111
112
      Cil.DoChildrenPost Logic_const.refresh_identified_term

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

118
let dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi =
119
120
  new_vi.vdefined <- true;
  let formals = Kernel_function.get_formals kf in
121
122
123
  let mk_formal vi =
    let name =
      if vi.vname = "" then
Andre Maroneze's avatar
Andre Maroneze committed
124
        (* unnamed formal parameter: must generate a fresh name since a fundec
Julien Signoles's avatar
Julien Signoles committed
125
           cannot have unnamed formals (see bts #2303). *)
126
127
        Varname.get
          ~scope:Varname.Function
128
          (Functions.RTL.mk_gen_name "unamed_formal")
129
130
131
132
133
134
      else
        vi.vname
    in
    Cil.copyVarinfo vi name
  in
  let new_formals = List.map mk_formal formals in
135
136
137
  let res =
    let ty = Kernel_function.get_return_type kf in
    if Cil.isVoidType ty then None
138
    else Some (Cil.makeVarinfo false false ~referenced:true "__retres" ty)
139
140
141
142
143
  in
  let return =
    Cil.mkStmt ~valid_sid:true
      (Return(Extlib.opt_map (Cil.evar ~loc) res, loc))
  in
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
  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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
  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
  { svar = new_vi;
    sformals = new_formals;
    slocals = locals;
    smaxid = List.length new_formals;
    sbody = body;
    smaxstmtid = None;
    sallstmts = [];
176
    sspec = new_spec }
177

178
let dup_global loc actions spec bhv sound_verdict_vi kf vi new_vi =
179
180
  let name = vi.vname in
  Options.feedback ~dkey ~level:2 "entering in function %s" name;
181
  let fundec = dup_fundec loc spec bhv sound_verdict_vi kf vi new_vi  in
182
  let fct = Definition(fundec, loc) in
183
  let new_spec = fundec.sspec in
184
  let new_kf = { fundec = fct; spec = new_spec } in
185
186
187
188
189
  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;
      Annotations.register_funspec new_kf)
190
    actions;
191
  Options.feedback ~dkey ~level:2 "function %s" name;
192
193
194
  (* 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. *)
195
  let kf = Visitor_behavior.Get.kernel_function bhv kf in
196
197
198
  if Kernel_function.is_definition kf then begin
    Queue.add
      (fun () ->
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
         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)
217
218
      actions
  end;
219
  GFun(fundec, loc), GFunDecl(new_spec, new_vi, loc)
220
221
222
223
224

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

225
type position = Before_gmp | Gmpz | After_gmp | Memory_model | Code
226

227
228
229
class dup_functions_visitor prj = object (self)
  inherit Visitor.frama_c_copy prj

230
231
232
233
234
235
236
237
238
239
240
241
  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

242
  val fct_tbl = Cil_datatype.Varinfo.Hashtbl.create 7
243
  val mutable before_memory_model = Before_gmp
244
245
  val mutable new_definitions: global list = []
  (* new definitions of the annotated functions which will contain the
Andre Maroneze's avatar
Andre Maroneze committed
246
     translation of the E-ACSL contract *)
247

248
249
250
251
252
253
254
  val mutable sound_verdict_vi =
    let name = Functions.RTL.mk_api_name "sound_verdict" in
    let vi = Project.on prj (Cil.makeGlobalVar name) Cil.intType in
    vi.vstorage <- Extern;
    vi.vreferenced <- true;
    vi

255
  method private before_memory_model = match before_memory_model with
256
257
    | Before_gmp | Gmpz | After_gmp -> true
    | Memory_model | Code -> false
258
259

  method private insert_libc l =
260
    match new_definitions with
261
262
    | [] -> l
    | _ :: _ ->
263
264
      (* 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
265
266
267
268
269
270
271
         memory model, GMP and the soundness variable).

         Also add the [__e_acsl_sound_verdict] variable at the beginning *)
      let res =
        GVarDecl(sound_verdict_vi, Cil_datatype.Location.unknown)
        :: l
        @ new_definitions in
272
      new_definitions <- [];
273
274
275
276
277
      res

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

283
  method !vlogic_info_decl li =
284
285
286
    Global.add_logic_info li;
    Cil.JustCopy

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

294
295
296
297
298
  method private is_unvariadic_function vi =
    match Cil.unrollType vi.vtype with
    | TFun(_, _, variadic, _) -> not variadic
    | _ -> false

299
  method !vglob_aux = function
300
    | GFunDecl(_, vi, loc) | GFun({ svar = vi }, loc)
301
302
      when (* duplicate a function iff: *)
        not (Cil_datatype.Varinfo.Hashtbl.mem fct_tbl vi)
303
304
305
        (* it is not already duplicated *)
        && not (Datatype.String.Set.mem vi.vname unduplicable_functions)
        (* it is duplicable *)
306
        && self#is_unvariadic_function vi (* it is not a variadic function *)
307
        && not (Misc.is_library_loc loc) (* it is not in the E-ACSL's RTL *)
308
        && not (Misc.is_fc_or_compiler_builtin vi) (* it is not a built-in *)
309
310
311
312
313
        &&
        (let kf =
           try Globals.Functions.get vi with Not_found -> assert false
         in
         not (Functions.instrument kf)
314
315
316
         (* either explicitely listed as to be not instrumented *)
         ||
         (* or: *)
317
318
319
         (not (Cil.is_empty_funspec
                 (Annotations.funspec ~populate:false
                    (Extlib.the self#current_kf)))
320
321
322
          (* it has a function contract *)
          && Functions.check kf
          (* its annotations must be monitored *)))
323
      ->
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
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
378
379
380
381
382
383
384
385
386
387
388
389
      self#next ();
      let name = Functions.RTL.mk_gen_name vi.vname in
      let new_vi =
        Project.on prj (Cil.makeGlobalVar name) vi.vtype
      in
      Cil_datatype.Varinfo.Hashtbl.add fct_tbl vi new_vi;
      Cil.DoChildrenPost
        (fun l -> match l with
           | [ GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _) as g ]
             ->
             (match g with
              | GFunDecl _ ->
                if not (Kernel_function.is_definition (Extlib.the self#current_kf))
                && vi.vname <> "malloc" && vi.vname <> "free"
                then
                  Options.warning "@[annotating undefined function `%a':@ \
                                   the generated program may miss memory instrumentation@ \
                                   if there are memory-related annotations.@]"
                    Printer.pp_varinfo vi
              | GFun _ -> ()
              | _ -> assert false);
             let tmp = vi.vname in
             if tmp = Kernel.MainFunction.get () then begin
               (* the new function becomes the new main: simply swap the name of both
                  functions *)
               vi.vname <- new_vi.vname;
               new_vi.vname <- tmp
             end;
             let kf =
               try
                 Globals.Functions.get (Visitor_behavior.Get_orig.varinfo self#behavior vi)
               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 vi_bhv = Visitor_behavior.Get.varinfo self#behavior vi in
             let new_g, new_decl =
               dup_global
                 loc
                 self#get_filling_actions
                 spec
                 self#behavior
                 sound_verdict_vi
                 kf
                 vi_bhv
                 new_vi
             in
             (* postpone the introduction of the new function definition to the
                end *)
             new_definitions <- new_g :: new_definitions;
             (* put the declaration before the original function in order to solve
                issue with recursive functions *)
             [ 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 *));
      Cil.JustCopy
    | GVarDecl(vi, _) | GFunDecl(_, vi, _) | GFun({ svar = vi }, _)
390
      when Misc.is_fc_or_compiler_builtin vi ->
391
392
393
394
395
      self#next ();
      Cil.JustCopy
    | _ ->
      self#next ();
      Cil.DoChildren
396

397
  method !vfile _ =
398
399
    Cil.DoChildrenPost
      (fun f ->
400
401
402
403
404
405
406
         match new_definitions with
         | [] -> f
         | _ :: _ ->
           (* required by the few cases where there is no global tagged as
              [Code] in the file. *)
           f.globals <- self#insert_libc f.globals;
           f)
407

Julien Signoles's avatar
Julien Signoles committed
408
  initializer
409
    Project.copy ~selection:(Parameter_state.get_selection ()) prj;
Julien Signoles's avatar
Julien Signoles committed
410
    reset ()
411
412
413

end

414
let dup () =
415
  Options.feedback ~level:2 "duplicating annotated functions";
416
417
  let prj =
    File.create_project_from_visitor
418
      "e_acsl_dup_functions"
419
420
      (new dup_functions_visitor)
  in
421
  Queue.iter (fun f -> f ()) actions;
422
423
424
425
426
427
428
  prj

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