Introduce project and stop merging all files generated by the compiler (rust-lang#1956)

This PR is a pre-req for getting a per-harness reachability algorithm. First we need to stop treating all goto generated by the compiler as the same model which is what this PR does.

For that, I introduce the concept of a project, which is basically a container of artifacts produced by the build system. The goal is to abstracts the verification code from the build system we pick. It also provide methods to get artifacts relevant to a harness. Today this method will return the artifact related to the crate where it is contained, but in the future it can be easily modified to be the harness specific goto model.

The only behavioral change in this PR is that we disabled `--gen-c` for `--function` and `--legacy-linker` to simplify the code since all these options are for internal usage or on track to be deleted.

This change also fixes inconsistent / incorrect behaviors. They are the following:

1. Kani is now sound when two or more targets contains harnesses or no mangled functions that have the same name (rust-lang#1974). Note that this is not the case for `--legacy-linker` and `--function` options.
2. `kani` now respects the `--target-dir` argument provided by the customer.
3. `kani` no longer crash when the crate has no harness (rust-lang#1910).

Co-authored-by: Zyad Hassan <[email protected]>

Author: celinval

kani-driver/src/args.rs

@@ -4,7 +4,7 @@
 #[cfg(feature = "unsound_experiments")]
 use crate::unsound_experiments::UnsoundExperimentArgs;
 
-use clap::{error::Error, error::ErrorKind, Parser, ValueEnum};
+use clap::{error::Error, error::ErrorKind, CommandFactory, Parser, ValueEnum};
 use std::ffi::OsString;
 use std::path::PathBuf;
 
@@ -72,7 +72,8 @@ pub struct KaniArgs {
         value_enum
     )]
     pub concrete_playback: Option<ConcretePlaybackMode>,
-    /// Keep temporary files generated throughout Kani process
+    /// Keep temporary files generated throughout Kani process. This is already the default
+    /// behavior for `cargo-kani`.
     #[arg(long, hide_short_help = true)]
     pub keep_temps: bool,
 
@@ -96,11 +97,12 @@ pub struct KaniArgs {
 
     /// Generate C file equivalent to inputted program.
     /// This feature is unstable and it requires `--enable-unstable` to be used
-    #[arg(long, hide_short_help = true, requires("enable_unstable"))]
+    #[arg(long, hide_short_help = true, requires("enable_unstable"),
+        conflicts_with_all(&["function", "legacy_linker"])
+)]
     pub gen_c: bool,
 
-    // TODO: currently only cargo-kani pays attention to this.
-    /// Directory for all generated artifacts. Only effective when running Kani with cargo
+    /// Directory for all generated artifacts.
     #[arg(long)]
     pub target_dir: Option<PathBuf>,
 
@@ -371,11 +373,39 @@ impl CheckArgs {
 impl StandaloneArgs {
     pub fn validate(&self) {
         self.common_opts.validate::<Self>();
+        self.valid_input()
+            .or_else(|e| -> Result<(), ()> { e.format(&mut Self::command()).exit() })
+            .unwrap()
+    }
+
+    fn valid_input(&self) -> Result<(), Error> {
+        if !self.input.is_file() {
+            Err(Error::raw(
+                ErrorKind::InvalidValue,
+                &format!(
+                    "Invalid argument: Input invalid. `{}` is not a regular file.",
+                    self.input.display()
+                ),
+            ))
+        } else {
+            Ok(())
+        }
     }
 }
 impl CargoKaniArgs {
     pub fn validate(&self) {
         self.common_opts.validate::<Self>();
+        // --assess requires --enable-unstable, but the subcommand needs manual checking
+        if (matches!(self.command, Some(CargoKaniSubcommand::Assess)) || self.common_opts.assess)
+            && !self.common_opts.enable_unstable
+        {
+            Self::command()
+                .error(
+                    ErrorKind::MissingRequiredArgument,
+                    "Assess is unstable and requires 'cargo kani --enable-unstable assess'",
+                )
+                .exit()
+        }
     }
 }
 impl KaniArgs {
@@ -454,6 +484,17 @@ impl KaniArgs {
                 "The `--dry-run` option is obsolete. Use --verbose instead.",
             ));
         }
+        if let Some(out_dir) = &self.target_dir {
+            if out_dir.exists() && !out_dir.is_dir() {
+                return Err(Error::raw(
+                    ErrorKind::InvalidValue,
+                    &format!(
+                        "Invalid argument: `--target-dir` argument `{}` is not a directory",
+                        out_dir.display()
+                    ),
+                ));
+            }
+        }
 
         Ok(())
     }
@@ -524,6 +565,14 @@ mod tests {
         assert_eq!(err.kind(), ErrorKind::ValueValidation);
     }
 
+    /// Kani should fail if the argument given is not a file.
+    #[test]
+    fn check_invalid_input_fails() {
+        let args = vec!["kani", "."];
+        let err = StandaloneArgs::parse_from(&args).valid_input().unwrap_err();
+        assert_eq!(err.kind(), ErrorKind::InvalidValue);
+    }
+
     #[test]
     fn check_unwind_conflicts() {
         // --unwind cannot be called without --harness

kani-driver/src/assess.rs

@@ -1,13 +1,15 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use std::{collections::HashMap, path::PathBuf};
+use std::collections::HashMap;
 
 use anyhow::Result;
 use comfy_table::Table;
-use kani_metadata::{ArtifactType, KaniMetadata};
+use kani_metadata::KaniMetadata;
 
 use crate::harness_runner::HarnessResult;
+use crate::metadata::merge_kani_metadata;
+use crate::project;
 use crate::session::KaniSession;
 
 /// Set some defaults for how we format tables
@@ -211,65 +213,42 @@ fn build_promising_tests_table(results: &[HarnessResult]) -> Table {
     }
 }
 
-pub(crate) fn cargokani_assess_main(mut ctx: KaniSession) -> Result<()> {
+pub(crate) fn cargokani_assess_main(mut session: KaniSession) -> Result<()> {
     // fix some settings
-    ctx.args.unwind = Some(1);
-    ctx.args.tests = true;
-    ctx.args.output_format = crate::args::OutputFormat::Terse;
-    ctx.codegen_tests = true;
-    if ctx.args.jobs.is_none() {
+    session.args.unwind = Some(1);
+    session.args.tests = true;
+    session.args.output_format = crate::args::OutputFormat::Terse;
+    session.codegen_tests = true;
+    if session.args.jobs.is_none() {
         // assess will default to fully parallel instead of single-threaded.
         // can be overridden with e.g. `cargo kani --enable-unstable -j 8 assess`
-        ctx.args.jobs = Some(None); // -j, num_cpu
+        session.args.jobs = Some(None); // -j, num_cpu
     }
 
-    let outputs = ctx.cargo_build()?;
-    let metadata = ctx.collect_kani_metadata(&outputs.metadata)?;
+    let project = project::cargo_project(&session)?;
 
-    let crate_count = outputs.metadata.len();
+    let crate_count = project.metadata.len();
 
     // An interesting thing to print here would be "number of crates without any warnings"
     // however this will have to wait until a refactoring of how we aggregate metadata
     // from multiple crates together here.
     // tracking for that: https://github.com/model-checking/kani/issues/1758
     println!("Analyzed {crate_count} crates");
 
+    let metadata = merge_kani_metadata(project.metadata.clone());
     if !metadata.unsupported_features.is_empty() {
         println!("{}", build_unsupported_features_table(&metadata));
     } else {
         println!("No crates contained Rust features unsupported by Kani");
     }
 
-    // The section is a "copy and paste" from cargo kani.
-    // We could start thinking about abtracting this stuff out into a shared function...
-    let mut goto_objs: Vec<PathBuf> = Vec::new();
-    for symtab in &outputs.symtabs {
-        let goto_obj_filename = symtab.with_extension(ArtifactType::Goto);
-        goto_objs.push(goto_obj_filename);
-    }
-
-    if ctx.args.only_codegen {
+    if session.args.only_codegen {
         return Ok(());
     }
 
-    let linked_obj = outputs.outdir.join("cbmc-linked.out");
-    ctx.link_goto_binary(&goto_objs, &linked_obj)?;
-    if let Some(restrictions) = outputs.restrictions {
-        ctx.apply_vtable_restrictions(&linked_obj, &restrictions)?;
-    }
-
     // Done with the 'cargo-kani' part, now we're going to run *test* harnesses instead of proof:
-
     let harnesses = metadata.test_harnesses;
-    let report_base = ctx.args.target_dir.clone().unwrap_or(PathBuf::from("target"));
-
-    let runner = crate::harness_runner::HarnessRunner {
-        sess: &ctx,
-        linked_obj: &linked_obj,
-        report_base: &report_base,
-        symtabs: &outputs.symtabs,
-        retain_specialized_harnesses: false,
-    };
+    let runner = crate::harness_runner::HarnessRunner { sess: &session, project };
 
     let results = runner.check_all_harnesses(&harnesses)?;
 

kani-driver/src/call_goto_instrument.rs

@@ -9,20 +9,27 @@ use std::path::Path;
 use std::process::Command;
 
 use crate::metadata::collect_and_link_function_pointer_restrictions;
+use crate::project::Project;
 use crate::session::KaniSession;
 use crate::util::alter_extension;
+use kani_metadata::{ArtifactType, HarnessMetadata};
 
 impl KaniSession {
-    /// Postprocess a goto binary (before cbmc, after linking) in-place by calling goto-instrument
-    pub fn run_goto_instrument(
+    /// Instrument and optimize a goto binary in-place.
+    pub fn instrument_model(
         &self,
         input: &Path,
         output: &Path,
-        symtabs: &[impl AsRef<Path>],
-        function: &str,
+        project: &Project,
+        harness: &HarnessMetadata,
     ) -> Result<()> {
         // We actually start by calling goto-cc to start the specialization:
-        self.specialize_to_proof_harness(input, output, function)?;
+        self.specialize_to_proof_harness(input, output, &harness.mangled_name)?;
+
+        let restrictions = project.get_harness_artifact(&harness, ArtifactType::VTableRestriction);
+        if let Some(restrictions_path) = restrictions {
+            self.apply_vtable_restrictions(&output, restrictions_path)?;
+        }
 
         // Run sanity checks in the model generated by kani-compiler before any goto-instrument
         // transformation.
@@ -50,7 +57,8 @@ impl KaniSession {
             }
 
             let c_demangled = alter_extension(output, "demangled.c");
-            self.demangle_c(symtabs, &c_outfile, &c_demangled)?;
+            let symtab = project.get_harness_artifact(&harness, ArtifactType::SymTab).unwrap();
+            self.demangle_c(symtab, &c_outfile, &c_demangled)?;
             if !self.args.quiet {
                 println!("Demangled GotoC code written to {}", c_demangled.to_string_lossy())
             }
@@ -60,19 +68,16 @@ impl KaniSession {
     }
 
     /// Apply --restrict-vtable to a goto binary.
-    /// `source` is either a `*.restrictions.json` file or a directory containing mutiple such files.
-    pub fn apply_vtable_restrictions(&self, file: &Path, source: &Path) -> Result<()> {
-        let linked_restrictions = alter_extension(file, "linked-restrictions.json");
-
+    pub fn apply_vtable_restrictions(&self, goto_file: &Path, restrictions: &Path) -> Result<()> {
+        let linked_restrictions = alter_extension(goto_file, "linked-restrictions.json");
         self.record_temporary_files(&[&linked_restrictions]);
-
-        collect_and_link_function_pointer_restrictions(source, &linked_restrictions)?;
+        collect_and_link_function_pointer_restrictions(restrictions, &linked_restrictions)?;
 
         let args: Vec<OsString> = vec![
             "--function-pointer-restrictions-file".into(),
             linked_restrictions.into(),
-            file.to_owned().into_os_string(), // input
-            file.to_owned().into_os_string(), // output
+            goto_file.to_owned().into_os_string(), // input
+            goto_file.to_owned().into_os_string(), // output
         ];
 
         self.call_goto_instrument(args)
@@ -154,29 +159,27 @@ impl KaniSession {
         self.call_goto_instrument(args)
     }
 
-    /// Generate a .demangled.c file from the .c file using the `prettyName`s from the symbol tables
+    /// Generate a .demangled.c file from the .c file using the `prettyName`s from the symbol table
     ///
     /// 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<Path>],
+        symtab_file: &impl AsRef<Path>,
         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);
-                        }
+        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);
                     }
                 }
             }