Intervals [FALSE, TRUE] go to top.

Intervals with range [min(type), max(type)] go top. However, by
extension [FALSE, TRUE] should also go top. This change extends the TOP
check constructing interval_abstract_values to cover intervals of type
bool and c_bool.

Author: jezhiggins

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

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

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 \

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