Add implementation for the #[kani::should_panic] attribute

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,35 @@ 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,
 }
 
+/// Classifies all possible outcomes when `#[kani::should_panic]` is being
+/// applied to the harness
+#[derive(Clone, Copy, Debug)]
+pub enum PanicOutcome {
+    // No failures were found
+    Zero,
+    // Found one or more panic-related failures
+    OneOrMore,
+    // Found other failures that weren't panic-related
+    OtherFailures,
+}
+
 /// 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,
+    /// Indicates if verification results are expected to contain panic-related failures and,
+    /// if they are, whether all failures in the results were panic-related or not.
+    ///  * `None` means panic-related failures aren't expected.
+    ///  * `Some(outcome)` means panic-related failures are expected, and `outcome`
+    ///     represents information about panic-related failures in the results.
+    pub should_panic: Option<PanicOutcome>,
     /// 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 +94,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 +252,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, should_panic) =
+                verification_outcome_from_properties(&results, should_panic);
             VerificationResult {
-                status: determine_status_from_properties(&results),
+                status,
+                should_panic,
                 messages: Some(items),
                 results: Ok(results),
                 runtime,
@@ -250,6 +275,7 @@ impl VerificationResult {
             // We never got results from CBMC - something went wrong (e.g. crash) so it's failure
             VerificationResult {
                 status: VerificationStatus::Failure,
+                should_panic: None,
                 messages: Some(items),
                 results: Err(output.process_status),
                 runtime,
@@ -261,6 +287,7 @@ impl VerificationResult {
     pub fn mock_success() -> VerificationResult {
         VerificationResult {
             status: VerificationStatus::Success,
+            should_panic: None,
             messages: None,
             results: Ok(vec![]),
             runtime: Duration::from_secs(0),
@@ -271,6 +298,7 @@ impl VerificationResult {
     fn mock_failure() -> VerificationResult {
         VerificationResult {
             status: VerificationStatus::Failure,
+            should_panic: None,
             messages: None,
             // on failure, exit codes in theory might be used,
             // but `mock_failure` should never be used in a context where they will,
@@ -284,8 +312,10 @@ impl VerificationResult {
     pub fn render(&self, output_format: &OutputFormat) -> String {
         match &self.results {
             Ok(results) => {
+                let status = self.status;
+                let should_panic = self.should_panic;
                 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, show_checks);
                 writeln!(result, "Verification Time: {}s", self.runtime.as_secs_f32()).unwrap();
                 result
             }
@@ -310,13 +340,30 @@ 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, Option<PanicOutcome>) {
+    let failed_properties: Vec<&Property> =
+        properties.iter().filter(|prop| prop.status == CheckStatus::Failure).collect();
+    if should_panic {
+        // Return `FAILURE` if there isn't at least one failed property
+        if failed_properties.is_empty() {
+            return (VerificationStatus::Failure, Some(PanicOutcome::Zero));
+        }
+        // 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 {
+            (VerificationStatus::Success, Some(PanicOutcome::OneOrMore))
+        } else {
+            (VerificationStatus::Failure, Some(PanicOutcome::OtherFailures))
+        }
+    } else if failed_properties.is_empty() {
+        (VerificationStatus::Success, None)
     } else {
-        VerificationStatus::Failure
+        (VerificationStatus::Failure, None)
     }
 }
 

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::{PanicOutcome, VerificationStatus};
 use crate::cbmc_output_parser::{CheckStatus, ParserItem, Property, TraceItem};
 use console::style;
 use once_cell::sync::Lazy;
@@ -241,7 +242,12 @@ 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: Option<PanicOutcome>,
+    show_checks: bool,
+) -> String {
     let mut result_str = String::new();
     let mut number_checks_failed = 0;
     let mut number_checks_unreachable = 0;
@@ -376,9 +382,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 panic_info = if let Some(panic_outcome) = should_panic {
+        match panic_outcome {
+            PanicOutcome::Zero => " (encountered no panics, but at least one was expected)",
+            PanicOutcome::OneOrMore => " (encountered one or more panics as expected)",
+            PanicOutcome::OtherFailures => {
+                " (encountered failures other than panics, which were unexpected)"
+            }
+        }
+    } else {
+        ""
+    };
+    let overall_result = format!("\nVERIFICATION:- {verification_result}{panic_info}\n");
     result_str.push_str(&overall_result);
 
     // Ideally, we should generate two `ParserItem::Message` and push them

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

@@ -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 for now");
+    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/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,2 @@
+ ** 0 of 0 failed
+VERIFICATION:- FAILED (encountered no panics, but at least one was expected)

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

@@ -0,0 +1,9 @@
+// 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() {}

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();
+            ()
+        }
+    }
+}

tests/ui/should-panic-attribute/with-args/expected

@@ -0,0 +1,3 @@
+error: custom attribute panicked
+help: message: `#[kani::should_panic]` does not take any arguments for now
+error: aborting due to previous error

tests/ui/should-panic-attribute/with-args/test.rs

@@ -0,0 +1,8 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Checks that `#[kani::should_panic]` doesn't accept arguments.
+
+#[kani::proof]
+#[kani::should_panic(arg)]
+fn check() {}