---
title: "opsem Meeting proposal: behavior of _ in match patterns"
date: 2023-09-26
tags: T-opsem, meeting
meeting-issue: https://github.com/rust-lang/opsem-team/issues/16
url: https://hackmd.io/A_3l7azoTOK6buOxOZr-pw
---

# opsem Meeting proposal: behavior of _ in match patterns

The opsem question is whether code like the following has UB:

fn main() {
    let ptr = 32 as *const (u8, u8);
    unsafe {
        match (*ptr).1 { _ => {} }
    }
}

Currently, MIR building throws away the entire `match` since the `_` pattern is interpreted as "ignore this". This is how `let _ = (*ptr).1;` used to behave as well, but that [got fixed](https://github.com/rust-lang/rust/pull/104844).
For `_` pattern in `match`, the old behavior is still in place.

Arguably, this code creates a place `(*ptr).1`, but never turns it into a value, so it should have all the UB from place construction (such as ensuring that the projection is in-bounds) but none of the UB from actually loading from memory or constructing a value of the given type.

This is what [this PR](https://github.com/rust-lang/rust/pull/103208) achieves with a new MIR desugaring for matches.
Old:

FakeRead(FakeReadCause::ForMatchedPlace(None), x);
match x {
  PATTERN => ARM,
  // compiler inserted fallback pattern
  // (only reachable with uninhabited types)
  _ => {
    Unreachable;
  }
}

New:

PlaceMention(x); // for uniformity, to avoid losing information
match x {
  PATTERN => ARM,
  // compiler inserted fallback pattern
  // (only reachable with uninhabited types)
  _ => {
    // instruct borrowck to check that `x` is initialized here
    FakeRead(FakeReadCause::ForMatchedPlace(None), x);
    Unreachable;
  }
}

The `FakeRead` here is a "read for the purpose of borrowck" that however has no operational effects (i.e., it is a NOP in Miri).

The PR replaces the `FakeRead` before the `match` by a `PlaceMention`. For Miri this means *more* UB since `PlaceMention` actually computes the place and ensures that doing so does not raise UB. For the borrow checker however this means a *weaker* requirement than the status quo: `PlaceMention` does not require the place to be initialized! It can be partially borrowed/moved-out.

For normal exhaustive matches, the `_` arm is unreachable (has no incoming MIR edge), and thus will be ignored by the borrow checker. However, when match checking exploited that the type is uninhabited, the fallback path *can* become reachable, and in that case (a) the borrow checker must ensure that the place is initialized (since creating an uninitialize uninhabited place is possible in safe code) and (b) Miri must raise UB. (a) is achieved by the `FakeRead`; (b) is achieved by the `Unreachable`.

The borrow checker ramifications are T-types/T-lang questions, but for T-opsem the question is: do we support the change in the operational desugaring of `match` that that PR proposes?

Other documents/notes:

- T-lang [has a design doc](https://hackmd.io/fqEtqAvBQTGiitn0Q_Y1iA?both) on this as well.
- The PR would [fix this Miri issue](https://github.com/rust-lang/miri/issues/2360) -- or alternatively T-opsem should declare that Miri's current behavior is correct.

## Examples

This proposal accepts strictly more code in the borrow checker (since `PlaceMention` has weaker requirements than `FakeRead`).
Code that now gets accepted by the borrow checker:

enum Void {}
let x: (i32, Void); // storage for this local is allocated here
match x.1 { // so this is a fine place to mention
    _ if {
        println!("Executed match!");
        loop {}
    } => (),
}

However this still gets rejected, of course:

enum Void {}
let x: (i32, Void);
match x.1 {}

This hits the `FakeRead` in the fallback arm, so the compiler checks that `x.1` is initialized, which it is not, and then we bail out.

On the Miri side it leads to strictly less UB though, see the motivating exampe at the beginning of this document.

# Meeting questions and notes (2023-09-26)

Attendance: Monadic Cat, Connor Horman, carbotaniuman, Ralf, Mario Carneiro, Ben Kimock, Jacob, TC

## Connor: Extending UB interacts with Borrowck Question

If T-opsem chose to expand what is considered defined or undefined, would that not necessarily implicate the borrowck question.

Ralf: We've been asked by t-lang to weigh in on the opsem question. My interpretation is that t-lang is fine with the borrowck implications of [that PR](https://github.com/rust-lang/rust/pull/103208).

I guess there would be an alternative desugaring that avoids extending what borrowck accepts:

PlaceMention(x);
FakeRead(FakeReadCause::ForMatchedPlace(None), x);
match x {
  PATTERN => ARM,
  // compiler inserted fallback pattern
  // (only reachable with uninhabited types)
  _ => {
    Unreachable;
  }
}

For opsem this is equivalent. The original example gets accepted by borrowck either way. We can leave that choice to t-lang.

## Mario: FakeRead is suspicious

Why not just use `Read`? A read that only exists for the purpose of borrowck is almost always a suspicious thing to do, and at least in this case it should be the same thing to `Read` instead of `FakeRead` since the read will terminate and there is an `Unreachable` right after.

Connor: It has strictly less UB when the `match` does not do any actual reads - the place may refer to uinitialized memory, or the read may be a data race at runtime. - Referring to original version and alternative desugaring that does `FakeRead` before the `match`.

RJ: Fair point, in the new desugaring `FakeRead; Unreachable` vs `Read; Unreachable` makes no difference. I don't know if there are other `FakeRead`; the [`FakeReadCause` enum](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.FakeReadCause.html) indicates that there are. I'd view this more as a DSL to program the borrowck (to ask it to check that something is initialized) than an actual read.

## Mario: Can we do without the FakeRead entirely?

The only case where it makes a difference is when the unreachable arm is not unreachable by an edge in the CFG, and in that case there should actually have been a discriminant read (a switchInt) to get us there

Connor:

// This must be rejected.
let x: Void;
match x {} // "sugar for" match x { ! }

// This should be accepted.
let x: Void;
match x { _ => () }