Add pushScope, popScope, hide and reveal commands
#891
Conversation
keyboardDrummer
changed the title
push, pop, hide and reveal` commands
keyboardDrummer
changed the title
push, pop, hide and reveal` commandspush, pop, hide and reveal commands
keyboardDrummer
changed the title
push, pop, hide and reveal commandspushScope, popScope, hide and reveal commands
| /// However, in the future these scopes should also allow lexical scoping and variable shadowing. | ||
| /// </summary> | ||
| public class ChangeScope : Cmd { | ||
| public bool Push { get; } |
There was a problem hiding this comment.
An enum of Push and Pop would be a bit nicer than a bool here.
| /// A popScope command will undo any hide and reveal operations that came after the last pushScope command. | ||
| /// </summary> | ||
| public class HideRevealCmd : Cmd { | ||
| public bool Hide { get; } |
There was a problem hiding this comment.
Similar to push/pop, an enum would be nicer than a bool here.
| @@ -81,6 +81,13 @@ public virtual Cmd VisitAssertCmd(AssertCmd node) | |||
| VisitAttributes(node); | |||
| return node; | |||
| } | |||
|
|
|||
| public virtual Cmd VisitRevealCmd(HideRevealCmd node) | |||
There was a problem hiding this comment.
Do you not need a method for ChangeScope here, too?
| @@ -1421,6 +1421,12 @@ private void AddDebugInfo(Cmd c, Dictionary<Variable, Expr> incarnationMap, List | |||
| else if (c is CommentCmd) | |||
| { | |||
| // comments are just for debugging and don't affect verification | |||
| } else if (c is HideRevealCmd) | |||
| { | |||
| passiveCmds.Add(c); | |||
There was a problem hiding this comment.
The fact that these stick around until the passive stage is unfortunate, in the sense that it's nice for that set of commands to be as small as possible, but I think it's also necessary for the goal of this PR.
There was a problem hiding this comment.
Seems fine to me :-) They are used only in the passive stage.
| Expr/*!*/ e; | ||
| QKeyValue kv = null; | ||
| bool canHide = false; .) | ||
| [ "hideable" (. canHide = true; .) ] |
There was a problem hiding this comment.
I might be more inclined to make this an attribute than a keyword, though I don't have a super strong opinion about that.
There was a problem hiding this comment.
I thought about that, especially since adding a parsing keyword is more difficult implementation wise, but I can't really defend introducing keywords for half a feature and not for the other half.
| ";" | ||
| ) | ||
| | LabelOrAssign<out c, out label> | ||
| | "popScope" (. c = new ChangeScope(t, false); .) |
There was a problem hiding this comment.
I don't think anything else in Boogie, the language, uses camel case like this. I'd maybe prefer just push and pop. The word Scope doesn't really tell you what kind of scope it is, so I'm not sure it adds much.
| /// <summary> | ||
| /// Allows defining dataflow analysis | ||
| /// </summary> | ||
| abstract class DataflowAnalysis<TNode, TState> { |
There was a problem hiding this comment.
This is simple enough that it might not provide a benefit, but have you looked at whether this can be a special case of what's defined in the AbstractInterpretation project? Dataflow analysis is generally a special case of abstract interpretation.
There was a problem hiding this comment.
I had a look at that package but it's a but hard to see how to extract what I need from there. Also, there isn't much code to deduplicate, since this DataflowAnalysis is tiny and all it really needs that could already be defined somewhere else, is a control flow graph with Cmd as a Node.
Changes
hideable. The hide and reveal commands can hide or reveal a set of functions, a state which is maintained throughout the execution of a Boogie implementation. During pruning, if a live but hidden function uses a hideable axiom, then the axiom will not be made live.pushScopeandpopScopecommands, which represents entering and leaving lexical scopes. Right now, these commands only influence the behavior ofhideandreveal, but in the future they may also allow local variable shadowing, which would reduce the translation burden of downstream tools.Testing
Reveal.bplwhich tests the new featureAssumeFalseSplit.bpl, which tests an existing piece of the behavior of splits