Upgrade toolchain to 2024-05-14

cprover_bindings/src/goto_program/expr.rs

@@ -1331,11 +1331,11 @@ impl Expr {
     fn unop_return_type(op: UnaryOperator, arg: &Expr) -> Type {
         match op {
             Bitnot | BitReverse | Bswap | UnaryMinus => arg.typ.clone(),
-            CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.clone(),
+            CountLeadingZeros { .. } | CountTrailingZeros { .. } => Type::unsigned_int(32),
             ObjectSize | PointerObject => Type::size_t(),
             PointerOffset => Type::ssize_t(),
             IsDynamicObject | IsFinite | Not => Type::bool(),
-            Popcount => arg.typ.clone(),
+            Popcount => Type::unsigned_int(32),
         }
     }
     /// Private helper function to make unary operators

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -18,7 +18,7 @@ use rustc_middle::ty::{List, TypeFoldable};
 use rustc_smir::rustc_internal;
 use rustc_span::def_id::DefId;
 use rustc_target::abi::{
-    Abi::Vector, FieldIdx, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding,
+    Abi::Vector, FieldIdx, FieldsShape, Float, Integer, LayoutS, Primitive, Size, TagEncoding,
     TyAndLayout, VariantIdx, Variants,
 };
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
@@ -1354,13 +1354,18 @@ impl<'tcx> GotocCtx<'tcx> {
                     }
                 }
             },
+            Primitive::Float(f) => self.codegen_float_type(f),
+            Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
+        }
+    }
 
-            Primitive::F32 => self.tcx.types.f32,
-            Primitive::F64 => self.tcx.types.f64,
+    pub fn codegen_float_type(&self, f: Float) -> Ty<'tcx> {
+        match f {
+            Float::F32 => self.tcx.types.f32,
+            Float::F64 => self.tcx.types.f64,
             // `F16` and `F128` are not yet handled.
             // Tracked here: <https://github.com/model-checking/kani/issues/3069>
-            Primitive::F16 | Primitive::F128 => unimplemented!(),
-            Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
+            Float::F16 | Float::F128 => unimplemented!(),
         }
     }
 
@@ -1672,7 +1677,7 @@ pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
 /// Extracts the pointee type if the given mir type is either a known smart pointer (Box, Rc, ..)
 /// or a regular pointer.
 pub fn std_pointee_type(mir_type: Ty) -> Option<Ty> {
-    mir_type.builtin_deref(true).map(|tm| tm.ty)
+    mir_type.builtin_deref(true)
 }
 
 /// This is a place holder function that should normalize the given type.

kani-compiler/src/kani_middle/coercion.rs

@@ -16,8 +16,8 @@
 use rustc_hir::lang_items::LangItem;
 use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
+use rustc_middle::ty::TraitRef;
 use rustc_middle::ty::{ParamEnv, Ty, TyCtxt};
-use rustc_middle::ty::{TraitRef, TypeAndMut};
 use rustc_smir::rustc_internal;
 use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
 use stable_mir::Symbol;
@@ -263,5 +263,5 @@ fn custom_coerce_unsize_info<'tcx>(
 
 /// Extract pointee type from builtin pointer types.
 fn extract_pointee(tcx: TyCtxt<'_>, typ: TyStable) -> Option<Ty<'_>> {
-    rustc_internal::internal(tcx, typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
+    rustc_internal::internal(tcx, typ).builtin_deref(true)
 }

library/kani_macros/build.rs

@@ -0,0 +1,7 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+fn main() {
+    // Make sure `kani_sysroot` is a recognized config
+    println!("cargo::rustc-check-cfg=cfg(kani_sysroot)");
+}

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-04-22"
+channel = "nightly-2024-05-14"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/coroutines/as_parameter/main.rs

@@ -21,8 +21,11 @@ where
 
 #[kani::proof]
 fn main() {
-    foo(|| {
-        yield 1;
-        return 2;
-    });
+    foo(
+        #[coroutine]
+        || {
+            yield 1;
+            return 2;
+        },
+    );
 }

tests/expected/coroutines/main.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
@@ -10,7 +11,8 @@ use std::pin::Pin;
 #[kani::unwind(2)]
 fn main() {
     let val: bool = kani::any();
-    let mut coroutine = move || {
+    let mut coroutine = #[coroutine]
+    move || {
         let x = val;
         yield x;
         return !x;

tests/expected/coroutines/pin/main.rs

@@ -5,13 +5,15 @@
 // from https://github.com/model-checking/kani/issues/416
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
-    let mut coroutine = || {
+    let mut coroutine = #[coroutine]
+    || {
         yield 1;
         return true;
     };

tests/kani/Coroutines/main.rs

@@ -4,14 +4,16 @@
 // This tests that coroutines work, even with a non-() resume type.
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::{Coroutine, CoroutineState};
 use std::pin::Pin;
 
 #[kani::proof]
 #[kani::unwind(3)]
 fn main() {
-    let mut add_one = |mut resume: u8| {
+    let mut add_one = #[coroutine]
+    |mut resume: u8| {
         loop {
             resume = yield resume.saturating_add(1);
         }

tests/kani/Coroutines/rustc-coroutine-tests/conditional-drop.rs

@@ -12,6 +12,7 @@
 //[nomiropt]compile-flags: -Z mir-opt-level=0
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::Coroutine;
 use std::pin::Pin;
@@ -41,7 +42,8 @@ fn main() {
 }
 
 fn t1() {
-    let mut a = || {
+    let mut a = #[coroutine]
+    || {
         let b = B;
         if test() {
             drop(b);
@@ -57,7 +59,8 @@ fn t1() {
 }
 
 fn t2() {
-    let mut a = || {
+    let mut a = #[coroutine]
+    || {
         let b = B;
         if test2() {
             drop(b);

tests/kani/Coroutines/rustc-coroutine-tests/control-flow.rs

@@ -35,32 +35,52 @@ where
 #[kani::proof]
 #[kani::unwind(16)]
 fn main() {
-    finish(1, || yield);
-    finish(8, || {
-        for _ in 0..8 {
-            yield;
-        }
-    });
-    finish(1, || {
-        if true {
-            yield;
-        } else {
-        }
-    });
-    finish(1, || {
-        if false {
-        } else {
-            yield;
-        }
-    });
-    finish(2, || {
-        if {
-            yield;
-            false
-        } {
-            yield;
-            panic!()
-        }
-        yield
-    });
+    finish(
+        1,
+        #[coroutine]
+        || yield,
+    );
+    finish(
+        8,
+        #[coroutine]
+        || {
+            for _ in 0..8 {
+                yield;
+            }
+        },
+    );
+    finish(
+        1,
+        #[coroutine]
+        || {
+            if true {
+                yield;
+            } else {
+            }
+        },
+    );
+    finish(
+        1,
+        #[coroutine]
+        || {
+            if false {
+            } else {
+                yield;
+            }
+        },
+    );
+    finish(
+        2,
+        #[coroutine]
+        || {
+            if {
+                yield;
+                false
+            } {
+                yield;
+                panic!()
+            }
+            yield
+        },
+    );
 }

tests/kani/Coroutines/rustc-coroutine-tests/env-drop.rs

@@ -12,6 +12,7 @@
 //[nomiropt]compile-flags: -Z mir-opt-level=0
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::Coroutine;
 use std::pin::Pin;
@@ -36,7 +37,8 @@ fn main() {
 
 fn t1() {
     let b = B;
-    let mut foo = || {
+    let mut foo = #[coroutine]
+    || {
         yield;
         drop(b);
     };
@@ -50,7 +52,8 @@ fn t1() {
 
 fn t2() {
     let b = B;
-    let mut foo = || {
+    let mut foo = #[coroutine]
+    || {
         yield b;
     };
 
@@ -63,7 +66,8 @@ fn t2() {
 
 fn t3() {
     let b = B;
-    let foo = || {
+    let foo = #[coroutine]
+    || {
         yield;
         drop(b);
     };

tests/kani/Coroutines/rustc-coroutine-tests/iterator-count.rs

@@ -30,6 +30,7 @@ impl<T: Coroutine<(), Return = ()> + Unpin> Iterator for W<T> {
 }
 
 fn test() -> impl Coroutine<(), Return = (), Yield = u8> + Unpin {
+    #[coroutine]
     || {
         for i in 1..6 {
             yield i
@@ -43,6 +44,7 @@ fn main() {
     let end = 11;
 
     let closure_test = |start| {
+        #[coroutine]
         move || {
             for i in start..end {
                 yield i

tests/kani/Coroutines/rustc-coroutine-tests/live-upvar-across-yield.rs

@@ -9,14 +9,16 @@
 // run-pass
 
 #![feature(coroutines, coroutine_trait)]
+#![feature(stmt_expr_attributes)]
 
 use std::ops::Coroutine;
 use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
     let b = |_| 3;
-    let mut a = || {
+    let mut a = #[coroutine]
+    || {
         b(yield);
     };
     Pin::new(&mut a).resume(());

tests/kani/Coroutines/rustc-coroutine-tests/moved-locals-size.rs

@@ -41,6 +41,7 @@ impl Drop for Foo {
 }
 
 fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let first = Foo([0; FOO_SIZE]);
         let _second = first;
@@ -52,6 +53,7 @@ fn move_before_yield() -> impl Coroutine<Yield = (), Return = ()> {
 fn noop() {}
 
 fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let first = Foo([0; FOO_SIZE]);
         noop();
@@ -64,6 +66,7 @@ fn move_before_yield_with_noop() -> impl Coroutine<Yield = (), Return = ()> {
 // Today we don't have NRVO (we allocate space for both `first` and `second`,)
 // but we can overlap `first` with `_third`.
 fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let first = Foo([0; FOO_SIZE]);
         yield;
@@ -75,6 +78,7 @@ fn overlap_move_points() -> impl Coroutine<Yield = (), Return = ()> {
 }
 
 fn overlap_x_and_y() -> impl Coroutine<Yield = (), Return = ()> {
+    #[coroutine]
     static || {
         let x = Foo([0; FOO_SIZE]);
         yield;