From ba7a56abdcf38308420a0cd2bf371cfbddbbefdd Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Thu, 18 Jun 2020 12:18:52 -0400
Subject: [PATCH 238/315] FIXME: avoid creating ECs when rejecting
 self-comparisons

---
 gcc/analyzer/constraint-manager2.cc | 83 +++++++++++++++++++++++++++--
 gcc/analyzer/constraint-manager2.h  |  4 ++
 2 files changed, 83 insertions(+), 4 deletions(-)

diff --git a/gcc/analyzer/constraint-manager2.cc b/gcc/analyzer/constraint-manager2.cc
index 7e09e69d869..0f2b8244507 100644
--- a/gcc/analyzer/constraint-manager2.cc
+++ b/gcc/analyzer/constraint-manager2.cc
@@ -768,9 +768,38 @@ constraint_manager2::add_constraint (const svalue2 *lhs,
     /* Not a contradiction.  */
     return true;
 
+  /* Check the conditions on svalues.  */
+  {
+    tristate t_cond = eval_condition (lhs, op, rhs);
+
+    /* If we already have the condition, do nothing.  */
+    if (t_cond.is_true ())
+      return true;
+
+    /* Reject a constraint that would contradict existing knowledge, as
+       unsatisfiable.  */
+    if (t_cond.is_false ())
+      return false;
+  }
+
   equiv_class2_id lhs_ec_id = get_or_add_equiv_class2 (lhs);
   equiv_class2_id rhs_ec_id = get_or_add_equiv_class2 (rhs);
-  return add_constraint (lhs_ec_id, op,rhs_ec_id);
+
+  /* Check the stronger conditions on ECs.  */
+  {
+    tristate t = eval_condition (lhs_ec_id, op, rhs_ec_id);
+
+    /* Discard constraints that are already known.  */
+    if (t.is_true ())
+      return true;
+
+    /* Reject unsatisfiable constraints.  */
+    if (t.is_false ())
+      return false;
+  }
+
+  add_unknown_constraint (lhs_ec_id, op, rhs_ec_id);
+  return true;
 }
 
 /* Attempt to add the constraint LHS_EC_ID OP RHS_EC_ID to this
@@ -780,8 +809,8 @@ constraint_manager2::add_constraint (const svalue2 *lhs,
 
 bool
 constraint_manager2::add_constraint (equiv_class2_id lhs_ec_id,
-				    enum tree_code op,
-				    equiv_class2_id rhs_ec_id)
+				     enum tree_code op,
+				     equiv_class2_id rhs_ec_id)
 {
   tristate t = eval_condition (lhs_ec_id, op, rhs_ec_id);
 
@@ -793,6 +822,18 @@ constraint_manager2::add_constraint (equiv_class2_id lhs_ec_id,
   if (t.is_false ())
     return false;
 
+  add_unknown_constraint (lhs_ec_id, op, rhs_ec_id);
+  return true;
+}
+
+/* Add the constraint LHS_EC_ID OP RHS_EC_ID to this constraint_manager2,
+   where the constraint has already been checked for being "unknown".  */
+
+void
+constraint_manager2::add_unknown_constraint (equiv_class2_id lhs_ec_id,
+					     enum tree_code op,
+					     equiv_class2_id rhs_ec_id)
+{
   gcc_assert (lhs_ec_id != rhs_ec_id);
 
   /* For now, simply accumulate constraints, without attempting any further
@@ -871,7 +912,6 @@ constraint_manager2::add_constraint (equiv_class2_id lhs_ec_id,
       break;
     }
   validate ();
-  return true;
 }
 
 /* Subroutine of constraint_manager2::add_constraint, for handling all
@@ -1280,6 +1320,26 @@ constraint_manager2::eval_condition (const svalue2 *lhs,
       || rhs->get_kind () == svalue2::SK_UNKNOWN)
     return tristate (tristate::TS_UNKNOWN);
 
+  if (lhs == rhs
+      && !(FLOAT_TYPE_P (lhs->get_type ())
+	   || FLOAT_TYPE_P (rhs->get_type ())))
+    {
+      switch (op)
+	{
+	case EQ_EXPR:
+	case GE_EXPR:
+	case LE_EXPR:
+	  return tristate (tristate::TS_TRUE);
+
+	case NE_EXPR:
+	case GT_EXPR:
+	case LT_EXPR:
+	  return tristate (tristate::TS_FALSE);
+	default:
+	  break;
+	}
+    }
+
   equiv_class2_id lhs_ec (-1);
   equiv_class2_id rhs_ec (-1);
   get_equiv_class2_by_svalue2 (lhs, &lhs_ec);
@@ -1846,6 +1906,21 @@ test_constraint_conditions ()
     ASSERT_CONDITION_FALSE2 (model, x, GT_EXPR, x);
   }
 
+  /* Adding self-equality shouldn't add equiv classes.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, x);
+    ADD_SAT_CONSTRAINT (model, int_42, EQ_EXPR, int_42);
+    /* ...even when done directly via svalues: */
+    const svalue2 *sval_int_42 = model.get_rvalue (int_42, NULL);
+    bool sat = model.get_constraints2 ()->add_constraint (sval_int_42,
+							  EQ_EXPR,
+							  sval_int_42);
+    ASSERT_TRUE (sat);
+    ASSERT_EQ (model.get_constraints2 ()->m_equiv_classes.length (), 0);
+  }
+
   /* x == y.  */
   {
     region_model2_manager mgr;
diff --git a/gcc/analyzer/constraint-manager2.h b/gcc/analyzer/constraint-manager2.h
index 275ab262fe5..37d329bb83c 100644
--- a/gcc/analyzer/constraint-manager2.h
+++ b/gcc/analyzer/constraint-manager2.h
@@ -247,6 +247,10 @@ public:
 		       enum tree_code op,
 		       equiv_class2_id rhs_ec_id);
 
+  void add_unknown_constraint (equiv_class2_id lhs_ec_id,
+			       enum tree_code op,
+			       equiv_class2_id rhs_ec_id);
+
   bool get_equiv_class2_by_svalue2 (const svalue2 *sval,
 				    equiv_class2_id *out) const;
   equiv_class2_id get_or_add_equiv_class2 (const svalue2 *sval);
-- 
2.26.2