Add tooltip on assertions that shows which functions are hidden

Source/DafnyCore/AST/RangeToken.cs

@@ -0,0 +1,97 @@
+using System;
+using System.Text;
+
+namespace Microsoft.Dafny;
+
+public class RangeToken : TokenWrapper {
+  public IToken StartToken => WrappedToken;
+
+  public IToken EndToken => endToken ?? StartToken;
+
+  public bool InclusiveEnd => endToken != null;
+
+  public override bool Equals(object obj) {
+    if (obj is RangeToken other) {
+      return StartToken.Equals(other.StartToken) && EndToken.Equals(other.EndToken);
+    }
+    return false;
+  }
+
+  public override int GetHashCode() {
+    return HashCode.Combine(StartToken.GetHashCode(), EndToken.GetHashCode());
+  }
+
+  public DafnyRange ToDafnyRange(bool includeTrailingWhitespace = false) {
+    var startLine = StartToken.line - 1;
+    var startColumn = StartToken.col - 1;
+    var endLine = EndToken.line - 1;
+    int whitespaceOffset = 0;
+    if (includeTrailingWhitespace) {
+      string trivia = EndToken.TrailingTrivia;
+      // Don't want to remove newlines or comments -- just spaces and tabs
+      while (whitespaceOffset < trivia.Length && (trivia[whitespaceOffset] == ' ' || trivia[whitespaceOffset] == '\t')) {
+        whitespaceOffset++;
+      }
+    }
+
+    var endColumn = EndToken.col + (InclusiveEnd ? EndToken.val.Length : 0) + whitespaceOffset - 1;
+    return new DafnyRange(
+      new DafnyPosition(startLine, startColumn),
+      new DafnyPosition(endLine, endColumn));
+  }
+
+  public RangeToken(IToken startToken, IToken endToken) : base(startToken) {
+    this.endToken = endToken;
+  }
+
+  public string PrintOriginal() {
+    var token = StartToken;
+    var originalString = new StringBuilder();
+    originalString.Append(token.val);
+    while (token.Next != null && token.pos < EndToken.pos) {
+      originalString.Append(token.TrailingTrivia);
+      token = token.Next;
+      originalString.Append(token.LeadingTrivia);
+      originalString.Append(token.val);
+    }
+
+    return originalString.ToString();
+  }
+
+  public int Length() {
+    return EndToken.pos - StartToken.pos;
+  }
+
+  public RangeToken MakeAutoGenerated() {
+    return new RangeToken(new AutoGeneratedToken(StartToken), EndToken);
+  }
+
+  public RangeToken MakeRefined(ModuleDefinition module) {
+    return new RangeToken(new RefinementToken(StartToken, module), EndToken);
+  }
+
+  // TODO rename to Generated, and Token.NoToken to Token.Generated, and remove AutoGeneratedToken.
+  public static RangeToken NoToken = new(Token.NoToken, Token.NoToken);
+  private readonly IToken endToken;
+
+  public override IToken WithVal(string newVal) {
+    throw new NotImplementedException();
+  }
+
+  public override bool IsSourceToken => this != NoToken;
+
+  public BoogieRangeToken ToToken() {
+    return new BoogieRangeToken(StartToken, EndToken, null);
+  }
+
+  public bool Contains(IToken otherToken) {
+    return StartToken.Uri == otherToken.Uri &&
+           StartToken.pos <= otherToken.pos &&
+           (EndToken == null || otherToken.pos <= EndToken.pos);
+  }
+
+  public bool Intersects(RangeToken other) {
+    return !(other.EndToken.pos + other.EndToken.val.Length <= StartToken.pos
+             || EndToken.pos + EndToken.val.Length <= other.StartToken.pos);
+  }
+}

Source/DafnyCore/AST/Tokens.cs

@@ -2,7 +2,6 @@
 using System;
 using System.Diagnostics.Contracts;
 using System.IO;
-using System.Text;
 
 namespace Microsoft.Dafny;
 
@@ -204,6 +203,22 @@ public int CompareTo(IToken other) {
   public int CompareTo(Boogie.IToken other) {
     return WrappedToken.CompareTo(other);
   }
+
+  /// <summary>
+  ///  Removes token wrappings from a given token, so that it returns the bare token
+  /// </summary>
+  public static IToken Unwrap(IToken token, bool includeRanges = false) {
+    if (token is TokenWrapper wrapper
+        && (includeRanges || token is not RangeToken)) {
+      return Unwrap(wrapper.WrappedToken);
+    }
+
+    if (token is RangeToken rangeToken) {
+      return new RangeToken(Unwrap(rangeToken.StartToken), Unwrap(rangeToken.EndToken));
+    }
+
+    return token;
+  }
 }
 
 public static class TokenExtensions {
@@ -244,88 +259,6 @@ public static RangeToken ToRange(this IToken token) {
   }
 }
 
-public class RangeToken : TokenWrapper {
-  public IToken StartToken => WrappedToken;
-
-  public IToken EndToken => endToken ?? StartToken;
-
-  public bool InclusiveEnd => endToken != null;
-
-  public DafnyRange ToDafnyRange(bool includeTrailingWhitespace = false) {
-    var startLine = StartToken.line - 1;
-    var startColumn = StartToken.col - 1;
-    var endLine = EndToken.line - 1;
-    int whitespaceOffset = 0;
-    if (includeTrailingWhitespace) {
-      string trivia = EndToken.TrailingTrivia;
-      // Don't want to remove newlines or comments -- just spaces and tabs
-      while (whitespaceOffset < trivia.Length && (trivia[whitespaceOffset] == ' ' || trivia[whitespaceOffset] == '\t')) {
-        whitespaceOffset++;
-      }
-    }
-
-    var endColumn = EndToken.col + (InclusiveEnd ? EndToken.val.Length : 0) + whitespaceOffset - 1;
-    return new DafnyRange(
-      new DafnyPosition(startLine, startColumn),
-      new DafnyPosition(endLine, endColumn));
-  }
-
-  public RangeToken(IToken startToken, IToken endToken) : base(startToken) {
-    this.endToken = endToken;
-  }
-
-  public string PrintOriginal() {
-    var token = StartToken;
-    var originalString = new StringBuilder();
-    originalString.Append(token.val);
-    while (token.Next != null && token.pos < EndToken.pos) {
-      originalString.Append(token.TrailingTrivia);
-      token = token.Next;
-      originalString.Append(token.LeadingTrivia);
-      originalString.Append(token.val);
-    }
-
-    return originalString.ToString();
-  }
-
-  public int Length() {
-    return EndToken.pos - StartToken.pos;
-  }
-
-  public RangeToken MakeAutoGenerated() {
-    return new RangeToken(new AutoGeneratedToken(StartToken), EndToken);
-  }
-
-  public RangeToken MakeRefined(ModuleDefinition module) {
-    return new RangeToken(new RefinementToken(StartToken, module), EndToken);
-  }
-
-  // TODO rename to Generated, and Token.NoToken to Token.Generated, and remove AutoGeneratedToken.
-  public static RangeToken NoToken = new(Token.NoToken, Token.NoToken);
-  private readonly IToken endToken;
-
-  public override IToken WithVal(string newVal) {
-    throw new NotImplementedException();
-  }
-
-  public override bool IsSourceToken => this != NoToken;
-
-  public BoogieRangeToken ToToken() {
-    return new BoogieRangeToken(StartToken, EndToken, null);
-  }
-
-  public bool Contains(IToken otherToken) {
-    return StartToken.Uri == otherToken.Uri &&
-           StartToken.pos <= otherToken.pos &&
-           (EndToken == null || otherToken.pos <= EndToken.pos);
-  }
-
-  public bool Intersects(RangeToken other) {
-    return !(other.EndToken.pos + other.EndToken.val.Length <= StartToken.pos
-             || EndToken.pos + EndToken.val.Length <= other.StartToken.pos);
-  }
-}
-
 public class BoogieRangeToken : TokenWrapper {
   // The wrapped token is the startTok
   public IToken StartToken { get; }

Source/DafnyCore/DafnyCore.csproj

@@ -34,7 +34,7 @@
       <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
       <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
       <PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
-      <PackageReference Include="Boogie.ExecutionEngine" Version="3.4.2" />
+      <PackageReference Include="Boogie.ExecutionEngine" Version="3.4.3" />
       <PackageReference Include="Tomlyn" Version="0.16.2" />
   </ItemGroup>
 

Source/DafnyCore/Pipeline/Compilation.cs

@@ -356,15 +356,29 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
         return result;
       });
       if (updated || randomSeed != null) {
-        updates.OnNext(new CanVerifyPartsIdentified(canVerify,
-          tasksPerVerifiable[canVerify].ToList()));
+        updates.OnNext(new CanVerifyPartsIdentified(canVerify, tasks));
       }
 
       // When multiple calls to VerifyUnverifiedSymbol are made, the order in which they pass this await matches the call order.
       await ticket;
 
       if (!onlyPrepareVerificationForGutterTests) {
+        var groups = tasks.GroupBy(t =>
+            // We unwrap so that we group on tokens as they are displayed to the user by Reporter.Info
+            TokenWrapper.Unwrap(BoogieGenerator.ToDafnyToken(true, t.Token))).
+          OrderBy(g => g.Key);
+        foreach (var tokenTasks in groups) {
+          var functions = tokenTasks.SelectMany(t => t.Split.HiddenFunctions.Select(f => f.tok).
+            OfType<FromDafnyNode>().Select(n => n.Node).
+            OfType<Function>()).Distinct().OrderBy(f => f.tok);
+          var hiddenFunctions = string.Join(", ", functions.Select(f => f.FullDafnyName));
+          if (!string.IsNullOrEmpty(hiddenFunctions)) {
+            Reporter.Info(MessageSource.Verifier, tokenTasks.Key, $"hidden functions: {hiddenFunctions}");
+          }
+        }
+
         foreach (var task in tasks.Where(taskFilter)) {
+
           var seededTask = randomSeed == null ? task : task.FromSeed(randomSeed.Value);
           VerifyTask(canVerify, seededTask);
         }

Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs

@@ -889,6 +889,13 @@ public static IToken ToDafnyToken(bool reportRanges, Bpl.IToken boogieToken) {
 
         return new RangeToken(boogieRangeToken.StartToken, boogieRangeToken.EndToken);
       }
+
+      if (boogieToken is NestedToken nestedToken) {
+        return new NestedToken(
+          ToDafnyToken(reportRanges, nestedToken.Outer),
+          ToDafnyToken(reportRanges, nestedToken.Inner));
+      }
+
       if (boogieToken == null) {
         return null;
       } else if (boogieToken is IToken dafnyToken) {

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -20,6 +20,7 @@
 using static Microsoft.Dafny.Util;
 using DafnyCore.Verifier;
 using JetBrains.Annotations;
+using Microsoft.Dafny;
 using Microsoft.Dafny.Triggers;
 using PODesc = Microsoft.Dafny.ProofObligationDescription;
 using static Microsoft.Dafny.GenericErrors;
@@ -2697,7 +2698,7 @@ private Bpl.Function GetFunctionBoogieDefinition(Function f) {
           formals.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(f.IdGenerator), TrType(p.Type)), true));
         }
         var res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, TrType(f.ResultType)), false);
-        func = new Bpl.Function(f.tok, f.FullSanitizedName, new List<Bpl.TypeVariable>(), formals, res, "function declaration for " + f.FullName);
+        func = new Bpl.Function(new FromDafnyNode(f), f.FullSanitizedName, new List<Bpl.TypeVariable>(), formals, res, "function declaration for " + f.FullName);
         if (InsertChecksums) {
           InsertChecksum(f, func);
         }
@@ -4802,3 +4803,11 @@ public enum AssertMode { Keep, Assume, Check }
 }
 
 public enum IsAllocType { ISALLOC, NOALLOC, NEVERALLOC };  // NEVERALLOC is like NOALLOC, but overrides AlwaysAlloc
+
+class FromDafnyNode : VCGeneration.TokenWrapper {
+  public INode Node { get; }
+
+  public FromDafnyNode(INode node) : base(node.Tok) {
+    this.Node = node;
+  }
+}