Replace AddAssignedVariables with AddAssignedIdentifiers #945
Conversation
keyboardDrummer
requested review from
MikaelMayer
and removed request for
atomb
Source/VCGeneration/Prune/Pruner.cs
Outdated
| return parent is not Function function || child is not Axiom axiom || revealedState.IsRevealed(function) | ||
| || !axiom.CanHide; | ||
| || !axiom.CanHide || function.AlwaysRevealed; |
There was a problem hiding this comment.
Could this additional disjunct go into revealedState.IsRevealed(function)?
| public IEnumerable<Variable> GetAssignedVariables() { | ||
| List<IdentifierExpr> ids = new(); | ||
| AddAssignedIdentifiers(ids); | ||
| return ids.Select(id => id.Decl); |
There was a problem hiding this comment.
What you are saying is that .Decl is available only after resolution, whereas the id is available after parsing, correct? If that is the case, could you just add a comment to this function that says something like "Can be called only after resolution" ? Or I'm mistaken.
There was a problem hiding this comment.
That's correct.
| .) | ||
| [ "revealed" (. revealed = true; .) |
There was a problem hiding this comment.
What is the use of "revealed"? Every time the function is in scope, its axiom is automatically revealed? Is it like equivalent to having automatic reveal functionName after hide * ?
I would have thought the other way: That whatever visibility functions would have for themselves by default could be overridden by statements in an implementation.
At least, this is the affordance we now provide in Dafny thanks to your hide statements.
Special rules like this remind me of the CSS !important and their 5 prioritization rules that they ended up implementing, with a weight depending on the number of qualifiers in each categories, IDs, classes, tagNames.
So are we envisioning other uses cases? I can think of
- Functions which are opaque by default, and can be revealed
- Functions which are revealed by default, and can be hidden
- Functions which are always opaque even with
reveal *, unless we use their name explicitly - Functions which are always revealed even with
hide *, unless we use their name explicitly - Function which can't be made opaque, always revealed
- Functions which can't be revealed, truly black boxes
My mind is not clear on all these use cases, so perhaps could you detail a bit more why this "revealed" is now necessary and why there is no other way?
There was a problem hiding this comment.
Is it like equivalent to having automatic reveal functionName after hide * ?
Yes
perhaps could you detail a bit more why this "revealed" is now necessary and why there is no other way?
Currently Dafny does not allow its users to reference definitions from the prelude, so functions from there can not be revealed, which means they should also not be hidden using hide *. In the future, the prelude should be a Dafny library that users can see and reference, and then we could allow hiding prelude functions using hide *.
So are we envisioning other uses cases?
Indeed in the future we may want more complicated systems for hiding and revealing, but I want to wait for user feedback before designing that.
|
|
||
| procedure AlwaysRevealed() { | ||
| hide *; | ||
| assert alwaysRevealed(3) == 42; |
There was a problem hiding this comment.
| assert alwaysRevealed(3) == 42; | |
| hide alwaysRevealed; | |
| assert alwaysRevealed(3) == 42; |
Would that work too?
There was a problem hiding this comment.
Yes, although in Dafny you wouldn't be able to write this, since you can't mark any Dafny functions as being always revealed. Only the prelude functions will get this property.
Fixes #5763 Requires the upcoming Boogie version 3.2.5, for which this PR needs to be merged first: boogie-org/boogie#945 ### Description - No longer allow hiding functions from the Dafny prelude by using `hide *`. This affected recursive functions because they use `$LS` which is defined in the prelude. ### How has this been tested? - Added a CLI test-case to `revealFunctions.dfy` <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Changes
Testing
AddAssignedIdentifiers: Opaque block dafny-lang/dafny#5761Reveal.bpltest to test Always revealed