From c0b4b2235754920c49bc1972d2b682a8eb57546b Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Fri, 25 Sep 2026 12:10:47 +0700 Subject: [PATCH] Growing, shrinking or freeing a container reached through a [const T] is refused, and a function that only reads a slice stands where one that may write it is wanted --- lib/check.ml | 89 +++++++++++++++++++++------------- lib/types.ml | 13 +++++ test/programs/const-slice.flan | 9 ++++ test/test_acceptance.ml | 2 +- test/test_flan.ml | 31 ++++++++++++ 5 files changed, 110 insertions(+), 34 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index c1bf23c0..e22d0889 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -2192,8 +2192,57 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc = crosses as ptr+len like any other. *) let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc)) +(* The read-only slice a value's storage is reached through, if there is one: + an element of a [[const T]], a field of such an element, or an element of + 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) = + 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 + | _ -> None + +(* [ro] after stepping [n] dimensions into [ty], the way [indexed] steps. *) +and const_steps ro (ty : Types.t) n = + if n = 0 then ro + else + match ty with + | Types.Slice (Types.Const, t) -> const_steps (Some ty) t (n - 1) + | Types.Slice (Types.Mut, t) -> const_steps None t (n - 1) + | Types.Array (_, t) -> const_steps ro t (n - 1) + | _ -> ro + +(* A store, or an [addr], through a read-only view. *) +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 + (* A runtime call, with the result type spelled at the site. *) -let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args)) +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)) (* ── The allocation registry's note ────────────────────────────────── @@ -3093,8 +3142,13 @@ let expect ctx loc ~want (got : Tast.expr) = [CFn] has nowhere to put one — so the reverse falls through to the ordinary refusal, which names both types and is the right sentence. *) | Types.Fn (ps, r), Types.CFn (ps', r') - when Types.equal (Types.Fn (ps, r)) (Types.Fn (ps', r')) -> + when Types.fn_accepts ~from:(ps', r') ~into:(ps, r) -> mk loc w (Tast.Thicken (thick_thunk ctx.env loc ps r, got)) + (* The same signature up to const, which [Types.fn_accepts] defines. *) + | Types.Fn (ps, r), Types.Fn (ps', r') + | Types.CFn (ps, r), Types.CFn (ps', r') + when Types.fn_accepts ~from:(ps', r') ~into:(ps, r) -> + { got with Tast.ty = w } (* A writable view seen as a read-only one. The two are the same two words, so the value is only retyped; the reverse is refused below, with [const_note] naming the copy that would make it writable. *) @@ -6448,37 +6502,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" -(* The read-only slice a value's storage is reached through, if there is one: - an element of a [[const T]], a field of such an element, or an element of - 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. *) -and const_reached (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 - | _ -> None - -(* [ro] after stepping [n] dimensions into [ty], the way [indexed] steps. *) -and const_steps ro (ty : Types.t) n = - if n = 0 then ro - else - match ty with - | Types.Slice (Types.Const, t) -> const_steps (Some ty) t (n - 1) - | Types.Slice (Types.Mut, t) -> const_steps None t (n - 1) - | Types.Array (_, t) -> const_steps ro t (n - 1) - | _ -> ro - -(* A store, or an [addr], through a read-only view. *) -and 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) - (* [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 diff --git a/lib/types.ml b/lib/types.ml index c6bc9ae7..7ef1cd4d 100644 --- a/lib/types.ml +++ b/lib/types.ml @@ -346,3 +346,16 @@ let rec const_widens ~(from : t) ~(into : t) = match from, into with | Slice (_, a), Slice (Const, b) -> equal a b || const_widens ~from:a ~into:b | _ -> false + +(* 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 ps', r' = from and ps, r = into in + List.length ps = List.length ps' + && List.for_all2 + (fun p p' -> equal p p' || const_widens ~from:p ~into:p') ps ps' + && (equal r r' || const_widens ~from:r' ~into:r) diff --git a/test/programs/const-slice.flan b/test/programs/const-slice.flan index 3d83ebde..6ab1db0f 100644 --- a/test/programs/const-slice.flan +++ b/test/programs/const-slice.flan @@ -18,6 +18,14 @@ (set n (+ n (length (at parts i))))) n)) +;; A function that only reads stands where one that may write is wanted, and +;; one returning a writable slice where a read-only one is wanted. +(defn rd [s [const u8]] i32 (length s)) +(defn call-rd [f (Fn [[u8]] i32)] i32 (f (bytes "abc"))) +(defn call-bare [f (CFn [[u8]] i32)] i32 (f (bytes "abcd"))) +(defn mk [] [u8] (bytes "xy")) +(defn call-mk [f (Fn [] [const u8])] i32 (length (f))) + (defn main [] i32 (let [xs [3 1 2] w (slice xs) @@ -45,5 +53,6 @@ (sort-bytes (slice f)) (println (string (slice (join (slice f) (bytes-view "-")))))) (println (at r 0)) + (println (call-rd rd) (call-bare rd) (call-mk mk)) (free names)) 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 7b1b65c5..4ef0165a 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -872,7 +872,7 @@ let () = (* [const T]: the checker's alone, so the three builds agree and every row is about which values reach which parameters. *) let const_slice_out = - "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n" + "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n3 4 2\n" in outputs "const slices" "programs/const-slice.flan" const_slice_out; outputs ~opt:"-O0" "const slices, -O0" "programs/const-slice.flan" diff --git a/test/test_flan.ml b/test/test_flan.ml index c4fc6f18..77abd557 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -2291,6 +2291,37 @@ let () = rejects_check "no conversion under a writable slice" "(defn g [p [[const u8]]] i32 0) (defn f [p [[u8]]] i32 (g p))" ~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)]"; + 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)]"; + 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)]"; + 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)]"; + 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)]"; + 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]"; + 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" + "(defn rd [s [const u8]] i32 0) (defn c [f (Fn [[u8]] i32)] i32 0) \ + (defn m [] i32 (c rd))"; + rejects_check "not a writing function where a reading one is wanted" + "(defn wr [s [u8]] i32 0) (defn c [f (Fn [[const u8]] i32)] i32 0) \ + (defn m [] i32 (c wr))" + ~needle:"expected (Fn [[const u8]] i32), found (CFn [[u8]] i32)"; + rejects_check "nor a read-only result where a writable one is wanted" + "(defn mk [] [const u8] (bytes-view \"a\")) \ + (defn c [f (Fn [] [u8])] i32 0) (defn m [] i32 (c mk))" + ~needle:"expected (Fn [] [u8]), found (CFn [] [const u8])"; 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]. *)