Ensuring that MIR constants are marked as static consts (#4233)

Currently, we rely on the `mutability` of the `Allocation` when marking
constants. However, my understanding is that for various internal
reasons the compiler may use mutable allocations even for constants.
Instead, we should probably track whether a variable is constant
ourselves.

Resolves #3905
Resolves #4029

Also fixes `tests/expected/function-contract/valid_ptr.expected` (see
comments below).

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Fedor Ryabinin <[email protected]>
Co-authored-by: Michael Tautschnig <[email protected]>

Author: 3 people

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

@@ -131,7 +131,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // First try to generate the constant without allocating memory.
         let expr = self.try_codegen_constant(alloc, ty, loc).unwrap_or_else(|| {
             debug!("codegen_allocation try_fail");
-            let mem_var = self.codegen_const_allocation(alloc, None, loc);
+            let mem_var = self.codegen_const_allocation(alloc, None, loc, true);
             mem_var
                 .cast_to(Type::unsigned_int(8).to_pointer())
                 .cast_to(self.codegen_ty_stable(ty).to_pointer())
@@ -282,7 +282,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     let GlobalAlloc::Memory(data) = GlobalAlloc::from(alloc_id) else {
                         unreachable!()
                     };
-                    let mem_var = self.codegen_const_allocation(&data, None, loc);
+                    let mem_var = self.codegen_const_allocation(&data, None, loc, false);
 
                     // Extract identifier for static variable.
                     // codegen_allocation_auto_imm_name returns the *address* of
@@ -323,7 +323,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     let GlobalAlloc::Memory(data) = GlobalAlloc::from(alloc_id) else {
                         unreachable!()
                     };
-                    let mem_var = self.codegen_const_allocation(&data, None, loc);
+                    let mem_var = self.codegen_const_allocation(&data, None, loc, false);
                     let inner_typ = self.codegen_ty_stable(inner_ty);
                     let len = data.bytes.len() / inner_typ.sizeof(&self.symbol_table) as usize;
                     let data_expr = mem_var.cast_to(inner_typ.to_pointer());
@@ -394,7 +394,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // crates do not conflict. The name alone is insufficient because Rust
                 // allows different versions of the same crate to be used.
                 let name = format!("{}::{alloc_id:?}", self.full_crate_name());
-                self.codegen_const_allocation(&alloc, Some(name), loc)
+                self.codegen_const_allocation(&alloc, Some(name), loc, false)
             }
             alloc @ GlobalAlloc::VTable(..) => {
                 // This is similar to GlobalAlloc::Memory but the type is opaque to rust and it
@@ -404,7 +404,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     unreachable!()
                 };
                 let name = format!("{}::{alloc_id:?}", self.full_crate_name());
-                self.codegen_const_allocation(&alloc, Some(name), loc)
+                self.codegen_const_allocation(&alloc, Some(name), loc, false)
             }
             GlobalAlloc::TypeId { ty: _ } => todo!(),
         };
@@ -486,6 +486,7 @@ impl<'tcx> GotocCtx<'tcx> {
         alloc: &Allocation,
         name: Option<String>,
         loc: Location,
+        is_definitely_const: bool,
     ) -> Expr {
         debug!(?name, ?alloc, "codegen_const_allocation");
         let alloc_name = match self.alloc_map.get(alloc) {
@@ -497,6 +498,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     alloc_name.clone(),
                     loc,
                     has_interior_mutabity,
+                    is_definitely_const,
                 );
                 alloc_name
             }
@@ -517,7 +519,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // 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)
+        self.codegen_const_allocation(alloc, name, loc, false)
     }
 
     /// Insert an allocation into the goto symbol table, and generate an init value.
@@ -530,6 +532,7 @@ impl<'tcx> GotocCtx<'tcx> {
         name: String,
         loc: Location,
         has_interior_mutabity: bool,
+        is_definitely_const: bool,
     ) {
         debug!(?name, ?alloc, "codegen_alloc_in_memory");
         let struct_name = &format!("{name}::struct");
@@ -583,7 +586,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let _var = self.ensure_global_var_init(
             &name,
             false, //TODO is this correct?
-            alloc.mutability == Mutability::Not && !has_interior_mutabity,
+            (is_definitely_const || alloc.mutability == Mutability::Not) && !has_interior_mutabity,
             alloc_typ_ref.clone(),
             loc,
             init_fn,

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

@@ -24,6 +24,7 @@ impl GotocCtx<'_> {
             symbol_name,
             self.codegen_span_stable(def.span()),
             is_interior_mut(self.tcx, def.ty()),
+            false,
         );
     }
 

tests/expected/function-contract/const_block.expected

@@ -0,0 +1,11 @@
+assertion\
+	- Status: SUCCESS\
+	- Description: "|result| *result == Enum::Second"\
+
+assertion\
+	- Status: SUCCESS\
+	- Description: "|result| *result == Enum::First"\
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 5 successfully verified harnesses, 0 failures, 5 total.

tests/expected/function-contract/const_block.rs

@@ -0,0 +1,74 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z function-contracts
+
+//! Checking that constant blocks are correctly verified in contracts.
+//! See https://github.com/model-checking/kani/issues/3905
+
+#![feature(ptr_alignment_type)]
+
+use std::mem;
+use std::ptr::{Alignment, NonNull};
+
+#[derive(PartialEq)]
+enum Enum {
+    First,
+    Second,
+}
+
+#[kani::ensures(|result| *result == Enum::First)]
+const fn first() -> Enum {
+    const { Enum::First }
+}
+
+#[kani::ensures(|result| *result == Enum::Second)]
+const fn second() -> Enum {
+    Enum::Second
+}
+
+#[kani::proof_for_contract(first)]
+pub fn check_first() {
+    let _ = first();
+}
+
+#[kani::proof_for_contract(second)]
+pub fn check_second() {
+    let _ = second();
+}
+
+#[kani::ensures(|result| result.as_usize().is_power_of_two())]
+pub const fn Align_of<T>() -> Alignment {
+    // This can't actually panic since type alignment is always a power of two.
+    const { Alignment::new(mem::align_of::<T>()).unwrap() }
+}
+
+#[kani::ensures(|result| result.as_usize().is_power_of_two())]
+pub const fn Align_of_no_const<T>() -> Alignment {
+    // This can't actually panic since type alignment is always a power of two.
+    Alignment::new(mem::align_of::<T>()).unwrap()
+}
+
+#[kani::proof_for_contract(Align_of)]
+pub fn check_of_i32() {
+    let _ = Align_of::<i32>();
+}
+
+#[kani::proof_for_contract(Align_of_no_const)]
+pub fn check_of_i32_no_const() {
+    let _ = Align_of_no_const::<i32>();
+}
+
+#[kani::requires(true)]
+pub const unsafe fn byte_add_n<T>(s: NonNull<T>, count: usize) -> NonNull<T> {
+    unsafe { NonNull::new_unchecked(s.as_ptr().byte_add(count)) }
+}
+
+#[kani::proof_for_contract(byte_add_n)]
+pub fn non_null_byte_add_dangling_proof() {
+    let ptr = NonNull::<i32>::dangling();
+    assert!(ptr.as_ptr().addr() == 4);
+    assert!(ptr.as_ptr().addr() <= (isize::MAX as usize));
+    unsafe {
+        let _ = byte_add_n(ptr, 0);
+    }
+}

tests/expected/function-contract/valid_ptr.expected

@@ -4,9 +4,7 @@ Failed Checks: |result| kani::mem::can_dereference(result.0)
 VERIFICATION:- FAILED
 
 Checking harness pre_condition::harness_invalid_ptr...
-Failed Checks: assertion failed: unsafe { read_ptr(ptr) } == -20
 Failed Checks: Kani does not support reasoning about pointer to unallocated memory
-Failed Checks: dereference failure: pointer outside object bounds
 VERIFICATION:- FAILED
 
 Checking harness pre_condition::harness_stack_ptr...

tests/kani/FunctionContracts/modify_slice_elem_fixme.rs renamed to tests/kani/FunctionContracts/modify_slice_elem.rs

@@ -4,6 +4,7 @@
 //!
 //! This started failing with the 2025-04-05 toolchain upgrade
 //! Tracking issue: https://github.com/model-checking/kani/issues/4029
+//! Was fixed with https://github.com/model-checking/kani/pull/4233
 //!
 //! Note that this test used to crash while parsing the annotations.
 // kani-flags: -Zfunction-contracts