From fdbb893350e7496e823a1704450fbe843f6a250c Mon Sep 17 00:00:00 2001 From: Joshua Liebow-Feeser Date: Mon, 18 Sep 2023 17:13:33 -0700 Subject: [PATCH] [ci] Run byteorder tests under Kani (#394) Co-authored-by: Jack Wrenn --- .github/workflows/ci.yml | 25 ++++++++ src/byteorder.rs | 122 +++++++++++++++++++++++++++++++-------- src/lib.rs | 2 +- 3 files changed, 125 insertions(+), 24 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6b048be24c..5a091aa3cb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -239,6 +239,29 @@ jobs: rust-toolchain: nightly if: matrix.crate == 'zerocopy' && matrix.features == '--all-features' && matrix.toolchain == 'nightly' + kani: + runs-on: ubuntu-latest + name: Run tests under Kani + needs: generate_cache + steps: + - uses: actions/checkout@3df4ab11eba7bda6032a0b82a6bb43b11571feac # v4.0.0 + - name: Configure ZC_TOOLCHAIN environment variable + run: | + set -eo pipefail + echo "ZC_TOOLCHAIN=$(./cargo.sh --version nightly)" >> $GITHUB_ENV + - name: Install nigtly Rust toolchain (${{ env.ZC_TOOLCHAIN }}) + uses: dtolnay/rust-toolchain@00b49be78f40fba4e87296b2ead62868750bdd83 # stable + with: + toolchain: ${{ env.ZC_TOOLCHAIN }} + - run: | + set -eo pipefail + cargo install --locked kani-verifier + cargo kani setup + RUSTFLAGS="$ZC_NIGHTLY_RUSTFLAGS" ./cargo.sh +nightly kani \ + --package zerocopy --all-features --output-format terse --randomize-layout \ + --memory-safety-checks --overflow-checks --undefined-function-checks \ + --unwinding-checks + check_fmt: runs-on: ubuntu-latest name: Check Rust formatting @@ -428,3 +451,5 @@ jobs: cargo check --workspace --tests &> /dev/null || true cargo metadata &> /dev/null || true cargo install cargo-readme --version 3.2.0 &> /dev/null || true + cargo install --locked kani-verifier &> /dev/null || true + cargo kani setup &> /dev/null || true diff --git a/src/byteorder.rs b/src/byteorder.rs index ecee7a07c9..01c3c4751f 100644 --- a/src/byteorder.rs +++ b/src/byteorder.rs @@ -495,22 +495,61 @@ module!(little_endian, LittleEndian, "little-endian"); module!(network_endian, NetworkEndian, "network-endian"); module!(native_endian, NativeEndian, "native-endian"); -#[cfg(test)] +#[cfg(any(test, kani))] mod tests { use ::byteorder::NativeEndian; - use rand::{ - distributions::{Distribution, Standard}, - rngs::SmallRng, - Rng, SeedableRng, - }; use { super::*, crate::{AsBytes, FromBytes, Unaligned}, }; + #[cfg(not(kani))] + mod compatibility { + pub(super) use rand::{ + distributions::{Distribution, Standard}, + rngs::SmallRng, + Rng, SeedableRng, + }; + + pub(crate) trait Arbitrary {} + + impl Arbitrary for T {} + } + + #[cfg(kani)] + mod compatibility { + pub(crate) use kani::Arbitrary; + + pub(crate) struct SmallRng; + + impl SmallRng { + pub(crate) fn seed_from_u64(_state: u64) -> Self { + Self + } + } + + pub(crate) trait Rng { + fn sample>(&mut self, _distr: D) -> T + where + T: Arbitrary, + { + kani::any() + } + } + + impl Rng for SmallRng {} + + pub(crate) trait Distribution {} + impl Distribution for U {} + + pub(crate) struct Standard; + } + + use compatibility::*; + // A native integer type (u16, i32, etc). - trait Native: FromBytes + AsBytes + Copy + PartialEq + Debug { + trait Native: Arbitrary + FromBytes + AsBytes + Copy + PartialEq + Debug { const ZERO: Self; const MAX_VALUE: Self; @@ -520,6 +559,13 @@ mod tests { fn rand(rng: &mut R) -> Self { rng.sample(Self::DIST) } + + #[cfg(kani)] + fn any() -> Self { + kani::any() + } + + fn is_nan(self) -> bool; } trait ByteArray: @@ -572,7 +618,7 @@ mod tests { } macro_rules! impl_traits { - ($name:ident, $native:ident, $bytes:expr, $sign:ident) => { + ($name:ident, $native:ident, $bytes:expr, $sign:ident $(, $is_nan:ident)?) => { impl Native for $native { // For some types, `0 as $native` is required (for example, when // `$native` is a floating-point type; `0` is an integer), but @@ -584,6 +630,10 @@ mod tests { type Distribution = Standard; const DIST: Standard = Standard; + + fn is_nan(self) -> bool { + false $(|| self.$is_nan())? + } } impl ByteOrderType for $name { @@ -625,8 +675,8 @@ mod tests { impl_traits!(I32, i32, 4, signed); impl_traits!(I64, i64, 8, signed); impl_traits!(I128, i128, 16, signed); - impl_traits!(F32, f32, 4, signed); - impl_traits!(F64, f64, 8, signed); + impl_traits!(F32, f32, 4, signed, is_nan); + impl_traits!(F64, f64, 8, signed, is_nan); macro_rules! call_for_all_types { ($fn:ident, $byteorder:ident) => { @@ -663,7 +713,7 @@ mod tests { // conditional compilation by `target_pointer_width`. const RNG_SEED: u64 = 0x7A03CAE2F32B5B8F; - const RAND_ITERS: usize = if cfg!(miri) { + const RAND_ITERS: usize = if cfg!(any(miri, kani)) { // The tests below which use this constant used to take a very long time // on Miri, which slows down local development and CI jobs. We're not // using Miri to check for the correctness of our code, but rather its @@ -687,7 +737,8 @@ mod tests { 1024 }; - #[test] + #[cfg_attr(test, test)] + #[cfg_attr(kani, kani::proof)] fn test_zero() { fn test_zero() { assert_eq!(T::ZERO.get(), T::Native::ZERO); @@ -697,7 +748,8 @@ mod tests { call_for_all_types!(test_zero, NonNativeEndian); } - #[test] + #[cfg_attr(test, test)] + #[cfg_attr(kani, kani::proof)] fn test_max_value() { fn test_max_value() { assert_eq!(T::MAX_VALUE.get(), T::Native::MAX_VALUE); @@ -707,7 +759,8 @@ mod tests { call_for_unsigned_types!(test_max_value, NonNativeEndian); } - #[test] + #[cfg_attr(test, test)] + #[cfg_attr(kani, kani::proof)] fn test_native_endian() { fn test_native_endian() { let mut r = SmallRng::seed_from_u64(RNG_SEED); @@ -717,22 +770,34 @@ mod tests { bytes.as_bytes_mut().copy_from_slice(native.as_bytes()); let mut from_native = T::new(native); let from_bytes = T::from_bytes(bytes); - assert_eq!(from_native, from_bytes); - assert_eq!(from_native.get(), native); - assert_eq!(from_bytes.get(), native); + + // For `f32` and `f64`, NaN values are not considered equal to + // themselves. + if !T::Native::is_nan(native) { + assert_eq!(from_native, from_bytes); + assert_eq!(from_native.get(), native); + assert_eq!(from_bytes.get(), native); + } + assert_eq!(from_native.into_bytes(), bytes); assert_eq!(from_bytes.into_bytes(), bytes); let updated = T::Native::rand(&mut r); from_native.set(updated); - assert_eq!(from_native.get(), updated); + + // For `f32` and `f64`, NaN values are not considered equal to + // themselves. + if !T::Native::is_nan(from_native.get()) { + assert_eq!(from_native.get(), updated); + } } } call_for_all_types!(test_native_endian, NativeEndian); } - #[test] + #[cfg_attr(test, test)] + #[cfg_attr(kani, kani::proof)] fn test_non_native_endian() { fn test_non_native_endian() { let mut r = SmallRng::seed_from_u64(RNG_SEED); @@ -743,15 +808,26 @@ mod tests { bytes = bytes.invert(); let mut from_native = T::new(native); let from_bytes = T::from_bytes(bytes); - assert_eq!(from_native, from_bytes); - assert_eq!(from_native.get(), native); - assert_eq!(from_bytes.get(), native); + + // For `f32` and `f64`, NaN values are not considered equal to + // themselves. + if !T::Native::is_nan(native) { + assert_eq!(from_native, from_bytes); + assert_eq!(from_native.get(), native); + assert_eq!(from_bytes.get(), native); + } + assert_eq!(from_native.into_bytes(), bytes); assert_eq!(from_bytes.into_bytes(), bytes); let updated = T::Native::rand(&mut r); from_native.set(updated); - assert_eq!(from_native.get(), updated); + + // For `f32` and `f64`, NaN values are not considered equal to + // themselves. + if !T::Native::is_nan(from_native.get()) { + assert_eq!(from_native.get(), updated); + } } } diff --git a/src/lib.rs b/src/lib.rs index dae778bbaf..7f7170e6dc 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -147,7 +147,7 @@ )] // In test code, it makes sense to weight more heavily towards concise, readable // code over correct or debuggable code. -#![cfg_attr(test, allow( +#![cfg_attr(any(test, kani), allow( // In tests, you get line numbers and have access to source code, so panic // messages are less important. You also often unwrap a lot, which would // make expect'ing instead very verbose.