Add exact summaries for pointwise loops behind --functionalize-loops

[shaobo-he]

This lands the loop-functionalization branch as an opt-in option, --functionalize-loops, after an audit and the fixes it called for. The branch is squashed as the first commit; the six commits on top are what changed to land it.

What the option does

SMACK explores every loop --unroll times, so a bug that needs one more iteration is missed. For loops the recognizer can prove pointwise — one positive affine induction, an exact trip count, affine stores with injective and pairwise-disjoint images, right-hand sides reading only loop-entry memory — the loop's blocks are replaced by an exact summary: a memory-update loop assigns each written map a function of the entry maps; a search loop becomes a quantified predicate plus a failure witness; a loop of __VERIFIER_assert/assume becomes a quantified assumption plus one witness per assertion. A bug at iteration 4 is then found at --unroll=1. Its measured reach on the SV-COMP suites is in the branch's history; the precision limits the audit confirmed are listed at the end.

Lambdas re-encoded so stock Corral takes them

The branch emitted Boogie lambda expressions, which Corral 1.1.8 (Boogie 2.9.1) fails on before its own lambda lifting runs — the feature only worked through a patched Corral. SMACK now lifts each summary map itself, the way /freeVarLambdaLifting would: a map-valued function of the locals and maps the body mentions, defined by one read axiom whose only trigger is a read of the result, carrying {:weight 0} for the same reason the memcpy summaries do (a chain of summaries must not become a Z3 generation cost). Measured on the suite with stock Corral 1.1.8: without {:weight 0} every configuration times out; with it, 468/468 pass.

The flag-off rule

Before the fixes, 0 of 768 flag-off translations were byte-identical to develop: smack.h annotated the verifier primitives for every user (a new llvm.global.annotations global and its strings, and the annotation kept the library body of __VERIFIER_assert alive through DCE), verifier.primitive metadata reached the Boogie output as attributes, and -svcomp was passed for every SV-COMP task. The annotation now exists only under a define the frontend sets with the option, the metadata is filtered, and -svcomp goes only with the option. After: 1290 of 1293 identical across 14 folders × 3 memory models; the remaining 3 are pthread/lockattr.c, whose sea-DSA region numbering is nondeterministic on develop itself.

What the audit found and what changed

Six lenses, 46 findings, each sent to two adversarial verifiers; 27 confirmed, 4 refuted (summarised here). Every confirmed agreement defect had a witness whose verdict flipped between flag-off and flag-on; each now agrees and has a regression:

defect	witness	fix
i != e trip count is e - start modulo 2^N; under unbounded integers the loop never exits, the summary ran zero iterations and dropped a memory-safety bug	ne_wrap_ms.c: flag-off invalid dereference, flag-on no errors	equality exits accepted only with a constant count
summary constants printed signed where SmackRep::bop/select print unsigned magnitudes (two representatives per bit pattern)	a[i] = i * 2654435761u vs a[j] == j * 2654435761u: spurious error	mirror the per-opcode conventions; recurrences rendered from the update instruction, not SCEV's fold
escaping header PHI of a bottom-tested loop assigned start + step*T instead of T-1	do { … last = i; } while (i < n): safe last == n-1 errored, unsafe last == n verified	correct value when the exit test follows the body
failure-witness prefix was an untriggered forall never instantiated: an earlier failed assumption could not block a later assertion	spurious error	read-triggered form added, as the normal path had
recursive firstStop unfolded ≤ ~20 levels (Z3 generation cost), Boogie reported the unknown as a definite error on a safe 30-element scan	late_stop_30.c: definite spurious error	defined by its own {:weight 0} axiom; verifies in 1 s, symbolic stops to n ≤ 1000
under -svcomp a task-provided primitive was assumed memory-pure	—	required to be (body scan)

Also fixed: the bit-precise fallback path re-queried ScalarEvolution on normalized loops (the crash the branch had worked around); the SV-COMP regression's property path did not resolve from test/, so that test silently dropped out of every run; the folder was not in the CI matrix.

Verification

• test/c/functionalize-loops: 78 tests × 3 memory models × Boogie + stock Corral 1.1.8: 468/468. Ten new tests discriminate the fixes (each fails on the previous commit) and two decide bugs at iteration 3 with --unroll=1, which only the summary can.
• Flag off: byte-identical to develop as above.
• Flag on, injected into every test of 14 folders: 2335 passed, 0 failed, 0 unknown, 8 timeouts — all in the two_arrays family (see below). The same folders pass 100% flag-off. Through the Boogie-3.5.7 Corral fork the functionalize-loops suite is likewise 468/468.
• Zero compiler warnings from the new code.

Known limits

Precision items the audit confirmed and this PR leaves as they are: the region-shape gate runs on a not-yet-final Regions partition; a loop-invariant load on the right-hand side rejects the loop; load/store disjointness is checked symmetrically; the ITE order among stores to one map is justified by LLVM-object disjointness, so a program that is already memory-unsafe can see a different value; arrays filled by an initializer list or memset are never summarised.

Known cost

With stock Corral 1.1.8 and z3 5.x (the CI combination), test/c/data/two_arrays*.c go from ~30 s flag-off to a timeout flag-on; the same Boogie file verifies in 27 s with Corral's bundled z3 and in 6 s through the Boogie-3.5.7 Corral fork. /useArrayTheory, qi thresholds, smt.arith.solver=2 and smt.relevancy=1 do not help; {:weight 0} is already load-bearing. Not diagnosed further; the option is opt-in and off by default.

🤖 Generated with Claude Code