Skip to content

Commit ec19653

Browse files
feat(parser): CORE-01 pt2 — &mut e exclusive-borrow surface (Refs #177) (#269)
The pt2 residual was parser-gated: the shared-XOR-exclusive rules from pt1 (#240 UseWhileExclusivelyBorrowed / ConflictingBorrow) could never fire from real source because `&mut e` did not parse — only shared `&e` (OpRef) existed. This adds the exclusive-borrow expression surface. - ast.ml: new `unary_op` variant `OpMutRef` (`&mut e`). Documented: only the borrow checker distinguishes it from `OpRef`; every other backend treats `&mut e` exactly like `&e` (a reference is the same runtime pointer — exclusivity is a static property). - parser.mly: `expr_unary | AMP MUT e -> ExprUnary (OpMutRef, e)`, ordered before `AMP e`. `AMP MUT` is unambiguous (an expression cannot begin with the MUT keyword) — **zero Menhir conflict delta**: 21 S/R states + 1 R/R + 68/7 arbitrarily-resolved baseline held (ADR-012). - borrow.ml: `OpMutRef` => *Exclusive* borrow (vs `OpRef` Shared); `ref_target`/`is_copy` also match it. This is the soundness payload. - typecheck/codegen: `OpMutRef` folded into the `OpRef` arm (typed `TRef`, same heap-pointer codegen); `gen_unop` made exhaustive. Verified: `&mut x` parses; two `&mut x` => ConflictingBorrow; read `x` while `&mut x` live => UseWhileExclusivelyBorrowed; `return &mut local` => BorrowOutlivesOwner (composes with pt2 return-escape); shared `&x` unchanged; `&mut x` emits wasm (177 B). Full gate 278 -> 281 (+3 hermetic "E2E Borrow Graph" tests + 3 fixtures); all stdlib AOT green — zero over-rejection. Scope: `&`-in-`#{` literals + bare block-statements already parse on main; the `-> &T`/`&T` *type* sigil is deliberately NOT added (`ref T`/ `mut T` keyword types already express reference types — a `&T` sigil is duplicate surface, ADR territory, not a soundness gap). The pt2 residual is now the NLL/`outer=&x` *analysis* (expressible, no longer parser-gated), not surface. Ledger + borrow.ml comment truthed. Refs #177 (not Closes — NLL analysis remains). Co-authored-by: hyperpolymath <hyperpolymath@users.noreply.github.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent d19afa1 commit ec19653

10 files changed

Lines changed: 125 additions & 23 deletions

docs/TECH-DEBT.adoc

Lines changed: 16 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -93,13 +93,22 @@ at a *callee-owned* binding (local or by-value/`own` param) is now
9393
`BorrowOutlivesOwner` (pt1 only saw block tails — `return r` slipped
9494
through); `ref`/`mut` params are caller-owned and not flagged (no
9595
over-rejection; full stdlib AOT green). 3 hermetic tests in "E2E Borrow
96-
Graph". *Part 2 residual — parser-gated (honest finding):* NLL/region
97-
inference (Polonius); flow-sensitive escape via `outer = &x`; tighter
98-
quantity integration. These are *not reachable unsoundnesses today* — the
99-
surface to express them does not parse (`&mut e`, `-> &T`, `&`-in-literal,
100-
bare block-statements), so the next move is the parser surface, then the
101-
analysis. |S1 |pt1 #240 + pt2 return-escape DONE (Refs #177); pt2 residual
102-
parser-gated — issue #177
96+
Graph". *Part 2 — `&mut e` parser surface LANDED* (Refs #177, gate
97+
278→281, **zero Menhir conflict delta** — 21 S/R + 1 R/R baseline held;
98+
`AMP MUT e` is unambiguous): the exclusive-borrow expression is now
99+
expressible, so the pt1 shared-XOR-exclusive rules
100+
(`ConflictingBorrow`/`UseWhileExclusivelyBorrowed`) are *reachable from
101+
source* for the first time (3 hermetic "E2E Borrow Graph" tests; `&mut e`
102+
typed/codegen'd like `&e` — exclusivity is a static borrow property).
103+
`&`-in-`#{` literals and bare block-statements already parse on `main`;
104+
`-> &T`/`&T` *type* sigil deliberately **not** added — `ref T`/`mut T`
105+
keyword types already express reference types; a `&T` sigil is duplicate
106+
surface (ADR territory, not a soundness gap). *Part 2 residual — now the
107+
analysis, not surface:* NLL/region inference (Polonius) + flow-sensitive
108+
escape via `outer = &x` are now *expressible* (surface unblocked); the
109+
remaining work is the dataflow analysis itself. |S1 |pt1 #240 + pt2
110+
return-escape + `&mut` surface DONE (Refs #177); residual = NLL analysis
111+
— issue #177
103112
|CORE-02 |Effect-handler dispatch on WasmGC (currently `UnsupportedFeature`;
104113
EH proposal or CPS). The #225 CPS line closes the async slice. |S2 |partial
105114
(#225 line CLOSED PR1..PR3d+PR4; #234 generalises the recogniser —

lib/ast.ml

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -198,7 +198,12 @@ and binary_op =
198198
| OpBitAnd | OpBitOr | OpBitXor | OpShl | OpShr
199199

200200
and unary_op =
201-
| OpNeg | OpNot | OpBitNot | OpRef | OpDeref
201+
| OpNeg | OpNot | OpBitNot | OpRef | OpMutRef | OpDeref
202+
(** [OpMutRef] is `&mut e` — an *exclusive* borrow expression. `&e`
203+
is [OpRef] (shared). Only the borrow checker distinguishes them
204+
(shared-XOR-exclusive); every other backend treats `&mut e`
205+
exactly like `&e` (a reference is the same runtime pointer —
206+
exclusivity is a static property). CORE-01 pt2 / #177. *)
202207

203208
and assign_op =
204209
| AssignEq | AssignAdd | AssignSub | AssignMul | AssignDiv

lib/borrow.ml

Lines changed: 19 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -198,7 +198,7 @@ let is_copy_expr (expr : expr) : bool =
198198
| ExprLit (LitBool _) -> true
199199
| ExprLit (LitChar _) -> true
200200
| ExprLit (LitUnit _) -> true
201-
| ExprUnary (OpRef, _) -> true (* Reference creation produces a Copy pointer *)
201+
| ExprUnary ((OpRef | OpMutRef), _) -> true (* Reference creation produces a Copy pointer *)
202202
| _ -> false
203203

204204
(** Walk to the root variable of a place, if any. *)
@@ -469,7 +469,7 @@ let lookup_symbol_by_name (symbols : Symbol.t) (name : string) : Symbol.symbol o
469469
let rec ref_target (symbols : Symbol.t) (expr : expr) : place option =
470470
match expr with
471471
| ExprSpan (e, _) -> ref_target symbols e
472-
| ExprUnary (OpRef, e) -> expr_to_place symbols e
472+
| ExprUnary ((OpRef | OpMutRef), e) -> expr_to_place symbols e
473473
| _ -> None
474474

475475
(** Convert an expression to a place (if it's an l-value) *)
@@ -903,12 +903,16 @@ let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr :
903903

904904
| ExprUnary (op, e) ->
905905
begin match op with
906-
| OpRef ->
907-
(* Taking a reference: &expr - creates a shared borrow *)
906+
| OpRef | OpMutRef ->
907+
(* `&expr` is a shared borrow; `&mut expr` an *exclusive* one.
908+
This is the surface that finally makes an exclusive borrow
909+
expressible — shared-XOR-exclusive then enforces it at use
910+
sites (CORE-01 pt1 `UseWhileExclusivelyBorrowed`). *)
911+
let kind = (match op with OpMutRef -> Exclusive | _ -> Shared) in
908912
begin match expr_to_place symbols e with
909913
| Some place ->
910914
let span = expr_span e in
911-
let* _borrow = record_borrow state place Shared span in
915+
let* _borrow = record_borrow state place kind span in
912916
Ok ()
913917
| None ->
914918
(* Can't borrow non-place expressions, but check the expression *)
@@ -1179,13 +1183,17 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
11791183
flagged (probed: `fn ok(x: ref Int) -> ref Int { return x; }` passes).
11801184
Sound + non-over-rejecting (full stdlib AOT + borrow suite green).
11811185
1182-
Still deferred to a later CORE-01 part (docs/TECH-DEBT.adoc) — and note
1183-
these are *parser-gated*: the surface to express them does not parse
1184-
today (`&mut e`, `-> &T`, `&`-in-literal, bare block-statements), so
1185-
they are not reachable unsoundnesses until the surface lands:
1186+
CORE-01 pt2 parser surface (2026-05-19): `&mut e` now parses
1187+
(ExprUnary OpMutRef; `AMP MUT e`, zero Menhir conflict delta) and is an
1188+
*Exclusive* borrow here — so shared-XOR-exclusive + return-escape are
1189+
reachable from real source for the first time. `&`-in-`#{` literals and
1190+
bare block-statements already parsed; the `-> &T`/`&T` *type* sigil was
1191+
deliberately not added (`ref T`/`mut T` keyword types already exist).
1192+
1193+
Still deferred — now the *analysis*, no longer parser-gated:
11861194
- Non-lexical lifetimes with region inference (Polonius-style).
11871195
- Flow-sensitive escape via assignment to an outer mutable
1188-
(`outer = &x`) — blocked on assignment-of-borrow + inner-block-stmt
1189-
surface, not just the analysis.
1196+
(`outer = &x`) — now *expressible* (`&mut`, assignment, blocks all
1197+
parse); the remaining work is the dataflow analysis itself.
11901198
- Tighter integration with the quantity checker for captured linears.
11911199
*)

lib/codegen.ml

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -419,7 +419,7 @@ let gen_unop (op : unary_op) : instr result =
419419
| OpNeg -> Ok I32Sub (* 0 - x *)
420420
| OpNot -> Ok I32Eqz (* x == 0 *)
421421
| OpBitNot -> Ok I32Xor (* -1 ^ x *)
422-
| OpRef -> Error (UnsupportedFeature "OpRef handled in ExprUnary")
422+
| OpRef | OpMutRef -> Error (UnsupportedFeature "OpRef/OpMutRef handled in ExprUnary")
423423
| OpDeref -> Error (UnsupportedFeature "OpDeref handled in ExprUnary")
424424

425425
(** ADR-013 #225 PR3c — recursive CPS hook. The async-boundary transform
@@ -528,8 +528,9 @@ let rec gen_expr (ctx : context) (expr : expr) : (context * instr list) result =
528528

529529
| ExprUnary (op, operand) ->
530530
begin match op with
531-
| OpRef ->
532-
(* Take reference: &expr *)
531+
| OpRef | OpMutRef ->
532+
(* Take reference: &expr / &mut expr — same pointer representation;
533+
exclusivity is a static borrow property (CORE-01 pt2 / #177). *)
533534
(* Allocate heap memory, store the value, return pointer *)
534535
let* (ctx', operand_code) = gen_expr ctx operand in
535536
let (ctx_with_heap, alloc_code) = gen_heap_alloc ctx' 4 in

lib/parser.mly

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -768,6 +768,7 @@ expr_unary:
768768
| MINUS e = expr_unary { ExprUnary (OpNeg, e) }
769769
| BANG e = expr_unary { ExprUnary (OpNot, e) }
770770
| TILDE e = expr_unary { ExprUnary (OpBitNot, e) }
771+
| AMP MUT e = expr_unary { ExprUnary (OpMutRef, e) }
771772
| AMP e = expr_unary { ExprUnary (OpRef, e) }
772773
| STAR e = expr_unary { ExprUnary (OpDeref, e) }
773774
| e = expr_postfix { e }

lib/typecheck.ml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -513,7 +513,9 @@ let type_of_unop (op : unary_op) : ty * ty =
513513
| OpNeg -> (ty_int, ty_int)
514514
| OpNot -> (ty_bool, ty_bool)
515515
| OpBitNot -> (ty_int, ty_int)
516-
| OpRef ->
516+
| OpRef | OpMutRef ->
517+
(* `&mut e` types exactly like `&e` — a reference. Exclusivity is a
518+
static borrow-checker property only (CORE-01 pt2 / #177). *)
517519
let tv = fresh_tyvar 0 in
518520
(tv, TRef tv)
519521
| OpDeref ->
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell
3+
//
4+
// CORE-01 pt2 parser surface / #177: `&mut e` is now expressible. Two
5+
// exclusive borrows of the same owner must conflict — previously this
6+
// program could not even be written (no `&mut` expression surface).
7+
8+
module BorrowMutRefConflict;
9+
10+
fn bad() -> Int {
11+
let mut x = 5;
12+
let a = &mut x;
13+
let b = &mut x;
14+
*a
15+
}
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell
3+
//
4+
// CORE-01 pt2 parser surface / #177 non-regression guard: adding `&mut e`
5+
// must not perturb shared `&e` — multiple shared borrows are still fine.
6+
7+
module BorrowMutRefSharedOk;
8+
9+
fn good() -> Int {
10+
let x = 5;
11+
let a = &x;
12+
let b = &x;
13+
*a + *b
14+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell
3+
//
4+
// CORE-01 pt2 parser surface / #177: an exclusive `&mut` borrow held
5+
// while the owner is read = UseWhileExclusivelyBorrowed. The pt1 rule
6+
// existed but was unreachable from source until `&mut e` parsed.
7+
8+
module BorrowMutRefUseWhile;
9+
10+
fn bad() -> Int {
11+
let mut x = 5;
12+
let a = &mut x;
13+
let y = x;
14+
*a + y
15+
}

test/test_e2e.ml

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3751,9 +3751,41 @@ let test_borrow_return_refparam_ok () =
37513751
Alcotest.fail ("sound `return ref-param` spuriously rejected: "
37523752
^ Borrow.format_borrow_error e)
37533753

3754+
(* CORE-01 pt2 parser surface / #177 — `&mut e` exclusive-borrow surface.
3755+
These programs were previously *unrepresentable* (no `&mut` expression);
3756+
the pt1 shared-XOR-exclusive rules were unreachable from source. *)
3757+
let test_borrow_mutref_conflict () =
3758+
match borrow_result (fixture "borrow_mutref_conflict.affine") with
3759+
| Error (Borrow.ConflictingBorrow _) -> ()
3760+
| Error e ->
3761+
Alcotest.fail ("expected ConflictingBorrow (two &mut of one owner), got: "
3762+
^ Borrow.format_borrow_error e)
3763+
| Ok () -> Alcotest.fail "two `&mut x` did not conflict"
3764+
3765+
let test_borrow_mutref_use_while () =
3766+
match borrow_result (fixture "borrow_mutref_use_while.affine") with
3767+
| Error (Borrow.UseWhileExclusivelyBorrowed _) -> ()
3768+
| Error e ->
3769+
Alcotest.fail ("expected UseWhileExclusivelyBorrowed (read x while &mut x \
3770+
live), got: " ^ Borrow.format_borrow_error e)
3771+
| Ok () -> Alcotest.fail "read while `&mut` live was not rejected"
3772+
3773+
let test_borrow_mutref_shared_ok () =
3774+
match borrow_result (fixture "borrow_mutref_shared_ok.affine") with
3775+
| Ok () -> ()
3776+
| Error e ->
3777+
Alcotest.fail ("shared `&x` spuriously rejected after adding `&mut`: "
3778+
^ Borrow.format_borrow_error e)
3779+
37543780
let borrow_tests = [
37553781
Alcotest.test_case "BorrowOutlivesOwner: &local escapes its block"
37563782
`Quick test_borrow_outlives_owner;
3783+
Alcotest.test_case "&mut: two exclusive borrows conflict (#177 pt2 surface)"
3784+
`Quick test_borrow_mutref_conflict;
3785+
Alcotest.test_case "&mut: read while exclusively borrowed rejected (#177)"
3786+
`Quick test_borrow_mutref_use_while;
3787+
Alcotest.test_case "&mut added: shared &x still sound (no regression)"
3788+
`Quick test_borrow_mutref_shared_ok;
37573789
Alcotest.test_case "UseWhileExclusivelyBorrowed: mut+read in one call"
37583790
`Quick test_borrow_use_while_excl;
37593791
Alcotest.test_case "temporary call-arg borrow released (no over-reject)"

0 commit comments

Comments
 (0)