From 2a95fe23bbaeafcb79cba5f6386f6ea60d3a9768 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 26 Jul 2024 13:48:22 -0700 Subject: [PATCH 01/11] Add kind to harness metadata This allow us to get more information in the Kani driver about which kind of proof it is. For proof_for_contract, we can now check which function is the target. --- kani-compiler/src/kani_middle/attributes.rs | 45 ++++++++++--------- .../src/kani_middle/codegen_units.rs | 2 +- kani-compiler/src/kani_middle/metadata.rs | 4 +- kani-driver/src/metadata.rs | 16 ++++--- kani_metadata/src/harness.rs | 32 ++++++++++++- 5 files changed, 67 insertions(+), 32 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 9eb6d3d6ee4e..8c729bbdec9f 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -4,7 +4,7 @@ use std::collections::BTreeMap; -use kani_metadata::{CbmcSolver, HarnessAttributes, Stub}; +use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use rustc_ast::{ attr, token::Token, @@ -310,7 +310,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// the session and emit all errors found. pub(super) fn check_attributes(&self) { // Check that all attributes are correctly used and well formed. - let is_harness = self.is_harness(); + let is_harness = self.is_proof_harness(); for (&kind, attrs) in self.map.iter() { let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span, msg); @@ -454,7 +454,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// Is this item a harness? (either `proof` or `proof_for_contract` /// attribute are present) - fn is_harness(&self) -> bool { + fn is_proof_harness(&self) -> bool { self.map.contains_key(&KaniAttributeKind::Proof) || self.map.contains_key(&KaniAttributeKind::ProofForContract) } @@ -469,13 +469,18 @@ impl<'tcx> KaniAttributes<'tcx> { panic!("Expected a local item, but got: {:?}", self.item); }; trace!(?self, "extract_harness_attributes"); - assert!(self.is_harness()); - self.map.iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| { + assert!(self.is_proof_harness()); + let harness_attrs = if let Some(Ok(harness)) = self.proof_for_contract() { + HarnessAttributes::new(HarnessKind::ProofForContract { target_fn: harness.to_string() }) + } else { + HarnessAttributes::new(HarnessKind::Proof) + }; + self.map.iter().fold(harness_attrs, |mut harness, (kind, attributes)| { match kind { KaniAttributeKind::ShouldPanic => harness.should_panic = true, KaniAttributeKind::Recursion => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), "The attribute `kani::recursion` should only be used in combination with function contracts."); - }, + } KaniAttributeKind::Solver => { harness.solver = parse_solver(self.tcx, attributes[0]); } @@ -485,7 +490,7 @@ impl<'tcx> KaniAttributes<'tcx> { KaniAttributeKind::Unwind => { harness.unwind_value = parse_unwind(self.tcx, attributes[0]) } - KaniAttributeKind::Proof => harness.proof = true, + KaniAttributeKind::Proof => { /* no-op */ } KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness), KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness), KaniAttributeKind::Unstable => { @@ -498,7 +503,7 @@ impl<'tcx> KaniAttributes<'tcx> { | KaniAttributeKind::InnerCheck | KaniAttributeKind::ReplacedWith => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); - }, + } KaniAttributeKind::DisableChecks => { // Internal attribute which shouldn't exist here. unreachable!() @@ -552,14 +557,14 @@ impl<'tcx> KaniAttributes<'tcx> { self.item_name(), ), ) - .with_span_note( - self.tcx.def_span(def_id), - format!( - "Try adding a contract to this function or use the unsound `{}` attribute instead.", - KaniAttributeKind::Stub.as_ref(), + .with_span_note( + self.tcx.def_span(def_id), + format!( + "Try adding a contract to this function or use the unsound `{}` attribute instead.", + KaniAttributeKind::Stub.as_ref(), + ), ) - ) - .emit(); + .emit(); continue; } Some(Ok(replacement_name)) => replacement_name, @@ -689,7 +694,7 @@ fn has_kani_attribute bool>( tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate) } -/// Same as [`KaniAttributes::is_harness`] but more efficient because less +/// Same as [`KaniAttributes::is_proof_harness`] but more efficient because less /// attribute parsing is performed. pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool { let def_id = rustc_internal::internal(tcx, instance.def.def_id()); @@ -896,7 +901,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec { tcx.dcx().span_err( error_span, - "attribute `kani::stub` takes two path arguments; found argument that is not a path", + "attribute `kani::stub` takes two path arguments; found argument that is not a path", ); None } @@ -910,9 +915,9 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option { const ATTRIBUTE: &str = "#[kani::solver]"; let invalid_arg_err = |attr: &Attribute| { tcx.dcx().span_err( - attr.span, - format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"\"`)") - ) + attr.span, + format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"\"`)"), + ) }; let attr_args = attr.meta_item_list().unwrap(); diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 260b363a868a..3f88ad2ecd3b 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -104,7 +104,7 @@ impl CodegenUnits { /// Generate [KaniMetadata] for the target crate. fn generate_metadata(&self) -> KaniMetadata { let (proof_harnesses, test_harnesses) = - self.harness_info.values().cloned().partition(|md| md.attributes.proof); + self.harness_info.values().cloned().partition(|md| md.attributes.is_proof()); KaniMetadata { crate_name: self.crate_info.name.clone(), proof_harnesses, diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index c00f38be4cb0..2f0f22d49e1c 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -6,7 +6,7 @@ use std::path::Path; use crate::kani_middle::attributes::test_harness_name; -use kani_metadata::{ArtifactType, HarnessAttributes, HarnessMetadata}; +use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::CrateDef; @@ -61,7 +61,7 @@ pub fn gen_test_metadata( original_file: loc.filename, original_start_line: loc.start_line, original_end_line: loc.end_line, - attributes: HarnessAttributes::default(), + attributes: HarnessAttributes::new(HarnessKind::Test), // TODO: This no longer needs to be an Option. goto_file: Some(model_file), contract: Default::default(), diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index cd916358d92e..3f9cd8f2bf84 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -200,7 +200,7 @@ fn find_proof_harnesses<'a>( #[cfg(test)] pub mod tests { use super::*; - use kani_metadata::HarnessAttributes; + use kani_metadata::{HarnessAttributes, HarnessKind}; use std::path::PathBuf; pub fn mock_proof_harness( @@ -209,6 +209,8 @@ pub mod tests { krate: Option<&str>, model_file: Option, ) -> HarnessMetadata { + let mut attributes = HarnessAttributes::new(HarnessKind::Proof); + attributes.unwind_value = unwind_value; HarnessMetadata { pretty_name: name.into(), mangled_name: name.into(), @@ -216,7 +218,7 @@ pub mod tests { original_file: "".into(), original_start_line: 0, original_end_line: 0, - attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() }, + attributes, goto_file: model_file, contract: Default::default(), } @@ -236,7 +238,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_three".to_string()]), &ref_harnesses, - false + false, ) .len(), 1 @@ -245,7 +247,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_two".to_string()]), &ref_harnesses, - false + false, ) .first() .unwrap() @@ -256,7 +258,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_one".to_string()]), &ref_harnesses, - false + false, ) .first() .unwrap() @@ -280,7 +282,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"check_three".to_string()]), &ref_harnesses, - true + true, ) .is_empty() ); @@ -299,7 +301,7 @@ pub mod tests { find_proof_harnesses( &BTreeSet::from([&"module::not_check_three".to_string()]), &ref_harnesses, - true + true, ) .first() .unwrap() diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 3dd6c82ebd39..5ae16aae7a33 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -38,10 +38,10 @@ pub struct HarnessMetadata { } /// The attributes added by the user to control how a harness is executed. -#[derive(Debug, Clone, Serialize, Deserialize, Default, PartialEq)] +#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] pub struct HarnessAttributes { /// Whether the harness has been annotated with proof. - pub proof: bool, + pub kind: HarnessKind, /// Whether the harness is expected to panic or not. pub should_panic: bool, /// Optional data to store solver. @@ -52,6 +52,34 @@ pub struct HarnessAttributes { pub stubs: Vec, } +#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)] +pub enum HarnessKind { + /// Function was annotated with `#[kani::proof]`. + Proof, + /// Function was annotated with `#[kani::proof_for_contract(target_fn)]`. + ProofForContract { target_fn: String }, + /// This is a test harness annotated with `#[test]`. + Test, +} + +impl HarnessAttributes { + /// Create a new harness with of the provided kind. + pub fn new(kind: HarnessKind) -> HarnessAttributes { + HarnessAttributes { + kind, + should_panic: false, + solver: None, + unwind_value: None, + stubs: vec![], + } + } + + /// Return whether this is a proof harness. + pub fn is_proof(&self) -> bool { + matches!(self.kind, HarnessKind::Proof | HarnessKind::ProofForContract { .. }) + } +} + /// The stubbing type. #[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] pub struct Stub { From a060b801f55687124fd2638ba015b72ec7e6b693 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 26 Jul 2024 15:24:44 -0700 Subject: [PATCH 02/11] Enable concrete playback for stubs / contract --- kani-driver/src/args/mod.rs | 23 +++---- .../src/concrete_playback/test_generator.rs | 60 ++++++++++++++++--- 2 files changed, 60 insertions(+), 23 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index d043035bcab2..04f84821660f 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -137,10 +137,10 @@ pub struct VerificationArgs { /// If value supplied is 'inplace', Kani automatically adds the unit test to your source code. /// This option does not work with `--output-format old`. #[arg( - long, - conflicts_with_all(&["visualize"]), - ignore_case = true, - value_enum + long, + conflicts_with_all(& ["visualize"]), + ignore_case = true, + value_enum )] pub concrete_playback: Option, /// Keep temporary files generated throughout Kani process. This is already the default @@ -210,10 +210,10 @@ pub struct VerificationArgs { /// Pass through directly to CBMC; must be the last flag. /// This feature is unstable and it requires `--enable_unstable` to be used #[arg( - long, - allow_hyphen_values = true, - requires("enable_unstable"), - num_args(0..) + long, + allow_hyphen_values = true, + requires("enable_unstable"), + num_args(0..) )] // consumes everything pub cbmc_args: Vec, @@ -567,13 +567,6 @@ impl ValidateArgs for VerificationArgs { --output-format=old.", )); } - if self.concrete_playback.is_some() && self.is_stubbing_enabled() { - // Concrete playback currently does not work with contracts or stubbing. - return Err(Error::raw( - ErrorKind::ArgumentConflict, - "Conflicting options: --concrete-playback isn't compatible with stubbing.", - )); - } if self.concrete_playback.is_some() && self.jobs() != Some(1) { // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called. return Err(Error::raw( diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index dbd2fb9e03d2..62169d357579 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -9,7 +9,7 @@ use crate::call_cbmc::VerificationResult; use crate::session::KaniSession; use anyhow::{Context, Result}; use concrete_vals_extractor::{extract_harness_values, ConcreteVal}; -use kani_metadata::HarnessMetadata; +use kani_metadata::{HarnessKind, HarnessMetadata}; use std::collections::hash_map::DefaultHasher; use std::ffi::OsString; use std::fs::{read_to_string, File}; @@ -45,7 +45,7 @@ impl KaniSession { .iter() .map(|concrete_vals| { let pretty_name = harness.get_harness_name_unqualified(); - format_unit_test(&pretty_name, &concrete_vals) + format_unit_test(&pretty_name, &concrete_vals, gen_test_doc(harness)) }) .collect(); unit_tests.dedup_by(|a, b| a.name == b.name); @@ -231,8 +231,45 @@ impl KaniSession { } } +fn gen_test_doc(harness: &HarnessMetadata) -> String { + let mut doc_str = match &harness.attributes.kind { + HarnessKind::Proof => { + format!("/// Test generated for harness `{}` \n", harness.pretty_name) + } + HarnessKind::ProofForContract { target_fn } => { + format!( + "/// Test generated for harness `{}` that check contract for `{target_fn}`\n", + harness.pretty_name + ) + } + HarnessKind::Test => { + unreachable!("Concrete playback for tests is not supported") + } + }; + if !harness.attributes.stubs.is_empty() { + doc_str.push_str("///\n"); + doc_str.push_str( + "/// # Warning\n\ + ///\n\ + /// Concrete playback tests combined with stubs is highly experimental, and\n\ + /// subject to change.\n\ + ///\n\ + /// The original harness has stubs which are not applied to this test.\n\ + /// This may cause a mismatch of non-deterministic values if the stub\n\ + /// creates any non-deterministic value.\n\ + /// The execution path may also differ, which can be used to refine the stub\n\ + /// logic.", + ); + } + doc_str +} + /// Generate a formatted unit test from a list of concrete values. -fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTest { +fn format_unit_test( + harness_name: &str, + concrete_vals: &[ConcreteVal], + doc_str: String, +) -> UnitTest { // Hash the concrete values along with the proof harness name. let mut hasher = DefaultHasher::new(); harness_name.hash(&mut hasher); @@ -241,6 +278,7 @@ fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTe let func_name = format!("kani_concrete_playback_{harness_name}_{hash}"); let func_before_concrete_vals = [ + doc_str, "#[test]".to_string(), format!("fn {func_name}() {{"), format!("{:<4}let concrete_vals: Vec> = vec![", " "), @@ -484,9 +522,10 @@ mod tests { /// Since hashes can not be relied on in tests, this compares all parts of a unit test except the hash. #[test] fn format_unit_test_full_func() { + let doc_str = "/// Test documentation"; 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 unit_test = format_unit_test(harness_name, &concrete_vals, doc_str.to_string()); let full_func = unit_test.code; let split_unit_test_name = split_unit_test_name(&unit_test.name); let expected_after_func_name = vec![ @@ -498,18 +537,23 @@ mod tests { "}".to_string(), ]; - assert_eq!(full_func[0], "#[test]"); + assert_eq!(full_func[0], doc_str); + assert_eq!(full_func[1], "#[test]"); assert_eq!( split_unit_test_name.before_hash, format!("kani_concrete_playback_{harness_name}") ); - assert_eq!(full_func[1], format!("fn {}() {{", unit_test.name)); - assert_eq!(full_func[2..], expected_after_func_name); + assert_eq!(full_func[2], format!("fn {}() {{", unit_test.name)); + assert_eq!(full_func[3..], 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); + let unit_test = format_unit_test( + harness_name, + concrete_vals, + "/// Harness created for unit test".to_string(), + ); split_unit_test_name(&unit_test.name).hash } From 33188d12532a2c30c2c7b0edafef43775d841667 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 26 Jul 2024 16:49:21 -0700 Subject: [PATCH 03/11] Fix concrete playback for array and add test --- .../src/concrete_playback/test_generator.rs | 34 ++++++++++++------- library/kani/src/arbitrary.rs | 2 +- library/kani/src/lib.rs | 19 ++++++++--- .../kani_macros/src/sysroot/contracts/mod.rs | 11 +++--- .../playback_contracts/original.rs | 19 +++++++++++ .../playback_with_contracts.expected | 15 ++++++++ .../playback_with_contracts.sh | 20 +++++++++++ 7 files changed, 96 insertions(+), 24 deletions(-) create mode 100644 tests/script-based-pre/playback_contracts/original.rs create mode 100644 tests/script-based-pre/playback_contracts/playback_with_contracts.expected create mode 100755 tests/script-based-pre/playback_contracts/playback_with_contracts.sh diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 62169d357579..946ff9eb4e9b 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -6,6 +6,7 @@ use crate::args::ConcretePlaybackMode; use crate::call_cbmc::VerificationResult; +use crate::cbmc_output_parser::Property; use crate::session::KaniSession; use anyhow::{Context, Result}; use concrete_vals_extractor::{extract_harness_values, ConcreteVal}; @@ -32,7 +33,7 @@ impl KaniSession { }; if let Ok(result_items) = &verification_result.results { - let harness_values: Vec> = extract_harness_values(result_items); + let harness_values = extract_harness_values(result_items); if harness_values.is_empty() { println!( @@ -43,9 +44,9 @@ impl KaniSession { } else { let mut unit_tests: Vec = harness_values .iter() - .map(|concrete_vals| { + .map(|(prop, concrete_vals)| { let pretty_name = harness.get_harness_name_unqualified(); - format_unit_test(&pretty_name, &concrete_vals, gen_test_doc(harness)) + format_unit_test(&pretty_name, &concrete_vals, gen_test_doc(harness, *prop)) }) .collect(); unit_tests.dedup_by(|a, b| a.name == b.name); @@ -168,6 +169,9 @@ impl KaniSession { writeln!(temp_file, "{line}")?; if curr_line_num == proof_harness_end_line { for unit_test in unit_tests.iter() { + // Write an empty line before the unit test. + writeln!(temp_file, "")?; + for unit_test_line in unit_test.code.iter() { curr_line_num += 1; writeln!(temp_file, "{unit_test_line}")?; @@ -176,7 +180,7 @@ impl KaniSession { } } - // Renames are usually automic, so we won't corrupt the user's source file during a + // Renames are usually atomic, so we won't corrupt the user's source file during a // crash; but first flush all updates to disk, which persist wouldn't take care of. temp_file.as_file().sync_all()?; temp_file.persist(source_path).expect("Could not rename file"); @@ -231,14 +235,14 @@ impl KaniSession { } } -fn gen_test_doc(harness: &HarnessMetadata) -> String { +fn gen_test_doc(harness: &HarnessMetadata, property: &Property) -> String { let mut doc_str = match &harness.attributes.kind { HarnessKind::Proof => { format!("/// Test generated for harness `{}` \n", harness.pretty_name) } HarnessKind::ProofForContract { target_fn } => { format!( - "/// Test generated for harness `{}` that check contract for `{target_fn}`\n", + "/// Test generated for harness `{}` that checks contract for `{target_fn}`\n", harness.pretty_name ) } @@ -246,13 +250,19 @@ fn gen_test_doc(harness: &HarnessMetadata) -> String { unreachable!("Concrete playback for tests is not supported") } }; + doc_str.push_str("///\n"); + doc_str.push_str(&format!( + "/// Check for `{}`: \"{}\"\n", + property.property_class(), + property.description + )); if !harness.attributes.stubs.is_empty() { doc_str.push_str("///\n"); doc_str.push_str( "/// # Warning\n\ ///\n\ - /// Concrete playback tests combined with stubs is highly experimental, and\n\ - /// subject to change.\n\ + /// Concrete playback tests combined with stubs or contracts is highly \n\ + /// experimental, and subject to change.\n\ ///\n\ /// The original harness has stubs which are not applied to this test.\n\ /// This may cause a mismatch of non-deterministic values if the stub\n\ @@ -362,7 +372,7 @@ mod concrete_vals_extractor { /// Extract a set of concrete values that trigger one assertion /// failure. Each element of the outer vector corresponds to /// inputs triggering one assertion failure or cover statement. - pub fn extract_harness_values(result_items: &[Property]) -> Vec> { + pub fn extract_harness_values(result_items: &[Property]) -> Vec<(&Property, Vec)> { result_items .iter() .filter(|prop| { @@ -378,7 +388,7 @@ mod concrete_vals_extractor { let concrete_vals: Vec = trace.iter().filter_map(&extract_from_trace_item).collect(); - concrete_vals + (property, concrete_vals) }) .collect() } @@ -397,7 +407,7 @@ mod concrete_vals_extractor { { if trace_item.step_type == "assignment" && lhs.starts_with("goto_symex$$return_value") - && func.starts_with("kani::any_raw_internal") + && func.starts_with("kani::any_raw_") { let declared_width = width_u64 as usize; let actual_width = bit_concrete_val.len(); @@ -647,7 +657,7 @@ mod tests { }), }]), }]; - let concrete_vals = extract_harness_values(&processed_items).pop().unwrap(); + let (_, concrete_vals) = extract_harness_values(&processed_items).pop().unwrap(); let concrete_val = &concrete_vals[0]; assert_eq!(concrete_val.byte_arr, vec![1, 3]); diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index ef6e2ef23dd4..83b113d64927 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -31,7 +31,7 @@ macro_rules! trivial_arbitrary { unsafe { crate::any_raw_internal::() } } fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - unsafe { crate::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() } + unsafe { crate::any_raw_array::() } } } }; diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 3cf46bd7af07..b0a190f89cf2 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -250,20 +250,31 @@ pub fn any_where bool>(f: F) -> T { #[inline(never)] #[cfg(not(feature = "concrete_playback"))] pub(crate) unsafe fn any_raw_internal() -> T { - any_raw_inner::() + any_raw::() } +/// This is the same as [any_raw_internal] for verification flow, but not for concrete playback. #[inline(never)] +#[cfg(not(feature = "concrete_playback"))] +pub(crate) unsafe fn any_raw_array() -> [T; N] { + any_raw::<[T; N]>() +} + #[cfg(feature = "concrete_playback")] -pub(crate) unsafe fn any_raw_internal() -> T { - concrete_playback::any_raw_internal::() +use concrete_playback::any_raw_internal; + +/// Iterate over `any_raw_internal` since CBMC produces assignment per element. +#[inline(never)] +#[cfg(feature = "concrete_playback")] +pub(crate) unsafe fn any_raw_array() -> [T; N] { + [(); N].map(|_| any_raw_internal::()) } /// This low-level function returns nondet bytes of size T. #[rustc_diagnostic_item = "KaniAnyRaw"] #[inline(never)] #[allow(dead_code)] -fn any_raw_inner() -> T { +fn any_raw() -> T { kani_intrinsic() } diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index defcd9dae1b4..12a1215de2c7 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -336,7 +336,7 @@ use proc_macro::TokenStream; use proc_macro2::{Ident, TokenStream as TokenStream2}; use quote::{quote, ToTokens}; -use syn::{parse_macro_input, Expr, ExprClosure, ItemFn}; +use syn::{parse_macro_input, parse_quote, Expr, ExprClosure, ItemFn}; mod bootstrap; mod check; @@ -387,15 +387,12 @@ passthrough!(stub_verified, false); pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { let args = proc_macro2::TokenStream::from(attr); - let ItemFn { attrs, vis, sig, block } = parse_macro_input!(item as ItemFn); + let mut fn_item = parse_macro_input!(item as ItemFn); + fn_item.block.stmts.insert(0, parse_quote!(kani::internal::init_contracts();)); quote!( #[allow(dead_code)] #[kanitool::proof_for_contract = stringify!(#args)] - #(#attrs)* - #vis #sig { - kani::internal::init_contracts(); - #block - } + #fn_item ) .into() } diff --git a/tests/script-based-pre/playback_contracts/original.rs b/tests/script-based-pre/playback_contracts/original.rs new file mode 100644 index 000000000000..8271e9a3d03f --- /dev/null +++ b/tests/script-based-pre/playback_contracts/original.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani correctly adds tests to when the harness is a proof for contract. +extern crate kani; + +#[kani::requires(idx < slice.len())] +#[kani::modifies(slice)] +#[kani::ensures(| _ | slice[idx] == new_val)] +fn modify_slice(slice: &mut [u32], idx: usize, new_val: u32) { + // Inject bug by incrementing index first. + let new_idx = idx + 1; + *slice.get_mut(new_idx).expect("Expected valid index, but contract is wrong") = new_val; +} + +#[kani::proof_for_contract(modify_slice)] +fn check_modify_slice() { + let mut data: [u32; 4] = kani::any(); + modify_slice(&mut data, kani::any(), kani::any()) +} diff --git a/tests/script-based-pre/playback_contracts/playback_with_contracts.expected b/tests/script-based-pre/playback_contracts/playback_with_contracts.expected new file mode 100644 index 000000000000..48aab190b0a4 --- /dev/null +++ b/tests/script-based-pre/playback_contracts/playback_with_contracts.expected @@ -0,0 +1,15 @@ +[TEST] Generate test... +Checking harness check_modify_slice... + +Failed Checks: | _ | slice[idx] == new_val +Failed Checks:\ +in std::option::expect_failed + +VERIFICATION:- FAILED + +[TEST] Run test... + +running 2 tests + +Expected valid index, but contract is wrong +test result: FAILED. 1 passed; 1 failed; diff --git a/tests/script-based-pre/playback_contracts/playback_with_contracts.sh b/tests/script-based-pre/playback_contracts/playback_with_contracts.sh new file mode 100755 index 000000000000..be8fd0279a2d --- /dev/null +++ b/tests/script-based-pre/playback_contracts/playback_with_contracts.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# Test that concrete playback -Z concrete-playback executes as expected +set -o nounset + +RS_FILE="modified.rs" +cp original.rs ${RS_FILE} + +echo "[TEST] Generate test..." +kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace -Z function-contracts --output-format terse + +# Note that today one of the tests will succeed since the contract pre-conditions are not inserted by Kani. +# Hopefully this will change with https://github.com/model-checking/kani/issues/3326 +echo "[TEST] Run test..." +kani playback -Z concrete-playback ${RS_FILE} -- kani_concrete_playback + +# Cleanup +rm ${RS_FILE} +rm kani_concrete_playback \ No newline at end of file From a1437477b3becc248d50d6ce758a52d3d4df3559 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 26 Jul 2024 22:05:22 -0700 Subject: [PATCH 04/11] Fix clippy --- kani-driver/src/concrete_playback/test_generator.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 946ff9eb4e9b..4bf81471b760 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -46,7 +46,7 @@ impl KaniSession { .iter() .map(|(prop, concrete_vals)| { let pretty_name = harness.get_harness_name_unqualified(); - format_unit_test(&pretty_name, &concrete_vals, gen_test_doc(harness, *prop)) + format_unit_test(&pretty_name, &concrete_vals, gen_test_doc(harness, prop)) }) .collect(); unit_tests.dedup_by(|a, b| a.name == b.name); @@ -170,7 +170,7 @@ impl KaniSession { if curr_line_num == proof_harness_end_line { for unit_test in unit_tests.iter() { // Write an empty line before the unit test. - writeln!(temp_file, "")?; + writeln!(temp_file)?; for unit_test_line in unit_test.code.iter() { curr_line_num += 1; From 5922fdbcd8681aeb0ff4f783c84f56ce29a0eae9 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 29 Jul 2024 13:16:40 -0700 Subject: [PATCH 05/11] Fix unit tests and apply changes to `kani_core` --- kani-driver/src/args/mod.rs | 22 +++++++++---------- library/kani/src/concrete_playback.rs | 5 +++++ library/kani/src/lib.rs | 13 +++-------- library/kani_core/src/arbitrary.rs | 2 +- library/kani_core/src/lib.rs | 16 +++++++++----- .../verify_std_cmd/verify_std.sh | 2 +- 6 files changed, 31 insertions(+), 29 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 04f84821660f..cb597120608d 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -137,10 +137,10 @@ pub struct VerificationArgs { /// If value supplied is 'inplace', Kani automatically adds the unit test to your source code. /// This option does not work with `--output-format old`. #[arg( - long, - conflicts_with_all(& ["visualize"]), - ignore_case = true, - value_enum + long, + conflicts_with_all(&["visualize"]), + ignore_case = true, + value_enum )] pub concrete_playback: Option, /// Keep temporary files generated throughout Kani process. This is already the default @@ -210,10 +210,10 @@ pub struct VerificationArgs { /// Pass through directly to CBMC; must be the last flag. /// This feature is unstable and it requires `--enable_unstable` to be used #[arg( - long, - allow_hyphen_values = true, - requires("enable_unstable"), - num_args(0..) + long, + allow_hyphen_values = true, + requires("enable_unstable"), + num_args(0..) )] // consumes everything pub cbmc_args: Vec, @@ -870,13 +870,13 @@ mod tests { let res = parse_unstable_disabled("--harness foo -Z stubbing").unwrap(); assert!(res.verify_opts.is_stubbing_enabled()); - // `-Z stubbing` cannot be called with `--concrete-playback` + // `-Z stubbing` can now be called with concrete playback. let res = parse_unstable_disabled( "--harness foo --concrete-playback=print -Z concrete-playback -Z stubbing", ) .unwrap(); - let err = res.validate().unwrap_err(); - assert_eq!(err.kind(), ErrorKind::ArgumentConflict); + // Note that `res.validate()` fails because input file does not exist. + assert!(matches!(res.verify_opts.validate(), Ok(()))); } #[test] diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs index aa6cd7e4018d..0de51862b7d8 100644 --- a/library/kani/src/concrete_playback.rs +++ b/library/kani/src/concrete_playback.rs @@ -40,6 +40,11 @@ pub fn concrete_playback_run(mut local_concrete_vals: Vec>, pro }); } +/// Iterate over `any_raw_internal` since CBMC produces assignment per element. +pub(crate) unsafe fn any_raw_array() -> [T; N] { + [(); N].map(|_| crate::any_raw_internal::()) +} + /// Concrete playback implementation of /// kani::any_raw_internal. Because CBMC does not bother putting in /// Zero-Sized Types, those are defaulted to an empty vector. diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index b0a190f89cf2..046c6e7a0667 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -249,26 +249,19 @@ pub fn any_where bool>(f: F) -> T { /// Note that SIZE_T must be equal the size of type T in bytes. #[inline(never)] #[cfg(not(feature = "concrete_playback"))] -pub(crate) unsafe fn any_raw_internal() -> T { +unsafe fn any_raw_internal() -> T { any_raw::() } /// This is the same as [any_raw_internal] for verification flow, but not for concrete playback. #[inline(never)] #[cfg(not(feature = "concrete_playback"))] -pub(crate) unsafe fn any_raw_array() -> [T; N] { +unsafe fn any_raw_array() -> [T; N] { any_raw::<[T; N]>() } #[cfg(feature = "concrete_playback")] -use concrete_playback::any_raw_internal; - -/// Iterate over `any_raw_internal` since CBMC produces assignment per element. -#[inline(never)] -#[cfg(feature = "concrete_playback")] -pub(crate) unsafe fn any_raw_array() -> [T; N] { - [(); N].map(|_| any_raw_internal::()) -} +use concrete_playback::{any_raw_array, any_raw_internal}; /// This low-level function returns nondet bytes of size T. #[rustc_diagnostic_item = "KaniAnyRaw"] diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 7cfb649b11a0..ab5213af9b6c 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -34,7 +34,7 @@ macro_rules! generate_arbitrary { unsafe { crate::kani::any_raw_internal::() } } fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - unsafe { crate::kani::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() } + unsafe { crate::kani::any_raw_aray::<[Self; MAX_ARRAY_LENGTH]>() } } } }; diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 016c805e8f8e..9baba1abe886 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -248,21 +248,25 @@ macro_rules! kani_intrinsics { /// Note that SIZE_T must be equal the size of type T in bytes. #[inline(never)] #[cfg(not(feature = "concrete_playback"))] - pub(crate) unsafe fn any_raw_internal() -> T { - any_raw_inner::() + unsafe fn any_raw_internal() -> T { + any_raw::() } + /// This is the same as [any_raw_internal] for verification flow, but not for concrete playback. #[inline(never)] - #[cfg(feature = "concrete_playback")] - pub(crate) unsafe fn any_raw_internal() -> T { - concrete_playback::any_raw_internal::() + #[cfg(not(feature = "concrete_playback"))] + unsafe fn any_raw_array() -> [T; N] { + any_raw::<[T; N]>() } + #[cfg(feature = "concrete_playback")] + use concrete_playback::{any_raw_array, any_raw_internal}; + /// This low-level function returns nondet bytes of size T. #[rustc_diagnostic_item = "KaniAnyRaw"] #[inline(never)] #[allow(dead_code)] - pub fn any_raw_inner() -> T { + fn any_raw() -> T { kani_intrinsic() } diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index 91454c4b65e7..3a24bf15241e 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -29,7 +29,7 @@ mod verify { use core::kani; #[kani::proof] fn check_non_zero() { - let orig: u32 = kani::any_raw_inner(); + let orig: u32 = kani::any(); if let Some(val) = core::num::NonZeroU32::new(orig) { assert!(orig == val.into()); } else { From e2a2e4a48aaaeab5c23c461ca3f580786f6e450c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 29 Jul 2024 14:35:33 -0700 Subject: [PATCH 06/11] Add missing test configuration file --- tests/script-based-pre/playback_contracts/config.yml | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 tests/script-based-pre/playback_contracts/config.yml diff --git a/tests/script-based-pre/playback_contracts/config.yml b/tests/script-based-pre/playback_contracts/config.yml new file mode 100644 index 000000000000..98e3546f5b78 --- /dev/null +++ b/tests/script-based-pre/playback_contracts/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: playback_with_contracts.sh +expected: playback_with_contracts.expected From eb67857236759f730b84a04bcb787be491160224 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 29 Jul 2024 20:37:11 -0700 Subject: [PATCH 07/11] Update library/kani_core/src/arbitrary.rs Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/kani_core/src/arbitrary.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index ab5213af9b6c..43f4b74c183a 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -34,7 +34,7 @@ macro_rules! generate_arbitrary { unsafe { crate::kani::any_raw_internal::() } } fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - unsafe { crate::kani::any_raw_aray::<[Self; MAX_ARRAY_LENGTH]>() } + unsafe { crate::kani::any_raw_array::() } } } }; From 3b75f2c3dc41f63b81e1b1f5d24891fdf2cee7cb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 29 Jul 2024 20:37:24 -0700 Subject: [PATCH 08/11] Update kani_metadata/src/harness.rs Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- kani_metadata/src/harness.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 5ae16aae7a33..b4e24a8de10f 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -63,7 +63,7 @@ pub enum HarnessKind { } impl HarnessAttributes { - /// Create a new harness with of the provided kind. + /// Create a new harness of the provided kind. pub fn new(kind: HarnessKind) -> HarnessAttributes { HarnessAttributes { kind, From a25f1a479a9150c2956a82cb5bf26b68e87b25ee Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 30 Jul 2024 18:27:27 -0700 Subject: [PATCH 09/11] Add more tests and fix typo in kani_core --- library/kani_core/src/arbitrary.rs | 2 +- .../playback_contracts/config.yml | 4 -- .../playback_with_contracts.expected | 15 ------- .../playback_with_contracts.sh | 20 ---------- .../playback_expected/config.yml | 4 ++ .../playback_expected/expected | 8 ++++ .../playback_expected/playback.sh | 39 +++++++++++++++++++ .../src/playback_contract.rs} | 0 .../playback_expected/src/playback_stubs.rs | 34 ++++++++++++++++ 9 files changed, 86 insertions(+), 40 deletions(-) delete mode 100644 tests/script-based-pre/playback_contracts/config.yml delete mode 100644 tests/script-based-pre/playback_contracts/playback_with_contracts.expected delete mode 100755 tests/script-based-pre/playback_contracts/playback_with_contracts.sh create mode 100644 tests/script-based-pre/playback_expected/config.yml create mode 100644 tests/script-based-pre/playback_expected/expected create mode 100755 tests/script-based-pre/playback_expected/playback.sh rename tests/script-based-pre/{playback_contracts/original.rs => playback_expected/src/playback_contract.rs} (100%) create mode 100644 tests/script-based-pre/playback_expected/src/playback_stubs.rs diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 43f4b74c183a..8c6cfd335104 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -34,7 +34,7 @@ macro_rules! generate_arbitrary { unsafe { crate::kani::any_raw_internal::() } } fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - unsafe { crate::kani::any_raw_array::() } + unsafe { crate::kani::any_raw_array::() } } } }; diff --git a/tests/script-based-pre/playback_contracts/config.yml b/tests/script-based-pre/playback_contracts/config.yml deleted file mode 100644 index 98e3546f5b78..000000000000 --- a/tests/script-based-pre/playback_contracts/config.yml +++ /dev/null @@ -1,4 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -script: playback_with_contracts.sh -expected: playback_with_contracts.expected diff --git a/tests/script-based-pre/playback_contracts/playback_with_contracts.expected b/tests/script-based-pre/playback_contracts/playback_with_contracts.expected deleted file mode 100644 index 48aab190b0a4..000000000000 --- a/tests/script-based-pre/playback_contracts/playback_with_contracts.expected +++ /dev/null @@ -1,15 +0,0 @@ -[TEST] Generate test... -Checking harness check_modify_slice... - -Failed Checks: | _ | slice[idx] == new_val -Failed Checks:\ -in std::option::expect_failed - -VERIFICATION:- FAILED - -[TEST] Run test... - -running 2 tests - -Expected valid index, but contract is wrong -test result: FAILED. 1 passed; 1 failed; diff --git a/tests/script-based-pre/playback_contracts/playback_with_contracts.sh b/tests/script-based-pre/playback_contracts/playback_with_contracts.sh deleted file mode 100755 index be8fd0279a2d..000000000000 --- a/tests/script-based-pre/playback_contracts/playback_with_contracts.sh +++ /dev/null @@ -1,20 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -# Test that concrete playback -Z concrete-playback executes as expected -set -o nounset - -RS_FILE="modified.rs" -cp original.rs ${RS_FILE} - -echo "[TEST] Generate test..." -kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace -Z function-contracts --output-format terse - -# Note that today one of the tests will succeed since the contract pre-conditions are not inserted by Kani. -# Hopefully this will change with https://github.com/model-checking/kani/issues/3326 -echo "[TEST] Run test..." -kani playback -Z concrete-playback ${RS_FILE} -- kani_concrete_playback - -# Cleanup -rm ${RS_FILE} -rm kani_concrete_playback \ No newline at end of file diff --git a/tests/script-based-pre/playback_expected/config.yml b/tests/script-based-pre/playback_expected/config.yml new file mode 100644 index 000000000000..d15b5d277ed6 --- /dev/null +++ b/tests/script-based-pre/playback_expected/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: playback.sh +expected: expected diff --git a/tests/script-based-pre/playback_expected/expected b/tests/script-based-pre/playback_expected/expected new file mode 100644 index 000000000000..bedb39581b7f --- /dev/null +++ b/tests/script-based-pre/playback_expected/expected @@ -0,0 +1,8 @@ +[TEST] Generate test for playback_contract.rs... +Verification failed for - check_modify_slice +Result for playback_contract.rs: test result: FAILED. 1 passed; 1 failed + +[TEST] Generate test for playback_stubs.rs... +Verification failed for - check_lt_0 +Verification failed for - check_bad_stub +Result for playback_stubs.rs: test result: FAILED. 1 passed; 1 failed diff --git a/tests/script-based-pre/playback_expected/playback.sh b/tests/script-based-pre/playback_expected/playback.sh new file mode 100755 index 000000000000..0a1a6997e59e --- /dev/null +++ b/tests/script-based-pre/playback_expected/playback.sh @@ -0,0 +1,39 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# This will run Kani verification in every `src/*.rs` file followed by playback command. +# Expected output is generated from individual expected files. +set -o nounset + +run() { + input_rs=${1:?"Missing input file"} + + echo "[TEST] Generate test for $input_rs..." + kani ${input_rs} \ + -Z concrete-playback --concrete-playback=inplace \ + -Z function-contracts -Z stubbing --output-format terse + + # Note that today one of the tests will succeed since the contract pre-conditions are not inserted by Kani. + # Hopefully this will change with https://github.com/model-checking/kani/issues/3326 + echo "[TEST] Run test for $input_rs..." + summary=$(kani playback -Z concrete-playback ${input_rs} -- kani_concrete_playback | grep "test result") + echo "Result for $input_rs: $summary" +} + +ROOT_DIR=$(git rev-parse --show-toplevel) +MODIFIED_DIR=modified +rm -rf $MODIFIED_DIR +mkdir $MODIFIED_DIR + +for rs in src/*.rs +do + [[ -e "${rs}" ]] || exit 1 + echo "Running ${rs}" + cp "$rs" $MODIFIED_DIR + pushd $MODIFIED_DIR + run $(basename $rs) + popd +done + + # Cleanup +rm -rf $MODIFIED_DIR \ No newline at end of file diff --git a/tests/script-based-pre/playback_contracts/original.rs b/tests/script-based-pre/playback_expected/src/playback_contract.rs similarity index 100% rename from tests/script-based-pre/playback_contracts/original.rs rename to tests/script-based-pre/playback_expected/src/playback_contract.rs diff --git a/tests/script-based-pre/playback_expected/src/playback_stubs.rs b/tests/script-based-pre/playback_expected/src/playback_stubs.rs new file mode 100644 index 000000000000..ce5107949f04 --- /dev/null +++ b/tests/script-based-pre/playback_expected/src/playback_stubs.rs @@ -0,0 +1,34 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani playback works with stubs. +#![allow(dead_code)] + +fn is_zero(val: u8) -> bool { + val == 0 +} + +fn not_zero(val: u8) -> bool { + val != 0 +} + +/// Add a harness that will fail due to incorrect stub but the test will succeed. +#[kani::proof] +#[kani::stub(is_zero, not_zero)] +fn check_bad_stub() { + assert!(is_zero(kani::any())) +} + +fn lt_zero(val: i8) -> bool { + val < 0 +} + +fn lt_ten(val: i8) -> bool { + val < 10 +} + +/// Add a harness that will fail in an equivalent way. +#[kani::proof] +#[kani::stub(lt_zero, lt_ten)] +fn check_lt_0() { + assert!(lt_zero(kani::any())) +} From 5fab5147aa6ada04518e5cad3cda863783557b65 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 31 Jul 2024 10:28:20 -0700 Subject: [PATCH 10/11] Apply suggestions from code review Co-authored-by: Felipe R. Monteiro --- .../src/concrete_playback/test_generator.rs | 25 +++++++------- .../playback_expected/playback.sh | 33 ++++++++++--------- 2 files changed, 30 insertions(+), 28 deletions(-) diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 4bf81471b760..4029893ecf34 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -257,19 +257,18 @@ fn gen_test_doc(harness: &HarnessMetadata, property: &Property) -> String { property.description )); if !harness.attributes.stubs.is_empty() { - doc_str.push_str("///\n"); - doc_str.push_str( - "/// # Warning\n\ - ///\n\ - /// Concrete playback tests combined with stubs or contracts is highly \n\ - /// experimental, and subject to change.\n\ - ///\n\ - /// The original harness has stubs which are not applied to this test.\n\ - /// This may cause a mismatch of non-deterministic values if the stub\n\ - /// creates any non-deterministic value.\n\ - /// The execution path may also differ, which can be used to refine the stub\n\ - /// logic.", - ); +doc_str.push_str(r#"/// +/// # Warning +/// +/// Concrete playback tests combined with stubs or contracts is highly +/// experimental, and subject to change. +/// +/// The original harness has stubs which are not applied to this test. +/// This may cause a mismatch of non-deterministic values if the stub +/// creates any non-deterministic value. +/// The execution path may also differ, which can be used to refine the stub +/// logic. +"#); } doc_str } diff --git a/tests/script-based-pre/playback_expected/playback.sh b/tests/script-based-pre/playback_expected/playback.sh index 0a1a6997e59e..722c96239371 100755 --- a/tests/script-based-pre/playback_expected/playback.sh +++ b/tests/script-based-pre/playback_expected/playback.sh @@ -6,18 +6,18 @@ set -o nounset run() { - input_rs=${1:?"Missing input file"} + local input_rs=${1:?"Missing input file"} - echo "[TEST] Generate test for $input_rs..." - kani ${input_rs} \ + echo "[TEST] Generate test for ${input_rs}..." + kani "${input_rs}" \ -Z concrete-playback --concrete-playback=inplace \ -Z function-contracts -Z stubbing --output-format terse # Note that today one of the tests will succeed since the contract pre-conditions are not inserted by Kani. # Hopefully this will change with https://github.com/model-checking/kani/issues/3326 - echo "[TEST] Run test for $input_rs..." - summary=$(kani playback -Z concrete-playback ${input_rs} -- kani_concrete_playback | grep "test result") - echo "Result for $input_rs: $summary" + echo "[TEST] Run test for ${input_rs}..." + summary=$(kani playback -Z concrete-playback "${input_rs}" -- kani_concrete_playback | grep "test result") + echo "Result for ${input_rs}: ${summary}" } ROOT_DIR=$(git rev-parse --show-toplevel) @@ -25,15 +25,18 @@ MODIFIED_DIR=modified rm -rf $MODIFIED_DIR mkdir $MODIFIED_DIR -for rs in src/*.rs -do - [[ -e "${rs}" ]] || exit 1 - echo "Running ${rs}" - cp "$rs" $MODIFIED_DIR - pushd $MODIFIED_DIR - run $(basename $rs) - popd +for rs in src/*.rs; do + if [[ -e "${rs}" ]]; then + echo "Running ${rs}" + cp "${rs}" "${MODIFIED_DIR}" + pushd "${MODIFIED_DIR}" > /dev/null + run "$(basename "${rs}")" + popd > /dev/null + else + echo "No .rs files found in src directory" + exit 1 + fi done # Cleanup -rm -rf $MODIFIED_DIR \ No newline at end of file +rm -rf "${MODIFIED_DIR}" \ No newline at end of file From f4260e024977d37d2cffd6bd46e36ccdd2134638 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 31 Jul 2024 10:44:52 -0700 Subject: [PATCH 11/11] Address PR comments --- kani-compiler/src/kani_middle/codegen_units.rs | 2 +- kani-driver/src/concrete_playback/test_generator.rs | 12 +++++++----- kani_metadata/src/harness.rs | 2 +- tests/script-based-pre/playback_expected/playback.sh | 4 ++-- 4 files changed, 11 insertions(+), 9 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 3f88ad2ecd3b..b4ea06c8d5db 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -104,7 +104,7 @@ impl CodegenUnits { /// Generate [KaniMetadata] for the target crate. fn generate_metadata(&self) -> KaniMetadata { let (proof_harnesses, test_harnesses) = - self.harness_info.values().cloned().partition(|md| md.attributes.is_proof()); + self.harness_info.values().cloned().partition(|md| md.attributes.is_proof_harness()); KaniMetadata { crate_name: self.crate_info.name.clone(), proof_harnesses, diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 4029893ecf34..5faa6299a5d3 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -257,18 +257,20 @@ fn gen_test_doc(harness: &HarnessMetadata, property: &Property) -> String { property.description )); if !harness.attributes.stubs.is_empty() { -doc_str.push_str(r#"/// + doc_str.push_str( + r#"/// /// # Warning -/// -/// Concrete playback tests combined with stubs or contracts is highly +/// +/// Concrete playback tests combined with stubs or contracts is highly /// experimental, and subject to change. -/// +/// /// The original harness has stubs which are not applied to this test. /// This may cause a mismatch of non-deterministic values if the stub /// creates any non-deterministic value. /// The execution path may also differ, which can be used to refine the stub /// logic. -"#); +"#, + ); } doc_str } diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index b4e24a8de10f..41eb4eb20919 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -75,7 +75,7 @@ impl HarnessAttributes { } /// Return whether this is a proof harness. - pub fn is_proof(&self) -> bool { + pub fn is_proof_harness(&self) -> bool { matches!(self.kind, HarnessKind::Proof | HarnessKind::ProofForContract { .. }) } } diff --git a/tests/script-based-pre/playback_expected/playback.sh b/tests/script-based-pre/playback_expected/playback.sh index 722c96239371..3b358db257a2 100755 --- a/tests/script-based-pre/playback_expected/playback.sh +++ b/tests/script-based-pre/playback_expected/playback.sh @@ -22,8 +22,8 @@ run() { ROOT_DIR=$(git rev-parse --show-toplevel) MODIFIED_DIR=modified -rm -rf $MODIFIED_DIR -mkdir $MODIFIED_DIR +rm -rf "${MODIFIED_DIR}" +mkdir "${MODIFIED_DIR}" for rs in src/*.rs; do if [[ -e "${rs}" ]]; then