diff --git a/docs/TECH-DEBT.adoc b/docs/TECH-DEBT.adoc index 2ae8f133..02a0f707 100644 --- a/docs/TECH-DEBT.adoc +++ b/docs/TECH-DEBT.adoc @@ -93,13 +93,22 @@ at a *callee-owned* binding (local or by-value/`own` param) is now `BorrowOutlivesOwner` (pt1 only saw block tails — `return r` slipped through); `ref`/`mut` params are caller-owned and not flagged (no over-rejection; full stdlib AOT green). 3 hermetic tests in "E2E Borrow -Graph". *Part 2 residual — parser-gated (honest finding):* NLL/region -inference (Polonius); flow-sensitive escape via `outer = &x`; tighter -quantity integration. These are *not reachable unsoundnesses today* — the -surface to express them does not parse (`&mut e`, `-> &T`, `&`-in-literal, -bare block-statements), so the next move is the parser surface, then the -analysis. |S1 |pt1 #240 + pt2 return-escape DONE (Refs #177); pt2 residual -parser-gated — issue #177 +Graph". *Part 2 — `&mut e` parser surface LANDED* (Refs #177, gate +278→281, **zero Menhir conflict delta** — 21 S/R + 1 R/R baseline held; +`AMP MUT e` is unambiguous): the exclusive-borrow expression is now +expressible, so the pt1 shared-XOR-exclusive rules +(`ConflictingBorrow`/`UseWhileExclusivelyBorrowed`) are *reachable from +source* for the first time (3 hermetic "E2E Borrow Graph" tests; `&mut e` +typed/codegen'd like `&e` — exclusivity is a static borrow property). +`&`-in-`#{` literals and bare block-statements already parse on `main`; +`-> &T`/`&T` *type* sigil 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). *Part 2 residual — now the +analysis, not surface:* NLL/region inference (Polonius) + flow-sensitive +escape via `outer = &x` are now *expressible* (surface unblocked); the +remaining work is the dataflow analysis itself. |S1 |pt1 #240 + pt2 +return-escape + `&mut` surface DONE (Refs #177); residual = NLL analysis +— issue #177 |CORE-02 |Effect-handler dispatch on WasmGC (currently `UnsupportedFeature`; EH proposal or CPS). The #225 CPS line closes the async slice. |S2 |partial (PR3a/b/c merged; #234 generalises the recogniser) diff --git a/lib/ast.ml b/lib/ast.ml index 42dd2855..f6c9849f 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -198,7 +198,12 @@ and binary_op = | OpBitAnd | OpBitOr | OpBitXor | OpShl | OpShr and unary_op = - | OpNeg | OpNot | OpBitNot | OpRef | OpDeref + | OpNeg | OpNot | OpBitNot | OpRef | OpMutRef | OpDeref + (** [OpMutRef] is `&mut e` — an *exclusive* borrow expression. `&e` + is [OpRef] (shared). Only the borrow checker distinguishes them + (shared-XOR-exclusive); every other backend treats `&mut e` + exactly like `&e` (a reference is the same runtime pointer — + exclusivity is a static property). CORE-01 pt2 / #177. *) and assign_op = | AssignEq | AssignAdd | AssignSub | AssignMul | AssignDiv diff --git a/lib/borrow.ml b/lib/borrow.ml index 51cdb658..307d5e7d 100644 --- a/lib/borrow.ml +++ b/lib/borrow.ml @@ -198,7 +198,7 @@ let is_copy_expr (expr : expr) : bool = | ExprLit (LitBool _) -> true | ExprLit (LitChar _) -> true | ExprLit (LitUnit _) -> true - | ExprUnary (OpRef, _) -> true (* Reference creation produces a Copy pointer *) + | ExprUnary ((OpRef | OpMutRef), _) -> true (* Reference creation produces a Copy pointer *) | _ -> false (** 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 let rec ref_target (symbols : Symbol.t) (expr : expr) : place option = match expr with | ExprSpan (e, _) -> ref_target symbols e - | ExprUnary (OpRef, e) -> expr_to_place symbols e + | ExprUnary ((OpRef | OpMutRef), e) -> expr_to_place symbols e | _ -> None (** 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 : | ExprUnary (op, e) -> begin match op with - | OpRef -> - (* Taking a reference: &expr - creates a shared borrow *) + | OpRef | OpMutRef -> + (* `&expr` is a shared borrow; `&mut expr` an *exclusive* one. + This is the surface that finally makes an exclusive borrow + expressible — shared-XOR-exclusive then enforces it at use + sites (CORE-01 pt1 `UseWhileExclusivelyBorrowed`). *) + let kind = (match op with OpMutRef -> Exclusive | _ -> Shared) in begin match expr_to_place symbols e with | Some place -> let span = expr_span e in - let* _borrow = record_borrow state place Shared span in + let* _borrow = record_borrow state place kind span in Ok () | None -> (* Can't borrow non-place expressions, but check the expression *) @@ -1179,13 +1183,17 @@ let check_program (symbols : Symbol.t) (program : program) : unit result = flagged (probed: `fn ok(x: ref Int) -> ref Int { return x; }` passes). Sound + non-over-rejecting (full stdlib AOT + borrow suite green). - Still deferred to a later CORE-01 part (docs/TECH-DEBT.adoc) — and note - these are *parser-gated*: the surface to express them does not parse - today (`&mut e`, `-> &T`, `&`-in-literal, bare block-statements), so - they are not reachable unsoundnesses until the surface lands: + CORE-01 pt2 parser surface (2026-05-19): `&mut e` now parses + (ExprUnary OpMutRef; `AMP MUT e`, zero Menhir conflict delta) and is an + *Exclusive* borrow here — so shared-XOR-exclusive + return-escape are + reachable from real source for the first time. `&`-in-`#{` literals and + bare block-statements already parsed; the `-> &T`/`&T` *type* sigil was + deliberately not added (`ref T`/`mut T` keyword types already exist). + + Still deferred — now the *analysis*, no longer parser-gated: - Non-lexical lifetimes with region inference (Polonius-style). - Flow-sensitive escape via assignment to an outer mutable - (`outer = &x`) — blocked on assignment-of-borrow + inner-block-stmt - surface, not just the analysis. + (`outer = &x`) — now *expressible* (`&mut`, assignment, blocks all + parse); the remaining work is the dataflow analysis itself. - Tighter integration with the quantity checker for captured linears. *) diff --git a/lib/codegen.ml b/lib/codegen.ml index 8a3dd4fb..1b0c74b8 100644 --- a/lib/codegen.ml +++ b/lib/codegen.ml @@ -419,7 +419,7 @@ let gen_unop (op : unary_op) : instr result = | OpNeg -> Ok I32Sub (* 0 - x *) | OpNot -> Ok I32Eqz (* x == 0 *) | OpBitNot -> Ok I32Xor (* -1 ^ x *) - | OpRef -> Error (UnsupportedFeature "OpRef handled in ExprUnary") + | OpRef | OpMutRef -> Error (UnsupportedFeature "OpRef/OpMutRef handled in ExprUnary") | OpDeref -> Error (UnsupportedFeature "OpDeref handled in ExprUnary") (** 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 = | ExprUnary (op, operand) -> begin match op with - | OpRef -> - (* Take reference: &expr *) + | OpRef | OpMutRef -> + (* Take reference: &expr / &mut expr — same pointer representation; + exclusivity is a static borrow property (CORE-01 pt2 / #177). *) (* Allocate heap memory, store the value, return pointer *) let* (ctx', operand_code) = gen_expr ctx operand in let (ctx_with_heap, alloc_code) = gen_heap_alloc ctx' 4 in diff --git a/lib/parser.mly b/lib/parser.mly index 18448868..0438444d 100644 --- a/lib/parser.mly +++ b/lib/parser.mly @@ -768,6 +768,7 @@ expr_unary: | MINUS e = expr_unary { ExprUnary (OpNeg, e) } | BANG e = expr_unary { ExprUnary (OpNot, e) } | TILDE e = expr_unary { ExprUnary (OpBitNot, e) } + | AMP MUT e = expr_unary { ExprUnary (OpMutRef, e) } | AMP e = expr_unary { ExprUnary (OpRef, e) } | STAR e = expr_unary { ExprUnary (OpDeref, e) } | e = expr_postfix { e } diff --git a/lib/typecheck.ml b/lib/typecheck.ml index cb6354f6..5e072494 100644 --- a/lib/typecheck.ml +++ b/lib/typecheck.ml @@ -513,7 +513,9 @@ let type_of_unop (op : unary_op) : ty * ty = | OpNeg -> (ty_int, ty_int) | OpNot -> (ty_bool, ty_bool) | OpBitNot -> (ty_int, ty_int) - | OpRef -> + | OpRef | OpMutRef -> + (* `&mut e` types exactly like `&e` — a reference. Exclusivity is a + static borrow-checker property only (CORE-01 pt2 / #177). *) let tv = fresh_tyvar 0 in (tv, TRef tv) | OpDeref -> diff --git a/test/e2e/fixtures/borrow_mutref_conflict.affine b/test/e2e/fixtures/borrow_mutref_conflict.affine new file mode 100644 index 00000000..62d75084 --- /dev/null +++ b/test/e2e/fixtures/borrow_mutref_conflict.affine @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// CORE-01 pt2 parser surface / #177: `&mut e` is now expressible. Two +// exclusive borrows of the same owner must conflict — previously this +// program could not even be written (no `&mut` expression surface). + +module BorrowMutRefConflict; + +fn bad() -> Int { + let mut x = 5; + let a = &mut x; + let b = &mut x; + *a +} diff --git a/test/e2e/fixtures/borrow_mutref_shared_ok.affine b/test/e2e/fixtures/borrow_mutref_shared_ok.affine new file mode 100644 index 00000000..d986f85d --- /dev/null +++ b/test/e2e/fixtures/borrow_mutref_shared_ok.affine @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// CORE-01 pt2 parser surface / #177 non-regression guard: adding `&mut e` +// must not perturb shared `&e` — multiple shared borrows are still fine. + +module BorrowMutRefSharedOk; + +fn good() -> Int { + let x = 5; + let a = &x; + let b = &x; + *a + *b +} diff --git a/test/e2e/fixtures/borrow_mutref_use_while.affine b/test/e2e/fixtures/borrow_mutref_use_while.affine new file mode 100644 index 00000000..aeffa4c1 --- /dev/null +++ b/test/e2e/fixtures/borrow_mutref_use_while.affine @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell +// +// CORE-01 pt2 parser surface / #177: an exclusive `&mut` borrow held +// while the owner is read = UseWhileExclusivelyBorrowed. The pt1 rule +// existed but was unreachable from source until `&mut e` parsed. + +module BorrowMutRefUseWhile; + +fn bad() -> Int { + let mut x = 5; + let a = &mut x; + let y = x; + *a + y +} diff --git a/test/test_e2e.ml b/test/test_e2e.ml index 83bbf603..b5e43dba 100644 --- a/test/test_e2e.ml +++ b/test/test_e2e.ml @@ -3751,9 +3751,41 @@ let test_borrow_return_refparam_ok () = Alcotest.fail ("sound `return ref-param` spuriously rejected: " ^ Borrow.format_borrow_error e) +(* CORE-01 pt2 parser surface / #177 — `&mut e` exclusive-borrow surface. + These programs were previously *unrepresentable* (no `&mut` expression); + the pt1 shared-XOR-exclusive rules were unreachable from source. *) +let test_borrow_mutref_conflict () = + match borrow_result (fixture "borrow_mutref_conflict.affine") with + | Error (Borrow.ConflictingBorrow _) -> () + | Error e -> + Alcotest.fail ("expected ConflictingBorrow (two &mut of one owner), got: " + ^ Borrow.format_borrow_error e) + | Ok () -> Alcotest.fail "two `&mut x` did not conflict" + +let test_borrow_mutref_use_while () = + match borrow_result (fixture "borrow_mutref_use_while.affine") with + | Error (Borrow.UseWhileExclusivelyBorrowed _) -> () + | Error e -> + Alcotest.fail ("expected UseWhileExclusivelyBorrowed (read x while &mut x \ + live), got: " ^ Borrow.format_borrow_error e) + | Ok () -> Alcotest.fail "read while `&mut` live was not rejected" + +let test_borrow_mutref_shared_ok () = + match borrow_result (fixture "borrow_mutref_shared_ok.affine") with + | Ok () -> () + | Error e -> + Alcotest.fail ("shared `&x` spuriously rejected after adding `&mut`: " + ^ Borrow.format_borrow_error e) + let borrow_tests = [ Alcotest.test_case "BorrowOutlivesOwner: &local escapes its block" `Quick test_borrow_outlives_owner; + Alcotest.test_case "&mut: two exclusive borrows conflict (#177 pt2 surface)" + `Quick test_borrow_mutref_conflict; + Alcotest.test_case "&mut: read while exclusively borrowed rejected (#177)" + `Quick test_borrow_mutref_use_while; + Alcotest.test_case "&mut added: shared &x still sound (no regression)" + `Quick test_borrow_mutref_shared_ok; Alcotest.test_case "UseWhileExclusivelyBorrowed: mut+read in one call" `Quick test_borrow_use_while_excl; Alcotest.test_case "temporary call-arg borrow released (no over-reject)"