Three ways to pass the checker and die afterwards

Found by a read-only audit of emit.ml's failwith sites, each of which is a claim
that the checker guarantees something. Three of those claims were false, and
every one failed in the shape NEXT.md calls the worst available: type checks,
then dies with no source location.

An enum comparison is lowered now rather than refused. Types.is_comparable
already admits an enum, so the checker was stating an intent the backend never
honoured - (= k :a) is the first thing anyone writes with an enum, and it raised
Failure("comparison on K"). An enum is an i32 at run time, so all six
operators are an icmp. Signed, because (defenum K [a -1]) is accepted and an
unsigned compare would call -1 the largest member.

A union in a type position is refused instead. Constructing a union value and
reading a field of one were already refused, so nothing could ever be done with
such a value - only the declaration got through, and it reached clang as a
reference to an undefined %"U", which is a link error naming an emitted symbol
with the source location long gone.

A function type annotation is refused too. The function *value* was refused
where it is written; the annotation was refused nowhere, so (defn f [g (Fn []
i32)]) died with "no layout for". It now sits beside the Map line directly
above it, which is the same shape of not-yet.

The audit also found the sentence that covered the last two: NEXT.md and
check.ml's header both claim unions and function values are rejected by name.
That is true of values and false of types, which is exactly the gap the two
findings lived in.
This commit is contained in:
Joseph Ferano 2026-09-11 20:21:33 +07:00
parent 1b2533b41e
commit 4f0b1012e8
4 changed files with 58 additions and 4 deletions

View File

@ -160,8 +160,11 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
| Ast.Tslice e -> Types.Slice (resolve env ~seen e)
| Ast.Tarray (l, e) -> Types.Array (array_len env loc l, resolve env ~seen e)
| Ast.Tmap _ -> unimplemented loc "the Map type" 6
| Ast.Tfn (ps, r) ->
Types.Fn (List.map (resolve env ~seen) ps, resolve env ~seen r)
(* The function *value* is refused where it is written; the annotation was
not refused anywhere, so [(defn f [g (Fn [] i32)])] type checked and then
died in emit with "no layout for". Refused here, beside the Map line
above, which is the same shape of not-yet. *)
| Ast.Tfn _ -> unimplemented loc "a function type" 5
| Ast.Tapp (name, args) ->
(match name, args with
| "Ptr", [ a ] -> Types.Ptr (resolve env ~seen a)
@ -223,8 +226,13 @@ and resolve_name env ~seen loc n =
if List.mem n seen then
fail loc "the type alias %s is defined in terms of itself" n
else resolve env ~seen:(n :: seen) (Hashtbl.find env.aliases n)
| _ when Hashtbl.mem env.structs n || Hashtbl.mem env.unions n ->
Types.Named n
| _ when Hashtbl.mem env.structs n -> Types.Named n
(* A union has no layout in emit — nothing there mentions unions at all —
so a union-typed global reached clang as a reference to an undefined
%"U". Constructing one and reading a field of one are already refused,
so there is nothing to lower: only a declaration that got through. *)
| _ when Hashtbl.mem env.unions n ->
unimplemented loc (Printf.sprintf "the union type %s" n) 6
| _ when Hashtbl.mem env.enums n -> Types.Enum n
(* A typo in a primitive is lowercase too, and the type-variable rule
below would otherwise report [f65] as unimplemented generics and send

View File

@ -834,6 +834,12 @@ and prim f (e : Tast.expr) (p : Tast.prim) (args : Tast.expr list) =
| Types.Int k ->
ins f "%s = icmp %s %s %s, %s" t (icmp_op (Types.signed k) p)
(ll x.Tast.ty) a b
(* An enum is an i32 at run time, and [Types.is_comparable] says so by
admitting one the checker was stating an intent the backend never
honoured, so [(= k :a)] type checked and then died here with no source
location. Signed, because a member may be declared negative. *)
| Types.Enum _ ->
ins f "%s = icmp %s %s %s, %s" t (icmp_op true p) (ll x.Tast.ty) a b
| t' -> failwith ("comparison on " ^ Types.to_string t'));
t
| (Tast.BitAnd | Tast.BitOr | Tast.BitXor | Tast.Shl | Tast.Shr), [ x; y ] ->

View File

@ -0,0 +1,27 @@
;;;; Comparing enums, which type checked and then died in the backend.
;;;;
;;;; Types.is_comparable admits an enum, so the checker was stating an intent
;;;; emit never honoured: (= k :a) passed check and then raised
;;;; Failure("comparison on K") with no source location. An enum is an i32 at
;;;; run time, so all six operators lower to icmp.
(defenum K [lo -1 mid 0 hi 1])
(defstruct S [k K])
(defn eq? [k K] bool (= k :mid))
(defn below? [k K] bool (< k :mid))
(defn main [] i32
;; Equality, both ways round.
(print-line (if (eq? :mid) "eq yes" "eq no"))
(print-line (if (eq? :hi) "eq yes" "eq no"))
;; Ordering, and signed: lo is -1, so an unsigned compare would call it the
;; largest member and answer the other way.
(print-line (if (below? :lo) "lo below mid" "lo not below mid"))
(print-line (if (below? :hi) "hi below mid" "hi not below mid"))
;; And through a struct field, which is a different path to the same compare.
(let [s (S {:k :hi})]
(print-line (if (= (.k s) :hi) "field eq yes" "field eq no")))
0)

View File

@ -698,6 +698,19 @@ ERR@7 unexpected token: not the kind the caller was reading
outputs "edn tokenizer" "programs/edn.flan" edn_out;
outputs ~opt:"-O0" "edn tokenizer, -O0" "programs/edn.flan" edn_out;
(* Comparing enums, found by auditing emit.ml's failwith sites. It type
checked and then died in the backend with no source location, which is
the project's worst failure shape. All six operators, a negative member
so that an unsigned compare would answer the other way, and a compare
through a struct field, which reaches the same lowering by another
path. *)
let enum_out =
"eq yes\neq no\nlo below mid\nhi not below mid\nfield eq yes\n"
in
outputs "enum comparison" "programs/enum-compare.flan" enum_out;
outputs ~opt:"-O0" "enum comparison, -O0" "programs/enum-compare.flan"
enum_out;
if !failures = 0 then print_endline "acceptance: all tests passed"
else begin
Printf.printf "\n%d failure(s)\n" !failures;