Don't rely on JSON symtabs for --gen-c, --function (rust-lang#2221)

Author: remi-delmas-3000

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -159,6 +159,10 @@ impl CodegenBackend for GotocCodegenBackend {
         // Print compilation report.
         print_report(&gcx, tcx);
 
+        // Map from name to prettyName for all symbols
+        let pretty_name_map: BTreeMap<InternedString, Option<InternedString>> =
+            BTreeMap::from_iter(gcx.symbol_table.iter().map(|(k, s)| (*k, s.pretty_name)));
+
         // Map MIR types to GotoC types
         let type_map: BTreeMap<InternedString, InternedString> =
             BTreeMap::from_iter(gcx.type_map.iter().map(|(k, v)| (*k, v.to_string().into())));
@@ -177,6 +181,7 @@ impl CodegenBackend for GotocCodegenBackend {
             let outputs = tcx.output_filenames(());
             let base_filename = outputs.output_path(OutputType::Object);
             let pretty = self.queries.lock().unwrap().get_output_pretty_json();
+            write_file(&base_filename, ArtifactType::PrettyNameMap, &pretty_name_map, pretty);
             write_file(&base_filename, ArtifactType::SymTab, &gcx.symbol_table, pretty);
             write_file(&base_filename, ArtifactType::TypeMap, &type_map, pretty);
             write_file(&base_filename, ArtifactType::Metadata, &metadata, pretty);

kani-driver/src/call_cargo.rs

@@ -29,8 +29,8 @@ pub struct CargoOutputs {
     /// The directory where compiler outputs should be directed.
     /// Usually 'target/BUILD_TRIPLE/debug/deps/'
     pub outdir: PathBuf,
-    /// The collection of *.symtab.json files written.
-    pub symtabs: Vec<PathBuf>,
+    /// The collection of *.symtab.out goto binary files written.
+    pub symtab_gotos: Vec<PathBuf>,
     /// The location of vtable restrictions files (a directory of *.restrictions.json)
     pub restrictions: Option<PathBuf>,
     /// The kani-metadata.json files written by kani-compiler.
@@ -129,7 +129,7 @@ impl KaniSession {
 
         Ok(CargoOutputs {
             outdir: outdir.clone(),
-            symtabs: glob(&outdir.join("*.symtab.json"))?,
+            symtab_gotos: glob(&outdir.join("*.symtab.out"))?,
             metadata: glob(&outdir.join("*.kani-metadata.json"))?,
             restrictions: self.args.restrict_vtable().then_some(outdir),
             cargo_metadata: metadata,

kani-driver/src/call_goto_instrument.rs

@@ -57,8 +57,9 @@ impl KaniSession {
             }
 
             let c_demangled = alter_extension(output, "demangled.c");
-            let symtab = project.get_harness_artifact(&harness, ArtifactType::SymTab).unwrap();
-            self.demangle_c(symtab, &c_outfile, &c_demangled)?;
+            let prett_name_map =
+                project.get_harness_artifact(&harness, ArtifactType::PrettyNameMap).unwrap();
+            self.demangle_c(prett_name_map, &c_outfile, &c_demangled)?;
             if !self.args.quiet {
                 println!("Demangled GotoC code written to {}", c_demangled.to_string_lossy())
             }
@@ -165,22 +166,21 @@ impl KaniSession {
     /// For local variables, it would be more complicated than a simple search and replace to obtain the demangled name.
     pub fn demangle_c(
         &self,
-        symtab_file: &impl AsRef<Path>,
+        pretty_name_map_file: &impl AsRef<Path>,
         c_file: &Path,
         demangled_file: &Path,
     ) -> Result<()> {
         let mut c_code = std::fs::read_to_string(c_file)?;
-        let reader = BufReader::new(File::open(symtab_file)?);
-        let symtab: serde_json::Value = serde_json::from_reader(reader)?;
-        for (_, symbol) in symtab["symbolTable"].as_object().unwrap() {
-            if let Some(serde_json::Value::String(name)) = symbol.get("name") {
-                if let Some(serde_json::Value::String(pretty)) = symbol.get("prettyName") {
-                    // Struct names start with "tag-", but this prefix is not used in the GotoC files, so we strip it.
-                    // If there is no such prefix, we leave the name unchanged.
-                    let name = name.strip_prefix("tag-").unwrap_or(name);
-                    if !pretty.is_empty() && pretty != name {
-                        c_code = c_code.replace(name, pretty);
-                    }
+        let reader = BufReader::new(File::open(pretty_name_map_file)?);
+        let value: serde_json::Value = serde_json::from_reader(reader)?;
+        let pretty_name_map = value.as_object().unwrap();
+        for (name, pretty_name) in pretty_name_map {
+            if let Some(pretty_name) = pretty_name.as_str() {
+                // Struct names start with "tag-", but this prefix is not used in the GotoC files, so we strip it.
+                // If there is no such prefix, we leave the name unchanged.
+                let name = name.strip_prefix("tag-").unwrap_or(name);
+                if !pretty_name.is_empty() && pretty_name != name {
+                    c_code = c_code.replace(name, pretty_name);
                 }
             }
         }

kani-driver/src/project.rs

@@ -155,10 +155,8 @@ pub fn cargo_project(session: &KaniSession) -> Result<Project> {
         // Merge goto files.
         let joined_name = "cbmc-linked";
         let base_name = outdir.join(joined_name);
-        let symtab_gotos: Vec<_> =
-            outputs.symtabs.iter().map(|p| convert_type(p, SymTab, SymTabGoto)).collect();
         let goto = base_name.with_extension(Goto);
-        session.link_goto_binary(&symtab_gotos, &goto)?;
+        session.link_goto_binary(&outputs.symtab_gotos, &goto)?;
         artifacts.push(Artifact::try_new(&goto, Goto)?);
 
         // Merge metadata files.
@@ -227,8 +225,8 @@ struct StandaloneProjectBuilder<'a> {
 }
 
 /// All the type of artifacts that may be generated as part of the build.
-const BUILD_ARTIFACTS: [ArtifactType; 6] =
-    [Metadata, Goto, SymTab, SymTabGoto, TypeMap, VTableRestriction];
+const BUILD_ARTIFACTS: [ArtifactType; 7] =
+    [Metadata, Goto, SymTab, SymTabGoto, TypeMap, VTableRestriction, PrettyNameMap];
 
 impl<'a> StandaloneProjectBuilder<'a> {
     /// Create a `StandaloneProjectBuilder` from the given input and session.

kani_metadata/src/artifact.rs

@@ -22,6 +22,9 @@ pub enum ArtifactType {
     /// A `json` file that has information about the function pointer restrictions derived from
     /// vtable generation.
     VTableRestriction,
+    /// A `json` file that stores the name to prettyName mapping for symbols
+    /// (used to demangle names from the C dump).
+    PrettyNameMap,
 }
 
 impl ArtifactType {
@@ -33,6 +36,7 @@ impl ArtifactType {
             ArtifactType::SymTabGoto => "symtab.out",
             ArtifactType::TypeMap => "type_map.json",
             ArtifactType::VTableRestriction => "restrictions.json",
+            ArtifactType::PrettyNameMap => "pretty_name_map.json",
         }
     }
 }
@@ -59,7 +63,8 @@ pub fn convert_type(path: &Path, from: ArtifactType, to: ArtifactType) -> PathBu
         | ArtifactType::SymTab
         | ArtifactType::SymTabGoto
         | ArtifactType::TypeMap
-        | ArtifactType::VTableRestriction => {
+        | ArtifactType::VTableRestriction
+        | ArtifactType::PrettyNameMap => {
             result.set_extension("");
             result.set_extension(&to);
         }