-
Notifications
You must be signed in to change notification settings - Fork 3.7k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[Prover] add support of abort in spec function (#14939)
* [single-node-performance] Add runner information in the output (#14932) * [single-node-performance] Add runner information in the output * adding skip move e2e * recalibration * add support of abort when in spec --------- Co-authored-by: igor-aptos <[email protected]>
- Loading branch information
1 parent
8b7aee1
commit d2eaddb
Showing
11 changed files
with
242 additions
and
15 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
121 changes: 121 additions & 0 deletions
121
third_party/move/move-prover/tests/sources/functional/abort_in_fun.move
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,121 @@ | ||
| module 0x42::TestAbortInFunction { | ||
|
|
||
| fun aborts_with(x: u64, y: u64): u64 { | ||
| if (x == 1) { | ||
| abort 2 | ||
| } else if (y == 2) { | ||
| abort 3 | ||
| } else { | ||
| x | ||
| } | ||
| } | ||
| spec aborts_with { | ||
| aborts_if x == 1 with 2; | ||
| aborts_if y == 2 with 3; | ||
| ensures result == x; | ||
| } | ||
|
|
||
| fun call_aborts_with(): u64 { | ||
| aborts_with(2, 3) | ||
| } | ||
|
|
||
| spec call_aborts_with { | ||
| ensures result == aborts_with(2, 3); | ||
| } | ||
|
|
||
| fun abort_generic<Element: copy + drop>(x: Element, y: Element): Element { | ||
| if (x == y) { | ||
| abort 0 | ||
| } else { | ||
| x | ||
| } | ||
| } | ||
|
|
||
| fun call_aborts_generic(): u64 { | ||
| abort_generic(2, 3) | ||
| } | ||
|
|
||
| spec call_aborts_generic { | ||
| ensures result == abort_generic(2, 3); | ||
| } | ||
|
|
||
| struct S<Element: copy + drop> has copy, drop { | ||
| value: Element | ||
| } | ||
|
|
||
| fun abort_generic_struct<Element: copy + drop>(x: S<Element>, y: S<Element>): S<Element> { | ||
| if (x == y) { | ||
| abort 0 | ||
| } else { | ||
| x | ||
| } | ||
| } | ||
|
|
||
| fun spec_abort_generic_struct<Element: copy + drop>(x: S<Element>, y: S<Element>): S<Element> { | ||
| if (x == y) { | ||
| abort 0 | ||
| } else { | ||
| x | ||
| } | ||
| } | ||
|
|
||
| fun call_abort_generic_struct<Element: copy + drop>(x: Element, y: Element): Element { | ||
| let sx = S { | ||
| value: x | ||
| }; | ||
| let sy = S { | ||
| value: y | ||
| }; | ||
| abort_generic_struct(sx, sy).value | ||
| } | ||
|
|
||
| spec call_abort_generic_struct { | ||
| aborts_if x == y; | ||
| ensures result == call_abort_generic_struct(x, y); | ||
| } | ||
|
|
||
| struct T has copy, drop { | ||
| v: u64 | ||
| } | ||
|
|
||
| spec T { | ||
| pragma bv=b"0"; | ||
| } | ||
|
|
||
| fun call_abort_generic_struct_concrete(x: u64, y: u64, test_assert1: bool): T { | ||
| let sx = S { | ||
| value: T { | ||
| v: x | ||
| } | ||
| }; | ||
| let sy = S { | ||
| value: T { | ||
| v: y | ||
| } | ||
| }; | ||
| assert!(test_assert1, 0); | ||
| abort_generic_struct(sx, sy).value | ||
| } | ||
|
|
||
| spec call_abort_generic_struct_concrete { | ||
| aborts_if x == y; | ||
| aborts_if !test_assert1; | ||
| ensures result == call_abort_generic_struct_concrete(x, y, test_assert1); | ||
| ensures result == spec_call_abort_generic_struct_concrete(x, y); | ||
| } | ||
|
|
||
| spec fun spec_call_abort_generic_struct_concrete(x: u64, y: u64): T { | ||
| let sx = S { | ||
| value: T { | ||
| v: x | ||
| } | ||
| }; | ||
| let sy = S { | ||
| value: T { | ||
| v: y | ||
| } | ||
| }; | ||
| spec_abort_generic_struct(sx, sy).value | ||
| } | ||
|
|
||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
13 changes: 13 additions & 0 deletions
13
third_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.exp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| Move prover returns: exiting with condition generation errors | ||
| error: imperative expressions not supported in specs | ||
| ┌─ tests/sources/functional/spec_fun_imperative_expression_err.move:2:27 | ||
| │ | ||
| 2 │ fun sequential(): u64 { | ||
| │ ╭───────────────────────────^ | ||
| 3 │ │ let _x = 2; | ||
| 4 │ │ let _y = 3; | ||
| 5 │ │ while(_y > 0) { | ||
| · │ | ||
| 16 │ │ _x | ||
| 17 │ │ } | ||
| │ ╰─────^ |
26 changes: 26 additions & 0 deletions
26
...d_party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.move
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,26 @@ | ||
| module 0x42::M { | ||
| fun sequential(): u64 { | ||
| let _x = 2; | ||
| let _y = 3; | ||
| while(_y > 0) { | ||
| break | ||
| }; | ||
| if (_x > 0) { | ||
| abort(0) | ||
| }; | ||
| let _z = if (_x > 5) { | ||
| _x | ||
| } else { | ||
| _y | ||
| }; | ||
| _x | ||
| } | ||
|
|
||
| fun m() { | ||
| let _z = 2; | ||
| spec { | ||
| assert _z == sequential(); | ||
| }; | ||
| } | ||
|
|
||
| } |
13 changes: 13 additions & 0 deletions
13
...party/move/move-prover/tests/sources/functional/spec_fun_imperative_expression_err.v2_exp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| Move prover returns: exiting with condition generation errors | ||
| error: imperative expressions not supported in specs | ||
| ┌─ tests/sources/functional/spec_fun_imperative_expression_err.move:2:27 | ||
| │ | ||
| 2 │ fun sequential(): u64 { | ||
| │ ╭───────────────────────────^ | ||
| 3 │ │ let _x = 2; | ||
| 4 │ │ let _y = 3; | ||
| 5 │ │ while(_y > 0) { | ||
| · │ | ||
| 16 │ │ _x | ||
| 17 │ │ } | ||
| │ ╰─────^ |