iter eob.1: effect-op args walk as Borrow; heap-Str RC discipline closes
Language rule: Term::Do.args[*] are walked in Position::Borrow by
the uniqueness + linearity passes, symmetric to Term::Ctor.args[*]
being walked in Position::Consume. The kind itself carries the
ownership default — no per-op field on EffectOpSig. Three
analyser sites flip in lockstep: uniqueness.rs:289, linearity.rs:506,
and the shared doc-comment at linearity.rs:42.
Heap-Str-specific consequences (closing hs.4's leak):
- int_to_str / float_to_str ret_mode: Implicit → Own at four lockstep
sites (builtins.rs:200,210 + synth.rs:172,179). The codegen
trackability gate (drop.rs:464-475, iter 18g.2) now fires on these
callees, so the let-binder receives a scope-close drop.
- drop_symbol_for_binder's App arm gets a Type::Con{name:"Str"} →
"ailang_rc_dec" carve-out, symmetric to field_drop_call's existing
Str arm. Without it, the new Own-trackable App binder would emit
drop_<m>_Str (undefined).
Tests: the two pre-existing RED tests at e2e.rs (commit 592d87b)
flip to GREEN unchanged with predicted numbers (allocs=1,frees=1,
live=0 and allocs=2,frees=2,live=0). Two new positive tests pin
the rule's coverage: primitive-Int arg through io/print_int produces
zero RC traffic; heap-Str through 2× io/print_str in sequence
typechecks (no use-after-consume) and balances allocs=1,frees=1,
live=0.
DESIGN.md §Decision 10 gets the arg-position-policy table for both
AST node kinds (Ctor=Consume, Do=Borrow) plus a linking paragraph
explaining how Do=Borrow cooperates with ret_mode==Own.
heap-str-abi milestone closes here: WhatsNew entry shipped (Strings
produced at runtime now release cleanly), roadmap P1 entry checked
off, Post-22-Prelude depends-on line removed.
Workspace cargo test + cross_lang.py + compile_check.py all green.
check.py noisy latency cluster + bench_list_sum.bump_s ±12% — same
precedent as the previous two audits, not coupled to this milestone.
This commit is contained in:
@@ -2622,3 +2622,36 @@ fn str_field_in_adt_drops_heap_str_correctly() {
|
||||
assert_eq!(allocs, frees, "every RC slab must be freed; allocs={allocs}, frees={frees}");
|
||||
assert_eq!(live, 0, "no leaked RC slabs allowed; live={live}");
|
||||
}
|
||||
|
||||
/// Iter eob.1: primitive-Int arg passed to an effect-op. Under the
|
||||
/// new "Term::Do args = Borrow" rule, the let-binder `n` is not
|
||||
/// consumed by `io/print_int`; but Int is unboxed, so there is no
|
||||
/// pointer to RC-track. Pin: zero allocs / zero frees / zero live —
|
||||
/// the rule introduces no spurious bookkeeping on primitives.
|
||||
#[test]
|
||||
fn int_arg_to_effect_op_does_not_rc_track() {
|
||||
let (stdout, allocs, frees, live) =
|
||||
build_and_run_with_rc_stats("int_to_print_int_borrow.ail.json");
|
||||
assert_eq!(stdout, "7\n");
|
||||
assert_eq!(allocs, 0, "Int arg should not trigger any RC alloc; got allocs={allocs}");
|
||||
assert_eq!(frees, 0, "Int arg should not trigger any RC free; got frees={frees}");
|
||||
assert_eq!(live, 0, "no leaked RC slabs allowed; live={live}");
|
||||
}
|
||||
|
||||
/// Iter eob.1: heap-Str let-binder consumed by two `io/print_str`
|
||||
/// calls in sequence. Pins the linearity-side consequence of the new
|
||||
/// rule: under the old Position::Consume walk for Term::Do args, the
|
||||
/// second print would have triggered `use-after-consume`. Under the
|
||||
/// new Position::Borrow walk, both calls are borrows and the program
|
||||
/// typechecks. Under --alloc=rc the slab is allocated once by
|
||||
/// int_to_str, lives through both prints, and is freed exactly once
|
||||
/// at scope close — allocs == 1, frees == 1, live == 0.
|
||||
#[test]
|
||||
fn heap_str_repeated_print_balances_rc_stats() {
|
||||
let (stdout, allocs, frees, live) =
|
||||
build_and_run_with_rc_stats("heap_str_repeated_print_borrow.ail.json");
|
||||
assert_eq!(stdout, "42\n42\n");
|
||||
assert_eq!(allocs, 1, "expected exactly one heap-Str slab; got allocs={allocs}");
|
||||
assert_eq!(frees, 1, "expected exactly one free; got frees={frees}");
|
||||
assert_eq!(live, 0, "no leaked heap-Str slabs allowed; live={live}");
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user