package frama-c

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

Source file RegionDump.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         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 Wp = Wp_parameters
module G = Dotgraph
module R = G.Node(Region.Map)

let node_default = [`Attr("fontname","monospace")]
let edge_default = [`Attr("fontname","monospace")]

let attr_offset = [ `Filled ; `Color "grey" ; `Box ]
let attr_write = [ `Label "W" ; `Fillcolor "green" ; `Filled ]
let attr_read  = [ `Label "R" ; `Fillcolor "green" ; `Filled ]
let attr_alias = [ `Label "&" ; `Fillcolor "orange" ; `Filled ]
let attr_merge = [ `Color "red" ; `Fillcolor "red" ; `Filled ]
let attr_shift = [ `Label "[]" ]
let attr_delta = [ `Filled ; `Color "lightblue" ; `Box ]
let attr_deref = [ `ArrowHead "tee" ]
let attr_cil = [ `Filled ; `Fillcolor "yellow" ]
let attr_region = `Shape "tab" :: attr_cil
let attr_var = `Shape "cds" :: attr_cil
let attr_garbled = [`Fillcolor "red";`Filled]
let attr_froms = [ `Color "blue" ; `Attr("dir","back") ]

let attr_pointed = [
  `Color "red"
]

let attr_pointed_deref = [
  `Attr("taillabel","*");
  `Attr("labelangle","+30");
  `Color "red";
]

let attr_pointed_shift = [
  `Attr("taillabel","[..]");
  `Attr("labeldistance","1.7");
  `Attr("labelangle","+40");
  `Color "red";
]

let rid_key = Wp.register_category "rid"
let dot_key = Wp.register_category "dot"
let pdf_key = Wp.register_category "pdf"
let deref_key = Wp.register_category "deref"
let roots_key = Wp.register_category "roots"
let froms_key = Wp.register_category "froms"
let cluster_key = Wp.register_category "cluster"
let chunk_key = Wp.register_category "chunk"
let offset_key = Wp.register_category "offset"

let sfprintf = Format.asprintf

let dotpointed ~label r =
  let attr =
    if Region.is_shifted r
    then attr_pointed_shift else attr_pointed_deref in
  let target = G.port (R.get r) "w" in
  `Port ("",["",attr,target],label)

let dotvalue ?(prefix="") value : Dotgraph.record =
  let open Layout in
  match value with
  | Int i -> `Label (sfprintf "%s%a" prefix Ctypes.pp_int i)
  | Float f -> `Label (sfprintf "%s%a" prefix Ctypes.pp_float f)
  | Pointer r -> dotpointed ~label:(prefix ^ "ptr") r

let dotrange ?(prefix="") rg : Dotgraph.record =
  let open Layout in
  let pp_dim fmt = function
    | Raw _ -> Format.pp_print_string fmt "raw"
    | Dim(s,ds) -> Format.fprintf fmt "%d%a" s Matrix.pretty ds
  in
  let label = sfprintf "%d..%d: %s%a"
      rg.ofs (rg.ofs + rg.len - 1)
      prefix pp_dim rg.dim in
  `Port("",["",[`Dotted],R.get rg.reg],label)

let dotcluster cluster : Dotgraph.record =
  let open Layout in
  match cluster with
  | Empty -> `Label "-"
  | Garbled -> `Label "Garbled"
  | Chunk v -> dotvalue v
  | Layout { sizeof ; layout } ->
    let label = Printf.sprintf "sizeof:%d" sizeof in
    `Hbox (`Label label :: List.map dotrange layout)

let dotchunk mem : Dotgraph.record =
  let open Layout in
  match mem with
  | Mraw(_,None) -> `Label "Raw"
  | Mraw(_,Some r) -> dotpointed ~label:"Raw" r
  | Mref r -> dotpointed ~label:"Ref" r
  | Mmem(rt,v) ->
    let prefix = if Layout.Root.indexed rt then "Mem " else "Var " in
    dotvalue ~prefix v
  | Mcomp(_,ovl) ->
    let range rg = dotrange
        ~prefix:(if Overlay.once rg.reg ovl then "D" else "C") rg in
    `Hbox (List.map range ovl)

let dotregion dot map region node =
  begin
    let is_read = Region.is_read region in
    let is_written = Region.is_written region in
    let is_aliased = Region.is_aliased region in
    let is_accessed = is_read || is_written || is_aliased in
    let has_deref = Wp.has_dkey deref_key && Region.has_deref region in
    let has_roots = Wp.has_dkey roots_key && Region.has_roots map region in
    let has_index_infos = has_deref || has_roots in
    let has_side_cluster =
      is_accessed ||
      has_index_infos ||
      Region.has_names region ||
      Wp.has_dkey offset_key ||
      Wp.has_dkey rid_key ||
      not (Wp.has_dkey cluster_key || Wp.has_dkey chunk_key) ||
      not (Wp.Region_fixpoint.get ())
    in
    if has_side_cluster then
      begin
        let attr = G.decorate [ `Oval ] [
            is_read , attr_read ;
            Region.has_pointed region , [ `Label "D" ] ;
            is_written , attr_write ;
            Region.is_shifted region , attr_shift ;
            is_aliased , attr_alias ;
            Region.get_alias map region != region , attr_merge ;
            Region.is_garbled region , attr_merge ;
          ] in
        G.node dot node attr ;
      end ;
    if Wp.has_dkey offset_key then
      Region.iter_offset map
        (fun offset target ->
           let label = Pretty_utils.to_string Layout.Offset.pretty offset in
           let delta = G.inode dot (`Label label :: attr_offset) in
           G.link dot [node;delta;R.get target] [`Dotted]
        ) region ;
    if Wp.has_dkey offset_key then
      Option.iter
        (fun target ->
           let label = if Region.is_shifted target then "[..]" else "*" in
           let deref = G.inode dot (`Label label :: attr_offset) in
           G.link dot [node;deref;R.get target] attr_pointed
        ) (Region.get_pointed map region) ;
    if has_index_infos then
      begin
        let derefs = ref [] in
        let label s = derefs := s :: !derefs in
        if has_roots then
          label @@ sfprintf "roots:%a"
            Layout.Root.pretty (Region.get_roots map region) ;
        if has_deref then
          Region.iter_deref
            (fun deref ->
               label @@ Pretty_utils.to_string Layout.Deref.pretty deref
            ) region ;
        if !derefs <> [] then
          begin
            let label = String.concat "\n" (List.rev !derefs) in
            let delta = G.inode dot (`Label label :: attr_delta) in
            G.rank dot [node;delta] ;
            G.edge dot delta node attr_deref
          end
      end ;
    if Wp.has_dkey cluster_key then
      begin
        let cluster = Region.cluster map region in
        if not (has_side_cluster && Layout.Cluster.is_empty cluster) then
          let record = dotcluster cluster in
          let attr = if Region.is_garbled region then attr_garbled else [] in
          if has_side_cluster then
            let delta = G.irecord dot ~attr record in
            G.edge dot node (G.port delta "w") attr_deref
          else
            G.record dot node ~attr record
      end ;
    if Wp.has_dkey chunk_key then
      begin
        let chunk = Region.chunk map region in
        let record = dotchunk chunk in
        let attr = if Region.is_garbled region then attr_garbled else [] in
        if has_side_cluster then
          let delta = G.irecord dot ~attr record in
          G.edge dot node (G.port delta "w") attr_deref
        else
          G.record dot node ~attr record
      end ;
    if Wp.has_dkey froms_key then
      begin
        let open Layout in
        List.iter
          (function
            | Fvar _ -> ()
            | Farray r ->
              G.edge dot (R.get r) node (`Label "[]"::attr_froms)
            | Fderef r ->
              G.edge dot (R.get r) node (`Label "*"::attr_froms)
            | Findex r ->
              G.edge dot (R.get r) node (`Label "+(..)"::attr_froms)
            | Ffield(r,ofs) ->
              let label = Printf.sprintf "+%d" ofs in
              G.edge dot (R.get r) node (`Label label::attr_froms)
          ) (Region.get_froms map region)
      end ;
    Region.iter_copies map
      (fun target ->
         G.edge dot node (R.get target) [`Color "green"]
      ) region ;
    Option.iter
      (fun target ->
         G.edge dot node (R.get target) [`Color "red"]
      ) (Region.get_merged map region) ;
  end

let dotvar dot x r =
  begin
    let open Cil_types in
    let xnode = G.inode dot ~prefix:"V" (`Label x.vname :: attr_var) in
    G.edge dot (G.port xnode "e") (R.get r) [] ;
  end

let dotlabel dot a r =
  begin
    let anode = G.inode dot ~prefix:"R" (`Label a :: attr_region) in
    let rnode = R.get r in
    G.rank dot [ anode ; rnode ] ;
    G.edge dot anode rnode []
  end

let dotrid dot r =
  dotlabel dot (Pretty_utils.to_string Region.R.pretty r) r

let dotstr dot r cst =
  dotlabel dot (String.escaped cst) r

let dotgraph dot map =
  begin
    G.node_default dot node_default ;
    G.edge_default dot edge_default ;
    R.clear () ;
    R.define dot (dotregion dot map) ;
    Region.iter_vars map (dotvar dot) ;
    Region.iter_strings map (dotstr dot) ;
    G.run dot ;
    if Wp.has_dkey rid_key then Region.iter map (dotrid dot) ;
    Region.iter_names map (dotlabel dot) ;
    if Region.has_return map then
      dotlabel dot "\\result" (Region.of_return map) ;
    Region.iter_fusion map (fun i r ->
        let rid = Region.id r in
        if i <> rid then
          dotlabel dot (Printf.sprintf "Fusion R%03d" i) r
        else
          dotlabel dot "Fusion (Self)" r
      ) ;
    G.run dot ;
  end

let dump_in_file ~file name map =
  if Wp.has_dkey dot_key || Wp.has_dkey pdf_key then
    begin
      let file = Pretty_utils.to_string Datatype.Filepath.pretty file in
      let dot = Dotgraph.open_dot ~attr:[`LR] ~name ~file () in
      dotgraph dot map ;
      Dotgraph.close dot ;
      let outcome =
        if Wp.has_dkey pdf_key
        then Dotgraph.layout dot
        else file in
      Wp.result "Region Graph: %s" outcome
    end

let dump_in_dir ~dir name map =
  let file = Datatype.Filepath.concat dir (name ^ ".dot") in
  dump_in_file ~file name map
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