Make dependence graph merge() return true when abstract state changes

The dependency graph has special handling for function entry edges (in
transform()) where it merges the current state into the state of the return
location before entering the function. This may change the abstract state at the
return location. When later the function exit edge is handled, the merge() into
the return location may not change the state, thus merge() may not return true,
and thus the return location may not be inserted into the worklist of the
fixpoint computation when it should.

We introduce a flag has_changed that records whether the abstract state has
changed on the handling of the function entry edge. On the function return edge
later, merge() checks the flag to know whether it needs to return true.

Author: danpoe

src/analyses/dependence_graph.cpp

@@ -27,18 +27,27 @@ bool dep_graph_domaint::merge(
   goto_programt::const_targett from,
   goto_programt::const_targett to)
 {
-  bool changed = false;
-
-  if(is_bottom())
+  // An abstract state at location `to` may be non-bottom even if
+  // `merge(..., `to`) has not been called so far. This is due to the special
+  // handling of function entry edges (see transform()).
+  bool changed = is_bottom() || has_changed;
+
+  // For computing the data dependencies, we would not need a fixpoint
+  // computation. The data dependencies at a location are computed from the
+  // result of the reaching definitions analysis at that location
+  // (in data_dependencies()). Thus, we only need to set the data dependencies
+  // part of an abstract state at a certain location once.
+  if(changed && data_deps.empty())
   {
-    has_values = tvt::unknown();
     data_deps = src.data_deps;
-    changed = true;
+    has_values = tvt::unknown();
   }
 
   changed |= util_set_union(control_deps, src.control_deps);
   changed |= util_set_union(control_dep_candidates, src.control_dep_candidates);
 
+  has_changed = false;
+
   return changed;
 }
 
@@ -205,8 +214,15 @@ void dep_graph_domaint::transform(
         dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));
       assert(s!=nullptr);
 
-      util_set_union(s->control_deps, control_deps);
-      util_set_union(s->control_dep_candidates, control_dep_candidates);
+      if(s->is_bottom())
+      {
+        s->has_values = tvt::unknown();
+        s->has_changed = true;
+      }
+
+      s->has_changed |= util_set_union(s->control_deps, control_deps);
+      s->has_changed |=
+        util_set_union(s->control_dep_candidates, control_dep_candidates);
 
       control_deps.clear();
       control_dep_candidates.clear();

src/analyses/dependence_graph.h

@@ -68,9 +68,10 @@ class dep_graph_domaint:public ai_domain_baset
 public:
   typedef grapht<dep_nodet>::node_indext node_indext;
 
-  dep_graph_domaint():
-    has_values(false),
-    node_id(std::numeric_limits<node_indext>::max())
+  dep_graph_domaint()
+    : has_values(false),
+      node_id(std::numeric_limits<node_indext>::max()),
+      has_changed(false)
   {
   }
 
@@ -101,6 +102,7 @@ class dep_graph_domaint:public ai_domain_baset
 
     has_values=tvt(true);
     control_deps.clear();
+    control_dep_candidates.clear();
     data_deps.clear();
   }
 
@@ -111,22 +113,36 @@ class dep_graph_domaint:public ai_domain_baset
 
     has_values=tvt(false);
     control_deps.clear();
+    control_dep_candidates.clear();
     data_deps.clear();
+
+    has_changed = false;
   }
 
   void make_entry() final override
   {
-    make_top();
+    DATA_INVARIANT(
+      node_id != std::numeric_limits<node_indext>::max(),
+      "node_id must not be valid");
+
+    has_values = tvt::unknown();
+    control_deps.clear();
+    control_dep_candidates.clear();
+    data_deps.clear();
+
+    has_changed = false;
   }
 
   bool is_top() const final override
   {
     DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
                    "node_id must be valid");
 
-    DATA_INVARIANT(!has_values.is_true() ||
-                   (control_deps.empty() && data_deps.empty()),
-                   "If the domain is top, it must have no dependencies");
+    DATA_INVARIANT(
+      !has_values.is_true() ||
+        (control_deps.empty() && control_dep_candidates.empty() &&
+         data_deps.empty()),
+      "If the domain is top, it must have no dependencies");
 
     return has_values.is_true();
   }
@@ -136,9 +152,11 @@ class dep_graph_domaint:public ai_domain_baset
     DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
                    "node_id must be valid");
 
-    DATA_INVARIANT(!has_values.is_false() ||
-                   (control_deps.empty() && data_deps.empty()),
-                   "If the domain is bottom, it must have no dependencies");
+    DATA_INVARIANT(
+      !has_values.is_false() ||
+        (control_deps.empty() && control_dep_candidates.empty() &&
+         data_deps.empty()),
+      "If the domain is bottom, it must have no dependencies");
 
     return has_values.is_false();
   }
@@ -160,6 +178,7 @@ class dep_graph_domaint:public ai_domain_baset
 private:
   tvt has_values;
   node_indext node_id;
+  bool has_changed;
 
   typedef std::set<goto_programt::const_targett> depst;