Fix BoogieToStrata: handle cross-nesting and backward gotos#655
Fix BoogieToStrata: handle cross-nesting and backward gotos#655tautschnig merged 9 commits intomainfrom
Conversation
There was a problem hiding this comment.
Pull request overview
Improves the Boogie-to-Strata-Core translator’s handling of goto-driven control flow that crosses structured nesting boundaries, aiming to eliminate Strata type-check failures related to invalid exit targets.
Changes:
- Recursively collects
gototargets from within nestedif/whilebodies to drive wrapper-block creation at the appropriate nesting level. - Tracks “currently enclosing” wrapper labels to avoid emitting duplicate/shadowing labeled blocks.
- Adds a new Boogie regression test (
CrossNestingExit) and expected verification output.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| Tools/BoogieToStrata/Source/StrataGenerator.cs | Adds nested goto-target collection and wrapper/label handling logic for cross-nesting (and attempted back-edge) scenarios. |
| Tools/BoogieToStrata/Tests/CrossNestingExit.bpl | New regression test exercising cross-nesting exits and back-edge gotos. |
| Tools/BoogieToStrata/Tests/CrossNestingExit.expect | Expected verifier output for the new regression test. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tautschnig
force-pushed
the
tautschnig/fix-boogie-to-strata
branch
from
7f5cab1 to
5352445
Compare
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Cross-nesting forward gotos: recursively collect goto targets from nested if/while bodies so wrapper blocks are created at the correct nesting level. Track enclosing wrapper labels to avoid emitting duplicate labeled blocks. Backward gotos (loops): translate back-edges to while(true) loops instead of extending wrapper closeAt indices (which broke Strata's exit semantics). For each detected back-edge, the affected blocks are wrapped in while(true) with the back-edge target label wrapping the entire loop body, so 'exit <label>' acts as continue. Forward targets within the loop body use inner wrappers; forward exits to labels outside the loop propagate through the while as normal. Add CrossNestingExit regression test covering: - CrossNestingForward: goto from inside if-branch to sibling block - BackwardGotoBuggy: demonstrates the old approach incorrectly passed a buggy assertion (g <= 2 after a doubling loop), while the new while-loop encoding correctly detects the bug - BackwardGotoLoop: simple backward goto forming a loop - CrossNestingInLoop: cross-nesting goto inside a loop body Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
tautschnig/fix-boogie-to-strata
branch
from
5352445 to
1db2cac
Compare
The loop region detection incorrectly rejected nested loops as irreducible control flow. When an inner loop's back-edge target fell within an outer loop's range but had a different start index, the code threw an error instead of recognizing valid nesting. Changes: - Introduce LoopRegion class with children list for tree-structured loop nesting - BuildLoopRegions/InsertRegion: build a tree of loop regions where properly contained regions become children instead of being rejected - EmitLoopRegion: recursively emit child loop regions as nested while(true) blocks, with forward wrappers for child back-edge labels that close before the child's while opens (avoiding label shadowing) - EmitStmtList: treat child back-edge labels as inner targets of their parent loop rather than outer wrappers Add NestedLoops regression test covering: - NestedLoops: simple nested backward gotos (outer i-loop, inner j-loop) - NestedLoopsCrossNesting: nested loops with cross-nesting forward goto inside the inner loop body Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Replace all occurrences of the "_exit" string literal with a named constant to prevent subtle bugs from typos. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
When a new loop region fully contains an existing sibling, reparent the existing region (and any subsequent contained siblings) as children of the new region. This makes InsertRegion robust regardless of insertion order, rather than relying on the sort in BuildLoopRegions to always process outer loops before inner ones. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add comment in EmitStmtList explaining that inner target classification only checks top-level regions, with targets delegated down through recursive EmitLoopRegion calls for nested (child/grandchild) regions. Add TripleNestedLoops regression test exercising three levels of backward gotos to verify the delegation chain works correctly. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
atomb
left a comment
atomb
left a comment
There was a problem hiding this comment.
As much as the logic here is complex, and I'm not 100% sure I've convinced myself that it's correct, I'm pretty confident that it's at least an improvement on where we were. So let's merge it and go from there.
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
Solid implementation of cross-nesting and backward goto handling. The decomposition into ComputeMaxSourceForTarget, DetectBackEdges, BuildLoopRegions, InsertRegion, and EmitLoopRegion keeps the complexity manageable. The irreducible control-flow detection is a nice safety net. Test coverage is thorough — the BackwardGotoBuggy test demonstrating that the old approach missed a real bug is a great regression test.
A few observations below, nothing blocking.
CollectNestedGotoTargets already collects from each BigBlock tc (GotoCmd/ReturnCmd) before recursing into nested structures, making the prior CollectGotoTargets call a strict subset. Replace both with a single CollectNestedGotoTargets call. Remove LoopRegion.Deconstruct — it was used only once with labels discarded. Direct field access is clearer. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…schnig/fix-boogie-to-strata
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
I think the PR is doing what it claims and seems nicely implemented, and my agent also reviewed it accordingly. I'm just not sure about the "All 0 goals passed".
Oh, that was just that there were no properties to be proved in one of the tests. |
Cross-nesting forward gotos: recursively collect goto targets from nested if/while bodies so wrapper blocks are created at the correct nesting level. Track enclosing wrapper labels to avoid emitting duplicate labeled blocks.
Backward gotos (loops): translate back-edges to while(true) loops instead of extending wrapper closeAt indices (which broke Strata's exit semantics). For each detected back-edge, the affected blocks are wrapped in while(true) with the back-edge target label wrapping the entire loop body, so 'exit ' acts as continue. Forward targets within the loop body use inner wrappers; forward exits to labels outside the loop propagate through the while as normal.
Add CrossNestingExit regression test covering:
Co-authored-by: Kiro kiro-agent@users.noreply.github.com
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.