Skip to content
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

Closed
pcwalton opened this issue Sep 16, 2010 · 2 comments
Closed

Back-edge check (Semant.is_back_edge) is too strong #162

pcwalton opened this issue Sep 16, 2010 · 2 comments
Labels
A-type-system Area: Type system

Comments

@pcwalton
Copy link
Contributor

The back-edge check to prevent infinitely nested tag types rejects some valid programs, namely those that look like this:

tag a { ... }
tag b { FOO(a); }

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.

@dherman
Copy link
Contributor

dherman commented Sep 16, 2010

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:

tag list { CONS(int, list); NIL(); }

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:

tag void { VOID(void); }

compared to the type:

tag void { VOID(@void); }

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.

@pcwalton
Copy link
Contributor Author

Fixed in commit bc03c82.

arielb1 pushed a commit to arielb1/rust that referenced this issue Apr 10, 2015
Fix "&mut sef" typo in RFC 39 Lifetime Elision
oli-obk pushed a commit to oli-obk/rust that referenced this issue Jul 19, 2017
Update to rustc 1.19.0-nightly (777ee20 2017-05-01)
keeperofdakeys pushed a commit to keeperofdakeys/rust that referenced this issue Dec 12, 2017
dlrobertson pushed a commit to dlrobertson/rust that referenced this issue Nov 29, 2018
antoyo added a commit to antoyo/rust that referenced this issue Jun 7, 2022
celinval pushed a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
* Install CBMC viewer in CI

* Require cbmc-viewer version for installation
This issue was closed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-type-system Area: Type system
Projects
None yet
Development

No branches or pull requests

2 participants