Implemented resolution, verification, and (poorly performing) compilation of existential if guards.

Fixed bugs in ghost checks involving comprehensions and attributes.
Added SubstituteBoundedPool method.

4 files changed, 198 insertions, 43 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 13381cc7..aa4ca3ec 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1455,10 +1455,17 @@ namespace Microsoft.Dafny {
           }

         } else {

           Indent(indent);  wr.Write("if (");

-          TrExpr(s.Guard);

+          TrExpr(s.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)s.Guard, "eg_d", new Translator(null)) : s.Guard);

           wr.WriteLine(")");

 

-          TrStmt(s.Thn, indent);

+          // We'd like to do "TrStmt(s.Thn, indent)", except we want the scope of any existential variables to come inside the block

+          Indent(indent); wr.WriteLine("{");

+          if (s.IsExistentialGuard) {

+            IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)s.Guard);

+          }

+          TrStmtList(s.Thn.Body, indent);

+          Indent(indent); wr.WriteLine("}");

+

           if (s.Els != null) {

             Indent(indent);  wr.WriteLine("else");

             TrStmt(s.Els, indent);

@@ -1467,13 +1474,14 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is AlternativeStmt) {

         var s = (AlternativeStmt)stmt;

-        foreach (var alternative in s.Alternatives) {

-        }

         Indent(indent);

         foreach (var alternative in s.Alternatives) {

           wr.Write("if (");

-          TrExpr(alternative.Guard);

+          TrExpr(alternative.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)alternative.Guard, "eg_d", new Translator(null)) : alternative.Guard);

           wr.WriteLine(") {");

+          if (alternative.IsExistentialGuard) {

+            IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)alternative.Guard);

+          }

           TrStmtList(alternative.Body, indent);

           Indent(indent);

           wr.Write("} else ");

@@ -1766,6 +1774,18 @@ namespace Microsoft.Dafny {
       }

     }

 

+    private void IntroduceAndAssignBoundVars(int indent, ExistsExpr exists) {

+      Contract.Requires(0 <= indent);

+      Contract.Requires(exists != null);

+      Contract.Assume(exists.Bounds != null);  // follows from successful resolution

+      Contract.Assert(exists.Range == null);  // follows from invariant of class IfStmt

+      foreach (var bv in exists.BoundVars) {

+        TrLocalVar(bv, false, indent);

+      }

+      var ivars = exists.BoundVars.ConvertAll(bv => (IVariable)bv);

+      TrAssignSuchThat(indent, ivars, exists.Term, exists.Bounds, exists.tok.line);

+    }

+

     private void TrAssignSuchThat(int indent, List<IVariable> lhss, Expression constraint, List<ComprehensionExpr.BoundedPool> bounds, int debuginfoLine) {

       Contract.Requires(0 <= indent);

       Contract.Requires(lhss != null);

@@ -2155,18 +2175,18 @@ namespace Microsoft.Dafny {
       }

     }

 

-    void TrLocalVar(LocalVariable s, bool alwaysInitialize, int indent) {

-      Contract.Requires(s != null);

-      if (s.IsGhost) {

+    void TrLocalVar(IVariable v, bool alwaysInitialize, int indent) {

+      Contract.Requires(v != null);

+      if (v.IsGhost) {

         // only emit non-ghosts (we get here only for local variables introduced implicitly by call statements)

         return;

       }

 

       Indent(indent);

-      wr.Write("{0} @{1}", TypeName(s.Type), s.CompileName);

+      wr.Write("{0} @{1}", TypeName(v.Type), v.CompileName);

       if (alwaysInitialize) {

         // produce a default value

-        wr.WriteLine(" = {0};", DefaultValue(s.Type));

+        wr.WriteLine(" = {0};", DefaultValue(v.Type));

       } else {

         wr.WriteLine(";");

       }

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 64af1425..667f8407 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3903,7 +3903,7 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Expr != null);

     }

 

-    public ExprRhs(Expression expr, Attributes attrs = null)

+    public ExprRhs(Expression expr, Attributes attrs = null)  // TODO: these 'attrs' apparently aren't handled correctly in the Cloner, and perhaps not in various visitors either (for example, CheckIsCompilable should not go into attributes)

       : base(expr.tok, attrs)

     {

       Contract.Requires(expr != null);

@@ -7175,9 +7175,16 @@ namespace Microsoft.Dafny {
     public override IEnumerable<Expression> SubExpressions {

       get {

         if (SplitQuantifier == null) {

-          return base.SubExpressions;

+          foreach (var e in base.SubExpressions) {

+            yield return e;

+          }

         } else {

-          return SplitQuantifier;

+          foreach (var e in Attributes.SubExpressions(Attributes)) {

+            yield return e;

+          }

+          foreach (var e in SplitQuantifier) {

+            yield return e;

+          }

         }

       }

     }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index bc94e491..1798243c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2264,12 +2264,14 @@ namespace Microsoft.Dafny
             what = "quantifier";

             whereToLookForBounds = ((QuantifierExpr)e).LogicalBody();

             polarity = e is ExistsExpr;

-          } else if (e is SetComprehension && ((SetComprehension)e).Finite) {

+          } else if (e is SetComprehension) {

             what = "set comprehension";

             whereToLookForBounds = e.Range;

-          } else if (e is MapComprehension && ((MapComprehension)e).Finite) {

+          } else if (e is MapComprehension) {

             what = "map comprehension";

             whereToLookForBounds = e.Range;

+          } else {

+            Contract.Assume(e is LambdaExpr);  // otherwise, unexpected ComprehensionExpr

           }

           if (whereToLookForBounds != null) {

             List<BoundVar> missingBounds;

@@ -2278,9 +2280,9 @@ namespace Microsoft.Dafny
               e.MissingBounds = missingBounds;

 

               if ((e is SetComprehension && !((SetComprehension)e).Finite) || (e is MapComprehension && !((MapComprehension)e).Finite)) {

-                // a possibly infinite set/map has no restrictions on its range

+                // a possibly infinite set/map has no restrictions on its range (unless it's used in a compilable context, which is checked later)

               } else if (e is QuantifierExpr) {

-                // don't report any errors at this time (instead, wait to see if the quantifier is used in a non-ghost context)

+                // a quantifier has no restrictions on its range (unless it's used in a compilable context, which is checked later)

               } else if (e is SetComprehension && e.Type.HasFinitePossibleValues) {

                 // This means the set is finite, regardless of if the Range is bounded.  So, we don't give any error here.

                 // However, if this expression is used in a non-ghost context (which is not yet known at this stage of

@@ -2341,7 +2343,6 @@ namespace Microsoft.Dafny
           var bin = expr as BinaryExpr;

           if (bin != null) {

             bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type);

-          

           }

         }

       }

@@ -5647,7 +5648,17 @@ namespace Microsoft.Dafny
           Contract.Assert(s.Guard.Type != null);  // follows from postcondition of ResolveExpression

           ConstrainTypes(s.Guard.Type, Type.Bool, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);

         }

-        ResolveStatement(s.Thn, codeContext);

+

+        scope.PushMarker();

+        if (s.IsExistentialGuard) {

+          var exists = (ExistsExpr)s.Guard;

+          foreach (var v in exists.BoundVars) {

+            ScopePushAndReport(scope, v, "bound-variable");

+          }

+        }

+        ResolveBlockStatement(s.Thn, codeContext);

+        scope.PopMarker();

+

         if (s.Els != null) {

           ResolveStatement(s.Els, codeContext);

         }

@@ -6525,7 +6536,7 @@ namespace Microsoft.Dafny
       Contract.Requires(alternatives != null);

       Contract.Requires(codeContext != null);

 

-      // first, resolve the guards, which tells us whether or not the entire statement is a ghost statement

+      // first, resolve the guards

       foreach (var alternative in alternatives) {

         int prevErrorCount = reporter.Count(ErrorLevel.Error);

         ResolveExpression(alternative.Guard, new ResolveOpts(codeContext, true));

@@ -6539,6 +6550,12 @@ namespace Microsoft.Dafny
       }

       foreach (var alternative in alternatives) {

         scope.PushMarker();

+        if (alternative.IsExistentialGuard) {

+          var exists = (ExistsExpr)alternative.Guard;

+          foreach (var v in exists.BoundVars) {

+            ScopePushAndReport(scope, v, "bound-variable");

+          }

+        }

         foreach (Statement ss in alternative.Body) {

           ResolveStatement(ss, codeContext);

         }

@@ -9508,9 +9525,9 @@ namespace Microsoft.Dafny
         if (uncompilableBoundVars.Count != 0) {

           string what;

           if (e is SetComprehension) {

-            what = "set comprehensions";

+            what = ((SetComprehension)e).Finite ? "set comprehensions" : "iset comprehensions";

           } else if (e is MapComprehension) {

-            what = "map comprehensions";

+            what = ((MapComprehension)e).Finite ? "map comprehensions" : "imap comprehensions";

           } else {

             Contract.Assume(e is QuantifierExpr);  // otherwise, unexpected ComprehensionExpr (since LambdaExpr is handled separately above)

             Contract.Assert(((QuantifierExpr)e).SplitQuantifier == null); // No split quantifiers during resolution

@@ -9521,15 +9538,11 @@ namespace Microsoft.Dafny
           }

           return;

         }

+        // don't recurse down any attributes

+        if (e.Range != null) { CheckIsCompilable(e.Range); }

+        CheckIsCompilable(e.Term);

+        return;

 

-      } else if (expr is MapComprehension) {

-        var e = (MapComprehension)expr;

-        if (e.MissingBounds != null && !e.Finite) {

-          foreach (var bv in e.MissingBounds) {

-            reporter.Error(MessageSource.Resolver, expr, "imaps in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);

-          }

-          return;

-        }

       } else if (expr is NamedExpr) {

         if (!moduleInfo.IsAbstract)

           CheckIsCompilable(((NamedExpr)expr).Body);

@@ -10436,7 +10449,7 @@ namespace Microsoft.Dafny
       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;

         Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution

-        return e.UncompilableBoundVars().Count != 0;

+        return e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.LogicalBody());

       } else if (expr is SetComprehension) {

         var e = (SetComprehension)expr;

         return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index c84f0cec..18b50686 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4740,7 +4740,7 @@ namespace Microsoft.Dafny {
         var typeMap = Util.Dict(e.TypeArgs, Map(typeArgumentCopies, tp => (Type)new UserDefinedType(tp)));

         var newLocals = Map(typeArgumentCopies, tp => new Bpl.LocalVariable(tp.tok, new TypedIdent(tp.tok, nameTypeParam(tp), predef.Ty)));

         locals.AddRange(newLocals);

-        // Create local variables corresponding to the in-parameters:

+        // Create local variables corresponding to the bound variables:

         var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran, typeMap);

         // Get the body of the quantifier and suitably substitute for the type variables and bound variables

         var body = Substitute(e.LogicalBody(true), null, substMap, typeMap);

@@ -7244,24 +7244,30 @@ namespace Microsoft.Dafny {
       } else if (stmt is IfStmt) {

         AddComment(builder, stmt, "if statement");

         IfStmt s = (IfStmt)stmt;

-        Bpl.Expr guard;

+        Expression guard;

         if (s.Guard == null) {

           guard = null;

         } else {

-          TrStmt_CheckWellformed(s.Guard, builder, locals, etran, true);

-          guard = etran.TrExpr(s.Guard);

+          guard = s.IsExistentialGuard ? AlphaRename((ExistsExpr)s.Guard, "eg$", this) : s.Guard;

+          TrStmt_CheckWellformed(guard, builder, locals, etran, true);

         }

         Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();

         CurrentIdGenerator.Push();

+        if (s.IsExistentialGuard) {

+          var exists = (ExistsExpr)s.Guard;  // the original (that is, not alpha-renamed) guard

+          IntroduceAndAssignExistentialVars(exists, b, builder, locals, etran);

+        }

         Bpl.StmtList thn = TrStmt2StmtList(b, s.Thn, locals, etran);

         CurrentIdGenerator.Pop();

         Bpl.StmtList els;

         Bpl.IfCmd elsIf = null;

+        b = new Bpl.StmtListBuilder();

+        if (s.IsExistentialGuard) {

+          b.Add(new Bpl.AssumeCmd(guard.tok, Bpl.Expr.Not(etran.TrExpr(guard))));

+        }

         if (s.Els == null) {

-          b = new Bpl.StmtListBuilder();

           els = b.Collect(s.Tok);

         } else {

-          b = new Bpl.StmtListBuilder();

           els = TrStmt2StmtList(b, s.Els, locals, etran);

           if (els.BigBlocks.Count == 1) {

             Bpl.BigBlock bb = els.BigBlocks[0];

@@ -7271,7 +7277,7 @@ namespace Microsoft.Dafny {
             }

           }

         }

-        builder.Add(new Bpl.IfCmd(stmt.Tok, guard, thn, elsIf, els));

+        builder.Add(new Bpl.IfCmd(stmt.Tok, guard == null || s.IsExistentialGuard ? null : etran.TrExpr(guard), thn, elsIf, els));

 

       } else if (stmt is AlternativeStmt) {

         AddComment(builder, stmt, "alternative statement");

@@ -7551,6 +7557,26 @@ namespace Microsoft.Dafny {
       }

     }

 

+    private void IntroduceAndAssignExistentialVars(ExistsExpr exists, Bpl.StmtListBuilder builder, Bpl.StmtListBuilder builderOutsideIfConstruct, List<Variable> locals, ExpressionTranslator etran) {

+      Contract.Requires(exists != null);

+      Contract.Requires(exists.Range == null);

+      Contract.Requires(builder != null);

+      Contract.Requires(builderOutsideIfConstruct != null);

+      Contract.Requires(locals != null);

+      Contract.Requires(etran != null);

+      // declare and havoc the bound variables of 'exists' as local variables

+      var iesForHavoc = new List<Bpl.IdentifierExpr>();

+      foreach (var bv in exists.BoundVars) {

+        Bpl.Type varType = TrType(bv.Type);

+        Bpl.Expr wh = GetWhereClause(bv.Tok, new Bpl.IdentifierExpr(bv.Tok, bv.AssignUniqueName(currentDeclaration.IdGenerator), varType), bv.Type, etran);

+        Bpl.Variable local = new Bpl.LocalVariable(bv.Tok, new Bpl.TypedIdent(bv.Tok, bv.AssignUniqueName(currentDeclaration.IdGenerator), varType, wh));

+        locals.Add(local);

+        iesForHavoc.Add(new Bpl.IdentifierExpr(local.tok, local));

+      }

+      builderOutsideIfConstruct.Add(new Bpl.HavocCmd(exists.tok, iesForHavoc));

+      builder.Add(new Bpl.AssumeCmd(exists.tok, etran.TrExpr(exists.Term)));

+    }

+

     void TrStmtList(List<Statement> stmts, Bpl.StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {

       Contract.Requires(stmts != null);

       Contract.Requires(builder != null);

@@ -7565,6 +7591,46 @@ namespace Microsoft.Dafny {
     }

 

     /// <summary>

+    /// Returns an expression like 'exists' but where the bound variables have been renamed to have

+    /// 'prefix' as a prefix to their previous names.

+    /// Assumes the expression has been resolved.

+    /// </summary>

+    public static Expression AlphaRename(ExistsExpr exists, string prefix, Translator translator) {

+      Contract.Requires(exists != null);

+      Contract.Requires(prefix != null);

+      Contract.Requires(translator != null);

+

+      if (exists.SplitQuantifier != null) {

+        // TODO: what to do?  Substitute(exists.SplitQuantifierExpression);

+      }

+

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

+      var var4var = new Dictionary<BoundVar, BoundVar>();

+      var bvars = new List<BoundVar>();

+      foreach (var bv in exists.BoundVars) {

+        var newBv = new BoundVar(bv.tok, prefix + bv.Name, bv.Type);

+        bvars.Add(newBv);

+        var4var.Add(bv, newBv);

+        var ie = new IdentifierExpr(newBv.tok, newBv.Name);

+        ie.Var = newBv;  // resolve here

+        ie.Type = newBv.Type;  // resolve here

+        substMap.Add(bv, ie);

+      }

+      var s = new Substituter(null, substMap, new Dictionary<TypeParameter, Type>(), translator);

+      var range = exists.Range == null ? null : s.Substitute(exists.Range);

+      var term = s.Substitute(exists.Term);

+      var attrs = s.SubstAttributes(exists.Attributes);

+      var ex = new ExistsExpr(exists.tok, exists.TypeArgs, bvars, range, term, attrs);

+      if (exists.Bounds != null) {

+        ex.Bounds = exists.Bounds.ConvertAll(bound => s.SubstituteBoundedPool(bound));

+      }

+      if (exists.MissingBounds != null) {

+        ex.MissingBounds = exists.MissingBounds.ConvertAll(bv => var4var[bv]);

+      }

+      return ex;

+    }

+

+    /// <summary>

     /// Generate:

     ///   havoc Heap \ {this} \ _reads \ _new;

     ///   assume this.Valid();

@@ -8569,7 +8635,7 @@ namespace Microsoft.Dafny {
     void TrAlternatives(List<GuardedAlternative> alternatives, Bpl.Cmd elseCase0, Bpl.StructuredCmd elseCase1,

                         Bpl.StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {

       Contract.Requires(alternatives != null);

-      Contract.Requires((elseCase0 != null) == (elseCase1 == null));  // ugly way of doing a type union

+      Contract.Requires((elseCase0 == null) != (elseCase1 == null));  // ugly way of doing a type union

       Contract.Requires(builder != null);

       Contract.Requires(locals != null);

       Contract.Requires(etran != null);

@@ -8583,10 +8649,13 @@ namespace Microsoft.Dafny {
         return;

       }

 

+      // alpha-rename any existential guards

+      var guards = alternatives.ConvertAll(alt => alt.IsExistentialGuard ? AlphaRename((ExistsExpr)alt.Guard, "eg$", this) : alt.Guard);

+

       // build the negation of the disjunction of all guards (that is, the conjunction of their negations)

       Bpl.Expr noGuard = Bpl.Expr.True;

-      foreach (var alternative in alternatives) {

-        noGuard = BplAnd(noGuard, Bpl.Expr.Not(etran.TrExpr(alternative.Guard)));

+      foreach (var g in guards) {

+        noGuard = BplAnd(noGuard, Bpl.Expr.Not(etran.TrExpr(g)));

       }

 

       var b = new Bpl.StmtListBuilder();

@@ -8605,8 +8674,13 @@ namespace Microsoft.Dafny {
         CurrentIdGenerator.Push();

         var alternative = alternatives[i];

         b = new Bpl.StmtListBuilder();

-        TrStmt_CheckWellformed(alternative.Guard, b, locals, etran, true);

-        b.Add(new AssumeCmd(alternative.Guard.tok, etran.TrExpr(alternative.Guard)));

+        TrStmt_CheckWellformed(guards[i], b, locals, etran, true);

+        if (alternative.IsExistentialGuard) {

+          var exists = (ExistsExpr)alternative.Guard;  // the original (that is, not alpha-renamed) guard

+          IntroduceAndAssignExistentialVars(exists, b, builder, locals, etran);

+        } else {

+          b.Add(new AssumeCmd(alternative.Guard.tok, etran.TrExpr(alternative.Guard)));

+        }

         foreach (var s in alternative.Body) {

           TrStmt(s, b, locals, etran);

         }

@@ -13705,6 +13779,9 @@ namespace Microsoft.Dafny {
               Contract.Assert(false);  // unexpected ComprehensionExpr

             }

           }

+          if (e.Bounds != null) {

+            ((ComprehensionExpr)newExpr).Bounds = e.Bounds.ConvertAll(bound => SubstituteBoundedPool(bound));

+          }

           // undo any changes to substMap (could be optimized to do this only if newBoundVars != e.BoundVars)

           foreach (var bv in e.BoundVars) {

             substMap.Remove(bv);

@@ -13761,6 +13838,44 @@ namespace Microsoft.Dafny {
         }

       }

 

+      public ComprehensionExpr.BoundedPool SubstituteBoundedPool(ComprehensionExpr.BoundedPool bound) {

+        if (bound == null) {

+          return null;

+        } else if (bound is ComprehensionExpr.ExactBoundedPool) {

+          var b = (ComprehensionExpr.ExactBoundedPool)bound;

+          return new ComprehensionExpr.ExactBoundedPool(Substitute(b.E));

+        } else if (bound is ComprehensionExpr.BoolBoundedPool) {

+          return bound;  // nothing to substitute

+        } else if (bound is ComprehensionExpr.CharBoundedPool) {

+          return bound;  // nothing to substitute

+        } else if (bound is ComprehensionExpr.RefBoundedPool) {

+          return bound;  // nothing to substitute

+        } else if (bound is ComprehensionExpr.IntBoundedPool) {

+          var b = (ComprehensionExpr.IntBoundedPool)bound;

+          return new ComprehensionExpr.IntBoundedPool(b.LowerBound == null ? null : Substitute(b.LowerBound), b.UpperBound == null ? null : Substitute(b.UpperBound));

+        } else if (bound is ComprehensionExpr.SetBoundedPool) {

+          var b = (ComprehensionExpr.SetBoundedPool)bound;

+          return new ComprehensionExpr.SetBoundedPool(Substitute(b.Set));

+        } else if (bound is ComprehensionExpr.SubSetBoundedPool) {

+          var b = (ComprehensionExpr.SubSetBoundedPool)bound;

+          return new ComprehensionExpr.SubSetBoundedPool(Substitute(b.UpperBound));

+        } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {

+          var b = (ComprehensionExpr.SuperSetBoundedPool)bound;

+          return new ComprehensionExpr.SuperSetBoundedPool(Substitute(b.LowerBound));

+        } else if (bound is ComprehensionExpr.MapBoundedPool) {

+          var b = (ComprehensionExpr.MapBoundedPool)bound;

+          return new ComprehensionExpr.MapBoundedPool(Substitute(b.Map));

+        } else if (bound is ComprehensionExpr.SeqBoundedPool) {

+          var b = (ComprehensionExpr.SeqBoundedPool)bound;

+          return new ComprehensionExpr.SeqBoundedPool(Substitute(b.Seq));

+        } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {

+          return bound;  // nothing to substitute

+        } else {

+          Contract.Assume(false);  // unexpected ComprehensionExpr.BoundedPool

+          throw new cce.UnreachableException();  // to please compiler

+        }

+      }

+

       /// <summary>

       /// Return a list of bound variables, of the same length as 'vars' but with possible substitutions.

       /// For any change necessary, update 'substMap' to reflect the new substitution; the caller is responsible for