From 4a4539be611f0786a428f4ea4a01bdf8e63a7979 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 5 Jul 2022 20:45:56 -0700 Subject: [PATCH 1/4] Update toolchain to 2022-07-05 The updates required were related to the following changes: - Simplify memory ordering intrinsics - https://github.com/rust-lang/rust/pull/97423 - once cell renamings - https://github.com/rust-lang/rust/pull/98165 - Rename the ConstS::val field as kind - https://github.com/rust-lang/rust/pull/97935 - Remove the source archive functionality of ArchiveWriter - https://github.com/rust-lang/rust/pull/98098 - Use valtrees as the type-system representation for constant values - https://github.com/rust-lang/rust/pull/96591 --- .../src/codegen_cprover_gotoc/archive.rs | 41 ++------- .../codegen/intrinsic.rs | 86 +++++++++---------- .../codegen_cprover_gotoc/codegen/operand.rs | 13 +-- .../codegen_cprover_gotoc/codegen/place.rs | 4 +- .../src/codegen_cprover_gotoc/utils/debug.rs | 8 +- kani-compiler/src/session.rs | 8 +- rust-toolchain.toml | 2 +- .../Atomic/Unstable/AtomicAdd/main.rs | 9 +- .../Atomic/Unstable/AtomicAnd/main.rs | 11 +-- .../Atomic/Unstable/AtomicCxchg/main.rs | 42 ++++----- .../Atomic/Unstable/AtomicCxchgWeak/main.rs | 46 +++++----- .../Atomic/Unstable/AtomicFence/main.rs | 10 ++- .../Atomic/Unstable/AtomicLoad/main.rs | 8 +- .../Atomic/Unstable/AtomicMax/main.rs | 11 +-- .../Atomic/Unstable/AtomicMin/main.rs | 11 +-- .../Atomic/Unstable/AtomicNand/main.rs | 17 ++-- .../Atomic/Unstable/AtomicOr/main.rs | 14 +-- .../Unstable/AtomicSingleThreadFence/main.rs | 12 +-- .../Atomic/Unstable/AtomicStore/main.rs | 8 +- .../Atomic/Unstable/AtomicSub/main.rs | 11 +-- .../Atomic/Unstable/AtomicUmax/main.rs | 11 +-- .../Atomic/Unstable/AtomicUmin/main.rs | 11 +-- .../Atomic/Unstable/AtomicXchg/main.rs | 17 ++-- .../Atomic/Unstable/AtomicXor/main.rs | 11 +-- .../Copy/copy_nonoverlapping_append.rs | 1 + tests/kani/Refs/main.rs | 1 + tests/ui/code-location/expected | 2 +- 27 files changed, 207 insertions(+), 219 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/archive.rs b/kani-compiler/src/codegen_cprover_gotoc/archive.rs index ae865cf86086..53df0135766d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/archive.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/archive.rs @@ -44,47 +44,16 @@ pub(crate) struct ArArchiveBuilder<'a> { } impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> { - fn new(sess: &'a Session, output: &Path, input: Option<&Path>) -> Self { - let (src_archives, entries) = if let Some(input) = input { - let read_cache = ReadCache::new(File::open(input).unwrap()); - let archive = ArchiveFile::parse(&read_cache).unwrap(); - let mut entries = Vec::new(); - - for entry in archive.members() { - let entry = entry.unwrap(); - entries.push(( - entry.name().to_vec(), - ArchiveEntry::FromArchive { archive_index: 0, file_range: entry.file_range() }, - )); - } - - (vec![read_cache.into_inner()], entries) - } else { - (vec![], Vec::new()) - }; - + fn new(sess: &'a Session, output: &Path) -> Self { ArArchiveBuilder { sess, dst: output.to_path_buf(), use_gnu_style_archive: sess.target.archive_format == "gnu", - src_archives, - entries, + src_archives: vec![], + entries: vec![], } } - fn src_files(&mut self) -> Vec { - self.entries.iter().map(|(name, _)| String::from_utf8(name.clone()).unwrap()).collect() - } - - fn remove_file(&mut self, name: &str) { - let index = self - .entries - .iter() - .position(|(entry_name, _)| entry_name == name.as_bytes()) - .expect("Tried to remove file not existing in src archive"); - self.entries.remove(index); - } - fn add_file(&mut self, file: &Path) { self.entries.push(( file.file_name().unwrap().to_str().unwrap().to_string().into_bytes(), @@ -116,7 +85,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> { Ok(()) } - fn build(mut self) { + fn build(mut self) -> bool { enum BuilderKind { Bsd(ar::Builder), Gnu(ar::GnuBuilder), @@ -168,6 +137,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> { }; // Add all files + let any_members = !entries.is_empty(); for (entry_name, data) in entries.into_iter() { let header = ar::Header::new(entry_name, data.len() as u64); match builder { @@ -178,6 +148,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> { // Finalize archive std::mem::drop(builder); + any_members } fn inject_dll_import_lib( diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 2ec2278dd44e..83dacec015f0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -396,79 +396,79 @@ impl<'tcx> GotocCtx<'tcx> { "assumption failed", loc, ), - "atomic_and" => codegen_atomic_binop!(bitand), - "atomic_and_acq" => codegen_atomic_binop!(bitand), + "atomic_and_seqcst" => codegen_atomic_binop!(bitand), + "atomic_and_acquire" => codegen_atomic_binop!(bitand), "atomic_and_acqrel" => codegen_atomic_binop!(bitand), - "atomic_and_rel" => codegen_atomic_binop!(bitand), + "atomic_and_release" => codegen_atomic_binop!(bitand), "atomic_and_relaxed" => codegen_atomic_binop!(bitand), name if name.starts_with("atomic_cxchg") => { self.codegen_atomic_cxchg(intrinsic, fargs, p, loc) } - "atomic_fence" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_fence_acq" => self.codegen_atomic_noop(intrinsic, loc), + "atomic_fence_seqcst" => self.codegen_atomic_noop(intrinsic, loc), + "atomic_fence_acquire" => self.codegen_atomic_noop(intrinsic, loc), "atomic_fence_acqrel" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_fence_rel" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_load" => self.codegen_atomic_load(intrinsic, fargs, p, loc), - "atomic_load_acq" => self.codegen_atomic_load(intrinsic, fargs, p, loc), + "atomic_fence_release" => self.codegen_atomic_noop(intrinsic, loc), + "atomic_load_seqcst" => self.codegen_atomic_load(intrinsic, fargs, p, loc), + "atomic_load_acquire" => self.codegen_atomic_load(intrinsic, fargs, p, loc), "atomic_load_relaxed" => self.codegen_atomic_load(intrinsic, fargs, p, loc), "atomic_load_unordered" => self.codegen_atomic_load(intrinsic, fargs, p, loc), - "atomic_max" => codegen_atomic_binop!(max), - "atomic_max_acq" => codegen_atomic_binop!(max), + "atomic_max_seqcst" => codegen_atomic_binop!(max), + "atomic_max_acquire" => codegen_atomic_binop!(max), "atomic_max_acqrel" => codegen_atomic_binop!(max), - "atomic_max_rel" => codegen_atomic_binop!(max), + "atomic_max_release" => codegen_atomic_binop!(max), "atomic_max_relaxed" => codegen_atomic_binop!(max), - "atomic_min" => codegen_atomic_binop!(min), - "atomic_min_acq" => codegen_atomic_binop!(min), + "atomic_min_seqcst" => codegen_atomic_binop!(min), + "atomic_min_acquire" => codegen_atomic_binop!(min), "atomic_min_acqrel" => codegen_atomic_binop!(min), - "atomic_min_rel" => codegen_atomic_binop!(min), + "atomic_min_release" => codegen_atomic_binop!(min), "atomic_min_relaxed" => codegen_atomic_binop!(min), - "atomic_nand" => codegen_atomic_binop!(bitnand), - "atomic_nand_acq" => codegen_atomic_binop!(bitnand), + "atomic_nand_seqcst" => codegen_atomic_binop!(bitnand), + "atomic_nand_acquire" => codegen_atomic_binop!(bitnand), "atomic_nand_acqrel" => codegen_atomic_binop!(bitnand), - "atomic_nand_rel" => codegen_atomic_binop!(bitnand), + "atomic_nand_release" => codegen_atomic_binop!(bitnand), "atomic_nand_relaxed" => codegen_atomic_binop!(bitnand), - "atomic_or" => codegen_atomic_binop!(bitor), - "atomic_or_acq" => codegen_atomic_binop!(bitor), + "atomic_or_seqcst" => codegen_atomic_binop!(bitor), + "atomic_or_acquire" => codegen_atomic_binop!(bitor), "atomic_or_acqrel" => codegen_atomic_binop!(bitor), - "atomic_or_rel" => codegen_atomic_binop!(bitor), + "atomic_or_release" => codegen_atomic_binop!(bitor), "atomic_or_relaxed" => codegen_atomic_binop!(bitor), - "atomic_singlethreadfence" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_singlethreadfence_acq" => self.codegen_atomic_noop(intrinsic, loc), + "atomic_singlethreadfence_seqcst" => self.codegen_atomic_noop(intrinsic, loc), + "atomic_singlethreadfence_acquire" => self.codegen_atomic_noop(intrinsic, loc), "atomic_singlethreadfence_acqrel" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_singlethreadfence_rel" => self.codegen_atomic_noop(intrinsic, loc), - "atomic_store" => self.codegen_atomic_store(intrinsic, fargs, p, loc), - "atomic_store_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc), + "atomic_singlethreadfence_release" => self.codegen_atomic_noop(intrinsic, loc), + "atomic_store_seqcst" => self.codegen_atomic_store(intrinsic, fargs, p, loc), + "atomic_store_release" => self.codegen_atomic_store(intrinsic, fargs, p, loc), "atomic_store_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc), "atomic_store_unordered" => self.codegen_atomic_store(intrinsic, fargs, p, loc), - "atomic_umax" => codegen_atomic_binop!(max), - "atomic_umax_acq" => codegen_atomic_binop!(max), + "atomic_umax_seqcst" => codegen_atomic_binop!(max), + "atomic_umax_acquire" => codegen_atomic_binop!(max), "atomic_umax_acqrel" => codegen_atomic_binop!(max), - "atomic_umax_rel" => codegen_atomic_binop!(max), + "atomic_umax_release" => codegen_atomic_binop!(max), "atomic_umax_relaxed" => codegen_atomic_binop!(max), - "atomic_umin" => codegen_atomic_binop!(min), - "atomic_umin_acq" => codegen_atomic_binop!(min), + "atomic_umin_seqcst" => codegen_atomic_binop!(min), + "atomic_umin_acquire" => codegen_atomic_binop!(min), "atomic_umin_acqrel" => codegen_atomic_binop!(min), - "atomic_umin_rel" => codegen_atomic_binop!(min), + "atomic_umin_release" => codegen_atomic_binop!(min), "atomic_umin_relaxed" => codegen_atomic_binop!(min), - "atomic_xadd" => codegen_atomic_binop!(plus), - "atomic_xadd_acq" => codegen_atomic_binop!(plus), + "atomic_xadd_seqcst" => codegen_atomic_binop!(plus), + "atomic_xadd_acquire" => codegen_atomic_binop!(plus), "atomic_xadd_acqrel" => codegen_atomic_binop!(plus), - "atomic_xadd_rel" => codegen_atomic_binop!(plus), + "atomic_xadd_release" => codegen_atomic_binop!(plus), "atomic_xadd_relaxed" => codegen_atomic_binop!(plus), - "atomic_xchg" => self.codegen_atomic_store(intrinsic, fargs, p, loc), - "atomic_xchg_acq" => self.codegen_atomic_store(intrinsic, fargs, p, loc), + "atomic_xchg_seqcst" => self.codegen_atomic_store(intrinsic, fargs, p, loc), + "atomic_xchg_acquire" => self.codegen_atomic_store(intrinsic, fargs, p, loc), "atomic_xchg_acqrel" => self.codegen_atomic_store(intrinsic, fargs, p, loc), - "atomic_xchg_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc), + "atomic_xchg_release" => self.codegen_atomic_store(intrinsic, fargs, p, loc), "atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc), - "atomic_xor" => codegen_atomic_binop!(bitxor), - "atomic_xor_acq" => codegen_atomic_binop!(bitxor), + "atomic_xor_seqcst" => codegen_atomic_binop!(bitxor), + "atomic_xor_acquire" => codegen_atomic_binop!(bitxor), "atomic_xor_acqrel" => codegen_atomic_binop!(bitxor), - "atomic_xor_rel" => codegen_atomic_binop!(bitxor), + "atomic_xor_release" => codegen_atomic_binop!(bitxor), "atomic_xor_relaxed" => codegen_atomic_binop!(bitxor), - "atomic_xsub" => codegen_atomic_binop!(sub), - "atomic_xsub_acq" => codegen_atomic_binop!(sub), + "atomic_xsub_seqcst" => codegen_atomic_binop!(sub), + "atomic_xsub_acquire" => codegen_atomic_binop!(sub), "atomic_xsub_acqrel" => codegen_atomic_binop!(sub), - "atomic_xsub_rel" => codegen_atomic_binop!(sub), + "atomic_xsub_release" => codegen_atomic_binop!(sub), "atomic_xsub_relaxed" => codegen_atomic_binop!(sub), "bitreverse" => self.codegen_expr_to_place(p, fargs.remove(0).bitreverse()), // black_box is an identity function that hints to the compiler diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 610dff983f09..da7c953c493c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -57,7 +57,7 @@ impl<'tcx> GotocCtx<'tcx> { debug!("found literal: {:?}", lit); let lit = self.monomorphize(lit); - match lit.val() { + match lit.kind() { // evaluate constant if it has no been evaluated yet ConstKind::Unevaluated(unevaluated) => { debug!("The literal was a Unevaluated"); @@ -68,14 +68,15 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_const_value(const_val, lit.ty(), span) } - ConstKind::Value(v) => { - debug!("The literal was a ConstValue {:?}", v); - self.codegen_const_value(v, lit.ty(), span) + ConstKind::Value(valtree) => { + let value = self.tcx.valtree_to_const_val((lit.ty(), valtree)); + debug!("The literal was a ConstValue {:?}", value); + self.codegen_const_value(value, lit.ty(), span) } _ => { unreachable!( "monomorphized item shouldn't have this constant value: {:?}", - lit.val() + lit.kind() ) } } @@ -128,7 +129,7 @@ impl<'tcx> GotocCtx<'tcx> { _ => {} } } - unimplemented!("\nv {:?}\nlit_ty {:?}\nspan {:?}", v, lit_ty, span); + unimplemented!("\nv {:?}\nlit_ty {:?}\nspan {:?}", v, lit_ty.kind(), span); } pub fn codegen_const_value( diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 40051137ff19..d35e6e6d8bf3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -446,7 +446,7 @@ impl<'tcx> GotocCtx<'tcx> { // https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html match before.mir_typ().kind() { ty::Array(ty, len) => { - let len = len.val().try_to_machine_usize(self.tcx).unwrap(); + let len = len.kind().try_to_machine_usize(self.tcx).unwrap(); let subarray_len = if from_end { // `to` counts from the end of the array len - to - from @@ -578,7 +578,7 @@ impl<'tcx> GotocCtx<'tcx> { match before.mir_typ().kind() { //TODO, ask on zulip if we can ever have from_end here? ty::Array(elemt, length) => { - let length = length.val().try_to_machine_usize(self.tcx).unwrap(); + let length = length.kind().try_to_machine_usize(self.tcx).unwrap(); assert!(length >= min_length); let idx = if from_end { length - offset } else { offset }; let idxe = Expr::int_constant(idx, Type::ssize_t()); diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs index 590e6b078523..92af99445146 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs @@ -10,8 +10,8 @@ use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::Instance; use rustc_span::def_id::DefId; use std::cell::RefCell; -use std::lazy::SyncLazy; use std::panic; +use std::sync::LazyLock; use tracing::debug; // Use a thread-local global variable to track the current codegen item for debugging. @@ -21,12 +21,12 @@ thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option, Option) + Sync + Send + 'static>> = - SyncLazy::new(|| { +static DEFAULT_HOOK: LazyLock) + Sync + Send + 'static>> = + LazyLock::new(|| { let hook = panic::take_hook(); panic::set_hook(Box::new(|info| { // Invoke the default handler, which prints the actual panic message and diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 37d3f87343f3..f577d251ee56 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -5,9 +5,9 @@ use crate::parser; use clap::ArgMatches; -use std::lazy::SyncLazy; use std::panic; use std::str::FromStr; +use std::sync::LazyLock; use tracing_subscriber::{filter::Directive, layer::SubscriberExt, EnvFilter, Registry}; use tracing_tree::HierarchicalLayer; @@ -19,8 +19,8 @@ const BUG_REPORT_URL: &str = "https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md"; // Custom panic hook. -static PANIC_HOOK: SyncLazy) + Sync + Send + 'static>> = - SyncLazy::new(|| { +static PANIC_HOOK: LazyLock) + Sync + Send + 'static>> = + LazyLock::new(|| { let hook = panic::take_hook(); panic::set_hook(Box::new(|info| { // Print stack trace. @@ -92,5 +92,5 @@ fn hier_logs(args: &ArgMatches, filter: EnvFilter) { fn init_panic_hook() { // Install panic hook - SyncLazy::force(&PANIC_HOOK); // Install ice hook + LazyLock::force(&PANIC_HOOK); // Install ice hook } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index de3911297898..468e8286bdab 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2022-06-09" +channel = "nightly-2022-07-05" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs index 95a466f27888..2f85653b0631 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAdd/main.rs @@ -6,7 +6,8 @@ #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_xadd, atomic_xadd_acq, atomic_xadd_acqrel, atomic_xadd_rel, atomic_xadd_relaxed, + atomic_xadd_acqrel, atomic_xadd_acquire, atomic_xadd_relaxed, atomic_xadd_release, + atomic_xadd_seqcst, }; #[kani::proof] @@ -27,10 +28,10 @@ fn main() { let c = 1 as u8; unsafe { - let x1 = atomic_xadd(ptr_a1, b); - let x2 = atomic_xadd_acq(ptr_a2, b); + 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_rel(ptr_a4, b); + let x4 = atomic_xadd_release(ptr_a4, b); let x5 = atomic_xadd_relaxed(ptr_a5, b); assert!(x1 == 0); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs index 913b66c72ecd..6be83c2eaa2b 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicAnd/main.rs @@ -1,12 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_and` and other variants (unstable version) return the +// Check that `atomic_and_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_and, atomic_and_acq, atomic_and_acqrel, atomic_and_rel, atomic_and_relaxed, + atomic_and_acqrel, atomic_and_acquire, atomic_and_relaxed, atomic_and_release, + atomic_and_seqcst, }; #[kani::proof] @@ -26,10 +27,10 @@ fn main() { let b = 0 as u8; unsafe { - let x1 = atomic_and(ptr_a1, b); - let x2 = atomic_and_acq(ptr_a2, b); + 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_rel(ptr_a4, b); + let x4 = atomic_and_release(ptr_a4, b); let x5 = atomic_and_relaxed(ptr_a5, b); assert!(x1 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs index 19293b3a9151..898ad26dd514 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs @@ -6,9 +6,9 @@ #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_cxchg, atomic_cxchg_acq, atomic_cxchg_acq_failrelaxed, atomic_cxchg_acqrel, - atomic_cxchg_acqrel_failrelaxed, atomic_cxchg_failacq, atomic_cxchg_failrelaxed, - atomic_cxchg_rel, atomic_cxchg_relaxed, + atomic_cxchg_acqrel_acquire, atomic_cxchg_acqrel_relaxed, atomic_cxchg_acquire_acquire, + atomic_cxchg_acquire_relaxed, atomic_cxchg_relaxed_relaxed, atomic_cxchg_release_relaxed, + atomic_cxchg_seqcst_acquire, atomic_cxchg_seqcst_relaxed, atomic_cxchg_seqcst_seqcst, }; #[kani::proof] @@ -38,15 +38,15 @@ fn main() { // Returns (val, ok) where // * val: the old value // * ok: bool indicating whether the operation was successful or not - let x1 = atomic_cxchg(ptr_a1, 0, 1); - let x2 = atomic_cxchg_acq(ptr_a2, 0, 1); - let x3 = atomic_cxchg_acq_failrelaxed(ptr_a3, 0, 1); - let x4 = atomic_cxchg_acqrel(ptr_a4, 0, 1); - let x5 = atomic_cxchg_acqrel_failrelaxed(ptr_a5, 0, 1); - let x6 = atomic_cxchg_failacq(ptr_a6, 0, 1); - let x7 = atomic_cxchg_failrelaxed(ptr_a7, 0, 1); - let x8 = atomic_cxchg_rel(ptr_a8, 0, 1); - let x9 = atomic_cxchg_relaxed(ptr_a9, 0, 1); + let x1 = atomic_cxchg_seqcst_seqcst(ptr_a1, 0, 1); + let x2 = atomic_cxchg_acquire_acquire(ptr_a2, 0, 1); + let x3 = atomic_cxchg_acquire_relaxed(ptr_a3, 0, 1); + let x4 = atomic_cxchg_acqrel_acquire(ptr_a4, 0, 1); + let x5 = atomic_cxchg_acqrel_relaxed(ptr_a5, 0, 1); + let x6 = atomic_cxchg_seqcst_acquire(ptr_a6, 0, 1); + let x7 = atomic_cxchg_seqcst_relaxed(ptr_a7, 0, 1); + let x8 = atomic_cxchg_release_relaxed(ptr_a8, 0, 1); + let x9 = atomic_cxchg_relaxed_relaxed(ptr_a9, 0, 1); assert!(x1 == (0, true)); assert!(x2 == (0, true)); @@ -58,15 +58,15 @@ fn main() { assert!(x8 == (0, true)); assert!(x9 == (0, true)); - let y1 = atomic_cxchg(ptr_a1, 1, 1); - let y2 = atomic_cxchg_acq(ptr_a2, 1, 1); - let y3 = atomic_cxchg_acq_failrelaxed(ptr_a3, 1, 1); - let y4 = atomic_cxchg_acqrel(ptr_a4, 1, 1); - let y5 = atomic_cxchg_acqrel_failrelaxed(ptr_a5, 1, 1); - let y6 = atomic_cxchg_failacq(ptr_a6, 1, 1); - let y7 = atomic_cxchg_failrelaxed(ptr_a7, 1, 1); - let y8 = atomic_cxchg_rel(ptr_a8, 1, 1); - let y9 = atomic_cxchg_relaxed(ptr_a9, 1, 1); + let y1 = atomic_cxchg_seqcst_seqcst(ptr_a1, 1, 1); + let y2 = atomic_cxchg_acquire_acquire(ptr_a2, 1, 1); + let y3 = atomic_cxchg_acqrel_relaxed(ptr_a3, 1, 1); + let y4 = atomic_cxchg_acqrel_acquire(ptr_a4, 1, 1); + let y5 = atomic_cxchg_acqrel_relaxed(ptr_a5, 1, 1); + let y6 = atomic_cxchg_seqcst_acquire(ptr_a6, 1, 1); + let y7 = atomic_cxchg_seqcst_relaxed(ptr_a7, 1, 1); + let y8 = atomic_cxchg_release_relaxed(ptr_a8, 1, 1); + let y9 = atomic_cxchg_relaxed_relaxed(ptr_a9, 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 e83359b9eefa..f3a615c07c7b 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchgWeak/main.rs @@ -1,14 +1,16 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_cxchgweak` and other variants (unstable version) return +// Check that `atomic_cxchgweak_seqcst` and other variants (unstable version) return // the expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_cxchgweak, atomic_cxchgweak_acq, atomic_cxchgweak_acq_failrelaxed, - atomic_cxchgweak_acqrel, atomic_cxchgweak_acqrel_failrelaxed, atomic_cxchgweak_failacq, - atomic_cxchgweak_failrelaxed, atomic_cxchgweak_rel, atomic_cxchgweak_relaxed, + atomic_cxchgweak_acqrel_acquire, atomic_cxchgweak_acqrel_relaxed, + atomic_cxchgweak_acquire_acquire, atomic_cxchgweak_acquire_relaxed, + atomic_cxchgweak_relaxed_relaxed, atomic_cxchgweak_release_seqcst, + atomic_cxchgweak_seqcst_acquire, atomic_cxchgweak_seqcst_relaxed, + atomic_cxchgweak_seqcst_seqcst, }; #[kani::proof] @@ -38,15 +40,15 @@ fn main() { // Returns (val, ok) where // * val: the old value // * ok: bool indicating whether the operation was successful or not - let x1 = atomic_cxchgweak(ptr_a1, 0, 1); - let x2 = atomic_cxchgweak_acq(ptr_a2, 0, 1); - let x3 = atomic_cxchgweak_acq_failrelaxed(ptr_a3, 0, 1); - let x4 = atomic_cxchgweak_acqrel(ptr_a4, 0, 1); - let x5 = atomic_cxchgweak_acqrel_failrelaxed(ptr_a5, 0, 1); - let x6 = atomic_cxchgweak_failacq(ptr_a6, 0, 1); - let x7 = atomic_cxchgweak_failrelaxed(ptr_a7, 0, 1); - let x8 = atomic_cxchgweak_rel(ptr_a8, 0, 1); - let x9 = atomic_cxchgweak_relaxed(ptr_a9, 0, 1); + let x1 = atomic_cxchgweak_seqcst_seqcst(ptr_a1, 0, 1); + let x2 = atomic_cxchgweak_acquire_acquire(ptr_a2, 0, 1); + let x3 = atomic_cxchgweak_acquire_relaxed(ptr_a3, 0, 1); + let x4 = atomic_cxchgweak_acqrel_acquire(ptr_a4, 0, 1); + let x5 = atomic_cxchgweak_acqrel_relaxed(ptr_a5, 0, 1); + let x6 = atomic_cxchgweak_seqcst_acquire(ptr_a6, 0, 1); + let x7 = atomic_cxchgweak_seqcst_relaxed(ptr_a7, 0, 1); + let x8 = atomic_cxchgweak_release_seqcst(ptr_a8, 0, 1); + let x9 = atomic_cxchgweak_relaxed_relaxed(ptr_a9, 0, 1); assert!(x1 == (0, true)); assert!(x2 == (0, true)); @@ -58,15 +60,15 @@ fn main() { assert!(x8 == (0, true)); assert!(x9 == (0, true)); - let y1 = atomic_cxchgweak(ptr_a1, 1, 1); - let y2 = atomic_cxchgweak_acq(ptr_a2, 1, 1); - let y3 = atomic_cxchgweak_acq_failrelaxed(ptr_a3, 1, 1); - let y4 = atomic_cxchgweak_acqrel(ptr_a4, 1, 1); - let y5 = atomic_cxchgweak_acqrel_failrelaxed(ptr_a5, 1, 1); - let y6 = atomic_cxchgweak_failacq(ptr_a6, 1, 1); - let y7 = atomic_cxchgweak_failrelaxed(ptr_a7, 1, 1); - let y8 = atomic_cxchgweak_rel(ptr_a8, 1, 1); - let y9 = atomic_cxchgweak_relaxed(ptr_a9, 1, 1); + let y1 = atomic_cxchgweak_seqcst_seqcst(ptr_a1, 1, 1); + let y2 = atomic_cxchgweak_acquire_acquire(ptr_a2, 1, 1); + let y3 = atomic_cxchgweak_acquire_relaxed(ptr_a3, 1, 1); + let y4 = atomic_cxchgweak_acqrel_acquire(ptr_a4, 1, 1); + let y5 = atomic_cxchgweak_acqrel_relaxed(ptr_a5, 1, 1); + let y6 = atomic_cxchgweak_seqcst_acquire(ptr_a6, 1, 1); + let y7 = atomic_cxchgweak_seqcst_relaxed(ptr_a7, 1, 1); + let y8 = atomic_cxchgweak_release_seqcst(ptr_a8, 1, 1); + let y9 = atomic_cxchgweak_relaxed_relaxed(ptr_a9, 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 5eb770563819..44cddd82e7dc 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicFence/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicFence/main.rs @@ -5,14 +5,16 @@ // processed. #![feature(core_intrinsics)] -use std::intrinsics::{atomic_fence, atomic_fence_acq, atomic_fence_acqrel, atomic_fence_rel}; +use std::intrinsics::{ + atomic_fence_acqrel, atomic_fence_acquire, atomic_fence_release, atomic_fence_seqcst, +}; #[kani::proof] fn main() { unsafe { - atomic_fence(); - atomic_fence_acq(); + atomic_fence_seqcst(); + atomic_fence_acquire(); atomic_fence_acqrel(); - atomic_fence_rel(); + atomic_fence_release(); } } diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs index f326cdb7c091..b646c8326229 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicLoad/main.rs @@ -1,11 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_load` and other variants (unstable version) return the +// Check that `atomic_load_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{atomic_load, atomic_load_acq, atomic_load_relaxed}; +use std::intrinsics::{atomic_load_acquire, atomic_load_relaxed, atomic_load_seqcst}; #[kani::proof] fn main() { @@ -18,8 +18,8 @@ fn main() { let ptr_a3: *const u8 = &a3; unsafe { - let x1 = atomic_load(ptr_a1); - let x2 = atomic_load_acq(ptr_a2); + let x1 = atomic_load_seqcst(ptr_a1); + let x2 = atomic_load_acquire(ptr_a2); let x3 = atomic_load_relaxed(ptr_a3); assert!(x1 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs index a8fed921ceae..9d5d850fe1c0 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMax/main.rs @@ -1,12 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_max` and other variants (unstable version) return the +// Check that `atomic_max_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_max, atomic_max_acq, atomic_max_acqrel, atomic_max_rel, atomic_max_relaxed, + atomic_max_acqrel, atomic_max_acquire, atomic_max_relaxed, atomic_max_release, + atomic_max_seqcst, }; #[kani::proof] @@ -26,10 +27,10 @@ fn main() { let b = 1 as u8; unsafe { - let x1 = atomic_max(ptr_a1, b); - let x2 = atomic_max_acq(ptr_a2, b); + 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_rel(ptr_a4, b); + let x4 = atomic_max_release(ptr_a4, b); let x5 = atomic_max_relaxed(ptr_a5, b); assert!(x1 == 0); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs index 0091bfb54209..ea9caf5971de 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicMin/main.rs @@ -1,12 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_min` and other variants (unstable version) return the +// Check that `atomic_min_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_min, atomic_min_acq, atomic_min_acqrel, atomic_min_rel, atomic_min_relaxed, + atomic_min_acqrel, atomic_min_acquire, atomic_min_relaxed, atomic_min_release, + atomic_min_seqcst, }; #[kani::proof] @@ -26,10 +27,10 @@ fn main() { let b = 0 as u8; unsafe { - let x1 = atomic_min(ptr_a1, b); - let x2 = atomic_min_acq(ptr_a2, b); + 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_rel(ptr_a4, b); + let x4 = atomic_min_release(ptr_a4, b); let x5 = atomic_min_relaxed(ptr_a5, b); assert!(x1 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs index 342886ca0837..c058dadfd0a1 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicNand/main.rs @@ -1,12 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_nand` and other variants (unstable version) return the +// Check that `atomic_nand_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_nand, atomic_nand_acq, atomic_nand_acqrel, atomic_nand_rel, atomic_nand_relaxed, + atomic_nand_acqrel, atomic_nand_acquire, atomic_nand_relaxed, atomic_nand_release, + atomic_nand_seqcst, }; #[kani::proof] @@ -26,10 +27,10 @@ fn main() { let b = u8::MAX as u8; unsafe { - let x1 = atomic_nand(ptr_a1, b); - let x2 = atomic_nand_acq(ptr_a2, 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_rel(ptr_a4, b); + let x4 = atomic_nand_release(ptr_a4, b); let x5 = atomic_nand_relaxed(ptr_a5, b); assert!(x1 == 0); @@ -44,10 +45,10 @@ fn main() { assert!(*ptr_a4 == b); assert!(*ptr_a5 == b); - let x1 = atomic_nand(ptr_a1, b); - let x2 = atomic_nand_acq(ptr_a2, 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_rel(ptr_a4, b); + let x4 = atomic_nand_release(ptr_a4, b); let x5 = atomic_nand_relaxed(ptr_a5, b); assert!(x1 == b); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs index ce2332458d4f..4f21e7dc7a77 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs @@ -1,12 +1,12 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT +// Copyright Kani Contributor_seqcsts +// SPDX-License-Identifier: Apache-2.0 OR_seqcst MIT -// Check that `atomic_or` and other variants (unstable version) return the +// Check that `atomic_or_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_or, atomic_or_acq, atomic_or_acqrel, atomic_or_rel, atomic_or_relaxed, + atomic_or_acqrel, atomic_or_acquire, atomic_or_relaxed, atomic_or_release, atomic_or_seqcst, }; #[kani::proof] @@ -27,10 +27,10 @@ fn main() { let c = 1 as u8; unsafe { - let x1 = atomic_or(ptr_a1, b); - let x2 = atomic_or_acq(ptr_a2, b); + 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_rel(ptr_a4, b); + let x4 = atomic_or_release(ptr_a4, b); let x5 = atomic_or_relaxed(ptr_a5, b); assert!(x1 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs index d2367f987498..1b5b7df8bd34 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSingleThreadFence/main.rs @@ -1,21 +1,21 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_singlethreadfence` and other variants (unstable version) +// Check that `atomic_singlethreadfence_seqcst` and other variants (unstable version) // can be processed. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_singlethreadfence, atomic_singlethreadfence_acq, atomic_singlethreadfence_acqrel, - atomic_singlethreadfence_rel, + atomic_singlethreadfence_acqrel, atomic_singlethreadfence_acquire, + atomic_singlethreadfence_release, atomic_singlethreadfence_seqcst, }; #[kani::proof] fn main() { unsafe { - atomic_singlethreadfence(); - atomic_singlethreadfence_acq(); + atomic_singlethreadfence_seqcst(); + atomic_singlethreadfence_acquire(); atomic_singlethreadfence_acqrel(); - atomic_singlethreadfence_rel(); + atomic_singlethreadfence_release(); } } diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs index 815076381719..fd73c1c863eb 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicStore/main.rs @@ -1,11 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_store` and other variants (unstable version) return the +// Check that `atomic_store_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] -use std::intrinsics::{atomic_store, atomic_store_rel, atomic_store_relaxed}; +use std::intrinsics::{atomic_store_relaxed, atomic_store_release, atomic_store_seqcst}; #[kani::proof] fn main() { @@ -18,8 +18,8 @@ fn main() { let ptr_a3: *mut u8 = &mut a3; unsafe { - atomic_store(ptr_a1, 0); - atomic_store_rel(ptr_a2, 0); + atomic_store_seqcst(ptr_a1, 0); + atomic_store_release(ptr_a2, 0); atomic_store_relaxed(ptr_a3, 0); assert!(*ptr_a1 == 0); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs index 474dae07ca23..3f205068948c 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicSub/main.rs @@ -1,12 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_xsub` and other variants (unstable version) return the +// Check that `atomic_xsub_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_xsub, atomic_xsub_acq, atomic_xsub_acqrel, atomic_xsub_rel, atomic_xsub_relaxed, + atomic_xsub_acqrel, atomic_xsub_acquire, atomic_xsub_relaxed, atomic_xsub_release, + atomic_xsub_seqcst, }; #[kani::proof] @@ -27,10 +28,10 @@ fn main() { let c = 0 as u8; unsafe { - let x1 = atomic_xsub(ptr_a1, b); - let x2 = atomic_xsub_acq(ptr_a2, b); + 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_rel(ptr_a4, b); + let x4 = atomic_xsub_release(ptr_a4, b); let x5 = atomic_xsub_relaxed(ptr_a5, b); assert!(x1 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs index be35b59ad2b7..ee05691da839 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmax/main.rs @@ -1,12 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_umax` and other variants (unstable version) return the +// Check that `atomic_umax_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_umax, atomic_umax_acq, atomic_umax_acqrel, atomic_umax_rel, atomic_umax_relaxed, + atomic_umax_acqrel, atomic_umax_acquire, atomic_umax_relaxed, atomic_umax_release, + atomic_umax_seqcst, }; #[kani::proof] @@ -26,10 +27,10 @@ fn main() { let b = 1 as u8; unsafe { - let x1 = atomic_umax(ptr_a1, b); - let x2 = atomic_umax_acq(ptr_a2, b); + 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_rel(ptr_a4, b); + let x4 = atomic_umax_release(ptr_a4, b); let x5 = atomic_umax_relaxed(ptr_a5, b); assert!(x1 == 0); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs index 032413a1b64c..69aea2493c85 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicUmin/main.rs @@ -1,12 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_umin` and other variants (unstable version) return the +// Check that `atomic_umin_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_umin, atomic_umin_acq, atomic_umin_acqrel, atomic_umin_rel, atomic_umin_relaxed, + atomic_umin_acqrel, atomic_umin_acquire, atomic_umin_relaxed, atomic_umin_release, + atomic_umin_seqcst, }; #[kani::proof] @@ -26,10 +27,10 @@ fn main() { let b = 0 as u8; unsafe { - let x1 = atomic_umin(ptr_a1, b); - let x2 = atomic_umin_acq(ptr_a2, b); + 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_rel(ptr_a4, b); + let x4 = atomic_umin_release(ptr_a4, b); let x5 = atomic_umin_relaxed(ptr_a5, b); assert!(x1 == 1); diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs index 28f75728b7bf..e91027f61b5a 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXchg/main.rs @@ -1,12 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_xchg` and other variants (unstable version) return the +// Check that `atomic_xchg_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_xchg, atomic_xchg_acq, atomic_xchg_acqrel, atomic_xchg_rel, atomic_xchg_relaxed, + atomic_xchg_acqrel, atomic_xchg_acquire, atomic_xchg_relaxed, atomic_xchg_release, + atomic_xchg_seqcst, }; #[kani::proof] @@ -28,14 +29,14 @@ fn main() { // Returns (val, ok) where // * val: the old value // * ok: bool indicating whether the operation was successful or not - assert!(atomic_xchg(ptr_a1, 1) == 0); - assert!(atomic_xchg(ptr_a1, 0) == 1); - assert!(atomic_xchg_acq(ptr_a2, 1) == 0); - assert!(atomic_xchg_acq(ptr_a2, 0) == 1); + 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_rel(ptr_a4, 1) == 0); - assert!(atomic_xchg_rel(ptr_a4, 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); } diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs index 2ca0f05760ce..e9953aa7852d 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicXor/main.rs @@ -1,12 +1,13 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `atomic_xor` and other variants (unstable version) return the +// Check that `atomic_xor_seqcst` and other variants (unstable version) return the // expected result. #![feature(core_intrinsics)] use std::intrinsics::{ - atomic_xor, atomic_xor_acq, atomic_xor_acqrel, atomic_xor_rel, atomic_xor_relaxed, + atomic_xor_acqrel, atomic_xor_acquire, atomic_xor_relaxed, atomic_xor_release, + atomic_xor_seqcst, }; #[kani::proof] @@ -26,10 +27,10 @@ fn main() { let b = 1 as u8; unsafe { - let x1 = atomic_xor(ptr_a1, b); - let x2 = atomic_xor_acq(ptr_a2, b); + 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_rel(ptr_a4, b); + let x4 = atomic_xor_release(ptr_a4, b); let x5 = atomic_xor_relaxed(ptr_a5, b); assert!(x1 == 1); diff --git a/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs index a9c0d3a5eb9a..047c6bc2de60 100644 --- a/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs +++ b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs @@ -6,6 +6,7 @@ use std::ptr; #[kani::proof] +#[kani::unwind(17)] fn test_append() { let mut a = vec!['r']; let mut b = vec!['u', 's', 't']; diff --git a/tests/kani/Refs/main.rs b/tests/kani/Refs/main.rs index a93e3f40f082..bfac8efb4aef 100644 --- a/tests/kani/Refs/main.rs +++ b/tests/kani/Refs/main.rs @@ -80,6 +80,7 @@ impl<'a> ArgParser<'a> { } #[kani::proof] +#[kani::unwind(2)] fn main() { let a: ArgParser = ArgParser { arguments: BTreeMap::new() }; a.format_arguments(); diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected index 6179fa7c8d96..3dc32e899534 100644 --- a/tests/ui/code-location/expected +++ b/tests/ui/code-location/expected @@ -1,7 +1,7 @@ module/mod.rs:10:5 in function module::not_empty main.rs:13:5 in function same_file /toolchains/ -alloc/src/vec/mod.rs:2888:81 in function as std::ops::Drop>::drop +alloc/src/vec/mod.rs:2920:81 in function as std::ops::Drop>::drop VERIFICATION:- SUCCESSFUL From 71b1188cc8beba8ea4029f0ea4da6711a80339d7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 5 Jul 2022 23:16:45 -0700 Subject: [PATCH 2/4] Codegen unimplemented for unsupported constant slices See https://github.com/model-checking/kani/issues/1339 for more details. --- .../src/codegen_cprover_gotoc/codegen/operand.rs | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index da7c953c493c..15975bf1ee54 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -105,8 +105,6 @@ impl<'tcx> GotocCtx<'tcx> { ty::Slice(slice_ty) => { if let Uint(UintTy::U8) = slice_ty.kind() { // The case where we have a slice of u8 is easy enough: make an array of u8 - // TODO: Handle cases with larger int types by making an array of bytes, - // then using byte-extract on it. let slice = data.inspect_with_uninit_and_ptr_outside_interpreter(start..end); let vec_of_bytes: Vec = slice @@ -124,6 +122,16 @@ impl<'tcx> GotocCtx<'tcx> { len_expr, &self.symbol_table, ); + } else { + // TODO: Handle cases with other types such as tuples and larger integers. + let loc = span.map_or(Location::none(), |s| self.codegen_span(s)); + let typ = self.codegen_ty(lit_ty); + return self.codegen_unimplemented( + "Constant slice value with 2+ bytes", + typ, + loc, + "https://github.com/model-checking/kani/issues/1339", + ); } } _ => {} From 9f17da99f39eba51144bf985eb1076810249a207 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 6 Jul 2022 10:33:01 -0700 Subject: [PATCH 3/4] Fix copyright check --- tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs b/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs index 4f21e7dc7a77..9eba4396b560 100644 --- a/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs +++ b/tests/kani/Intrinsics/Atomic/Unstable/AtomicOr/main.rs @@ -1,5 +1,5 @@ -// Copyright Kani Contributor_seqcsts -// SPDX-License-Identifier: Apache-2.0 OR_seqcst MIT +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT // Check that `atomic_or_seqcst` and other variants (unstable version) return the // expected result. From 6134f1d687727d03163dc24b85901edabb39a1c4 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 6 Jul 2022 13:03:22 -0700 Subject: [PATCH 4/4] Use codegen_option_span instead --- kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 15975bf1ee54..83e759f87c61 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -124,7 +124,7 @@ impl<'tcx> GotocCtx<'tcx> { ); } else { // TODO: Handle cases with other types such as tuples and larger integers. - let loc = span.map_or(Location::none(), |s| self.codegen_span(s)); + let loc = self.codegen_span_option(span.cloned()); let typ = self.codegen_ty(lit_ty); return self.codegen_unimplemented( "Constant slice value with 2+ bytes",