Remove temporary variables from trace (rust-lang#817)

These changes set all temporary variables as hidden. The cbmc trace will no longer include them.

Author: celinval

src/kani-compiler/cbmc/src/goto_program/symbol.rs

@@ -90,7 +90,7 @@ impl Symbol {
             is_state_var: false,
             is_type: false,
             // ansi-C properties
-            is_auxiliary: false,
+            is_auxiliary: true,
             is_extern: false,
             is_file_local: false,
             is_lvalue: false,
@@ -297,6 +297,11 @@ impl Symbol {
         self.pretty_name = Some(pretty_name.into());
         self
     }
+
+    pub fn with_is_hidden(mut self, hidden: bool) -> Symbol {
+        self.is_auxiliary = hidden;
+        self
+    }
 }
 
 /// Predicates

src/kani-compiler/rustc_codegen_kani/src/codegen/function.rs

@@ -53,7 +53,8 @@ impl<'tcx> GotocCtx<'tcx> {
             let t = self.codegen_ty(t);
             let loc = self.codegen_span(&ldata.source_info.span);
             let sym =
-                Symbol::variable(name, base_name, t, self.codegen_span(&ldata.source_info.span));
+                Symbol::variable(name, base_name, t, self.codegen_span(&ldata.source_info.span))
+                    .with_is_hidden(!ldata.is_user_variable());
             let sym_e = sym.to_expr();
             self.symbol_table.insert(sym);
 
@@ -194,7 +195,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 // This follows the naming convention defined in `typ.rs`.
                 let lc = Local::from_usize(arg_i + starting_idx);
                 let (name, base_name) = self.codegen_spread_arg_name(&lc);
-                let sym = Symbol::variable(name, base_name, self.codegen_ty(arg_t), loc.clone());
+                let sym = Symbol::variable(name, base_name, self.codegen_ty(arg_t), loc.clone())
+                    .with_is_hidden(false);
                 // The spread arguments are additional function paramaters that are patched in
                 // They are to the function signature added in the `fn_typ` function.
                 // But they were never added to the symbol table, which we currently do here.

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

@@ -7,8 +7,12 @@ use crate::GotocCtx;
 use cbmc::goto_program::Symbol;
 use rustc_hir::def_id::DefId;
 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");
@@ -18,12 +22,21 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn declare_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) {
-        debug!("declare_static {:?}", def_id);
+        // Unique mangled monomorphized name.
         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);
+
         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.to_string(), symbol_name, typ, location);
+        let symbol = Symbol::static_variable(symbol_name.to_string(), base_name, typ, location)
+            .with_is_hidden(false) // Static items are always user defined.
+            .with_pretty_name(pretty_name);
         self.symbol_table.insert(symbol);
     }
 }

src/kani-compiler/rustc_codegen_kani/src/context/goto_ctx.rs

@@ -182,8 +182,10 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> Expr {
         let name = name.into();
         if !self.symbol_table.contains(name) {
+            tracing::debug!(?name, "Ensure global variable");
             let sym = Symbol::static_variable(name, name, t.clone(), loc)
-                .with_is_file_local(is_file_local);
+                .with_is_file_local(is_file_local)
+                .with_is_hidden(false);
             let var = sym.to_expr();
             self.symbol_table.insert(sym);
             if let Some(body) = init_fn(self, var) {

tests/kani/Static/method_static_var.rs

@@ -0,0 +1,23 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks static variables declared inside methods are still unique.
+
+// There should be no name collision.
+static counter: i8 = 0;
+
+fn new_id() -> i8 {
+    static mut counter: i8 = 0;
+    unsafe {
+        counter += 1;
+        counter
+    }
+}
+
+fn main() {
+    let id_1 = new_id();
+    let id_2 = new_id();
+    assert!(id_1 == 1);
+    assert!(id_2 == 2);
+    assert!(counter == 0);
+}