test(s2n-quic-core): add a bolero harness for the varint table #1584
Conversation
|
|
||
| #[test] | ||
| #[cfg_attr(miri, ignore)] // This test is too expensive for miri to complete in a reasonable amount of time | ||
| fn round_trip() { | ||
| fn round_trip_bytes_test() { |
There was a problem hiding this comment.
Is Kani unable to handle this one?
There was a problem hiding this comment.
I tried it but it kept wanting a higher unwind value. I put kani::unwind(50) and it still complained. I also put a kani::assume(bytes.len() <= 8) and it didn't make a difference, unfortunately. I didn't want to block the rest of these proofs on it, though, but definitely worth exploring.
There was a problem hiding this comment.
I see. I'll investigate.
There was a problem hiding this comment.
It seems there's a loop that requires an unwinding greater than 256. Setting the unwind to 256 results in an unwinding assertion failure:
Check 941: std::array::try_collect_into_array::<std::iter::Map<&mut std::iter::Map<std::array::IntoIter<(), 256>, [closure@<[u8; 256] as kani::Arbitrary>::any::{closure#0}]>, fn(u8) -> std::ops::try_trait::NeverShortCircuit<u8> {std::ops::try_trait::NeverShortCircuit::<u8>}>, u8, std::ops::try_trait::NeverShortCircuitResidual, 256>.unwind.0
- Status: FAILURE
- Description: "unwinding assertion loop 0"
- Location: ../../../../.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/array/mod.rs:884:21 in function std::array::try_collect_into_array::<std::iter::Map<&mut std::iter::Map<std::array::IntoIter<(), 256>, [closure@<[u8; 256] as kani::Arbitrary>::any::{closure#0}]>, fn(u8) -> std::ops::try_trait::NeverShortCircuit<u8> {std::ops::try_trait::NeverShortCircuit::<u8>}>, u8, std::ops::try_trait::NeverShortCircuitResidual, 256>
and with 257, it keeps unwinding till it runs out of memory :(
There was a problem hiding this comment.
| } | ||
|
|
||
| #[test] | ||
| #[cfg_attr(kani, kani::proof, kani::unwind(5))] |
There was a problem hiding this comment.
Is an unwind annotation necessary?
There was a problem hiding this comment.
I can try it without. Although, generally I've just put unwind values on every harness. We had a harness that didn't have an unwind (worked fine) and upgraded kani and then it unwound forever.
There was a problem hiding this comment.
yep that completes without. but like I mentioned, I think I prefer the explicit unwind value TBH.
Description of changes:
I had a branch from ~6 months ago that included a kani proof showing that the optimized version of the varint table matches the non-optimized version that more clearly matches what the RFC describes. It also included a proof that the math operations matched the underlying
u64operations, when possible.Testing:
CI Job
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.