From a160eed99a2c4a88b43d768c50cc7ff0b44b9aaa Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 16 Feb 2023 02:14:47 +0000 Subject: [PATCH 01/14] Generate unit test, line by line --- kani-driver/Cargo.toml | 1 + kani-driver/src/concrete_playback.rs | 234 +++++++++++++++++---------- 2 files changed, 150 insertions(+), 85 deletions(-) diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index b9f01738d000..79942e3b4788 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -38,6 +38,7 @@ tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_de tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} tracing-tree = "0.2.2" which = "4.4.0" +tempfile = "3.3.0" # A good set of suggested dependencies can be found in rustup: # https://github.com/rust-lang/rustup/blob/master/Cargo.toml diff --git a/kani-driver/src/concrete_playback.rs b/kani-driver/src/concrete_playback.rs index c146ebfc256a..f5dfbffd3065 100644 --- a/kani-driver/src/concrete_playback.rs +++ b/kani-driver/src/concrete_playback.rs @@ -14,9 +14,10 @@ use std::collections::hash_map::DefaultHasher; use std::ffi::OsString; use std::fs::{self, File}; use std::hash::{Hash, Hasher}; -use std::io::{Read, Write}; +use std::io::{BufRead, BufReader, BufWriter, Write}; use std::path::Path; use std::process::Command; +use tempfile; impl KaniSession { /// The main driver for generating concrete playback unit tests and adding them to source code. @@ -39,30 +40,31 @@ impl KaniSession { ), Some(concrete_vals) => { let pretty_name = harness.get_harness_name_unqualified(); - let concrete_playback = format_unit_test(&pretty_name, &concrete_vals); + let generated_unit_test = format_unit_test(&pretty_name, &concrete_vals); match playback_mode { ConcretePlaybackMode::Print => { println!( "Concrete playback unit test for `{}`:\n```\n{}\n```", - &harness.pretty_name, &concrete_playback.unit_test_str + &harness.pretty_name, + &generated_unit_test.code.join("\n") ); println!( "INFO: To automatically add the concrete playback unit test `{}` to the \ src code, run Kani with `--concrete-playback=inplace`.", - &concrete_playback.unit_test_name + &generated_unit_test.name ); } ConcretePlaybackMode::InPlace => { if !self.args.quiet { println!( "INFO: Now modifying the source code to include the concrete playback unit test `{}`.", - &concrete_playback.unit_test_name + &generated_unit_test.name ); } self.modify_src_code( &harness.original_file, harness.original_end_line, - &concrete_playback, + &generated_unit_test, ) .expect("Failed to modify source code"); } @@ -79,88 +81,79 @@ impl KaniSession { &self, src_path: &str, proof_harness_end_line: usize, - concrete_playback: &UnitTest, + unit_test: &UnitTest, ) -> Result<()> { - let mut src_file = File::open(src_path) - .with_context(|| format!("Couldn't open user's source code file `{src_path}`"))?; - let mut src_as_str = String::new(); - src_file.read_to_string(&mut src_as_str).with_context(|| { - format!("Couldn't read user's source code file `{src_path}` as a string") - })?; + let unit_test_already_in_src = + self.add_test_inplace(src_path, proof_harness_end_line, unit_test)?; - // Short circuit if unit test already in source code. - if src_as_str.contains(&concrete_playback.unit_test_name) { - if !self.args.quiet { - println!( - "Concrete playback unit test `{}/{}` already found in source code, so skipping modification.", - src_path, concrete_playback.unit_test_name, - ); - } + if unit_test_already_in_src { return Ok(()); } - // Split the code into two different parts around the insertion point. - let src_newline_matches: Vec<_> = src_as_str.match_indices('\n').collect(); - // If the proof harness ends on the last line of source code, there won't be a newline. - let insertion_pt = if proof_harness_end_line == src_newline_matches.len() + 1 { - src_as_str.len() - } else { - // Existing newline goes with 2nd src half. We also manually add newline before unit test. - src_newline_matches[proof_harness_end_line - 1].0 - }; - let src_before_concrete_playback = &src_as_str[..insertion_pt]; - let src_after_concrete_playback = &src_as_str[insertion_pt..]; - - // Write new source lines to a tmp file, and then rename it to the actual user's source file. - // Renames are usually automic, so we won't corrupt the user's source file during a crash. - let tmp_src_path = src_path.to_string() + ".concrete_playback_overwrite"; - let mut tmp_src_file = File::create(&tmp_src_path) - .with_context(|| format!("Couldn't create tmp source code file `{tmp_src_path}`"))?; - write!( - tmp_src_file, - "{}\n{}{}", - src_before_concrete_playback, - concrete_playback.unit_test_str, - src_after_concrete_playback - ) - .with_context(|| { - format!("Couldn't write new src str into tmp src file `{tmp_src_path}`") - })?; - fs::rename(&tmp_src_path, src_path).with_context(|| { - format!("Couldn't rename tmp src file `{tmp_src_path}` to actual src file `{src_path}`") - })?; - // Run rustfmt on just the inserted lines. - let source_path = Path::new(src_path); - let parent_dir_as_path = source_path.parent().with_context(|| { - format!("Expected source file `{}` to be in a directory", source_path.display()) - })?; - let parent_dir_as_str = parent_dir_as_path.to_str().with_context(|| { - format!( - "Couldn't convert source file parent directory `{}` from str", - parent_dir_as_path.display() - ) - })?; - let src_file_name_as_osstr = source_path.file_name().with_context(|| { - format!("Couldn't get the file name from the source file `{}`", source_path.display()) - })?; - let src_file_name_as_str = src_file_name_as_osstr.to_str().with_context(|| { - format!( - "Couldn't convert source code file name `{src_file_name_as_osstr:?}` from OsStr to str" - ) - })?; - - let concrete_playback_num_lines = concrete_playback.unit_test_str.matches('\n').count() + 1; + let concrete_playback_num_lines = unit_test.code.len(); let unit_test_start_line = proof_harness_end_line + 1; let unit_test_end_line = unit_test_start_line + concrete_playback_num_lines - 1; + let src_path = Path::new(src_path); + let (path, file_name) = extract_parent_dir_and_src_file(src_path)?; let file_line_ranges = vec![FileLineRange { - file: src_file_name_as_str.to_string(), + file: file_name, line_range: Some((unit_test_start_line, unit_test_end_line)), }]; - self.run_rustfmt(&file_line_ranges, Some(parent_dir_as_str))?; + self.run_rustfmt(&file_line_ranges, Some(&path))?; Ok(()) } + /// Writes the new source code to a temporary file. Returns whether the unit test was already in the old source code. + fn add_test_inplace( + &self, + source_path: &str, + proof_harness_end_line: usize, + unit_test: &UnitTest, + ) -> Result { + let source_file = File::open(source_path)?; + let source_reader = BufReader::new(source_file); + let mut temp_file = tempfile::NamedTempFile::new()?; + let mut temp_writer = BufWriter::new(&mut temp_file); + let mut curr_line_num = 0; + + // Use a buffered reader/writer to generate the unit test line by line + for line in source_reader.lines().flatten() { + if line.contains(&unit_test.name) { + if !self.args.quiet { + println!( + "Concrete playback unit test `{}/{}` already found in source code, so skipping modification.", + source_path, unit_test.name, + ); + } + // temp file gets deleted automatically when function goes out of scope + return Ok(true); + } + curr_line_num += 1; + writeln!(temp_writer, "{}", line)?; + if curr_line_num == proof_harness_end_line { + for unit_test_line in unit_test.code.iter() { + curr_line_num += 1; + writeln!(temp_writer, "{}", unit_test_line)?; + } + } + } + + // Flush before we remove/rename the file. + temp_writer.flush()?; + + // Have to drop the bufreader to be able to reuse and rename the moved temp file + drop(temp_writer); + + // Renames are usually automic, so we won't corrupt the user's source file during a crash. + fs::rename(temp_file.path(), source_path).with_context(|| { + format!("Couldn't rename tmp source file to actual src file `{source_path}`.") + })?; + + // temp file gets deleted automatically by the NamedTempFile handler + Ok(false) + } + /// Run rustfmt on the given src file, and optionally on only the specific lines. fn run_rustfmt( &self, @@ -207,6 +200,11 @@ impl KaniSession { } } +struct UnitTest { + code: Vec, + name: String, +} + /// Generate a formatted unit test from a list of concrete values. fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTest { // Hash the concrete values along with the proof harness name. @@ -235,8 +233,7 @@ fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTe .chain(func_after_concrete_vals) .collect(); - let full_func_code: String = full_func.join("\n"); - UnitTest { unit_test_str: full_func_code, unit_test_name: func_name } + UnitTest { code: full_func, name: func_name } } /// Format an initializer expression for a number of concrete values. @@ -256,16 +253,20 @@ fn format_concrete_vals(concrete_vals: &[ConcreteVal]) -> impl Iterator Result<(String, String)> { + let parent_dir_as_path = src_path.parent().unwrap(); + let parent_dir = parent_dir_as_path.to_string_lossy().to_string(); + let src_file_name_as_osstr = src_path.file_name(); + let src_file = src_file_name_as_osstr.unwrap().to_string_lossy().to_string(); + Ok((parent_dir, src_file)) +} + struct FileLineRange { file: String, line_range: Option<(usize, usize)>, } -struct UnitTest { - unit_test_str: String, - unit_test_name: String, -} - /// Extract concrete values from the CBMC output processed items. /// Note: we extract items that roughly look like the following: /// ```json @@ -379,6 +380,32 @@ mod tests { CheckStatus, Property, PropertyId, SourceLocation, TraceData, TraceItem, TraceValue, }; + /// util function for unit tests taht generates the rustfmt args used for formatting specific lines inside specific files. + /// note - adding this within the test mod because it gives a lint warning without it. + fn rustfmt_args(file_line_ranges: &[FileLineRange]) -> Vec { + let mut args: Vec = Vec::new(); + let mut line_range_dicts: Vec = Vec::new(); + for file_line_range in file_line_ranges { + if let Some((start_line, end_line)) = file_line_range.line_range { + let src_file = &file_line_range.file; + let line_range_dict = + format!("{{\"file\":\"{src_file}\",\"range\":[{start_line},{end_line}]}}"); + line_range_dicts.push(line_range_dict); + } + } + if !line_range_dicts.is_empty() { + // `--file-lines` arg is currently unstable. + args.push("--unstable-features".into()); + args.push("--file-lines".into()); + let line_range_dicts_combined = format!("[{}]", line_range_dicts.join(",")); + args.push(line_range_dicts_combined.into()); + } + for file_line_range in file_line_ranges { + args.push((&file_line_range.file).into()); + } + args + } + #[test] fn format_zero_concrete_vals() { let concrete_vals: [ConcreteVal; 0] = []; @@ -426,8 +453,8 @@ mod tests { let harness_name = "test_proof_harness"; let concrete_vals = [ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }]; let unit_test = format_unit_test(harness_name, &concrete_vals); - let full_func: Vec<&str> = unit_test.unit_test_str.split('\n').collect(); - let split_unit_test_name = split_unit_test_name(&unit_test.unit_test_name); + let full_func = unit_test.code; + let split_unit_test_name = split_unit_test_name(&unit_test.name); let expected_after_func_name = vec![ format!("{:<4}let concrete_vals: Vec> = vec![", " "), format!("{:<8}// 0", " "), @@ -442,14 +469,14 @@ mod tests { split_unit_test_name.before_hash, format!("kani_concrete_playback_{harness_name}") ); - assert_eq!(full_func[1], format!("fn {}() {{", unit_test.unit_test_name)); + assert_eq!(full_func[1], format!("fn {}() {{", unit_test.name)); assert_eq!(full_func[2..], expected_after_func_name); } /// Generates a unit test and returns its hash. fn extract_hash_from_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> String { let unit_test = format_unit_test(harness_name, concrete_vals); - split_unit_test_name(&unit_test.unit_test_name).hash + split_unit_test_name(&unit_test.name).hash } /// Two hashes should not be the same if either the harness_name or the concrete_vals changes. @@ -471,6 +498,43 @@ mod tests { assert_ne!(hash_base, hash_diff_interp_val); } + #[test] + fn check_rustfmt_args_no_line_ranges() { + let file_line_ranges = [FileLineRange { file: "file1".to_string(), line_range: None }]; + let args = rustfmt_args(&file_line_ranges); + let expected: Vec = vec!["file1".into()]; + assert_eq!(args, expected); + } + + #[test] + fn check_rustfmt_args_some_line_ranges() { + let file_line_ranges = [ + FileLineRange { file: "file1".to_string(), line_range: None }, + FileLineRange { file: "path/to/file2".to_string(), line_range: Some((1, 3)) }, + ]; + let args = rustfmt_args(&file_line_ranges); + let expected: Vec = [ + "--unstable-features", + "--file-lines", + "[{\"file\":\"path/to/file2\",\"range\":[1,3]}]", + "file1", + "path/to/file2", + ] + .into_iter() + .map(|arg| arg.into()) + .collect(); + assert_eq!(args, expected); + } + + #[test] + fn check_extract_parent_dir_and_src_file() { + let src_path = "/path/to/file.txt"; + let src_path = Path::new(src_path); + let (path, file_name) = extract_parent_dir_and_src_file(src_path).unwrap(); + assert_eq!(path, "/path/to"); + assert_eq!(file_name, "file.txt"); + } + /// Test util functions which extract the counter example values from a property. #[test] fn check_concrete_vals_extractor() { From 01689176f5c92f4250fc1aed80e6647c7f58a18d Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 16 Feb 2023 02:18:01 +0000 Subject: [PATCH 02/14] clippy changes --- kani-driver/src/concrete_playback.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/kani-driver/src/concrete_playback.rs b/kani-driver/src/concrete_playback.rs index f5dfbffd3065..a067cbc4535d 100644 --- a/kani-driver/src/concrete_playback.rs +++ b/kani-driver/src/concrete_playback.rs @@ -17,7 +17,7 @@ use std::hash::{Hash, Hasher}; use std::io::{BufRead, BufReader, BufWriter, Write}; use std::path::Path; use std::process::Command; -use tempfile; +use tempfile::NamedTempFile; impl KaniSession { /// The main driver for generating concrete playback unit tests and adding them to source code. @@ -113,7 +113,7 @@ impl KaniSession { ) -> Result { let source_file = File::open(source_path)?; let source_reader = BufReader::new(source_file); - let mut temp_file = tempfile::NamedTempFile::new()?; + let mut temp_file = NamedTempFile::new()?; let mut temp_writer = BufWriter::new(&mut temp_file); let mut curr_line_num = 0; @@ -130,11 +130,11 @@ impl KaniSession { return Ok(true); } curr_line_num += 1; - writeln!(temp_writer, "{}", line)?; + writeln!(temp_writer, "{line}")?; if curr_line_num == proof_harness_end_line { for unit_test_line in unit_test.code.iter() { curr_line_num += 1; - writeln!(temp_writer, "{}", unit_test_line)?; + writeln!(temp_writer, "{unit_test_line}")?; } } } From 964c22e5b2bd098a1ec090b1adf22f67d56f3fc4 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 16 Feb 2023 02:19:55 +0000 Subject: [PATCH 03/14] add tempfile dependency --- Cargo.lock | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/Cargo.lock b/Cargo.lock index 99c954cb1c6d..6e1eb9cccad9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -348,6 +348,15 @@ dependencies = [ "libc", ] +[[package]] +name = "fastrand" +version = "1.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e51093e27b0797c359783294ca4f0a911c270184cb10f85783b118614a1501be" +dependencies = [ + "instant", +] + [[package]] name = "getopts" version = "0.2.21" @@ -447,6 +456,15 @@ dependencies = [ "hashbrown 0.12.3", ] +[[package]] +name = "instant" +version = "0.1.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7a5bbe824c507c5da5956355e86a746d82e0e1464f65d862cc5e71da70e94b2c" +dependencies = [ + "cfg-if", +] + [[package]] name = "io-lifetimes" version = "1.0.5" @@ -531,6 +549,7 @@ dependencies = [ "serde_json", "strum", "strum_macros", + "tempfile", "toml", "tracing", "tracing-subscriber", @@ -949,6 +968,15 @@ version = "0.6.28" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "456c603be3e8d448b072f410900c09faf164fbce2d480456f50eea6e25f9c848" +[[package]] +name = "remove_dir_all" +version = "0.5.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3acd125665422973a33ac9d3dd2df85edad0f4ae9b00dafb1a05e43a9f5ef8e7" +dependencies = [ + "winapi", +] + [[package]] name = "rustc-demangle" version = "0.1.21" @@ -1179,6 +1207,20 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "tempfile" +version = "3.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5cdb1ef4eaeeaddc8fbd371e5017057064af0911902ef36b39801f67cc6d79e4" +dependencies = [ + "cfg-if", + "fastrand", + "libc", + "redox_syscall", + "remove_dir_all", + "winapi", +] + [[package]] name = "termcolor" version = "1.2.0" From d51294e8f8c9d820525bed9701e2fb951310e0cc Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 6 Apr 2023 00:14:36 +0000 Subject: [PATCH 04/14] Add concrete_playback feature to kani_macros --- library/kani/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 3 +++ library/kani_macros/src/lib.rs | 20 ++++++++++---------- 3 files changed, 14 insertions(+), 11 deletions(-) diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 6f699da31681..fa30d21ae9af 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -12,4 +12,4 @@ publish = false kani_macros = { path = "../kani_macros" } [features] -concrete_playback = [] +concrete_playback = ["kani_macros/concrete_playback"] diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 24570002f90b..04df9ab50151 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -16,3 +16,6 @@ proc-macro2 = "1.0" proc-macro-error = "1.0.4" quote = "1.0.20" syn = { version = "1.0.98", features = ["full"] } + +[features] +concrete_playback = [] diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 27a811a7bd3a..c0108d06c530 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -19,7 +19,7 @@ use { syn::{parse_macro_input, ItemFn}, }; -#[cfg(not(kani))] +#[cfg(any(not(kani), feature = "concrete_playback"))] #[proc_macro_attribute] pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream { // Leave the code intact, so it can be easily be edited in an IDE, @@ -38,7 +38,7 @@ pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream { /// Marks a Kani proof harness /// /// For async harnesses, this will call [`kani::block_on`] (see its documentation for more information). -#[cfg(kani)] +#[cfg(all(kani, not(feature = "concrete_playback")))] #[proc_macro_attribute] pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { let fn_item = parse_macro_input!(item as ItemFn); @@ -98,14 +98,14 @@ pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { } } -#[cfg(not(kani))] +#[cfg(any(not(kani), feature = "concrete_playback"))] #[proc_macro_attribute] pub fn should_panic(_attr: TokenStream, item: TokenStream) -> TokenStream { // No-op in non-kani mode item } -#[cfg(kani)] +#[cfg(all(kani, not(feature = "concrete_playback")))] #[proc_macro_attribute] pub fn should_panic(attr: TokenStream, item: TokenStream) -> TokenStream { assert!(attr.is_empty(), "`#[kani::should_panic]` does not take any arguments currently"); @@ -117,7 +117,7 @@ pub fn should_panic(attr: TokenStream, item: TokenStream) -> TokenStream { result } -#[cfg(not(kani))] +#[cfg(any(not(kani), feature = "concrete_playback"))] #[proc_macro_attribute] pub fn unwind(_attr: TokenStream, item: TokenStream) -> TokenStream { // When the config is not kani, we should leave the function alone @@ -127,7 +127,7 @@ pub fn unwind(_attr: TokenStream, item: TokenStream) -> TokenStream { /// Set Loop unwind limit for proof harnesses /// The attribute '#[kani::unwind(arg)]' can only be called alongside '#[kani::proof]'. /// arg - Takes in a integer value (u32) that represents the unwind value for the harness. -#[cfg(kani)] +#[cfg(all(kani, not(feature = "concrete_playback")))] #[proc_macro_attribute] pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream { let mut result = TokenStream::new(); @@ -140,7 +140,7 @@ pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream { result } -#[cfg(not(kani))] +#[cfg(any(not(kani), feature = "concrete_playback"))] #[proc_macro_attribute] pub fn stub(_attr: TokenStream, item: TokenStream) -> TokenStream { // When the config is not kani, we should leave the function alone @@ -154,7 +154,7 @@ pub fn stub(_attr: TokenStream, item: TokenStream) -> TokenStream { /// # Arguments /// * `original` - The function or method to replace, specified as a path. /// * `replacement` - The function or method to use as a replacement, specified as a path. -#[cfg(kani)] +#[cfg(all(kani, not(feature = "concrete_playback")))] #[proc_macro_attribute] pub fn stub(attr: TokenStream, item: TokenStream) -> TokenStream { let mut result = TokenStream::new(); @@ -167,7 +167,7 @@ pub fn stub(attr: TokenStream, item: TokenStream) -> TokenStream { result } -#[cfg(not(kani))] +#[cfg(any(not(kani), feature = "concrete_playback"))] #[proc_macro_attribute] pub fn solver(_attr: TokenStream, item: TokenStream) -> TokenStream { // No-op in non-kani mode @@ -178,7 +178,7 @@ pub fn solver(_attr: TokenStream, item: TokenStream) -> TokenStream { /// The attribute `#[kani::solver(arg)]` can only be used alongside `#[kani::proof]`` /// /// arg - name of solver, e.g. kissat -#[cfg(kani)] +#[cfg(all(kani, not(feature = "concrete_playback")))] #[proc_macro_attribute] pub fn solver(attr: TokenStream, item: TokenStream) -> TokenStream { let mut result = TokenStream::new(); From 6c59f18268fa2fd82773efab47fb22a530a9fb99 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 6 Apr 2023 06:56:09 +0000 Subject: [PATCH 05/14] Add regression test --- .../concrete_playback_test/bin/Cargo.toml | 11 ++++ .../concrete_playback_test/bin/src/main.rs | 26 +++++++++ .../concrete_playback_test.expected | 1 + .../concrete_playback_test.sh | 54 +++++++++++++++++++ .../concrete_playback_test/config.yml | 4 ++ 5 files changed, 96 insertions(+) create mode 100644 tests/script-based-pre/concrete_playback_test/bin/Cargo.toml create mode 100644 tests/script-based-pre/concrete_playback_test/bin/src/main.rs create mode 100644 tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected create mode 100755 tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh create mode 100644 tests/script-based-pre/concrete_playback_test/config.yml diff --git a/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml b/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml new file mode 100644 index 000000000000..c280801e21e2 --- /dev/null +++ b/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "bin" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] + +[dev-dependencies] +kani = { path = "../../../../library/kani", features = ["concrete_playback"] } diff --git a/tests/script-based-pre/concrete_playback_test/bin/src/main.rs b/tests/script-based-pre/concrete_playback_test/bin/src/main.rs new file mode 100644 index 000000000000..e7663f041880 --- /dev/null +++ b/tests/script-based-pre/concrete_playback_test/bin/src/main.rs @@ -0,0 +1,26 @@ +fn main() {} + +#[cfg(kani)] +mod harnesses { + #[kani::proof] + fn harness() { + let result_1: Result = kani::any(); + let result_2: Result = kani::any(); + assert!(!(result_1 == Ok(101) && result_2 == Err(102))); + } + + #[test] + fn kani_concrete_playback_harness_15598097466099501582() { + let concrete_vals: Vec> = vec![ + // 1 + vec![1], + // 101 + vec![101], + // 0 + vec![0], + // 102 + vec![102], + ]; + kani::concrete_playback_run(concrete_vals, harness); + } +} diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected new file mode 100644 index 000000000000..ef55eb4ce828 --- /dev/null +++ b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected @@ -0,0 +1 @@ +Tests failed as expected diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh new file mode 100755 index 000000000000..1416e72c97e1 --- /dev/null +++ b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh @@ -0,0 +1,54 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set +e + +OUT_DIR=bin/target + +echo +echo "Starting output file check..." +echo + + +# Check if cargo is installed +if ! command -v cargo &> /dev/null; then + echo "cargo command not found. Please install Rust and Cargo." + exit 1 +fi + +# Check if the directory containing cargo is in the PATH environment variable +if ! echo "$PATH" | grep -q "$(dirname "$(command -v cargo)")"; then + echo "Directory containing cargo is not in PATH. Adding directory to PATH..." + echo "export PATH=$PATH:$(dirname "$(command -v cargo)")" >> ~/.bashrc + source ~/.bashrc +fi + +echo "Running cargo test on the unit test ..." +echo + +rm -f test_output.log + +cd bin/ + +# Run cargo test on the unit test +RUSTFLAGS="--cfg=kani" cargo +nightly test 2>/dev/null > test_output.log + +echo "Checking content" +echo + +# Check if the test failed +if grep -q "test result: FAILED" test_output.log; then + echo "Tests failed as expected" +else + echo "Tests passed" +fi + +rm -f test_output.log + +cd .. + +# Try to leave a clean output folder at the end +rm -rf ${OUT_DIR} + +set -eu diff --git a/tests/script-based-pre/concrete_playback_test/config.yml b/tests/script-based-pre/concrete_playback_test/config.yml new file mode 100644 index 000000000000..9c4e0fbd6494 --- /dev/null +++ b/tests/script-based-pre/concrete_playback_test/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: concrete_playback_test.sh +expected: concrete_playback_test.expected From bc3671a6f2c64c4d37210f7fe23ad4d8cc14bae0 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 6 Apr 2023 07:12:22 +0000 Subject: [PATCH 06/14] Delete accidental changes --- Cargo.lock | 43 +--------------------------- kani-driver/Cargo.toml | 1 - kani-driver/src/concrete_playback.rs | 6 ---- 3 files changed, 1 insertion(+), 49 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 8a609c8f5ab2..ac97fb956a43 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -410,15 +410,6 @@ dependencies = [ "libc", ] -[[package]] -name = "fastrand" -version = "1.9.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e51093e27b0797c359783294ca4f0a911c270184cb10f85783b118614a1501be" -dependencies = [ - "instant", -] - [[package]] name = "getopts" version = "0.2.21" @@ -518,15 +509,6 @@ dependencies = [ "hashbrown 0.12.3", ] -[[package]] -name = "instant" -version = "0.1.12" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a5bbe824c507c5da5956355e86a746d82e0e1464f65d862cc5e71da70e94b2c" -dependencies = [ - "cfg-if", -] - [[package]] name = "io-lifetimes" version = "1.0.10" @@ -622,7 +604,6 @@ dependencies = [ "serde_json", "strum", "strum_macros", - "tempfile", "toml", "tracing", "tracing-subscriber", @@ -905,7 +886,7 @@ checksum = "9069cbb9f99e3a5083476ccb29ceb1de18b9118cafa53e90c9551235de2b9521" dependencies = [ "cfg-if", "libc", - "redox_syscall 0.2.16", + "redox_syscall", "smallvec", "windows-sys 0.45.0", ] @@ -1042,15 +1023,6 @@ dependencies = [ "bitflags", ] -[[package]] -name = "redox_syscall" -version = "0.3.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "567664f262709473930a4bf9e51bf2ebf3348f2e748ccc50dea20646858f8f29" -dependencies = [ - "bitflags", -] - [[package]] name = "regex" version = "1.7.3" @@ -1318,19 +1290,6 @@ dependencies = [ "unicode-ident", ] -[[package]] -name = "tempfile" -version = "3.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b9fbec84f381d5795b08656e4912bec604d162bff9291d6189a78f4c8ab87998" -dependencies = [ - "cfg-if", - "fastrand", - "redox_syscall 0.3.5", - "rustix", - "windows-sys 0.45.0", -] - [[package]] name = "thiserror" version = "1.0.40" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 291035121fef..caa14c813282 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -39,7 +39,6 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt" tracing-tree = "0.2.2" rand = "0.8" which = "4.4.0" -tempfile = "3.3.0" # A good set of suggested dependencies can be found in rustup: # https://github.com/rust-lang/rustup/blob/master/Cargo.toml diff --git a/kani-driver/src/concrete_playback.rs b/kani-driver/src/concrete_playback.rs index b06c00790f56..66971603c7b7 100644 --- a/kani-driver/src/concrete_playback.rs +++ b/kani-driver/src/concrete_playback.rs @@ -18,7 +18,6 @@ use std::hash::{Hash, Hasher}; use std::io::{BufRead, BufReader, Write}; use std::path::Path; use std::process::Command; -use tempfile::NamedTempFile; impl KaniSession { /// The main driver for generating concrete playback unit tests and adding them to source code. @@ -198,11 +197,6 @@ impl KaniSession { } } -struct UnitTest { - code: Vec, - name: String, -} - /// Generate a formatted unit test from a list of concrete values. fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTest { // Hash the concrete values along with the proof harness name. From 4ae20a333045e765ebfeb53375d702b5c8f42fee Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 6 Apr 2023 07:22:14 +0000 Subject: [PATCH 07/14] Add copyright strings --- tests/script-based-pre/concrete_playback_test/bin/Cargo.toml | 2 ++ tests/script-based-pre/concrete_playback_test/bin/src/main.rs | 3 +++ 2 files changed, 5 insertions(+) diff --git a/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml b/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml index c280801e21e2..c1358e9443c1 100644 --- a/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml +++ b/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml @@ -1,3 +1,5 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT [package] name = "bin" version = "0.1.0" diff --git a/tests/script-based-pre/concrete_playback_test/bin/src/main.rs b/tests/script-based-pre/concrete_playback_test/bin/src/main.rs index e7663f041880..7052cbe78a1b 100644 --- a/tests/script-based-pre/concrete_playback_test/bin/src/main.rs +++ b/tests/script-based-pre/concrete_playback_test/bin/src/main.rs @@ -1,3 +1,6 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + fn main() {} #[cfg(kani)] From 3429b9e5a05fc4fee4256d918afd684f1613805f Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 6 Apr 2023 08:10:45 +0000 Subject: [PATCH 08/14] Fix cargo.toml --- tests/script-based-pre/concrete_playback_test/bin/Cargo.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml b/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml index c1358e9443c1..1b330c2e7f03 100644 --- a/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml +++ b/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml @@ -1,5 +1,5 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT [package] name = "bin" version = "0.1.0" From c728dc3dbf262b15698575588e9d6f55ca54a862 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 6 Apr 2023 15:01:01 +0000 Subject: [PATCH 09/14] Remove logging in CI test --- .../concrete_playback_test.expected | 18 +++++++++++++++++- .../concrete_playback_test.sh | 18 ++---------------- 2 files changed, 19 insertions(+), 17 deletions(-) diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected index ef55eb4ce828..910b5f8cd2d7 100644 --- a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected +++ b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected @@ -1 +1,17 @@ -Tests failed as expected + +running 1 test +test harnesses::kani_concrete_playback_harness_15598097466099501582 ... FAILED + +failures: + +---- harnesses::kani_concrete_playback_harness_15598097466099501582 stdout ---- +thread 'harnesses::kani_concrete_playback_harness_15598097466099501582' panicked at 'assertion failed: !(result_1 == Ok(101) && result_2 == Err(102))', src/main.rs:12:9 +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + + +failures: + harnesses::kani_concrete_playback_harness_15598097466099501582 + +test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s + +error: test failed, to rerun pass `--bin bin` diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh index 1416e72c97e1..4fcc77870d3b 100755 --- a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh +++ b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh @@ -27,28 +27,14 @@ fi echo "Running cargo test on the unit test ..." echo -rm -f test_output.log - cd bin/ # Run cargo test on the unit test -RUSTFLAGS="--cfg=kani" cargo +nightly test 2>/dev/null > test_output.log - -echo "Checking content" -echo - -# Check if the test failed -if grep -q "test result: FAILED" test_output.log; then - echo "Tests failed as expected" -else - echo "Tests passed" -fi - -rm -f test_output.log +RUSTFLAGS="--cfg=kani" cargo +nightly test cd .. # Try to leave a clean output folder at the end rm -rf ${OUT_DIR} -set -eu +set -e From d1ddd11887816fcfc1f2d16fd9812dd9ebba199e Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 6 Apr 2023 15:37:39 +0000 Subject: [PATCH 10/14] Add nightly from toolchain file --- .../concrete_playback_test/concrete_playback_test.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh index 4fcc77870d3b..800585d989c9 100755 --- a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh +++ b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh @@ -29,8 +29,11 @@ echo cd bin/ +output=$(grep 'channel = ' ../../../../rust-toolchain.toml | cut -d '"' -f 2) +echo "$output" + # Run cargo test on the unit test -RUSTFLAGS="--cfg=kani" cargo +nightly test +RUSTFLAGS="--cfg=kani" cargo +${output} test cd .. From f43e284099fa85b4fb0bd8c6d4e5c57bd54ed626 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 6 Apr 2023 15:58:28 +0000 Subject: [PATCH 11/14] Fix diff error in CI --- .../concrete_playback_test.expected | 11 ----------- .../concrete_playback_test/concrete_playback_test.sh | 3 ++- 2 files changed, 2 insertions(+), 12 deletions(-) diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected index 910b5f8cd2d7..54e9e8a12ed6 100644 --- a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected +++ b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected @@ -1,14 +1,3 @@ - -running 1 test -test harnesses::kani_concrete_playback_harness_15598097466099501582 ... FAILED - -failures: - ----- harnesses::kani_concrete_playback_harness_15598097466099501582 stdout ---- -thread 'harnesses::kani_concrete_playback_harness_15598097466099501582' panicked at 'assertion failed: !(result_1 == Ok(101) && result_2 == Err(102))', src/main.rs:12:9 -note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace - - failures: harnesses::kani_concrete_playback_harness_15598097466099501582 diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh index 800585d989c9..bec3d2943d6e 100755 --- a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh +++ b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh @@ -33,7 +33,8 @@ output=$(grep 'channel = ' ../../../../rust-toolchain.toml | cut -d '"' -f 2) echo "$output" # Run cargo test on the unit test -RUSTFLAGS="--cfg=kani" cargo +${output} test +cargo_output=$(RUSTFLAGS="--cfg=kani" cargo +${output} test) +echo "$cargo_output" cd .. From c111570d0ebad08807f147f0631b70f088cfa10d Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 6 Apr 2023 16:09:08 +0000 Subject: [PATCH 12/14] Remove time from expected --- .../concrete_playback_test/concrete_playback_test.expected | 4 +--- .../concrete_playback_test/concrete_playback_test.sh | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected index 54e9e8a12ed6..042d881412c2 100644 --- a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected +++ b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected @@ -1,6 +1,4 @@ failures: harnesses::kani_concrete_playback_harness_15598097466099501582 -test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s - -error: test failed, to rerun pass `--bin bin` +test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh index bec3d2943d6e..6a6e9274a532 100755 --- a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh +++ b/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh @@ -33,7 +33,7 @@ output=$(grep 'channel = ' ../../../../rust-toolchain.toml | cut -d '"' -f 2) echo "$output" # Run cargo test on the unit test -cargo_output=$(RUSTFLAGS="--cfg=kani" cargo +${output} test) +cargo_output=$(RUSTFLAGS="--cfg=kani" cargo +${output} test 2>/dev/null) echo "$cargo_output" cd .. From 223b9a82ad8962bbc68f4ab48c3807010d5770a6 Mon Sep 17 00:00:00 2001 From: jaisnan Date: Thu, 6 Apr 2023 20:47:12 +0000 Subject: [PATCH 13/14] Address comments --- .../concrete_playback_test/config.yml | 4 ---- .../playback_with_cfg_kani/config.yml | 4 ++++ .../playback_with_cfg_kani.expected} | 0 .../playback_with_cfg_kani.sh} | 16 +++------------- .../sample_crate}/Cargo.toml | 2 +- .../sample_crate}/src/main.rs | 5 +++++ 6 files changed, 13 insertions(+), 18 deletions(-) delete mode 100644 tests/script-based-pre/concrete_playback_test/config.yml create mode 100644 tests/script-based-pre/playback_with_cfg_kani/config.yml rename tests/script-based-pre/{concrete_playback_test/concrete_playback_test.expected => playback_with_cfg_kani/playback_with_cfg_kani.expected} (100%) rename tests/script-based-pre/{concrete_playback_test/concrete_playback_test.sh => playback_with_cfg_kani/playback_with_cfg_kani.sh} (55%) rename tests/script-based-pre/{concrete_playback_test/bin => playback_with_cfg_kani/sample_crate}/Cargo.toml (93%) rename tests/script-based-pre/{concrete_playback_test/bin => playback_with_cfg_kani/sample_crate}/src/main.rs (64%) diff --git a/tests/script-based-pre/concrete_playback_test/config.yml b/tests/script-based-pre/concrete_playback_test/config.yml deleted file mode 100644 index 9c4e0fbd6494..000000000000 --- a/tests/script-based-pre/concrete_playback_test/config.yml +++ /dev/null @@ -1,4 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -script: concrete_playback_test.sh -expected: concrete_playback_test.expected diff --git a/tests/script-based-pre/playback_with_cfg_kani/config.yml b/tests/script-based-pre/playback_with_cfg_kani/config.yml new file mode 100644 index 000000000000..a487f834d1e7 --- /dev/null +++ b/tests/script-based-pre/playback_with_cfg_kani/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: playback_with_cfg_kani.sh +expected: playback_with_cfg_kani.expected diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected b/tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.expected similarity index 100% rename from tests/script-based-pre/concrete_playback_test/concrete_playback_test.expected rename to tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.expected diff --git a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh b/tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.sh similarity index 55% rename from tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh rename to tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.sh index 6a6e9274a532..fd2eeec37e38 100755 --- a/tests/script-based-pre/concrete_playback_test/concrete_playback_test.sh +++ b/tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.sh @@ -4,7 +4,7 @@ set +e -OUT_DIR=bin/target +OUT_DIR=sample_crate/target echo echo "Starting output file check..." @@ -17,28 +17,18 @@ if ! command -v cargo &> /dev/null; then exit 1 fi -# Check if the directory containing cargo is in the PATH environment variable -if ! echo "$PATH" | grep -q "$(dirname "$(command -v cargo)")"; then - echo "Directory containing cargo is not in PATH. Adding directory to PATH..." - echo "export PATH=$PATH:$(dirname "$(command -v cargo)")" >> ~/.bashrc - source ~/.bashrc -fi - echo "Running cargo test on the unit test ..." echo -cd bin/ +cd sample_crate/ output=$(grep 'channel = ' ../../../../rust-toolchain.toml | cut -d '"' -f 2) echo "$output" # Run cargo test on the unit test -cargo_output=$(RUSTFLAGS="--cfg=kani" cargo +${output} test 2>/dev/null) -echo "$cargo_output" +RUSTFLAGS="--cfg=kani" cargo +${output} test 2>/dev/null cd .. # Try to leave a clean output folder at the end rm -rf ${OUT_DIR} - -set -e diff --git a/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml b/tests/script-based-pre/playback_with_cfg_kani/sample_crate/Cargo.toml similarity index 93% rename from tests/script-based-pre/concrete_playback_test/bin/Cargo.toml rename to tests/script-based-pre/playback_with_cfg_kani/sample_crate/Cargo.toml index 1b330c2e7f03..053feb5be3b3 100644 --- a/tests/script-based-pre/concrete_playback_test/bin/Cargo.toml +++ b/tests/script-based-pre/playback_with_cfg_kani/sample_crate/Cargo.toml @@ -1,7 +1,7 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT [package] -name = "bin" +name = "sample_crate" version = "0.1.0" edition = "2021" diff --git a/tests/script-based-pre/concrete_playback_test/bin/src/main.rs b/tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs similarity index 64% rename from tests/script-based-pre/concrete_playback_test/bin/src/main.rs rename to tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs index 7052cbe78a1b..4c2506e2c41a 100644 --- a/tests/script-based-pre/concrete_playback_test/bin/src/main.rs +++ b/tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs @@ -1,6 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// This module contains a harness and it's associated unit test that is generated +// by running concrete-playback on it. There is an existing UI test to generate the unit test +// itself (in kani/tests/ui/concrete-playback/result). The current module runs `cargo test` on the unit test +// on the unit test and checks the output to test the rest of the concrete-playback flow. + fn main() {} #[cfg(kani)] From 1c5c5b72c4aa1a06232261acaf5787d66f86798b Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Thu, 6 Apr 2023 17:38:35 -0400 Subject: [PATCH 14/14] Update tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- .../playback_with_cfg_kani/sample_crate/src/main.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs b/tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs index 4c2506e2c41a..7d3dd90a9aac 100644 --- a/tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs +++ b/tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs @@ -1,10 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// This module contains a harness and it's associated unit test that is generated -// by running concrete-playback on it. There is an existing UI test to generate the unit test -// itself (in kani/tests/ui/concrete-playback/result). The current module runs `cargo test` on the unit test -// on the unit test and checks the output to test the rest of the concrete-playback flow. +// This test checks that running the unit test generated using the concrete playback feature +// with `RUSTFLAGS="--cfg=kani" cargo +nightly test doesn't cause a compilation error. +// There is an existing UI test to generate the unit test itself (in kani/tests/ui/concrete-playback/result). fn main() {}