Author: Wei Yi Tee Date: 2022-06-25T00:10:35+02:00 New Revision: 0f65a3e610051fc319372eea647fb50f60b2b21c
URL: https://github.com/llvm/llvm-project/commit/0f65a3e610051fc319372eea647fb50f60b2b21c DIFF: https://github.com/llvm/llvm-project/commit/0f65a3e610051fc319372eea647fb50f60b2b21c.diff LOG: [clang][dataflow] Implement functionality to compare if two boolean values are equivalent. `equivalentBoolValues` compares equivalence between two booleans. The current implementation does not consider constraints imposed by flow conditions on the booleans and its subvalues. Depends On D128520 Reviewed By: gribozavr2, xazax.hun Differential Revision: https://reviews.llvm.org/D128521 Added: Modified: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h index 8a1fc9745b21..6011584f2006 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -203,6 +203,11 @@ class DataflowAnalysisContext { /// 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 index 57c8750a67e6..475eeef53737 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -137,6 +137,13 @@ bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) { return isUnsatisfiable(std::move(Constraints)); } +bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1, + BoolValue &Val2) { + llvm::DenseSet<BoolValue *> Constraints = { + &getOrCreateNegation(getOrCreateIff(Val1, Val2))}; + return isUnsatisfiable(Constraints); +} + void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints, llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) { diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp index 1ff7cf1dce9e..1f0116cdbf2e 100644 --- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp @@ -213,4 +213,67 @@ TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) { 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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
