Test ResolutionErrors[01238] with new resolver (#5324)

This PR changes 5 of the 10 `dafny0/ResolutionErrors*.dfy` tests so that
they test not only the legacy resolver, but also the resolver refresh.
The process of converting these tests over detected several omissions
and other issues with the resolver refresh, and the PR fixes those
problems. In several other cases, the new resolver produces the errors
in different phases than the old resolver; to make the tests apply to
both legacy and refresh resolver, some tests had to be split into
several methods or several modules.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs

@@ -12,7 +12,7 @@ public class IdPattern : ExtendedPattern, IHasUsages {
  public bool HasParenthesis { get; }
  public String Id;
  public PreType PreType;
- public Type Type; // This is the syntactic type, ExtendedPatterns dissapear during resolution.
+ public Type Type; // This is the syntactic type, ExtendedPatterns disappear during resolution.
  public IVariable BoundVar { get; set; }
  public List<ExtendedPattern> Arguments; // null if just an identifier; possibly empty argument list if a constructor call
  public LiteralExpr ResolvedLit; // null if just an identifier
@@ -108,8 +108,9 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
  };
  BoundVar = localVariable;
  } else {
- var boundVar = new BoundVar(Tok, Id, Type);
- boundVar.IsGhost = isGhost;
+ var boundVar = new BoundVar(Tok, Id, Type) {
+ IsGhost = isGhost
+ };
  BoundVar = boundVar;
  }
 

Source/DafnyCore/AST/SubstitutingCloner.cs

@@ -3,18 +3,18 @@
 namespace Microsoft.Dafny;
 
 class SubstitutingCloner : Cloner {
- private readonly Dictionary<IVariable, Expression> substitutions;
+ private readonly Dictionary<IVariable, IVariable> substitutions;
 
- public SubstitutingCloner(Dictionary<IVariable, Expression> substitutions, bool cloneResolvedFields)
+ public SubstitutingCloner(Dictionary<IVariable, IVariable> substitutions, bool cloneResolvedFields)
  : base(false, cloneResolvedFields) {
  this.substitutions = substitutions;
  }
 
  public override Expression CloneExpr(Expression expr) {
  if (expr is IdentifierExpr identifierExpr) {
- if (substitutions.TryGetValue(identifierExpr.Var, out var substitution)) {
- // TODO consider using the code from Substitutor
- return substitution;
+ if (substitutions.TryGetValue(identifierExpr.Var, out var variableReplacement)) {
+ // TODO consider using the code from Substituter
+ return new IdentifierExpr(expr.tok, variableReplacement);
  }
  }
 

Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs

@@ -711,15 +711,17 @@ private PatternPath LetBind(IdPattern var, Expression genExpr, PatternPath bodyP
  return stmtPath;
  }
 
- var caseLocal = new LocalVariable(var.RangeToken, name, type, isGhost);
- caseLocal.type = type;
+ var caseLocal = new LocalVariable(var.RangeToken, name, type, isGhost) {
+ type = type
+ };
  var casePattern = new CasePattern<LocalVariable>(caseLocal.RangeToken.EndToken, caseLocal);
  casePattern.AssembleExpr(new List<Type>());
- var caseLet = new VarDeclPattern(caseLocal.RangeToken, casePattern, expr, false);
- caseLet.IsGhost = isGhost;
+ var caseLet = new VarDeclPattern(caseLocal.RangeToken, casePattern, expr, false) {
+ IsGhost = isGhost
+ };
 
- var substitutions = new Dictionary<IVariable, Expression>() {
- { var.BoundVar, new IdentifierExpr(var.BoundVar.Tok, caseLocal)}
+ var substitutions = new Dictionary<IVariable, IVariable>() {
+ { var.BoundVar, caseLocal }
  };
 
  var cloner = new SubstitutingCloner(substitutions, true);

Source/DafnyCore/Resolver/ExpressionTester.cs

@@ -7,7 +7,7 @@
 namespace Microsoft.Dafny;
 
 public class ExpressionTester {
- private DafnyOptions options;
+ private readonly DafnyOptions options;
  private bool ReportErrors => reporter != null;
  [CanBeNull] private readonly ErrorReporter reporter; // if null, no errors will be reported
 
@@ -26,25 +26,35 @@ private ExpressionTester([CanBeNull] ModuleResolver resolver, [CanBeNull] ErrorR
  this.options = options;
  }
 
- // Static call to CheckIsCompilable
+ /// <summary>
+ /// Determines whether or not "expr" is compilable, and returns the answer.
+ /// If "resolver" is non-null and "expr" is not compilable, then an error is reported.
+ /// Also, updates various bookkeeping information (see instance method CheckIsCompilable for more details).
+ /// </summary>
  public static bool CheckIsCompilable(DafnyOptions options, [CanBeNull] ModuleResolver resolver, Expression expr, ICodeContext codeContext) {
  return new ExpressionTester(resolver, resolver?.Reporter, options).CheckIsCompilable(expr, codeContext, true);
  }
 
- public static bool CheckIsCompilable(ModuleResolver resolver, ErrorReporter reporter, Expression expr, ICodeContext codeContext) {
- return new ExpressionTester(resolver, reporter, reporter.Options).CheckIsCompilable(expr, codeContext, true);
+ /// <summary>
+ /// Checks that "expr" is compilable and report an error if it is not.
+ /// Also, updates various bookkeeping information (see instance method CheckIsCompilable for more details).
+ /// </summary>
+ public static void CheckIsCompilable(ModuleResolver resolver, ErrorReporter reporter, Expression expr, ICodeContext codeContext) {
+ new ExpressionTester(resolver, reporter, reporter.Options).CheckIsCompilable(expr, codeContext, true);
  }
 
- public void ReportError(ErrorId errorId, Expression e, string msg, params object[] args) {
+ private void ReportError(ErrorId errorId, Expression e, string msg, params object[] args) {
  reporter?.Error(MessageSource.Resolver, errorId, e, msg, args);
  }
 
- public void ReportError(ErrorId errorId, IToken t, string msg, params object[] args) {
+ private void ReportError(ErrorId errorId, IToken t, string msg, params object[] args) {
  reporter?.Error(MessageSource.Resolver, errorId, t, msg, args);
  }
 
  /// <summary>
- /// Checks that "expr" is compilable and reports an error if it is not.
+ /// Determines and returns whether or not "expr" is compilable.
+ /// If it is not, it calls ReportError. (Note, whether or not ReportError reports an error depends on if "reporter" is non-null.)
+ ///
  /// Also, updates bookkeeping information for the verifier to record the fact that "expr" is to be compiled.
  /// For example, this bookkeeping information keeps track of if the constraint of a let-such-that expression
  /// must determine the value uniquely.
@@ -219,23 +229,21 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext, bool i
  } else if (expr is LetExpr letExpr) {
  if (letExpr.Exact) {
  Contract.Assert(letExpr.LHSs.Count == letExpr.RHSs.Count);
- var i = 0;
- foreach (var ee in letExpr.RHSs) {
+ for (var i = 0; i < letExpr.RHSs.Count; i++) {
+  var rhs = letExpr.RHSs[i];
  var lhs = letExpr.LHSs[i];
  // Make LHS vars ghost if the RHS is a ghost
- if (UsesSpecFeatures(ee)) {
+ if (UsesSpecFeatures(rhs)) {
  foreach (var bv in lhs.Vars) {
  if (!bv.IsGhost) {
  bv.MakeGhost();
- isCompilable = false;
  }
  }
  }
 
  if (!lhs.Vars.All(bv => bv.IsGhost)) {
- isCompilable = CheckIsCompilable(ee, codeContext) && isCompilable;
+ isCompilable = CheckIsCompilable(rhs, codeContext) && isCompilable;
  }
- i++;
  }
  isCompilable = CheckIsCompilable(letExpr.Body, codeContext, insideBranchesOnly) && isCompilable;
  } else {
@@ -247,13 +255,19 @@ private bool CheckIsCompilable(Expression expr, ICodeContext codeContext, bool i
  isCompilable = CheckIsCompilable(letExpr.Body, codeContext, insideBranchesOnly) && isCompilable;
 
  // fill in bounds for this to-be-compiled let-such-that expression
- Contract.Assert(letExpr.RHSs.Count == 1);  // if we got this far, the resolver will have checked this condition successfully
+ Contract.Assert(letExpr.RHSs.Count == 1); // if we got this far, the resolver will have checked this condition successfully
  var constraint = letExpr.RHSs[0];
  if (resolver != null) {
  letExpr.Constraint_Bounds = ModuleResolver.DiscoverBestBounds_MultipleVars(letExpr.BoundVars.ToList<IVariable>(), constraint, true);
  }
  }
  return isCompilable;
+
+ } else if (expr is NestedMatchExpr nestedMatchExpr) {
+ foreach (var kase in nestedMatchExpr.Cases) {
+ MakeGhostAsNeeded(kase.Pat, false);
+ }
+
  } else if (expr is LambdaExpr lambdaExpr) {
  return CheckIsCompilable(lambdaExpr.Body, codeContext);
  } else if (expr is ComprehensionExpr comprehensionExpr) {
@@ -653,6 +667,30 @@ static void MakeGhostAsNeeded(CasePattern<BoundVar> arg, DatatypeDestructor d) {
  }
  }
 
+ public static void MakeGhostAsNeeded(ExtendedPattern extendedPattern, bool inGhostContext) {
+ if (extendedPattern is DisjunctivePattern disjunctivePattern) {
+ foreach (var alternative in disjunctivePattern.Alternatives) {
+ MakeGhostAsNeeded(alternative, inGhostContext);
+ }
+ } else if (extendedPattern is LitPattern) {
+ // nothing to do
+ } else if (extendedPattern is IdPattern idPattern) {
+ if (idPattern.BoundVar != null) {
+ if (inGhostContext && !idPattern.BoundVar.IsGhost) {
+ idPattern.BoundVar.MakeGhost();
+ }
+ } else if (idPattern.Ctor != null) {
+ var argumentCount = idPattern.Ctor.Formals.Count;
+ Contract.Assert(argumentCount == (idPattern.Arguments?.Count ?? 0));
+ for (var i = 0; i < argumentCount; i++) {
+ MakeGhostAsNeeded(idPattern.Arguments[i], inGhostContext || idPattern.Ctor.Formals[i].IsGhost);
+ }
+ }
+ } else {
+ Contract.Assert(false); // unexpected ExtendedPattern
+ }
+ }
+
  /// <summary>
  /// Return the first ghost constructor listed in a case, or null, if there is none.
  /// </summary>

Source/DafnyCore/Resolver/GhostInterestVisitor.cs

@@ -448,6 +448,10 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC
  .OfType<IdPattern>().Any(idPattern => idPattern.Ctor != null && idPattern.Ctor.IsGhost);
  nestedMatchStmt.IsGhost = mustBeErasable || ExpressionTester.UsesSpecFeatures(nestedMatchStmt.Source) || hasGhostPattern;
 
+ foreach (var kase in nestedMatchStmt.Cases) {
+ ExpressionTester.MakeGhostAsNeeded(kase.Pat, nestedMatchStmt.IsGhost);
+ }
+
  if (!mustBeErasable && nestedMatchStmt.IsGhost) {
  reporter.Info(MessageSource.Resolver, nestedMatchStmt.Tok, "ghost match");
  }

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -3040,7 +3040,7 @@ public void CheckIsLvalue(Expression lhs, ResolutionContext resolutionContext) {
  ConstrainSubtypeRelation(ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy(), resolutionContext, true), ll.Seq.Type, ll.Seq,
  "LHS of array assignment must denote an array element (found {0})", ll.Seq.Type);
  if (!ll.SelectOne) {
- reporter.Error(MessageSource.Resolver, ll.Seq, "cannot assign to a range of array elements (try the 'forall' statement)");
+ reporter.Error(MessageSource.Resolver, ll, "cannot assign to a range of array elements (try the 'forall' statement)");
  }
  } else if (lhs is MultiSelectExpr) {
  // nothing to check; this can only denote an array element

Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs

@@ -49,7 +49,10 @@ public DPreType ApproximateReceiverType(PreType preType, [CanBeNull] string memb
  if (preType is DPreType dPreType) {
  return dPreType;
  }
- var proxy = (PreTypeProxy)preType;
+ if (preType is not PreTypeProxy proxy) {
+ // preType could be a PreTypePlaceholder, resulting from an error somewhere
+ return null;
+ }
 
  var approximateReceiverType = ApproximateReceiverTypeViaBounds(proxy, memberName, out var subProxies);
  if (approximateReceiverType != null) {

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -162,21 +162,21 @@ public void ResolveExpression(Expression expr, ResolutionContext resolutionConte
 
  if (e.PreType is PreTypePlaceholderModule) {
  ReportError(e.tok, "name of module ({0}) is used as a variable", e.Name);
- e.ResetTypeAssignment(); // the rest of type checking assumes actual types
+ ResetTypeAssignment(e); // the rest of type checking assumes actual types
  } else if (e.PreType is PreTypePlaceholderType) {
  ReportError(e.tok, "name of type ({0}) is used as a variable", e.Name);
- e.ResetTypeAssignment(); // the rest of type checking assumes actual types
+ ResetTypeAssignment(e); // the rest of type checking assumes actual types
  }
 
  } else if (expr is ExprDotName) {
  var e = (ExprDotName)expr;
  ResolveDotSuffix(e, true, null, resolutionContext, false);
  if (e.PreType is PreTypePlaceholderModule) {
  ReportError(e.tok, "name of module ({0}) is used as a variable", e.SuffixName);
- e.ResetTypeAssignment(); // the rest of type checking assumes actual types
+ ResetTypeAssignment(e); // the rest of type checking assumes actual types
  } else if (e.PreType is PreTypePlaceholderType) {
  ReportError(e.tok, "name of type ({0}) is used as a variable", e.SuffixName);
- e.ResetTypeAssignment(); // the rest of type checking assumes actual types
+ ResetTypeAssignment(e); // the rest of type checking assumes actual types
  }
 
  } else if (expr is ApplySuffix applySuffix) {
@@ -282,9 +282,9 @@ public void ResolveExpression(Expression expr, ResolutionContext resolutionConte
  var familyDeclName = ancestorPreType?.Decl.Name;
  if (familyDeclName == PreType.TypeNameSeq) {
  var elementPreType = ancestorPreType.Arguments[0];
- ConstrainToIntFamilyOrBitvector(e.Index.PreType, e.Index.tok, "sequence update requires integer- or bitvector-based index (got {0})");
+ ConstrainToIntFamilyOrBitvector(e.Index.PreType, e.Index.tok, "sequence update requires integer- or bitvector-based index (got {1})");
  AddSubtypeConstraint(elementPreType, e.Value.PreType, e.Value.tok,
- "sequence update requires the value to have the element type of the sequence (got {0})");
+ "sequence update requires the value to have the element type of the sequence (got {1})");
  return true;
  } else if (familyDeclName is PreType.TypeNameMap or PreType.TypeNameImap) {
  var domainPreType = ancestorPreType.Arguments[0];

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs

@@ -544,7 +544,9 @@ private void ResolveCalc(CalcStmt s, ResolutionContext resolutionContext) {
 #if SOON
  // reuse the error object if we're on the dummy line; this prevents a duplicate error message
 #endif
- AddSubtypeConstraint(linePreType, e1.PreType, e1.tok, "all lines in a calculation must have the same type (got {1} after {0})");
+ if (i < s.Lines.Count - 1) {
+ AddSubtypeConstraint(linePreType, e1.PreType, e1.tok, "all lines in a calculation must have the same type (got {1} after {0})");
+ }
  var step = (s.StepOps[i - 1] ?? s.Op).StepExpr(e0, e1); // Use custom line operator
  ResolveExpression(step, resolutionContext);
  s.Steps.Add(step);
@@ -1308,7 +1310,7 @@ public void CheckIsLvalue(Expression lhs, ResolutionContext resolutionContext) {
  var arrayType = resolver.ResolvedArrayType(ll.Seq.tok, 1, new InferredTypeProxy(), resolutionContext, true);
  AddSubtypeConstraint(Type2PreType(arrayType), ll.Seq.PreType, ll.Seq.tok, "LHS of array assignment must denote an array element (found {1})");
  if (!ll.SelectOne) {
- ReportError(ll.Seq, "cannot assign to a range of array elements (try the 'forall' statement)");
+ ReportError(ll, "cannot assign to a range of array elements (try the 'forall' statement)");
  }
  } else if (lhs is MultiSelectExpr) {
  // nothing to check; this can only denote an array element

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

@@ -174,6 +174,15 @@ public PreType CreatePreTypeProxy(string description = null) {
  return proxy;
  }
 
+ /// <summary>
+ /// This method can be used when .PreType has been found to be erroneous and its current value
+ /// would be unexpected by the rest of the resolver. This method then sets .Type and .PreType to neutral values.
+ /// </summary>
+ void ResetTypeAssignment(Expression expr) {
+ expr.PreType = CreatePreTypeProxy();
+ expr.ResetTypeAssignment();
+ }
+
  public enum Type2PreTypeOption { GoodForInference, GoodForPrinting, GoodForBoth }
 
  public PreType Type2PreType(Type type, string description = null, Type2PreTypeOption option = Type2PreTypeOption.GoodForBoth) {
@@ -884,14 +893,14 @@ void ComputePreTypeMethod(Method method) {
  // bitvector types. That's now handled in a different way, which does not use SelfType.
  } else {
  ComputePreTypeFunction(function);
- if (function is ExtremePredicate extremePredicate) {
- ComputePreTypeFunction(extremePredicate.PrefixPredicate);
+ if (function is ExtremePredicate { PrefixPredicate: { } prefixPredicate }) {
+ ComputePreTypeFunction(prefixPredicate);
  }
  }
  } else if (declaration is Method method) {
  ComputePreTypeMethod(method);
- if (method is ExtremeLemma extremeLemma) {
- ComputePreTypeMethod(extremeLemma.PrefixLemma);
+ if (method is ExtremeLemma { PrefixLemma: { } prefixLemma }) {
+ ComputePreTypeMethod(prefixLemma);
  }
  } else {
  Contract.Assert(false); // unexpected declaration

Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs

@@ -143,8 +143,8 @@ private void CheckMember(MemberDecl member) {
  CheckStatement(method.Body, context);
  }
  if (errorCount == ErrorCount) {
- if (method is ExtremeLemma extremeLemma) {
- CheckMember(extremeLemma.PrefixLemma);
+ if (method is ExtremeLemma { PrefixLemma: { } prefixLemma }) {
+ CheckMember(prefixLemma);
  }
  }
 
@@ -158,8 +158,8 @@ private void CheckMember(MemberDecl member) {
  CheckExpression(function.Body, context);
  }
  if (errorCount == ErrorCount) {
- if (function is ExtremePredicate extremePredicate) {
- CheckMember(extremePredicate.PrefixPredicate);
+ if (function is ExtremePredicate { PrefixPredicate: { } prefixPredicate }) {
+ CheckMember(prefixPredicate);
  } else if (function.ByMethodDecl != null) {
  CheckMember(function.ByMethodDecl);
  }