refactor: Clean up resolution passes 0 and 1

Source/DafnyCore/AST/AstVisitor.cs

@@ -57,7 +57,7 @@ protected virtual void VisitOneDeclaration(TopLevelDecl decl) {
  }
 
  if (decl is TopLevelDeclWithMembers cl) {
- cl.Members.Iter(member => VisitMember(cl, member));
+ cl.Members.Iter(VisitMember);
  }
  }
 
@@ -89,19 +89,9 @@ private void VisitIterator(IteratorDecl iteratorDecl) {
  }
  }
 
- protected virtual void VisitMember(TopLevelDeclWithMembers cl, MemberDecl member) {
- if (member is ConstantField constantField) {
- var context = GetContext(constantField, false);
- VisitAttributes(constantField, constantField.EnclosingModule);
- VisitUserProvidedType(constantField.Type, context);
- if (constantField.Rhs != null) {
- VisitExpression(constantField.Rhs, context);
- }
-
- } else if (member is Field field) {
- var context = GetContext(new NoContext(cl.EnclosingModuleDefinition), false);
- VisitAttributes(field, cl.EnclosingModuleDefinition);
- VisitUserProvidedType(field.Type, context);
+ public void VisitMember(MemberDecl member) {
+ if (member is Field field) {
+ VisitField(field);
 
  } else if (member is Function function) {
  VisitFunction(function);
@@ -129,6 +119,18 @@ protected virtual void VisitMember(TopLevelDeclWithMembers cl, MemberDecl member
  }
  }
 
+ public virtual void VisitField(Field field) {
+ var enclosingModule = field.EnclosingClass.EnclosingModuleDefinition;
+ VisitAttributes(field, enclosingModule);
+
+ var context = GetContext(field as IASTVisitorContext ?? new NoContext(enclosingModule), false);
+ VisitUserProvidedType(field.Type, context);
+
+ if (field is ConstantField { Rhs: { } rhs }) {
+ VisitExpression(rhs, context);
+ }
+ }
+
  public virtual void VisitFunction(Function function) {
  var context = GetContext(function, false);
 
@@ -260,18 +262,26 @@ protected virtual void VisitExpression(Expression expr, VisitorContext context)
 
  // Visit subexpressions
  expr.SubExpressions.Iter(ee => VisitExpression(ee, context));
+
+ // Finish by calling the post-visitor method
+ PostVisitOneExpression(expr, context);
  }
  }
 
  /// <summary>
  /// Visits the given expression.
- /// Returns "true" to request that the caller keeps visiting all user-provided types, subexpressions, and substatements of "expr", and
- /// returns "false" to tell the caller not to.
+ /// Returns "true" to request that the caller
+ /// - keeps visiting all user-provided types, subexpressions, and substatements of "expr", and
+ /// - then calls PostVisitOneExpression.
+ /// Returns "false" to tell the caller not to do those things.
  /// </summary>
  protected virtual bool VisitOneExpression(Expression expr, VisitorContext context) {
  return true;
  }
 
+ protected virtual void PostVisitOneExpression(Expression expr, VisitorContext context) {
+ }
+
  protected virtual void VisitStatement(Statement stmt, VisitorContext context) {
  if (VisitOneStatement(stmt, context)) {
  // Visit user-provided types
@@ -317,17 +327,25 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) {
 
  // Visit substatements
  stmt.SubStatements.Iter(ss => VisitStatement(ss, context));
+
+ // Finish by calling the post-visitor method
+ PostVisitOneStatement(stmt, context);
  }
  }
 
  /// <summary>
  /// Visits the given statement.
- /// Returns "true" to request that the caller keeps visiting all user-provided types, subexpressions, and substatements of "stmt", and
- /// returns "false" to tell the caller not to.
+ /// Returns "true" to request that the caller
+ /// - keeps visiting all user-provided types, subexpressions, and substatements of "stmt", and
+ /// - then calls PostVisitOneStatement.
+ /// Returns "false" to tell the caller not to do those things.
  /// </summary>
  protected virtual bool VisitOneStatement(Statement stmt, VisitorContext context) {
  return true;
  }
+
+ protected virtual void PostVisitOneStatement(Statement stmt, VisitorContext context) {
+ }
  }
 
 }

Source/DafnyCore/AST/DafnyAst.cs

@@ -345,22 +345,21 @@ public static bool Contains(Attributes attrs, string nm) {
  /// - if the attribute is {:nm true}, then value==true
  /// - if the attribute is {:nm false}, then value==false
  /// - if the attribute is anything else, then value returns as whatever it was passed in as.
+ /// This method does NOT use type information of the attribute arguments, so it can safely
+ /// be called very early during resolution before types are available and names have been resolved.
  /// </summary>
  [Pure]
  public static bool ContainsBool(Attributes attrs, string nm, ref bool value) {
  Contract.Requires(nm != null);
- foreach (var attr in attrs.AsEnumerable()) {
- if (attr.Name == nm) {
- if (attr.Args.Count == 1) {
- var arg = attr.Args[0] as LiteralExpr;
- if (arg != null && arg.Value is bool) {
- value = (bool)arg.Value;
- }
- }
- return true;
- }
+ var attr = attrs.AsEnumerable().FirstOrDefault(attr => attr.Name == nm);
+ if (attr == null) {
+ return false;
  }
- return false;
+
+ if (attr.Args.Count == 1 && attr.Args[0] is LiteralExpr { Value: bool v }) {
+ value = v;
+ }
+ return true;
  }
 
  /// <summary>

Source/DafnyCore/AST/Printer.cs

@@ -309,6 +309,7 @@ public void PrintTopLevelDecls(List<TopLevelDecl> decls, int indent, List<IToken
  }
  }
  if (dd.Members.Count != 0) {
+ Indent(indent);
  wr.WriteLine("{");
  PrintMembers(dd.Members, indent + IndentAmount, fileBeingPrinted);
  Indent(indent);

Source/DafnyCore/ExpressionTester.cs

@@ -230,33 +230,30 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext) {
  return isCompilable;
  } else if (expr is LambdaExpr lambdaExpr) {
  return CheckIsCompilable(lambdaExpr.Body, codeContext);
- } else if (expr is ComprehensionExpr comprehensionExpr) {
- var uncompilableBoundVars = comprehensionExpr.UncompilableBoundVars();
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ var uncompilableBoundVars = e.UncompilableBoundVars();
  if (uncompilableBoundVars.Count != 0) {
- if (ReportErrors == false) {
- return false;
- }
-
  string what;
- if (comprehensionExpr is SetComprehension comprehension) {
+ if (e is SetComprehension comprehension) {
  what = comprehension.Finite ? "set comprehensions" : "iset comprehensions";
- } else if (comprehensionExpr is MapComprehension mapComprehension) {
+ } else if (e is MapComprehension mapComprehension) {
  what = mapComprehension.Finite ? "map comprehensions" : "imap comprehensions";
  } else {
- Contract.Assume(comprehensionExpr is QuantifierExpr); // otherwise, unexpected ComprehensionExpr (since LambdaExpr is handled separately above)
- Contract.Assert(((QuantifierExpr)comprehensionExpr).SplitQuantifier == null); // No split quantifiers during resolution
+ 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
  what = "quantifiers";
  }
  foreach (var bv in uncompilableBoundVars) {
- reporter.Error(MessageSource.Resolver, comprehensionExpr, "{0} in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for '{1}'", what, bv.Name);
+ reporter?.Error(MessageSource.Resolver, e, "{0} in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for '{1}'", what, bv.Name);
+ isCompilable = false;
  }
- return false;
  }
  // don't recurse down any attributes
- if (comprehensionExpr.Range != null) {
- isCompilable = CheckIsCompilable(comprehensionExpr.Range, codeContext) && isCompilable;
+ if (e.Range != null) {
+ isCompilable = CheckIsCompilable(e.Range, codeContext) && isCompilable;
  }
- isCompilable = CheckIsCompilable(comprehensionExpr.Term, codeContext) && isCompilable;
+ isCompilable = CheckIsCompilable(e.Term, codeContext) && isCompilable;
  return isCompilable;
 
  } else if (expr is ChainingExpression chainingExpression) {

Source/DafnyCore/Resolver/BoundsDiscovery.cs

@@ -11,6 +11,91 @@
 
 namespace Microsoft.Dafny {
  public partial class Resolver {
+ private class BoundsDiscoveryVisitor : ASTVisitor<IASTVisitorContext> {
+ private readonly ErrorReporter reporter;
+
+ public BoundsDiscoveryVisitor(ErrorReporter reporter) {
+ this.reporter = reporter;
+ }
+
+ public override IASTVisitorContext GetContext(IASTVisitorContext astVisitorContext, bool inFunctionPostcondition) {
+ return astVisitorContext;
+ }
+
+ protected override bool VisitOneStatement(Statement stmt, IASTVisitorContext context) {
+ if (stmt is ForallStmt forallStmt) {
+ forallStmt.Bounds = DiscoverBestBounds_MultipleVars(forallStmt.BoundVars, forallStmt.Range, true,
+ ComprehensionExpr.BoundedPool.PoolVirtues.Enumerable);
+ } else if (stmt is AssignSuchThatStmt assignSuchThatStmt) {
+ if (assignSuchThatStmt.AssumeToken == null) {
+ var varLhss = new List<IVariable>();
+ foreach (var lhs in assignSuchThatStmt.Lhss) {
+ var ide = (IdentifierExpr)lhs.Resolved; // successful resolution implies all LHS's are IdentifierExpr's
+ varLhss.Add(ide.Var);
+ }
+ assignSuchThatStmt.Bounds = DiscoverBestBounds_MultipleVars(varLhss, assignSuchThatStmt.Expr, true,
+ ComprehensionExpr.BoundedPool.PoolVirtues.None);
+ }
+ }
+
+ return base.VisitOneStatement(stmt, context);
+ }
+
+ protected override bool VisitOneExpression(Expression expr, IASTVisitorContext context) {
+ if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ // apply bounds discovery to quantifiers, finite sets, and finite maps
+ string what = e.WhatKind;
+ Expression whereToLookForBounds = null;
+ var polarity = true;
+ if (e is QuantifierExpr quantifierExpr) {
+ whereToLookForBounds = quantifierExpr.LogicalBody();
+ polarity = quantifierExpr is ExistsExpr;
+ } else if (e is SetComprehension setComprehension) {
+ whereToLookForBounds = setComprehension.Range;
+ } else if (e is MapComprehension) {
+ whereToLookForBounds = e.Range;
+ } else {
+ Contract.Assume(e is LambdaExpr); // otherwise, unexpected ComprehensionExpr
+ }
+ if (whereToLookForBounds != null) {
+ e.Bounds = DiscoverBestBounds_MultipleVars_AllowReordering(e.BoundVars, whereToLookForBounds, polarity, ComprehensionExpr.BoundedPool.PoolVirtues.None);
+ if (2 <= DafnyOptions.O.Allocated && (context is Function or ConstantField or RedirectingTypeDecl)) {
+ // functions are not allowed to depend on the set of allocated objects
+ foreach (var bv in ComprehensionExpr.BoundedPool.MissingBounds(e.BoundVars, e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.IndependentOfAlloc)) {
+ var msgFormat = "a {0} involved in a {3} definition is not allowed to depend on the set of allocated references, but values of '{1}' may contain references";
+ if (bv.Type.IsTypeParameter || bv.Type.IsOpaqueType) {
+ msgFormat += " (perhaps declare its type, '{2}', as '{2}(!new)')";
+ }
+ msgFormat += " (see documentation for 'older' parameters)";
+ var declKind = context is RedirectingTypeDecl redir ? redir.WhatKind : ((MemberDecl)context).WhatKind;
+ reporter.Error(MessageSource.Resolver, e, msgFormat, e.WhatKind, bv.Name, bv.Type, declKind);
+ }
+ }
+
+ if ((e as SetComprehension)?.Finite == true || (e as MapComprehension)?.Finite == true) {
+ // the comprehension had better produce a finite set
+ if (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
+ // resolution), the resolver will generate an error about that later.
+ } else {
+ // we cannot be sure that the set/map really is finite
+ foreach (var bv in ComprehensionExpr.BoundedPool.MissingBounds(e.BoundVars, e.Bounds, ComprehensionExpr.BoundedPool.PoolVirtues.Finite)) {
+ reporter.Error(MessageSource.Resolver, e,
+ "the result of a {0} must be finite, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{1}'",
+ e.WhatKind, bv.Name);
+ }
+ }
+ }
+ }
+
+ }
+
+ return base.VisitOneExpression(expr, context);
+ }
+ }
+
  /// <summary>
  /// For a list of variables "bvars", returns a list of best bounds, subject to the constraint "requiredVirtues", for each respective variable.
  /// If no bound matching "requiredVirtues" is found for a variable "v", then the bound for "v" in the returned list is set to "null".