Extend Cmds.toGotoTransform to handle all Stmt types#289
Extend Cmds.toGotoTransform to handle all Stmt types#289tautschnig wants to merge 5 commits intomainfrom
Conversation
Extended transformation to handle all `Stmt` constructors (`.block`, `.ite`, `.loop`, `.goto` in addition to `.cmd`, which was already being handled). Ten new tests cover basic, nested, and edge-case scenarios.
tautschnig
force-pushed
the
tautschnig/ToCProverGOTO-Stmt
branch
from
b7a830b to
7b8e91f
Compare
| nextLoc := trans.nextLoc + 1 } | ||
| Block.toGotoInstructions trans.T functionName body trans | ||
|
|
||
| | .ite cond thenb elseb _md => |
There was a problem hiding this comment.
This case is getting a bit long and hard to read. I'd recommend using helper functions. Perhaps use Lean's where clauses? E.g.,:
def foo (x : Nat) : Nat :=
x + bar x + baz x
where
bar x := x
baz x := x
|
|
||
| return { trans with instructions := insts } | ||
|
|
||
| | .loop guard _measure _invariant body _md => |
There was a problem hiding this comment.
Another place where helper functions can improve readability.
|
One general comment on this: I have plans to add unstructured CFGs in Strata (started in #202), and it would probably make sense in the long run to have a a pipeline that does Strata Stmt -> Strata CFG -> GOTO instruction CFG. I'd paused work on #202 because it wasn't clear what we'd use it for right now, but I could finish it up and merge it if you think it'd be useful for this PR. |
There'll certainly be interactions between your PR and this one, but I'm happy for these to be worked on in either order: if #202 goes in first, this PR will be updated, else #202 should likely include changes to GOTO instruction support (which I'm then happy to contribute myself). |
There was a problem hiding this comment.
Pull request overview
This PR extends the transformation functionality from imperative commands to GOTO instructions by adding support for all statement types (.block, .ite, .loop, and .goto), not just the previously-supported .cmd statements.
Key Changes:
- Implemented mutual recursive functions
Stmt.toGotoInstructionsandBlock.toGotoInstructionsto handle all statement constructors - Added comprehensive test coverage with 10 test cases covering basic, nested, and edge-case scenarios
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
Strata/DL/Imperative/ToCProverGOTO.lean |
Adds mutual recursive transformation functions for statements and blocks, handling control flow constructs (blocks, conditionals, loops, gotos) with proper label generation and GOTO instruction patching |
StrataTest/Backends/CBMC/ToCProverGOTO.lean |
Adds 10 comprehensive test cases covering all new statement types including basic transformations, nested control flow, empty branches/bodies, and assertions/assumptions within control structures |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
I mostly just wanted to make sure we're both aware of each other's work. Since this PR seems just about ready to go, and #202 still needs some tests which I won't have a chance to add right away, let's go ahead and merge this one and update #202 later. |
3 participants
Description of changes:
Extended transformation to handle all
Stmtconstructors (.block,.ite,.loop,.gotoin addition to.cmd, which was already being handled).Ten new tests cover basic, nested, and edge-case scenarios.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.