fix(compiler): demand promotion targets the escaping projection's class
The escape hook promoted the borrow-root local's class, so `return h.box` over-promoted the container `Holder` alongside `Box`. Now `owner.ml`'s `transfer` passes the escaping place's type (`place_ty p`) as `~promote_class`, so only the value that actually escapes is promoted. - escape: takes ~promote_class; records it in collect mode, else reports WO-E304. - borrow-escape.wo now promotes only Box (was Box + Holder); rc.wo sans @gc still promotes Cache. Verified: woc-test 566/0, test_diag 14/0, oop-e2e 79/0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This commit is contained in:
parent
cc5228a2cf
commit
c301d1acb1
2 changed files with 15 additions and 14 deletions
|
|
@ -13,10 +13,9 @@
|
|||
`infer`, so `Types.is_gc_class` — which field-kind derivation, owner
|
||||
exemptions, and the class flag all key off — answers identically everywhere.
|
||||
|
||||
KNOWN LIMITATION (to refine with the Phase-3 landing): the demand hook
|
||||
promotes the escaping *root local's* class, so `return h.box` over-promotes
|
||||
`Holder` as well as `Box`. It should promote the escaping projection's type
|
||||
only. Sound (never under-promotes) but imprecise. *)
|
||||
The demand hook promotes the escaping *projection's* type (owner.ml's
|
||||
`transfer` passes `place_ty p`), so `return h.box` promotes `Box`, never the
|
||||
container `Holder`. *)
|
||||
|
||||
module SMap = Types.StringMap
|
||||
|
||||
|
|
|
|||
|
|
@ -1075,15 +1075,15 @@ let class_of_ty (syms : Types.symbols) (t : Ast.field_ty) : string option =
|
|||
| Ast.Scalar n when Types.StringMap.mem n syms.Types.classes -> Some n
|
||||
| _ -> None
|
||||
|
||||
let escape (ctx : ctx) (l : local) ~(pos : Ast.pos) ~message : unit =
|
||||
match ctx.promote with
|
||||
| Some record -> (
|
||||
match class_of_ty ctx.syms l.l_ty with
|
||||
| Some c -> record c (* demand promotion instead of WO-E304 *)
|
||||
| None ->
|
||||
report ctx ~code:borrow_escape_code ~pos ~message ~rel:l.l_pos
|
||||
~label:(borrow_label l))
|
||||
| None ->
|
||||
let escape (ctx : ctx) (l : local) ~(pos : Ast.pos) ~message
|
||||
~(promote_class : string option) : unit =
|
||||
(* `promote_class` is the class of the value that actually escapes (the
|
||||
escaping place's type), not the borrow-root local's — so `return h.box`
|
||||
promotes `Box`, never `Holder`. In collect mode with a class in hand, record
|
||||
it; otherwise report WO-E304. *)
|
||||
match (ctx.promote, promote_class) with
|
||||
| Some record, Some c -> record c
|
||||
| _ ->
|
||||
report ctx ~code:borrow_escape_code ~pos ~message ~rel:l.l_pos
|
||||
~label:(borrow_label l)
|
||||
|
||||
|
|
@ -1139,7 +1139,9 @@ let transfer (ctx : ctx) (p : place) ~(what : string) : bool =
|
|||
escape ctx l ~pos:p.ppos
|
||||
~message:
|
||||
(Printf.sprintf "borrow of `%s` %s — borrows cannot outlive their scope" (place_text p)
|
||||
what);
|
||||
what)
|
||||
~promote_class:
|
||||
(match place_ty ctx p with Some t -> class_of_ty ctx.syms t | None -> None);
|
||||
false
|
||||
| None -> (
|
||||
match root_local ctx p with
|
||||
|
|
|
|||
Loading…
Reference in a new issue