diff options
| -rw-r--r-- | Source/Dafny/Triggers/QuantifiersCollection.cs | 42 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/TriggerUtils.cs | 11 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/TriggersCollector.cs | 35 | ||||
| -rw-r--r-- | Test/triggers/useless-triggers-are-removed.dfy | 25 | ||||
| -rw-r--r-- | Test/triggers/useless-triggers-are-removed.dfy.expect | 17 |
5 files changed, 106 insertions, 24 deletions
diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index e2afa2ee..bfa90d81 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -7,7 +7,6 @@ using System.Text; using Microsoft.Boogie;
using System.Diagnostics.Contracts;
-//FIXME Generated triggers should be _triggers
//FIXME: When scoring, do not consider old(x) to be higher than x.
namespace Microsoft.Dafny.Triggers {
@@ -28,7 +27,7 @@ namespace Microsoft.Dafny.Triggers { internal void TrimInvalidTriggers() {
Contract.Requires(CandidateTerms != null);
Contract.Requires(Candidates != null);
- Candidates = TriggerUtils.Filter(Candidates, tr => tr.MentionsAll(quantifier.BoundVars), tr => { }).ToList();
+ Candidates = TriggerUtils.Filter(Candidates, tr => tr, (tr, _) => tr.MentionsAll(quantifier.BoundVars), (tr, _) => { }).ToList();
}
}
@@ -60,7 +59,13 @@ namespace Microsoft.Dafny.Triggers { return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();
}
- //FIXME document that this assumes that the quantifiers live in the same context and share the same variables
+ /// <summary>
+ /// 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.
+ /// </summary>
+ /// <param name="triggersCollector"></param>
void CollectAndShareTriggers(TriggersCollector triggersCollector) {
var pool = quantifiers.SelectMany(q => triggersCollector.CollectTriggers(q.quantifier));
var distinctPool = pool.Deduplicate(TriggerTerm.Eq);
@@ -79,13 +84,10 @@ namespace Microsoft.Dafny.Triggers { }
void BuildDependenciesGraph() {
- // FIXME: Think more about multi-quantifier dependencies
- //class QuantifierDependency {
- // QuantifierWithTriggers Cause;
- // QuantifierWithTriggers Consequence;
- // List<TriggerCandidate> Triggers;
- // List<Expression> MatchingTerm;
- //}
+ // 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
}
void SuppressMatchingLoops() {
@@ -111,14 +113,14 @@ namespace Microsoft.Dafny.Triggers { foreach (var q in quantifiers) {
var looping = new List<TriggerCandidate>();
- var loopingSubterms = q.Candidates.ToDictionary(candidate => candidate, candidate => candidate.LoopingSubterms(q.quantifier).ToList());
var safe = TriggerUtils.Filter(
q.Candidates,
- c => !loopingSubterms[c].Any(),
- c => {
- looping.Add(c);
- c.Annotation = "loops with " + loopingSubterms[c].MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");
+ candidate => candidate.LoopingSubterms(q.quantifier).ToList(),
+ (candidate, loopingSubterms) => !loopingSubterms.Any(),
+ (candidate, loopingSubterms) => {
+ looping.Add(candidate);
+ candidate.Annotation = "loops with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");
}).ToList();
q.CouldSuppressLoops = safe.Count > 0;
@@ -131,7 +133,15 @@ namespace Microsoft.Dafny.Triggers { }
void SelectTriggers() {
- //FIXME
+ 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 = "stronger than " + String.Join(", ", weakerCandidates);
+ }).ToList();
+ }
}
private void CommitOne(QuantifierWithTriggers q, bool addHeader) {
diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index 9ebcf846..6f76464b 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -76,13 +76,14 @@ namespace Microsoft.Dafny.Triggers { return it1_has == it2_has && acc;
}
- internal static IEnumerable<T> Filter<T>(IEnumerable<T> elements, Func<T, bool> predicate, Action<T> reject) {
+ internal static IEnumerable<T> Filter<T, U>(IEnumerable<T> elements, Func<T, U> Converter, Func<T, U, bool> predicate, Action<T, U> reject) {
var positive = new List<T>();
- foreach (var c in elements) {
- if (predicate(c)) {
- yield return c;
+ foreach (var elem in elements) {
+ var conv = Converter(elem);
+ if (predicate(elem, conv)) {
+ yield return elem;
} else {
- reject(c);
+ reject(elem, conv);
}
}
}
diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 735baa01..3b2853ed 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -20,6 +20,20 @@ namespace Microsoft.Dafny.Triggers { // 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).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);
}
@@ -41,7 +55,7 @@ namespace Microsoft.Dafny.Triggers { return vars.All(x => Terms.Any(term => term.Variables.Contains(x)));
}
- private string Repr { get { return String.Join(", ", Terms); } }
+ internal string Repr { get { return String.Join(", ", Terms); } }
public override string ToString() {
return "{" + Repr + "}" + (String.IsNullOrWhiteSpace(Annotation) ? "" : " (" + Annotation + ")");
@@ -58,8 +72,23 @@ namespace Microsoft.Dafny.Triggers { return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq);
}
- public String AsDafnyAttributeString() {
- return "{:trigger " + Repr + "}";
+ 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;
}
}
diff --git a/Test/triggers/useless-triggers-are-removed.dfy b/Test/triggers/useless-triggers-are-removed.dfy new file mode 100644 index 00000000..16458e41 --- /dev/null +++ b/Test/triggers/useless-triggers-are-removed.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /printTooltips /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file ensures that Dafny does get rid of redundant triggers before
+// annotating a quantifier, and that ths process does not interfere with cycle
+// detection.
+
+function f(x: int): int
+function g(x: int): int
+function h(x: int): int
+
+method M()
+ // In the following, only f(x) is kept. Note that the subset enumeration was
+ // already smart enough to not build any trigger with multiple terms (it only
+ // built 5 candidates)
+ requires forall x: int :: f(x) + g(f(x)) + h(f(x)) + g(h(f(x))) + h(g(f(x))) == 0
+
+ // Loop detection still works fine: in the following example, the trigger is
+ // f(f(x))
+ requires forall x: int :: f(x) == f(f(x))
+
+ // This works for multi-triggers, too:
+ requires forall x, y :: f(x) + g(f(y)) + g(y) + g(f(x)) == 0
+{
+}
diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect new file mode 100644 index 00000000..6c2c0a2b --- /dev/null +++ b/Test/triggers/useless-triggers-are-removed.dfy.expect @@ -0,0 +1,17 @@ +useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)}
+ Rejected triggers:
+ {h(g(f(x)))} (stronger than {g(f(x))}, {f(x)})
+ {g(h(f(x)))} (stronger than {h(f(x))}, {f(x)})
+ {h(f(x))} (stronger than {f(x)})
+ {g(f(x))} (stronger than {f(x)})
+useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))}
+ Rejected triggers: {f(x)} (loops with {f(f(x))})
+useless-triggers-are-removed.dfy(23,11): Info: Selected triggers:
+ {g(f(x)), g(y)}, {f(y), f(x)}
+ Rejected triggers:
+ {g(y), f(x)} (loops with {g(f(y))}, {g(f(x))})
+ {g(f(x)), g(f(y))} (stronger than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)})
+ {g(f(x)), f(y)} (stronger than {f(y), f(x)})
+ {g(f(y)), f(x)} (stronger than {f(y), f(x)})
+
+Dafny program verifier finished with 5 verified, 0 errors
|