Add support for anonymous nested statics

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<String>,
+        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

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<FnDef> {
     if let TyKind::RigidTy(RigidTy::FnDef(def, _)) =

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<MonoItem> {
+fn collect_alloc_items(tcx: TyCtxt, alloc_id: AllocId) -> Vec<MonoItem> {
     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

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);
+        }
+    }
+}

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<imm>─────╼ 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<imm>─────╼ 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());
+}