From e37a168b7a10ef1e1819a9a9f447b2c1e1ccb9c4 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 8 Dec 2023 16:17:31 +0000 Subject: [PATCH 1/5] Get `alloc_id` from provenance --- kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index d297d9d90a52..59a18348d582 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -421,7 +421,8 @@ impl<'tcx> GotocCtx<'tcx> { } (Scalar::Ptr(ptr, _size), _) => { let res_t = self.codegen_ty(ty); - let (alloc_id, offset) = ptr.into_parts(); + let (prov, offset) = ptr.into_parts(); + let alloc_id = prov.alloc_id(); self.codegen_alloc_pointer(res_t, alloc_id, offset, span) } _ => unimplemented!(), @@ -646,7 +647,8 @@ impl<'tcx> GotocCtx<'tcx> { Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes()); let mut next_offset = Size::ZERO; - for &(offset, alloc_id) in alloc.provenance().ptrs().iter() { + for &(offset, prov) in alloc.provenance().ptrs().iter() { + let alloc_id = prov.alloc_id(); if offset > next_offset { let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( next_offset.bytes_usize()..offset.bytes_usize(), From 21d2623c31b9e674ad29a6f3110bec75b4dd965b Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 8 Dec 2023 16:20:10 +0000 Subject: [PATCH 2/5] Update toolchain to `nightly-2023-12-08` --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 2bdb5cdf793a..6c7de32c5e63 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-12-07" +channel = "nightly-2023-12-08" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 09b29828f7a371de0e94eb10507943712f7afec9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 8 Dec 2023 16:20:49 +0000 Subject: [PATCH 3/5] Use `GenSig` instead of `PolyGenSig` --- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index aec9d8143818..ec5756c4d09b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -332,11 +332,11 @@ impl<'tcx> GotocCtx<'tcx> { ty: Ty<'tcx>, args: ty::GenericArgsRef<'tcx>, ) -> ty::PolyFnSig<'tcx> { - let sig = args.as_coroutine().poly_sig(); + let sig = args.as_coroutine().sig(); - let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter( - sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))), - ); + let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(iter::once( + ty::BoundVariableKind::Region(ty::BrEnv), + )); let br = ty::BoundRegion { var: ty::BoundVar::from_usize(bound_vars.len() - 1), kind: ty::BoundRegionKind::BrEnv, @@ -349,7 +349,6 @@ impl<'tcx> GotocCtx<'tcx> { 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 coroutines main // `coroutine::resume(...) -> CoroutineState` function in case we // have an ordinary coroutine, or the `Future::poll(...) -> Poll` From 5415041c651d0d140323380b1d20a68e90615b80 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 8 Dec 2023 18:18:22 +0000 Subject: [PATCH 4/5] Remove workaround in `reachable_items` --- kani-compiler/src/kani_middle/reachability.rs | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index a8e7d9fe3f83..bab77c5b4347 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -153,11 +153,7 @@ impl<'tcx> MonoItemsCollector<'tcx> { /// instruction looking for the items that should be included in the compilation. fn reachable_items(&mut self) { while let Some(to_visit) = self.queue.pop() { - // TODO: This should only check is_foreign_item() or even `has_body()`. - // We need https://github.com/rust-lang/rust/pull/118681 to land first. - if !self.collected.contains(&to_visit) - && !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id()) - { + if !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id()) { self.collected.insert(to_visit.clone()); let next_items = match &to_visit { MonoItem::Fn(instance) => self.visit_fn(*instance), From 29ac9629a3f10db5521223bfc7cd3047cc402826 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 8 Dec 2023 10:48:48 -0800 Subject: [PATCH 5/5] Update kani-compiler/src/kani_middle/reachability.rs --- kani-compiler/src/kani_middle/reachability.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index bab77c5b4347..216feb66fb87 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -153,7 +153,7 @@ impl<'tcx> MonoItemsCollector<'tcx> { /// instruction looking for the items that should be included in the compilation. fn reachable_items(&mut self) { while let Some(to_visit) = self.queue.pop() { - if !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id()) { + if !self.collected.contains(&to_visit) { self.collected.insert(to_visit.clone()); let next_items = match &to_visit { MonoItem::Fn(instance) => self.visit_fn(*instance),