From c72723793d969895d94632cb460531c09b4673d1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 24 Jul 2024 13:04:09 +0000 Subject: [PATCH] chore: selectively change solvers to use with Kani CaDiCaL version 1.9.2 and later have a substantially worse performance on some instances produced by CBMC (via Kani). Use MiniSat or Kissat instead to avoid this performance penalty when running proofs with (future versions of) Kani. --- quic/s2n-quic-core/src/slice.rs | 2 +- quic/s2n-quic-platform/src/message/cmsg/tests.rs | 6 +++--- quic/s2n-quic-platform/src/message/msg/tests.rs | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/quic/s2n-quic-core/src/slice.rs b/quic/s2n-quic-core/src/slice.rs index cbe7cd381d..563f282005 100644 --- a/quic/s2n-quic-core/src/slice.rs +++ b/quic/s2n-quic-core/src/slice.rs @@ -233,7 +233,7 @@ mod tests { const LEN: usize = if cfg!(kani) { 2 } else { 32 }; #[test] - #[cfg_attr(kani, kani::proof, kani::unwind(5), kani::solver(cadical))] + #[cfg_attr(kani, kani::proof, kani::unwind(5), kani::solver(kissat))] #[cfg_attr(miri, ignore)] // This test is too expensive for miri to complete in a reasonable amount of time fn vectored_copy_fuzz_test() { check!() diff --git a/quic/s2n-quic-platform/src/message/cmsg/tests.rs b/quic/s2n-quic-platform/src/message/cmsg/tests.rs index 3e920a3e25..7555db7fb5 100644 --- a/quic/s2n-quic-platform/src/message/cmsg/tests.rs +++ b/quic/s2n-quic-platform/src/message/cmsg/tests.rs @@ -23,7 +23,7 @@ fn aligned_iter(bytes: &[u8], f: impl FnOnce(decode::Iter)) { /// Ensures the cmsg iterator doesn't crash or segfault #[test] -#[cfg_attr(kani, kani::proof, kani::solver(cadical), kani::unwind(17))] +#[cfg_attr(kani, kani::proof, kani::solver(minisat), kani::unwind(17))] fn iter_test() { check!().for_each(|bytes| { aligned_iter(bytes, |iter| { @@ -37,7 +37,7 @@ fn iter_test() { /// Ensures the `decode::Iter::collect` doesn't crash or segfault #[test] -#[cfg_attr(kani, kani::proof, kani::solver(cadical), kani::unwind(17))] +#[cfg_attr(kani, kani::proof, kani::solver(minisat), kani::unwind(17))] fn collect_test() { check!().for_each(|bytes| { aligned_iter(bytes, |iter| { @@ -117,7 +117,7 @@ type Ops = Vec; type Ops = s2n_quic_core::testing::InlineVec; #[test] -#[cfg_attr(kani, kani::proof, kani::solver(cadical), kani::unwind(9))] +#[cfg_attr(kani, kani::proof, kani::solver(kissat), kani::unwind(9))] fn round_trip_test() { check!().with_type::().for_each(|ops| round_trip(ops)); } diff --git a/quic/s2n-quic-platform/src/message/msg/tests.rs b/quic/s2n-quic-platform/src/message/msg/tests.rs index 06b48149ab..28c443d18e 100644 --- a/quic/s2n-quic-platform/src/message/msg/tests.rs +++ b/quic/s2n-quic-platform/src/message/msg/tests.rs @@ -65,7 +65,7 @@ fn address_inverse_pair_test() { #[cfg_attr( kani, kani::proof, - kani::solver(cadical), + kani::solver(minisat), kani::unwind(65), // it's safe to stub out cmsg::decode since the cmsg result isn't actually checked in this particular test kani::stub(cmsg::decode::collect, stubs::collect)