Open enjhnsn2 opened 4 months ago
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.
Ah, alright. At least there's an easy workaround
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
}
The following code is safe, but flux flags that it may integer underflow:
fails with:
This does not happen if the function takes a immutable parameter. The following code passes: