main.ml 9.2 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
Virgile Prevosto's avatar
Virgile Prevosto committed
3
(*  This file is part of Frama-C.                                         *)
4
(*                                                                        *)
5
(*  Copyright (C) 2007-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.";
Kostyantyn Vorobyov's avatar
Kostyantyn Vorobyov committed
152
          Temporal.enable (Options.Temporal_validity.get ());
153
          let prepared_prj = Prepare_ast.prepare () in
154
          let res =
155
156
157
            Project.on prepared_prj
            (fun () ->
              let dup_prj = Dup_functions.dup () in
Julien Signoles's avatar
Julien Signoles committed
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
              let res =
                Project.on
                  dup_prj
                  (fun () ->
                    Gmpz.init_t ();
                    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)
179
                ()
Julien Signoles's avatar
Julien Signoles committed
180
181
182
183
              in
              if Options.Debug.get () = 0 then
                Project.remove ~project:dup_prj ();
              res)
184
185
              ()
          in
186
187
188
          if Options.Debug.get () = 0 then begin
            Project.remove ~project:prepared_prj ();
          end;
189
190
191
192
          Options.feedback "translation done in project \"%s\"."
            (Options.Project_name.get ());
          res)
        ())
Julien Signoles's avatar
Julien Signoles committed
193
194
195

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

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

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

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

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

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

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

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