-
Notifications
You must be signed in to change notification settings - Fork 13.2k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Back-edge check (Semant.is_back_edge) is too strong #162
Comments
Thank you so much for figuring this out, Patrick. I was pretty frustrated that I couldn't make sense of the problem before, and you cut to the heart of it. Some clarification that at least helps me: there's a very concrete reason why the ordering and the restriction are necessary. It's not that the type has unbounded size (all trees have unbounded size), nor even that it has infinite size. For example, with the type:
could still have finite size. CONS(1, CONS(2, CONS(3, NIL()))) is perfectly finite. But the problem is that it doesn't have /statically predictable size/, which is one of the key aspects of the Rust design. As another example: in a sense, there's nothing inherently worse about the type:
compared to the type:
Both of them are impossible to instantiate, so neither really threatens any kind of safety properties. But the first type has statically unpredictable size, whereas the second has a static size that can be inductively computed, thanks to the ordering you describe. So in summary: by imposing a well-ordering on these potentially cyclic types, we recover an inductively defined, static sizeof operation. |
Fixed in commit bc03c82. |
Fix "&mut sef" typo in RFC 39 Lifetime Elision
Update to rustc 1.19.0-nightly (777ee20 2017-05-01)
stdbuild conditional change
Constant item grammar
* Install CBMC viewer in CI * Require cbmc-viewer version for installation
The back-edge check to prevent infinitely nested tag types rejects some valid programs, namely those that look like this:
The order of the tag declarations must be switched.
Instead of comparing opaque IDs, we could instead do the following: In the Semant context, store a well-ordering on every tag type. Every time a type /a/ is contained in a type /b/ without boxing, we declare that /a/ < /b/. Then boxed back-pointers from /b/ to /a/ result in opaque types. Any contradiction (declaring that /b/ < /a/ when /a/ < /b/ is already established) results in an error, because a type would have infinite size.
The text was updated successfully, but these errors were encountered: