From 2f700d3d5eb143ba15811e1d37afa7c49ff49f25 Mon Sep 17 00:00:00 2001 From: Manuel Dublanc <19774382+manud99@users.noreply.github.com> Date: Mon, 13 May 2024 11:53:59 +0200 Subject: [PATCH 1/3] Add test suite that I used while developing magic wand snap functions. --- .../resources/wands/snap_functions/README.md | 27 ++++++ .../resources/wands/snap_functions/test01.vpr | 47 ++++++++++ .../resources/wands/snap_functions/test02.vpr | 47 ++++++++++ .../resources/wands/snap_functions/test03.vpr | 47 ++++++++++ .../resources/wands/snap_functions/test04.vpr | 47 ++++++++++ .../resources/wands/snap_functions/test05.vpr | 47 ++++++++++ .../resources/wands/snap_functions/test06.vpr | 16 ++++ .../resources/wands/snap_functions/test07.vpr | 16 ++++ .../resources/wands/snap_functions/test08.vpr | 29 +++++++ .../resources/wands/snap_functions/test09.vpr | 26 ++++++ .../resources/wands/snap_functions/test10.vpr | 30 +++++++ .../resources/wands/snap_functions/test11.vpr | 87 +++++++++++++++++++ 12 files changed, 466 insertions(+) create mode 100644 src/test/resources/wands/snap_functions/README.md create mode 100644 src/test/resources/wands/snap_functions/test01.vpr create mode 100644 src/test/resources/wands/snap_functions/test02.vpr create mode 100644 src/test/resources/wands/snap_functions/test03.vpr create mode 100644 src/test/resources/wands/snap_functions/test04.vpr create mode 100644 src/test/resources/wands/snap_functions/test05.vpr create mode 100644 src/test/resources/wands/snap_functions/test06.vpr create mode 100644 src/test/resources/wands/snap_functions/test07.vpr create mode 100644 src/test/resources/wands/snap_functions/test08.vpr create mode 100644 src/test/resources/wands/snap_functions/test09.vpr create mode 100644 src/test/resources/wands/snap_functions/test10.vpr create mode 100644 src/test/resources/wands/snap_functions/test11.vpr diff --git a/src/test/resources/wands/snap_functions/README.md b/src/test/resources/wands/snap_functions/README.md new file mode 100644 index 000000000..a3305229c --- /dev/null +++ b/src/test/resources/wands/snap_functions/README.md @@ -0,0 +1,27 @@ +# 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 | ✓ | + +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) diff --git a/src/test/resources/wands/snap_functions/test01.vpr b/src/test/resources/wands/snap_functions/test01.vpr new file mode 100644 index 000000000..5aba1313c --- /dev/null +++ b/src/test/resources/wands/snap_functions/test01.vpr @@ -0,0 +1,47 @@ +field b: Bool + +method test01a(x: Ref) +{ + inhale acc(x.b) && x.b + + package true --* acc(x.b) + + 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) + + 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) + + assert applying (true --* acc(x.b)) in x.b == a + + apply true --* acc(x.b) + + assert x.b == a +} \ No newline at end of file diff --git a/src/test/resources/wands/snap_functions/test02.vpr b/src/test/resources/wands/snap_functions/test02.vpr new file mode 100644 index 000000000..7c9e6d792 --- /dev/null +++ b/src/test/resources/wands/snap_functions/test02.vpr @@ -0,0 +1,47 @@ +field f: Int + +method test02a(x: Ref) +{ + inhale acc(x.f) && x.f == 42 + + package true --* acc(x.f) + + 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) + + 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) + + assert applying (true --* acc(x.f)) in x.f == a + + apply true --* acc(x.f) + + assert x.f == a +} \ No newline at end of file diff --git a/src/test/resources/wands/snap_functions/test03.vpr b/src/test/resources/wands/snap_functions/test03.vpr new file mode 100644 index 000000000..e673a5984 --- /dev/null +++ b/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 +} \ No newline at end of file diff --git a/src/test/resources/wands/snap_functions/test04.vpr b/src/test/resources/wands/snap_functions/test04.vpr new file mode 100644 index 000000000..91cc63212 --- /dev/null +++ b/src/test/resources/wands/snap_functions/test04.vpr @@ -0,0 +1,47 @@ +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) + + 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) + + 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) + + 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 +} \ No newline at end of file diff --git a/src/test/resources/wands/snap_functions/test05.vpr b/src/test/resources/wands/snap_functions/test05.vpr new file mode 100644 index 000000000..3ce73962d --- /dev/null +++ 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) +} \ No newline at end of file diff --git a/src/test/resources/wands/snap_functions/test06.vpr b/src/test/resources/wands/snap_functions/test06.vpr new file mode 100644 index 000000000..2b666f1d6 --- /dev/null +++ b/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 +} diff --git a/src/test/resources/wands/snap_functions/test07.vpr b/src/test/resources/wands/snap_functions/test07.vpr new file mode 100644 index 000000000..f5c07ae7d --- /dev/null +++ b/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 +} diff --git a/src/test/resources/wands/snap_functions/test08.vpr b/src/test/resources/wands/snap_functions/test08.vpr new file mode 100644 index 000000000..7a9185b0f --- /dev/null +++ b/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 +} diff --git a/src/test/resources/wands/snap_functions/test09.vpr b/src/test/resources/wands/snap_functions/test09.vpr new file mode 100644 index 000000000..04698b8a4 --- /dev/null +++ b/src/test/resources/wands/snap_functions/test09.vpr @@ -0,0 +1,26 @@ +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 +{ + 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 +} diff --git a/src/test/resources/wands/snap_functions/test10.vpr b/src/test/resources/wands/snap_functions/test10.vpr new file mode 100644 index 000000000..843193945 --- /dev/null +++ b/src/test/resources/wands/snap_functions/test10.vpr @@ -0,0 +1,30 @@ +field f: Int +field g: Int + +predicate foo(x: Ref) { + acc(x.f) +} + +method test10a(x: Ref) +{ + inhale foo(x) && unfolding foo(x) in x.f == 42 + + package foo(x) --* foo(x) + + apply foo(x) --* foo(x) + + assert foo(x) && unfolding foo(x) in x.f == 42 +} + +method test10b(x: Ref) +{ + inhale acc(x.f) && x.f == 42 + + package acc(x.f) --* foo(x) { + fold foo(x) + } + + apply acc(x.f) --* foo(x) + + assert foo(x) && unfolding foo(x) in x.f == 42 +} diff --git a/src/test/resources/wands/snap_functions/test11.vpr b/src/test/resources/wands/snap_functions/test11.vpr new file mode 100644 index 000000000..8fa3f95e2 --- /dev/null +++ b/src/test/resources/wands/snap_functions/test11.vpr @@ -0,0 +1,87 @@ +field next : Ref +field val : Int + +predicate List(start : Ref) +{ + acc(start.val) && acc(start.next) && (start.next != null ==> List(start.next)) +} + +function elems(start: Ref) : Seq[Int] + requires List(start) +{ + unfolding List(start) in ( + (start.next == null ? Seq(start.val) : Seq(start.val) ++ elems(start.next) ) + ) +} + +function sorted(start: Ref) : Bool + requires List(start) +{ + unfolding List(start) in + start.next == null + ? true + : (unfolding List(start.next) in start.val <= start.next.val) + && sorted(start.next) +} + +method append_it(l1 : Ref, l2: Ref) + requires List(l1) && List(l2) && l2 != null + ensures List(l1) && elems(l1) == old(elems(l1) ++ elems(l2)) +{ + unfold List(l1) + + if (l1.next == null) { + l1.next := l2 + fold List(l1) + + } else { + var tmp : Ref := l1.next + var index : Int := 1 + + package List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp)) + { + fold List(l1) + } + + while (unfolding List(tmp) in tmp.next != null) + invariant index >= 0 + invariant List(tmp) && elems(tmp) == old(elems(l1))[index..] + + invariant List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp)) + { + unfold List(tmp) + var prev : Ref := tmp + tmp := tmp.next + index := index + 1 + + package List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp)) + { + fold List(prev) + + apply List(prev) --* List(l1) && elems(l1) == old(elems(l1)[..index-1]) ++ old[lhs](elems(prev)) + } + } + + unfold List(tmp) + tmp.next := l2 + fold List(tmp) + + apply List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp)) + } +} + +method traverse_sorted(l: Ref) + requires List(l) && sorted(l) + ensures List(l) && sorted(l) && (unfolding List(l) in l.val) == old(unfolding List(l) in l.val) +{ + unfold List(l) + + if (l == null) { + fold List(l) + } elseif (l.next == null) { + fold List(l) + } else { + traverse_sorted(l.next) + fold List(l) + } +} From 637470913ed4c98e4e35e60739f42905e057b2bd Mon Sep 17 00:00:00 2001 From: Manuel Dublanc <19774382+manud99@users.noreply.github.com> Date: Mon, 13 May 2024 14:00:32 +0200 Subject: [PATCH 2/3] Add UnexpectedOutput annotations for Carbon. --- src/test/resources/wands/snap_functions/test01.vpr | 3 +++ src/test/resources/wands/snap_functions/test02.vpr | 3 +++ src/test/resources/wands/snap_functions/test04.vpr | 3 +++ src/test/resources/wands/snap_functions/test09.vpr | 1 + src/test/resources/wands/snap_functions/test10.vpr | 1 + src/test/resources/wands/snap_functions/test11.vpr | 2 ++ 6 files changed, 13 insertions(+) diff --git a/src/test/resources/wands/snap_functions/test01.vpr b/src/test/resources/wands/snap_functions/test01.vpr index 5aba1313c..5ede73fad 100644 --- a/src/test/resources/wands/snap_functions/test01.vpr +++ b/src/test/resources/wands/snap_functions/test01.vpr @@ -6,6 +6,7 @@ method test01a(x: Ref) package true --* acc(x.b) + //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/) assert applying (true --* acc(x.b)) in x.b } @@ -26,6 +27,7 @@ method test01c(x: Ref) 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) @@ -39,6 +41,7 @@ method test01d(x: Ref, a: Bool) 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) diff --git a/src/test/resources/wands/snap_functions/test02.vpr b/src/test/resources/wands/snap_functions/test02.vpr index 7c9e6d792..789669d7a 100644 --- a/src/test/resources/wands/snap_functions/test02.vpr +++ b/src/test/resources/wands/snap_functions/test02.vpr @@ -6,6 +6,7 @@ method test02a(x: Ref) package true --* acc(x.f) + //:: UnexpectedOutput(exhale.failed:insufficient.permission, /Carbon/issue/488/) assert applying (true --* acc(x.f)) in x.f == 42 } @@ -26,6 +27,7 @@ method test02c(x: Ref) 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) @@ -39,6 +41,7 @@ method test02d(x: Ref, a: Int) 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) diff --git a/src/test/resources/wands/snap_functions/test04.vpr b/src/test/resources/wands/snap_functions/test04.vpr index 91cc63212..7c80ab883 100644 --- a/src/test/resources/wands/snap_functions/test04.vpr +++ b/src/test/resources/wands/snap_functions/test04.vpr @@ -6,6 +6,7 @@ method test04a(x: Ref, y: Ref) 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 } @@ -26,6 +27,7 @@ method test04c(x: Ref, y: Ref) 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) @@ -39,6 +41,7 @@ method test04d(x: Ref, y: Ref, a: Int, b: Int) 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) diff --git a/src/test/resources/wands/snap_functions/test09.vpr b/src/test/resources/wands/snap_functions/test09.vpr index 04698b8a4..081fbdbdd 100644 --- a/src/test/resources/wands/snap_functions/test09.vpr +++ b/src/test/resources/wands/snap_functions/test09.vpr @@ -4,6 +4,7 @@ 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 } diff --git a/src/test/resources/wands/snap_functions/test10.vpr b/src/test/resources/wands/snap_functions/test10.vpr index 843193945..7e01925a1 100644 --- a/src/test/resources/wands/snap_functions/test10.vpr +++ b/src/test/resources/wands/snap_functions/test10.vpr @@ -26,5 +26,6 @@ method test10b(x: Ref) apply acc(x.f) --* foo(x) + //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/216/) assert foo(x) && unfolding foo(x) in x.f == 42 } diff --git a/src/test/resources/wands/snap_functions/test11.vpr b/src/test/resources/wands/snap_functions/test11.vpr index 8fa3f95e2..3e5751e7e 100644 --- a/src/test/resources/wands/snap_functions/test11.vpr +++ b/src/test/resources/wands/snap_functions/test11.vpr @@ -26,6 +26,7 @@ function sorted(start: Ref) : Bool method append_it(l1 : Ref, l2: Ref) requires List(l1) && List(l2) && l2 != null + //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/000/) ensures List(l1) && elems(l1) == old(elems(l1) ++ elems(l2)) { unfold List(l1) @@ -54,6 +55,7 @@ method append_it(l1 : Ref, l2: Ref) tmp := tmp.next index := index + 1 + //:: UnexpectedOutput(assert.failed:assertion.false, /Carbon/issue/000/) package List(tmp) --* List(l1) && elems(l1) == old(elems(l1)[..index]) ++ old[lhs](elems(tmp)) { fold List(prev) From e0c11acdefdbbd9dd4abac445dfe041f2033d7c4 Mon Sep 17 00:00:00 2001 From: Manuel Dublanc <19774382+manud99@users.noreply.github.com> Date: Mon, 13 May 2024 14:54:55 +0200 Subject: [PATCH 3/3] Add unsound example illustrating issue viperproject/silicon#307. --- .../resources/wands/snap_functions/README.md | 1 + .../resources/wands/snap_functions/test12.vpr | 70 +++++++++++++++++++ 2 files changed, 71 insertions(+) create mode 100644 src/test/resources/wands/snap_functions/test12.vpr diff --git a/src/test/resources/wands/snap_functions/README.md b/src/test/resources/wands/snap_functions/README.md index a3305229c..d9ac96798 100644 --- a/src/test/resources/wands/snap_functions/README.md +++ b/src/test/resources/wands/snap_functions/README.md @@ -17,6 +17,7 @@ This folder contains Viper test files that I used when working on MagicWandSnapF | [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) diff --git a/src/test/resources/wands/snap_functions/test12.vpr b/src/test/resources/wands/snap_functions/test12.vpr new file mode 100644 index 000000000..01add1335 --- /dev/null +++ b/src/test/resources/wands/snap_functions/test12.vpr @@ -0,0 +1,70 @@ +// Test cases showing unsound behaviour of current Viper +// Related to wands/new_syntax/QPWands.vpr + +field f: Int + +method test12a(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 acc(some.f) --* true + + var completed: Seq[Ref] := Seq(some) + assert forall x: Ref :: x in completed ==> acc(x.f) --* true + + some.f := 1 + assert applying (acc(some.f) --* true) in true + + some.f := 2 + assert applying (acc(some.f) --* true) in true + + //:: ExpectedOutput(assert.failed:assertion.false) + //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/307/) + assert false +} + +method test12b(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 acc(some.f) --* acc(some.f) + + var completed: Seq[Ref] := Seq(some) + assert forall x: Ref :: x in completed ==> acc(x.f) --* acc(x.f) + + some.f := applying (acc(some.f) --* acc(some.f)) in some.f + 1 + apply acc(some.f) --* acc(some.f) + + //:: ExpectedOutput(assert.failed:assertion.false) + //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/307/) + assert false +} + +method test12c(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 acc(some.f) --* acc(some.f) + + var completed: Seq[Ref] := Seq(some) + assert forall x: Ref :: x in completed ==> acc(x.f) --* acc(x.f) + + some.f := applying (acc(some.f) --* acc(some.f)) in some.f + 1 + some.f := applying (acc(some.f) --* acc(some.f)) in some.f + 1 + + //:: ExpectedOutput(assert.failed:assertion.false) + //:: MissingOutput(assert.failed:assertion.false, /Silicon/issue/307/) + assert false +}