verify: Bound what a run builds and what its solvers allocate

clang/lib/Verify/Backend/CVC5Backend.cpp

@@ -30,6 +30,7 @@
 #else
 #include <cerrno>
 #include <csignal>
+#include <sys/resource.h>
 #include <sys/wait.h>
 #endif
 
@@ -1505,15 +1506,9 @@ class SMTLibEncoder {
 static VerifyResult querySizeLimitResult(const ObligationModule &Module,
                                          uint64_t MaxQueryNodes,
                                          llvm::StringRef BackendName) {
-  VerifyResult Result;
-  if (MaxQueryNodes == 0 || obligationModuleNodeCount(Module) <= MaxQueryNodes)
-    return Result;
-  Result.Status = VerifyStatus::Unresolved;
-  Result.Reason = VerifyReason::QuerySizeLimit;
-  Result.Message = "canonical obligation module exceeds query node budget " +
-                   std::to_string(MaxQueryNodes);
-  Result.BackendName = BackendName.str();
-  return Result;
+  if (auto Limited = moduleSizeLimit(Module, MaxQueryNodes, BackendName))
+    return std::move(*Limited);
+  return VerifyResult();
 }
 
 static std::optional<std::string>
@@ -2404,7 +2399,8 @@ CVC5VerifyBackend::CVC5VerifyBackend(const BackendExecutionOptions &Execution)
     : TimeoutMs(Execution.SolverTimeoutMs),
       CollectionTimeoutMs(Execution.CollectionTimeoutMs),
       CertifyTimeoutMs(Execution.CertifyTimeoutMs),
-      ResourceLimit(Execution.SolverResourceLimit), Jobs(Execution.Jobs),
+      ResourceLimit(Execution.SolverResourceLimit),
+      MemoryLimitMB(Execution.MemoryLimitMB), Jobs(Execution.Jobs),
       Pool(Execution.Pool), MaxQueryNodes(Execution.MaxQueryNodes),
       IntegerEncoding(Execution.IntegerEncoding) {
   llvm::StringRef Requested = Execution.CVC5Path.empty()
@@ -2431,6 +2427,7 @@ struct SolverRun {
 
 static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
                          unsigned TimeoutMs, unsigned ResourceLimit,
+                         uint64_t MemoryLimitMB = 0,
                          const std::atomic<bool> *Cancelled = nullptr);
 
 /// Whether the cvc5 at \p SolverPath prints a sequence value last element
@@ -2473,6 +2470,7 @@ static bool printsSequencesReversed(const std::string &SolverPath) {
 
 static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
                          unsigned TimeoutMs, unsigned ResourceLimit,
+                         uint64_t MemoryLimitMB,
                          const std::atomic<bool> *Cancelled) {
   SolverRun Run;
   VerifyResult &Result = Run.Failure;
@@ -2530,9 +2528,27 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
                                                 ErrorPath.str()};
   std::string InvocationError;
   bool ExecutionFailed = false;
+  // On Windows the limit bounds the process's committed memory. On POSIX
+  // hosts a limit makes ExecuteNoWait fork rather than spawn, and fork runs
+  // Z3's fork handlers, which wait for the timers of every check running in
+  // the process; the limit is set on the spawned process instead.
+#if defined(_WIN32)
+  const unsigned SpawnLimit = static_cast<unsigned>(
+      std::min<uint64_t>(MemoryLimitMB, std::numeric_limits<unsigned>::max()));
+#else
+  const unsigned SpawnLimit = 0;
+#endif
   llvm::sys::ProcessInfo Process =
-      llvm::sys::ExecuteNoWait(SolverPath, Args, std::nullopt, Redirects, 0,
-                               &InvocationError, &ExecutionFailed);
+      llvm::sys::ExecuteNoWait(SolverPath, Args, std::nullopt, Redirects,
+                               SpawnLimit, &InvocationError, &ExecutionFailed);
+#if defined(__linux__)
+  // What cvc5 allocates: its data segment and private writable mappings.
+  if (MemoryLimitMB != 0 && Process.Pid != llvm::sys::ProcessInfo::InvalidPid) {
+    struct rlimit Data;
+    Data.rlim_cur = Data.rlim_max = static_cast<rlim_t>(MemoryLimitMB) << 20;
+    (void)::prlimit(Process.Pid, RLIMIT_DATA, &Data, nullptr);
+  }
+#endif
   if (ExecutionFailed || Process.Pid == llvm::sys::ProcessInfo::InvalidPid) {
     Result.Reason = VerifyReason::SolverInvocationFailure;
     Result.Message = InvocationError.empty() ? "cannot start cvc5 process"
@@ -2615,16 +2631,33 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script,
     return Run;
   }
   if (ExitCode != 0) {
+    std::string OutputError;
+    std::optional<std::string> StandardOutput =
+        readSolverOutput(OutputPath, OutputError, MaxSolverOutputBytes);
+    // An allocation past the limit fails, and cvc5 reports it as an error
+    // ((error "std::bad_alloc")) or aborts on it (std::bad_alloc, or its SAT
+    // solver's Minisat::OutOfMemoryException).
+    auto outOfMemory = [](llvm::StringRef Text) {
+      return Text.contains("bad_alloc") || Text.contains("OutOfMemory");
+    };
+    if (outOfMemory(*StandardError) ||
+        (StandardOutput && outOfMemory(*StandardOutput))) {
+      Result.Reason = VerifyReason::SolverMemoryLimit;
+      Result.Message = "cvc5 ran out of memory";
+      if (MemoryLimitMB != 0)
+        Result.Message += ": each cvc5 process may use " +
+                          std::to_string(MemoryLimitMB) +
+                          " MB (--memory-limit)";
+      return Run;
+    }
     Result.Reason = VerifyReason::SolverInvocationFailure;
     Result.Message = "cvc5 exited with status " + std::to_string(ExitCode);
     if (!InvocationError.empty())
       Result.Message += ": " + InvocationError;
     if (!StandardError->empty())
       Result.Message += ": " + diagnosticText(*StandardError);
     // cvc5 reports a script it rejects on standard output.
-    std::string OutputError;
-    if (std::optional<std::string> StandardOutput =
-            readSolverOutput(OutputPath, OutputError, MaxSolverOutputBytes))
+    if (StandardOutput)
       for (llvm::StringRef Rest = *StandardOutput; !Rest.empty();) {
         auto [Line, Next] = Rest.split('\n');
         if (Line.trim().starts_with("(error")) {
@@ -2802,8 +2835,8 @@ CVC5VerifyBackend::verifyQuery(const ObligationModule &Module,
       }
       Budget = static_cast<unsigned>(Remaining);
     }
-    SolverRun Run =
-        runCVC5(SolverPath, *Script, Budget, ResourceLimit, &Cancelled);
+    SolverRun Run = runCVC5(SolverPath, *Script, Budget, ResourceLimit,
+                            MemoryLimitMB, &Cancelled);
     auto giveUp = [&](llvm::StringRef Outcome) {
       RefinementDecision Exhausted = Refinement.exhausted(Outcome);
       Result.Reason = Exhausted.Reason;

clang/lib/Verify/Backend/CVC5Backend.h

@@ -30,6 +30,7 @@ class CVC5VerifyBackend : public VerifyBackend {
   /// Set by cancel(): the running process is stopped and no other starts.
   std::atomic<bool> Cancelled{false};
   unsigned ResourceLimit;
+  uint64_t MemoryLimitMB;
   unsigned Jobs;
   llvm::StdThreadPool *Pool;
   std::optional<std::chrono::steady_clock::time_point> Deadline;

clang/lib/Verify/Backend/Obligation.cpp

@@ -1,11 +1,13 @@
 //===--- Obligation.cpp ---------------------------------------------------===//
 #include "LogicTerms.h"
 #include "ObligationLowering.h"
+#include "ObligationSimplify.h"
 #include "SpecAxioms.h"
 #include "llvm/ADT/APInt.h"
 #include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/StringRef.h"
 #include "llvm/Support/Error.h"
+#include "llvm/Support/MathExtras.h"
 #include <algorithm>
 #include <tuple>
 
@@ -2159,7 +2161,8 @@ class ObligationBuilder {
     return std::move(Result);
   }
 
-  llvm::Expected<ObligationModule> buildPassive(const PassiveProgram &P) {
+  llvm::Expected<ObligationModule> buildPassive(const PassiveProgram &P,
+                                                uint64_t MaxNodes) {
     ObligationModule M;
     M.FunctionName = P.FunctionName;
     M.FunctionIdentity = P.FunctionIdentity;
@@ -2272,6 +2275,37 @@ class ObligationBuilder {
       return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s",
                                      ConstructionError.c_str());
 
+    // The goals' size is known before any is built: each is its condition
+    // under a negated copy of every assumption before it (a Not and an Or
+    // each), each query is its goal negated, and the complete goal joins the
+    // goals by And, with its query.
+    uint64_t Prefix = 0, Goals = 0, GoalCount = 0;
+    auto assumed = [&](const VCExpr *Assumption) {
+      Prefix =
+          llvm::SaturatingAdd(Prefix, logicNodeCount(Assumption), uint64_t(2));
+    };
+    auto goal = [&](const VCExpr *Condition) {
+      Goals = llvm::SaturatingAdd(Goals, Prefix, logicNodeCount(Condition));
+      ++GoalCount;
+    };
+    for (const auto &Entry : EntryAssumes)
+      assumed(Entry.get());
+    for (const LoweredStmt &Stmt : Stmts) {
+      if (Stmt.Kind == PassiveStmt::Assume)
+        assumed(Stmt.Cond.get());
+      else
+        goal(Stmt.Cond.get());
+    }
+    for (const auto &Exit : ExitAsserts)
+      goal(std::get<1>(Exit).get());
+    const uint64_t GoalNodes =
+        GoalCount == 0
+            ? 3
+            : llvm::SaturatingAdd(llvm::SaturatingMultiply(Goals, uint64_t(4)),
+                                  3 * GoalCount - 1);
+    if (MaxNodes != 0 && GoalNodes > MaxNodes)
+      return ObligationSizeError::obligations(GoalNodes, MaxNodes);
+
     std::vector<const VCExpr *> Assumptions;
     for (const auto &Entry : EntryAssumes)
       Assumptions.push_back(Entry.get());
@@ -2324,10 +2358,13 @@ class ObligationBuilder {
 
     M.CorrectnessGoal = buildCompleteGoal(M.Obligations);
     M.CounterexampleQuery = vcNot(cloneVCExpr(M.CorrectnessGoal.get()));
+    assert(GoalNodes == obligationModuleNodeCount(M) &&
+           "the goals' size was not predicted exactly");
 
     SpecAxiomContext AxiomContext{P.SpecFunctions, P.SpecFuel, P.HiddenSpecs,
                                   P.RevealedSpecs};
-    if (llvm::Error Error = materializeLogicFunctions(M, AxiomContext))
+    if (llvm::Error Error =
+            materializeLogicFunctions(M, AxiomContext, MaxNodes, GoalNodes))
       return std::move(Error);
 
     auto RequiredFeatures = validateObligationModule(M);
@@ -2588,14 +2625,32 @@ verify::validateObligationModule(const ObligationModule &M) {
   return RequiredFeatures;
 }
 
+char ObligationSizeError::ID = 0;
+
+llvm::Error ObligationSizeError::obligations(uint64_t Nodes, uint64_t Limit) {
+  return llvm::make_error<ObligationSizeError>(
+      "the proof obligations", Nodes, Limit,
+      "each check repeats every assumption before it, so split the function "
+      "or raise the limit");
+}
+
+void ObligationSizeError::log(llvm::raw_ostream &OS) const {
+  OS << What << " would take at least " << Nodes
+     << " expression nodes, more than the limit of " << Limit
+     << " (--max-query-nodes): " << Advice;
+}
+
 llvm::Expected<ObligationModule>
-verify::buildObligationModule(const PassiveProgram &P) {
+verify::buildObligationModule(const PassiveProgram &P, uint64_t MaxNodes) {
   ObligationBuilder B(P.ResultVarName,
                       P.OldHeapName.empty() ? std::string(VHeapName) + "_0"
                                             : P.OldHeapName,
                       P.CallerIntMode, P.HeapVariables,
                       /*ForceCallerMode=*/false, &P.SpecFunctions);
-  auto Module = B.buildPassive(P);
+  if (const auto &Over = P.TooLarge)
+    return llvm::make_error<ObligationSizeError>(Over->What, Over->Nodes,
+                                                 Over->Limit, Over->Advice);
+  auto Module = B.buildPassive(P, MaxNodes);
   if (Module) {
     Module->AssumedPosts = P.AssumedPosts;
     Module->AssumedUnfoldings = P.AssumedUnfoldings;

clang/lib/Verify/Backend/Obligation.h

@@ -3,6 +3,7 @@
 #ifndef LLVM_CLANG_VERIFY_BACKEND_OBLIGATION_H
 #define LLVM_CLANG_VERIFY_BACKEND_OBLIGATION_H
 
+#include "../IR/NodeBudget.h"
 #include "clang/Basic/SourceLocation.h"
 #include "llvm/Support/Error.h"
 #include <cstdint>
@@ -217,7 +218,7 @@ class LogicExpr {
   /// archives.
   std::vector<std::unique_ptr<LogicExpr>> Patterns;
 
-  explicit LogicExpr(Kind K) : K(K) {}
+  explicit LogicExpr(Kind K) : K(K) { NodeBudget::count(); }
 };
 
 // Compatibility name for the Z3/spec adapters while they migrate internally.

clang/lib/Verify/Backend/ObligationLowering.h

@@ -10,8 +10,37 @@
 namespace clang {
 namespace verify {
 
+/// Something a function's verification builds would have more expression
+/// nodes than the limit allows (--max-query-nodes), found before or as it
+/// was built: the obligations, each repeating every assumption before it
+/// (their size is known before any is built), or a spec's definition
+/// unfolded as deep as its fuel.
+class ObligationSizeError : public llvm::ErrorInfo<ObligationSizeError> {
+public:
+  static char ID;
+  ObligationSizeError(std::string What, uint64_t Nodes, uint64_t Limit,
+                      std::string Advice)
+      : What(std::move(What)), Nodes(Nodes), Limit(Limit),
+        Advice(std::move(Advice)) {}
+  /// The obligations of a module of \p Nodes nodes.
+  static llvm::Error obligations(uint64_t Nodes, uint64_t Limit);
+  void log(llvm::raw_ostream &OS) const override;
+  std::error_code convertToErrorCode() const override {
+    return llvm::inconvertibleErrorCode();
+  }
+  std::string What;
+  /// At least this many: a construction stops once it passes the limit.
+  uint64_t Nodes;
+  uint64_t Limit;
+  std::string Advice;
+};
+
+/// With \p MaxNodes, a module that would have more nodes than that (as
+/// obligationModuleNodeCount counts them) is an ObligationSizeError, before
+/// its goals are built. So is a program one of whose constructions passed
+/// its limit (PassiveProgram::TooLarge).
 llvm::Expected<ObligationModule>
-buildObligationModule(const PassiveProgram &Program);
+buildObligationModule(const PassiveProgram &Program, uint64_t MaxNodes = 0);
 
 ObligationKind obligationKind(ProofObligationKind Kind);
 

clang/lib/Verify/Backend/SpecAxioms.cpp

@@ -1,8 +1,10 @@
 //===--- SpecAxioms.cpp - Verus-style spec defining axioms ----------------===//
 #include "SpecAxioms.h"
 #include "../Transform/SpecInline.h"
+#include "LogicTerms.h"
 #include "ObligationLowering.h"
 #include "llvm/Support/Error.h"
+#include "llvm/Support/MathExtras.h"
 
 using namespace clang;
 using namespace verify;
@@ -114,7 +116,9 @@ static const VFunction *findSpecFunction(const FunctionMap &Functions,
 }
 
 llvm::Error verify::materializeLogicFunctions(ObligationModule &Module,
-                                              const SpecAxiomContext &Ctx) {
+                                              const SpecAxiomContext &Ctx,
+                                              uint64_t MaxNodes,
+                                              uint64_t Nodes) {
   // The functions the query reaches; then, for a counterexample check only,
   // those their unfoldings and postconditions apply, where a failure leaves
   // the function out instead of failing the module.
@@ -153,6 +157,20 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module,
         Module.LogicFunctions.try_emplace(Identity, std::move(Declaration));
     (void)Inserted;
     LogicFunctionDecl &Owned = It->second;
+    // Its definitions join the module's nodes once all are lowered.
+    uint64_t Own = 0;
+    auto count = [&](const LogicExpr *Definition) -> llvm::Error {
+      Own = llvm::SaturatingAdd(Own, logicNodeCount(Definition));
+      const uint64_t Total = llvm::SaturatingAdd(Nodes, Own);
+      if (MaxNodes != 0 && Total > MaxNodes)
+        return llvm::make_error<ObligationSizeError>(
+            "the proof obligations with the definitions of the specs they "
+            "apply",
+            Total, MaxNodes,
+            "lower the fuel cppverify::reveal_with_fuel gives, split the "
+            "function, or raise the limit");
+      return llvm::Error::success();
+    };
     const std::string DefinitionHeap = Spec->ReadsHeap
                                            ? std::string(VSpecHeapName)
                                            : std::string(VHeapName) + "_0";
@@ -223,13 +241,26 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module,
       return llvm::createStringError(
           llvm::inconvertibleErrorCode(),
           "spec step definition result sort mismatch: %s", Spec->Name.c_str());
+    if (llvm::Error Error = count(Owned.StepDefinition.get()))
+      return Error;
     collectReferencedLogicFunctions(Owned.StepDefinition.get(), Pending);
 
     const unsigned MaxDepth =
         Spec->NeedsDecreasesCheck ? Fuel : std::min(Fuel, 1U);
     Owned.DefinitionFuel = MaxDepth;
     for (unsigned Depth = 1; Depth <= MaxDepth; ++Depth) {
-      std::unique_ptr<VExpr> Body = unfoldSpecDefinition(*Spec, Ctx, Depth);
+      std::unique_ptr<VExpr> Body;
+      {
+        NodeBudget Unfolding;
+        Body = unfoldSpecDefinition(*Spec, Ctx, Depth);
+        if (Unfolding.exceeded())
+          return llvm::make_error<ObligationSizeError>(
+              "the definition of " + Spec->Name + " unfolded " +
+                  std::to_string(Depth) + " levels deep",
+              Unfolding.built(), Unfolding.limit(),
+              "lower its fuel (cppverify::reveal_with_fuel), or raise the "
+              "limit");
+      }
       if (!Body)
         continue;
       auto Lowered = lowerLogicExpr(Body.get(), "", DefinitionHeap,
@@ -245,6 +276,8 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module,
         return llvm::createStringError(
             llvm::inconvertibleErrorCode(),
             "spec definition result sort mismatch: %s", Spec->Name.c_str());
+      if (llvm::Error Error = count(Definition.get()))
+        return Error;
       collectReferencedLogicFunctions(Definition.get(), Pending);
       Owned.DefinitionLevels.push_back(std::move(Definition));
     }
@@ -262,6 +295,7 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module,
         Owned.Decreases.push_back(std::move(*Lowered));
       }
     }
+    Nodes = llvm::SaturatingAdd(Nodes, Own);
     return llvm::Error::success();
   };
   std::set<std::string> Pending;