Related locations available in Resolver and prints to Console and LSP Diagnostics (#1695)

* Support for messages in nested tokens.
Console printing now displays information in nested tokens coming from the Resolution phase
The Language Server now displays in formation in nested tokens from the resolution phase
No more duplicate messages.

Author: MikaelMayer

Source/Dafny/AST/DafnyAst.cs

@@ -8900,14 +8900,16 @@ public virtual string val {
   }
 
   public class NestedToken : TokenWrapper {
-    public NestedToken(IToken outer, IToken inner)
+    public NestedToken(IToken outer, IToken inner, string message = null)
       : base(outer) {
       Contract.Requires(outer != null);
       Contract.Requires(inner != null);
       Inner = inner;
+      this.Message = message;
     }
     public IToken Outer { get { return WrappedToken; } }
     public readonly IToken Inner;
+    public readonly string Message;
   }
 
   /// <summary>

Source/Dafny/Reporting.cs

@@ -199,7 +199,19 @@ public override bool Message(MessageSource source, ErrorLevel level, IToken tok,
 
         ConsoleColor previousColor = Console.ForegroundColor;
         Console.ForegroundColor = ColorForLevel(level);
-        Console.WriteLine(ErrorToString(level, tok, msg));
+        var errorLine = ErrorToString(level, tok, msg);
+        while (tok is NestedToken nestedToken) {
+          tok = nestedToken.Inner;
+          if (tok.filename == nestedToken.filename &&
+              tok.line == nestedToken.line &&
+              tok.col == nestedToken.col) {
+            continue;
+          }
+          msg = nestedToken.Message ?? "[Related location]";
+          errorLine += $" {msg} {TokenToString(tok)}";
+        }
+        Console.WriteLine(errorLine);
+
         Console.ForegroundColor = previousColor;
         return true;
       } else {

Source/Dafny/Resolver.cs

@@ -18547,6 +18547,25 @@ public bool ContainsDecl(Thing t) {
   // Looks for every non-ghost comprehensions, and if they are using a subset type,
   // check that the subset constraint is compilable. If it is not compilable, raises an error.
   public class SubsetConstraintGhostChecker : ProgramTraverser {
+    public class FirstErrorCollector : ErrorReporter {
+      public string FirstCollectedMessage = "";
+      public IToken FirstCollectedToken = Token.NoToken;
+      public bool Collected = false;
+
+      public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {
+        if (!Collected && level == ErrorLevel.Error) {
+          FirstCollectedMessage = msg;
+          FirstCollectedToken = tok;
+          Collected = true;
+        }
+        return true;
+      }
+
+      public override int Count(ErrorLevel level) {
+        return level == ErrorLevel.Error && Collected ? 1 : 0;
+      }
+    }
+
     public Resolver resolver;
 
     public SubsetConstraintGhostChecker(Resolver resolver) {
@@ -18610,15 +18629,19 @@ public override bool Traverse(Expression expr, [CanBeNull] string field, [CanBeN
             }
 
             if (!constraintIsCompilable) {
-              // Explicitly report the error
-              var showProvenance = constraint.tok.line != 0;
-              this.resolver.Reporter.Error(MessageSource.Resolver, boundVar.tok,
-                $"{boundVar.Type} is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in {what}." +
-                (showProvenance ? " The next error will explain why the constraint is not compilable." : ""));
-              if (showProvenance) {
-                ExpressionTester.CheckIsCompilable(this.resolver, constraint,
+              IToken finalToken = boundVar.tok;
+              if (constraint.tok.line != 0) {
+                var errorCollector = new FirstErrorCollector();
+                ExpressionTester.CheckIsCompilable(this.resolver, errorCollector, constraint,
                   new CodeContextWrapper(subsetTypeDecl, true));
+                if (errorCollector.Collected) {
+                  finalToken = new NestedToken(finalToken, errorCollector.FirstCollectedToken,
+                    "The constraint is not compilable because " + errorCollector.FirstCollectedMessage
+                  );
+                }
               }
+              this.resolver.Reporter.Error(MessageSource.Resolver, finalToken,
+                $"{boundVar.Type} is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in {what}.");
             }
           }
         }

Source/Dafny/Triggers/QuantifiersCollection.cs

@@ -285,10 +285,18 @@ private void CommitOne(QuantifierWithTriggers q, bool addHeader) {
       var msg = new StringBuilder();
       var indent = addHeader ? "  " : "";
       bool suppressWarnings = Attributes.Contains(q.quantifier.Attributes, "nowarn");
+      var reportingToken = q.quantifier.tok;
+
+      void SetRelatedLocationMessage(string msg) {
+        if (reportingToken is NestedToken nestedToken) {
+          reportingToken = new NestedToken(nestedToken.Outer, nestedToken.Inner, msg);
+        }
+      }
 
       if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: split and autotriggers attributes are passed down to Boogie
         var extraMsg = TriggerUtils.WantsAutoTriggers(q.quantifier) ? "" : " Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.";
         msg.AppendFormat("Not generating triggers for \"{0}\".{1}", Printer.ExprToString(q.quantifier.Term), extraMsg).AppendLine();
+        SetRelatedLocationMessage("Trigger position:");
       } else {
         if (addHeader) {
           msg.AppendFormat("For expression \"{0}\":", Printer.ExprToString(q.quantifier.Term)).AppendLine();
@@ -299,32 +307,42 @@ private void CommitOne(QuantifierWithTriggers q, bool addHeader) {
         }
 
         AddTriggersToMessage("Selected triggers:", q.Candidates, msg, indent);
+        if (q.Candidates.Count > 0) {
+          SetRelatedLocationMessage("Trigger position:");
+        }
         AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);
+        if (q.RejectedCandidates.Count > 0 && q.Candidates.Count == 0) {
+          SetRelatedLocationMessage("Rejected trigger position:");
+        }
 
 #if QUANTIFIER_WARNINGS
-        var WARN_TAG = DafnyOptions.O.UnicodeOutput ? "⚠ " : "/!\\ ";
+        var WARN_TAG = DafnyOptions.O.UnicodeOutput ? "⚠ " : @"/!\ ";
         var WARN_TAG_OVERRIDE = suppressWarnings ? "(Suppressed warning) " : WARN_TAG;
         var WARN_LEVEL = suppressWarnings ? ErrorLevel.Info : ErrorLevel.Warning;
         var WARN = indent + WARN_TAG_OVERRIDE;
         if (!q.CandidateTerms.Any()) {
           errorLevel = WARN_LEVEL;
           msg.Append(WARN).AppendLine("No terms found to trigger on.");
+          SetRelatedLocationMessage("Potential trigger not suitable:");
         } else if (!q.Candidates.Any()) {
           errorLevel = WARN_LEVEL;
           msg.Append(WARN).AppendLine("No trigger covering all quantified variables found.");
+          SetRelatedLocationMessage("Potential trigger not suitable:");
         } else if (!q.CouldSuppressLoops && !q.AllowsLoops) {
           errorLevel = WARN_LEVEL;
           msg.Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers.");
+          SetRelatedLocationMessage("Trigger position:");
         } else if (suppressWarnings) {
           errorLevel = ErrorLevel.Warning;
           msg.Append(indent).Append(WARN_TAG).AppendLine("There is no warning here to suppress.");
+          SetRelatedLocationMessage("Trigger position:");
         }
 #endif
       }
 
       if (msg.Length > 0) {
         var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray());
-        reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr);
+        reporter.Message(MessageSource.Rewriter, errorLevel, reportingToken, msgStr);
       }
     }
 

Source/Dafny/Util.cs

@@ -757,20 +757,25 @@ public class ExpressionTester {
     private ErrorReporter reporter = null;
     private Resolver resolver = null;
 
-    public ExpressionTester(Resolver resolver = null, bool reportErrors = false) {
-      Contract.Requires(reportErrors == false || resolver != null);
-      if (resolver != null) {
-        this.reporter = resolver.Reporter;
-        this.resolver = resolver;
-      }
+    public ExpressionTester(Resolver resolver = null, bool reportErrors = false) :
+      this(resolver, resolver?.Reporter, reportErrors) {
+    }
 
+    public ExpressionTester(Resolver resolver, ErrorReporter reporter, bool reportErrors = false) {
+      Contract.Requires(reportErrors == false || resolver != null);
+      this.resolver = resolver;
+      this.reporter = reporter;
       this.reportErrors = reportErrors;
     }
 
     // Static call to CheckIsCompilable
     public static bool CheckIsCompilable(Resolver resolver, Expression expr, ICodeContext codeContext) {
       return new ExpressionTester(resolver, resolver != null).CheckIsCompilable(expr, codeContext);
     }
+    // Static call to CheckIsCompilable
+    public static bool CheckIsCompilable(Resolver resolver, ErrorReporter reporter, Expression expr, ICodeContext codeContext) {
+      return new ExpressionTester(resolver, reporter, resolver != null).CheckIsCompilable(expr, codeContext);
+    }
 
     /// <summary>
     /// Try to make "expr" compilable (in particular, mark LHSs of a let-expression as ghosts if

Source/DafnyLanguageServer/Language/DiagnosticErrorReporter.cs

@@ -93,12 +93,19 @@ public override bool Message(MessageSource source, ErrorLevel level, IToken tok,
       if (ErrorsOnly && level != ErrorLevel.Error) {
         return false;
       }
-
+      var relatedInformation = new List<DiagnosticRelatedInformation>();
+      if (tok is NestedToken nestedToken) {
+        relatedInformation.AddRange(
+          CreateDiagnosticRelatedInformationFor(
+            nestedToken.Inner, nestedToken.Message ?? "Related location")
+        );
+      }
       var item = new Diagnostic {
         Severity = ToSeverity(level),
         Message = msg,
         Range = tok.GetLspRange(),
-        Source = source.ToString()
+        Source = source.ToString(),
+        RelatedInformation = relatedInformation,
       };
       AddDiagnosticForFile(item, GetDocumentUriOrDefault(tok));
       return true;

Test/allocated1/dafny0/DiscoverBounds.dfy.expect

@@ -1,8 +1,8 @@
-DiscoverBounds.dfy(32,7): Warning: /!\ No terms found to trigger on.
-DiscoverBounds.dfy(33,7): Warning: /!\ No terms found to trigger on.
-DiscoverBounds.dfy(34,7): Warning: /!\ No terms found to trigger on.
-DiscoverBounds.dfy(35,7): Warning: /!\ No terms found to trigger on.
-DiscoverBounds.dfy(36,7): Warning: /!\ No terms found to trigger on.
+DiscoverBounds.dfy(32,7): Warning: /!\ No terms found to trigger on. Potential trigger not suitable: DiscoverBounds.dfy(32,33)
+DiscoverBounds.dfy(33,7): Warning: /!\ No terms found to trigger on. Potential trigger not suitable: DiscoverBounds.dfy(33,33)
+DiscoverBounds.dfy(34,7): Warning: /!\ No terms found to trigger on. Potential trigger not suitable: DiscoverBounds.dfy(34,36)
+DiscoverBounds.dfy(35,7): Warning: /!\ No terms found to trigger on. Potential trigger not suitable: DiscoverBounds.dfy(35,39)
+DiscoverBounds.dfy(36,7): Warning: /!\ No terms found to trigger on. Potential trigger not suitable: DiscoverBounds.dfy(36,42)
 
 Dafny program verifier finished with 7 verified, 0 errors
 0

Test/allocated1/dafny0/InSetComprehension.dfy.expect

@@ -11,7 +11,7 @@ InSetComprehension.dfy(39,16): Info: Not generating triggers for "Id(u)". Note t
 InSetComprehension.dfy(76,13): Info: Selected triggers: {x in si}
 InSetComprehension.dfy(78,13): Info: Selected triggers: {y in ti}
 InSetComprehension.dfy(81,13): Info: Selected triggers: {n in si}
-InSetComprehension.dfy(82,5): Info: Selected triggers: {si[i]}
+InSetComprehension.dfy(82,5): Info: Selected triggers: {si[i]} Trigger position: InSetComprehension.dfy(82,37)
 InSetComprehension.dfy(53,24): Info: Selected triggers: {x in elems}
 InSetComprehension.dfy(51,25): Info: Selected triggers: {x in elems}
 InSetComprehension.dfy(67,24): Info: Selected triggers: {x in elems}

Test/allocated1/dafny0/LetExpr.dfy.expect

@@ -1,5 +1,5 @@
-LetExpr.dfy(45,2): Warning: /!\ No terms found to trigger on.
-LetExpr.dfy(206,4): Warning: /!\ No terms found to trigger on.
+LetExpr.dfy(45,2): Warning: /!\ No terms found to trigger on. Potential trigger not suitable: LetExpr.dfy(45,39)
+LetExpr.dfy(206,4): Warning: /!\ No terms found to trigger on. Potential trigger not suitable: LetExpr.dfy(206,30)
 LetExpr.dfy(340,18): Error: value does not satisfy the subset constraints of 'nat'
 LetExpr.dfy(344,13): Error: value does not satisfy the subset constraints of 'nat'
 LetExpr.dfy(390,33): Error: assertion violation
@@ -15,7 +15,7 @@ LetExpr.dfy(323,11): Error: to be compilable, the value of a let-such-that expre
 LetExpr.dfy(109,22): Error: assertion violation
 
 Dafny program verifier finished with 37 verified, 13 errors
-LetExpr.dfy.tmp.dprint.dfy(281,4): Warning: /!\ No terms found to trigger on.
-LetExpr.dfy.tmp.dprint.dfy(46,2): Warning: /!\ No terms found to trigger on.
+LetExpr.dfy.tmp.dprint.dfy(281,4): Warning: /!\ No terms found to trigger on. Potential trigger not suitable: LetExpr.dfy.tmp.dprint.dfy(283,8)
+LetExpr.dfy.tmp.dprint.dfy(46,2): Warning: /!\ No terms found to trigger on. Potential trigger not suitable: LetExpr.dfy.tmp.dprint.dfy(47,12)
 
 Dafny program verifier did not attempt verification

Test/allocated1/dafny0/Matrix-OOB.dfy.expect

@@ -1,4 +1,4 @@
-Matrix-OOB.dfy(11,10): Info: Selected triggers: {m[i, j]}
+Matrix-OOB.dfy(11,10): Info: Selected triggers: {m[i, j]} Trigger position: Matrix-OOB.dfy(11,33)
 Matrix-OOB.dfy(11,26): Error: index 0 out of range
 Matrix-OOB.dfy(11,26): Error: index 1 out of range
 Matrix-OOB.dfy(12,0): Error: A postcondition might not hold on this return path.