Skip to content

Commit 456ff2d

Browse files
hyperpolymathclaude
andcommitted
feat(borrow): wire borrow checker into compile pipeline; E0501-E0506 diagnostics
Borrow checker was fully modelled (lib/borrow.ml, 669 LOC) but never invoked. This commit makes it a live gate on check/compile paths. lib/borrow.ml: - PlaceVar now carries (string * symbol_id) so error messages name the variable rather than printing an opaque integer symbol ID. - format_place, format_span, format_borrow_error added — human-readable diagnostics with file:line:col for both the use site and the move/borrow site (e.g. "use of moved value: `v`\n used at foo.affine:8:7\n moved at foo.affine:7:15"). - ExprMatch arm processing fixed: each arm now runs against an independent snapshot of the post-scrutinee state; after the match, borrows are the intersection of all arm borrows and moves are the union. - check_block now snapshots borrows at block entry and restores them at block exit — a lexical-lifetime approximation. - is_copy_type updated to use TyCon/TyRef constructors. - record_borrow mutability check restructured (unit/result discipline). - lib/dune: borrow module added to the library. lib/json_output.ml: - of_borrow_error: E0501 (UseAfterMove) through E0506 (CannotBorrowAsMutable). lib/face.ml: - format_borrow_error: face-aware wrapper with Python-face prefixes. bin/main.ml: - Borrow.check_program wired at all 4 Typecheck.check_program success sites. All 73 tests pass. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 919ec34 commit 456ff2d

5 files changed

Lines changed: 260 additions & 88 deletions

File tree

bin/main.ml

Lines changed: 89 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -151,7 +151,11 @@ let check_file face json path =
151151
(match Affinescript.Typecheck.check_program resolve_ctx.symbols prog with
152152
| Error e ->
153153
add (Affinescript.Json_output.of_type_error e)
154-
| Ok _ctx -> ()))
154+
| Ok _ctx ->
155+
(match Affinescript.Borrow.check_program resolve_ctx.symbols prog with
156+
| Error e ->
157+
add (Affinescript.Json_output.of_borrow_error e)
158+
| Ok () -> ())))
155159
with
156160
| Affinescript.Lexer.Lexer_error (msg, pos) ->
157161
add (Affinescript.Json_output.of_lexer_error msg pos path)
@@ -190,8 +194,14 @@ let check_file face json path =
190194
(Affinescript.Face.format_type_error face e);
191195
`Error (false, "Type error")
192196
| Ok _ctx ->
193-
Format.printf "Type checking passed@.";
194-
`Ok ()))
197+
(match Affinescript.Borrow.check_program resolve_ctx.symbols prog with
198+
| Error e ->
199+
Format.eprintf "@[<v>Borrow error: %s@]@."
200+
(Affinescript.Face.format_borrow_error face e);
201+
`Error (false, "Borrow error")
202+
| Ok () ->
203+
Format.printf "Type checking passed@.";
204+
`Ok ())))
195205
with
196206
| Affinescript.Lexer.Lexer_error (msg, pos) ->
197207
Format.eprintf "@[<v>%s:%d:%d: lexer error: %s@]@." path pos.line pos.col msg;
@@ -304,37 +314,41 @@ let compile_file face json wasm_gc path output =
304314
| Error e ->
305315
add (Affinescript.Json_output.of_type_error e)
306316
| Ok _type_ctx ->
307-
let is_julia = Filename.check_suffix output ".jl" in
308-
if is_julia then begin
309-
match Affinescript.Julia_codegen.codegen_julia prog resolve_ctx.symbols with
310-
| Error msg ->
311-
add { severity = Error; code = "E0800";
312-
message = Printf.sprintf "Julia codegen error: %s" msg;
313-
span = Affinescript.Span.dummy; help = None; labels = [] }
314-
| Ok julia_code ->
315-
let oc = open_out output in
316-
output_string oc julia_code;
317-
close_out oc
318-
end else if wasm_gc then begin
319-
match Affinescript.Codegen_gc.generate_gc_module prog with
320-
| Error e ->
321-
add { severity = Error; code = "E0802";
322-
message = Printf.sprintf "WASM GC codegen error: %s"
323-
(Affinescript.Codegen_gc.format_codegen_error e);
324-
span = Affinescript.Span.dummy; help = None; labels = [] }
325-
| Ok gc_module ->
326-
Affinescript.Wasm_gc_encode.write_gc_module_to_file output gc_module
327-
end else begin
328-
let optimized_prog = Affinescript.Opt.fold_constants_program prog in
329-
match Affinescript.Codegen.generate_module optimized_prog with
330-
| Error e ->
331-
add { severity = Error; code = "E0801";
332-
message = Printf.sprintf "WASM codegen error: %s"
333-
(Affinescript.Codegen.show_codegen_error e);
334-
span = Affinescript.Span.dummy; help = None; labels = [] }
335-
| Ok wasm_module ->
336-
Affinescript.Wasm_encode.write_module_to_file output wasm_module
337-
end))
317+
(match Affinescript.Borrow.check_program resolve_ctx.symbols prog with
318+
| Error e ->
319+
add (Affinescript.Json_output.of_borrow_error e)
320+
| Ok () ->
321+
let is_julia = Filename.check_suffix output ".jl" in
322+
if is_julia then begin
323+
match Affinescript.Julia_codegen.codegen_julia prog resolve_ctx.symbols with
324+
| Error msg ->
325+
add { severity = Error; code = "E0800";
326+
message = Printf.sprintf "Julia codegen error: %s" msg;
327+
span = Affinescript.Span.dummy; help = None; labels = [] }
328+
| Ok julia_code ->
329+
let oc = open_out output in
330+
output_string oc julia_code;
331+
close_out oc
332+
end else if wasm_gc then begin
333+
match Affinescript.Codegen_gc.generate_gc_module prog with
334+
| Error e ->
335+
add { severity = Error; code = "E0802";
336+
message = Printf.sprintf "WASM GC codegen error: %s"
337+
(Affinescript.Codegen_gc.format_codegen_error e);
338+
span = Affinescript.Span.dummy; help = None; labels = [] }
339+
| Ok gc_module ->
340+
Affinescript.Wasm_gc_encode.write_gc_module_to_file output gc_module
341+
end else begin
342+
let optimized_prog = Affinescript.Opt.fold_constants_program prog in
343+
match Affinescript.Codegen.generate_module optimized_prog with
344+
| Error e ->
345+
add { severity = Error; code = "E0801";
346+
message = Printf.sprintf "WASM codegen error: %s"
347+
(Affinescript.Codegen.show_codegen_error e);
348+
span = Affinescript.Span.dummy; help = None; labels = [] }
349+
| Ok wasm_module ->
350+
Affinescript.Wasm_encode.write_module_to_file output wasm_module
351+
end)))
338352
with
339353
| Affinescript.Lexer.Lexer_error (msg, pos) ->
340354
add (Affinescript.Json_output.of_lexer_error msg pos path)
@@ -359,39 +373,47 @@ let compile_file face json wasm_gc path output =
359373
(Affinescript.Face.format_type_error face e);
360374
`Error (false, "Type error")
361375
| Ok _type_ctx ->
362-
let is_julia = Filename.check_suffix output ".jl" in
363-
if is_julia then
364-
(match Affinescript.Julia_codegen.codegen_julia prog resolve_ctx.symbols with
365-
| Error e ->
366-
Format.eprintf "@[<v>Julia codegen error: %s@]@." e;
367-
`Error (false, "Julia codegen error")
368-
| Ok julia_code ->
369-
let oc = open_out output in
370-
output_string oc julia_code;
371-
close_out oc;
372-
Format.printf "Compiled %s -> %s (Julia)@." path output;
373-
`Ok ())
374-
else if wasm_gc then
375-
(match Affinescript.Codegen_gc.generate_gc_module prog with
376-
| Error e ->
377-
Format.eprintf "@[<v>%s@]@."
378-
(Affinescript.Codegen_gc.format_codegen_error e);
379-
`Error (false, "WASM GC codegen error")
380-
| Ok gc_module ->
381-
Affinescript.Wasm_gc_encode.write_gc_module_to_file output gc_module;
382-
Format.printf "Compiled %s -> %s (WASM GC)@." path output;
383-
`Ok ())
384-
else
385-
let optimized_prog = Affinescript.Opt.fold_constants_program prog in
386-
(match Affinescript.Codegen.generate_module optimized_prog with
387-
| Error e ->
388-
Format.eprintf "@[<v>Code generation error: %s@]@."
389-
(Affinescript.Codegen.show_codegen_error e);
390-
`Error (false, "Code generation error")
391-
| Ok wasm_module ->
392-
Affinescript.Wasm_encode.write_module_to_file output wasm_module;
393-
Format.printf "Compiled %s -> %s (WASM)@." path output;
394-
`Ok ())))
376+
(match Affinescript.Borrow.check_program resolve_ctx.symbols prog with
377+
| Error e ->
378+
Format.eprintf "@[<v>Borrow error: %s@]@."
379+
(Affinescript.Face.format_borrow_error face e);
380+
`Error (false, "Borrow error")
381+
| Ok () ->
382+
begin
383+
let is_julia = Filename.check_suffix output ".jl" in
384+
if is_julia then
385+
(match Affinescript.Julia_codegen.codegen_julia prog resolve_ctx.symbols with
386+
| Error e ->
387+
Format.eprintf "@[<v>Julia codegen error: %s@]@." e;
388+
`Error (false, "Julia codegen error")
389+
| Ok julia_code ->
390+
let oc = open_out output in
391+
output_string oc julia_code;
392+
close_out oc;
393+
Format.printf "Compiled %s -> %s (Julia)@." path output;
394+
`Ok ())
395+
else if wasm_gc then
396+
(match Affinescript.Codegen_gc.generate_gc_module prog with
397+
| Error e ->
398+
Format.eprintf "@[<v>%s@]@."
399+
(Affinescript.Codegen_gc.format_codegen_error e);
400+
`Error (false, "WASM GC codegen error")
401+
| Ok gc_module ->
402+
Affinescript.Wasm_gc_encode.write_gc_module_to_file output gc_module;
403+
Format.printf "Compiled %s -> %s (WASM GC)@." path output;
404+
`Ok ())
405+
else
406+
let optimized_prog = Affinescript.Opt.fold_constants_program prog in
407+
(match Affinescript.Codegen.generate_module optimized_prog with
408+
| Error e ->
409+
Format.eprintf "@[<v>Code generation error: %s@]@."
410+
(Affinescript.Codegen.show_codegen_error e);
411+
`Error (false, "Code generation error")
412+
| Ok wasm_module ->
413+
Affinescript.Wasm_encode.write_module_to_file output wasm_module;
414+
Format.printf "Compiled %s -> %s (WASM)@." path output;
415+
`Ok ())
416+
end)))
395417
with
396418
| Affinescript.Lexer.Lexer_error (msg, pos) ->
397419
Format.eprintf "@[<v>%s:%d:%d: lexer error: %s@]@." path pos.line pos.col msg;

lib/borrow.ml

Lines changed: 127 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ open Ast
1515

1616
(** A place is an l-value that can be borrowed *)
1717
type place =
18-
| PlaceVar of Symbol.symbol_id
18+
| PlaceVar of string * Symbol.symbol_id (** human name, symbol id *)
1919
| PlaceField of place * string
2020
| PlaceIndex of place * int option (** None for dynamic index *)
2121
| PlaceDeref of place
@@ -129,10 +129,10 @@ let rec is_copy_type (ty_opt : type_expr option) : bool =
129129
| None -> false (* Unknown type, assume not Copy *)
130130
| Some ty ->
131131
begin match ty with
132-
| TyNamed id when id.name = "Int" || id.name = "Bool" || id.name = "Char" -> true
133-
| TyNamed id when id.name = "Unit" -> true
132+
| TyCon id when id.name = "Int" || id.name = "Bool" || id.name = "Char" -> true
133+
| TyCon id when id.name = "Unit" -> true
134134
| TyTuple tys -> List.for_all (fun t -> is_copy_type (Some t)) tys
135-
| TyApp (TyNamed id, _) when id.name = "Ref" -> true (* Shared references are Copy *)
135+
| TyRef _ -> true (* Shared references are Copy *)
136136
| _ -> false (* Records, arrays, owned types, etc. are not Copy *)
137137
end
138138

@@ -149,7 +149,7 @@ let is_copy_expr (expr : expr) : bool =
149149
(** Check if two places overlap *)
150150
let rec places_overlap (p1 : place) (p2 : place) : bool =
151151
match (p1, p2) with
152-
| (PlaceVar v1, PlaceVar v2) -> v1 = v2
152+
| (PlaceVar (_, v1), PlaceVar (_, v2)) -> v1 = v2
153153
| (PlaceField (base1, _), PlaceField (base2, _)) ->
154154
places_overlap base1 base2
155155
| (PlaceVar _, PlaceField (base, _))
@@ -199,14 +199,17 @@ let record_borrow (state : state) (place : place) (kind : borrow_kind)
199199
Error (UseAfterMove (place, span, move_site))
200200
| None ->
201201
(* Check if trying to mutably borrow an immutable place *)
202-
begin match kind with
202+
let mut_check = match kind with
203203
| Exclusive ->
204204
if not (is_mutable state place) then
205205
Error (CannotBorrowAsMutable (place, span))
206206
else
207-
()
208-
| Shared -> ()
209-
end;
207+
Ok ()
208+
| Shared -> Ok ()
209+
in
210+
match mut_check with
211+
| Error _ as err -> err
212+
| Ok () ->
210213
let new_borrow = {
211214
b_place = place;
212215
b_kind = kind;
@@ -229,6 +232,52 @@ let check_use (state : state) (place : place) (span : Span.t) : unit result =
229232
| Some move_site -> Error (UseAfterMove (place, span, move_site))
230233
| None -> Ok ()
231234

235+
(** Format a place for display in error messages. *)
236+
let rec format_place (p : place) : string =
237+
match p with
238+
| PlaceVar (name, _) -> name
239+
| PlaceField (base, f) -> format_place base ^ "." ^ f
240+
| PlaceIndex (base, Some i) -> format_place base ^ "[" ^ string_of_int i ^ "]"
241+
| PlaceIndex (base, None) -> format_place base ^ "[_]"
242+
| PlaceDeref p' -> "*" ^ format_place p'
243+
244+
(** Format a span for display. *)
245+
let format_span (span : Span.t) : string =
246+
Format.asprintf "%a" Span.pp_short span
247+
248+
(** Format a borrow error as a human-readable string. *)
249+
let format_borrow_error (e : borrow_error) : string =
250+
match e with
251+
| UseAfterMove (place, use_span, move_span) ->
252+
Printf.sprintf
253+
"use of moved value: `%s`\n \
254+
value used at %s\n \
255+
value moved at %s"
256+
(format_place place) (format_span use_span) (format_span move_span)
257+
| ConflictingBorrow (b1, b2) ->
258+
Printf.sprintf
259+
"conflicting borrows on `%s`:\n \
260+
%s borrow (id %d) at %s conflicts with earlier %s borrow (id %d) at %s"
261+
(format_place b1.b_place)
262+
(show_borrow_kind b1.b_kind) b1.b_id (format_span b1.b_span)
263+
(show_borrow_kind b2.b_kind) b2.b_id (format_span b2.b_span)
264+
| BorrowOutlivesOwner (b, sym_id) ->
265+
Printf.sprintf
266+
"borrow of `%s` (id %d) outlives its owner (symbol %d)"
267+
(format_place b.b_place) b.b_id sym_id
268+
| MoveWhileBorrowed (place, b) ->
269+
Printf.sprintf
270+
"cannot move `%s` while it is %s-borrowed at %s"
271+
(format_place place) (show_borrow_kind b.b_kind) (format_span b.b_span)
272+
| CannotMoveOutOfBorrow (place, b) ->
273+
Printf.sprintf
274+
"cannot move out of `%s`, which is behind a %s borrow at %s"
275+
(format_place place) (show_borrow_kind b.b_kind) (format_span b.b_span)
276+
| CannotBorrowAsMutable (place, span) ->
277+
Printf.sprintf
278+
"cannot borrow `%s` as mutable — it is not declared with `let mut` (at %s)"
279+
(format_place place) (format_span span)
280+
232281
(** Get span from an expression *)
233282
let rec expr_span (expr : expr) : Span.t =
234283
match expr with
@@ -327,7 +376,7 @@ let rec expr_to_place (symbols : Symbol.t) (expr : expr) : place option =
327376
match expr with
328377
| ExprVar id ->
329378
begin match lookup_symbol_by_name symbols id.name with
330-
| Some sym -> Some (PlaceVar sym.sym_id)
379+
| Some sym -> Some (PlaceVar (id.name, sym.sym_id))
331380
| None -> None
332381
end
333382
| ExprField (base, field) ->
@@ -447,14 +496,61 @@ let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr :
447496

448497
| ExprMatch em ->
449498
let* () = check_expr ctx state symbols em.em_scrutinee in
450-
List.fold_left (fun acc arm ->
451-
let* () = acc in
452-
let* () = match arm.ma_guard with
453-
| Some g -> check_expr ctx state symbols g
454-
| None -> Ok ()
499+
(* Each arm is independent: run each against the post-scrutinee state,
500+
then merge. A place is moved after the match if it is moved in any
501+
arm (conservative: we require moves to happen in all arms before
502+
assuming the value is gone from the outer scope). Borrows from
503+
individual arms expire at arm exit. *)
504+
let base_borrows = state.borrows in
505+
let base_moved = state.moved in
506+
let arm_results = List.map (fun arm ->
507+
(* Reset to post-scrutinee state for each arm *)
508+
state.borrows <- base_borrows;
509+
state.moved <- base_moved;
510+
let r =
511+
let open Result in
512+
bind (match arm.ma_guard with
513+
| Some g -> check_expr ctx state symbols g
514+
| None -> Ok ())
515+
(fun () -> check_expr ctx state symbols arm.ma_body)
516+
in
517+
(r, state.borrows, state.moved)
518+
) em.em_arms in
519+
(* Propagate the first error, or merge successful states *)
520+
let errors = List.filter_map (fun (r, _, _) ->
521+
match r with Error e -> Some e | Ok () -> None) arm_results in
522+
begin match errors with
523+
| e :: _ -> Error e
524+
| [] ->
525+
(* Borrows: active after match only if active in ALL arms *)
526+
let all_borrows = List.map (fun (_, bs, _) -> bs) arm_results in
527+
let merged_borrows = match all_borrows with
528+
| [] -> base_borrows
529+
| first :: rest ->
530+
List.fold_left (fun acc arm_borrows ->
531+
List.filter (fun b ->
532+
List.exists (fun b' -> b.b_id = b'.b_id) arm_borrows
533+
) acc
534+
) first rest
455535
in
456-
check_expr ctx state symbols arm.ma_body
457-
) (Ok ()) em.em_arms
536+
(* Moves: conservative union — moved in any arm *)
537+
let all_moves = List.concat_map (fun (_, _, ms) ->
538+
List.filter (fun mr ->
539+
not (List.exists (fun base_mr ->
540+
places_overlap mr.m_place base_mr.m_place
541+
) base_moved)
542+
) ms
543+
) arm_results in
544+
(* Deduplicate moves by place *)
545+
let unique_moves = List.fold_left (fun acc mr ->
546+
if List.exists (fun mr' -> places_overlap mr.m_place mr'.m_place) acc
547+
then acc
548+
else mr :: acc
549+
) [] all_moves in
550+
state.borrows <- merged_borrows;
551+
state.moved <- base_moved @ unique_moves;
552+
Ok ()
553+
end
458554

459555
| ExprTuple exprs ->
460556
List.fold_left (fun acc e ->
@@ -581,13 +677,24 @@ let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr :
581677
check_expr ctx state symbols e
582678

583679
and check_block (ctx : context) (state : state) (symbols : Symbol.t) (blk : block) : unit result =
680+
(* Snapshot borrows at block entry. Borrows created inside this block for
681+
block-local variables expire at block exit (lexical lifetimes).
682+
Moves persist — a moved value stays moved after the block. *)
683+
let borrows_at_entry = state.borrows in
584684
let* () = List.fold_left (fun acc stmt ->
585685
let* () = acc in
586686
check_stmt ctx state symbols stmt
587687
) (Ok ()) blk.blk_stmts in
588-
match blk.blk_expr with
589-
| Some e -> check_expr ctx state symbols e
590-
| None -> Ok ()
688+
let* () = match blk.blk_expr with
689+
| Some e -> check_expr ctx state symbols e
690+
| None -> Ok ()
691+
in
692+
(* End borrows for places bound in this block: restore to pre-block borrows,
693+
keeping only those that existed before the block (i.e., borrow outer-scope
694+
variables that the block merely uses — these are unaffected).
695+
This is a conservative lexical-lifetime approximation. *)
696+
state.borrows <- borrows_at_entry;
697+
Ok ()
591698

592699
and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt) : unit result =
593700
match stmt with

0 commit comments

Comments
 (0)