How does UnsafeCell interact with match; can op.sem ensure exhaustiveness?

[chorman0773]

Currently, under both Stacked Borrows and Treed Borrows, the following code has defined behaviour:

use std::cell::Cell;

pub fn evil(x: &Result<bool, Cell<u8>>) -> bool {
    unsafe { *(x as *const _ as *const bool as *mut bool).add(1) = false }
    false
}

pub fn main() {
    let x = Ok(true);
    match &x {
        Ok(true) if evil(&x) => unreachable!(),
        Ok(false) => println!("Ok(false) = {x:?}"),
        Ok(true) => println!("Ok(true) = {x:?}"),
        Err(_) => unreachable!(),
    }
}

(Credit to @digama0)

On current rustc, this compiles and prints Ok(true) = Ok(false). However, given no undefined behaviour, this seems to conflict with the fact that patterns are evaluated linearily -> Ok(false) should hit first.

The question is: Does this code have UB (most likely in evil) or is this defined behaviour. If we answer the latter, we must then answer whether rustc's lowering of the match is correct, or if a linear evaluation is correct.

From https://rust-lang.zulipchat.com/#narrow/stream/136281-t-opsem/topic/How.20does.20match.20interact.20with.20.60.26UnsafeCell.60, it's clear to me that rustc's lowering should be deemed correct in some manner, but I also believe that we currently promise sequential evaluation (additionally, even if we don't, I believe that a naive lowering of cascading if/else if statements should be valid). Given the two constraints being conflicting, if both are satisfied, then the code must have undefined behaviour.

[chorman0773]

For my part - on LE platforms (BE swap the order of the bytes being used for discrim vs. field) the following is logically the same as what I'd like to lower the match to on lccc, and seems to be logically equivalent with what rustc emits today:

match mem::transmute_copy::<_,u16>(&x){
    0x100 => {
        if evil(&x){
            unreachable!()
        }else{ 
            println!("Ok(true) = {x:?}") 
        }
    }
   0 =>  println!("Ok(false) = {x:?}"),
   0x101 | 1 => unreachable!(),
   _ => unreachable_unchecked()
}

[RalfJung]

We had a similar discussion not too long ago in Zulip... here it is.

To summarize my stance from that discussion, I think we should change the lowering to MIR. It should involve creating a new reference for all "match reads", tagged SharedReadOnly (or Freeze in TB). When we decide to enter a particular match arm, we use that particular reference to re-read all bytes that are relevant for this variant, thereby asserting that they did not change. That should make your example UB.

[chorman0773]

From https://rust-lang.zulipchat.com/#narrow/stream/136281-t-opsem/topic/How.20does.20match.20interact.20with.20.60.26UnsafeCell.60, it's clear to me that rustc's lowering should be deemed correct in some manner, but I also believe that we currently promise sequential evaluation (additionally, even if we don't, I believe that a naive lowering of cascading if/else if statements should be valid). Given the two constraints being conflicting, if both are satisfied, then the code must have undefined behaviour.

I have to amend this previous statement. Absent any undefined behaviour, then rustc's behaviour is just wrong, and not merely inconsistent with a sequential evaluation promise/desired semantics.

[chorman0773]

@rustbot label +A-stacked-borrows +A-optimization +C-open-queston +S-pending-design

[chorman0773]

@rustbot label +A-stacked-borrows +A-optimization +C-open-queston +S-pending-design