Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add tooltip on assertions that shows which functions are hidden #5929

Merged
merged 17 commits into from
Nov 28, 2024
Merged

Add tooltip on assertions that shows which functions are hidden #5929

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
2a92810
Use custom Boogie
keyboardDrummer Nov 22, 2024
ea4cbb0
Add tooltip on assertions for what is hidden when verifying
keyboardDrummer Nov 22, 2024
8dedb49
Add tests and a fix
keyboardDrummer Nov 25, 2024
a6e2f8f
Merge branch 'master' into whatIsHiddenHint
keyboardDrummer Nov 25, 2024
3bf7ab4
Improvements
keyboardDrummer Nov 25, 2024
6293a27
Revert bad change
keyboardDrummer Nov 26, 2024
2b63912
Fix test
keyboardDrummer Nov 26, 2024
f68416e
Code review
keyboardDrummer Nov 26, 2024
b2daf87
Remove Boogie submodule
keyboardDrummer Nov 26, 2024
45a6b9d
Update Boogie version
keyboardDrummer Nov 26, 2024
9e0feff
Merge branch 'master' into whatIsHiddenHint
keyboardDrummer Nov 26, 2024
ea82f96
Merge branch 'whatIsHiddenHint' of github.com:keyboardDrummer/dafny i…
keyboardDrummer Nov 26, 2024
6e0dbfc
Submodule attempt
keyboardDrummer Nov 26, 2024
6f2abe4
Trigger CI
keyboardDrummer Nov 28, 2024
eecb794
Merge branch 'master' into whatIsHiddenHint
keyboardDrummer Nov 28, 2024
5c074df
Trigger CI
keyboardDrummer Nov 28, 2024
d8eb6cd
Merge branch 'whatIsHiddenHint' of github.com:keyboardDrummer/dafny i…
keyboardDrummer Nov 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[submodule "boogie"]
path = boogie
url = [email protected]:keyboardDrummer/boogie.git
38 changes: 38 additions & 0 deletions Source/Dafny.sln
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
12 changes: 11 additions & 1 deletion Source/DafnyCore/DafnyCore.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>

Expand Down
16 changes: 14 additions & 2 deletions Source/DafnyCore/Pipeline/Compilation.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<FromDafnyNode>().Select(n => n.Node).
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wrapping tokens to filter functions is not ideal. There are multi competing token wrapping strategies that will end up failing this test in the future. For example, refinement tokens will wrap your FromDafnyNode token making them not pass this test. There are other wrapped tokens types, like auto-generated tokens, nested tokens, override tokens for traits, etc.
I have always advocated for replacing tokens with a single meta-data field on which we would add some flags as needed.

I'm not expecting you to do this refactoring, so in the meantime, please use something like FromDafnyNode.Has() that would recursively traverse the tokens to find one of its kind.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here the wrapping happens right before handing the token to Boogie, so Dafny won't do any further wrapper, and Boogie might do some wrapping on tokens but only use that for nodes that it creates, so not on the nodes that I'm interested in. I don't think there's a potential issue here. If there is one, how can we test for it?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, good to know that the risk is mitigated. I think that we still have the risk that later, someone will wrap your token after your own wrapping and their test cases will be orthogonal to yours, so both won't be tested together.
If you want to make sure your wrapping is the last one before sending the token to boogie, I'd suggest: changing the name to something like DafnyMetaData so that future development will become compelled to add metadata here rather than adding a new wrapping token.

OfType<Function>()).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)) {

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change

var seededTask = randomSeed == null ? task : task.FromSeed(randomSeed.Value);
VerifyTask(canVerify, seededTask);
}
Expand Down
11 changes: 10 additions & 1 deletion Source/DafnyCore/Verifier/BoogieGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
}
Expand Down Expand Up @@ -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;
}
}
31 changes: 31 additions & 0 deletions Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
}
}
Expand Down
1 change: 0 additions & 1 deletion Source/DafnyLanguageServer/Workspace/IdeState.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 => {
Expand Down
24 changes: 23 additions & 1 deletion Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 {
Expand Down Expand Up @@ -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;
}
}
17 changes: 16 additions & 1 deletion Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions boogie
Open in desktop
Submodule boogie added at 940997
Loading