package frama-c

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

Source file translate.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
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-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).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Va_types
open Options
module Typ = Extends.Typ

(* List of builtin function names to translate *)

let is_framac_builtin vi = Classify.is_frama_c_builtin vi.vname

(* In place visitor for translation *)

let translate_variadics (file : file) =
  (* Environment filled with global symbols. *)
  let env = Environment.from_file file in

  (* Table associating varinfo of variadic functions to a variadic_function
     description *)
  let module Table = Cil_datatype.Varinfo.Hashtbl in
  let classification : variadic_function Table.t = Table.create 17 in
  let v = object
    inherit Cil.nopCilVisitor

    method! vglob glob =
      begin match glob with
        | GFunDecl(_, vi, _) | GFun ({svar = vi}, _) ->
          if not (Table.mem classification vi) then begin
            let vf = Classify.classify env vi in
            Option.iter (Table.add classification vi) vf
          end;
          Cil.SkipChildren
        | _ ->
          Cil.SkipChildren
      end
  end
  in
  Cil.visitCilFile v file;

  (* Utility function that tells if there is a call inside a statement *)
  let contains_call stmt =
    let result = ref false in
    let vis = object
      inherit Cil.nopCilVisitor
      method! vinst = function
        | Call _ -> result := true; Cil.SkipChildren
        | _ -> Cil.DoChildren
      method! vexpr _ = Cil.SkipChildren
      method! vtype _ = Cil.SkipChildren
    end
    in
    ignore (Cil.visitCilStmt vis stmt);
    !result
  in

  (* The translating visitor *)
  let v = object (self)
    inherit Cil.nopCilVisitor

    val curr_block = Stack.create () (* Opened blocks to store generated locals *)
    val mutable pending_globals = [] (* List of globals to add before the current global once it's finished visiting *)

    method! vblock b =
      Stack.push b curr_block;
      Cil.DoChildrenPost (fun b -> ignore (Stack.pop curr_block); b)

    method private enclosing_block () =
      try Stack.top curr_block
      with Stack.Empty -> Options.Self.fatal "No enclosing block here"

    method private make_builder ~loc ~fundec ~ghost ~mk_call =
      let module B =
      struct
        include Cil_builder.Stateful ()

        let loc = loc

        let finish_function () =
          pending_globals <- finish_function () :: pending_globals

        let finish_declaration () =
          pending_globals <-
            finish_declaration ~register:false () :: pending_globals

        let start_translation () =
          open_block ~loc ~into:fundec ~ghost ()

        let translated_call callee args =
          of_instr
            (mk_call (cil_exp ~loc callee) (List.map (cil_exp ~loc) args))
      end
      in
      (module B : Builder.S)


    method! vtype _typ =
      Cil.DoChildrenPost (Generic.translate_type)

    (* Translate types and signatures *)
    method! vglob glob =
      begin match glob with
        | GFunDecl(_, vi, _) ->
          (match Table.find_opt classification vi with
           | None -> Cil.DoChildren (* may transform the type *)
           | Some { vf_class = Builtin } ->
             Self.result ~level:2 ~current:true
               "Variadic builtin %s left untransformed." vi.vname;
             Cil.SkipChildren
           | Some _ ->
             Generic.add_vpar vi;
             Cil.DoChildren)

        | GFun ({svar = vi} as fundec, _) ->
          if Table.mem classification vi then begin
            Generic.add_vpar vi;
            fundec.sformals <- Cil.getFormalsDecl vi;
          end;
          pending_globals <- [];
          Cil.DoChildrenPost (fun globs ->
              List.rev_append pending_globals globs)

        | _ ->
          Cil.DoChildren
      end

    method! vstmt s =
      match s.skind with
      | Instr (Call _) ->
        (* Separate locals created by a variadic call in their own block.
           This can't be done for Local_init(x,ConsInit _,_), as this
           instruction must be kept a direct child of the enclosing block,
           that determines the scope of x.
        *)
        let block = Cil.mkBlock [] in
        Stack.push block curr_block;
        let keep_block_if_needed s =
          ignore (Stack.pop curr_block);
          match s.skind with
          | Block b' ->
            (* We have introduced several instructions, and potentially locals.
               Scope of locals is in [block], that will replace b'. *)
            block.bstmts <- b'.bstmts;
            s.skind <- Block block;
            s
          | _ -> s
        in
        Cil.DoChildrenPost keep_block_if_needed
      | UnspecifiedSequence _ ->
        let update_seq_if_needed s =
          match s.skind with
          | UnspecifiedSequence seq ->
            let update (stmt,modified,writes,reads,calls) =
              let contains_call' stmt_ref = contains_call !stmt_ref in
              (stmt,modified,writes,reads,List.filter contains_call' calls)
            in
            s.skind <- UnspecifiedSequence (List.map update seq);
            s
          | _ -> s
        in
        Cil.DoChildrenPost update_seq_if_needed
      | _ -> Cil.DoChildren

    (* Replace variadic calls *)
    method! vinst i =
      let fundec = Option.get self#current_func in
      let loc = Cil_datatype.Instr.loc i in
      let block = self#enclosing_block () in
      let ghost = (Option.get self#current_stmt).ghost in
      let translate_call mk_call translator args =
        File.must_recompute_cfg fundec;
        let builder = self#make_builder ~loc ~fundec ~ghost ~mk_call in
        translator ~builder args;
        let module Builder = (val builder : Builder.S) in
        Builder.finish_instr_list ~scope:block ()
      in
      let mk_translator f =
        let vf = Table.find classification f in
        let cover_failure f =
          fun ~builder args ->
            try
              f ~builder args
            with Standard.Translate_call_exn callee ->
              Standard.fallback_fun_call ~callee ~builder env vf args
        in
        match vf.vf_class with
        | Overload o -> cover_failure (Standard.overloaded_call o vf)
        | Aggregator a -> cover_failure (Standard.aggregator_call a vf)
        | FormatFun f -> cover_failure (Standard.format_fun_call env f vf)
        | Builtin ->
          Self.result ~level:2 ~current:true
            "Call to variadic builtin %s left untransformed." f.vname;
          raise Not_found
        | _ ->
          Generic.translate_call (Cil.evar ~loc f)
      in
      begin match i with
        (* Translate builtins *)
        | Call(_, {enode = Lval(Var vi, _)}, _, _)
          when Classify.is_va_builtin vi.vname ->
          File.must_recompute_cfg fundec;
          Cil.ChangeTo (Generic.translate_va_builtin fundec i)

        (* Translate variadic calls *)
        | Call(lv, {enode = Lval(Var vi, NoOffset)}, args, loc) ->
          begin
            try
              let mk_call f args = Call (lv, f, args, loc) in
              let translator = mk_translator vi in
              let instr_list = translate_call mk_call translator args in
              Cil.ChangeTo instr_list
            with Not_found ->
              Cil.DoChildren
          end

        | Call(lv, callee, args, loc) ->
          let is_variadic =
            List.mem Generic.vpar (Typ.params (Cil.typeOf callee))
          in
          if is_variadic then begin
            let mk_call f args = Call (lv, f, args, loc) in
            let translator = Generic.translate_call callee in
            let instr_list = translate_call mk_call translator args in
            Cil.ChangeTo instr_list
          end else
            Cil.DoChildren

        | Local_init(v, ConsInit(c, args, kind), loc) ->
          begin
            try
              let mk_call f args =
                let args =
                  match kind, args with
                  | Constructor, [] ->
                    Options.Self.fatal
                      "Constructor %a is expected to have at least one argument"
                      Cil_printer.pp_varinfo c
                  | Constructor, _::tl -> tl
                  | Plain_func, args -> args
                in
                let f =
                  match f.enode with
                  | Lval (Var f, NoOffset) -> f
                  | _ ->
                    Options.Self.fatal
                      "Constructor cannot be translated as indirect call"
                in
                Local_init(v,ConsInit(f,args,kind),loc)
              in
              let args =
                match kind with
                | Plain_func -> args
                | Constructor -> Cil.mkAddrOfVi v :: args
              in
              let translator = mk_translator c in
              let instr_list = translate_call mk_call translator args in
              Cil.ChangeTo instr_list
            with Not_found ->
              Cil.DoChildren
          end
        | _-> Cil.DoChildren
      end

    method! vexpr exp =
      begin match exp.enode with
        | AddrOf (Var vi, NoOffset)
          when Classify.is_variadic_function vi && is_framac_builtin vi ->
          Self.not_yet_implemented
            ~source:(fst exp.eloc)
            "The variadic plugin doesn't handle calls to a pointer to the \
             variadic builtin %s."
            vi.vname
        | _ -> Cil.DoChildren
      end
  end
  in
  Cil.visitCilFile v file
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