Stream: t-compiler/wg-nll

Topic: Miri vs. NLL


Jake Goulding (Feb 12 2019 at 16:31, on Zulip):

In https://github.com/solson/miri/issues/628, @RalfJ showed me how Miri can treat a function call differently from how NLL treats it based on the ordering of arguments. Specifically:

fn test(x_0: &mut [i32; 2]) {
    let x_1: &mut [i32; 2] = unsafe { &mut *(x_0 as *mut [i32; 2]) };
    // OK by Miri
    println!("{}, {}", x_1[0], x_0[1]);
    // Flagged by Miri
    println!("{}, {}", x_0[1], x_1[0]);
}

fn main() {
    test(&mut [42, 84]);
}
Jake Goulding (Feb 12 2019 at 16:35, on Zulip):

And it appears that this extends to straight-forward function calls:

fn double_drop<T0, T1>(_: T0, _: T1) {}

fn main() {
    let x = &mut 0;
    let y = &mut *x;

    // OK
    //let _val = *y;
    //let _val = *x;

    // Bad
    // let _val = *x;
    // let _val = *y;

    // OK
    // double_drop(*y, *x);

    // Bad
    // double_drop(*x, *y);
}
Jake Goulding (Feb 12 2019 at 16:36, on Zulip):

Is it just that the formatting macros are doing something complicated compared to a function?

Jake Goulding (Feb 12 2019 at 16:36, on Zulip):

I do know that they do some trickery

RalfJ (Feb 12 2019 at 21:07, on Zulip):

it's not really Miri treating it "differently", at least not in the sense of there being a conflict. Miri accepts more code than NLL does, for sure -- by design. NLL and Miri both care about the order in which accesses happen. Miri, being a dynamic check, should IMO not give a meaning to the "statement boundary" (that's C "sequence points" all over again, no thanks). NLL decides to be somewhat more conservative here.

RalfJ (Feb 12 2019 at 21:08, on Zulip):

And it appears that this extends to straight-forward function calls

is "Ok"/"Bad" here describing Miri or NLL behavior?

Jake Goulding (Feb 13 2019 at 17:12, on Zulip):

NLL decides to be somewhat more conservative here.

I think that was my (unstated) question — should/can NLL not have that conservatism?

is "Ok"/"Bad" here describing Miri or NLL behavior?

OK means that the code can compile, Bad means it does not; Miri is not involved there

Last update: Nov 21 2019 at 13:50UTC