1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
|
#define QUANTIFIER_WARNINGS
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using System.Diagnostics.Contracts;
namespace Microsoft.Dafny.Triggers {
class QuantifierWithTriggers {
internal QuantifierExpr quantifier;
internal List<TriggerTerm> CandidateTerms;
internal List<TriggerCandidate> Candidates;
internal List<TriggerCandidate> RejectedCandidates;
internal bool AllowsLoops { get { return TriggerUtils.AllowsMatchingLoops(quantifier); } }
internal bool CouldSuppressLoops { get; set; }
internal QuantifierWithTriggers(QuantifierExpr quantifier) {
this.quantifier = quantifier;
this.RejectedCandidates = new List<TriggerCandidate>();
}
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 List<QuantifierWithTriggers> quantifiers;
internal QuantifiersCollection(IEnumerable<QuantifierExpr> quantifiers, ErrorReporter reporter) {
Contract.Requires(quantifiers.All(q => q.SplitQuantifier == null));
this.reporter = reporter;
this.quantifiers = quantifiers.Select(q => new QuantifierWithTriggers(q)).ToList();
}
internal void ComputeTriggers(TriggersCollector triggersCollector) {
CollectAndShareTriggers(triggersCollector);
TrimInvalidTriggers();
BuildDependenciesGraph();
SuppressMatchingLoops();
SelectTriggers();
}
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();
}
/// <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);
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();
}
}
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
}
void 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.
foreach (var q in quantifiers) {
var looping = new List<TriggerCandidate>();
var safe = TriggerUtils.Filter(
q.Candidates,
candidate => candidate.LoopingSubterms(q.quantifier).ToList(),
(candidate, loopingSubterms) => !loopingSubterms.Any(),
(candidate, loopingSubterms) => {
looping.Add(candidate);
candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "\"" + Printer.ExprToString(t.OriginalExpr) + "\"", ", ");
}).ToList();
q.CouldSuppressLoops = safe.Count > 0;
if (!q.AllowsLoops && q.CouldSuppressLoops) {
q.Candidates = safe;
q.RejectedCandidates.AddRange(looping);
}
}
}
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();
}
}
private void CommitOne(QuantifierWithTriggers q, bool addHeader) {
var errorLevel = ErrorLevel.Info;
var msg = new StringBuilder();
var indent = addHeader ? " " : "";
bool suppressWarnings = Attributes.Contains(q.quantifier.Attributes, "nowarn");
if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: split and autotriggers attributes are passed down to Boogie
var extraMsg = TriggerUtils.WantsAutoTriggers(q.quantifier) ? "" : " Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.";
msg.AppendFormat("Not generating triggers for \"{0}\".{1}", Printer.ExprToString(q.quantifier.Term), extraMsg).AppendLine();
} else {
if (addHeader) {
msg.AppendFormat("For expression \"{0}\":", Printer.ExprToString(q.quantifier.Term)).AppendLine();
}
foreach (var candidate in q.Candidates) {
q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes);
}
AddTriggersToMessage("Selected triggers:", q.Candidates, msg, indent);
AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);
#if QUANTIFIER_WARNINGS
var WARN_TAG = DafnyOptions.O.UnicodeOutput ? "⚠ " : "/!\\ ";
var WARN_TAG_OVERRIDE = suppressWarnings ? "(Suppressed warning) " : WARN_TAG;
var WARN_LEVEL = suppressWarnings ? ErrorLevel.Info : ErrorLevel.Warning;
var WARN = indent + WARN_TAG_OVERRIDE;
if (!q.CandidateTerms.Any()) {
errorLevel = WARN_LEVEL;
msg.Append(WARN).AppendLine("No terms found to trigger on.");
} else if (!q.Candidates.Any()) {
errorLevel = WARN_LEVEL;
msg.Append(WARN).AppendLine("No trigger covering all quantified variables found.");
} else if (!q.CouldSuppressLoops && !q.AllowsLoops) {
errorLevel = WARN_LEVEL;
msg.Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers.");
} else if (suppressWarnings) {
errorLevel = ErrorLevel.Warning;
msg.Append(indent).Append(WARN_TAG).AppendLine("There is no warning here to suppress.");
}
#endif
}
if (msg.Length > 0) {
var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray());
reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr);
}
}
private static void AddTriggersToMessage<T>(string header, List<T> 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() {
foreach (var q in quantifiers) {
CommitOne(q, quantifiers.Count > 1);
}
}
}
}
|
