From bfdd971baa82015f6f93533ec95e330596e08e4d Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 26 Sep 2026 12:22:17 +0700 Subject: [PATCH] A String compares equal to a String or a str by its bytes, and a prelude builder's String is checked at the caller's line. --- TODO.org | 3 +- docs/BUILT.md | 8 ++- lib/check.ml | 109 +++++++++++++++++++++++++++++++- lib/prelude.ml | 19 ++++-- test/programs/string-owned.flan | 8 +++ test/programs/string-traps.flan | 6 +- test/test_acceptance.ml | 17 +++-- test/test_flan.ml | 11 ++++ 8 files changed, 162 insertions(+), 19 deletions(-) diff --git a/TODO.org b/TODO.org index aa83a2a7..e233f2f0 100644 --- a/TODO.org +++ b/TODO.org @@ -33,7 +33,8 @@ str. Waits on the dyn-unless-annotated design. CLOSED: [2026-09-26] Its field and constructor are refused outside the prelude; a str or a code point is checked at run time at the append that stores it (literals at compile time), a [const u8] is refused for -(str b). Rules out a String type in the backends, s[i] = c, and a byte path that skips the check. +(str b); a prelude builder's String is checked at the caller's call. = and != compare bytes. +Rules out a String type in the backends, s[i] = c, a String map key, and a byte path that skips the check. ** DONE Any typed container crosses into dyn as a view CLOSED: [2026-09-26] diff --git a/docs/BUILT.md b/docs/BUILT.md index ac196fad..e762bb35 100644 --- a/docs/BUILT.md +++ b/docs/BUILT.md @@ -7536,8 +7536,12 @@ byte arrives through `string-new`, `append`, `insert` or `bytes->string`. Text the checker cannot prove valid — any str, since `(str b)` does not check — is checked by `flan_utf8_check` at the site that stores it; a code point by `flan_rune_check` inside `flan_string_put_rune`. Literals are checked at compile -time. The prelude's builders end in `(bytes->string b)`, so a builder given bytes -that are not UTF-8 stops at the prelude's line, not the caller's. +time. The prelude's builders wrap their Vec unchecked, and `ordinary_call` +checks any String a prelude function answers at the caller's call +(`checked_string`), so bytes that are not UTF-8 stop at the line that asked. +`=` and `!=` compare a String with a String or a str through their str views; +`peeks_string` decides that from the operands' declared types without checking +them twice. Ordering and map keys are refused with the fix named. Positions are characters: `flan_string_index` walks to one and signals BoundsError with the character count as the length, which is why it joins diff --git a/lib/check.ml b/lib/check.ml index 87a38627..dd7fd9bd 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -4924,6 +4924,13 @@ let rec key_pair env loc (k : Types.t) : Tast.fnref * Tast.fnref = | Types.String -> Tast.Rtfn "flan_hash_str", Tast.Rtfn "flan_eq_str" | t when bytewise_key t -> Tast.Rtfn "flan_hash_flat", Tast.Rtfn "flan_eq_flat" + | t when is_string_ty t -> + fail loc + "a String owns its bytes, and a map would share them with it rather \ + than copy them, so a String is not a map key. Key the map by str and \ + put %s, which is the String's text for as long as the String is not \ + changed" + (if fln_source loc then "str(s)" else "(str s)") | Types.Named n when Hashtbl.mem env.structs n -> struct_key_pair env loc n (* A data type key would have to hash the tag and then only the bytes the case in hand actually uses — the rest of the payload is indeterminate, @@ -11131,6 +11138,97 @@ and prelude_fn ctx name = let moved = "prelude~/" ^ name in if Hashtbl.mem ctx.env.fns moved then moved else name +(* Whether [name] is the prelude's own function. *) +and prelude_defined ctx name = + match Hashtbl.find_opt ctx.env.fn_locs name with + | Some at -> String.equal at.Loc.file Prelude.file + | None -> false + +(* A String a prelude builder answered, checked here, at the call the program + wrote. The builders take bytes — (to-lower b), (join parts sep) — and wrap + what they built without a check of their own, because a check inside the + prelude would stop the program at the prelude's line rather than at the + caller's. A builder reached through a function value is not checked. *) +and checked_string ctx loc (call : Tast.expr) = + let sl = fresh_slot ctx string_ty in + let s = mk loc string_ty (Tast.Local sl) in + mk loc string_ty + (Tast.Let ([ (sl, call) ], + [ rt loc Types.Unit "flan_utf8_check" [ string_bytes ctx loc s; here loc ]; + s ])) + +(* Whether an operand is a String, read off what the operand is without + checking it: a local or a global of that type, a call to a function that + answers one, a field of that type, or one of the builtins that make one. A + comparison asks this of every operand, so it must not walk them. *) +and peeks_string ctx (a : Ast.expr) = + let rec ty (a : Ast.expr) = + match a.Ast.e with + | Ast.Var n -> + (match lookup ctx n with + | Some b -> Some b.bty + | None -> + (match Hashtbl.find_opt ctx.env.globals n with + | Some (t, _) -> Some t + | None -> None)) + | Ast.Call ({ Ast.e = Ast.Var ("string-new" | "bytes->string"); _ }, _) -> + Some string_ty + | Ast.Call ({ Ast.e = Ast.Var "deref"; _ }, [ p ]) -> + (match ty p with Some (Types.Ptr (_, t)) -> Some t | _ -> None) + | Ast.Call ({ Ast.e = Ast.Var f; _ }, _) -> + (match Hashtbl.find_opt ctx.env.fns f with + | Some (_, ret) -> Some ret + | None -> None) + | Ast.Field (t, name) -> + (match ty t with + | Some (Types.Named n | Types.Ptr (_, Types.Named n)) -> + (match fields_named ctx.env n with + | Some st -> + (match Tast.field_index st name with + | Some i -> Some (List.nth st.Tast.fields i).Tast.fty + | None -> None) + | None -> None) + | _ -> None) + | _ -> None + in + match ty a with Some t -> string_or_ptr t | None -> false + +(* = and != over a String and a String or a str: the texts' bytes compared, + through the str view each has, which is the comparison str already has. + The orderings are refused as they are on a str, naming bytes () + | _ -> + fail loc + "%s orders machine numbers and enums, and a String is neither. Text is \ + ordered by its bytes with %s" + name + (if fln_source loc then "bytes check ctx ~want:Types.String x + | _ -> check ctx x + in + match e.Tast.ty with + | Types.String -> e + | t when string_or_ptr t -> + mk x.Ast.loc Types.String + (Tast.Prim (Tast.StrOfBytes, [ string_bytes ctx x.Ast.loc e ])) + | other -> + fail x.Ast.loc "%s compares a String with a String or a str, found %s" + name (tyname x.Ast.loc other) + in + let ops = List.map as_str args in + let link u v = mk loc Types.Bool (Tast.Prim (p, [ u; v ])) in + match ops with + | [ a; b ] -> expect ctx loc ~want (link a b) + | _ -> + let pairs = if String.equal name "!=" then all_pairs else adjacent_pairs in + expect ctx loc ~want (cmp_over ctx loc Types.String ~pairs ~link ops) + and string_call ctx ~want loc name args = let i64 n = mk loc (Types.Int Types.I64) (Tast.Int (n, Types.I64)) in match name, args with @@ -11366,6 +11464,9 @@ and named_call ?(qualified = false) ctx ~want loc name args = let x, y, rest = match args with x :: y :: rest -> x, y, rest | _ -> assert false in + if List.exists (fun a -> peeks_string ctx a) args then + string_compare ctx ~want loc name p args + else (* The first pair decides the type, and whether this is a dyn comparison at all, exactly as it does for the folding operators: [binary] joins the two, and every operand after them is checked against the answer. @@ -13892,7 +13993,13 @@ and ordinary_call ctx ~want loc name args = (temps, [ rt loc Types.Unit "flan_dyn_ctor_site" [ here loc ]; mk loc ret (Tast.Call (name, uses)) ]))) - | None -> expect ctx loc ~want (mk loc ret (Tast.Call (name, args)))) + | None -> + let call = mk loc ret (Tast.Call (name, args)) in + expect ctx loc ~want + (if is_string_ty ret && prelude_defined ctx name + && not (String.equal loc.Loc.file Prelude.file) + then checked_string ctx loc call + else call)) | None -> if Hashtbl.mem ctx.env.datas name then fail loc diff --git a/lib/prelude.ml b/lib/prelude.ml index b8d8e2ed..b88636b1 100644 --- a/lib/prelude.ml +++ b/lib/prelude.ml @@ -1719,6 +1719,11 @@ let source = {flan| ;; writes (with-allocator a (join parts sep)) and the Vec records the arena, so ;; the free and the clone never need it named again. ;; +;; **The text builders answer a String without checking it.** Each takes +;; bytes, and a check here would stop the program at this file's line; the +;; checker checks the String at the caller's call instead (check.ml, +;; [checked_string]). +;; ;; **No Result, anywhere.** Running out of storage signals StorageExhausted ;; under a `retry` restart and no allocating operation returns an error ;; (spec-memory.md, "Allocation failure"), so these signatures say what they @@ -1777,7 +1782,7 @@ let source = {flan| (let [b (vec-new u8)] (dotimes [i (length parts)] (append (addr b) (at parts i))) - (bytes->string b))) + (String {.bytes b}))) ;; n parts yield n-1 separators, and the empty slice of parts yields the empty ;; result rather than a leading separator — which is the off-by-one a join @@ -1789,13 +1794,13 @@ let source = {flan| (when (> i 0) (append (addr b) sep)) (append (addr b) (at parts i))) - (bytes->string b))) + (String {.bytes b}))) (defn repeat-bytes [s [const u8] n i32] String (let [b (vec-new u8)] (dotimes [i n] (append (addr b) s)) - (bytes->string b))) + (String {.bytes b}))) ;; The allocating halves of the ASCII case pair. The note above lower-ascii ;; says why there is no in-place one; these write only bytes of their own. @@ -1803,13 +1808,13 @@ let source = {flan| (let [b (vec-new u8)] (dotimes [i (length s)] (push b (lower-ascii (at s i)))) - (bytes->string b))) + (String {.bytes b}))) (defn to-upper [s [const u8]] String (let [b (vec-new u8)] (dotimes [i (length s)] (push b (upper-ascii (at s i)))) - (bytes->string b))) + (String {.bytes b}))) ;; Every non-overlapping occurrence, left to right, which is the rule that ;; makes (replace-bytes (bytes-view "aaa") (bytes-view "aa") (bytes-view "b")) answer "ba" and @@ -1840,7 +1845,7 @@ let source = {flan| (do (append (addr b) (slice s i (length s))) (set i (length s)))))) - (bytes->string b))) + (String {.bytes b}))) ;; A (Vec [u8]) cannot be written at a let, and this one-line function is where ;; the type is said instead. (vec-new) takes its element type as a *bare @@ -1960,7 +1965,7 @@ let source = {flan| (dotimes [i (- p (length d))] (push b \0)) (append (addr b) d)))))))) - (bytes->string b))) + (String {.bytes b}))) ;; ── Still refused, and what the reason is now ───────────────────────── ;; diff --git a/test/programs/string-owned.flan b/test/programs/string-owned.flan index bf3b5c5c..65f30d6a 100644 --- a/test/programs/string-owned.flan +++ b/test/programs/string-owned.flan @@ -57,6 +57,14 @@ (let [j (join (slice [(bytes-view "a") (bytes-view "b")]) (bytes-view "-"))] (println j) (free j)) + ;; = and != compare bytes, against a String or a str, either side first. + (let [a (string-new "日本") + b (string-new "日")] + (append b 0x672c) + (println (= a b) (!= a b) (= a "日本") (= "日本" a) (= a "日") (!= b "x")) + (println (= a b (to-upper (bytes-view "日本")))) + (free a) + (free b)) (let [e (string-new)] (println (length e) (rune-count e)) (free e)) diff --git a/test/programs/string-traps.flan b/test/programs/string-traps.flan index c444b3f9..27947dce 100644 --- a/test/programs/string-traps.flan +++ b/test/programs/string-traps.flan @@ -1,8 +1,9 @@ ;;;; What a String refuses at run time, one per run: the argument chooses. ;;;; Bytes that are not UTF-8, reached through a str, stop the program at the ;;;; append; so does a code point with no encoding; a character position past -;;;; the end signals BoundsError counted in characters. The test asserts the -;;;; line and column of each. +;;;; the end signals BoundsError counted in characters; and a text builder +;;;; given bytes that are not UTF-8 stops at the call that asked for it. The +;;;; test asserts the line and column of each. (defonce bad [2 u8]) (defn main [args [str]] i32 @@ -16,6 +17,7 @@ (= which 1) (append s (+ 0xd800 which -1)) (= which 2) (insert s 3 "x") (= which 3) (println (remove s 2)) + (= which 5) (println (to-lower (slice bad))) :else (append s (bytes->string (let [v (vec-new u8)] (push v 0xff) v)))) (println s)) 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index e0593838..c8f955b2 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -2024,7 +2024,8 @@ let () = let owned_out = "héllo wörld日!\n17 13\n😀h→éllo wörld日!\n8594\n128512\n\ héllo wörld日!\nabababab 8\n233 246 26085 13\n17 18\ntrue\n17\n\ - (Named {.label \"x\" .n 3})\nhéllo wörld日!\n:text\na-b\n0 0\n" + (Named {.label \"x\" .n 3})\nhéllo wörld日!\n:text\na-b\n\ + true false true true false true\ntrue\n0 0\n" in outputs "an owned String" "programs/string-owned.flan" owned_out; outputs ~opt:"-O0" "an owned String, -O0" "programs/string-owned.flan" @@ -2050,12 +2051,16 @@ let () = arg (match x86 with Some true -> ", --x86" | _ -> "") text code want end) - [ ("0", "string-traps.flan:15:19: this text is not valid UTF-8 — byte 0 \ + [ ("0", "string-traps.flan:16:19: this text is not valid UTF-8 — byte 0 \ is 0xc3"); - ("1", "string-traps.flan:16:19: 55296 is not a Unicode scalar value"); - ("2", "string-traps.flan:17:19: index 3 is out of bounds for length 2"); - ("3", "string-traps.flan:18:28: index 2 is out of bounds for length 2"); - ("4", "string-traps.flan:19:23: this text is not valid UTF-8 — byte 0 \ + ("1", "string-traps.flan:17:19: 55296 is not a Unicode scalar value"); + ("2", "string-traps.flan:18:19: index 3 is out of bounds for length 2"); + ("3", "string-traps.flan:19:28: index 2 is out of bounds for length 2"); + (* The builder's own check is made at the call, not inside the + prelude. *) + ("5", "string-traps.flan:20:28: this text is not valid UTF-8 — byte 0 \ + is 0xc3"); + ("4", "string-traps.flan:21:23: this text is not valid UTF-8 — byte 0 \ is 0xff") ]; (try Sys.remove exe with Sys_error _ -> ()) in diff --git a/test/test_flan.ml b/test/test_flan.ml index ecc9d668..5440e2cc 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -2354,6 +2354,17 @@ let () = rejects_check "a String through a const pointer is not changed" "(defn f [s (Ptr const String)] () (append s \"x\"))" ~needle:"can only be read"; + rejects_check "a String is not ordered" + "(defn f [a String b String] bool (< a b))" + ~needle:"(bytes