From 5eb855972c191ed6323253329fc50ebd1683fdd6 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 1 Jul 2016 02:17:05 -0700 Subject: [PATCH] Merge split quantifiers with same triggers into one Group split quantifiers by what triggers they got, and merged them back into one quantifier. --- Source/Dafny/Triggers/QuantifierSplitter.cs | 24 ++---- .../Dafny/Triggers/QuantifiersCollection.cs | 81 +++++++++++++++++- Source/Dafny/Triggers/QuantifiersCollector.cs | 6 +- Source/Dafny/Triggers/TriggerUtils.cs | 8 ++ Test/dafny0/AutoReq.dfy.expect | 8 +- Test/dafny0/TriggerInPredicate.dfy.expect | 3 +- Test/dafny4/git-issue2.dfy | 83 +++++++++++++++++++ Test/dafny4/git-issue2.dfy.expect | 2 + ...ction-applications-are-triggers.dfy.expect | 8 +- ...-detection-messages--unit-tests.dfy.expect | 22 ++--- ...ok-like-the-triggers-they-match.dfy.expect | 8 +- ...plitting-picks-the-right-tokens.dfy.expect | 28 +------ ...-triggers-recovers-expressivity.dfy.expect | 13 +-- ...ter-precondition-related-errors.dfy.expect | 23 +---- ...cks-use-the-original-quantifier.dfy.expect | 19 +---- 15 files changed, 208 insertions(+), 128 deletions(-) create mode 100644 Test/dafny4/git-issue2.dfy create mode 100644 Test/dafny4/git-issue2.dfy.expect diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index 7ef7d5c949..eab000cb6c 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -5,8 +5,10 @@ using System.Linq; using System.Text; -namespace Microsoft.Dafny.Triggers { - class QuantifierSplitter : BottomUpVisitor { +namespace Microsoft.Dafny.Triggers +{ + class QuantifierSplitter : BottomUpVisitor + { /// This cache was introduced because some statements (notably calc) return the same SubExpression multiple times. /// This ended up causing an inconsistent situation when the calc statement's subexpressions contained the same quantifier /// twice: on the first pass that quantifier got its SplitQuantifiers generated, and on the the second pass these @@ -21,7 +23,7 @@ class QuantifierSplitter : BottomUpVisitor { return BinaryExpr.Opcode.And; } else { throw new ArgumentException(); - } + } } // NOTE: If we wanted to split quantifiers as far as possible, it would be @@ -35,14 +37,6 @@ class QuantifierSplitter : BottomUpVisitor { return new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type }; } - private static Attributes CopyAttributes(Attributes source) { - if (source == null) { - return null; - } else { - return new Attributes(source.Name, source.Args, CopyAttributes(source.Prev)); - } - } - internal static IEnumerable SplitExpr(Expression expr, BinaryExpr.Opcode separator) { expr = expr.Resolved; var unary = expr as UnaryOpExpr; @@ -81,7 +75,7 @@ class QuantifierSplitter : BottomUpVisitor { } foreach (var e in stream) { var tok = new NestedToken(quantifier.tok, e.tok); - yield return new ForallExpr(tok, ((ForallExpr)quantifier).TypeArgs, quantifier.BoundVars, quantifier.Range, e, CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type }; + yield return new ForallExpr(tok, ((ForallExpr)quantifier).TypeArgs, quantifier.BoundVars, quantifier.Range, e, TriggerUtils.CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type }; } } else if (quantifier is ExistsExpr) { IEnumerable stream; @@ -92,16 +86,16 @@ class QuantifierSplitter : BottomUpVisitor { } foreach (var e in stream) { var tok = new NestedToken(quantifier.tok, e.tok); - yield return new ExistsExpr(tok, ((ExistsExpr)quantifier).TypeArgs, quantifier.BoundVars, quantifier.Range, e, CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type }; + yield return new ExistsExpr(tok, ((ExistsExpr)quantifier).TypeArgs, quantifier.BoundVars, quantifier.Range, e, TriggerUtils.CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type }; } } else { yield return quantifier; } } - + private static bool AllowsSplitting(ComprehensionExpr quantifier) { // allow split if attributes doesn't contains "split" or it is "split: true" and it is not an empty QuantifierExpr (boundvar.count>0) - bool splitAttr = true; + bool splitAttr = true; return (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) && (quantifier.BoundVars.Count > 0); } diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 21a076a4f5..5ac151a071 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -31,11 +31,13 @@ class QuantifierWithTriggers { class QuantifiersCollection { readonly ErrorReporter reporter; - readonly List quantifiers; + readonly ComprehensionExpr expr; // the expression where the splits are originated from + List quantifiers; - internal QuantifiersCollection(IEnumerable quantifiers, ErrorReporter reporter) { + internal QuantifiersCollection(ComprehensionExpr expr, IEnumerable quantifiers, ErrorReporter reporter) { Contract.Requires(quantifiers.All(q => !(q is QuantifierExpr) || ((QuantifierExpr)q).SplitQuantifier == null)); this.reporter = reporter; + this.expr = expr; this.quantifiers = quantifiers.Select(q => new QuantifierWithTriggers(q)).ToList(); } @@ -45,6 +47,7 @@ class QuantifiersCollection { BuildDependenciesGraph(); SuppressMatchingLoops(); SelectTriggers(); + CombineSplitQuantifier(); } private bool SubsetGenerationPredicate(TriggerUtils.SetOfTerms terms, TriggerTerm additionalTerm) { @@ -151,6 +154,80 @@ class QuantifiersCollection { } } + internal class QuantifierGroup + { + internal QuantifierWithTriggers quantifier; + internal List expressions; + + public QuantifierGroup(QuantifierWithTriggers q, List expressions) { + this.quantifier = q; + this.expressions = expressions; + } + } + + // group split quantifier by what triggers they got, and merged them back into one quantifier. + private void CombineSplitQuantifier() { + if (quantifiers.Count > 1) { + List groups = new List(); + groups.Add(new QuantifierGroup(quantifiers[0], new List { quantifiers[0].quantifier })); + for (int i = 1; i < quantifiers.Count; i++) { + bool found = false; + for (int j = 0; j < groups.Count; j++) { + if (HasSameTriggers(quantifiers[i], groups[j].quantifier)) { + // belong to the same group + groups[j].expressions.Add(quantifiers[i].quantifier); + found = true; + break; + } + } + if (!found) { + // start a new group + groups.Add(new QuantifierGroup(quantifiers[i], new List { quantifiers[i].quantifier })); + } + } + if (groups.Count == quantifiers.Count) { + // have the same number of splits, so no splits are combined. + return; + } + // merge expressions in each group back to one quantifier. + List list = new List(); + List splits = new List(); + foreach (var group in groups) { + QuantifierWithTriggers q = group.quantifier; + if (q.quantifier is ForallExpr) { + ForallExpr quantifier = (ForallExpr)q.quantifier; + Expression expr = QuantifiersToExpression(quantifier.tok, BinaryExpr.ResolvedOpcode.And, group.expressions); + q.quantifier = new ForallExpr(quantifier.tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, expr, TriggerUtils.CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type }; + } else if (q.quantifier is ExistsExpr) { + ExistsExpr quantifier = (ExistsExpr)q.quantifier; + Expression expr = QuantifiersToExpression(quantifier.tok, BinaryExpr.ResolvedOpcode.Or, group.expressions); + q.quantifier = new ExistsExpr(quantifier.tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, expr, TriggerUtils.CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type }; + } + list.Add(q); + splits.Add(q.quantifier); + } + this.quantifiers = list; + Contract.Assert(this.expr is QuantifierExpr); // only QuantifierExpr has SplitQuantifier + ((QuantifierExpr)this.expr).SplitQuantifier = splits; + } + } + + private bool HasSameTriggers(QuantifierWithTriggers one, QuantifierWithTriggers other) { + return TriggerUtils.SameLists(one.Candidates, other.Candidates, SameTriggerCandidate); + } + + private static bool SameTriggerCandidate(TriggerCandidate arg1, TriggerCandidate arg2) { + return TriggerUtils.SameLists(arg1.Terms, arg2.Terms, TriggerTerm.Eq); + } + + private Expression QuantifiersToExpression(IToken tok, BinaryExpr.ResolvedOpcode op, List expressions) { + var expr = expressions[0].Term; + for (int i = 1; i < expressions.Count; i++) { + expr = new BinaryExpr(tok, op, expr, expressions[i].Term); + } + return expr; + } + private void CommitOne(QuantifierWithTriggers q, bool addHeader) { var errorLevel = ErrorLevel.Info; var msg = new StringBuilder(); diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs index 07399a02cc..cc040766d2 100644 --- a/Source/Dafny/Triggers/QuantifiersCollector.cs +++ b/Source/Dafny/Triggers/QuantifiersCollector.cs @@ -25,16 +25,16 @@ internal class QuantifierCollector : TopDownVisitor { if (e != null && (e.BoundVars.Count > 0) && !quantifiers.Contains(e)) { if (e is SetComprehension || e is MapComprehension) { quantifiers.Add(e); - quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(e, 1), reporter)); + quantifierCollections.Add(new QuantifiersCollection(e, Enumerable.Repeat(e, 1), reporter)); } else if (e is ForallExpr || e is ExistsExpr) { var quantifier = e as QuantifierExpr; quantifiers.Add(quantifier); if (quantifier.SplitQuantifier != null) { var collection = quantifier.SplitQuantifier.Select(q => q as ComprehensionExpr).Where(q => q != null); - quantifierCollections.Add(new QuantifiersCollection(collection, reporter)); + quantifierCollections.Add(new QuantifiersCollection(e, collection, reporter)); quantifiers.UnionWith(quantifier.SplitQuantifier); } else { - quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter)); + quantifierCollections.Add(new QuantifiersCollection(e, Enumerable.Repeat(quantifier, 1), reporter)); } } } diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index a8f1499aae..60a6d0a6df 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -15,6 +15,14 @@ class TriggerUtils { return copy; } + public static Attributes CopyAttributes(Attributes source) { + if (source == null) { + return null; + } else { + return new Attributes(source.Name, source.Args, CopyAttributes(source.Prev)); + } + } + internal class SetOfTerms { internal bool IsRedundant { get; private set; } internal List Terms { get; set; } diff --git a/Test/dafny0/AutoReq.dfy.expect b/Test/dafny0/AutoReq.dfy.expect index 25f00797e8..8e389f2cc5 100644 --- a/Test/dafny0/AutoReq.dfy.expect +++ b/Test/dafny0/AutoReq.dfy.expect @@ -1,11 +1,5 @@ AutoReq.dfy(247,4): Error: possible violation of function precondition AutoReq.dfy(239,13): Related location -AutoReq.dfy(239,59): Related location -Execution trace: - (0,0): anon0 - (0,0): anon4_Else -AutoReq.dfy(247,4): Error: possible violation of function precondition -AutoReq.dfy(239,13): Related location AutoReq.dfy(239,35): Related location Execution trace: (0,0): anon0 @@ -49,4 +43,4 @@ Execution trace: (0,0): anon0 (0,0): anon11_Then -Dafny program verifier finished with 52 verified, 9 errors +Dafny program verifier finished with 52 verified, 8 errors diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect index b3d4ff34d1..8d42a37c75 100644 --- a/Test/dafny0/TriggerInPredicate.dfy.expect +++ b/Test/dafny0/TriggerInPredicate.dfy.expect @@ -1,5 +1,4 @@ -TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "A(x, y)". -TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "z". +TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "A(x, y) && 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. diff --git a/Test/dafny4/git-issue2.dfy b/Test/dafny4/git-issue2.dfy new file mode 100644 index 0000000000..76bed9bcd8 --- /dev/null +++ b/Test/dafny4/git-issue2.dfy @@ -0,0 +1,83 @@ +// RUN: %dafny /rprint:"%t.rprint" /print:"%t.print" /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type sp_state +type operand = int + +function sp_op_const(c:int) : int { c } + +predicate {:opaque} InBounds(s:sp_state, o:operand, v:int) +{ + 0 <= o < 0x1_0000_0000 +} + +lemma lemma_K_InBounds() + ensures forall s:sp_state :: + InBounds(s, sp_op_const(0x428a2f98), 0x428a2f98) && + InBounds(s, sp_op_const(0x71374491), 0x71374491) && + InBounds(s, sp_op_const(0xb5c0fbcf), 0xb5c0fbcf) && + InBounds(s, sp_op_const(0xe9b5dba5), 0xe9b5dba5) && + InBounds(s, sp_op_const(0x3956c25b), 0x3956c25b) && + InBounds(s, sp_op_const(0x59f111f1), 0x59f111f1) && + InBounds(s, sp_op_const(0x923f82a4), 0x923f82a4) && + InBounds(s, sp_op_const(0xab1c5ed5), 0xab1c5ed5) && + InBounds(s, sp_op_const(0xd807aa98), 0xd807aa98) && + InBounds(s, sp_op_const(0x12835b01), 0x12835b01) && + InBounds(s, sp_op_const(0x243185be), 0x243185be) && + InBounds(s, sp_op_const(0x550c7dc3), 0x550c7dc3) && + InBounds(s, sp_op_const(0x72be5d74), 0x72be5d74) && + InBounds(s, sp_op_const(0x80deb1fe), 0x80deb1fe) && + InBounds(s, sp_op_const(0x9bdc06a7), 0x9bdc06a7) && + InBounds(s, sp_op_const(0xc19bf174), 0xc19bf174) && + InBounds(s, sp_op_const(0xe49b69c1), 0xe49b69c1) && + InBounds(s, sp_op_const(0xefbe4786), 0xefbe4786) && + InBounds(s, sp_op_const(0x0fc19dc6), 0x0fc19dc6) && + InBounds(s, sp_op_const(0x240ca1cc), 0x240ca1cc) && + InBounds(s, sp_op_const(0x2de92c6f), 0x2de92c6f) && + InBounds(s, sp_op_const(0x4a7484aa), 0x4a7484aa) && + InBounds(s, sp_op_const(0x5cb0a9dc), 0x5cb0a9dc) && + InBounds(s, sp_op_const(0x76f988da), 0x76f988da) && + InBounds(s, sp_op_const(0x983e5152), 0x983e5152) && + InBounds(s, sp_op_const(0xa831c66d), 0xa831c66d) && + InBounds(s, sp_op_const(0xb00327c8), 0xb00327c8) && + InBounds(s, sp_op_const(0xbf597fc7), 0xbf597fc7) && + InBounds(s, sp_op_const(0xc6e00bf3), 0xc6e00bf3) && + InBounds(s, sp_op_const(0xd5a79147), 0xd5a79147) && + InBounds(s, sp_op_const(0x06ca6351), 0x06ca6351) && + InBounds(s, sp_op_const(0x14292967), 0x14292967) && + InBounds(s, sp_op_const(0x27b70a85), 0x27b70a85) && + InBounds(s, sp_op_const(0x2e1b2138), 0x2e1b2138) && + InBounds(s, sp_op_const(0x4d2c6dfc), 0x4d2c6dfc) && + InBounds(s, sp_op_const(0x53380d13), 0x53380d13) && + InBounds(s, sp_op_const(0x650a7354), 0x650a7354) && + InBounds(s, sp_op_const(0x766a0abb), 0x766a0abb) && + InBounds(s, sp_op_const(0x81c2c92e), 0x81c2c92e) && + InBounds(s, sp_op_const(0x92722c85), 0x92722c85) && + InBounds(s, sp_op_const(0xa2bfe8a1), 0xa2bfe8a1) && + InBounds(s, sp_op_const(0xa81a664b), 0xa81a664b) && + InBounds(s, sp_op_const(0xc24b8b70), 0xc24b8b70) && + InBounds(s, sp_op_const(0xc76c51a3), 0xc76c51a3) && + InBounds(s, sp_op_const(0xd192e819), 0xd192e819) && + InBounds(s, sp_op_const(0xd6990624), 0xd6990624) && + InBounds(s, sp_op_const(0xf40e3585), 0xf40e3585) && + InBounds(s, sp_op_const(0x106aa070), 0x106aa070) && + InBounds(s, sp_op_const(0x19a4c116), 0x19a4c116) && + InBounds(s, sp_op_const(0x1e376c08), 0x1e376c08) && + InBounds(s, sp_op_const(0x2748774c), 0x2748774c) && + InBounds(s, sp_op_const(0x34b0bcb5), 0x34b0bcb5) && + InBounds(s, sp_op_const(0x391c0cb3), 0x391c0cb3) && + InBounds(s, sp_op_const(0x4ed8aa4a), 0x4ed8aa4a) && + InBounds(s, sp_op_const(0x5b9cca4f), 0x5b9cca4f) && + InBounds(s, sp_op_const(0x682e6ff3), 0x682e6ff3) && + InBounds(s, sp_op_const(0x748f82ee), 0x748f82ee) && + InBounds(s, sp_op_const(0x78a5636f), 0x78a5636f) && + InBounds(s, sp_op_const(0x84c87814), 0x84c87814) && + InBounds(s, sp_op_const(0x8cc70208), 0x8cc70208) && + InBounds(s, sp_op_const(0x90befffa), 0x90befffa) && + InBounds(s, sp_op_const(0xa4506ceb), 0xa4506ceb) && + InBounds(s, sp_op_const(0xbef9a3f7), 0xbef9a3f7) && + InBounds(s, sp_op_const(0xc67178f2), 0xc67178f2) +{ reveal_InBounds(); } + + + diff --git a/Test/dafny4/git-issue2.dfy.expect b/Test/dafny4/git-issue2.dfy.expect new file mode 100644 index 0000000000..e4e323ccb5 --- /dev/null +++ b/Test/dafny4/git-issue2.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 5 verified, 0 errors diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect index 1214536dd4..b840623255 100644 --- a/Test/triggers/function-applications-are-triggers.dfy.expect +++ b/Test/triggers/function-applications-are-triggers.dfy.expect @@ -1,10 +1,6 @@ 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(10,9): Info: 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: diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect index eba8c1796b..6998fe9772 100644 --- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect +++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect @@ -9,28 +9,16 @@ loop-detection-messages--unit-tests.dfy(15,9): Info: For expression "false ==> f 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)": - 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)": - Selected triggers: {f(i)} +loop-detection-messages--unit-tests.dfy(16,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(17,9): Info: Selected triggers: {f(i)} (may loop with "f(i + 1)") 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". 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)": - 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(25,9): Info: Selected triggers: {g(j), f(i)} +loop-detection-messages--unit-tests.dfy(26,9): Warning: /!\ 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)". 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 1a143edb00..e152a10823 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,6 @@ 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(15,17): Warning: Selected triggers: {s[x]} (may loop with "s[x + 1]") + /!\ 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 f01ed1a0b0..202491c3d2 100644 --- a/Test/triggers/splitting-picks-the-right-tokens.dfy.expect +++ b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect @@ -1,21 +1,5 @@ -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": - Selected triggers: {Id(x)} -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": - Selected triggers: {Id(x)} -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": - 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. -splitting-picks-the-right-tokens.dfy(16,48): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Then +splitting-picks-the-right-tokens.dfy(9,11): Info: Selected triggers: {Id(x)} +splitting-picks-the-right-tokens.dfy(16,11): Info: 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. splitting-picks-the-right-tokens.dfy(16,39): Related location @@ -24,15 +8,9 @@ Execution trace: (0,0): anon3_Then splitting-picks-the-right-tokens.dfy(22,13): Error BP5002: A precondition for this call might not hold. splitting-picks-the-right-tokens.dfy(9,11): Related location: This is the precondition that might not hold. -splitting-picks-the-right-tokens.dfy(9,46): Related location -Execution trace: - (0,0): anon0 - (0,0): anon3_Else -splitting-picks-the-right-tokens.dfy(22,13): Error BP5002: A precondition for this call might not hold. -splitting-picks-the-right-tokens.dfy(9,11): Related location: This is the precondition that might not hold. splitting-picks-the-right-tokens.dfy(9,37): Related location Execution trace: (0,0): anon0 (0,0): anon3_Else -Dafny program verifier finished with 6 verified, 4 errors +Dafny program verifier finished with 6 verified, 2 errors diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect index a8bb234539..cb95261661 100644 --- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect +++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect @@ -6,10 +6,7 @@ splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q 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)": - 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 "P(i) || !Q(i)": Selected triggers: {Q(i)}, {P(i)} splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression "P(i + 1)": @@ -21,12 +18,8 @@ splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression "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)} (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)} (may loop with "P(i + 1)"), {Q(i)} +splitting-triggers-recovers-expressivity.dfy(58,11): Info: Selected triggers: + {P(i)}, {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 27548ac9f7..05e39d4b61 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,16 +1,5 @@ -splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression "y > 0": - /!\ No terms found to trigger on. -splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression "y < 0": - /!\ No terms found to trigger on. -splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression "y > 0": - /!\ No terms found to trigger on. -splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression "y < 0": - /!\ No terms found to trigger on. -splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold. -splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold. -splitting-triggers-yields-better-precondition-related-errors.dfy(7,34): Related location -Execution trace: - (0,0): anon0 +splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: /!\ No terms found to trigger on. +splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: /!\ 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,25): Related location @@ -18,15 +7,9 @@ Execution trace: (0,0): anon0 splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location -splitting-triggers-yields-better-precondition-related-errors.dfy(15,34): Related location -Execution trace: - (0,0): anon0 - (0,0): anon4_Else -splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition -splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location splitting-triggers-yields-better-precondition-related-errors.dfy(15,25): Related location Execution trace: (0,0): anon0 (0,0): anon4_Else -Dafny program verifier finished with 4 verified, 4 errors +Dafny program verifier finished with 4 verified, 2 errors 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 6c3e485351..dad1b37907 100644 --- a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect +++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect @@ -1,17 +1,6 @@ -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))": - 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": - 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": - 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": - 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(26,11): Info: Selected triggers: {f(n)} + Rejected triggers: {P(f(n))} (more specific than {f(n)}) +wf-checks-use-the-original-quantifier.dfy(27,11): Info: Selected triggers: + {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s} Dafny program verifier finished with 4 verified, 0 errors