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