Update toolchain to 2022-07-05

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<String> {
-        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<File>),
             Gnu(ar::GnuBuilder<File>),
@@ -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(

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

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()
                 )
             }
         }
@@ -104,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<Expr> = slice
@@ -123,12 +122,22 @@ 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",
+                        );
                     }
                 }
                 _ => {}
             }
         }
-        unimplemented!("\nv {:?}\nlit_ty {:?}\nspan {:?}", v, lit_ty, span);
+        unimplemented!("\nv {:?}\nlit_ty {:?}\nspan {:?}", v, lit_ty.kind(), span);
     }
 
     pub fn codegen_const_value(

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());

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<String>, Option<Locat
 
 pub fn init() {
     // Install panic hook
-    SyncLazy::force(&DEFAULT_HOOK); // Install ice hook
+    LazyLock::force(&DEFAULT_HOOK); // Install ice hook
 }
 
 // Custom panic hook to add more information when panic occurs during goto-c codegen.
-static DEFAULT_HOOK: SyncLazy<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
-    SyncLazy::new(|| {
+static DEFAULT_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + 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

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<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
-    SyncLazy::new(|| {
+static PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + 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
 }

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"]

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);

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);