Vsd - widening during abstract object merge

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\]
 --

regression/goto-analyzer/value-set-convert-to-interval/test.desc → regression/goto-analyzer/value-set-compact-01/test.desc

@@ -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\]
 --

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

@@ -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/test.desc

@@ -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-03/main.c

@@ -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/test.desc

@@ -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\]\} .*
+--

src/analyses/Makefile

@@ -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/variable-sensitivity/abstract_aggregate_object.h

@@ -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);
       }
     }
 

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -312,38 +312,33 @@ abstract_object_pointert abstract_environmentt::add_object_context(
   return object_factory->wrap_with_context(abstract_object);
 }
 
-bool abstract_environmentt::merge(const abstract_environmentt &env)
+bool abstract_environmentt::merge(
+  const abstract_environmentt &env,
+  widen_modet widen_mode)
 {
   // for each entry in the incoming environment we need to either add it
   // if it is new, or merge with the existing key if it is not present
-
   if(bottom)
   {
     *this = env;
     return !env.bottom;
   }
-  else if(env.bottom)
-  {
+
+  if(env.bottom)
     return false;
-  }
-  else
-  {
-    // For each element in the intersection of map and env.map merge
-    // If the result of the merge is top, remove from the map
-    bool modified = false;
-    decltype(env.map)::delta_viewt delta_view;
-    env.map.get_delta_view(map, delta_view);
-    for(const auto &entry : delta_view)
-    {
-      bool object_modified = false;
-      abstract_object_pointert new_object = abstract_objectt::merge(
-        entry.get_other_map_value(), entry.m, object_modified);
-      modified |= object_modified;
-      map.replace(entry.k, new_object);
-    }
 
-    return modified;
+  // For each element in the intersection of map and env.map merge
+  // If the result of the merge is top, remove from the map
+  bool modified = false;
+  for(const auto &entry : env.map.get_delta_view(map))
+  {
+    auto merge_result =
+      abstract_objectt::merge(entry.get_other_map_value(), entry.m, widen_mode);
+    modified |= merge_result.modified;
+    map.replace(entry.k, merge_result.object);
   }
+
+  return modified;
 }
 
 void abstract_environmentt::havoc(const std::string &havoc_string)
@@ -508,12 +503,8 @@ std::vector<abstract_object_pointert> eval_operands(
 ///////////
 abstract_value_pointert as_value(const abstract_object_pointert &obj)
 {
-  auto context_value =
-    std::dynamic_pointer_cast<const context_abstract_objectt>(obj);
-
-  return context_value
-           ? as_value(context_value->unwrap_context())
-           : std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
+  return std::dynamic_pointer_cast<const abstract_value_objectt>(
+    obj->unwrap_context());
 }
 
 bool is_value(const abstract_object_pointert &obj)

src/analyses/variable-sensitivity/abstract_environment.h

@@ -25,6 +25,12 @@ class variable_sensitivity_object_factoryt;
 using variable_sensitivity_object_factory_ptrt =
   std::shared_ptr<variable_sensitivity_object_factoryt>;
 
+enum class widen_modet
+{
+  no,
+  could_widen
+};
+
 class abstract_environmentt
 {
 public:
@@ -180,9 +186,10 @@ class abstract_environmentt
   /// Computes the join between "this" and "b"
   ///
   /// \param env: the other environment
+  /// \param widen_mode: indicates if this is a widening merge
   ///
   /// \return A Boolean, true when the merge has changed something
-  virtual bool merge(const abstract_environmentt &env);
+  virtual bool merge(const abstract_environmentt &env, widen_modet widen_mode);
 
   /// This should be used as a default case / everything else has failed
   /// The string is so that I can easily find and diagnose cases where this

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -48,8 +48,9 @@ const typet &abstract_objectt::type() const
   return t;
 }
 
-abstract_object_pointert
-abstract_objectt::merge(const abstract_object_pointert &other) const
+abstract_object_pointert abstract_objectt::merge(
+  const abstract_object_pointert &other,
+  const widen_modet &widen_mode) const
 {
   return abstract_object_merge(other);
 }
@@ -182,26 +183,16 @@ void abstract_objectt::output(
   }
 }
 
-abstract_object_pointert abstract_objectt::merge(
+abstract_objectt::combine_result abstract_objectt::merge(
   const abstract_object_pointert &op1,
   const abstract_object_pointert &op2,
-  bool &out_modifications)
+  const widen_modet &widen_mode)
 {
   abstract_object_pointert result = op1->should_use_base_merge(op2)
                                       ? op1->abstract_object_merge(op2)
-                                      : op1->merge(op2);
+                                      : op1->merge(op2, widen_mode);
   // If no modifications, we will return the original pointer
-  out_modifications = result != op1;
-
-  return result;
-}
-
-abstract_object_pointert abstract_objectt::merge(
-  const abstract_object_pointert &op1,
-  const abstract_object_pointert &op2)
-{
-  bool dummy;
-  return merge(op1, op2, dummy);
+  return {result, result != op1};
 }
 
 bool abstract_objectt::should_use_base_merge(
@@ -210,18 +201,15 @@ bool abstract_objectt::should_use_base_merge(
   return is_top() || other->is_bottom() || other->is_top();
 }
 
-abstract_object_pointert abstract_objectt::meet(
+abstract_objectt::combine_result abstract_objectt::meet(
   const abstract_object_pointert &op1,
-  const abstract_object_pointert &op2,
-  bool &out_modifications)
+  const abstract_object_pointert &op2)
 {
   abstract_object_pointert result = op1->should_use_base_meet(op2)
                                       ? op1->abstract_object_meet(op2)
                                       : op1->meet(op2);
   // If no modifications, we will return the original pointer
-  out_modifications = result != op1;
-
-  return result;
+  return {result, result != op1};
 }
 
 bool abstract_objectt::should_use_base_meet(