From 21e945458bc5840c53c739e83363ab49947deddf Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 21 Mar 2025 16:18:19 -0400 Subject: [PATCH 1/5] codegen support for pointer to anon static --- .../codegen_cprover_gotoc/codegen/operand.rs | 15 +++- kani-compiler/src/kani_middle/reachability.rs | 68 +++++++++++++------ tests/kani/Static/anon_static.rs | 56 +++++++++++++++ 3 files changed, 117 insertions(+), 22 deletions(-) create mode 100644 tests/kani/Static/anon_static.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 3c67741667c2..a47f7cc7e0a4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -372,7 +372,20 @@ impl<'tcx> GotocCtx<'tcx> { // We want to return the function pointer (not to be confused with function item) self.codegen_func_expr(instance, loc).address_of() } - GlobalAlloc::Static(def) => self.codegen_static_pointer(def), + GlobalAlloc::Static(def) => { + let int_def_id = rustc_internal::internal(self.tcx, def.def_id()); + let anonymous = match self.tcx.def_kind(int_def_id) { + rustc_hir::def::DefKind::Static { nested, .. } => nested, + _ => false, + }; + if anonymous { + let alloc = def.eval_initializer().unwrap(); + let name = format!("{}::{alloc_id:?}", self.full_crate_name()); + self.codegen_const_allocation(&alloc, Some(name), loc) + } else { + self.codegen_static_pointer(def) + } + } GlobalAlloc::Memory(alloc) => { // Full (mangled) crate name added so that allocations from different // crates do not conflict. The name alone is insufficient because Rust diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index e8bff532f1e7..b9bb109cd353 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -219,20 +219,30 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> { let _guard = debug_span!("visit_static", ?def).entered(); let mut next_items = vec![]; - // Collect drop function. - let static_ty = def.ty(); - let instance = Instance::resolve_drop_in_place(static_ty); - next_items - .push(CollectedItem { item: instance.into(), reason: CollectionReason::StaticDrop }); + // Collect drop function, unless it's an anonymous static. + let int_def_id = rustc_internal::internal(self.tcx, def.def_id()); + let anonymous = match self.tcx.def_kind(int_def_id) { + rustc_hir::def::DefKind::Static { nested, .. } => nested, + _ => false, + }; + if !anonymous { + let static_ty = def.ty(); + let instance = Instance::resolve_drop_in_place(static_ty); + next_items.push(CollectedItem { + item: instance.into(), + reason: CollectionReason::StaticDrop, + }); - // Collect initialization. - let alloc = def.eval_initializer().unwrap(); - for (_, prov) in alloc.provenance.ptrs { - next_items.extend( - collect_alloc_items(prov.0) - .into_iter() - .map(|item| CollectedItem { item, reason: CollectionReason::Static }), - ); + // Collect initialization. + let alloc = def.eval_initializer().unwrap(); + debug!(?alloc, "visit_static: initializer"); + for (_, prov) in alloc.provenance.ptrs { + next_items.extend( + collect_alloc_items(self.tcx, prov.0) + .into_iter() + .map(|item| CollectedItem { item, reason: CollectionReason::Static }), + ); + } } next_items @@ -331,7 +341,7 @@ impl MonoItemsFnCollector<'_, '_> { debug!(?alloc, "collect_allocation"); for (_, id) in &alloc.provenance.ptrs { self.collected.extend( - collect_alloc_items(id.0) + collect_alloc_items(self.tcx, id.0) .into_iter() .map(|item| CollectedItem { item, reason: CollectionReason::Static }), ) @@ -520,27 +530,43 @@ fn should_codegen_locally(instance: &Instance) -> bool { !instance.is_foreign_item() } -fn collect_alloc_items(alloc_id: AllocId) -> Vec { +fn collect_alloc_items(tcx: TyCtxt, alloc_id: AllocId) -> Vec { trace!(?alloc_id, "collect_alloc_items"); let mut items = vec![]; match GlobalAlloc::from(alloc_id) { GlobalAlloc::Static(def) => { - // This differ from rustc's collector since rustc does not include static from - // upstream crates. - let instance = Instance::try_from(CrateItem::from(def)).unwrap(); - should_codegen_locally(&instance).then(|| items.push(MonoItem::from(def))); + let int_def_id = rustc_internal::internal(tcx, def.def_id()); + let anonymous = match tcx.def_kind(int_def_id) { + rustc_hir::def::DefKind::Static { nested, .. } => nested, + _ => false, + }; + if anonymous { + let alloc = def.eval_initializer().unwrap(); + items.extend( + alloc + .provenance + .ptrs + .iter() + .flat_map(|(_, prov)| collect_alloc_items(tcx, prov.0)), + ); + } else { + // This differ from rustc's collector since rustc does not include static from + // upstream crates. + let instance = Instance::try_from(CrateItem::from(def)).unwrap(); + should_codegen_locally(&instance).then(|| items.push(MonoItem::from(def))); + } } GlobalAlloc::Function(instance) => { should_codegen_locally(&instance).then(|| items.push(MonoItem::from(instance))); } GlobalAlloc::Memory(alloc) => { items.extend( - alloc.provenance.ptrs.iter().flat_map(|(_, prov)| collect_alloc_items(prov.0)), + alloc.provenance.ptrs.iter().flat_map(|(_, prov)| collect_alloc_items(tcx, prov.0)), ); } vtable_alloc @ GlobalAlloc::VTable(..) => { let vtable_id = vtable_alloc.vtable_allocation().unwrap(); - items = collect_alloc_items(vtable_id); + items = collect_alloc_items(tcx, vtable_id); } }; items diff --git a/tests/kani/Static/anon_static.rs b/tests/kani/Static/anon_static.rs new file mode 100644 index 000000000000..83dde569ee16 --- /dev/null +++ b/tests/kani/Static/anon_static.rs @@ -0,0 +1,56 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that Kani can codegen statics that contain pointers to nested statics. +// See https://github.com/model-checking/kani/issues/3904 + +mod example_1 { + // FOO contains a pointer to the anonymous nested static alloc2. + // alloc1 (static: FOO, size: 8, align: 8) { + // ╾───────alloc2────────╼ │ ╾──────╼ + // } + + // alloc2 (static: FOO::{constant#0}, size: 4, align: 4) { + // 2a 00 00 00 │ *... + // } + static mut FOO: &mut u32 = &mut 42; + + #[kani::proof] + fn main() { + unsafe { + *FOO = 43; + } + } +} + +mod example_2 { + // FOO and BAR both point to the anonymous nested static alloc2. + // Test taken from https://github.com/rust-lang/rust/issues/71212#issuecomment-738666248 + // alloc3 (static: BAR, size: 16, align: 8) { + // ╾───────alloc2────────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........ + // } + + // alloc2 (static: FOO::{constant#0}, size: 4, align: 4) { + // 2a 00 00 00 │ *... + // } + + // alloc1 (static: FOO, size: 16, align: 8) { + // ╾───────alloc2────────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........ + // } + pub mod a { + #[no_mangle] + pub static mut FOO: &mut [i32] = &mut [42]; + } + + pub mod b { + #[no_mangle] + pub static mut BAR: &mut [i32] = unsafe { &mut *crate::example_2::a::FOO }; + } + + #[kani::proof] + fn main() { + unsafe { + assert_eq!(a::FOO.as_ptr(), b::BAR.as_ptr()); + } + } +} From d689ea257da7e79b913310dfff87d434466bb142 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 21 Mar 2025 12:57:32 -0400 Subject: [PATCH 2/5] Add test for pointer to constant memory allocation This isn't related to issue 3904. In codegen_alloc_pointer, the GlobalAlloc::from call returns GlobalAlloc::Memory, so we already codegened it as a constant allocation prior to this PR. But I thought it would be good to have a test that exercises this case explicitly, and that demonstrates the difference between this case and the nested statics case, so I added it in this PR. --- tests/kani/Static/pointer_to_const_alloc.rs | 24 +++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/kani/Static/pointer_to_const_alloc.rs diff --git a/tests/kani/Static/pointer_to_const_alloc.rs b/tests/kani/Static/pointer_to_const_alloc.rs new file mode 100644 index 000000000000..242342e7635a --- /dev/null +++ b/tests/kani/Static/pointer_to_const_alloc.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that Kani can codegen statics that contain pointers to constant allocations. +// Test taken from https://github.com/rust-lang/rust/issues/79738#issuecomment-1946578159 + +// alloc4 (static: BAR, size: 16, align: 8) { +// ╾─────alloc3─────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........ +// } + +// alloc3 (size: 4, align: 4) { +// 2a 00 00 00 │ *... +// } + +// alloc1 (static: FOO, size: 16, align: 8) { +// ╾─────alloc3─────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........ +// } +pub static FOO: &[i32] = &[42]; +pub static BAR: &[i32] = &*FOO; + +#[kani::proof] +fn main() { + assert_eq!(FOO.as_ptr(), BAR.as_ptr()); +} From 873a18598f2664c68909b69b91a3bbfb96fbd8ad Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 21 Mar 2025 16:40:41 -0400 Subject: [PATCH 3/5] create wrapper around codegen_const_allocation for clarity --- .../src/codegen_cprover_gotoc/codegen/operand.rs | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index a47f7cc7e0a4..7b7f61548a66 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -381,7 +381,7 @@ impl<'tcx> GotocCtx<'tcx> { if anonymous { let alloc = def.eval_initializer().unwrap(); let name = format!("{}::{alloc_id:?}", self.full_crate_name()); - self.codegen_const_allocation(&alloc, Some(name), loc) + self.codegen_nested_static_allocation(&alloc, Some(name), loc) } else { self.codegen_static_pointer(def) } @@ -503,6 +503,19 @@ impl<'tcx> GotocCtx<'tcx> { mem_place.address_of() } + /// Generate an expression that represents the address of a nested static allocation. + fn codegen_nested_static_allocation( + &mut self, + alloc: &Allocation, + name: Option, + loc: Location, + ) -> Expr { + // The memory behind this allocation isn't constant, but codegen_alloc_in_memory (which codegen_const_allocation calls) + // uses alloc's mutability field to set the const-ness of the allocation in CBMC's symbol table, + // so we can reuse the code and without worrying that the allocation is set as immutable. + self.codegen_const_allocation(alloc, name, loc) + } + /// Insert an allocation into the goto symbol table, and generate an init value. /// /// This function is ultimately responsible for creating new statically initialized global From 6ae6f9de46d9f056da878107fd62519e5fd974be Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 21 Mar 2025 17:59:26 -0400 Subject: [PATCH 4/5] improve test: check that both aliases see mutations --- tests/kani/Static/anon_static.rs | 29 +++++++++++---------- tests/kani/Static/pointer_to_const_alloc.rs | 3 ++- 2 files changed, 17 insertions(+), 15 deletions(-) diff --git a/tests/kani/Static/anon_static.rs b/tests/kani/Static/anon_static.rs index 83dde569ee16..915dd967e8ec 100644 --- a/tests/kani/Static/anon_static.rs +++ b/tests/kani/Static/anon_static.rs @@ -6,6 +6,7 @@ mod example_1 { // FOO contains a pointer to the anonymous nested static alloc2. + // The MIR is: // alloc1 (static: FOO, size: 8, align: 8) { // ╾───────alloc2────────╼ │ ╾──────╼ // } @@ -25,32 +26,32 @@ mod example_1 { mod example_2 { // FOO and BAR both point to the anonymous nested static alloc2. - // Test taken from https://github.com/rust-lang/rust/issues/71212#issuecomment-738666248 - // alloc3 (static: BAR, size: 16, align: 8) { - // ╾───────alloc2────────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........ + // The MIR is: + // alloc3 (static: BAR, size: 8, align: 8) { + // ╾───────alloc2────────╼ │ ╾──────╼ // } // alloc2 (static: FOO::{constant#0}, size: 4, align: 4) { // 2a 00 00 00 │ *... // } - // alloc1 (static: FOO, size: 16, align: 8) { - // ╾───────alloc2────────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........ + // alloc1 (static: FOO, size: 8, align: 8) { + // ╾───────alloc2────────╼ │ ╾──────╼ // } - pub mod a { - #[no_mangle] - pub static mut FOO: &mut [i32] = &mut [42]; - } - pub mod b { - #[no_mangle] - pub static mut BAR: &mut [i32] = unsafe { &mut *crate::example_2::a::FOO }; - } + static mut FOO: &mut i32 = &mut 12; + static mut BAR: *mut i32 = unsafe { FOO as *mut _ }; #[kani::proof] fn main() { unsafe { - assert_eq!(a::FOO.as_ptr(), b::BAR.as_ptr()); + // check that we see the same initial value from all aliases + assert_eq!(*FOO, 12); + assert_eq!(*BAR, 12); + *FOO = 13; + // check that we see the same mutated value from all aliases + assert_eq!(*FOO, 13); + assert_eq!(*BAR, 13); } } } diff --git a/tests/kani/Static/pointer_to_const_alloc.rs b/tests/kani/Static/pointer_to_const_alloc.rs index 242342e7635a..d73a99e00139 100644 --- a/tests/kani/Static/pointer_to_const_alloc.rs +++ b/tests/kani/Static/pointer_to_const_alloc.rs @@ -1,9 +1,10 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Test that Kani can codegen statics that contain pointers to constant allocations. +// Test that Kani can codegen statics that contain pointers to constant (i.e., immutable) allocations. // Test taken from https://github.com/rust-lang/rust/issues/79738#issuecomment-1946578159 +// The MIR is: // alloc4 (static: BAR, size: 16, align: 8) { // ╾─────alloc3─────╼ 01 00 00 00 00 00 00 00 │ ╾──────╼........ // } From 1f0828b0828cfb4ebf75c266b2ae46470bbfa4f8 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 21 Mar 2025 19:14:24 -0400 Subject: [PATCH 5/5] refactor is_anon_static into function in reachability.rs --- .../src/codegen_cprover_gotoc/codegen/operand.rs | 8 ++------ kani-compiler/src/kani_middle/mod.rs | 11 ++++++++++- kani-compiler/src/kani_middle/reachability.rs | 15 +++------------ 3 files changed, 15 insertions(+), 19 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 7b7f61548a66..1a110d8dab24 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::codegen_cprover_gotoc::GotocCtx; use crate::codegen_cprover_gotoc::utils::slice_fat_ptr; +use crate::kani_middle::is_anon_static; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type}; use rustc_middle::ty::Const as ConstInternal; @@ -373,12 +374,7 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_func_expr(instance, loc).address_of() } GlobalAlloc::Static(def) => { - let int_def_id = rustc_internal::internal(self.tcx, def.def_id()); - let anonymous = match self.tcx.def_kind(int_def_id) { - rustc_hir::def::DefKind::Static { nested, .. } => nested, - _ => false, - }; - if anonymous { + if is_anon_static(self.tcx, def.def_id()) { let alloc = def.eval_initializer().unwrap(); let name = format!("{}::{alloc_id:?}", self.full_crate_name()); self.codegen_nested_static_allocation(&alloc, Some(name), loc) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 690ff03058bc..e6839487c046 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -9,10 +9,10 @@ use crate::kani_queries::QueryDb; use rustc_hir::{def::DefKind, def_id::DefId as InternalDefId, def_id::LOCAL_CRATE}; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; -use stable_mir::CrateDef; use stable_mir::mir::mono::MonoItem; use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; use stable_mir::visitor::{Visitable, Visitor as TyVisitor}; +use stable_mir::{CrateDef, DefId}; use std::ops::ControlFlow; use self::attributes::KaniAttributes; @@ -146,6 +146,15 @@ impl SourceLocation { } } +/// Return whether `def_id` refers to a nested static allocation. +pub fn is_anon_static(tcx: TyCtxt, def_id: DefId) -> bool { + let int_def_id = rustc_internal::internal(tcx, def_id); + match tcx.def_kind(int_def_id) { + rustc_hir::def::DefKind::Static { nested, .. } => nested, + _ => false, + } +} + /// Try to convert an internal `DefId` to a `FnDef`. pub fn stable_fn_def(tcx: TyCtxt, def_id: InternalDefId) -> Option { if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index b9bb109cd353..237fbf5f8b41 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -42,6 +42,7 @@ use std::{ use crate::kani_middle::coercion; use crate::kani_middle::coercion::CoercionBase; +use crate::kani_middle::is_anon_static; use crate::kani_middle::transform::BodyTransformation; /// Collect all reachable items starting from the given starting points. @@ -220,12 +221,7 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> { let mut next_items = vec![]; // Collect drop function, unless it's an anonymous static. - let int_def_id = rustc_internal::internal(self.tcx, def.def_id()); - let anonymous = match self.tcx.def_kind(int_def_id) { - rustc_hir::def::DefKind::Static { nested, .. } => nested, - _ => false, - }; - if !anonymous { + if !is_anon_static(self.tcx, def.def_id()) { let static_ty = def.ty(); let instance = Instance::resolve_drop_in_place(static_ty); next_items.push(CollectedItem { @@ -535,12 +531,7 @@ fn collect_alloc_items(tcx: TyCtxt, alloc_id: AllocId) -> Vec { let mut items = vec![]; match GlobalAlloc::from(alloc_id) { GlobalAlloc::Static(def) => { - let int_def_id = rustc_internal::internal(tcx, def.def_id()); - let anonymous = match tcx.def_kind(int_def_id) { - rustc_hir::def::DefKind::Static { nested, .. } => nested, - _ => false, - }; - if anonymous { + if is_anon_static(tcx, def.def_id()) { let alloc = def.eval_initializer().unwrap(); items.extend( alloc