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

[roypat]

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]

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.