Cap maximum depth of incomplete type display#221
Conversation
apoelstra
force-pushed
the
2024-06--infinite-loop
branch
from
343b1ec to
868964a
Compare
| // input type. Will fail trying to unify the input type with the unit type *before* | ||
| // doing the occurs check, putting an infinitely-sized type into the error variant. | ||
| // Check that this error type can be printed in finite space/time. | ||
| let mut iter = BitIter::from([0xc1, 0x07, 0x20, 0x30].iter().copied()); |
There was a problem hiding this comment.
50293ca This test case would be better maintainable if we wrote it in the human encoding. We should strive to remove all byte blobs from the code base.
There was a problem hiding this comment.
I'll take a look, but our options for decoding ConstructNodes are pretty limited.
| } | ||
|
|
||
| #[test] | ||
| fn regression_177_1() { |
There was a problem hiding this comment.
50293ca: Adding this test case before the infinite loop is fixed means that CI runs forever on this commit. @apoelstra Does your local CI have a timeout?
There was a problem hiding this comment.
Oh, lol, let me reorder the commits. I don't know if I have a timeout, but if I do, it is in exceess of an hour..
uncomputable
left a comment
uncomputable
left a comment
There was a problem hiding this comment.
868964a Looks great, but let's move the test commit to the back.
I originally wanted to do this but couldn't because we weren't capping the depth of error bound prints. Now we are.
Our existing occurs-check loop iterates through an incomplete type using the NoSharing sharing tracker. This means that for exponentially-sized types, we will do exponentially many iterations, even though the types by-construction have a linear-sized description (in the number of shared nodes in the program). What we want to do is use the InternalSharing sharing tracker, *but* this tracker is too agressive about sharing: it will not repeat nodes at all, while to do the occurs-check, we want to repeat nodes that occur inside themselves. Instead we just implement a pre-order iterator inline (it is very simple and we don't really need the dag.rs abstractions), implementing exactly the occurs-check that we need.
apoelstra
force-pushed
the
2024-06--infinite-loop
branch
from
868964a to
66b2ddb
Compare
|
Reordered commits and rewrote the regression test to use the human-readable encoding. Conveniently with the human-readable encoding I can test both the bind error and the occurs-check error at once, since it attempts to continue after the first error. |
2 participants
This limit may still be too high -- I think you can output a 2^64 sized type which will wreck any terminal. But at least it's finite now.
Every instance of
_itermethods called on an incomplete type (in the types/ module anyway) now has a maximum depth on it, which should eliminate all the places where we might loop forever with incomplete types.Fixes #177