[SwayamInSync]

Plan item T7 (fuzz the archive reader). An archive given to --obligation-in is untrusted input, and the reader was tested only with the hand-written mutations of obligation_archive.test. This adds a libFuzzer target, runs it every night, and fixes the crash its first run found.

The bug it found

A product, quotient, or remainder with one operand made replay crash. The validator checked the operand count, and on failure built its error message from both operands anyway (Obligation.cpp, validateLogicNode), reading past the end of the operand vector. Under AddressSanitizer it is a SEGV in IntrusiveRefCntPtr::operator->; in a release build replay printed whatever lay there:

$ cpp-verify --obligation-in=unary.cpv          # on main
error: invalid obligation archive: arithmetic term 17 has result sort bitvector, left sort bitvector, and right sort invalid
$ cpp-verify --obligation-in=unary.cpv          # with this PR
error: invalid obligation archive: malformed obligation term: unexpected operand count

The other cases of the validator check the count before they read an operand; these three now do too. The fuzzer found it within about 7,000 inputs.

The target

clang/tools/cpp-verify-archive-fuzzer/ArchiveFuzzer.cpp states, for any byte string, what replay relies on, and aborts when one does not hold:

• deserializeObligationModules returns an error, or modules that validateObligationModule accepts;
• each module's record reads back as one module whose record is the same bytes, with the same module hash and the same semantic, statement, and query hash for every obligation;
• simplifyObligationModule succeeds on it, and again on its result, which serializes to the same bytes (canonicalization is a fixpoint, as replay's convergence claim needs);
• Z3 and cvc5 lower the canonical module in each machine-integer encoding, and Lean exports it unless it is bounded (Lean replay rejects bounded records first), without a crash. A result other than Lowered is a verdict replay reports, not a broken property.

It is built with add_llvm_fuzzer, as LLVM's fuzzers are: with -DLLVM_USE_SANITIZE_COVERAGE=On and a Clang host it is a libFuzzer binary; otherwise its DummyArchiveFuzzer.cpp main runs the target on the files it is given (llvm::runFuzzerOnInputs), so every build has it and lit runs it.

Nightly CI

.github/workflows/cppverify-fuzz.yml builds the verifier and the target with Clang 18, AddressSanitizer, assertions, and sanitizer coverage, writes an archive for every test program under clang/test/Verify (--lower-only --obligation-out), splits them into records of at most 64 KiB (cppverify-fuzz-seeds.py), and fuzzes for half an hour on every core from those seeds and the corpus earlier nights grew (kept in the Actions cache, merged to its minimal covering set after each run). A crash or a failed property fails the job and uploads the inputs. A pull request that changes the fuzzer or the workflow runs it for five minutes, so this PR runs it.

Testing

• suite/archive_fuzzer.test (new) writes archives of programs with every kind of term (obligation_ir, collections, sequences, inductive_predicates, choose, heap_reading_spec, a BMC archive of bmc_incremental, and a small program with *, /, %), mutates one into a product with one operand (mutate_obligation_archive.py unary-product, new), checks replay's error, and runs the target on all of them. It takes 4 s.
• On main, the UNARY check fails (the message above); with this PR it passes, as does obligation_archive.test.
• Locally, the target built with libFuzzer and ASan from this branch's sources ran from 916 seed records of the test programs' archives (every record of at most 64 KiB) for 40 minutes on 8 workers: about 3.6 million inputs, coverage 8528 edges and 31419 features, no crash and no failed property after the fix. The first run, before the fix, found this bug three times within the first minute.

Docs

• The reference (tooling, the archive section): archives are untrusted input and the reader is fuzzed, with the properties;
• ARCHITECTURE ("Canonical archives and semantic identity", and "Regression and Coverage"), REPO_LAYOUT;
• release notes ("Testing").

Not done

• The fuzzer mutates bytes. A structure-aware mutator, decoding a record, changing a term, and encoding it again, would reach the adapters with valid modules more often; the seeds give it valid modules of every kind meanwhile.