Add pushScope, popScope, hide and reveal commands

.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)
       {