StorageDead is not dominated by StorageLive

[vakaras]

As far as I understand, a StorageDead has to be dominated by StorageLive. For this code (which is a simplified version of #[derive(PartialEq, Eq)] on E):

struct E {
    g: i32,
    f: i32,
}

fn test(a: &E, b: &E) -> bool {
    a.g == b.g && a.f == b.f
}

This does not seem to be the case. I get the following MIR (mir_dump/test.test.-------.renumber.0.mir produced with rustc +nightly -Zdump-mir=all -Zdump-mir-dataflow=y -Zdump-mir-graphviz=y --crate-type lib test.rs):

// MIR for `test` 0 renumber

fn test(_1: &E, _2: &E) -> bool {
    debug a => _1;                       // in scope 0 at test.rs:6:9: 6:10
    debug b => _2;                       // in scope 0 at test.rs:6:16: 6:17
    let mut _0: bool;                    // return place in scope 0 at test.rs:6:26: 6:30
    let mut _3: bool;                    // in scope 0 at test.rs:7:5: 7:15
    let mut _4: i32;                     // in scope 0 at test.rs:7:5: 7:8
    let mut _5: i32;                     // in scope 0 at test.rs:7:12: 7:15
    let mut _6: bool;                    // in scope 0 at test.rs:7:19: 7:29
    let mut _7: i32;                     // in scope 0 at test.rs:7:19: 7:22
    let mut _8: i32;                     // in scope 0 at test.rs:7:26: 7:29

    bb0: {
        StorageLive(_3);                 // scope 0 at test.rs:7:5: 7:15
        StorageLive(_4);                 // scope 0 at test.rs:7:5: 7:8
        _4 = ((*_1).0: i32);             // scope 0 at test.rs:7:5: 7:8
        StorageLive(_5);                 // scope 0 at test.rs:7:12: 7:15
        _5 = ((*_2).0: i32);             // scope 0 at test.rs:7:12: 7:15
        _3 = Eq(move _4, move _5);       // scope 0 at test.rs:7:5: 7:15
        StorageDead(_5);                 // scope 0 at test.rs:7:14: 7:15
        StorageDead(_4);                 // scope 0 at test.rs:7:14: 7:15
        switchInt(move _3) -> [false: bb1, otherwise: bb2]; // scope 0 at test.rs:7:5: 7:29
    }

    bb1: {
        _0 = const false;                // scope 0 at test.rs:7:5: 7:29
        goto -> bb3;                     // scope 0 at test.rs:7:5: 7:29
    }

    bb2: {
        StorageLive(_6);                 // scope 0 at test.rs:7:19: 7:29
        StorageLive(_7);                 // scope 0 at test.rs:7:19: 7:22
        _7 = ((*_1).1: i32);             // scope 0 at test.rs:7:19: 7:22
        StorageLive(_8);                 // scope 0 at test.rs:7:26: 7:29
        _8 = ((*_2).1: i32);             // scope 0 at test.rs:7:26: 7:29
        _6 = Eq(move _7, move _8);       // scope 0 at test.rs:7:19: 7:29
        StorageDead(_8);                 // scope 0 at test.rs:7:28: 7:29
        StorageDead(_7);                 // scope 0 at test.rs:7:28: 7:29
        _0 = move _6;                    // scope 0 at test.rs:7:5: 7:29
        goto -> bb3;                     // scope 0 at test.rs:7:5: 7:29
    }

    bb3: {
        StorageDead(_6);                 // scope 0 at test.rs:7:28: 7:29
        StorageDead(_3);                 // scope 0 at test.rs:7:28: 7:29
        return;                          // scope 0 at test.rs:8:2: 8:2
    }
}

The execution path bb0 → bb1 → bb3 executes StorageDead(_6); without executing StorageLive(_6);, which, as far as I understand, is a bug.

Meta

rustc --version --verbose:

rustc +nightly --version --verbose
rustc 1.64.0-nightly (495b21669 2022-07-03)
binary: rustc
commit-hash: 495b216696ccbc27c73d6bdc486bf4621d610f4b
commit-date: 2022-07-03
host: x86_64-unknown-linux-gnu
release: 1.64.0-nightly
LLVM version: 14.0.6

Related issues

#68622

[pierwill]

@rustbot claim

[pierwill]

@rustbot label +T-compiler +A-mir

[RalfJung]

Ah, I think I just reported the same problem: #99085.

[RalfJung]

In #99160 we are considering allowing redundant StorageLive; if we went that way, we would most probably want to keep allowing redundant StorageDead as well.

[JakobDegen]

As far as I understand, a StorageDead has to be dominated by StorageLive

@vakaras I'd also be interested to know if you have a reason for wanting this. I can't think of any real benefits myself, but I totally might be missing something

[vakaras]

As far as I understand, a StorageDead has to be dominated by StorageLive

@vakaras I'd also be interested to know if you have a reason for wanting this. I can't think of any real benefits myself, but I totally might be missing something

I am working on a verifier for Rust called Prusti. Simply speaking, if I can treat StorageLive as a malloc for stack and StorageDead as a free for stack, it makes my life easy because our infrastructure directly supports working with such concepts. If the use of StorageLive and StorageDead does not follow this model, for example, having StorageDead without preceding StorageLive is fine, then I have to implement a static analysis in Prusti that maps the more complicated model into the one supported by our infrastructure. In this case, the analysis should be simple to implement, so I am not too worried about that part. The part that worries me is how can I ensure that Prusti interprets MIR in the same way as the Rust compiler, especially over a longer period of time when small changes occur.

[JakobDegen]

I am working on a verifier for Rust called Prusti. Simply speaking, if I can treat StorageLive as a malloc for stack and StorageDead as a free for stack, it makes my life easy because our infrastructure directly supports working with such concepts. If the use of StorageLive and StorageDead does not follow this model, for example, having StorageDead without preceding StorageLive is fine, then I have to implement a static analysis in Prusti that maps the more complicated model into the one supported by our infrastructure

So slightly generalizing this, I'm interpreting this as "I want to lower MIR to an IR which does not support these semantics" - this seems like a good reason to me. LLVM is not the only IR that MIR needs to be lowered to, SMIR, gcc, etc. are also there, and this might make sense for that reason.

That being said, this is still not enough for the desired conclusion from the title that there is a dominance requirement. Indeed, even if we don't allow redundant storage markers, they are still dynamic statements, and so are allowed to be all kinds of wrong in dead code.

The part that worries me is how can I ensure that Prusti interprets MIR in the same way as the Rust compiler, especially over a longer period of time when small changes occur.

You can submit a PR to add your github tag here to be notified whenever a PR changes MIR semantics.

[vakaras]

I am working on a verifier for Rust called Prusti. Simply speaking, if I can treat StorageLive as a malloc for stack and StorageDead as a free for stack, it makes my life easy because our infrastructure directly supports working with such concepts. If the use of StorageLive and StorageDead does not follow this model, for example, having StorageDead without preceding StorageLive is fine, then I have to implement a static analysis in Prusti that maps the more complicated model into the one supported by our infrastructure

So slightly generalizing this, I'm interpreting this as "I want to lower MIR to an IR which does not support these semantics"

Yes, exactly.

That being said, this is still not enough for the desired conclusion from the title that there is a dominance requirement. Indeed, even if we don't allow redundant storage markers, they are still dynamic statements, and so are allowed to be all kinds of wrong in dead code.

For Prusti, dead code is not a problem (as long as it is provably dead) because unreachable code is not analyzed. Whether it would be a problem for other compiler consumers, I do not know and would be open to discuss this.

The part that worries me is how can I ensure that Prusti interprets MIR in the same way as the Rust compiler, especially over a longer period of time when small changes occur.

You can submit a PR to add your github tag here to be notified whenever a PR changes MIR semantics.

Thanks! I just did that.