JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

A value that owns storage is never copied out of read-only storage, and two arguments at one type variable meet at const

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-25 13:30:47 +07:00
parent 0358f6637c
commit c6ad71dc5b
5 changed files with 247 additions and 78 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

173
lib/check.ml
View File

@ -556,8 +556,11 @@ type ctx = {
the outer scope is a list and the names on it were not all written for the outer scope is a list and the names on it were not all written for
this body's sake. *) this body's sake. *)
mutable caught : (string * (binding * int)) list; mutable caught : (string * (binding * int)) list;
(* Locals bound from read-only storage, and the view each came through. *) (* Whether the form being checked is the target of a place — indexed,
mutable const_locals : (int * Types.t) list; sliced, a field read, its address taken — rather than a value. Granted by
[check_target] to the one form it checks and withdrawn at the top of
[check]. See [refuse_owned_copy]. *)
mutable place_ok : bool;
(* The context this body was lifted out of, so that capture can be (* The context this body was lifted out of, so that capture can be
transitive: an [fn] inside an [fn] naming a local of the function both transitive: an [fn] inside an [fn] naming a local of the function both
were written in is captured by the middle one and then by the inner one were written in is captured by the middle one and then by the inner one
@ -1859,7 +1862,16 @@ let rec bind_ty ?(widen = false) ?(ro = true) subst (pat : Types.t)
| Types.Var v, a -> | Types.Var v, a ->
(match List.assoc_opt v !subst with (match List.assoc_opt v !subst with
| None -> subst := (v, a) :: !subst; true | None -> subst := (v, a) :: !subst; true
| Some b -> Types.equal a b) | Some b when Types.equal a b -> true
(* Two arguments that differ only in const bind the variable to the
read-only one, whichever came first — the same meeting an [if]'s two
branches have. [expect] converts the writable argument afterwards. *)
| Some b when ro ->
(match Types.const_join a b with
| Some j ->
subst := (v, j) :: List.remove_assoc v !subst; true
| None -> false)
| Some _ -> false)
| Types.Slice (m, p), Types.Slice (m', a) | Types.Slice (m, p), Types.Slice (m', a)
when m = m' || (ro && m = Types.Const) -> when m = m' || (ro && m = Types.Const) ->
bind_ty ~ro:(m = Types.Const) subst p a bind_ty ~ro:(m = Types.Const) subst p a
@ -2198,12 +2210,11 @@ let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc))
an array that is. The last slice stepped through decides, because the an array that is. The last slice stepped through decides, because the
const is shallow — an element of a [[const [u8]]] is itself a writable const is shallow — an element of a [[const [u8]]] is itself a writable
[[u8]], and what it views is not the outer slice's to protect. *) [[u8]], and what it views is not the outer slice's to protect. *)
let rec const_reached ?(local = fun (_ : int) -> None) (e : Tast.expr) = let rec const_reached (e : Tast.expr) =
match e.Tast.e with match e.Tast.e with
| Tast.Prim (Tast.At, target :: idx) -> | Tast.Prim (Tast.At, target :: idx) ->
const_steps (const_reached ~local target) target.Tast.ty (List.length idx) const_steps (const_reached target) target.Tast.ty (List.length idx)
| Tast.Field (target, _) -> const_reached ~local target | Tast.Field (target, _) -> const_reached target
| Tast.Local s -> local s
| Tast.Deref p -> | Tast.Deref p ->
(match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None) (match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None)
| _ -> None | _ -> None
@ -2222,13 +2233,12 @@ and const_steps ro (ty : Types.t) n =
compiles. Only for elements that own nothing: an element holding a Vec or compiles. Only for elements that own nothing: an element holding a Vec or
a Map — directly or inside a struct — would copy only its header, and the a Map — directly or inside a struct — would copy only its header, and the
copy would share the original's block. *) copy would share the original's block. *)
let const_copy (e : Types.t) = let const_copy env (e : Types.t) =
match e with if owning env e then None
| Types.Vec _ | Types.Map _ | Types.Named _ -> None else Some (Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e))
| _ -> Some (Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e))
(* A store through a read-only view: a [[const T]] or a (Ptr const T). *) (* A store through a read-only view: a [[const T]] or a (Ptr const T). *)
let refuse_const_place loc (view : Types.t) = let refuse_const_place env loc (view : Types.t) =
match view with match view with
| Types.Ptr (_, ((Types.Vec _ | Types.Map _) as t)) -> | Types.Ptr (_, ((Types.Vec _ | Types.Map _) as t)) ->
Loc.failk "check/store-through-const" loc Loc.failk "check/store-through-const" loc
@ -2247,7 +2257,7 @@ let refuse_const_place loc (view : Types.t) =
"this writes through a %s, which can only be read, so the element is a \ "this writes through a %s, which can only be read, so the element is a \
value and not a place. %s" value and not a place. %s"
(Types.to_string view) (Types.to_string view)
(match const_copy elem with (match const_copy env elem with
| Some c -> | Some c ->
Printf.sprintf Printf.sprintf
"Write into a slice that can be written: %s copies v's elements \ "Write into a slice that can be written: %s copies v's elements \
@ -3096,14 +3106,14 @@ let numeric_note ~(want : Types.t) ~(got : Types.t) =
copies it names compile today: [string] reads any byte slice and [bytes] copies it names compile today: [string] reads any byte slice and [bytes]
copies a string, and [into] pushes any slice's elements into a Vec that copies a string, and [into] pushes any slice's elements into a Vec that
[slice] then views. *) [slice] then views. *)
let const_note ~(want : Types.t) ~(got : Types.t) = let const_note env ~(want : Types.t) ~(got : Types.t) =
match want, got with match want, got with
| Types.Slice (Types.Mut, e), Types.Slice (Types.Const, e') | Types.Slice (Types.Mut, e), Types.Slice (Types.Const, e')
when Types.equal e e' -> when Types.equal e e' ->
let copy = let copy =
match e with match e with
| Types.Int Types.U8 -> Some "(bytes (string v))" | Types.Int Types.U8 -> Some "(bytes (string v))"
| _ -> const_copy e | _ -> const_copy env e
in in
Printf.sprintf Printf.sprintf
" — a %s can only be read, and never becomes a %s that can be written \ " — a %s can only be read, and never becomes a %s that can be written \
@ -3200,7 +3210,7 @@ let expect ctx loc ~want (got : Tast.expr) =
Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s" Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s"
(Types.to_string w) (Types.to_string got.Tast.ty) (Types.to_string w) (Types.to_string got.Tast.ty)
(numeric_note ~want:w ~got:got.Tast.ty) (numeric_note ~want:w ~got:got.Tast.ty)
(const_note ~want:w ~got:got.Tast.ty) (const_note ctx.env ~want:w ~got:got.Tast.ty)
(* Something a [break] may not jump out of, named so the refusal can say which. (* Something a [break] may not jump out of, named so the refusal can say which.
See [lentry]: it is a barrier and not a blanket refusal, so a loop written See [lentry]: it is a barrier and not a blanket refusal, so a loop written
@ -3262,7 +3272,7 @@ let hash_ty = Types.Int Types.U64
would share a slot counter. *) would share a slot counter. *)
let invented_ctx env ret = let invented_ctx env ret =
{ env; ret; slots = 0; slot_tys = []; slot_names = []; scope = []; { env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; const_locals = []; envslot = None; parent = None; in_frames = None; loops = []; tail = false; defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; place_ok = false; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
in_defer = false; defer_ok = false; defer_block = "a nested form"; in_defer = false; defer_ok = false; defer_block = "a nested form";
owner = "<none>" } owner = "<none>" }
@ -3701,7 +3711,51 @@ let tracked_call loc env name (tr : Shim.track) ret (args : Tast.expr list) =
| [], [] -> call | [], [] -> call
| pre, post -> mk loc ret (Tast.Do (pre @ [ call ] @ post)) | pre, post -> mk loc ret (Tast.Do (pre @ [ call ] @ post))
(* Every expression goes through here, and [check_value] is the one that
knows the forms. What this adds is [refuse_owned_copy], asked of whatever
came back unless the form was checked as the target of a place. *)
let rec check ctx ?want (e : Ast.expr) : Tast.expr = let rec check ctx ?want (e : Ast.expr) : Tast.expr =
let place = ctx.place_ok in
ctx.place_ok <- false;
let r = check_value ctx ?want e in
if not place then refuse_owned_copy ctx r;
r
(* A form checked as the target of a place: indexed, sliced, a field read,
measured, its address taken, or handed to a builtin that works on the
container where it stands. *)
and check_target ctx (e : Ast.expr) =
ctx.place_ok <- true;
check ctx e
(* Decision 81 (2026-09-25). A value that owns storage — a Vec, a Map, or an
array, Option or struct holding one — reached through a [[const T]] or a
(Ptr const T) is not copied out as a value. Its header shares its block
with the original, so a copy that could be grown, freed or handed on as
writable would be the original written through. It is used where it
stands instead: indexed, sliced (to a [[const T]]), its fields read when
they own nothing, or its address taken as a (Ptr const T). Refusing at the
source is the whole rule; there is no tracking of where a copy went. *)
and refuse_owned_copy ctx (r : Tast.expr) =
match const_reached r with
| Some view when owning ctx.env r.Tast.ty ->
let t = Types.to_string r.Tast.ty in
let fix =
match r.Tast.ty with
| (Types.Vec _ | Types.Map _) when not (region_only ctx.env r.Tast.ty) ->
Printf.sprintf "(clone v) copies it into a %s of its own" t
(* TODO.org, "(clone slice)": once clone copies any value that owns
storage, this should say (clone v) too. *)
| _ -> Printf.sprintf "(addr v) gives a (Ptr const %s) to read it through" t
in
Loc.failk "check/const-owned-copy" r.Tast.loc
"this copies a %s out of a %s, which can only be read, and the copy \
would share its storage with the original. Use it where it stands — \
index it, slice it or read its fields — or %s"
t (Types.to_string view) fix
| _ -> ()
and check_value ctx ?want (e : Ast.expr) : Tast.expr =
let loc = e.Ast.loc in let loc = e.Ast.loc in
(* Read the permission this form was given and withdraw it in the same (* Read the permission this form was given and withdraw it in the same
breath, so that nothing reached from here inherits it. The two callers breath, so that nothing reached from here inherits it. The two callers
@ -3928,7 +3982,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
than once — nothing in this milestone builds one — still falls to the than once — nothing in this milestone builds one — still falls to the
ordinary [Ast.Set] arm below, and [indexed] refuses it by name. *) ordinary [Ast.Set] arm below, and [indexed] refuses it by name. *)
| Ast.Set (Ast.Pindex (target, [ idx ]), v) -> | Ast.Set (Ast.Pindex (target, [ idx ]), v) ->
let target = check ctx target in let target = check_target ctx target in
if target.Tast.ty = Types.Dyn then if target.Tast.ty = Types.Dyn then
let i = check ctx ~want:Types.Dyn idx in let i = check ctx ~want:Types.Dyn idx in
let v = check ctx ~want:Types.Dyn v in let v = check ctx ~want:Types.Dyn v in
@ -5010,13 +5064,6 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
| _ -> ()); | _ -> ());
(* Locals are assignable places; parameters are not. *) (* Locals are assignable places; parameters are not. *)
let slot = bind ctx b.Ast.bname v.Tast.ty ~assignable:true in let slot = bind ctx b.Ast.bname v.Tast.ty ~assignable:true in
(* A Vec or Map header copied out of read-only storage still
shares its block with the original, so a push through the copy
is a push through the original. The local remembers where it
came from, for [refuse_const_change]. *)
Option.iter
(fun view -> ctx.const_locals <- (slot, view) :: ctx.const_locals)
(const_reached ~local:(const_local ctx) v);
(slot, v)) (slot, v))
bs bs
in in
@ -6502,7 +6549,7 @@ and fields_named env n : Tast.structure option =
pointer to one. The auto-deref is inserted here as a real node, so no pointer to one. The auto-deref is inserted here as a real node, so no
backend re-derives it. *) backend re-derives it. *)
and struct_target ctx (target : Ast.expr) : Tast.expr * string = and struct_target ctx (target : Ast.expr) : Tast.expr * string =
let t = check ctx target in let t = check_target ctx target in
let has n = fields_named ctx.env n <> None in let has n = fields_named ctx.env n <> None in
match t.Tast.ty with match t.Tast.ty with
| Types.Named n when has n -> t, n | Types.Named n when has n -> t, n
@ -6573,15 +6620,13 @@ and place_const (p : Tast.place) =
const_steps (const_reached t) t.Tast.ty (List.length idx) <> None const_steps (const_reached t) t.Tast.ty (List.length idx) <> None
|| through_string t.Tast.ty (List.length idx) || through_string t.Tast.ty (List.length idx)
and const_local ctx slot = List.assoc_opt slot ctx.const_locals (* Growing, shrinking or freeing a Vec or a Map that is read-only storage.
The backends hand the runtime the container's address, so this is the
(* Growing, shrinking or freeing a Vec or a Map that is read-only storage, or store [check_place] refuses, made through the header instead of through a
a copy of one. The backends hand the runtime the container's address, and [set]. Writing into the Vec's own buffer is not refused: the const is
the header's block is shared with every copy, so this is the store shallow. *)
[check_place] refuses, made through the header instead of through a [set]. and refuse_const_change _ctx loc (target : Tast.expr) =
Writing into the Vec's own buffer is not refused: the const is shallow. *) match const_reached target with
and refuse_const_change ctx loc (target : Tast.expr) =
match const_reached ~local:(const_local ctx) target with
| None -> () | None -> ()
| Some view -> | Some view ->
let t = Types.to_string target.Tast.ty in let t = Types.to_string target.Tast.ty in
@ -6646,10 +6691,10 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
Loc.failk "check/unknown-field" loc ~notes:(declared_note ctx.env sname) Loc.failk "check/unknown-field" loc ~notes:(declared_note ctx.env sname)
"%s has no field %s" sname name "%s has no field %s" sname name
| Some i -> | Some i ->
if store then Option.iter (refuse_const_place loc) (const_reached target); if store then Option.iter (refuse_const_place ctx.env loc) (const_reached target);
Tast.Pfield (target, i), (List.nth s.Tast.fields i).Tast.fty) Tast.Pfield (target, i), (List.nth s.Tast.fields i).Tast.fty)
| Ast.Pindex (target, idx) -> | Ast.Pindex (target, idx) ->
let target = check ctx target in let target = check_target ctx target in
(match target.Tast.ty with (match target.Tast.ty with
(* The same bounds and epoch check the value form gets, through the same (* The same bounds and epoch check the value form gets, through the same
helper: an element of a Vec is a place because a Vec element is helper: an element of a Vec is a place because a Vec element is
@ -6665,7 +6710,7 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
let target = check ctx target in let target = check ctx target in
(match target.Tast.ty with (match target.Tast.ty with
| Types.Ptr (Types.Const, _) as view when store -> | Types.Ptr (Types.Const, _) as view when store ->
refuse_const_place loc view refuse_const_place ctx.env loc view
| Types.Ptr (_, t) -> Tast.Pderef target, t | Types.Ptr (_, t) -> Tast.Pderef target, t
| other -> | other ->
fail loc "deref takes a (Ptr T), found %s" (Types.to_string other)) fail loc "deref takes a (Ptr T), found %s" (Types.to_string other))
@ -6724,7 +6769,7 @@ and index_expr ctx (e : Ast.expr) =
and indexed ?place ?(store = true) ctx (target : Tast.expr) (idx : Ast.expr list) = and indexed ?place ?(store = true) ctx (target : Tast.expr) (idx : Ast.expr list) =
(match place with (match place with
| Some l when store -> | Some l when store ->
Option.iter (refuse_const_place l) Option.iter (refuse_const_place ctx.env l)
(const_steps (const_reached target) target.Tast.ty (List.length idx)) (const_steps (const_reached target) target.Tast.ty (List.length idx))
| _ -> ()); | _ -> ());
let rec go ty = function let rec go ty = function
@ -8087,7 +8132,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 2 args; arity ctx loc name 2 args;
(match args with (match args with
| [ target; x ] -> | [ target; x ] ->
let target = check ctx target in let target = check_target ctx target in
refuse_const_change ctx loc target; refuse_const_change ctx loc target;
(* A push into a dyn container is a call and nothing else: no allocation (* A push into a dyn container is a call and nothing else: no allocation
guard, no restart, no region check. The dyn runtime owns the storage guard, no restart, no region check. The dyn runtime owns the storage
@ -8128,7 +8173,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 2 args; arity ctx loc name 2 args;
(match args with (match args with
| [ target; n ] -> | [ target; n ] ->
let target = check ctx target in let target = check_target ctx target in
refuse_const_change ctx loc target; refuse_const_change ctx loc target;
let n = check ctx ~want:index_ty n in let n = check ctx ~want:index_ty n in
let n64 = let n64 =
@ -8172,7 +8217,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
is a thing you write, and writing it twice is yours to not do. *) is a thing you write, and writing it twice is yours to not do. *)
| "free" -> | "free" ->
arity ctx loc name 1 args; arity ctx loc name 1 args;
let target = check ctx (List.hd args) in let target = check_target ctx (List.hd args) in
refuse_const_change ctx loc target; refuse_const_change ctx loc target;
(* A container of owning elements is refused here, and a reader will (* A container of owning elements is refused here, and a reader will
assume the opposite — that [free] recurses — so this says why it does assume the opposite — that [free] recurses — so this says why it does
@ -8227,7 +8272,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
(* Checked once, then dispatched on what it turned out to be: checking (* Checked once, then dispatched on what it turned out to be: checking
it inside a guard as well would allocate the target's slots twice and it inside a guard as well would allocate the target's slots twice and
evaluate whatever it was written as twice. *) evaluate whatever it was written as twice. *)
let target = check ctx target in let target = check_target ctx target in
let a = allocator_arg ctx loc rest in let a = allocator_arg ctx loc rest in
(match target.Tast.ty with (match target.Tast.ty with
(* The refusal that did *not* come down with the type-level ones, and (* The refusal that did *not* come down with the type-level ones, and
@ -8342,7 +8387,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 3 args; arity ctx loc name 3 args;
(match args with (match args with
| [ target; k; v ] -> | [ target; k; v ] ->
let target = check ctx target in let target = check_target ctx target in
refuse_const_change ctx loc target; refuse_const_change ctx loc target;
(* A put into a dyn map is a call and nothing else, the way a push into (* A put into a dyn map is a call and nothing else, the way a push into
a dyn vec is: the runtime owns the storage, so there is no guard, no a dyn vec is: the runtime owns the storage, so there is no guard, no
@ -8393,7 +8438,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 2 args; arity ctx loc name 2 args;
(match args with (match args with
| [ target; k ] -> | [ target; k ] ->
let target = check ctx target in let target = check_target ctx target in
(* A dyn map's absence is nil, not None: the typed map can promise an (* A dyn map's absence is nil, not None: the typed map can promise an
(Option V) because V was written down, and a dyn map has nothing to (Option V) because V was written down, and a dyn map has nothing to
write. nil is an ordinary dyn value the caller compares against — write. nil is an ordinary dyn value the caller compares against —
@ -8468,7 +8513,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 2 args; arity ctx loc name 2 args;
(match args with (match args with
| [ target; k ] -> | [ target; k ] ->
let target = check ctx target in let target = check_target ctx target in
refuse_const_change ctx loc target; refuse_const_change ctx loc target;
let kt, vt = map_kv loc "map-remove" target.Tast.ty in let kt, vt = map_kv loc "map-remove" target.Tast.ty in
let k = check ctx ~want:kt k in let k = check ctx ~want:kt k in
@ -8506,7 +8551,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 4 args; arity ctx loc name 4 args;
(match args with (match args with
| [ target; cur; k; v ] -> | [ target; cur; k; v ] ->
let target = check ctx target in let target = check_target ctx target in
let kt, vt = map_kv loc "map-next" target.Tast.ty in let kt, vt = map_kv loc "map-next" target.Tast.ty in
let cur = check ctx ~want:(Types.Ptr (Types.Mut, (Types.Int Types.I64))) cur in let cur = check ctx ~want:(Types.Ptr (Types.Mut, (Types.Int Types.I64))) cur in
let k = check ctx ~want:(Types.Ptr (Types.Mut, kt)) k in let k = check ctx ~want:(Types.Ptr (Types.Mut, kt)) k in
@ -8530,7 +8575,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 2 args; arity ctx loc name 2 args;
(match args with (match args with
| [ target; k ] -> | [ target; k ] ->
let target = check ctx target in let target = check_target ctx target in
(* The dyn map's question, one word with the typed one. It exists on (* The dyn map's question, one word with the typed one. It exists on
the dyn side because absence there is nil, and a map can also store the dyn side because absence there is nil, and a map can also store
nil under a key — (get m k) answering nil cannot tell the two nil under a key — (get m k) answering nil cannot tell the two
@ -8849,7 +8894,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
| "length" -> | "length" ->
arity ctx loc name 1 args; arity ctx loc name 1 args;
let target = List.hd args in let target = List.hd args in
let a = check ctx target in let a = check_target ctx target in
(match a.Tast.ty with (match a.Tast.ty with
| Types.Array _ | Types.Slice _ | Types.String -> | Types.Array _ | Types.Slice _ | Types.String ->
prim Tast.Len index_ty [ a ] prim Tast.Len index_ty [ a ]
@ -8876,7 +8921,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
| "at" -> | "at" ->
(match args with (match args with
| target :: idx when idx <> [] -> | target :: idx when idx <> [] ->
let target = check ctx target in let target = check_target ctx target in
(match target.Tast.ty with (match target.Tast.ty with
| Types.Vec _ -> | Types.Vec _ ->
let p, elem = vec_at ctx loc target idx in let p, elem = vec_at ctx loc target idx in
@ -8923,7 +8968,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
"slice is (slice a), (slice a lo) or (slice a lo hi) — given %d \ "slice is (slice a), (slice a lo) or (slice a lo hi) — given %d \
arguments" (List.length args) arguments" (List.length args)
| target :: bounds -> | target :: bounds ->
let target = check ctx target in let target = check_target ctx target in
let ty = target.Tast.ty in let ty = target.Tast.ty in
match ty with match ty with
(* A Vec leaves here: everything below is written around a length the (* A Vec leaves here: everything below is written around a length the
@ -10004,8 +10049,19 @@ and generic_call ctx ~want loc name vars pats pret args =
| Ast.Int _ | Ast.UInt _ | Ast.Float _ | Ast.Byte _ -> true | Ast.Int _ | Ast.UInt _ | Ast.Float _ | Ast.Byte _ -> true
| _ -> false | _ -> false
in in
(* A bare [$t] an earlier argument bound to a slice or a pointer:
this argument may differ from it only in const, and the two meet
at the read-only one ([Types.const_join]), whichever came first.
So it is checked on its own terms rather than against the
binding. *)
let bound_view =
match pat, p with
| Types.Var v, (Types.Slice _ | Types.Ptr _)
when not (generic_ty p || bound_exactly v) -> Some v
| _ -> None
in
let a = let a =
if generic_ty p then check ctx a if generic_ty p || bound_view <> None then check ctx a
else if bound_scalar <> None && not untyped_literal then else if bound_scalar <> None && not untyped_literal then
(* On its own terms first. A form that has no type without a want (* On its own terms first. A form that has no type without a want
— [(zeroed)] is the one that matters — refuses here and is — [(zeroed)] is the one that matters — refuses here and is
@ -10038,6 +10094,11 @@ and generic_call ctx ~want loc name vars pats pret args =
bound to i64 is an ordinary mismatch and gets the ordinary bound to i64 is an ordinary mismatch and gets the ordinary
refusal below. *) refusal below. *)
let handled = let handled =
match bound_view, Types.const_join p a.Tast.ty with
| Some v, Some j ->
subst := (v, j) :: List.remove_assoc v !subst;
true
| _ ->
match bound_scalar with match bound_scalar with
| Some v | Some v
when (not (Types.equal p a.Tast.ty)) when (not (Types.equal p a.Tast.ty))
@ -10076,7 +10137,7 @@ and generic_call ctx ~want loc name vars pats pret args =
" — %s takes a slice it may write through, and a %s can \ " — %s takes a slice it may write through, and a %s can \
only be read%s" only be read%s"
name (Types.to_string a.Tast.ty) name (Types.to_string a.Tast.ty)
(match const_copy e with (match const_copy ctx.env e with
| Some c -> | Some c ->
Printf.sprintf ". %s copies v into one that can be written" c Printf.sprintf ". %s copies v into one that can be written" c
| None -> "") | None -> "")
@ -10126,6 +10187,8 @@ and generic_call ctx ~want loc name vars pats pret args =
&& Types.is_numeric a.Tast.ty && Types.is_numeric a.Tast.ty
&& Types.widens_to ~from:a.Tast.ty ~into:f -> && Types.widens_to ~from:a.Tast.ty ~into:f ->
widen a.Tast.loc f a widen a.Tast.loc f a
| Some f when Types.const_widens ~from:a.Tast.ty ~into:f ->
{ a with Tast.ty = f }
| _ -> a) | _ -> a)
(* And the other widening, for the same reason and at the same (* And the other widening, for the same reason and at the same
moment: a [CFn] argument against an [(Fn [$t] $t)] parameter. moment: a [CFn] argument against an [(Fn [$t] $t)] parameter.
@ -10436,7 +10499,7 @@ and trial ctx f =
resource failure into a wrong answer. *) resource failure into a wrong answer. *)
let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope; let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
defers; defer_slot; defer_ok; defer_block; outer = _; defers; defer_slot; defer_ok; defer_block; outer = _;
outer_what; caught; const_locals; envslot; parent = _; outer_what; caught; place_ok; envslot; parent = _;
in_frames; loops; tail; in_defer; in_frames; loops; tail; in_defer;
owner = _ } = ctx in owner = _ } = ctx in
match f () with match f () with
@ -10447,7 +10510,7 @@ and trial ctx f =
ctx.defers <- defers; ctx.defer_slot <- defer_slot; ctx.defers <- defers; ctx.defer_slot <- defer_slot;
ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block; ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block;
ctx.outer_what <- outer_what; ctx.in_frames <- in_frames; ctx.outer_what <- outer_what; ctx.in_frames <- in_frames;
ctx.caught <- caught; ctx.const_locals <- const_locals; ctx.envslot <- envslot; ctx.caught <- caught; ctx.place_ok <- place_ok; ctx.envslot <- envslot;
ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer; ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer;
Error d Error d

17
lib/types.ml
View File

@ -349,20 +349,21 @@ let rec const_widens ~(from : t) ~(into : t) =
equal a b || const_widens ~from:a ~into:b equal a b || const_widens ~from:a ~into:b
| _ -> false | _ -> false
(* A function of one signature standing where another is wanted, when the (* The one type two branches of an [if], or two arguments at one type
two differ only in const. A parameter may be more permissive than asked — variable, meet at when they differ only in const: the read-only one,
a function that takes a [[const T]] only reads what it is handed, so a whichever came first. *)
caller handing it a [[T]] loses nothing — and a result may be less so: a
[[T]] returned where a [[const T]] is wanted is [const_widens]'s case. The
two words are the same either way, so [Check.expect] only retypes. *)
(* The one type two branches of an [if] meet at when they differ only in
const: the read-only one, whichever branch it came from. *)
let const_join a b = let const_join a b =
if equal a b then Some a if equal a b then Some a
else if const_widens ~from:a ~into:b then Some b else if const_widens ~from:a ~into:b then Some b
else if const_widens ~from:b ~into:a then Some a else if const_widens ~from:b ~into:a then Some a
else None else None
(* A function of one signature standing where another is wanted, when the
two differ only in const. A parameter may be more permissive than asked —
a function that takes a [[const T]] only reads what it is handed, so a
caller handing it a [[T]] loses nothing — and a result may be less so: a
[[T]] returned where a [[const T]] is wanted is [const_widens]'s case. The
two words are the same either way, so [Check.expect] only retypes. *)
let fn_accepts ~(from : t list * t) ~(into : t list * t) = let fn_accepts ~(from : t list * t) ~(into : t list * t) =
let ps', r' = from and ps, r = into in let ps', r' = from and ps, r = into in
List.length ps = List.length ps' List.length ps = List.length ps'

39
test/programs/const-owned.flan Normal file
View File

@ -0,0 +1,39 @@
;;;; A Vec reached through a [const (Vec T)] or a (Ptr const (Vec T)) is used
;;;; where it stands — indexed, measured, sliced, its address taken — and never
;;;; copied out as a value; (clone v) is the copy. The refusals are in
;;;; test_flan.ml; this is the half that compiles, on both backends.
(defstruct Bag [items (Vec i32) n i32])
(defn total [vs [const (Vec i32)]] i32
(let [t 0]
(dotimes [i (length vs)]
(dotimes [j (length (at vs i))]
(set t (+ t (at (at vs i) j)))))
t))
(defn first-len [p (Ptr const (Vec i32))] i32 (length (deref p)))
(defn bag-n [bs [const Bag]] i32 (+ (.n (at bs 0)) (length (.items (at bs 0)))))
(defn pick [c bool a $t b $t] $t (if c a b))
(defn main [] i32
(let [a (vec-new i32)
b (vec-new i32)]
(push a 1) (push a 2)
(push b 30)
(let [vs [a b]
cv (the-const (slice vs))
w (clone (at cv 0))
bags [(Bag {.items b .n 4})]]
(push w 99)
;; The shallow rule: the Vec's own buffer is writable through the view.
(set (at (at cv 1) 0) 31)
(println (total cv) (length w) (length (at cv 0)))
(println (first-len (addr (at cv 0))) (bag-n (slice bags)))
(println (length (pick true (bytes-view "abc") (bytes "de")))
(length (pick false (bytes "de") (bytes-view "abc"))))))
0)
(defn the-const [s [const (Vec i32)]] [const (Vec i32)] s)

6
test/test_acceptance.ml
View File

@ -879,6 +879,12 @@ let () =
const_slice_out; const_slice_out;
outputs ~x86:true "const slices, --x86" "programs/const-slice.flan" outputs ~x86:true "const slices, --x86" "programs/const-slice.flan"
const_slice_out; const_slice_out;
let const_owned_out = "34 3 2\n2 5\n3 3\n" in
outputs "const owned" "programs/const-owned.flan" const_owned_out;
outputs ~opt:"-O0" "const owned, -O0" "programs/const-owned.flan"
const_owned_out;
outputs ~x86:true "const owned, --x86" "programs/const-owned.flan"
const_owned_out;
(* (string b). The conversion emits nothing — String and Slice _ are the (* (string b). The conversion emits nothing — String and Slice _ are the
same %slice — so the rows are about length and ownership rather than same %slice — so the rows are about length and ownership rather than
arithmetic: a number round-tripped, an empty slice, sub-views whose arithmetic: a number round-tripped, an empty slice, sub-views whose

90
test/test_flan.ml
View File

@ -2361,21 +2361,81 @@ let () =
"(defn f [p (Ptr const $t)] $t (deref p)) (defn g [q (Ptr i32)] i32 (f q))"; "(defn f [p (Ptr const $t)] $t (deref p)) (defn g [q (Ptr i32)] i32 (f q))";
accepts "vec-new reads (Ptr const u8) as a type" accepts "vec-new reads (Ptr const u8) as a type"
"(defn f [] i32 (let [v (vec-new (Ptr const u8))] (length v)))"; "(defn f [] i32 (let [v (vec-new (Ptr const u8))] (length v)))";
(* A Vec header copied out of read-only storage shares its block, so the (* Decision 81: a value that owns storage, reached through read-only
copy is as read-only as the original, through any number of lets. *) storage, is used where it stands and never copied out. Every route a
rejects_check "push through a let-bound copy of a const element" copy could take is refused at the copy. *)
"(defn f [cs [const (Vec i32)]] () (let [v (at cs 0)] (push v 1)))" let copied = "this copies a (Vec i32) out of a [const (Vec i32)]" in
~needle:"reached through a [const (Vec i32)]"; List.iter
rejects_check "reserve through a copy of a copy" (fun (name, src) -> rejects_check ("no copy out: " ^ name) src ~needle:copied)
"(defn f [cs [const (Vec i32)]] () (let [v (at cs 0) w v] (reserve w 9)))" [ "let", "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0)] (push v 1)))";
~needle:"reached through a [const (Vec i32)]"; "loop binding",
rejects_check "put through a let-bound copy of a const element" "(defn f [cs [const (Vec i32)]] () (loop [v (at cs 0)] (push v 1)))";
"(defn f [cs [const (Map string i32)]] () (let [m (at cs 0)] (put m \"a\" 1)))" "if value",
~needle:"reached through a [const (Map string i32)]"; "(defn f [c bool cs [const (Vec i32)]] () \
rejects_check "push into a field of a let-bound copy" (let [v (if c (at cs 0) (at cs 1))] (push v 1)))";
"(defstruct P [v (Vec i32)]) \ "do value",
(defn f [cs [const P]] () (let [p (at cs 0)] (push (.v p) 1)))" "(defn f [cs [const (Vec i32)]] () (let [v (do (at cs 0))] (push v 1)))";
~needle:"take the P it lives in as a [P]"; "set into a local",
"(defn f [cs [const (Vec i32)]] () \
(let [v (vec-new i32)] (set v (at cs 0)) (push v 1)))";
"match binding",
"(defn f [cs [const (Vec i32)]] i32 \
(match (Some (at cs 0)) (Some v) (do (push v 1) 0) None 0))";
"array destructure",
"(defn f [cs [const (Vec i32)]] () \
(let [[a b] [(at cs 0) (at cs 1)]] (push a 1)))";
"closure capture",
"(defn app [g (Fn [] ())] () (g)) (defn f [cs [const (Vec i32)]] () \
(let [v (at cs 0)] (app (fn [] (push v 1)))))";
"passed by value",
"(defn pusher [v (Vec i32)] () (push v 1)) \
(defn f [cs [const (Vec i32)]] () (pusher (at cs 0)))";
"returned by value",
"(defn g [cs [const (Vec i32)]] (Vec i32) (at cs 0))";
"through a generic",
"(defn id [x $t] $t x) (defn f [cs [const (Vec i32)]] () (push (id (at cs 0)) 1))" ];
rejects_check "no copy out through a const pointer"
"(defn f [p (Ptr const (Vec i32))] () (let [v (deref p)] (push v 1)))"
~needle:"this copies a (Vec i32) out of a (Ptr const (Vec i32))";
rejects_check "and the copy that is allowed is named"
"(defn f [cs [const (Vec i32)]] (Vec i32) (at cs 0))"
~needle:"(clone v) copies it into a (Vec i32) of its own";
rejects_check "a struct holding a Vec is not copied out either"
"(defstruct P [v (Vec i32)]) (defn f [cs [const P]] P (at cs 0))"
~needle:"(addr v) gives a (Ptr const P) to read it through";
rejects_check "nor an array of them"
"(defn f [cs [const [2 (Vec i32)]]] [2 (Vec i32)] (at cs 0))"
~needle:"this copies a [2 (Vec i32)] out of a [const [2 (Vec i32)]]";
rejects_check "nor an Option of one"
"(defn f [cs [const (Option (Vec i32))]] (Option (Vec i32)) (at cs 0))"
~needle:"this copies a (Option (Vec i32)) out";
rejects_check "nor a field that owns storage"
"(defstruct P [v (Vec i32)]) (defn f [cs [const P]] (Vec i32) (.v (at cs 0)))"
~needle:"this copies a (Vec i32) out of a [const P]";
accepts "used where it stands"
"(defstruct P [v (Vec i32) n i32]) \
(defn f [cs [const (Vec i32)] ps [const P] p (Ptr const (Vec i32))] i32 \
(+ (at (at cs 0) 1) (length (at cs 0)) (length (slice (at cs 0))) \
(.n (at ps 0)) (length (.v (at ps 0))) (length (deref p)) \
(length (deref (addr (at cs 0)))) (length (clone (at cs 0)))))";
accepts "a copy of a scalar element is still a copy"
"(defn f [cs [const i32]] i32 (let [x (at cs 0)] (set x 5) x))";
(* The header copy is suggested only for elements that own nothing. *)
rejects_check "no header copy suggested for an array of Vecs"
"(defn f [cs [const [2 (Vec i32)]]] () (set (at cs 0) (at cs 1)))"
~needle:"take it as a [[2 (Vec i32)]] instead";
rejects_check "nor for an Option of a Vec"
"(defn f [cs [const (Option (Vec i32))]] () (set (at cs 0) None))"
~needle:"take it as a [(Option (Vec i32))] instead";
(* Two arguments at one type variable meet at const, either order. *)
accepts "a generic's arguments join at const"
"(defn pick [c bool a $t b $t] $t (if c a b)) \
(defn f [c bool cs [const u8] ms [u8]] i32 (+ (length (pick c ms cs)) \
(length (pick c cs ms))))";
rejects_check "and the join is read-only"
"(defn pick [c bool a $t b $t] $t (if c a b)) \
(defn f [c bool cs [const u8] ms [u8]] () (set (at (pick c ms cs) 0) 1))"
~needle:"this writes through a [const u8]";
rejects_check "no copy of Vec headers is suggested" rejects_check "no copy of Vec headers is suggested"
"(defn f [cs [const (Vec i32)]] () (set (at cs 0) (vec-new i32)))" "(defn f [cs [const (Vec i32)]] () (set (at cs 0) (vec-new i32)))"
~needle:"take it as a [(Vec i32)] instead"; ~needle:"take it as a [(Vec i32)] instead";