boogie-org · shazqadeer · Jul 30, 2024 · Jul 30, 2024
diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs
@@ -297,7 +297,15 @@ private void ProcessCallCmd(CallCmd newCall)
           }
           else if (IsRefinementLayer)
           {
-            AddPendingAsync(newCall, yieldingProc);
+            if (newCall.HasAttribute(CivlAttributes.SKIP))
+            {
+              var calleeRefinedAction = PrepareNewCall(newCall, yieldingProc);
+              InjectGate(calleeRefinedAction, newCall);
+            }
+            else
+            {
+              AddPendingAsync(newCall, yieldingProc);
+            }
           }
         }
         else
@@ -406,7 +414,7 @@ private void ProcessParCallCmd(ParCallCmd newParCall)
       }
     }
 
-    private void AddActionCall(CallCmd newCall, YieldProcedureDecl calleeActionProc)
+    private Action PrepareNewCall(CallCmd newCall, YieldProcedureDecl calleeActionProc)
     {
       var calleeRefinedAction = civlTypeChecker.Action(calleeActionProc.RefinedActionAtLayer(layerNum));
 
@@ -438,6 +446,12 @@ private void AddActionCall(CallCmd newCall, YieldProcedureDecl calleeActionProc)
       newCall.Ins = newIns;
       newCall.Outs = newOuts;
 
+      return calleeRefinedAction;
+    }
+
+    private void AddActionCall(CallCmd newCall, YieldProcedureDecl calleeActionProc)
+    {
+      var calleeRefinedAction = PrepareNewCall(newCall, calleeActionProc);
       InjectGate(calleeRefinedAction, newCall, !IsRefinementLayer);
       newCmdSeq.Add(newCall);
 

diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
@@ -3166,6 +3166,15 @@ public IEnumerable<ActionDeclRef> ActionDeclRefs()
       return Creates.Append(RefinedAction).Append(InvariantAction);
     }
 
+    public bool IsSkippable()
+    {
+      return
+        Creates.Count == 0 &&
+        ModifiedVars.All(v => v.LayerRange.UpperLayer == LayerRange.UpperLayer) &&
+        Asserts.Count > 0 &&
+        !VariableCollector.Collect(Asserts).Any(v => v is GlobalVariable);
+    }
+
     public IEnumerable<ActionDecl> CreateActionDecls => Creates.Select(x => x.ActionDecl);
 
     public bool MaybePendingAsync => PendingAsyncCtorDecl != null;
@@ -3415,10 +3424,8 @@ public ActionDecl RefinedActionAtLayer(int layer)
         {
           return actionDecl;
         }
-
         actionDeclRef = actionDecl.RefinedAction;
       }
-
       return null;
     }
 

diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/CallCmd.cs
@@ -301,6 +301,7 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
     if (Proc is YieldProcedureDecl calleeDecl)
     {
       var isSynchronized = this.HasAttribute(CivlAttributes.SYNC);
+      var isSkipped = this.HasAttribute(CivlAttributes.SKIP);
       if (calleeDecl.Layer > callerDecl.Layer)
       {
         tc.Error(this, "layer of callee must not be more than layer of caller");
@@ -319,33 +320,58 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
             else
             {
               CheckModifies(highestRefinedActionDecl.ModifiedVars);
-              if (highestRefinedActionDecl.Creates.Any())
+              if (!IsAsync)
               {
-                if (callerDecl.HasMoverType)
+                if (highestRefinedActionDecl.Creates.Any() && callerDecl.HasMoverType)
                 {
                   tc.Error(this, "caller must not be a mover procedure");
                 }
+                // check there is no application of IS_RIGHT in the entire chain of refined actions
+                var calleeRefinedAction = calleeDecl.RefinedAction;
+                while (calleeRefinedAction != null)
+                {
+                  if (calleeRefinedAction.HasAttribute(CivlAttributes.IS_RIGHT))
+                  {
+                    tc.Error(this, "this must be an async call");
+                    break;
+                  }
+                  var calleeActionDecl = calleeRefinedAction.ActionDecl;
+                  if (calleeActionDecl == highestRefinedActionDecl)
+                  {
+                    break;
+                  }
+                  calleeRefinedAction = calleeActionDecl.RefinedAction;
+                }
               }
-              else if (IsAsync && isSynchronized)
+              else if (isSynchronized)
               {
                 // check that entire chain of refined actions all the way to highestRefinedAction is comprised of left movers
-                var actionDeclRef = calleeDecl.RefinedAction;
-                while (actionDeclRef != null)
+                var calleeRefinedAction = calleeDecl.RefinedAction;
+                while (calleeRefinedAction != null)
                 {
-                  var actionDecl = actionDeclRef.ActionDecl;
-                  if (!actionDecl.IsLeftMover)
+                  var calleeActionDecl = calleeRefinedAction.ActionDecl;
+                  if (!calleeActionDecl.IsLeftMover)
                   {
                     tc.Error(this,
-                      $"callee abstraction in synchronized call must be a left mover: {actionDecl.Name}");
-                  }
-                  else if (actionDecl != highestRefinedActionDecl)
-                  {
-                    actionDeclRef = actionDecl.RefinedAction;
+                      $"callee abstraction in synchronized call must be a left mover: {calleeActionDecl.Name}");
+                    break;
                   }
-                  else
+                  if (calleeActionDecl == highestRefinedActionDecl)
                   {
-                    actionDeclRef = null;
+                    break;
                   }
+                  calleeRefinedAction = calleeActionDecl.RefinedAction;
+                }
+              }
+              else if (isSkipped)
+              {
+                if (highestRefinedActionDecl.LayerRange.UpperLayer != callerDecl.Layer)
+                {
+                  tc.Error(this, $"upper layer of action {highestRefinedActionDecl.Name} must be same as layer of caller");
+                }
+                else if (!highestRefinedActionDecl.IsSkippable())
+                {
+                  tc.Error(this, $"action {highestRefinedActionDecl.Name} must be skippable");
                 }
               }
             }
@@ -357,41 +383,23 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
           {
             tc.Error(this, "caller must not be a mover procedure");
           }
-          else if (IsAsync && isSynchronized)
-          {
-            tc.Error(this, "layer of callee in synchronized call must be less than layer of caller");
-          }
-        }
-
-        if (!IsAsync) {
-          var calleeRefinedAction = calleeDecl.RefinedAction;
-          while (calleeRefinedAction != null) {
-            var calleeActionDecl = calleeRefinedAction.ActionDecl;
-            if (calleeActionDecl.LayerRange.UpperLayer >= callerDecl.Layer) {
-              break;
-            }
-            calleeRefinedAction = calleeActionDecl.RefinedAction;
-            if (calleeRefinedAction != null && calleeRefinedAction.HasAttribute(CivlAttributes.IS_RIGHT)) {
-              tc.Error(this, "this must be an async call");
-            }
-          }
-        }
-        else if (!isSynchronized)
-        {
-          if (callerDecl.HasMoverType)
-          {
-            tc.Error(this, "caller must not be a mover procedure");
-          }
-          else if (calleeDecl.RefinedAction != null)
+          else if (IsAsync && calleeDecl.RefinedAction != null)
           {
-            var highestRefinedAction = calleeDecl.RefinedActionAtLayer(callerDecl.Layer + 1);
-            if (highestRefinedAction == null)
+            if (isSynchronized)
             {
-              tc.Error(this, $"called action is not available at layer {callerDecl.Layer + 1}");
+              tc.Error(this, "layer of callee in synchronized call must be less than layer of caller");
             }
-            else if (!highestRefinedAction.MaybePendingAsync)
+            else
             {
-              tc.Error(this, $"action {highestRefinedAction.Name} refined by callee must be eligible to be a pending async");
+              var highestRefinedAction = calleeDecl.RefinedActionAtLayer(callerDecl.Layer + 1);
+              if (highestRefinedAction == null)
+              {
+                tc.Error(this, $"called action is not available at layer {callerDecl.Layer + 1}");
+              }
+              else if (!highestRefinedAction.MaybePendingAsync)
+              {
+                tc.Error(this, $"action {highestRefinedAction.Name} refined by callee must be eligible to be a pending async");
+              }
             }
           }
         }

diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs
@@ -86,7 +86,7 @@ public static class CivlAttributes
     public const string HIDE = "hide";
     public const string PENDING_ASYNC = "pending_async";
     public const string SYNC = "sync";
-
+    public const string SKIP = "skip";
     public const string IS_RIGHT = "IS_right";
     public const string IS_LEFT = "IS_left";
 

diff --git a/Test/civl/regression-tests/refinement3.bpl b/Test/civl/regression-tests/refinement3.bpl
@@ -0,0 +1,26 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+yield procedure {:layer 1} Good()
+{
+    async call {:skip} P_A();
+}
+
+atomic action {:layer 1} A()
+asserts true;
+{}
+
+yield procedure {:layer 0} P_A();
+refines A;
+
+yield procedure {:layer 1} Bad()
+{
+    async call {:skip} P_B();
+}
+
+atomic action {:layer 1} B()
+asserts false;
+{}
+
+yield procedure {:layer 0} P_B();
+refines B;
diff --git a/Test/civl/regression-tests/refinement3.bpl.expect b/Test/civl/regression-tests/refinement3.bpl.expect
@@ -0,0 +1,5 @@
+refinement3.bpl(22,1): Error: this gate of B could not be proved
+Execution trace:
+    refinement3.bpl(18,11): anon0
+
+Boogie program verifier finished with 3 verified, 1 error