package frama-c

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

Source file 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
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
(**************************************************************************)
(*                                                                        *)
(*  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 Cil_datatype
open Cil
open Visitor
open Options

module Occurrence_datatype =
  Datatype.Triple(Datatype.Option(Kernel_function))(Kinstr)(Lval)

module Occurrences: sig
  val add: varinfo -> kernel_function option -> kinstr -> lval -> unit
  val get: varinfo -> (kernel_function option * kinstr * lval) list
  val self: State.t
  val get_last_result: unit ->
    ((Kernel_function.t option * Cil_types.kinstr *
      (Cil_types.lhost * Cil_types.offset))
       list * Cil_types.varinfo)
      option
  val iter_sorted:
    (varinfo -> (kernel_function option * kinstr * lval) list -> unit) -> unit
end = struct

  module IState =
    Cil_state_builder.Varinfo_hashtbl
      (Occurrence_datatype)
      (struct
        let size = 17
        let name = "Occurrences.State"
        let dependencies = [ Eva.Analysis.self ]
      end)

  module LastResult =
    State_builder.Option_ref
      (Varinfo)
      (struct
        let name = "Occurrences.LastResult"
        let dependencies = [ Ast.self; IState.self ]
      end)

  let add vi kf ki lv = IState.add vi (kf, ki, lv)

  let unsafe_get vi = try IState.find_all vi with Not_found -> []

  let get vi =
    LastResult.set vi;
    unsafe_get vi

  let get_last_result () =
    try
      let vi = LastResult.get () in
      Some (unsafe_get vi, vi)
    with Not_found ->
      None

  let iter_aux fold f =
    let old, l =
      fold
        (fun v elt (old, l) -> match v, old with
           | v, None ->
             assert (l = []);
             Some v, [ elt ]
           | v, (Some old as some) when Varinfo.equal v old ->
             some, elt :: l
           | v, Some old ->
             f old l;
             Some v, [ elt ])
        (None, [])
    in
    Option.iter (fun v -> f v l) old

  let fold_sorted f init =
    let map = IState.fold Varinfo.Map.add Varinfo.Map.empty in
    Varinfo.Map.fold f map init

  let iter_sorted = iter_aux fold_sorted

  let self = IState.self

end

class occurrence = object (self)

  inherit Visitor.frama_c_inplace as super

  method! vlval lv =
    let ki = self#current_kinstr in
    begin
      let z = Eva.Results.(before_kinstr ki |> eval_address lv |> as_zone) in
      try
        Locations.Zone.fold_topset_ok
          (fun b _ () ->
             match b with
             | Base.Var (vi, _) | Base.Allocated (vi, _, _) ->
               Occurrences.add vi self#current_kf ki lv
             | _ -> ()
          ) z ()
      with Abstract_interp.Error_Top ->
        error ~current:true "Found completely imprecise value (%a). Ignoring@."
          Printer.pp_lval lv
    end;
    DoChildren

  method! vterm_lval tlv =
    (try
       let lv = Logic_to_c.term_lval_to_lval tlv in
       ignore (self#vlval lv)
     with
     (* Translation to lval failed.*)
     | Logic_to_c.No_conversion -> ());
    DoChildren

  method! vstmt_aux s =
    Async.yield ();
    super#vstmt_aux s

  initializer Eva.Analysis.compute ()

end

type access_type = Read | Write | Both

(** Try to find [lv] somewhere within a Cil value *)
class is_sub_lval lv = object
  inherit Cil.nopCilVisitor

  method! vlval lv' =
    if Cil_datatype.Lval.equal lv lv' then raise Exit;
    DoChildren
end

(** Occurrence has found the given [lv] somewhere inside [ki]. We try to find
    whether this was inside a read or a write operation. This is difficult to
    do directly inside the {!occurrence} class, as the [vlval] method
    has no information about the origin of the lval it was called on *)
let classify_accesses (_kf, ki, lv) =
  let vis = new is_sub_lval lv in
  let aux f v = try ignore (f vis v); false with Exit -> true in
  let is_lv = Cil_datatype.Lval.equal lv in
  let contained_exp = aux Cil.visitCilExpr in
  match ki with
  | Kglobal -> (* Probably initializers *) Read

  | Kstmt { skind = Instr i } ->
    (match i with
     | Set (lv', e, _) ->
       if is_lv lv' then
         if contained_exp e then Both
         else Write
       else Read

     | Call (Some lv', f, args, _) ->
       if is_lv lv' then
         if contained_exp f || List.exists contained_exp args then Both
         else Write
       else Read

     | Local_init (v, _, _) ->
       (match lv with
        | Var v', _ when Cil_datatype.Varinfo.equal v v' ->
          (* We are initializing v. We can't read from it at the same time.
             Hence, there's no need to perform the additional checks done
             in the cases above. *)
          Write
        | _ -> Read)

     | Asm (_, _, Some { asm_outputs; asm_inputs },_) ->
       if List.exists (fun (_, _, out) -> is_lv out) asm_outputs then
         if List.exists (fun (_, _, inp) -> contained_exp inp) asm_inputs
         then Both
         else Write
       else Read

     | _ -> Read)
  | _ -> Read

let compute, _self =
  let run () =
    feedback "beginning analysis";
    ignore (visitFramacFile (new occurrence) (Ast.get ()));
    feedback "analysis done"
  in
  State_builder.apply_once "Occurrence.compute" [ Occurrences.self ] run

let get vi =
  compute ();
  try Occurrences.get vi with Not_found -> assert false

let d_ki fmt = function
  | None, Kglobal -> Format.fprintf fmt "global"
  | Some kf, Kglobal ->
    Format.fprintf fmt "specification of %a" Kernel_function.pretty kf
  | _, Kstmt s -> Format.fprintf fmt "sid %d" s.sid

let print_one fmt v l =
  Format.fprintf fmt "variable %s (%s):@\n"
    v.vname
    (if v.vglob then "global"
     else
       let kf_name = match l with
         | [] -> assert false
         | (Some kf, _, _) :: _ -> Kernel_function.get_name kf
         | (None,Kstmt _,_)::_ -> assert false
         | (None,Kglobal,_)::_ ->
           fatal "inconsistent context for occurrence of variable %s" v.vname
       in
       if v.vformal then "parameter of " ^ kf_name
       else "local of " ^ kf_name);
  List.iter
    (fun (kf, ki, lv) ->
       Format.fprintf fmt "  %a: %a@\n" d_ki (kf,ki) Printer.pp_lval lv) l

let print_all () =
  compute ();
  result "%t" (fun fmt -> Occurrences.iter_sorted (print_one fmt))

(* ************************************************************************** *)
(* Exported API *)
(* ************************************************************************** *)

let self = Occurrences.self
let get_last_result = Occurrences.get_last_result
let get = get
let print_all = print_all

(* ************************************************************************** *)
(* Main *)
(* ************************************************************************** *)

let main _fmt = if Print.get () then print_all ()
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