Test suite for magic wand snap functions.

src/test/resources/wands/snap_functions/README.md

@@ -0,0 +1,28 @@
+# Test Suite for Magic Wand Snap Functions
+
+This folder contains Viper test files that I used when working on MagicWandSnapFunctions for the Silicon project.
+
+## Overview
+
+| Name                       | Description                                                                                     | Expected Result |
+|----------------------------|-------------------------------------------------------------------------------------------------|-----------------|
+| [test01.vpr](./test01.vpr) | Boolean Magic Wand with trivial LHS                                                             | ✓               |
+| [test02.vpr](./test02.vpr) | Integer Magic Wand with trivial LHS                                                             | ✓               |
+| [test03.vpr](./test03.vpr) | Integer Magic Wand with LHS = RHS                                                               | ✓               |
+| [test04.vpr](./test04.vpr) | Integer Magic Wand with LHS < RHS                                                               | ✓               |
+| [test05.vpr](./test05.vpr) | Integer Magic Wand with LHS > RHS                                                               | ✓               |
+| [test06.vpr](./test06.vpr) | Applying the magic wand multiple times. Original version leaks information into the outer state | ×               |
+| [test07.vpr](./test07.vpr) | Assigning result of applying expression to the same field using booleans                        | ×               |
+| [test08.vpr](./test08.vpr) | Assigning result of applying expression to the same field using integers                        | ×               |
+| [test09.vpr](./test09.vpr) | Inhaling a magic wand                                                                           | ✓               |
+| [test10.vpr](./test10.vpr) | Magic wand with predicates                                                                      | ✓               |
+| [test11.vpr](./test11.vpr) | Iterate over a List                                                                             | ✓               |
+| [test12.vpr](./test12.vpr) | Applying a quantified magic wand multiple times. Original version verifies this unsoundly       | ✓               |
+
+Other interesting test cases in the [Silver repository](https://github.com/viperproject/silver/tree/master/src/test/resources) during the development of `MagicWandSnapFunctions` were:
+* [wands/examples_paper/conditionals.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/examples_paper/conditionals.vpr)
+* [wands/new_syntax/QPFields.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPFields.vpr)
+* [wands/new_syntax/SnapshotsNestedMagicWands.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/SnapshotsNestedMagicWands.vpr)
+* [wands/regression/conditionals2.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/conditionals2.vpr)
+* [wands/regression/issue024.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue024.vpr)
+* [wands/regression/issue029.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/regression/issue029.vpr)

src/test/resources/wands/snap_functions/test01.vpr

@@ -0,0 +1,50 @@
+field b: Bool
+
+method test01a(x: Ref)
+{
+    inhale acc(x.b) && x.b
+
+    package true --* acc(x.b)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    assert applying (true --* acc(x.b)) in x.b
+}
+
+method test01b(x: Ref)
+{
+    inhale acc(x.b) && x.b
+
+    package true --* acc(x.b)
+
+    apply true --* acc(x.b)
+
+    assert x.b
+}
+
+method test01c(x: Ref)
+{
+    inhale acc(x.b) && x.b
+
+    package true --* acc(x.b)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    assert applying (true --* acc(x.b)) in x.b
+
+    apply true --* acc(x.b)
+
+    assert x.b
+}
+
+method test01d(x: Ref, a: Bool)
+{
+    inhale acc(x.b) && x.b == a
+
+    package true --* acc(x.b)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    assert applying (true --* acc(x.b)) in x.b == a
+
+    apply true --* acc(x.b)
+
+    assert x.b == a
+}

src/test/resources/wands/snap_functions/test02.vpr

@@ -0,0 +1,50 @@
+field f: Int
+
+method test02a(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package true --* acc(x.f)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    assert applying (true --* acc(x.f)) in x.f == 42
+}
+
+method test02b(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package true --* acc(x.f)
+
+    apply true --* acc(x.f)
+
+    assert x.f == 42
+}
+
+method test02c(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package true --* acc(x.f)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    assert applying (true --* acc(x.f)) in x.f == 42
+
+    apply true --* acc(x.f)
+
+    assert x.f == 42
+}
+
+method test02d(x: Ref, a: Int)
+{
+    inhale acc(x.f) && x.f == a
+
+    package true --* acc(x.f)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    assert applying (true --* acc(x.f)) in x.f == a
+
+    apply true --* acc(x.f)
+
+    assert x.f == a
+}

src/test/resources/wands/snap_functions/test03.vpr

@@ -0,0 +1,47 @@
+field f: Int
+
+method test03a(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package acc(x.f) --* acc(x.f)
+
+    assert applying (acc(x.f) --* acc(x.f)) in x.f == 42
+}
+
+method test03b(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package acc(x.f) --* acc(x.f)
+
+    apply acc(x.f) --* acc(x.f)
+
+    assert x.f == 42
+}
+
+method test03c(x: Ref)
+{
+    inhale acc(x.f) && x.f == 42
+
+    package acc(x.f) --* acc(x.f)
+
+    assert applying (acc(x.f) --* acc(x.f)) in x.f == 42
+
+    apply acc(x.f) --* acc(x.f)
+
+    assert x.f == 42
+}
+
+method test03d(x: Ref, a: Int)
+{
+    inhale acc(x.f) && x.f == a
+
+    package acc(x.f) --* acc(x.f)
+
+    assert applying (acc(x.f) --* acc(x.f)) in x.f == a
+
+    apply acc(x.f) --* acc(x.f)
+
+    assert x.f == a
+}

src/test/resources/wands/snap_functions/test04.vpr

@@ -0,0 +1,50 @@
+field f: Int
+
+method test04a(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) --* acc(x.f) && acc(y.f)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == 42 && y.f == 37
+}
+
+method test04b(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) --* acc(x.f) && acc(y.f)
+
+    apply acc(x.f) --* acc(x.f) && acc(y.f)
+
+    assert x.f == 42 && y.f == 37
+}
+
+method test04c(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) --* acc(x.f) && acc(y.f)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == 42 && y.f == 37
+
+    apply acc(x.f) --* acc(x.f) && acc(y.f)
+
+    assert x.f == 42 && y.f == 37
+}
+
+method test04d(x: Ref, y: Ref, a: Int, b: Int)
+{
+    inhale acc(x.f) && x.f == a && acc(y.f) && y.f == b
+
+    package acc(x.f) --* acc(x.f) && acc(y.f)
+
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    assert applying (acc(x.f) --* acc(x.f) && acc(y.f)) in x.f == a && y.f == b
+
+    apply acc(x.f) --* acc(x.f) && acc(y.f)
+
+    assert x.f == a && y.f == b
+}

src/test/resources/wands/snap_functions/test05.vpr

@@ -0,0 +1,47 @@
+field f: Int
+
+method test05a(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert (applying (acc(x.f) && acc(y.f) --* acc(x.f)) in x.f == 42) && y.f == 37
+}
+
+method test05b(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) && acc(y.f) --* acc(x.f)
+
+    apply acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert x.f == 42 && acc(y.f, none)
+}
+
+method test05c(x: Ref, y: Ref)
+{
+    inhale acc(x.f) && x.f == 42 && acc(y.f) && y.f == 37
+
+    package acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert (applying (acc(x.f) && acc(y.f) --* acc(x.f)) in x.f == 42) && y.f == 37
+
+    apply acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert x.f == 42 && acc(y.f, none)
+}
+
+method test05d(x: Ref, y: Ref, a: Int, b: Int)
+{
+    inhale acc(x.f) && x.f == a && acc(y.f) && y.f == b
+
+    package acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert (applying (acc(x.f) && acc(y.f) --* acc(x.f)) in x.f == a) && y.f == b
+
+    apply acc(x.f) && acc(y.f) --* acc(x.f)
+
+    assert x.f == a && acc(y.f, none)
+}

src/test/resources/wands/snap_functions/test06.vpr

@@ -0,0 +1,16 @@
+field b: Bool
+
+method test06(x: Ref) {
+    inhale acc(x.b)
+
+    package acc(x.b) --* true
+
+    x.b := true
+    assert applying (acc(x.b) --* true) in true
+
+    x.b := false
+    assert applying (acc(x.b) --* true) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}

src/test/resources/wands/snap_functions/test07.vpr

@@ -0,0 +1,16 @@
+field b: Bool
+
+method test07a(x: Ref)
+    requires acc(x.b)
+{
+    package acc(x.b) --* acc(x.b)
+
+    x.b := applying (acc(x.b) --* acc(x.b)) in !x.b
+
+    apply acc(x.b) --* acc(x.b)
+
+    assert acc(x.b) && x.b != old(x.b)
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}

src/test/resources/wands/snap_functions/test08.vpr

@@ -0,0 +1,29 @@
+field f: Int
+
+method test08a(x: Ref)
+    requires acc(x.f)
+{
+    package acc(x.f) --* acc(x.f)
+
+    x.f := applying (acc(x.f) --* acc(x.f)) in x.f + 1
+
+    apply acc(x.f) --* acc(x.f)
+
+    assert acc(x.f) && x.f == old(x.f) + 1
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test08b(x: Ref)
+    requires acc(x.f) && x.f == 42
+{
+    package acc(x.f) --* acc(x.f)
+
+    x.f := applying (acc(x.f) --* acc(x.f)) in x.f + 1
+
+    apply acc(x.f) --* acc(x.f)
+
+    assert acc(x.f) && x.f == 43
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}

src/test/resources/wands/snap_functions/test09.vpr

@@ -0,0 +1,27 @@
+field f: Int
+
+method test09a(x: Ref, y: Ref)
+    requires acc(x.f) && x.f == 42
+    requires acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37
+{
+    //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/)
+    assert applying (acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37) in y.f == 37
+}
+
+method test09b(x: Ref, y: Ref)
+    requires acc(x.f) && x.f == 42
+    requires acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37
+{
+    apply acc(x.f) --* acc(x.f) && acc(y.f) && y.f == 37
+
+    assert y.f == 37
+}
+
+method test09c(x: Ref, y: Ref, z: Ref)
+    requires acc(x.f) && x.f == 42
+    requires acc(x.f) --* acc(x.f) && acc(y.f) && acc(z.f) && y.f == 37
+{
+    apply acc(x.f) --* acc(x.f) && acc(y.f) && acc(z.f) && y.f == 37
+
+    assert y.f == 37
+}