diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 1097d96ed327c..0ea305ecc763d 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -3,6 +3,8 @@ use anyhow::Result; use std::ffi::OsString; +use std::fs::File; +use std::io::BufReader; use std::path::Path; use std::process::Command; @@ -12,7 +14,13 @@ use crate::util::alter_extension; impl KaniSession { /// Postprocess a goto binary (before cbmc, after linking) in-place by calling goto-instrument - pub fn run_goto_instrument(&self, input: &Path, output: &Path, function: &str) -> Result<()> { + pub fn run_goto_instrument( + &self, + input: &Path, + output: &Path, + symtabs: &[impl AsRef], + function: &str, + ) -> Result<()> { // We actually start by calling goto-cc to start the specialization: self.specialize_to_proof_harness(input, output, function)?; @@ -26,13 +34,20 @@ impl KaniSession { self.rewrite_back_edges(output)?; if self.args.gen_c { + let c_outfile = alter_extension(output, "c"); + // We don't put the C file into temporaries to be deleted. + + self.gen_c(output, &c_outfile)?; + + if !self.args.quiet { + println!("Generated C code written to {}", c_outfile.to_string_lossy()); + } + + let c_demangled = alter_extension(output, "demangled.c"); + self.demangle_c(symtabs, &c_outfile, &c_demangled)?; if !self.args.quiet { - println!( - "Generated C code written to {}", - alter_extension(output, "c").to_string_lossy() - ); + println!("Demangled GotoC code written to {}", c_demangled.to_string_lossy()) } - self.gen_c(output)?; } Ok(()) @@ -116,19 +131,47 @@ impl KaniSession { } /// Generate a .c file from a goto binary (i.e. --gen-c) - pub fn gen_c(&self, file: &Path) -> Result<()> { - let output_filename = alter_extension(file, "c"); - // We don't put the C file into temporaries to be deleted. - + pub fn gen_c(&self, file: &Path, output_file: &Path) -> Result<()> { let args: Vec = vec![ "--dump-c".into(), file.to_owned().into_os_string(), - output_filename.into_os_string(), + output_file.to_owned().into_os_string(), ]; self.call_goto_instrument(args) } + /// Generate a .demangled.c file from the .c file using the `prettyName`s from the symbol tables + /// + /// Currently, only top-level function names and (most) type names are demangled. + /// 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_files: &[impl AsRef], + c_file: &Path, + demangled_file: &Path, + ) -> Result<()> { + let mut c_code = std::fs::read_to_string(c_file)?; + for symtab_file in symtab_files { + let reader = BufReader::new(File::open(symtab_file.as_ref())?); + 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); + } + } + } + } + } + std::fs::write(demangled_file, c_code)?; + Ok(()) + } + /// Non-public helper function to actually do the run of goto-instrument fn call_goto_instrument(&self, args: Vec) -> Result<()> { // TODO get goto-instrument path from self diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 00d5256cf291f..a264d98ca588c 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -63,7 +63,12 @@ fn cargokani_main(input_args: Vec) -> Result<()> { let harness_filename = harness.pretty_name.replace("::", "-"); let report_dir = report_base.join(format!("report-{}", harness_filename)); let specialized_obj = outputs.outdir.join(format!("cbmc-for-{}.out", harness_filename)); - ctx.run_goto_instrument(&linked_obj, &specialized_obj, &harness.mangled_name)?; + ctx.run_goto_instrument( + &linked_obj, + &specialized_obj, + &outputs.symtabs, + &harness.mangled_name, + )?; let result = ctx.check_harness(&specialized_obj, &report_dir, harness)?; if result == VerificationStatus::Failure { @@ -109,7 +114,12 @@ fn standalone_main() -> Result<()> { let mut temps = ctx.temporaries.borrow_mut(); temps.push(specialized_obj.to_owned()); } - ctx.run_goto_instrument(&linked_obj, &specialized_obj, &harness.mangled_name)?; + ctx.run_goto_instrument( + &linked_obj, + &specialized_obj, + &[&outputs.symtab], + &harness.mangled_name, + )?; let result = ctx.check_harness(&specialized_obj, &report_dir, harness)?; if result == VerificationStatus::Failure { diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index b2f8dc24a1cbd..ff1acedb9425c 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -36,6 +36,10 @@ cargo test -p cprover_bindings cargo test -p kani-compiler cargo test -p kani-driver +# Check output files (--gen-c option) +echo "Check GotoC output file generation" +time "$KANI_DIR"/tests/output-files/check-output.sh + # Declare testing suite information (suite and mode) TESTS=( "kani kani" diff --git a/tests/output-files/.gitignore b/tests/output-files/.gitignore new file mode 100644 index 0000000000000..b2ea61f4103f0 --- /dev/null +++ b/tests/output-files/.gitignore @@ -0,0 +1,4 @@ +target/ +Cargo.lock +*.c +build/ diff --git a/tests/output-files/check-output.sh b/tests/output-files/check-output.sh new file mode 100755 index 0000000000000..eb671b1b29b0c --- /dev/null +++ b/tests/output-files/check-output.sh @@ -0,0 +1,81 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -eu + +echo +echo "Starting output file check..." +echo + +# Test for platform +PLATFORM=$(uname -sp) +if [[ $PLATFORM == "Linux x86_64" ]] +then + TARGET="x86_64-unknown-linux-gnu" +elif [[ $PLATFORM == "Darwin i386" ]] +then + TARGET="x86_64-apple-darwin" +elif [[ $PLATFORM == "Darwin arm" ]] +then + TARGET="aarch64-apple-darwin" +else + echo + echo "Test only works on Linux or OSX platforms, skipping..." + echo + exit 0 +fi + +cd $(dirname $0) + +echo "Running single-file check..." +rm -rf *.c +RUST_BACKTRACE=1 kani --gen-c --enable-unstable singlefile.rs --quiet +if ! [ -e singlefile.out.c ] +then + echo "Error: no GotoC file generated. Expected: singlefile.out.c" + exit 1 +fi + +if ! [ -e singlefile.out.demangled.c ] +then + echo "Error: no demangled GotoC file generated. Expected singlefile.out.demangled.c." + exit 1 +fi + +if ! grep -Fq "struct PrettyStruct pretty_function(struct PrettyStruct" singlefile.out.demangled.c; +then + echo "Error: demangled file singlefile.out.demangled.c did not contain expected demangled struct and function name." + exit 1 +fi +echo "Finished single-file check successfully..." +echo + +(cd multifile +echo "Running multi-file check..." +rm -rf build +RUST_BACKTRACE=1 cargo kani --target-dir build --gen-c --enable-unstable --quiet +cd build/${TARGET}/debug/deps/ + +if ! [ -e cbmc-for-main.c ] +then + echo "Error: no GotoC file generated. Expected: build/${TARGET}/debug/deps/cbmc-for-main.c" + exit 1 +fi + +if ! [ -e cbmc-for-main.demangled.c ] +then + echo "Error: no demangled GotoC file generated. Expected build/${TARGET}/debug/deps/cbmc-for-main.demangled.c." + exit 1 +fi + +if ! grep -Fq "struct PrettyStruct pretty_function(struct PrettyStruct" cbmc-for-main.demangled.c; +then + echo "Error: demangled file build/${TARGET}/debug/deps/cbmc-for-main.demangled.c did not contain expected demangled struct and function name." + exit 1 +fi +echo "Finished multi-file check successfully..." +) + +echo "Finished output file check successfully." +echo diff --git a/tests/output-files/multifile/Cargo.toml b/tests/output-files/multifile/Cargo.toml new file mode 100644 index 0000000000000..6d122ab436950 --- /dev/null +++ b/tests/output-files/multifile/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "multifile" +version = "0.1.0" +edition = "2021" + +[workspace] + +[dependencies] diff --git a/tests/output-files/multifile/src/main.rs b/tests/output-files/multifile/src/main.rs new file mode 100644 index 0000000000000..8b4cd8dd03f65 --- /dev/null +++ b/tests/output-files/multifile/src/main.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub struct PrettyStruct; + +#[kani::proof] +fn main() { + pretty_function(PrettyStruct); +} + +pub fn pretty_function(argument: PrettyStruct) -> PrettyStruct { + argument +} diff --git a/tests/output-files/singlefile.rs b/tests/output-files/singlefile.rs new file mode 100644 index 0000000000000..2dc13c48a7ddb --- /dev/null +++ b/tests/output-files/singlefile.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub struct PrettyStruct; + +#[kani::proof] +pub fn main() { + pretty_function(PrettyStruct); +} + +pub fn pretty_function(argument: PrettyStruct) -> PrettyStruct { + argument +}