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

[Yitzhak Mandelbaum via cfe-commits]

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