From 0817efecd1fb038bcb3d134ac6b657e9a6269e57 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 9 Dec 2022 21:28:01 +0000 Subject: [PATCH 1/5] Update Rust toolchain to version `2022-12-04` --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 0fb3d8fbb64a..c2e75d7d6b3c 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2022-11-20" +channel = "nightly-2022-12-04" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From d0c6fff5bdcb5b695ddfe0cf40bff69965c8d195 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 9 Dec 2022 21:30:52 +0000 Subject: [PATCH 2/5] Conform with changes to `GenericArg` --- kani-compiler/src/kani_middle/coercion.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index a92c2f366ae9..799ba3b4766c 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -215,7 +215,7 @@ fn custom_coerce_unsize_info<'tcx>( let trait_ref = ty::Binder::dummy(TraitRef { def_id, - substs: tcx.mk_substs_trait(source_ty, &[target_ty.into()]), + substs: tcx.mk_substs_trait(source_ty, [target_ty.into()]), }); match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) { From b8d808029223c15e47de494c41d1fcffae4ac0c0 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 9 Dec 2022 21:34:07 +0000 Subject: [PATCH 3/5] Conform with changes to `NestedMetaItem` --- kani-compiler/src/kani_middle/attributes.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index b850b590a344..45748b873753 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -33,7 +33,7 @@ pub fn extract_integer_argument(attr: &Attribute) -> Option { let attr_args = attr.meta_item_list()?; // Only extracts one integer value as argument if attr_args.len() == 1 { - let x = attr_args[0].literal()?; + let x = attr_args[0].lit()?; match x.kind { LitKind::Int(y, ..) => Some(y), _ => None, From 341b5bd53395c868329c90d1d41e7a6f9932f45c Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 12 Dec 2022 15:32:49 +0000 Subject: [PATCH 4/5] Make new `ConstKind::Expr` return on reach visitor --- kani-compiler/src/kani_middle/reachability.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 45ecb59c0d0a..6cd9e9c87abb 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -365,7 +365,10 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { ConstKind::Value(v) => self.tcx.valtree_to_const_val((ct.ty(), v)), ConstKind::Unevaluated(_) => unreachable!(), // Nothing to do - ConstKind::Param(..) | ConstKind::Infer(..) | ConstKind::Error(..) => return, + ConstKind::Param(..) + | ConstKind::Infer(..) + | ConstKind::Error(..) + | ConstKind::Expr(..) => return, // Shouldn't happen ConstKind::Placeholder(..) | ConstKind::Bound(..) => { From 3d523aaec1383c4e2b4841fab2f4517cfb4c1ece Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 12 Dec 2022 21:41:37 +0000 Subject: [PATCH 5/5] Conform with changes to `Layout` --- .../src/codegen_cprover_gotoc/codegen/typ.rs | 41 +++++++++---------- 1 file changed, 19 insertions(+), 22 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 50423310cd61..92b30e42c381 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -20,7 +20,7 @@ use rustc_middle::ty::{ use rustc_middle::ty::{List, TypeFoldable}; use rustc_span::def_id::DefId; use rustc_target::abi::{ - Abi::Vector, FieldsShape, Integer, Layout, Primitive, Size, TagEncoding, TyAndLayout, + Abi::Vector, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding, TyAndLayout, VariantIdx, Variants, }; use rustc_target::spec::abi::Abi; @@ -862,10 +862,10 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_alignment_padding( &self, size: Size, - layout: &Layout, + layout: &LayoutS, idx: usize, ) -> Option { - let align = Size::from_bits(layout.align().abi.bits()); + let align = Size::from_bits(layout.align.abi.bits()); let overhang = Size::from_bits(size.bits() % align.bits()); if overhang != Size::ZERO { self.codegen_struct_padding(size, size + align - overhang, idx) @@ -887,16 +887,16 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_struct_fields( &mut self, flds: Vec<(String, Ty<'tcx>)>, - layout: &Layout, + layout: &LayoutS, initial_offset: Size, ) -> Vec { - match &layout.fields() { + match &layout.fields { FieldsShape::Arbitrary { offsets, memory_index } => { assert_eq!(flds.len(), offsets.len()); assert_eq!(offsets.len(), memory_index.len()); let mut final_fields = Vec::with_capacity(flds.len()); let mut offset = initial_offset; - for idx in layout.fields().index_by_increasing_offset() { + for idx in layout.fields.index_by_increasing_offset() { let fld_offset = offsets[idx]; let (fld_name, fld_ty) = &flds[idx]; if let Some(padding) = @@ -919,7 +919,7 @@ impl<'tcx> GotocCtx<'tcx> { } // Primitives, such as NEVER, have no fields FieldsShape::Primitive => vec![], - _ => unreachable!("{}\n{:?}", self.current_fn().readable_name(), layout.fields()), + _ => unreachable!("{}\n{:?}", self.current_fn().readable_name(), layout.fields), } } @@ -928,7 +928,7 @@ impl<'tcx> GotocCtx<'tcx> { let flds: Vec<_> = tys.iter().enumerate().map(|(i, t)| (GotocCtx::tuple_fld_name(i), *t)).collect(); // tuple cannot have other initial offset - self.codegen_struct_fields(flds, &layout.layout, Size::ZERO) + self.codegen_struct_fields(flds, &layout.layout.0, Size::ZERO) } /// A closure in Rust MIR takes two arguments: @@ -1133,7 +1133,7 @@ impl<'tcx> GotocCtx<'tcx> { } fields.extend(ctx.codegen_alignment_padding( offset, - &type_and_layout.layout, + &type_and_layout.layout.0, fields.len(), )); fields @@ -1331,7 +1331,7 @@ impl<'tcx> GotocCtx<'tcx> { self.ensure_struct(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |ctx, _| { let variant = &def.variants().raw[0]; let layout = ctx.layout_of(ty); - ctx.codegen_variant_struct_fields(variant, subst, &layout.layout, Size::ZERO) + ctx.codegen_variant_struct_fields(variant, subst, &layout.layout.0, Size::ZERO) }) } @@ -1340,7 +1340,7 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, variant: &VariantDef, subst: &'tcx InternalSubsts<'tcx>, - layout: &Layout, + layout: &LayoutS, initial_offset: Size, ) -> Vec { let flds: Vec<_> = @@ -1423,7 +1423,7 @@ impl<'tcx> GotocCtx<'tcx> { Some(variant) => { // a single enum is pretty much like a struct let layout = gcx.layout_of(ty).layout; - gcx.codegen_variant_struct_fields(variant, subst, &layout, Size::ZERO) + gcx.codegen_variant_struct_fields(variant, subst, &layout.0, Size::ZERO) } } }) @@ -1509,9 +1509,9 @@ impl<'tcx> GotocCtx<'tcx> { ty: Ty<'tcx>, adtdef: &'tcx AdtDef, subst: &'tcx InternalSubsts<'tcx>, - variants: &IndexVec, + variants: &IndexVec>, ) -> Type { - let non_zst_count = variants.iter().filter(|layout| layout.size().bytes() > 0).count(); + let non_zst_count = variants.iter().filter(|layout| layout.size.bytes() > 0).count(); let mangled_name = self.ty_mangled_name(ty); let pretty_name = self.ty_pretty_name(ty); tracing::trace!(?pretty_name, ?variants, ?subst, ?non_zst_count, "codegen_enum: Niche"); @@ -1528,12 +1528,12 @@ impl<'tcx> GotocCtx<'tcx> { pub(crate) fn variant_min_offset( &self, - variants: &IndexVec, + variants: &IndexVec>, ) -> Option { variants .iter() .filter_map(|lo| { - if lo.fields().count() == 0 { + if lo.fields.count() == 0 { None } else { // get the offset of the leftmost field, which is the one @@ -1541,10 +1541,7 @@ impl<'tcx> GotocCtx<'tcx> { // in the order of increasing offsets. Note that this is not // necessarily the 0th field since the compiler may reorder // fields. - Some( - lo.fields() - .offset(lo.fields().index_by_increasing_offset().next().unwrap()), - ) + Some(lo.fields.offset(lo.fields.index_by_increasing_offset().next().unwrap())) } }) .min() @@ -1615,7 +1612,7 @@ impl<'tcx> GotocCtx<'tcx> { pretty_name: InternedString, def: &'tcx AdtDef, subst: &'tcx InternalSubsts<'tcx>, - layouts: &IndexVec, + layouts: &IndexVec>, initial_offset: Size, ) -> Vec { def.variants() @@ -1647,7 +1644,7 @@ impl<'tcx> GotocCtx<'tcx> { pretty_name: InternedString, case: &VariantDef, subst: &'tcx InternalSubsts<'tcx>, - variant: &Layout, + variant: &LayoutS, initial_offset: Size, ) -> Type { let case_name = format!("{name}::{}", case.name);