Fix problems with isolate each assertion and isolating jumps

Source/Core/AST/GotoBoogie/ImplicitJump.cs

@@ -0,0 +1,10 @@
+#nullable enable
+using Microsoft.Boogie;
+
+namespace VCGeneration;
+
+public class ImplicitJump : TokenWrapper {
+  public ImplicitJump(IToken inner) : base(inner)
+  {
+  }
+}

Source/Core/AST/StructuredBoogie/BigBlocksResolutionContext.cs

@@ -2,6 +2,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using VCGeneration;
 
 namespace Microsoft.Boogie;
 
@@ -581,11 +582,11 @@ TransferCmd GotoSuccessor(IToken tok, BigBlock b)
     Contract.Ensures(Contract.Result<TransferCmd>() != null);
     if (b.successorBigBlock != null)
     {
-      return new GotoCmd(tok, new List<String> {b.successorBigBlock.LabelName});
+      return new GotoCmd(new ImplicitJump(tok), new List<String> {b.successorBigBlock.LabelName});
     }
     else
     {
-      return new ReturnCmd(tok);
+      return new ReturnCmd(new ImplicitJump(tok));
     }
   }
 }

Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs

@@ -61,7 +61,8 @@ List<Cmd> GetCommands(Block oldBlock) =>
           : oldBlock.Cmds.Select(rewriter.TransformAssertCmd).ToList();
 
       var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToKeep, GetCommands);
-      return rewriter.CreateSplit(new IsolatedAssertionOrigin(assertCmd), newBlocks);
+      var origin = new IsolatedAssertionOrigin(partToDivide.Token, assertCmd);
+      return rewriter.CreateSplit(origin, newBlocks);
     }
 
     List<Cmd> GetCommandsForBlockWithAssert(Block currentBlock, AssertCmd assert)
@@ -79,28 +80,28 @@ List<Cmd> GetCommandsForBlockWithAssert(Block currentBlock, AssertCmd assert)
     }
 
     ManualSplit GetSplitWithoutIsolatedAssertions() {
-      var origin = new ImplementationRootOrigin(partToDivide.Implementation);
       if (!isolatedAssertions.Any()) {
-        return rewriter.CreateSplit(origin, partToDivide.Blocks);
+        return rewriter.CreateSplit(partToDivide.Token, partToDivide.Blocks);
       }
 
-      var (newBlocks, mapping) = rewriter.ComputeNewBlocks(null, GetCommands);
+      var (newBlocks, _) = rewriter.ComputeNewBlocks(null, GetCommands);
 
-      return rewriter.CreateSplit(origin, newBlocks);
+      return rewriter.CreateSplit(partToDivide.Token, newBlocks);
 
       List<Cmd> GetCommands(Block block) => block.Cmds.Select(cmd => 
         isolatedAssertions.Contains(cmd) ? rewriter.TransformAssertCmd(cmd) : cmd).ToList();
     }
   }
 }
 
-
 public class IsolatedAssertionOrigin : TokenWrapper, IImplementationPartOrigin {
+  public IImplementationPartOrigin Origin { get; }
   public AssertCmd IsolatedAssert { get; }
 
-  public IsolatedAssertionOrigin(AssertCmd isolatedAssert) : base(isolatedAssert.tok) {
+  public IsolatedAssertionOrigin(IImplementationPartOrigin origin, AssertCmd isolatedAssert) : base(isolatedAssert.tok) {
+    Origin = origin;
     this.IsolatedAssert = isolatedAssert;
   }
 
-  public string ShortName => $"/assert@{IsolatedAssert.Line}";
+  public string ShortName => $"{Origin.ShortName}/assert@{IsolatedAssert.Line}";
 }

Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs

@@ -44,11 +44,16 @@ public static (List<ManualSplit> Isolated, ManualSplit Remainder) GetParts(VCGen
       var blocksToInclude = ancestors.Union(descendants).ToHashSet();
 
       var originalReturn = ((GotoFromReturn)gotoCmd.tok).Origin;
+      if (originalReturn.tok is ImplicitJump) {
+        continue;
+      }
+
       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);
-        results.AddRange(rewriter.GetSplitsForIsolatedPaths(gotoCmd.LabelTargets[0], blocksToInclude, originalReturn.tok));
+        var origin = new ReturnOrigin(originalReturn);
+        results.AddRange(rewriter.GetSplitsForIsolatedPaths(gotoCmd.LabelTargets[0], blocksToInclude, origin));
       } else {
         var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToInclude, ancestors.ToHashSet());
         results.Add(rewriter.CreateSplit(new ReturnOrigin(originalReturn), newBlocks));

Source/VCGeneration/Splits/ManualSplitFinder.cs

@@ -14,17 +14,26 @@ public static IEnumerable<ManualSplit> GetParts(VCGenOptions options, Implementa
     Func<IImplementationPartOrigin, List<Block>, ManualSplit> createPart) {
 
     var focussedParts = FocusAttributeHandler.GetParts(options, run, createPart);
-    var result = focussedParts.SelectMany(focussedPart => {
+    var result = focussedParts.SelectMany(focussedPart =>
+    {
       var (isolatedJumps, withoutIsolatedJumps) =
         IsolateAttributeOnJumpsHandler.GetParts(options, focussedPart, createPart);
-      var (isolatedAssertions, withoutIsolatedAssertions) =
-        IsolateAttributeOnAssertsHandler.GetParts(options, withoutIsolatedJumps, createPart);
-    
-      var splitParts = SplitAttributeHandler.GetParts(withoutIsolatedAssertions);
-      var splits = isolatedJumps.Concat(isolatedAssertions).Concat(splitParts).Where(s => s.Asserts.Any()).ToList();
-      return splits.Any() ? splits : new List<ManualSplit> { focussedPart };
-    });
-    return result;
+      return 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();
+
+    if (result.Any())
+    {
+      return result;
+    }
+
+    return focussedParts.Take(1);
   }
 }
 

Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl

@@ -0,0 +1,27 @@
+// RUN: %boogie /printSplit:- /errorTrace:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure {:vcs_split_on_every_assert} MergeAtEnd(x: int) returns (r: int) 
+  ensures r > 1;
+{
+  if (x > 0) {
+    r := 1;
+  } 
+  else {
+    r := 2;
+  }
+}
+
+procedure {:vcs_split_on_every_assert} MultipleEnsures(x: int) returns (r: int) 
+  ensures r > 1;
+  ensures r < 10;
+{
+  if (x > 0) {
+    r := 1;
+    return;
+  } 
+  else {
+    r := 20;
+    return;
+  }
+}

Test/implementationDivision/isolateJump/isolateJumpAndSplitOnEveryAssert.bpl.expect

@@ -0,0 +1,100 @@
+implementation {:vcs_split_on_every_assert} MergeAtEnd/assert@5(x: int) returns (r: int)
+{
+
+  anon0:
+    goto anon3_Then, anon3_Else;
+
+  anon3_Then:
+    assume {:partition} x > 0;
+    assume r#AT#0 == 1;
+    goto GeneratedUnifiedExit;
+
+  anon3_Else:
+    assume {:partition} 0 >= x;
+    assume r#AT#0 == 2;
+    goto GeneratedUnifiedExit;
+
+  GeneratedUnifiedExit:
+    assert r#AT#0 > 1;
+    return;
+}
+
+
+isolateJumpAndSplitOnEveryAssert.bpl(9,3): Error: a postcondition could not be proved on this return path
+isolateJumpAndSplitOnEveryAssert.bpl(5,3): Related location: this is the postcondition that could not be proved
+implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@16(x: int) returns (r: int)
+{
+
+  anon0:
+    goto anon3_Else;
+
+  anon3_Else:
+    assume {:partition} 0 >= x;
+    assume r#AT#0 == 20;
+    goto GeneratedUnifiedExit;
+
+  GeneratedUnifiedExit:
+    assert r#AT#0 > 1;
+    return;
+}
+
+
+implementation {:vcs_split_on_every_assert} MultipleEnsures/return@25/assert@17(x: int) returns (r: int)
+{
+
+  anon0:
+    goto anon3_Else;
+
+  anon3_Else:
+    assume {:partition} 0 >= x;
+    assume r#AT#0 == 20;
+    goto GeneratedUnifiedExit;
+
+  GeneratedUnifiedExit:
+    assume r#AT#0 > 1;
+    assert r#AT#0 < 10;
+    return;
+}
+
+
+implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@16(x: int) returns (r: int)
+{
+
+  anon0:
+    goto anon3_Then;
+
+  anon3_Then:
+    assume {:partition} x > 0;
+    assume r#AT#0 == 1;
+    goto GeneratedUnifiedExit;
+
+  GeneratedUnifiedExit:
+    assert r#AT#0 > 1;
+    return;
+}
+
+
+implementation {:vcs_split_on_every_assert} MultipleEnsures/return@21/assert@17(x: int) returns (r: int)
+{
+
+  anon0:
+    goto anon3_Then;
+
+  anon3_Then:
+    assume {:partition} x > 0;
+    assume r#AT#0 == 1;
+    goto GeneratedUnifiedExit;
+
+  GeneratedUnifiedExit:
+    assume r#AT#0 > 1;
+    assert r#AT#0 < 10;
+    return;
+}
+
+
+isolateJumpAndSplitOnEveryAssert.bpl(21,5): Error: a postcondition could not be proved on this return path
+isolateJumpAndSplitOnEveryAssert.bpl(16,3): Related location: this is the postcondition that could not be proved
+isolateJumpAndSplitOnEveryAssert.bpl(25,5): Error: a postcondition could not be proved on this return path
+isolateJumpAndSplitOnEveryAssert.bpl(17,3): Related location: this is the postcondition that could not be proved
+
+Boogie program verifier finished with 0 verified, 3 errors