Feature : Unwind attribute (model-checking#1031)

* Hook up unwind attribute to Kani

* Add tests and make Harness, a required argument

* Refactor tests and replace --unwind with --default-unwind

docs/src/kani-single-file.md

@@ -24,7 +24,7 @@ The most common `kani` arguments are the following:
  * `--harness <name>`: By default, Kani checks all proof harnesses it finds. You
    can switch to checking a single harness using this flag.
 
- * `--unwind <n>`: Set a global upper [loop
+ * `--default-unwind <n>`: Set a global upper [loop
    unwinding](./tutorial-loop-unwinding.md) bound on all loops. This can force
    termination when CBMC tries to unwind loops indefinitely.
 

docs/src/regression-testing.md

@@ -107,7 +107,7 @@ be specified in single Rust files by adding a comment at the top of the file:
 For example, to use an unwinding value of 4 in a test, we can write:
 
 ```rust,noplaypen
-// kani-flags: --unwind 4
+// kani-flags: --default-unwind 4
 ```
 
 For `cargo-kani` tests, the preferred way to pass command-line options is adding

docs/src/tutorial-loop-unwinding.md

@@ -30,13 +30,13 @@ Bounding proofs like this means we may no longer be proving as much as we origin
 Who's to say, if we prove everything works up to size 10, that there isn't a novel bug lurking, expressible only with problems of size 11+?
 But, let's get back to the issue at hand.
 
-We can "make progress" in our work by giving Kani a global bound on the problem size using the `--unwind <bound>` flag.
+We can "make progress" in our work by giving Kani a global bound on the problem size using the `--default-unwind <bound>` flag.
 This flag puts a fixed upper bound on loop unwinding.
 Kani will automatically generate verification conditions that help us understand if that bound isn't enough.
 Let's start with a small unwinding value:
 
 ```
-# kani src/lib.rs --unwind 1
+# kani src/lib.rs --default-unwind 1
 Check 69: .unwind.0
          - Status: FAILURE
          - Description: "unwinding assertion loop 0"
@@ -50,19 +50,19 @@ This output is showing us two things:
 2. We aren't seeing other failures if we only unwind the loop once.
 The execution can't progress far enough to reveal the bug we're interested in (which actually only happens in the last iteration of the loop).
 
-Doing an initial `--unwind 1` is generally enough to force termination, but often too little for verification.
+Doing an initial `--default-unwind 1` is generally enough to force termination, but often too little for verification.
 
 We were clearly aiming at a size limit of 10 in our proof harness, so let's try a few things:
 
 ```
-# kani src/lib.rs --unwind 10 | grep Failed
+# kani src/lib.rs --default-unwind 10 | grep Failed
 Failed Checks: unwinding assertion loop 0
 ```
 
 A bound of 10 still isn't enough because we generally need to unwind one greater than the number of executed loop iterations:
 
 ```
-# kani src/lib.rs --unwind 11 | grep Failed
+# kani src/lib.rs --default-unwind 11 | 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
 Failed Checks: unwinding assertion loop 0
@@ -72,12 +72,12 @@ We're still not seeing the unwinding assertion failure go away!
 This is because our error is really an off-by-one problem, we loop one too many times, so let's add one more:
 
 ```
-# kani src/lib.rs --unwind 12 | grep Failed
+# kani src/lib.rs --default-unwind 12 | 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
 ```
 
 Kani is now sure we've unwound the loop enough to verify our proof harness, and now we're seeing just the bound checking failures from the off-by-one error.
 
 1. Exercise: Fix the off-by-one bounds error and get Kani to verify successfully.
-2. Exercise: After fixing the error, `--unwind 11` works. Why?
+2. Exercise: After fixing the error, `--default-unwind 11` works. Why?

docs/src/tutorial-real-code.md

@@ -77,7 +77,7 @@ Running Kani on this simple starting point will help figure out:
 2. Whether you're over-constrained. Check the coverage report using `--visualize`. Ideally you'd see 100% coverage, and if not, it's usually because now you've over-constrained the inputs.
 3. Whether Kani will support all the Rust features involved.
 4. Whether you've started with a tractable problem.
-(If the problem is initially intractable, try `--unwind 1` and see if you can follow the techniques in the previous section to put a bound on the problem.)
+(If the problem is initially intractable, try `--default-unwind 1` and see if you can follow the techniques in the previous section to put a bound on the problem.)
 
 Once you've got something working, the next step is to prove more interesting properties than what Kani covers by default.
 You accomplish this by adding new assertions (not just in your harness, but also to the code being run).

docs/src/tutorial/loops-unwinding/Cargo.toml

@@ -5,9 +5,4 @@ name = "loops-unwinding"
 version = "0.1.0"
 edition = "2018"
 
-[dependencies]
-
-[workspace]
-
-[package.metadata.kani]
-flags = { unwind = "11" }
+[workspace]

docs/src/tutorial/loops-unwinding/src/lib.rs

@@ -17,6 +17,7 @@ fn initialize_prefix(length: usize, buffer: &mut [u8]) {
 // ANCHOR: kani
 #[cfg(kani)]
 #[kani::proof]
+#[kani::unwind(11)]
 fn main() {
     const LIMIT: usize = 10;
     let mut buffer: [u8; LIMIT] = [1; LIMIT];

docs/src/workarounds.md

@@ -6,7 +6,7 @@ issues in the Kani project.
 ## CBMC arguments
 
 Kani is able to handle common CBMC arguments as if they were its own (e.g.,
-`--unwind <n>`), but sometimes it may be necessary to use CBMC arguments which
+`--default-unwind <n>`), but sometimes it may be necessary to use CBMC arguments which
 are not handled by Kani.
 
 To pass additional arguments for CBMC, you pass `--cbmc-args` to Kani. Note that
@@ -26,7 +26,7 @@ cargo kani [<kani-args>]* --cbmc-args [<cbmc-args>]*
 
 ### Individual loop bounds
 
-Setting `--unwind <n>` affects every loop in a harness.
+Setting `--default-unwind <n>` affects every loop in a harness.
 Once you know a particular loop is causing trouble, sometimes it can be helpful to provide a specific bound for it.
 
 In the general case, specifying just the highest bound globally for all loops

kani-driver/src/args.rs

@@ -104,6 +104,9 @@ pub struct KaniArgs {
     pub object_bits: u32,
     /// Specify the value used for loop unwinding in CBMC
     #[structopt(long)]
+    pub default_unwind: Option<u32>,
+    /// Specify the value used for loop unwinding for the specified harness in CBMC
+    #[structopt(long, requires("harness"))]
     pub unwind: Option<u32>,
     /// Turn on automatic loop unwinding
     #[structopt(long)]
@@ -283,15 +286,15 @@ impl KaniArgs {
         let extra_unwind = self.cbmc_args.contains(&OsString::from("--unwind"));
         let extra_auto_unwind = self.cbmc_args.contains(&OsString::from("--auto-unwind"));
         let extras = extra_auto_unwind || extra_unwind;
-        let natives = self.auto_unwind || self.unwind.is_some();
+        let natives = self.auto_unwind || self.default_unwind.is_some();
         let any_auto_unwind = extra_auto_unwind || self.auto_unwind;
-        let any_unwind = self.unwind.is_some() || extra_unwind;
+        let any_unwind = self.default_unwind.is_some() || extra_unwind;
 
         // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified.
         // We should consider improving the error messages slightly in a later pull request.
         if any_auto_unwind && any_unwind {
             Error::with_description(
-                "Conflicting flags: `--auto-unwind` is not compatible with other `--unwind` flags.",
+                "Conflicting flags: `--auto-unwind` is not compatible with other `--default-unwind` flags.",
                 ErrorKind::ArgumentConflict,
             )
             .exit();
@@ -365,6 +368,15 @@ mod tests {
         assert_eq!(err.kind, ErrorKind::ArgumentConflict);
     }
 
+    #[test]
+    fn check_unwind_conflicts() {
+        // --unwind cannot be called without --harness
+        let args = vec!["kani", "file.rs", "--unwind", "3"];
+        let app = StandaloneArgs::clap();
+        let err = app.get_matches_from_safe(args).unwrap_err();
+        assert_eq!(err.kind, ErrorKind::MissingRequiredArgument);
+    }
+
     fn parse_unstable_disabled(args: &str) -> Result<ArgMatches<'_>, Error> {
         let args = format!("kani file.rs {}", args);
         let app = StandaloneArgs::clap();

kani-driver/src/args_toml.rs

@@ -152,18 +152,18 @@ mod tests {
     #[test]
     fn check_toml_parsing() {
         let a = "[workspace.metadata.kani]
-                      flags = { default-checks = false, unwind = \"2\", cbmc-args = [\"--fake\"] }";
+                      flags = { default-checks = false, default-unwind = \"2\", cbmc-args = [\"--fake\"] }";
         let b = toml_to_args(a).unwrap();
         // default first, then unwind thanks to btree ordering.
         // cbmc-args always last.
-        assert_eq!(b.0, vec!["--no-default-checks", "--unwind", "2"]);
+        assert_eq!(b.0, vec!["--no-default-checks", "--default-unwind", "2"]);
         assert_eq!(b.1, vec!["--cbmc-args", "--fake"]);
     }
 
     #[test]
     fn check_merge_args_with_only_command_line_args() {
         let cmd_args: Vec<OsString> =
-            ["cargo_kani", "--no-default-checks", "--unwind", "2", "--cbmc-args", "--fake"]
+            ["cargo_kani", "--no-default-checks", "--default-unwind", "2", "--cbmc-args", "--fake"]
                 .iter()
                 .map(|&s| s.into())
                 .collect();
@@ -174,7 +174,7 @@ mod tests {
     #[test]
     fn check_merge_args_with_only_config_kani_args() {
         let cfg_args: Vec<OsString> =
-            ["--no-default-checks", "--unwind", "2"].iter().map(|&s| s.into()).collect();
+            ["--no-default-checks", "--default-unwind", "2"].iter().map(|&s| s.into()).collect();
         let merged = merge_args(vec!["kani".into()], cfg_args.clone(), Vec::new()).unwrap();
         assert_eq!(merged[0], OsString::from("kani"));
         assert_eq!(merged[1..], cfg_args);

kani-driver/src/call_cbmc.rs

@@ -2,10 +2,12 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use anyhow::{bail, Result};
+use kani_metadata::HarnessMetadata;
 use std::ffi::OsString;
 use std::path::Path;
 use std::process::Command;
 
+use crate::args::KaniArgs;
 use crate::session::KaniSession;
 
 #[derive(PartialEq)]
@@ -16,15 +18,15 @@ pub enum VerificationStatus {
 
 impl KaniSession {
     /// Verify a goto binary that's been prepared with goto-instrument
-    pub fn run_cbmc(&self, file: &Path) -> Result<VerificationStatus> {
+    pub fn run_cbmc(&self, file: &Path, harness: &HarnessMetadata) -> Result<VerificationStatus> {
         let output_filename = crate::util::append_path(file, "cbmc_output");
 
         {
             let mut temps = self.temporaries.borrow_mut();
             temps.push(output_filename.clone());
         }
 
-        let args: Vec<OsString> = self.cbmc_flags(file)?;
+        let args: Vec<OsString> = self.cbmc_flags(file, harness)?;
 
         // TODO get cbmc path from self
         let mut cmd = Command::new("cbmc");
@@ -73,15 +75,19 @@ impl KaniSession {
     }
 
     /// "Internal," but also used by call_cbmc_viewer
-    pub fn cbmc_flags(&self, file: &Path) -> Result<Vec<OsString>> {
+    pub fn cbmc_flags(
+        &self,
+        file: &Path,
+        harness_metadata: &HarnessMetadata,
+    ) -> Result<Vec<OsString>> {
         let mut args = self.cbmc_check_flags();
 
         args.push("--object-bits".into());
         args.push(self.args.object_bits.to_string().into());
 
-        if let Some(unwind) = self.args.unwind {
+        if let Some(unwind_value) = resolve_unwind_value(&self.args, harness_metadata) {
             args.push("--unwind".into());
-            args.push(unwind.to_string().into());
+            args.push(unwind_value.to_string().into());
         } else if self.args.auto_unwind {
             args.push("--auto-unwind".into());
         }
@@ -127,3 +133,76 @@ impl KaniSession {
         args
     }
 }
+
+/// Solve Unwind Value from conflicting inputs of unwind values. (--default-unwind, annotation-unwind, --unwind)
+pub fn resolve_unwind_value(args: &KaniArgs, harness_metadata: &HarnessMetadata) -> Option<u32> {
+    // Check for which flag is being passed and prioritize extracting unwind from the
+    // respective flag/annotation.
+    if let Some(harness_unwind) = args.unwind {
+        Some(harness_unwind)
+    } else if let Some(annotation_unwind) = harness_metadata.unwind_value {
+        Some(annotation_unwind)
+    } else if let Some(default_unwind) = args.default_unwind {
+        Some(default_unwind)
+    } else {
+        None
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::args;
+    use crate::metadata::mock_proof_harness;
+    use structopt::StructOpt;
+
+    use super::*;
+
+    #[test]
+    fn check_resolve_unwind_value() {
+        // Command line unwind value for specific harnesses take precedence over default annotation value
+        let args_empty = ["kani"];
+        let args_only_default = ["kani", "--default-unwind", "2"];
+        let args_only_harness = ["kani", "--unwind", "1", "--harness", "check_one"];
+        let args_both =
+            ["kani", "--default-unwind", "2", "--unwind", "1", "--harness", "check_one"];
+
+        let harness_none = mock_proof_harness("check_one", None);
+        let harness_some = mock_proof_harness("check_one", Some(3));
+
+        // test against no unwind annotation
+        assert_eq!(
+            resolve_unwind_value(&args::KaniArgs::from_iter(args_empty), &harness_none),
+            None
+        );
+        assert_eq!(
+            resolve_unwind_value(&args::KaniArgs::from_iter(args_only_default), &harness_none),
+            Some(2)
+        );
+        assert_eq!(
+            resolve_unwind_value(&args::KaniArgs::from_iter(args_only_harness), &harness_none),
+            Some(1)
+        );
+        assert_eq!(
+            resolve_unwind_value(&args::KaniArgs::from_iter(args_both), &harness_none),
+            Some(1)
+        );
+
+        // test against unwind annotation
+        assert_eq!(
+            resolve_unwind_value(&args::KaniArgs::from_iter(args_empty), &harness_some),
+            Some(3)
+        );
+        assert_eq!(
+            resolve_unwind_value(&args::KaniArgs::from_iter(args_only_default), &harness_some),
+            Some(3)
+        );
+        assert_eq!(
+            resolve_unwind_value(&args::KaniArgs::from_iter(args_only_harness), &harness_some),
+            Some(1)
+        );
+        assert_eq!(
+            resolve_unwind_value(&args::KaniArgs::from_iter(args_both), &harness_some),
+            Some(1)
+        );
+    }
+}

kani-driver/src/call_cbmc_viewer.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use anyhow::Result;
+use kani_metadata::HarnessMetadata;
 use std::ffi::OsString;
 use std::path::Path;
 use std::process::Command;
@@ -12,7 +13,12 @@ use crate::util::alter_extension;
 impl KaniSession {
     /// Run CBMC appropriately to produce 3 output XML files, then run cbmc-viewer on them to produce a report.
     /// Viewer doesn't give different error codes depending on verification failure, so as long as it works, we report success.
-    pub fn run_visualize(&self, file: &Path, report_dir: &Path) -> Result<()> {
+    pub fn run_visualize(
+        &self,
+        file: &Path,
+        report_dir: &Path,
+        harness_metadata: &HarnessMetadata,
+    ) -> Result<()> {
         let results_filename = alter_extension(file, "results.xml");
         let coverage_filename = alter_extension(file, "coverage.xml");
         let property_filename = alter_extension(file, "property.xml");
@@ -24,9 +30,19 @@ impl KaniSession {
             temps.push(property_filename.clone());
         }
 
-        self.cbmc_variant(file, &["--xml-ui", "--trace"], &results_filename)?;
-        self.cbmc_variant(file, &["--xml-ui", "--cover", "location"], &coverage_filename)?;
-        self.cbmc_variant(file, &["--xml-ui", "--show-properties"], &property_filename)?;
+        self.cbmc_variant(file, &["--xml-ui", "--trace"], &results_filename, harness_metadata)?;
+        self.cbmc_variant(
+            file,
+            &["--xml-ui", "--cover", "location"],
+            &coverage_filename,
+            harness_metadata,
+        )?;
+        self.cbmc_variant(
+            file,
+            &["--xml-ui", "--show-properties"],
+            &property_filename,
+            harness_metadata,
+        )?;
 
         let args: Vec<OsString> = vec![
             "--result".into(),
@@ -59,8 +75,14 @@ impl KaniSession {
         Ok(())
     }
 
-    fn cbmc_variant(&self, file: &Path, extra_args: &[&str], output: &Path) -> Result<()> {
-        let mut args = self.cbmc_flags(file)?;
+    fn cbmc_variant(
+        &self,
+        file: &Path,
+        extra_args: &[&str],
+        output: &Path,
+        harness: &HarnessMetadata,
+    ) -> Result<()> {
+        let mut args = self.cbmc_flags(file, harness)?;
         args.extend(extra_args.iter().map(|x| x.into()));
 
         // TODO fix this hack, abstractions are wrong