Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add support for const promotion #886

Open
ranjitjhala opened this issue Nov 15, 2024 · 1 comment
Open

Add support for const promotion #886

ranjitjhala opened this issue Nov 15, 2024 · 1 comment
Assignees

Comments

@ranjitjhala
Copy link
Contributor

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?
}
@ranjitjhala ranjitjhala self-assigned this Nov 15, 2024
@nilehmann
Copy link
Member

nilehmann commented Nov 22, 2024

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).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants