Undo some concurrent changes

Source/Concurrency/YieldingProcInstrumentation.cs

@@ -474,71 +474,65 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
 
       // add jumps to noninterferenceChecker, returnChecker, and refinementChecker blocks
       var implRefinementCheckingBlocks = new List<Block>();
-      foreach (var block in impl.Blocks) {
-        if (block.TransferCmd is not GotoCmd gotoCmd)
-        {
-          block.TransferCmd = new GotoCmd(block.TransferCmd.tok,
-            new List<Block> { returnCheckerBlock, returnBlock, noninterferenceCheckerBlock });
-          continue;
-        }
-
-        var targetBlocks = new List<Block>();
-        var addEdge = false;
-        foreach (var nextBlock in gotoCmd.LabelTargets)
+      foreach (var b in impl.Blocks)
+      {
+        if (b.TransferCmd is GotoCmd gotoCmd)
         {
-          if (nextBlock.Cmds.Count <= 0)
+          var targetBlocks = new List<Block>();
+          var addEdge = false;
+          foreach (var nextBlock in gotoCmd.LabelTargets)
           {
-            continue;
-          }
-
-          var cmd = nextBlock.Cmds[0];
-          if (cmd is not ParCallCmd parCallCmd)
-          {
-            continue;
+            if (nextBlock.cmds.Count > 0)
+            {
+              var cmd = nextBlock.cmds[0];
+              if (cmd is ParCallCmd parCallCmd)
+              {
+                foreach (var callCmd in parCallCmd.CallCmds)
+                {
+                  if (refinementBlocks.ContainsKey(callCmd))
+                  {
+                    var targetBlock = refinementBlocks[callCmd];
+                    FixUpImplRefinementCheckingBlock(targetBlock,
+                      CivlAttributes.IsCallMarked(callCmd)
+                        ? returnCheckerBlock
+                        : unchangedCheckerBlock);
+                    targetBlocks.Add(targetBlock);
+                    implRefinementCheckingBlocks.Add(targetBlock);
+                  }
+                }
+                addEdge = true;
+              }
+            }
           }
 
-          foreach (var callCmd in parCallCmd.CallCmds)
+          gotoCmd.AddTargets(targetBlocks);
+          if (addEdge)
           {
-            if (!refinementBlocks.TryGetValue(callCmd, out var targetBlock))
+            AddEdge(gotoCmd, noninterferenceCheckerBlock);
+            if (blocksInYieldingLoops.Contains(b))
             {
-              continue;
+              AddEdge(gotoCmd, unchangedCheckerBlock);
+            }
+            else
+            {
+              b.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds());
+              AddEdge(gotoCmd, refinementCheckerBlock);
             }
-
-            FixUpImplRefinementCheckingBlock(targetBlock,
-              CivlAttributes.IsCallMarked(callCmd)
-                ? returnCheckerBlock
-                : unchangedCheckerBlock);
-            targetBlocks.Add(targetBlock);
-            implRefinementCheckingBlocks.Add(targetBlock);
           }
-
-          addEdge = true;
-        }
-
-        gotoCmd.AddTargets(targetBlocks);
-        if (!addEdge)
-        {
-          continue;
-        }
-
-        AddEdge(gotoCmd, noninterferenceCheckerBlock);
-        if (blocksInYieldingLoops.Contains(block))
-        {
-          AddEdge(gotoCmd, unchangedCheckerBlock);
         }
         else
         {
-          block.Cmds.AddRange(refinementInstrumentation.CreateActionEvaluationCmds());
-          AddEdge(gotoCmd, refinementCheckerBlock);
+          b.TransferCmd = new GotoCmd(b.TransferCmd.tok,
+            new List<Block> {returnCheckerBlock, returnBlock, noninterferenceCheckerBlock});
         }
       }
 
       // desugar ParCallCmd 
       foreach (Block b in impl.Blocks)
       {
-        if (b.Cmds.Count > 0)
+        if (b.cmds.Count > 0)
         {
-          var cmd = b.Cmds[0];
+          var cmd = b.cmds[0];
           if (cmd is ParCallCmd)
           {
             DesugarParCallCmdInBlock(b, blocksInYieldingLoops.Contains(b));
@@ -551,9 +545,7 @@ private void DesugarConcurrency(Implementation impl, List<Cmd> preconditions)
       impl.Blocks.Add(unchangedCheckerBlock);
       impl.Blocks.Add(returnCheckerBlock);
       impl.Blocks.Add(returnBlock);
-      foreach (var block in implRefinementCheckingBlocks) {
-        impl.Blocks.Add(block);
-      }
+      impl.Blocks.AddRange(implRefinementCheckingBlocks);
       impl.Blocks.Insert(0, CreateInitialBlock(impl, preconditions));
     }
 
@@ -586,33 +578,31 @@ private void SplitBlocks(Implementation impl)
       {
         var currTransferCmd = b.TransferCmd;
         int labelCount = 0;
-        int lastSplitIndex = b.Cmds.Count;
-        for (int i = b.Cmds.Count - 1; i >= 0; i--)
+        int lastSplitIndex = b.cmds.Count;
+        for (int i = b.cmds.Count - 1; i >= 0; i--)
         {
           var split = false;
-          var cmd = b.Cmds[i];
+          var cmd = b.cmds[i];
           if (cmd is ParCallCmd)
           {
             split = true;
           }
 
           if (split)
           {
-            var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.Cmds.GetRange(i, lastSplitIndex - i),
+            var newBlock = new Block(b.tok, $"{b.Label}_{labelCount++}", b.cmds.GetRange(i, lastSplitIndex - i),
               currTransferCmd);
             newBlocks.Add(newBlock);
             currTransferCmd = new GotoCmd(b.tok, new List<Block> {newBlock});
             lastSplitIndex = i;
           }
         }
 
-        b.Cmds = b.Cmds.GetRange(0, lastSplitIndex);
+        b.cmds = b.cmds.GetRange(0, lastSplitIndex);
         b.TransferCmd = currTransferCmd;
       }
 
-      foreach (var newBlock in newBlocks) {
-        impl.Blocks.Add(newBlock);
-      }
+      impl.Blocks.AddRange(newBlocks);
     }
 
     private Block CreateNoninterferenceCheckerBlock()
@@ -724,8 +714,8 @@ private void DesugarParCallCmdInBlock(Block block, bool isBlockInYieldingLoop)
       newCmds.AddRange(CreateUpdatesToOldGlobalVars());
       newCmds.AddRange(refinementInstrumentation.CreateUpdatesToOldOutputVars());
       newCmds.AddRange(CreateUpdatesToPermissionCollector(parCallCmd));
-      newCmds.AddRange(block.Cmds.GetRange(1, block.Cmds.Count - 1));
-      block.Cmds = newCmds;
+      newCmds.AddRange(block.cmds.GetRange(1, block.cmds.Count - 1));
+      block.cmds = newCmds;
     }
 
     private Formal ParCallDesugarFormal(Variable v, int count, bool incoming)