Conversation
Introduce a Static Single Assignment (SSA) transformation that converts procedure bodies so every variable is assigned exactly once via init. Mutations (set, havoc) become fresh init declarations. At if-then-else join points, conditional init expressions merge divergent variable versions. The transformation: - Runs after callElim and loopElim (no calls or loops expected) - Converts set to init with fresh variable names (x_0, x_1, ...) - Converts havoc to nondet init - Rewrites expressions to reference current SSA variable versions - Emits conditional merge inits at if-then-else join points - Uses modelPreserving validation (semantics-preserving) Integration: - Available as --pass ssa in the transform CLI command - Available as TransformPass.ssa in the SimpleAPI - Not part of the default verification pipeline (opt-in) Files: - Strata/Transform/SSA.lean: transformation implementation - StrataTest/Transform/SSA.lean: 16 tests covering straight-line, if-then-else, havoc, nested branches, multiple variables, inout params, and pipeline chaining - Strata/SimpleAPI.lean: TransformPass.ssa + applyPass integration - StrataMain.lean: ssa added to valid transform passes
Refactor SSA transformation to use the standard CoreTransformM monad instead of a custom SSAM monad. This aligns with the transform API conventions used by other transforms (CallElim, LoopElim, etc.). Changes: - Use CoreGenState.gen for fresh name generation (ssa_ prefix) - Use Transform.incrementStat for statistics - Use Transform.createFvar for fvar construction - Thread Env through function parameters instead of custom state - Replace panic! with empty program fallback in test helper
Use #eval instead of #eval! as recommended. The #eval! was a leftover from an earlier iteration that had sorry dependencies.
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
1 participant
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.
Introduce a Static Single Assignment (SSA) transformation that converts
procedure bodies so every variable is assigned exactly once via init.
Mutations (set, havoc) become fresh init declarations. At if-then-else
join points, conditional init expressions merge divergent variable versions.
Uses the standard CoreTransformM monad with CoreGenState.gen for fresh
name generation (ssa_ prefix), aligning with transform API conventions.
Integration:
Files: