summaryrefslogtreecommitdiff
path: root/Source/Dafny/Triggers
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny/Triggers')
-rw-r--r--Source/Dafny/Triggers/QuantifierSplitter.cs138
-rw-r--r--Source/Dafny/Triggers/QuantifiersCollection.cs211
-rw-r--r--Source/Dafny/Triggers/QuantifiersCollector.cs57
-rw-r--r--Source/Dafny/Triggers/TriggerExtensions.cs509
-rw-r--r--Source/Dafny/Triggers/TriggerUtils.cs265
-rw-r--r--Source/Dafny/Triggers/TriggersCollector.cs325
6 files changed, 1505 insertions, 0 deletions
diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
new file mode 100644
index 00000000..b039a402
--- /dev/null
+++ b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -0,0 +1,138 @@
+using Microsoft.Boogie;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using System.Text;
+
+namespace Microsoft.Dafny.Triggers {
+ class QuantifierSplitter : BottomUpVisitor {
+ /// This cache was introduced because some statements (notably calc) return the same SubExpression multiple times.
+ /// This ended up causing an inconsistent situation when the calc statement's subexpressions contained the same quantifier
+ /// twice: on the first pass that quantifier got its SplitQuantifiers generated, and on the the second pass these
+ /// split quantifiers got re-split, creating a situation where the direct children of a split quantifier were
+ /// also split quantifiers.
+ private Dictionary<QuantifierExpr, List<Expression>> splits = new Dictionary<QuantifierExpr, List<Expression>>();
+
+ private static BinaryExpr.Opcode FlipOpcode(BinaryExpr.Opcode opCode) {
+ if (opCode == BinaryExpr.Opcode.And) {
+ return BinaryExpr.Opcode.Or;
+ } else if (opCode == BinaryExpr.Opcode.Or) {
+ return BinaryExpr.Opcode.And;
+ } else {
+ throw new ArgumentException();
+ }
+ }
+
+ // NOTE: If we wanted to split quantifiers as far as possible, it would be
+ // enough to put the formulas in DNF (for foralls) or CNF (for exists).
+ // Unfortunately, this would cause ill-behaved quantifiers to produce
+ // exponentially many smaller quantifiers. Thus we only do one step of
+ // distributing, which takes care of the usual precondition case:
+ // forall x :: P(x) ==> (Q(x) && R(x))
+
+ private static UnaryOpExpr Not(Expression expr) {
+ return new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type };
+ }
+
+ private static Attributes CopyAttributes(Attributes source) {
+ if (source == null) {
+ return null;
+ } else {
+ return new Attributes(source.Name, source.Args, CopyAttributes(source.Prev));
+ }
+ }
+
+ internal static IEnumerable<Expression> 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) {
+ foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return Not(e); }
+ } else if (binary != null && binary.Op == separator) {
+ foreach (var e in SplitExpr(binary.E0, separator)) { yield return e; }
+ foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; }
+ } else if (binary != null && binary.Op == BinaryExpr.Opcode.Imp && separator == BinaryExpr.Opcode.Or) {
+ foreach (var e in SplitExpr(Not(binary.E0), separator)) { yield return e; }
+ foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; }
+ } else {
+ yield return expr;
+ }
+ }
+
+ internal static IEnumerable<Expression> SplitAndStich(BinaryExpr pair, BinaryExpr.Opcode separator) {
+ foreach (var e1 in SplitExpr(pair.E1, separator)) {
+ // Notice the token. This makes triggers/splitting-picks-the-right-tokens.dfy possible
+ yield return new BinaryExpr(e1.tok, pair.Op, pair.E0, e1) { ResolvedOp = pair.ResolvedOp, Type = pair.Type };
+ }
+ }
+
+ internal static IEnumerable<Expression> SplitQuantifier(QuantifierExpr quantifier) {
+ var body = quantifier.Term;
+ var binary = body as BinaryExpr;
+
+ if (quantifier is ForallExpr) {
+ IEnumerable<Expression> stream;
+ if (binary != null && (binary.Op == BinaryExpr.Opcode.Imp || binary.Op == BinaryExpr.Opcode.Or)) {
+ stream = SplitAndStich(binary, BinaryExpr.Opcode.And);
+ } else {
+ stream = SplitExpr(body, BinaryExpr.Opcode.And);
+ }
+ foreach (var e in stream) {
+ var tok = new NestedToken(quantifier.tok, e.tok);
+ yield return new ForallExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type };
+ }
+ } else if (quantifier is ExistsExpr) {
+ IEnumerable<Expression> stream;
+ if (binary != null && binary.Op == BinaryExpr.Opcode.And) {
+ stream = SplitAndStich(binary, BinaryExpr.Opcode.Or);
+ } else {
+ stream = SplitExpr(body, BinaryExpr.Opcode.Or);
+ }
+ foreach (var e in stream) {
+ var tok = new NestedToken(quantifier.tok, e.tok);
+ yield return new ExistsExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type };
+ }
+ } else {
+ yield return quantifier;
+ }
+ }
+
+ private static bool AllowsSplitting(QuantifierExpr quantifier) {
+ // allow split if attributes doesn't contains "split" or it is "split: true" and it is not an empty QuantifierExpr (boundvar.count>0)
+ bool splitAttr = true;
+ return (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) && (quantifier.BoundVars.Count > 0);
+ }
+
+ protected override void VisitOneExpr(Expression expr) {
+ var quantifier = expr as QuantifierExpr;
+ if (quantifier != null) {
+ Contract.Assert(quantifier.SplitQuantifier == null);
+ if (!splits.ContainsKey(quantifier) && AllowsSplitting(quantifier)) {
+ splits[quantifier] = SplitQuantifier(quantifier).ToList();
+ }
+ }
+ }
+
+ protected override void VisitOneStmt(Statement stmt) {
+ if (stmt is ForallStmt) {
+ ForallStmt s = (ForallStmt)stmt;
+ if (s.ForallExpressions != null) {
+ foreach (Expression expr in s.ForallExpressions) {
+ VisitOneExpr(expr);
+ }
+ }
+ }
+ }
+
+ /// <summary>
+ /// See comments above definition of splits for reason why this method exists
+ /// </summary>
+ internal void Commit() {
+ foreach (var quantifier in splits.Keys) {
+ quantifier.SplitQuantifier = splits[quantifier];
+ }
+ }
+ }
+}
diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
new file mode 100644
index 00000000..f72dab7f
--- /dev/null
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -0,0 +1,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);
+ }
+ }
+ }
+}
diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
new file mode 100644
index 00000000..cb2d5c6d
--- /dev/null
+++ b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -0,0 +1,57 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Collections.ObjectModel;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Dafny.Triggers {
+ internal class QuantifierCollector : TopDownVisitor<bool> {
+ readonly ErrorReporter reporter;
+ private readonly HashSet<Expression> quantifiers = new HashSet<Expression>();
+ internal readonly HashSet<Expression> exprsInOldContext = new HashSet<Expression>();
+ internal readonly List<QuantifiersCollection> quantifierCollections = new List<QuantifiersCollection>();
+
+ public QuantifierCollector(ErrorReporter reporter) {
+ Contract.Requires(reporter != null);
+ this.reporter = reporter;
+ }
+
+ protected override bool VisitOneExpr(Expression expr, ref bool inOldContext) {
+ var quantifier = expr as QuantifierExpr;
+
+ // only consider quantifiers that are not empty (Bound.Vars.Count > 0)
+ if (quantifier != null && (quantifier.BoundVars.Count > 0) && !quantifiers.Contains(quantifier)) {
+ quantifiers.Add(quantifier);
+ if (quantifier.SplitQuantifier != null) {
+ var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null);
+ quantifierCollections.Add(new QuantifiersCollection(collection, reporter));
+ quantifiers.UnionWith(quantifier.SplitQuantifier);
+ } else {
+ quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter));
+ }
+ }
+
+ if (expr is OldExpr) {
+ inOldContext = true;
+ } else if (inOldContext) { // FIXME be more restrctive on the type of stuff that we annotate
+ exprsInOldContext.Add(expr);
+ }
+
+ return true;
+ }
+
+ protected override bool VisitOneStmt(Statement stmt, ref bool st) {
+ if (stmt is ForallStmt) {
+ ForallStmt s = (ForallStmt)stmt;
+ if (s.ForallExpressions != null) {
+ foreach (Expression expr in s.ForallExpressions) {
+ VisitOneExpr(expr, ref st);
+ }
+ }
+ }
+ return true;
+ }
+ }
+}
diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs
new file mode 100644
index 00000000..d4a822a8
--- /dev/null
+++ b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -0,0 +1,509 @@
+#define THROW_UNSUPPORTED_COMPARISONS
+
+using Microsoft.Dafny;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using System.Text;
+
+namespace Microsoft.Dafny.Triggers {
+ internal static class DeduplicateExtension {
+ public static List<T> Deduplicate<T>(this IEnumerable<T> seq, Func<T, T, bool> eq) {
+ List<T> deduplicated = new List<T>();
+
+ foreach (var elem in seq) {
+ if (!deduplicated.Any(other => eq(elem, other))) {
+ deduplicated.Add(elem);
+ }
+ }
+
+ return deduplicated;
+ }
+ }
+
+ internal struct TriggerMatch {
+ internal Expression Expr;
+ internal Expression OriginalExpr;
+ internal Dictionary<IVariable, Expression> Bindings;
+
+ internal static bool Eq(TriggerMatch t1, TriggerMatch t2) {
+ return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr);
+ }
+
+ /// <summary>
+ /// 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.
+ /// </summary>
+ internal bool CouldCauseLoops(List<TriggerTerm> terms, ISet<BoundVar> boundVars) {
+ var expr = Expr;
+ return !terms.Any(term => term.Expr.ExpressionEqModuloExpressionsNotInvolvingBoundVariables(expr, boundVars));
+ }
+ }
+
+ internal static class ExprExtensions {
+ internal static IEnumerable<Expression> AllSubExpressions(this Expression expr, bool wrapOld, bool strict) {
+ bool isOld = expr is OldExpr;
+
+ foreach (var subexpr in expr.SubExpressions) {
+ foreach (var r_subexpr in AllSubExpressions(subexpr, wrapOld, false)) {
+ yield return TriggerUtils.MaybeWrapInOld(r_subexpr, isOld);
+ }
+ }
+
+ if (expr is StmtExpr) {
+ foreach (var r_subexpr in AllSubExpressions(((StmtExpr)expr).S, wrapOld, false)) {
+ yield return TriggerUtils.MaybeWrapInOld(r_subexpr, isOld);
+ }
+ }
+
+ if (!strict) {
+ yield return expr;
+ }
+ }
+
+ internal static IEnumerable<Expression> AllSubExpressions(this Statement stmt, bool wrapOld, bool strict) {
+ foreach (var subexpr in stmt.SubExpressions) {
+ foreach (var r_subexpr in AllSubExpressions(subexpr, wrapOld, false)) {
+ yield return r_subexpr;
+ }
+ }
+
+ foreach (var substmt in stmt.SubStatements) {
+ foreach (var r_subexpr in AllSubExpressions(substmt, wrapOld, false)) {
+ yield return r_subexpr;
+ }
+ }
+ }
+
+ 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));
+ }
+
+ internal static bool ExpressionEqModuloExpressionsNotInvolvingBoundVariables(this Expression expr1, Expression expr2, ISet<BoundVar> boundVars) {
+ expr1 = expr1.Resolved;
+ expr2 = expr2.Resolved;
+
+ if (expr1 is IdentifierExpr) {
+ if (expr2 is IdentifierExpr) {
+ return true;
+ } else {
+ var freeInE2 = Translator.ComputeFreeVariables(expr2);
+ freeInE2.IntersectWith(boundVars);
+ return !freeInE2.Any();
+ }
+ }
+
+ return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions,
+ expr2.SubExpressions, (e1, e2) => ExpressionEqModuloExpressionsNotInvolvingBoundVariables(e1, e2, boundVars));
+ }
+
+ internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet<BoundVar> holes, Dictionary<IVariable, Expression> bindings) {
+ expr = expr.Resolved;
+ trigger = trigger.Resolved;
+
+ if (trigger is IdentifierExpr) {
+ var var = ((IdentifierExpr)trigger).Var;
+
+ if (holes.Contains(var)) {
+ Expression existing_binding = null;
+ if (bindings.TryGetValue(var, out existing_binding)) {
+ return ExpressionEq(expr, existing_binding);
+ } else {
+ bindings[var] = expr;
+ return true;
+ }
+ }
+ }
+
+ return ShallowEq_Top(expr, trigger) && TriggerUtils.SameLists(expr.SubExpressions, trigger.SubExpressions, (e1, e2) => MatchesTrigger(e1, e2, holes, bindings));
+ }
+
+ private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, IEnumerable<BoundVar> holes, Expression originalExpr) {
+ var bindings = new Dictionary<IVariable, Expression>();
+ if (expr.MatchesTrigger(trigger, new HashSet<BoundVar>(holes), bindings)) {
+ return new TriggerMatch { Expr = expr, OriginalExpr = originalExpr ?? expr, Bindings = bindings };
+ } else {
+ return null;
+ }
+ }
+
+ internal static IEnumerable<TriggerMatch> SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) {
+ return quantifier.AllSubExpressions(true, true)
+ .Select(e => TriggerUtils.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);
+ }
+
+ private static bool ShallowSameSingleAttribute(Attributes arg1, Attributes arg2) {
+ return arg1.Name == arg2.Name;
+ }
+
+ private static bool SameBoundVar(IVariable arg1, IVariable arg2) {
+ return arg1 == arg2 ||
+ (arg1.Name == arg2.Name &&
+ arg1.CompileName == arg2.CompileName &&
+ arg1.DisplayName == arg2.DisplayName &&
+ arg1.UniqueName == arg2.UniqueName &&
+ arg1.IsGhost == arg2.IsGhost &&
+ arg1.IsMutable == arg2.IsMutable &&
+ ((arg1.Type == null && arg2.Type == null) || arg1.Type.Equals(arg2.Type)));
+ }
+
+ /// <summary>
+ /// Compares two abstract syntax expressions, looking only at their direct members. Subexpressions and substatements are not compared.
+ /// </summary>
+ /// <returns></returns>
+ internal static bool ShallowEq_Top(Expression expr1, Expression expr2) {
+ Contract.Requires(expr1 != null);
+ Contract.Requires(expr2 != null);
+
+ // We never compare concrete expressions
+ Contract.Requires(!(expr1 is ConcreteSyntaxExpression));
+ Contract.Requires(!(expr2 is ConcreteSyntaxExpression));
+
+ // CPC: Hey future editor: the following block of code is auto-generated. Just add your own cases at the end.
+ // This could be a visitor pattern, except I need to visit a pair of nodes.
+ // It could also be implemented in each individual class. I'd have a slight preference for that.
+ // This really just wants to use double dispatch.
+ if (expr1 is UnboxingCastExpr && expr2 is UnboxingCastExpr) {
+ return ShallowEq((UnboxingCastExpr)expr1, (UnboxingCastExpr)expr2);
+ } else if (expr1 is BoxingCastExpr && expr2 is BoxingCastExpr) {
+ return ShallowEq((BoxingCastExpr)expr1, (BoxingCastExpr)expr2);
+ } else if (expr1 is MatchExpr && expr2 is MatchExpr) {
+ return ShallowEq((MatchExpr)expr1, (MatchExpr)expr2);
+ } else if (expr1 is ITEExpr && expr2 is ITEExpr) {
+ return ShallowEq((ITEExpr)expr1, (ITEExpr)expr2);
+ } else if (expr1 is StmtExpr && expr2 is StmtExpr) {
+ return ShallowEq((StmtExpr)expr1, (StmtExpr)expr2);
+ } else if (expr1 is WildcardExpr && expr2 is WildcardExpr) {
+ return ShallowEq((WildcardExpr)expr1, (WildcardExpr)expr2);
+ } else if (expr1 is ComprehensionExpr && expr2 is ComprehensionExpr) {
+ return ShallowEq((ComprehensionExpr)expr1, (ComprehensionExpr)expr2);
+ } else if (expr1 is NamedExpr && expr2 is NamedExpr) {
+ return ShallowEq((NamedExpr)expr1, (NamedExpr)expr2);
+ } else if (expr1 is LetExpr && expr2 is LetExpr) {
+ return ShallowEq((LetExpr)expr1, (LetExpr)expr2);
+ } else if (expr1 is TernaryExpr && expr2 is TernaryExpr) {
+ return ShallowEq((TernaryExpr)expr1, (TernaryExpr)expr2);
+ } else if (expr1 is BinaryExpr && expr2 is BinaryExpr) {
+ return ShallowEq((BinaryExpr)expr1, (BinaryExpr)expr2);
+ } else if (expr1 is UnaryExpr && expr2 is UnaryExpr) {
+ return ShallowEq((UnaryExpr)expr1, (UnaryExpr)expr2);
+ } else if (expr1 is MultiSetFormingExpr && expr2 is MultiSetFormingExpr) {
+ return ShallowEq((MultiSetFormingExpr)expr1, (MultiSetFormingExpr)expr2);
+ } else if (expr1 is OldExpr && expr2 is OldExpr) {
+ return ShallowEq((OldExpr)expr1, (OldExpr)expr2);
+ } else if (expr1 is FunctionCallExpr && expr2 is FunctionCallExpr) {
+ return ShallowEq((FunctionCallExpr)expr1, (FunctionCallExpr)expr2);
+ } else if (expr1 is ApplyExpr && expr2 is ApplyExpr) {
+ return ShallowEq((ApplyExpr)expr1, (ApplyExpr)expr2);
+ } else if (expr1 is SeqUpdateExpr && expr2 is SeqUpdateExpr) {
+ return ShallowEq((SeqUpdateExpr)expr1, (SeqUpdateExpr)expr2);
+ } else if (expr1 is MultiSelectExpr && expr2 is MultiSelectExpr) {
+ return ShallowEq((MultiSelectExpr)expr1, (MultiSelectExpr)expr2);
+ } else if (expr1 is SeqSelectExpr && expr2 is SeqSelectExpr) {
+ return ShallowEq((SeqSelectExpr)expr1, (SeqSelectExpr)expr2);
+ } else if (expr1 is MemberSelectExpr && expr2 is MemberSelectExpr) {
+ return ShallowEq((MemberSelectExpr)expr1, (MemberSelectExpr)expr2);
+ } else if (expr1 is MapDisplayExpr && expr2 is MapDisplayExpr) { //Note: MapDisplayExpr is not a DisplayExpression
+ return ShallowEq((MapDisplayExpr)expr1, (MapDisplayExpr)expr2);
+ } else if (expr1 is DisplayExpression && expr2 is DisplayExpression) {
+ return ShallowEq((DisplayExpression)expr1, (DisplayExpression)expr2);
+ } else if (expr1 is IdentifierExpr && expr2 is IdentifierExpr) {
+ return ShallowEq((IdentifierExpr)expr1, (IdentifierExpr)expr2);
+ } else if (expr1 is ThisExpr && expr2 is ThisExpr) {
+ return ShallowEq((ThisExpr)expr1, (ThisExpr)expr2);
+ } else if (expr1 is DatatypeValue && expr2 is DatatypeValue) {
+ return ShallowEq((DatatypeValue)expr1, (DatatypeValue)expr2);
+ } else if (expr1 is LiteralExpr && expr2 is LiteralExpr) {
+ return ShallowEq((LiteralExpr)expr1, (LiteralExpr)expr2);
+ } else {
+ // If this assertion fail, then a new abstract AST node was probably introduced but not registered here.
+ Contract.Assert(expr1.GetType() != expr2.GetType());
+ return false;
+ }
+ }
+
+ private static bool ShallowEq(UnboxingCastExpr expr1, UnboxingCastExpr expr2) {
+ Contract.Requires(false);
+ throw new InvalidOperationException();
+ }
+
+ private static bool ShallowEq(BoxingCastExpr expr1, BoxingCastExpr expr2) {
+ return expr1.FromType == expr2.FromType &&
+ expr1.ToType == expr2.ToType;
+ }
+
+ private static bool ShallowEq(MatchExpr expr1, MatchExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(ITEExpr expr1, ITEExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(StmtExpr expr1, StmtExpr expr2) {
+#if THROW_UNSUPPORTED_COMPARISONS
+ Contract.Assume(false); // This kind of expression never appears in a trigger
+ throw new NotImplementedException();
+#else
+ return expr1.S == expr2.S;
+#endif
+ }
+
+ private static bool ShallowEq(WildcardExpr expr1, WildcardExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(LambdaExpr expr1, LambdaExpr expr2) {
+#if THROW_UNSUPPORTED_COMPARISONS
+ Contract.Assume(false); // This kind of expression never appears in a trigger
+ throw new NotImplementedException();
+#else
+ return false;
+#endif
+ }
+
+ private static bool ShallowEq(MapComprehension expr1, MapComprehension expr2) {
+ return expr1.Finite == expr2.Finite;
+ }
+
+ private static bool ShallowEq(SetComprehension expr1, SetComprehension expr2) {
+ return expr1.TermIsImplicit == expr2.TermIsImplicit && //TODO
+ expr1.Finite == expr2.Finite;
+ }
+
+ private static bool ShallowEq(ExistsExpr expr1, ExistsExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(ForallExpr expr1, ForallExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(QuantifierExpr expr1, QuantifierExpr expr2) {
+ if (!TriggerUtils.SameNullity(expr1.SplitQuantifier, expr2.SplitQuantifier)) {
+ return false;
+ }
+
+ if (expr1.SplitQuantifier != null && expr2.SplitQuantifier != null) {
+ return ShallowEq_Top(expr1.SplitQuantifierExpression, expr2.SplitQuantifierExpression);
+ }
+
+ if (expr1.TypeArgs.Count != expr2.TypeArgs.Count ||
+ !TriggerUtils.SameNullity(expr1.Range, expr2.Range)) {
+ return false;
+ }
+
+ if (expr1 is ExistsExpr && expr2 is ExistsExpr) {
+ return ShallowEq((ExistsExpr)expr1, (ExistsExpr)expr2);
+ } else if (expr1 is ForallExpr && expr2 is ForallExpr) {
+ return ShallowEq((ForallExpr)expr1, (ForallExpr)expr2);
+ } else {
+ return false;
+ }
+ }
+
+ private static bool ShallowEq(ComprehensionExpr expr1, ComprehensionExpr expr2) {
+ if (!TriggerUtils.SameLists(expr1.BoundVars, expr2.BoundVars, SameBoundVar) ||
+ !ShallowSameAttributes(expr1.Attributes, expr2.Attributes) ||
+ // Filled in during resolution: !SameLists(expr1.Bounds, expr2.Bounds, ReferenceCompare) ||
+ // !SameLists(expr1.MissingBounds, expr2.MissingBounds, SameBoundVar) ||
+ !TriggerUtils.SameNullity(expr1.Range, expr2.Range)) { //TODO Check
+ return false;
+ }
+
+ if (expr1 is LambdaExpr && expr2 is LambdaExpr) {
+ return ShallowEq((LambdaExpr)expr1, (LambdaExpr)expr2);
+ } else if (expr1 is MapComprehension && expr2 is MapComprehension) {
+ return ShallowEq((MapComprehension)expr1, (MapComprehension)expr2);
+ } else if (expr1 is SetComprehension && expr2 is SetComprehension) {
+ return ShallowEq((SetComprehension)expr1, (SetComprehension)expr2);
+ } else if (expr1 is QuantifierExpr && expr2 is QuantifierExpr) {
+ return ShallowEq((QuantifierExpr)expr1, (QuantifierExpr)expr2);
+ } else {
+ return false; // ComprehensionExpr is abstract
+ }
+ }
+
+ private static bool ShallowEq(NamedExpr expr1, NamedExpr expr2) {
+ return expr1.Name == expr2.Name &&
+ TriggerUtils.SameNullity(expr1.Contract, expr2.Contract);
+ }
+
+ private static bool ShallowEq(LetExpr expr1, LetExpr expr2) {
+ return expr1.Exact == expr2.Exact &&
+ ShallowSameAttributes(expr1.Attributes, expr2.Attributes);
+ }
+
+ private static bool ShallowEq(TernaryExpr expr1, TernaryExpr expr2) {
+ return expr1.Op == expr2.Op;
+ }
+
+ private static bool ShallowEq(BinaryExpr expr1, BinaryExpr expr2) {
+ Contract.Requires(expr1.ResolvedOp != BinaryExpr.ResolvedOpcode.YetUndetermined);
+ Contract.Requires(expr2.ResolvedOp != BinaryExpr.ResolvedOpcode.YetUndetermined);
+ return expr1.ResolvedOp == expr2.ResolvedOp;
+ }
+
+ private static bool ShallowEq(ConversionExpr expr1, ConversionExpr expr2) {
+ return expr1.Type == expr2.Type; //TODO equality on types?
+ }
+
+ private static bool ShallowEq(UnaryOpExpr expr1, UnaryOpExpr expr2) {
+ return expr1.Op == expr2.Op;
+ }
+
+ private static bool ShallowEq(UnaryExpr expr1, UnaryExpr expr2) {
+ if (expr1 is ConversionExpr && expr2 is ConversionExpr) {
+ return ShallowEq((ConversionExpr)expr1, (ConversionExpr)expr2);
+ } else if (expr1 is UnaryOpExpr && expr2 is UnaryOpExpr) {
+ return ShallowEq((UnaryOpExpr)expr1, (UnaryOpExpr)expr2);
+ } else {
+ return false; // UnaryExpr is abstract
+ }
+ }
+
+ private static bool ShallowEq(MultiSetFormingExpr expr1, MultiSetFormingExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(OldExpr expr1, OldExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(FunctionCallExpr expr1, FunctionCallExpr expr2) {
+ return expr1.Name == expr2.Name &&
+ expr1.CoCall == expr2.CoCall && //TODO
+ expr1.Function == expr2.Function; // TODO TypeArgumentSubstitutions?
+ }
+
+ private static bool ShallowEq(ApplyExpr expr1, ApplyExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(SeqUpdateExpr expr1, SeqUpdateExpr expr2) {
+ Contract.Requires(expr1.ResolvedUpdateExpr != null && expr2.ResolvedUpdateExpr != null);
+ return true;
+ }
+
+ private static bool ShallowEq(MultiSelectExpr expr1, MultiSelectExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(SeqSelectExpr expr1, SeqSelectExpr expr2) {
+ return expr1.SelectOne == expr2.SelectOne &&
+ TriggerUtils.SameNullity(expr1.Seq, expr2.Seq) &&
+ TriggerUtils.SameNullity(expr1.E0, expr2.E0) &&
+ TriggerUtils.SameNullity(expr1.E1, expr2.E1);
+ }
+
+ private static bool ShallowEq(MemberSelectExpr expr1, MemberSelectExpr expr2) {
+ return expr1.MemberName == expr2.MemberName &&
+ expr1.Member == expr2.Member &&
+ TriggerUtils.SameLists(expr1.TypeApplication, expr2.TypeApplication, Microsoft.Dafny.Type.Equals);
+ }
+
+ private static bool ShallowEq(SeqDisplayExpr expr1, SeqDisplayExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(MapDisplayExpr expr1, MapDisplayExpr expr2) {
+ return expr1.Finite == expr2.Finite;
+ }
+
+ private static bool ShallowEq(MultiSetDisplayExpr expr1, MultiSetDisplayExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(SetDisplayExpr expr1, SetDisplayExpr expr2) {
+ return expr1.Finite == expr2.Finite;
+ }
+
+ private static bool ShallowEq(DisplayExpression expr1, DisplayExpression expr2) {
+ if (expr1 is SeqDisplayExpr && expr2 is SeqDisplayExpr) {
+ return ShallowEq((SeqDisplayExpr)expr1, (SeqDisplayExpr)expr2);
+ } else if (expr1 is MultiSetDisplayExpr && expr2 is MultiSetDisplayExpr) {
+ return ShallowEq((MultiSetDisplayExpr)expr1, (MultiSetDisplayExpr)expr2);
+ } else if (expr1 is SetDisplayExpr && expr2 is SetDisplayExpr) {
+ return ShallowEq((SetDisplayExpr)expr1, (SetDisplayExpr)expr2);
+ } else {
+ return false;
+ }
+ }
+
+ private static bool ShallowEq(AutoGhostIdentifierExpr expr1, AutoGhostIdentifierExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(IdentifierExpr expr1, IdentifierExpr expr2) {
+ if (expr1.Name != expr2.Name ||
+ expr1.Var != expr2.Var) {
+ return false;
+ }
+
+ if (expr1 is AutoGhostIdentifierExpr && expr2 is AutoGhostIdentifierExpr) {
+ return ShallowEq((AutoGhostIdentifierExpr)expr1, (AutoGhostIdentifierExpr)expr2);
+ } else {
+ return true;
+ }
+ }
+
+ private static bool ShallowEq(ImplicitThisExpr expr1, ImplicitThisExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(ThisExpr expr1, ThisExpr expr2) {
+ if (expr1 is ImplicitThisExpr && expr2 is ImplicitThisExpr) {
+ return ShallowEq((ImplicitThisExpr)expr1, (ImplicitThisExpr)expr2);
+ } else {
+ return (expr1.GetType() == expr2.GetType()); // LiteralExpr is not abstract
+ }
+ }
+
+ private static bool ShallowEq(DatatypeValue expr1, DatatypeValue expr2) {
+ 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, Microsoft.Dafny.Type.Equals);
+ }
+
+ private static bool ShallowEq(StringLiteralExpr expr1, StringLiteralExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(CharLiteralExpr expr1, CharLiteralExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(StaticReceiverExpr expr1, StaticReceiverExpr expr2) {
+ return true;
+ }
+
+ private static bool ShallowEq(LiteralExpr expr1, LiteralExpr expr2) {
+ if (!TriggerUtils.SameNullity(expr1.Value, expr2.Value) || (expr1.Value != null && !expr1.Value.Equals(expr2.Value))) {
+ return false;
+ }
+
+ if (expr1 is StringLiteralExpr && expr2 is StringLiteralExpr) {
+ return ShallowEq((StringLiteralExpr)expr1, (StringLiteralExpr)expr2);
+ } else if (expr1 is CharLiteralExpr && expr2 is CharLiteralExpr) {
+ return ShallowEq((CharLiteralExpr)expr1, (CharLiteralExpr)expr2);
+ } else if (expr1 is StaticReceiverExpr && expr2 is StaticReceiverExpr) {
+ return ShallowEq((StaticReceiverExpr)expr1, (StaticReceiverExpr)expr2);
+ } else {
+ return (expr1.GetType() == expr2.GetType()); // LiteralExpr is not abstract
+ }
+ }
+ }
+}
diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
new file mode 100644
index 00000000..c16a3e44
--- /dev/null
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -0,0 +1,265 @@
+#define DEBUG_AUTO_TRIGGERS
+
+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<T> CopyAndAdd<T>(List<T> seq, T elem) {
+ var copy = new List<T>(seq);
+ copy.Add(elem);
+ return copy;
+ }
+
+ internal class SetOfTerms {
+ internal bool IsRedundant { get; private set; }
+ internal List<TriggerTerm> Terms { get; set; }
+
+ private ISet<BoundVar> variables;
+ private Dictionary<BoundVar, TriggerTerm> termOwningAUniqueVar;
+ private Dictionary<TriggerTerm, ISet<BoundVar>> 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<TriggerTerm>();
+ newSet.variables = new HashSet<BoundVar>();
+ newSet.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>();
+ newSet.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>();
+ return newSet;
+ }
+
+ /// <summary>
+ /// 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).
+ /// </summary>
+ internal SetOfTerms CopyWithAdd(TriggerTerm term, ISet<BoundVar> relevantVariables) {
+ var copy = new SetOfTerms();
+ copy.Terms = new List<TriggerTerm>(Terms);
+ copy.variables = new HashSet<BoundVar>(variables);
+ copy.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>(termOwningAUniqueVar);
+ copy.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>(uniqueVarsOwnedByATerm);
+
+ copy.Terms.Add(term);
+
+ var varsInNewTerm = new HashSet<BoundVar>(term.BoundVars);
+ varsInNewTerm.IntersectWith(relevantVariables);
+
+ var ownedByNewTerm = new HashSet<BoundVar>();
+
+ // 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) {
+ TriggerTerm originalOwner;
+ if (copy.termOwningAUniqueVar.TryGetValue(v, out 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<SetOfTerms> AllSubsets(IList<TriggerTerm> source, Func<SetOfTerms, TriggerTerm, bool> predicate, int offset, ISet<BoundVar> 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<SetOfTerms> AllNonEmptySubsets(IList<TriggerTerm> source, Func<SetOfTerms, TriggerTerm, bool> predicate, IEnumerable<BoundVar> relevantVariables) {
+ foreach (var subset in AllSubsets(source, predicate, 0, new HashSet<BoundVar>(relevantVariables))) {
+ if (subset.Count > 0) {
+ yield return subset;
+ }
+ }
+ }
+
+ internal static List<T> MergeAlterFirst<T>(List<T> a, List<T> b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ a.AddRange(b);
+ return a;
+ }
+
+ internal static ISet<T> MergeAlterFirst<T>(ISet<T> a, ISet<T> b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ a.UnionWith(b);
+ return a;
+ }
+
+ internal static bool SameLists<T>(IEnumerable<T> list1, IEnumerable<T> list2, Func<T, T, bool> 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<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 elem in elements) {
+ var conv = Converter(elem);
+ if (predicate(elem, conv)) {
+ yield return elem;
+ } else {
+ reject(elem, conv);
+ }
+ }
+ }
+
+ internal static bool SameNullity<T>(T x1, T x2) where T : class {
+ return (x1 == null) == (x2 == null);
+ }
+
+ internal string JoinStringsWithHeader(string header, IEnumerable<string> lines) {
+ return header + String.Join(Environment.NewLine + new String(' ', header.Length), lines);
+ }
+
+ [Conditional("DEBUG_AUTO_TRIGGERS")]
+ internal static void DebugTriggers(string format, params object[] more) {
+ Console.Error.WriteLine(format, more);
+ }
+
+ internal static bool AllowsMatchingLoops(QuantifierExpr quantifier) {
+ Contract.Requires(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(QuantifierExpr quantifier) {
+ Contract.Requires(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(QuantifierExpr quantifier) {
+ Contract.Requires(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 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 static Expression PrepareExprForInclusionInTrigger(Expression expr, out bool isKiller) {
+ isKiller = false;
+
+ var ret = expr;
+ if (ret is BinaryExpr) {
+ ret = PrepareInMultisetForInclusionInTrigger(PrepareNotInForInclusionInTrigger((BinaryExpr)ret), ref isKiller);
+ }
+
+ return ret;
+ }
+
+ private static BinaryExpr PrepareNotInForInclusionInTrigger(BinaryExpr bexpr) {
+ if (bexpr.Op == BinaryExpr.Opcode.NotIn) {
+ var new_expr = new BinaryExpr(bexpr.tok, BinaryExpr.Opcode.In, bexpr.E0, bexpr.E1);
+ new_expr.ResolvedOp = RemoveNotInBinaryExprIn(bexpr.ResolvedOp);
+ new_expr.Type = bexpr.Type;
+ return new_expr;
+ } else {
+ return bexpr;
+ }
+ }
+
+ private static Expression PrepareInMultisetForInclusionInTrigger(BinaryExpr bexpr, ref bool isKiller) {
+ if (bexpr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) {
+ var new_expr = new SeqSelectExpr(bexpr.tok, true, bexpr.E1, bexpr.E0, null);
+ new_expr.Type = bexpr.Type;
+ isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer
+ return new_expr;
+ } else {
+ return bexpr;
+ }
+ }
+
+ internal static Expression PrepareExprForInclusionInTrigger(Expression expr) {
+ bool _;
+ return PrepareExprForInclusionInTrigger(expr, out _);
+ }
+
+ internal static Expression MaybeWrapInOld(Expression expr, bool wrap) {
+ if (wrap && !(expr is NameSegment) && !(expr is IdentifierExpr)) {
+ var newExpr = new OldExpr(expr.tok, expr);
+ newExpr.Type = expr.Type;
+ return newExpr;
+ } else {
+ return expr;
+ }
+ }
+ }
+}
diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
new file mode 100644
index 00000000..4204cc29
--- /dev/null
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -0,0 +1,325 @@
+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<IVariable> Variables { get; set; }
+ internal IEnumerable<BoundVar> BoundVars {
+ get {
+ return Variables.Select(v => v as BoundVar).Where(v => v != null);
+ }
+ }
+
+ public override string ToString() {
+ return Printer.ExprToString(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 ExprExtensions.ExpressionEq(t1.Expr, t2.Expr);
+ }
+ }
+
+ class TriggerCandidate {
+ internal List<TriggerTerm> Terms { get; set; }
+ internal string Annotation { get; set; }
+
+ internal TriggerCandidate(List<TriggerTerm> terms) {
+ this.Terms = terms;
+ }
+
+ public TriggerCandidate(TriggerCandidate candidate) {
+ this.Terms = candidate.Terms;
+ }
+
+ internal bool MentionsAll(List<BoundVar> vars) {
+ return vars.All(x => Terms.Any(term => term.Variables.Contains(x)));
+ }
+
+ internal string Repr { get { return String.Join(", ", Terms); } }
+
+ public override string ToString() {
+ return "{" + Repr + "}" + (String.IsNullOrWhiteSpace(Annotation) ? "" : " (" + Annotation + ")");
+ }
+
+ internal IEnumerable<TriggerMatch> LoopingSubterms(QuantifierExpr quantifier) {
+ Contract.Requires(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<BoundVar>(quantifier.BoundVars);
+ return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms, boundVars));
+ }
+
+ internal List<TriggerMatch> MatchingSubterms(QuantifierExpr quantifier) {
+ Contract.Requires(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;
+ }
+ }
+
+ internal class TriggerAnnotation {
+ internal bool IsTriggerKiller;
+ internal ISet<IVariable> Variables;
+ internal readonly List<TriggerTerm> PrivateTerms;
+ internal readonly List<TriggerTerm> ExportedTerms;
+
+ internal TriggerAnnotation(bool IsTriggerKiller, IEnumerable<IVariable> Variables, IEnumerable<TriggerTerm> AllTerms, IEnumerable<TriggerTerm> PrivateTerms = null) {
+ this.IsTriggerKiller = IsTriggerKiller;
+ this.Variables = new HashSet<IVariable>(Variables);
+ this.PrivateTerms = new List<TriggerTerm>(PrivateTerms == null ? Enumerable.Empty<TriggerTerm>() : PrivateTerms);
+ this.ExportedTerms = new List<TriggerTerm>(AllTerms == null ? Enumerable.Empty<TriggerTerm>() : 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();
+ }
+ }
+
+ internal class TriggerAnnotationsCache {
+ public readonly HashSet<Expression> exprsInOldContext;
+ public readonly Dictionary<Expression, TriggerAnnotation> annotations;
+
+ /// <summary>
+ /// For certain operations, the TriggersCollector class needs to know whether
+ /// an particular expression is under an old(...) wrapper. This is in particular
+ /// true for generating trigger terms (but it is not for checking wehter something
+ /// is a trigger killer, so passing an empty set here for that case would be fine.
+ /// </summary>
+ public TriggerAnnotationsCache(HashSet<Expression> exprsInOldContext) {
+ this.exprsInOldContext = exprsInOldContext;
+ annotations = new Dictionary<Expression, TriggerAnnotation>();
+ }
+ }
+
+ internal class TriggersCollector {
+ TriggerAnnotationsCache cache;
+
+ internal TriggersCollector(HashSet<Expression> exprsInOldContext) {
+ this.cache = new TriggerAnnotationsCache(exprsInOldContext);
+ }
+
+ private T ReduceAnnotatedSubExpressions<T>(Expression expr, T seed, Func<TriggerAnnotation, T> map, Func<T, T, T> reduce) {
+ return expr.SubExpressions.Select(e => map(Annotate(e)))
+ .Aggregate(seed, (acc, e) => reduce(acc, e));
+ }
+
+ private List<TriggerTerm> CollectExportedCandidates(Expression expr) {
+ return ReduceAnnotatedSubExpressions<List<TriggerTerm>>(expr, new List<TriggerTerm>(), a => a.ExportedTerms, TriggerUtils.MergeAlterFirst);
+ }
+
+ private ISet<IVariable> CollectVariables(Expression expr) {
+ return ReduceAnnotatedSubExpressions(expr, new HashSet<IVariable>(), a => a.Variables, TriggerUtils.MergeAlterFirst);
+ }
+
+ private bool CollectIsKiller(Expression expr) {
+ return ReduceAnnotatedSubExpressions(expr, false, a => a.IsTriggerKiller, (a, b) => a || b);
+ }
+
+ private IEnumerable<TriggerTerm> OnlyPrivateCandidates(List<TriggerTerm> terms, IEnumerable<IVariable> privateVars) {
+ return terms.Where(c => privateVars.Intersect(c.Variables).Any()); //TODO Check perf
+ }
+
+ private TriggerAnnotation Annotate(Expression expr) {
+ TriggerAnnotation cached;
+ if (cache.annotations.TryGetValue(expr, out cached)) {
+ return cached;
+ }
+
+ expr.SubExpressions.Iter(e => Annotate(e));
+
+ TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort
+ if (expr is FunctionCallExpr ||
+ expr is SeqSelectExpr ||
+ expr is MultiSelectExpr ||
+ expr is MemberSelectExpr ||
+ expr is OldExpr ||
+ expr is ApplyExpr ||
+ expr is DisplayExpression ||
+ TranslateToFunctionCall(expr) ||
+ (expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944
+ (expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) {
+ 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 ComprehensionExpr) {
+ annotation = AnnotateComprehensionExpr((ComprehensionExpr)expr);
+ } else if (expr is ConcreteSyntaxExpression ||
+ expr is LiteralExpr ||
+ expr is OldExpr ||
+ expr is ThisExpr ||
+ expr is BoxingCastExpr ||
+ expr is DatatypeValue) {
+ annotation = AnnotateOther(expr, false);
+ } else {
+ annotation = AnnotateOther(expr, true);
+ }
+
+ TriggerUtils.DebugTriggers("{0} ({1})\n{2}", Printer.ExprToString(expr), expr.GetType(), annotation);
+ cache.annotations[expr] = annotation;
+ return annotation;
+ }
+
+ // 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.NumericPersuation.Real);
+ 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:
+ case BinaryExpr.ResolvedOpcode.Mul:
+ case BinaryExpr.ResolvedOpcode.Div:
+ case BinaryExpr.ResolvedOpcode.Mod:
+ if (!isReal && DafnyOptions.O.DisableNLarith) {
+ return true;
+ }
+ break;
+ }
+ return false;
+ }
+ private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) {
+ bool expr_is_killer = false;
+ var new_expr = TriggerUtils.MaybeWrapInOld(TriggerUtils.PrepareExprForInclusionInTrigger(expr, out expr_is_killer), cache.exprsInOldContext.Contains(expr));
+ var new_term = new TriggerTerm { Expr = new_expr, OriginalExpr = expr, Variables = CollectVariables(expr) };
+
+ List<TriggerTerm> collected_terms = CollectExportedCandidates(expr);
+ var 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);
+ }
+
+ // 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 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 AnnotateQuantifierOrLetExpr(Expression expr, IEnumerable<BoundVar> boundVars) {
+ var terms = CollectExportedCandidates(expr);
+ return new TriggerAnnotation(true, CollectVariables(expr), terms, OnlyPrivateCandidates(terms, boundVars));
+ }
+
+ private TriggerAnnotation AnnotateQuantifier(QuantifierExpr expr) {
+ return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars);
+ }
+
+ private TriggerAnnotation AnnotateLetExpr(LetExpr expr) {
+ return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars);
+ }
+
+ private TriggerAnnotation AnnotateIdentifier(IdentifierExpr expr) {
+ return new TriggerAnnotation(false, Enumerable.Repeat(expr.Var, 1), null);
+ }
+
+ private TriggerAnnotation AnnotateComprehensionExpr(ComprehensionExpr expr) {
+ var terms = CollectExportedCandidates(expr);
+ return new TriggerAnnotation(true, CollectVariables(expr), terms, OnlyPrivateCandidates(terms, expr.BoundVars));
+ }
+
+ private TriggerAnnotation AnnotateOther(Expression expr, bool isTriggerKiller) {
+ return new TriggerAnnotation(isTriggerKiller || CollectIsKiller(expr), CollectVariables(expr), CollectExportedCandidates(expr));
+ }
+
+ /// <summary>
+ /// Collect terms in the body of the subexpressions of the argument that look like quantifiers. The results of this function can contain duplicate terms.
+ /// </summary>
+ internal List<TriggerTerm> CollectTriggers(QuantifierExpr quantifier) {
+ Contract.Requires(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;
+ }
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 12:56:25 +0000