value_set_abstract_objectt non destruct compact

If the size of the set is large, if there are any intervals in the set,
try merging values into them.

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_object_set.h

@@ -44,6 +44,12 @@ class abstract_object_sett
       insert(value);
   }
 
+  void push_back(const abstract_object_pointert &v)
+  {
+    // alias for insert so we can use back_inserter
+    values.insert(v);
+  }
+
   abstract_object_pointert first() const
   {
     return *begin();

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -113,6 +113,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);
+
 value_set_abstract_objectt::value_set_abstract_objectt(const typet &type)
   : abstract_value_objectt(type)
 {
@@ -148,6 +150,8 @@ abstract_object_pointert value_set_abstract_objectt::make_value_set(
 
   auto values = unwrap_and_extract_values(initial_values);
 
+  values = compact_values(values);
+
   const auto &type = values.first()->type();
   auto value_set =
     std::make_shared<value_set_abstract_objectt>(type, false, false);
@@ -342,3 +346,65 @@ static bool are_any_top(const abstract_object_sett &set)
              return value->is_top();
            }) != set.end();
 }
+
+/////////////////
+static abstract_object_sett
+non_destructive_compact(const abstract_object_sett &values);
+static bool value_is_not_contained_in(
+  const abstract_object_pointert &object,
+  const std::vector<constant_interval_exprt> &intervals);
+
+static abstract_object_sett compact_values(const abstract_object_sett &values)
+{
+  if(values.size() <= value_set_abstract_objectt::max_value_set_size)
+    return values;
+
+  return non_destructive_compact(values);
+}
+
+static abstract_object_sett
+non_destructive_compact(const abstract_object_sett &values)
+{
+  auto intervals = std::vector<constant_interval_exprt>{};
+  for(auto const &object : values)
+  {
+    auto value =
+      std::dynamic_pointer_cast<const abstract_value_objectt>(object);
+    auto as_expr = value->to_interval();
+    if(!as_expr.is_single_value_interval())
+      intervals.push_back(as_expr);
+  }
+
+  if(intervals.empty())
+    return values;
+
+  auto compacted = 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),
+    [&intervals](const abstract_object_pointert &object) {
+      return value_is_not_contained_in(object, intervals);
+    });
+
+  return compacted;
+}
+
+static bool value_is_not_contained_in(
+  const abstract_object_pointert &object,
+  const std::vector<constant_interval_exprt> &intervals)
+{
+  auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(object);
+  auto as_expr = value->to_interval();
+
+  return std::none_of(
+    intervals.begin(),
+    intervals.end(),
+    [&as_expr](const constant_interval_exprt &interval) {
+      if(interval == as_expr)
+        return false;
+      return interval.contains(as_expr);
+    });
+}

unit/Makefile

@@ -28,6 +28,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/variable-sensitivity/last_written_location.cpp \
        analyses/variable-sensitivity/value_expression_evaluation/assume.cpp \
        analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp \
+       analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp \
        analyses/variable-sensitivity/value_set_abstract_object/meet.cpp \
        analyses/variable-sensitivity/value_set_abstract_object/merge.cpp \
        analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \

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

@@ -0,0 +1,169 @@
+/*******************************************************************\
+
+ Module: Unit tests for value_set_abstract_valuet compacting
+
+ Compacting occurs when the value_set get 'large', and takes two forms
+ non-destructive (eg, can we merge constants into an existing interval
+ with no loss of precision) and desctructive (creating intervals from
+ the constants, or merging existing intervals).
+
+ Author: Jez Higgins, [email protected]
+
+\*******************************************************************/
+
+#include "../variable_sensitivity_test_helpers.h"
+
+#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
+
+#include <testing-utils/use_catch.h>
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/mathematical_types.h>
+
+SCENARIO(
+  "compacting value sets",
+  "[core][analysis][variable-sensitivity][value_set_abstract_object][compact]")
+{
+  const typet type = signedbv_typet(32);
+  const exprt val1 = from_integer(1, type);
+  const exprt val2 = from_integer(2, type);
+  const exprt val3 = from_integer(3, type);
+  const exprt val4 = from_integer(4, type);
+  const exprt val5 = from_integer(5, type);
+  const exprt val6 = from_integer(6, type);
+  const exprt val7 = from_integer(7, type);
+  const exprt val8 = from_integer(8, type);
+  const exprt val9 = from_integer(9, type);
+  const exprt val10 = from_integer(10, type);
+  const exprt val11 = from_integer(11, type);
+  const exprt val12 = from_integer(12, type);
+  const exprt interval_5_10 = constant_interval_exprt(val5, val10);
+  const exprt interval_1_10 = constant_interval_exprt(val1, val10);
+
+  auto config = vsd_configt::constant_domain();
+  config.context_tracking.data_dependency_context = false;
+  config.context_tracking.last_write_context = false;
+  auto object_factory =
+    variable_sensitivity_object_factoryt::configured_with(config);
+  auto environment = abstract_environmentt{object_factory};
+  environment.make_top();
+  auto symbol_table = symbol_tablet{};
+  auto ns = namespacet{symbol_table};
+
+  GIVEN("compact values into existing interval")
+  {
+    WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, [5, 10]")
+    {
+      auto value_set = make_value_set(
+        {val1,
+         val2,
+         val3,
+         val4,
+         val5,
+         val6,
+         val7,
+         val8,
+         val9,
+         val10,
+         interval_5_10},
+        environment,
+        ns);
+      THEN("{ 1, 2, 3, 4, [5, 10] }")
+      {
+        EXPECT(value_set, {val1, val2, val3, val4, interval_5_10});
+      }
+    }
+    WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, [1, 10]")
+    {
+      auto value_set = make_value_set(
+        {val1,
+         val2,
+         val3,
+         val4,
+         val5,
+         val6,
+         val7,
+         val8,
+         val9,
+         val10,
+         interval_1_10},
+        environment,
+        ns);
+      THEN("{ [1, 10] }")
+      {
+        EXPECT(value_set, {interval_1_10});
+      }
+    }
+    WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, [5, 10]")
+    {
+      auto value_set = make_value_set(
+        {val1,
+         val2,
+         val3,
+         val4,
+         val5,
+         val6,
+         val7,
+         val8,
+         val9,
+         val10,
+         val11,
+         val12,
+         interval_5_10},
+        environment,
+        ns);
+      THEN("{ 1, 2, 3, 4, 11, 12, [5, 10] }")
+      {
+        EXPECT(
+          value_set, {val1, val2, val3, val4, val11, val12, interval_5_10});
+      }
+    }
+    WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, [1, 10], [5, 10]")
+    {
+      auto value_set = make_value_set(
+        {val1,
+         val2,
+         val3,
+         val4,
+         val5,
+         val6,
+         val7,
+         val8,
+         val9,
+         val10,
+         interval_1_10,
+         interval_5_10},
+        environment,
+        ns);
+      THEN("{ [1, 10] }")
+      {
+        EXPECT(value_set, {interval_1_10});
+      }
+    }
+    WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, [5, 10], [1, 10]")
+    {
+      auto value_set = make_value_set(
+        {val1,
+         val2,
+         val3,
+         val4,
+         val5,
+         val6,
+         val7,
+         val8,
+         val9,
+         val10,
+         val11,
+         val12,
+         interval_5_10,
+         interval_1_10},
+        environment,
+        ns);
+      THEN("{ 11, 12, [1, 10] }")
+      {
+        EXPECT(value_set, {val11, val12, interval_1_10});
+      }
+    }
+  }
+}