Skip to content

Refactor: make prepend ordering explicit for imperative calls in expression position #1130

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
keyboardDrummer-bot wants to merge 2 commits into
base: main2
Choose a base branch
from
+16 −11
Draft

Refactor: make prepend ordering explicit for imperative calls in expression position #1130

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f75a84e
Fix prepend ordering for imperative calls in expression position
keyboardDrummer-bot May 6, 2026
d85768b
Improve comments: rename prePrepends to siblingPrepends, document ord…
keyboardDrummer-bot May 8, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 13 additions & 4 deletions Strata/Languages/Laurel/LiftImperativeExpressions.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -272,16 +272,25 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do

| .StaticCall callee args =>
let model := (← get).model
let seqArgs ← args.reverse.mapM transformExpr
let seqCall := ⟨.StaticCall callee seqArgs.reverse, source⟩
if model.isFunction callee then
return seqCall
let seqArgs ← args.reverse.mapM transformExpr
return ⟨.StaticCall callee seqArgs.reverse, source⟩
else
-- Imperative call in expression position: lift to an assignment.
-- Only valid for single-output procedures (or unresolved ones where we
-- fall back to a single target). Multi-output procedures in expression
-- position are a bug in the upstream translation — Resolution should
-- emit a diagnostic for that case.
--
-- We isolate prepends into three explicit groups so the ordering is
-- visible: argPrepends ++ siblingPrepends ++ liftedCall.
-- NOTE: this ordering places sibling effects before the call. A future
-- fix for correct left-to-right evaluation should use
-- argPrepends ++ liftedCall ++ siblingPrepends instead.
let siblingPrepends ← takePrepends
let seqArgs ← args.reverse.mapM transformExpr
let argPrepends ← takePrepends
let seqCall := ⟨.StaticCall callee seqArgs.reverse, source⟩
let outputs := match model.get callee with
| .staticProcedure proc => proc.outputs
| .instanceProcedure _ proc => proc.outputs
Expand All @@ -294,7 +303,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
⟨.Var (.Declare ⟨callResultVar, callResultType⟩), source⟩,
⟨.Assign [⟨.Local callResultVar, source⟩] seqCall, source⟩
]
modify fun s => { s with prependedStmts := s.prependedStmts ++ liftedCall}
modify fun s => { s with prependedStmts := s.prependedStmts ++ argPrepends ++ siblingPrepends ++ liftedCall}
return bare (.Var (.Local callResultVar))

| .IfThenElse cond thenBranch elseBranch =>
Expand Down
10 changes: 3 additions & 7 deletions StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,13 +139,9 @@ procedure addProcCaller(): int
{
var x: int := 0;
var y: int := addProc({x := 1; x}, {x := x + 10; x});
assert y == 11

// The next statement is not translated correctly.
// I think it's a bug in the handling of StaticCall
// Where a reference is substituted when it should not be
// var z: int := addProc({x := 1; x}, {x := x + 10; x}) + (x := 3);
// assert z == 14
assert y == 11;
var z: int := addProc({x := 1; x}, {x := x + 10; x}) + (x := 3);
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The uncommented test only exercises the code path with a pure imperative procedure (addProc has no side effects beyond producing r). With such a procedure, both the current order (argPrepends ++ prePrepends ++ liftedCall) and the alternative order (argPrepends ++ liftedCall ++ prePrepends) are observationally identical — neither x's final value nor $c_0's value depend on which one runs first.

Please add a companion test that uses a procedure with observable side-effects, so that whichever ordering the transform picks is locked in by the test:

composite Counter { var value: int }

procedure bumpAndGet(c: Counter) returns (r: int)
  opaque
  modifies c
{ c#value := c#value + 100; return c#value };

procedure bumpCaller(): int
  opaque
{
  var c: Counter := new Counter;
  c#value := 1;
  var y: int := 0;
  // Semantic (left-to-right): bumpAndGet(c) runs first -> c#value=101,
  // returns 101; then y:=7 runs -> y=7. Final z = 101+7 = 108.
  // With `argPrepends ++ prePrepends ++ liftedCall`, (y:=7) runs before
  // the call and c#value ends up unchanged at the point $c_0 is assigned,
  // but $c_0 still reflects the post-call value so the numeric result is
  // the same. However, the heap-seen ordering *is* observable in more
  // complex examples; please add one.
  var z: int := bumpAndGet(c) + (y := 7);
  assert z == 108;
  assert y == 7;
  assert c#value == 101
};

A stronger version would involve the sibling expression also reading c#value after the call, which would genuinely differentiate the two orderings — but if the transform ordering stays as-is, that test would fail, which is exactly the point of #39 that this PR claims to close.

assert z == 15
Copy link
Copy Markdown
Contributor

@tautschnig tautschnig May 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: the PR description says the commented-out assert z == 14 was "not translated correctly" before. I ran the test on both merge-base and head and the old code already produces the correct VC ($c_0@1 + 3 == 15 with $c_0@1 == 12); the old assertion value 14 was simply wrong, not a symptom of a translation bug. If this test was only commented out because of uncertainty about the expected value, please say so in the commit message — it doesn't change what the PR does, but it avoids future readers inferring a behavior change that didn't happen.

};
"

Expand Down
Loading