Add push, pop, hide and reveal commands (#891)

### Changes
- Add hide and reveal commands, that works together with pruning to
enable preventing specific edges in the dependency graph from being
traversed, thereby causing more to be pruned. An axiom can be marked as
`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.
- Add the `pushScope` and `popScope` commands, which represents entering
and leaving lexical scopes. Right now, these commands only influence the
behavior of `hide` and `reveal`, but in the future they may also allow
local variable shadowing.

### Testing
- Add test `Reveal.bpl` which tests the new feature
- Add test `AssumeFalseSplit.bpl`, which tests an existing piece of the
behavior of splits

.gitignore

@@ -1,5 +1,7 @@
 MSBuild_Logs/
 
+.lit_test_times.txt
+
 # Nuget
 Source/packages/
 

Source/AbstractInterpretation/NativeLattice.cs

@@ -377,6 +377,11 @@ NativeLattice.Element Step(NativeLattice lattice, Cmd cmd, NativeLattice.Element
       {
         // skip
       }
+      else if (cmd is HideRevealCmd) {
+        // skip
+      } else if (cmd is ChangeScope) {
+        // skip
+      }
       else
       {
         Contract.Assert(false); // unknown command

Source/Core/AST/Absy.cs

@@ -576,13 +576,14 @@ public override void Emit(TokenTextWriter stream, int level)
 
   public class Axiom : Declaration
   {
+    public bool CanHide { get; set; }
+
     public override string ToString()
     {
       return "Axiom: " + expression.ToString();
     }
 
-    private Expr /*!*/
-      expression;
+    private Expr /*!*/  expression;
 
     public Expr Expr
     {
@@ -606,24 +607,25 @@ void ExprInvariant()
 
     public string Comment;
 
-    public Axiom(IToken tok, Expr expr)
-      : this(tok, expr, null)
+    public Axiom(IToken tok, Expr expr, bool canHide = false)
+      : this(tok, expr, null, canHide)
     {
       Contract.Requires(expr != null);
       Contract.Requires(tok != null);
     }
 
-    public Axiom(IToken /*!*/ tok, Expr /*!*/ expr, string comment)
+    public Axiom(IToken /*!*/ tok, Expr /*!*/ expr, string comment, bool canHide = false)
       : base(tok)
     {
       Contract.Requires(tok != null);
       Contract.Requires(expr != null);
       this.expression = expr;
       Comment = comment;
+      CanHide = canHide;
     }
 
-    public Axiom(IToken tok, Expr expr, string comment, QKeyValue kv)
-      : this(tok, expr, comment)
+    public Axiom(IToken tok, Expr expr, string comment, QKeyValue kv, bool canHide = false)
+      : this(tok, expr, comment, canHide)
     {
       Contract.Requires(expr != null);
       Contract.Requires(tok != null);
@@ -3516,7 +3518,6 @@ public Block getBlock(string label)
   }
 
   public class Implementation : DeclWithFormals {
-
     public List<Variable> LocVars;
 
     [Rep] public StmtList StructuredStmts;
@@ -4447,26 +4448,31 @@ override public void ResetAbstractInterpretationState()
     /// </summary>
     public void ComputePredecessorsForBlocks()
     {
-      foreach (Block b in this.Blocks)
+      var blocks = this.Blocks;
+      foreach (Block b in blocks)
       {
         b.Predecessors = new List<Block>();
       }
 
-      foreach (Block b in this.Blocks)
-      {
-        GotoCmd gtc = b.TransferCmd as GotoCmd;
-        if (gtc != null)
+      ComputePredecessorsForBlocks(blocks);
+
+      this.BlockPredecessorsComputed = true;
+    }
+
+    public static void ComputePredecessorsForBlocks(List<Block> blocks)
+    {
+      foreach (var block in blocks) {
+        if (block.TransferCmd is not GotoCmd gtc) {
+          continue;
+        }
+
+        Contract.Assert(gtc.labelTargets != null);
+        foreach (var /*!*/ dest in gtc.labelTargets)
         {
-          Contract.Assert(gtc.labelTargets != null);
-          foreach (Block /*!*/ dest in gtc.labelTargets)
-          {
-            Contract.Assert(dest != null);
-            dest.Predecessors.Add(b);
-          }
+          Contract.Assert(dest != null);
+          dest.Predecessors.Add(block);
         }
       }
-
-      this.BlockPredecessorsComputed = true;
     }
 
     public void PruneUnreachableBlocks(CoreOptions options)

Source/Core/AST/AbsyCmd.cs

@@ -43,6 +43,9 @@ public string LabelName
 
     [Rep] private List<Cmd> /*!*/ _simpleCmds;
 
+    /// <summary>
+    /// These come before the structured command
+    /// </summary>
     public List<Cmd> /*!*/ simpleCmds
     {
       get
@@ -1189,8 +1192,7 @@ public override void Emit(TokenTextWriter stream, int level)
   // Block
   public sealed class Block : Absy
   {
-    private string /*!*/
-      label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
+    private string /*!*/ label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
 
     public string /*!*/ Label
     {
@@ -1257,8 +1259,7 @@ public int
       iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not
 
     // VC generation and SCC computation
-    public List<Block> /*!*/
-      Predecessors;
+    public List<Block> /*!*/ Predecessors;
 
     // This field is used during passification to null-out entries in block2Incarnation dictionary early
     public int succCount;
@@ -1548,6 +1549,13 @@ public static byte[] CombineChecksums(byte[] first, byte[] second, bool unordere
     }
   }
 
+  /// <summary>
+  /// Could have also been called a statement.
+  ///
+  /// Does not include commands that contain other commands,
+  /// for those, look at StructuredCmd
+  /// 
+  /// </summary>
   [ContractClass(typeof(CmdContracts))]
   public abstract class Cmd : Absy
   {

Source/Core/AST/ChangeScope.cs

@@ -0,0 +1,34 @@
+#nullable enable
+using System.Collections.Generic;
+
+namespace Microsoft.Boogie;
+
+/// <summary>
+/// Allows pushing and popping scopes inside a Boogie implementation.
+/// 
+/// Right now these scopes only affect the state of what functions are hidden and revealed using the hide and reveal keywords.
+/// However, in the future these scopes should also allow lexical scoping and variable shadowing.
+/// </summary>
+public class ChangeScope : Cmd {
+  public bool Push { get; }
+
+  public ChangeScope(IToken tok, bool push) : base(tok) {
+    Push = push;
+  }
+
+  public override void Resolve(ResolutionContext rc) {
+  }
+
+  public override void Typecheck(TypecheckingContext tc) {
+  }
+
+  public override void Emit(TokenTextWriter stream, int level) {
+  }
+
+  public override void AddAssignedVariables(List<Variable> vars) {
+  }
+
+  public override Absy StdDispatch(StandardVisitor visitor) {
+    return this;
+  }
+}

Source/Core/AST/Expression/FunctionCall.cs

@@ -45,7 +45,7 @@ void ObjectInvariant()
     Contract.Invariant(name != null);
   }
 
-  public FunctionCall createUnresolvedCopy()
+  public FunctionCall CreateUnresolvedCopy()
   {
     return new FunctionCall(new IdentifierExpr(name.tok, name.Name, name.Type));
   }
@@ -72,7 +72,7 @@ public override int GetHashCode()
     return Func.GetHashCode();
   }
 
-  virtual public void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext)
+  public virtual void Emit(IList<Expr> args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext)
   {
     //Contract.Requires(stream != null);
     //Contract.Requires(args != null);

Source/Core/AST/HideRevealCmd.cs

@@ -0,0 +1,54 @@
+#nullable enable
+using System.Collections.Generic;
+
+namespace Microsoft.Boogie;
+
+/// <summary>
+/// Can be used to hide or reveal a specific function, or all functions
+/// If pruning is turned on, a hidden function will be pruned despite being referenced in a Boogie implementation.
+/// The function is only partially pruned though: the function definition itself is kept, and only axioms
+/// that the function depends on, that are marked as hideable, are pruned.
+///
+/// Hide and revealing takes into account lexical scoping:
+/// 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; }
+  private readonly FunctionCall? functionCall;
+
+  public HideRevealCmd(IToken tok, bool hide) : base(tok) {
+    this.Hide = hide;
+  }
+
+  public HideRevealCmd(IdentifierExpr name, bool hide) : base(name.tok) {
+    this.Hide = hide;
+    this.functionCall = new FunctionCall(name);
+  }
+
+  public Function? Function => functionCall?.Func;
+
+  public override void Resolve(ResolutionContext rc)
+  {
+    functionCall?.Resolve(rc, null);
+  }
+
+  public override void Typecheck(TypecheckingContext tc)
+  {
+  }
+
+  public override void Emit(TokenTextWriter stream, int level)
+  {
+    stream.Write(this, level, Hide ? "hide " : "reveal ");
+    stream.Write(this, level, Function == null ? "*" : Function.Name);
+    stream.WriteLine(";");
+  }
+
+  public override void AddAssignedVariables(List<Variable> vars)
+  {
+  }
+
+  public override Absy StdDispatch(StandardVisitor visitor)
+  {
+    return visitor.VisitRevealCmd(this);
+  }
+}

Source/Core/BoogiePL.atg

@@ -564,11 +564,16 @@ VarOrType<out TypedIdent/*!*/ tyd, out QKeyValue kv>
 
 /*------------------------------------------------------------------------*/
 Axiom<out Axiom/*!*/ m>
-= (.Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null; .)
+= (.
+    Contract.Ensures(Contract.ValueAtReturn(out m) != null); 
+    Expr/*!*/ e; 
+    QKeyValue kv = null; 
+    bool canHide = false; .)
+  [ "hideable" (. canHide = true; .) ]
   "axiom"
    { Attribute<ref kv> }
    (. IToken/*!*/ x = t; .)
-  Proposition<out e> ";"  (. m = new Axiom(x,e, null, kv); .)
+  Proposition<out e> ";"  (. m = new Axiom(x,e, null, kv, canHide); .)
   .
 
 /*------------------------------------------------------------------------*/
@@ -1110,8 +1115,24 @@ LabelOrCmd<out Cmd c, out IToken label>
      c = dummyCmd;  label = null;
      Cmd/*!*/ cn;
      QKeyValue kv = null;
+     bool isHide;
+     IdentifierExpr hideRevealId = null;
   .)
-  ( LabelOrAssign<out c, out label>
+  ( (
+      ( "reveal" (. isHide = false; .) 
+      | "hide"   (. isHide = true;  .)
+      )
+      ( ident    (. hideRevealId = new IdentifierExpr(t, t.val); .)
+      | "*"
+      )
+      (. c = hideRevealId == null ? new HideRevealCmd(t, isHide) : new HideRevealCmd(hideRevealId, isHide); .)
+      ";"
+    )
+  | LabelOrAssign<out c, out label>
+  | "popScope"            (. c = new ChangeScope(t, false); .)
+    ";"
+  | "pushScope"           (. c = new ChangeScope(t, true); .)
+    ";"
   | "assert"              (. x = t; .)
     { Attribute<ref kv> }
     Proposition<out e>    (. c = new AssertCmd(x, e, kv); .)
@@ -1682,17 +1703,17 @@ Attribute<ref QKeyValue kv>
 
 AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>
 = (. IToken/*!*/ tok;  Expr/*!*/ e;  List<Expr>/*!*/ es;
-     string key;
+     IToken id;
      List<object/*!*/> parameters;  object/*!*/ param;
   .)
   "{"                                         (. tok = t; .)
      (
-       ":" ident                              (. key = t.val;  parameters = new List<object/*!*/>(); .)
+       ":" Ident<out id>                      (. parameters = new List<object/*!*/>(); .)
        [ AttributeParameter<out param>        (. parameters.Add(param); .)
          { "," AttributeParameter<out param>  (. parameters.Add(param); .)
          }
        ]
-       (. if (key == "nopats") {
+       (. if (id.val == "nopats") {
             if (parameters.Count == 1 && parameters[0] is Expr) {
               e = (Expr)parameters[0];
               if(trig==null){
@@ -1705,9 +1726,9 @@ AttributeOrTrigger<ref QKeyValue kv, ref Trigger trig>
             }
           } else {
             if (kv==null) {
-              kv = new QKeyValue(tok, key, parameters, null);
+              kv = new QKeyValue(tok, id.val, parameters, null);
             } else {
-              kv.AddLast(new QKeyValue(tok, key, parameters, null));
+              kv.AddLast(new QKeyValue(tok, id.val, parameters, null));
             }
           }
        .)
@@ -1812,6 +1833,7 @@ Ident<out IToken/*!*/ x>
   | "both"     (. t.kind = _ident; .) // convert to ident
   | "left"     (. t.kind = _ident; .) // convert to ident
   | "right"    (. t.kind = _ident; .) // convert to ident
+  | "hide"     (. t.kind = _ident; .) // convert to ident
   )
   (.
     x = t;

Source/Core/CoreOptions.cs

@@ -3,7 +3,6 @@
 
 namespace Microsoft.Boogie
 {
-
   /// <summary>
   /// Boogie command-line options (other tools can subclass this class in order to support a
   /// superset of Boogie's options).

Source/Core/DeadVarElim.cs

@@ -699,6 +699,11 @@ public void Propagate(Cmd cmd, HashSet<Variable /*!*/> /*!*/ liveSet)
       else if (cmd is CommentCmd)
       {
         // comments are just for debugging and don't affect verification
+      } else if (cmd is HideRevealCmd)
+      {
+        // reveal references no variables
+      } else if (cmd is ChangeScope)
+      {
       }
       else if (cmd is SugaredCmd)
       {