PointerCast::ClosureFnPointer is unimplemented

[danielsn]

I tried this code:

#![feature(core_intrinsics)]
use std::intrinsics::r#try;

fn main() {
    unsafe {
        r#try(
            |_a: *mut u8| panic!("foo"),
            std::ptr::null_mut(),
            |_a: *mut u8, _b: *mut u8| println!("bar"),
        );
    }
}

using the following command line invocation:

rmc try.rs

with RMC version: 1.53

I expected to see this happen: It compiled

Instead, this happened: explanation
Crashed with an unimplemented on this construct

[avanhatt]

Also used in a Rust UI test:

src/test/ui/functions-closures/closure_to_fn_coercion-expected-types.rs

// run-pass
#![allow(unused_variables)]
// Ensure that we deduce expected argument types when a `fn()` type is expected (#41755)

fn foo(f: fn(Vec<u32>) -> usize) { }

fn main() {
    foo(|x| x.len())
}

[zhassan-aws]

The examples no longer crash, but keeping the issue open to track adding support for PointerCast::ClosureFnPointer.

[YoshikiTakashima]

4/5 tests in prost-types failing with this issue.

Verification failed for - datetime::tests::check_timestamp_parse_to_string_roundtrip
Verification failed for - datetime::tests::check_duration_parse_to_string_roundtrip
Verification failed for - tests::check_system_time_roundtrip
Verification failed for - tests::check_duration_roundtrip
Complete - 1 successfully verified harnesses, 4 failures, 5 total.

[celinval]

It looks like rustc reify the closure into FnOnce and pass the pointer to the call_once() implementation. Since this function doesn't capture anything, it doesn't pass Self as a parameter. We need to implement the reification.

[rod-chapman]

I also get this unimplemented feature reported on s2n-quic/quic/s2n-quic-core/src/counter.rs

[YoshikiTakashima]

@celinval Are you taking this on before Jan'23? I'm thinking of taking a stab at this issue since it looks pretty severe for prost-types.

P.S. 2023-01-06: No progress on this one. I got it drop self but have not found a way to codegen that function so kani still fails to verify.

[celinval]

@celinval Are you taking this on before Jan'23? I'm thinking of taking a stab at this issue since it looks pretty severe for prost-types.

P.S. 2023-01-06: No progress on this one. I got it drop self but have not found a way to codegen that function so kani still fails to verify.

Ok. Let me take a look.