Joseph Ferano
3c1fb1b31e
Both directions of the boundary go through expect, the way every other dyn crossing does. A dyn's tag decides which case an (Option T) becomes on the way in; an Option's own tag decides nil or a boxed payload on the way out. box_option/unbox_option build the same If-over-a-tag shape get and map-remove already build for the same reason, reading an Option's tag and payload with the raw Field access Render's structural printer already uses — nothing new for either backend to lower. A literal Some/None skips the runtime check entirely, since the checker already knows which case it is. A bare T has no None to become. The literal nil the checker can see is refused right there, at compile time, in expect itself — the author's decision to do both halves rather than settle for the runtime trap alone. Everything one step removed from the syntax — a dyn that only turns out to be nil once the program runs — reaches flan_dyn_need_i64's existing DynType trap, unchanged; there is no dataflow in this checker for it to be otherwise (see "Ownership tracking repealed"). (Some nil) is refused the same way: the literal at compile time, with a message saying why nil and None would collide; a dyn that turns out to be nil only at run time through the new flan_dyn_need_not_nil, which traps by the same route flan_dyn_need_i64 does. (Option (Option T)) does not cross either direction — boxing Some of an inner None would box it as nil, indistinguishable from the outer None, the same ambiguity (Some nil) is refused for. The type itself stays legal on the typed side; only the crossing does not exist for it. (Option dyn) needs no case of its own in the boundary code — the payload is already dyn, so box_option/unbox_option treat it as the identity — but it is not yet a value a program can hold anywhere. The per-type-descriptor pass (M2 item 2) refuses it at every storage site today, the same way it refuses (Vec dyn), because a struct's dyn fields are marked by byte offsets and (Option dyn)'s payload has none. Item 4 does not lift that gate; it only makes the boundary already correct for the day items 2/3 do. expect grew a ctx parameter to build the fresh slot the two new crossings need — every call site threaded through, one context mismatch caught and fixed in check_fn's tail-expression case along the way. var's None case grew a direct Dyn arm: None at a dyn want is nil outright, with nothing to build. nil-option.flan carries the crossings that succeed and ends on the bare-T trap; some-nil.flan is (Some nil)'s run-time half, kept in its own file the way dyn-boundary.flan is one trap per program. Both are in no_fallback_slots and test_sanitize.ml: the new dyn temporary unbox_option's tag test mints is rooted, and reads its Option's tag and payload through ASan clean, --sanitize matching the unsanitized run byte for byte.
54 lines
2.2 KiB
Plaintext
54 lines
2.2 KiB
Plaintext
;;;; nil <-> None at (Option T) boundaries -- M2 queue item 4.
|
|
;;;;
|
|
;;;; nil is dyn's own absence and None is (Option T)'s; this is the boundary
|
|
;;;; where the checker decides they are the same absence. [absent] and
|
|
;;;; [opt-of] take it in at the two annotated sites that are not a function
|
|
;;;; argument -- a global's declared type and a return type; [via-param]
|
|
;;;; takes it in at the third, a parameter. [as-dyn] is the other direction:
|
|
;;;; a written (Option i64) crossing into dyn becomes nil or the boxed
|
|
;;;; payload. [box-it]/[unbox-opt] round-trip a value through both crossings.
|
|
;;;;
|
|
;;;; The last line is the trap: a dyn that is nil only once the program runs,
|
|
;;;; reaching a bare i64. The literal [nil] two lines above it would have been
|
|
;;;; refused at compile time instead -- see test_flan.ml and
|
|
;;;; test_acceptance.ml's "nil at a bare T, compile time" row for that half.
|
|
|
|
(defvar absent (Option i64) nil)
|
|
|
|
(defn opt-of [flag bool] (Option i64)
|
|
(if flag (Some 7) nil))
|
|
|
|
(defn via-param [o (Option i64)] i64
|
|
(match o (Some v) v None -1))
|
|
|
|
(defn as-dyn [o (Option i64)] dyn o)
|
|
|
|
(defn box-it [x i64] dyn x)
|
|
(defn unbox-opt [d dyn] (Option i64) d)
|
|
|
|
(defn maybe-nil [flag bool] dyn (if flag 5 nil))
|
|
(defn take-i64 [n i64] i64 n)
|
|
|
|
(defn show [o (Option i64)] ()
|
|
(print (match o (Some v) v None -1)) (println ""))
|
|
|
|
(defn main [] ()
|
|
;; nil -> None, at a global's declared type, a return type and a parameter.
|
|
(show absent) ; -1
|
|
(show (opt-of true)) ; 7
|
|
(show (opt-of false)) ; -1
|
|
(print (via-param nil)) (println "") ; -1
|
|
(print (via-param (Some 3))) (println "") ; 3
|
|
|
|
;; None -> nil, crossing into dyn; Some x -> the boxed x.
|
|
(print (= (as-dyn None) nil)) (println "") ; true
|
|
(print (as-dyn (Some 9))) (println "") ; 9
|
|
|
|
;; A value round-tripped through both crossings: typed -> dyn -> (Option T).
|
|
(show (unbox-opt (box-it 42))) ; 42
|
|
|
|
;; The trap: a dyn that turns out to be nil only when the program runs,
|
|
;; reaching a bare i64. flan_dyn_need_i64 owns the wording.
|
|
(print (take-i64 (maybe-nil false)))
|
|
(println ""))
|