From 19c70cd0d7a65c46bcaafa66b13bde43316bc081 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 22:16:02 -0700 Subject: Add tests for quantifier splitting and trigger generation --- .../function-applications-are-triggers.dfy | 15 ++++++ .../function-applications-are-triggers.dfy.expect | 2 + .../large-quantifiers-dont-break-dafny.dfy | 61 ++++++++++++++++++++++ .../large-quantifiers-dont-break-dafny.dfy.expect | 2 + Test/triggers/loop-detection-is-not-too-strict.dfy | 21 ++++++++ .../loop-detection-is-not-too-strict.dfy.expect | 4 ++ .../nested-quantifiers-all-get-triggers.dfy | 9 ++++ .../nested-quantifiers-all-get-triggers.dfy.expect | 2 + ...ms-do-not-look-like-the-triggers-they-match.dfy | 16 ++++++ ...ot-look-like-the-triggers-they-match.dfy.expect | 10 ++++ ...s-yields-better-precondition-related-errors.dfy | 21 ++++++++ ...s-better-precondition-related-errors.dfy.expect | 32 ++++++++++++ Test/triggers/triggers-prevent-some-inlining.dfy | 26 +++++++++ .../triggers-prevent-some-inlining.dfy.expect | 2 + 14 files changed, 223 insertions(+) create mode 100644 Test/triggers/function-applications-are-triggers.dfy create mode 100644 Test/triggers/function-applications-are-triggers.dfy.expect create mode 100644 Test/triggers/large-quantifiers-dont-break-dafny.dfy create mode 100644 Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect create mode 100644 Test/triggers/loop-detection-is-not-too-strict.dfy create mode 100644 Test/triggers/loop-detection-is-not-too-strict.dfy.expect create mode 100644 Test/triggers/nested-quantifiers-all-get-triggers.dfy create mode 100644 Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect create mode 100644 Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy create mode 100644 Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect create mode 100644 Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy create mode 100644 Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect create mode 100644 Test/triggers/triggers-prevent-some-inlining.dfy create mode 100644 Test/triggers/triggers-prevent-some-inlining.dfy.expect (limited to 'Test/triggers') 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, 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, 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, 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 -- cgit v1.2.3