w6c+wwstage: reject untyped empty-[] alloc — require context, loud cannot-infer (#3 B', subsumes #5)

An empty `[]` carries no element type; ww gets it only from a let
annotation (the #45 retype). Both stages used to silently default the
element to u8, and in value-form positions (return / call-arg) the
lowering miscompiled — malloc(8) ignoring n, a 16B *u8|nomem where a 24B
slice was expected (#5). Now every empty alloc that isn't a
let-annotated binding fails to infer with a loud error, aligning ww DOWN
to harec (ref/harec/src/check.c:1801-1802).

Mechanism: clet / checkletassign flags the single alloc call node that a
`let x: []T =` rescues (save/restore around the init walk); the alloc
branch errors on any empty alloc that isn't that node. The #45 wide-T
retype path is kept. wwstage needs an extra not-yet-stamped guard because
resolvewalk re-types value nodes context-free after checkletassign.

Tests: negative cstage-driver 729 (table-driven: bare-let, return,
call-arg, assignment) + positive @test in attest_pass.ww exercising the
u8 and the wide-i32 (#45) paths at runtime. Both stages reject
symmetrically; byte-id verified on []u8 and []i32.
This commit is contained in:
2026-06-02 18:54:35 +09:00
parent bec1e7d6b0
commit 90479fed68
8 changed files with 440 additions and 0 deletions

View File

@@ -2,6 +2,8 @@
package data;
import rt; // #3/B': check_empty_alloc_annotated calls alloc → rt_malloc.
type point = struct { x: i32, y: i32 };
@test fn check_add() void = {
@@ -104,3 +106,24 @@ type point = struct { x: i32, y: i32 };
let _: i32 = 1 / 0;
};
};
// #3/B': the let-annotation context path keeps `alloc([], n)` inferring
// its element type for ANY T (u8 default + non-u8 #45 retype). The bare /
// return / arg empty allocs that lost the silent u8 default are covered by
// the negative test (test/wcc/729). Here we pin that annotated allocs of
// both an 8-bit and a wide element still compile and index correctly.
// alloc([], n) is Hare's len=0 / cap=n empty slice, so we write into the
// cap-backed memory and read it back (ref/hare expects len 0, not n).
@test fn check_empty_alloc_annotated() void = {
let b: []u8 = alloc([], 8u64)!;
b[0] = 7u8;
b[3] = 9u8;
if (b[0] != 7 || b[3] != 9) {
let _: i32 = 1 / 0;
};
let w: []i32 = alloc([], 4u64)!;
w[2] = 5i32;
if (w[2] != 5) {
let _: i32 = 1 / 0;
};
};