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

(* Basic plug-in internal documentation at the end of this file. *)

open Pdg_types

let () =
  Cmdline.run_after_extended_stage
    (fun () ->
       State_dependency_graph.add_codependencies
         ~onto:Pdg_tbl.self
         [ From.self ])

let deps =
  [Pdg_tbl.self; Pdg_parameters.BuildAll.self; Pdg_parameters.BuildFct.self]

let () = Pdg_parameters.BuildAll.set_output_dependencies deps

let compute_for_kf kf =
  let all = Pdg_parameters.BuildAll.get () in
  (all && Eva.Results.is_called kf) ||
  Kernel_function.Set.mem kf (Pdg_parameters.BuildFct.get ())

let compute () =
  Eva.Analysis.compute ();
  let do_kf_pdg kf =
    if compute_for_kf kf then
      let pdg = Pdg_tbl.get kf in
      let dot_basename = Pdg_parameters.DotBasename.get () in
      if dot_basename <> "" then
        let fname = Kernel_function.get_name kf in
        Pdg_tbl.print_dot pdg (dot_basename ^ "." ^ fname ^ ".dot")
  in
  Callgraph.Uses.iter_in_rev_order do_kf_pdg;
  let pp_sep fmt () = Format.pp_print_string fmt "," in
  Pdg_parameters.(
    debug "Logging keys : %a"
      (Format.pp_print_list ~pp_sep pp_category) (get_debug_keys ()));
  if Pdg_parameters.BuildAll.get () then
    Pdg_parameters.feedback "====== PDG GRAPH COMPUTED ======"

let compute_once, _ =
  State_builder.apply_once "Pdg.Register.compute_once" deps compute

let output () =
  let bw  = Pdg_parameters.PrintBw.get () in
  let do_kf_pdg kf =
    if compute_for_kf kf then
      let pdg = Pdg_tbl.get kf in
      let header fmt =
        Format.fprintf fmt "PDG for %a" Kernel_function.pretty kf
      in
      Pdg_parameters.printf ~header "@[ @[%a@]@]"
        (PdgTypes.Pdg.pretty_bw ~bw) pdg
  in
  Callgraph.Uses.iter_in_rev_order do_kf_pdg

let something_to_do () =
  Pdg_parameters.BuildAll.get ()
  || not (Kernel_function.Set.is_empty (Pdg_parameters.BuildFct.get ()))

let main () =
  if something_to_do () then
    (compute_once ();
     Pdg_parameters.BuildAll.output output)

let () = Boot.Main.extend main

(* {2 Overview}

   The main modules are :
   - {!module: PdgIndex} that can be used to store different kind of information
     related to a function (not only related to PDG)
   - the types are defined in {!module: PdgTypes}.
   - the PDG computation is done in {!module: Build}.  It also use the lexical
     successor graph, which is computed in {!module:Lexical_successors}.
   - {!module:Sets} provides functions to read a PDG.
   - {!module:Print} provides functions to print a PDG either in textual form or
     in a dot file (See {i "How to see a PDG"} below).


   {2 What is a PDG ?}

   A {b Program Dependences Graph} represent the dependences between the
   statements of a function. So the nodes of the graph mainly represent the
   statements (some more nodes are used to represents things like declarations,
   inputs, outputs, etc.) and the edges represent the dependences.

   [Y -> X] means that the computation of the statement Y depend on (the result of)
   the statement X. Example :
   {C {v X : x = a + b; Y : y = x + 1; v}}

   There are three kinds of dependencies :
   - a {b data} dependency : the simpler one, illustrated by the above example,
   - a {b control} dependency :
     {C Example : {v if (c) X : x = a + b; v}}
     X is control dependent on (c) because the statement will be executed or not
     according to the evaluation of the condition,
   - an {b address} dependency : dependencies on the elements that are used to
     compute the left part of an assignment, ie that decide which data will be
     modified.
     {C Example : {v t[i] = 3; v}}
    We say that this statement have address dependencies on the declaration of
    [tab] and the computation of [i].

   A dependency between two nodes can have any combination of these kinds.

   {2 Dynamic dependencies}

   After having built the PDG for a function, there is a way of adding dynamically
   some dependencies to it. There are not stored directly in the PDG so they can be
   cleared later on.

   As PDG doesn't interpret the annotations of the code,
   this feature can for instance be used to add dependencies on assertions.

   To see an example of how to use it, please have a look at
   [tests/pdg/dyn_dpds.ml].

   {2 How to see a PDG ?}

   Please, use the [-help] option of the tool to get the PDG options names.

   The PDG of a function can be seen either in textual form
   or exported in a {b dot} file
   which is the format of the {{:http://www.graphviz.org/}Graphviz}
   tool set.
   They can be viewed using
   {{:http://zvtm.sourceforge.net/zgrviewer.html}zgrviewer}
   or exported in SVG format to be seen with some browser
   or {{:http://www.inkscape.org/}Inkscape}.

   The graph is unfortunately generated with the output of the function at the top
   and its inputs at the bottom. If you find it uncomfortable to read,
   just change [TB] by [BT] in the [rankdir] property at the beginning of the
   dot file before viewing it.

   The color and the shape of the nodes are used to make it easier to read the
   graph, but add no more meaning.

   For the edges :
   - the color (blue) represent the {b data} dependency,
   - the shape of the arrow (circled) represent the {b control} dependency,
   - and the kind of line (dotted) represent the {b address} dependency.

   So a solid blue edge with a circle arrow represent a data+control dependency for
   instance, while a dotted black edge with a triangle arrow represent a address
   dependency.
*)


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