Skip to content

Commit

Permalink
[compiler-v2] Adding and verifying some missing v1 tests
Browse files Browse the repository at this point in the history
This goes through all urgent bugs in the spreadsheet from issue #13747 and verifies that they have been resolved with recent changes.
  • Loading branch information
wrwg committed Aug 19, 2024
1 parent 7964b40 commit 6957ff6
Show file tree
Hide file tree
Showing 32 changed files with 468 additions and 6 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@

Diagnostics:
error: unnecessary acquires annotation
┌─ tests/acquires-checker/v1-borrow-tests/acquires_list_generic.move:6:24
6 │ fun foo() acquires B<CupC<R>> {
│ ^^^^^^^^^^^
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module 0x42::M {
struct CupC<phantom T> {}
struct R {}
struct B<phantom T> {}

fun foo() acquires B<CupC<R>> {
abort 0
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@

Diagnostics:
error: not supported before language version `2.0-unstable`: access specifier type instantiation. Try removing the type instantiation.
┌─ tests/checking-lang-v1/acquires_list_generic.move:6:24
6 │ fun foo() acquires B<CupC<R>> {
│ ^^^^^^^^^^^
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module 0x42::M {
struct CupC<phantom T> {}
struct R {}
struct B<phantom T> {}

fun foo() acquires B<CupC<R>> {
abort 0
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
// -- Model dump before bytecode pipeline
module 0x42::M {
struct B {
dummy_field: bool,
}
struct CupC {
dummy_field: bool,
}
struct R {
dummy_field: bool,
}
private fun foo()
acquires M::B<M::CupC<M::R>>(*)
{
Abort(0)
}
} // end 0x42::M
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module 0x42::M {
struct CupC<phantom T> {}
struct R {}
struct B<phantom T> {}

fun foo() acquires B<CupC<R>> {
abort 0
}
}
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,42 @@
module 0x8675309::Tester {
fun eqtest1() {
let x: u64;
let r: &mut u64;

x = 0;
r = &mut x;
_ = copy r == copy r;
}

fun eqtest2() {
let x: u64;
let r: &mut u64;

x = 0;
r = &mut x;
_ = copy r == move r;
}

fun neqtest1() {
let x: u64;
let r: &mut u64;

x = 0;
r = &mut x;
_ = copy r != copy r;
}

fun neqtest2() {
let x: u64;
let r: &mut u64;

x = 0;
r = &mut x;
_ = copy r != move r;
}
}

// check: READREF_EXISTS_MUTABLE_BORROW_ERROR
// check: READREF_EXISTS_MUTABLE_BORROW_ERROR
// check: READREF_EXISTS_MUTABLE_BORROW_ERROR
// check: READREF_EXISTS_MUTABLE_BORROW_ERROR
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,41 @@

Diagnostics:
error: mutable reference in local `r` requires exclusive access but is borrowed
┌─ tests/reference-safety/v1-borrow-tests/eq_bad.move:8:23
8 │ _ = copy r == copy r;
│ ----------^^^^^^
│ │ │
│ │ requirement enforced here
│ conflicting reference used here
│ previous freeze

error: mutable reference in local `r` requires exclusive access but is borrowed
┌─ tests/reference-safety/v1-borrow-tests/eq_bad.move:17:23
17 │ _ = copy r == move r;
│ ----------^^^^^^
│ │ │
│ │ requirement enforced here
│ conflicting reference used here
│ previous freeze

error: mutable reference in local `r` requires exclusive access but is borrowed
┌─ tests/reference-safety/v1-borrow-tests/eq_bad.move:26:23
26 │ _ = copy r != copy r;
│ ----------^^^^^^
│ │ │
│ │ requirement enforced here
│ conflicting reference used here
│ previous freeze

error: mutable reference in local `r` requires exclusive access but is borrowed
┌─ tests/reference-safety/v1-borrow-tests/eq_bad.move:35:23
35 │ _ = copy r != move r;
│ ----------^^^^^^
│ │ │
│ │ requirement enforced here
│ conflicting reference used here
│ previous freeze
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,37 @@
module 0x8675309::Tester {
fun eqtest1() {
let x: u64;
let r: &mut u64;

x = 0;
r = &mut x;
_ = freeze(copy r) == freeze(copy r);
}

fun eqtest2() {
let x: u64;
let r: &mut u64;

x = 0;
r = &mut x;
_ = freeze(copy r) == freeze(move r);
}

fun neqtest1() {
let x: u64;
let r: &mut u64;

x = 0;
r = &mut x;
_ = freeze(copy r) != freeze(copy r);
}

fun neqtest2() {
let x: u64;
let r: &mut u64;

x = 0;
r = &mut x;
_ = freeze(copy r) != freeze(move r);
}
}
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,41 @@

Diagnostics:
error: mutable reference in local `r` requires exclusive access but is borrowed
┌─ tests/reference-safety/v1-borrow-tests/eq_ok.move:8:38
8 │ _ = freeze(copy r) == freeze(copy r);
│ -------------------------^^^^^^-
│ │ │
│ │ requirement enforced here
│ conflicting reference used here
│ previous freeze

error: mutable reference in local `r` requires exclusive access but is borrowed
┌─ tests/reference-safety/v1-borrow-tests/eq_ok.move:17:38
17 │ _ = freeze(copy r) == freeze(move r);
│ -------------------------^^^^^^-
│ │ │
│ │ requirement enforced here
│ conflicting reference used here
│ previous freeze

error: mutable reference in local `r` requires exclusive access but is borrowed
┌─ tests/reference-safety/v1-borrow-tests/eq_ok.move:26:38
26 │ _ = freeze(copy r) != freeze(copy r);
│ -------------------------^^^^^^-
│ │ │
│ │ requirement enforced here
│ conflicting reference used here
│ previous freeze

error: mutable reference in local `r` requires exclusive access but is borrowed
┌─ tests/reference-safety/v1-borrow-tests/eq_ok.move:35:38
35 │ _ = freeze(copy r) != freeze(move r);
│ -------------------------^^^^^^-
│ │ │
│ │ requirement enforced here
│ conflicting reference used here
│ previous freeze
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,45 @@
module 0x8675309::M {
struct S { g: u64 }

fun t1(root: &mut S, cond: bool) {
let x1 = 0;
let eps = if (cond) bar(root) else &x1;
let g = &root.g;
eps;
g;
eps;
}

fun t2() {
let x1 = 0;
let x2 = 1;
let eps = foo(&x1, &x2);
baz(&x1, eps);
}

fun t3() {
let x1 = 0;
let x2 = 1;
let eps = foo(&x1, &x2);
baz(freeze(&mut x1), eps);
}

fun foo(a: &u64, b: &u64): &u64 {
let ret;
if (*a > *b) {
ret = move a;
move b;
} else {
ret = move b;
move a;
};
ret
}

fun bar(a: &mut S): &u64 {
&a.g
}

fun baz(_a: &u64, _b: &u64) {
}
}
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,15 @@

Diagnostics:
error: cannot mutably borrow since immutable references exist
┌─ tests/reference-safety/v1-borrow-tests/factor_valid_2.move:24:20
23 │ let eps = foo(&x1, &x2);
│ -------------
│ │ │
│ │ previous local borrow
│ used by call result
24 │ baz(freeze(&mut x1), eps);
│ -----------^^^^^^^-------
│ │ │
│ │ mutable borrow attempted here
│ requirement enforced here
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,38 @@
module 0x8675309::Tester {
use std::signer;

struct Data has key { v1: u64, v2: u64 }
struct Box has key { f: u64 }

// the resource struct is here to just give a feeling why the computation might not be reorderable
fun bump_and_pick(account: &signer, b1: &mut Box, b2: &mut Box): &u64 acquires Data {
let sender = signer::address_of(account);
let data = borrow_global_mut<Data>(sender);
b1.f = data.v1;
b2.f = data.v2;
if (b1.f > b2.f) &b1.f else &b2.f
}

fun larger_field(account: &signer, drop: address, result: &mut u64) acquires Box, Data {
let sender = signer::address_of(account);
let b1 = move_from<Box>(sender);
let b2 = move_from<Box>(drop);

assert!(b1.f == 0, 42);
assert!(b2.f == 0, 42);

let returned_ref = bump_and_pick(account, &mut b1, &mut b2);

// imagine some more interesting check than these asserts
assert!(b1.f != 0, 42);
assert!(b2.f != 0, 42);
assert!(
(returned_ref == &(&mut b1).f) != (returned_ref == &(&mut b2).f),
42
);

*result = *returned_ref;
move_to<Box>(account, b1);
Box { f: _ } = b2;
}
}
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,37 @@

Diagnostics:
error: cannot immutably borrow since mutable references exist
┌─ tests/reference-safety/v1-borrow-tests/imm_borrow_loc_valid.move:27:17
24 │ let returned_ref = bump_and_pick(account, &mut b1, &mut b2);
│ ----------------------------------------
│ │ │
│ │ previous mutable local borrow
│ used by call result
·
27 │ assert!(b1.f != 0, 42);
│ ^^--
│ │
│ requirement enforced here
│ immutable borrow attempted here
·
30 │ (returned_ref == &(&mut b1).f) != (returned_ref == &(&mut b2).f),
│ ------------------------------ conflicting reference `returned_ref` used here

error: cannot immutably borrow since mutable references exist
┌─ tests/reference-safety/v1-borrow-tests/imm_borrow_loc_valid.move:28:17
24 │ let returned_ref = bump_and_pick(account, &mut b1, &mut b2);
│ ----------------------------------------
│ │ │
│ │ previous mutable local borrow
│ used by call result
·
28 │ assert!(b2.f != 0, 42);
│ ^^--
│ │
│ requirement enforced here
│ immutable borrow attempted here
29 │ assert!(
30 │ (returned_ref == &(&mut b1).f) != (returned_ref == &(&mut b2).f),
│ ------------------------------ conflicting reference `returned_ref` used here
Loading

0 comments on commit 6957ff6

Please sign in to comment.