Improve short names for splits (#976)

### Changes
Improve short names for splits

### Testing
Updated tests

Source/Directory.Build.props

@@ -2,7 +2,7 @@
 
   <!-- Target framework and package configuration -->
   <PropertyGroup>
-    <Version>3.4.0</Version>
+    <Version>3.4.1</Version>
     <TargetFramework>net6.0</TargetFramework>
     <GeneratePackageOnBuild>false</GeneratePackageOnBuild>
     <Authors>Boogie</Authors>

Source/VCGeneration/Splits/BlockRewriter.cs

@@ -74,7 +74,7 @@ void AddSplitsFromIndex(ImmutableStack<IToken> choices, int gotoIndex, IReadOnly
               newBlock.TransferCmd = new ReturnCmd(origin);
             }
           });
-        result.Add(CreateSplit(new PathOrigin(origin, choices.OrderBy(b => b.pos).ToList(), "paths"), newBlocks));
+        result.Add(CreateSplit(new PathOrigin(origin, choices.OrderBy(b => b.pos).ToList()), newBlocks));
       } else {
         var splitGoto = splitCommands[gotoIndex];
         if (!blocksToIncludeForChoices.Contains(splitGoto.Block))

Source/VCGeneration/Splits/FocusAttributeHandler.cs

@@ -48,38 +48,39 @@ public static List<ManualSplit> GetParts(VCGenOptions options, ImplementationRun
     AddSplitsFromIndex(ImmutableStack<IToken>.Empty, 0, implementation.Blocks.ToHashSet(), ImmutableHashSet<Block>.Empty);
     return result;
 
-    void AddSplitsFromIndex(ImmutableStack<IToken> path, int focusIndex, IReadOnlySet<Block> blocksToInclude, ISet<Block> freeAssumeBlocks) {
+    void AddSplitsFromIndex(ImmutableStack<IToken> focusedBlocks, int focusIndex, IReadOnlySet<Block> blocksToInclude, ISet<Block> freeAssumeBlocks) {
       var allFocusBlocksHaveBeenProcessed = focusIndex == focusBlocks.Count;
       if (allFocusBlocksHaveBeenProcessed) {
 
         // freeBlocks consist of the predecessors of the relevant foci.
         // Their assertions turn into assumes and any splits inside them are disabled.
         var newBlocks = rewriter.ComputeNewBlocks(blocksToInclude, freeAssumeBlocks);
-        IImplementationPartOrigin token = path.Any() 
-          ? new PathOrigin(new ImplementationRootOrigin(run.Implementation), 
-            path.OrderBy(t => t.pos).ToList(), "focus") 
+        var focussedSet = focusedBlocks.ToHashSet();
+        IImplementationPartOrigin token = focusedBlocks.Any() 
+          ? new FocusOrigin(new ImplementationRootOrigin(run.Implementation), 
+            focusBlocks.Select(b => (b.Token, focussedSet.Contains(b.Token))).ToList()) 
           : new ImplementationRootOrigin(run.Implementation); 
         result.Add(rewriter.CreateSplit(token, newBlocks));
       } else {
         var (focusBlock, nextToken) = focusBlocks[focusIndex]; // assert b in blocks
         if (!blocksToInclude.Contains(focusBlock) || freeAssumeBlocks.Contains(focusBlock))
         {
           // This focus block can not be reached in our current path, so we ignore it by continuing
-          AddSplitsFromIndex(path, focusIndex + 1, blocksToInclude, freeAssumeBlocks);
+          AddSplitsFromIndex(focusedBlocks, focusIndex + 1, blocksToInclude, freeAssumeBlocks);
         }
         else
         {
           var dominatedBlocks = BlockRewriter.DominatedBlocks(rewriter.OrderedBlocks, focusBlock, blocksToInclude);
           // Recursive call that does NOT focus the block
           // Contains all blocks except the ones dominated by the focus block
-          AddSplitsFromIndex(path, focusIndex + 1, 
+          AddSplitsFromIndex(focusedBlocks, focusIndex + 1, 
             blocksToInclude.Where(blk => !dominatedBlocks.Contains(blk)).ToHashSet(), freeAssumeBlocks);
           var ancestors = ancestorsPerBlock[focusBlock];
           var descendants = descendantsPerBlock[focusBlock];
 
           // Recursive call that does focus the block
           // Contains all the ancestors, the focus block, and the descendants.
-          AddSplitsFromIndex(path.Push(nextToken), focusIndex + 1, 
+          AddSplitsFromIndex(focusedBlocks.Push(nextToken), focusIndex + 1, 
             ancestors.Union(descendants).Intersect(blocksToInclude).ToHashSet(), 
             ancestors.Union(freeAssumeBlocks).ToHashSet());
         } 

Source/VCGeneration/Splits/FocusOrigin.cs

@@ -0,0 +1,23 @@
+#nullable enable
+using System.Collections.Generic;
+using System.Linq;
+using Microsoft.Boogie;
+
+namespace VCGeneration;
+
+public class FocusOrigin : TokenWrapper, IImplementationPartOrigin {
+
+  public FocusOrigin(IImplementationPartOrigin inner, List<(IToken Token, bool DidFocus)> focusChoices) : base(inner) {
+    Inner = inner;
+    FocusChoices = focusChoices;
+  }
+
+  public new IImplementationPartOrigin Inner { get; }
+  public List<(IToken Token, bool DidFocus)> FocusChoices { get; }
+  public string ShortName {
+    get {
+      var choices = string.Join(",", FocusChoices.Select(b => (b.DidFocus ? "+" : "-") + b.Token.line));
+      return $"{Inner.ShortName}/focus[{choices}]";
+    }
+  }
+}

Source/VCGeneration/Splits/ImplementationRootOrigin.cs

@@ -0,0 +1,12 @@
+#nullable enable
+using Microsoft.Boogie;
+
+namespace VCGeneration;
+
+public class ImplementationRootOrigin : TokenWrapper, IImplementationPartOrigin {
+  public ImplementationRootOrigin(Implementation implementation) : base(implementation.tok)
+  {
+  }
+
+  public string ShortName => "";
+}

Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs

@@ -81,7 +81,7 @@ List<Cmd> GetCommandsForBlockWithAssert(Block currentBlock, AssertCmd assert)
 
     ManualSplit GetSplitWithoutIsolatedAssertions() {
       if (!isolatedAssertions.Any()) {
-        return rewriter.CreateSplit(partToDivide.Token, partToDivide.Blocks);
+        return rewriter.CreateSplit(new RemainingAssertionsOrigin(partToDivide.Token), partToDivide.Blocks);
       }
 
       var newBlocks = rewriter.ComputeNewBlocks(null, (oldBlock, newBlock) => newBlock.Cmds = GetCommands(oldBlock));
@@ -103,5 +103,4 @@ public IsolatedAssertionOrigin(IImplementationPartOrigin origin, AssertCmd isola
   }
 
   public string ShortName => $"{Origin.ShortName}/assert@{IsolatedAssert.Line}";
-  public string KindName => "assertion";
 }

Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs

@@ -45,12 +45,12 @@ public static (List<ManualSplit> Isolated, ManualSplit Remainder) GetParts(VCGen
       var blocksToInclude = ancestors.Union(descendants).ToHashSet();
 
       var originalJump = gotoFromReturn?.Origin ?? (TransferCmd)gotoCmd;
+      var origin = new JumpOrigin(partToDivide.Token, originalJump);
 
       if (isolateAttribute != null && isolateAttribute.Params.OfType<string>().Any(p => Equals(p, "paths"))) {
         // These conditions hold if the goto was originally a return
         Debug.Assert(gotoCmd.LabelTargets.Count == 1);
         Debug.Assert(gotoCmd.LabelTargets[0].TransferCmd is not GotoCmd);
-        var origin = new JumpOrigin(originalJump);
         results.AddRange(rewriter.GetSplitsForIsolatedPaths(gotoCmd.LabelTargets[0], blocksToInclude, origin));
       } else {
         var newBlocks = rewriter.ComputeNewBlocks(blocksToInclude, (oldBlock, newBlock) => {
@@ -68,7 +68,7 @@ Possibly two block are coalesced which deletes the goto with the GotoFromReturn
             }
           }
         });
-        results.Add(rewriter.CreateSplit(new JumpOrigin(originalJump), newBlocks));
+        results.Add(rewriter.CreateSplit(origin, newBlocks));
       }
     }
 
@@ -84,20 +84,20 @@ ManualSplit GetPartWithoutIsolatedReturns() {
           newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
         }
       });
-      return rewriter.CreateSplit(new ImplementationRootOrigin(partToDivide.Implementation), 
-        newBlocks);
+      return rewriter.CreateSplit(new RemainingAssertionsOrigin(partToDivide.Token), newBlocks);
     }
   }
 }
 
-
 public class JumpOrigin : TokenWrapper, IImplementationPartOrigin {
+  public IImplementationPartOrigin Origin { get; }
   public TransferCmd IsolatedReturn { get; }
 
-  public JumpOrigin(TransferCmd isolatedReturn) : base(isolatedReturn.tok) {
+  public JumpOrigin(IImplementationPartOrigin origin, TransferCmd isolatedReturn) : base(isolatedReturn.tok) {
+    Origin = origin;
     this.IsolatedReturn = isolatedReturn;
   }
 
-  public string ShortName => $"/{KindName}@{IsolatedReturn.Line}";
+  public string ShortName => $"{Origin.ShortName}/{KindName}@{IsolatedReturn.Line}";
   public string KindName => IsolatedReturn is ReturnCmd ? "return" : "goto";
 }

Source/VCGeneration/Splits/ManualSplitFinder.cs

@@ -45,5 +45,4 @@ public static IEnumerable<ManualSplit> GetParts(VCGenOptions options, Implementa
 
 public interface IImplementationPartOrigin : IToken {
   string ShortName { get; }
-  string KindName { get; }
 }

Source/VCGeneration/Splits/PathOrigin.cs

@@ -0,0 +1,18 @@
+#nullable enable
+using System.Collections.Generic;
+using System.Linq;
+using Microsoft.Boogie;
+
+namespace VCGeneration;
+
+public class PathOrigin : TokenWrapper, IImplementationPartOrigin {
+
+  public PathOrigin(IImplementationPartOrigin inner, List<IToken> branchTokens) : base(inner) {
+    Inner = inner;
+    BranchTokens = branchTokens;
+  }
+
+  public new IImplementationPartOrigin Inner { get; }
+  public List<IToken> BranchTokens { get; }
+  public string ShortName => $"{Inner.ShortName}/path[{string.Join(",", BranchTokens.Select(b => b.line))}]";
+}

Source/VCGeneration/Splits/RemainingAssertionsOrigin.cs

@@ -0,0 +1,12 @@
+#nullable enable
+namespace VCGeneration;
+
+public class RemainingAssertionsOrigin : TokenWrapper, IImplementationPartOrigin {
+  public IImplementationPartOrigin Origin { get; }
+
+  public RemainingAssertionsOrigin(IImplementationPartOrigin origin) : base(origin) {
+    Origin = origin;
+  }
+
+  public string ShortName => $"{Origin.ShortName}/remainingAssertions";
+}

Source/VCGeneration/Splits/SplitAttributeHandler.cs

@@ -38,7 +38,7 @@ public static List<ManualSplit> GetParts(ManualSplit partToSplit) {
     var blockStartToSplit = GetMapFromBlockStartToSplit(partToSplit.Blocks, splitsPerBlock);
 
     var beforeSplitsVc = GetImplementationPartAfterSplit(CreateVc, partToSplit, blockStartToSplit,
-      entryPoint, splits, null);
+      entryPoint, splits, null, new UntilFirstSplitOrigin(partToSplit.Token));
     if (beforeSplitsVc != null)
     {
       vcs.Add(beforeSplitsVc);
@@ -52,7 +52,7 @@ public static List<ManualSplit> GetParts(ManualSplit partToSplit) {
       foreach (var split in splitsForBlock)
       {
         var splitVc = GetImplementationPartAfterSplit(CreateVc, partToSplit, 
-          blockStartToSplit, block, splits, split);
+          blockStartToSplit, block, splits, split, new AfterSplitOrigin(partToSplit.Token, split.tok));
         if (splitVc != null)
         {
           vcs.Add(splitVc);
@@ -112,7 +112,7 @@ private static bool ShouldSplitHere(Cmd c) {
   private static ManualSplit? GetImplementationPartAfterSplit(Func<IImplementationPartOrigin, List<Block>, ManualSplit> createVc, 
     ManualSplit partToSplit, 
     Dictionary<Block, Cmd?> blockStartToSplit, Block blockWithSplit, 
-    HashSet<Cmd> splits, Cmd? split) 
+    HashSet<Cmd> splits, Cmd? split, IImplementationPartOrigin origin) 
   {
     var assertionCount = 0;
 
@@ -132,7 +132,7 @@ private static bool ShouldSplitHere(Cmd c) {
       return null;
     }
 
-    return createVc(split == null ? partToSplit.Token : new SplitOrigin(partToSplit.Token, split.tok), newBlocks);
+    return createVc(origin, newBlocks);
 
     List<Cmd> GetCommandsForBlockImmediatelyDominatedBySplit(Block currentBlock)
     {
@@ -208,15 +208,24 @@ private static void AddJumpsToNewBlocks(Dictionary<Block, Block> oldToNewBlockMa
   }
 }
 
-class SplitOrigin : TokenWrapper, IImplementationPartOrigin {
+public class UntilFirstSplitOrigin : TokenWrapper, IImplementationPartOrigin {
+  public new IImplementationPartOrigin Inner { get; }
+
+  public UntilFirstSplitOrigin(IImplementationPartOrigin inner) : base(inner) {
+    Inner = inner;
+  }
+
+  public string ShortName => $"{Inner.ShortName}/untilFirstSplit";
+}
+
+public class AfterSplitOrigin : TokenWrapper, IImplementationPartOrigin {
   public new IImplementationPartOrigin Inner { get; }
   public IToken Tok { get; }
 
-  public SplitOrigin(IImplementationPartOrigin inner, IToken tok) : base(tok) {
+  public AfterSplitOrigin(IImplementationPartOrigin inner, IToken tok) : base(tok) {
     Inner = inner;
     Tok = tok;
   }
 
-  public string ShortName => $"{Inner.ShortName}/split@{line}";
-  public string KindName => "split";
+  public string ShortName => $"{Inner.ShortName}/afterSplit@{line}";
 }

Test/implementationDivision/focus/focus.bpl.expect

@@ -13,7 +13,7 @@ implementation Ex() returns (y: int)
 }
 
 
-implementation Ex/focus[16]/split@15() returns (y: int)
+implementation Ex/focus[+16,-20,-25]/afterSplit@15() returns (y: int)
 {
 
   anon0:
@@ -32,7 +32,7 @@ implementation Ex/focus[16]/split@15() returns (y: int)
 }
 
 
-implementation Ex/focus[16,25]() returns (y: int)
+implementation Ex/focus[+16,-20,+25]() returns (y: int)
 {
 
   anon0:
@@ -56,7 +56,7 @@ implementation Ex/focus[16,25]() returns (y: int)
 }
 
 
-implementation Ex/focus[16,20]() returns (y: int)
+implementation Ex/focus[+16,+20,-25]() returns (y: int)
 {
 
   anon0:
@@ -76,7 +76,7 @@ implementation Ex/focus[16,20]() returns (y: int)
 }
 
 
-implementation Ex/focus[16,20,25]() returns (y: int)
+implementation Ex/focus[+16,+20,+25]() returns (y: int)
 {
 
   anon0:
@@ -102,7 +102,7 @@ implementation Ex/focus[16,20,25]() returns (y: int)
 
 
 focus.bpl(15,5): Error: this assertion could not be proved
-implementation focusInconsistency/focus[38](x: int) returns (y: int)
+implementation focusInconsistency/focus[+38](x: int) returns (y: int)
 {
 
   anon0: