main.ml 8.9 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              *)
Julien Signoles's avatar
Julien Signoles committed
7
(*         alternatives)                                                  *)
8
9
10
11
12
13
14
15
16
17
18
(*                                                                        *)
(*  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
(*                                                                        *)
(**************************************************************************)
Julien Signoles's avatar
Julien Signoles committed
22

23
let check () = assert false (* [TODO ARCHI] kill check *)
Julien Signoles's avatar
Julien Signoles committed
24
25
26
27
28
29
30
31
32

let check =
  Dynamic.register
    ~plugin:"e-acsl"
    ~journalize:true
    "check"
    (Datatype.func Datatype.unit Datatype.bool)
    check

33
34
35
36
37
type extended_project =
  | To_be_extended
  | Already_extended of Project.t option (* None = keep the current project *)

let extended_ast_project: extended_project ref = ref To_be_extended
38
39
40

let unmemoized_extend_ast () =
  let extend () =
41
    let share = Options.Share.dir ~error:true () in
42
    Options.feedback ~level:3 "setting kernel options for E-ACSL.";
43
    Kernel.CppExtraArgs.add
44
      (Format.asprintf " -DE_ACSL_MACHDEP=%s -I%s/memory_model"
45
46
         (Kernel.Machdep.get ())
         share);
47
    Kernel.Keep_unused_specified_functions.off ();
48
49
    if Plugin.is_present "variadic-translation" then
      Dynamic.Parameter.Bool.off "-variadic-translation" ();
50
    let ppc, ppk = File.get_preprocessor_command () in
51
    let register s =
52
53
      File.pre_register
        (File.NeedCPP
54
           (s,
55
            ppc
56
            ^ Format.asprintf " -I%s" share,
57
            ppk))
58
59
60
61
62
63
    in
    List.iter register (Misc.library_files ())
  in
  if Ast.is_computed () then begin
    (* do not modify the existing project: work on a copy.
       Must also extend the current AST with the E-ACSL's library files. *)
64
65
    Options.feedback ~level:2
      "AST already computed: E-ACSL is going to work on a copy.";
66
    let name = Project.get_name (Project.current ()) in
67
    let tmpfile =
68
69
70
71
      Extlib.temp_file_cleanup_at_exit ("e_acsl_" ^ name) ".i" in
    let cout = open_out tmpfile in
    let fmt = Format.formatter_of_out_channel cout in
    File.pretty_ast ~fmt ();
72
    let selection =
73
      State_selection.diff
74
75
        State_selection.full
        (State_selection.with_dependencies Ast.self)
76
77
78
    in
    let prj =
      Project.create_by_copy
79
        ~last:false
80
81
        ~selection
        (Format.asprintf "%s for E-ACSL" name)
82
83
84
    in
    Project.on prj
      (fun () ->
85
         Kernel.Files.set [ Datatype.Filepath.of_string tmpfile ];
Julien Signoles's avatar
Julien Signoles committed
86
         extend ())
87
      ();
88
    Some prj
89
90
  end else begin
    extend ();
91
    None
92
93
  end

94
let extend_ast () = match !extended_ast_project with
95
  | To_be_extended ->
96
    let prj = unmemoized_extend_ast () in
97
98
    extended_ast_project := Already_extended prj;
    (match prj with
Julien Signoles's avatar
Julien Signoles committed
99
100
     | None -> Project.current ()
     | Some prj -> prj)
101
102
103
  | Already_extended None ->
    Project.current ()
  | Already_extended(Some prj) ->
104
    prj
105
106
107
108

let apply_on_e_acsl_ast f x =
  let tmp_prj = extend_ast () in
  let res = Project.on tmp_prj f x in
109
  (match !extended_ast_project with
Julien Signoles's avatar
Julien Signoles committed
110
111
112
113
114
115
   | To_be_extended -> assert false
   | Already_extended None -> ()
   | Already_extended (Some prj) ->
     assert (Project.equal prj tmp_prj);
     extended_ast_project := To_be_extended;
     if Options.Debug.get () = 0 then Project.remove ~project:tmp_prj ());
116
117
  res

Julien Signoles's avatar
Julien Signoles committed
118
119
120
121
122
123
124
module Resulting_projects =
  State_builder.Hashtbl
    (Datatype.String.Hashtbl)
    (Project.Datatype)
    (struct
      let name = "E-ACSL resulting projects"
      let size = 7
125
      let dependencies = Ast.self :: Options.parameter_states
Julien Signoles's avatar
Julien Signoles committed
126
    end)
Julien Signoles's avatar
Julien Signoles committed
127

128
129
130
131
132
let () =
  State_dependency_graph.add_dependencies
    ~from:Resulting_projects.self
    [ Label.self ]

Julien Signoles's avatar
Julien Signoles committed
133
134
135
let generate_code =
  Resulting_projects.memo
    (fun name ->
136
137
138
139
140
141
       apply_on_e_acsl_ast
         (fun () ->
            Options.feedback "beginning translation.";
            Temporal.enable (Options.Temporal_validity.get ());
            let prepared_prj = Prepare_ast.prepare () in
            let res =
142
143
              Project.on
                prepared_prj
144
145
                (fun () ->
                   let dup_prj = Dup_functions.dup () in
146
                   let copied_prj =
147
                     Project.create_by_copy name ~last:true ~src:dup_prj
148
                   in
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
                   Project.on
                     copied_prj
                     (fun () ->
                        Gmp_types.init ();
                        Mmodel_analysis.reset ();
                        Injector.inject ();
                        (* remove the RTE's results computed from E-ACSL:
                           they are partial and associated with the wrong
                           kernel function (the one of the old project). *)
                        (* [TODO ARCHI] what if RTE was already computed? *)
                        let selection =
                          State_selection.with_dependencies !Db.RteGen.self
                        in
                        Project.clear ~selection ~project:copied_prj ();
                        Resulting_projects.mark_as_computed ())
Julien Signoles's avatar
Julien Signoles committed
164
                     ();
165
166
                   if Options.Debug.get () = 0 then
                     Project.remove ~project:dup_prj ();
167
                   copied_prj)
168
                ()
169
170
171
172
173
174
175
176
            in
            if Options.Debug.get () = 0 then begin
              Project.remove ~project:prepared_prj ();
            end;
            Options.feedback "translation done in project \"%s\"."
              (Options.Project_name.get ());
            res)
         ())
Julien Signoles's avatar
Julien Signoles committed
177
178
179

let generate_code =
  Dynamic.register
180
    ~plugin:"E_ACSL"
Julien Signoles's avatar
Julien Signoles committed
181
182
183
184
185
    ~journalize:true
    "generate_code"
    (Datatype.func Datatype.string Project.ty)
    generate_code

186
187
let predicate_to_exp =
  Dynamic.register
188
    ~plugin:"E_ACSL"
189
190
191
    ~journalize:false
    "predicate_to_exp"
    (Datatype.func2
192
       Kernel_function.ty Cil_datatype.Predicate.ty Cil_datatype.Exp.ty)
193
194
    Translate.predicate_to_exp

195
let add_e_acsl_library _files =
196
  if Options.must_visit () || Options.Prepare.get () then ignore (extend_ast ())
197

198
199
200
201
(* extending the AST as soon as possible reduce the amount of time the AST is
   duplicated:
   - that is faster
   - locations are better (indicate an existing file, and not a temp file) *)
202
203
let () = Cmdline.run_after_configuring_stage add_e_acsl_library

204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
(* The Frama-C standard library contains specific built-in variables prefixed by
   "__fc_" and declared as extern: they prevent the generated code to be
   linked. This modification of the default printer replaces them by their
   original version from the stdlib. For instance, [__fc_stdout] is replaced by
   [stdout]. That is very hackish since it modifies the default Frama-C
   printer.

   TODO: should be done by the Frama-C default printer at some points. *)
let change_printer =
  (* not projectified on purpose: this printer change is common to each
     project. *)
  let first = ref true in
  fun () ->
    if !first then begin
      first := false;
      let r = Str.regexp "^__fc_" in
220
221
222
223
      let module Printer_class(X: Printer.PrinterClass) = struct
        class printer = object
          inherit X.printer as super
          method !varinfo fmt vi =
224
225
226
227
            if vi.Cil_types.vghost || vi.Cil_types.vstorage <> Cil_types.Extern
            then
              super#varinfo fmt vi
            else
228
229
230
              let s = Str.replace_first r "" vi.Cil_types.vname in
              Format.fprintf fmt "%s" s
        end
231
      end in
232
      Printer.update_printer (module Printer_class: Printer.PrinterExtension)
233
234
    end

235
let main () =
236
  Keep_status.clear ();
237
238
  if Options.Run.get () then begin
    change_printer ();
239
    ignore (generate_code (Options.Project_name.get ()))
240
  end else
Julien Signoles's avatar
Julien Signoles committed
241
242
243
244
245
246
  if Options.Check.get () then
    apply_on_e_acsl_ast
      (fun () ->
         Gmp_types.init ();
         ignore (check ()))
      ()
247

248
249
250
251
let () = Db.Main.extend main

(*
Local Variables:
252
compile-command: "make -C .."
253
254
End:
*)