diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -203,6 +203,11 @@ /// identified by `Token` are always true. bool flowConditionIsTautology(AtomicBoolValue &Token); + /// Returns true if `Val1` is equivalent to `Val2`. + /// Note: This function doesn't take into account constraints on `Val1` and + /// `Val2` imposed by the flow condition. + bool equivalentBoolValues(BoolValue &Val1, BoolValue &Val2); + private: /// Adds all constraints of the flow condition identified by `Token` and all /// of its transitive dependencies to `Constraints`. `VisitedTokens` is used diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -137,6 +137,13 @@ return isUnsatisfiable(std::move(Constraints)); } +bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1, + BoolValue &Val2) { + llvm::DenseSet Constraints = { + &getOrCreateNegation(getOrCreateIff(Val1, Val2))}; + return isUnsatisfiable(Constraints); +} + void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( AtomicBoolValue &Token, llvm::DenseSet &Constraints, llvm::DenseSet &VisitedTokens) { diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp --- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp @@ -213,4 +213,67 @@ EXPECT_TRUE(Context.flowConditionIsTautology(FC5)); } +TEST_F(DataflowAnalysisContextTest, EquivBoolVals) { + auto &X = Context.createAtomicBoolValue(); + auto &Y = Context.createAtomicBoolValue(); + auto &Z = Context.createAtomicBoolValue(); + auto &True = Context.getBoolLiteralValue(true); + auto &False = Context.getBoolLiteralValue(false); + + // X == X + EXPECT_TRUE(Context.equivalentBoolValues(X, X)); + // X != Y + EXPECT_FALSE(Context.equivalentBoolValues(X, Y)); + + // !X != X + EXPECT_FALSE(Context.equivalentBoolValues(Context.getOrCreateNegation(X), X)); + // !(!X) = X + EXPECT_TRUE(Context.equivalentBoolValues( + Context.getOrCreateNegation(Context.getOrCreateNegation(X)), X)); + + // (X || X) == X + EXPECT_TRUE( + Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, X), X)); + // (X || Y) != X + EXPECT_FALSE( + Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), X)); + // (X || True) == True + EXPECT_TRUE(Context.equivalentBoolValues( + Context.getOrCreateDisjunction(X, True), True)); + // (X || False) == X + EXPECT_TRUE(Context.equivalentBoolValues( + Context.getOrCreateDisjunction(X, False), X)); + + // (X && X) == X + EXPECT_TRUE( + Context.equivalentBoolValues(Context.getOrCreateConjunction(X, X), X)); + // (X && Y) != X + EXPECT_FALSE( + Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y), X)); + // (X && True) == X + EXPECT_TRUE( + Context.equivalentBoolValues(Context.getOrCreateConjunction(X, True), X)); + // (X && False) == False + EXPECT_TRUE(Context.equivalentBoolValues( + Context.getOrCreateConjunction(X, False), False)); + + // (X || Y) == (Y || X) + EXPECT_TRUE( + Context.equivalentBoolValues(Context.getOrCreateDisjunction(X, Y), + Context.getOrCreateDisjunction(Y, X))); + // (X && Y) == (Y && X) + EXPECT_TRUE( + Context.equivalentBoolValues(Context.getOrCreateConjunction(X, Y), + Context.getOrCreateConjunction(Y, X))); + + // ((X || Y) || Z) == (X || (Y || Z)) + EXPECT_TRUE(Context.equivalentBoolValues( + Context.getOrCreateDisjunction(Context.getOrCreateDisjunction(X, Y), Z), + Context.getOrCreateDisjunction(X, Context.getOrCreateDisjunction(Y, Z)))); + // ((X && Y) && Z) == (X && (Y && Z)) + EXPECT_TRUE(Context.equivalentBoolValues( + Context.getOrCreateConjunction(Context.getOrCreateConjunction(X, Y), Z), + Context.getOrCreateConjunction(X, Context.getOrCreateConjunction(Y, Z)))); +} + } // namespace