[Boogie Backend] Use the original names of variables when generating …

…Boogie (#2902)

For MIR variables that map to a user variable in the source code, use
their name in the source code in the generated Boogie.

If there are multiple occurrences (due to SSA), append a `_i` to the
variable name, where `i` is 0, 1, ...

This change allows one to refer to the original variable name when
adding contracts (e.g. loop invariants) in the output Boogie.

Example:

For the following Rust program:

```rust
#[kani::proof]
fn main() {
    let mut x = 41;
    let mut y = 43;
    x = 42;
    y = 42;
    kani::assert(x == y, "");
}
```
before this change, the generated Boogie was:
```
// Procedures:
procedure _RNvCsjrUp1z5o1KH_5test64main() 
{
  var _1: int;
  var _2: int;
  var _4: bool;
  var _5: int;
  var _6: int;
  _1 := 41;
  _2 := 43;
  _1 := 42;
  _2 := 42;
  _5 := _1;
  _6 := _2;
  _4 := (_5 == _6);
  assert _4;
  return;
}
```
but with this change, the generated Boogie is:
```
// Procedures:
procedure _RNvCsjrUp1z5o1KH_5test64main() 
{
  var x: int;
  var y: int;
  var _4: bool;
  var _5: int;
  var _6: int;
  x := 41;
  y := 43;
  x := 42;
  y := 42;
  _5 := x;
  _6 := y;
  _4 := (_5 == _6);
  assert _4;
  return;
}
```

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

kani-compiler/src/codegen_boogie/context/boogie_ctx.rs

@@ -5,12 +5,13 @@ use std::io::Write;
 
 use crate::kani_queries::QueryDb;
 use boogie_ast::boogie_program::{BinaryOp, BoogieProgram, Expr, Literal, Procedure, Stmt, Type};
+use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::mir::interpret::Scalar;
 use rustc_middle::mir::traversal::reverse_postorder;
 use rustc_middle::mir::{
     BasicBlock, BasicBlockData, BinOp, Body, Const as mirConst, ConstOperand, ConstValue,
     HasLocalDecls, Local, Operand, Place, Rvalue, Statement, StatementKind, Terminator,
-    TerminatorKind,
+    TerminatorKind, VarDebugInfoContents,
 };
 use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
@@ -19,6 +20,7 @@ use rustc_middle::ty::layout::{
 use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy};
 use rustc_span::Span;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
+use std::collections::hash_map::Entry;
 use tracing::{debug, debug_span, trace};
 
 use super::kani_intrinsic::get_kani_intrinsic;
@@ -74,26 +76,64 @@ impl<'tcx> BoogieCtx<'tcx> {
 
 pub(crate) struct FunctionCtx<'a, 'tcx> {
     bcx: &'a BoogieCtx<'tcx>,
+    instance: Instance<'tcx>,
     mir: &'a Body<'tcx>,
+    /// Maps from local to the name of the corresponding Boogie variable.
+    local_names: FxHashMap<Local, String>,
 }
 
 impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
     pub fn new(bcx: &'a BoogieCtx<'tcx>, instance: Instance<'tcx>) -> FunctionCtx<'a, 'tcx> {
-        Self { bcx, mir: bcx.tcx.instance_mir(instance.def) }
+        // create names for all locals
+        let mut local_names = FxHashMap::default();
+        let mut name_occurrences: FxHashMap<String, usize> = FxHashMap::default();
+        let mir = bcx.tcx.instance_mir(instance.def);
+        let ldecls = mir.local_decls();
+        for local in ldecls.indices() {
+            let debug_info = mir.var_debug_info.iter().find(|info| match info.value {
+                VarDebugInfoContents::Place(p) => p.local == local && p.projection.len() == 0,
+                VarDebugInfoContents::Const(_) => false,
+            });
+            let name = if let Some(debug_info) = debug_info {
+                let base_name = format!("{}", debug_info.name);
+                let entry = name_occurrences.entry(base_name.clone());
+                let name = match entry {
+                    Entry::Occupied(mut o) => {
+                        let occ = o.get_mut();
+                        let index = *occ;
+                        *occ += 1;
+                        format!("{base_name}_{}", index)
+                    }
+                    Entry::Vacant(v) => {
+                        v.insert(1);
+                        base_name
+                    }
+                };
+                name
+            } else {
+                format!("{local:?}")
+            };
+            local_names.insert(local, name);
+        }
+        Self { bcx, instance, mir, local_names }
     }
 
     fn codegen_declare_variables(&self) -> Vec<Stmt> {
         let ldecls = self.mir.local_decls();
         let decls: Vec<Stmt> = ldecls
             .indices()
-            .enumerate()
-            .filter_map(|(_idx, lc)| {
-                let typ = ldecls[lc].ty;
+            .filter_map(|lc| {
+                let typ = self.instance.instantiate_mir_and_normalize_erasing_regions(
+                    self.tcx(),
+                    ty::ParamEnv::reveal_all(),
+                    ty::EarlyBinder::bind(ldecls[lc].ty),
+                );
+                // skip ZSTs
                 if self.layout_of(typ).is_zst() {
                     return None;
                 }
                 debug!(?lc, ?typ, "codegen_declare_variables");
-                let name = format!("{lc:?}");
+                let name = self.local_name(lc).clone();
                 let boogie_type = self.codegen_type(typ);
                 Some(Stmt::Decl { name, typ: boogie_type })
             })
@@ -143,8 +183,9 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
             StatementKind::Assign(box (place, rvalue)) => {
                 debug!(?place, ?rvalue, "codegen_statement");
                 let rv = self.codegen_rvalue(rvalue);
+                let place_name = self.local_name(place.local).clone();
                 // assignment statement
-                let asgn = Stmt::Assignment { target: format!("{:?}", place.local), value: rv.1 };
+                let asgn = Stmt::Assignment { target: place_name, value: rv.1 };
                 // add it to other statements generated while creating the rvalue (if any)
                 add_statement(rv.0, asgn)
             }
@@ -277,7 +318,11 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
 
     fn codegen_local(&self, local: Local) -> Expr {
         // TODO: handle function definitions
-        Expr::Symbol { name: format!("{local:?}") }
+        Expr::Symbol { name: self.local_name(local).clone() }
+    }
+
+    fn local_name(&self, local: Local) -> &String {
+        &self.local_names[&local]
     }
 
     fn codegen_constant(&self, c: &ConstOperand<'tcx>) -> Expr {

tests/expected/boogie/hello/test__RNvCs9oo0zocGbI4_4test19check_boogie_option.symtab.bpl

@@ -0,0 +1,5 @@
+// Procedures:
+procedure _RNvCs9oo0zocGbI4_4test19check_boogie_option() 
+{
+  return;
+}