package frama-c

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

Source file print.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
(**************************************************************************)
(*                                                                        *)
(*  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

let pretty_stmt fmt s = Cil_printer.pp_stmt fmt s

module Printer = struct

  type t = string * (Stmt.Hptset.t option Kinstr.Hashtbl.t)
  module V = struct
    type t = Cil_types.stmt * bool
    let pretty fmt v = pretty_stmt fmt v
  end
  module E = struct
    type t = (V.t * V.t)
    let src e = fst e
    let dst e = snd e
  end

  let iter_vertex f (_, graph) =
    let do_s ki postdom =
      let s = match ki with Kstmt s -> s | _  -> assert false in
      Postdominators_parameters.debug "iter_vertex %d : %a\n" s.sid V.pretty s;
      let has_postdom = match postdom with None -> false | _ -> true in
      f (s, has_postdom)
    in
    Kinstr.Hashtbl.iter do_s graph

  let iter_edges_e f (_, graph) =
    let do_s ki postdom =
      let s = match ki with Kstmt s -> s | _  -> assert false in
      match postdom with None -> ()
                       | Some postdom ->
                         let do_edge p = f ((s, true), (p, true)) in
                         Stmt.Hptset.iter do_edge postdom
    in
    Kinstr.Hashtbl.iter do_s graph


  let vertex_name (s, _) = string_of_int s.sid

  let graph_attributes (title, _) = [`Label title]

  let default_vertex_attributes _g = [`Style `Filled]
  let default_edge_attributes _g = []

  let vertex_attributes (s, has_postdom) =
    let attrib = [] in
    let txt = Format.asprintf "%a" V.pretty s in
    let attrib = (`Label txt) :: attrib in
    let color = if has_postdom then 0x7FFFD4 else 0xFF0000 in
    let attrib = (`Shape `Box) :: attrib in
    let attrib = (`Fillcolor color) :: attrib in
    attrib

  let edge_attributes _s = []

  let get_subgraph _v = None
end

module PostdomGraph = Graph.Graphviz.Dot(Printer)

let get_postdom kf graph s =
  try
    match Kinstr.Hashtbl.find graph (Kstmt s) with
    | None -> Stmt.Hptset.empty
    | Some l -> l
  with Not_found ->
  try
    let postdom = Compute.stmt_postdominators kf s in
    let postdom = Stmt.Hptset.remove s postdom in
    Postdominators_parameters.debug "postdom for %d:%a = %a\n"
      s.sid pretty_stmt s Stmt.Hptset.pretty postdom;
    Kinstr.Hashtbl.add graph (Kstmt s) (Some postdom); postdom
  with Compute.Top ->
    Kinstr.Hashtbl.add graph (Kstmt s) None;
    raise Compute.Top

(** [s_postdom] are [s] postdominators, including [s].
 * We don't have to represent the relation between s and s.
 * And because the postdom relation is transitive, if [p] is in [s_postdom],
 * we can remove [p_postdom] from [s_postdom] in order to have a clearer graph.
*)
let reduce kf graph s =
  let remove p s_postdom =
    if Stmt.Hptset.mem p s_postdom
    then
      try
        let p_postdom = get_postdom kf graph p in
        let s_postdom = Stmt.Hptset.diff s_postdom p_postdom
        in s_postdom
      with Compute.Top -> assert false
      (* p postdom s -> cannot be top *)
    else s_postdom (* p has already been removed from s_postdom *)
  in
  try
    let postdom = get_postdom kf graph s in
    let postdom = Stmt.Hptset.fold remove postdom postdom in
    Postdominators_parameters.debug "new postdom for %d:%a = %a\n"
      s.sid pretty_stmt s Stmt.Hptset.pretty postdom;
    Kinstr.Hashtbl.replace graph (Kstmt s) (Some postdom)
  with Compute.Top ->
    ()

let build_reduced_graph kf graph stmts =
  List.iter (reduce kf graph) stmts

let build_dot filename kf =
  match kf.fundec with
  | Definition (fct, _) ->
    let stmts = fct.sallstmts in
    let graph = Kinstr.Hashtbl.create (List.length stmts) in
    let _ = build_reduced_graph kf graph stmts in
    let name = Kernel_function.get_name kf in
    let title = "Postdominators for function " ^ name in
    let file = open_out filename in
    PostdomGraph.output_graph file (title, graph);
    close_out file
  | Declaration _ ->
    Kernel.error "cannot compute for a function without body %a"
      Kernel_function.pretty kf

(*
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