diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index fbc882befb9f..ca9e3d04959c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/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> = + BTreeMap::from_iter(gcx.symbol_table.iter().map(|(k, s)| (*k, s.pretty_name))); + // Map MIR types to GotoC types let type_map: BTreeMap = 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); diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index a9cdcfbae9e7..1b3b69b93385 100644 --- a/kani-driver/src/call_cargo.rs +++ b/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, + /// The collection of *.symtab.out goto binary files written. + pub symtab_gotos: Vec, /// The location of vtable restrictions files (a directory of *.restrictions.json) pub restrictions: Option, /// 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, diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index f1076ee39ef2..58096f1953e4 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/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, + pretty_name_map_file: &impl AsRef, 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); } } } diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index 25648ae4a460..043ec2994f55 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -155,10 +155,8 @@ pub fn cargo_project(session: &KaniSession) -> Result { // 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. diff --git a/kani_metadata/src/artifact.rs b/kani_metadata/src/artifact.rs index 64e99c09e5b8..55db234e51c3 100644 --- a/kani_metadata/src/artifact.rs +++ b/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); }