refactor is_anon_static into function in reachability.rs

Author: carolynzech

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)

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.
@@ -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<MonoItem> {
     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