Skip to content

Commit

Permalink
[sui-verifier] Added support for characteristic types (MystenLabs#3563)
Browse files Browse the repository at this point in the history
* [sui-verifier] Added support for characteristic types

* Fixed a problem related to another struct being defined

* Adjusted tests and examples to work with the new verifier pass

* Fixed another problem plus adjusted more test outputs

* Another bug fix

* Yet another fix

* Addressed review comments

* Addressed more review comments

* Addressed even more review comments
  • Loading branch information
awelc authored Aug 2, 2022
1 parent 4b5ee7d commit 7942def
Show file tree
Hide file tree
Showing 39 changed files with 638 additions and 130 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ written: object(109), object(110)

task 6 'run'. lines 89-89:
Error: Transaction Effects Status: Invalid Shared Child Object Usage. When a child object (either direct or indirect) of a shared object is passed by-value to an entry function, either the child object's type or the shared object's type must be defined in the same module as the called function. This is violated by object fake(109), whose ancestor fake(111) is a shared object, and neither are defined in this module..
Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: InvalidSharedChildUse(InvalidSharedChildUse { child: fake(109), ancestor: fake(111) }), source: Some("When a child object (either direct or indirect) of a shared object is passed by-value to an entry function, either the child object's type or the shared object's type must be defined in the same module as the called function. This is violated by object fake(109) (defined in module 'T3::O3'), whose ancestor fake(111) is a shared object (defined in module 'T2::O2'), and neither are defined in this module 'T1::O1'") } }
Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: InvalidSharedChildUse(InvalidSharedChildUse { child: fake(109), ancestor: fake(111) }), source: Some("When a child object (either direct or indirect) of a shared object is passed by-value to an entry function, either the child object's type or the shared object's type must be defined in the same module as the called function. This is violated by object fake(109) (defined in module 't3::o3'), whose ancestor fake(111) is a shared object (defined in module 't2::o2'), and neither are defined in this module 't1::o1'") } }

task 7 'run'. lines 91-91:
written: object(109), object(111), object(113)
Original file line number Diff line number Diff line change
@@ -1,91 +1,91 @@
// Copyright (c) 2022, Mysten Labs, Inc.
// SPDX-License-Identifier: Apache-2.0

//# init --addresses T1=0x0 T2=0x0 T3=0x0 A=0x42
//# init --addresses t1=0x0 t2=0x0 t3=0x0 A=0x42

//# publish

module T3::O3 {
module t3::o3 {
use sui::object::{Self, Info};
use sui::transfer;
use sui::tx_context::{Self, TxContext};

struct O3 has key, store {
struct Obj3 has key, store {
info: Info,
}

public entry fun create(ctx: &mut TxContext) {
let o = O3 { info: object::new(ctx) };
let o = Obj3 { info: object::new(ctx) };
transfer::transfer(o, tx_context::sender(ctx))
}
}

//# publish

module T2::O2 {
module t2::o2 {
use sui::object::{Self, Info};
use sui::transfer;
use sui::tx_context::{Self, TxContext};
use T3::O3::O3;
use t3::o3::Obj3;

struct O2 has key, store {
struct Obj2 has key, store {
info: Info,
}

public entry fun create_shared(child: O3, ctx: &mut TxContext) {
public entry fun create_shared(child: Obj3, ctx: &mut TxContext) {
transfer::share_object(new(child, ctx))
}

public entry fun create_owned(child: O3, ctx: &mut TxContext) {
public entry fun create_owned(child: Obj3, ctx: &mut TxContext) {
transfer::transfer(new(child, ctx), tx_context::sender(ctx))
}

public entry fun use_o2_o3(_o2: &mut O2, o3: O3, ctx: &mut TxContext) {
public entry fun use_o2_o3(_o2: &mut Obj2, o3: Obj3, ctx: &mut TxContext) {
transfer::transfer(o3, tx_context::sender(ctx))
}

fun new(child: O3, ctx: &mut TxContext): O2 {
fun new(child: Obj3, ctx: &mut TxContext): Obj2 {
let info = object::new(ctx);
transfer::transfer_to_object_id(child, &info);
O2 { info }
Obj2 { info }
}
}


//# publish

module T1::O1 {
module t1::o1 {
use sui::object::{Self, Info};
use sui::transfer;
use sui::tx_context::{Self, TxContext};
use T2::O2::O2;
use T3::O3::O3;
use t2::o2::Obj2;
use t3::o3::Obj3;

struct O1 has key {
struct Obj1 has key {
info: Info,
}

public entry fun create_shared(child: O2, ctx: &mut TxContext) {
public entry fun create_shared(child: Obj2, ctx: &mut TxContext) {
transfer::share_object(new(child, ctx))
}

// This function will be invalid if _o2 is a shared object and owns _o3.
public entry fun use_o2_o3(_o2: &mut O2, o3: O3, ctx: &mut TxContext) {
public entry fun use_o2_o3(_o2: &mut Obj2, o3: Obj3, ctx: &mut TxContext) {
transfer::transfer(o3, tx_context::sender(ctx))
}

fun new(child: O2, ctx: &mut TxContext): O1 {
fun new(child: Obj2, ctx: &mut TxContext): Obj1 {
let info = object::new(ctx);
transfer::transfer_to_object_id(child, &info);
O1 { info }
Obj1 { info }
}
}

//# run T3::O3::create
//# run t3::o3::create

//# run T2::O2::create_shared --args object(109)
//# run t2::o2::create_shared --args object(109)

// This run should error as O2/O3 were not defined in O1
//# run T1::O1::use_o2_o3 --args object(111) object(109)
// This run should error as Obj2/Obj3 were not defined in o1
//# run t1::o1::use_o2_o3 --args object(111) object(109)

//# run T2::O2::use_o2_o3 --args object(111) object(109)
//# run t2::o2::use_o2_o3 --args object(111) object(109)
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,4 @@ processed 2 tasks

task 1 'publish'. lines 5-24:
Error: Transaction Effects Status: Sui Move Bytecode Verification Error. Please run the Sui Move Verifier for more information.
Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: SuiMoveVerificationError, source: Some("Expected exactly one parameter for _::M1::init of type &mut sui::tx_context::TxContext") } }
Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: SuiMoveVerificationError, source: Some("Expected last parameter for _::M1::init to be &mut sui::tx_context::TxContext, but found &mut sui::tx_context::TxContext") } }
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ written: object(106)

task 4 'view-object'. lines 43-43:
Owner: Shared
Contents: t2::o2::O2 {info: sui::object::Info {id: sui::object::ID {bytes: fake(107)}, version: 1u64}}
Contents: t2::o2::Obj2 {info: sui::object::Info {id: sui::object::ID {bytes: fake(107)}, version: 1u64}}

task 5 'run'. lines 45-45:
Error: Transaction Effects Status: Entry Argument Type Error. Error for argument at index 0: Immutable and shared objects cannot be passed by-value.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,27 +12,27 @@ module t2::o2 {
use sui::transfer;
use sui::tx_context::TxContext;

struct O2 has key, store {
struct Obj2 has key, store {
info: Info,
}

public entry fun create(ctx: &mut TxContext) {
let o = O2 { info: object::new(ctx) };
let o = Obj2 { info: object::new(ctx) };
transfer::share_object(o)
}

public entry fun consume_o2(o2: O2) {
let O2 { info } = o2;
public entry fun consume_o2(o2: Obj2) {
let Obj2 { info } = o2;
object::delete(info);
}
}

//# publish

module t1::o1 {
use t2::o2::{Self, O2};
use t2::o2::{Self, Obj2};

public entry fun consume_o2(o2: O2) {
public entry fun consume_o2(o2: Obj2) {
o2::consume_o2(o2);
}
}
Expand Down
37 changes: 26 additions & 11 deletions crates/sui-adapter/src/adapter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,8 +37,8 @@ use sui_types::{
SUI_SYSTEM_STATE_OBJECT_ID,
};
use sui_verifier::{
entry_points_verifier::{is_tx_context, INIT_FN_NAME, RESOLVED_STD_OPTION, RESOLVED_SUI_ID},
verifier,
entry_points_verifier::{is_tx_context, RESOLVED_STD_OPTION, RESOLVED_SUI_ID},
verifier, INIT_FN_NAME,
};

use crate::bytecode_rewriter::ModuleHandleRewriter;
Expand Down Expand Up @@ -264,12 +264,17 @@ pub fn store_package_and_init_modules<
let modules_to_init = modules
.iter()
.filter_map(|module| {
module.function_defs.iter().find(|fdef| {
let fhandle = module.function_handle_at(fdef.function).name;
let fname = module.identifier_at(fhandle);
fname == INIT_FN_NAME
})?;
Some(module.self_id())
for fdef in &module.function_defs {
let fhandle = module.function_handle_at(fdef.function);
let fname = module.identifier_at(fhandle.name);
if fname == INIT_FN_NAME {
return Some((
module.self_id(),
module.signature_at(fhandle.parameters).len(),
));
}
}
None
})
.collect();

Expand All @@ -286,13 +291,23 @@ pub fn store_package_and_init_modules<
fn init_modules<E: Debug, S: ResourceResolver<Error = E> + ModuleResolver<Error = E> + Storage>(
state_view: &mut S,
vm: &MoveVM,
module_ids_to_init: Vec<ModuleId>,
module_ids_to_init: Vec<(ModuleId, usize)>,
ctx: &mut TxContext,
gas_status: &mut SuiGasStatus,
) -> Result<(), ExecutionError> {
let init_ident = Identifier::new(INIT_FN_NAME.as_str()).unwrap();
for module_id in module_ids_to_init {
let args = vec![ctx.to_vec()];
for (module_id, num_args) in module_ids_to_init {
let mut args = vec![];
// an init function can have one or two arguments, with the last one always being of type
// &mut TxContext and the additional (first) one representing a characteristic type (see
// char_type verfier pass for additional explanation)
if num_args == 2 {
// characteristic type is a struct with a single bool filed which in bcs is encoded as
// 0x01
let bcs_char_type_value = vec![0x01];
args.push(bcs_char_type_value);
}
args.push(ctx.to_vec());
let has_ctx_arg = true;

execute_internal(
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
processed 2 tasks

task 1 'publish'. lines 8-15:
created: object(103)
written: object(102)
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// Copyright (c) 2022, Mysten Labs, Inc.
// SPDX-License-Identifier: Apache-2.0

// correct, bool field specified at source level

//# init --addresses test=0x0

//# publish
module test::m {

struct M has drop { some_field: bool }

fun init(_: M, _ctx: &mut sui::tx_context::TxContext) {
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
processed 2 tasks

task 1 'publish'. lines 8-20:
Error: Transaction Effects Status: Sui Move Bytecode Verification Error. Please run the Sui Move Verifier for more information.
Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: SuiMoveVerificationError, source: Some("characteristic type _::m::M is instantiated in the _::m::pack function and must never be") } }
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
// Copyright (c) 2022, Mysten Labs, Inc.
// SPDX-License-Identifier: Apache-2.0

// invalid, struct type incorrectly instantiated

//# init --addresses test=0x0

//# publish
module test::m {

struct M has drop { }

fun init(_: M, _ctx: &mut sui::tx_context::TxContext) {
}


fun pack(): M {
M {}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
processed 2 tasks

task 1 'publish'. lines 8-20:
Error: Transaction Effects Status: Sui Move Bytecode Verification Error. Please run the Sui Move Verifier for more information.
Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: SuiMoveVerificationError, source: Some("characteristic type candidate _::m::M must have a single ability: drop") } }
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
// Copyright (c) 2022, Mysten Labs, Inc.
// SPDX-License-Identifier: Apache-2.0

// invalid, struct type has abilities beyond drop

//# init --addresses test=0x0

//# publish
module test::m {

struct M has drop, copy { }

fun init(_: M, _ctx: &mut sui::tx_context::TxContext) {
}


fun pack(): M {
M {}
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
processed 2 tasks

task 1 'publish'. lines 8-16:
Error: Transaction Effects Status: Sui Move Bytecode Verification Error. Please run the Sui Move Verifier for more information.
Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: SuiMoveVerificationError, source: Some("characteristic type candidate _::m::M must have a single ability: drop") } }
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
// Copyright (c) 2022, Mysten Labs, Inc.
// SPDX-License-Identifier: Apache-2.0

// invalid, char type has no drop ability

//# init --addresses test=0x0

//# publish
module test::m {

struct M { }

fun init(t: M, _: &mut sui::tx_context::TxContext) {
let M { } = t;
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
processed 2 tasks

task 1 'publish'. lines 8-15:
created: object(103)
written: object(102)
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// Copyright (c) 2022, Mysten Labs, Inc.
// SPDX-License-Identifier: Apache-2.0

// correct, no field specified at source level

//# init --addresses test=0x0

//# publish
module test::m {

struct M has drop { }

fun init(_: M, _ctx: &mut sui::tx_context::TxContext) {
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
processed 2 tasks

task 1 'publish'. lines 8-15:
Error: Transaction Effects Status: Sui Move Bytecode Verification Error. Please run the Sui Move Verifier for more information.
Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: SuiMoveVerificationError, source: Some("init function of a module containing characteristic type candidate must have _::m::M as the first parameter") } }
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// Copyright (c) 2022, Mysten Labs, Inc.
// SPDX-License-Identifier: Apache-2.0

// invalid, no char type parameter in init

//# init --addresses test=0x0

//# publish
module test::m {

struct M has drop { value: bool }

fun init(_: &mut sui::tx_context::TxContext) {
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
processed 3 tasks

task 1 'publish'. lines 8-12:
created: object(103)
written: object(102)

task 2 'publish'. lines 14-19:
Error: Transaction Effects Status: Sui Move Bytecode Verification Error. Please run the Sui Move Verifier for more information.
Execution Error: ExecutionError: ExecutionError { inner: ExecutionErrorInner { kind: SuiMoveVerificationError, source: Some("Expected exactly one parameter for _::n::init of type &mut sui::tx_context::TxContext") } }
Loading

0 comments on commit 7942def

Please sign in to comment.