diff --git a/src/analyses/README.md b/src/analyses/README.md index 5bde0b64a42..2b13ddb425c 100644 --- a/src/analyses/README.md +++ b/src/analyses/README.md @@ -92,7 +92,65 @@ To be documented. \subsection analyses-dependence-graph Data- and control-dependence analysis (dependence_grapht) -To be documented. +### Dependence graph + +Implemented in `src/analyses/dependence_graph.h(cpp)`. It is a graph and an +abstract interpreter at the same time. The abstract interpretation nature +allows a dependence graph to [build itself](#Construction) +(the graph) from a given GOTO program. + +A dependence graph extends the class `grapht` with `dep_nodet` as the type of +nodes (see `src/util/graph.h` for more details about +[graph representation]("../util/README.md")). +The `dep_nodet` extends `graph_nodet` with an iterator to a GOTO +program instruction. It means that each graph node corresponds to a particular +program instruction. A labelled edge `(u, v)` of a dependence graph expresses +a dependency of the program instruction corresponding to node `u` on the program +instruction corresponding to node `v`. The label of the edge (data of the +type `dep_edget` attached to the edge) denotes the kind of dependency. It can be +`control-dependency`, `data-dependency`, or both. + +#### Control dependency + +An instruction `j` corresponding to node `v` is control-dependent on instruction +`i` corresponding to node `u` if and only if `j` post-dominates at least one +but not all successors instructions of `i`. + +An instruction `j` post-dominates an instruction `i` if and only if each +execution path going through `i` eventually reaches `j`. + +Post-dominators analysis is implemented in `src/analyses/cfg_dominators.h(cpp)`. + +#### Data dependency + +The instruction `j` corresponding to node `v` is data-dependent on the +instruction `i` corresponding to node `u` if and only if `j` may read data from +the memory location defined (i.e. written) by `i`. + +The reaching definitions analysis is used together with the read-write ranges +analysis to check whether one instruction may read data writen by another +instruction. For more details see `src/analyses/reaching_definitions.h(cpp)` and +`src/analyses/goto_rw.h(cpp)`. + +#### Construction + +The dependence graph extends the standard abstract interpreter class `ait` +with post-dominators analysis and reaching definitions analysis. The domain of +the abstract interpreter is defined in the class `dep_graph_domaint`. + +For each instruction `i` an instance of `dep_graph_domaint` associated with `i` +is created. The instance stores a set `control_deps` of program +instructions the instruction `i` depends on via control-dependency, and a set +`data_deps` of program instructions the instruction `i` depends on via +data-dependency. These sets are updated (increased) during the computation, +until a fix-point is reached. + +The construction of a dependence graph is started by calling its `initialize` +method and then, once a fix-point is reached by the abstract interpreter, the +method `finalize` converts data in the interpreter's domain (i.e. from +`dep_graph_domaint` instances) into edges of the graph. Nodes of the graph are +created during the run of the abstract interpreter; they are linked to the +corresponding program instructions. \subsection analyses-dirtyt Address-taken lvalue analysis (dirtyt) diff --git a/src/util/README.md b/src/util/README.md index 52432e42b42..54054da7505 100644 --- a/src/util/README.md +++ b/src/util/README.md @@ -383,3 +383,48 @@ _not_ be extended - but it may be helpful to be aware of where this happens. These are in the process of being removed - no new output should go via `std::cout` or `std::cerr`, but should instead use the \ref messaget and \ref message_handlert infrastructure. + + +\subsection Graph +### Graph + +Implemented in `src/util/graph.h` as `grapht` class. The `grapht` class +represents a directed graph. However, an undirected graph can be emulated by +inserting for each edge (u, v) also (v, u). A multi-graph is not supported +though, because parallel edges are not allowed between vertices. + +#### Data representation + +A graph is defined by a template class `grapht`, where `N` is the type of the +nodes of the graph. The class `grapht` stores the nodes in a vector. A user of +the graph is supposed to access the nodes via their indices in the vector. The +node type `N` must meet these requirements: +- It must be default constructible; the common way how to insert a node to the + graph is to call method `add_node` which pushes a new default-constructed + instance of `N` to the end of the vector and returns its index. + Then `operator[]` can be used to obtain a reference to the pushed instance and + set its content as desired. +- It must define a type `edget`, representing type of data attached to any edge + of the graph; in case edges should not have any data attached, then one can + use a predefined class `empty_edget`. The type must be default-constructible. +- It must define a type `edgets` as an associative container compatible with the + type `std::map`. +- It must define publicly accessible members of the type `edgest`, named `in` + and `out`. The members represent edges in the graph. Namely, if `u` is an + index of some node in the graph and `v` is a key in the map `in` (resp. `out`) + of that node, then `(v, u)` (resp. `(u, v)`) represent an edge in the graph, + with attached data `in[v]` (resp. `out[v]`). +- It must define methods `add_in`, `erase_in`, and `add_out`, `erase_out` for + insertion and removal of values to and from the maps `in` and `out`. +- It must define a method `pretty` converting the node to a "pretty" string. + +One can use a predefined template class `graph_nodet` as the template +parameter `N` of the graph. The template parameter `E` allows to define the type +`edget`. + +#### Graph algorithms + +The graph implementation comes with several graph algorithms. We describe each +of them in following paragraphs. + +TODO!