diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs index b7669f65e..c5a2c181b 100644 --- a/Source/Concurrency/LinearRewriter.cs +++ b/Source/Concurrency/LinearRewriter.cs @@ -17,14 +17,9 @@ public LinearRewriter(CivlTypeChecker civlTypeChecker) this.civlTypeChecker = civlTypeChecker; } - public static bool IsPrimitive(DeclWithFormals decl) - { - return CivlPrimitives.LinearPrimitives.Contains(Monomorphizer.GetOriginalDecl(decl).Name); - } - public static void Rewrite(CivlTypeChecker civlTypeChecker, Implementation impl) { - if (IsPrimitive(impl)) { + if (CivlPrimitives.IsPrimitive(impl)) { return; } var linearRewriter = new LinearRewriter(civlTypeChecker); @@ -38,7 +33,7 @@ private List RewriteCmdSeq(List cmdSeq) { if (cmd is CallCmd callCmd) { - if (IsPrimitive(callCmd.Proc)) + if (CivlPrimitives.IsPrimitive(callCmd.Proc)) { newCmdSeq.AddRange(RewriteCallCmd(callCmd)); } diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index 883bf4e71..ec49ab946 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -191,7 +191,7 @@ private HashSet PropagateAvailableLinearVarsAcrossBlock(Block b) } else if (cmd is CallCmd callCmd) { - var isPrimitive = LinearRewriter.IsPrimitive(callCmd.Proc); + var isPrimitive = CivlPrimitives.IsPrimitive(callCmd.Proc); if (!isPrimitive) { linearGlobalVariables.Except(start).ForEach(g => @@ -338,7 +338,7 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node) public override Implementation VisitImplementation(Implementation node) { - if (LinearRewriter.IsPrimitive(node)) + if (CivlPrimitives.IsPrimitive(node)) { return node; } @@ -538,7 +538,7 @@ public override Cmd VisitUnpackCmd(UnpackCmd node) public override Cmd VisitCallCmd(CallCmd node) { - var isPrimitive = LinearRewriter.IsPrimitive(node.Proc); + var isPrimitive = CivlPrimitives.IsPrimitive(node.Proc); var inVars = new HashSet(); var globalInVars = new HashSet(); for (int i = 0; i < node.Proc.InParams.Count; i++) @@ -752,7 +752,7 @@ enclosingProc is not YieldProcedureDecl && public override Cmd VisitParCallCmd(ParCallCmd node) { - if (node.CallCmds.Any(callCmd => LinearRewriter.IsPrimitive(callCmd.Proc))) + if (node.CallCmds.Any(callCmd => CivlPrimitives.IsPrimitive(callCmd.Proc))) { Error(node, "linear primitives may not be invoked in a parallel call"); return node; @@ -831,7 +831,7 @@ private bool InvalidAssignmentWithKeyCollection(Variable target, Variable source private void CheckLinearStoreAccessInGuards() { program.Implementations.ForEach(impl => { - if (LinearRewriter.IsPrimitive(impl)) + if (CivlPrimitives.IsPrimitive(impl)) { return; } diff --git a/Source/Concurrency/YieldingProcDuplicator.cs b/Source/Concurrency/YieldingProcDuplicator.cs index 00179df17..182c494db 100644 --- a/Source/Concurrency/YieldingProcDuplicator.cs +++ b/Source/Concurrency/YieldingProcDuplicator.cs @@ -259,7 +259,7 @@ private void ProcessCallCmd(CallCmd newCall) InjectGate(pureAction, newCall); newCmdSeq.Add(newCall); } - else if (LinearRewriter.IsPrimitive(newCall.Proc)) + else if (CivlPrimitives.IsPrimitive(newCall.Proc)) { newCmdSeq.AddRange(linearRewriter.RewriteCallCmd(newCall)); } diff --git a/Source/Core/Analysis/ModSetCollector.cs b/Source/Core/Analysis/ModSetCollector.cs index f7e0f0a4f..c1939d9c1 100644 --- a/Source/Core/Analysis/ModSetCollector.cs +++ b/Source/Core/Analysis/ModSetCollector.cs @@ -194,6 +194,15 @@ public override Cmd VisitCallCmd(CallCmd callCmd) } } + if (CivlPrimitives.IsPrimitive(callCmd.Proc)) + { + var modifiedArgument = CivlPrimitives.ModifiedArgument(callCmd)?.Decl; + if (modifiedArgument != null) + { + ProcessVariable(modifiedArgument); + } + } + return ret; } diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 348ac2580..7cabd38ce 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -759,17 +759,19 @@ SpecRefinedActionForAtomicAction SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List ins, List outs.> = - (. IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List locals; StmtList stmtList; .) + (. IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List locals; StmtList stmtList; .) "refines" { Attribute } ( MoverQualifier "action" (. tok = t; .) { Attribute } - Ident + Ident ImplBody (. - if (refinedAction == null) { + if (m.val != "_") { + this.SemErr("expected _ for name of anoonymous action"); + } else if (refinedAction == null) { var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), false, new List(), null, null, new List(), new List(), new List(), new List(), null, akv); diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs index 3e3ff4bc5..425d70be4 100644 --- a/Source/Core/CivlAttributes.cs +++ b/Source/Core/CivlAttributes.cs @@ -223,6 +223,11 @@ public static class CivlPrimitives "Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put" }; + public static bool IsPrimitive(DeclWithFormals decl) + { + return LinearPrimitives.Contains(Monomorphizer.GetOriginalDecl(decl).Name); + } + public static IdentifierExpr ExtractRootFromAccessPathExpr(Expr expr) { if (expr is IdentifierExpr identifierExpr) diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 703fa7b8b..e048776fe 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1219,7 +1219,7 @@ void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) { } void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken name, List ins, List outs) { - IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List locals; StmtList stmtList; + IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List locals; StmtList stmtList; Expect(41); while (la.kind == 26) { Attribute(ref kv); @@ -1231,9 +1231,11 @@ void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken while (la.kind == 26) { Attribute(ref akv); } - Ident(out unused); + Ident(out m); ImplBody(out locals, out stmtList); - if (refinedAction == null) { + if (m.val != "_") { + this.SemErr("expected _ for name of anoonymous action"); + } else if (refinedAction == null) { var actionDecl = new ActionDecl(tok, null, moverType, Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), false, new List(), null, null, new List(), new List(), new List(), new List(), null, akv); diff --git a/Test/civl/large-samples/treiber-stack.bpl b/Test/civl/large-samples/treiber-stack.bpl index 44008baa2..7f999cad2 100644 --- a/Test/civl/large-samples/treiber-stack.bpl +++ b/Test/civl/large-samples/treiber-stack.bpl @@ -43,20 +43,17 @@ invariant Map_Contains(ts, loc_t); invariant (var t := ts->val[loc_t]; Between(t->stack->val, t->top, t->top, None())); invariant (var t := ts->val[loc_t]; IsSubset(BetweenSet(t->stack->val, t->top, None()), Domain(ts, loc_t)->val)); invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t)); -invariant (forall {:pool "A"} loc_n: LocTreiberNode :: {:add_to_pool "A", loc_n} Set_Contains(Domain(ts, loc_t), loc_n) ==> - loc_n == KeyedLoc(loc_n->l, Left()) && - (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t))); +invariant (forall {:pool "A"} loc_n: LocTreiberNode :: {:add_to_pool "A", loc_n} Set_Contains(Domain(ts, loc_t), loc_n) ==> loc_n == KeyedLoc(loc_n->l, Left())); invariant Map_At(Stack, loc_t) == Abs(Map_At(ts, loc_t)); yield invariant {:layer 4} StackDom(); invariant Stack->dom == ts->dom; -yield invariant {:layer 4} PushLocInStack( - loc_t: Loc, node: StackElem X, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One LocTreiberNode); +yield invariant {:layer 4} PushLocInStack(loc_t: Loc, node: StackElem X, new_loc_n: LocTreiberNode, {:linear} right_loc_piece: One LocTreiberNode); invariant Map_Contains(ts, loc_t); invariant Set_Contains(Domain(ts, loc_t), new_loc_n); -invariant right_loc_piece->val == KeyedLoc(new_loc_n->l, Right()); invariant new_loc_n == KeyedLoc(new_loc_n->l, Left()); +invariant right_loc_piece->val == KeyedLoc(new_loc_n->l, Right()); invariant (var t := ts->val[loc_t]; Map_At(t->stack, new_loc_n) == node && !BetweenSet(t->stack->val, t->top, None())[new_loc_n]); /// Layered implementation @@ -309,8 +306,8 @@ refines AtomicLoadNode#1; yield procedure {:layer 0} LoadNode#0(loc_t: Loc, loc_n: LocTreiberNode) returns (node: StackElem X); refines AtomicLoadNode#0; -atomic action {:layer 1,2} AtomicReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode) -modifies ts; +yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode); +refines atomic action {:layer 1,2} _ { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; @@ -319,12 +316,10 @@ modifies ts; loc_n := treiber->top; call Map_Put(ts, one_loc_t, treiber); } -yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc) returns (loc_n: Option LocTreiberNode); -refines AtomicReadTopOfStack#0; -atomic action {:layer 1,4} AtomicWriteTopOfStack#0( - loc_t: Loc, old_loc_n: Option LocTreiberNode, new_loc_n: Option LocTreiberNode) returns (success: bool) -modifies ts; +yield procedure {:layer 0} WriteTopOfStack#0( + loc_t: Loc, old_loc_n: Option LocTreiberNode, new_loc_n: Option LocTreiberNode) returns (success: bool); +refines atomic action {:layer 1,4} _ { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; @@ -338,12 +333,9 @@ modifies ts; } call Map_Put(ts, one_loc_t, treiber); } -yield procedure {:layer 0} WriteTopOfStack#0( - loc_t: Loc, old_loc_n: Option LocTreiberNode, new_loc_n: Option LocTreiberNode) returns (success: bool); -refines AtomicWriteTopOfStack#0; -atomic action {:layer 1,3} AtomicAllocNode#0(loc_t: Loc, {:linear_in} loc_piece: One LocTreiberNode, node: StackElem X) -modifies ts; +yield procedure {:layer 0} AllocNode#0(loc_t: Loc, {:linear_in} loc_piece: One LocTreiberNode, node: StackElem X); +refines atomic action {:layer 1,3} _ { var {:linear} one_loc_t: One Loc; var {:linear} treiber: Treiber X; @@ -352,16 +344,12 @@ modifies ts; call Map_Put(treiber->stack, loc_piece, node); call Map_Put(ts, one_loc_t, treiber); } -yield procedure {:layer 0} AllocNode#0(loc_t: Loc, {:linear_in} loc_piece: One LocTreiberNode, node: StackElem X); -refines AtomicAllocNode#0; -atomic action {:layer 1,4} AtomicAllocTreiber#0({:linear_in} one_loc_t: One Loc, {:linear_in} treiber: Treiber X) -modifies ts; +yield procedure {:layer 0} AllocTreiber#0({:linear_in} one_loc_t: One Loc, {:linear_in} treiber: Treiber X); +refines atomic action {:layer 1,4} _ { call Map_Put(ts, one_loc_t, treiber); } -yield procedure {:layer 0} AllocTreiber#0({:linear_in} one_loc_t: One Loc, {:linear_in} treiber: Treiber X); -refines AtomicAllocTreiber#0; /// Proof of abstraction with a manual encoding of termination diff --git a/Test/civl/paxos/PaxosImpl.bpl b/Test/civl/paxos/PaxosImpl.bpl index 9e97e1917..81479d4ba 100644 --- a/Test/civl/paxos/PaxosImpl.bpl +++ b/Test/civl/paxos/PaxosImpl.bpl @@ -290,9 +290,8 @@ ensures MaxRound(r, MapOr(ns1, ns2), voteInfo) == //////////////////////////////////////////////////////////////////////////////// -atomic action {:layer 1} A_JoinUpdate(r: Round, n: Node) -returns (join:bool, lastVoteRound: Round, lastVoteValue: Value) -modifies acceptorState; +yield procedure {:layer 0} JoinUpdate(r: Round, n: Node) returns (join:bool, lastVoteRound: Round, lastVoteValue: Value); +refines atomic action {:layer 1} _ { var lastJoinRound: Round; lastJoinRound := acceptorState[n]->lastJoinRound; @@ -306,9 +305,8 @@ modifies acceptorState; } } -atomic action {:layer 1} A_VoteUpdate(r: Round, n: Node, v: Value) -returns (vote:bool) -modifies acceptorState; +yield procedure {:layer 0} VoteUpdate(r: Round, n: Node, v: Value) returns (vote:bool); +refines atomic action {:layer 1} _ { var lastJoinRound: Round; lastJoinRound := acceptorState[n]->lastJoinRound; @@ -320,58 +318,34 @@ modifies acceptorState; } } -yield procedure {:layer 0} JoinUpdate(r: Round, n: Node) returns (join:bool, lastVoteRound: Round, lastVoteValue: Value); -refines A_JoinUpdate; - -yield procedure {:layer 0} VoteUpdate(r: Round, n: Node, v: Value) returns (vote:bool); -refines A_VoteUpdate; - //// Channel send/receive actions -left action {:layer 1} A_SendJoinResponse(round: Round, from: Node, lastVoteRound: Round, lastVoteValue: Value) -modifies joinChannel; +yield procedure {:layer 0} SendJoinResponse(round: Round, from: Node, lastVoteRound: Round, lastVoteValue: Value); +refines left action {:layer 1} _ { joinChannel[round][JoinResponse(from, lastVoteRound, lastVoteValue)] := joinChannel[round][JoinResponse(from, lastVoteRound, lastVoteValue)] + 1; } -right action {:layer 1} A_ReceiveJoinResponse(round: Round) -returns (joinResponse: JoinResponse) -modifies joinChannel; +yield procedure {:layer 0} ReceiveJoinResponse(round: Round) returns (joinResponse: JoinResponse); +refines right action {:layer 1} _ { assume joinChannel[round][joinResponse] > 0; joinChannel[round][joinResponse] := joinChannel[round][joinResponse] - 1; } -left action {:layer 1} A_SendVoteResponse(round: Round, from: Node) -modifies voteChannel; +yield procedure {:layer 0} SendVoteResponse(round: Round, from: Node); +refines left action {:layer 1} _ { voteChannel[round][VoteResponse(from)] := voteChannel[round][VoteResponse(from)] + 1; } -right action {:layer 1} A_ReceiveVoteResponse(round: Round) -returns (voteResponse: VoteResponse) -modifies voteChannel; +yield procedure {:layer 0} ReceiveVoteResponse(round: Round) returns (voteResponse: VoteResponse); +refines right action {:layer 1} _ { assume voteChannel[round][voteResponse] > 0; voteChannel[round][voteResponse] := voteChannel[round][voteResponse] - 1; } -yield procedure {:layer 0} -SendJoinResponse(round: Round, from: Node, lastVoteRound: Round, lastVoteValue: Value); -refines A_SendJoinResponse; - -yield procedure {:layer 0} -ReceiveJoinResponse(round: Round) returns (joinResponse: JoinResponse); -refines A_ReceiveJoinResponse; - -yield procedure {:layer 0} -SendVoteResponse(round: Round, from: Node); -refines A_SendVoteResponse; - -yield procedure {:layer 0} -ReceiveVoteResponse(round: Round) returns (voteResponse: VoteResponse); -refines A_ReceiveVoteResponse; - //// Introduction procedures to make send/receive more abstract pure action SendJoinResponseIntro(joinResponse: JoinResponse, {:linear_in} p: One Permission, {:linear_in} permJoinChannel: JoinResponseChannel) diff --git a/Test/civl/regression-tests/anonymous-action-fail.bpl b/Test/civl/regression-tests/anonymous-action-fail.bpl new file mode 100644 index 000000000..3ce5c15b1 --- /dev/null +++ b/Test/civl/regression-tests/anonymous-action-fail.bpl @@ -0,0 +1,9 @@ +// RUN: %parallel-boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +var {:layer 0,2} x: int; + +yield procedure {:layer 0} A(i: int) returns (j: int); +refines both action {:layer 1} B { + x := x + 1; +} \ No newline at end of file diff --git a/Test/civl/regression-tests/anonymous-action-fail.bpl.expect b/Test/civl/regression-tests/anonymous-action-fail.bpl.expect new file mode 100644 index 000000000..ad2fa5050 --- /dev/null +++ b/Test/civl/regression-tests/anonymous-action-fail.bpl.expect @@ -0,0 +1,2 @@ +anonymous-action-fail.bpl(9,1): error: expected _ for name of anoonymous action +1 parse errors detected in anonymous-action-fail.bpl