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 @@ -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 #include @@ -200,7 +201,7 @@ /// to track tokens of flow conditions that were already visited by recursive /// calls. void addTransitiveFlowConditionConstraints( - AtomicBoolValue &Token, llvm::DenseSet &Constraints, + AtomicBoolValue &Token, llvm::SetVector &Constraints, llvm::DenseSet &VisitedTokens); /// Returns the outcome of satisfiability checking on `Constraints`. @@ -208,11 +209,11 @@ /// - `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 Constraints); + Solver::Result querySolver(llvm::SetVector Constraints); /// Returns true if the solver is able to prove that there is no satisfying /// assignment for `Constraints` - bool isUnsatisfiable(llvm::DenseSet Constraints) { + bool isUnsatisfiable(llvm::SetVector 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 --- a/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h +++ b/clang/include/clang/Analysis/FlowSensitive/DebugSupport.h @@ -57,7 +57,7 @@ /// /// Names assigned to atoms should not be repeated in `AtomNames`. std::string debugString( - const llvm::DenseSet &Constraints, + const llvm::ArrayRef Constraints, llvm::DenseMap AtomNames = {{}}); /// Returns a string representation for `Constraints` - a collection of boolean @@ -73,14 +73,6 @@ std::string debugString( ArrayRef Constraints, const Solver::Result &Result, llvm::DenseMap AtomNames = {{}}); -inline std::string debugString( - const llvm::DenseSet &Constraints, - const Solver::Result &Result, - llvm::DenseMap AtomNames = {{}}) { - std::vector 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 --- 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 +#include namespace clang { namespace dataflow { @@ -87,7 +91,12 @@ /// Requirements: /// /// All elements in `Vals` must not be null. - virtual Result solve(llvm::DenseSet Vals) = 0; + virtual Result solve(llvm::ArrayRef Vals) = 0; + + LLVM_DEPRECATED("Pass ArrayRef for determinism", "") + virtual Result solve(llvm::DenseSet Vals) { + return solve(ArrayRef(std::vector(Vals.begin(), Vals.end()))); + } }; } // namespace dataflow diff --git a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h --- 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 namespace clang { @@ -46,7 +46,7 @@ explicit WatchedLiteralsSolver(std::int64_t WorkLimit) : MaxIterations(WorkLimit) {} - Result solve(llvm::DenseSet Vals) override; + Result solve(llvm::ArrayRef Vals) override; }; } // namespace dataflow 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 @@ -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 @@ } Solver::Result -DataflowAnalysisContext::querySolver(llvm::DenseSet Constraints) { +DataflowAnalysisContext::querySolver(llvm::SetVector 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 @@ // 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 Constraints = {&Token, - &arena().makeNot(Val)}; + llvm::SetVector Constraints; + Constraints.insert(&Token); + Constraints.insert(&arena().makeNot(Val)); llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); @@ -149,8 +150,8 @@ 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 = { - &arena().makeNot(Token)}; + llvm::SetVector Constraints; + Constraints.insert(&arena().makeNot(Token)); llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); return isUnsatisfiable(std::move(Constraints)); @@ -158,13 +159,13 @@ bool DataflowAnalysisContext::equivalentBoolValues(BoolValue &Val1, BoolValue &Val2) { - llvm::DenseSet Constraints = { - &arena().makeNot(arena().makeEquals(Val1, Val2))}; - return isUnsatisfiable(Constraints); + llvm::SetVector Constraints; + Constraints.insert(&arena().makeNot(arena().makeEquals(Val1, Val2))); + return isUnsatisfiable(std::move(Constraints)); } void DataflowAnalysisContext::addTransitiveFlowConditionConstraints( - AtomicBoolValue &Token, llvm::DenseSet &Constraints, + AtomicBoolValue &Token, llvm::SetVector &Constraints, llvm::DenseSet &VisitedTokens) { auto Res = VisitedTokens.insert(&Token); if (!Res.second) @@ -190,14 +191,15 @@ void DataflowAnalysisContext::dumpFlowCondition(AtomicBoolValue &Token, llvm::raw_ostream &OS) { - llvm::DenseSet Constraints = {&Token}; + llvm::SetVector Constraints; + Constraints.insert(&Token); llvm::DenseSet VisitedTokens; addTransitiveFlowConditionConstraints(Token, Constraints, VisitedTokens); llvm::DenseMap 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 --- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -150,17 +150,10 @@ return formatv("{0}", fmt_pad(S, Indent, 0)); } - std::string debugString(const llvm::DenseSet &Constraints) { - std::vector ConstraintsStrings; - ConstraintsStrings.reserve(Constraints.size()); - for (BoolValue *Constraint : Constraints) { - ConstraintsStrings.push_back(debugString(*Constraint)); - } - llvm::sort(ConstraintsStrings); - + std::string debugString(const llvm::ArrayRef &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 @@ } std::string -debugString(const llvm::DenseSet &Constraints, +debugString(llvm::ArrayRef Constraints, llvm::DenseMap AtomNames) { return DebugStringGenerator(std::move(AtomNames)).debugString(Constraints); } diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp --- 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 @@ /// 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 &Vals) { +BooleanFormula buildBooleanFormula(const llvm::ArrayRef &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 @@ std::vector ActiveVars; public: - explicit WatchedLiteralsSolverImpl(const llvm::DenseSet &Vals) + explicit WatchedLiteralsSolverImpl(const llvm::ArrayRef &Vals) : Formula(buildBooleanFormula(Vals)), LevelVars(Formula.LargestVar + 1), LevelStates(Formula.LargestVar + 1) { assert(!Vals.empty()); @@ -718,7 +719,7 @@ } }; -Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet Vals) { +Solver::Result WatchedLiteralsSolver::solve(llvm::ArrayRef 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 --- a/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp @@ -187,34 +187,32 @@ } TEST(ConstraintSetDebugStringTest, Empty) { - llvm::DenseSet Constraints; + llvm::ArrayRef Constraints; EXPECT_THAT(debugString(Constraints), StrEq("")); } TEST(ConstraintSetDebugStringTest, Simple) { ConstraintContext Ctx; - llvm::DenseSet Constraints; + std::vector Constraints; auto X = cast(Ctx.atom()); auto Y = cast(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 Constraints) { - llvm::DenseSet 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 --- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp @@ -30,8 +30,8 @@ // Checks if the conjunction of `Vals` is satisfiable and returns the // corresponding result. -Solver::Result solve(llvm::DenseSet Vals) { - return WatchedLiteralsSolver().solve(std::move(Vals)); +Solver::Result solve(llvm::ArrayRef Vals) { + return WatchedLiteralsSolver().solve(Vals); } void expectUnsatisfiable(Solver::Result Result) {