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/triggers-prevent-some-inlining.dfy.expect | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 Test/triggers/triggers-prevent-some-inlining.dfy.expect (limited to 'Test/triggers/triggers-prevent-some-inlining.dfy.expect') diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect new file mode 100644 index 00000000..73ba063c --- /dev/null +++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 4 verified, 0 errors -- cgit v1.2.3 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/triggers-prevent-some-inlining.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 736969063f99babb854a2ac7c2c2b0d11a8fc253 Mon Sep 17 00:00:00 2001 From: leino Date: Sat, 24 Oct 2015 17:43:46 -0700 Subject: In method and iterator specifications, inline top-level predicates (except protected predicated in cross-module calls) like in other places. --- Source/Dafny/Translator.cs | 166 +++++++++++---------- Test/dafny0/TriggerInPredicate.dfy.expect | 1 + Test/dafny2/SnapshotableTrees.dfy.expect | 9 +- .../triggers-prevent-some-inlining.dfy.expect | 2 + 4 files changed, 98 insertions(+), 80 deletions(-) (limited to 'Test/triggers/triggers-prevent-some-inlining.dfy.expect') diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 7d3f570d..172005cc 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1466,13 +1466,15 @@ namespace Microsoft.Dafny { /// /// Returns true if the body of function "f" is available in module "context". - /// This happens when "f" has a body, "f" is not opaque, and either "f" is declared - /// in module "context" or "f" is not protected. + /// This happens when the following conditions all hold: + /// - "f" has a body + /// - "f" is not opaque + /// - "f" is declared as protected, then "context" is the current module and parameter "revealProtectedBody" is passed in as "true". /// - static bool FunctionBodyIsAvailable(Function f, ModuleDefinition context) { + static bool FunctionBodyIsAvailable(Function f, ModuleDefinition context, bool revealProtectedBody) { Contract.Requires(f != null); Contract.Requires(context != null); - return f.Body != null && !IsOpaqueFunction(f) && (f.EnclosingClass.Module == context || !f.IsProtected); + return f.Body != null && !IsOpaqueFunction(f) && (!f.IsProtected || (revealProtectedBody && f.EnclosingClass.Module == context)); } static bool IsOpaqueFunction(Function f) { Contract.Requires(f != null); @@ -1571,8 +1573,7 @@ namespace Microsoft.Dafny { req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment)); comment = null; } else { - bool splitHappened; // we actually don't care - foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, true, out splitHappened)) { + foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { if (kind == MethodTranslationKind.IntraModuleCall && RefinementToken.IsInherited(s.E.tok, currentModule)) { // this precondition was inherited into this module, so just ignore it } else { @@ -1589,8 +1590,7 @@ namespace Microsoft.Dafny { ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, comment)); comment = null; } else { - bool splitHappened; // we actually don't care - foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, true, out splitHappened)) { + foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) { // this postcondition was inherited into this module, so just ignore it } else { @@ -2966,7 +2966,7 @@ namespace Microsoft.Dafny { { var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f); var splits = new List(); - bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight,false, etran); + bool splitHappened/*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, true, false, etran); foreach (var s in splits) { if (s.IsChecked && !RefinementToken.IsInherited(s.E.tok, currentModule)) @@ -3975,7 +3975,7 @@ namespace Microsoft.Dafny { foreach (Expression p in f.Ens) { var functionHeight = currentModule.CallGraph.GetSCCRepresentativeId(f); var splits = new List(); - bool splitHappened /*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, true, etran); + bool splitHappened /*we actually don't care*/ = TrSplitExpr(p, splits, true, functionHeight, true, true, etran); foreach (var s in splits) { if (s.IsChecked && !RefinementToken.IsInherited(s.E.tok, currentModule)) { ens.Add(Ensures(s.E.tok, false, s.E, null, null)); @@ -6233,8 +6233,7 @@ namespace Microsoft.Dafny { req.Add(Requires(p.E.tok, true, etran.TrExpr(p.E), null, comment)); comment = null; } else { - bool splitHappened; // we actually don't care - foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, true /* kind == MethodTranslationKind.Implementation */, out splitHappened)) { + foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { if (s.IsOnlyChecked && bodyKind) { // don't include in split } else if (s.IsOnlyFree && !bodyKind) { @@ -6254,8 +6253,7 @@ namespace Microsoft.Dafny { if (p.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) { ens.Add(Ensures(p.E.tok, true, etran.TrExpr(p.E), null, null)); } else { - bool splitHappened; // we actually don't care - foreach (var s in TrSplitExpr(p.E, etran, kind == MethodTranslationKind.InterModuleCall ? 0 : int.MaxValue, true /* kind == MethodTranslationKind.Implementation */ , out splitHappened)) { + foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { var post = s.E; if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.E.tok, currentModule)) { // this postcondition was inherited into this module, so make it into the form "$_reverifyPost ==> s.E" @@ -11115,7 +11113,7 @@ namespace Microsoft.Dafny { result = translator.CondApplyUnbox(e.tok, result, e.Function.ResultType, e.Type); bool callIsLit = argsAreLit - && Translator.FunctionBodyIsAvailable(e.Function, translator.currentModule) + && Translator.FunctionBodyIsAvailable(e.Function, translator.currentModule, true) && !e.Function.Reads.Any(); // Function could depend on external values if (callIsLit) { result = MaybeLit(result, ty); @@ -12754,18 +12752,20 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result>() != null); var splits = new List(); - splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, apply_induction, etran); + splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, true, apply_induction, etran); return splits; } - List/*!*/ TrSplitExpr(Expression expr, ExpressionTranslator etran, int heightLimit, bool apply_induction, out bool splitHappened) + List TrSplitExprForMethodSpec(Expression expr, ExpressionTranslator etran, MethodTranslationKind kind) { Contract.Requires(expr != null); Contract.Requires(etran != null); Contract.Ensures(Contract.Result>() != null); var splits = new List(); - splitHappened = TrSplitExpr(expr, splits, true, heightLimit, apply_induction, etran); + var apply_induction = true;/*kind == MethodTranslationKind.Implementation*/; + bool splitHappened; // we don't actually care + splitHappened = TrSplitExpr(expr, splits, true, int.MaxValue, kind != MethodTranslationKind.InterModuleCall, apply_induction, etran); return splits; } @@ -12795,7 +12795,7 @@ namespace Microsoft.Dafny { /// if its body is available in the current context and its height is less than "heightLimit" (if "heightLimit" is /// passed in as 0, then no functions will be inlined). /// - bool TrSplitExpr(Expression expr, List/*!*/ splits, bool position, int heightLimit, bool apply_induction, ExpressionTranslator etran) { + bool TrSplitExpr(Expression expr, List/*!*/ splits, bool position, int heightLimit, bool inlineProtectedFunctions, bool apply_induction, ExpressionTranslator etran) { Contract.Requires(expr != null); Contract.Requires(expr.Type.IsBoolType || (expr is BoxingCastExpr && ((BoxingCastExpr)expr).E.Type.IsBoolType)); Contract.Requires(splits != null); @@ -12804,7 +12804,7 @@ namespace Microsoft.Dafny { if (expr is BoxingCastExpr) { var bce = (BoxingCastExpr)expr; var ss = new List(); - if (TrSplitExpr(bce.E, ss, position, heightLimit, apply_induction, etran)) { + if (TrSplitExpr(bce.E, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) { foreach (var s in ss) { splits.Add(new SplitExprInfo(s.Kind, CondApplyBox(s.E.tok, s.E, bce.FromType, bce.ToType))); } @@ -12813,22 +12813,22 @@ namespace Microsoft.Dafny { } else if (expr is ConcreteSyntaxExpression) { var e = (ConcreteSyntaxExpression)expr; - return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, apply_induction, etran); + return TrSplitExpr(e.ResolvedExpression, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); } else if (expr is LetExpr) { var e = (LetExpr)expr; if (e.Exact) { - return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, heightLimit, apply_induction, etran); + return TrSplitExpr(etran.GetSubstitutedBody(e), splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); } else { var d = LetDesugaring(e); - return TrSplitExpr(d, splits, position, heightLimit, apply_induction, etran); + return TrSplitExpr(d, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); } } else if (expr is UnaryOpExpr) { var e = (UnaryOpExpr)expr; if (e.Op == UnaryOpExpr.Opcode.Not) { var ss = new List(); - if (TrSplitExpr(e.E, ss, !position, heightLimit, apply_induction, etran)) { + if (TrSplitExpr(e.E, ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran)) { foreach (var s in ss) { splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Unary(s.E.tok, UnaryOperator.Opcode.Not, s.E))); } @@ -12839,13 +12839,13 @@ namespace Microsoft.Dafny { } else if (expr is BinaryExpr) { var bin = (BinaryExpr)expr; if (position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And) { - TrSplitExpr(bin.E0, splits, position, heightLimit, apply_induction, etran); - TrSplitExpr(bin.E1, splits, position, heightLimit, apply_induction, etran); + TrSplitExpr(bin.E0, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); + TrSplitExpr(bin.E1, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); return true; } else if (!position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) { - TrSplitExpr(bin.E0, splits, position, heightLimit, apply_induction, etran); - TrSplitExpr(bin.E1, splits, position, heightLimit, apply_induction, etran); + TrSplitExpr(bin.E0, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); + TrSplitExpr(bin.E1, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); return true; } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) { @@ -12853,14 +12853,14 @@ namespace Microsoft.Dafny { if (position) { var lhs = etran.TrExpr(bin.E0); var ss = new List(); - TrSplitExpr(bin.E1, ss, position, heightLimit, apply_induction, etran); + TrSplitExpr(bin.E1, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); foreach (var s in ss) { // as the source location in the following implication, use that of the translated "s" splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, lhs, s.E))); } } else { var ss = new List(); - TrSplitExpr(bin.E0, ss, !position, heightLimit, apply_induction, etran); + TrSplitExpr(bin.E0, ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran); var rhs = etran.TrExpr(bin.E1); foreach (var s in ss) { // as the source location in the following implication, use that of the translated "s" @@ -12907,8 +12907,8 @@ namespace Microsoft.Dafny { var ssThen = new List(); var ssElse = new List(); - TrSplitExpr(ite.Thn, ssThen, position, heightLimit, apply_induction, etran); - TrSplitExpr(ite.Els, ssElse, position, heightLimit, apply_induction, etran); + TrSplitExpr(ite.Thn, ssThen, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); + TrSplitExpr(ite.Els, ssElse, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); var op = position ? BinaryOperator.Opcode.Imp : BinaryOperator.Opcode.And; var test = etran.TrExpr(ite.Test); @@ -12934,14 +12934,14 @@ namespace Microsoft.Dafny { if (position) { var conclusion = etran.TrExpr(e.GetSConclusion()); var ss = new List(); - TrSplitExpr(e.E, ss, position, heightLimit, apply_induction, etran); + TrSplitExpr(e.E, ss, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); foreach (var s in ss) { // as the source location in the following implication, use that of the translated "s" splits.Add(new SplitExprInfo(s.Kind, Bpl.Expr.Binary(s.E.tok, BinaryOperator.Opcode.Imp, conclusion, s.E))); } } else { var ss = new List(); - TrSplitExpr(e.GetSConclusion(), ss, !position, heightLimit, apply_induction, etran); + TrSplitExpr(e.GetSConclusion(), ss, !position, heightLimit, inlineProtectedFunctions, apply_induction, etran); var rhs = etran.TrExpr(e.E); foreach (var s in ss) { // as the source location in the following implication, use that of the translated "s" @@ -12952,7 +12952,7 @@ namespace Microsoft.Dafny { } else if (expr is OldExpr) { var e = (OldExpr)expr; - return TrSplitExpr(e.E, splits, position, heightLimit, apply_induction, etran.Old); + return TrSplitExpr(e.E, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran.Old); } else if (expr is FunctionCallExpr && position) { var fexp = (FunctionCallExpr)expr; @@ -12961,22 +12961,17 @@ namespace Microsoft.Dafny { var module = f.EnclosingClass.Module; var functionHeight = module.CallGraph.GetSCCRepresentativeId(f); - if (module == currentModule && functionHeight < heightLimit && f.Body != null && !(f.Body.Resolved is MatchExpr)) { + if (functionHeight < heightLimit && f.Body != null && !(f.Body.Resolved is MatchExpr)) { if (RefinementToken.IsInherited(fexp.tok, currentModule) && f is Predicate && ((Predicate)f).BodyOrigin == Predicate.BodyOriginKind.DelayedDefinition && (codeContext == null || !codeContext.MustReverify)) { // The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything // that needed to be proved about the function was proved already in the previous module, even without the body definition). - } else if (!FunctionBodyIsAvailable(f, currentModule)) { + } else if (!FunctionBodyIsAvailable(f, currentModule, inlineProtectedFunctions)) { // Don't inline opaque functions or foreign protected functions } else if (Attributes.Contains(f.Attributes, "no_inline")) { // User manually prevented inlining - } else if (CanSafelyInline(fexp, f)) { - // inline this body - var body = GetSubstitutedBody(fexp, f, false); - var typeSpecializedBody = GetSubstitutedBody(fexp, f, true); - var typeSpecializedResultType = Resolver.SubstType(f.ResultType, fexp.TypeArgumentSubstitutions); - + } else { // Produce, for a "body" split into b0, b1, b2: // checked F#canCall(args) ==> F(args) || b0 // checked F#canCall(args) ==> F(args) || b1 @@ -12999,49 +12994,62 @@ namespace Microsoft.Dafny { // F(args) fargs = etran.TrExpr(fexp); - // recurse on body - var ss = new List(); - TrSplitExpr(typeSpecializedBody, ss, position, functionHeight, apply_induction, etran); - var needsTokenAdjust = TrSplitNeedsTokenAdjustment(typeSpecializedBody); - foreach (var s in ss) { - if (s.IsChecked) { - var unboxedConjunct = CondApplyUnbox(s.E.tok, s.E, typeSpecializedResultType, expr.Type); - var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct); - var tok = needsTokenAdjust ? (IToken)new ForceCheckToken(typeSpecializedBody.tok) : (IToken)new NestedToken(fexp.tok, s.E.tok); - var p = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct); - splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p)); + if (!CanSafelyInline(fexp, f)) { + // Skip inlining, as it would cause arbitrary expressions to pop up in the trigger + // TODO this should appear at the outmost call site, not at the innermost. See SnapshotableTrees.dfy + reporter.Info(MessageSource.Translator, fexp.tok, "Some instances of this call cannot safely be inlined."); + // F#canCall(args) ==> F(args) + var p = Bpl.Expr.Binary(fargs.tok, BinaryOperator.Opcode.Imp, canCall, fargs); + splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p)); + // F#canCall(args) && F(args) + var fr = Bpl.Expr.And(canCall, fargs); + splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr)); + + } else { + // inline this body + var typeSpecializedBody = GetSubstitutedBody(fexp, f); + var typeSpecializedResultType = Resolver.SubstType(f.ResultType, fexp.TypeArgumentSubstitutions); + + // recurse on body + var ss = new List(); + TrSplitExpr(typeSpecializedBody, ss, position, functionHeight, inlineProtectedFunctions, apply_induction, etran); + var needsTokenAdjust = TrSplitNeedsTokenAdjustment(typeSpecializedBody); + foreach (var s in ss) { + if (s.IsChecked) { + var unboxedConjunct = CondApplyUnbox(s.E.tok, s.E, typeSpecializedResultType, expr.Type); + var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct); + var tok = needsTokenAdjust ? (IToken)new ForceCheckToken(typeSpecializedBody.tok) : (IToken)new NestedToken(fexp.tok, s.E.tok); + var p = Bpl.Expr.Binary(tok, BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct); + splits.Add(new SplitExprInfo(SplitExprInfo.K.Checked, p)); + } } - } - // allocatedness for arguments to the inlined call in body - if (typeSpecializedBody is FunctionCallExpr) { - FunctionCallExpr e = (FunctionCallExpr)typeSpecializedBody; - for (int i = 0; i < e.Args.Count; i++) { - Expression ee = e.Args[i]; - Type t = e.Function.Formals[i].Type; - Expr tr_ee = etran.TrExpr(ee); - Bpl.Expr wh = GetWhereClause(e.tok, tr_ee, cce.NonNull(ee.Type), etran); - if (wh != null) { fargs = Bpl.Expr.And(fargs, wh); } + // allocatedness for arguments to the inlined call in body + if (typeSpecializedBody is FunctionCallExpr) { + FunctionCallExpr e = (FunctionCallExpr)typeSpecializedBody; + for (int i = 0; i < e.Args.Count; i++) { + Expression ee = e.Args[i]; + Type t = e.Function.Formals[i].Type; + Expr tr_ee = etran.TrExpr(ee); + Bpl.Expr wh = GetWhereClause(e.tok, tr_ee, cce.NonNull(ee.Type), etran); + if (wh != null) { fargs = Bpl.Expr.And(fargs, wh); } + } } - } - // body - var trBody = etran.TrExpr(typeSpecializedBody); - trBody = CondApplyUnbox(trBody.tok, trBody, typeSpecializedResultType, expr.Type); - // F#canCall(args) && F(args) && (b0 && b1 && b2) - var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody)); - splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr)); + // body + var trBody = etran.TrExpr(typeSpecializedBody); + trBody = CondApplyUnbox(trBody.tok, trBody, typeSpecializedResultType, expr.Type); + // F#canCall(args) && F(args) && (b0 && b1 && b2) + var fr = Bpl.Expr.And(canCall, BplAnd(fargs, trBody)); + splits.Add(new SplitExprInfo(SplitExprInfo.K.Free, fr)); + } return true; - } else { - // Skip inlining, as it would cause arbitrary expressions to pop up in the trigger - // TODO this should appear at the outmost call site, not at the innermost. See SnapshotableTrees.dfy - reporter.Info(MessageSource.Translator, fexp.tok, "Some instances of this call cannot safely be inlined."); } } } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier != null) { - return TrSplitExpr(((QuantifierExpr)expr).SplitQuantifierExpression, splits, position, heightLimit, apply_induction, etran); + return TrSplitExpr(((QuantifierExpr)expr).SplitQuantifierExpression, splits, position, heightLimit, inlineProtectedFunctions, apply_induction, etran); } else if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) /* NB: only for type arg less quantifiers for now: */ && ((QuantifierExpr)expr).TypeArgs.Count == 0) { @@ -13220,14 +13228,14 @@ namespace Microsoft.Dafny { } } - private Expression GetSubstitutedBody(FunctionCallExpr fexp, Function f, bool specializeTypeParameters) { + private Expression GetSubstitutedBody(FunctionCallExpr fexp, Function f) { Contract.Requires(fexp != null); Contract.Requires(f != null); var substMap = new Dictionary(); Contract.Assert(fexp.Args.Count == f.Formals.Count); for (int i = 0; i < f.Formals.Count; i++) { Formal p = f.Formals[i]; - var formalType = specializeTypeParameters ? Resolver.SubstType(p.Type, fexp.TypeArgumentSubstitutions) : p.Type; + var formalType = Resolver.SubstType(p.Type, fexp.TypeArgumentSubstitutions); Expression arg = fexp.Args[i]; arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), formalType); arg.Type = formalType; // resolve here @@ -13238,7 +13246,7 @@ namespace Microsoft.Dafny { var pp = (PrefixPredicate)f; body = PrefixSubstitution(pp, body); } - body = Substitute(body, fexp.Receiver, substMap, specializeTypeParameters ? fexp.TypeArgumentSubstitutions : null); + body = Substitute(body, fexp.Receiver, substMap, fexp.TypeArgumentSubstitutions); return body; } diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect index b3fb9cc0..b3d4ff34 100644 --- a/Test/dafny0/TriggerInPredicate.dfy.expect +++ b/Test/dafny0/TriggerInPredicate.dfy.expect @@ -2,5 +2,6 @@ TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "A(x, y)". TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "z". TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined. TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined. +TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined. Dafny program verifier finished with 8 verified, 0 errors diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect index 808fe0f9..68b4ff73 100644 --- a/Test/dafny2/SnapshotableTrees.dfy.expect +++ b/Test/dafny2/SnapshotableTrees.dfy.expect @@ -1,8 +1,15 @@ SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold. SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold. +SnapshotableTrees.dfy(545,15): Related location +Execution trace: + (0,0): anon0 + (0,0): anon3_Then +SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold. +SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold. +SnapshotableTrees.dfy(548,18): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -Dafny program verifier finished with 65 verified, 1 error +Dafny program verifier finished with 65 verified, 2 errors Compiled assembly into SnapshotableTrees.exe diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect index 4c24893e..0b6f3e30 100644 --- a/Test/triggers/triggers-prevent-some-inlining.dfy.expect +++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect @@ -3,5 +3,7 @@ triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call can 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. +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 -- cgit v1.2.3