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.

[zhassan-aws]

Confirmed that 5539c0d brings down memory usage and run time significantly.

[celinval]

@camshaft / @toidiu can you please post the total time, compilation time and verification time that you are experiencing? I tested before and after #1717 was merged. With the MIR Linker, the compilation time didn't change much (it's about 20s for me), but the verification time and memory consumption has changed dramatically.

@tautschnig this is puzzling me quite a bit. The #1717 has fixed the missing symbols problem with the std library, and it actually increases the amount of functions / static that we are translating into goto model (from 356 to 1139). How come the verification time drops down dramatically like that?

Could it affect constant propagation?? We encode missing definitions as assert(false); assume(false).

What happens if we have the following code:

let my_const = if any() { 10 } else { missing_method() };

will constant propagation be able to assign 10 to my_const?

[zhassan-aws]

Version 0.12.0 was released on Tuesday. @toidiu @camshaft can you confirm if this harness now finishes quickly (with --enable-unstable --mir-linker)?

[camshaft]

If I run that on my x86 macbook it's now super fast! That seems to have addressed the issue. However on my Linux machine I'm seeing a verification error, even after nuking /target:

...
 518   │ Check 95: std::option::Option::<usize>::unwrap.unreachable.1
 519   │      - Status: SUCCESS
 520   │      - Description: "unreachable code"
 521   │      - Location: ../../../../../../runner/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs:773:15 in function std::option::Option::<usize>::unwrap
 522   │
 523   │ Check 96: memcpy$link1.assertion.1
 524   │      - Status: FAILURE
 525   │      - Description: "undefined function should be unreachable"
 526   │      - Location: <builtin-library-memcpy> in function memcpy$link1
 527   │
 528   │ Check 97: std::vec::Vec::<std::option::Option<()>>::as_mut_ptr.assume.1
 529   │      - Status: SUCCESS
 530   │      - Description: "assumption failed"
 531   │      - Location: ../../../../../../runner/.rustup/toolchains/nightly-2022-09-13-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs:1210:13 in function std::vec::Vec::<std::option::Option<()>>::as_mut_ptr
 532   │
...

SUMMARY:
 ** 1 of 1104 failed (24 unreachable)
Failed Checks: undefined function should be unreachable

VERIFICATION:- FAILED

Verification Time: 0.4641839s

This may be worth opening another issue for, though.

[tedinski]

The $link1 is weird, I haven't seen that before. I am noticing this comment in CBMC:

    // Linker renaming may have added $linkN suffixes to the name, and other
    // suffixes such as #return_value may have then be subsequently added.
    // Strip out the first $linkN substring and then see if the criterion holds

So we might be triggering something weird in CBMC?

[tautschnig]

I looks like you have multiple declarations of memcpy, which is weird in several ways: do you now link together multiple object files via goto-cc or in the call to CBMC?

[tautschnig]

@tautschnig this is puzzling me quite a bit. The #1717 has fixed the missing symbols problem with the std library, and it actually increases the amount of functions / static that we are translating into goto model (from 356 to 1139). How come the verification time drops down dramatically like that?

Could it affect constant propagation?? We encode missing definitions as assert(false); assume(false).

What happens if we have the following code:

let my_const = if any() { 10 } else { missing_method() };

will constant propagation be able to assign 10 to my_const?

My apologies for the late response! Yes, such constant propagation should take place, but also it might be that you're now providing definitions that result in precisely specified behaviour where previously a lot of non-determinism was present. But that's all guess work, I'd have to look at this in much more detail if this is still relevant.

[tedinski]

Perhaps the memcpy issue is another manifestation of our just mashing all the tests together when they were originally multiple binaries? Was this built with --tests ?

• cargo kani --tests fails on crates with integration tests #1448

Weird that it only affects one platform though.

[tautschnig]

It might be worth doing a goto-instrument --show-symbol-table on those binaries.

[celinval]

Perhaps the memcpy issue is another manifestation of our just mashing all the tests together when they were originally multiple binaries? Was this built with --tests ?

* [cargo kani --tests fails on crates with integration tests #1448](https://github.com/model-checking/kani/issues/1448)

Weird that it only affects one platform though.

I don't think that's related to #1448. In this issue, the cargo command fails to run in the first place.

[celinval]

I created a new issue to track the spurious failure. I'll take a look at it today.

[camshaft]

I think we can call this ticket closed, yeah?

[zhassan-aws]

Closing per the comment above.