kani fails to unwind 2 x 1 elements nested loop in firecracker code

[kalyazin]

I am running the following command

cargo kani -p arch --enable-unstable=mir-linker --harness test_msr_allowlist --restrict-vtable

on this Firecracker version:
firecracker-microvm/firecracker@99f3023
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

0001-kani-unwinding-failures.patch.txt

[adpaco-aws]

Thanks for the bug report, @kalyazin !

Unfortunately, this means you need to keep increasing the unwind value until the unwinding failure doesn't show. The reason is that the underlying code may contain loops that you cannot see directly. Have you tried increasing the unwinding value or is does it take too long in that case?

[kalyazin]

@adpaco-aws , thanks for getting back.
I have just inspected the underlying code, it adds x2 complexity:

ALLOWED_MSR_RANGES.iter().any(|range| range.contains(index))

ALLOWED_MSR_RANGES has 2 elements now. So the overall complexity is 2 x 1 x 2 which is 4.
I'm using the following command now:

cargo kani -p arch --enable-unstable=mir-linker --harness test_msr_allowlist --restrict-vtable --unwind 20

I believe unwinding value 20 should be well enough to cover 4 iterations. Am I missing something?

[adpaco-aws]

@kalyazin as I mentioned, the code underneath those methods may contain loops which require a higher unwinding limit. We acknowledge this isn't intuitive at the moment. Our recommendation is:

1. Increase the unwinding value until you don't get failures. It's not a problem to unwind more than you need (only performance may suffer) so you can use increments higher than one. For your example, I would increase by 5 or 10 each time you get an unwinding assertion in your example.
2. Now that the proof completes without unwinding assertions. The goal is to reduce the unwinding value to the minimum needed for the unwinding assertion to not fail. So keep decreasing it in smaller quantities (e.g., 2 or 3) until you see the unwinding assertion fail again.
3. Keep increasing the unwinding value by 1 until the unwinding assertion goes away. That's the minimum unwinding value you should use for the proof.

You can use different strategies in step (1) to find the value that doesn't trigger the unwinding assertion, like doubling the value each time. But it depends very much on the project, and it's not strange to go to values like 256 if the code underneath performs, for example, manipulations over byte streams. Hope this is helpful!

[kalyazin]

@adpaco-aws thanks for the suggestion.
I have experimented a bit and noticed the following. If i replace the line

for msr in range.base..(range.base + range.nmsrs) {

with

for msr in 0..2 {

I am able to run kani with just --unwind 3, however the original code is not even passing with --unwind 50 and takes decades of minutes to run.
I am highly confident that range.base takes values 0 or 1 and range.nmsrs is always 1, so the modified version is not very far from the original semantically.
I appreciate the approach you mentioned (pick the unwind value that passes and keep decreasing it), but 50 compared to 3 looks like a big difference to me for almost equivalent pieces of code.
I will be trying to increase the unwind number to succeed.

[adpaco-aws]

You're right, that's a big difference. The root cause for this issue might be the same as in #1676 and #1766, which is related to the handling of unions in CBMC (looking at MsrRange in particular). Please let us take a closer look to the example you provided and we'll get back to you.

[kalyazin]

Just an update here. I tried --unwind 100. It took longer than 2.5 hours, but still didn't succeed with the same error.

[zhassan-aws]

This is definitely a bug. Here's a minimal reproducer that exhibits the same behavior:

#[kani::proof]
#[kani::unwind(50)]
fn main() {
    let a: &[(i32, i32)] = &[(0, 1), (1, 2)];
    for e in a {
        let lb = e.0;
        let ub = e.0 + e.1;
        for i in lb..ub {
            assert!(i <= 2);
        }
    }
}

$ kani range.rs
# snip ...


Check 126: main.unwind.0
         - Status: FAILURE
         - Description: "unwinding assertion loop 0"
         - Location: range.rs:8:18 in function main

Check 127: main.unwind.1
         - Status: UNDETERMINED
         - Description: "unwinding assertion loop 1"
         - Location: range.rs:9:13 in function main


SUMMARY:
 ** 1 of 127 failed (126 undetermined)
Failed Checks: unwinding assertion loop 0
 File: "/home/ubuntu/examples/range.rs", line 8, in main

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: 16.814152s

[zhassan-aws]

This simpler example fails as well:

#[cfg_attr(kani, kani::proof, kani::unwind(50))]
fn main() {
    let a: &[i32] = &[0, 1];
    for e in a {
        let lb = *e;
        let ub = lb + 1;
        for i in lb..ub {
            assert!(i <= 2);
        }
    }
}

[zhassan-aws]

It seems that the outer loop, which is iterating over the slice, is somehow causing a non-det to be introduced. The unwinding assertion fails for this program:

#[cfg_attr(kani, kani::proof, kani::unwind(50))]
fn main() {
    let a: &[i32] = &[0, 0];
    for &e in a {
        assert_eq!(e, 0);
        for i in e..1 {
            assert_eq!(i, 0);
        }
    }
}

but if I change the outer loop to iterate over the indices, it works fine:

#[cfg_attr(kani, kani::proof, kani::unwind(50))]
fn main() {
    let a: &[i32] = &[0, 0];
    for j in 0..a.len() {
        let e = a[j];
        assert_eq!(e, 0);
        for i in e..1 {
            assert_eq!(i, 0);
        }
    }
}

SUMMARY:
 ** 0 of 83 failed

VERIFICATION:- SUCCESSFUL

Verification Time: 0.9310525s

[zhassan-aws]

This smaller program also exhibits the same behavior:

#[cfg_attr(kani, kani::proof, kani::unwind(20))]
fn main() {
    for e in &[0, 0] {
        for _i in *e..1 {
        }
    }
}

[zhassan-aws]

An observation from offline discussions is that adding any dummy statement after the inner loop makes the problem go away, e.g.:

#[cfg_attr(kani, kani::proof, kani::unwind(4))]
fn main() {
    for e in &[0, 0] {
        for _i in *e..1 {
        }
        assert!(1 + 1 == 2);
    }
}

$ kani range.rs
...
SUMMARY:
 ** 0 of 122 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.47980258s

[zhassan-aws]

Another observation is that the behavior is the same whether we use goto-instrument's --ensure-one-backedge-per-target or not.

[tautschnig]

Perhaps there is a bug in this rewriter? Will investigate later on this week.

[tautschnig]

It seems that at the goto-program level the loops here form a figure-of-eight. They are two (nested) natural loops, but not two nested lexical loops. ensure-one-backedge-per-target does seem to be doing what it says on the tin: there just is one back-edge for each of the loops, it just so happens that the back-edge for the outer loop sits within the inner loop. It seems we need a new transform that restores lexical loops.

[tautschnig]

I have issued a draft PR, which is waiting for me to piece together a test case.

[tautschnig]

I have issued a draft PR, which is waiting for me to piece together a test case.

That PR is now awaiting feedback/approval by code owners.

[tautschnig]

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).

[celinval]

Adding this to our sprint board so we remember to close it as part of our next release.