From 0b8bc3d64a563e05299dbf074a521ce74aff3144 Mon Sep 17 00:00:00 2001 From: Casper Meijn Date: Wed, 21 Aug 2024 13:43:44 +0200 Subject: [PATCH] tests: Change some proptest to kani proofs Three proptests are executed as kani proofs in CI. Make that explicit by marking them as kani proof. This removes the dependency on propproof dependency when using kani. --- .github/workflows/ci.yml | 13 +---- KANI.md | 51 ++-------------- prost-types/Cargo.toml | 3 + prost-types/src/duration.rs | 109 ++++++++++++++++++----------------- prost-types/src/timestamp.rs | 33 +++++++---- 5 files changed, 86 insertions(+), 123 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7b26868b2..f3046552c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -182,19 +182,8 @@ jobs: - name: Verify with Kani uses: model-checking/kani-github-action@v0.32 with: - enable-propproof: true args: | - --tests -p prost-types --default-unwind 3 \ - --harness "tests::check_timestamp_roundtrip_via_system_time" \ - --harness "tests::check_duration_roundtrip" \ - --harness "tests::check_duration_roundtrip_nanos" - # --default-unwind N roughly corresponds to how much effort - # Kani will spend trying to prove correctness of the - # program. Higher the number, more programs can be proven - # correct. However, Kani will require more time and memory. If - # Kani fails with "Failed Checks: unwinding assertion," this - # number may need to be raised for Kani to succeed. - + -p prost-types no-std: runs-on: ubuntu-latest steps: diff --git a/KANI.md b/KANI.md index cafb0131d..a74d1b364 100644 --- a/KANI.md +++ b/KANI.md @@ -1,6 +1,5 @@ # Kani -This document describes how to **locally** install and use Kani, along -with its experimental PropProof feature. Because of instability in +This document describes how to **locally** install and use Kani. Because of instability in Kani internals, the GitHub action is the recommended option if you are running in CI. @@ -10,39 +9,15 @@ overflows, and assertion failures. See the [Kani book](https://model-checking.github.io/kani/) for a full list of capabilities and limitations. -## Installing Kani and PropProof +## Installing Kani - The install instructions for Kani can be [found here](https://model-checking.github.io/kani/install-guide.html). Once Kani is installed, you can run with `cargo kani` for projects or `kani` for individual Rust files. -- **[UNSTABLE]** To use PropProof, first download the source code - from the Kani repository. - ```bash - git clone https://github.com/model-checking/kani.git --branch features/proptest propproof - cd propproof; git submodule update --init - ``` - - Then, use `.cargo/config.toml` enable it in the local directory you - want to run Kani in. This will override the `proptest` import in - your repo. - - ```bash - cd $YOUR_REPO_LOCAL_PATH - mkdir '.cargo' - echo "paths =[\"$PATH_TO_PROPPROOF\"]" > .cargo/config.toml - ``` - -**Please Note**: -- `features/proptest` branch under Kani is likely not the final - location for this code. If these instructions stop working, please - consult the Kani documentation and file an issue on [the Kani - repo](https://github.com/model-checking/kani.git). -- The cargo config file will force cargo to always use PropProof. To - use `proptest`, delete the file. ## Running Kani -After installing Kani and PropProof, `cargo kani --tests` should -automatically run `proptest!` harnesses inside your crate. Use +After installing Kani, `cargo kani` should +automatically run `kani::proof` harnesses inside your crate. Use `--harness` to run a specific harness, and `-p` for a specific sub-crate. @@ -50,20 +25,4 @@ If Kani returns with an error, you can use the concrete playback feature using `--enable-unstable --concrete-playback print` and paste in the code to your repository. Running this harness with `cargo test` will replay the input found by Kani that produced this crash. Please -note that this feature is unstable and using `--concrete-playback -inplace` to automatically inject a replay harness is not supported -when using PropProof. - -## Debugging CI Failure -```yaml - - name: Verify with Kani - uses: model-checking/kani-github-action@v0.xx - with: - enable-propproof: true - args: | - $KANI_ARGUMENTS -``` - -The above GitHub CI workflow is equivalent to `cargo kani -$KANI_ARGUMENTS` with PropProof installed. To replicate issues -locally, run `cargo kani` with the same arguments. +note that this feature is unstable. diff --git a/prost-types/Cargo.toml b/prost-types/Cargo.toml index 87bcad3c5..8689f5ff3 100644 --- a/prost-types/Cargo.toml +++ b/prost-types/Cargo.toml @@ -21,3 +21,6 @@ prost = { version = "0.13.1", path = "../prost", default-features = false, featu [dev-dependencies] proptest = "1" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/prost-types/src/duration.rs b/prost-types/src/duration.rs index 36606cbab..42abc2385 100644 --- a/prost-types/src/duration.rs +++ b/prost-types/src/duration.rs @@ -173,69 +173,72 @@ impl FromStr for Duration { datetime::parse_duration(s).ok_or(DurationError::ParseFailure) } } -#[cfg(test)] -mod tests { + +#[cfg(kani)] +mod proofs { use super::*; #[cfg(feature = "std")] - use proptest::prelude::*; + #[kani::proof] + fn check_duration_roundtrip() { + let seconds = kani::any(); + let nanos = kani::any(); + kani::assume(nanos < 1_000_000_000); + let std_duration = std::time::Duration::new(seconds, nanos); + let Ok(prost_duration) = Duration::try_from(std_duration) else { + // Test case not valid: duration out of range + return; + }; + assert_eq!( + time::Duration::try_from(prost_duration).unwrap(), + std_duration + ); - #[cfg(feature = "std")] - proptest! { - #[test] - fn check_duration_roundtrip( - seconds in u64::arbitrary(), - nanos in 0u32..1_000_000_000u32, - ) { - let std_duration = time::Duration::new(seconds, nanos); - let prost_duration = match Duration::try_from(std_duration) { - Ok(duration) => duration, - Err(_) => return Err(TestCaseError::reject("duration out of range")), + if std_duration != time::Duration::default() { + let neg_prost_duration = Duration { + seconds: -prost_duration.seconds, + nanos: -prost_duration.nanos, }; - prop_assert_eq!(time::Duration::try_from(prost_duration).unwrap(), std_duration); - - if std_duration != time::Duration::default() { - let neg_prost_duration = Duration { - seconds: -prost_duration.seconds, - nanos: -prost_duration.nanos, - }; - - prop_assert!( - matches!( - time::Duration::try_from(neg_prost_duration), - Err(DurationError::NegativeDuration(d)) if d == std_duration, - ) - ) - } + + assert!(matches!( + time::Duration::try_from(neg_prost_duration), + Err(DurationError::NegativeDuration(d)) if d == std_duration, + )) } + } + + #[cfg(feature = "std")] + #[kani::proof] + fn check_duration_roundtrip_nanos() { + let seconds = 0; + let nanos = kani::any(); + let std_duration = std::time::Duration::new(seconds, nanos); + let Ok(prost_duration) = Duration::try_from(std_duration) else { + // Test case not valid: duration out of range + return; + }; + assert_eq!( + time::Duration::try_from(prost_duration).unwrap(), + std_duration + ); - #[test] - fn check_duration_roundtrip_nanos( - nanos in u32::arbitrary(), - ) { - let seconds = 0; - let std_duration = std::time::Duration::new(seconds, nanos); - let prost_duration = match Duration::try_from(std_duration) { - Ok(duration) => duration, - Err(_) => return Err(TestCaseError::reject("duration out of range")), + if std_duration != time::Duration::default() { + let neg_prost_duration = Duration { + seconds: -prost_duration.seconds, + nanos: -prost_duration.nanos, }; - prop_assert_eq!(time::Duration::try_from(prost_duration).unwrap(), std_duration); - - if std_duration != time::Duration::default() { - let neg_prost_duration = Duration { - seconds: -prost_duration.seconds, - nanos: -prost_duration.nanos, - }; - - prop_assert!( - matches!( - time::Duration::try_from(neg_prost_duration), - Err(DurationError::NegativeDuration(d)) if d == std_duration, - ) - ) - } + + assert!(matches!( + time::Duration::try_from(neg_prost_duration), + Err(DurationError::NegativeDuration(d)) if d == std_duration, + )) } } +} + +#[cfg(test)] +mod tests { + use super::*; #[cfg(feature = "std")] #[test] diff --git a/prost-types/src/timestamp.rs b/prost-types/src/timestamp.rs index e5be2e0f2..813d9f883 100644 --- a/prost-types/src/timestamp.rs +++ b/prost-types/src/timestamp.rs @@ -231,6 +231,27 @@ impl fmt::Display for Timestamp { datetime::DateTime::from(*self).fmt(f) } } + +#[cfg(kani)] +mod proofs { + use super::*; + + #[cfg(feature = "std")] + #[kani::proof] + #[kani::unwind(3)] + fn check_timestamp_roundtrip_via_system_time() { + let seconds = kani::any(); + let nanos = kani::any(); + + let mut timestamp = Timestamp { seconds, nanos }; + timestamp.normalize(); + + if let Ok(system_time) = std::time::SystemTime::try_from(timestamp) { + assert_eq!(Timestamp::from(system_time), timestamp); + } + } +} + #[cfg(test)] mod tests { use super::*; @@ -248,18 +269,6 @@ mod tests { ) { prop_assert_eq!(SystemTime::try_from(Timestamp::from(system_time)).unwrap(), system_time); } - - #[test] - fn check_timestamp_roundtrip_via_system_time( - seconds in i64::arbitrary(), - nanos in i32::arbitrary(), - ) { - let mut timestamp = Timestamp { seconds, nanos }; - timestamp.normalize(); - if let Ok(system_time) = SystemTime::try_from(timestamp) { - prop_assert_eq!(Timestamp::from(system_time), timestamp); - } - } } #[cfg(feature = "std")]