diff --git a/src/cargo-kani/src/call_cargo.rs b/src/cargo-kani/src/call_cargo.rs index d1d02184800d..25df4b03dcf2 100644 --- a/src/cargo-kani/src/call_cargo.rs +++ b/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>" into "Result, E>" doesn't play well - // with anyhow, so a type annotation is required - let symtabs: core::result::Result, 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> { + let results = glob::glob(path.to_str().context("Non-UTF-8 path enountered")?)?; + // the logic to turn "Iter>" into "Result, E>" doesn't play well + // with anyhow, so a type annotation is required + let v: core::result::Result, glob::GlobError> = results.collect(); + Ok(v?) +} diff --git a/src/cargo-kani/src/call_goto_cc.rs b/src/cargo-kani/src/call_goto_cc.rs index 691911f1d904..5d8d76c263bf 100644 --- a/src/cargo-kani/src/call_goto_cc.rs +++ b/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 = 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 = 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(()) + } } diff --git a/src/cargo-kani/src/call_goto_instrument.rs b/src/cargo-kani/src/call_goto_instrument.rs index 9414d6de743b..23c1c9481fc7 100644 --- a/src/cargo-kani/src/call_goto_instrument.rs +++ b/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 = 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 = 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 = vec![ "--drop-unused-functions".into(), diff --git a/src/cargo-kani/src/main.rs b/src/cargo-kani/src/main.rs index cfb381aed0ca..0b9d66e95dc1 100644 --- a/src/cargo-kani/src/main.rs +++ b/src/cargo-kani/src/main.rs @@ -42,18 +42,20 @@ fn cargokani_main(mut input_args: Vec) -> 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")?; diff --git a/tests/expected/dry-run/expected b/tests/expected/dry-run/expected index 4ac86a1e8406..a5cf02609518 100644 --- a/tests/expected/dry-run/expected +++ b/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