Recursion unwinding does not terminate

[thanhnguyen-aws]

I ran a small experiment to check the equivalence of the two versions of the greatest-common-divisor function, one is written with a loop and one in recursion.

I tried this code:

fn gcd (mut u: u8, mut v: u8) -> u8 {
    if u == 0 { return v; }
    if v == 0 { return u; }
    loop {
        if u > v {
            let temp = u;
            u = v;
            v = temp;
        }
        v -= u; // here v >= u
        if v == 0 { break; }
    }
    u 
}


fn gcd_rec(x: u8, y: u8) -> u8 {
    if y == 0 {
        x
    } 
    else if x == 0 {
        y
    } 
    else if x> y {
        gcd_rec(y, x - y)
    } 
    else
    {
        gcd_rec(x, y - x)
    }
} 

#[cfg(kani)]
#[kani::proof]
#[kani::unwind(256)]
fn main() {
    let x: u8 = kani::any();
    let y: u8 = kani::any();
    assert_eq!(gcd(x,y), gcd_rec(x,y));
}

using the following command line invocation:

kani  src/main.rs

with Kani version: 0.56.0

I expected to see this happen: Kani can verify the equivalence of the two versions. Note that, for the loop version, after each iteration max(u,v) decreases at least by 1 and u, v are u8, so the maximum number of iterations (unwinding) should be 256. It is similar for the two arguments of the recursive version.

Instead, this happened: The recursive version seems to be unwinded forever.

[feliperodri]

Thanks for the report, @thanhnguyen-aws! Have you tried https://github.com/model-checking/kani/blob/db1c5fe86609272f618695594d7d8f15a8f99480/docs/src/reference/experimental/contracts.md?plain=1#L28?

You would have to annotate the recursive function with contracts.

[zhassan-aws]

@feliperodri The #[kani::recursion] attribute should only be needed if contracts are used. Without contracts, the unwinding should eventually terminate.

[zhassan-aws]

Apparently, this occurs because of an exponential blow-up in the recursion tree? Here's a simpler reproducer:

fn rec(n: u8) -> u8 {
    if n == 0 {
        return 0;
    }
    //if n > 10 {
    //    return rec(n - 1);
    //}
    return rec(n - 1);
}

#[kani::proof]
#[kani::unwind(256)]
fn main() {
    let n: u8 = kani::any();
    let z = rec(n);
    assert!(z == 0);
}

This terminates immediately:

$ kani iss3771.rs
...

SUMMARY:
 ** 0 of 3 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.57622415s

but if I enable the commented-out code (which doesn't change the semantics of the function), CBMC keeps unwinding for more than 10 minutes without terminating:

Not unwinding recursion rec iteration 257
Not unwinding recursion rec iteration 257
Unwinding recursion rec iteration 256
Not unwinding recursion rec iteration 257
Not unwinding recursion rec iteration 257
Unwinding recursion rec iteration 254
Unwinding recursion rec iteration 255
Unwinding recursion rec iteration 256
Not unwinding recursion rec iteration 257
Not unwinding recursion rec iteration 257
Unwinding recursion rec iteration 256
Not unwinding recursion rec iteration 257
Not unwinding recursion rec iteration 257
Unwinding recursion rec iteration 255
Unwinding recursion rec iteration 256
Not unwinding recursion rec iteration 257
Not unwinding recursion rec iteration 257
Unwinding recursion rec iteration 256
Not unwinding recursion rec iteration 257
Not unwinding recursion rec iteration 257

@tautschnig do you think there's anything that can be done here?

[zhassan-aws]

@thanhnguyen-aws You can work around the issue by rewriting gcd_rec using tail recursion:

fn gcd_rec(x: u8, y: u8) -> u8 {
    if y == 0 {
        x
    } else if x == 0 {
        y
    } else {
        let mut x = x;
        let mut y = y;
        if y > x {
            let temp = x;
            x = y;
            y = temp;
        }
        gcd_rec(y, x - y)
    }
}

With that, verification terminates successfully in ~1 minute:

SUMMARY:
 ** 0 of 5 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 56.013733s

[thanhnguyen-aws]

@feliperodri @zhassan-aws Thank you very much for your response.