diff --git a/bin/main.ml b/bin/main.ml index 032fe0e..1b3193e 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -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 [-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 diff --git a/lib/check.ml b/lib/check.ml index 50be294..a8bf82a 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -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) diff --git a/spike/x86/survey.sh b/spike/x86/survey.sh index 85ac83d..919ae80 100755 --- a/spike/x86/survey.sh +++ b/spike/x86/survey.sh @@ -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. diff --git a/test/programs/dyn-boundary.flan b/test/programs/dyn-boundary.flan new file mode 100644 index 0000000..9556c0e --- /dev/null +++ b/test/programs/dyn-boundary.flan @@ -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")) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 78aab49..69f2e82 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -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 diff --git a/test/test_flan.ml b/test/test_flan.ml index 817e0bd..cd0041d 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -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