An array reached through read-only storage slices to a [const T], a Vec or Map copied out of one stays read-only through lets, and an if's const and writable branches meet at const in either order

This commit is contained in:
Joseph Ferano 2026-09-25 13:08:29 +07:00
parent 37e577d5e1
commit 1e5be63a1a
4 changed files with 157 additions and 51 deletions

View File

@ -1043,7 +1043,7 @@ the only two under which a mark and a sweep run at all. `dev_segv` sits beside t
program that faults cannot be compared against an unsanitized run — that build's handler parks in the break loop, and program that faults cannot be compared against an unsanitized run — that build's handler parks in the break loop, and
the two builds are *supposed* to differ, since `flan_dev_crash_enable` checks a weak `__asan_init` and declines to the two builds are *supposed* to differ, since `flan_dev_crash_enable` checks a weak `__asan_init` and declines to
install the handler when ASan is in the process. So the case asserts ASan's report and the absence of the handler's install the handler when ASan is in the process. So the case asserts ASan's report and the absence of the handler's
line, built at `-O0` because at `-O2` the write through a pointer to a literal's bytes does not fault at all. That yield had line, built at `-O0` because at `-O2` a store through a zeroed `(Ptr u8)` is undefined and need not fault. That yield had
never run in any build anywhere: it was behind a link that did not happen. Twenty-six seconds of the alias's 2m30 warm. never run in any build anywhere: it was behind a link that did not happen. Twenty-six seconds of the alias's 2m30 warm.
What it still does not reach is a program driven by a real daemon under ASan: `flan dev` builds its host through its own What it still does not reach is a program driven by a real daemon under ASan: `flan dev` builds its host through its own
path and has no `--sanitize` to pass it. path and has no `--sanitize` to pass it.

View File

@ -556,6 +556,8 @@ 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. *)
mutable const_locals : (int * Types.t) list;
(* 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
@ -2211,11 +2213,12 @@ 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 (e : Tast.expr) = let rec const_reached ?(local = fun (_ : int) -> None) (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 target) target.Tast.ty (List.length idx) const_steps (const_reached ~local target) target.Tast.ty (List.length idx)
| Tast.Field (target, _) -> const_reached target | Tast.Field (target, _) -> const_reached ~local 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
@ -2230,6 +2233,15 @@ and const_steps ro (ty : Types.t) n =
| Types.Array (_, t) -> const_steps ro t (n - 1) | Types.Array (_, t) -> const_steps ro t (n - 1)
| _ -> ro | _ -> ro
(* A copy of a read-only slice's elements that can be written, spelled so it
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
copy would share the original's block. *)
let const_copy (e : Types.t) =
match e with
| Types.Vec _ | Types.Map _ | Types.Named _ -> None
| _ -> 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 loc (view : Types.t) =
match view with match view with
@ -2248,30 +2260,19 @@ let refuse_const_place loc (view : Types.t) =
let elem = match view with Types.Slice (_, t) -> t | t -> t in let elem = match view with Types.Slice (_, t) -> t | t -> t in
Loc.failk "check/store-through-const" loc Loc.failk "check/store-through-const" loc
"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. Write into a slice that can be written: \ value and not a place. %s"
(slice (into v (vec-new %s))) copies v's elements into one" (Types.to_string view)
(Types.to_string view) (Types.to_string elem) (match const_copy elem with
| Some c ->
(* The runtime entry points that change a Vec or a Map, which the backends Printf.sprintf
hand the container's address. An element of a [[const (Vec T)]], or a field "Write into a slice that can be written: %s copies v's elements \
reached through one, is storage the view may not write, so growing, into one" c
shrinking or freeing it there is the same store [check_place] refuses — | None ->
made through the header instead of through a [set]. Writing into the Printf.sprintf "Where it has to be written, take it as a [%s] instead"
Vec's own buffer is not refused: the const is shallow, and the buffer is (Types.to_string elem))
not the slice's storage. *)
let changes_container = function
| "flan_vec_push" | "flan_vec_reserve" | "flan_vec_free"
| "flan_map_put" | "flan_map_remove" | "flan_map_reserve" | "flan_map_free" ->
true
| _ -> false
(* A runtime call, with the result type spelled at the site. *) (* A runtime call, with the result type spelled at the site. *)
let rt loc ty sym args = let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args))
(if changes_container sym then
match args with
| target :: _ -> Option.iter (refuse_const_place loc) (const_reached target)
| [] -> ());
mk loc ty (Tast.Prim (Tast.Rt sym, args))
(* ── The allocation registry's note ────────────────────────────────── (* ── The allocation registry's note ──────────────────────────────────
@ -3116,14 +3117,19 @@ let const_note ~(want : Types.t) ~(got : Types.t) =
when Types.equal e e' -> when Types.equal e e' ->
let copy = let copy =
match e with match e with
| Types.Int Types.U8 -> "(bytes (string v))" | Types.Int Types.U8 -> Some "(bytes (string v))"
| _ -> Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e) | _ -> const_copy 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 \
through. %s copies v into a %s of its own; where nothing writes \ through. %sWhere nothing writes through it, the %s can be declared %s \
through it, the %s can be declared %s instead" instead"
(Types.to_string got) (Types.to_string want) copy (Types.to_string want) (Types.to_string got) (Types.to_string want)
(match copy with
| Some c ->
Printf.sprintf "%s copies v into a %s of its own. " c
(Types.to_string want)
| None -> "")
(Types.to_string want) (Types.to_string got) (Types.to_string want) (Types.to_string got)
| Types.Ptr (Types.Mut, e), Types.Ptr (Types.Const, e') | Types.Ptr (Types.Mut, e), Types.Ptr (Types.Const, e')
when Types.equal e e' -> when Types.equal e e' ->
@ -3271,7 +3277,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 = []; envslot = None; parent = None; in_frames = None; loops = []; tail = false; defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; const_locals = []; 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>" }
@ -5019,6 +5025,13 @@ 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
@ -5478,10 +5491,18 @@ and check_if ctx ?(tail = false) ?want loc c t e =
let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in
(* With no expectation the then-branch supplies one for the else-branch, (* With no expectation the then-branch supplies one for the else-branch,
unless it diverges, in which case the else-branch decides. *) unless it diverges, in which case the else-branch decides. *)
(* A slice or a pointer from the then-branch is not the else-branch's
want: the two may differ only in const, and they meet at the
read-only one whichever side it is on — [Types.const_join]. *)
let free_join =
want = None
&& (match t.Tast.ty with Types.Slice _ | Types.Ptr _ -> true | _ -> false)
in
let ewant = let ewant =
match want with match want with
| Some _ -> want | Some _ -> want
| None -> if t.Tast.ty = Types.Never then None else Some t.Tast.ty | None ->
if t.Tast.ty = Types.Never || free_join then None else Some t.Tast.ty
in in
(* [(and a b c)] is [(let [t a] (if t (let [u b] (if u c u)) t))], so the (* [(and a b c)] is [(let [t a] (if t (let [u b] (if u c u)) t))], so the
*last* operand of an [and] is the then arm and the sentinel that carries *last* operand of an [and] is the then arm and the sentinel that carries
@ -5514,6 +5535,13 @@ and check_if ctx ?(tail = false) ?want loc c t e =
one type — this operand is %s, and false is a bool" one type — this operand is %s, and false is a bool"
(Types.to_string t.Tast.ty) (Types.to_string t.Tast.ty)
in in
let t, e =
match free_join, Types.const_join t.Tast.ty e.Tast.ty with
| true, Some j when e.Tast.ty <> Types.Never ->
expect ctx t.Tast.loc ~want:(Some j) t,
expect ctx e.Tast.loc ~want:(Some j) e
| _ -> t, e
in
let ty = let ty =
if t.Tast.ty = Types.Never then e.Tast.ty if t.Tast.ty = Types.Never then e.Tast.ty
else if e.Tast.ty = Types.Never then t.Tast.ty else if e.Tast.ty = Types.Never then t.Tast.ty
@ -6540,12 +6568,6 @@ and refuse_string_place loc (ty : Types.t) =
"a string is read-only, so (at s i) is a value and not a place. Copy \ "a string is read-only, so (at s i) is a value and not a place. Copy \
the bytes into a buffer you own and write that" the bytes into a buffer you own and write that"
(* [store] is false for [addr] alone. A (Ptr T) is the C boundary, where the
program is already trusted — [slice-from-ptr] and [declare-c] take its word
— and a [[const u8]] handed to a C function that takes a [const T *] has no
other way across: [load-image-from-memory] over an [embed] is the case. So
the address of a read-only element may be taken, and it is a store that is
refused. *)
(* Whether a checked place is read-only storage: reached through a (* Whether a checked place is read-only storage: reached through a
[[const T]] or a (Ptr const T), or a byte of a string. Its address is a [[const T]] or a (Ptr const T), or a byte of a string. Its address is a
(Ptr const T). *) (Ptr const T). *)
@ -6566,6 +6588,28 @@ 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, or
a copy of one. The backends hand the runtime the container's address, and
the header's block is shared with every copy, so this is the store
[check_place] refuses, made through the header instead of through a [set].
Writing into the Vec's own buffer is not refused: the const is shallow. *)
and refuse_const_change ctx loc (target : Tast.expr) =
match const_reached ~local:(const_local ctx) target with
| None -> ()
| Some view ->
let t = Types.to_string target.Tast.ty in
let holder =
match view with Types.Slice (_, e) | Types.Ptr (_, e) -> e | t -> t
in
Loc.failk "check/store-through-const" loc
"this changes a %s reached through a %s, which can only be read. Where \
it has to change, take the %s it lives in as a [%s] or a (Ptr %s) \
instead"
t (Types.to_string view) (Types.to_string holder)
(Types.to_string holder) (Types.to_string holder)
and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t = and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
match p with match p with
| Ast.Pvar name -> | Ast.Pvar name ->
@ -8059,6 +8103,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
(match args with (match args with
| [ target; x ] -> | [ target; x ] ->
let target = check ctx target in let target = check ctx target in
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
and answers a failure to grow it on its own terms — the guard and the and answers a failure to grow it on its own terms — the guard and the
@ -8099,6 +8144,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
(match args with (match args with
| [ target; n ] -> | [ target; n ] ->
let target = check ctx target in let target = check ctx target in
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 =
mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Cast (Types.Int Types.I64), [ n ])) mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Cast (Types.Int Types.I64), [ n ]))
@ -8142,6 +8188,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
| "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 ctx (List.hd args) in
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
not and what does. not and what does.
@ -8311,6 +8358,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
(match args with (match args with
| [ target; k; v ] -> | [ target; k; v ] ->
let target = check ctx target in let target = check ctx target in
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
restart and no region check. An equal key's value is replaced. *) restart and no region check. An equal key's value is replaced. *)
@ -8436,6 +8484,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
(match args with (match args with
| [ target; k ] -> | [ target; k ] ->
let target = check ctx target in let target = check ctx target in
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
(* Deferred exactly as [get] is, and with [None] for the same reason: (* Deferred exactly as [get] is, and with [None] for the same reason:
@ -8901,6 +8950,10 @@ and named_call ?(qualified = false) ctx ~want loc name args =
calling it a byte slice would hand out a writable-looking view of calling it a byte slice would hand out a writable-looking view of
storage the program does not own. *) storage the program does not own. *)
let result = match ty with let result = match ty with
(* An array reached through a [[const T]] or a (Ptr const T) is
read-only storage, and so is a view of it. *)
| Types.Array (_, t) when const_reached target <> None ->
Types.Slice (Types.Const, t)
| Types.Array (_, t) -> Types.Slice (Types.Mut, t) | Types.Array (_, t) -> Types.Slice (Types.Mut, t)
| Types.Slice (m, t) -> Types.Slice (m, t) | Types.Slice (m, t) -> Types.Slice (m, t)
| Types.String -> Types.String | Types.String -> Types.String
@ -10036,9 +10089,12 @@ and generic_call ctx ~want loc name vars pats pret args =
| Types.Slice (Types.Mut, _), Types.Slice (Types.Const, e) -> | Types.Slice (Types.Mut, _), Types.Slice (Types.Const, e) ->
Printf.sprintf Printf.sprintf
" — %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. (slice (into v (vec-new %s))) copies v into \ only be read%s"
one that can be written" name (Types.to_string a.Tast.ty)
name (Types.to_string a.Tast.ty) (Types.to_string e) (match const_copy e with
| Some c ->
Printf.sprintf ". %s copies v into one that can be written" c
| None -> "")
| _ -> ""); | _ -> "");
a) a)
pats args pats args
@ -10395,7 +10451,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; envslot; parent = _; outer_what; caught; const_locals; 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
@ -10406,7 +10462,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.envslot <- envslot; ctx.caught <- caught; ctx.const_locals <- const_locals; 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

View File

@ -355,6 +355,14 @@ let rec const_widens ~(from : t) ~(into : t) =
caller handing it a [[T]] loses nothing — and a result may be less 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 [[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. *) 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 =
if equal a b then Some a
else if const_widens ~from:a ~into:b then Some b
else if const_widens ~from:b ~into:a then Some a
else None
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'

View File

@ -2291,22 +2291,22 @@ let () =
~needle:"expected [[const u8]], found [[u8]]"; ~needle:"expected [[const u8]], found [[u8]]";
rejects_check "push through a const slice of Vecs" rejects_check "push through a const slice of Vecs"
"(defn f [s [const (Vec i32)]] () (push (at s 0) 5))" "(defn f [s [const (Vec i32)]] () (push (at s 0) 5))"
~needle:"this writes through a [const (Vec i32)]"; ~needle:"reached through a [const (Vec i32)]";
rejects_check "put through a const slice of maps" rejects_check "put through a const slice of maps"
"(defn f [s [const (Map string i32)]] () (put (at s 0) \"a\" 5))" "(defn f [s [const (Map string i32)]] () (put (at s 0) \"a\" 5))"
~needle:"this writes through a [const (Map string i32)]"; ~needle:"reached through a [const (Map string i32)]";
rejects_check "map-remove through a const slice of maps" rejects_check "map-remove through a const slice of maps"
"(defn f [s [const (Map string i32)]] bool (map-remove (at s 0) \"a\"))" "(defn f [s [const (Map string i32)]] bool (map-remove (at s 0) \"a\"))"
~needle:"this writes through a [const (Map string i32)]"; ~needle:"reached through a [const (Map string i32)]";
rejects_check "reserve through a const slice of Vecs" rejects_check "reserve through a const slice of Vecs"
"(defn f [s [const (Vec i32)]] () (reserve (at s 0) 10))" "(defn f [s [const (Vec i32)]] () (reserve (at s 0) 10))"
~needle:"this writes through a [const (Vec i32)]"; ~needle:"reached through a [const (Vec i32)]";
rejects_check "free through a const slice of Vecs" rejects_check "free through a const slice of Vecs"
"(defn f [s [const (Vec i32)]] () (free (at s 0)))" "(defn f [s [const (Vec i32)]] () (free (at s 0)))"
~needle:"this writes through a [const (Vec i32)]"; ~needle:"reached through a [const (Vec i32)]";
rejects_check "push into a field reached through a const slice" rejects_check "push into a field reached through a const slice"
"(defstruct P [v (Vec i32)]) (defn f [s [const P]] () (push (.v (at s 0)) 1))" "(defstruct P [v (Vec i32)]) (defn f [s [const P]] () (push (.v (at s 0)) 1))"
~needle:"this writes through a [const P]"; ~needle:"reached through a [const P]";
accepts "a Vec's own buffer is not the const slice's storage" accepts "a Vec's own buffer is not the const slice's storage"
"(defn f [s [const (Vec i32)]] () (set (at (at s 0) 0) 5))"; "(defn f [s [const (Vec i32)]] () (set (at (at s 0) 0) 5))";
accepts "a reading function where a writing one is wanted" accepts "a reading function where a writing one is wanted"
@ -2341,7 +2341,7 @@ let () =
~needle:"this writes through a (Ptr const P)"; ~needle:"this writes through a (Ptr const P)";
rejects_check "a push through a const pointer" rejects_check "a push through a const pointer"
"(defn f [p (Ptr const (Vec i32))] () (push (deref p) 1))" "(defn f [p (Ptr const (Vec i32))] () (push (deref p) 1))"
~needle:"behind a (Ptr const (Vec i32))"; ~needle:"this changes a (Vec i32) reached through a (Ptr const (Vec i32))";
rejects_check "a const pointer is not a writable one" rejects_check "a const pointer is not a writable one"
"(defn g [p (Ptr u8)] i32 0) (defn f [v [const u8]] i32 (g (addr (at v 0))))" "(defn g [p (Ptr u8)] i32 0) (defn f [v [const u8]] i32 (g (addr (at v 0))))"
~needle:"expected (Ptr u8), found (Ptr const u8)"; ~needle:"expected (Ptr u8), found (Ptr const u8)";
@ -2361,6 +2361,48 @@ 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
copy is as read-only as the original, through any number of lets. *)
rejects_check "push through a let-bound copy of a const element"
"(defn f [cs [const (Vec i32)]] () (let [v (at cs 0)] (push v 1)))"
~needle:"reached through a [const (Vec i32)]";
rejects_check "reserve through a copy of a copy"
"(defn f [cs [const (Vec i32)]] () (let [v (at cs 0) w v] (reserve w 9)))"
~needle:"reached through a [const (Vec i32)]";
rejects_check "put through a let-bound copy of a const element"
"(defn f [cs [const (Map string i32)]] () (let [m (at cs 0)] (put m \"a\" 1)))"
~needle:"reached through a [const (Map string i32)]";
rejects_check "push into a field of a let-bound copy"
"(defstruct P [v (Vec i32)]) \
(defn f [cs [const P]] () (let [p (at cs 0)] (push (.v p) 1)))"
~needle:"take the P it lives in as a [P]";
rejects_check "no copy of Vec headers is suggested"
"(defn f [cs [const (Vec i32)]] () (set (at cs 0) (vec-new i32)))"
~needle:"take it as a [(Vec i32)] instead";
(* A fixed array reached through read-only storage slices to a read-only
view. *)
rejects_check "slice of an array element of a const slice"
"(defn f [cs [const [4 u8]]] () (let [s (slice (at cs 0))] (set (at s 0) 9)))"
~needle:"this writes through a [const u8]";
rejects_check "slice of an array behind a const pointer"
"(defn f [p (Ptr const [4 u8])] () (let [s (slice (deref p))] (set (at s 0) 9)))"
~needle:"this writes through a [const u8]";
rejects_check "slice of an array field reached through a const slice"
"(defstruct B [buf [4 u8]]) \
(defn f [cs [const B]] () (let [s (slice (.buf (at cs 0)))] (set (at s 0) 9)))"
~needle:"this writes through a [const u8]";
infers "a local array still slices to a writable slice"
"(let [a [1 2]] (slice a))" "[i32]";
(* The branches of an if meet at the read-only type, in either order. *)
accepts "if: writable then read-only"
"(defn f [c bool cs [const u8] ms [u8]] i32 (length (if c ms cs)))";
accepts "if: read-only then writable"
"(defn f [c bool cs [const u8] ms [u8]] i32 (length (if c cs ms)))";
rejects_check "and the join is read-only"
"(defn f [c bool cs [const u8] ms [u8]] () (set (at (if c ms cs) 0) 1))"
~needle:"this writes through a [const u8]";
accepts "if over pointers joins the same way"
"(defn f [c bool a (Ptr const i32) b (Ptr i32)] i32 (deref (if c b a)))";
rejects_check "const is not a name a constant can have" rejects_check "const is not a name a constant can have"
"(defconst const 4)" ~needle:"const cannot be declared"; "(defconst const 4)" ~needle:"const cannot be declared";
(* The const is shallow: an element of a [const [u8]] is a writable [u8]. *) (* The const is shallow: an element of a [const [u8]] is a writable [u8]. *)