Use IList<Block> instead of List<Block> for Implementation

Source/AbstractInterpretation/NativeLattice.cs

@@ -185,8 +185,7 @@ public void Analyze(Implementation impl, NativeLattice lattice, NativeLattice.El
       // We need to keep track of some information for each(some) block(s).  To do that efficiently,
       // we number the implementation's blocks sequentially, and then we can use arrays to store
       // the additional information.
-      var pre = new NativeLattice.Element[impl.Blocks
-        .Count]; // set to null if we never compute a join/widen at this block
+      var pre = new NativeLattice.Element[impl.Blocks.Count]; // set to null if we never compute a join/widen at this block
       var post = options.InstrumentInfer == CoreOptions.InstrumentationPlaces.Everywhere
         ? new NativeLattice.Element[impl.Blocks.Count]
         : null;

Source/Concurrency/YieldingProcInstrumentation.cs

@@ -551,7 +551,9 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
       impl.Blocks.Add(unchangedCheckerBlock);
       impl.Blocks.Add(returnCheckerBlock);
       impl.Blocks.Add(returnBlock);
-      impl.Blocks.AddRange(implRefinementCheckingBlocks);
+      foreach (var block in implRefinementCheckingBlocks) {
+        impl.Blocks.Add(block);
+      }
       impl.Blocks.Insert(0, CreateInitialBlock(impl, preconditions));
     }
 
@@ -608,7 +610,9 @@ private void SplitBlocks(Implementation impl)
         b.TransferCmd = currTransferCmd;
       }
 
-      impl.Blocks.AddRange(newBlocks);
+      foreach (var newBlock in newBlocks) {
+        impl.Blocks.Add(newBlock);
+      }
     }
 
     private Block CreateNoninterferenceCheckerBlock()

Source/Core/AST/Expression/AbsyExpr.cs

@@ -3890,7 +3890,7 @@ public class CodeExpr : Expr
     public List<Variable> /*!*/
       LocVars;
 
-    [Rep] public List<Block /*!*/> /*!*/ Blocks;
+    [Rep] public IList<Block /*!*/> /*!*/ Blocks;
 
     [ContractInvariantMethod]
     void ObjectInvariant()

Source/Core/AST/Implementation.cs

@@ -10,18 +10,19 @@ namespace Microsoft.Boogie;
 public class Implementation : DeclWithFormals {
   public List<Variable> LocVars;
 
-  [Rep] public StmtList StructuredStmts;
+  [Rep] 
+  public StmtList StructuredStmts { get; set; }
 
-  [field: Rep]
-  public List<Block> Blocks {
+  [Rep]
+  public IList<Block> Blocks {
     get; 
     set;
   }
   public Procedure Proc;
 
   // Blocks before applying passification etc.
   // Both are used only when /inline is set.
-  public List<Block> OriginalBlocks;
+  public IList<Block> OriginalBlocks;
   public List<Variable> OriginalLocVars;
 
   // Map filled in during passification to allow augmented error trace reporting
@@ -965,7 +966,7 @@ public void ComputePredecessorsForBlocks()
     this.BlockPredecessorsComputed = true;
   }
 
-  public static void ComputePredecessorsForBlocks(List<Block> blocks)
+  public static void ComputePredecessorsForBlocks(IList<Block> blocks)
   {
     foreach (var block in blocks) {
       if (block.TransferCmd is not GotoCmd gtc) {

Source/Core/AST/Program.cs

@@ -498,7 +498,7 @@ public static Graph<Implementation> BuildCallGraph(CoreOptions options, Program
     return callGraph;
   }
 
-  public static Graph<Block> GraphFromBlocksSubset(IReadOnlyList<Block> blocks, IReadOnlySet<Block> subset = null, bool forward = true)
+  public static Graph<Block> GraphFromBlocksSubset(IList<Block> blocks, IReadOnlySet<Block> subset = null, bool forward = true)
   {
     var result = new Graph<Block>();
     if (!blocks.Any())
@@ -529,7 +529,7 @@ void AddEdge(Block a, Block b) {
     return result;
   }
 
-  public static Graph<Block> GraphFromBlocks(IReadOnlyList<Block> blocks, bool forward = true) {
+  public static Graph<Block> GraphFromBlocks(IList<Block> blocks, bool forward = true) {
     return GraphFromBlocksSubset(blocks, null, forward);
   }
 

Source/Core/Analysis/BlockCoalescer.cs

@@ -85,7 +85,7 @@ public static void CoalesceInPlace(List<Block> blocks) {
     blocks.AddRange(coalesced);
   }
 
-  public static List<Block> CoalesceFromRootBlock(List<Block> blocks)
+  public static IList<Block> CoalesceFromRootBlock(IList<Block> blocks)
   {
     if (!blocks.Any())
     {

Source/Core/Duplicator.cs

@@ -142,7 +142,7 @@ public override List<Block> VisitBlockSeq(List<Block> blockSeq)
       return base.VisitBlockSeq(new List<Block>(blockSeq));
     }
 
-    public override List<Block /*!*/> /*!*/ VisitBlockList(List<Block /*!*/> /*!*/ blocks)
+    public override IList<Block> /*!*/ VisitBlockList(IList<Block> blocks /*!*/ /*!*/)
     {
       //Contract.Requires(cce.NonNullElements(blocks));
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

Source/Core/Inline.cs

@@ -354,7 +354,7 @@ private int InlineCallCmd(Block block, CallCmd callCmd, Implementation impl, Lis
       return nextlblCount;
     }
 
-    public virtual List<Block /*!*/> /*!*/ DoInlineBlocks(List<Block /*!*/> /*!*/ blocks, ref bool inlinedSomething)
+    public virtual List<Block /*!*/> /*!*/ DoInlineBlocks(IList<Block /*!*/> /*!*/ blocks, ref bool inlinedSomething)
     {
       Contract.Requires(cce.NonNullElements(blocks));
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
@@ -625,8 +625,7 @@ private List<Cmd> RemoveAsserts(List<Cmd> cmds)
       Contract.Requires(codeCopier.oldSubstMap != null);
 
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
-      List<Block /*!*/> /*!*/
-        implBlocks = cce.NonNull(impl.OriginalBlocks);
+      var /*!*/ implBlocks = cce.NonNull(impl.OriginalBlocks);
       Contract.Assert(implBlocks.Count > 0);
 
       Procedure proc = impl.Proc;

Source/Core/StandardVisitor.cs

@@ -219,7 +219,7 @@ public virtual List<Block> VisitBlockSeq(List<Block> blockSeq)
       return blockSeq;
     }
 
-    public virtual List<Block /*!*/> /*!*/ VisitBlockList(List<Block /*!*/> /*!*/ blocks)
+    public virtual IList<Block> /*!*/ VisitBlockList(IList<Block> blocks /*!*/ /*!*/)
     {
       Contract.Requires(blocks != null);
       Contract.Ensures(Contract.Result<List<Block>>() != null);
@@ -1150,14 +1150,12 @@ public override List<Block> VisitBlockSeq(List<Block> blockSeq)
       return blockSeq;
     }
 
-    public override List<Block /*!*/> /*!*/ VisitBlockList(List<Block /*!*/> /*!*/ blocks)
+    public override IList<Block> /*!*/ VisitBlockList(IList<Block> blocks /*!*/ /*!*/)
     {
       Contract.Ensures(Contract.Result<List<Block>>() == blocks);
-      for (int i = 0, n = blocks.Count; i < n; i++)
-      {
-        this.VisitBlock(blocks[i]);
+      foreach (var block in blocks) {
+        this.VisitBlock(block);
       }
-
       return blocks;
     }
 

Source/Provers/LeanAuto/LeanAutoGenerator.cs

@@ -879,7 +879,7 @@ public override List<Block> VisitBlockSeq(List<Block> blockSeq)
     throw new LeanConversionException(Token.NoToken, $"Internal: List<Block> should never be directly visited ({blockSeq}).");
   }
 
-  public override List<Block> VisitBlockList(List<Block> blocks)
+  public override IList<Block> VisitBlockList(IList<Block> blocks)
   {
     throw new LeanConversionException(Token.NoToken, $"Internal: List<Block> should never be directly visited ({blocks}).");
   }

Source/Provers/SMTLib/SMTLibProcess.cs

@@ -69,7 +69,7 @@ public SMTLibProcess(SMTLibOptions libOptions, SMTLibSolverOptions options)
       }
       catch (System.ComponentModel.Win32Exception e)
       {
-        throw new ProverException(string.Format("Unable to start the process {0}: {1}", psi.FileName, e.Message));
+        throw new ProverException($"Unable to start the process {psi.FileName}: {e.Message}");
       }
     }
 

Source/VCExpr/Boogie2VCExpr.cs

@@ -889,7 +889,7 @@ public override List<Block> VisitBlockSeq(List<Block> blockSeq)
       throw new cce.UnreachableException();
     }
 
-    public override List<Block /*!*/> /*!*/ VisitBlockList(List<Block /*!*/> /*!*/ blocks)
+    public override IList<Block> /*!*/ VisitBlockList(IList<Block> blocks /*!*/ /*!*/)
     {
       //Contract.Requires(cce.NonNullElements(blocks));
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

Source/VCGeneration/BlockTransformations.cs

@@ -96,7 +96,7 @@ private static bool ContainsAssert(Block b)
 
   public static bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd { Expr: not LiteralExpr { asBool: true } }; }
 
-  public static void DeleteStraightLineBlocksWithoutCommands(List<Block> blocks) {
+  public static void DeleteStraightLineBlocksWithoutCommands(IList<Block> blocks) {
     var toVisit = new HashSet<Block>(blocks);
     var removed = new HashSet<Block>();
     while(toVisit.Count > 0) {

Source/VCGeneration/ConditionGeneration.cs

@@ -450,7 +450,7 @@ public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool pr
       options.PrintDesugarings = oldPrintDesugaringSetting;
     }
 
-    public static void ResetPredecessors(List<Block> blocks)
+    public static void ResetPredecessors(IList<Block> blocks)
     {
       Contract.Requires(blocks != null);
       foreach (Block b in blocks)
@@ -686,7 +686,7 @@ protected Dictionary<Variable, Expr> Convert2PassiveCmd(ImplementationRun run, M
 
       var start = DateTime.UtcNow;
 
-      Dictionary<Variable, Expr> r = ConvertBlocks2PassiveCmd(run.OutputWriter, implementation.Blocks, implementation.Proc.Modifies, mvInfo, implementation.debugInfos);
+      var r = ConvertBlocks2PassiveCmd(run.OutputWriter, implementation.Blocks, implementation.Proc.Modifies, mvInfo, implementation.debugInfos);
 
       var end = DateTime.UtcNow;
 
@@ -722,7 +722,7 @@ protected Dictionary<Variable, Expr> Convert2PassiveCmd(ImplementationRun run, M
       return r;
     }
 
-    protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(TextWriter traceWriter, List<Block> blocks, List<IdentifierExpr> modifies,
+    protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(TextWriter traceWriter, IList<Block> blocks, List<IdentifierExpr> modifies,
       ModelViewInfo mvInfo, Dictionary<Cmd, List<object>> debugInfos)
     {
       Contract.Requires(blocks != null);
@@ -1427,7 +1427,7 @@ public Block CreateBlockBetween(int predIndex, Block succ)
       return newBlock;
     }
 
-    protected void AddBlocksBetween(List<Block> blocks)
+    protected void AddBlocksBetween(IList<Block> blocks)
     {
       Contract.Requires(blocks != null);
 
@@ -1451,7 +1451,9 @@ protected void AddBlocksBetween(List<Block> blocks)
         }
       }
 
-      blocks.AddRange(tweens); // must wait until iteration is done before changing the list
+      foreach (var tween in tweens) {
+        blocks.Add(tween); // must wait until iteration is done before changing the list
+      }
 
       #endregion
     }

Source/VCGeneration/ManualSplit.cs

@@ -11,7 +11,7 @@ public class ManualSplit : Split
   public IImplementationPartOrigin Token { get; }
 
   public ManualSplit(VCGenOptions options, 
-    Func<List<Block>> blocks, 
+    Func<IList<Block>> blocks, 
     VerificationConditionGenerator parent, 
     ImplementationRun run, 
     IImplementationPartOrigin origin, int? randomSeed = null) 

Source/VCGeneration/Prune/Pruner.cs

@@ -57,7 +57,7 @@ public class Pruner {
      * See Checker.Setup for more information.
      * Data type constructor declarations are not pruned and they do affect VC generation.
      */
-    public static IEnumerable<Declaration> GetLiveDeclarations(VCGenOptions options, Program program, List<Block>? blocks)
+    public static IEnumerable<Declaration> GetLiveDeclarations(VCGenOptions options, Program program, IList<Block>? blocks)
     {
       if (program.DeclarationDependencies == null || blocks == null || !options.Prune)
       {
@@ -83,7 +83,7 @@ bool TraverseDeclaration(object parent, object child) {
       }
     }
 
-    private static RevealedState GetRevealedState(List<Block> blocks)
+    private static RevealedState GetRevealedState(IList<Block> blocks)
     {
       var controlFlowGraph = GetControlFlowGraph(blocks);
       var starts = controlFlowGraph.Nodes.Where(n => !controlFlowGraph.Predecessors(n).Any()).ToList();
@@ -97,7 +97,7 @@ private static RevealedState GetRevealedState(List<Block> blocks)
         Aggregate(RevealedState.AllHidden, RevealedAnalysis.MergeStates);
     }
 
-    public static Graph<Absy> GetControlFlowGraph(List<Block> blocks)
+    public static Graph<Absy> GetControlFlowGraph(IList<Block> blocks)
     {
       /*
        * Generally the blocks created by splitting have unset block.Predecessors fields

Source/VCGeneration/SmokeTester.cs

@@ -262,7 +262,7 @@ async Task<bool> CheckUnreachable(TextWriter traceWriter, Block cur, List<Cmd> s
     Block copy = CopyBlock(cur);
     Contract.Assert(copy != null);
     copy.Cmds = seq;
-    List<Block> backup = run.Implementation.Blocks;
+    var backup = run.Implementation.Blocks;
     Contract.Assert(backup != null);
     run.Implementation.Blocks = GetCopiedBlocks();
     copy.TransferCmd = new ReturnCmd(Token.NoToken);

Source/VCGeneration/Splits/BlockRewriter.cs

@@ -19,10 +19,10 @@ public class BlockRewriter {
   public List<Block> OrderedBlocks { get; }
   public VCGenOptions Options { get; }
   public Graph<Block> Dag { get; }
-  public Func<IImplementationPartOrigin, List<Block>, ManualSplit> CreateSplit { get; }
+  public Func<IImplementationPartOrigin, IList<Block>, ManualSplit> CreateSplit { get; }
 
-  public BlockRewriter(VCGenOptions options, List<Block> blocks,
-    Func<IImplementationPartOrigin, List<Block>, ManualSplit> createSplit) {
+  public BlockRewriter(VCGenOptions options, IList<Block> blocks,
+    Func<IImplementationPartOrigin, IList<Block>, ManualSplit> createSplit) {
     this.Options = options;
     CreateSplit = createSplit;
     Dag = Program.GraphFromBlocks(blocks);

Source/VCGeneration/Splits/FocusAttributeHandler.cs

@@ -19,7 +19,7 @@ public class FocusAttributeHandler {
   /// We recurse twice for each focus, leading to potentially 2^N splits
   /// </summary>
   public static List<ManualSplit> GetParts(VCGenOptions options, ImplementationRun run, 
-    Func<IImplementationPartOrigin, List<Block>, ManualSplit> createPart)
+    Func<IImplementationPartOrigin, IList<Block>, ManualSplit> createPart)
   {
     var rewriter = new BlockRewriter(options, run.Implementation.Blocks, createPart);
 

Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs

@@ -11,7 +11,7 @@ namespace VCGeneration;
 class IsolateAttributeOnAssertsHandler {
 
   public static (List<ManualSplit> IsolatedParts, ManualSplit Remainder) GetParts(VCGenOptions options, ManualSplit partToDivide, 
-    Func<IImplementationPartOrigin, List<Block>, ManualSplit> createPart) {
+    Func<IImplementationPartOrigin, IList<Block>, ManualSplit> createPart) {
     var rewriter = new BlockRewriter(options, partToDivide.Blocks, createPart);
 
     var splitOnEveryAssert = partToDivide.Options.VcsSplitOnEveryAssert;

Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs

@@ -13,7 +13,7 @@ namespace VCGeneration;
 
 class IsolateAttributeOnJumpsHandler {
   public static (List<ManualSplit> Isolated, ManualSplit Remainder) GetParts(VCGenOptions options, ManualSplit partToDivide, 
-    Func<IImplementationPartOrigin, List<Block>, ManualSplit> createPart) {
+    Func<IImplementationPartOrigin, IList<Block>, ManualSplit> createPart) {
 
     var rewriter = new BlockRewriter(options, partToDivide.Blocks, createPart);
 

Source/VCGeneration/Splits/ManualSplitFinder.cs

@@ -11,7 +11,7 @@ namespace VCGeneration;
 public static class ManualSplitFinder {
 
   public static IEnumerable<ManualSplit> GetParts(VCGenOptions options, ImplementationRun run,
-    Func<IImplementationPartOrigin, List<Block>, ManualSplit> createPart) {
+    Func<IImplementationPartOrigin, IList<Block>, ManualSplit> createPart) {
 
     var focussedParts = FocusAttributeHandler.GetParts(options, run, createPart);
     var result = focussedParts.SelectMany(focussedPart => {

Source/VCGeneration/Splits/Split.cs

@@ -22,8 +22,8 @@ public class Split : ProofRun
 
       public int RandomSeed { get; }
 
-      private List<Block> blocks;
-      public List<Block> Blocks => blocks ??= getBlocks();
+      private IList<Block> blocks;
+      public IList<Block> Blocks => blocks ??= getBlocks();
 
       readonly List<Block> bigBlocks = new();
       public List<AssertCmd> Asserts => Blocks.SelectMany(block => block.Cmds.OfType<AssertCmd>()).ToList();
@@ -74,7 +74,7 @@ public readonly VerificationConditionGenerator /*!*/
       public int SplitIndex { get; set; }
       public VerificationConditionGenerator.ErrorReporter reporter;
 
-      public Split(VCGenOptions options, Func<List<Block /*!*/>> /*!*/ getBlocks,
+      public Split(VCGenOptions options, Func<IList<Block /*!*/>> /*!*/ getBlocks,
         VerificationConditionGenerator /*!*/ parent, ImplementationRun run, int? randomSeed = null)
       {
         Contract.Requires(parent != null);
@@ -199,7 +199,7 @@ public void DumpDot(int splitNum)
       }
 
       int bsid;
-      private readonly Func<List<Block>> getBlocks;
+      private readonly Func<IList<Block>> getBlocks;
 
       BlockStats GetBlockStats(Block b)
       {

Source/VCGeneration/Splits/SplitAttributeHandler.cs

@@ -77,7 +77,7 @@ private static bool ShouldSplitHere(Cmd c) {
     return predicateCmd.Attributes.FindBoolAttribute("split_here");
   }
 
-  private static Dictionary<Block, Cmd?> GetMapFromBlockStartToSplit(List<Block> blocks, Dictionary<Block, List<Cmd>> splitsPerBlock) {
+  private static Dictionary<Block, Cmd?> GetMapFromBlockStartToSplit(IList<Block> blocks, Dictionary<Block, List<Cmd>> splitsPerBlock) {
     var todo = new Stack<Block>();
     var blockAssignments = new Dictionary<Block, Cmd?>();
     var immediateDominators = Program.GraphFromBlocks(blocks).ImmediateDominator();
@@ -169,7 +169,7 @@ List<Cmd> GetCommandsForBlockWithSplit(Block currentBlock)
     }
   }
 
-  private static List<Block> UpdateBlocks(IReadOnlyList<Block> blocks,
+  private static List<Block> UpdateBlocks(IList<Block> blocks,
     Func<Block, List<Cmd>> getCommands)
   {
     var newBlocks = new List<Block>(blocks.Count);