From 4b2f05f62cf62c6e34ae604cbe09aa513f42c017 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 12 Jun 2025 18:29:20 -0400 Subject: [PATCH 1/8] update to 6/4 --- kani-compiler/src/kani_middle/resolve.rs | 6 ++++-- rust-toolchain.toml | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 060f68ac88f7..865a96d408e4 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -434,7 +434,9 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> R let item = tcx.hir_item(item_id); if item.kind.ident().is_some_and(|ident| ident.as_str() == name) { match item.kind { - ItemKind::Use(use_path, UseKind::Single(_)) => use_path.res[0].opt_def_id(), + ItemKind::Use(use_path, UseKind::Single(_)) => { + use_path.res.present_items().filter_map(|res| res.opt_def_id()).next() + } ItemKind::ExternCrate(orig_name, _) => resolve_external( tcx, orig_name.as_ref().map(|sym| sym.as_str()).unwrap_or(name), @@ -445,7 +447,7 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> R if let ItemKind::Use(use_path, UseKind::Glob) = item.kind { // Do not immediately try to resolve the path using this glob, // since paths resolved via non-globs take precedence. - glob_imports.push(use_path.res[0]); + glob_imports.extend(use_path.res.present_items()); } None } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 04b2342ca7c0..2c13f7d97213 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-03" +channel = "nightly-2025-06-04" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 241f2edc281a41eee369f0e4137e458425fc08fd Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 12 Jun 2025 18:53:46 -0400 Subject: [PATCH 2/8] update to 6/5 --- rust-toolchain.toml | 2 +- .../arbitrary/ptrs/pointer_generator_error.expected | 7 +++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 2c13f7d97213..c235b4d6286e 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-04" +channel = "nightly-2025-06-05" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/arbitrary/ptrs/pointer_generator_error.expected b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected index 06496f4313d7..836af138165c 100644 --- a/tests/expected/arbitrary/ptrs/pointer_generator_error.expected +++ b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected @@ -1,6 +1,9 @@ -error[E0080]: evaluation of `kani::PointerGenerator::<0>::VALID` failed\ +error[E0080]: evaluation panicked: PointerGenerator requires at least one byte.\ -evaluation panicked: PointerGenerator requires at least one byte.\ +|\ +| kani_core::kani_lib!(kani);\ +| ^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation of `kani::PointerGenerator::<0>::VALID` failed here\ +|\ note: the above error was encountered while instantiating `fn kani::PointerGenerator::<0>::new`\ pointer_generator_error.rs\ From 3a06fe9c6640f997c79cf828083f93b00f937d47 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 12 Jun 2025 18:54:42 -0400 Subject: [PATCH 3/8] update to 6/6 --- cprover_bindings/src/irep/irep_id.rs | 2 +- kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 4 ++-- kani-compiler/src/kani_middle/provide.rs | 4 ++-- library/kani_macros/src/sysroot/contracts/helpers.rs | 2 +- rust-toolchain.toml | 2 +- 6 files changed, 8 insertions(+), 8 deletions(-) diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index 4a975e3df40c..a6ba0f86e3ef 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/cprover_bindings/src/irep/irep_id.rs @@ -887,7 +887,7 @@ impl ToString for IrepId { } impl IrepId { - pub fn to_string_cow(&self) -> Cow { + pub fn to_string_cow(&self) -> Cow<'_, str> { match self.to_owned_string() { Some(owned) => Cow::Owned(owned), None => Cow::Borrowed(self.to_static_string()), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 243262a875b5..05995ca4bb71 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -519,7 +519,7 @@ impl GotocCtx<'_> { .index_by_increasing_offset() .map(|idx| { let field_ty = layout.field(self, idx).ty; - if idx == *discriminant_field { + if idx == (*discriminant_field).as_usize() { Expr::int_constant(0, self.codegen_ty(field_ty)) } else { self.codegen_operand_stable(&operands[idx]) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 56bc2b728244..45455251b8cd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -914,7 +914,7 @@ impl<'tcx> GotocCtx<'tcx> { pretty_name, type_and_layout, "DirectFields".into(), - Some(*discriminant_field), + Some((*discriminant_field).as_usize()), ), }; let mut fields = vec![direct_fields]; @@ -1277,7 +1277,7 @@ impl<'tcx> GotocCtx<'tcx> { // Contrary to coroutines, currently enums have only one field (the discriminant), the rest are in the variants: assert!(layout.fields.count() <= 1); // Contrary to coroutines, the discriminant is the first (and only) field for enums: - assert_eq!(*tag_field, 0); + assert_eq!((*tag_field).as_usize(), 0); match tag_encoding { TagEncoding::Direct => { self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, name| { diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index 91b830a2349b..52c3a789e8bf 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -28,7 +28,7 @@ fn should_override(args: &Arguments) -> bool { /// Returns the optimized code for the external function associated with `def_id` by /// running rustc's optimization passes followed by Kani-specific passes. -fn run_mir_passes_extern(tcx: TyCtxt, def_id: DefId) -> &Body { +fn run_mir_passes_extern(tcx: TyCtxt<'_>, def_id: DefId) -> &Body<'_> { tracing::debug!(?def_id, "run_mir_passes_extern"); let body = (rustc_interface::DEFAULT_QUERY_PROVIDERS.extern_queries.optimized_mir)(tcx, def_id); run_kani_mir_passes(tcx, def_id, body) @@ -36,7 +36,7 @@ fn run_mir_passes_extern(tcx: TyCtxt, def_id: DefId) -> &Body { /// Returns the optimized code for the local function associated with `def_id` by /// running rustc's optimization passes followed by Kani-specific passes. -fn run_mir_passes(tcx: TyCtxt, def_id: LocalDefId) -> &Body { +fn run_mir_passes(tcx: TyCtxt<'_>, def_id: LocalDefId) -> &Body<'_> { tracing::debug!(?def_id, "run_mir_passes"); let body = (rustc_interface::DEFAULT_QUERY_PROVIDERS.optimized_mir)(tcx, def_id); run_kani_mir_passes(tcx, def_id.to_def_id(), body) diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index c79a5520ceb3..e4182041e18b 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -10,7 +10,7 @@ use syn::spanned::Spanned; use syn::{Attribute, Expr, ExprBlock, Local, LocalInit, PatIdent, Stmt, parse_quote}; /// If an explicit return type was provided it is returned, otherwise `()`. -pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { +pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow<'_, syn::Type> { match return_type { syn::ReturnType::Default => Cow::Owned(syn::Type::Tuple(syn::TypeTuple { paren_token: syn::token::Paren::default(), diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c235b4d6286e..e800ac6b9d34 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-05" +channel = "nightly-2025-06-06" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From e5f548cc2d13c70ae8a78bc407b71fe805fe9a52 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 12 Jun 2025 19:01:45 -0400 Subject: [PATCH 4/8] update to 6/7 --- kani-compiler/src/kani_middle/coercion.rs | 3 ++- rust-toolchain.toml | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 5fe1e50948a5..cc67cc886665 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -19,6 +19,7 @@ use rustc_middle::ty::TraitRef; use rustc_middle::ty::adjustment::CustomCoerceUnsized; use rustc_middle::ty::{PseudoCanonicalInput, Ty, TyCtxt, TypingEnv}; use rustc_smir::rustc_internal; +use rustc_span::DUMMY_SP; use stable_mir::Symbol; use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind}; use tracing::trace; @@ -245,7 +246,7 @@ fn custom_coerce_unsize_info<'tcx>( source_ty: Ty<'tcx>, target_ty: Ty<'tcx>, ) -> CustomCoerceUnsized { - let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None); + let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, DUMMY_SP); let trait_ref = TraitRef::new(tcx, def_id, tcx.mk_args_trait(source_ty, [target_ty.into()])); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index e800ac6b9d34..02164adcad61 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-06" +channel = "nightly-2025-06-07" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From e3a7bec488e1b719b034af63b15d66b63d6ddd0e Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 12 Jun 2025 19:09:33 -0400 Subject: [PATCH 5/8] update to 6/9 --- kani-compiler/src/intrinsics.rs | 32 ++--- rust-toolchain.toml | 2 +- tests/expected/uninit/atomic/atomic.rs | 12 +- .../Atomic/Unstable/AtomicAdd/main.rs | 15 +- .../Atomic/Unstable/AtomicAnd/main.rs | 15 +- .../Atomic/Unstable/AtomicCxchg/main.rs | 126 ++++++++++++----- .../Atomic/Unstable/AtomicCxchgWeak/main.rs | 131 ++++++++++++------ .../Atomic/Unstable/AtomicFence/main.rs | 12 +- .../Atomic/Unstable/AtomicMax/main.rs | 15 +- .../Atomic/Unstable/AtomicMin/main.rs | 15 +- .../Atomic/Unstable/AtomicNand/main.rs | 25 ++-- .../Atomic/Unstable/AtomicOr/main.rs | 14 +- .../Unstable/AtomicSingleThreadFence/main.rs | 13 +- .../Atomic/Unstable/AtomicStore/main.rs | 8 +- .../Atomic/Unstable/AtomicSub/main.rs | 15 +- .../Atomic/Unstable/AtomicUmax/main.rs | 15 +- .../Atomic/Unstable/AtomicUmin/main.rs | 15 +- .../Atomic/Unstable/AtomicXchg/main.rs | 25 ++-- .../Atomic/Unstable/AtomicXor/main.rs | 15 +- 19 files changed, 293 insertions(+), 227 deletions(-) diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index 94b9462612b1..862438f3cfc8 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -471,55 +471,55 @@ impl Intrinsic { fn try_match_atomic(intrinsic_instance: &Instance) -> Option { let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap(); let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder(); - if let Some(suffix) = intrinsic_str.strip_prefix("atomic_and_") { + if let Some(suffix) = intrinsic_str.strip_prefix("atomic_and") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicAnd(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchgweak_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchgweak") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_)); Some(Intrinsic::AtomicCxchgWeak(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchg_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchg") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_)); Some(Intrinsic::AtomicCxchg(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_fence_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_fence") { assert_sig_matches!(sig, => RigidTy::Tuple(_)); Some(Intrinsic::AtomicFence(suffix.into())) } else if intrinsic_str == "atomic_load" { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _); Some(Intrinsic::AtomicLoad) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_max_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_max") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicMax(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_min_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_min") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicMin(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_nand_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_nand") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicNand(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_or_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_or") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicOr(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_singlethreadfence_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_singlethreadfence") { assert_sig_matches!(sig, => RigidTy::Tuple(_)); Some(Intrinsic::AtomicSingleThreadFence(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_store_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_store") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_)); Some(Intrinsic::AtomicStore(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umax_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umax") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicUmax(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umin_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umin") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicUmin(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xadd_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xadd") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicXadd(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xchg_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xchg") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicXchg(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xor_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xor") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicXor(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xsub_") { + } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xsub") { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); Some(Intrinsic::AtomicXsub(suffix.into())) } else { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 02164adcad61..e6ffe0e9051f 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-07" +channel = "nightly-2025-06-09" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs index 6bc98252dc45..a5bb0cbe9561 100644 --- a/tests/expected/uninit/atomic/atomic.rs +++ b/tests/expected/uninit/atomic/atomic.rs @@ -5,7 +5,7 @@ #![feature(core_intrinsics)] use std::alloc::{Layout, alloc}; -use std::sync::atomic::{AtomicU8, Ordering}; +use std::intrinsics::{AtomicOrdering, atomic_cxchg, atomic_load, atomic_store}; // Checks if memory initialization checks correctly fail when uninitialized memory is passed to // atomic intrinsics. @@ -18,15 +18,15 @@ fn local_atomic_uninit() { unsafe { match kani::any() { 0 => { - std::intrinsics::atomic_store_relaxed(ptr, 1); + atomic_store::<_, { AtomicOrdering::Relaxed }>(ptr, 1); } 1 => { - std::intrinsics::atomic_load::<_, { std::intrinsics::AtomicOrdering::Relaxed }>( - ptr as *const u8, - ); + atomic_load::<_, { AtomicOrdering::Relaxed }>(ptr as *const u8); } _ => { - std::intrinsics::atomic_cxchg_relaxed_relaxed(ptr, 1, 1); + atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Relaxed }>( + ptr, 1, 1, + ); } }; } diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs index 2f85653b0631..5789d9d62c0c 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs @@ -5,10 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_xadd_acqrel, atomic_xadd_acquire, atomic_xadd_relaxed, atomic_xadd_release, - atomic_xadd_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_xadd}; #[kani::proof] fn main() { @@ -28,11 +25,11 @@ fn main() { let c = 1 as u8; unsafe { - let x1 = atomic_xadd_seqcst(ptr_a1, b); - let x2 = atomic_xadd_acquire(ptr_a2, b); - let x3 = atomic_xadd_acqrel(ptr_a3, b); - let x4 = atomic_xadd_release(ptr_a4, b); - let x5 = atomic_xadd_relaxed(ptr_a5, b); + let x1 = atomic_xadd::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_xadd::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_xadd::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_xadd::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_xadd::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == 0); assert!(x2 == 0); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs index 6be83c2eaa2b..8eccf86bce49 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs @@ -5,10 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_and_acqrel, atomic_and_acquire, atomic_and_relaxed, atomic_and_release, - atomic_and_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_and}; #[kani::proof] fn main() { @@ -27,11 +24,11 @@ fn main() { let b = 0 as u8; unsafe { - let x1 = atomic_and_seqcst(ptr_a1, b); - let x2 = atomic_and_acquire(ptr_a2, b); - let x3 = atomic_and_acqrel(ptr_a3, b); - let x4 = atomic_and_release(ptr_a4, b); - let x5 = atomic_and_relaxed(ptr_a5, b); + let x1 = atomic_and::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_and::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_and::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_and::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_and::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == 1); assert!(x2 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs index 996741467cfa..57ccdb841c92 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs @@ -5,13 +5,7 @@ // return the expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_cxchg_acqrel_acquire, atomic_cxchg_acqrel_relaxed, atomic_cxchg_acqrel_seqcst, - atomic_cxchg_acquire_acquire, atomic_cxchg_acquire_relaxed, atomic_cxchg_acquire_seqcst, - atomic_cxchg_relaxed_acquire, atomic_cxchg_relaxed_relaxed, atomic_cxchg_relaxed_seqcst, - atomic_cxchg_release_acquire, atomic_cxchg_release_relaxed, atomic_cxchg_release_seqcst, - atomic_cxchg_seqcst_acquire, atomic_cxchg_seqcst_relaxed, atomic_cxchg_seqcst_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_cxchg}; #[kani::proof] fn main() { @@ -52,21 +46,50 @@ fn main() { // Returns (val, ok) where // * val: the old value // * ok: bool indicating whether the operation was successful or not - let x1 = atomic_cxchg_acqrel_acquire(ptr_a1, 0, 1); - let x2 = atomic_cxchg_acqrel_relaxed(ptr_a2, 0, 1); - let x3 = atomic_cxchg_acqrel_seqcst(ptr_a3, 0, 1); - let x4 = atomic_cxchg_acquire_acquire(ptr_a4, 0, 1); - let x5 = atomic_cxchg_acquire_relaxed(ptr_a5, 0, 1); - let x6 = atomic_cxchg_acquire_seqcst(ptr_a6, 0, 1); - let x7 = atomic_cxchg_relaxed_acquire(ptr_a7, 0, 1); - let x8 = atomic_cxchg_relaxed_relaxed(ptr_a8, 0, 1); - let x9 = atomic_cxchg_relaxed_seqcst(ptr_a9, 0, 1); - let x10 = atomic_cxchg_release_acquire(ptr_a10, 0, 1); - let x11 = atomic_cxchg_release_relaxed(ptr_a11, 0, 1); - let x12 = atomic_cxchg_release_seqcst(ptr_a12, 0, 1); - let x13 = atomic_cxchg_seqcst_acquire(ptr_a13, 0, 1); - let x14 = atomic_cxchg_seqcst_relaxed(ptr_a14, 0, 1); - let x15 = atomic_cxchg_seqcst_seqcst(ptr_a15, 0, 1); + let x1 = atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Acquire }>( + ptr_a1, 0, 1, + ); + let x2 = atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Relaxed }>( + ptr_a2, 0, 1, + ); + let x3 = + atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::SeqCst }>(ptr_a3, 0, 1); + let x4 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Acquire }>( + ptr_a4, 0, 1, + ); + let x5 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Relaxed }>( + ptr_a5, 0, 1, + ); + let x6 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::SeqCst }>( + ptr_a6, 0, 1, + ); + let x7 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Acquire }>( + ptr_a7, 0, 1, + ); + let x8 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Relaxed }>( + ptr_a8, 0, 1, + ); + let x9 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::SeqCst }>( + ptr_a9, 0, 1, + ); + let x10 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::Acquire }>( + ptr_a10, 0, 1, + ); + let x11 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::Relaxed }>( + ptr_a11, 0, 1, + ); + let x12 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::SeqCst }>( + ptr_a12, 0, 1, + ); + let x13 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Acquire }>( + ptr_a13, 0, 1, + ); + let x14 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Relaxed }>( + ptr_a14, 0, 1, + ); + let x15 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::SeqCst }>( + ptr_a15, 0, 1, + ); assert!(x1 == (0, true)); assert!(x2 == (0, true)); @@ -84,21 +107,50 @@ fn main() { assert!(x14 == (0, true)); assert!(x15 == (0, true)); - let y1 = atomic_cxchg_acqrel_acquire(ptr_a1, 1, 1); - let y2 = atomic_cxchg_acqrel_relaxed(ptr_a2, 1, 1); - let y3 = atomic_cxchg_acqrel_seqcst(ptr_a3, 1, 1); - let y4 = atomic_cxchg_acquire_acquire(ptr_a4, 1, 1); - let y5 = atomic_cxchg_acquire_relaxed(ptr_a5, 1, 1); - let y6 = atomic_cxchg_acquire_seqcst(ptr_a6, 1, 1); - let y7 = atomic_cxchg_relaxed_acquire(ptr_a7, 1, 1); - let y8 = atomic_cxchg_relaxed_relaxed(ptr_a8, 1, 1); - let y9 = atomic_cxchg_relaxed_seqcst(ptr_a9, 1, 1); - let y10 = atomic_cxchg_release_acquire(ptr_a10, 1, 1); - let y11 = atomic_cxchg_release_relaxed(ptr_a11, 1, 1); - let y12 = atomic_cxchg_release_seqcst(ptr_a12, 1, 1); - let y13 = atomic_cxchg_seqcst_acquire(ptr_a13, 1, 1); - let y14 = atomic_cxchg_seqcst_relaxed(ptr_a14, 1, 1); - let y15 = atomic_cxchg_seqcst_seqcst(ptr_a15, 1, 1); + let y1 = atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Acquire }>( + ptr_a1, 1, 1, + ); + let y2 = atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Relaxed }>( + ptr_a2, 1, 1, + ); + let y3 = + atomic_cxchg::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::SeqCst }>(ptr_a3, 1, 1); + let y4 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Acquire }>( + ptr_a4, 1, 1, + ); + let y5 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Relaxed }>( + ptr_a5, 1, 1, + ); + let y6 = atomic_cxchg::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::SeqCst }>( + ptr_a6, 1, 1, + ); + let y7 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Acquire }>( + ptr_a7, 1, 1, + ); + let y8 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Relaxed }>( + ptr_a8, 1, 1, + ); + let y9 = atomic_cxchg::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::SeqCst }>( + ptr_a9, 1, 1, + ); + let y10 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::Acquire }>( + ptr_a10, 1, 1, + ); + let y11 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::Relaxed }>( + ptr_a11, 1, 1, + ); + let y12 = atomic_cxchg::<_, { AtomicOrdering::Release }, { AtomicOrdering::SeqCst }>( + ptr_a12, 1, 1, + ); + let y13 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Acquire }>( + ptr_a13, 1, 1, + ); + let y14 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Relaxed }>( + ptr_a14, 1, 1, + ); + let y15 = atomic_cxchg::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::SeqCst }>( + ptr_a15, 1, 1, + ); assert!(y1 == (1, true)); assert!(y2 == (1, true)); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs index 6beb66dec5c7..b30cd8aa079b 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs @@ -5,16 +5,7 @@ // version) return the expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_cxchgweak_acqrel_acquire, atomic_cxchgweak_acqrel_relaxed, - atomic_cxchgweak_acqrel_seqcst, atomic_cxchgweak_acquire_acquire, - atomic_cxchgweak_acquire_relaxed, atomic_cxchgweak_acquire_seqcst, - atomic_cxchgweak_relaxed_acquire, atomic_cxchgweak_relaxed_relaxed, - atomic_cxchgweak_relaxed_seqcst, atomic_cxchgweak_release_acquire, - atomic_cxchgweak_release_relaxed, atomic_cxchgweak_release_seqcst, - atomic_cxchgweak_seqcst_acquire, atomic_cxchgweak_seqcst_relaxed, - atomic_cxchgweak_seqcst_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_cxchgweak}; #[kani::proof] fn main() { @@ -55,21 +46,51 @@ fn main() { // Returns (val, ok) where // * val: the old value // * ok: bool indicating whether the operation was successful or not - let x1 = atomic_cxchgweak_acqrel_acquire(ptr_a1, 0, 1); - let x2 = atomic_cxchgweak_acqrel_relaxed(ptr_a2, 0, 1); - let x3 = atomic_cxchgweak_acqrel_seqcst(ptr_a3, 0, 1); - let x4 = atomic_cxchgweak_acquire_acquire(ptr_a4, 0, 1); - let x5 = atomic_cxchgweak_acquire_relaxed(ptr_a5, 0, 1); - let x6 = atomic_cxchgweak_acquire_seqcst(ptr_a6, 0, 1); - let x7 = atomic_cxchgweak_relaxed_acquire(ptr_a7, 0, 1); - let x8 = atomic_cxchgweak_relaxed_relaxed(ptr_a8, 0, 1); - let x9 = atomic_cxchgweak_relaxed_seqcst(ptr_a9, 0, 1); - let x10 = atomic_cxchgweak_release_acquire(ptr_a10, 0, 1); - let x11 = atomic_cxchgweak_release_relaxed(ptr_a11, 0, 1); - let x12 = atomic_cxchgweak_release_seqcst(ptr_a12, 0, 1); - let x13 = atomic_cxchgweak_seqcst_acquire(ptr_a13, 0, 1); - let x14 = atomic_cxchgweak_seqcst_relaxed(ptr_a14, 0, 1); - let x15 = atomic_cxchgweak_seqcst_seqcst(ptr_a15, 0, 1); + let x1 = atomic_cxchgweak::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Acquire }>( + ptr_a1, 0, 1, + ); + let x2 = atomic_cxchgweak::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Relaxed }>( + ptr_a2, 0, 1, + ); + let x3 = atomic_cxchgweak::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::SeqCst }>( + ptr_a3, 0, 1, + ); + let x4 = atomic_cxchgweak::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Acquire }>( + ptr_a4, 0, 1, + ); + let x5 = atomic_cxchgweak::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Relaxed }>( + ptr_a5, 0, 1, + ); + let x6 = atomic_cxchgweak::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::SeqCst }>( + ptr_a6, 0, 1, + ); + let x7 = atomic_cxchgweak::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Acquire }>( + ptr_a7, 0, 1, + ); + let x8 = atomic_cxchgweak::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Relaxed }>( + ptr_a8, 0, 1, + ); + let x9 = atomic_cxchgweak::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::SeqCst }>( + ptr_a9, 0, 1, + ); + let x10 = atomic_cxchgweak::<_, { AtomicOrdering::Release }, { AtomicOrdering::Acquire }>( + ptr_a10, 0, 1, + ); + let x11 = atomic_cxchgweak::<_, { AtomicOrdering::Release }, { AtomicOrdering::Relaxed }>( + ptr_a11, 0, 1, + ); + let x12 = atomic_cxchgweak::<_, { AtomicOrdering::Release }, { AtomicOrdering::SeqCst }>( + ptr_a12, 0, 1, + ); + let x13 = atomic_cxchgweak::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Acquire }>( + ptr_a13, 0, 1, + ); + let x14 = atomic_cxchgweak::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Relaxed }>( + ptr_a14, 0, 1, + ); + let x15 = atomic_cxchgweak::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::SeqCst }>( + ptr_a15, 0, 1, + ); assert!(x1 == (0, true)); assert!(x2 == (0, true)); @@ -87,21 +108,51 @@ fn main() { assert!(x14 == (0, true)); assert!(x15 == (0, true)); - let y1 = atomic_cxchgweak_acqrel_acquire(ptr_a1, 1, 1); - let y2 = atomic_cxchgweak_acqrel_relaxed(ptr_a2, 1, 1); - let y3 = atomic_cxchgweak_acqrel_seqcst(ptr_a3, 1, 1); - let y4 = atomic_cxchgweak_acquire_acquire(ptr_a4, 1, 1); - let y5 = atomic_cxchgweak_acquire_relaxed(ptr_a5, 1, 1); - let y6 = atomic_cxchgweak_acquire_seqcst(ptr_a6, 1, 1); - let y7 = atomic_cxchgweak_relaxed_acquire(ptr_a7, 1, 1); - let y8 = atomic_cxchgweak_relaxed_relaxed(ptr_a8, 1, 1); - let y9 = atomic_cxchgweak_relaxed_seqcst(ptr_a9, 1, 1); - let y10 = atomic_cxchgweak_release_acquire(ptr_a10, 1, 1); - let y11 = atomic_cxchgweak_release_relaxed(ptr_a11, 1, 1); - let y12 = atomic_cxchgweak_release_seqcst(ptr_a12, 1, 1); - let y13 = atomic_cxchgweak_seqcst_acquire(ptr_a13, 1, 1); - let y14 = atomic_cxchgweak_seqcst_relaxed(ptr_a14, 1, 1); - let y15 = atomic_cxchgweak_seqcst_seqcst(ptr_a15, 1, 1); + let y1 = atomic_cxchgweak::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Acquire }>( + ptr_a1, 1, 1, + ); + let y2 = atomic_cxchgweak::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::Relaxed }>( + ptr_a2, 1, 1, + ); + let y3 = atomic_cxchgweak::<_, { AtomicOrdering::AcqRel }, { AtomicOrdering::SeqCst }>( + ptr_a3, 1, 1, + ); + let y4 = atomic_cxchgweak::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Acquire }>( + ptr_a4, 1, 1, + ); + let y5 = atomic_cxchgweak::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::Relaxed }>( + ptr_a5, 1, 1, + ); + let y6 = atomic_cxchgweak::<_, { AtomicOrdering::Acquire }, { AtomicOrdering::SeqCst }>( + ptr_a6, 1, 1, + ); + let y7 = atomic_cxchgweak::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Acquire }>( + ptr_a7, 1, 1, + ); + let y8 = atomic_cxchgweak::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::Relaxed }>( + ptr_a8, 1, 1, + ); + let y9 = atomic_cxchgweak::<_, { AtomicOrdering::Relaxed }, { AtomicOrdering::SeqCst }>( + ptr_a9, 1, 1, + ); + let y10 = atomic_cxchgweak::<_, { AtomicOrdering::Release }, { AtomicOrdering::Acquire }>( + ptr_a10, 1, 1, + ); + let y11 = atomic_cxchgweak::<_, { AtomicOrdering::Release }, { AtomicOrdering::Relaxed }>( + ptr_a11, 1, 1, + ); + let y12 = atomic_cxchgweak::<_, { AtomicOrdering::Release }, { AtomicOrdering::SeqCst }>( + ptr_a12, 1, 1, + ); + let y13 = atomic_cxchgweak::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Acquire }>( + ptr_a13, 1, 1, + ); + let y14 = atomic_cxchgweak::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::Relaxed }>( + ptr_a14, 1, 1, + ); + let y15 = atomic_cxchgweak::<_, { AtomicOrdering::SeqCst }, { AtomicOrdering::SeqCst }>( + ptr_a15, 1, 1, + ); assert!(y1 == (1, true)); assert!(y2 == (1, true)); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicFence/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicFence/main.rs index 44cddd82e7dc..b27c2f02994b 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicFence/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicFence/main.rs @@ -5,16 +5,14 @@ // processed. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_fence_acqrel, atomic_fence_acquire, atomic_fence_release, atomic_fence_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_fence}; #[kani::proof] fn main() { unsafe { - atomic_fence_seqcst(); - atomic_fence_acquire(); - atomic_fence_acqrel(); - atomic_fence_release(); + atomic_fence::<{ AtomicOrdering::SeqCst }>(); + atomic_fence::<{ AtomicOrdering::Acquire }>(); + atomic_fence::<{ AtomicOrdering::AcqRel }>(); + atomic_fence::<{ AtomicOrdering::Release }>(); } } diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs index 9d5d850fe1c0..14bdcaac7f6c 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs @@ -5,10 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_max_acqrel, atomic_max_acquire, atomic_max_relaxed, atomic_max_release, - atomic_max_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_max}; #[kani::proof] fn main() { @@ -27,11 +24,11 @@ fn main() { let b = 1 as u8; unsafe { - let x1 = atomic_max_seqcst(ptr_a1, b); - let x2 = atomic_max_acquire(ptr_a2, b); - let x3 = atomic_max_acqrel(ptr_a3, b); - let x4 = atomic_max_release(ptr_a4, b); - let x5 = atomic_max_relaxed(ptr_a5, b); + let x1 = atomic_max::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_max::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_max::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_max::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_max::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == 0); assert!(x2 == 0); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs index ea9caf5971de..64238ace2819 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs @@ -5,10 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_min_acqrel, atomic_min_acquire, atomic_min_relaxed, atomic_min_release, - atomic_min_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_min}; #[kani::proof] fn main() { @@ -27,11 +24,11 @@ fn main() { let b = 0 as u8; unsafe { - let x1 = atomic_min_seqcst(ptr_a1, b); - let x2 = atomic_min_acquire(ptr_a2, b); - let x3 = atomic_min_acqrel(ptr_a3, b); - let x4 = atomic_min_release(ptr_a4, b); - let x5 = atomic_min_relaxed(ptr_a5, b); + let x1 = atomic_min::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_min::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_min::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_min::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_min::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == 1); assert!(x2 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs index c058dadfd0a1..4cae3c56988c 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs @@ -5,10 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_nand_acqrel, atomic_nand_acquire, atomic_nand_relaxed, atomic_nand_release, - atomic_nand_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_nand}; #[kani::proof] fn main() { @@ -27,11 +24,11 @@ fn main() { let b = u8::MAX as u8; unsafe { - let x1 = atomic_nand_seqcst(ptr_a1, b); - let x2 = atomic_nand_acquire(ptr_a2, b); - let x3 = atomic_nand_acqrel(ptr_a3, b); - let x4 = atomic_nand_release(ptr_a4, b); - let x5 = atomic_nand_relaxed(ptr_a5, b); + let x1 = atomic_nand::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_nand::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_nand::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_nand::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_nand::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == 0); assert!(x2 == 0); @@ -45,11 +42,11 @@ fn main() { assert!(*ptr_a4 == b); assert!(*ptr_a5 == b); - let x1 = atomic_nand_seqcst(ptr_a1, b); - let x2 = atomic_nand_acquire(ptr_a2, b); - let x3 = atomic_nand_acqrel(ptr_a3, b); - let x4 = atomic_nand_release(ptr_a4, b); - let x5 = atomic_nand_relaxed(ptr_a5, b); + let x1 = atomic_nand::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_nand::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_nand::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_nand::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_nand::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == b); assert!(x2 == b); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs index 9eba4396b560..aca7f25940b3 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs @@ -5,9 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_or_acqrel, atomic_or_acquire, atomic_or_relaxed, atomic_or_release, atomic_or_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_or}; #[kani::proof] fn main() { @@ -27,11 +25,11 @@ fn main() { let c = 1 as u8; unsafe { - let x1 = atomic_or_seqcst(ptr_a1, b); - let x2 = atomic_or_acquire(ptr_a2, b); - let x3 = atomic_or_acqrel(ptr_a3, b); - let x4 = atomic_or_release(ptr_a4, b); - let x5 = atomic_or_relaxed(ptr_a5, b); + let x1 = atomic_or::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_or::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_or::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_or::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_or::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == 1); assert!(x2 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs index 1b5b7df8bd34..e388ada3affa 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs @@ -5,17 +5,14 @@ // can be processed. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_singlethreadfence_acqrel, atomic_singlethreadfence_acquire, - atomic_singlethreadfence_release, atomic_singlethreadfence_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_singlethreadfence}; #[kani::proof] fn main() { unsafe { - atomic_singlethreadfence_seqcst(); - atomic_singlethreadfence_acquire(); - atomic_singlethreadfence_acqrel(); - atomic_singlethreadfence_release(); + atomic_singlethreadfence::<{ AtomicOrdering::SeqCst }>(); + atomic_singlethreadfence::<{ AtomicOrdering::Acquire }>(); + atomic_singlethreadfence::<{ AtomicOrdering::AcqRel }>(); + atomic_singlethreadfence::<{ AtomicOrdering::Release }>(); } } diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs index fd73c1c863eb..8581c6b9698a 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs @@ -5,7 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{atomic_store_relaxed, atomic_store_release, atomic_store_seqcst}; +use std::intrinsics::{AtomicOrdering, atomic_store}; #[kani::proof] fn main() { @@ -18,9 +18,9 @@ fn main() { let ptr_a3: *mut u8 = &mut a3; unsafe { - atomic_store_seqcst(ptr_a1, 0); - atomic_store_release(ptr_a2, 0); - atomic_store_relaxed(ptr_a3, 0); + atomic_store::<_, { AtomicOrdering::SeqCst }>(ptr_a1, 0); + atomic_store::<_, { AtomicOrdering::Release }>(ptr_a2, 0); + atomic_store::<_, { AtomicOrdering::Relaxed }>(ptr_a3, 0); assert!(*ptr_a1 == 0); assert!(*ptr_a2 == 0); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs index 3f205068948c..e57a3a12fe15 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs @@ -5,10 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_xsub_acqrel, atomic_xsub_acquire, atomic_xsub_relaxed, atomic_xsub_release, - atomic_xsub_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_xsub}; #[kani::proof] fn main() { @@ -28,11 +25,11 @@ fn main() { let c = 0 as u8; unsafe { - let x1 = atomic_xsub_seqcst(ptr_a1, b); - let x2 = atomic_xsub_acquire(ptr_a2, b); - let x3 = atomic_xsub_acqrel(ptr_a3, b); - let x4 = atomic_xsub_release(ptr_a4, b); - let x5 = atomic_xsub_relaxed(ptr_a5, b); + let x1 = atomic_xsub::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_xsub::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_xsub::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_xsub::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_xsub::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == 1); assert!(x2 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs index ee05691da839..1973125180f0 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs @@ -5,10 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_umax_acqrel, atomic_umax_acquire, atomic_umax_relaxed, atomic_umax_release, - atomic_umax_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_umax}; #[kani::proof] fn main() { @@ -27,11 +24,11 @@ fn main() { let b = 1 as u8; unsafe { - let x1 = atomic_umax_seqcst(ptr_a1, b); - let x2 = atomic_umax_acquire(ptr_a2, b); - let x3 = atomic_umax_acqrel(ptr_a3, b); - let x4 = atomic_umax_release(ptr_a4, b); - let x5 = atomic_umax_relaxed(ptr_a5, b); + let x1 = atomic_umax::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_umax::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_umax::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_umax::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_umax::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == 0); assert!(x2 == 0); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs index 69aea2493c85..9a9d9f81fc58 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs @@ -5,10 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_umin_acqrel, atomic_umin_acquire, atomic_umin_relaxed, atomic_umin_release, - atomic_umin_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_umin}; #[kani::proof] fn main() { @@ -27,11 +24,11 @@ fn main() { let b = 0 as u8; unsafe { - let x1 = atomic_umin_seqcst(ptr_a1, b); - let x2 = atomic_umin_acquire(ptr_a2, b); - let x3 = atomic_umin_acqrel(ptr_a3, b); - let x4 = atomic_umin_release(ptr_a4, b); - let x5 = atomic_umin_relaxed(ptr_a5, b); + let x1 = atomic_umin::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_umin::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_umin::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_umin::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_umin::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == 1); assert!(x2 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs index e91027f61b5a..e8a1524cbdbd 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs @@ -5,10 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_xchg_acqrel, atomic_xchg_acquire, atomic_xchg_relaxed, atomic_xchg_release, - atomic_xchg_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_xchg}; #[kani::proof] fn main() { @@ -29,15 +26,15 @@ fn main() { // Returns (val, ok) where // * val: the old value // * ok: bool indicating whether the operation was successful or not - assert!(atomic_xchg_seqcst(ptr_a1, 1) == 0); - assert!(atomic_xchg_seqcst(ptr_a1, 0) == 1); - assert!(atomic_xchg_acquire(ptr_a2, 1) == 0); - assert!(atomic_xchg_acquire(ptr_a2, 0) == 1); - assert!(atomic_xchg_acqrel(ptr_a3, 1) == 0); - assert!(atomic_xchg_acqrel(ptr_a3, 0) == 1); - assert!(atomic_xchg_release(ptr_a4, 1) == 0); - assert!(atomic_xchg_release(ptr_a4, 0) == 1); - assert!(atomic_xchg_relaxed(ptr_a5, 1) == 0); - assert!(atomic_xchg_relaxed(ptr_a5, 0) == 1); + assert!(atomic_xchg::<_, { AtomicOrdering::SeqCst }>(ptr_a1, 1) == 0); + assert!(atomic_xchg::<_, { AtomicOrdering::SeqCst }>(ptr_a1, 0) == 1); + assert!(atomic_xchg::<_, { AtomicOrdering::Acquire }>(ptr_a2, 1) == 0); + assert!(atomic_xchg::<_, { AtomicOrdering::Acquire }>(ptr_a2, 0) == 1); + assert!(atomic_xchg::<_, { AtomicOrdering::AcqRel }>(ptr_a3, 1) == 0); + assert!(atomic_xchg::<_, { AtomicOrdering::AcqRel }>(ptr_a3, 0) == 1); + assert!(atomic_xchg::<_, { AtomicOrdering::Release }>(ptr_a4, 1) == 0); + assert!(atomic_xchg::<_, { AtomicOrdering::Release }>(ptr_a4, 0) == 1); + assert!(atomic_xchg::<_, { AtomicOrdering::Relaxed }>(ptr_a5, 1) == 0); + assert!(atomic_xchg::<_, { AtomicOrdering::Relaxed }>(ptr_a5, 0) == 1); } } diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs index e9953aa7852d..61a9e397e167 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs @@ -5,10 +5,7 @@ // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{ - atomic_xor_acqrel, atomic_xor_acquire, atomic_xor_relaxed, atomic_xor_release, - atomic_xor_seqcst, -}; +use std::intrinsics::{AtomicOrdering, atomic_xor}; #[kani::proof] fn main() { @@ -27,11 +24,11 @@ fn main() { let b = 1 as u8; unsafe { - let x1 = atomic_xor_seqcst(ptr_a1, b); - let x2 = atomic_xor_acquire(ptr_a2, b); - let x3 = atomic_xor_acqrel(ptr_a3, b); - let x4 = atomic_xor_release(ptr_a4, b); - let x5 = atomic_xor_relaxed(ptr_a5, b); + let x1 = atomic_xor::<_, { AtomicOrdering::SeqCst }>(ptr_a1, b); + let x2 = atomic_xor::<_, { AtomicOrdering::Acquire }>(ptr_a2, b); + let x3 = atomic_xor::<_, { AtomicOrdering::AcqRel }>(ptr_a3, b); + let x4 = atomic_xor::<_, { AtomicOrdering::Release }>(ptr_a4, b); + let x5 = atomic_xor::<_, { AtomicOrdering::Relaxed }>(ptr_a5, b); assert!(x1 == 1); assert!(x2 == 1); From e338bc9599303f98dd66a57796580be42786e406 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 12 Jun 2025 19:23:27 -0400 Subject: [PATCH 6/8] update to 6/10 --- docs/src/rust-feature-support/intrinsics.md | 1 - .../codegen/intrinsic.rs | 1 - .../compiler_interface.rs | 9 +- kani-compiler/src/intrinsics.rs | 5 -- .../points_to/points_to_analysis.rs | 1 - .../check_uninit/ptr_uninit/uninit_visitor.rs | 1 - rust-toolchain.toml | 2 +- .../Intrinsics/ConstEval/pref_align_of.rs | 85 ------------------- 8 files changed, 6 insertions(+), 99 deletions(-) delete mode 100644 tests/kani/Intrinsics/ConstEval/pref_align_of.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 2fa8b54094fc..9e4c26639f88 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -187,7 +187,6 @@ powf32 | Partial | Results are overapproximated | powf64 | Partial | Results are overapproximated | powif32 | Partial | Results are overapproximated | powif64 | Partial | Results are overapproximated | -pref_align_of | Yes | | prefetch_read_data | No | | prefetch_read_instruction | No | | prefetch_write_data | No | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 01ba2c8caeaa..29085b561e21 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -419,7 +419,6 @@ impl GotocCtx<'_> { Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow), Intrinsic::PowIF32 => codegen_simple_intrinsic!(Powif), Intrinsic::PowIF64 => codegen_simple_intrinsic!(Powi), - Intrinsic::PrefAlignOf => codegen_intrinsic_const!(), Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc), diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 2561c51b2c68..ae245ddca8f2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -20,7 +20,7 @@ use cbmc::{InternedString, MachineModel}; use kani_metadata::artifact::convert_type; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata, UnsupportedFeature}; use kani_metadata::{AssignsContract, CompilerArtifactStub}; -use rustc_abi::Endian; +use rustc_abi::{Align, Endian}; use rustc_codegen_ssa::back::archive::{ ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER, }; @@ -511,10 +511,11 @@ fn check_options(session: &Session) { // a valid CBMC machine model in function `machine_model_from_session` from // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs match session.target.options.min_global_align { - Some(1) => (), + Some(Align::ONE) => (), Some(align) => { let err_msg = format!( - "Kani requires the target architecture option `min_global_align` to be 1, but it is {align}." + "Kani requires the target architecture option `min_global_align` to be 1, but it is {}.", + align.bytes() ); session.dcx().err(err_msg); } @@ -705,7 +706,7 @@ fn new_machine_model(sess: &Session) -> MachineModel { // We check these options in function `check_options` from // src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs // and error if their values are not the ones we expect. - let alignment = sess.target.options.min_global_align.unwrap_or(1); + let alignment = sess.target.options.min_global_align.map_or(1, |align| align.bytes()); let is_big_endian = match sess.target.options.endian { Endian::Little => false, Endian::Big => true, diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index 862438f3cfc8..d9698bbc1586 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -91,7 +91,6 @@ pub enum Intrinsic { PowF64, PowIF32, PowIF64, - PrefAlignOf, PtrGuaranteedCmp, PtrOffsetFrom, PtrOffsetFromUnsigned, @@ -330,10 +329,6 @@ impl Intrinsic { "offset" => unreachable!( "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`" ), - "pref_align_of" => { - assert_sig_matches!(sig, => RigidTy::Uint(UintTy::Usize)); - Self::PrefAlignOf - } "ptr_guaranteed_cmp" => { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::U8)); Self::PtrGuaranteedCmp diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index a3526d9979d8..d617c9ccdc6c 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -669,7 +669,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::PowF64 | Intrinsic::PowIF32 | Intrinsic::PowIF64 - | Intrinsic::PrefAlignOf | Intrinsic::PtrGuaranteedCmp | Intrinsic::PtrOffsetFrom | Intrinsic::PtrOffsetFromUnsigned diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index ea3c5db5c216..01606b8497d9 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -629,7 +629,6 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::PowF64 | Intrinsic::PowIF32 | Intrinsic::PowIF64 - | Intrinsic::PrefAlignOf | Intrinsic::RawEq | Intrinsic::RotateLeft | Intrinsic::RotateRight diff --git a/rust-toolchain.toml b/rust-toolchain.toml index e6ffe0e9051f..ce52977b8ae8 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-09" +channel = "nightly-2025-06-10" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Intrinsics/ConstEval/pref_align_of.rs b/tests/kani/Intrinsics/ConstEval/pref_align_of.rs deleted file mode 100644 index d495bffef5f8..000000000000 --- a/tests/kani/Intrinsics/ConstEval/pref_align_of.rs +++ /dev/null @@ -1,85 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Check that we get the expected results for the `pref_align_of` intrinsic -// with common data types -#![feature(core_intrinsics)] -use std::intrinsics::pref_align_of; - -struct MyStruct {} - -enum MyEnum {} - -#[kani::proof] -fn main() { - #[cfg(target_arch = "x86_64")] - { - // Scalar types - assert!(unsafe { pref_align_of::() } == 1); - assert!(unsafe { pref_align_of::() } == 2); - assert!(unsafe { pref_align_of::() } == 4); - assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 16); - assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 1); - assert!(unsafe { pref_align_of::() } == 2); - assert!(unsafe { pref_align_of::() } == 4); - assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 16); - assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 4); - assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 1); - assert!(unsafe { pref_align_of::() } == 4); - // Compound types (tuple and array) - assert!(unsafe { pref_align_of::<(i32, i32)>() } == 8); - assert!(unsafe { pref_align_of::<[i32; 5]>() } == 4); - // Custom data types (struct and enum) - assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 1); - } - #[cfg(target_arch = "aarch64")] - { - // Scalar types - #[cfg(target_os = "linux")] - assert!(unsafe { pref_align_of::() } == 4); - #[cfg(target_os = "macos")] - assert!(unsafe { pref_align_of::() } == 1); - #[cfg(target_os = "linux")] - assert!(unsafe { pref_align_of::() } == 4); - #[cfg(target_os = "macos")] - assert!(unsafe { pref_align_of::() } == 2); - assert!(unsafe { pref_align_of::() } == 4); - assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 16); - assert!(unsafe { pref_align_of::() } == 8); - #[cfg(target_os = "linux")] - assert!(unsafe { pref_align_of::() } == 4); - #[cfg(target_os = "macos")] - assert!(unsafe { pref_align_of::() } == 1); - #[cfg(target_os = "linux")] - assert!(unsafe { pref_align_of::() } == 4); - #[cfg(target_os = "macos")] - assert!(unsafe { pref_align_of::() } == 2); - assert!(unsafe { pref_align_of::() } == 4); - assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 16); - assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 4); - assert!(unsafe { pref_align_of::() } == 8); - #[cfg(target_os = "linux")] - assert!(unsafe { pref_align_of::() } == 4); - #[cfg(target_os = "macos")] - assert!(unsafe { pref_align_of::() } == 1); - assert!(unsafe { pref_align_of::() } == 4); - // Compound types (tuple and array) - assert!(unsafe { pref_align_of::<(i32, i32)>() } == 8); - assert!(unsafe { pref_align_of::<[i32; 5]>() } == 4); - // Custom data types (struct and enum) - assert!(unsafe { pref_align_of::() } == 8); - #[cfg(target_os = "linux")] - assert!(unsafe { pref_align_of::() } == 4); - #[cfg(target_os = "macos")] - assert!(unsafe { pref_align_of::() } == 1); - } -} From c9976b4edddc5c39a393f5bfffb8c5015a67b13a Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 12 Jun 2025 19:25:48 -0400 Subject: [PATCH 7/8] update to 6/13 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index ce52977b8ae8..b0e88c8f2fc0 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-10" +channel = "nightly-2025-06-13" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 2086875d86fd3c11090fc014153851329079dea1 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Sat, 14 Jun 2025 13:56:45 -0400 Subject: [PATCH 8/8] atomic intrinsics no longer have suffixes --- .../codegen/intrinsic.rs | 32 ++-- kani-compiler/src/intrinsics.rs | 155 ++++++++++-------- .../points_to/points_to_analysis.rs | 28 ++-- .../check_uninit/ptr_uninit/uninit_visitor.rs | 30 ++-- 4 files changed, 130 insertions(+), 115 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 29085b561e21..921d9bd8c33e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -302,27 +302,25 @@ impl GotocCtx<'_> { "Rust intrinsic assumption failed", loc, ), - Intrinsic::AtomicAnd(_) => codegen_atomic_binop!(bitand), - Intrinsic::AtomicCxchg(_) | Intrinsic::AtomicCxchgWeak(_) => { + Intrinsic::AtomicAnd => codegen_atomic_binop!(bitand), + Intrinsic::AtomicCxchg | Intrinsic::AtomicCxchgWeak => { self.codegen_atomic_cxchg(intrinsic_str, fargs, place, loc) } - Intrinsic::AtomicFence(_) => self.codegen_atomic_noop(intrinsic_str, loc), + Intrinsic::AtomicFence => self.codegen_atomic_noop(intrinsic_str, loc), Intrinsic::AtomicLoad => self.codegen_atomic_load(intrinsic_str, fargs, place, loc), - Intrinsic::AtomicMax(_) => codegen_atomic_binop!(max), - Intrinsic::AtomicMin(_) => codegen_atomic_binop!(min), - Intrinsic::AtomicNand(_) => codegen_atomic_binop!(bitnand), - Intrinsic::AtomicOr(_) => codegen_atomic_binop!(bitor), - Intrinsic::AtomicSingleThreadFence(_) => self.codegen_atomic_noop(intrinsic_str, loc), - Intrinsic::AtomicStore(_) => { - self.codegen_atomic_store(intrinsic_str, fargs, place, loc) - } - Intrinsic::AtomicUmax(_) => codegen_atomic_binop!(max), - Intrinsic::AtomicUmin(_) => codegen_atomic_binop!(min), - Intrinsic::AtomicXadd(_) => codegen_atomic_binop!(plus), - Intrinsic::AtomicXchg(_) => self.codegen_atomic_store(intrinsic_str, fargs, place, loc), - Intrinsic::AtomicXor(_) => codegen_atomic_binop!(bitxor), - Intrinsic::AtomicXsub(_) => codegen_atomic_binop!(sub), + Intrinsic::AtomicMax => codegen_atomic_binop!(max), + Intrinsic::AtomicMin => codegen_atomic_binop!(min), + Intrinsic::AtomicNand => codegen_atomic_binop!(bitnand), + Intrinsic::AtomicOr => codegen_atomic_binop!(bitor), + Intrinsic::AtomicSingleThreadFence => self.codegen_atomic_noop(intrinsic_str, loc), + Intrinsic::AtomicStore => self.codegen_atomic_store(intrinsic_str, fargs, place, loc), + Intrinsic::AtomicUmax => codegen_atomic_binop!(max), + Intrinsic::AtomicUmin => codegen_atomic_binop!(min), + Intrinsic::AtomicXadd => codegen_atomic_binop!(plus), + Intrinsic::AtomicXchg => self.codegen_atomic_store(intrinsic_str, fargs, place, loc), + Intrinsic::AtomicXor => codegen_atomic_binop!(bitxor), + Intrinsic::AtomicXsub => codegen_atomic_binop!(sub), Intrinsic::Bitreverse => { self.codegen_expr_to_place_stable(place, fargs.remove(0).bitreverse(), loc) } diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index d9698bbc1586..613c078cac0f 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -19,23 +19,23 @@ pub enum Intrinsic { AssertMemUninitializedValid, AssertZeroValid, Assume, - AtomicAnd(String), - AtomicCxchg(String), - AtomicCxchgWeak(String), - AtomicFence(String), + AtomicAnd, + AtomicCxchg, + AtomicCxchgWeak, + AtomicFence, AtomicLoad, - AtomicMax(String), - AtomicMin(String), - AtomicNand(String), - AtomicOr(String), - AtomicSingleThreadFence(String), - AtomicStore(String), - AtomicUmax(String), - AtomicUmin(String), - AtomicXadd(String), - AtomicXchg(String), - AtomicXor(String), - AtomicXsub(String), + AtomicMax, + AtomicMin, + AtomicNand, + AtomicOr, + AtomicSingleThreadFence, + AtomicStore, + AtomicUmax, + AtomicUmin, + AtomicXadd, + AtomicXchg, + AtomicXor, + AtomicXsub, Bitreverse, BlackBox, Breakpoint, @@ -466,59 +466,76 @@ impl Intrinsic { fn try_match_atomic(intrinsic_instance: &Instance) -> Option { let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap(); let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder(); - if let Some(suffix) = intrinsic_str.strip_prefix("atomic_and") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicAnd(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchgweak") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_)); - Some(Intrinsic::AtomicCxchgWeak(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchg") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_)); - Some(Intrinsic::AtomicCxchg(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_fence") { - assert_sig_matches!(sig, => RigidTy::Tuple(_)); - Some(Intrinsic::AtomicFence(suffix.into())) - } else if intrinsic_str == "atomic_load" { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _); - Some(Intrinsic::AtomicLoad) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_max") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicMax(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_min") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicMin(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_nand") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicNand(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_or") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicOr(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_singlethreadfence") { - assert_sig_matches!(sig, => RigidTy::Tuple(_)); - Some(Intrinsic::AtomicSingleThreadFence(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_store") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_)); - Some(Intrinsic::AtomicStore(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umax") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicUmax(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umin") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicUmin(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xadd") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicXadd(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xchg") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicXchg(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xor") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicXor(suffix.into())) - } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xsub") { - assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); - Some(Intrinsic::AtomicXsub(suffix.into())) - } else { - None + match intrinsic_str.as_str() { + "atomic_and" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicAnd) + } + "atomic_cxchgweak" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_)); + Some(Intrinsic::AtomicCxchgWeak) + } + "atomic_cxchg" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_)); + Some(Intrinsic::AtomicCxchg) + } + "atomic_fence" => { + assert_sig_matches!(sig, => RigidTy::Tuple(_)); + Some(Intrinsic::AtomicFence) + } + "atomic_load" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _); + Some(Intrinsic::AtomicLoad) + } + "atomic_max" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicMax) + } + "atomic_min" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicMin) + } + "atomic_nand" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicNand) + } + "atomic_or" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicOr) + } + "atomic_singlethreadfence" => { + assert_sig_matches!(sig, => RigidTy::Tuple(_)); + Some(Intrinsic::AtomicSingleThreadFence) + } + "atomic_store" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_)); + Some(Intrinsic::AtomicStore) + } + "atomic_umax" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicUmax) + } + "atomic_umin" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicUmin) + } + "atomic_xadd" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicXadd) + } + "atomic_xchg" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicXchg) + } + "atomic_xor" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicXor) + } + "atomic_xsub" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _); + Some(Intrinsic::AtomicXsub) + } + _ => None, } } diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index d617c9ccdc6c..363831c1db26 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -218,7 +218,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { } // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments. // This is equivalent to `destination = *dst; *dst = src`. - Intrinsic::AtomicCxchg(_) | Intrinsic::AtomicCxchgWeak(_) => { + Intrinsic::AtomicCxchg | Intrinsic::AtomicCxchgWeak => { let src_set = self.successors_for_operand(state, args[2].node.clone()); let dst_set = self.successors_for_deref(state, args[0].node.clone()); let destination_set = state.resolve_place(*destination, self.instance); @@ -234,24 +234,24 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { } // All `atomic_store` intrinsics take `dst, val` as arguments. // This is equivalent to `*dst = val`. - Intrinsic::AtomicStore(_) => { + Intrinsic::AtomicStore => { let dst_set = self.successors_for_deref(state, args[0].node.clone()); let val_set = self.successors_for_operand(state, args[1].node.clone()); state.extend(&dst_set, &val_set); } // All other `atomic` intrinsics take `dst, src` as arguments. // This is equivalent to `destination = *dst; *dst = src`. - Intrinsic::AtomicAnd(_) - | Intrinsic::AtomicMax(_) - | Intrinsic::AtomicMin(_) - | Intrinsic::AtomicNand(_) - | Intrinsic::AtomicOr(_) - | Intrinsic::AtomicUmax(_) - | Intrinsic::AtomicUmin(_) - | Intrinsic::AtomicXadd(_) - | Intrinsic::AtomicXchg(_) - | Intrinsic::AtomicXor(_) - | Intrinsic::AtomicXsub(_) => { + Intrinsic::AtomicAnd + | Intrinsic::AtomicMax + | Intrinsic::AtomicMin + | Intrinsic::AtomicNand + | Intrinsic::AtomicOr + | Intrinsic::AtomicUmax + | Intrinsic::AtomicUmin + | Intrinsic::AtomicXadd + | Intrinsic::AtomicXchg + | Intrinsic::AtomicXor + | Intrinsic::AtomicXsub => { let src_set = self.successors_for_operand(state, args[1].node.clone()); let dst_set = self.successors_for_deref(state, args[0].node.clone()); let destination_set = state.resolve_place(*destination, self.instance); @@ -727,7 +727,7 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { /* SIMD operations */ true } - Intrinsic::AtomicFence(_) | Intrinsic::AtomicSingleThreadFence(_) => { + Intrinsic::AtomicFence | Intrinsic::AtomicSingleThreadFence => { /* Atomic fences */ true } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 01606b8497d9..62161d28dee2 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -283,21 +283,21 @@ impl MirVisitor for CheckUninitVisitor { intrinsic_name if can_skip_intrinsic(intrinsic_name.clone()) => { /* Intrinsics that can be safely skipped */ } - Intrinsic::AtomicAnd(_) - | Intrinsic::AtomicCxchg(_) - | Intrinsic::AtomicCxchgWeak(_) + Intrinsic::AtomicAnd + | Intrinsic::AtomicCxchg + | Intrinsic::AtomicCxchgWeak | Intrinsic::AtomicLoad - | Intrinsic::AtomicMax(_) - | Intrinsic::AtomicMin(_) - | Intrinsic::AtomicNand(_) - | Intrinsic::AtomicOr(_) - | Intrinsic::AtomicStore(_) - | Intrinsic::AtomicUmax(_) - | Intrinsic::AtomicUmin(_) - | Intrinsic::AtomicXadd(_) - | Intrinsic::AtomicXchg(_) - | Intrinsic::AtomicXor(_) - | Intrinsic::AtomicXsub(_) => { + | Intrinsic::AtomicMax + | Intrinsic::AtomicMin + | Intrinsic::AtomicNand + | Intrinsic::AtomicOr + | Intrinsic::AtomicStore + | Intrinsic::AtomicUmax + | Intrinsic::AtomicUmin + | Intrinsic::AtomicXadd + | Intrinsic::AtomicXchg + | Intrinsic::AtomicXor + | Intrinsic::AtomicXsub => { self.push_target(MemoryInitOp::Check { operand: args[0].clone() }); } Intrinsic::CompareBytes => { @@ -685,7 +685,7 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool { /* SIMD operations */ true } - Intrinsic::AtomicFence(_) | Intrinsic::AtomicSingleThreadFence(_) => { + Intrinsic::AtomicFence | Intrinsic::AtomicSingleThreadFence => { /* Atomic fences */ true }