From 0029300cc400551433b5f77b0663cdc13b405b2c Mon Sep 17 00:00:00 2001
From: Teng Zhang <rahxephon89@163.com>
Date: Tue, 26 Nov 2024 21:17:37 +0000
Subject: [PATCH] fix enum bug (#15403)
---
.../boogie-backend/src/bytecode_translator.rs | 7 +-
.../tests/sources/functional/enum.exp | 20 +++--
.../tests/sources/functional/enum.move | 8 ++
.../tests/sources/functional/enum.v2_exp | 90 +++++++++----------
4 files changed, 72 insertions(+), 53 deletions(-)
diff --git a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
index 661c782d8aac8..c6f7d71839415 100644
--- a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
+++ b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
@@ -445,7 +445,12 @@ impl<'env> StructTranslator<'env> {
"", // not inlined!
&format!("$IsValid'{}'(s: {}): bool", suffix_variant, struct_name),
|| {
- if struct_env.is_intrinsic() || struct_env.get_field_count() == 0 {
+ if struct_env.is_intrinsic()
+ || struct_env
+ .get_fields_of_variant(variant)
+ .collect_vec()
+ .is_empty()
+ {
emitln!(writer, "true")
} else {
let mut sep = "";
diff --git a/third_party/move/move-prover/tests/sources/functional/enum.exp b/third_party/move/move-prover/tests/sources/functional/enum.exp
index 914ff680e45c2..a4b90881bf502 100644
--- a/third_party/move/move-prover/tests/sources/functional/enum.exp
+++ b/third_party/move/move-prover/tests/sources/functional/enum.exp
@@ -2,23 +2,29 @@ Move prover returns: exiting with model building errors
error: unsupported language construct
┌─ tests/sources/functional/enum.move:3:5
│
-3 │ enum CommonFields has copy, drop {
+3 │ enum TestNoField has copy, drop {
│ ^^^^ Move 2 language construct is not enabled: enum types
error: unsupported language construct
- ┌─ tests/sources/functional/enum.move:10:25
+ ┌─ tests/sources/functional/enum.move:11:5
│
-10 │ invariant (self is CommonFields::Bar) ==> self.z > 10;
+11 │ enum CommonFields has copy, drop {
+ │ ^^^^ Move 2 language construct is not enabled: enum types
+
+error: unsupported language construct
+ ┌─ tests/sources/functional/enum.move:18:25
+ │
+18 │ invariant (self is CommonFields::Bar) ==> self.z > 10;
│ ^^ Move 2 language construct is not enabled: `is` expression
error: unsupported language construct
- ┌─ tests/sources/functional/enum.move:39:9
+ ┌─ tests/sources/functional/enum.move:47:9
│
-39 │ match (&common) {
+47 │ match (&common) {
│ ^^^^^ Move 2 language construct is not enabled: match expression
error: unsupported language construct
- ┌─ tests/sources/functional/enum.move:49:5
+ ┌─ tests/sources/functional/enum.move:57:5
│
-49 │ enum CommonFieldsVector has drop {
+57 │ enum CommonFieldsVector has drop {
│ ^^^^ Move 2 language construct is not enabled: enum types
diff --git a/third_party/move/move-prover/tests/sources/functional/enum.move b/third_party/move/move-prover/tests/sources/functional/enum.move
index 9ac6876a40186..89d005e08f2a3 100644
--- a/third_party/move/move-prover/tests/sources/functional/enum.move
+++ b/third_party/move/move-prover/tests/sources/functional/enum.move
@@ -1,5 +1,13 @@
module 0x815::m {
+ enum TestNoField has copy, drop {
+ NoField
+ }
+
+ fun test_no_field(): TestNoField {
+ TestNoField::NoField
+ }
+
enum CommonFields has copy, drop {
Foo{x: u64, y: u8},
Bar{x: u64, y: u8, z: u32}
diff --git a/third_party/move/move-prover/tests/sources/functional/enum.v2_exp b/third_party/move/move-prover/tests/sources/functional/enum.v2_exp
index a4c03bfa8340f..9a4eed455c87b 100644
--- a/third_party/move/move-prover/tests/sources/functional/enum.v2_exp
+++ b/third_party/move/move-prover/tests/sources/functional/enum.v2_exp
@@ -1,63 +1,63 @@
Move prover returns: exiting with verification errors
error: data invariant does not hold
- ┌─ tests/sources/functional/enum.move:9:9
- │
-9 │ invariant self.x > 20;
- │ ^^^^^^^^^^^^^^^^^^^^^^
- │
- = at tests/sources/functional/enum.move:15: t9_common_field
- = at tests/sources/functional/enum.move:16: t9_common_field
- = at tests/sources/functional/enum.move:17: t9_common_field
- = at tests/sources/functional/enum.move:14: t9_common_field
- = at tests/sources/functional/enum.move:9
- = at tests/sources/functional/enum.move:10
- = at tests/sources/functional/enum.move:14: t9_common_field
- = common = <redacted>
- = at tests/sources/functional/enum.move:19: t9_common_field
- = at tests/sources/functional/enum.move:9
+ ┌─ tests/sources/functional/enum.move:17:9
+ │
+17 │ invariant self.x > 20;
+ │ ^^^^^^^^^^^^^^^^^^^^^^
+ │
+ = at tests/sources/functional/enum.move:23: t9_common_field
+ = at tests/sources/functional/enum.move:24: t9_common_field
+ = at tests/sources/functional/enum.move:25: t9_common_field
+ = at tests/sources/functional/enum.move:22: t9_common_field
+ = at tests/sources/functional/enum.move:17
+ = at tests/sources/functional/enum.move:18
+ = at tests/sources/functional/enum.move:22: t9_common_field
+ = common = <redacted>
+ = at tests/sources/functional/enum.move:27: t9_common_field
+ = at tests/sources/functional/enum.move:17
error: data invariant does not hold
- ┌─ tests/sources/functional/enum.move:10:9
+ ┌─ tests/sources/functional/enum.move:18:9
│
-10 │ invariant (self is CommonFields::Bar) ==> self.z > 10;
+18 │ invariant (self is CommonFields::Bar) ==> self.z > 10;
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
- = at tests/sources/functional/enum.move:25: test_data_invariant
- = at tests/sources/functional/enum.move:26: test_data_invariant
- = at tests/sources/functional/enum.move:27: test_data_invariant
- = at tests/sources/functional/enum.move:24: test_data_invariant
- = at tests/sources/functional/enum.move:9
- = at tests/sources/functional/enum.move:10
- = at tests/sources/functional/enum.move:24: test_data_invariant
+ = at tests/sources/functional/enum.move:33: test_data_invariant
+ = at tests/sources/functional/enum.move:34: test_data_invariant
+ = at tests/sources/functional/enum.move:35: test_data_invariant
+ = at tests/sources/functional/enum.move:32: test_data_invariant
+ = at tests/sources/functional/enum.move:17
+ = at tests/sources/functional/enum.move:18
+ = at tests/sources/functional/enum.move:32: test_data_invariant
= common = <redacted>
- = at tests/sources/functional/enum.move:29: test_data_invariant
+ = at tests/sources/functional/enum.move:37: test_data_invariant
= <redacted> = <redacted>
= z = <redacted>
- = at tests/sources/functional/enum.move:30: test_data_invariant
- = at tests/sources/functional/enum.move:9
- = at tests/sources/functional/enum.move:10
+ = at tests/sources/functional/enum.move:38: test_data_invariant
+ = at tests/sources/functional/enum.move:17
+ = at tests/sources/functional/enum.move:18
error: unknown assertion failed
- ┌─ tests/sources/functional/enum.move:68:13
+ ┌─ tests/sources/functional/enum.move:76:13
│
-68 │ assert _common_vector_1.x != _common_vector_2.x; // this fails
+76 │ assert _common_vector_1.x != _common_vector_2.x; // this fails
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
- = at tests/sources/functional/enum.move:56: test_enum_vector
- = at tests/sources/functional/enum.move:55: test_enum_vector
- = _common_vector_1 = <redacted>
- = at tests/sources/functional/enum.move:59: test_enum_vector
- = at tests/sources/functional/enum.move:60: test_enum_vector
- = at tests/sources/functional/enum.move:61: test_enum_vector
- = at tests/sources/functional/enum.move:58: test_enum_vector
- = at tests/sources/functional/enum.move:9
- = at tests/sources/functional/enum.move:10
- = at tests/sources/functional/enum.move:58: test_enum_vector
- = _common_fields = <redacted>
= at tests/sources/functional/enum.move:64: test_enum_vector
- = at tests/sources/functional/enum.move:65: test_enum_vector
- = at tests/sources/functional/enum.move:9
- = at tests/sources/functional/enum.move:65: test_enum_vector
= at tests/sources/functional/enum.move:63: test_enum_vector
- = _common_vector_2 = <redacted>
+ = _common_vector_1 = <redacted>
+ = at tests/sources/functional/enum.move:67: test_enum_vector
= at tests/sources/functional/enum.move:68: test_enum_vector
+ = at tests/sources/functional/enum.move:69: test_enum_vector
+ = at tests/sources/functional/enum.move:66: test_enum_vector
+ = at tests/sources/functional/enum.move:17
+ = at tests/sources/functional/enum.move:18
+ = at tests/sources/functional/enum.move:66: test_enum_vector
+ = _common_fields = <redacted>
+ = at tests/sources/functional/enum.move:72: test_enum_vector
+ = at tests/sources/functional/enum.move:73: test_enum_vector
+ = at tests/sources/functional/enum.move:17
+ = at tests/sources/functional/enum.move:73: test_enum_vector
+ = at tests/sources/functional/enum.move:71: test_enum_vector
+ = _common_vector_2 = <redacted>
+ = at tests/sources/functional/enum.move:76: test_enum_vector