Fix prepend ordering for imperative calls in expression position#42
Fix prepend ordering for imperative calls in expression position#42keyboardDrummer-bot wants to merge 1 commit intomainfrom
Conversation
Save prepends before processing arguments so that: 1. Argument side-effects execute first (defining snapshot variables) 2. Outer prepends (from sibling expressions) execute next (defining their snapshot variables that the call may reference) 3. The lifted call executes last (after all referenced variables exist) Also uncomments the addProcCaller test case. The correct assertion value is 15 (not 14): addProc(1,11)=12, plus (x:=3)=3, total 15. Closes #39
|
The "Run internal benchmarks of Strata" failure is not caused by this PR's code changes. It's an infrastructure issue affecting all PRs on this fork. Root cause: The benchmark CI job (ci.yml L345) uses Evidence: PR #38 (unrelated changes) has the exact same benchmark failure. The build, lint, tests, CBMC, Python tests, and documentation all pass. Local verification:
|
|
@keyboardDrummer-bot please cut this PR with a branch in strata-org/strata, immediately take it out of draft and only assign yourself to it |
|
Done. Created strata-org#1130 in |
2 participants
Fixes #39
Problem
When an imperative call appears in expression position alongside other side-effecting expressions (e.g.
addProc({x := 1; x}, {x := x + 10; x}) + (x := 3)), the lifted call could reference snapshot variables that hadn't been declared yet.Fix
Save prepends BEFORE processing the call's arguments, then reassemble in the correct order:
Test
Uncommented the
addProcCallertest case. The correct assertion value isz == 15:addProc({x := 1; x}, {x := x + 10; x})= addProc(1, 11) = 12(x := 3)evaluates to 3All 591 existing tests continue to pass.