From 6f7aa65d60340f5b14f90cc5a56a6f230f6522ce Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 15 May 2023 20:19:03 -0700 Subject: [PATCH] Upgrade the toolchain to nightly-2023-04-16 (#2406) Update the toolchain to use nightly-2023-04-16. Changes were related to the following changes to the toolchain: - https://github.com/rust-lang/rust/pull/108944 - https://github.com/rust-lang/rust/pull/108148 - https://github.com/rust-lang/rust/pull/108471 - https://github.com/rust-lang/rust/pull/109358 - https://github.com/rust-lang/rust/pull/109849 - https://github.com/rust-lang/rust/pull/109819 - https://github.com/rust-lang/rust/pull/109718 - https://github.com/rust-lang/rust/pull/109092 - https://github.com/rust-lang/rust/pull/108856 - https://github.com/rust-lang/rust/pull/105613 - https://github.com/rust-lang/rust/pull/103042 - https://github.com/rust-lang/rust/pull/109716 - https://github.com/rust-lang/rust/pull/108340 - https://github.com/rust-lang/rust/pull/102906 - https://github.com/rust-lang/rust/pull/98112 - https://github.com/rust-lang/rust/pull/108080 --- cprover_bindings/src/goto_program/expr.rs | 11 +++++++ .../codegen_cprover_gotoc/codegen/assert.rs | 4 +-- .../codegen_cprover_gotoc/codegen/function.rs | 2 +- .../codegen/intrinsic.rs | 19 ++++++++---- .../codegen_cprover_gotoc/codegen/operand.rs | 6 ++-- .../codegen_cprover_gotoc/codegen/place.rs | 11 +++---- .../codegen_cprover_gotoc/codegen/rvalue.rs | 30 ++++++++++++------- .../codegen/statement.rs | 25 +++++++++++----- .../src/codegen_cprover_gotoc/codegen/typ.rs | 27 +++++++++-------- .../compiler_interface.rs | 7 ++++- .../codegen_cprover_gotoc/context/goto_ctx.rs | 19 ------------ .../src/codegen_cprover_gotoc/utils/names.rs | 4 +++ kani-compiler/src/kani_middle/analysis.rs | 4 +-- kani-compiler/src/kani_middle/attributes.rs | 13 +++++--- kani-compiler/src/kani_middle/coercion.rs | 2 +- kani-compiler/src/kani_middle/mod.rs | 2 +- kani-compiler/src/kani_middle/provide.rs | 28 +++++++++-------- kani-compiler/src/kani_middle/reachability.rs | 8 ++--- kani-compiler/src/main.rs | 3 +- kani-compiler/src/session.rs | 7 ++--- rust-toolchain.toml | 2 +- ...doesnt_call_crate_with_global_asm.expected | 1 - tests/cargo-ui/unstable-attr/invalid/expected | 6 ++-- .../cargo-ui/unstable-attr/invalid/src/lib.rs | 5 ++++ tests/expected/array/main.rs | 10 ++++++- .../rustc-generator-tests/yield-in-box.rs | 10 +++---- .../{phantom_fixme.rs => phantom_data.rs} | 0 tests/ui/cbmc_checks/pointer/expected | 7 ++--- tests/ui/cbmc_checks/signed-overflow/expected | 2 -- .../ui/cbmc_checks/unsigned-overflow/expected | 1 - tests/ui/code-location/expected | 2 +- .../should-panic-attribute/no-panics/expected | 7 +++-- .../unexpected-failures/expected | 9 +++--- .../unexpected-failures/test.rs | 3 +- tools/bookrunner/librustdoc/doctest.rs | 7 +++-- tools/bookrunner/librustdoc/lib.rs | 2 -- tools/compiletest/src/header.rs | 6 ++++ 37 files changed, 181 insertions(+), 131 deletions(-) rename tests/kani/PhantomData/{phantom_fixme.rs => phantom_data.rs} (100%) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index b1c7ec455bc5..2ea84eaaf043 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -851,6 +851,17 @@ impl Expr { Expr::struct_expr_with_explicit_padding(typ, fields, values) } + /// Initializer for a zero sized type (ZST). + /// Since this is a ZST, we call nondet to simplify everything. + pub fn init_unit(typ: Type, symbol_table: &SymbolTable) -> Self { + assert!( + typ.is_struct_tag(), + "Zero sized types should be represented as struct: but found: {typ:?}" + ); + assert_eq!(typ.sizeof_in_bits(symbol_table), 0); + Expr::nondet(typ) + } + /// `identifier` pub fn symbol_expression>(identifier: T, typ: Type) -> Self { let identifier = identifier.into(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 8dfb31af85cc..1003681bce80 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -154,11 +154,11 @@ impl<'tcx> GotocCtx<'tcx> { if self.queries.get_check_assertion_reachability() { // Generate a unique ID for the assert let assert_id = self.next_check_id(); - // Generate a message for the reachability check that includes the unique ID - let reach_msg = assert_id.clone(); // Also add the unique ID as a prefix to the assert message so that it can be // easily paired with the reachability check let msg = GotocCtx::add_prefix_to_msg(&msg, &assert_id); + // Generate a message for the reachability check that includes the unique ID + let reach_msg = assert_id; // inject a reachability check, which is a (non-blocking) // assert(false) whose failure indicates that this line is reachable. // The property class (`PropertyClass:ReachabilityCheck`) is used by diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index cdab6d58251f..800ec8219e40 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -51,7 +51,7 @@ impl<'tcx> GotocCtx<'tcx> { var_type, self.codegen_span(&ldata.source_info.span), ) - .with_is_hidden(!ldata.is_user_variable()) + .with_is_hidden(!self.is_user_variable(&lc)) .with_is_parameter((idx > 0 && idx <= num_args) && !self.is_zst(var_ty)); let sym_e = sym.to_expr(); self.symbol_table.insert(sym); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index df89deb7cc59..554ba6a03a61 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -9,7 +9,7 @@ use cbmc::goto_program::{ Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, }; use rustc_middle::mir::{BasicBlock, Operand, Place}; -use rustc_middle::ty::layout::LayoutOf; +use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement}; use rustc_middle::ty::{self, Ty}; use rustc_middle::ty::{Instance, InstanceDef}; use rustc_span::Span; @@ -753,7 +753,7 @@ impl<'tcx> GotocCtx<'tcx> { /// layout is invalid so we get a message that mentions the offending type. /// /// - /// + /// /// fn codegen_assert_intrinsic( &mut self, @@ -781,7 +781,10 @@ impl<'tcx> GotocCtx<'tcx> { // Then we check if the type allows "raw" initialization for the cases // where memory is zero-initialized or entirely uninitialized if intrinsic == "assert_zero_valid" - && !self.tcx.permits_zero_init(param_env_and_type).ok().unwrap() + && !self + .tcx + .check_validity_requirement((ValidityRequirement::Zero, param_env_and_type)) + .unwrap() { return self.codegen_fatal_error( PropertyClass::SafetyCheck, @@ -790,8 +793,14 @@ impl<'tcx> GotocCtx<'tcx> { ); } - if intrinsic == "assert_uninit_valid" - && !self.tcx.permits_uninit_init(param_env_and_type).ok().unwrap() + if intrinsic == "assert_mem_uninitialized_valid" + && !self + .tcx + .check_validity_requirement(( + ValidityRequirement::UninitMitigated0x01Fill, + param_env_and_type, + )) + .unwrap() { return self.codegen_fatal_error( PropertyClass::SafetyCheck, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 2b6c26a7592b..b247e49593a8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -141,7 +141,7 @@ impl<'tcx> GotocCtx<'tcx> { ConstValue::ZeroSized => match lit_ty.kind() { // Rust "function items" (not closures, not function pointers, see `codegen_fndef`) ty::FnDef(d, substs) => self.codegen_fndef(*d, substs, span), - _ => unimplemented!(), + _ => Expr::init_unit(self.codegen_ty(lit_ty), &self.symbol_table), }, } } @@ -310,7 +310,7 @@ impl<'tcx> GotocCtx<'tcx> { } } else { // otherwise, there is just one field, which is stored as the scalar data - let field = &variant.fields[0]; + let field = &variant.fields[0usize.into()]; let fty = field.ty(self.tcx, subst); let overall_t = self.codegen_ty(ty); @@ -336,7 +336,7 @@ impl<'tcx> GotocCtx<'tcx> { &self.symbol_table, ), 1 => { - let fty = variant.fields[0].ty(self.tcx, subst); + let fty = variant.fields[0usize.into()].ty(self.tcx, subst); self.codegen_single_variant_single_field( s, span, overall_t, fty, ) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index dc6938f780f1..f3310498f842 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -11,10 +11,11 @@ use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; use crate::codegen_cprover_gotoc::GotocCtx; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{Expr, Location, Type}; +use rustc_abi::FieldIdx; use rustc_hir::Mutability; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::{ - mir::{Field, Local, Place, ProjectionElem}, + mir::{Local, Place, ProjectionElem}, ty::{self, Ty, TypeAndMut, VariantDef}, }; use rustc_target::abi::{TagEncoding, VariantIdx, Variants}; @@ -238,7 +239,7 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, res: Expr, t: TypeOrVariant<'tcx>, - f: &Field, + f: &FieldIdx, ) -> Result { match t { TypeOrVariant::Type(t) => { @@ -278,12 +279,12 @@ impl<'tcx> GotocCtx<'tcx> { } // if we fall here, then we are handling either a struct or a union ty::Adt(def, _) => { - let field = &def.variants().raw[0].fields[f.index()]; + let field = &def.variants().raw[0].fields[*f]; Ok(res.member(&field.name.to_string(), &self.symbol_table)) } ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)), ty::Generator(..) => { - let field_name = self.generator_field_name(f.index()); + let field_name = self.generator_field_name(f.as_usize()); Ok(res .member("direct_fields", &self.symbol_table) .member(field_name, &self.symbol_table)) @@ -293,7 +294,7 @@ impl<'tcx> GotocCtx<'tcx> { } // if we fall here, then we are handling an enum TypeOrVariant::Variant(v) => { - let field = &v.fields[f.index()]; + let field = &v.fields[*f]; Ok(res.member(&field.name.to_string(), &self.symbol_table)) } TypeOrVariant::GeneratorVariant(_var_idx) => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 8d212c75fda4..6fc139b9d5f2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -17,6 +17,8 @@ use cbmc::goto_program::{ use cbmc::MachineModel; use cbmc::{btree_string_map, InternString, InternedString}; use num::bigint::BigInt; +use rustc_abi::FieldIdx; +use rustc_index::vec::IndexVec; use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp}; use rustc_middle::ty::adjustment::PointerCast; use rustc_middle::ty::layout::LayoutOf; @@ -321,7 +323,11 @@ impl<'tcx> GotocCtx<'tcx> { } /// Create an initializer for a generator struct. - fn codegen_rvalue_generator(&mut self, operands: &[Operand<'tcx>], ty: Ty<'tcx>) -> Expr { + fn codegen_rvalue_generator( + &mut self, + operands: &IndexVec>, + ty: Ty<'tcx>, + ) -> Expr { let layout = self.layout_of(ty); let discriminant_field = match &layout.variants { Variants::Multiple { tag_encoding: TagEncoding::Direct, tag_field, .. } => tag_field, @@ -341,7 +347,7 @@ impl<'tcx> GotocCtx<'tcx> { if idx == *discriminant_field { Expr::int_constant(0, self.codegen_ty(field_ty)) } else { - self.codegen_operand(&operands[idx]) + self.codegen_operand(&operands[idx.into()]) } }) .collect(), @@ -358,7 +364,7 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_rvalue_enum_aggregate( &mut self, variant_index: VariantIdx, - operands: &[Operand<'tcx>], + operands: &IndexVec>, res_ty: Ty<'tcx>, loc: Location, ) -> Expr { @@ -400,7 +406,7 @@ impl<'tcx> GotocCtx<'tcx> { variant_expr.typ().clone(), fields .index_by_increasing_offset() - .map(|idx| self.codegen_operand(&operands[idx])) + .map(|idx| self.codegen_operand(&operands[idx.into()])) .collect(), &self.symbol_table, ); @@ -419,7 +425,7 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_rvalue_aggregate( &mut self, aggregate: &AggregateKind<'tcx>, - operands: &[Operand<'tcx>], + operands: &IndexVec>, res_ty: Ty<'tcx>, loc: Location, ) -> Expr { @@ -449,8 +455,8 @@ impl<'tcx> GotocCtx<'tcx> { let components = typ.lookup_components(&self.symbol_table).unwrap(); Expr::union_expr( typ, - components[active_field_index].name(), - self.codegen_operand(&operands[0]), + components[active_field_index.as_usize()].name(), + self.codegen_operand(&operands[0usize.into()]), &self.symbol_table, ) } @@ -464,7 +470,7 @@ impl<'tcx> GotocCtx<'tcx> { .fields .index_by_increasing_offset() .map(|idx| { - let cgo = self.codegen_operand(&operands[idx]); + let cgo = self.codegen_operand(&operands[idx.into()]); // The input operand might actually be a one-element array, as seen // when running assess on firecracker. if *cgo.typ() == vector_element_type { @@ -487,7 +493,7 @@ impl<'tcx> GotocCtx<'tcx> { layout .fields .index_by_increasing_offset() - .map(|idx| self.codegen_operand(&operands[idx])) + .map(|idx| self.codegen_operand(&operands[idx.into()])) .collect(), &self.symbol_table, ) @@ -537,6 +543,10 @@ impl<'tcx> GotocCtx<'tcx> { let t = self.monomorphize(*t); self.codegen_pointer_cast(k, e, t, loc) } + Rvalue::Cast(CastKind::Transmute, operand, ty) => { + let goto_typ = self.codegen_ty(self.monomorphize(*ty)); + self.codegen_operand(operand).transmute_to(goto_typ, &self.symbol_table) + } Rvalue::BinaryOp(op, box (ref e1, ref e2)) => { self.codegen_rvalue_binary_op(op, e1, e2, loc) } @@ -636,7 +646,7 @@ impl<'tcx> GotocCtx<'tcx> { // See also the cranelift backend: // https://github.com/rust-lang/rust/blob/05d22212e89588e7c443cc6b9bc0e4e02fdfbc8d/compiler/rustc_codegen_cranelift/src/discriminant.rs#L116 let offset = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => offsets[0], + FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()], _ => unreachable!("niche encoding must have arbitrary fields"), }; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 4892ed988e39..18f510dc7a56 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -86,6 +86,7 @@ impl<'tcx> GotocCtx<'tcx> { location, ) } + StatementKind::PlaceMention(_) => todo!(), StatementKind::FakeRead(_) | StatementKind::Retag(_, _) | StatementKind::AscribeUserType(_, _) @@ -122,8 +123,8 @@ impl<'tcx> GotocCtx<'tcx> { loc, "https://github.com/model-checking/kani/issues/692", ), - TerminatorKind::Abort => self.codegen_mimic_unimplemented( - "TerminatorKind::Abort", + TerminatorKind::Terminate => self.codegen_mimic_unimplemented( + "TerminatorKind::Terminate", loc, "https://github.com/model-checking/kani/issues/692", ), @@ -165,6 +166,10 @@ impl<'tcx> GotocCtx<'tcx> { // "index out of bounds: the length is {len} but the index is {index}", // but CBMC only accepts static messages so we don't add values to the message. "index out of bounds: the length is less than or equal to the given index" + } else if let AssertKind::MisalignedPointerDereference { .. } = msg { + // Misaligned pointer dereference check messages is also a runtime messages. + // Generate a generic one here. + "misaligned pointer dereference: address must be a multiple of its type's alignment" } else { // For all other assert kind we can get the static message. msg.description() @@ -187,9 +192,7 @@ impl<'tcx> GotocCtx<'tcx> { loc, ) } - TerminatorKind::DropAndReplace { .. } - | TerminatorKind::FalseEdge { .. } - | TerminatorKind::FalseUnwind { .. } => { + TerminatorKind::FalseEdge { .. } | TerminatorKind::FalseUnwind { .. } => { unreachable!("drop elaboration removes these TerminatorKind") } TerminatorKind::Yield { .. } | TerminatorKind::GeneratorDrop => { @@ -232,19 +235,23 @@ impl<'tcx> GotocCtx<'tcx> { // DISCRIMINANT - val:255 ty:i8 // DISCRIMINANT - val:0 ty:i8 // DISCRIMINANT - val:1 ty:i8 - let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t)); - self.codegen_discriminant_field(dest_expr, dest_ty).assign(discr, location) + trace!(?discr, ?discr_t, ?dest_ty, "codegen_set_discriminant direct"); + // The discr.ty doesn't always match the tag type. Explicitly cast if needed. + let discr_expr = Expr::int_constant(discr.val, self.codegen_ty(discr.ty)) + .cast_to(self.codegen_ty(discr_t)); + self.codegen_discriminant_field(dest_expr, dest_ty).assign(discr_expr, location) } TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => { if *untagged_variant != variant_index { let offset = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => offsets[0], + FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()], _ => unreachable!("niche encoding must have arbitrary fields"), }; let discr_ty = self.codegen_enum_discr_typ(dest_ty); let discr_ty = self.codegen_ty(discr_ty); let niche_value = variant_index.as_u32() - niche_variants.start().as_u32(); let niche_value = (niche_value as u128).wrapping_add(*niche_start); + trace!(val=?niche_value, typ=?discr_ty, "codegen_set_discriminant niche"); let value = if niche_value == 0 && matches!(tag.primitive(), Primitive::Pointer(_)) { @@ -548,6 +555,7 @@ impl<'tcx> GotocCtx<'tcx> { // Normal, non-virtual function calls InstanceDef::Item(..) | InstanceDef::DropGlue(_, Some(_)) + | InstanceDef::FnPtrAddrShim(_, _) | InstanceDef::Intrinsic(..) | InstanceDef::FnPtrShim(..) | InstanceDef::VTableShim(..) @@ -562,6 +570,7 @@ impl<'tcx> GotocCtx<'tcx> { .with_location(loc), ] } + InstanceDef::ThreadLocalShim(_) => todo!(), }; stmts.push(self.codegen_end_call(target.as_ref(), loc)); Stmt::block(stmts, loc) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 6520b330af03..8459c2581381 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -297,7 +297,7 @@ impl<'tcx> GotocCtx<'tcx> { // In addition to `def_id` and `substs`, we need to provide the kind of region `env_region` // in `closure_env_ty`, which we can build from the bound variables as follows - let bound_vars = self.tcx.mk_bound_variable_kinds( + let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter( sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))), ); let br = ty::BoundRegion { @@ -314,7 +314,7 @@ impl<'tcx> GotocCtx<'tcx> { // * the rest of attributes are obtained from `sig` let sig = ty::Binder::bind_with_vars( self.tcx.mk_fn_sig( - iter::once(env_ty).chain(iter::once(sig.inputs()[0])), + [env_ty, sig.inputs()[0]], sig.output(), sig.c_variadic, sig.unsafety, @@ -338,7 +338,7 @@ impl<'tcx> GotocCtx<'tcx> { ) -> ty::PolyFnSig<'tcx> { let sig = substs.as_generator().poly_sig(); - let bound_vars = self.tcx.mk_bound_variable_kinds( + let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter( sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))), ); let br = ty::BoundRegion { @@ -346,11 +346,11 @@ impl<'tcx> GotocCtx<'tcx> { kind: ty::BoundRegionKind::BrEnv, }; let env_region = ty::ReLateBound(ty::INNERMOST, br); - let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region(env_region), ty); + let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region_from_kind(env_region), ty); let pin_did = self.tcx.require_lang_item(LangItem::Pin, None); let pin_adt_ref = self.tcx.adt_def(pin_did); - let pin_substs = self.tcx.intern_substs(&[env_ty.into()]); + let pin_substs = self.tcx.mk_substs(&[env_ty.into()]); let env_ty = self.tcx.mk_adt(pin_adt_ref, pin_substs); let sig = sig.skip_binder(); @@ -363,7 +363,7 @@ impl<'tcx> GotocCtx<'tcx> { // The signature should be `Future::poll(_, &mut Context<'_>) -> Poll` let poll_did = tcx.require_lang_item(LangItem::Poll, None); let poll_adt_ref = tcx.adt_def(poll_did); - let poll_substs = tcx.intern_substs(&[sig.return_ty.into()]); + let poll_substs = tcx.mk_substs(&[sig.return_ty.into()]); let ret_ty = tcx.mk_adt(poll_adt_ref, poll_substs); // We have to replace the `ResumeTy` that is used for type and borrow checking @@ -384,7 +384,7 @@ impl<'tcx> GotocCtx<'tcx> { // The signature should be `Generator::resume(_, Resume) -> GeneratorState` let state_did = tcx.require_lang_item(LangItem::GeneratorState, None); let state_adt_ref = tcx.adt_def(state_did); - let state_substs = tcx.intern_substs(&[sig.yield_ty.into(), sig.return_ty.into()]); + let state_substs = tcx.mk_substs(&[sig.yield_ty.into(), sig.return_ty.into()]); let ret_ty = tcx.mk_adt(state_adt_ref, state_substs); (sig.resume_ty, ret_ty) @@ -392,8 +392,8 @@ impl<'tcx> GotocCtx<'tcx> { ty::Binder::bind_with_vars( tcx.mk_fn_sig( - [env_ty, resume_ty].iter(), - &ret_ty, + [env_ty, resume_ty], + ret_ty, false, Unsafety::Normal, rustc_target::spec::abi::Abi::Rust, @@ -423,7 +423,7 @@ impl<'tcx> GotocCtx<'tcx> { impl<'tcx> GotocCtx<'tcx> { pub fn monomorphize(&self, value: T) -> T where - T: TypeFoldable<'tcx>, + T: TypeFoldable>, { // Instance is Some(..) only when current codegen unit is a function. if let Some(current_fn) = &self.current_fn { @@ -937,7 +937,7 @@ impl<'tcx> GotocCtx<'tcx> { let mut final_fields = Vec::with_capacity(flds.len()); let mut offset = initial_offset; for idx in layout.fields.index_by_increasing_offset() { - let fld_offset = offsets[idx]; + let fld_offset = offsets[idx.into()]; let (fld_name, fld_ty) = &flds[idx]; if let Some(padding) = self.codegen_struct_padding(offset, fld_offset, final_fields.len()) @@ -1804,6 +1804,7 @@ impl<'tcx> GotocCtx<'tcx> { let components = fields_shape .index_by_increasing_offset() .map(|idx| { + let idx = idx.into(); let name = fields[idx].name.to_string().intern(); let field_ty = fields[idx].ty(ctx.tcx, adt_substs); let typ = if !ctx.is_zst(field_ty) { @@ -1839,8 +1840,8 @@ impl<'tcx> GotocCtx<'tcx> { while let ty::Adt(adt_def, adt_substs) = typ.kind() { assert_eq!(adt_def.variants().len(), 1, "Expected a single-variant ADT. Found {typ:?}"); let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields; - let last_field = fields.last().expect("Trait should be the last element."); - typ = last_field.ty(self.tcx, adt_substs); + let last_field = fields.last_index().expect("Trait should be the last element."); + typ = fields[last_field].ty(self.tcx, adt_substs); } if typ.is_trait() { Some(typ) } else { None } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index fbd8b583a820..318334805283 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -29,7 +29,7 @@ use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CodegenResults, CrateInfo}; use rustc_data_structures::fx::FxHashMap; use rustc_data_structures::temp_dir::MaybeTempDir; -use rustc_errors::ErrorGuaranteed; +use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; use rustc_hir::def_id::LOCAL_CRATE; use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; @@ -201,6 +201,11 @@ impl CodegenBackend for GotocCodegenBackend { println!("Kani-goto version: {}", env!("CARGO_PKG_VERSION")); } + fn locale_resource(&self) -> &'static str { + // We don't currently support multiple languages. + DEFAULT_LOCALE_RESOURCE + } + fn codegen_crate( &self, tcx: TyCtxt, diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index b260df32f881..9f068850c5f2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -24,9 +24,6 @@ use cbmc::{InternedString, MachineModel}; use kani_metadata::HarnessMetadata; use kani_queries::{QueryDb, UserInput}; use rustc_data_structures::fx::FxHashMap; -use rustc_data_structures::owning_ref::OwningRef; -use rustc_data_structures::rustc_erase_owner; -use rustc_data_structures::sync::MetadataRef; use rustc_middle::mir::interpret::Allocation; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ @@ -34,12 +31,9 @@ use rustc_middle::ty::layout::{ TyAndLayout, }; use rustc_middle::ty::{self, Instance, Ty, TyCtxt}; -use rustc_session::cstore::MetadataLoader; use rustc_span::source_map::{respan, Span}; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; -use rustc_target::spec::Target; -use std::path::Path; pub struct GotocCtx<'tcx> { /// the typing context @@ -396,16 +390,3 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> { } } } - -pub struct GotocMetadataLoader(); -impl MetadataLoader for GotocMetadataLoader { - fn get_rlib_metadata(&self, _: &Target, _filename: &Path) -> Result { - let buf = vec![]; - let buf: OwningRef, [u8]> = OwningRef::new(buf); - Ok(rustc_erase_owner!(buf.map_owner_box())) - } - - fn get_dylib_metadata(&self, target: &Target, filename: &Path) -> Result { - self.get_rlib_metadata(target, filename) - } -} diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index 5a8538ff47b4..a2c3ea3518e9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -34,6 +34,10 @@ impl<'tcx> GotocCtx<'tcx> { } } + pub fn is_user_variable(&self, var: &Local) -> bool { + self.find_debug_info(var).is_some() + } + // Special naming conventions for parameters that are spread from a tuple // into its individual components at the LLVM level, see comment at // compiler/rustc_codegen_llvm/src/gotoc/mod.rs:codegen_function_prelude diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index e618d8ec2163..ee0b8e769bc7 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -138,6 +138,7 @@ impl<'tcx> From<&Statement<'tcx>> for Key { | StatementKind::ConstEvalCounter | StatementKind::FakeRead(_) | StatementKind::Nop + | StatementKind::PlaceMention(_) | StatementKind::Retag(_, _) | StatementKind::StorageLive(_) | StatementKind::StorageDead(_) => Key("Ignored"), @@ -148,11 +149,9 @@ impl<'tcx> From<&Statement<'tcx>> for Key { impl<'tcx> From<&Terminator<'tcx>> for Key { fn from(value: &Terminator<'tcx>) -> Self { match value.kind { - TerminatorKind::Abort => Key("Abort"), TerminatorKind::Assert { .. } => Key("Assert"), TerminatorKind::Call { .. } => Key("Call"), TerminatorKind::Drop { .. } => Key("Drop"), - TerminatorKind::DropAndReplace { .. } => Key("DropAndReplace"), TerminatorKind::GeneratorDrop => Key("GeneratorDrop"), TerminatorKind::Goto { .. } => Key("Goto"), TerminatorKind::FalseEdge { .. } => Key("FalseEdge"), @@ -161,6 +160,7 @@ impl<'tcx> From<&Terminator<'tcx>> for Key { TerminatorKind::Resume => Key("Resume"), TerminatorKind::Return => Key("Return"), TerminatorKind::SwitchInt { .. } => Key("SwitchInt"), + TerminatorKind::Terminate => Key("Terminate"), TerminatorKind::Unreachable => Key("Unreachable"), TerminatorKind::Yield { .. } => Key("Yield"), } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 0a4f5a4c4e8b..4abc3495e6ec 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -5,10 +5,10 @@ use std::collections::BTreeMap; use kani_metadata::{CbmcSolver, HarnessAttributes, Stub}; -use rustc_ast::{AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem}; +use rustc_ast::{attr, AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem}; use rustc_errors::ErrorGuaranteed; use rustc_hir::{def::DefKind, def_id::DefId}; -use rustc_middle::ty::{Instance, TyCtxt}; +use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_span::Span; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; @@ -75,13 +75,13 @@ pub fn is_proof_harness(tcx: TyCtxt, def_id: DefId) -> bool { /// Does this `def_id` have `#[rustc_test_marker]`? pub fn is_test_harness_description(tcx: TyCtxt, def_id: DefId) -> bool { let attrs = tcx.get_attrs_unchecked(def_id); - tcx.sess.contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker) + 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_id: DefId) -> String { let attrs = tcx.get_attrs_unchecked(def_id); - let marker = tcx.sess.find_by_name(attrs, rustc_span::symbol::sym::rustc_test_marker).unwrap(); + let marker = attr::find_by_name(attrs, rustc_span::symbol::sym::rustc_test_marker).unwrap(); parse_str_value(&marker).unwrap() } @@ -133,6 +133,11 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option Iterator for CoerceUnsizedIterator<'tcx> { let CustomCoerceUnsized::Struct(coerce_index) = custom_coerce_unsize_info(self.tcx, src_ty, dst_ty); - assert!(coerce_index < src_fields.len()); + assert!(coerce_index.as_usize() < src_fields.len()); self.src_ty = Some(src_fields[coerce_index].ty(self.tcx, src_substs)); self.dst_ty = Some(dst_fields[coerce_index].ty(self.tcx, dst_substs)); diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 5405da3ef1b2..358ec2149f67 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -65,7 +65,7 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) { // Avoid printing the same error multiple times for different instantiations of the same item. let mut def_ids = HashSet::new(); - for item in items { + for item in items.iter().filter(|i| matches!(i, MonoItem::Fn(..) | MonoItem::Static(..))) { let def_id = item.def_id(); if !def_ids.contains(&def_id) { // Check if any unstable attribute was reached. diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index 03cf5bd5d9f6..aaef3037ad7b 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -8,7 +8,7 @@ use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_ite use crate::kani_middle::stubbing; use crate::kani_middle::ty::query::query_provided::collect_and_partition_mono_items; use kani_queries::{QueryDb, UserInput}; -use rustc_hir::def_id::DefId; +use rustc_hir::def_id::{DefId, LocalDefId}; use rustc_interface; use rustc_middle::{ mir::Body, @@ -18,7 +18,7 @@ use rustc_middle::{ /// Sets up rustc's query mechanism to apply Kani's custom queries to code from /// the present crate. pub fn provide(providers: &mut Providers, queries: &QueryDb) { - providers.optimized_mir = run_mir_passes::; + providers.optimized_mir = run_mir_passes; if queries.get_stubbing_enabled() { providers.collect_and_partition_mono_items = collect_and_partition_mono_items; } @@ -27,23 +27,25 @@ pub fn provide(providers: &mut Providers, queries: &QueryDb) { /// Sets up rustc's query mechanism to apply Kani's custom queries to code from /// external crates. pub fn provide_extern(providers: &mut ExternProviders) { - providers.optimized_mir = run_mir_passes::; + providers.optimized_mir = run_mir_passes_extern; } -/// Returns the optimized code for the function associated with `def_id` by +/// Returns the optimized code for the external function associated with `def_id` by /// running rustc's optimization passes followed by Kani-specific passes. -fn run_mir_passes(tcx: TyCtxt, def_id: DefId) -> &Body { - tracing::debug!(?def_id, "Run rustc transformation passes"); - let optimized_mir = if EXTERN { - rustc_interface::DEFAULT_EXTERN_QUERY_PROVIDERS.optimized_mir - } else { - rustc_interface::DEFAULT_QUERY_PROVIDERS.optimized_mir - }; - let body = optimized_mir(tcx, def_id); - +fn run_mir_passes_extern(tcx: TyCtxt, def_id: DefId) -> &Body { + tracing::debug!(?def_id, "run_mir_passes_extern"); + let body = (rustc_interface::DEFAULT_EXTERN_QUERY_PROVIDERS.optimized_mir)(tcx, def_id); run_kani_mir_passes(tcx, def_id, body) } +/// Returns the optimized code for the local function associated with `def_id` by +/// running rustc's optimization passes followed by Kani-specific passes. +fn run_mir_passes(tcx: TyCtxt, def_id: LocalDefId) -> &Body { + tracing::debug!(?def_id, "run_mir_passes"); + let body = (rustc_interface::DEFAULT_QUERY_PROVIDERS.optimized_mir)(tcx, def_id); + run_kani_mir_passes(tcx, def_id.to_def_id(), body) +} + /// Returns the optimized code for the function associated with `def_id` by /// running Kani-specific passes. The argument `body` should be the optimized /// code rustc generates for this function. diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 5e8144be0d16..c35fdfe18df5 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -237,7 +237,7 @@ struct MonoItemsFnCollector<'a, 'tcx> { impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { fn monomorphize(&self, value: T) -> T where - T: TypeFoldable<'tcx>, + T: TypeFoldable>, { trace!(instance=?self.instance, ?value, "monomorphize"); self.instance.subst_mir_and_normalize_erasing_regions( @@ -305,6 +305,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { | InstanceDef::Item(..) | InstanceDef::ReifyShim(..) | InstanceDef::VTableShim(..) => true, + InstanceDef::ThreadLocalShim(_) | InstanceDef::FnPtrAddrShim(_, _) => true, }; if should_collect && should_codegen_locally(self.tcx, &instance) { trace!(?instance, "collect_instance"); @@ -509,8 +510,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { ); } } - TerminatorKind::Drop { ref place, .. } - | TerminatorKind::DropAndReplace { ref place, .. } => { + TerminatorKind::Drop { ref place, .. } => { let place_ty = place.ty(self.body, self.tcx).ty; let place_mono_ty = self.monomorphize(place_ty); let instance = Instance::resolve_drop_in_place(self.tcx, place_mono_ty); @@ -520,7 +520,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { // We don't support inline assembly. This shall be replaced by an unsupported // construct during codegen. } - TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => { + TerminatorKind::Terminate { .. } | TerminatorKind::Assert { .. } => { // We generate code for this without invoking any lang item. } TerminatorKind::Goto { .. } diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 599806f8de2b..31bf1eb553ff 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -10,10 +10,11 @@ #![feature(extern_types)] #![recursion_limit = "256"] #![feature(box_patterns)] -#![feature(once_cell)] #![feature(rustc_private)] +#![feature(lazy_cell)] #![feature(more_qualified_paths)] #![feature(iter_intersperse)] +extern crate rustc_abi; extern crate rustc_ast; extern crate rustc_ast_pretty; extern crate rustc_codegen_ssa; diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 99d7b7239d05..3900aba5e82f 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -48,7 +48,7 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + Send // Print stack trace. let msg = format!("Kani unexpectedly panicked at {info}.",); let fallback_bundle = - fallback_fluent_bundle(rustc_errors::DEFAULT_LOCALE_RESOURCES, false); + fallback_fluent_bundle(rustc_driver::DEFAULT_LOCALE_RESOURCES.to_vec(), false); let mut emitter = JsonEmitter::basic( false, HumanReadableErrorType::Default(ColorConfig::Never), @@ -71,10 +71,7 @@ pub fn init_session(args: &ArgMatches, json_hook: bool) { // Initialize the rustc logger using value from RUSTC_LOG. We keep the log control separate // because we cannot control the RUSTC log format unless if we match the exact tracing // version used by RUSTC. - // TODO: Enable rustc log when we upgrade the toolchain. - // - // - // rustc_driver::init_rustc_env_logger(); + rustc_driver::init_rustc_env_logger(); // Install Kani panic hook. if json_hook { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 5ce9d4ff0e42..968c1e04951e 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-02-18" +channel = "nightly-2023-04-16" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected b/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected index 59aa1503d9a4..961b5f960b0b 100644 --- a/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected +++ b/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected @@ -1,2 +1 @@ error: Crate crate_with_global_asm contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**). -error: could not compile `crate_with_global_asm` due to 2 previous errors diff --git a/tests/cargo-ui/unstable-attr/invalid/expected b/tests/cargo-ui/unstable-attr/invalid/expected index 66d0c5271668..b3acac173184 100644 --- a/tests/cargo-ui/unstable-attr/invalid/expected +++ b/tests/cargo-ui/unstable-attr/invalid/expected @@ -1,8 +1,8 @@ -error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature("invalid_args")`\ +error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found\ src/lib.rs\ |\ -| #[kani::unstable(feature("invalid_args"))]\ -| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\ +| #[kani::unstable(\ +| ^^^^^^^^^^^^^^^^^^\ |\ = note: expected format: #[kani::unstable(feature="", issue="", reason="")]\ = note: this error originates in the attribute macro `kani::unstable` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/tests/cargo-ui/unstable-attr/invalid/src/lib.rs b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs index f6f55bc112ef..5fbfc768c883 100644 --- a/tests/cargo-ui/unstable-attr/invalid/src/lib.rs +++ b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs @@ -1,6 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +//! All the unstable definitions below should fail. +//! The expected file only contains a generic check since we trigger an ICE for debug builds and +//! we don't guarantee the order that these will be evaluated. +//! TODO: We should break down this test to ensure all of these fail. + #[kani::unstable(reason = "just checking", issue = "")] pub fn missing_feature() { todo!() diff --git a/tests/expected/array/main.rs b/tests/expected/array/main.rs index 1f2e04ed0b5a..44c9ca376a07 100644 --- a/tests/expected/array/main.rs +++ b/tests/expected/array/main.rs @@ -6,11 +6,19 @@ fn foo(x: [i32; 5]) -> [i32; 2] { [x[0], x[1]] } +/// Generate an out-of-bound index with the given length. +/// +/// We use a function to prevent constant progragation, so the out-of-bounds +/// error is not detected at compilation time. +fn oob_index(len: usize) -> usize { + len +} + #[kani::proof] fn main() { let x = [1, 2, 3, 4, 5]; let y = foo(x); - let z = 2; + let z = oob_index(y.len()); assert!(y[0] == 1); assert!(y[1] == 2); assert!(y[z] == 3); diff --git a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs index c249d0a10b7c..79690d9140c1 100644 --- a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs +++ b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs @@ -9,7 +9,7 @@ // run-pass // Test that box-statements with yields in them work. -#![feature(generators, box_syntax, generator_trait)] +#![feature(generators, generator_trait)] use std::ops::Generator; use std::ops::GeneratorState; use std::pin::Pin; @@ -21,14 +21,14 @@ fn main() { //~ WARN unused generator that must be used let y = 2u32; { - let _t = box (&x, yield 0, &y); + let _t = Box::new((&x, yield 0, &y)); } - match box (&x, yield 0, &y) { + match Box::new((&x, yield 0, &y)) { _t => {} } }; - let mut g = |_| box yield; + let mut g = |_| Box::new(yield); assert_eq!(Pin::new(&mut g).resume(1), GeneratorState::Yielded(())); - assert_eq!(Pin::new(&mut g).resume(2), GeneratorState::Complete(box 2)); + assert_eq!(Pin::new(&mut g).resume(2), GeneratorState::Complete(Box::new(2))); } diff --git a/tests/kani/PhantomData/phantom_fixme.rs b/tests/kani/PhantomData/phantom_data.rs similarity index 100% rename from tests/kani/PhantomData/phantom_fixme.rs rename to tests/kani/PhantomData/phantom_data.rs diff --git a/tests/ui/cbmc_checks/pointer/expected b/tests/ui/cbmc_checks/pointer/expected index 5c002065b37f..5a1d87cf2e3d 100644 --- a/tests/ui/cbmc_checks/pointer/expected +++ b/tests/ui/cbmc_checks/pointer/expected @@ -1,5 +1,2 @@ -Failed Checks: dereference failure: pointer NULL -Failed Checks: dereference failure: deallocated dynamic object -Failed Checks: dereference failure: dead object -Failed Checks: dereference failure: pointer outside object bounds -Failed Checks: dereference failure: invalid integer address +Failed Checks: misaligned pointer dereference: address must be a multiple of its type's alignment +Failed Checks: assertion failed: unsafe { *p1 != 0 } diff --git a/tests/ui/cbmc_checks/signed-overflow/expected b/tests/ui/cbmc_checks/signed-overflow/expected index b725337fbddb..143dd683f76f 100644 --- a/tests/ui/cbmc_checks/signed-overflow/expected +++ b/tests/ui/cbmc_checks/signed-overflow/expected @@ -9,5 +9,3 @@ Failed Checks: attempt to shift left with overflow Failed Checks: attempt to shift right with overflow Failed Checks: arithmetic overflow on signed shl Failed Checks: shift operand is negative -Failed Checks: shift distance is negative -Failed Checks: shift distance too large \ No newline at end of file diff --git a/tests/ui/cbmc_checks/unsigned-overflow/expected b/tests/ui/cbmc_checks/unsigned-overflow/expected index ef0f06506b36..fd6e760da3c8 100644 --- a/tests/ui/cbmc_checks/unsigned-overflow/expected +++ b/tests/ui/cbmc_checks/unsigned-overflow/expected @@ -5,4 +5,3 @@ Failed Checks: attempt to subtract with overflow Failed Checks: attempt to multiply with overflow Failed Checks: attempt to shift right with overflow Failed Checks: attempt to shift left with overflow -Failed Checks: shift distance too large diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected index 79e1ac6cb30e..cced065e9f1a 100644 --- a/tests/ui/code-location/expected +++ b/tests/ui/code-location/expected @@ -1,6 +1,6 @@ module/mod.rs:10:5 in function module::not_empty main.rs:13:5 in function same_file /toolchains/ -alloc/src/vec/mod.rs:3030:81 in function as std::ops::Drop>::drop +alloc/src/vec/mod.rs:3018:81 in function as std::ops::Drop>::drop VERIFICATION:- SUCCESSFUL diff --git a/tests/ui/should-panic-attribute/no-panics/expected b/tests/ui/should-panic-attribute/no-panics/expected index 37cd42b86d22..be42df7fb7f6 100644 --- a/tests/ui/should-panic-attribute/no-panics/expected +++ b/tests/ui/should-panic-attribute/no-panics/expected @@ -1,4 +1,5 @@ -- Status: SUCCESS\ -- Description: "assertion failed: 1 + 1 == 2" - ** 0 of 1 failed +check.assertion\ +SUCCESS\ +assertion failed: 1 + 1 == 2 + VERIFICATION:- FAILED (encountered no panics, but at least one was expected) diff --git a/tests/ui/should-panic-attribute/unexpected-failures/expected b/tests/ui/should-panic-attribute/unexpected-failures/expected index 513744fa06fb..6cd10b4bafd5 100644 --- a/tests/ui/should-panic-attribute/unexpected-failures/expected +++ b/tests/ui/should-panic-attribute/unexpected-failures/expected @@ -1,8 +1,9 @@ -overflow.undefined-shift.1\ -- Status: FAILURE\ -- Description: "shift distance too large" -Failed Checks: attempt to shift left with overflow +undefined-shift\ +Status: FAILURE\ +Description: "shift distance too large" + Failed Checks: panicked on the `1` arm! Failed Checks: panicked on the `0` arm! Failed Checks: shift distance too large + VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected) diff --git a/tests/ui/should-panic-attribute/unexpected-failures/test.rs b/tests/ui/should-panic-attribute/unexpected-failures/test.rs index 776bc87d3b62..625a15c89683 100644 --- a/tests/ui/should-panic-attribute/unexpected-failures/test.rs +++ b/tests/ui/should-panic-attribute/unexpected-failures/test.rs @@ -3,10 +3,11 @@ //! Checks that verfication fails when `#[kani::should_panic]` is used but not //! all failures encountered are panics. +#![feature(unchecked_math)] fn trigger_overflow() { let x: u32 = kani::any(); - let _ = 42 << x; + let _ = unsafe { 42u32.unchecked_shl(x) }; } #[kani::proof] diff --git a/tools/bookrunner/librustdoc/doctest.rs b/tools/bookrunner/librustdoc/doctest.rs index 58f6ea8d1b18..5d11ea7ec55b 100644 --- a/tools/bookrunner/librustdoc/doctest.rs +++ b/tools/bookrunner/librustdoc/doctest.rs @@ -4,6 +4,7 @@ // See GitHub history for details. use rustc_ast as ast; use rustc_data_structures::sync::Lrc; +use rustc_driver::DEFAULT_LOCALE_RESOURCES; use rustc_errors::{ColorConfig, TerminalUrl}; use rustc_span::edition::Edition; use rustc_span::source_map::SourceMap; @@ -79,7 +80,7 @@ pub fn make_test( let sm = Lrc::new(SourceMap::new(FilePathMapping::empty())); let fallback_bundle = - rustc_errors::fallback_fluent_bundle(rustc_errors::DEFAULT_LOCALE_RESOURCES, false); + rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false); supports_color = EmitterWriter::stderr( ColorConfig::Auto, None, @@ -95,7 +96,7 @@ pub fn make_test( .supports_color(); let emitter = EmitterWriter::new( - box io::sink(), + Box::new(io::sink()), None, None, fallback_bundle, @@ -109,7 +110,7 @@ pub fn make_test( ); // FIXME(misdreavus): pass `-Z treat-err-as-bug` to the doctest parser - let handler = Handler::with_emitter(false, None, box emitter); + let handler = Handler::with_emitter(false, None, Box::new(emitter)); let sess = ParseSess::with_span_handler(handler, sm); let mut found_main = false; diff --git a/tools/bookrunner/librustdoc/lib.rs b/tools/bookrunner/librustdoc/lib.rs index 57ae24335c2a..9046478cf502 100644 --- a/tools/bookrunner/librustdoc/lib.rs +++ b/tools/bookrunner/librustdoc/lib.rs @@ -11,10 +11,8 @@ #![feature(assert_matches)] #![feature(box_patterns)] #![feature(control_flow_enum)] -#![feature(box_syntax)] #![feature(test)] #![feature(never_type)] -#![feature(once_cell)] #![feature(type_ascription)] #![feature(iter_intersperse)] #![recursion_limit = "256"] diff --git a/tools/compiletest/src/header.rs b/tools/compiletest/src/header.rs index afb9057ad451..89e3603a8510 100644 --- a/tools/compiletest/src/header.rs +++ b/tools/compiletest/src/header.rs @@ -233,5 +233,11 @@ pub fn make_test_description( compile_fail: false, no_run: false, test_type: test::TestType::Unknown, + // Enter dummy values since the test doesn't have a line per-se. + source_file: "unknown_file", + start_line: 0, + start_col: 0, + end_line: 0, + end_col: 0, } }