[Civl] bug fix for noninterference checking for pending asyncs (#773)

For a particular layer number, those pending asyncs must be collected
for which noninterference checking against yield invariants must be
performed. The collection of pending asyncs was not sound earlier. This
PR makes a fix to make it sound.

Source/Concurrency/YieldingProcInstrumentation.cs

@@ -134,7 +134,7 @@ private List<Cmd> CreateUpdatesToOldGlobalVars()
       return cmds;
     }
 
-    private List<Cmd> CreateCallToYieldProc()
+    private List<Cmd> CreateCallToNoninterferenceChecker()
     {
       var cmds = new List<Cmd>();
       if (!civlTypeChecker.Options.TrustNoninterference)
@@ -608,7 +608,7 @@ private void SplitBlocks(Implementation impl)
     private Block CreateNoninterferenceCheckerBlock()
     {
       var newCmds = new List<Cmd>();
-      newCmds.AddRange(CreateCallToYieldProc());
+      newCmds.AddRange(CreateCallToNoninterferenceChecker());
       newCmds.Add(CmdHelper.AssumeCmd(Expr.False));
       return BlockHelper.Block(civlTypeChecker.AddNamePrefix("NoninterferenceChecker"), newCmds);
     }
@@ -756,10 +756,9 @@ private IEnumerable<Declaration> PendingAsyncNoninterferenceCheckers()
         yield break;
       }
 
-      var pendingAsyncsToCheck = new HashSet<Action>(
-        civlTypeChecker.MoverActions
-          .Where(a => a.LayerRange.Contains(layerNum) && a.HasPendingAsyncs)
-          .SelectMany(a => a.PendingAsyncs).Select(a => civlTypeChecker.Action(a)));
+      var pendingAsyncsToCheck =
+        new HashSet<Action>(civlTypeChecker.MoverActions.Where(a =>
+          a.LayerRange.Contains(layerNum) && a.ActionDecl.MaybePendingAsync));
 
       foreach (var action in pendingAsyncsToCheck)
       {
@@ -774,7 +773,7 @@ private IEnumerable<Declaration> PendingAsyncNoninterferenceCheckers()
         cmds.AddRange(CreateUpdatesToOldGlobalVars());
         cmds.AddRange(CreateUpdatesToPermissionCollector(action.Impl));
         cmds.Add(CmdHelper.CallCmd(action.Impl.Proc, inputs, outputs));
-        cmds.AddRange(CreateCallToYieldProc());
+        cmds.AddRange(CreateCallToNoninterferenceChecker());
         var blocks = new List<Block> { BlockHelper.Block("init", cmds) };
 
         var name = civlTypeChecker.AddNamePrefix($"PendingAsyncNoninterferenceChecker_{action.Name}_{layerNum}");

Test/civl/async/async3.bpl.expect

@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 4 verified, 0 errors
+Boogie program verifier finished with 5 verified, 0 errors

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

@@ -0,0 +1,32 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+atomic action {:layer 3} A_Foo()
+creates A_Incr;
+{
+    call create_async(A_Incr());
+}
+
+yield procedure {:layer 2} Foo()
+refines A_Foo;
+{
+    async call Incr();
+}
+
+async atomic action {:layer 1,3} A_Incr()
+modifies x;
+{
+    x := x + 1;
+}
+
+yield procedure {:layer 0} Incr();
+refines A_Incr;
+
+yield invariant {:layer 1} Inv();
+invariant x == 0;
+
+var {:layer 0,3} x: int;
+
+yield procedure {:layer 1} Bar()
+preserves call Inv();
+{ }

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

@@ -0,0 +1,7 @@
+pa-noninterference-check.bpl(26,1): Error: Non-interference check failed
+Execution trace:
+    pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Entry
+    pa-noninterference-check.bpl(19,7): inline$A_Incr$0$anon0
+    pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Return
+
+Boogie program verifier finished with 4 verified, 1 error