Remove support for the unstable argument --function (rust-lang#3278)

This is a legacy argument that we have very limited support to. We kept
it around for bookrunner tests, which has been removed already.

Resolves rust-lang#2129

Author: celinval

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

@@ -95,7 +95,7 @@ impl<'tcx> GotocCtx<'tcx> {
             vec![]
         });
         self.attach_modifies_contract(instance_of_check, assigns_contract);
-        let wrapper_name = self.symbol_name_stable(instance_of_check);
+        let wrapper_name = instance_of_check.mangled_name();
 
         AssignsContract {
             recursion_tracker: full_recursion_tracker_name,

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

@@ -49,7 +49,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// handled later.
     pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol {
         debug!(?instance, "codegen_foreign_function");
-        let fn_name = self.symbol_name_stable(instance).intern();
+        let fn_name = instance.mangled_name().intern();
         let loc = self.codegen_span_stable(instance.def.span());
         if self.symbol_table.contains(fn_name) {
             // Symbol has been added (either a built-in CBMC function or a Rust allocation function).
@@ -134,7 +134,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Generate type for the given foreign instance.
     fn codegen_ffi_type(&mut self, instance: Instance) -> Type {
-        let fn_name = self.symbol_name_stable(instance);
+        let fn_name = instance.mangled_name();
         let fn_abi = instance.fn_abi().unwrap();
         let loc = self.codegen_span_stable(instance.def.span());
         let params = fn_abi
@@ -166,7 +166,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This will behave like `codegen_unimplemented_stmt` but print a message that includes
     /// the name of the function not supported and the calling convention.
     fn codegen_ffi_unsupported(&mut self, instance: Instance, loc: Location) -> Stmt {
-        let fn_name = &self.symbol_name_stable(instance);
+        let fn_name = &instance.mangled_name();
         debug!(?fn_name, ?loc, "codegen_ffi_unsupported");
 
         // Save this occurrence so we can emit a warning in the compilation report.

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

@@ -52,7 +52,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_function(&mut self, instance: Instance) {
-        let name = self.symbol_name_stable(instance);
+        let name = instance.mangled_name();
         let old_sym = self.symbol_table.lookup(&name).unwrap();
 
         let _trace_span = debug_span!("CodegenFunction", name = instance.name()).entered();
@@ -204,7 +204,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let body = self.transformer.body(self.tcx, instance);
         self.set_current_fn(instance, &body);
         debug!(krate=?instance.def.krate(), is_std=self.current_fn().is_std(), "declare_function");
-        self.ensure(self.symbol_name_stable(instance), |ctx, fname| {
+        self.ensure(instance.mangled_name(), |ctx, fname| {
             Symbol::function(
                 fname,
                 ctx.fn_typ(instance, &body),

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

@@ -628,7 +628,7 @@ impl<'tcx> GotocCtx<'tcx> {
         } else {
             // All non-foreign functions should've been declared beforehand.
             trace!(func=?instance, "codegen_func_symbol");
-            let func = self.symbol_name_stable(instance);
+            let func = instance.mangled_name();
             self.symbol_table
                 .lookup(&func)
                 .unwrap_or_else(|| panic!("Function `{func}` should've been declared before usage"))

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

@@ -1299,7 +1299,7 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!(?vtable_field_name, ?vtable_type, "codegen_vtable_method_field");
 
         // Lookup in the symbol table using the full symbol table name/key
-        let fn_name = self.symbol_name_stable(instance);
+        let fn_name = instance.mangled_name();
 
         if let Some(fn_symbol) = self.symbol_table.lookup(&fn_name) {
             if self.vtable_ctx.emit_vtable_restrictions {

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

@@ -44,7 +44,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_fndef_type_stable(&mut self, instance: Instance) -> Type {
-        let func = self.symbol_name_stable(instance);
+        let func = instance.mangled_name();
         self.ensure_struct(
             format!("{func}::FnDefStruct"),
             format!("{}::FnDefStruct", instance.name()),

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -133,7 +133,7 @@ impl GotocCodegenBackend {
                                 format!(
                                     "codegen_function: {}\n{}",
                                     instance.name(),
-                                    gcx.symbol_name_stable(instance)
+                                    instance.mangled_name()
                                 ),
                                 instance.def,
                             );

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

@@ -39,8 +39,7 @@ impl<'tcx> CurrentFnCtx<'tcx> {
     pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>, body: &Body) -> Self {
         let instance_internal = rustc_internal::internal(gcx.tcx, instance);
         let readable_name = instance.name();
-        let name =
-            if &readable_name == "main" { readable_name.clone() } else { instance.mangled_name() };
+        let name = instance.mangled_name();
         let locals = body.locals().to_vec();
         let local_names = body
             .var_debug_info

kani-compiler/src/codegen_cprover_gotoc/utils/names.rs

@@ -8,7 +8,6 @@ use cbmc::InternedString;
 use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_middle::mir::mono::CodegenUnitNameBuilder;
 use rustc_middle::ty::TyCtxt;
-use stable_mir::mir::mono::Instance;
 use stable_mir::mir::Local;
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -50,15 +49,6 @@ impl<'tcx> GotocCtx<'tcx> {
         format!("{var_name}_init")
     }
 
-    /// Return the mangled name to be used in the symbol table.
-    ///
-    /// We special case main function in order to support `--function main`.
-    // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
-    pub fn symbol_name_stable(&self, instance: Instance) -> String {
-        let pretty = instance.name();
-        if pretty == "main" { pretty } else { instance.mangled_name() }
-    }
-
     /// The name for a tuple field
     pub fn tuple_fld_name(n: usize) -> String {
         format!("{n}")

kani-compiler/src/kani_middle/metadata.rs

@@ -13,19 +13,12 @@ use stable_mir::CrateDef;
 
 use super::{attributes::KaniAttributes, SourceLocation};
 
-pub fn canonical_mangled_name(instance: Instance) -> String {
-    let pretty_name = instance.name();
-    // Main function a special case in order to support `--function main`
-    // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
-    if pretty_name == "main" { pretty_name } else { instance.mangled_name() }
-}
-
 /// Create the harness metadata for a proof harness for a given function.
 pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
     let def = instance.def;
     let kani_attributes = KaniAttributes::for_instance(tcx, instance);
     let pretty_name = instance.name();
-    let mangled_name = canonical_mangled_name(instance);
+    let mangled_name = instance.mangled_name();
 
     // We get the body span to include the entire function definition.
     // This is required for concrete playback to properly position the generated test.