[COMMITTED] Provide a relation verification mechanism.

[COMMITTED] Provide a relation verification mechanism.

[Andrew MacLeod]

[-- Attachment #1: Type: text/plain, Size: 2043 bytes --]

the relation oracle works on a purely symbolic basis. It assumes for 
instance that x == x, along with everything in the equivalency set.

With the coming introduction of floating point ranges, we have 
circumstances beyond the symbol relation which can affect the result.  
If the range of X may contain a NaN, then  x != x.

Within ranger, folding these sorts of things is not much of an issue.  
For x == x when we invoke fold_range (==, range x, range x, VREL_EQ) 
that will be dispatched to the floating point version of 
operator_equal() which first checks if either operand has a Nan, and if 
so, ignores the incoming equality relation.

Although there are no current clients of the relation oracle outside of 
ranger, I see the potential need for a mechanism to validate any 
relation returned by the oracle with specific ranges or ssa-names.  I 
don't *THINK* we need this within ranger yet, but haven't been able to 
convince myself 100% yet :-).

This patch adds 2 new API entry points to the oracle:

   relation_kind validate_relation (relation_kind k, tree ssa1, tree ssa2);
   relation_kind validate_relation (relation_kind k, vrange &op1, vrange 
&op2);

They basically do what ranger currently does, takes the relation and 
checks to see if folding the appropriate expression with the relation 
returns the expected [1, 1]

ie  it tries folding     fold_range (r, EQ_EXPR, op1, op2, VREL_EQ)  and 
returns either VREL_EQ if the result is [1, 1], or VREL_VARYING 
otherwise.  so if op1 or op2 had a NaN, then we'd get VREL_VARYING .   
The ssa-name version simply uses a value of VARYING of the approrate type.

Anyway, Ive tested it on all the integer code by having the oracle 
always validate any relation it returns. which bootstraps with no 
regressions on 86_64-pc-linux-gnu.

The default I have checked in does not actually call these new 
routines.  but they are there when we need them now.

Andrew

PS. It also allows x == x to be registered to the oracle, which use to 
trap for no really good reason.

[-- Attachment #2: 0001-Provide-a-relation-verification-mechanism.patch --]
[-- Type: text/x-patch, Size: 5351 bytes --]

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