JVerify front-end: handle loop bodies without a contract block

[tautschnig]

What was changed?

Defensive hardening around contract-bearing loop/method blocks.

MethodOrLoopContractCompiler.getContractBlock casts a loop body's first statement to JCBlock. If a loop body without the contract-bearing shape ever reached it, that cast would throw a ClassCastException.

• Adds a hasContractStructure() predicate and has getContractBlock validate the shape up front, throwing a descriptive JavaViolationException (which the per-method handler catches, so the method is skipped gracefully) instead of letting the unchecked cast fail.
• Guards extractLoopParts in JavaToLaurelCompiler so a loop body without the contract-bearing shape is processed as pure implementation statements with no invariants (threading the caller's renames map, like the contract and non-block branches).

Note: forward-looking, not a currently-reachable crash

This is defensive hardening, not a fix for a crash reachable on the current tree. Hand-written contract-free loops are wrapped by MethodOrLoopContractCompiler and so already have the expected structure; the only unwrapped loop form is enhanced-for, which needs array/Iterable support that errors out first (Unsupported type: int[]). For that reason no regression test is constructible yet. Soundness is fine: the empty-invariant fallback is conservative, and real invariant() clauses are always wrapped.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache-2.0.

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Adds a safe predicate and better error handling around “contract-bearing” loop/method blocks, and updates loop extraction to gracefully handle loops without invariant wrappers (including javac desugared enhanced-for loops).

Changes:

• Add hasContractStructure(...) and validate contract block shape before extracting it.
• Throw a clearer IllegalArgumentException when contract structure is missing.
• Update loop extraction to bypass contract parsing when the wrapper block is absent.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.

File	Description
verifier/src/main/java/org/strata/jverify/verifier/compiler/simplifications/MethodOrLoopContractCompiler.java	Adds structural guard + predicate to avoid invalid casts when extracting contract blocks.
verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java	Uses the new predicate to handle loops without invariant wrappers as plain bodies.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[fabiomadge]

Sound defensive fix; the guard + descriptive exception beat a bare CCE.

Couldn't reproduce the CCE on the current tree — hand-written contract-free loops all get wrapped by MethodOrLoopContractCompiler, so they have the expected structure. The only unwrapped case is enhanced-for (no visitForeachLoop), which needs array/Iterable support, and those error first (Unsupported type: int[]). So it's latent hardening, not a currently-reachable crash. Soundness is fine (empty-invariant fallback is conservative; real invariant()s are always wrapped).

[fabiomadge]

Re-checked 95c15cb: both points addressed (getContractBlock throws catchable JavaViolationException; unreachable branch documented). Full suite passes, fallback is sound. No regression test yet (not constructible until arrays land — fine as forward-hardening); needs a rebase (BEHIND). LGTM.