Add tests for quantifier splitting and trigger generation

14 files changed, 223 insertions, 0 deletions

diff --git a/Test/triggers/function-applications-are-triggers.dfy b/Test/triggers/function-applications-are-triggers.dfy
new file mode 100644
index 00000000..0fae8c0e
--- /dev/null
+++ b/Test/triggers/function-applications-are-triggers.dfy
@@ -0,0 +1,15 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This files checks that function applications yield trigger candidates

+

+method M(P: (int -> int) -> bool, g: int -> int)

+  requires P.requires(g)

+  requires P(g) {

+  assume forall f: int -> int :: P.requires(f);

+  assume forall f: int -> int :: P(f) ==> f.requires(10) && f(10) == 0;

+  assert forall f: int -> int ::

+    (forall x :: f.requires(x) && g.requires(x) ==> f(x) == g(x)) ==>

+    f.requires(10) ==>

+    f(10) == 0;

+}

diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
new file mode 100644
index 00000000..8becae97
--- /dev/null
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
@@ -0,0 +1,61 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This test ensures that the trigger  collector (the routine that picks trigger

+// candidates) does not  actually consider all subsets of terms;  if it did, the

+// following would take horribly long

+

+predicate P0(x: bool)

+predicate P1(x: bool)

+predicate P2(x: bool)

+predicate P3(x: bool)

+predicate P4(x: bool)

+predicate P5(x: bool)

+predicate P6(x: bool)

+predicate P7(x: bool)

+predicate P8(x: bool)

+predicate P9(x: bool)

+predicate P10(x: bool)

+predicate P11(x: bool)

+predicate P12(x: bool)

+predicate P13(x: bool)

+predicate P14(x: bool)

+predicate P15(x: bool)

+predicate P16(x: bool)

+predicate P17(x: bool)

+predicate P18(x: bool)

+predicate P19(x: bool)

+predicate P20(x: bool)

+predicate P21(x: bool)

+predicate P22(x: bool)

+predicate P23(x: bool)

+predicate P24(x: bool)

+predicate P25(x: bool)

+predicate P26(x: bool)

+predicate P27(x: bool)

+predicate P28(x: bool)

+predicate P29(x: bool)

+predicate P30(x: bool)

+predicate P31(x: bool)

+predicate P32(x: bool)

+predicate P33(x: bool)

+predicate P34(x: bool)

+predicate P35(x: bool)

+predicate P36(x: bool)

+predicate P37(x: bool)

+predicate P38(x: bool)

+predicate P39(x: bool)

+predicate P40(x: bool)

+predicate P41(x: bool)

+predicate P42(x: bool)

+predicate P43(x: bool)

+predicate P44(x: bool)

+predicate P45(x: bool)

+predicate P46(x: bool)

+predicate P47(x: bool)

+predicate P48(x: bool)

+predicate P49(x: bool)

+

+method M() {

+  assert forall x :: true || P0(x) || P1(x) || P2(x) || P3(x) || P4(x) || P5(x) || P6(x) || P7(x) || P8(x) || P9(x) || P10(x) || P11(x) || P12(x) || P13(x) || P14(x) || P15(x) || P16(x) || P17(x) || P18(x) || P19(x) || P20(x) || P21(x) || P22(x) || P23(x) || P24(x) || P25(x) || P26(x) || P27(x) || P28(x) || P29(x) || P30(x) || P31(x) || P32(x) || P33(x) || P34(x) || P35(x) || P36(x) || P37(x) || P38(x) || P39(x) || P40(x) || P41(x) || P42(x) || P43(x) || P44(x) || P45(x) || P46(x) || P47(x) || P48(x) || P49(x);

+}

diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
new file mode 100644
index 00000000..c90560b0
--- /dev/null
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 52 verified, 0 errors

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy
new file mode 100644
index 00000000..c6722399
--- /dev/null
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This test shows that the loop detection engine makes compromises when looking

+// for subexpressions matching a trigger; in particular, it allows a

+// subexpression to match a trigger without reporting a loop and without being

+// equal to that trigger, as long as the only differences are variable

+

+predicate P(x: int, y: int)

+

+method Test() {

+  // P(x, y) and P(y, x) might look like they would cause a loop. Since they

+  // only differ by their variables, though, they won't raise flags.

+  assume forall x: int, y: int :: P(x, y) == P(y, x);

+

+  // This works independent of extra parentheses:

+  assume forall x: int, y: int :: P(x, y) == (P(y, x));

+

+  // Contrast with the following:

+  assume forall x: int, y: int :: P(x, y) == P(x, y+1);

+}

diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
new file mode 100644
index 00000000..c2e5ef3a
--- /dev/null
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -0,0 +1,4 @@
+loop-detection-is-not-too-strict.dfy(20,9): Warning:  Selected triggers: {P(x, y)} (loops with {P(x, y + 1)})

+ (!) Suppressing loops would leave this expression without triggers.

+

+Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
new file mode 100644
index 00000000..c75cfab9
--- /dev/null
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
@@ -0,0 +1,9 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This checks that nested quantifiers do get triggers, and that the parent

+// quantifier does not get annotated twice

+

+method M() {

+  ghost var x := forall s: set<int>, x: int :: (x in s ==> forall y :: y == x ==> y in s);

+}

diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
new file mode 100644
index 00000000..7423e086
--- /dev/null
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
@@ -0,0 +1,16 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file shows how Dafny detects loops even for terms that are not literal

+// AST matches. This file also checks that triggers are reported exactly as

+// picked (that is, `x in s` yields `s[x]` for a multiset s), but matches as

+// they appear in the buffer text (that is, `x+1 in s` is not translated to

+// s[x+1] when highlited as a cause for a potential matching loop.

+

+method M() {

+  // This is an obvious loop

+  ghost var b := forall s: multiset<int>, x: int :: s[x] > 0 ==> s[x+1] > 0;

+

+  // x in s loops with s[x+1] due to the way [x in s] is translated

+  ghost var a := forall s: multiset<int>, x: int :: x in s ==> s[x+1] > 0 && x+2 !in s;

+}

diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
new file mode 100644
index 00000000..ef48f568
--- /dev/null
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
@@ -0,0 +1,10 @@
+some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning:  Selected triggers: {s[x]} (loops with {s[x + 1]})

+ (!) Suppressing loops would leave this expression without triggers.

+some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> s[x + 1] > 0}:

+   Selected triggers: {s[x]} (loops with {s[x + 1]})

+   (!) Suppressing loops would leave this expression without triggers.

+some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> x + 2 !in s}:

+   Selected triggers: {s[x]} (loops with {x + 2 !in s})

+   (!) Suppressing loops would leave this expression without triggers.

+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
new file mode 100644
index 00000000..f25a624e
--- /dev/null
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This tests shows that, since quantifiers are split, it becomes possible to know more precisely what part of a precondition did not hold at the call site.

+

+method f()

+  requires forall y :: y > 0 && y < 0 {

+}

+

+method g(x: int) {

+  f();

+}

+

+function gf(): int

+  requires forall y :: y > 0 && y < 0 {

+    1

+}

+

+function gg(x: int): int {

+  gf()

+}

diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
new file mode 100644
index 00000000..c8e1a5fa
--- /dev/null
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
@@ -0,0 +1,32 @@
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y > 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y < 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y > 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y < 0}:

+   (!) No terms found to trigger on.

+splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,34): Related location

+Execution trace:

+    (0,0): anon0

+splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.

+splitting-triggers-yields-better-precondition-related-errors.dfy(7,25): Related location

+Execution trace:

+    (0,0): anon0

+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,34): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location

+splitting-triggers-yields-better-precondition-related-errors.dfy(15,25): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon4_Else

+

+Dafny program verifier finished with 4 verified, 4 errors

diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy b/Test/triggers/triggers-prevent-some-inlining.dfy
new file mode 100644
index 00000000..04b8051c
--- /dev/null
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy
@@ -0,0 +1,26 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This  file looks  at the  interactions  between inlining  and triggers.   The

+// sum_is_sum predicate gets a {sum(a,  b)} trigger, which explicitly depends on

+// one of the  variables being passed in. Since triggers  are generated prior to

+// inlining  (inlining  happens  during  translation),  inlining  the  last  two

+// instances of that call below would cause  b+1 (a trigger killer) to pop up in

+// a trigger.   This would create  an invalid trigger,  so Dafny doesn't  let it

+// happen.

+

+function sum(a: int, b: int): int {

+  a + b

+}

+

+predicate sum_is_sum(b: int, c: int) {

+  forall a: int :: sum(a, b) + c == a + b + c

+}

+

+method can_we_inline(b: int, c: int)

+  ensures sum_is_sum(0, 0)     // OK  to inline

+  ensures sum_is_sum(b, c)     // OK  to inline

+  ensures sum_is_sum(b, c+1)   // OK  to inline

+  ensures sum_is_sum(b+1, c)   // NOK to inline

+  ensures sum_is_sum(b+1, c+1) // NOK to inline

+{ }

diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 4 verified, 0 errors