Closed petrosagg closed 2 years ago
Can you talk me through why it isn't a false positive? The loop invariant is that offset < index
, and if that isn't true there is a bigger problem. Does the test case demonstrate a violation of this invariant?
// LOOP INVARIANT: offset < index
let ptr1 = slice.as_mut_ptr().offset(offset as isize);
let ptr2 = slice.as_mut_ptr().offset(index as isize);
Edit: mystery resolved: we re-bind ptr1
just a few lines later. It seems like these lines might just be in the wrong order; I'd rather sort that out than put some more conditional logic in.
let ptr1 = slice.as_mut_ptr().offset(offset as isize);
Yeah the invariant is violated in the else statement with the test case I added
So I think I figured out what I meant by "in the wrong order" above. The consolidation logic switches from "validating" in which all adjacent elements are distinct, to "compacting" as soon as two elements have equal keys. In the former no movement needs to happen, and in the latter the swapping is always between distinct locations.
If you don't mind, I'll write that up, and then maybe we can check that it passes the test?
@frankmcsherry I updated the code to a version that doesn't have an extra check. edit: I maybe have talked too fast. Validating again now
ok I put up a final version that replaces std::mem::swap
with std::ptr::swap
which is ok with aliasing mut pointers
Running the added testcase under miri without the equality check results in Undefined Behaviour from creating two mutable references pointing to the same location.