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 --- Test/triggers/loop-detection-is-not-too-strict.dfy.expect | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 Test/triggers/loop-detection-is-not-too-strict.dfy.expect (limited to 'Test/triggers/loop-detection-is-not-too-strict.dfy.expect') 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 -- cgit v1.2.3 From aeb38d63369ee5b584ef9f5574c7371aea423759 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 10:37:11 -0700 Subject: Simplify error reporting in the trigger generator to get cleaner messages --- Source/Dafny/Triggers/QuantifiersCollection.cs | 10 ++++++---- Test/triggers/loop-detection-is-not-too-strict.dfy.expect | 2 +- ...e-terms-do-not-look-like-the-triggers-they-match.dfy.expect | 2 +- 3 files changed, 8 insertions(+), 6 deletions(-) (limited to 'Test/triggers/loop-detection-is-not-too-strict.dfy.expect') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 49cd84df..ec2f1777 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -137,9 +137,9 @@ namespace Microsoft.Dafny.Triggers { private void CommitOne(QuantifierWithTriggers q, bool addHeader) { var errorLevel = ErrorLevel.Info; var msg = new StringBuilder(); - var indent = addHeader ? " " : " "; //FIXME if multiline messages were properly supported, this indentation wouldn't be needed + var indent = addHeader ? " " : ""; - if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop and autotriggers attributes are passed down to Boogie + if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop, split and autotriggers attributes are passed down to Boogie msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy) // FIXME typeQuantifier? @@ -156,7 +156,7 @@ namespace Microsoft.Dafny.Triggers { AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true); #if QUANTIFIER_WARNINGS - string WARN = (msg.Length > 0 ? indent : "") + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "); + string WARN = indent + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "); if (!q.CandidateTerms.Any()) { errorLevel = ErrorLevel.Warning; msg.Append(WARN).AppendLine("No terms found to trigger on."); @@ -171,7 +171,9 @@ namespace Microsoft.Dafny.Triggers { } if (msg.Length > 0) { - reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msg.ToString().TrimEnd("\r\n".ToCharArray())); + // Extra indent added to make it easier to distinguish multiline error messages + var msgStr = msg.ToString().Replace(Environment.NewLine, Environment.NewLine + " ").TrimEnd("\r\n ".ToCharArray()); + reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr); } } 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 c2e5ef3a..29882da7 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect @@ -1,4 +1,4 @@ -loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (loops with {P(x, y + 1)}) +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/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 index ef48f568..83648626 100644 --- 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 @@ -1,4 +1,4 @@ -some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (loops with {s[x + 1]}) +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]}) -- 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/loop-detection-is-not-too-strict.dfy.expect') 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 From 7cd998145a00c54a25cc46a82f034769b281c4c1 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 14:09:00 -0700 Subject: s/loops with/may loop with/ --- Source/Dafny/Triggers/QuantifiersCollection.cs | 2 +- Test/triggers/loop-detection-is-not-too-strict.dfy.expect | 2 +- .../triggers/loop-detection-looks-at-ranges-too.dfy.expect | 4 ++-- .../loop-detection-messages--unit-tests.dfy.expect | 12 ++++++------ .../looping-is-hard-to-decide-modulo-equality.dfy.expect | 4 ++-- Test/triggers/matrix-accesses-are-triggers.dfy.expect | 2 +- .../triggers/old-is-a-special-case-for-triggers.dfy.expect | 10 +++++----- ...rms-do-not-look-like-the-triggers-they-match.dfy.expect | 6 +++--- .../splitting-triggers-recovers-expressivity.dfy.expect | 14 +++++++------- Test/triggers/useless-triggers-are-removed.dfy.expect | 4 ++-- 10 files changed, 30 insertions(+), 30 deletions(-) (limited to 'Test/triggers/loop-detection-is-not-too-strict.dfy.expect') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 0ef59bad..6555b52a 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -119,7 +119,7 @@ namespace Microsoft.Dafny.Triggers { (candidate, loopingSubterms) => !loopingSubterms.Any(), (candidate, loopingSubterms) => { looping.Add(candidate); - candidate.Annotation = "loops with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", "); + candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", "); }).ToList(); q.CouldSuppressLoops = safe.Count > 0; 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 270f7e57..6f5ed3d7 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect @@ -2,7 +2,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)}) +loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (may loop 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/loop-detection-looks-at-ranges-too.dfy.expect b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect index 72482de5..ce62d868 100644 --- a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect +++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect @@ -1,6 +1,6 @@ -loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (loops with {P(x + 1)}) +loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)}) (!) Suppressing loops would leave this expression without triggers. -loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (loops with {P(x + 1)}) +loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)}) (!) Suppressing loops would leave this expression without triggers. Dafny program verifier finished with 3 verified, 0 errors diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect index 89d7265c..804a0116 100644 --- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect +++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect @@ -1,21 +1,21 @@ 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)}) + Rejected triggers: {f(i)} (may loop with {f(f(i))}) +loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop 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(13,9): Info: Selected triggers: {f(i)} (may loop 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)}) + Rejected triggers: {f(i)} (may loop 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)}) + Selected triggers: {f(i)} (may loop 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)}) + Selected triggers: {f(i)} (may loop 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)} diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect index c0eebdba..58094110 100644 --- a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect +++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect @@ -1,10 +1,10 @@ looping-is-hard-to-decide-modulo-equality.dfy(21,9): Info: Selected triggers: {h(h(c, j), j)}, {h(c, i)}, {c in sc} - Rejected triggers: {h(c, j)} (loops with {h(h(c, j), j)}) + Rejected triggers: {h(c, j)} (may loop with {h(h(c, j), j)}) looping-is-hard-to-decide-modulo-equality.dfy(26,9): Info: Selected triggers: {f(x)} Rejected triggers: {g(f(x))} (more specific than {f(x)}) looping-is-hard-to-decide-modulo-equality.dfy(31,9): Info: Selected triggers: {old(f(f(c)))}, {f(c)}, {c in sc} - Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))}) + Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))}) Dafny program verifier finished with 9 verified, 0 errors diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy.expect b/Test/triggers/matrix-accesses-are-triggers.dfy.expect index b9dd1d88..35df02f5 100644 --- a/Test/triggers/matrix-accesses-are-triggers.dfy.expect +++ b/Test/triggers/matrix-accesses-are-triggers.dfy.expect @@ -1,4 +1,4 @@ -matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (loops with {m[j, i + 1]}) +matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (may loop with {m[j, i + 1]}) (!) Suppressing loops would leave this expression without triggers. matrix-accesses-are-triggers.dfy(8,81): Error: index 0 out of range Execution trace: diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect index 23ec089d..313d7c16 100644 --- a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect +++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect @@ -2,14 +2,14 @@ old-is-a-special-case-for-triggers.dfy(15,10): Info: Selected triggers: {old(f(c))}, {c in sc} old-is-a-special-case-for-triggers.dfy(20,10): Info: Selected triggers: {old(f(f(c)))}, {f(c)}, {c in sc} - Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))}) + Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))}) old-is-a-special-case-for-triggers.dfy(21,10): Info: Selected triggers: {f(g(c))}, {g(f(c))}, {old(f(g(c)))}, {old(g(f(c)))}, {old(f(f(c)))}, {c in sc} Rejected triggers: - {g(c)} (loops with {g(f(c))}) - {f(c)} (loops with {f(g(c))}) - {old(g(c))} (loops with {old(g(f(c)))}) - {old(f(c))} (loops with {old(f(f(c)))}, {old(f(g(c)))}) + {g(c)} (may loop with {g(f(c))}) + {f(c)} (may loop with {f(g(c))}) + {old(g(c))} (may loop with {old(g(f(c)))}) + {old(f(c))} (may loop with {old(f(f(c)))}, {old(f(g(c)))}) old-is-a-special-case-for-triggers.dfy(25,10): Info: Selected triggers: {old(f(c))}, {f(c)}, {c in sc} Rejected triggers: {old(g(f(c)))} (more specific than {old(f(c))}) 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 index 83648626..f5e47454 100644 --- 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 @@ -1,10 +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]}) +some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (may loop 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]}) + Selected triggers: {s[x]} (may loop 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}) + Selected triggers: {s[x]} (may loop 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-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect index 63cbc476..58c8dd2b 100644 --- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect +++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect @@ -1,11 +1,11 @@ splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)} - Rejected triggers: {P(i)} (loops with {P(i + 1)}) + Rejected triggers: {P(i)} (may loop 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)}) + Rejected triggers: {P(j)} (may loop 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)}) + Rejected triggers: {P(i)} (may loop 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)}) + Rejected triggers: {P(j)} (may loop with {P(j + 1)}) splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i)}: Selected triggers: {Q(i)}, {P(i)} @@ -14,19 +14,19 @@ splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {!Q(i) {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)}) + Rejected triggers: {P(i)} (may loop 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)}) + Rejected triggers: {P(j)} (may loop 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)} + {P(i)} (may loop 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/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect index a526e517..2e9bbedf 100644 --- a/Test/triggers/useless-triggers-are-removed.dfy.expect +++ b/Test/triggers/useless-triggers-are-removed.dfy.expect @@ -5,11 +5,11 @@ useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)} {h(f(x))} (more specific than {f(x)}) {g(f(x))} (more specific than {f(x)}) useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))} - Rejected triggers: {f(x)} (loops with {f(f(x))}) + Rejected triggers: {f(x)} (may loop with {f(f(x))}) useless-triggers-are-removed.dfy(23,11): Info: Selected triggers: {g(f(x)), g(y)}, {f(y), f(x)} Rejected triggers: - {g(y), f(x)} (loops with {g(f(y))}, {g(f(x))}) + {g(y), f(x)} (may loop with {g(f(y))}, {g(f(x))}) {g(f(x)), g(f(y))} (more specific than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)}) {g(f(x)), f(y)} (more specific than {f(y), f(x)}) {g(f(y)), f(x)} (more specific than {f(y), f(x)}) -- cgit v1.2.3 From 1e725f0c9382a3dd8be109d160581868c9567f61 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 21:25:06 -0700 Subject: Further relax the loop detection conditions Mismatches are now allowed up to expressions not involving any of the bound variables of the quantifier under inspection. --- Source/Dafny/Triggers/QuantifiersCollection.cs | 7 +++++-- Source/Dafny/Triggers/TriggerExtensions.cs | 23 +++++++++++++++++----- Source/Dafny/Triggers/TriggersCollector.cs | 3 ++- Test/triggers/loop-detection-is-not-too-strict.dfy | 21 +++++++++++++++++++- .../loop-detection-is-not-too-strict.dfy.expect | 17 ++++++++++++---- 5 files changed, 58 insertions(+), 13 deletions(-) (limited to 'Test/triggers/loop-detection-is-not-too-strict.dfy.expect') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index b77afccb..50458ab7 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -101,8 +101,11 @@ namespace Microsoft.Dafny.Triggers { // [∀ x {f(x), f(f(x))} ⋅ f(x) = f(f(x))] is not a loop). And we even // ignore terms that almost match a trigger term, modulo a single variable // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop). - // The last thing that we ignore is matching variables against constants, - // to ensure that P(x) is not flagged as looping with P(0). + // In addition, we ignore cases where the only differences between a trigger + // and a trigger match are places where a variable is replaced with an + // expression whose free variables do not intersect that of the quantifier + // in which that expression is found. For examples of this behavious, see + // triggers/literals-do-not-cause-loops. // This ignoring logic is implemented by the CouldCauseLoops method. foreach (var q in quantifiers) { diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index dccd996d..d4a822a8 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -31,9 +31,15 @@ namespace Microsoft.Dafny.Triggers { return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr); } - internal bool CouldCauseLoops(List terms) { + /// + /// This method checks whether this match could actually cause a loop, given a set of terms participating in a trigger; + /// to compute an answer, we match the Expr of this match against the Exprs of each of these term, allowing for harmless + /// variations. If any of these tests does match, this term likely won't cause a loop. + /// The boundVars list is useful to determine that forall x :: P(x) == P(y+z) does not loop. + /// + internal bool CouldCauseLoops(List terms, ISet boundVars) { var expr = Expr; - return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNamesAndConstants(expr)); + return !terms.Any(term => term.Expr.ExpressionEqModuloExpressionsNotInvolvingBoundVariables(expr, boundVars)); } } @@ -79,15 +85,22 @@ namespace Microsoft.Dafny.Triggers { return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEq(e1, e2)); } - internal static bool ExpressionEqModuloVariableNamesAndConstants(this Expression expr1, Expression expr2) { + internal static bool ExpressionEqModuloExpressionsNotInvolvingBoundVariables(this Expression expr1, Expression expr2, ISet boundVars) { expr1 = expr1.Resolved; expr2 = expr2.Resolved; if (expr1 is IdentifierExpr) { - return expr2 is IdentifierExpr || expr2 is LiteralExpr; + if (expr2 is IdentifierExpr) { + return true; + } else { + var freeInE2 = Translator.ComputeFreeVariables(expr2); + freeInE2.IntersectWith(boundVars); + return !freeInE2.Any(); + } } - return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNamesAndConstants(e1, e2)); + return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, + expr2.SubExpressions, (e1, e2) => ExpressionEqModuloExpressionsNotInvolvingBoundVariables(e1, e2, boundVars)); } internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet holes, Dictionary bindings) { diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index d78bcb9e..cc3b1978 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -69,7 +69,8 @@ namespace Microsoft.Dafny.Triggers { internal IEnumerable LoopingSubterms(QuantifierExpr quantifier) { Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier var matchingSubterms = this.MatchingSubterms(quantifier); - return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms)); + var boundVars = new HashSet(quantifier.BoundVars); + return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms, boundVars)); } internal List MatchingSubterms(QuantifierExpr quantifier) { diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy index a5a30c81..81f764ad 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy @@ -7,8 +7,9 @@ // equal to that trigger, as long as the only differences are variable predicate P(x: int, y: int) +predicate Q(x: int) -method Test() { +method Test(z: int) { // 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); @@ -18,4 +19,22 @@ method Test() { // Contrast with the following: assume forall x: int, y: int :: P(x, y) == P(x, y+1); + + // The following examples were made legal after an exchange where Chris + // pointed examples in the IronClad sources where things like this were + // incorrectly flagged. + assert forall x :: true || Q(x) || Q(0); + assert forall x :: true || Q(x) || Q(z); + assert forall x :: true || P(x, 1) || P(x, z); + + // Support for the following was added following a discussion with Rustan; in + // the second one the expression `if z > 1 then z else 3 * z + 1` is not + // directly a constant expression, but it does not involve x, so it's ok: + assert forall x :: true || Q(x) || Q(0+1); + assert forall x :: true || Q(x) || Q(if z > 1 then z else 3 * z + 1); + // Sanity check: + assert forall x :: true || Q(x) || Q(if z > 1 then x else 3 * z + 1); + + // WISH: It might also be good to zeta-reduce before loop detection. + assert forall x :: true || Q(x) || (var xx := x+1; Q(xx)); } 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 6f5ed3d7..705c2a8c 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect @@ -1,8 +1,17 @@ -loop-detection-is-not-too-strict.dfy(14,9): Info: Selected triggers: +loop-detection-is-not-too-strict.dfy(15,9): Info: Selected triggers: {P(y, x)}, {P(x, y)} -loop-detection-is-not-too-strict.dfy(17,9): Info: Selected triggers: +loop-detection-is-not-too-strict.dfy(18,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)} (may loop with {P(x, y + 1)}) +loop-detection-is-not-too-strict.dfy(21,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)}) (!) Suppressing loops would leave this expression without triggers. +loop-detection-is-not-too-strict.dfy(26,9): Info: Selected triggers: {Q(x)} +loop-detection-is-not-too-strict.dfy(27,9): Info: Selected triggers: {Q(x)} +loop-detection-is-not-too-strict.dfy(28,9): Info: Selected triggers: + {P(x, z)}, {P(x, 1)} +loop-detection-is-not-too-strict.dfy(33,9): Info: Selected triggers: {Q(x)} +loop-detection-is-not-too-strict.dfy(34,9): Info: Selected triggers: {Q(x)} +loop-detection-is-not-too-strict.dfy(36,9): Warning: Selected triggers: {Q(x)} (may loop with {Q(if z > 1 then x else 3 * z + 1)}) + (!) Suppressing loops would leave this expression without triggers. +loop-detection-is-not-too-strict.dfy(39,9): Info: Selected triggers: {Q(x)} -Dafny program verifier finished with 3 verified, 0 errors +Dafny program verifier finished with 4 verified, 0 errors -- cgit v1.2.3 From 2db858bf6e72e521b49aa0ae3a993dc943b8c875 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 28 Aug 2015 20:39:02 -0700 Subject: Implement {:nowarn}, clarify some messages, and add a few tests --- Source/Dafny/Triggers/QuantifiersCollection.cs | 26 +++++++---- Source/Dafny/Triggers/TriggerUtils.cs | 11 +++-- .../triggers/constructors-cause-matching-loops.dfy | 11 +++++ .../constructors-cause-matching-loops.dfy.expect | 6 +++ .../function-applications-are-triggers.dfy.expect | 4 +- .../loop-detection-is-not-too-strict.dfy.expect | 8 ++-- .../loop-detection-looks-at-ranges-too.dfy.expect | 8 ++-- .../loop-detection-messages--unit-tests.dfy.expect | 50 +++++++++++----------- ...ng-is-hard-to-decide-modulo-equality.dfy.expect | 4 +- .../matrix-accesses-are-triggers.dfy.expect | 4 +- .../old-is-a-special-case-for-triggers.dfy.expect | 10 ++--- Test/triggers/regression-tests.dfy.expect | 2 +- .../some-proofs-only-work-without-autoTriggers.dfy | 48 +++++++++++++++++++++ ...roofs-only-work-without-autoTriggers.dfy.expect | 31 ++++++++++++++ ...ot-look-like-the-triggers-they-match.dfy.expect | 16 +++---- .../splitting-picks-the-right-tokens.dfy.expect | 12 +++--- ...tting-triggers-recovers-expressivity.dfy.expect | 28 ++++++------ ...s-better-precondition-related-errors.dfy.expect | 16 +++---- .../suppressing-warnings-behaves-properly.dfy | 21 +++++++++ ...uppressing-warnings-behaves-properly.dfy.expect | 14 ++++++ .../useless-triggers-are-removed.dfy.expect | 4 +- ...f-checks-use-the-original-quantifier.dfy.expect | 10 ++--- 22 files changed, 244 insertions(+), 100 deletions(-) create mode 100644 Test/triggers/constructors-cause-matching-loops.dfy create mode 100644 Test/triggers/constructors-cause-matching-loops.dfy.expect create mode 100644 Test/triggers/some-proofs-only-work-without-autoTriggers.dfy create mode 100644 Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect create mode 100644 Test/triggers/suppressing-warnings-behaves-properly.dfy create mode 100644 Test/triggers/suppressing-warnings-behaves-properly.dfy.expect (limited to 'Test/triggers/loop-detection-is-not-too-strict.dfy.expect') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 50458ab7..f72dab7f 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -117,7 +117,7 @@ namespace Microsoft.Dafny.Triggers { (candidate, loopingSubterms) => !loopingSubterms.Any(), (candidate, loopingSubterms) => { looping.Add(candidate); - candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", "); + candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "\"" + Printer.ExprToString(t.OriginalExpr) + "\"", ", "); }).ToList(); q.CouldSuppressLoops = safe.Count > 0; @@ -145,12 +145,14 @@ namespace Microsoft.Dafny.Triggers { var errorLevel = ErrorLevel.Info; var msg = new StringBuilder(); var indent = addHeader ? " " : ""; + bool suppressWarnings = Attributes.Contains(q.quantifier.Attributes, "nowarn"); - if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: matchingloop, split and autotriggers attributes are passed down to Boogie - msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); + if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: split and autotriggers attributes are passed down to Boogie + var extraMsg = TriggerUtils.WantsAutoTriggers(q.quantifier) ? "" : " Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead."; + msg.AppendFormat("Not generating triggers for \"{0}\".{1}", Printer.ExprToString(q.quantifier.Term), extraMsg).AppendLine(); } else { if (addHeader) { - msg.AppendFormat("For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine(); + msg.AppendFormat("For expression \"{0}\":", Printer.ExprToString(q.quantifier.Term)).AppendLine(); } foreach (var candidate in q.Candidates) { @@ -161,20 +163,26 @@ namespace Microsoft.Dafny.Triggers { AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true); #if QUANTIFIER_WARNINGS - string WARN = indent + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) "); + var WARN_TAG = DafnyOptions.O.UnicodeOutput ? "⚠ " : "/!\\ "; + var WARN_TAG_OVERRIDE = suppressWarnings ? "(Suppressed warning) " : WARN_TAG; + var WARN_LEVEL = suppressWarnings ? ErrorLevel.Info : ErrorLevel.Warning; + var WARN = indent + WARN_TAG_OVERRIDE; if (!q.CandidateTerms.Any()) { - errorLevel = ErrorLevel.Warning; + errorLevel = WARN_LEVEL; msg.Append(WARN).AppendLine("No terms found to trigger on."); } else if (!q.Candidates.Any()) { - errorLevel = ErrorLevel.Warning; + errorLevel = WARN_LEVEL; msg.Append(WARN).AppendLine("No trigger covering all quantified variables found."); } else if (!q.CouldSuppressLoops && !q.AllowsLoops) { - errorLevel = ErrorLevel.Warning; + errorLevel = WARN_LEVEL; msg.Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers."); + } else if (suppressWarnings) { + errorLevel = ErrorLevel.Warning; + msg.Append(indent).Append(WARN_TAG).AppendLine("There is no warning here to suppress."); } #endif } - + if (msg.Length > 0) { var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray()); reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr); diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index efa1f167..c16a3e44 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -183,14 +183,19 @@ namespace Microsoft.Dafny.Triggers { internal static bool AllowsMatchingLoops(QuantifierExpr quantifier) { Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier + // This is different from nowarn: it won't remove loops at all, even if another trigger is available. return Attributes.Contains(quantifier.Attributes, "matchingloop"); } - internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) { + internal static bool WantsAutoTriggers(QuantifierExpr quantifier) { Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier bool wantsAutoTriggers = true; - return !Attributes.Contains(quantifier.Attributes, "trigger") && - (!Attributes.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers); + return !Attributes.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers; + } + + internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) { + Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier + return !Attributes.Contains(quantifier.Attributes, "trigger") && WantsAutoTriggers(quantifier); } internal static BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) { diff --git a/Test/triggers/constructors-cause-matching-loops.dfy b/Test/triggers/constructors-cause-matching-loops.dfy new file mode 100644 index 00000000..61e6a66b --- /dev/null +++ b/Test/triggers/constructors-cause-matching-loops.dfy @@ -0,0 +1,11 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This file is just a small test to check that constructors do cause loops + +datatype Nat = Zero | Succ(x: Nat) +function f(n: Nat): Nat + +method M() { + assert forall s :: true || f(Succ(s)) == f(s); +} diff --git a/Test/triggers/constructors-cause-matching-loops.dfy.expect b/Test/triggers/constructors-cause-matching-loops.dfy.expect new file mode 100644 index 00000000..e7a671ab --- /dev/null +++ b/Test/triggers/constructors-cause-matching-loops.dfy.expect @@ -0,0 +1,6 @@ +constructors-cause-matching-loops.dfy(10,9): Info: Selected triggers: {Succ(s)} + Rejected triggers: + {f(s)} (may loop with "f(Succ(s))") + {f(Succ(s))} (more specific than {Succ(s)}) + +Dafny program verifier finished with 3 verified, 0 errors diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect index 501cfa51..1214536d 100644 --- a/Test/triggers/function-applications-are-triggers.dfy.expect +++ b/Test/triggers/function-applications-are-triggers.dfy.expect @@ -1,8 +1,8 @@ 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)}: +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}: +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: 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 705c2a8c..65ea0d79 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect @@ -2,16 +2,16 @@ loop-detection-is-not-too-strict.dfy(15,9): Info: Selected triggers: {P(y, x)}, {P(x, y)} loop-detection-is-not-too-strict.dfy(18,9): Info: Selected triggers: {P(y, x)}, {P(x, y)} -loop-detection-is-not-too-strict.dfy(21,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)}) - (!) Suppressing loops would leave this expression without triggers. +loop-detection-is-not-too-strict.dfy(21,9): Warning: Selected triggers: {P(x, y)} (may loop with "P(x, y + 1)") + /!\ Suppressing loops would leave this expression without triggers. loop-detection-is-not-too-strict.dfy(26,9): Info: Selected triggers: {Q(x)} loop-detection-is-not-too-strict.dfy(27,9): Info: Selected triggers: {Q(x)} loop-detection-is-not-too-strict.dfy(28,9): Info: Selected triggers: {P(x, z)}, {P(x, 1)} loop-detection-is-not-too-strict.dfy(33,9): Info: Selected triggers: {Q(x)} loop-detection-is-not-too-strict.dfy(34,9): Info: Selected triggers: {Q(x)} -loop-detection-is-not-too-strict.dfy(36,9): Warning: Selected triggers: {Q(x)} (may loop with {Q(if z > 1 then x else 3 * z + 1)}) - (!) Suppressing loops would leave this expression without triggers. +loop-detection-is-not-too-strict.dfy(36,9): Warning: Selected triggers: {Q(x)} (may loop with "Q(if z > 1 then x else 3 * z + 1)") + /!\ Suppressing loops would leave this expression without triggers. loop-detection-is-not-too-strict.dfy(39,9): Info: Selected triggers: {Q(x)} Dafny program verifier finished with 4 verified, 0 errors diff --git a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect index ce62d868..a32e4a60 100644 --- a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect +++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect @@ -1,6 +1,6 @@ -loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)}) - (!) Suppressing loops would leave this expression without triggers. -loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)}) - (!) Suppressing loops would leave this expression without triggers. +loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (may loop with "P(x + 1)") + /!\ Suppressing loops would leave this expression without triggers. +loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (may loop with "P(x + 1)") + /!\ Suppressing loops would leave this expression without triggers. Dafny program verifier finished with 3 verified, 0 errors diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect index 804a0116..eba8c179 100644 --- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect +++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect @@ -1,37 +1,37 @@ loop-detection-messages--unit-tests.dfy(11,9): Info: Selected triggers: {f(f(i))} - Rejected triggers: {f(i)} (may loop with {f(f(i))}) -loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop 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)} (may loop with {f(i + 1)}) -loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == f(i + 1)}: + Rejected triggers: {f(i)} (may loop with "f(f(i))") +loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop 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)} (may loop 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)} (may loop with {f(i + 1)}) -loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == g(i)}: + Rejected triggers: {f(i)} (may loop 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)} (may loop 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)}: +loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression "false ==> f(i) == f(i + 1)": + Selected triggers: {f(i)} (may loop 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)} (may loop with {f(i + 1)}) -loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i)}: +loop-detection-messages--unit-tests.dfy(17,9): Info: For expression "false ==> f(i) == f(i + 1)": + Selected triggers: {f(i)} (may loop 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(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". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead. 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)}: +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}: +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)}. +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)". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead. +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/looping-is-hard-to-decide-modulo-equality.dfy.expect b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect index 58094110..e900c1f9 100644 --- a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect +++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect @@ -1,10 +1,10 @@ looping-is-hard-to-decide-modulo-equality.dfy(21,9): Info: Selected triggers: {h(h(c, j), j)}, {h(c, i)}, {c in sc} - Rejected triggers: {h(c, j)} (may loop with {h(h(c, j), j)}) + Rejected triggers: {h(c, j)} (may loop with "h(h(c, j), j)") looping-is-hard-to-decide-modulo-equality.dfy(26,9): Info: Selected triggers: {f(x)} Rejected triggers: {g(f(x))} (more specific than {f(x)}) looping-is-hard-to-decide-modulo-equality.dfy(31,9): Info: Selected triggers: {old(f(f(c)))}, {f(c)}, {c in sc} - Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))}) + Rejected triggers: {old(f(c))} (may loop with "old(f(f(c)))") Dafny program verifier finished with 9 verified, 0 errors diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy.expect b/Test/triggers/matrix-accesses-are-triggers.dfy.expect index 35df02f5..572fc41f 100644 --- a/Test/triggers/matrix-accesses-are-triggers.dfy.expect +++ b/Test/triggers/matrix-accesses-are-triggers.dfy.expect @@ -1,5 +1,5 @@ -matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (may loop with {m[j, i + 1]}) - (!) Suppressing loops would leave this expression without triggers. +matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (may loop with "m[j, i + 1]") + /!\ Suppressing loops would leave this expression without triggers. matrix-accesses-are-triggers.dfy(8,81): Error: index 0 out of range Execution trace: (0,0): anon0 diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect index 313d7c16..7388a911 100644 --- a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect +++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect @@ -2,14 +2,14 @@ old-is-a-special-case-for-triggers.dfy(15,10): Info: Selected triggers: {old(f(c))}, {c in sc} old-is-a-special-case-for-triggers.dfy(20,10): Info: Selected triggers: {old(f(f(c)))}, {f(c)}, {c in sc} - Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))}) + Rejected triggers: {old(f(c))} (may loop with "old(f(f(c)))") old-is-a-special-case-for-triggers.dfy(21,10): Info: Selected triggers: {f(g(c))}, {g(f(c))}, {old(f(g(c)))}, {old(g(f(c)))}, {old(f(f(c)))}, {c in sc} Rejected triggers: - {g(c)} (may loop with {g(f(c))}) - {f(c)} (may loop with {f(g(c))}) - {old(g(c))} (may loop with {old(g(f(c)))}) - {old(f(c))} (may loop with {old(f(f(c)))}, {old(f(g(c)))}) + {g(c)} (may loop with "g(f(c))") + {f(c)} (may loop with "f(g(c))") + {old(g(c))} (may loop with "old(g(f(c)))") + {old(f(c))} (may loop with "old(f(f(c)))", "old(f(g(c)))") old-is-a-special-case-for-triggers.dfy(25,10): Info: Selected triggers: {old(f(c))}, {f(c)}, {c in sc} Rejected triggers: {old(g(f(c)))} (more specific than {old(f(c))}) diff --git a/Test/triggers/regression-tests.dfy.expect b/Test/triggers/regression-tests.dfy.expect index a03810fb..e780e966 100644 --- a/Test/triggers/regression-tests.dfy.expect +++ b/Test/triggers/regression-tests.dfy.expect @@ -1,3 +1,3 @@ -regression-tests.dfy(16,5): Warning: (!) No terms found to trigger on. +regression-tests.dfy(16,5): Warning: /!\ No terms found to trigger on. Dafny program verifier finished with 2 verified, 0 errors diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy new file mode 100644 index 00000000..98cea392 --- /dev/null +++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy @@ -0,0 +1,48 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// The examples below work nicely with /autoTriggers:0, but break when we ass +// /autoTriggers. + +// The issue is that the axioms for sequences are missing a number of facts, +// which was not a problem before /autoTriggers and /stricterTriggers, but has +// become one. Here are examples of things that Dafny won’t prove with +// /autoTriggers (I would expect it wouldn’t with stricterTriggers either, +// though the second example is trickier than the first): + +method M(a: seq) { + if * { + // This fails; it needs the following axiom: + // axiom (forall s: Seq T :: + // { Seq#Take(s, Seq#Length(s)) } + // Seq#Take(s, Seq#Length(s)) == s); + assume forall x :: x in a ==> x > 0; + assert forall x :: x in a[..|a|] ==> x > 0; + } else if * { + // This fails; it needs the following axiom: + // axiom (forall s: Seq T, i: int :: + // { Seq#Index(s, i) } + // 0 <= i && i < Seq#Length(s) ==> + // Seq#Contains(s, Seq#Index(s, i))); + assume forall x :: x in a ==> x > 0; + assert forall i | 0 <= i < |a| :: a[i] > 0; + } else if * { + assume |a| > 3; + assume forall x | x in a[..3] :: x > 1; + // This fails, but here it's a lot harder to know what a good axiom would be. + assert forall x | x in a[..2] :: x > 1; + } +} + + +// In the first case, the Boogie version is +// +// Seq#Contains(Seq#Take(a#0, Seq#Length(a#0)), $Box(x#0_1)) ⟹ x#0_1 > 0 +// +// And of course Z3 picks $Box(x#0_1). The third case is similar. +// +// The problem is of course that knowing that x ∈ a[..2] doesn’t magically give +// you a term that matches x ∈ a[..3]. One could imagine introducing an extra +// symbol in the translation to put x and a together for triggering purposes, +// but that would have the same sort of issues as adding symbols for arithmetic +// operators. diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect new file mode 100644 index 00000000..d48840b8 --- /dev/null +++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect @@ -0,0 +1,31 @@ +some-proofs-only-work-without-autoTriggers.dfy(19,11): Info: Selected triggers: {x in a} +some-proofs-only-work-without-autoTriggers.dfy(20,11): Info: Selected triggers: {x in a[..|a|]} +some-proofs-only-work-without-autoTriggers.dfy(27,11): Info: Selected triggers: {x in a} +some-proofs-only-work-without-autoTriggers.dfy(28,11): Info: Selected triggers: {a[i]} +some-proofs-only-work-without-autoTriggers.dfy(31,11): Info: Selected triggers: {x in a[..3]} +some-proofs-only-work-without-autoTriggers.dfy(33,11): Info: Selected triggers: {x in a[..2]} +some-proofs-only-work-without-autoTriggers.dfy(20,11): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon22_Then + (0,0): anon3 + (0,0): anon23_Then + (0,0): anon5 +some-proofs-only-work-without-autoTriggers.dfy(28,11): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon25_Then + (0,0): anon9 + (0,0): anon26_Then + (0,0): anon27_Then + (0,0): anon13 +some-proofs-only-work-without-autoTriggers.dfy(33,11): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon28_Then + (0,0): anon29_Then + (0,0): anon17 + (0,0): anon30_Then + (0,0): anon19 + +Dafny program verifier finished with 1 verified, 3 errors 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 index f5e47454..1a143edb 100644 --- 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 @@ -1,10 +1,10 @@ -some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (may loop 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]} (may loop 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]} (may loop with {x + 2 !in s}) - (!) Suppressing loops would leave this expression without triggers. +some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (may loop 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]} (may loop 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]} (may loop 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-picks-the-right-tokens.dfy.expect b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect index af274e75..f01ed1a0 100644 --- a/Test/triggers/splitting-picks-the-right-tokens.dfy.expect +++ b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect @@ -1,14 +1,14 @@ -splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {Id(x) > 1}: +splitting-picks-the-right-tokens.dfy(9,11): Info: For expression "Id(x) > 1": Selected triggers: {Id(x)} -splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {x > 2}: +splitting-picks-the-right-tokens.dfy(9,11): Info: For expression "x > 2": Selected triggers: {Id(x)} -splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {x > -1}: +splitting-picks-the-right-tokens.dfy(9,11): Info: For expression "x > -1": Selected triggers: {Id(x)} -splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> Id(x) > 1}: +splitting-picks-the-right-tokens.dfy(16,11): Info: For expression "x > 0 ==> Id(x) > 1": Selected triggers: {Id(x)} -splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> x > 2}: +splitting-picks-the-right-tokens.dfy(16,11): Info: For expression "x > 0 ==> x > 2": Selected triggers: {Id(x)} -splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> x > -1}: +splitting-picks-the-right-tokens.dfy(16,11): Info: For expression "x > 0 ==> x > -1": Selected triggers: {Id(x)} splitting-picks-the-right-tokens.dfy(20,12): Error BP5002: A precondition for this call might not hold. splitting-picks-the-right-tokens.dfy(16,11): Related location: This is the precondition that might not hold. diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect index 58c8dd2b..a8bb2345 100644 --- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect +++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect @@ -1,32 +1,32 @@ splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)} - Rejected triggers: {P(i)} (may loop with {P(i + 1)}) + Rejected triggers: {P(i)} (may loop with "P(i + 1)") splitting-triggers-recovers-expressivity.dfy(17,11): Info: Selected triggers: {Q(j)} - Rejected triggers: {P(j)} (may loop with {P(j + 1)}) + Rejected triggers: {P(j)} (may loop with "P(j + 1)") splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)} - Rejected triggers: {P(i)} (may loop with {P(i + 1)}) + Rejected triggers: {P(i)} (may loop with "P(i + 1)") splitting-triggers-recovers-expressivity.dfy(33,11): Info: Selected triggers: {Q(j)} - Rejected triggers: {P(j)} (may loop with {P(j + 1)}) -splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i)}: + Rejected triggers: {P(j)} (may loop 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)}: +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)}: +splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression "P(i + 1)": Selected triggers: {Q(i)} - Rejected triggers: {P(i)} (may loop with {P(i + 1)}) -splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> P(j)}: + Rejected triggers: {P(i)} (may loop 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)}: +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)} (may loop with {P(j + 1)}) -splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> Q(i)}: + Rejected triggers: {P(j)} (may loop 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)}: +splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression "i >= 0 ==> P(i) ==> P(i + 1)": Selected triggers: - {P(i)} (may loop with {P(i + 1)}), {Q(i)} + {P(i)} (may loop 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.expect b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect index c8e1a5fa..27548ac9 100644 --- a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect +++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect @@ -1,11 +1,11 @@ -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(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 diff --git a/Test/triggers/suppressing-warnings-behaves-properly.dfy b/Test/triggers/suppressing-warnings-behaves-properly.dfy new file mode 100644 index 00000000..237269e5 --- /dev/null +++ b/Test/triggers/suppressing-warnings-behaves-properly.dfy @@ -0,0 +1,21 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This file checks that suppressing warnings works properly + +predicate f(x: int) +predicate g(x: int) + +method M() { + assert forall n :: n >= 0 || n < 0; + assert forall n {:nowarn} :: n >= 0 || n < 0; + assert forall n {:autotriggers false} :: n >= 0 || n < 0; + + assert forall n: nat :: (n != 0) == f(n) || true; + assert forall n: nat {:nowarn} :: (n != 0) == f(n) || true; + assert forall n: nat {:autotriggers false} :: (n != 0) == f(n) || true; + + assert forall n: nat :: f(n) == f(n+1) || g(n) || true; + assert forall n: nat {:nowarn} :: (n != 0) == f(n) || true; + assert forall n: nat {:autotriggers false} :: (n != 0) == f(n) || true; +} diff --git a/Test/triggers/suppressing-warnings-behaves-properly.dfy.expect b/Test/triggers/suppressing-warnings-behaves-properly.dfy.expect new file mode 100644 index 00000000..124984b1 --- /dev/null +++ b/Test/triggers/suppressing-warnings-behaves-properly.dfy.expect @@ -0,0 +1,14 @@ +suppressing-warnings-behaves-properly.dfy(10,9): Warning: /!\ No terms found to trigger on. +suppressing-warnings-behaves-properly.dfy(11,9): Info: (Suppressed warning) No terms found to trigger on. +suppressing-warnings-behaves-properly.dfy(12,9): Info: Not generating triggers for "n >= 0 || n < 0". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead. +suppressing-warnings-behaves-properly.dfy(14,9): Info: Selected triggers: {f(n)} +suppressing-warnings-behaves-properly.dfy(15,9): Warning: Selected triggers: {f(n)} + /!\ There is no warning here to suppress. +suppressing-warnings-behaves-properly.dfy(16,9): Info: Not generating triggers for "(n != 0) == f(n) || true". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead. +suppressing-warnings-behaves-properly.dfy(18,9): Info: Selected triggers: {g(n)} + Rejected triggers: {f(n)} (may loop with "f(n + 1)") +suppressing-warnings-behaves-properly.dfy(19,9): Warning: Selected triggers: {f(n)} + /!\ There is no warning here to suppress. +suppressing-warnings-behaves-properly.dfy(20,9): Info: Not generating triggers for "(n != 0) == f(n) || true". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead. + +Dafny program verifier finished with 4 verified, 0 errors diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect index 2e9bbedf..d6b49a9e 100644 --- a/Test/triggers/useless-triggers-are-removed.dfy.expect +++ b/Test/triggers/useless-triggers-are-removed.dfy.expect @@ -5,11 +5,11 @@ useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)} {h(f(x))} (more specific than {f(x)}) {g(f(x))} (more specific than {f(x)}) useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))} - Rejected triggers: {f(x)} (may loop with {f(f(x))}) + Rejected triggers: {f(x)} (may loop with "f(f(x))") useless-triggers-are-removed.dfy(23,11): Info: Selected triggers: {g(f(x)), g(y)}, {f(y), f(x)} Rejected triggers: - {g(y), f(x)} (may loop with {g(f(y))}, {g(f(x))}) + {g(y), f(x)} (may loop with "g(f(y))", "g(f(x))") {g(f(x)), g(f(y))} (more specific than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)}) {g(f(x)), f(y)} (more specific than {f(y), f(x)}) {g(f(y)), f(x)} (more specific than {f(y), f(x)}) diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect index 6b152262..6c3e4853 100644 --- a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect +++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect @@ -1,16 +1,16 @@ -wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {0 <= f(n)}: +wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression "0 <= f(n)": Selected triggers: {f(n)} Rejected triggers: {P(f(n))} (more specific than {f(n)}) -wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {P(f(n))}: +wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression "P(f(n))": Selected triggers: {f(n)} Rejected triggers: {P(f(n))} (more specific than {f(n)}) -wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c != null}: +wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c != null": Selected triggers: {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s} -wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c' != null}: +wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c' != null": Selected triggers: {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s} -wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c.x == c'.x}: +wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c.x == c'.x": Selected triggers: {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s} -- cgit v1.2.3