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

Improve the check_generics pass #515

Merged
merged 8 commits into from
Jan 6, 2025

Conversation

Nadrieril
Copy link
Member

This does a few things to improve the check_generics pass:

  • We now track for each GenericArgs what item it applies to. This greatly simplifies the pass and will be a tremendous help for Hide associated types equality constraints #127;
  • We pretty-print the llbc before running the pass, which makes it possible to inspect the llbc output even when it faile;
  • We now track which items have been visited so that errors have more context to them.

@Nadrieril
Copy link
Member Author

Nadrieril commented Jan 6, 2025

Other features I'd like to eventually add to this pass:

  • Check that each generic variable reference points to something;
  • Check the number and type of function arguments in function calls (will likely require fixing closures first);
  • Check that referenced associated types actually exist (I'm waiting for Support for Generic Associated Types #477);
  • Check the number and type of aggregate fields (also waiting for closure fixes);
  • Check the generics and arguments of built-in types and functions.

@Nadrieril Nadrieril merged commit 3a41196 into AeneasVerif:main Jan 6, 2025
5 checks passed
@Nadrieril Nadrieril deleted the generics-source branch January 6, 2025 13:58
@sonmarcho
Copy link
Member

Checking that I understand what you are doing: the GenericSource tracks the item owning the generic args, correct?
For instance, if I have Array::index<T, N> then the generic source of <T, N> is Builtin, while it is Item if I have Vec<T>, right?
Whenever I need this kind of information in a micro-pass, I implement a visitor which carries an (optional) environment around, by overriding the proper methods to update the environments whenever I, say, visit a Call, Adt construct, etc. I'm wondering: why didn't you make that choice (it may be more straightforward/natural to do in OCaml of course)?

@Nadrieril
Copy link
Member Author

Nadrieril commented Jan 6, 2025

For instance, if I have Array::index<T, N> then the generic source of <T, N> is Builtin, while it is Item if I have Vec, right?

Correct

Whenever I need this kind of information in a micro-pass, I implement a visitor which carries an (optional) environment around, by overriding the proper methods to update the environments whenever I, say, visit a Call, Adt construct, etc. I'm wondering: why didn't you make that choice (it may be more straightforward/natural to do in OCaml of course)?

This is pretty much what I did before, you can see the diff in the PR. The problem is that this requires manually listing every spot where a GenericArgs might be, which is error-prone and annoying to maintain. In fact my previous attempt at simplifying this was by using FunDeclRef/TraitDeclRef/etc consistently, but this wasn't enough for e.g. function calls without other undesirable changes.

This would have been fine if it was just for this pass, but #127 requires something similar and even more subtle, hence why I came up with this imo very pleasing solution.

@sonmarcho
Copy link
Member

That makes sense, thanks for the explanations!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants