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 --- ...me-terms-do-not-look-like-the-triggers-they-match.dfy | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy (limited to 'Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy') 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; +} -- cgit v1.2.3 From af6f23ba1869c0450c44e917becc48263b565327 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 21 Aug 2015 09:39:49 -0700 Subject: Add /printTooltips to trigger tests --- .../function-applications-are-triggers.dfy | 2 +- .../function-applications-are-triggers.dfy.expect | 11 ++++++++ .../large-quantifiers-dont-break-dafny.dfy | 2 +- .../large-quantifiers-dont-break-dafny.dfy.expect | 2 ++ Test/triggers/loop-detection-is-not-too-strict.dfy | 2 +- .../loop-detection-is-not-too-strict.dfy.expect | 4 +++ .../loop-detection-messages--unit-tests.dfy | 2 +- .../loop-detection-messages--unit-tests.dfy.expect | 24 ++++++++++++++++++ .../nested-quantifiers-all-get-triggers.dfy | 2 +- .../nested-quantifiers-all-get-triggers.dfy.expect | 2 ++ ...ms-do-not-look-like-the-triggers-they-match.dfy | 2 +- .../splitting-triggers-recovers-expressivity.dfy | 2 +- ...tting-triggers-recovers-expressivity.dfy.expect | 29 ++++++++++++++++++++++ ...s-yields-better-precondition-related-errors.dfy | 2 +- Test/triggers/triggers-prevent-some-inlining.dfy | 2 +- .../triggers-prevent-some-inlining.dfy.expect | 5 ++++ Test/triggers/useless-triggers-are-removed.dfy | 2 +- 17 files changed, 87 insertions(+), 10 deletions(-) (limited to 'Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy') diff --git a/Test/triggers/function-applications-are-triggers.dfy b/Test/triggers/function-applications-are-triggers.dfy index 67ffe4e4..0aad9018 100644 --- a/Test/triggers/function-applications-are-triggers.dfy +++ b/Test/triggers/function-applications-are-triggers.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This file checks that function applications yield trigger candidates diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect index 069e7767..7922e88d 100644 --- a/Test/triggers/function-applications-are-triggers.dfy.expect +++ b/Test/triggers/function-applications-are-triggers.dfy.expect @@ -1,2 +1,13 @@ +function-applications-are-triggers.dfy(9,9): Info: Selected triggers: {P.requires(f)} +function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f.requires(10)}: + Selected triggers: + {f(10)}, {f.requires(10)}, {P(f)} +function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(10) == 0}: + Selected triggers: + {f(10)}, {f.requires(10)}, {P(f)} +function-applications-are-triggers.dfy(11,9): Info: Selected triggers: + {f(10)}, {f.requires(10)} +function-applications-are-triggers.dfy(12,5): Info: Selected triggers: + {g(x), f(x)}, {g(x), f.requires(x)}, {g(x)}, {f(x)}, {g.requires(x), f.requires(x)}, {g.requires(x)}, {f.requires(x)} 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 index 8becae97..58eb56e1 100644 --- a/Test/triggers/large-quantifiers-dont-break-dafny.dfy +++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This test ensures that the trigger collector (the routine that picks trigger diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect index c90560b0..5e7c14b9 100644 --- a/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect +++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect @@ -1,2 +1,4 @@ +large-quantifiers-dont-break-dafny.dfy(60,9): Info: Selected triggers: + {P49(x)}, {P48(x)}, {P47(x)}, {P46(x)}, {P45(x)}, {P44(x)}, {P43(x)}, {P42(x)}, {P41(x)}, {P40(x)}, {P39(x)}, {P38(x)}, {P37(x)}, {P36(x)}, {P35(x)}, {P34(x)}, {P33(x)}, {P32(x)}, {P31(x)}, {P30(x)}, {P29(x)}, {P28(x)}, {P27(x)}, {P26(x)}, {P25(x)}, {P24(x)}, {P23(x)}, {P22(x)}, {P21(x)}, {P20(x)}, {P19(x)}, {P18(x)}, {P17(x)}, {P16(x)}, {P15(x)}, {P14(x)}, {P13(x)}, {P12(x)}, {P11(x)}, {P10(x)}, {P9(x)}, {P8(x)}, {P7(x)}, {P6(x)}, {P5(x)}, {P4(x)}, {P3(x)}, {P2(x)}, {P1(x)}, {P0(x)} 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 index c6722399..a5a30c81 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This test shows that the loop detection engine makes compromises when looking diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect index 29882da7..270f7e57 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect @@ -1,3 +1,7 @@ +loop-detection-is-not-too-strict.dfy(14,9): Info: Selected triggers: + {P(y, x)}, {P(x, y)} +loop-detection-is-not-too-strict.dfy(17,9): Info: Selected triggers: + {P(y, x)}, {P(x, y)} 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. diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy b/Test/triggers/loop-detection-messages--unit-tests.dfy index d5439e09..c1560317 100644 --- a/Test/triggers/loop-detection-messages--unit-tests.dfy +++ b/Test/triggers/loop-detection-messages--unit-tests.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This file is a series of basic tests for loop detection, focusing on the diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect index 1ebc0bce..89d7265c 100644 --- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect +++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect @@ -1,13 +1,37 @@ +loop-detection-messages--unit-tests.dfy(11,9): Info: Selected triggers: {f(f(i))} + Rejected triggers: {f(i)} (loops with {f(f(i))}) loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (loops with {f(i + 1)}) (!) Suppressing loops would leave this expression without triggers. +loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(i)} (loops with {f(i + 1)}) +loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == f(i + 1)}: + Selected triggers: {g(i)} + Rejected triggers: {f(i)} (loops with {f(i + 1)}) +loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == g(i)}: + Selected triggers: + {g(i)}, {f(i)} loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression {false ==> f(i) == f(i + 1)}: Selected triggers: {f(i)} (loops with {f(i + 1)}) (!) Suppressing loops would leave this expression without triggers. +loop-detection-messages--unit-tests.dfy(16,9): Info: For expression {false ==> f(i) == f(i)}: + Selected triggers: {f(i)} +loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i + 1)}: + Selected triggers: {f(i)} (loops with {f(i + 1)}) +loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i)}: + Selected triggers: {f(i)} +loop-detection-messages--unit-tests.dfy(19,9): Info: Selected triggers: {f(i)} loop-detection-messages--unit-tests.dfy(20,9): Warning: (!) No terms found to trigger on. +loop-detection-messages--unit-tests.dfy(21,9): Info: Not generating triggers for {false ==> f(i + 1) == 0}. +loop-detection-messages--unit-tests.dfy(23,9): Info: Selected triggers: {f(j), f(i)} loop-detection-messages--unit-tests.dfy(24,9): Warning: (!) No trigger covering all quantified variables found. +loop-detection-messages--unit-tests.dfy(25,9): Info: For expression {false ==> f(i) == f(i)}: + Selected triggers: {g(j), f(i)} +loop-detection-messages--unit-tests.dfy(25,9): Info: For expression {false ==> g(j) == 0}: + Selected triggers: {g(j), f(i)} loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> f(i) == f(i)}: (!) No trigger covering all quantified variables found. loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> g(j + 1) == 0}: (!) No trigger covering all quantified variables found. +loop-detection-messages--unit-tests.dfy(27,9): Info: Not generating triggers for {false ==> f(i) == f(i)}. +loop-detection-messages--unit-tests.dfy(28,9): Info: Not generating triggers for {false ==> f(i) == f(i)}. Dafny program verifier finished with 4 verified, 0 errors diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy b/Test/triggers/nested-quantifiers-all-get-triggers.dfy index c75cfab9..a55019db 100644 --- a/Test/triggers/nested-quantifiers-all-get-triggers.dfy +++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This checks that nested quantifiers do get triggers, and that the parent diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect index 069e7767..172f5607 100644 --- a/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect +++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect @@ -1,2 +1,4 @@ +nested-quantifiers-all-get-triggers.dfy(8,17): Info: Selected triggers: {x in s} +nested-quantifiers-all-get-triggers.dfy(8,59): Info: Selected triggers: {y in s} 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 index 7423e086..d7636ea2 100644 --- 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 @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This file shows how Dafny detects loops even for terms that are not literal diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy b/Test/triggers/splitting-triggers-recovers-expressivity.dfy index 79a0dc72..dd1bd81d 100644 --- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy +++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" predicate P(i: int) diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect index 8d7ff4ef..63cbc476 100644 --- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect +++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect @@ -1,3 +1,32 @@ +splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)} + Rejected triggers: {P(i)} (loops with {P(i + 1)}) +splitting-triggers-recovers-expressivity.dfy(17,11): Info: Selected triggers: {Q(j)} + Rejected triggers: {P(j)} (loops with {P(j + 1)}) +splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)} + Rejected triggers: {P(i)} (loops with {P(i + 1)}) +splitting-triggers-recovers-expressivity.dfy(33,11): Info: Selected triggers: {Q(j)} + Rejected triggers: {P(j)} (loops with {P(j + 1)}) +splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i)}: + Selected triggers: + {Q(i)}, {P(i)} +splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {!Q(i)}: + Selected triggers: + {Q(i)}, {P(i)} +splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i + 1)}: + Selected triggers: {Q(i)} + Rejected triggers: {P(i)} (loops with {P(i + 1)}) +splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> P(j)}: + Selected triggers: + {Q(j)}, {P(j)} +splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> Q(j) ==> P(j + 1)}: + Selected triggers: {Q(j)} + Rejected triggers: {P(j)} (loops with {P(j + 1)}) +splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> Q(i)}: + Selected triggers: + {P(i)}, {Q(i)} +splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> P(i) ==> P(i + 1)}: + Selected triggers: + {P(i)} (loops with {P(i + 1)}), {Q(i)} splitting-triggers-recovers-expressivity.dfy(12,63): Error BP5003: A postcondition might not hold on this return path. splitting-triggers-recovers-expressivity.dfy(12,10): Related location: This is the postcondition that might not hold. Execution trace: diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy index f25a624e..20e90843 100644 --- a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy +++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%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. diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy b/Test/triggers/triggers-prevent-some-inlining.dfy index 04b8051c..90af62a3 100644 --- a/Test/triggers/triggers-prevent-some-inlining.dfy +++ b/Test/triggers/triggers-prevent-some-inlining.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This file looks at the interactions between inlining and triggers. The diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect index 73ba063c..4c24893e 100644 --- a/Test/triggers/triggers-prevent-some-inlining.dfy.expect +++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect @@ -1,2 +1,7 @@ +triggers-prevent-some-inlining.dfy(17,2): Info: Selected triggers: {sum(a, b)} +triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined. +triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined. +triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined. +triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined. Dafny program verifier finished with 4 verified, 0 errors diff --git a/Test/triggers/useless-triggers-are-removed.dfy b/Test/triggers/useless-triggers-are-removed.dfy index 16458e41..658890f2 100644 --- a/Test/triggers/useless-triggers-are-removed.dfy +++ b/Test/triggers/useless-triggers-are-removed.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /printTooltips /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This file ensures that Dafny does get rid of redundant triggers before -- cgit v1.2.3