Merge pull request #6209 from jezhiggins/vsd-bool-intervals-go-top

VSD - bool intervals go top

Author: martin-cs

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-intervals.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 main::1::b1 \(\) -> \[1, 1\] @ \[2\]
 main::1::b2 \(\) -> \[0, 0\] @ \[3\]
-main::1::b3 \(\) -> \[0, 1\] @ \[5\]
+main::1::b3 \(\) -> TOP @ \[5\]
 main::1::i \(\) -> \[A, A\] @ \[7\]
 main::1::j \(\) -> \[14, 14\] @ \[9\]
 main::1::k \(\) -> \[A, 14\] @ \[11\]

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/interval_abstract_value.cpp

@@ -244,9 +244,25 @@ interval_abstract_valuet::interval_abstract_valuet(
 {
 }
 
+bool new_interval_is_top(const constant_interval_exprt &e)
+{
+  if(e.is_top())
+    return true;
+
+  if(e.get_lower().is_false() && e.get_upper().is_true())
+    return true;
+  if(
+    e.type().id() == ID_c_bool && e.get_lower().is_zero() &&
+    e.get_upper().is_one())
+    return true;
+
+  return false;
+}
+
 interval_abstract_valuet::interval_abstract_valuet(
   const constant_interval_exprt &e)
-  : abstract_value_objectt(e.type(), e.is_top(), e.is_bottom()), interval(e)
+  : abstract_value_objectt(e.type(), new_interval_is_top(e), e.is_bottom()),
+    interval(e)
 {
 }
 
@@ -290,6 +306,11 @@ exprt interval_abstract_valuet::to_constant() const
 #endif
 }
 
+void interval_abstract_valuet::set_top_internal()
+{
+  interval = constant_interval_exprt(type());
+}
+
 size_t interval_abstract_valuet::internal_hash() const
 {
   return std::hash<std::string>{}(interval.pretty());

src/analyses/variable-sensitivity/interval_abstract_value.h

@@ -96,6 +96,8 @@ class interval_abstract_valuet : public abstract_value_objectt
 
 private:
   constant_interval_exprt interval;
+
+  void set_top_internal() override;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H

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

@@ -21,6 +21,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \
        analyses/variable-sensitivity/eval.cpp \
        analyses/variable-sensitivity/eval-member-access.cpp \
+       analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp \
        analyses/variable-sensitivity/interval_abstract_value/meet.cpp \
        analyses/variable-sensitivity/interval_abstract_value/merge.cpp \
        analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp \
@@ -29,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/interval_abstract_value/extremes-go-top.cpp

@@ -0,0 +1,73 @@
+/*******************************************************************\
+
+ Module: Unit tests for interval_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>
+
+static void
+verify_extreme_interval(typet type, abstract_environmentt &env, namespacet &ns)
+{
+  auto interval = make_interval(min_exprt(type), max_exprt(type), env, ns);
+
+  EXPECT_TOP(interval);
+}
+
+SCENARIO(
+  "extreme intervals go TOP",
+  "[core][analyses][variable-sensitivity][interval_abstract_value][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("[min-max] signed goes TOP")
+  {
+    verify_extreme_interval(signedbv_typet(32), environment, ns);
+  }
+  GIVEN("[min-max] unsigned goes TOP")
+  {
+    verify_extreme_interval(unsignedbv_typet(32), environment, ns);
+  }
+  GIVEN("[min-max] bool goes TOP")
+  {
+    verify_extreme_interval(bool_typet(), environment, ns);
+  }
+  GIVEN("[min-max] c_bool goes TOP")
+  {
+    verify_extreme_interval(bitvector_typet(ID_c_bool, 8), environment, ns);
+  }
+  GIVEN("[FALSE, TRUE] goes TOP")
+  {
+    auto boolInterval =
+      make_interval(false_exprt(), true_exprt(), 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_interval(
+      from_integer(0, c_bool_type),
+      from_integer(1, c_bool_type),
+      environment,
+      ns);
+
+    EXPECT_TOP(boolInterval);
+  }
+}

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