From 7ad3d5121a72b931024612614114282362a4a7c5 Mon Sep 17 00:00:00 2001 From: Teng Zhang Date: Fri, 21 Jun 2024 17:18:06 -0700 Subject: [PATCH] temp --- .../move-command-line-common/src/address.rs | 4 - .../tests/ability-check/index_ability_err.exp | 7 + .../ability-check/index_ability_err.move | 15 + .../ability-check/index_ability_err_2.exp | 7 + .../ability-check/index_ability_err_2.move | 12 + .../tests/checking-lang-v1/index.exp | 91 ++++++ .../tests/checking-lang-v1}/index.move | 27 +- .../tests/checking/typing/index_err.exp | 20 +- .../tests/checking/typing/index_err.move | 6 +- .../tests/checking/typing/index_err_2.exp | 4 +- .../index_acquires_err.exp | 28 ++ .../index_acquires_err.move | 23 ++ .../index_acquires_err.opt.exp | 28 ++ .../tests/no-v1-comparison/index.exp | 2 +- .../tests/no-v1-comparison/index.move | 134 ++++++++- .../move/move-compiler/src/expansion/ast.rs | 6 +- .../move-compiler/src/expansion/translate.rs | 209 ++------------ .../move/move-compiler/src/parser/ast.rs | 12 - .../parser/spec_parsing_index_fail.exp | 4 +- .../move_check/v2-not-supported/index.exp | 102 ------- third_party/move/move-model/src/ast.rs | 4 + .../move-model/src/builder/exp_builder.rs | 269 +++++++++++++++++- .../sources/functional/resource_index.exp | 12 - .../move/move-prover/tests/testsuite.rs | 3 + 24 files changed, 653 insertions(+), 376 deletions(-) create mode 100644 third_party/move/move-compiler-v2/tests/ability-check/index_ability_err.exp create mode 100644 third_party/move/move-compiler-v2/tests/ability-check/index_ability_err.move create mode 100644 third_party/move/move-compiler-v2/tests/ability-check/index_ability_err_2.exp create mode 100644 third_party/move/move-compiler-v2/tests/ability-check/index_ability_err_2.move create mode 100644 third_party/move/move-compiler-v2/tests/checking-lang-v1/index.exp rename third_party/move/{move-compiler/tests/move_check/v2-not-supported => move-compiler-v2/tests/checking-lang-v1}/index.move (68%) create mode 100644 third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.exp create mode 100644 third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.move create mode 100644 third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.opt.exp delete mode 100644 third_party/move/move-compiler/tests/move_check/v2-not-supported/index.exp delete mode 100644 third_party/move/move-prover/tests/sources/functional/resource_index.exp diff --git a/third_party/move/move-command-line-common/src/address.rs b/third_party/move/move-command-line-common/src/address.rs index 11d0935ebb9a0..2121f16addbbf 100644 --- a/third_party/move/move-command-line-common/src/address.rs +++ b/third_party/move/move-command-line-common/src/address.rs @@ -49,10 +49,6 @@ impl NumericalAddress { bytes: AccountAddress::MAX_ADDRESS, format: NumberFormat::Hex, }; - pub const STD_ADDRESS: Self = NumericalAddress { - bytes: AccountAddress::ONE, - format: NumberFormat::Hex, - }; pub const fn new(bytes: [u8; AccountAddress::LENGTH], format: NumberFormat) -> Self { Self { diff --git a/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err.exp b/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err.exp new file mode 100644 index 0000000000000..f43ecc4cd3d91 --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err.exp @@ -0,0 +1,7 @@ + +Diagnostics: +error: value of type `test::Y>` does not have the `copy` ability + ┌─ tests/ability-check/index_ability_err.move:12:17 + │ +12 │ let _ = Y>[addr]; + │ ^^^^^^^^^^^^^^^^ reference content copied here diff --git a/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err.move b/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err.move new file mode 100644 index 0000000000000..b577118be038b --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err.move @@ -0,0 +1,15 @@ +module 0x42::test { + + struct X has copy, drop, store { + value: M + } + struct Y has key, drop { + field: T + } + + fun test_resource_no_copy() acquires Y { + let addr = @0x1; + let _ = Y>[addr]; + } + +} diff --git a/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err_2.exp b/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err_2.exp new file mode 100644 index 0000000000000..ab52f302465d8 --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err_2.exp @@ -0,0 +1,7 @@ + +Diagnostics: +error: resource indexing can only applied to a resource type (a struct type which has key ability) + ┌─ tests/ability-check/index_ability_err_2.move:9:17 + │ +9 │ let _ = X[addr]; + │ ^^^^^^^^^^^^^ diff --git a/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err_2.move b/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err_2.move new file mode 100644 index 0000000000000..3417377361c05 --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/ability-check/index_ability_err_2.move @@ -0,0 +1,12 @@ +module 0x42::test { + + struct X has copy, drop, store { + value: M + } + + fun test_struct_no_resource() acquires X { + let addr = @0x1; + let _ = X[addr]; + } + +} diff --git a/third_party/move/move-compiler-v2/tests/checking-lang-v1/index.exp b/third_party/move/move-compiler-v2/tests/checking-lang-v1/index.exp new file mode 100644 index 0000000000000..e09cc1425dc4e --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/checking-lang-v1/index.exp @@ -0,0 +1,91 @@ + +Diagnostics: +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:11:17 + │ +11 │ assert!((test::R[@0x1]).value == true, 0); + │ ^^^^^^^^^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:15:9 + │ +15 │ 0x42::test::R[@0x1].value = false; + │ ^^^^^^^^^^^^^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:16:17 + │ +16 │ assert!(R[@0x1].value == false, 1); + │ ^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:38:17 + │ +38 │ assert!(test::Y>[@0x1].field.value == true, 0); + │ ^^^^^^^^^^^^^^^^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:43:22 + │ +43 │ let y = &mut 0x42::test ::Y> [addr]; + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:45:17 + │ +45 │ assert!(Y>[addr].field.value == false, 1); + │ ^^^^^^^^^^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:53:17 + │ +53 │ assert!(v[0].value == 2, 0); + │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:70:17 + │ +70 │ assert!(v[0].field.value == true, 0); + │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:71:17 + │ +71 │ assert!(v[1].field.value == false, 0); + │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:88:17 + │ +88 │ assert!(v[0].field.value == true, 0); + │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:89:17 + │ +89 │ assert!(v[1].field.value == false, 0); + │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:90:9 + │ +90 │ v[0].field.value = false; + │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:91:9 + │ +91 │ v[1].field.value = true; + │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:92:17 + │ +92 │ assert!(v[0].field.value == false, 0); + │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond + +error: unsupported language construct + ┌─ tests/checking-lang-v1/index.move:93:17 + │ +93 │ assert!(v[1].field.value == true, 0); + │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond diff --git a/third_party/move/move-compiler/tests/move_check/v2-not-supported/index.move b/third_party/move/move-compiler-v2/tests/checking-lang-v1/index.move similarity index 68% rename from third_party/move/move-compiler/tests/move_check/v2-not-supported/index.move rename to third_party/move/move-compiler-v2/tests/checking-lang-v1/index.move index 6acd20cc0f940..bc24338a2b93d 100644 --- a/third_party/move/move-compiler/tests/move_check/v2-not-supported/index.move +++ b/third_party/move/move-compiler-v2/tests/checking-lang-v1/index.move @@ -8,13 +8,12 @@ module 0x42::test { fun test_resource_1() acquires R { use 0x42::test; - assert!((&test::R[@0x1]).value == true, 0); + assert!((test::R[@0x1]).value == true, 0); } fun test_resource_2() acquires R { - let x = &mut 0x42::test::R[@0x1]; - x.value = false; - assert!((&R[@0x1]).value == false, 1); + 0x42::test::R[@0x1].value = false; + assert!(R[@0x1].value == false, 1); } struct X has copy, drop, store { @@ -36,14 +35,14 @@ module 0x42::test { fun test_resource_3() { use 0x42::test; - assert!((&test::Y>[@0x1]).field.value == true, 0); + assert!(test::Y>[@0x1].field.value == true, 0); } fun test_resource_4() { let addr = @0x1; let y = &mut 0x42::test ::Y> [addr]; y.field.value = false; - assert!((&Y>[addr]) .field.value == false, 1); + assert!(Y>[addr].field.value == false, 1); } fun test_vector() { @@ -68,8 +67,8 @@ module 0x42::test { field: x2 }; let v = vector[y1, y2]; - assert!((&v[0]).field.value == true, 0); - assert!((&v[1]).field.value == false, 0); + assert!(v[0].field.value == true, 0); + assert!(v[1].field.value == false, 0); } fun test_vector_borrow_mut() { @@ -86,12 +85,12 @@ module 0x42::test { field: x2 }; let v = vector[y1, y2]; - assert!((&v[0]).field.value == true, 0); - assert!((&v[1]).field.value == false, 0); - (&mut v[0]).field.value = false; - (&mut v[1]).field.value = true; - assert!((&v[0]).field.value == false, 0); - assert!((&v[1]).field.value == true, 0); + assert!(v[0].field.value == true, 0); + assert!(v[1].field.value == false, 0); + v[0].field.value = false; + v[1].field.value = true; + assert!(v[0].field.value == false, 0); + assert!(v[1].field.value == true, 0); } diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/index_err.exp b/third_party/move/move-compiler-v2/tests/checking/typing/index_err.exp index 3705aa028cd09..b29b7bc9f3cd3 100644 --- a/third_party/move/move-compiler-v2/tests/checking/typing/index_err.exp +++ b/third_party/move/move-compiler-v2/tests/checking/typing/index_err.exp @@ -1,19 +1,13 @@ Diagnostics: -error: unexpected token - ┌─ tests/checking/typing/index_err.move:10:17 - │ -10 │ assert!((test::R[@0x1]).value == true, 0); - │ ^^^^^^^^^^^^^^^ resource indexing using `_[_]` needs to be paired with `&` or `&mut` - -error: unexpected token +error: indexing can only be applied to a vector or a resource type (a struct type which has key ability) ┌─ tests/checking/typing/index_err.move:14:9 │ -14 │ Test[@0x1]; - │ ^^^^^^^^^^ index notation `_[_]` expects a resource or vector +14 │ UNUSED_Test[@0x1]; + │ ^^^^^^^^^^^^^^^^^ -error: unexpected token - ┌─ tests/checking/typing/index_err.move:19:10 +error: indexing can only be applied to a vector or a resource type (a struct type which has key ability) + ┌─ tests/checking/typing/index_err.move:19:9 │ -19 │ &test::Test[@0x1]; - │ ^^^^^^^^^^^^^^^^ index notation `_[_]` expects a resource or vector +19 │ &test::UNUSED_Test[@0x1]; + │ ^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/index_err.move b/third_party/move/move-compiler-v2/tests/checking/typing/index_err.move index 18da37683e07f..1208c0c44334b 100644 --- a/third_party/move/move-compiler-v2/tests/checking/typing/index_err.move +++ b/third_party/move/move-compiler-v2/tests/checking/typing/index_err.move @@ -2,7 +2,7 @@ module 0x42::test { struct R has key, drop { value: bool } - spec schema Test { + spec schema UNUSED_Test { } fun test_no_ref_for_resource() acquires R { @@ -11,12 +11,12 @@ module 0x42::test { } fun test_no_schema() { - Test[@0x1]; + UNUSED_Test[@0x1]; } fun test_no_schema_ref() { use 0x42::test; - &test::Test[@0x1]; + &test::UNUSED_Test[@0x1]; } } diff --git a/third_party/move/move-compiler-v2/tests/checking/typing/index_err_2.exp b/third_party/move/move-compiler-v2/tests/checking/typing/index_err_2.exp index d8c7ca70c1e62..fd1d47a3ccdf1 100644 --- a/third_party/move/move-compiler-v2/tests/checking/typing/index_err_2.exp +++ b/third_party/move/move-compiler-v2/tests/checking/typing/index_err_2.exp @@ -1,7 +1,7 @@ Diagnostics: -error: cannot pass `&X` to a function which expects argument of type `&vector<_>` +error: expected `vector` but found a value of type `X` ┌─ tests/checking/typing/index_err_2.move:11:17 │ 11 │ assert!(x[0].value == 2, 0); - │ ^^^^ + │ ^ diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.exp new file mode 100644 index 0000000000000..f5de8b96bbaec --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.exp @@ -0,0 +1,28 @@ + +Diagnostics: +error: Invalid operation: storage operation on type `test::Y` can only be done within the defining module `0x42::test` + ┌─ tests/file-format-generator/index_acquires_err.move:14:9 + │ +14 │ fun test_resource_other_module() acquires 0x42::test::Y { + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^ +15 │ let addr = @0x1; +16 │ assert!((&0x42::test::Y<0x42::test::X>[addr]).field.value == true, 1); + │ ------------------------------------------- called here + +error: Invalid operation: access of the field `field` on type `test::Y` can only be done within the defining module `0x42::test` + ┌─ tests/file-format-generator/index_acquires_err.move:14:9 + │ +14 │ fun test_resource_other_module() acquires 0x42::test::Y { + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^ +15 │ let addr = @0x1; +16 │ assert!((&0x42::test::Y<0x42::test::X>[addr]).field.value == true, 1); + │ ------------------------------------------------- accessed here + +error: Invalid operation: access of the field `value` on type `test::X` can only be done within the defining module `0x42::test` + ┌─ tests/file-format-generator/index_acquires_err.move:14:9 + │ +14 │ fun test_resource_other_module() acquires 0x42::test::Y { + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^ +15 │ let addr = @0x1; +16 │ assert!((&0x42::test::Y<0x42::test::X>[addr]).field.value == true, 1); + │ ------------------------------------------------------- accessed here diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.move b/third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.move new file mode 100644 index 0000000000000..432c3e211b774 --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.move @@ -0,0 +1,23 @@ +module 0x42::test { + + struct X has copy, drop, store { + value: M + } + struct Y has key, drop { + field: T + } + +} + +module 0x42::test2 { + + fun test_resource_other_module() acquires 0x42::test::Y { + let addr = @0x1; + assert!((&0x42::test::Y<0x42::test::X>[addr]).field.value == true, 1); + spec { + // This is OK + assert 0x42::test::Y<0x42::test::X>[addr].field.value == true; + } + } + +} diff --git a/third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.opt.exp b/third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.opt.exp new file mode 100644 index 0000000000000..f5de8b96bbaec --- /dev/null +++ b/third_party/move/move-compiler-v2/tests/file-format-generator/index_acquires_err.opt.exp @@ -0,0 +1,28 @@ + +Diagnostics: +error: Invalid operation: storage operation on type `test::Y` can only be done within the defining module `0x42::test` + ┌─ tests/file-format-generator/index_acquires_err.move:14:9 + │ +14 │ fun test_resource_other_module() acquires 0x42::test::Y { + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^ +15 │ let addr = @0x1; +16 │ assert!((&0x42::test::Y<0x42::test::X>[addr]).field.value == true, 1); + │ ------------------------------------------- called here + +error: Invalid operation: access of the field `field` on type `test::Y` can only be done within the defining module `0x42::test` + ┌─ tests/file-format-generator/index_acquires_err.move:14:9 + │ +14 │ fun test_resource_other_module() acquires 0x42::test::Y { + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^ +15 │ let addr = @0x1; +16 │ assert!((&0x42::test::Y<0x42::test::X>[addr]).field.value == true, 1); + │ ------------------------------------------------- accessed here + +error: Invalid operation: access of the field `value` on type `test::X` can only be done within the defining module `0x42::test` + ┌─ tests/file-format-generator/index_acquires_err.move:14:9 + │ +14 │ fun test_resource_other_module() acquires 0x42::test::Y { + │ ^^^^^^^^^^^^^^^^^^^^^^^^^^ +15 │ let addr = @0x1; +16 │ assert!((&0x42::test::Y<0x42::test::X>[addr]).field.value == true, 1); + │ ------------------------------------------------------- accessed here diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/index.exp b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/index.exp index 211e45bf31ae9..c40f8232f0285 100644 --- a/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/index.exp +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/index.exp @@ -1 +1 @@ -processed 14 tasks +processed 21 tasks diff --git a/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/index.move b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/index.move index a66801a28270f..1129ee1d16605 100644 --- a/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/index.move +++ b/third_party/move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/index.move @@ -11,19 +11,21 @@ module 0x42::test { fun test_resource_1() acquires R { use 0x42::test; - assert!((&test::R[@0x1]).value == true, 0); + assert!(test::R[@0x1].value == true, 0); + R[@0x1] = R{value: false}; + assert!(test::R[@0x1].value == false, 0); } fun test_resource_2() acquires R { let x = &mut 0x42::test::R[@0x1]; x.value = false; - assert!((&R[@0x1]).value == false, 1); + assert!(R[@0x1].value == false, 1); } struct X has copy, drop, store { value: M } - struct Y has key, drop { + struct Y has key, drop, copy { field: T } @@ -39,7 +41,13 @@ module 0x42::test { fun test_resource_3() acquires Y { use 0x42::test; - assert!((&test::Y>[@0x1]).field.value == true, 0); + assert!(test::Y>[@0x1].field.value == true, 0); + } + + fun test_resource_freeze() acquires Y { + use 0x42::test; + let y: &Y> = &mut test::Y>[@0x1]; + assert!(y.field.value == true, 0); } fun test_resource_4() acquires Y { @@ -49,7 +57,17 @@ module 0x42::test { spec { assert Y>[addr].field.value == false; }; - assert!((&Y>[addr]) .field.value == false, 1); + assert!(Y>[addr].field.value == false, 1); + } + + fun test_resource_5() acquires Y { + let addr = @0x1; + 0x42::test ::Y> [addr].field.value = false; + spec { + assert Y>[addr].field.value == false; + }; + let y_resource = Y>[addr]; + assert!(y_resource.field.value == false, 1); } fun test_vector() { @@ -58,6 +76,20 @@ module 0x42::test { }; let v = vector[x, x]; assert!(v[0].value == 2, 0); + v[0].value = 3; + assert!(v[0].value == 3, 0); + } + + fun test_two_dimension() { + let x = vector[vector[1, 2], vector[3, 4]]; + assert!(x[0][0] == 1, 0); + x[0] = vector[2, 3, 4]; + assert!(x[0][0] == 2, 0); + x[0][1] = 4; + assert!(x[0][1] == 4, 0); + let x = vector[vector[1, 2], vector[3, 4]]; + let y = 0; + assert!(x[{y = y + 1; y}][{y = y - 1; y}] == 3, 0); } fun test_vector_borrow() { @@ -74,8 +106,33 @@ module 0x42::test { field: x2 }; let v = vector[y1, y2]; - assert!((&v[0]).field.value == true, 0); - assert!((&v[1]).field.value == false, 0); + assert!(v[0].field.value == true, 0); + assert!(v[1].field.value == false, 0); + } + + fun foo(v: &Y>) { + assert!(v.field.value == true, 0); + } + + fun test_vector_borrow_freeze() { + let x1 = X { + value: true + }; + let x2 = X { + value: false + }; + let y1 = Y { + field: x1 + }; + let y2 = Y { + field: x2 + }; + let v = vector[y1, y2]; + let v_y1: &Y> = &mut v[0]; + assert!(v_y1.field.value == true, 0); + assert!(v[0].field.value == true, 0); + assert!(v[1].field.value == false, 0); + foo(&mut v[0]); } fun test_vector_borrow_mut() { @@ -92,12 +149,12 @@ module 0x42::test { field: x2 }; let v = vector[y1, y2]; - assert!((&v[0]).field.value == true, 0); - assert!((&v[1]).field.value == false, 0); - (&mut v[0]).field.value = false; - (&mut v[1]).field.value = true; - assert!((&v[0]).field.value == false, 0); - assert!((&v[1]).field.value == true, 0); + assert!(v[0].field.value == true, 0); + assert!(v[1].field.value == false, 0); + v[0].field.value = false; + v[1].field.value = true; + assert!(v[0].field.value == false, 0); + assert!(v[1].field.value == true, 0); } fun test_vector_const() { @@ -131,6 +188,43 @@ module 0x42::test { let v = vector[x, x]; let y = &(v[0].vec)[2]; assert!(*y == 3, 0); + assert!(v[1].vec[0] == 1, 0); + } + + fun init_3(s: &signer) { + let y = Y { + field: vector[(1 as u8),2,3] + }; + move_to(s, y); + } + + fun test_resource_with_vector() acquires Y { + assert!(Y>[@0x2].field[0] == 1, 0); + } + + fun bubble_sort(v: vector) { + use std::vector; + let n = vector::length(&v); + let i = 0; + + while (i < n) { + let j = 0; + while (j < n - i - 1) { + if (v[j] > v[j + 1]) { + let t = v[j]; + v[j] = v[j + 1]; + v[j + 1] = t; + }; + j = j + 1; + }; + i = i + 1; + }; + assert!(v[0] == 1, 0); + } + + fun call_sort() { + let v = vector[3, 1, 2]; + bubble_sort(v); } } @@ -143,16 +237,24 @@ module 0x42::test { //# run --verbose -- 0x42::test::test_vector +//# run --verbose -- 0x42::test::test_two_dimension + //# run --verbose -- 0x42::test::test_vector_borrow +//# run --verbose -- 0x42::test::test_vector_borrow_freeze + //# run --verbose -- 0x42::test::test_vector_borrow_mut //# run --verbose --signers 0x1 -- 0x42::test::init_2 //# run --verbose -- 0x42::test::test_resource_3 +//# run --verbose -- 0x42::test::test_resource_freeze + //# run --verbose -- 0x42::test::test_resource_4 +//# run --verbose -- 0x42::test::test_resource_5 + //# run --verbose -- 0x42::test::test_vector_const //# run --verbose -- 0x42::test::test_vector_in_struct @@ -160,3 +262,9 @@ module 0x42::test { //# run --verbose -- 0x42::test::test_vector_in_struct_2 //# run --verbose -- 0x42::test::test_vector_in_struct_3 + +//# run --verbose --signers 0x2 -- 0x42::test::init_3 + +//# run --verbose -- 0x42::test::test_resource_with_vector + +//# run --verbose -- 0x42::test::call_sort diff --git a/third_party/move/move-compiler/src/expansion/ast.rs b/third_party/move/move-compiler/src/expansion/ast.rs index 3189ff702b406..30b50b9e191ed 100644 --- a/third_party/move/move-compiler/src/expansion/ast.rs +++ b/third_party/move/move-compiler/src/expansion/ast.rs @@ -488,7 +488,7 @@ pub enum Exp_ { Borrow(bool, Box), ExpDotted(Box), - Index(Box, Box), // spec only (no mutation needed right now) + Index(Box, Box), // spec only unless language >= v2 Cast(Box, Type), Annotate(Box, Type), @@ -1655,7 +1655,9 @@ impl AstDebug for Exp_ { rhs.ast_debug(w); }, E::Mutate(lhs, rhs) => { - w.write("*"); + if !matches!(lhs.value, E::Index(_, _)) { + w.write("*"); + } lhs.ast_debug(w); w.write(" = "); rhs.ast_debug(w); diff --git a/third_party/move/move-compiler/src/expansion/translate.rs b/third_party/move/move-compiler/src/expansion/translate.rs index 2fd6f8b8ae8c5..990149d2c7c6e 100644 --- a/third_party/move/move-compiler/src/expansion/translate.rs +++ b/third_party/move/move-compiler/src/expansion/translate.rs @@ -2492,116 +2492,13 @@ fn exps(context: &mut Context, pes: Vec) -> Vec { pes.into_iter().map(|pe| exp_(context, pe)).collect() } -/// This function assumes `e` and `i` are from an index expression `e[i]` and generates -/// the expression `& vector::borrow(&e, i)` or `&mut vector::borrow_mut(&e, i)` based on -/// the `mutable` flag -fn call_to_vector_borrow( - context: &mut Context, - loc: &Loc, - e: P::Exp, - i: P::Exp, - mutable: bool, -) -> E::Exp { - use E::Exp_ as EE; - let std_address = Address::Numerical(None, Spanned { - loc: *loc, - value: NumericalAddress::STD_ADDRESS, - }); - let module_name = ModuleName(Name::new(*loc, Symbol::from("vector"))); - let ident = E::ModuleIdent_::new(std_address, module_name); - let borrow_fun = if mutable { "borrow_mut" } else { "borrow" }; - let access = E::ModuleAccess::new( - *loc, - E::ModuleAccess_::ModuleAccess( - sp(*loc, ident), - Name::new(*loc, Symbol::from(borrow_fun)), - None, - ), - ); - let vector_var = exp_(context, e.clone()); - sp( - *loc, - EE::Call( - access, - CallKind::Regular, - None, - sp(*loc, vec![ - sp(*loc, EE::Borrow(mutable, Box::new(vector_var))), - exp_(context, i), - ]), - ), - ) -} - -/// This function assumes `e` and `i` are from an index expression `e[i]` and generates -/// the expression `borrow_global(i)` or `borrow_global_mut(i)` based on -/// the `mutable` flag. -/// Assumption: -/// `e` must be a struct type -fn call_to_borrow_global( - context: &mut Context, - loc: &Loc, - e: P::Type_, - i: P::Exp, - mutable: bool, -) -> E::Exp { - use E::Exp_ as EE; - let borrow_global_fun = if mutable { - "borrow_global_mut" - } else { - "borrow_global" - }; - let access = E::ModuleAccess::new( - *loc, - E::ModuleAccess_::Name(Name::new(*loc, Symbol::from(borrow_global_fun))), - ); - let tys_opt = optional_types(context, Some(vec![sp(*loc, e)])); - sp( - *loc, - EE::Call( - access, - CallKind::Regular, - tys_opt, - sp(*loc, vec![exp_(context, i)]), - ), - ) -} - -fn is_valid_local_name(s: Symbol) -> bool { - s.starts_with('_') || s.starts_with(|c: char| c.is_ascii_lowercase()) -} - -fn is_struct_in_current_module(context: &Context, name: &Name) -> bool { - if let Some(m) = context.current_module { - if context.module_members.0.contains_key(&m.value) { - let vs = context.module_members.0.get(&m.value).unwrap(); - return vs.1.iter().any(|(info_name, info)| { - info.kind == ModuleMemberKind::Struct && info_name == name - }); - } - } - false -} - -fn is_constant(context: &Context, name: &Name) -> bool { - for (_, members) in context.module_members.0.values() { - if members - .iter() - .any(|(info_name, info)| info.kind == ModuleMemberKind::Constant && info_name == name) - { - return true; - } - } - false -} - fn exp(context: &mut Context, pe: P::Exp) -> Box { Box::new(exp_(context, pe)) } fn exp_(context: &mut Context, sp!(loc, pe_): P::Exp) -> E::Exp { use E::Exp_ as EE; - use P::{Exp_ as PE, Type_ as PT}; + use P::Exp_ as PE; let e_ = match pe_ { PE::Unit => EE::Unit { trailing: false }, PE::Value(pv) => match value(context, pv) { @@ -2613,7 +2510,7 @@ fn exp_(context: &mut Context, sp!(loc, pe_): P::Exp) -> E::Exp { }, PE::Move(v) => EE::Move(v), PE::Copy(v) => EE::Copy(v), - PE::Name(_pn, Some(_ty)) if !context.in_spec_context => { + PE::Name(_pn, Some(_ty)) if !context.in_spec_context && !context.env.flags().lang_v2() => { context.env.add_diag(diag!( Syntax::SpecContextRestricted, ( @@ -2792,38 +2689,7 @@ fn exp_(context: &mut Context, sp!(loc, pe_): P::Exp) -> E::Exp { EE::BinopExp(exp(context, *pl), op, exp(context, *pr)) } }, - PE::Borrow(mut_, pr) => { - if let PE::Index(ref e, ref i) = pr.value { - // handling `&_[_]` or `&mut _[_]` - if context.env.flags().compiler_v2() { - if let PE::Name(sp!(_, ref ptn), _) = e.value { - let name = ptn.name(); - if is_struct_in_current_module(context, name) { - if let PE::Name(chain, types) = &e.value { - let ty = PT::Apply( - Box::new(chain.clone()), - types.clone().unwrap_or(vec![]), - ); - return call_to_borrow_global(context, &loc, ty, *i.clone(), mut_); - } - } else if !context.in_spec_context - && (is_valid_local_name(name.value) || is_constant(context, name)) - { - return call_to_vector_borrow( - context, - &loc, - *e.clone(), - *i.clone(), - mut_, - ); - } - } else if !context.in_spec_context { - return call_to_vector_borrow(context, &loc, *e.clone(), *i.clone(), mut_); - } - } - } - EE::Borrow(mut_, exp(context, *pr)) - }, + PE::Borrow(mut_, pr) => EE::Borrow(mut_, exp(context, *pr)), pdotted_ @ PE::Dot(_, _) => match exp_dotted(context, sp(loc, pdotted_)) { Some(edotted) => EE::ExpDotted(Box::new(edotted)), None => { @@ -2833,61 +2699,19 @@ fn exp_(context: &mut Context, sp!(loc, pe_): P::Exp) -> E::Exp { }, PE::Cast(e, ty) => EE::Cast(exp(context, *e), type_(context, ty)), PE::Index(e, i) => { - if context.env.flags().compiler_v2() { - // handling `_[_]` or `_[_]` (without `&` or `&mut`) - if let PE::Name(sp!(_, ref ptn), _) = e.value { - let name = ptn.name(); - if is_struct_in_current_module(context, name) { - if let PE::Name(chain, types) = &e.value { - let ty = - PT::Apply(Box::new(chain.clone()), types.clone().unwrap_or(vec![])); - let call = call_to_borrow_global(context, &loc, ty, *i.clone(), false); - if !context.in_spec_context { - context - .env - .add_diag(diag!(Syntax::UnexpectedToken, (loc, "resource indexing using `_[_]` needs to be paired with `&` or `&mut`"))); - } - return call; - } - } else { - let exp_ = if context.in_spec_context { - EE::Index(exp(context, *e.clone()), exp(context, *i)) - } else { - // v[i] without `&` or `&mut` is translated into - // *(vector::borrow(&v, i)) - EE::Dereference(Box::new(sp( - loc, - call_to_vector_borrow(context, &loc, *e.clone(), *i, false).value, - ))) - }; - if !is_valid_local_name(name.value) && !is_constant(context, name) { - context.env.add_diag(diag!( - Syntax::UnexpectedToken, - (loc, "index notation `_[_]` expects a resource or vector") - )); - } - return sp(loc, exp_); - } - } else { - let exp_ = if context.in_spec_context { - EE::Index(exp(context, *e), exp(context, *i)) - } else { - EE::Dereference(Box::new(sp( - loc, - call_to_vector_borrow(context, &loc, *e, *i, false).value, - ))) - }; - return sp(loc, exp_); - } - unreachable!(); - } else if context.in_spec_context { + if context.env.flags().lang_v2() || context.in_spec_context { EE::Index(exp(context, *e), exp(context, *i)) } else { + // If it is a name, call `name_access_chain` to avoid + // the unused alias warning + if let PE::Name(pn, _) = e.value { + let _ = name_access_chain(context, Access::Term, pn, None); + } context.env.add_diag(diag!( - Syntax::SpecContextRestricted, + Syntax::UnsupportedLanguageItem, ( loc, - "`_[_]` index operator in non-specification code only allowed in Move 2" + "`_[_]` index operator in non-specification code only allowed in Move 2 and beyond" ) )); EE::UnresolvedError @@ -3125,6 +2949,10 @@ fn lvalues(context: &mut Context, sp!(loc, e_): P::Exp) -> Option { pes.into_iter().map(|pe| assign(context, pe)).collect(); L::Assigns(sp(loc, al_opt?)) }, + PE::Index(_, _) if context.env.flags().lang_v2() => { + let er = exp(context, sp(loc, e_)); + L::Mutate(er) + }, PE::Dereference(pr) => { let er = exp(context, *pr); L::Mutate(er) @@ -3488,7 +3316,10 @@ fn check_valid_address_name_( } fn check_valid_local_name(context: &mut Context, v: &Var) { - if !is_valid_local_name(v.value()) { + fn is_valid(s: Symbol) -> bool { + s.starts_with('_') || s.starts_with(|c: char| c.is_ascii_lowercase()) + } + if !is_valid(v.value()) { let msg = format!( "Invalid local variable name '{}'. Local variable names must start with 'a'..'z' (or \ '_')", @@ -3507,7 +3338,7 @@ struct ModuleMemberInfo { pub deprecation: Option, // Some(loc) if member is deprecated at loc } -#[derive(Copy, Clone, Debug, PartialEq)] +#[derive(Copy, Clone, Debug)] enum ModuleMemberKind { Constant, Function, diff --git a/third_party/move/move-compiler/src/parser/ast.rs b/third_party/move/move-compiler/src/parser/ast.rs index 67e0854a30cd3..74a209128256b 100644 --- a/third_party/move/move-compiler/src/parser/ast.rs +++ b/third_party/move/move-compiler/src/parser/ast.rs @@ -466,18 +466,6 @@ pub enum NameAccessChain_ { // (|):::::: Four(Spanned<(LeadingNameAccess, Name)>, Name, Name), } - -impl NameAccessChain_ { - pub fn name(&self) -> &Name { - match &self { - NameAccessChain_::One(x) => x, - NameAccessChain_::Two(_, x) => x, - NameAccessChain_::Three(_, x) => x, - NameAccessChain_::Four(_, x, _) => x, - } - } -} - pub type NameAccessChain = Spanned; #[derive(Debug, PartialEq, Eq, PartialOrd, Ord, Clone, Copy, Hash)] diff --git a/third_party/move/move-compiler/tests/move_check/parser/spec_parsing_index_fail.exp b/third_party/move/move-compiler/tests/move_check/parser/spec_parsing_index_fail.exp index eaeac52c2b659..58d12e8a6325b 100644 --- a/third_party/move/move-compiler/tests/move_check/parser/spec_parsing_index_fail.exp +++ b/third_party/move/move-compiler/tests/move_check/parser/spec_parsing_index_fail.exp @@ -1,6 +1,6 @@ -error[E01010]: syntax item restricted to spec contexts +error[E01013]: unsupported language construct ┌─ tests/move_check/parser/spec_parsing_index_fail.move:3:15 │ 3 │ let _ = x[1]; - │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 + │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 and beyond diff --git a/third_party/move/move-compiler/tests/move_check/v2-not-supported/index.exp b/third_party/move/move-compiler/tests/move_check/v2-not-supported/index.exp deleted file mode 100644 index a9e9c5ba03258..0000000000000 --- a/third_party/move/move-compiler/tests/move_check/v2-not-supported/index.exp +++ /dev/null @@ -1,102 +0,0 @@ -warning[W09001]: unused alias - ┌─ tests/move_check/v2-not-supported/index.move:10:19 - │ -10 │ use 0x42::test; - │ ^^^^ Unused 'use' of alias 'test'. Consider removing it - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:11:19 - │ -11 │ assert!((&test::R[@0x1]).value == true, 0); - │ ^^^^^^^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:15:22 - │ -15 │ let x = &mut 0x42::test::R[@0x1]; - │ ^^^^^^^^^^^^^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:17:19 - │ -17 │ assert!((&R[@0x1]).value == false, 1); - │ ^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -warning[W09001]: unused alias - ┌─ tests/move_check/v2-not-supported/index.move:38:19 - │ -38 │ use 0x42::test; - │ ^^^^ Unused 'use' of alias 'test'. Consider removing it - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:39:19 - │ -39 │ assert!((&test::Y>[@0x1]).field.value == true, 0); - │ ^^^^^^^^^^^^^^^^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:44:22 - │ -44 │ let y = &mut 0x42::test ::Y> [addr]; - │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:46:19 - │ -46 │ assert!((&Y>[addr]) .field.value == false, 1); - │ ^^^^^^^^^^^^^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:54:17 - │ -54 │ assert!(v[0].value == 2, 0); - │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:71:19 - │ -71 │ assert!((&v[0]).field.value == true, 0); - │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:72:19 - │ -72 │ assert!((&v[1]).field.value == false, 0); - │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:89:19 - │ -89 │ assert!((&v[0]).field.value == true, 0); - │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:90:19 - │ -90 │ assert!((&v[1]).field.value == false, 0); - │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:91:15 - │ -91 │ (&mut v[0]).field.value = false; - │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:92:15 - │ -92 │ (&mut v[1]).field.value = true; - │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:93:19 - │ -93 │ assert!((&v[0]).field.value == false, 0); - │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - -error[E01010]: syntax item restricted to spec contexts - ┌─ tests/move_check/v2-not-supported/index.move:94:19 - │ -94 │ assert!((&v[1]).field.value == true, 0); - │ ^^^^ `_[_]` index operator in non-specification code only allowed in Move 2 - diff --git a/third_party/move/move-model/src/ast.rs b/third_party/move/move-model/src/ast.rs index a43c54fa96b37..e06543c6fd668 100644 --- a/third_party/move/move-model/src/ast.rs +++ b/third_party/move/move-model/src/ast.rs @@ -2704,6 +2704,10 @@ impl Address { panic!("expected numerical address, found symbolic") } } + + pub fn is_one(&self) -> bool { + matches!(self, Address::Numerical(AccountAddress::ONE)) + } } // enables `env.display(address)` diff --git a/third_party/move/move-model/src/builder/exp_builder.rs b/third_party/move/move-model/src/builder/exp_builder.rs index e9f859d19bb55..c85ebb4bc0ae7 100644 --- a/third_party/move/move-model/src/builder/exp_builder.rs +++ b/third_party/move/move-model/src/builder/exp_builder.rs @@ -25,10 +25,11 @@ use crate::{ ReceiverFunctionInstance, ReferenceKind, Substitution, Type, TypeDisplayContext, TypeUnificationError, UnificationContext, Variance, WideningOrder, BOOL_TYPE, }, + FunId, }; use codespan_reporting::diagnostic::Severity; use itertools::Itertools; -use move_binary_format::file_format::{self, AbilitySet}; +use move_binary_format::file_format::{self, Ability, AbilitySet}; use move_compiler::{ expansion::ast as EA, hlir::ast as HA, @@ -381,7 +382,6 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo let mut reported_vars = BTreeSet::new(); for i in self.node_counter_start..self.env().next_free_node_number() { let node_id = NodeId::new(i); - if let Some(ty) = self.get_node_type_opt(node_id) { let ty = self.finalize_type(node_id, &ty, &mut reported_vars); self.update_node_type(node_id, ty); @@ -1636,7 +1636,9 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo context, ) }, - EA::Exp_::ExpDotted(dotted) => self.translate_dotted(dotted, expected_type, context), + EA::Exp_::ExpDotted(dotted) => { + self.translate_dotted(dotted, expected_type, false, context) + }, EA::Exp_::Index(target, index) => { self.translate_index(&loc, target, index, expected_type, context) }, @@ -1735,7 +1737,19 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo let (rhs_ty, rhs) = self.translate_exp_free(rhs); // Do not freeze when translating the lhs of a mutate operation self.insert_freeze = false; - let (lhs_ty, lhs) = self.translate_exp_free(lhs); + let (lhs_ty, lhs) = if let EA::Exp_::Index(target, index) = &lhs.value { + let result_ty = + Type::Reference(ReferenceKind::Mutable, Box::new(rhs_ty.clone())); + if let Some(call) = self.try_resource_or_vector_index( + &loc, target, index, context, &result_ty, true, + ) { + (result_ty, call) + } else { + self.translate_exp_free(lhs) + } + } else { + self.translate_exp_free(lhs) + }; self.insert_freeze = true; self.check_type( &self.get_node_loc(lhs.node_id()), @@ -1751,7 +1765,7 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo let (ty, rhs) = self.translate_exp_free(rhs); // Do not freeze when translating the lhs of a mutate operation self.insert_freeze = false; - let lhs = self.translate_dotted(lhs, &ty, &ErrorMessageContext::Assignment); + let lhs = self.translate_dotted(lhs, &ty, true, &ErrorMessageContext::Assignment); self.insert_freeze = true; let result_ty = self.check_type(&loc, &Type::unit(), expected_type, context); let id = self.new_node_id_with_type_loc(&result_ty, &loc); @@ -1774,6 +1788,13 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo let target_ty = self.fresh_type_var(); let ty = Type::Reference(ref_kind, Box::new(target_ty.clone())); let result_ty = self.check_type(&loc, &ty, expected_type, context); + if let EA::Exp_::Index(target, index) = &exp.value { + if let Some(call) = self.try_resource_or_vector_index( + &loc, target, index, context, &result_ty, *mutable, + ) { + return call; + } + } let target_exp = self.translate_exp(exp, &target_ty); if self.subs.specialize(&target_ty).is_reference() { self.error(&loc, "cannot borrow from a reference") @@ -3236,6 +3257,201 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo } } + fn call_to_borrow_global_for_index_op( + &mut self, + loc: &Loc, + resource_ty_exp: &EA::Exp, + addr_exp: &EA::Exp, + mutable: bool, + expected_type: &Type, + context: &ErrorMessageContext, + ) -> ExpData { + fn convert_name_to_type( + loc: &move_ir_types::location::Loc, + exp_: EA::Exp_, + ) -> Option { + if let EA::Exp_::Name(m, type_opt) = exp_ { + Some(EA::Type::new( + *loc, + EA::Type_::Apply(m, type_opt.unwrap_or(vec![])), + )) + } else { + None + } + } + let type_opt = convert_name_to_type(&resource_ty_exp.loc, resource_ty_exp.clone().value); + if let Some(ty) = type_opt { + let resource_ty = self.translate_type(&ty); + let ref_t = Type::Reference( + ReferenceKind::from_is_mut(mutable), + Box::new(resource_ty.clone()), + ); + let ty = self.check_type(loc, &ref_t, expected_type, context); + if ty.is_error() { + return self.new_error_exp(); + } + let addr = self.translate_exp_in_context( + addr_exp, + &Type::Primitive(PrimitiveType::Address), + context, + ); + let node = self.new_node_id_with_type_loc( + &Type::Reference( + ReferenceKind::from_is_mut(mutable), + Box::new(resource_ty.clone()), + ), + loc, + ); + self.set_node_instantiation(node, vec![resource_ty.clone()]); + ExpData::Call( + node, + Operation::BorrowGlobal(ReferenceKind::from_is_mut(mutable)), + vec![addr.into()], + ) + } else { + self.new_error_exp() + } + } + + //TODO: make a Lazy const for mid and fid of vector functions + fn get_vector_borrow(&self, mutable: bool) -> (Option, Option) { + let target_str = if mutable { + "vector::borrow_mut" + } else { + "vector::borrow" + }; + for m in self.env().get_modules() { + if m.is_std_vector() { + let mid = m.get_id(); + for f in m.get_functions() { + if f.get_full_name_str() == target_str { + let fid = f.get_id(); + return (Some(mid), Some(fid)); + } + } + } + } + (None, None) + } + + fn call_to_vector_borrow_for_index_op( + &mut self, + loc: &Loc, + vec_exp: &EA::Exp, + idx_exp: &EA::Exp, + mutable: bool, + expected_type: &Type, + context: &ErrorMessageContext, + ) -> ExpData { + let inner_ty = if let Type::Reference(_, in_ty) = &expected_type { + in_ty.as_ref().clone() + } else { + expected_type.clone() + }; + let ref_vec_exp_e = &sp( + vec_exp.loc, + EA::Exp_::Borrow(mutable, Box::new(vec_exp.clone())), + ); + let vec_exp_e = self.translate_exp_in_context( + ref_vec_exp_e, + &Type::Reference( + ReferenceKind::from_is_mut(mutable), + Box::new(Type::Vector(Box::new(inner_ty.clone()))), + ), + context, + ); + let idx_exp_e = + self.translate_exp_in_context(idx_exp, &Type::Primitive(PrimitiveType::U64), context); + if self.had_errors { + return self.new_error_exp(); + } + if let (Some(mid), Some(fid)) = self.get_vector_borrow(mutable) { + let instantiated_inner = self.subs.specialize(&inner_ty); + let node_id = self.env().new_node( + loc.clone(), + Type::Reference( + ReferenceKind::from_is_mut(mutable), + Box::new(instantiated_inner.clone()), + ), + ); + self.set_node_instantiation(node_id, vec![inner_ty.clone()]); + let call = ExpData::Call(node_id, Operation::MoveFunction(mid, fid), vec![ + vec_exp_e.into_exp(), + idx_exp_e.clone().into_exp(), + ]); + return call; + } + ExpData::Invalid(self.env().new_node_id()) + } + + /// Try to translate a resource or vector Index expression + fn try_resource_or_vector_index( + &mut self, + loc: &Loc, + target: &EA::Exp, + index: &EA::Exp, + context: &ErrorMessageContext, + ty: &Type, + mutable: bool, + ) -> Option { + let mut call = None; + if let EA::Exp_::Name(m, _) = &target.value { + let global_var_sym = match &m.value { + EA::ModuleAccess_::ModuleAccess(..) => self.parent.module_access_to_qualified(m), + EA::ModuleAccess_::Name(name) => { + let sym = self.symbol_pool().make(name.value.as_str()); + self.parent.qualified_by_module(sym) + }, + }; + if self + .parent + .parent + .struct_table + .contains_key(&global_var_sym) + { + self.check_language_version(loc, "resource indexing", LanguageVersion::V2_0); + if self + .parent + .parent + .struct_table + .get(&global_var_sym) + .is_some_and(|entry| entry.abilities.has_ability(Ability::Key)) + { + call = Some(self.call_to_borrow_global_for_index_op( + loc, target, index, mutable, ty, context, + )); + } else { + self.error(loc, "resource indexing can only applied to a resource type (a struct type which has key ability)"); + call = Some(self.new_error_exp()); + } + } else if self + .parent + .parent + .spec_schema_table + .contains_key(&global_var_sym) + && self + .env() + .language_version + .is_at_least(LanguageVersion::V2_0) + { + self.error(loc, "indexing can only be applied to a vector or a resource type (a struct type which has key ability)"); + call = Some(self.new_error_exp()); + } + } + if !self.is_spec_mode() { + self.check_language_version(loc, "vector indexing", LanguageVersion::V2_0); + // Translate to vector indexing in impl mode if the target is not a resource or a spec schema + // spec mode is handled in `translate_index` + if call.is_none() { + call = + Some(self.call_to_vector_borrow_for_index_op( + loc, target, index, mutable, ty, context, + )); + } + } + call + } + /// Translate an Index expression. fn translate_index( &mut self, @@ -3245,6 +3461,22 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo expected_type: &Type, context: &ErrorMessageContext, ) -> ExpData { + let index_call_opt = self.try_resource_or_vector_index( + loc, + target, + index, + context, + &Type::Reference(ReferenceKind::Immutable, Box::new(expected_type.clone())), + false, + ); + if let Some(call) = index_call_opt { + if !self.is_spec_mode() { + // if v[i] is on right hand side, need deref to get the value + let deref_id = self.new_node_id_with_type_loc(expected_type, loc); + return ExpData::Call(deref_id, Operation::Deref, vec![call.into_exp()]); + } + return call; + } // We must concretize the type of index to decide whether this is a slice // or not. This is not compatible with full type inference, so we may // try to actually represent slicing explicitly in the syntax to fix this. @@ -3277,10 +3509,28 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo &mut self, dotted: &EA::ExpDotted, expected_type: &Type, + index_mutate: bool, context: &ErrorMessageContext, ) -> ExpData { match &dotted.value { - EA::ExpDotted_::Exp(e) => self.translate_exp_in_context(e, expected_type, context), + EA::ExpDotted_::Exp(e) => { + if let EA::Exp_::Index(target, index) = &e.value { + if let Some(call) = self.try_resource_or_vector_index( + &self.to_loc(&e.loc), + target, + index, + context, + &Type::Reference( + ReferenceKind::from_is_mut(index_mutate), + Box::new(expected_type.clone()), + ), + index_mutate, + ) { + return call; + } + } + self.translate_exp_in_context(e, expected_type, context) + }, EA::ExpDotted_::Dot(e, n) => { let loc = self.to_loc(&dotted.loc); let field_name = self.symbol_pool().make(n.value.as_str()); @@ -3289,7 +3539,12 @@ impl<'env, 'translator, 'module_translator> ExpTranslator<'env, 'translator, 'mo ); let ty = self.fresh_type_var_constr(loc.clone(), WideningOrder::RightToLeft, constraint); - let exp = self.translate_dotted(e.as_ref(), &ty, &ErrorMessageContext::General); + let exp = self.translate_dotted( + e.as_ref(), + &ty, + index_mutate, + &ErrorMessageContext::General, + ); let id = self.new_node_id_with_type_loc(expected_type, &loc); self.set_node_instantiation(id, vec![ty.clone()]); let oper = if let Type::Struct(mid, sid, _inst) = self.subs.specialize(&ty) { diff --git a/third_party/move/move-prover/tests/sources/functional/resource_index.exp b/third_party/move/move-prover/tests/sources/functional/resource_index.exp deleted file mode 100644 index d82a90e348624..0000000000000 --- a/third_party/move/move-prover/tests/sources/functional/resource_index.exp +++ /dev/null @@ -1,12 +0,0 @@ -Move prover returns: exiting with model building errors -error: undeclared `test::Y` - ┌─ tests/sources/functional/resource_index.move:15:20 - │ -15 │ assert Y>[addr].field.value == false; - │ ^ - -error: expected `num` but found a value of type `address` - ┌─ tests/sources/functional/resource_index.move:15:20 - │ -15 │ assert Y>[addr].field.value == false; - │ ^^^^^^^^^^^^^^^^ diff --git a/third_party/move/move-prover/tests/testsuite.rs b/third_party/move/move-prover/tests/testsuite.rs index df422fbf3f1b3..ce00af413d996 100644 --- a/third_party/move/move-prover/tests/testsuite.rs +++ b/third_party/move/move-prover/tests/testsuite.rs @@ -8,6 +8,7 @@ use datatest_stable::Requirements; use itertools::Itertools; use log::{info, warn}; use move_command_line_common::{env::read_env_var, testing::EXP_EXT}; +use move_model::metadata::LanguageVersion; use move_prover::{cli::Options, run_move_prover, run_move_prover_v2}; use move_prover_test_utils::{baseline_test::verify_or_update_baseline, extract_test_directives}; use once_cell::sync::OnceCell; @@ -168,8 +169,10 @@ fn test_runner_for_feature(path: &Path, feature: &Feature) -> datatest_stable::R let mut error_writer = Buffer::no_color(); let result = if feature.v2 { + options.language_version = Some(LanguageVersion::V2_0); run_move_prover_v2(&mut error_writer, options) } else { + options.model_builder.language_version = LanguageVersion::V2_0; run_move_prover(&mut error_writer, options) }; let mut diags = match result {