Upgrade toolchain to 2024-03-11

model-checking · Mar 11, 2024 · 0a371ce · 0a371ce
1 parent a8db120
commit 0a371ce
Show file tree

Hide file tree

Showing 9 changed files with 37 additions and 13 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -474,6 +474,11 @@ impl<'tcx> GotocCtx<'tcx> {
                 let binop_stmt = codegen_intrinsic_binop!(sub);
                 self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
             }
+            "is_val_statically_known" => {
+                // Returning false is sound according do this intrinsic's documentation:
+                // https://doc.rust-lang.org/nightly/std/intrinsics/fn.is_val_statically_known.html
+                self.codegen_expr_to_place_stable(place, Expr::c_false())
+            }
             "likely" => self.codegen_expr_to_place_stable(place, fargs.remove(0)),
             "log10f32" => unstable_codegen!(codegen_simple_intrinsic!(Log10f)),
             "log10f64" => unstable_codegen!(codegen_simple_intrinsic!(Log10)),
@@ -506,6 +511,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc),
             "ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, place, loc),
             "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
+            "retag_box_to_raw" => self.codegen_retag_box_to_raw(fargs, place, loc),
             "rintf32" => codegen_simple_intrinsic!(Rintf),
             "rintf64" => codegen_simple_intrinsic!(Rint),
             "rotate_left" => codegen_intrinsic_binop!(rol),
@@ -1259,6 +1265,19 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_expr_to_place_stable(p, e)
     }
 
+    // This is an operation that is primarily relevant for stacked borrow
+    // checks.  For Kani, we simply return the pointer.
+    fn codegen_retag_box_to_raw(
+        &mut self,
+        mut fargs: Vec<Expr>,
+        p: &Place,
+        _loc: Location,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 1, "raw_box_to_box expected one argument");
+        let arg = fargs.remove(0);
+        self.codegen_expr_to_place_stable(p, arg)
+    }
+
     fn vtable_info(
         &mut self,
         info: VTableInfo,

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -725,7 +725,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             .bytes(),
                         Type::size_t(),
                     ),
-                    NullOp::DebugAssertions => Expr::c_false(),
+                    NullOp::UbCheck(_) => Expr::c_false(),
                 }
             }
             Rvalue::ShallowInitBox(ref operand, content_ty) => {

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -542,6 +542,9 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Float(k) => match k {
                 FloatTy::F32 => Type::float(),
                 FloatTy::F64 => Type::double(),
+                // `F16` and `F128` are not yet handled.
+                // Tracked here: <https://github.com/model-checking/kani/issues/3069>
+                FloatTy::F16 | FloatTy::F128 => unimplemented!(),
             },
             ty::Adt(def, _) if def.repr().simd() => self.codegen_vector(ty),
             ty::Adt(def, subst) => {
@@ -1346,6 +1349,9 @@ impl<'tcx> GotocCtx<'tcx> {
 
             Primitive::F32 => self.tcx.types.f32,
             Primitive::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,
                 ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not },

diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -397,7 +397,7 @@ impl CodegenBackend for GotocCodegenBackend {
                 let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps);
                 let (metadata, _metadata_position) = create_wrapper_file(
                     sess,
-                    b".rmeta".to_vec(),
+                    ".rmeta".to_string(),
                     codegen_results.metadata.raw_data(),
                 );
                 let metadata = emit_wrapper_file(sess, &metadata, &path, METADATA_FILENAME);

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
@@ -611,9 +611,8 @@ fn parse_modify_values<'a>(
     let mut iter = t.trees();
     std::iter::from_fn(move || {
         let tree = iter.next()?;
-        let wrong_token_err = || {
-            tcx.sess.parse_sess.dcx.span_err(tree.span(), "Unexpected token. Expected identifier.")
-        };
+        let wrong_token_err =
+            || tcx.sess.psess.dcx.span_err(tree.span(), "Unexpected token. Expected identifier.");
         let result = match tree {
             TokenTree::Token(token, _) => {
                 if let TokenKind::Ident(id, _) = &token.kind {
@@ -640,7 +639,7 @@ fn parse_modify_values<'a>(
         match iter.next() {
             None | Some(comma_tok!()) => (),
             Some(not_comma) => {
-                tcx.sess.parse_sess.dcx.span_err(
+                tcx.sess.psess.dcx.span_err(
                     not_comma.span(),
                     "Unexpected token, expected end of attribute or comma",
                 );

diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs
@@ -6,7 +6,7 @@ use rustc_index::IndexVec;
 use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, TerminatorKind};
 use rustc_middle::mir::{Local, LocalDecl};
 use rustc_middle::ty::{self, Ty, TyCtxt};
-use rustc_middle::ty::{Const, GenericArgsRef};
+use rustc_middle::ty::{Const, GenericArgsRef, IntrinsicDef};
 use rustc_span::source_map::Spanned;
 use rustc_span::symbol::{sym, Symbol};
 use tracing::{debug, trace};
@@ -33,8 +33,8 @@ impl<'tcx> ModelIntrinsics<'tcx> {
             let terminator = block.terminator_mut();
             if let TerminatorKind::Call { func, args, .. } = &mut terminator.kind {
                 let func_ty = func.ty(&self.local_decls, self.tcx);
-                if let Some((intrinsic_name, generics)) = resolve_rust_intrinsic(self.tcx, func_ty)
-                {
+                if let Some((intrinsic, generics)) = resolve_rust_intrinsic(self.tcx, func_ty) {
+                    let intrinsic_name = intrinsic.name;
                     trace!(?func, ?intrinsic_name, "run_pass");
                     if intrinsic_name == sym::simd_bitmask {
                         self.replace_simd_bitmask(func, args, generics)
@@ -99,7 +99,7 @@ fn simd_len_and_type<'tcx>(tcx: TyCtxt<'tcx>, simd_ty: Ty<'tcx>) -> (Const<'tcx>
 fn resolve_rust_intrinsic<'tcx>(
     tcx: TyCtxt<'tcx>,
     func_ty: Ty<'tcx>,
-) -> Option<(Symbol, GenericArgsRef<'tcx>)> {
+) -> Option<(IntrinsicDef, GenericArgsRef<'tcx>)> {
     if let ty::FnDef(def_id, args) = *func_ty.kind() {
         if let Some(symbol) = tcx.intrinsic(def_id) {
             return Some((symbol, args));

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-03-01"
+channel = "nightly-2024-03-11"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/coverage/unreachable/variant/expected b/tests/coverage/unreachable/variant/expected
@@ -1,4 +1,4 @@
-coverage/unreachable/variant/main.rs, 15, PARTIAL
+coverage/unreachable/variant/main.rs, 15, FULL
 coverage/unreachable/variant/main.rs, 16, NONE
 coverage/unreachable/variant/main.rs, 17, NONE
 coverage/unreachable/variant/main.rs, 18, FULL

diff --git a/tools/bookrunner/librustdoc/html/markdown.rs b/tools/bookrunner/librustdoc/html/markdown.rs
@@ -225,7 +225,7 @@ impl LangString {
         let mut data = LangString::default();
         let mut ignores = vec![];
 
-        data.original = string.to_owned();
+        string.clone_into(&mut data.original);
 
         for token in Self::tokens(string) {
             match token {