[clang][dataflow] Support limits on the SAT solver to force timeouts.

[ymandel]

Summary

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.

[xazax.hun]

Huge +1, I think most solvers need to have some resource limits in place as the runtime can explode. I am just not 100% what is the best approach here, putting a global limit on the solver instance vs having a limit per query. Any thoughts on that?

[ymandel]

In D152732#4414661, @xazax.hun wrote:

Huge +1, I think most solvers need to have some resource limits in place as the runtime can explode. I am just not 100% what is the best approach here, putting a global limit on the solver instance vs having a limit per query. Any thoughts on that?

Excellent question. Ultimately what matters for a user is the global limit. So, in that sense, a global limit makes sense. But, it also makes it harder (in principle) to pinpoint the problem, because you could have it timeout on a small query right after a large query that was actually responsible for consuming the resources. That said, I'm guessing in practice it's binary, because of the exponential: either a single call exhausts all resources or it barely uses them. I suspect we'll ~never hit the case I described. So, I'm inclined to start global (to keep it simple) and then refine if necessary. As you probably noticed, this patch actually has both -- the user specifies the global limit, but the implementation is local. So, changing this would be easy.

That said, I should note that it's not global for a TU - just for a function, at least given the way we currently implement our clang-tidy checks. So, that seems a reasonable compromise.

WDYT?

[kinu]

LGTM as well, I was initially thinking about having a local limit per query (which could be easier to pinpoint the particular query that explodes), but per-solver instance limit could make sense as a starter too.

[xazax.hun]

In D152732#4414707, @ymandel wrote:

Ultimately what matters for a user is the global limit.

I am not 100% sure about that. While it is true that the user cares about the process not hanging, but global vs local limits can have observable effects on the analysis results. With a global limit, after a query exhausted all the budget, for all intents and purposes we continue the analysis without a solver for the rest of the function and all queries would just time out, even the simple ones. With a local limit, the solver might time out for a couple of queries, but we keep the precision for the simple queries. That being said, it is possible that the scenario where we have a few big queries that blows the solver up but the rest of them are simple just does not happen that much. Also, a local timeout produces less reliable worst case runtime results. This makes me think it might be possible that we want both, but this decision is probably better made when we have some evidence that we actually need both. So, I am ok with committing this as is for now.

[ymandel]

In D152732#4414771, @xazax.hun wrote:

In D152732#4414707, @ymandel wrote:

Ultimately what matters for a user is the global limit.

I am not 100% sure about that. While it is true that the user cares about the process not hanging, but global vs local limits can have observable effects on the analysis results. With a global limit, after a query exhausted all the budget, for all intents and purposes we continue the analysis without a solver for the rest of the function and all queries would just time out, even the simple ones. With a local limit, the solver might time out for a couple of queries, but we keep the precision for the simple queries. That being said, it is possible that the scenario where we have a few big queries that blows the solver up but the rest of them are simple just does not happen that much. Also, a local timeout produces less reliable worst case runtime results. This makes me think it might be possible that we want both, but this decision is probably better made when we have some evidence that we actually need both. So, I am ok with committing this as is for now.

Great! Yes, I think you're right that having both is probably the ideal solution. Let's start here, but that will be an easy step if and when we need it.

[gribozavr2]

clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h

37

Consider renaming to RemainingWorkUnits

42

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

462

Why not add a separate getter for the remaining work amount?

[mboehme]

In D152732#4414707, @ymandel wrote:

In D152732#4414661, @xazax.hun wrote:

Huge +1, I think most solvers need to have some resource limits in place as the runtime can explode. I am just not 100% what is the best approach here, putting a global limit on the solver instance vs having a limit per query. Any thoughts on that?

Excellent question. Ultimately what matters for a user is the global limit. So, in that sense, a global limit makes sense. But, it also makes it harder (in principle) to pinpoint the problem, because you could have it timeout on a small query right after a large query that was actually responsible for consuming the resources. That said, I'm guessing in practice it's binary, because of the exponential: either a single call exhausts all resources or it barely uses them. I suspect we'll ~never hit the case I described. So, I'm inclined to start global (to keep it simple) and then refine if necessary. As you probably noticed, this patch actually has both -- the user specifies the global limit, but the implementation is local. So, changing this would be easy.

I'm a bit late to this discussion but still wanted to chime in.

I would actually argue that a local limit more accurately reflects what we want to limit. The functions we analyze will be distributed across a fairly broad range of size and complexity. It seems reasonable to allow more resources to be used to analyze a large and complex function than a small and simple function, and I think this is aligned with users' expectations. So I think it would be reasonable to allow the analysis to use an amount of resources that's proportional to the number of solve() invocations; we just want to limit the amount of resources consumed in a given solve() invocation.

I do follow your argument that "local versus global" likely won't make much of a difference in practice -- the number of solve() invocations is polynomial in the size of the function (I believe?), and that pales against the exponential blowup that can potentially occur inside solve().

However, I don't follow the argument that you want to "start global (to keep it simple)". I think a "local" limit would be simpler: WatchedLiteralsSolverImpl::solve() wouldn't need to return the final value of its parameter MaxIterations, and WatchedLiteralsSolver::solve() wouldn't need to write that back into its member variable MaxIterations (which would instead be const).

I don't think, in any case, that we should have a global _and_ a local limit -- that would really be overcomplicating things.

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

378

Do we really need such a complex formula to test this? Couldn't we make the formula simpler (can we get as simple as "a && !a"?) and reduce the maximum number of iterations accordingly so we still get a timeout?

[ymandel]

In D152732#4415168, @mboehme wrote:

In D152732#4414707, @ymandel wrote:

In D152732#4414661, @xazax.hun wrote:

Huge +1, I think most solvers need to have some resource limits in place as the runtime can explode. I am just not 100% what is the best approach here, putting a global limit on the solver instance vs having a limit per query. Any thoughts on that?

Excellent question. Ultimately what matters for a user is the global limit. So, in that sense, a global limit makes sense. But, it also makes it harder (in principle) to pinpoint the problem, because you could have it timeout on a small query right after a large query that was actually responsible for consuming the resources. That said, I'm guessing in practice it's binary, because of the exponential: either a single call exhausts all resources or it barely uses them. I suspect we'll ~never hit the case I described. So, I'm inclined to start global (to keep it simple) and then refine if necessary. As you probably noticed, this patch actually has both -- the user specifies the global limit, but the implementation is local. So, changing this would be easy.

I'm a bit late to this discussion but still wanted to chime in.

At a high level, I really don't care much -- I just want one mechanism that works well enough. With that said, here are my (weak) arguments in favor of global vs local. If you feel strongly though, feel free to push back and I'll change it (I have some small things to fix anyhow based on Dmitri's comments) or even just send a patch.

I would actually argue that a local limit more accurately reflects what we want to limit. The functions we analyze will be distributed across a fairly broad range of size and complexity. It seems reasonable to allow more resources to be used to analyze a large and complex function than a small and simple function, and I think this is aligned with users' expectations. So I think it would be reasonable to allow the analysis to use an amount of resources that's proportional to the number of solve() invocations; we just want to limit the amount of resources consumed in a given solve() invocation.

I agree about resource usage, but this is about a ceiling. Like timeouts that we place on our clang-tidy invocations and elsewhere, we're looking for a cap. This lets you cap the total, regardless of size. If you want to account for larger functions, just set the cap higher. I'd say that a local mechanism, then, is basically a way to be more restrictive on smaller functions, which begs the question of: what is the particular benefit?

I do follow your argument that "local versus global" likely won't make much of a difference in practice -- the number of solve() invocations is polynomial in the size of the function (I believe?), and that pales against the exponential blowup that can potentially occur inside solve().

Yeah, that's the key and drives the decision here.

However, I don't follow the argument that you want to "start global (to keep it simple)". I think a "local" limit would be simpler: WatchedLiteralsSolverImpl::solve() wouldn't need to return the final value of its parameter MaxIterations, and WatchedLiteralsSolver::solve() wouldn't need to write that back into its member variable MaxIterations (which would instead be const).

True - the code would be simpler and maybe we should just go by this. What I meant is that it is simpler in terms of tuning, since the user is setting the cap for the function. I find the predictability of a total cap simpler to reason about.

I don't think, in any case, that we should have a global _and_ a local limit -- that would really be overcomplicating things.

I actually think you just made the case for both: these accomplish different things. So, if it turns out we want both global caps (for catastrophes) and function-proportional limits, then two limits make sense. It doesn't make sense at the outset for sure -- just if we need, at which point by definition we need it. :)

clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h

37

I like that. Will do in followup.

42

ack (for followup patch).

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

462

It's a different object -- WatchedLiteralsSolverImpl (here) vs WatchedLiteralsSolver (where the field MaxIterations is located).

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

378

No, I simply copied this from elsewhere. I just wanted an example that had a non trivial number of variables. I think its worth commenting that it's an arbitrary choice, but I don't seen particular value in trying to fine tune this for simplicity. But, if you have some argument for it, by all means.

clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h

 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H
 
 #include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseSet.h"
+#include <limits>
 
 namespace clang {
 namespace dataflow {
 
 /// A SAT solver that is an implementation of Algorithm D from Knuth's The Art
 /// of Computer Programming Volume 4: Satisfiability, Fascicle 6. It is based on
 /// the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, keeps references to a
 /// 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;
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H

clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

explicit WatchedLiteralsSolverImpl(const llvm::DenseSet<BoolValue *> &Vals)
 
     // Initialize the active variables.
     for (Variable Var = Formula.LargestVar; Var != NullVar; --Var) {
       if (isWatched(posLit(Var)) || isWatched(negLit(Var)))
         ActiveVars.push_back(Var);
     }
   }
 
-  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.
       // 3. Unassigned variables that form watched literals are active.
       // FIXME: Consider replacing these with test cases that fail if the any
       // of the invariants is broken. That might not be easy due to the
       // transformations performed by `buildBooleanFormula`.
       assert(activeVarsAreUnassigned());
while (I < ActiveVars.size()) {
 
         // Backtrack and rewind the `Level` until the most recent non-forced
         // assignment.
         reverseForcedMoves();
 
         // 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.
         LevelStates[Level] = State::Forced;
         const Variable Var = LevelVars[Level];
         VarAssignments[Var] = VarAssignments[Var] == Assignment::AssignedTrue
                                   ? Assignment::AssignedFalse
                                   : Assignment::AssignedTrue;
while (I < ActiveVars.size()) {
 
         // This was the last active variable. Repeat the process from the
         // beginning.
         I = 0;
       } else {
         ++I;
       }
     }
-    return Solver::Result::Satisfiable(buildSolution());
+    return std::make_pair(Solver::Result::Satisfiable(buildSolution()), MaxIterations);
   }
 
 private:
   /// Returns a satisfying truth assignment to the atomic values in the boolean
   /// formula.
   llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
   buildSolution() {
     llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution;
for (Literal Lit : watchedLiterals()) {
         continue;
       return false;
     }
     return true;
   }
 };
 
 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
 } // namespace clang

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

TEST(SolverTest, ImplicationConflict) {
   auto Y = Ctx.atom();
   auto *XImplY = Ctx.impl(X, Y);
   auto *XAndNotY = Ctx.conj(X, Ctx.neg(Y));
 
   // X => Y ^ X ^ !Y
   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