Skip to content

v1.1.16 — inline argument forwarding (#228 secondary)#230

Merged
avrabe merged 2 commits into
mainfrom
feat/tier0-inline-argfwd
Jun 22, 2026
Merged

v1.1.16 — inline argument forwarding (#228 secondary)#230
avrabe merged 2 commits into
mainfrom
feat/tier0-inline-argfwd

Conversation

@avrabe

@avrabe avrabe commented Jun 22, 2026

Copy link
Copy Markdown
Contributor

Tier 0 of the post-v1.1.15 inliner feature loop. Z3-gated, no behavior change beyond cleaner inlined code.

#228 secondary finding: inlining spilled EVERY callee param to a fresh temp, so a bare local.get K arg became local.set TEMP; … local.get TEMP. simplify_locals cleans that in straight-line callers but bails on any control flow, so in CF callers (the gust hot path) the copy survived.

Fix: forward a trailing local.get K arg directly into the inlined body when the callee does NOT write that param (callee_param_writes). Sound — K isn't rewritten before the inlined body, and the body never writes K (param unwritten; callee locals remap to a disjoint range). Forwardable args are a value-stack top-suffix; remap_locals_in_block now takes a per-param target array. The Z3 verify-or-revert stays the correctness gate.

Validation: new test_inline_arg_forwarding_no_redundant_copy (2 local.get args → 0 spills) + test_inline_arg_forwarding_skips_written_param (written param stays spilled, no caller-local clobber). 416 lib tests green; multisite + mix repros still inline + validate. Merge only through passing required checks; the two known-infra reds (Rocq-upstream, Verification-Gate comment-403) don't block.

Refs #228

avrabe and others added 2 commits June 22, 2026 23:26
…spill+reload

Tier 0 follow-up to #228's secondary finding. inline_calls_in_block spilled EVERY
param to a fresh temp; when the arg was a bare `local.get K` this produced a
`local.set TEMP; … local.get TEMP` round-trip. simplify_locals cleans that in
straight-line callers but BAILS on any control flow (lib.rs ~8905), so in CF callers
(the gust hot path) the copy survived.

Forward a trailing `local.get K` arg directly into the inlined body when the callee
does NOT write that param (callee_param_writes). Sound: K isn't rewritten before the
inlined body, and the body never writes K (param not written; callee locals remap to a
disjoint range above param_start_idx). Forwardable args are a top-suffix (only bare
local.gets pop contiguously off the value stack). remap_locals_in_block now takes a
per-param target array. Z3 verify-or-revert stays the backstop.

Tests: test_inline_arg_forwarding_no_redundant_copy (2 local.get args → 0 spills);
test_inline_arg_forwarding_skips_written_param (written param stays spilled, no
caller-local clobber). 416 lib tests green; multisite + mix still inline + validate.

Refs #228

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Forward a bare `local.get K` argument directly into the inlined body when the
callee doesn't write that param, instead of spilling to a temp + reloading. Cleans
the redundant arg-copy that survived in control-flow callers (where simplify_locals
bails). Z3-gated; sound (callee_param_writes guards written params). No behavior
change beyond cleaner inlined code.

Refs #228

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@avrabe avrabe merged commit 4aa0bda into main Jun 22, 2026
22 of 24 checks passed
@avrabe avrabe deleted the feat/tier0-inline-argfwd branch June 22, 2026 22:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant