From dbd883181a7aae41c956891dc5aa5213968113ea Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Mon, 29 Jul 2024 17:13:13 -0700 Subject: [PATCH] first commit --- Source/Concurrency/YieldingProcDuplicator.cs | 18 +++- Source/Core/AST/Absy.cs | 11 ++- Source/Core/AST/CallCmd.cs | 98 ++++++++++--------- Source/Core/CivlAttributes.cs | 2 +- Test/civl/regression-tests/refinement3.bpl | 26 +++++ .../regression-tests/refinement3.bpl.expect | 5 + 6 files changed, 110 insertions(+), 50 deletions(-) create mode 100644 Test/civl/regression-tests/refinement3.bpl create mode 100644 Test/civl/regression-tests/refinement3.bpl.expect diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs index 61a20c07d..00179df17 100644 --- 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 index adead1f1f..483652543 100644 --- a/Source/Core/AST/Absy.cs +++ b/Source/Core/AST/Absy.cs @@ -3166,6 +3166,15 @@ public IEnumerable 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 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 index 1fd4cab7a..12646a965 100644 --- a/Source/Core/AST/CallCmd.cs +++ b/Source/Core/AST/CallCmd.cs @@ -301,6 +301,7 @@ void CheckModifies(IEnumerable 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 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 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 index 5c86ee686..50df03fa1 100644 --- 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 new file mode 100644 index 000000000..3de8708c6 --- /dev/null +++ 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; \ No newline at end of file diff --git a/Test/civl/regression-tests/refinement3.bpl.expect b/Test/civl/regression-tests/refinement3.bpl.expect new file mode 100644 index 000000000..3cee83cf8 --- /dev/null +++ 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