Refactoring related to https://github.com/boogie-org/boogie/pull/891

Source/Core/AST/Absy.cs

@@ -3521,7 +3521,12 @@ public class Implementation : DeclWithFormals {
     public List<Variable> LocVars;
 
     [Rep] public StmtList StructuredStmts;
-    [Rep] public List<Block> Blocks;
+
+    [field: Rep]
+    public List<Block> Blocks {
+      get; 
+      set;
+    }
     public Procedure Proc;
 
     // Blocks before applying passification etc.
@@ -4477,47 +4482,36 @@ public static void ComputePredecessorsForBlocks(List<Block> blocks)
 
     public void PruneUnreachableBlocks(CoreOptions options)
     {
-      ArrayList /*Block!*/
-        visitNext = new ArrayList /*Block!*/();
-      List<Block /*!*/> reachableBlocks = new List<Block /*!*/>();
-      HashSet<Block> reachable = new HashSet<Block>(); // the set of elements in "reachableBlocks"
+      var toVisit = new Stack<Block>();
+      var reachableBlocks = new List<Block /*!*/>();
+      var reachable = new HashSet<Block>(); // the set of elements in "reachableBlocks"
 
-      visitNext.Add(this.Blocks[0]);
-      while (visitNext.Count != 0)
+      toVisit.Push(Blocks[0]);
+      while (toVisit.Count != 0)
       {
-        Block b = cce.NonNull((Block) visitNext[visitNext.Count - 1]);
-        visitNext.RemoveAt(visitNext.Count - 1);
-        if (!reachable.Contains(b))
-        {
-          reachableBlocks.Add(b);
-          reachable.Add(b);
-          if (b.TransferCmd is GotoCmd)
-          {
-            if (options.PruneInfeasibleEdges)
-            {
-              foreach (Cmd /*!*/ s in b.Cmds)
-              {
-                Contract.Assert(s != null);
-                if (s is PredicateCmd)
-                {
-                  LiteralExpr e = ((PredicateCmd) s).Expr as LiteralExpr;
-                  if (e != null && e.IsFalse)
-                  {
-                    // This statement sequence will never reach the end, because of this "assume false" or "assert false".
-                    // Hence, it does not reach its successors.
-                    b.TransferCmd = new ReturnCmd(b.TransferCmd.tok);
-                    goto NEXT_BLOCK;
-                  }
-                }
+        var block = toVisit.Pop();
+        if (!reachable.Add(block)) {
+          continue;
+        }
+
+        reachableBlocks.Add(block);
+        if (block.TransferCmd is GotoCmd gotoCmd) {
+          if (options.PruneInfeasibleEdges) {
+            foreach (var command in block.Cmds) {
+              Contract.Assert(command != null);
+              if (command is PredicateCmd { Expr: LiteralExpr { IsFalse: true } }) {
+                // This statement sequence will never reach the end, because of this "assume false" or "assert false".
+                // Hence, it does not reach its successors.
+                block.TransferCmd = new ReturnCmd(block.TransferCmd.tok);
+                goto NEXT_BLOCK;
               }
             }
+          }
 
-            // it seems that the goto statement at the end may be reached
-            foreach (Block succ in cce.NonNull((GotoCmd) b.TransferCmd).labelTargets)
-            {
-              Contract.Assume(succ != null);
-              visitNext.Add(succ);
-            }
+          // it seems that the goto statement at the end may be reached
+          foreach (var next in gotoCmd.labelTargets) {
+            Contract.Assume(next != null);
+            toVisit.Push(next);
           }
         }
 

Source/Core/AST/AbsyCmd.cs

@@ -264,8 +264,7 @@ public bool PrefixFirstBlock([Captured] List<Cmd> prefixCmds, ref string suggest
   /// </summary>
   public class StmtListBuilder
   {
-    List<BigBlock /*!*/> /*!*/
-      bigBlocks = new List<BigBlock /*!*/>();
+    readonly List<BigBlock /*!*/> /*!*/ bigBlocks = new();
 
     string label;
     List<Cmd> simpleCmds;
@@ -858,16 +857,16 @@ void CreateBlocks(StmtList stmtList, string runOffTheEndLabel)
             }
 
             // ... goto Then, Else;
-            Block block = new Block(b.tok, predLabel, predCmds,
+            var jumpBlock = new Block(b.tok, predLabel, predCmds,
               new GotoCmd(ifcmd.tok, new List<String> {thenLabel, elseLabel}));
-            blocks.Add(block);
+            blocks.Add(jumpBlock);
 
             if (!thenGuardTakenCareOf)
             {
               // Then: assume guard; goto firstThenBlock;
-              block = new Block(ifcmd.tok, thenLabel, ssThen,
+              var thenJumpBlock = new Block(ifcmd.tok, thenLabel, ssThen,
                 new GotoCmd(ifcmd.tok, new List<String> {ifcmd.thn.BigBlocks[0].LabelName}));
-              blocks.Add(block);
+              blocks.Add(thenJumpBlock);
             }
 
             // recurse to create the blocks for the then branch
@@ -879,9 +878,9 @@ void CreateBlocks(StmtList stmtList, string runOffTheEndLabel)
               if (!elseGuardTakenCareOf)
               {
                 // Else: assume !guard; goto firstElseBlock;
-                block = new Block(ifcmd.tok, elseLabel, ssElse,
+                var elseJumpBlock = new Block(ifcmd.tok, elseLabel, ssElse,
                   new GotoCmd(ifcmd.tok, new List<String> {ifcmd.elseBlock.BigBlocks[0].LabelName}));
-                blocks.Add(block);
+                blocks.Add(elseJumpBlock);
               }
 
               // recurse to create the blocks for the else branch
@@ -914,7 +913,7 @@ void CreateBlocks(StmtList stmtList, string runOffTheEndLabel)
                 trCmd = GotoSuccessor(ifcmd.tok, b);
               }
 
-              block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd);
+              var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd);
               blocks.Add(block);
             }
           }

Source/Core/AST/ChangeScope.cs

@@ -10,10 +10,11 @@ namespace Microsoft.Boogie;
 /// However, in the future these scopes should also allow lexical scoping and variable shadowing.
 /// </summary>
 public class ChangeScope : Cmd {
-  public bool Push { get; }
+  public enum Modes { Push, Pop }
+  public Modes Mode { get; }
 
-  public ChangeScope(IToken tok, bool push) : base(tok) {
-    Push = push;
+  public ChangeScope(IToken tok, Modes mode) : base(tok) {
+    Mode = mode;
   }
 
   public override void Resolve(ResolutionContext rc) {
@@ -29,6 +30,6 @@ public override void AddAssignedVariables(List<Variable> vars) {
   }
 
   public override Absy StdDispatch(StandardVisitor visitor) {
-    return this;
+    return visitor.VisitChangeScopeCmd(this);
   }
 }

Source/Core/AST/HideRevealCmd.cs

@@ -13,15 +13,16 @@ namespace Microsoft.Boogie;
 /// 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; }
+  public enum Modes { Hide, Reveal }
+  public Modes Mode { get; }
   private readonly FunctionCall? functionCall;
 
-  public HideRevealCmd(IToken tok, bool hide) : base(tok) {
-    this.Hide = hide;
+  public HideRevealCmd(IToken tok, Modes mode) : base(tok) {
+    this.Mode = mode;
   }
 
-  public HideRevealCmd(IdentifierExpr name, bool hide) : base(name.tok) {
-    this.Hide = hide;
+  public HideRevealCmd(IdentifierExpr name, Modes mode) : base(name.tok) {
+    this.Mode = mode;
     this.functionCall = new FunctionCall(name);
   }
 
@@ -38,8 +39,8 @@ 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.Write(this, level, Mode == Modes.Hide ? "hide " : "reveal ");
+    stream.Write(this, functionCall == null ? "*" : functionCall.FunctionName);
     stream.WriteLine(";");
   }
 

Source/Core/BoogiePL.atg

@@ -1115,24 +1115,24 @@ LabelOrCmd<out Cmd c, out IToken label>
      c = dummyCmd;  label = null;
      Cmd/*!*/ cn;
      QKeyValue kv = null;
-     bool isHide;
+     HideRevealCmd.Modes mode;
      IdentifierExpr hideRevealId = null;
   .)
   ( (
-      ( "reveal" (. isHide = false; .) 
-      | "hide"   (. isHide = true;  .)
+      ( "reveal" (. mode = HideRevealCmd.Modes.Reveal; .) 
+      | "hide"   (. mode = HideRevealCmd.Modes.Hide;  .)
       )
       ( ident    (. hideRevealId = new IdentifierExpr(t, t.val); .)
       | "*"
       )
-      (. c = hideRevealId == null ? new HideRevealCmd(t, isHide) : new HideRevealCmd(hideRevealId, isHide); .)
+      (. c = hideRevealId == null ? new HideRevealCmd(t, mode) : new HideRevealCmd(hideRevealId, mode); .)
       ";"
     )
-  | LabelOrAssign<out c, out label>
-  | "popScope"            (. c = new ChangeScope(t, false); .)
+  | "pop"            (. c = new ChangeScope(t, ChangeScope.Modes.Pop); .)
     ";"
-  | "pushScope"           (. c = new ChangeScope(t, true); .)
+  | "push"           (. c = new ChangeScope(t, ChangeScope.Modes.Push); .)
     ";"
+  | LabelOrAssign<out c, out label>
   | "assert"              (. x = t; .)
     { Attribute<ref kv> }
     Proposition<out e>    (. c = new AssertCmd(x, e, kv); .)
@@ -1833,7 +1833,10 @@ 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
+  | "reveal"     (. t.kind = _ident; .) // convert to ident
   | "hide"     (. t.kind = _ident; .) // convert to ident
+  | "push"     (. t.kind = _ident; .) // convert to ident
+  | "pop"     (. t.kind = _ident; .) // convert to ident
   )
   (.
     x = t;