Skip to content

Commit

Permalink
Refactor the verifier and add more mvir tests. (#1742)
Browse files Browse the repository at this point in the history
  • Loading branch information
steelgeek091 authored May 26, 2024
1 parent 89e35df commit 7a85750
Show file tree
Hide file tree
Showing 26 changed files with 309 additions and 49 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
processed 1 task

task 0 'publish'. lines 1-11:
status ABORTED with code 10013 in 0000000000000000000000000000000000000000000000000000000000000002::move_module
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
//# publish
module 0x1.TestModule1 {
// error code 10013: INVALID_DATA_STRUCT_WITHOUT_COPY_ABILITY
struct S0 has drop {v: u64}

metadata {
data_struct {
0x1::TestModule1::S0 -> true;
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
processed 1 task

task 0 'publish'. lines 1-11:
status ABORTED with code 10012 in 0000000000000000000000000000000000000000000000000000000000000002::move_module
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
//# publish
module 0x1.TestModule1 {
// error code 10012: INVALID_DATA_STRUCT_WITHOUT_DROP_ABILITY
struct S0 has copy {v: u64}

metadata {
data_struct {
0x1::TestModule1::S0 -> true;
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
//# publish
module 0x1.TestModule1 {
metadata {
data_struct {
// error code 10010: INVALID_MODULE_OWNER
0x123::SomeModule::Struct0 -> true;
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
processed 1 task

task 0 'publish'. lines 1-11:
status ABORTED with code 10002 in 0000000000000000000000000000000000000000000000000000000000000002::move_module
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
//# publish
module 0x1.TestModule1 {
struct S0 has drop { x: u64 }

metadata {
data_struct {
// error code 10002: STRUCT_NOT_EXISTS
0x1::TestModule1::S1 -> true;
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
processed 1 task

task 0 'publish'. lines 1-9:
status ABORTED with code 10010 in 0000000000000000000000000000000000000000000000000000000000000002::move_module
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module 0x1.TestModule1 {
metadata {
private_generics {
// error code 10010: INVALID_MODULE_OWNER
0x123::SomeModule::f1 -> true;
0x123::SomeModule::f1 -> [0, 1];
}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
processed 1 task

task 0 'publish'. lines 1-26:
status ABORTED with code 10011 in 0000000000000000000000000000000000000000000000000000000000000002::move_module
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
//# publish
module 0x1.TestModule1 {
metadata {
private_generics {
0x1::TestModule1::f1 -> [0, 1];
}
}

public f1<T1: copy+drop, T2: copy+drop>(arg1: T1, arg2: T1) {
label b0:
_ = move(arg1);
_ = move(arg2);
return;
}

public f2() {
let a1: u32;
let a2: u32;
label b0:
a1 = 123u32;
a2 = 456u32;
// error code 10011: INVALID_PRIVATE_GENERICS_TYPE
Self.f1<u32, u32>(copy(a1), copy(a2));
return;
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,4 @@ task 0 'publish'. lines 1-8:
status EXECUTED

task 1 'publish'. lines 10-36:
status ABORTED with code 10008 in 0000000000000000000000000000000000000000000000000000000000000002::move_module
status ABORTED with code 10011 in 0000000000000000000000000000000000000000000000000000000000000002::move_module
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ module 0x1.TestModule1 {
label b0:
s0 = TestModule0.new();
s1 = TestModule0.new();
// error code 10008: INVALID_DATA_STRUCT
// error code 10011: INVALID_PRIVATE_GENERICS_TYPE
Self.f1<TestModule0.S0, TestModule0.S0>(move(s0), move(s1));
return;
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
processed 2 tasks

task 0 'publish'. lines 1-8:
status EXECUTED

task 1 'publish'. lines 10-36:
status ABORTED with code 10004 in 0000000000000000000000000000000000000000000000000000000000000002::move_module
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
//# publish
module 0x1.TestModule0 {
struct S0 has drop { x: u64 }
public new(): Self.S0 {
label b0:
return S0{ x: 123 };
}
}

//# publish
module 0x1.TestModule1 {
import 0x1.TestModule0;
metadata {
private_generics {
// error code 10004: TOO_MANY_PARAMETERS
0x1::TestModule1::f1 -> [1, 1, 1, 1, 1, 1];
}
}

public f1<T1: drop, T2: drop>(arg1: T1, arg2: T2) {
label b0:
_ = move(arg1);
_ = move(arg2);
return;
}

public f2() {
let s0: TestModule0.S0;
let s1: TestModule0.S0;
label b0:
s0 = TestModule0.new();
s1 = TestModule0.new();
Self.f1<TestModule0.S0, TestModule0.S0>(move(s0), move(s1));
return;
}
}
3 changes: 3 additions & 0 deletions moveos/moveos-verifier/src/error_code.rs
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,9 @@ pub enum ErrorCode {
INVALID_DATA_STRUCT = 10008,
INVALID_DATA_STRUCT_TYPE = 10009,
INVALID_MODULE_OWNER = 10010,
INVALID_PRIVATE_GENERICS_TYPE = 10011,
INVALID_DATA_STRUCT_WITHOUT_DROP_ABILITY = 10012,
INVALID_DATA_STRUCT_WITHOUT_COPY_ABILITY = 10013,

INVALID_ENTRY_FUNC_SIGNATURE = 11000,
INVALID_PARAM_TYPE_ENTRY_FUNCTION = 11001,
Expand Down
Loading

0 comments on commit 7a85750

Please sign in to comment.