forked from aptos-labs/aptos-core
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[compiler-v2] Adapt reference safety to quirks of v1 bytecode verifie…
…r semantics (aptos-labs#12757) * [compiler-v2] Adapt reference safety to quirks of v1 bytecode verifier semantics This does a number of adaptions to reference safety to deal with some of the unexpected quirks of the v1 borrow semantics. Additional cases are now detected which are logical safe but anyway rejected by v1. Also, the treatment of freeze has been updated to relax some corner cases which led to failures in framework compilation. With this PR, all known bytecode verification failures are now detected except of a few which are sensitive to optimizations on and which pass without optimizations but not without (see aptos-labs#12756). This closes aptos-labs#12301 and closes aptos-labs#12701 - Fixes `borrow_global` borrow edge to carry a code offset, to be able to distinguish multiple global borrows with different addresses. Since the address in `borrow_global<R>(addr)` is dynamic, the reference checker cannot know whether to borrows results in the same reference. We already tackle this situation for calls which derive reference by adding the code offset, and now do the same for borrow global. - Makes assignment and let a checkpoint for borrow safety. Until now, we have considered those operations as no-ops for safety (which is safe from memory perspective), but v1 insists on borrow safety for those ops. - Adds a new check to borrow safety for mut refs which are duplicated and live beyond a safety check point. A particular quirk in v1 is that a mut ref which was used to derive another mut ref is allowed, but one which is duplicated is not. Since the information from which temps refs have been derived is not present in the borrow graph, which is designed to abstract from mut ref copies, we needed to introduce a new field in the borrow state to track this information. Specifically, the following is _not_ allowed in v1: `let r = &mut s; let r1 = r; let x = &mut r.f; *x; *r1`. However, this is allowed: `let r = &mut s; let x = &mut r.f; *x; *r`. The v1 logic behind this seems to be that `x` is derived from `r` but not (for the first example) from `r1`. * Addessing reviewer comments
- Loading branch information
Showing
41 changed files
with
879 additions
and
238 deletions.
There are no files selected for viewing
162 changes: 132 additions & 30 deletions
162
third_party/move/move-compiler-v2/src/pipeline/reference_safety_processor.rs
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
18 changes: 18 additions & 0 deletions
18
third_party/move/move-compiler-v2/tests/reference-safety/multiple_use_bug_12301.exp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,18 @@ | ||
|
|
||
| Diagnostics: | ||
| error: mutable reference in local `a` requires exclusive access but is borrowed | ||
| ┌─ tests/reference-safety/multiple_use_bug_12301.move:8:9 | ||
| │ | ||
| 8 │ *a = 0; | ||
| │ ^^^^^^ requirement enforced here | ||
| 9 │ *c | ||
| │ -- conflicting reference `c` used here | ||
|
|
||
| error: mutable reference in local `a` requires exclusive access but is borrowed | ||
| ┌─ tests/reference-safety/multiple_use_bug_12301.move:17:9 | ||
| │ | ||
| 17 │ *a = 0; | ||
| │ ^^^^^^ requirement enforced here | ||
| 18 │ *k = 1; | ||
| 19 │ *c | ||
| │ -- conflicting reference `c` used here |
21 changes: 21 additions & 0 deletions
21
third_party/move/move-compiler-v2/tests/reference-safety/multiple_use_bug_12301.move
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,21 @@ | ||
| // See also #12301 | ||
| module 0x42::m { | ||
| // Expected to be invalid | ||
| public fun test1(p: u64): u64 { | ||
| let a = &mut p; | ||
| let b = a; | ||
| let c = b; | ||
| *a = 0; | ||
| *c | ||
| } | ||
| // Expected to be invalid | ||
| public fun test2(p: u64): u64 { | ||
| let a = &mut p; | ||
| let k = &mut p; | ||
| let b = a; | ||
| let c = b; | ||
| *a = 0; | ||
| *k = 1; | ||
| *c | ||
| } | ||
| } |
18 changes: 18 additions & 0 deletions
18
third_party/move/move-compiler-v2/tests/reference-safety/multiple_use_bug_12301.no-opt.exp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,18 @@ | ||
|
|
||
| Diagnostics: | ||
| error: mutable reference in local `a` requires exclusive access but is borrowed | ||
| ┌─ tests/reference-safety/multiple_use_bug_12301.move:8:9 | ||
| │ | ||
| 8 │ *a = 0; | ||
| │ ^^^^^^ requirement enforced here | ||
| 9 │ *c | ||
| │ -- conflicting reference `c` used here | ||
|
|
||
| error: mutable reference in local `a` requires exclusive access but is borrowed | ||
| ┌─ tests/reference-safety/multiple_use_bug_12301.move:17:9 | ||
| │ | ||
| 17 │ *a = 0; | ||
| │ ^^^^^^ requirement enforced here | ||
| 18 │ *k = 1; | ||
| 19 │ *c | ||
| │ -- conflicting reference `c` used here |
25 changes: 25 additions & 0 deletions
25
third_party/move/move-compiler-v2/tests/reference-safety/mut_borrow_after_invalid.exp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
|
|
||
| Diagnostics: | ||
| error: mutable reference in local `f` requires exclusive access but is borrowed | ||
| ┌─ tests/reference-safety/mut_borrow_after_invalid.move:8:9 | ||
| │ | ||
| 8 │ *f; | ||
| │ ^^ requirement enforced here | ||
| 9 │ *s1; | ||
| │ --- conflicting reference `s1` used here | ||
|
|
||
| error: mutable reference in local `a` requires exclusive access but is borrowed | ||
| ┌─ tests/reference-safety/mut_borrow_after_invalid.move:16:9 | ||
| │ | ||
| 16 │ *a = 0; | ||
| │ ^^^^^^ requirement enforced here | ||
| 17 │ *b | ||
| │ -- conflicting reference `b` used here | ||
|
|
||
| error: mutable reference in local `a` requires exclusive access but is borrowed | ||
| ┌─ tests/reference-safety/mut_borrow_after_invalid.move:25:9 | ||
| │ | ||
| 25 │ *a = 0; | ||
| │ ^^^^^^ requirement enforced here | ||
| 26 │ *c | ||
| │ -- conflicting reference `c` used here |
40 changes: 40 additions & 0 deletions
40
third_party/move/move-compiler-v2/tests/reference-safety/mut_borrow_after_invalid.move
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,40 @@ | ||
| module 0x42::m { | ||
| struct S has copy, drop { f: u64, g: u64 } | ||
|
|
||
| // bytecode verification fails | ||
| fun t1(s: &mut S) { | ||
| let s1 = s; | ||
| let f = &mut s.f; | ||
| *f; | ||
| *s1; | ||
| } | ||
|
|
||
| // bytecode verification fails | ||
| fun t3(p: u64): u64 { | ||
| let a = &mut p; | ||
| let b = a; | ||
| *a = 0; | ||
| *b | ||
| } | ||
|
|
||
| // bytecode verification fails | ||
| fun t4(p: u64): u64 { | ||
| let a = &mut p; | ||
| let b = a; | ||
| let c = b; | ||
| *a = 0; | ||
| *c | ||
| } | ||
|
|
||
| fun id_mut<T>(r: &mut T): &mut T { | ||
| r | ||
| } | ||
|
|
||
| // bytecode verification fails | ||
| fun t5() { | ||
| let x = &mut 0; | ||
| let y = id_mut(x); | ||
| *y; | ||
| *x; | ||
| } | ||
| } |
25 changes: 25 additions & 0 deletions
25
third_party/move/move-compiler-v2/tests/reference-safety/mut_borrow_after_invalid.no-opt.exp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,25 @@ | ||
|
|
||
| Diagnostics: | ||
| error: mutable reference in local `f` requires exclusive access but is borrowed | ||
| ┌─ tests/reference-safety/mut_borrow_after_invalid.move:8:9 | ||
| │ | ||
| 8 │ *f; | ||
| │ ^^ requirement enforced here | ||
| 9 │ *s1; | ||
| │ --- conflicting reference `s1` used here | ||
|
|
||
| error: mutable reference in local `a` requires exclusive access but is borrowed | ||
| ┌─ tests/reference-safety/mut_borrow_after_invalid.move:16:9 | ||
| │ | ||
| 16 │ *a = 0; | ||
| │ ^^^^^^ requirement enforced here | ||
| 17 │ *b | ||
| │ -- conflicting reference `b` used here | ||
|
|
||
| error: mutable reference in local `a` requires exclusive access but is borrowed | ||
| ┌─ tests/reference-safety/mut_borrow_after_invalid.move:25:9 | ||
| │ | ||
| 25 │ *a = 0; | ||
| │ ^^^^^^ requirement enforced here | ||
| 26 │ *c | ||
| │ -- conflicting reference `c` used here |
2 changes: 2 additions & 0 deletions
2
third_party/move/move-compiler-v2/tests/reference-safety/mut_borrow_after_valid.exp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,2 @@ | ||
|
|
||
| ============ bytecode verification succeeded ======== |
Oops, something went wrong.