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
|
#*************************************************************************#
#* #
#* This file is part of Frama-C. #
#* #
#* Copyright (C) 2007-2016 #
#* 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). #
#* #
#*************************************************************************#
{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.
You can find more documentation, particularly on how this graph is built,
in this {{:../../pdg/index.html}report} (in French).
{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.
You are invited to look at
{{:../../../tests/pdg/doc.g.svg}a simple example}
to see the different kinds of dependencies.
|
