This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rGd85c233e4b05: [dataflow] Make SAT solver deterministic
(authored by sammccall).
Changed prior to commit:
https://reviews.llvm.org/D153584?vs=533740&id=534699#toc
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D153584/new/
https://reviews.llvm.org/D153584
Files:
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
Index: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ 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<BoolValue *> Vals) {
- return WatchedLiteralsSolver().solve(std::move(Vals));
+Solver::Result solve(llvm::ArrayRef<BoolValue *> Vals) {
+ return WatchedLiteralsSolver().solve(Vals);
}
void expectUnsatisfiable(Solver::Result Result) {
Index: clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
===================================================================
--- clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
+++ clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp
@@ -187,34 +187,32 @@
}
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) {
Index: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ 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<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 @@
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 @@
}
};
-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] =
Index: clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
+++ clang/lib/Analysis/FlowSensitive/DebugSupport.cpp
@@ -150,17 +150,10 @@
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 @@
}
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);
}
Index: clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/DataflowAnalysisContext.cpp
+++ 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<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 @@
// 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::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::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::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 *
Index: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
+++ 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 @@
explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
: MaxIterations(WorkLimit) {}
- Result solve(llvm::DenseSet<BoolValue *> Vals) override;
+ Result solve(llvm::ArrayRef<BoolValue *> Vals) override;
};
} // namespace dataflow
Index: clang/include/clang/Analysis/FlowSensitive/Solver.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/Solver.h
+++ 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 @@
/// 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
Index: clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DebugSupport.h
+++ 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<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(
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
Index: clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/DataflowAnalysisContext.h
+++ 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 @@
/// 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 @@
/// - `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;
}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
