From 2ff1da88da6b948f5827480bafbcd999a5a5d1e1 Mon Sep 17 00:00:00 2001
From: Joseph Ferano
[n T] is inline storage
and copies on assignment and on pass-by-value.[T] is ptr+len and owns nothing.
- Copying a slice copies the view, never the elements.[const T] is the
+ same view with no stores through it.
(addr x) takes the address of
any assignable place and gives (Ptr T). It does not extend anything's
lifetime, and keeping one past its frame is your contract to honour — there is no
@@ -518,6 +519,7 @@ notation reads as exactly one data item.
booli1string[T][const T][T] converts to one, never the reverse[n T](Vec T)(Map K V)(defstruct Cursor
- [src [u8] ; a non-owning slice
+ [src [const u8] ; a read-only, non-owning slice
pos i32]) ; no initialiser means zeroed
(defn peek [c (Ptr Cursor)] u8
@@ -829,8 +831,8 @@ its bytes.
There are two ways to see a string's bytes and the difference is whether anything
is allocated. (bytes-view s) is the string's own storage seen as a
-[u8] and costs nothing; it aliases the string, so a literal's view points
-into .rodata and writing through it traps. (bytes s) and
+[const u8] and costs nothing; it aliases the string, and a store through
+it is a compile error. (bytes s) and
(bytes s allocator) make a writable copy through the allocator — never a
hidden malloc, which is the rule every allocating operation follows. The
example above wants a view and takes one.
From 7cf57eb8ba10d715396df549832005ea1951845d Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 11:49:17 +0700
Subject: [PATCH 02/13] A read-only slice refuses a dyn view without promising
one later, and taking a read-only element's address is recorded as an open
decision
---
TODO.org | 3 +++
lib/check.ml | 10 +++++-----
2 files changed, 8 insertions(+), 5 deletions(-)
diff --git a/TODO.org b/TODO.org
index 0d77b3b9..7a48a077 100644
--- a/TODO.org
+++ b/TODO.org
@@ -948,6 +948,9 @@ deliberate absence.
CLOSED: [2026-09-25]
=[const T]=; a =[T]= converts at the top of a type or under another const slice, never inside a writable one. =(addr (at v i))= of a read-only element is allowed, since a =(Ptr T)= is the C boundary and has no const form; a store is what is refused.
+** TODO The address of a read-only element is taken without complaint
+=(addr (at v i))= over a =[const T]= answers a writable =(Ptr T)=, so =slice-from-ptr= launders one back into a =[T]=; a string's byte refuses the same =addr=. Allowed because raylib's =load-image-from-memory= and =get-codepoint-previous= have no other way to hand a =[const u8]= to C. Decision needed: a const pointer type, or a refusal plus another route to C.
+
** TODO (slice d 1) over a dyn string is refused where (at d i) works
The typed and dyn spaces disagree about a spelling, which the standing rule
forbids. A dyn slice should exist.
diff --git a/lib/check.ml b/lib/check.ml
index 652612ad..89648d89 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -2563,11 +2563,11 @@ let box loc (e : Tast.expr) : Tast.expr =
dyn side can tell a read-only one apart, so a [[const T]] does not
cross. *)
| Types.Slice (Types.Const, elem) ->
- no_dyn_yet loc ~into:true e.Tast.ty
- (Printf.sprintf
- ": a dyn view can be written through, and a [const %s] can only be \
- read. A dyn view is taken of the writable storage it came from"
- (Types.to_string elem))
+ Loc.failk "check/dyn-const-view" loc
+ "%s does not cross into dyn: a dyn view can be written through, and a \
+ [const %s] can only be read. A dyn view is taken of the writable \
+ storage it came from"
+ (Types.to_string e.Tast.ty) (Types.to_string elem)
| Types.Slice (Types.Mut, elem) ->
(match view_elem elem with
| None -> view_not_yet loc e.Tast.ty elem
From c0b4b2235754920c49bc1972d2b682a8eb57546b Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 12:10:47 +0700
Subject: [PATCH 03/13] Growing, shrinking or freeing a container reached
through a [const T] is refused, and a function that only reads a slice stands
where one that may write it is wanted
---
lib/check.ml | 89 +++++++++++++++++++++-------------
lib/types.ml | 13 +++++
test/programs/const-slice.flan | 9 ++++
test/test_acceptance.ml | 2 +-
test/test_flan.ml | 31 ++++++++++++
5 files changed, 110 insertions(+), 34 deletions(-)
diff --git a/lib/check.ml b/lib/check.ml
index c1bf23c0..e22d0889 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -2192,8 +2192,57 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc =
crosses as ptr+len like any other. *)
let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc))
+(* The read-only slice a value's storage is reached through, if there is one:
+ an element of a [[const T]], a field of such an element, or an element of
+ an array that is. The last slice stepped through decides, because the
+ const is shallow — an element of a [[const [u8]]] is itself a writable
+ [[u8]], and what it views is not the outer slice's to protect. *)
+let rec const_reached (e : Tast.expr) =
+ match e.Tast.e with
+ | Tast.Prim (Tast.At, target :: idx) ->
+ const_steps (const_reached target) target.Tast.ty (List.length idx)
+ | Tast.Field (target, _) -> const_reached target
+ | _ -> None
+
+(* [ro] after stepping [n] dimensions into [ty], the way [indexed] steps. *)
+and const_steps ro (ty : Types.t) n =
+ if n = 0 then ro
+ else
+ match ty with
+ | Types.Slice (Types.Const, t) -> const_steps (Some ty) t (n - 1)
+ | Types.Slice (Types.Mut, t) -> const_steps None t (n - 1)
+ | Types.Array (_, t) -> const_steps ro t (n - 1)
+ | _ -> ro
+
+(* A store, or an [addr], through a read-only view. *)
+let refuse_const_place loc (view : Types.t) =
+ let elem = match view with Types.Slice (_, t) -> t | t -> t in
+ Loc.failk "check/store-through-const" loc
+ "this writes through a %s, which can only be read, so the element is a \
+ value and not a place. Write into a slice that can be written: \
+ (slice (into v (vec-new %s))) copies v's elements into one"
+ (Types.to_string view) (Types.to_string elem)
+
+(* The runtime entry points that change a Vec or a Map, which the backends
+ hand the container's address. An element of a [[const (Vec T)]], or a field
+ reached through one, is storage the view may not write, so growing,
+ shrinking or freeing it there is the same store [check_place] refuses —
+ made through the header instead of through a [set]. Writing into the
+ Vec's own buffer is not refused: the const is shallow, and the buffer is
+ not the slice's storage. *)
+let changes_container = function
+ | "flan_vec_push" | "flan_vec_reserve" | "flan_vec_free"
+ | "flan_map_put" | "flan_map_remove" | "flan_map_reserve" | "flan_map_free" ->
+ true
+ | _ -> false
+
(* A runtime call, with the result type spelled at the site. *)
-let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args))
+let rt loc ty sym args =
+ (if changes_container sym then
+ match args with
+ | target :: _ -> Option.iter (refuse_const_place loc) (const_reached target)
+ | [] -> ());
+ mk loc ty (Tast.Prim (Tast.Rt sym, args))
(* ── The allocation registry's note ──────────────────────────────────
@@ -3093,8 +3142,13 @@ let expect ctx loc ~want (got : Tast.expr) =
[CFn] has nowhere to put one — so the reverse falls through to the
ordinary refusal, which names both types and is the right sentence. *)
| Types.Fn (ps, r), Types.CFn (ps', r')
- when Types.equal (Types.Fn (ps, r)) (Types.Fn (ps', r')) ->
+ when Types.fn_accepts ~from:(ps', r') ~into:(ps, r) ->
mk loc w (Tast.Thicken (thick_thunk ctx.env loc ps r, got))
+ (* The same signature up to const, which [Types.fn_accepts] defines. *)
+ | Types.Fn (ps, r), Types.Fn (ps', r')
+ | Types.CFn (ps, r), Types.CFn (ps', r')
+ when Types.fn_accepts ~from:(ps', r') ~into:(ps, r) ->
+ { got with Tast.ty = w }
(* A writable view seen as a read-only one. The two are the same two
words, so the value is only retyped; the reverse is refused below,
with [const_note] naming the copy that would make it writable. *)
@@ -6448,37 +6502,6 @@ and refuse_string_place loc (ty : Types.t) =
"a string is read-only, so (at s i) is a value and not a place. Copy \
the bytes into a buffer you own and write that"
-(* The read-only slice a value's storage is reached through, if there is one:
- an element of a [[const T]], a field of such an element, or an element of
- an array that is. The last slice stepped through decides, because the
- const is shallow — an element of a [[const [u8]]] is itself a writable
- [[u8]], and what it views is not the outer slice's to protect. *)
-and const_reached (e : Tast.expr) =
- match e.Tast.e with
- | Tast.Prim (Tast.At, target :: idx) ->
- const_steps (const_reached target) target.Tast.ty (List.length idx)
- | Tast.Field (target, _) -> const_reached target
- | _ -> None
-
-(* [ro] after stepping [n] dimensions into [ty], the way [indexed] steps. *)
-and const_steps ro (ty : Types.t) n =
- if n = 0 then ro
- else
- match ty with
- | Types.Slice (Types.Const, t) -> const_steps (Some ty) t (n - 1)
- | Types.Slice (Types.Mut, t) -> const_steps None t (n - 1)
- | Types.Array (_, t) -> const_steps ro t (n - 1)
- | _ -> ro
-
-(* A store, or an [addr], through a read-only view. *)
-and refuse_const_place loc (view : Types.t) =
- let elem = match view with Types.Slice (_, t) -> t | t -> t in
- Loc.failk "check/store-through-const" loc
- "this writes through a %s, which can only be read, so the element is a \
- value and not a place. Write into a slice that can be written: \
- (slice (into v (vec-new %s))) copies v's elements into one"
- (Types.to_string view) (Types.to_string elem)
-
(* [store] is false for [addr] alone. A (Ptr T) is the C boundary, where the
program is already trusted — [slice-from-ptr] and [declare-c] take its word
— and a [[const u8]] handed to a C function that takes a [const T *] has no
diff --git a/lib/types.ml b/lib/types.ml
index c6bc9ae7..7ef1cd4d 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -346,3 +346,16 @@ let rec const_widens ~(from : t) ~(into : t) =
match from, into with
| Slice (_, a), Slice (Const, b) -> equal a b || const_widens ~from:a ~into:b
| _ -> false
+
+(* A function of one signature standing where another is wanted, when the
+ two differ only in const. A parameter may be more permissive than asked —
+ a function that takes a [[const T]] only reads what it is handed, so a
+ caller handing it a [[T]] loses nothing — and a result may be less so: a
+ [[T]] returned where a [[const T]] is wanted is [const_widens]'s case. The
+ two words are the same either way, so [Check.expect] only retypes. *)
+let fn_accepts ~(from : t list * t) ~(into : t list * t) =
+ let ps', r' = from and ps, r = into in
+ List.length ps = List.length ps'
+ && List.for_all2
+ (fun p p' -> equal p p' || const_widens ~from:p ~into:p') ps ps'
+ && (equal r r' || const_widens ~from:r' ~into:r)
diff --git a/test/programs/const-slice.flan b/test/programs/const-slice.flan
index 3d83ebde..6ab1db0f 100644
--- a/test/programs/const-slice.flan
+++ b/test/programs/const-slice.flan
@@ -18,6 +18,14 @@
(set n (+ n (length (at parts i)))))
n))
+;; A function that only reads stands where one that may write is wanted, and
+;; one returning a writable slice where a read-only one is wanted.
+(defn rd [s [const u8]] i32 (length s))
+(defn call-rd [f (Fn [[u8]] i32)] i32 (f (bytes "abc")))
+(defn call-bare [f (CFn [[u8]] i32)] i32 (f (bytes "abcd")))
+(defn mk [] [u8] (bytes "xy"))
+(defn call-mk [f (Fn [] [const u8])] i32 (length (f)))
+
(defn main [] i32
(let [xs [3 1 2]
w (slice xs)
@@ -45,5 +53,6 @@
(sort-bytes (slice f))
(println (string (slice (join (slice f) (bytes-view "-"))))))
(println (at r 0))
+ (println (call-rd rd) (call-bare rd) (call-mk mk))
(free names))
0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 7b1b65c5..4ef0165a 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -872,7 +872,7 @@ let () =
(* [const T]: the checker's alone, so the three builds agree and every
row is about which values reach which parameters. *)
let const_slice_out =
- "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n"
+ "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n3 4 2\n"
in
outputs "const slices" "programs/const-slice.flan" const_slice_out;
outputs ~opt:"-O0" "const slices, -O0" "programs/const-slice.flan"
diff --git a/test/test_flan.ml b/test/test_flan.ml
index c4fc6f18..77abd557 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2291,6 +2291,37 @@ let () =
rejects_check "no conversion under a writable slice"
"(defn g [p [[const u8]]] i32 0) (defn f [p [[u8]]] i32 (g p))"
~needle:"expected [[const u8]], found [[u8]]";
+ rejects_check "push through a const slice of Vecs"
+ "(defn f [s [const (Vec i32)]] () (push (at s 0) 5))"
+ ~needle:"this writes through a [const (Vec i32)]";
+ rejects_check "put through a const slice of maps"
+ "(defn f [s [const (Map string i32)]] () (put (at s 0) \"a\" 5))"
+ ~needle:"this writes through a [const (Map string i32)]";
+ rejects_check "map-remove through a const slice of maps"
+ "(defn f [s [const (Map string i32)]] bool (map-remove (at s 0) \"a\"))"
+ ~needle:"this writes through a [const (Map string i32)]";
+ rejects_check "reserve through a const slice of Vecs"
+ "(defn f [s [const (Vec i32)]] () (reserve (at s 0) 10))"
+ ~needle:"this writes through a [const (Vec i32)]";
+ rejects_check "free through a const slice of Vecs"
+ "(defn f [s [const (Vec i32)]] () (free (at s 0)))"
+ ~needle:"this writes through a [const (Vec i32)]";
+ rejects_check "push into a field reached through a const slice"
+ "(defstruct P [v (Vec i32)]) (defn f [s [const P]] () (push (.v (at s 0)) 1))"
+ ~needle:"this writes through a [const P]";
+ accepts "a Vec's own buffer is not the const slice's storage"
+ "(defn f [s [const (Vec i32)]] () (set (at (at s 0) 0) 5))";
+ accepts "a reading function where a writing one is wanted"
+ "(defn rd [s [const u8]] i32 0) (defn c [f (Fn [[u8]] i32)] i32 0) \
+ (defn m [] i32 (c rd))";
+ rejects_check "not a writing function where a reading one is wanted"
+ "(defn wr [s [u8]] i32 0) (defn c [f (Fn [[const u8]] i32)] i32 0) \
+ (defn m [] i32 (c wr))"
+ ~needle:"expected (Fn [[const u8]] i32), found (CFn [[u8]] i32)";
+ rejects_check "nor a read-only result where a writable one is wanted"
+ "(defn mk [] [const u8] (bytes-view \"a\")) \
+ (defn c [f (Fn [] [u8])] i32 0) (defn m [] i32 (c mk))"
+ ~needle:"expected (Fn [] [u8]), found (CFn [] [const u8])";
rejects_check "const is not a name a constant can have"
"(defconst const 4)" ~needle:"const cannot be declared";
(* The const is shallow: an element of a [const [u8]] is a writable [u8]. *)
From d8945ae4ae4ca4f8d08db418e16a274bb52910f1 Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 12:43:04 +0700
Subject: [PATCH 04/13] The address of read-only storage is a (Ptr const T),
which nothing is written through and which a C const T * parameter takes
---
lib/check.ml | 166 +++++++++++++++++++++++----------
lib/cimport.ml | 65 ++++++++-----
lib/dev.ml | 8 +-
lib/emit.ml | 14 +--
lib/render.ml | 2 +-
lib/session.ml | 38 ++++----
lib/shim.ml | 2 +
lib/types.ml | 10 +-
lib/x86.ml | 18 ++--
runtime/flan_dev.c | 2 +-
spike/x86/survey.sh | 8 +-
test/programs/const-slice.flan | 7 ++
test/programs/dev-segv.flan | 33 ++++---
test/test_acceptance.ml | 2 +-
test/test_dev.ml | 7 +-
test/test_flan.ml | 67 +++++++++++--
test/test_sanitize.ml | 5 +-
vendor/raylib/generated.flan | 54 +++++------
vendor/raylib/raylib.flan | 26 +++---
19 files changed, 335 insertions(+), 199 deletions(-)
diff --git a/lib/check.ml b/lib/check.ml
index e22d0889..dfd97c60 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -1172,6 +1172,10 @@ let tyvar_in_scope env n =
let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
let loc = t.Ast.tloc in
match t.Ast.t with
+ | Ast.Tname "const" ->
+ fail loc
+ "const is not a type on its own — it marks one that can only be read, \
+ as in [const u8] or (Ptr const u8)"
| Ast.Tname n -> resolve_name env ~seen loc n
| Ast.Tslice (c, e) ->
Types.Slice ((if c then Types.Const else Types.Mut), resolve env ~seen e)
@@ -1209,9 +1213,16 @@ let rec resolve env ?(seen = []) (t : Ast.texpr) : Types.t =
if env' then Types.Fn (ps, r) else Types.CFn (ps, r)
| Ast.Tapp (name, args) ->
(match name, args with
- | "Ptr", [ a ] -> Types.Ptr (resolve env ~seen a)
+ | "Ptr", [ a ] -> Types.Ptr (Types.Mut, resolve env ~seen a)
+ (* The pointer beside [[const T]]: nothing is written through it, and a
+ (Ptr T) converts to one. [const] cannot name a type, so this reading
+ is the only one the two arguments have. *)
+ | "Ptr", [ { Ast.t = Ast.Tname "const"; _ }; a ] ->
+ Types.Ptr (Types.Const, resolve env ~seen a)
| "Option", [ a ] -> Types.Option (resolve env ~seen a)
- | ("Ptr" | "Option"), _ -> fail loc "(%s T) takes exactly one type" name
+ | "Ptr", _ -> fail loc "a pointer type is (Ptr T), or (Ptr const T) for one \
+ nothing is written through"
+ | "Option", _ -> fail loc "(Option T) takes exactly one type"
| "Vec", [ a ] ->
let e = resolve env ~seen a in
(* A Vec of a Vec used to be refused here, and the refusal named two
@@ -1865,7 +1876,9 @@ let rec bind_ty ?(widen = false) ?(ro = true) subst (pat : Types.t)
| Types.Slice (m, p), Types.Slice (m', a)
when m = m' || (ro && m = Types.Const) ->
bind_ty ~ro:(m = Types.Const) subst p a
- | Types.Ptr p, Types.Ptr a
+ | Types.Ptr (m, p), Types.Ptr (m', a)
+ when m = m' || (ro && m = Types.Const) ->
+ bind_ty ~ro:(m = Types.Const) subst p a
| Types.Vec p, Types.Vec a
| Types.Option p, Types.Option a -> inner p a
| Types.Array (n, p), Types.Array (m, a) -> Int64.equal n m && inner p a
@@ -1912,7 +1925,7 @@ let rec subst_ty subst (t : Types.t) =
| Types.Slice (m, e) -> Types.Slice (m, subst_ty subst e)
| Types.Array (n, e) -> Types.Array (n, subst_ty subst e)
| Types.Map (k, v) -> Types.Map (subst_ty subst k, subst_ty subst v)
- | Types.Ptr e -> Types.Ptr (subst_ty subst e)
+ | Types.Ptr (m, e) -> Types.Ptr (m, subst_ty subst e)
| Types.Vec e -> Types.Vec (subst_ty subst e)
| Types.Option e -> Types.Option (subst_ty subst e)
| Types.Fn (ps, r) -> Types.Fn (List.map (subst_ty subst) ps, subst_ty subst r)
@@ -1924,7 +1937,7 @@ let rec subst_ty subst (t : Types.t) =
let rec generic_ty (t : Types.t) =
match t with
| Types.Var _ -> true
- | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+ | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e
| Types.Option e -> generic_ty e
| Types.Map (k, v) -> generic_ty k || generic_ty v
| Types.Fn (ps, r) | Types.CFn (ps, r) ->
@@ -1938,7 +1951,7 @@ let rec generic_ty (t : Types.t) =
let rec reaches_dyn (t : Types.t) =
match t with
| Types.Dyn -> true
- | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+ | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e
| Types.Option e -> reaches_dyn e
| Types.Map (k, v) -> reaches_dyn k || reaches_dyn v
| Types.Fn (ps, r) | Types.CFn (ps, r) ->
@@ -1982,7 +1995,8 @@ let rec mangle_ty (t : Types.t) =
| Types.Slice (Types.Const, e) -> "cslice-" ^ mangle_ty e
| Types.Array (n, e) -> Printf.sprintf "arr%Ld-%s" n (mangle_ty e)
| Types.Map (k, v) -> Printf.sprintf "map-%s-%s" (mangle_ty k) (mangle_ty v)
- | Types.Ptr e -> "ptr-" ^ mangle_ty e
+ | Types.Ptr (Types.Mut, e) -> "ptr-" ^ mangle_ty e
+ | Types.Ptr (Types.Const, e) -> "cptr-" ^ mangle_ty e
| Types.Vec e -> "vec-" ^ mangle_ty e
| Types.Option e -> "opt-" ^ mangle_ty e
| Types.Fn (ps, r) ->
@@ -2023,7 +2037,7 @@ let rec occurs_in ~needle (t : Types.t) =
Types.equal needle t
||
match t with
- | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+ | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e
| Types.Option e -> occurs_in ~needle e
| Types.Map (k, v) -> occurs_in ~needle k || occurs_in ~needle v
| Types.Fn (ps, r) | Types.CFn (ps, r) ->
@@ -2164,11 +2178,11 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc =
in
Hashtbl.replace fctx.env.structs ename { Tast.sname = ename; fields };
let ety = Types.Named ename in
- let eslot = fresh_slot fctx (Types.Ptr ety) in
+ let eslot = fresh_slot fctx (Types.Ptr (Types.Mut, ety)) in
let binds =
List.mapi
(fun i (_, ((b : binding), slot)) ->
- let p = mk loc (Types.Ptr ety) (Tast.Local eslot) in
+ let p = mk loc (Types.Ptr (Types.Mut, ety)) (Tast.Local eslot) in
(slot, mk loc b.bty (Tast.Field (mk loc ety (Tast.Deref p), i))))
caught
in
@@ -2183,7 +2197,7 @@ let close_over ~fname (octx : ctx) (fctx : ctx) loc =
caught))
in
prefix, Some eslot, Some (mslot, make),
- Some (mk loc (Types.Ptr ety) (Tast.Addr (Tast.Plocal mslot)))
+ Some (mk loc (Types.Ptr (Types.Mut, ety)) (Tast.Addr (Tast.Plocal mslot)))
(* A source location as a value, for a runtime trap that has to name the site
rather than the runtime. The bounds and slice traps get theirs from [Emit],
@@ -2202,6 +2216,8 @@ let rec const_reached (e : Tast.expr) =
| Tast.Prim (Tast.At, target :: idx) ->
const_steps (const_reached target) target.Tast.ty (List.length idx)
| Tast.Field (target, _) -> const_reached target
+ | Tast.Deref p ->
+ (match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None)
| _ -> None
(* [ro] after stepping [n] dimensions into [ty], the way [indexed] steps. *)
@@ -2214,14 +2230,27 @@ and const_steps ro (ty : Types.t) n =
| Types.Array (_, t) -> const_steps ro t (n - 1)
| _ -> ro
-(* A store, or an [addr], through a read-only view. *)
+(* A store through a read-only view: a [[const T]] or a (Ptr const T). *)
let refuse_const_place loc (view : Types.t) =
- let elem = match view with Types.Slice (_, t) -> t | t -> t in
- Loc.failk "check/store-through-const" loc
- "this writes through a %s, which can only be read, so the element is a \
- value and not a place. Write into a slice that can be written: \
- (slice (into v (vec-new %s))) copies v's elements into one"
- (Types.to_string view) (Types.to_string elem)
+ match view with
+ | Types.Ptr (_, ((Types.Vec _ | Types.Map _) as t)) ->
+ Loc.failk "check/store-through-const" loc
+ "this changes the %s behind a %s, which can only be read through. A \
+ container that has to change is handed over as a (Ptr %s)"
+ (Types.to_string t) (Types.to_string view) (Types.to_string t)
+ | Types.Ptr (_, t) ->
+ Loc.failk "check/store-through-const" loc
+ "this writes through a %s, which can only be read, so what it points at \
+ is a value and not a place. (deref p) copies the %s out, and the copy \
+ can be written"
+ (Types.to_string view) (Types.to_string t)
+ | _ ->
+ let elem = match view with Types.Slice (_, t) -> t | t -> t in
+ Loc.failk "check/store-through-const" loc
+ "this writes through a %s, which can only be read, so the element is a \
+ value and not a place. Write into a slice that can be written: \
+ (slice (into v (vec-new %s))) copies v's elements into one"
+ (Types.to_string view) (Types.to_string elem)
(* The runtime entry points that change a Vec or a Map, which the backends
hand the container's address. An element of a [[const (Vec T)]], or a field
@@ -2358,7 +2387,7 @@ let align_of loc t = mk loc (Types.Int Types.I64) (Tast.Prim (Tast.AlignOf t, []
(* The address of an expression, place or not: the type-erased runtime takes
the element [push] copies by pointer. *)
let addr_of loc (e : Tast.expr) =
- mk loc (Types.Ptr e.Tast.ty) (Tast.Prim (Tast.AddrOf, [ e ]))
+ mk loc (Types.Ptr (Types.Mut, e.Tast.ty)) (Tast.Prim (Tast.AddrOf, [ e ]))
(* ── Where a rendered number's bytes live ──────────────────────────────
@@ -3015,7 +3044,8 @@ let rec thick_enc (t : Types.t) =
| Types.Var v -> "y" ^ atom v
| Types.Slice (Types.Mut, e) -> "s" ^ thick_enc e
| Types.Slice (Types.Const, e) -> "k" ^ thick_enc e
- | Types.Ptr e -> "p" ^ thick_enc e
+ | Types.Ptr (Types.Mut, e) -> "p" ^ thick_enc e
+ | Types.Ptr (Types.Const, e) -> "q" ^ thick_enc e
| Types.Vec e -> "v" ^ thick_enc e
| Types.Option e -> "o" ^ thick_enc e
| Types.Array (n, e) -> Printf.sprintf "a%Ld-%s" n (thick_enc e)
@@ -3060,7 +3090,7 @@ let thick_thunk env loc ps r =
that never reads it costs one store the optimiser drops. *)
let declare_env ctx = function
| Some _ as s -> s
- | None -> Some (fresh_slot ctx (Types.Ptr Types.Unit))
+ | None -> Some (fresh_slot ctx (Types.Ptr (Types.Mut, Types.Unit)))
let numeric_note ~(want : Types.t) ~(got : Types.t) =
if not (Types.is_numeric want && Types.is_numeric got) then ""
@@ -3095,6 +3125,14 @@ let const_note ~(want : Types.t) ~(got : Types.t) =
through it, the %s can be declared %s instead"
(Types.to_string got) (Types.to_string want) copy (Types.to_string want)
(Types.to_string want) (Types.to_string got)
+ | Types.Ptr (Types.Mut, e), Types.Ptr (Types.Const, e')
+ when Types.equal e e' ->
+ Printf.sprintf
+ " — a %s can only be read through, and never becomes a %s that can be \
+ written through. Copy the %s out with (deref p) and point at the copy; \
+ where nothing writes through it, the %s can be declared %s instead"
+ (Types.to_string got) (Types.to_string want) (Types.to_string e)
+ (Types.to_string want) (Types.to_string got)
| _ -> ""
let expect ctx loc ~want (got : Tast.expr) =
@@ -3152,7 +3190,7 @@ let expect ctx loc ~want (got : Tast.expr) =
(* A writable view seen as a read-only one. The two are the same two
words, so the value is only retyped; the reverse is refused below,
with [const_note] naming the copy that would make it writable. *)
- | Types.Slice (Types.Const, _), _
+ | (Types.Slice (Types.Const, _) | Types.Ptr (Types.Const, _)), _
when Types.const_widens ~from:got.Tast.ty ~into:w ->
{ got with Tast.ty = w }
| _ -> got
@@ -3239,8 +3277,8 @@ let invented_ctx env ret =
(* The address of field [i] of the struct the pointer in slot [p] points at. *)
let field_addr_of loc sty fty p i =
- let target = mk loc sty (Tast.Deref (mk loc (Types.Ptr sty) (Tast.Local p))) in
- mk loc (Types.Ptr fty) (Tast.Addr (Tast.Pfield (target, i)))
+ let target = mk loc sty (Tast.Deref (mk loc (Types.Ptr (Types.Mut, sty)) (Tast.Local p))) in
+ mk loc (Types.Ptr (Types.Mut, fty)) (Tast.Addr (Tast.Pfield (target, i)))
(* The pointer form is what a Map_Info holds; the direct form is what an
emitted hasher calls. See flan_rt.c on why they are two symbols. *)
@@ -3337,8 +3375,8 @@ and struct_key_pair env loc n =
fail loc
"%s has no fields, so it is not a map key — every value of it would \
be the same key" n;
- let hparams = [ Types.Ptr sty; hash_ty; Types.Int Types.I64 ] in
- let eparams = [ Types.Ptr sty; Types.Ptr sty; Types.Int Types.I64 ] in
+ let hparams = [ Types.Ptr (Types.Mut, sty); hash_ty; Types.Int Types.I64 ] in
+ let eparams = [ Types.Ptr (Types.Mut, sty); Types.Ptr (Types.Mut, sty); Types.Int Types.I64 ] in
(* Registered before the fields are walked, so a struct reached twice
through two different fields emits one pair and not two. A struct cannot
contain itself by value, so there is no cycle to break — only sharing.
@@ -3358,7 +3396,7 @@ and struct_key_pair env loc n =
hashes its bytes and a nested struct hashes field by field. Padding is
never reached, because nothing here addresses anything but a field. *)
let hctx = invented_ctx env hash_ty in
- let kp = fresh_slot ~name:"key" hctx (Types.Ptr sty) in
+ let kp = fresh_slot ~name:"key" hctx (Types.Ptr (Types.Mut, sty)) in
let seed = fresh_slot ~name:"seed" hctx hash_ty in
ignore (fresh_slot ~name:"size" hctx (Types.Int Types.I64));
let acc = fresh_slot ~name:"h" hctx hash_ty in
@@ -3395,8 +3433,8 @@ and struct_key_pair env loc n =
field that differs, which for a struct with a string field is the
difference between one memcmp and two. *)
let ectx = invented_ctx env (Types.Int Types.I8) in
- let ap = fresh_slot ~name:"a" ectx (Types.Ptr sty) in
- let bp = fresh_slot ~name:"b" ectx (Types.Ptr sty) in
+ let ap = fresh_slot ~name:"a" ectx (Types.Ptr (Types.Mut, sty)) in
+ let bp = fresh_slot ~name:"b" ectx (Types.Ptr (Types.Mut, sty)) in
ignore (fresh_slot ~name:"size" ectx (Types.Int Types.I64));
let i8 v = mk loc (Types.Int Types.I8) (Tast.Int (v, Types.I8)) in
let checks =
@@ -3648,7 +3686,7 @@ let tracked_call loc env name (tr : Shim.track) ret (args : Tast.expr list) =
List.filter_map
(fun i ->
match List.nth_opt args i with
- | Some ({ Tast.ty = Types.Ptr t; _ } as p) when res_pure p ->
+ | Some ({ Tast.ty = Types.Ptr (_, t); _ } as p) when res_pure p ->
Some (mk loc t (Tast.Deref p), t)
| _ -> None)
tr.Shim.rekey
@@ -4600,7 +4638,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
pointer is a hidden parameter and the name is a slot loaded from
it — a handler that passed [c] to something expecting the struct
would otherwise be handed an address. *)
- let pslot = fresh_slot hctx (Types.Ptr ty) in
+ let pslot = fresh_slot hctx (Types.Ptr (Types.Mut, ty)) in
let cslot = bind hctx c.Ast.hname ty ~assignable:false in
let hbody = map_lr (fun e -> check hctx e) c.Ast.hbody in
let hbody =
@@ -4609,7 +4647,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
([ (cslot,
mk c.Ast.hloc ty
(Tast.Deref
- (mk c.Ast.hloc (Types.Ptr ty) (Tast.Local pslot)))) ],
+ (mk c.Ast.hloc (Types.Ptr (Types.Mut, ty)) (Tast.Local pslot)))) ],
hbody)) ]
in
(* Named after the function it came out of, and numbered within it:
@@ -4642,7 +4680,7 @@ and check_handler_bind ctx ?want ?(what = "handler-bind") loc clauses body =
clause matched, and it cannot know which of them captured. *)
let fenv = declare_env hctx fenv in
ctx.env.lifted <-
- { Tast.name = fname; params = [ Types.Ptr ty ];
+ { Tast.name = fname; params = [ Types.Ptr (Types.Mut, ty) ];
slots = Array.of_list (List.rev hctx.slot_tys);
snames = Array.of_list (List.rev hctx.slot_names);
ret = Types.Unit; body = prefix hbody; fdefers = [];
@@ -6362,7 +6400,7 @@ and unknown_name : 'a. ?setting:bool -> ctx -> Loc.t -> string -> 'a =
let sname =
match ty with
| Some (Types.Named n) when fields_named ctx.env n <> None -> Some n
- | Some (Types.Ptr (Types.Named n)) when fields_named ctx.env n <> None -> Some n
+ | Some (Types.Ptr (_, (Types.Named n))) when fields_named ctx.env n <> None -> Some n
| _ -> None
in
match sname, ty with
@@ -6455,13 +6493,13 @@ and struct_target ctx (target : Ast.expr) : Tast.expr * string =
let has n = fields_named ctx.env n <> None in
match t.Tast.ty with
| Types.Named n when has n -> t, n
- | Types.Ptr (Types.Named n) when has n ->
+ | Types.Ptr (_, (Types.Named n)) when has n ->
mk t.Tast.loc (Types.Named n) (Tast.Deref t), n
(* A data type's fields belong to one case, and which case it is holding is
only known after the tag has been read. [.field] would have to be a read
that might be reading something else, so it is not one: [match] is how a
data type is opened, and it binds the fields it has proved are there. *)
- | (Types.Named n | Types.Ptr (Types.Named n))
+ | (Types.Named n | Types.Ptr (_, Types.Named n))
when Hashtbl.mem ctx.env.datas n ->
fail target.Ast.loc
"%s is a data type, and its fields belong to a case — reach them with \
@@ -6508,6 +6546,26 @@ and refuse_string_place loc (ty : Types.t) =
other way across: [load-image-from-memory] over an [embed] is the case. So
the address of a read-only element may be taken, and it is a store that is
refused. *)
+(* Whether a checked place is read-only storage: reached through a
+ [[const T]] or a (Ptr const T), or a byte of a string. Its address is a
+ (Ptr const T). *)
+and place_const (p : Tast.place) =
+ match p with
+ | Tast.Plocal _ | Tast.Pglobal _ -> false
+ | Tast.Pfield (t, _) -> const_reached t <> None
+ | Tast.Pderef t ->
+ (match t.Tast.ty with Types.Ptr (Types.Const, _) -> true | _ -> false)
+ | Tast.Pindex (t, idx) ->
+ let rec through_string ty n =
+ n > 0
+ && (match ty with
+ | Types.String -> true
+ | Types.Array (_, e) | Types.Slice (_, e) -> through_string e (n - 1)
+ | _ -> false)
+ in
+ const_steps (const_reached t) t.Tast.ty (List.length idx) <> None
+ || through_string t.Tast.ty (List.length idx)
+
and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
match p with
| Ast.Pvar name ->
@@ -6577,7 +6635,9 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
| Ast.Pderef target ->
let target = check ctx target in
(match target.Tast.ty with
- | Types.Ptr t -> Tast.Pderef target, t
+ | Types.Ptr (Types.Const, _) as view when store ->
+ refuse_const_place loc view
+ | Types.Ptr (_, t) -> Tast.Pderef target, t
| other ->
fail loc "deref takes a (Ptr T), found %s" (Types.to_string other))
@@ -6646,7 +6706,7 @@ and indexed ?place ?(store = true) ctx (target : Tast.expr) (idx : Ast.expr list
| Types.Array (_, t) | Types.Slice (_, t) -> t
(* A string indexes to its bytes, and only to read them. *)
| Types.String ->
- Option.iter (fun l -> refuse_string_place l ty) place;
+ if store then Option.iter (fun l -> refuse_string_place l ty) place;
Types.Int Types.U8
| other ->
fail i.Ast.loc "%s cannot be indexed" (Types.to_string other)
@@ -7290,7 +7350,7 @@ and vec_at ctx loc (target : Tast.expr) (idx : Ast.expr list) =
match idx with
| [ i ] ->
let i = index_expr ctx i in
- rt loc (Types.Ptr elem) "flan_vec_at"
+ rt loc (Types.Ptr (Types.Mut, elem)) "flan_vec_at"
[ target; i; size_of loc elem; here loc ], elem
| _ ->
fail loc
@@ -8414,9 +8474,9 @@ and named_call ?(qualified = false) ctx ~want loc name args =
| [ target; cur; k; v ] ->
let target = check ctx target in
let kt, vt = map_kv loc "map-next" target.Tast.ty in
- let cur = check ctx ~want:(Types.Ptr (Types.Int Types.I64)) cur in
- let k = check ctx ~want:(Types.Ptr kt) k in
- let v = check ctx ~want:(Types.Ptr vt) v in
+ let cur = check ctx ~want:(Types.Ptr (Types.Mut, (Types.Int Types.I64))) cur in
+ let k = check ctx ~want:(Types.Ptr (Types.Mut, kt)) k in
+ let v = check ctx ~want:(Types.Ptr (Types.Mut, vt)) v in
let found =
rt loc (Types.Int Types.I8) "flan_map_next"
[ target; cur; k; v; size_of loc kt; size_of loc vt; here loc ]
@@ -8951,7 +9011,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
let target = check ctx target in
let elem =
match target.Tast.ty with
- | Types.Ptr t -> t
+ | Types.Ptr (_, t) -> t
| other ->
fail loc
"slice-from-ptr takes a (Ptr T) and the number of elements behind \
@@ -8967,7 +9027,10 @@ and named_call ?(qualified = false) ctx ~want loc name args =
fail n_loc
"slice-from-ptr length %Ld is negative" k
| _ -> ());
- prim Tast.SliceFromPtr (Types.Slice (Types.Mut, elem)) [ target; n ]
+ (* A read-only pointer gives a read-only slice, or [slice-from-ptr]
+ would undo the const [addr] put there. *)
+ let m = match target.Tast.ty with Types.Ptr (m, _) -> m | _ -> Types.Mut in
+ prim Tast.SliceFromPtr (Types.Slice (m, elem)) [ target; n ]
| _ -> assert false)
(* ── pointers ──────────────────────────────────────────────────── *)
@@ -8981,12 +9044,13 @@ and named_call ?(qualified = false) ctx ~want loc name args =
or (deref p)"
| Some p ->
let p, ty = check_place ~store:false ctx a.Ast.loc p in
- expect ctx loc ~want (mk loc (Types.Ptr ty) (Tast.Addr p)))
+ let m = if place_const p then Types.Const else Types.Mut in
+ expect ctx loc ~want (mk loc (Types.Ptr (m, ty)) (Tast.Addr p)))
| "deref" ->
arity ctx loc name 1 args;
let a = check ctx (List.hd args) in
(match a.Tast.ty with
- | Types.Ptr t -> expect ctx loc ~want (mk loc t (Tast.Deref a))
+ | Types.Ptr (_, t) -> expect ctx loc ~want (mk loc t (Tast.Deref a))
| other -> fail loc "deref takes a (Ptr T), found %s"
(Types.to_string other))
@@ -9857,7 +9921,7 @@ and generic_call ctx ~want loc name vars pats pret args =
let rec mentions v (t : Types.t) =
match t with
| Types.Var u -> String.equal u v
- | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr e | Types.Vec e
+ | Types.Slice (_, e) | Types.Array (_, e) | Types.Ptr (_, e) | Types.Vec e
| Types.Option e -> mentions v e
| Types.Map (k, w) -> mentions v k || mentions v w
| Types.Fn (ps, r) | Types.CFn (ps, r) ->
@@ -12197,7 +12261,7 @@ let rec dyn_reach ~through p seen (t : Types.t) =
| Types.Dyn -> true
| Types.Array (_, e) | Types.Vec e | Types.Option e -> go e
| Types.Map (k, v) -> go k || go v
- | Types.Ptr e | Types.Slice (_, e) -> through && go e
+ | Types.Ptr (_, e) | Types.Slice (_, e) -> through && go e
| Types.Fn _ -> false
| Types.Named n when not (List.mem n seen) ->
let seen = n :: seen in
@@ -12252,7 +12316,7 @@ let rec dyn_behind_pointer p seen (t : Types.t) =
It still terminates. This walk's own [seen] guards its own [Named]
recursion, and each crossing starts a separate finite walk of its own. *)
- | Types.Ptr e | Types.Slice (_, e) -> dyn_through p [] e
+ | Types.Ptr (_, e) | Types.Slice (_, e) -> dyn_through p [] e
| Types.Array (_, e) | Types.Vec e | Types.Option e -> go e
| Types.Map (k, v) -> go k || go v
| Types.Dyn | Types.Fn _ -> false
@@ -12327,7 +12391,7 @@ let rec hidden_dyn p seen (t : Types.t) : Types.t option =
if dyn_anywhere p seen k || dyn_anywhere p seen v then Some t else None
(* A pointer and a slice are views of storage something else roots; see the
note above. What they point at is checked where it is declared. *)
- | Types.Ptr e | Types.Slice (_, e) -> hidden_dyn p seen e
+ | Types.Ptr (_, e) | Types.Slice (_, e) -> hidden_dyn p seen e
| Types.Fn _ -> None
| Types.Named n when not (List.mem n seen) ->
let seen = n :: seen in
@@ -12476,7 +12540,7 @@ let dyn_descriptors (p : Tast.program) =
foreign parameter of pointer or slice type receives is the address
of a place. Below it the question is [dyn_behind_pointer]'s again. *)
let below (t : Types.t) =
- match t with Types.Ptr e | Types.Slice (_, e) -> e | t -> t
+ match t with Types.Ptr (_, e) | Types.Slice (_, e) -> e | t -> t
in
List.iteri
(fun i t ->
diff --git a/lib/cimport.ml b/lib/cimport.ml
index d72a954b..6d5d067c 100644
--- a/lib/cimport.ml
+++ b/lib/cimport.ml
@@ -556,6 +556,13 @@ let param_ty env (s : string) : Ast.texpr =
"char * is a parameter C may write through, and a Flan string crosses \
as a NUL-terminated copy — the writes would be lost. const char * is \
a string; this one needs a declare-c saying (Ptr u8)"
+ (* [const T *] is the one pointer C promises not to write through, so it
+ takes a (Ptr const T) — and with it the address of a read-only
+ element, which a (Ptr T) parameter would refuse. *)
+ | _ when is_const ->
+ (match (value_ty env s).Ast.t with
+ | Ast.Tapp ("Ptr", [ e ]) -> ty (Ast.Tapp ("Ptr", [ tname "const"; e ]))
+ | _ -> value_ty env s)
| _ -> value_ty env s
end
else value_ty env s
@@ -949,33 +956,41 @@ let c_pointee (s : string) : string option =
Some (String.trim (String.sub s 0 (String.length s - 1)))
else None
+let ptr_agrees_elem env ~inner (elem : Ast.texpr) =
+ (* [void *] agrees with a pointer to anything, and this is the judgement
+ call of the arm. C's [void *] is opaque about *what it points at* — that
+ is the whole of what the spelling means — so there is no element type in
+ the header to disagree with, and a check that reported one would be
+ reporting [value_ty]'s guess of [u8] back at the author as if the header
+ had said it. What is *not* given up is that it is a pointer at all: the
+ match above requires [(Ptr _)] on the Flan side, so an [i32] or a
+ [string] declared against a [void *] is still a finding. That
+ asymmetry is the point — raylib spells thirty-odd parameters [void *]
+ and none of them is a scalar. *)
+ let b = bare inner in
+ if String.equal b "void" then true
+ else (
+ match (try Some (value_ty env inner) with Refused _ -> None) with
+ | None ->
+ (* A pointee this cannot render says nothing, exactly as an
+ unrenderable field type says nothing in [check_structs]. *)
+ false
+ | Some want ->
+ let a = ty_source want and b = ty_source elem in
+ (* [agrees] and not [String.equal], so a [(Ptr Key)] against the
+ header's [(Ptr int)] lands on the enum arm. The four bytes are the
+ same four bytes through a pointer as they are beside one. *)
+ agrees env want elem || (byte a && byte b))
+
let ptr_agrees env ~(c : string) (t : Ast.texpr) =
match (c_pointee c, t.Ast.t) with
- | Some inner, Ast.Tapp ("Ptr", [ elem ]) ->
- (* [void *] agrees with a pointer to anything, and this is the judgement
- call of the arm. C's [void *] is opaque about *what it points at* — that
- is the whole of what the spelling means — so there is no element type in
- the header to disagree with, and a check that reported one would be
- reporting [value_ty]'s guess of [u8] back at the author as if the header
- had said it. What is *not* given up is that it is a pointer at all: the
- match above requires [(Ptr _)] on the Flan side, so an [i32] or a
- [string] declared against a [void *] is still a finding. That
- asymmetry is the point — raylib spells thirty-odd parameters [void *]
- and none of them is a scalar. *)
- let b = bare inner in
- if String.equal b "void" then true
- else (
- match (try Some (value_ty env inner) with Refused _ -> None) with
- | None ->
- (* A pointee this cannot render says nothing, exactly as an
- unrenderable field type says nothing in [check_structs]. *)
- false
- | Some want ->
- let a = ty_source want and b = ty_source elem in
- (* [agrees] and not [String.equal], so a [(Ptr Key)] against the
- header's [(Ptr int)] lands on the enum arm. The four bytes are the
- same four bytes through a pointer as they are beside one. *)
- agrees env want elem || (byte a && byte b))
+ (* A (Ptr const T) promises C will not write, so the header has to promise
+ it too: over a [T *] without const, C may write through storage Flan
+ holds read-only. *)
+ | Some inner, Ast.Tapp ("Ptr", [ { Ast.t = Ast.Tname "const"; _ }; elem ]) ->
+ strip_prefix "const " inner <> None
+ && ptr_agrees_elem env ~inner elem
+ | Some inner, Ast.Tapp ("Ptr", [ elem ]) -> ptr_agrees_elem env ~inner elem
| _ -> false
(* The two together, for the one caller that still has the C spelling. A
diff --git a/lib/dev.ml b/lib/dev.ml
index dfe19dda..7170de14 100644
--- a/lib/dev.ml
+++ b/lib/dev.ml
@@ -2726,7 +2726,7 @@ let type_of_spelling t spelling : (Types.t, string) result =
let addr_extern : Tast.extern =
{ Tast.ename = "flan/dev-addr"; esym = "flan_dev_reg_addr";
eparams = [ Types.Int Types.I64 ];
- eret = Types.Ptr (Types.Int Types.U8); eloc = Loc.unknown }
+ eret = Types.Ptr (Types.Mut, (Types.Int Types.U8)); eloc = Loc.unknown }
(* Renders the value [(Ptr ty)] holding [addr], in the program.
@@ -2761,7 +2761,7 @@ let render_addr (s : Session.t) ~addr ~(ty : Types.t)
extra := ty :: !extra;
i) }
in
- let pty = Types.Ptr ty in
+ let pty = Types.Ptr (Types.Mut, ty) in
let root =
{ Tast.e =
Tast.Prim
@@ -2771,7 +2771,7 @@ let render_addr (s : Session.t) ~addr ~(ty : Types.t)
("flan/dev-addr",
[ { Tast.e = Tast.Int (Int64.of_int addr, Types.I64);
ty = Types.Int Types.I64; loc } ]);
- ty = Types.Ptr (Types.Int Types.U8); loc } ]);
+ ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc } ]);
ty = pty; loc }
in
match Render.render c 0 root with
@@ -2935,7 +2935,7 @@ let inspect_addr t ~addr ~want_type =
| Ok v ->
ok
([ Printf.sprintf ":addr %d" addr;
- ":type " ^ Wire.quote (Types.to_string (Types.Ptr ty));
+ ":type " ^ Wire.quote (Types.to_string (Types.Ptr (Types.Mut, ty)));
":value " ^ Wire.quote v; ":live " ^ live ]
@ told @ where))))))
diff --git a/lib/emit.ml b/lib/emit.ml
index a8ccfff7..3e229510 100644
--- a/lib/emit.ml
+++ b/lib/emit.ml
@@ -791,7 +791,7 @@ let rec dty m d (t : Types.t) : int =
| Types.Bool -> basic "bool" 8 "DW_ATE_boolean"
| Types.Enum e -> basic e 32 "DW_ATE_signed"
| Types.Unit | Types.Never -> composite (Types.to_string t) []
- | Types.Ptr e ->
+ | Types.Ptr (_, e) ->
let id = dalloc d in
Hashtbl.replace d.dtys key id;
(* [(Ptr Unit)] and [(Ptr Never)] are the opaque pointer, and a DWARF
@@ -817,10 +817,10 @@ let rec dty m d (t : Types.t) : int =
capacity, so two members are the whole truth about a slice. *)
| Types.String ->
composite "string"
- [ ("ptr", Types.Ptr (Types.Int Types.U8)); ("len", Types.Int Types.I64) ]
+ [ ("ptr", Types.Ptr (Types.Mut, (Types.Int Types.U8))); ("len", Types.Int Types.I64) ]
| Types.Slice (_, e) ->
composite (Types.to_string t)
- [ ("ptr", Types.Ptr e); ("len", Types.Int Types.I64) ]
+ [ ("ptr", Types.Ptr (Types.Mut, e)); ("len", Types.Int Types.I64) ]
| Types.Option e ->
composite (Types.to_string t)
[ ("tag", Types.Int Types.U8); ("value", e) ]
@@ -888,7 +888,7 @@ let rec dty m d (t : Types.t) : int =
would put the reader's offsets out by one. *)
| Types.Vec e ->
composite (Types.to_string t)
- [ ("ptr", Types.Ptr e); ("len", Types.Int Types.I64);
+ [ ("ptr", Types.Ptr (Types.Mut, e)); ("len", Types.Int Types.I64);
("cap", Types.Int Types.I64); ("allocator", Types.Alloc);
("epoch", Types.Int Types.I64) ]
(* Five fields again, and shown as five for the same reason: a debugger
@@ -898,7 +898,7 @@ let rec dty m d (t : Types.t) : int =
describing a field that is not there. *)
| Types.Map (k, v) ->
composite (Types.to_string t)
- [ ("data", Types.Ptr (Types.Int Types.U8));
+ [ ("data", Types.Ptr (Types.Mut, (Types.Int Types.U8)));
("len", Types.Int Types.I64); ("log2cap", Types.Int Types.I64);
("allocator", Types.Alloc); ("epoch", Types.Int Types.I64) ]
|> fun n -> ignore k; ignore v; n
@@ -913,7 +913,7 @@ let rec dty m d (t : Types.t) : int =
locals, where they are under the names the source gave them. *)
| Types.Fn _ ->
composite (Types.to_string t)
- [ ("code", Types.Ptr Types.Unit); ("env", Types.Ptr Types.Unit) ]
+ [ ("code", Types.Ptr (Types.Mut, Types.Unit)); ("env", Types.Ptr (Types.Mut, Types.Unit)) ]
(* And the bare one is what it always was: a pointer to code, and lldb
is told exactly that and no more. DWARF has DW_TAG_subroutine_type
for the signature behind it, and spelling one out would buy a reader
@@ -2568,7 +2568,7 @@ and place f (p : Tast.place) : string * Types.t =
| Tast.Pindex (target, idx) -> element_addr f target idx
| Tast.Pderef target ->
let t = match target.Tast.ty with
- | Types.Ptr t -> t | t -> internal "deref of %s" (Types.to_string t)
+ | Types.Ptr (_, t) -> t | t -> internal "deref of %s" (Types.to_string t)
in
value f target, t
diff --git a/lib/render.ml b/lib/render.ml
index d45251b6..c5cf9f6d 100644
--- a/lib/render.ml
+++ b/lib/render.ml
@@ -193,7 +193,7 @@ let rec render ?(refuse = print_refusal) c depth (e : Tast.expr) : Tast.expr lis
An address the registry never saw is neither: it prints []. That
is a stack local, a global, or a pointer from C, and the shadow stack
and the static type table already answer for the first two by name. *)
- | Types.Ptr t ->
+ | Types.Ptr (_, t) ->
(match c.ptrs with
| None -> [ lit "" ]
| Some pt ->
diff --git a/lib/session.ml b/lib/session.ml
index b86df0e4..2aba91a8 100644
--- a/lib/session.ml
+++ b/lib/session.ml
@@ -1202,12 +1202,12 @@ let externs : Tast.extern list =
is. See [render_locals]. *)
{ Tast.ename = "flan/dev-slot"; esym = "flan_agent_frame_slot";
eparams = [ Types.Int Types.I64; Types.Int Types.I64 ];
- eret = Types.Ptr (Types.Int Types.U8); eloc = Loc.unknown };
+ eret = Types.Ptr (Types.Mut, (Types.Int Types.U8)); eloc = Loc.unknown };
(* The condition the stopped program is holding, same contract: the agent
resolves it against the snapshot on top when the thunk runs, and NULL
when there is none. See [render_condition]. *)
{ Tast.ename = "flan/dev-cond"; esym = "flan_agent_condition";
- eparams = []; eret = Types.Ptr (Types.Int Types.U8);
+ eparams = []; eret = Types.Ptr (Types.Mut, (Types.Int Types.U8));
eloc = Loc.unknown };
(* The character beside a rendered byte. See [Render.pointers]. *)
{ Tast.ename = "flan/dev-emit-u8-char"; esym = "flan_dev_emit_u8_char";
@@ -1232,10 +1232,10 @@ let externs : Tast.extern list =
written" is already the right rendering for an address the registry
never saw. *)
{ Tast.ename = "flan/reg-live"; esym = "flan_dev_reg_live";
- eparams = [ Types.Ptr (Types.Int Types.U8) ];
+ eparams = [ Types.Ptr (Types.Mut, (Types.Int Types.U8)) ];
eret = Types.Int Types.I32; eloc = Loc.unknown };
{ Tast.ename = "flan/reg-emit"; esym = "flan_dev_reg_emit";
- eparams = [ Types.Ptr (Types.Int Types.U8) ];
+ eparams = [ Types.Ptr (Types.Mut, (Types.Int Types.U8)) ];
eret = Types.Int Types.I32; eloc = Loc.unknown } ]
(* The REPL's emitter. Each piece is one extern call: the dev runtime already
@@ -1264,8 +1264,8 @@ let dev_pointers : Render.pointers =
let ask name (p : Tast.expr) : Tast.expr =
let loc = p.Tast.loc in
let byte =
- { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Int Types.U8)), [ p ]);
- ty = Types.Ptr (Types.Int Types.U8); loc }
+ { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, (Types.Int Types.U8))), [ p ]);
+ ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
in
{ Tast.e = Tast.Call (name, [ byte ]); ty = i32; loc }
in
@@ -1405,11 +1405,11 @@ let render_locals ?(origin = "") t ~frame ~(fn : Tast.fn) ~bound
in
let address =
{ Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx i ]);
- ty = Types.Ptr (Types.Int Types.U8); loc }
+ ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
in
let typed =
- { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]);
- ty = Types.Ptr ty; loc }
+ { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]);
+ ty = Types.Ptr (Types.Mut, ty); loc }
in
let v = { Tast.e = Tast.Deref typed; ty; loc } in
match Render.render c 0 v with
@@ -1513,11 +1513,11 @@ let render_condition t ~(st : Tast.structure) : change * (string * string) list
let cty = Types.Named st.Tast.sname in
let address =
{ Tast.e = Tast.Call ("flan/dev-cond", []);
- ty = Types.Ptr (Types.Int Types.U8); loc }
+ ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
in
let typed =
- { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr cty), [ address ]);
- ty = Types.Ptr cty; loc }
+ { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, cty)), [ address ]);
+ ty = Types.Ptr (Types.Mut, cty); loc }
in
let root = { Tast.e = Tast.Deref typed; ty = cty; loc } in
let one i (f : Tast.field) =
@@ -1770,11 +1770,11 @@ let render_slot ?(origin = "") t ~frame ~(fn : Tast.fn) ~slot ~path
let ty = fn.Tast.slots.(slot) in
let address =
{ Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx slot ]);
- ty = Types.Ptr (Types.Int Types.U8); loc }
+ ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
in
let typed =
- { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]);
- ty = Types.Ptr ty; loc }
+ { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]);
+ ty = Types.Ptr (Types.Mut, ty); loc }
in
let root = { Tast.e = Tast.Deref typed; ty; loc } in
let rec walk v = function
@@ -1805,7 +1805,7 @@ let render_slot ?(origin = "") t ~frame ~(fn : Tast.fn) ~slot ~path
Tast.Prim
(Tast.Cast (Types.Int Types.I64),
[ { Tast.e = Tast.Prim (Tast.AddrOf, [ v ]);
- ty = Types.Ptr v.Tast.ty; loc } ]);
+ ty = Types.Ptr (Types.Mut, v.Tast.ty); loc } ]);
ty = Types.Int Types.I64; loc }
in
let newline =
@@ -1985,11 +1985,11 @@ let write_slot ?(origin = "") t ~frame ~(fn : Tast.fn) ~slot ~path
let ty = fn.Tast.slots.(slot) in
let address =
{ Tast.e = Tast.Call ("flan/dev-slot", [ idx frame; idx slot ]);
- ty = Types.Ptr (Types.Int Types.U8); loc }
+ ty = Types.Ptr (Types.Mut, (Types.Int Types.U8)); loc }
in
let typed =
- { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr ty), [ address ]);
- ty = Types.Ptr ty; loc }
+ { Tast.e = Tast.Prim (Tast.Cast (Types.Ptr (Types.Mut, ty)), [ address ]);
+ ty = Types.Ptr (Types.Mut, ty); loc }
in
let root = { Tast.e = Tast.Deref typed; ty; loc } in
let rec walk v = function
diff --git a/lib/shim.ml b/lib/shim.ml
index 2c590440..e185d325 100644
--- a/lib/shim.ml
+++ b/lib/shim.ml
@@ -221,6 +221,8 @@ let rec cty env ~needed ~loc ~what (t : Ast.texpr) : string =
else
fail loc "%s is %s, which is not a type this shim generator knows" what n)
| Ast.Tapp ("Ptr", [ e ]) -> cty env ~needed ~loc ~what e ^ " *"
+ | Ast.Tapp ("Ptr", [ { Ast.t = Ast.Tname "const"; _ }; e ]) ->
+ "const " ^ cty env ~needed ~loc ~what e ^ " *"
| Ast.Tapp ("Option", _) ->
fail loc
"%s is an Option, which C has no shape for — declare what C returns and \
diff --git a/lib/types.ml b/lib/types.ml
index 7ef1cd4d..bccd930a 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -43,7 +43,7 @@ type t =
| Slice of access * t (* [T] [const T] ptr+len, non-owning *)
| Array of int64 * t (* [n T] inline, a value, copies *)
| Map of t * t (* (Map K V) *)
- | Ptr of t (* (Ptr T) *)
+ | Ptr of access * t (* (Ptr T) (Ptr const T) *)
(* [Allocator]: a builtin opaque type, the way [string] is a builtin
ptr+len. It is a [Types.t] case with no user-writable constructor, which
is what lets spec-memory.md's "procedure plus an opaque data pointer" be
@@ -193,7 +193,7 @@ let rec equal a b =
| Slice (a, x), Slice (b, y) -> a = b && equal x y
| Array (n, x), Array (m, y) -> Int64.equal n m && equal x y
| Map (k, v), Map (k', v') -> equal k k' && equal v v'
- | Ptr x, Ptr y -> equal x y
+ | Ptr (a, x), Ptr (b, y) -> a = b && equal x y
| Alloc, Alloc -> true
| Vec x, Vec y -> equal x y
| Option x, Option y -> equal x y
@@ -219,7 +219,8 @@ let rec to_string = function
| Slice (Const, t) -> "[const " ^ to_string t ^ "]"
| Array (n, t) -> Printf.sprintf "[%Ld %s]" n (to_string t)
| Map (k, v) -> Printf.sprintf "(Map %s %s)" (to_string k) (to_string v)
- | Ptr t -> "(Ptr " ^ to_string t ^ ")"
+ | Ptr (Mut, t) -> "(Ptr " ^ to_string t ^ ")"
+ | Ptr (Const, t) -> "(Ptr const " ^ to_string t ^ ")"
| Alloc -> "Allocator"
| Vec t -> "(Vec " ^ to_string t ^ ")"
| Option t -> "(Option " ^ to_string t ^ ")"
@@ -344,7 +345,8 @@ let join a b =
same at run time. *)
let rec const_widens ~(from : t) ~(into : t) =
match from, into with
- | Slice (_, a), Slice (Const, b) -> equal a b || const_widens ~from:a ~into:b
+ | Slice (_, a), Slice (Const, b) | Ptr (_, a), Ptr (Const, b) ->
+ equal a b || const_widens ~from:a ~into:b
| _ -> false
(* A function of one signature standing where another is wanted, when the
diff --git a/lib/x86.ml b/lib/x86.ml
index 7b1f5521..fd80d5f8 100644
--- a/lib/x86.ml
+++ b/lib/x86.ml
@@ -1554,7 +1554,7 @@ type arg =
move-only container by address. *)
let classify_c (l : loc) (t : Types.t) =
match t with
- | Types.String | Types.Slice _ -> [ Aint (l, Types.Ptr Types.Unit); Alen l ]
+ | Types.String | Types.Slice _ -> [ Aint (l, Types.Ptr (Types.Mut, Types.Unit)); Alen l ]
| Types.Unit | Types.Never -> []
| Types.Vec _ | Types.Map _ -> [ Aptr l ]
(* A fixed array crossing into a dyn view (M2 item 3) needs its address for
@@ -1816,7 +1816,7 @@ and lower_at f (e : Tast.expr) (dst : loc) : unit =
store_int f.b ~src:rax ~mm:(lmem f dst ~scratch:r11) ~size:8;
(match env with
| None -> xor_rr f.b ~dst:rax ~src:rax
- | Some ev -> let l = eval f ev in load_loc f ~reg:rax l (Types.Ptr Types.Unit));
+ | Some ev -> let l = eval f ev in load_loc f ~reg:rax l (Types.Ptr (Types.Mut, Types.Unit)));
store_int f.b ~src:rax ~mm:(lmem f (shift dst 8) ~scratch:r11) ~size:8
| Tast.FnAddr r ->
fnaddr_at f ~loc:e.Tast.loc ~reg:rax r;
@@ -1844,7 +1844,7 @@ and lower_at f (e : Tast.expr) (dst : loc) : unit =
let c = eval f callee in
let env =
match callee.Tast.ty with
- | Types.Fn _ -> Some (Aint (shift c 8, Types.Ptr Types.Unit))
+ | Types.Fn _ -> Some (Aint (shift c 8, Types.Ptr (Types.Mut, Types.Unit)))
| _ -> None
in
call_flan f ?env ~target:(`Loc c) ~args ~rty:t dst
@@ -2059,7 +2059,7 @@ and emit_handled f frames body dst t =
(match h.Tast.henv with
| Some ev ->
let l = scoped f (fun () -> eval f ev) in
- load_loc f ~reg:rax l (Types.Ptr Types.Unit)
+ load_loc f ~reg:rax l (Types.Ptr (Types.Mut, Types.Unit))
| None -> xor_rr f.b ~dst:rax ~src:rax);
store_int f.b ~src:rax ~mm:(Frame (slot + h_env)) ~size:8;
lea f.b ~dst:rdi ~mm:(Frame slot);
@@ -2573,7 +2573,7 @@ and emit_match f (scrut : Tast.expr) (arms : Tast.arm list) dst t =
and field_loc f (base : loc) (ty : Types.t) i =
match ty with
| Types.Named sn -> shift base (List.nth (field_offsets f sn) i)
- | Types.Ptr (Types.Named sn) ->
+ | Types.Ptr (_, (Types.Named sn)) ->
shift (Lp (off_of base, 0)) (List.nth (field_offsets f sn) i)
| Types.String | Types.Slice _ -> shift base (if i = 0 then 0 else 8)
| Types.Option el -> let ot, ov = option_lay f el in
@@ -2606,7 +2606,7 @@ and elements f (base : loc) (ty : Types.t) (is : Tast.expr list) : loc =
| i :: rest ->
let elem =
match ty with
- | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr el -> el
+ | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr (_, el) -> el
| Types.String -> Types.Int Types.U8
| t -> unsupported "index into %s" (Types.to_string t)
in
@@ -2904,7 +2904,7 @@ and check_cast f (loc : Loc.t) (src : Types.fkind) (k : Types.ikind) =
and element f (base : loc) (ty : Types.t) (i : Tast.expr) : loc =
let elem =
match ty with
- | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr el -> el
+ | Types.Array (_, el) | Types.Slice (_, el) | Types.Ptr (_, el) -> el
| Types.String -> Types.Int Types.U8
| t -> unsupported "index into %s" (Types.to_string t)
in
@@ -2966,7 +2966,7 @@ and call_flan f ?env ~target ~args ~rty dst =
in
(* The channel is this frame's own: a callee that transfers writes through
the pointer we were handed, so one cell serves the whole chain. *)
- let chan = [ Aint (Lf f.xfer_off, Types.Ptr Types.Unit) ] in
+ let chan = [ Aint (Lf f.xfer_off, Types.Ptr (Types.Mut, Types.Unit)) ] in
(* And the environment last of all, on exactly one kind of call: one through
a [(Fn ...)] value, which cannot know whether the body it reaches
declared one. Every other call passes what it always passed — this is
@@ -3074,7 +3074,7 @@ and call_native f ~sym ?(chan = false) ~(args : Tast.expr list) ~rty dst =
args
in
let flat = List.concat_map (fun (l, ty) -> classify_c l ty) vals in
- let flat = if chan then flat @ [ Aint (Lf f.xfer_off, Types.Ptr Types.Unit) ] else flat in
+ let flat = if chan then flat @ [ Aint (Lf f.xfer_off, Types.Ptr (Types.Mut, Types.Unit)) ] else flat in
let nsse = emit_args f flat in
(* [al] is how many SSE registers were used, which a variadic callee reads.
Harmless on a fixed one, and a [declare] does not say which it is. *)
diff --git a/runtime/flan_dev.c b/runtime/flan_dev.c
index ec4e0e3f..82c1120c 100644
--- a/runtime/flan_dev.c
+++ b/runtime/flan_dev.c
@@ -2325,7 +2325,7 @@ static void crash_handler(int sig, siginfo_t *si, void *uc) {
}
{
static const char why[] =
- "\nflan: a write through a pointer into read-only memory, "
+ "\nflan: a write into read-only memory, "
"a null, or a stack overflow\n";
crash_puts(why, sizeof why - 1);
}
diff --git a/spike/x86/survey.sh b/spike/x86/survey.sh
index c6b9a598..c0c58015 100755
--- a/spike/x86/survey.sh
+++ b/spike/x86/survey.sh
@@ -95,10 +95,10 @@ forever="dev-loop dev-watch dev-chatty agent-auto"
# sweep now and they are five of the MATCHes.
# The one whose whole point is a fault, and which therefore cannot be compared
-# at this sweep's optimisation level. dev-segv stores through a pointer to a
-# string literal's bytes, which is a store into .rodata: LLVM at -O2 deletes it
-# as undefined and exits 0, and this backend has no optimiser and exits 139.
-# That is not a lowering disagreement. test_dev.ml builds it in a dev session,
+# at this sweep's optimisation level. dev-segv stores through a null pointer,
+# which is undefined: what LLVM at -O2 does with it is its own business, and
+# this backend has no optimiser and exits 139. That is not a lowering
+# disagreement. test_dev.ml builds it in a dev session,
# where the fault is the thing asserted. It also calls agent/start, so it
# leaves a socket in /tmp on both runs, and under SURVEY_FLAGS=--dev it parks
# in the break loop instead of dying.
diff --git a/test/programs/const-slice.flan b/test/programs/const-slice.flan
index 6ab1db0f..3c64505f 100644
--- a/test/programs/const-slice.flan
+++ b/test/programs/const-slice.flan
@@ -18,6 +18,9 @@
(set n (+ n (length (at parts i)))))
n))
+;; A (Ptr const T) is what the address of read-only storage is.
+(defn peek [p (Ptr const u8)] u8 (deref p))
+
;; A function that only reads stands where one that may write is wanted, and
;; one returning a writable slice where a read-only one is wanted.
(defn rd [s [const u8]] i32 (length s))
@@ -54,5 +57,9 @@
(println (string (slice (join (slice f) (bytes-view "-"))))))
(println (at r 0))
(println (call-rd rd) (call-bare rd) (call-mk mk))
+ (let [b (bytes "q")]
+ (println (peek (addr (at r 1))) (peek (addr (at "abc" 2)))
+ (peek (addr (at b 0)))
+ (string (slice-from-ptr (addr (at r 7)) 5))))
(free names))
0)
diff --git a/test/programs/dev-segv.flan b/test/programs/dev-segv.flan
index 1ea5ca31..95ce1f54 100644
--- a/test/programs/dev-segv.flan
+++ b/test/programs/dev-segv.flan
@@ -1,22 +1,21 @@
-;;;; The dogfooding crash, replayed on purpose: a store through a pointer to
-;;;; a string literal's bytes lands in read-only memory and takes SIGSEGV. In
-;;;; a dev session that used to kill the whole process — daemon, compiler and
-;;;; socket together, with no message at all. The dev build's crash handler
-;;;; turns it into the same park the no-channel traps take: one line naming
-;;;; the address and the frame, then the break loop, with the daemon alive
-;;;; and answering behind it. There is no restart to list — a faulting
-;;;; instruction has nowhere to resume at — which is the same empty-list
-;;;; shape dev-trap-null-alloc.flan pins for free-all.
+;;;; A hardware fault, taken on purpose: a store through a null pointer takes
+;;;; SIGSEGV. In a dev session that used to kill the whole process — daemon,
+;;;; compiler and socket together, with no message at all. The dev build's
+;;;; crash handler turns it into the same park the no-channel traps take: one
+;;;; line naming the address and the frame, then the break loop, with the
+;;;; daemon alive and answering behind it. There is no restart to list — a
+;;;; faulting instruction has nowhere to resume at — which is the same
+;;;; empty-list shape dev-trap-null-alloc.flan pins for free-all.
;;;;
-;;;; Through a pointer, because a store through the [const u8] itself is
-;;;; refused at compile time; a (Ptr T) is the C boundary, where nothing is
-;;;; checked.
+;;;; The crash that first raised this was a write through a bytes-view of a
+;;;; string literal, which no longer compiles; a zeroed pointer is the
+;;;; surviving way to fault.
(import agent "vendor:agent")
+(defonce nowhere (Ptr u8))
+
(defn main [] i32
(agent/start "/tmp/flan-dev-segv-fallback.sock")
- (let [v (bytes-view "INSERTIONSORT")
- p (addr (at v 0))]
- (set (deref p) \Z)
- (print (string v))
- 0))
+ (set (deref nowhere) \Z)
+ (println "not reached")
+ 0)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 4ef0165a..f06512f6 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -872,7 +872,7 @@ let () =
(* [const T]: the checker's alone, so the three builds agree and every
row is about which values reach which parameters. *)
let const_slice_out =
- "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n3 4 2\n"
+ "6 5\n1 122\nhello world 5\ntrue true\n10\n5\nAb\na-b-c\n104\n3 4 2\n101 99 113 world\n"
in
outputs "const slices" "programs/const-slice.flan" const_slice_out;
outputs ~opt:"-O0" "const slices, -O0" "programs/const-slice.flan"
diff --git a/test/test_dev.ml b/test/test_dev.ml
index 7701bb2d..46af004a 100644
--- a/test/test_dev.ml
+++ b/test/test_dev.ml
@@ -1922,7 +1922,7 @@ let () =
if refault then begin
let faulting =
"(:op \"eval-expr\" :code \
- \"(let [v (bytes-view \\\"refault\\\") p (addr (at v 0))] (set (deref p) 90) 1)\" \
+ \"(do (set (deref nowhere) 90) 1)\" \
:file \"/tmp/buf.flan\")"
in
(match ask faulting with _ -> () | exception _ -> ());
@@ -2028,9 +2028,8 @@ let () =
word. The dev build's crash handler (flan_dev_crash_enable) enters the
same trap hook the six no-channel refusals use, so everything trap_park
asserts for them holds here too: stopped and describable, an eval still
- answered, a resume refused. The program writes through a pointer to
- a literal's bytes, which is the surviving spelling of that crash: a
- store through the bytes-view itself no longer compiles. *)
+ answered, a resume refused. The program stores through a null
+ pointer: the bytes-view write that first crashed no longer compiles. *)
trap_park ~refault:true "segfault" "dev-segv.flan" "SegFault" [];
(* ── The locals of a stopped frame ─────────────────────────────── *)
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 77abd557..adc0a418 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2238,12 +2238,10 @@ let () =
rejects_check "set through a string's slice"
"(defn f [s string] () (set (at (slice s 1) 0) 65))"
~needle:"not a place";
- (* The address of one is the same question and gets the same answer, so
- the message has to fit a reader who asked for a pointer and not a
- store. *)
- rejects_check "the address of a string's byte"
+ (* The address of one is a (Ptr const u8), so it is not a (Ptr u8). *)
+ rejects_check "the address of a string's byte is read-only"
"(defn f [s string] (Ptr u8) (addr (at s 0)))"
- ~needle:"(at s i) is a value and not a place";
+ ~needle:"expected (Ptr u8), found (Ptr const u8)";
(* And a string is still not a [u8]: slicing one does not smuggle a byte
slice out of it. *)
rejects_check "a string slice is not a byte slice"
@@ -2322,6 +2320,47 @@ let () =
"(defn mk [] [const u8] (bytes-view \"a\")) \
(defn c [f (Fn [] [u8])] i32 0) (defn m [] i32 (c mk))"
~needle:"expected (Fn [] [u8]), found (CFn [] [const u8])";
+ (* (Ptr const T): the pointer beside [const T]. *)
+ infers "the address of a const element" "(addr (at (bytes-view \"hi\") 0))"
+ "(Ptr const u8)";
+ infers "the address of a string's byte" "(addr (at \"hi\" 0))"
+ "(Ptr const u8)";
+ infers "a const pointer slices to a const slice"
+ "(slice-from-ptr (addr (at (bytes-view \"hi\") 0)) 2)" "[const u8]";
+ rejects_check "a store through a const pointer"
+ "(defn f [p (Ptr const i32)] () (set (deref p) 1))"
+ ~needle:"this writes through a (Ptr const i32)";
+ rejects_check "a store through the address of a const element"
+ "(defn f [v [const u8]] () (set (deref (addr (at v 0))) 1))"
+ ~needle:"this writes through a (Ptr const u8)";
+ rejects_check "a store through the address of a string's byte"
+ "(defn f [s string] () (set (deref (addr (at s 0))) 1))"
+ ~needle:"this writes through a (Ptr const u8)";
+ rejects_check "a field store through a const pointer"
+ "(defstruct P [x i32]) (defn f [p (Ptr const P)] () (set (.x p) 1))"
+ ~needle:"this writes through a (Ptr const P)";
+ rejects_check "a push through a const pointer"
+ "(defn f [p (Ptr const (Vec i32))] () (push (deref p) 1))"
+ ~needle:"behind a (Ptr const (Vec i32))";
+ rejects_check "a const pointer is not a writable one"
+ "(defn g [p (Ptr u8)] i32 0) (defn f [v [const u8]] i32 (g (addr (at v 0))))"
+ ~needle:"expected (Ptr u8), found (Ptr const u8)";
+ rejects_check "slice-from-ptr keeps the const"
+ "(defn f [v [const u8]] [u8] (slice-from-ptr (addr (at v 0)) 1))"
+ ~needle:"expected [u8], found [const u8]";
+ rejects_check "const alone is not a type" "(defn f [p (Ptr const)] i32 0)"
+ ~needle:"const is not a type on its own";
+ rejects_check "no conversion under a writable pointer"
+ "(defn f [p (Ptr (Ptr i32))] (Ptr (Ptr const i32)) p)"
+ ~needle:"expected (Ptr (Ptr const i32)), found (Ptr (Ptr i32))";
+ accepts "a writable pointer is a const one"
+ "(defn f [p (Ptr i32)] (Ptr const i32) p)";
+ accepts "and under a const pointer, one level down"
+ "(defn f [p (Ptr (Ptr i32))] (Ptr const (Ptr const i32)) p)";
+ accepts "a generic const pointer binds from a writable one"
+ "(defn f [p (Ptr const $t)] $t (deref p)) (defn g [q (Ptr i32)] i32 (f q))";
+ accepts "vec-new reads (Ptr const u8) as a type"
+ "(defn f [] i32 (let [v (vec-new (Ptr const u8))] (length v)))";
rejects_check "const is not a name a constant can have"
"(defconst const 4)" ~needle:"const cannot be declared";
(* The const is shallow: an element of a [const [u8]] is a writable [u8]. *)
@@ -2334,7 +2373,7 @@ let () =
accepts "under a const slice the element converts too"
"(defn g [p [const [const u8]]] i32 0) (defn f [p [[u8]]] i32 (g p))";
accepts "the address of a const element, for C"
- "(defn f [s [const u8]] (Ptr u8) (addr (at s 0)))";
+ "(defn f [s [const u8]] (Ptr const u8) (addr (at s 0)))";
accepts "a generic reader takes both"
"(defn f [a [const i32] b [i32]] i64 (+ (sum-i32 a) (sum-i32 b)))";
@@ -4503,8 +4542,9 @@ let () =
something different in a parameter than it does anywhere else. *)
emits "const char * as a string parameter"
"(declare-c name-length [text string] i32 \"name_length\")";
- emits "a pointer parameter"
- "(declare-c count-at [values (Ptr i32) n i32] i32 \"count_at\")";
+ (* const int * is a pointer C promises not to write through. *)
+ emits "a const pointer parameter"
+ "(declare-c count-at [values (Ptr const i32) n i32] i32 \"count_at\")";
(* struct Pair is both Pair and Point in the header and the package
describes it once, so both names have to land on the one defstruct —
raylib does exactly this with Texture2D and TextureCubemap. *)
@@ -5140,6 +5180,10 @@ let () =
"(declare-c name-length [text string] i32 \"name_length\")";
agreed "a pointer that matches the header exactly"
"(declare-c count-at [values (Ptr i32) n i32] i32 \"count_at\")";
+ agreed "a const pointer that matches the header exactly"
+ "(declare-c count-at [values (Ptr const i32) n i32] i32 \"count_at\")";
+ agreed "a const pointer where the header says const void *"
+ "(declare-c blit [dst (Ptr Pair) src (Ptr const Shade) n i32] \"blit\")";
(* void * is opaque about what it points at, so there is no element type in
the header to disagree with — §A.2's LoadImageColors → UpdateTexture. *)
agreed "any pointer where the header says void *"
@@ -5155,12 +5199,17 @@ let () =
name the disagreement. *)
differs "a pointer to the wrong named type"
"(declare-c pair-len-p [p (Ptr Shade)] f32 \"pair_len_p\")"
- "parameter p is (Ptr Shade) and the header says (Ptr Pair)";
+ "parameter p is (Ptr Shade) and the header says (Ptr const Pair)";
differs "a pointer to the wrong width"
"(declare-c count-at [values (Ptr f64) n i32] i32 \"count_at\")"
"parameter values is (Ptr f64)";
(* void * gives up the element type and nothing else. It is still a pointer,
and a scalar declared against one is still a finding. *)
+ (* A (Ptr const T) promises C will not write, and the header has to say so
+ too. *)
+ differs "a const pointer where the header may write"
+ "(declare-c blit [dst (Ptr const u8) src (Ptr u8) n i32] \"blit\")"
+ "parameter dst is (Ptr const u8)";
differs "a scalar where the header says void *"
"(declare-c blit [dst i64 src (Ptr u8) n i32] \"blit\")"
"parameter dst is i64";
diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml
index b381a2fe..fad8cea3 100644
--- a/test/test_sanitize.ml
+++ b/test/test_sanitize.ml
@@ -441,9 +441,8 @@ let dev_sweep () =
sanitized run must produce ASan's report and must NOT produce the
handler's line, and that is the assertion.
- And it has to be built at -O0. At the sweep's -O2 the write through a
- pointer to a string literal's bytes does not fault at all — measured, both
- builds print the unmodified string — so a case that is about what happens
+ And it has to be built at -O0. At the sweep's -O2 a store through a null
+ pointer is undefined and need not fault — so a case that is about what happens
on a fault has to be compiled where the fault happens. Same family as the
-O0/-O2 split [unchecked_controls] records for bounds.flan.
diff --git a/vendor/raylib/generated.flan b/vendor/raylib/generated.flan
index 7ff58dbd..2ce0d70f 100644
--- a/vendor/raylib/generated.flan
+++ b/vendor/raylib/generated.flan
@@ -78,7 +78,7 @@
(declare-c load-file-data [file-name string data-size (Ptr i32)] (Ptr u8) "LoadFileData")
(declare-c unload-file-data [data (Ptr u8)] "UnloadFileData")
(declare-c save-file-data [file-name string data (Ptr u8) data-size i32] bool "SaveFileData")
-(declare-c export-data-as-code [data (Ptr u8) data-size i32 file-name string] bool "ExportDataAsCode")
+(declare-c export-data-as-code [data (Ptr const u8) data-size i32 file-name string] bool "ExportDataAsCode")
(declare-c file-exists [file-name string] bool "FileExists")
(declare-c directory-exists [dir-path string] bool "DirectoryExists")
(declare-c file-extension? [file-name string ext string] bool "IsFileExtension")
@@ -95,9 +95,9 @@
(declare-c path-file? [path string] bool "IsPathFile")
(declare-c file-name-valid? [file-name string] bool "IsFileNameValid")
(declare-c file-dropped? [] bool "IsFileDropped")
-(declare-c compress-data [data (Ptr u8) data-size i32 comp-data-size (Ptr i32)] (Ptr u8) "CompressData")
-(declare-c decompress-data [comp-data (Ptr u8) comp-data-size i32 data-size (Ptr i32)] (Ptr u8) "DecompressData")
-(declare-c decode-data-base-64 [data (Ptr u8) output-size (Ptr i32)] (Ptr u8) "DecodeDataBase64")
+(declare-c compress-data [data (Ptr const u8) data-size i32 comp-data-size (Ptr i32)] (Ptr u8) "CompressData")
+(declare-c decompress-data [comp-data (Ptr const u8) comp-data-size i32 data-size (Ptr i32)] (Ptr u8) "DecompressData")
+(declare-c decode-data-base-64 [data (Ptr const u8) output-size (Ptr i32)] (Ptr u8) "DecodeDataBase64")
(declare-c compute-crc32 [data (Ptr u8) data-size i32] u32 "ComputeCRC32")
(declare-c compute-md5 [data (Ptr u8) data-size i32] (Ptr u32) "ComputeMD5")
(declare-c compute-sha1 [data (Ptr u8) data-size i32] (Ptr u32) "ComputeSHA1")
@@ -117,7 +117,7 @@
(declare-c set-mouse-scale [scale-x f32 scale-y f32] "SetMouseScale")
(declare-c get-mouse-wheel-move-v [] Vector2 "GetMouseWheelMoveV")
(declare-c update-camera-pro [camera (Ptr Camera3D) movement Vector3 rotation Vector3 zoom f32] "UpdateCameraPro")
-(declare-c draw-line-strip-raw [points (Ptr Vector2) point-count i32 color Color] "DrawLineStrip")
+(declare-c draw-line-strip-raw [points (Ptr const Vector2) point-count i32 color Color] "DrawLineStrip")
(declare-c draw-line-bezier [start-pos Vector2 end-pos Vector2 thick f32 color Color] "DrawLineBezier")
(declare-c draw-circle-sector [center Vector2 radius f32 start-angle f32 end-angle f32 segments i32 color Color] "DrawCircleSector")
(declare-c draw-circle-sector-lines [center Vector2 radius f32 start-angle f32 end-angle f32 segments i32 color Color] "DrawCircleSectorLines")
@@ -126,16 +126,16 @@
(declare-c draw-rectangle-gradient-v [pos-x i32 pos-y i32 width i32 height i32 top Color bottom Color] "DrawRectangleGradientV")
(declare-c draw-rectangle-gradient-h [pos-x i32 pos-y i32 width i32 height i32 left Color right Color] "DrawRectangleGradientH")
(declare-c draw-rectangle-gradient-ex [rec Rectangle top-left Color bottom-left Color top-right Color bottom-right Color] "DrawRectangleGradientEx")
-(declare-c draw-triangle-fan-raw [points (Ptr Vector2) point-count i32 color Color] "DrawTriangleFan")
-(declare-c draw-triangle-strip-raw [points (Ptr Vector2) point-count i32 color Color] "DrawTriangleStrip")
+(declare-c draw-triangle-fan-raw [points (Ptr const Vector2) point-count i32 color Color] "DrawTriangleFan")
+(declare-c draw-triangle-strip-raw [points (Ptr const Vector2) point-count i32 color Color] "DrawTriangleStrip")
(declare-c draw-poly [center Vector2 sides i32 radius f32 rotation f32 color Color] "DrawPoly")
(declare-c draw-poly-lines [center Vector2 sides i32 radius f32 rotation f32 color Color] "DrawPolyLines")
(declare-c draw-poly-lines-ex [center Vector2 sides i32 radius f32 rotation f32 line-thick f32 color Color] "DrawPolyLinesEx")
-(declare-c draw-spline-linear-raw [points (Ptr Vector2) point-count i32 thick f32 color Color] "DrawSplineLinear")
-(declare-c draw-spline-basis-raw [points (Ptr Vector2) point-count i32 thick f32 color Color] "DrawSplineBasis")
-(declare-c draw-spline-catmull-rom-raw [points (Ptr Vector2) point-count i32 thick f32 color Color] "DrawSplineCatmullRom")
-(declare-c draw-spline-bezier-quadratic-raw [points (Ptr Vector2) point-count i32 thick f32 color Color] "DrawSplineBezierQuadratic")
-(declare-c draw-spline-bezier-cubic-raw [points (Ptr Vector2) point-count i32 thick f32 color Color] "DrawSplineBezierCubic")
+(declare-c draw-spline-linear-raw [points (Ptr const Vector2) point-count i32 thick f32 color Color] "DrawSplineLinear")
+(declare-c draw-spline-basis-raw [points (Ptr const Vector2) point-count i32 thick f32 color Color] "DrawSplineBasis")
+(declare-c draw-spline-catmull-rom-raw [points (Ptr const Vector2) point-count i32 thick f32 color Color] "DrawSplineCatmullRom")
+(declare-c draw-spline-bezier-quadratic-raw [points (Ptr const Vector2) point-count i32 thick f32 color Color] "DrawSplineBezierQuadratic")
+(declare-c draw-spline-bezier-cubic-raw [points (Ptr const Vector2) point-count i32 thick f32 color Color] "DrawSplineBezierCubic")
(declare-c draw-spline-segment-linear [p-1 Vector2 p-2 Vector2 thick f32 color Color] "DrawSplineSegmentLinear")
(declare-c draw-spline-segment-basis [p-1 Vector2 p-2 Vector2 p-3 Vector2 p-4 Vector2 thick f32 color Color] "DrawSplineSegmentBasis")
(declare-c draw-spline-segment-catmull-rom [p-1 Vector2 p-2 Vector2 p-3 Vector2 p-4 Vector2 thick f32 color Color] "DrawSplineSegmentCatmullRom")
@@ -148,7 +148,7 @@
(declare-c get-spline-point-bezier-cubic [p-1 Vector2 c-2 Vector2 c-3 Vector2 p-4 Vector2 t f32] Vector2 "GetSplinePointBezierCubic")
(declare-c load-image-raw [file-name string width i32 height i32 format i32 header-size i32] Image "LoadImageRaw")
(declare-c load-image-anim [file-name string frames (Ptr i32)] Image "LoadImageAnim")
-(declare-c load-image-anim-from-memory [file-type string file-data (Ptr u8) data-size i32 frames (Ptr i32)] Image "LoadImageAnimFromMemory")
+(declare-c load-image-anim-from-memory [file-type string file-data (Ptr const u8) data-size i32 frames (Ptr i32)] Image "LoadImageAnimFromMemory")
(declare-c load-image-from-texture [texture Texture2D] Image "LoadImageFromTexture")
(declare-c load-image-from-screen [] Image "LoadImageFromScreen")
(declare-c export-image-to-memory [image Image file-type string file-size (Ptr i32)] (Ptr u8) "ExportImageToMemory")
@@ -171,7 +171,7 @@
(declare-c image-alpha-mask [image (Ptr Image) alpha-mask Image] "ImageAlphaMask")
(declare-c image-alpha-premultiply [image (Ptr Image)] "ImageAlphaPremultiply")
(declare-c image-blur-gaussian [image (Ptr Image) blur-size i32] "ImageBlurGaussian")
-(declare-c image-kernel-convolution [image (Ptr Image) kernel (Ptr f32) kernel-size i32] "ImageKernelConvolution")
+(declare-c image-kernel-convolution [image (Ptr Image) kernel (Ptr const f32) kernel-size i32] "ImageKernelConvolution")
(declare-c image-resize-canvas [image (Ptr Image) new-width i32 new-height i32 offset-x i32 offset-y i32 fill Color] "ImageResizeCanvas")
(declare-c image-mipmaps [image (Ptr Image)] "ImageMipmaps")
(declare-c image-dither [image (Ptr Image) r-bpp i32 g-bpp i32 b-bpp i32 a-bpp i32] "ImageDither")
@@ -211,8 +211,8 @@
(declare-c image-draw-text [dst (Ptr Image) text string pos-x i32 pos-y i32 font-size i32 color Color] "ImageDrawText")
(declare-c image-draw-text-ex [dst (Ptr Image) font Font text string position Vector2 font-size f32 spacing f32 tint Color] "ImageDrawTextEx")
(declare-c load-texture-cubemap [image Image layout i32] Texture2D "LoadTextureCubemap")
-(declare-c update-texture [texture Texture2D pixels (Ptr u8)] "UpdateTexture")
-(declare-c update-texture-rec [texture Texture2D rec Rectangle pixels (Ptr u8)] "UpdateTextureRec")
+(declare-c update-texture [texture Texture2D pixels (Ptr const u8)] "UpdateTexture")
+(declare-c update-texture-rec [texture Texture2D rec Rectangle pixels (Ptr const u8)] "UpdateTextureRec")
(declare-c gen-texture-mipmaps [texture (Ptr Texture2D)] "GenTextureMipmaps")
(declare-c set-texture-wrap [texture Texture2D wrap i32] "SetTextureWrap")
(declare-c color-is-equal [col-1 Color col-2 Color] bool "ColorIsEqual")
@@ -229,13 +229,13 @@
(declare-c set-pixel-color [dst-ptr (Ptr u8) color Color format i32] "SetPixelColor")
(declare-c get-pixel-data-size [width i32 height i32 format i32] i32 "GetPixelDataSize")
(declare-c load-font-from-image [image Image key Color first-char i32] Font "LoadFontFromImage")
-(declare-c load-font-from-memory [file-type string file-data (Ptr u8) data-size i32 font-size i32 codepoints (Ptr i32) codepoint-count i32] Font "LoadFontFromMemory")
-(declare-c load-font-data [file-data (Ptr u8) data-size i32 font-size i32 codepoints (Ptr i32) codepoint-count i32 type i32] (Ptr GlyphInfo) "LoadFontData")
-(declare-c gen-image-font-atlas [glyphs (Ptr GlyphInfo) glyph-recs (Ptr (Ptr Rectangle)) glyph-count i32 font-size i32 padding i32 pack-method i32] Image "GenImageFontAtlas")
+(declare-c load-font-from-memory [file-type string file-data (Ptr const u8) data-size i32 font-size i32 codepoints (Ptr i32) codepoint-count i32] Font "LoadFontFromMemory")
+(declare-c load-font-data [file-data (Ptr const u8) data-size i32 font-size i32 codepoints (Ptr i32) codepoint-count i32 type i32] (Ptr GlyphInfo) "LoadFontData")
+(declare-c gen-image-font-atlas [glyphs (Ptr const GlyphInfo) glyph-recs (Ptr (Ptr Rectangle)) glyph-count i32 font-size i32 padding i32 pack-method i32] Image "GenImageFontAtlas")
(declare-c unload-font-data [glyphs (Ptr GlyphInfo) glyph-count i32] "UnloadFontData")
(declare-c export-font-as-code [font Font file-name string] bool "ExportFontAsCode")
(declare-c draw-text-pro [font Font text string position Vector2 origin Vector2 rotation f32 font-size f32 spacing f32 tint Color] "DrawTextPro")
-(declare-c draw-text-codepoints [font Font codepoints (Ptr i32) codepoint-count i32 position Vector2 font-size f32 spacing f32 tint Color] "DrawTextCodepoints")
+(declare-c draw-text-codepoints [font Font codepoints (Ptr const i32) codepoint-count i32 position Vector2 font-size f32 spacing f32 tint Color] "DrawTextCodepoints")
(declare-c set-text-line-spacing [spacing i32] "SetTextLineSpacing")
(declare-c load-codepoints [text string count (Ptr i32)] (Ptr i32) "LoadCodepoints")
(declare-c unload-codepoints [codepoints (Ptr i32)] "UnloadCodepoints")
@@ -246,7 +246,7 @@
(declare-c text-is-equal [text-1 string text-2 string] bool "TextIsEqual")
(declare-c text-length [text string] u32 "TextLength")
(declare-c text-subtext [text string position i32 length i32] string "TextSubtext")
-(declare-c text-join [text-list (Ptr (Ptr i8)) count i32 delimiter string] string "TextJoin")
+(declare-c text-join [text-list (Ptr const (Ptr i8)) count i32 delimiter string] string "TextJoin")
(declare-c text-split [text string delimiter i8 count (Ptr i32)] (Ptr (Ptr i8)) "TextSplit")
(declare-c text-find-index [text string find string] i32 "TextFindIndex")
(declare-c text-to-upper [text string] string "TextToUpper")
@@ -260,7 +260,7 @@
(declare-c draw-point-3d [position Vector3 color Color] "DrawPoint3D")
(declare-c draw-circle-3d [center Vector3 radius f32 rotation-axis Vector3 rotation-angle f32 color Color] "DrawCircle3D")
(declare-c draw-triangle-3d [v-1 Vector3 v-2 Vector3 v-3 Vector3 color Color] "DrawTriangle3D")
-(declare-c draw-triangle-strip-3d-raw [points (Ptr Vector3) point-count i32 color Color] "DrawTriangleStrip3D")
+(declare-c draw-triangle-strip-3d-raw [points (Ptr const Vector3) point-count i32 color Color] "DrawTriangleStrip3D")
(declare-c draw-cube-wires-v [position Vector3 size Vector3 color Color] "DrawCubeWiresV")
(declare-c draw-sphere-ex [center-pos Vector3 radius f32 rings i32 slices i32 color Color] "DrawSphereEx")
(declare-c draw-cylinder [position Vector3 radius-top f32 radius-bottom f32 height f32 slices i32 color Color] "DrawCylinder")
@@ -286,7 +286,7 @@
(declare-c draw-billboard-rec [camera Camera3D texture Texture2D source Rectangle position Vector3 size Vector2 tint Color] "DrawBillboardRec")
(declare-c draw-billboard-pro [camera Camera3D texture Texture2D source Rectangle position Vector3 up Vector3 size Vector2 origin Vector2 rotation f32 tint Color] "DrawBillboardPro")
(declare-c upload-mesh [mesh (Ptr Mesh) dynamic bool] "UploadMesh")
-(declare-c update-mesh-buffer [mesh Mesh index i32 data (Ptr u8) data-size i32 offset i32] "UpdateMeshBuffer")
+(declare-c update-mesh-buffer [mesh Mesh index i32 data (Ptr const u8) data-size i32 offset i32] "UpdateMeshBuffer")
(declare-c unload-mesh [mesh Mesh] "UnloadMesh")
(declare-c get-mesh-bounding-box [mesh Mesh] BoundingBox "GetMeshBoundingBox")
(declare-c gen-mesh-tangents [mesh (Ptr Mesh)] "GenMeshTangents")
@@ -312,14 +312,14 @@
(declare-c get-ray-collision-mesh [ray Ray mesh Mesh transform Matrix] RayCollision "GetRayCollisionMesh")
(declare-c get-ray-collision-triangle [ray Ray p-1 Vector3 p-2 Vector3 p-3 Vector3] RayCollision "GetRayCollisionTriangle")
(declare-c get-ray-collision-quad [ray Ray p-1 Vector3 p-2 Vector3 p-3 Vector3 p-4 Vector3] RayCollision "GetRayCollisionQuad")
-(declare-c load-wave-from-memory [file-type string file-data (Ptr u8) data-size i32] Wave "LoadWaveFromMemory")
-(declare-c update-sound [sound Sound data (Ptr u8) sample-count i32] "UpdateSound")
+(declare-c load-wave-from-memory [file-type string file-data (Ptr const u8) data-size i32] Wave "LoadWaveFromMemory")
+(declare-c update-sound [sound Sound data (Ptr const u8) sample-count i32] "UpdateSound")
(declare-c export-wave-as-code [wave Wave file-name string] bool "ExportWaveAsCode")
-(declare-c load-music-stream-from-memory [file-type string data (Ptr u8) data-size i32] Music "LoadMusicStreamFromMemory")
+(declare-c load-music-stream-from-memory [file-type string data (Ptr const u8) data-size i32] Music "LoadMusicStreamFromMemory")
(declare-c load-audio-stream [sample-rate u32 sample-size u32 channels u32] AudioStream "LoadAudioStream")
(declare-c audio-stream-valid? [stream AudioStream] bool "IsAudioStreamValid")
(declare-c unload-audio-stream [stream AudioStream] "UnloadAudioStream")
-(declare-c update-audio-stream [stream AudioStream data (Ptr u8) frame-count i32] "UpdateAudioStream")
+(declare-c update-audio-stream [stream AudioStream data (Ptr const u8) frame-count i32] "UpdateAudioStream")
(declare-c audio-stream-processed? [stream AudioStream] bool "IsAudioStreamProcessed")
(declare-c play-audio-stream [stream AudioStream] "PlayAudioStream")
(declare-c pause-audio-stream [stream AudioStream] "PauseAudioStream")
diff --git a/vendor/raylib/raylib.flan b/vendor/raylib/raylib.flan
index cba15d63..702129ba 100644
--- a/vendor/raylib/raylib.flan
+++ b/vendor/raylib/raylib.flan
@@ -582,10 +582,10 @@
;; out-of-bounds read, and raylib answers false for a polygon with no points
;; anyway.
(declare-c collision-point-poly?-raw
- [point Vector2 points (Ptr Vector2) count i32] bool
+ [point Vector2 points (Ptr const Vector2) count i32] bool
"CheckCollisionPointPoly")
-(defn collision-point-poly? [point Vector2 points [Vector2]] bool
+(defn collision-point-poly? [point Vector2 points [const Vector2]] bool
(if (= (length points) 0)
false
(collision-point-poly?-raw point (addr (at points 0)) (length points))))
@@ -801,7 +801,7 @@
;; which integer type a C count parameter is. The Flan wrapper below takes the
;; slice apart, which is where that idiom lives everywhere else in this file.
(declare-c load-image-from-memory-raw
- [file-type string file-data (Ptr u8) data-size i32] Image
+ [file-type string file-data (Ptr const u8) data-size i32] Image
"LoadImageFromMemory")
;; Empty is answered here rather than passed on, exactly as in
@@ -1015,42 +1015,42 @@
;; Each -raw below is a generated declaration whose name moved aside; see the
;; `name` lines at the foot of `bindings`.
-(defn draw-line-strip [points [Vector2] color Color] ()
+(defn draw-line-strip [points [const Vector2] color Color] ()
(when (> (length points) 0)
(draw-line-strip-raw (addr (at points 0)) (length points) color)))
-(defn draw-triangle-fan [points [Vector2] color Color] ()
+(defn draw-triangle-fan [points [const Vector2] color Color] ()
(when (> (length points) 0)
(draw-triangle-fan-raw (addr (at points 0)) (length points) color)))
-(defn draw-triangle-strip [points [Vector2] color Color] ()
+(defn draw-triangle-strip [points [const Vector2] color Color] ()
(when (> (length points) 0)
(draw-triangle-strip-raw (addr (at points 0)) (length points) color)))
-(defn draw-triangle-strip-3d [points [Vector3] color Color] ()
+(defn draw-triangle-strip-3d [points [const Vector3] color Color] ()
(when (> (length points) 0)
(draw-triangle-strip-3d-raw (addr (at points 0)) (length points) color)))
;; The five spline drawers. raylib reads the same point array five different
;; ways; the only difference between these wrappers is which one it calls.
-(defn draw-spline-linear [points [Vector2] thick f32 color Color] ()
+(defn draw-spline-linear [points [const Vector2] thick f32 color Color] ()
(when (> (length points) 0)
(draw-spline-linear-raw (addr (at points 0)) (length points) thick color)))
-(defn draw-spline-basis [points [Vector2] thick f32 color Color] ()
+(defn draw-spline-basis [points [const Vector2] thick f32 color Color] ()
(when (> (length points) 0)
(draw-spline-basis-raw (addr (at points 0)) (length points) thick color)))
-(defn draw-spline-catmull-rom [points [Vector2] thick f32 color Color] ()
+(defn draw-spline-catmull-rom [points [const Vector2] thick f32 color Color] ()
(when (> (length points) 0)
(draw-spline-catmull-rom-raw (addr (at points 0)) (length points) thick color)))
-(defn draw-spline-bezier-quadratic [points [Vector2] thick f32 color Color] ()
+(defn draw-spline-bezier-quadratic [points [const Vector2] thick f32 color Color] ()
(when (> (length points) 0)
(draw-spline-bezier-quadratic-raw
(addr (at points 0)) (length points) thick color)))
-(defn draw-spline-bezier-cubic [points [Vector2] thick f32 color Color] ()
+(defn draw-spline-bezier-cubic [points [const Vector2] thick f32 color Color] ()
(when (> (length points) 0)
(draw-spline-bezier-cubic-raw
(addr (at points 0)) (length points) thick color)))
@@ -1595,7 +1595,7 @@
;; half no longer carries the string-faced version at all — a binding that is
;; wrong for the only direction it reads in is worse than no binding.
(declare-c get-codepoint-previous-raw
- [text (Ptr u8) codepoint-size (Ptr i32)] i32
+ [text (Ptr const u8) codepoint-size (Ptr i32)] i32
"GetCodepointPrevious")
;; The face a caller wants: the bytes and an offset into them, rather than an
From 11e1ff10a76a21d89f174ce8a513c29c5480cd7d Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 12:44:15 +0700
Subject: [PATCH 05/13] flan dev starts on a file with no main and links the
agent into every program it builds, C-c C-k loads a file keeping what
compiles, and an expression sent from a package's file resolves in that
package
---
TODO.org | 23 +-
emacs/MANUAL.md | 38 ++-
emacs/flan.el | 68 ++++--
emacs/test-flan.el | 61 +++++
lib/dev.ml | 229 ++++++++++++++----
lib/dune | 7 +-
lib/session.ml | 113 ++++++++-
test/programs/dev-load-errors.flan | 8 +
test/programs/dev-load-generic.flan | 9 +
test/programs/dev-noagent-running.flan | 20 +-
test/programs/dev-noagent.flan | 14 +-
test/programs/dev-nomain.flan | 4 +-
test/test_dev.ml | 319 +++++++++++++------------
test/test_session.ml | 84 +++++++
14 files changed, 721 insertions(+), 276 deletions(-)
create mode 100644 test/programs/dev-load-errors.flan
create mode 100644 test/programs/dev-load-generic.flan
diff --git a/TODO.org b/TODO.org
index eb6d0923..b58d5201 100644
--- a/TODO.org
+++ b/TODO.org
@@ -1693,10 +1693,9 @@ nothing sweeps other sessions' directories.
CLOSED: [2026-09-20]
The zero-argument form takes the daemon's socket where there is one and an
announced path where there is not, bound by a constructor before =main=. =Reach=
-prunes a package nothing calls into, so the constructor reaches only a program
-that polls or waits. Full invisibility — a dev build linking the agent whether or
-not the source says so — needs the package force-linked and is a decision about
-what =--dev= means.
+prunes a package nothing calls into in a release build. =flan dev= links the
+agent's C into every program it builds whether or not the source imports it; a
+release build links it only when the program calls into it.
** NEXT FLAN_AGENT_SOCKET in a shell's environment steals the socket
Decided 2026-09-25: narrow the gate. The daemon also exports its own pid, and the constructor binds the socket only when that pid is the program's parent (or the program itself, in a merged build).
@@ -2091,12 +2090,6 @@ motion states in that mode; every other key, including what =special-mode-map=
binds, stays Evil's. The other special-mode buffers (inspect, watch, doc, disassembly,
diagnostics, lower) have the same exposure and are not changed.
-** NEXT C-x C-e in a package's file resolves names in that package
-Decided 2026-09-25: CIDER's rule — an evaluation sent from a file resolves names
-as code written in that file would, so =(integrate 1.0)= in =physics/step.flan=
-reaches the package's own functions, =defn-= included. Today it answers
-"unknown function", resolving as the program's main file.
-
** NEXT Evil takes the keys in the other Flan buffers
The inspect, watch, doc, disassembly, diagnostics and lower buffers get the break
buffer's treatment: the keys each binds itself go to Evil's normal and motion
@@ -2174,13 +2167,9 @@ daemon asks for the sink off (=lib/loc.ml:185=) and gets one exception, so a
function with three bad expressions takes three round trips. The sink is
per-phase; making it per-form would need a resync point inside a body.
-** NEXT A session should start before a program compiles
-Decided 2026-09-25: SBCL/nREPL order: an empty host session, then a load-file op. Re-running with no =main= says there is none; a half-loaded file keeps what compiled and lists the errors. =C-c C-k= is load-file and the inspector moves to =C-c M-i=, CIDER's key.
-=flan dev= builds the program first, so a =main= that does not compile gives no
-session. Want SBCL/nREPL order: empty image, then load a file into it. Needs a
-host built with no user program, and a load-file op — the reload machinery
-already builds a file as a module. Open: what =flan-rerun= does with no =main=,
-and a half-loaded file. =C-c C-k= is taken by the inspector.
+** DONE A session should start before a program compiles
+CLOSED: [2026-09-25]
+A file with no =main= starts on a stub =main= that returns and parks; =load-file= (=C-c C-k=, already its key — the inspector stays on =C-c C-i=) keeps what compiles and lists the rest. Rules out =flan dev= with no file at all, and =--two-process= on a file with no =main=.
** NEXT The daemon buffer is navigable but not coloured
Decided 2026-09-25: errors, warnings and notes take compilation-mode's faces, and the program's own output takes a face of its own so it reads apart from the compiler's.
diff --git a/emacs/MANUAL.md b/emacs/MANUAL.md
index c8f211a0..4910a7fa 100644
--- a/emacs/MANUAL.md
+++ b/emacs/MANUAL.md
@@ -90,6 +90,20 @@ stops the program too — but only one this Emacs started. A daemon you launched
in a terminal is not Emacs' to kill, and it will say so rather than do something
surprising.
+### A file with no `main`
+
+A file of functions with no `main` — a scratch file, a library being written —
+starts a session too. Nothing runs, and the session is there to take
+definitions and expressions: `C-x C-e` on `(fib 10)` answers, and `C-c C-k`
+loads more into it. `M-x flan-rerun` says there is no `main` until one has been
+loaded.
+
+A form in such a file that does not compile is left out of the start and printed
+in `*flan*`, and the session starts with the rest.
+
+The program does not have to import the agent. `flan dev` links it into every
+program it builds, and a release build is unaffected.
+
### Which backend the session uses, and what it costs
`flan dev` compiles the session with the hand-written x86-64 backend. That is
@@ -195,6 +209,11 @@ The form before point can also be a declaration — a `defonce` typed at the top
a file — in which case `C-x C-e` installs it rather than refusing it, and says
which names changed instead of printing a value.
+**Names mean what they mean in the file.** An expression sent from a package's
+file resolves as code written in that file would: `(integrate 1.0)` in
+`physics/step.flan` reaches `physics/integrate`, a `defn-` included. The REPL is
+not a file, so there the program's own names apply.
+
### `C-u C-c C-c` — stop there
The same key with a prefix argument **marks a form as a breakpoint**. `C-u C-c
@@ -261,12 +280,18 @@ drawn on the call — it does not hang.
### `C-c C-k` — the whole buffer
-The whole buffer, sent as **one** module rather than as a form at a time. That
-matters: a `defonce` and the function that uses it have to arrive together, or the
-function refers to storage that does not exist yet.
+The whole buffer is loaded into the running program, as `C-c C-k` loads a file in
+SLIME and CIDER. It is sent as **one** module rather than as a form at a time.
+That matters: a `defonce` and the function that uses it have to arrive together,
+or the function refers to storage that does not exist yet.
-Use this when you have changed several things at once, or when you have added a
-new global.
+A form that does not compile is left out, and so is any form that uses it; the
+rest are installed. Each form left out is marked in the buffer and listed in
+`*flan-diagnostics*`, and the echo area counts them. When nothing compiles,
+nothing is installed and the first error is reported as `C-c C-c` reports one.
+
+Use this when you have changed several things at once, when you have added a new
+global, or to load a file into a session started on another.
### When it lands
@@ -1155,7 +1180,8 @@ Use `C-c C-g` if you need frames.
| `C-c C-c` | the top-level form at point: a declaration installed, anything else evaluated |
| `C-u C-c C-c` | ...and stop at the form point is inside (`C-u C-u`: on entry) |
| `C-M-x` | the same as `C-c C-c`, on the binding SLIME and CIDER use |
-| `C-c C-k` | the whole buffer, as one module |
+| `C-c C-k` | load the whole buffer, as one module; what does not compile is listed |
+
| `C-x C-e` | the form before point, evaluated — or installed, if it is a declaration |
| `C-u C-x C-e` | ...and stop at it instead of showing its value |
| `C-c C-z` | connect (finds `.flan-dev.sock` upward) |
diff --git a/emacs/flan.el b/emacs/flan.el
index b1ec4960..9fd06092 100644
--- a/emacs/flan.el
+++ b/emacs/flan.el
@@ -1618,15 +1618,17 @@ quitting the program — which is the point of it."
(set-marker flan--diagnostics-memory-start nil)
(setq flan--diagnostics-memory-start nil))))
-(defun flan--show-error (loc msg)
+(defun flan--show-error (loc msg &optional keep)
"Mark MSG at LOC, if LOC names a file some buffer is visiting.
+The buffer's other error marks are taken down first unless KEEP is non-nil.
Returns non-nil when it put an overlay somewhere."
(let ((parts (flan--parse-loc loc)))
(when parts
(let ((buf (flan--buffer-visiting (nth 0 parts))))
(when buf
(with-current-buffer buf
- (flan-clear-errors buf)
+ (unless keep (flan-clear-errors buf))
+
;; A refusal is not a value, and the two must never be drawn over
;; one form at once. Ordinarily the command that ran this
;; evaluation already cleared the last one through the hook; this
@@ -1651,7 +1653,8 @@ Returns non-nil when it put an overlay somewhere."
;; Point goes there too, but only in the buffer being looked at:
;; moving point in a buffer nobody is showing is a surprise the
;; next time it is visited.
- (when (eq buf (current-buffer)) (goto-char beg))
+ (when (and (not keep) (eq buf (current-buffer)))
+ (goto-char beg))
t)))))))
;;; Inline results
@@ -2795,18 +2798,55 @@ declaration for it to live in."
;;;###autoload
(defun flan-eval-buffer ()
- "Recompile every top-level form in this buffer and install them together.
-One module, not one per form: a var and the function that uses it have to
-arrive in the same load or the first refers to storage that does not exist."
+ "Load this buffer into the running program, as `C-c C-k' does in SLIME and CIDER.
+Every top-level form is compiled and installed together, as one module: a var
+and the function that uses it have to arrive in the same load or the first
+refers to storage that does not exist.
+
+A form that does not compile is left out, and so is a form that uses it; the
+rest are installed. Each one left out is marked in the buffer and listed in
+`flan-diagnostics-buffer'. When nothing compiles, nothing is installed and
+the command signals, as `C-c C-c' does."
(interactive)
- (flan--eval (buffer-substring-no-properties (point-min) (point-max))
- (buffer-name))
- ;; `flan--eval' signals on a rejection, so reaching here means every
- ;; declaration in the buffer was just replaced by an unmarked one — and
- ;; therefore that every mark in it is gone. Done here rather than by passing
- ;; bounds, because those are also what gets flashed and pulsing a whole
- ;; buffer is not feedback, it is a flicker.
- (flan-clear-pause))
+ (let* ((reply (flan--request
+ (list :op "load-file" :file (or buffer-file-name "")
+ :code (buffer-substring-no-properties
+ (point-min) (point-max)))))
+ (errors (plist-get reply :errors)))
+ (if (equal (plist-get reply :status) "ok")
+ (progn
+ (flan--report reply (buffer-name))
+ ;; Every declaration that installed was replaced by an unmarked one,
+ ;; so every mark in the buffer is gone. Done here rather than by
+ ;; passing bounds, because those are also what gets flashed and
+ ;; pulsing a whole buffer is not feedback, it is a flicker.
+ (flan-clear-pause)
+ (when errors
+ (flan--report-load-errors errors)
+ (message "flan: %s loaded; %d form%s did not compile, listed in %s"
+ (buffer-name) (length errors)
+ (if (= (length errors) 1) "" "s")
+ flan-diagnostics-buffer)))
+ ;; `flan--report' records, marks and signals the first; the others are
+ ;; recorded and marked beside it before the signal leaves.
+ (condition-case err
+ (flan--report reply (buffer-name))
+ (user-error
+ (flan--report-load-errors (cdr errors) t)
+ (signal (car err) (cdr err)))))
+ reply))
+
+(defun flan--report-load-errors (errors &optional keep)
+ "Record and mark each of ERRORS, a load reply's `:errors' list.
+The marks from earlier in the same load are kept, and so are the marks
+already in the buffer when KEEP is non-nil."
+ (let ((first (not keep)))
+ (dolist (e errors)
+ (let ((loc (plist-get e :loc))
+ (msg (plist-get e :message)))
+ (ignore-errors (flan--record-diagnostic loc msg))
+ (ignore-errors (flan--show-error loc msg (not first)))
+ (setq first nil)))))
;;;###autoload
(defun flan-eval-last-sexp (&optional arg)
diff --git a/emacs/test-flan.el b/emacs/test-flan.el
index 30bb649e..c46f5dcc 100644
--- a/emacs/test-flan.el
+++ b/emacs/test-flan.el
@@ -2302,6 +2302,67 @@ already rely on it — so nothing here is a stand-in for the real thing."
(flan-quit)
(ignore-errors (delete-file socket5)))
+ ;; ── A file with no main ───────────────────────────────────────────────
+ ;;
+ ;; SBCL's order: the session comes up on a file that has nothing to run,
+ ;; and `C-c C-k' loads into it. A load keeps what compiles and marks what
+ ;; does not; a re-run says there is no main.
+ (let ((socket6 (concat socket "-nomain"))
+ (scratch (expand-file-name "nomain.flan" (file-name-directory file)))
+ (value (lambda (code)
+ (plist-get (flan--request
+ (list :op "eval-expr" :code code :file ""))
+ :value))))
+ (with-temp-file scratch
+ (insert "(defn fib [n i64] i64\n (if (< n 2) n (+ (fib (- n 1)) (fib (- n 2)))))\n"))
+ (ignore-errors (delete-file socket6))
+ (flan scratch socket6)
+ (test-flan--check "a daemon starts on a file with no main"
+ (process-live-p flan--connection))
+ (test-flan--check "and an expression reaches the file's functions"
+ (equal (funcall value "(fib 10)") "55"))
+ (with-current-buffer (find-file-noselect scratch)
+ (goto-char (point-max))
+ (insert "\n(defn biggest [xs [$t]] $t\n {:where (ordered? $t)}\n"
+ " (let [m (at xs 0)]\n (dotimes [i (length xs)]\n"
+ " (set m (max m (at xs i))))\n m))\n\n"
+ "(defn twice [n i64] i64 (* 2 n))\n")
+ (flan-eval-buffer)
+ (test-flan--check "C-c C-k loads a generic into it"
+ (equal (funcall value "(let [ns [3 9 2]] (biggest (slice ns 0 3)))")
+ "9"))
+ (test-flan--check "and a plain function"
+ (equal (funcall value "(twice 21)") "42"))
+ (erase-buffer)
+ (insert "(defn good [] i64 (bad))\n\n(defn bad [] i64 \"x\")\n\n"
+ "(defn fine [] i64 42)\n")
+ (let ((said (test-flan--said (flan-eval-buffer))))
+ (test-flan--check "a load with errors installs the rest and counts what it left out"
+ (and said (string-match-p "2 forms did not compile" said))))
+ (test-flan--check "and marks each form it left out"
+ (= 2 (length (flan--error-overlays))))
+ (test-flan--check "what compiled is in the program"
+ (equal (funcall value "(fine)") "42"))
+ (test-flan--check "and what used a form that did not is not"
+ (equal (plist-get (flan--request
+ (list :op "eval-expr" :code "(good)"
+ :file ""))
+ :status)
+ "error"))
+ (erase-buffer)
+ (insert "(defn bad [] i64 \"x\")\n")
+ (test-flan--check "a load where nothing compiles is refused"
+ (condition-case nil (progn (flan-eval-buffer) nil)
+ (user-error t)))
+ (set-buffer-modified-p nil))
+ (test-flan--check "a re-run with no main says there is none"
+ (condition-case err (progn (flan-rerun) nil)
+ (user-error
+ (string-match-p "has no main" (error-message-string err)))))
+ (flan-quit)
+ (ignore-errors (delete-file socket6))
+ (ignore-errors (delete-file scratch)))
+
(if (zerop test-flan--failures)
(message "flan.el: all tests passed")
(message "\n%d failure(s)" test-flan--failures)
diff --git a/lib/dev.ml b/lib/dev.ml
index aa138b5a..ae563a46 100644
--- a/lib/dev.ml
+++ b/lib/dev.ml
@@ -122,27 +122,10 @@ let await ?(ms = 5000) f =
in
go ms
-(* What a program needs so that code from the editor can reach it. Spelled once
- because three replies give it: a delivery, an evaluation and the daemon's
- own warning. Both lines compile as written. *)
-let agent_howto =
- "Import the agent with (import agent \"vendor:agent\") and call \
- (agent/poll) once in each pass of the program's main loop, then start \
- flan dev again."
-
-let no_agent =
- "the program has no agent, so nothing in it can receive code from the \
- editor. " ^ agent_howto
-
-(* Whether anything in this session can hand code to the program. A merged
- build with no agent linked has no agent to call and never binds a socket,
- and a connect to one answers "No such file or directory" about a path the
- reader never chose; that is the case this names. *)
-let agentless t = t.child = None && not (Agent.present ())
-
-let unreachable t e =
- if agentless t then no_agent
- else "cannot reach the program: " ^ Unix.error_message e
+(* Every program [flan dev] builds has the agent linked — see [with_agent] — so
+ a program that cannot be reached is one whose socket went away, not one that
+ never had an agent. *)
+let unreachable _t e = "cannot reach the program: " ^ Unix.error_message e
(* Whether the program has bound the socket it receives modules on.
@@ -183,7 +166,7 @@ let agent_check t =
t.agent_watch <- None;
Printf.eprintf
"flan dev: nothing is listening on %s, so code from the editor cannot \
- reach the program. %s\n%!" t.agent agent_howto
+ reach the program.\n%!" t.agent
end
(* ── Asking the agent ──────────────────────────────────────────────── *)
@@ -826,8 +809,8 @@ let refusal ~parked reply =
[max_socket_path], which [session_dir] refuses before building — and there
the module is still queued through the in-process call. A note saying the
program "has not called (agent/start ...)" named a cause that was not the
- cause, so there is none. A program with no agent linked has nothing to
- queue a module on, and its delivery is refused with [no_agent]. *)
+ cause, so there is none. *)
+
let install_note t ~parked =
if parked then begin
let first = not t.park_noted in
@@ -882,7 +865,7 @@ let stale_field (ss : Session.stale list) =
(if x.Session.running then " :running t" else ""))
ss) ]
-let eval t ~code ~origin ~pause =
+let eval ?forms ?base ?(extra = []) t ~code ~origin ~pause =
let now = liveness t in
let parked_now = now = Parked in
(* A park that is over takes its note with it: the long sentence below is
@@ -905,15 +888,19 @@ let eval t ~code ~origin ~pause =
let refused msg = Session.restore t.session before; error msg in
if now = Gone then error gone
else
- match Session.eval ~origin ?pause ~running:(not parked_now) t.session code with
+ match
+ Session.eval ~origin ?base ?forms ?pause ~running:(not parked_now)
+ t.session code
+ with
| c when not c.Session.installs ->
(* Accepted into the session and nothing to send: a declaration the
program already has, with no body and no new storage. Saying "ok" and
shipping an empty module would report success for a change that cannot
have taken effect. *)
ok
- [ ":names " ^ Wire.strings c.Session.names; ":fns ()";
- ":note " ^ Wire.quote "nothing to install" ]
+ ([ ":names " ^ Wire.strings c.Session.names; ":fns ()";
+ ":note " ^ Wire.quote "nothing to install" ]
+ @ extra)
| c ->
(* Everything from here to the delivery is inside the restore, and by
exception type as well as by arm. The three named below are the ones
@@ -965,14 +952,13 @@ let eval t ~code ~origin ~pause =
| Some (l, c) ->
[ ":pause " ^ Wire.quote (Printf.sprintf "%d:%d" l c) ]
| None -> [])
- @ install_note t ~parked:parked_now)
+ @ install_note t ~parked:parked_now
+ @ extra)
| reply -> refused (refusal ~parked:parked_now reply)
| exception Unix.Unix_error (e, _, _) ->
refused
- (if agentless t then no_agent
- else
- "cannot reach the program on " ^ t.agent ^ ": "
- ^ Unix.error_message e))
+ ("cannot reach the program on " ^ t.agent ^ ": "
+ ^ Unix.error_message e))
| exception Failure m -> refused m)
with e when not !accepted -> Session.restore t.session before; raise e)
(* Nothing to put back: the check itself raised, so [Session.eval] never
@@ -984,6 +970,60 @@ let eval t ~code ~origin ~pause =
Session.restore t.session before;
error ~loc:(Loc.to_string l) msg
+(* The refusals a load answered beside what it installed, one plist each. *)
+let errors_field (ds : Loc.diag list) =
+ match ds with
+ | [] -> []
+ | ds ->
+ [ ":errors "
+ ^ Wire.list
+ (List.map
+ (fun (d : Loc.diag) ->
+ Printf.sprintf "(:loc %s :message %s)"
+ (Wire.quote (Loc.to_string d.Loc.dloc))
+ (Wire.quote d.Loc.dmsg))
+ ds) ]
+
+(* C-c C-k: a whole file into the running session, SBCL's [load]. [eval] with
+ one difference — a form that does not compile is left out and listed
+ rather than refusing the rest, so a file with one broken function still
+ defines the others ([Session.pruned] finds which). The survivors go through
+ [eval] as one module, as the whole buffer always has. When nothing
+ survives the reply is a refusal, with the first error where every other
+ refusal puts it. *)
+let load_file t ~code ~origin =
+ match Reader.read_all ~file:origin code with
+ | exception Loc.Error { Loc.dloc = l; dmsg = msg; _ } ->
+ error ~loc:(Loc.to_string l) msg
+ | forms ->
+ (* The imports of a file on disk are its own, wherever the session's file
+ is. *)
+ let base = if Sys.file_exists origin then Some origin else None in
+ let running = liveness t <> Parked in
+ let check forms =
+ let before = Session.held t.session in
+ Fun.protect
+ ~finally:(fun () -> Session.restore t.session before)
+ (fun () ->
+ ignore (Session.eval ~origin ?base ~forms ~running t.session code))
+ in
+ (match Session.pruned check forms with
+ | exception Loc.Error { Loc.dloc = l; dmsg = msg; _ } ->
+ error ~loc:(Loc.to_string l) msg
+ | exception Loc.Errors ({ Loc.dloc = l; dmsg = msg; _ } :: _ as ds) ->
+ let e = error ~loc:(Loc.to_string l) msg in
+ String.sub e 0 (String.length e - 1)
+ ^ " " ^ String.concat " " (errors_field ds) ^ ")"
+ | (), kept, errs ->
+ if errs <> [] && kept = [] then
+ let d = List.hd errs in
+ let e = error ~loc:(Loc.to_string d.Loc.dloc) d.Loc.dmsg in
+ String.sub e 0 (String.length e - 1)
+ ^ " " ^ String.concat " " (errors_field errs) ^ ")"
+ else
+ eval ~forms:kept ?base ~extra:(errors_field errs) t ~code ~origin
+ ~pause:None)
+
(* Redefining a name installs a body; evaluating an expression has no name to
install into, so the module carries a thunk the agent runs once. The value
comes back through the runtime rather than through this reply, because the
@@ -1023,7 +1063,6 @@ let eval t ~code ~origin ~pause =
let eval_expr t ~code ~origin ~pause =
match liveness t with
| Gone -> error gone
- | (Live | Parked) when agentless t -> error no_agent
| Live | Parked ->
(* The same rollback [eval] takes, for the same reason and a smaller
cargo. A thunk is not a declaration and never joins the session, but the
@@ -3315,6 +3354,17 @@ let abort t =
let rerun t =
match liveness t with
| Gone -> error gone
+ (* A file started with no [main] runs a stub that returns at once; running
+ it again would answer "running main again" about nothing. *)
+ | (Live | Parked) when not (Session.has_main t.session) ->
+ error
+ (Printf.sprintf
+ "%s has no main, so there is nothing to run. A program starts at a \
+ function named main; add one and load the file with C-c C-k, for \
+ example:\n\n\
+ \ (defn main [] i32\n\
+ \ 0)"
+ t.session.Session.file)
| Live | Parked ->
(* Read before the request and not after it. Taking a re-run is what ends
the park — the C stores the new state as it accepts — so by the time
@@ -4008,7 +4058,21 @@ let handle t req =
in
macroexpand t ~code ~origin ~all
| None -> error "macroexpand needs :code")
+ (* A whole file, [:code] being its text as the editor holds it — which need
+ not be what is saved — and [:file] where it lives. Without [:code] the
+ file is read from disk. *)
+ | Some "load-file" ->
+ (match Wire.string_field req "file" with
+ | None -> error "load-file needs :file"
+ | Some origin ->
+ (match Wire.string_field req "code" with
+ | Some code -> load_file t ~code ~origin
+ | None ->
+ (match read_file origin with
+ | code -> load_file t ~code ~origin
+ | exception Sys_error m -> error ("cannot read the file: " ^ m))))
| Some "describe" -> describe t
+
| Some "defs" -> defs t
| Some "break" -> break t
| Some "condition" -> condition_op t
@@ -4539,9 +4603,10 @@ let make_session_dir ~file dir =
dev %s"
dir (Unix.error_message e) (Filename.quote file))
-(* A session over a file with no [main] has nothing to run, and the build
- would find that out at the link — as a missing symbol, or as the merged
- build's rename finding nothing to rename. *)
+(* The two-process daemon's program is a child process, and a child whose
+ [main] returns at once is a dead child rather than a parked one — so the
+ stub [Session.create_dev] gives a file with no [main] is no use to it. The
+ one-process daemon takes such a file. *)
let need_main ~file (session : Session.t) =
if not
(List.exists (fun (f : Tast.fn) -> f.Tast.name = "main")
@@ -4549,12 +4614,49 @@ let need_main ~file (session : Session.t) =
then
failwith
(Printf.sprintf
- "%s has no main, so flan dev has nothing to run. A program starts at \
- a function named main, for example:\n\n\
+ "%s has no main, and flan dev --two-process runs the program as a \
+ separate process, which needs one. Start flan dev without \
+ --two-process, or add a function named main, for example:\n\n\
\ (defn main [] i32\n\
\ 0)"
file)
+(* The agent's C, in every program [flan dev] builds, whether or not the source
+ imports the package: its constructor binds the socket before [main], so a
+ file that never mentions the agent can still be reached from the editor. A
+ program that imports it already has it, and is left alone — two copies
+ would collide at the link. A release build is not built here and is not
+ affected. *)
+let with_agent ~dir csrcs lflags =
+ let csrcs =
+ if List.exists (fun c -> Filename.basename c = "flan_agent.c") csrcs then
+ csrcs
+ else begin
+ let c = Filename.concat dir "flan_agent.c" in
+ write_file c Runtime_src.agent_source;
+ csrcs @ [ c ]
+ end
+ in
+ let lflags =
+ lflags
+ @ List.filter (fun f -> not (List.mem f lflags)) [ "-lpthread"; "-ldl" ]
+ in
+ (csrcs, lflags)
+
+(* What [flan dev] says about the forms of a file with no [main] that did not
+ compile. The session starts without them; C-c C-k loads the file again once
+ they are fixed. *)
+let report_dropped ~file = function
+ | [] -> ()
+ | ds ->
+ Printf.eprintf "%s\n%!" (Loc.report_all ds);
+ Printf.eprintf
+ "flan dev: %s has %d form%s that did not compile; the session starts \
+ without %s\n%!"
+ file (List.length ds)
+ (if List.length ds = 1 then "" else "s")
+ (if List.length ds = 1 then "it" else "them")
+
(* [debug] is off by default, which keeps [flan dev] exactly what it was: a
-O2 host and -O2 modules. It is opt-in rather than always-on because a debug
build is an -O0 build — [llvm.dbg.declare] describes an alloca and mem2reg
@@ -4574,6 +4676,7 @@ let two_process ?(debug = false) ?(x86 = true) ~file ~sock () =
let session, l = Session.create ~debug ~x86 ~file () in
need_main ~file:given session;
make_session_dir ~file:given dir;
+ let csrcs, lflags = with_agent ~dir l.Load.csrcs l.Load.lflags in
let exe = Filename.concat dir "program" in
(* [keep] so the host's own IR survives the build. It is the text [llc] was
actually given, not a second emission of it, which is the difference
@@ -4590,7 +4693,7 @@ let two_process ?(debug = false) ?(x86 = true) ~file ~sock () =
Build.executable
~opts:{ Build.default with Build.dev = true; Build.keep = true;
Build.debug; Build.x86 }
- ~csrcs:l.Load.csrcs ~lflags:l.Load.lflags session.Session.host ~out:exe
+ ~csrcs ~lflags session.Session.host ~out:exe
in
(* Host and modules are chosen together, which is the whole licence: an
[--x86] host gets [--x86] modules because one flag set both, and the
@@ -4642,7 +4745,7 @@ let two_process ?(debug = false) ?(x86 = true) ~file ~sock () =
failwith
("the program did not open its agent socket at " ^ agent
^ ". Under --two-process every edit reaches the program through that \
- socket. " ^ agent_howto)
+ socket.")
end;
let t =
@@ -4723,10 +4826,9 @@ let two_process ?(debug = false) ?(x86 = true) ~file ~sock () =
the process starts rather than because anybody asked — and the startup below
is still the one place that decides, in three lines of C.
- What is genuinely open is the *session*: [Session.create ~file] is the only
- entry there is, so a REPL that starts empty and accumulates as files are
- loaded needs [Session] to have a second constructor. It already accumulates;
- it just cannot start from nothing. And [rerun] runs [main] and nothing else,
+ The session starts from a file with no [main] as well: [Session.create_dev]
+ gives it a stub that returns at once, so the process comes up, parks, and
+ accumulates what the editor loads into it. And [rerun] runs [main] and nothing else,
deliberately — running a *named* function is what [eval-expr] already is,
and the two should not grow into one verb with a mode. *)
@@ -4971,11 +5073,26 @@ static void flan_merged_park(void) {
program_state = PROGRAM_PARKED;
pthread_mutex_unlock(&program_lock);
fflush(NULL);
- fprintf(stderr,
- "flan dev: the program finished with %d; the process is parked and "
- "its globals are as it left them — M-x flan-rerun runs it again\n",
- (int)program_status);
+ /* A file with no main is started on a stub that returns at once, and its
+ * first park is the session coming up rather than a program finishing. */
+ {
+ static int first_park = 1;
+ const char *no_main = getenv("FLAN_DEV_NO_MAIN");
+ if (first_park && no_main != NULL && no_main[0] == '1')
+ fprintf(stderr,
+ "flan dev: the file has no main, so nothing runs until one is "
+ "loaded; the session is up and takes definitions and "
+ "expressions\n");
+ else
+ fprintf(stderr,
+ "flan dev: the program finished with %d; the process is parked "
+ "and its globals are as it left them — M-x flan-rerun runs it "
+ "again\n",
+ (int)program_status);
+ first_park = 0;
+ }
fflush(stderr);
+
pthread_mutex_lock(&program_lock);
for (;;) {
while (!program_asked && !program_poll)
@@ -5472,7 +5589,7 @@ let merged_setup () =
marshalling a [Session.t] through a file, which buys nothing: the source
cannot have changed between the two, because the build that produced
this binary is the one that exec'd it. *)
- let session, _ = Session.create ~debug ~x86 ~file () in
+ let session, _, _ = Session.create_dev ~debug ~x86 ~file () in
(* The program's output has to reach an editor exactly as it did when the
daemon held the other end of a pipe. Same pipe, one process: fd 1 is
replaced before the program starts, and the accept loop drains it —
@@ -5576,9 +5693,10 @@ let start_merged ?(debug = false) ?(x86 = true) ~file ~sock () =
let dir = session_dir ~file ~sock in
let given = file in
let file = try Unix.realpath file with Unix.Unix_error _ -> file in
- let session, l = Session.create ~debug ~x86 ~file () in
- need_main ~file:given session;
+ let session, l, dropped = Session.create_dev ~debug ~x86 ~file () in
+ report_dropped ~file:given dropped;
make_session_dir ~file:given dir;
+ let csrcs, lflags = with_agent ~dir l.Load.csrcs l.Load.lflags in
let exe = Filename.concat dir "program" in
(* The host's IR goes straight to its final home rather than being written
into the build's working directory and moved: the merged link is spelled
@@ -5589,8 +5707,13 @@ let start_merged ?(debug = false) ?(x86 = true) ~file ~sock () =
ignore
(merged_executable
~opts:{ Build.default with Build.dev = true; Build.debug; Build.x86 }
- ~csrcs:l.Load.csrcs ~lflags:l.Load.lflags ~pnames:[]
+ ~csrcs ~lflags ~pnames:[]
session.Session.host ~out:exe ~ll:host_ll);
+ (* Read by the park, so the first one says the session is waiting rather
+ than that a program finished. *)
+ Unix.putenv "FLAN_DEV_NO_MAIN"
+ (if Session.has_main session then "0" else "1");
+
let agent = Filename.concat dir "agent.sock" in
(* Every one of these is read by the exec'd binary and by nothing else. They
are set before the exec rather than by the compiler thread afterwards, so
diff --git a/lib/dune b/lib/dune
index 4bb39b77..c2d5b71a 100644
--- a/lib/dune
+++ b/lib/dune
@@ -39,7 +39,8 @@
%{workspace_root}/runtime/flan_rt.c
%{workspace_root}/runtime/flan_dev.c
%{workspace_root}/runtime/flan_dyn.c
- %{workspace_root}/runtime/flan_dyn.h)
+ %{workspace_root}/runtime/flan_dyn.h
+ %{workspace_root}/vendor/agent/flan_agent.c)
(action
(with-stdout-to
runtime_src.ml
@@ -58,4 +59,8 @@
; compiled against the old one.
(echo "|c}\n\nlet dyn_header = {c|\n")
(cat %{workspace_root}/runtime/flan_dyn.h)
+ ; And the agent's C, which flan dev links into every program it builds
+ ; whether or not the source imports the package. See [Dev.with_agent].
+ (echo "|c}\n\nlet agent_source = {c|\n")
+ (cat %{workspace_root}/vendor/agent/flan_agent.c)
(echo "|c}\n")))))
diff --git a/lib/session.ml b/lib/session.ml
index f62654f3..cc3ca9cd 100644
--- a/lib/session.ml
+++ b/lib/session.ml
@@ -252,8 +252,7 @@ let with_expansion_macros (forms : Form.t list) (load : unit -> 'a) : 'a * Form.
Parse.expansion_macros := [];
(r, Load.macro_union (own_macros forms) defined)
-let create ?(debug = false) ?(x86 = false) ~file () =
- let forms = Reader.read_file file in
+let of_forms ~debug ~x86 ~file forms =
let l, mine = with_expansion_macros forms (fun () -> Load.program ~file forms) in
let p, env = Check.program_with_env l.Load.decls in
({ file; decls = l.Load.decls; program = p; env; host = p; pkgs = l.Load.pkgs;
@@ -264,6 +263,92 @@ let create ?(debug = false) ?(x86 = false) ~file () =
thunks = 0; debug; x86;
built = record_built env p p.Tast.fns SM.empty; live = SM.empty }, l)
+let create ?(debug = false) ?(x86 = false) ~file () =
+ of_forms ~debug ~x86 ~file (Reader.read_file file)
+
+(* ── A file loaded a form at a time, keeping what compiles ─────────── *)
+
+(* The form a diagnostic is about: the last one in [forms] that starts at or
+ before the position it was reported at — the call, for an error inside a
+ macro's expansion. [None] when the position is in no file these forms came
+ from, which is an error nothing here can drop a form to avoid. *)
+let blame (forms : Form.t list) (d : Loc.diag) : Form.t option =
+ let at = Loc.call_site d.Loc.dloc in
+ List.fold_left
+ (fun acc (f : Form.t) ->
+ if String.equal f.Form.loc.Loc.file at.Loc.file
+ && Loc.before f.Form.loc at <= 0
+ then Some f
+ else acc)
+ None forms
+
+(* SBCL's [load] and CIDER's load-file: a file whose third form does not
+ compile still defines the other two. [attempt] is run over [forms]; each
+ refusal drops the form it is about and runs it again over the rest, so a
+ form that only failed because it called one that was dropped is dropped
+ with its own error on the next round. Each round drops at least one form,
+ so this ends. Answers what [attempt] returned, the forms it was given, and
+ every error in the order found. An error no form can be blamed for is
+ raised as it came. *)
+let pruned (attempt : Form.t list -> 'a) (forms : Form.t list) :
+ 'a * Form.t list * Loc.diag list =
+ let rec go forms errs =
+ let drop ds e =
+ let bad = List.map (blame forms) ds in
+ if List.exists Option.is_none bad then raise e
+ else
+ let bad = List.filter_map Fun.id bad in
+ go (List.filter (fun f -> not (List.memq f bad)) forms)
+ (List.rev_append ds errs)
+ in
+ match attempt forms with
+ | r -> (r, forms, List.rev errs)
+ | exception (Loc.Error d as e) -> drop [ d ] e
+ | exception (Loc.Errors ds as e) -> drop ds e
+ in
+ go forms []
+
+(* Where [flan dev] writes the [main] a file without one is given. Not a path:
+ nothing reads it back, and a location here is how the session tells that
+ [main] apart from one somebody wrote. *)
+let stub_file = ""
+
+let stub_main () = Reader.read_all ~file:stub_file "(defn main [] i32 0)"
+
+let declares_main (forms : Form.t list) =
+ List.exists
+ (fun (f : Form.t) ->
+ match f.Form.v with
+ | Form.List
+ ({ Form.v = Form.Sym "defn"; _ } :: { Form.v = Form.Sym "main"; _ } :: _)
+ -> true
+ | _ -> false)
+ forms
+
+(* Whether the [main] this session would run is one somebody wrote. *)
+let has_main t =
+ List.exists
+ (fun (d : Ast.decl) ->
+ Ast.declared_name d = Some "main"
+ && not (String.equal d.Ast.dloc.Loc.file stub_file))
+ t.decls
+
+(* The session [flan dev] starts. A file with a [main] is [create]'s. A file
+ without one is the empty image of SBCL's order: a [main] that returns at
+ once is added so there is a process to park, and the file's forms are
+ loaded into it as [pruned] loads them — what compiles is in the host, and
+ what does not is answered beside the session rather than instead of it. A
+ [main] loaded later replaces the stub like any other redefinition. *)
+let create_dev ?(debug = false) ?(x86 = false) ~file () =
+ let forms = Reader.read_file file in
+ if declares_main forms then
+ let t, l = create ~debug ~x86 ~file () in
+ (t, l, [])
+ else
+ let build forms = of_forms ~debug ~x86 ~file (forms @ stub_main ()) in
+ let (t, l), _, errs = pruned build forms in
+ (t, l, errs)
+
(* What a macro may call, for the same reason [macros] is held: an evaluation
parses one form with no import in sight, and a package macro whose body
calls its own package's functions has to find them. [Load.program] hands
@@ -669,8 +754,15 @@ let restore t h =
newest one and no older activation is left running. *)
let rerun t = t.live <- SM.empty
-let eval ?(origin = "") ?pause ?(running = true) t src : change =
- let forms = Reader.read_all ~file:origin src in
+(* [forms], when given, are [src] already read — [pruned] runs this over a
+ file a form fewer each round and has no text for the subset. [base] is the
+ file an [(import ...)] in them is resolved against, the session's own when
+ absent: a file loaded from another directory names its packages from
+ there. *)
+let eval ?(origin = "") ?base ?forms ?pause ?(running = true) t src : change =
+ let forms =
+ match forms with Some f -> f | None -> Reader.read_all ~file:origin src
+ in
(* What an annotated listing quotes for this form is what was sent, not what
the file on disk said when it was last read. *)
Loc.remember ~file:origin src;
@@ -683,7 +775,8 @@ let eval ?(origin = "") ?pause ?(running = true) t src : change =
let macros = ref t.macros in
let incoming =
let l, mine =
- with_expansion_macros forms (fun () -> Load.program ~file:t.file forms)
+ with_expansion_macros forms (fun () ->
+ Load.program ~file:(Option.value base ~default:t.file) forms)
in
(* An evaluated import *adds* to the session's set, so a macro brought in
by C-c C-k is there for the C-c C-c after it. A union and not an
@@ -2236,6 +2329,16 @@ let eval_expr ?(origin = "") ?(pause = false) t src : change =
and the non-termination refusals raise [Loc.Error] out of this call, which
the daemon already answers as an error rather than a silence. *)
let parsed = Parse.with_imported ~decls:(package_decls t) t.macros (fun () -> Parse.expr form) in
+ (* CIDER's rule: an expression sent from a package's file means what it
+ would mean written in that file, so [(integrate 1.0)] in physics/step.flan
+ reaches [physics/integrate]. The qualification [eval] gives a declaration
+ from the same buffer. A [defn-] is reachable too, because the location
+ [private_ref] compares is the buffer's own path. *)
+ let parsed =
+ match package_of t origin with
+ | None -> parsed
+ | Some p -> Load.rename_expr p.Load.owns p.Load.alias [] parsed
+ in
(* Wrapped before the checker, so the call is checked like any other and a
prelude that stopped offering [pause] would be an ordinary unknown name
rather than a thunk that silently did not stop. The [Do] takes the
diff --git a/test/programs/dev-load-errors.flan b/test/programs/dev-load-errors.flan
new file mode 100644
index 00000000..dc280e6b
--- /dev/null
+++ b/test/programs/dev-load-errors.flan
@@ -0,0 +1,8 @@
+;;;; A file loaded into a session with two forms that do not compile: [bad]
+;;;; returns a string where it says i64, and [good] calls [bad], so it goes
+;;;; when [bad] does. [fine] is the form that has to arrive anyway.
+(defn good [] i64 (bad))
+
+(defn bad [] i64 "x")
+
+(defn fine [] i64 42)
diff --git a/test/programs/dev-load-generic.flan b/test/programs/dev-load-generic.flan
new file mode 100644
index 00000000..53dbc372
--- /dev/null
+++ b/test/programs/dev-load-generic.flan
@@ -0,0 +1,9 @@
+;;;; A file loaded into a session with no main: a generic and a plain function.
+(defn biggest [xs [$t]] $t
+ {:where (ordered? $t)}
+ (let [m (at xs 0)]
+ (dotimes [i (length xs)]
+ (set m (max m (at xs i))))
+ m))
+
+(defn twice [n i64] i64 (* 2 n))
diff --git a/test/programs/dev-noagent-running.flan b/test/programs/dev-noagent-running.flan
index f9768554..b4047422 100644
--- a/test/programs/dev-noagent-running.flan
+++ b/test/programs/dev-noagent-running.flan
@@ -1,19 +1,9 @@
-;;;; A program that has not been told about the agent and is still running.
+;;;; A program that never imports the agent and is still running. flan dev
+;;;; links the agent anyway, so a delivery is queued rather than refused; it
+;;;; installs at a frame boundary the program never reaches, since nothing in
+;;;; it calls (agent/poll).
;;;;
-;;;; dev-noagent.flan is the other half of this pair and stops short of it: its
-;;;; main returns, so a moment later it is parked, and a redefinition sent to a
-;;;; parked program is answered by the parking path. This one keeps running,
-;;;; which is the state nothing had pinned: there is no agent in the process to
-;;;; hand a module to and no socket to fall back on, so the daemon refuses the
-;;;; delivery.
-;;;;
-;;;; That is the honest answer for it: the reply says the program has no agent
-;;;; and how to add one. A program that *links* the agent has its socket bound
-;;;; by the package's constructor before main, and the one way that bind fails
-;;;; — a socket path too long for a unix socket — is refused when flan dev
-;;;; starts.
-;;;;
-;;;; So: no (import agent ...) anywhere, and a loop that outlasts the test.
+;;;; No (import agent ...) anywhere, and a loop that outlasts the test.
(defn step [] i64 7)
(defn main [] i32
diff --git a/test/programs/dev-noagent.flan b/test/programs/dev-noagent.flan
index df9fedc8..1133a41f 100644
--- a/test/programs/dev-noagent.flan
+++ b/test/programs/dev-noagent.flan
@@ -1,13 +1,7 @@
-;;;; A program [flan dev] can host that never calls (agent/start ...), which
-;;;; is the one condition the merged session and the two-process daemon answer
-;;;; differently: [two_process] kills the child and fails, [merged_serve]
-;;;; warns and serves anyway. See test_dev.ml's last block.
-;;;;
-;;;; No (import agent ...) at all, because the point is a program that has not
-;;;; been told about the agent rather than one that forgot a call. It prints
-;;;; and returns: a Flan main that returns under [flan dev] parks instead of
-;;;; ending the process (flan_merged_exit), so the session outlives it and the
-;;;; accept loop keeps answering.
+;;;; A program that never imports the agent. flan dev links the agent's C into
+;;;; every program it builds, so a definition and an expression sent while it
+;;;; is parked both land. It prints and returns: a Flan main that returns under
+;;;; flan dev parks instead of ending the process (flan_merged_exit).
(defn step [] i64 7)
(defn main [] i32
diff --git a/test/programs/dev-nomain.flan b/test/programs/dev-nomain.flan
index 217a0b02..8b823dc6 100644
--- a/test/programs/dev-nomain.flan
+++ b/test/programs/dev-nomain.flan
@@ -1,2 +1,4 @@
-;;;; A file with no main: flan dev has nothing to run, and says so before building.
+;;;; A file with no main. flan dev starts a session on it anyway, with a stub
+;;;; main that returns at once, and the file's functions are in the host.
+;;;; flan dev --two-process refuses it, since its program is a child process.
(defn helper [] i64 1)
diff --git a/test/test_dev.ml b/test/test_dev.ml
index 3d8ff53c..b49bd1e0 100644
--- a/test/test_dev.ml
+++ b/test/test_dev.ml
@@ -4885,55 +4885,20 @@ let () =
(try ignore (Unix.waitpid [ Unix.WNOHANG ] opid) with Unix.Unix_error _ -> ());
List.iter (fun f -> try Sys.remove f with Sys_error _ -> ()) [ osock; oout ];
- (* A program that never calls [agent/start], which is the one condition on
- which the two shapes of [flan dev] deliberately disagree. [two_process]
- kills its child and [failwith]s: the program is a separate process, the
- daemon owns it, and a daemon with nothing to deliver to is useless.
- [merged_serve] prints a warning and serves anyway, because the thing it
- would have to kill is itself — an editor connected to it still deserves
- [describe], [defs] and the program's output, and only a *delivery*
- needs the agent.
+ (* A program whose source never mentions the agent. [flan dev] links the
+ agent's C into every program it builds ([Dev.with_agent]), and the
+ constructor binds the socket before main, so the file is reachable from
+ the editor as it stands: dev-noagent.flan's main prints and returns,
+ and a definition and an expression sent to the park both land.
- That second policy was held up by nothing at all. Nothing in the suite
- reached lib/dev.ml's warning branch, and the shape of the mistake it
- guards against is a small one: copying the daemon's answer back into
- the merged path is the obvious tidy-up, and it would turn every program
- without an agent into a session that dies at startup, silently, because
- no test would have noticed.
-
- So what is asserted is the policy and not the sentence: the session
- answers. The warning text is checked second, as the evidence that this
- is the branch that produced it and not some other path that happened to
- work.
-
- WHEN it answers is asserted too, and that is the newer half. The wait
- for the agent socket used to sit in front of [accept_loop], so this
- [describe] could not arrive until the ten seconds had run out — the
- block's cost, and every real session's first keystroke. The wait is a
- deadline the session passes now ([Dev.agent_check]), so the reply comes
- back immediately and the sentence is said later, by the accept loop,
- once the deadline is behind it. The second half is what still costs ten
- seconds here: a warning about a program that is never going to start an
- agent cannot honestly be said before waiting for one.
-
- [describe] and not a cheaper op on purpose: it is what
- [emacs/flan.el] sends straight after [flan--open] (flan.el:646) and
- what its poll sends after that, so this is the stall a person would
- actually have felt. *)
+ [--llvm] here, on a daemon that was going to stand up anyway: one
+ merged LLVM daemon stays in the suite now that a flagless one is x86,
+ and the host listing proves the opt-in reached the build. *)
let nsock = tmp "noagent.sock" and nlog = tmp "noagent.log" in
(try Sys.remove nsock with Sys_error _ -> ());
- (* Its own stderr, unlike every other daemon here: the warning is the
- evidence and it is written there. *)
let nfd =
Unix.openfile nlog [ Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC ] 0o600
in
- (* [--llvm] here, on a daemon that was going to stand up anyway: the
- opt-in is the other half of the default checked at the top of this file,
- and proving it costs the same [stat] on the same directory. It also
- keeps one merged LLVM daemon in the suite now that a flagless one is an
- x86 one -- this test is about a program with no [(agent/start ...)],
- which is a claim about the daemon and not about a backend, so it is the
- cheapest place for both. *)
let npid =
Unix.create_process flan
[| flan; "dev"; "programs/dev-noagent.flan"; "-s"; nsock; "--llvm" |]
@@ -4955,78 +4920,44 @@ let () =
if Sys.file_exists (nhost "s") then
fail "flan dev --llvm left an x86 listing at %s" (nhost "s");
let nc = connect nsock in
- (* The exception arm is not defensive: a session that adopted the
- daemon's policy would exit here, and the connection would come back
- ECONNRESET rather than with a status. Reported by name because an
- uncaught [Unix_error] out of a test binary says nothing about which
- test. *)
- let nt0 = Unix.gettimeofday () in
- (match Wire.parse (Wire.send nc "(:op \"describe\")"; Wire.recv nc) with
- | r when status r = "ok" -> ()
- | r ->
- fail "a program without (agent/start ...) was not served: describe: %s"
- (status r)
- | exception e ->
- fail
- "a program without (agent/start ...) ended the session instead of \
- drawing a warning: %s" (Printexc.to_string e));
- let ndt = Unix.gettimeofday () -. nt0 in
- (* Two seconds, against a stall that was ten and a reply that is a
- fraction of one. The threshold is loose on purpose: what is being
- held is "the session does not wait for the program's socket before
- answering", and a number close to the real cost would fail on a
- loaded machine for a reason that has nothing to do with the wait. *)
- if ndt > 2. then
- fail
- "the first editor request waited %.1fs on a program without \
- (agent/start ...); the accept loop is gated on the agent again"
- ndt;
- (* Dropped rather than closed with [(:op "close")], and the difference
- is the rest of this row: [close] ends the session, the process
- [_exit]s, and the deadline below would be waited out by nobody. A
- dropped connection leaves the accept loop cycling, which is where
- the sentence is said from. *)
+ let parked () =
+ match Wire.field (request nc "(:op \"describe\")") "parked" with
+ | Some { Form.v = Form.Sym "t"; _ } -> true
+ | _ -> false
+ in
+ if not (await parked) then fail "the agentless program never parked"
+ else begin
+ let said r = Option.value ~default:"" (Wire.string_field r "message") in
+ let r =
+ request nc
+ "(:op \"eval\" :code \"(defn step [] i64 8)\" :file \
+ \"programs/dev-noagent.flan\")"
+ in
+ if status r <> "ok" then
+ fail "a definition for a program that never imports the agent: %s"
+ (said r);
+ let r =
+ request nc
+ "(:op \"eval-expr\" :code \"(step)\" :file \
+ \"programs/dev-noagent.flan\")"
+ in
+ if Wire.string_field r "value" <> Some "8" then
+ fail "an expression for a program that never imports the agent: %s %s"
+ (status r) (said r)
+ end;
+ (try
+ ignore (Wire.send nc "(:op \"close\")");
+ ignore (Wire.recv nc)
+ with _ -> ());
(try Unix.close nc with Unix.Unix_error _ -> ())
end;
- (* And the sentence, which arrives after the deadline rather than before
- the loop. Awaited with the daemon still alive — the accept loop is what
- says it, so killing first would be testing that a dead process does not
- print. Generous against the ten-second deadline for the reason the
- threshold above is loose. *)
- let nlog_says () =
- contains_sub
- (try In_channel.with_open_bin nlog In_channel.input_all
- with Sys_error _ -> "")
- "(import agent \"vendor:agent\")"
- in
- ignore (await ~ms:30000 nlog_says);
(try Unix.kill npid Sys.sigkill with Unix.Unix_error _ -> ());
(try ignore (Unix.waitpid [] npid) with Unix.Unix_error _ -> ());
- if not (nlog_says ()) then
- fail
- "a program with no agent drew no warning from flan dev:\n%s"
- (try In_channel.with_open_bin nlog In_channel.input_all
- with Sys_error _ -> "");
List.iter (fun f -> try Sys.remove f with Sys_error _ -> ())
[ nsock; nlog ];
- (* ── ...and what a delivery to one is told ────────────────────────
-
- The row above is about the daemon's own stderr. This one is about the
- reply an editor gets for a redefinition, and it is here because that
- reply was never pinned and this lane changed which of two it is.
-
- A program that does not link the agent at all has no agent in this
- process to call and no socket to fall back to, so the delivery is
- REFUSED, and the reply says the program has no agent and how to give it
- one — both for a redefinition and for an expression. "Queued" would
- have promised a poll that has nothing to drain, and "connect: No such
- file or directory" names a path the reader never chose.
-
- It needs the program to be running, which is why it is not folded into
- the row above: dev-noagent.flan's main returns, so it parks within the
- first moment and a delivery to it is answered by the parking path
- instead. This fixture loops. *)
+ (* And one still running, which never calls [(agent/poll)]: a delivery is
+ queued rather than refused, because the agent is there to take it. *)
let gsock = tmp "noagent-running.sock" and glog = tmp "noagent-running.log" in
(try Sys.remove gsock with Sys_error _ -> ());
let gfd =
@@ -5049,46 +4980,9 @@ let () =
"(:op \"eval\" :code \"(defn step [] i64 9)\" :file \
\"programs/dev-noagent-running.flan\")"
in
- let msg = Option.value ~default:"" (Wire.string_field r "message") in
- (* Refused, and the reason is the program's rather than the compiler's:
- the module built, and what is missing is an agent to hand it to. The
- fix it names is the import. *)
- let names_the_fix m =
- contains_sub m "has no agent"
- && contains_sub m "(import agent \"vendor:agent\")"
- && contains_sub m "(agent/poll)"
- in
- if status r = "ok" then
- fail
- "a redefinition for a program with no agent in it was answered \
- ok%s — nothing can install it"
- (match Wire.string_field r "note" with
- | Some n -> Printf.sprintf " (note: %S)" n
- | None -> "")
- else if not (names_the_fix msg) then
- fail "a delivery to a running agentless program was refused with: %S"
- msg;
- (* And an expression, which used to be answered with the connect's own
- errno. *)
- let r =
- request gc
- "(:op \"eval-expr\" :code \"(step)\" :file \
- \"programs/dev-noagent-running.flan\")"
- in
- let msg = Option.value ~default:"" (Wire.string_field r "message") in
- if status r = "ok" || not (names_the_fix msg) then
- fail "an expression for a running agentless program was answered %s: %S"
- (status r) msg;
- (* And the session is still there afterwards, which is the rest of the
- claim: a refusal is a reply, not the end. *)
- (match request gc "(:op \"describe\")" with
- | r when status r = "ok" -> ()
- | r ->
- fail "the session did not survive an unreachable delivery: %s"
- (status r)
- | exception e ->
- fail "the session ended on an unreachable delivery: %s"
- (Printexc.to_string e));
+ if status r <> "ok" then
+ fail "a delivery to a running program that never imports the agent: %s"
+ (Option.value ~default:"" (Wire.string_field r "message"));
(try
ignore (Wire.send gc "(:op \"close\")");
ignore (Wire.recv gc)
@@ -5154,8 +5048,11 @@ let () =
refused_at_start "a TMPDIR that does not exist" ~tmpdir:missing
~prog:"programs/dev-lateagent.flan" ~mode
[ missing ^ " does not exist"; "TMPDIR=/tmp flan dev" ];
- refused_at_start "a program with no main" ~tmpdir:here ~prog:nomain
- ~mode [ "has no main"; "(defn main [] i32" ])
+ (* Only the two-process daemon: its program is a child, and a child
+ whose main returns is gone. One process starts on the file. *)
+ if mode <> [||] then
+ refused_at_start "a program with no main" ~tmpdir:here ~prog:nomain
+ ~mode [ "has no main"; "(defn main [] i32"; "without --two-process" ])
[ [||]; [| "--two-process" |] ];
(try Unix.rmdir deep with Unix.Unix_error _ -> ());
@@ -7264,10 +7161,9 @@ let () =
let lc = connect lsock in
let said r = Option.value ~default:"" (Wire.string_field r "message") in
(* The program sleeps for three seconds before [agent/start], so this is
- asked inside the delay. Two seconds is the threshold for the reason
- the agentless row gives: the reply is a fraction of one and the bug
- was ten, so anything in between is a loaded machine rather than a
- regression. *)
+ asked inside the delay. Two seconds is the threshold because the reply
+ is a fraction of one and the bug was ten, so anything in between is a
+ loaded machine rather than a regression. *)
let lt0 = Unix.gettimeofday () in
let r = request lc "(:op \"describe\")" in
let ldt = Unix.gettimeofday () -. lt0 in
@@ -7450,6 +7346,121 @@ let () =
List.iter (fun f -> try Sys.remove f with Sys_error _ -> ())
[ psock; pout ];
+ (* ── A session on a file with no main ─────────────────────────────
+ SBCL's order: the session comes up with nothing to run, and a file is
+ loaded into it. A load that has forms which do not compile installs the
+ rest and lists them; a re-run says there is no main and how to add one. *)
+ let msock = tmp "nomain.sock" and mout = tmp "nomain.out" in
+ (try Sys.remove msock with Sys_error _ -> ());
+ let mfd =
+ Unix.openfile mout [ Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC ] 0o600
+ in
+ let mpid =
+ Unix.create_process flan
+ [| flan; "dev"; "programs/dev-nomain.flan"; "-s"; msock |]
+ Unix.stdin mfd mfd
+ in
+ Unix.close mfd;
+ if not (listening ~pid:mpid msock) then begin
+ fail "a daemon on a file with no main %s (%S)" !listen_why
+ (In_channel.with_open_bin mout In_channel.input_all);
+ (try Unix.kill mpid Sys.sigkill with Unix.Unix_error _ -> ())
+ end
+ else begin
+ let mc = connect msock in
+ let said r = Option.value ~default:"" (Wire.string_field r "message") in
+ let value code =
+ let r =
+ request mc
+ (Printf.sprintf "(:op \"eval-expr\" :code %s :file \"\")"
+ (Wire.quote code))
+ in
+ match Wire.string_field r "value" with
+ | Some v -> v
+ | None -> "refused: " ^ said r
+ in
+ let load file = request mc (Printf.sprintf "(:op \"load-file\" :file %S)" file) in
+ let errors r =
+ match Wire.field r "errors" with
+ | Some { Form.v = Form.List l; _ } ->
+ List.map
+ (fun e -> Option.value ~default:"" (Wire.string_field e "message"))
+ l
+ | _ -> []
+ in
+ (match value "(helper)" with
+ | "1" -> ()
+ | v -> fail "the no-main file's own function: %s" v);
+ let r = load "programs/dev-load-generic.flan" in
+ if status r <> "ok" then fail "loading a generic and a function: %s" (said r)
+ else begin
+ (match value "(let [ns [3 9 2]] (biggest (slice ns 0 3)))" with
+ | "9" -> ()
+ | v -> fail "a loaded generic, called: %s" v);
+ match value "(twice 21)" with
+ | "42" -> ()
+ | v -> fail "a loaded function, called: %s" v
+ end;
+ let r = load "programs/dev-load-errors.flan" in
+ if status r <> "ok" then
+ fail "a load with two bad forms installed nothing: %s" (said r)
+ else begin
+ (match errors r with
+ | [ a; b ] ->
+ if not (contains_sub a "expected i64" && contains_sub b "unknown function bad")
+ then fail "a load listed %S and %S" a b
+ | es -> fail "a load with two bad forms listed %d" (List.length es));
+ (match value "(fine)" with
+ | "42" -> ()
+ | v -> fail "the form that compiled beside two that did not: %s" v);
+ if not (contains_sub (value "(good)") "refused") then
+ fail "a form that called one left out was installed"
+ end;
+ (* Nothing compiles: a refusal, with the error where every refusal
+ puts it and the list beside it. *)
+ let r =
+ request mc
+ "(:op \"load-file\" :file \"programs/dev-load-errors.flan\" :code \
+ \"(defn bad [] i64 \\\"x\\\")\")"
+ in
+ if status r <> "error" || errors r = [] || Wire.string_field r "loc" = None
+ then fail "a load where nothing compiles: %s %s" (status r) (said r);
+ let r = request mc "(:op \"rerun\")" in
+ if status r <> "error"
+ || not (contains_sub (said r) "has no main")
+ || not (contains_sub (said r) "(defn main [] i32")
+ then fail "a re-run with no main: %s %s" (status r) (said r);
+ (* A main loaded into it is the one a re-run runs. *)
+ let r =
+ request mc
+ "(:op \"eval\" :code \"(defn main [] i32 (println \\\"from main\\\") 0)\" \
+ :file \"programs/dev-nomain.flan\")"
+ in
+ if status r <> "ok" then fail "loading a main: %s" (said r)
+ else begin
+ let before = Buffer.length output in
+ let r = request mc "(:op \"rerun\")" in
+ if status r <> "ok" then fail "a re-run after a main was loaded: %s" (said r)
+ else if
+ not
+ (await (fun () ->
+ ignore (request mc "(:op \"describe\")");
+ contains_sub
+ (Buffer.sub output before (Buffer.length output - before))
+ "from main"))
+ then fail "the loaded main did not run"
+ end;
+ (try
+ ignore (Wire.send mc "(:op \"close\")");
+ ignore (Wire.recv mc)
+ with _ -> ());
+ (try Unix.close mc with Unix.Unix_error _ -> ())
+ end;
+ (try Unix.kill mpid Sys.sigkill with Unix.Unix_error _ -> ());
+ (try ignore (Unix.waitpid [] mpid) with Unix.Unix_error _ -> ());
+ List.iter (fun f -> try Sys.remove f with Sys_error _ -> ())
+ [ msock; mout ];
+
(* ── A class redefined under its own instances ──────────────────
CLHS 4.3.6's update protocol, end to end, with a real editor at one
end and the running program's own heap at the other. "A method added
diff --git a/test/test_session.ml b/test/test_session.ml
index f2d3f6a0..4ec393b2 100644
--- a/test/test_session.ml
+++ b/test/test_session.ml
@@ -1619,4 +1619,88 @@ let () =
| _ ->
fail "two slots that strip to one name did not keep their raw spellings"));
+ (* ── A file with no main ───────────────────────────────────────────
+ [create_dev] gives it a [main] that returns, so there is a process to
+ start, and [has_main] tells that stub from one somebody wrote. *)
+ (match Session.create_dev ~file:"programs/dev-nomain.flan" () with
+ | t, _, [] ->
+ if Session.has_main t then fail "the stub main counted as the file's own";
+ if not
+ (List.exists (fun (f : Tast.fn) -> f.Tast.name = "main")
+ t.Session.host.Tast.fns)
+ then fail "a file with no main was given no main to start";
+ (* A [main] loaded later is the file's own. *)
+ (match Session.eval ~origin:"programs/dev-nomain.flan" t
+ "(defn main [] i32 3)" with
+ | _ ->
+ if not (Session.has_main t) then
+ fail "a main loaded into the session did not replace the stub"
+ | exception Loc.Error { Loc.dmsg = m; _ } ->
+ fail "loading a main into a session started without one: %s" m)
+ | _, _, _ :: _ -> fail "dev-nomain.flan had forms that did not compile"
+ | exception Loc.Error { Loc.dmsg = m; _ } ->
+ fail "a session over a file with no main: %s" m);
+ (match Session.create_dev ~file:"programs/dev-parknote.flan" () with
+ | t, _, _ ->
+ if not (Session.has_main t) then fail "a file's own main was not its own"
+ | exception Loc.Error { Loc.dmsg = m; _ } -> fail "dev-parknote.flan: %s" m);
+
+ (* A file with no main whose forms do not all compile starts without them,
+ and names them. [good] goes because it calls [bad]. *)
+ (match Session.create_dev ~file:"programs/dev-load-errors.flan" () with
+ | t, _, errs ->
+ let fns = List.map (fun (f : Tast.fn) -> f.Tast.name) t.Session.host.Tast.fns in
+ if not (List.mem "fine" fns) then fail "the form that compiled was left out";
+ if List.mem "good" fns || List.mem "bad" fns then
+ fail "a form that did not compile is in the host";
+ if List.length errs <> 2 then
+ fail "a start with two bad forms named %d" (List.length errs)
+ | exception Loc.Error { Loc.dmsg = m; _ } ->
+ fail "a no-main file with a bad form refused the session: %s" m);
+
+ (* [pruned] on its own, as the daemon's load-file runs it: each round drops
+ the form the error is in, and one it could not blame is raised. *)
+ (let t, _ = Session.create ~file:"programs/dev-parknote.flan" () in
+ let src =
+ In_channel.with_open_bin "programs/dev-load-errors.flan" In_channel.input_all
+ in
+ let origin = "programs/dev-load-errors.flan" in
+ let forms = Reader.read_all ~file:origin src in
+ let check forms =
+ let h = Session.held t in
+ Fun.protect ~finally:(fun () -> Session.restore t h)
+ (fun () -> ignore (Session.eval ~origin ~forms t src))
+ in
+ match Session.pruned check forms with
+ | (), kept, errs ->
+ if List.length kept <> 1 then fail "load kept %d forms, not 1" (List.length kept);
+ (match errs with
+ | [ a; b ] ->
+ if not (has a.Loc.dmsg "expected i64") then
+ fail "the first error a load found was %S" a.Loc.dmsg;
+ if not (has b.Loc.dmsg "unknown function bad") then
+ fail "the form that used a dropped one went for %S" b.Loc.dmsg
+ | _ -> fail "load found %d errors, not 2" (List.length errs))
+ | exception Loc.Error { Loc.dmsg = m; _ } -> fail "pruned raised: %s" m);
+
+ (* ── An expression from a package's file ─────────────────────────────
+ CIDER's rule: it resolves as the file would, so the package's own names
+ reach it bare, a [defn-] included. From the program's file the same bare
+ name is not the package's. *)
+ (let tq, _ = Session.create ~file:"programs/pkg-private.flan" () in
+ (match
+ Session.eval_expr ~origin:"programs/pkgs/secret/secret.flan" tq
+ "(+ (combine 1 2) (mix 3 4))"
+ with
+ | c ->
+ if not (has c.Session.ir "secret") then
+ fail "an expression from a package's file did not reach the package"
+ | exception Loc.Error { Loc.dmsg = m; _ } ->
+ fail "an expression from a package's file: %s" m);
+ match
+ Session.eval_expr ~origin:"programs/pkg-private.flan" tq "(combine 1 2)"
+ with
+ | _ -> fail "a package's bare name resolved from the program's own file"
+ | exception Loc.Error _ -> ());
+
Test_support.report ~label:"session" ()
From 37e577d5e165f6358b89e9a27846fb30574b7ad8 Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 12:46:07 +0700
Subject: [PATCH 06/13] (Ptr const T) is documented beside [const T], and the
TODO entries for it are closed
---
TODO.org | 10 +---------
web/index.html | 1 +
2 files changed, 2 insertions(+), 9 deletions(-)
diff --git a/TODO.org b/TODO.org
index cce2e0a9..545df224 100644
--- a/TODO.org
+++ b/TODO.org
@@ -975,10 +975,7 @@ deliberate absence.
** DONE A read-only slice type
CLOSED: [2026-09-25]
-=[const T]=; a =[T]= converts at the top of a type or under another const slice, never inside a writable one. =(addr (at v i))= of a read-only element is allowed, since a =(Ptr T)= is the C boundary and has no const form; a store is what is refused.
-
-** TODO The address of a read-only element is taken without complaint
-=(addr (at v i))= over a =[const T]= answers a writable =(Ptr T)=, so =slice-from-ptr= launders one back into a =[T]=; a string's byte refuses the same =addr=. Allowed because raylib's =load-image-from-memory= and =get-codepoint-previous= have no other way to hand a =[const u8]= to C. Decision needed: a const pointer type, or a refusal plus another route to C.
+=[const T]= and =(Ptr const T)=; a =[T]= or =(Ptr T)= converts at the top of a type or under another const one, never inside a writable one. The const is shallow: an element of a =[const [u8]]= and a Vec's buffer are writable. The address of read-only storage, a string's byte included, is a =(Ptr const T)=, and a C =const T *= parameter takes one.
** TODO (slice d 1) over a dyn string is refused where (at d i) works
The typed and dyn spaces disagree about a spelling, which the standing rule
@@ -1089,11 +1086,6 @@ Decided 2026-09-25: the type-limit constants as a form taking a type, Odin's
max(T), valid at any numeric type or a numeric?-bounded variable. For a float,
min-of is the most negative finite value.
-** NEXT (Ptr const T), the pointer beside [const T]
-Decided 2026-09-25: addr through a read-only slice gives a (Ptr const T), which
-nothing writes through; (Ptr T) widens to it and never back; a C parameter
-declared const T* takes one. Closes the addr hole in [const T].
-
* Backends
** DONE The x86 backend tracks LLVM at -O0
diff --git a/web/index.html b/web/index.html
index 67ffbe3f..a232e51b 100644
--- a/web/index.html
+++ b/web/index.html
@@ -526,6 +526,7 @@ notation reads as exactly one data item.
(Pool T)generational slab storage, owning, copies the same way items + slots + its allocator
(Handle T)a reference into a pool that reports a dead referent index and generation packed into an i64
(Ptr T)raw pointer a pointer
+(Ptr const T)a pointer nothing is written through: the address of read-only storage, and what a C const T * takes. A (Ptr T) converts to one, never the reverse a pointer
(Option T)Some / Nonetag byte + T
(Fn [T ...] R)a function value, which may have captured a code address and an environment pointer
(CFn [T ...] R)a function value that cannot capture — the C is what a C function pointer would need, not a way to reach C today a pointer
From f87d596bdcf888a3153827312c5db0df1380178f Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 13:06:36 +0700
Subject: [PATCH 07/13] A file with a broken form still starts a session, a
package's macros expand bare from its file, a delivery a running program
never polls for says so with a fix that compiles, and aborting an expression
stopped in the park abandons it and keeps the session
---
emacs/MANUAL.md | 7 ++-
emacs/flan.el | 17 ++++--
emacs/test-flan.el | 6 ++
lib/dev.ml | 96 ++++++++++++++++++++++++------
lib/session.ml | 53 ++++++++++++-----
test/programs/dev-main-broken.flan | 7 +++
test/test_dev.ml | 49 +++++++++++++++
test/test_session.ml | 28 +++++++++
vendor/agent/flan_agent.c | 10 ++++
9 files changed, 230 insertions(+), 43 deletions(-)
create mode 100644 test/programs/dev-main-broken.flan
diff --git a/emacs/MANUAL.md b/emacs/MANUAL.md
index 9550860f..34130ffa 100644
--- a/emacs/MANUAL.md
+++ b/emacs/MANUAL.md
@@ -285,8 +285,10 @@ SLIME and CIDER. It is sent as **one** module rather than as a form at a time.
That matters: a `defonce` and the function that uses it have to arrive together,
or the function refers to storage that does not exist yet.
-A form that does not compile is left out, and so is any form that uses it; the
-rest are installed. Each form left out is marked in the buffer and listed in
+A form that does not compile is left out, and the rest are installed. A name
+that was already in the program keeps its earlier definition, and the forms that
+use it are compiled against that one; a form that uses a name defined nowhere
+else is left out too. Each form left out is marked in the buffer and listed in
`*flan-diagnostics*`, and the echo area counts them. When nothing compiles,
nothing is installed and the first error is reported as `C-c C-c` reports one.
@@ -1184,7 +1186,6 @@ Use `C-c C-g` if you need frames.
| `C-u C-c C-c` | ...and stop at the form point is inside (`C-u C-u`: on entry) |
| `C-M-x` | the same as `C-c C-c`, on the binding SLIME and CIDER use |
| `C-c C-k` | load the whole buffer, as one module; what does not compile is listed |
-
| `C-x C-e` | the form before point, evaluated — or installed, if it is a declaration |
| `C-u C-x C-e` | ...and stop at it instead of showing its value |
| `C-c C-z` | connect (finds `.flan-dev.sock` upward) |
diff --git a/emacs/flan.el b/emacs/flan.el
index a76f1ce4..bf3b1f50 100644
--- a/emacs/flan.el
+++ b/emacs/flan.el
@@ -537,7 +537,12 @@ with it, and a rejected evaluation is a likely moment to *become* stopped."
(unless (eq was now)
(force-mode-line-update t)
(when now
- (message "flan: the program finished; C-c C-M-x runs it again"))))
+ ;; `:main nil' is a file with no main of its own: nothing ran, and
+ ;; there is nothing to run again until one is loaded.
+ (if (and (plist-member reply :main) (null (plist-get reply :main)))
+ (message "flan: the file has no main; C-x C-e and C-c C-k work \
+on the session, and C-c C-M-x runs main once one is loaded")
+ (message "flan: the program finished; C-c C-M-x runs it again")))))
(let ((was flan--stopped)
(now (and (plist-get reply :stopped)
(or (plist-get reply :condition) "a condition"))))
@@ -1290,7 +1295,8 @@ one process would be writing the same globals at once."
(defun flan-abort ()
"Let the stopped program die where it stopped.
This ends `flan dev' too: the daemon owns the program's lifetime and has
-nothing left to serve once it has gone."
+nothing left to serve once it has gone. An expression that stopped while the
+program was parked is abandoned instead, and the session stays."
(interactive)
(let ((r (flan--request '(:op "abort"))))
(if (equal (plist-get r :status) "ok")
@@ -1690,7 +1696,6 @@ Returns non-nil when it put an overlay somewhere."
(when buf
(with-current-buffer buf
(unless keep (flan-clear-errors buf))
-
;; A refusal is not a value, and the two must never be drawn over
;; one form at once. Ordinarily the command that ran this
;; evaluation already cleared the last one through the hook; this
@@ -2875,8 +2880,10 @@ Every top-level form is compiled and installed together, as one module: a var
and the function that uses it have to arrive in the same load or the first
refers to storage that does not exist.
-A form that does not compile is left out, and so is a form that uses it; the
-rest are installed. Each one left out is marked in the buffer and listed in
+A form that does not compile is left out, and the rest are installed. A name
+already in the program keeps its earlier definition, and forms that use it are
+compiled against that one; a form that uses a name defined nowhere else is
+left out too. Each one left out is marked in the buffer and listed in
`flan-diagnostics-buffer'. When nothing compiles, nothing is installed and
the command signals, as `C-c C-c' does."
(interactive)
diff --git a/emacs/test-flan.el b/emacs/test-flan.el
index 15a4ad81..74853a05 100644
--- a/emacs/test-flan.el
+++ b/emacs/test-flan.el
@@ -2405,6 +2405,12 @@ already rely on it — so nothing here is a stand-in for the real thing."
(flan scratch socket6)
(test-flan--check "a daemon starts on a file with no main"
(process-live-p flan--connection))
+ (let* ((reply (flan--request '(:op "describe")))
+ (said (progn (setq flan--parked nil)
+ (test-flan--said (flan--absorb reply)))))
+ (test-flan--check "a parked session with no main does not say a program finished"
+ (and said (string-match-p "has no main" said)
+ (not (string-match-p "finished" said)))))
(test-flan--check "and an expression reaches the file's functions"
(equal (funcall value "(fib 10)") "55"))
(with-current-buffer (find-file-noselect scratch)
diff --git a/lib/dev.ml b/lib/dev.ml
index c82236d9..efb8e50c 100644
--- a/lib/dev.ml
+++ b/lib/dev.ml
@@ -137,6 +137,14 @@ let await ?(ms = 5000) f =
(* Every program [flan dev] builds has the agent linked — see [with_agent] — so
a program that cannot be reached is one whose socket went away, not one that
never had an agent. *)
+(* What a program does so that code from the editor reaches it while it runs.
+ Every program [flan dev] builds has the agent's C, but only the program can
+ decide where its frames end. Both forms compile as written. *)
+let polls_for_it =
+ "Code from the editor runs where the program polls for it: import the \
+ agent with (import agent \"vendor:agent\") and call (agent/poll) once in \
+ each pass of the main loop"
+
let unreachable _t e = "cannot reach the program: " ^ Unix.error_message e
(* Whether the program has bound the socket it receives modules on.
@@ -734,6 +742,11 @@ let with_break t reply =
let fields =
fields ^ (if liveness t = Parked then " :parked t" else " :parked nil")
in
+ (* Only when there is no [main] of the file's own: a parked session over a
+ file without one finished nothing, and an editor should not say it did. *)
+ let fields =
+ if Session.has_main t.session then fields else fields ^ " :main nil"
+ in
String.sub reply 0 (String.length reply - 1) ^ fields ^ ")"
let error ?loc msg =
@@ -875,6 +888,37 @@ let refusal ~parked reply =
the module is still queued through the in-process call. A note saying the
program "has not called (agent/start ...)" named a cause that was not the
cause, so there is none. *)
+(* A running program takes a queued module at its next [(agent/poll)], and one
+ that never polls never takes it. The agent always accepts, so "ok" alone
+ would report a change that does not land: the ring is watched for a moment
+ and a module still waiting at the end is said to be waiting, with the fix.
+ An agent without the [pending] verb (a program vendoring an older one) is
+ not asked twice. A stopped program polls from its break loop, and a parked
+ one gets its own note. *)
+let unpolled_note t ~parked =
+ if parked || state t <> Running then []
+ else begin
+ let deadline = Unix.gettimeofday () +. 3. in
+ let rec taken () =
+ match int_of_string_opt (String.trim (request t "pending")) with
+ | None | Some 0 -> true
+ | Some _ ->
+ if Unix.gettimeofday () >= deadline then false
+ else begin
+ drain t;
+ ignore (Unix.select [] [] [] 0.005);
+ taken ()
+ end
+ | exception Unix.Unix_error _ -> true
+ in
+ if taken () then []
+ else
+ [ ":note "
+ ^ Wire.quote
+ ("queued, but the running program has not taken it in three \
+ seconds, so it has not reached a frame boundary. "
+ ^ polls_for_it ^ "; it installs at the first poll") ]
+ end
let install_note t ~parked =
if parked then begin
@@ -1018,6 +1062,7 @@ let eval ?forms ?base ?(extra = []) t ~code ~origin ~pause =
[ ":pause " ^ Wire.quote (Printf.sprintf "%d:%d" l c) ]
| None -> [])
@ install_note t ~parked:parked_now
+ @ unpolled_note t ~parked:parked_now
@ extra)
| reply -> refused (refusal ~parked:parked_now reply)
| exception Unix.Unix_error (e, _, _) ->
@@ -1424,8 +1469,8 @@ let eval_expr t ~code ~origin ~pause =
break buffer, and evaluate this again"
else
error
- "the program did not reach a frame boundary; is it calling \
- (agent/poll)?")
+ ("the program did not reach a frame boundary in five seconds. "
+ ^ polls_for_it))
(* A module that was taken is the program's from here on, whatever
the wait then says: a timeout is a frame boundary not reached
yet, not a module refused, so the instances in it stay in the
@@ -2195,8 +2240,8 @@ let run_render_thunk ?(stopped_only = false) ?at_stop t ~tag
it stands now"
else
Error
- "the program did not reach a frame boundary; is it calling \
- (agent/poll)?"
+ ("the program did not reach a frame boundary in five seconds. "
+ ^ polls_for_it)
in
if ms <= 0 then gave_up ()
else begin
@@ -3402,11 +3447,28 @@ let abort t =
parked
"the program has already finished, so there is nothing to abort and \
nothing that would end by aborting it but this session"
- (* The one exception, and it is the same exception the restarts are: a thunk
- stopped in the break loop on the parked thread is something to abort, and
- for a condition with no restart worth taking it is the only thing that
- ends it. What it costs is unchanged and is what the reply has always said
- — the process goes, and the session with it. *)
+ (* A thunk stopped in the break loop on the parked thread. Aborting it is
+ abandoning the expression, not ending the process: the program had
+ already finished, and the break loop offers the thunk's own boundary as a
+ restart, so that is what is taken and the session stays parked. A trap
+ offers nothing that can be taken, and there abort still ends the
+ process. *)
+ | Parked
+ when match restarts t with
+ | Ok (rs, false) -> List.exists (fun (_, f, _) -> f = Boundary) rs
+ | _ -> false ->
+ (match restarts t with
+ | Ok (rs, _) ->
+ let i, _, _ = List.find (fun (_, f, _) -> f = Boundary) rs in
+ (match ask t ("restart-at " ^ string_of_int i) with
+ | reply when accepted reply <> None ->
+ ok
+ [ ":note "
+ ^ Wire.quote
+ "the evaluation is abandoned; the program is still parked, and anything the expression changed before it stopped stays changed" ]
+ | reply -> error (String.trim reply)
+ | exception Unix.Unix_error (e, _, _) -> error (unreachable t e))
+ | Error m -> error m)
| Live | Parked ->
match ask t "abort" with
| reply when String.trim reply = "ok" ->
@@ -4229,7 +4291,6 @@ let handle t req =
| code -> load_file t ~code ~origin
| exception Sys_error m -> error ("cannot read the file: " ^ m))))
| Some "describe" -> describe t
-
| Some "defs" -> defs t
| Some "break" -> break t
| Some "condition" -> condition_op t
@@ -4956,10 +5017,7 @@ let make_session_dir ~file dir =
stub [Session.create_dev] gives a file with no [main] is no use to it. The
one-process daemon takes such a file. *)
let need_main ~file (session : Session.t) =
- if not
- (List.exists (fun (f : Tast.fn) -> f.Tast.name = "main")
- session.Session.host.Tast.fns)
- then
+ if not (Session.has_main session) then
failwith
(Printf.sprintf
"%s has no main, and flan dev --two-process runs the program as a \
@@ -4991,9 +5049,9 @@ let with_agent ~dir csrcs lflags =
in
(csrcs, lflags)
-(* What [flan dev] says about the forms of a file with no [main] that did not
- compile. The session starts without them; C-c C-k loads the file again once
- they are fixed. *)
+(* What [flan dev] says about the forms of its file that did not compile. The
+ session starts without them; C-c C-k loads the file again once they are
+ fixed. *)
let report_dropped ~file = function
| [] -> ()
| ds ->
@@ -5021,8 +5079,9 @@ let two_process ?(debug = false) ?(x86 = true) ~file ~sock () =
let dir = session_dir ~file ~sock in
let given = file in
let file = try Unix.realpath file with Unix.Unix_error _ -> file in
- let session, l = Session.create ~debug ~x86 ~file () in
+ let session, l, dropped = Session.create_dev ~debug ~x86 ~file () in
need_main ~file:given session;
+ report_dropped ~file:given dropped;
make_session_dir ~file:given dir;
let csrcs, lflags = with_agent ~dir l.Load.csrcs l.Load.lflags in
let exe = Filename.concat dir "program" in
@@ -6061,7 +6120,6 @@ let start_merged ?(debug = false) ?(x86 = true) ~file ~sock () =
than that a program finished. *)
Unix.putenv "FLAN_DEV_NO_MAIN"
(if Session.has_main session then "0" else "1");
-
let agent = Filename.concat dir "agent.sock" in
(* Every one of these is read by the exec'd binary and by nothing else. They
are set before the exec rather than by the compiler thread afterwards, so
diff --git a/lib/session.ml b/lib/session.ml
index cc3ca9cd..09f1d965 100644
--- a/lib/session.ml
+++ b/lib/session.ml
@@ -333,21 +333,19 @@ let has_main t =
&& not (String.equal d.Ast.dloc.Loc.file stub_file))
t.decls
-(* The session [flan dev] starts. A file with a [main] is [create]'s. A file
- without one is the empty image of SBCL's order: a [main] that returns at
- once is added so there is a process to park, and the file's forms are
- loaded into it as [pruned] loads them — what compiles is in the host, and
- what does not is answered beside the session rather than instead of it. A
+(* The session [flan dev] starts: the file's forms loaded as [pruned] loads
+ them, so what compiles is in the host and what does not is answered beside
+ the session rather than instead of it. A file with no [main] — or whose
+ [main] is one of the forms left out — is the empty image of SBCL's order: a
+ [main] that returns at once is added so there is a process to park, and a
[main] loaded later replaces the stub like any other redefinition. *)
let create_dev ?(debug = false) ?(x86 = false) ~file () =
- let forms = Reader.read_file file in
- if declares_main forms then
- let t, l = create ~debug ~x86 ~file () in
- (t, l, [])
- else
- let build forms = of_forms ~debug ~x86 ~file (forms @ stub_main ()) in
- let (t, l), _, errs = pruned build forms in
- (t, l, errs)
+ let build forms =
+ of_forms ~debug ~x86 ~file
+ (if declares_main forms then forms else forms @ stub_main ())
+ in
+ let (t, l), _, errs = pruned build (Reader.read_file file) in
+ (t, l, errs)
(* What a macro may call, for the same reason [macros] is held: an evaluation
parses one form with no import in sight, and a package macro whose body
@@ -420,6 +418,29 @@ let package_of t origin =
(* A name the running process exports. Everything else is looked up by name at
install time — see [Emit.redefinition]'s [known]. *)
+(* The macros a form sent from [origin] can call. From a package's file that
+ is the package's own under the bare names the file writes, in front of the
+ rest: the session holds them qualified, as the importer calls them, and a
+ bare call parsed without these is a call to an unknown function that the
+ qualification afterwards turns into a call to the macro's own name. *)
+let macros_for t origin =
+ match package_of t origin with
+ | None -> t.macros
+ | Some p ->
+ let pre = p.Load.alias ^ "/" in
+ let bare =
+ List.filter_map
+ (fun (f : Form.t) ->
+ match f.Form.v with
+ | Form.List (hd :: ({ Form.v = Form.Sym n; _ } as nf) :: rest)
+ when String.starts_with ~prefix:pre n ->
+ let b = String.sub n (String.length pre) (String.length n - String.length pre) in
+ Some { f with Form.v = Form.List (hd :: { nf with Form.v = Form.Sym b } :: rest) }
+ | _ -> None)
+ t.macros
+ in
+ Load.macro_union bare t.macros
+
let known t n =
List.exists (fun (f : Tast.fn) -> String.equal f.Tast.name n) t.host.Tast.fns
|| List.exists
@@ -766,7 +787,7 @@ let eval ?(origin = "") ?base ?forms ?pause ?(running = true) t src : chan
(* What an annotated listing quotes for this form is what was sent, not what
the file on disk said when it was last read. *)
Loc.remember ~file:origin src;
- Parse.with_imported ~decls:(package_decls t) t.macros @@ fun () ->
+ Parse.with_imported ~decls:(package_decls t) (macros_for t origin) @@ fun () ->
(* Through [Load] like any other source, so an evaluated (import ...) means
what it means in a file. Its expansion is what gets spliced, which is also
why the accumulated list is the post-Load one: re-evaluating a file that
@@ -2328,7 +2349,7 @@ let eval_expr ?(origin = "") ?(pause = false) t src : change =
a cold macro module costs its ~300ms before that clock starts,
and the non-termination refusals raise [Loc.Error] out of this call, which
the daemon already answers as an error rather than a silence. *)
- let parsed = Parse.with_imported ~decls:(package_decls t) t.macros (fun () -> Parse.expr form) in
+ let parsed = Parse.with_imported ~decls:(package_decls t) (macros_for t origin) (fun () -> Parse.expr form) in
(* CIDER's rule: an expression sent from a package's file means what it
would mean written in that file, so [(integrate 1.0)] in physics/step.flan
reaches [physics/integrate]. The qualification [eval] gives a declaration
@@ -2482,7 +2503,7 @@ let macroexpand ?(origin = "") ~(all : bool) t (src : string) : expansion
let before = Expand.quasiquote form in
(* And the session's macros in front of it, as [eval] and [eval_expr] both
put them: [Macro.program] reads [Parse.imported_macros] directly. *)
- Parse.with_imported ~decls:(package_decls t) t.macros @@ fun () ->
+ Parse.with_imported ~decls:(package_decls t) (macros_for t origin) @@ fun () ->
let after, name =
if all then Macro.expand_all before else Macro.expand_step before
in
diff --git a/test/programs/dev-main-broken.flan b/test/programs/dev-main-broken.flan
new file mode 100644
index 00000000..6ef4433e
--- /dev/null
+++ b/test/programs/dev-main-broken.flan
@@ -0,0 +1,7 @@
+;;;; A file with a main and one form that does not compile: flan dev starts
+;;;; with the rest.
+(defn fine [] i64 42)
+
+(defn bad [] i64 "x")
+
+(defn main [] i32 0)
diff --git a/test/test_dev.ml b/test/test_dev.ml
index adf51d38..5d4046b3 100644
--- a/test/test_dev.ml
+++ b/test/test_dev.ml
@@ -5219,8 +5219,28 @@ let () =
"(:op \"eval\" :code \"(defn step [] i64 9)\" :file \
\"programs/dev-noagent-running.flan\")"
in
+ let fix m =
+ contains_sub m "(import agent \"vendor:agent\")"
+ && contains_sub m "(agent/poll)"
+ in
if status r <> "ok" then
fail "a delivery to a running program that never imports the agent: %s"
+ (Option.value ~default:"" (Wire.string_field r "message"))
+ else if not (fix (Option.value ~default:"" (Wire.string_field r "note")))
+ then
+ fail "a delivery the running program never takes did not say so: %s"
+ (Option.value ~default:"(no note)" (Wire.string_field r "note"));
+ (* And an expression, which waits for a frame boundary the program never
+ reaches, and names the same fix. *)
+ let r =
+ request gc
+ "(:op \"eval-expr\" :code \"(step)\" :file \
+ \"programs/dev-noagent-running.flan\")"
+ in
+ if status r <> "error"
+ || not (fix (Option.value ~default:"" (Wire.string_field r "message")))
+ then
+ fail "an expression for a program that never polls: %s %s" (status r)
(Option.value ~default:"" (Wire.string_field r "message"));
(try
ignore (Wire.send gc "(:op \"close\")");
@@ -7669,6 +7689,35 @@ let () =
|| not (contains_sub (said r) "has no main")
|| not (contains_sub (said r) "(defn main [] i32")
then fail "a re-run with no main: %s %s" (status r) (said r);
+ (* The replies say there is no main of the file's own, so an editor
+ does not report a program that finished. *)
+ (match Wire.field (request mc "(:op \"describe\")") "main" with
+ | Some { Form.v = Form.Sym "nil"; _ } -> ()
+ | _ -> fail "a session with no main did not say so on its replies");
+ (* An expression that stops in the park, aborted: the expression is
+ abandoned and the session stays. *)
+ let r =
+ request mc
+ "(:op \"eval-expr\" :code \"(twice 1)\" :pause t :file \"\")"
+ in
+ ignore r;
+ if not
+ (await (fun () ->
+ match Wire.field (request mc "(:op \"describe\")") "stopped" with
+ | Some { Form.v = Form.Sym "t"; _ } -> true
+ | _ -> false))
+ then fail "a paused expression in the park did not stop"
+ else begin
+ match request mc "(:op \"abort\")" with
+ | r when status r <> "ok" -> fail "aborting a parked expression: %s" (said r)
+ | _ ->
+ (match value "(twice 2)" with
+ | "4" -> ()
+ | v -> fail "the session after aborting a parked expression: %s" v
+ | exception e ->
+ fail "aborting a parked expression ended the session: %s"
+ (Printexc.to_string e))
+ end;
(* A main loaded into it is the one a re-run runs. *)
let r =
request mc
diff --git a/test/test_session.ml b/test/test_session.ml
index 4ec393b2..c612c83d 100644
--- a/test/test_session.ml
+++ b/test/test_session.ml
@@ -1658,6 +1658,19 @@ let () =
| exception Loc.Error { Loc.dmsg = m; _ } ->
fail "a no-main file with a bad form refused the session: %s" m);
+ (* A file with a main of its own and a form that does not compile starts
+ the same way, with its own main. *)
+ (match Session.create_dev ~file:"programs/dev-main-broken.flan" () with
+ | t, _, errs ->
+ if not (Session.has_main t) then fail "the file's own main was left out";
+ let fns = List.map (fun (f : Tast.fn) -> f.Tast.name) t.Session.host.Tast.fns in
+ if not (List.mem "fine" fns) || List.mem "bad" fns then
+ fail "a file with a main started with the wrong forms";
+ if List.length errs <> 1 then
+ fail "a start with one bad form named %d" (List.length errs)
+ | exception Loc.Error { Loc.dmsg = m; _ } ->
+ fail "a file with a main and a bad form refused the session: %s" m);
+
(* [pruned] on its own, as the daemon's load-file runs it: each round drops
the form the error is in, and one it could not blame is raised. *)
(let t, _ = Session.create ~file:"programs/dev-parknote.flan" () in
@@ -1697,6 +1710,21 @@ let () =
fail "an expression from a package's file did not reach the package"
| exception Loc.Error { Loc.dmsg = m; _ } ->
fail "an expression from a package's file: %s" m);
+ (* The package's own macro, bare, from its file: an expression and a
+ declaration both expand it as the file would. *)
+ (match
+ Session.eval_expr ~origin:"programs/pkgs/secret/secret.flan" tq "(mixed 1 1)"
+ with
+ | _ -> ()
+ | exception Loc.Error { Loc.dmsg = m; _ } ->
+ fail "a package's macro, bare, from its file: %s" m);
+ (match
+ Session.eval ~origin:"programs/pkgs/secret/secret.flan" tq
+ "(defn via-mixed [] i32 (mixed 1 2))"
+ with
+ | _ -> ()
+ | exception Loc.Error { Loc.dmsg = m; _ } ->
+ fail "a package's macro, bare, in a declaration from its file: %s" m);
match
Session.eval_expr ~origin:"programs/pkg-private.flan" tq "(combine 1 2)"
with
diff --git a/vendor/agent/flan_agent.c b/vendor/agent/flan_agent.c
index 2ca2aadb..65e14c7e 100644
--- a/vendor/agent/flan_agent.c
+++ b/vendor/agent/flan_agent.c
@@ -1195,6 +1195,16 @@ static void handle_line(char *line, sink *o) {
* running too — "running" is an answer, not a refusal — because this is
* the one question an editor asks without knowing the state already, and
* refusing it would leave nothing to poll. */
+ /* How many modules are queued and not yet taken by a poll. The daemon asks
+ * after a delivery to a running program, so that one which never polls is
+ * told so rather than answered "ok" for a change that never lands. */
+ if (strcmp(line, "pending") == 0) {
+ char b[32];
+ unsigned h = atomic_load(&head), t = atomic_load(&tail);
+ snprintf(b, sizeof b, "%u\n", h - t);
+ reply(o, b);
+ return;
+ }
if (strcmp(line, "status") == 0) {
if ((atomic_load(&depth) > 0)) {
reply(o, "stopped ");
From 1e5be63a1ad46e9849d148086d7398b023ce6d89 Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 13:08:29 +0700
Subject: [PATCH 08/13] An array reached through read-only storage slices to a
[const T], a Vec or Map copied out of one stays read-only through lets, and
an if's const and writable branches meet at const in either order
---
docs/BUILT.md | 2 +-
lib/check.ml | 142 ++++++++++++++++++++++++++++++++--------------
lib/types.ml | 8 +++
test/test_flan.ml | 56 +++++++++++++++---
4 files changed, 157 insertions(+), 51 deletions(-)
diff --git a/docs/BUILT.md b/docs/BUILT.md
index 9974edcd..5050d0a2 100644
--- a/docs/BUILT.md
+++ b/docs/BUILT.md
@@ -1043,7 +1043,7 @@ the only two under which a mark and a sweep run at all. `dev_segv` sits beside t
program that faults cannot be compared against an unsanitized run — that build's handler parks in the break loop, and
the two builds are *supposed* to differ, since `flan_dev_crash_enable` checks a weak `__asan_init` and declines to
install the handler when ASan is in the process. So the case asserts ASan's report and the absence of the handler's
-line, built at `-O0` because at `-O2` the write through a pointer to a literal's bytes does not fault at all. That yield had
+line, built at `-O0` because at `-O2` a store through a zeroed `(Ptr u8)` is undefined and need not fault. That yield had
never run in any build anywhere: it was behind a link that did not happen. Twenty-six seconds of the alias's 2m30 warm.
What it still does not reach is a program driven by a real daemon under ASan: `flan dev` builds its host through its own
path and has no `--sanitize` to pass it.
diff --git a/lib/check.ml b/lib/check.ml
index dfd97c60..4be7ddf2 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -556,6 +556,8 @@ type ctx = {
the outer scope is a list and the names on it were not all written for
this body's sake. *)
mutable caught : (string * (binding * int)) list;
+ (* Locals bound from read-only storage, and the view each came through. *)
+ mutable const_locals : (int * Types.t) list;
(* The context this body was lifted out of, so that capture can be
transitive: an [fn] inside an [fn] naming a local of the function both
were written in is captured by the middle one and then by the inner one
@@ -2211,11 +2213,12 @@ let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc))
an array that is. The last slice stepped through decides, because the
const is shallow — an element of a [[const [u8]]] is itself a writable
[[u8]], and what it views is not the outer slice's to protect. *)
-let rec const_reached (e : Tast.expr) =
+let rec const_reached ?(local = fun (_ : int) -> None) (e : Tast.expr) =
match e.Tast.e with
| Tast.Prim (Tast.At, target :: idx) ->
- const_steps (const_reached target) target.Tast.ty (List.length idx)
- | Tast.Field (target, _) -> const_reached target
+ const_steps (const_reached ~local target) target.Tast.ty (List.length idx)
+ | Tast.Field (target, _) -> const_reached ~local target
+ | Tast.Local s -> local s
| Tast.Deref p ->
(match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None)
| _ -> None
@@ -2230,6 +2233,15 @@ and const_steps ro (ty : Types.t) n =
| Types.Array (_, t) -> const_steps ro t (n - 1)
| _ -> ro
+(* A copy of a read-only slice's elements that can be written, spelled so it
+ compiles. Only for elements that own nothing: an element holding a Vec or
+ a Map — directly or inside a struct — would copy only its header, and the
+ copy would share the original's block. *)
+let const_copy (e : Types.t) =
+ match e with
+ | Types.Vec _ | Types.Map _ | Types.Named _ -> None
+ | _ -> Some (Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e))
+
(* A store through a read-only view: a [[const T]] or a (Ptr const T). *)
let refuse_const_place loc (view : Types.t) =
match view with
@@ -2248,30 +2260,19 @@ let refuse_const_place loc (view : Types.t) =
let elem = match view with Types.Slice (_, t) -> t | t -> t in
Loc.failk "check/store-through-const" loc
"this writes through a %s, which can only be read, so the element is a \
- value and not a place. Write into a slice that can be written: \
- (slice (into v (vec-new %s))) copies v's elements into one"
- (Types.to_string view) (Types.to_string elem)
-
-(* The runtime entry points that change a Vec or a Map, which the backends
- hand the container's address. An element of a [[const (Vec T)]], or a field
- reached through one, is storage the view may not write, so growing,
- shrinking or freeing it there is the same store [check_place] refuses —
- made through the header instead of through a [set]. Writing into the
- Vec's own buffer is not refused: the const is shallow, and the buffer is
- not the slice's storage. *)
-let changes_container = function
- | "flan_vec_push" | "flan_vec_reserve" | "flan_vec_free"
- | "flan_map_put" | "flan_map_remove" | "flan_map_reserve" | "flan_map_free" ->
- true
- | _ -> false
+ value and not a place. %s"
+ (Types.to_string view)
+ (match const_copy elem with
+ | Some c ->
+ Printf.sprintf
+ "Write into a slice that can be written: %s copies v's elements \
+ into one" c
+ | None ->
+ Printf.sprintf "Where it has to be written, take it as a [%s] instead"
+ (Types.to_string elem))
(* A runtime call, with the result type spelled at the site. *)
-let rt loc ty sym args =
- (if changes_container sym then
- match args with
- | target :: _ -> Option.iter (refuse_const_place loc) (const_reached target)
- | [] -> ());
- mk loc ty (Tast.Prim (Tast.Rt sym, args))
+let rt loc ty sym args = mk loc ty (Tast.Prim (Tast.Rt sym, args))
(* ── The allocation registry's note ──────────────────────────────────
@@ -3116,14 +3117,19 @@ let const_note ~(want : Types.t) ~(got : Types.t) =
when Types.equal e e' ->
let copy =
match e with
- | Types.Int Types.U8 -> "(bytes (string v))"
- | _ -> Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e)
+ | Types.Int Types.U8 -> Some "(bytes (string v))"
+ | _ -> const_copy e
in
Printf.sprintf
" — a %s can only be read, and never becomes a %s that can be written \
- through. %s copies v into a %s of its own; where nothing writes \
- through it, the %s can be declared %s instead"
- (Types.to_string got) (Types.to_string want) copy (Types.to_string want)
+ through. %sWhere nothing writes through it, the %s can be declared %s \
+ instead"
+ (Types.to_string got) (Types.to_string want)
+ (match copy with
+ | Some c ->
+ Printf.sprintf "%s copies v into a %s of its own. " c
+ (Types.to_string want)
+ | None -> "")
(Types.to_string want) (Types.to_string got)
| Types.Ptr (Types.Mut, e), Types.Ptr (Types.Const, e')
when Types.equal e e' ->
@@ -3271,7 +3277,7 @@ let hash_ty = Types.Int Types.U64
would share a slot counter. *)
let invented_ctx env ret =
{ env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
- defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
+ defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; const_locals = []; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
in_defer = false; defer_ok = false; defer_block = "a nested form";
owner = "" }
@@ -5019,6 +5025,13 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
| _ -> ());
(* Locals are assignable places; parameters are not. *)
let slot = bind ctx b.Ast.bname v.Tast.ty ~assignable:true in
+ (* A Vec or Map header copied out of read-only storage still
+ shares its block with the original, so a push through the copy
+ is a push through the original. The local remembers where it
+ came from, for [refuse_const_change]. *)
+ Option.iter
+ (fun view -> ctx.const_locals <- (slot, view) :: ctx.const_locals)
+ (const_reached ~local:(const_local ctx) v);
(slot, v))
bs
in
@@ -5478,10 +5491,18 @@ and check_if ctx ?(tail = false) ?want loc c t e =
let t = branch ctx (fun () -> in_tail (fun () -> check ctx ?want t)) in
(* With no expectation the then-branch supplies one for the else-branch,
unless it diverges, in which case the else-branch decides. *)
+ (* A slice or a pointer from the then-branch is not the else-branch's
+ want: the two may differ only in const, and they meet at the
+ read-only one whichever side it is on — [Types.const_join]. *)
+ let free_join =
+ want = None
+ && (match t.Tast.ty with Types.Slice _ | Types.Ptr _ -> true | _ -> false)
+ in
let ewant =
match want with
| Some _ -> want
- | None -> if t.Tast.ty = Types.Never then None else Some t.Tast.ty
+ | None ->
+ if t.Tast.ty = Types.Never || free_join then None else Some t.Tast.ty
in
(* [(and a b c)] is [(let [t a] (if t (let [u b] (if u c u)) t))], so the
*last* operand of an [and] is the then arm and the sentinel that carries
@@ -5514,6 +5535,13 @@ and check_if ctx ?(tail = false) ?want loc c t e =
one type — this operand is %s, and false is a bool"
(Types.to_string t.Tast.ty)
in
+ let t, e =
+ match free_join, Types.const_join t.Tast.ty e.Tast.ty with
+ | true, Some j when e.Tast.ty <> Types.Never ->
+ expect ctx t.Tast.loc ~want:(Some j) t,
+ expect ctx e.Tast.loc ~want:(Some j) e
+ | _ -> t, e
+ in
let ty =
if t.Tast.ty = Types.Never then e.Tast.ty
else if e.Tast.ty = Types.Never then t.Tast.ty
@@ -6540,12 +6568,6 @@ and refuse_string_place loc (ty : Types.t) =
"a string is read-only, so (at s i) is a value and not a place. Copy \
the bytes into a buffer you own and write that"
-(* [store] is false for [addr] alone. A (Ptr T) is the C boundary, where the
- program is already trusted — [slice-from-ptr] and [declare-c] take its word
- — and a [[const u8]] handed to a C function that takes a [const T *] has no
- other way across: [load-image-from-memory] over an [embed] is the case. So
- the address of a read-only element may be taken, and it is a store that is
- refused. *)
(* Whether a checked place is read-only storage: reached through a
[[const T]] or a (Ptr const T), or a byte of a string. Its address is a
(Ptr const T). *)
@@ -6566,6 +6588,28 @@ and place_const (p : Tast.place) =
const_steps (const_reached t) t.Tast.ty (List.length idx) <> None
|| through_string t.Tast.ty (List.length idx)
+and const_local ctx slot = List.assoc_opt slot ctx.const_locals
+
+(* Growing, shrinking or freeing a Vec or a Map that is read-only storage, or
+ a copy of one. The backends hand the runtime the container's address, and
+ the header's block is shared with every copy, so this is the store
+ [check_place] refuses, made through the header instead of through a [set].
+ Writing into the Vec's own buffer is not refused: the const is shallow. *)
+and refuse_const_change ctx loc (target : Tast.expr) =
+ match const_reached ~local:(const_local ctx) target with
+ | None -> ()
+ | Some view ->
+ let t = Types.to_string target.Tast.ty in
+ let holder =
+ match view with Types.Slice (_, e) | Types.Ptr (_, e) -> e | t -> t
+ in
+ Loc.failk "check/store-through-const" loc
+ "this changes a %s reached through a %s, which can only be read. Where \
+ it has to change, take the %s it lives in as a [%s] or a (Ptr %s) \
+ instead"
+ t (Types.to_string view) (Types.to_string holder)
+ (Types.to_string holder) (Types.to_string holder)
+
and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
match p with
| Ast.Pvar name ->
@@ -8059,6 +8103,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
(match args with
| [ target; x ] ->
let target = check ctx target in
+ refuse_const_change ctx loc target;
(* A push into a dyn container is a call and nothing else: no allocation
guard, no restart, no region check. The dyn runtime owns the storage
and answers a failure to grow it on its own terms — the guard and the
@@ -8099,6 +8144,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
(match args with
| [ target; n ] ->
let target = check ctx target in
+ refuse_const_change ctx loc target;
let n = check ctx ~want:index_ty n in
let n64 =
mk loc (Types.Int Types.I64) (Tast.Prim (Tast.Cast (Types.Int Types.I64), [ n ]))
@@ -8142,6 +8188,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
| "free" ->
arity ctx loc name 1 args;
let target = check ctx (List.hd args) in
+ refuse_const_change ctx loc target;
(* A container of owning elements is refused here, and a reader will
assume the opposite — that [free] recurses — so this says why it does
not and what does.
@@ -8311,6 +8358,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
(match args with
| [ target; k; v ] ->
let target = check ctx target in
+ refuse_const_change ctx loc target;
(* A put into a dyn map is a call and nothing else, the way a push into
a dyn vec is: the runtime owns the storage, so there is no guard, no
restart and no region check. An equal key's value is replaced. *)
@@ -8436,6 +8484,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
(match args with
| [ target; k ] ->
let target = check ctx target in
+ refuse_const_change ctx loc target;
let kt, vt = map_kv loc "map-remove" target.Tast.ty in
let k = check ctx ~want:kt k in
(* Deferred exactly as [get] is, and with [None] for the same reason:
@@ -8901,6 +8950,10 @@ and named_call ?(qualified = false) ctx ~want loc name args =
calling it a byte slice would hand out a writable-looking view of
storage the program does not own. *)
let result = match ty with
+ (* An array reached through a [[const T]] or a (Ptr const T) is
+ read-only storage, and so is a view of it. *)
+ | Types.Array (_, t) when const_reached target <> None ->
+ Types.Slice (Types.Const, t)
| Types.Array (_, t) -> Types.Slice (Types.Mut, t)
| Types.Slice (m, t) -> Types.Slice (m, t)
| Types.String -> Types.String
@@ -10036,9 +10089,12 @@ and generic_call ctx ~want loc name vars pats pret args =
| Types.Slice (Types.Mut, _), Types.Slice (Types.Const, e) ->
Printf.sprintf
" — %s takes a slice it may write through, and a %s can \
- only be read. (slice (into v (vec-new %s))) copies v into \
- one that can be written"
- name (Types.to_string a.Tast.ty) (Types.to_string e)
+ only be read%s"
+ name (Types.to_string a.Tast.ty)
+ (match const_copy e with
+ | Some c ->
+ Printf.sprintf ". %s copies v into one that can be written" c
+ | None -> "")
| _ -> "");
a)
pats args
@@ -10395,7 +10451,7 @@ and trial ctx f =
resource failure into a wrong answer. *)
let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
defers; defer_slot; defer_ok; defer_block; outer = _;
- outer_what; caught; envslot; parent = _;
+ outer_what; caught; const_locals; envslot; parent = _;
in_frames; loops; tail; in_defer;
owner = _ } = ctx in
match f () with
@@ -10406,7 +10462,7 @@ and trial ctx f =
ctx.defers <- defers; ctx.defer_slot <- defer_slot;
ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block;
ctx.outer_what <- outer_what; ctx.in_frames <- in_frames;
- ctx.caught <- caught; ctx.envslot <- envslot;
+ ctx.caught <- caught; ctx.const_locals <- const_locals; ctx.envslot <- envslot;
ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer;
Error d
diff --git a/lib/types.ml b/lib/types.ml
index bccd930a..eefb0bbf 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -355,6 +355,14 @@ let rec const_widens ~(from : t) ~(into : t) =
caller handing it a [[T]] loses nothing — and a result may be less so: a
[[T]] returned where a [[const T]] is wanted is [const_widens]'s case. The
two words are the same either way, so [Check.expect] only retypes. *)
+(* The one type two branches of an [if] meet at when they differ only in
+ const: the read-only one, whichever branch it came from. *)
+let const_join a b =
+ if equal a b then Some a
+ else if const_widens ~from:a ~into:b then Some b
+ else if const_widens ~from:b ~into:a then Some a
+ else None
+
let fn_accepts ~(from : t list * t) ~(into : t list * t) =
let ps', r' = from and ps, r = into in
List.length ps = List.length ps'
diff --git a/test/test_flan.ml b/test/test_flan.ml
index adc0a418..31722fd1 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2291,22 +2291,22 @@ let () =
~needle:"expected [[const u8]], found [[u8]]";
rejects_check "push through a const slice of Vecs"
"(defn f [s [const (Vec i32)]] () (push (at s 0) 5))"
- ~needle:"this writes through a [const (Vec i32)]";
+ ~needle:"reached through a [const (Vec i32)]";
rejects_check "put through a const slice of maps"
"(defn f [s [const (Map string i32)]] () (put (at s 0) \"a\" 5))"
- ~needle:"this writes through a [const (Map string i32)]";
+ ~needle:"reached through a [const (Map string i32)]";
rejects_check "map-remove through a const slice of maps"
"(defn f [s [const (Map string i32)]] bool (map-remove (at s 0) \"a\"))"
- ~needle:"this writes through a [const (Map string i32)]";
+ ~needle:"reached through a [const (Map string i32)]";
rejects_check "reserve through a const slice of Vecs"
"(defn f [s [const (Vec i32)]] () (reserve (at s 0) 10))"
- ~needle:"this writes through a [const (Vec i32)]";
+ ~needle:"reached through a [const (Vec i32)]";
rejects_check "free through a const slice of Vecs"
"(defn f [s [const (Vec i32)]] () (free (at s 0)))"
- ~needle:"this writes through a [const (Vec i32)]";
+ ~needle:"reached through a [const (Vec i32)]";
rejects_check "push into a field reached through a const slice"
"(defstruct P [v (Vec i32)]) (defn f [s [const P]] () (push (.v (at s 0)) 1))"
- ~needle:"this writes through a [const P]";
+ ~needle:"reached through a [const P]";
accepts "a Vec's own buffer is not the const slice's storage"
"(defn f [s [const (Vec i32)]] () (set (at (at s 0) 0) 5))";
accepts "a reading function where a writing one is wanted"
@@ -2341,7 +2341,7 @@ let () =
~needle:"this writes through a (Ptr const P)";
rejects_check "a push through a const pointer"
"(defn f [p (Ptr const (Vec i32))] () (push (deref p) 1))"
- ~needle:"behind a (Ptr const (Vec i32))";
+ ~needle:"this changes a (Vec i32) reached through a (Ptr const (Vec i32))";
rejects_check "a const pointer is not a writable one"
"(defn g [p (Ptr u8)] i32 0) (defn f [v [const u8]] i32 (g (addr (at v 0))))"
~needle:"expected (Ptr u8), found (Ptr const u8)";
@@ -2361,6 +2361,48 @@ let () =
"(defn f [p (Ptr const $t)] $t (deref p)) (defn g [q (Ptr i32)] i32 (f q))";
accepts "vec-new reads (Ptr const u8) as a type"
"(defn f [] i32 (let [v (vec-new (Ptr const u8))] (length v)))";
+ (* A Vec header copied out of read-only storage shares its block, so the
+ copy is as read-only as the original, through any number of lets. *)
+ rejects_check "push through a let-bound copy of a const element"
+ "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0)] (push v 1)))"
+ ~needle:"reached through a [const (Vec i32)]";
+ rejects_check "reserve through a copy of a copy"
+ "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0) w v] (reserve w 9)))"
+ ~needle:"reached through a [const (Vec i32)]";
+ rejects_check "put through a let-bound copy of a const element"
+ "(defn f [cs [const (Map string i32)]] () (let [m (at cs 0)] (put m \"a\" 1)))"
+ ~needle:"reached through a [const (Map string i32)]";
+ rejects_check "push into a field of a let-bound copy"
+ "(defstruct P [v (Vec i32)]) \
+ (defn f [cs [const P]] () (let [p (at cs 0)] (push (.v p) 1)))"
+ ~needle:"take the P it lives in as a [P]";
+ rejects_check "no copy of Vec headers is suggested"
+ "(defn f [cs [const (Vec i32)]] () (set (at cs 0) (vec-new i32)))"
+ ~needle:"take it as a [(Vec i32)] instead";
+ (* A fixed array reached through read-only storage slices to a read-only
+ view. *)
+ rejects_check "slice of an array element of a const slice"
+ "(defn f [cs [const [4 u8]]] () (let [s (slice (at cs 0))] (set (at s 0) 9)))"
+ ~needle:"this writes through a [const u8]";
+ rejects_check "slice of an array behind a const pointer"
+ "(defn f [p (Ptr const [4 u8])] () (let [s (slice (deref p))] (set (at s 0) 9)))"
+ ~needle:"this writes through a [const u8]";
+ rejects_check "slice of an array field reached through a const slice"
+ "(defstruct B [buf [4 u8]]) \
+ (defn f [cs [const B]] () (let [s (slice (.buf (at cs 0)))] (set (at s 0) 9)))"
+ ~needle:"this writes through a [const u8]";
+ infers "a local array still slices to a writable slice"
+ "(let [a [1 2]] (slice a))" "[i32]";
+ (* The branches of an if meet at the read-only type, in either order. *)
+ accepts "if: writable then read-only"
+ "(defn f [c bool cs [const u8] ms [u8]] i32 (length (if c ms cs)))";
+ accepts "if: read-only then writable"
+ "(defn f [c bool cs [const u8] ms [u8]] i32 (length (if c cs ms)))";
+ rejects_check "and the join is read-only"
+ "(defn f [c bool cs [const u8] ms [u8]] () (set (at (if c ms cs) 0) 1))"
+ ~needle:"this writes through a [const u8]";
+ accepts "if over pointers joins the same way"
+ "(defn f [c bool a (Ptr const i32) b (Ptr i32)] i32 (deref (if c b a)))";
rejects_check "const is not a name a constant can have"
"(defconst const 4)" ~needle:"const cannot be declared";
(* The const is shallow: an element of a [const [u8]] is a writable [u8]. *)
From 639ff1859cd6368c7f9208c0ee09a08d76b8a7d0 Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 13:28:16 +0700
Subject: [PATCH 09/13] Aborting an expression that trapped in the park
abandons it by a jump back to the poll that called it, and the session stays
---
lib/dev.ml | 12 +++--
runtime/flan_dev.c | 5 ++
runtime/flan_dyn.c | 5 ++
runtime/flan_dyn.h | 2 +
runtime/flan_rt.c | 15 ++++++
test/test_dev.ml | 103 ++++++++++++++++++++++++++++++++------
vendor/agent/flan_agent.c | 102 ++++++++++++++++++++++++++++++++-----
7 files changed, 210 insertions(+), 34 deletions(-)
diff --git a/lib/dev.ml b/lib/dev.ml
index efb8e50c..2346f35d 100644
--- a/lib/dev.ml
+++ b/lib/dev.ml
@@ -3450,12 +3450,12 @@ let abort t =
(* A thunk stopped in the break loop on the parked thread. Aborting it is
abandoning the expression, not ending the process: the program had
already finished, and the break loop offers the thunk's own boundary as a
- restart, so that is what is taken and the session stays parked. A trap
- offers nothing that can be taken, and there abort still ends the
- process. *)
+ restart, so that is what is taken and the session stays parked. At a
+ trap the boundary is left by a jump rather than a transfer (the agent's
+ [eval_escape]), and it is offered the same way. *)
| Parked
when match restarts t with
- | Ok (rs, false) -> List.exists (fun (_, f, _) -> f = Boundary) rs
+ | Ok (rs, _) -> List.exists (fun (_, f, _) -> f = Boundary) rs
| _ -> false ->
(match restarts t with
| Ok (rs, _) ->
@@ -3465,7 +3465,9 @@ let abort t =
ok
[ ":note "
^ Wire.quote
- "the evaluation is abandoned; the program is still parked, and anything the expression changed before it stopped stays changed" ]
+ "the evaluation is abandoned; the program is still parked, \
+ and anything the expression changed before it stopped \
+ stays changed" ]
| reply -> error (String.trim reply)
| exception Unix.Unix_error (e, _, _) -> error (unreachable t e))
| Error m -> error m)
diff --git a/runtime/flan_dev.c b/runtime/flan_dev.c
index b31cf16b..a7d99675 100644
--- a/runtime/flan_dev.c
+++ b/runtime/flan_dev.c
@@ -1064,6 +1064,11 @@ flan_frame *flan_frame_head;
* which is the failure this whole file exists to avoid. */
void flan_dev_frames_reset(void) { flan_frame_head = NULL; }
+/* Where the chain stood, and putting it back there: the agent's way out of a
+ * trapped evaluation jumps past the frames the evaluation pushed. */
+void *flan_dev_frames_mark(void) { return flan_frame_head; }
+void flan_dev_frames_restore(void *head) { flan_frame_head = (flan_frame *)head; }
+
/* [i] counts from the innermost. NULL past the end, which is how a caller
* learns the depth without a second walk. */
void *flan_dev_frame_at(int32_t i) {
diff --git a/runtime/flan_dyn.c b/runtime/flan_dyn.c
index fb76e66e..0743bfc8 100644
--- a/runtime/flan_dyn.c
+++ b/runtime/flan_dyn.c
@@ -1406,6 +1406,11 @@ void flan_dyn_root_globals_end(void) { roots_base = roots_n; }
void flan_dyn_root_reset(void) { roots_n = roots_base; }
+/* The same for one evaluation that trapped: the roots its frames pushed are
+ * dropped, and the ones below it kept. */
+int64_t flan_dyn_root_mark(void) { return roots_n; }
+void flan_dyn_root_restore(int64_t n) { if (n <= roots_n) roots_n = n; }
+
/* ── Constructors ──────────────────────────────────────────────────────*/
flan_dyn flan_dyn_nil(void) { return dyn_make(BOX_NIL, 0); }
diff --git a/runtime/flan_dyn.h b/runtime/flan_dyn.h
index 8e119e57..de2a3ae7 100644
--- a/runtime/flan_dyn.h
+++ b/runtime/flan_dyn.h
@@ -416,6 +416,8 @@ void flan_dyn_track_vecs(void);
* every dyn global for the whole of the park. This resets to the line
* [flan_dyn_root_globals_end] recorded. */
void flan_dyn_root_reset(void);
+int64_t flan_dyn_root_mark(void);
+void flan_dyn_root_restore(int64_t n);
/* Where that line comes from. The emitted [main] brackets its global pushes
* with these: [begin] immediately before the first, [end] immediately after
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index 5ed878ed..7746b3ad 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -278,6 +278,21 @@ void flan_condition_stacks_reset(void) {
c_restart_depth = 0;
}
+/* The same three, marked and put back rather than emptied: an evaluation that
+ * trapped is left by a jump past every frame it pushed, so the chains are
+ * returned to where they stood when it was called (see the agent's poll). */
+void flan_condition_stacks_mark(void **h, void **r, int32_t *d) {
+ *h = handlers;
+ *r = restarts;
+ *d = c_restart_depth;
+}
+
+void flan_condition_stacks_restore(void *h, void *r, int32_t d) {
+ handlers = (flan_handler *)h;
+ restarts = (flan_restart *)r;
+ c_restart_depth = d;
+}
+
/* The conversions are *text*: bytes->f64 parses "12.5", f64->bytes renders it.
* calc-me's tokenizer needs the first, the prelude's printers the second. */
diff --git a/test/test_dev.ml b/test/test_dev.ml
index 55925846..cc7c1d9e 100644
--- a/test/test_dev.ml
+++ b/test/test_dev.ml
@@ -1937,16 +1937,10 @@ let () =
is only as good as SA_NODEFER: %s"
what (status r)
end;
- (* The one case where "just ignore that whole call" cannot hold, and
- it is the same reason every other refusal at a trap has: an
- evaluation that *traps* stops with no transfer channel anywhere in
- the call, so there is nothing for the boundary restart to unwind
- through either. It is listed — it is a live frame, and hiding it
- would make the one break where it does not work the one break that
- never mentions it — and it is listed as untakeable, with
- [:abandon] saying there is no position to offer. Fix the
- expression and evaluate it again; that is the whole of the way
- out. *)
+ (* An evaluation that traps stops with no transfer channel anywhere
+ in the call, so no restart can be unwound to — but the evaluation's
+ own boundary is left by the agent's jump back to the poll that
+ called it, so it is listed as takeable and [:abandon] names it. *)
if trapping <> "" then begin
let r =
ask
@@ -1970,15 +1964,16 @@ let () =
(String.concat ", " names)
| _ -> fail "break at a trap inside an evaluation listed nothing");
(match Wire.field r "unreachable" with
- | Some { Form.v = Form.List [ { Form.v = Form.Int 0L; _ } ]; _ } -> ()
+ | None | Some { Form.v = Form.Sym "nil"; _ }
+ | Some { Form.v = Form.List []; _ } -> ()
| _ ->
- fail "the boundary restart was offered at a trap, where nothing \
- can be taken");
+ fail "the boundary restart was refused at a trap inside an \
+ evaluation");
(match Wire.field r "abandon" with
- | Some { Form.v = Form.Sym "nil"; _ } -> ()
+ | Some { Form.v = Form.Int 0L; _ } -> ()
| _ ->
- fail "a trap inside an evaluation named a position that abandons \
- it");
+ fail "a trap inside an evaluation did not name the position \
+ that abandons it");
(* And the reason those positions are refused, which is the half an
editor puts in front of somebody. [:abandon] being nil cannot
carry it: a break the program took on its own has a nil there
@@ -7761,6 +7756,82 @@ let () =
List.iter (fun f -> try Sys.remove f with Sys_error _ -> ())
[ msock; mout ];
+ (* ── A trap in an expression evaluated in the park ──────────────────
+ A trap has no transfer channel, so no restart can be taken from it —
+ but the evaluation's own boundary can, by the agent's jump back to the
+ poll that called it. Abort takes it, and the session answers after.
+ A null allocator and a stack overflow, on both backends. *)
+ List.iter
+ (fun backend ->
+ let tsock = tmp "trap.sock" and tout = tmp "trap.out" in
+ (try Sys.remove tsock with Sys_error _ -> ());
+ let tfd =
+ Unix.openfile tout [ Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC ] 0o600
+ in
+ let tpid =
+ Unix.create_process flan
+ (Array.append
+ [| flan; "dev"; "programs/dev-nomain.flan"; "-s"; tsock |]
+ backend)
+ Unix.stdin tfd tfd
+ in
+ Unix.close tfd;
+ let shape = if backend = [||] then "x86" else "llvm" in
+ if not (listening ~pid:tpid tsock) then
+ fail "a trap daemon (%s) %s" shape !listen_why
+ else begin
+ let tc = connect tsock in
+ let said r = Option.value ~default:"" (Wire.string_field r "message") in
+ let r =
+ request tc
+ "(:op \"eval\" :code \"(defonce nowhere Allocator)\n\
+ (defn deep [n i64] i64 (+ 1 (deep (+ n 1))))\" \
+ :file \"programs/dev-nomain.flan\")"
+ in
+ if status r <> "ok" then fail "trap definitions (%s): %s" shape (said r);
+ List.iter
+ (fun code ->
+ ignore
+ (request tc
+ (Printf.sprintf "(:op \"eval-expr\" :code %S :file \"\")"
+ code));
+ if not
+ (await (fun () ->
+ match Wire.field (request tc "(:op \"describe\")") "stopped" with
+ | Some { Form.v = Form.Sym "t"; _ } -> true
+ | _ -> false))
+ then fail "%s (%s) did not stop" code shape
+ else
+ match request tc "(:op \"abort\")" with
+ | r when status r <> "ok" ->
+ fail "aborting %s (%s): %s" code shape (said r)
+ | _ ->
+ (match
+ Wire.string_field
+ (request tc
+ "(:op \"eval-expr\" :code \"(helper)\" :file \"\")")
+ "value"
+ with
+ | Some "1" -> ()
+ | v ->
+ fail "the session after aborting %s (%s): %s" code shape
+ (Option.value ~default:"no value" v)
+ | exception e ->
+ fail "aborting %s (%s) ended the session: %s" code shape
+ (Printexc.to_string e)))
+ [ "(free-all nowhere)"; "(deep 0)" ];
+ (try
+ ignore (Wire.send tc "(:op \"close\")");
+ ignore (Wire.recv tc)
+ with _ -> ());
+ (try Unix.close tc with Unix.Unix_error _ -> ())
+ end;
+ (try Unix.kill tpid Sys.sigkill with Unix.Unix_error _ -> ());
+ (try ignore (Unix.waitpid [] tpid) with Unix.Unix_error _ -> ());
+ List.iter (fun f -> try Sys.remove f with Sys_error _ -> ())
+ [ tsock; tout ])
+ [ [||]; [| "--llvm" |] ];
+
(* ── A class redefined under its own instances ──────────────────
CLHS 4.3.6's update protocol, end to end, with a real editor at one
end and the running program's own heap at the other. "A method added
diff --git a/vendor/agent/flan_agent.c b/vendor/agent/flan_agent.c
index 65e14c7e..54c5d5a6 100644
--- a/vendor/agent/flan_agent.c
+++ b/vendor/agent/flan_agent.c
@@ -41,6 +41,7 @@
#include
#include
#include
+#include
#include
#include
#include
@@ -402,6 +403,28 @@ static int32_t frame_floor = -1;
static void *eval_boundary;
static const uint8_t abandon_name[] = "abandon-evaluation";
+/* The way out of the innermost evaluation for a break that has no transfer
+ * channel — a trap: a fault, a failed bounds check, a null allocator. A
+ * restart is a return that unwinds frame by frame, and a trap has nothing to
+ * return through, so abandoning the evaluation from one is a jump straight
+ * back to the poll that called it ([flan_agent_poll]), which puts the
+ * condition, frame and root chains back where they stood. The defers of the
+ * frames jumped over do not run. NULL when no evaluation is in progress;
+ * saved and restored around the call like [eval_boundary]. */
+static sigjmp_buf *eval_escape;
+
+/* What the chains looked like when the evaluation was called, weak for the
+ * reason the frame walk below is: the runtime is linked into every program
+ * that links this, but not every build carries the dev and dyn halves. */
+extern void flan_condition_stacks_mark(void **h, void **r, int32_t *d)
+ __attribute__((weak));
+extern void flan_condition_stacks_restore(void *h, void *r, int32_t d)
+ __attribute__((weak));
+extern void *flan_dev_frames_mark(void) __attribute__((weak));
+extern void flan_dev_frames_restore(void *head) __attribute__((weak));
+extern int64_t flan_dyn_root_mark(void) __attribute__((weak));
+extern void flan_dyn_root_restore(int64_t n) __attribute__((weak));
+
/* The three of them, dropped between two runs of [main]. The counterpart of
* flan_rt.c's [flan_condition_stacks_reset] and flan_dev.c's
* [flan_dev_frames_reset], called from the same one place and for the same
@@ -417,6 +440,7 @@ static const uint8_t abandon_name[] = "abandon-evaluation";
* would be strange to empty two thirds of it. */
void flan_agent_run_reset(void) {
eval_boundary = NULL;
+ eval_escape = NULL;
restart_floor = 0;
frame_floor = -1;
}
@@ -503,6 +527,9 @@ typedef struct {
* client that matched on the name would offer the program's restart as the
* way out of an evaluation. The address is what makes it this one. */
int32_t boundary;
+ /* A trap inside an evaluation: nothing on the list can be taken, except the
+ * boundary, which is left by [eval_escape] rather than by a transfer. */
+ int32_t escapable;
int32_t used;
char names[SNAP_NAMES];
/* Where the stopped thread is, taken at the same moment and for the same
@@ -592,6 +619,12 @@ static snapshot *snap_top(void) {
* to nest, which the caller reports rather than serving a stale one. */
static int32_t snap_gen; /* monotone; 0 is "no snapshot" */
+/* Whether entry [i] can be taken: any reachable one at a break that can
+ * resume, and the evaluation's boundary at a trap inside an evaluation. */
+static int can_take(const snapshot *s, int32_t i) {
+ return (s->resumable && s->reachable[i]) || (s->escapable && i == s->boundary);
+}
+
static int snap_push(int resumable, void *cond) {
int d = atomic_load(&snap_depth);
if (d >= BREAK_MAX) return 0;
@@ -677,6 +710,7 @@ static int snap_push(int resumable, void *cond) {
s->names[s->used++] = 0;
s->n++;
}
+ s->escapable = !s->resumable && eval_escape != NULL && s->boundary >= 0;
/* And the frames, from the same held-still stack. A deep recursion is
* truncated rather than followed: the innermost frames are the ones the
* question is about, and the count says how many were left out. */
@@ -849,7 +883,11 @@ static void break_loop_at(const uint8_t *name, int64_t namelen, void *condition,
* when none of it can be taken — and because the same names come back
* from a `restarts' query, and the terminal and the socket must not be
* describing two different programs. */
- if (!s->resumable)
+ if (s->escapable)
+ fprintf(stderr,
+ " nothing here can be resumed into; abandon the expression, "
+ "or read the frame, then fix and reload\n");
+ else if (!s->resumable)
fprintf(stderr,
" nothing here can be resumed into; read the frame, then fix "
"and reload, or abort\n");
@@ -861,7 +899,9 @@ static void break_loop_at(const uint8_t *name, int64_t namelen, void *condition,
* than hidden, since "why can I not have that one" is a fair question
* and silence is how this went wrong the first time. */
fprintf(stderr, " %2d. restart: %s%s\n", i, s->names + s->off[i],
- !s->resumable ? " (cannot be taken from this trap)"
+ i == s->boundary && can_take(s, i)
+ ? " (stop running the expression; the program carries on)"
+ : !s->resumable ? " (cannot be taken from this trap)"
: i == s->boundary
? " (stop running the expression; the program carries on)"
: s->reachable[i] ? ""
@@ -914,7 +954,23 @@ static void break_loop_at(const uint8_t *name, int64_t namelen, void *condition,
atomic_store(&chosen_ready, 0);
snapshot *s = snap_top();
int ok = s != NULL && s->gen == my_gen && take >= 0 && take < s->n
- && s->resumable && s->reachable[take];
+ && can_take(s, take);
+ if (ok && !s->resumable) {
+ /* The boundary, at a trap: nothing to return through, so the way out
+ * is [eval_escape]. The break is unwound here, as a resume unwinds
+ * it below, and the poll that called the evaluation puts the chains
+ * back. */
+ fprintf(stderr,
+ "flan: the evaluation is abandoned; the program carries on "
+ "from where it was called. Anything it changed before it "
+ "stopped stays changed.\n");
+ fflush(stderr);
+ memcpy(condition_name, outer_name, sizeof condition_name);
+ atomic_store(&aborting, 0);
+ snap_pop();
+ atomic_fetch_sub(&depth, 1);
+ siglongjmp(*eval_escape, 1);
+ }
if (ok) {
/* Which of the two things a take is, decided here because this is the
* only place that holds both the choice and the boundary. The transfer
@@ -1042,7 +1098,27 @@ int32_t flan_agent_poll(void) {
* that were there when the thunk started, and this one is the thunk's.
* Pushed first it would be below its own boundary and refused. */
eval_boundary = flan_restart_push_c(abandon_name, sizeof abandon_name - 1);
- j.call();
+ /* The marks are taken after the boundary is pushed, so a jump back
+ * here leaves it on the chain for the pop below, as a return does.
+ * [sigsetjmp] with the mask saved: a fault's break loop runs inside the
+ * signal handler, and the jump leaves the handler. */
+ sigjmp_buf escape;
+ sigjmp_buf *oescape = eval_escape;
+ void *mh = NULL, *mr = NULL, *mf = NULL;
+ int32_t md = 0;
+ int64_t mroots = 0;
+ if (flan_condition_stacks_mark) flan_condition_stacks_mark(&mh, &mr, &md);
+ if (flan_dev_frames_mark) mf = flan_dev_frames_mark();
+ if (flan_dyn_root_mark) mroots = flan_dyn_root_mark();
+ if (sigsetjmp(escape, 1) == 0) {
+ eval_escape = &escape;
+ j.call();
+ } else {
+ if (flan_condition_stacks_restore) flan_condition_stacks_restore(mh, mr, md);
+ if (flan_dev_frames_restore) flan_dev_frames_restore(mf);
+ if (flan_dyn_root_restore) flan_dyn_root_restore(mroots);
+ }
+ eval_escape = oescape;
/* Popped whichever way the thunk left — returning with a value, or
* unwinding past this frame because someone abandoned it. */
flan_restart_pop_c(eval_boundary);
@@ -1278,7 +1354,7 @@ static void handle_line(char *line, sink *o) {
* reads a takeable restart as takeable, and only misses that this one
* is the way out. */
int k = snprintf(hdr, sizeof hdr, "%d %c ", i,
- !(s->resumable && s->reachable[i]) ? '-'
+ !can_take(s, i) ? '-'
: i == s->boundary ? '*'
: '+');
if (k > 0) emit(o, hdr, (size_t)k);
@@ -1400,13 +1476,13 @@ static void handle_line(char *line, sink *o) {
* with the better sentence: at a trap every restart is unreachable, and
* answering with the thunk-boundary reason would send the reader looking
* for an evaluation that is not there. */
- if (!s->resumable) {
+ if (!s->resumable && !can_take(s, idx)) {
reply(o, "err this break was taken by a trap with no transfer channel, "
- "so no restart can be taken from it; read the frame, then fix "
- "and reload, or abort\n");
+ "so no restart can be taken from it but the evaluation's own; "
+ "read the frame, then fix and reload, or abort\n");
return;
}
- if (!s->reachable[idx]) {
+ if (!can_take(s, idx)) {
/* Refused, with the reason, rather than accepted and dropped. The
* transfer would unwind to the thunk this break is inside and stop
* there, and the program would carry on as if nothing had been
@@ -1452,13 +1528,13 @@ static void handle_line(char *line, sink *o) {
reply(o, " is active\n");
return;
}
- if (!s->resumable) {
+ if (!s->resumable && !can_take(s, at)) {
reply(o, "err this break was taken by a trap with no transfer channel, "
- "so no restart can be taken from it; read the frame, then fix "
- "and reload, or abort\n");
+ "so no restart can be taken from it but the evaluation's own; "
+ "read the frame, then fix and reload, or abort\n");
return;
}
- if (!s->reachable[at]) {
+ if (!can_take(s, at)) {
reply(o, "err restart ");
reply(o, line + 8);
reply(o, " is below the evaluation this break is inside, so a "
From c6ad71dc5bdc5da0ffee9415c2177288b8989f1b Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 13:30:47 +0700
Subject: [PATCH 10/13] A value that owns storage is never copied out of
read-only storage, and two arguments at one type variable meet at const
---
lib/check.ml | 173 ++++++++++++++++++++++-----------
lib/types.ml | 17 ++--
test/programs/const-owned.flan | 39 ++++++++
test/test_acceptance.ml | 6 ++
test/test_flan.ml | 90 ++++++++++++++---
5 files changed, 247 insertions(+), 78 deletions(-)
create mode 100644 test/programs/const-owned.flan
diff --git a/lib/check.ml b/lib/check.ml
index e42e90ab..60c3244a 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -556,8 +556,11 @@ type ctx = {
the outer scope is a list and the names on it were not all written for
this body's sake. *)
mutable caught : (string * (binding * int)) list;
- (* Locals bound from read-only storage, and the view each came through. *)
- mutable const_locals : (int * Types.t) list;
+ (* Whether the form being checked is the target of a place — indexed,
+ sliced, a field read, its address taken — rather than a value. Granted by
+ [check_target] to the one form it checks and withdrawn at the top of
+ [check]. See [refuse_owned_copy]. *)
+ mutable place_ok : bool;
(* The context this body was lifted out of, so that capture can be
transitive: an [fn] inside an [fn] naming a local of the function both
were written in is captured by the middle one and then by the inner one
@@ -1859,7 +1862,16 @@ let rec bind_ty ?(widen = false) ?(ro = true) subst (pat : Types.t)
| Types.Var v, a ->
(match List.assoc_opt v !subst with
| None -> subst := (v, a) :: !subst; true
- | Some b -> Types.equal a b)
+ | Some b when Types.equal a b -> true
+ (* Two arguments that differ only in const bind the variable to the
+ read-only one, whichever came first — the same meeting an [if]'s two
+ branches have. [expect] converts the writable argument afterwards. *)
+ | Some b when ro ->
+ (match Types.const_join a b with
+ | Some j ->
+ subst := (v, j) :: List.remove_assoc v !subst; true
+ | None -> false)
+ | Some _ -> false)
| Types.Slice (m, p), Types.Slice (m', a)
when m = m' || (ro && m = Types.Const) ->
bind_ty ~ro:(m = Types.Const) subst p a
@@ -2198,12 +2210,11 @@ let here loc = mk loc Types.String (Tast.Str (Loc.to_string loc))
an array that is. The last slice stepped through decides, because the
const is shallow — an element of a [[const [u8]]] is itself a writable
[[u8]], and what it views is not the outer slice's to protect. *)
-let rec const_reached ?(local = fun (_ : int) -> None) (e : Tast.expr) =
+let rec const_reached (e : Tast.expr) =
match e.Tast.e with
| Tast.Prim (Tast.At, target :: idx) ->
- const_steps (const_reached ~local target) target.Tast.ty (List.length idx)
- | Tast.Field (target, _) -> const_reached ~local target
- | Tast.Local s -> local s
+ const_steps (const_reached target) target.Tast.ty (List.length idx)
+ | Tast.Field (target, _) -> const_reached target
| Tast.Deref p ->
(match p.Tast.ty with Types.Ptr (Types.Const, _) -> Some p.Tast.ty | _ -> None)
| _ -> None
@@ -2222,13 +2233,12 @@ and const_steps ro (ty : Types.t) n =
compiles. Only for elements that own nothing: an element holding a Vec or
a Map — directly or inside a struct — would copy only its header, and the
copy would share the original's block. *)
-let const_copy (e : Types.t) =
- match e with
- | Types.Vec _ | Types.Map _ | Types.Named _ -> None
- | _ -> Some (Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e))
+let const_copy env (e : Types.t) =
+ if owning env e then None
+ else Some (Printf.sprintf "(slice (into v (vec-new %s)))" (Types.to_string e))
(* A store through a read-only view: a [[const T]] or a (Ptr const T). *)
-let refuse_const_place loc (view : Types.t) =
+let refuse_const_place env loc (view : Types.t) =
match view with
| Types.Ptr (_, ((Types.Vec _ | Types.Map _) as t)) ->
Loc.failk "check/store-through-const" loc
@@ -2247,7 +2257,7 @@ let refuse_const_place loc (view : Types.t) =
"this writes through a %s, which can only be read, so the element is a \
value and not a place. %s"
(Types.to_string view)
- (match const_copy elem with
+ (match const_copy env elem with
| Some c ->
Printf.sprintf
"Write into a slice that can be written: %s copies v's elements \
@@ -3096,14 +3106,14 @@ let numeric_note ~(want : Types.t) ~(got : Types.t) =
copies it names compile today: [string] reads any byte slice and [bytes]
copies a string, and [into] pushes any slice's elements into a Vec that
[slice] then views. *)
-let const_note ~(want : Types.t) ~(got : Types.t) =
+let const_note env ~(want : Types.t) ~(got : Types.t) =
match want, got with
| Types.Slice (Types.Mut, e), Types.Slice (Types.Const, e')
when Types.equal e e' ->
let copy =
match e with
| Types.Int Types.U8 -> Some "(bytes (string v))"
- | _ -> const_copy e
+ | _ -> const_copy env e
in
Printf.sprintf
" — a %s can only be read, and never becomes a %s that can be written \
@@ -3200,7 +3210,7 @@ let expect ctx loc ~want (got : Tast.expr) =
Loc.failk "check/type-mismatch" loc "expected %s, found %s%s%s"
(Types.to_string w) (Types.to_string got.Tast.ty)
(numeric_note ~want:w ~got:got.Tast.ty)
- (const_note ~want:w ~got:got.Tast.ty)
+ (const_note ctx.env ~want:w ~got:got.Tast.ty)
(* Something a [break] may not jump out of, named so the refusal can say which.
See [lentry]: it is a barrier and not a blanket refusal, so a loop written
@@ -3262,7 +3272,7 @@ let hash_ty = Types.Int Types.U64
would share a slot counter. *)
let invented_ctx env ret =
{ env; ret; slots = 0; slot_tys = []; slot_names = []; scope = [];
- defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; const_locals = []; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
+ defers = []; defer_slot = None; outer = []; outer_what = None; caught = []; place_ok = false; envslot = None; parent = None; in_frames = None; loops = []; tail = false;
in_defer = false; defer_ok = false; defer_block = "a nested form";
owner = "" }
@@ -3701,7 +3711,51 @@ let tracked_call loc env name (tr : Shim.track) ret (args : Tast.expr list) =
| [], [] -> call
| pre, post -> mk loc ret (Tast.Do (pre @ [ call ] @ post))
+(* Every expression goes through here, and [check_value] is the one that
+ knows the forms. What this adds is [refuse_owned_copy], asked of whatever
+ came back unless the form was checked as the target of a place. *)
let rec check ctx ?want (e : Ast.expr) : Tast.expr =
+ let place = ctx.place_ok in
+ ctx.place_ok <- false;
+ let r = check_value ctx ?want e in
+ if not place then refuse_owned_copy ctx r;
+ r
+
+(* A form checked as the target of a place: indexed, sliced, a field read,
+ measured, its address taken, or handed to a builtin that works on the
+ container where it stands. *)
+and check_target ctx (e : Ast.expr) =
+ ctx.place_ok <- true;
+ check ctx e
+
+(* Decision 81 (2026-09-25). A value that owns storage — a Vec, a Map, or an
+ array, Option or struct holding one — reached through a [[const T]] or a
+ (Ptr const T) is not copied out as a value. Its header shares its block
+ with the original, so a copy that could be grown, freed or handed on as
+ writable would be the original written through. It is used where it
+ stands instead: indexed, sliced (to a [[const T]]), its fields read when
+ they own nothing, or its address taken as a (Ptr const T). Refusing at the
+ source is the whole rule; there is no tracking of where a copy went. *)
+and refuse_owned_copy ctx (r : Tast.expr) =
+ match const_reached r with
+ | Some view when owning ctx.env r.Tast.ty ->
+ let t = Types.to_string r.Tast.ty in
+ let fix =
+ match r.Tast.ty with
+ | (Types.Vec _ | Types.Map _) when not (region_only ctx.env r.Tast.ty) ->
+ Printf.sprintf "(clone v) copies it into a %s of its own" t
+ (* TODO.org, "(clone slice)": once clone copies any value that owns
+ storage, this should say (clone v) too. *)
+ | _ -> Printf.sprintf "(addr v) gives a (Ptr const %s) to read it through" t
+ in
+ Loc.failk "check/const-owned-copy" r.Tast.loc
+ "this copies a %s out of a %s, which can only be read, and the copy \
+ would share its storage with the original. Use it where it stands — \
+ index it, slice it or read its fields — or %s"
+ t (Types.to_string view) fix
+ | _ -> ()
+
+and check_value ctx ?want (e : Ast.expr) : Tast.expr =
let loc = e.Ast.loc in
(* Read the permission this form was given and withdraw it in the same
breath, so that nothing reached from here inherits it. The two callers
@@ -3928,7 +3982,7 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
than once — nothing in this milestone builds one — still falls to the
ordinary [Ast.Set] arm below, and [indexed] refuses it by name. *)
| Ast.Set (Ast.Pindex (target, [ idx ]), v) ->
- let target = check ctx target in
+ let target = check_target ctx target in
if target.Tast.ty = Types.Dyn then
let i = check ctx ~want:Types.Dyn idx in
let v = check ctx ~want:Types.Dyn v in
@@ -5010,13 +5064,6 @@ and check_let ctx ?(tail = false) ?want ?(defer_ok = false) loc bs body =
| _ -> ());
(* Locals are assignable places; parameters are not. *)
let slot = bind ctx b.Ast.bname v.Tast.ty ~assignable:true in
- (* A Vec or Map header copied out of read-only storage still
- shares its block with the original, so a push through the copy
- is a push through the original. The local remembers where it
- came from, for [refuse_const_change]. *)
- Option.iter
- (fun view -> ctx.const_locals <- (slot, view) :: ctx.const_locals)
- (const_reached ~local:(const_local ctx) v);
(slot, v))
bs
in
@@ -6502,7 +6549,7 @@ and fields_named env n : Tast.structure option =
pointer to one. The auto-deref is inserted here as a real node, so no
backend re-derives it. *)
and struct_target ctx (target : Ast.expr) : Tast.expr * string =
- let t = check ctx target in
+ let t = check_target ctx target in
let has n = fields_named ctx.env n <> None in
match t.Tast.ty with
| Types.Named n when has n -> t, n
@@ -6573,15 +6620,13 @@ and place_const (p : Tast.place) =
const_steps (const_reached t) t.Tast.ty (List.length idx) <> None
|| through_string t.Tast.ty (List.length idx)
-and const_local ctx slot = List.assoc_opt slot ctx.const_locals
-
-(* Growing, shrinking or freeing a Vec or a Map that is read-only storage, or
- a copy of one. The backends hand the runtime the container's address, and
- the header's block is shared with every copy, so this is the store
- [check_place] refuses, made through the header instead of through a [set].
- Writing into the Vec's own buffer is not refused: the const is shallow. *)
-and refuse_const_change ctx loc (target : Tast.expr) =
- match const_reached ~local:(const_local ctx) target with
+(* Growing, shrinking or freeing a Vec or a Map that is read-only storage.
+ The backends hand the runtime the container's address, so this is the
+ store [check_place] refuses, made through the header instead of through a
+ [set]. Writing into the Vec's own buffer is not refused: the const is
+ shallow. *)
+and refuse_const_change _ctx loc (target : Tast.expr) =
+ match const_reached target with
| None -> ()
| Some view ->
let t = Types.to_string target.Tast.ty in
@@ -6646,10 +6691,10 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
Loc.failk "check/unknown-field" loc ~notes:(declared_note ctx.env sname)
"%s has no field %s" sname name
| Some i ->
- if store then Option.iter (refuse_const_place loc) (const_reached target);
+ if store then Option.iter (refuse_const_place ctx.env loc) (const_reached target);
Tast.Pfield (target, i), (List.nth s.Tast.fields i).Tast.fty)
| Ast.Pindex (target, idx) ->
- let target = check ctx target in
+ let target = check_target ctx target in
(match target.Tast.ty with
(* The same bounds and epoch check the value form gets, through the same
helper: an element of a Vec is a place because a Vec element is
@@ -6665,7 +6710,7 @@ and check_place ?(store = true) ctx loc (p : Ast.place) : Tast.place * Types.t =
let target = check ctx target in
(match target.Tast.ty with
| Types.Ptr (Types.Const, _) as view when store ->
- refuse_const_place loc view
+ refuse_const_place ctx.env loc view
| Types.Ptr (_, t) -> Tast.Pderef target, t
| other ->
fail loc "deref takes a (Ptr T), found %s" (Types.to_string other))
@@ -6724,7 +6769,7 @@ and index_expr ctx (e : Ast.expr) =
and indexed ?place ?(store = true) ctx (target : Tast.expr) (idx : Ast.expr list) =
(match place with
| Some l when store ->
- Option.iter (refuse_const_place l)
+ Option.iter (refuse_const_place ctx.env l)
(const_steps (const_reached target) target.Tast.ty (List.length idx))
| _ -> ());
let rec go ty = function
@@ -8087,7 +8132,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 2 args;
(match args with
| [ target; x ] ->
- let target = check ctx target in
+ let target = check_target ctx target in
refuse_const_change ctx loc target;
(* A push into a dyn container is a call and nothing else: no allocation
guard, no restart, no region check. The dyn runtime owns the storage
@@ -8128,7 +8173,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 2 args;
(match args with
| [ target; n ] ->
- let target = check ctx target in
+ let target = check_target ctx target in
refuse_const_change ctx loc target;
let n = check ctx ~want:index_ty n in
let n64 =
@@ -8172,7 +8217,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
is a thing you write, and writing it twice is yours to not do. *)
| "free" ->
arity ctx loc name 1 args;
- let target = check ctx (List.hd args) in
+ let target = check_target ctx (List.hd args) in
refuse_const_change ctx loc target;
(* A container of owning elements is refused here, and a reader will
assume the opposite — that [free] recurses — so this says why it does
@@ -8227,7 +8272,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
(* Checked once, then dispatched on what it turned out to be: checking
it inside a guard as well would allocate the target's slots twice and
evaluate whatever it was written as twice. *)
- let target = check ctx target in
+ let target = check_target ctx target in
let a = allocator_arg ctx loc rest in
(match target.Tast.ty with
(* The refusal that did *not* come down with the type-level ones, and
@@ -8342,7 +8387,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 3 args;
(match args with
| [ target; k; v ] ->
- let target = check ctx target in
+ let target = check_target ctx target in
refuse_const_change ctx loc target;
(* A put into a dyn map is a call and nothing else, the way a push into
a dyn vec is: the runtime owns the storage, so there is no guard, no
@@ -8393,7 +8438,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 2 args;
(match args with
| [ target; k ] ->
- let target = check ctx target in
+ let target = check_target ctx target in
(* A dyn map's absence is nil, not None: the typed map can promise an
(Option V) because V was written down, and a dyn map has nothing to
write. nil is an ordinary dyn value the caller compares against —
@@ -8468,7 +8513,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 2 args;
(match args with
| [ target; k ] ->
- let target = check ctx target in
+ let target = check_target ctx target in
refuse_const_change ctx loc target;
let kt, vt = map_kv loc "map-remove" target.Tast.ty in
let k = check ctx ~want:kt k in
@@ -8506,7 +8551,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 4 args;
(match args with
| [ target; cur; k; v ] ->
- let target = check ctx target in
+ let target = check_target ctx target in
let kt, vt = map_kv loc "map-next" target.Tast.ty in
let cur = check ctx ~want:(Types.Ptr (Types.Mut, (Types.Int Types.I64))) cur in
let k = check ctx ~want:(Types.Ptr (Types.Mut, kt)) k in
@@ -8530,7 +8575,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
arity ctx loc name 2 args;
(match args with
| [ target; k ] ->
- let target = check ctx target in
+ let target = check_target ctx target in
(* The dyn map's question, one word with the typed one. It exists on
the dyn side because absence there is nil, and a map can also store
nil under a key — (get m k) answering nil cannot tell the two
@@ -8849,7 +8894,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
| "length" ->
arity ctx loc name 1 args;
let target = List.hd args in
- let a = check ctx target in
+ let a = check_target ctx target in
(match a.Tast.ty with
| Types.Array _ | Types.Slice _ | Types.String ->
prim Tast.Len index_ty [ a ]
@@ -8876,7 +8921,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
| "at" ->
(match args with
| target :: idx when idx <> [] ->
- let target = check ctx target in
+ let target = check_target ctx target in
(match target.Tast.ty with
| Types.Vec _ ->
let p, elem = vec_at ctx loc target idx in
@@ -8923,7 +8968,7 @@ and named_call ?(qualified = false) ctx ~want loc name args =
"slice is (slice a), (slice a lo) or (slice a lo hi) — given %d \
arguments" (List.length args)
| target :: bounds ->
- let target = check ctx target in
+ let target = check_target ctx target in
let ty = target.Tast.ty in
match ty with
(* A Vec leaves here: everything below is written around a length the
@@ -10004,8 +10049,19 @@ and generic_call ctx ~want loc name vars pats pret args =
| Ast.Int _ | Ast.UInt _ | Ast.Float _ | Ast.Byte _ -> true
| _ -> false
in
+ (* A bare [$t] an earlier argument bound to a slice or a pointer:
+ this argument may differ from it only in const, and the two meet
+ at the read-only one ([Types.const_join]), whichever came first.
+ So it is checked on its own terms rather than against the
+ binding. *)
+ let bound_view =
+ match pat, p with
+ | Types.Var v, (Types.Slice _ | Types.Ptr _)
+ when not (generic_ty p || bound_exactly v) -> Some v
+ | _ -> None
+ in
let a =
- if generic_ty p then check ctx a
+ if generic_ty p || bound_view <> None then check ctx a
else if bound_scalar <> None && not untyped_literal then
(* On its own terms first. A form that has no type without a want
— [(zeroed)] is the one that matters — refuses here and is
@@ -10038,6 +10094,11 @@ and generic_call ctx ~want loc name vars pats pret args =
bound to i64 is an ordinary mismatch and gets the ordinary
refusal below. *)
let handled =
+ match bound_view, Types.const_join p a.Tast.ty with
+ | Some v, Some j ->
+ subst := (v, j) :: List.remove_assoc v !subst;
+ true
+ | _ ->
match bound_scalar with
| Some v
when (not (Types.equal p a.Tast.ty))
@@ -10076,7 +10137,7 @@ and generic_call ctx ~want loc name vars pats pret args =
" — %s takes a slice it may write through, and a %s can \
only be read%s"
name (Types.to_string a.Tast.ty)
- (match const_copy e with
+ (match const_copy ctx.env e with
| Some c ->
Printf.sprintf ". %s copies v into one that can be written" c
| None -> "")
@@ -10126,6 +10187,8 @@ and generic_call ctx ~want loc name vars pats pret args =
&& Types.is_numeric a.Tast.ty
&& Types.widens_to ~from:a.Tast.ty ~into:f ->
widen a.Tast.loc f a
+ | Some f when Types.const_widens ~from:a.Tast.ty ~into:f ->
+ { a with Tast.ty = f }
| _ -> a)
(* And the other widening, for the same reason and at the same
moment: a [CFn] argument against an [(Fn [$t] $t)] parameter.
@@ -10436,7 +10499,7 @@ and trial ctx f =
resource failure into a wrong answer. *)
let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
defers; defer_slot; defer_ok; defer_block; outer = _;
- outer_what; caught; const_locals; envslot; parent = _;
+ outer_what; caught; place_ok; envslot; parent = _;
in_frames; loops; tail; in_defer;
owner = _ } = ctx in
match f () with
@@ -10447,7 +10510,7 @@ and trial ctx f =
ctx.defers <- defers; ctx.defer_slot <- defer_slot;
ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block;
ctx.outer_what <- outer_what; ctx.in_frames <- in_frames;
- ctx.caught <- caught; ctx.const_locals <- const_locals; ctx.envslot <- envslot;
+ ctx.caught <- caught; ctx.place_ok <- place_ok; ctx.envslot <- envslot;
ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer;
Error d
diff --git a/lib/types.ml b/lib/types.ml
index eefb0bbf..d2dff244 100644
--- a/lib/types.ml
+++ b/lib/types.ml
@@ -349,20 +349,21 @@ let rec const_widens ~(from : t) ~(into : t) =
equal a b || const_widens ~from:a ~into:b
| _ -> false
-(* A function of one signature standing where another is wanted, when the
- two differ only in const. A parameter may be more permissive than asked —
- a function that takes a [[const T]] only reads what it is handed, so a
- caller handing it a [[T]] loses nothing — and a result may be less so: a
- [[T]] returned where a [[const T]] is wanted is [const_widens]'s case. The
- two words are the same either way, so [Check.expect] only retypes. *)
-(* The one type two branches of an [if] meet at when they differ only in
- const: the read-only one, whichever branch it came from. *)
+(* The one type two branches of an [if], or two arguments at one type
+ variable, meet at when they differ only in const: the read-only one,
+ whichever came first. *)
let const_join a b =
if equal a b then Some a
else if const_widens ~from:a ~into:b then Some b
else if const_widens ~from:b ~into:a then Some a
else None
+(* A function of one signature standing where another is wanted, when the
+ two differ only in const. A parameter may be more permissive than asked —
+ a function that takes a [[const T]] only reads what it is handed, so a
+ caller handing it a [[T]] loses nothing — and a result may be less so: a
+ [[T]] returned where a [[const T]] is wanted is [const_widens]'s case. The
+ two words are the same either way, so [Check.expect] only retypes. *)
let fn_accepts ~(from : t list * t) ~(into : t list * t) =
let ps', r' = from and ps, r = into in
List.length ps = List.length ps'
diff --git a/test/programs/const-owned.flan b/test/programs/const-owned.flan
new file mode 100644
index 00000000..60f2d142
--- /dev/null
+++ b/test/programs/const-owned.flan
@@ -0,0 +1,39 @@
+;;;; A Vec reached through a [const (Vec T)] or a (Ptr const (Vec T)) is used
+;;;; where it stands — indexed, measured, sliced, its address taken — and never
+;;;; copied out as a value; (clone v) is the copy. The refusals are in
+;;;; test_flan.ml; this is the half that compiles, on both backends.
+
+(defstruct Bag [items (Vec i32) n i32])
+
+(defn total [vs [const (Vec i32)]] i32
+ (let [t 0]
+ (dotimes [i (length vs)]
+ (dotimes [j (length (at vs i))]
+ (set t (+ t (at (at vs i) j)))))
+ t))
+
+(defn first-len [p (Ptr const (Vec i32))] i32 (length (deref p)))
+
+(defn bag-n [bs [const Bag]] i32 (+ (.n (at bs 0)) (length (.items (at bs 0)))))
+
+(defn pick [c bool a $t b $t] $t (if c a b))
+
+(defn main [] i32
+ (let [a (vec-new i32)
+ b (vec-new i32)]
+ (push a 1) (push a 2)
+ (push b 30)
+ (let [vs [a b]
+ cv (the-const (slice vs))
+ w (clone (at cv 0))
+ bags [(Bag {.items b .n 4})]]
+ (push w 99)
+ ;; The shallow rule: the Vec's own buffer is writable through the view.
+ (set (at (at cv 1) 0) 31)
+ (println (total cv) (length w) (length (at cv 0)))
+ (println (first-len (addr (at cv 0))) (bag-n (slice bags)))
+ (println (length (pick true (bytes-view "abc") (bytes "de")))
+ (length (pick false (bytes "de") (bytes-view "abc"))))))
+ 0)
+
+(defn the-const [s [const (Vec i32)]] [const (Vec i32)] s)
diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml
index 6aa6fc54..47b9cdda 100644
--- a/test/test_acceptance.ml
+++ b/test/test_acceptance.ml
@@ -879,6 +879,12 @@ let () =
const_slice_out;
outputs ~x86:true "const slices, --x86" "programs/const-slice.flan"
const_slice_out;
+ let const_owned_out = "34 3 2\n2 5\n3 3\n" in
+ outputs "const owned" "programs/const-owned.flan" const_owned_out;
+ outputs ~opt:"-O0" "const owned, -O0" "programs/const-owned.flan"
+ const_owned_out;
+ outputs ~x86:true "const owned, --x86" "programs/const-owned.flan"
+ const_owned_out;
(* (string b). The conversion emits nothing — String and Slice _ are the
same %slice — so the rows are about length and ownership rather than
arithmetic: a number round-tripped, an empty slice, sub-views whose
diff --git a/test/test_flan.ml b/test/test_flan.ml
index 3624a82b..a0c8c6ca 100644
--- a/test/test_flan.ml
+++ b/test/test_flan.ml
@@ -2361,21 +2361,81 @@ let () =
"(defn f [p (Ptr const $t)] $t (deref p)) (defn g [q (Ptr i32)] i32 (f q))";
accepts "vec-new reads (Ptr const u8) as a type"
"(defn f [] i32 (let [v (vec-new (Ptr const u8))] (length v)))";
- (* A Vec header copied out of read-only storage shares its block, so the
- copy is as read-only as the original, through any number of lets. *)
- rejects_check "push through a let-bound copy of a const element"
- "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0)] (push v 1)))"
- ~needle:"reached through a [const (Vec i32)]";
- rejects_check "reserve through a copy of a copy"
- "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0) w v] (reserve w 9)))"
- ~needle:"reached through a [const (Vec i32)]";
- rejects_check "put through a let-bound copy of a const element"
- "(defn f [cs [const (Map string i32)]] () (let [m (at cs 0)] (put m \"a\" 1)))"
- ~needle:"reached through a [const (Map string i32)]";
- rejects_check "push into a field of a let-bound copy"
- "(defstruct P [v (Vec i32)]) \
- (defn f [cs [const P]] () (let [p (at cs 0)] (push (.v p) 1)))"
- ~needle:"take the P it lives in as a [P]";
+ (* Decision 81: a value that owns storage, reached through read-only
+ storage, is used where it stands and never copied out. Every route a
+ copy could take is refused at the copy. *)
+ let copied = "this copies a (Vec i32) out of a [const (Vec i32)]" in
+ List.iter
+ (fun (name, src) -> rejects_check ("no copy out: " ^ name) src ~needle:copied)
+ [ "let", "(defn f [cs [const (Vec i32)]] () (let [v (at cs 0)] (push v 1)))";
+ "loop binding",
+ "(defn f [cs [const (Vec i32)]] () (loop [v (at cs 0)] (push v 1)))";
+ "if value",
+ "(defn f [c bool cs [const (Vec i32)]] () \
+ (let [v (if c (at cs 0) (at cs 1))] (push v 1)))";
+ "do value",
+ "(defn f [cs [const (Vec i32)]] () (let [v (do (at cs 0))] (push v 1)))";
+ "set into a local",
+ "(defn f [cs [const (Vec i32)]] () \
+ (let [v (vec-new i32)] (set v (at cs 0)) (push v 1)))";
+ "match binding",
+ "(defn f [cs [const (Vec i32)]] i32 \
+ (match (Some (at cs 0)) (Some v) (do (push v 1) 0) None 0))";
+ "array destructure",
+ "(defn f [cs [const (Vec i32)]] () \
+ (let [[a b] [(at cs 0) (at cs 1)]] (push a 1)))";
+ "closure capture",
+ "(defn app [g (Fn [] ())] () (g)) (defn f [cs [const (Vec i32)]] () \
+ (let [v (at cs 0)] (app (fn [] (push v 1)))))";
+ "passed by value",
+ "(defn pusher [v (Vec i32)] () (push v 1)) \
+ (defn f [cs [const (Vec i32)]] () (pusher (at cs 0)))";
+ "returned by value",
+ "(defn g [cs [const (Vec i32)]] (Vec i32) (at cs 0))";
+ "through a generic",
+ "(defn id [x $t] $t x) (defn f [cs [const (Vec i32)]] () (push (id (at cs 0)) 1))" ];
+ rejects_check "no copy out through a const pointer"
+ "(defn f [p (Ptr const (Vec i32))] () (let [v (deref p)] (push v 1)))"
+ ~needle:"this copies a (Vec i32) out of a (Ptr const (Vec i32))";
+ rejects_check "and the copy that is allowed is named"
+ "(defn f [cs [const (Vec i32)]] (Vec i32) (at cs 0))"
+ ~needle:"(clone v) copies it into a (Vec i32) of its own";
+ rejects_check "a struct holding a Vec is not copied out either"
+ "(defstruct P [v (Vec i32)]) (defn f [cs [const P]] P (at cs 0))"
+ ~needle:"(addr v) gives a (Ptr const P) to read it through";
+ rejects_check "nor an array of them"
+ "(defn f [cs [const [2 (Vec i32)]]] [2 (Vec i32)] (at cs 0))"
+ ~needle:"this copies a [2 (Vec i32)] out of a [const [2 (Vec i32)]]";
+ rejects_check "nor an Option of one"
+ "(defn f [cs [const (Option (Vec i32))]] (Option (Vec i32)) (at cs 0))"
+ ~needle:"this copies a (Option (Vec i32)) out";
+ rejects_check "nor a field that owns storage"
+ "(defstruct P [v (Vec i32)]) (defn f [cs [const P]] (Vec i32) (.v (at cs 0)))"
+ ~needle:"this copies a (Vec i32) out of a [const P]";
+ accepts "used where it stands"
+ "(defstruct P [v (Vec i32) n i32]) \
+ (defn f [cs [const (Vec i32)] ps [const P] p (Ptr const (Vec i32))] i32 \
+ (+ (at (at cs 0) 1) (length (at cs 0)) (length (slice (at cs 0))) \
+ (.n (at ps 0)) (length (.v (at ps 0))) (length (deref p)) \
+ (length (deref (addr (at cs 0)))) (length (clone (at cs 0)))))";
+ accepts "a copy of a scalar element is still a copy"
+ "(defn f [cs [const i32]] i32 (let [x (at cs 0)] (set x 5) x))";
+ (* The header copy is suggested only for elements that own nothing. *)
+ rejects_check "no header copy suggested for an array of Vecs"
+ "(defn f [cs [const [2 (Vec i32)]]] () (set (at cs 0) (at cs 1)))"
+ ~needle:"take it as a [[2 (Vec i32)]] instead";
+ rejects_check "nor for an Option of a Vec"
+ "(defn f [cs [const (Option (Vec i32))]] () (set (at cs 0) None))"
+ ~needle:"take it as a [(Option (Vec i32))] instead";
+ (* Two arguments at one type variable meet at const, either order. *)
+ accepts "a generic's arguments join at const"
+ "(defn pick [c bool a $t b $t] $t (if c a b)) \
+ (defn f [c bool cs [const u8] ms [u8]] i32 (+ (length (pick c ms cs)) \
+ (length (pick c cs ms))))";
+ rejects_check "and the join is read-only"
+ "(defn pick [c bool a $t b $t] $t (if c a b)) \
+ (defn f [c bool cs [const u8] ms [u8]] () (set (at (pick c ms cs) 0) 1))"
+ ~needle:"this writes through a [const u8]";
rejects_check "no copy of Vec headers is suggested"
"(defn f [cs [const (Vec i32)]] () (set (at cs 0) (vec-new i32)))"
~needle:"take it as a [(Vec i32)] instead";
From e6ea6572634c94058b43760486bb239cfb033dd0 Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 13:41:49 +0700
Subject: [PATCH 11/13] The array literal given a slice type by the matches a
read-only slice too
---
lib/check.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/lib/check.ml b/lib/check.ml
index 3f2fcda1..a97daa0a 100644
--- a/lib/check.ml
+++ b/lib/check.ml
@@ -6564,7 +6564,7 @@ and check_the ctx ~want loc (t : Ast.texpr) (v : Ast.expr) =
end;
let r =
match ty, v.Ast.e with
- | Types.Slice elem, Ast.Arr items ->
+ | Types.Slice (_, elem), Ast.Arr items ->
check_arr ctx
~want:(Some (Types.Array (Int64.of_int (List.length items), elem)))
v.Ast.loc items
From 8bb2885e63aefec94345f071aad2ac96d9795b10 Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 13:49:24 +0700
Subject: [PATCH 12/13] An abandoned evaluation puts the context allocator
back, and a fault's break loop runs on a guarded stack of its own so a
runaway recursion evaluated there is another break rather than a dead session
---
runtime/flan_dev.c | 93 +++++++++++++++++++++++++++++++++++++++
runtime/flan_rt.c | 14 ++++++
test/test_dev.ml | 50 +++++++++++++++++++++
vendor/agent/flan_agent.c | 8 +++-
4 files changed, 164 insertions(+), 1 deletion(-)
diff --git a/runtime/flan_dev.c b/runtime/flan_dev.c
index a7d99675..332da73e 100644
--- a/runtime/flan_dev.c
+++ b/runtime/flan_dev.c
@@ -2255,8 +2255,95 @@ void flan_dev_crash_enable(void) {}
#include
#include
#include
+#if defined(__linux__) && (defined(__x86_64__) || defined(__aarch64__))
+#include
+#include
+#define FLAN_PARK_STACKS 1
+#endif
extern void (*flan_trap_hook)(const uint8_t *name, int64_t namelen);
+
+#ifdef FLAN_PARK_STACKS
+/* Where a fault's break loop runs. Not the signal stack: the loop evaluates
+ * whatever is typed at it, and a runaway recursion there ran off the end of a
+ * 1 MiB malloc'd block with nothing below it, into the heap. And a fault taken
+ * while already on the signal stack has no stack to be delivered on, so the
+ * kernel kills the process.
+ *
+ * So the handler moves to one of these before calling the hook: 8 MiB each,
+ * mapped on first use, with a guard page at the low end. An overflow on one
+ * faults on its guard, the fault is delivered on the signal stack (the
+ * interrupted code was not on it), and its break loop gets the next stack up.
+ * Which stack is next is read off the interrupted stack pointer: a fault in
+ * code running on stack k parks on k + 1, and every stack above k is free,
+ * because a break loop is only ever left by a jump down to its caller. */
+#define PARK_COUNT 10
+#define PARK_SIZE ((size_t)8 << 20)
+static char *park_lo[PARK_COUNT];
+static ucontext_t park_uc[PARK_COUNT];
+static const uint8_t *park_name;
+static int64_t park_namelen;
+
+/* The guard page counts as the stack's: an overflow's stack pointer is in it
+ * when the fault is taken, and reading it as some other stack's would park the
+ * overflow's break loop on the very stack it overflowed. */
+static int park_index_of(uintptr_t sp) {
+ uintptr_t pg = (uintptr_t)sysconf(_SC_PAGESIZE);
+ for (int i = 0; i < PARK_COUNT; i++)
+ if (park_lo[i] != NULL && sp >= (uintptr_t)park_lo[i] - pg
+ && sp <= (uintptr_t)park_lo[i] + PARK_SIZE)
+ return i;
+ return -1;
+}
+
+static char *park_stack(int i) {
+ if (park_lo[i] == NULL) {
+ size_t pg = (size_t)sysconf(_SC_PAGESIZE);
+ char *m = mmap(NULL, PARK_SIZE + pg, PROT_READ | PROT_WRITE,
+ MAP_PRIVATE | MAP_ANONYMOUS | MAP_NORESERVE, -1, 0);
+ if (m == MAP_FAILED) return NULL;
+ if (mprotect(m, pg, PROT_NONE) != 0) {
+ munmap(m, PARK_SIZE + pg);
+ return NULL;
+ }
+ park_lo[i] = m + pg;
+ }
+ return park_lo[i];
+}
+
+static uintptr_t park_interrupted_sp(void *uc) {
+ const ucontext_t *u = (const ucontext_t *)uc;
+#if defined(__x86_64__)
+ return (uintptr_t)u->uc_mcontext.gregs[15]; /* REG_RSP */
+#else
+ return (uintptr_t)u->uc_mcontext.sp;
+#endif
+}
+
+static void park_run(void) {
+ flan_trap_hook(park_name, park_namelen);
+ /* The hook parks and is left only by a jump; reaching here is dying. */
+ signal(SIGSEGV, SIG_DFL);
+ raise(SIGSEGV);
+}
+
+/* Calls the hook on the next park stack, or returns 0 when there is none to
+ * be had and the caller should call it where it stands. */
+static int park_elsewhere(void *uc, const uint8_t *name, int64_t namelen) {
+ int k = park_index_of(park_interrupted_sp(uc)) + 1;
+ char *st = k < PARK_COUNT ? park_stack(k) : NULL;
+ if (st == NULL) return 0;
+ park_name = name;
+ park_namelen = namelen;
+ if (getcontext(&park_uc[k]) != 0) return 0;
+ park_uc[k].uc_stack.ss_sp = st;
+ park_uc[k].uc_stack.ss_size = PARK_SIZE;
+ park_uc[k].uc_link = NULL;
+ makecontext(&park_uc[k], park_run, 0);
+ setcontext(&park_uc[k]);
+ return 0;
+}
+#endif
extern void __asan_init(void) __attribute__((weak));
static volatile sig_atomic_t flan_crash_entered;
@@ -2347,6 +2434,12 @@ static void crash_handler(int sig, siginfo_t *si, void *uc) {
/* Parks for good, exactly like NullAllocator and the other no-channel
* traps: there is no address to resume *at* — the faulting instruction
* would fault again — so this is a place to stand and read. */
+#ifdef FLAN_PARK_STACKS
+ if (sig == SIGBUS)
+ park_elsewhere(uc, (const uint8_t *)"BusError", 8);
+ else
+ park_elsewhere(uc, (const uint8_t *)"SegFault", 8);
+#endif
if (sig == SIGBUS)
flan_trap_hook((const uint8_t *)"BusError", 8);
else
diff --git a/runtime/flan_rt.c b/runtime/flan_rt.c
index 40495be1..5e6bb186 100644
--- a/runtime/flan_rt.c
+++ b/runtime/flan_rt.c
@@ -1561,6 +1561,20 @@ void flan_context_restore(flan_allocator *a) {
if (a) flan_ctx_alloc = a;
}
+/* The context as it stands, and putting it back: the agent's way out of an
+ * evaluation that trapped jumps past the [with-allocator] that would have
+ * restored it. Two words, which is room for whatever the context grows into;
+ * the agent only carries them. */
+void flan_context_save(uint64_t m[2]) {
+ m[0] = (uint64_t)(uintptr_t)flan_ctx_alloc;
+ m[1] = 0;
+}
+
+void flan_context_load(const uint64_t m[2]) {
+ flan_allocator *a = (flan_allocator *)(uintptr_t)m[0];
+ flan_ctx_alloc = a ? a : &flan_heap;
+}
+
/* Allocator headers [flan_arena_destroy] retired, linked through [data]. See
* there for why a header is never freed; this is why that does not grow. */
static flan_allocator *flan_retired;
diff --git a/test/test_dev.ml b/test/test_dev.ml
index 8eba3fdc..5a92bb29 100644
--- a/test/test_dev.ml
+++ b/test/test_dev.ml
@@ -7785,6 +7785,7 @@ let () =
let r =
request tc
"(:op \"eval\" :code \"(defonce nowhere Allocator)\n\
+ (defonce frame Allocator)\n\
(defn deep [n i64] i64 (+ 1 (deep (+ n 1))))\" \
:file \"programs/dev-nomain.flan\")"
in
@@ -7820,6 +7821,55 @@ let () =
fail "aborting %s (%s) ended the session: %s" code shape
(Printexc.to_string e)))
[ "(free-all nowhere)"; "(deep 0)" ];
+ let stopped () =
+ await (fun () ->
+ match Wire.field (request tc "(:op \"describe\")") "stopped" with
+ | Some { Form.v = Form.Sym "t"; _ } -> true
+ | _ -> false)
+ in
+ let eval_expr code =
+ request tc
+ (Printf.sprintf "(:op \"eval-expr\" :code %S :file \"\")" code)
+ in
+ let answers code want what =
+ match Wire.string_field (eval_expr code) "value" with
+ | Some v when v = want -> ()
+ | v ->
+ fail "%s (%s): %s" what shape (Option.value ~default:"no value" v)
+ | exception e ->
+ fail "%s (%s) ended the session: %s" what shape (Printexc.to_string e)
+ in
+ (* The context allocator a trapped [with-allocator] had bound is put
+ back: a push through the context afterwards goes to the heap, not
+ to the 4 KiB arena, which would run out. *)
+ ignore (eval_expr "(do (set frame (arena-new 4096)) 0)");
+ ignore (eval_expr "(with-allocator frame (deep 0))");
+ if not (stopped ()) then fail "a trap inside with-allocator (%s) did not stop" shape
+ else begin
+ ignore (request tc "(:op \"abort\")");
+ answers
+ "(let [v (vec-new i64)] (dotimes [i 100000] (push v i)) (length v))"
+ "100000" "the context allocator after a trap inside with-allocator"
+ end;
+ (* A runaway recursion evaluated in the break loop of a fault: the
+ loop runs on a stack of its own with a guard page, so the second
+ overflow is a second break, and both abort. *)
+ ignore (eval_expr "(deep 0)");
+ if not (stopped ()) then fail "the first overflow (%s) did not stop" shape
+ else begin
+ ignore (eval_expr "(deep 0)");
+ (match request tc "(:op \"abort\")" with
+ | r when status r = "ok" -> ()
+ | r -> fail "aborting a nested overflow (%s): %s" shape (said r)
+ | exception e ->
+ fail "a nested overflow (%s) ended the session: %s" shape
+ (Printexc.to_string e));
+ (* The inner break unwinds on the program's thread; the second
+ abort is for the outer one, so it waits for that. *)
+ Unix.sleepf 0.5;
+ ignore (request tc "(:op \"abort\")");
+ answers "(helper)" "1" "the session after a nested overflow"
+ end;
(try
ignore (Wire.send tc "(:op \"close\")");
ignore (Wire.recv tc)
diff --git a/vendor/agent/flan_agent.c b/vendor/agent/flan_agent.c
index 7945a954..d151ca7d 100644
--- a/vendor/agent/flan_agent.c
+++ b/vendor/agent/flan_agent.c
@@ -410,7 +410,8 @@ static const uint8_t abandon_name[] = "abandon-evaluation";
* restart is a return that unwinds frame by frame, and a trap has nothing to
* return through, so abandoning the evaluation from one is a jump straight
* back to the poll that called it ([flan_agent_poll]), which puts the
- * condition, frame and root chains back where they stood. The defers of the
+ * condition, frame and root chains and the context allocator back where
+ * they stood. The defers of the
* frames jumped over do not run. NULL when no evaluation is in progress;
* saved and restored around the call like [eval_boundary]. */
static sigjmp_buf *eval_escape;
@@ -426,6 +427,8 @@ extern void *flan_dev_frames_mark(void) __attribute__((weak));
extern void flan_dev_frames_restore(void *head) __attribute__((weak));
extern int64_t flan_dyn_root_mark(void) __attribute__((weak));
extern void flan_dyn_root_restore(int64_t n) __attribute__((weak));
+extern void flan_context_save(uint64_t m[2]) __attribute__((weak));
+extern void flan_context_load(const uint64_t m[2]) __attribute__((weak));
/* -- update-instance-for-redefined-class ------------------------------ */
@@ -1153,6 +1156,8 @@ int32_t flan_agent_poll(void) {
if (flan_condition_stacks_mark) flan_condition_stacks_mark(&mh, &mr, &md);
if (flan_dev_frames_mark) mf = flan_dev_frames_mark();
if (flan_dyn_root_mark) mroots = flan_dyn_root_mark();
+ uint64_t mctx[2] = { 0, 0 };
+ if (flan_context_save) flan_context_save(mctx);
if (sigsetjmp(escape, 1) == 0) {
eval_escape = &escape;
j.call();
@@ -1160,6 +1165,7 @@ int32_t flan_agent_poll(void) {
if (flan_condition_stacks_restore) flan_condition_stacks_restore(mh, mr, md);
if (flan_dev_frames_restore) flan_dev_frames_restore(mf);
if (flan_dyn_root_restore) flan_dyn_root_restore(mroots);
+ if (flan_context_load) flan_context_load(mctx);
}
eval_escape = oescape;
/* Popped whichever way the thunk left — returning with a value, or
From 9373c4311338177c759f9cddaaaf52e6cc778c72 Mon Sep 17 00:00:00 2001
From: Joseph Ferano
Date: Fri, 25 Sep 2026 13:56:11 +0700
Subject: [PATCH 13/13] The nested-overflow test waits for the outer break to
be on top instead of sleeping, and names a session that dies
---
test/test_dev.ml | 24 +++++++++++++++++++++---
1 file changed, 21 insertions(+), 3 deletions(-)
diff --git a/test/test_dev.ml b/test/test_dev.ml
index 5a92bb29..4708ba89 100644
--- a/test/test_dev.ml
+++ b/test/test_dev.ml
@@ -7854,10 +7854,23 @@ let () =
(* A runaway recursion evaluated in the break loop of a fault: the
loop runs on a stack of its own with a guard page, so the second
overflow is a second break, and both abort. *)
+ (try
ignore (eval_expr "(deep 0)");
if not (stopped ()) then fail "the first overflow (%s) did not stop" shape
else begin
ignore (eval_expr "(deep 0)");
+ (* How many restarts the stopped break lists, which is what tells
+ the inner break from the outer — both are SegFault. The inner
+ one lists its own evaluation's boundary and, below it, the
+ outer one's. *)
+ let listed () =
+ match Wire.field (request tc "(:op \"break\")") "restarts" with
+ | Some { Form.v = Form.List l; _ } -> List.length l
+ | _ -> -1
+ in
+ let inner = listed () in
+ if inner < 2 then
+ fail "the nested overflow (%s) listed %d restarts" shape inner;
(match request tc "(:op \"abort\")" with
| r when status r = "ok" -> ()
| r -> fail "aborting a nested overflow (%s): %s" shape (said r)
@@ -7865,11 +7878,16 @@ let () =
fail "a nested overflow (%s) ended the session: %s" shape
(Printexc.to_string e));
(* The inner break unwinds on the program's thread; the second
- abort is for the outer one, so it waits for that. *)
- Unix.sleepf 0.5;
+ abort is for the outer one, so it waits until the break on top
+ is the outer one. *)
+ if not (await ~ms:30000 (fun () -> let d = listed () in d > 0 && d < inner))
+ then fail "the inner overflow's break (%s) was never left" shape;
ignore (request tc "(:op \"abort\")");
answers "(helper)" "1" "the session after a nested overflow"
- end;
+ end
+ with (Wire.Closed | Unix.Unix_error _) as e ->
+ fail "a nested overflow (%s) ended the session: %s" shape
+ (Printexc.to_string e));
(try
ignore (Wire.send tc "(:op \"close\")");
ignore (Wire.recv tc)