[SwayamInSync]

Plan item T3 (sanitizer builds). Nothing ran the verifier under AddressSanitizer or UndefinedBehaviorSanitizer, though it shares a thread pool, a proof cache, and racing solvers between threads, and parses untrusted archives.

Change

• -DCPPVERIFY_SANITIZER="address;undefined" builds clangVerify and cpp-verify with those sanitizers, beside an uninstrumented LLVM, Clang, and Z3 (-fno-sanitize=vptr,function, since the verifier has no RTTI), as CPPVERIFY_ENABLE_COVERAGE instruments clangVerify alone. A fully sanitized LLVM and Clang take hours to build on a CI runner and slow the suite until its timeouts change verdicts; the code we write is what the sanitizers should check. The sanitized targets do not reuse the libraries' precompiled header, which is built without the sanitizers (DISABLE_PCH_REUSE).
• .github/workflows/cppverify-sanitize.sh BUILD runs every Verify test program through such a build, with --jobs=2, and fails on any sanitizer report. It does not compare verdicts, which lit checks. It sets allow_user_poisoning=0: LLVM's allocators poison memory in the instrumented code's copies of their inline functions, and the uninstrumented libraries then write it (use-after-poison in Preprocessor::RegisterBuiltinMacro).
• .github/workflows/cppverify-sanitizers.yml builds it with Clang 18 every night and runs the script; a pull request that changes the setup runs it, so this PR does.

What the first CI run found: the certifier's stack

The first CI run (40836155635) failed 11 of 465 programs with ASan reports deep inside the counterexample checker's evaluation (Evaluator::eval / evalNode / definition, recursing): spec_proof_functions, clause_proofs, counterexample_confirmation, induction_mutual_recursion, induction_schemes, interrupt, spec_automation, spec_fuel_counterexamples, spec_induction, spec_termination, time_report. With ASan's fake stack off the same programs still crashed, on the real stack: a stack overflow.

The checker runs on a thread of its own with a fixed 256 MiB stack and allows 50,000 nested evaluations (CertifyLimits::Frames), one eval and one evalNode frame each. That fits only while a level is small, and its size depends on the build (-fstack-usage, and ASan's __asan_stack_malloc_N class for the instrumented frame):

Build of Certify.cpp	eval	evalNode	50,000 levels
GCC 14 -O3	176 B	736 B	45 MiB
Clang 18 -O3	216 B	1080 B	63 MiB
Clang 18 -O0	360 B	2744 B	152 MiB
Clang 18 -O3 + ASan	216 B + 512 B	408 B + 8 to 16 KiB	0.4 to 0.8 GiB

ASan gives every local of evalNode, a large switch, its own guarded slot, so 50,000 levels need up to 0.8 GiB. The script's ulimit -s could not help: it sizes the pool's threads, not the checker's.

The fix makes the nesting limit independent of frame sizes, as Clang's runWithSufficientStackSpace and rustc's ensure_sufficient_stack do: the evaluator records where its stack begins, and once half of it is used it continues the evaluation on a fresh stack of the same size (llvm::runOnNewStack), returning to the old one afterwards (Evaluator::evalNodeWithStackSpace). The stack size is now CertifyLimits::StackBytes (256 MiB, as before), so a test can choose it. An optimized build uses at most about 63 MiB for 50,000 levels and never switches, so release behavior is unchanged; an ASan build switches every 128 MiB and reaches the same nesting limit, so its verdicts are the release build's. The evaluation's state is in the Evaluator object, the certifier already ran on a thread of its own, and nothing it uses is thread-local (NodeBudget is not used there).

Testing

• CertifyTest.DeepNestingContinuesOnFreshStacks evaluates a sum nested 10,000 deep with a 1 MiB stack and checks the value. Mutant (never switch stacks): the test crashes with SIGSEGV.
• The sweep of this branch, run locally with a Clang 18 ASan build configured as the workflow configures it, the default 8 MiB stack, and the script as committed: no reports in 466 programs in 299 s on 64 cores. The 11 programs above now reach the nesting limit (the evaluation nesting limit was reached while evaluating odd, as in a release build) instead of crashing. One program dies by design (crash_report_url.cpp, #pragma clang __debug crash).
• Without the fix they crash: on CI (this configuration, before the fix) and locally with an ASan build by Clang 23 (clause_proofs and spec_termination, with ASan's fake stack on or off). The script no longer sets ulimit -s 1048576, which never reached the checker's thread.

Why there is no ThreadSanitizer job

This PR first had a TSan job too. In this setup, with only the verifier instrumented, TSan's runtime failed:

• Its first CI run stopped after 10 minutes of the sweep ("The runner has received a shutdown signal").
• Locally, a TSan run of suite/spec_automation.cpp with --jobs=4 hung for 3 hours. Under gdb, 66 of 69 runs of it failed inside the runtime: 58 with SIGSEGV in TSan's trace lists (tsan_ilist.h Push, from TraceSwitchPartImpl; and in the deadlock detector's removeLock while Z3 unlocks its global parameter mutex), and 8 hung with every worker waiting on TSan's trace locks (TracePartAlloc).

So a TSan run could not tell a race from its runtime's failure. #137 found the cause (the checker's nesting overflows TSan's 64 Ki-frame shadow stack) and adds the job; ARCHITECTURE.md here records only what was observed.

Docs

• The reference (tooling, beside CPPVERIFY_ENABLE_COVERAGE): the option, the script, and why poisoning is off;
• ARCHITECTURE ("Regression and Coverage"): the stack overflow and its fix, and why TSan is not run here;
• release notes ("Testing").