Two kinds of defconst, and only one of them is unreloadable
Refusing every defconst was right about the class and wrong about most of the instances. A constant the checker consumed - (defconst rows (/ h c)), which decides grid's type before anything else resolves - is in the shape of the program and no store can reach it. A constant that is only ever read at run time is just bytes in memory. sand's colors is the second kind, and tuning a colour table live is exactly the thing you would want a dev loop for. So a dev build emits every defconst as a mutable global rather than a constant. LLVM can then no longer fold a read of it and a module can store into it, and a changed one is published at the frame boundary the same way a new function body is. Release builds emit constant and get all the folding back. Tast.global.gfolded records which kind it is, because nothing downstream of the checker can tell: env.consts holds exactly the constants the folding pass consumed, and membership is the question "is this value in the program's shape?". The session keys its refusal on that, with a message that says what the constant is used for rather than just that it changed. Verified against a running sand: sim/colors is accepted, sim/rows is refused and says why.
This commit is contained in:
parent
7ce1d09900
commit
335e817676
11
NEXT.md
11
NEXT.md
@ -557,7 +557,7 @@ Two things the session knows that no single evaluation could:
|
||||
| a function's signature | a cell is a bare `ptr`; every call site compiled before the change still passes the old arguments through it |
|
||||
| a global's type | the storage exists and has a shape — reuse reads at the wrong offsets, replacement discards the state the reload exists to preserve |
|
||||
| a struct's fields | the values the process is holding have the old layout |
|
||||
| a `defconst`'s value | it is folded into every call site — into an array length, at worst, which is decided before any type resolves |
|
||||
| a `defconst`'s value, **when the checker consumed it** | it is in the *shape* of the program — `(defconst rows (/ h c))` decides `grid`'s type before anything else resolves — so no store can reach it |
|
||||
| a `defenum` member | `:space` is erased to an `i32` literal in the caller, so it is folded there too |
|
||||
|
||||
A `defvar`'s *initial value* is deliberately **not** in that table. Its
|
||||
@ -574,6 +574,15 @@ Two things the session knows that no single evaluation could:
|
||||
the program uses, which is exactly where the silent version lives. The
|
||||
fixtures carry an unused `defvar` and a C-called `defn` for that reason.
|
||||
|
||||
A `defconst` the checker never consumed is a different matter and **can** be
|
||||
changed: it is only ever bytes in memory. A dev build emits every `defconst` as
|
||||
a mutable `global` rather than a `constant` — so LLVM cannot fold a read of it
|
||||
and a module can store into it — and a changed one is published at the frame
|
||||
boundary exactly as a new function body is. That is how sand's `colors` gets
|
||||
tuned live while `rows` stays refused. Release builds emit `constant` and get
|
||||
all the folding back; `Tast.global.gfolded` is what tells the two apart, because
|
||||
nothing downstream of the checker could.
|
||||
|
||||
**A form typed into a file that is imported as a package is qualified the way
|
||||
the import qualified it.** `settle` in `sand-sim/sim.flan` becomes `sim/settle`,
|
||||
and its call to `move-grain` becomes `sim/move-grain` — through `Load`'s own
|
||||
|
||||
@ -1268,7 +1268,7 @@ let check_global env (d : Ast.decl) : Tast.global option =
|
||||
| Ast.Uninit -> { Tast.e = Tast.Uninit ty; ty; loc = d.Ast.dloc }
|
||||
| Ast.Init v -> check (ctx ()) ~want:ty v
|
||||
in
|
||||
Some { Tast.gname = n; gty = ty; ginit; gconst = false }
|
||||
Some { Tast.gname = n; gty = ty; ginit; gconst = false; gfolded = false }
|
||||
| Ast.Defconst (n, _, v) ->
|
||||
let ty, _ = Hashtbl.find env.globals n in
|
||||
(* [collect] already folded the integer constants, because an array length
|
||||
@ -1285,7 +1285,10 @@ let check_global env (d : Ast.decl) : Tast.global option =
|
||||
loc = d.Ast.dloc }
|
||||
| _ -> check (ctx ()) ~want:ty v
|
||||
in
|
||||
Some { Tast.gname = n; gty = ty; ginit; gconst = true }
|
||||
(* [env.consts] holds exactly the constants the folding pass consumed, so
|
||||
membership is the question "is this value in the program's shape?" *)
|
||||
Some { Tast.gname = n; gty = ty; ginit; gconst = true;
|
||||
gfolded = Hashtbl.mem env.consts n }
|
||||
| _ -> None
|
||||
|
||||
(* The entry point, plan.org: (defn main [args [string]] i32), with both the
|
||||
|
||||
24
lib/emit.ml
24
lib/emit.ml
@ -847,10 +847,15 @@ let rec const m (e : Tast.expr) =
|
||||
fail e.Tast.loc
|
||||
"a global's value must be a compile-time constant — this one is computed"
|
||||
|
||||
(* A dev build emits a [defconst] as a mutable [global]. Two things follow, and
|
||||
both are wanted: LLVM can no longer fold a read of it, and a redefinition
|
||||
module can store a new value into it — so tuning a constant live works,
|
||||
which it cannot when its only copy is immutable in .rodata. A release build
|
||||
emits [constant] and gets all the folding back. *)
|
||||
let emit_global m (g : Tast.global) =
|
||||
Buffer.add_string m.out
|
||||
(Printf.sprintf "%s = %s %s %s\n" (gname g.Tast.gname)
|
||||
(if g.Tast.gconst then "constant" else "global")
|
||||
(if g.Tast.gconst && not m.dev then "constant" else "global")
|
||||
(ll g.Tast.gty) (const m g.Tast.ginit))
|
||||
|
||||
(* ── Program ───────────────────────────────────────────────────────── *)
|
||||
@ -992,7 +997,7 @@ let program ?(checks = true) ?(dev = false) (p : Tast.program) : string =
|
||||
String literals still have to come along: they are this module's own
|
||||
constants, and omitting them is an undefined [@.str.N] at link time. *)
|
||||
let redefinition ?(checks = true) ?(dev = false) ?(known = fun _ -> true)
|
||||
?call (p : Tast.program) ~fns : string =
|
||||
?call ?(consts = []) (p : Tast.program) ~fns : string =
|
||||
let target name =
|
||||
match List.find_opt (fun (f : Tast.fn) -> f.Tast.name = name) p.Tast.fns with
|
||||
| Some f -> f
|
||||
@ -1010,7 +1015,8 @@ let redefinition ?(checks = true) ?(dev = false) ?(known = fun _ -> true)
|
||||
Buffer.add_string m.out
|
||||
(if known g.Tast.gname then
|
||||
Printf.sprintf "%s = external %s %s\n" (gname g.Tast.gname)
|
||||
(if g.Tast.gconst then "constant" else "global") (ll g.Tast.gty)
|
||||
(if g.Tast.gconst && not dev then "constant" else "global")
|
||||
(ll g.Tast.gty)
|
||||
else
|
||||
Printf.sprintf "%s = internal global ptr null\n"
|
||||
(globalptr g.Tast.gname)))
|
||||
@ -1086,6 +1092,18 @@ let redefinition ?(checks = true) ?(dev = false) ?(known = fun _ -> true)
|
||||
t (cstring m ("flan." ^ g.Tast.gname)) (ll g.Tast.gty) init t
|
||||
(globalptr g.Tast.gname)))
|
||||
new_globals;
|
||||
(* A constant whose value the checker never consumed is just bytes in the
|
||||
program's memory, so a new value is published the same way a new body
|
||||
is: one store, at the frame boundary. One the checker *did* consume is
|
||||
in the shape of the program and never gets here — the session refuses
|
||||
it. *)
|
||||
List.iter
|
||||
(fun (g : Tast.global) ->
|
||||
if List.exists (String.equal g.Tast.gname) consts then
|
||||
Buffer.add_string b
|
||||
(Printf.sprintf " store %s %s, ptr %s\n" (ll g.Tast.gty)
|
||||
(const m g.Tast.ginit) (gname g.Tast.gname)))
|
||||
p.Tast.globals;
|
||||
List.iter
|
||||
(fun (f : Tast.fn) ->
|
||||
if known f.Tast.name then
|
||||
|
||||
@ -156,13 +156,20 @@ let compatible ~loc (old_ : Tast.program) (new_ : Tast.program) =
|
||||
storage holds live state the program has long since moved past, which
|
||||
is the whole of "edit the code, keep the sand". Same record, opposite
|
||||
answers, told apart by [gconst]. *)
|
||||
(* Only a constant the *checker* consumed. Its value is in the shape of
|
||||
the running program — [(defconst rows (/ h c))] decides the type of
|
||||
[grid] before anything else resolves — so no store can reach it. A
|
||||
constant that is only ever read at run time is just bytes in memory:
|
||||
a dev build emits it as a mutable global and a redefinition stores
|
||||
the new value, which is how a colour table is tuned live. *)
|
||||
| Some h
|
||||
when h.Tast.gconst && g.Tast.gconst
|
||||
when h.Tast.gconst && g.Tast.gconst && h.Tast.gfolded
|
||||
&& Types.equal g.Tast.gty h.Tast.gty
|
||||
&& not (same_const g.Tast.ginit h.Tast.ginit) ->
|
||||
fail loc
|
||||
"%s changes value; the running program folded the old one into its \
|
||||
code, where a reload cannot reach it. Restart to change it."
|
||||
"%s is used at compile time — an array length or a type — so the \
|
||||
running program has its old value in its shape, where a reload \
|
||||
cannot reach it. Restart to change it."
|
||||
g.Tast.gname
|
||||
| Some h when not (Types.equal g.Tast.gty h.Tast.gty) ->
|
||||
(* The storage exists and has a shape. Reusing it for another one
|
||||
@ -310,7 +317,21 @@ let eval ?(origin = "<eval>") t src : change =
|
||||
program.Tast.fns)
|
||||
names
|
||||
in
|
||||
let ir = Emit.redefinition ~dev:true ~known:(known t) program ~fns in
|
||||
(* A constant that changed and can be published: known to the host, not
|
||||
consumed by the checker. The module stores its new value at the frame
|
||||
boundary, exactly as it stores a new function body. *)
|
||||
let consts =
|
||||
List.filter
|
||||
(fun n ->
|
||||
known t n
|
||||
&& List.exists
|
||||
(fun (g : Tast.global) ->
|
||||
String.equal g.Tast.gname n && g.Tast.gconst
|
||||
&& not g.Tast.gfolded)
|
||||
program.Tast.globals)
|
||||
names
|
||||
in
|
||||
let ir = Emit.redefinition ~dev:true ~known:(known t) ~consts program ~fns in
|
||||
let allocates =
|
||||
List.exists
|
||||
(fun (g : Tast.global) -> not (known t g.Tast.gname))
|
||||
@ -319,7 +340,7 @@ let eval ?(origin = "<eval>") t src : change =
|
||||
t.decls <- decls;
|
||||
t.program <- program;
|
||||
t.env <- env;
|
||||
{ ir; names; fns; installs = fns <> [] || allocates }
|
||||
{ ir; names; fns; installs = fns <> [] || allocates || consts <> [] }
|
||||
|
||||
(* ── Evaluating an expression ──────────────────────────────────────── *)
|
||||
|
||||
|
||||
13
lib/tast.ml
13
lib/tast.ml
@ -91,7 +91,18 @@ type fn = {
|
||||
floc : Loc.t;
|
||||
}
|
||||
|
||||
type global = { gname : string; gty : Types.t; ginit : expr; gconst : bool }
|
||||
(* [gfolded] is the difference between a constant whose value the *checker*
|
||||
consumed — an array length, decided before any type resolves — and one that
|
||||
is only ever read at run time. The first is in the program's shape and can
|
||||
never be reloaded; the second is just bytes in memory and can. Nothing else
|
||||
can tell them apart afterwards, so it is recorded here. *)
|
||||
type global = {
|
||||
gname : string;
|
||||
gty : Types.t;
|
||||
ginit : expr;
|
||||
gconst : bool;
|
||||
gfolded : bool;
|
||||
}
|
||||
|
||||
(* A foreign function: no body, and [esym] is the symbol the linker sees. The
|
||||
aggregate calling convention is not modelled here — a C shim flattens every
|
||||
|
||||
@ -23,6 +23,9 @@
|
||||
;;; either. Nothing here reads them, so the checker has no opinion and the
|
||||
;;; session's rule is the only thing that can speak.
|
||||
(defconst folded i64 7)
|
||||
;;; ...and one that is not: an array constant is never an array length, so its
|
||||
;;; value is only ever read at run time and a dev build can store a new one.
|
||||
(defconst palette [2 u32] [1 2])
|
||||
(defenum Colour [red 0 green 1])
|
||||
|
||||
(defn helper [x i64] i64 (* x 2))
|
||||
|
||||
@ -19,6 +19,10 @@ let has hay needle =
|
||||
|
||||
(* Every rejection is asserted on its reason, not just on the failure: the
|
||||
reason is the part that has to survive a refactor. *)
|
||||
let checked_program file =
|
||||
Check.program
|
||||
(Load.program ~file (Parse.program (Reader.read_file file))).Load.decls
|
||||
|
||||
let refuses ?(file = "programs/reload.flan") name src reason =
|
||||
let t, _ = Session.create ~file in
|
||||
match Session.eval t src with
|
||||
@ -49,12 +53,12 @@ let () =
|
||||
"(defvar spare i32)"
|
||||
"changes type";
|
||||
(* Values of the type are already in the running program's memory. *)
|
||||
(* A defconst is folded into its call sites — into an array length, at worst,
|
||||
which is decided before any type resolves — so its value lives in the
|
||||
program's code and not only in its storage. *)
|
||||
refuses "a changed defconst"
|
||||
(* A defconst the *checker* consumed is in the shape of the program — an
|
||||
array length is decided before any type resolves — so no store can reach
|
||||
it. One that is only read at run time is a different matter; see below. *)
|
||||
refuses "a changed defconst used at compile time"
|
||||
"(defconst folded i64 8)"
|
||||
"changes value";
|
||||
"used at compile time";
|
||||
(* An enum member is erased to an i32 literal in the caller, so the same
|
||||
applies. It is compared over declarations because Tast.program carries no
|
||||
enums at all, for exactly that reason. *)
|
||||
@ -96,6 +100,25 @@ let () =
|
||||
| c -> if c.Session.installs then fail "an empty change claimed to install"
|
||||
| exception Loc.Error (_, m) -> fail "redeclaring a var unchanged: %s" m);
|
||||
|
||||
(* A constant that is only ever read at run time is just bytes in the
|
||||
program's memory. A dev build emits it as a mutable global and the module
|
||||
stores the new value at the frame boundary, which is how a colour table
|
||||
gets tuned live. *)
|
||||
(match Session.eval t "(defconst palette [2 u32] [9 9])" with
|
||||
| c ->
|
||||
if not c.Session.installs then
|
||||
fail "a changed run-time constant had nothing to install";
|
||||
if not (has c.Session.ir "store [2 x i32]") then
|
||||
fail "a changed run-time constant published no new value"
|
||||
| exception Loc.Error (_, m) -> fail "changing a run-time constant: %s" m);
|
||||
(* And in a dev build its storage is writable, where a release build keeps
|
||||
it immutable and gets all the folding back. *)
|
||||
let host = checked_program "programs/reload.flan" in
|
||||
if not (has (Emit.program ~dev:true host) "@\"flan.palette\" = global") then
|
||||
fail "a dev build left a constant immutable";
|
||||
if not (has (Emit.program host) "@\"flan.palette\" = constant") then
|
||||
fail "a release build made a constant mutable";
|
||||
|
||||
(* A new global carries its declared initial value, copied once when the
|
||||
storage is allocated and never again — calloc alone would make it zero. *)
|
||||
let c = Session.eval t "(defvar started i64 42) (defn read-started [] i64 started)" in
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user