From f8fabc4c6e08d2a8e28a39f316c54e8342d9c77e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 7 Feb 2024 19:07:40 -0800 Subject: [PATCH] Upgrade Rust toolchain to nightly-2024-01-23 (#2983) Related PRs so far: - https://github.com/rust-lang/rust/pull/119869 - https://github.com/rust-lang/rust/pull/120080 - https://github.com/rust-lang/rust/pull/120128 - https://github.com/rust-lang/rust/pull/119369 - https://github.com/rust-lang/rust/pull/116672 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Signed-off-by: Felipe R. Monteiro Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> Co-authored-by: tautschnig Co-authored-by: Qinheping Hu Co-authored-by: Michael Tautschnig Co-authored-by: Felipe R. Monteiro --- .../codegen_cprover_gotoc/codegen/contract.rs | 2 +- .../codegen/intrinsic.rs | 50 ++++++++++--------- .../codegen_cprover_gotoc/codegen/place.rs | 9 ++-- .../codegen_cprover_gotoc/codegen/rvalue.rs | 17 ++++--- .../src/codegen_cprover_gotoc/codegen/span.rs | 2 +- .../codegen/statement.rs | 8 +-- .../codegen/ty_stable.rs | 40 +++++++-------- .../src/codegen_cprover_gotoc/codegen/typ.rs | 4 +- .../compiler_interface.rs | 2 +- .../context/current_fn.rs | 19 ++++--- .../codegen_cprover_gotoc/overrides/hooks.rs | 4 +- .../src/codegen_cprover_gotoc/utils/utils.rs | 2 +- kani-compiler/src/kani_middle/attributes.rs | 10 ++-- kani-compiler/src/kani_middle/coercion.rs | 18 +++---- kani-compiler/src/kani_middle/mod.rs | 10 ++-- kani-compiler/src/kani_middle/reachability.rs | 20 ++++---- kani-compiler/src/kani_middle/resolve.rs | 9 ++-- kani-compiler/src/kani_middle/stubbing/mod.rs | 8 +-- .../src/sysroot/contracts/bootstrap.rs | 2 +- rust-toolchain.toml | 2 +- .../Intrinsics/AlignOfVal/align_of_basic.rs | 4 +- .../Intrinsics/AlignOfVal/align_of_fat_ptr.rs | 2 +- .../kani/Intrinsics/ConstEval/min_align_of.rs | 4 +- .../Intrinsics/ConstEval/pref_align_of.rs | 4 +- tests/perf/hashset/expected | 2 +- tests/perf/hashset/src/lib.rs | 42 ++++++++-------- 26 files changed, 157 insertions(+), 139 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 964286984fc6..2bd3e1ff7c35 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -39,7 +39,7 @@ impl<'tcx> GotocCtx<'tcx> { let mut instance_under_contract = items.iter().filter_map(|i| match i { MonoItem::Fn(instance @ Instance { def, .. }) - if wrapped_fn == rustc_internal::internal(def.def_id()) => + if wrapped_fn == rustc_internal::internal(tcx, def.def_id()) => { Some(*instance) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 0709682afa65..6c711e3d20e4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -3,7 +3,7 @@ //! this module handles intrinsics use super::typ; use super::{bb_label, PropertyClass}; -use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type_stable, pretty_ty}; +use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; use crate::codegen_cprover_gotoc::{utils, GotocCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{ @@ -646,7 +646,7 @@ impl<'tcx> GotocCtx<'tcx> { span, format!( "Type check failed for intrinsic `{name}`: Expected {expected}, found {}", - pretty_ty(actual) + self.pretty_ty(actual) ), ); self.tcx.dcx().abort_if_errors(); @@ -779,12 +779,16 @@ impl<'tcx> GotocCtx<'tcx> { if layout.abi.is_uninhabited() { return self.codegen_fatal_error( PropertyClass::SafetyCheck, - &format!("attempted to instantiate uninhabited type `{}`", pretty_ty(*target_ty)), + &format!( + "attempted to instantiate uninhabited type `{}`", + self.pretty_ty(*target_ty) + ), span, ); } - let param_env_and_type = ParamEnv::reveal_all().and(rustc_internal::internal(target_ty)); + let param_env_and_type = + ParamEnv::reveal_all().and(rustc_internal::internal(self.tcx, target_ty)); // Then we check if the type allows "raw" initialization for the cases // where memory is zero-initialized or entirely uninitialized @@ -798,7 +802,7 @@ impl<'tcx> GotocCtx<'tcx> { PropertyClass::SafetyCheck, &format!( "attempted to zero-initialize type `{}`, which is invalid", - pretty_ty(*target_ty) + self.pretty_ty(*target_ty) ), span, ); @@ -817,7 +821,7 @@ impl<'tcx> GotocCtx<'tcx> { PropertyClass::SafetyCheck, &format!( "attempted to leave type `{}` uninitialized, which is invalid", - pretty_ty(*target_ty) + self.pretty_ty(*target_ty) ), span, ); @@ -1285,7 +1289,7 @@ impl<'tcx> GotocCtx<'tcx> { _ => { let err_msg = format!( "simd_shuffle index must be an array of `u32`, got `{}`", - pretty_ty(farg_types[2]) + self.pretty_ty(farg_types[2]) ); utils::span_err(self.tcx, span, err_msg); // Return a dummy value @@ -1378,7 +1382,7 @@ impl<'tcx> GotocCtx<'tcx> { // Packed types ignore the alignment of their fields. if let TyKind::RigidTy(RigidTy::Adt(def, _)) = ty.kind() { - if rustc_internal::internal(def).repr().packed() { + if rustc_internal::internal(self.tcx, def).repr().packed() { unsized_align = sized_align.clone(); } } @@ -1426,9 +1430,9 @@ impl<'tcx> GotocCtx<'tcx> { if rust_ret_type != vector_base_type { let err_msg = format!( "expected return type `{}` (element of input `{}`), found `{}`", - pretty_ty(vector_base_type), - pretty_ty(rust_arg_types[0]), - pretty_ty(rust_ret_type) + self.pretty_ty(vector_base_type), + self.pretty_ty(rust_arg_types[0]), + self.pretty_ty(rust_ret_type) ); utils::span_err(self.tcx, span, err_msg); } @@ -1466,9 +1470,9 @@ impl<'tcx> GotocCtx<'tcx> { if vector_base_type != rust_arg_types[2] { let err_msg = format!( "expected inserted type `{}` (element of input `{}`), found `{}`", - pretty_ty(vector_base_type), - pretty_ty(rust_arg_types[0]), - pretty_ty(rust_arg_types[2]), + self.pretty_ty(vector_base_type), + self.pretty_ty(rust_arg_types[0]), + self.pretty_ty(rust_arg_types[2]), ); utils::span_err(self.tcx, span, err_msg); } @@ -1534,8 +1538,8 @@ impl<'tcx> GotocCtx<'tcx> { "expected return type with length {} (same as input type `{}`), \ found `{}` with length {}", arg1.typ().len().unwrap(), - pretty_ty(rust_arg_types[0]), - pretty_ty(rust_ret_type), + self.pretty_ty(rust_arg_types[0]), + self.pretty_ty(rust_ret_type), ret_typ.len().unwrap() ); utils::span_err(self.tcx, span, err_msg); @@ -1545,8 +1549,8 @@ impl<'tcx> GotocCtx<'tcx> { let (_, rust_base_type) = self.simd_size_and_type(rust_ret_type); let err_msg = format!( "expected return type with integer elements, found `{}` with non-integer `{}`", - pretty_ty(rust_ret_type), - pretty_ty(rust_base_type), + self.pretty_ty(rust_ret_type), + self.pretty_ty(rust_base_type), ); utils::span_err(self.tcx, span, err_msg); } @@ -1740,7 +1744,7 @@ impl<'tcx> GotocCtx<'tcx> { if ret_type_len != n { let err_msg = format!( "expected return type of length {n}, found `{}` with length {ret_type_len}", - pretty_ty(rust_ret_type), + self.pretty_ty(rust_ret_type), ); utils::span_err(self.tcx, span, err_msg); } @@ -1748,10 +1752,10 @@ impl<'tcx> GotocCtx<'tcx> { let err_msg = format!( "expected return element type `{}` (element of input `{}`), \ found `{}` with element type `{}`", - pretty_ty(vec_subtype), - pretty_ty(rust_arg_types[0]), - pretty_ty(rust_ret_type), - pretty_ty(ret_type_subtype), + self.pretty_ty(vec_subtype), + self.pretty_ty(rust_arg_types[0]), + self.pretty_ty(rust_ret_type), + self.pretty_ty(ret_type_subtype), ); utils::span_err(self.tcx, span, err_msg); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index fd9ff33e164e..9296b713c862 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -260,7 +260,7 @@ impl<'tcx> GotocCtx<'tcx> { Ok(parent_expr.member(Self::tuple_fld_name(field_idx), &self.symbol_table)) } TyKind::RigidTy(RigidTy::Adt(def, _)) - if rustc_internal::internal(def).repr().simd() => + if rustc_internal::internal(self.tcx, def).repr().simd() => { Ok(self.codegen_simd_field( parent_expr, @@ -415,7 +415,7 @@ impl<'tcx> GotocCtx<'tcx> { }; let inner_mir_typ_internal = - std_pointee_type(rustc_internal::internal(base_type)).unwrap(); + std_pointee_type(rustc_internal::internal(self.tcx, base_type)).unwrap(); let inner_mir_typ = rustc_internal::stable(inner_mir_typ_internal); let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self .use_thin_pointer(inner_mir_typ_internal) @@ -436,6 +436,7 @@ impl<'tcx> GotocCtx<'tcx> { ); assert!( self.use_fat_pointer(rustc_internal::internal( + self.tcx, pointee_type(fat_ptr_mir_typ.unwrap()).unwrap() )), "Unexpected type: {:?} -- {:?}", @@ -582,7 +583,7 @@ impl<'tcx> GotocCtx<'tcx> { (variant.name().into(), TypeOrVariant::Variant(variant)) } TyKind::RigidTy(RigidTy::Coroutine(..)) => { - let idx_internal = rustc_internal::internal(idx); + let idx_internal = rustc_internal::internal(self.tcx, idx); ( self.coroutine_variant_name(idx_internal), TypeOrVariant::CoroutineVariant(*idx), @@ -593,7 +594,7 @@ impl<'tcx> GotocCtx<'tcx> { &ty.kind() ), }; - let layout = self.layout_of(rustc_internal::internal(ty)); + let layout = self.layout_of(rustc_internal::internal(self.tcx, ty)); let expr = match &layout.variants { Variants::Single { .. } => before.goto_expr, Variants::Multiple { tag_encoding, .. } => match tag_encoding { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index c4ea258fe79e..e7501df3aac4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -555,7 +555,7 @@ impl<'tcx> GotocCtx<'tcx> { let layout = self.layout_of_stable(res_ty); let fields = match &layout.variants { Variants::Single { index } => { - if *index != rustc_internal::internal(variant_index) { + if *index != rustc_internal::internal(self.tcx, variant_index) { // This may occur if all variants except for the one pointed by // index can never be constructed. Generic code might still try // to initialize the non-existing invariant. @@ -565,7 +565,7 @@ impl<'tcx> GotocCtx<'tcx> { &layout.fields } Variants::Multiple { variants, .. } => { - &variants[rustc_internal::internal(variant_index)].fields + &variants[rustc_internal::internal(self.tcx, variant_index)].fields } }; @@ -716,7 +716,10 @@ impl<'tcx> GotocCtx<'tcx> { .offset_of_subfield( self, fields.iter().map(|(var_idx, field_idx)| { - (rustc_internal::internal(var_idx), (*field_idx).into()) + ( + rustc_internal::internal(self.tcx, var_idx), + (*field_idx).into(), + ) }), ) .bytes(), @@ -1180,7 +1183,7 @@ impl<'tcx> GotocCtx<'tcx> { if self.vtable_ctx.emit_vtable_restrictions { // Add to the possible method names for this trait type self.vtable_ctx.add_possible_method( - self.normalized_trait_name(rustc_internal::internal(ty)).into(), + self.normalized_trait_name(rustc_internal::internal(self.tcx, ty)).into(), idx, fn_name.into(), ); @@ -1205,7 +1208,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Generate a function pointer to drop_in_place for entry into the vtable fn codegen_vtable_drop_in_place(&mut self, ty: Ty, trait_ty: Ty) -> Expr { - let trait_ty = rustc_internal::internal(trait_ty); + let trait_ty = rustc_internal::internal(self.tcx, trait_ty); let drop_instance = Instance::resolve_drop_in_place(ty); let drop_sym_name: InternedString = drop_instance.mangled_name().into(); @@ -1296,7 +1299,7 @@ impl<'tcx> GotocCtx<'tcx> { _ => unreachable!("Cannot codegen_vtable for type {:?}", dst_mir_type.kind()), }; - let src_name = self.ty_mangled_name(rustc_internal::internal(src_mir_type)); + let src_name = self.ty_mangled_name(rustc_internal::internal(self.tcx, src_mir_type)); // The name needs to be the same as inserted in typ.rs let vtable_name = self.vtable_name_stable(trait_type).intern(); let vtable_impl_name = format!("{vtable_name}_impl_for_{src_name}"); @@ -1310,7 +1313,7 @@ impl<'tcx> GotocCtx<'tcx> { // Build the vtable, using Rust's vtable_entries to determine field order let vtable_entries = if let Some(principal) = trait_type.kind().trait_principal() { let trait_ref_binder = principal.with_self_ty(src_mir_type); - ctx.tcx.vtable_entries(rustc_internal::internal(trait_ref_binder)) + ctx.tcx.vtable_entries(rustc_internal::internal(ctx.tcx, trait_ref_binder)) } else { TyCtxt::COMMON_VTABLE_ENTRIES }; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index c06d64d298c4..d06829822274 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -31,7 +31,7 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn codegen_caller_span_stable(&self, sp: SpanStable) -> Location { - self.codegen_caller_span(&rustc_internal::internal(sp)) + self.codegen_caller_span(&rustc_internal::internal(self.tcx, sp)) } /// Get the location of the caller. This will attempt to reach the macro caller. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 3a62a3f91d1a..05eb1bc41dc7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -220,8 +220,8 @@ impl<'tcx> GotocCtx<'tcx> { location: Location, ) -> Stmt { // this requires place points to an enum type. - let dest_ty_internal = rustc_internal::internal(dest_ty); - let variant_index_internal = rustc_internal::internal(variant_index); + let dest_ty_internal = rustc_internal::internal(self.tcx, dest_ty); + let variant_index_internal = rustc_internal::internal(self.tcx, variant_index); let layout = self.layout_of(dest_ty_internal); match &layout.variants { Variants::Single { .. } => Stmt::skip(location), @@ -533,7 +533,7 @@ impl<'tcx> GotocCtx<'tcx> { let instance = Instance::resolve(def, &subst).unwrap(); // TODO(celina): Move this check to be inside codegen_funcall_args. - if self.ty_needs_untupled_args(rustc_internal::internal(funct)) { + if self.ty_needs_untupled_args(rustc_internal::internal(self.tcx, funct)) { self.codegen_untupled_args(instance, &mut fargs, args.last()); } @@ -595,7 +595,7 @@ impl<'tcx> GotocCtx<'tcx> { fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty) -> Expr { // Generate an expression that indexes the pointer. let expr = self - .receiver_data_path(rustc_internal::internal(arg_ty)) + .receiver_data_path(rustc_internal::internal(self.tcx, arg_ty)) .fold(arg_expr, |curr_expr, (name, _)| curr_expr.member(name, &self.symbol_table)); trace!(?arg_ty, gotoc_ty=?expr.typ(), gotoc_expr=?expr.value(), "extract_ptr"); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs index c4f03e6c2cef..0130beffe84b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs @@ -20,11 +20,11 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn codegen_ty_stable(&mut self, ty: Ty) -> Type { - self.codegen_ty(rustc_internal::internal(ty)) + self.codegen_ty(rustc_internal::internal(self.tcx, ty)) } pub fn codegen_ty_ref_stable(&mut self, ty: Ty) -> Type { - self.codegen_ty_ref(rustc_internal::internal(ty)) + self.codegen_ty_ref(rustc_internal::internal(self.tcx, ty)) } pub fn local_ty_stable(&self, local: Local) -> Ty { @@ -36,11 +36,11 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn is_zst_stable(&self, ty: Ty) -> bool { - self.is_zst(rustc_internal::internal(ty)) + self.is_zst(rustc_internal::internal(self.tcx, ty)) } pub fn layout_of_stable(&self, ty: Ty) -> TyAndLayout<'tcx> { - self.layout_of(rustc_internal::internal(ty)) + self.layout_of(rustc_internal::internal(self.tcx, ty)) } pub fn codegen_fndef_type_stable(&mut self, instance: Instance) -> Type { @@ -53,27 +53,27 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn use_fat_pointer_stable(&self, pointer_ty: Ty) -> bool { - self.use_fat_pointer(rustc_internal::internal(pointer_ty)) + self.use_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty)) } pub fn use_thin_pointer_stable(&self, pointer_ty: Ty) -> bool { - self.use_thin_pointer(rustc_internal::internal(pointer_ty)) + self.use_thin_pointer(rustc_internal::internal(self.tcx, pointer_ty)) } pub fn is_fat_pointer_stable(&self, pointer_ty: Ty) -> bool { - self.is_fat_pointer(rustc_internal::internal(pointer_ty)) + self.is_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty)) } pub fn is_vtable_fat_pointer_stable(&self, pointer_ty: Ty) -> bool { - self.is_vtable_fat_pointer(rustc_internal::internal(pointer_ty)) + self.is_vtable_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty)) } pub fn use_vtable_fat_pointer_stable(&self, pointer_ty: Ty) -> bool { - self.use_vtable_fat_pointer(rustc_internal::internal(pointer_ty)) + self.use_vtable_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty)) } pub fn vtable_name_stable(&self, ty: Ty) -> String { - self.vtable_name(rustc_internal::internal(ty)) + self.vtable_name(rustc_internal::internal(self.tcx, ty)) } pub fn rvalue_ty_stable(&self, rvalue: &Rvalue) -> Ty { @@ -81,12 +81,12 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn simd_size_and_type(&self, ty: Ty) -> (u64, Ty) { - let (sz, ty) = rustc_internal::internal(ty).simd_size_and_type(self.tcx); + let (sz, ty) = rustc_internal::internal(self.tcx, ty).simd_size_and_type(self.tcx); (sz, rustc_internal::stable(ty)) } pub fn codegen_enum_discr_typ_stable(&self, ty: Ty) -> Ty { - rustc_internal::stable(self.codegen_enum_discr_typ(rustc_internal::internal(ty))) + rustc_internal::stable(self.codegen_enum_discr_typ(rustc_internal::internal(self.tcx, ty))) } pub fn codegen_function_sig_stable(&mut self, sig: FnSig) -> Type { @@ -107,6 +107,14 @@ impl<'tcx> GotocCtx<'tcx> { Type::code_with_unnamed_parameters(params, self.codegen_ty_stable(sig.output())) } } + + /// Convert a type into a user readable type representation. + /// + /// This should be replaced by StableMIR `pretty_ty()` after + /// is merged. + pub fn pretty_ty(&self, ty: Ty) -> String { + rustc_internal::internal(self.tcx, ty).to_string() + } } /// If given type is a Ref / Raw ref, return the pointee type. pub fn pointee_type(mir_type: Ty) -> Option { @@ -117,14 +125,6 @@ pub fn pointee_type(mir_type: Ty) -> Option { } } -/// Convert a type into a user readable type representation. -/// -/// This should be replaced by StableMIR `pretty_ty()` after -/// is merged. -pub fn pretty_ty(ty: Ty) -> String { - rustc_internal::internal(ty).to_string() -} - pub fn pointee_type_stable(ty: Ty) -> Option { match ty.kind() { TyKind::RigidTy(RigidTy::Ref(_, pointee_ty, _)) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 83ec6c3374ae..62b5cbedd95a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1101,7 +1101,7 @@ impl<'tcx> GotocCtx<'tcx> { .map(|(_, arg_abi)| { let arg_ty_stable = arg_abi.ty; let kind = arg_ty_stable.kind(); - let arg_ty = rustc_internal::internal(arg_ty_stable); + let arg_ty = rustc_internal::internal(self.tcx, arg_ty_stable); if is_first { is_first = false; debug!(self_type=?arg_ty, ?fn_abi, "codegen_dynamic_function_sig"); @@ -1686,7 +1686,7 @@ impl<'tcx> GotocCtx<'tcx> { instance: InstanceStable, fn_abi: &'a FnAbi, ) -> impl Iterator { - let instance_internal = rustc_internal::internal(instance); + let instance_internal = rustc_internal::internal(self.tcx, instance); let requires_caller_location = instance_internal.def.requires_caller_location(self.tcx); let num_args = fn_abi.args.len(); fn_abi.args.iter().enumerate().filter(move |(idx, arg_abi)| { diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 1cfff307f856..810c5707aad4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -307,7 +307,7 @@ impl CodegenBackend for GotocCodegenBackend { let main_instance = stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap()); let local_reachable = filter_crate_items(tcx, |_, instance| { - let def_id = rustc_internal::internal(instance.def.def_id()); + let def_id = rustc_internal::internal(tcx, instance.def.def_id()); Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id) }) .into_iter() diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs index b8251b153e5a..adac294e30eb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -4,8 +4,8 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Stmt; use cbmc::InternedString; -use rustc_middle::mir::Body as InternalBody; -use rustc_middle::ty::Instance as InternalInstance; +use rustc_middle::mir::Body as BodyInternal; +use rustc_middle::ty::Instance as InstanceInternal; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::{Body, Local, LocalDecl}; @@ -22,7 +22,9 @@ pub struct CurrentFnCtx<'tcx> { /// The crate this function is from krate: String, /// The MIR for the current instance. This is using the internal representation. - mir: &'tcx InternalBody<'tcx>, + mir: &'tcx BodyInternal<'tcx>, + /// The current instance. This is using the internal representation. + instance_internal: InstanceInternal<'tcx>, /// A list of local declarations used to retrieve MIR component types. locals: Vec, /// A list of pretty names for locals that corrspond to user variables. @@ -38,7 +40,7 @@ pub struct CurrentFnCtx<'tcx> { /// Constructor impl<'tcx> CurrentFnCtx<'tcx> { pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>, body: &Body) -> Self { - let internal_instance = rustc_internal::internal(instance); + let instance_internal = rustc_internal::internal(gcx.tcx, instance); let readable_name = instance.name(); let name = if &readable_name == "main" { readable_name.clone() } else { instance.mangled_name() }; @@ -51,7 +53,8 @@ impl<'tcx> CurrentFnCtx<'tcx> { Self { block: vec![], instance, - mir: gcx.tcx.instance_mir(internal_instance.def), + mir: gcx.tcx.instance_mir(instance_internal.def), + instance_internal, krate: instance.def.krate().name, locals, local_names, @@ -83,8 +86,8 @@ impl<'tcx> CurrentFnCtx<'tcx> { /// Getters impl<'tcx> CurrentFnCtx<'tcx> { /// The function we are currently compiling - pub fn instance(&self) -> InternalInstance<'tcx> { - rustc_internal::internal(self.instance) + pub fn instance(&self) -> InstanceInternal<'tcx> { + self.instance_internal } pub fn instance_stable(&self) -> Instance { @@ -92,7 +95,7 @@ impl<'tcx> CurrentFnCtx<'tcx> { } /// The internal MIR for the function we are currently compiling using internal APIs. - pub fn body_internal(&self) -> &'tcx InternalBody<'tcx> { + pub fn body_internal(&self) -> &'tcx BodyInternal<'tcx> { self.mir } diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 97606688d1ed..0141c2886539 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -38,7 +38,7 @@ pub trait GotocHook { fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool { let attr_sym = rustc_span::symbol::Symbol::intern(attr_name); if let Some(attr_id) = tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) { - if rustc_internal::internal(instance.def.def_id()) == *attr_id { + if rustc_internal::internal(tcx, instance.def.def_id()) == *attr_id { debug!("matched: {:?} {:?}", attr_id, attr_sym); return true; } @@ -196,7 +196,7 @@ struct Panic; impl GotocHook for Panic { fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { - let def_id = rustc_internal::internal(instance.def.def_id()); + let def_id = rustc_internal::internal(tcx, instance.def.def_id()); Some(def_id) == tcx.lang_items().panic_fn() || tcx.has_attr(def_id, rustc_span::sym::rustc_const_panic_str) || Some(def_id) == tcx.lang_items().panic_fmt() diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs index d81839ea097c..e369f64beda9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs @@ -194,5 +194,5 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn span_err(tcx: TyCtxt, span: Span, msg: String) { - tcx.dcx().span_err(rustc_internal::internal(span), msg); + tcx.dcx().span_err(rustc_internal::internal(tcx, span), msg); } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index e9edbedfcd82..32425204d76a 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -141,7 +141,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// Look up the attributes by a stable MIR DefID pub fn for_def_id(tcx: TyCtxt<'tcx>, def_id: StableDefId) -> Self { - KaniAttributes::for_item(tcx, rustc_internal::internal(def_id)) + KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, def_id)) } pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self { @@ -671,7 +671,7 @@ pub fn is_function_contract_generated(tcx: TyCtxt, def_id: DefId) -> bool { /// Same as [`KaniAttributes::is_harness`] but more efficient because less /// attribute parsing is performed. pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool { - let def_id = rustc_internal::internal(instance.def.def_id()); + let def_id = rustc_internal::internal(tcx, instance.def.def_id()); has_kani_attribute(tcx, def_id, |a| { matches!(a, KaniAttributeKind::Proof | KaniAttributeKind::ProofForContract) }) @@ -679,14 +679,14 @@ pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool { /// Does this `def_id` have `#[rustc_test_marker]`? pub fn is_test_harness_description(tcx: TyCtxt, item: impl CrateDef) -> bool { - let def_id = rustc_internal::internal(item.def_id()); + let def_id = rustc_internal::internal(tcx, item.def_id()); let attrs = tcx.get_attrs_unchecked(def_id); attr::contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker) } /// Extract the test harness name from the `#[rustc_test_maker]` pub fn test_harness_name(tcx: TyCtxt, def: &impl CrateDef) -> String { - let def_id = rustc_internal::internal(def.def_id()); + let def_id = rustc_internal::internal(tcx, def.def_id()); let attrs = tcx.get_attrs_unchecked(def_id); let marker = attr::find_by_name(attrs, rustc_span::symbol::sym::rustc_test_marker).unwrap(); parse_str_value(&marker).unwrap() @@ -944,7 +944,7 @@ fn parse_integer(attr: &Attribute) -> Option { if attr_args.len() == 1 { let x = attr_args[0].lit()?; match x.kind { - LitKind::Int(y, ..) => Some(y), + LitKind::Int(y, ..) => Some(y.get()), _ => None, } } diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 85d59215d661..94879b5b65e6 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -66,8 +66,8 @@ pub fn extract_unsize_casting_stable( ) -> CoercionBaseStable { let CoercionBase { src_ty, dst_ty } = extract_unsize_casting( tcx, - rustc_internal::internal(src_ty), - rustc_internal::internal(dst_ty), + rustc_internal::internal(tcx, src_ty), + rustc_internal::internal(tcx, dst_ty), ); CoercionBaseStable { src_ty: rustc_internal::stable(src_ty), @@ -90,11 +90,11 @@ pub fn extract_unsize_casting<'tcx>( .last() .unwrap(); // Extract the pointee type that is being coerced. - let src_pointee_ty = extract_pointee(coerce_info.src_ty).expect(&format!( + let src_pointee_ty = extract_pointee(tcx, coerce_info.src_ty).expect(&format!( "Expected source to be a pointer. Found {:?} instead", coerce_info.src_ty )); - let dst_pointee_ty = extract_pointee(coerce_info.dst_ty).expect(&format!( + let dst_pointee_ty = extract_pointee(tcx, coerce_info.dst_ty).expect(&format!( "Expected destination to be a pointer. Found {:?} instead", coerce_info.dst_ty )); @@ -216,8 +216,8 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> { let CustomCoerceUnsized::Struct(coerce_index) = custom_coerce_unsize_info( self.tcx, - rustc_internal::internal(src_ty), - rustc_internal::internal(dst_ty), + rustc_internal::internal(self.tcx, src_ty), + rustc_internal::internal(self.tcx, dst_ty), ); let coerce_index = coerce_index.as_usize(); assert!(coerce_index < src_fields.len()); @@ -229,7 +229,7 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> { _ => { // Base case is always a pointer (Box, raw_pointer or reference). assert!( - extract_pointee(src_ty).is_some(), + extract_pointee(self.tcx, src_ty).is_some(), "Expected a pointer, but found {src_ty:?}" ); None @@ -262,6 +262,6 @@ fn custom_coerce_unsize_info<'tcx>( } /// Extract pointee type from builtin pointer types. -fn extract_pointee<'tcx>(typ: TyStable) -> Option> { - rustc_internal::internal(typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty) +fn extract_pointee(tcx: TyCtxt<'_>, typ: TyStable) -> Option> { + rustc_internal::internal(tcx, typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty) } diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 66fb2ca0aa33..e65befc9624e 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -92,7 +92,10 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) // We don't short circuit here since this is a type check and can shake // out differently depending on generic parameters. if let MonoItem::Fn(instance) = item { - if attributes::is_function_contract_generated(tcx, rustc_internal::internal(def_id)) { + if attributes::is_function_contract_generated( + tcx, + rustc_internal::internal(tcx, def_id), + ) { check_is_contract_safe(tcx, *instance); } } @@ -167,7 +170,7 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) { for var in &bound_fn_sig.bound_vars { if let BoundVariableKind::Ty(t) = var { tcx.dcx().span_err( - rustc_internal::internal(instance.def.span()), + rustc_internal::internal(tcx, instance.def.span()), format!("Found a bound type variable {t:?} after monomorphization"), ); } @@ -211,7 +214,8 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) { // For each def_id, dump their MIR for (item, def_id) in items.iter().filter_map(visible_item) { writeln!(writer, "// Item: {item:?}").unwrap(); - write_mir_pretty(tcx, Some(rustc_internal::internal(def_id)), &mut writer).unwrap(); + write_mir_pretty(tcx, Some(rustc_internal::internal(tcx, def_id)), &mut writer) + .unwrap(); } } } diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 424077a622f9..63ed41bfd4c1 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -75,7 +75,7 @@ where .filter_map(|item| { // Only collect monomorphic items. // TODO: Remove the def_kind check once https://github.com/rust-lang/rust/pull/119135 has been released. - let def_id = rustc_internal::internal(item.def_id()); + let def_id = rustc_internal::internal(tcx, item.def_id()); (matches!(tcx.def_kind(def_id), rustc_hir::def::DefKind::Ctor(..)) || matches!(item.kind(), ItemKind::Fn)) .then(|| { @@ -237,7 +237,8 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { let poly_trait_ref = principal.with_self_ty(concrete_ty); // Walk all methods of the trait, including those of its supertraits - let entries = self.tcx.vtable_entries(rustc_internal::internal(&poly_trait_ref)); + let entries = + self.tcx.vtable_entries(rustc_internal::internal(self.tcx, &poly_trait_ref)); let methods = entries.iter().filter_map(|entry| match entry { VtblEntry::MetadataAlign | VtblEntry::MetadataDropInPlace @@ -395,9 +396,10 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { let caller = CrateItem::try_from(*self.instance).unwrap().name(); let callee = fn_def.name(); // Check if the current function has been stubbed. - if let Some(stub) = - get_stub(self.tcx, rustc_internal::internal(self.instance).def_id()) - { + if let Some(stub) = get_stub( + self.tcx, + rustc_internal::internal(self.tcx, self.instance).def_id(), + ) { // During the MIR stubbing transformation, we do not // force type variables in the stub's signature to // implement the same traits as those in the @@ -413,7 +415,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { let sep = callee.rfind("::").unwrap(); let trait_ = &callee[..sep]; self.tcx.dcx().span_err( - rustc_internal::internal(terminator.span), + rustc_internal::internal(self.tcx, terminator.span), format!( "`{}` doesn't implement \ `{}`. The function `{}` \ @@ -465,8 +467,8 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty) { let CoercionBase { src_ty, dst_ty } = coercion::extract_unsize_casting( tcx, - rustc_internal::internal(orig_ty), - rustc_internal::internal(dst_trait), + rustc_internal::internal(tcx, orig_ty), + rustc_internal::internal(tcx, dst_trait), ); (rustc_internal::stable(src_ty), rustc_internal::stable(dst_ty)) } @@ -476,7 +478,7 @@ fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty) fn to_fingerprint(tcx: TyCtxt, item: &MonoItem) -> Fingerprint { tcx.with_stable_hashing_context(|mut hcx| { let mut hasher = StableHasher::new(); - rustc_internal::internal(item).hash_stable(&mut hcx, &mut hasher); + rustc_internal::internal(tcx, item).hash_stable(&mut hcx, &mut hasher); hasher.finish() }) } diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index e88485ebc6d7..53670bfd482d 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -399,8 +399,11 @@ fn resolve_in_type<'tcx>( name: &str, ) -> Result> { debug!(?name, ?type_id, "resolve_in_type"); + let missing_item_err = + || ResolveError::MissingItem { tcx, base: type_id, unresolved: name.to_string() }; // Try the inherent `impl` blocks (i.e., non-trait `impl`s). tcx.inherent_impls(type_id) + .map_err(|_| missing_item_err())? .iter() .flat_map(|impl_id| tcx.associated_item_def_ids(impl_id)) .cloned() @@ -409,9 +412,5 @@ fn resolve_in_type<'tcx>( let last = item_path.split("::").last().unwrap(); last == name }) - .ok_or_else(|| ResolveError::MissingItem { - tcx, - base: type_id, - unresolved: name.to_string(), - }) + .ok_or_else(missing_item_err) } diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 9dda0144eda4..0db518ceef9f 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -27,7 +27,7 @@ pub fn harness_stub_map( harness: Instance, metadata: &HarnessMetadata, ) -> BTreeMap { - let def_id = rustc_internal::internal(harness.def.def_id()); + let def_id = rustc_internal::internal(tcx, harness.def.def_id()); let attrs = &metadata.attributes; let mut stub_pairs = BTreeMap::default(); for stubs in &attrs.stubs { @@ -44,7 +44,7 @@ pub fn harness_stub_map( /// In stable MIR, trying to retrieve an `Instance::body()` will ICE if we cannot evaluate a /// constant as expected. For now, use internal APIs to anticipate this issue. pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool { - let internal_instance = rustc_internal::internal(instance); + let internal_instance = rustc_internal::internal(tcx, instance); if get_stub(tcx, internal_instance.def_id()).is_some() { debug!(?instance, "validate_instance"); let item = CrateItem::try_from(instance).unwrap(); @@ -87,7 +87,7 @@ impl<'tcx> StubConstChecker<'tcx> { impl<'tcx> MirVisitor for StubConstChecker<'tcx> { /// Collect constants that are represented as static variables. fn visit_constant(&mut self, constant: &Constant, location: Location) { - let const_ = self.monomorphize(rustc_internal::internal(&constant.literal)); + let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.literal)); debug!(?constant, ?location, ?const_, "visit_constant"); match const_ { Const::Val(..) | Const::Ty(..) => {} @@ -109,7 +109,7 @@ impl<'tcx> MirVisitor for StubConstChecker<'tcx> { tcx.def_path_str(trait_), self.source.name() ); - tcx.dcx().span_err(rustc_internal::internal(location.span()), msg); + tcx.dcx().span_err(rustc_internal::internal(self.tcx, location.span()), msg); self.is_valid = false; } } diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index f02eaa627477..98f52c19d9e7 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -11,7 +11,7 @@ use syn::ItemFn; use super::{ helpers::*, shared::{attach_require_kani_any, identifier_for_generated_function}, - ContractConditionsData, ContractConditionsHandler, + ContractConditionsHandler, }; impl<'a> ContractConditionsHandler<'a> { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 2914c0609c1a..510d3e13b50b 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-01-17" +channel = "nightly-2024-01-23" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs index 9e76a55a2cb3..ba482248898c 100644 --- a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs +++ b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs @@ -30,13 +30,13 @@ fn main() { assert!(min_align_of_val(&0i16) == 2); assert!(min_align_of_val(&0i32) == 4); assert!(min_align_of_val(&0i64) == 8); - assert!(min_align_of_val(&0i128) == 8); + assert!(min_align_of_val(&0i128) == 16); assert!(min_align_of_val(&0isize) == 8); assert!(min_align_of_val(&0u8) == 1); assert!(min_align_of_val(&0u16) == 2); assert!(min_align_of_val(&0u32) == 4); assert!(min_align_of_val(&0u64) == 8); - assert!(min_align_of_val(&0u128) == 8); + assert!(min_align_of_val(&0u128) == 16); assert!(min_align_of_val(&0usize) == 8); assert!(min_align_of_val(&0f32) == 4); assert!(min_align_of_val(&0f64) == 8); diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs index e1b3e1dd4491..426f09de1a59 100644 --- a/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs +++ b/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs @@ -19,7 +19,7 @@ fn check_align_simple() { let a = A { id: 0 }; let t: &dyn T = &a; #[cfg(target_arch = "x86_64")] - assert_eq!(align_of_val(t), 8); + assert_eq!(align_of_val(t), 16); #[cfg(target_arch = "aarch64")] assert_eq!(align_of_val(t), 16); assert_eq!(align_of_val(&t), 8); diff --git a/tests/kani/Intrinsics/ConstEval/min_align_of.rs b/tests/kani/Intrinsics/ConstEval/min_align_of.rs index eed572b8dc9f..425f27084076 100644 --- a/tests/kani/Intrinsics/ConstEval/min_align_of.rs +++ b/tests/kani/Intrinsics/ConstEval/min_align_of.rs @@ -19,13 +19,13 @@ fn main() { assert!(min_align_of::() == 2); assert!(min_align_of::() == 4); assert!(min_align_of::() == 8); - assert!(min_align_of::() == 8); + assert!(min_align_of::() == 16); assert!(min_align_of::() == 8); assert!(min_align_of::() == 1); assert!(min_align_of::() == 2); assert!(min_align_of::() == 4); assert!(min_align_of::() == 8); - assert!(min_align_of::() == 8); + assert!(min_align_of::() == 16); assert!(min_align_of::() == 8); assert!(min_align_of::() == 4); assert!(min_align_of::() == 8); diff --git a/tests/kani/Intrinsics/ConstEval/pref_align_of.rs b/tests/kani/Intrinsics/ConstEval/pref_align_of.rs index 22ff342a8198..d495bffef5f8 100644 --- a/tests/kani/Intrinsics/ConstEval/pref_align_of.rs +++ b/tests/kani/Intrinsics/ConstEval/pref_align_of.rs @@ -19,13 +19,13 @@ fn main() { assert!(unsafe { pref_align_of::() } == 2); assert!(unsafe { pref_align_of::() } == 4); assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 8); + assert!(unsafe { pref_align_of::() } == 16); assert!(unsafe { pref_align_of::() } == 8); assert!(unsafe { pref_align_of::() } == 1); assert!(unsafe { pref_align_of::() } == 2); assert!(unsafe { pref_align_of::() } == 4); assert!(unsafe { pref_align_of::() } == 8); - assert!(unsafe { pref_align_of::() } == 8); + assert!(unsafe { pref_align_of::() } == 16); assert!(unsafe { pref_align_of::() } == 8); assert!(unsafe { pref_align_of::() } == 4); assert!(unsafe { pref_align_of::() } == 8); diff --git a/tests/perf/hashset/expected b/tests/perf/hashset/expected index 8ba783d580f9..1fbcbbd13c25 100644 --- a/tests/perf/hashset/expected +++ b/tests/perf/hashset/expected @@ -1 +1 @@ -4 successfully verified harnesses, 0 failures, 4 total +3 successfully verified harnesses, 0 failures, 3 total diff --git a/tests/perf/hashset/src/lib.rs b/tests/perf/hashset/src/lib.rs index fb29db5c7ed6..e2f1fc16666a 100644 --- a/tests/perf/hashset/src/lib.rs +++ b/tests/perf/hashset/src/lib.rs @@ -1,11 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-stubbing --enable-unstable +// kani-flags: -Z stubbing //! Try to verify HashSet basic behavior. use std::collections::{hash_map::RandomState, HashSet}; use std::mem::{size_of, size_of_val, transmute}; +#[allow(dead_code)] fn concrete_state() -> RandomState { let keys: [u64; 2] = [0, 0]; assert_eq!(size_of_val(&keys), size_of::()); @@ -14,7 +15,7 @@ fn concrete_state() -> RandomState { #[kani::proof] #[kani::stub(RandomState::new, concrete_state)] -#[kani::unwind(2)] +#[kani::unwind(5)] #[kani::solver(kissat)] fn check_insert() { let mut set: HashSet = HashSet::default(); @@ -26,41 +27,29 @@ fn check_insert() { #[kani::proof] #[kani::stub(RandomState::new, concrete_state)] -#[kani::unwind(2)] +#[kani::unwind(5)] #[kani::solver(kissat)] fn check_contains() { let first = kani::any(); - let mut set: HashSet = HashSet::from([first]); + let set: HashSet = HashSet::from([first]); assert!(set.contains(&first)); } #[kani::proof] #[kani::stub(RandomState::new, concrete_state)] -#[kani::unwind(2)] +#[kani::unwind(5)] +#[kani::solver(kissat)] fn check_contains_str() { - let mut set = HashSet::from(["s"]); + let set = HashSet::from(["s"]); assert!(set.contains(&"s")); } -#[kani::proof] -#[kani::stub(RandomState::new, concrete_state)] -#[kani::unwind(2)] -#[kani::solver(kissat)] -fn check_insert_two_concrete() { - let mut set: HashSet = HashSet::default(); - let first = 10; - let second = 20; - set.insert(first); - set.insert(second); - assert_eq!(set.len(), 2); -} - // too slow so don't run in the regression for now #[cfg(slow)] mod slow { #[kani::proof] #[kani::stub(RandomState::new, concrete_state)] - #[kani::unwind(3)] + #[kani::unwind(5)] fn check_insert_two_elements() { let mut set: HashSet = HashSet::default(); let first = kani::any(); @@ -71,4 +60,17 @@ mod slow { if first == second { assert_eq!(set.len(), 1) } else { assert_eq!(set.len(), 2) } } + + #[kani::proof] + #[kani::stub(RandomState::new, concrete_state)] + #[kani::unwind(5)] + #[kani::solver(kissat)] + fn check_insert_two_concrete() { + let mut set: HashSet = HashSet::default(); + let first = 10; + let second = 20; + set.insert(first); + set.insert(second); + assert_eq!(set.len(), 2); + } }