Fix issue where merge() did not return true in the dependence graph when the

abstract state changed

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,19 +27,20 @@ bool dep_graph_domaint::merge(
   goto_programt::const_targett from,
   goto_programt::const_targett to)
 {
-  bool changed = false;
+  bool changed = is_bottom() || has_changed;
 
-  if(is_bottom())
+  if(is_bottom() || (has_changed && data_deps.empty()))
   {
-    has_values = tvt::unknown();
     data_deps = src.data_deps;
-    changed = true;
+    has_values = tvt::unknown();
   }
 
   changed |= union_ordered_range(control_deps, src.control_deps);
   changed |=
     union_ordered_range(control_dep_candidates, src.control_dep_candidates);
 
+  has_changed = false;
+
   return changed;
 }
 
@@ -206,8 +207,15 @@ void dep_graph_domaint::transform(
         dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));
       assert(s!=nullptr);
 
-      union_ordered_range(s->control_deps, control_deps);
-      union_ordered_range(s->control_dep_candidates, control_dep_candidates);
+      if(s->is_bottom())
+      {
+        s->has_values = tvt::unknown();
+        s->has_changed = true;
+      }
+
+      s->has_changed |= union_ordered_range(s->control_deps, control_deps);
+      s->has_changed |=
+        union_ordered_range(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;
   depst control_deps;