From 69e834b2eddc6fc76f1eb4c26dad0aa797e14d1d Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Fri, 29 Mar 2019 12:15:28 -0400
Subject: [PATCH 165/169] FIXME: WIP on better constraints

---
 gcc/analyzer/constraints.cc | 184 +++++++++++++++++++++++++++++++++++---------
 gcc/analyzer/constraints.h  |  11 +++
 2 files changed, 158 insertions(+), 37 deletions(-)

diff --git a/gcc/analyzer/constraints.cc b/gcc/analyzer/constraints.cc
index c7a0844..d72e600 100644
--- a/gcc/analyzer/constraints.cc
+++ b/gcc/analyzer/constraints.cc
@@ -108,7 +108,10 @@ void
 equiv_class::add (path_var v)
 {
   if (CONSTANT_CLASS_P (v.m_tree))
-    m_constant = v.m_tree;
+    {
+      gcc_assert (m_constant == NULL_TREE);
+      m_constant = v.m_tree;
+    }
   else
     {
       m_vars.safe_push (v);
@@ -547,19 +550,19 @@ path_state::add_constraint (path_var lhs, enum tree_code op, path_var rhs)
       }
       break;
     case GE_EXPR:
-      m_constraints.safe_push (constraint (rhs_ec_id, CONSTRAINT_LE, lhs_ec_id));
+      add_constraint_internal (rhs_ec_id, CONSTRAINT_LE, lhs_ec_id);
       break;
     case LE_EXPR:
-      m_constraints.safe_push (constraint (lhs_ec_id, CONSTRAINT_LE, rhs_ec_id));
+      add_constraint_internal (lhs_ec_id, CONSTRAINT_LE, rhs_ec_id);
       break;
     case NE_EXPR:
-      m_constraints.safe_push (constraint (lhs_ec_id, CONSTRAINT_NE, rhs_ec_id));
+      add_constraint_internal (lhs_ec_id, CONSTRAINT_NE, rhs_ec_id);
       break;
     case GT_EXPR:
-      m_constraints.safe_push (constraint (rhs_ec_id, CONSTRAINT_LT, lhs_ec_id));
+      add_constraint_internal (rhs_ec_id, CONSTRAINT_LT, lhs_ec_id);
       break;
     case LT_EXPR:
-      m_constraints.safe_push (constraint (lhs_ec_id, CONSTRAINT_LT, rhs_ec_id));
+      add_constraint_internal (lhs_ec_id, CONSTRAINT_LT, rhs_ec_id);
       break;
     default:
       /* do nothing.  */
@@ -568,6 +571,63 @@ path_state::add_constraint (path_var lhs, enum tree_code op, path_var rhs)
   return true;
 }
 
+void
+path_state::add_constraint_internal (equiv_class_id lhs_id,
+				     enum constraint_op c_op,
+				     equiv_class_id rhs_id)
+{
+  m_constraints.safe_push (constraint (lhs_id, c_op, rhs_id));
+
+  if (c_op != CONSTRAINT_NE)
+    {
+      /* Handle transitivity of ordering by adding additional constraints
+	 based on what we already knew.
+
+	 So if we have already have:
+	   (a < b)
+	   (c < d)
+	 Then adding:
+	   (b < c)
+	 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++)
+	{
+	  const constraint *other = &m_constraints[i];
+	  if (other->is_ordering_p ())
+	    {
+	      /* We have "LHS </<= RHS" and "other.lhs </<= other.rhs".  */
+	      if (rhs_id == other->m_lhs)
+		{
+		  /* With RHS == other.lhs, we have:
+		     "LHS </<= (RHS, other.lhs) </<= other.rhs"
+		     and thus this implies "LHS </<= other.rhs".  */
+		  enum constraint_op 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));
+		}
+	      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
+		    = ((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));
+		}
+	    }
+	}
+    }
+}
+
 /* FIXME.  */
 
 bool
@@ -701,35 +761,6 @@ path_state::eval_condition (equiv_class_id lhs_ec,
 	}
     }
 
-#if 0
-  // TODO: what about implied orderings?
-  // transitivity:
-  // Only makes sense for inequalities
-  // e.g. x < z
-  if (op != EQ_EXPR && op != NE_EXPR)
-    {
-      int i;
-      constraint *c;
-      FOR_EACH_VEC_ELT (m_constraints, i, c)
-	{
-	  /* If we have "lhs OP mid", then
-	     consider comparisons with "mid", recursively.  */
-	  // FIXME: exactly what should the ops be?
-	  if (c->m_lhs == lhs_ec)
-	    if (op == LT_EXPR && c->m_op == CONSTRAINT_LT)
-	      {
-		tristate result_for_mid
-		  = eval_condition (c->m_rhs, op, rhs_ec);
-		if (result_for_mid.is_known ())
-		  return result_for_mid;
-	      }
-	  // FIXME: this is O(N^2)
-	  // FIXME: what about the other way around?
-	  // FIXME: other ops?  etc
-	}
-    }
-#endif
-
   return tristate (tristate::TS_UNKNOWN);
 }
 
@@ -1101,16 +1132,94 @@ test_constraint_conditions_2 ()
     ASSERT_CONDITION_TRUE (ps, a, EQ_EXPR, d);
   }
 
-#if 0
-  /* Transitivity: a < b, then b < c.  */
+  /* Transitivity: "a < b", "b < c" should imply "a < c".  */
   {
     path_state ps;
     ADD_SAT_CONSTRAINT (ps, a, LT_EXPR, b);
     ADD_SAT_CONSTRAINT (ps, b, LT_EXPR, c);
 
     ASSERT_CONDITION_TRUE (ps, a, LT_EXPR, c);
+    ASSERT_CONDITION_FALSE (ps, a, EQ_EXPR, c);
   }
+
+  /* Transitivity: "a <= b", "b < c" should imply "a < c".  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, a, LE_EXPR, b);
+    ADD_SAT_CONSTRAINT (ps, b, LT_EXPR, c);
+
+    ASSERT_CONDITION_TRUE (ps, a, LT_EXPR, c);
+    ASSERT_CONDITION_FALSE (ps, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "a <= b", "b <= c" should imply "a <= c".  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, a, LE_EXPR, b);
+    ADD_SAT_CONSTRAINT (ps, b, LE_EXPR, c);
+
+    ASSERT_CONDITION_TRUE (ps, a, LE_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN (ps, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "a > b", "b > c" should imply "a > c".  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, a, GT_EXPR, b);
+    ADD_SAT_CONSTRAINT (ps, b, GT_EXPR, c);
+
+    ASSERT_CONDITION_TRUE (ps, a, GT_EXPR, c);
+    ASSERT_CONDITION_FALSE (ps, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "a >= b", "b > c" should imply " a > c".  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (ps, b, GT_EXPR, c);
+
+    ASSERT_CONDITION_TRUE (ps, a, GT_EXPR, c);
+    ASSERT_CONDITION_FALSE (ps, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "a >= b", "b >= c" should imply "a >= c".  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (ps, b, GE_EXPR, c);
+
+    ASSERT_CONDITION_TRUE (ps, a, GE_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN (ps, a, EQ_EXPR, c);
+  }
+
+}
+
+/* FIXME.  */
+
+static void
+test_constraint_conditions_3 ()
+{
+  path_var int_1023 (build_int_cst (integer_type_node, 1023), 0);
+  path_var int_1024 (build_int_cst (integer_type_node, 1024), 0);
+
+  path_var a (build_decl (UNKNOWN_LOCATION, PARM_DECL,
+			  get_identifier ("a"),
+			  integer_type_node), 0);
+
+  /* a >= 1024, then a <= 1023.  */
+  {
+    path_state ps;
+    ADD_SAT_CONSTRAINT (ps, a, GE_EXPR, int_1024);
+
+#if 0
+    range r = ps.get_range (ps.get_or_add_equiv_class (a));
+    ASSERT_EQ (r.m_lower_bound.m_constant, int_1024.m_tree);
+    ASSERT_TRUE (r.m_lower_bound.m_open);
+    ASSERT_EQ (r.m_upper_bound.m_constant, NULL_TREE);
 #endif
+
+    //ADD_UNSAT_CONSTRAINT (ps, a, LE_EXPR, int_1023);
+  }
 }
 
 /* FIXME.  */
@@ -1246,6 +1355,7 @@ analyzer_constraints_cc_tests ()
 {
   test_constraint_conditions ();
   test_constraint_conditions_2 ();
+  test_constraint_conditions_3 ();
   test_constraint_impl ();
   test_assignment ();
   test_stack_frames ();
diff --git a/gcc/analyzer/constraints.h b/gcc/analyzer/constraints.h
index 97149ba..0df40a9 100644
--- a/gcc/analyzer/constraints.h
+++ b/gcc/analyzer/constraints.h
@@ -120,6 +120,12 @@ class constraint {
 
   std::string to_str (const path_state &ps) const;
 
+  /* Is this an ordering, rather than a "!=".  */
+  bool is_ordering_p () const
+  {
+    return m_op != CONSTRAINT_NE;
+  }
+
   equiv_class_id m_lhs;
   enum constraint_op m_op;
   equiv_class_id m_rhs;
@@ -181,6 +187,11 @@ public:
   auto_vec<equiv_class *> m_equiv_classes;
   auto_vec<constraint> m_constraints;
   int m_stack_depth;
+
+ private:
+  void add_constraint_internal (equiv_class_id lhs_id,
+				enum constraint_op c_op,
+				equiv_class_id rhs_id);
 };
 
 
-- 
1.8.5.3

