plan: hs.2 — runtime sentinel + Str-in-ADT drop safety, 3 tasks
Second iter of the heap-Str ABI milestone. Adds the UINT64_MAX sentinel-header short-circuit to ailang_rc_inc / ailang_rc_dec so the hs.1 packed-struct globals (whose first slot is i64 -1) flow safely through generic RC paths. Tasks: (1) author rc_str_field_in_adt_static.ail.json + confirm builds; (2) TDD cycle for the safety test + runtime guards; (3) full regression sweep.
This commit is contained in:
@@ -0,0 +1,418 @@
|
||||
# hs.2 — Heap-Str ABI: runtime sentinel + Str-in-ADT drop safety — Implementation Plan
|
||||
|
||||
> **Parent spec:** `docs/specs/2026-05-12-heap-str-abi.md`
|
||||
>
|
||||
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
|
||||
> to run this plan. Steps use `- [ ]` checkboxes for tracking.
|
||||
|
||||
**Goal:** Make `ailang_rc_inc` and `ailang_rc_dec` short-circuit on
|
||||
a `UINT64_MAX` sentinel header, so the static-`Str` slabs emitted
|
||||
by hs.1's packed-struct layout (whose first slot is `i64 -1`) flow
|
||||
safely through generic RC paths instead of attempting to write
|
||||
back to `.rodata` memory. Add the load-bearing safety test
|
||||
`str_field_in_adt_drops_static_str_noop`, which is the first test
|
||||
in the project to exercise the path "ADT with a `Str` field,
|
||||
instantiated with a static literal, dropped under `--alloc=rc`".
|
||||
|
||||
**Architecture:** Pure runtime-side change plus one new fixture
|
||||
and one new e2e test. The hs.1 codegen change emits static-Str
|
||||
globals whose first `i64` slot is `-1` (= `UINT64_MAX` when read
|
||||
as `uint64_t`). The hs.1 IR-Str-pointer convention places the
|
||||
flowing pointer at the `len`-field of the struct, so
|
||||
`header_of(payload) = payload - 8` lands on that sentinel slot.
|
||||
Pre-hs.2, `ailang_rc_dec(static_str_field_ptr)` reads
|
||||
`*hdr = UINT64_MAX` (passes the underflow check at `runtime/rc.c:166`
|
||||
since `UINT64_MAX != 0`), then `*hdr -= 1` attempts to write
|
||||
`UINT64_MAX - 1` to the read-only data section → SIGSEGV. hs.2
|
||||
inserts a sentinel check that short-circuits both functions
|
||||
before either reads or writes the header value any further, making
|
||||
the static-`Str` case a defined no-op. `ailang_rc_alloc`'s counters
|
||||
are untouched on the short-circuit path (`g_rc_alloc_count` only
|
||||
fires inside `ailang_rc_alloc` itself; `g_rc_free_count` only fires
|
||||
on the to-zero branch in `ailang_rc_dec`, after the sentinel check)
|
||||
— so `AILANG_RC_STATS`-based tests continue to report accurate
|
||||
allocs/frees for the heap path while seeing zero traffic from
|
||||
static `Str` literals.
|
||||
|
||||
**Tech Stack:** C runtime (`runtime/rc.c`), AILang fixture
|
||||
(`examples/`), Rust e2e harness (`crates/ail/tests/e2e.rs`).
|
||||
|
||||
---
|
||||
|
||||
## Files this plan creates or modifies
|
||||
|
||||
- **Create:** `examples/rc_str_field_in_adt_static.ail.json` — new
|
||||
fixture mirroring `examples/rc_box_drop.ail.json` shape with a
|
||||
`Str` field in place of an `Int` field. Exercises the
|
||||
static-`Str`-in-ADT drop path under `--alloc=rc`.
|
||||
- **Modify:** `runtime/rc.c:132-145` — add sentinel-header
|
||||
short-circuit to `ailang_rc_inc`.
|
||||
- **Modify:** `runtime/rc.c:161-177` — add sentinel-header
|
||||
short-circuit to `ailang_rc_dec`.
|
||||
- **Test:** `crates/ail/tests/e2e.rs` (append at end of file, after
|
||||
current line 2561) — new test `str_field_in_adt_drops_static_str_noop`
|
||||
using the existing `build_and_run_with_rc_stats` helper at
|
||||
`crates/ail/tests/e2e.rs:2093-2150`.
|
||||
|
||||
---
|
||||
|
||||
## Task 1: Author the static-Str-in-ADT fixture and confirm it builds
|
||||
|
||||
The new test in Task 2 requires a `.ail.json` fixture exercising
|
||||
`type StrBox = | MkStrBox(Str)` with a static-`Str` payload under
|
||||
`--alloc=rc`. This task creates that fixture and confirms it
|
||||
typechecks and builds without errors (running the binary is
|
||||
deferred to Task 2 — pre-hs.2 the binary would crash under
|
||||
`--alloc=rc`).
|
||||
|
||||
**Files:**
|
||||
- Create: `examples/rc_str_field_in_adt_static.ail.json`
|
||||
|
||||
- [ ] **Step 1: Create the fixture.**
|
||||
|
||||
Write the file at `examples/rc_str_field_in_adt_static.ail.json`
|
||||
with this exact content, modelled verbatim on
|
||||
`examples/rc_box_drop.ail.json` with `Int` → `Str` and
|
||||
`io/print_int` → `io/print_str`:
|
||||
|
||||
```json
|
||||
{
|
||||
"schema": "ailang/v0",
|
||||
"name": "rc_str_field_in_adt_static",
|
||||
"imports": [],
|
||||
"defs": [
|
||||
{
|
||||
"kind": "type",
|
||||
"name": "StrBox",
|
||||
"vars": [],
|
||||
"doc": "Single-cell ADT around a Str. Iter hs.2 RC fixture: exercises the static-Str-in-ADT drop path under --alloc=rc. Pre-hs.2 the binary segfaults at drop time because `ailang_rc_dec(static_str_payload_ptr)` reads UINT64_MAX from the sentinel header slot and attempts to write UINT64_MAX-1 to .rodata. Post-hs.2 `ailang_rc_dec` short-circuits on the sentinel; the drop is a defined no-op and the outer StrBox cell frees normally.",
|
||||
"ctors": [
|
||||
{
|
||||
"name": "MkStrBox",
|
||||
"fields": [{ "k": "con", "name": "Str" }]
|
||||
}
|
||||
]
|
||||
},
|
||||
{
|
||||
"kind": "fn",
|
||||
"name": "main",
|
||||
"type": {
|
||||
"k": "fn",
|
||||
"params": [],
|
||||
"ret": { "k": "con", "name": "Unit" },
|
||||
"effects": ["IO"]
|
||||
},
|
||||
"params": [],
|
||||
"doc": "Bind a heap-allocated MkStrBox(\"hello\") to `b`, read its Str via match, print it. Under --alloc=rc the let-scope close calls drop_t_StrBox(b), which in turn calls ailang_rc_dec on the Str field — that pointer is the static-Str literal global from hs.1, so the sentinel-header short-circuit must make this safe.",
|
||||
"body": {
|
||||
"t": "let",
|
||||
"name": "b",
|
||||
"value": {
|
||||
"t": "ctor",
|
||||
"type": "StrBox",
|
||||
"ctor": "MkStrBox",
|
||||
"args": [{ "t": "lit", "lit": { "kind": "str", "value": "hello" } }]
|
||||
},
|
||||
"body": {
|
||||
"t": "match",
|
||||
"scrutinee": { "t": "var", "name": "b" },
|
||||
"arms": [
|
||||
{
|
||||
"pat": {
|
||||
"p": "ctor",
|
||||
"ctor": "MkStrBox",
|
||||
"fields": [{ "p": "var", "name": "s" }]
|
||||
},
|
||||
"body": {
|
||||
"t": "do",
|
||||
"op": "io/print_str",
|
||||
"args": [{ "t": "var", "name": "s" }]
|
||||
}
|
||||
}
|
||||
]
|
||||
}
|
||||
}
|
||||
}
|
||||
]
|
||||
}
|
||||
```
|
||||
|
||||
- [ ] **Step 2: Confirm the fixture typechecks.**
|
||||
|
||||
Run: `cargo run --bin ail --quiet -- check examples/rc_str_field_in_adt_static.ail.json`
|
||||
Expected: exit 0, no diagnostics on stderr. The fixture follows
|
||||
the canonical-form schema verbatim; any diagnostic would indicate
|
||||
a copy-paste error.
|
||||
|
||||
- [ ] **Step 3: Confirm the fixture builds under `--alloc=rc`.**
|
||||
|
||||
Run: `cargo run --bin ail --quiet -- build examples/rc_str_field_in_adt_static.ail.json --alloc=rc -o /tmp/hs2_fixture_build_check`
|
||||
Expected: exit 0; a binary appears at `/tmp/hs2_fixture_build_check`.
|
||||
**Do NOT execute the binary in this step** — pre-hs.2 it segfaults
|
||||
on the static-Str field drop. The Task 2 RED-test step runs it.
|
||||
|
||||
---
|
||||
|
||||
## Task 2: Sentinel-header short-circuit in `ailang_rc_inc` and `ailang_rc_dec` (TDD)
|
||||
|
||||
This is the heart of the iter. The RED test is the
|
||||
spec's load-bearing `str_field_in_adt_drops_static_str_noop`
|
||||
safety gate — until hs.2's runtime change lands, no test in the
|
||||
project exercises this path, and the path is latent UB.
|
||||
|
||||
**Files:**
|
||||
- Modify: `runtime/rc.c:132-145, 161-177`
|
||||
- Test: `crates/ail/tests/e2e.rs` (append after current line 2561)
|
||||
|
||||
- [ ] **Step 1: Write the failing test `str_field_in_adt_drops_static_str_noop`.**
|
||||
|
||||
Append to `crates/ail/tests/e2e.rs` at the end of the file:
|
||||
|
||||
```rust
|
||||
/// Iter hs.2 load-bearing safety gate. The hs.1 layout migration
|
||||
/// turned the path "ADT-with-Str-field instantiated with a static
|
||||
/// literal, dropped under --alloc=rc" into latent UB: the
|
||||
/// per-type drop fn calls `ailang_rc_dec(field_ptr)` on the
|
||||
/// static-Str payload pointer, which under hs.1 lands on the
|
||||
/// `len`-field of the packed-struct global; `header_of(ptr) =
|
||||
/// ptr - 8` reads the sentinel slot (= UINT64_MAX); the
|
||||
/// underflow check `*hdr == 0` passes (UINT64_MAX != 0); then
|
||||
/// `*hdr -= 1` attempts to write to the read-only data section.
|
||||
/// hs.2 short-circuits both `ailang_rc_inc` and `ailang_rc_dec`
|
||||
/// on the sentinel before the header is mutated, making the
|
||||
/// path a defined no-op. This test is the first in the project
|
||||
/// to exercise it: pre-hs.2 the binary segfaults; post-hs.2 it
|
||||
/// reports `live=0` and exits cleanly.
|
||||
#[test]
|
||||
fn str_field_in_adt_drops_static_str_noop() {
|
||||
let (stdout, allocs, frees, live) =
|
||||
build_and_run_with_rc_stats("rc_str_field_in_adt_static.ail.json");
|
||||
assert_eq!(
|
||||
stdout.trim(),
|
||||
"hello",
|
||||
"fixture must print the matched Str payload"
|
||||
);
|
||||
assert_eq!(
|
||||
live, 0,
|
||||
"static-Str-in-ADT drop must not leak; live={live} \
|
||||
(allocs={allocs} frees={frees}). The sentinel short-circuit \
|
||||
in ailang_rc_dec for static-Str field pointers must not \
|
||||
increment g_rc_free_count, and the outer StrBox cell must \
|
||||
drop normally."
|
||||
);
|
||||
}
|
||||
```
|
||||
|
||||
- [ ] **Step 2: Run the test to verify it fails.**
|
||||
|
||||
Run: `cargo test --workspace -p ail str_field_in_adt_drops_static_str_noop`
|
||||
Expected: FAIL. The most likely failure mode is the assertion
|
||||
`output.status.success()` inside `build_and_run_with_rc_stats`
|
||||
at `crates/ail/tests/e2e.rs:2119-2123` panicking with
|
||||
`binary <path> (--alloc=rc, AILANG_RC_STATS=1) exited non-zero`,
|
||||
because the binary either SIGSEGVs writing to `.rodata` or
|
||||
gets caught by `ailang_rc_dec`'s `abort()` on a write attempt.
|
||||
A secondary possible failure mode is the rc-stats line being
|
||||
absent from stderr because the program crashed before the
|
||||
`atexit` handler ran — in that case the panic is at
|
||||
`crates/ail/tests/e2e.rs:2129-2131`
|
||||
(`missing ailang_rc_stats line in stderr`). Either failure
|
||||
shape is the expected RED state; both go GREEN once Step 3
|
||||
lands.
|
||||
|
||||
- [ ] **Step 3: Add the sentinel-header short-circuit to `ailang_rc_inc`.**
|
||||
|
||||
Modify `runtime/rc.c:132-145`. The current body is:
|
||||
|
||||
```c
|
||||
void ailang_rc_inc(void *payload) {
|
||||
if (payload == NULL) {
|
||||
return;
|
||||
}
|
||||
/* Static closure-pair env pointers (Iter 8b) live in the LLVM data
|
||||
* segment, not in heap memory we allocated. Codegen elides inc/dec
|
||||
* for known-static pointers (the `@`-prefix gate added in 18c.3),
|
||||
* so this path is not reached for them in practice. The runtime
|
||||
* itself has no header-bit flag distinguishing static from heap;
|
||||
* if codegen ever loses the elision, inc on a static pointer is
|
||||
* undefined behaviour. */
|
||||
ailang_rc_header_t *hdr = header_of(payload);
|
||||
*hdr += 1;
|
||||
}
|
||||
```
|
||||
|
||||
Replace with:
|
||||
|
||||
```c
|
||||
void ailang_rc_inc(void *payload) {
|
||||
if (payload == NULL) {
|
||||
return;
|
||||
}
|
||||
/* Static closure-pair env pointers (Iter 8b) live in the LLVM data
|
||||
* segment, not in heap memory we allocated. Codegen elides inc/dec
|
||||
* for known-static pointers (the `@`-prefix gate added in 18c.3),
|
||||
* so this path is not reached for them in practice. The runtime
|
||||
* itself has no header-bit flag distinguishing static from heap;
|
||||
* if codegen ever loses the elision, inc on a static pointer is
|
||||
* undefined behaviour. */
|
||||
ailang_rc_header_t *hdr = header_of(payload);
|
||||
/* Iter hs.2: static-Str literal slabs (emitted by the codegen as
|
||||
* packed-struct globals in iter hs.1) carry the sentinel header
|
||||
* value UINT64_MAX in the slot at `payload - 8`. Such slabs live
|
||||
* in the `.rodata` section; their refcount must never be mutated.
|
||||
* Codegen does not elide inc/dec on static-Str field pointers
|
||||
* (the `@`-prefix elision in 18c.3 covered only closure-pair
|
||||
* env pointers, not Str payload pointers materialised via
|
||||
* constexpr GEP). The sentinel-header short-circuit makes inc
|
||||
* a defined no-op for such pointers. The same convention
|
||||
* applies to `ailang_rc_dec` below. */
|
||||
if (*hdr == UINT64_MAX) {
|
||||
return;
|
||||
}
|
||||
*hdr += 1;
|
||||
}
|
||||
```
|
||||
|
||||
- [ ] **Step 4: Add the sentinel-header short-circuit to `ailang_rc_dec`.**
|
||||
|
||||
Modify `runtime/rc.c:161-177`. The current body is:
|
||||
|
||||
```c
|
||||
void ailang_rc_dec(void *payload) {
|
||||
if (payload == NULL) {
|
||||
return;
|
||||
}
|
||||
ailang_rc_header_t *hdr = header_of(payload);
|
||||
if (*hdr == 0) {
|
||||
fprintf(stderr,
|
||||
"ailang_rc_dec: refcount underflow at %p (already zero)\n",
|
||||
payload);
|
||||
abort();
|
||||
}
|
||||
*hdr -= 1;
|
||||
if (*hdr == 0) {
|
||||
free(hdr);
|
||||
g_rc_free_count++;
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
Replace with:
|
||||
|
||||
```c
|
||||
void ailang_rc_dec(void *payload) {
|
||||
if (payload == NULL) {
|
||||
return;
|
||||
}
|
||||
ailang_rc_header_t *hdr = header_of(payload);
|
||||
/* Iter hs.2: static-Str literal slabs carry the sentinel
|
||||
* UINT64_MAX in the header slot and live in `.rodata`.
|
||||
* Short-circuit before the underflow check (UINT64_MAX != 0
|
||||
* would otherwise pass the underflow guard and reach the
|
||||
* read-modify-write at `*hdr -= 1`, segfaulting on `.rodata`).
|
||||
* See the matching comment in `ailang_rc_inc` above. */
|
||||
if (*hdr == UINT64_MAX) {
|
||||
return;
|
||||
}
|
||||
if (*hdr == 0) {
|
||||
fprintf(stderr,
|
||||
"ailang_rc_dec: refcount underflow at %p (already zero)\n",
|
||||
payload);
|
||||
abort();
|
||||
}
|
||||
*hdr -= 1;
|
||||
if (*hdr == 0) {
|
||||
free(hdr);
|
||||
g_rc_free_count++;
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
- [ ] **Step 5: Confirm `UINT64_MAX` is reachable in `runtime/rc.c`.**
|
||||
|
||||
Run: `grep -n '#include <stdint.h>' runtime/rc.c`
|
||||
Expected: a single line `48:#include <stdint.h>` (or equivalent).
|
||||
`UINT64_MAX` is provided by `<stdint.h>`, which is already
|
||||
included by `runtime/rc.c:48`. No new include is needed.
|
||||
If for some reason the include is missing, add `#include <stdint.h>`
|
||||
to the include block at the top of the file.
|
||||
|
||||
- [ ] **Step 6: Run the test to verify it passes.**
|
||||
|
||||
Run: `cargo test --workspace -p ail str_field_in_adt_drops_static_str_noop`
|
||||
Expected: PASS. The fixture's binary runs cleanly, prints
|
||||
`hello`, the atexit handler reports `allocs=N frees=N live=0`
|
||||
for the heap-side StrBox cell (one alloc for the StrBox outer,
|
||||
one matching free at let-scope close), and the test's
|
||||
`assert_eq!(live, 0, ...)` succeeds.
|
||||
|
||||
---
|
||||
|
||||
## Task 3: Full regression sweep
|
||||
|
||||
Confirm the runtime change broke nothing else. The sentinel
|
||||
short-circuit adds one early-return branch in two hot-path
|
||||
functions; in principle the only behavioural effect is on
|
||||
pointers whose header equals `UINT64_MAX`, which today is only
|
||||
the static-Str case. Belt-and-braces verify against every other
|
||||
RC-discipline test and against the cross-language reference
|
||||
corpus.
|
||||
|
||||
**Files:**
|
||||
- (none — read-only verification)
|
||||
|
||||
- [ ] **Step 1: Run the full cargo test workspace.**
|
||||
|
||||
Run: `cargo test --workspace`
|
||||
Expected: PASS, all tests green. Specifically, the existing
|
||||
`alloc_rc_*` tests (12 fixtures exercising heap allocations
|
||||
of various ADTs under `--alloc=rc`) continue to report
|
||||
matching allocs/frees because none of them carry a `Str`
|
||||
field and therefore none of them ever calls
|
||||
`ailang_rc_dec(static_str_ptr)`.
|
||||
|
||||
- [ ] **Step 2: Run `bench/compile_check.py`.**
|
||||
|
||||
Run: `python3 bench/compile_check.py`
|
||||
Expected: every `examples/` program — including the new
|
||||
`rc_str_field_in_adt_static.ail.json` — compiles without
|
||||
errors or warnings; the script exits 0.
|
||||
|
||||
- [ ] **Step 3: Run `bench/cross_lang.py`.**
|
||||
|
||||
Run: `python3 bench/cross_lang.py`
|
||||
Expected: every fixture in `bench/reference/` produces
|
||||
byte-identical stdout from its AILang and C implementations;
|
||||
the script exits 0. None of these fixtures carries an
|
||||
ADT-with-`Str`-field today, so the sentinel short-circuit
|
||||
is not exercised; the test confirms no orthogonal regression
|
||||
crept in.
|
||||
|
||||
---
|
||||
|
||||
## Notes for the implementer
|
||||
|
||||
- The hs.1 packed-struct globals emit `i64 -1` for the sentinel
|
||||
slot. When read as `uint64_t` this is bit-for-bit equivalent to
|
||||
`UINT64_MAX` (`0xFFFFFFFFFFFFFFFF` in both signed twos-complement
|
||||
-1 and unsigned UINT64_MAX representations). The codegen-side
|
||||
emits `-1`; the runtime-side checks against `UINT64_MAX`. Both
|
||||
refer to the same 64-bit pattern.
|
||||
|
||||
- Beyond the sentinel-Str case, the only way a real refcount could
|
||||
reach `UINT64_MAX` is via `2^64` independent references — which
|
||||
would consume more memory than exists on any machine. The
|
||||
collision-with-real-refcount case is structurally impossible,
|
||||
not just unlikely.
|
||||
|
||||
- The block-comment at `runtime/rc.c:136-142` describes a different
|
||||
static-pointer case (closure-pair env pointers in the `.data`
|
||||
segment, which have no header at all and rely entirely on
|
||||
codegen-side elision). It is NOT outdated by hs.2 — the
|
||||
closure-pair case still relies on codegen-side elision, and the
|
||||
sentinel guard is orthogonal additional protection for a
|
||||
different kind of static pointer (Str literals). Do not edit
|
||||
that comment.
|
||||
|
||||
- No `git commit` step. The Boss commits the working-tree diff at
|
||||
iter end after audit-level inspection.
|
||||
Reference in New Issue
Block a user