ymandel created this revision.
ymandel added reviewers: kinu, xazax.hun, mboehme, sgatev.
Herald added a subscriber: martong.
Herald added a reviewer: NoQ.
Herald added a project: All.
ymandel requested review of this revision.
Herald added a project: clang.
This patch allows the client of a `WatchedLiteralsSolver` to specify a
computation limit on the use of the solver. After the limit is exhausted, the
SAT solver times out.
Fixes issues #60265.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D152732
Files:
clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.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
@@ -360,4 +360,22 @@
expectUnsatisfiable(solve({XImplY, XAndNotY}));
}
+TEST(SolverTest, LowTimeoutResultsInTimedOut) {
+ WatchedLiteralsSolver solver(10);
+ ConstraintContext Ctx;
+ auto X = Ctx.atom();
+ auto Y = Ctx.atom();
+ auto Z = Ctx.atom();
+ auto W = Ctx.atom();
+
+ // !(X v Y) <=> !X ^ !Y
+ auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y)));
+
+ // !(Z ^ W) <=> !Z v !W
+ auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
+
+ // A ^ B
+ EXPECT_EQ(solver.solve({A, B}).getStatus(), Solver::Result::Status::TimedOut);
+}
+
} // namespace
Index: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
===================================================================
--- clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
+++ clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp
@@ -458,9 +458,15 @@
}
}
- Solver::Result solve() && {
+ // Returns the `Result` and the number of iterations "remaining" from
+ // `MaxIterations` (that is, `MaxIterations` - iterations in this call).
+ std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && {
size_t I = 0;
while (I < ActiveVars.size()) {
+ if (MaxIterations == 0)
+ return std::make_pair(Solver::Result::TimedOut(), 0);
+ --MaxIterations;
+
// Assert that the following invariants hold:
// 1. All active variables are unassigned.
// 2. All active variables form watched literals.
@@ -487,7 +493,7 @@
// If the root level is reached, then all possible assignments lead to
// a conflict.
if (Level == 0)
- return Solver::Result::Unsatisfiable();
+ return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations);
// Otherwise, take the other branch at the most recent level where a
// decision was made.
@@ -544,7 +550,7 @@
++I;
}
}
- return Solver::Result::Satisfiable(buildSolution());
+ return std::make_pair(Solver::Result::Satisfiable(buildSolution()), MaxIterations);
}
private:
@@ -713,8 +719,12 @@
};
Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) {
- return Vals.empty() ? Solver::Result::Satisfiable({{}})
- : WatchedLiteralsSolverImpl(Vals).solve();
+ if (Vals.empty())
+ return Solver::Result::Satisfiable({{}});
+ auto [Res, Iterations] =
+ WatchedLiteralsSolverImpl(Vals).solve(MaxIterations);
+ MaxIterations = Iterations;
+ return Res;
}
} // namespace dataflow
Index: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
+++ clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
@@ -17,6 +17,7 @@
#include "clang/Analysis/FlowSensitive/Solver.h"
#include "clang/Analysis/FlowSensitive/Value.h"
#include "llvm/ADT/DenseSet.h"
+#include <limits>
namespace clang {
namespace dataflow {
@@ -27,7 +28,24 @@
/// single "watched" literal per clause, and uses a set of "active" variables
/// for unit propagation.
class WatchedLiteralsSolver : public Solver {
+ // Count of the iterations of the main loop of the solver. This spans *all*
+ // calls to the underlying solver across the life of this object. It is
+ // reduced with every (non-trivial) call to the solver.
+ //
+ // We give control over the abstract count of iterations instead of concrete
+ // measurements like CPU cycles or time to ensure deterministic results.
+ std::int64_t MaxIterations = std::numeric_limits<std::int64_t>::max();
+
public:
+ WatchedLiteralsSolver() = default;
+
+ // `Work` specifies a computational limit on the solver. Units of "work"
+ // roughly correspond to attempts to assign a value to a single
+ // variable. Since the algorithm is exponential in the number of variables,
+ // this is the most direct (abstract) unit to target.
+ explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
+ : MaxIterations(WorkLimit) {}
+
Result solve(llvm::DenseSet<BoolValue *> Vals) override;
};
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
