Separate cmbc-linked and harness-specialized goto binaries (rust-lang…

…#913)

* factor out globbing to a helper function

* Separate cmbc-linked and harness-specialized goto binaries

src/cargo-kani/src/call_cargo.rs

@@ -62,20 +62,12 @@ impl KaniSession {
             // mock an answer
             return Ok(CargoOutputs {
                 outdir: outdir.clone(),
-                symtabs: vec![target_dir.join(build_target).join("debug/deps/dry-run.symtab.json")],
+                symtabs: vec![outdir.join("dry-run.symtab.json")],
                 restrictions: self.args.restrict_vtable().then(|| outdir),
             });
         }
 
-        let build_glob = target_dir.join(build_target).join("debug/deps/*.symtab.json");
-        // There isn't a good way to glob with non-UTF-8 paths.
-        // https://github.com/rust-lang-nursery/glob/issues/78
-        let build_glob = build_glob.to_str().context("Non-UTF-8 path enountered")?;
-        let results = glob::glob(build_glob)?;
-
-        // 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
-        let symtabs: core::result::Result<Vec<PathBuf>, glob::GlobError> = results.collect();
+        let symtabs = glob(&outdir.join("*.symtab.json"));
 
         Ok(CargoOutputs {
             outdir: outdir.clone(),
@@ -84,3 +76,12 @@ impl KaniSession {
         })
     }
 }
+
+/// Given a `path` with glob characters in it (e.g. `*.json`), return a vector of matching files
+fn glob(path: &PathBuf) -> 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
+    let v: core::result::Result<Vec<PathBuf>, glob::GlobError> = results.collect();
+    Ok(v?)
+}

src/cargo-kani/src/call_goto_cc.rs

@@ -11,15 +11,9 @@ use crate::session::KaniSession;
 
 impl KaniSession {
     /// Given a set of goto binaries (`inputs`), produce `output` by linking everything
-    /// together (including essential libraries) and also specializing to the proof harness
-    /// `function`.
-    pub fn link_c_lib(&self, inputs: &[PathBuf], output: &Path, function: &str) -> Result<()> {
-        {
-            let mut temps = self.temporaries.borrow_mut();
-            temps.push(output.to_owned());
-        }
-
-        let mut args: Vec<OsString> = vec!["--function".into(), function.into()];
+    /// together (including essential libraries). The result is generic over all proof harnesses.
+    pub fn link_goto_binary(&self, inputs: &[PathBuf], output: &Path) -> Result<()> {
+        let mut args: Vec<OsString> = Vec::new();
         args.extend(inputs.iter().map(|x| x.clone().into_os_string()));
         args.extend(self.args.c_lib.iter().map(|x| x.clone().into_os_string()));
 
@@ -47,4 +41,19 @@ impl KaniSession {
 
         Ok(())
     }
+
+    /// Produce a goto binary with its entry point set to a particular proof harness.
+    pub fn specialize_to_proof_harness(
+        &self,
+        input: &Path,
+        output: &Path,
+        function: &str,
+    ) -> Result<()> {
+        let mut cmd = Command::new("goto-cc");
+        cmd.arg(input).args(["--function", function, "-o"]).arg(output);
+
+        self.run_suppress(cmd)?;
+
+        Ok(())
+    }
 }

src/cargo-kani/src/call_goto_instrument.rs

@@ -16,16 +16,19 @@ 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, file: &Path) -> Result<()> {
+    pub fn run_goto_instrument(&self, input: &Path, output: &Path, function: &str) -> Result<()> {
+        // We actually start by calling goto-cc to start the specialization:
+        self.specialize_to_proof_harness(input, output, function)?;
+
         if self.args.checks.undefined_function_on() {
-            self.add_library(file)?;
-            self.undefined_functions(file)?;
+            self.add_library(output)?;
+            self.undefined_functions(output)?;
         } else {
-            self.just_drop_unused_functions(file)?;
+            self.just_drop_unused_functions(output)?;
         }
 
         if self.args.gen_c {
-            self.gen_c(file)?;
+            self.gen_c(output)?;
         }
 
         Ok(())
@@ -53,6 +56,10 @@ impl KaniSession {
         self.call_goto_instrument(args)
     }
 
+    /// Link the binary against the CBMC model for C library functions.
+    /// Normally this happens implicitly, but we use this explicitly
+    /// before we invoke `undefined_functions` below, otherwise these
+    /// functions appear undefined.
     fn add_library(&self, file: &Path) -> Result<()> {
         let args: Vec<OsString> = vec![
             "--add-library".into(),
@@ -63,6 +70,12 @@ impl KaniSession {
         self.call_goto_instrument(args)
     }
 
+    /// Instruct CBMC to "assert false" when invoking an undefined function.
+    /// (This contrasts with its default behavior of returning `nondet`, which is
+    /// unsound in the face of side-effects.)
+    /// Then remove unused functions. (Oddly, it seems CBMC will both see some
+    /// functions as unused and remove them, and also as used and so would
+    /// generate "assert false". So it's essential to do this afterwards.)
     fn undefined_functions(&self, file: &Path) -> Result<()> {
         let args: Vec<OsString> = vec![
             "--generate-function-body-options".into(),
@@ -77,6 +90,7 @@ impl KaniSession {
         self.call_goto_instrument(args)
     }
 
+    /// Remove all functions unreachable from the current proof harness.
     fn just_drop_unused_functions(&self, file: &Path) -> Result<()> {
         let args: Vec<OsString> = vec![
             "--drop-unused-functions".into(),

src/cargo-kani/src/main.rs

@@ -42,18 +42,20 @@ fn cargokani_main(mut input_args: Vec<OsString>) -> Result<()> {
     for symtab in &outputs.symtabs {
         goto_objs.push(ctx.symbol_table_to_gotoc(symtab)?);
     }
-    let linked_obj = outputs.outdir.join("cbmc.out");
 
-    ctx.link_c_lib(&goto_objs, &linked_obj, &ctx.args.function)?;
+    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)?;
     }
-    ctx.run_goto_instrument(&linked_obj)?;
+
+    let specialized_obj = outputs.outdir.join(format!("cbmc-for-{}.out", &ctx.args.function));
+    ctx.run_goto_instrument(&linked_obj, &specialized_obj, &ctx.args.function)?;
 
     if ctx.args.visualize {
-        ctx.run_visualize(&linked_obj, "target/report")?;
+        ctx.run_visualize(&specialized_obj, "target/report")?;
     } else {
-        let result = ctx.run_cbmc(&linked_obj)?;
+        let result = ctx.run_cbmc(&specialized_obj)?;
         if result == VerificationStatus::Failure {
             // Failure exit code without additional error message
             drop(ctx);
@@ -71,13 +73,17 @@ fn standalone_main() -> Result<()> {
 
     let outputs = ctx.compile_single_rust_file(&args.input)?;
     let goto_obj = ctx.symbol_table_to_gotoc(&outputs.symtab)?;
-    let linked_obj = util::alter_extension(&args.input, "out");
 
-    ctx.link_c_lib(&[goto_obj], &linked_obj, &ctx.args.function)?;
+    let linked_obj = util::alter_extension(&args.input, "out");
+    {
+        let mut temps = ctx.temporaries.borrow_mut();
+        temps.push(linked_obj.to_owned());
+    }
+    ctx.link_goto_binary(&[goto_obj], &linked_obj)?;
     if let Some(restriction) = outputs.restrictions {
         ctx.apply_vtable_restrictions(&linked_obj, &restriction)?;
     }
-    ctx.run_goto_instrument(&linked_obj)?;
+    ctx.run_goto_instrument(&linked_obj, &linked_obj, &ctx.args.function)?;
 
     if ctx.args.visualize {
         ctx.run_visualize(&linked_obj, "report")?;

tests/expected/dry-run/expected

@@ -1,4 +1,6 @@
 kani-rustc --goto-c
 symtab2gb
-goto-cc --function main
+goto-cc
+--function main
+goto-instrument
 cbmc --bounds-check --pointer-check --pointer-primitive-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --undefined-shift-check --unwinding-assertions --object-bits 16