first commit

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<Cmd> RewriteCmdSeq(List<Cmd> cmdSeq)
     {
       if (cmd is CallCmd callCmd)
       {
-        if (IsPrimitive(callCmd.Proc))
+        if (CivlPrimitives.IsPrimitive(callCmd.Proc))
         {
           newCmdSeq.AddRange(RewriteCallCmd(callCmd));
         }

Source/Concurrency/LinearTypeChecker.cs

@@ -191,7 +191,7 @@ private HashSet<Variable> 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<Variable>();
       var globalInVars = new HashSet<Variable>();
       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;
         }

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));
           }

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;
   }
 

Source/Core/BoogiePL.atg

@@ -759,17 +759,19 @@ SpecRefinedActionForAtomicAction<ref ActionDeclRef refinedAction>
 
 SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs.>
 =
-  (. IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList; .)
+  (. IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList; .)
   "refines"
   { Attribute<ref kv> }
   (
     MoverQualifier<ref moverType>
     "action" (. tok = t; .)
     { 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<ActionDeclRef>(), null, null,
                                       new List<Requires>(), new List<CallCmd>(), new List<AssertCmd>(), new List<IdentifierExpr>(), null, akv);

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)

Source/Core/Parser.cs

@@ -1219,7 +1219,7 @@ void SpecRefinedActionForAtomicAction(ref ActionDeclRef refinedAction) {
 	}
 
 	void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs) {
-		IToken tok, unused; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> locals; StmtList stmtList; 
+		IToken tok, m; QKeyValue kv = null, akv = null; MoverType moverType = MoverType.None; List<Variable> 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<ActionDeclRef>(), null, null,
 			                               new List<Requires>(), new List<CallCmd>(), new List<AssertCmd>(), new List<IdentifierExpr>(), null, akv);

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
 

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)

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;
+}

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