Fix multi-output calls in expression position (Python front-end) by tautschnig · Pull Request #1117 · strata-org/Strata

tautschnig · 2026-05-05T16:42:40Z

When translateExpr produces an expression containing a nested multi-output procedure call (e.g., PSub(base, timedelta_func(...))), the new extractMultiOutputCalls pass in translateAssign rewrites it into a preceding multi-target assignment and a variable reference:

var $mo_N := ...; assign $mo_N, maybe_except := timedelta_func(...);
delta := PSub(base, $mo_N)

This prevents multi-output calls from appearing in expression position, which would silently discard the error channel.

Key design choices:

Counter seeded from source range hash to avoid temp name collisions across assignments
Branch-local multi-output calls are wrapped in Block nodes inside their respective IfThenElse branches (not hoisted unconditionally)
Generated wrapper statements propagate source metadata from the original call
Block-flattening in the lifter uses cons-based prepend for correct evaluation order
containsBareAssignment skips Blocks so generated wrappers pass through assert/assume handlers

Tested: existing tests pass, builds cleanly.

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.

When translateExpr produces an expression containing a nested multi- output procedure call (e.g., PSub(base, timedelta_func(...))), the new extractMultiOutputCalls pass in translateAssign rewrites it into a preceding multi-target assignment and a variable reference: var $mo_0 := ...; assign $mo_0, maybe_except := timedelta_func(...); delta := PSub(base, $mo_0) This prevents multi-output calls from appearing in expression position, which would silently discard the error channel. Changes: - Add extractMultiOutputCalls (StateM Nat) and translateExprExtractingCalls in PythonToLaurel.lean - Extend containsUserCall to detect multi-output prelude calls and Blocks (preventing duplication in exception checks) - Add containsBareAssignment in LiftImperativeExpressions.lean that skips Blocks, used by assert/assume handlers - Add Block-flattening in the lifter for generated multi-output wrappers (pattern: [VarDecl, MultiAssign(2+ targets), VarRef]) - Restore test_procedure_in_assert.py with the original multi-output call in expression position (base - timedelta(days=7)) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Copilot

Pull request overview

This PR updates the Python→Laurel translation pipeline to prevent multi-output procedure calls (those producing an error channel via maybe_except) from appearing in expression position by extracting them into preceding statements, and adjusts the Laurel imperative-expression lifter/assert handling to accommodate the generated wrapper patterns.

Changes:

Add an extraction pass for nested multi-output calls during assignment translation (extractMultiOutputCalls, translateExprExtractingCalls).
Extend procedure-call detection used by exception-check preambles, and update the lifter to allow/flatten generated Block wrappers in assert/assume conditions.
Update the regression test and expected Laurel output to cover a multi-output call nested inside an expression (base - timedelta(days=7)).

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 6 comments.

File	Description
Strata/Languages/Python/PythonToLaurel.lean	Adds nested multi-output call extraction and adjusts exception-check placement logic around assignments.
Strata/Languages/Laurel/LiftImperativeExpressions.lean	Adds `containsBareAssignment`, updates assert/assume handling, and flattens specific generated Block wrapper shapes.
StrataTest/Languages/Python/tests/test_procedure_in_assert.py	Restores a nested multi-output call in expression position for coverage.
StrataTest/Languages/Python/expected_laurel/test_procedure_in_assert.expected	Updates expected proof log/output to match the new translation shape.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

MikaelMayer · 2026-05-19T22:11:42Z

+    if withException ctx callee.text then
+      -- Multi-output call: extract into a temp assignment and add exception check
+      let n ← get
+      set (n + 1)
+      let varName := s!"$mo_{n}"
+      let varDecl := mkVarDeclInit varName AnyTy AnyNone
+      let assign := mkStmtExprMd (StmtExpr.Assign
+        [mkVariableMd (.Local varName), maybeExceptVar] e)
+      let varRef := mkStmtExprMd (StmtExpr.Var (.Local varName))
+      return ([varDecl, assign], varRef)
+    else
+      -- Recurse into arguments
+      let mut preamble : List StmtExprMd := []
+      let mut newArgs : List StmtExprMd := []
+      for arg in args do
+        let (pre, arg') ← extractMultiOutputCalls ctx arg
+        preamble := preamble ++ pre
+        newArgs := newArgs ++ [arg']
+      if preamble.isEmpty then
+        return ([], e)
+      else
+        return (preamble, mkStmtExprMdWithLoc (.StaticCall callee.text newArgs) e.source)


🤖 Fixed: source metadata is now propagated to the generated assign and varRef statements using mkStmtExprMdWithLoc. The rebuilt call also preserves the original source. See 23cff9f.

MikaelMayer · 2026-05-19T22:10:43Z

  | .Block stmts labelOption =>
      let newStmts := (← stmts.reverse.mapM transformExpr).reverse
-      return ⟨ .Block (← onlyKeepSideEffectStmtsAndLast newStmts) labelOption, source⟩
+      let filtered ← onlyKeepSideEffectStmtsAndLast newStmts
+      -- Flatten generated multi-output call wrappers: Blocks of the form
+      -- [VarDecl, MultiAssign, VarRef] where the assign has 2+ targets.
+      match filtered with
+      | [decl, assign, last] =>
+        match decl.val, assign.val with
+        | .Assign [t] _, .Assign targets _ =>
+          match t.val with
+          | .Declare _ =>
+            if targets.length ≥ 2 then
+              modify fun s => { s with prependedStmts := s.prependedStmts ++ [decl, assign] }
+              return last
+            else
+              return ⟨ .Block filtered labelOption, source⟩
+          | _ => return ⟨ .Block filtered labelOption, source⟩
+        | _, _ => return ⟨ .Block filtered labelOption, source⟩
+      | _ => return ⟨ .Block filtered labelOption, source⟩


🤖 Safe: the flattening only triggers for the specific [VarDecl, MultiAssign(2+ targets), VarRef] pattern, which is exclusively generated by extractMultiOutputCalls with none label. User-authored labeled blocks won't match this pattern.

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

MikaelMayer

🤖🔍 The latest commit (7c11a98) introduces build failures. Beyond those, the IfThenElse branch-extraction logic has a semantic gap.

MikaelMayer · 2026-05-19T20:56:13Z

+      if preThen.isEmpty then
+        then'
+      else
+        mkStmtExprMdWithLoc (.Block (preThen ++ [then'])) thenBr.source


🤖🔍 Build failure: .Block requires a second (label : Option String) argument. Should be .Block (preThen ++ [then']) none. Same issue on line 1396.

🤖 Already fixed in a previous commit — .Block now receives none as the second argument on both lines.

MikaelMayer · 2026-05-19T20:56:13Z

  let rhsCtx := if isSelfFieldAssign then {ctx with suppressDispatch := true} else ctx
-  let rhs_trans ←  translateExpr rhsCtx rhs
+  let extractionSeedText :=
+    match pyRangeToFileRange rhs.ann with


🤖🔍 Build failure: pyRangeToFileRange and rangeToTempName (line 1449) are not defined in this file or its imports. The seed computation doesn't compile.

🤖 Already fixed in a previous commit — replaced pyRangeToFileRange/rangeToTempName with a simple hash computation using rhs.ann.start/rhs.ann.stop and String.foldl. Compiles cleanly now.

MikaelMayer · 2026-05-19T20:56:13Z

+        else'
+      else
+        mkStmtExprMdWithLoc (.Block (pre ++ [else'])) else'.source
+    if preCond.isEmpty then


🤖🔍 When preCond is empty but preThen or preElse is non-empty, this returns ([], e) — discarding the branch rewrites. A multi-output call nested in a then/else branch (but not the condition) would be silently ignored. The guard should also check whether any branch preamble is non-empty.

🤖 Fixed: the condition now checks anyRewrite (preCond, preThen, or preElse non-empty) instead of only preCond.isEmpty. Multi-output calls in then/else branches are no longer silently discarded. See 23cff9f.

MikaelMayer · 2026-05-19T20:56:13Z

  }
+  -- When the RHS is a direct multi-output call (top-level), translateAssign
+  -- already handles it with multi-target assignment. Don't double-extract.
+  let moExtracts := match rhs_trans.val with


🤖🔍 This guard is dead code. extractMultiOutputCalls already rewrites a top-level withException call into a Var reference, so rhs_trans.val can never be .StaticCall callee _ with withException ctx callee.text true by the time this check runs.

🤖 Removed: the guard was dead code since extractMultiOutputCalls already rewrites top-level withException calls into Var references — rhs_trans.val can never be a .StaticCall with withException at that point. See 23cff9f.

- Add missing 'none' label argument to .Block constructors in extractMultiOutputCalls IfThenElse case - Replace non-existent pyRangeToFileRange/rangeToTempName with inline SourceRange field access for extraction seed generation

…-multi-output-diagnostic

MikaelMayer

🤖🔍 Two of four previous comments were addressed (.Block label argument and undefined pyRangeToFileRange/rangeToTempName). Two remain:

Branch preamble discarded when preCond.isEmpty (line ~1397): When preCond is empty but preThen or preElse is non-empty, the code still returns ([], e) — the original expression — discarding the computed thenExpr/elseExpr that contain the branch-local extractions. A multi-output call nested only inside a then/else branch (not the condition) would be silently ignored. The fix should return the rewritten IfThenElse even when preCond is empty.
Dead-code guard at line ~1484: extractMultiOutputCalls already rewrites a top-level withException call into a Var reference, so rhs_trans.val can never match .StaticCall callee _ with withException ctx callee.text == true by the time the guard runs. This is harmless but misleading — consider removing it or adding a comment explaining why it's kept as a safety net.

…pagate source metadata

MikaelMayer

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

…-multi-output-diagnostic

MikaelMayer

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

Two bugs fixed: - extractMultiOutputCalls used pre.reverse.foldl to accumulate preamble statements, which reversed the declaration order (assign before varDecl). Fixed to use pre.foldl so declarations precede their uses. - Block flattening in the lifter checked for the multi-output pattern after onlyKeepSideEffectStmtsAndLast, which dropped the multi-target assign. Moved the pattern check before that function runs.

MikaelMayer

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

…ource Two issues caused golden-file test failures: 1. withExceptionChecks only looked at the very last statement in the list, but when a type assertion (Assert) is appended after the assignment, the last statement is no longer an Assign and no exception check is generated. Fix: search backwards for the last Assign statement. 2. extractMultiOutputCalls used the expression's source location for extracted assignments, causing requires-check diagnostics to report the expression position instead of the statement position. Fix: override extracted assignment sources with the statement's source.

MikaelMayer

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

tautschnig self-assigned this May 5, 2026

github-actions Bot added Laurel Python labels May 5, 2026

github-actions Bot added the Git conflicts label May 19, 2026

tautschnig force-pushed the tautschnig/resolution-multi-output-diagnostic branch from e0b67ad to 285216a Compare May 19, 2026 09:39

tautschnig marked this pull request as ready for review May 19, 2026 09:39

tautschnig requested review from a team and Copilot May 19, 2026 09:39

github-actions Bot added Waiting-For-Review and removed Git conflicts labels May 19, 2026

Copilot started reviewing on behalf of tautschnig May 19, 2026 09:40 View session

Copilot AI reviewed May 19, 2026

View reviewed changes

MikaelMayer assigned MikaelMayer and unassigned tautschnig May 19, 2026

Apply suggestions from code review

7c11a98

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

MikaelMayer reviewed May 19, 2026

View reviewed changes

MikaelMayer added 2 commits May 19, 2026 22:02

Merge remote-tracking branch 'origin/main' into tautschnig/resolution…

e48f3f7

…-multi-output-diagnostic

MikaelMayer reviewed May 19, 2026

View reviewed changes

Address review: fix IfThenElse branch discard, remove dead guard, pro…

23cff9f

…pagate source metadata

MikaelMayer reviewed May 19, 2026

View reviewed changes

Merge remote-tracking branch 'origin/main' into tautschnig/resolution…

f2fd8cf

…-multi-output-diagnostic

MikaelMayer reviewed May 19, 2026

View reviewed changes

MikaelMayer reviewed May 20, 2026

View reviewed changes

Conversation

tautschnig commented May 5, 2026 • edited by MikaelMayer Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tautschnig commented May 5, 2026 •

edited by MikaelMayer

Loading