Function Contracts: Mutual recursion function contract wrapper for replace code stub

[pi314mm]

Function contracts are not being properly expanded when the recursive call to the function occurs outside of the function body

Consider the following code:

#[kani::recursion]
#[kani::ensures(|r| if n==0 {*r == true} else {true})]
fn even(n: u32) -> bool {
    if n == 0 {
        true
    } else {
        odd(n - 1)
    }
}

#[kani::recursion]
fn odd(n: u32) -> bool {
    if n == 0 {
        false
    } else {
        even(n - 1)
    }
}

#[kani::proof_for_contract(even)]
fn harness(){
    let x = kani::any();
    even(x);
}

Within the verification of even, we would expect it to call odd which refers to the code stub recursively marked version of even because you are re-entering the even function during the verification of it.

Instead, we get the following expansion:

#[kanitool::recursion]
#[kanitool::checked_with = "even_recursion_wrapper_882c72"]
#[kanitool::replaced_with = "even_replace_882c72"]
#[kanitool::inner_check = "even_wrapper_882c72"]
fn even(n: u32) -> bool { { if n == 0 { true } else { odd(n - 1) } } }
#[allow(dead_code, unused_variables, unused_mut)]
#[kanitool::is_contract_generated(recursion_wrapper)]
fn even_recursion_wrapper_882c72(arg0: u32) -> bool {
    static mut REENTRY: bool = false;
    if unsafe { REENTRY } {
            even_replace_882c72(arg0)
        } else {
           unsafe { REENTRY = true };
           let result_kani_internal = even_check_882c72(arg0);
           unsafe { REENTRY = false };
           result_kani_internal
       }
}
#[allow(dead_code, unused_variables, unused_mut)]
#[kanitool::recursion]
#[kanitool::is_contract_generated(check)]
fn even_check_882c72(n: u32) -> bool {
    let result_kani_internal: bool = even_wrapper_882c72(n);
    kani::assert(kani::internal::apply_closure(|r|
                if n == 0 { *r == true } else { true },
            &result_kani_internal),
        "|r| if n==0 { *r == true } else { true }");
    result_kani_internal
}
#[allow(dead_code, unused_variables, unused_mut)]
#[kanitool::recursion]
#[kanitool::is_contract_generated(replace)]
fn even_replace_882c72(n: u32) -> bool {
    let result_kani_internal: bool = kani::any_modifies();
    kani::assume(kani::internal::apply_closure(|r|
                if n == 0 { *r == true } else { true },
            &result_kani_internal));
    result_kani_internal
}
#[allow(dead_code, unused_variables, unused_mut)]
#[kanitool::recursion]
#[kanitool::is_contract_generated(wrapper)]
fn even_wrapper_882c72(n: u32) -> bool {
    if n == 0 { true } else { odd(n - 1) }
}
#[kanitool::recursion]
fn odd(n: u32) -> bool { if n == 0 { false } else { even(n - 1) } }
#[allow(dead_code)]
#[kanitool::proof_for_contract = "even"]
fn harness() {
    kani::internal::init_contracts();
    { let x = kani::any(); even(x); }
}

Note that even_check_882c72 calls odd which calls even instead of the recursive wrapper even_recursion_wrapper_882c72 even though functions are marked by #[kanitool::recursion]

While this example is easier, consider the example of mutually recursive functions with mutable arguments:

#[kani::recursion]
#[kani::modifies(n)]
#[kani::ensures(|r| if old(*n)==0 {*r == true} else {true})]
fn even(n: &mut u32) -> bool {
    if *n == 0 {
        true
    } else {
        *n -= 1;
        odd(n)
    }
}

#[kani::recursion]
fn odd(n: &mut u32) -> bool {
    if *n == 0 {
        false
    } else {
        *n -= 1;
        even(n)
    }
}

#[kani::proof_for_contract(even)]
fn harness(){
    let x = &mut kani::any();
    even(x);
}

We would expect odd to expand out with the same modifies clause wrapper in the way that CBMC augments all functions with a write set. Instead we get the following:

#[kanitool::recursion]
#[kanitool::checked_with = "even_recursion_wrapper_5d92e8"]
#[kanitool::replaced_with = "even_replace_5d92e8"]
#[kanitool::inner_check = "even_wrapper_5d92e8"]
fn even(n: &mut u32) -> bool {
    { if *n == 0 { true } else { *n -= 1; odd(n) } }
}
#[allow(dead_code, unused_variables, unused_mut)]
#[kanitool::is_contract_generated(recursion_wrapper)]
fn even_recursion_wrapper_5d92e8(arg0: &mut u32) -> bool {
    static mut REENTRY: bool = false;
    if unsafe { REENTRY } {
            even_replace_5d92e8(arg0)
        } else {
           unsafe { REENTRY = true };
           let result_kani_internal = even_check_5d92e8(arg0);
           unsafe { REENTRY = false };
           result_kani_internal
       }
}
#[allow(dead_code, unused_variables, unused_mut)]
#[kanitool::recursion]
#[kanitool::is_contract_generated(check)]
fn even_check_5d92e8(n: &mut u32) -> bool {
    let remember_kani_internal_1e56f1c07b14a51c = *n;
    let _wrapper_arg_1 =
        unsafe { kani::internal::Pointer::decouple_lifetime(&n) };
    let result_kani_internal: bool = even_wrapper_5d92e8(n, _wrapper_arg_1);
    kani::assert(kani::internal::apply_closure(|r|
                if (remember_kani_internal_1e56f1c07b14a51c) == 0 {
                        *r == true
                    } else { true }, &result_kani_internal),
        "|r| if old(*n)==0 { *r == true } else { true }");
    result_kani_internal
}
#[allow(dead_code, unused_variables, unused_mut)]
#[kanitool::recursion]
#[kanitool::is_contract_generated(replace)]
fn even_replace_5d92e8(n: &mut u32) -> bool {
    let remember_kani_internal_1e56f1c07b14a51c = *n;
    let result_kani_internal: bool = kani::any_modifies();
    *unsafe {
                kani::internal::Pointer::assignable(kani::internal::untracked_deref(&(n)))
            } = kani::any_modifies();
    kani::assume(kani::internal::apply_closure(|r|
                if (remember_kani_internal_1e56f1c07b14a51c) == 0 {
                        *r == true
                    } else { true }, &result_kani_internal));
    result_kani_internal
}
#[kanitool::modifies(_wrapper_arg_1)]
#[allow(dead_code, unused_variables, unused_mut)]
#[kanitool::recursion]
#[kanitool::is_contract_generated(wrapper)]
fn even_wrapper_5d92e8<'_wrapper_arg_1,
    WrapperArgType1>(n: &mut u32, _wrapper_arg_1: &WrapperArgType1) -> bool {
    if *n == 0 { true } else { *n -= 1; odd(n) }
}
#[kanitool::recursion]
fn odd(n: &mut u32) -> bool { if *n == 0 { false } else { *n -= 1; even(n) } }
#[allow(dead_code)]
#[kanitool::proof_for_contract = "even"]
fn harness() {
    kani::internal::init_contracts();
    { let x = &mut kani::any(); even(x); }
}

This suggests we might need some kind of transformation on the whole code base like CBMC does where the write set is a pointer to pointers, and if the pointer is NULL, we don't check for inclusion into the write set, but if the pointer is a valid pointer of pointers, then we check the write set.