1 files changed, 325 insertions, 0 deletions
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;
+    }
+  }
+}