search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.24k stars 93 forks source link

Replacing `Vec` with `SmallVec` causes CMBC's memory usage to grow unboundedly during post-processing #2944

Open roypat opened 11 months ago

roypat commented 11 months ago

Hi all, Over at Firecracker we recently had to make some changes to our virtio code (which is covered by kani harnesses). As part of this, we replaced a Vec with a SmallVec for performance reasons (as descriptor chains heuristically are "short", so by using a SmallVec we can avoid an allocation most of the time). However, the harnesses at https://github.com/firecracker-microvm/firecracker/blob/main/src/vmm/src/devices/virtio/iovec.rs#L714 started timing out in our CI after that. Investigating manually showed that after the Symex step, Kani seemingly gets stuck in its post-processing phase, where CMBC just slowly uses more and more RAM until the system locks up.

To reproduce, remove the cfg directives at https://github.com/firecracker-microvm/firecracker/blob/036d9906a09ed759597ee88bab6c1278e4fd7655/src/vmm/src/devices/virtio/iovec.rs#L28-L31 and try to run the iovec harnesses.

Command line invocation:

cargo kani --enable-unstable -Z stubbing -Z function-contracts --restrict-vtable -j --output-format terse --harness iovec

Kani version: 0.41.0

tautschnig commented 11 months ago

The symptoms point to a use of arrays of non-fixed size. It's not really obvious to me from SmallVec's documentation why we newly should end up with such, so I'll have to look at the intermediate representation that's being produced.