sammccall created this revision.
sammccall added reviewers: ymandel, xazax.hun.
Herald added subscribers: martong, mgrang.
Herald added a reviewer: NoQ.
Herald added a project: All.
sammccall requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
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.
Repository:
rG LLVM Github Monorepo
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,8 +15,8 @@
#define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_SOLVER_H
#include "clang/Analysis/FlowSensitive/Value.h"
+#include "llvm/ADT/ArrayRef.h"
#include "llvm/ADT/DenseMap.h"
-#include "llvm/ADT/DenseSet.h"
#include <optional>
namespace clang {
@@ -87,7 +87,7 @@
/// 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;
};
} // 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
