Skip to content

Commit

Permalink
fix enum bug (#15403)
Browse files Browse the repository at this point in the history
  • Loading branch information
@rahxephon89
rahxephon89 authored Nov 26, 2024
1 parent 7b69d4c commit 0029300
Show file tree
Hide file tree
Showing 4 changed files with 72 additions and 53 deletions.
7 changes: 6 additions & 1 deletion third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 = "";
Expand Down
20 changes: 13 additions & 7 deletions third_party/move/move-prover/tests/sources/functional/enum.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
8 changes: 8 additions & 0 deletions third_party/move/move-prover/tests/sources/functional/enum.move
View file
Original file line number Diff line number Diff line change
@@ -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}
Expand Down
90 changes: 45 additions & 45 deletions third_party/move/move-prover/tests/sources/functional/enum.v2_exp
View file
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 0029300

Please sign in to comment.