types: eliminate some blowups when finalizing and dropping types - #375
Open
apoelstra wants to merge 4 commits into
Open
types: eliminate some blowups when finalizing and dropping types#375apoelstra wants to merge 4 commits into
apoelstra wants to merge 4 commits into
Conversation
I have a 300kb program (produced by a clanker) that has an
exponentially-sized type DAG. This is fine until we call
`Type::finalize`, which has the amusing comment
// Now that we know our types have finite size, we can safely use a
// post-order iterator to finalize them.
Well, this -would- be safe if we weren't using the `NoSharing` tracker in
our post-order iterator. AFAICT I did this just to be lazy. Stop being
lazy and implement a sharing tracker that tracks BoundRefs, thereby only
iterating through as many nodes an we actually allocated.
I don't have a good unit test; for one thing, my test vector is 300kb so
I don't want to put it in this repo (I'll throw it in qa-assets so it's
at least available, though I need to think what kind of harness we
should write for it). But also, the failure mode is that this code just
iterates forever, allocating 600Gb+ of RAM, which Rust makes a bit hard
to detect. We should investigate using an alternate allocator that can
limit memory, or something, in the fuzzer.
But the existing unit and fuzz tests should confirm that this doesn't
break anything. In fact the fuzzer should run much faster now.
For `Node` this is actually not too bad, because the type is mutally recursive with `Inner`, so we can move out of the Inner type without getting stupid "cannot move out of type that implements Drop" errors. High-level structure was written by ChatGPT 5.6 Sol, but I rewrote it to factor out the `into_dag` method and make the other code more terse.
Just copy exactly the same logic we added for Type in src/types/mod.rs. When we panic on type-inference errors we often try to debug-dump an entire Incomplete, which may be exponential in size. Possibly we want BoundRef-sharing here too? At least for Debug output? I dunno. Certainly what we -don't- want is to run forever outputting nothing, which is the existing behavior that this commit fixes.
Unlike the case for `Node`, `types::Incomplete` is a directly recursive type (or rather, it holds an `Arc<Incomplete>`, but we can't implement anything on `Arc` so for our purposes it may as well just be `Incomplete`) which means that we hit a Rust bug preventing us moving stuff out of it. We need unsafe code to move out of the Rust bug. Hopefully this code, which is mostly comments and directly analogous to the code we just added to Node, is easy enough to follow. You can run the `root_unit_to_unit` in Miri which exercises this path, and if you introduce UB (say, by removing the call to `mem::forget`) it'll detect it.
Collaborator
Author
|
On 51992e5 successfully ran local tests |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Improves
types::Type::finalizeso that it doesn't unshare the type DAG when finalizing. This is important because we need to finalize the types before we can get static bounds, meaning that we can't reject exponentially-sized programs until after this method has succeeded.Along the way, because I was testing with an extremely deep program found by the Bitcoin Red Team, I ran into stack overflows dropping both
Nodeandtypes::Incomplete. This PR replaces those with manually-written non-recursive impls. It also copies the display-limiting logic fromtypes::Typetotypes::Incomplete.