Added MIR optimization to avoid unnecessary re-borrows

[dewert99]

In trying to come up with a good way to handle #869 and #902, most of the trouble seems to come from unnecessary reborrowing in the MIR. If it wasn't for that adding a third field to mutable references might be enough to solve these issues while not breaking too many tests ({ x with current = y } would preserve the third field but Borrow.borrow_mut y would not).
Removing these reborrows also simplifies the Why3 a bit, it probably doesn't make a huge difference to provers, but it might be nice for people using the Why3IDE.

Since I didn't want to mess with the MIR to FMIR transformation I implemented this as a MIR optimization that runs before the analysis so the borrow-checker facts used to determine resolution are accurate. The "optimization" translates statements of the form _x = &mut *_y to _x = move _y when _y: &mut _ and _y is dead after the statement. I think this should be sound but I'm just making this a draft to see what you think.

[xldenis]

Since I didn't want to mess with the MIR to FMIR transformation I implemented this as a MIR optimization that runs before the analysis so the borrow-checker facts used to determine resolution are accurate.

The alternative would be to do it as an FMIR -> FMIR pass.

In trying to come up with a good way to handle #869 and #902, most of the trouble seems to come from unnecessary reborrowing in the MIR. If it wasn't for that adding a third field to mutable references might be enough to solve these issues while not breaking too many tests ({ x with current = y } would preserve the third field but Borrow.borrow_mut y would not).

Indeed, but one thing we're trying to balance with this is ensuring that x is equivalent to &mut * x, I think the current design for non-extensionality has that property.

[jhjourdan]

I think that indeed removing these unnecessary reborrows can help simplify the generated MLCFG code and thus the goal in Why3IDE.

That being said, I don't think this helps much for having non-extensional reborrows that would solve the unsoundness in #869. The reason for that is that we want to address simultaneously solve the following goals:

1. Make borrows non-extensional in a way that fixes the unsoundness. In particular, this implies that two borrows with two different prophecies should be considered different, even if the value of the prophecy is the same. So, if a variable is reborrowed in a way where the initial borrow can be reused, then the reborrow and the initial borrow should not be considered equal, even if their current value and their prophetic values turn out to be equal.

2. Make reborrows in executable code equivalent to logical reborrowing, when the initial borrow will not be reused. In particular, this should be true for field reborrows:

#[ensures(result == &mut x.0)]
fn f(x : &mut (i32, i32)) -> &mut i32 {
  &mut x.0
}

I don't think this last example can be handle by a MIR/FMIR optimization, it should really be handle by translating "dead reborrows" in a specific way.

A particularly tricky example is in 15_enumerate.rs:

    #[open]
    #[predicate]
    fn completed(&mut self) -> bool {
        pearlite! { self.iter.completed() }
    }

    #[ensures(match result {
      None => self.completed(),
      Some(v) => ...
    })]
    fn next(&mut self) -> Option<Self::Item> {
        match self.iter.next() {
            None => None,
            Some(x) => {
                let n = self.count;
                self.count += 1;
                Some((n, x))
            }
        }
    }

Here, in the None case, we want the reborrow &mut self.iter to be equal to its logical equivalent so that we can use the completed logical function in the post-condition. However, the borrow self is still used in the Some branch.

We could even imagine an example where we reborrow self.iter in the Some branch. In this case, we would still want the reborrow to be equal to its logical counterpart in the None branch, even though at the time of reborrowing the parent borrow is not dead.

[dewert99]

The alternative would be to do it as an FMIR -> FMIR pass.

I think doing MIR->MIR was easier since the change is more local (it doesn't need to consider resolves), and it could use the existing MIR liveness analysis.

[jhjourdan]

What's the status of this? Now that #912 is merged, it seems like the only motivation for this is simplifying the generated MLCFG. Is this something that we still want to put some energy in?

[xldenis]

Perhaps not this exact code, but I think it would probably be worthwhile to validate whether we have improved performance with this, especially if we can whip up a simple PoC version. My biggest worry is that this optimization would fundamentally change which borrows are final, and thus be observable at verification time.

[jhjourdan]

My biggest worry is that this optimization would fundamentally change which borrows are final, and thus be observable at verification time.

That's a good point that we should take care, although I'm pretty sure that in most of the cases the finality of borrows should not change.

[jhjourdan]

(My point being that these unecessaries reborrows that we are removing in this PR would have been considered final afterwards, thus we would essentially have the same behavior.)

[xldenis]

That's a good point that we should take care, although I'm pretty sure that in most of the cases the finality of borrows should not change.

Yes, but we would need to verify that this is true.