Author: Wei Yi Tee Date: 2022-06-25T00:05:43+02:00 New Revision: 42a7ddb428c999229491b0effbb1a4059149fba8
URL: https://github.com/llvm/llvm-project/commit/42a7ddb428c999229491b0effbb1a4059149fba8 DIFF: https://github.com/llvm/llvm-project/commit/42a7ddb428c999229491b0effbb1a4059149fba8.diff LOG: [clang][dataflow] Refactor function that queries the solver for satisfiability checking. 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 Reviewed By: gribozavr2, xazax.hun Differential Revision: https://reviews.llvm.org/D128520 Added: Modified: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h index 9f89b2ff5b831..8a1fc9745b215 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -212,6 +212,19 @@ class DataflowAnalysisContext { 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 isUnsatisfiable(llvm::DenseSet<BoolValue *> Constraints) { + return querySolver(std::move(Constraints)) == Solver::Result::Unsatisfiable; + } + std::unique_ptr<Solver> S; // Storage for the state of a program. diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index 10e7df394f40f..57c8750a67e66 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -108,6 +108,13 @@ DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken, 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 @@ -115,28 +122,19 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token, // 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 isUnsatisfiable(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 isUnsatisfiable(std::move(Constraints)); } void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
