Author: Yitzhak Mandelbaum Date: 2023-06-12T18:34:32Z New Revision: b639ebaa8f83dbed8adeae0a178a43d6115c9590
URL: https://github.com/llvm/llvm-project/commit/b639ebaa8f83dbed8adeae0a178a43d6115c9590 DIFF: https://github.com/llvm/llvm-project/commit/b639ebaa8f83dbed8adeae0a178a43d6115c9590.diff LOG: [clang][dataflow] Support limits on the SAT solver to force timeouts. 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. Differential Revision: https://reviews.llvm.org/D152732 Added: Modified: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp clang/unittests/Analysis/FlowSensitive/SolverTest.cpp Removed: ################################################################################ diff --git a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h index 702da97349da9..5d44e57dbaa99 100644 --- a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h +++ b/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 @@ namespace dataflow { /// 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; }; diff --git a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp index caa1ed266c5f2..2943bc5a5b368 100644 --- a/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp +++ b/clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp @@ -458,9 +458,15 @@ class WatchedLiteralsSolverImpl { } } - 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 @@ class WatchedLiteralsSolverImpl { // 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 @@ class WatchedLiteralsSolverImpl { ++I; } } - return Solver::Result::Satisfiable(buildSolution()); + return std::make_pair(Solver::Result::Satisfiable(buildSolution()), MaxIterations); } private: @@ -713,8 +719,12 @@ class WatchedLiteralsSolverImpl { }; 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 diff --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp index b56ad9a201ce5..0a45637d2662e 100644 --- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp +++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp @@ -360,4 +360,22 @@ TEST(SolverTest, ImplicationConflict) { 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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
