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

Simple Stubbing with Contracts #2746

Merged
merged 29 commits into from
Sep 27, 2023

Conversation

JustusAdam
Copy link
Contributor

@JustusAdam JustusAdam commented Sep 7, 2023

Description of changes:

Expands the contract features introduced in #2655 by completing the checking with stubbing/replacement capabilities.

Resolved issues:

Resolves #2621

Related RFC: 0009 Function Contracts

Tracking issue: #2652

Optional #ISSUE-NUMBER.

Call-outs:

This makes the internal state machine in the macro expansion more explicit. Previously it was a single, long function it is now a struct and an enum that hold the state and the generation is split into multiple methods on those. While technically a refactoring change to some degree it really only made sense to do this now, as now there are two dimensions along which the macro codegen operates.

  1. Type of attribute (requires/ensures). This one was present before also.
  2. Type of generated function (checking/replacement). This is new.

Testing:

  • How is this change tested? New expected test cases

  • Is this a refactor change? No

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@JustusAdam JustusAdam added this to the Function Contracts MVP milestone Sep 7, 2023
@JustusAdam JustusAdam self-assigned this Sep 7, 2023
@JustusAdam JustusAdam changed the title Simple contract replacement Simple Stubbing with Contracts Sep 7, 2023
@JustusAdam JustusAdam marked this pull request as ready for review September 8, 2023 21:10
@JustusAdam JustusAdam requested a review from a team as a code owner September 8, 2023 21:10
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

It looks good so far! I still need to review the proc_macro logic.

kani-compiler/src/kani_middle/attributes.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/attributes.rs Outdated Show resolved Hide resolved
kani-compiler/src/kani_middle/attributes.rs Outdated Show resolved Hide resolved
library/kani_macros/src/lib.rs Outdated Show resolved Hide resolved
@JustusAdam
Copy link
Contributor Author

I've made a bit of a major change and added a "module-level" contract documentation as kani::contracts that provides a general overview and a central place for information about contracts and also how the various attributes interact.

I would appreciate any feedback you ahve on this new "module-level" documentation. I think at this point it doesn't have to be perfect as it will expand with future contract PRs anyway but whether it's good in broad strokes. Also if you have the time, download it and build the docs for the kani library and let me know if it works.

This now offers also the possibility of grouping all contract attributes in this module. I haven't done that here, I just reexport them, but I could if people want.

Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

I'm impressed with all this macro magic. Thanks!

library/kani/src/contracts.rs Outdated Show resolved Hide resolved
library/kani_macros/src/lib.rs Show resolved Hide resolved
library/kani/src/contracts.rs Show resolved Hide resolved
library/kani_macros/src/sysroot/contracts.rs Outdated Show resolved Hide resolved
library/kani_macros/src/sysroot/contracts.rs Outdated Show resolved Hide resolved
library/kani_macros/src/sysroot/contracts.rs Outdated Show resolved Hide resolved
library/kani_macros/src/sysroot/contracts.rs Outdated Show resolved Hide resolved
library/kani_macros/src/sysroot/contracts.rs Outdated Show resolved Hide resolved
library/kani_macros/src/sysroot/contracts.rs Show resolved Hide resolved
tests/expected/function-contract/type_annotation_needed.rs Outdated Show resolved Hide resolved
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Amazing! Thanks @JustusAdam

@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Sep 26, 2023
@JustusAdam
Copy link
Contributor Author

Resolving the last conversation (the obscure paragraph) was quite tricky and lead to a major expansion in the docs. You may want to give them a read and see if they make sense @celinval and also it now has the diagram you wanted @feliperodri.

You may want to read the rendered version which you can get with cargo rustdoc -p kani_macros -- --cfg kani --document-private-items

Copy link
Contributor

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

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

Thank you, Justus! Only small nitpicks (feel free to merge) and the state machine looks very clear!

kani-compiler/src/kani_middle/attributes.rs Outdated Show resolved Hide resolved
library/kani/src/contracts.rs Outdated Show resolved Hide resolved
library/kani/src/contracts.rs Outdated Show resolved Hide resolved
library/kani_macros/src/sysroot/contracts.rs Outdated Show resolved Hide resolved
@JustusAdam JustusAdam merged commit dba1674 into model-checking:main Sep 27, 2023
13 checks passed
@JustusAdam JustusAdam deleted the simple-contract-replacement branch September 27, 2023 18:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
No open projects
Status: No status
Status: No status
Development

Successfully merging this pull request may close these issues.

Stubbing with Contracts
3 participants