spirv-fuzz: Improve the handling of equation facts (#3281)
The management of equation facts suffered from two problems:
(1) The processing of an equation fact required the data descriptors
used in the equation to be in canonical form. However, during
fact processing it can be deduced that certain data descriptors
are equivalent, causing their equivalence classes to be merged,
and that could cause previously canonical data descriptors to no
longer be canonical.
(2) Related to this, if id equations were known about a canonical data
descriptor dd1, and other id equations known about a different
canonical data descriptor dd2, the equation facts about these data
descriptors were not being merged in the event that dd1 and dd2
were deduced to be equivalent.
This changes solves (1) by not requiring equation facts to be in
canonical form while processing them, but instead always checking
whether (not necessary canonical) data descriptors are equivalent when
looking for corollaries of equation facts, rather than comparing them
using ==.
Problem (2) is solved by adding logic to merge sets of equations when
data descriptors are made equivalent.
In addition, the change also requires elements to be registered in an
equivalence relation before they can be made equivalent, rather than
being added (if not already present) at the point of being made
equivalent.diff --git a/source/fuzz/equivalence_relation.h b/source/fuzz/equivalence_relation.h
index 7bb8b66..6d0b63e 100644
--- a/source/fuzz/equivalence_relation.h
+++ b/source/fuzz/equivalence_relation.h
@@ -68,17 +68,14 @@
template <typename T, typename PointerHashT, typename PointerEqualsT>
class EquivalenceRelation {
public:
- // Merges the equivalence classes associated with |value1| and |value2|.
- // If any of these values was not previously in the equivalence relation, it
- // is added to the pool of values known to be in the relation.
+ // Requires that |value1| and |value2| are already registered in the
+ // equivalence relation. Merges the equivalence classes associated with
+ // |value1| and |value2|.
void MakeEquivalent(const T& value1, const T& value2) {
- // Register each value if necessary.
- for (auto value : {value1, value2}) {
- if (!Exists(value)) {
- // Register the value in the equivalence relation.
- Register(value);
- }
- }
+ assert(Exists(value1) &&
+ "Precondition: value1 must already be registered.");
+ assert(Exists(value2) &&
+ "Precondition: value2 must already be registered.");
// Look up canonical pointers to each of the values in the value pool.
const T* value1_ptr = *value_set_.find(&value1);
@@ -105,7 +102,7 @@
// Requires that |value| is not known to the equivalence relation. Registers
// it in its own equivalence class and returns a pointer to the equivalence
// class representative.
- const T* Register(T& value) {
+ const T* Register(const T& value) {
assert(!Exists(value));
// This relies on T having a copy constructor.
diff --git a/source/fuzz/fact_manager.cpp b/source/fuzz/fact_manager.cpp
index 31d3b94..7901341 100644
--- a/source/fuzz/fact_manager.cpp
+++ b/source/fuzz/fact_manager.cpp
@@ -445,6 +445,15 @@
// 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;
+
// Returns true if and only if |dd1| and |dd2| are valid data descriptors
// whose associated data have the same type (modulo integer signedness).
bool DataDescriptorsAreWellFormedAndComparable(
@@ -452,10 +461,11 @@
const protobufs::DataDescriptor& dd2) const;
// Requires that |lhs_dd| and every element of |rhs_dds| is present in the
- // |synonymous_| equivalence relation and is its own representative. Records
- // the fact that the equation "|lhs_dd| |opcode| |rhs_dds|" holds, and adds
- // any corollaries, in the form of data synonym or equation facts, that
- // follow from this and other known facts.
+ // |synonymous_| equivalence relation, but is not necessarily its own
+ // representative. Records the fact that the equation
+ // "|lhs_dd| |opcode| |rhs_dds_non_canonical|" holds, and adds any
+ // corollaries, in the form of data synonym or equation facts, that follow
+ // from this and other known facts.
void AddEquationFactRecursive(
const protobufs::DataDescriptor& lhs_dd, SpvOp opcode,
const std::vector<const protobufs::DataDescriptor*>& rhs_dds,
@@ -493,7 +503,12 @@
// 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.
- std::unordered_map<
+ //
+ // 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<
const protobufs::DataDescriptor*,
std::unordered_set<Operation, OperationHash, OperationEquals>>
id_equations_;
@@ -510,12 +525,10 @@
const protobufs::FactIdEquation& fact, opt::IRContext* context) {
protobufs::DataDescriptor lhs_dd = MakeDataDescriptor(fact.lhs_id(), {});
- // Register the LHS in the equivalence relation if needed, and get a pointer
- // to its representative.
+ // Register the LHS in the equivalence relation if needed.
if (!synonymous_.Exists(lhs_dd)) {
synonymous_.Register(lhs_dd);
}
- const protobufs::DataDescriptor* lhs_dd_ptr = synonymous_.Find(&lhs_dd);
// Get equivalence class representatives for all ids used on the RHS of the
// equation.
@@ -529,10 +542,9 @@
}
rhs_dd_ptrs.push_back(synonymous_.Find(&rhs_dd));
}
- // We now have the equation in a form where it refers exclusively to
- // equivalence class representatives. Add it to our set of facts and work
- // out any follow-on facts.
- AddEquationFactRecursive(*lhs_dd_ptr, static_cast<SpvOp>(fact.opcode()),
+
+ // Now add the fact.
+ AddEquationFactRecursive(lhs_dd, static_cast<SpvOp>(fact.opcode()),
rhs_dd_ptrs, context);
}
@@ -540,27 +552,27 @@
const protobufs::DataDescriptor& lhs_dd, SpvOp opcode,
const std::vector<const protobufs::DataDescriptor*>& rhs_dds,
opt::IRContext* context) {
- // Precondition: all data descriptors referenced in this equation must be
- // equivalence class representatives - i.e. the equation must be in canonical
- // form.
- assert(synonymous_.Exists(lhs_dd));
- assert(synonymous_.Find(&lhs_dd) == &lhs_dd);
+ assert(synonymous_.Exists(lhs_dd) &&
+ "The LHS must be known to the equivalence relation.");
for (auto rhs_dd : rhs_dds) {
- (void)(rhs_dd); // Keep compilers happy in release mode.
- assert(synonymous_.Exists(*rhs_dd));
- assert(synonymous_.Find(rhs_dd) == rhs_dd);
+ // Keep release compilers happy.
+ (void)(rhs_dd);
+ assert(synonymous_.Exists(*rhs_dd) &&
+ "The RHS operands must be known to the equivalence relation.");
}
- if (id_equations_.count(&lhs_dd) == 0) {
+ auto lhs_dd_representative = synonymous_.Find(&lhs_dd);
+
+ if (id_equations_.count(lhs_dd_representative) == 0) {
// We have not seen an equation with this LHS before, so associate the LHS
// with an initially empty set.
id_equations_.insert(
- {&lhs_dd,
+ {lhs_dd_representative,
std::unordered_set<Operation, OperationHash, OperationEquals>()});
}
{
- auto existing_equations = id_equations_.find(&lhs_dd);
+ auto existing_equations = id_equations_.find(lhs_dd_representative);
assert(existing_equations != id_equations_.end() &&
"A set of operations should be present, even if empty.");
@@ -584,13 +596,15 @@
for (auto equation : existing_first_operand_equations->second) {
if (equation.opcode == SpvOpISub) {
// Equation form: "a = (d - e) + c"
- if (equation.operands[1] == rhs_dds[1]) {
+ if (synonymous_.IsEquivalent(*equation.operands[1],
+ *rhs_dds[1])) {
// Equation form: "a = (d - c) + c"
// We can thus infer "a = d"
AddDataSynonymFactRecursive(lhs_dd, *equation.operands[0],
context);
}
- if (equation.operands[0] == rhs_dds[1]) {
+ if (synonymous_.IsEquivalent(*equation.operands[0],
+ *rhs_dds[1])) {
// Equation form: "a = (c - e) + c"
// We can thus infer "a = -e"
AddEquationFactRecursive(lhs_dd, SpvOpSNegate,
@@ -606,7 +620,8 @@
for (auto equation : existing_second_operand_equations->second) {
if (equation.opcode == SpvOpISub) {
// Equation form: "a = b + (d - e)"
- if (equation.operands[1] == rhs_dds[0]) {
+ if (synonymous_.IsEquivalent(*equation.operands[1],
+ *rhs_dds[0])) {
// Equation form: "a = b + (d - b)"
// We can thus infer "a = d"
AddDataSynonymFactRecursive(lhs_dd, *equation.operands[0],
@@ -626,13 +641,15 @@
for (auto equation : existing_first_operand_equations->second) {
if (equation.opcode == SpvOpIAdd) {
// Equation form: "a = (d + e) - c"
- if (equation.operands[0] == rhs_dds[1]) {
+ if (synonymous_.IsEquivalent(*equation.operands[0],
+ *rhs_dds[1])) {
// Equation form: "a = (c + e) - c"
// We can thus infer "a = e"
AddDataSynonymFactRecursive(lhs_dd, *equation.operands[1],
context);
}
- if (equation.operands[1] == rhs_dds[1]) {
+ if (synonymous_.IsEquivalent(*equation.operands[1],
+ *rhs_dds[1])) {
// Equation form: "a = (d + c) - c"
// We can thus infer "a = d"
AddDataSynonymFactRecursive(lhs_dd, *equation.operands[0],
@@ -642,7 +659,8 @@
if (equation.opcode == SpvOpISub) {
// Equation form: "a = (d - e) - c"
- if (equation.operands[0] == rhs_dds[1]) {
+ if (synonymous_.IsEquivalent(*equation.operands[0],
+ *rhs_dds[1])) {
// Equation form: "a = (c - e) - c"
// We can thus infer "a = -e"
AddEquationFactRecursive(lhs_dd, SpvOpSNegate,
@@ -659,13 +677,15 @@
for (auto equation : existing_second_operand_equations->second) {
if (equation.opcode == SpvOpIAdd) {
// Equation form: "a = b - (d + e)"
- if (equation.operands[0] == rhs_dds[0]) {
+ if (synonymous_.IsEquivalent(*equation.operands[0],
+ *rhs_dds[0])) {
// Equation form: "a = b - (b + e)"
// We can thus infer "a = -e"
AddEquationFactRecursive(lhs_dd, SpvOpSNegate,
{equation.operands[1]}, context);
}
- if (equation.operands[1] == rhs_dds[0]) {
+ if (synonymous_.IsEquivalent(*equation.operands[1],
+ *rhs_dds[0])) {
// Equation form: "a = b - (d + b)"
// We can thus infer "a = -d"
AddEquationFactRecursive(lhs_dd, SpvOpSNegate,
@@ -674,7 +694,8 @@
}
if (equation.opcode == SpvOpISub) {
// Equation form: "a = b - (d - e)"
- if (equation.operands[0] == rhs_dds[0]) {
+ if (synonymous_.IsEquivalent(*equation.operands[0],
+ *rhs_dds[0])) {
// Equation form: "a = b - (b - e)"
// We can thus infer "a = e"
AddDataSynonymFactRecursive(lhs_dd, *equation.operands[1],
@@ -712,12 +733,7 @@
assert(DataDescriptorsAreWellFormedAndComparable(context, dd1, dd2));
// Record that the data descriptors provided in the fact are equivalent.
- synonymous_.MakeEquivalent(dd1, dd2);
- // As we have updated the equivalence relation, we might be able to deduce
- // more facts by performing a closure computation, so we record that such a
- // computation is required; it will be performed next time a method answering
- // a data synonym fact-related question is invoked.
- closure_computation_required_ = true;
+ MakeEquivalent(dd1, dd2);
// We now check whether this is a synonym about composite objects. If it is,
// we can recursively add synonym facts about their associated sub-components.
@@ -1029,10 +1045,7 @@
// synonymous.
assert(DataDescriptorsAreWellFormedAndComparable(
context, dd1_prefix, dd2_prefix));
- synonymous_.MakeEquivalent(dd1_prefix, dd2_prefix);
- // As we have added a new synonym fact, we might benefit from doing
- // another pass over the equivalence relation.
- closure_computation_required_ = true;
+ MakeEquivalent(dd1_prefix, dd2_prefix);
// Now that we know this pair of data descriptors are synonymous,
// there is no point recording how close they are to being
// synonymous.
@@ -1044,6 +1057,84 @@
}
}
+void FactManager::DataSynonymAndIdEquationFacts::MakeEquivalent(
+ const protobufs::DataDescriptor& dd1,
+ const protobufs::DataDescriptor& dd2) const {
+ // Register the data descriptors if they are not already known to the
+ // equivalence relation.
+ for (const auto& dd : {dd1, dd2}) {
+ if (!synonymous_.Exists(dd)) {
+ synonymous_.Register(dd);
+ }
+ }
+
+ if (synonymous_.IsEquivalent(dd1, dd2)) {
+ // The data descriptors are already known to be equivalent, so there is
+ // nothing to do.
+ return;
+ }
+
+ // We must make the data descriptors equivalent, and also make sure any
+ // equation facts known about their representatives are merged.
+
+ // Record the original equivalence class representatives of the data
+ // descriptors.
+ auto dd1_original_representative = synonymous_.Find(&dd1);
+ auto dd2_original_representative = synonymous_.Find(&dd2);
+
+ // Make the data descriptors equivalent.
+ synonymous_.MakeEquivalent(dd1, dd2);
+ // As we have updated the equivalence relation, we might be able to deduce
+ // more facts by performing a closure computation, so we record that such a
+ // computation is required.
+ closure_computation_required_ = true;
+
+ // At this point, exactly one of |dd1_original_representative| and
+ // |dd2_original_representative| will be the representative of the combined
+ // equivalence class. We work out which one of them is still the class
+ // representative and which one is no longer the class representative.
+
+ auto still_representative = synonymous_.Find(dd1_original_representative) ==
+ dd1_original_representative
+ ? dd1_original_representative
+ : dd2_original_representative;
+ auto no_longer_representative =
+ still_representative == dd1_original_representative
+ ? dd2_original_representative
+ : dd1_original_representative;
+
+ assert(no_longer_representative != still_representative &&
+ "The current and former representatives cannot be the same.");
+
+ // We now need to add all equations about |no_longer_representative| to the
+ // set of equations known about |still_representative|.
+
+ // Get the equations associated with |no_longer_representative|.
+ auto no_longer_representative_id_equations =
+ id_equations_.find(no_longer_representative);
+ if (no_longer_representative_id_equations != id_equations_.end()) {
+ // There are some equations to transfer. There might not yet be any
+ // equations about |still_representative|; create an empty set of equations
+ // if this is the case.
+ if (!id_equations_.count(still_representative)) {
+ id_equations_.insert(
+ {still_representative,
+ std::unordered_set<Operation, OperationHash, OperationEquals>()});
+ }
+ auto still_representative_id_equations =
+ id_equations_.find(still_representative);
+ assert(still_representative_id_equations != id_equations_.end() &&
+ "At this point there must be a set of equations.");
+ // Add all the equations known about |no_longer_representative| to the set
+ // of equations known about |still_representative|.
+ still_representative_id_equations->second.insert(
+ no_longer_representative_id_equations->second.begin(),
+ no_longer_representative_id_equations->second.end());
+ }
+ // Delete the no longer-relevant equations about |no_longer_representative|.
+ id_equations_.erase(no_longer_representative);
+}
+
bool FactManager::DataSynonymAndIdEquationFacts::
DataDescriptorsAreWellFormedAndComparable(
opt::IRContext* context, const protobufs::DataDescriptor& dd1,
diff --git a/test/fuzz/equivalence_relation_test.cpp b/test/fuzz/equivalence_relation_test.cpp
index 3f2ea58..280aa3a 100644
--- a/test/fuzz/equivalence_relation_test.cpp
+++ b/test/fuzz/equivalence_relation_test.cpp
@@ -47,6 +47,10 @@
EquivalenceRelation<uint32_t, UInt32Hash, UInt32Equals> relation;
ASSERT_TRUE(relation.GetAllKnownValues().empty());
+ for (uint32_t element = 0; element < 100; element++) {
+ relation.Register(element);
+ }
+
for (uint32_t element = 2; element < 80; element += 2) {
relation.MakeEquivalent(0, element);
relation.MakeEquivalent(element - 1, element + 1);
@@ -123,6 +127,11 @@
EquivalenceRelation<uint32_t, UInt32Hash, UInt32Equals> relation2;
for (uint32_t i = 0; i < 1000; ++i) {
+ relation1.Register(i);
+ relation2.Register(i);
+ }
+
+ for (uint32_t i = 0; i < 1000; ++i) {
if (i >= 10) {
relation1.MakeEquivalent(i, i - 10);
relation2.MakeEquivalent(i, i - 10);
diff --git a/test/fuzz/fact_manager_test.cpp b/test/fuzz/fact_manager_test.cpp
index 2c79f12..625eb72 100644
--- a/test/fuzz/fact_manager_test.cpp
+++ b/test/fuzz/fact_manager_test.cpp
@@ -1373,6 +1373,78 @@
MakeDataDescriptor(23, {}), MakeDataDescriptor(16, {}), context.get()));
}
+TEST(FactManagerTest, EquationAndEquivalenceFacts) {
+ std::string shader = R"(
+ OpCapability Shader
+ %1 = OpExtInstImport "GLSL.std.450"
+ OpMemoryModel Logical GLSL450
+ OpEntryPoint Fragment %12 "main"
+ OpExecutionMode %12 OriginUpperLeft
+ OpSource ESSL 310
+ %2 = OpTypeVoid
+ %3 = OpTypeFunction %2
+ %6 = OpTypeInt 32 1
+ %15 = OpConstant %6 24
+ %16 = OpConstant %6 37
+ %12 = OpFunction %2 None %3
+ %13 = OpLabel
+ %14 = OpISub %6 %15 %16
+ %114 = OpCopyObject %6 %14
+ %17 = OpIAdd %6 %114 %16 ; ==> synonymous(%17, %15)
+ %18 = OpIAdd %6 %16 %114 ; ==> synonymous(%17, %18, %15)
+ %19 = OpISub %6 %114 %15
+ %119 = OpCopyObject %6 %19
+ %20 = OpSNegate %6 %119 ; ==> synonymous(%20, %16)
+ %21 = OpISub %6 %14 %19 ; ==> synonymous(%21, %15)
+ %22 = OpISub %6 %14 %18
+ %220 = OpCopyObject %6 %22
+ %23 = OpSNegate %6 %220 ; ==> synonymous(%23, %16)
+ OpReturn
+ OpFunctionEnd
+ )";
+
+ const auto env = SPV_ENV_UNIVERSAL_1_3;
+ const auto consumer = nullptr;
+ const auto context = BuildModule(env, consumer, shader, kFuzzAssembleOption);
+ ASSERT_TRUE(IsValid(env, context.get()));
+
+ FactManager fact_manager;
+
+ fact_manager.AddFactIdEquation(14, SpvOpISub, {15, 16}, context.get());
+ fact_manager.AddFactDataSynonym(MakeDataDescriptor(114, {}),
+ MakeDataDescriptor(14, {}), context.get());
+ fact_manager.AddFactIdEquation(17, SpvOpIAdd, {114, 16}, context.get());
+
+ ASSERT_TRUE(fact_manager.IsSynonymous(
+ MakeDataDescriptor(17, {}), MakeDataDescriptor(15, {}), context.get()));
+
+ fact_manager.AddFactIdEquation(18, SpvOpIAdd, {16, 114}, context.get());
+
+ ASSERT_TRUE(fact_manager.IsSynonymous(
+ MakeDataDescriptor(18, {}), MakeDataDescriptor(15, {}), context.get()));
+ ASSERT_TRUE(fact_manager.IsSynonymous(
+ MakeDataDescriptor(17, {}), MakeDataDescriptor(18, {}), context.get()));
+
+ fact_manager.AddFactIdEquation(19, SpvOpISub, {14, 15}, context.get());
+ fact_manager.AddFactDataSynonym(MakeDataDescriptor(119, {}),
+ MakeDataDescriptor(19, {}), context.get());
+ fact_manager.AddFactIdEquation(20, SpvOpSNegate, {119}, context.get());
+
+ ASSERT_TRUE(fact_manager.IsSynonymous(
+ MakeDataDescriptor(20, {}), MakeDataDescriptor(16, {}), context.get()));
+
+ fact_manager.AddFactIdEquation(21, SpvOpISub, {14, 19}, context.get());
+ ASSERT_TRUE(fact_manager.IsSynonymous(
+ MakeDataDescriptor(21, {}), MakeDataDescriptor(15, {}), context.get()));
+
+ fact_manager.AddFactIdEquation(22, SpvOpISub, {14, 18}, context.get());
+ fact_manager.AddFactDataSynonym(MakeDataDescriptor(22, {}),
+ MakeDataDescriptor(220, {}), context.get());
+ fact_manager.AddFactIdEquation(23, SpvOpSNegate, {220}, context.get());
+ ASSERT_TRUE(fact_manager.IsSynonymous(
+ MakeDataDescriptor(23, {}), MakeDataDescriptor(16, {}), context.get()));
+}
+
} // namespace
} // namespace fuzz
} // namespace spvtools
diff --git a/test/fuzz/transformation_equation_instruction_test.cpp b/test/fuzz/transformation_equation_instruction_test.cpp
index be9024e..3155b18 100644
--- a/test/fuzz/transformation_equation_instruction_test.cpp
+++ b/test/fuzz/transformation_equation_instruction_test.cpp
@@ -486,6 +486,146 @@
ASSERT_TRUE(IsEqual(env, after_transformation, context.get()));
}
+TEST(TransformationEquationInstructionTest, Miscellaneous1) {
+ std::string shader = R"(
+ OpCapability Shader
+ %1 = OpExtInstImport "GLSL.std.450"
+ OpMemoryModel Logical GLSL450
+ OpEntryPoint Fragment %12 "main"
+ OpExecutionMode %12 OriginUpperLeft
+ OpSource ESSL 310
+ %2 = OpTypeVoid
+ %3 = OpTypeFunction %2
+ %6 = OpTypeInt 32 1
+ %113 = OpConstant %6 24
+ %12 = OpFunction %2 None %3
+ %13 = OpLabel
+ OpReturn
+ OpFunctionEnd
+ )";
+
+ const auto env = SPV_ENV_UNIVERSAL_1_3;
+ const auto consumer = nullptr;
+ const auto context = BuildModule(env, consumer, shader, kFuzzAssembleOption);
+ ASSERT_TRUE(IsValid(env, context.get()));
+
+ FactManager fact_manager;
+ spvtools::ValidatorOptions validator_options;
+ TransformationContext transformation_context(&fact_manager,
+ validator_options);
+
+ protobufs::InstructionDescriptor return_instruction =
+ MakeInstructionDescriptor(13, SpvOpReturn, 0);
+
+ auto transformation1 = TransformationEquationInstruction(
+ 522, SpvOpISub, {113, 113}, return_instruction);
+ ASSERT_TRUE(
+ transformation1.IsApplicable(context.get(), transformation_context));
+ transformation1.Apply(context.get(), &transformation_context);
+ ASSERT_TRUE(IsValid(env, context.get()));
+
+ auto transformation2 = TransformationEquationInstruction(
+ 570, SpvOpIAdd, {522, 113}, return_instruction);
+ ASSERT_TRUE(
+ transformation2.IsApplicable(context.get(), transformation_context));
+ transformation2.Apply(context.get(), &transformation_context);
+ ASSERT_TRUE(IsValid(env, context.get()));
+
+ std::string after_transformation = R"(
+ OpCapability Shader
+ %1 = OpExtInstImport "GLSL.std.450"
+ OpMemoryModel Logical GLSL450
+ OpEntryPoint Fragment %12 "main"
+ OpExecutionMode %12 OriginUpperLeft
+ OpSource ESSL 310
+ %2 = OpTypeVoid
+ %3 = OpTypeFunction %2
+ %6 = OpTypeInt 32 1
+ %113 = OpConstant %6 24
+ %12 = OpFunction %2 None %3
+ %13 = OpLabel
+ %522 = OpISub %6 %113 %113
+ %570 = OpIAdd %6 %522 %113
+ OpReturn
+ OpFunctionEnd
+ )";
+
+ ASSERT_TRUE(transformation_context.GetFactManager()->IsSynonymous(
+ MakeDataDescriptor(570, {}), MakeDataDescriptor(113, {}), context.get()));
+
+ ASSERT_TRUE(IsEqual(env, after_transformation, context.get()));
+}
+
+TEST(TransformationEquationInstructionTest, Miscellaneous2) {
+ std::string shader = R"(
+ OpCapability Shader
+ %1 = OpExtInstImport "GLSL.std.450"
+ OpMemoryModel Logical GLSL450
+ OpEntryPoint Fragment %12 "main"
+ OpExecutionMode %12 OriginUpperLeft
+ OpSource ESSL 310
+ %2 = OpTypeVoid
+ %3 = OpTypeFunction %2
+ %6 = OpTypeInt 32 1
+ %113 = OpConstant %6 24
+ %12 = OpFunction %2 None %3
+ %13 = OpLabel
+ OpReturn
+ OpFunctionEnd
+ )";
+
+ const auto env = SPV_ENV_UNIVERSAL_1_3;
+ const auto consumer = nullptr;
+ const auto context = BuildModule(env, consumer, shader, kFuzzAssembleOption);
+ ASSERT_TRUE(IsValid(env, context.get()));
+
+ FactManager fact_manager;
+ spvtools::ValidatorOptions validator_options;
+ TransformationContext transformation_context(&fact_manager,
+ validator_options);
+
+ protobufs::InstructionDescriptor return_instruction =
+ MakeInstructionDescriptor(13, SpvOpReturn, 0);
+
+ auto transformation1 = TransformationEquationInstruction(
+ 522, SpvOpISub, {113, 113}, return_instruction);
+ ASSERT_TRUE(
+ transformation1.IsApplicable(context.get(), transformation_context));
+ transformation1.Apply(context.get(), &transformation_context);
+ ASSERT_TRUE(IsValid(env, context.get()));
+
+ auto transformation2 = TransformationEquationInstruction(
+ 570, SpvOpIAdd, {522, 113}, return_instruction);
+ ASSERT_TRUE(
+ transformation2.IsApplicable(context.get(), transformation_context));
+ transformation2.Apply(context.get(), &transformation_context);
+ ASSERT_TRUE(IsValid(env, context.get()));
+
+ std::string after_transformation = R"(
+ OpCapability Shader
+ %1 = OpExtInstImport "GLSL.std.450"
+ OpMemoryModel Logical GLSL450
+ OpEntryPoint Fragment %12 "main"
+ OpExecutionMode %12 OriginUpperLeft
+ OpSource ESSL 310
+ %2 = OpTypeVoid
+ %3 = OpTypeFunction %2
+ %6 = OpTypeInt 32 1
+ %113 = OpConstant %6 24
+ %12 = OpFunction %2 None %3
+ %13 = OpLabel
+ %522 = OpISub %6 %113 %113
+ %570 = OpIAdd %6 %522 %113
+ OpReturn
+ OpFunctionEnd
+ )";
+
+ ASSERT_TRUE(transformation_context.GetFactManager()->IsSynonymous(
+ MakeDataDescriptor(570, {}), MakeDataDescriptor(113, {}), context.get()));
+
+ ASSERT_TRUE(IsEqual(env, after_transformation, context.get()));
+}
+
} // namespace
} // namespace fuzz
} // namespace spvtools
