Merge branch 'main' into docs-struct

src/cargo-kani/src/args_toml.rs

@@ -9,10 +9,54 @@ use std::process::Command;
 use toml::value::Table;
 use toml::Value;
 
-/// Produces a set of arguments to pass to ourself (cargo-kani) from a Cargo.toml project file
-pub fn config_toml_to_args() -> Result<Vec<OsString>> {
+/// Produce the list of arguments to pass to ourself (cargo-kani).
+///
+/// The arguments passed via command line have precedence over the ones from the Cargo.toml.
+pub fn join_args(input_args: Vec<OsString>) -> Result<Vec<OsString>> {
     let file = std::fs::read_to_string(cargo_locate_project()?)?;
-    toml_to_args(&file)
+    let (kani_args, cbmc_args) = toml_to_args(&file)?;
+    merge_args(input_args, kani_args, cbmc_args)
+}
+
+/// Join the arguments passed via command line with the ones found in the Cargo.toml.
+///
+/// The arguments passed via command line have precedence over the ones from the Cargo.toml. Thus,
+/// we need to inject the command line arguments after the ones read from Cargo.toml. This can be
+/// a bit annoying given that cbmc args have to be at the end of the arguments and the "--cbmc-args"
+/// flag must only be included once.
+///
+/// This function will return the arguments in the following order:
+/// ```
+/// <bin_name> [<cfg_kani_args>]* [<cmd_kani_args>]* [--cbmc-args [<cfg_cbmc_args>]* [<cmd_cbmc_args>]*]
+/// ```
+fn merge_args(
+    cmd_args: Vec<OsString>,
+    cfg_kani_args: Vec<OsString>,
+    cfg_cbmc_args: Vec<OsString>,
+) -> Result<Vec<OsString>> {
+    let mut merged_args =
+        vec![cmd_args.first().expect("Expected binary path as one argument").clone()];
+    merged_args.extend(cfg_kani_args);
+    if cfg_cbmc_args.is_empty() {
+        // No need to handle cbmc_args. Just merge the Cargo.toml args with the original input:
+        // [<config_kani_args>]* [input_args]*
+        merged_args.extend_from_slice(&cmd_args[1..]);
+    } else {
+        let cbmc_flag = cmd_args.iter().enumerate().find(|&f| f.1.eq("--cbmc-args".into()));
+        if let Some((idx, _)) = cbmc_flag {
+            // Both command line and config file have --cbmc-args. Merge them to be in order.
+            merged_args.extend_from_slice(&cmd_args[1..idx]);
+            merged_args.extend(cfg_cbmc_args);
+            // Remove --cbmc-args from the input.
+            merged_args.extend_from_slice(&cmd_args[idx + 1..]);
+        } else {
+            // Command line doesn't have --cbmc-args. Put command line arguments in the middle.
+            // [<cfg_kani_args>]* [<cmd_args>]* --cbmc-args [<cfg_cbmc_args>]+
+            merged_args.extend_from_slice(&cmd_args[1..]);
+            merged_args.extend(cfg_cbmc_args);
+        }
+    }
+    Ok(merged_args)
 }
 
 /// `locate-project` produces a response like: `/full/path/to/src/cargo-kani/Cargo.toml`
@@ -28,8 +72,9 @@ fn cargo_locate_project() -> Result<PathBuf> {
     Ok(path.trim().into())
 }
 
-/// Parse a config toml string and extract the cargo-kani arguments we should try injecting
-fn toml_to_args(tomldata: &str) -> Result<Vec<OsString>> {
+/// Parse a config toml string and extract the cargo-kani arguments we should try injecting.
+/// This returns two different vectors since all cbmc-args have to be at the end.
+fn toml_to_args(tomldata: &str) -> Result<(Vec<OsString>, Vec<OsString>)> {
     let config = tomldata.parse::<Value>()?;
     // To make testing easier, our function contract is to produce a stable ordering of flags for a given input.
     // Consequently, we use BTreeMap instead of HashMap here.
@@ -43,20 +88,18 @@ fn toml_to_args(tomldata: &str) -> Result<Vec<OsString>> {
     }
 
     let mut args = Vec::new();
-    let mut suffixed_args = Vec::new();
+    let mut cbmc_args = Vec::new();
 
     for (flag, value) in map {
         if flag == "cbmc-args" {
             // --cbmc-args has to come last because it eats all remaining arguments
-            insert_arg_from_toml(&flag, &value, &mut suffixed_args)?;
+            insert_arg_from_toml(&flag, &value, &mut cbmc_args)?;
         } else {
             insert_arg_from_toml(&flag, &value, &mut args)?;
         }
     }
 
-    args.extend(suffixed_args);
-
-    Ok(args)
+    Ok((args, cbmc_args))
 }
 
 /// Translates one toml entry (flag, value) into arguments and inserts it into `args`
@@ -113,6 +156,44 @@ mod tests {
         let b = toml_to_args(a).unwrap();
         // default first, then unwind thanks to btree ordering.
         // cbmc-args always last.
-        assert_eq!(b, vec!["--no-default-checks", "--unwind", "2", "--cbmc-args", "--fake"]);
+        assert_eq!(b.0, vec!["--no-default-checks", "--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"]
+                .iter()
+                .map(|&s| s.into())
+                .collect();
+        let merged = merge_args(cmd_args.clone(), Vec::new(), Vec::new()).unwrap();
+        assert_eq!(merged, cmd_args);
+    }
+
+    #[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();
+        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);
+    }
+
+    #[test]
+    fn check_merge_args_order() {
+        let cmd_args: Vec<OsString> =
+            vec!["kani".into(), "--debug".into(), "--cbmc-args".into(), "--fake".into()];
+        let cfg_kani_args: Vec<OsString> = vec!["--no-default-checks".into()];
+        let cfg_cbmc_args: Vec<OsString> = vec!["--cbmc-args".into(), "--trace".into()];
+        let merged =
+            merge_args(cmd_args.clone(), cfg_kani_args.clone(), cfg_cbmc_args.clone()).unwrap();
+        assert_eq!(merged.len(), cmd_args.len() + cfg_kani_args.len() + cfg_cbmc_args.len() - 1);
+        assert_eq!(merged[0], OsString::from("kani"));
+        assert_eq!(merged[1], OsString::from("--no-default-checks"));
+        assert_eq!(merged[2], OsString::from("--debug"));
+        assert_eq!(merged[3], OsString::from("--cbmc-args"));
+        assert_eq!(merged[4], OsString::from("--trace"));
+        assert_eq!(merged[5], OsString::from("--fake"));
     }
 }

src/cargo-kani/src/main.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use anyhow::Result;
-use args_toml::config_toml_to_args;
+use args_toml::join_args;
 use call_cbmc::VerificationStatus;
 use std::ffi::OsString;
 use std::path::PathBuf;
@@ -28,8 +28,8 @@ fn main() -> Result<()> {
     }
 }
 
-fn cargokani_main(mut input_args: Vec<OsString>) -> Result<()> {
-    input_args.extend(config_toml_to_args()?);
+fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
+    let input_args = join_args(input_args)?;
     let args = args::CargoKaniArgs::from_iter(input_args);
     args.validate();
     let ctx = session::KaniSession::new(args.common_opts)?;

tests/cargo-kani/simple-unwind-annotation/Cargo.toml

@@ -8,5 +8,6 @@ edition = "2021"
 
 [dependencies]
 
-[kani.flags]
-function = "harness"
+# Remove this once unwind has been hooked up
+[package.metadata.kani]
+flags = {function = "harness"}

tests/cargo-kani/simple-unwind-annotation/harness.expected

@@ -0,0 +1,2 @@
+FAILURE\
+assertion failed: counter < 10

tests/cargo-kani/simple-unwind-annotation/main.expected

@@ -1,2 +1 @@
-FAILURE\
-assertion failed: counter < 10
+Failed Checks: assertion failed: 1 == 2

tests/cargo-kani/simple-unwind-annotation/src/main.rs

@@ -1,12 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
-// kani-flags: --function harness
-
-// The expected file presently looks for "1 == 2" above.
-// But eventually this test may start to fail as we might stop regarding 'main'
-// as a valid proof harness, since it isn't annotated as such.
-// This test should be updated if we go that route.
+//
+// This harness should fail because unwind limit is too high.
 
 fn main() {
     assert!(1 == 2);