Add implementation for the #[kani::should_panic] attribute (rust-lang#2315)

Author: adpaco-aws

kani-compiler/src/kani_middle/attributes.rs

@@ -23,6 +23,7 @@ use super::resolve;
 #[strum(serialize_all = "snake_case")]
 enum KaniAttributeKind {
     Proof,
+    ShouldPanic,
     Solver,
     Stub,
     Unwind,
@@ -96,6 +97,10 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option<HarnessA
             HarnessAttributes::default(),
             |mut harness, (kind, attributes)| {
                 match kind {
+                    KaniAttributeKind::ShouldPanic => {
+                        expect_single(tcx, kind, &attributes);
+                        harness.should_panic = true
+                    }
                     KaniAttributeKind::Solver => {
                         // Make sure the solver is not already set
                         harness.solver = parse_solver(tcx, expect_single(tcx, kind, &attributes));

kani-driver/src/call_cbmc.rs

@@ -16,17 +16,31 @@ use crate::cbmc_output_parser::{
 use crate::cbmc_property_renderer::{format_result, kani_cbmc_output_filter};
 use crate::session::KaniSession;
 
-#[derive(Debug, PartialEq, Eq)]
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
 pub enum VerificationStatus {
     Success,
     Failure,
 }
 
+/// Represents failed properties in three different categories.
+/// This simplifies the process to determine and format verification results.
+#[derive(Clone, Copy, Debug)]
+pub enum FailedProperties {
+    // No failures
+    None,
+    // One or more panic-related failures
+    PanicsOnly,
+    // One or more failures that aren't panic-related
+    Other,
+}
+
 /// Our (kani-driver) notions of CBMC results.
 #[derive(Debug)]
 pub struct VerificationResult {
     /// Whether verification should be considered to have succeeded, or have failed.
     pub status: VerificationStatus,
+    /// The compact representation for failed properties
+    pub failed_properties: FailedProperties,
     /// The parsed output, message by message, of CBMC. However, the `Result` message has been
     /// removed and is available in `results` instead.
     pub messages: Option<Vec<ParserItem>>,
@@ -76,7 +90,7 @@ impl KaniSession {
                 )
             })?;
 
-            VerificationResult::from(output, start_time)
+            VerificationResult::from(output, harness.attributes.should_panic, start_time)
         };
 
         self.gen_and_add_concrete_playback(harness, &mut verification_results)?;
@@ -234,13 +248,20 @@ impl VerificationResult {
     ///       (CBMC will regularly report "failure" but that's just our cover checks.)
     ///   2. Positively checking for the presence of results.
     ///       (Do not mistake lack of results for success: report it as failure.)
-    fn from(output: VerificationOutput, start_time: Instant) -> VerificationResult {
+    fn from(
+        output: VerificationOutput,
+        should_panic: bool,
+        start_time: Instant,
+    ) -> VerificationResult {
         let runtime = start_time.elapsed();
         let (items, results) = extract_results(output.processed_items);
 
         if let Some(results) = results {
+            let (status, failed_properties) =
+                verification_outcome_from_properties(&results, should_panic);
             VerificationResult {
-                status: determine_status_from_properties(&results),
+                status,
+                failed_properties,
                 messages: Some(items),
                 results: Ok(results),
                 runtime,
@@ -250,6 +271,7 @@ impl VerificationResult {
             // We never got results from CBMC - something went wrong (e.g. crash) so it's failure
             VerificationResult {
                 status: VerificationStatus::Failure,
+                failed_properties: FailedProperties::Other,
                 messages: Some(items),
                 results: Err(output.process_status),
                 runtime,
@@ -261,6 +283,7 @@ impl VerificationResult {
     pub fn mock_success() -> VerificationResult {
         VerificationResult {
             status: VerificationStatus::Success,
+            failed_properties: FailedProperties::None,
             messages: None,
             results: Ok(vec![]),
             runtime: Duration::from_secs(0),
@@ -271,6 +294,7 @@ impl VerificationResult {
     fn mock_failure() -> VerificationResult {
         VerificationResult {
             status: VerificationStatus::Failure,
+            failed_properties: FailedProperties::Other,
             messages: None,
             // on failure, exit codes in theory might be used,
             // but `mock_failure` should never be used in a context where they will,
@@ -281,11 +305,14 @@ impl VerificationResult {
         }
     }
 
-    pub fn render(&self, output_format: &OutputFormat) -> String {
+    pub fn render(&self, output_format: &OutputFormat, should_panic: bool) -> String {
         match &self.results {
             Ok(results) => {
+                let status = self.status;
+                let failed_properties = self.failed_properties;
                 let show_checks = matches!(output_format, OutputFormat::Regular);
-                let mut result = format_result(results, show_checks);
+                let mut result =
+                    format_result(results, status, should_panic, failed_properties, show_checks);
                 writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap();
                 result
             }
@@ -310,13 +337,42 @@ impl VerificationResult {
 }
 
 /// We decide if verification succeeded based on properties, not (typically) on exit code
-fn determine_status_from_properties(properties: &[Property]) -> VerificationStatus {
-    let number_failed_properties =
-        properties.iter().filter(|prop| prop.status == CheckStatus::Failure).count();
-    if number_failed_properties == 0 {
-        VerificationStatus::Success
+fn verification_outcome_from_properties(
+    properties: &[Property],
+    should_panic: bool,
+) -> (VerificationStatus, FailedProperties) {
+    let failed_properties = determine_failed_properties(properties);
+    let status = if should_panic {
+        match failed_properties {
+            FailedProperties::None | FailedProperties::Other => VerificationStatus::Failure,
+            FailedProperties::PanicsOnly => VerificationStatus::Success,
+        }
     } else {
-        VerificationStatus::Failure
+        match failed_properties {
+            FailedProperties::None => VerificationStatus::Success,
+            FailedProperties::PanicsOnly | FailedProperties::Other => VerificationStatus::Failure,
+        }
+    };
+    (status, failed_properties)
+}
+
+/// Determines the `FailedProperties` variant that corresponds to an array of properties
+fn determine_failed_properties(properties: &[Property]) -> FailedProperties {
+    let failed_properties: Vec<&Property> =
+        properties.iter().filter(|prop| prop.status == CheckStatus::Failure).collect();
+    // Return `FAILURE` if there isn't at least one failed property
+    if failed_properties.is_empty() {
+        FailedProperties::None
+    } else {
+        // Check if all failed properties correspond to the `assertion` class.
+        // Note: Panics caused by `panic!` and `assert!` fall into this class.
+        let all_failed_checks_are_panics =
+            failed_properties.iter().all(|prop| prop.property_class() == "assertion");
+        if all_failed_checks_are_panics {
+            FailedProperties::PanicsOnly
+        } else {
+            FailedProperties::Other
+        }
     }
 }
 

kani-driver/src/cbmc_property_renderer.rs

@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::args::OutputFormat;
+use crate::call_cbmc::{FailedProperties, VerificationStatus};
 use crate::cbmc_output_parser::{CheckStatus, ParserItem, Property, TraceItem};
 use console::style;
 use once_cell::sync::Lazy;
@@ -241,7 +242,13 @@ fn format_item_terse(_item: &ParserItem) -> Option<String> {
 ///
 /// TODO: We could `write!` to `result_str` instead
 /// <https://github.com/model-checking/kani/issues/1480>
-pub fn format_result(properties: &Vec<Property>, show_checks: bool) -> String {
+pub fn format_result(
+    properties: &Vec<Property>,
+    status: VerificationStatus,
+    should_panic: bool,
+    failed_properties: FailedProperties,
+    show_checks: bool,
+) -> String {
     let mut result_str = String::new();
     let mut number_checks_failed = 0;
     let mut number_checks_unreachable = 0;
@@ -376,9 +383,23 @@ pub fn format_result(properties: &Vec<Property>, show_checks: bool) -> String {
         result_str.push_str(&failure_message);
     }
 
-    let verification_result =
-        if number_checks_failed == 0 { style("SUCCESSFUL").green() } else { style("FAILED").red() };
-    let overall_result = format!("\nVERIFICATION:- {verification_result}\n");
+    let verification_result = if status == VerificationStatus::Success {
+        style("SUCCESSFUL").green()
+    } else {
+        style("FAILED").red()
+    };
+    let should_panic_info = if should_panic {
+        match failed_properties {
+            FailedProperties::None => " (encountered no panics, but at least one was expected)",
+            FailedProperties::PanicsOnly => " (encountered one or more panics as expected)",
+            FailedProperties::Other => {
+                " (encountered failures other than panics, which were unexpected)"
+            }
+        }
+    } else {
+        ""
+    };
+    let overall_result = format!("\nVERIFICATION:- {verification_result}{should_panic_info}\n");
     result_str.push_str(&overall_result);
 
     // Ideally, we should generate two `ParserItem::Message` and push them

kani-driver/src/harness_runner.rs

@@ -101,7 +101,10 @@ impl KaniSession {
             // When quiet, we don't want to print anything at all.
             // When output is old, we also don't have real results to print.
             if !self.args.quiet && self.args.output_format != OutputFormat::Old {
-                println!("{}", result.render(&self.args.output_format));
+                println!(
+                    "{}",
+                    result.render(&self.args.output_format, harness.attributes.should_panic)
+                );
             }
 
             Ok(result)

kani_metadata/src/harness.rs

@@ -31,6 +31,8 @@ pub struct HarnessMetadata {
 pub struct HarnessAttributes {
     /// Whether the harness has been annotated with proof.
     pub proof: bool,
+    /// Whether the harness is expected to panic or not.
+    pub should_panic: bool,
     /// Optional data to store solver.
     pub solver: Option<CbmcSolver>,
     /// Optional data to store unwind value.

library/kani_macros/src/lib.rs

@@ -52,7 +52,7 @@ pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
         #[kanitool::proof]
     );
 
-    assert!(attr.is_empty(), "#[kani::proof] does not take any arguments for now");
+    assert!(attr.is_empty(), "#[kani::proof] does not take any arguments currently");
 
     if sig.asyncness.is_none() {
         // Adds `#[kanitool::proof]` and other attributes
@@ -98,6 +98,25 @@ pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
     }
 }
 
+#[cfg(not(kani))]
+#[proc_macro_attribute]
+pub fn should_panic(_attr: TokenStream, item: TokenStream) -> TokenStream {
+    // No-op in non-kani mode
+    item
+}
+
+#[cfg(kani)]
+#[proc_macro_attribute]
+pub fn should_panic(attr: TokenStream, item: TokenStream) -> TokenStream {
+    assert!(attr.is_empty(), "`#[kani::should_panic]` does not take any arguments currently");
+    let mut result = TokenStream::new();
+    let insert_string = "#[kanitool::should_panic]";
+    result.extend(insert_string.parse::<TokenStream>().unwrap());
+
+    result.extend(item);
+    result
+}
+
 #[cfg(not(kani))]
 #[proc_macro_attribute]
 pub fn unwind(_attr: TokenStream, item: TokenStream) -> TokenStream {

tests/expected/async_proof/expected

@@ -1,5 +1,5 @@
 error: custom attribute panicked
-#[kani::proof] does not take any arguments for now
+#[kani::proof] does not take any arguments currently
 
 error: custom attribute panicked
 #[kani::proof] cannot be applied to async functions that take inputs for now

tests/ui/should-panic-attribute/expected-panics/expected

@@ -0,0 +1,4 @@
+ ** 2 of 2 failed\
+Failed Checks: panicked on the `if` branch!
+Failed Checks: panicked on the `else` branch!
+VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)

tests/ui/should-panic-attribute/expected-panics/test.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that verfication passes when `#[kani::should_panic]` is used and all
+//! failures encountered are panics.
+
+#[kani::proof]
+#[kani::should_panic]
+fn check() {
+    if kani::any() {
+        panic!("panicked on the `if` branch!");
+    } else {
+        panic!("panicked on the `else` branch!");
+    }
+}

tests/ui/should-panic-attribute/multiple-attrs/expected

@@ -0,0 +1,2 @@
+error: only one '#[kani::should_panic]' attribute is allowed per harness
+error: aborting due to previous error

tests/ui/should-panic-attribute/multiple-attrs/test.rs

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that `#[kani::should_panic]` can only be used once.
+
+#[kani::proof]
+#[kani::should_panic]
+#[kani::should_panic]
+fn check() {}

tests/ui/should-panic-attribute/multiple-harnesses-panic/expected

@@ -0,0 +1 @@
+Complete - 3 successfully verified harnesses, 0 failures, 3 total.

tests/ui/should-panic-attribute/multiple-harnesses-panic/test.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that the verification summary printed at the end considers all
+//! harnesses as "successfully verified".
+
+#[kani::proof]
+#[kani::should_panic]
+fn harness1() {
+    panic!("panicked on `harness1`!");
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn harness2() {
+    panic!("panicked on `harness2`!");
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn harness3() {
+    panic!("panicked on `harness3`!");
+}

tests/ui/should-panic-attribute/no-panics/expected

@@ -0,0 +1,4 @@
+- Status: SUCCESS\
+- Description: "assertion failed: 1 + 1 == 2"
+ ** 0 of 1 failed
+VERIFICATION:- FAILED (encountered no panics, but at least one was expected)

tests/ui/should-panic-attribute/no-panics/test.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that verfication fails when `#[kani::should_panic]` is used and no
+//! panics are encountered.
+
+#[kani::proof]
+#[kani::should_panic]
+fn check() {
+    assert!(1 + 1 == 2);
+}

tests/ui/should-panic-attribute/unexpected-failures/expected

@@ -0,0 +1,8 @@
+overflow.undefined-shift.1\
+- Status: FAILURE\
+- Description: "shift distance too large"
+Failed Checks: attempt to shift left with overflow
+Failed Checks: panicked on the `1` arm!
+Failed Checks: panicked on the `0` arm!
+Failed Checks: shift distance too large
+VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)

tests/ui/should-panic-attribute/unexpected-failures/test.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that verfication fails when `#[kani::should_panic]` is used but not
+//! all failures encountered are panics.
+
+fn trigger_overflow() {
+    let x: u32 = kani::any();
+    let _ = 42 << x;
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check() {
+    match kani::any() {
+        0 => panic!("panicked on the `0` arm!"),
+        1 => panic!("panicked on the `1` arm!"),
+        _ => {
+            trigger_overflow();
+            ()
+        }
+    }
+}