kani: kani fails to unwind 2 x 1 elements nested loop in firecracker code
I am running the following command
cargo kani -p arch --enable-unstable=mir-linker --harness test_msr_allowlist --restrict-vtable
on this Firecracker version: https://github.com/firecracker-microvm/firecracker/commit/99f30233a28b30bac4d041a40e2c547a4c43d8e0 with the attached patch applied, with Kani version: 0.0.1.
I expected for Kani to be able to unwind the nested loop (outer loop is 2 elements, inner loop is 1 element). Instead, I see the following output:
SUMMARY:
** 1 of 187 failed (186 undetermined)
Failed Checks: unwinding assertion loop 0
File: "/local/home/kalyazin/workspace/firecracker/src/arch/src/x86_64/msr.rs", line 354, in x86_64::msr::tests::test_msr_allowlist
VERIFICATION:- FAILED
[Kani] info: Verification output shows one or more unwinding failures.
[Kani] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.
Verification Time: 10.091045s
About this issue
- Original URL
- State: closed
- Created 2 years ago
- Comments: 18 (15 by maintainers)
The CBMC PR is now merged and will be part of the next release. No changes in Kani should be required, so once you updated to the next CBMC release this issue should be addressed (I suppose you’ll want to include a test).
I have issued a draft PR, which is waiting for me to piece together a test case.
Just an update here. I tried
--unwind 100. It took longer than 2.5 hours, but still didn’t succeed with the same error.