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

maps.flan, and a move refusal that names the type it is about

Browse Source 
test/programs/maps.flan is seven claims over the Map, each one a
plausible wrong version gets wrong, with the numbers differing per
failure so a single wrong answer names its own cause: an integer key
past eight grows, a struct key whose padding must never be hashed, a
struct key holding a string, an enum key, clone's independence, upsert
not growing the length, and a map living in an arena.

The move refusal said "a Vec is move-only" whatever had been moved, so
moving a Map was reported as a fact about Vecs. It names the type now.
This commit is contained in:
Joseph Ferano 2026-09-12 15:59:19 +07:00
parent 008eec0ad5
commit e0aedadd74
3 changed files with 111 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
lib/check.ml
View File

@ -1071,7 +1071,7 @@ and var ctx loc ~want name =
| _ ->
match lookup ctx name with
| Some b ->
if Types.is_move_only b.bty then moved ctx loc name b.slot;
if Types.is_move_only b.bty then moved ~ty:b.bty ctx loc name b.slot;
expect loc ~want (mk loc b.bty (Tast.Local b.slot))
| None ->
match Hashtbl.find_opt ctx.env.globals name with
@ -1086,15 +1086,16 @@ and var ctx loc ~want name =
a borrow, which is the conservative direction: passing one to a function,
binding it, returning it and [free]ing it are all moves and all reach here,
and the handful of operations that only look at a container say so. *)
and moved ctx loc name slot =
and moved ?ty ctx loc name slot =
(match List.assoc_opt slot ctx.dead with
| Some where ->
fail loc
"%s was moved at %s and cannot be used again — a Vec is move-only, so \
"%s was moved at %s and cannot be used again — %s is move-only, so \
binding, passing or returning one transfers ownership and the source \
binding is dead afterwards (spec-memory.md). That rule is what makes a \
double free unrepresentable; (clone %s) if you wanted a second one"
name (Loc.to_string where) name
name (Loc.to_string where)
(match ty with Some t -> Types.to_string t | None -> "a Vec") name
| None -> ());
if not ctx.borrow then ctx.dead <- (slot, loc) :: ctx.dead

106
test/programs/maps.flan Normal file
View File

@ -0,0 +1,106 @@
;;;; (Map K V) — spec-memory.md, step 4 of the container build order.
;;;;
;;;; Odin's map: open-addressed Robin Hood hashing at a 75% load factor, with
;;;; cache-line cell packing. Every claim below is one a plausible wrong
;;;; version gets wrong, and the numbers differ per failure so a single wrong
;;;; answer names its own cause.
(defstruct Cell [x i32 y i32])
(defstruct Named [tag string n i32])
(defenum Suit [hearts 0 spades 1 clubs 2])
(defn main [] i32
;; (1) An integer key past several grows. The map starts at 8 slots, so 2000
;; entries is eight reallocations, and every one of them rehashes against a
;; fresh seed — the seed is derived from the block address, so carrying the
;; old hashes over would put every entry in the wrong slot. A wrong grow
;; shows up as a non-zero second number, not as a crash.
(let [m (map-new i32 i64)]
(dotimes [i 2000]
(put m i (* (i64 i) 3)))
(print (len m)) (println "") ; 2000
(let [bad 0]
(dotimes [i 2000]
(match (get m i)
(Some v) (if (not (= v (* (i64 i) 3))) (set bad (+ bad 1)))
None (set bad (+ bad 1))))
(print bad) (println "")) ; 0
(free m))
;; (2) A struct key. The compiler emits a hash and an equality pair for Cell
;; and walks it field by field, so the padding a struct may carry is never
;; read — bytewise hashing of a padded struct is the failure this covers, and
;; it would show as entries that cannot be found again.
(let [g (map-new Cell i32)]
(dotimes [i 40]
(dotimes [j 40]
(put g (Cell {.x i .y j}) (+ (* i 100) j))))
(print (len g)) (println "") ; 1600
(match (get g (Cell {.x 7 .y 9}))
(Some v) (do (print v) (println "")) ; 709
None (println "missing"))
(print (has-key? g (Cell {.x 39 .y 39}))) (println "") ; true
(print (has-key? g (Cell {.x 40 .y 0}))) (println "") ; false
(free g))
;; (3) A struct key holding a string. The string field hashes its *bytes*, so
;; two equal strings at different addresses find the same entry; hashing the
;; ptr+len pair bytewise instead would make every lookup here miss.
(let [n (map-new Named i32)]
(put n (Named {.tag "alpha" .n 1}) 10)
(put n (Named {.tag "alpha" .n 2}) 20)
(put n (Named {.tag "beta" .n 1}) 30)
(print (len n)) (println "") ; 3
(match (get n (Named {.tag "alpha" .n 2}))
(Some v) (do (print v) (println "")) ; 20
None (println "missing"))
(print (has-key? n (Named {.tag "alpha" .n 3}))) (println "") ; false
(free n))
;; (4) An enum key, which is an i32 at run time but its own type here.
(let [s (map-new Suit i32)]
(put s :hearts 1)
(put s :clubs 3)
(print (len s)) (println "") ; 2
(match (get s :clubs)
(Some v) (do (print v) (println "")) ; 3
None (println "missing"))
(print (has-key? s :spades)) (println "") ; false
(free s))
;; (5) clone is a deep, independent copy — spec-memory.md, "copying is always
;; explicit". A map's clone reinserts rather than copying the block, because
;; the seed moves with the address; a bytewise copy would be a map whose
;; stored hashes disagree with its own seed and whose every lookup missed.
(let [a (map-new i32 i32)]
(put a 1 100)
(put a 2 200)
(let [b (clone a)]
(put b 1 999)
(match (get a 1) (Some v) (do (print v) (println "")) None (println "?")) ; 100
(match (get b 1) (Some v) (do (print v) (println "")) None (println "?")) ; 999
(print (len b)) (println "") ; 2
(free b))
(free a))
;; (6) Upsert replaces and does not grow the length, and reserve means room
;; for n *entries* — n still under the load factor — not n slots.
(let [u (map-new string i32)]
(reserve u 100)
(put u "k" 1)
(put u "k" 2)
(put u "k" 3)
(print (len u)) (println "") ; 1
(match (get u "k") (Some v) (do (print v) (println "")) None (println "?")) ; 3
(free u))
;; (7) A map lives in an arena as happily as on the heap. The arena cannot
;; free, so free keeps the block — releasing it is free-all's job — and
;; nothing here may read the block back after the region is reset.
(let [ar (arena-new 1048576)]
(with-allocator ar
(let [t (map-new i32 i32)]
(dotimes [i 500] (put t i (* i 2)))
(print (len t)) (println "") ; 500
(match (get t 499) (Some v) (do (print v) (println "")) None (println "?")))) ; 998
(free-all ar))
0)

52
tmpchk/m2.flan
View File

@ -1,52 +0,0 @@
(defstruct Cell [x i32 y i32])
(defstruct Named [tag string n i32])
(defn main [] i32
;; An integer key, past several grows: 2000 entries in a map that starts at 8.
(let [m (map-new i32 i64)]
(dotimes [i 2000]
(put m i (* (i64 i) 3)))
(print (len m)) (println "")
(let [bad 0]
(dotimes [i 2000]
(match (get m i)
(Some v) (if (not (= v (* (i64 i) 3))) (set bad (+ bad 1)))
None (set bad (+ bad 1))))
(print bad) (println ""))
(free m))
;; A struct key: the compiler emits a hash and an equality pair for Cell and
;; walks it field by field, so padding is never read.
(let [g (map-new Cell i32)]
(dotimes [i 40]
(dotimes [j 40]
(put g (Cell {.x i .y j}) (+ (* i 100) j))))
(print (len g)) (println "")
(match (get g (Cell {.x 7 .y 9})) (Some v) (do (print v) (println "")) None (println "missing"))
(print (has-key? g (Cell {.x 39 .y 39}))) (println "")
(print (has-key? g (Cell {.x 40 .y 0}))) (println "")
(free g))
;; A struct key holding a string: the string field hashes its bytes, so two
;; equal strings at different addresses find the same entry.
(let [n (map-new Named i32)]
(put n (Named {.tag "alpha" .n 1}) 10)
(put n (Named {.tag "alpha" .n 2}) 20)
(put n (Named {.tag "beta" .n 1}) 30)
(print (len n)) (println "")
(match (get n (Named {.tag "alpha" .n 2})) (Some v) (do (print v) (println "")) None (println "missing"))
(print (has-key? n (Named {.tag "alpha" .n 3}))) (println "")
(free n))
;; clone is a deep, independent copy.
(let [a (map-new i32 i32)]
(put a 1 100)
(put a 2 200)
(let [b (clone a)]
(put b 1 999)
(match (get a 1) (Some v) (do (print v) (println "")) None (println "missing"))
(match (get b 1) (Some v) (do (print v) (println "")) None (println "missing"))
(print (len b)) (println "")
(free b))
(free a))
0)