Documentation for cfg dominator class

Author: Daniel Poetzl

src/analyses/cfg_dominators.h

@@ -28,6 +28,9 @@ Author: Georg Weissenbacher, [email protected]
 #include <goto-programs/goto_program.h>
 #include <goto-programs/cfg.h>
 
+/// Dominator tree
+/// Node indices are 0-based here (unlike in the internal data structures of
+/// the algorithm).
 template <typename T, typename node_indext>
 struct dominators_datat
 {
@@ -41,13 +44,16 @@ struct dominators_datat
     : data(data), immediate_dominator(immediate_dominator)
   {
   }
+
+  /// Maps node to T
   std::vector<T> data;
+
+  /// Maps node to its immediate dominator
   std::vector<node_indext> immediate_dominator;
 };
 
-/// An immutable set of dominators. Constant memory usage and creation time,
-/// but linear lookup time
-/// Immutability is necessary because the structure uses sharing
+/// An immutable set of dominators. Constant memory usage and creation time.
+/// Immutability is necessary because the structure uses sharing.
 template <typename T, typename node_indext>
 class dominatorst
 {
@@ -62,8 +68,8 @@ class dominatorst
 
 public:
   /// Create an empty set
-  /// Note: Only unreachable nodes should be assigned
-  /// empty sets after the algorithm completes
+  /// Note: Only unreachable nodes should be assigned empty sets after the
+  /// algorithm completes
   dominatorst() : dominators_data(nullptr), node_index(npos), cached_distance(0)
   {
   }
@@ -180,26 +186,23 @@ class dominatorst
   /// Return an iterator node if node is in this dominators set, end() otherwise
   /// Note: O(n), when making many queries against the same set it is probably
   /// worth copying into a std::set
-
   const_iterator find(const T &node) const
   {
     std::less<T> less;
-    // FIXME This works around a bug in other parts of the code
-    // in particular, dependence_graph.cpp,
-    // where iterators to different lists than those that are
-    // stored in this set are passed to find.
-    // The Debug libstdc++ will (correctly!) run into an assertion failure
-    // using std::find. std::less for some reason doesn't trigger this assertion
-    // failure, so we use this as an ugly workaround until that code is fixed.
+    // FIXME This works around a bug in other parts of the code in particular,
+    // dependence_graph.cpp, where iterators to different lists than those that
+    // are stored in this set are passed to find. The Debug libstdc++ will
+    // (correctly!) run into an assertion failure using std::find. std::less for
+    // some reason doesn't trigger this assertion failure, so we use this as an
+    // ugly workaround until that code is fixed.
 
     // NOLINTNEXTLINE
     return std::find_if(cbegin(), cend(), [&](const T &other_node) {
       return !less(node, other_node) && !less(other_node, node);
     });
   }
 
-  /// The size of the set; Linear time on the first call,
-  /// constant after that
+  /// The size of the set. Linear time on the first call, constant after that.
   std::size_t size() const
   {
     if(cached_distance == npos)
@@ -219,6 +222,7 @@ template <typename T, typename node_indext>
 const node_indext
   dominatorst<T, node_indext>::npos = std::numeric_limits<node_indext>::max();
 
+/// Dominators for each instruction in a goto program
 template <class P, class T, bool post_dom>
 class cfg_dominators_templatet
 {
@@ -248,15 +252,17 @@ class cfg_dominators_templatet
     explicit fixedpointt(cfg_dominators_templatet &cfg_dominators)
       : cfg_dominators(cfg_dominators),
         dfs_counter(0),
+        // Data structures have size cfg.size() + 1 as node indices are 1-based
+        // to match the paper of Lengauer/Tarjan.
         parent(cfg_dominators.cfg.size() + 1),
-        ancestor(cfg_dominators.cfg.size() + 1),
-        child(cfg_dominators.cfg.size() + 1),
         vertex(cfg_dominators.cfg.size() + 1),
         dom(cfg_dominators.cfg.size() + 1),
-        label(cfg_dominators.cfg.size() + 1),
         semi(cfg_dominators.cfg.size() + 1),
+        bucket(cfg_dominators.cfg.size() + 1),
+        ancestor(cfg_dominators.cfg.size() + 1),
+        label(cfg_dominators.cfg.size() + 1),
         size(cfg_dominators.cfg.size() + 1),
-        bucket(cfg_dominators.cfg.size() + 1)
+        child(cfg_dominators.cfg.size() + 1)
     {
     }
 
@@ -265,12 +271,34 @@ class cfg_dominators_templatet
   private:
     cfg_dominators_templatet &cfg_dominators;
     node_indext dfs_counter;
-    std::vector<node_indext> parent, ancestor, child, vertex, dom;
 
-    std::vector<node_indext> label, semi, size;
+    /// Maps node to its parent in the DFS-generated spanning tree
+    std::vector<node_indext> parent;
+
+    /// Maps number to node (according to the DFS numbering)
+    std::vector<node_indext> vertex;
+
+    /// Maps node to its immediate dominator
+    std::vector<node_indext> dom;
 
+    /// Maps node to its semi-dominator (as defined by Lengauer/Tarjan)
+    /// A semidominator of a node w is the minimum node v (according to the DFS
+    /// numbering) for which there is a path from v to w such that all nodes
+    /// occuring on that path (other than v, w) have a larger number than w
+    /// (according to the DFS numbering)
+    std::vector<node_indext> semi;
+
+    /// Maps node to the set of nodes of which it is the semi-dominator
     std::vector<std::set<node_indext>> bucket;
 
+    // Used by link() and eval(), which are used to create and query
+    // an auxiliary data structure which is a forest that is contained
+    // in the DFS spanning tree.
+    std::vector<node_indext> ancestor;
+    std::vector<node_indext> label;
+    std::vector<node_indext> size;
+    std::vector<node_indext> child;
+
     T get_entry_node(P &program)
     {
       if(post_dom)
@@ -283,6 +311,9 @@ class cfg_dominators_templatet
       }
     };
 
+    /// DFS numbering
+    /// Number nodes in the order in which they are reached during a DFS,
+    /// intialize data structures
     void dfs(node_indext root)
     {
       struct dfs_statet
@@ -299,16 +330,20 @@ class cfg_dominators_templatet
         node_indext v = state.current;
         if(semi[v] == 0)
         {
+          // Initialize data structures
           parent[v] = state.parent;
           semi[v] = ++dfs_counter;
           vertex[dfs_counter] = label[v] = v;
           ancestor[v] = child[v] = 0;
           size[v] = 1;
+          // Explore children
           for_each_successor(v, [&](node_indext w) { work.push({v, w}); });
         }
       }
     }
 
+    /// Compress path from v to the root in the tree of the forest that contains
+    /// v, by directly attaching nodes to the root
     void compress(node_indext v)
     {
       if(ancestor[ancestor[v]] != 0)
@@ -322,6 +357,8 @@ class cfg_dominators_templatet
       }
     }
 
+    /// Return node with minimum semidominator on the path from the root of the
+    /// tree in the forest containing v to v, and compress path
     node_indext eval(node_indext v)
     {
       if(ancestor[v] == 0)
@@ -336,6 +373,9 @@ class cfg_dominators_templatet
       return label[ancestor[v]];
     }
 
+    /// Add an edge to the forest
+    /// \param v: source node of edge
+    /// \param w: target node of edge
     void link(node_indext v, node_indext w)
     {
       node_indext s = w;
@@ -365,15 +405,19 @@ class cfg_dominators_templatet
       }
     }
 
+    /// Fill output data structures
     void assign_dominators(node_indext root)
     {
+      // Fill dominator tree output data structure
       auto dominators_data = std::make_shared<typename target_sett::datat>(
         cfg_dominators.cfg.size());
       for(node_indext i = 0; i < cfg_dominators.cfg.size(); ++i)
       {
         dominators_data->immediate_dominator[i] = dom[i + 1] - 1;
         dominators_data->data[i] = cfg_dominators.cfg[i].PC;
       }
+
+      // Assign immediate dominator to nodes in the cfg
       std::stack<node_indext> work;
       work.push(root);
       while(!work.empty())
@@ -389,10 +433,11 @@ class cfg_dominators_templatet
       }
     }
 
+    /// Perform action on each child node
     template <typename Action>
     void for_each_successor(node_indext node_index, Action action)
     {
-      // the -1 / +1 adjusts indices from 1 based to 0 based and back
+      // The -1 / +1 adjusts indices from 1 based to 0 based and back
       auto ix = node_index - 1;
       for(auto const &next :
           post_dom ? cfg_dominators.cfg.in(ix) : cfg_dominators.cfg.out(ix))
@@ -401,6 +446,7 @@ class cfg_dominators_templatet
       }
     }
 
+    /// Perform action on each parent node
     template <typename Action>
     void for_each_predecessor(node_indext node_index, Action action)
     {
@@ -414,38 +460,53 @@ class cfg_dominators_templatet
   };
 };
 
+/// Dominator tree computation
+/// Follows "A fast algorithm for finding dominators in a flow graph" of
+/// Lengauer and Tarjan. Node indices are 1-based as in the paper, with the
+/// first element (with index 0) of each data structure simply left empty.
 template <class P, class T, bool post_dom>
 void cfg_dominators_templatet<P, T, post_dom>::fixedpointt::fixedpoint(
   P &program)
 {
-  // Dominator Tree according to Lengauer and Tarjan
-  // "A fast algorithm for finding dominators in a flow graph"
-  // This is ununderstandable without reading the paper!
-  // assumption: Vertex indices >= 0 and < cfg.size()
+  // The nodes in the cfg data structure are represented by indices >= 0 and <
+  // cfg.size(), whereas the internal data structures of the algorithm use
+  // 1-based indices to represent nodes
   if(cfg_dominators.cfg.nodes_empty(program))
   {
     return;
   }
   cfg_dominators.entry_node = get_entry_node(program);
   node_indext root =
     cfg_dominators.cfg.entry_map[cfg_dominators.entry_node] + 1;
+
+  // The computation is carried out in four steps as given in the paper.
+
+  // Step 1
+  // Number nodes in the order in which they are reached during DFS, and
+  // initialize data structures
   dfs_counter = 0;
   dfs(root);
+
   for(node_indext i = dfs_counter; i >= 2; --i)
   {
+    // Step 2
+    // Compute semidominators
     node_indext w = vertex[i];
     // NOLINTNEXTLINE
     for_each_predecessor(w, [&](node_indext v) {
       node_indext u = eval(v);
-      // reachable nodes may have unreachable
-      // nodes as their parents
+      // Reachable nodes may have unreachable nodes as their parents
       if(semi[u] != 0 && semi[u] < semi[w])
       {
         semi[w] = semi[u];
       }
     });
+
     bucket[vertex[semi[w]]].insert(w);
     link(parent[w], w);
+
+    // Step 3
+    // Implicitely define immediate dominator
     auto &w_parent_bucket = bucket[parent[w]];
     for(auto v_it = begin(w_parent_bucket); v_it != end(w_parent_bucket);)
     {
@@ -462,6 +523,9 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpointt::fixedpoint(
       }
     }
   }
+
+  // Step 4
+  // Compute immediate dominator
   for(node_indext i = 2; i <= dfs_counter; ++i)
   {
     node_indext w = vertex[i];
@@ -471,10 +535,14 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpointt::fixedpoint(
     }
   }
 
+  // Fill output data structures
   assign_dominators(root);
 }
 
 /// Print the result of the dominator computation
+/// \param out: output stream
+/// \param cfg_dominators: structure containing the result of the dominator
+///   computation
 template <class P, class T, bool post_dom>
 std::ostream &operator<<(
   std::ostream &out,
@@ -500,23 +568,40 @@ void cfg_dominators_templatet<P, T, post_dom>::initialise(P &program)
   cfg(program);
 }
 
-/// Pretty-print a single node in the dominator tree. Supply a specialisation if
-/// operator<< is not sufficient.
-/// \par parameters: `node` to print and stream `out` to pretty-print it to
+/// Pretty-print a single node. Supply a specialisation if operator<< is not
+/// sufficient.
+/// \param node: node to print
+/// \param out: output stream
 template <class T>
 void dominators_pretty_print_node(const T &node, std::ostream &out)
 {
   out << node;
 }
 
+/// Pretty-print a single node.
+/// \param node: node to print
+/// \param out: output stream
+template <>
 inline void dominators_pretty_print_node(
   const goto_programt::targett &target,
   std::ostream &out)
 {
   out << target->code.pretty();
 }
 
+/// Pretty-print a single node.
+/// \param node: node to print
+/// \param out: output stream
+template <>
+inline void dominators_pretty_print_node(
+  const goto_programt::const_targett &node,
+  std::ostream &out)
+{
+  out << node->location_number;
+}
+
 /// Print the result of the dominator computation
+/// \param out: output stream
 template <class P, class T, bool post_dom>
 void cfg_dominators_templatet<P, T, post_dom>::output(std::ostream &out) const
 {
@@ -551,12 +636,4 @@ typedef cfg_dominators_templatet<const goto_programt,
                                  true>
   cfg_post_dominatorst;
 
-template <>
-inline void dominators_pretty_print_node(
-  const goto_programt::const_targett &node,
-  std::ostream &out)
-{
-  out << node->location_number;
-}
-
 #endif // CPROVER_ANALYSES_CFG_DOMINATORS_H