diff --git a/FIX.org b/FIX.org index f0153b5..17f6851 100644 --- a/FIX.org +++ b/FIX.org @@ -952,6 +952,24 @@ Interned and immortal — flan_dyn.c's intern table holds the only copy of each name, nothing removes one, and [mark_value] walks BOX_OBJ and nothing else. There is no GC object to attribute. +*** Dyn push and put are not marked. +Added 2026-09-20, from a review: it had only ever been in a test comment. +[flan_dyn_push] and [flan_dyn_map_set] are not in [Check.memory_class]'s +table and they provably may allocate — a dyn vector or map growing itself is +[gc_alloc] on the collector's heap, the same class every other gc row names. +This is the one row the precision rule does not decide; it is a judgement. +The unit this pass reports is a line the programmer can act on — crossing +into dyn is a choice, pushing onto an allocator's Vec is a choice — and a dyn +container taking a block to hold what was just put in it is the only thing it +could do. Marking it would squiggle every =(push dv x)= in a program that +chose dyn, which is the noise the rule exists to keep out. Pinned as a +negative in test_flan.ml's "collected heap" row, beside the typed push that +IS marked on the line above it. + +The consequence is that the daemon's =:note= cannot claim "every site the +checker can prove may allocate", and no longer does: lib/dev.ml's memory op +says what holds and names this exception. + *** The overlays outlive the next command. The spec asked for the paths that clear an error overlay. Those hang off [pre-command-hook], which takes an overlay down before the next keystroke — @@ -1077,7 +1095,14 @@ that two mentions of one site share a pointer. Sixty-four sites, and past that it stops deduplicating rather than stops warning — the noisy failure, not the silent one. The line is: - flan FILE:LINE:COL: (f64 x) found a dyn holding an int, and converted it to f64 — warned once for this site + FILE:LINE:COL: (f64 x) found a dyn holding an int, and converted it to f64 — warned once for this site + +The bare =FILE:LINE:COL:= is the house shape for a loc-bearing runtime +diagnostic — flan_rt.c's bounds, divide-by-zero and null-allocator sentences +all open that way, and the =flan:= prefix is reserved for the lines that carry +no location (the leak report at flan_dev.c:1765, the argv failure at +flan_rt.c:179). An earlier draft of this warning wore =flan= in front of the +location; it was taken off to match the neighbours. Both builds warn, dev and release. No precedent was found making a diagnostic of this kind dev-only: the allocation registry's notes are the one runtime @@ -1125,3 +1150,70 @@ sand.flan defines =dyn->f64= and =dyn->u32=, one-line functions whose only job is that their parameter slot unboxes. Every call site can now write the cast directly — =(f64 d)=, =(u32 d)= — and the two defns deleted. Not done here: sand.flan is the author's WIP and this lane did not touch it. + +* Follow-ups from the 2026-09-20 reviews +Small, verified findings the reviews turned up after their lanes had landed. +Each was re-checked against the tree before it was written or fixed. + +** runtime/flan_dyn_stub.c is dead, and the author should decide its fate +RECOMMENDATION: delete it. Not done here — it is a file the author added and +removing it is his call, so the facts are written down instead. + +*** What it was for, in its own words +Its header says it plainly: "a standing-in implementation of the flan_dyn.h +ABI ... THE MERGE REPLACES THIS FILE WITH runtime/flan_dyn.c. It exists so +that the compiler side of dynamic-by-default can be built and run against the +fixed ABI before the real runtime lands." The merge it names happened. The +real runtime is =runtime/flan_dyn.c=, and lib/dune pastes *that* file — not +this one — into Runtime_src (lib/dune:41, :52). + +*** Why it is dead +- No dune rule mentions it, in lib/dune, runtime/ or test/dune. +- No .ml refers to it; no test links it; =flan build= never compiles it. +- The only mentions anywhere are two historical citations in docs — + docs/SPIKE-DUPLICITY.md:58 cites a line number in it, and + docs/handoffs/HANDOFF-dyn-m1.md:131 explains that the stub verified nothing + about root discipline. Both are narrative about a period that has ended; + neither gives the file a live job. + +*** It does not compile +Two conflicting-type errors against its own header, both pre-existing and +neither caught by anything, because nothing builds it: + + clang -c runtime/flan_dyn_stub.c -Iruntime + flan_dyn_stub.c:90: flan_dyn flan_dyn_from_bool(int32_t v) + vs flan_dyn.h:68: flan_dyn flan_dyn_from_bool(uint8_t b); + flan_dyn_stub.c:293: int32_t flan_dyn_need_bool(flan_dyn v) + vs flan_dyn.h:145: uint8_t flan_dyn_need_bool(flan_dyn v); + +So the one thing it could still be — a second implementation the header is +diffed against — is a thing it has already stopped being. + +*** The cost of keeping it +It is maintained by accident: the dyn-cast lane added [flan_dyn_cast_kind] to +it (flan_dyn_stub.c:333) alongside the real one. That is a duplicity the +doctrine does not ask for — the same side of the same capability, written +twice — and the copy is the one no test can reach. This batch deliberately did +NOT carry the warning-prefix change below into it, so the two now disagree. + +** The cast warning wears the house prefix +See "The warning is once per SITE" above. The =flan= in front of the location +came off; a loc-bearing runtime diagnostic opens with a bare =FILE:LINE:COL:= +everywhere else in the runtime. + +** Where the memory classifier overrode the spec: dyn push and put +Written into the memory-diagnostics decision above, where its siblings live: +see "Dyn push and put are not marked" under "Where this overrode the spec, +and the evidence". It had only ever been in a test comment. + +** Two stale "kept honest by" claims, corrected +lib/build.ml's note beside the header write and test/dyn_ops.c's own header +both said dyn_ops.c calls every function runtime/flan_dyn.h declares. It does +not, and the corrected header made that visible: [flan_dyn_cast_kind], +[flan_dyn_is_nil], [flan_dyn_need_not_nil], [flan_dyn_map_get], +[flan_dyn_map_set] and [flan_dyn_map_contains] are declared and never called +there. The check the include buys is real but narrower than the claim: for a +function dyn_ops.c *calls*, the call is compiled against the header and the +symbol has to resolve against flan_dyn.o, so a rename, a removal or a changed +argument list is a compile or link error in =dune test=. A function nothing +here calls gets neither. Both comments now say that instead. diff --git a/emacs/MANUAL.md b/emacs/MANUAL.md index 3c4ecad..1644d47 100644 --- a/emacs/MANUAL.md +++ b/emacs/MANUAL.md @@ -595,10 +595,21 @@ what it should call, and the message shape is what it should parse: :command ("flan" "check" "--warn-memory" source-original) :error-patterns ((warning line-start (file-name) ":" line ":" column - ": warning: " (message) line-end)) + ": warning: " (message) line-end) + (error line-start (file-name) ":" line ":" column + ": " (message) line-end)) :modes flan-mode) ``` +**Both patterns, and in that order.** A rejection is not labelled: `flan check` +prints `file:line:col: message` and exits 1, so a checker with only the warning +pattern reports "checker returned non-zero but no errors" on every real type +error — the one case you most want it for. The error pattern is second because +flycheck takes the first that matches a line, and the warning line would +otherwise land in the error bucket with `warning: ` glued to the front of its +message. The squiggle lines under each diagnostic and the closing `1 error` are +matched by neither, which is fine. + Only the file named on the command line is reported, so the prelude's own pushes — real, and none of your business — stay out of it. diff --git a/emacs/flan.el b/emacs/flan.el index 92cb2dc..31bcdf4 100644 --- a/emacs/flan.el +++ b/emacs/flan.el @@ -2766,18 +2766,29 @@ can print the same breakdown to stderr under FLAN_DEV_LEAKS." (overlays-in (point-min) (point-max))))) (defun flan-clear-memory (&optional buffer) - "Remove the allocation annotations from BUFFER, or from the current buffer." + "Remove the allocation annotations from BUFFER. +Called with no BUFFER, which is what running the command does, it takes +them down everywhere instead: every buffer that has them. One +request paints every buffer visiting a file the answer names, so the marks +are one reading spread over several buffers and not a per-buffer thing; +clearing only the one point happens to be in would leave the rest of that +reading up. This is the same sweep the toggle in `flan-check-memory' does." (interactive) - (with-current-buffer (or buffer (current-buffer)) - (remove-overlays (point-min) (point-max) 'flan-memory t) - (remove-hook 'after-change-functions #'flan--clear-memory-on-change t))) + (dolist (b (if buffer (list buffer) (flan--marked-buffers))) + (with-current-buffer b + (remove-overlays (point-min) (point-max) 'flan-memory t) + (remove-hook 'after-change-functions #'flan--clear-memory-on-change t)))) (defun flan--clear-memory-on-change (_beg _end _len) "Take this buffer's allocation annotations down, as an `after-change-functions'. They are a reading of the source as it was when you asked, and an edit is what makes that reading stale — nothing smaller does, which is why this is -not the `pre-command-hook' the error overlays use." - (flan-clear-memory)) +not the `pre-command-hook' the error overlays use. + +This one is deliberately per-buffer where the command is not: editing one +file stales that file's reading, and the marks still standing in the others +are still true." + (flan-clear-memory (current-buffer))) (defun flan--marked-buffers () "Every buffer that currently has allocation annotations in it. diff --git a/lib/build.ml b/lib/build.ml index f76bce3..e0628e0 100644 --- a/lib/build.ml +++ b/lib/build.ml @@ -698,8 +698,14 @@ let compile_c ~opts ?tflags ?(warn = []) ~src ~name () = flan_dyn.c does *not* include it. The object cache is keyed on the source text, so a header edit would serve an object compiled against the - previous one, and the two copies of the declarations are kept honest by - test/dyn_ops.c naming every function instead. *) + previous one. What keeps the two copies of the declarations honest is + test/dyn_ops.c, which includes this header and links against flan_dyn.c: + every function it *calls* is compiled against the header and has to + resolve against the object, so a rename, a removal or a changed argument + list is a compile or link error in [dune test]. That is not the whole + header — six entry points are declared and never called there, listed in + dyn_ops.c's own comment — so it is a check with a known edge, not a + proof. *) write (Filename.concat dir "flan_dyn.h") Runtime_src.dyn_header; write c src; (* A distinct temporary target, renamed into place, so two builds running diff --git a/lib/check.ml b/lib/check.ml index 87f2457..0bd25c3 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1418,11 +1418,20 @@ let restart_sig tys = let dyn_i64 = Types.Int Types.I64 let dyn_f64 = Types.Float Types.F64 -(* Widening to the one width the ABI carries. runtime/flan_dyn.h boxes integers - as [i64] and floats as [f64] and offers no other width, which is the - language's "dyn integers are i64" written where it is enforced. The cast is - explicit in the tree rather than left to the backend: a [Cast] is what the - language's own conversions emit, and a widening one loses nothing. *) +(* Converting to whatever width the other side of the boundary wants, with a + [Cast] and not a silent reinterpretation. The name is for the direction it + was written for: runtime/flan_dyn.h boxes integers as [i64] and floats as + [f64] and offers no other width, so *into* a box this only ever widens, and + a widening cast loses nothing. + + Coming back *out* it is used in both directions, and that is deliberate: + [cast_dyn] below unboxes to [i64]/[f64] and then hands the value to this to + reach the cast's target, which may be narrower ([(i32 d)]) or a different + kind ([(f32 d)]). Nothing is lost quietly there either — the [Cast] emitted + is the same node [(i32 x)] on a typed value emits, so the narrowing rule, + the fptosi range check and NaN are the emitter's, identical to the typed + spelling. This helper picks the node; it does not promise the conversion is + free. *) let widen loc (want : Types.t) (e : Tast.expr) = if Types.equal want e.Tast.ty then e else mk loc want (Tast.Prim (Tast.Cast want, [ e ])) @@ -8530,6 +8539,15 @@ let no_gc (p : Tast.program) = integer type provably cannot. - A keyword is interned and immortal — [flan_dyn_kw]'s entry is not a GC object and the collector never traces one — so it is not named here. + - A dyn container growing itself is not named, and this one is a judgement + rather than a fact about the runtime: [flan_dyn_push] and + [flan_dyn_map_set] provably may [gc_alloc], and they are still left out. + The unit this pass reports is a line the programmer can act on — crossing + into dyn is a choice, pushing onto an allocator's Vec is a choice — and a + dyn vector taking a block to hold what was just put in it is the only + thing it could do. Marking it would squiggle every [(push dv x)] in a + program that chose dyn. Written down in FIX.org, because it is the one + row here that the precision rule alone does not decide. - Dyn arithmetic is not named. [flan_dyn_add] and its siblings end in [flan_dyn_from_i64], so a wide enough result spills, but nothing static knows the operands and a squiggle on every [(+ a b)] over dyn is the diff --git a/lib/dev.ml b/lib/dev.ml index b5d4b9a..b3d6709 100644 --- a/lib/dev.ml +++ b/lib/dev.ml @@ -3038,9 +3038,12 @@ let memory_op t ~file = Printf.sprintf ":count %d" (List.length ds); ":note " ^ Wire.quote - "every site the checker can prove allocates, and every one it can \ - prove may; a dyn immediate — nil, a bool, an f64, a keyword, an \ - int inside the payload — is not one and is not listed" ] + "a site listed here allocates, or says in its first two words that \ + it may; a dyn immediate — nil, a bool, an f64, a keyword, an int \ + inside the payload — is not one and is not listed. Not every \ + allocation the checker could prove: a dyn container growing itself \ + on a push or a put is deliberately silent, being the container \ + doing the only thing it can. See FIX.org" ] let handle t req = match Wire.string_field req "op" with diff --git a/lib/emit.ml b/lib/emit.ml index f6261c7..c76dbe4 100644 --- a/lib/emit.ml +++ b/lib/emit.ml @@ -4301,7 +4301,7 @@ let redefinition ?(checks = true) ?(dev = false) ?(debug = false) host's marker is the only part that matters. *) Buffer.add_string m.out (Printf.sprintf "%s = external global i64\n%s = hidden global ptr %s\n\n" - abi_marker_sym ("@" ^ quoted "flan.abi.require") abi_marker_sym); + abi_marker_sym ("@" ^ quoted Mangle.abi_require) abi_marker_sym); (* The cells are the host's, like the globals. Referencing one is how a redefined function reaches its siblings, and storing into one is how it replaces itself. A name the host lacks gets a slot instead, filled by diff --git a/lib/mangle.ml b/lib/mangle.ml index 3300e2c..fa4be4d 100644 --- a/lib/mangle.ml +++ b/lib/mangle.ml @@ -12,11 +12,13 @@ Flan name holds -, ?, > and /, which is why every emitted name is quoted at all. This module only decides *which string* is quoted. - Not here: the ABI marker. [Emit.abi_marker] is ["flan.abi.llvm"] and + Not here: the ABI marker itself. [Emit.abi_marker] is ["flan.abi.llvm"] and [X86.abi_marker] is ["flan.abi.x86"], and the two must stay distinct — a crossed pair is refused at [dlopen] precisely because the marker one image defines is not the one the other references. Sharing that string - would delete the mechanism. *) + would delete the mechanism. The *label* a module hangs its requirement on + is the other half of that mechanism and is shared, so it is here: see + [abi_require] below. *) (* The prefix itself. It keeps the Flan [main] from colliding with C's, and it is what makes every Flan symbol recognisable in a disassembly. *) @@ -40,3 +42,11 @@ let globalptr n = prefix ^ "gp." ^ n (* A compiled macro's entry point, which the expander dlsyms by this name out of the module [Build.macro_module] wrote. *) let macro n = prefix ^ "macro." ^ n + +(* The datum a redefinition module puts its host's ABI marker into. Nothing + outside the module names it — the relocation against the marker is the + whole of what it does — but both backends emit it, so the string is spelled + once here rather than twice, beside every other name that has to read the + same on both sides. What it *holds* is each backend's own marker, and that + pair stays distinct; see the paragraph at the top. *) +let abi_require = prefix ^ "abi.require" diff --git a/lib/x86.ml b/lib/x86.ml index f32b12b..c585400 100644 --- a/lib/x86.ml +++ b/lib/x86.ml @@ -4893,7 +4893,7 @@ let redefinition ~checks ?(dev = true) ?(known = fun _ -> true) relocation against the marker matters. *) Buffer.add_string out (Printf.sprintf "\n\t.data\n\t.align\t8\n%s:\n\t.quad\t%s\n" - (asm_sym "flan.abi.require") (asm_sym abi_marker)); + (asm_sym Mangle.abi_require) (asm_sym abi_marker)); (* Nothing outside this module refers to anything in it once the call has returned -- no cell holds an address in its text, the registry has no slot for it, and the value it produced was copied out. So it says so, and the diff --git a/runtime/flan_dyn.c b/runtime/flan_dyn.c index 3a4436f..34afd76 100644 --- a/runtime/flan_dyn.c +++ b/runtime/flan_dyn.c @@ -1174,10 +1174,29 @@ uint8_t flan_dyn_need_bool(flan_dyn v) { * number of cross-kind cast sites a program has, which is a handful in the * programs this was written for. A program with more than [SITE_MAX] of them * stops deduplicating for the overflow — it still warns, every time, which - * is the noisy failure rather than the silent one. Not thread-safe, and - * deliberately: a duplicated or dropped line under a race is a diagnostic - * that came out twice, and the alternative is a lock on a path that runs per - * cast in a frame loop. */ + * is the noisy failure rather than the silent one. + * + * What the table stores is the loc's pointer, never a copy — the same licence + * the allocation registry takes for its type names (flan_dev.c:1073-1075). + * The bytes are a string constant in the image of whatever module emitted the + * cast, and a module that emitted a string constant is never unloaded: the + * cell table forbids dlclose outright (flan_dev.c:27), and the one path that + * does unload — an expression thunk — is gated on the module having emitted + * no string literal at all ([nstr] in lib/emit.ml:383-391). A cast site's loc + * IS a string literal, emitted through [string_const] like any other, so a + * module holding one of these sites is on the never-unloaded side of that + * test. If that ever stops being true the table has to copy. + * + * Not thread-safe, and that is a statement about who runs this rather than a + * shrug: [flan_dyn_cast_kind] runs on the program's own thread and Flan has + * no second one today. The dev agent's listener thread reads flan_dev.c's + * tables — which is why *those* carry a seqlock — and never touches this one. + * Were a second thread ever to reach a cast, the cost would not be a line + * printed twice: {ptr, len} is a pair only meaningful together, and a reader + * that took the new pointer with the old length would read off the end of a + * string literal, exactly the hazard flan_dev.c:1126-1129 describes. The fix + * then is the registry's, not a lock on a path that runs per cast in a frame + * loop. */ #define SITE_MAX 64 @@ -1216,7 +1235,7 @@ int32_t flan_dyn_cast_kind(flan_dyn v, const uint8_t *loc, int64_t loc_len, if (is_float != (want_float ? 1 : 0) && site_first_time(loc, loc_len)) { fflush(stdout); fprintf(stderr, - "flan %.*s: (%.*s x) found a dyn holding %s, and converted it to " + "%.*s: (%.*s x) found a dyn holding %s, and converted it to " "%.*s — warned once for this site\n", (int)loc_len, (const char *)loc, (int)target_len, (const char *)target, is_float ? "a float" : "an int", diff --git a/test/dyn_ops.c b/test/dyn_ops.c index 9450f29..09e715d 100644 --- a/test/dyn_ops.c +++ b/test/dyn_ops.c @@ -5,13 +5,22 @@ * there is no program that could reach it. The .flan this links against * therefore has no [main] of its own; see programs/dyn-host.flan. * - * This file includes runtime/flan_dyn.h and calls every function the header + * This file includes runtime/flan_dyn.h and calls most of what the header * declares. That is not tidiness — the build compiles flan_dyn.c on its own * with no include path, so the implementation declares its own prototypes and * the header is a second copy of them. Including it *here* is what makes a * divergence between the two a compile or link error in `dune test` rather * than a surprise in the compiler lane's emitted code. * + * "Most", not "every", and the gap is worth knowing: the check only covers a + * function this file calls. flan_dyn_cast_kind, flan_dyn_is_nil, + * flan_dyn_need_not_nil, flan_dyn_map_get, flan_dyn_map_set and + * flan_dyn_map_contains are declared in the header and reached from nowhere + * here, so nothing compares their two declarations. Each is lowered by + * lib/check.ml and so is exercised by the Flan programs the acceptance tests + * run — a check on the behaviour, not on the header. Adding a call for each + * is the way to close it. + * * One mode per run, chosen by argv, because most of the modes end in a trap * and a trap ends the process. The happy paths share one run; each refusal * gets its own.