From 09dddcb4688f5b85ef02e2eb2039a8b56f35f704 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Fri, 29 Mar 2019 15:23:33 -0400
Subject: [PATCH 166/217] FIXME: recursive transitivity for constraints

---
 gcc/analyzer/constraints.cc | 87 ++++++++++++++++++++++++++++++++++++++-------
 gcc/analyzer/constraints.h  |  4 +++
 2 files changed, 78 insertions(+), 13 deletions(-)

diff --git a/gcc/analyzer/constraints.cc b/gcc/analyzer/constraints.cc
index d72e600..3bd7b09 100644
--- a/gcc/analyzer/constraints.cc
+++ b/gcc/analyzer/constraints.cc
@@ -486,7 +486,16 @@ path_state::add_constraint (path_var lhs, enum tree_code op, path_var rhs)
 {
   equiv_class_id lhs_ec_id = get_or_add_equiv_class (lhs);
   equiv_class_id rhs_ec_id = get_or_add_equiv_class (rhs);
+  return add_constraint (lhs_ec_id, op,rhs_ec_id);
+}
+
+/* FIXME.  */
 
+bool
+path_state::add_constraint (equiv_class_id lhs_ec_id,
+			    enum tree_code op,
+			    equiv_class_id rhs_ec_id)
+{
   tristate t = eval_condition (lhs_ec_id, op, rhs_ec_id);
 
   /* Discard constraints that are already known.  */
@@ -571,6 +580,8 @@ path_state::add_constraint (path_var lhs, enum tree_code op, path_var rhs)
   return true;
 }
 
+/* FIXME.  */
+
 void
 path_state::add_constraint_internal (equiv_class_id lhs_id,
 				     enum constraint_op c_op,
@@ -591,9 +602,12 @@ path_state::add_constraint_internal (equiv_class_id lhs_id,
 	 will also add:
 	   (a < c)
 	   (b < d)
-	 TODO: but it doesn't add (a < d), I think.  */
-      int limit = m_constraints.length () - 1;
-      for (int i = 0; i < limit; i++)
+	 We need to recurse to ensure we also add:
+	   (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.  */
+      for (unsigned i = 0; i < m_constraints.length (); i++)
 	{
 	  const constraint *other = &m_constraints[i];
 	  if (other->is_ordering_p ())
@@ -604,24 +618,20 @@ path_state::add_constraint_internal (equiv_class_id lhs_id,
 		  /* With RHS == other.lhs, we have:
 		     "LHS </<= (RHS, other.lhs) </<= other.rhs"
 		     and thus this implies "LHS </<= other.rhs".  */
-		  enum constraint_op new_op
+		  enum tree_code new_op
 		    = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
-		       ? CONSTRAINT_LE : CONSTRAINT_LT);
-		  m_constraints.safe_push (constraint (lhs_id,
-						       new_op,
-						       other->m_rhs));
+		       ? LE_EXPR : LT_EXPR);
+		  add_constraint (lhs_id, new_op, other->m_rhs);
 		}
 	      if (other->m_rhs == lhs_id)
 		{
 		  /* With other.rhs == LHS, we have:
 		     "other.lhs </<= (other.rhs, LHS) </<= RHS"
 		     and thus this implies "other.lhs </<= RHS".  */
-		  enum constraint_op new_op
+		  enum tree_code new_op
 		    = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
-		       ? CONSTRAINT_LE : CONSTRAINT_LT);
-		  m_constraints.safe_push (constraint (other->m_lhs,
-						       new_op,
-						       rhs_id));
+		       ? LE_EXPR : LT_EXPR);
+		  add_constraint (other->m_lhs, new_op, rhs_id);
 		}
 	    }
 	}
@@ -1192,6 +1202,57 @@ test_constraint_conditions_2 ()
     ASSERT_CONDITION_UNKNOWN (ps, a, EQ_EXPR, c);
   }
 
+  /* Transitivity: "(a < b)", "(c < d)", "(b < c)" should
+     imply the easy cases:
+       (a < c)
+       (b < d)
+     but also that:
+       (a < d).  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, a, LT_EXPR, b);
+    ADD_SAT_CONSTRAINT (ps, c, LT_EXPR, d);
+    ADD_SAT_CONSTRAINT (ps, b, LT_EXPR, c);
+
+    ASSERT_CONDITION_TRUE (ps, a, LT_EXPR, c);
+    ASSERT_CONDITION_TRUE (ps, b, LT_EXPR, d);
+    ASSERT_CONDITION_TRUE (ps, a, LT_EXPR, d);
+  }
+
+  /* Transitivity: "a >= b", "b >= a" should imply that a == b.  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (ps, b, GE_EXPR, a);
+
+    // TODO:
+    //ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, b);
+  }
+
+  /* Transitivity: "a >= b", "b >= c", "c >= a" should imply
+     that a == b == c.  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, b);
+    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);
+  }
+
+  /* Transitivity: "a > b", "b > c", "c > a"
+     should be impossible.  */
+  {
+    path_state ps;
+    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);
+  }
+
 }
 
 /* FIXME.  */
diff --git a/gcc/analyzer/constraints.h b/gcc/analyzer/constraints.h
index 0df40a9..2b99743 100644
--- a/gcc/analyzer/constraints.h
+++ b/gcc/analyzer/constraints.h
@@ -164,6 +164,10 @@ public:
 
   bool add_constraint (path_var lhs, enum tree_code op, path_var rhs);
 
+  bool add_constraint (equiv_class_id lhs_ec_id,
+		       enum tree_code op,
+		       equiv_class_id rhs_ec_id);
+
   //private:
   bool apply_constraints_for_call (const call_superedge& edge);
 
-- 
1.8.5.3

