From 2a92810261d237e302671841c980deba908de893 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 22 Nov 2024 14:36:31 +0100 Subject: [PATCH 01/12] Use custom Boogie --- .gitmodules | 3 +++ Source/Dafny.sln | 38 +++++++++++++++++++++++++++++++ Source/DafnyCore/DafnyCore.csproj | 12 +++++++++- boogie | 1 + 4 files changed, 53 insertions(+), 1 deletion(-) create mode 100644 .gitmodules create mode 160000 boogie diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000000..094a08ca18f --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "boogie"] + path = boogie + url = git@github.com:keyboardDrummer/boogie.git diff --git a/Source/Dafny.sln b/Source/Dafny.sln index 23297b185ed..fc8e8b1fa49 100644 --- a/Source/Dafny.sln +++ b/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 diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 6c65a128f29..c15a3145ea3 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,7 +34,17 @@ - + + + + + + + + + + + diff --git a/boogie b/boogie new file mode 160000 index 00000000000..98fafe3c869 --- /dev/null +++ b/boogie @@ -0,0 +1 @@ +Subproject commit 98fafe3c8696bb7309e8ef4d0ec00ea4c0e300c1 From ea4cbb05103a3fea6fa28a43fb055017aa708c03 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 22 Nov 2024 16:01:38 +0100 Subject: [PATCH 02/12] Add tooltip on assertions for what is hidden when verifying --- Source/DafnyCore/Pipeline/Compilation.cs | 16 ++++++++-- Source/DafnyCore/Verifier/BoogieGenerator.cs | 11 ++++++- .../Diagnostics/DiagnosticsTest.cs | 31 +++++++++++++++++++ .../DafnyLanguageServer/Workspace/IdeState.cs | 1 - .../LitTest/ast/reveal/revealFunctions.dfy | 24 +++++++++++++- .../ast/reveal/revealFunctions.dfy.expect | 17 +++++++++- boogie | 2 +- 7 files changed, 95 insertions(+), 7 deletions(-) diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index de3d093754c..d7d47a49793 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -356,15 +356,27 @@ 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) { + foreach (var tokenTasks in tasks.GroupBy(t => + BoogieGenerator.ToDafnyToken(true, t.Token)). + OrderBy(g => g.Key)) { + var functions = tokenTasks.SelectMany(t => t.Split.HiddenFunctions.Select(f => f.tok). + OfType().Select(n => n.Node). + OfType()).Distinct(); + 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.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index c670672eb96..62b90a9cc8d 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..a44efc205ce 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -1307,6 +1307,37 @@ 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); + } + 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/boogie b/boogie index 98fafe3c869..9409974da90 160000 --- a/boogie +++ b/boogie @@ -1 +1 @@ -Subproject commit 98fafe3c8696bb7309e8ef4d0ec00ea4c0e300c1 +Subproject commit 9409974da90281c5f371c6d8285eb44bf52decb6 From 8dedb49474cf3cd9e58b1b3bc944ec72f8abe460 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 25 Nov 2024 13:55:30 +0100 Subject: [PATCH 03/12] Add tests and a fix --- Source/DafnyCore/AST/Tokens.cs | 9 ++ Source/DafnyCore/Pipeline/Compilation.cs | 10 +- .../Diagnostics/DiagnosticsTest.cs | 94 +++++++++++++++++++ boogie | 2 +- 4 files changed, 110 insertions(+), 5 deletions(-) diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index f2144918121..7538863998a 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/DafnyCore/AST/Tokens.cs @@ -204,6 +204,15 @@ 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); + } + + return token; + } } public static class TokenExtensions { diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index d7d47a49793..f91facf84bc 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -363,12 +363,14 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT await ticket; if (!onlyPrepareVerificationForGutterTests) { - foreach (var tokenTasks in tasks.GroupBy(t => - BoogieGenerator.ToDafnyToken(true, t.Token)). - OrderBy(g => g.Key)) { + 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(); + 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}"); diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index a44efc205ce..da0991e34d9 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -1331,11 +1331,105 @@ 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); + } + + [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 +} + +method {:isolate_assertions} TestIsolateAssertions() { + hide *; + reveal P; + assert P(6); +} +".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/boogie b/boogie index 9409974da90..4d2d7ad983d 160000 --- a/boogie +++ b/boogie @@ -1 +1 @@ -Subproject commit 9409974da90281c5f371c6d8285eb44bf52decb6 +Subproject commit 4d2d7ad983d508c8e21f2d59c06cecc1c6446ac2 From 3bf7ab45b8bbc69d95ce678e10290b9715b658a0 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Mon, 25 Nov 2024 17:32:57 +0100 Subject: [PATCH 04/12] Improvements --- Source/DafnyCore/AST/RangeToken.cs | 97 +++++++++++++++++++ Source/DafnyCore/AST/Tokens.cs | 87 +---------------- .../Verifier/BoogieGenerator.BoogieFactory.cs | 7 ++ .../Diagnostics/DiagnosticsTest.cs | 5 + .../FunctionHidingRefactoring.dfy.expect | 8 ++ Source/XUnitExtensions/Lit/DiffCommand.cs | 2 +- 6 files changed, 122 insertions(+), 84 deletions(-) create mode 100644 Source/DafnyCore/AST/RangeToken.cs 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 7538863998a..fd27013eaa9 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; @@ -211,6 +210,10 @@ public static IToken Unwrap(IToken token, bool includeRanges = false) { return Unwrap(wrapper.WrappedToken); } + if (token is RangeToken rangeToken) { + return new RangeToken(Unwrap(rangeToken.StartToken), Unwrap(rangeToken.EndToken)); + } + return token; } } @@ -253,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; } 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/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index da0991e34d9..b817ea8b898 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -1396,6 +1396,11 @@ predicate P(x: int) { 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 < 3; index++) { + Assert.Equal(sorted[index * 2].Range, sorted[index * 2 + 1].Range); + } } [Fact] 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/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs index db7408470f2..4de3766db77 100644 --- a/Source/XUnitExtensions/Lit/DiffCommand.cs +++ b/Source/XUnitExtensions/Lit/DiffCommand.cs @@ -11,7 +11,7 @@ namespace XUnitExtensions.Lit { /// because 'diff' does not exist on Windows. /// public class DiffCommand : ILitCommand { - public static readonly bool UpdateExpectFile = Environment.GetEnvironmentVariable("DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE") == "true"; + public static readonly bool UpdateExpectFile = true; public string ExpectedPath { get; } public string ActualPath { get; } From 6293a2713e5e1bdcfea726244302c18d022d354b Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 26 Nov 2024 11:01:17 +0100 Subject: [PATCH 05/12] Revert bad change --- Source/XUnitExtensions/Lit/DiffCommand.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs index 4de3766db77..db7408470f2 100644 --- a/Source/XUnitExtensions/Lit/DiffCommand.cs +++ b/Source/XUnitExtensions/Lit/DiffCommand.cs @@ -11,7 +11,7 @@ namespace XUnitExtensions.Lit { /// because 'diff' does not exist on Windows. /// public class DiffCommand : ILitCommand { - public static readonly bool UpdateExpectFile = true; + public static readonly bool UpdateExpectFile = Environment.GetEnvironmentVariable("DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE") == "true"; public string ExpectedPath { get; } public string ActualPath { get; } From 2b63912290ec1786d25237e3c938c317b4b607b3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 26 Nov 2024 12:01:12 +0100 Subject: [PATCH 06/12] Fix test --- Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index b817ea8b898..d2cf2fc4789 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -1398,7 +1398,7 @@ predicate P(x: int) { Assert.Single(infoDiagnostics); var sorted = diagnostics.OrderBy(d => d.Range.Start).ToList(); - for (int index = 0; index < 3; index++) { + for (int index = 0; index < sorted.Count / 2; index++) { Assert.Equal(sorted[index * 2].Range, sorted[index * 2 + 1].Range); } } From f68416ea07d5c5cf9d0be9a2248a23514adbdea6 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 26 Nov 2024 14:22:43 +0100 Subject: [PATCH 07/12] Code review --- Source/DafnyCore/AST/Tokens.cs | 3 +++ .../DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs | 5 +++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index fd27013eaa9..4b7bba0513f 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/DafnyCore/AST/Tokens.cs @@ -204,6 +204,9 @@ 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)) { diff --git a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs index d2cf2fc4789..4ae464d630d 100644 --- a/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs +++ b/Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs @@ -1423,10 +1423,11 @@ requires A(x) && B(x) true } -method {:isolate_assertions} TestIsolateAssertions() { +@IsolateAssertions +method TestIsolateAssertions(x: int) { hide *; reveal P; - assert P(6); + assert P(x); } ".TrimStart(); var documentItem = CreateTestDocument(source, "HiddenFunctionHints.dfy"); From b2daf87673f307bd72705e01868861425e464fc8 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 26 Nov 2024 16:34:49 +0100 Subject: [PATCH 08/12] Remove Boogie submodule --- .gitmodules | 3 --- boogie | 1 - 2 files changed, 4 deletions(-) delete mode 160000 boogie diff --git a/.gitmodules b/.gitmodules index 094a08ca18f..e69de29bb2d 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +0,0 @@ -[submodule "boogie"] - path = boogie - url = git@github.com:keyboardDrummer/boogie.git diff --git a/boogie b/boogie deleted file mode 160000 index 4d2d7ad983d..00000000000 --- a/boogie +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 4d2d7ad983d508c8e21f2d59c06cecc1c6446ac2 From 45a6b9d6a29b491076375cd12bf32fa7a31751d1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 26 Nov 2024 16:44:49 +0100 Subject: [PATCH 09/12] Update Boogie version --- Source/Dafny.sln | 38 ------------------------------- Source/DafnyCore/DafnyCore.csproj | 12 +--------- customBoogie.patch | 2 +- 3 files changed, 2 insertions(+), 50 deletions(-) diff --git a/Source/Dafny.sln b/Source/Dafny.sln index fc8e8b1fa49..23297b185ed 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln @@ -43,32 +43,6 @@ 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 @@ -164,17 +138,5 @@ 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 diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index c15a3145ea3..3ac2ed66bb6 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -34,17 +34,7 @@ - - - - - - - - - - - + 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 -- +- + + + From 6e0dbfce959eabc75c0e303e2b8b32c037fb04fa Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 26 Nov 2024 17:35:58 +0100 Subject: [PATCH 10/12] Submodule attempt From 6f2abe4f634f6b79859f1decc0dbdda61a62e610 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 28 Nov 2024 12:52:09 +0100 Subject: [PATCH 11/12] Trigger CI From 5c074dfcdb3c962983f77dc1ed23ec70d77499e0 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 28 Nov 2024 15:41:24 +0100 Subject: [PATCH 12/12] Trigger CI