Uh oh!
There was an error while loading. Please reload this page.
Add a #[derive(Invariant)] macro - #3250
Merged
Merged
Conversation
celinval
left a comment
Contributor
There was a problem hiding this comment.
Can you add a little test where an invariant created fails? Something like you have a type A with a custom safety invariant and a struct B with a derived Invariant that has a member of type A. Now ensure that breaking the A invariant in the B field also breaks B invariant. Thanks!
adpaco
commented
Jun 13, 2024
ContributorAuthor
Added a test where the invariant check fails but let me know if you have suggestions for the setup step (right now it's just an overly generic |
celinval
approved these changes
Jun 13, 2024
celinval
left a comment
Contributor
There was a problem hiding this comment.
We need to figure out how to ensure Arbitrary respects Invariant.
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
adpaco
enabled auto-merge (squash)
June 13, 2024 23:14
This was referenced Jun 21, 2024
Merged
adpaco added a commit
that referenced
this pull request
Jul 22, 2024
…rary` and `Invariant` macros (#3283) This PR enables an `#[safety_constraint(...)]` attribute helper for the `#[derive(Arbitrary)]` and `#[derive(Invariant)]` macro. For the `Invariant` derive macro, this allows users to derive more sophisticated invariants for their data types by annotating individual named fields with the `#[safety_constraint(<cond>)]` attribute, where `<cond>` represents the predicate to be evaluated for the corresponding field. In addition, the implementation always checks `#field.is_safe()` for each field. For example, let's say we are working with the `Point` type from #3250 ```rs #[derive(kani::Invariant)] struct Point<X, Y> { x: X, y: Y, } ``` and we need to extend it to only allow positive values for both `x` and `y`. With the `[safety_constraint(...)]` attribute, we can achieve this without explicitly writing the `impl Invariant for ...` as follows: ```rs #[derive(kani::Invariant)] struct PositivePoint { #[safety_constraint(*x >= 0)] x: i32, #[safety_constraint(*y >= 0)] y: i32, } ``` For the `Arbitrary` derive macro, this allows users to derive more sophisticated `kani::any()` generators that respect the specified invariants. In other words, the `kani::any()` will assume any invariants specified through the `#[safety_constraint(...)]` attribute helper. Going back to the `PositivePoint` example, we'd expect this harness to be successful: ```rs #[kani::proof] fn check_invariant_helper_ok() { let pos_point: PositivePoint = kani::any(); assert!(pos_point.x >= 0); assert!(pos_point.y >= 0); } ``` The PR includes tests to ensure it's working as expected, in addition to UI tests checking for cases where the arguments provided to the macro are incorrect. Happy to add any other cases that you feel are missing. Related #3095
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds a
#[derive(Invariant)]macro for structs which allows users to automatically derive theInvariantimplementations for any struct. The derived implementation determines the invariant for the struct as the conjunction of invariants of its fields. In other words, the invariant is derived astrue && self.field1.is_safe() && self.field2.is_safe() && ...For example, for the struct
we derive the
Invariantimplementation asRelated #3095
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.