Log an error instead of crashing in FindTokenRangeFromLspRange (#4869)

Fixes #4818

### How has this been tested?
Not. There's no known reproduction for the issue. This change uses
defensive coding to reduce the chance of a crash

<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/DafnyLanguageServer/Handlers/DafnyCodeActionHandler.cs

@@ -88,9 +88,9 @@ public override async Task<CommandOrCodeActionContainer> Handle(CodeActionParams
 
  private DafnyCodeActionProvider[] GetDafnyCodeActionProviders() {
  return new List<DafnyCodeActionProvider>() {
- new VerificationDafnyCodeActionProvider()
- , new ErrorMessageDafnyCodeActionProvider()
- , new ImplicitFailingAssertionCodeActionProvider(options)
+ new VerificationDafnyCodeActionProvider(logger)
+ , new ErrorMessageDafnyCodeActionProvider(logger)
+ , new ImplicitFailingAssertionCodeActionProvider(logger, options)
  }
  .Concat(
  options.Plugins.SelectMany(plugin =>

Source/DafnyLanguageServer/Language/ErrorMessageDafnyCodeActionProvider.cs

@@ -1,8 +1,10 @@
 using System.Collections.Generic;
 using System.Linq;
+using Microsoft.Dafny.LanguageServer.Handlers;
 using Microsoft.Dafny.LanguageServer.Plugins;
 using Microsoft.Dafny.LanguageServer.Util;
 using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
@@ -18,6 +20,9 @@ public class ErrorMessageDafnyCodeActionProvider : DiagnosticDafnyCodeActionProv
  var actions = new List<DafnyCodeAction>();
  if (actionSigs != null) {
  var range = FindTokenRangeFromLspRange(input, diagnostic.Range);
+ if (range == null) {
+ return actions;
+ }
  foreach (var sig in actionSigs) {
  var dafnyActions = sig(range);
  actions.AddRange(dafnyActions.Select(dafnyAction => new InstantDafnyCodeAction(dafnyAction.Title, new[] { diagnostic }, dafnyAction.Edits)));
@@ -26,13 +31,6 @@ public class ErrorMessageDafnyCodeActionProvider : DiagnosticDafnyCodeActionProv
  return actions;
  }
 
- public static RangeToken FindTokenRangeFromLspRange(IDafnyCodeActionInput input, Range range) {
- var start = range.Start;
- var startNode = input.Program.FindNode<Node>(input.Uri.ToUri(), start.ToDafnyPosition());
- var startToken = startNode.CoveredTokens.First(t => t.line - 1 == start.Line && t.col - 1 == start.Character);
- var end = range.End;
- var endNode = input.Program.FindNode<Node>(input.Uri.ToUri(), end.ToDafnyPosition());
- var endToken = endNode.CoveredTokens.FirstOrDefault(t => t.line - 1 == end.Line && t.col - 1 + t.val.Length == end.Character);
- return new RangeToken(startToken, endToken);
+ public ErrorMessageDafnyCodeActionProvider(ILogger<DafnyCodeActionHandler> logger) : base(logger) {
  }
 }

Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs

@@ -2,9 +2,11 @@
 using System.Collections.Generic;
 using System.Linq;
 using JetBrains.Annotations;
+using Microsoft.Dafny.LanguageServer.Handlers;
 using Microsoft.Dafny.LanguageServer.Plugins;
 using Microsoft.Dafny.LanguageServer.Workspace;
 using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
@@ -16,9 +18,9 @@ namespace Microsoft.Dafny.LanguageServer.Language;
 /// indicated on the '{' -- meaning there is no explicit return.
 /// </summary>
 class ImplicitFailingAssertionCodeActionProvider : DiagnosticDafnyCodeActionProvider {
- private DafnyOptions options;
+ private readonly DafnyOptions options;
 
- public ImplicitFailingAssertionCodeActionProvider(DafnyOptions options) {
+ public ImplicitFailingAssertionCodeActionProvider(ILogger<DafnyCodeActionHandler> logger, DafnyOptions options) : base(logger) {
  this.options = options;
  }
 

Source/DafnyLanguageServer/Language/VerificationDafnyCodeActionProvider.cs

@@ -1,8 +1,10 @@
 using System;
 using System.Collections.Generic;
 using System.Linq;
+using Microsoft.Dafny.LanguageServer.Handlers;
 using Microsoft.Dafny.LanguageServer.Plugins;
 using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
@@ -29,7 +31,10 @@ class VerificationDafnyCodeActionProvider : DiagnosticDafnyCodeActionProvider {
  return null;
  }
 
- var range = ErrorMessageDafnyCodeActionProvider.FindTokenRangeFromLspRange(input, relatedInformation.Location.Range);
+ var range = FindTokenRangeFromLspRange(input, relatedInformation.Location.Range);
+ if (range == null) {
+ return null;
+ }
  var expression = range.PrintOriginal();
  var statement = $"assert {expression};";
  var edit = DafnyCodeActionHelpers.InsertAtEndOfBlock(input, diagnostic.Range.Start, statement);
@@ -46,4 +51,7 @@ class VerificationDafnyCodeActionProvider : DiagnosticDafnyCodeActionProvider {
  };
 
  }
+
+ public VerificationDafnyCodeActionProvider(ILogger<DafnyCodeActionHandler> logger) : base(logger) {
+ }
 }

Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs

@@ -1,5 +1,9 @@
 using System.Collections.Generic;
+using System.Linq;
+using Microsoft.Dafny.LanguageServer.Handlers;
 using Microsoft.Dafny.LanguageServer.Language;
+using Microsoft.Dafny.LanguageServer.Util;
+using Microsoft.Extensions.Logging;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
@@ -45,6 +49,12 @@ protected static RangeToken InsertAfter(IToken tok) {
 /// that are being touched by the selection
 /// </summary>
 public abstract class DiagnosticDafnyCodeActionProvider : DafnyCodeActionProvider {
+ private ILogger<DafnyCodeActionHandler> logger;
+
+ protected DiagnosticDafnyCodeActionProvider(ILogger<DafnyCodeActionHandler> logger) {
+ this.logger = logger;
+ }
+
  public override IEnumerable<DafnyCodeAction> GetDafnyCodeActions(IDafnyCodeActionInput input, Range selection) {
  if (input.Program == null) {
  return System.Array.Empty<DafnyCodeAction>();
@@ -74,4 +84,18 @@ public override IEnumerable<DafnyCodeAction> GetDafnyCodeActions(IDafnyCodeActio
  /// <param name="selection">Where the user's caret is</param>
  protected abstract IEnumerable<DafnyCodeAction>? GetDafnyCodeActions(IDafnyCodeActionInput input,
  Diagnostic diagnostic, Range selection);
+
+ public RangeToken? FindTokenRangeFromLspRange(IDafnyCodeActionInput input, Range range) {
+ var start = range.Start;
+ var startNode = input.Program.FindNode<Node>(input.Uri.ToUri(), start.ToDafnyPosition());
+ var startToken = startNode.CoveredTokens.FirstOrDefault(t => t.line - 1 == start.Line && t.col - 1 == start.Character);
+ if (startToken == null) {
+ logger.LogError($"Could not find starting token for position {start} in node {startNode}");
+ return null;
+ }
+ var end = range.End;
+ var endNode = input.Program.FindNode<Node>(input.Uri.ToUri(), end.ToDafnyPosition());
+ var endToken = endNode.CoveredTokens.FirstOrDefault(t => t.line - 1 == end.Line && t.col - 1 + t.val.Length == end.Character);
+ return new RangeToken(startToken, endToken);
+ }
 }

docs/dev/news/4818.fix

@@ -0,0 +1 @@
+Use defensive coding to prevent a crash in the IDE that could occur in the context of code actions.