Fix multiple apply of magic wands with quantified expressions

src/test/resources/all/heap-dependent_triggers/triggerFoldPackage.vpr

@@ -12,7 +12,7 @@ method m1(xs: Set[Ref], y: Ref, zs: Seq[Ref]) {
     assume z in zs
     assume !(z in xs)
     package acc(z.f) --* acc(y.f)
-
+    //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/000/)
     //:: ExpectedOutput(assert.failed:assertion.false)
     assert z != y
 }

src/test/resources/all/impure_assume/assume10QPwand-light.vpr

@@ -0,0 +1,25 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+field f: Int
+
+predicate p(x: Ref)
+
+method m(xs: Set[Ref], q: Perm, xs1: Set[Ref]) {
+
+  inhale none < q
+  inhale forall x: Ref :: (x in xs) ==> acc(x.f) --* acc(p(x))
+
+  assume (forall x1: Ref :: {acc(x1.f, q) --* acc(p(x1), q)} (x1 in xs1) ==> acc(x1.f, q) --* acc(p(x1), q))
+
+  var a: Ref
+
+  assume a in xs1
+
+  //:: UnexpectedOutput(assert.failed:wand.not.found, /carbon/issue/257/)
+  assert acc(a.f, q) --* acc(p(a), q)
+
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert q == write ==> false // MS: Can we expect this to hold?
+}

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

@@ -0,0 +1,35 @@
+# 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 |
+|----------------------------------------------------------------------------|-------------------------------------------------------------------------------------------------|-----------------|
+| [basic-bool.vpr](./basic-bool.vpr)                                         | Boolean Magic Wand with trivial LHS                                                             | ✓               |
+| [basic-int.vpr](./basic-int.vpr)                                           | Integer Magic Wand with trivial LHS                                                             | ✓               |
+| [basic-lhs-eq-rhs.vpr](./basic-lhs-equal-to-rhs.vpr)                             | Integer Magic Wand with LHS = RHS                                                               | ✓               |
+| [basic-lhs-lt-rhs.vpr](./basic-lhs-smaller-than-rhs.vpr)                             | Integer Magic Wand with LHS < RHS                                                               | ✓               |
+| [basic-lhs-gt-rhs.vpr](./basic-lhs-larger-than-rhs.vpr)                             | Integer Magic Wand with LHS > RHS                                                               | ✓               |
+| [applying-twice-bool.vpr](./applying-twice-bool.vpr)                       | Applying the magic wand multiple times. Original version leaks information into the outer state | ×               |
+| [assign-applying-bool.vpr](./assign-applying-bool.vpr)                     | Assigning result of applying expression to the same field using booleans                        | ×               |
+| [assign-applying-int.vpr](./assign-applying-int.vpr)                       | Assigning result of applying expression to the same field using integers                        | ×               |
+| [inhaling-magic-wand.vpr](./inhaling-magic-wand.vpr)                       | Inhaling a magic wand                                                                           | ✓               |
+| [predicates-in-magic-wands.vpr](./predicates-in-magic-wands.vpr)           | Magic wand with predicates                                                                      | ✓               |
+| [example-list.vpr](./example-list.vpr)                                     | Iterate over a List                                                                             | ✓               |
+| [applying-twice-quantified-wand.vpr](./applying-twice-quantified-wand.vpr) | Applying a quantified magic wand multiple times.                                                | ✓               |
+| [applying-twice-quantified-lhs.vpr](./applying-twice-quantified-lhs.vpr)   | Applying a magic wand multiple times with a quantified expression on the LHS.                   | ✓               |
+| [applying-twice-qp-fields.vpr](./applying-twice-qp-fields.vpr)             | Test from QPFields.vpr adapted to test some unsound behavior.                                   | ✓               |
+| [applying-twice-qp-predicates.vpr](./applying-twice-qp-predicates.vpr)     | Test from QPPredicates.vpr adapted to test some unsound behavior.                               | ✓               |
+| [quantified-magic-wands.vpr](./quantified-magic-wands.vpr)                 | Tests with quantified magic wands.                                                              | ✓               |
+| [two-fields.vpr](./two-fields.vpr)                                         | Magic wand with quantifier over two fields.                                                     | ✓               |
+
+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/QPPredicates.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPPredicates.vpr)
+* [wands/new_syntax/QPWands.vpr](https://github.com/viperproject/silver/tree/master/src/test/resources/wands/new_syntax/QPWands.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/mwsf/applying-twice-bool.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/mwsf/applying-twice-qp-fields.vpr

@@ -0,0 +1,49 @@
+field f: Int
+
+// based on test7 in QPFields.vpr
+method test14a(x: Ref)
+    requires forall y: Ref :: true ==> acc(y.f)
+{
+    package (forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))
+
+    x.f := 0
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+    x.f := 1
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+// based on test9 in QPFields.vpr
+method test14b(x: Ref)
+    requires forall y: Ref :: true ==> acc(y.f)
+{
+    package (forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)
+
+    x.f := 0
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)) in true
+    x.f := 1
+    assert applying ((forall y: Ref :: true ==> acc(y.f)) --* acc(x.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+// based on test11 in QPFields.vpr
+method test14c(x: Ref, z: Ref)
+    requires acc(x.f) && z != x
+{
+    package (forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))
+    inhale forall y: Ref :: y != x ==> acc(y.f)
+
+    assert acc(z.f)
+
+    z.f := 0
+    assert applying ((forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+    z.f := 1
+    assert applying ((forall y: Ref :: y != x ==> acc(y.f)) --* (forall y: Ref :: true ==> acc(y.f))) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}

src/test/resources/wands/mwsf/applying-twice-qp-predicates.vpr

@@ -0,0 +1,73 @@
+field f: Int
+
+predicate Cell(x: Ref) {
+    acc(x.f)
+}
+
+function get(x: Ref): Int
+    requires acc(Cell(x), 1/2)
+{
+    unfolding acc(Cell(x), 1/2) in x.f
+}
+
+// based on test7 in QPPredicates.vpr
+method test14d(x: Ref)
+    requires forall y: Ref :: true ==> Cell(y)
+{
+    package (forall y: Ref :: true ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))
+
+    unfold Cell(x)
+    x.f := 0
+    fold Cell(x)
+    assert applying ((forall y: Ref :: true ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))) in true
+
+    unfold Cell(x)
+    x.f := 1
+    fold Cell(x)
+    assert applying ((forall y: Ref :: true ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+// based on test9 in QPPredicates.vpr
+method test14e(x: Ref)
+    requires forall y: Ref :: true ==> Cell(y)
+{
+    package (forall y: Ref :: true ==> Cell(y)) --* Cell(x)
+
+    unfold Cell(x)
+    x.f := 0
+    fold Cell(x)
+    assert applying ((forall y: Ref :: true ==> Cell(y)) --* Cell(x)) in true
+
+    unfold Cell(x)
+    x.f := 1
+    fold Cell(x)
+    assert applying ((forall y: Ref :: true ==> Cell(y)) --* Cell(x)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+// based on test11 in QPPredicates.vpr
+method test14f(x: Ref, z: Ref)
+    requires Cell(x)
+    requires x != z
+{
+    package (forall y: Ref :: y != x ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))
+    inhale forall y: Ref :: y != x ==> Cell(y)
+
+    unfold Cell(z)
+    z.f := 0
+    fold Cell(z)
+    assert applying ((forall y: Ref :: y != x ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))) in true
+
+    unfold Cell(z)
+    z.f := 1
+    fold Cell(z)
+    assert applying ((forall y: Ref :: y != x ==> Cell(y)) --* (forall y: Ref :: true ==> Cell(y))) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}

src/test/resources/wands/mwsf/applying-twice-quantified-lhs.vpr

@@ -0,0 +1,85 @@
+field f: Int
+
+method test13a(xs: Seq[Ref])
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package (forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)
+
+    some.f := 1
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
+
+    some.f := 2
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test13b(xs: Seq[Ref])
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package (forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)
+
+    some.f := 1
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
+
+    some.f := 2
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> (forall x: Ref :: x in xs ==> acc(x.f)) --* acc(z.f)
+}
+
+method test13c(xs: Seq[Ref], y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+    requires acc(y.f)
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package (forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)
+
+    some.f := 1
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
+
+    some.f := 2
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}
+
+method test13d(xs: Seq[Ref], y: Ref)
+    requires forall x: Ref :: x in xs ==> acc(x.f)
+    requires |xs| >= 1
+    requires acc(y.f)
+{
+    xs[0].f := 0
+    var some: Ref := xs[0]
+
+    package (forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)
+
+    some.f := 1
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
+
+    some.f := 2
+    assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+
+    var completed: Seq[Ref] := Seq(some)
+    assert forall z: Ref :: z in completed ==> (forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(z.f) && acc(y.f)
+}