main.ml 9.15 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
      apply_on_e_acsl_ast
150
151
        (fun () ->
          Options.feedback "beginning translation.";
152
          let prepared_prj = Prepare_ast.prepare () in
153
          let res =
154
155
156
            Project.on prepared_prj
            (fun () ->
              let dup_prj = Dup_functions.dup () in
Julien Signoles's avatar
Julien Signoles committed
157
158
159
160
              let res =
                Project.on
                  dup_prj
                  (fun () ->
161
                    Gmp_types.init ();
Julien Signoles's avatar
Julien Signoles committed
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
                    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 ();
                    Project.copy
                      ~selection:(State_selection.singleton Kernel.Files.self)
                      prj;
                    prj)
178
                ()
Julien Signoles's avatar
Julien Signoles committed
179
180
181
182
              in
              if Options.Debug.get () = 0 then
                Project.remove ~project:dup_prj ();
              res)
183
184
              ()
          in
185
186
187
          if Options.Debug.get () = 0 then begin
            Project.remove ~project:prepared_prj ();
          end;
188
189
190
191
          Options.feedback "translation done in project \"%s\"."
            (Options.Project_name.get ());
          res)
        ())
Julien Signoles's avatar
Julien Signoles committed
192
193
194

let generate_code =
  Dynamic.register
195
    ~plugin:"E_ACSL"
Julien Signoles's avatar
Julien Signoles committed
196
197
198
199
200
    ~journalize:true
    "generate_code"
    (Datatype.func Datatype.string Project.ty)
    generate_code

201
202
let predicate_to_exp =
  Dynamic.register
203
    ~plugin:"E_ACSL"
204
205
206
    ~journalize:false
    "predicate_to_exp"
    (Datatype.func2
207
       Kernel_function.ty Cil_datatype.Predicate.ty Cil_datatype.Exp.ty)
208
209
    Translate.predicate_to_exp

210
let add_e_acsl_library _files =
211
  if Options.must_visit () || Options.Prepare.get () then ignore (extend_ast ())
212

213
214
215
216
(* 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) *)
217
218
let () = Cmdline.run_after_configuring_stage add_e_acsl_library

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

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

263
264
265
266
let () = Db.Main.extend main

(*
Local Variables:
267
compile-command: "make -C .."
268
269
End:
*)