Add support for anonymous nested statics

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_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 +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<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/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<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)));
+            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

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

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