Skip to content

Commit

Permalink
[Compiler-v2] Relax check on whether a local can be written (#12890)
Browse files Browse the repository at this point in the history
* fix

* release
  • Loading branch information
rahxephon89 committed Apr 30, 2024
1 parent 1682e86 commit e5d6d25
Show file tree
Hide file tree
Showing 9 changed files with 146 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -1005,6 +1005,26 @@ impl<'env, 'state> LifetimeAnalysisStep<'env, 'state> {
}
}

/// Release all references that are not alive after this program point
/// from temp_to_label_map if `dests` do not contain any references
/// This function should be called before `check_write_local`
fn release_before_write_local(&mut self, dests: &[TempIndex]) {
let alive_temps = self.alive.after_set();
if !dests.iter().any(|temp| self.is_ref(*temp)) {
for temp in self
.state
.temp_to_label_map
.keys()
.cloned()
.collect::<Vec<_>>()
{
if !alive_temps.contains(&temp) && self.is_ref(temp) {
self.state.release_ref(temp)
}
}
}
}

/// Check whether a local can be written. This is only allowed if no borrowed references exist.
fn check_write_local(&self, local: TempIndex) {
if self.is_ref(local) {
Expand Down Expand Up @@ -1433,6 +1453,7 @@ impl<'env, 'state> LifetimeAnalysisStep<'env, 'state> {
}
} else {
self.check_read_local(src, mode);
self.release_before_write_local(&[dest]);
self.check_write_local(dest);
}
}
Expand Down Expand Up @@ -1498,6 +1519,7 @@ impl<'env, 'state> LifetimeAnalysisStep<'env, 'state> {
self.check_read_local(*src, ReadMode::Argument);
}
// Next check whether we can assign to the destinations.
self.release_before_write_local(dests);
for dest in dests {
self.check_write_local(*dest)
}
Expand Down Expand Up @@ -1688,6 +1710,7 @@ impl<'env, 'state> LifetimeAnalysisStep<'env, 'state> {
/// Process a MoveFrom instruction.
fn move_from(&mut self, dest: TempIndex, resource: &QualifiedInstId<StructId>, src: TempIndex) {
self.check_read_local(src, ReadMode::Argument);
self.release_before_write_local(&[dest]);
self.check_write_local(dest);
if let Some(label) = self.state.label_for_global_with_children(resource) {
self.error_with_hints(
Expand Down Expand Up @@ -1746,6 +1769,7 @@ impl<'env, 'state> LifetimeAnalysisStep<'env, 'state> {
/// Process a ReadRef instruction.
fn read_ref(&mut self, dest: TempIndex, src: TempIndex) {
debug_assert!(self.is_ref(src));
self.release_before_write_local(&[dest]);
self.check_write_local(dest);
self.check_read_local(src, ReadMode::Argument);
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

============ bytecode verification succeeded ========
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
module 0x42::m {

fun foo(x: &vector<u64>): (vector<u64>, u64) {
(*x, 0)
}


fun test_call() {
let y = vector[];
(y, _) = foo(&y);
assert!(y == vector[], 0);
}

fun test_assign() {
let y = vector[1];
(y, _) = (*&y, 1);
}

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@

============ bytecode verification succeeded ========
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@

Diagnostics:
error: cannot assign to borrowed local `_y`
┌─ tests/reference-safety/write_ref_dest_err.move:18:19
17 │ let z = &_y;
│ --- previous local borrow
18 │ (_y, _) = foo(&_y);
│ ^^^^^^^^ attempted to assign here
19 │ *z;
│ -- conflicting reference `z` used here

error: cannot assign to borrowed local `_y`
┌─ tests/reference-safety/write_ref_dest_err.move:25:9
24 │ let z = &_y;
│ --- previous local borrow
25 │ _y = vector[2];
│ ^^^^^^^^^^^^^^ attempted to assign here
26 │ *z;
│ -- conflicting reference `z` used here
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
module 0x42::m {

struct S has key, drop {

}

fun g(s: &S): &S {
s
}

fun foo(x: &vector<u64>): (vector<u64>, u64) {
(*x, 0)
}

fun test_call() {
let _y = vector[1];
let z = &_y;
(_y, _) = foo(&_y);
*z;
}

fun test_assign() {
let _y = vector[1];
let z = &_y;
_y = vector[2];
*z;
}

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@

Diagnostics:
error: cannot assign to borrowed local `_y`
┌─ tests/reference-safety/write_ref_dest_err.move:18:19
17 │ let z = &_y;
│ --- previous local borrow
18 │ (_y, _) = foo(&_y);
│ ^^^^^^^^ attempted to assign here
19 │ *z;
│ -- conflicting reference `z` used here

error: cannot assign to borrowed local `_y`
┌─ tests/reference-safety/write_ref_dest_err.move:25:9
24 │ let z = &_y;
│ --- previous local borrow
25 │ _y = vector[2];
│ ^^^^^^^^^^^^^^ attempted to assign here
26 │ *z;
│ -- conflicting reference `z` used here
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
processed 3 tasks

==> Compiler v2 delivered same results!
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
//# publish
module 0x42::m {

fun foo(x: &vector<u64>): (vector<u64>, u64) {
(*x, 0)
}


fun test_call() {
let y = vector[];
(y, _) = foo(&y);
assert!(y == vector[], 0);
}

fun test_assign() {
let y = vector[1];
(y, _) = (*&y, 1);
assert!(y == vector[1], 0);
}

}

//# run 0x42::m::test_call --check-runtime-types

//# run 0x42::m::test_assign --check-runtime-types

0 comments on commit e5d6d25

Please sign in to comment.