From c6754a1c970a809f200dcda4c65dbb7c0b9fb804 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 24 May 2023 17:48:23 -0700 Subject: [PATCH] Avoid an unnecssary suffix to the goto filename --- kani-driver/src/harness_runner.rs | 19 ++++------------ kani-driver/src/util.rs | 22 ------------------- tests/kani/LongNames/test.rs | 17 ++++++++++++++ .../check-output/check-output.sh | 20 ++++++++--------- 4 files changed, 31 insertions(+), 47 deletions(-) create mode 100644 tests/kani/LongNames/test.rs diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index e0da3c9a73c5..d2885c69429a 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -11,7 +11,7 @@ use crate::args::OutputFormat; use crate::call_cbmc::{VerificationResult, VerificationStatus}; use crate::project::Project; use crate::session::KaniSession; -use crate::util::{error, specialized_harness_name, warning}; +use crate::util::{error, warning}; /// A HarnessRunner is responsible for checking all proof harnesses. The data in this structure represents /// "background information" that the controlling driver (e.g. cargo-kani or kani) computed. @@ -56,24 +56,13 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> { let report_dir = self.project.outdir.join(format!("report-{harness_filename}")); let goto_file = self.project.get_harness_artifact(&harness, ArtifactType::Goto).unwrap(); - let specialized_obj = specialized_harness_name(goto_file, &harness_filename); - self.sess.record_temporary_file(&specialized_obj); - self.sess.instrument_model( - goto_file, - &specialized_obj, - &self.project, - &harness, - )?; + self.sess.instrument_model(goto_file, goto_file, &self.project, &harness)?; if self.sess.args.synthesize_loop_contracts { - self.sess.synthesize_loop_contracts( - &specialized_obj, - &specialized_obj, - &harness, - )?; + self.sess.synthesize_loop_contracts(goto_file, &goto_file, &harness)?; } - let result = self.sess.check_harness(&specialized_obj, &report_dir, harness)?; + let result = self.sess.check_harness(goto_file, &report_dir, harness)?; Ok(HarnessResult { harness, result }) }) .collect::>>() diff --git a/kani-driver/src/util.rs b/kani-driver/src/util.rs index 66fc39e59841..a9800785f869 100644 --- a/kani-driver/src/util.rs +++ b/kani-driver/src/util.rs @@ -157,11 +157,6 @@ pub fn render_command(cmd: &Command) -> OsString { str } -/// Generate the filename for a specialized harness from the base linked object -pub fn specialized_harness_name(linked_obj: &Path, harness_filename: &str) -> PathBuf { - alter_extension(linked_obj, &format!("for-{harness_filename}.out")) -} - /// Print a warning message. This will add a "warning:" tag before the message and style accordingly. pub fn warning(msg: &str) { let warning = console::style("warning:").bold().yellow(); @@ -229,21 +224,4 @@ mod tests { c1.env("PARAM", "VALUE"); assert_eq!(render_command(&c1), OsString::from("PARAM=\"VALUE\" a b \"/c d/\"")); } - - #[test] - fn check_specialized_harness_name() { - // It's important that the filenames produced end in `.out` as we produce - // `--gen-c` filenames with `alter_extension` and we previously had a bug where - // `for-harness` was the "extension" being removed, and all filenames collided. - - // cargo kani typically produced a file name like this - let h1 = PathBuf::from("./cbmc-linked.out"); - assert_eq!(specialized_harness_name(&h1, "main"), Path::new("./cbmc-linked.for-main.out")); - assert_eq!(specialized_harness_name(&h1, "hs_n"), Path::new("./cbmc-linked.for-hs_n.out")); - - // kani typically produces a file name like this - let h2 = PathBuf::from("./rs-file.out"); - assert_eq!(specialized_harness_name(&h2, "main"), Path::new("./rs-file.for-main.out")); - assert_eq!(specialized_harness_name(&h2, "hs_n"), Path::new("./rs-file.for-hs_n.out")); - } } diff --git a/tests/kani/LongNames/test.rs b/tests/kani/LongNames/test.rs new file mode 100644 index 000000000000..91888c0277bb --- /dev/null +++ b/tests/kani/LongNames/test.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks that Kani handles harnesses with long name, e.g. due to +//! nested modules +//! The test is from https://github.com/model-checking/kani/issues/2468 + +mod a_really_long_module_name { + mod yet_another_really_long_module_name { + mod one_more_really_long_module_name { + #[kani::proof] + fn a_really_long_harness_name() { + assert_eq!(1, 1); + } + } + } +} diff --git a/tests/script-based-pre/check-output/check-output.sh b/tests/script-based-pre/check-output/check-output.sh index 45cb3b166669..8e872079003a 100755 --- a/tests/script-based-pre/check-output/check-output.sh +++ b/tests/script-based-pre/check-output/check-output.sh @@ -34,15 +34,15 @@ rm -rf *.c kani --gen-c --enable-unstable singlefile.rs >& kani.log || \ { ret=$?; echo "== Failed to run Kani"; cat kani.log; rm kani.log; exit 1; } rm -f kani.log -if ! [ -e singlefile_main.for-main.c ] +if ! [ -e singlefile_main.c ] then - echo "Error: no GotoC file generated. Expected: singlefile_main.for-main.c" + echo "Error: no GotoC file generated. Expected: singlefile_main.c" exit 1 fi -if ! [ -e singlefile_main.for-main.demangled.c ] +if ! [ -e singlefile_main.demangled.c ] then - echo "Error: no demangled GotoC file generated. Expected singlefile_main.for-main.demangled.c." + echo "Error: no demangled GotoC file generated. Expected singlefile_main.demangled.c." exit 1 fi @@ -57,9 +57,9 @@ declare -a PATTERNS=( ) for val in "${PATTERNS[@]}"; do - if ! grep -Fq "$val" singlefile_main.for-main.demangled.c; + if ! grep -Fq "$val" singlefile_main.demangled.c; then - echo "Error: demangled file singlefile_main.for-main.demangled.c did not contain expected pattern '$val'." + echo "Error: demangled file singlefile_main.demangled.c did not contain expected pattern '$val'." exit 1 fi done @@ -75,17 +75,17 @@ cargo kani --target-dir build --gen-c --enable-unstable >& kani.log || \ rm -f kani.log cd build/kani/${TARGET}/debug/deps/ -mangled=$(ls multifile*.for-main.c) +mangled=$(ls multifile*_main.c) if ! [ -e "${mangled}" ] then - echo "Error: no GotoC file found. Expected: build/${TARGET}/debug/deps/multifile*.for-main.c" + echo "Error: no GotoC file found. Expected: build/kani/${TARGET}/debug/deps/multifile*_main.c" exit 1 fi -demangled=$(ls multifile*.for-main.demangled.c) +demangled=$(ls multifile*_main.demangled.c) if ! [ -e "${demangled}" ] then - echo "Error: no demangled GotoC file found. Expected build/${TARGET}/debug/deps/multifile*.for-main.demangled.c." + echo "Error: no demangled GotoC file found. Expected build/kani/${TARGET}/debug/deps/multifile*_main.demangled.c." exit 1 fi