bug fix

boogie-org · Aug 13, 2023 · 2c4ed4c · 2c4ed4c
1 parent eb7e2e5
commit 2c4ed4c
Show file tree

Hide file tree

Showing 4 changed files with 46 additions and 8 deletions.
diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/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}");

diff --git a/Test/civl/async/async3.bpl.expect b/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
diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl b/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();
+{ }
diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect b/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