Consuming a heap sub-binder of a borrowed scrutinee is accepted -> double-free #58

New Issue

2026-06-02T00:20:05+02:00

Brummel commented

2026-06-02 00:20:05 +02:00

Symptom

The strict linearity check does NOT reject consuming a heap pattern sub-binder extracted from a borrow-mode match scrutinee. The sub-binder aliases caller-owned heap, so consuming it (passing it to an own param) double-frees.

Surfaced by fieldtest spec docs/specs/0065-fieldtest-eliminate-implicit-mode.md (cut55_2c) post-#55 cutover. NOT introduced by #55 — the cutover's universal activation of the strict check exposed a pre-existing hole the corpus never exercised.

Repro

(module df_repro
  (data List (ctor Nil) (ctor Cons (con Int) (con List)))
  (fn sum_own
    (type (fn-type (params (own (con List))) (ret (own (con Int)))))
    (params xs)
    (body (match xs (case (pat-ctor Nil) 0) (case (pat-ctor Cons h t) (app + h (app sum_own t))))))
  (fn leak
    (type (fn-type (params (borrow (con List))) (ret (own (con Int)))))
    (params xs)
    (body (match xs (case (pat-ctor Nil) 0) (case (pat-ctor Cons h t) (app sum_own t)))))
  (fn main
    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
    (params)
    (body
      (let lst (term-ctor List Cons 1 (term-ctor List Cons 2 (term-ctor List Nil)))
        (seq (app print (app leak lst))
             (seq (app print (app leak lst))
                  (do io/print_str "done\n")))))))

ail check -> ok, exit 0 (WRONG: should fire consume-while-borrowed on t).
ail build + run -> exit 139 (SIGSEGV, double-free of the freed tail on the second leak).
AILANG_RC_STATS=1 masks the crash (exit 0) — same divergence as the #55 drop legs.

Root hypothesis

A borrow-mode match scrutinee's pattern sub-binders that are heap-typed must INHERIT borrowed status, so consuming them fires consume-while-borrowed. The linearity pass (crates/ailang-check/src/linearity.rs) currently catches the whole-param consume (cut55_2d, correctly rejected) but not the moved-out heap sub-binder. Sibling to the #57 (spec 0064) class-2 let-alias-of-borrow hardening; this is the pattern-sub-binder analog. RED-first.

Note

Value-typed sub-binders (an Int h) are fine to consume (copied, no heap alias) — only HEAP sub-binders of a borrowed scrutinee are the hole.

## Symptom The strict linearity check does NOT reject consuming a heap pattern sub-binder extracted from a `borrow`-mode match scrutinee. The sub-binder aliases caller-owned heap, so consuming it (passing it to an `own` param) double-frees. Surfaced by fieldtest spec `docs/specs/0065-fieldtest-eliminate-implicit-mode.md` (cut55_2c) post-#55 cutover. NOT introduced by #55 — the cutover's universal activation of the strict check exposed a pre-existing hole the corpus never exercised. ## Repro ``` (module df_repro (data List (ctor Nil) (ctor Cons (con Int) (con List))) (fn sum_own (type (fn-type (params (own (con List))) (ret (own (con Int))))) (params xs) (body (match xs (case (pat-ctor Nil) 0) (case (pat-ctor Cons h t) (app + h (app sum_own t)))))) (fn leak (type (fn-type (params (borrow (con List))) (ret (own (con Int))))) (params xs) (body (match xs (case (pat-ctor Nil) 0) (case (pat-ctor Cons h t) (app sum_own t))))) (fn main (type (fn-type (params) (ret (own (con Unit))) (effects IO))) (params) (body (let lst (term-ctor List Cons 1 (term-ctor List Cons 2 (term-ctor List Nil))) (seq (app print (app leak lst)) (seq (app print (app leak lst)) (do io/print_str "done\n"))))))) ``` - `ail check` -> ok, exit 0 (WRONG: should fire `consume-while-borrowed` on `t`). - `ail build` + run -> exit 139 (SIGSEGV, double-free of the freed tail on the second `leak`). - `AILANG_RC_STATS=1` masks the crash (exit 0) — same divergence as the #55 drop legs. ## Root hypothesis A `borrow`-mode match scrutinee's pattern sub-binders that are heap-typed must INHERIT borrowed status, so consuming them fires `consume-while-borrowed`. The linearity pass (`crates/ailang-check/src/linearity.rs`) currently catches the whole-param consume (cut55_2d, correctly rejected) but not the moved-out heap sub-binder. Sibling to the #57 (spec 0064) class-2 let-alias-of-borrow hardening; this is the pattern-sub-binder analog. RED-first. ## Note Value-typed sub-binders (an Int `h`) are fine to consume (copied, no heap alias) — only HEAP sub-binders of a borrowed scrutinee are the hole.

Brummel added the bug BLOCKER labels 2026-06-02 00:20:05 +02:00

Brummel referenced this issue from a commit

2026-06-02 01:11:02 +02:00

fix(check): inherit borrow on heap sub-binders of a borrowed scrutinee (#58)

Brummel closed this issue

2026-06-02 01:11:02 +02:00

Brummel referenced this issue from a commit

2026-06-02 01:11:02 +02:00

test(cutover): live accept/reject corpus for the #55 ownership surface

Sign in to join this conversation.