Two gaps in the loop-exit soundness rule from 6adcc24, both found in
review and reproduced as Proved always-conditions:
- `continue` was not an escape. The walkers drop an arm that ends in
`continue` (it always leaves the iteration), so iterations that took it
were never modeled, yet the unroll still counted as exact and the
loop's variables were not havocked:
for (i = 0; i < 2; i++) { if (y) continue; x++; } if (x == 2)
was "always true" although y != 0 gives x == 0. containsLoopEscape now
treats a continue that targets the loop as an escape (a switch
captures break but not continue; a nested loop captures both).
- Havocking a truncated loop reset scalar variables only. Array element
and member stores from the partial unroll survived:
for (i = 0; i < n && i < 4; i++) buf[i] = 1; if (buf[0] == 1)
was "always true" although n == 0 leaves buf[0] == 0. The unroll now
records the base variables of array/member stores and replaces their
arrays/values with fresh ones of the same sort; a store through a
pointer havocs every tracked heap array (SymbolicEnv::havocHeapArrays)
and marks the env over-approximated. The three walkers share this via
LoopUnrollExits::havoc.
Tests (test_loop_exit_soundness): continue, local-array and heap-pointer
stores are no longer Proved by dead-branch, always-condition or
unreachable; the exact constant-bound loop stays Proved (negative
control). A pointer-mutating call inside the loop (review #9) did not
reproduce for unreachable; its case is kept as a regression guard.
The dead-branch, always-condition and unreachable walkers unroll loops
loop_unroll times, following only the path on which the guard holds.
When the guard could also be false (any symbolic bound), that early
exit was dropped, and the loop's assigned variables were havocked only
for loops containing calls. The state after the loop was therefore
"the loop ran exactly loop_unroll times", and conditions on it were
reported as Proved:
int s = 0; for (unsigned i = 0; i < n; ++i) s += 1;
if (s == 0) ... // "dead" proved/exact, "always false" proved
The same held for `s > 100`, while loops, and a `break` out of a
constant loop. On the audit probes this was 7 Proved findings, all
false.
LoopUnrollExits now records whether the unroll saw every way out of
the loop: no iteration could exit early (the guard's false branch was
infeasible), the unroll stopped because the guard became infeasible
rather than because loop_unroll ran out, and the body has no break or
goto that escapes. When any of that fails, the walker havocs the loop's
assigned variables and restores the entry path, as it already did for
opaque loops. A loop the unroll exits exactly (constant bound within
budget) keeps its precise state, so a genuinely dead branch after it
is still Proved.
Loop-bound provenance (--suppress-loop-bound-always-conditions) stays
off by default: it existed to downgrade proofs that leaned on the
unroll bound, and an inexact loop exit now havocs instead of producing
such a proof in the first place.
The duplicated helpers (containsCallExpr, collectAssignedVars,
appendAssignedVars, havocAssignedVars) move from dead_branch.cpp and
always_condition.cpp into detect/loop_havoc so all three walkers share
them; dead_branch.cpp drops under the 800-line soft cap.
Tests: test_loop_exit_soundness covers the symbolic-bound cases for all
three detectors (4 Proved each for dead and always-condition before),
the break escape, the exact-loop negative control, and the extracted
helpers (containsLoopEscape, LoopUnrollExits). Full suite 136/136.
