[move-prover] treat store as copy in borrow analysis

[meng-xu-cs]

Prover panic-ed when trying to verify this simple program:

    fun one_of_two(cond: bool, r1: &mut u64, r2: &mut u64): &mut u64 {
        if (cond) {r1} else {r2}
    }

    fun test1(cond: bool, v1: u64, v2: u64) {
        let r = one_of_two(cond, &mut v1, &mut v2);
        *r = 0;

        spec {
            assert cond ==> v1 == 0;
            assert !cond ==> v2 == 0;
        }
    }

A further analysis found that the borrow summary for function one_of_two is not
properly constructed, with the return result not borrowing from neither r1 or r2
(which it should be a direct borrow of r1 or r2).

After some digging in the bytecode, it seems that we are using r := r1 and r = r2
for the assignment, which is considered as a Store assignment and is treated
the same way as a Move assignment. This seems correct in terms borrow semantics
but there is no way of summarizing that r can be borrowed from either r1 or r2
which is needed in the verification of test1.

A quick solution to this is to model Store as a Copy assignment, which adds
the BorrowEdge::Direct in the borrow graph. The downside, however, is that the
RHS of the assignment now lives longer until it is destroy()-ed, as can be seen in
the changes of the baseline file.

Motivation

To verify the above simple program.

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

• CI
• A new unit test is added
• Manually run the prover inconsistency tests against DPN

[emmazzz]

Good catch! The solution makes sense to me too.

[meng-xu-cs]

Still self-debating whether we should call this type of edge 'Direct' or invent a new name, but that can be addressed separately.