Skip to content

Commit

Permalink
[move-prover] type dependent code test cases
Browse files Browse the repository at this point in the history 
Existing test cases covers the situations where a type parameter is
instantiated with a concrete type `T := u8`. This commit adds two new
test cases where type dependent code can be written out of two type
parameters where `T1 := T2`.

Closes: aptos-labs#9420
  • Loading branch information
@meng-xu-cs @bors-libra
meng-xu-cs authored and bors-libra committed Oct 14, 2021
1 parent 49994f4 commit ba17245
Show file tree
Hide file tree
Showing 2 changed files with 107 additions and 29 deletions.
77 changes: 61 additions & 16 deletions language/move-prover/tests/sources/functional/type_dependent_code.exp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ error: abort not covered by any of the `aborts_if` clauses
8 │ move_to<S<u8>>(&account, S { x: 0 });
│ ------- abort happened here with execution failure
9 │ }
10 │ ╭ spec extract {
10 │ ╭ spec test1 {
11 │ │ aborts_if exists<S<X>>(Signer::address_of(account));
12 │ │ aborts_if exists<S<u8>>(Signer::address_of(account));
13 │ │
Expand All @@ -14,32 +14,77 @@ error: abort not covered by any of the `aborts_if` clauses
20 │ │ }
│ ╰─────^
│
= at tests/sources/functional/type_dependent_code.move:6: extract
= at tests/sources/functional/type_dependent_code.move:6: test1
= account = <redacted>
= x = <redacted>
= at tests/sources/functional/type_dependent_code.move:7: extract
= at tests/sources/functional/type_dependent_code.move:8: extract
= at tests/sources/functional/type_dependent_code.move:8: extract
= at tests/sources/functional/type_dependent_code.move:7: test1
= at tests/sources/functional/type_dependent_code.move:8: test1
= at tests/sources/functional/type_dependent_code.move:8: test1
= ABORTED

error: function does not abort under this condition
┌─ tests/sources/functional/type_dependent_code.move:35:9
error: abort not covered by any of the `aborts_if` clauses
┌─ tests/sources/functional/type_dependent_code.move:26:5
│
24 │ move_to<S<T2>>(&account, S { x: t2 });
│ ------- abort happened here with execution failure
25 │ }
26 │ ╭ spec test2 {
27 │ │ aborts_if exists<S<T1>>(Signer::address_of(account));
28 │ │ aborts_if exists<S<T2>>(Signer::address_of(account));
29 │ │
· │
35 │ │ // abort condition.
36 │ │ }
│ ╰─────^
│
35 │ aborts_if !exists<S<X>>(Signer::address_of(account));
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= at tests/sources/functional/type_dependent_code.move:22: test2
= account = <redacted>
= t1 = <redacted>
= t2 = <redacted>
= at tests/sources/functional/type_dependent_code.move:23: test2
= at tests/sources/functional/type_dependent_code.move:24: test2
= at tests/sources/functional/type_dependent_code.move:24: test2
= ABORTED

error: post-condition does not hold
┌─ tests/sources/functional/type_dependent_code.move:50:9
│
= at tests/sources/functional/type_dependent_code.move:28: extract
50 │ ensures global<S<u8>>(Signer::address_of(account)).x == 0;
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
= at tests/sources/functional/type_dependent_code.move:44: test1
= account = <redacted>
= x = <redacted>
= at tests/sources/functional/type_dependent_code.move:29: extract
= at tests/sources/functional/type_dependent_code.move:30: extract
= at tests/sources/functional/type_dependent_code.move:45: test1
= at tests/sources/functional/type_dependent_code.move:46: test1
= at ../move-stdlib/sources/Signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/Signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/Signer.move:14: address_of
= r = <redacted>
= at tests/sources/functional/type_dependent_code.move:47: test1
= at tests/sources/functional/type_dependent_code.move:48: test1
= at tests/sources/functional/type_dependent_code.move:50

error: post-condition does not hold
┌─ tests/sources/functional/type_dependent_code.move:66:9
│
66 │ ensures global<S<T1>>(Signer::address_of(account)).x == t1;
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
│
= at tests/sources/functional/type_dependent_code.move:58: test2
= account = <redacted>
= t1 = <redacted>
= t2 = <redacted>
= at tests/sources/functional/type_dependent_code.move:61: test2
= at tests/sources/functional/type_dependent_code.move:62: test2
= at ../move-stdlib/sources/Signer.move:12: address_of
= s = <redacted>
= at ../move-stdlib/sources/Signer.move:13: address_of
= result = <redacted>
= at ../move-stdlib/sources/Signer.move:14: address_of
= r = <redacted>
= at tests/sources/functional/type_dependent_code.move:31: extract
= at tests/sources/functional/type_dependent_code.move:32: extract
= at tests/sources/functional/type_dependent_code.move:34
= at tests/sources/functional/type_dependent_code.move:35
= at tests/sources/functional/type_dependent_code.move:63: test2
= at tests/sources/functional/type_dependent_code.move:64: test2
= at tests/sources/functional/type_dependent_code.move:66
59 changes: 46 additions & 13 deletions language/move-prover/tests/sources/functional/type_dependent_code.move
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@ module 0x42::M {

struct S<X: store> has key { x: X }

public fun extract<X: store>(account: signer, x: X) {
public fun test1<X: store>(account: signer, x: X) {
move_to<S<X>>(&account, S { x });
move_to<S<u8>>(&account, S { x: 0 });
}
spec extract {
spec test1 {
aborts_if exists<S<X>>(Signer::address_of(account));
aborts_if exists<S<u8>>(Signer::address_of(account));

Expand All @@ -18,32 +18,65 @@ module 0x42::M {
// TODO: currently we don't even have a way to specify this additional
// abort condition.
}

public fun test2<T1: store, T2: store>(account: signer, t1: T1, t2: T2) {
move_to<S<T1>>(&account, S { x: t1 });
move_to<S<T2>>(&account, S { x: t2 });
}
spec test2 {
aborts_if exists<S<T1>>(Signer::address_of(account));
aborts_if exists<S<T2>>(Signer::address_of(account));

// NOTE: besides the above aborts_if conditions, this function
// also aborts if type parameters `T1` and `T2` are the same.`
// This additional abort condition is not captured by the spec.
//
// TODO: currently we don't even have a way to specify this additional
// abort condition.
}
}

module 0x42::N {
use Std::Signer;

struct S<X: store + drop> has key { x: X }

public fun extract<X: store + drop>(account: signer, x: X) acquires S {
public fun test1<X: store + drop>(account: signer, x: X) acquires S {
move_to<S<u8>>(&account, S { x: 0 });
let r = borrow_global_mut<S<X>>(Signer::address_of(&account));
*&mut r.x = x;
}
spec extract {
aborts_if exists<S<u8>>(Signer::address_of(account));
aborts_if !exists<S<X>>(Signer::address_of(account));
spec test1 {
ensures global<S<u8>>(Signer::address_of(account)).x == 0;

// NOTE: there are two issues with the spec
// 1) the second `aborts_if` condition is necessary only when X != u8
// 2) the `ensures` condition might not hold, as `extract<u8>(_, 1)`
// will violate the `ensures` condition.
// NOTE: the `ensures` condition might not hold when `X == u8`.
//
// TODO: currently the exp file does not show that the `ensures` is
// violated, not sure whehter this is shadowed by the `aborts_if`.
// Similar to the test cases above, we also don't have a
// good way to specify these type equality conditions in spec.
}

public fun test2<T1: store + drop, T2: store + drop>(
account: signer, t1: T1, t2: T2
) acquires S {
move_to<S<T1>>(&account, S { x: t1 });
let r = borrow_global_mut<S<T2>>(Signer::address_of(&account));
*&mut r.x = t2;
}
spec test2 {
ensures global<S<T1>>(Signer::address_of(account)).x == t1;

// NOTE: the `ensures` condition might not hold when `T1 == T2`.
//
// In addition, similar to the test case above, we also don't have a
// Similar to the test cases above, we also don't have a
// good way to specify these type equality conditions in spec.
//
// Further note that in the exp files, we see two error messages
// on that this `ensures` condition is violated. This is expected.
// If we take a look at the Boogie output, we will notice three
// verification targets generated:
// - test2<#0, #1>
// - test2<#0, #0>
// - test2<#1. #1>
// The `ensures` condition does not hold in the later two cases.
}
}

0 comments on commit ba17245

Please sign in to comment.