wyt created this revision.
Herald added subscribers: martong, tschuett, xazax.hun.
Herald added a project: All.
wyt requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
Given a set of `Constraints`, `querySolver` adds common background information
across queries (`TrueVal` is always true and `FalseVal` is always false) and
passes the query to the solver.
`checkUnsatisfiable` is a simple wrapper around `querySolver` for checking that
the solver returns an unsatisfiable result.
Depends On D128519 <https://reviews.llvm.org/D128519>
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D128520
Files:
clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -106,6 +106,13 @@
return Token;
}
+Solver::Result
+DataflowAnalysisContext::querySolver(llvm::DenseSet<BoolValue *> Constraints) {
+ Constraints.insert(&getBoolLiteralValue(true));
+ Constraints.insert(&getOrCreateNegation(getBoolLiteralValue(false)));
+ return S->solve(std::move(Constraints));
+}
+
bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
BoolValue &Val) {
// Returns true if and only if truth assignment of the flow condition implies
@@ -113,28 +120,19 @@
// reducing the problem to satisfiability checking. In other words, we
attempt
// to show that assuming `Val` is false makes the constraints induced by the
// flow condition unsatisfiable.
- llvm::DenseSet<BoolValue *> Constraints = {
- &Token,
- &getBoolLiteralValue(true),
- &getOrCreateNegation(getBoolLiteralValue(false)),
- &getOrCreateNegation(Val),
- };
+ llvm::DenseSet<BoolValue *> Constraints = {&Token,
&getOrCreateNegation(Val)};
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
- return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+ return checkUnsatisfiable(std::move(Constraints));
}
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),
- &getOrCreateNegation(getBoolLiteralValue(false)),
- &getOrCreateNegation(Token),
- };
+ llvm::DenseSet<BoolValue *> Constraints = {&getOrCreateNegation(Token)};
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
- return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+ return checkUnsatisfiable(std::move(Constraints));
}
void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -212,6 +212,19 @@
AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
+ /// Returns the result of satisfiability checking on `Constraints`.
+ /// Possible return values are:
+ /// - `Satisfiable`: There exists a satisfying assignment for `Constraints`.
+ /// - `Unsatisfiable`: There is no satisfying assignment for `Constraints`.
+ /// - `TimedOut`: The solver gives up on finding a satisfying assignment.
+ Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
+
+ /// Returns true if the solver is able to prove that there is no satisfying
+ /// assignment for `Constraints`
+ bool checkUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
+ return querySolver(std::move(Constraints)) ==
Solver::Result::Unsatisfiable;
+ }
+
std::unique_ptr<Solver> S;
// Storage for the state of a program.
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
@@ -106,6 +106,13 @@
return Token;
}
+Solver::Result
+DataflowAnalysisContext::querySolver(llvm::DenseSet<BoolValue *> Constraints) {
+ Constraints.insert(&getBoolLiteralValue(true));
+ Constraints.insert(&getOrCreateNegation(getBoolLiteralValue(false)));
+ return S->solve(std::move(Constraints));
+}
+
bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token,
BoolValue &Val) {
// Returns true if and only if truth assignment of the flow condition implies
@@ -113,28 +120,19 @@
// reducing the problem to satisfiability checking. In other words, we attempt
// to show that assuming `Val` is false makes the constraints induced by the
// flow condition unsatisfiable.
- llvm::DenseSet<BoolValue *> Constraints = {
- &Token,
- &getBoolLiteralValue(true),
- &getOrCreateNegation(getBoolLiteralValue(false)),
- &getOrCreateNegation(Val),
- };
+ llvm::DenseSet<BoolValue *> Constraints = {&Token, &getOrCreateNegation(Val)};
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
- return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+ return checkUnsatisfiable(std::move(Constraints));
}
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),
- &getOrCreateNegation(getBoolLiteralValue(false)),
- &getOrCreateNegation(Token),
- };
+ llvm::DenseSet<BoolValue *> Constraints = {&getOrCreateNegation(Token)};
llvm::DenseSet<AtomicBoolValue *> VisitedTokens;
addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens);
- return S->solve(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+ return checkUnsatisfiable(std::move(Constraints));
}
void DataflowAnalysisContext::addTransitiveFlowConditionConstraints(
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
@@ -212,6 +212,19 @@
AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints,
llvm::DenseSet<AtomicBoolValue *> &VisitedTokens);
+ /// Returns the result of satisfiability checking on `Constraints`.
+ /// Possible return values are:
+ /// - `Satisfiable`: There exists a satisfying assignment for `Constraints`.
+ /// - `Unsatisfiable`: There is no satisfying assignment for `Constraints`.
+ /// - `TimedOut`: The solver gives up on finding a satisfying assignment.
+ Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
+
+ /// Returns true if the solver is able to prove that there is no satisfying
+ /// assignment for `Constraints`
+ bool checkUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) {
+ return querySolver(std::move(Constraints)) == Solver::Result::Unsatisfiable;
+ }
+
std::unique_ptr<Solver> S;
// Storage for the state of a program.
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
