Some code cleanup related to BasicBlock labels in the current funct…

…ion context (`CurrentFnCtx`) (rust-lang#769)

- Populate the `BasicBlock` labels for the current function *while* creating the current function context to avoid the need for a follow-up call to set the labels

- Removed the method that returns all the labels from the current function context (`labels`), and replaced calls to it with calls to the `find_label` method

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

@@ -85,14 +85,6 @@ impl<'tcx> GotocCtx<'tcx> {
             assert!(old_sym.is_function());
             let mir = self.current_fn().mir();
             self.print_instance(instance, mir);
-            let labels = self
-                .current_fn()
-                .mir()
-                .basic_blocks()
-                .indices()
-                .map(|bb| format!("{:?}", bb))
-                .collect();
-            self.current_fn_mut().set_labels(labels);
             self.codegen_function_prelude();
             self.codegen_declare_variables();
 

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

@@ -3,7 +3,7 @@
 use super::typ::{is_pointer, pointee_type, TypeExt};
 use crate::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::{GotocCtx, VtableCtx};
-use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
+use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::utils::{aggr_tag, BUG_REPORT_URL};
 use cbmc::MachineModel;
 use cbmc::NO_PRETTY_NAME;

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

@@ -213,14 +213,14 @@ impl<'tcx> GotocCtx<'tcx> {
                     v.eq(Expr::int_constant(first_target.0, self.codegen_ty(switch_ty)))
                         .if_then_else(
                             Stmt::goto(
-                                self.current_fn().labels()[first_target.1.index()].clone(),
+                                self.current_fn().find_label(&first_target.1),
                                 Location::none(),
                             ),
                             None,
                             Location::none(),
                         ),
                     Stmt::goto(
-                        self.current_fn().labels()[targets.otherwise().index()].clone(),
+                        self.current_fn().find_label(&targets.otherwise()),
                         Location::none(),
                     ),
                 ],
@@ -233,15 +233,13 @@ impl<'tcx> GotocCtx<'tcx> {
                 .iter()
                 .map(|(c, bb)| {
                     Expr::int_constant(c, self.codegen_ty(switch_ty)).switch_case(Stmt::goto(
-                        self.current_fn().labels()[bb.index()].clone(),
+                        self.current_fn().find_label(&bb),
                         Location::none(),
                     ))
                 })
                 .collect();
-            let default = Stmt::goto(
-                self.current_fn().labels()[targets.otherwise().index()].clone(),
-                Location::none(),
-            );
+            let default =
+                Stmt::goto(self.current_fn().find_label(&targets.otherwise()), Location::none());
             v.switch(cases, Some(default), Location::none())
         }
     }

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

@@ -33,12 +33,12 @@ pub struct CurrentFnCtx<'tcx> {
 
 /// Constructor
 impl CurrentFnCtx<'tcx> {
-    pub fn new(instance: Instance<'tcx>, gcx: &GotocCtx<'tcx>) -> Self {
+    pub fn new(instance: Instance<'tcx>, gcx: &GotocCtx<'tcx>, labels: Vec<String>) -> Self {
         Self {
             block: vec![],
             current_bb: None,
             instance,
-            labels: vec![],
+            labels,
             mir: gcx.tcx.instance_mir(instance.def),
             name: gcx.symbol_name(instance),
             readable_name: gcx.readable_instance_name(instance),
@@ -72,11 +72,6 @@ impl CurrentFnCtx<'tcx> {
     pub fn set_current_bb(&mut self, bb: BasicBlock) {
         self.current_bb = Some(bb);
     }
-
-    pub fn set_labels(&mut self, labels: Vec<String>) {
-        assert!(self.labels.is_empty());
-        self.labels = labels;
-    }
 }
 
 /// Getters
@@ -91,11 +86,6 @@ impl CurrentFnCtx<'tcx> {
         self.instance
     }
 
-    /// The labels in the function we are currently compiling
-    pub fn labels(&self) -> &Vec<String> {
-        &self.labels
-    }
-
     /// The MIR for the function we are currently compiling
     pub fn mir(&self) -> &'tcx Body<'tcx> {
         self.mir

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

@@ -271,7 +271,16 @@ impl<'tcx> GotocCtx<'tcx> {
 /// Mutators
 impl<'tcx> GotocCtx<'tcx> {
     pub fn set_current_fn(&mut self, instance: Instance<'tcx>) {
-        self.current_fn = Some(CurrentFnCtx::new(instance, self));
+        self.current_fn = Some(CurrentFnCtx::new(
+            instance,
+            self,
+            self.tcx
+                .instance_mir(instance.def)
+                .basic_blocks()
+                .indices()
+                .map(|bb| format!("{:?}", bb))
+                .collect(),
+        ));
     }
 
     pub fn reset_current_fn(&mut self) {