diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000000..e69de29bb2d diff --git a/Source/DafnyCore/AST/RangeToken.cs b/Source/DafnyCore/AST/RangeToken.cs new file mode 100644 index 00000000000..722a5ff90a0 --- /dev/null +++ b/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); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index f2144918121..4b7bba0513f 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/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); } + + /// + /// Removes token wrappings from a given token, so that it returns the bare token + /// + 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; } diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 6c65a128f29..3ac2ed66bb6 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,7 @@ - + diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index de3d093754c..f91facf84bc 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/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().Select(n => n.Node). + OfType()).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); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs index 76cb56e2163..b63e172efe6 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs +++ b/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) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index bda723ef86a..3a6adb62a25 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/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(), formals, res, "function declaration for " + f.FullName); + func = new Bpl.Function(new FromDafnyNode(f), f.FullSanitizedName, new List(), 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; + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index 943a593b878..4ae464d630d 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -1307,6 +1307,137 @@ method Foo() { Assert.Empty(diagnostics2); } + [Fact] + public async Task HiddenFunctionHints() { + var source = @" +predicate Outer(x: int) { + Inner(x) +} + +predicate Inner(x: int) { + x > 3 +} + +method {:isolate_assertions} InnerOuterUser() { + hide *; + assert Outer(0); + assert Outer(1) by { + reveal Outer; + } + assert Outer(2) by { + reveal Inner; + } + assert Outer(3) by { + reveal Outer, Inner; + } +} + + +".TrimStart(); + var documentItem = CreateTestDocument(source, "HiddenFunctionHints.dfy"); + client.OpenDocument(documentItem); + var diagnostics = await GetLastDiagnostics(documentItem, minimumSeverity: DiagnosticSeverity.Hint); + + Assert.Equal(6, diagnostics.Length); + var sorted = diagnostics.OrderBy(d => d.Range.Start).ToList(); + for (int index = 0; index < 3; index++) { + Assert.Equal(sorted[index * 2].Range, sorted[index * 2 + 1].Range); + } + } + + [Fact] + public async Task HiddenFunctionTooltipBlowup() { + var source = @" +predicate A(x: int) { + x < 5 +} +predicate B(x: int) { + x > 3 +} +predicate P(x: int) { + A(x) && B(x) +} + +method {:isolate_assertions} TestIsolateAssertions() { + hide *; + assert P(3); +} +".TrimStart(); + var documentItem = CreateTestDocument(source, "HiddenFunctionHints.dfy"); + client.OpenDocument(documentItem); + var diagnostics = await GetLastDiagnostics(documentItem, minimumSeverity: DiagnosticSeverity.Hint); + + var infoDiagnostics = diagnostics.Where(d => d.Severity >= DiagnosticSeverity.Information).ToList(); + Assert.Single(infoDiagnostics); + } + + [Fact] + public async Task HiddenFunctionTooltipBlowup2() { + var source = @" +predicate A(x: int) { + x < 5 +} +predicate B(x: int) { + x > 3 +} +predicate P(x: int) { + A(x) && B(x) +} + +method {:isolate_assertions} TestIsolateAssertions() { + hide *; + reveal P; + assert P(3); +} +".TrimStart(); + var documentItem = CreateTestDocument(source, "HiddenFunctionHints.dfy"); + client.OpenDocument(documentItem); + var diagnostics = await GetLastDiagnostics(documentItem, minimumSeverity: DiagnosticSeverity.Hint); + + var infoDiagnostics = diagnostics.Where(d => d.Severity >= DiagnosticSeverity.Information).ToList(); + Assert.Single(infoDiagnostics); + + var sorted = diagnostics.OrderBy(d => d.Range.Start).ToList(); + for (int index = 0; index < sorted.Count / 2; index++) { + Assert.Equal(sorted[index * 2].Range, sorted[index * 2 + 1].Range); + } + } + + [Fact] + public async Task HiddenFunctionTooltipBlowup3() { + var source = @" +predicate A(x: int) { + x < 7 && C(x) +} +predicate B(x: int) { + x > 3 +} + +predicate C(x: int) { + x < 5 +} + +predicate P(x: int) + requires A(x) && B(x) +{ + true +} + +@IsolateAssertions +method TestIsolateAssertions(x: int) { + hide *; + reveal P; + assert P(x); +} +".TrimStart(); + var documentItem = CreateTestDocument(source, "HiddenFunctionHints.dfy"); + client.OpenDocument(documentItem); + var diagnostics = await GetLastDiagnostics(documentItem, minimumSeverity: DiagnosticSeverity.Hint); + + var infoDiagnostics = diagnostics.Where(d => d.Severity >= DiagnosticSeverity.Information).ToList(); + Assert.Single(infoDiagnostics); + } + public DiagnosticsTest(ITestOutputHelper output) : base(output) { } } diff --git a/Source/DafnyLanguageServer/Workspace/IdeState.cs b/Source/DafnyLanguageServer/Workspace/IdeState.cs index 7b0d383293d..d466a920e13 100644 --- a/Source/DafnyLanguageServer/Workspace/IdeState.cs +++ b/Source/DafnyLanguageServer/Workspace/IdeState.cs @@ -393,7 +393,6 @@ private IdeState HandleCanVerifyPartsUpdated(ILogger logger, CanVerifyPartsIdent var range = canVerifyPartsIdentified.CanVerify.NavigationToken.GetLspRange(); var previousImplementations = previousState.CanVerifyStates[uri][range].VerificationTasks; - var names = canVerifyPartsIdentified.Parts.Select(Compilation.GetTaskName); var verificationResult = new IdeCanVerifyState(PreparationProgress: VerificationPreparationState.Done, VerificationTasks: canVerifyPartsIdentified.Parts.ToImmutableDictionary(Compilation.GetTaskName, k => { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy index 8233d2f066e..4738c07be2b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy @@ -1,4 +1,4 @@ -// RUN: ! %verify --type-system-refresh --allow-axioms --isolate-assertions %s > %t +// RUN: ! %verify --type-system-refresh --allow-axioms --show-hints --isolate-assertions %s > %t // RUN: %diff "%s.expect" "%t" function P(x: int): bool { @@ -102,4 +102,26 @@ module M2 { hide *; reveal RecFunc; } +} + +predicate Outer(x: int) { + Inner(x) +} + +predicate Inner(x: int) { + x > 3 +} + +method InnerOuterUser() { + hide *; + assert Outer(0); + assert Outer(1) by { + reveal Outer; + } + assert Outer(2) by { + reveal Inner; + } + assert Outer(3) by { + reveal Outer, Inner; + } } \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect index 875e3bafe09..dddd31ea545 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect @@ -1,5 +1,20 @@ +revealFunctions.dfy(90,19): Info: auto-accumulator tail recursive +revealFunctions.dfy(90,19): Info: decreases x +revealFunctions.dfy(15,12): Info: hidden functions: P +revealFunctions.dfy(22,12): Info: hidden functions: P +revealFunctions.dfy(49,21): Info: hidden functions: OpaqueFunc +revealFunctions.dfy(57,11): Info: hidden functions: Natty +revealFunctions.dfy(60,11): Info: hidden functions: Natty +revealFunctions.dfy(79,4): Info: hidden functions: Obj +revealFunctions.dfy(81,18): Info: hidden functions: Obj +revealFunctions.dfy(117,14): Info: hidden functions: Outer +revealFunctions.dfy(118,14): Info: hidden functions: Inner +revealFunctions.dfy(121,14): Info: hidden functions: Outer revealFunctions.dfy(15,12): Error: assertion might not hold revealFunctions.dfy(22,12): Error: assertion might not hold revealFunctions.dfy(49,21): Error: assertion might not hold +revealFunctions.dfy(117,14): Error: assertion might not hold +revealFunctions.dfy(118,14): Error: assertion might not hold +revealFunctions.dfy(121,14): Error: assertion might not hold -Dafny program verifier finished with 22 verified, 3 errors +Dafny program verifier finished with 23 verified, 6 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect index fe3c1324406..942699e6865 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/FunctionHidingRefactoring.dfy.expect @@ -1,3 +1,11 @@ +FunctionHidingRefactoring.dfy(35,12): Info: hidden functions: Id +FunctionHidingRefactoring.dfy(46,12): Info: hidden functions: Square +FunctionHidingRefactoring.dfy(51,2): Info: hidden functions: Square +FunctionHidingRefactoring.dfy(52,14): Info: hidden functions: Square +FunctionHidingRefactoring.dfy(52,16): Info: hidden functions: Square +FunctionHidingRefactoring.dfy(53,14): Info: hidden functions: Square +FunctionHidingRefactoring.dfy(55,9): Info: hidden functions: Square +FunctionHidingRefactoring.dfy(58,7): Info: hidden functions: Square FunctionHidingRefactoring.dfy(13,0): Info: Consider hiding these functions, which are unused by the proof: Id, Square FunctionHidingRefactoring.dfy(19,0): Info: Consider hiding these functions, which are unused by the proof: Id, Square FunctionHidingRefactoring.dfy(36,0): Info: Consider hiding this function, which is unused by the proof: Square diff --git a/customBoogie.patch b/customBoogie.patch index 9023f27d395..911dc435a47 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + + +