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.

This commit is contained in:
Joseph Ferano 2026-09-26 12:29:59 +07:00
parent bfdd971baa
commit ef87bdb3b3
7 changed files with 76 additions and 36 deletions

View File

@ -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 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 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 `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` time. A direct call to a prelude function that answers a String has its text
checks any String a prelude function answers at the caller's call arguments checked before the call, at the caller's line (`prechecked_call`);
(`checked_string`), so bytes that are not UTF-8 stop at the line that asked. 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; `=` 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 `peeks_string` decides that from the operands' declared types without checking
them twice. Ordering and map keys are refused with the fix named. them twice. Ordering and map keys are refused with the fix named.

View File

@ -11144,18 +11144,39 @@ and prelude_defined ctx name =
| Some at -> String.equal at.Loc.file Prelude.file | Some at -> String.equal at.Loc.file Prelude.file
| None -> false | None -> false
(* A String a prelude builder answered, checked here, at the call the program (* A call to a prelude function that answers a String, its text arguments
wrote. The builders take bytes — (to-lower b), (join parts sep) — and wrap checked here, at the call the program wrote, before the call is made. The
what they built without a check of their own, because a check inside the builders — (to-lower b), (join parts sep) — take bytes, and their answer is
prelude would stop the program at the prelude's line rather than at the valid exactly when every piece of text they were given is (UTF-8 is
caller's. A builder reached through a function value is not checked. *) self-synchronising, so a valid [from] matches a valid [s] only on
and checked_string ctx loc (call : Tast.expr) = character boundaries). Each builder also checks its own answer, the
let sl = fresh_slot ctx string_ty in backstop for a builder reached through a function value; on this path that
let s = mk loc string_ty (Tast.Local sl) in check has nothing left to find, and stops nobody at the prelude's line. *)
mk loc string_ty and prechecked_call ctx loc name ret (args : Tast.expr list) =
(Tast.Let ([ (sl, call) ], let bytes = function
[ rt loc Types.Unit "flan_utf8_check" [ string_bytes ctx loc s; here loc ]; | Types.Slice (_, Types.Int Types.U8) | Types.String -> true
s ])) | _ -> 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 (* 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 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 expect ctx loc ~want
(if is_string_ty ret && prelude_defined ctx name (if is_string_ty ret && prelude_defined ctx name
&& not (String.equal loc.Loc.file Prelude.file) && not (String.equal loc.Loc.file Prelude.file)
then checked_string ctx loc call then prechecked_call ctx loc name ret args
else call)) else call))
| None -> | None ->
if Hashtbl.mem ctx.env.datas name then if Hashtbl.mem ctx.env.datas name then

View File

@ -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 ; 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. ; 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(ptr, i64, ptr, i64)
declare void @flan_utf8_check_parts(ptr, i64, ptr, i64)
declare void @flan_rune_check(i32, 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 ; (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 ; hash and equality pair, which the checker emits per key type and passes here

View File

@ -1719,10 +1719,11 @@ let source = {flan|
;; writes (with-allocator a (join parts sep)) and the Vec records the arena, so ;; 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 free and the clone never need it named again.
;; ;;
;; **The text builders answer a String without checking it.** Each takes ;; **The text builders check what they answer**, with (bytes->string b), and
;; bytes, and a check here would stop the program at this file's line; the ;; that check stops the program at this file's line. A call the program writes
;; checker checks the String at the caller's call instead (check.ml, ;; is checked first, at its own line, on the text it passes (check.ml,
;; [checked_string]). ;; [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 ;; **No Result, anywhere.** Running out of storage signals StorageExhausted
;; under a `retry` restart and no allocating operation returns an error ;; under a `retry` restart and no allocating operation returns an error
@ -1782,7 +1783,7 @@ let source = {flan|
(let [b (vec-new u8)] (let [b (vec-new u8)]
(dotimes [i (length parts)] (dotimes [i (length parts)]
(append (addr b) (at parts i))) (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 ;; 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 ;; result rather than a leading separator — which is the off-by-one a join
@ -1794,13 +1795,13 @@ let source = {flan|
(when (> i 0) (when (> i 0)
(append (addr b) sep)) (append (addr b) sep))
(append (addr b) (at parts i))) (append (addr b) (at parts i)))
(String {.bytes b}))) (bytes->string b)))
(defn repeat-bytes [s [const u8] n i32] String (defn repeat-bytes [s [const u8] n i32] String
(let [b (vec-new u8)] (let [b (vec-new u8)]
(dotimes [i n] (dotimes [i n]
(append (addr b) s)) (append (addr b) s))
(String {.bytes b}))) (bytes->string b)))
;; The allocating halves of the ASCII case pair. The note above lower-ascii ;; 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. ;; 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)] (let [b (vec-new u8)]
(dotimes [i (length s)] (dotimes [i (length s)]
(push b (lower-ascii (at s i)))) (push b (lower-ascii (at s i))))
(String {.bytes b}))) (bytes->string b)))
(defn to-upper [s [const u8]] String (defn to-upper [s [const u8]] String
(let [b (vec-new u8)] (let [b (vec-new u8)]
(dotimes [i (length s)] (dotimes [i (length s)]
(push b (upper-ascii (at s i)))) (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 ;; 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 ;; makes (replace-bytes (bytes-view "aaa") (bytes-view "aa") (bytes-view "b")) answer "ba" and
@ -1845,7 +1846,7 @@ let source = {flan|
(do (do
(append (addr b) (slice s i (length s))) (append (addr b) (slice s i (length s)))
(set 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 ;; 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 ;; 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))] (dotimes [i (- p (length d))]
(push b \0)) (push b \0))
(append (addr b) d)))))))) (append (addr b) d))))))))
(String {.bytes b}))) (bytes->string b)))
;; ── Still refused, and what the reason is now ───────────────────────── ;; ── Still refused, and what the reason is now ─────────────────────────
;; ;;

View File

@ -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); 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) { void flan_rune_check(int32_t c, const uint8_t *loc, int64_t loclen) {
if (c >= 0 && c <= 0x10ffff && !(c >= 0xd800 && c <= 0xdfff)) return; if (c >= 0 && c <= 0x10ffff && !(c >= 0xd800 && c <= 0xdfff)) return;
flan_say(loc, loclen, flan_say(loc, loclen,

View File

@ -2,7 +2,8 @@
;;;; Bytes that are not UTF-8, reached through a str, stop the program at the ;;;; 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 ;;;; append; so does a code point with no encoding; a character position past
;;;; the end signals BoundsError counted in characters; and a text builder ;;;; 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. ;;;; test asserts the line and column of each.
(defonce bad [2 u8]) (defonce bad [2 u8])
@ -18,6 +19,7 @@
(= which 2) (insert s 3 "x") (= which 2) (insert s 3 "x")
(= which 3) (println (remove s 2)) (= which 3) (println (remove s 2))
(= which 5) (println (to-lower (slice bad))) (= 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)))) :else (append s (bytes->string (let [v (vec-new u8)] (push v 0xff) v))))
(println s)) (println s))
0) 0)

View File

@ -2051,16 +2051,21 @@ let () =
arg (match x86 with Some true -> ", --x86" | _ -> "") arg (match x86 with Some true -> ", --x86" | _ -> "")
text code want text code want
end) 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"); is 0xc3");
("1", "string-traps.flan:17:19: 55296 is not a Unicode scalar value"); ("1", "string-traps.flan:18:19: 55296 is not a Unicode scalar value");
("2", "string-traps.flan:18:19: index 3 is out of bounds for length 2"); ("2", "string-traps.flan:19: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"); ("3", "string-traps.flan:20:28: index 2 is out of bounds for length 2");
(* The builder's own check is made at the call, not inside the (* A builder called by name is checked at the call, before it runs. *)
prelude. *) ("5", "string-traps.flan:21:28: this text is not valid UTF-8 — byte 0 \
("5", "string-traps.flan:20:28: this text is not valid UTF-8 — byte 0 \
is 0xc3"); 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", "<prelude>:");
("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") ]; is 0xff") ];
(try Sys.remove exe with Sys_error _ -> ()) (try Sys.remove exe with Sys_error _ -> ())
in in