This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rG58abe36ae765: [clang][dataflow] Add flowConditionIsTautology
function (authored by li.zhe.hua).
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D124943/new/
https://reviews.llvm.org/D124943
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
Index: clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ 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
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ 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<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 {
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ 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
Index: clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DataflowAnalysisContextTest.cpp
+++ 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
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ 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<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 {
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ 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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
