search

move-language / move

Apache License 2.0
2.26k stars 688 forks source link

[Move Prover] Move prover returns: cannot extract version from `Users/username/.dotnet/tools/boogie` #534

Open junkil-park opened 2 years ago

junkil-park commented 2 years ago

Boogie version: 2.15.8 Z3 version: 4.11.0

When performing cargo test -p move-prover --release, Prover sometimes (non-deterministically, not all the times) terminates with the following error:

Move prover returns: cannot extract version from `Users/username/.dotnet/tools/boogie`

Edited:

Also Prover sometimes produces the following this error:

+ Move prover returns: Boogie error (signal: 5 (SIGTRAP)):

In one occasion: 

test prover unit[cvc5]::functional/disable_inv_friends.move ... FAILED
Error:
New output differs from baseline!
Call this test with env variable UPBL=1 to regenerate or remove old baseline files.
Then use your favorite changelist diff tool to verify you are good with the changes.

Or check the rudimentary diff below:

- Move prover returns: exiting with verification errors
- error: global memory invariant does not hold
-    ┌─ tests/sources/functional/disable_inv_friends.move:25:10
-    │
- 25 │          invariant [global, suspendable] forall addr: address: exists<M3::R3>(addr) <==> exists<M2::R2>(addr);
-    │          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-    │
-    =     at tests/sources/functional/disable_inv_friends.move:85: f5_incorrect
-    =     at tests/sources/functional/disable_inv_friends.move:91: f5_incorrect (spec)
-    =     at tests/sources/functional/disable_inv_friends.move:92: f5_incorrect (spec)
-    =     at tests/sources/functional/disable_inv_friends.move:85: f5_incorrect
-    =         s = <redacted>
-    =     at tests/sources/functional/disable_inv_friends.move:86: f5_incorrect
-    =     at tests/sources/functional/disable_inv_friends.move:25
+ Move prover returns: cannot extract version from `/Users/username/.dotnet/tools/boogie`

In another occasion:

test prover unit[default]::functional/aborts_if.move ... FAILED
Error:
New output differs from baseline!
Call this test with env variable UPBL=1 to regenerate or remove old baseline files.
Then use your favorite changelist diff tool to verify you are good with the changes.

Or check the rudimentary diff below:

- Move prover returns: exiting with verification errors
- error: function does not abort under this condition
-    ┌─ tests/sources/functional/aborts_if.move:35:9
-    │
- 35 │         aborts_if _x <= _y;
-    │         ^^^^^^^^^^^^^^^^^^^
-    │
-    =     at tests/sources/functional/aborts_if.move:32: abort2_incorrect
-    =         _x = <redacted>
-    =         _y = <redacted>
-    =     at tests/sources/functional/aborts_if.move:33: abort2_incorrect
-    =     at tests/sources/functional/aborts_if.move:35: abort2_incorrect (spec)
-
- error: function does not abort under this condition
-    ┌─ tests/sources/functional/aborts_if.move:52:9
-    │
- 52 │         aborts_if x <= y;
-    │         ^^^^^^^^^^^^^^^^^
-    │
-    =     at tests/sources/functional/aborts_if.move:47: abort4_incorrect
-    =         x = <redacted>
-    =         y = <redacted>
-    =     at tests/sources/functional/aborts_if.move:48: abort4_incorrect
-    =     at tests/sources/functional/aborts_if.move:49: abort4_incorrect
-    =     at tests/sources/functional/aborts_if.move:52: abort4_incorrect (spec)
-
- error: abort not covered by any of the `aborts_if` clauses
-    ┌─ tests/sources/functional/aborts_if.move:59:5
-    │
- 57 │           if (x <= y) abort 1
-    │                       ------- abort happened here with code 0x1
- 58 │       }
- 59 │ ╭     spec abort5_incorrect {
- 60 │ │         aborts_if x < y;
- 61 │ │     }
-    │ ╰─────^
-    │
-    =     at tests/sources/functional/aborts_if.move:56: abort5_incorrect
-    =         x = <redacted>
-    =         y = <redacted>
-    =     at tests/sources/functional/aborts_if.move:57: abort5_incorrect
-    =         ABORTED
-
- error: function does not abort under this condition
-    ┌─ tests/sources/functional/aborts_if.move:68:9
-    │
- 68 │         aborts_if x <= y;
-    │         ^^^^^^^^^^^^^^^^^
-    │
-    =     at tests/sources/functional/aborts_if.move:64: abort6_incorrect
-    =         x = <redacted>
-    =         y = <redacted>
-    =     at tests/sources/functional/aborts_if.move:65: abort6_incorrect
-    =     at tests/sources/functional/aborts_if.move:66: abort6_incorrect
-    =     at tests/sources/functional/aborts_if.move:68: abort6_incorrect (spec)
-
- error: function does not abort under this condition
-     ┌─ tests/sources/functional/aborts_if.move:151:9
-     │
- 151 │         aborts_if x == 4;
-     │         ^^^^^^^^^^^^^^^^^
-     │
-     =     at tests/sources/functional/aborts_if.move:145: abort_at_2_or_3_spec_incorrect
-     =         x = <redacted>
-     =     at tests/sources/functional/aborts_if.move:146: abort_at_2_or_3_spec_incorrect
-     =     at tests/sources/functional/aborts_if.move:147: abort_at_2_or_3_spec_incorrect
-     =     at tests/sources/functional/aborts_if.move:151: abort_at_2_or_3_spec_incorrect (spec)
-
- error: abort not covered by any of the `aborts_if` clauses
-     ┌─ tests/sources/functional/aborts_if.move:157:5
-     │
- 155 │           if (x == 2 || x == 3) abort 1;
-     │                                 ------- abort happened here with code 0x1
- 156 │       }
- 157 │ ╭     spec abort_at_2_or_3_strict_incorrect {
- 158 │ │         // When the strict mode is enabled, no aborts_if clause means aborts_if false.
- 159 │ │         pragma aborts_if_is_strict = true;
- 160 │ │     }
-     │ ╰─────^
-     │
-     =     at tests/sources/functional/aborts_if.move:154: abort_at_2_or_3_strict_incorrect
-     =         x = <redacted>
-     =     at tests/sources/functional/aborts_if.move:155: abort_at_2_or_3_strict_incorrect
-     =         ABORTED
-
- error: abort not covered by any of the `aborts_if` clauses
-     ┌─ tests/sources/functional/aborts_if.move:139:5
-     │
- 137 │           if (x == 2 || x == 3) abort 1;
-     │                                 ------- abort happened here with code 0x1
- 138 │       }
- 139 │ ╭     spec abort_at_2_or_3_total_incorrect {
- 140 │ │         // Counter check that we get an error message without the pragma.
- 141 │ │         // pragma aborts_if_is_partial = false;  // default
- 142 │ │         aborts_if x == 2;
- 143 │ │     }
-     │ ╰─────^
-     │
-     =     at tests/sources/functional/aborts_if.move:136: abort_at_2_or_3_total_incorrect
-     =         x = <redacted>
-     =     at tests/sources/functional/aborts_if.move:137: abort_at_2_or_3_total_incorrect
-     =         ABORTED
-
- error: function does not abort under this condition
-    ┌─ tests/sources/functional/aborts_if.move:91:9
-    │
- 91 │         aborts_if x == y;
-    │         ^^^^^^^^^^^^^^^^^
-    │
-    =     at tests/sources/functional/aborts_if.move:86: multi_abort2_incorrect
-    =         x = <redacted>
-    =         y = <redacted>
-    =     at tests/sources/functional/aborts_if.move:87: multi_abort2_incorrect
-    =     at tests/sources/functional/aborts_if.move:88: multi_abort2_incorrect
-    =     at tests/sources/functional/aborts_if.move:90: multi_abort2_incorrect (spec)
-    =     at tests/sources/functional/aborts_if.move:91: multi_abort2_incorrect (spec)
-
- error: abort not covered by any of the `aborts_if` clauses
-     ┌─ tests/sources/functional/aborts_if.move:98:5
-     │
-  96 │           abort 1
-     │           ------- abort happened here with code 0x1
-  97 │       }
-  98 │ ╭     spec multi_abort3_incorrect {
-  99 │ │         aborts_if _x < _y;
- 100 │ │         aborts_if _x == _y;
- 101 │ │     }
-     │ ╰─────^
-     │
-     =     at tests/sources/functional/aborts_if.move:95: multi_abort3_incorrect
-     =         _x = <redacted>
-     =         _y = <redacted>
-     =     at tests/sources/functional/aborts_if.move:96: multi_abort3_incorrect
-     =         ABORTED
-
- error: function does not abort under this condition
-     ┌─ tests/sources/functional/aborts_if.move:119:9
-     │
- 119 │         aborts_if true;
-     │         ^^^^^^^^^^^^^^^
-     │
-     =     at tests/sources/functional/aborts_if.move:113: multi_abort5_incorrect
-     =         x = <redacted>
-     =     at tests/sources/functional/aborts_if.move:114: multi_abort5_incorrect
-     =     at tests/sources/functional/aborts_if.move:117: multi_abort5_incorrect
-     =     at tests/sources/functional/aborts_if.move:119: multi_abort5_incorrect (spec)
+ Move prover returns: cannot extract version from `/Users/username/.dotnet/tools/boogie`

In yet another occasion:

test prover unit[cvc5]::functional/strong_edges.move ... FAILED
Error:
New output differs from baseline!
Call this test with env variable UPBL=1 to regenerate or remove old baseline files.
Then use your favorite changelist diff tool to verify you are good with the changes.

Or check the rudimentary diff below:

- Move prover returns: exiting with verification errors
- error: post-condition does not hold
-    ┌─ tests/sources/functional/strong_edges.move:54:9
-    │
- 54 │         ensures global<S>(addr).x == 3;
-    │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-    │
-    =     at tests/sources/functional/strong_edges.move:47: glob_and_field_edges_incorrect
-    =     at tests/sources/functional/strong_edges.move:56: glob_and_field_edges_incorrect (spec)
-    =     at tests/sources/functional/strong_edges.move:47: glob_and_field_edges_incorrect
-    =         addr = <redacted>
-    =     at tests/sources/functional/strong_edges.move:48: glob_and_field_edges_incorrect
-    =         s = <redacted>
-    =     at tests/sources/functional/strong_edges.move:49: glob_and_field_edges_incorrect
-    =     at tests/sources/functional/strong_edges.move:50: glob_and_field_edges_incorrect
-    =     at tests/sources/functional/strong_edges.move:55: glob_and_field_edges_incorrect (spec)
-    =     at tests/sources/functional/strong_edges.move:54: glob_and_field_edges_incorrect (spec)
+ Move prover returns: Boogie error (signal: 5 (SIGTRAP)):
=
- error: unknown assertion failed
-    ┌─ tests/sources/functional/strong_edges.move:64:13
-    │
- 64 │             assert r == 5;
-    │             ^^^^^^^^^^^^^^
-    │
-    =     at tests/sources/functional/strong_edges.move:60: loc__edge_incorrect
-    =         r = <redacted>
-    =     at tests/sources/functional/strong_edges.move:61: loc__edge_incorrect
-    =         r_ref = <redacted>
-    =     at tests/sources/functional/strong_edges.move:62: loc__edge_incorrect
-    =         r = <redacted>
-    =     at tests/sources/functional/strong_edges.move:64: loc__edge_incorrect
wrwg commented 2 years ago

In order to diagnose, we should probably modify the code which prints cannot extract version to be a bit more detailed. Does the version pattern not match? Or did boogie crash (like with this SIGTRAP). To mitigate we could loop 3 times or so and try again.

meng-xu-cs commented 2 years ago

SIGTRAP usually indicates there are some memory error (undefined behavior) in Boogie. A typical case of getting SIGTRAP is like:

string getName() {
  printf("Hello World!");
  // I forgot to return a string and the compiler might return garbage.
};

Looping will help with it.

wrwg commented 2 years ago

SIGTRAP usually indicates there are some memory error (undefined behavior) in Boogie. A typical case of getting SIGTRAP is like:

string getName() {
  printf("Hello World!");
  // I forgot to return a string and the compiler might return garbage.
};

Looping will help with it.

C# should not result in this because of the managed runtime. I'm afraid it might be a bug in the .Net runtime.