Add tooltip on assertions that shows which functions are hidden

[keyboardDrummer]

Depends on Boogie change: boogie-org/boogie#989

Description

• Add tooltip on assertions that shows which functions are hidden

Program:

Tooltip:

How has this been tested?

• Extend a CLI test and add an IDE test.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

I have a very substantial request for this PR. I have seen many places on which there can be 50 propositions under a single one. For example, when asserting a predicate that is a conjunct of a lot of propositions, we get one assertion batch for each.
That means, we'd also get a lot of "hidden functions" tooltips for each batch, and there will be no relationship between the error/success messages and the "hidden" tooltip, making them effectively useless.

Please test this hypothesis with the following code:

predicate A()
predicate B()
predicate P() {
  A() && B()
}

method {:isolate_assertions} TestIsolateAssertions() {
  assert P();
}

I understand that when you hide functions, you hide all of them on which the proof depends, so there is not a method-level set of hidden functions like there was for {:autoRevealDependencies}, correct? I believe that it makes the interface harder to think of.

If I understand this correctly, could you perhaps do the following:

• Display the tooltip only on assertions that failed?
• Incorporate the tooltip in the rich tooltip that the Dafny language server generates

At worst, I'd request to at least include the assertion batch number that the hidden tooltip refers to, but that still would be overwhelming. I've heard of codebases which routinely hide 100+ functions. Even if you only display the first generation of hidden functions, that'd be still a lot.

[MikaelMayer]

Suggested change

[MikaelMayer]

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.

[keyboardDrummer]

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?

[MikaelMayer]

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.

[keyboardDrummer]

Please test this hypothesis with the following code:

I totally didn't think about the assertion splitting, thanks for reminding me! However, testing the example code you gave still gives good results: "hidden functions: P" is shown.

Investigating why, it's actually something that might need to be improved/fixed. The function TrSplitFunctionCallExpr has the following early exit code:

} else if (context.ContainsHide) {
  // Do not inline in a blind context

so it won't perform any splitting inside functions using hide. This might also explain part of why hide * seems to achieve such good results: it not only hides function bodies but also reduces SMT clutter from expression splitting.

I'm not sure what the right next step is. Would be great if we can add precise error message without splitting to Boogie.

so there is not a method-level set of hidden functions like there was for {:autoRevealDependencies}, correct?

There is not, since you can hide/reveal through the function. Each assertion in the method effectively has its own set of what's revealed/hidden.

I've heard of codebases which routinely hide 100+ functions. Even if you only display the first generation of hidden functions, that'd be still a lot.

Just to be clear, when you do hide *, only functions that are called from the current assertion batch will show up in the list, until you reveal one of them and then the functions that the revealed function calls also show.

Display the tooltip only on assertions that failed?
Right now it'll show it during the verification process, but before SMT verification starts. I think that could be nice cause then you can evaluate whether you need to hide more/less if verification takes long.

Incorporate the tooltip in the rich tooltip that the Dafny language server generates
I'd like to keep the IDE and CLI consistent. What would be the advantage of using the rich tooltip?

[MikaelMayer]

Oh I forgot that hiding makes function opaque so they are not split. Interesting.

Please try the following example:

predicate A()
predicate B()
predicate P() {
  A() && B()
}

method {:isolate_assertions} TestIsolateAssertions() {
  hide *;
  reveal P();
  assert P();
}

[keyboardDrummer]

predicate A()
predicate B()
predicate P() {
  A() && B()
}

method {:isolate_assertions} TestIsolateAssertions() {
  hide *;
  reveal P();
  assert P();
}

Shows: hidden functions: A, B

As expected

[MikaelMayer]

Can you please try this as well:

predicate A()
predicate B()
predicate P()
  requires A() && B()
{
  true
}

method {:isolate_assertions} TestIsolateAssertions() {
  hide *;
  reveal P();
  assert P();
}