JosephFerano/flan
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

--no-gc is a pass, not a flag the emitter can see

Browse Source 
The promise is that this program carries no collector, and the way to keep it is
to refuse every dyn rather than to emit a different program: a dyn value is one
the runtime allocates and the collector owns, and there is no smaller version to
fall back to. So it runs between checking and emission, answers unit or raises,
and hands the very same program on. Emit has no field to branch on and is told
nothing.

That is what makes the byte-identity claim true rather than approximate, and it
is tested by compiling three annotated programs twice and comparing the text. A
field, a mode, or a comment that mentioned the flag would break it on something
incidental, a long way from anything to do with dyn.

Every site is named, the way the global cycle refusal names the whole ring: a
reader who has to annotate their program wants the list, not the first one and
then another compile. Globals and signatures as well as body values -- the two
files it is tested against report nine sites each, and the floors are set under
that so an added line does not fail the test and a pass that named one site and
stopped would.

The four programs run at -O2 and -O0. dyn-boundary is asserted on its exit
status as well as its output, because the boundary is only interesting in that
it can fail and a test that showed it working would be testing the easy half.
The x86 survey skips them by name: a REFUSED there means a node that backend has
stopped lowering, which is a regression, and this is the opposite -- a lane that
has not started. Take a name off llvmonly when the lowering arrives and the
survey will say whether it works. 128 match, 0 differ, 0 refused.

Checked while writing these: a dyn function with an early return pops its roots
on both paths, and one with a defer pops on the transfer path too.
This commit is contained in:
Joseph Ferano 2026-09-19 06:33:28 +07:00
parent 9f2f0b1635
commit 7c7586ebc6
6 changed files with 319 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
bin/main.ml
View File

@ -195,9 +195,17 @@ let llvm_flag = "--llvm"
assembler is worth measuring rather than asserting. *)
let no_annotate_flag = "--no-annotate"
(* "This program carries no collector", and the way it is kept is a refusal
rather than a different lowering: every dyn left in the program is named,
with its location, and nothing downstream is told the flag was given. See
[Check.no_gc], which is a pass between checking and emission and answers
unit — an annotated program's output is byte for byte what it is without
the flag, and that is the property the flag is worth having for. *)
let no_gc_flag = "--no-gc"
let flags =
[ no_checks_flag; dev_flag; debug_flag; sanitize_flag; two_process_flag;
x86_flag; llvm_flag; no_annotate_flag ]
x86_flag; llvm_flag; no_annotate_flag; no_gc_flag ]
(* Which backend a command got, from the two flags and the default it would
have taken. One function because there is one rule, and the only thing that
@ -616,8 +624,12 @@ let () =
with_errors path (fun () ->
let l = load path in
let pnames = if debug then param_names l else [] in
Flan.Check.program_all l.decls
|> Flan.Emit.program ~checks ~dev ~debug ~pnames ~sanitize
let p = Flan.Check.program_all l.decls in
(* Between checking and emission, and it hands the very same program
on: the flag is a question asked of what was checked, never a
parameter of what is emitted. *)
if List.mem no_gc_flag args then Flan.Check.no_gc p;
Flan.Emit.program ~checks ~dev ~debug ~pnames ~sanitize p
|> print_string))
files
| _ :: "build" :: path :: rest ->
@ -654,12 +666,17 @@ let () =
prerr_endline
"usage: flan build <file.flan> [-o out] [-O0|-O1|-O2|-O3] \
[--no-bounds-checks] \
[--dev] [--debug] [--sanitize] [--target=wasm32-wasi|web|js]";
[--dev] [--debug] [--sanitize] [--no-gc] [--target=wasm32-wasi|web|js]";
exit 2
in
with_errors path (fun () ->
let l = load path in
let p = Flan.Check.program_all l.decls in
(* Before reachability rather than after: a dyn in a function nothing
calls is still a dyn somebody wrote, and a refusal that depended on
what [main] happened to reach would come and go as the program was
edited elsewhere. *)
if List.mem no_gc_flag rest then Flan.Check.no_gc p;
(* The link follows the program, not the import list: a package nothing
reachable calls into contributes no C and no linker argument, and its
functions are not emitted either. That is what lets one file import

67
lib/check.ml
View File

@ -7080,3 +7080,70 @@ let expression env (e : Ast.expr) :
let t = check ctx e in
(t, Array.of_list (List.rev ctx.slot_tys),
Array.of_list (List.rev ctx.slot_names))
(* ── --no-gc ────────────────────────────────────────────────────────────
The flag that says this program is to be compiled with no collector in it,
and the way to keep that promise is to refuse every dyn rather than to emit
a different program. A dyn value is a value the runtime allocates and the
collector owns; there is no smaller version of it to fall back to, and
quietly leaking instead would be a memory model nobody asked for.
So this is a pass and not a flag. It runs between [Check] and [Emit], it
answers unit or it refuses, and nothing downstream of it is told the flag
exists — which is what makes a fully annotated program's output byte for
byte identical with the flag and without it. Emit has no [no_gc] field to
branch on, and that is deliberate: a field would be one more thing that
could change a comment, a name or an ordering, and the identity is worth
more than the branch would ever buy.
Every site is named, the way the global cycle refusal names the whole ring
rather than one member of it. A reader who has to annotate their program
wants the list, not the first one and then another compile. *)
let dyn_sites (p : Tast.program) : Loc.diag list =
let found = ref [] in
let add loc what = found := (loc, what) :: !found in
List.iter
(fun (g : Tast.global) ->
if g.Tast.gty = Types.Dyn then
add g.Tast.ginit.Tast.loc (Printf.sprintf "the global %s" g.Tast.gname))
p.Tast.globals;
List.iter
(fun (fn : Tast.fn) ->
List.iteri
(fun i t ->
if t = Types.Dyn then
add fn.Tast.floc
(Printf.sprintf "parameter %d of %s" (i + 1) fn.Tast.name))
fn.Tast.params;
if fn.Tast.ret = Types.Dyn then
add fn.Tast.floc (Printf.sprintf "the return type of %s" fn.Tast.name);
(* The body's own dyn values, which are the ones a signature does not
show: a let bound to a boxed literal, a (vec-new dyn) deep inside an
expression. Reported at the node, because that is the character to
change. *)
List.iter
(Tast.walk
(fun (e : Tast.expr) ->
match e.Tast.e with
| Tast.Prim (Tast.Rt sym, _)
when e.Tast.ty = Types.Dyn
&& String.length sym > 8
&& String.sub sym 0 8 = "flan_dyn" ->
add e.Tast.loc (Printf.sprintf "this value in %s" fn.Tast.name)
| _ -> ()))
fn.Tast.body)
p.Tast.fns;
List.rev_map
(fun (loc, what) ->
Loc.diag ~kind:"check/no-gc" loc
(Printf.sprintf
"%s is dyn, and --no-gc says this program carries no collector. A \
dyn value is one the runtime allocates and the collector owns, so \
there is nothing smaller to compile it to — write the type"
what))
!found
let no_gc (p : Tast.program) =
match dyn_sites p with [] -> () | ds -> raise (Loc.Errors ds)

10
spike/x86/survey.sh
View File

@ -78,6 +78,15 @@ out=$(mktemp -d); trap 'rm -rf "$out"' EXIT
# truncations are both empty.
forever="dev-loop dev-watch dev-chatty"
# The dyn programs, which this backend refuses by name and is meant to: every
# operation on a dyn value is a call into the dynamic runtime and x86.ml emits
# none of them. They are listed rather than left to be counted as refusals
# because a REFUSED here means "a node this backend has stopped lowering",
# which is a regression, and this is the opposite -- a lane that has not
# started. Take a name off this list when the backend grows the lowering, and
# the survey will say whether it works.
llvmonly="dyn-basic dyn-vec dyn-global dyn-boundary"
TIMEOUT=${TIMEOUT:-20}
# Extra flags, given to *both* sides. SURVEY_FLAGS=--dev is the one that has a
@ -101,6 +110,7 @@ for src in "$corpus"/test/programs/*.flan "$corpus"/spike/x86/*.flan \
[ $want = 1 ] || continue
fi
case " $forever " in *" $name "*) skip+=("$name:runs-forever"); continue;; esac
case " $llvmonly " in *" $name "*) skip+=("$name:dyn-is-llvm-only"); continue;; esac
# LLVM first. A program that does not compile at all, or has no main, is not
# this backend's business -- the frontend refused it either way.

42
test/programs/dyn-boundary.flan Normal file
View File

@ -0,0 +1,42 @@
;;;; The boundary in both directions, and the trap when a claim is wrong.
;;;;
;;;; Typed to dyn is implicit: take-dyn is called with an i64 and the boxing is
;;;; written nowhere. Dyn to typed is not: take-i64's parameter says i64, and
;;;; that annotation is the whole of why the unboxing is allowed to happen —
;;;; and the whole of why it may fail, which the last line of main proves by
;;;; handing it a float.
;;;;
;;;; A let carries no type in this language, so the annotation sites a dyn can
;;;; be unboxed at are the ones that do: a parameter, a return type, and a
;;;; global's declared type. All three are here.
(defvar seven i64 7)
(defvar boxed dyn 21)
;; The other direction at a global: a dyn initialiser meeting a written type.
(defvar unboxed i64 boxed)
(defn take-dyn [d dyn] dyn
(+ d 100))
(defn take-i64 [n i64] i64
(* n 2))
(defn identity-dyn [d] dyn d)
;; A dyn value answered at a written return type, which is the third site.
(defn as-i64 [d] i64 d)
(defn main [] ()
;; Typed in: the i64 is boxed at the call with nothing written.
(print (take-dyn seven))
(print "\n")
;; Dyn out: the parameter is typed, so the word is unboxed at the call.
(print (take-i64 boxed))
(print "\n")
(print unboxed)
(print "\n")
(print (as-i64 (identity-dyn 5)))
(print "\n")
;; And the claim that is wrong. The runtime owns the message.
(print (take-i64 (identity-dyn 1.5)))
(print "\n"))

132
test/test_acceptance.ml
View File

@ -2967,6 +2967,138 @@ level "1"
outputs ~opt:"-O0" "unions, -O0" "programs/unions.flan" unions_out;
outputs ~dev:true "unions, dev" "programs/unions.flan" unions_out;
(* ── dyn, milestone 1 ────────────────────────────────────────────
Four programs, and between them every claim the feature makes that can
be run rather than argued.
[dyn-basic] is the one the feature exists for: a defn that annotates
nothing, called at two types, answering correctly to both. Nothing the
typed language can express does that.
[dyn-vec] is the heterogeneous container, which is where a dynamic
language stops being a convenience and starts being a different data
model — four types in one vector, read back out one at a time.
[dyn-global] is the case that needed the startup function: a call is not
a constant, so a dyn global is a computed global, and it turned out to
need no new machinery at all.
[dyn-boundary] is the one with a trap in it, and it is asserted on its
exit status and its message: the boundary is only interesting because it
can fail, and a test that only showed it working would be testing the
easy half. It is at -O2 and -O0 like the rest, because the unboxing is a
call whose result feeds a machine instruction and that is exactly the
shape the optimiser could launder away.
They are LLVM-only, and the [@x86] survey skips them by name — see
[llvmonly] in spike/x86/survey.sh. Not compiled by the dev backend, so
not run as dev builds either. *)
let dyn_basic_out = "5\n3.75\n" in
outputs "dyn: an unannotated defn at two types"
"programs/dyn-basic.flan" dyn_basic_out;
outputs ~opt:"-O0" "dyn: an unannotated defn at two types, -O0"
"programs/dyn-basic.flan" dyn_basic_out;
let dyn_vec_out = "4\n[1 2.5 three true]\n1 2.5 three true \n" in
outputs "dyn: a heterogeneous vector"
"programs/dyn-vec.flan" dyn_vec_out;
outputs ~opt:"-O0" "dyn: a heterogeneous vector, -O0"
"programs/dyn-vec.flan" dyn_vec_out;
let dyn_global_out = "0 start\n2 done\n" in
outputs "dyn: a global" "programs/dyn-global.flan" dyn_global_out;
outputs ~opt:"-O0" "dyn: a global, -O0"
"programs/dyn-global.flan" dyn_global_out;
(* The boundary, both directions, and then the claim that is wrong. The
first four lines are the conversions; the trap is the fifth, and the
runtime owns its wording — the compiler could only have said that two
dyns did not agree, which is what they are for. *)
let dyn_boundary ?opt () =
let exe = compile ?opt "programs/dyn-boundary.flan" in
let code, text = run exe None in
let want = "107\n42\n21\n5\n" in
let name =
"dyn: the boundary both ways, and the trap"
^ (match opt with Some o -> ", " ^ o | None -> "")
in
if code <> 134
|| not (contains text want)
|| not (contains text "required to be an i64")
then begin
incr failures;
Printf.printf
"FAIL %s\n got: %S (exit %d)\n wanted: %S then a trap \
(exit 134)\n"
name text code want
end;
(try Sys.remove exe with Sys_error _ -> ())
in
dyn_boundary ();
dyn_boundary ~opt:"-O0" ();
(* ── --no-gc ─────────────────────────────────────────────────────
The flag is a pass between checking and emission that answers unit or
refuses, and these are its two halves.
Every dyn is named. Not the first one and then another compile: a reader
who has to annotate their program wants the list, which is why the pass
collects and raises [Loc.Errors] the way the global cycle refusal does.
Asserted on the count as well as on the text, because "it refused" would
pass just as well if it named one site and stopped. *)
let no_gc_sites path least =
let l = Load.program ~file:path (Reader.read_file path) in
let p = Check.program_all l.Load.decls in
match Check.no_gc p with
| () ->
incr failures;
Printf.printf "FAIL --no-gc on %s: it was accepted\n" path
| exception Loc.Errors ds ->
if List.length ds < least then begin
incr failures;
Printf.printf
"FAIL --no-gc on %s: named %d sites, wanted at least %d\n"
path (List.length ds) least
end;
List.iter
(fun (d : Loc.diag) ->
if not (contains d.Loc.dmsg "carries no collector") then begin
incr failures;
Printf.printf "FAIL --no-gc on %s: said %S\n" path d.Loc.dmsg
end)
ds
in
(* The vec file reports nine: a vec-new, four boxed pushes, a len, an at
and the dotimes bound. The floor is under that rather than equal to it
so an added line does not fail the test, and well over one so that a
pass which named the first site and stopped would. *)
no_gc_sites "programs/dyn-vec.flan" 8;
(* The global file reports nine too, and the point of it is the mix: two
[the global ...] sites and two [the return type of ...] ones, which a
walk over function bodies alone would never have found. *)
no_gc_sites "programs/dyn-global.flan" 6;
(* The other half, and the reason the flag is a pass and not a parameter of
[Emit]: a program with nothing to refuse compiles to the same bytes with
the flag and without it. If [--no-gc] were ever plumbed into the emitter
— a field, a mode, a comment that mentioned it — this is what would
start failing, and it would fail on something incidental rather than on
anything to do with dyn. *)
let identical path =
let l = Load.program ~file:path (Reader.read_file path) in
let p = Check.program_all l.Load.decls in
let a = Emit.program p in
Check.no_gc p;
let b = Emit.program p in
if a <> b then begin
incr failures;
Printf.printf
"FAIL --no-gc changed the IR of %s (%d bytes vs %d)\n"
path (String.length a) (String.length b)
end
in
identical "programs/algorithms.flan";
identical "programs/conditions.flan";
identical "programs/unions.flan";
(* The refusals, each by name. The first is the diagnostics bug NEXT.md
listed and this lane fixed: a case name written as if it were a struct
reported "unknown struct A", because nothing in the environment could

47
test/test_flan.ml
View File

@ -866,6 +866,53 @@ let () =
rejects_check "an unknown concrete type" "(defn f [x Widget] ())"
~needle:"unknown type Widget";
(* ── dyn, and what it does not do yet ──────────────────────────── *)
(* The pairing rule's own refusal. A name that is also a type's has no good
reading — taken as written it is a parameter called [i64] — and the
likelier intent is a pair the wrong way round, which the message names. *)
rejects_check "a parameter named after a type" "(defn f [i64 x] ())"
~needle:"cannot also be this parameter's name";
(* The three "not yet" refusals, each by name and each for its own reason.
A typed container does not box: [(Vec i64)] has a representation the dyn
runtime cannot walk, and the heterogeneous container at this milestone is
the runtime's own from [(vec-new dyn)]. *)
rejects_check "a typed container boxed into dyn"
"(defn take [d dyn] i32 1)\n\
(defn main [] i32 (take [1 2 3]))"
~needle:"does not cross into dyn yet";
(* A condition crosses a handler boundary as a pointer to a live frame, and
a dyn payload has to stay rooted across that transfer — the collector's
question, and milestone 2's. *)
rejects_check "a dyn in a condition's payload"
"(defstruct Boom [what dyn])\n\
(defn main [] () (signal (Boom {.what 1})))"
~needle:"milestone 2";
(* And the C boundary, which is the one that would otherwise pass silently:
a dyn is one word and would cross as an integer, and nothing on the other
side can ask what the word means. *)
rejects_check "a dyn crossing to C"
"(declare c-take [d dyn] () \"c_take\")"
~needle:"does not cross to C";
(* The x86 backend refuses dyn by name, and the sentence has to be good: the
dev daemon takes that backend by default, so this is the first thing a
user of dyn sees. Neither half of the message names [--llvm] — Session and
main.ml each add that, differently and for their own reasons — so what is
pinned here is the half this file owns. *)
(match
X86.program ~checks:true
(Check.program_all
(program "(defn add [x y] dyn (+ x y))\n\
(defn main [] () (print (add 1 2)))"))
with
| _ -> check "the x86 backend refuses dyn" false
| exception X86.Unsupported m ->
check "the x86 backend refuses dyn by name"
(contains m "a dyn value" && contains m "dynamic runtime"));
(* ── Static bounds ─────────────────────────────────────────────── *)
(* A literal index into a fixed array is known now, so it is an error now
rather than a trap later; everything else is the emitted bounds check's