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.
This commit is contained in:
Andrew MacLeod 2022-07-05 10:54:26 -04:00
parent c73e8d45ca
commit 1d2aa26248
2 changed files with 75 additions and 5 deletions

View file

@ -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;
}

View file

@ -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