Harden check against verdicts the run did not establish

Merged
JS
14d ago
+7611-485

This applies what seven external Frama-C projects (acsl-skills, dawnr, Deadlock_and_Racer, FermatVerification-bench, fragma, seal, VerNFR) taught about ways check could report "proved" for something the run never established, and closes each one that reproduced here.

The two that changed real verdicts: Frama-C 33 defaults -rte-use-eva-results on, so running EVA before WP removed runtime-error goals from every function EVA analyzed (an out-of-bounds write proved 5/5; it is 5/6 now), and a scoped check started EVA from the globals' initializers instead of an unknown state. Fixing the first surfaced a real overflow in tests/fixtures/test_abs.c that EVA had been hiding, and its contract is corrected. The plug-in now invalidates WP's cache after inserting ghost code, which before let run_wp prove the body as it was before the insertion. New incomplete codes and two informational fields say what a proof rested on; docs/design/verdict-hardening/architecture.md has the design, including one rule a Codex review found unsound and that was replaced.

Verified with scripts/run-gates.sh: all 18 gates pass, unit 705/705 and the MCP stdio suite 175/175, against Frama-C 33.0 with Alt-Ergo 2.6.3. Each soundness fix has a test that was confirmed to fail without it. The two intermediate commits build and pass their own tests on their own.

Left out, with their reasons in the design docs: a verdict narrowed by target (established reports the split instead), cross-architecture machdep generation, and a prover memory cap, which needs measuring first.

Summary by cubic

Hardens check so a "proved" verdict can no longer claim more than the run established, and repairs the two adjacent holes that allowed it: the concurrency screen and ghost insertion.

Verdict soundness

  • Frama-C 33 defaults -rte-use-eva-results on; every run now starts with -rte-no-use-eva-results, so EVA can no longer delete WP's runtime-error goals (an out-of-bounds write proved 5/5 before, 5/6 now).
  • That change surfaced a real overflow in tests/fixtures/test_abs.c, whose contract is corrected.
  • A scoped check now runs EVA under -lib-entry from an unknown global state instead of the globals' initializers, and run_wp puts -main and -lib-entry back, failing closed if the reset discards EVA's results.
  • Ghost insertion now invalidates WP's cache, resolves names through the enclosing blocks, and declares ghost locals in their own block; before, an inserted assignment's assertion could be proved against the unmodified body. Every mutating request runs the kernel's Filecheck.
  • check reports the recursive logic definitions WP assumes without a termination check and splits established verdicts by target.
  • New gap codes cover unencoded SV-COMP reachability properties, thread bodies never analyzed, compile flags dropped on database import, missing or unproved pinned properties, decorative contracts and unchecked contract mutants.
  • New opt-in load options rte_pointer and builtin_models, and a WP step budget, enter the proof receipt only when set; sandboxes inherit the project's RTE switches.
  • One-shot Frama-C runs now run in their own process group: they null stdin, wait on the exit, then kill the group, and abort their pipe readers on every path out, so orphaned provers cannot survive a timeout, a finished run is not held open by a pipe, and a failed or truncated read is an error rather than a short buffer.
  • Review fixes: pins unwrap \old only where the printer adds it, pinned admits a stringified array, compile-database flags are split as a shell splits words, and analyze_concurrency is suggested only after both sequential analyses ran.

Concurrency screening

  • A spawn now repeats when its creating function may run more than once (multiple call sites, loops, recursion, repeating callers), so a counter two thread instances increment raises a candidate.
  • __atomic_*, __sync_* and C11 atomic accesses no longer pair, SV-COMP atomic sections hold a pseudo-lock, only stdatomic.h type names count as atomic, and a failed compare-exchange's expected argument is a write.
  • Lock calls come from a table covering mutexes, spin locks, rwlocks, semaphores and cond waits; locks follow calls, so a two-wrapper ABBA is a candidate, and a lock reached through a parameter counts at each call site.
  • Lock order reports cycles as deadlock candidates (a reader-only cycle is not one), double locks, threads exiting holding a lock, and a continue inside a switch lands at the nearest loop instead of merging paths after the switch.

Each soundness fix has a test confirmed to fail without it; all gates pass against Frama-C 33.0 with Alt-Ergo 2.6.3. Left out with reasons in the design docs: verdicts narrowed by target, cross-architecture machdep generation, and a prover memory cap.