Change f32::midpoint to upcast to f64 · model-checking/verify-rust-std@e929c7f (original) (raw)
`@@ -719,7 +719,7 @@ assume_usize_width! {
`
719
719
`}
`
720
720
``
721
721
`macro_rules! test_float {
`
722
``
`-
($modname: ident, fty:ty,fty: ty, fty:ty,inf: expr, neginf:expr,neginf: expr, neginf:expr,nan: expr, min:expr,min: expr, min:expr,max: expr, $min_pos: expr) => {
`
``
722
`+
($modname: ident, fty:ty,fty: ty, fty:ty,inf: expr, neginf:expr,neginf: expr, neginf:expr,nan: expr, min:expr,min: expr, min:expr,max: expr, minpos:expr,min_pos: expr, minpos:expr,max_exp:expr) => {
`
723
723
`mod $modname {
`
724
724
` #[test]
`
725
725
`fn min() {
`
`@@ -870,6 +870,27 @@ macro_rules! test_float {
`
870
870
` assert!(($nan as $fty).midpoint(1.0).is_nan());
`
871
871
` assert!((1.0 as fty).midpoint(fty).midpoint(fty).midpoint(nan).is_nan());
`
872
872
` assert!(($nan as fty).midpoint(fty).midpoint(fty).midpoint(nan).is_nan());
`
``
873
+
``
874
`+
// test if large differences in magnitude are still correctly computed.
`
``
875
`+
// NOTE: that because of how small x and y are, x + y can never overflow
`
``
876
`+
// so (x + y) / 2.0 is always correct
`
``
877
`` +
// in particular, 2.pow(i) will never be at the max exponent, so it could
``
``
878
`+
// be safely doubled, while j is significantly smaller.
`
``
879
`+
for i in maxexp.saturatingsub(64)..max_exp.saturating_sub(64)..maxexp.saturatingsub(64)..max_exp {
`
``
880
`+
for j in 0..64u8 {
`
``
881
`+
let large = <$fty>::from(2.0f32).powi(i);
`
``
882
`+
// a much smaller number, such that there is no chance of overflow to test
`
``
883
`+
// potential double rounding in midpoint's implementation.
`
``
884
`+
let small = <$fty>::from(2.0f32).powi($max_exp - 1)
`
``
885
`+
- <$fty>::EPSILON
`
``
886
`+
- <$fty>::from(j);
`
``
887
+
``
888
`+
let naive = (large + small) / 2.0;
`
``
889
`+
let midpoint = large.midpoint(small);
`
``
890
+
``
891
`+
assert_eq!(naive, midpoint);
`
``
892
`+
}
`
``
893
`+
}
`
873
894
`}
`
874
895
` #[test]
`
875
896
`fn rem_euclid() {
`
`@@ -902,7 +923,8 @@ test_float!(
`
902
923
`f32::NAN,
`
903
924
`f32::MIN,
`
904
925
`f32::MAX,
`
905
``
`-
f32::MIN_POSITIVE
`
``
926
`+
f32::MIN_POSITIVE,
`
``
927
`+
f32::MAX_EXP
`
906
928
`);
`
907
929
`test_float!(
`
908
930
`f64,
`
`@@ -912,5 +934,6 @@ test_float!(
`
912
934
`f64::NAN,
`
913
935
`f64::MIN,
`
914
936
`f64::MAX,
`
915
``
`-
f64::MIN_POSITIVE
`
``
937
`+
f64::MIN_POSITIVE,
`
``
938
`+
f64::MAX_EXP
`
916
939
`);
`