Further refactoring

Source/Core/AST/BigBlocksResolutionContext.cs

@@ -33,7 +33,7 @@ void ObjectInvariant()
     Contract.Invariant(ErrorHandler != null);
   }
 
-  public void ComputeAllLabels(StmtList stmts)
+  private void ComputeAllLabels(StmtList stmts)
   {
     if (stmts == null)
     {
@@ -47,18 +47,16 @@ public void ComputeAllLabels(StmtList stmts)
         allLabels.Add(bb.LabelName);
       }
 
-      bb.ec?.ComputeAllLabels(this);
-    }
-  }
-
-  private void ComputeAllLabels(StructuredCmd cmd)
-  {
-    if (cmd == null)
-    {
-      return;
+      if (bb.ec == null)
+      {
+        continue;
+      }
+      
+      foreach (var list in bb.ec.StatementLists)
+      {
+        ComputeAllLabels(list);
+      }
     }
-
-    cmd.ComputeAllLabels(this);
   }
 
   public BigBlocksResolutionContext(StmtList stmtList, Errors errorHandler)
@@ -194,50 +192,22 @@ void NameAnonymousBlocks(StmtList stmtList)
         b.LabelName = FreshPrefix();
       }
 
-      if (b.ec is WhileCmd)
+      foreach (var l in b.ec.StatementLists)
       {
-        WhileCmd wcmd = (WhileCmd) b.ec;
-        NameAnonymousBlocks(wcmd.Body);
-      }
-      else
-      {
-        for (IfCmd ifcmd = b.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf)
-        {
-          NameAnonymousBlocks(ifcmd.thn);
-          if (ifcmd.elseBlock != null)
-          {
-            NameAnonymousBlocks(ifcmd.elseBlock);
-          }
-        }
+        NameAnonymousBlocks(l);
       }
     }
   }
 
-  void RecordSuccessors(StmtList stmtList, BigBlock successor)
+  public void RecordSuccessors(StmtList stmtList, BigBlock successor)
   {
     Contract.Requires(stmtList != null);
     for (int i = stmtList.BigBlocks.Count; 0 <= --i;)
     {
       BigBlock big = stmtList.BigBlocks[i];
       big.successorBigBlock = successor;
 
-      if (big.ec is WhileCmd)
-      {
-        WhileCmd wcmd = (WhileCmd) big.ec;
-        RecordSuccessors(wcmd.Body, big);
-      }
-      else
-      {
-        for (IfCmd ifcmd = big.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf)
-        {
-          RecordSuccessors(ifcmd.thn, successor);
-          if (ifcmd.elseBlock != null)
-          {
-            RecordSuccessors(ifcmd.elseBlock, successor);
-          }
-        }
-      }
-
+      big.ec.RecordSuccessors(this, big);
       successor = big;
     }
   }
@@ -293,7 +263,7 @@ public void CreateBlocks(StmtList stmtList, string runOffTheEndLabel)
       }
       else
       {
-        b.ec.CreateBlocks(this, b, theSimpleCmds, stmtList, n == 0 ? runOffTheEndLabel : null);
+        b.ec.CreateBlocks(this, b, theSimpleCmds, n == 0 ? runOffTheEndLabel : null);
       }
     }
   }

Source/Core/AST/StructuredCommands/BreakCmd.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 
 namespace Microsoft.Boogie;
 
@@ -84,15 +85,16 @@ public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtLi
     }
   }
 
-  public override void ComputeAllLabels(BigBlocksResolutionContext context)
-  {
-  }
-
-  public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List<Cmd> theSimpleCmds, StmtList stmtList,
+  public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List<Cmd> theSimpleCmds,
     string runOffTheEndLabel)
   {
     Contract.Assert(this.BreakEnclosure != null);
-    Block block = new Block(b.tok, b.LabelName, theSimpleCmds, BigBlocksResolutionContext.GotoSuccessor(b.ec.tok, BreakEnclosure));
+    Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds, BigBlocksResolutionContext.GotoSuccessor(bigBlock.ec.tok, BreakEnclosure));
     context.AddBlock(block);
   }
+
+  public override IEnumerable<StmtList> StatementLists => Enumerable.Empty<StmtList>();
+  public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock)
+  {
+  }
 }

Source/Core/AST/StructuredCommands/ByProofCmd.cs

@@ -26,13 +26,14 @@ public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtLi
     throw new System.NotImplementedException();
   }
 
-  public override void ComputeAllLabels(BigBlocksResolutionContext context)
+  public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List<Cmd> theSimpleCmds,
+    string runOffTheEndLabel)
   {
     throw new System.NotImplementedException();
   }
 
-  public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List<Cmd> theSimpleCmds, StmtList stmtList,
-    string runOffTheEndLabel)
+  public override IEnumerable<StmtList> StatementLists => new[] { Body, Proof };
+  public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock)
   {
     throw new System.NotImplementedException();
   }

Source/Core/AST/StructuredCommands/IfCmd.cs

@@ -134,18 +134,11 @@ public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtLi
     }
   }
 
-  public override void ComputeAllLabels(BigBlocksResolutionContext context)
-  {
-    context.ComputeAllLabels(thn);
-    elseIf.ComputeAllLabels(context);
-    context.ComputeAllLabels(elseBlock);
-  }
-
-  public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List<Cmd> theSimpleCmds, StmtList stmtList,
+  public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List<Cmd> theSimpleCmds,
     string runOffTheEndLabel)
   {
-    IfCmd ifcmd = (IfCmd) b.ec;
-    string predLabel = b.LabelName;
+    IfCmd ifcmd = (IfCmd) bigBlock.ec;
+    string predLabel = bigBlock.LabelName;
     List<Cmd> predCmds = theSimpleCmds;
 
     for (; ifcmd != null; ifcmd = ifcmd.elseIf)
@@ -178,7 +171,7 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b
       }
 
       // ... goto Then, Else;
-      var jumpBlock = new Block(b.tok, predLabel, predCmds,
+      var jumpBlock = new Block(bigBlock.tok, predLabel, predCmds,
         new GotoCmd(ifcmd.tok, new List<String> {thenLabel, elseLabel}));
       context.AddBlock(jumpBlock);
 
@@ -231,12 +224,38 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b
         }
         else
         {
-          trCmd = BigBlocksResolutionContext.GotoSuccessor(ifcmd.tok, b);
+          trCmd = BigBlocksResolutionContext.GotoSuccessor(ifcmd.tok, bigBlock);
         }
 
         var block = new Block(ifcmd.tok, elseLabel, ssElse, trCmd);
         context.AddBlock(block);
       }
     }
   }
+
+  public override IEnumerable<StmtList> StatementLists {
+    get
+    {
+      for (var ifcmd = this; ifcmd != null; ifcmd = ifcmd.elseIf)
+      {
+        yield return ifcmd.thn;
+        if (ifcmd.elseBlock != null)
+        {
+          yield return ifcmd.elseBlock;
+        }
+      }
+    }
+  }
+
+  public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock)
+  {
+    for (var ifcmd = this; ifcmd != null; ifcmd = ifcmd.elseIf)
+    {
+      context.RecordSuccessors(ifcmd.thn, bigBlock.successorBigBlock);
+      if (ifcmd.elseBlock != null)
+      {
+        context.RecordSuccessors(ifcmd.elseBlock, bigBlock.successorBigBlock);
+      }
+    }
+  }
 }

Source/Core/AST/StructuredCommands/StructuredCmd.cs

@@ -39,8 +39,10 @@ public StructuredCmd(IToken tok)
 
   public abstract void InjectEmptyBigBlockInsideWhileLoopBody(BigBlocksResolutionContext context);
   public abstract void CheckLegalLabels(BigBlocksResolutionContext context, StmtList stmtList, BigBlock bigBlock);
-  public abstract void ComputeAllLabels(BigBlocksResolutionContext context);
-  public abstract void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List<Cmd> theSimpleCmds,
-    StmtList stmtList,
+
+  public abstract void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List<Cmd> theSimpleCmds,
     string runOffTheEndLabel);
+
+  public abstract IEnumerable<StmtList> StatementLists { get; }
+  public abstract void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock);
 }

Source/Core/AST/StructuredCommands/WhileCmd.cs

@@ -92,13 +92,7 @@ public override void CheckLegalLabels(BigBlocksResolutionContext context, StmtLi
     context.CheckLegalLabels(Body, stmtList, bigBlock);
   }
 
-  public override void ComputeAllLabels(BigBlocksResolutionContext context)
-  {
-    context.ComputeAllLabels(Body);
-  }
-
-  public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b, List<Cmd> theSimpleCmds,
-    StmtList stmtList,
+  public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock bigBlock, List<Cmd> theSimpleCmds,
     string runOffTheEndLabel)
   {
       WhileCmd wcmd = (WhileCmd) this;
@@ -124,7 +118,7 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b
       bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel);
 
       // ... goto LoopHead;
-      Block block = new Block(b.tok, b.LabelName, theSimpleCmds,
+      Block block = new Block(bigBlock.tok, bigBlock.LabelName, theSimpleCmds,
         new GotoCmd(wcmd.tok, new List<String> {loopHeadLabel}));
       context.AddBlock(block);
 
@@ -163,10 +157,16 @@ public override void CreateBlocks(BigBlocksResolutionContext context, BigBlock b
       }
       else
       {
-        trCmd = BigBlocksResolutionContext.GotoSuccessor(wcmd.tok, b);
+        trCmd = BigBlocksResolutionContext.GotoSuccessor(wcmd.tok, bigBlock);
       }
 
       block = new Block(wcmd.tok, loopDoneLabel, ssDone, trCmd);
       context.AddBlock(block);
   }
+
+  public override IEnumerable<StmtList> StatementLists => new [] { Body };
+  public override void RecordSuccessors(BigBlocksResolutionContext context, BigBlock bigBlock)
+  {
+    context.RecordSuccessors(Body, bigBlock);
+  }
 }