[move-prover] Fixed hyper edge ordering problem

[awelc]

trafficstars

Motivation

This is an attempt to fix the Move prover problem reported and analyzed in https://github.com/move-language/move/issues/270

Please note that the bytecode translator changes are failing - due to changes that have been made expected result no longer matches the expected output - if the solution is correct we should update expected output.

Admittedly this solution has been crated "by feel" rather than by a super-deep knowledge of the borrow analyzer, but perhaps even if it's not 100% correct, it will inspire a proper solution.

Some observations:

1. It seems to me that hyper edges in borrowed_by and borrowed_from sets should be reverted, which is currently not the case (hence edge revert operation in consolidate).
2. The failure in the bytecode translator for the example in the related issue (https://github.com/move-language/move/issues/270) is due to a hyper edge in the borrowed_from set being in the wrong order, which means that considering the bullet above, it's the borrowed_from set should keep the "correct" (from the bytecode translator's perspective) order
3. The final bit is that in constructing function annotation (in summarize and then construct_hyper_edges) we use borrowed_from edge ("correct" order) to construct a borrowed_by edge (incorrect order), so we have to reverse the hyper edge (but not any edge as before).

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

I don't think we have Boogie backend tests, but with this PR in the test exposing the bug (added in https://github.com/move-language/move/pull/284) no longer crashes the prover.

[emmazzz]

Thanks! Awesome investigation @awelc ! Your solution looks sensible to me but will let Wolfgang check and approve it.

[awelc]

Superseded by https://github.com/move-language/move/pull/298