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

Support building Heapster shapes from Rust type declarations #85

Merged
merged 35 commits into from
Apr 29, 2021

Conversation

ChrisEPhifer
Copy link
Member

This PR adds a number of RsConvert instances and a simple parser entry-point to support the synthesis of Heapster shapes from Rust types.

Marked as WIP as I implement the saw-script side of things (adding a command to interface with these features); there is a branch off wip-heapster for that work, named the same as this one (feature/rust-type-decls).

@ChrisEPhifer ChrisEPhifer changed the title WIP: Support building Heapster shapes from Rust type declarations Support building Heapster shapes from Rust type declarations Apr 27, 2021
@ChrisEPhifer
Copy link
Member Author

@eddywestbrook I believe this is ready to go! All of the examples in rust_data.saw have been updated to use this new machinery, and the Coq output looks to be error-free.

Once we get this merged I'll tag you in saw-script for the corresponding merge into wip-heapster.

Copy link
Contributor

@eddywestbrook eddywestbrook left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A few nitpicky things:

  1. Please add a Haddock to isRecursiveDef
  2. Maybe change the Haddock for parseLLVMShapeFromRust to say that it is parsing a type definition or declaration or whatever you think the correct noun is. It's a bit confusing (at least to me) to say it is parsing types, because other code in the same module does in fact parse types to shapes
  3. And on a similar note, maybe change the name of parseLLVMShapeFromRust to something like parseNamedShapeFromRustDecl or parseRustTypeDecl or rsParseConvertTypeDecl or something like that

@ChrisEPhifer
Copy link
Member Author

Nits have been picked :) Gonna merge this in!

@ChrisEPhifer ChrisEPhifer merged commit 313c7b7 into master Apr 29, 2021
@ChrisEPhifer ChrisEPhifer deleted the feature/rust-type-decls branch April 29, 2021 21:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants