From 6180646b4dbdcc3148039e61a693e4d0e891d25d Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Fri, 29 Mar 2019 16:04:31 -0400
Subject: [PATCH 167/169] FIXME: handle (a >= b) and (b >=a) implying (a == b)
 and similar

---
 gcc/analyzer/constraints.cc | 60 +++++++++++++++++++++++++++++++++++++++------
 gcc/analyzer/constraints.h  |  2 ++
 2 files changed, 54 insertions(+), 8 deletions(-)

diff --git a/gcc/analyzer/constraints.cc b/gcc/analyzer/constraints.cc
index 3bd7b09..2bb07a7 100644
--- a/gcc/analyzer/constraints.cc
+++ b/gcc/analyzer/constraints.cc
@@ -174,6 +174,21 @@ equiv_class::purge_stack_frame (int callee_stack_depth)
   // FIXME: doesn't need to preserve order
 }
 
+/* Get a representative member of this class, for handling cases
+   where the IDs can change mid-traversal.  */
+
+path_var
+equiv_class::get_representative () const
+{
+  if (m_constant)
+    return path_var (m_constant, 0);
+  else
+    {
+      gcc_assert (m_vars.length () > 0);
+      return m_vars[0];
+    }
+}
+
 /* FIXME.  */
 
 const char *
@@ -606,13 +621,39 @@ path_state::add_constraint_internal (equiv_class_id lhs_id,
 	   (a < d).
 	 We call the checked add_constraint to avoid adding constraints
 	 that are already present.  Doing so also ensures termination
-	 in the case of cycles.  */
+	 in the case of cycles.
+
+	 We can potentially add EQ_EXPR facts, which could lead to ECs
+	 being merged, which would change the meaning of the EC IDs.
+	 Hence we need to do this via path vars.  */
+      path_var lhs = lhs_id.get_obj (*this).get_representative ();
+      path_var rhs = rhs_id.get_obj (*this).get_representative ();
+
       for (unsigned i = 0; i < m_constraints.length (); i++)
 	{
 	  const constraint *other = &m_constraints[i];
 	  if (other->is_ordering_p ())
 	    {
+	      /* Refresh the EC IDs, in case any mergers have happened.  */
+	      lhs_id = get_or_add_equiv_class (lhs);
+	      rhs_id = get_or_add_equiv_class (rhs);
+
 	      /* We have "LHS </<= RHS" and "other.lhs </<= other.rhs".  */
+
+	      /* If we have LHS </<= RHS and RHS </<= LHS, then we have a
+		 cycle.  */
+	      if (rhs_id == other->m_lhs
+		  && other->m_rhs == lhs_id)
+		{
+		  /* We must have equality for this to be possible.  */
+		  gcc_assert (c_op == CONSTRAINT_LE
+			      && other->m_op == CONSTRAINT_LE);
+		  add_constraint (lhs_id, EQ_EXPR, rhs_id);
+		  /* Adding an equality will merge the two ECs and potentially
+		     reorganize the constraints.  Stop iterating.  */
+		  return;
+		}
+	      /* Otherwise, check for transitivity.  */
 	      if (rhs_id == other->m_lhs)
 		{
 		  /* With RHS == other.lhs, we have:
@@ -623,7 +664,7 @@ path_state::add_constraint_internal (equiv_class_id lhs_id,
 		       ? LE_EXPR : LT_EXPR);
 		  add_constraint (lhs_id, new_op, other->m_rhs);
 		}
-	      if (other->m_rhs == lhs_id)
+	      else if (other->m_rhs == lhs_id)
 		{
 		  /* With other.rhs == LHS, we have:
 		     "other.lhs </<= (other.rhs, LHS) </<= RHS"
@@ -1226,7 +1267,14 @@ test_constraint_conditions_2 ()
     ADD_SAT_CONSTRAINT (ps, b, GE_EXPR, a);
 
     // TODO:
-    //ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, b);
+  }
+
+  /* Transitivity: "a >= b", "b > a" should be impossible.  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, b);
+    ADD_UNSAT_CONSTRAINT (ps, b, GT_EXPR, a);
   }
 
   /* Transitivity: "a >= b", "b >= c", "c >= a" should imply
@@ -1237,8 +1285,7 @@ test_constraint_conditions_2 ()
     ADD_SAT_CONSTRAINT (ps, b, GE_EXPR, c);
     ADD_SAT_CONSTRAINT (ps, c, GE_EXPR, a);
 
-    // TODO:
-    //ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a > b", "b > c", "c > a"
@@ -1248,9 +1295,6 @@ test_constraint_conditions_2 ()
     ADD_SAT_CONSTRAINT (ps, a, GT_EXPR, b);
     ADD_SAT_CONSTRAINT (ps, b, GT_EXPR, c);
     ADD_UNSAT_CONSTRAINT (ps, c, GT_EXPR, a);
-
-    // TODO:
-    //ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, c);
   }
 
 }
diff --git a/gcc/analyzer/constraints.h b/gcc/analyzer/constraints.h
index 2b99743..0a22c28 100644
--- a/gcc/analyzer/constraints.h
+++ b/gcc/analyzer/constraints.h
@@ -68,6 +68,8 @@ public:
 
   void purge_stack_frame (int callee_stack_depth);
 
+  path_var get_representative () const;
+
   /* An equivalence class can contain at most one constant.  */
   tree m_constant;
 
-- 
1.8.5.3

