package frama-c

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

Source file main.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
(*                                                                        *)
(*  Copyright (C) 2012-2024                                               *)
(*    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 licenses/LGPLv2.1).            *)
(**************************************************************************)

module Resulting_projects =
  State_builder.Hashtbl
    (Datatype.String.Hashtbl)
    (Project.Datatype)
    (struct
      let name = "E-ACSL resulting projects"
      let size = 7
      let dependencies = Ast.self :: Options.parameter_states
    end)

let generate_code =
  Resulting_projects.memo
    (fun name ->
       Options.feedback "beginning translation.";
       Temporal.enable (Options.Temporal_validity.get ());
       Options.setup ();
       (* slightly more efficient to copy the project before computing the AST
          if it is not yet computed *)
       let rtl_prj_name = Options.Project_name.get () ^ " RTL" in
       let rtl_prj = Project.create_by_copy ~last:false rtl_prj_name in
       (* force AST computation before copying the project it belongs to *)
       Ast.compute ();
       let copied_prj = Project.create_by_copy ~last:true name in
       Project.on
         copied_prj
         (fun () ->
            (* preparation of the AST does not concern the E-ACSL RTL:
               do it first *)
            Prepare_ast.prepare ();
            Memory_tracking.SpecialPointers.initialize ();
            Rtl.link rtl_prj;
            (* the E-ACSL type system ensures the soundness of the generated
               arithmetic operations. Therefore, deactivate the corresponding
               options in order to prevent RTE to generate spurious alarms. *)
            let signed = Kernel.SignedOverflow.get () in
            let unsigned = Kernel.UnsignedOverflow.get () in
            (* we do know that setting these flags does not modify the program's
               semantics: using their unsafe variants is thus safe and preserve
               all emitted property statuses. *)
            Kernel.SignedOverflow.unsafe_set false;
            Kernel.UnsignedOverflow.unsafe_set false;
            let finally () =
              Kernel.SignedOverflow.unsafe_set signed;
              Kernel.UnsignedOverflow.unsafe_set unsigned
            in
            Fun.protect
              ~finally
              (fun () ->
                 Gmp_types.init ();
                 Analyses.preprocess ();
                 Injector.inject ()) ;
            (* remove the RTE's results computed from E-ACSL: they are partial
               and associated with the wrong kernel function (the one of the old
               project). *)
            (* [TODO] what if RTE was already computed? To be fixed when
               redoing the RTE management system  *)
            let selection =
              State_selection.union
                (Rte.get_state_selection_with_dependencies ())
                (State_selection.with_dependencies Options.Run.self)
            in
            Project.clear ~selection ~project:copied_prj ();
            Resulting_projects.mark_as_computed ())
         ();
       if not (Options.debug_atleast 1) then Project.remove ~project:rtl_prj ();
       Options.feedback "translation done in project \"%s\"."
         (Options.Project_name.get ());
       copied_prj)

let generate_code =
  Dynamic.register
    ~plugin:"E_ACSL"
    "generate_code"
    (Datatype.func Datatype.string Project.ty)
    generate_code

(* 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
      let module Printer_class(X: Printer.PrinterClass) = struct
        class printer = object
          inherit X.printer as super

          method !varinfo fmt vi =
            if Functions.Libc.is_vla_alloc_name vi.Cil_types.vname then
              (* Replace VLA allocation with calls to [__builtin_alloca] *)
              Format.fprintf fmt "%s" Functions.Libc.actual_alloca
            else if (not vi.vghost) && vi.vstorage == Cil_types.Extern then
              (* Replace calls to Frama-C builtins with calls to their original
                 version from the libc *)
              let s = Str.replace_first r "" vi.Cil_types.vname in
              Format.fprintf fmt "%s" s
            else
              (* Otherwise use the original printer *)
              super#varinfo fmt vi

          method !instr fmt i =
            match i with
            | Call(_, fct, _, _) when Functions.Libc.is_vla_free fct ->
              (* Nothing to print: VLA deallocation is done automatically when
                 leaving the scope *)
              Format.fprintf fmt "/* ";
              super#instr fmt i;
              Format.fprintf fmt " */"
            | _ ->
              super#instr fmt i

          method !global fmt g =
            let is_vla_builtin vi =
              Functions.Libc.is_vla_alloc_name vi.Cil_types.vname ||
              Functions.Libc.is_vla_free_name vi.Cil_types.vname
            in
            match g with
            | GFunDecl (_, vi, _) when is_vla_builtin vi ->
              (* Nothing to print: the VLA builtins don't have an original libc
                 version. *)
              ()
            | _ ->
              super#global fmt g
        end
      end in
      Printer.update_printer (module Printer_class: Printer.PrinterExtension)
    end

let main () =
  if Options.Run.get () then begin
    change_printer ();
    ignore (generate_code (Options.Project_name.get ()));
  end

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