Merge remote-tracking branch 'fork/isolatePaths' into isolatePathsNext

Source/Concurrency/CivlUtil.cs

@@ -307,14 +307,16 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars)
 
   public static class BlockHelper
   {
+    public static readonly IToken /*!*/ ReportedNoToken = new Token();
+
     public static Block Block(string label, List<Cmd> cmds)
     {
-      return new Block(Token.NoToken, label, cmds, CmdHelper.ReturnCmd);
+      return new Block(ReportedNoToken, label, cmds, CmdHelper.ReturnCmd);
     }
 
     public static Block Block(string label, List<Cmd> cmds, List<Block> gotoTargets)
     {
-      return new Block(Token.NoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
+      return new Block(ReportedNoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
     }
   }
 

Source/Core/AST/ICarriesAttributes.cs

@@ -40,8 +40,6 @@ public List<int> FindLayers()
     }
     return layers.Distinct().OrderBy(l => l).ToList();
   }
-
-
 }
 
 public static class QKeyValueExtensions {

Source/Core/Token.cs

@@ -33,8 +33,7 @@ public string /*!*/
 
     public Token next; // ML 2005-03-11 Tokens are kept in linked list
 
-    public static readonly IToken /*!*/
-      NoToken = new Token();
+    public static readonly IToken /*!*/ NoToken = new Token();
 
     public Token()
     {

Source/Core/VariableDependenceAnalyser.cs

@@ -548,7 +548,7 @@ private Dictionary<Block, HashSet<Block>> ComputeGlobalControlDependences()
             var indirectCallees = ComputeIndirectCallees(callGraph, directCallee);
             foreach (var control in GetControllingBlocks(b, localCtrlDeps[impl]))
             {
-              foreach (var c in indirectCallees.Select(Item => Item.Blocks).SelectMany(item => item))
+              foreach (var c in indirectCallees.Select(item => item.Blocks).SelectMany(item => item))
               {
                 globalCtrlDep[control].Add(c);
               }

Source/Directory.Build.props

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

Source/VCGeneration/Counterexample/Counterexample.cs

@@ -124,8 +124,6 @@ public void Print(int indent, TextWriter tw, Action<Block> blockAction = null)
         }
         else {
           // for ErrorTrace == 1 restrict the output;
-          // do not print tokens with -17:-4 as their location because they have been
-          // introduced in the translation and do not give any useful feedback to the user
           if (Options.ErrorTrace == 1 && block.tok == Token.NoToken) {
             continue;
           }

Source/VCGeneration/Splits/BlockRewriter.cs

@@ -167,4 +167,10 @@ public List<Block> ComputeNewBlocks(
     BlockCoalescer.CoalesceInPlace(newBlocks);
     return newBlocks;
   }
+
+
+  public static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute)
+  {
+    return splitOnEveryAssert || isolateAttribute != null;
+  }
 }

Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs

@@ -28,7 +28,7 @@ public static (List<ManualSplit> IsolatedParts, ManualSplit Remainder) GetParts(
       foreach (var assert in block.Cmds.OfType<AssertCmd>()) {
         var attributes = assert.Attributes;
         var isolateAttribute = QKeyValue.FindAttribute(attributes, p => p.Key == "isolate");
-        if (!ShouldIsolate(splitOnEveryAssert, isolateAttribute)) {
+        if (!BlockRewriter.ShouldIsolate(splitOnEveryAssert, isolateAttribute)) {
           continue;
         }
 
@@ -90,18 +90,6 @@ List<Cmd> GetCommands(Block block) => block.Cmds.Select(cmd =>
         isolatedAssertions.Contains(cmd) ? rewriter.TransformAssertCmd(cmd) : cmd).ToList();
     }
   }
-
-  private static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute) {
-    if (splitOnEveryAssert) {
-      if (isolateAttribute == null) {
-        return true;
-      }
-
-      return !isolateAttribute.Params.OfType<string>().Any(p => Equals(p, "none"));
-    }
-
-    return isolateAttribute != null;
-  }
 }
 
 

Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs

@@ -33,7 +33,7 @@ public static (List<ManualSplit> Isolated, ManualSplit Remainder) GetParts(VCGen
 
       var isTypeOfAssert = gotoCmd.tok is GotoFromReturn;
       var isolateAttribute = QKeyValue.FindAttribute(gotoCmd.Attributes, p => p.Key == "isolate");
-      var isolate = ShouldIsolate(isTypeOfAssert && splitOnEveryAssert, isolateAttribute);
+      var isolate = BlockRewriter.ShouldIsolate(isTypeOfAssert && splitOnEveryAssert, isolateAttribute);
       if (!isolate) {
         continue;
       }
@@ -62,7 +62,6 @@ public static (List<ManualSplit> Isolated, ManualSplit Remainder) GetParts(VCGen
     return (results, GetPartWithoutIsolatedReturns());
 
     ManualSplit GetPartWithoutIsolatedReturns() {
-      // TODO this needs an extra test. In case the isolated jump is followed by something it dominates
       var newBlocks = rewriter.ComputeNewBlocks(blocks.ToHashSet(), (oldBlock, newBlock) => {
         if (isolatedBlockJumps.Contains(oldBlock)) {
           newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
@@ -72,18 +71,6 @@ ManualSplit GetPartWithoutIsolatedReturns() {
         newBlocks);
     }
   }
-
-  private static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute) {
-    if (splitOnEveryAssert) {
-      if (isolateAttribute == null) {
-        return true;
-      }
-
-      return !isolateAttribute.Params.OfType<string>().Any(p => Equals(p, "none"));
-    }
-
-    return isolateAttribute != null;
-  }
 }
 
 

Source/VCGeneration/Splits/Split.cs

@@ -98,7 +98,7 @@ private void PrintSplit() {
           Thread.Sleep(100);
         }
 
-        var prefix = (this is ManualSplit manualSplit) ? manualSplit.Token.ShortName : "";
+        var prefix = this is ManualSplit manualSplit ? manualSplit.Token.ShortName : "";
         var name = Implementation.Name + prefix; 
         using var writer = printToConsole
           ? new TokenTextWriter("<console>", Options.OutputWriter, false, Options.PrettyPrint, Options) 

Source/VCGeneration/VerificationConditionGenerator.cs

@@ -1352,22 +1352,22 @@ public static Counterexample AssertCmdToCounterexample(VCGenOptions options, Ass
     /// <summary>
     /// Returns a clone of "cex", but with the location stored in "cex" replaced by those from "assrt".
     /// </summary>
-    public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assrt,
+    public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assert,
       Counterexample cex,
       Block implEntryBlock)
     {
-      Contract.Requires(assrt != null);
+      Contract.Requires(assert != null);
       Contract.Requires(cex != null);
       Contract.Requires(implEntryBlock != null);
       Contract.Ensures(Contract.Result<Counterexample>() != null);
 
       Counterexample cc;
-      if (assrt is AssertRequiresCmd assertRequiresCmd)
+      if (assert is AssertRequiresCmd assertRequiresCmd)
       {
         cc = new CallCounterexample(options, cex.Trace, cex.AugmentedTrace, assertRequiresCmd, cex.Model, cex.MvInfo, cex.Context,
           cex.ProofRun, assertRequiresCmd.Checksum);
       }
-      else if (assrt is AssertEnsuresCmd assertEnsuresCmd && cex is ReturnCounterexample returnCounterexample)
+      else if (assert is AssertEnsuresCmd assertEnsuresCmd && cex is ReturnCounterexample returnCounterexample)
       {
         // The first three parameters of ReturnCounterexample are: List<Block> trace, List<object> augmentedTrace, TransferCmd failingReturn, Ensures failingEnsures.
         // We have the "aa" version of failingEnsures, namely aa.Ensures.  The first and third parameters take more work to reconstruct.
@@ -1451,7 +1451,7 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options
       }
       else
       {
-        cc = new AssertCounterexample(options, cex.Trace, cex.AugmentedTrace, assrt, cex.Model, cex.MvInfo, cex.Context,
+        cc = new AssertCounterexample(options, cex.Trace, cex.AugmentedTrace, assert, cex.Model, cex.MvInfo, cex.Context,
           cex.ProofRun);
       }
 

Test/civl/regression-tests/intro-nonblocking.bpl.expect

@@ -1,4 +1,5 @@
 intro-nonblocking.bpl(4,13): Error: Cooperation check for intro failed
 Execution trace:
+    (0,0): init
 
 Boogie program verifier finished with 0 verified, 1 error

Test/civl/regression-tests/left-mover.bpl.expect

@@ -10,5 +10,6 @@ Execution trace:
     left-mover.bpl(6,24): inline$inc$0$Return
 left-mover.bpl(26,24): Error: Cooperation check for block failed
 Execution trace:
+    (0,0): init
 
 Boogie program verifier finished with 3 verified, 3 errors

Test/civl/regression-tests/non-interference-1.bpl.expect

@@ -2,5 +2,6 @@ non-interference-1.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     non-interference-1.bpl(7,3): anon0
     non-interference-1.bpl(12,5): inline$AtomicIncr$0$anon0
+    (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L
 
 Boogie program verifier finished with 4 verified, 1 error

Test/civl/regression-tests/non-interference-2.bpl.expect

@@ -2,8 +2,10 @@ non-interference-2.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     non-interference-2.bpl(7,3): anon0
     non-interference-2.bpl(12,5): inline$AtomicIncr$0$anon0
+    (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L
 non-interference-2.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     non-interference-2.bpl(34,3): anon0
+    (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L
 
 Boogie program verifier finished with 2 verified, 2 errors

Test/civl/regression-tests/pa-noninterference-check.bpl.expect

@@ -1,5 +1,6 @@
 pa-noninterference-check.bpl(26,1): Error: Non-interference check failed
 Execution trace:
+    (0,0): init
     pa-noninterference-check.bpl(19,7): inline$A_Incr$0$anon0
     pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Return
 

Test/civl/regression-tests/parallel1.bpl.expect

@@ -2,5 +2,6 @@ parallel1.bpl(25,1): Error: Non-interference check failed
 Execution trace:
     parallel1.bpl(7,3): anon0
     parallel1.bpl(12,5): inline$AtomicIncr$0$anon0
+    (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L
 
 Boogie program verifier finished with 3 verified, 1 error

Test/civl/regression-tests/parallel6.bpl.expect

@@ -7,5 +7,6 @@ Execution trace:
     parallel6.bpl(11,5): anon0_0
     parallel6.bpl(30,7): inline$atomic_incr$2$anon0
     parallel6.bpl(30,7): inline$atomic_incr$3$anon0
+    (0,0): Civl_ReturnChecker
 
 Boogie program verifier finished with 7 verified, 1 error

Test/civl/regression-tests/pending-async-1.bpl.expect

@@ -5,6 +5,7 @@ Execution trace:
     pending-async-1.bpl(51,3): anon0$1
     pending-async-1.bpl(11,9): inline$B$1$anon0
     pending-async-1.bpl(51,3): anon0$2
+    (0,0): Civl_ReturnChecker
 pending-async-1.bpl(67,3): Error: Pending asyncs to action A created by this call are not summarized
 Execution trace:
     pending-async-1.bpl(67,3): anon0

Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect

@@ -1,5 +1,6 @@
 pending-async-noninterference-fail.bpl(7,1): Error: Non-interference check failed
 Execution trace:
+    (0,0): init
     pending-async-noninterference-fail.bpl(12,5): inline$A$0$anon0
     pending-async-noninterference-fail.bpl(9,32): inline$A$0$Return
 

Test/civl/regression-tests/refinement.bpl.expect

@@ -5,21 +5,25 @@ Execution trace:
     refinement.bpl(10,3): anon0$1
     refinement.bpl(10,3): anon0_0
     refinement.bpl(58,5): inline$INCR$1$anon0
+    (0,0): Civl_ReturnChecker
 refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state in a way that does not match the refined atomic action
 Execution trace:
     refinement.bpl(18,3): anon0
     refinement.bpl(64,5): inline$DECR$0$anon0
     refinement.bpl(18,3): anon0$1
+    (0,0): Civl_RefinementChecker
 refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state
 Execution trace:
     refinement.bpl(18,3): anon0
     refinement.bpl(64,5): inline$DECR$0$anon0
     refinement.bpl(18,3): anon0$1
     refinement.bpl(18,3): anon0_0
     refinement.bpl(58,5): inline$INCR$0$anon0
+    (0,0): Civl_ReturnChecker
 refinement.bpl(37,28): Error: On some path no yield-to-yield fragment matched the refined atomic action
 Execution trace:
     refinement.bpl(41,1): anon0
+    (0,0): Civl_ReturnChecker
 refinement.bpl(43,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals
 Execution trace:
     refinement.bpl(46,3): anon0
@@ -28,5 +32,6 @@ Execution trace:
     refinement.bpl(46,3): anon0_0
     refinement.bpl(48,3): anon2_LoopHead
     refinement.bpl(58,5): inline$INCR$1$anon0
+    (0,0): Civl_UnchangedChecker
 
 Boogie program verifier finished with 3 verified, 5 errors

Test/civl/regression-tests/refinement2.bpl.expect

@@ -1,11 +1,15 @@
 refinement2.bpl(13,28): Error: On some path no yield-to-yield fragment matched the refined atomic action
 Execution trace:
     refinement2.bpl(16,5): anon0
+    (0,0): Civl_call_refinement_4
     refinement2.bpl(27,28): inline$atomic_nop$0$Return
+    (0,0): Civl_ReturnChecker
 refinement2.bpl(13,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals
 Execution trace:
     refinement2.bpl(16,5): anon0
+    (0,0): Civl_call_refinement_3
     refinement2.bpl(22,7): inline$atomic_incr$0$anon0
     refinement2.bpl(19,28): inline$atomic_incr$0$Return
+    (0,0): Civl_UnchangedChecker
 
 Boogie program verifier finished with 1 verified, 2 errors

Test/civl/regression-tests/yield-invariant-fails.bpl.expect

@@ -2,5 +2,6 @@ yield-invariant-fails.bpl(7,1): Error: Non-interference check failed
 Execution trace:
     yield-invariant-fails.bpl(11,5): anon0
     yield-invariant-fails.bpl(19,7): inline$atomic_A$0$anon0
+    (0,0): inline$Civl_NoninterferenceChecker_yield_Inv$0$L
 
 Boogie program verifier finished with 0 verified, 1 error