main.ml 9.49 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              *)
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

Julien Signoles's avatar
Julien Signoles committed
23
let check () =
Julien Signoles's avatar
Julien Signoles committed
24
25
26
27
  Visitor.visitFramacFileSameGlobals (Visit.do_visit false) (Ast.get ());
  let t = Error.nb_untypable () in
  let n = Error.nb_not_yet () in
  let print msg n =
28
    Options.result "@[%d annotation%s %s ignored,@ being %s.@]"
Julien Signoles's avatar
Julien Signoles committed
29
30
31
32
33
34
35
36
      n
      (if n > 1 then "s" else "")
      (if n > 1 then "were" else "was")
      msg
  in
  print "untypable" t;
  print "unsupported" n;
  n + t = 0
Julien Signoles's avatar
Julien Signoles committed
37
38
39
40
41
42
43
44
45

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

46
47
48
49
50
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
51
52
53

let unmemoized_extend_ast () =
  let extend () =
54
    let share = Options.Share.dir ~error:true () in
55
    Options.feedback ~level:3 "setting kernel options for E-ACSL.";
56
    Kernel.CppExtraArgs.add
57
      (Format.asprintf " -DE_ACSL_MACHDEP=%s -I%s/memory_model"
58
59
         (Kernel.Machdep.get ())
         share);
60
    Kernel.Keep_unused_specified_functions.off ();
61
62
    if Plugin.is_present "variadic-translation" then
      Dynamic.Parameter.Bool.off "-variadic-translation" ();
63
    let ppc, ppk = File.get_preprocessor_command () in
64
    let register s =
65
66
      File.pre_register
        (File.NeedCPP
67
           (s,
68
            ppc
69
            ^ Format.asprintf " -I%s" share,
70
            ppk))
71
72
73
74
75
76
    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. *)
77
78
    Options.feedback ~level:2 "AST already computed: \
E-ACSL is going to work on a copy.";
79
    let name = Project.get_name (Project.current ()) in
80
    let tmpfile =
81
82
83
84
      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 ();
85
    let selection =
86
      State_selection.diff
87
88
        State_selection.full
        (State_selection.with_dependencies Ast.self)
89
90
91
    in
    let prj =
      Project.create_by_copy
92
        ~last:false
93
94
        ~selection
        (Format.asprintf "%s for E-ACSL" name)
95
96
97
    in
    Project.on prj
      (fun () ->
98
99
        Kernel.Files.set [ tmpfile ];
        extend ())
100
      ();
101
    Some prj
102
103
  end else begin
    extend ();
104
    None
105
106
  end

107
let extend_ast () = match !extended_ast_project with
108
  | To_be_extended ->
109
    let prj = unmemoized_extend_ast () in
110
111
112
113
114
115
116
    extended_ast_project := Already_extended prj;
    (match prj with
    | None -> Project.current ()
    | Some prj -> prj)
  | Already_extended None ->
    Project.current ()
  | Already_extended(Some prj) ->
117
    prj
118
119
120
121

let apply_on_e_acsl_ast f x =
  let tmp_prj = extend_ast () in
  let res = Project.on tmp_prj f x in
122
123
124
125
126
127
  (match !extended_ast_project with
  | To_be_extended -> assert false
  | Already_extended None -> ()
  | Already_extended (Some prj) ->
    assert (Project.equal prj tmp_prj);
    extended_ast_project := To_be_extended;
128
    if Options.Debug.get () = 0 then Project.remove ~project:tmp_prj ());
129
130
  res

Julien Signoles's avatar
Julien Signoles committed
131
132
133
134
135
136
137
module Resulting_projects =
  State_builder.Hashtbl
    (Datatype.String.Hashtbl)
    (Project.Datatype)
    (struct
      let name = "E-ACSL resulting projects"
      let size = 7
138
      let dependencies = Ast.self :: Options.parameter_states
Julien Signoles's avatar
Julien Signoles committed
139
140
     end)

141
142
143
144
145
let () =
  State_dependency_graph.add_dependencies
    ~from:Resulting_projects.self
    [ Label.self ]

Julien Signoles's avatar
Julien Signoles committed
146
147
148
let generate_code =
  Resulting_projects.memo
    (fun name ->
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
       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 =
              Project.on prepared_prj
                (fun () ->
                   let dup_prj = Dup_functions.dup () in
                   let res =
                     Project.on
                       dup_prj
                       (fun () ->
                          Gmp_types.init ();
                          Mmodel_analysis.reset ();
                          let visit prj = Visit.do_visit ~prj true in
                          let prj =
                            File.create_project_from_visitor name visit
                          in
                          Loops.apply_after_transformation prj;
                          (* remove the RTE's results computed from E-ACSL:
                             their are partial and associated with the wrong
                             kernel function (the one of the old project). *)
                          let selection =
                            State_selection.with_dependencies !Db.RteGen.self
                          in
                          Project.clear ~selection ~project:prj ();
                          Resulting_projects.mark_as_computed ();
                          let selection =
                            State_selection.singleton Kernel.Files.self
                          in
                          Project.copy ~selection prj;
                          prj)
                       ()
                   in
                   if Options.Debug.get () = 0 then
                     Project.remove ~project:dup_prj ();
                   res)
187
                ()
188
189
190
191
192
193
194
195
            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
196
197
198

let generate_code =
  Dynamic.register
199
    ~plugin:"E_ACSL"
Julien Signoles's avatar
Julien Signoles committed
200
201
202
203
204
    ~journalize:true
    "generate_code"
    (Datatype.func Datatype.string Project.ty)
    generate_code

205
206
let predicate_to_exp =
  Dynamic.register
207
    ~plugin:"E_ACSL"
208
209
210
    ~journalize:false
    "predicate_to_exp"
    (Datatype.func2
211
       Kernel_function.ty Cil_datatype.Predicate.ty Cil_datatype.Exp.ty)
212
213
    Translate.predicate_to_exp

214
let add_e_acsl_library _files =
215
  if Options.must_visit () || Options.Prepare.get () then ignore (extend_ast ())
216

217
218
219
220
(* 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) *)
221
222
let () = Cmdline.run_after_configuring_stage add_e_acsl_library

223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
(* 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
239
240
241
242
      let module Printer_class(X: Printer.PrinterClass) = struct
        class printer = object
          inherit X.printer as super
          method !varinfo fmt vi =
243
244
245
246
            if vi.Cil_types.vghost || vi.Cil_types.vstorage <> Cil_types.Extern
            then
              super#varinfo fmt vi
            else
247
248
249
              let s = Str.replace_first r "" vi.Cil_types.vname in
              Format.fprintf fmt "%s" s
        end
250
      end in
251
      Printer.update_printer (module Printer_class: Printer.PrinterExtension)
252
253
    end

254
let main () =
255
  Keep_status.clear ();
256
257
  if Options.Run.get () then begin
    change_printer ();
258
    ignore (generate_code (Options.Project_name.get ()))
259
  end else
260
261
    if Options.Check.get () then
      apply_on_e_acsl_ast
262
        (fun () ->
263
          Gmp_types.init ();
264
265
          ignore (check ()))
        ()
266

267
268
269
270
let () = Db.Main.extend main

(*
Local Variables:
271
compile-command: "make -C .."
272
273
End:
*)