package frama-c

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

Source file api.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
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
(**************************************************************************)
(*                                                                        *)
(*  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
module FC_file = File
open Cil_datatype

exception Cannot_expand
exception Cannot_change

(* Build the term [p+i], assuming that [p] has pointer type *)
let plus_pi ~loc p i =
  if Integer.(equal zero i) then
    p
  else
    Cil.mkBinOp ~loc PlusPI p (Cil.kinteger64 ~loc i)

(** This visitor also performs a deep copy. *)
class propagate project fnames ~cast_intro = object(self)
  inherit Visitor.frama_c_copy project

  (* Variables which have already been declared earlier in the list of
     globals. Varinfos of the old project. *)
  val mutable known_globals = Varinfo.Set.empty

  (* Variables whose declaration must be put before the global we are visiting.
     Reset before each global. Varinfos of the _new_ project. *)
  val mutable must_add_decl = Varinfo.Set.empty

  method! vstmt_aux s=
    (* Do not propagate on 'return' statements: one invariant of the AST is
       that they must be of the form 'return v;' where 'v' is a variable *)
    match s.skind with
    | Return _ -> Cil.JustCopy
    | _ -> Cil.DoChildren

  method! vfunc fundec =
    if Cil_datatype.Fundec.Set.is_empty fnames ||
       Cil_datatype.Fundec.Set.mem fundec fnames
    then begin
      PropagationParameters.feedback
        ~level:2
        "propagated constant in function %s"
        (fundec.svar.vname);
      Cil.DoChildren
    end else Cil.JustCopy

  method private add_decl_non_source_var vi =
    PropagationParameters.debug ~level:2
      "Need to declare %a earlier" Printer.pp_varinfo vi;
    let vi' =
      Visitor.visitFramacVarDecl (self :> Visitor.frama_c_visitor) vi
    in
    must_add_decl <- Varinfo.Set.add vi' must_add_decl;
    known_globals <- Varinfo.Set.add vi known_globals;
    if Cil.isFunctionType vi.vtype then begin
      let kf = Globals.Functions.get vi in
      let new_kf = Visitor_behavior.Memo.kernel_function self#behavior kf in
      Queue.add (fun () -> Globals.Functions.register new_kf)
        self#get_filling_actions;
    end

  (* introduce a new cast from [oldt] to [newt] or do not expand [e] *)
  method private add_cast ~ignore_const_cast ~oldt ~newt e =
    (* strip the superfluous 'const' attribute (see bts #1787) on
       pointed values. *)
    let oldt, newt =
      if ignore_const_cast then
        match Cil.unrollType oldt, Cil.unrollType newt with
        | TPtr(typ, attrs), TPtr(typ', attrs') ->
          let drop_const ty = Cil.typeRemoveAttributes ["const"] ty in
          TPtr(drop_const typ, attrs), TPtr(drop_const typ', attrs')
        | _ -> oldt, newt
      else
        oldt, newt
    in
    let exp = Cil.mkCastT ~oldt ~newt e in
    if cast_intro then
      exp
    else match exp.enode with
      | CastE _ ->
        if exp == e (* older cast, no new cast added *) then
          exp
        else begin
          (* without [cast_intro], introducing such a cast is not
             allowed: do not expand [e] *)
          PropagationParameters.debug
            ~level:2
            "Need a cast introduction (force using -scf-allow-cast option)";
          raise Cannot_expand
        end
      | _ ->
        (* remember the change done by [mkCastT] (if any).
           note that [mkCastT] make some modifications, even if it
           does not introduce a new cast. *)
        exp

  (* Make sure that [expr] is in the original project. *)
  method private propagated expr ~ignore_const_cast =
    PropagationParameters.debug ~level:2
      "Replacing %s%a?"
      (if ignore_const_cast then "(without const* cast) " else "")
      Printer.pp_exp expr;
    try
      let loc = expr.eloc in
      let typ = Cil.typeOf expr in
      let typ_e = Cil.unrollType typ in
      begin match typ_e with
        | (TInt _
          | TFloat _
          | TPtr _
          | TEnum _) -> ()
        | _ -> raise Cannot_expand
      end;
      let stmt = match self#current_stmt with
        | None -> raise Cannot_change
        | Some s -> s
      in
      let evaled = Eva.Results.(before stmt |> eval_exp expr |> as_cvalue) in
      let b, m = Cvalue.V.find_lonely_binding evaled in
      let can_replace vi =
        (* can replace the current expr by [vi] iff (1) it is a source var, or
           expansion of non-source var is allowed. *)
        (vi.vsource || PropagationParameters.ExpandLogicContext.get ())
        &&
        (* (2) [vi] is bound in this function *)
        (vi.vglob ||
         Option.fold
           ~some:(Kernel_function.is_formal_or_local vi) ~none:false
           self#current_kf)
      in
      let change_to = match b with
        | Base.Var(vi, _) | Base.Allocated (vi, _, _)
          when not (Base.is_weak b) &&  can_replace vi ->
          if vi.vglob && not (Varinfo.Set.mem vi known_globals) then
            self#add_decl_non_source_var vi;
          PropagationParameters.debug
            "Trying replacing %a from a pointer value {&%a + %a}"
            Printer.pp_exp expr Base.pretty b Ival.pretty m;
          let offset = Ival.project_int m in (* these are bytes *)
          let expr' =
            try
              if not (Cil.isPointerType typ_e) then
                raise Bit_utils.NoMatchingOffset;
              let typ_pointed = Cil.unrollType (Cil.typeOf_pointed typ_e) in
              if Cil.isVoidType typ_pointed then
                raise Bit_utils.NoMatchingOffset;
              let offset = Integer.mul offset Integer.eight in
              let m = Bit_utils.MatchType typ_pointed in
              let off, _ = Bit_utils.(find_offset vi.vtype ~offset m) in
              Cil.mkAddrOrStartOf ~loc (Var vi, off)
            with Bit_utils.NoMatchingOffset ->
              (* Build [((char* )&t[idx])+rem] when vi is an array, or
                 [(char* )(&vi+idx)+rem] otherwise. Automatically simplify
                 when [idx] or [rem] is zero. *)
              let array, idx, rem =
                let array, sizeof_pointed =
                  let array = Cil.isArrayType vi.vtype in
                  let size = if array
                    then Bit_utils.osizeof_pointed vi.vtype
                    else Bit_utils.osizeof vi.vtype
                  in
                  array, Int_Base.project size
                in
                let div,rem = Integer.e_div_rem offset sizeof_pointed in
                array,div,rem
              in
              let expr' =
                if array then
                  let off_idx =
                    if Integer.is_zero idx
                    then NoOffset
                    else Index (Cil.kinteger64 ~loc idx, NoOffset)
                  in
                  Cil.mkAddrOrStartOf ~loc (Var vi, off_idx)
                else
                  let start = Cil.mkAddrOrStartOf ~loc (Var vi, NoOffset) in
                  plus_pi ~loc start idx
              in
              if Integer.is_zero rem then expr'
              else
                plus_pi ~loc
                  (self#add_cast
                     ~ignore_const_cast:false
                     ~oldt:(Cil.typeOf expr')
                     ~newt:Cil.charPtrType
                     expr')
                  rem
          in
          (* preserve typing: propagating constant could change the type
             of the expression. We have to put back the original type. *)
          self#add_cast
            ~ignore_const_cast
            ~oldt:(Cil.typeOf expr')
            ~newt:typ
            expr'

        | Base.Null ->
          let const_integer m ikind =
            try
              let v = Ival.project_int m in
              if not (Cil.fitsInInt ikind v) then
                PropagationParameters.error "Constant found by Value (%a) \
                                             does not fit inside type %a. Please report"
                  Abstract_interp.Int.pretty v
                  Printer.pp_typ typ;
              Cil.kinteger64 ~loc ~kind:ikind v
            with Ival.Not_Singleton_Int -> raise Cannot_expand
          and const_float m fkind =
            try
              let f = Ival.project_float m in
              let f =  Fval.(F.to_float (project_float f)) in
              Cil.kfloat ~loc:expr.eloc fkind f
            with Fval.Not_Singleton_Float->
              raise Cannot_expand
          in
          (match typ_e with
           | TFloat (fkind, _) -> const_float m fkind
           | TInt (ikind, _) | TEnum ({ ekind = ikind}, _) ->
             const_integer m ikind
           | _ -> raise Cannot_expand)

        | Base.String _ | Base.Var _ | Base.Allocated _
        | Base.CLogic_Var _ -> raise Cannot_change
      in
      PropagationParameters.debug "Replacing %a with %a"
        Printer.pp_exp expr Printer.pp_exp change_to;
      Some change_to
    with
    | Cannot_change -> None
    | Not_found | Cannot_expand | Cil.Not_representable
    | Abstract_interp.Error_Top as e ->
      PropagationParameters.debug "Replacement failed %s"
        (Printexc.to_string e);
      None

  method! vexpr expr =
    (* nothing is done for [expr] already being a constant *)
    match expr.enode with
    | Const (_) -> Cil.DoChildren
    | _ -> begin
        (* Start by trying to constant-propagate all of [expr]. Casts are allowed
           only if -scf-allow-cast is set *)
        match self#propagated expr ~ignore_const_cast:false with
        | Some expr' -> Cil.ChangeDoChildrenPost (expr', fun x -> x)
        | None -> begin
            (* Global constant propagation of [expr] failed. We try a special
               const-folding, AND simplify the sub-expressions in all cases *)
            match expr.enode with
            | Lval (Mem exp_mem, off) -> begin
                (* [expr] is a Mem. Try to see if we can propagate [exp_mem] into
                   something simpler, because the result will be of the form
                   [Var _, offs'], which can be simplified under a [Mem]. This time,
                   we ignore const-related casts when simplifying [exp_mem], because
                   they will disappear when the l-value is dereferenced. *)
                match self#propagated exp_mem ~ignore_const_cast:true with
                | Some exp_mem' ->
                  let lv =
                    Cil.new_exp ~loc:expr.eloc (Lval (Cil.mkMem ~addr:exp_mem' ~off))
                  in
                  Cil.ChangeDoChildrenPost (lv, fun x -> x)
                | None -> Cil.DoChildren
              end
            | _ -> Cil.DoChildren
          end
      end

  method! vvdec v =
    if v.vglob then begin
      known_globals <- Varinfo.Set.add v known_globals;
    end;
    Cil.DoChildren

  method! vglob_aux g =
    must_add_decl <- Varinfo.Set.empty;
    (* Check if [g] has already been declared earlier, due to being used in
       some earlier values. If so, we will skip [g]. We do this check now and
       not in [add_decls], because [self#vvdec] will mark g as known. *)
    let g_is_known = match g with
      | GVarDecl (vi, _) | GFunDecl (_, vi, _) -> Varinfo.Set.mem vi known_globals
      | _ -> false
    in
    let add_decls l =
      (* Do not re-add a declaration for g if it is known. *)
      let l = if g_is_known then [] else l in
      (* Add declarations for the globals that are referenced in g's propagated
         value. *)
      Varinfo.Set.fold
        (fun vi l ->
           PropagationParameters.feedback ~level:2
             "Adding declaration of global %a" Printer.pp_varinfo vi;
           let g' =
             if Cil.isFunctionType vi.vtype
             then GFunDecl(Cil.empty_funspec(), vi, vi.vdecl)
             else GVarDecl(vi, vi.vdecl)
           in
           g' ::l)
        must_add_decl l
    in
    Cil.DoChildrenPost add_decls

  method! vlval lv =
    let simplify (host,off as lv) = match host with
      | Mem e -> Cil.mkMem ~addr:e ~off (* canonize in case the propagation
                                           simplified [lv] *)
      | Var _ -> lv
    in
    Cil.ChangeDoChildrenPost(lv, simplify)

end

module Result_pair =
  Datatype.Pair_with_collections(Cil_datatype.Fundec.Set)(Datatype.Bool)
    (struct let module_name = "Constant_propagation.Register.Result_pair.t" end)
module Result =
  State_builder.Hashtbl
    (Datatype.Hashtbl
       (Result_pair.Hashtbl)
       (Result_pair)
       (struct let module_name = "Semantical constant propagation" end))
    (Project.Datatype)
    (struct
      let size = 7
      let name = "Semantical constant propagation"
      let dependencies =
        [ Eva.Analysis.self;
          PropagationParameters.CastIntro.self;
          PropagationParameters.Project_name.self ]
    end)

let selection_command_line_option =
  State_selection.singleton PropagationParameters.SemanticConstFolding.self

(* add labels *)
let get fnames ~cast_intro =
  Result.memo
    (fun _ ->
       Eva.Analysis.compute ();
       let fresh_project =
         FC_file.create_project_from_visitor
           (PropagationParameters.Project_name.get ())
           (fun prj -> new propagate prj fnames ~cast_intro)
       in
       let ctx = Parameter_state.get_selection_context () in
       let ctx = State_selection.diff ctx selection_command_line_option in
       Project.copy ~selection:ctx fresh_project;
       fresh_project)
    (fnames, cast_intro)

(** Constant Propagation *)

let compute () =
  PropagationParameters.feedback "beginning constant propagation";
  let fnames = PropagationParameters.SemanticConstFold.get () in
  let cast_intro = PropagationParameters.CastIntro.get () in
  let propagated = get fnames ~cast_intro in
  if PropagationParameters.SemanticConstFolding.get () then
    FC_file.pretty_ast ~prj:propagated ();
  let project_name = Project.get_unique_name propagated in
  PropagationParameters.feedback  "@[constant propagation done%t@]"
    (fun fmt ->
       if project_name <> PropagationParameters.Project_name.get () then
         Format.fprintf fmt ",@ result is in project@ `%s`" project_name)

let compute, self =
  let name = "Constant_Propagation.compute" in
  let deps = [ PropagationParameters.SemanticConstFold.self;
               PropagationParameters.SemanticConstFolding.self;
               Result.self ]
  in
  State_builder.apply_once name deps compute

let main () =
  let force_semantic_folding =
    PropagationParameters.SemanticConstFolding.get ()
    || not (Cil_datatype.Fundec.Set.is_empty
              (PropagationParameters.SemanticConstFold.get ()))
  in
  if force_semantic_folding then compute ()

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