Fix panic warning and add arbitrary Duration (#2820)

Add an Arbitrary implementation for Duration and also fix unused
variable warnings when panic message uses a variable in its format
string.

library/kani/src/arbitrary.rs

@@ -170,3 +170,12 @@ where
  Box::new(T::any())
  }
 }
+
+impl Arbitrary for std::time::Duration {
+ fn any() -> Self {
+ const NANOS_PER_SEC: u32 = 1_000_000_000;
+ let nanos = u32::any();
+ crate::assume(nanos < NANOS_PER_SEC);
+ std::time::Duration::new(u64::any(), nanos)
+ }
+}

library/std/src/lib.rs

@@ -180,7 +180,10 @@ macro_rules! panic {
  // The argument is a literal that represents the error message, i.e.:
  // `panic!("Error message")`
  ($msg:literal $(,)?) => ({
- kani::panic(concat!($msg));
+ if false {
+ __kani__workaround_core_assert!(true, $msg);
+ }
+ kani::panic(concat!($msg))
  });
  // The argument is an expression, such as a variable.
  // ```

tests/expected/arbitrary/duration.expected

@@ -0,0 +1,25 @@
+Checking harness check_limits...
+
+Status: SATISFIED\
+Description: "Zero Duration"
+
+Status: SATISFIED\
+Description: "MAX Duration"
+
+Status: SATISFIED\
+Description: "Max Secs"
+
+Status: SATISFIED\
+Description: "Max millis"
+
+Status: SATISFIED\
+Description: "Max micros"
+
+Status: SATISFIED\
+Description: "Max nanos"
+
+Status: SUCCESS\
+Description: ""Is Zero""
+
+6 of 6 cover properties satisfied
+1 successfully verified harnesses, 0 failures

tests/expected/arbitrary/duration.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Ensure that kani::any can be used with Duration.
+
+use std::time::Duration;
+
+#[kani::proof]
+fn check_limits() {
+ let any_duration: Duration = kani::any();
+ kani::cover!(any_duration == Duration::ZERO, "Zero Duration");
+ kani::cover!(any_duration == Duration::MAX, "MAX Duration");
+ kani::cover!(any_duration == Duration::from_secs(u64::MAX), "Max Secs");
+ kani::cover!(any_duration == Duration::from_millis(u64::MAX), "Max millis");
+ kani::cover!(any_duration == Duration::from_micros(u64::MAX), "Max micros");
+ kani::cover!(any_duration == Duration::from_nanos(u64::MAX), "Max nanos");
+
+ assert_eq!(any_duration.is_zero(), any_duration == Duration::ZERO, "Is Zero");
+}

tests/perf/kani-lib/arbitrary/src/check_arbitrary.rs

@@ -79,3 +79,14 @@ fn check_any_bool() {
 
  assert!(!all_true || !all_false);
 }
+
+#[kani::proof]
+fn check_duration() {
+ let durations: [Duration; 10] = kani::any();
+ let (max, zero): (usize, usize) = kani::any();
+ kani::assume(max < durations.len() && zero < durations.len());
+ kani::assume(durations[max] == Duration::MAX);
+ kani::assume(durations[zero] == Duration::ZERO);
+ assert_eq!(durations.iter().min(), Some(&Duration::ZERO));
+ assert_eq!(durations.iter().max(), Some(&Duration::MAX));
+}

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

@@ -1,6 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-
+//
+// compile-flags: -Copt-level=1
 //! Checks that verfication passes when `#[kani::should_panic]` is used and all
 //! failures encountered are panics.
 

tests/ui/std-override/format_panic.expected

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

tests/ui/std-override/format_panic.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Ensure Kani override doesn't result in extra warnings which could block compilation when
+//! users have strict lints.
+
+#![deny(unused_variables)]
+
+#[kani::proof]
+pub fn check_panic_format() {
+ let val: bool = kani::any();
+ panic!("Invalid value {val}");
+}
+
+#[kani::proof]
+pub fn check_panic_format_expr() {
+ let val: bool = kani::any();
+ panic!("Invalid value {}", !val);
+}