Fix static variable malformed symbol (rust-lang#1380)

A symbol's `base_name` has to be a suffix of its `name` otherwise it is
considered a malformed symbol. For static variables, Kani was using the
`pretty_name` to generate the `base_name` which was generating invalid
iRep as a result. This was caught while trying to run symtab2gb after
the std compilation.

Fixes rust-lang#1361

Author: celinval

cprover_bindings/src/goto_program/symbol.rs

@@ -71,6 +71,13 @@ impl Symbol {
         let name = name.into();
         let base_name = base_name.intern();
         let pretty_name = pretty_name.intern();
+        // See https://github.com/model-checking/kani/issues/1361#issuecomment-1181499683
+        assert!(
+            name.to_string().ends_with(&base_name.map_or(String::new(), |s| s.to_string())),
+            "Symbol's base_name must be the suffix of its name.\nName: {:?}\nBase name: {:?}",
+            name,
+            base_name
+        );
         Symbol {
             name,
             location,

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

@@ -10,9 +10,6 @@ use rustc_middle::mir::mono::MonoItem;
 use rustc_middle::ty::{subst::InternalSubsts, Instance};
 use tracing::debug;
 
-/// Separator used to generate function static variable names (<function_name>::<variable_name>).
-const SEPARATOR: &str = "::";
-
 impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) {
         debug!("codegen_static");
@@ -26,15 +23,12 @@ impl<'tcx> GotocCtx<'tcx> {
         let symbol_name = item.symbol_name(self.tcx).to_string();
         // Pretty name which may include function name.
         let pretty_name = Instance::new(def_id, InternalSubsts::empty()).to_string();
-        // Name of the variable in the local context.
-        let base_name =
-            pretty_name.rsplit_once(SEPARATOR).map(|names| names.1).unwrap_or(pretty_name.as_str());
-        debug!(?symbol_name, ?pretty_name, ?base_name, "declare_static {}", item);
+        debug!(?symbol_name, ?pretty_name, "declare_static {}", item);
 
         let typ = self.codegen_ty(self.tcx.type_of(def_id));
         let span = self.tcx.def_span(def_id);
         let location = self.codegen_span(&span);
-        let symbol = Symbol::static_variable(symbol_name, base_name, typ, location)
+        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);

scripts/std-lib-regression.sh

@@ -61,6 +61,7 @@ kani = {path=\"${KANI_DIR}/library/kani\"}
 cp ${KANI_DIR}/rust-toolchain.toml .
 
 echo "Starting cargo build with Kani"
+export RUST_BACKTRACE=1
 export RUSTC_LOG=error
 export KANIFLAGS="--goto-c --ignore-global-asm"
 export RUSTFLAGS="--kani-flags"