Merge pull request #6046 from jezhiggins/vsd-widening-in-merge

Vsd - widening during abstract object merge

Author: martin-cs

regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc

@@ -4,5 +4,5 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^main::1::1::i .* \[5, 5\] @ \[6\]
-^main::1::p .* \[2, 20\] @ \[5\]
+^main::1::p .* \[2, 1F9\] @ \[5\]
 --

regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc

@@ -4,5 +4,5 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[6\]
-^main::1::p .* value-set-begin: 2, 17, 32 :value-set-end @ \[5\]
+^main::1::p .* value-set-begin: 2, \[11, 21\], \[20, 1F9\] :value-set-end @ \[5\]
 --

…zer/value-set-convert-to-interval/main.c …oto-analyzer/value-set-compact-01/main.cregression/goto-analyzer/value-set-convert-to-interval/main.c renamed to regression/goto-analyzer/value-set-compact-01/main.c regression/goto-analyzer/value-set-convert-to-interval/main.c renamed to regression/goto-analyzer/value-set-compact-01/main.c

@@ -5,5 +5,5 @@ main.c
 ^SIGNAL=0$
 main::1::a .* value-set-begin: 0, 1, 2, 3, 4, 5, 6 :value-set-end @ \[1, 12, 15, 18, 21, 24, 26\]
 main::1::b .* value-set-begin: 20, 21, 22, 23, 24 :value-set-end @ \[3, 13, 16, 19, 22\]
-main::1::c .* \[14, 1E\] @ \[30\]
+main::1::c .* value-set-begin: 24, 25, 26, \[14, 17\], \[1B, 1E\] :value-set-end @ \[30\]
 --

…/value-set-convert-to-interval/test.desc …-analyzer/value-set-compact-01/test.descregression/goto-analyzer/value-set-convert-to-interval/test.desc renamed to regression/goto-analyzer/value-set-compact-01/test.desc regression/goto-analyzer/value-set-convert-to-interval/test.desc renamed to regression/goto-analyzer/value-set-compact-01/test.desc

@@ -0,0 +1,49 @@
+#include <stdbool.h>
+
+extern int x;
+
+int main(void)
+{
+  int a[1] = {0};
+  switch(x)
+  {
+  case 1:
+    a[0] = 1;
+    break;
+  case 2:
+    a[0] = 2;
+    break;
+  case 3:
+    a[0] = 3;
+    break;
+  case 4:
+    a[0] = 4;
+    break;
+  case 5:
+    a[0] = 5;
+    break;
+  case 6:
+    a[0] = 6;
+    break;
+  case 7:
+    a[0] = 7;
+    break;
+  case 8:
+    a[0] = 8;
+    break;
+  case 9:
+    a[0] = 9;
+    break;
+  case 10:
+    a[0] = 10;
+    break;
+  case 11:
+    a[0] = 11;
+    break;
+  case 12:
+    a[0] = 12;
+    break;
+  }
+
+  return 0;
+}

regression/goto-analyzer/value-set-compact-02/main.c

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::a .* value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\]
+--

regression/goto-analyzer/value-set-compact-02/test.desc

@@ -0,0 +1,55 @@
+#include <stdbool.h>
+
+extern int x;
+
+struct S
+{
+  int a;
+};
+
+int main(void)
+{
+  struct S a;
+  a.a = 0;
+  switch(x)
+  {
+  case 1:
+    a.a = 1;
+    break;
+  case 2:
+    a.a = 2;
+    break;
+  case 3:
+    a.a = 3;
+    break;
+  case 4:
+    a.a = 4;
+    break;
+  case 5:
+    a.a = 5;
+    break;
+  case 6:
+    a.a = 6;
+    break;
+  case 7:
+    a.a = 7;
+    break;
+  case 8:
+    a.a = 8;
+    break;
+  case 9:
+    a.a = 9;
+    break;
+  case 10:
+    a.a = 10;
+    break;
+  case 11:
+    a.a = 11;
+    break;
+  case 12:
+    a.a = 12;
+    break;
+  }
+
+  return 0;
+}

regression/goto-analyzer/value-set-compact-03/main.c

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::a .* \{.a=value-set-begin: 4, 5, 6, 11, 12, \[0, 3\], \[7, A\] :value-set-end @ \[1, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 36, 38\]\} .*
+--

regression/goto-analyzer/value-set-compact-03/test.desc

@@ -47,7 +47,6 @@ SRC = ai.cpp \
       variable-sensitivity/interval_abstract_value.cpp \
       variable-sensitivity/three_way_merge_abstract_interpreter.cpp \
       variable-sensitivity/value_set_abstract_object.cpp \
-      variable-sensitivity/value_set_abstract_value.cpp \
       variable-sensitivity/value_set_pointer_abstract_object.cpp \
       variable-sensitivity/variable_sensitivity_configuration.cpp \
       variable-sensitivity/variable_sensitivity_dependence_graph.cpp \

src/analyses/Makefile

@@ -127,7 +127,8 @@ class abstract_aggregate_objectt : public abstract_objectt,
   static bool merge_shared_maps(
     const sharing_mapt<keyt, abstract_object_pointert, false, hash> &map1,
     const sharing_mapt<keyt, abstract_object_pointert, false, hash> &map2,
-    sharing_mapt<keyt, abstract_object_pointert, false, hash> &out_map)
+    sharing_mapt<keyt, abstract_object_pointert, false, hash> &out_map,
+    const widen_modet &widen_mode)
   {
     bool modified = false;
 
@@ -137,13 +138,12 @@ class abstract_aggregate_objectt : public abstract_objectt,
 
     for(auto &item : delta_view)
     {
-      bool changes = false;
-      abstract_object_pointert v_new =
-        abstract_objectt::merge(item.m, item.get_other_map_value(), changes);
-      if(changes)
+      auto v_new =
+        abstract_objectt::merge(item.m, item.get_other_map_value(), widen_mode);
+      if(v_new.modified)
       {
         modified = true;
-        out_map.replace(item.k, v_new);
+        out_map.replace(item.k, v_new.object);
       }
     }