From f88f3c71812cee94301243079ad3a42db9180671 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Mon, 15 Jun 2020 11:57:22 -0400
Subject: [PATCH 229/315] FIXME: more on
 widening_svalue2::eval_condition_without_cm

---
 gcc/analyzer/region-model2.cc | 129 +++++++++++++++++++++++++++++++---
 1 file changed, 120 insertions(+), 9 deletions(-)

diff --git a/gcc/analyzer/region-model2.cc b/gcc/analyzer/region-model2.cc
index 621fced83b8..0a622b4a881 100644
--- a/gcc/analyzer/region-model2.cc
+++ b/gcc/analyzer/region-model2.cc
@@ -864,32 +864,61 @@ widening_svalue2::eval_condition_without_cm (enum tree_code op,
       /* LHS is in [base_cst, +ve infinity), assuming no overflow.  */
       switch (op)
 	{
+	case LE_EXPR:
 	case LT_EXPR:
 	  {
-	    /* [BASE, +INF) < RHS:
-	       This is false at +ve ininity.  It can be true for points
-	       X where X < RHS, so we have either "false", or "unknown".  */
-	    tree base_lt_rhs = fold_binary (op, boolean_type_node,
+	    /* [BASE, +INF) OP RHS:
+	       This is either true or false at +ve ininity,
+	       It can be true for points X where X OP RHS, so we have either
+	       "false", or "unknown".  */
+	    tree base_op_rhs = fold_binary (op, boolean_type_node,
 					    base_cst, rhs_cst);
-	    if (base_lt_rhs == boolean_true_node)
+	    if (base_op_rhs == boolean_true_node)
 	      return tristate::TS_UNKNOWN;
 	    else
 	      return tristate::TS_FALSE;
 	  }
 
 	case GE_EXPR:
+	case GT_EXPR:
 	  {
-	    /* [BASE, +INF) >= RHS:
+	    /* [BASE, +INF) OP RHS:
 	       This is true at +ve infinity.  It will be true everywhere
 	       in the range if BASE >= RHS.  */
-	    tree base_ge_rhs = fold_binary (op, boolean_type_node,
+	    tree base_op_rhs = fold_binary (op, boolean_type_node,
 					    base_cst, rhs_cst);
-	    if (base_ge_rhs == boolean_true_node)
+	    if (base_op_rhs == boolean_true_node)
 	      return tristate::TS_TRUE;
 	    else
 	      return tristate::TS_UNKNOWN;
 	  }
 
+	case EQ_EXPR:
+	  {
+	    /* [BASE, +INF) == RHS:
+	       Could this be true at any point in the range?  If so we
+	       have "unknown", otherwise we have "false".  */
+	    tree base_le_rhs = fold_binary (LE_EXPR, boolean_type_node,
+					    base_cst, rhs_cst);
+	    if (base_le_rhs == boolean_true_node)
+	      return tristate::TS_UNKNOWN;
+	    else
+	      return tristate::TS_FALSE;
+	  }
+
+	case NE_EXPR:
+	  {
+	    /* [BASE, +INF) != RHS:
+	       Could we have equality at any point in the range?  If so we
+	       have "unknown", otherwise we have "true".  */
+	    tree base_le_rhs = fold_binary (LE_EXPR, boolean_type_node,
+					    base_cst, rhs_cst);
+	    if (base_le_rhs == boolean_true_node)
+	      return tristate::TS_UNKNOWN;
+	    else
+	      return tristate::TS_TRUE;
+	  }
+
 	default:
 	  return tristate::TS_UNKNOWN;
 	}
@@ -10024,6 +10053,84 @@ test_constraint_merging ()
 	     tristate (tristate::TS_UNKNOWN));
 }
 
+/* FIXME.  */
+
+static void
+test_widening_constraints ()
+{
+  program_point point (program_point::origin ());
+  tree int_0 = build_int_cst (integer_type_node, 0);
+  tree int_m1 = build_int_cst (integer_type_node, -1);
+  tree int_1 = build_int_cst (integer_type_node, 1);
+  tree int_256 = build_int_cst (integer_type_node, 256);
+  region_model2_manager mgr;
+  test_region_model2_context ctxt;
+  const svalue2 *int_0_sval = mgr.get_or_create_constant_svalue2 (int_0);
+  const svalue2 *int_1_sval = mgr.get_or_create_constant_svalue2 (int_1);
+  const svalue2 *w_zero_then_one_sval
+    = mgr.get_or_create_widening_svalue2 (integer_type_node, point,
+					  int_0_sval, int_1_sval);
+  const widening_svalue2 *w_zero_then_one
+    = w_zero_then_one_sval->dyn_cast_widening_svalue2 ();
+  ASSERT_EQ (w_zero_then_one->get_direction (),
+	     widening_svalue2::DIR_ASCENDING);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LT_EXPR, int_m1),
+	     tristate::TS_FALSE);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LT_EXPR, int_0),
+	     tristate::TS_FALSE);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LT_EXPR, int_1),
+	     tristate::TS_UNKNOWN);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LT_EXPR, int_256),
+	     tristate::TS_UNKNOWN);
+
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LE_EXPR, int_m1),
+	     tristate::TS_FALSE);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LE_EXPR, int_0),
+	     tristate::TS_UNKNOWN);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LE_EXPR, int_1),
+	     tristate::TS_UNKNOWN);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (LE_EXPR, int_256),
+	     tristate::TS_UNKNOWN);
+
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GT_EXPR, int_m1),
+	     tristate::TS_TRUE);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GT_EXPR, int_0),
+	     tristate::TS_UNKNOWN);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GT_EXPR, int_1),
+	     tristate::TS_UNKNOWN);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GT_EXPR, int_256),
+	     tristate::TS_UNKNOWN);
+
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GE_EXPR, int_m1),
+	     tristate::TS_TRUE);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GE_EXPR, int_0),
+	     tristate::TS_TRUE);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GE_EXPR, int_1),
+	     tristate::TS_UNKNOWN);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (GE_EXPR, int_256),
+	     tristate::TS_UNKNOWN);
+
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (EQ_EXPR, int_m1),
+	     tristate::TS_FALSE);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (EQ_EXPR, int_0),
+	     tristate::TS_UNKNOWN);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (EQ_EXPR, int_1),
+	     tristate::TS_UNKNOWN);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (EQ_EXPR, int_256),
+	     tristate::TS_UNKNOWN);
+
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (NE_EXPR, int_m1),
+	     tristate::TS_TRUE);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (NE_EXPR, int_0),
+	     tristate::TS_UNKNOWN);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (NE_EXPR, int_1),
+	     tristate::TS_UNKNOWN);
+  ASSERT_EQ (w_zero_then_one->eval_condition_without_cm (NE_EXPR, int_256),
+	     tristate::TS_UNKNOWN);
+
+  // TODO: a descending value
+}
+
 /* Verify merging constraints for states simulating successive iterations
    of a loop.
    Simulate:
@@ -10143,8 +10250,11 @@ test_iteration_1 ()
   ASSERT_TRUE (model5.can_merge_with_p (model2, point, &model6));
   const svalue2 *merged_widening = model6.get_rvalue (i, &ctxt);
   ASSERT_EQ (merged_widening->get_kind (), svalue2::SK_WIDENING);
+  // FIXME: what constraints should we have here?
 
-  // TODO
+  // TODO: constraints at end of loop (with i >= 256; should get i == 256)
+  /* TODO: unittests for widening_svalue2::eval_condition_without_cm
+     (separately).  */
 #endif
 }
 
@@ -10517,6 +10627,7 @@ analyzer_region_model2_cc_tests ()
 #endif
   test_state_merging ();
   test_constraint_merging ();
+  test_widening_constraints ();
   test_iteration_1 ();
   test_iteration_2 ();
 #if 0
-- 
2.26.2

