From 922e423dc5d9bc069ecdd2cea92f1b0cb14bb6f2 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jan 2024 18:12:57 +0100 Subject: [PATCH] Improve trigger related warnings (#5000) ### Description - Refactor trigger related code. Sorry for not having this be a separate PR. I can still try to split it if that helps a lot. - Add a section to the reference manual to help debug trigger related warnings - Improve diagnostics generated for triggers. - Trigger generation related warnings now point to the relevant section in the reference manual - Trigger generation related warnings now mention how to silence them - Splitting of quantifiers is reported more explicitly - UI tweaks to the diagnostics, best inspected through the diff of the expect files ### How has this been tested? - Updated expect files of existing tests By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- Source/DafnyCore/AST/Attributes.cs | 2 +- .../Expressions/Comprehensions/ForallExpr.cs | 2 +- .../Comprehensions/QuantifierExpr.cs | 2 +- .../Conditional/NestedMatchCaseExpr.cs | 3 +- .../Conditional/NestedMatchCaseStmt.cs | 3 +- .../AST/Expressions/Variables/LetExpr.cs | 3 +- .../DafnyCore/AST/Modules/ModuleDefinition.cs | 3 +- .../ControlFlow/GuardedAlternative.cs | 3 +- .../CompileNestedMatch/MatchFlattener.cs | 2 +- .../Generic/PredicateEqualityComparer.cs | 20 + Source/DafnyCore/Generic/SinglyLinkedList.cs | 24 +- .../Rewriters/TriggerGeneratingRewriter.cs | 2 +- .../Triggers/ComprehensionTriggerGenerator.cs | 234 ++++++ .../DafnyCore/Triggers/QuantifierSplitter.cs | 64 +- .../Triggers/QuantifiersCollection.cs | 375 --------- .../Triggers/QuantifiersCollector.cs | 8 +- .../Triggers/SplitPartTriggerWriter.cs | 216 ++++++ .../DafnyCore/Triggers/TriggerAnnotation.cs | 48 ++ .../Triggers/TriggerAnnotationsCache.cs | 19 + Source/DafnyCore/Triggers/TriggerCandidate.cs | 70 ++ .../DafnyCore/Triggers/TriggerExtensions.cs | 51 +- Source/DafnyCore/Triggers/TriggerMatch.cs | 25 + Source/DafnyCore/Triggers/TriggerTerm.cs | 40 + Source/DafnyCore/Triggers/TriggerTermSet.cs | 105 +++ Source/DafnyCore/Triggers/TriggerUtils.cs | 251 +----- .../DafnyCore/Triggers/TriggersCollector.cs | 720 ++++++++---------- .../LitTest/auditor/TestAuditor.dfy.expect | 6 +- .../dafny0/BitvectorResolution.dfy.expect | 12 +- .../LitTest/dafny0/Comprehensions.dfy.expect | 12 +- .../dafny0/ComprehensionsNewSyntax.dfy.expect | 12 +- .../dafny0/ConcurrentAttribute.dfy.expect | 8 +- .../LitTest/dafny0/DirtyLoops.dfy.expect | 4 +- .../dafny0/DiscoverBounds.dfy.verifier.expect | 10 +- ...llCompilationNewSyntax.dfy.verifier.expect | 8 +- .../LitTests/LitTest/dafny0/IMaps.dfy.expect | 8 +- .../LitTests/LitTest/dafny0/ISets.dfy.expect | 4 +- .../dafny0/InSetComprehension.dfy.expect | 12 +- .../LitTest/dafny0/LetExpr.dfy.expect | 8 +- .../LitTests/LitTest/dafny0/Maps.dfy.expect | 2 +- .../dafny0/QuantificationNewSyntax.dfy.expect | 4 +- .../LitTest/dafny0/ReadsOnMethods.dfy.expect | 4 +- .../LitTest/dafny0/SmallTests.dfy.expect | 4 +- .../dafny0/TriggerInPredicate.dfy.expect | 1 - .../dafny0/Wellfounded.dfy.verifier.expect | 4 +- .../Snapshots5.run.legacy.dfy.expect | 18 +- ...ssingNumber-functional.dfy.verifier.expect | 2 +- .../LitTest/dafny3/InductionVsCoinduction.dfy | 2 +- .../dafny3/InductionVsCoinduction.dfy.expect | 2 +- .../LitTest/dafny3/Streams.dfy.expect | 4 +- .../dafny4/Ackermann.dfy.verifier.expect | 4 +- .../LitTests/LitTest/dafny4/Bug63.dfy.expect | 2 +- .../LitTest/dafny4/Regression1.dfy.expect | 2 +- .../LitTest/dafny4/git-issue1.dfy.expect | 4 +- .../LitTest/dafny4/git-issue18.dfy.expect | 2 +- .../LitTest/dafny4/git-issue22.dfy.expect | 2 +- .../LitTest/dafny4/git-issue48.dfy.expect | 2 +- .../LitTest/dafny4/git-issue75.dfy.expect | 4 +- .../LitTest/dafny4/git-issue92.dfy.expect | 2 +- .../LitTest/dafny4/git-issue96.dfy.expect | 3 +- .../LitTest/dafny4/set-compr.dfy.expect | 12 +- .../git-issues/git-issue-1207.dfy.expect | 10 +- .../git-issues/git-issue-2265.dfy.expect | 2 +- .../git-issues/git-issue-2593.dfy.expect | 2 +- .../git-issues/git-issue-2747.dfy.expect | 2 +- .../git-issues/git-issue-3358.dfy.expect | 2 +- .../git-issue-4007.dfy.verifier.expect | 2 +- .../git-issue-697j.dfy.verifier.expect | 98 +-- .../git-issues/git-issue-851.dfy.expect | 42 +- .../git-issues/git-issue-897.dfy.expect | 2 +- .../git-issues/git-issue-897a.dfy.expect | 2 +- .../git-issues/github-issue-4144.dfy.expect | 36 +- .../LitTests/LitTest/hofs/SumSum.dfy.expect | 4 +- ...stBeyondVerifierExpect.dfy.verifier.expect | 2 +- ...MissingVerifierExpect.dfy.testdafny.expect | 2 +- ...stWrongVerifierExpect.dfy.testdafny.expect | 2 +- .../LitTest/patterns/nested.dfy.expect | 4 +- .../assumptions.dfy.expect | 6 +- .../server/simple-session.transcript.expect | 14 +- ...-detection-messages--unit-tests.dfy.expect | 40 +- .../triggers/regression-tests.dfy.expect | 2 +- ...ok-like-the-triggers-they-match.dfy.expect | 27 +- ...-triggers-recovers-expressivity.dfy.expect | 26 +- ...ter-precondition-related-errors.dfy.expect | 4 +- ...ssing-warnings-behaves-properly.dfy.expect | 16 +- docs/DafnyRef/Statements.13.expect | 2 +- docs/DafnyRef/Statements.14.expect | 2 +- docs/DafnyRef/Topics.md | 26 + docs/OnlineTutorial/Sets.W1.expect | 2 +- docs/OnlineTutorial/Sets.W2.expect | 2 +- docs/OnlineTutorial/Sets.W3.expect | 2 +- docs/OnlineTutorial/guide.17.expect | 2 +- 91 files changed, 1452 insertions(+), 1420 deletions(-) create mode 100644 Source/DafnyCore/Generic/PredicateEqualityComparer.cs create mode 100644 Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs delete mode 100644 Source/DafnyCore/Triggers/QuantifiersCollection.cs create mode 100644 Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs create mode 100644 Source/DafnyCore/Triggers/TriggerAnnotation.cs create mode 100644 Source/DafnyCore/Triggers/TriggerAnnotationsCache.cs create mode 100644 Source/DafnyCore/Triggers/TriggerCandidate.cs create mode 100644 Source/DafnyCore/Triggers/TriggerMatch.cs create mode 100644 Source/DafnyCore/Triggers/TriggerTerm.cs create mode 100644 Source/DafnyCore/Triggers/TriggerTermSet.cs diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index 0e1d27dd64..92c6a81e04 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -235,7 +235,7 @@ public interface IAttributeBearingDeclaration { Attributes Attributes { get; } } -public static class IAttributeBearingDeclarationExtensions { +public static class AttributeBearingDeclarationExtensions { public static bool HasUserAttribute(this IAttributeBearingDeclaration decl, string name, out Attributes attribute) { if (Attributes.Find(decl.Attributes, name) is UserSuppliedAttributes attr) { attribute = attr; diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs index 36f29c10f7..64e3fd1e84 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; public class ForallExpr : QuantifierExpr, ICloneable { public override string WhatKind => "forall expression"; - protected override BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.And; } } + protected override BinaryExpr.ResolvedOpcode SplitResolvedOp => BinaryExpr.ResolvedOpcode.And; public ForallExpr(IToken tok, RangeToken rangeToken, List bvars, Expression range, Expression term, Attributes attrs) : base(tok, rangeToken, bvars, range, term, attrs) { diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs index e2f17c62ef..c829236b45 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs @@ -11,7 +11,7 @@ public abstract class QuantifierExpr : ComprehensionExpr, TypeParameter.ParentTy private readonly int UniqueId; private static int currentQuantId = -1; - protected virtual BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.Or; } } + protected virtual BinaryExpr.ResolvedOpcode SplitResolvedOp => BinaryExpr.ResolvedOpcode.Or; private Expression SplitQuantifierToExpression() { Contract.Requires(SplitQuantifier != null && SplitQuantifier.Any()); diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs index 87f15ac5fc..603ec190c3 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseExpr.cs @@ -7,8 +7,7 @@ namespace Microsoft.Dafny; public class NestedMatchCaseExpr : NestedMatchCase, IAttributeBearingDeclaration { public Expression Body; - public Attributes Attributes; - Attributes IAttributeBearingDeclaration.Attributes => Attributes; + public Attributes Attributes { get; set; } public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Attributes attrs) : base(tok, pat) { Contract.Requires(body != null); diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs index d9f33f8771..9ca9017801 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs @@ -7,8 +7,7 @@ namespace Microsoft.Dafny; public class NestedMatchCaseStmt : NestedMatchCase, IAttributeBearingDeclaration, ICloneable { public readonly List Body; - public Attributes Attributes; - Attributes IAttributeBearingDeclaration.Attributes => Attributes; + public Attributes Attributes { get; set; } public NestedMatchCaseStmt(RangeToken rangeToken, ExtendedPattern pat, List body) : base(rangeToken.StartToken, pat) { RangeToken = rangeToken; Contract.Requires(body != null); diff --git a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs index 5fd6b36887..d8481a419d 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs @@ -9,8 +9,7 @@ public class LetExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBeari public readonly List RHSs; public readonly Expression Body; public readonly bool Exact; // Exact==true means a regular let expression; Exact==false means an assign-such-that expression - public readonly Attributes Attributes; - Attributes IAttributeBearingDeclaration.Attributes => Attributes; + public Attributes Attributes { get; set; } [FilledInDuringResolution] public List Constraint_Bounds; // null for Exact=true and for when expression is in a ghost context // invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count; private Expression translationDesugaring; // filled in during translation, lazily; to be accessed only via Translation.LetDesugaring; always null when Exact==true diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 5ee071d9f9..03a2961bd8 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -62,8 +62,7 @@ public string FullName { public readonly List PrefixIds; // The qualified module name, except the last segment when a // nested module declaration is outside its enclosing module public ModuleDefinition EnclosingModule; // readonly, except can be changed by resolver for prefix-named modules when the real parent is discovered - public readonly Attributes Attributes; - Attributes IAttributeBearingDeclaration.Attributes => Attributes; + public Attributes Attributes { get; set; } public readonly Implements Implements; // null if no refinement base public bool SuccessfullyResolved; // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved public readonly ModuleKindEnum ModuleKind; diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs b/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs index 93ecceb9f3..3a9f844448 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/GuardedAlternative.cs @@ -8,10 +8,9 @@ public class GuardedAlternative : TokenNode, IAttributeBearingDeclaration { public readonly bool IsBindingGuard; public readonly Expression Guard; public readonly List Body; - public Attributes Attributes; + public Attributes Attributes { get; set; } public override IEnumerable Children => (Attributes != null ? new List { Attributes } : Enumerable.Empty()).Concat(new List() { Guard }).Concat(Body); public override IEnumerable PreResolveChildren => Children; - Attributes IAttributeBearingDeclaration.Attributes => Attributes; [ContractInvariantMethod] void ObjectInvariant() { diff --git a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs index 650fdc62d4..0d90dc899a 100644 --- a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs +++ b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs @@ -374,7 +374,7 @@ private CaseBody CompileHeadsContainingConstructor(MatchCompilationState mti, Ma var freshMatchees = freshPatBV.ConvertAll(x => new IdentifierExpr(x.tok, x)); // Update the current context var newContext = context.FillHole(new IdCtx(ctor)); - var body = CompilePatternPaths(mti, newContext, LinkedLists.Concat(freshMatchees, remainingMatchees), constructorPaths); + var body = CompilePatternPaths(mti, newContext, LinkedLists.FromList(freshMatchees, remainingMatchees), constructorPaths); if (body is null) { // If no path matches this constructor, drop the case continue; diff --git a/Source/DafnyCore/Generic/PredicateEqualityComparer.cs b/Source/DafnyCore/Generic/PredicateEqualityComparer.cs new file mode 100644 index 0000000000..b05572acd2 --- /dev/null +++ b/Source/DafnyCore/Generic/PredicateEqualityComparer.cs @@ -0,0 +1,20 @@ +using System; +using System.Collections.Generic; + +namespace DafnyCore.Generic; + +public class PredicateEqualityComparer : IEqualityComparer { + private readonly Func comparer; + + public PredicateEqualityComparer(Func comparer) { + this.comparer = comparer; + } + + public bool Equals(T a, T b) { + return comparer(a, b); + } + + public int GetHashCode(T a) { + return a.GetHashCode(); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Generic/SinglyLinkedList.cs b/Source/DafnyCore/Generic/SinglyLinkedList.cs index 2e43c3e33e..0e77c90f74 100644 --- a/Source/DafnyCore/Generic/SinglyLinkedList.cs +++ b/Source/DafnyCore/Generic/SinglyLinkedList.cs @@ -38,20 +38,32 @@ public abstract record SinglyLinkedList : IEnumerable { IEnumerator IEnumerable.GetEnumerator() { return GetEnumerator(); } + + public bool Any() { + return this is not Nil; + } } public static class LinkedLists { - public static SinglyLinkedList Concat(IEnumerable left, SinglyLinkedList right) { - SinglyLinkedList result = right; - foreach (var value in left.Reverse()) { - result = new Cons(value, result); - } + public static SinglyLinkedList Concat(SinglyLinkedList left, SinglyLinkedList right) { + return left switch { + Nil => right, + Cons cons => new Cons(cons.Head, Concat(cons.Tail, right)), + _ => throw new ArgumentOutOfRangeException(nameof(left)) + }; + } + + public static SinglyLinkedList FromList(IReadOnlyList values, SinglyLinkedList tail = null) { + SinglyLinkedList result = tail ?? new Nil(); + for (int i = values.Count - 1; i >= 0; i--) { + result = new Cons(values[i], result); + } return result; } public static SinglyLinkedList Create(params T[] values) { - return Concat(values, new Nil()); + return FromList(values); } } diff --git a/Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs b/Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs index 42a4aad89e..e8283ee85e 100644 --- a/Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs +++ b/Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs @@ -19,7 +19,7 @@ internal override void PostCyclicityResolve(ModuleDefinition definition, ErrorRe var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext, Reporter.Options, definition); foreach (var quantifierCollection in finder.quantifierCollections) { quantifierCollection.ComputeTriggers(triggersCollector); - quantifierCollection.CommitTriggers(Reporter.Options, systemModuleManager); + quantifierCollection.CommitTriggers(systemModuleManager); } } } \ No newline at end of file diff --git a/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs b/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs new file mode 100644 index 0000000000..be69c3977c --- /dev/null +++ b/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs @@ -0,0 +1,234 @@ +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Diagnostics.Contracts; +using DafnyCore.Generic; + +namespace Microsoft.Dafny.Triggers { + + record QuantifierGroup(SplitPartTriggerWriter Quantifier, List Expressions); + + /// + /// For a comprehension that has been split into parts, determine triggers for each part. + /// + /// See section 2.3 of "Trigger Selection Strategies to Stabilize Program Verifiers" to learn + /// why we introduce these splits, and what interaction there is between the generation of their triggers. + /// + class ComprehensionTriggerGenerator { + private readonly ErrorReporter reporter; + private readonly ComprehensionExpr comprehension; // the expression where the splits are originated from + private List partWriters; + + internal ComprehensionTriggerGenerator(ComprehensionExpr comprehension, IEnumerable quantifiers, ErrorReporter reporter) { + Contract.Requires(quantifiers.All(q => !(q is QuantifierExpr) || ((QuantifierExpr)q).SplitQuantifier == null)); + this.reporter = reporter; + this.comprehension = comprehension; + partWriters = quantifiers.Select(q => new SplitPartTriggerWriter(q)).ToList(); + } + + internal void ComputeTriggers(TriggersCollector triggersCollector) { + CollectAndShareTriggers(triggersCollector); + TrimInvalidTriggers(); + BuildDependenciesGraph(); + if (DetectAndFilterLoopingCandidates() && RewriteMatchingLoop(triggersCollector.ForModule)) { + CollectWithoutShareTriggers(triggersCollector); + TrimInvalidTriggers(); + DetectAndFilterLoopingCandidates(); + } + FilterWeakerTriggers(); + CombineSplitQuantifier(); + } + + private bool SubsetGenerationPredicate(TriggerTermSet terms, TriggerTerm additionalTerm) { + return true; // FIXME Remove this + //return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any(); + } + + /// + /// Collect triggers from the body of each quantifier, and share them + /// between all quantifiers. This method assumes that all quantifiers + /// actually come from the same context, and were the result of a split that + /// gave them all the same variables. + /// + /// See section 2.1 of "Trigger Selection Strategies to Stabilize Program Verifiers" to learn + /// how we collect triggers + /// + void CollectAndShareTriggers(TriggersCollector triggersCollector) { + var pool = new List(); + foreach (var triggerWriter in partWriters) { + var candidates = triggersCollector.CollectTriggers(triggerWriter.Comprehension).Deduplicate(TriggerTerm.Eq); + var greatTerms = candidates.Where(term => !triggersCollector.TranslateToFunctionCall(term.Expr)).ToList(); + if (greatTerms.Any()) { + // If we have great terms, only use those + candidates = greatTerms; + } + pool.AddRange(candidates); + } + var distinctPool = pool.Deduplicate(TriggerTerm.Eq); + + foreach (var triggerWriter in partWriters) { + triggerWriter.CandidateTerms = distinctPool; // The list of candidate terms is immutable + triggerWriter.Candidates = TriggerTermSet.ComputeNonEmptyTriggerCandidatesTerms(LinkedLists.FromList(distinctPool), triggerWriter.Comprehension.BoundVars) + .Select(set => set.ToTriggerCandidate()).ToList(); + } + } + + void CollectWithoutShareTriggers(TriggersCollector triggersCollector) { + foreach (var triggerWriter in partWriters) { + var candidates = triggersCollector.CollectTriggers(triggerWriter.Comprehension).Deduplicate(TriggerTerm.Eq); + triggerWriter.CandidateTerms = candidates; // The list of candidate terms is immutable + triggerWriter.Candidates = TriggerTermSet.ComputeNonEmptyTriggerCandidatesTerms( + LinkedLists.FromList(candidates), triggerWriter.Comprehension.BoundVars). + Select(set => set.ToTriggerCandidate()).ToList(); + } + } + + private void TrimInvalidTriggers() { + foreach (var triggerWriter in partWriters) { + triggerWriter.TrimInvalidTriggers(); + } + } + + void BuildDependenciesGraph() { + // The problem of finding matching loops between multiple-triggers is hard; it + // seems to require one to track exponentially-sized dependencies between parts + // of triggers and quantifiers. For now, we only do single-quantifier loop + // detection + } + + bool DetectAndFilterLoopingCandidates() { + // NOTE: This only looks for self-loops; that is, loops involving a single + // quantifier. + + // For a given quantifier q, we introduce a triggering relation between trigger + // candidates by writing t1 → t2 if instantiating q from t1 introduces a ground + // term that matches t2. Then, we notice that this relation is transitive, since + // all triggers yield the same set of terms. This means that any matching loop + // t1 → ... → t1 can be reduced to a self-loop t1 → t1. Detecting such + // self-loops is then only a matter of finding terms in the body of the + // quantifier that match a given trigger. + + // Of course, each trigger that actually appears in the body of the quantifier + // yields a trivial self-loop (e.g. P(i) in [∀ i {P(i)} ⋅ P(i)]), so we + // ignore this type of loops. In fact, we ignore any term in the body of the + // quantifier that matches one of the terms of the trigger (this ensures that + // [∀ 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). + + // 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. + bool foundLoop = false; + foreach (var quantifier in partWriters) { + foundLoop |= quantifier.DetectAndFilterLoopingCandidates(reporter); + } + return foundLoop; + } + + private bool RewriteMatchingLoop(ModuleDefinition module) { + if (comprehension is QuantifierExpr unSplitQuantifier) { + bool rewritten = false; + foreach (var triggerWriter in partWriters) { + rewritten |= triggerWriter.RewriteMatchingLoop(reporter, module); + } + if (rewritten) { + unSplitQuantifier.SplitQuantifier = partWriters.Select(q => (Expression)q.Comprehension).ToList(); + return true; + } + } + return false; + } + + void FilterWeakerTriggers() { + foreach (var triggerWriter in partWriters) { + triggerWriter.FilterStrongCandidates(); + } + } + + // group split quantifier by what triggers they got, and merged them back into one quantifier. + private void CombineSplitQuantifier() { + if (partWriters.Count > 1) { + var groups = new List(); + groups.Add(new QuantifierGroup(partWriters[0], new List { partWriters[0].Comprehension })); + for (int i = 1; i < partWriters.Count; i++) { + bool found = false; + for (int j = 0; j < groups.Count; j++) { + if (HasSameTriggers(partWriters[i], groups[j].Quantifier)) { + // belong to the same group + groups[j].Expressions.Add(partWriters[i].Comprehension); + found = true; + break; + } + } + if (!found) { + // start a new group + groups.Add(new QuantifierGroup(partWriters[i], new List { partWriters[i].Comprehension })); + } + } + if (groups.Count == partWriters.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) { + SplitPartTriggerWriter q = group.Quantifier; + if (q.Comprehension is ForallExpr forallExpr) { + IToken tok = forallExpr.tok is NestedToken nestedToken ? nestedToken.Outer : forallExpr.tok; + Expression expr = QuantifiersToExpression(tok, BinaryExpr.ResolvedOpcode.And, group.Expressions); + q.Comprehension = new ForallExpr(tok, forallExpr.RangeToken, forallExpr.BoundVars, forallExpr.Range, expr, TriggerUtils.CopyAttributes(forallExpr.Attributes)) { Type = forallExpr.Type, Bounds = forallExpr.Bounds }; + } else if (q.Comprehension is ExistsExpr existsExpr) { + IToken tok = existsExpr.tok is NestedToken nestedToken ? nestedToken.Outer : existsExpr.tok; + Expression expr = QuantifiersToExpression(tok, BinaryExpr.ResolvedOpcode.Or, group.Expressions); + q.Comprehension = new ExistsExpr(tok, existsExpr.RangeToken, existsExpr.BoundVars, existsExpr.Range, expr, TriggerUtils.CopyAttributes(existsExpr.Attributes)) { Type = existsExpr.Type, Bounds = existsExpr.Bounds }; + } + list.Add(q); + splits.Add(q.Comprehension); + } + + partWriters = list; + Contract.Assert(this.comprehension is QuantifierExpr); // only QuantifierExpr has SplitQuantifier + ((QuantifierExpr)this.comprehension).SplitQuantifier = splits; + } + } + + private bool HasSameTriggers(SplitPartTriggerWriter one, SplitPartTriggerWriter other) { + return one.Candidates.SequenceEqual(other.Candidates, new PredicateEqualityComparer(SameTriggerCandidate)); + } + + private static bool SameTriggerCandidate(TriggerCandidate arg1, TriggerCandidate arg2) { + Func comparer = TriggerTerm.Eq; + return arg1.Terms.SequenceEqual(arg2.Terms, new PredicateEqualityComparer(comparer)); + } + + 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; + } + + internal void CommitTriggers(SystemModuleManager systemModuleManager) { + if (partWriters.Count > 1) { + reporter.Message(MessageSource.Rewriter, ErrorLevel.Info, null, + comprehension.Tok, $"Quantifier was split into {partWriters.Count} parts. " + + "Better verification performance and error reporting may be obtained by splitting the quantifier in source. " + + $"For more information, see the section quantifier instantiation rules in the reference manual."); + } + + for (var index = 0; index < partWriters.Count; index++) { + var triggerWriter = partWriters[index]; + triggerWriter.CommitTrigger(reporter, partWriters.Count > 1 ? index : null, systemModuleManager); + } + } + } +} diff --git a/Source/DafnyCore/Triggers/QuantifierSplitter.cs b/Source/DafnyCore/Triggers/QuantifierSplitter.cs index 8b418004c5..fe3bf03377 100644 --- a/Source/DafnyCore/Triggers/QuantifierSplitter.cs +++ b/Source/DafnyCore/Triggers/QuantifierSplitter.cs @@ -5,16 +5,20 @@ using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; -using System.Text; namespace Microsoft.Dafny.Triggers { + + /// + /// See section 2.3 of "Trigger Selection Strategies to Stabilize Program Verifiers" to learn + /// why we split quantifiers + /// 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 /// split quantifiers got re-split, creating a situation where the direct children of a split quantifier were /// also split quantifiers. - private Dictionary> splits = new Dictionary>(); + private readonly Dictionary> splits = new(); private static BinaryExpr.Opcode FlipOpcode(BinaryExpr.Opcode opCode) { if (opCode == BinaryExpr.Opcode.And) { @@ -37,12 +41,11 @@ private static UnaryOpExpr Not(Expression expr) { return new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type }; } - internal static IEnumerable SplitExpr(Expression expr, BinaryExpr.Opcode separator) { + private static IEnumerable SplitExpr(Expression expr, BinaryExpr.Opcode separator) { expr = expr.Resolved; - var unary = expr as UnaryOpExpr; var binary = expr as BinaryExpr; - if (unary != null && unary.Op == UnaryOpExpr.Opcode.Not) { + if (expr is UnaryOpExpr unary && unary.Op == UnaryOpExpr.Opcode.Not) { foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return Not(e); } } else if (binary != null && binary.Op == separator) { if (Expression.IsBoolLiteral(binary.E0, out var b) && (binary.Op == BinaryExpr.Opcode.And ? b : !b)) { @@ -67,7 +70,7 @@ internal static IEnumerable SplitAndStitch(BinaryExpr pair, BinaryEx } } - internal static IEnumerable SplitQuantifier(ComprehensionExpr quantifier) { + private static IEnumerable SplitQuantifier(ComprehensionExpr quantifier) { var body = quantifier.Term; var binary = body as BinaryExpr; @@ -145,53 +148,4 @@ internal void Commit() { } } } - - class MatchingLoopRewriter { - public MatchingLoopRewriter(DafnyOptions options, ModuleDefinition forModule) { - triggersCollector = new TriggersCollector(new Dictionary>(), options, forModule); - } - - TriggersCollector triggersCollector; - List> substMap; - - public QuantifierExpr RewriteMatchingLoops(QuantifierWithTriggers q) { - // rewrite quantifier to avoid matching loops - // before: - // assert forall i :: 0 <= i < a.Length-1 ==> a[i] <= a[i+1]; - // after: - // assert forall i,j :: j == i+1 ==> 0 <= i < a.Length-1 ==> a[i] <= a[j]; - substMap = new List>(); - foreach (var m in q.LoopingMatches) { - var e = m.OriginalExpr; - if (triggersCollector.IsPotentialTriggerCandidate(e) && triggersCollector.IsTriggerKiller(e)) { - foreach (var sub in e.SubExpressions) { - if (triggersCollector.IsTriggerKiller(sub) && (!triggersCollector.IsPotentialTriggerCandidate(sub))) { - var entry = substMap.Find(x => ExprExtensions.ExpressionEq(sub, x.Item1)); - if (entry == null) { - var newBv = new BoundVar(sub.tok, "_t#" + substMap.Count, sub.Type); - var ie = new IdentifierExpr(sub.tok, newBv.Name); - ie.Var = newBv; - ie.Type = newBv.Type; - substMap.Add(new Tuple(sub, ie)); - } - } - } - } - } - - var expr = (QuantifierExpr)q.quantifier; - if (substMap.Count > 0) { - var s = new ExprSubstituter(substMap); - expr = s.Substitute(q.quantifier) as QuantifierExpr; - } else { - // make a copy of the expr - if (expr is ForallExpr) { - expr = new ForallExpr(expr.tok, expr.RangeToken, expr.BoundVars, expr.Range, expr.Term, TriggerUtils.CopyAttributes(expr.Attributes)) { Type = expr.Type, Bounds = expr.Bounds }; - } else { - expr = new ExistsExpr(expr.tok, expr.RangeToken, expr.BoundVars, expr.Range, expr.Term, TriggerUtils.CopyAttributes(expr.Attributes)) { Type = expr.Type, Bounds = expr.Bounds }; - } - } - return expr; - } - } } diff --git a/Source/DafnyCore/Triggers/QuantifiersCollection.cs b/Source/DafnyCore/Triggers/QuantifiersCollection.cs deleted file mode 100644 index 1a10da79ed..0000000000 --- a/Source/DafnyCore/Triggers/QuantifiersCollection.cs +++ /dev/null @@ -1,375 +0,0 @@ -// Copyright by the contributors to the Dafny Project -// SPDX-License-Identifier: MIT - -#define QUANTIFIER_WARNINGS - -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Diagnostics.Contracts; -using static Microsoft.Dafny.ErrorRegistry; - -namespace Microsoft.Dafny.Triggers { - class QuantifierWithTriggers { - internal ComprehensionExpr quantifier; - internal List CandidateTerms; - internal List Candidates; - internal List RejectedCandidates; - internal List LoopingMatches; - - internal bool AllowsLoops { get { return TriggerUtils.AllowsMatchingLoops(quantifier); } } - internal bool CouldSuppressLoops { get; set; } - - internal QuantifierWithTriggers(ComprehensionExpr quantifier) { - this.quantifier = quantifier; - this.RejectedCandidates = new List(); - } - - internal void TrimInvalidTriggers() { - Contract.Requires(CandidateTerms != null); - Contract.Requires(Candidates != null); - Candidates = TriggerUtils.Filter(Candidates, tr => tr, (tr, _) => tr.MentionsAll(quantifier.BoundVars), (tr, _) => { }).ToList(); - } - } - - class QuantifiersCollection { - readonly ErrorReporter reporter; - readonly ComprehensionExpr expr; // the expression where the splits are originated from - List quantifiers; - - 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(); - } - - internal void ComputeTriggers(TriggersCollector triggersCollector) { - CollectAndShareTriggers(triggersCollector); - TrimInvalidTriggers(); - BuildDependenciesGraph(); - if (SuppressMatchingLoops() && RewriteMatchingLoop(triggersCollector)) { - CollectWithoutShareTriggers(triggersCollector); - TrimInvalidTriggers(); - SuppressMatchingLoops(); - } - SelectTriggers(); - CombineSplitQuantifier(); - } - - private bool SubsetGenerationPredicate(TriggerUtils.SetOfTerms terms, TriggerTerm additionalTerm) { - return true; // FIXME Remove this - //return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any(); - } - - /// - /// Collect triggers from the body of each quantifier, and share them - /// between all quantifiers. This method assumes that all quantifiers - /// actually come from the same context, and were the result of a split that - /// gave them all the same variables. - /// - /// - void CollectAndShareTriggers(TriggersCollector triggersCollector) { - List pool = new List(); - foreach (var q in quantifiers) { - var candidates = triggersCollector.CollectTriggers(q.quantifier).Deduplicate(TriggerTerm.Eq); - // filter out the candidates that was "second-class" - var filtered = TriggerUtils.Filter(candidates, tr => tr, - (tr, _) => !triggersCollector.TranslateToFunctionCall(tr.Expr), (tr, _) => { }).ToList(); - // if there are only "second-class" candidates, add them back. - if (filtered.Count == 0) { - filtered = candidates; - } - pool.AddRange(filtered); - } - var distinctPool = pool.Deduplicate(TriggerTerm.Eq); - - foreach (var q in quantifiers) { - q.CandidateTerms = distinctPool; // The list of candidate terms is immutable - q.Candidates = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate, q.quantifier.BoundVars) - .Select(set => set.ToTriggerCandidate()).ToList(); - } - } - - void CollectWithoutShareTriggers(TriggersCollector triggersCollector) { - foreach (var q in quantifiers) { - var candidates = triggersCollector.CollectTriggers(q.quantifier).Deduplicate(TriggerTerm.Eq); - q.CandidateTerms = candidates; // The list of candidate terms is immutable - q.Candidates = TriggerUtils.AllNonEmptySubsets(candidates, SubsetGenerationPredicate, q.quantifier.BoundVars).Select(set => set.ToTriggerCandidate()).ToList(); - } - } - - private void TrimInvalidTriggers() { - foreach (var q in quantifiers) { - q.TrimInvalidTriggers(); - } - } - - void BuildDependenciesGraph() { - // The problem of finding matching loops between multiple-triggers is hard; it - // seems to require one to track exponentially-sized dependencies between parts - // of triggers and quantifiers. For now, we only do single-quantifier loop - // detection - } - - bool SuppressMatchingLoops() { - // NOTE: This only looks for self-loops; that is, loops involving a single - // quantifier. - - // For a given quantifier q, we introduce a triggering relation between trigger - // candidates by writing t1 → t2 if instantiating q from t1 introduces a ground - // term that matches t2. Then, we notice that this relation is transitive, since - // all triggers yield the same set of terms. This means that any matching loop - // t1 → ... → t1 can be reduced to a self-loop t1 → t1. Detecting such - // self-loops is then only a matter of finding terms in the body of the - // quantifier that match a given trigger. - - // Of course, each trigger that actually appears in the body of the quantifier - // yields a trivial self-loop (e.g. P(i) in [∀ i {P(i)} ⋅ P(i)]), so we - // ignore this type of loops. In fact, we ignore any term in the body of the - // quantifier that matches one of the terms of the trigger (this ensures that - // [∀ 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). - // 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. - bool foundloop = false; - foreach (var q in quantifiers) { - var looping = new List(); - var loopingMatches = new List(); - - var safe = TriggerUtils.Filter( - q.Candidates, - candidate => candidate.LoopingSubterms(q.quantifier, reporter.Options).ToList(), - (candidate, loopingSubterms) => !loopingSubterms.Any(), - (candidate, loopingSubterms) => { - looping.Add(candidate); - loopingMatches = loopingSubterms.ToList(); - candidate.Annotation = "may loop with " + - String.Join(", ", - loopingSubterms.Select(t => "\"" + Printer.ExprToString(reporter.Options, t.OriginalExpr) + "\"")); - }).ToList(); - - q.CouldSuppressLoops = safe.Count > 0; - q.LoopingMatches = loopingMatches; - if (!q.AllowsLoops && q.CouldSuppressLoops) { - q.Candidates = safe; - q.RejectedCandidates.AddRange(looping); - } - - if (looping.Count > 0) { - foundloop = true; - } - } - return foundloop; - } - - bool RewriteMatchingLoop(TriggersCollector triggersCollector) { - if (expr is QuantifierExpr) { - QuantifierExpr quantifier = (QuantifierExpr)expr; - var l = new List(); - List splits = new List(); - bool rewritten = false; - foreach (var q in quantifiers) { - if (TriggerUtils.NeedsAutoTriggers(q.quantifier) && TriggerUtils.WantsMatchingLoopRewrite(q.quantifier)) { - var matchingLoopRewriter = new MatchingLoopRewriter(reporter.Options, triggersCollector.ForModule); - var qq = matchingLoopRewriter.RewriteMatchingLoops(q); - splits.Add(qq); - l.Add(new QuantifierWithTriggers(qq)); - rewritten = true; - } else { - // don't rewrite the quantifier if we are not auto generate triggers. - // This is because rewriting introduces new boundvars and will cause - // user provided triggers not mention all boundvars - splits.Add(q.quantifier); - l.Add(q); - } - } - if (rewritten) { - quantifier.SplitQuantifier = splits; - quantifiers = l; - return true; - } - } - return false; - } - - void SelectTriggers() { - foreach (var q in quantifiers) { //FIXME Check whether this makes verification faster - q.Candidates = TriggerUtils.Filter(q.Candidates, - candidate => q.Candidates.Where(candidate.IsStrongerThan).ToList(), - (candidate, weakerCandidates) => !weakerCandidates.Any(), - (candidate, weakerCandidates) => { - q.RejectedCandidates.Add(candidate); - candidate.Annotation = "more specific than " + String.Join(", ", weakerCandidates); - }).ToList(); - } - } - - 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; - IToken tok = quantifier.tok is NestedToken nestedToken ? nestedToken.Outer : quantifier.tok; - Expression expr = QuantifiersToExpression(tok, BinaryExpr.ResolvedOpcode.And, group.expressions); - q.quantifier = new ForallExpr(tok, quantifier.RangeToken, quantifier.BoundVars, quantifier.Range, expr, TriggerUtils.CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type, Bounds = quantifier.Bounds }; - } else if (q.quantifier is ExistsExpr) { - ExistsExpr quantifier = (ExistsExpr)q.quantifier; - IToken tok = quantifier.tok is NestedToken nestedToken ? nestedToken.Outer : quantifier.tok; - Expression expr = QuantifiersToExpression(tok, BinaryExpr.ResolvedOpcode.Or, group.expressions); - q.quantifier = new ExistsExpr(tok, quantifier.RangeToken, quantifier.BoundVars, quantifier.Range, expr, TriggerUtils.CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type, Bounds = quantifier.Bounds }; - } - 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(DafnyOptions options, QuantifierWithTriggers q, bool addHeader, SystemModuleManager systemModuleManager) { - var errorLevel = ErrorLevel.Info; - var msg = new StringBuilder(); - var indent = addHeader ? " " : ""; - bool suppressWarnings = Attributes.Contains(q.quantifier.Attributes, "nowarn"); - var reportingToken = q.quantifier.tok; - // If there is only one subexpression, we discard the nested token information. - if (reportingToken is NestedToken nestedToken && !addHeader) { - reportingToken = nestedToken.Outer; - } - - void FirstLetterCapitalOnNestedToken() { - if (reportingToken is NestedToken nestToken && nestToken.Message != null && nestToken.Message.Length > 1) { - reportingToken = new NestedToken(nestToken.Outer, nestToken.Inner, - char.ToUpper(nestToken.Message[0]) + nestToken.Message.Substring(1)); - } - } - - 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(options, q.quantifier.Term), extraMsg).AppendLine(); - } else { - if (addHeader) { - msg.AppendFormat("For expression \"{0}\":", Printer.ExprToString(options, q.quantifier.Term)).AppendLine(); - } - - foreach (var candidate in q.Candidates) { - q.quantifier.Attributes = new Attributes("trigger", - candidate.Terms.ConvertAll(t => Expression.WrapAsParsedStructureIfNecessary(t.Expr, systemModuleManager)), - q.quantifier.Attributes); - } - - AddTriggersToMessage("Selected triggers:", q.Candidates, msg, indent); - AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true); - -#if QUANTIFIER_WARNINGS - var WARN_TAG = options.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 = WARN_LEVEL; - msg.Append(WARN).AppendLine("No terms found to trigger on."); - FirstLetterCapitalOnNestedToken(); - } else if (!q.Candidates.Any()) { - errorLevel = WARN_LEVEL; - msg.Append(WARN).AppendLine("No trigger covering all quantified variables found."); - FirstLetterCapitalOnNestedToken(); - } else if (!q.CouldSuppressLoops && !q.AllowsLoops) { - errorLevel = WARN_LEVEL; - msg.Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers."); - FirstLetterCapitalOnNestedToken(); - } else if (suppressWarnings) { - errorLevel = ErrorLevel.Warning; - msg.Append(indent).Append(WARN_TAG).AppendLine("There is no warning here to suppress."); - FirstLetterCapitalOnNestedToken(); - } -#endif - } - - if (msg.Length > 0 && !Attributes.Contains(q.quantifier.Attributes, "auto_generated")) { - var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray()); - reporter.Message(MessageSource.Rewriter, errorLevel, null, reportingToken, msgStr); - } - } - - private static void AddTriggersToMessage(string header, List triggers, StringBuilder msg, string indent, bool newlines = false) { - if (triggers.Any()) { - msg.Append(indent).Append(header); - if (triggers.Count == 1) { - msg.Append(" "); - } else if (triggers.Count > 1) { - msg.AppendLine().Append(indent).Append(" "); - } - var separator = newlines && triggers.Count > 1 ? Environment.NewLine + indent + " " : ", "; - msg.AppendLine(String.Join(separator, triggers)); - } - } - - internal void CommitTriggers(DafnyOptions options, SystemModuleManager systemModuleManager) { - foreach (var q in quantifiers) { - CommitOne(options, q, quantifiers.Count > 1, systemModuleManager); - } - } - } -} diff --git a/Source/DafnyCore/Triggers/QuantifiersCollector.cs b/Source/DafnyCore/Triggers/QuantifiersCollector.cs index 13038fa9c6..1f169e161b 100644 --- a/Source/DafnyCore/Triggers/QuantifiersCollector.cs +++ b/Source/DafnyCore/Triggers/QuantifiersCollector.cs @@ -13,7 +13,7 @@ internal class QuantifierCollector : TopDownVisitor { readonly ErrorReporter reporter; private readonly HashSet quantifiers = new HashSet(); internal readonly Dictionary> exprsInOldContext = new Dictionary>(); - internal readonly List quantifierCollections = new List(); + internal readonly List quantifierCollections = new List(); public QuantifierCollector(ErrorReporter reporter) { Contract.Requires(reporter != null); @@ -25,15 +25,15 @@ protected override bool VisitOneExpr(Expression expr, ref OldExpr/*?*/ enclosing if (expr is ComprehensionExpr e && e.BoundVars.Count > 0 && !quantifiers.Contains(e)) { if (e is SetComprehension or MapComprehension) { quantifiers.Add(e); - quantifierCollections.Add(new QuantifiersCollection(e, Enumerable.Repeat(e, 1), reporter)); + quantifierCollections.Add(new ComprehensionTriggerGenerator(e, Enumerable.Repeat(e, 1), reporter)); } else if (e is QuantifierExpr quantifier) { quantifiers.Add(quantifier); if (quantifier.SplitQuantifier != null) { var collection = quantifier.SplitQuantifier.Select(q => q as ComprehensionExpr).Where(q => q != null); - quantifierCollections.Add(new QuantifiersCollection(e, collection, reporter)); + quantifierCollections.Add(new ComprehensionTriggerGenerator(e, collection, reporter)); quantifiers.UnionWith(quantifier.SplitQuantifier); } else { - quantifierCollections.Add(new QuantifiersCollection(e, Enumerable.Repeat(quantifier, 1), reporter)); + quantifierCollections.Add(new ComprehensionTriggerGenerator(e, Enumerable.Repeat(quantifier, 1), reporter)); } } } diff --git a/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs b/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs new file mode 100644 index 0000000000..05ad11d54c --- /dev/null +++ b/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs @@ -0,0 +1,216 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Dafny.Triggers; + +/// +/// Determines the triggers for a comprehension that resulted from splitting another one +/// +class SplitPartTriggerWriter { + public ComprehensionExpr Comprehension { get; set; } + public List CandidateTerms { get; set; } + public List Candidates { get; set; } + private List RejectedCandidates { get; } + private List loopingMatches; + + private bool AllowsLoops { + get { + Contract.Requires(!(Comprehension is QuantifierExpr) || ((QuantifierExpr)Comprehension).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(Comprehension.Attributes, "matchingloop"); + } + } + + private bool CouldSuppressLoops { get; set; } + + internal SplitPartTriggerWriter(ComprehensionExpr comprehension) { + this.Comprehension = comprehension; + this.RejectedCandidates = new List(); + } + + internal void TrimInvalidTriggers() { + Contract.Requires(CandidateTerms != null); + Contract.Requires(Candidates != null); + Candidates = Candidates.Where(tr => tr.MentionsAll(Comprehension.BoundVars)).ToList(); + } + + public bool DetectAndFilterLoopingCandidates(ErrorReporter reporter) { + var looping = new List(); + var loopingMatches = new List(); + + var nonLoopingCandidates = new List(); + foreach (var candidate in Candidates) { + var loopingSubterms = candidate.LoopingSubterms(Comprehension, reporter.Options).ToList(); + if (loopingSubterms.Any()) { + looping.Add(candidate); + loopingMatches = loopingSubterms.ToList(); + candidate.Annotation = "may loop with " + string.Join(", ", + loopingSubterms.Select(t => "\"" + Printer.ExprToString(reporter.Options, t.OriginalExpr) + "\"")); + } else { + nonLoopingCandidates.Add(candidate); + } + } + + CouldSuppressLoops = nonLoopingCandidates.Count > 0; + this.loopingMatches = loopingMatches; + if (!AllowsLoops && CouldSuppressLoops) { + Candidates = nonLoopingCandidates; + RejectedCandidates.AddRange(looping); + } + + return looping.Count > 0; + } + + public bool RewriteMatchingLoop(ErrorReporter reporter, ModuleDefinition module) { + if (!NeedsAutoTriggers() || !WantsMatchingLoopRewrite()) { + return false; + } + + var triggersCollector = new TriggersCollector(new(), + reporter.Options, module); + // rewrite quantifier to avoid matching loops + // before: + // assert forall i :: 0 <= i < a.Length-1 ==> a[i] <= a[i+1]; + // after: + // assert forall i,j :: j == i+1 ==> 0 <= i < a.Length-1 ==> a[i] <= a[j]; + var substMap = new List>(); + foreach (var triggerMatch in loopingMatches) { + var e = triggerMatch.OriginalExpr; + if (triggersCollector.IsPotentialTriggerCandidate(e) && triggersCollector.IsTriggerKiller(e)) { + foreach (var sub in e.SubExpressions) { + if (triggersCollector.IsTriggerKiller(sub) && (!triggersCollector.IsPotentialTriggerCandidate(sub))) { + var entry = substMap.Find(x => ExprExtensions.ExpressionEq(sub, x.Item1)); + if (entry == null) { + var newBv = new BoundVar(sub.tok, "_t#" + substMap.Count, sub.Type); + var ie = new IdentifierExpr(sub.tok, newBv.Name); + ie.Var = newBv; + ie.Type = newBv.Type; + substMap.Add(new Tuple(sub, ie)); + } + } + } + } + } + + var expr = (QuantifierExpr)Comprehension; + if (substMap.Count > 0) { + var s = new ExprSubstituter(substMap); + expr = s.Substitute(Comprehension) as QuantifierExpr; + } else { + // make a copy of the expr + if (expr is ForallExpr) { + expr = new ForallExpr(expr.tok, expr.RangeToken, expr.BoundVars, expr.Range, expr.Term, + TriggerUtils.CopyAttributes(expr.Attributes)) { Type = expr.Type, Bounds = expr.Bounds }; + } else { + expr = new ExistsExpr(expr.tok, expr.RangeToken, expr.BoundVars, expr.Range, expr.Term, + TriggerUtils.CopyAttributes(expr.Attributes)) { Type = expr.Type, Bounds = expr.Bounds }; + } + } + var qq = expr; + + Comprehension = qq; + Candidates.Clear(); + CandidateTerms.Clear(); + loopingMatches.Clear(); + RejectedCandidates.Clear(); + return true; + + // don't rewrite the quantifier if we are not auto generate triggers. + // This is because rewriting introduces new boundvars and will cause + // user provided triggers not mention all boundvars + } + + // TODO Check whether this makes verification faster + public void FilterStrongCandidates() { + var newCandidates = new List(); + foreach (var candidate in Candidates) { + var weakerCandidates = Candidates.Where(candidate.IsStrongerThan).ToList(); + if (weakerCandidates.Any()) { + RejectedCandidates.Add(candidate); + candidate.Annotation = "more specific than " + string.Join(", ", weakerCandidates); + } else { + newCandidates.Add(candidate); + } + } + Candidates = newCandidates; + } + + public void CommitTrigger(ErrorReporter errorReporter, int? splitPartIndex, SystemModuleManager systemModuleManager) { + bool suppressWarnings = Attributes.Contains(Comprehension.Attributes, "nowarn"); + var reportingToken = Comprehension.Tok; + var warningLevel = suppressWarnings ? ErrorLevel.Info : ErrorLevel.Warning; + + if (!WantsAutoTriggers()) { + // NOTE: split and autotriggers attributes are passed down to Boogie + errorReporter.Message(MessageSource.Rewriter, ErrorLevel.Info, null, reportingToken, + "The attribute {:autotriggers false} may cause brittle verification. " + + "It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. " + + "For more information, see the section quantifier instantiation rules in the reference manual."); + } + + if (!NeedsAutoTriggers()) { + return; + } + + AddTriggerAttribute(systemModuleManager); + + if (Attributes.Contains(Comprehension.Attributes, "auto_generated")) { + return; + } + + string InfoFirstLineEnd(int count) { + return count < 2 ? " " : "\n "; + } + + var messages = new List(); + if (splitPartIndex != null) { + messages.Add($"Part #{splitPartIndex} is '{Comprehension.Term}'"); + } + if (Candidates.Any()) { + messages.Add($"Selected triggers:{InfoFirstLineEnd(Candidates.Count)}{string.Join(", ", Candidates)}"); + } + if (RejectedCandidates.Any()) { + messages.Add($"Rejected triggers:{InfoFirstLineEnd(RejectedCandidates.Count)}{string.Join("\n ", RejectedCandidates)}"); + } + + if (messages.Any()) { + errorReporter.Message(MessageSource.Rewriter, ErrorLevel.Info, null, reportingToken, string.Join("\n", messages)); + } + + if (!CandidateTerms.Any() || !Candidates.Any()) { + errorReporter.Message(MessageSource.Rewriter, warningLevel, null, reportingToken, + $"Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. " + + $"To silence this warning, add an explicit trigger using the {{:trigger}} attribute. " + + $"For more information, see the section quantifier instantiation rules in the reference manual."); + } else if (!CouldSuppressLoops && !AllowsLoops) { + errorReporter.Message(MessageSource.Rewriter, warningLevel, null, reportingToken, + $"Triggers were added to this quantifier that may introduce matching loops, which may cause brittle verification. " + + $"To silence this warning, add an explicit trigger using the {{:trigger}} attribute. " + + $"For more information, see the section quantifier instantiation rules in the reference manual."); + } + } + + private void AddTriggerAttribute(SystemModuleManager systemModuleManager) { + foreach (var candidate in Candidates) { + Comprehension.Attributes = new Attributes("trigger", + candidate.Terms.ConvertAll(t => Expression.WrapAsParsedStructureIfNecessary(t.Expr, systemModuleManager)), + Comprehension.Attributes); + } + } + + private bool WantsAutoTriggers() { + bool wantsAutoTriggers = true; + return !Attributes.ContainsBool(Comprehension.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers; + } + + private bool NeedsAutoTriggers() { + return !Attributes.Contains(Comprehension.Attributes, "trigger") && WantsAutoTriggers(); + } + + bool WantsMatchingLoopRewrite() { + bool wantsMatchingLoopRewrite = true; + return (!Attributes.ContainsBool(Comprehension.Attributes, "matchinglooprewrite", ref wantsMatchingLoopRewrite) || wantsMatchingLoopRewrite) && WantsAutoTriggers(); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Triggers/TriggerAnnotation.cs b/Source/DafnyCore/Triggers/TriggerAnnotation.cs new file mode 100644 index 0000000000..81e6d73ff1 --- /dev/null +++ b/Source/DafnyCore/Triggers/TriggerAnnotation.cs @@ -0,0 +1,48 @@ +using System.Collections.Generic; +using System.Linq; +using System.Text; + +namespace Microsoft.Dafny.Triggers; + +internal class TriggerAnnotation { + public readonly bool IsTriggerKiller; + internal readonly ISet Variables; + internal readonly List PrivateTerms; + internal readonly List ExportedTerms; + + internal TriggerAnnotation(bool isTriggerKiller, + IEnumerable variables, + IEnumerable allTerms, + IEnumerable privateTerms = null) { + this.IsTriggerKiller = isTriggerKiller; + this.Variables = new HashSet(variables); + this.PrivateTerms = new List(privateTerms ?? Enumerable.Empty()); + this.ExportedTerms = new List(allTerms == null ? Enumerable.Empty() : allTerms.Except(this.PrivateTerms)); + } + + public override string ToString() { + StringBuilder sb = new StringBuilder(); + string indent = " {0}", nindent = "\n - {0}", subindent = "\n * {0}"; + + sb.AppendFormat(indent, IsTriggerKiller); + + sb.AppendFormat(nindent, "Variables:"); + foreach (var bv in Variables) { + sb.AppendFormat(subindent, bv.Name); + } + + sb.AppendFormat(nindent, "Exported terms:"); + foreach (var term in ExportedTerms) { + sb.AppendFormat(subindent, term); + } + + if (PrivateTerms.Any()) { + sb.AppendFormat(nindent, "Private terms:"); + foreach (var term in PrivateTerms) { + sb.AppendFormat(subindent, term); + } + } + + return sb.ToString(); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Triggers/TriggerAnnotationsCache.cs b/Source/DafnyCore/Triggers/TriggerAnnotationsCache.cs new file mode 100644 index 0000000000..2632735d5b --- /dev/null +++ b/Source/DafnyCore/Triggers/TriggerAnnotationsCache.cs @@ -0,0 +1,19 @@ +using System.Collections.Generic; + +namespace Microsoft.Dafny.Triggers; + +internal class TriggerAnnotationsCache { + public readonly Dictionary> ExpressionsInOldContext; + public readonly Dictionary Annotations; + + /// + /// For certain operations, the TriggersCollector class needs to know whether + /// a particular expression is under an old(...) wrapper. This is in particular + /// true for generating trigger terms (but it is not for checking whether something + /// is a trigger killer, so passing an empty set here for that case would be fine. + /// + public TriggerAnnotationsCache(Dictionary> expressionsInOldContext) { + this.ExpressionsInOldContext = expressionsInOldContext; + Annotations = new Dictionary(); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Triggers/TriggerCandidate.cs b/Source/DafnyCore/Triggers/TriggerCandidate.cs new file mode 100644 index 0000000000..9a7a7aebf4 --- /dev/null +++ b/Source/DafnyCore/Triggers/TriggerCandidate.cs @@ -0,0 +1,70 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Dafny.Triggers; + +/// +/// A trigger consist of a number of terms +/// +class TriggerCandidate { + internal List Terms { get; set; } + internal string Annotation { get; set; } + + internal TriggerCandidate(List terms) { + this.Terms = terms; + } + + public TriggerCandidate(TriggerCandidate candidate) { + this.Terms = candidate.Terms; + } + + internal bool MentionsAll(List vars) { + return vars.All(x => Terms.Any(term => term.Variables.Contains(x))); + } + + private string Repr => String.Join(", ", Terms); + + public override string ToString() { + return "{" + Repr + "}" + (String.IsNullOrWhiteSpace(Annotation) ? "" : " (" + Annotation + ")"); + } + + /// + /// See section 2.2 of "Trigger Selection Strategies to Stabilize Program Verifiers" to learn + /// how we find potentially looping subterms. + /// + /// Roughly, this heuristic flags a trigger as potentially looping if + /// instantiating the quantifier may lead to a ground term that again matches the trigger + /// + internal IEnumerable LoopingSubterms(ComprehensionExpr quantifier, DafnyOptions options) { + Contract.Requires(!(quantifier is QuantifierExpr) || ((QuantifierExpr)quantifier).SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier + var matchingSubterms = MatchingSubterms(quantifier); + var boundVars = new HashSet(quantifier.BoundVars); + return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms, boundVars, options)); + } + + private List MatchingSubterms(ComprehensionExpr quantifier) { + Contract.Requires(!(quantifier is QuantifierExpr) || ((QuantifierExpr)quantifier).SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier + return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq); + } + + internal bool IsStrongerThan(TriggerCandidate that) { + if (this == that) { + return false; + } + + var hasStrictlyStrongerTerm = false; + foreach (var t in Terms) { + var comparison = that.Terms.Select(t.CompareTo).Max(); + + // All terms of `this` must be at least as strong as a term of `that` + if (comparison == TriggerTerm.TermComparison.NotStronger) { return false; } + + // Did we find a strictly stronger term? + hasStrictlyStrongerTerm = hasStrictlyStrongerTerm || comparison == TriggerTerm.TermComparison.Stronger; + } + + return hasStrictlyStrongerTerm; + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Triggers/TriggerExtensions.cs b/Source/DafnyCore/Triggers/TriggerExtensions.cs index 50bc2cf66c..7166b8d954 100644 --- a/Source/DafnyCore/Triggers/TriggerExtensions.cs +++ b/Source/DafnyCore/Triggers/TriggerExtensions.cs @@ -9,6 +9,7 @@ using System.Diagnostics.Contracts; using System.Linq; using System.Text; +using DafnyCore.Generic; namespace Microsoft.Dafny.Triggers { internal static class DeduplicateExtension { @@ -25,29 +26,8 @@ public static List Deduplicate(this IEnumerable seq, Func e } } - internal struct TriggerMatch { - internal Expression Expr; - internal Expression OriginalExpr; - internal Dictionary Bindings; - - internal static bool Eq(TriggerMatch t1, TriggerMatch t2) { - return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr); - } - - /// - /// 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, DafnyOptions options) { - var expr = Expr; - return !terms.Any(term => term.Expr.ExpressionEqModuloExpressionsNotInvolvingBoundVariables(expr, boundVars, options)); - } - } - internal static class ExprExtensions { - internal static bool IsInlineable(this LetExpr expr) { + private static bool IsInlineable(this LetExpr expr) { return expr.LHSs.All(p => p.Var != null) && expr.Exact; } @@ -103,7 +83,8 @@ internal static bool ExpressionEq(this Expression expr1, Expression expr2) { expr1 = expr1.Resolved; expr2 = expr2.Resolved; - return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEq(e1, e2)); + return ShallowEq_Top(expr1, expr2) && + expr1.SubExpressions.SequenceEqual(expr2.SubExpressions, new PredicateEqualityComparer(ExpressionEq)); } internal static bool ExpressionEqModuloExpressionsNotInvolvingBoundVariables(this Expression expr1, Expression expr2, ISet boundVars, DafnyOptions options) { @@ -120,8 +101,8 @@ internal static bool ExpressionEqModuloExpressionsNotInvolvingBoundVariables(thi } } - return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, - expr2.SubExpressions, (e1, e2) => ExpressionEqModuloExpressionsNotInvolvingBoundVariables(e1, e2, boundVars, options)); + Func comparer = (e1, e2) => ExpressionEqModuloExpressionsNotInvolvingBoundVariables(e1, e2, boundVars, options); + return ShallowEq_Top(expr1, expr2) && expr1.SubExpressions.SequenceEqual(expr2.SubExpressions, new PredicateEqualityComparer(comparer)); } internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet holes, Dictionary bindings) { @@ -142,7 +123,8 @@ internal static bool MatchesTrigger(this Expression expr, Expression trigger, IS } } - return ShallowEq_Top(expr, trigger) && TriggerUtils.SameLists(expr.SubExpressions, trigger.SubExpressions, (e1, e2) => MatchesTrigger(e1, e2, holes, bindings)); + Func comparer = (e1, e2) => MatchesTrigger(e1, e2, holes, bindings); + return ShallowEq_Top(expr, trigger) && expr.SubExpressions.SequenceEqual(trigger.SubExpressions, new PredicateEqualityComparer(comparer)); } private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, IEnumerable holes, Expression originalExpr) { @@ -156,12 +138,13 @@ internal static bool MatchesTrigger(this Expression expr, Expression trigger, IS internal static IEnumerable SubexpressionsMatchingTrigger(this ComprehensionExpr quantifier, Expression trigger) { return quantifier.AllSubExpressions(true, true, true) - .Select(e => TriggerUtils.PrepareExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars, e)) + .Select(e => TriggersCollector.PrepareExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars, e)) .Where(e => e.HasValue).Select(e => e.Value); } private static bool ShallowSameAttributes(Attributes attributes1, Attributes attributes2) { - return TriggerUtils.SameLists(attributes1.AsEnumerable(), attributes2.AsEnumerable(), ShallowSameSingleAttribute); + Func comparer = ShallowSameSingleAttribute; + return attributes1.AsEnumerable().SequenceEqual(attributes2.AsEnumerable(), new PredicateEqualityComparer(comparer)); } private static bool ShallowSameSingleAttribute(Attributes arg1, Attributes arg2) { @@ -334,7 +317,8 @@ private static bool ShallowEq(QuantifierExpr expr1, QuantifierExpr expr2) { } private static bool ShallowEq(ComprehensionExpr expr1, ComprehensionExpr expr2) { - if (!TriggerUtils.SameLists(expr1.BoundVars, expr2.BoundVars, SameBoundVar) || + Func comparer = SameBoundVar; + if (!expr1.BoundVars.SequenceEqual(expr2.BoundVars, new PredicateEqualityComparer(comparer)) || !ShallowSameAttributes(expr1.Attributes, expr2.Attributes) || // Filled in during resolution: !SameLists(expr1.Bounds, expr2.Bounds, ReferenceCompare) || // !SameLists(expr1.MissingBounds, expr2.MissingBounds, SameBoundVar) || @@ -430,10 +414,12 @@ private static bool ShallowEq(SeqSelectExpr expr1, SeqSelectExpr expr2) { } private static bool ShallowEq(MemberSelectExpr expr1, MemberSelectExpr expr2) { + Func comparer = TypeEq; + Func comparer1 = TypeEq; return expr1.MemberName == expr2.MemberName && expr1.Member == expr2.Member && - TriggerUtils.SameLists(expr1.TypeApplication_AtEnclosingClass, expr2.TypeApplication_AtEnclosingClass, TypeEq) && - TriggerUtils.SameLists(expr1.TypeApplication_JustMember, expr2.TypeApplication_JustMember, TypeEq); + expr1.TypeApplication_AtEnclosingClass.SequenceEqual(expr2.TypeApplication_AtEnclosingClass, new PredicateEqualityComparer(comparer)) && + expr1.TypeApplication_JustMember.SequenceEqual(expr2.TypeApplication_JustMember, new PredicateEqualityComparer(comparer1)); } internal static bool TypeEq(Type type1, Type type2) { @@ -498,11 +484,12 @@ private static bool ShallowEq(ThisExpr expr1, ThisExpr expr2) { } private static bool ShallowEq(DatatypeValue expr1, DatatypeValue expr2) { + Func comparer = TypeEq; return // Implied by Ctor equality: expr1.DatatypeName == expr2.DatatypeName && // Implied by Ctor equality: expr1.MemberName == expr2.MemberName && expr1.Ctor == expr2.Ctor && // Contextual information: expr1.IsCoCall == expr2.IsCoCall && - TriggerUtils.SameLists(expr1.InferredTypeArgs, expr2.InferredTypeArgs, TypeEq); + expr1.InferredTypeArgs.SequenceEqual(expr2.InferredTypeArgs, new PredicateEqualityComparer(comparer)); } private static bool ShallowEq(StringLiteralExpr expr1, StringLiteralExpr expr2) { diff --git a/Source/DafnyCore/Triggers/TriggerMatch.cs b/Source/DafnyCore/Triggers/TriggerMatch.cs new file mode 100644 index 0000000000..005b5b6072 --- /dev/null +++ b/Source/DafnyCore/Triggers/TriggerMatch.cs @@ -0,0 +1,25 @@ +using System.Collections.Generic; +using System.Linq; + +namespace Microsoft.Dafny.Triggers; + +internal struct TriggerMatch { + internal Expression Expr; + internal Expression OriginalExpr; + internal Dictionary Bindings; + + internal static bool Eq(TriggerMatch t1, TriggerMatch t2) { + return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr); + } + + /// + /// 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, DafnyOptions options) { + var expr = Expr; + return !terms.Any(term => term.Expr.ExpressionEqModuloExpressionsNotInvolvingBoundVariables(expr, boundVars, options)); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Triggers/TriggerTerm.cs b/Source/DafnyCore/Triggers/TriggerTerm.cs new file mode 100644 index 0000000000..3324af277b --- /dev/null +++ b/Source/DafnyCore/Triggers/TriggerTerm.cs @@ -0,0 +1,40 @@ +using System.Collections.Generic; +using System.Linq; + +namespace Microsoft.Dafny.Triggers; + +/// +/// A trigger may consist of several terms. A term must match with a ground term for the trigger to be active. +/// +internal class TriggerTerm { + internal Expression Expr { get; init; } + internal Expression OriginalExpr { get; set; } + internal ISet Variables { get; init; } + internal IEnumerable BoundVars => Variables.Select(v => v as BoundVar).Where(v => v != null); + + public override string ToString() { + return Printer.ExprToString(DafnyOptions.DefaultImmutableOptions, Expr); + // NOTE: Using OriginalExpr here could cause some confusion: + // for example, {a !in b} is a binary expression, yielding + // trigger {a in b}. Saying the trigger is a !in b would be + // rather misleading. + } + + internal enum TermComparison { + SameStrength = 0, Stronger = 1, NotStronger = -1 + } + + internal TermComparison CompareTo(TriggerTerm other) { + if (this == other) { + return TermComparison.SameStrength; + } else if (Expr.AllSubExpressions(true, true).Any(other.Expr.ExpressionEq)) { + return TermComparison.Stronger; + } else { + return TermComparison.NotStronger; + } + } + + internal static bool Eq(TriggerTerm t1, TriggerTerm t2) { + return t1.Expr.ExpressionEq(t2.Expr); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Triggers/TriggerTermSet.cs b/Source/DafnyCore/Triggers/TriggerTermSet.cs new file mode 100644 index 0000000000..8553eabf3e --- /dev/null +++ b/Source/DafnyCore/Triggers/TriggerTermSet.cs @@ -0,0 +1,105 @@ +using System; +using System.Collections.Generic; +using System.Linq; + +namespace Microsoft.Dafny.Triggers; + +/// +/// To generate triggers, we collect sets of terms. Each set may become a trigger candidate. +/// +internal class TriggerTermSet { + public bool IsRedundant { get; private set; } + private List Terms { get; set; } + + private ISet variables; + private Dictionary termOwningAUniqueVar; + private Dictionary> uniqueVarsOwnedByATerm; + + private int Count => Terms.Count; + + private TriggerTermSet() { } + + internal TriggerCandidate ToTriggerCandidate() { + return new TriggerCandidate(Terms); + } + + private static IEnumerable ComputeTriggerCandidatesTerms(SinglyLinkedList source, + ISet relevantVariables) { + return source switch { + Cons triggerTerms => ComputeTriggerCandidatesTerms(triggerTerms.Tail, relevantVariables).SelectMany( + child => { + var newSet = child.CopyWithAdd(triggerTerms.Head, relevantVariables); + return !newSet.IsRedundant ? new[] { newSet, child } : new[] { child }; + }), + Nil => new[] { Empty() }, + _ => throw new ArgumentOutOfRangeException(nameof(source)) + }; + } + + internal static IEnumerable ComputeNonEmptyTriggerCandidatesTerms(SinglyLinkedList source, IEnumerable relevantVariables) { + return ComputeTriggerCandidatesTerms(source, new HashSet(relevantVariables)).Where(subset => subset.Count > 0); + } + + private static TriggerTermSet Empty() { + var newSet = new TriggerTermSet { + IsRedundant = false, + Terms = new List(), + variables = new HashSet(), + termOwningAUniqueVar = new Dictionary(), + uniqueVarsOwnedByATerm = new Dictionary>() + }; + return newSet; + } + + /// + /// Simple formulas like [P0(i) && P1(i) && P2(i) && P3(i) && P4(i)] yield very + /// large numbers of multi-triggers, most of which are useless. As it copies its + /// argument, this method updates various datastructures that allow it to + /// efficiently track ownership relations between formulae and bound variables, + /// and sets the IsRedundant flag of the returned set, allowing the caller to + /// discard that set of terms, and the ones that would have been built on top of + /// it, thus ensuring that the only sets of terms produced in the end are sets + /// of terms in which each element contributes (owns) at least one variable. + /// + /// Note that this is trickier than just checking every term for new variables; + /// indeed, a new term that does bring new variables in can make an existing + /// term redundant (see redundancy-detection-does-its-job-properly.dfy). + /// + private TriggerTermSet CopyWithAdd(TriggerTerm term, IEnumerable relevantVariables) { + var copy = new TriggerTermSet(); + copy.Terms = new List(Terms); + copy.variables = new HashSet(variables); + copy.termOwningAUniqueVar = new Dictionary(termOwningAUniqueVar); + copy.uniqueVarsOwnedByATerm = new Dictionary>(uniqueVarsOwnedByATerm); + + copy.Terms.Add(term); + + var varsInNewTerm = new HashSet(term.BoundVars); + varsInNewTerm.IntersectWith(relevantVariables); + + var ownedByNewTerm = new HashSet(); + + // Check #0: does this term bring anything new? + copy.IsRedundant = IsRedundant || varsInNewTerm.All(bv => copy.variables.Contains(bv)); + copy.variables.UnionWith(varsInNewTerm); + + // Check #1: does this term claiming ownership of all its variables cause another term to become useless? + foreach (var v in varsInNewTerm) { + if (copy.termOwningAUniqueVar.TryGetValue(v, out var originalOwner)) { + var alsoOwnedByOriginalOwner = copy.uniqueVarsOwnedByATerm[originalOwner]; + alsoOwnedByOriginalOwner.Remove(v); + if (!alsoOwnedByOriginalOwner.Any()) { + copy.IsRedundant = true; + } + } else { + ownedByNewTerm.Add(v); + copy.termOwningAUniqueVar[v] = term; + } + } + + // Actually claim ownership + copy.uniqueVarsOwnedByATerm[term] = ownedByNewTerm; + + return copy; + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Triggers/TriggerUtils.cs b/Source/DafnyCore/Triggers/TriggerUtils.cs index 9034be9f27..c68866fb3f 100644 --- a/Source/DafnyCore/Triggers/TriggerUtils.cs +++ b/Source/DafnyCore/Triggers/TriggerUtils.cs @@ -5,127 +5,13 @@ using System; using System.Collections.Generic; -using System.Diagnostics; using System.Diagnostics.Contracts; using System.Linq; -using System.Text; namespace Microsoft.Dafny.Triggers { - class TriggerUtils { - internal static List CopyAndAdd(List seq, T elem) { - var copy = new List(seq); - copy.Add(elem); - return copy; - } - + internal static class TriggerUtils { 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; } - - private ISet variables; - private Dictionary termOwningAUniqueVar; - private Dictionary> uniqueVarsOwnedByATerm; - - public int Count { get { return Terms.Count; } } - - private SetOfTerms() { } - - internal TriggerCandidate ToTriggerCandidate() { - return new TriggerCandidate(Terms); - } - - internal static SetOfTerms Empty() { - var newSet = new SetOfTerms(); - newSet.IsRedundant = false; - newSet.Terms = new List(); - newSet.variables = new HashSet(); - newSet.termOwningAUniqueVar = new Dictionary(); - newSet.uniqueVarsOwnedByATerm = new Dictionary>(); - return newSet; - } - - /// - /// Simple formulas like [P0(i) && P1(i) && P2(i) && P3(i) && P4(i)] yield very - /// large numbers of multi-triggers, most of which are useless. As it copies its - /// argument, this method updates various datastructures that allow it to - /// efficiently track ownership relations between formulae and bound variables, - /// and sets the IsRedundant flag of the returned set, allowing the caller to - /// discard that set of terms, and the ones that would have been built on top of - /// it, thus ensuring that the only sets of terms produced in the end are sets - /// of terms in which each element contributes (owns) at least one variable. - /// - /// Note that this is trickier than just checking every term for new variables; - /// indeed, a new term that does bring new variables in can make an existing - /// term redundant (see redundancy-detection-does-its-job-properly.dfy). - /// - internal SetOfTerms CopyWithAdd(TriggerTerm term, ISet relevantVariables) { - var copy = new SetOfTerms(); - copy.Terms = new List(Terms); - copy.variables = new HashSet(variables); - copy.termOwningAUniqueVar = new Dictionary(termOwningAUniqueVar); - copy.uniqueVarsOwnedByATerm = new Dictionary>(uniqueVarsOwnedByATerm); - - copy.Terms.Add(term); - - var varsInNewTerm = new HashSet(term.BoundVars); - varsInNewTerm.IntersectWith(relevantVariables); - - var ownedByNewTerm = new HashSet(); - - // Check #0: does this term bring anything new? - copy.IsRedundant = IsRedundant || varsInNewTerm.All(bv => copy.variables.Contains(bv)); - copy.variables.UnionWith(varsInNewTerm); - - // Check #1: does this term claiming ownership of all its variables cause another term to become useless? - foreach (var v in varsInNewTerm) { - if (copy.termOwningAUniqueVar.TryGetValue(v, out var originalOwner)) { - var alsoOwnedByOriginalOwner = copy.uniqueVarsOwnedByATerm[originalOwner]; - alsoOwnedByOriginalOwner.Remove(v); - if (!alsoOwnedByOriginalOwner.Any()) { - copy.IsRedundant = true; - } - } else { - ownedByNewTerm.Add(v); - copy.termOwningAUniqueVar[v] = term; - } - } - - // Actually claim ownership - copy.uniqueVarsOwnedByATerm[term] = ownedByNewTerm; - - return copy; - } - } - - internal static IEnumerable AllSubsets(IList source, Func predicate, int offset, ISet relevantVariables) { - if (offset >= source.Count) { - yield return SetOfTerms.Empty(); - yield break; - } - - foreach (var subset in AllSubsets(source, predicate, offset + 1, relevantVariables)) { - var newSet = subset.CopyWithAdd(source[offset], relevantVariables); - if (!newSet.IsRedundant && predicate(subset, source[offset])) { // Fixme remove the predicate? - yield return newSet; - } - yield return subset; - } - } - - internal static IEnumerable AllNonEmptySubsets(IList source, Func predicate, IEnumerable relevantVariables) { - foreach (var subset in AllSubsets(source, predicate, 0, new HashSet(relevantVariables))) { - if (subset.Count > 0) { - yield return subset; - } - } + return source == null ? null : new Attributes(source.Name, source.Args, CopyAttributes(source.Prev)); } internal static List MergeAlterFirst(List a, List b) { @@ -142,143 +28,10 @@ internal static ISet MergeAlterFirst(ISet a, ISet b) { return a; } - internal static bool SameLists(IEnumerable list1, IEnumerable list2, Func comparer) { - if (ReferenceEquals(list1, list2)) { - return true; - } else if ((list1 == null) != (list2 == null)) { - return false; - } - - var it1 = list1.GetEnumerator(); - var it2 = list2.GetEnumerator(); - bool it1_has, it2_has; - bool acc = true; - - do { - it1_has = it1.MoveNext(); - it2_has = it2.MoveNext(); - - if (it1_has == true && it2_has == true) { - acc = acc && comparer(it1.Current, it2.Current); - } - } while (it1_has && it2_has); - - return it1_has == it2_has && acc; - } - - internal static IEnumerable Filter(IEnumerable elements, Func Converter, Func predicate, Action reject) { - var positive = new List(); - foreach (var elem in elements) { - var conv = Converter(elem); - if (predicate(elem, conv)) { - yield return elem; - } else { - reject(elem, conv); - } - } - } - internal static bool SameNullity(T x1, T x2) where T : class { return (x1 == null) == (x2 == null); } - internal string JoinStringsWithHeader(string header, IEnumerable lines) { - return header + String.Join(Environment.NewLine + new String(' ', header.Length), lines); - } - - [Conditional("DEBUG_AUTO_TRIGGERS")] - internal static void DebugTriggers(DafnyOptions options, string format, params object[] more) { - options.ErrorWriter.WriteLine(format, more); - } - - internal static bool AllowsMatchingLoops(ComprehensionExpr quantifier) { - Contract.Requires(!(quantifier is QuantifierExpr) || ((QuantifierExpr)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 WantsAutoTriggers(ComprehensionExpr quantifier) { - Contract.Requires(!(quantifier is QuantifierExpr) || ((QuantifierExpr)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.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers; - } - - internal static bool NeedsAutoTriggers(ComprehensionExpr quantifier) { - Contract.Requires(!(quantifier is QuantifierExpr) || ((QuantifierExpr)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 bool WantsMatchingLoopRewrite(ComprehensionExpr quantifier) { - Contract.Requires(!(quantifier is QuantifierExpr) || ((QuantifierExpr)quantifier).SplitQuantifier == null); - bool wantsMatchingLoopRewrite = true; - return (!Attributes.ContainsBool(quantifier.Attributes, "matchinglooprewrite", ref wantsMatchingLoopRewrite) || wantsMatchingLoopRewrite) && WantsAutoTriggers(quantifier); - } - - private static BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) { - switch (opcode) { - case BinaryExpr.ResolvedOpcode.NotInMap: - return BinaryExpr.ResolvedOpcode.InMap; - case BinaryExpr.ResolvedOpcode.NotInSet: - return BinaryExpr.ResolvedOpcode.InSet; - case BinaryExpr.ResolvedOpcode.NotInSeq: - return BinaryExpr.ResolvedOpcode.InSeq; - case BinaryExpr.ResolvedOpcode.NotInMultiSet: - return BinaryExpr.ResolvedOpcode.InMultiSet; - } - - Contract.Assert(false); - throw new ArgumentException(); - } - - private static BinaryExpr.ResolvedOpcode ChangeProperToInclusiveContainment(BinaryExpr.ResolvedOpcode opcode) { - return opcode switch { - BinaryExpr.ResolvedOpcode.ProperSubset => BinaryExpr.ResolvedOpcode.Subset, - BinaryExpr.ResolvedOpcode.ProperMultiSubset => BinaryExpr.ResolvedOpcode.MultiSubset, - BinaryExpr.ResolvedOpcode.ProperSuperset => BinaryExpr.ResolvedOpcode.Superset, - BinaryExpr.ResolvedOpcode.ProperMultiSuperset => BinaryExpr.ResolvedOpcode.MultiSuperset, - _ => opcode - }; - } - - internal static Expression PrepareExprForInclusionInTrigger(Expression expr, out bool isKiller) { - isKiller = false; - - Expression ret; - do { - ret = expr; - if (expr is BinaryExpr bin) { - if (bin.Op == BinaryExpr.Opcode.NotIn) { - expr = new BinaryExpr(bin.tok, BinaryExpr.Opcode.In, bin.E0, bin.E1) { - ResolvedOp = RemoveNotInBinaryExprIn(bin.ResolvedOp), - Type = bin.Type - }; - } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) { - expr = new SeqSelectExpr(bin.tok, true, bin.E1, bin.E0, null, null) { - Type = bin.Type - }; - isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer - } else { - var newOpcode = ChangeProperToInclusiveContainment(bin.ResolvedOp); - if (newOpcode != bin.ResolvedOp) { - // For sets, isets, and multisets, change < to <= in triggers (and analogously - // > to >=), since "a < b" translates as "a <= b && !(b <= a)" or - // "a <= b && !(a == b)". - expr = new BinaryExpr(bin.tok, BinaryExpr.ResolvedOp2SyntacticOp(newOpcode), bin.E0, bin.E1) { - ResolvedOp = newOpcode, - Type = bin.Type - }; - } - } - } - } while (ret != expr); - - return ret; - } - - internal static Expression PrepareExprForInclusionInTrigger(Expression expr) { - return PrepareExprForInclusionInTrigger(expr, out var @_); - } - internal static IEnumerable MaybeWrapInOld(Expression expr, HashSet/*?*/ wrap) { Contract.Requires(expr != null); Contract.Requires(wrap == null || wrap.Count != 0); diff --git a/Source/DafnyCore/Triggers/TriggersCollector.cs b/Source/DafnyCore/Triggers/TriggersCollector.cs index 9b73f3bec0..a39c6ce38e 100644 --- a/Source/DafnyCore/Triggers/TriggersCollector.cs +++ b/Source/DafnyCore/Triggers/TriggersCollector.cs @@ -4,468 +4,370 @@ using System; using System.Collections.Generic; using System.Linq; -using System.Text; using Microsoft.Boogie; using System.Diagnostics.Contracts; -using System.Diagnostics; - -namespace Microsoft.Dafny.Triggers { - class TriggerTerm { - internal Expression Expr { get; set; } - internal Expression OriginalExpr { get; set; } - internal ISet Variables { get; set; } - internal IEnumerable BoundVars { - get { - return Variables.Select(v => v as BoundVar).Where(v => v != null); - } - } - public override string ToString() { - return Printer.ExprToString(DafnyOptions.DefaultImmutableOptions, Expr); - // NOTE: Using OriginalExpr here could cause some confusion: - // for example, {a !in b} is a binary expression, yielding - // trigger {a in b}. Saying the trigger is a !in b would be - // rather misleading. - } +namespace Microsoft.Dafny.Triggers; - internal enum TermComparison { - SameStrength = 0, Stronger = 1, NotStronger = -1 - } +internal class TriggersCollector { + public ModuleDefinition ForModule { get; } + private readonly DafnyOptions options; + private readonly TriggerAnnotationsCache cache; - internal TermComparison CompareTo(TriggerTerm other) { - if (this == other) { - return TermComparison.SameStrength; - } else if (Expr.AllSubExpressions(true, true).Any(other.Expr.ExpressionEq)) { - return TermComparison.Stronger; - } else { - return TermComparison.NotStronger; - } - } - - internal static bool Eq(TriggerTerm t1, TriggerTerm t2) { - return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr); - } + internal TriggersCollector(Dictionary> exprsInOldContext, DafnyOptions options, ModuleDefinition forModule) { + this.options = options; + this.ForModule = forModule; + this.cache = new TriggerAnnotationsCache(exprsInOldContext); } - class TriggerCandidate { - internal List Terms { get; set; } - internal string Annotation { get; set; } + private T ReduceAnnotatedSubExpressions(Expression expr, T seed, Func map, Func reduce) { + return expr.SubExpressions.Select(e => map(Annotate(e))) + .Aggregate(seed, (acc, e) => reduce(acc, e)); + } - internal TriggerCandidate(List terms) { - this.Terms = terms; - } + private List CollectExportedCandidates(Expression expr) { + return ReduceAnnotatedSubExpressions(expr, new List(), a => a.ExportedTerms, TriggerUtils.MergeAlterFirst); + } - public TriggerCandidate(TriggerCandidate candidate) { - this.Terms = candidate.Terms; - } + private ISet CollectVariables(Expression expr) { + return ReduceAnnotatedSubExpressions>(expr, new HashSet(), a => a.Variables, TriggerUtils.MergeAlterFirst); + } - internal bool MentionsAll(List vars) { - return vars.All(x => Terms.Any(term => term.Variables.Contains(x))); - } + private bool CollectIsKiller(Expression expr) { + return ReduceAnnotatedSubExpressions(expr, false, a => a.IsTriggerKiller, (a, b) => a || b); + } - internal string Repr { get { return String.Join(", ", Terms); } } + private IEnumerable OnlyPrivateCandidates(List terms, IEnumerable privateVars) { + return terms.Where(c => privateVars.Intersect(c.Variables).Any()); //TODO Check perf + } - public override string ToString() { - return "{" + Repr + "}" + (String.IsNullOrWhiteSpace(Annotation) ? "" : " (" + Annotation + ")"); + private TriggerAnnotation Annotate(Expression expr) { + if (cache.Annotations.TryGetValue(expr, out var cached)) { + return cached; } - internal IEnumerable LoopingSubterms(ComprehensionExpr quantifier, DafnyOptions options) { - Contract.Requires(!(quantifier is QuantifierExpr) || ((QuantifierExpr)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); - var boundVars = new HashSet(quantifier.BoundVars); - return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms, boundVars, options)); - } + TriggerAnnotation annotation = null; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort - internal List MatchingSubterms(ComprehensionExpr quantifier) { - Contract.Requires(!(quantifier is QuantifierExpr) || ((QuantifierExpr)quantifier).SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier - return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq); + if (expr is LetExpr) { + var le = (LetExpr)expr; + if (le.LHSs.All(p => p.Var != null) && le.Exact) { + // Inline the let expression before doing trigger selection. + annotation = Annotate(BoogieGenerator.InlineLet(le)); + } } - internal bool IsStrongerThan(TriggerCandidate that) { - if (this == that) { - return false; + if (annotation == null) { + expr.SubExpressions.ForEach(e => Annotate(e)); + + if (IsPotentialTriggerCandidate(expr)) { + annotation = AnnotatePotentialCandidate(expr); + } else if (expr is QuantifierExpr) { + annotation = AnnotateQuantifier((QuantifierExpr)expr); + } else if (expr is LetExpr) { + annotation = AnnotateLetExpr((LetExpr)expr); + } else if (expr is IdentifierExpr) { + annotation = AnnotateIdentifier((IdentifierExpr)expr); + } else if (expr is ApplySuffix) { + annotation = AnnotateApplySuffix((ApplySuffix)expr); + } else if (expr is MatchExpr) { + annotation = AnnotateMatchExpr((MatchExpr)expr); + } else if (expr is NestedMatchExpr nestedMatchExpr) { + annotation = AnnotateNestedMatchExpr(nestedMatchExpr); + } else if (expr is ComprehensionExpr) { + annotation = AnnotateComprehensionExpr((ComprehensionExpr)expr); + } else if (expr is ConcreteSyntaxExpression || + expr is LiteralExpr || + expr is ThisExpr || + expr is BoxingCastExpr || + expr is MultiSetFormingExpr || + expr is SeqConstructionExpr) { + annotation = AnnotateOther(expr, false); + } else { + annotation = AnnotateOther(expr, true); } + } - var hasStrictlyStrongerTerm = false; - foreach (var t in Terms) { - var comparison = that.Terms.Select(t.CompareTo).Max(); - - // All terms of `this` must be at least as strong as a term of `that` - if (comparison == TriggerTerm.TermComparison.NotStronger) { return false; } + cache.Annotations[expr] = annotation; + return annotation; + } - // Did we find a strictly stronger term? - hasStrictlyStrongerTerm = hasStrictlyStrongerTerm || comparison == TriggerTerm.TermComparison.Stronger; + public bool IsPotentialTriggerCandidate(Expression expr) { + if (expr is FunctionCallExpr || + expr is SeqSelectExpr || + expr is MultiSelectExpr || + expr is MemberSelectExpr || + (expr is OldExpr { Useless: false }) || + expr is ApplyExpr || + expr is DisplayExpression || + expr is MapDisplayExpr || + expr is DatatypeValue || + TranslateToFunctionCall(expr)) { + return true; + } else if (expr is BinaryExpr) { + var e = (BinaryExpr)expr; + if ((e.Op == BinaryExpr.Opcode.NotIn || e.Op == BinaryExpr.Opcode.In) && !BoogieGenerator.ExpressionTranslator.RewriteInExpr(e.E1, false)) { + return true; + } else if (CandidateCollectionOperation(e)) { + return true; + } else if (e.E0.Type.IsBigOrdinalType && + (e.ResolvedOp == BinaryExpr.ResolvedOpcode.Lt || e.ResolvedOp == BinaryExpr.ResolvedOpcode.LessThanLimit || e.ResolvedOp == BinaryExpr.ResolvedOpcode.Gt)) { + return true; + } else { + return false; } - - return hasStrictlyStrongerTerm; + } else if (expr is UnaryOpExpr) { + var e = (UnaryOpExpr)expr; + return e.Op == UnaryOpExpr.Opcode.Cardinality; // FIXME || e.Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944 + } else if (expr is ConversionExpr) { + var e = (ConversionExpr)expr; + return e.ToType.IsBigOrdinalType; + } else { + return false; } } - internal class TriggerAnnotation { - internal bool IsTriggerKiller; - internal ISet Variables; - internal readonly List PrivateTerms; - internal readonly List ExportedTerms; - - internal TriggerAnnotation(bool IsTriggerKiller, IEnumerable Variables, IEnumerable AllTerms, IEnumerable PrivateTerms = null) { - this.IsTriggerKiller = IsTriggerKiller; - this.Variables = new HashSet(Variables); - this.PrivateTerms = new List(PrivateTerms == null ? Enumerable.Empty() : PrivateTerms); - this.ExportedTerms = new List(AllTerms == null ? Enumerable.Empty() : AllTerms.Except(this.PrivateTerms)); + // math operations can be turned into a Boogie-level function as in the + // case with /noNLarith. + public bool TranslateToFunctionCall(Expression expr) { + if (!(expr is BinaryExpr)) { + return false; } - - public override string ToString() { - StringBuilder sb = new StringBuilder(); - string indent = " {0}", nindent = "\n - {0}", subindent = "\n * {0}"; - - sb.AppendFormat(indent, IsTriggerKiller); - - sb.AppendFormat(nindent, "Variables:"); - foreach (var bv in Variables) { - sb.AppendFormat(subindent, bv.Name); - } - - sb.AppendFormat(nindent, "Exported terms:"); - foreach (var term in ExportedTerms) { - sb.AppendFormat(subindent, term); - } - - if (PrivateTerms.Any()) { - sb.AppendFormat(nindent, "Private terms:"); - foreach (var term in PrivateTerms) { - sb.AppendFormat(subindent, term); + BinaryExpr e = (BinaryExpr)expr; + bool isReal = e.E0.Type.IsNumericBased(Type.NumericPersuasion.Real); + var disableNonLinearArithmetic = BoogieGenerator.DetermineDisableNonLinearArithmetic(ForModule, options); + switch (e.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Lt: + case BinaryExpr.ResolvedOpcode.Le: + case BinaryExpr.ResolvedOpcode.Ge: + case BinaryExpr.ResolvedOpcode.Gt: + case BinaryExpr.ResolvedOpcode.Add: + case BinaryExpr.ResolvedOpcode.Sub: + if (!isReal && !e.E0.Type.IsBitVectorType && !e.E0.Type.IsBigOrdinalType && disableNonLinearArithmetic) { + return true; } - } - - return sb.ToString(); - } - } - - internal class TriggerAnnotationsCache { - public readonly Dictionary> exprsInOldContext; - public readonly Dictionary annotations; - - /// - /// For certain operations, the TriggersCollector class needs to know whether - /// a particular expression is under an old(...) wrapper. This is in particular - /// true for generating trigger terms (but it is not for checking whether something - /// is a trigger killer, so passing an empty set here for that case would be fine. - /// - public TriggerAnnotationsCache(Dictionary> exprsInOldContext) { - this.exprsInOldContext = exprsInOldContext; - annotations = new Dictionary(); + break; + case BinaryExpr.ResolvedOpcode.Mul: + case BinaryExpr.ResolvedOpcode.Div: + case BinaryExpr.ResolvedOpcode.Mod: + if (!isReal && !e.E0.Type.IsBitVectorType && !e.E0.Type.IsBigOrdinalType) { + if (disableNonLinearArithmetic || (options.ArithMode != 0 && options.ArithMode != 3)) { + return true; + } + } + break; } + return false; } - internal class TriggersCollector { - public ModuleDefinition ForModule { get; } - private DafnyOptions options; - TriggerAnnotationsCache cache; - - internal TriggersCollector(Dictionary> exprsInOldContext, DafnyOptions options, ModuleDefinition forModule) { - this.options = options; - this.ForModule = forModule; - this.cache = new TriggerAnnotationsCache(exprsInOldContext); - } - - private T ReduceAnnotatedSubExpressions(Expression expr, T seed, Func map, Func reduce) { - return expr.SubExpressions.Select(e => map(Annotate(e))) - .Aggregate(seed, (acc, e) => reduce(acc, e)); - } - - private List CollectExportedCandidates(Expression expr) { - return ReduceAnnotatedSubExpressions>(expr, new List(), a => a.ExportedTerms, TriggerUtils.MergeAlterFirst); - } - - private ISet CollectVariables(Expression expr) { - return ReduceAnnotatedSubExpressions>(expr, new HashSet(), a => a.Variables, TriggerUtils.MergeAlterFirst); - } - - private bool CollectIsKiller(Expression expr) { - return ReduceAnnotatedSubExpressions(expr, false, a => a.IsTriggerKiller, (a, b) => a || b); - } - - private IEnumerable OnlyPrivateCandidates(List terms, IEnumerable privateVars) { - return terms.Where(c => privateVars.Intersect(c.Variables).Any()); //TODO Check perf + static bool CandidateCollectionOperation(BinaryExpr binExpr) { + Contract.Requires(binExpr != null); + var type = binExpr.E0.Type.AsCollectionType; + if (type == null) { + return false; } - - private TriggerAnnotation Annotate(Expression expr) { - if (cache.annotations.TryGetValue(expr, out var cached)) { - return cached; - } - - TriggerAnnotation annotation = null; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort - - if (expr is LetExpr) { - var le = (LetExpr)expr; - if (le.LHSs.All(p => p.Var != null) && le.Exact) { - // Inline the let expression before doing trigger selection. - annotation = Annotate(BoogieGenerator.InlineLet(le)); - } - } - - if (annotation == null) { - expr.SubExpressions.ForEach(e => Annotate(e)); - - if (IsPotentialTriggerCandidate(expr)) { - annotation = AnnotatePotentialCandidate(expr); - } else if (expr is QuantifierExpr) { - annotation = AnnotateQuantifier((QuantifierExpr)expr); - } else if (expr is LetExpr) { - annotation = AnnotateLetExpr((LetExpr)expr); - } else if (expr is IdentifierExpr) { - annotation = AnnotateIdentifier((IdentifierExpr)expr); - } else if (expr is ApplySuffix) { - annotation = AnnotateApplySuffix((ApplySuffix)expr); - } else if (expr is MatchExpr) { - annotation = AnnotateMatchExpr((MatchExpr)expr); - } else if (expr is NestedMatchExpr nestedMatchExpr) { - annotation = AnnotateNestedMatchExpr(nestedMatchExpr); - } else if (expr is ComprehensionExpr) { - annotation = AnnotateComprehensionExpr((ComprehensionExpr)expr); - } else if (expr is ConcreteSyntaxExpression || - expr is LiteralExpr || - expr is ThisExpr || - expr is BoxingCastExpr || - expr is MultiSetFormingExpr || - expr is SeqConstructionExpr) { - annotation = AnnotateOther(expr, false); - } else { - annotation = AnnotateOther(expr, true); - } + if (type is SetType) { + switch (binExpr.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Union: + case BinaryExpr.ResolvedOpcode.Intersection: + case BinaryExpr.ResolvedOpcode.SetDifference: + case BinaryExpr.ResolvedOpcode.ProperSubset: + case BinaryExpr.ResolvedOpcode.Subset: + case BinaryExpr.ResolvedOpcode.Superset: + case BinaryExpr.ResolvedOpcode.ProperSuperset: + return true; } - - TriggerUtils.DebugTriggers(options, "{0} ({1})\n{2}", Printer.ExprToString(options, expr), expr.GetType(), annotation); - cache.annotations[expr] = annotation; - return annotation; - } - - public bool IsPotentialTriggerCandidate(Expression expr) { - if (expr is FunctionCallExpr || - expr is SeqSelectExpr || - expr is MultiSelectExpr || - expr is MemberSelectExpr || - (expr is OldExpr { Useless: false }) || - expr is ApplyExpr || - expr is DisplayExpression || - expr is MapDisplayExpr || - expr is DatatypeValue || - TranslateToFunctionCall(expr)) { - return true; - } else if (expr is BinaryExpr) { - var e = (BinaryExpr)expr; - if ((e.Op == BinaryExpr.Opcode.NotIn || e.Op == BinaryExpr.Opcode.In) && !BoogieGenerator.ExpressionTranslator.RewriteInExpr(e.E1, false)) { + } else if (type is MultiSetType) { + switch (binExpr.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.MultiSetUnion: + case BinaryExpr.ResolvedOpcode.MultiSetIntersection: + case BinaryExpr.ResolvedOpcode.MultiSetDifference: + case BinaryExpr.ResolvedOpcode.ProperMultiSubset: + case BinaryExpr.ResolvedOpcode.MultiSubset: + case BinaryExpr.ResolvedOpcode.MultiSuperset: + case BinaryExpr.ResolvedOpcode.ProperMultiSuperset: return true; - } else if (CandidateCollectionOperation(e)) { + } + } else if (type is SeqType) { + switch (binExpr.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Concat: return true; - } else if (e.E0.Type.IsBigOrdinalType && - (e.ResolvedOp == BinaryExpr.ResolvedOpcode.Lt || e.ResolvedOp == BinaryExpr.ResolvedOpcode.LessThanLimit || e.ResolvedOp == BinaryExpr.ResolvedOpcode.Gt)) { + } + } else if (type is MapType) { + switch (binExpr.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.MapMerge: + case BinaryExpr.ResolvedOpcode.MapSubtraction: return true; - } else { - return false; - } - } else if (expr is UnaryOpExpr) { - var e = (UnaryOpExpr)expr; - return e.Op == UnaryOpExpr.Opcode.Cardinality; // FIXME || e.Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944 - } else if (expr is ConversionExpr) { - var e = (ConversionExpr)expr; - return e.ToType.IsBigOrdinalType; - } else { - return false; } } + return false; + } - // math operations can be turned into a Boogie-level function as in the - // case with /noNLarith. - public bool TranslateToFunctionCall(Expression expr) { - if (!(expr is BinaryExpr)) { - return false; - } - BinaryExpr e = (BinaryExpr)expr; - bool isReal = e.E0.Type.IsNumericBased(Type.NumericPersuasion.Real); - var disableNonLinearArithmetic = BoogieGenerator.DetermineDisableNonLinearArithmetic(ForModule, options); - switch (e.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.Lt: - case BinaryExpr.ResolvedOpcode.Le: - case BinaryExpr.ResolvedOpcode.Ge: - case BinaryExpr.ResolvedOpcode.Gt: - case BinaryExpr.ResolvedOpcode.Add: - case BinaryExpr.ResolvedOpcode.Sub: - if (!isReal && !e.E0.Type.IsBitVectorType && !e.E0.Type.IsBigOrdinalType && disableNonLinearArithmetic) { - return true; - } - break; - case BinaryExpr.ResolvedOpcode.Mul: - case BinaryExpr.ResolvedOpcode.Div: - case BinaryExpr.ResolvedOpcode.Mod: - if (!isReal && !e.E0.Type.IsBitVectorType && !e.E0.Type.IsBigOrdinalType) { - if (disableNonLinearArithmetic || (options.ArithMode != 0 && options.ArithMode != 3)) { - return true; - } - } - break; + private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) { + var oldExprSet = cache.ExpressionsInOldContext.GetValueOrDefault(expr); + // oldExpr has been set to the value found + var newExpressions = TriggerUtils.MaybeWrapInOld(PrepareExprForInclusionInTrigger(expr, out var exprIsKiller), oldExprSet); + // We expect there to be at least one "newExpressions". + // We also expect that the computation of new_term.Variables, collected_terms, and children_contain_killers will be the + // same for each of the "new_exprs". + // Therefore, we use the values of these variables from the last iteration in the expression that is ultimately returned. + TriggerTerm newTerm = null; + List collectedTerms = null; + var childrenContainKillers = false; + foreach (var newExpression in newExpressions) { + newTerm = new TriggerTerm { Expr = newExpression, OriginalExpr = expr, Variables = CollectVariables(expr) }; + + collectedTerms = CollectExportedCandidates(expr); + childrenContainKillers = CollectIsKiller(expr); + + if (!childrenContainKillers) { + // Add only if the children are not killers; the head has been cleaned up into non-killer form + collectedTerms.Add(newTerm); } - return false; } + Contract.Assert(newTerm != null); // this checks our assumption that "new_exprs" contains at least one value. - static bool CandidateCollectionOperation(BinaryExpr binExpr) { - Contract.Requires(binExpr != null); - var type = binExpr.E0.Type.AsCollectionType; - if (type == null) { - return false; - } - if (type is SetType) { - switch (binExpr.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.Union: - case BinaryExpr.ResolvedOpcode.Intersection: - case BinaryExpr.ResolvedOpcode.SetDifference: - case BinaryExpr.ResolvedOpcode.ProperSubset: - case BinaryExpr.ResolvedOpcode.Subset: - case BinaryExpr.ResolvedOpcode.Superset: - case BinaryExpr.ResolvedOpcode.ProperSuperset: - return true; - default: - break; - } - } else if (type is MultiSetType) { - switch (binExpr.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.MultiSetUnion: - case BinaryExpr.ResolvedOpcode.MultiSetIntersection: - case BinaryExpr.ResolvedOpcode.MultiSetDifference: - case BinaryExpr.ResolvedOpcode.ProperMultiSubset: - case BinaryExpr.ResolvedOpcode.MultiSubset: - case BinaryExpr.ResolvedOpcode.MultiSuperset: - case BinaryExpr.ResolvedOpcode.ProperMultiSuperset: - return true; - default: - break; - } - } else if (type is SeqType) { - switch (binExpr.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.Concat: - return true; - default: - break; - } - } else if (type is MapType) { - switch (binExpr.ResolvedOp) { - case BinaryExpr.ResolvedOpcode.MapMerge: - case BinaryExpr.ResolvedOpcode.MapSubtraction: - return true; - default: - break; - } - } - return false; - } + // This new node is a killer if its children were killers, or if it's non-cleaned-up head is a killer + return new TriggerAnnotation(childrenContainKillers || exprIsKiller, newTerm.Variables, collectedTerms); + } - private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) { - bool expr_is_killer = false; - if (cache.exprsInOldContext.TryGetValue(expr, out var oldExprSet)) { - // oldExpr has been set to the value found - } else { - oldExprSet = null; - } - var new_exprs = TriggerUtils.MaybeWrapInOld(TriggerUtils.PrepareExprForInclusionInTrigger(expr, out expr_is_killer), oldExprSet); - // We expect there to be at least one "new_exprs". - // We also expect that the computation of new_term.Variables, collected_terms, and children_contain_killers will be the - // same for each of the "new_exprs". - // Therefore, we use the values of these variables from the last iteration in the expression that is ultimately returned. - TriggerTerm new_term = null; - List collected_terms = null; - var children_contain_killers = false; - foreach (var new_expr in new_exprs) { - new_term = new TriggerTerm { Expr = new_expr, OriginalExpr = expr, Variables = CollectVariables(expr) }; - - collected_terms = CollectExportedCandidates(expr); - children_contain_killers = CollectIsKiller(expr); - - if (!children_contain_killers) { - // Add only if the children are not killers; the head has been cleaned up into non-killer form - collected_terms.Add(new_term); - } - } - Contract.Assert(new_term != null); // this checks our assumption that "new_exprs" contains at least one value. + private TriggerAnnotation AnnotateApplySuffix(ApplySuffix expr) { + // This is a bit tricky. A funcall node is generally meaningful as a trigger candidate, + // but when it's part of an ApplySuffix the function call itself may not resolve properly + // when the second round of resolving is done after modules are duplicated. + // Thus first we annotate expr and create a trigger candidate, and then we remove the + // candidate matching its direct subexpression if needed. Note that function calls are not the + // only possible child here; there can be DatatypeValue nodes, for example (see vstte2012/Combinators.dfy). + var annotation = AnnotatePotentialCandidate(expr); + // Comparing by reference is fine here. Using sets could yield a small speedup + annotation.ExportedTerms.RemoveAll(term => expr.SubExpressions.Contains(term.Expr)); + return annotation; + } - // This new node is a killer if its children were killers, or if it's non-cleaned-up head is a killer - return new TriggerAnnotation(children_contain_killers || expr_is_killer, new_term.Variables, collected_terms); - } + private TriggerAnnotation AnnotateQuantifierOrLetExpr(Expression expr, IEnumerable boundVars) { + var terms = CollectExportedCandidates(expr); + return new TriggerAnnotation(true, CollectVariables(expr), terms, OnlyPrivateCandidates(terms, boundVars)); + } - private TriggerAnnotation AnnotateApplySuffix(ApplySuffix expr) { - // This is a bit tricky. A funcall node is generally meaningful as a trigger candidate, - // but when it's part of an ApplySuffix the function call itself may not resolve properly - // when the second round of resolving is done after modules are duplicated. - // Thus first we annotate expr and create a trigger candidate, and then we remove the - // candidate matching its direct subexpression if needed. Note that function calls are not the - // only possible child here; there can be DatatypeValue nodes, for example (see vstte2012/Combinators.dfy). - var annotation = AnnotatePotentialCandidate(expr); - // Comparing by reference is fine here. Using sets could yield a small speedup - annotation.ExportedTerms.RemoveAll(term => expr.SubExpressions.Contains(term.Expr)); - return annotation; - } + private TriggerAnnotation AnnotateQuantifier(QuantifierExpr expr) { + return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars); + } - private TriggerAnnotation AnnotateQuantifierOrLetExpr(Expression expr, IEnumerable boundVars) { - var terms = CollectExportedCandidates(expr); - return new TriggerAnnotation(true, CollectVariables(expr), terms, OnlyPrivateCandidates(terms, boundVars)); - } + private TriggerAnnotation AnnotateLetExpr(LetExpr expr) { + return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars); + } - private TriggerAnnotation AnnotateQuantifier(QuantifierExpr expr) { - return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars); - } + private TriggerAnnotation AnnotateIdentifier(IdentifierExpr expr) { + return new TriggerAnnotation(false, Enumerable.Repeat(expr.Var, 1), null); + } - private TriggerAnnotation AnnotateLetExpr(LetExpr expr) { - return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars); - } + private TriggerAnnotation AnnotateComprehensionExpr(ComprehensionExpr expr) { + var terms = CollectExportedCandidates(expr); + return new TriggerAnnotation(true, CollectVariables(expr), terms, OnlyPrivateCandidates(terms, expr.BoundVars)); + } - private TriggerAnnotation AnnotateIdentifier(IdentifierExpr expr) { - return new TriggerAnnotation(false, Enumerable.Repeat(expr.Var, 1), null); - } + private TriggerAnnotation AnnotateNestedMatchExpr(NestedMatchExpr expr) { + var candidateTerms = CollectExportedCandidates(expr); + // collects that argument boundvar of matchcaseexpr + var variables = expr.Cases.SelectMany(e => e.Pat.DescendantsAndSelf). + OfType().Select(id => id.BoundVar).Where(b => b != null).ToList(); + // remove terms that mentions argument boundvar of matchcaseexpr + var terms = candidateTerms.Where(term => variables.Any(x => !term.Variables.Contains(x))).ToList(); + return new TriggerAnnotation(true, CollectVariables(expr), terms); + } - private TriggerAnnotation AnnotateComprehensionExpr(ComprehensionExpr expr) { - var terms = CollectExportedCandidates(expr); - return new TriggerAnnotation(true, CollectVariables(expr), terms, OnlyPrivateCandidates(terms, expr.BoundVars)); + private TriggerAnnotation AnnotateMatchExpr(MatchExpr expr) { + var pts = CollectExportedCandidates(expr); + // collects that argument boundvar of matchcaseexpr + var variables = expr.Cases.Select(e => e.Arguments). + Aggregate(new List(), (acc, e) => TriggerUtils.MergeAlterFirst(acc, e)); + // remove terms that mentions argument boundvar of matchcaseexpr + var terms = new List(); + foreach (var term in pts) { + if (!(variables.All(x => term.Variables.Contains(x)))) { + terms.Add(term); + } } + return new TriggerAnnotation(true, CollectVariables(expr), terms); + } - private TriggerAnnotation AnnotateNestedMatchExpr(NestedMatchExpr expr) { - var candidateTerms = CollectExportedCandidates(expr); - // collects that argument boundvar of matchcaseexpr - var variables = expr.Cases.SelectMany(e => e.Pat.DescendantsAndSelf). - OfType().Select(id => id.BoundVar).Where(b => b != null).ToList(); - // remove terms that mentions argument boundvar of matchcaseexpr - var terms = candidateTerms.Where(term => variables.Any(x => !term.Variables.Contains(x))).ToList(); - return new TriggerAnnotation(true, CollectVariables(expr), terms); - } + private TriggerAnnotation AnnotateOther(Expression expr, bool isTriggerKiller) { + return new TriggerAnnotation(isTriggerKiller || CollectIsKiller(expr), CollectVariables(expr), CollectExportedCandidates(expr)); + } - private TriggerAnnotation AnnotateMatchExpr(MatchExpr expr) { - var pts = CollectExportedCandidates(expr); - // collects that argument boundvar of matchcaseexpr - var variables = expr.Cases.Select(e => e.Arguments). - Aggregate(new List(), (acc, e) => TriggerUtils.MergeAlterFirst(acc, e)); - // remove terms that mentions argument boundvar of matchcaseexpr - var terms = new List(); - foreach (var term in pts) { - if (!(variables.All(x => term.Variables.Contains(x)))) { - terms.Add(term); + /// + /// Collect terms in the body of the subexpressions of the argument that look like quantifiers. The results of this function can contain duplicate terms. + /// + internal List CollectTriggers(ComprehensionExpr quantifier) { + Contract.Requires(!(quantifier is QuantifierExpr) || ((QuantifierExpr)quantifier).SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier + // NOTE: We could check for existing trigger attributes and return that instead + return Annotate(quantifier).PrivateTerms; + } + + internal bool IsTriggerKiller(Expression expr) { + return Annotate(expr).IsTriggerKiller; + } + + internal static Expression PrepareExprForInclusionInTrigger(Expression expr) { + return PrepareExprForInclusionInTrigger(expr, out var @_); + } + + private static Expression PrepareExprForInclusionInTrigger(Expression expr, out bool isKiller) { + isKiller = false; + + Expression ret; + do { + ret = expr; + if (expr is BinaryExpr bin) { + if (bin.Op == BinaryExpr.Opcode.NotIn) { + expr = new BinaryExpr(bin.tok, BinaryExpr.Opcode.In, bin.E0, bin.E1) { + ResolvedOp = RemoveNotInBinaryExprIn(bin.ResolvedOp), + Type = bin.Type + }; + } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) { + expr = new SeqSelectExpr(bin.tok, true, bin.E1, bin.E0, null, null) { + Type = bin.Type + }; + isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer + } else { + var newOpcode = ChangeProperToInclusiveContainment(bin.ResolvedOp); + if (newOpcode != bin.ResolvedOp) { + // For sets, isets, and multisets, change < to <= in triggers (and analogously + // > to >=), since "a < b" translates as "a <= b && !(b <= a)" or + // "a <= b && !(a == b)". + expr = new BinaryExpr(bin.tok, BinaryExpr.ResolvedOp2SyntacticOp(newOpcode), bin.E0, bin.E1) { + ResolvedOp = newOpcode, + Type = bin.Type + }; + } } } - return new TriggerAnnotation(true, CollectVariables(expr), terms); - } - - private TriggerAnnotation AnnotateOther(Expression expr, bool isTriggerKiller) { - return new TriggerAnnotation(isTriggerKiller || CollectIsKiller(expr), CollectVariables(expr), CollectExportedCandidates(expr)); - } + } while (ret != expr); - /// - /// Collect terms in the body of the subexpressions of the argument that look like quantifiers. The results of this function can contain duplicate terms. - /// - internal List CollectTriggers(ComprehensionExpr quantifier) { - Contract.Requires(!(quantifier is QuantifierExpr) || ((QuantifierExpr)quantifier).SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier - // NOTE: We could check for existing trigger attributes and return that instead - return Annotate(quantifier).PrivateTerms; - } + return ret; + } + private static BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) { + switch (opcode) { + case BinaryExpr.ResolvedOpcode.NotInMap: + return BinaryExpr.ResolvedOpcode.InMap; + case BinaryExpr.ResolvedOpcode.NotInSet: + return BinaryExpr.ResolvedOpcode.InSet; + case BinaryExpr.ResolvedOpcode.NotInSeq: + return BinaryExpr.ResolvedOpcode.InSeq; + case BinaryExpr.ResolvedOpcode.NotInMultiSet: + return BinaryExpr.ResolvedOpcode.InMultiSet; + } + + Contract.Assert(false); + throw new ArgumentException(); + } - internal bool IsTriggerKiller(Expression expr) { - return Annotate(expr).IsTriggerKiller; - } + private static BinaryExpr.ResolvedOpcode ChangeProperToInclusiveContainment(BinaryExpr.ResolvedOpcode opcode) { + return opcode switch { + BinaryExpr.ResolvedOpcode.ProperSubset => BinaryExpr.ResolvedOpcode.Subset, + BinaryExpr.ResolvedOpcode.ProperMultiSubset => BinaryExpr.ResolvedOpcode.MultiSubset, + BinaryExpr.ResolvedOpcode.ProperSuperset => BinaryExpr.ResolvedOpcode.Superset, + BinaryExpr.ResolvedOpcode.ProperMultiSuperset => BinaryExpr.ResolvedOpcode.MultiSuperset, + _ => opcode + }; } -} +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.expect index 90b6f86140..6a415d0758 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.expect @@ -4,9 +4,9 @@ TestAuditor.dfy(95,4): Warning: note, this forall statement has no body TestAuditor.dfy(102,4): Warning: note, this loop has no body (loop frame: i) TestAuditor.dfy(139,2): Warning: note, this forall statement has no body TestAuditor.dfy(143,2): Warning: note, this loop has no body (loop frame: i) -TestAuditor.dfy(93,10): Warning: /!\ No terms found to trigger on. -TestAuditor.dfy(95,4): Warning: /!\ No terms found to trigger on. -TestAuditor.dfy(139,2): Warning: /!\ No terms found to trigger on. +TestAuditor.dfy(93,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +TestAuditor.dfy(95,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +TestAuditor.dfy(139,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. TestAuditor.dfy(22,6): Warning: MinusBv8NoBody: Ghost declaration has no body and has an ensures clause. Possible mitigation: Provide a body or add `{:axiom}`. TestAuditor.dfy(27,15): Warning: LeftShiftBV128: Declaration has explicit `{:axiom}` attribute. Possible mitigation: Provide a proof or test. TestAuditor.dfy(38,2): Warning: MinusBv8Assume: Definition has `assume` statement in body. Possible mitigation: Replace with `assert` and prove or add `{:axiom}`. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorResolution.dfy.expect index 257b30e428..fd0c43672d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorResolution.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorResolution.dfy.expect @@ -10,11 +10,11 @@ BitvectorResolution.dfy(40,15): Error: type of right argument to << (real) must BitvectorResolution.dfy(41,15): Error: type of right argument to << (SmallReal) must be an integer-numeric or bitvector type BitvectorResolution.dfy(42,25): Error: incorrect argument type for function parameter 'w' (expected nat, found real) BitvectorResolution.dfy(43,25): Error: incorrect argument type for function parameter 'w' (expected nat, found SmallReal) -BitvectorResolution.dfy(94,10): Warning: /!\ No terms found to trigger on. -BitvectorResolution.dfy(95,10): Warning: /!\ No terms found to trigger on. -BitvectorResolution.dfy(96,10): Warning: /!\ No terms found to trigger on. -BitvectorResolution.dfy(98,14): Warning: /!\ No terms found to trigger on. -BitvectorResolution.dfy(99,14): Warning: /!\ No terms found to trigger on. -BitvectorResolution.dfy(100,14): Warning: /!\ No terms found to trigger on. +BitvectorResolution.dfy(94,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +BitvectorResolution.dfy(95,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +BitvectorResolution.dfy(96,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +BitvectorResolution.dfy(98,14): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +BitvectorResolution.dfy(99,14): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +BitvectorResolution.dfy(100,14): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. BitvectorResolution.dfy(110,19): Error: the type of this expression is underspecified 13 resolution/type errors detected in BitvectorResolution.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Comprehensions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Comprehensions.dfy.expect index 96cc85d3cf..5a5ad58161 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Comprehensions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Comprehensions.dfy.expect @@ -1,9 +1,9 @@ -Comprehensions.dfy(6,17): Warning: /!\ No terms found to trigger on. -Comprehensions.dfy(22,11): Warning: /!\ No terms found to trigger on. -Comprehensions.dfy(24,7): Warning: /!\ No terms found to trigger on. -Comprehensions.dfy(25,11): Warning: /!\ No terms found to trigger on. -Comprehensions.dfy(32,11): Warning: /!\ No trigger covering all quantified variables found. -Comprehensions.dfy(54,11): Warning: /!\ No terms found to trigger on. +Comprehensions.dfy(6,17): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Comprehensions.dfy(22,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Comprehensions.dfy(24,7): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Comprehensions.dfy(25,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Comprehensions.dfy(32,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Comprehensions.dfy(54,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Comprehensions.dfy(12,13): Error: assertion might not hold Comprehensions.dfy(78,22): Error: assertion might not hold Comprehensions.dfy(99,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ComprehensionsNewSyntax.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ComprehensionsNewSyntax.dfy.expect index 39cf742db4..bc8699851c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ComprehensionsNewSyntax.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ComprehensionsNewSyntax.dfy.expect @@ -1,9 +1,9 @@ -ComprehensionsNewSyntax.dfy(6,17): Warning: /!\ No terms found to trigger on. -ComprehensionsNewSyntax.dfy(22,11): Warning: /!\ No terms found to trigger on. -ComprehensionsNewSyntax.dfy(24,7): Warning: /!\ No terms found to trigger on. -ComprehensionsNewSyntax.dfy(25,11): Warning: /!\ No terms found to trigger on. -ComprehensionsNewSyntax.dfy(32,11): Warning: /!\ No trigger covering all quantified variables found. -ComprehensionsNewSyntax.dfy(54,11): Warning: /!\ No terms found to trigger on. +ComprehensionsNewSyntax.dfy(6,17): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ComprehensionsNewSyntax.dfy(22,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ComprehensionsNewSyntax.dfy(24,7): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ComprehensionsNewSyntax.dfy(25,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ComprehensionsNewSyntax.dfy(32,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ComprehensionsNewSyntax.dfy(54,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. ComprehensionsNewSyntax.dfy(12,13): Error: assertion might not hold ComprehensionsNewSyntax.dfy(78,22): Error: assertion might not hold ComprehensionsNewSyntax.dfy(99,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ConcurrentAttribute.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ConcurrentAttribute.dfy.expect index 4438ad7c20..b3ad582b88 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ConcurrentAttribute.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ConcurrentAttribute.dfy.expect @@ -1,7 +1,7 @@ -ConcurrentAttribute.dfy(117,10): Warning: /!\ No terms found to trigger on. -ConcurrentAttribute.dfy(118,13): Warning: /!\ No terms found to trigger on. -ConcurrentAttribute.dfy(123,10): Warning: /!\ No terms found to trigger on. -ConcurrentAttribute.dfy(124,13): Warning: /!\ No terms found to trigger on. +ConcurrentAttribute.dfy(117,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ConcurrentAttribute.dfy(118,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ConcurrentAttribute.dfy(123,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ConcurrentAttribute.dfy(124,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. ConcurrentAttribute.dfy(49,25): Error: reads clause could not be proved to be empty ({:concurrent} restriction) ConcurrentAttribute.dfy(67,32): Error: reads clause could not be proved to be empty ({:concurrent} restriction) ConcurrentAttribute.dfy(74,23): Error: reads clause could not be proved to be empty ({:concurrent} restriction) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DirtyLoops.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DirtyLoops.dfy.expect index 2005bbe0f7..6b336d7326 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DirtyLoops.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DirtyLoops.dfy.expect @@ -42,7 +42,7 @@ DirtyLoops.dfy(436,4): Warning: note, this loop has no body (loop frame: $Heap) DirtyLoops.dfy(452,6): Warning: note, this loop has no body (loop frame: i, $Heap) DirtyLoops.dfy(468,6): Warning: note, this loop has no body (loop frame: i, $Heap) DirtyLoops.dfy(485,6): Warning: note, this loop has no body (loop frame: j, $Heap) -DirtyLoops.dfy(515,2): Warning: /!\ No terms found to trigger on. +DirtyLoops.dfy(515,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. DirtyLoops.dfy(30,11): Error: assertion might not hold DirtyLoops.dfy(39,11): Error: assertion might not hold DirtyLoops.dfy(48,11): Error: assertion might not hold @@ -136,6 +136,6 @@ DirtyLoops.dfy.tmp.dprint.dfy(453,4): Warning: note, this loop has no body (loop DirtyLoops.dfy.tmp.dprint.dfy(469,6): Warning: note, this loop has no body (loop frame: i, $Heap) DirtyLoops.dfy.tmp.dprint.dfy(485,6): Warning: note, this loop has no body (loop frame: i, $Heap) DirtyLoops.dfy.tmp.dprint.dfy(502,6): Warning: note, this loop has no body (loop frame: j, $Heap) -DirtyLoops.dfy.tmp.dprint.dfy(408,2): Warning: /!\ No terms found to trigger on. +DirtyLoops.dfy.tmp.dprint.dfy(408,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier did not attempt verification diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBounds.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBounds.dfy.verifier.expect index 7c4de01ee0..d5c625f883 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBounds.dfy.verifier.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiscoverBounds.dfy.verifier.expect @@ -1,5 +1,5 @@ -DiscoverBounds.dfy(31,7): Warning: /!\ No terms found to trigger on. -DiscoverBounds.dfy(32,7): Warning: /!\ No terms found to trigger on. -DiscoverBounds.dfy(33,7): Warning: /!\ No terms found to trigger on. -DiscoverBounds.dfy(34,7): Warning: /!\ No terms found to trigger on. -DiscoverBounds.dfy(35,7): Warning: /!\ No terms found to trigger on. +DiscoverBounds.dfy(31,7): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +DiscoverBounds.dfy(32,7): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +DiscoverBounds.dfy(33,7): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +DiscoverBounds.dfy(34,7): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +DiscoverBounds.dfy(35,7): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilationNewSyntax.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilationNewSyntax.dfy.verifier.expect index a94cd5ea60..9fa737d84b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilationNewSyntax.dfy.verifier.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilationNewSyntax.dfy.verifier.expect @@ -1,4 +1,4 @@ -ForallCompilationNewSyntax.dfy(25,4): Warning: /!\ No terms found to trigger on. -ForallCompilationNewSyntax.dfy(34,4): Warning: /!\ No terms found to trigger on. -ForallCompilationNewSyntax.dfy(43,4): Warning: /!\ No terms found to trigger on. -ForallCompilationNewSyntax.dfy(63,4): Warning: /!\ No trigger covering all quantified variables found. +ForallCompilationNewSyntax.dfy(25,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ForallCompilationNewSyntax.dfy(34,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ForallCompilationNewSyntax.dfy(43,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ForallCompilationNewSyntax.dfy(63,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/IMaps.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/IMaps.dfy.expect index be7fe6720a..2b345c100f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/IMaps.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/IMaps.dfy.expect @@ -1,7 +1,7 @@ -IMaps.dfy(36,18): Warning: /!\ No terms found to trigger on. -IMaps.dfy(36,49): Warning: /!\ No terms found to trigger on. -IMaps.dfy(51,18): Warning: /!\ No terms found to trigger on. -IMaps.dfy(79,33): Warning: /!\ No terms found to trigger on. +IMaps.dfy(36,18): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +IMaps.dfy(36,49): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +IMaps.dfy(51,18): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +IMaps.dfy(79,33): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. IMaps.dfy(52,7): Error: element might not be in domain Dafny program verifier finished with 14 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy.expect index 0a1a7c2605..e07c395e63 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ISets.dfy.expect @@ -1,4 +1,4 @@ -ISets.dfy(38,15): Warning: /!\ No terms found to trigger on. -ISets.dfy(40,9): Warning: /!\ No terms found to trigger on. +ISets.dfy(38,15): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ISets.dfy(40,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 2 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/InSetComprehension.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/InSetComprehension.dfy.expect index 8b1b941f01..071f0763f2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/InSetComprehension.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/InSetComprehension.dfy.expect @@ -1,13 +1,13 @@ -InSetComprehension.dfy(10,17): Warning: /!\ No terms found to trigger on. -InSetComprehension.dfy(12,17): Warning: /!\ No terms found to trigger on. +InSetComprehension.dfy(10,17): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +InSetComprehension.dfy(12,17): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. InSetComprehension.dfy(14,16): Info: Selected triggers: {Even(m)} InSetComprehension.dfy(16,17): Info: Selected triggers: {u in uu} -InSetComprehension.dfy(18,17): Info: Not generating triggers for "Id(u)". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead. -InSetComprehension.dfy(28,16): Warning: /!\ No terms found to trigger on. -InSetComprehension.dfy(30,16): Warning: /!\ No terms found to trigger on. +InSetComprehension.dfy(18,17): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual. +InSetComprehension.dfy(28,16): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +InSetComprehension.dfy(30,16): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. InSetComprehension.dfy(33,16): Info: Selected triggers: {Even(m)} InSetComprehension.dfy(37,16): Info: Selected triggers: {u in uu} -InSetComprehension.dfy(39,16): Info: Not generating triggers for "Id(u)". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead. +InSetComprehension.dfy(39,16): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual. InSetComprehension.dfy(76,13): Info: Selected triggers: {x in si} InSetComprehension.dfy(78,13): Info: Selected triggers: {y in ti} InSetComprehension.dfy(81,13): Info: Selected triggers: {n in si} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LetExpr.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LetExpr.dfy.expect index b0ba2e8272..ff0182bcae 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LetExpr.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LetExpr.dfy.expect @@ -1,5 +1,5 @@ -LetExpr.dfy(45,2): Warning: /!\ No terms found to trigger on. -LetExpr.dfy(206,4): Warning: /!\ No terms found to trigger on. +LetExpr.dfy(45,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +LetExpr.dfy(206,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. LetExpr.dfy(9,11): Error: assertion might not hold LetExpr.dfy(109,22): Error: assertion might not hold LetExpr.dfy(260,18): Error: value does not satisfy the subset constraints of 'nat' @@ -15,7 +15,7 @@ LetExpr.dfy(390,33): Error: assertion might not hold LetExpr.dfy(403,24): Error: assertion might not hold Dafny program verifier finished with 37 verified, 13 errors -LetExpr.dfy.tmp.print.dfy(44,2): Warning: /!\ No terms found to trigger on. -LetExpr.dfy.tmp.print.dfy(279,4): Warning: /!\ No terms found to trigger on. +LetExpr.dfy.tmp.print.dfy(44,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +LetExpr.dfy.tmp.print.dfy(279,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier did not attempt verification diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Maps.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Maps.dfy.expect index 735cf402a2..b365e9c1f8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Maps.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Maps.dfy.expect @@ -1,4 +1,4 @@ -Maps.dfy(200,11): Warning: /!\ No terms found to trigger on. +Maps.dfy(200,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Maps.dfy(78,7): Error: element might not be in domain Maps.dfy(128,17): Error: assertion might not hold Maps.dfy(220,36): Error: key expressions might be referring to the same value diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/QuantificationNewSyntax.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/QuantificationNewSyntax.dfy.expect index 7505a33194..2c62dba784 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/QuantificationNewSyntax.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/QuantificationNewSyntax.dfy.expect @@ -1,5 +1,5 @@ -QuantificationNewSyntax.dfy(11,13): Warning: /!\ No trigger covering all quantified variables found. -QuantificationNewSyntax.dfy(12,13): Warning: /!\ No trigger covering all quantified variables found. +QuantificationNewSyntax.dfy(11,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +QuantificationNewSyntax.dfy(12,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. QuantificationNewSyntax.dfy(11,42): Error: possible division by zero QuantificationNewSyntax.dfy(13,36): Error: function precondition could not be proved QuantificationNewSyntax.dfy(19,48): Related location diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy.expect index a9c9b85eba..3647f28b04 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy.expect @@ -1,5 +1,5 @@ -ReadsOnMethods.dfy(279,8): Warning: /!\ No terms found to trigger on. -ReadsOnMethods.dfy(280,11): Warning: /!\ No terms found to trigger on. +ReadsOnMethods.dfy(279,8): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +ReadsOnMethods.dfy(280,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. ReadsOnMethods.dfy(19,16): Error: insufficient reads clause to read field ReadsOnMethods.dfy(29,29): Error: insufficient reads clause to read field ReadsOnMethods.dfy(44,32): Error: insufficient reads clause to read field diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect index f4cb7d70ec..ff19928a29 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SmallTests.dfy.expect @@ -1,7 +1,7 @@ SmallTests.dfy(920,4): Warning: You have written an assert statement with a negated condition, but the lack of whitespace between 'assert' and '!' suggests you may be used to Rust and have accidentally negated the asserted condition. If you did not intend the negation, remove the '!' and the parentheses; if you do want the negation, please add a space between the 'assert' and '!'. SmallTests.dfy(926,4): Warning: You have written an assert statement with a negated condition, but the lack of whitespace between 'assert' and '!' suggests you may be used to Rust and have accidentally negated the asserted condition. If you did not intend the negation, remove the '!' and the parentheses; if you do want the negation, please add a space between the 'assert' and '!'. SmallTests.dfy(599,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect -SmallTests.dfy(548,4): Warning: /!\ No trigger covering all quantified variables found. +SmallTests.dfy(548,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. SmallTests.dfy(34,11): Error: index out of range SmallTests.dfy(65,35): Error: possible division by zero SmallTests.dfy(66,50): Error: possible division by zero @@ -58,6 +58,6 @@ SmallTests.dfy(926,10): Error: assertion might not hold Dafny program verifier finished with 56 verified, 50 errors SmallTests.dfy.tmp.dprint.dfy(121,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect -SmallTests.dfy.tmp.dprint.dfy(685,4): Warning: /!\ No trigger covering all quantified variables found. +SmallTests.dfy.tmp.dprint.dfy(685,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier did not attempt verification diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect index 165522db59..e47d3f949d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TriggerInPredicate.dfy.expect @@ -1,4 +1,3 @@ -TriggerInPredicate.dfy(6,38): Info: Not generating triggers for "A(x, y) && z". TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. TriggerInPredicate.dfy(9,20): Info: Some instances of this call are not inlined. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Wellfounded.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Wellfounded.dfy.verifier.expect index e61f12f01b..06c8e5daba 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Wellfounded.dfy.verifier.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Wellfounded.dfy.verifier.expect @@ -1,2 +1,2 @@ -Wellfounded.dfy(48,14): Warning: /!\ No terms found to trigger on. -Wellfounded.dfy(76,5): Warning: /!\ No terms found to trigger on. +Wellfounded.dfy(48,14): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Wellfounded.dfy(76,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect index 2649fdc725..2c26e09e57 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/snapshots/Snapshots5.run.legacy.dfy.expect @@ -1,7 +1,7 @@ -Snapshots5.v0.dfy(10,12): Warning: /!\ No terms found to trigger on. -Snapshots5.v0.dfy(13,10): Warning: /!\ No terms found to trigger on. -Snapshots5.v0.dfy(20,12): Warning: /!\ No terms found to trigger on. -Snapshots5.v0.dfy(26,11): Warning: /!\ No terms found to trigger on. +Snapshots5.v0.dfy(10,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Snapshots5.v0.dfy(13,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Snapshots5.v0.dfy(20,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Snapshots5.v0.dfy(26,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Processing command (at Snapshots5.v0.dfy(10,40)) assert {:id "id1"} (forall b#1_1: bool :: true ==> b#1_1 || !b#1_1) || 0 != 0; >>> DoNothingToAssert Processing command (at Snapshots5.v0.dfy(13,38)) assert {:id "id3"} (forall b#1: bool :: true ==> b#1 || !b#1) || 3 != 3; @@ -10,11 +10,11 @@ Processing command (at Snapshots5.v0.dfy(20,40)) assert {:id "id4"} (forall b#3_ >>> DoNothingToAssert Dafny program verifier finished with 1 verified, 0 errors -Snapshots5.v1.dfy(10,12): Warning: /!\ No terms found to trigger on. -Snapshots5.v1.dfy(13,10): Warning: /!\ No terms found to trigger on. -Snapshots5.v1.dfy(20,12): Warning: /!\ No terms found to trigger on. -Snapshots5.v1.dfy(22,10): Warning: /!\ No terms found to trigger on. -Snapshots5.v1.dfy(27,11): Warning: /!\ No terms found to trigger on. +Snapshots5.v1.dfy(10,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Snapshots5.v1.dfy(13,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Snapshots5.v1.dfy(20,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Snapshots5.v1.dfy(22,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Snapshots5.v1.dfy(27,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Processing command (at Snapshots5.v1.dfy(10,40)) assert {:id "id10"} (forall b#1_1: bool :: true ==> b#1_1 || !b#1_1) || 0 != 0; >>> MarkAsFullyVerified Processing command (at Snapshots5.v1.dfy(13,38)) assert {:id "id12"} (forall b#1: bool :: true ==> b#1 || !b#1) || 3 != 3; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy.verifier.expect index cf10280f37..9c931e1983 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy.verifier.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SmallestMissingNumber-functional.dfy.verifier.expect @@ -1 +1 @@ -SmallestMissingNumber-functional.dfy(212,11): Warning: /!\ No terms found to trigger on. +SmallestMissingNumber-functional.dfy(212,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy index 91b2c8966a..daeb4e94fe 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy @@ -80,7 +80,7 @@ lemma SAppendIsAssociative(a:Stream, b:Stream, c:Stream) { forall k:nat { SAppendIsAssociativeK(k, a, b, c); } // assert for clarity only, postcondition follows directly from it - assert (forall k:nat {:autotriggers false} :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c))); //FIXME: Should Dafny generate a trigger here? If so then which one? + assert (forall k:nat {:trigger} :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c))); //FIXME: Should Dafny generate a trigger here? If so then which one? } // Equivalent proof using the greatest lemma syntax. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy.expect index db81f5e678..73aebefff5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/InductionVsCoinduction.dfy.expect @@ -1,3 +1,3 @@ -InductionVsCoinduction.dfy(81,2): Warning: /!\ No terms found to trigger on. +InductionVsCoinduction.dfy(81,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 12 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy.expect index 183d373ac7..a08ea0c11d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Streams.dfy.expect @@ -1,4 +1,4 @@ -Streams.dfy(65,2): Warning: /!\ No terms found to trigger on. -Streams.dfy(105,2): Warning: /!\ No terms found to trigger on. +Streams.dfy(65,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Streams.dfy(105,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 29 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Ackermann.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Ackermann.dfy.verifier.expect index b302e2b4da..4d91fcbd46 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Ackermann.dfy.verifier.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Ackermann.dfy.verifier.expect @@ -1,2 +1,2 @@ -Ackermann.dfy(162,4): Warning: /!\ No terms found to trigger on. -Ackermann.dfy(180,4): Warning: /!\ No terms found to trigger on. +Ackermann.dfy(162,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +Ackermann.dfy(180,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug63.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug63.dfy.expect index 96e4b779fc..2647ac5097 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug63.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug63.dfy.expect @@ -1,3 +1,3 @@ -Bug63.dfy(5,11): Warning: /!\ No terms found to trigger on. +Bug63.dfy(5,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression1.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression1.dfy.expect index db802e5c4b..79f7ff5f4e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression1.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression1.dfy.expect @@ -1,3 +1,3 @@ -Regression1.dfy(8,20): Warning: /!\ No terms found to trigger on. +Regression1.dfy(8,20): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue1.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue1.dfy.expect index 960e4210e3..d6b019f4a8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue1.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue1.dfy.expect @@ -1,4 +1,4 @@ -git-issue1.dfy(15,11): Warning: /!\ No terms found to trigger on. -git-issue1.dfy(16,11): Warning: /!\ No terms found to trigger on. +git-issue1.dfy(15,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue1.dfy(16,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 2 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue18.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue18.dfy.expect index 48ecd75ed5..79c4758c85 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue18.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue18.dfy.expect @@ -1,3 +1,3 @@ -git-issue18.dfy(7,4): Warning: /!\ No terms found to trigger on. +git-issue18.dfy(7,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue22.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue22.dfy.expect index 201dbe5d40..ad161f5949 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue22.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue22.dfy.expect @@ -1,3 +1,3 @@ -git-issue22.dfy(6,4): Warning: /!\ No terms found to trigger on. +git-issue22.dfy(6,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue48.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue48.dfy.expect index d97f45ab82..3e367ca610 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue48.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue48.dfy.expect @@ -1,3 +1,3 @@ -git-issue48-include.dfyi(4,8): Warning: /!\ No terms found to trigger on. +git-issue48-include.dfyi(4,8): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue75.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue75.dfy.expect index c49f71430d..21cd575191 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue75.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue75.dfy.expect @@ -1,4 +1,4 @@ -git-issue75.dfy(12,7): Warning: /!\ No terms found to trigger on. -git-issue75.dfy(17,7): Warning: /!\ No terms found to trigger on. +git-issue75.dfy(12,7): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue75.dfy(17,7): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 3 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue92.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue92.dfy.expect index 5e6b805f90..e02488acf4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue92.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue92.dfy.expect @@ -1,3 +1,3 @@ -git-issue92.dfy(6,25): Warning: /!\ No terms found to trigger on. +git-issue92.dfy(6,25): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue96.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue96.dfy.expect index af531c064a..c7082dd9b1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue96.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue96.dfy.expect @@ -1,4 +1,3 @@ -git-issue96.dfy(14,21): Warning: For expression "0 <= i && i < j && j < 5 ==> s[_t#0] == s[i]": - /!\ No trigger covering all quantified variables found. +git-issue96.dfy(14,21): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 4 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/set-compr.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/set-compr.dfy.expect index c427728058..d45d2b6bb1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/set-compr.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/set-compr.dfy.expect @@ -1,9 +1,9 @@ -set-compr.dfy(6,13): Warning: /!\ No terms found to trigger on. -set-compr.dfy(12,20): Warning: /!\ No terms found to trigger on. -set-compr.dfy(11,21): Warning: /!\ No terms found to trigger on. -set-compr.dfy(13,14): Warning: /!\ No terms found to trigger on. -set-compr.dfy(20,19): Warning: /!\ No terms found to trigger on. -set-compr.dfy(21,9): Warning: /!\ No terms found to trigger on. +set-compr.dfy(6,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +set-compr.dfy(12,20): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +set-compr.dfy(11,21): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +set-compr.dfy(13,14): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +set-compr.dfy(20,19): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +set-compr.dfy(21,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. set-compr.dfy(28,9): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o' set-compr.dfy(39,34): Error: a function definition is not allowed to depend on the set of allocated references set-compr.dfy(41,26): Error: a function definition is not allowed to depend on the set of allocated references diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1207.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1207.dfy.expect index 40d9f8c148..e3502c90ac 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1207.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1207.dfy.expect @@ -1,8 +1,8 @@ -git-issue-1207.dfy(17,9): Warning: /!\ No terms found to trigger on. -git-issue-1207.dfy(29,9): Warning: /!\ No terms found to trigger on. -git-issue-1207.dfy(41,9): Warning: /!\ No terms found to trigger on. -git-issue-1207.dfy(47,9): Warning: /!\ No terms found to trigger on. -git-issue-1207.dfy(48,9): Warning: /!\ No terms found to trigger on. +git-issue-1207.dfy(17,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-1207.dfy(29,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-1207.dfy(41,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-1207.dfy(47,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-1207.dfy(48,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. git-issue-1207.dfy(10,9): Error: assertion might not hold git-issue-1207.dfy(11,9): Error: assertion might not hold git-issue-1207.dfy(14,9): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2265.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2265.dfy.expect index 6562976839..ae693e9a9c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2265.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2265.dfy.expect @@ -1,3 +1,3 @@ -git-issue-2265.dfy(9,11): Warning: /!\ No terms found to trigger on. +git-issue-2265.dfy(9,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2593.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2593.dfy.expect index c56ec7986a..bdd5deee7f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2593.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2593.dfy.expect @@ -1,4 +1,4 @@ git-issue-2593.dfy(7,24): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect -git-issue-2593.dfy(7,10): Warning: /!\ No terms found to trigger on. +git-issue-2593.dfy(7,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2747.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2747.dfy.expect index 881388148e..f68c94f540 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2747.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2747.dfy.expect @@ -1,3 +1,3 @@ -git-issue-2747.dfy(8,9): Warning: /!\ No terms found to trigger on. +git-issue-2747.dfy(8,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3358.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3358.dfy.expect index 646fb336ae..7ef2a6b120 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3358.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3358.dfy.expect @@ -1,2 +1,2 @@ -git-issue-3358.dfy(6,2): Error: /!\ No trigger covering all quantified variables found. +git-issue-3358.dfy(6,2): Error: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. 1 resolution/type errors detected in git-issue-3358.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4007.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4007.dfy.verifier.expect index 1d4310d09b..ea6781257d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4007.dfy.verifier.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4007.dfy.verifier.expect @@ -1 +1 @@ -git-issue-4007.dfy(5,20): Warning: /!\ No terms found to trigger on. +git-issue-4007.dfy(5,20): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.verifier.expect index f4e6be29b1..177ea6f609 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.verifier.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697j.dfy.verifier.expect @@ -1,49 +1,49 @@ -git-issue-697j.dfy(41,12): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(45,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(46,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(47,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(50,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(51,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(55,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(56,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(57,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(59,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(60,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(110,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(111,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(112,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(113,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(117,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(118,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(119,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(144,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(145,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(146,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(147,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(151,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(152,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(153,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(178,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(179,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(180,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(181,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(185,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(186,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(187,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(212,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(213,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(214,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(215,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(219,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(220,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(221,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(240,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(241,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(244,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(245,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(246,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(247,10): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(259,13): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(277,13): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(278,13): Warning: /!\ No terms found to trigger on. -git-issue-697j.dfy(279,13): Warning: /!\ No terms found to trigger on. +git-issue-697j.dfy(41,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(45,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(46,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(47,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(50,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(51,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(55,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(56,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(57,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(59,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(60,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(110,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(111,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(112,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(113,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(117,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(118,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(119,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(144,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(145,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(146,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(147,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(151,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(152,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(153,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(178,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(179,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(180,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(181,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(185,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(186,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(187,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(212,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(213,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(214,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(215,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(219,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(220,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(221,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(240,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(241,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(244,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(245,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(246,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(247,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(259,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(277,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(278,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-697j.dfy(279,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-851.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-851.dfy.expect index 14abeb3988..9a779bc194 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-851.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-851.dfy.expect @@ -1,24 +1,24 @@ -git-issue-851.dfy(116,9): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(144,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(150,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(156,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(162,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(168,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(174,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(180,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(186,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(192,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(211,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(217,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(223,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(229,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(235,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(241,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(247,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(253,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(259,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(265,13): Warning: /!\ No terms found to trigger on. -git-issue-851.dfy(271,13): Warning: /!\ No terms found to trigger on. +git-issue-851.dfy(116,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(144,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(150,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(156,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(162,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(168,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(174,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(180,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(186,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(192,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(211,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(217,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(223,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(229,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(235,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(241,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(247,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(253,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(259,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(265,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +git-issue-851.dfy(271,13): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. git-issue-851.dfy(17,4): Error: cannot establish the existence of LHS values that satisfy the such-that predicate git-issue-851.dfy(37,4): Error: cannot establish the existence of LHS values that satisfy the such-that predicate git-issue-851.dfy(55,4): Error: variable 'd', which is subject to definite-assignment rules, might be uninitialized here diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897.dfy.expect index 7ed98a5a0c..b6de6c6eba 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897.dfy.expect @@ -1,4 +1,4 @@ -git-issue-897.dfy(10,17): Warning: /!\ No terms found to trigger on. +git-issue-897.dfy(10,17): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. git-issue-897.dfy(11,19): Error: assertion might not hold git-issue-897.dfy(16,30): Error: possible violation of postcondition of forall statement diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy.expect index 0db280ffed..b2b4a91b6f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-897a.dfy.expect @@ -1,3 +1,3 @@ -git-issue-897a.dfy(10,17): Warning: /!\ No terms found to trigger on. +git-issue-897a.dfy(10,17): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4144.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4144.dfy.expect index 748466e904..a8a90ef0af 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4144.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4144.dfy.expect @@ -1,20 +1,20 @@ -github-issue-4144.dfy(9,31): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy(10,31): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy(11,31): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy(13,23): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy(14,23): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy(15,23): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](9,31): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](9,31): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](10,31): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](10,31): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](11,31): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](11,31): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](13,23): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](13,23): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](14,23): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](14,23): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](15,23): Warning: /!\ No terms found to trigger on. -github-issue-4144.dfy[Q](15,23): Warning: /!\ No terms found to trigger on. +github-issue-4144.dfy(9,31): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy(10,31): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy(11,31): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy(13,23): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy(14,23): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy(15,23): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](9,31): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](9,31): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](10,31): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](10,31): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](11,31): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](11,31): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](13,23): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](13,23): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](14,23): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](14,23): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](15,23): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +github-issue-4144.dfy[Q](15,23): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 2 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy.expect index 909b183fd5..081616a94b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy.expect @@ -1,4 +1,4 @@ -SumSum.dfy(77,2): Warning: /!\ No terms found to trigger on. -SumSum.dfy(106,6): Warning: /!\ No terms found to trigger on. +SumSum.dfy(77,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +SumSum.dfy(106,6): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 11 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.verifier.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.verifier.expect index dc52d4a07e..2d8130bc48 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.verifier.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestBeyondVerifierExpect.dfy.verifier.expect @@ -1 +1 @@ -TestBeyondVerifierExpect.dfy(6,5): Warning: /!\ No terms found to trigger on. +TestBeyondVerifierExpect.dfy(6,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestMissingVerifierExpect.dfy.testdafny.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestMissingVerifierExpect.dfy.testdafny.expect index 93a2696a0d..4a06fe9d9b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestMissingVerifierExpect.dfy.testdafny.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestMissingVerifierExpect.dfy.testdafny.expect @@ -1,6 +1,6 @@ Using legacy resolver and verifying... AssertEqualWithDiff() Failure Diff (changing expected into actual): -+TestMissingVerifierExpect.dfy(6,5): Warning: /!\ No terms found to trigger on. ++TestMissingVerifierExpect.dfy(6,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. + diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestWrongVerifierExpect.dfy.testdafny.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestWrongVerifierExpect.dfy.testdafny.expect index b31db3c85a..fe05592e8a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestWrongVerifierExpect.dfy.testdafny.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/TestWrongVerifierExpect.dfy.testdafny.expect @@ -2,6 +2,6 @@ Using legacy resolver and verifying... AssertEqualWithDiff() Failure Diff (changing expected into actual): -warning: out of bananas -+TestWrongVerifierExpect.dfy(6,5): Warning: /!\ No terms found to trigger on. ++TestWrongVerifierExpect.dfy(6,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/nested.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/nested.dfy.expect index 1b1813fe52..d49ac978b0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/nested.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/nested.dfy.expect @@ -1,6 +1,6 @@ nested.dfy(8,6): Warning: note, this forall statement has no body -nested.dfy(8,6): Warning: /!\ No terms found to trigger on. -nested.dfy(16,11): Warning: /!\ No terms found to trigger on. +nested.dfy(8,6): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +nested.dfy(16,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. nested.dfy(8,28): Error: match has no cases and this is only allowed when the verifier can prove the match is unreachable nested.dfy(16,11): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions.dfy.expect index 15a41dd21a..d10a298ac9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions.dfy.expect @@ -4,9 +4,9 @@ TestAuditor.dfy(95,4): Warning: note, this forall statement has no body TestAuditor.dfy(102,4): Warning: note, this loop has no body (loop frame: i) TestAuditor.dfy(139,2): Warning: note, this forall statement has no body TestAuditor.dfy(143,2): Warning: note, this loop has no body (loop frame: i) -TestAuditor.dfy(93,10): Warning: /!\ No terms found to trigger on. -TestAuditor.dfy(95,4): Warning: /!\ No terms found to trigger on. -TestAuditor.dfy(139,2): Warning: /!\ No terms found to trigger on. +TestAuditor.dfy(93,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +TestAuditor.dfy(95,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +TestAuditor.dfy(139,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier did not attempt verification TestAuditor.dfy(22,6): Error: Ghost declaration has no body and has an ensures clause. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/simple-session.transcript.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/simple-session.transcript.expect index 610c69ce67..4bf7c322a6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/simple-session.transcript.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/server/simple-session.transcript.expect @@ -253,7 +253,7 @@ transcript(33,0): Warning: module-level methods are always non-instance, so the transcript(10,9): Info: Selected triggers: {x' * x'} transcript(20,9): Info: Selected triggers: {x' * x'} transcript(29,9): Info: Selected triggers: {x' * x'} -transcript(38,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Retrieving cached verification result for implementation M' (correctness)... [1 proof obligation] verified Retrieving cached verification result for implementation M0 (correctness)... @@ -280,7 +280,7 @@ transcript(33,0): Warning: module-level methods are always non-instance, so the transcript(10,9): Info: Selected triggers: {x' * x'} transcript(20,9): Info: Selected triggers: {x' * x'} transcript(29,9): Info: Selected triggers: {x' * x'} -transcript(38,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Retrieving cached verification result for implementation M' (correctness)... [1 proof obligation] verified Retrieving cached verification result for implementation M0 (correctness)... @@ -300,7 +300,7 @@ transcript(33,0): Warning: module-level methods are always non-instance, so the transcript(10,9): Info: Selected triggers: {x' * x'} transcript(20,9): Info: Selected triggers: {x' * x'} transcript(29,9): Info: Selected triggers: {x' * x'} -transcript(38,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Retrieving cached verification result for implementation M' (correctness)... [1 proof obligation] verified Retrieving cached verification result for implementation M0 (correctness)... @@ -319,7 +319,7 @@ transcript(33,0): Warning: module-level methods are always non-instance, so the transcript(10,9): Info: Selected triggers: {x' * x'} transcript(20,9): Info: Selected triggers: {x' * x'} transcript(29,9): Info: Selected triggers: {x' * x'} -transcript(38,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Retrieving cached verification result for implementation M' (correctness)... [1 proof obligation] verified Retrieving cached verification result for implementation M0 (correctness)... @@ -358,7 +358,7 @@ transcript(33,0): Warning: module-level methods are always non-instance, so the transcript(10,9): Info: Selected triggers: {x' * x'} transcript(20,9): Info: Selected triggers: {x' * x'} transcript(29,9): Info: Selected triggers: {x' * x'} -transcript(38,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Retrieving cached verification result for implementation M' (correctness)... [1 proof obligation] verified Retrieving cached verification result for implementation M0 (correctness)... @@ -398,7 +398,7 @@ transcript(33,0): Warning: module-level methods are always non-instance, so the transcript(10,9): Info: Selected triggers: {x' * x'} transcript(20,9): Info: Selected triggers: {x' * x'} transcript(29,9): Info: Selected triggers: {x' * x'} -transcript(38,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Retrieving cached verification result for implementation M' (correctness)... [1 proof obligation] verified Retrieving cached verification result for implementation M0 (correctness)... @@ -417,7 +417,7 @@ transcript(33,0): Warning: module-level methods are always non-instance, so the transcript(10,9): Info: Selected triggers: {x' * x'} transcript(20,9): Info: Selected triggers: {x' * x'} transcript(29,9): Info: Selected triggers: {x' * x'} -transcript(38,9): Warning: /!\ No terms found to trigger on. +transcript(38,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Retrieving cached verification result for implementation M' (correctness)... [1 proof obligation] verified Retrieving cached verification result for implementation M0 (correctness)... diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect index dbc1a3f43f..374f02b7f9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect @@ -2,27 +2,29 @@ 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): Info: Selected triggers: {f(_t#0), f(i)} loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(_t#0), f(i)} -loop-detection-messages--unit-tests.dfy(15,9): Info: For expression "false ==> f(i) == f(_t#0)": - Selected triggers: {f(_t#0), f(i)} -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): Info: For expression "false ==> f(i) == f(_t#0)": - Selected triggers: {f(_t#0), f(i)} -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(_t#0)": - Selected triggers: {f(_t#0), f(i)} -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(15,9): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual. +loop-detection-messages--unit-tests.dfy(15,9): Info: Part #0 is 'false ==> f(i) == f(_t#0)' + Selected triggers: {f(_t#0), f(i)} +loop-detection-messages--unit-tests.dfy(15,9): Info: Part #1 is 'false ==> f(i) == g(i)' + Selected triggers: + {g(i)}, {f(i)} +loop-detection-messages--unit-tests.dfy(16,9): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual. +loop-detection-messages--unit-tests.dfy(16,9): Info: Part #0 is 'false ==> f(i) == f(_t#0)' + Selected triggers: {f(_t#0), f(i)} +loop-detection-messages--unit-tests.dfy(16,9): Info: Part #1 is 'false ==> f(i) == f(i)' + Selected triggers: {f(i)} +loop-detection-messages--unit-tests.dfy(17,9): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual. +loop-detection-messages--unit-tests.dfy(17,9): Info: Part #0 is 'false ==> f(i) == f(_t#0)' + Selected triggers: {f(_t#0), f(i)} +loop-detection-messages--unit-tests.dfy(17,9): Info: Part #1 is '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". 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(20,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +loop-detection-messages--unit-tests.dfy(21,9): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual. 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(24,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. 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)". +loop-detection-messages--unit-tests.dfy(26,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +loop-detection-messages--unit-tests.dfy(27,9): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/regression-tests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/regression-tests.dfy.expect index 5552a60370..87d8839650 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/regression-tests.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/regression-tests.dfy.expect @@ -1,4 +1,4 @@ regression-tests.dfy(15,4): Info: == -regression-tests.dfy(16,5): Warning: /!\ No terms found to trigger on. +regression-tests.dfy(16,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect index d8b5bacaf8..592b2b34dc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect @@ -1,8 +1,9 @@ some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Info: Selected triggers: {s[_t#0], s[x]} -some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: For expression "x in s ==> s[_t#0] > 0": - Selected triggers: {s[_t#0], s[x]} -some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: For expression "x in s ==> _t#0 !in s": - Selected triggers: {s[_t#0], s[x]} +some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual. +some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: Part #0 is 'x in s ==> s[_t#0] > 0' + Selected triggers: {s[_t#0], s[x]} +some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: Part #1 is 'x in s ==> _t#0 !in s' + Selected triggers: {s[_t#0], s[x]} some-terms-do-not-look-like-the-triggers-they-match.dfy(24,18): Info: Selected triggers: {x in s + t} some-terms-do-not-look-like-the-triggers-they-match.dfy(25,18): Info: Selected triggers: {x in t}, {x in s} @@ -15,15 +16,15 @@ some-terms-do-not-look-like-the-triggers-they-match.dfy(32,18): Info: Selected t some-terms-do-not-look-like-the-triggers-they-match.dfy(36,18): Info: Selected triggers: {x in s - t} some-terms-do-not-look-like-the-triggers-they-match.dfy(37,18): Info: Selected triggers: {x in t}, {x in s}, {x in s - t} -some-terms-do-not-look-like-the-triggers-they-match.dfy(43,20): Warning: /!\ No terms found to trigger on. -some-terms-do-not-look-like-the-triggers-they-match.dfy(44,20): Warning: /!\ No terms found to trigger on. +some-terms-do-not-look-like-the-triggers-they-match.dfy(43,20): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +some-terms-do-not-look-like-the-triggers-they-match.dfy(44,20): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. some-terms-do-not-look-like-the-triggers-they-match.dfy(49,20): Info: Selected triggers: {x in s} some-terms-do-not-look-like-the-triggers-they-match.dfy(50,20): Info: Selected triggers: {x in s} -some-terms-do-not-look-like-the-triggers-they-match.dfy(55,18): Warning: /!\ No terms found to trigger on. +some-terms-do-not-look-like-the-triggers-they-match.dfy(55,18): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. some-terms-do-not-look-like-the-triggers-they-match.dfy(55,36): Info: Selected triggers: {y in s} -some-terms-do-not-look-like-the-triggers-they-match.dfy(56,18): Warning: /!\ No terms found to trigger on. +some-terms-do-not-look-like-the-triggers-they-match.dfy(56,18): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. some-terms-do-not-look-like-the-triggers-they-match.dfy(56,39): Info: Selected triggers: {y in s} -some-terms-do-not-look-like-the-triggers-they-match.dfy(58,18): Warning: /!\ No terms found to trigger on. +some-terms-do-not-look-like-the-triggers-they-match.dfy(58,18): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. some-terms-do-not-look-like-the-triggers-they-match.dfy(58,41): Info: Selected triggers: {y in s} some-terms-do-not-look-like-the-triggers-they-match.dfy(59,18): Info: Selected triggers: {x in s} some-terms-do-not-look-like-the-triggers-they-match.dfy(60,18): Info: Selected triggers: {x in F(s)} @@ -42,8 +43,8 @@ some-terms-do-not-look-like-the-triggers-they-match.dfy(84,18): Info: Selected t {t[x]}, {s[x]} some-terms-do-not-look-like-the-triggers-they-match.dfy(86,11): Info: Selected triggers: {t[x]}, {s[x]}, {(s - t)[x]} -some-terms-do-not-look-like-the-triggers-they-match.dfy(92,20): Warning: /!\ No terms found to trigger on. -some-terms-do-not-look-like-the-triggers-they-match.dfy(93,20): Warning: /!\ No terms found to trigger on. +some-terms-do-not-look-like-the-triggers-they-match.dfy(92,20): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +some-terms-do-not-look-like-the-triggers-they-match.dfy(93,20): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. some-terms-do-not-look-like-the-triggers-they-match.dfy(98,20): Info: Selected triggers: {ms[x]} some-terms-do-not-look-like-the-triggers-they-match.dfy(99,20): Info: Selected triggers: {ms[x]} some-terms-do-not-look-like-the-triggers-they-match.dfy(106,18): Info: Selected triggers: {x in s + t} @@ -71,8 +72,8 @@ some-terms-do-not-look-like-the-triggers-they-match.dfy(161,12): Info: Selected some-terms-do-not-look-like-the-triggers-they-match.dfy(162,12): Info: Selected triggers: {x <= ms} some-terms-do-not-look-like-the-triggers-they-match.dfy(163,12): Info: Selected triggers: {x >= ms} some-terms-do-not-look-like-the-triggers-they-match.dfy(164,12): Info: Selected triggers: {x >= ms} -some-terms-do-not-look-like-the-triggers-they-match.dfy(166,12): Warning: /!\ No terms found to trigger on. -some-terms-do-not-look-like-the-triggers-they-match.dfy(167,12): Warning: /!\ No terms found to trigger on. +some-terms-do-not-look-like-the-triggers-they-match.dfy(166,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +some-terms-do-not-look-like-the-triggers-they-match.dfy(167,12): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. some-terms-do-not-look-like-the-triggers-they-match.dfy(152,9): Error: assertion might not hold Dafny program verifier finished with 4 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect index baa42dc513..e66366bd3e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect @@ -6,18 +6,20 @@ 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) || !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)} (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)} (may loop with "P(j + 1)") +splitting-triggers-recovers-expressivity.dfy(44,10): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual. +splitting-triggers-recovers-expressivity.dfy(44,10): Info: Part #0 is 'P(i) || !Q(i)' + Selected triggers: + {Q(i)}, {P(i)} +splitting-triggers-recovers-expressivity.dfy(44,10): Info: Part #1 is '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: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual. +splitting-triggers-recovers-expressivity.dfy(49,11): Info: Part #0 is 'j >= 0 ==> P(j)' + Selected triggers: + {Q(j)}, {P(j)} +splitting-triggers-recovers-expressivity.dfy(49,11): Info: Part #1 is '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: Selected triggers: {P(i)}, {Q(i)} splitting-triggers-recovers-expressivity.dfy(12,63): Error: a postcondition could not be proved on this return path diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect index 447f9feb0b..40a1accb4e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect @@ -1,5 +1,5 @@ -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(7,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error: a precondition for this call could not be proved splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: this is the precondition that could not be proved splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: function precondition could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect index 41cae53559..4abcebe894 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect @@ -1,14 +1,12 @@ -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(10,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +suppressing-warnings-behaves-properly.dfy(11,9): Info: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. +suppressing-warnings-behaves-properly.dfy(12,9): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual. 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(15,9): Info: Selected triggers: {f(n)} +suppressing-warnings-behaves-properly.dfy(16,9): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual. suppressing-warnings-behaves-properly.dfy(18,9): Info: Selected triggers: {g(n), f(_t#0)}, {f(_t#0), f(n)} -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. +suppressing-warnings-behaves-properly.dfy(19,9): Info: Selected triggers: {f(n)} +suppressing-warnings-behaves-properly.dfy(20,9): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 1 verified, 0 errors diff --git a/docs/DafnyRef/Statements.13.expect b/docs/DafnyRef/Statements.13.expect index 4e574bf02a..bb385285b2 100644 --- a/docs/DafnyRef/Statements.13.expect +++ b/docs/DafnyRef/Statements.13.expect @@ -1,3 +1,3 @@ -text.dfy(3,5): Warning: /!\ No terms found to trigger on. +text.dfy(3,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier did not attempt verification diff --git a/docs/DafnyRef/Statements.14.expect b/docs/DafnyRef/Statements.14.expect index 4939363652..9932a32402 100644 --- a/docs/DafnyRef/Statements.14.expect +++ b/docs/DafnyRef/Statements.14.expect @@ -1,3 +1,3 @@ -text.dfy(13,5): Warning: /!\ No terms found to trigger on. +text.dfy(13,5): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier did not attempt verification diff --git a/docs/DafnyRef/Topics.md b/docs/DafnyRef/Topics.md index 866a853718..2dda40fa2a 100644 --- a/docs/DafnyRef/Topics.md +++ b/docs/DafnyRef/Topics.md @@ -1146,3 +1146,29 @@ method TestD(dd: D) { } } ``` + +## 12.8. Quantifier instantiation rules {#sec-quantifier-triggers} +During verification, when Dafny knows that a universal quantifier is true, such as when verifying the body of a function that has the requires clause `forall x :: f(x) == 1`, it may instantiate the quantifier. Instantiation means Dafny will pick a value for all the variables of the quantifier, leading to a new expression, which it hopes to use to prove an assertion. In the above example, instantiating using `3` for `x` will lead to the expression `f(3) == 1`. + +For each universal quantifier, Dafny generates rules to determine which instantiations are worthwhile doing. We call these rules triggers, a term that originates from SMT solvers. If Dafny can not generate triggers for a specific quantifier, it falls back to a set of generic rules. However, this is likely to be problematic, since the generic rules can cause many useless instantiations, leading to verification timing out or failing to proof a valid assertion. When the generic rules are used, Dafny emits a warning telling the user no triggers were found for the quantifier, indicating the Dafny program should be changed so Dafny can find triggers for this quantifier. + +Here follows the approach Dafny uses to generate triggers based on a quantifier. Dafny finds terms in the quantifier body where a quantified variable is used in an operation, such as in a function application `P(x)`, array access `a[x]`, member accesses `x.someField`, or set membership tests `x in S`. To find a trigger, Dafny must find a set of such terms so that each quantified variable is used. You can investigate which triggers Dafny finds by hovering over quantifiers in the IDE and looking for 'Selected triggers', or by using the options `--show-tooltips` when using the LCI. + +There are particular expressions which, for technical reasons, Dafny can not use as part of a trigger. Among others, these expression include: [match](#sec-match-expression), [let](#sec-let-expression), [arithmetic operations and logical connectives](#sec-expressions). For example, in the quantifier `forall x :: x in S ⇐⇒ f(x) > f(x+1)`, Dafny will use `x in S` and `f(x)` as trigger terms, but will not use `x+1` or any terms that contain it. You can investigate which triggers Dafny can not use by hovering over quantifiers in the IDE and looking for 'Rejected triggers', or by using the options `--show-tooltips` when using the LCI. + +Besides not finding triggers, another problematic situation is when Dafny was able to generate triggers, but believes the triggers it found may still cause useless instantiations because they create matching loops. Dafny emits a warning when this happens, indicating the Dafny program should be changed so Dafny can find triggers for this quantifier that do not cause matching loops. + +To understand matching loops, one needs to understand how triggers are used. During a single verification run, such as verifying a method or function, Dafny maintains a set of expressions which it believes to be true, which we call the ground terms. For example, in the body of a method, Dafny knows the requires clauses of that method hold, so the expressions in those will be ground terms. When Dafny steps through the statements of the body, the set of ground terms grows. For example, when an assignment `var x := 3` is evaluated, a ground term `x == 3` will be added. Given a universal quantifier that's a ground term, Dafny will try to pattern match its triggers on sub-expressions of other ground terms. If the pattern matches, that sub-expression is used to instantiate the quantifier. + +Dafny makes sure not to perform the exact same instantiation twice. However, if an instantiation leads to a new term that also matches the trigger, but is different from the term used for the instantiation, the quantifier may be instantiated too often, an event we call a matching loop. For example, given the ground terms `f(3)` and `forall x {f(x)} :: f(x) + f(f(x))`, where `{f(x)}` indicates the trigger for the quantifier, Dafny may instantiate the quantifier using `3` for `x`. This creates a new ground term `f(3) + f(f(3))`, of which the right hand side again matches the trigger, allowing Dafny to instantiate the quantifier again using `f(3)` for `x`, and again and again, leading to an unbounded amount of instantiations. + +Even existential quantifiers need triggers. This is because when Dafny determines an existential quantifier is false, for example in the body of a method that has `requires !exists x :: f(x) == 2`, Dafny will use a logical rewrite rule to change this existential into a universal quantifier, so it becomes `requires forall x :: f(x) != 2`. Before verification, Dafny can not determine whether quantifiers will be determined to be true or false, so it must assume any quantifier may turn into a universal quantifier, and thus they all need triggers. Besides quantifiers, comprehensions such as set and map comprehensions also need triggers, since these are modeled using universal quantifiers. + +Dafny may report 'Quantifier was split into X parts'. This occurs when Dafny determines it can only generate good triggers for a quantifier by splitting it into multiple smaller quantifiers, whose aggregation is logically equivalent to the original one. To maintain logical equivalence, Dafny may have to generate more triggers than if the split had been done manually in the Dafny source file. An example is the expression `forall x :: P(x) && (Q(x) =⇒ P(x+1))`, which Dafny will split into + +```dafny +forall x {P(x)} {Q(x)} :: P(x) && +forall x {(Q(x)} :: Q(x) =⇒ P(x+1) +``` + +Note the trigger `{Q(x)}` in the first quantifier, which was added to maintain equivalence with the original quantifier. If the quantifier had been split in source, only the trigger `{P(x)}` would have been added for `forall x :: P(x)`. diff --git a/docs/OnlineTutorial/Sets.W1.expect b/docs/OnlineTutorial/Sets.W1.expect index 25779fa85c..f331a19471 100644 --- a/docs/OnlineTutorial/Sets.W1.expect +++ b/docs/OnlineTutorial/Sets.W1.expect @@ -1,3 +1,3 @@ -text.dfy(6,9): Warning: /!\ No terms found to trigger on. +text.dfy(6,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 1 verified, 0 errors diff --git a/docs/OnlineTutorial/Sets.W2.expect b/docs/OnlineTutorial/Sets.W2.expect index 687ed435e3..0f54bf67b6 100644 --- a/docs/OnlineTutorial/Sets.W2.expect +++ b/docs/OnlineTutorial/Sets.W2.expect @@ -1,3 +1,3 @@ -text.dfy(3,10): Warning: /!\ No terms found to trigger on. +text.dfy(3,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 1 verified, 0 errors diff --git a/docs/OnlineTutorial/Sets.W3.expect b/docs/OnlineTutorial/Sets.W3.expect index 687ed435e3..0f54bf67b6 100644 --- a/docs/OnlineTutorial/Sets.W3.expect +++ b/docs/OnlineTutorial/Sets.W3.expect @@ -1,3 +1,3 @@ -text.dfy(3,10): Warning: /!\ No terms found to trigger on. +text.dfy(3,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 1 verified, 0 errors diff --git a/docs/OnlineTutorial/guide.17.expect b/docs/OnlineTutorial/guide.17.expect index 169c34eac1..baa44a334d 100644 --- a/docs/OnlineTutorial/guide.17.expect +++ b/docs/OnlineTutorial/guide.17.expect @@ -1,3 +1,3 @@ -text.dfy(3,9): Warning: /!\ No terms found to trigger on. +text.dfy(3,9): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. Dafny program verifier finished with 1 verified, 0 errors