A u64 past the largest i64 traps where it crosses into dyn, a dyn nil past a fold's first pair traps at run time, and an is-numeric $t boxes beside a dyn.

This commit is contained in:
Joseph Ferano 2026-09-26 16:47:28 +07:00
parent 3a2f3327f6
commit 7dcef05df3
8 changed files with 204 additions and 36 deletions

View File

@ -800,14 +800,6 @@ One spelling for one operation; != stays, and not= is refused with a suggestion
of !=.
* Checker
** TODO A u64 above the i64 maximum becomes -1 when it crosses into dyn
=(+ z u)= and =(max u 0 z)= with u = u64 max read u as -1, silently. It should trap at
the crossing, as a u64 field read through a view already does.
** TODO A dyn nil past the first pair of a fold is refused at compile time
=(+ 1 2 (the dyn nil))= says nil has no None at i32, while =(+ (the dyn nil) 1 2)= traps
at run time. Both should trap at run time.
** TODO A generic $t beside a dyn operand is refused
"does not cross into a written type yet"; rule 117 says typed beside dyn gives dyn.
** WAIT Checking a wide fold of let operands is slow
Parked 2026-09-26: design first; remeasure on a quiet machine, it was timed under load 20.
A 2000-operand (bit-and (let …) …) takes 32 s to check (37 s before the bit operators);

View File

@ -4415,6 +4415,10 @@ let box ?ctx loc (e : Tast.expr) : Tast.expr =
(* Dyn text is immutable and a String is not, so a String crosses as a copy
of its bytes rather than as the view any other struct would be. *)
| t when is_string_ty t -> dyn "flan_dyn_from_string" [ string_vec loc e ]
(* A dyn int is an i64, so a u64 past the largest i64 has none to become:
read as its bits it would be a different, negative number. It traps
here, at the crossing, as one read through a view does. *)
| Types.Int Types.U64 -> dyn "flan_dyn_from_u64" [ e; here loc ]
| Types.Int _ -> dyn "flan_dyn_from_i64" [ widen loc dyn_i64 e ]
| Types.Float _ -> dyn "flan_dyn_from_f64" [ widen loc dyn_f64 e ]
(* The ABI takes an [int32_t], because a C signature that says [_Bool] is a
@ -4435,6 +4439,28 @@ let box ?ctx loc (e : Tast.expr) : Tast.expr =
Loc.failk "check/dyn-unit" loc
"() does not box into dyn. The absent dyn value is nil — write nil"
| Types.Never -> e
(* A [$t] is seen only in a generic's abstract pass; each copy is checked
again at its concrete type, where the value boxes as that type does, and
this node is thrown away with the rest of the pass. Admitting it is sound
only when every type the variable can be at crosses, or a refusal would
move from the definition to whichever call instantiates it at a pointer,
an enum or a function, with no written requirement to blame — the rule
beside [println]'s deferral. Every [is-numeric] type crosses (a u64 past
the largest i64 traps at run time, not at a copy's check), so that bound
admits it. [is-ordered] and [is-equal] do not: both admit an enum, which
has no dyn value. The node is a cast rather than [flan_dyn_nil] because
[is_nil_lit] would read that as a nil literal. *)
| Types.Var v
when (match ctx with
| Some c -> declares c.env.tvpreds v "is-numeric"
| None -> false) ->
mk loc Types.Dyn (Tast.Prim (Tast.Cast Types.Dyn, [ e ]))
| Types.Var _ ->
let t = tyname loc e.Tast.ty in
Loc.failk "check/dyn-type-variable" loc
"%s may be a type with no dyn value, such as a pointer or an enum, so \
it crosses into dyn only as a number. Write %s at the head of the body"
t (where_text loc "is-numeric" t)
(* A view, not a copy: the box holds a small record naming where the
storage is and what one element is (its descriptor, [view_desc]), and
every read or write goes straight through to the container's own
@ -4522,7 +4548,7 @@ let box ?ctx loc (e : Tast.expr) : Tast.expr =
caller that starts doing that gets a sentence instead of a silent
mis-lowering. *)
| Types.Named _ | Types.Enum _ | Types.Option _ | Types.Ptr _
| Types.Alloc | Types.Fn _ | Types.CFn _ | Types.Var _ | Types.Len _
| Types.Alloc | Types.Fn _ | Types.CFn _ | Types.Len _
| Types.LArray _ | Types.Vec _ | Types.Array _ | Types.Slice _ ->
no_dyn_yet loc ~into:true e.Tast.ty ""
@ -6812,9 +6838,9 @@ and wide_literal loc ~want n s =
| Some Types.Dyn ->
Loc.failk literal_at_want loc
"expected dyn, found the integer literal %s, which only a u64 holds — a \
dyn integer is an i64. Write (u64 %s) for the u64, which a dyn holds as \
the i64 with the same bits, %Ld"
s s n
dyn integer is an i64, and no i64 is this large. Give what holds it \
the type u64"
s
| Some other ->
Loc.failk literal_at_want loc
"expected %s, found the integer literal %s, which only a u64 holds"
@ -11820,7 +11846,7 @@ and fold_left_prim ctx ~want loc name p ~needs ok what args =
| `Typed v -> steps (mk loc acc.Tast.ty (Tast.Prim (p, [ acc; v ]))) tl
| `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
else
match fold_operand ctx acc.Tast.ty (check ctx ~want:acc.Tast.ty arg) with
match fold_arg ctx acc.Tast.ty arg with
| `Typed v -> steps (mk loc acc.Tast.ty (Tast.Prim (p, [ acc; v ]))) tl
| `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
in
@ -11847,7 +11873,7 @@ and fold_left_prim ctx ~want loc name p ~needs ok what args =
let rec steps acc = function
| [] -> expect ctx loc ~want acc
| arg :: tl ->
match fold_operand ctx ty (check ctx ~want:ty arg) with
match fold_arg ctx ty arg with
| `Typed v -> steps (mk loc ty (Tast.Prim (p, [ acc; v ]))) tl
| `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
in
@ -11865,6 +11891,26 @@ and fold_operand ctx ty (v : Tast.expr) =
| Some d -> `Dyn d
| None -> `Typed v
(* An operand past a fold's first pair, from the source: at the type so far,
and on its own terms only when that is refused, as [binary_pair] checks
the second of the pair. A dyn it turns out to be joins the fold as a dyn,
so (+ 1 2 (the dyn nil)) traps at run time as (+ (the dyn nil) 1 2) does
instead of being refused for a nil with no value at i32, and a dyn beside
a [$t] is not opened at the variable. Anything else is checked at the type
again, for real, so its refusal is the one it always gave and recovery
records it. *)
and fold_arg ctx ty (arg : Ast.expr) =
match trial_at ctx arg ty with
| Ok v -> fold_operand ctx ty v
| Error _ ->
let own () =
let v = check ctx arg in
if v.Tast.ty = Types.Dyn then v else fail arg.Ast.loc "not a dyn"
in
match trial ctx own with
| Ok v -> `Dyn v
| Error _ -> fold_operand ctx ty (check ctx ~want:ty arg)
(* A pair an arithmetic operator refused, when one operand is a char: that
is the refusal to give, rather than the mismatch between the two. Asked
only after the refusal, so a pair that checks costs nothing more. *)
@ -11976,10 +12022,10 @@ and dyn_fold ctx ~want loc name first rest =
language's type error, and until now it printed with no file, no line and
no column — [here loc] is the same string literal [cast_dyn] hands the
runtime, and the runtime prints it as a GNU prefix. *)
let apply acc b = rt loc Types.Dyn sym [ acc; box loc b; here loc ] in
let apply acc b = rt loc Types.Dyn sym [ acc; box ~ctx loc b; here loc ] in
let acc =
match first with
| [ a; b ] -> apply (box loc a) b
| [ a; b ] -> apply (box ~ctx loc a) b
| _ -> assert false
in
let operand arg =
@ -13464,15 +13510,15 @@ and named_call ?(qualified = false) ctx ~want loc name args =
in
let r =
match rest with
| [] -> link (box loc a) (box loc b)
| [] -> link (box ~ctx loc a) (box ~ctx loc b)
| _ -> cmp_over ctx loc Types.Dyn ~pairs ~link (ops ())
in
expect ctx loc ~want r
in
if a.Tast.ty = Types.Dyn || b.Tast.ty = Types.Dyn then
dyn_chain (fun () ->
box loc a :: box loc b
:: map_lr (fun e -> box loc (check ctx ~want:Types.Dyn e)) rest)
box ~ctx loc a :: box ~ctx loc b
:: map_lr (fun e -> box ~ctx loc (check ctx ~want:Types.Dyn e)) rest)
else begin
(* [=] and [!=] admit types [<] does not. A handle is one: a pair of
numbers in one word and where being the same entity is the question the
@ -13508,14 +13554,14 @@ and named_call ?(qualified = false) ctx ~want loc name args =
| _ ->
let ty = a.Tast.ty in
let link u v = mk loc Types.Bool (Tast.Prim (p, [ u; v ])) in
let rest = map_lr (fun e -> fold_operand ctx ty (check ctx ~want:ty e)) rest in
let rest = map_lr (fold_arg ctx ty) rest in
(* A dyn past the first pair makes the whole chain the dyn runtime's,
for [fold_operand]'s reason: a chain is its pairs, and a pair with a
dyn in it is a dyn comparison. *)
if List.exists (function `Dyn _ -> true | `Typed _ -> false) rest then
dyn_chain (fun () ->
box loc a :: box loc b
:: List.map (function `Dyn d -> d | `Typed v -> box loc v) rest)
box ~ctx loc a :: box ~ctx loc b
:: List.map (function `Dyn d -> d | `Typed v -> box ~ctx loc v) rest)
else
let ops =
a :: b :: List.map (function `Typed v -> v | `Dyn d -> d) rest in
@ -13598,7 +13644,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
if v.Tast.ty <> Types.Dyn then bits_operand ctx v.Tast.loc name v)
[ a; b ];
expect ctx loc ~want
(rt loc Types.Dyn (dyn_bits_sym name) [ box loc a; box loc b; here loc ])
(rt loc Types.Dyn (dyn_bits_sym name) [ box ~ctx loc a; box ~ctx loc b; here loc ])
end else begin
bits_operand ctx loc name a;
(* A shift by the operand's own width or more is poison in LLVM, which at
@ -13663,7 +13709,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
let rec steps acc = function
| [] -> expect ctx loc ~want acc
| arg :: tl ->
match fold_operand ctx ty (check ctx ~want:ty arg) with
match fold_arg ctx ty arg with
| `Typed v -> steps (pick acc v) tl
| `Dyn d -> dyn_fold ctx ~want loc name [ acc; d ] tl
in
@ -20745,6 +20791,9 @@ let memory_class (sym : string) (args : Tast.expr list) =
| "flan_dyn_from_i64" when (match args with [ x ] -> int_may_spill x | _ -> true) ->
gc "may allocate: an i64 outside ±2^47 does not fit a dyn's payload and \
spills onto the collector's heap"
| "flan_dyn_from_u64" when (match args with x :: _ -> int_may_spill x | [] -> true) ->
gc "may allocate: a u64 above 2^47 does not fit a dyn's payload and \
spills onto the collector's heap"
(* ── An allocator the program named ── *)
| "flan_arena_new" ->
native "allocates: an arena takes its whole region from the host here"

View File

@ -5067,6 +5067,7 @@ declare void @flan_alloc_set_budget(ptr, i64)
; ever looks inside one, so every operation on a dyn value is one of these.
declare i64 @flan_dyn_nil()
declare i64 @flan_dyn_from_i64(i64)
declare i64 @flan_dyn_from_u64(i64, ptr, i64)
declare i64 @flan_dyn_from_f64(double)
declare i64 @flan_dyn_from_bool(i32)
declare i64 @flan_dyn_from_bytes(ptr, i64)

View File

@ -1909,6 +1909,26 @@ flan_dyn flan_dyn_from_i64(int64_t x) {
return dyn_make(BOX_OBJ, (uint64_t)(uintptr_t)o);
}
/* A u64 has a dyn int to become only up to the largest i64; past it the trap
* names the number, which read as an i64 would be a different one. [what] is
* "u64" for a scalar crossing and "u64 element" for one read through a view,
* so both say the same sentence. */
static flan_dyn u64_to_dyn(const uint8_t *loc, int64_t loclen, const char *op,
const char *what, uint64_t x) {
if (x > (uint64_t)INT64_MAX) {
flan_say(loc, loclen,
"dyn%s%s: this %s is %llu, above the largest dyn int "
"(9223372036854775807), so it has no dyn value",
op[0] ? " " : "", op, what, (unsigned long long)x);
dyn_trap((const uint8_t *)"DynRange", 8);
}
return flan_dyn_from_i64((int64_t)x);
}
flan_dyn flan_dyn_from_u64(uint64_t x, const uint8_t *loc, int64_t loclen) {
return u64_to_dyn(loc, loclen, "", "u64", x);
}
flan_dyn flan_dyn_from_f64(double x) {
flan_dyn v;
/* Every NaN becomes the one positive quiet NaN, which is what keeps a
@ -4046,14 +4066,7 @@ static flan_dyn view_read(const uint8_t *loc, int64_t loclen, const char *op,
case 'L': {
uint64_t x;
memcpy(&x, p, 8);
if (x > (uint64_t)INT64_MAX) {
flan_say(loc, loclen,
"dyn %s: this u64 element is %llu, above the largest dyn int "
"(9223372036854775807), so it has no dyn value",
op, (unsigned long long)x);
dyn_trap((const uint8_t *)"DynRange", 8);
}
return flan_dyn_from_i64((int64_t)x);
return u64_to_dyn(loc, loclen, op, "u64 element", x);
}
case 'f': { float x; memcpy(&x, p, 4); return flan_dyn_from_f64((double)x); }
case 'd': { double x; memcpy(&x, p, 8); return flan_dyn_from_f64(x); }

View File

@ -86,6 +86,8 @@ typedef struct flan_desc {
flan_dyn flan_dyn_nil(void);
flan_dyn flan_dyn_from_i64(int64_t x);
/* Traps at [loc] on a u64 above the largest i64, which no dyn int holds. */
flan_dyn flan_dyn_from_u64(uint64_t x, const uint8_t *loc, int64_t loclen);
flan_dyn flan_dyn_from_f64(double x);
flan_dyn flan_dyn_from_bool(uint8_t b);

View File

@ -0,0 +1,59 @@
;;;; Typed values crossing into dyn beside a dyn operand: a u64, a dyn nil past
;;;; a fold's first pair, and a $t bounded by is-numeric. With an argument, the
;;;; program runs the trap that argument names instead.
(defn add-dyn [x $t] dyn
{:where (is-numeric $t)}
(+ x (the dyn 1)))
(defn add-late [x $t d dyn] dyn
{:where (is-numeric $t)}
(+ x 1 d))
(defn dyn-first [x $t d dyn] dyn
{:where (is-numeric $t)}
(* d x 2))
(defn less-late [x $t d dyn] bool
{:where (is-numeric $t)}
(< x 10 d))
(defn biggest [x $t d dyn] dyn
{:where (is-numeric $t)}
(max x d 0))
(defn low-bits [x $t d dyn] dyn
{:where (is-integer $t)}
(bit-and x 7 d))
(defn boxed [x $t] dyn
{:where (is-numeric $t)}
(the dyn x))
(defn main [args [str]] i32
(let [z (the dyn 0)
n (the dyn 4)
small (the u64 9223372036854775807)
big (the u64 18446744073709551615)
nothing (the dyn nil)]
;; A u64 up to the largest i64 crosses as its value.
(println (+ z small) (max small 0 z) (the dyn small) (= small (+ z small)))
;; A $t at i32, f64 and u64, beside a dyn in any position.
(println (add-dyn 2) (add-dyn 2.5) (add-dyn (the u64 7)))
(println (add-late 2 n) (add-late 2.5 n) (dyn-first 3 n) (dyn-first 1.5 n))
(println (less-late 1 n) (less-late 1 (the dyn 20)) (less-late 0.5 (the dyn 10.5)))
(println (biggest 3 n) (biggest -2.5 (the dyn -1)) (low-bits 13 n) (low-bits (the u8 255) n))
(println (boxed 7) (boxed 0.25) (boxed small))
;; A nil past the pair is compared, not refused.
(println (= 1 1 nothing) (!= 1 2 nothing) (= 1 1 (the dyn nil)))
(when (> (length args) 1)
(let [a (at args 1)]
(when (= a "u64") (println (+ z big)))
(when (= a "u64-max") (println (max big 0 z)))
(when (= a "u64-generic") (println (boxed big)))
(when (= a "nil-first") (println (+ (the dyn nil) 1 2)))
(when (= a "nil-last") (println (+ 1 2 (the dyn nil))))
(when (= a "nil-less") (println (< 1 2 (the dyn nil))))
(when (= a "nil-min") (println (min 1 2 nil)))
(when (= a "nil-bits") (println (bit-or 1 2 nothing))))))
0)

View File

@ -5665,6 +5665,46 @@ level "1"
(if x86 then ", --x86" else "") text code
end)
[ false; true ];
(* A u64, a dyn nil past the pair and an is-numeric $t, each beside a
dyn: the typed value crosses, and what cannot cross traps at its site. *)
let crossing_out =
"9223372036854775807 9223372036854775807 9223372036854775807 true\n\
3 3.5 8\n7 7.5 24 12\nfalse true true\n4 0 4 4\n\
7 0.25 9223372036854775807\nfalse true false\n"
in
outputs "dyn: typed values crossing beside a dyn" "programs/dyn-crossing.flan"
crossing_out;
outputs ~opt:"-O0" "dyn: typed values crossing beside a dyn, -O0"
"programs/dyn-crossing.flan" crossing_out;
outputs ~x86:true "dyn: typed values crossing beside a dyn, --x86"
"programs/dyn-crossing.flan" crossing_out;
let too_big = "dyn: this u64 is 18446744073709551615, above the largest \
dyn int (9223372036854775807), so it has no dyn value" in
let crossing_traps =
[ "u64", "51:36", too_big;
"u64-max", "52:40", too_big;
"u64-generic", "31:12", too_big;
"nil-first", "54:42", "dyn +: nil and int, and it takes two numbers — (+ nil 1)";
"nil-last", "55:41", "dyn +: int and nil, and it takes two numbers — (+ 3 nil)";
"nil-less", "56:41", "dyn <: int and nil";
"nil-min", "57:40", "dyn min: int and nil";
"nil-bits", "58:41", "dyn bit-or: int and nil" ]
in
List.iter
(fun x86 ->
let exe = compile ~x86 "programs/dyn-crossing.flan" in
List.iter
(fun (arg, at, msg) ->
let code, text = run exe (Some arg) in
let want = "programs/dyn-crossing.flan:" ^ at ^ ": " ^ msg in
if code <> 134 || not (contains text want) then begin
incr failures;
Printf.printf "FAIL dyn: crossing trap %s%s\n \
got: %S (exit %d)\n"
arg (if x86 then ", --x86" else "") text code
end)
crossing_traps)
[ false; true ];
List.iter
(fun x86 ->
let exe = compile ~x86 "programs/char-arith.flan" in

View File

@ -2066,6 +2066,18 @@ let () =
rejects_check "nil at a bare T is refused at compile time"
"(defn take [n i32] i32 n)\n(defn main [] i32 (take nil))"
~needle:"nil has no None to become";
(* A $t crosses into dyn only under a bound every type of which has a dyn
value; an unbounded one could be a pointer, refused at no call site. *)
rejects_check "an unbounded $t does not cross into dyn"
"(defn f [x $t] dyn (+ x (the dyn 1)))\n\
(defn main [] i32 (println (f 2)) 0)"
~needle:"$t may be a type with no dyn value, such as a pointer or an \
enum, so it crosses into dyn only as a number. Write \
{:where (is-numeric $t)}";
rejects_check "an is-ordered $t does not cross into dyn"
"(defn f [x $t] dyn {:where (is-ordered $t)} (the dyn x))\n\
(defn main [] i32 (println (f 2)) 0)"
~needle:"crosses into dyn only as a number";
rejects_check "nil at a bare T is refused at compile time, return position"
"(defn f [] i64 nil)\n(defn main [] i32 0)"
~needle:"nil has no None to become";
@ -8018,11 +8030,11 @@ let () =
parse_rejects "a wide enum member is refused for its range"
"(defenum E [A 0xFFFFFFFFFFFFFFFF B])"
~needle:"the member A of E is 0xFFFFFFFFFFFFFFFF, which does not fit i32";
rejects_check "a wide literal in a dyn global names the u64 cast"
rejects_check "a wide literal in a dyn global names the type u64"
"(defonce big 0xFFFFFFFFFFFFFFFF)"
~needle:"Write (u64 0xFFFFFFFFFFFFFFFF) for the u64";
accepts "the cast the dyn refusal names compiles"
"(defonce big (u64 0xFFFFFFFFFFFFFFFF))";
~needle:"no i64 is this large. Give what holds it the type u64";
accepts "the type the dyn refusal names compiles"
"(defonce big u64 0xFFFFFFFFFFFFFFFF)";
(* A macro's Form has one integer case; the literal comes back wide all the
same, and is refused where it would have been refused unexpanded. *)
rejects_check "a wide literal through a macro is still wide"