Fix for focus.dfy

boogie-org · Oct 23, 2024 · b40821a · b40821a
1 parent 1e5cd52
commit b40821a
Show file tree

Hide file tree

Showing 5 changed files with 22 additions and 11 deletions.
diff --git a/Source/Core/AST/GotoBoogie/Block.cs b/Source/Core/AST/GotoBoogie/Block.cs
@@ -7,6 +7,7 @@ namespace Microsoft.Boogie;
 
 public sealed class Block : Absy
 {
+
   public string Label { get; set; } // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
 
   [Rep]

diff --git a/Source/Core/Analysis/BlockCoalescer.cs b/Source/Core/Analysis/BlockCoalescer.cs
@@ -79,7 +79,7 @@ public override Implementation VisitImplementation(Implementation impl)
     return impl;
   }
 
-  public static void CoalesceInPlace(List<Block> blocks) {
+  public static void CoalesceInPlace(IList<Block> blocks) {
     var coalesced = CoalesceFromRootBlock(blocks);
     blocks.Clear();
     blocks.AddRange(coalesced);
@@ -140,7 +140,10 @@ public static IList<Block> CoalesceFromRootBlock(IList<Block> blocks)
         continue;
       }
 
-      block.Cmds.AddRange(successor.Cmds);
+      // Previously this was block.Cmds.AddRange,
+      // command lists are reused between blocks
+      // so that was buggy. Maybe Block.Cmds should be made immutable
+      block.Cmds = block.Cmds.Concat(successor.Cmds).ToList();
       var originalTransferToken = block.TransferCmd.tok;
       block.TransferCmd = successor.TransferCmd;
       if (!block.TransferCmd.tok.IsValid) {

diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs
@@ -12,7 +12,7 @@ namespace VCGeneration;
 
 public static class BlockTransformations {
 
-  public static void Optimize(List<Block> blocks) {
+  public static void Optimize(IList<Block> blocks) {
     foreach (var block in blocks)
     {
       // make blocks ending in assume false leaves of the CFG-DAG
@@ -46,7 +46,7 @@ private static void StopControlFlowAtAssumeFalse(Block block)
 
   private static bool IsAssumeFalse (Cmd c) { return c is AssumeCmd { Expr: LiteralExpr { asBool: false } }; }
 
-  public static void DeleteBlocksNotLeadingToAssertions(List<Block> blocks)
+  public static void DeleteBlocksNotLeadingToAssertions(IList<Block> blocks)
   {
     var todo = new Stack<Block>();
     var peeked = new HashSet<Block>();

diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs
@@ -16,17 +16,26 @@ public static IEnumerable<ManualSplit> GetParts(VCGenOptions options, Implementa
     var focussedParts = FocusAttributeHandler.GetParts(options, run, createPart);
     var result = focussedParts.SelectMany(focussedPart =>
     {
+      foreach(var block in focussedPart.Blocks)
+      {
+        block.Predecessors.Clear();
+      }
+      Implementation.ComputePredecessorsForBlocks(focussedPart.Blocks);
       var (isolatedJumps, withoutIsolatedJumps) =
         IsolateAttributeOnJumpsHandler.GetParts(options, focussedPart, createPart);
-      return new[] { withoutIsolatedJumps }.Concat(isolatedJumps).SelectMany(isolatedJumpSplit =>
+      var resultForFocusPart = new[] { withoutIsolatedJumps }.Concat(isolatedJumps).SelectMany(isolatedJumpSplit =>
       {
         var (isolatedAssertions, withoutIsolatedAssertions) =
           IsolateAttributeOnAssertsHandler.GetParts(options, isolatedJumpSplit, createPart);
 
         var splitParts = SplitAttributeHandler.GetParts(withoutIsolatedAssertions);
         return isolatedAssertions.Concat(splitParts);
-      });
-    }).Where(s => s.Asserts.Any()).ToList();
+      }).ToList();
+      return resultForFocusPart;
+    }).Where(s => s.Asserts.Any()).Select(s => {
+      BlockTransformations.Optimize(s.Blocks);
+      return s;
+    }).ToList();
 
     if (result.Any())
     {

diff --git a/Source/VCGeneration/Splits/SplitAttributeHandler.cs b/Source/VCGeneration/Splits/SplitAttributeHandler.cs
@@ -62,10 +62,8 @@ public static List<ManualSplit> GetParts(ManualSplit partToSplit) {
     return vcs;
 
     ManualSplit CreateVc(IImplementationPartOrigin token, List<Block> blocks) {
-      return new ManualSplit(partToSplit.Options, () => {
-        BlockTransformations.Optimize(blocks);
-        return blocks;
-      }, partToSplit.parent, partToSplit.Run, token);
+      return new ManualSplit(partToSplit.Options, () => blocks, 
+        partToSplit.parent, partToSplit.Run, token);
     }
   }