forked from MystenLabs/sui
-
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.
[verifier] Migrate global_storage_access tests (MystenLabs#2017)
- Migrated global_storage_access Rust tests to expected output tests
- Loading branch information
Showing
13 changed files
with
214 additions
and
44 deletions.
There are no files selected for viewing
4 changes: 4 additions & 0 deletions
4
.../sui-verifier-transactional-tests/transactional-tests/tests/global_storage_access/all.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,4 @@ | ||
processed 1 task | ||
|
||
task 0 'publish'. lines 4-31: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [Exists(StructDefinitionIndex(0)), ExistsGeneric(StructDefInstantiationIndex(0)), ImmBorrowGlobal(StructDefinitionIndex(0)), ImmBorrowGlobalGeneric(StructDefInstantiationIndex(0)), MutBorrowGlobal(StructDefinitionIndex(0)), MutBorrowGlobalGeneric(StructDefInstantiationIndex(0)), MoveFrom(StructDefinitionIndex(0)), MoveFromGeneric(StructDefInstantiationIndex(0)), MoveTo(StructDefinitionIndex(0)), MoveToGeneric(StructDefInstantiationIndex(0))]". |
31 changes: 31 additions & 0 deletions
31
...sui-verifier-transactional-tests/transactional-tests/tests/global_storage_access/all.mvir
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,31 @@ | ||
// Copyright (c) 2022, Mysten Labs, Inc. | ||
// SPDX-License-Identifier: Apache-2.0 | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R has key { id: ID.VersionedID } | ||
struct G<phantom T> has key { id: ID.VersionedID } | ||
|
||
|
||
no<T>(s: &signer, addr: address, r: Self.R, g: Self.G<T>) acquires R, G { | ||
label l0: | ||
_ = exists<R>(copy(addr)); | ||
_ = exists<G<T>>(copy(addr)); | ||
_ = borrow_global<R>(copy(addr)); | ||
_ = borrow_global<G<T>>(copy(addr)); | ||
_ = borrow_global_mut<R>(copy(addr)); | ||
_ = borrow_global_mut<G<T>>(copy(addr)); | ||
Self.consume<Self.R>(move_from<R>(copy(addr))); | ||
Self.consume<Self.G<T>>(move_from<G<T>>(copy(addr))); | ||
move_to<R>(copy(s), move(r)); | ||
move_to<G<T>>(copy(s), move(g)); | ||
return; | ||
} | ||
|
||
consume<T>(t: T) { | ||
label l0: | ||
abort 0; | ||
} | ||
|
||
} |
7 changes: 7 additions & 0 deletions
7
...ier-transactional-tests/transactional-tests/tests/global_storage_access/borrow_global.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,7 @@ | ||
processed 2 tasks | ||
|
||
task 0 'publish'. lines 4-15: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [ImmBorrowGlobal(StructDefinitionIndex(0))]". | ||
|
||
task 1 'publish'. lines 17-27: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [ImmBorrowGlobalGeneric(StructDefInstantiationIndex(0))]". |
27 changes: 27 additions & 0 deletions
27
...er-transactional-tests/transactional-tests/tests/global_storage_access/borrow_global.mvir
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,27 @@ | ||
// Copyright (c) 2022, Mysten Labs, Inc. | ||
// SPDX-License-Identifier: Apache-2.0 | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R has key { id: ID.VersionedID } | ||
|
||
no(addr: address) acquires R { | ||
label l0: | ||
_ = borrow_global<R>(move(addr)); | ||
return; | ||
} | ||
|
||
} | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R<phantom T> has key { id: ID.VersionedID } | ||
|
||
no<T>(addr: address) acquires R { | ||
label l0: | ||
_ = borrow_global<R<T>>(move(addr)); | ||
return; | ||
} | ||
} |
7 changes: 7 additions & 0 deletions
7
...transactional-tests/transactional-tests/tests/global_storage_access/borrow_global_mut.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,7 @@ | ||
processed 2 tasks | ||
|
||
task 0 'publish'. lines 4-15: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [MutBorrowGlobal(StructDefinitionIndex(0))]". | ||
|
||
task 1 'publish'. lines 17-27: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [MutBorrowGlobalGeneric(StructDefInstantiationIndex(0))]". |
27 changes: 27 additions & 0 deletions
27
...ransactional-tests/transactional-tests/tests/global_storage_access/borrow_global_mut.mvir
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,27 @@ | ||
// Copyright (c) 2022, Mysten Labs, Inc. | ||
// SPDX-License-Identifier: Apache-2.0 | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R has key { id: ID.VersionedID } | ||
|
||
no(addr: address) acquires R { | ||
label l0: | ||
_ = borrow_global_mut<R>(move(addr)); | ||
return; | ||
} | ||
|
||
} | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R<phantom T> has key { id: ID.VersionedID } | ||
|
||
no<T>(addr: address) acquires R { | ||
label l0: | ||
_ = borrow_global_mut<R<T>>(move(addr)); | ||
return; | ||
} | ||
} |
7 changes: 7 additions & 0 deletions
7
...i-verifier-transactional-tests/transactional-tests/tests/global_storage_access/exists.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,7 @@ | ||
processed 2 tasks | ||
|
||
task 0 'publish'. lines 4-14: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [Exists(StructDefinitionIndex(0))]". | ||
|
||
task 1 'publish'. lines 16-25: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [ExistsGeneric(StructDefInstantiationIndex(0))]". |
25 changes: 25 additions & 0 deletions
25
...-verifier-transactional-tests/transactional-tests/tests/global_storage_access/exists.mvir
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 @@ | ||
// Copyright (c) 2022, Mysten Labs, Inc. | ||
// SPDX-License-Identifier: Apache-2.0 | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R has key { id: ID.VersionedID } | ||
|
||
no(addr: address): bool { | ||
label l0: | ||
return exists<R>(move(addr)); | ||
} | ||
|
||
} | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R<phantom T> has key { id: ID.VersionedID } | ||
|
||
no<T>(addr: address): bool { | ||
label l0: | ||
return exists<R<T>>(move(addr)); | ||
} | ||
} |
7 changes: 7 additions & 0 deletions
7
...erifier-transactional-tests/transactional-tests/tests/global_storage_access/move_from.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,7 @@ | ||
processed 2 tasks | ||
|
||
task 0 'publish'. lines 4-20: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [MoveFrom(StructDefinitionIndex(0))]". | ||
|
||
task 1 'publish'. lines 22-38: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [MoveFromGeneric(StructDefInstantiationIndex(0))]". |
38 changes: 38 additions & 0 deletions
38
...rifier-transactional-tests/transactional-tests/tests/global_storage_access/move_from.mvir
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,38 @@ | ||
// Copyright (c) 2022, Mysten Labs, Inc. | ||
// SPDX-License-Identifier: Apache-2.0 | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R has key { id: ID.VersionedID } | ||
|
||
no(addr: address) acquires R { | ||
label l0: | ||
Self.consume<Self.R>(move_from<R>(move(addr))); | ||
return; | ||
} | ||
|
||
consume<T>(t: T) { | ||
label l0: | ||
abort 0; | ||
} | ||
|
||
} | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R<phantom T> has key { id: ID.VersionedID } | ||
|
||
no<T>(addr: address) acquires R { | ||
label l0: | ||
Self.consume<Self.R<T>>(move_from<R<T>>(move(addr))); | ||
return; | ||
} | ||
|
||
consume<T>(t: T) { | ||
label l0: | ||
abort 0; | ||
} | ||
|
||
} |
7 changes: 7 additions & 0 deletions
7
...-verifier-transactional-tests/transactional-tests/tests/global_storage_access/move_to.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,7 @@ | ||
processed 2 tasks | ||
|
||
task 0 'publish'. lines 4-15: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [MoveTo(StructDefinitionIndex(0))]". | ||
|
||
task 1 'publish'. lines 17-27: | ||
Error: Failed to verify the Move module, reason: "Access to Move global storage is not allowed. Found in function no: [MoveToGeneric(StructDefInstantiationIndex(0))]". |
27 changes: 27 additions & 0 deletions
27
...verifier-transactional-tests/transactional-tests/tests/global_storage_access/move_to.mvir
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,27 @@ | ||
// Copyright (c) 2022, Mysten Labs, Inc. | ||
// SPDX-License-Identifier: Apache-2.0 | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R has key { id: ID.VersionedID } | ||
|
||
no(s: &signer, r: Self.R) { | ||
label l0: | ||
move_to<R>(copy(s), move(r)); | ||
abort 0; | ||
} | ||
|
||
} | ||
|
||
//# publish | ||
module 0x0.M { | ||
import 0x2.ID; | ||
struct R<phantom T> has key { id: ID.VersionedID } | ||
|
||
no<T>(s: &signer, r: Self.R<T>) { | ||
label l0: | ||
move_to<R<T>>(copy(s), move(r)); | ||
abort 0; | ||
} | ||
} |
44 changes: 0 additions & 44 deletions
44
crates/sui-verifier/tests/global_storage_access_verification_tests.rs
This file was deleted.
Oops, something went wrong.