Skip to content

Commit 1da964c

Browse files
committed
An overview of grapht and dependence_grapht in corresponding README.md.
1 parent 4293897 commit 1da964c

File tree

2 files changed

+100
-1
lines changed

2 files changed

+100
-1
lines changed

src/analyses/README.md

Lines changed: 58 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,64 @@ To be documented.
9292

9393
\subsection analyses-dependence-graph Data- and control-dependence analysis (dependence_grapht)
9494

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 the program instruction corresponding to node `u` on the program
108+
instruction corresponding to node `v`. The label of the edge (i.e. data of the
109+
type `dep_edget` attached to the edge) denotes the kind of dependency. It can be
110+
`control-dependency`, `data-dependency`, or both.
111+
112+
#### Control dependency
113+
114+
An instruction `j` corresponding to node `v` is control-dependent on instruction
115+
`i` corresponding to node `u` if and only if `j` post-dominates at least one
116+
but not all successors instructions of `i`.
117+
118+
An instruction `j` post-dominates an instruction `i` if and only if each
119+
execution path going through `i` eventually reaches `j`.
120+
121+
Post-dominators analysis is implemented in `src/analyses/cfg_dominators.h(cpp)`.
122+
123+
#### Data dependency
124+
125+
The instruction `j` corresponding to node `v` is data-dependent on the
126+
instruction `i` corresponding to node `u` if and only if `j` may read data from
127+
memory location defined (i.e. written) by `i`.
128+
129+
Reaching definitions analysis together with read-write ranges analysis are used
130+
to check whether one instruction may read data writen by another instruction.
131+
For more details see `src/analyses/reaching_definitions.h(cpp)` and
132+
`src/analyses/goto_rw.h(cpp)`.
133+
134+
#### Construction
135+
136+
The dependence graph extends the standard abstract interpreter class `ait`
137+
with post-dominators analysis and reaching definitions analysis. The domain of
138+
the abstract interpreter is defined in the class `dep_graph_domaint`.
139+
140+
For each instruction `i` there is created an instance of `dep_graph_domaint`
141+
associated with `i`. The instance stores a set `control_deps` of program
142+
instructions the instruction `i` depends on via control-dependency, and a set
143+
`data_deps` of program instructions the instruction `i` depends on via
144+
data-dependency. These sets are updated (increased) during the computation,
145+
until a fix-point is reached.
146+
147+
The construction of a dependence graph is started by calling its `initialize`
148+
method and then, once a fix-point is reached by the abstract interpreter, the
149+
method `finalize` converts data in the interpreter's domain (i.e. from
150+
`dep_graph_domaint` instances) into edges of the graph. Nodes of the graph are
151+
created during the run of the abstract interpreter; they are linked to the
152+
corresponding program instructions.
96153

97154
\subsection analyses-dirtyt Address-taken lvalue analysis (dirtyt)
98155

src/util/README.md

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -383,3 +383,45 @@ _not_ be extended - but it may be helpful to be aware of where this happens.
383383
These are in the process of being removed - no new output should go
384384
via `std::cout` or `std::cerr`, but should instead use the
385385
\ref messaget and \ref message_handlert infrastructure.
386+
387+
388+
\subsection Graph
389+
### Graph
390+
391+
Implemented in `src/util/graph.h` as `grapht` class. The class natively defines
392+
only a directional graph. However, an undirected graph can be emulated by
393+
inserting for each edge (u, v) also (v, u). A multi-graph is not supported
394+
though, because parallel edges are not allowed between vertices.
395+
396+
#### Data representation
397+
398+
A graph is defined by a template class `grapht<N>`, where the type `N` defines
399+
a node of the graph. The class `grapht` stores the nodes in a vector. A user of
400+
the graph is supposed to access the nodes via their indices in the vector. The
401+
node type `N` must meet these requirements:
402+
- It must be default constructible; the common way how to insert a node to the
403+
graph is to call method `add_node` which pushes a new default-constructed
404+
instance of `N` to the end of the vector and returns its index.
405+
- It must define a type `edget`, representing type of data attached to any edge
406+
of the graph; in case edges should not have any data attached, then one can
407+
use a predefined class `empty_edget`. The type must be default-constructible.
408+
- It must define a type `edgets` as an associative container compatible with the
409+
type `std::map<std::size_t, edget>`.
410+
- It must define publicly accessible members of the type `edgest`, named `in`
411+
and `out`. The members represent edges in the graph. Namely, if `u` is an
412+
index of some node in the graph and `v` is a key in the map `in` (resp. `out`)
413+
of that node, then `(v, u)` (resp. `(u, v)`) represent an edge in the graph,
414+
with attached data `in[v]` (resp. `out[v]`).
415+
- It must define methods `add_in`, `erase_in`, and `add_out`, `erase_out` for
416+
insertion and removal of values to and from the maps `in` and `out`.
417+
- It must define a method `pretty` converting the node to a "pretty" string.
418+
419+
One can use a predefined template class `graph_nodet<E>` as the template
420+
parameter `N` of the graph.
421+
422+
#### Graph algorithms
423+
424+
The graph implementation comes with several graph algorithms. We describe each
425+
of them in following paragraphs.
426+
427+
TODO!

0 commit comments

Comments
 (0)