Add support for atomic_min* and atomic_umin* intrinsics#1212
Merged
danielsn merged 8 commits intomodel-checking:mainfrom May 26, 2022
Merged
Add support for atomic_min* and atomic_umin* intrinsics#1212danielsn merged 8 commits intomodel-checking:mainfrom
atomic_min* and atomic_umin* intrinsics#1212danielsn merged 8 commits intomodel-checking:mainfrom
Conversation
danielsn
suggested changes
May 25, 2022
| // Expressions defined on top of other expressions | ||
|
|
||
| /// `min(self, e)` | ||
| pub fn min(self, e: Expr) -> Expr { |
Contributor
There was a problem hiding this comment.
If there are side effects, this will evaluate them twice
Contributor
Author
There was a problem hiding this comment.
Please take a look at the new changes, which complete the definition for is_side_effect and assert that neither of these cause side effects.
danielsn
reviewed
May 25, 2022
Comment on lines
+290
to
+297
| fn are_side_effect(exprs: &Vec<Expr>) -> bool { | ||
| for expr in exprs { | ||
| if expr.is_side_effect() { | ||
| return true; | ||
| } | ||
| } | ||
| false | ||
| } |
Contributor
There was a problem hiding this comment.
Style ⛏️ : you could use exprs.iter().any(|e| e.is_side_effect())
|
|
||
| #[kani::proof] | ||
| fn main() { | ||
| let mut a1 = 1 as u8; |
Contributor
There was a problem hiding this comment.
Is there a reason we only test for u8? Could we make this take a <T> and then test multiple bitwidths?
Contributor
Author
There was a problem hiding this comment.
Yes, that's pending in #25. But I'd like to do it once all atomic tests are in.
danielsn
approved these changes
May 26, 2022
4 tasks
77 tasks
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 free
to 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.
Description of changes:
Defines a
minexpression on top of other expressions. Then uses theminexpression to add support foratomic_min*andatomic_umin*intrinsics.Resolved issues:
Part of #1163
Testing:
How is this change tested? Removes 10 tests and adds 2.
Is this a refactor change? No.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.