Skip to content

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

Open
@chorman0773

Description

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    A-aliasing-modelTopic: Related to the aliasing model (e.g. Stacked/Tree Borrows)A-optimizationCategory: Discussing optimizations we might (not) want to supportC-open-questionCategory: An open question that we should revisitS-pending-designStatus: Resolving this issue requires addressing some open design questions

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions