diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 3c67741667c2..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; @@ -372,7 +373,15 @@ 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) => { + 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) + } 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 @@ -490,6 +499,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 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 e8bff532f1e7..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. @@ -219,20 +220,25 @@ 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. + 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 { + 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 +337,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 +526,38 @@ 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))); + if is_anon_static(tcx, def.def_id()) { + 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..915dd967e8ec --- /dev/null +++ b/tests/kani/Static/anon_static.rs @@ -0,0 +1,57 @@ +// 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. + // The MIR is: + // 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. + // 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: 8, align: 8) { + // ╾───────alloc2────────╼ │ ╾──────╼ + // } + + static mut FOO: &mut i32 = &mut 12; + static mut BAR: *mut i32 = unsafe { FOO as *mut _ }; + + #[kani::proof] + fn main() { + unsafe { + // 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 new file mode 100644 index 000000000000..d73a99e00139 --- /dev/null +++ b/tests/kani/Static/pointer_to_const_alloc.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// 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 │ ╾──────╼........ +// } + +// 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()); +}