From 70f87d90b235a1832e535add8eb8fd9eb07c7647 Mon Sep 17 00:00:00 2001 From: Joseph Ferano Date: Sun, 20 Sep 2026 00:25:49 +0700 Subject: [PATCH] A visited set crossed a question it was never asked MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- lib/check.ml | 14 +++++++++++++- test/test_flan.ml | 43 ++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 53 insertions(+), 4 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index 3f45eb6..982a30a 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -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 diff --git a/test/test_flan.ml b/test/test_flan.ml index d530b2e..bac3efa 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -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\