Skip to content

Commit e52145d

Browse files
wrwgwrwg
authored
[compiler v2] New Borrow Analysis (aptos-labs#11892)
* [compiler v2] New Borrow Analysis This is a major rewrite of the reference safety analysis. This PR closes aptos-labs#11251 which shows the problem with the previous version: essentially, it is necessary to allow for a sequence of instructions an "unsafe" borrow graph and only enforce safety at particular instruction boundaries. The simplest example to demonstrate the problem is `f(&mut s.x, &mut s.y)`. If broken down to instructions, at some point there will be a reference to `&mut s` where at the same time there is another one `&mut s.f`, which is unsafe if those refs would be passed as function parameters. The rewrite does the following: - Instead of checking safety of borrow operations at the time they are performed, the graph is now constructed first, and later checked for safety at particular instructions (read ref, write ref, and function calls) - The borrow graph stays mostly the same, instead of Skip edges for graph glueing which became overly complex, glueing is now performed by graph renaming. - There are various enhancements in error reporting (and potentially because of the delayed borrow checking also some regressions) It might be useful to review the new version without diff from scratch. * Adding some ASCII graphics to the documentation of the analysis domain. * Adding a copy of the new analysis in `reference_safety_processor_v2.rs`. This allows for review from the basics. * Updating reference safety: - Unifying the three borrow safety checks now in `check_graph_safety`. Documenting them more concisely in the module overview with a sketch of a more formal semantics. - Reducing graph safety checks to argument locals, removing some false positives. - Covering a missed violation of using the same reference multiple times in an argument list * Minor renamings, fixing tests * Addressing reviewer comments * Updating reference_safety_processor_v2, renaming more local to temp * Fixing tests * Change permutations to combinations * Addressing reviewer comments. * Final touches for merge
1 parent b16459e commit e52145d

File tree

74 files changed

+3910
-2994
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

74 files changed

+3910
-2994
lines changed

‎.github/workflows/coverage-move-only.yaml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ jobs:
5050
with:
5151
tool: nextest,cargo-llvm-cov
5252
- run: docker run --detach -p 5432:5432 cimg/postgres:14.2
53-
- run: cargo llvm-cov --ignore-run-fail -p aptos-framework -p "move*" -p e2e-move-tests --lcov --jobs 32 --output-path lcov_unit.info
53+
- run: cargo llvm-cov --ignore-run-fail -p aptos-framework -p "move*" --lcov --jobs 32 --output-path lcov_unit.info
5454
env:
5555
INDEXER_DATABASE_URL: postgresql://postgres@localhost/postgres
5656
- uses: actions/upload-artifact@v3

‎third_party/move/move-compiler-v2/src/lib.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ pub mod flow_insensitive_checkers;
99
pub mod function_checker;
1010
pub mod inliner;
1111
pub mod logging;
12-
mod options;
12+
pub mod options;
1313
pub mod pipeline;
1414

1515
use crate::pipeline::{

‎third_party/move/move-compiler-v2/src/pipeline/reference_safety_processor.rs‎

Lines changed: 1113 additions & 832 deletions
Large diffs are not rendered by default.

‎third_party/move/move-compiler-v2/tests/ability-checker/ability_violation.exp‎

Lines changed: 38 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ fun ability::no_key($t0: address) {
115115
6: return ()
116116
}
117117

118-
============ after MemorySafetyProcessor: ================
118+
============ after ReferenceSafetyProcessor: ================
119119

120120
[variant baseline]
121121
fun ability::invalid_copy() {
@@ -126,43 +126,43 @@ fun ability::invalid_copy() {
126126
var $t4: ability::Impotent
127127
# live vars:
128128
# graph: {}
129-
# local_to_label: {}
130-
# global_to_label: {}
129+
# locals: {}
130+
# globals: {}
131131
# moved: {}
132132
#
133133
0: $t2 := false
134134
# live vars: $t2
135135
# graph: {}
136-
# local_to_label: {}
137-
# global_to_label: {}
136+
# locals: {}
137+
# globals: {}
138138
# moved: {}
139139
#
140140
1: $t1 := pack ability::Impotent($t2)
141141
# live vars: $t1
142142
# graph: {}
143-
# local_to_label: {}
144-
# global_to_label: {}
143+
# locals: {}
144+
# globals: {}
145145
# moved: {$t2}
146146
#
147147
2: $t0 := move($t1)
148148
# live vars: $t0
149149
# graph: {}
150-
# local_to_label: {}
151-
# global_to_label: {}
150+
# locals: {}
151+
# globals: {}
152152
# moved: {$t1,$t2}
153153
#
154154
3: $t3 := copy($t0)
155155
# live vars: $t0
156156
# graph: {}
157-
# local_to_label: {}
158-
# global_to_label: {}
157+
# locals: {}
158+
# globals: {}
159159
# moved: {$t1,$t2}
160160
#
161161
4: $t4 := move($t0)
162162
# live vars:
163163
# graph: {}
164-
# local_to_label: {}
165-
# global_to_label: {}
164+
# locals: {}
165+
# globals: {}
166166
# moved: {$t0,$t1,$t2}
167167
#
168168
5: return ()
@@ -174,30 +174,30 @@ fun ability::invalid_move_to($t0: &signer) {
174174
var $t1: ability::Impotent
175175
var $t2: bool
176176
# live vars: $t0
177-
# graph: {}
178-
# local_to_label: {}
179-
# global_to_label: {}
177+
# graph: {@1000000=external[borrow(false) -> @2000000],@2000000=derived[]}
178+
# locals: {$t0=@2000000}
179+
# globals: {}
180180
# moved: {}
181181
#
182182
0: $t2 := false
183183
# live vars: $t0, $t2
184-
# graph: {}
185-
# local_to_label: {}
186-
# global_to_label: {}
184+
# graph: {@1000000=external[borrow(false) -> @2000000],@2000000=derived[]}
185+
# locals: {$t0=@2000000}
186+
# globals: {}
187187
# moved: {}
188188
#
189189
1: $t1 := pack ability::Impotent($t2)
190190
# live vars: $t0, $t1
191-
# graph: {}
192-
# local_to_label: {}
193-
# global_to_label: {}
191+
# graph: {@1000000=external[borrow(false) -> @2000000],@2000000=derived[]}
192+
# locals: {$t0=@2000000}
193+
# globals: {}
194194
# moved: {$t2}
195195
#
196196
2: move_to<ability::Impotent>($t0, $t1)
197197
# live vars:
198198
# graph: {}
199-
# local_to_label: {}
200-
# global_to_label: {}
199+
# locals: {}
200+
# globals: {}
201201
# moved: {$t0,$t1,$t2}
202202
#
203203
3: return ()
@@ -214,50 +214,50 @@ fun ability::no_key($t0: address) {
214214
var $t6: bool
215215
# live vars: $t0
216216
# graph: {}
217-
# local_to_label: {}
218-
# global_to_label: {}
217+
# locals: {}
218+
# globals: {}
219219
# moved: {}
220220
#
221221
0: $t1 := copy($t0)
222222
# live vars: $t0, $t1
223223
# graph: {}
224-
# local_to_label: {}
225-
# global_to_label: {}
224+
# locals: {}
225+
# globals: {}
226226
# moved: {}
227227
#
228228
1: $t2 := move_from<ability::Impotent>($t1)
229229
# live vars: $t0
230230
# graph: {}
231-
# local_to_label: {}
232-
# global_to_label: {}
231+
# locals: {}
232+
# globals: {}
233233
# moved: {}
234234
#
235235
2: $t3 := move_from<ability::S<ability::Impotent>>($t0)
236236
# live vars: $t0
237237
# graph: {}
238-
# local_to_label: {}
239-
# global_to_label: {}
238+
# locals: {}
239+
# globals: {}
240240
# moved: {}
241241
#
242242
3: $t4 := borrow_global<ability::Impotent>($t0)
243243
# live vars: $t0
244244
# graph: {}
245-
# local_to_label: {}
246-
# global_to_label: {}
245+
# locals: {}
246+
# globals: {}
247247
# moved: {}
248248
#
249249
4: $t5 := borrow_global<ability::Impotent>($t0)
250250
# live vars: $t0
251251
# graph: {}
252-
# local_to_label: {}
253-
# global_to_label: {}
252+
# locals: {}
253+
# globals: {}
254254
# moved: {}
255255
#
256256
5: $t6 := exists<ability::Impotent>($t0)
257257
# live vars:
258258
# graph: {}
259-
# local_to_label: {}
260-
# global_to_label: {}
259+
# locals: {}
260+
# globals: {}
261261
# moved: {$t0}
262262
#
263263
6: return ()

‎third_party/move/move-compiler-v2/tests/ability-checker/assign.exp‎

Lines changed: 42 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -104,29 +104,29 @@ fun assign::assign_struct($t0: &mut assign::S) {
104104
5: return ()
105105
}
106106

107-
============ after MemorySafetyProcessor: ================
107+
============ after ReferenceSafetyProcessor: ================
108108

109109
[variant baseline]
110110
fun assign::assign_field($t0: &mut assign::S, $t1: u64) {
111111
var $t2: &mut u64
112112
# live vars: $t0, $t1
113-
# graph: {}
114-
# local_to_label: {}
115-
# global_to_label: {}
113+
# graph: {@1000000=external[borrow(true) -> @2000000],@2000000=derived[]}
114+
# locals: {$t0=@2000000}
115+
# globals: {}
116116
# moved: {}
117117
#
118118
0: $t2 := borrow_field<assign::S>.f($t0)
119119
# live vars: $t1, $t2
120-
# graph: {L0=local($t0)[borrow_field(true) -> L1],L1=local($t2)[]}
121-
# local_to_label: {$t0=L0,$t2=L1}
122-
# global_to_label: {}
120+
# graph: {@1=derived[],@1000000=external[borrow(true) -> @2000000],@2000000=derived[borrow_field(true) -> @1]}
121+
# locals: {$t2=@1}
122+
# globals: {}
123123
# moved: {}
124124
#
125125
1: write_ref($t2, $t1)
126126
# live vars:
127127
# graph: {}
128-
# local_to_label: {}
129-
# global_to_label: {}
128+
# locals: {}
129+
# globals: {}
130130
# moved: {}
131131
#
132132
2: return ()
@@ -137,23 +137,23 @@ fun assign::assign_field($t0: &mut assign::S, $t1: u64) {
137137
fun assign::assign_int($t0: &mut u64) {
138138
var $t1: u64
139139
# live vars: $t0
140-
# graph: {}
141-
# local_to_label: {}
142-
# global_to_label: {}
140+
# graph: {@1000000=external[borrow(true) -> @2000000],@2000000=derived[]}
141+
# locals: {$t0=@2000000}
142+
# globals: {}
143143
# moved: {}
144144
#
145145
0: $t1 := 42
146146
# live vars: $t0, $t1
147-
# graph: {}
148-
# local_to_label: {}
149-
# global_to_label: {}
147+
# graph: {@1000000=external[borrow(true) -> @2000000],@2000000=derived[]}
148+
# locals: {$t0=@2000000}
149+
# globals: {}
150150
# moved: {}
151151
#
152152
1: write_ref($t0, $t1)
153153
# live vars:
154154
# graph: {}
155-
# local_to_label: {}
156-
# global_to_label: {}
155+
# locals: {}
156+
# globals: {}
157157
# moved: {}
158158
#
159159
2: return ()
@@ -166,29 +166,29 @@ fun assign::assign_pattern($t0: assign::S, $t1: u64, $t2: u64): u64 {
166166
var $t4: assign::T
167167
# live vars: $t0
168168
# graph: {}
169-
# local_to_label: {}
170-
# global_to_label: {}
169+
# locals: {}
170+
# globals: {}
171171
# moved: {}
172172
#
173173
0: ($t1, $t4) := unpack assign::S($t0)
174174
# live vars: $t1, $t4
175175
# graph: {}
176-
# local_to_label: {}
177-
# global_to_label: {}
176+
# locals: {}
177+
# globals: {}
178178
# moved: {$t0}
179179
#
180180
1: $t2 := unpack assign::T($t4)
181181
# live vars: $t1, $t2
182182
# graph: {}
183-
# local_to_label: {}
184-
# global_to_label: {}
183+
# locals: {}
184+
# globals: {}
185185
# moved: {$t0,$t4}
186186
#
187187
2: $t3 := +($t1, $t2)
188188
# live vars: $t3
189189
# graph: {}
190-
# local_to_label: {}
191-
# global_to_label: {}
190+
# locals: {}
191+
# globals: {}
192192
# moved: {$t0,$t1,$t2,$t4}
193193
#
194194
3: return $t3
@@ -202,44 +202,44 @@ fun assign::assign_struct($t0: &mut assign::S) {
202202
var $t3: assign::T
203203
var $t4: u64
204204
# live vars: $t0
205-
# graph: {}
206-
# local_to_label: {}
207-
# global_to_label: {}
205+
# graph: {@1000000=external[borrow(true) -> @2000000],@2000000=derived[]}
206+
# locals: {$t0=@2000000}
207+
# globals: {}
208208
# moved: {}
209209
#
210210
0: $t2 := 42
211211
# live vars: $t0, $t2
212-
# graph: {}
213-
# local_to_label: {}
214-
# global_to_label: {}
212+
# graph: {@1000000=external[borrow(true) -> @2000000],@2000000=derived[]}
213+
# locals: {$t0=@2000000}
214+
# globals: {}
215215
# moved: {}
216216
#
217217
1: $t4 := 42
218218
# live vars: $t0, $t2, $t4
219-
# graph: {}
220-
# local_to_label: {}
221-
# global_to_label: {}
219+
# graph: {@1000000=external[borrow(true) -> @2000000],@2000000=derived[]}
220+
# locals: {$t0=@2000000}
221+
# globals: {}
222222
# moved: {}
223223
#
224224
2: $t3 := pack assign::T($t4)
225225
# live vars: $t0, $t2, $t3
226-
# graph: {}
227-
# local_to_label: {}
228-
# global_to_label: {}
226+
# graph: {@1000000=external[borrow(true) -> @2000000],@2000000=derived[]}
227+
# locals: {$t0=@2000000}
228+
# globals: {}
229229
# moved: {$t4}
230230
#
231231
3: $t1 := pack assign::S($t2, $t3)
232232
# live vars: $t0, $t1
233-
# graph: {}
234-
# local_to_label: {}
235-
# global_to_label: {}
233+
# graph: {@1000000=external[borrow(true) -> @2000000],@2000000=derived[]}
234+
# locals: {$t0=@2000000}
235+
# globals: {}
236236
# moved: {$t2,$t3,$t4}
237237
#
238238
4: write_ref($t0, $t1)
239239
# live vars:
240240
# graph: {}
241-
# local_to_label: {}
242-
# global_to_label: {}
241+
# locals: {}
242+
# globals: {}
243243
# moved: {$t2,$t3,$t4}
244244
#
245245
5: return ()

0 commit comments

Comments
 (0)