Fix reaching definitions merge

Author: danpoe

regression/goto-analyzer/dependence-graph-periodic-task-02/main.c

@@ -0,0 +1,14 @@
+int g_x;
+int g_y;
+
+int x;
+int y;
+
+void main(void)
+{
+  g_x = g_y;
+  x = y;
+
+  g_y = 1;
+  y = 1;
+}

regression/goto-analyzer/dependence-graph-periodic-task-02/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--show --dependence-graph --periodic-task --json -
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+"line": "2",\n.*\n.*\n\s*"task": "first"
+"line": "12",\n.*\n.*\n\s*"task": "later"
+"line": "5",\n.*\n.*\n\s*"task": "first"
+"line": "13",\n.*\n.*\n\s*"task": "later"
+--
+^warning: ignoring
+--

src/analyses/reaching_definitions.cpp

@@ -16,6 +16,7 @@ Author: Michael Tautschnig
 
 #include "reaching_definitions.h"
 
+#include <algorithm>
 #include <memory>
 
 #include <util/pointer_offset_size.h>
@@ -575,51 +576,78 @@ bool rd_range_domaint::merge(
   locationt from,
   locationt to)
 {
-  bool changed=false;
+  bool changed = false;
 
-  if(other.has_values.is_false())
+  if(other.is_bottom())
   {
-    assert(other.values.empty());
     return false;
   }
 
-  if(has_values.is_false())
+  if(is_bottom())
   {
-    assert(values.empty());
-    values=other.values;
-    assert(!other.has_values.is_true());
-    has_values=other.has_values;
+    values = other.values;
+
+    INVARIANT(!other.is_top(), "top unused");
+    has_values = other.has_values;
+
     return true;
   }
-  rd_range_domaint &o=const_cast<rd_range_domaint &>(other);
+
+  rd_range_domaint &o =
+    const_cast<rd_range_domaint &>(other);
   values.swap(o.values);
-  valuest::delta_viewt delta_view;
-  o.values.get_delta_view(values, delta_view);
+
+  {
+    // Needed to set changed
+    typename valuest::delta_viewt delta_view_test;
+    values.get_delta_view(o.values, delta_view_test, false);
+
+    for(const auto &element : delta_view_test)
+    {
+      if(!element.in_both)
+      {
+        changed = true;
+        break;
+      }
+    }
+  }
+
+  typename valuest::delta_viewt delta_view;
+  o.values.get_delta_view(values, delta_view, false);
+
   for(const auto &element : delta_view)
   {
-    bool in_both=element.in_both;
-    const irep_idt &k=element.k;
-    const values_innert &inner_other=element.m; // in other
-    const values_innert &inner=element.other_m; // in this
+    bool in_both = element.in_both;
+    const irep_idt &k = element.k;
+    const values_innert &inner_other = element.m; // in other
+    const values_innert &inner = element.other_m; // in this
 
     if(!in_both)
     {
       values.insert(k, inner_other);
-      changed=true;
     }
     else
     {
-      if(inner!=inner_other)
+      bool inner_is_superset = std::includes(
+        inner.begin(), inner.end(), inner_other.begin(), inner_other.end());
+
+      if(!inner_is_superset)
       {
-        auto &v=values.find(k);
-        assert(v.second);
+        auto &v = values.find(k);
+        INVARIANT(v.second, "key exists as in_both is true");
 
-        values_innert &inner=v.first;
+        values_innert &inner = v.first;
+        const values_innert copy(inner_other);
 
-        size_t n=inner.size();
         inner.insert(inner_other.begin(), inner_other.end());
-        if(inner.size()!=n)
-          changed=true;
+
+        if(inner != copy)
+          changed = true;
+      }
+      else
+      {
+        if(inner != inner_other)
+          changed = true;
       }
     }
   }