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] 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) + } +}