Remove unnecessary dependency (rust-lang#2438)

We don't need name demangling since we store the mangled and pretty name of harnesses in the metadata file. I also updated the comment in the `symbol_name` function.

Author: celinval

Cargo.lock

@@ -571,7 +571,6 @@ dependencies = [
  "num",
  "object",
  "regex",
- "rustc-demangle",
  "serde",
  "serde_json",
  "shell-words",

kani-compiler/Cargo.toml

@@ -22,7 +22,6 @@ libc = { version = "0.2", optional = true }
 num = { version = "0.4.0", optional = true }
 object = { version = "0.30.0", default-features = false, features = ["std", "read_core", "write", "archive", "coff", "elf", "macho", "pe"], optional = true }
 regex = "1.7.0"
-rustc-demangle = { version = "0.1.21", optional = true }
 serde = { version = "1", optional = true }
 serde_json = { version = "1", optional = true }
 strum = {version = "0.24.0", optional = true}
@@ -35,7 +34,7 @@ tracing-tree = "0.2.2"
 # Future proofing: enable backend dependencies using feature.
 [features]
 default = ['cprover']
-cprover = ['ar', 'cbmc', 'libc', 'num', 'object', 'rustc-demangle', 'serde',
+cprover = ['ar', 'cbmc', 'libc', 'num', 'object', 'serde',
     'serde_json', "strum", "strum_macros"]
 write_json_symtab = []
 

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

@@ -59,34 +59,18 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn symbol_name(&self, instance: Instance<'tcx>) -> String {
         let llvm_mangled = self.tcx.symbol_name(instance).name.to_string();
         debug!(
-            "finding function name for instance: {}, debug: {:?}, name: {}, symbol: {}, demangle: {}",
+            "finding function name for instance: {}, debug: {:?}, name: {}, symbol: {}",
             instance,
             instance,
             self.readable_instance_name(instance),
             llvm_mangled,
-            rustc_demangle::demangle(&llvm_mangled).to_string()
         );
 
         let pretty = self.readable_instance_name(instance);
 
-        // Make main function a special case for easy CBMC entry
-        // TODO: probably need to edit for https://github.com/model-checking/kani/issues/169
-        if pretty == "main" {
-            "main".to_string()
-        } else {
-            // TODO: llvm mangled string is not very readable. one way to tackle this is to
-            // demangle it. but the demangled string has no generic info.
-            // the best scenario is to use v0 mangler, but this is not default at this moment.
-            // this is the kind of tiny but annoying issue.
-            // c.f. https://github.com/rust-lang/rust/issues/60705
-            //
-            // the following solution won't work pretty:
-            // match self.tcx.sess.opts.debugging_opts.symbol_mangling_version {
-            //     SymbolManglingVersion::Legacy => llvm_mangled,
-            //     SymbolManglingVersion::V0 => rustc_demangle::demangle(llvm_mangled.as_str()).to_string(),
-            // }
-            llvm_mangled
-        }
+        // Make 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 == "main" { pretty } else { llvm_mangled }
     }
 
     /// The name for a tuple field