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

A visited set crossed a question it was never asked

Browse Source 
The foreign boundary walks two questions, and they are not the same question:
one counts a dyn reachable only through a further pointer, the other counts
any dyn at all.  They shared a [seen] set across the crossing between them, so
a type name marked visited on the way down was pruned from the walk below the
pointer — and the shape that hits it is a struct with a pointer to its own
name.  [(defstruct Node [next (Ptr Node) x dyn])] at a [(Ptr Node)] parameter
was accepted, while exactly the same thing unrolled into two types was
refused, which is the tell.  A cycle of two, [A {b (Ptr B), x dyn}] and
[B {a (Ptr A)}], went the same way.

C hung a malloc'd node off [next], put a dyn in it, and Flan allocated a
hundred thousand times: heap-use-after-free in flan_dyn_tag out of c_peek,
freed by gc_sweep out of flan_gc_collect.  The checker accepted it and the
collector freed a live value, which is the one failure this boundary exists to
prevent.

The set does not travel across the crossing now.  It still terminates — each
walk's own set guards its own recursion over names, and a crossing starts a
separate finite walk — and it does not start refusing a recursive shape with
no dyn under it, which has rows of its own here because that is the way a fix
like this goes wrong.

Neither recursive shape had a row.  That gap is why it took four passes over
this code to surface, so both are pinned now, alongside the two acceptances
that say termination held.  And the three return rows stop sharing one needle:
each names its own type, because three rows against the common half of one
sentence would all pass on a message that named the wrong shape.

dune test --force: green, 0 failures.
This commit is contained in:
Joseph Ferano 2026-09-20 00:25:49 +07:00
parent a1111f7b3c
commit 70f87d90b2
2 changed files with 53 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
lib/check.ml
View File

@ -7486,7 +7486,19 @@ let dyn_through p seen t = dyn_reach ~through:true p seen t
let rec dyn_behind_pointer p seen (t : Types.t) =
let go = dyn_behind_pointer p seen in
match t with
| Types.Ptr e | Types.Slice e -> dyn_through p seen e
(* The crossing, and the [seen] set does *not* travel across it. The two
walks ask different questions — this one does not count a direct dyn, the
one below it does — so a name already visited on the way here would be
pruned from a question it was never asked. That is not a nicety: a struct
with a pointer to itself and a dyn field is exactly the shape that hits
it, and [(defstruct Node [next (Ptr Node) x dyn])] at [(Ptr Node)] was
accepted while the same thing unrolled into two types was refused. C
hung a node off [next], put a dyn in it, and the collector freed it —
which is the one failure this whole boundary exists to prevent.
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.Array (_, e) | Types.Vec e | Types.Option e -> go e
| Types.Map (k, v) -> go k || go v
| Types.Dyn | Types.Fn _ -> false

43
test/test_flan.ml
View File

@ -976,23 +976,26 @@ let () =
and stopped let the other two through: each of them stores a dyn into C
memory and reads it back after a collection, and each is a
heap-use-after-free in flan_dyn_tag under ASan. *)
(* Each on the *type* it names and not on the shared half of the sentence:
three rows against one needle would all still pass if the message named
the wrong shape, which is the one thing these rows exist to tell apart. *)
rejects_check "a pointer to a dyn-bearing struct returned from C"
"(defstruct S [x dyn])\n\
(declare grab [] (Ptr S) \"c_grab\")\n\
(defn main [] i32 0)"
~needle:"storage this compiler never rooted";
~needle:"the return type of grab (the C symbol c_grab) is (Ptr S)";
rejects_check "a pointer to a pointer to one, returned from C"
"(defstruct S [x dyn])\n\
(declare grab [] (Ptr (Ptr S)) \"c_grab\")\n\
(defn main [] i32 0)"
~needle:"storage this compiler never rooted";
~needle:"is (Ptr (Ptr S)), and a dyn is reachable through it";
(* The shape shim.ml's own advice tells people to write for an aggregate
result, which is what made this one worth having a test of its own. *)
rejects_check "a pointer to a slice of them, returned from C"
"(defstruct S [x dyn])\n\
(declare grab [] (Ptr [S]) \"c_grab\")\n\
(defn main [] i32 0)"
~needle:"storage this compiler never rooted";
~needle:"is (Ptr [S]), and a dyn is reachable through it";
(* And an out-parameter, which is a return wearing a parameter's clothes:
the cell is this compiler's, the pointer C writes into it is C's. *)
rejects_check "an out-parameter handing back a pointer to one"
@ -1013,6 +1016,40 @@ let () =
"(defstruct S [x dyn])\n\
(declare take [s [S]] () \"c_take\")\n\
(defn main [] i32 0)";
(* A pointer field back to the type's own name, which is the shape that had
no row and needed four passes to surface. The two walks at this boundary
ask different questions — one counts a direct dyn and the other does not
— and they shared a visited set, so [Node] was marked seen on the way
down and then pruned from the question below the pointer. It came out
accepted while the same thing written as two types came out refused,
which is the tell. C hung a malloc'd node off [next], put a dyn in it and
read it back after a hundred thousand allocations: heap-use-after-free in
flan_dyn_tag, freed by gc_sweep. *)
rejects_check "a struct with a pointer to itself and a dyn field"
"(defstruct Node [next (Ptr Node) x dyn])\n\
(declare walk [p (Ptr Node)] () \"c_walk\")\n\
(defn main [] i32 0)"
~needle:"is (Ptr Node), and a dyn is reachable through it";
(* And the same fact through a cycle of two, because a fix that only reset
the set for a self-reference would pass the row above and fail this. *)
rejects_check "two structs pointing at each other, with a dyn in one"
"(defstruct A [b (Ptr B) x dyn])\n\
(defstruct B [a (Ptr A)])\n\
(declare walk [p (Ptr A)] () \"c_walk\")\n\
(defn main [] i32 0)"
~needle:"is (Ptr A), and a dyn is reachable through it";
(* The other side of resetting the set: it must still terminate, and it must
not start refusing a recursive shape with no dyn anywhere under it. Both
of these walk a cycle and both are ordinary. *)
accepts "a self-referential struct with no dyn in it"
"(defstruct L [next (Ptr L) n i64])\n\
(declare walk [p (Ptr L)] () \"c_walk\")\n\
(defn main [] i32 0)";
accepts "a cycle of two with no dyn in either"
"(defstruct M [other (Ptr N) n i64])\n\
(defstruct N [back (Ptr M)])\n\
(declare walk [p (Ptr M)] () \"c_walk\")\n\
(defn main [] i32 0)";
rejects_check "a dyn field under an Option"
"(defstruct S [x dyn])\n\
(defn f [] (Option S) None)\n\