Value sets spanning the min-max range of its type go to TOP.

Author: jezhiggins

regression/goto-analyzer/nondet-bool/main.c

@@ -0,0 +1,11 @@
+_Bool nondet_bool();
+int main()
+{
+  int x = 0;
+  while(1)
+  {
+    if(nondet_bool())
+      x = x + 1;
+    assert(x != 1000);
+  }
+}

regression/goto-analyzer/nondet-bool/test-constants.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--vsd --one-domain-per-history --three-way-merge --loop-unwind-and-branching 16 --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line 9 assertion x != 1000: UNKNOWN
+--

regression/goto-analyzer/nondet-bool/test-intervals.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--vsd --one-domain-per-history --three-way-merge --loop-unwind-and-branching 16 --vsd-values intervals --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line 9 assertion x != 1000: UNKNOWN
+--

regression/goto-analyzer/nondet-bool/test-value-sets.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--vsd --one-domain-per-history --three-way-merge --loop-unwind-and-branching 16 --vsd-values set-of-constants --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line 9 assertion x != 1000: UNKNOWN
+--

regression/goto-analyzer/ternary-operator/test-value-sets.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 main::1::b1 \(\) -> value-set-begin: TRUE :value-set-end
 main::1::b2 \(\) -> value-set-begin: FALSE :value-set-end
-main::1::b3 \(\) -> value-set-begin: TRUE, FALSE :value-set-end
+main::1::b3 \(\) -> TOP @ \[5\]
 main::1::i \(\) -> value-set-begin: 10 :value-set-end
 main::1::j \(\) -> value-set-begin: 20 :value-set-end
 main::1::k \(\) -> value-set-begin: 10, 20 :value-set-end

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -116,6 +116,7 @@ static abstract_object_pointert
 maybe_extract_single_value(const abstract_object_pointert &maybe_singleton);
 
 static bool are_any_top(const abstract_object_sett &set);
+static bool is_set_extreme(const typet &type, const abstract_object_sett &set);
 
 static abstract_object_sett compact_values(const abstract_object_sett &values);
 static abstract_object_sett widen_value_set(
@@ -296,7 +297,7 @@ void value_set_abstract_objectt::set_values(
   const abstract_object_sett &other_values)
 {
   PRECONDITION(!other_values.empty());
-  if(are_any_top(other_values))
+  if(are_any_top(other_values) || is_set_extreme(type(), other_values))
   {
     set_top();
   }
@@ -391,6 +392,65 @@ static bool are_any_top(const abstract_object_sett &set)
            }) != set.end();
 }
 
+using set_predicate_fn = std::function<bool(const abstract_value_objectt &)>;
+static bool set_contains(const abstract_object_sett &set, set_predicate_fn pred)
+{
+  return std::find_if(
+           set.begin(),
+           set.end(),
+           [&pred](const abstract_object_pointert &obj) {
+             const auto &value =
+               std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
+             return pred(*value);
+           }) != set.end();
+}
+
+static bool set_has_extremes(
+  const abstract_object_sett &set,
+  set_predicate_fn lower_fn,
+  set_predicate_fn upper_fn)
+{
+  bool has_lower = set_contains(set, lower_fn);
+  if(!has_lower)
+    return false;
+
+  bool has_upper = set_contains(set, upper_fn);
+  return has_upper;
+}
+
+static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
+{
+  if(type.id() == ID_bool)
+  {
+    return set_has_extremes(
+      set,
+      [](const abstract_value_objectt &value) {
+        auto c = value.to_constant();
+        return c.is_false() || (c.id() == ID_min);
+      },
+      [](const abstract_value_objectt &value) {
+        auto c = value.to_constant();
+        return c.is_true() || (c.id() == ID_max);
+      });
+  }
+
+  if(type.id() == ID_c_bool)
+  {
+    return set_has_extremes(
+      set,
+      [](const abstract_value_objectt &value) {
+        auto c = value.to_constant();
+        return c.is_zero() || (c.id() == ID_min);
+      },
+      [](const abstract_value_objectt &value) {
+        auto c = value.to_constant();
+        return c.is_one() || (c.id() == ID_max);
+      });
+  }
+
+  return false;
+}
+
 /////////////////
 static abstract_object_sett
 non_destructive_compact(const abstract_object_sett &values);

unit/Makefile

@@ -30,6 +30,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/variable-sensitivity/value_expression_evaluation/assume.cpp \
        analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp \
        analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp \
+       analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.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 \

unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp

@@ -0,0 +1,63 @@
+/*******************************************************************\
+
+ Module: Unit tests for value_set_abstract_valuet
+
+ Author: Jez Higgins
+
+\*******************************************************************/
+
+#include <analyses/variable-sensitivity/abstract_environment.h>
+#include <analyses/variable-sensitivity/abstract_object.h>
+#include <analyses/variable-sensitivity/interval_abstract_value.h>
+#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
+#include <testing-utils/use_catch.h>
+
+#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+
+SCENARIO(
+  "value-sets spanning min-max go TOP",
+  "[core][analyses][variable-sensitivity][value_set_abstract_object][extreme]")
+{
+  auto object_factory = variable_sensitivity_object_factoryt::configured_with(
+    vsd_configt::intervals());
+
+  auto environment = abstract_environmentt{object_factory};
+  environment.make_top();
+  auto symbol_table = symbol_tablet{};
+  auto ns = namespacet{symbol_table};
+
+  GIVEN("{FALSE, TRUE} goes TOP")
+  {
+    auto boolInterval =
+      make_value_set({false_exprt(), true_exprt()}, environment, ns);
+
+    EXPECT_TOP(boolInterval);
+  }
+  GIVEN("{min(bool), max(bool)} goes TOP")
+  {
+    auto boolInterval = make_value_set(
+      {min_exprt(bool_typet()), max_exprt(bool_typet())}, environment, ns);
+
+    EXPECT_TOP(boolInterval);
+  }
+  GIVEN("{0, 1} c_bool goes TOP")
+  {
+    auto c_bool_type = bitvector_typet(ID_c_bool, 8);
+    auto boolInterval = make_value_set(
+      {from_integer(0, c_bool_type), from_integer(1, c_bool_type)},
+      environment,
+      ns);
+
+    EXPECT_TOP(boolInterval);
+  }
+  GIVEN("{min(c_bool), max(c_bool)} goes TOP")
+  {
+    auto c_bool_type = bitvector_typet(ID_c_bool, 8);
+    auto boolInterval = make_value_set(
+      {min_exprt(c_bool_type), max_exprt(c_bool_type)}, environment, ns);
+
+    EXPECT_TOP(boolInterval);
+  }
+}