fix(compiler): lang-41 side defects — ?T-typed nil try, WO-E305 on moves out of a field

- emit.ml: a `try … catch (e) nil` is `?T` (ty_of_expr) and the nil arm takes that destination, so a `?Int` nil is WO_NIL_SCALAR and an Int body's legitimate 0 no longer reads as nil (it used to fall back to the zero word via the body type / enclosing return type)
- owner.ml: `transfer` on a projection (`d.tags`, `x[i]`) of an owned value reports WO-E305 instead of returning false silently — the silent path compiled `Out { tags: d.tags }` to an alias that both records dropped (the "json.decode as T corruption": not json's, a double free language 44's poison now aborts on); heap scalars exempt (store sites copy)
- error catalog: WO-E305 row; owner.ml module doc updated
- corpus: run/try-nil-int-zero, compile-fail/no-partial-move, run/decode-record-crosses-return (Text copied, record moved whole — the archived `.. ""` workaround is unnecessary)
- verified: oop-e2e 126/0, tests/regress/lang-41 compile, --emit sweep over the non-porch examples, web-app gate 56/0 (porch in project mode) — no legitimate program trips WO-E305
- story 41: both side defects marked fixed; board prose updated

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
(cherry picked from commit 2d54710e693fafee4b8d6561cc9cba7b95415d89)
This commit is contained in:
shoney.arickathil 2026-09-09 17:22:04 +02:00
parent dd426d0581
commit 82efb498d4
11 changed files with 151 additions and 10 deletions

View file

@ -1177,6 +1177,12 @@ let query_elem_scalar (p : pctx) (q : Ast.query) ~(src : string) : string =
| None -> "Int") | None -> "Int")
| _ -> "Int" | _ -> "Int"
(* `try … catch (e) nil`: the catch arm's value is the literal nil *)
let try_handler_is_nil (handler : Ast.stmt list) : bool =
match List.rev handler with
| { Ast.s_kind = Ast.ExprStmt { Ast.kind = Ast.NilLit; _ }; _ } :: _ -> true
| _ -> false
let rec ty_of_expr (p : pctx) (f : fstate) (e : Ast.expr) : Ast.field_ty option = let rec ty_of_expr (p : pctx) (f : fstate) (e : Ast.expr) : Ast.field_ty option =
match e.kind with match e.kind with
| IntLit _ -> Some (Scalar "Int") | IntLit _ -> Some (Scalar "Int")
@ -1192,8 +1198,14 @@ let rec ty_of_expr (p : pctx) (f : fstate) (e : Ast.expr) : Ast.field_ty option
| NilLit -> None | NilLit -> None
| As (_, ty) -> Some (Nullable ty) | As (_, ty) -> Some (Nullable ty)
(* haxe-parity Task 5: a `try` yields its try arm's type — types.ml has (* haxe-parity Task 5: a `try` yields its try arm's type — types.ml has
already required the catch arm to agree. *) already required the catch arm to agree. A `catch (e) nil` arm makes it
| Try t -> ty_of_expr p f t.body `?T`, so a `?scalar`'s nil is the sentinel and an Int body's 0 stays 0
(lang-41 side defect). *)
| Try t -> (
match ty_of_expr p f t.body with
| Some (Nullable _) as n -> n
| Some bt when try_handler_is_nil t.handler -> Some (Nullable bt)
| other -> other)
| Ident n -> ( | Ident n -> (
match List.assoc_opt n f.f_env with match List.assoc_opt n f.f_env with
| Some (_, t) -> Some t | Some (_, t) -> Some t
@ -2665,7 +2677,13 @@ and emit_try (p : pctx) (f : fstate) (v : views) ~(dst : int) ?expected (e : Ast
f.f_cur_line <- last.Ast.s_pos.line; f.f_cur_line <- last.Ast.s_pos.line;
(match expected with (match expected with
| Some t -> emit_expr p f v ~dst ~expected:t ve | Some t -> emit_expr p f v ~dst ~expected:t ve
| None -> emit_expr p f v ~dst ve); | None -> (
(* a `nil` arm takes the try's own type as its destination: `?Int`
selects the scalar sentinel, so an `Int` body's legitimate 0 is
never read as nil (lang-41 side defect; see ty_of_expr's Try) *)
match (if is_nil_lit ve then ty_of_expr p f e else None) with
| Some t -> emit_expr p f v ~dst ~expected:t ve
| None -> emit_expr p f v ~dst ve));
(* iteration 24 fix (the catch half of the arm-copy rule): a bare (* iteration 24 fix (the catch half of the arm-copy rule): a bare
`e.msg` arm aliases the Error record's field, and the record is `e.msg` arm aliases the Error record's field, and the record is
dropped at CATCH scope end below — ASan-confirmed use-after-free dropped at CATCH scope end below — ASan-confirmed use-after-free

View file

@ -69,7 +69,8 @@
a place where this pass is wrong-by-accident: a place where this pass is wrong-by-accident:
- No partial moves. A move site must name a whole local (`x`), never - No partial moves. A move site must name a whole local (`x`), never
a projection (`x.f`, `x[0]`); see the `let` case above. a projection (`x.f`, `x[0]`); see the `let` case above. A projection
at a transfer site is WO-E305, not a silent alias (transfer).
- Alias provability is syntactic *after canonicalization*: a place - Alias provability is syntactic *after canonicalization*: a place
written through a borrow binding is first rewritten to the storage written through a borrow binding is first rewritten to the storage
that borrow names (see canon), then two places overlap only if they that borrow names (see canon), then two places overlap only if they
@ -131,6 +132,15 @@ let conflicting_borrow_code = Diag.ownership_prefix ^ "03"
escape. Related: where the borrow was created. *) escape. Related: where the borrow was created. *)
let borrow_escape_code = Diag.ownership_prefix ^ "04" let borrow_escape_code = Diag.ownership_prefix ^ "04"
(* WO-E305 — an owned value is moved out of a field or element (`x.f`,
`x[i]`) while its record/container still owns it: stored into a record,
pushed into a container, passed to a `take` parameter, or returned.
Milestone 1 has no partial moves, and silently allowing the store put one
owned value under two owners — a double free at the second drop (the
lang-41 side defect). Heap scalars are exempt: every store site copies
them (stores_by_copy). Primary site: the move. Related: the owner. *)
let partial_move_code = Diag.ownership_prefix ^ "05"
(* ============================================================ (* ============================================================
Ownership classes and places Ownership classes and places
============================================================ *) ============================================================ *)
@ -1112,7 +1122,22 @@ let transfer (ctx : ctx) (p : place) ~(what : string) : bool =
| Moved _ -> false (* already reported at the read *) | Moved _ -> false (* already reported at the read *)
| Borrowed _ -> false (* unreachable: is_borrow_root covered it *) | Borrowed _ -> false (* unreachable: is_borrow_root covered it *)
| Live -> | Live ->
if p.projs <> [] then false (* no partial moves in milestone 1 *) if p.projs <> [] then begin
(* no partial moves in milestone 1 — and no silent alias either:
the record/container still owns this place, so the transfer
would give one owned value two owners (WO-E305) *)
if not (stores_by_copy ctx p) then
report ctx ~code:partial_move_code ~pos:p.ppos
~message:
(Printf.sprintf
"`%s` %s — it is part of `%s`, and an owned value cannot be moved out of a \
field or element (no partial moves): move `%s` whole, or build a fresh \
container from its elements"
(place_text p) what l.l_name l.l_name)
~rel:l.l_pos
~label:(Printf.sprintf "`%s` owns it" l.l_name);
false
end
else begin else begin
check_against_borrows ctx ~node:p.pnode ~pos:p.ppos p AMove; check_against_borrows ctx ~node:p.pnode ~pos:p.ppos p AMove;
l.l_state <- Moved p.ppos; l.l_state <- Moved p.ppos;

View file

@ -139,6 +139,7 @@ renders indented beneath it.
| WO-E302 | a place is moved while a live borrow of it, or of an overlapping place, still exists. | `cannot move \`bag.items\` while \`r\` is borrowed` | | WO-E302 | a place is moved while a live borrow of it, or of an overlapping place, still exists. | `cannot move \`bag.items\` while \`r\` is borrowed` |
| WO-E303 | two exclusive (`mut`) accesses of the same place, or two accesses the analysis can *prove* overlap, conflict in one region (e.g. two `mut` element accesses through the same provable index, or the same place borrowed and then mutated). Cases the analysis can't prove either way become a residual site for the VM to guard at runtime, not this diagnostic. | `cannot borrow \`bag.items[i]\` as \`mut\` twice in the same call` | | WO-E303 | two exclusive (`mut`) accesses of the same place, or two accesses the analysis can *prove* overlap, conflict in one region (e.g. two `mut` element accesses through the same provable index, or the same place borrowed and then mutated). Cases the analysis can't prove either way become a residual site for the VM to guard at runtime, not this diagnostic. | `cannot borrow \`bag.items[i]\` as \`mut\` twice in the same call` |
| WO-E304 | a borrow is returned or stored somewhere that outlives the scope it borrowed from. `@gc`-typed values are exempt (freely aliased by design). | `borrow of \`x\` returned — borrows cannot outlive their scope` | | WO-E304 | a borrow is returned or stored somewhere that outlives the scope it borrowed from. `@gc`-typed values are exempt (freely aliased by design). | `borrow of \`x\` returned — borrows cannot outlive their scope` |
| WO-E305 | an owned value is moved out of a field or element (`x.f`, `x[i]`) — stored into a record, pushed into a container, passed to a `take` parameter, or returned — while its record/container still owns it (no partial moves; before this diagnostic the store silently aliased, a double free at the second drop). Heap scalars (`Text`, `Bytes`) are exempt: those sites copy. Move the whole owner, or build a fresh container from its elements. | `\`d.tags\` cannot be stored in \`Out.tags\` — it is part of \`d\`, and an owned value cannot be moved out of a field or element (no partial moves): move \`d\` whole, or build a fresh container from its elements` |
## WO-E4xx — emitter (plan 3 Task 1, `compiler/src/emit.ml`) ## WO-E4xx — emitter (plan 3 Task 1, `compiler/src/emit.ml`)

View file

@ -659,7 +659,12 @@ localises it: every failure belonged to the path with 5x the allocation inside
sequential insert+delete volume on one key (N=4/5 crashed, N=1-3 clean over 12+ sequential insert+delete volume on one key (N=4/5 crashed, N=1-3 clean over 12+
trials). Two smaller runtime defects came with it — `try/catch` cannot tell a trials). Two smaller runtime defects came with it — `try/catch` cannot tell a
literal `Int 0` reply from a trap, and a `json.decode` value is corrupted when literal `Int 0` reply from a trap, and a `json.decode` value is corrupted when
embedded in a struct crossing a function-return boundary. embedded in a struct crossing a function-return boundary. **Both fixed
2026-09-09**: a nil-armed `try` is `?T` (its nil is the scalar sentinel, so 0
stays 0), and the "corruption" was a silent alias — an owned container field
stored into another record with both records dropping it — now **WO-E305** at
compile time (corpus: `try-nil-int-zero`, `no-partial-move`,
`decode-record-crosses-return`).
**Corrections to our own record:** the earlier claim that `Pool` being traced **Corrections to our own record:** the earlier claim that `Pool` being traced
forces a one-slot re-wrap was WRONG — WO-E222 fires on the class, not on forces a one-slot re-wrap was WRONG — WO-E222 fires on the class, not on

View file

@ -378,7 +378,21 @@ fixed.
dropping, run 5× under `WO_SHARDS=4` + ASan by `scripts/db-actor-accept.sh` dropping, run 5× under `WO_SHARDS=4` + ASan by `scripts/db-actor-accept.sh`
(`just db-actor`). It lives in `tests/regress` rather than the corpus because (`just db-actor`). It lives in `tests/regress` rather than the corpus because
the corpus runner pins `WO_SHARDS=1`. the corpus runner pins `WO_SHARDS=1`.
- **The two smaller runtime defects found alongside** (above): the - ~~**The two smaller runtime defects found alongside** (above)~~ ✅ **both
`try EXPR catch (e) nil` Int-0-vs-trap ambiguity and the `json.decode ... as T` fixed 2026-09-09**, each with its corpus fixture:
cross-return-boundary corruption. Both worked around in the archived code; - `try EXPR catch (e) nil` over an `Int` body spelled its nil as the zero
each deserves its own minimal fixture and fix, neither blocks this. word (the try took the body's type, `Int`, so `nil_const_for` chose 0 and
`x == nil` compared against 0). The emitter now types a nil-armed try as
`?T` and the nil arm takes that destination, so a `?Int` nil is the
`WO_NIL_SCALAR` sentinel and a legitimate 0 stays 0 —
`tests/corpus/run/try-nil-int-zero`.
- the "`json.decode … as T` corruption" was not json's: storing a record's
owned **container** field into another record (`Out { tags: d.tags }`)
compiled to a silent alias — `transfer` returned false for any projection
("no partial moves") without reporting, so `d` and `Out` both dropped the
multi (a double free, which language 44's poisoned header now aborts on).
A projection at a transfer site is **WO-E305** (heap scalars exempt: those
sites copy) — `tests/corpus/compile-fail/no-partial-move`; the sanctioned
shapes (Text copied, record moved whole) —
`tests/corpus/run/decode-record-crosses-return`. The archived `.. ""`
workaround is unnecessary.

View file

@ -0,0 +1 @@
WO-E305

View file

@ -0,0 +1,21 @@
-- lang-41 side defect 2: storing `d.tags` into another record used to
-- compile to a silent alias — `d` still owned the multi, so both records
-- dropped it (a double free the poisoned header now aborts on). A
-- projection at a transfer site is WO-E305; the Text field is exempt
-- because SETF copies it.
class D {
name: Text
tags: multi Text
}
class Out {
label: Text
tags: multi Text
}
fn build() -> Out {
let d = D { name: "alpha", tags: ["t1", "t2"] }
return Out { label: d.name, tags: d.tags }
}
fn main() {
let o = build()
print(o.label)
}

View file

@ -0,0 +1,3 @@
alpha
7
beta

View file

@ -0,0 +1,32 @@
-- lang-41 side defect 2, the sanctioned shapes: a Text read off a decoded
-- record into another record's ctor is COPIED (SETF's rule), and the decoded
-- record itself moves whole across a return. Neither needs the archived
-- porch code's `.. ""` workaround; a container field must move with its
-- record (see compile-fail/no-partial-move).
use json
class D {
name: Text
n: Int
}
class Out {
label: Text
n: Int
}
fn build(t: Text) -> Out {
let d = json.decode(t) as D
if d != nil { return Out { label: d.name, n: d.n } }
return Out { label: "none", n: 0 }
}
fn build2(t: Text) -> ?D {
let d = json.decode(t) as D
return d
}
fn main() {
let o = build("{\"name\":\"alpha\",\"n\":7}")
let junk = "z" .. "y" .. "x"
print(o.label)
print_int(o.n)
let d2 = build2("{\"name\":\"beta\",\"n\":8}")
let junk2 = "a" .. "s" .. "d"
if d2 != nil { print(d2.name) }
}

View file

@ -0,0 +1,3 @@
0
trap-is-nil
zero-kept-in-int-fn

View file

@ -0,0 +1,18 @@
-- lang-41 side defect 1: `try EXPR catch (e) nil` over an Int body used to
-- spell its nil as the zero word, so a legitimate 0 reply read as a trap.
-- The try is `?Int`: nil is the scalar sentinel, 0 stays 0, in a void fn
-- and in one whose own return type is Int (the archived porch shape).
fn zero() -> Int { return 0 }
fn boom() -> Int { let d = 0; return 1 / d }
fn probe() -> Int {
let z = try zero() catch (e) nil
if z == nil { print("ZERO-READ-AS-NIL-IN-INT-FN") } else { print("zero-kept-in-int-fn") }
return 1
}
fn main() {
let z = try zero() catch (e) nil
if z == nil { print("ZERO-READ-AS-NIL") } else { print_int(z) }
let t = try boom() catch (e) nil
if t == nil { print("trap-is-nil") } else { print("TRAP-READ-AS-VALUE") }
probe()
}