Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 16 additions & 7 deletions docs/TECH-DEBT.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
7 changes: 6 additions & 1 deletion lib/ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
30 changes: 19 additions & 11 deletions lib/borrow.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down Expand Up @@ -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) *)
Expand Down Expand Up @@ -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 *)
Expand Down Expand Up @@ -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.
*)
7 changes: 4 additions & 3 deletions lib/codegen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions lib/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down
4 changes: 3 additions & 1 deletion lib/typecheck.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
15 changes: 15 additions & 0 deletions test/e2e/fixtures/borrow_mutref_conflict.affine
Original file line number Diff line number Diff line change
@@ -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
}
14 changes: 14 additions & 0 deletions test/e2e/fixtures/borrow_mutref_shared_ok.affine
Original file line number Diff line number Diff line change
@@ -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
}
15 changes: 15 additions & 0 deletions test/e2e/fixtures/borrow_mutref_use_while.affine
Original file line number Diff line number Diff line change
@@ -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
}
32 changes: 32 additions & 0 deletions test/test_e2e.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)"
Expand Down
Loading