docs(vcr-ra): resolve #470 — optimized-path ABI model is non-AAPCS by design#473
Merged
Conversation
… design (analysis) #470 asked whether the optimized (non-relocatable) path emitting an exported leaf that clobbers callee-saved r4-r8 with `bx lr` and no push is an AAPCS violation. Determination: by-design, not a bug. synth has two ABI models selected by --relocatable: the optimized path is the self-contained bare-metal model (non-AAPCS by design — documented in arm_backend.rs: "does not preserve caller-saved registers across calls"; ir_to_arm also emits no callee-saved push and its temp pool prefers r4-r8), and --relocatable is the AAPCS/host-link path (select_with_stack, fp-relative, proper preservation). The self-contained model is self-consistent (verified — intra_module_callee_saved.wat): a call-containing function is declined by the optimizer to the direct selector, which holds across-call values on the FRAME (caller `a`: str [sp] before `bl`, ldr [sp] after — never relies on the callee preserving r4-r8) and pushes/pops {r4-r8,lr} for ITS caller. So an optimized leaf's callee-saved clobber corrupts nothing intra-module; the only exposure is an external AAPCS caller, for which --relocatable is the required documented path. No fix warranted. Also resolves the VCR-RA-002 (#471) baseline worry: the measured `push {r4-r8,lr}` is on the call-containing/relocatable path, NOT optimized leaves — so #470 does not reset VCR-RA-002's baseline. Adds the generic evidence fixture + the ABI-model note. Refs #470, #428, #242 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
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.
Resolves #470 (analysis-only, frozen-safe — no codegen change; frozen gate green).
Determination: by-design, not a bug
synth has two ABI models selected by
--relocatable:--relocatableir_to_armselect_with_stackDocumented in
arm_backend.rs: the optimized path "does not preserve caller-saved registers across calls." The callee-saved clobber #470 spotted is the same fact deeper:ir_to_armemits no callee-saved push and its temp pool prefers r4-r8.Self-consistency verified (
intra_module_callee_saved.wat)A call-containing function is declined to the direct selector, which holds across-call values on the frame (caller
a:str [sp]beforebl,ldr [sp]after — never relies on the callee preserving r4-r8) and pushes/pops{r4-r8,lr}for its caller. So an optimized leaf's clobber corrupts nothing intra-module. The only exposure is an external AAPCS caller — for which--relocatableis the required, documented path. No fix warranted.Bonus: clears the VCR-RA-002 baseline worry (#471)
The measured
push {r4-r8,lr}is on the call-containing/relocatable path, not optimized leaves — so #470 does not reset VCR-RA-002's baseline.Adds the generic evidence fixture + an ABI-model note.
Refs #470, #428, #242
🤖 Generated with Claude Code