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

The gen word leaves both headers: a check nothing runs is weight, and Odin carries none of it

Browse Source
This commit is contained in:
Joseph Ferano 2026-09-18 12:23:39 +07:00
parent 4a563d0e67
commit bb2471f7a1
4 changed files with 29 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
lib/check.ml
View File

@ -3831,9 +3831,9 @@ and named_call ctx ~want loc name args =
(* spec-memory.md's first release point. Since the repeal, what it consumes
it consumes at run time only: nothing marks the binding dead, so a second
[free] or a read after this one type-checks and misbehaves at run time —
the allocator aborts on a double free it can see, and the dev build's
generation word traps a stale read. That is the Odin contract: free is a
thing you write, and writing it twice is yours to not do. *)
the allocator aborts on a double free it can see, and the epoch word
traps a read through a released region. That is the Odin contract: free
is a thing you write, and writing it twice is yours to not do. *)
| "free" ->
arity loc name 1 args;
let target = check ctx (List.hd args) in

19
lib/emit.ml
View File

@ -287,7 +287,7 @@ let rec lay m (t : Types.t) : int * int =
| Types.Ptr _ -> 8, 8
| Types.Alloc -> 8, 8
| Types.Fn _ -> 8, 8
| Types.Vec _ | Types.Map _ -> 48, 8
| Types.Vec _ | Types.Map _ -> 40, 8
(* [n x T] adds no padding of its own: T's size already carries its tail. *)
| Types.Array (n, e) -> let s, a = lay m e in Int64.to_int n * s, a
| Types.Option e -> let s, a, _ = lay_fields m [ Types.Int Types.I8; e ] in s, a
@ -512,15 +512,15 @@ let rec dty m d (t : Types.t) : int =
| Types.Alloc ->
dnode d
"!DIDerivedType(tag: DW_TAG_pointer_type, name: \"Allocator\", baseType: null, size: 64)"
(* Shown as what it is. The two dev words are in the layout and so they
are here too: a debugger that showed four fields of a six-field struct
would put the reader's offsets out by two. *)
(* Shown as what it is. The epoch word is in the layout and so it is
here too: a debugger that showed four fields of a five-field struct
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);
("cap", Types.Int Types.I64); ("allocator", Types.Alloc);
("gen", Types.Int Types.I64); ("epoch", Types.Int Types.I64) ]
(* Six fields again, and shown as six for the same reason: a debugger
("epoch", Types.Int Types.I64) ]
(* Five fields again, and shown as five for the same reason: a debugger
that showed fewer would put the reader's offsets out. [log2cap] is
shown rather than a capacity because that is what is stored — the
capacity is 1 << it, and a debugger that invented the shift would be
@ -529,8 +529,7 @@ let rec dty m d (t : Types.t) : int =
composite (Types.to_string t)
[ ("data", Types.Ptr (Types.Int Types.U8));
("len", Types.Int Types.I64); ("log2cap", Types.Int Types.I64);
("allocator", Types.Alloc); ("gen", Types.Int Types.I64);
("epoch", Types.Int Types.I64) ]
("allocator", Types.Alloc); ("epoch", Types.Int Types.I64) ]
|> fun n -> ignore k; ignore v; n
(* 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
@ -2668,11 +2667,11 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
%slice = type { ptr, i64 }
; (Vec T), spec-memory.md. The element type is nowhere in it: the runtime is
; type-erased and every operation is handed size and align at its call site.
%vec = type { ptr, i64, i64, ptr, i64, i64 }
%vec = type { ptr, i64, i64, ptr, i64 }
; (Map K V), spec-memory.md — Odin's open-addressed Robin Hood map. Neither key
; nor value type appears in it, for the same reason: one type-erased runtime,
; handed the two sizes and a hash/equality pair at each call site.
%map = type { ptr, i64, i64, ptr, i64, i64 }
%map = type { ptr, i64, i64, ptr, i64 }
; A handler frame: the one it displaced, the condition type it matches, and
; the lifted function that runs. Allocated on the establishing frame's stack.
%handler = type { ptr, i32, ptr }

45
runtime/flan_rt.c
View File

@ -906,8 +906,7 @@ struct flan_allocator {
void *data;
uint32_t caps;
/* Bumped on every free-all. A container records it and traps if it moved:
* spec-memory.md, "Dev builds detect a released region". Separate from the
* per-Vec generation word, which answers a different question. */
* spec-memory.md, "Dev builds detect a released region". */
uint64_t epoch;
/* Dev accounting for the general-purpose tier: "did you forget to free" is
* an allocator-tier question and this is the allocator's answer. */
@ -1392,30 +1391,26 @@ _Noreturn void flan_region_only_fail(const uint8_t *loc, int64_t loclen) {
* produce the numbers, and it passes them in. There are no generics here and
* none are needed.
*
* Header, and it is six words rather than the spec's four:
* Header, and it is five words rather than the spec's four:
*
* ptr len cap allocator the release layout spec-memory.md fixes
* gen bumped on every reallocation — the stale-slice
* word spec-memory.md asks for. It has no reader
* and cannot have one as things stand, which is
* the part "not yet" used to hide: a slice is
* ptr+len, so it carries neither the Vec it came
* from nor the generation it was taken at, and
* the check has nothing to compare. Giving it a
* reader is a third word on every slice in the
* language, not a change to this file. Nothing
* here or anywhere else reads it; do not write
* code that trusts it. See docs/BUILT.md.
* epoch the allocator's epoch when this Vec last
* touched it. Any operation on a container whose
* recorded epoch has moved traps.
*
* The two dev words are present in every build, not only a dev one, and that
* There used to be a sixth word, gen, the stale-slice generation
* spec-memory.md once asked for. It was bumped on every reallocation and
* consulted by nothing — a slice is ptr+len and carries neither the Vec it
* came from nor the generation it was taken at, so the check it promised had
* nothing to compare — and Odin's header (data, len, cap, allocator, and
* nothing else) is the model this one follows. Deleted 2026-09-18 with the
* ownership repeal; see docs/BUILT.md.
*
* The epoch word is present in every build, not only a dev one, and that
* is not laziness: a redefinition module is built by llc and ld against a host
* that was built separately, and nothing makes the two agree on a struct size.
* A layout that changes with a build flag is a layout that can disagree across
* that boundary silently. Dropping them in release is deferred and docs/BUILT.md
* says what it is blocked on.
* that boundary silently.
*
* Every entry point returns int8_t 1/0 for "did it fit", and never reports
* failure any other way: the condition, the restart and the message are the
@ -1426,7 +1421,6 @@ typedef struct flan_vec {
int64_t len;
int64_t cap;
flan_allocator *alloc;
int64_t gen;
int64_t epoch;
} flan_vec;
@ -1546,7 +1540,6 @@ static int8_t flan_vec_grow(flan_vec *v, int64_t want, int64_t size,
v->cap = cap;
/* Any slice taken before this points at storage that may have moved. The
* word is bumped here and read nowhere yet; see docs/BUILT.md. */
v->gen++;
return 1;
}
@ -1565,7 +1558,6 @@ int8_t flan_vec_init(flan_vec *v, flan_allocator *a, int64_t cap, int64_t size,
v->ptr = NULL;
v->len = 0;
v->cap = 0;
v->gen = 0;
v->alloc = a;
v->epoch = (int64_t)v->alloc->epoch;
if (cap <= 0) return 1;
@ -1649,7 +1641,6 @@ void flan_vec_free(flan_vec *v, int64_t size, int64_t align,
v->len = 0;
v->cap = 0;
v->alloc = NULL;
v->gen++;
v->epoch = 0;
}
@ -1701,11 +1692,11 @@ int8_t flan_vec_clone(flan_vec *dst, flan_vec *src, flan_allocator *a,
* data one allocation: keys | values | hashes | scratch
* len live entries
* log2cap 0 until something is allocated; never 1 or 2 after
* allocator gen epoch as on a Vec, and checked the same way
* allocator epoch as on a Vec, and checked the same way
*
* Odin stuffs log2cap into the low six bits of the data pointer because its
* Raw_Map must be three words. This header already carries an allocator, a
* generation and an epoch, so the bit-stuffing would buy nothing and cost a
* Raw_Map must be three words. This header already carries an allocator and
* an epoch, so the bit-stuffing would buy nothing and cost a
* mask on every access — and, more usefully, not tagging means correctness
* never depends on the block being 64-byte aligned. It is requested as 64, and
* cell packing pays off when the request is honoured, but an arena whose base
@ -1757,7 +1748,6 @@ typedef struct flan_map {
int64_t len;
int64_t log2cap;
flan_allocator *alloc;
int64_t gen;
int64_t epoch;
} flan_map;
@ -2274,7 +2264,7 @@ static int8_t flan_map_grow(flan_map *m, int64_t want, int64_t ksize,
if (log2cap <= m->log2cap && m->data) return 1;
fresh.data = NULL; fresh.len = 0; fresh.log2cap = 0;
fresh.alloc = a; fresh.gen = 0; fresh.epoch = (int64_t)a->epoch;
fresh.alloc = a; fresh.epoch = (int64_t)a->epoch;
if (!flan_map_alloc(&fresh, a, log2cap, ksize, vsize)) return 0;
if (m->data) {
@ -2302,7 +2292,6 @@ static int8_t flan_map_grow(flan_map *m, int64_t want, int64_t ksize,
m->len = fresh.len;
/* Every key and value moved, so any pointer into the old block is stale —
* the same word, bumped for the same reason, as a Vec's reallocation. */
m->gen++;
return 1;
}
@ -2313,7 +2302,6 @@ int8_t flan_map_init(flan_map *m, flan_allocator *a, int64_t ksize,
m->data = NULL;
m->len = 0;
m->log2cap = 0;
m->gen = 0;
m->alloc = a;
m->epoch = (int64_t)a->epoch;
/* No block until something is put in it: an empty map that is never written
@ -2529,7 +2517,6 @@ void flan_map_free(flan_map *m, int64_t ksize, int64_t vsize,
m->len = 0;
m->log2cap = 0;
m->alloc = NULL;
m->gen++;
m->epoch = 0;
}

2
test/test_acceptance.ml
View File

@ -762,7 +762,7 @@ let () =
let dbg = Emit.program ~debug:true (Check.program
(Parse.program (Reader.read_file "programs/vec.flan"))) in
if not (contains dbg "name: \"Allocator\"")
|| not (contains dbg "name: \"(Vec i32)\", size: 384")
|| not (contains dbg "name: \"(Vec i32)\", size: 320")
then begin
incr failures;
print_endline "FAIL debug info for Allocator and (Vec T)"