|
|
@@ -416,17 +416,18 @@ class FactManager::DataSynonymAndIdEquationFacts {
|
|
|
|
|
|
// See method in FactManager which delegates to this method.
|
|
|
std::vector<const protobufs::DataDescriptor*> GetSynonymsForDataDescriptor(
|
|
|
- const protobufs::DataDescriptor& data_descriptor,
|
|
|
- opt::IRContext* context) const;
|
|
|
+ const protobufs::DataDescriptor& data_descriptor) const;
|
|
|
|
|
|
// See method in FactManager which delegates to this method.
|
|
|
- std::vector<uint32_t> GetIdsForWhichSynonymsAreKnown(
|
|
|
- opt::IRContext* context) const;
|
|
|
+ std::vector<uint32_t> GetIdsForWhichSynonymsAreKnown() const;
|
|
|
|
|
|
// See method in FactManager which delegates to this method.
|
|
|
bool IsSynonymous(const protobufs::DataDescriptor& data_descriptor1,
|
|
|
- const protobufs::DataDescriptor& data_descriptor2,
|
|
|
- opt::IRContext* context) const;
|
|
|
+ const protobufs::DataDescriptor& data_descriptor2) const;
|
|
|
+
|
|
|
+ // See method in FactManager which delegates to this method.
|
|
|
+ void ComputeClosureOfFacts(opt::IRContext* context,
|
|
|
+ uint32_t maximum_equivalence_class_size);
|
|
|
|
|
|
private:
|
|
|
// Adds the synonym |dd1| = |dd2| to the set of managed facts, and recurses
|
|
|
@@ -436,23 +437,10 @@ class FactManager::DataSynonymAndIdEquationFacts {
|
|
|
const protobufs::DataDescriptor& dd2,
|
|
|
opt::IRContext* context);
|
|
|
|
|
|
- // Inspects all known facts and adds corollary facts; e.g. if we know that
|
|
|
- // a.x == b.x and a.y == b.y, where a and b have vec2 type, we can record
|
|
|
- // that a == b holds.
|
|
|
- //
|
|
|
- // This method is expensive, and is thus called on demand: rather than
|
|
|
- // computing the closure of facts each time a data synonym fact is added, we
|
|
|
- // compute the closure only when a data synonym fact is *queried*.
|
|
|
- void ComputeClosureOfFacts(opt::IRContext* context) const;
|
|
|
-
|
|
|
// Records the fact that |dd1| and |dd2| are equivalent, and merges the sets
|
|
|
// of equations that are known about them.
|
|
|
- //
|
|
|
- // This is a const method, despite the fact that it mutates the (mutable)
|
|
|
- // set of facts about data descriptors because it is invoked in a lazy fashion
|
|
|
- // when querying facts.
|
|
|
void MakeEquivalent(const protobufs::DataDescriptor& dd1,
|
|
|
- const protobufs::DataDescriptor& dd2) const;
|
|
|
+ const protobufs::DataDescriptor& dd2);
|
|
|
|
|
|
// Returns true if and only if |dd1| and |dd2| are valid data descriptors
|
|
|
// whose associated data have the same type (modulo integer signedness).
|
|
|
@@ -473,28 +461,17 @@ class FactManager::DataSynonymAndIdEquationFacts {
|
|
|
|
|
|
// The data descriptors that are known to be synonymous with one another are
|
|
|
// captured by this equivalence relation.
|
|
|
- //
|
|
|
- // This member is mutable in order to allow the closure of facts captured by
|
|
|
- // the relation to be computed lazily when a question about data synonym
|
|
|
- // facts is asked.
|
|
|
- mutable EquivalenceRelation<protobufs::DataDescriptor, DataDescriptorHash,
|
|
|
- DataDescriptorEquals>
|
|
|
+ EquivalenceRelation<protobufs::DataDescriptor, DataDescriptorHash,
|
|
|
+ DataDescriptorEquals>
|
|
|
synonymous_;
|
|
|
|
|
|
// When a new synonym fact is added, it may be possible to deduce further
|
|
|
- // synonym facts by computing a closure of all known facts. However, there is
|
|
|
- // no point computing this closure until a question regarding synonym facts is
|
|
|
- // actually asked: if several facts are added in succession with no questions
|
|
|
- // asked in between, we can avoid computing fact closures multiple times.
|
|
|
- //
|
|
|
- // This boolean tracks whether a closure computation is required - i.e.,
|
|
|
- // whether a new fact has been added since the last time such a computation
|
|
|
- // was performed.
|
|
|
- //
|
|
|
- // It is mutable to facilitate having const methods, that provide answers to
|
|
|
- // questions about data synonym facts, triggering closure computation on
|
|
|
- // demand.
|
|
|
- mutable bool closure_computation_required_ = false;
|
|
|
+ // synonym facts by computing a closure of all known facts. However, this is
|
|
|
+ // an expensive operation, so it should be performed sparingly and only there
|
|
|
+ // is some chance of new facts being deduced. This boolean tracks whether a
|
|
|
+ // closure computation is required - i.e., whether a new fact has been added
|
|
|
+ // since the last time such a computation was performed.
|
|
|
+ bool closure_computation_required_ = false;
|
|
|
|
|
|
// Represents a set of equations on data descriptors as a map indexed by
|
|
|
// left-hand-side, mapping a left-hand-side to a set of operations, each of
|
|
|
@@ -503,12 +480,7 @@ class FactManager::DataSynonymAndIdEquationFacts {
|
|
|
// All data descriptors occurring in equations are required to be present in
|
|
|
// the |synonymous_| equivalence relation, and to be their own representatives
|
|
|
// in that relation.
|
|
|
- //
|
|
|
- // It is mutable because a closure computation can be triggered from a const
|
|
|
- // method, and when a closure computation detects that two data descriptors
|
|
|
- // are equivalent it is necessary to merge the equation facts for those data
|
|
|
- // descriptors.
|
|
|
- mutable std::unordered_map<
|
|
|
+ std::unordered_map<
|
|
|
const protobufs::DataDescriptor*,
|
|
|
std::unordered_set<Operation, OperationHash, OperationEquals>>
|
|
|
id_equations_;
|
|
|
@@ -770,7 +742,17 @@ void FactManager::DataSynonymAndIdEquationFacts::AddDataSynonymFactRecursive(
|
|
|
// obj_1[a_1, ..., a_m] == obj_2[b_1, ..., b_n]
|
|
|
// then for each composite index i, we add a fact of the form:
|
|
|
// obj_1[a_1, ..., a_m, i] == obj_2[b_1, ..., b_n, i]
|
|
|
- for (uint32_t i = 0; i < num_composite_elements; i++) {
|
|
|
+ //
|
|
|
+ // However, to avoid adding a large number of synonym facts e.g. in the case
|
|
|
+ // of arrays, we bound the number of composite elements to which this is
|
|
|
+ // applied. Nevertheless, we always add a synonym fact for the final
|
|
|
+ // components, as this may be an interesting edge case.
|
|
|
+
|
|
|
+ // The bound on the number of indices of the composite pair to note as being
|
|
|
+ // synonymous.
|
|
|
+ const uint32_t kCompositeElementBound = 10;
|
|
|
+
|
|
|
+ for (uint32_t i = 0; i < num_composite_elements;) {
|
|
|
std::vector<uint32_t> extended_indices1 =
|
|
|
fuzzerutil::RepeatedFieldToVector(dd1.index());
|
|
|
extended_indices1.push_back(i);
|
|
|
@@ -781,11 +763,21 @@ void FactManager::DataSynonymAndIdEquationFacts::AddDataSynonymFactRecursive(
|
|
|
MakeDataDescriptor(dd1.object(), std::move(extended_indices1)),
|
|
|
MakeDataDescriptor(dd2.object(), std::move(extended_indices2)),
|
|
|
context);
|
|
|
+
|
|
|
+ if (i < kCompositeElementBound - 1 || i == num_composite_elements - 1) {
|
|
|
+ // We have not reached the bound yet, or have already skipped ahead to the
|
|
|
+ // last element, so increment the loop counter as standard.
|
|
|
+ i++;
|
|
|
+ } else {
|
|
|
+ // We have reached the bound, so skip ahead to the last element.
|
|
|
+ assert(i == kCompositeElementBound - 1);
|
|
|
+ i = num_composite_elements - 1;
|
|
|
+ }
|
|
|
}
|
|
|
}
|
|
|
|
|
|
void FactManager::DataSynonymAndIdEquationFacts::ComputeClosureOfFacts(
|
|
|
- opt::IRContext* context) const {
|
|
|
+ opt::IRContext* context, uint32_t maximum_equivalence_class_size) {
|
|
|
// Suppose that obj_1[a_1, ..., a_m] and obj_2[b_1, ..., b_n] are distinct
|
|
|
// data descriptors that describe objects of the same composite type, and that
|
|
|
// the composite type is comprised of k components.
|
|
|
@@ -871,6 +863,13 @@ void FactManager::DataSynonymAndIdEquationFacts::ComputeClosureOfFacts(
|
|
|
synonymous_.GetEquivalenceClassRepresentatives()) {
|
|
|
auto equivalence_class = synonymous_.GetEquivalenceClass(*representative);
|
|
|
|
|
|
+ if (equivalence_class.size() > maximum_equivalence_class_size) {
|
|
|
+ // This equivalence class is larger than the maximum size we are willing
|
|
|
+ // to consider, so we skip it. This potentially leads to missed fact
|
|
|
+ // deductions, but avoids excessive runtime for closure computation.
|
|
|
+ continue;
|
|
|
+ }
|
|
|
+
|
|
|
// Consider every data descriptor in the equivalence class.
|
|
|
for (auto dd1_it = equivalence_class.begin();
|
|
|
dd1_it != equivalence_class.end(); ++dd1_it) {
|
|
|
@@ -1059,7 +1058,7 @@ void FactManager::DataSynonymAndIdEquationFacts::ComputeClosureOfFacts(
|
|
|
|
|
|
void FactManager::DataSynonymAndIdEquationFacts::MakeEquivalent(
|
|
|
const protobufs::DataDescriptor& dd1,
|
|
|
- const protobufs::DataDescriptor& dd2) const {
|
|
|
+ const protobufs::DataDescriptor& dd2) {
|
|
|
// Register the data descriptors if they are not already known to the
|
|
|
// equivalence relation.
|
|
|
for (const auto& dd : {dd1, dd2}) {
|
|
|
@@ -1185,9 +1184,7 @@ bool FactManager::DataSynonymAndIdEquationFacts::
|
|
|
|
|
|
std::vector<const protobufs::DataDescriptor*>
|
|
|
FactManager::DataSynonymAndIdEquationFacts::GetSynonymsForDataDescriptor(
|
|
|
- const protobufs::DataDescriptor& data_descriptor,
|
|
|
- opt::IRContext* context) const {
|
|
|
- ComputeClosureOfFacts(context);
|
|
|
+ const protobufs::DataDescriptor& data_descriptor) const {
|
|
|
if (synonymous_.Exists(data_descriptor)) {
|
|
|
return synonymous_.GetEquivalenceClass(data_descriptor);
|
|
|
}
|
|
|
@@ -1195,9 +1192,8 @@ FactManager::DataSynonymAndIdEquationFacts::GetSynonymsForDataDescriptor(
|
|
|
}
|
|
|
|
|
|
std::vector<uint32_t>
|
|
|
-FactManager::DataSynonymAndIdEquationFacts ::GetIdsForWhichSynonymsAreKnown(
|
|
|
- opt::IRContext* context) const {
|
|
|
- ComputeClosureOfFacts(context);
|
|
|
+FactManager::DataSynonymAndIdEquationFacts::GetIdsForWhichSynonymsAreKnown()
|
|
|
+ const {
|
|
|
std::vector<uint32_t> result;
|
|
|
for (auto& data_descriptor : synonymous_.GetAllKnownValues()) {
|
|
|
if (data_descriptor->index().empty()) {
|
|
|
@@ -1209,10 +1205,7 @@ FactManager::DataSynonymAndIdEquationFacts ::GetIdsForWhichSynonymsAreKnown(
|
|
|
|
|
|
bool FactManager::DataSynonymAndIdEquationFacts::IsSynonymous(
|
|
|
const protobufs::DataDescriptor& data_descriptor1,
|
|
|
- const protobufs::DataDescriptor& data_descriptor2,
|
|
|
- opt::IRContext* context) const {
|
|
|
- const_cast<FactManager::DataSynonymAndIdEquationFacts*>(this)
|
|
|
- ->ComputeClosureOfFacts(context);
|
|
|
+ const protobufs::DataDescriptor& data_descriptor2) const {
|
|
|
return synonymous_.Exists(data_descriptor1) &&
|
|
|
synonymous_.Exists(data_descriptor2) &&
|
|
|
synonymous_.IsEquivalent(data_descriptor1, data_descriptor2);
|
|
|
@@ -1394,31 +1387,27 @@ FactManager::GetConstantUniformFactsAndTypes() const {
|
|
|
return uniform_constant_facts_->GetConstantUniformFactsAndTypes();
|
|
|
}
|
|
|
|
|
|
-std::vector<uint32_t> FactManager::GetIdsForWhichSynonymsAreKnown(
|
|
|
- opt::IRContext* context) const {
|
|
|
- return data_synonym_and_id_equation_facts_->GetIdsForWhichSynonymsAreKnown(
|
|
|
- context);
|
|
|
+std::vector<uint32_t> FactManager::GetIdsForWhichSynonymsAreKnown() const {
|
|
|
+ return data_synonym_and_id_equation_facts_->GetIdsForWhichSynonymsAreKnown();
|
|
|
}
|
|
|
|
|
|
std::vector<const protobufs::DataDescriptor*>
|
|
|
FactManager::GetSynonymsForDataDescriptor(
|
|
|
- const protobufs::DataDescriptor& data_descriptor,
|
|
|
- opt::IRContext* context) const {
|
|
|
+ const protobufs::DataDescriptor& data_descriptor) const {
|
|
|
return data_synonym_and_id_equation_facts_->GetSynonymsForDataDescriptor(
|
|
|
- data_descriptor, context);
|
|
|
+ data_descriptor);
|
|
|
}
|
|
|
|
|
|
std::vector<const protobufs::DataDescriptor*> FactManager::GetSynonymsForId(
|
|
|
- uint32_t id, opt::IRContext* context) const {
|
|
|
- return GetSynonymsForDataDescriptor(MakeDataDescriptor(id, {}), context);
|
|
|
+ uint32_t id) const {
|
|
|
+ return GetSynonymsForDataDescriptor(MakeDataDescriptor(id, {}));
|
|
|
}
|
|
|
|
|
|
bool FactManager::IsSynonymous(
|
|
|
const protobufs::DataDescriptor& data_descriptor1,
|
|
|
- const protobufs::DataDescriptor& data_descriptor2,
|
|
|
- opt::IRContext* context) const {
|
|
|
- return data_synonym_and_id_equation_facts_->IsSynonymous(
|
|
|
- data_descriptor1, data_descriptor2, context);
|
|
|
+ const protobufs::DataDescriptor& data_descriptor2) const {
|
|
|
+ return data_synonym_and_id_equation_facts_->IsSynonymous(data_descriptor1,
|
|
|
+ data_descriptor2);
|
|
|
}
|
|
|
|
|
|
bool FactManager::BlockIsDead(uint32_t block_id) const {
|
|
|
@@ -1463,5 +1452,11 @@ void FactManager::AddFactIdEquation(uint32_t lhs_id, SpvOp opcode,
|
|
|
data_synonym_and_id_equation_facts_->AddFact(fact, context);
|
|
|
}
|
|
|
|
|
|
+void FactManager::ComputeClosureOfFacts(
|
|
|
+ opt::IRContext* ir_context, uint32_t maximum_equivalence_class_size) {
|
|
|
+ data_synonym_and_id_equation_facts_->ComputeClosureOfFacts(
|
|
|
+ ir_context, maximum_equivalence_class_size);
|
|
|
+}
|
|
|
+
|
|
|
} // namespace fuzz
|
|
|
} // namespace spvtools
|