package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file aorai_register.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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
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
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Aorai plug-in of Frama-C.                        *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*    INRIA (Institut National de Recherche en Informatique et en         *)
(*           Automatique)                                                 *)
(*    INSA  (Institut National des Sciences Appliquees)                   *)
(*                                                                        *)
(*  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 licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* [VP] Need to get rid of those global references at some point. *)
let c_file = ref Filepath.Normalized.empty
let dot_file = ref Filepath.Normalized.empty

(* Performs some checks before calling [open_in f], reporting ["errmsg: <f>"]
   in case of error. *)
let check_and_open_in (f : Filepath.Normalized.t) errmsg =
  if not (Filepath.Normalized.is_file f) then
    Aorai_option.abort "%s: %a" errmsg Filepath.Normalized.pretty f;
  open_in (f :> string)

let load_ya_file filename  =
  let channel = check_and_open_in filename "invalid Ya file" in
  let lexbuf = Lexing.from_channel channel in
  Lexing.(lexbuf.lex_curr_p <-
            { lexbuf.lex_curr_p with pos_fname = (filename :> string) });
  try
    let automata = Yaparser.main Yalexer.token lexbuf in
    close_in channel;
    Data_for_aorai.setAutomata automata
  with
  | Parsing.Parse_error ->
    Utils_parser.abort_current lexbuf "syntax error"

let display_status () =
  if Aorai_option.verbose_atleast 2 then begin
    Aorai_option.feedback "\n"  ;
    Aorai_option.feedback "C file:            '%a'\n" Filepath.Normalized.pretty !c_file ;
    Aorai_option.feedback "Entry point:       '%a'\n"
      Kernel_function.pretty (fst (Globals.entry_point())) ;
    if Aorai_option.Dot.get () then
      Aorai_option.feedback "Dot file:          '%a'\n" Filepath.Normalized.pretty !dot_file;
  end

let init_file_names () =
  let freshname ?opt_suf file suf =
    let name = (file:Filepath.Normalized.t:>string) in
    let pre = Filename.remove_extension name in
    let pre = match opt_suf with None -> pre | Some s -> pre ^ s in
    let rec fn p s n =
      let fp = Filepath.Normalized.of_string (p ^ (string_of_int n) ^ s) in
      if not (Filepath.exists fp) then fp
      else fn p s (n+1)
    in
    let name =
      let fp = Filepath.Normalized.of_string (pre^suf) in
      if not (Filepath.exists fp) then fp
      else fn pre suf 0
    in
    name
  in
  if Aorai_option.Ya.is_empty () then
    Aorai_option.abort "empty Ya file name";
  if Aorai_option.Dot.get() then
    dot_file := freshname (Aorai_option.Ya.get ()) ".dot";
  display_status ()

let printverb s = Aorai_option.feedback ~level:2 "%s" s

let output () =
  (* Dot file *)
  if (Aorai_option.Dot.get()) then
    begin
      Pretty_automaton.Typed.output_dot_automata (Data_for_aorai.getAutomata ())
        (!dot_file:>string);
      printverb "Generating dot file    : done\n"
    end

let work () =
  let file = Ast.get () in
  Aorai_utils.initFile file;
  printverb "C file loading         : done\n";
  if not (Aorai_option.Ya.is_empty ()) then
    load_ya_file (Aorai_option.Ya.get ());
  let root = fst (Globals.entry_point ()) in
  let axiomatization = Aorai_option.Axiomatization.get() in
  if axiomatization then
    begin
      (* Step 5 : incrementing pre/post
             conditions with states and transitions information *)
      printverb "Refining pre/post      : \n";
      Aorai_dataflow.compute ();
      (* Step 6 : Removing transitions never crossed *)
      let automaton_has_states =
        if (Aorai_option.AutomataSimplification.get()) then
          begin
            printverb "Removing unused trans  : done\n";
            try
              Data_for_aorai.removeUnusedTransitionsAndStates ();
              true
            with Data_for_aorai.Empty_automaton ->
              Aorai_option.warning
                "No state of the automaton is reachable. \
                 Program and specification are incompatible, \
                 instrumentation will not be generated.";
              false
          end
        else
          (printverb "Removing unused trans  : skipped\n"; true)
      in
      if automaton_has_states then begin
        (* Step 7 : Labeling abstract file *)
        (* Finally the information is added into the Cil automata. *)
        Aorai_utils.initGlobals root axiomatization;
        Aorai_visitors.add_sync_with_buch file;
        if Aorai_option.GenerateAnnotations.get () then
          Aorai_visitors.add_pre_post_from_buch file
            (Aorai_option.advance_abstract_interpretation ())
        else if Aorai_option.ConsiderAcceptance.get () then begin
          let kf,_ = Globals.entry_point() in
          let bhv = Aorai_utils.mk_acceptance_bhv () in
          Annotations.add_behaviors Aorai_option.emitter kf [bhv]
        end;
        Aorai_eva_analysis.setup ();
        printverb "Annotation of Cil      : done\n";
      end
    end
  else
    begin
      (* Step 4': Computing the set of possible pre-states and post-states of each function *)
      (*          And so for pre/post transitions *)
      printverb "Abstracting pre/post   : skipped\n";

      (* Step 5': incrementing pre/post conditions with states and transitions information *)
      printverb "Refining pre/post      : skipped\n";

      (* Step 6 : Removing transitions never crossed *)
      printverb "Removing unused trans  : skipped\n";

      (* Step 7 : Labeling abstract file *)
      (* Finally the information is added into the Cil automata. *)
      Aorai_utils.initGlobals root axiomatization;
      Aorai_visitors.add_sync_with_buch file;
      printverb "Annotation of Cil      : partial\n"
    end;

  (* Step 8 : clearing tables whose information has been
     invalidated by our transformations.
  *)
  Ast.mark_as_changed();
  Cfg.clearFileCFG ~clear_id:false file;
  Cfg.computeFileCFG file;
  Ast.clear_last_decl ();
  if Kernel.Check.get() then Filecheck.check_ast "aorai";
  output ()

let run () =
  (* Step 1 : Capture files names *)
  init_file_names ();
  (* Step 2 : Work in our own project, initialized by a copy of the main
     one. *)
  let work_prj =
    File.create_project_from_visitor "aorai"
      (fun prj -> new Visitor.frama_c_copy prj)
  in
  Project.copy ~selection:(Parameter_state.get_selection ()) work_prj;
  Project.on work_prj work ()

(* Plugin registration *)

let run =
  Dynamic.register
    ~plugin:"Aorai"
    "run"
    (Datatype.func Datatype.unit Datatype.unit)
    run

let run, _ =
  State_builder.apply_once
    "Aorai"
    (let module O = Aorai_option in
     [ O.Ya.self; O.Axiomatization.self; O.ConsiderAcceptance.self;
       O.AutomataSimplification.self; O.AbstractInterpretation.self;
       O.AddingOperationNameAndStatusInSpecification.self ])
    run

let main () = if Aorai_option.is_on () then run ()
let () = Boot.Main.extend main

(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct