Summary
When a verification failure occurs at an instruction that has predecessors via backward edges (loops), the verifier's -v output stops printing invariants at the first error. This makes it impossible to see the computed invariants for predecessor blocks that appear later in the instruction stream, preventing effective debugging.
Problem
The print_invariants function in src/printing.cpp iterates over basic blocks in program order (by PC/label) and prints their pre/post invariants. When it encounters an error, it prints the error and immediately returns (line 195):
if (current.error) {
os << "\nVerification error:\n";
// ...
print_error(os, *current.error);
os << "\n";
return; // <-- Stops all output here
}This works fine for straight-line code, but breaks down for loops.
Real-World Example
From a verification failure trace, instruction 184 fails with:
from 339:184;
184:
assert r0.type in {ctx, stack, packet, shared};
assert valid_access(r0.offset+80, width=8) for read;
r1 = *(u64 *)(r0 + 80);
Verification error:
184: Upper bound must be at most r0.shared_region_size (valid_access(r0.offset+80, width=8) for read)
The trace shows:
- Instruction 184 has a predecessor
339:184 (a backward edge from instruction 339)
- The trace includes
from 339; references
- But instruction 339's invariants are never printed — the output stops at 184 because that's where the error occurred
Searching for ^339: in the output only finds edge labels (339:184: and 339:340:) — there is no block showing the pre-invariant for the actual instruction at PC 339.
Impact
- Debugging loop-related failures is nearly impossible — the invariants that flow into the failing instruction via backward edges aren't visible
- Users see references to labels (like
339) that don't appear in the invariant output
- The only workaround is modifying the source code to comment out the early
return
Suggested Fix
Add an option (e.g., --print-all-invariants or change the default behavior of -v) to continue printing invariants after the first error:
- Remove or guard the early
return on line 195 of src/printing.cpp
- Continue iterating through all basic blocks, printing their invariants
- Mark error locations inline but don't stop the iteration
This would allow users to see the full invariant state across the entire CFG, including backward-edge predecessors, enabling proper debugging of loop-related failures.
Summary
When a verification failure occurs at an instruction that has predecessors via backward edges (loops), the verifier's
-voutput stops printing invariants at the first error. This makes it impossible to see the computed invariants for predecessor blocks that appear later in the instruction stream, preventing effective debugging.Problem
The
print_invariantsfunction insrc/printing.cppiterates over basic blocks in program order (by PC/label) and prints their pre/post invariants. When it encounters an error, it prints the error and immediately returns (line 195):This works fine for straight-line code, but breaks down for loops.
Real-World Example
From a verification failure trace, instruction 184 fails with:
The trace shows:
339:184(a backward edge from instruction 339)from 339;referencesSearching for
^339:in the output only finds edge labels (339:184:and339:340:) — there is no block showing the pre-invariant for the actual instruction at PC 339.Impact
339) that don't appear in the invariant outputreturnSuggested Fix
Add an option (e.g.,
--print-all-invariantsor change the default behavior of-v) to continue printing invariants after the first error:returnon line 195 ofsrc/printing.cppThis would allow users to see the full invariant state across the entire CFG, including backward-edge predecessors, enabling proper debugging of loop-related failures.