From 1d2aa262482fc9b23201200ca82aa3b8659b072e Mon Sep 17 00:00:00 2001
From: Andrew MacLeod <amacleod@redhat.com>
Date: Tue, 5 Jul 2022 10:54:26 -0400
Subject: [PATCH] Provide a relation verification mechanism.

Provide a relation oracle API which validates a relation between 2 ranges.
This allows relation queries that are symbolicly true to be overridden
by range specific information.  ie. x == x is true symbolically, but for
floating point a NaN may invalidate this assumption.

	* value-relation.cc (relation_to_code): New vector.
	(relation_oracle::validate_relation): New.
	(set_relation): Allow ssa1 == ssa2 to be registered.
	* value-relation.h (validate_relation): New prototype.
	(query_relation): Make internal variant protected.
---
 gcc/value-relation.cc | 70 +++++++++++++++++++++++++++++++++++++++++--
 gcc/value-relation.h  | 10 +++++--
 2 files changed, 75 insertions(+), 5 deletions(-)

diff --git a/gcc/value-relation.cc b/gcc/value-relation.cc
index 85d159f5d96..13ce44199f7 100644
--- a/gcc/value-relation.cc
+++ b/gcc/value-relation.cc
@@ -184,6 +184,71 @@ relation_transitive (relation_kind r1, relation_kind r2)
   return rr_transitive_table[r1][r2];
 }
 
+// This vector maps a relation to the equivalent tree code.
+
+tree_code relation_to_code [VREL_LAST + 1] = {
+  ERROR_MARK, ERROR_MARK, LT_EXPR, LE_EXPR, GT_EXPR, GE_EXPR, EQ_EXPR,
+  NE_EXPR };
+
+// This routine validates that a relation can be applied to a specific set of
+// ranges.  In particular, floating point x == x may not be true if the NaN bit
+// is set in the range.  Symbolically the oracle will determine x == x,
+// but specific range instances may override this.
+// To verify, attempt to fold the relation using the supplied ranges.
+// One would expect [1,1] to be returned, anything else means there is something
+// in the range preventing the relation from applying.
+// If there is no mechanism to verify, assume the relation is acceptable.
+
+relation_kind
+relation_oracle::validate_relation (relation_kind rel, vrange &op1, vrange &op2)
+{
+  // If there is no mapping to a tree code, leave the relation as is.
+  tree_code code = relation_to_code [rel];
+  if (code == ERROR_MARK)
+    return rel;
+
+  // Undefined ranges cannot be checked either.
+  if (op1.undefined_p () || op2.undefined_p ())
+    return rel;
+
+  tree t1 = op1.type ();
+  tree t2 = op2.type ();
+
+  // If the range types are not compatible, no relation can exist.
+  if (!range_compatible_p (t1, t2))
+    return VREL_VARYING;
+
+  // If there is no handler, leave the relation as is.
+  range_op_handler handler (code, t1);
+  if (!handler)
+    return rel;
+
+  // If the relation cannot be folded for any reason, leave as is.
+  Value_Range result (boolean_type_node);
+  if (!handler.fold_range (result, boolean_type_node, op1, op2, rel))
+    return rel;
+
+  // The expression op1 REL op2 using REL should fold to [1,1].
+  // Any other result means the relation is not verified to be true.
+  if (result.varying_p () || result.zero_p ())
+    return VREL_VARYING;
+
+  return rel;
+}
+
+// If no range is available, create a varying range for each SSA name and
+// verify.
+
+relation_kind
+relation_oracle::validate_relation (relation_kind rel, tree ssa1, tree ssa2)
+{
+  Value_Range op1, op2;
+  op1.set_varying (TREE_TYPE (ssa1));
+  op2.set_varying (TREE_TYPE (ssa2));
+
+  return validate_relation (rel, op1, op2);
+}
+
 // Given an equivalence set EQUIV, set all the bits in B that are still valid
 // members of EQUIV in basic block BB.
 
@@ -602,7 +667,8 @@ private:
 inline void
 value_relation::set_relation (relation_kind r, tree n1, tree n2)
 {
-  gcc_checking_assert (SSA_NAME_VERSION (n1) != SSA_NAME_VERSION (n2));
+  gcc_checking_assert (SSA_NAME_VERSION (n1) != SSA_NAME_VERSION (n2)
+		       || r == VREL_EQ);
   related = r;
   name1 = n1;
   name2 = n2;
@@ -1199,7 +1265,7 @@ dom_oracle::query_relation (basic_block bb, tree ssa1, tree ssa2)
   if (kind != VREL_VARYING)
     return kind;
 
-  // Query using the equiovalence sets.
+  // Query using the equivalence sets.
   kind = query_relation (bb, equiv1, equiv2);
   return kind;
 }
diff --git a/gcc/value-relation.h b/gcc/value-relation.h
index 478729be0bf..77e12085eea 100644
--- a/gcc/value-relation.h
+++ b/gcc/value-relation.h
@@ -95,15 +95,19 @@ public:
   virtual void register_relation (basic_block, relation_kind, tree, tree) = 0;
   // Query for a relation between two ssa names in a basic block.
   virtual relation_kind query_relation (basic_block, tree, tree) = 0;
-  // Query for a relation between two equivalency stes in a basic block.
-  virtual relation_kind query_relation (basic_block, const_bitmap,
-					const_bitmap) = 0;
+
+  relation_kind validate_relation (relation_kind, tree, tree);
+  relation_kind validate_relation (relation_kind, vrange &, vrange &);
 
   virtual void dump (FILE *, basic_block) const = 0;
   virtual void dump (FILE *) const = 0;
   void debug () const;
 protected:
   void valid_equivs (bitmap b, const_bitmap equivs, basic_block bb);
+  // Query for a relation between two equivalency sets in a basic block.
+  virtual relation_kind query_relation (basic_block, const_bitmap,
+					const_bitmap) = 0;
+  friend class path_oracle;
 };
 
 // This class represents an equivalency set, and contains a link to the next
-- 
2.17.2