Add tooltip on assertions that shows which functions are hidden

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "boogie"]
+	path = boogie
+	url = git@github.com:keyboardDrummer/boogie.git

Source/Dafny.sln

@@ -43,6 +43,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
 EndProject
+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}"
+EndProject
 EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -138,5 +164,17 @@ Global
 		SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187}
 	EndGlobalSection
 	GlobalSection(NestedProjects) = preSolution
+		{68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90}
+		{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90}
 	EndGlobalSection
 EndGlobal

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,19 @@ public int CompareTo(IToken other) {
   public int CompareTo(Boogie.IToken other) {
     return WrappedToken.CompareTo(other);
   }
+
+  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 +256,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,17 @@
       <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" />
+      <ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Graph\Graph.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Model\Model.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\VCExpr\VCExpr.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\VCGeneration\VCGeneration.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Provers\SMTLib\SMTLib.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Houdini\Houdini.csproj" />
+      <ProjectReference Include="..\..\boogie\Source\Concurrency\Concurrency.csproj" />
       <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;
+  }
+}