From 5ad2413289644c7f78e75ffb30480bccdfce4014 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Mon, 10 Jun 2024 16:51:38 +0200
Subject: [PATCH] Fix null ref in covered tokens (#5548)

Fixes #5355

### Description
- Fix null reference exception that occurred when looking at the tokens
of a generated node

### How has this been tested?
- Add LSP 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>
---
 Source/DafnyCore/AST/Members/Function.cs      |  1 -
 Source/DafnyCore/AST/Members/Method.cs        |  1 -
 .../DafnyCore/AST/Members/MethodOrFunction.cs |  6 +---
 Source/DafnyCore/Generic/Node.cs              |  3 ++
 .../CodeActions/CodeActionsTest.cs            | 36 +++++++++++++++++++
 5 files changed, 40 insertions(+), 7 deletions(-)

diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs
index 53aad21edb5..7a901fe1917 100644
--- a/Source/DafnyCore/AST/Members/Function.cs
+++ b/Source/DafnyCore/AST/Members/Function.cs
@@ -96,7 +96,6 @@ public TailStatus
   public readonly Formal Result;
   public PreType ResultPreType;
   public readonly Type ResultType;
-  public readonly Specification<FrameExpression> Reads;
   public Expression Body; // an extended expression; Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution
   public IToken /*?*/ ByMethodTok; // null iff ByMethodBody is null
   public BlockStmt /*?*/ ByMethodBody;
diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs
index 5a45db2a28d..ff275773731 100644
--- a/Source/DafnyCore/AST/Members/Method.cs
+++ b/Source/DafnyCore/AST/Members/Method.cs
@@ -36,7 +36,6 @@ static Method() {
   public bool MustReverify;
   public bool IsEntryPoint = false;
   public readonly List<Formal> Outs;
-  public readonly Specification<FrameExpression> Reads;
   public readonly Specification<FrameExpression> Mod;
   [FilledInDuringResolution] public bool IsRecursive;
   [FilledInDuringResolution] public bool IsTailRecursive;
diff --git a/Source/DafnyCore/AST/Members/MethodOrFunction.cs b/Source/DafnyCore/AST/Members/MethodOrFunction.cs
index 87fa7f263e2..ea5b76dd09f 100644
--- a/Source/DafnyCore/AST/Members/MethodOrFunction.cs
+++ b/Source/DafnyCore/AST/Members/MethodOrFunction.cs
@@ -93,9 +93,5 @@ public void ResolveMethodOrFunction(INewOrOldResolver resolver) {
   protected MethodOrFunction(RangeToken tok, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining) : base(tok, name, hasStaticKeyword, isGhost, attributes, isRefining) {
   }
 
-  public Specification<FrameExpression> Reads => this switch {
-    Method m => m.Reads,
-    Function f => f.Reads,
-    _ => throw new cce.UnreachableException()
-  };
+  public Specification<FrameExpression> Reads { get; set; }
 }
\ No newline at end of file
diff --git a/Source/DafnyCore/Generic/Node.cs b/Source/DafnyCore/Generic/Node.cs
index 8af38a147e8..62e982d174c 100644
--- a/Source/DafnyCore/Generic/Node.cs
+++ b/Source/DafnyCore/Generic/Node.cs
@@ -56,6 +56,9 @@ public abstract class Node : INode {
   public IEnumerable<IToken> CoveredTokens {
     get {
       var token = StartToken;
+      if (token == Token.NoToken) {
+        yield break;
+      }
       while (token.Prev != EndToken) {
         yield return token;
         token = token.Next;
diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs
index 3f23530cf1b..c2a8b8162a1 100644
--- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs
+++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs
@@ -40,6 +40,42 @@ public async Task MethodKeywordCodeAction() {
       Assert.Empty(completionList);
     }
 
+    [Fact]
+    public async Task TypeTestCodeAction() {
+      await SetUp(o => o.Set(CommonOptionBag.RelaxDefiniteAssignment, true));
+
+      MarkupTestFile.GetPositionsAndAnnotatedRanges(@"module M {
+  trait Object {
+   ghost function typeId() : (id: string)
+  }
+
+  type A extends Object {
+   ghost function typeId() : (id: string)  { ""A"" }
+  }
+
+  type B extends Object {
+   ghost function typeId() : (id: string)  { ""B"" }
+  }
+  type C extends Object {
+   ghost function typeId() : (id: string)  { ""C"" }
+  }
+
+  lemma test(x: Object)
+    ensures multiset{x is A, x is B, x is C}[true] == 1
+  {
+    var _ := x.typeId();
+    if (x is A) {
+      assert x !is B.><
+    }
+  }
+}".TrimStart(), out var source, out var positions,
+        out var ranges);
+      var documentItem = await CreateOpenAndWaitForResolve(source);
+      var position = positions[0];
+      var completionList = await RequestCodeActionAsync(documentItem, new Range(position, position));
+      Assert.Empty(completionList);
+    }
+
     [Fact]
     public async Task GitIssue4401CorrectInsertionPlace() {
       await TestCodeAction(@"