Author: Sam McCall Date: 2023-06-26T21:16:25+02:00 New Revision: d85c233e4b05497a6d8c6e3f2a5fd63d9eeb200d
URL: https://github.com/llvm/llvm-project/commit/d85c233e4b05497a6d8c6e3f2a5fd63d9eeb200d DIFF: https://github.com/llvm/llvm-project/commit/d85c233e4b05497a6d8c6e3f2a5fd63d9eeb200d.diff LOG: [dataflow] Make SAT solver deterministic The SAT solver imported its constraints by iterating over an unordered DenseSet. The path taken, and ultimately the runtime, the specific solution found, and whether it would time out or complete could depend on the iteration order. Instead, have the caller specify an ordered collection of constraints. If this is built in a deterministic way, the system can have deterministic behavior. (The main alternative is to sort the constraints by value, but this option is simpler today). A lot of nondeterminism still appears to be remain in the framework, so today the solver's inputs themselves are not deterministic yet. Differential Revision: https://reviews.llvm.org/D153584 Added: Modified: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h clang/include/clang/Analysis/FlowSensitive/DebugSupport.h clang/include/clang/Analysis/FlowSensitive/Solver.h clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp clang/lib/Analysis/FlowSensitive/DebugSupport.cpp clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp clang/unittests/Analysis/FlowSensitive/SolverTest.cpp Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h index 3a149b5ff397f..eba42fc3418f6 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h +++ b/clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h @@ -25,6 +25,7 @@ #include "clang/Analysis/FlowSensitive/Value.h" #include "llvm/ADT/DenseMap.h" #include "llvm/ADT/DenseSet.h" +#include "llvm/ADT/SetVector.h" #include "llvm/Support/Compiler.h" #include <cassert> #include <memory> @@ -200,7 +201,7 @@ class DataflowAnalysisContext { /// to track tokens of flow conditions that were already visited by recursive /// calls. void addTransitiveFlowConditionConstraints( - AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints, + AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints, llvm::DenseSet<AtomicBoolValue *> &VisitedTokens); /// Returns the outcome of satisfiability checking on `Constraints`. @@ -208,11 +209,11 @@ class DataflowAnalysisContext { /// - `Satisfiable`: A satisfying assignment exists and is returned. /// - `Unsatisfiable`: A satisfying assignment does not exist. /// - `TimedOut`: The search for a satisfying assignment was not completed. - Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints); + Solver::Result querySolver(llvm::SetVector<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) { + bool isUnsatisfiable(llvm::SetVector<BoolValue *> Constraints) { return querySolver(std::move(Constraints)).getStatus() == Solver::Result::Status::Unsatisfiable; } diff --git a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h index ca50ffc5f5c8a..360786b02729f 100644 --- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h +++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h @@ -57,7 +57,7 @@ std::string debugString( /// /// Names assigned to atoms should not be repeated in `AtomNames`. std::string debugString( - const llvm::DenseSet<BoolValue *> &Constraints, + const llvm::ArrayRef<BoolValue *> Constraints, llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}}); /// Returns a string representation for `Constraints` - a collection of boolean @@ -73,14 +73,6 @@ std::string debugString( std::string debugString( ArrayRef<BoolValue *> Constraints, const Solver::Result &Result, llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}}); -inline std::string debugString( - const llvm::DenseSet<BoolValue *> &Constraints, - const Solver::Result &Result, - llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}}) { - std::vector<BoolValue *> ConstraintsVec(Constraints.begin(), - Constraints.end()); - return debugString(ConstraintsVec, Result, std::move(AtomNames)); -} } // namespace dataflow } // namespace clang diff --git a/clang/include/clang/Analysis/FlowSensitive/Solver.h b/clang/include/clang/Analysis/FlowSensitive/Solver.h index e4d450c8d12bb..10964eab8c34c 100644 --- a/clang/include/clang/Analysis/FlowSensitive/Solver.h +++ b/clang/include/clang/Analysis/FlowSensitive/Solver.h @@ -15,9 +15,13 @@ #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H #include "clang/Analysis/FlowSensitive/Value.h" +#include "clang/Basic/LLVM.h" +#include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/DenseMap.h" #include "llvm/ADT/DenseSet.h" +#include "llvm/Support/Compiler.h" #include <optional> +#include <vector> namespace clang { namespace dataflow { @@ -87,7 +91,12 @@ class Solver { /// Requirements: /// /// All elements in `Vals` must not be null. - virtual Result solve(llvm::DenseSet<BoolValue *> Vals) = 0; + virtual Result solve(llvm::ArrayRef<BoolValue *> Vals) = 0; + + LLVM_DEPRECATED("Pass ArrayRef for determinism", "") + virtual Result solve(llvm::DenseSet<BoolValue *> Vals) { + return solve(ArrayRef(std::vector<BoolValue *>(Vals.begin(), Vals.end()))); + } }; } // namespace dataflow diff --git a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h index 5d44e57dbaa99..b69cc01542c55 100644 --- a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h +++ b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h @@ -16,7 +16,7 @@ #include "clang/Analysis/FlowSensitive/Solver.h" #include "clang/Analysis/FlowSensitive/Value.h" -#include "llvm/ADT/DenseSet.h" +#include "llvm/ADT/ArrayRef.h" #include <limits> namespace clang { @@ -46,7 +46,7 @@ class WatchedLiteralsSolver : public Solver { explicit WatchedLiteralsSolver(std::int64_t WorkLimit) : MaxIterations(WorkLimit) {} - Result solve(llvm::DenseSet<BoolValue *> Vals) override; + Result solve(llvm::ArrayRef<BoolValue *> Vals) override; }; } // namespace dataflow diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index 27ec15adc5350..37bcc8be95879 100644 --- a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp +++ b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp @@ -18,6 +18,7 @@ #include "clang/Analysis/FlowSensitive/Logger.h" #include "clang/Analysis/FlowSensitive/Value.h" #include "llvm/ADT/SetOperations.h" +#include "llvm/ADT/SetVector.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Debug.h" #include "llvm/Support/FileSystem.h" @@ -125,11 +126,10 @@ DataflowAnalysisContext::joinFlowConditions(AtomicBoolValue &FirstToken, } Solver::Result -DataflowAnalysisContext::querySolver(llvm::DenseSet<BoolValue *> Constraints) { +DataflowAnalysisContext::querySolver(llvm::SetVector<BoolValue *> Constraints) { Constraints.insert(&arena().makeLiteral(true)); - Constraints.insert( - &arena().makeNot(arena().makeLiteral(false))); - return S->solve(std::move(Constraints)); + Constraints.insert(&arena().makeNot(arena().makeLiteral(false))); + return S->solve(Constraints.getArrayRef()); } bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token, @@ -139,8 +139,9 @@ 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, - &arena().makeNot(Val)}; + llvm::SetVector<BoolValue *> Constraints; + Constraints.insert(&Token); + Constraints.insert(&arena().makeNot(Val)); llvm::DenseSet<AtomicBoolValue *> VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); @@ -149,8 +150,8 @@ bool DataflowAnalysisContext::flowConditionImplies(AtomicBoolValue &Token, 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 = { - &arena().makeNot(Token)}; + llvm::SetVector<BoolValue *> Constraints; + Constraints.insert(&arena().makeNot(Token)); llvm::DenseSet<AtomicBoolValue *> VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); @@ -158,13 +159,13 @@ bool DataflowAnalysisContext::flowConditionIsTautology(AtomicBoolValue &Token) { bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1, BoolValue &Val2) { - llvm::DenseSet<BoolValue *> Constraints = { - &arena().makeNot(arena().makeEquals(Val1, Val2))}; - return isUnsatisfiable(Constraints); + llvm::SetVector<BoolValue*> Constraints; + Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2))); + return isUnsatisfiable(std::move(Constraints)); } void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( - AtomicBoolValue &Token, llvm::DenseSet<BoolValue *> &Constraints, + AtomicBoolValue &Token, llvm::SetVector<BoolValue *> &Constraints, llvm::DenseSet<AtomicBoolValue *> &VisitedTokens) { auto Res = VisitedTokens.insert(&Token); if (!Res.second) @@ -190,14 +191,15 @@ void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token, llvm::raw_ostream &OS) { - llvm::DenseSet<BoolValue *> Constraints = {&Token}; + llvm::SetVector<BoolValue *> Constraints; + Constraints.insert(&Token); llvm::DenseSet<AtomicBoolValue *> VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = { {&arena().makeLiteral(false), "False"}, {&arena().makeLiteral(true), "True"}}; - OS << debugString(Constraints, AtomNames); + OS << debugString(Constraints.getArrayRef(), AtomNames); } const ControlFlowContext * diff --git a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp index 6ac90e3970cc8..25225ed6266fb 100644 --- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -150,17 +150,10 @@ class DebugStringGenerator { return formatv("{0}", fmt_pad(S, Indent, 0)); } - std::string debugString(const llvm::DenseSet<BoolValue *> &Constraints) { - std::vector<std::string> ConstraintsStrings; - ConstraintsStrings.reserve(Constraints.size()); - for (BoolValue *Constraint : Constraints) { - ConstraintsStrings.push_back(debugString(*Constraint)); - } - llvm::sort(ConstraintsStrings); - + std::string debugString(const llvm::ArrayRef<BoolValue *> &Constraints) { std::string Result; - for (const std::string &S : ConstraintsStrings) { - Result += S; + for (const BoolValue *S : Constraints) { + Result += debugString(*S); Result += '\n'; } return Result; @@ -247,7 +240,7 @@ debugString(const BoolValue &B, } std::string -debugString(const llvm::DenseSet<BoolValue *> &Constraints, +debugString(llvm::ArrayRef<BoolValue *> Constraints, llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) { return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints); } diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp index 2943bc5a5b368..db2e1d694457b 100644 --- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp +++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp @@ -20,6 +20,7 @@ #include "clang/Analysis/FlowSensitive/Solver.h" #include "clang/Analysis/FlowSensitive/Value.h" #include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h" +#include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/DenseMap.h" #include "llvm/ADT/DenseSet.h" #include "llvm/ADT/STLExtras.h" @@ -177,7 +178,7 @@ struct BooleanFormula { /// Converts the conjunction of `Vals` into a formula in conjunctive normal /// form where each clause has at least one and at most three literals. -BooleanFormula buildBooleanFormula(const llvm::DenseSet<BoolValue *> &Vals) { +BooleanFormula buildBooleanFormula(const llvm::ArrayRef<BoolValue *> &Vals) { // The general strategy of the algorithm implemented below is to map each // of the sub-values in `Vals` to a unique variable and use these variables in // the resulting CNF expression to avoid exponential blow up. The number of @@ -438,7 +439,7 @@ class WatchedLiteralsSolverImpl { std::vector<Variable> ActiveVars; public: - explicit WatchedLiteralsSolverImpl(const llvm::DenseSet<BoolValue *> &Vals) + explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef<BoolValue *> &Vals) : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1), LevelStates(Formula.LargestVar + 1) { assert(!Vals.empty()); @@ -718,7 +719,7 @@ class WatchedLiteralsSolverImpl { } }; -Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) { +Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef<BoolValue *> Vals) { if (Vals.empty()) return Solver::Result::Satisfiable({{}}); auto [Res, Iterations] = diff --git a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp index 810ba82e4c33d..10fcd204c9ab0 100644 --- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp @@ -187,34 +187,32 @@ TEST(BoolValueDebugStringTest, ComplexBooleanWithSomeNames) { } TEST(ConstraintSetDebugStringTest, Empty) { - llvm::DenseSet<BoolValue *> Constraints; + llvm::ArrayRef<BoolValue *> Constraints; EXPECT_THAT(debugString(Constraints), StrEq("")); } TEST(ConstraintSetDebugStringTest, Simple) { ConstraintContext Ctx; - llvm::DenseSet<BoolValue *> Constraints; + std::vector<BoolValue *> Constraints; auto X = cast<AtomicBoolValue>(Ctx.atom()); auto Y = cast<AtomicBoolValue>(Ctx.atom()); - Constraints.insert(Ctx.disj(X, Y)); - Constraints.insert(Ctx.disj(X, Ctx.neg(Y))); + Constraints.push_back(Ctx.disj(X, Y)); + Constraints.push_back(Ctx.disj(X, Ctx.neg(Y))); auto Expected = R"((or X - (not - Y)) + Y) (or X - Y) + (not + Y)) )"; EXPECT_THAT(debugString(Constraints, {{X, "X"}, {Y, "Y"}}), StrEq(Expected)); } Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) { - llvm::DenseSet<BoolValue *> ConstraintsSet(Constraints.begin(), - Constraints.end()); - return WatchedLiteralsSolver().solve(std::move(ConstraintsSet)); + return WatchedLiteralsSolver().solve(std::move(Constraints)); } TEST(SATCheckDebugStringTest, AtomicBoolean) { diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp index 0a45637d2662e..9999dd3a475f1 100644 --- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp @@ -30,8 +30,8 @@ using testing::UnorderedElementsAre; // Checks if the conjunction of `Vals` is satisfiable and returns the // corresponding result. -Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) { - return WatchedLiteralsSolver().solve(std::move(Vals)); +Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) { + return WatchedLiteralsSolver().solve(Vals); } void expectUnsatisfiable(Solver::Result Result) { _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
