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")]