Source file meta_run.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's MetACSL plug-in.                   *)
(*                                                                        *)
(*  Copyright (C) 2018-2025                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         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                 *)
(*  for more details (enclosed in the file LICENSE)                       *)
(*                                                                        *)
(**************************************************************************)

open Meta_utils
open Meta_options
open Meta_parse

(* Main procedure *)
let generate flags =
  (* Copy current project and work on the copy *)
  let prj = Project.current () in
  (* Retrieve MPs gathered during parsing *)
  let mps = Meta_parse.metaproperties () in
  let prj_name =
    if Meta_options.Separate_annots.get() then "translation-tmp"
    else "translation"
  in
  let new_prj = Project.create_by_copy ~last:true prj_name in
  Project.set_current new_prj;
  (* Filter only specified ones (-meta-set) *)
  let to_translate = match flags.target_set with
    | None -> mps
    | Some set -> List.filter (fun mp -> StrSet.mem mp.mp_name set) mps
  in
  Self.feedback "Will process %d properties" (List.length to_translate);
  (* Dispatch MPs according to their targets and context to ease annotation *)
  let tables, all_mp = Meta_dispatch.dispatch flags to_translate in
  Meta_bindings.add_ghost_code flags;
  (* Actually annotate (in a new project) *)
  Meta_annotate.annotate flags all_mp tables;
  Meta_dispatch.finalize_dependencies ();
  File.reorder_ast ();
  (* At this point, AST should pass integrity check. *)
  if (Kernel.Check.get()) then Filecheck.check_ast "MetAcsl annotations";
  (* Return the annotated project *)
  let final_prj =
    if Meta_options.Separate_annots.get () then begin
      File.create_rebuilt_project_from_visitor
        ~last:true "translation" (fun prj -> new Visitor.frama_c_copy prj)
    end else new_prj
  in
  Project.set_current prj;
  if Meta_options.Separate_annots.get () then
    Project.remove ~project:new_prj ();
  final_prj

let register () =
  if Enabled.get () then
    (
      Self.feedback "Translation is enabled";
      Ast.compute () ;
      let flags = {
        check_external = Check_External.get ();
        check_callee_assigns = Check_Callee_Assigns.get ();
        simpl = Simpl.get ();
        number_assertions = Number_assertions.get ();
        prefix_meta = Prefix_meta.get ();
        static_bindings = (let r = Static_bindings.get () in
                           if r <= 0 then None else Some r);
        keep_proof_files = Keep_proof_files.get();
        list_targets = List_targets.get ();
        default_to_assert = Default_to_assert.get ();
        target_set = if Targets.is_empty () then None else
            let set = Targets.fold StrSet.add StrSet.empty in
            Some set;
      } in
      ignore @@ generate flags ;
      Self.feedback "Successful translation";
      Enabled.set false
    )

(* External API *)
let translate ?(check_external=true) ?(check_callee_assigns=Kernel_function.Set.empty) ?(simpl=true) ?target_set
    ?(number_assertions=false) ?(prefix_meta=true) ?static_bindings () =
  let flags = {
    number_assertions; default_to_assert = true;
    static_bindings; prefix_meta; list_targets = false;
    check_external; check_callee_assigns; simpl; target_set; keep_proof_files = false;
  } in generate flags

let () =
  Boot.Main.extend register ;
  Meta_parse.register_parsing ()