Fix contract handling of promoted constants and constant static (#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 #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);
  }
 }