When widening value-sets, only do a limited compact

Only collapse constants or intervals which overlap the extended upper or
lower bound. Don't perform a general compact, unless the set has become
large.

Author: jezhiggins

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, \[11, 1F9\] :value-set-end @ \[5\]
+^main::1::p .* value-set-begin: 2, \[11, 21\], \[20, 1F9\] :value-set-end @ \[5\]
 --

scripts/expected_doxygen_warnings.txt

@@ -1,6 +1,6 @@
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (93), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'arith_tools.h' not generated, too many nodes (167), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (168), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (128), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'invariant.h' not generated, too many nodes (172), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -9,12 +9,14 @@
 /// \file
 /// Value Set Abstract Object
 
-#include "interval_abstract_value.h"
 #include <analyses/variable-sensitivity/constant_abstract_value.h>
 #include <analyses/variable-sensitivity/context_abstract_object.h>
+#include <analyses/variable-sensitivity/interval_abstract_value.h>
 #include <analyses/variable-sensitivity/value_set_abstract_object.h>
 
+#include <util/arith_tools.h>
 #include <util/make_unique.h>
+#include <util/simplify_expr.h>
 
 #include "abstract_environment.h"
 
@@ -114,9 +116,8 @@ maybe_extract_single_value(const abstract_object_pointert &maybe_singleton);
 static bool are_any_top(const abstract_object_sett &set);
 
 static abstract_object_sett compact_values(const abstract_object_sett &values);
-static abstract_object_sett
-non_destructive_compact(const abstract_object_sett &values);
 static abstract_object_sett widen_value_set(
+  const abstract_object_sett &values,
   const constant_interval_exprt &lhs,
   const constant_interval_exprt &rhs);
 
@@ -227,8 +228,8 @@ abstract_object_pointert value_set_abstract_objectt::merge_with_value(
     widen_mode == widen_modet::could_widen && has_values(shared_from_this()) &&
     has_values(other))
   {
-    union_values.insert(widen_value_set(to_interval(), other->to_interval()));
-    union_values = non_destructive_compact(union_values);
+    union_values =
+      widen_value_set(union_values, to_interval(), other->to_interval());
   }
 
   return resolve_values(union_values);
@@ -389,6 +390,9 @@ static abstract_object_sett compact_values(const abstract_object_sett &values)
 
 static exprt eval_expr(const exprt &e);
 static bool is_le(const exprt &lhs, const exprt &rhs);
+static abstract_object_sett collapse_values_in_intervals(
+  const abstract_object_sett &values,
+  const std::vector<constant_interval_exprt> &intervals);
 static void
 collapse_overlapping_intervals(std::vector<constant_interval_exprt> &intervals);
 
@@ -447,24 +451,31 @@ non_destructive_compact(const abstract_object_sett &values)
   if(intervals.empty())
     return values;
 
-  auto compacted = abstract_object_sett{};
+  return collapse_values_in_intervals(values, intervals);
+}
+
+static abstract_object_sett collapse_values_in_intervals(
+  const abstract_object_sett &values,
+  const std::vector<constant_interval_exprt> &intervals)
+{
+  auto collapsed = abstract_object_sett{};
   // for each value, including the intervals
   // keep it if it is not in any of the intervals
   std::copy_if(
     values.begin(),
     values.end(),
-    std::back_inserter(compacted),
+    std::back_inserter(collapsed),
     [&intervals](const abstract_object_pointert &object) {
       return value_is_not_contained_in(object, intervals);
     });
   std::transform(
     intervals.begin(),
     intervals.end(),
-    std::back_inserter(compacted),
+    std::back_inserter(collapsed),
     [](const constant_interval_exprt &interval) {
       return interval_abstract_valuet::make_interval(interval);
     });
-  return compacted;
+  return collapsed;
 }
 
 static abstract_object_sett
@@ -527,13 +538,14 @@ static bool is_le(const exprt &lhs, const exprt &rhs)
 }
 
 static abstract_object_sett widen_value_set(
+  const abstract_object_sett &values,
   const constant_interval_exprt &lhs,
   const constant_interval_exprt &rhs)
 {
-  auto widened_ends = abstract_object_sett{};
-
   if(lhs.contains(rhs))
-    return widened_ends;
+    return values;
+
+  auto widened_ends = std::vector<constant_interval_exprt>{};
 
   auto lower_bound =
     constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower());
@@ -548,19 +560,32 @@ static abstract_object_sett widen_value_set(
   // should extend lower bound?
   if(rhs.get_lower() < lhs.get_lower())
   {
-    auto widened_lower_bound =
-      simplify_expr(minus_exprt(lower_bound, range), ns);
-    widened_ends.insert(interval_abstract_valuet::make_interval(
-      constant_interval_exprt(widened_lower_bound, lower_bound)));
+    auto widened_lower_bound = constant_interval_exprt(
+      simplify_expr(minus_exprt(lower_bound, range), ns), lower_bound);
+    widened_ends.push_back(widened_lower_bound);
+    for(auto &obj : values)
+    {
+      auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
+      auto as_expr = value->to_interval();
+      if(is_le(as_expr.get_lower(), lower_bound))
+        widened_ends.push_back(as_expr);
+    }
   }
   // should extend upper bound?
   if(lhs.get_upper() < rhs.get_upper())
   {
-    auto widened_upper_bound =
-      simplify_expr(plus_exprt(upper_bound, range), ns);
-    widened_ends.insert(interval_abstract_valuet::make_interval(
-      constant_interval_exprt(upper_bound, widened_upper_bound)));
+    auto widened_upper_bound = constant_interval_exprt(
+      upper_bound, simplify_expr(plus_exprt(upper_bound, range), ns));
+    widened_ends.push_back(widened_upper_bound);
+    for(auto &obj : values)
+    {
+      auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
+      auto as_expr = value->to_interval();
+      if(is_le(upper_bound, as_expr.get_upper()))
+        widened_ends.push_back(as_expr);
+    }
   }
 
-  return widened_ends;
+  collapse_overlapping_intervals(widened_ends);
+  return collapse_values_in_intervals(values, widened_ends);
 }

unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp

@@ -251,19 +251,67 @@ SCENARIO(
         EXPECT_MODIFIED(merged, {interval_4minus_1, val2, val4, val4});
       }
     }
-    /*
-    WHEN("merging [2, 3] with [1, 5]")
+    WHEN("merging {[1, 3]} with {2, 4}")
+    {
+      auto interval_1_3 = constant_interval_exprt(val1, val3);
+      auto op1 = make_value_set(interval_1_3, environment, ns);
+      auto op2 = make_value_set({val2, val4}, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("widen upper-bound, {[1, 3], 2 [4, 8]}")
+      {
+        auto interval_4_8 = constant_interval_exprt(val4, val8);
+        EXPECT_MODIFIED(merged, {interval_1_3, val2, interval_4_8});
+      }
+    }
+    WHEN("merging {[1, 3]} with {[2, 4]}")
+    {
+      auto interval_1_3 = constant_interval_exprt(val1, val3);
+      auto interval_2_4 = constant_interval_exprt(val2, val4);
+      auto op1 = make_value_set(interval_1_3, environment, ns);
+      auto op2 = make_value_set(interval_2_4, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("widen upper-bound, {[1, 3], [2, 8]}")
+      {
+        auto interval_2_8 = constant_interval_exprt(val2, val8);
+        EXPECT_MODIFIED(merged, {interval_1_3, interval_2_8});
+      }
+    }
+    WHEN("merging {[2, 4]} with {1, 3}")
+    {
+      auto interval_2_4 = constant_interval_exprt(val2, val4);
+      auto op1 = make_value_set(interval_2_4, environment, ns);
+      auto op2 = make_value_set({val1, val3}, environment, ns);
+
+      auto merged = widening_merge(op1, op2);
+
+      THEN("widen lower bound - {[-3, 1], 3, [2, 4]}")
+      {
+        auto interval_3minus_1 =
+          constant_interval_exprt(from_integer(-3, type), val1);
+        EXPECT_MODIFIED(merged, {interval_2_4, val3, interval_3minus_1});
+      }
+    }
+    WHEN("merging {[2, 4]} with {[1, 3]}")
     {
-      auto op1 = make_value_set(val2, val3, environment, ns);
-      auto op2 = make_value_set(val1, val5, environment, ns);
+      auto interval_2_4 = constant_interval_exprt(val2, val4);
+      auto interval_1_3 = constant_interval_exprt(val1, val3);
+      auto op1 = make_value_set(interval_2_4, environment, ns);
+      auto op2 = make_value_set(interval_1_3, environment, ns);
 
       auto merged = widening_merge(op1, op2);
 
-      THEN("result is widen both bounds - [-4, 10]")
+      THEN("widen lower bound - {[-3, 3], [2, 4]}")
       {
-        EXPECT_MODIFIED(merged, val4minus, val10);
+        auto interval_3minus_3 =
+          constant_interval_exprt(from_integer(-3, type), val3);
+        EXPECT_MODIFIED(merged, {interval_3minus_3, interval_2_4});
       }
     }
+    /*
     WHEN("merging [-3, -1] with [-4, -2]")
     {
       auto op1 = make_value_set(val3minus, val1minus, environment, ns);