Author: Eric Li Date: 2022-05-05T03:57:43Z New Revision: 58abe36ae7654987f5af793e3e261ac0b43c870b
URL: https://github.com/llvm/llvm-project/commit/58abe36ae7654987f5af793e3e261ac0b43c870b DIFF: https://github.com/llvm/llvm-project/commit/58abe36ae7654987f5af793e3e261ac0b43c870b.diff LOG: [clang][dataflow] Add flowConditionIsTautology function Provide a way for users to check if a flow condition is unconditionally true. Differential Revision: https://reviews.llvm.org/D124943 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 5cf681e4e489c..a762cb9de48bd 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -173,6 +173,10 @@ class DataflowAnalysisContext { /// identified by `Token` imply that `Val` is true. bool flowConditionImplies(AtomicBoolValue &Token, BoolValue &Val); + /// Returns true if and only if the constraints of the flow condition + /// identified by `Token` are always true. + bool flowConditionIsTautology(AtomicBoolValue &Token); + 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 4274fca4e3c14..b29983eed79f9 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -117,6 +117,19 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token, return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable; } +bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) { + // Returns true if and only if we cannot prove that the flow condition can + // ever be false. + llvm::DenseSet<BoolValue *> Constraints = { + &getBoolLiteralValue(true), + &getOrCreateNegationValue(getBoolLiteralValue(false)), + &getOrCreateNegationValue(Token), + }; + llvm::DenseSet<AtomicBoolValue *> VisitedTokens; + addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); + return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable; +} + void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints, llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) const { diff --git a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp index b4b9b169f440e..b8a9ef52504af 100644 --- a/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp @@ -140,4 +140,33 @@ TEST_F(DataflowAnalysisContextTest, JoinFlowConditions) { EXPECT_TRUE(Context.flowConditionImplies(FC3, C3)); } +TEST_F(DataflowAnalysisContextTest, FlowConditionTautologies) { + // Fresh flow condition with empty/no constraints is always true. + auto &FC1 = Context.makeFlowConditionToken(); + EXPECT_TRUE(Context.flowConditionIsTautology(FC1)); + + // Literal `true` is always true. + auto &FC2 = Context.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC2, Context.getBoolLiteralValue(true)); + EXPECT_TRUE(Context.flowConditionIsTautology(FC2)); + + // Literal `false` is never true. + auto &FC3 = Context.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC3, Context.getBoolLiteralValue(false)); + EXPECT_FALSE(Context.flowConditionIsTautology(FC3)); + + // We can't prove that an arbitrary bool A is always true... + auto &C1 = Context.createAtomicBoolValue(); + auto &FC4 = Context.makeFlowConditionToken(); + Context.addFlowConditionConstraint(FC4, C1); + EXPECT_FALSE(Context.flowConditionIsTautology(FC4)); + + // ... but we can prove A || !A is true. + auto &FC5 = Context.makeFlowConditionToken(); + Context.addFlowConditionConstraint( + FC5, Context.getOrCreateDisjunctionValue( + C1, Context.getOrCreateNegationValue(C1))); + EXPECT_TRUE(Context.flowConditionIsTautology(FC5)); +} + } // namespace _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
