Fix contract handling of promoted constants and constant static (mode…

…l-checking#3305)

When verifying contracts, CBMC initializes all static variables to
non-deterministic values, except for those with constant types or with
types / values annotated with `ID_C_no_nondet_initialization`.

Kani compiler never set these flags, which caused spurious failures when
verification depended on promoted constants or constant static
variables. This fix changes that.

First, I did a bit of refactoring since we may need to set this `Symbol`
property at a later time for static variables.
I also got rid of the initialization function, since the allocation
initialization can be done directly from an expression.

Then, I added the new property to the `Symbol` type. In CBMC, this is a
property of the type or expression. However, I decided to add it to
`Symbol` to avoid having to add this attribute to all variants of `Type`
and `Expr`.

Resolves model-checking#3228

cprover_bindings/src/goto_program/symbol.rs

@@ -8,6 +8,8 @@ use std::fmt::Display;
 
 /// Based off the CBMC symbol implementation here:
 /// <https://github.com/diffblue/cbmc/blob/develop/src/util/symbol.h>
+///
+/// TODO: We should consider using BitFlags for all the boolean flags.
 #[derive(Clone, Debug)]
 pub struct Symbol {
     /// Unique identifier. Mangled name from compiler `foo12_bar17_x@1`
@@ -46,6 +48,14 @@ pub struct Symbol {
     pub is_thread_local: bool,
     pub is_volatile: bool,
     pub is_weak: bool,
+
+    /// This flag marks a variable as constant (IrepId: `ID_C_constant`).
+    ///
+    /// In CBMC, this is a property of the type or expression. However, we keep it here to avoid
+    /// having to propagate the attribute to all variants of `Type` and `Expr`.
+    ///
+    /// During contract verification, CBMC will not havoc static variables marked as constant.
+    pub is_static_const: bool,
 }
 
 /// The equivalent of a "mathematical function" in CBMC. Semantically this is an
@@ -157,6 +167,7 @@ impl Symbol {
             is_lvalue: false,
             is_parameter: false,
             is_static_lifetime: false,
+            is_static_const: false,
             is_thread_local: false,
             is_volatile: false,
             is_weak: false,
@@ -363,6 +374,11 @@ impl Symbol {
         self
     }
 
+    pub fn set_is_static_const(&mut self, v: bool) -> &mut Symbol {
+        self.is_static_const = v;
+        self
+    }
+
     pub fn with_is_state_var(mut self, v: bool) -> Symbol {
         self.is_state_var = v;
         self
@@ -383,11 +399,21 @@ impl Symbol {
         self
     }
 
+    pub fn set_pretty_name<T: Into<InternedString>>(&mut self, pretty_name: T) -> &mut Symbol {
+        self.pretty_name = Some(pretty_name.into());
+        self
+    }
+
     pub fn with_is_hidden(mut self, hidden: bool) -> Symbol {
         self.is_auxiliary = hidden;
         self
     }
 
+    pub fn set_is_hidden(&mut self, hidden: bool) -> &mut Symbol {
+        self.is_auxiliary = hidden;
+        self
+    }
+
     /// Set `is_property`.
     pub fn with_is_property(mut self, v: bool) -> Self {
         self.is_property = v;

cprover_bindings/src/goto_program/symbol_table.rs

@@ -107,6 +107,11 @@ impl SymbolTable {
         self.symbol_table.get(&name)
     }
 
+    pub fn lookup_mut<T: Into<InternedString>>(&mut self, name: T) -> Option<&mut Symbol> {
+        let name = name.into();
+        self.symbol_table.get_mut(&name)
+    }
+
     pub fn machine_model(&self) -> &MachineModel {
         &self.machine_model
     }

cprover_bindings/src/irep/to_irep.rs

@@ -598,6 +598,10 @@ impl goto_program::Symbol {
                 Irep::just_sub(contract.assigns.iter().map(|req| req.to_irep(mm)).collect()),
             );
         }
+        if self.is_static_const {
+            // Add a `const` to the type.
+            typ = typ.with_named_sub(IrepId::CConstant, Irep::just_id(IrepId::from_int(1)))
+        }
         super::Symbol {
             typ,
             value: match &self.value {

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

@@ -3,13 +3,13 @@
 use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented;
-use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Symbol, Type};
+use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type};
 use rustc_middle::ty::Const as ConstInternal;
 use rustc_smir::rustc_internal;
 use rustc_span::Span as SpanInternal;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, StaticDef};
-use stable_mir::mir::Operand;
+use stable_mir::mir::{Mutability, Operand};
 use stable_mir::ty::{
     Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Ty,
     TyConst, TyConstKind, TyKind, UintTy,
@@ -470,11 +470,17 @@ impl<'tcx> GotocCtx<'tcx> {
         name: Option<String>,
         loc: Location,
     ) -> Expr {
-        debug!(?name, "codegen_const_allocation");
+        debug!(?name, ?alloc, "codegen_const_allocation");
         let alloc_name = match self.alloc_map.get(alloc) {
             None => {
                 let alloc_name = if let Some(name) = name { name } else { self.next_global_name() };
-                self.codegen_alloc_in_memory(alloc.clone(), alloc_name.clone(), loc);
+                let has_interior_mutabity = false; // Constants cannot be mutated.
+                self.codegen_alloc_in_memory(
+                    alloc.clone(),
+                    alloc_name.clone(),
+                    loc,
+                    has_interior_mutabity,
+                );
                 alloc_name
             }
             Some(name) => name.clone(),
@@ -484,13 +490,18 @@ impl<'tcx> GotocCtx<'tcx> {
         mem_place.address_of()
     }
 
-    /// Insert an allocation into the goto symbol table, and generate a goto function that will
-    /// initialize it.
+    /// Insert an allocation into the goto symbol table, and generate an init value.
     ///
-    /// This function is ultimately responsible for creating new statically initialized global variables
-    /// in our goto binaries.
-    pub fn codegen_alloc_in_memory(&mut self, alloc: Allocation, name: String, loc: Location) {
-        debug!(?alloc, ?name, "codegen_alloc_in_memory");
+    /// This function is ultimately responsible for creating new statically initialized global
+    /// variables.
+    pub fn codegen_alloc_in_memory(
+        &mut self,
+        alloc: Allocation,
+        name: String,
+        loc: Location,
+        has_interior_mutabity: bool,
+    ) {
+        debug!(?name, ?alloc, "codegen_alloc_in_memory");
         let struct_name = &format!("{name}::struct");
 
         // The declaration of a static variable may have one type and the constant initializer for
@@ -513,50 +524,40 @@ impl<'tcx> GotocCtx<'tcx> {
                 .collect()
         });
 
+        // Create the allocation from a byte array.
+        let init_fn = |gcx: &mut GotocCtx, var: Symbol| {
+            let val = Expr::struct_expr_from_values(
+                alloc_typ_ref.clone(),
+                alloc_data
+                    .iter()
+                    .map(|d| match d {
+                        AllocData::Bytes(bytes) => Expr::array_expr(
+                            Type::unsigned_int(8).array_of(bytes.len()),
+                            bytes
+                                .iter()
+                                // We should consider adding a poison / undet where we have none
+                                // This mimics the behaviour before StableMIR though.
+                                .map(|b| Expr::int_constant(b.unwrap_or(0), Type::unsigned_int(8)))
+                                .collect(),
+                        ),
+                        AllocData::Expr(e) => e.clone(),
+                    })
+                    .collect(),
+                &gcx.symbol_table,
+            );
+            if val.typ() == &var.typ { val } else { val.transmute_to(var.typ, &gcx.symbol_table) }
+        };
+
         // The global static variable may not be in the symbol table if we are dealing
-        // with a literal that can be statically allocated.
-        // We need to make a constructor whether it was in the table or not, so we can't use the
-        // closure argument to ensure_global_var to do that here.
-        let var = self.ensure_global_var(
+        // with a promoted constant.
+        let _var = self.ensure_global_var_init(
             &name,
             false, //TODO is this correct?
+            alloc.mutability == Mutability::Not && !has_interior_mutabity,
             alloc_typ_ref.clone(),
             loc,
-            |_, _| None,
-        );
-        let var_typ = var.typ().clone();
-
-        // Assign the initial value `val` to `var` via an intermediate `temp_var` to allow for
-        // transmuting the allocation type to the global static variable type.
-        let val = Expr::struct_expr_from_values(
-            alloc_typ_ref.clone(),
-            alloc_data
-                .iter()
-                .map(|d| match d {
-                    AllocData::Bytes(bytes) => Expr::array_expr(
-                        Type::unsigned_int(8).array_of(bytes.len()),
-                        bytes
-                            .iter()
-                            // We should consider adding a poison / undet where we have none
-                            // This mimics the behaviour before StableMIR though.
-                            .map(|b| Expr::int_constant(b.unwrap_or(0), Type::unsigned_int(8)))
-                            .collect(),
-                    ),
-                    AllocData::Expr(e) => e.clone(),
-                })
-                .collect(),
-            &self.symbol_table,
-        );
-        let fn_name = Self::initializer_fn_name(&name);
-        let temp_var = self.gen_function_local_variable(0, &fn_name, alloc_typ_ref, loc).to_expr();
-        let body = Stmt::block(
-            vec![
-                Stmt::decl(temp_var.clone(), Some(val), loc),
-                var.assign(temp_var.transmute_to(var_typ, &self.symbol_table), loc),
-            ],
-            loc,
+            init_fn,
         );
-        self.register_initializer(&name, body);
 
         self.alloc_map.insert(alloc, name);
     }
@@ -663,12 +664,6 @@ impl<'tcx> GotocCtx<'tcx> {
         let fn_item_struct_ty = self.codegen_fndef_type_stable(instance);
         // This zero-sized object that a function name refers to in Rust is globally unique, so we create such a global object.
         let fn_singleton_name = format!("{mangled_name}::FnDefSingleton");
-        self.ensure_global_var(
-            &fn_singleton_name,
-            false,
-            fn_item_struct_ty,
-            loc,
-            |_, _| None, // zero-sized, so no initialization necessary
-        )
+        self.ensure_global_var(&fn_singleton_name, false, fn_item_struct_ty, loc).to_expr()
     }
 }

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

@@ -1444,9 +1444,10 @@ impl<'tcx> GotocCtx<'tcx> {
         let vtable_name = self.vtable_name_stable(trait_type).intern();
         let vtable_impl_name = format!("{vtable_name}_impl_for_{src_name}");
 
-        self.ensure_global_var(
+        self.ensure_global_var_init(
             vtable_impl_name,
             true,
+            true,
             Type::struct_tag(vtable_name),
             loc,
             |ctx, var| {
@@ -1487,11 +1488,10 @@ impl<'tcx> GotocCtx<'tcx> {
                     vtable_fields,
                     &ctx.symbol_table,
                 );
-                let body = var.assign(vtable, loc);
-                let block = Stmt::block(vec![size_assert, body], loc);
-                Some(block)
+                Expr::statement_expression(vec![size_assert, vtable.as_stmt(loc)], var.typ, loc)
             },
         )
+        .to_expr()
     }
 
     /// Cast a pointer to a fat pointer.

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

@@ -317,9 +317,8 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_ret_unit(&mut self, loc: Location) -> Stmt {
         let is_file_local = false;
         let ty = self.codegen_ty_unit();
-        let var =
-            self.ensure_global_var(FN_RETURN_VOID_VAR_NAME, is_file_local, ty, loc, |_, _| None);
-        Stmt::ret(Some(var), loc)
+        let var = self.ensure_global_var(FN_RETURN_VOID_VAR_NAME, is_file_local, ty, loc);
+        Stmt::ret(Some(var.to_expr()), loc)
     }
 
     /// Generates Goto-C for MIR [TerminatorKind::Drop] calls. We only handle code _after_ Rust's "drop elaboration"

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

@@ -4,7 +4,7 @@
 //! This file contains functions related to codegenning MIR static variables into gotoc
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::goto_program::Symbol;
+use crate::kani_middle::is_interior_mut;
 use stable_mir::mir::mono::{Instance, StaticDef};
 use stable_mir::CrateDef;
 use tracing::debug;
@@ -19,7 +19,12 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!("codegen_static");
         let alloc = def.eval_initializer().unwrap();
         let symbol_name = Instance::from(def).mangled_name();
-        self.codegen_alloc_in_memory(alloc, symbol_name, self.codegen_span_stable(def.span()));
+        self.codegen_alloc_in_memory(
+            alloc,
+            symbol_name,
+            self.codegen_span_stable(def.span()),
+            is_interior_mut(self.tcx, def.ty()),
+        );
     }
 
     /// Mutates the Goto-C symbol table to add a forward-declaration of the static variable.
@@ -37,9 +42,8 @@ impl<'tcx> GotocCtx<'tcx> {
         // havoc static variables. Kani uses the location and pretty name to identify
         // the correct variables. If the wrong name is used, CBMC may fail silently.
         // More details at https://github.com/diffblue/cbmc/issues/8225.
-        let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location)
-            .with_is_hidden(false) // Static items are always user defined.
-            .with_pretty_name(pretty_name);
-        self.symbol_table.insert(symbol);
+        self.ensure_global_var(symbol_name, false, typ, location)
+            .set_is_hidden(false) // Static items are always user defined.
+            .set_pretty_name(pretty_name);
     }
 }