[Civl] Bug fix in anonymous actions (#981)

boogie-org · Nov 10, 2024 · 29a06a9 · 29a06a9
1 parent 20e2656
commit 29a06a9
Show file tree

Hide file tree

Showing 12 changed files with 203 additions and 228 deletions.
diff --git 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<Cmd> RewriteCmdSeq(List<Cmd> 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
@@ -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;
         }

diff --git 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
@@ -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
@@ -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);

diff --git 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
@@ -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);