Incorrect verification results for function/closure dyn traits

[avanhatt]

The following fails to verify:

fn foo(fun: &mut dyn FnMut(i32) -> i32) -> i32 {
    fun(1)
}

fn main() {
    let r = foo(&mut move |z : i32| { z } );
    assert!(r == 1); // should succeed
}

In the generated CBMC-C code, in some places we pass the closure argument as a tuple, but in others we expect the flattened int.

[avanhatt]

This is blocking #220

[avanhatt]

A similar example (without an explicit FnOnce) that demonstrates that this is a soundness issue:

fn takes_dyn_fun(fun: &dyn Fn() -> u32) {
    let x = fun();
}

pub fn unit_to_u32() -> u32 {
    assert!(false); 
    0
}

fn main() {
    takes_dyn_fun(&unit_to_u32)
}

Should fail from this explicit assert false, but:

VERIFICATION SUCCESSFUL

[avanhatt]

This does fail as expected with --pointer-check:

$ rmc --gen-c src/test/cbmc/DynTrait/dyn_fn_minimal.rs --pointer-check | grep FAIL
[pointer_dereference.7] invalid function pointer: FAILURE
VERIFICATION FAILED

But, this means we are generating some bad function dereference, so still a bug.

[avanhatt]

Weird thing to maybe investigate separately:

The following hangs RMC at the gotoc-cc call (?!?)

    // Create a nested boxed once-callable closure
    let f: Box<Box<dyn FnOnce(i32)>> = Box::new(Box::new(|x| assert!(x == 1)));
    f(1);

    // Create a pointer to a closure
    let g = |y| assert!(y == 2);
    let p: &dyn Fn(i32) = &g;
    p(2);

    // Additional level of pointer nesting
    let q: &dyn Fn(i32) = &p;
    q(2);

Even though the first chunk of code should be independent from the 2nd, commenting it out gets rid of the hang.