Trivial kani test takes a very long time to complete

[toidiu]

aws/s2n-quic#1508

I used the following command to execute the kani test and it took close to 30 min on my M1 mac
cargo kani --tests --harness kani_test --mir-linker --enable-unstable

    #[test]
    #[cfg_attr(kani, kani::proof, kani::unwind(9))]
    fn kani_test() {
        // Confirm that a 
        let gen = gen::<VarInt>();

        check!()
            .with_generator(gen)
            .cloned()
            .for_each(|pn| {
                let space = PacketNumberSpace::ApplicationData;
                let mut map = Map::default();
                assert!(map.is_empty());
                let pn = space.new_packet_number(pn);

                map.insert(pn, ());

                assert!(map.get(pn).is_some());
                assert!(!map.is_empty());
            });
    }

[celinval]

Hi @toidiu, thanks for raising this issue. Is the verification step the one that is taking most of the time?

[celinval]

Looking at #1713, I'm assuming that the verification is the culprit. @zhassan-aws do you have any insight on what might help here?

[zhassan-aws]

I ran it on my end with the MIR linker, and it takes less than a minute, so it's likely that the 30 minutes was dominated by compilation time:

$ git branch
* ak-kani_pnm
  camshaft/varint-kani
  concrete-playback
  interval_set_insert_test
  main
$ pwd
/home/ubuntu/git/s2n-quic/quic/s2n-quic-core
$ cargo clean
$ /usr/bin/time -p cargo kani --tests --harness insert_value --enable-unstable --mir-linker
<snip>
SUMMARY:
 ** 0 of 1271 failed (15 unreachable)

VERIFICATION:- SUCCESSFUL

Verification Time: 4.1324267s
real 31.07
user 52.12
sys 5.63

[camshaft]

I'm seeing both long compilation and verification times.

Runtime Symex: 9.51718s
size of program expression: 95755 steps
slicing removed 51665 assignments
Generated 9068 VCC(s), 4618 remaining after simplification
Runtime Postprocess Equation: 0.0973145s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 1.09764s
Running propositional reduction
Post-processing
Runtime Post-process: 447.195s

The cbmc process was consuming 22GiB and about 30% CPU for the majority of the run

[zhassan-aws]

@camshaft This was without the MIR linker?

[camshaft]

yeah MIR linker:

$ cargo kani --tests --harness insert_value --mir-linker --enable-unstable

[toidiu]

I'm seeing both long compilation and verification times.

Correct, both compilation and verification took long and I was also using miri linker. This was run on a M1 mac if that makes a difference.

[zhassan-aws]

Ah, looks like #1717 brings down the time considerably; I observed the high memory usage with the previous commit (f3b5a97). The next release, which should be out on Tuesday 10/4 will include #1717.