Unfolding of mutable references

[enjhnsn2]

The following code is safe, but flux flags that it may integer underflow:

pub(crate) struct DummyStruct {
    offset: usize,
    index: usize,
}

impl DummyStruct {
    fn set_safe_offset(&mut self) {
        let new_offset = if self.offset <= self.index {
            0
        } else {
            self.offset - self.index
        };
        self.offset = new_offset;
    }
}

fails with:

error[E0999]: arithmetic operation may overflow
   --> src/main.rs:157:13
    |
    |             self.offset - self.index
    |             ^^^^^^^^^^^^^^^^^^^^^^^^

This does not happen if the function takes a immutable parameter. The following code passes:

impl DummyStruct {
    fn get_safe_offset(&self) -> usize {
        if self.offset <= self.index {
            0
        } else {
            self.offset - self.index
        }
    }
}

[nilehmann]

This a known issue. We call it unfolding of mutable references. The issue is that unfolding only happens "atomically" within a statement so after checking self.offset <= self.index we forget the relationship because the references are folded back. (The issue doesn't apply to shared references because existentials inside shared references can be eagerly unpacked without loss of generality). For mutable references to primitive types like in this example the workaround is to read before doing the comparison.

        let a = self.offset;
        let b = self.index;
        let new_offset = if a <= b {
            0
        } else {
            a - b
        };
        self.offset = new_offset;

We've been postponing this for a while, so it may be time to tackle it. The general case is complicated, but I think it shouldn't be terribly difficult to handle this example.

[enjhnsn2]

Ah, alright. At least there's an easy workaround

[nilehmann]

Adding an extra example for this extracted from vtock.

#[flux::refined_by(head: int)]
pub struct AssignmentUnsafe {
    #[flux::field({usize[head] | head >= 0})]
    head: usize,
}

fn set(s: &mut AssignmentUnsafe) {
    s.head = 0; // causes assignment might be unsafe, but it shouldn't
}