Make `old` a special case for trigger generation.

Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and
old(f(x)). This has a number of implications; see the new tests files for more
information.

9 files changed, 178 insertions, 42 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 230d9349..557eee93 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -47,10 +47,10 @@ namespace Microsoft.Dafny
       var finder = new Triggers.QuantifierCollector(reporter);

         

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

-        finder.Visit(decl, null);

+        finder.Visit(decl, false);

       }

       

-      var triggersCollector = new Triggers.TriggersCollector();

+      var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext);

       foreach (var quantifierCollection in finder.quantifierCollections) {

         quantifierCollection.ComputeTriggers(triggersCollector);

         quantifierCollection.CommitTriggers();

diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
index b30cb6b1..3385f36e 100644
--- a/Source/Dafny/Triggers/QuantifiersCollector.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -6,18 +6,19 @@ using Microsoft.Boogie;
 using System.Collections.ObjectModel;

 using System.Diagnostics.Contracts;

 

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

-  internal class QuantifierCollector : TopDownVisitor<object> {

+namespace Microsoft.Dafny.Triggers {

+  internal class QuantifierCollector : TopDownVisitor<bool> {

     readonly ErrorReporter reporter;

-    private HashSet<Expression> quantifiers = new HashSet<Expression>();

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

+    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 object _) {

+    protected override bool VisitOneExpr(Expression expr, ref bool inOldContext) {

       var quantifier = expr as QuantifierExpr;

 

       if (quantifier != null && !quantifiers.Contains(quantifier)) {

@@ -31,6 +32,12 @@ namespace Microsoft.Dafny.Triggers { //FIXME rename this file
         }

       }

 

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

     }

   }

diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs
index 6c3f4ee7..02deb92f 100644
--- a/Source/Dafny/Triggers/TriggerExtensions.cs
+++ b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -38,17 +38,18 @@ namespace Microsoft.Dafny.Triggers {
   }

 

   internal static class ExprExtensions {

-    internal static IEnumerable<Expression> AllSubExpressions(this Expression expr, bool strict = false) {

+    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, false)) {

-          yield return r_subexpr;

+        foreach (var r_subexpr in AllSubExpressions(subexpr, wrapOld, false)) {

+          yield return TriggerUtils.MaybeWrapInOld(r_subexpr, isOld);

         }

-        yield return subexpr;

       }

 

       if (expr is StmtExpr) {

-        foreach (var r_subexpr in AllSubExpressions(((StmtExpr)expr).S, false)) {

-          yield return r_subexpr;

+        foreach (var r_subexpr in AllSubExpressions(((StmtExpr)expr).S, wrapOld, false)) {

+          yield return TriggerUtils.MaybeWrapInOld(r_subexpr, isOld);

         }

       }

 

@@ -57,16 +58,15 @@ namespace Microsoft.Dafny.Triggers {
       }

     }

 

-    internal static IEnumerable<Expression> AllSubExpressions(this Statement stmt, bool strict = false) {

+    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, false)) {

+        foreach (var r_subexpr in AllSubExpressions(subexpr, wrapOld, false)) {

           yield return r_subexpr;

         }

-        yield return subexpr;

       }

 

       foreach (var substmt in stmt.SubStatements) {

-        foreach (var r_subexpr in AllSubExpressions(substmt, false)) {

+        foreach (var r_subexpr in AllSubExpressions(substmt, wrapOld, false)) {

           yield return r_subexpr;

         }

       }

@@ -121,8 +121,8 @@ namespace Microsoft.Dafny.Triggers {
     }

 

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

-      return quantifier.Term.AllSubExpressions()

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

+      return quantifier.Term.AllSubExpressions(true, false) //FIXME should loop detection actually pass true here?

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

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

     }

 

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index 6f76464b..4fd139e2 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -129,35 +129,52 @@ namespace Microsoft.Dafny.Triggers {
       throw new ArgumentException();

     }

 

-    internal static Expression CleanupExprForInclusionInTrigger(Expression expr, out bool isKiller) {

+    internal static Expression PrepareExprForInclusionInTrigger(Expression expr, out bool isKiller) {

       isKiller = false;

 

-      if (!(expr is BinaryExpr)) {

-        return expr;

+      var ret = expr;

+      if (ret is BinaryExpr) {

+        ret = PrepareInMultisetForInclusionInTrigger(PrepareNotInForInclusionInTrigger((BinaryExpr)ret), ref isKiller);

       }

 

-      var bexpr = expr as BinaryExpr;

+      return ret;

+    }

 

-      BinaryExpr new_expr = bexpr;

+    private static BinaryExpr PrepareNotInForInclusionInTrigger(BinaryExpr bexpr) {

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

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

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

       }

+    }

 

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

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

       }

-

-      return returned_expr;

     }

 

-    internal static Expression CleanupExprForInclusionInTrigger(Expression expr) {

+    internal static Expression PrepareExprForInclusionInTrigger(Expression expr) {

       bool _;

-      return CleanupExprForInclusionInTrigger(expr, out _);

+      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
index 167a6a1b..11860404 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -27,7 +27,7 @@ namespace Microsoft.Dafny.Triggers {
     internal TermComparison CompareTo(TriggerTerm other) {

       if (this == other) {

         return TermComparison.SameStrength;

-      } else if (Expr.AllSubExpressions(true).Any(other.Expr.ExpressionEq)) {

+      } else if (Expr.AllSubExpressions(true, true).Any(other.Expr.ExpressionEq)) {

         return TermComparison.Stronger;

       } else {

         return TermComparison.NotStronger;

@@ -92,7 +92,7 @@ namespace Microsoft.Dafny.Triggers {
     }

   }

 

-  class TriggerAnnotation {

+  internal class TriggerAnnotation {

     internal bool IsTriggerKiller;

     internal ISet<IVariable> Variables;

     internal readonly List<TriggerTerm> PrivateTerms;

@@ -132,11 +132,27 @@ namespace Microsoft.Dafny.Triggers {
     }

   }

 

-  public class TriggersCollector {

-    Dictionary<Expression, TriggerAnnotation> cache;

+  internal class TriggerAnnotationsCache {

+    public readonly HashSet<Expression> exprsInOldContext;

+    public readonly Dictionary<Expression, TriggerAnnotation> annotations;

 

-    internal TriggersCollector() {

-      this.cache = new Dictionary<Expression, TriggerAnnotation>();

+    /// <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) {

@@ -162,7 +178,7 @@ namespace Microsoft.Dafny.Triggers {
 

     private TriggerAnnotation Annotate(Expression expr) {

       TriggerAnnotation cached;

-      if (cache.TryGetValue(expr, out cached)) {

+      if (cache.annotations.TryGetValue(expr, out cached)) {

         return cached;

       }

 

@@ -193,13 +209,13 @@ namespace Microsoft.Dafny.Triggers {
       }

 

       TriggerUtils.DebugTriggers("{0} ({1})\n{2}", Printer.ExprToString(expr), expr.GetType(), annotation);

-      cache[expr] = annotation;

+      cache.annotations[expr] = annotation;

       return annotation;

     }

 

     private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) {

       bool expr_is_killer = false;

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

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

diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy
new file mode 100644
index 00000000..c54089f2
--- /dev/null
+++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy
@@ -0,0 +1,32 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file shows cases where loops could hide behind equalities. In all three

+// cases we behave the same; that is, we don't warn for loops that would only

+// exist in the presence of an equality. The easiest way to understand the

+// issue, I (CPC) feel, is to look at the old case: f(x) could very well loop

+// with old(f(f(x))) if f(f(x)) did not change the heap at all.

+

+// This equality issue is generally undecidable. It could make sense to special

+// case `old`, but KRML and CPC decided against it on 2015-08-21. Future

+// experiences could cause a change of mind.

+

+class C { }

+function f(c: C): C

+function g(c: C): C

+function h(c: C, i: int): C

+

+// With explicit arguments

+method M0(i: int, j: int, sc: set<C>) {

+  assert forall c | c in sc :: true || h(c, i) == h(h(c, j), j);

+}

+

+// With implicit arguments (f and g respectively, to Apply)

+method M1(f: int -> int, g: int -> int) {

+  assert forall x :: true || f(x) == g(f(x));

+}

+

+// With implicit arguments (the heap, to old)

+method M2(sc: set<C>) {

+  assert forall c | c in sc :: true || f(c) == old(f(f(c)));

+}

diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect
new file mode 100644
index 00000000..c0eebdba
--- /dev/null
+++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect
@@ -0,0 +1,10 @@
+looping-is-hard-to-decide-modulo-equality.dfy(21,9): Info: Selected triggers:

+   {h(h(c, j), j)}, {h(c, i)}, {c in sc}

+ Rejected triggers: {h(c, j)} (loops with {h(h(c, j), j)})

+looping-is-hard-to-decide-modulo-equality.dfy(26,9): Info: Selected triggers: {f(x)}

+ Rejected triggers: {g(f(x))} (more specific than {f(x)})

+looping-is-hard-to-decide-modulo-equality.dfy(31,9): Info: Selected triggers:

+   {old(f(f(c)))}, {f(c)}, {c in sc}

+ Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))})

+

+Dafny program verifier finished with 9 verified, 0 errors

diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy b/Test/triggers/old-is-a-special-case-for-triggers.dfy
new file mode 100644
index 00000000..4424e8d3
--- /dev/null
+++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy
@@ -0,0 +1,32 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This file ensures that `old()` receives the special treatment that it

+// requires; that is, `old(f(x))` is not less liberal than `f(x)`, and

+// old(f(f(x))) does not loop with f(x) (doesn't it?)

+

+class C { }

+function f(c: C): C

+function g(c: C): C

+function h(c: C, i: int): C

+

+method M(sc: set<C>)

+  // Ensure that old(c) does not get picked as a trigger

+  ensures forall c | c in sc :: true || c == old(f(c))

+

+  // This checks whether loop detection handles `old` expressions properly.

+  // In the first one f(c)/old(f(f(c))) is not reported as a loop. See

+  // looping-is-hard-to-decide-modulo-equalities.dfy for an explanation.

+  ensures forall c | c in sc :: true || f(c) == old(f(f(c)))

+  ensures forall c | c in sc :: true || old(f(f(c))) == old(g(f(c))) || old(f(g(c))) == g(f(c)) || f(g(c)) == g(f(c))

+

+  // These check that the final trigger filtering step doesn't get confused

+  // between old expressions and regular expressions.

+  ensures forall c | c in sc :: true || f(c) == old(g(f(c)))

+  ensures forall c | c in sc :: true || f(c) == old(f(c)) || old(g(f(c))) == g(f(c))

+

+  // WISH: A Dafny rewriter could cleanup expressions so that adding the

+  //       expression forall c :: c == old(c) in a quantifier would cause a warning,

+  //       instead of a trigger generation error as it does now.

+{

+}

diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
new file mode 100644
index 00000000..23ec089d
--- /dev/null
+++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
@@ -0,0 +1,22 @@
+old-is-a-special-case-for-triggers.dfy(15,10): Info: Selected triggers:

+   {old(f(c))}, {c in sc}

+old-is-a-special-case-for-triggers.dfy(20,10): Info: Selected triggers:

+   {old(f(f(c)))}, {f(c)}, {c in sc}

+ Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))})

+old-is-a-special-case-for-triggers.dfy(21,10): Info: Selected triggers:

+   {f(g(c))}, {g(f(c))}, {old(f(g(c)))}, {old(g(f(c)))}, {old(f(f(c)))}, {c in sc}

+ Rejected triggers:

+   {g(c)} (loops with {g(f(c))})

+   {f(c)} (loops with {f(g(c))})

+   {old(g(c))} (loops with {old(g(f(c)))})

+   {old(f(c))} (loops with {old(f(f(c)))}, {old(f(g(c)))})

+old-is-a-special-case-for-triggers.dfy(25,10): Info: Selected triggers:

+   {old(f(c))}, {f(c)}, {c in sc}

+ Rejected triggers: {old(g(f(c)))} (more specific than {old(f(c))})

+old-is-a-special-case-for-triggers.dfy(26,10): Info: Selected triggers:

+   {old(f(c))}, {f(c)}, {c in sc}

+ Rejected triggers:

+   {g(f(c))} (more specific than {f(c)})

+   {old(g(f(c)))} (more specific than {old(f(c))})

+

+Dafny program verifier finished with 5 verified, 0 errors