From ac03425437df4038dd75dbc8ab96d2c9e8dea307 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 15 Nov 2022 22:52:48 -0800 Subject: [PATCH 1/3] Add a kani cover statement --- .../codegen_cprover_gotoc/overrides/hooks.rs | 33 +++++++++++++++++++ kani-driver/src/cbmc_property_renderer.rs | 21 ++++++++++-- library/kani/src/lib.rs | 31 +++++++++++++++++ tests/expected/cover-fail/expected | 8 +++++ tests/expected/cover-fail/main.rs | 32 ++++++++++++++++++ tests/expected/cover-pass/expected | 9 +++++ tests/expected/cover-pass/main.rs | 14 ++++++++ tests/expected/cover-undetermined/expected | 9 +++++ tests/expected/cover-undetermined/main.rs | 16 +++++++++ tests/kani/Cover/simp_fail.rs | 14 ++++++++ tests/kani/Cover/simp_pass.rs | 10 ++++++ 11 files changed, 195 insertions(+), 2 deletions(-) create mode 100644 tests/expected/cover-fail/expected create mode 100644 tests/expected/cover-fail/main.rs create mode 100644 tests/expected/cover-pass/expected create mode 100644 tests/expected/cover-pass/main.rs create mode 100644 tests/expected/cover-undetermined/expected create mode 100644 tests/expected/cover-undetermined/main.rs create mode 100644 tests/kani/Cover/simp_fail.rs create mode 100644 tests/kani/Cover/simp_pass.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 7c7066863be6..129ddb052555 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -46,6 +46,38 @@ fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool { false } +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(), 1); + let cond = fargs.remove(0).cast_to(Type::bool()); + let target = target.unwrap(); + let loc = tcx.codegen_span_option(span); + + let msg = "condition is satisfiable"; + + Stmt::block( + vec![ + tcx.codegen_cover(cond, &msg, span), + Stmt::goto(tcx.current_fn().find_label(&target), loc), + ], + loc, + ) + } +} + struct ExpectFail; impl<'tcx> GotocHook<'tcx> for ExpectFail { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { @@ -369,6 +401,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_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 3a105f9c5937..6d8fc8c8f985 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -429,7 +429,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 +497,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 +527,21 @@ fn update_properties_with_reach_status( properties } +/// Flip the results of cover properties (SUCCESS -> FAILURE and FAILURE -> +/// SUCCESS) since we encode cover(cond) as assert(!cond), so if the assertion +/// fails, then the cover property is satisfied and vice versa +fn update_results_of_cover_checks(mut properties: Vec) -> Vec { + for prop in properties.iter_mut() { + if prop.property_class() == "cover" { + if prop.status == CheckStatus::Success { + prop.status = CheckStatus::Failure; + } else if prop.status == CheckStatus::Failure { + prop.status = CheckStatus::Success; + } + } + } + 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..6d1c5bc81f09 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -64,6 +64,37 @@ pub const fn assert(_cond: bool, _msg: &'static str) { } } +/// Check if a condition is satisfiable at a specific location in the code. +/// +/// # Example 1: +/// +/// ```rust +/// let mut set: BTreeSet = BTreeSet::new(); +/// for i in 0..5 { +/// set.insert(kani::any()); +/// } +/// // check if the set can end up with a single element (if all the elements +/// // inserted were the same) +/// kani::cover(set.len() == 1); +/// ``` +/// +/// # Example 2: +/// +/// ```rust +/// let (x, y) = ... +/// if x > y { +/// ... +/// } else if x < y { +/// ... +/// } else { +/// // check if it's possible for `x` and `y` to be equal +/// kani::cover(true); +/// } +/// Verification fails if there is no execution that would satisfy the condition +#[inline(never)] +#[rustc_diagnostic_item = "KaniCover"] +pub fn cover(_cond: bool) {} + /// 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. /// diff --git a/tests/expected/cover-fail/expected b/tests/expected/cover-fail/expected new file mode 100644 index 000000000000..de8933a96a8a --- /dev/null +++ b/tests/expected/cover-fail/expected @@ -0,0 +1,8 @@ +Status: FAILURE\ +Description: "condition is satisfiable"\ +main.rs:29:23 in function cover_overconstrained + + +Failed Checks: condition is satisfiable + +VERIFICATION:- FAILED diff --git a/tests/expected/cover-fail/main.rs b/tests/expected/cover-fail/main.rs new file mode 100644 index 000000000000..94feaaf3e94a --- /dev/null +++ b/tests/expected/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(true), + _ => {} + } +} diff --git a/tests/expected/cover-pass/expected b/tests/expected/cover-pass/expected new file mode 100644 index 000000000000..2f6cee2ae5df --- /dev/null +++ b/tests/expected/cover-pass/expected @@ -0,0 +1,9 @@ +Status: SUCCESS\ +Description: "condition is satisfiable"\ +main.rs:12:5 in function main + +Status: SUCCESS\ +Description: "condition is satisfiable"\ +main.rs:13:5 in function main + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/cover-pass/main.rs b/tests/expected/cover-pass/main.rs new file mode 100644 index 000000000000..6883441d363d --- /dev/null +++ b/tests/expected/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-undetermined/expected b/tests/expected/cover-undetermined/expected new file mode 100644 index 000000000000..aafed6733fc3 --- /dev/null +++ b/tests/expected/cover-undetermined/expected @@ -0,0 +1,9 @@ +Status: UNDETERMINED\ +Description: "condition is satisfiable"\ +main.rs:15:5 in function cover_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-undetermined/main.rs b/tests/expected/cover-undetermined/main.rs new file mode 100644 index 000000000000..f87c254f0482 --- /dev/null +++ b/tests/expected/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_fail.rs b/tests/kani/Cover/simp_fail.rs new file mode 100644 index 000000000000..7f042f6cef3f --- /dev/null +++ b/tests/kani/Cover/simp_fail.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-verify-fail + +/// A simple cover statement that should fail + +#[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); +} diff --git a/tests/kani/Cover/simp_pass.rs b/tests/kani/Cover/simp_pass.rs new file mode 100644 index 000000000000..38f6affacf21 --- /dev/null +++ b/tests/kani/Cover/simp_pass.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); +} From a87c74cdbd62324853535e9fc060a3952973f99b Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 16 Dec 2022 13:53:16 -0800 Subject: [PATCH 2/3] Address PR comments --- .../codegen_cprover_gotoc/overrides/hooks.rs | 8 +++++ kani-driver/src/cbmc_property_renderer.rs | 33 +++++++++++-------- library/kani/src/lib.rs | 11 +++++++ tests/expected/cover/cover-fail/expected | 2 +- tests/expected/cover/cover-message/expected | 2 +- tests/expected/cover/cover-pass/expected | 2 +- .../cover/cover-undetermined/expected | 2 +- 7 files changed, 42 insertions(+), 18 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 3ff90c38039e..d4f2c4e08309 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -46,6 +46,14 @@ 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 +/// https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0003-cover-statement.md +/// for more details. struct Cover; impl<'tcx> GotocHook<'tcx> for Cover { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index c1a4ab594838..81bf7a411d5c 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -231,13 +231,18 @@ 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 @@ -260,21 +265,21 @@ 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 => { if prop.is_cover_property() { number_covers_undetermined += 1; } else { - number_tests_undetermined += 1; + number_checks_undetermined += 1; } } CheckStatus::Unreachable => { if prop.is_cover_property() { number_covers_unreachable += 1; } else { - number_tests_unreachable += 1; + number_checks_unreachable += 1; } } CheckStatus::Satisfied => { @@ -320,16 +325,16 @@ pub fn format_result(properties: &Vec, show_checks: bool) -> String { let number_properties = properties.len() - number_cover_properties; - let summary = format!("\n ** {number_tests_failed} of {} failed", number_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() { @@ -342,7 +347,7 @@ pub fn format_result(properties: &Vec, show_checks: bool) -> String { if number_cover_properties > 0 { // Print a summary line for cover properties let summary = format!( - "\n ** {number_covers_unsatisfiable} of {} cover properties unsatisfiable", + "\n ** {number_covers_satisfied} of {} cover properties satisfied", number_cover_properties ); result_str.push_str(&summary); @@ -370,7 +375,7 @@ pub fn format_result(properties: &Vec, show_checks: bool) -> String { } 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); @@ -588,7 +593,7 @@ fn update_properties_with_reach_status( /// - FAILURE -> SATISFIED fn update_results_of_cover_checks(mut properties: Vec) -> Vec { for prop in properties.iter_mut() { - if prop.property_class() == "cover" { + if prop.is_cover_property() { if prop.status == CheckStatus::Success { prop.status = CheckStatus::Unsatisfiable; } else if prop.status == CheckStatus::Failure { diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 083101ae0acd..b5b96c5b6fd7 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -71,6 +71,17 @@ pub const fn assert(_cond: bool, _msg: &'static str) { /// ```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 [`kani::cover!`] macro. The macro is more +/// convenient to use. +/// #[inline(never)] #[rustc_diagnostic_item = "KaniCover"] pub fn cover(_cond: bool, _msg: &'static str) {} diff --git a/tests/expected/cover/cover-fail/expected b/tests/expected/cover/cover-fail/expected index 0f501cdc1acb..49ffe167a124 100644 --- a/tests/expected/cover/cover-fail/expected +++ b/tests/expected/cover/cover-fail/expected @@ -2,6 +2,6 @@ Status: UNSATISFIABLE\ Description: "cover location"\ main.rs:29:23 in function cover_overconstrained - ** 1 of 1 cover properties unsatisfiable + ** 0 of 1 cover properties satisfied VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/cover/cover-message/expected b/tests/expected/cover/cover-message/expected index 9c5d7b9c9cdf..e229cf8167ae 100644 --- a/tests/expected/cover/cover-message/expected +++ b/tests/expected/cover/cover-message/expected @@ -10,6 +10,6 @@ Status: UNSATISFIABLE\ Description: "y may be greater than 10"\ main.rs:16:18 in function cover_match - ** 1 of 3 cover properties unsatisfiable + ** 2 of 3 cover properties satisfied VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/cover/cover-pass/expected b/tests/expected/cover/cover-pass/expected index e2cb5ba5aafb..59b85ec64ee1 100644 --- a/tests/expected/cover/cover-pass/expected +++ b/tests/expected/cover/cover-pass/expected @@ -6,6 +6,6 @@ Status: SATISFIED\ Description: "cover condition: sorted != arr"\ main.rs:13:5 in function cover_sorted - ** 0 of 2 cover properties unsatisfiable + ** 2 of 2 cover properties satisfied VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/cover/cover-undetermined/expected b/tests/expected/cover/cover-undetermined/expected index 2b9a60a57af7..dcbc9fddb12e 100644 --- a/tests/expected/cover/cover-undetermined/expected +++ b/tests/expected/cover/cover-undetermined/expected @@ -2,7 +2,7 @@ Status: UNDETERMINED\ Description: "cover condition: sum == 10"\ main.rs:15:5 in function cover_undetermined - ** 0 of 1 cover properties unsatisfiable (1 undetermined) + ** 0 of 1 cover properties satisfied (1 undetermined) Failed Checks: unwinding assertion loop 0 From 56eeca2e019aa91ac06812559671e9eece7d7967 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 16 Dec 2022 14:33:23 -0800 Subject: [PATCH 3/3] Fix documentation comments --- kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs | 2 +- library/kani/src/lib.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index d4f2c4e08309..f51eea38cbd8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -52,7 +52,7 @@ fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool { /// 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 -/// https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0003-cover-statement.md +/// /// for more details. struct Cover; impl<'tcx> GotocHook<'tcx> for Cover { diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index b5b96c5b6fd7..2e63ba41cc35 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -79,7 +79,7 @@ pub const fn assert(_cond: bool, _msg: &'static str) { /// - 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 [`kani::cover!`] macro. The macro is more +/// This function is called by the [`cover!`] macro. The macro is more /// convenient to use. /// #[inline(never)]