Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Feat rust newtypes members #5918

Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Open

Conversation

MikaelMayer
Copy link
Member

@MikaelMayer MikaelMayer commented Nov 14, 2024

Description

This PR adds

  • Support for newtypes wrapping other newtypes
  • Full conversions between newtypes and primitive types
  • Support for methods on newtypes
  • It also adds an attribute {:rust_erased true/false} for newtypes to override the default erasure setting for newtypes, which is:
    • Newtypes without members: Erased (so that we can see Rust's native types like u8, u32, etc.)
    • Newtypes with members: Not erased (to improve legibility of the code in Rust)
  • Support for general newtypes on booleans
  • Support in the generated Rust AST for metadata on types, to know if a type supports Copy or now. Previously it had to be known statically for primitive, but now with newtypes we need to embed this information into the tree.
  • Support for wrapping operations for bitvectors and newtypes based on bitvectors

How has this been tested?

  • Modified the test comp/rust/newtypes.dfy to support all the new cases, including use of the attribute {:rust_erased} and various cases
  • Added test case newtypesrefresh.dfy for the newtypes on booleans
  • Had to fix the code to make existing tests to pass

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

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

Successfully merging this pull request may close these issues.

1 participant