From 023517c98657c91fce8101155f24790334643975 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Thu, 18 Jun 2020 16:34:34 -0400
Subject: [PATCH 239/315] FIXME: add test_redundant_constraints

---
 gcc/analyzer/constraint-manager2.cc | 33 +++++++++++++++++++++++++++++
 gcc/analyzer/region-model2.cc       | 18 ++++++++++++++++
 2 files changed, 51 insertions(+)

diff --git a/gcc/analyzer/constraint-manager2.cc b/gcc/analyzer/constraint-manager2.cc
index 0f2b8244507..8fd8351c935 100644
--- a/gcc/analyzer/constraint-manager2.cc
+++ b/gcc/analyzer/constraint-manager2.cc
@@ -2632,6 +2632,38 @@ test_many_constants ()
     }
 }
 
+/* FIXME.  */
+
+static void
+test_redundant_constraints ()
+{
+  tree int_257 = build_int_cst (integer_type_node, 257);
+  tree int_256 = build_int_cst (integer_type_node, 256);
+  tree i = build_global_decl ("i", integer_type_node);
+
+  {
+    /* i < 257 then i < 256.  */
+    region_model2_manager mgr;
+    region_model2 model0 (&mgr);
+    ADD_SAT_CONSTRAINT (model0, i, LT_EXPR, int_257);
+    ADD_SAT_CONSTRAINT (model0, i, LT_EXPR, int_256);
+    ASSERT_CONDITION_TRUE2 (model0, i, LT_EXPR, int_256);
+    ASSERT_CONDITION_TRUE2 (model0, i, LT_EXPR, int_257);
+
+    /* i < 256 then i < 257.  */
+    region_model2 model1 (&mgr);
+    ADD_SAT_CONSTRAINT (model1, i, LT_EXPR, int_256);
+    ADD_SAT_CONSTRAINT (model1, i, LT_EXPR, int_257);
+    ASSERT_CONDITION_TRUE2 (model1, i, LT_EXPR, int_256);
+    ASSERT_CONDITION_TRUE2 (model1, i, LT_EXPR, int_257);
+    ASSERT_EQ (model1.get_constraints2 ()->m_equiv_classes.length (), 2);
+    ASSERT_EQ (model1.get_constraints2 ()->m_constraints.length (), 1);
+
+    // TODO:
+    //ASSERT_EQ (model1, model0);
+  }
+}
+
 /* Run the selftests in this file, temporarily overriding
    flag_analyzer_transitivity with TRANSITIVITY.  */
 
@@ -2651,6 +2683,7 @@ run_constraint_manager2_tests (bool transitivity)
   test_constraint_impl ();
   test_equality ();
   test_many_constants ();
+  test_redundant_constraints ();
 
   flag_analyzer_transitivity = saved_flag_analyzer_transitivity;
 }
diff --git a/gcc/analyzer/region-model2.cc b/gcc/analyzer/region-model2.cc
index 9c7ae379b2a..cfea545d5bb 100644
--- a/gcc/analyzer/region-model2.cc
+++ b/gcc/analyzer/region-model2.cc
@@ -10086,6 +10086,7 @@ test_iteration_1 ()
   tree int_0 = build_int_cst (integer_type_node, 0);
   tree int_1 = build_int_cst (integer_type_node, 1);
   tree int_256 = build_int_cst (integer_type_node, 256);
+  tree int_257 = build_int_cst (integer_type_node, 257);
   tree i = build_global_decl ("i", integer_type_node);
 
   region_model2_manager mgr;
@@ -10154,6 +10155,23 @@ test_iteration_1 ()
   ASSERT_EQ (merged_widening->get_kind (), svalue2::SK_WIDENING);
   // FIXME: what constraints should we have here?
 
+  ASSERT_CONDITION_TRUE2 (model6, i, LT_EXPR, int_257);
+
+  /* This is a cache miss (we have i < 257 rather than i < 256).
+     However, on applying the loop-bound condition...
+     FIXME.  */
+
+  region_model2 model7_t (model6);
+  ADD_SAT_CONSTRAINT (model7_t, i, LT_EXPR, int_256);
+
+  region_model2 model7_f (model6);
+#if ITERATED_BINOPS
+  ADD_SAT_CONSTRAINT (model7_f, i, GE_EXPR, int_256);
+  ASSERT_CONDITION_TRUE2 (model7_f, i, EQ_EXPR, int_256);
+#endif /* ITERATED_BINOPS */
+
+  //ASSERT_EQ (model6, model3);
+
   // TODO: constraints at end of loop (with i >= 256; should get i == 256)
   /* TODO: unittests for widening_svalue2::eval_condition_without_cm
      (separately).  */
-- 
2.26.2