Fix BoogieToStrata: handle cross-nesting and backward gotos#655
Open
tautschnig wants to merge 7 commits intomainfrom
Open
Fix BoogieToStrata: handle cross-nesting and backward gotos#655tautschnig wants to merge 7 commits intomainfrom
tautschnig wants to merge 7 commits intomainfrom
Conversation
Contributor
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
Contributor
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>
atomb
reviewed
Mar 27, 2026
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
approved these changes
Mar 27, 2026
Contributor
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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.