From 477fe788caba5d3c63197771078fdd31715ef516 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Mon, 11 Mar 2024 14:50:28 -0700 Subject: [PATCH] Upgrade toolchain to 2024-03-11 --- .../codegen/intrinsic.rs | 19 +++++++++++++++++++ .../codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 6 ++++++ .../compiler_interface.rs | 2 +- kani-compiler/src/kani_middle/attributes.rs | 7 +++---- kani-compiler/src/kani_middle/intrinsics.rs | 8 ++++---- rust-toolchain.toml | 2 +- tests/coverage/unreachable/variant/expected | 2 +- 8 files changed, 36 insertions(+), 12 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 20e3f34f48bf..2cabc4cfd273 100644 --- 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, + 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 index 3df6d807aaea..5867448d9973 100644 --- 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 index 57af958abf41..089d871d22b4 100644 --- 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: + 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: + 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 index 91e6c2538195..cad8bcbfb9ce 100644 --- 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 index 621107acd13e..df494d7daa3c 100644 --- 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 index 404cb0f277c3..51e6140b7e1a 100644 --- 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 index 747a9f2f5295..b6f6e8a63534 100644 --- 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 index 08a2f824da83..8fa3ec8b870f 100644 --- 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