From b824e448f7be5d83f03d1666ac418daa1301620a Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 3 Aug 2023 21:08:01 +0000 Subject: [PATCH 01/13] bump nihtly to 2023-08-03 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index f672b2397f5a..855a4d3ee2e6 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-07-01" +channel = "nightly-2023-08-03" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 85aa5a30316dbb93b13fe5f6ff3eccc61781996d Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 3 Aug 2023 22:51:58 +0000 Subject: [PATCH 02/13] propagate refactors --- Cargo.lock | 59 ++++++++++--------- .../codegen/intrinsic.rs | 10 ++-- .../codegen_cprover_gotoc/codegen/operand.rs | 2 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 20 +++---- .../codegen/static_var.rs | 6 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 36 +++++------ .../src/codegen_cprover_gotoc/utils/names.rs | 2 +- kani-compiler/src/kani_middle/reachability.rs | 8 +-- 8 files changed, 73 insertions(+), 70 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index c1579b23041d..ae781d4b0003 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -162,9 +162,12 @@ dependencies = [ [[package]] name = "cc" -version = "1.0.79" +version = "1.0.81" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "50d30906286121d95be3d479533b458f87493b30a4b5f79a607db8f5d11aa91f" +checksum = "6c6b2562119bf28c3439f7f02db99faf0aa1a8cdfe5772a2ee155d32227239f0" +dependencies = [ + "libc", +] [[package]] name = "cfg-if" @@ -205,7 +208,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] @@ -365,9 +368,9 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" -version = "0.3.1" +version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a" +checksum = "6b30f669a7961ef1631673d2766cc92f52d64f7ef354d4fe0ddfd30ed52f0f4f" dependencies = [ "errno-dragonfly", "libc", @@ -553,7 +556,7 @@ dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] @@ -590,9 +593,9 @@ dependencies = [ [[package]] name = "linux-raw-sys" -version = "0.4.3" +version = "0.4.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09fc20d2ca12cb9f044c93e3bd6d32d523e6e2ec3db4f7b2939cd99026ecd3f0" +checksum = "57bcfdad1b858c2db7c38303a6d2ad4dfaf5eb53dfeb0910128b2c26d6158503" [[package]] name = "lock_api" @@ -933,7 +936,7 @@ checksum = "b2eae68fc220f7cf2532e4494aded17545fce192d59cd996e0fe7887f4ceb575" dependencies = [ "aho-corasick", "memchr", - "regex-automata 0.3.3", + "regex-automata 0.3.4", "regex-syntax 0.7.4", ] @@ -948,9 +951,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.3.3" +version = "0.3.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "39354c10dd07468c2e73926b23bb9c2caca74c5501e38a35da70406f1d923310" +checksum = "b7b6d6190b7594385f61bd3911cd1be99dfddcfc365a4160cc2ab5bff4aed294" dependencies = [ "aho-corasick", "memchr", @@ -984,9 +987,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.4" +version = "0.38.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0a962918ea88d644592894bc6dc55acc6c0956488adcebbfb6e273506b7fd6e5" +checksum = "1ee020b1716f0a80e2ace9b03441a749e402e86712f15f16fe8a8f75afac732f" dependencies = [ "bitflags 2.3.3", "errno", @@ -1033,29 +1036,29 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.175" +version = "1.0.180" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5d25439cd7397d044e2748a6fe2432b5e85db703d6d097bd014b3c0ad1ebff0b" +checksum = "0ea67f183f058fe88a4e3ec6e2788e003840893b91bac4559cabedd00863b3ed" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.175" +version = "1.0.180" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b23f7ade6f110613c0d63858ddb8b94c1041f550eab58a16b371bdf2c9c80ab4" +checksum = "24e744d7782b686ab3b73267ef05697159cc0e5abbed3f47f9933165e5219036" dependencies = [ "proc-macro2", "quote", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] name = "serde_json" -version = "1.0.103" +version = "1.0.104" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d03b412469450d4404fe8499a268edd7f8b79fecb074b0d812ad64ca21f4031b" +checksum = "076066c5f1078eac5b722a31827a8832fe108bed65dfa75e233c89f8206e976c" dependencies = [ "itoa", "ryu", @@ -1073,9 +1076,9 @@ dependencies = [ [[package]] name = "serde_test" -version = "1.0.175" +version = "1.0.176" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "29baf0f77ca9ad9c6ed46e1b408b5e0f30b5184bcd66884e7f6d36bd7a65a8a4" +checksum = "5a2f49ace1498612d14f7e0b8245519584db8299541dfe31a06374a828d620ab" dependencies = [ "serde", ] @@ -1200,9 +1203,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.27" +version = "2.0.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b60f673f44a8255b9c8c657daf66a596d435f2da81a555b06dc644d080ba45e0" +checksum = "04361975b3f5e348b2189d8dc55bc942f278b2d482a6a0365de5bdd62d351567" dependencies = [ "proc-macro2", "quote", @@ -1226,7 +1229,7 @@ checksum = "090198534930841fab3a5d1bb637cde49e339654e606195f8d9c76eeb081dc96" dependencies = [ "proc-macro2", "quote", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] @@ -1293,7 +1296,7 @@ checksum = "5f4f31f56159e98206da9efd823404b79b6ef3143b4a7ab76e67b1751b25a4ab" dependencies = [ "proc-macro2", "quote", - "syn 2.0.27", + "syn 2.0.28", ] [[package]] @@ -1595,9 +1598,9 @@ checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" [[package]] name = "winnow" -version = "0.5.1" +version = "0.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "25b5872fa2e10bd067ae946f927e726d7d603eaeb6e02fa6a350e0722d2b8c11" +checksum = "f46aab759304e4d7b2075a9aecba26228bb073ee8c50db796b2c72c676b5d807" dependencies = [ "memchr", ] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 0f4279a97a14..10fe28caf9bd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -245,7 +245,7 @@ impl<'tcx> GotocCtx<'tcx> { macro_rules! codegen_size_align { ($which: ident) => {{ - let tp_ty = instance.substs.type_at(0); + let tp_ty = instance.args.type_at(0); let arg = fargs.remove(0); let size_align = self.size_and_align_of_dst(tp_ty, arg); self.codegen_expr_to_place(p, size_align.$which) @@ -422,7 +422,7 @@ impl<'tcx> GotocCtx<'tcx> { "cttz" => codegen_count_intrinsic!(cttz, true), "cttz_nonzero" => codegen_count_intrinsic!(cttz, false), "discriminant_value" => { - let ty = instance.substs.type_at(0); + let ty = instance.args.type_at(0); let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty); self.codegen_expr_to_place(p, e) } @@ -764,7 +764,7 @@ impl<'tcx> GotocCtx<'tcx> { intrinsic: &str, span: Option, ) -> Stmt { - let ty = instance.substs.type_at(0); + let ty = instance.args.type_at(0); let layout = self.layout_of(ty); // Note: We follow the pattern seen in `codegen_panic_intrinsic` from `rustc_codegen_ssa` // https://github.com/rust-lang/rust/blob/master/compiler/rustc_codegen_ssa/src/mir/block.rs @@ -1034,7 +1034,7 @@ impl<'tcx> GotocCtx<'tcx> { let offset = fargs.remove(0); // Check that computing `offset` in bytes would not overflow - let ty = self.monomorphize(instance.substs.type_at(0)); + let ty = self.monomorphize(instance.args.type_at(0)); let (offset_bytes, bytes_overflow_check) = self.count_in_bytes(offset.clone(), ty, Type::ssize_t(), intrinsic, loc); @@ -1184,7 +1184,7 @@ impl<'tcx> GotocCtx<'tcx> { p: &Place<'tcx>, loc: Location, ) -> Stmt { - let ty = self.monomorphize(instance.substs.type_at(0)); + let ty = self.monomorphize(instance.args.type_at(0)); let dst = fargs.remove(0).cast_to(Type::void_pointer()); let val = fargs.remove(0).cast_to(Type::void_pointer()); let layout = self.layout_of(ty); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 23211f022b23..18aa1871e510 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -699,7 +699,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_fndef( &mut self, d: DefId, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, span: Option<&Span>, ) -> Expr { let instance = diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index bfb3313a5ae9..ee269aba16a1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -20,7 +20,7 @@ use num::bigint::BigInt; use rustc_abi::FieldIdx; use rustc_index::IndexVec; use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp}; -use rustc_middle::ty::adjustment::PointerCast; +use rustc_middle::ty::adjustment::PointerCoercion; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry}; use rustc_target::abi::{FieldsShape, Size, TagEncoding, VariantIdx, Variants}; @@ -706,7 +706,7 @@ impl<'tcx> GotocCtx<'tcx> { "https://github.com/model-checking/kani/issues/1784", ) } - Rvalue::Cast(CastKind::Pointer(k), e, t) => { + Rvalue::Cast(CastKind::PointerCoercion(k), e, t) => { let t = self.monomorphize(*t); self.codegen_pointer_cast(k, e, t, loc) } @@ -991,19 +991,19 @@ impl<'tcx> GotocCtx<'tcx> { } /// "Pointer casts" are particular kinds of pointer-to-pointer casts. - /// See the [`PointerCast`] type for specifics. + /// See the [`PointerCoercion`] type for specifics. /// Note that this does not include all casts involving pointers, /// many of which are instead handled by [`Self::codegen_misc_cast`] instead. fn codegen_pointer_cast( &mut self, - k: &PointerCast, + k: &PointerCoercion, operand: &Operand<'tcx>, t: Ty<'tcx>, loc: Location, ) -> Expr { debug!(cast=?k, op=?operand, ?loc, "codegen_pointer_cast"); match k { - PointerCast::ReifyFnPointer => match self.operand_ty(operand).kind() { + PointerCoercion::ReifyFnPointer => match self.operand_ty(operand).kind() { ty::FnDef(def_id, substs) => { let instance = Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, substs) @@ -1015,8 +1015,8 @@ impl<'tcx> GotocCtx<'tcx> { } _ => unreachable!(), }, - PointerCast::UnsafeFnPointer => self.codegen_operand(operand), - PointerCast::ClosureFnPointer(_) => { + PointerCoercion::UnsafeFnPointer => self.codegen_operand(operand), + PointerCoercion::ClosureFnPointer(_) => { if let ty::Closure(def_id, substs) = self.operand_ty(operand).kind() { let instance = Instance::resolve_closure( self.tcx, @@ -1031,8 +1031,8 @@ impl<'tcx> GotocCtx<'tcx> { unreachable!("{:?} cannot be cast to a fn ptr", operand) } } - PointerCast::MutToConstPointer => self.codegen_operand(operand), - PointerCast::ArrayToPointer => { + PointerCoercion::MutToConstPointer => self.codegen_operand(operand), + PointerCoercion::ArrayToPointer => { // TODO: I am not sure whether it is correct or not. // // some reasoning is as follows. @@ -1054,7 +1054,7 @@ impl<'tcx> GotocCtx<'tcx> { _ => unreachable!(), } } - PointerCast::Unsize => { + PointerCoercion::Unsize => { let src_goto_expr = self.codegen_operand(operand); let src_mir_type = self.operand_ty(operand); let dst_mir_type = t; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs index e71bea1f2066..13e4a5402e06 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -7,7 +7,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Symbol; use rustc_hir::def_id::DefId; use rustc_middle::mir::mono::MonoItem; -use rustc_middle::ty::{subst::InternalSubsts, Instance}; +use rustc_middle::ty::{GenericArgs, Instance}; use tracing::debug; impl<'tcx> GotocCtx<'tcx> { @@ -28,10 +28,10 @@ impl<'tcx> GotocCtx<'tcx> { // Unique mangled monomorphized name. let symbol_name = item.symbol_name(self.tcx).to_string(); // Pretty name which may include function name. - let pretty_name = Instance::new(def_id, InternalSubsts::empty()).to_string(); + let pretty_name = Instance::new(def_id, GenericArgs::empty()).to_string(); debug!(?symbol_name, ?pretty_name, "declare_static {}", item); - let typ = self.codegen_ty(self.tcx.type_of(def_id).subst_identity()); + let typ = self.codegen_ty(self.tcx.type_of(def_id).instantiate_identity()); let span = self.tcx.def_span(def_id); let location = self.codegen_span(&span); let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 881dec1765f9..b581624ee707 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -12,9 +12,9 @@ use rustc_middle::mir::{HasLocalDecls, Local, Operand, Place, Rvalue}; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::print::FmtPrinter; -use rustc_middle::ty::subst::InternalSubsts; +use rustc_middle::ty::GenericArgsRef; use rustc_middle::ty::{ - self, AdtDef, Const, FloatTy, GeneratorSubsts, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind, + self, AdtDef, Const, FloatTy, GeneratorArgs, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind, UintTy, VariantDef, VtblEntry, }; use rustc_middle::ty::{List, TypeFoldable}; @@ -291,7 +291,7 @@ impl<'tcx> GotocCtx<'tcx> { fn closure_sig( &self, def_id: DefId, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, ) -> ty::PolyFnSig<'tcx> { let sig = self.monomorphize(substs.as_closure().sig()); @@ -334,7 +334,7 @@ impl<'tcx> GotocCtx<'tcx> { &self, did: &DefId, ty: Ty<'tcx>, - substs: ty::subst::SubstsRef<'tcx>, + substs: ty::GenericArgsRef<'tcx>, ) -> ty::PolyFnSig<'tcx> { let sig = substs.as_generator().poly_sig(); @@ -350,7 +350,7 @@ impl<'tcx> GotocCtx<'tcx> { 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.mk_substs(&[env_ty.into()]); + let pin_substs = self.tcx.mk_args(&[env_ty.into()]); let env_ty = self.tcx.mk_adt(pin_adt_ref, pin_substs); let sig = sig.skip_binder(); @@ -363,8 +363,8 @@ 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.mk_substs(&[sig.return_ty.into()]); - let ret_ty = tcx.mk_adt(poll_adt_ref, poll_substs); + let poll_substs = tcx.mk_args(&[sig.return_ty.into()]); + let ret_ty = tcx.mk_adt_def(poll_adt_ref, poll_substs); // We have to replace the `ResumeTy` that is used for type and borrow checking // with `&mut Context<'_>` which is used in codegen. @@ -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.mk_substs(&[sig.yield_ty.into(), sig.return_ty.into()]); + let state_substs = tcx.mk_args(&[sig.yield_ty.into(), sig.return_ty.into()]); let ret_ty = tcx.mk_adt(state_adt_ref, state_substs); (sig.resume_ty, ret_ty) @@ -982,7 +982,7 @@ impl<'tcx> GotocCtx<'tcx> { /// A closure is a struct of all its environments. That is, a closure is /// just a tuple with a unique type identifier, so that Fn related traits /// can find its impl. - fn codegen_ty_closure(&mut self, t: Ty<'tcx>, substs: ty::subst::SubstsRef<'tcx>) -> Type { + fn codegen_ty_closure(&mut self, t: Ty<'tcx>, substs: ty::GenericArgsRef<'tcx>) -> Type { self.ensure_struct(self.ty_mangled_name(t), self.ty_pretty_name(t), |ctx, _| { ctx.codegen_ty_tuple_like(t, substs.as_closure().upvar_tys().collect()) }) @@ -1091,7 +1091,7 @@ impl<'tcx> GotocCtx<'tcx> { }; let mut fields = vec![direct_fields]; for var_idx in variants.indices() { - let variant_name = GeneratorSubsts::variant_name(var_idx).into(); + let variant_name = GeneratorArgs::variant_name(var_idx).into(); fields.push(DatatypeComponent::Field { name: ctx.generator_variant_name(var_idx), typ: ctx.codegen_generator_variant_struct( @@ -1156,7 +1156,7 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn generator_variant_name(&self, var_idx: VariantIdx) -> InternedString { - format!("generator_variant_{}", GeneratorSubsts::variant_name(var_idx)).into() + format!("generator_variant_{}", GeneratorArgs::variant_name(var_idx)).into() } pub fn generator_field_name(&self, field_idx: usize) -> InternedString { @@ -1346,7 +1346,7 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, ty: Ty<'tcx>, def: &'tcx AdtDef, - subst: &'tcx InternalSubsts<'tcx>, + subst: &'tcx GenericArgsRef<'tcx>, ) -> Type { self.ensure_struct(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |ctx, _| { let variant = &def.variants().raw[0]; @@ -1359,7 +1359,7 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_variant_struct_fields( &mut self, variant: &VariantDef, - subst: &'tcx InternalSubsts<'tcx>, + subst: &'tcx GenericArgsRef<'tcx>, layout: &LayoutS, initial_offset: Size, ) -> Vec { @@ -1373,7 +1373,7 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, ty: Ty<'tcx>, def: &'tcx AdtDef, - subst: &'tcx InternalSubsts<'tcx>, + subst: &'tcx GenericArgsRef<'tcx>, ) -> Type { self.ensure_union(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |ctx, _| { def.variants().raw[0] @@ -1425,7 +1425,7 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, ty: Ty<'tcx>, adtdef: &'tcx AdtDef, - subst: &'tcx InternalSubsts<'tcx>, + subst: &'tcx GenericArgsRef<'tcx>, ) -> Type { let pretty_name = self.ty_pretty_name(ty); // variants appearing in source code (in source code order) @@ -1528,7 +1528,7 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, ty: Ty<'tcx>, adtdef: &'tcx AdtDef, - subst: &'tcx InternalSubsts<'tcx>, + subst: &'tcx GenericArgsRef<'tcx>, variants: &IndexVec, ) -> Type { let non_zst_count = variants.iter().filter(|layout| layout.size.bytes() > 0).count(); @@ -1631,7 +1631,7 @@ impl<'tcx> GotocCtx<'tcx> { name: InternedString, pretty_name: InternedString, def: &'tcx AdtDef, - subst: &'tcx InternalSubsts<'tcx>, + subst: &'tcx GenericArgsRef<'tcx>, layouts: &IndexVec, initial_offset: Size, ) -> Vec { @@ -1663,7 +1663,7 @@ impl<'tcx> GotocCtx<'tcx> { name: InternedString, pretty_name: InternedString, case: &VariantDef, - subst: &'tcx InternalSubsts<'tcx>, + subst: &'tcx GenericArgsRef<'tcx>, variant: &LayoutS, initial_offset: Size, ) -> Type { diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index a2c3ea3518e9..e5e34ffc114c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -55,7 +55,7 @@ impl<'tcx> GotocCtx<'tcx> { /// A human readable name in Rust for reference, should not be used as a key. pub fn readable_instance_name(&self, instance: Instance<'tcx>) -> String { with_no_trimmed_paths!( - self.tcx.def_path_str_with_substs(instance.def_id(), instance.substs) + self.tcx.def_path_str_with_substs(instance.def_id(), instance.args) ) } diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index a3110426dc57..214fa7ac51cb 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -28,7 +28,7 @@ use rustc_middle::mir::{ Body, CastKind, Constant, ConstantKind, Location, Rvalue, Terminator, TerminatorKind, }; use rustc_middle::span_bug; -use rustc_middle::ty::adjustment::PointerCast; +use rustc_middle::ty::adjustment::PointerCoercion; use rustc_middle::ty::{ Closure, ClosureKind, ConstKind, EarlyBinder, Instance, InstanceDef, ParamEnv, Ty, TyCtxt, TyKind, TypeFoldable, VtblEntry, @@ -355,7 +355,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { trace!(rvalue=?*rvalue, "visit_rvalue"); match *rvalue { - Rvalue::Cast(CastKind::Pointer(PointerCast::Unsize), ref operand, target) => { + Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::Unsize), ref operand, target) => { // Check if the conversion include casting a concrete type to a trait type. // If so, collect items from the impl `Trait for Concrete {}`. let target_ty = self.monomorphize(target); @@ -367,7 +367,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { self.collect_vtable_methods(base_coercion.src_ty, base_coercion.dst_ty); } } - Rvalue::Cast(CastKind::Pointer(PointerCast::ReifyFnPointer), ref operand, _) => { + Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::ReifyFnPointer), ref operand, _) => { let fn_ty = operand.ty(self.body, self.tcx); let fn_ty = self.monomorphize(fn_ty); if let TyKind::FnDef(def_id, substs) = *fn_ty.kind() { @@ -383,7 +383,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { unreachable!("Expected FnDef type, but got: {:?}", fn_ty); } } - Rvalue::Cast(CastKind::Pointer(PointerCast::ClosureFnPointer(_)), ref operand, _) => { + Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::ClosureFnPointer(_)), ref operand, _) => { let source_ty = operand.ty(self.body, self.tcx); let source_ty = self.monomorphize(source_ty); match *source_ty.kind() { From 691f8c65d7e06085ba35ceb561bcb03bec160985 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 3 Aug 2023 23:14:03 +0000 Subject: [PATCH 03/13] rewrite tctx.mk_x(...) -> Ty::new_x(tctx, ...) --- .../src/codegen_cprover_gotoc/codegen/place.rs | 10 +++++----- .../src/codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 11 ++++++----- .../src/codegen_cprover_gotoc/utils/names.rs | 2 +- kani-compiler/src/kani_middle/coercion.rs | 2 +- 5 files changed, 14 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 4482ee1d1f84..2687a4d8cfe9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -512,14 +512,14 @@ impl<'tcx> GotocCtx<'tcx> { // https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html match before.mir_typ().kind() { ty::Array(ty, len) => { - let len = len.kind().try_to_target_usize(self.tcx).unwrap(); + let len = len.try_to_target_usize(self.tcx).unwrap(); let subarray_len = if from_end { // `to` counts from the end of the array len - to - from } else { to - from }; - let typ = self.tcx.mk_array(*ty, subarray_len); + let typ = Ty::new_array(self.tcx, *ty, subarray_len); let goto_typ = self.codegen_ty(typ); // unimplemented Err(UnimplementedData::new( @@ -541,9 +541,9 @@ impl<'tcx> GotocCtx<'tcx> { } else { Expr::int_constant(to - from, Type::size_t()) }; - let typ = self.tcx.mk_slice(*elemt); + let typ = Ty::new_slice(self.tcx, *elemt); let typ_and_mut = TypeAndMut { ty: typ, mutbl: Mutability::Mut }; - let ptr_typ = self.tcx.mk_ptr(typ_and_mut); + let ptr_typ = Ty::new_ptr(self.tcx, typ_and_mut); let goto_type = self.codegen_ty(ptr_typ); let index = Expr::int_constant(from, Type::ssize_t()); @@ -703,7 +703,7 @@ impl<'tcx> GotocCtx<'tcx> { match before.mir_typ().kind() { //TODO, ask on zulip if we can ever have from_end here? ty::Array(elemt, length) => { - let length = length.kind().try_to_target_usize(self.tcx).unwrap(); + let length = length.try_to_target_usize(self.tcx).unwrap(); assert!(length >= min_length); let idx = if from_end { length - offset } else { offset }; let idxe = Expr::int_constant(idx, Type::ssize_t()); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index ee269aba16a1..b22d89aea1de 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -738,7 +738,7 @@ impl<'tcx> GotocCtx<'tcx> { // See https://github.com/rust-lang/compiler-team/issues/460 for more details. let operand = self.codegen_operand(operand); let t = self.monomorphize(*content_ty); - let box_ty = self.tcx.mk_box(t); + let box_ty = Ty::new_box(self.tcx, t); let box_ty = self.codegen_ty(box_ty); let cbmc_t = self.codegen_ty(t); let box_contents = operand.cast_to(cbmc_t.to_pointer()); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index b581624ee707..c630b743779f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -346,12 +346,12 @@ impl<'tcx> GotocCtx<'tcx> { kind: ty::BoundRegionKind::BrEnv, }; let env_region = ty::ReLateBound(ty::INNERMOST, br); - let env_ty = self.tcx.mk_mut_ref(ty::Region::new_from_kind(self.tcx, env_region), ty); + let env_ty = Ty::new_mut_ref(self.tcx, ty::Region::new_from_kind(self.tcx, 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.mk_args(&[env_ty.into()]); - let env_ty = self.tcx.mk_adt(pin_adt_ref, pin_substs); + let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_substs); let sig = sig.skip_binder(); // The `FnSig` and the `ret_ty` here is for a generators main @@ -364,6 +364,7 @@ impl<'tcx> GotocCtx<'tcx> { let poll_did = tcx.require_lang_item(LangItem::Poll, None); let poll_adt_ref = tcx.adt_def(poll_did); let poll_substs = tcx.mk_args(&[sig.return_ty.into()]); + // TODO figure out where this one went let ret_ty = tcx.mk_adt_def(poll_adt_ref, poll_substs); // We have to replace the `ResumeTy` that is used for type and borrow checking @@ -377,7 +378,7 @@ impl<'tcx> GotocCtx<'tcx> { panic!("expected `ResumeTy`, found `{:?}`", sig.resume_ty); }; } - let context_mut_ref = tcx.mk_task_context(); + let context_mut_ref = Ty::new_task_context(tcx); (context_mut_ref, ret_ty) } else { @@ -385,7 +386,7 @@ impl<'tcx> GotocCtx<'tcx> { let state_did = tcx.require_lang_item(LangItem::GeneratorState, None); let state_adt_ref = tcx.adt_def(state_did); let state_substs = tcx.mk_args(&[sig.yield_ty.into(), sig.return_ty.into()]); - let ret_ty = tcx.mk_adt(state_adt_ref, state_substs); + let ret_ty = Ty::new_adt(tcx, state_adt_ref, state_substs); (sig.resume_ty, ret_ty) }; @@ -1610,7 +1611,7 @@ impl<'tcx> GotocCtx<'tcx> { Primitive::F32 => self.tcx.types.f32, Primitive::F64 => self.tcx.types.f64, Primitive::Pointer(_) => { - self.tcx.mk_ptr(ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not }) + Ty::new_ptr(self.tcx, ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not }) } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index e5e34ffc114c..c9f93a50cd2f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -55,7 +55,7 @@ impl<'tcx> GotocCtx<'tcx> { /// A human readable name in Rust for reference, should not be used as a key. pub fn readable_instance_name(&self, instance: Instance<'tcx>) -> String { with_no_trimmed_paths!( - self.tcx.def_path_str_with_substs(instance.def_id(), instance.args) + self.tcx.def_path_str_with_args(instance.def_id(), instance.args) ) } diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 42f3cfb0a702..bfebc5414386 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -216,7 +216,7 @@ fn custom_coerce_unsize_info<'tcx>( let trait_ref = ty::Binder::dummy(TraitRef::new( tcx, def_id, - tcx.mk_substs_trait(source_ty, [target_ty.into()]), + tcx.mk_args_trait(source_ty, [target_ty.into()]), )); match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) { From e4514d78946ebbe4678f0e23fdbd996d7288d92a Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 3 Aug 2023 23:38:41 +0000 Subject: [PATCH 04/13] final fix --- .../codegen_cprover_gotoc/codegen/function.rs | 2 +- .../codegen_cprover_gotoc/codegen/operand.rs | 6 +-- .../codegen_cprover_gotoc/codegen/place.rs | 2 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 8 +-- .../src/codegen_cprover_gotoc/codegen/typ.rs | 52 +++++++++---------- kani-compiler/src/kani_middle/coercion.rs | 10 ++-- kani-compiler/src/kani_middle/reachability.rs | 4 +- 7 files changed, 42 insertions(+), 42 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 800ec8219e40..77d68af745ae 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -187,7 +187,7 @@ impl<'tcx> GotocCtx<'tcx> { let tupe = sig.inputs().last().unwrap(); let args = match tupe.kind() { - ty::Tuple(substs) => *substs, + ty::Tuple(args) => *args, _ => unreachable!("a function's spread argument must be a tuple"), }; let starting_idx = sig.inputs().len(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 18aa1871e510..dac8ec2c51a8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -139,7 +139,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), + ty::FnDef(d, args) => self.codegen_fndef(*d, args, span), _ => Expr::init_unit(self.codegen_ty(lit_ty), &self.symbol_table), }, } @@ -699,11 +699,11 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_fndef( &mut self, d: DefId, - substs: ty::GenericArgsRef<'tcx>, + args: ty::GenericArgsRef<'tcx>, span: Option<&Span>, ) -> Expr { let instance = - Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, substs).unwrap().unwrap(); + Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, args).unwrap().unwrap(); self.codegen_fn_item(instance, span) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 2687a4d8cfe9..b9e8513c497d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -367,7 +367,7 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_local_fndef(&mut self, ty: ty::Ty<'tcx>) -> Option { match ty.kind() { // A local that is itself a FnDef, like Fn::call_once - ty::FnDef(defid, substs) => Some(self.codegen_fndef(*defid, substs, None)), + ty::FnDef(defid, args) => Some(self.codegen_fndef(*defid, args, None)), // A local can be pointer to a FnDef, like Fn::call and Fn::call_mut ty::RawPtr(inner) => self .codegen_local_fndef(inner.ty) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index b22d89aea1de..da114ad6cd58 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1004,9 +1004,9 @@ impl<'tcx> GotocCtx<'tcx> { debug!(cast=?k, op=?operand, ?loc, "codegen_pointer_cast"); match k { PointerCoercion::ReifyFnPointer => match self.operand_ty(operand).kind() { - ty::FnDef(def_id, substs) => { + ty::FnDef(def_id, args) => { let instance = - Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, substs) + Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args) .unwrap() .unwrap(); // We need to handle this case in a special way because `codegen_operand` compiles FnDefs to dummy structs. @@ -1017,11 +1017,11 @@ impl<'tcx> GotocCtx<'tcx> { }, PointerCoercion::UnsafeFnPointer => self.codegen_operand(operand), PointerCoercion::ClosureFnPointer(_) => { - if let ty::Closure(def_id, substs) = self.operand_ty(operand).kind() { + if let ty::Closure(def_id, args) = self.operand_ty(operand).kind() { let instance = Instance::resolve_closure( self.tcx, *def_id, - substs, + args, ty::ClosureKind::FnOnce, ) .expect("failed to normalize and resolve closure during codegen") diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index c630b743779f..07868ab11609 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -263,7 +263,7 @@ impl<'tcx> GotocCtx<'tcx> { let fn_sig = sig.skip_binder(); if let Some((tupe, prev_args)) = fn_sig.inputs().split_last() { let args = match *tupe.kind() { - ty::Tuple(substs) => substs, + ty::Tuple(args) => args, _ => unreachable!("the final argument of a closure must be a tuple"), }; @@ -291,11 +291,11 @@ impl<'tcx> GotocCtx<'tcx> { fn closure_sig( &self, def_id: DefId, - substs: ty::GenericArgsRef<'tcx>, + args: ty::GenericArgsRef<'tcx>, ) -> ty::PolyFnSig<'tcx> { - let sig = self.monomorphize(substs.as_closure().sig()); + let sig = self.monomorphize(args.as_closure().sig()); - // In addition to `def_id` and `substs`, we need to provide the kind of region `env_region` + // In addition to `def_id` and `args`, 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_from_iter( sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))), @@ -305,7 +305,7 @@ impl<'tcx> GotocCtx<'tcx> { kind: ty::BoundRegionKind::BrEnv, }; let env_region = ty::Region::new_late_bound(self.tcx, ty::INNERMOST, br); - let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap(); + let env_ty = self.tcx.closure_env_ty(def_id, args, env_region).unwrap(); let sig = sig.skip_binder(); @@ -334,9 +334,9 @@ impl<'tcx> GotocCtx<'tcx> { &self, did: &DefId, ty: Ty<'tcx>, - substs: ty::GenericArgsRef<'tcx>, + args: ty::GenericArgsRef<'tcx>, ) -> ty::PolyFnSig<'tcx> { - let sig = substs.as_generator().poly_sig(); + let sig = args.as_generator().poly_sig(); let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter( sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))), @@ -350,8 +350,8 @@ impl<'tcx> GotocCtx<'tcx> { 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.mk_args(&[env_ty.into()]); - let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_substs); + let pin_args = self.tcx.mk_args(&[env_ty.into()]); + let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args); let sig = sig.skip_binder(); // The `FnSig` and the `ret_ty` here is for a generators main @@ -363,9 +363,9 @@ 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.mk_args(&[sig.return_ty.into()]); + let poll_args = tcx.mk_args(&[sig.return_ty.into()]); // TODO figure out where this one went - let ret_ty = tcx.mk_adt_def(poll_adt_ref, poll_substs); + let ret_ty = Ty::new_adt(tcx, poll_adt_ref, poll_args); // We have to replace the `ResumeTy` that is used for type and borrow checking // with `&mut Context<'_>` which is used in codegen. @@ -385,8 +385,8 @@ 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.mk_args(&[sig.yield_ty.into(), sig.return_ty.into()]); - let ret_ty = Ty::new_adt(tcx, state_adt_ref, state_substs); + let state_args = tcx.mk_args(&[sig.yield_ty.into(), sig.return_ty.into()]); + let ret_ty = Ty::new_adt(tcx, state_adt_ref, state_args); (sig.resume_ty, ret_ty) }; @@ -415,7 +415,7 @@ impl<'tcx> GotocCtx<'tcx> { } sig } - ty::Generator(did, substs, _) => self.generator_sig(did, fntyp, substs), + ty::Generator(did, args, _) => self.generator_sig(did, fntyp, args), _ => unreachable!("Can't get function signature of type: {:?}", fntyp), }) } @@ -661,7 +661,7 @@ impl<'tcx> GotocCtx<'tcx> { // linked C libraries // https://github.com/model-checking/kani/issues/450 match t.kind() { - TyKind::Adt(def, substs) if substs.is_empty() && def.repr().c() => { + TyKind::Adt(def, args) if args.is_empty() && def.repr().c() => { // For non-generic #[repr(C)] types, use the literal path instead of mangling it. self.tcx.def_path_str(def.did()).intern() } @@ -785,9 +785,9 @@ impl<'tcx> GotocCtx<'tcx> { ty::Slice(e) => self.codegen_ty(*e).flexible_array_of(), ty::Str => Type::unsigned_int(8).flexible_array_of(), ty::Ref(_, t, _) | ty::RawPtr(ty::TypeAndMut { ty: t, .. }) => self.codegen_ty_ref(*t), - ty::FnDef(def_id, substs) => { + ty::FnDef(def_id, args) => { let instance = - Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, substs) + Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args) .unwrap() .unwrap(); self.codegen_fndef_type(instance) @@ -983,9 +983,9 @@ impl<'tcx> GotocCtx<'tcx> { /// A closure is a struct of all its environments. That is, a closure is /// just a tuple with a unique type identifier, so that Fn related traits /// can find its impl. - fn codegen_ty_closure(&mut self, t: Ty<'tcx>, substs: ty::GenericArgsRef<'tcx>) -> Type { + fn codegen_ty_closure(&mut self, t: Ty<'tcx>, args: ty::GenericArgsRef<'tcx>) -> Type { self.ensure_struct(self.ty_mangled_name(t), self.ty_pretty_name(t), |ctx, _| { - ctx.codegen_ty_tuple_like(t, substs.as_closure().upvar_tys().collect()) + ctx.codegen_ty_tuple_like(t, args.as_closure().upvar_tys().to_vec()) }) } @@ -1773,7 +1773,7 @@ impl<'tcx> GotocCtx<'tcx> { // Codegen the type replacing the non-zst field. let new_name = self.ty_mangled_name(*curr).to_string() + "::WithDataPtr"; let new_pretty_name = format!("{}::WithDataPtr", self.ty_pretty_name(*curr)); - if let ty::Adt(adt_def, adt_substs) = curr.kind() { + if let ty::Adt(adt_def, adt_args) = curr.kind() { let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields; self.ensure_struct(new_name, new_pretty_name, |ctx, s_name| { let fields_shape = ctx.layout_of(*curr).layout.fields(); @@ -1782,7 +1782,7 @@ impl<'tcx> GotocCtx<'tcx> { .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 field_ty = fields[idx].ty(ctx.tcx, adt_args); let typ = if !ctx.is_zst(field_ty) { last_type.clone() } else { @@ -1813,11 +1813,11 @@ impl<'tcx> GotocCtx<'tcx> { } let mut typ = struct_type; - while let ty::Adt(adt_def, adt_substs) = typ.kind() { + while let ty::Adt(adt_def, adt_args) = 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_index().expect("Trait should be the last element."); - typ = fields[last_field].ty(self.tcx, adt_substs); + typ = fields[last_field].ty(self.tcx, adt_args); } if typ.is_trait() { Some(typ) } else { None } } @@ -1860,7 +1860,7 @@ impl<'tcx> GotocCtx<'tcx> { type Item = (String, Ty<'tcx>); fn next(&mut self) -> Option { - if let ty::Adt(adt_def, adt_substs) = self.curr.kind() { + if let ty::Adt(adt_def, adt_args) = self.curr.kind() { assert_eq!( adt_def.variants().len(), 1, @@ -1871,8 +1871,8 @@ impl<'tcx> GotocCtx<'tcx> { let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields; let mut non_zsts = fields .iter() - .filter(|field| !ctx.is_zst(field.ty(ctx.tcx, adt_substs))) - .map(|non_zst| (non_zst.name.to_string(), non_zst.ty(ctx.tcx, adt_substs))); + .filter(|field| !ctx.is_zst(field.ty(ctx.tcx, adt_args))) + .map(|non_zst| (non_zst.name.to_string(), non_zst.ty(ctx.tcx, adt_args))); let (name, next) = non_zsts.next().expect("Expected one non-zst field."); self.curr = next; assert!(non_zsts.next().is_none(), "Expected only one non-zst field."); diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index bfebc5414386..92c603ffe2f4 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -174,7 +174,7 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> { let src_ty = self.src_ty.take().unwrap(); let dst_ty = self.dst_ty.take().unwrap(); let field = match (&src_ty.kind(), &dst_ty.kind()) { - (&ty::Adt(src_def, src_substs), &ty::Adt(dst_def, dst_substs)) => { + (&ty::Adt(src_def, src_args), &ty::Adt(dst_def, dst_args)) => { // Handle smart pointers by using CustomCoerceUnsized to find the field being // coerced. assert_eq!(src_def, dst_def); @@ -186,8 +186,8 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> { custom_coerce_unsize_info(self.tcx, src_ty, dst_ty); 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)); + self.src_ty = Some(src_fields[coerce_index].ty(self.tcx, src_args)); + self.dst_ty = Some(dst_fields[coerce_index].ty(self.tcx, dst_args)); Some(src_fields[coerce_index].name) } _ => { @@ -213,11 +213,11 @@ fn custom_coerce_unsize_info<'tcx>( ) -> CustomCoerceUnsized { let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None); - let trait_ref = ty::Binder::dummy(TraitRef::new( + let trait_ref = TraitRef::new( tcx, def_id, tcx.mk_args_trait(source_ty, [target_ty.into()]), - )); + ); match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) { Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => { diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 214fa7ac51cb..dc25772ff54b 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -461,7 +461,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { let tcx = self.tcx; match terminator.kind { - TerminatorKind::Call { ref func, ref args, .. } => { + TerminatorKind::Call { ref func, args: ref outer_args, .. } => { let callee_ty = func.ty(self.body, tcx); let fn_ty = self.monomorphize(callee_ty); if let TyKind::FnDef(def_id, substs) = *fn_ty.kind() { @@ -479,7 +479,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { // implement the same traits as those in the // original function/method. A trait mismatch shows // up here, when we try to resolve a trait method - let generic_ty = args[0].ty(self.body, tcx).peel_refs(); + let generic_ty = outer_args[0].ty(self.body, tcx).peel_refs(); let receiver_ty = tcx.subst_and_normalize_erasing_regions( substs, ParamEnv::reveal_all(), From 08e5ebfee1adb6bdac970a122e08cbf1ee88d9d3 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 4 Aug 2023 00:13:16 +0000 Subject: [PATCH 05/13] format --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 12 ++++-------- .../src/codegen_cprover_gotoc/codegen/typ.rs | 13 +++++-------- .../src/codegen_cprover_gotoc/utils/names.rs | 4 +--- kani-compiler/src/kani_middle/coercion.rs | 6 +----- kani-compiler/src/kani_middle/reachability.rs | 18 +++++++++++++++--- kani-driver/src/assess/scan.rs | 12 +++++++++--- 6 files changed, 35 insertions(+), 30 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index da114ad6cd58..f57f42137574 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1018,14 +1018,10 @@ impl<'tcx> GotocCtx<'tcx> { PointerCoercion::UnsafeFnPointer => self.codegen_operand(operand), PointerCoercion::ClosureFnPointer(_) => { if let ty::Closure(def_id, args) = self.operand_ty(operand).kind() { - let instance = Instance::resolve_closure( - self.tcx, - *def_id, - args, - ty::ClosureKind::FnOnce, - ) - .expect("failed to normalize and resolve closure during codegen") - .polymorphize(self.tcx); + let instance = + Instance::resolve_closure(self.tcx, *def_id, args, ty::ClosureKind::FnOnce) + .expect("failed to normalize and resolve closure during codegen") + .polymorphize(self.tcx); self.codegen_func_expr(instance, None).address_of() } else { unreachable!("{:?} cannot be cast to a fn ptr", operand) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 07868ab11609..b1384d68013f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -288,11 +288,7 @@ impl<'tcx> GotocCtx<'tcx> { sig } - fn closure_sig( - &self, - def_id: DefId, - args: ty::GenericArgsRef<'tcx>, - ) -> ty::PolyFnSig<'tcx> { + fn closure_sig(&self, def_id: DefId, args: ty::GenericArgsRef<'tcx>) -> ty::PolyFnSig<'tcx> { let sig = self.monomorphize(args.as_closure().sig()); // In addition to `def_id` and `args`, we need to provide the kind of region `env_region` @@ -1610,9 +1606,10 @@ impl<'tcx> GotocCtx<'tcx> { Primitive::F32 => self.tcx.types.f32, Primitive::F64 => self.tcx.types.f64, - Primitive::Pointer(_) => { - Ty::new_ptr(self.tcx, ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not }) - } + 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/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index c9f93a50cd2f..98f6f533cd12 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -54,9 +54,7 @@ impl<'tcx> GotocCtx<'tcx> { /// A human readable name in Rust for reference, should not be used as a key. pub fn readable_instance_name(&self, instance: Instance<'tcx>) -> String { - with_no_trimmed_paths!( - self.tcx.def_path_str_with_args(instance.def_id(), instance.args) - ) + with_no_trimmed_paths!(self.tcx.def_path_str_with_args(instance.def_id(), instance.args)) } /// The actual function name used in the symbol table diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 92c603ffe2f4..0f4be88bc29e 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -213,11 +213,7 @@ fn custom_coerce_unsize_info<'tcx>( ) -> CustomCoerceUnsized { let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None); - let trait_ref = TraitRef::new( - tcx, - def_id, - tcx.mk_args_trait(source_ty, [target_ty.into()]), - ); + let trait_ref = TraitRef::new(tcx, def_id, tcx.mk_args_trait(source_ty, [target_ty.into()])); match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) { Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => { diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index dc25772ff54b..7f1daf98ecca 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -355,7 +355,11 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { trace!(rvalue=?*rvalue, "visit_rvalue"); match *rvalue { - Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::Unsize), ref operand, target) => { + Rvalue::Cast( + CastKind::PointerCoercion(PointerCoercion::Unsize), + ref operand, + target, + ) => { // Check if the conversion include casting a concrete type to a trait type. // If so, collect items from the impl `Trait for Concrete {}`. let target_ty = self.monomorphize(target); @@ -367,7 +371,11 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { self.collect_vtable_methods(base_coercion.src_ty, base_coercion.dst_ty); } } - Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::ReifyFnPointer), ref operand, _) => { + Rvalue::Cast( + CastKind::PointerCoercion(PointerCoercion::ReifyFnPointer), + ref operand, + _, + ) => { let fn_ty = operand.ty(self.body, self.tcx); let fn_ty = self.monomorphize(fn_ty); if let TyKind::FnDef(def_id, substs) = *fn_ty.kind() { @@ -383,7 +391,11 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { unreachable!("Expected FnDef type, but got: {:?}", fn_ty); } } - Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::ClosureFnPointer(_)), ref operand, _) => { + Rvalue::Cast( + CastKind::PointerCoercion(PointerCoercion::ClosureFnPointer(_)), + ref operand, + _, + ) => { let source_ty = operand.ty(self.body, self.tcx); let source_ty = self.monomorphize(source_ty); match *source_ty.kind() { diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs index 88bd8f643266..17a3a56e2171 100644 --- a/kani-driver/src/assess/scan.rs +++ b/kani-driver/src/assess/scan.rs @@ -201,10 +201,16 @@ fn scan_cargo_projects(path: PathBuf, accumulator: &mut Vec) { return; } // Errors are silently skipped entirely here - let Ok(entries) = std::fs::read_dir(path) else { return; }; + let Ok(entries) = std::fs::read_dir(path) else { + return; + }; for entry in entries { - let Ok(entry) = entry else { continue; }; - let Ok(typ) = entry.file_type() else { continue; }; + let Ok(entry) = entry else { + continue; + }; + let Ok(typ) = entry.file_type() else { + continue; + }; // symlinks are not `is_dir()` if typ.is_dir() { scan_cargo_projects(entry.path(), accumulator) From be87d3ec1dd487583c610e8269a076c2d05f5c03 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 4 Aug 2023 00:13:38 +0000 Subject: [PATCH 06/13] failing test with c_str_literals --- tests/expected/slice_c_str/c_str.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/slice_c_str/c_str.rs b/tests/expected/slice_c_str/c_str.rs index 9fa2feedc6ea..d5328b48e581 100644 --- a/tests/expected/slice_c_str/c_str.rs +++ b/tests/expected/slice_c_str/c_str.rs @@ -1,6 +1,6 @@ #![feature(rustc_private)] #![feature(c_str_literals)] - +// support seems currently disabled CF https://github.com/rust-lang/rust/issues/113333 extern crate libc; use libc::c_char; From 511bd7c5d16b05eef94c779d5dd99c1a22d696c2 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 4 Aug 2023 00:54:25 +0000 Subject: [PATCH 07/13] fix clippy warnings --- .../codegen/foreign_function.rs | 21 +++++++-------- .../compiler_interface.rs | 10 +++---- kani-driver/src/call_cargo.rs | 2 +- src/os_hacks.rs | 3 ++- tools/bookrunner/librustdoc/doctest.rs | 2 +- tools/compiletest/src/json.rs | 27 ++++++++++++------- 6 files changed, 35 insertions(+), 30 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index a102fb5fcd7b..06b259d9086e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -110,18 +110,15 @@ impl<'tcx> GotocCtx<'tcx> { .args .iter() .enumerate() - .filter_map(|(idx, arg)| { - (!arg.is_ignore()).then(|| { - let arg_name = format!("{fn_name}::param_{idx}"); - let base_name = format!("param_{idx}"); - let arg_type = self.codegen_ty(arg.layout.ty); - let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc) - .with_is_parameter(true); - self.symbol_table.insert(sym); - arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into())) - }) - }) - .collect(); + .filter(|&(_, arg)| (!arg.is_ignore())).map(|(idx, arg)| { + let arg_name = format!("{fn_name}::param_{idx}"); + let base_name = format!("param_{idx}"); + let arg_type = self.codegen_ty(arg.layout.ty); + let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc) + .with_is_parameter(true); + self.symbol_table.insert(sym); + arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into())) + }).collect(); let ret_type = self.codegen_ty(fn_abi.ret.layout.ty); if fn_abi.c_variadic { diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index a89e5035f2a2..f30ed663338a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -232,7 +232,7 @@ impl CodegenBackend for GotocCodegenBackend { // Cross-crate collecting of all items that are reachable from the crate harnesses. let harnesses = queries.target_harnesses(); let mut items: HashSet = HashSet::with_capacity(harnesses.len()); - items.extend(harnesses.into_iter()); + items.extend(harnesses); let harnesses = filter_crate_items(tcx, |_, def_id| items.contains(&tcx.def_path_hash(def_id))); for harness in harnesses { @@ -321,7 +321,7 @@ impl CodegenBackend for GotocCodegenBackend { match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() { Ok(val) => Ok(*val), - Err(val) => panic!("unexpected error: {:?}", val.type_id()), + Err(val) => panic!("unexpected error: {:?}", (*val).type_id()), } } @@ -571,9 +571,9 @@ impl<'tcx> GotoCodegenResults<'tcx> { metadata: Option, ) { let mut items = items; - self.harnesses.extend(metadata.into_iter()); - self.concurrent_constructs.extend(gcx.concurrent_constructs.into_iter()); - self.unsupported_constructs.extend(gcx.unsupported_constructs.into_iter()); + self.harnesses.extend(metadata); + self.concurrent_constructs.extend(gcx.concurrent_constructs); + self.unsupported_constructs.extend(gcx.unsupported_constructs); self.items.append(&mut items); } diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 82186e96a44e..54aef6e04c00 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -347,7 +347,7 @@ fn map_kani_artifact(rustc_artifact: cargo_metadata::Artifact) -> Option Result<()> { fn setup_nixos_patchelf(kani_dir: &Path) -> Result<()> { // Encode our assumption that we're working on x86 here, because when we add ARM // support, we need to look for a different path. - assert!(env!("TARGET") == "x86_64-unknown-linux-gnu"); + // TODO clippy detects this as statically true and complains + // assert!(env!("TARGET") == "x86_64-unknown-linux-gnu"); if Path::new("/lib64/ld-linux-x86-64.so.2").exists() { // if the expected path exists, I guess things are fine? return Ok(()); diff --git a/tools/bookrunner/librustdoc/doctest.rs b/tools/bookrunner/librustdoc/doctest.rs index 5d11ea7ec55b..3ec16ce7141c 100644 --- a/tools/bookrunner/librustdoc/doctest.rs +++ b/tools/bookrunner/librustdoc/doctest.rs @@ -110,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::new(emitter)); + let handler = Handler::with_emitter(Box::new(emitter)); let sess = ParseSess::with_span_handler(handler, sm); let mut found_main = false; diff --git a/tools/compiletest/src/json.rs b/tools/compiletest/src/json.rs index 299d81578eb3..d4e6f1a4c873 100644 --- a/tools/compiletest/src/json.rs +++ b/tools/compiletest/src/json.rs @@ -57,21 +57,28 @@ pub fn extract_rendered(output: &str) -> String { if report.future_incompat_report.is_empty() { None } else { + // TODO clippy madness + use std::fmt::Write; Some(format!( "Future incompatibility report: {}", report .future_incompat_report .into_iter() - .map(|item| { - format!( - "Future breakage diagnostic:\n{}", - item.diagnostic - .rendered - .unwrap_or_else(|| "Not rendered".to_string()) - ) - }) - .collect::() - )) + .fold(String::new(), |mut output, item| { + let _ = write!(output, "Future breakage diagnostic:\n"); + let s = item.diagnostic.rendered.unwrap_or_else(|| "Not rendered".to_string()); + let _ = write!(output,"{s}"); + output + }))) + // .map(|item| { + // format!( + // "Future breakage diagnostic:\n{}", + // item.diagnostic + // .rendered + // .unwrap_or_else(|| "Not rendered".to_string()) + // ) + // }) + // .collect::() // TODO use fold ??? } } else if serde_json::from_str::(line).is_ok() { // Ignore the notification. From dd8727e0411e04c5d854b0fbf00800e20bf9af2d Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 4 Aug 2023 01:00:02 +0000 Subject: [PATCH 08/13] format --- .../codegen/foreign_function.rs | 6 ++-- kani-driver/src/call_cargo.rs | 3 +- tools/compiletest/src/json.rs | 36 ++++++++++--------- 3 files changed, 25 insertions(+), 20 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 06b259d9086e..52b6ef0cc821 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -110,7 +110,8 @@ impl<'tcx> GotocCtx<'tcx> { .args .iter() .enumerate() - .filter(|&(_, arg)| (!arg.is_ignore())).map(|(idx, arg)| { + .filter(|&(_, arg)| (!arg.is_ignore())) + .map(|(idx, arg)| { let arg_name = format!("{fn_name}::param_{idx}"); let base_name = format!("param_{idx}"); let arg_type = self.codegen_ty(arg.layout.ty); @@ -118,7 +119,8 @@ impl<'tcx> GotocCtx<'tcx> { .with_is_parameter(true); self.symbol_table.insert(sym); arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into())) - }).collect(); + }) + .collect(); let ret_type = self.codegen_ty(fn_abi.ret.layout.ty); if fn_abi.c_variadic { diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 54aef6e04c00..6bd6a0c35f38 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -346,8 +346,7 @@ fn map_kani_artifact(rustc_artifact: cargo_metadata::Artifact) -> Option String { use std::fmt::Write; Some(format!( "Future incompatibility report: {}", - report - .future_incompat_report - .into_iter() - .fold(String::new(), |mut output, item| { + report.future_incompat_report.into_iter().fold( + String::new(), + |mut output, item| { let _ = write!(output, "Future breakage diagnostic:\n"); - let s = item.diagnostic.rendered.unwrap_or_else(|| "Not rendered".to_string()); - let _ = write!(output,"{s}"); + let s = item + .diagnostic + .rendered + .unwrap_or_else(|| "Not rendered".to_string()); + let _ = write!(output, "{s}"); output - }))) - // .map(|item| { - // format!( - // "Future breakage diagnostic:\n{}", - // item.diagnostic - // .rendered - // .unwrap_or_else(|| "Not rendered".to_string()) - // ) - // }) - // .collect::() // TODO use fold ??? + } + ) + )) + // .map(|item| { + // format!( + // "Future breakage diagnostic:\n{}", + // item.diagnostic + // .rendered + // .unwrap_or_else(|| "Not rendered".to_string()) + // ) + // }) + // .collect::() // TODO use fold ??? } } else if serde_json::from_str::(line).is_ok() { // Ignore the notification. From b8351547755403eb912efd170388e5ffecd29a05 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 4 Aug 2023 16:10:37 +0000 Subject: [PATCH 09/13] fix doc warnings --- cprover_bindings/src/goto_program/expr.rs | 2 +- kani-driver/src/args/mod.rs | 2 +- library/kani_macros/src/lib.rs | 10 ++++++---- src/os_hacks.rs | 5 +++-- .../slice_c_str/{c_str.rs => c_str_fixme.rs} | 2 +- tools/compiletest/src/json.rs | 12 +----------- 6 files changed, 13 insertions(+), 20 deletions(-) rename tests/expected/slice_c_str/{c_str.rs => c_str_fixme.rs} (86%) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 3a6da89239b5..4031d08fa9aa 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -1410,7 +1410,7 @@ impl Expr { ArithmeticOverflowResult { result, overflowed } } - /// Uses CBMC's [binop]-with-overflow operation that performs a single arithmetic + /// Uses CBMC's \[binop\]-with-overflow operation that performs a single arithmetic /// operation /// `struct (T, bool) overflow(binop, self, e)` where `T` is the type of `self` /// Pseudocode: diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 626f2d81be93..6de5be846ed7 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -447,7 +447,7 @@ impl CheckArgs { /// /// We currently define a bunch of cargo specific arguments as part of the overall arguments, /// however, they are invalid in the Kani standalone usage. Explicitly check them for now. -/// TODO: Remove this as part of https://github.com/model-checking/kani/issues/1831 +/// TODO: Remove this as part of fn check_no_cargo_opt(is_set: bool, name: &str) -> Result<(), Error> { if is_set { Err(Error::raw( diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 858efc6388d0..c83cfcb045e0 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -22,11 +22,12 @@ use regular as attr_impl; /// Marks a Kani proof harness /// -/// For async harnesses, this will call [`block_on`] to drive the future to completion (see its documentation for more information). +/// For async harnesses, this will call [`block_on`](/kani/futures/fn.block_on.html) to drive the future to completion (see its documentation for more information). /// /// If you want to spawn tasks in an async harness, you have to pass a schedule to the `#[kani::proof]` attribute, /// e.g. `#[kani::proof(schedule = kani::RoundRobin::default())]`. -/// This will wrap the async function in a call to [`block_on_with_spawn`] (see its documentation for more information). +/// +/// This will wrap the async function in a call to [`block_on_with_spawn`](/kani/futures/fn.block_on_with_spawn.html) (see its documentation for more information). #[proc_macro_error] #[proc_macro_attribute] pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { @@ -51,7 +52,7 @@ pub fn should_panic(attr: TokenStream, item: TokenStream) -> TokenStream { } /// Set Loop unwind limit for proof harnesses -/// The attribute '#[kani::unwind(arg)]' can only be called alongside '#[kani::proof]'. +/// The attribute `#[kani::unwind(arg)]` can only be called alongside `#[kani::proof]`. /// arg - Takes in a integer value (u32) that represents the unwind value for the harness. #[proc_macro_attribute] pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream { @@ -71,7 +72,8 @@ pub fn stub(attr: TokenStream, item: TokenStream) -> TokenStream { } /// Select the SAT solver to use with CBMC for this harness -/// The attribute `#[kani::solver(arg)]` can only be used alongside `#[kani::proof]`` +/// +/// The attribute `#[kani::solver(arg)]` can only be used alongside `#[kani::proof]`. /// /// arg - name of solver, e.g. kissat #[proc_macro_attribute] diff --git a/src/os_hacks.rs b/src/os_hacks.rs index 454170b2a9d8..e4a7fb9a6a4c 100644 --- a/src/os_hacks.rs +++ b/src/os_hacks.rs @@ -106,8 +106,9 @@ pub fn setup_os_hacks(kani_dir: &Path, os: &Info) -> Result<()> { fn setup_nixos_patchelf(kani_dir: &Path) -> Result<()> { // Encode our assumption that we're working on x86 here, because when we add ARM // support, we need to look for a different path. - // TODO clippy detects this as statically true and complains - // assert!(env!("TARGET") == "x86_64-unknown-linux-gnu"); + // Prevents clippy error. + let target = "x86_64-unknown-linux-gnu"; + assert!(env!("TARGET") == target); if Path::new("/lib64/ld-linux-x86-64.so.2").exists() { // if the expected path exists, I guess things are fine? return Ok(()); diff --git a/tests/expected/slice_c_str/c_str.rs b/tests/expected/slice_c_str/c_str_fixme.rs similarity index 86% rename from tests/expected/slice_c_str/c_str.rs rename to tests/expected/slice_c_str/c_str_fixme.rs index d5328b48e581..894746772100 100644 --- a/tests/expected/slice_c_str/c_str.rs +++ b/tests/expected/slice_c_str/c_str_fixme.rs @@ -1,6 +1,6 @@ #![feature(rustc_private)] #![feature(c_str_literals)] -// support seems currently disabled CF https://github.com/rust-lang/rust/issues/113333 +//! FIXME: extern crate libc; use libc::c_char; diff --git a/tools/compiletest/src/json.rs b/tools/compiletest/src/json.rs index 19a413e5024a..ec1de29aa640 100644 --- a/tools/compiletest/src/json.rs +++ b/tools/compiletest/src/json.rs @@ -57,13 +57,12 @@ pub fn extract_rendered(output: &str) -> String { if report.future_incompat_report.is_empty() { None } else { - // TODO clippy madness - use std::fmt::Write; Some(format!( "Future incompatibility report: {}", report.future_incompat_report.into_iter().fold( String::new(), |mut output, item| { + use std::fmt::Write; let _ = write!(output, "Future breakage diagnostic:\n"); let s = item .diagnostic @@ -74,15 +73,6 @@ pub fn extract_rendered(output: &str) -> String { } ) )) - // .map(|item| { - // format!( - // "Future breakage diagnostic:\n{}", - // item.diagnostic - // .rendered - // .unwrap_or_else(|| "Not rendered".to_string()) - // ) - // }) - // .collect::() // TODO use fold ??? } } else if serde_json::from_str::(line).is_ok() { // Ignore the notification. From 6c1e54e9ff0515fcbfccdc9e523afb2593785912 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 4 Aug 2023 17:07:49 +0000 Subject: [PATCH 10/13] fix cargo doc link resolution by using urls --- library/kani_macros/src/lib.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index c83cfcb045e0..509fd78c03ee 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -22,12 +22,12 @@ use regular as attr_impl; /// Marks a Kani proof harness /// -/// For async harnesses, this will call [`block_on`](/kani/futures/fn.block_on.html) to drive the future to completion (see its documentation for more information). +/// For async harnesses, this will call [`block_on`](https://model-checking.github.io/kani/crates/doc/kani/futures/fn.block_on.html) to drive the future to completion (see its documentation for more information). /// /// If you want to spawn tasks in an async harness, you have to pass a schedule to the `#[kani::proof]` attribute, /// e.g. `#[kani::proof(schedule = kani::RoundRobin::default())]`. /// -/// This will wrap the async function in a call to [`block_on_with_spawn`](/kani/futures/fn.block_on_with_spawn.html) (see its documentation for more information). +/// This will wrap the async function in a call to [`block_on_with_spawn`](https://model-checking.github.io/kani/crates/doc/kani/futures/fn.block_on_with_spawn.html) (see its documentation for more information). #[proc_macro_error] #[proc_macro_attribute] pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { From e9038e5d6764a7d0f37206688eb865f89a8d4545 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 4 Aug 2023 17:27:57 +0000 Subject: [PATCH 11/13] fix error message format --- tests/cargo-kani/stubbing-do-not-resolve/harness.expected | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/tests/cargo-kani/stubbing-do-not-resolve/harness.expected b/tests/cargo-kani/stubbing-do-not-resolve/harness.expected index e45663fe2800..f3e82d3620e9 100644 --- a/tests/cargo-kani/stubbing-do-not-resolve/harness.expected +++ b/tests/cargo-kani/stubbing-do-not-resolve/harness.expected @@ -1,4 +1,3 @@ -error: failed to resolve `crate::other_crate2::mock`: unable to find `other_crate2` inside module `stubbing_do_not_resolve` -error: failed to resolve `super::other_crate2::mock`: unable to find `other_crate2` inside module `stubbing_do_not_resolve` -error: failed to resolve `self::other_crate2::mock`: unable to find `other_crate2` inside module `my_mod` -error: failed to resolve `other_crate1::mock`: unable to find `mock` inside module `my_mod::other_crate1` +error[E0463]: can't find crate for `other_crate1` +error[E0463]: can't find crate for `other_crate2` +error: aborting due to 2 previous errors From d4723e2884f080484fbc650e88cc602fe0f2e4a1 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 4 Aug 2023 18:49:43 +0000 Subject: [PATCH 12/13] all tests passing --- rust-toolchain.toml | 2 +- tests/cargo-kani/stubbing-do-not-resolve/harness.expected | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 855a4d3ee2e6..be6cd2da995c 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-08-03" +channel = "nightly-2023-08-04" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/cargo-kani/stubbing-do-not-resolve/harness.expected b/tests/cargo-kani/stubbing-do-not-resolve/harness.expected index f3e82d3620e9..e45663fe2800 100644 --- a/tests/cargo-kani/stubbing-do-not-resolve/harness.expected +++ b/tests/cargo-kani/stubbing-do-not-resolve/harness.expected @@ -1,3 +1,4 @@ -error[E0463]: can't find crate for `other_crate1` -error[E0463]: can't find crate for `other_crate2` -error: aborting due to 2 previous errors +error: failed to resolve `crate::other_crate2::mock`: unable to find `other_crate2` inside module `stubbing_do_not_resolve` +error: failed to resolve `super::other_crate2::mock`: unable to find `other_crate2` inside module `stubbing_do_not_resolve` +error: failed to resolve `self::other_crate2::mock`: unable to find `other_crate2` inside module `my_mod` +error: failed to resolve `other_crate1::mock`: unable to find `mock` inside module `my_mod::other_crate1` From 3fd24f90d81553d402c7d8207fcf8932fad3a1d9 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 4 Aug 2023 20:24:28 +0000 Subject: [PATCH 13/13] restore Cargo.lock --- Cargo.lock | 59 ++++++++++++++++++++++++++---------------------------- 1 file changed, 28 insertions(+), 31 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index ae781d4b0003..c1579b23041d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -162,12 +162,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.0.81" +version = "1.0.79" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6c6b2562119bf28c3439f7f02db99faf0aa1a8cdfe5772a2ee155d32227239f0" -dependencies = [ - "libc", -] +checksum = "50d30906286121d95be3d479533b458f87493b30a4b5f79a607db8f5d11aa91f" [[package]] name = "cfg-if" @@ -208,7 +205,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.28", + "syn 2.0.27", ] [[package]] @@ -368,9 +365,9 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" -version = "0.3.2" +version = "0.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6b30f669a7961ef1631673d2766cc92f52d64f7ef354d4fe0ddfd30ed52f0f4f" +checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a" dependencies = [ "errno-dragonfly", "libc", @@ -556,7 +553,7 @@ dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.28", + "syn 2.0.27", ] [[package]] @@ -593,9 +590,9 @@ dependencies = [ [[package]] name = "linux-raw-sys" -version = "0.4.5" +version = "0.4.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "57bcfdad1b858c2db7c38303a6d2ad4dfaf5eb53dfeb0910128b2c26d6158503" +checksum = "09fc20d2ca12cb9f044c93e3bd6d32d523e6e2ec3db4f7b2939cd99026ecd3f0" [[package]] name = "lock_api" @@ -936,7 +933,7 @@ checksum = "b2eae68fc220f7cf2532e4494aded17545fce192d59cd996e0fe7887f4ceb575" dependencies = [ "aho-corasick", "memchr", - "regex-automata 0.3.4", + "regex-automata 0.3.3", "regex-syntax 0.7.4", ] @@ -951,9 +948,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.3.4" +version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b7b6d6190b7594385f61bd3911cd1be99dfddcfc365a4160cc2ab5bff4aed294" +checksum = "39354c10dd07468c2e73926b23bb9c2caca74c5501e38a35da70406f1d923310" dependencies = [ "aho-corasick", "memchr", @@ -987,9 +984,9 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.6" +version = "0.38.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ee020b1716f0a80e2ace9b03441a749e402e86712f15f16fe8a8f75afac732f" +checksum = "0a962918ea88d644592894bc6dc55acc6c0956488adcebbfb6e273506b7fd6e5" dependencies = [ "bitflags 2.3.3", "errno", @@ -1036,29 +1033,29 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.180" +version = "1.0.175" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0ea67f183f058fe88a4e3ec6e2788e003840893b91bac4559cabedd00863b3ed" +checksum = "5d25439cd7397d044e2748a6fe2432b5e85db703d6d097bd014b3c0ad1ebff0b" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.180" +version = "1.0.175" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "24e744d7782b686ab3b73267ef05697159cc0e5abbed3f47f9933165e5219036" +checksum = "b23f7ade6f110613c0d63858ddb8b94c1041f550eab58a16b371bdf2c9c80ab4" dependencies = [ "proc-macro2", "quote", - "syn 2.0.28", + "syn 2.0.27", ] [[package]] name = "serde_json" -version = "1.0.104" +version = "1.0.103" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "076066c5f1078eac5b722a31827a8832fe108bed65dfa75e233c89f8206e976c" +checksum = "d03b412469450d4404fe8499a268edd7f8b79fecb074b0d812ad64ca21f4031b" dependencies = [ "itoa", "ryu", @@ -1076,9 +1073,9 @@ dependencies = [ [[package]] name = "serde_test" -version = "1.0.176" +version = "1.0.175" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a2f49ace1498612d14f7e0b8245519584db8299541dfe31a06374a828d620ab" +checksum = "29baf0f77ca9ad9c6ed46e1b408b5e0f30b5184bcd66884e7f6d36bd7a65a8a4" dependencies = [ "serde", ] @@ -1203,9 +1200,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.28" +version = "2.0.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "04361975b3f5e348b2189d8dc55bc942f278b2d482a6a0365de5bdd62d351567" +checksum = "b60f673f44a8255b9c8c657daf66a596d435f2da81a555b06dc644d080ba45e0" dependencies = [ "proc-macro2", "quote", @@ -1229,7 +1226,7 @@ checksum = "090198534930841fab3a5d1bb637cde49e339654e606195f8d9c76eeb081dc96" dependencies = [ "proc-macro2", "quote", - "syn 2.0.28", + "syn 2.0.27", ] [[package]] @@ -1296,7 +1293,7 @@ checksum = "5f4f31f56159e98206da9efd823404b79b6ef3143b4a7ab76e67b1751b25a4ab" dependencies = [ "proc-macro2", "quote", - "syn 2.0.28", + "syn 2.0.27", ] [[package]] @@ -1598,9 +1595,9 @@ checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a" [[package]] name = "winnow" -version = "0.5.3" +version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f46aab759304e4d7b2075a9aecba26228bb073ee8c50db796b2c72c676b5d807" +checksum = "25b5872fa2e10bd067ae946f927e726d7d603eaeb6e02fa6a350e0722d2b8c11" dependencies = [ "memchr", ]