Correctly identify extern statics

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -497,18 +497,22 @@ impl<'tcx> GotocCtx<'tcx> {
         let instance = Instance::mono(self.tcx, def_id);
 
         let sym = self.ensure(&self.symbol_name(instance), |ctx, name| {
-            // check if this static is extern
-            let rlinkage = ctx.tcx.codegen_fn_attrs(def_id).linkage;
-
-            // we believe rlinkage being `Some` means the static not extern
-            // based on compiler/rustc_codegen_cranelift/src/linkage.rs#L21
-            // see https://github.com/model-checking/kani/issues/388
-            //
-            // Update: The assertion below may fail in similar environments.
-            // We are disabling it until we find out the root cause, see
-            // https://github.com/model-checking/kani/issues/400
-            //
-            // assert!(rlinkage.is_none());
+            // Rust has a notion of "extern static" variables. These are in an "extern" block,
+            // and so aren't initialized in the current codegen unit. For example (from std):
+            //      extern "C" {
+            //          #[linkage = "extern_weak"]
+            //          static __dso_handle: *mut u8;
+            //          #[linkage = "extern_weak"]
+            //          static __cxa_thread_atexit_impl: *const libc::c_void;
+            //      }
+            // CBMC shares C's notion of "extern" global variables. However, CBMC mostly does
+            // not use this information except when doing C typechecking.
+            // The one exception is handling static variables with no initializer (see
+            // CBMC's `static_lifetime_init`):
+            //   1. If they are `is_extern` they are nondet-initialized.
+            //   2. If they are `!is_extern`, they are zero-initialized.
+            // So we recognize a Rust "extern" declaration and pass that information along.
+            let is_extern = ctx.tcx.is_foreign_item(def_id);
 
             let span = ctx.tcx.def_span(def_id);
             Symbol::static_variable(
@@ -517,7 +521,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 ctx.codegen_ty(instance.ty(ctx.tcx, ty::ParamEnv::reveal_all())),
                 ctx.codegen_span(&span),
             )
-            .with_is_extern(rlinkage.is_none())
+            .with_is_extern(is_extern)
             .with_is_thread_local(is_thread_local)
         });
         sym.clone().to_expr().address_of()

tests/kani/Static/unsafe_extern_static_uninitialized.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-verify-fail
+
+//! This test exercises the `is_extern` property that CBMC makes use of during proof initialization.
+//! CBMC has two behaviors with an *uninitialized* static variable:
+//!   1. If it is declared `extern`, then it is nondet-initialized. (Possible in unsafe Rust)
+//!   2. If it is not `extern`, then it is zero-initialized. (Not possible in Rust)
+//!
+//! Here we test to see that we observe the nondet-initialization.
+//! If this extern static were zero-initialized, the assert below would pass.
+//! Instead, we expect to see failure, because nondet-initialization could be 1.
+
+extern "C" {
+    static an_uninitialized_variable: u32;
+}
+
+#[kani::proof]
+fn check_extern_static_isnt_deterministic() {
+    // If this is zero-initialized, this assertion will pass, but this
+    // test is labeled 'kani-verify-fail', and so the test would fail.
+    assert!(unsafe { an_uninitialized_variable } != 1);
+}