Skip to content

Commit ff0b5bf

Browse files
ShoyuVanillaShoyuVanilla
authored
Add harnesses for safety of primitive conversions (model-checking#233)
Towards model-checking#220 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent e2146fa commit ff0b5bf

File tree

1 file changed

+337
-0
lines changed
  • library/core/src/convert

1 file changed

+337
-0
lines changed

‎library/core/src/convert/num.rs

+337
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,10 @@
1+
use safety::requires;
2+
3+
#[cfg(kani)]
4+
use crate::kani;
15
use crate::num::TryFromIntError;
6+
#[allow(unused_imports)]
7+
use crate::ub_checks::float_to_int_in_range;
28

39
mod private {
410
/// This trait being unreachable from outside the crate
@@ -25,6 +31,9 @@ macro_rules! impl_float_to_int {
2531
#[unstable(feature = "convert_float_to_int", issue = "67057")]
2632
impl FloatToInt<$Int> for $Float {
2733
#[inline]
34+
#[requires(
35+
self.is_finite() && float_to_int_in_range::<$Float, $Int>(self)
36+
)]
2837
unsafe fn to_int_unchecked(self) -> $Int {
2938
// SAFETY: the safety contract must be upheld by the caller.
3039
unsafe { crate::intrinsics::float_to_int_unchecked(self) }
@@ -540,3 +549,331 @@ impl_nonzero_int_try_from_nonzero_int!(i32 => u8, u16, u32, u64, u128, usize);
540549
impl_nonzero_int_try_from_nonzero_int!(i64 => u8, u16, u32, u64, u128, usize);
541550
impl_nonzero_int_try_from_nonzero_int!(i128 => u8, u16, u32, u64, u128, usize);
542551
impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize);
552+
553+
#[cfg(kani)]
554+
#[unstable(feature = "kani", issue = "none")]
555+
mod verify {
556+
use super::*;
557+
558+
// Generate harnesses for `NonZero::<Large>::from(NonZero<Small>)`.
559+
macro_rules! generate_nonzero_int_from_nonzero_int_harness {
560+
($Small:ty => $Large:ty, $harness:ident) => {
561+
#[kani::proof]
562+
pub fn $harness() {
563+
let x: NonZero<$Small> = kani::any();
564+
let _ = NonZero::<$Large>::from(x);
565+
}
566+
};
567+
}
568+
569+
// This bundles the calls to `generate_nonzero_int_from_nonzero_int_harness`
570+
// macro into segregated namespaces for better organization and usability.
571+
macro_rules! generate_nonzero_int_from_nonzero_int_harnesses {
572+
($ns:ident, $Small:ty => $($Large:tt),+ $(,)?) => {
573+
mod $ns {
574+
use super::*;
575+
576+
$(
577+
mod $Large {
578+
use super::*;
579+
580+
generate_nonzero_int_from_nonzero_int_harness!(
581+
$Small => $Large,
582+
check_nonzero_int_from_nonzero_int
583+
);
584+
}
585+
)+
586+
}
587+
};
588+
}
589+
590+
// non-zero unsigned integer -> non-zero integer, infallible
591+
generate_nonzero_int_from_nonzero_int_harnesses!(
592+
check_nonzero_int_from_u8,
593+
u8 => u16, u32, u64, u128, usize, i16, i32, i64, i128, isize,
594+
);
595+
generate_nonzero_int_from_nonzero_int_harnesses!(
596+
check_nonzero_int_from_u16,
597+
u16 => u32, u64, u128, usize, i32, i64, i128,
598+
);
599+
generate_nonzero_int_from_nonzero_int_harnesses!(
600+
check_nonzero_int_from_u32,
601+
u32 => u64, u128, i64, i128,
602+
);
603+
generate_nonzero_int_from_nonzero_int_harnesses!(
604+
check_nonzero_int_from_u64,
605+
u64 => u128, i128,
606+
);
607+
608+
// non-zero signed integer -> non-zero signed integer, infallible
609+
generate_nonzero_int_from_nonzero_int_harnesses!(
610+
check_nonzero_int_from_i8,
611+
i8 => i16, i32, i64, i128, isize,
612+
);
613+
generate_nonzero_int_from_nonzero_int_harnesses!(
614+
check_nonzero_int_from_i16,
615+
i16 => i32, i64, i128, isize,
616+
);
617+
generate_nonzero_int_from_nonzero_int_harnesses!(
618+
check_nonzero_int_from_i32,
619+
i32 => i64, i128,
620+
);
621+
generate_nonzero_int_from_nonzero_int_harnesses!(
622+
check_nonzero_int_from_i64,
623+
i64 => i128,
624+
);
625+
626+
// Generates harnesses for `NonZero::<target>::try_from(NonZero<source>)`.
627+
// Since the function may be fallible or infallible depending on `source` and `target`,
628+
// this macro supports generating both cases.
629+
macro_rules! generate_nonzero_int_try_from_nonzero_int_harness {
630+
// Passing two identities - one for pass and one for panic - generates harnesses
631+
// for fallible cases.
632+
($source:ty => $target:ty, $harness_pass:ident, $harness_panic:ident $(,)?) => {
633+
#[kani::proof]
634+
pub fn $harness_pass() {
635+
let x_inner: $source = kani::any_where(|&v| {
636+
(v > 0 && (v as u128) <= (<$target>::MAX as u128))
637+
|| (v < 0 && (v as i128) >= (<$target>::MIN as i128))
638+
});
639+
let x = NonZero::new(x_inner).unwrap();
640+
let _ = NonZero::<$target>::try_from(x).unwrap();
641+
}
642+
643+
#[kani::proof]
644+
#[kani::should_panic]
645+
pub fn $harness_panic() {
646+
let x_inner: $source = kani::any_where(|&v| {
647+
(v > 0 && (v as u128) > (<$target>::MAX as u128))
648+
|| (v < 0 && (v as i128) < (<$target>::MIN as i128))
649+
|| (v == 0)
650+
});
651+
let x = NonZero::new(x_inner).unwrap();
652+
let _ = NonZero::<$target>::try_from(x).unwrap();
653+
}
654+
};
655+
// Passing a single identity generates harnesses for infallible cases.
656+
($source:ty => $target:ty, $harness_infallible:ident $(,)?) => {
657+
#[kani::proof]
658+
pub fn $harness_infallible() {
659+
let x: NonZero<$source> = kani::any();
660+
let _ = NonZero::<$target>::try_from(x).unwrap();
661+
}
662+
};
663+
}
664+
665+
// This bundles the calls to `generate_nonzero_int_try_from_nonzero_int_harness`
666+
// macro into segregated namespaces for better organization and usability.
667+
// Conversions from the source type to the target types inside the first pair
668+
// of square brackets are fallible, while those to the second pairs are
669+
// infallible.
670+
macro_rules! generate_nonzero_int_try_from_nonzero_int_harnesses {
671+
($ns:ident, $source:ty => ([$($target:tt),* $(,)?], [$($infallible:tt),* $(,)?] $(,)?)) => {
672+
mod $ns {
673+
use super::*;
674+
675+
$(
676+
mod $target {
677+
use super::*;
678+
679+
generate_nonzero_int_try_from_nonzero_int_harness!(
680+
$source => $target,
681+
check_nonzero_int_try_from_nonzero_int,
682+
check_nonzero_int_try_from_nonzero_int_should_panic,
683+
);
684+
}
685+
)*
686+
$(
687+
mod $infallible {
688+
use super::*;
689+
690+
generate_nonzero_int_try_from_nonzero_int_harness!(
691+
$source => $infallible,
692+
check_nonzero_int_try_from_nonzero_int_infallible,
693+
);
694+
}
695+
)*
696+
}
697+
};
698+
}
699+
700+
// unsigned non-zero integer -> non-zero integer fallible
701+
#[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))]
702+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
703+
check_nonzero_int_try_from_u16,
704+
u16 => (
705+
[u8, i8, i16],
706+
[isize],
707+
)
708+
);
709+
710+
#[cfg(target_pointer_width = "16")]
711+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
712+
check_nonzero_int_try_from_u16,
713+
u16 => (
714+
[u8, i8, i16, isize],
715+
[],
716+
)
717+
);
718+
719+
#[cfg(target_pointer_width = "64")]
720+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
721+
check_nonzero_int_try_from_u32,
722+
u32 => (
723+
[u8, u16, i8, i16, i32],
724+
[usize, isize],
725+
)
726+
);
727+
728+
#[cfg(target_pointer_width = "32")]
729+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
730+
check_nonzero_int_try_from_u32,
731+
u32 => (
732+
[u8, u16, i8, i16, i32, isize],
733+
[usize],
734+
)
735+
);
736+
737+
#[cfg(target_pointer_width = "16")]
738+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
739+
check_nonzero_int_try_from_u32,
740+
u32 => (
741+
[u8, u16, usize, i8, i16, i32, isize],
742+
[],
743+
)
744+
);
745+
746+
#[cfg(target_pointer_width = "64")]
747+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
748+
check_nonzero_int_try_from_u64,
749+
u64 => (
750+
[u8, u16, u32, i8, i16, i32, i64, isize],
751+
[usize],
752+
)
753+
);
754+
755+
#[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))]
756+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
757+
check_nonzero_int_try_from_u64,
758+
u64 => (
759+
[u8, u16, u32, usize, i8, i16, i32, i64, isize],
760+
[],
761+
)
762+
);
763+
764+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
765+
check_nonzero_int_try_from_u128,
766+
u128 => (
767+
[u8, u16, u32, u64, usize, i8, i16, i32, i64, i128, isize],
768+
[],
769+
)
770+
);
771+
772+
// signed non-zero integer -> non-zero integer fallible
773+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
774+
check_nonzero_int_try_from_i8,
775+
i8 => (
776+
[u8, u16, u32, u64, u128, usize],
777+
[],
778+
)
779+
);
780+
781+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
782+
check_nonzero_int_try_from_i16,
783+
i16 => (
784+
[u8, u16, u32, u64, u128, usize, i8],
785+
[],
786+
)
787+
);
788+
789+
#[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))]
790+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
791+
check_nonzero_int_try_from_i32,
792+
i32 => (
793+
[u8, u16, u32, u64, u128, usize, i8, i16],
794+
[isize],
795+
)
796+
);
797+
798+
#[cfg(target_pointer_width = "16")]
799+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
800+
check_nonzero_int_try_from_i32,
801+
i32 => (
802+
[u8, u16, u32, u64, u128, usize, i8, i16, isize],
803+
[],
804+
)
805+
);
806+
807+
#[cfg(target_pointer_width = "64")]
808+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
809+
check_nonzero_int_try_from_i64,
810+
i64 => (
811+
[u8, u16, u32, u64, u128, usize, i8, i16, i32],
812+
[isize],
813+
)
814+
);
815+
816+
#[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))]
817+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
818+
check_nonzero_int_try_from_i64,
819+
i64 => (
820+
[u8, u16, u32, u64, u128, usize, i8, i16, i32, isize],
821+
[],
822+
)
823+
);
824+
825+
generate_nonzero_int_try_from_nonzero_int_harnesses!(
826+
check_nonzero_int_try_from_i128,
827+
i128 => (
828+
[u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, isize],
829+
[],
830+
)
831+
);
832+
833+
// Generate harnesses for `<Float as FloatToInt<Int>>::to_int_unchecked(self)`.
834+
macro_rules! generate_float_to_int_harness {
835+
($Float:ty => $Int:ty, $harness:ident) => {
836+
#[kani::proof_for_contract(<$Float>::to_int_unchecked)]
837+
pub fn $harness() {
838+
let x: $Float = kani::any();
839+
let _: $Int = unsafe { x.to_int_unchecked() };
840+
}
841+
};
842+
}
843+
844+
// This bundles the calls to `generate_float_to_int_harness` macro into segregated
845+
// namespaces for better organization and usability.
846+
macro_rules! generate_float_to_int_harnesses {
847+
($ns:ident, $(($Float:tt => $($Int:tt),+ $(,)?)),+ $(,)?) => {
848+
mod $ns {
849+
use super::*;
850+
851+
$(
852+
mod $Float {
853+
use super::*;
854+
855+
$(
856+
mod $Int {
857+
use super::*;
858+
859+
generate_float_to_int_harness!(
860+
$Float => $Int,
861+
check_float_to_int_unchecked
862+
);
863+
}
864+
)+
865+
}
866+
)+
867+
}
868+
};
869+
}
870+
871+
// float -> integer unchecked
872+
generate_float_to_int_harnesses!(
873+
check_f16_to_int_unchecked,
874+
(f16 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize),
875+
(f32 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize),
876+
(f64 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize),
877+
(f128 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize),
878+
);
879+
}

0 commit comments

Comments
 (0)