diff options
Diffstat (limited to 'clang/lib')
3 files changed, 24 insertions, 28 deletions
diff --git a/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp b/clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp index 27ec15a..37bcc8b 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 6ac90e3..25225ed 100644 --- a/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp +++ b/clang/lib/Analysis/FlowSensitive/DebugSupport.cpp @@ -150,17 +150,10 @@ public: 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 2943bc5..db2e1d6 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 @@ private: } }; -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] = |