@@ -92,7 +92,62 @@ To be documented.
92
92
93
93
\subsection analyses-dependence-graph Data- and control-dependence analysis (dependence_grapht)
94
94
95
- To be documented.
95
+ ### Dependence graph
96
+
97
+ Implemented in ` src/analyses/dependence_graph.h(cpp) ` . It is a graph and an
98
+ abstract interpreter in the same time. The abstract interpretation nature
99
+ allows a dependence graph to build itself (the graph) from a given GOTO program.
100
+
101
+ A dependence graph extends the class ` grapht ` with ` dep_nodet ` as the type of
102
+ nodes (see ` src/util/graph.h ` for more details about
103
+ [ graph representation] ( ../util/README.md ) ).
104
+ The ` dep_nodet ` extends ` graph_nodet<dep_edget> ` by an iterator to a GOTO
105
+ program instruction. it means that each graph node corresponds to a particular
106
+ program instruction. A labelled edge ` (u, v) ` of a dependence graph expresses
107
+ a dependency of program instruction corresponding to node ` u ` on the program
108
+ instruction corresponding to node ` v ` . The label of the edge denoted the kind
109
+ of dependency. It can be ` control-dependency ` , ` data-dependency ` , or both.
110
+
111
+ #### Control dependency
112
+
113
+ An instruction ` j ` corresponding to node ` v ` is control-dependent on instruction
114
+ ` i ` corresponding to node ` u ` if and only if ` j ` post-dominates at least one
115
+ but not all of successors of ` i ` .
116
+
117
+ An instruction ` j ` post-dominates an instruction ` i ` if and only if each
118
+ execution path going through ` i ` eventually reaches ` j ` .
119
+
120
+ Post-dominators analysis implemented in ` src/analyses/cfg_dominators.h(cpp) ` .
121
+
122
+ #### Data dependency
123
+
124
+ The instruction ` j ` corresponding to node ` v ` is data-dependent on instruction
125
+ ` i ` corresponding to node ` u ` if and only if ` j ` may read data from memory
126
+ location defined (i.e. written) by ` i ` .
127
+
128
+ Reaching definitions analysis together with read-write ranges analysis are used
129
+ to check whether one instruction may read data writen by another instruction.
130
+ For more details see ` src/analyses/reaching_definitions.h(cpp) ` and
131
+ ` src/analyses/goto_rw.h(cpp) ` .
132
+
133
+ #### Construction
134
+
135
+ The dependence graph extends the standard abstract interpreter is class ` ait `
136
+ with post-dominators analysis and reaching definitions analysis. The domain of
137
+ the abstract interpreter is defined in the class ` dep_graph_domaint ` .
138
+
139
+ For each instruction ` i ` there is created an instance of ` dep_graph_domaint ` .
140
+ That instance stores a set ` control_deps ` of program instructions ` i ` depends
141
+ on via control-dependency, and a set ` data_deps ` of program instructions ` i `
142
+ depends on via data-dependency. These sets are updated (increased) during the
143
+ computation until a fix-point is reached.
144
+
145
+ The construction of a dependence graph is started by calling its ` initialize `
146
+ method and then, once a fix-point is reached by the abstract interpreter, the
147
+ method ` finalize ` converts data in the interpreter's domain (i.e. inside
148
+ ` dep_graph_domaint ` instances) into edges of the graph. Nodes of the graph are
149
+ created during the run of the abstract interpreter; they are linked to the
150
+ corresponding program instructions.
96
151
97
152
\subsection analyses-dirtyt Address-taken lvalue analysis (dirtyt)
98
153
0 commit comments