Write contracts + pre/post conditions for all unsafe methods in duration (#136)

sgpthomas · cvick32 · celinval · web-flow · commit 8a248d92fcf8 · 2024-12-10T20:57:07.000Z
Resolves #72 We added invariants for Nanoseconds and Duration to match the safety conditions for those types. We add safety requirements to the following methods: - `new`, `from_secs`, `from_millis`, `from_micros`, `from_nanos`, `as_secs`, `as_millis`, `as_micros`, `as_nanos`, `subsec_millis`, `subsec_micros`, `subsec_nanos`, `checked_add`, `checked_sub`, `checked_mul`, `checked_div` We additionally add correctness conditions to the following methods: - `from_secs`, `as_secs`, `subsec_millis`, `subsec_micros`, `subsec_nanos`, `as_millis`, `as_micros` Support for `kani::Invariant` depends on #87. For the interim we implemented a proxy trait `TempInvariant` that exposes the same `is_safe` method. We will update this once #87 is merged. While the safety check for `Duration::as_nanos()` succeeds, we ran into timeouts for `Duration::as_nanos()` when we tried to use a correctness contract and we're looking for advice on how to speed up that verification time. We were able to prove it for `u16::MAX`, but hit timeouts for larger numbers. We are unsure if the pre-conditions for `Duration::new()` are acceptable because they limit the range of values that you can call `Duration::new()` with. However, we think it's reasonable since we limit the values to values that don't panic. Let us know if this is a thing that we should change. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Cole Vick <cole.d.vick@gmail.com> Co-authored-by: Celina G. Val <celinval@amazon.com> Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
diff --git a/library/core/src/time.rs b/library/core/src/time.rs
@@ -19,10 +19,16 @@
 //! assert_eq!(total, Duration::new(10, 7));
 //! ```
 
+use safety::{ensures, Invariant};
 use crate::fmt;
 use crate::iter::Sum;
 use crate::ops::{Add, AddAssign, Div, DivAssign, Mul, MulAssign, Sub, SubAssign};
 
+#[cfg(kani)]
+use crate::kani;
+
+use crate::ub_checks::Invariant;
+
 const NANOS_PER_SEC: u32 = 1_000_000_000;
 const NANOS_PER_MILLI: u32 = 1_000_000;
 const NANOS_PER_MICRO: u32 = 1_000;
@@ -43,6 +49,12 @@ const DAYS_PER_WEEK: u64 = 7;
 #[rustc_layout_scalar_valid_range_end(999_999_999)]
 struct Nanoseconds(u32);
 
+impl Invariant for Nanoseconds {
+    fn is_safe(&self) -> bool {
+        self.0 < NANOS_PER_SEC
+    }
+}
+
 impl Nanoseconds {
     // SAFETY: 0 is within the valid range
     const ZERO: Self = unsafe { Nanoseconds(0) };
@@ -95,6 +107,7 @@ impl Default for Nanoseconds {
 #[stable(feature = "duration", since = "1.3.0")]
 #[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
 #[cfg_attr(not(test), rustc_diagnostic_item = "Duration")]
+#[derive(Invariant)]
 pub struct Duration {
     secs: u64,
     nanos: Nanoseconds, // Always 0 <= nanos < NANOS_PER_SEC
@@ -208,6 +221,7 @@ impl Duration {
     #[inline]
     #[must_use]
     #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")]
+    #[ensures(|duration| duration.is_safe())]
     pub const fn new(secs: u64, nanos: u32) -> Duration {
         if nanos < NANOS_PER_SEC {
             // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range
@@ -238,6 +252,8 @@ impl Duration {
     #[must_use]
     #[inline]
     #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")]
+    #[ensures(|duration| duration.is_safe())]
+    #[ensures(|duration| duration.secs == secs)]
     pub const fn from_secs(secs: u64) -> Duration {
         Duration { secs, nanos: Nanoseconds::ZERO }
     }
@@ -258,6 +274,7 @@ impl Duration {
     #[must_use]
     #[inline]
     #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")]
+    #[ensures(|duration| duration.is_safe())]
     pub const fn from_millis(millis: u64) -> Duration {
         let secs = millis / MILLIS_PER_SEC;
         let subsec_millis = (millis % MILLIS_PER_SEC) as u32;
@@ -284,6 +301,7 @@ impl Duration {
     #[must_use]
     #[inline]
     #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")]
+    #[ensures(|duration| duration.is_safe())]
     pub const fn from_micros(micros: u64) -> Duration {
         let secs = micros / MICROS_PER_SEC;
         let subsec_micros = (micros % MICROS_PER_SEC) as u32;
@@ -315,6 +333,7 @@ impl Duration {
     #[must_use]
     #[inline]
     #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")]
+    #[ensures(|duration| duration.is_safe())]
     pub const fn from_nanos(nanos: u64) -> Duration {
         const NANOS_PER_SEC: u64 = self::NANOS_PER_SEC as u64;
         let secs = nanos / NANOS_PER_SEC;
@@ -485,6 +504,7 @@ impl Duration {
     #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")]
     #[must_use]
     #[inline]
+    #[ensures(|secs| *secs == self.secs)]
     pub const fn as_secs(&self) -> u64 {
         self.secs
     }
@@ -508,6 +528,7 @@ impl Duration {
     #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")]
     #[must_use]
     #[inline]
+    #[ensures(|ms| *ms == self.nanos.0 / NANOS_PER_MILLI)]
     pub const fn subsec_millis(&self) -> u32 {
         self.nanos.0 / NANOS_PER_MILLI
     }
@@ -531,6 +552,7 @@ impl Duration {
     #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")]
     #[must_use]
     #[inline]
+    #[ensures(|ms| *ms == self.nanos.0 / NANOS_PER_MICRO)]
     pub const fn subsec_micros(&self) -> u32 {
         self.nanos.0 / NANOS_PER_MICRO
     }
@@ -554,6 +576,7 @@ impl Duration {
     #[rustc_const_stable(feature = "duration_consts", since = "1.32.0")]
     #[must_use]
     #[inline]
+    #[ensures(|nanos| *nanos == self.nanos.0)]
     pub const fn subsec_nanos(&self) -> u32 {
         self.nanos.0
     }
@@ -572,6 +595,7 @@ impl Duration {
     #[rustc_const_stable(feature = "duration_as_u128", since = "1.33.0")]
     #[must_use]
     #[inline]
+    #[ensures(|ms| *ms == self.secs as u128 * MILLIS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MILLI) as u128)]
     pub const fn as_millis(&self) -> u128 {
         self.secs as u128 * MILLIS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MILLI) as u128
     }
@@ -590,6 +614,7 @@ impl Duration {
     #[rustc_const_stable(feature = "duration_as_u128", since = "1.33.0")]
     #[must_use]
     #[inline]
+    #[ensures(|ms| *ms == self.secs as u128 * MICROS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MICRO) as u128)]
     pub const fn as_micros(&self) -> u128 {
         self.secs as u128 * MICROS_PER_SEC as u128 + (self.nanos.0 / NANOS_PER_MICRO) as u128
     }
@@ -647,6 +672,7 @@ impl Duration {
                   without modifying the original"]
     #[inline]
     #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")]
+    #[ensures(|duration| duration.is_none() || duration.unwrap().is_safe())]
     pub const fn checked_add(self, rhs: Duration) -> Option<Duration> {
         if let Some(mut secs) = self.secs.checked_add(rhs.secs) {
             let mut nanos = self.nanos.0 + rhs.nanos.0;
@@ -705,6 +731,7 @@ impl Duration {
                   without modifying the original"]
     #[inline]
     #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")]
+    #[ensures(|duration| duration.is_none() || duration.unwrap().is_safe())]
     pub const fn checked_sub(self, rhs: Duration) -> Option<Duration> {
         if let Some(mut secs) = self.secs.checked_sub(rhs.secs) {
             let nanos = if self.nanos.0 >= rhs.nanos.0 {
@@ -761,6 +788,7 @@ impl Duration {
                   without modifying the original"]
     #[inline]
     #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")]
+    #[ensures(|duration| duration.is_none() || duration.unwrap().is_safe())]
     pub const fn checked_mul(self, rhs: u32) -> Option<Duration> {
         // Multiply nanoseconds as u64, because it cannot overflow that way.
         let total_nanos = self.nanos.0 as u64 * rhs as u64;
@@ -816,13 +844,15 @@ impl Duration {
     #[must_use = "this returns the result of the operation, \
                   without modifying the original"]
     #[inline]
+    #[ensures(|duration| rhs == 0 || duration.unwrap().is_safe())]
     #[rustc_const_stable(feature = "duration_consts_2", since = "1.58.0")]
     pub const fn checked_div(self, rhs: u32) -> Option<Duration> {
         if rhs != 0 {
             let (secs, extra_secs) = (self.secs / (rhs as u64), self.secs % (rhs as u64));
             let (mut nanos, extra_nanos) = (self.nanos.0 / rhs, self.nanos.0 % rhs);
             nanos +=
                 ((extra_secs * (NANOS_PER_SEC as u64) + extra_nanos as u64) / (rhs as u64)) as u32;
+            #[cfg(not(kani))]
             debug_assert!(nanos < NANOS_PER_SEC);
             Some(Duration::new(secs, nanos))
         } else {
@@ -1698,3 +1728,213 @@ impl Duration {
         )
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod duration_verify {
+    use crate::kani;
+    use super::*;
+
+    impl kani::Arbitrary for Duration {
+        fn any() -> Duration {
+            let secs = kani::any::<u64>();
+            let nanos = kani::any::<u32>();
+            Duration::new(secs, nanos)
+        }
+    }
+
+    fn safe_duration() -> Duration {
+        let secs = kani::any::<u64>();
+        let nanos = kani::any::<u32>();
+        kani::assume(nanos < NANOS_PER_SEC || secs.checked_add((nanos / NANOS_PER_SEC) as u64).is_some());
+        Duration::new(secs, nanos)
+    }
+
+    #[kani::proof_for_contract(Duration::new)]
+    fn duration_new() {
+        let _ = safe_duration();
+    }
+
+    #[kani::proof_for_contract(Duration::new)]
+    #[kani::should_panic]
+    fn duration_new_panics() {
+        let secs = kani::any::<u64>();
+        let nanos = kani::any::<u32>();
+        let _ = Duration::new(secs, nanos);
+    }
+
+    #[kani::proof_for_contract(Duration::from_secs)]
+    fn duration_from_secs() {
+        let secs = kani::any::<u64>();
+        let _ = Duration::from_secs(secs);
+    }
+
+    #[kani::proof_for_contract(Duration::from_millis)]
+    fn duration_from_millis() {
+        let ms = kani::any::<u64>();
+        let _ = Duration::from_millis(ms);
+    }
+
+    #[kani::proof_for_contract(Duration::from_micros)]
+    fn duration_from_micros() {
+        let micros = kani::any::<u64>();
+        let _ = Duration::from_micros(micros);
+    }
+
+    #[kani::proof_for_contract(Duration::from_nanos)]
+    fn duration_from_nanos() {
+        let nanos = kani::any::<u64>();
+        let _ = Duration::from_nanos(nanos);
+    }
+
+    #[kani::proof_for_contract(Duration::as_secs)]
+    fn duration_as_secs() {
+        let dur = safe_duration();
+        let _ = dur.as_secs();
+    }
+
+    #[kani::proof_for_contract(Duration::as_secs)]
+    #[kani::should_panic]
+    fn duration_as_secs_panics() {
+        let dur = kani::any::<Duration>();
+        let _ = dur.as_secs();
+    }
+
+    #[kani::proof_for_contract(Duration::subsec_millis)]
+    fn duration_subsec_millis() {
+        let dur = safe_duration();
+        let _ = dur.subsec_millis();
+    }
+
+    #[kani::proof_for_contract(Duration::subsec_millis)]
+    #[kani::should_panic]
+    fn duration_subsec_millis_panics() {
+        let dur = kani::any::<Duration>();
+        let _ = dur.subsec_millis();
+    }
+
+    #[kani::proof_for_contract(Duration::subsec_micros)]
+    fn duration_subsec_micros() {
+        let dur = safe_duration();
+        let _ = dur.subsec_micros();
+    }
+
+    #[kani::proof_for_contract(Duration::subsec_micros)]
+    #[kani::should_panic]
+    fn duration_subsec_micros_panics() {
+        let dur = kani::any::<Duration>();
+        let _ = dur.subsec_micros();
+    }
+
+    #[kani::proof_for_contract(Duration::subsec_nanos)]
+    fn duration_subsec_nanos() {
+        let dur = safe_duration();
+        let _ = dur.subsec_nanos();
+    }
+
+    #[kani::proof_for_contract(Duration::subsec_nanos)]
+    #[kani::should_panic]
+    fn duration_subsec_nanos_panics() {
+        let dur = kani::any::<Duration>();
+        let _ = dur.subsec_nanos();
+    }
+
+    #[kani::proof_for_contract(Duration::as_millis)]
+    fn duration_as_millis() {
+        let dur = safe_duration();
+        let _ = dur.as_millis();
+    }
+
+    #[kani::proof_for_contract(Duration::as_millis)]
+    #[kani::should_panic]
+    fn duration_as_millis_panics() {
+        let dur = kani::any::<Duration>();
+        let _ = dur.as_millis();
+    }
+
+    #[kani::proof_for_contract(Duration::as_micros)]
+    fn duration_as_micros() {
+        let dur = safe_duration();
+        let _ = dur.as_micros();
+    }
+
+    #[kani::proof_for_contract(Duration::as_micros)]
+    #[kani::should_panic]
+    fn duration_as_micros_panics() {
+        let dur = kani::any::<Duration>();
+        let _ = dur.as_micros();
+    }
+
+    #[kani::proof]
+    fn duration_as_nanos() {
+        let dur = safe_duration();
+        let _ = dur.as_nanos();
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    fn duration_as_nanos_panics() {
+        let dur = kani::any::<Duration>();
+        let _ = dur.as_nanos();
+    }
+
+    #[kani::proof_for_contract(Duration::checked_add)]
+    fn duration_checked_add() {
+        let d0 = safe_duration();
+        let d1 = safe_duration();
+        let _ = d0.checked_add(d1);
+    }
+
+    #[kani::proof_for_contract(Duration::checked_add)]
+    #[kani::should_panic]
+    fn duration_checked_add_panics() {
+        let d0 = kani::any::<Duration>();
+        let d1 = kani::any::<Duration>();
+        let _ = d0.checked_add(d1);
+    }
+
+    #[kani::proof_for_contract(Duration::checked_sub)]
+    fn duration_checked_sub() {
+        let d0 = safe_duration();
+        let d1 = safe_duration();
+        let _ = d0.checked_sub(d1);
+    }
+
+    #[kani::proof_for_contract(Duration::checked_sub)]
+    #[kani::should_panic]
+    fn duration_checked_sub_panics() {
+        let d0 = kani::any::<Duration>();
+        let d1 = kani::any::<Duration>();
+        let _ = d0.checked_sub(d1);
+    }
+
+    #[kani::proof_for_contract(Duration::checked_mul)]
+    fn duration_checked_mul() {
+        let d0 = safe_duration();
+        let amt = kani::any::<u32>();
+        let _ = d0.checked_mul(amt);
+    }
+
+    #[kani::proof_for_contract(Duration::checked_mul)]
+    #[kani::should_panic]
+    fn duration_checked_mul_panics() {
+        let d0 = kani::any::<Duration>();
+        let amt = kani::any::<u32>();
+        let _ = d0.checked_mul(amt);
+    }
+
+    #[kani::proof_for_contract(Duration::checked_div)]
+    fn duration_checked_div() {
+        let d0 = safe_duration();
+        let amt = kani::any::<u32>();
+        let _ = d0.checked_div(amt);
+    }
+
+    #[kani::proof_for_contract(Duration::checked_div)]
+    #[kani::should_panic]
+    fn duration_checked_div_panics() {
+        let d0 = kani::any::<Duration>();
+        let amt = kani::any::<u32>();
+        let _ = d0.checked_div(amt);
+    }
+}
