Fix BoogieToStrata: handle cross-nesting and backward gotos#655
Open
tautschnig wants to merge 1 commit intomainfrom
Open
Fix BoogieToStrata: handle cross-nesting and backward gotos#655tautschnig wants to merge 1 commit intomainfrom
tautschnig wants to merge 1 commit 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 <[email protected]>
tautschnig
force-pushed
the
tautschnig/fix-boogie-to-strata
branch
from
5352445 to
1db2cac
Compare
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 [email protected]
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.