flux-rs / flux

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

Add support for const promotion #886

Open ranjitjhala opened 1 week ago

ranjitjhala commented 1 week ago

Per @nilehmann -- that is what will let us check stuff like the below

https://github.com/rust-lang/const-eval/blob/master/promotion.md

#[flux::sig(fn (a: &[&[i32][3]]))]
fn check_slice(_: &[&[i32]]) {}

fn test_slice1() {
    let x = &[1, 2, 3];
    check_slice(&[x]); // VERIFIES
}

fn test_slice2() {
    check_slice(&[&[1, 2, 3]]); // REJECTED because of const promotion?
}
nilehmann commented 1 day ago

Some thoughts on this.

The mir for test_slice2 looks like this

const test_slice2::promoted: &[&[i32]; 1] = {
    let mut _0: &[&[i32]; 1];
    let mut _1: [&[i32]; 1];
    let mut _2: &[i32];
    let mut _3: &[i32; 3];
    let mut _4: &[i32; 3];
    let mut _5: [i32; 3];

    bb0: {
        _5 = [const 1_i32, const 2_i32, const 3_i32];
        _4 = &_5;
        _3 = &(*_4);
        _2 = move _3 as &[i32] (PointerCoercion(Unsize));
        _1 = [move _2];
        _0 = &_1;
        return;
    }
}

fn test_slice2() -> () {
    let mut _0: ();
    let _1: ();
    let mut _2: &[&[i32]];
    let _3: &[&[i32]; 1];

    bb0: {
        _3 = const test_slice2::promoted;
        _2 = copy _3 as &[&[i32]] (PointerCoercion(Unsize));
        _1 = check_slice(move _2) -> [return: bb1, unwind continue];
    }

    bb1: {
        return;
    }
}

where test_slice2::promoted is an automatically generated constant with its own mir body.

I see two options to handle this. We could

  1. Inline the definition of the promoted constant, that's it, jump into the promoted body while checking the main function and then back.
  2. Compute the strongest type for the promoted body.

edit:

On second thought. There's not much difference between the two because (1) I don't think the promoted body can be recursive and (2) promoted constants are by definition used only once so we don't gain much by computing the strongest type and saving it.

The real issue is whether the promoted body has more than one return path. If there's more than one, we need to find the join with kvars (since it's not recursive it will still be the strongest).

edit2:

We can think of _3 = const test_slice2::promoted; as calling a function with no arguments for which we don't have a refined signature.

edit3:

Ok, thinking of it as a function makes it clearer. If we have a promoted const of (rust) type T, in general, we should check the promoted body against fn() -> T{v: $k}. Since we know the function won't be recursive, we could avoid the kvar if there's only one return path (this is probably the common case).