From ef87bdb3b321ad19e2d528b259c99ccc7bec7274 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sat, 26 Sep 2026 12:29:59 +0700 Subject: [PATCH] A prelude text builder checks its own String as a backstop, and a direct call checks the text it passes first, at the caller's line. --- docs/BUILT.md | 7 ++--- lib/check.ml | 47 ++++++++++++++++++++++++--------- lib/emit.ml | 1 + lib/prelude.ml | 23 ++++++++-------- runtime/flan_rt.c | 9 +++++++ test/programs/string-traps.flan | 4 ++- test/test_acceptance.ml | 21 +++++++++------ 7 files changed, 76 insertions(+), 36 deletions(-) diff --git a/docs/BUILT.md b/docs/BUILT.md index e762bb35..d16022d7 100644 --- a/docs/BUILT.md +++ b/docs/BUILT.md @@ -7536,9 +7536,10 @@ 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 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. +time. A direct call to a prelude function that answers a String has its text +arguments checked before the call, at the caller's line (`prechecked_call`); +each builder still ends in `(bytes->string b)`, the backstop for one reached +through a function value, which stops at the prelude's line. `=` 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. diff --git a/lib/check.ml b/lib/check.ml index dd7fd9bd..4dc386e3 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -11144,18 +11144,39 @@ and prelude_defined ctx name = | 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 ])) +(* A call to a prelude function that answers a String, its text arguments + checked here, at the call the program wrote, before the call is made. The + builders — (to-lower b), (join parts sep) — take bytes, and their answer is + valid exactly when every piece of text they were given is (UTF-8 is + self-synchronising, so a valid [from] matches a valid [s] only on + character boundaries). Each builder also checks its own answer, the + backstop for a builder reached through a function value; on this path that + check has nothing left to find, and stops nobody at the prelude's line. *) +and prechecked_call ctx loc name ret (args : Tast.expr list) = + let bytes = function + | Types.Slice (_, Types.Int Types.U8) | Types.String -> true + | _ -> false + in + let binds, checks, uses = + List.fold_right + (fun (a : Tast.expr) (bs, cs, us) -> + let check = + match a.Tast.ty with + | t when bytes t -> Some "flan_utf8_check" + | Types.Slice (_, t) when bytes t -> Some "flan_utf8_check_parts" + | _ -> None + in + match check with + | None -> (bs, cs, a :: us) + | Some sym -> + let sl = fresh_slot ctx a.Tast.ty in + let v = mk a.Tast.loc a.Tast.ty (Tast.Local sl) in + ((sl, a) :: bs, rt loc Types.Unit sym [ v; here loc ] :: cs, v :: us)) + args ([], [], []) + in + let call = mk loc ret (Tast.Call (name, uses)) in + if checks = [] then call + else mk loc ret (Tast.Let (binds, checks @ [ call ])) (* 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 @@ -13998,7 +14019,7 @@ and ordinary_call ctx ~want loc name args = 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 + then prechecked_call ctx loc name ret args else call)) | None -> if Hashtbl.mem ctx.env.datas name then diff --git a/lib/emit.ml b/lib/emit.ml index 015fed8e..09d6d8fd 100644 --- a/lib/emit.ml +++ b/lib/emit.ml @@ -5179,6 +5179,7 @@ declare i8 @flan_string_put_rune(ptr, i64, i32, ptr, i64) ; String's run-time checks: a text or a code point the checker could not prove ; valid, checked at the site of the append that stores it. declare void @flan_utf8_check(ptr, i64, ptr, i64) +declare void @flan_utf8_check_parts(ptr, i64, ptr, i64) declare void @flan_rune_check(i32, ptr, i64) ; (Map K V). The two ptr arguments before the location on put/get/clone are the ; hash and equality pair, which the checker emits per key type and passes here diff --git a/lib/prelude.ml b/lib/prelude.ml index b88636b1..3997843c 100644 --- a/lib/prelude.ml +++ b/lib/prelude.ml @@ -1719,10 +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]). +;; **The text builders check what they answer**, with (bytes->string b), and +;; that check stops the program at this file's line. A call the program writes +;; is checked first, at its own line, on the text it passes (check.ml, +;; [prechecked_call]); the check here is for a builder reached through a +;; function value, which has no call site to check at. ;; ;; **No Result, anywhere.** Running out of storage signals StorageExhausted ;; under a `retry` restart and no allocating operation returns an error @@ -1782,7 +1783,7 @@ let source = {flan| (let [b (vec-new u8)] (dotimes [i (length parts)] (append (addr b) (at parts i))) - (String {.bytes b}))) + (bytes->string 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 @@ -1794,13 +1795,13 @@ let source = {flan| (when (> i 0) (append (addr b) sep)) (append (addr b) (at parts i))) - (String {.bytes b}))) + (bytes->string b))) (defn repeat-bytes [s [const u8] n i32] String (let [b (vec-new u8)] (dotimes [i n] (append (addr b) s)) - (String {.bytes b}))) + (bytes->string 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. @@ -1808,13 +1809,13 @@ let source = {flan| (let [b (vec-new u8)] (dotimes [i (length s)] (push b (lower-ascii (at s i)))) - (String {.bytes b}))) + (bytes->string b))) (defn to-upper [s [const u8]] String (let [b (vec-new u8)] (dotimes [i (length s)] (push b (upper-ascii (at s i)))) - (String {.bytes b}))) + (bytes->string 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 @@ -1845,7 +1846,7 @@ let source = {flan| (do (append (addr b) (slice s i (length s))) (set i (length s)))))) - (String {.bytes b}))) + (bytes->string 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 @@ -1965,7 +1966,7 @@ let source = {flan| (dotimes [i (- p (length d))] (push b \0)) (append (addr b) d)))))))) - (String {.bytes b}))) + (bytes->string b))) ;; ── Still refused, and what the reason is now ───────────────────────── ;; diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c index 4232b07f..1b245a0f 100644 --- a/runtime/flan_rt.c +++ b/runtime/flan_rt.c @@ -2846,6 +2846,15 @@ void flan_utf8_check(const uint8_t *p, int64_t n, const uint8_t *loc, rt_trap((const uint8_t *)"InvalidUtf8", 11); } +/* The same over a slice of byte slices, each a (ptr, len) pair: the parts a + * join or a concat is handed. */ +void flan_utf8_check_parts(const void *parts, int64_t n, const uint8_t *loc, + int64_t loclen) { + const struct { const uint8_t *p; int64_t n; } *ps = parts; + int64_t i; + for (i = 0; i < n; i++) flan_utf8_check(ps[i].p, ps[i].n, loc, loclen); +} + void flan_rune_check(int32_t c, const uint8_t *loc, int64_t loclen) { if (c >= 0 && c <= 0x10ffff && !(c >= 0xd800 && c <= 0xdfff)) return; flan_say(loc, loclen, diff --git a/test/programs/string-traps.flan b/test/programs/string-traps.flan index 27947dce..3f951715 100644 --- a/test/programs/string-traps.flan +++ b/test/programs/string-traps.flan @@ -2,7 +2,8 @@ ;;;; 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; and a text builder -;;;; given bytes that are not UTF-8 stops at the call that asked for it. The +;;;; given bytes that are not UTF-8 stops at the call that asked for it, or, +;;;; called through a function value, at its own check in the prelude. The ;;;; test asserts the line and column of each. (defonce bad [2 u8]) @@ -18,6 +19,7 @@ (= which 2) (insert s 3 "x") (= which 3) (println (remove s 2)) (= which 5) (println (to-lower (slice bad))) + (= which 6) (let [f to-lower] (println (f (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 c8f955b2..b9c27dc3 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -2051,16 +2051,21 @@ let () = arg (match x86 with Some true -> ", --x86" | _ -> "") text code want end) - [ ("0", "string-traps.flan:16:19: this text is not valid UTF-8 — byte 0 \ + [ ("0", "string-traps.flan:17:19: this text is not valid UTF-8 — byte 0 \ is 0xc3"); - ("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 \ + ("1", "string-traps.flan:18:19: 55296 is not a Unicode scalar value"); + ("2", "string-traps.flan:19:19: index 3 is out of bounds for length 2"); + ("3", "string-traps.flan:20:28: index 2 is out of bounds for length 2"); + (* A builder called by name is checked at the call, before it runs. *) + ("5", "string-traps.flan:21: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 \ + (* Called through a function value, it has no call site to check at, + and its own check in the prelude stops it: the site is the + prelude's, and the line is not pinned here so that editing the + prelude does not move this row. *) + ("6", ":"); + ("6", ": this text is not valid UTF-8 — byte 0 is 0xc3"); + ("4", "string-traps.flan:23:23: this text is not valid UTF-8 — byte 0 \ is 0xff") ]; (try Sys.remove exe with Sys_error _ -> ()) in