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.

Sign up for GitHub

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

Jump to bottom

Finish refactoring on how we handle the metadata file for Tests and PubFns #2493

Closed
celinval opened this issue May 30, 2023 · 2 comments
Closed

Finish refactoring on how we handle the metadata file for Tests and PubFns #2493

celinval opened this issue May 30, 2023 · 2 comments
Assignees
@celinval
Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected. Z-Kani Compiler Issues that require some changes to the compiler
Milestone
Stubbing

Comments

@celinval
Copy link
Contributor

celinval commented May 30, 2023 •
edited
Loading

Proposed change: To solve #1841 we moved the metadata generation to the kani_compiler for the Harness reachability mode. We should also change how we handle Tests and PubFns.

Motivation: The code has two very distinct logic to handle metadata, which is more fragile and harder to maintain. We only partitioned this work into separate issues to reduce the size of the PR.

Note: We also need to ensure we store unsupported features to the metadata files.
@celinval celinval added the [C] Internal Tracks some internal work. I.e.: Users should not be affected. label May 30, 2023
@celinval celinval added this to the Stubbing milestone May 30, 2023
@celinval celinval mentioned this issue May 30, 2023
Merged
4 tasks
@celinval celinval added the Z-Kani Compiler Issues that require some changes to the compiler label May 30, 2023
@celinval celinval self-assigned this Jun 1, 2023
celinval added a commit to celinval/kani-dev that referenced this issue Jul 26, 2023
@celinval
Delay writing metadata file
e7d2c04 
Change required for model-checking#2493
and contracts work. This will allow us to store information collected
during code generation.
celinval added a commit to celinval/kani-dev that referenced this issue Jul 27, 2023
@celinval
Delay writing metadata file
f528e6e 
Change required for model-checking#2493
and contracts work. This will allow us to store information collected
during code generation.
@celinval celinval mentioned this issue Jul 27, 2023
Merged
4 tasks
celinval added a commit that referenced this issue Jul 29, 2023
@celinval
Delay writing metadata file (no UX impact) (#2628)
f024d23 
Kani compiler will now only store KaniMetadata after compiling all harnesses. Before, we were storing before codegen in the first iteration of the compiler.

This will still allow us to generate metadata without actually performing codegen, if we ever implement a `kani list` subcommand. The metadata won't be stored though if Kani fails to codegen. However, we don't do anything extra with that file if the compilation fails.

This change is required for #2493 and contracts work. This will allow us to store information collected during code generation.
@celinval
Copy link
Contributor Author

This is no longer needed since #3245.

@carolynzech
Copy link
Contributor

Closing since this is no longer needed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@celinval celinval

Labels
[C] Internal Tracks some internal work. I.e.: Users should not be affected. Z-Kani Compiler Issues that require some changes to the compiler
Projects
No open projects
Kani 2023-06-19
Status: No status
Milestone
Stubbing
Development

No branches or pull requests
2 participants
@celinval @carolynzech