[PATCH] D155636: [clang][dataflow] Add function to `WatchedLiteralsSolver` that reports whether the iteration limit has been reached.

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

ymandel created this revision.
ymandel added reviewers: xazax.hun, mboehme.
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 change provides a centralized record of whether the solver is
"exhausted". In general, once the solver is exhausted, further uses do not
produce meaningful conclusions. Clients can use this information, for example,
to choose to discard all results based on the solver, instead of trying to
distinguish those reached before the limit was reached. Providing it at in the
solver avoids the need to propagate it from each callsite to the client of the
solver.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D155636

Files:
  clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
  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
@@ -350,4 +350,23 @@
   EXPECT_EQ(solver.solve({A, B}).getStatus(), Solver::Result::Status::TimedOut);
 }
 
+TEST(SolverTest, ReachedLimitsReflectsTimeouts) {
+  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
+  ASSERT_EQ(solver.solve({A, B}).getStatus(), Solver::Result::Status::TimedOut);
+  EXPECT_TRUE(solver.reachedLimit());
+}
+
 } // namespace
Index: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
===================================================================
--- clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
+++ clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
@@ -47,6 +47,9 @@
       : MaxIterations(WorkLimit) {}
 
   Result solve(llvm::ArrayRef<const Formula *> Vals) override;
+
+  // The solver reached its maximum number of iterations.
+  bool reachedLimit() const { return MaxIterations == 0; }
 };
 
 } // namespace dataflow


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D155636.541709.patch
Type: text/x-patch
Size: 1494 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20230718/91d94ce2/attachment-0001.bin>