Skip to content

Commit

Permalink
Merge pull request #319 from nyx-space/317-gpst-roundtrip
Browse files Browse the repository at this point in the history
Prevent rounding of the GNSS from nanoseconds initializers
  • Loading branch information
ChristopherRabotin authored Jul 22, 2024
2 parents 55c91ba + f2a14d1 commit 18c8471
Show file tree
Hide file tree
Showing 13 changed files with 53 additions and 38 deletions.
2 changes: 1 addition & 1 deletion src/duration/kani_verif.rs
Original file line number Diff line number Diff line change
Expand Up @@ -125,8 +125,8 @@ mod tests {

#[cfg(kani)]
mod kani_harnesses {
use crate::Unit;
use super::*;
use crate::Unit;
#[kani::proof]
fn kani_harness_Duration_from_parts() {
let centuries: i16 = kani::any();
Expand Down
2 changes: 1 addition & 1 deletion src/duration/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -827,4 +827,4 @@ mod ut_duration {
assert_eq!(microseconds, 0);
assert_eq!(nanoseconds, 0);
}
}
}
2 changes: 1 addition & 1 deletion src/efmt/format.rs
Original file line number Diff line number Diff line change
Expand Up @@ -600,4 +600,4 @@ fn gh_248_regression() {
let e = Epoch::from_format_str("2023-117T12:55:26", "%Y-%jT%H:%M:%S").unwrap();

assert_eq!(format!("{e}"), "2023-04-27T12:55:26 UTC");
}
}
2 changes: 1 addition & 1 deletion src/efmt/formatter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -302,4 +302,4 @@ impl fmt::Display for Formatter {
}
Ok(())
}
}
}
8 changes: 4 additions & 4 deletions src/efmt/kani_verif.rs
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
use super::{
format::Format,
formatter::{Item, Formatter},
formatter::{Formatter, Item},
};
use crate::{duration::Duration, TimeScale};
use crate::Epoch;
use crate::parser::Token;
use crate::Epoch;
use crate::{duration::Duration, TimeScale};

#[cfg(kani)]
mod kani_harnesses {
use crate::*;
use super::*;
use crate::*;
#[kani::proof]
fn kani_harness_need_gregorian() {
let callee: Format = kani::any();
Expand Down
2 changes: 1 addition & 1 deletion src/efmt/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,4 @@ pub use format::Format;
pub use formatter::Formatter;

#[cfg(kani)]
mod kani_verif;
mod kani_verif;
4 changes: 2 additions & 2 deletions src/epoch/kani_verif.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
* Documentation: https://nyxspace.com/
*/

use super::{Duration, Epoch, TimeScale, Unit, TT_OFFSET_MS, Weekday};
use super::{Duration, Epoch, TimeScale, Unit, Weekday, TT_OFFSET_MS};
use crate::epoch::system_time::duration_since_unix_epoch;
use crate::leap_seconds::LeapSecond;

Expand Down Expand Up @@ -179,8 +179,8 @@ fn formal_epoch_julian() {

#[cfg(kani)]
mod kani_harnesses {
use crate::*;
use super::*;
use crate::*;
#[kani::proof]
fn kani_harness_Epoch_compute_gregorian() {
let duration: Duration = kani::any();
Expand Down
2 changes: 1 addition & 1 deletion src/epoch/leap_seconds.rs
Original file line number Diff line number Diff line change
Expand Up @@ -162,4 +162,4 @@ fn leap_second_fetch() {
leap_seconds[41],
LeapSecond::new(3_692_217_600.0, 37.0, true)
);
}
}
28 changes: 5 additions & 23 deletions src/epoch/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -526,7 +526,7 @@ impl Epoch {
/// defined as UTC midnight of January 5th to 6th 1980 (cf. <https://gssc.esa.int/navipedia/index.php/Time_References_in_GNSS#GPS_Time_.28GPST.29>).
/// This may be useful for time keeping devices that use GPS as a time source.
pub fn from_gpst_nanoseconds(nanoseconds: u64) -> Self {
Self::from_duration(nanoseconds as f64 * Unit::Nanosecond, TimeScale::GPST)
Self::from_duration(Duration::from_parts(0, nanoseconds), TimeScale::GPST)
}

#[must_use]
Expand All @@ -548,13 +548,7 @@ impl Epoch {
/// defined as UTC midnight of January 5th to 6th 1980 (cf. <https://gssc.esa.int/navipedia/index.php/Time_References_in_GNSS#GPS_Time_.28GPST.29>).
/// This may be useful for time keeping devices that use QZSS as a time source.
pub fn from_qzsst_nanoseconds(nanoseconds: u64) -> Self {
Self::from_duration(
Duration {
centuries: 0,
nanoseconds,
},
TimeScale::QZSST,
)
Self::from_duration(Duration::from_parts(0, nanoseconds), TimeScale::QZSST)
}

#[must_use]
Expand All @@ -578,13 +572,7 @@ impl Epoch {
/// starting August 21st 1999 midnight (UTC)
/// (cf. <https://gssc.esa.int/navipedia/index.php/Time_References_in_GNSS>)
pub fn from_gst_nanoseconds(nanoseconds: u64) -> Self {
Self::from_duration(
Duration {
centuries: 0,
nanoseconds,
},
TimeScale::GST,
)
Self::from_duration(Duration::from_parts(0, nanoseconds), TimeScale::GST)
}

#[must_use]
Expand All @@ -606,13 +594,7 @@ impl Epoch {
/// starting on January 1st 2006 (cf. <https://gssc.esa.int/navipedia/index.php/Time_References_in_GNSS>).
/// This may be useful for time keeping devices that use BDT as a time source.
pub fn from_bdt_nanoseconds(nanoseconds: u64) -> Self {
Self::from_duration(
Duration {
centuries: 0,
nanoseconds,
},
TimeScale::BDT,
)
Self::from_duration(Duration::from_parts(0, nanoseconds), TimeScale::BDT)
}

#[must_use]
Expand Down Expand Up @@ -1451,4 +1433,4 @@ mod kani_harnesses {
let rhs: f64 = kani::any();
rem_euclid_f64(lhs, rhs);
}
}
}
1 change: 0 additions & 1 deletion src/epoch/with_funcs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -148,4 +148,3 @@ impl Epoch {
)
}
}

2 changes: 1 addition & 1 deletion src/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -277,4 +277,4 @@ impl Token {
| Token::MonthNameShort
)
}
}
}
1 change: 0 additions & 1 deletion src/timeseries.rs
Original file line number Diff line number Diff line change
Expand Up @@ -416,4 +416,3 @@ mod tests {
assert_eq!(cur_epoch, start, "incorrect last item in iterator");
}
}

35 changes: 35 additions & 0 deletions tests/epoch.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2102,3 +2102,38 @@ fn regression_test_gh_288() {
format!("{}", epoch.to_isoformat())
);
}

#[test]
fn regression_test_gh_317() {
// This bug was due to "now-ish" GNSS times being rounded when converted to f64 upon initialization from their u64 nanoseconds.

use core::str::FromStr;
let epoch = Epoch::from_str("2020-11-15 12:34:56.789 GPST").unwrap();
let nanos = epoch.to_gpst_nanoseconds().unwrap();

// We'll use these nanoseconds to initialize any of the GNSS time scales and ensure that we can retrieve the correct nanoseconds.
assert_eq!(
Epoch::from_gpst_nanoseconds(nanos)
.to_gpst_nanoseconds()
.unwrap(),
nanos
);
assert_eq!(
Epoch::from_gst_nanoseconds(nanos)
.to_gst_nanoseconds()
.unwrap(),
nanos
);
assert_eq!(
Epoch::from_bdt_nanoseconds(nanos)
.to_bdt_nanoseconds()
.unwrap(),
nanos
);
assert_eq!(
Epoch::from_qzsst_nanoseconds(nanos)
.to_qzsst_nanoseconds()
.unwrap(),
nanos
);
}

0 comments on commit 18c8471

Please sign in to comment.