Undo some concurrent changes

boogie-org · Oct 8, 2024 · 36093f2 · 36093f2
1 parent f22112e
commit 36093f2
Show file tree

Hide file tree

Showing 2 changed files with 47 additions and 51 deletions.
diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs
@@ -474,62 +474,56 @@ 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)
-          {
-            continue;
-          }
-
-          var cmd = nextBlock.Cmds[0];
-          if (cmd is not ParCallCmd parCallCmd)
+          var targetBlocks = new List<Block>();
+          var addEdge = false;
+          foreach (var nextBlock in gotoCmd.LabelTargets)
           {
-            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});
         }
       }
 
@@ -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));
     }
 
@@ -610,9 +602,7 @@ private void SplitBlocks(Implementation impl)
         b.TransferCmd = currTransferCmd;
       }
 
-      foreach (var newBlock in newBlocks) {
-        impl.Blocks.Add(newBlock);
-      }
+      impl.Blocks.AddRange(newBlocks);
     }
 
     private Block CreateNoninterferenceCheckerBlock()

diff --git a/Source/Core/Generic/ListExtensions.cs b/Source/Core/Generic/ListExtensions.cs
@@ -5,6 +5,12 @@
 namespace Microsoft.Boogie;
 
 public static class ListExtensions {
+  public static void AddRange<T>(this IList<T> list, IEnumerable<T> newValues) {
+    foreach (var value in newValues) {
+      list.Add(value);
+    }
+  }
+
   public static IReadOnlyList<T> Reversed<T>(this IReadOnlyList<T> list) {
     return new ReversedReadOnlyList<T>(list);
   }