From 2536b5f535458cd398aa6a9c508d3362b1279ed7 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 1 Jun 2026 00:34:18 +0200 Subject: [PATCH] =?UTF-8?q?plan(mir.4):=20StrRep=20loop-carried=20Str=20?= =?UTF-8?q?=E2=87=92=20Heap,=20delete=20the=20recur=20!is=5Fstr=20gate?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit mir.4 closes bug #49 (a heap-Str loop binder replaced across `recur` leaks every superseded str_concat slab, live=3) structurally rather than with a fourth leg-by-leg patch. Design calls made in planning (folded into the spec as the mir.4 refinement note): - Mechanism: producer-side representation, codegen reads it — the milestone thesis. lower_to_mir sets rep = StrRep::Heap on every MTerm::Str literal that flows into a Str loop-binder alloca (seed inits AND recur args at Str-binder positions); codegen's MTerm::Str arm gains a Heap leg that promotes the static literal via ailang_str_clone (fresh ailang_rc_alloc slab, rc_header refcount 1). No special-casing in the codegen Loop/Recur store arms — the clone is emitted automatically when the Str{Heap} node is lowered. - Recur args are promoted too, not just seeds: `(recur "reset" …)` is well-typed (verified: `ail check` accepts it), and a seed-only promotion would leave a static literal under the now-unconditional dec — a constructible UB hole. Soundness over minimalism on the highest-risk RC/drop surface. - Only the recur dec gate (lib.rs:2231) loses !is_str. The drop.rs loop-RESULT trackability gate (drop.rs:493) STAYS conservative: deleting it needs a broader "every Str a loop can return is owned-heap" guarantee (a static exit-arm literal breaks it) and is not required by the #49 acceptance (the #49 loop result is consumed by print). drop.rs is untouched. - Boundary (out of scope, asserted ill-typed): a borrowed static-Str Var seeded/recur'd into a consumed Str loop binder is rejected upstream by uniqueness (a consumed binder position is owned), so it is not constructible. Plan 0119 carries exact code per step: producer rep promotion + a loop-frame-driven Str-binder mask for recur args (reusing the existing ctx.loop_stack, no new ctx field), the codegen Heap leg, the gate deletion, the #[ignore] lift on the #49 pin, a recur-literal witness fixture + runtime pin proving the recur-arg leg, and the full-suite + ir_snapshot verification. The existing lower_to_mir_ty Static-seed pin flips to assert Heap. --- .../0119-mir.4-strrep-loop-carried-heap.md | 654 ++++++++++++++++++ docs/specs/0060-typed-mir.md | 44 ++ 2 files changed, 698 insertions(+) create mode 100644 docs/plans/0119-mir.4-strrep-loop-carried-heap.md diff --git a/docs/plans/0119-mir.4-strrep-loop-carried-heap.md b/docs/plans/0119-mir.4-strrep-loop-carried-heap.md new file mode 100644 index 0000000..899296b --- /dev/null +++ b/docs/plans/0119-mir.4-strrep-loop-carried-heap.md @@ -0,0 +1,654 @@ +# mir.4 — StrRep: loop-carried `Str` ⇒ Heap — Implementation Plan + +> **Parent spec:** `docs/specs/0060-typed-mir.md` (the mir.4 row at the +> "Iteration decomposition" table + the `> mir.4 refinement` note). +> +> **For agentic workers:** REQUIRED SUB-SKILL: use the `implement` +> skill to run this plan. Steps use `- [ ]` checkboxes for tracking. + +**Goal:** Close bug #49 (a heap-`Str` loop binder replaced across +`recur` leaks every superseded `str_concat` slab) structurally: make +every value in a `Str` loop-binder alloca an owned heap slab, then drop +the `!is_str` carve-out from codegen's recur superseded-value dec gate. +`#49` reaches `live=0`; its `#[ignore]` is lifted. + +**Architecture:** Producer-side representation, codegen reads it (the +milestone thesis). `lower_to_mir` sets `rep = StrRep::Heap` on every +`MTerm::Str` literal flowing into a `Str` loop-binder alloca — both +binder **seed** inits and **recur args** at `Str`-binder positions. +codegen's `MTerm::Str` arm gains a `Heap` leg that promotes the static +literal via `ailang_str_clone` (a fresh `ailang_rc_alloc` slab with an +`rc_header` at refcount 1). With every loop-carried `Str` value now an +owned heap slab, the recur dec gate's `!is_str` clause is deleted — the +superseded-value dec is sound for `Str` exactly as for a boxed ADT. + +**Scope boundary (from the spec refinement):** Only the **recur dec +gate** (`crates/ailang-codegen/src/lib.rs:2231`) loses `!is_str`. The +*other* `!is_str` site — the `MTerm::Loop` arm of `is_rc_heap_allocated` +(`crates/ailang-codegen/src/drop.rs:493`, the loop-**result** +trackability gate) — **stays as-is** in mir.4: deleting it needs a +broader "every `Str` a loop can return is owned-heap" guarantee (a +static exit-arm literal breaks it) and is not required by the #49 +acceptance (the #49 loop result is consumed by `print`). Do **not** +touch `drop.rs`. + +**Tech Stack:** `ailang-check` (`lower_to_mir`), `ailang-codegen` +(`lower_term`), `ailang-mir` (`StrRep` — already defined, both variants +already present), `ail` integration tests, `examples/` fixtures. + +--- + +**Files this plan creates or modifies:** + +- Modify: `crates/ailang-check/src/lower_to_mir.rs` — the `Term::Loop` + arm (seed promotion), the `Term::Recur` arm (recur-arg promotion), a + new `is_str_ty` helper. +- Modify: `crates/ailang-check/tests/lower_to_mir_ty.rs` — flip the + existing Static-seed pin to Heap; add a recur-arg-Heap pin and a + non-loop-stays-Static control pin. +- Create: `examples/loop_str_recur_literal_no_leak_pin.ail` — a `Str` + loop binder whose `recur` rebinds it to a fresh static **literal** + (the recur-arg-promotion witness). +- Modify: `crates/ailang-codegen/src/lib.rs` — the `MTerm::Str` arm + (add the `Heap` leg), the recur dec gate (delete `!is_str`), the + `ailang_mir` use-import (ensure `StrRep`). +- Modify: `crates/ail/tests/loop_recur_str_binder_no_leak_pin.rs` — + lift the `#[ignore]` on the #49 pin, reword its doc to past tense, + append a runtime leak pin for the recur-literal fixture. + +--- + +## Task 1: Producer — `lower_to_mir` Heap-promotes loop-carried `Str` literals + +**Files:** +- Modify: `crates/ailang-check/src/lower_to_mir.rs:367-395` (Loop + Recur arms) + a new helper +- Modify: `crates/ailang-check/tests/lower_to_mir_ty.rs:39-49,219-230` +- Create: `examples/loop_str_recur_literal_no_leak_pin.ail` + +- [ ] **Step 1: Add the `is_str_ty` helper** + +In `crates/ailang-check/src/lower_to_mir.rs`, immediately **above** +`fn lower_term(ctx: &mut Ctx, t: &Term) -> Result {` (currently +line 195), insert: + +```rust +/// True for the `Str` con-type. mir.4 uses it to recognise a +/// loop-binder position whose seed / recur-arg `Str` literals must be +/// promoted to `StrRep::Heap` (an owned heap slab), so codegen's +/// superseded-value dec on the binder alloca is sound. `Type::Con` is +/// the same shape codegen matches at `lib.rs:2232`. +fn is_str_ty(t: &Type) -> bool { + matches!(t, Type::Con { name, .. } if name == "Str") +} +``` + +- [ ] **Step 2: Promote the loop-binder seed in the `Term::Loop` arm** + +In `crates/ailang-check/src/lower_to_mir.rs`, replace the binder-build +loop in the `Term::Loop` arm (currently lines 368-375): + +```rust + let mut m_binders = Vec::with_capacity(binders.len()); + for b in binders { + m_binders.push(MLoopBinder { + name: b.name.clone(), + ty: b.ty.clone(), + init: lower_term(ctx, &b.init)?, + }); + } +``` + +with: + +```rust + let mut m_binders = Vec::with_capacity(binders.len()); + for b in binders { + let mut init = lower_term(ctx, &b.init)?; + // mir.4: a `Str` literal seeding a loop binder must be + // an owned heap slab — the binder alloca is dec'd when a + // later `recur` supersedes it (codegen, lib.rs recur + // arm), and dec'ing a header-less static literal is UB. + // Flip the seed literal's rep to Heap; codegen's + // MTerm::Str arm then promotes it via `str_clone`. + if is_str_ty(&b.ty) { + if let MTerm::Str { rep, .. } = &mut init { + *rep = StrRep::Heap; + } + } + m_binders.push(MLoopBinder { + name: b.name.clone(), + ty: b.ty.clone(), + init, + }); + } +``` + +- [ ] **Step 3: Promote literal recur args in the `Term::Recur` arm** + +In `crates/ailang-check/src/lower_to_mir.rs`, replace the `Term::Recur` +arm (currently lines 389-395): + +```rust + Term::Recur { args } => { + let m_args = args + .iter() + .map(|a| Ok(arg(lower_term(ctx, a)?))) + .collect::>>()?; + MTerm::Recur { args: m_args, ty } + } +``` + +with: + +```rust + Term::Recur { args } => { + // mir.4: a `Str` literal recur arg at a `Str`-binder + // position must be an owned heap slab, for the same reason + // the seed is (the binder alloca is dec'd on the next + // supersede). The innermost loop frame (`loop_stack.last()`, + // the loop this `recur` targets) gives the per-position + // binder types. `(recur "reset" …)` is well-typed, so this + // leg is load-bearing even though #49 itself recurs with a + // `str_concat` (already heap) arg. + let binder_tys: Vec = ctx + .loop_stack + .last() + .map(|frame| frame.iter().map(|(_, t)| t.clone()).collect()) + .unwrap_or_default(); + let m_args = args + .iter() + .enumerate() + .map(|(i, a)| { + let mut m = lower_term(ctx, a)?; + if binder_tys.get(i).map_or(false, is_str_ty) { + if let MTerm::Str { rep, .. } = &mut m { + *rep = StrRep::Heap; + } + } + Ok(arg(m)) + }) + .collect::>>()?; + MTerm::Recur { args: m_args, ty } + } +``` + +- [ ] **Step 4: Create the recur-literal witness fixture** + +Create `examples/loop_str_recur_literal_no_leak_pin.ail`: + +```ail +(module loop_str_recur_literal_no_leak_pin + ; mir.4 (#49 soundness, recur-arg leg): a Str loop binder whose + ; `recur` rebinds it to a fresh static LITERAL each iteration. Without + ; recur-arg Heap promotion the literal "reset" would be stored static + ; into the binder alloca and dec'd on the next supersede — UB on a + ; header-less static. lower_to_mir flips both the seed "x" and the + ; recur literal "reset" to StrRep::Heap, so codegen str_clones each + ; into an owned heap slab; every supersede dec then frees a real slab. + ; Trace: seed slab1("x"); recur0 slab2("reset") decs slab1; recur1 + ; slab3 decs slab2; recur2 slab4 decs slab3; exit acc=slab4, print + ; consumes/frees it. allocs=4 frees=4 live=0. Expected stdout: reset. + (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) + (body + (let s + (loop (acc (con Str) "x") (i (con Int) 0) + (if (app ge i 3) + acc + (recur "reset" (app + i 1)))) + (app print s))))) +``` + +- [ ] **Step 5: Flip the existing Static-seed pin to Heap; add the + recur-arg and control pins** + +In `crates/ailang-check/tests/lower_to_mir_ty.rs`, replace the existing +test (lines 39-49): + +```rust +#[test] +fn str_literal_lowers_to_static_str_node() { + // #49 witness: the loop seed "x" is a Str literal → MTerm::Str, + // rep = Static at mir.1 (mir.4 flips loop seeds to Heap). + let m = "loop_recur_str_binder_no_leak_pin"; + let mir = elaborate_fixture(m); + assert!( + find_static_str_seed(body(&mir, m, "main")), + "loop seed \"x\" must lower to MTerm::Str {{ rep: Static }}" + ); +} +``` + +with: + +```rust +#[test] +fn loop_seed_str_literal_lowers_to_heap_str_node() { + // #49 witness: the loop seed "x" is a Str literal → MTerm::Str. + // mir.4: a loop-carried seed is promoted to rep = Heap so codegen + // emits the str_clone heap promotion and the recur superseded-value + // dec is sound (the prior alloca value is always an owned slab). + let m = "loop_recur_str_binder_no_leak_pin"; + let mir = elaborate_fixture(m); + assert_eq!( + loop_seed_rep(body(&mir, m, "main")), + Some(StrRep::Heap), + "loop seed \"x\" must lower to MTerm::Str {{ rep: Heap }}" + ); +} + +#[test] +fn loop_recur_literal_arg_lowers_to_heap_str_node() { + // mir.4: a literal recur arg at a Str-binder position is promoted + // to rep = Heap, mirroring the seed promotion — `(recur "reset" …)`. + let m = "loop_str_recur_literal_no_leak_pin"; + let mir = elaborate_fixture(m); + assert!( + find_recur_str_arg_with_rep(body(&mir, m, "main"), StrRep::Heap), + "the recur arg literal \"reset\" must lower to MTerm::Str {{ rep: Heap }}" + ); +} + +#[test] +fn non_loop_str_literal_stays_static() { + // Control: a Str literal NOT in a loop-carried position keeps + // rep = Static (no spurious heap promotion). `hello` prints the + // literal "Hello, AILang." via io/print_str. + let m = "hello"; + let mir = elaborate_fixture(m); + assert!( + find_str_node_with_rep(body(&mir, m, "main"), StrRep::Static), + "a non-loop Str literal must stay MTerm::Str {{ rep: Static }}" + ); +} +``` + +- [ ] **Step 6: Replace the `find_static_str_seed` helper with + rep-parameterised walkers** + +In `crates/ailang-check/tests/lower_to_mir_ty.rs`, replace the +`find_static_str_seed` helper (lines 219-230): + +```rust +fn find_static_str_seed(t: &MTerm) -> bool { + match t { + MTerm::Loop { binders, body, .. } => { + binders.iter().any(|b| matches!( + &b.init, + MTerm::Str { rep: StrRep::Static, .. } + )) || find_static_str_seed(body) + } + MTerm::Let { init, body, .. } => { + find_static_str_seed(init) || find_static_str_seed(body) + } + _ => false, + } +} +``` + +with: + +```rust +/// The rep of the first loop binder seed that is an `MTerm::Str`, +/// searching `Let`-init / `Let`-body / the loop's own binders. +fn loop_seed_rep(t: &MTerm) -> Option { + match t { + MTerm::Loop { binders, body, .. } => binders + .iter() + .find_map(|b| match &b.init { + MTerm::Str { rep, .. } => Some(*rep), + _ => None, + }) + .or_else(|| loop_seed_rep(body)), + MTerm::Let { init, body, .. } => { + loop_seed_rep(init).or_else(|| loop_seed_rep(body)) + } + _ => None, + } +} + +/// True if any `Recur` arg in `t` is an `MTerm::Str` with the given rep. +fn find_recur_str_arg_with_rep(t: &MTerm, want: StrRep) -> bool { + match t { + MTerm::Recur { args, .. } => args.iter().any(|a| matches!( + &a.term, MTerm::Str { rep, .. } if *rep == want + )), + MTerm::Loop { binders, body, .. } => { + binders.iter().any(|b| find_recur_str_arg_with_rep(&b.init, want)) + || find_recur_str_arg_with_rep(body, want) + } + MTerm::Let { init, body, .. } => { + find_recur_str_arg_with_rep(init, want) + || find_recur_str_arg_with_rep(body, want) + } + MTerm::If { cond, then, else_, .. } => { + find_recur_str_arg_with_rep(cond, want) + || find_recur_str_arg_with_rep(then, want) + || find_recur_str_arg_with_rep(else_, want) + } + _ => false, + } +} + +/// True if any `MTerm::Str` reachable in `t` carries the given rep +/// (used by the non-loop control: a plain literal stays Static). +fn find_str_node_with_rep(t: &MTerm, want: StrRep) -> bool { + match t { + MTerm::Str { rep, .. } => *rep == want, + MTerm::Let { init, body, .. } => { + find_str_node_with_rep(init, want) || find_str_node_with_rep(body, want) + } + MTerm::App { args, .. } => { + args.iter().any(|a| find_str_node_with_rep(&a.term, want)) + } + MTerm::Do { args, .. } => { + args.iter().any(|a| find_str_node_with_rep(&a.term, want)) + } + MTerm::If { cond, then, else_, .. } => { + find_str_node_with_rep(cond, want) + || find_str_node_with_rep(then, want) + || find_str_node_with_rep(else_, want) + } + _ => false, + } +} +``` + +> **Implementer note — the `MTerm` field shapes the walkers rely on +> (verified against `crates/ailang-mir/src/lib.rs`):** `MTerm::App`, +> `MTerm::Do`, and `MTerm::Recur` all carry `args: Vec` (the inner +> term is `a.term`) — `Do` is `{ op, args, tail, ty }` (lib.rs:92), and +> `find_app_with_fn` at lower_to_mir_ty.rs:209 already uses `&a.term` for +> `App`. `MTerm::If` fields are `cond`/`then`/`else_`. `hello`'s +> `(do io/print_str "Hello, AILang.")` lowers to `MTerm::Do` whose arg +> `.term` is the `MTerm::Str` literal — reached by the `Do` arm of +> `find_str_node_with_rep`. The assertion (a non-loop literal stays +> `Static`) is what must hold. + +- [ ] **Step 7: Run the producer test suite** + +Run: `cargo test -p ailang-check --test lower_to_mir_ty` +Expected: PASS — all tests green, including the three new/flipped pins +(`loop_seed_str_literal_lowers_to_heap_str_node`, +`loop_recur_literal_arg_lowers_to_heap_str_node`, +`non_loop_str_literal_stays_static`). No test named +`str_literal_lowers_to_static_str_node` remains. + +--- + +## Task 2: Codegen — `MTerm::Str` Heap leg + delete the recur `!is_str` gate + +**Files:** +- Modify: `crates/ailang-codegen/src/lib.rs:1674-1690` (Str arm), + `:2229-2235` (recur gate), the `ailang_mir` use-import. + +- [ ] **Step 1: Ensure `StrRep` is imported** + +Run: `git grep -n "use ailang_mir::" crates/ailang-codegen/src/lib.rs` +If the import list does not already include `StrRep`, add it (alongside +`MTerm`, `Mode`, `Callee`, …). The arm in Step 2 references +`StrRep::Static` / `StrRep::Heap`. + +- [ ] **Step 2: Add the `Heap` leg to the `MTerm::Str` arm** + +In `crates/ailang-codegen/src/lib.rs`, replace the `MTerm::Str` arm +(lines 1674-1690): + +```rust + MTerm::Str { lit, .. } => { + // language `Str` literals materialise as + // a constexpr-GEP into the packed-struct global, + // landing on the `len`-field (now the first field, + // since the hs.1-era sentinel rc-header slot was + // removed). IR-Str pointer carries len at 0, bytes + // at +8. The `rep` field is not consumed at mir.1b + // (mir.4 wires the heap-vs-static representation hook). + let g = self.intern_str_literal("str", lit); + let total = c_byte_len(lit); // bytes + NUL + Ok(( + format!( + "getelementptr inbounds (<{{ i64, [{total} x i8] }}>, ptr @{g}, i32 0, i32 0)", + ), + "ptr".into(), + )) + } +``` + +with: + +```rust + MTerm::Str { lit, rep } => { + // language `Str` literals materialise as a constexpr-GEP + // into the packed-struct global, landing on the `len` + // field (the first field). IR-Str pointer carries len at + // 0, bytes at +8. + let g = self.intern_str_literal("str", lit); + let total = c_byte_len(lit); // bytes + NUL + let gep = format!( + "getelementptr inbounds (<{{ i64, [{total} x i8] }}>, ptr @{g}, i32 0, i32 0)", + ); + match rep { + // Static: a constexpr-GEP into the rodata global, no + // rc_header — the default for every non-loop-carried + // literal. Never RC-dec'd (see drop.rs Str note). + StrRep::Static => Ok((gep, "ptr".into())), + // mir.4: a loop-carried Str literal (seed or recur + // arg, flipped to Heap by lower_to_mir) must be an + // owned heap slab so the recur superseded-value dec + // is sound. Promote via `ailang_str_clone`, which + // deep-copies into a fresh `ailang_rc_alloc` slab + // (rc_header refcount 1 — runtime/str.c). The GEP is + // a valid constexpr operand; str_clone reads `len` at + // offset 0 (ABI-shared between static and heap Str). + StrRep::Heap => { + let dst = self.fresh_ssa(); + self.body.push_str(&format!( + " {dst} = call ptr @ailang_str_clone(ptr {gep})\n" + )); + Ok((dst, "ptr".into())) + } + } + } +``` + +> **Implementer note:** `@ailang_str_clone` is unconditionally declared +> at `crates/ailang-codegen/src/lib.rs:595` +> (`declare ptr @ailang_str_clone(ptr)`), so the `Heap` leg needs no +> conditional declaration. `self.fresh_ssa()` and `self.body.push_str` +> are the same primitives the `str_clone` builtin arm uses at `:2592`. + +- [ ] **Step 3: Delete the `!is_str` clause from the recur dec gate** + +In `crates/ailang-codegen/src/lib.rs`, replace the gate region of the +`MTerm::Recur` arm (lines 2216-2235 — the `// Bug #49:` comment through +the `if matches!(…) && is_ptr && !is_str {` line): + +```rust + // Bug #49: this `recur` REPLACES the binder's prior + // heap value with `arg_ssa`. Without a dec here the + // superseded value leaks every iteration (the + // scope-close path in drop.rs only ever sees the + // loop's FINAL result). Dec the prior value iff the + // binder type is RC-heap-and-not-Str — the SAME gate + // the scope-close drop path uses (lowers to `ptr` AND + // not Str; the Str exclusion is the static-literal + // representation rule from commit 8bcdae1: a `Str` + // loop seed may be a static global with no rc_header, + // so dec'ing it is UB). Primitives (Int/Bool/Float/ + // Unit) lower to non-`ptr` and are excluded by the + // `ptr` gate. + let is_ptr = + matches!(llvm_type(ail_ty).as_deref(), Ok("ptr")); + let is_str = matches!( + ail_ty, + Type::Con { name, .. } if name == "Str" + ); + if matches!(self.alloc, AllocStrategy::Rc) && is_ptr && !is_str { +``` + +with: + +```rust + // Bug #49: this `recur` REPLACES the binder's prior + // heap value with `arg_ssa`. Without a dec here the + // superseded value leaks every iteration (the + // scope-close path in drop.rs only ever sees the + // loop's FINAL result). Dec the prior value iff the + // binder lowers to an RC-heap `ptr`. mir.4 removed + // the former `!is_str` carve-out: lower_to_mir now + // promotes every loop-carried `Str` literal (seed + + // recur args) to `StrRep::Heap`, so a `Str` loop + // binder alloca always holds an owned heap slab with + // an `rc_header` — the dec is sound for `Str` exactly + // as for a boxed ADT. (drop.rs's loop-RESULT + // trackability gate keeps its own `Str` carve-out — + // see spec 0060 mir.4 refinement.) Primitives + // (Int/Bool/Float/Unit) lower to non-`ptr` and are + // excluded by the `ptr` gate. + let is_ptr = + matches!(llvm_type(ail_ty).as_deref(), Ok("ptr")); + if matches!(self.alloc, AllocStrategy::Rc) && is_ptr { +``` + +> **Implementer note:** removing the `is_str` binding may make `Type` +> unused *in this arm*, but `ail_ty: &Type` is still consumed by +> `llvm_type(ail_ty)` and `field_drop_call(ail_ty)` just below, so the +> `Type` import stays. Do not remove it. The same-pointer guard, the +> `do_dec`/`after` blocks, `field_drop_call`, and the plain `store` +> (lines 2236-2268) are unchanged — they now run for `Str` binders too. + +- [ ] **Step 4: Compile gate** + +Run: `cargo build --workspace` +Expected: PASS — 0 errors (no unused-variable warning for `is_str`, +which is now deleted). Runtime behaviour is verified in Task 3 / Task 4. + +--- + +## Task 3: Lift the `#[ignore]` on the #49 pin + +**Files:** +- Modify: `crates/ail/tests/loop_recur_str_binder_no_leak_pin.rs:104-114` + +- [ ] **Step 1: Remove the `#[ignore]` and reword the doc to past tense** + +In `crates/ail/tests/loop_recur_str_binder_no_leak_pin.rs`, replace the +doc-comment + attributes of the #49 test (lines 102-114): + +```rust +/// The bug under test: a heap-Str loop binder replaced by `recur` leaks +/// every superseded `str_concat` slab. RED at HEAD (live=3). +/// +/// Ignored pending the #49 representation spec: the fix is not a +/// mechanical patch — closing the leak for ALL Str loop-carried state +/// (the per-iteration intermediates, the loop result, and a phi-join of +/// static/heap Str) requires a deliberate "every Str in loop-carried +/// state is heap" representation decision, routed through `brainstorm`. +/// This `#[ignore]` keeps `main` green while that cycle runs; the GREEN +/// implementation removes it. The assertion (the contract) is unchanged. +#[test] +#[ignore = "RED until the #49 Str-loop-binder representation fix lands (see brainstorm spec)"] +fn alloc_rc_str_loop_binder_replaced_by_recur_does_not_leak() { +``` + +with: + +```rust +/// The #49 fix (mir.4): a heap-Str loop binder replaced by `recur` no +/// longer leaks its superseded `str_concat` slabs. `lower_to_mir` +/// promotes the loop-carried Str seed to `StrRep::Heap` so codegen +/// `str_clone`s it into an owned heap slab, and the recur dec gate +/// (`crates/ailang-codegen/src/lib.rs`) dropped its `!is_str` carve-out +/// — so each superseded slab is RC-dec'd at the recur store. Was RED at +/// `live=3` before mir.4; now `live=0`. +#[test] +fn alloc_rc_str_loop_binder_replaced_by_recur_does_not_leak() { +``` + +- [ ] **Step 2: Run the #49 pin file** + +Run: `cargo test -p ail --test loop_recur_str_binder_no_leak_pin` +Expected: PASS — both tests green: +`alloc_rc_str_loop_binder_replaced_by_recur_does_not_leak` (now +un-ignored: stdout `xyyy`, `live=0`, `allocs==frees`) and the GREEN +guard `alloc_rc_adt_loop_binder_replaced_by_recur_stays_leak_clean`. +0 ignored in this file. + +--- + +## Task 4: Runtime leak pin for the recur-literal witness + +**Files:** +- Modify: `crates/ail/tests/loop_recur_str_binder_no_leak_pin.rs` + (append a GREEN test, after the existing tests, before EOF) + +- [ ] **Step 1: Append the recur-literal runtime pin** + +In `crates/ail/tests/loop_recur_str_binder_no_leak_pin.rs`, append at +end of file (after +`alloc_rc_adt_loop_binder_replaced_by_recur_stays_leak_clean`): + +```rust +/// mir.4 soundness, recur-arg leg: a Str loop binder whose `recur` +/// rebinds it to a fresh static LITERAL each iteration. This is the case +/// the seed-only promotion would miss — the recur literal "reset" must +/// also be Heap-promoted so its supersede dec frees a real slab instead +/// of UB-dec'ing a header-less static. stdout `reset`, `live=0`. +#[test] +fn alloc_rc_str_loop_binder_recur_literal_does_not_leak() { + let (allocs, frees, live, stdout) = + build_run_stats("loop_str_recur_literal_no_leak_pin.ail"); + assert_eq!( + stdout.trim_end(), + "reset", + "recur-literal loop result mis-built (allocs={allocs} frees={frees} live={live})" + ); + assert_eq!( + live, 0, + "a Str loop binder recur'd with a static literal leaks {live} \ + superseded slab(s) (allocs={allocs} frees={frees}); the recur \ + literal must be Heap-promoted (StrRep::Heap) like the seed." + ); + assert_eq!( + allocs, frees, + "recur-literal leg alloc/free mismatch (allocs={allocs} frees={frees} live={live})" + ); +} +``` + +- [ ] **Step 2: Run the recur-literal pin** + +Run: `cargo test -p ail --test loop_recur_str_binder_no_leak_pin alloc_rc_str_loop_binder_recur_literal_does_not_leak` +Expected: PASS — stdout `reset`, `live=0`, `allocs==frees`. + +--- + +## Task 5: Full verification — no snapshot drift, whole suite green + +**Files:** none (verification only). + +- [ ] **Step 1: IR snapshots must not drift** + +Run: `cargo test -p ail --test ir_snapshot` +Expected: PASS — no snapshot drift. The five snapshot programs +(`hello`, `list`, `max3`, `sum`, `ws_main`) carry no loop-carried `Str` +binder, so the Heap promotion does not reach them. If a snapshot *does* +shift, STOP and investigate — a shift means the `Heap` leg leaked onto a +non-loop-carried literal (an over-promotion bug in Task 1). + +- [ ] **Step 2: The boxed-ADT recur-dec guards must stay green** + +Run: `cargo test -p ail --test loop_recur_heap_binder_no_leak_pin` +Expected: PASS — +`alloc_rc_heap_loop_binder_replaced_by_recur_does_not_leak` green +(the f488d31 ADT leg the Str fix must not regress). + +- [ ] **Step 3: Whole workspace suite** + +Run: `cargo test --workspace` +Expected: PASS — every crate green. Per memory +`project_typed_mir_resynth_strictness`, run the FULL workspace, not just +`e2e`: a Str-representation change can surface in `show_print_e2e`, +`str_concat_e2e`, `print_no_leak_pin`, or the prelude-driven +`lower_to_mir_ty` walk. Confirm the previously-`#[ignore]`d #49 pin is +no longer counted as ignored (the ignored count drops by 1 versus the +mir.3b baseline: the two remaining ignores are doctests, not this test). diff --git a/docs/specs/0060-typed-mir.md b/docs/specs/0060-typed-mir.md index aa82ff3..b511601 100644 --- a/docs/specs/0060-typed-mir.md +++ b/docs/specs/0060-typed-mir.md @@ -352,6 +352,50 @@ class and deletes the matching codegen re-derivation. > not mir.5 — the mir.5 row's "last re-derivation residue" shrinks to > the element-type / `Term::New` (`New.elem`) work. +> mir.4 refinement (discovered in planning + recon, `docs/plans/0119-mir.4-strrep-loop-carried-heap.md`): +> The `!is_str` deletion is scoped to the **recur superseded-value dec +> gate** (`crates/ailang-codegen/src/lib.rs:2231`, the gate the row +> names by "recur dec gate"). The *other* `!is_str` site — the +> `MTerm::Loop` arm of `is_rc_heap_allocated` +> (`crates/ailang-codegen/src/drop.rs:493`, the loop-**result** +> trackability gate) — **stays conservative** in mir.4: deleting it +> would require every `Str` a loop can *return* to be owned-heap, which +> a loop's non-`recur` exit arm (`(if … "done" (recur …))`, a static +> exit literal) does not guarantee — a strictly larger representation +> change with its own static-`Str`-dec UB hole, and not required by the +> #49 acceptance (the #49 loop result is consumed by `print`, so the +> result gate is never exercised). +> +> **Mechanism (producer-side rep, codegen reads it — the milestone +> thesis applied):** `lower_to_mir` sets `rep = StrRep::Heap` on every +> `MTerm::Str` **literal that flows into a `Str` loop-binder alloca** — +> both the binder **seed** inits (the `Term::Loop` arm) AND the +> **recur args** at `Str`-binder positions (a per-loop `Str`-binder mask +> threaded on the lowering ctx, stacked for nested loops; the #49 +> program has only the seed literal, but a literal `recur` arg — +> `(recur "reset" …)` — is well-typed and would be a static value under +> the now-unconditional dec, so it must be promoted too). codegen's +> `MTerm::Str` arm (`lib.rs:1674`, today `{ lit, .. }` ignoring `rep`) +> gains a `Heap` leg: emit the interned static GEP, then +> `call ptr @ailang_str_clone(ptr )` — a fresh heap slab with an +> `rc_header` at refcount 1 (`runtime/str.c:211`). **No** special-casing +> in the codegen Loop/Recur store arms: the `str_clone` is emitted +> automatically when the `MTerm::Str{Heap}` node is lowered. This +> establishes the invariant **every value in a `Str` loop-binder alloca +> is an owned heap slab**, making the unconditional superseded-value dec +> at the recur gate sound (the prior value is always RC-tracked). The +> same-pointer guard (`lib.rs:2248`) still elides the identity-thread +> `(recur acc …)` case. +> +> **Boundary (out of scope, asserted ill-typed):** a **borrowed +> static-`Str` `Var`** seeded or recur'd into a *consumed* (dec'd) `Str` +> loop binder has no `rep` field to flip and would leave a static value +> under the unconditional dec. This is rejected upstream by uniqueness +> — a consumed loop-binder position is owned, and a borrowed `Str` `Var` +> there is a mode violation — so it is not constructible; the only owned +> `Str` values reaching such a binder are literals (promoted here) and +> already-heap expressions (`str_concat`, explicit `clone`). + mir.5 carries the ledger work as part of the milestone (per CLAUDE.md: contract changes ship with the iteration that needs them):