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.
diff --git a/gcc/value-relation.cc b/gcc/value-relation.cc
index 85d159f..13ce441 100644
--- a/gcc/value-relation.cc
+++ b/gcc/value-relation.cc
@@ -184,6 +184,71 @@
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 @@
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 @@
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 478729b..77e1208 100644
--- a/gcc/value-relation.h
+++ b/gcc/value-relation.h
@@ -95,15 +95,19 @@
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
