[SwayamInSync]

Nothing bounded the memory of a run. Two constructions grow faster than the program, and the process only stopped when the system killed it:

• Proof obligations. Each obligation's goal is its condition under every assumption before it, so a module grows with its obligations times the assumptions before them. Before verify: Share the subterms of logic terms instead of copying them #64, every goal copied those assumptions: in suite/llvm_uleb128_decoder_exhaustive.cpp, decode_uleb128_length_4 to _11 had modules of 41 to 248 million expression nodes, and the file took about 87 GB and 1655 s. verify: Share the subterms of logic terms instead of copying them #64 made the goals share their assumptions' terms, so a goal now adds three nodes per assumption, whatever the assumption's size. That is still quadratic in the function's length: a function of 800 checks took 13 GB, so one of 1,200 would take about 30 GB. --max-query-nodes existed but was 0 by default, and it was checked only once the module had been built.
• Spec definitions unfolded as deep as their fuel. A spec that applies itself twice doubles with every level. cppverify::reveal_with_fuel(fibo, 18) lowered in 267 s and peaked at 22 GB, and fuel 24 passed 40 GB within 65 s.

Z3 and cvc5 had no memory limit either.

This change bounds each of them. A function that reaches a limit is Unresolved, never a proof or a counterexample, and every function whose proof relies on its contract is Unresolved with callee.contract.

--max-query-nodes: what is built for one function (default 4,000,000 distinct expression nodes; 0 disables it)

• Distinct nodes, counted as they are built. Since verify: Share the subterms of logic terms instead of copying them #64 a node that several terms share takes memory once, so it counts once. NodeBudget (IR/NodeBudget.h) counts the VExpr and LogicExpr nodes built on its thread, against the limit the driver sets for the function.
  • The goals are built in a budget that starts from the distinct nodes of the lowered statements, and they stop with ObligationSizeError once they pass the limit.
  • The facts the passivizer adds at each spec application (postconditions, definitions unfolded as deep as their fuel) are built in a budget. A spent budget leaves PassiveProgram::TooLarge, which makes the build an ObligationSizeError.
  • The definitions SpecAxioms materializes are counted by their distinct nodes, from the module's own count.
  • Inlining specs for BMC is bounded the same way: the spec inliner unfolds nothing more once its budget is spent.
  • obligationModuleNodeCount, which the backends check for modules not built from source (archive replay), counts distinct nodes too.
• What states each term in full is checked as a tree. An SMT-LIB script for cvc5 and an archive record (--obligation-out) write a shared subterm at each of its places, so they are larger than what is built. Each counts the module's complete query and definitions as trees, stopping once past the limit (obligationModuleTreeNodesUpTo). Over it, cvc5's verdict is Unresolved with query.size-limit (its SMT-LIB script would state more than N expression nodes), and the record is an error. Z3 hash-conses terms, and the Lean printer names a shared subterm with a let, so the distinct count bounds them.
• One verdict, never a partial result. The driver reports a size error as the function's verdict, Unresolved with query.size-limit, at the function's declaration. The message says what was too large and what to change:

steps.cpp:1:5: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 427 expression nodes, more than the limit of 400 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit)

• Why 4 million. The largest function of the test suite is iterative_fibonacci in safe_fib.cpp, at 375,000 nodes with the definitions of the specs it applies (11.3 million as trees). The ULEB128 case study takes under 200,000 a function (22.6 million as trees), and the exhaustive decoder's largest function fits too. A node takes about 600 bytes, and Z3's encoding of it about five times that (massif sees the nodes, operator new in this static build, and RSS the rest). So the default lets one function take up to about 12 GB, with ten times the suite's largest function as headroom.
• This design replaces the first version of this PR. The first version predicted the obligations' size before building them, as trees: four times the goals' nodes, checked by an assertion against the built module. After verify: Share the subterms of logic terms instead of copying them #64 that counted far more than a module takes: a function of 400 checks was predicted at 45 million nodes and builds under 2 million.
• Backends and replay. The limit applies under every backend, since it bounds construction. The backend-side checks remain for modules that are not built from source, with the message the obligation module has N expression nodes, more than the limit of M (--max-query-nodes).

--memory-limit=MB: the solvers (default 8192; 0 disables it)

• Z3: its queries together, enforced by cpp-verify. Z3 runs in the process, so its queries share the limit. Every check's watchdog, which already interrupts a check at its time, polls Z3's allocation every 10 ms while a limit is set, and interrupts the check once it is past the limit. The encoder's result is then solver.memory-limit. Z3's own limits are not used:
  • memory_max_size fails whichever allocation passes it, in any context of the process. That includes Z3_mk_context's, which then returns no context, and z3++ dereferences it.
  • The high watermark stops the search where Z3 checks it. On the matching loop below it reported only smt-canceled, and the check freed its memory before returning, so a sample taken after the check could not tell why it stopped.
• The reason test. A check with an explicit memory reason (memout, max. memory, out of memory, as from a failed allocation) is also classified as solver.memory-limit. Following the existing API-error rule, an encoder that ran out reports that and proves nothing.
• cvc5: each process, as RLIMIT_DATA. The limit is set with prlimit once the process is spawned; on Windows, ExecuteNoWait's job object sets it.
  • Passing the limit to ExecuteNoWait on POSIX makes it fork rather than spawn. fork runs Z3's fork handler (scoped_timer::finalize), which waits for the timers of every running check: the fidelity gate's portfolio run hung with four threads in it.
  • When an allocation fails, cvc5 prints (error "std::bad_alloc"), or aborts with std::bad_alloc or its SAT solver's Minisat::OutOfMemoryException. Each of these is solver.memory-limit.
  • macOS applies no such limit to mapped memory, so there cvc5 is not bounded.
• Retry. Under --int-encoding=bitvector, a Z3 query stopped for memory is retried in the integer encoding, as after a timeout.
• Rejected with Lean. --memory-limit joins verify: Reject the solver options with the Lean backend #41's list of solver options, which are errors with Lean export (error: --memory-limit requires a backend that runs an SMT solver). --max-query-nodes leaves that list: it now bounds what is built under every backend, Lean's included.

Results

• The exhaustive decoder at the defaults (its own --jobs=8 --timeout=30000) verifies all 68 functions, lengths 0 to 11 included, in 253 s with a peak of 9.4 GB. Before verify: Share the subterms of logic terms instead of copying them #64 the file took about 87 GB and 1655 s, with length 10 timing out, and the first version of this PR refused lengths 4 to 11 for their size. The test stays UNSUPPORTED (T10): at that memory it is too large for the CI runners.

• reveal_with_fuel(fibo, 40) stops at the default limit in 0.9 s with a peak of 0.44 GB; before this change, fuel 24 took more than 40 GB.

• The matching loop ends at 0.14 GB with --memory-limit=100, against 2 GB at its 20 s timeout without a limit.

Docs

• tooling.rst: a "Memory limits" section with checked examples, matching the time limits section: obligations over a small limit, a deep fuel unfolding, and Z3's limit on a matching loop. It also covers what is counted (distinct nodes, scripts and records as trees), both options' rows, how to choose them, and the cvc5 platform note.
• Book: ch15 gets both flags, and ch16 gets the reasons, in its table and in its paragraph on undecided queries.
• limitations.rst: the size limit.
• DESIGN.md and ARCHITECTURE.md: the mechanism, including why Z3's own limits and a forked cvc5 are not used, and why the size is counted as built.
• Release notes: an entry under "Running cpp-verify", and the new reason under "Data formats".
• The docs checker: one rule, that a function a page says stays unresolved may fail to lower for its size (query.size-limit), since no obligations were built.

Testing

• suite/obligation_size_limit.cpp checks:
  • the refusal, its message and location, and its JSON record;
  • the caller demoted with callee.contract, and a sibling that still verifies;
  • the --lower-only error;
  • the exact boundary: at 1,939 nodes steps verifies, at 1,938 it is refused;
  • at 3,000 nodes, steps is built and proved, though its archive record would state more and is refused;
  • the facts of reveal_with_fuel(fibo, 40) stopping at the limit;
  • obligations plus spec definitions over the limit (2,637 nodes, exact);
  • the default in --help.
• suite/cvc5_script_size.test (new, requires cvc5) checks that cvc5 refuses steps at 3,000 nodes, where its script would state more.
• suite/solver_memory_limit.cpp checks that the matching loop stops at --memory-limit=100 with solver.memory-limit, in text and JSON, and that the next function verifies within the limit. It also checks that --memory-limit with Lean is an error.
• suite/cvc5_memory_limit.cpp (Linux, cvc5) checks that a cvc5 process limited to 5 MB reports solver.memory-limit.
• suite/memory_bounded.test (Linux) runs a 1,200-check function and reveal_with_fuel(fibo, 40) under ulimit -v 3000000. Both end with their verdicts within the address space.
• suite/backend_execution.test now expects the new messages; its --dump-ir=4 run, which builds no module, reports the verdict.

Mutants of the first version, each failing at least one of these tests:

• no size check;
• the size off by one;
• an inliner that ignores the budget;
• the passivizer's overrun not recorded;
• the size error reported as a lowering failure;
• spec definitions not counted;
• a watchdog that ignores memory;
• a memory stop not classified;
• cvc5's out-of-memory not recognized;
• cvc5's limit not applied.

Mutants of this design, each applied alone:

Mutant	Change	Fails
S1	the module is counted as trees	cvc5_script_size.test (and the boundary)
S2	the goals' budget starts from nothing, not from the lowered statements	obligation_size_limit.cpp
S3	the goals are checked only once all are built	memory_bounded.test
S4	the goals' budget stays open over the definitions	obligation_size_limit.cpp
S6	cvc5 scripts are not checked as trees	cvc5_script_size.test
S7	archive records are not checked as trees	obligation_size_limit.cpp
S8	the tree count stops at once	cvc5_script_size.test, obligation_size_limit.cpp
S9	the old default, 32 million	obligation_size_limit.cpp (--help)
S10	the distinct count sees one root	obligation_size_limit.cpp

S9 survived its first run: --help stated the default as a literal. It is now built from DefaultMaxQueryNodes. One mutant survives: S5, the definitions counted as trees. A definition is lowered fresh from its spec's body, and no definition in the suite shares a subterm, so its distinct count is its tree count.

Checked

• This branch has main merged into it (merge commit b782bf0473). The conflicts were:
  • Obligation.cpp: main's assumption origins next to the size check;
  • Passivize.cpp: finish returns nothing now;
  • CVC5Backend.cpp: includes;
  • check-doc-examples.py: main's Lean rule with this PR's size rule;
  • docs.
• lit of clang/test/Verify on the merged tree with this design: 478 passed, 1 unsupported (darwin only), no failure, including docs_examples.test and docs_coverage.test with the new numbers.