diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 7c7066863be6..f51eea38cbd8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -46,6 +46,47 @@ fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool { false } +/// A hook for Kani's `cover` function (declared in `library/kani/src/lib.rs`). +/// The function takes two arguments: a condition expression (bool) and a +/// message (&'static str). +/// The hook codegens the function as a cover property that checks whether the +/// condition is satisfiable. Unlike assertions, cover properties currently do +/// not have an impact on verification success or failure. See +/// +/// for more details. +struct Cover; +impl<'tcx> GotocHook<'tcx> for Cover { + fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { + matches_function(tcx, instance, "KaniCover") + } + + fn handle( + &self, + tcx: &mut GotocCtx<'tcx>, + _instance: Instance<'tcx>, + mut fargs: Vec, + _assign_to: Place<'tcx>, + target: Option, + span: Option, + ) -> Stmt { + assert_eq!(fargs.len(), 2); + let cond = fargs.remove(0).cast_to(Type::bool()); + let msg = fargs.remove(0); + let msg = tcx.extract_const_message(&msg).unwrap(); + let target = target.unwrap(); + let caller_loc = tcx.codegen_caller_span(&span); + let loc = tcx.codegen_span_option(span); + + Stmt::block( + vec![ + tcx.codegen_cover(cond, &msg, span), + Stmt::goto(tcx.current_fn().find_label(&target), caller_loc), + ], + loc, + ) + } +} + struct ExpectFail; impl<'tcx> GotocHook<'tcx> for ExpectFail { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { @@ -369,6 +410,7 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> { Rc::new(Panic), Rc::new(Assume), Rc::new(Assert), + Rc::new(Cover), Rc::new(ExpectFail), Rc::new(Nondet), Rc::new(RustAlloc), diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index c8588e06d450..1c1b88a51403 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -82,10 +82,17 @@ pub struct PropertyId { } impl Property { + const COVER_PROPERTY_CLASS: &str = "cover"; + pub fn property_class(&self) -> String { self.property_id.class.clone() } + /// Returns true if this is a cover property + pub fn is_cover_property(&self) -> bool { + self.property_id.class == Self::COVER_PROPERTY_CLASS + } + pub fn property_name(&self) -> String { let class = &self.property_id.class; let id = self.property_id.id; @@ -293,18 +300,22 @@ impl std::fmt::Display for TraceData { #[serde(rename_all = "UPPERCASE")] pub enum CheckStatus { Failure, + Satisfied, // for cover properties only Success, Undetermined, Unreachable, + Unsatisfiable, // for cover properties only } impl std::fmt::Display for CheckStatus { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let check_str = match self { + CheckStatus::Satisfied => style("SATISFIED").green(), CheckStatus::Success => style("SUCCESS").green(), CheckStatus::Failure => style("FAILURE").red(), CheckStatus::Unreachable => style("UNREACHABLE").yellow(), CheckStatus::Undetermined => style("UNDETERMINED").yellow(), + CheckStatus::Unsatisfiable => style("UNSATISFIABLE").yellow(), }; write!(f, "{check_str}") } diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 3a105f9c5937..81bf7a411d5c 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -231,15 +231,26 @@ fn format_item_terse(_item: &ParserItem) -> Option { /// This could be split into two functions for clarity, but at the moment /// it uses the flag `show_checks` which depends on the output format. /// +/// This function reports the results of normal checks (e.g. assertions and +/// arithmetic overflow checks) and cover properties (specified using the +/// `kani::cover` macro) separately. Cover properties currently do not impact +/// the overall verification success or failure. +/// /// TODO: We could `write!` to `result_str` instead /// pub fn format_result(properties: &Vec, show_checks: bool) -> String { let mut result_str = String::new(); - let mut number_tests_failed = 0; - let mut number_tests_unreachable = 0; - let mut number_tests_undetermined = 0; + let mut number_checks_failed = 0; + let mut number_checks_unreachable = 0; + let mut number_checks_undetermined = 0; let mut failed_tests: Vec<&Property> = vec![]; + // cover checks + let mut number_covers_satisfied = 0; + let mut number_covers_undetermined = 0; + let mut number_covers_unreachable = 0; + let mut number_covers_unsatisfiable = 0; + let mut index = 1; if show_checks { @@ -254,14 +265,30 @@ pub fn format_result(properties: &Vec, show_checks: bool) -> String { match status { CheckStatus::Failure => { - number_tests_failed += 1; + number_checks_failed += 1; failed_tests.push(prop); } CheckStatus::Undetermined => { - number_tests_undetermined += 1; + if prop.is_cover_property() { + number_covers_undetermined += 1; + } else { + number_checks_undetermined += 1; + } } CheckStatus::Unreachable => { - number_tests_unreachable += 1; + if prop.is_cover_property() { + number_covers_unreachable += 1; + } else { + number_checks_unreachable += 1; + } + } + CheckStatus::Satisfied => { + assert!(prop.is_cover_property()); + number_covers_satisfied += 1; + } + CheckStatus::Unsatisfiable => { + assert!(prop.is_cover_property()); + number_covers_unsatisfiable += 1; } _ => (), } @@ -291,16 +318,23 @@ pub fn format_result(properties: &Vec, show_checks: bool) -> String { result_str.push_str("\nVERIFICATION RESULT:"); } - let summary = format!("\n ** {number_tests_failed} of {} failed", properties.len()); + let number_cover_properties = number_covers_satisfied + + number_covers_unreachable + + number_covers_unsatisfiable + + number_covers_undetermined; + + let number_properties = properties.len() - number_cover_properties; + + let summary = format!("\n ** {number_checks_failed} of {} failed", number_properties); result_str.push_str(&summary); let mut other_status = Vec::::new(); - if number_tests_undetermined > 0 { - let undetermined_str = format!("{number_tests_undetermined} undetermined"); + if number_checks_undetermined > 0 { + let undetermined_str = format!("{number_checks_undetermined} undetermined"); other_status.push(undetermined_str); } - if number_tests_unreachable > 0 { - let unreachable_str = format!("{number_tests_unreachable} unreachable"); + if number_checks_unreachable > 0 { + let unreachable_str = format!("{number_checks_unreachable} unreachable"); other_status.push(unreachable_str); } if !other_status.is_empty() { @@ -310,13 +344,38 @@ pub fn format_result(properties: &Vec, show_checks: bool) -> String { } result_str.push('\n'); + if number_cover_properties > 0 { + // Print a summary line for cover properties + let summary = format!( + "\n ** {number_covers_satisfied} of {} cover properties satisfied", + number_cover_properties + ); + result_str.push_str(&summary); + let mut other_status = Vec::::new(); + if number_covers_undetermined > 0 { + let undetermined_str = format!("{number_covers_undetermined} undetermined"); + other_status.push(undetermined_str); + } + if number_covers_unreachable > 0 { + let unreachable_str = format!("{number_covers_unreachable} unreachable"); + other_status.push(unreachable_str); + } + if !other_status.is_empty() { + result_str.push_str(" ("); + result_str.push_str(&other_status.join(",")); + result_str.push(')'); + } + result_str.push('\n'); + result_str.push('\n'); + } + for prop in failed_tests { let failure_message = build_failure_message(prop.description.clone(), &prop.trace.clone()); result_str.push_str(&failure_message); } let verification_result = - if number_tests_failed == 0 { style("SUCCESSFUL").green() } else { style("FAILED").red() }; + if number_checks_failed == 0 { style("SUCCESSFUL").green() } else { style("FAILED").red() }; let overall_result = format!("\nVERIFICATION:- {verification_result}\n"); result_str.push_str(&overall_result); @@ -413,7 +472,7 @@ pub fn postprocess_result(properties: Vec, extra_ptr_checks: bool) -> let (properties_without_reachs, reach_checks) = filter_reach_checks(properties_with_undefined); // Filter out successful sanity checks introduced during compilation let properties_without_sanity_checks = filter_sanity_checks(properties_without_reachs); - // Annotate properties with the results from reachability checks + // Annotate properties with the results of reachability checks let properties_annotated = annotate_properties_with_reach_results(properties_without_sanity_checks, reach_checks); // Remove reachability check IDs from regular property descriptions @@ -429,7 +488,9 @@ pub fn postprocess_result(properties: Vec, extra_ptr_checks: bool) -> || has_failed_unwinding_asserts || has_reachable_undefined_functions; - update_properties_with_reach_status(properties_filtered, has_fundamental_failures) + let updated_properties = + update_properties_with_reach_status(properties_filtered, has_fundamental_failures); + update_results_of_cover_checks(updated_properties) } /// Determines if there is property with status `FAILURE` and the given description @@ -495,7 +556,7 @@ fn get_readable_description(property: &Property) -> String { original } -/// Performs a last pass to update all properties as follows: +/// Performs a pass to update all properties as follows: /// 1. Descriptions are replaced with more readable ones. /// 2. If there were failures that made the verification result unreliable /// (e.g., a reachable unsupported construct), changes all `SUCCESS` results @@ -525,6 +586,23 @@ fn update_properties_with_reach_status( properties } +/// Update the results of cover properties. +/// We encode cover(cond) as assert(!cond), so if the assertion +/// fails, then the cover property is satisfied and vice versa. +/// - SUCCESS -> UNSATISFIABLE +/// - FAILURE -> SATISFIED +fn update_results_of_cover_checks(mut properties: Vec) -> Vec { + for prop in properties.iter_mut() { + if prop.is_cover_property() { + if prop.status == CheckStatus::Success { + prop.status = CheckStatus::Unsatisfiable; + } else if prop.status == CheckStatus::Failure { + prop.status = CheckStatus::Satisfied; + } + } + } + properties +} /// Some Kani-generated asserts have a unique ID in their description of the form: /// ```text /// [KANI_CHECK_ID__] diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 1f983c472966..2e63ba41cc35 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -64,6 +64,28 @@ pub const fn assert(_cond: bool, _msg: &'static str) { } } +/// Creates a cover property with the specified condition and message. +/// +/// # Example: +/// +/// ```rust +/// kani::cover(slice.len() == 0, "The slice may have a length of 0"); +/// ``` +/// +/// A cover property checks if there is at least one execution that satisfies +/// the specified condition at the location in which the function is called. +/// +/// Cover properties are reported as: +/// - SATISFIED: if Kani found an execution that satisfies the condition +/// - UNSATISFIABLE: if Kani proved that the condition cannot be satisfied +/// +/// This function is called by the [`cover!`] macro. The macro is more +/// convenient to use. +/// +#[inline(never)] +#[rustc_diagnostic_item = "KaniCover"] +pub fn cover(_cond: bool, _msg: &'static str) {} + /// This creates an symbolic *valid* value of type `T`. You can assign the return value of this /// function to a variable that you want to make symbolic. /// @@ -138,5 +160,54 @@ pub const fn panic(message: &'static str) -> ! { panic!("{}", message) } +/// A macro to check if a condition is satisfiable at a specific location in the +/// code. +/// +/// # Example 1: +/// +/// ```rust +/// let mut set: BTreeSet = BTreeSet::new(); +/// set.insert(kani::any()); +/// set.insert(kani::any()); +/// // check if the set can end up with a single element (if both elements +/// // inserted were the same) +/// kani::cover!(set.len() == 1); +/// ``` +/// The macro can also be called without any arguments to check if a location is +/// reachable. +/// +/// # Example 2: +/// +/// ```rust +/// match e { +/// MyEnum::A => { /* .. */ } +/// MyEnum::B => { +/// // make sure the `MyEnum::B` variant is possible +/// kani::cover!(); +/// // .. +/// } +/// } +/// ``` +/// +/// A custom message can also be passed to the macro. +/// +/// # Example 3: +/// +/// ```rust +/// kani::cover!(x > y, "x can be greater than y") +/// ``` +#[macro_export] +macro_rules! cover { + () => { + kani::cover(true, "cover location"); + }; + ($cond:expr $(,)?) => { + kani::cover($cond, concat!("cover condition: ", stringify!($cond))); + }; + ($cond:expr, $msg:literal) => { + kani::cover($cond, $msg); + }; +} + /// Kani proc macros must be in a separate crate pub use kani_macros::*; diff --git a/tests/expected/cover/cover-fail/expected b/tests/expected/cover/cover-fail/expected new file mode 100644 index 000000000000..49ffe167a124 --- /dev/null +++ b/tests/expected/cover/cover-fail/expected @@ -0,0 +1,7 @@ +Status: UNSATISFIABLE\ +Description: "cover location"\ +main.rs:29:23 in function cover_overconstrained + + ** 0 of 1 cover properties satisfied + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/cover/cover-fail/main.rs b/tests/expected/cover/cover-fail/main.rs new file mode 100644 index 000000000000..1bd63ab4d126 --- /dev/null +++ b/tests/expected/cover/cover-fail/main.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that overconstraining could lead to unsatisfiable cover statements + +enum Sign { + Positive, + Negative, + Zero, +} + +fn get_sign(x: i32) -> Sign { + if x > 0 { + Sign::Positive + } else if x < 0 { + Sign::Negative + } else { + Sign::Zero + } +} + +#[kani::proof] +fn cover_overconstrained() { + let x: i32 = kani::any(); + kani::assume(x != 0); + let sign = get_sign(x); + + match sign { + Sign::Zero => kani::cover!(), + _ => {} + } +} diff --git a/tests/expected/cover/cover-message/expected b/tests/expected/cover/cover-message/expected new file mode 100644 index 000000000000..e229cf8167ae --- /dev/null +++ b/tests/expected/cover/cover-message/expected @@ -0,0 +1,15 @@ +Status: SATISFIED\ +Description: "foo may return Err"\ +main.rs:17:20 in function cover_match + +Status: SATISFIED\ +Description: "y may be greater than 20"\ +main.rs:15:28 in function cover_match + +Status: UNSATISFIABLE\ +Description: "y may be greater than 10"\ +main.rs:16:18 in function cover_match + + ** 2 of 3 cover properties satisfied + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/cover/cover-message/main.rs b/tests/expected/cover/cover-message/main.rs new file mode 100644 index 000000000000..3e40a90d05a0 --- /dev/null +++ b/tests/expected/cover/cover-message/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that the message used in the kani::cover macro appears in the results + +fn foo(x: i32) -> Result { + if x < 100 { Ok(x / 2) } else { Err("x is too big") } +} + +#[kani::proof] +#[kani::unwind(21)] +fn cover_match() { + let x = kani::any(); + match foo(x) { + Ok(y) if x > 20 => kani::cover!(y > 20, "y may be greater than 20"), // satisfiable + Ok(y) => kani::cover!(y > 10, "y may be greater than 10"), // unsatisfiable + Err(_s) => kani::cover!(true, "foo may return Err"), // satisfiable + } +} diff --git a/tests/expected/cover/cover-pass/expected b/tests/expected/cover/cover-pass/expected new file mode 100644 index 000000000000..59b85ec64ee1 --- /dev/null +++ b/tests/expected/cover/cover-pass/expected @@ -0,0 +1,11 @@ +Status: SATISFIED\ +Description: "cover condition: sorted == arr"\ +main.rs:12:5 in function cover_sorted + +Status: SATISFIED\ +Description: "cover condition: sorted != arr"\ +main.rs:13:5 in function cover_sorted + + ** 2 of 2 cover properties satisfied + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/cover/cover-pass/main.rs b/tests/expected/cover/cover-pass/main.rs new file mode 100644 index 000000000000..c0332e60f3f6 --- /dev/null +++ b/tests/expected/cover/cover-pass/main.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that a sorted array may be the same or different than the original + +#[kani::proof] +#[kani::unwind(21)] +fn cover_sorted() { + let arr: [i32; 5] = kani::any(); + let mut sorted = arr.clone(); + sorted.sort(); + kani::cover!(sorted == arr); + kani::cover!(sorted != arr); +} diff --git a/tests/expected/cover/cover-undetermined/expected b/tests/expected/cover/cover-undetermined/expected new file mode 100644 index 000000000000..dcbc9fddb12e --- /dev/null +++ b/tests/expected/cover/cover-undetermined/expected @@ -0,0 +1,11 @@ +Status: UNDETERMINED\ +Description: "cover condition: sum == 10"\ +main.rs:15:5 in function cover_undetermined + + ** 0 of 1 cover properties satisfied (1 undetermined) + +Failed Checks: unwinding assertion loop 0 + +VERIFICATION:- FAILED +[Kani] info: Verification output shows one or more unwinding failures. +[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`. diff --git a/tests/expected/cover/cover-undetermined/main.rs b/tests/expected/cover/cover-undetermined/main.rs new file mode 100644 index 000000000000..05afa581143b --- /dev/null +++ b/tests/expected/cover/cover-undetermined/main.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Check that a failed unwinding assertion would lead to reporting a cover +/// property as UNDETERMINED if it's not satisfiable with the given unwind bound + +#[kani::proof] +#[kani::unwind(10)] +fn cover_undetermined() { + let x = [1; 10]; + let mut sum = 0; + for i in x { + sum += i; + } + kani::cover!(sum == 10); +} diff --git a/tests/kani/Cover/simp_satisfied.rs b/tests/kani/Cover/simp_satisfied.rs new file mode 100644 index 000000000000..6eefce81ee1b --- /dev/null +++ b/tests/kani/Cover/simp_satisfied.rs @@ -0,0 +1,10 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// A simple cover statement that should pass + +#[kani::proof] +fn check_pass() { + let x: i32 = kani::any(); + kani::cover!(x == 58); +} diff --git a/tests/kani/Cover/simp_unsatisfiable.rs b/tests/kani/Cover/simp_unsatisfiable.rs new file mode 100644 index 000000000000..001bef844cf2 --- /dev/null +++ b/tests/kani/Cover/simp_unsatisfiable.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// A simple cover statement that is unsatisfiable + +#[kani::proof] +fn main() { + let x: u8 = kani::any(); + kani::assume(x < 5); // [0, 4] + let y: u8 = kani::any(); + kani::assume(y < x); // [0, 3] + kani::cover!(y > 3); +}