Avoid an unnecssary suffix to the goto filename (#2472)

Author: zhassan-aws

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::<Result<Vec<_>>>()

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"));
-    }
 }

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);
+            }
+        }
+    }
+}

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