flux-rs / flux

Refinement Types for Rust
MIT License
660 stars 21 forks source link

Unsoundness with `ReifyFnPtr` cast #859

Closed ranjitjhala closed 1 week ago

ranjitjhala commented 1 month ago
          This gives me the heebie-jeebies. The function pointer doesn't have refinements but the closure or function definition you are coercing from may, so this should involve function subtyping. 

Also, I think for closures this means we never check the closure's body.

_Originally posted by @nilehmann in https://github.com/flux-rs/flux/pull/854#discussion_r1806877393_

ranjitjhala commented 1 month ago

Specifically I think this would be unsoundly accepted

#![allow(dead_code)]

fn foo(f: fn(i32) -> i32) -> i32 {
    f(10)
}

#[flux::sig(fn (bool[true]))]
fn assert(_b:bool){}

#[flux::sig(fn (i32{v: v > 100}) -> i32)]
fn inc(x: i32) -> i32 {
    assert(x > 100);
    x + 1
}

fn baz() -> i32 {
    foo(inc)
}