Small cleanups, fixes, and refactorings

In particular, start detecting loops between terms that don't look like each
other at the Dafny level, such as {a[x]} and {x in a} (when a is a multiset)

7 files changed, 81 insertions, 64 deletions

diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index 5a824c36..13a1e53e 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -147,7 +147,7 @@
     <Compile Include="Triggers\QuantifiersCollection.cs" />

     <Compile Include="Triggers\QuantifierSplitter.cs" />

     <Compile Include="Triggers\TriggerExtensions.cs" />

-    <Compile Include="Triggers\TriggerGenerator.cs" />

+    <Compile Include="Triggers\QuantifiersCollector.cs" />

     <Compile Include="Triggers\TriggersCollector.cs" />

     <Compile Include="Triggers\TriggerUtils.cs" />

     <Compile Include="Util.cs" />

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 2c00e203..b6409b96 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -44,7 +44,7 @@ namespace Microsoft.Dafny
     }

 

     internal override void PostCyclicityResolve(ModuleDefinition m) {

-      var finder = new Triggers.QuantifierCollectionsFinder(reporter);

+      var finder = new Triggers.QuantifierCollector(reporter);

         

       foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {

         if (decl is Function) {

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index cbc212d2..01bceeb7 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -17,7 +17,7 @@ namespace Microsoft.Dafny.Triggers {
     internal List<TriggerCandidate> Candidates;

     internal List<TriggerCandidate> RejectedCandidates;

 

-    internal bool AllowsLoops { get { return quantifier.Attributes.AsEnumerable().Any(a => a.Name == "loop"); } }

+    internal bool AllowsLoops { get { return TriggerUtils.AllowsMatchingLoops(quantifier); } }

     internal bool CouldSuppressLoops { get; set; }

 

     internal QuantifierWithTriggers(QuantifierExpr quantifier) {

@@ -65,8 +65,8 @@ namespace Microsoft.Dafny.Triggers {
       var multiPool = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate).Select(candidates => new TriggerCandidate(candidates)).ToList();

 

       foreach (var q in quantifiers) {

-        q.CandidateTerms = distinctPool;

-        q.Candidates = multiPool;

+        q.CandidateTerms = distinctPool; //Candidate terms are immutable: no copy needed

+        q.Candidates = multiPool.Select(candidate => new TriggerCandidate(candidate)).ToList();

       }

     }

 

@@ -116,7 +116,7 @@ namespace Microsoft.Dafny.Triggers {
           c => !loopingSubterms[c].Any(),

           c => {

             looping.Add(c);

-            c.Annotation = "loop with " + loopingSubterms[c].MapConcat(t => Printer.ExprToString(t.Expr), ", ");

+            c.Annotation = "loops with " + loopingSubterms[c].MapConcat(t => Printer.ExprToString(t.Expr), ", ");

           }).ToList();

 

         q.CouldSuppressLoops = safe.Count > 0;

diff --git a/Source/Dafny/Triggers/TriggerGenerator.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
index e218ad7b..a43aae7a 100644
--- a/Source/Dafny/Triggers/TriggerGenerator.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -7,11 +7,11 @@ using System.Collections.ObjectModel;
 using System.Diagnostics.Contracts;

 

 namespace Microsoft.Dafny.Triggers { //FIXME rename this file

-  internal class QuantifierCollectionsFinder : TopDownVisitor<object> {

+  internal class QuantifierCollector : TopDownVisitor<object> {

     readonly ErrorReporter reporter;

     internal List<QuantifiersCollection> quantifierCollections = new List<QuantifiersCollection>();

 

-    public QuantifierCollectionsFinder(ErrorReporter reporter) {

+    public QuantifierCollector(ErrorReporter reporter) {

       Contract.Requires(reporter != null);

       this.reporter = reporter;

     }

@@ -22,6 +22,7 @@ namespace Microsoft.Dafny.Triggers { //FIXME rename this file
         if (quantifier.SplitQuantifier != null) {

           var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null);

           quantifierCollections.Add(new QuantifiersCollection(collection, reporter));

+          return false;

         } else {

           quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter));

         }

diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs
index 9fbc8a8a..0a0ad547 100644
--- a/Source/Dafny/Triggers/TriggerExtensions.cs
+++ b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -110,14 +110,18 @@ namespace Microsoft.Dafny.Triggers {
       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, ISet<BoundVar> holes) {

+    private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, IEnumerable<BoundVar> holes) {

       var bindings = new Dictionary<IVariable, Expression>();

-      return expr.MatchesTrigger(trigger, holes, bindings) ? new TriggerMatch { Expr = expr, Bindings = bindings } : (TriggerMatch?)null;

+      if (expr.MatchesTrigger(trigger, new HashSet<BoundVar>(holes), bindings)) {

+        return new TriggerMatch { Expr = expr, Bindings = bindings };

+      } else {

+        return null;

+      }

     }

 

     internal static IEnumerable<TriggerMatch> SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) {

       return quantifier.Term.AllSubExpressions()

-        .Select(e => e.MatchAgainst(trigger, new HashSet<BoundVar>(quantifier.BoundVars)))

+        .Select(e => TriggerUtils.CleanupExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars))

         .Where(e => e.HasValue).Select(e => e.Value);

     }

 

@@ -136,7 +140,8 @@ namespace Microsoft.Dafny.Triggers {
               arg1.DisplayName == arg2.DisplayName &&

               arg1.UniqueName == arg2.UniqueName &&

               arg1.IsGhost == arg2.IsGhost &&

-              arg1.IsMutable == arg2.IsMutable); //FIXME compare types?

+              arg1.IsMutable == arg2.IsMutable &&

+              ((arg1.Type == null && arg2.Type == null) || arg1.Type.Equals(arg2.Type))); 

     }

 

     /// <summary>

@@ -271,7 +276,7 @@ namespace Microsoft.Dafny.Triggers {
       return true;

     }

 

-    private static bool ShallowEq(QuantifierExpr expr1, QuantifierExpr expr2) { //FIXME are these TypeArgs still useful?

+    private static bool ShallowEq(QuantifierExpr expr1, QuantifierExpr expr2) {

       if (!TriggerUtils.SameNullity(expr1.SplitQuantifier, expr2.SplitQuantifier)) {

         return false;

       }

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index 6c6eede2..9ebcf846 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -100,9 +100,63 @@ namespace Microsoft.Dafny.Triggers {
       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

+      return Attributes.Contains(quantifier.Attributes, "matchingloop");

+    }

+

     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 quantifier.Attributes.AsEnumerable().All(aa => aa.Name != "trigger" && aa.Name != "no_trigger");

+      bool wantsAutoTriggers = true;

+      return !Attributes.Contains(quantifier.Attributes, "trigger") && 

+        (!Attributes.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers);

+    }

+

+    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 CleanupExprForInclusionInTrigger(Expression expr, out bool isKiller) {

+      isKiller = false;

+

+      if (!(expr is BinaryExpr)) {

+        return expr;

+      }

+

+      var bexpr = expr as BinaryExpr;

+

+      BinaryExpr new_expr = bexpr;

+      if (bexpr.Op == BinaryExpr.Opcode.NotIn) {

+        new_expr = new BinaryExpr(bexpr.tok, BinaryExpr.Opcode.In, bexpr.E0, bexpr.E1);

+        new_expr.ResolvedOp = RemoveNotInBinaryExprIn(bexpr.ResolvedOp);

+        new_expr.Type = bexpr.Type;

+      }

+

+      Expression returned_expr = new_expr;

+      if (new_expr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) {

+        returned_expr = new SeqSelectExpr(new_expr.tok, true, new_expr.E1, new_expr.E0, null);

+        returned_expr.Type = bexpr.Type;

+        isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer

+      }

+

+      return returned_expr;

+    }

+

+    internal static Expression CleanupExprForInclusionInTrigger(Expression expr) {

+      bool _;

+      return CleanupExprForInclusionInTrigger(expr, out _);

     }

   }

 }

diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index 9f721d9a..221a4255 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -9,10 +9,11 @@ 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; }

 

     public override string ToString() {

-      return Printer.ExprToString(Expr);

+      return Printer.ExprToString(OriginalExpr);

     }

 

     internal static bool Eq(TriggerTerm t1, TriggerTerm t2) {

@@ -28,16 +29,15 @@ namespace Microsoft.Dafny.Triggers {
       this.Terms = terms;

     }

 

-    public TriggerCandidate(TriggerCandidate mc, string annotation) {

-      this.Terms = mc.Terms;

-      this.Annotation = annotation;

+    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)));

     }

 

-    private string Repr { get { return Terms.MapConcat(t => Printer.ExprToString(t.Expr), ", "); } }

+    private string Repr { get { return String.Join(", ", Terms); } }

 

     public override string ToString() {

       return "{" + Repr + "}" + (String.IsNullOrWhiteSpace(Annotation) ? "" : " (" + Annotation + ")");

@@ -51,7 +51,6 @@ namespace Microsoft.Dafny.Triggers {
 

     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

-      //FIXME this will miss rewritten expressions (CleanupExpr). Should introduce an OriginalExpr to compare against.

       return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq);

     }

 

@@ -166,52 +165,10 @@ namespace Microsoft.Dafny.Triggers {
       return annotation;

     }

 

-    private BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) {

-      switch (opcode) {

-        case BinaryExpr.ResolvedOpcode.NotInMap:

-          return BinaryExpr.ResolvedOpcode.InMap;

-        case BinaryExpr.ResolvedOpcode.NotInSet:

-          return BinaryExpr.ResolvedOpcode.InSet;

-        case BinaryExpr.ResolvedOpcode.NotInSeq:

-          return BinaryExpr.ResolvedOpcode.InSeq;

-        case BinaryExpr.ResolvedOpcode.NotInMultiSet:

-          return BinaryExpr.ResolvedOpcode.InMultiSet;

-      }

-

-      Contract.Assert(false);

-      throw new ArgumentException();

-    }

-

-    private Expression CleanupExpr(Expression expr, out bool isKiller) {

-      isKiller = false;

-

-      if (!(expr is BinaryExpr)) {

-        return expr;

-      }

-

-      var bexpr = expr as BinaryExpr;

-

-      BinaryExpr new_expr = bexpr;

-      if (bexpr.Op == BinaryExpr.Opcode.NotIn) {

-        new_expr = new BinaryExpr(bexpr.tok, BinaryExpr.Opcode.In, bexpr.E0, bexpr.E1);

-        new_expr.ResolvedOp = RemoveNotInBinaryExprIn(bexpr.ResolvedOp);

-        new_expr.Type = bexpr.Type;

-      }

-

-      Expression returned_expr = new_expr;

-      if (new_expr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) {

-        returned_expr = new SeqSelectExpr(new_expr.tok, true, new_expr.E1, new_expr.E0, null);

-        returned_expr.Type = bexpr.Type;

-        isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer

-      }

-

-      return returned_expr;

-    }

-

     private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) {

       bool expr_is_killer = false;

-      var new_expr = CleanupExpr(expr, out expr_is_killer);

-      var new_term = new TriggerTerm { Expr = new_expr, Variables = CollectVariables(expr) };

+      var new_expr = TriggerUtils.CleanupExprForInclusionInTrigger(expr, out expr_is_killer);

+      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);