Run all proof harnesses by default

docs/src/kani-single-file.md

@@ -22,9 +22,9 @@ kani filenames.rs --visualize --cbmc-args --object-bits 11 --unwind 15
 **`--visualize`** will generate a report in the local directory accessible through `report/html/index.html`.
 This report will shows coverage information, as well as give traces for each failure Kani finds.
 
-**`--function <name>`** Kani defaults to assuming the starting function is called `main`.
-You can change it to a different function with this argument.
-Note that to "find" the function given, it needs to be given the `#[kani::proof]` annotation.
+**`--harness <name>`** Kani defaults to running all found proof harnesses.
+You can switch to running just one using this flag.
+Proof harnesses are functions that have been given the `#[kani::proof]` annotation.
 
 **`--gen-c`** will generate a C file that roughly corresponds to the input Rust file.
 This can sometimes be helpful when trying to debug a problem with Kani.

docs/src/tutorial-first-steps.md

@@ -185,7 +185,7 @@ Fortunately, Kani is able to report a coverage metric for each proof harness.
 Try running:
 
 ```
-kani --visualize src/final_form.rs --function verify_success
+kani --visualize src/final_form.rs --harness verify_success
 open report/html/index.html
 ```
 

docs/src/tutorial-kinds-of-failure.md

@@ -43,7 +43,7 @@ But we're able to check this unsafe code with Kani:
 ```
 
 ```
-# kani src/bounds_check.rs --function bound_check
+# kani src/bounds_check.rs --harness bound_check
 [...]
 ** 15 of 448 failed
 [...]
@@ -56,7 +56,7 @@ Kani is inserting a lot more checks than appear as asserts in our code, so the o
 Let's narrow that output down a bit:
 
 ```
-# kani src/bounds_check.rs --function bound_check | grep Failed
+# kani src/bounds_check.rs --harness bound_check | grep Failed
 Failed Checks: attempt to compute offset which would overflow
 Failed Checks: attempt to calculate the remainder with a divisor of zero
 Failed Checks: attempt to add with overflow
@@ -92,7 +92,7 @@ Consider trying a few more small exercises with this example:
 Having switched back to the safe indexing operation, Kani reports two failures:
 
 ```
-# kani src/bounds_check.rs --function bound_check | grep Failed
+# kani src/bounds_check.rs --harness bound_check | grep Failed
 Failed Checks: index out of bounds: the length is less than or equal to the given index
 Failed Checks: dereference failure: pointer outside object bounds
 ```
@@ -176,7 +176,7 @@ Kani will find these failures as well.
 Here's the output from Kani:
 
 ```
-# kani src/overflow.rs --function add_overflow
+# kani src/overflow.rs --harness add_overflow
 [...]
 RESULTS:
 Check 1: simple_addition.assertion.1

docs/src/tutorial-nondeterministic-variables.md

@@ -32,7 +32,7 @@ You can try it out by running the example under
 [arbitrary-variables directory](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/):
 
 ```
-cargo kani --function safe_update
+cargo kani --harness safe_update
 ```
 
 ## Unsafe nondeterministic variables
@@ -57,7 +57,7 @@ The compiler is able to represent `Option<NonZeroU32>` using `32` bits by using
 You can try it out by running the example under [arbitrary-variables directory](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/):
 
 ```
-cargo kani --function unsafe_update
+cargo kani --harness unsafe_update
 ```
 
 ## Safe nondeterministic variables for custom types
@@ -88,5 +88,5 @@ You can try it out by running the example under
 [`docs/src/tutorial/arbitrary-variables`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/):
 
 ```
-cargo kani --function check_rating
+cargo kani --harness check_rating
 ```

src/cargo-kani/src/args.rs

@@ -72,9 +72,12 @@ pub struct KaniArgs {
     #[structopt(flatten)]
     pub checks: CheckArgs,
 
-    /// Entry point for verification
-    #[structopt(long, default_value = "main")]
-    pub function: String,
+    /// Entry point for verification (symbol name)
+    #[structopt(long, hidden = true)]
+    pub function: Option<String>,
+    /// Entry point for verification (proof harness)
+    #[structopt(long, conflicts_with = "function", conflicts_with = "dry-run")]
+    pub harness: Option<String>,
     /// Link external C files referenced by Rust code
     #[structopt(long, parse(from_os_str))]
     pub c_lib: Vec<PathBuf>,
@@ -316,4 +319,13 @@ mod tests {
             assert_eq!(t, format!("{}", AbstractionType::from_str(t).unwrap()));
         }
     }
+
+    #[test]
+    fn check_dry_run_harness_conflicts() {
+        // harness needs metadata which we don't have with dry-run
+        let args = vec!["kani", "file.rs", "--dry-run", "--harness", "foo"];
+        let app = StandaloneArgs::clap();
+        let err = app.get_matches_from_safe(args).unwrap_err();
+        assert!(err.kind == ErrorKind::ArgumentConflict);
+    }
 }

src/cargo-kani/src/call_cargo.rs

@@ -3,7 +3,7 @@
 
 use anyhow::{Context, Result};
 use std::ffi::OsString;
-use std::path::PathBuf;
+use std::path::{Path, PathBuf};
 use std::process::Command;
 
 use crate::session::KaniSession;
@@ -17,6 +17,8 @@ pub struct CargoOutputs {
     pub symtabs: 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.
+    pub metadata: Vec<PathBuf>,
 }
 
 impl KaniSession {
@@ -44,7 +46,7 @@ impl KaniSession {
         args.push(build_target.into());
 
         args.push("--target-dir".into());
-        args.push(target_dir.clone().into());
+        args.push(target_dir.into());
 
         if self.args.verbose {
             args.push("-v".into());
@@ -59,26 +61,26 @@ impl KaniSession {
         self.run_terminal(cmd)?;
 
         if self.args.dry_run {
-            // mock an answer
+            // mock an answer: mostly the same except we don't/can't expand the globs
             return Ok(CargoOutputs {
                 outdir: outdir.clone(),
-                symtabs: vec![outdir.join("dry-run.symtab.json")],
+                symtabs: vec![outdir.join("*.symtab.json")],
+                metadata: vec![outdir.join("*.kani-metadata.json")],
                 restrictions: self.args.restrict_vtable().then(|| outdir),
             });
         }
 
-        let symtabs = glob(&outdir.join("*.symtab.json"));
-
         Ok(CargoOutputs {
             outdir: outdir.clone(),
-            symtabs: symtabs?,
+            symtabs: glob(&outdir.join("*.symtab.json"))?,
+            metadata: glob(&outdir.join("*.kani-metadata.json"))?,
             restrictions: self.args.restrict_vtable().then(|| outdir),
         })
     }
 }
 
 /// Given a `path` with glob characters in it (e.g. `*.json`), return a vector of matching files
-fn glob(path: &PathBuf) -> Result<Vec<PathBuf>> {
+fn glob(path: &Path) -> Result<Vec<PathBuf>> {
     let results = glob::glob(path.to_str().context("Non-UTF-8 path enountered")?)?;
     // the logic to turn "Iter<Result<T, E>>" into "Result<Vec<T>, E>" doesn't play well
     // with anyhow, so a type annotation is required

src/cargo-kani/src/call_goto_instrument.rs

@@ -6,14 +6,10 @@ use std::ffi::OsString;
 use std::path::Path;
 use std::process::Command;
 
+use crate::metadata::collect_and_link_function_pointer_restrictions;
 use crate::session::KaniSession;
 use crate::util::alter_extension;
 
-use kani_metadata::{InternedString, TraitDefinedMethod, VtableCtxResults};
-use std::collections::HashMap;
-use std::fs::File;
-use std::io::{BufReader, BufWriter};
-
 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<()> {
@@ -28,6 +24,7 @@ impl KaniSession {
         }
 
         if self.args.gen_c {
+            println!("Wrote {}", output.to_string_lossy());
             self.gen_c(output)?;
         }
 
@@ -124,77 +121,3 @@ impl KaniSession {
         self.run_suppress(cmd)
     }
 }
-
-/// Collect all vtable restriction metadata together, and write one combined output in CBMC's format
-fn link_function_pointer_restrictions(
-    data_per_crate: Vec<VtableCtxResults>,
-    output_filename: &Path,
-) -> Result<()> {
-    // Combine all method possibilities into one global mapping
-    let mut combined_possible_methods: HashMap<TraitDefinedMethod, Vec<InternedString>> =
-        HashMap::new();
-    for crate_data in &data_per_crate {
-        for entry in &crate_data.possible_methods {
-            combined_possible_methods
-                .insert(entry.trait_method.clone(), entry.possibilities.clone());
-        }
-    }
-
-    // Emit a restriction for every call site
-    let mut output = HashMap::new();
-    for crate_data in data_per_crate {
-        for call_site in crate_data.call_sites {
-            // CBMC Now supports referencing callsites by label:
-            // https://github.com/diffblue/cbmc/pull/6508
-            let cbmc_call_site_name = format!("{}.{}", call_site.function_name, call_site.label);
-            let trait_def = call_site.trait_method;
-
-            // Look up all possibilities, defaulting to the empty set
-            let possibilities =
-                combined_possible_methods.get(&trait_def).unwrap_or(&vec![]).clone();
-            output.insert(cbmc_call_site_name, possibilities);
-        }
-    }
-
-    let f = File::create(output_filename)?;
-    let f = BufWriter::new(f);
-    serde_json::to_writer(f, &output)?;
-    Ok(())
-}
-
-/// From either a file or a path with multiple files, output the CBMC restrictions file we should use.
-fn collect_and_link_function_pointer_restrictions(
-    path: &Path,
-    output_filename: &Path,
-) -> Result<()> {
-    let md = std::fs::metadata(path)?;
-
-    // Fill with data from all files in that path with the expected suffix
-    let mut per_crate_restrictions = Vec::new();
-
-    if md.is_dir() {
-        for element in path.read_dir()? {
-            let path = element?.path();
-            if path.as_os_str().to_str().unwrap().ends_with(".restrictions.json") {
-                let restrictions = read_restrictions(&path)?;
-                per_crate_restrictions.push(restrictions);
-            }
-        }
-    } else if md.is_file() {
-        assert!(path.as_os_str().to_str().unwrap().ends_with(".restrictions.json"));
-        let restrictions = read_restrictions(path)?;
-        per_crate_restrictions.push(restrictions);
-    } else {
-        unreachable!("Path must be restrcitions file or directory containing restrictions files")
-    }
-
-    link_function_pointer_restrictions(per_crate_restrictions, output_filename)
-}
-
-/// Deserialize a *.restrictions.json file
-fn read_restrictions(path: &Path) -> Result<VtableCtxResults> {
-    let file = File::open(path)?;
-    let reader = BufReader::new(file);
-    let restrictions = serde_json::from_reader(reader)?;
-    Ok(restrictions)
-}

src/cargo-kani/src/call_single_file.rs

@@ -18,6 +18,8 @@ pub struct SingleOutputs {
     pub symtab: PathBuf,
     /// The vtable restrictions files, if any.
     pub restrictions: Option<PathBuf>,
+    /// The kani-metadata.json file written by kani-compiler.
+    pub metadata: PathBuf,
 }
 
 impl KaniSession {
@@ -34,7 +36,7 @@ impl KaniSession {
             let mut temps = self.temporaries.borrow_mut();
             temps.push(output_filename.clone());
             temps.push(typemap_filename);
-            temps.push(metadata_filename);
+            temps.push(metadata_filename.clone());
             if self.args.restrict_vtable() {
                 temps.push(restrictions_filename.clone());
             }
@@ -55,14 +57,9 @@ impl KaniSession {
                 args.push(t);
             }
         } else {
-            if self.args.function != "main" {
-                // Unless entry function for proof harness is main, compile code as lib.
-                // This ensures that rustc won't prune functions that are not reachable
-                // from main as well as enable compilation of crates that don't have a main
-                // function.
-                args.push("--crate-type".into());
-                args.push("lib".into());
-            }
+            // Don't require a 'main' function to exist. We only run against proof harnesses.
+            args.push("--crate-type".into());
+            args.push("lib".into());
         }
 
         let mut cmd = Command::new(&self.kani_compiler);
@@ -80,6 +77,7 @@ impl KaniSession {
         Ok(SingleOutputs {
             outdir,
             symtab: output_filename,
+            metadata: metadata_filename,
             restrictions: if self.args.restrict_vtable() {
                 Some(restrictions_filename)
             } else {