PR11.23h auto-snapshot shared call arguments

[agentc1]

Summary

• generalize the shared-condition snapshot replacement pass so pre-rendered assignment RHS and call argument images can be rewritten through snapshot locals
• apply shared snapshot wrapping to assignment RHS paths, standalone calls, and print
• add pr1123h_shared_call_argument_snapshot_build.safe covering the original Auto-snapshot all shared field reads in compound expressions to eliminate interfering-context rejections #287 compound-condition shape plus flat and nested shared getter call arguments
• update proof inventory, README counts, roadmap, verification matrix, and emitted Ada snapshots

Pre-change failure evidence

Before the emitter change, the new fixture shape failed at level 2 with GNATprove volatile-call diagnostics:

error: shared reads in compound conditions must be snapshot first
raw: call to a volatile function in interfering context is not allowed in SPARK
raw: volatile function call as actual is not allowed in SPARK (SPARK RM 7.1.3(9)) [E0004]

Validation

• alr build
• python3 scripts/safe_cli.py prove --level 2 tests/build/pr1123h_shared_call_argument_snapshot_build.safe
• python3 scripts/snapshot_emitted_ada.py --check after regenerating snapshots
• python3 scripts/run_tests.py (1044 passed, 1 skipped, 0 failed)
• python3 scripts/run_samples.py (19 passed, 0 failed)
• python3 scripts/run_proofs.py (265 proved, 0 failed)
• pre-push hook reran tests, samples, and proofs successfully before branch push

Closes #287

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 11a045cfca

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[Copilot]

Pull request overview

Extends the Ada emitter’s shared-read snapshotting so volatile shared getter calls are automatically hoisted into per-statement snapshot locals not only in conditions, but also in assignment RHS and call-argument contexts (including nested calls and print), addressing #287.

Changes:

• Generalize the shared-condition snapshot replacement pipeline to work from pre-rendered statement images (call/print/assignment RHS).
• Apply shared snapshot wrapping to standalone calls, print, and multiple assignment RHS emission paths.
• Add a new build fixture covering compound conditions plus flat/nested shared getter call arguments; update proof/docs inventories and emitted Ada snapshots.

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
compiler_impl/src/safe_frontend-ada_emit-statements.adb	Generalizes snapshot replacement to operate on pre-rendered images and wraps call/print/assignment RHS statements with snapshot declare blocks as needed.
tests/build/pr1123h_shared_call_argument_snapshot_build.safe	New regression fixture for #287 covering compound conditions, flat call args, nested call args, and print.
scripts/_lib/proof_inventory.py	Adds the new PR11.23h fixture to the proof-expansion fixture manifest.
docs/roadmap.md	Documents PR11.23h scope and constraints (statement-context insertion point, per-root snapshot discipline).
docs/emitted_output_verification_matrix.md	Adds verification-matrix entry for the new shared call-argument snapshot surface.
tests/emitted_ada_snapshot.json	Updates emitted Ada snapshot hashes and adds snapshot entries for the new fixture.
README.md	Updates proved fixture/test corpus counts to reflect the new fixture.

---

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

[github-actions]

PR11.23h review

Overall the implementation is correct and consistent with the existing snapshot-replacement discipline. All claimed validation passes. A few items worth flagging:

Snapshot churn in pre-existing shared fixtures

tests/emitted_ada_snapshot.json shows changed hashes for pr1112a_shared_task_build, pr1112e_imported_shared_record_build, pr1112a_shared_field_access, and pr1112b_shared_snapshot — fixtures not directly targeted by this PR. The breadth is explained by Append_Assignment now running the snapshot pass over assignment RHS for all shared-field writes. The PR claims 265 proofs pass (confirming provability), but the roadmap note should mention the wider fixture churn or it will confuse future bisection.

Float narrowing: snapshot collection root vs. base image root

In Append_Assignment, the local helper Render_Shared_Value_From_Image always passes Stmt.Value to Collect_Shared_Condition_Snapshots, but the float-narrowing branch calls it with Render_Expr (Stmt.Value.Inner) as the base image. Correctness depends on: (a) all shared reads found in Stmt.Value appearing verbatim in Render_Expr (Stmt.Value.Inner), and (b) the snapshot collector not generating a replacement key using the outer narrowing wrapper's rendering context. This holds for the current float-narrowing shape, but the assumption is implicit and fragile if the narrowing wrapper ever adds a rendering prefix around the inner shared path.

Rendered_Value_Image empty-string sentinel

Using Rendered_Value_Image'Length > 0 as a "was a pre-rendered image supplied?" sentinel works because a valid Ada expression never renders to the empty string. A Boolean flag would make the intent clearer without adding complexity.

[agentc1]

Addressed in 609dc87. The roadmap now explicitly notes the adjacent shared-wrapper fixtures whose emitted hashes are refreshed by the generalized assignment/call snapshot pass, and the follow-up fixes cover the float-narrowing source/root alignment plus the explicit rendered-image flag. Local pre-push hook passed: 1044 tests passed, 19 samples passed, and 265 proofs passed.

[github-actions]

PR11.23h Review

Overall: correct approach, no logic bugs found. One implementation detail worth verifying.

What was checked

• Render_Call_From_Image declaration order: Target_Subprogram and Needs_Copy_Back are moved earlier so the nested function can capture them. Both are initialised by Find_Called_Subprogram before either Render_Call_From_Image call site is reached. Correct.
• Early-return path (null / zero-arg / getter calls): now routed through Render_Shared_Condition_From_Image on the whole Call_Expr. Snapshot collection traverses callee (no-op for plain identifiers) then args. No-arg shared getter calls land here via the Args.Is_Empty guard and are handled correctly.
• Copy-back path (Skip_Copy_Back_Actuals => True): snapshot declare block is nested inside the existing outer copy-back declare…begin…end at Depth + 1. Valid Ada. Writeback happens after the call in the same outer scope. Copy-back actuals appear in Call_Image as temp-variable names (not getter strings), so Apply_Shared_Condition_Replacements does not touch them.
• Wide-integer assignment: Render_Wide_Expr wraps each Expr_Call/Expr_Ident/Expr_Select node with Safe_Runtime.Wide_Integer (Render_Expr (...)) (expressions.adb:2724-2725), so the raw getter call image is always a substring of the wide image. Replacement correctly targets it.
• Append_Narrowing_Assignment: accepts Rendered_Value_Image/Has_Rendered_Value_Image as trailing defaulted params. All existing callers pass only up to Depth; new callers supply both. Compatible.
• Print path: Render_Print_Argument embeds Render_Expr (arg) as a substring in every type branch (integer, boolean, enum), so the getter call image is always present in Print_Image for replacement.

Item to verify

See inline comment on Append_Shared_Rendered_Statement regarding Snapshots vs Replacements divergence.

[Copilot]

Pull request overview

Copilot reviewed 7 out of 7 changed files in this pull request and generated no new comments.

---

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

[github-actions]

PR11.23h Review

The core design is sound: reusing Collect_Shared_Condition_Snapshots / Apply_Shared_Condition_Replacements as a pre-rendering filter across assignment RHS, call arguments, and print is correct, and the one-snapshot-per-shared-root-per-statement discipline is preserved.

Three issues:

1. Dead Rendered.Replacements update (minor)
   Apply_Shared_Condition_Replacements assigns Rendered.Replacements := Used_Replacements at the end, but no downstream caller reads .Replacements. Both Append_Shared_Rendered_Statement and Append_Shared_Condition_Declarations consume only .Snapshots and .Image. The pruned-replacements vector is computed and stored but never used.

2. Callee collection in Render_Call_From_Image (minor)
   Collect_Shared_Condition_Snapshots is called on Call_Expr.Callee before iterating args. In all expected cases the callee is a resolved function-name identifier (Expr_Ident), so this is a harmless no-op. But it is semantically inconsistent: the callee is a subprogram reference, not a value expression that can contain shared field reads. If a snapshot were somehow collected from the callee, its Call_Image would not appear in Base_Image (which uses the rendered callee name, not a getter call form), so Apply_Shared_Condition_Replacements would silently prune it anyway. Correct by accident rather than by design.

3. Print-path snapshot alignment gap for string-returning shared getters (latent)
   The print path constructs Print_Image via Render_Print_Argument, then collects snapshots from the full Item.Call AST. For integer/boolean/enum arguments Render_Print_Argument embeds Render_Expr (arg) verbatim, so the getter call image appears as a substring in Print_Image and the text replacement succeeds. For string-typed arguments Render_Print_Argument delegates to Render_String_Value_Image / Render_String_Expr, which may not preserve the getter call image as a literal substring. In that case Apply_Shared_Condition_Replacements silently prunes the snapshot and the volatile getter call remains in the emitted Ada. The current fixture only prints integer results so this gap is not exercised.

[github-actions]

Review: PR11.23h shared call-argument snapshot

Overall the refactor is structurally correct and the split of the old Render_Shared_Condition into Render_Shared_Condition_From_Image + Apply_Shared_Condition_Replacements is clean. The print, assignment-RHS, and call-argument paths all close the declare/begin/end block correctly. Two issues below.

Emitted Ada churn on pr1112a, pr1112b, pr1112e, pr1112a_shared_task is expected per the roadmap note and snapshots are regenerated — no concern there.

[Copilot]

Pull request overview

Copilot reviewed 7 out of 7 changed files in this pull request and generated 1 comment.

---

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

[github-actions]

Review: PR11.23h shared call-argument snapshot

Overall: the generalization of the snapshot replacement pass into assignment RHS and standalone call-argument contexts is structurally sound. The collector/replacer split, the pruning pass in Apply_Shared_Condition_Replacements, and the new Append_Shared_Rendered_Statement helper all follow the existing pattern cleanly.

Emitted Ada hash churn — intentional and correctly documented. Five existing fixtures (pr1112a_shared_task_build, pr1112e_imported_shared_record_build, pr1112a_shared_field_access, pr1112b_shared_snapshot, plus the new pr1123h_*) change hash because the pass now wraps shared reads in assignments and print calls with snapshot locals. The roadmap note and verification matrix entry both account for this.

Two items to address:

1. Apply_Shared_Condition_Replacements – Raise_Internal fires on any replacement whose Replacement_Image does not prefix-match a collected snapshot name (see inline). The check in Keep_Replacement_Snapshot scans all snapshots in Rendered.Snapshots for a prefix match; it does not verify that the matched snapshot is the one the collector actually associated with that replacement. If two shared roots ever share a snapshot-name prefix this could silently accept the wrong snapshot and emit the declaration while misidentifying which one is used.

2. Render_Call_From_Image – Params (Arg_Index) lower-bound assumption (see inline). Matches the existing pattern at lines 3238 and 3336, so not a new regression, but the implicit assumption that Args.First_Index = Params.First_Index is now repeated in a third place. Worth adding a comment or a Params.First_Index guard to make the assumption explicit.

No other correctness issues found.

[github-actions]

Review: PR11.23h shared call-argument snapshot

The overall approach is sound — reusing Collect_Shared_Condition_Snapshots across assignment RHS, standalone calls, and print is cleaner than duplicating the snapshot logic, and Apply_Shared_Condition_Replacements's pruning-plus-validation two-guard model (Collect_Replacement_Snapshot catches unpaired snapshots; Require_Shared_Replacements catches missing call images) provides good defence-in-depth.

Two issues flagged inline:

1. Print path: post-render validation order (Render_Statements, Is_Print_Call branch)
Require_Shared_Replacements runs after Render_Shared_Condition_From_Image. If a shared getter's call image is absent from Print_Image, Apply_Shared_Condition_Replacements silently prunes the snapshot and Rendered.Image carries the raw volatile call before the guard fires. The error is still fatal before emission, but the check reads more clearly as a pre-render invariant. See inline comment.

2. Actual.Prefix rendered twice in copy-back path (Growable_Indexed_Element_Image + Growable_Indexed_Writeback_Image)
Both helpers call Render_Expr (Unit, Document, Actual.Prefix, State) independently. The old Append_Growable_Indexed_Writeback rendered it once. If any State mutation triggered by prefix rendering is non-idempotent (beyond the Needs_Safe_Array_RT flag already visible here), the double call will fire it twice. Extracting the rendered prefix at the call site and threading it in as a String parameter would eliminate the risk. See inline comment.

No correctness defects in the snapshot pruning logic, Has_Formal_For_Arg guard, Always_Terminates additions, or the Append_Narrowing_Assignment Rendered_Value_Image default-parameter approach. Emitted-Ada snapshot churn for pr1112a, pr1112b, pr1112e, and pr1110b is expected per the roadmap note.

[github-actions]

Review: PR11.23h shared call argument snapshot

The generalization of the shared-condition snapshot pass into assignment RHS and call-argument contexts is structurally sound, and the pruning logic in Apply_Shared_Condition_Replacements is correct. Three issues below warrant attention before merge.

Correctness

Dead guard in Render_Call_From_Image (line 3181). The if not Target_Subprogram_Resolved then Raise_Internal branch is unreachable: the outer control flow returns early at the if not Target_Subprogram_Resolved or else Call_Expr.Args.Is_Empty gate (line 3312), so Render_Call_From_Image is only ever called when Target_Subprogram_Resolved = True. Dead internal-error paths can mask future caller-site bugs; the check should either be moved to the outer gate or removed.

Impure image functions (lines 3242, 3264). Growable_Indexed_Element_Image and Growable_Indexed_Writeback_Image both assign State.Needs_Safe_Array_RT := True through closure capture, but are named and structured as pure image producers. Callers in constant declarations (e.g. Actual_Value_Image : constant String := Growable_Indexed_Element_Image (...)) cannot signal that the mutation is intentional. If either is ever called in a branch that does not reach the emit path, the flag is set incorrectly. Recommend keeping the mutation at the call site or renaming to Emit_Growable_... to signal the side effect.

Minor / efficiency

Double snapshot collection for print (lines 3885–3900). Require_Shared_Replacements calls Collect_Shared_Condition_Snapshots internally on the print argument, then Render_Shared_Condition_From_Image immediately calls it again on the same expression. The result is correct but the collection runs twice per print statement with a shared argument. Consider folding the require-check into Render_Shared_Condition_From_Image or accepting the redundancy with a comment.

Ada/SPARK stdlib

Always_Terminates added to Replace_Element in both array RT specs — correct addition; the procedure body is bounded by the precondition Index <= Length (Value).

[Copilot]

Pull request overview

Copilot reviewed 9 out of 9 changed files in this pull request and generated 1 comment.

---

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

[github-actions]

Review: PR11.23h shared call-argument snapshot

The structural approach is sound — reusing the existing shared-condition snapshot collector in call-argument and assignment-RHS contexts is the right abstraction, and the copy-back index-temp split correctly avoids snapshotting the mutable write-back prefix.

Two correctness concerns:

[1] Type coercion dropped in copy-back init

The old copy-back path initialized the temp with Render_Expr_For_Target_Type (..., Formal.Type_Info, State), which applies Ada type conversions based on the formal parameter declared type. The replacement Growable_Indexed_Element_Image calls .Element (...) directly without consulting Formal.Type_Info. The new fixture exercises small_value -> small_value (same type), so this gap does not surface there, but if any copy-back formal has a different type than the array element type, the emitted initialization will be missing the explicit Ada conversion and may not prove at level 2.

[2] Missing Require_Shared_Value_Replacements in wide-integer and explicit-float-narrowing assignment branches

The stable float interpolation branch calls Require_Shared_Value_Replacements before rendering, turning image/collector mismatches into immediate internal errors. The wide-integer (Is_Wide_Name) and explicit-float-narrowing (Is_Explicit_Float_Narrowing) branches call Render_Shared_Value_From_Image directly — silently pruning replacements not found in the rendered image via Apply_Shared_Condition_Replacements. If Render_Wide_Expr produces a different string for a getter call than what Collect_Shared_Condition_Snapshots records as Call_Image, the volatile read survives into the emitted Ada and the error defers to GNATprove instead of failing at emit time.

[Copilot]

Pull request overview

Copilot reviewed 9 out of 9 changed files in this pull request and generated no new comments.

---

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

[github-actions]

Review: PR11.23h auto-snapshot shared call arguments

The generalization of the shared-condition snapshot pass into assignment RHS and call argument contexts is structurally sound. Snapshot collection, pruning via Apply_Shared_Condition_Replacements, and re-application via Apply_Shared_Replacements_To_Image follow a consistent pattern across the condition, assignment, print, non-copy-back call, and copy-back call paths. The Uses_Snapshot / Collect_Replacement_Snapshot deduplication logic is correct. Proof counts and snapshot hashes are internally consistent with the claimed 263-fixture inventory.

Three issues worth addressing before merge:

1. Copy_Back_Init_Image missing plain-string element type path (correctness gap)

Copy_Back_Init_Image covers integer, float, and binary types with an explicit subtype conversion and falls through to the raw Element_Image for everything else. Render_Expr_For_Target_Type — which was used prior to this PR — has an additional branch for plain string (heap-string) targets that calls Render_Heap_String_Expr instead of returning the element directly. If a growable array has plain string elements and a formal mode is mut/out/in out, the new path emits the raw .Element(...) result without the heap-string render, producing incorrect Ada. The fixture only exercises integer subtypes; the gap is latent for string-typed growable array elements.

2. pragma Assert (Target_Subprogram_Resolved) in Render_Call_From_Image is dead code

Render_Call_From_Image is only reachable after the early-return guard that exits when not Target_Subprogram_Resolved, so the condition is structurally guaranteed by the call site and the assert never fires on a false value. It provides no protection and could mislead a reader into thinking the function can be called from an unresolved context.

3. Apply_Shared_Condition_Replacements dual-purpose image side-effect (design concern)

The call at line 3597 uses Apply_Shared_Condition_Replacements purely to prune Statement_Rendered.Snapshots and .Replacements; the .Image side-effect (set to the rewritten Combined_Image) is silently discarded. The comment documents this, but a future caller porting this pattern could inadvertently emit Combined_Image if .Image is read. A dedicated Prune_Shared_Snapshots (Rendered, Image) that only touches .Snapshots and .Replacements would make the intent explicit.

[github-actions]

PR11.23h review

Overall the implementation is correct. The snapshot-collect/validate/apply pipeline is consistent across all five new sites (assignment wide, assignment narrowing, stable-float interpolation, standalone call, print). The copy-back path correctly restricts snapshot collection to the index expression only and guards against shared-rooted copy-back prefixes. Always_Terminates on Replace_Element is the right fix for SPARK's interfering-context check on the writeback.

Three things worth attention:

Require_Shared_Replacements for the copy-back index temp always passes (~line 3507). Index_Declaration_Image is constructed by embedding Render_Expr (Unit, Document, Index_Expr, State) directly, so the snapshot collector and renderer use the same Ada text and the call image is guaranteed present. This guard is functionally inert today; it would only fire if the collector and renderer diverged. If retained, a short comment explaining the triggering condition would help distinguish it from the load-bearing Require_Shared_Replacements calls elsewhere.

Apply_Shared_Replacements_To_Image applies replacements sequentially without an anti-chaining comment (~line 2749). Apply_Shared_Condition_Replacements explicitly notes that replacement images must not contain another getter call image to prevent double-substitution. Apply_Shared_Replacements_To_Image -- called at every copy-back emission site -- has no matching comment. The invariant holds by construction, but without the comment the safety assumption is invisible exactly where it matters most for future maintainers.

State.Needs_Safe_IO := True now fires after Render_Print_Argument (~line 3892). Render_Print_Argument does not read Needs_Safe_IO, so the ordering change is harmless today, but it reverses the prior convention where the flag was set before any rendering. Worth a note if the function's state dependencies ever widen.