Skip to content

Commit e3a7bec

Browse files
author
Carolyn Zech
committed
update to 6/9
1 parent e5f548c commit e3a7bec

File tree

19 files changed

+293
-227
lines changed

19 files changed

+293
-227
lines changed

‎kani-compiler/src/intrinsics.rs‎

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -471,55 +471,55 @@ impl Intrinsic {
471471
fn try_match_atomic(intrinsic_instance: &Instance) -> Option<Intrinsic> {
472472
let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap();
473473
let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder();
474-
if let Some(suffix) = intrinsic_str.strip_prefix("atomic_and_") {
474+
if let Some(suffix) = intrinsic_str.strip_prefix("atomic_and") {
475475
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
476476
Some(Intrinsic::AtomicAnd(suffix.into()))
477-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchgweak_") {
477+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchgweak") {
478478
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_));
479479
Some(Intrinsic::AtomicCxchgWeak(suffix.into()))
480-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchg_") {
480+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchg") {
481481
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_));
482482
Some(Intrinsic::AtomicCxchg(suffix.into()))
483-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_fence_") {
483+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_fence") {
484484
assert_sig_matches!(sig, => RigidTy::Tuple(_));
485485
Some(Intrinsic::AtomicFence(suffix.into()))
486486
} else if intrinsic_str == "atomic_load" {
487487
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _);
488488
Some(Intrinsic::AtomicLoad)
489-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_max_") {
489+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_max") {
490490
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
491491
Some(Intrinsic::AtomicMax(suffix.into()))
492-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_min_") {
492+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_min") {
493493
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
494494
Some(Intrinsic::AtomicMin(suffix.into()))
495-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_nand_") {
495+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_nand") {
496496
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
497497
Some(Intrinsic::AtomicNand(suffix.into()))
498-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_or_") {
498+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_or") {
499499
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
500500
Some(Intrinsic::AtomicOr(suffix.into()))
501-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_singlethreadfence_") {
501+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_singlethreadfence") {
502502
assert_sig_matches!(sig, => RigidTy::Tuple(_));
503503
Some(Intrinsic::AtomicSingleThreadFence(suffix.into()))
504-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_store_") {
504+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_store") {
505505
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_));
506506
Some(Intrinsic::AtomicStore(suffix.into()))
507-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umax_") {
507+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umax") {
508508
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
509509
Some(Intrinsic::AtomicUmax(suffix.into()))
510-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umin_") {
510+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umin") {
511511
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
512512
Some(Intrinsic::AtomicUmin(suffix.into()))
513-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xadd_") {
513+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xadd") {
514514
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
515515
Some(Intrinsic::AtomicXadd(suffix.into()))
516-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xchg_") {
516+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xchg") {
517517
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
518518
Some(Intrinsic::AtomicXchg(suffix.into()))
519-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xor_") {
519+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xor") {
520520
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
521521
Some(Intrinsic::AtomicXor(suffix.into()))
522-
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xsub_") {
522+
} else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xsub") {
523523
assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
524524
Some(Intrinsic::AtomicXsub(suffix.into()))
525525
} else {

‎rust-toolchain.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2025-06-07"
5+
channel = "nightly-2025-06-09"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

‎tests/expected/uninit/atomic/atomic.rs‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
#![feature(core_intrinsics)]
66

77
use std::alloc::{Layout, alloc};
8-
use std::sync::atomic::{AtomicU8, Ordering};
8+
use std::intrinsics::{AtomicOrdering, atomic_cxchg, atomic_load, atomic_store};
99

1010
// Checks if memory initialization checks correctly fail when uninitialized memory is passed to
1111
// atomic intrinsics.
@@ -18,15 +18,15 @@ fn local_atomic_uninit() {
1818
unsafe {
1919
match kani::any() {
2020
0 => {
21-
std::intrinsics::atomic_store_relaxed(ptr, 1);
21+
atomic_store::<_, { AtomicOrdering::Relaxed }>(ptr, 1);
2222
}
2323
1 => {
24-
std::intrinsics::atomic_load::<_, { std::intrinsics::AtomicOrdering::Relaxed }>(
25-
ptr as *const u8,
26-
);
24+
atomic_load::<_, { AtomicOrdering::Relaxed }>(ptr as *const u8);
2725
}
2826
_ => {
29-
std::intrinsics::atomic_cxchg_relaxed_relaxed(ptr, 1, 1);
27+
atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Relaxed }>(
28+
ptr, 1, 1,
29+
);
3030
}
3131
};
3232
}

‎tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,7 @@
55
// expected result.
66

77
#![feature(core_intrinsics)]
8-
use std::intrinsics::{
9-
atomic_xadd_acqrel, atomic_xadd_acquire, atomic_xadd_relaxed, atomic_xadd_release,
10-
atomic_xadd_seqcst,
11-
};
8+
use std::intrinsics::{AtomicOrdering, atomic_xadd};
129

1310
#[kani::proof]
1411
fn main() {
@@ -28,11 +25,11 @@ fn main() {
2825
let c = 1 as u8;
2926

3027
unsafe {
31-
let x1 = atomic_xadd_seqcst(ptr_a1, b);
32-
let x2 = atomic_xadd_acquire(ptr_a2, b);
33-
let x3 = atomic_xadd_acqrel(ptr_a3, b);
34-
let x4 = atomic_xadd_release(ptr_a4, b);
35-
let x5 = atomic_xadd_relaxed(ptr_a5, b);
28+
let x1 = atomic_xadd::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
29+
let x2 = atomic_xadd::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
30+
let x3 = atomic_xadd::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
31+
let x4 = atomic_xadd::<_, { AtomicOrdering::Release }>(ptr_a4, b);
32+
let x5 = atomic_xadd::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
3633

3734
assert!(x1 == 0);
3835
assert!(x2 == 0);

‎tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,7 @@
55
// expected result.
66

77
#![feature(core_intrinsics)]
8-
use std::intrinsics::{
9-
atomic_and_acqrel, atomic_and_acquire, atomic_and_relaxed, atomic_and_release,
10-
atomic_and_seqcst,
11-
};
8+
use std::intrinsics::{AtomicOrdering, atomic_and};
129

1310
#[kani::proof]
1411
fn main() {
@@ -27,11 +24,11 @@ fn main() {
2724
let b = 0 as u8;
2825

2926
unsafe {
30-
let x1 = atomic_and_seqcst(ptr_a1, b);
31-
let x2 = atomic_and_acquire(ptr_a2, b);
32-
let x3 = atomic_and_acqrel(ptr_a3, b);
33-
let x4 = atomic_and_release(ptr_a4, b);
34-
let x5 = atomic_and_relaxed(ptr_a5, b);
27+
let x1 = atomic_and::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b);
28+
let x2 = atomic_and::<_, { AtomicOrdering::Acquire }>(ptr_a2, b);
29+
let x3 = atomic_and::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b);
30+
let x4 = atomic_and::<_, { AtomicOrdering::Release }>(ptr_a4, b);
31+
let x5 = atomic_and::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b);
3532

3633
assert!(x1 == 1);
3734
assert!(x2 == 1);

‎tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs‎

Lines changed: 89 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,7 @@
55
// return the expected result.
66

77
#![feature(core_intrinsics)]
8-
use std::intrinsics::{
9-
atomic_cxchg_acqrel_acquire, atomic_cxchg_acqrel_relaxed, atomic_cxchg_acqrel_seqcst,
10-
atomic_cxchg_acquire_acquire, atomic_cxchg_acquire_relaxed, atomic_cxchg_acquire_seqcst,
11-
atomic_cxchg_relaxed_acquire, atomic_cxchg_relaxed_relaxed, atomic_cxchg_relaxed_seqcst,
12-
atomic_cxchg_release_acquire, atomic_cxchg_release_relaxed, atomic_cxchg_release_seqcst,
13-
atomic_cxchg_seqcst_acquire, atomic_cxchg_seqcst_relaxed, atomic_cxchg_seqcst_seqcst,
14-
};
8+
use std::intrinsics::{AtomicOrdering, atomic_cxchg};
159

1610
#[kani::proof]
1711
fn main() {
@@ -52,21 +46,50 @@ fn main() {
5246
// Returns (val, ok) where
5347
// * val: the old value
5448
// * ok: bool indicating whether the operation was successful or not
55-
let x1 = atomic_cxchg_acqrel_acquire(ptr_a1, 0, 1);
56-
let x2 = atomic_cxchg_acqrel_relaxed(ptr_a2, 0, 1);
57-
let x3 = atomic_cxchg_acqrel_seqcst(ptr_a3, 0, 1);
58-
let x4 = atomic_cxchg_acquire_acquire(ptr_a4, 0, 1);
59-
let x5 = atomic_cxchg_acquire_relaxed(ptr_a5, 0, 1);
60-
let x6 = atomic_cxchg_acquire_seqcst(ptr_a6, 0, 1);
61-
let x7 = atomic_cxchg_relaxed_acquire(ptr_a7, 0, 1);
62-
let x8 = atomic_cxchg_relaxed_relaxed(ptr_a8, 0, 1);
63-
let x9 = atomic_cxchg_relaxed_seqcst(ptr_a9, 0, 1);
64-
let x10 = atomic_cxchg_release_acquire(ptr_a10, 0, 1);
65-
let x11 = atomic_cxchg_release_relaxed(ptr_a11, 0, 1);
66-
let x12 = atomic_cxchg_release_seqcst(ptr_a12, 0, 1);
67-
let x13 = atomic_cxchg_seqcst_acquire(ptr_a13, 0, 1);
68-
let x14 = atomic_cxchg_seqcst_relaxed(ptr_a14, 0, 1);
69-
let x15 = atomic_cxchg_seqcst_seqcst(ptr_a15, 0, 1);
49+
let x1 = atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Acquire }>(
50+
ptr_a1, 0, 1,
51+
);
52+
let x2 = atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Relaxed }>(
53+
ptr_a2, 0, 1,
54+
);
55+
let x3 =
56+
atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::SeqCst }>(ptr_a3, 0, 1);
57+
let x4 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Acquire }>(
58+
ptr_a4, 0, 1,
59+
);
60+
let x5 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Relaxed }>(
61+
ptr_a5, 0, 1,
62+
);
63+
let x6 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::SeqCst }>(
64+
ptr_a6, 0, 1,
65+
);
66+
let x7 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Acquire }>(
67+
ptr_a7, 0, 1,
68+
);
69+
let x8 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Relaxed }>(
70+
ptr_a8, 0, 1,
71+
);
72+
let x9 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::SeqCst }>(
73+
ptr_a9, 0, 1,
74+
);
75+
let x10 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::Acquire }>(
76+
ptr_a10, 0, 1,
77+
);
78+
let x11 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::Relaxed }>(
79+
ptr_a11, 0, 1,
80+
);
81+
let x12 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::SeqCst }>(
82+
ptr_a12, 0, 1,
83+
);
84+
let x13 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Acquire }>(
85+
ptr_a13, 0, 1,
86+
);
87+
let x14 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Relaxed }>(
88+
ptr_a14, 0, 1,
89+
);
90+
let x15 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::SeqCst }>(
91+
ptr_a15, 0, 1,
92+
);
7093

7194
assert!(x1 == (0, true));
7295
assert!(x2 == (0, true));
@@ -84,21 +107,50 @@ fn main() {
84107
assert!(x14 == (0, true));
85108
assert!(x15 == (0, true));
86109

87-
let y1 = atomic_cxchg_acqrel_acquire(ptr_a1, 1, 1);
88-
let y2 = atomic_cxchg_acqrel_relaxed(ptr_a2, 1, 1);
89-
let y3 = atomic_cxchg_acqrel_seqcst(ptr_a3, 1, 1);
90-
let y4 = atomic_cxchg_acquire_acquire(ptr_a4, 1, 1);
91-
let y5 = atomic_cxchg_acquire_relaxed(ptr_a5, 1, 1);
92-
let y6 = atomic_cxchg_acquire_seqcst(ptr_a6, 1, 1);
93-
let y7 = atomic_cxchg_relaxed_acquire(ptr_a7, 1, 1);
94-
let y8 = atomic_cxchg_relaxed_relaxed(ptr_a8, 1, 1);
95-
let y9 = atomic_cxchg_relaxed_seqcst(ptr_a9, 1, 1);
96-
let y10 = atomic_cxchg_release_acquire(ptr_a10, 1, 1);
97-
let y11 = atomic_cxchg_release_relaxed(ptr_a11, 1, 1);
98-
let y12 = atomic_cxchg_release_seqcst(ptr_a12, 1, 1);
99-
let y13 = atomic_cxchg_seqcst_acquire(ptr_a13, 1, 1);
100-
let y14 = atomic_cxchg_seqcst_relaxed(ptr_a14, 1, 1);
101-
let y15 = atomic_cxchg_seqcst_seqcst(ptr_a15, 1, 1);
110+
let y1 = atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Acquire }>(
111+
ptr_a1, 1, 1,
112+
);
113+
let y2 = atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Relaxed }>(
114+
ptr_a2, 1, 1,
115+
);
116+
let y3 =
117+
atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::SeqCst }>(ptr_a3, 1, 1);
118+
let y4 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Acquire }>(
119+
ptr_a4, 1, 1,
120+
);
121+
let y5 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Relaxed }>(
122+
ptr_a5, 1, 1,
123+
);
124+
let y6 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::SeqCst }>(
125+
ptr_a6, 1, 1,
126+
);
127+
let y7 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Acquire }>(
128+
ptr_a7, 1, 1,
129+
);
130+
let y8 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Relaxed }>(
131+
ptr_a8, 1, 1,
132+
);
133+
let y9 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::SeqCst }>(
134+
ptr_a9, 1, 1,
135+
);
136+
let y10 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::Acquire }>(
137+
ptr_a10, 1, 1,
138+
);
139+
let y11 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::Relaxed }>(
140+
ptr_a11, 1, 1,
141+
);
142+
let y12 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::SeqCst }>(
143+
ptr_a12, 1, 1,
144+
);
145+
let y13 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Acquire }>(
146+
ptr_a13, 1, 1,
147+
);
148+
let y14 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Relaxed }>(
149+
ptr_a14, 1, 1,
150+
);
151+
let y15 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::SeqCst }>(
152+
ptr_a15, 1, 1,
153+
);
102154

103155
assert!(y1 == (1, true));
104156
assert!(y2 == (1, true));

0 commit comments

Comments
 (0)