Skip to content

Don't rely on JSON symtabs for --gen-c, --function #2221

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
zhassan-aws merged 2 commits into from
Feb 21, 2023
Merged

Don't rely on JSON symtabs for --gen-c, --function #2221

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c3b7034
Don't rely on JSON symtabs for --gen-c, --function
Feb 20, 2023
307ea01
Merge branch 'main' into dont-rely-on-json-symtab
zhassan-aws Feb 21, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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())));
Expand All @@ -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);
Expand Down
6 changes: 3 additions & 3 deletions kani-driver/src/call_cargo.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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,
Expand Down
28 changes: 14 additions & 14 deletions kani-driver/src/call_goto_instrument.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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())
}
Expand Down Expand Up @@ -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);
}
}
}
Expand Down
8 changes: 3 additions & 5 deletions kani-driver/src/project.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down
7 changes: 6 additions & 1 deletion kani_metadata/src/artifact.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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",
}
}
}
Expand All @@ -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);
}
Expand Down