Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[move-prover] multiple fixes to the memory model (move-language#312)
* [move-prover] fix is_parent tests for multiple write-back chains PR move-language#302 has an error in terms of placing `IsParent` checks for different borrow chains. Consider the following case: ``` --borrows_from--> C A --borrows_from--> B --| --borrows_from--> D ``` When references A, B, C, D go out of scope, this will yield two chain of references: A --> B --> C and A --> B --> D This is correctly captured in move-language#302. The bug is how to generate the `IsParent` test: The correct behavior is the following: ``` if IsParent[C](B) WriteBack[B](A) WriteBack[C](B) if IsParent[D](B) WriteBack[B](A) WriteBack[D](B) ``` i.e., branching at node B. But in move-language#302, I mistakenly used the root of the chain as the branching point and hence, both the tests become `IsParent[B](A)`, which is not correct. This commit fixes this issue by deriving the deterministic factor for the write-back chain. Consider the case with the borrowing graph: ``` ---> E ---> C -| A ---> B -| ---> F ---> D ``` This will yield three chains: ``` if IsParent[C](B) && IsParent[E](C) WriteBack[B](A) WriteBack[C](B) WriteBack[E](C) if IsParent[C](B) && IsParent[F](C) WriteBack[B](A) WriteBack[C](B) WriteBack[F](C) if IsParent[D](B) WriteBack[B](A) WriteBack[D](B) ``` * [move-prover] improve the peephole optimization for write-back chains * [move-prover] do not peephole optimize the initial local and global borrows Live variable analysis allows the following peephole optimization: ``` $t := call(...) x := $t <$t is dead> ~~~ x := call(...) ``` This optimization makes perfect sense but unfortunately conflicts with one policy later: IsParent test can only be applied on two references: Taking the following code as an example: ``` let v1 = 0; let v2 = 0; let r = if (cond) { let r1 = &mut v1; r1 } else { let r2 = &mut v2; r2 }; ``` References `r1` and `r2` will be optimized away after the live var analysis. This leaves the reference `r` pointing to two local locations. And later when translating `IsParent` test to Boogie, we will run into cases like: ``` IsParent[LocalRoot(v1)@](r) IsParent[LocalRoot(v2)@](r) ``` And this violates our policy that IsParent can only be applied among two references. As a result, we disable this optimization for the initial local/global borrowing, which leaves the IsParent tests to be ``` IsParent[Reference(r1)@](r) IsParent[Reference(r2]@](r) ``` An alternative solution to this problem is to implement IsParent tests between a reference to a `LocalRoot` and a `GloablRoot`. But that is a more significant change and does not buy much benefits performance-wise. * [move-prover] use a special location to mark uninitialized mut refs Mutable references cannot be arbitrarily initialized, they must be initialized into a state where the IsParent test have to fail if this reference is not assigned otherwise. To be specific, consider the folowing example: ``` let v1 = 0; let v2 = 0; let r = if (cond) { let r1 = &mut v1; r1 } else { let r2 = &mut v2; r2 }; ``` This will be translated to: ``` r1 := $uninitialized(); r2 := $uninitialized(); ... <omitted> ... if (cond) { r1 := borrow_local(v1); r := r1 } else { r2 := borrow_local(v2); r := r2 } ... <omitted> ... if (IsParent[r1](r)) { WriteBack[r1](r); WriteBack[v1](r1); } if (IsParent[r2](r)) { WriteBack[r2](r); WriteBack[v2](r2); } ``` It is very important to mark `r1` and `r2` and `$uninitialized()` to ensure that there will be one and only one `IsParent` test activated when the write-back happens. The previous approach is to `assume IsEmptyVec(p#$Mutation($t_i));` for all `t_i` that is a mutable reference used in function locals. However, setting the `path` vector in the `Mutation` struct to zero does not guarantee that this mutation, when put under `IsParent` test, is not going to return false when that mutation is not initialized. As can be seen in the example above, even after proper assignment, `r1` and `r2` both have a `path` equal to the length of zero... (because `r` is borrowing from `r1` and `r2` `as direct borrow, not field or element borrow). This commit fixes this issue with an explicit `$Uninitialize()` constructor for the `$Location` part of a `$Mutation`. * [move-prover] use an `Uninit` operation to mark uninitialized mut refs Following from the above commit, instead of marking all mutable references in the function locals (except the function arguments) as uninitialized, this commit further restrict the number of mutable references that can be marked as `Uninit`, hence, reducing the chances of introducing inconsistent assumptions in the verification. The basic idea is to leverage the livevar analysis results, and mark whatever mutable reference that is 1) alive even before the first instruction of the function and 2) is not a parameter, as uninitialized. This commit also includes a fix to the concrete spec executor such that we do not run into errors when a mutable reference is mysterously destroyed even before it is initialized. * [move-prover] do not let bind a mutable reference for `EmitEvent` ``` public fun emit_event<T>(handle_ref: &mut EventHandle<T>, msg: T) { ... } ``` Events are verified in Move Prover in a special manner. One example is that the `EmitEvent` bytecode is especially designed to simulate the `emit_event` function. During the invocation of `EmitEvent`, we might be let-binding a mutable reference which we really do not want as introcuing a mutable reference via `Assume(Identical)` complicates the live var and borrow analysis (for example, we will treat the newly bounded reference as uninitialized). While essentially we do not need a reference to the handle and we can just let-bound the `$Dereference ( <exp> )` value directly, which is what is essentially done in this commit. * [move-prover] update exp files for existing tests * [move-prover] new tests to summarize the changes * [move-prover][interpreter] update the concrete semantics with direct ref borrow This re-enables the failing `if_else.move` test which conditionally (and directly) assign references to another reference.
- Loading branch information
1 parent
0fda31b
commit e19e49a