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 @@ -173,6 +173,10 @@ /// 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 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -117,6 +117,19 @@ 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 Constraints = { + &getBoolLiteralValue(true), + &getOrCreateNegationValue(getBoolLiteralValue(false)), + &getOrCreateNegationValue(Token), + }; + llvm::DenseSet VisitedTokens; + addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); + return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable; +} + void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( AtomicBoolValue &Token, llvm::DenseSet &Constraints, llvm::DenseSet &VisitedTokens) const { 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 @@ -140,4 +140,33 @@ 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