Fix: Optional pre-type won't cause a crash anymore (#5442)

This PR fixes #5369
I added the corresponding test.


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

---------

Co-authored-by: Remy Willems <[email protected]>

Source/DafnyCore/Resolver/PreType/PreType.cs

@@ -455,10 +455,13 @@ public class PreTypePlaceholderModule : PreTypePlaceholder {
  public class PreTypePlaceholderType : PreTypePlaceholder {
  }
 
- public class UnusedPreType : PreTypePlaceholder {
+ /// Used for assigning a pre-type to MemberSelect expressions, such as "obj.method",
+ /// which is not considered an expression. This indicates that resolution has occurred,
+ /// even though the pre-type itself is not useful.
+ public class MethodPreType : PreTypePlaceholder {
  public readonly string Why;
 
- public UnusedPreType(string why) {
+ public MethodPreType(string why) {
  Why = why;
  }
 

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

@@ -1591,6 +1591,7 @@ public partial class PreTypeResolver {
  if (!allowMethodCall) {
  // it's a method and method calls are not allowed in the given resolutionContext
  ReportError(tok, "expression is not allowed to invoke a {0} ({1})", member.WhatKind, member.Name);
+ return null;
  }
  int suppliedTypeArguments = optTypeArguments == null ? 0 : optTypeArguments.Count;
  if (optTypeArguments != null) {
@@ -1608,7 +1609,7 @@ public partial class PreTypeResolver {
  rr.PreTypeApplication_JustMember.Add(ta);
  subst.Add(method.TypeArgs[i], ta);
  }
- rr.PreType = new UnusedPreType($"call to {method.WhatKind} {method.Name}"); // fill in this field, in order to make "rr" resolved
+ rr.PreType = new MethodPreType($"call to {method.WhatKind} {method.Name}"); // fill in this field, in order to make "rr" resolved
  }
  return rr;
  }

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

@@ -1590,7 +1590,7 @@ class PreTypeSanityChecker : BottomUpVisitor {
  preTypeResolver.ReportError(expr.tok, $"SANITY CHECK FAILED: .PreType is '{expr.PreType}' but .Type is null");
  } else if (PreType.Same(expr.PreType, preTypeResolver.Type2PreType(expr.Type))) {
  // all is cool
- } else if (expr.PreType is UnusedPreType && expr.Type is TypeProxy) {
+ } else if (expr.PreType is MethodPreType && expr.Type is TypeProxy) {
  // this is expected
  } else {
  preTypeResolver.ReportError(expr.tok, $"SANITY CHECK FAILED: pre-type '{expr.PreType}' does not correspond to type '{expr.Type}'");

Source/DafnyCore/Resolver/PreType/PreTypeToType.cs

@@ -140,7 +140,7 @@ class PreTypeToTypeVisitor : ASTVisitor<IASTVisitorContext> {
  return;
  }
 
- if (expr.PreType is UnusedPreType) {
+ if (expr.PreType is MethodPreType) {
  expr.Type = new InferredTypeProxy();
  return;
  }

Source/DafnyCore/Resolver/ResolutionContext.cs

@@ -36,6 +36,6 @@ public ResolutionContext(ICodeContext codeContext, bool isTwoState)
  if (CodeContext.IsGhost == isGhost) {
  return this;
  }
- return new ResolutionContext(new CodeContextWrapper(CodeContext, isGhost), IsTwoState, InOld, InReveal, InFunctionPostcondition, InFirstPhaseConstructor);
+ return this with { CodeContext = new CodeContextWrapper(CodeContext, isGhost) };
  }
 }

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5369.dfy

@@ -0,0 +1,43 @@
+// RUN: %exits-with 2 %baredafny verify %args --type-system-refresh "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+ghost function f2(items: set<nat>): (r:nat)
+ requires |items| > 0 {
+ var item :| item in items;
+ item
+}
+
+function f(items: set<nat>) : (r:nat)
+requires |items| > 0 {
+ //assume exists item :: item in items && forall other <- items :: item == other || item < other;
+ //assert exists item Smallest()
+ var item :| IsSmallest(items, item);
+ item
+}
+
+predicate IsSmallest(s: set<nat>, item: nat) 
+ requires item in s {
+ m in s && forall y: nat :: y in s ==> m <= y
+}
+
+lemma Smallest(s: set<nat>) returns (m: nat)
+ requires s != {}
+ ensures m in s && IsSmallest(s, m)
+ decreases s
+{
+ m :| m in s;
+ if y: nat :| y in s && y < m {
+ ghost var s' := s - {m};
+ assert y in s';
+ m := ThereIsASmallest(s');
+ }
+}
+
+function smallest(items: set<nat>): (r: nat)
+ requires |items| > 0
+
+method m(items: set<nat>) returns (r:nat)
+requires |items| > 0 {
+ var item :| item in items;
+ return item;
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5369.dfy.expect

@@ -0,0 +1,4 @@
+git-issue-5369.dfy(20,2): Error: expression is not allowed to invoke a method (m)
+git-issue-5369.dfy(20,40): Error: expression is not allowed to invoke a method (m)
+git-issue-5369.dfy(32,9): Error: unresolved identifier: ThereIsASmallest
+3 resolution/type errors detected in git-issue-5369.dfy

docs/dev/news/5369.fix

@@ -0,0 +1 @@
+Optional pre-type won't cause a crash anymore