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

Fix codegen_atomic_binop for atomic_ptr #3047

Merged
merged 5 commits into from
Feb 29, 2024

Conversation

qinheping
Copy link
Contributor

Fetch functions of atomic_ptr calls atomic intrinsic functions with pointer-type arguments (invalid_mut), which will cause typecheck failures. The change in this commit add support of pointer-type arguments into codegen_atomic_binop to fix the issue. The new codegen_atomic_binop will cast pointer arguments to size_t, apply op on them, and then cast the op result back to the pointer type.

The new test include all fetch functions of atomic_ptr except for fetch_ptr_add and fetch_ptr_sub, which do not call intrinsic functions.

Resolves #3042.

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

Fetch functions of atomic_ptr calls atomic intrinsics functions with pointer-type arguments (invalid_mut), which will cause typecheck failures.
The change in this commit add support of pointer-type arguments into codegen_atomic_binop to fix the issue.
The new codegen_atomic_binop will cast pointer arguments to size_t, apply op on them, and then cast the op result back to the pointer type.

Fix the issue model-checking#3042.
@qinheping qinheping requested a review from a team as a code owner February 28, 2024 06:56
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Feb 28, 2024
@qinheping
Copy link
Contributor Author

Partially resolve #25. The benchmarks included in this PR test atomic intrinsic with type of *mut i64.

tests/kani/AtomicPtr/atomic_ptr.rs Outdated Show resolved Hide resolved
tests/kani/AtomicPtr/atomic_ptr.rs Outdated Show resolved Hide resolved
tests/kani/AtomicPtr/atomic_ptr.rs Outdated Show resolved Hide resolved
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

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

Thanks @qinheping!

tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs Outdated Show resolved Hide resolved
@adpaco-aws adpaco-aws enabled auto-merge (squash) February 29, 2024 20:18
@adpaco-aws adpaco-aws merged commit 73b4c47 into model-checking:main Feb 29, 2024
20 checks passed
zhassan-aws added a commit that referenced this pull request Mar 13, 2024
These are the original release notes for the reference:

## What's Changed
* Automatic cargo update to 2024-02-26 by @github-actions in
#3043
* Upgrade rust toolchain to 2024-02-17 by @celinval in
#3040
* Upgrade `windows-targets` crate to version 0.52.4 by @adpaco-aws in
#3049
* Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in
#3047
* Upgrade Rust toolchain to `nightly-2024-02-25` by @adpaco-aws in
#3048
* Update s2n-quic submodule by @zhassan-aws in
#3050
* Update s2n-quic submodule weekly through dependabot by @zhassan-aws in
#3053
* Retrieve info for recursion tracker reliably by @feliperodri in
#3045
* Automatic cargo update to 2024-03-04 by @github-actions in
#3055
* Upgrade Rust toolchain to `nightly-2024-03-01` by @adpaco-aws in
#3052
* Add `--use-local-toolchain` to Kani setup by @jaisnan in
#3056
* Replace internal reverse_postorder by a stable one by @celinval in
#3064
* Add option to override `--crate-name` from `kani` by @adpaco-aws in
#3054
* cargo update and fix macos CI by @zhassan-aws in
#3067
* Bump tests/perf/s2n-quic from `d103836` to `1a7faa8` by @dependabot in
#3066
* Upgrade toolchain to 2024-03-11 by @zhassan-aws in
#3071
* Emit `dead` goto-instructions on MIR StatementDead by @karkhaz in
#3063


**Full Changelog**:
kani-0.47.0...kani-0.48.0
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
None yet
Development

Successfully merging this pull request may close these issues.

Kani crashes when handling code related to AtomicPtr
3 participants