From 1e5be63a1ad46e9849d148086d7398b023ce6d89 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 13:08:29 +0700 Subject: [PATCH] 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 --- docs/BUILT.md | 2 +- lib/check.ml | 142 ++++++++++++++++++++++++++++++++-------------- lib/types.ml | 8 +++ test/test_flan.ml | 56 +++++++++++++++--- 4 files changed, 157 insertions(+), 51 deletions(-) diff --git a/docs/BUILT.md b/docs/BUILT.md index 9974edcd..5050d0a2 100644 --- a/docs/BUILT.md +++ b/docs/BUILT.md @@ -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 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 -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. 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. diff --git a/lib/check.ml b/lib/check.ml index dfd97c60..4be7ddf2 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -556,6 +556,8 @@ type ctx = { the outer scope is a list and the names on it were not all written for this body's sake. *) 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 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 @@ -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 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. *) -let rec const_reached (e : Tast.expr) = +let rec const_reached ?(local = fun (_ : int) -> None) (e : Tast.expr) = match e.Tast.e with | Tast.Prim (Tast.At, target :: idx) -> - const_steps (const_reached target) target.Tast.ty (List.length idx) - | Tast.Field (target, _) -> const_reached target + const_steps (const_reached ~local target) target.Tast.ty (List.length idx) + | Tast.Field (target, _) -> const_reached ~local target + | Tast.Local s -> local s | Tast.Deref p -> (match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None) | _ -> None @@ -2230,6 +2233,15 @@ and const_steps ro (ty : Types.t) n = | Types.Array (_, t) -> const_steps ro t (n - 1) | _ -> 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). *) let refuse_const_place loc (view : Types.t) = 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 Loc.failk "check/store-through-const" loc "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: \ - (slice (into v (vec-new %s))) copies v's elements into one" - (Types.to_string view) (Types.to_string elem) - -(* The runtime entry points that change a Vec or a Map, which the backends - hand the container's address. An element of a [[const (Vec T)]], or a field - reached through one, is storage the view may not write, so growing, - shrinking or freeing it there is the same 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 the buffer is - 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 + value and not a place. %s" + (Types.to_string view) + (match const_copy elem with + | Some c -> + Printf.sprintf + "Write into a slice that can be written: %s copies v's elements \ + into one" c + | None -> + Printf.sprintf "Where it has to be written, take it as a [%s] instead" + (Types.to_string elem)) (* A runtime call, with the result type spelled at the site. *) -let rt loc ty 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)) +let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args)) (* ── The allocation registry's note ────────────────────────────────── @@ -3116,14 +3117,19 @@ let const_note ~(want : Types.t) ~(got : Types.t) = when Types.equal e e' -> let copy = match e with - | Types.Int Types.U8 -> "(bytes (string v))" - | _ -> Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e) + | Types.Int Types.U8 -> Some "(bytes (string v))" + | _ -> const_copy e in Printf.sprintf " — 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 it, the %s can be declared %s instead" - (Types.to_string got) (Types.to_string want) copy (Types.to_string want) + through. %sWhere nothing writes through it, the %s can be declared %s \ + instead" + (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.Ptr (Types.Mut, e), Types.Ptr (Types.Const, e') when Types.equal e e' -> @@ -3271,7 +3277,7 @@ let hash_ty = Types.Int Types.U64 would share a slot counter. *) let invented_ctx env ret = { 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"; owner = "" } @@ -5019,6 +5025,13 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body = | _ -> ()); (* Locals are assignable places; parameters are not. *) 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)) bs 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 (* With no expectation the then-branch supplies one for the else-branch, 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 = match want with | 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 (* [(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 @@ -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" (Types.to_string t.Tast.ty) 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 = if t.Tast.ty = Types.Never then e.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 \ 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 [[const T]] or a (Ptr const T), or a byte of a string. Its address is a (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 || 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 = match p with | Ast.Pvar name -> @@ -8059,6 +8103,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = (match args with | [ target; x ] -> 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 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 @@ -8099,6 +8144,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = (match args with | [ target; n ] -> let target = check ctx target in + refuse_const_change ctx loc target; let n = check ctx ~want:index_ty n in let n64 = 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" -> arity ctx loc name 1 args; 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 assume the opposite — that [free] recurses — so this says why it does not and what does. @@ -8311,6 +8358,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = (match args with | [ target; k; v ] -> 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 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. *) @@ -8436,6 +8484,7 @@ and named_call ?(qualified = false) ctx ~want loc name args = (match args with | [ target; k ] -> 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 k = check ctx ~want:kt k in (* 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 storage the program does not own. *) 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.Slice (m, t) -> Types.Slice (m, t) | 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) -> Printf.sprintf " — %s takes a slice it may write through, and a %s can \ - only be read. (slice (into v (vec-new %s))) copies v into \ - one that can be written" - name (Types.to_string a.Tast.ty) (Types.to_string e) + only be read%s" + name (Types.to_string a.Tast.ty) + (match const_copy e with + | Some c -> + Printf.sprintf ". %s copies v into one that can be written" c + | None -> "") | _ -> ""); a) pats args @@ -10395,7 +10451,7 @@ and trial ctx f = resource failure into a wrong answer. *) let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope; 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; owner = _ } = ctx in match f () with @@ -10406,7 +10462,7 @@ and trial ctx f = ctx.defers <- defers; ctx.defer_slot <- defer_slot; ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block; 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; Error d diff --git a/lib/types.ml b/lib/types.ml index bccd930a..eefb0bbf 100644 --- a/lib/types.ml +++ b/lib/types.ml @@ -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 [[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 = + 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 ps', r' = from and ps, r = into in List.length ps = List.length ps' diff --git a/test/test_flan.ml b/test/test_flan.ml index adc0a418..31722fd1 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -2291,22 +2291,22 @@ let () = ~needle:"expected [[const u8]], found [[u8]]"; rejects_check "push through a const slice of Vecs" "(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" "(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" "(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" "(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" "(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" "(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" "(defn f [s [const (Vec i32)]] () (set (at (at s 0) 0) 5))"; accepts "a reading function where a writing one is wanted" @@ -2341,7 +2341,7 @@ let () = ~needle:"this writes through a (Ptr const P)"; rejects_check "a push through a const pointer" "(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" "(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)"; @@ -2361,6 +2361,48 @@ let () = "(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" "(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" "(defconst const 4)" ~needle:"const cannot be declared"; (* The const is shallow: an element of a [const [u8]] is a writable [u8]. *)