[clang] 1defa78 - [clang][dataflow] Add function to `WatchedLiteralsSolver` that reports whether the iteration limit has been reached.

[Yitzhak Mandelbaum via cfe-commits]

Author: Yitzhak Mandelbaum
Date: 2023-07-18T21:43:55Z
New Revision: 1defa781243f9d0bc66719465e4de33e9fb7a243

URL: https://github.com/llvm/llvm-project/commit/1defa781243f9d0bc66719465e4de33e9fb7a243
DIFF: https://github.com/llvm/llvm-project/commit/1defa781243f9d0bc66719465e4de33e9fb7a243.diff

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

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.

Differential Revision: https://reviews.llvm.org/D155636

Added: 
    

Modified: 
    clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
    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 a0cdce93c9d470..5448eecf6d41a2 100644
--- a/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
+++ b/clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h
@@ -47,6 +47,9 @@ class WatchedLiteralsSolver : public Solver {
       : 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

diff  --git a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
index ba0a77a910d7c4..28f4adb2d39354 100644
--- a/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
+++ b/clang/unittests/Analysis/FlowSensitive/SolverTest.cpp
@@ -350,4 +350,23 @@ TEST(SolverTest, LowTimeoutResultsInTimedOut) {
   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