From 15af767a622993f7e26d9958d03adb463064178e Mon Sep 17 00:00:00 2001 From: cole Date: Thu, 11 Jul 2024 15:32:47 -0700 Subject: [PATCH] add autogenerated kani harnesses --- src/duration/mod.rs | 225 +++++++++++++++++++++++ src/efmt/format.rs | 11 ++ src/efmt/formatter.rs | 73 +++++++- src/epoch/gregorian.rs | 224 +++++++++++++++++++++++ src/epoch/leap_seconds.rs | 14 ++ src/epoch/mod.rs | 373 ++++++++++++++++++++++++++++++++++++++ src/epoch/ops.rs | 106 +++++++++++ src/epoch/system_time.rs | 14 ++ src/epoch/ut1.rs | 10 + src/epoch/with_funcs.rs | 43 +++++ src/errors.rs | 1 + src/month.rs | 1 + src/parser.rs | 31 ++++ src/timescale/mod.rs | 37 +++- src/timeseries.rs | 21 +++ src/timeunits.rs | 2 + src/weekday.rs | 11 ++ 17 files changed, 1194 insertions(+), 3 deletions(-) diff --git a/src/duration/mod.rs b/src/duration/mod.rs index 36dee40..ae5a8a7 100644 --- a/src/duration/mod.rs +++ b/src/duration/mod.rs @@ -828,3 +828,228 @@ mod ut_duration { assert_eq!(nanoseconds, 0); } } +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_Duration_from_parts() { + let centuries: i16 = kani::any(); + let nanoseconds: u64 = kani::any(); + Duration::from_parts(centuries, nanoseconds); + } + + #[kani::proof] + fn kani_harness_Duration_from_total_nanoseconds() { + let nanos: i128 = kani::any(); + Duration::from_total_nanoseconds(nanos); + } + + #[kani::proof] + fn kani_harness_Duration_from_truncated_nanoseconds() { + let nanos: i64 = kani::any(); + Duration::from_truncated_nanoseconds(nanos); + } + + #[kani::proof] + fn kani_harness_Duration_from_days() { + let value: f64 = kani::any(); + Duration::from_days(value); + } + + #[kani::proof] + fn kani_harness_Duration_from_hours() { + let value: f64 = kani::any(); + Duration::from_hours(value); + } + + #[kani::proof] + fn kani_harness_Duration_from_seconds() { + let value: f64 = kani::any(); + Duration::from_seconds(value); + } + + #[kani::proof] + fn kani_harness_Duration_from_milliseconds() { + let value: f64 = kani::any(); + Duration::from_milliseconds(value); + } + + #[kani::proof] + fn kani_harness_Duration_from_microseconds() { + let value: f64 = kani::any(); + Duration::from_microseconds(value); + } + + #[kani::proof] + fn kani_harness_Duration_from_nanoseconds() { + let value: f64 = kani::any(); + Duration::from_nanoseconds(value); + } + + #[kani::proof] + fn kani_harness_Duration_compose() { + let sign: i8 = kani::any(); + let days: u64 = kani::any(); + let hours: u64 = kani::any(); + let minutes: u64 = kani::any(); + let seconds: u64 = kani::any(); + let milliseconds: u64 = kani::any(); + let microseconds: u64 = kani::any(); + let nanoseconds: u64 = kani::any(); + Duration::compose( + sign, + days, + hours, + minutes, + seconds, + milliseconds, + microseconds, + nanoseconds, + ); + } + + #[kani::proof] + fn kani_harness_Duration_compose_f64() { + let sign: i8 = kani::any(); + let days: f64 = kani::any(); + let hours: f64 = kani::any(); + let minutes: f64 = kani::any(); + let seconds: f64 = kani::any(); + let milliseconds: f64 = kani::any(); + let microseconds: f64 = kani::any(); + let nanoseconds: f64 = kani::any(); + Duration::compose_f64( + sign, + days, + hours, + minutes, + seconds, + milliseconds, + microseconds, + nanoseconds, + ); + } + + #[kani::proof] + fn kani_harness_Duration_from_tz_offset() { + let sign: i8 = kani::any(); + let hours: i64 = kani::any(); + let minutes: i64 = kani::any(); + Duration::from_tz_offset(sign, hours, minutes); + } + + #[kani::proof] + fn kani_harness_normalize() { + let mut callee: Duration = kani::any(); + callee.normalize(); + } + + #[kani::proof] + fn kani_harness_to_parts() { + let callee: Duration = kani::any(); + callee.to_parts(); + } + + #[kani::proof] + fn kani_harness_total_nanoseconds() { + let callee: Duration = kani::any(); + callee.total_nanoseconds(); + } + + #[kani::proof] + fn kani_harness_try_truncated_nanoseconds() { + let callee: Duration = kani::any(); + callee.try_truncated_nanoseconds(); + } + + #[kani::proof] + fn kani_harness_truncated_nanoseconds() { + let callee: Duration = kani::any(); + callee.truncated_nanoseconds(); + } + + #[kani::proof] + fn kani_harness_to_seconds() { + let callee: Duration = kani::any(); + callee.to_seconds(); + } + + #[kani::proof] + fn kani_harness_to_unit() { + let unit: Unit = kani::any(); + let callee: Duration = kani::any(); + callee.to_unit(unit); + } + + #[kani::proof] + fn kani_harness_abs() { + let callee: Duration = kani::any(); + callee.abs(); + } + + #[kani::proof] + fn kani_harness_signum() { + let callee: Duration = kani::any(); + callee.signum(); + } + + #[kani::proof] + fn kani_harness_decompose() { + let callee: Duration = kani::any(); + callee.decompose(); + } + + #[kani::proof] + fn kani_harness_subdivision() { + let unit: Unit = kani::any(); + let callee: Duration = kani::any(); + callee.subdivision(unit); + } + + #[kani::proof] + fn kani_harness_floor() { + let duration: Duration = kani::any(); + let callee: Duration = kani::any(); + callee.floor(duration); + } + + #[kani::proof] + fn kani_harness_ceil() { + let duration: Duration = kani::any(); + let callee: Duration = kani::any(); + callee.ceil(duration); + } + + #[kani::proof] + fn kani_harness_round() { + let duration: Duration = kani::any(); + let callee: Duration = kani::any(); + callee.round(duration); + } + + #[kani::proof] + fn kani_harness_approx() { + let callee: Duration = kani::any(); + callee.approx(); + } + + #[kani::proof] + fn kani_harness_min() { + let other: Duration = kani::any(); + let callee: Duration = kani::any(); + callee.min(other); + } + + #[kani::proof] + fn kani_harness_max() { + let other: Duration = kani::any(); + let callee: Duration = kani::any(); + callee.max(other); + } + + #[kani::proof] + fn kani_harness_is_negative() { + let callee: Duration = kani::any(); + callee.is_negative(); + } +} diff --git a/src/efmt/format.rs b/src/efmt/format.rs index faafb5c..ba60667 100644 --- a/src/efmt/format.rs +++ b/src/efmt/format.rs @@ -110,6 +110,7 @@ const MAX_TOKENS: usize = 16; /// let fmt = Formatter::new(bday, consts::RFC2822); /// assert_eq!(format!("{fmt}"), format!("Tue, 29 Feb 2000 14:57:29")); /// ``` +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Copy, Clone, Default, PartialEq)] pub struct Format { pub(crate) items: [Option; MAX_TOKENS], @@ -600,3 +601,13 @@ fn gh_248_regression() { assert_eq!(format!("{e}"), "2023-04-27T12:55:26 UTC"); } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_need_gregorian() { + let callee: Format = kani::any(); + callee.need_gregorian(); + } +} diff --git a/src/efmt/formatter.rs b/src/efmt/formatter.rs index 26df41a..76a6c6e 100644 --- a/src/efmt/formatter.rs +++ b/src/efmt/formatter.rs @@ -17,7 +17,7 @@ use super::format::Format; #[cfg(not(feature = "std"))] #[allow(unused_imports)] // Import is indeed used. use num_traits::Float; - +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Copy, Clone, Default, Debug, PartialEq)] pub(crate) struct Item { pub(crate) token: Token, @@ -76,6 +76,7 @@ impl Item { } } +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Copy, Clone, Debug, PartialEq)] pub struct Formatter { epoch: Epoch, @@ -302,3 +303,73 @@ impl fmt::Display for Formatter { Ok(()) } } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_Item_new() { + let token: Token = kani::any(); + let sep_char: Option = kani::any(); + let second_sep_char: Option = kani::any(); + Item::new(token, sep_char, second_sep_char); + } + + #[kani::proof] + fn kani_harness_sep_char_is() { + let c_in: char = kani::any(); + let callee: Item = kani::any(); + callee.sep_char_is(c_in); + } + + #[kani::proof] + fn kani_harness_sep_char_is_not() { + let c_in: char = kani::any(); + let callee: Item = kani::any(); + callee.sep_char_is_not(c_in); + } + + #[kani::proof] + fn kani_harness_second_sep_char_is() { + let c_in: char = kani::any(); + let callee: Item = kani::any(); + callee.second_sep_char_is(c_in); + } + + #[kani::proof] + fn kani_harness_second_sep_char_is_not() { + let c_in: char = kani::any(); + let callee: Item = kani::any(); + callee.second_sep_char_is_not(c_in); + } + + #[kani::proof] + fn kani_harness_Formatter_new() { + let epoch: Epoch = kani::any(); + let format: Format = kani::any(); + Formatter::new(epoch, format); + } + + #[kani::proof] + fn kani_harness_Formatter_with_timezone() { + let epoch: Epoch = kani::any(); + let offset: Duration = kani::any(); + let format: Format = kani::any(); + Formatter::with_timezone(epoch, offset, format); + } + + #[kani::proof] + fn kani_harness_Formatter_to_time_scale() { + let epoch: Epoch = kani::any(); + let format: Format = kani::any(); + let time_scale: TimeScale = kani::any(); + Formatter::to_time_scale(epoch, format, time_scale); + } + + #[kani::proof] + fn kani_harness_set_timezone() { + let offset: Duration = kani::any(); + let mut callee: Formatter = kani::any(); + callee.set_timezone(offset); + } +} diff --git a/src/epoch/gregorian.rs b/src/epoch/gregorian.rs index fe1290e..a227558 100644 --- a/src/epoch/gregorian.rs +++ b/src/epoch/gregorian.rs @@ -795,3 +795,227 @@ mod ut_gregorian { } } } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_Epoch_compute_gregorian() { + let duration: Duration = kani::any(); + let time_scale: TimeScale = kani::any(); + Epoch::compute_gregorian(duration, time_scale); + } + + #[kani::proof] + fn kani_harness_to_gregorian_str() { + let time_scale: TimeScale = kani::any(); + let callee: Epoch = kani::any(); + callee.to_gregorian_str(time_scale); + } + + #[kani::proof] + fn kani_harness_to_gregorian_utc() { + let callee: Epoch = kani::any(); + callee.to_gregorian_utc(); + } + + #[kani::proof] + fn kani_harness_to_gregorian_tai() { + let callee: Epoch = kani::any(); + callee.to_gregorian_tai(); + } + + #[kani::proof] + fn kani_harness_Epoch_maybe_from_gregorian_tai() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let hour: u8 = kani::any(); + let minute: u8 = kani::any(); + let second: u8 = kani::any(); + let nanos: u32 = kani::any(); + Epoch::maybe_from_gregorian_tai(year, month, day, hour, minute, second, nanos); + } + + #[kani::proof] + fn kani_harness_Epoch_maybe_from_gregorian() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let hour: u8 = kani::any(); + let minute: u8 = kani::any(); + let second: u8 = kani::any(); + let nanos: u32 = kani::any(); + let time_scale: TimeScale = kani::any(); + Epoch::maybe_from_gregorian(year, month, day, hour, minute, second, nanos, time_scale); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_tai() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let hour: u8 = kani::any(); + let minute: u8 = kani::any(); + let second: u8 = kani::any(); + let nanos: u32 = kani::any(); + Epoch::from_gregorian_tai(year, month, day, hour, minute, second, nanos); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_tai_at_midnight() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + Epoch::from_gregorian_tai_at_midnight(year, month, day); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_tai_at_noon() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + Epoch::from_gregorian_tai_at_noon(year, month, day); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_tai_hms() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let hour: u8 = kani::any(); + let minute: u8 = kani::any(); + let second: u8 = kani::any(); + Epoch::from_gregorian_tai_hms(year, month, day, hour, minute, second); + } + + #[kani::proof] + fn kani_harness_Epoch_maybe_from_gregorian_utc() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let hour: u8 = kani::any(); + let minute: u8 = kani::any(); + let second: u8 = kani::any(); + let nanos: u32 = kani::any(); + Epoch::maybe_from_gregorian_utc(year, month, day, hour, minute, second, nanos); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_utc() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let hour: u8 = kani::any(); + let minute: u8 = kani::any(); + let second: u8 = kani::any(); + let nanos: u32 = kani::any(); + Epoch::from_gregorian_utc(year, month, day, hour, minute, second, nanos); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_utc_at_midnight() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + Epoch::from_gregorian_utc_at_midnight(year, month, day); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_utc_at_noon() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + Epoch::from_gregorian_utc_at_noon(year, month, day); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_utc_hms() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let hour: u8 = kani::any(); + let minute: u8 = kani::any(); + let second: u8 = kani::any(); + Epoch::from_gregorian_utc_hms(year, month, day, hour, minute, second); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let hour: u8 = kani::any(); + let minute: u8 = kani::any(); + let second: u8 = kani::any(); + let nanos: u32 = kani::any(); + let time_scale: TimeScale = kani::any(); + Epoch::from_gregorian(year, month, day, hour, minute, second, nanos, time_scale); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_at_midnight() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let time_scale: TimeScale = kani::any(); + Epoch::from_gregorian_at_midnight(year, month, day, time_scale); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_at_noon() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let time_scale: TimeScale = kani::any(); + Epoch::from_gregorian_at_noon(year, month, day, time_scale); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gregorian_hms() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let hour: u8 = kani::any(); + let minute: u8 = kani::any(); + let second: u8 = kani::any(); + let time_scale: TimeScale = kani::any(); + Epoch::from_gregorian_hms(year, month, day, hour, minute, second, time_scale); + } + + #[kani::proof] + fn kani_harness_is_gregorian_valid() { + let year: i32 = kani::any(); + let month: u8 = kani::any(); + let day: u8 = kani::any(); + let hour: u8 = kani::any(); + let minute: u8 = kani::any(); + let second: u8 = kani::any(); + let nanos: u32 = kani::any(); + is_gregorian_valid(year, month, day, hour, minute, second, nanos); + } + + #[kani::proof] + fn kani_harness_january_years() { + let year: i32 = kani::any(); + january_years(year); + } + + #[kani::proof] + fn kani_harness_july_years() { + let year: i32 = kani::any(); + july_years(year); + } + + #[kani::proof] + fn kani_harness_usual_days_per_month() { + let month: u8 = kani::any(); + usual_days_per_month(month); + } + + #[kani::proof] + fn kani_harness_is_leap_year() { + let year: i32 = kani::any(); + is_leap_year(year); + } +} diff --git a/src/epoch/leap_seconds.rs b/src/epoch/leap_seconds.rs index 94ba9bf..9f50133 100644 --- a/src/epoch/leap_seconds.rs +++ b/src/epoch/leap_seconds.rs @@ -19,6 +19,7 @@ use core::ops::Index; pub trait LeapSecondProvider: DoubleEndedIterator + Index {} /// A structure representing a leap second +#[cfg_attr(kani, derive(kani::Arbitrary))] #[repr(C)] #[cfg_attr(feature = "python", pyclass)] #[derive(Copy, Clone, Debug, PartialEq)] @@ -90,6 +91,7 @@ const LATEST_LEAP_SECONDS: [LeapSecond; 42] = [ /// This list corresponds the number of seconds in TAI to the UTC offset and to whether it was an announced leap second or not. /// The unannoucned leap seconds come from dat.c in the SOFA library. #[cfg_attr(feature = "python", pyclass)] +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Clone, Debug)] pub struct LatestLeapSeconds { data: [LeapSecond; 42], @@ -161,3 +163,15 @@ fn leap_second_fetch() { LeapSecond::new(3_692_217_600.0, 37.0, true) ); } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_LeapSecond_new() { + let timestamp_tai_s: f64 = kani::any(); + let delta_at: f64 = kani::any(); + let announced: bool = kani::any(); + LeapSecond::new(timestamp_tai_s, delta_at, announced); + } +} diff --git a/src/epoch/mod.rs b/src/epoch/mod.rs index 3e4b7b6..ec599a7 100644 --- a/src/epoch/mod.rs +++ b/src/epoch/mod.rs @@ -75,6 +75,7 @@ pub const NAIF_K: f64 = 1.657e-3; /// Defines a nanosecond-precision Epoch. /// /// Refer to the appropriate functions for initializing this Epoch from different time scales or representations. +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Copy, Clone, Default, Eq)] #[repr(C)] #[cfg_attr(feature = "python", pyclass)] @@ -1425,3 +1426,375 @@ mod ut_epoch { assert_eq!(e, parsed); } } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_to_time_scale() { + let ts: TimeScale = kani::any(); + let callee: Epoch = kani::any(); + callee.to_time_scale(ts); + } + + #[kani::proof] + fn kani_harness_Epoch_from_tai_duration() { + let duration: Duration = kani::any(); + Epoch::from_tai_duration(duration); + } + + + #[kani::proof] + fn kani_harness_Epoch_from_duration() { + let duration: Duration = kani::any(); + let ts: TimeScale = kani::any(); + Epoch::from_duration(duration, ts); + } + + #[kani::proof] + fn kani_harness_to_duration_since_j1900() { + let callee: Epoch = kani::any(); + callee.to_duration_since_j1900(); + } + + #[kani::proof] + fn kani_harness_Epoch_from_tai_parts() { + let centuries: i16 = kani::any(); + let nanoseconds: u64 = kani::any(); + Epoch::from_tai_parts(centuries, nanoseconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_tai_seconds() { + let seconds: f64 = kani::any(); + Epoch::from_tai_seconds(seconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_tai_days() { + let days: f64 = kani::any(); + Epoch::from_tai_days(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_utc_duration() { + let duration: Duration = kani::any(); + Epoch::from_utc_duration(duration); + } + + #[kani::proof] + fn kani_harness_Epoch_from_utc_seconds() { + let seconds: f64 = kani::any(); + Epoch::from_utc_seconds(seconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_utc_days() { + let days: f64 = kani::any(); + Epoch::from_utc_days(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gpst_duration() { + let duration: Duration = kani::any(); + Epoch::from_gpst_duration(duration); + } + + #[kani::proof] + fn kani_harness_Epoch_from_qzsst_duration() { + let duration: Duration = kani::any(); + Epoch::from_qzsst_duration(duration); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gst_duration() { + let duration: Duration = kani::any(); + Epoch::from_gst_duration(duration); + } + + #[kani::proof] + fn kani_harness_Epoch_from_bdt_duration() { + let duration: Duration = kani::any(); + Epoch::from_bdt_duration(duration); + } + + #[kani::proof] + fn kani_harness_Epoch_from_mjd_tai() { + let days: f64 = kani::any(); + Epoch::from_mjd_tai(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_mjd_in_time_scale() { + let days: f64 = kani::any(); + let time_scale: TimeScale = kani::any(); + Epoch::from_mjd_in_time_scale(days, time_scale); + } + + #[kani::proof] + fn kani_harness_Epoch_from_mjd_utc() { + let days: f64 = kani::any(); + Epoch::from_mjd_utc(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_mjd_gpst() { + let days: f64 = kani::any(); + Epoch::from_mjd_gpst(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_mjd_qzsst() { + let days: f64 = kani::any(); + Epoch::from_mjd_qzsst(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_mjd_gst() { + let days: f64 = kani::any(); + Epoch::from_mjd_gst(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_mjd_bdt() { + let days: f64 = kani::any(); + Epoch::from_mjd_bdt(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_jde_tai() { + let days: f64 = kani::any(); + Epoch::from_jde_tai(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_jde_in_time_scale() { + let days: f64 = kani::any(); + let time_scale: TimeScale = kani::any(); + Epoch::from_jde_in_time_scale(days, time_scale); + } + + #[kani::proof] + fn kani_harness_Epoch_from_jde_utc() { + let days: f64 = kani::any(); + Epoch::from_jde_utc(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_jde_gpst() { + let days: f64 = kani::any(); + Epoch::from_jde_gpst(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_jde_qzsst() { + let days: f64 = kani::any(); + Epoch::from_jde_qzsst(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_jde_gst() { + let days: f64 = kani::any(); + Epoch::from_jde_gst(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_jde_bdt() { + let days: f64 = kani::any(); + Epoch::from_jde_bdt(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_tt_seconds() { + let seconds: f64 = kani::any(); + Epoch::from_tt_seconds(seconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_tt_duration() { + let duration: Duration = kani::any(); + Epoch::from_tt_duration(duration); + } + + #[kani::proof] + fn kani_harness_Epoch_from_et_seconds() { + let seconds_since_j2000: f64 = kani::any(); + Epoch::from_et_seconds(seconds_since_j2000); + } + + #[kani::proof] + fn kani_harness_Epoch_from_et_duration() { + let duration_since_j2000: Duration = kani::any(); + Epoch::from_et_duration(duration_since_j2000); + } + + #[kani::proof] + fn kani_harness_Epoch_from_tdb_seconds() { + let seconds_j2000: f64 = kani::any(); + Epoch::from_tdb_seconds(seconds_j2000); + } + + #[kani::proof] + fn kani_harness_Epoch_from_tdb_duration() { + let duration_since_j2000: Duration = kani::any(); + Epoch::from_tdb_duration(duration_since_j2000); + } + + #[kani::proof] + fn kani_harness_Epoch_from_jde_et() { + let days: f64 = kani::any(); + Epoch::from_jde_et(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_jde_tdb() { + let days: f64 = kani::any(); + Epoch::from_jde_tdb(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gpst_seconds() { + let seconds: f64 = kani::any(); + Epoch::from_gpst_seconds(seconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gpst_days() { + let days: f64 = kani::any(); + Epoch::from_gpst_days(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gpst_nanoseconds() { + let nanoseconds: u64 = kani::any(); + Epoch::from_gpst_nanoseconds(nanoseconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_qzsst_seconds() { + let seconds: f64 = kani::any(); + Epoch::from_qzsst_seconds(seconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_qzsst_days() { + let days: f64 = kani::any(); + Epoch::from_qzsst_days(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_qzsst_nanoseconds() { + let nanoseconds: u64 = kani::any(); + Epoch::from_qzsst_nanoseconds(nanoseconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gst_seconds() { + let seconds: f64 = kani::any(); + Epoch::from_gst_seconds(seconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gst_days() { + let days: f64 = kani::any(); + Epoch::from_gst_days(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_gst_nanoseconds() { + let nanoseconds: u64 = kani::any(); + Epoch::from_gst_nanoseconds(nanoseconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_bdt_seconds() { + let seconds: f64 = kani::any(); + Epoch::from_bdt_seconds(seconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_bdt_days() { + let days: f64 = kani::any(); + Epoch::from_bdt_days(days); + } + + #[kani::proof] + fn kani_harness_Epoch_from_bdt_nanoseconds() { + let nanoseconds: u64 = kani::any(); + Epoch::from_bdt_nanoseconds(nanoseconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_unix_duration() { + let duration: Duration = kani::any(); + Epoch::from_unix_duration(duration); + } + + #[kani::proof] + fn kani_harness_Epoch_from_unix_seconds() { + let seconds: f64 = kani::any(); + Epoch::from_unix_seconds(seconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_unix_milliseconds() { + let millisecond: f64 = kani::any(); + Epoch::from_unix_milliseconds(millisecond); + } + + #[kani::proof] + fn kani_harness_Epoch_delta_et_tai() { + let seconds: f64 = kani::any(); + Epoch::delta_et_tai(seconds); + } + + #[kani::proof] + fn kani_harness_Epoch_inner_g() { + let seconds: f64 = kani::any(); + Epoch::inner_g(seconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_time_of_week() { + let week: u32 = kani::any(); + let nanoseconds: u64 = kani::any(); + let time_scale: TimeScale = kani::any(); + Epoch::from_time_of_week(week, nanoseconds, time_scale); + } + + #[kani::proof] + fn kani_harness_Epoch_from_time_of_week_utc() { + let week: u32 = kani::any(); + let nanoseconds: u64 = kani::any(); + Epoch::from_time_of_week_utc(week, nanoseconds); + } + + #[kani::proof] + fn kani_harness_Epoch_from_day_of_year() { + let year: i32 = kani::any(); + let days: f64 = kani::any(); + let time_scale: TimeScale = kani::any(); + Epoch::from_day_of_year(year, days, time_scale); + } + + #[kani::proof] + fn kani_harness_div_rem_f64() { + let me: f64 = kani::any(); + let rhs: f64 = kani::any(); + div_rem_f64(me, rhs); + } + + #[kani::proof] + fn kani_harness_div_euclid_f64() { + let lhs: f64 = kani::any(); + let rhs: f64 = kani::any(); + div_euclid_f64(lhs, rhs); + } + + #[kani::proof] + fn kani_harness_rem_euclid_f64() { + let lhs: f64 = kani::any(); + let rhs: f64 = kani::any(); + rem_euclid_f64(lhs, rhs); + } +} diff --git a/src/epoch/ops.rs b/src/epoch/ops.rs index 35c5f6d..e0dbfef 100644 --- a/src/epoch/ops.rs +++ b/src/epoch/ops.rs @@ -378,3 +378,109 @@ impl Hash for Epoch { self.time_scale.hash(state); } } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_min() { + let other: Epoch = kani::any(); + let callee: Epoch = kani::any(); + callee.min(other); + } + + #[kani::proof] + fn kani_harness_max() { + let other: Epoch = kani::any(); + let callee: Epoch = kani::any(); + callee.max(other); + } + + #[kani::proof] + fn kani_harness_floor() { + let duration: Duration = kani::any(); + let callee: Epoch = kani::any(); + callee.floor(duration); + } + + #[kani::proof] + fn kani_harness_ceil() { + let duration: Duration = kani::any(); + let callee: Epoch = kani::any(); + callee.ceil(duration); + } + + #[kani::proof] + fn kani_harness_round() { + let duration: Duration = kani::any(); + let callee: Epoch = kani::any(); + callee.round(duration); + } + + #[kani::proof] + fn kani_harness_to_time_of_week() { + let callee: Epoch = kani::any(); + callee.to_time_of_week(); + } + + #[kani::proof] + fn kani_harness_weekday_in_time_scale() { + let time_scale: TimeScale = kani::any(); + let callee: Epoch = kani::any(); + callee.weekday_in_time_scale(time_scale); + } + + #[kani::proof] + fn kani_harness_weekday() { + let callee: Epoch = kani::any(); + callee.weekday(); + } + + #[kani::proof] + fn kani_harness_weekday_utc() { + let callee: Epoch = kani::any(); + callee.weekday_utc(); + } + + #[kani::proof] + fn kani_harness_next() { + let weekday: Weekday = kani::any(); + let callee: Epoch = kani::any(); + callee.next(weekday); + } + + #[kani::proof] + fn kani_harness_next_weekday_at_midnight() { + let weekday: Weekday = kani::any(); + let callee: Epoch = kani::any(); + callee.next_weekday_at_midnight(weekday); + } + + #[kani::proof] + fn kani_harness_next_weekday_at_noon() { + let weekday: Weekday = kani::any(); + let callee: Epoch = kani::any(); + callee.next_weekday_at_noon(weekday); + } + + #[kani::proof] + fn kani_harness_previous() { + let weekday: Weekday = kani::any(); + let callee: Epoch = kani::any(); + callee.previous(weekday); + } + + #[kani::proof] + fn kani_harness_previous_weekday_at_midnight() { + let weekday: Weekday = kani::any(); + let callee: Epoch = kani::any(); + callee.previous_weekday_at_midnight(weekday); + } + + #[kani::proof] + fn kani_harness_previous_weekday_at_noon() { + let weekday: Weekday = kani::any(); + let callee: Epoch = kani::any(); + callee.previous_weekday_at_noon(weekday); + } +} diff --git a/src/epoch/system_time.rs b/src/epoch/system_time.rs index 4b04267..ed4748b 100644 --- a/src/epoch/system_time.rs +++ b/src/epoch/system_time.rs @@ -34,3 +34,17 @@ impl Epoch { Ok(Self::from_unix_duration(duration)) } } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_duration_since_unix_epoch() { + duration_since_unix_epoch(); + } + + #[kani::proof] + fn kani_harness_Epoch_now() { + Epoch::now(); + } +} diff --git a/src/epoch/ut1.rs b/src/epoch/ut1.rs index afcef9f..fd740dc 100644 --- a/src/epoch/ut1.rs +++ b/src/epoch/ut1.rs @@ -64,6 +64,7 @@ impl Epoch { } } +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Copy, Clone, Debug, Default, Tabled)] pub struct DeltaTaiUt1 { pub epoch: Epoch, @@ -233,3 +234,12 @@ impl Index for Ut1Provider { self.data.index(index) } } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_Ut1Provider_download_short_from_jpl() { + Ut1Provider::download_short_from_jpl(); + } +} diff --git a/src/epoch/with_funcs.rs b/src/epoch/with_funcs.rs index e3041a0..6194612 100644 --- a/src/epoch/with_funcs.rs +++ b/src/epoch/with_funcs.rs @@ -148,3 +148,46 @@ impl Epoch { ) } } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_with_hms() { + let hours: u64 = kani::any(); + let minutes: u64 = kani::any(); + let seconds: u64 = kani::any(); + let callee: Epoch = kani::any(); + callee.with_hms(hours, minutes, seconds); + } + + #[kani::proof] + fn kani_harness_with_hms_from() { + let other: Epoch = kani::any(); + let callee: Epoch = kani::any(); + callee.with_hms_from(other); + } + + #[kani::proof] + fn kani_harness_with_time_from() { + let other: Epoch = kani::any(); + let callee: Epoch = kani::any(); + callee.with_time_from(other); + } + + #[kani::proof] + fn kani_harness_with_hms_strict() { + let hours: u64 = kani::any(); + let minutes: u64 = kani::any(); + let seconds: u64 = kani::any(); + let callee: Epoch = kani::any(); + callee.with_hms_strict(hours, minutes, seconds); + } + + #[kani::proof] + fn kani_harness_with_hms_strict_from() { + let other: Epoch = kani::any(); + let callee: Epoch = kani::any(); + callee.with_hms_strict_from(other); + } +} diff --git a/src/errors.rs b/src/errors.rs index 20d9197..7211c35 100644 --- a/src/errors.rs +++ b/src/errors.rs @@ -40,6 +40,7 @@ pub enum HifitimeError { }, } +#[cfg_attr(kani, derive(kani::Arbitrary))] #[non_exhaustive] #[derive(Debug, Snafu, PartialEq)] pub enum DurationError { diff --git a/src/month.rs b/src/month.rs index d7d91f0..56bcefd 100644 --- a/src/month.rs +++ b/src/month.rs @@ -18,6 +18,7 @@ use pyo3::prelude::*; #[cfg(feature = "serde")] use serde_derive::{Deserialize, Serialize}; +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord)] #[repr(u8)] #[cfg_attr(feature = "python", pyclass(eq, eq_int))] diff --git a/src/parser.rs b/src/parser.rs index 246f713..62dc094 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -10,6 +10,7 @@ use crate::{HifitimeError, ParsingError}; +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Debug, Copy, Clone, PartialEq, Eq)] pub(crate) enum Token { Year, @@ -277,3 +278,33 @@ impl Token { ) } } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_value_ok() { + let val: i32 = kani::any(); + let callee: Token = kani::any(); + callee.value_ok(val); + } + + #[kani::proof] + fn kani_harness_gregorian_position() { + let callee: Token = kani::any(); + callee.gregorian_position(); + } + + #[kani::proof] + fn kani_harness_advance_with() { + let ending_char: char = kani::any(); + let mut callee: Token = kani::any(); + callee.advance_with(ending_char); + } + + #[kani::proof] + fn kani_harness_is_numeric() { + let callee: Token = kani::any(); + callee.is_numeric(); + } +} diff --git a/src/timescale/mod.rs b/src/timescale/mod.rs index 9255f25..e9ea64a 100644 --- a/src/timescale/mod.rs +++ b/src/timescale/mod.rs @@ -14,8 +14,6 @@ use pyo3::prelude::*; #[cfg(feature = "serde")] use serde_derive::{Deserialize, Serialize}; -#[cfg(kani)] -mod kani; mod fmt; @@ -79,6 +77,7 @@ pub const UNIX_REF_EPOCH: Epoch = Epoch::from_tai_duration(Duration { /// Reference year of the Hifitime prime epoch. pub(crate) const HIFITIME_REF_YEAR: i32 = 1900; +#[cfg_attr(kani, derive(kani::Arbitrary))] /// Enum of the different time systems available #[non_exhaustive] #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] @@ -262,3 +261,37 @@ mod unit_test_timescale { ); } } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_formatted_len() { + let callee: TimeScale = kani::any(); + callee.formatted_len(); + } + + #[kani::proof] + fn kani_harness_is_gnss() { + let callee: TimeScale = kani::any(); + callee.is_gnss(); + } + + #[kani::proof] + fn kani_harness_reference_epoch() { + let callee: TimeScale = kani::any(); + callee.reference_epoch(); + } + + #[kani::proof] + fn kani_harness_prime_epoch_offset() { + let callee: TimeScale = kani::any(); + callee.prime_epoch_offset(); + } + + #[kani::proof] + fn kani_harness_gregorian_epoch_offset() { + let callee: TimeScale = kani::any(); + callee.gregorian_epoch_offset(); + } +} diff --git a/src/timeseries.rs b/src/timeseries.rs index f9cea4a..566c0e3 100644 --- a/src/timeseries.rs +++ b/src/timeseries.rs @@ -26,6 +26,7 @@ NOTE: This is taken from itertools: https://docs.rs/itertools-num/0.1.3/src/iter */ /// An iterator of a sequence of evenly spaced Epochs. +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Clone, Debug, PartialEq, Eq)] #[cfg_attr(feature = "python", pyclass)] #[cfg_attr(feature = "python", pyo3(module = "hifitime"))] @@ -415,3 +416,23 @@ mod tests { assert_eq!(cur_epoch, start, "incorrect last item in iterator"); } } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_TimeSeries_exclusive() { + let start: Epoch = kani::any(); + let end: Epoch = kani::any(); + let step: Duration = kani::any(); + TimeSeries::exclusive(start, end, step); + } + + #[kani::proof] + fn kani_harness_TimeSeries_inclusive() { + let start: Epoch = kani::any(); + let end: Epoch = kani::any(); + let step: Duration = kani::any(); + TimeSeries::inclusive(start, end, step); + } +} diff --git a/src/timeunits.rs b/src/timeunits.rs index 5735092..035e93b 100644 --- a/src/timeunits.rs +++ b/src/timeunits.rs @@ -25,6 +25,7 @@ use crate::{ }; /// An Enum to perform time unit conversions. +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Copy, Clone, Debug, PartialEq, PartialOrd, Eq, Ord)] #[cfg_attr(feature = "python", pyclass(eq, eq_int))] pub enum Unit { @@ -41,6 +42,7 @@ pub enum Unit { } /// An Enum to convert frequencies to their approximate duration, **rounded to the closest nanosecond**. +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Copy, Clone, Debug, PartialEq, PartialOrd, Eq, Ord)] #[cfg_attr(feature = "python", pyclass(eq, eq_int))] pub enum Freq { diff --git a/src/weekday.rs b/src/weekday.rs index 88c4331..741374d 100644 --- a/src/weekday.rs +++ b/src/weekday.rs @@ -19,6 +19,7 @@ use pyo3::prelude::*; #[cfg(feature = "serde")] use serde_derive::{Deserialize, Serialize}; +#[cfg_attr(kani, derive(kani::Arbitrary))] #[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord)] #[repr(u8)] #[cfg_attr(feature = "python", pyclass(eq, eq_int))] @@ -202,3 +203,13 @@ fn test_iso_weekday() { assert_eq!(Weekday::Friday.to_c89_weekday(), 5); assert_eq!(Weekday::Saturday.to_c89_weekday(), 6); } + +#[cfg(kani)] +mod kani_harnesses { + use super::*; + #[kani::proof] + fn kani_harness_to_c89_weekday() { + let callee: Weekday = kani::any(); + callee.to_c89_weekday(); + } +}