[Civl] Anonymous actions in refinement specification of yield procedures

Source/Core/AST/Absy.cs

@@ -2867,6 +2867,7 @@ public class ActionDecl : Procedure
     public List<CallCmd> YieldRequires;
     public List<AssertCmd> Asserts;
     public DatatypeTypeCtorDecl PendingAsyncCtorDecl;
+    public bool IsAnonymous;
 
     public Implementation Impl; // set when the implementation of this action is resolved
     public LayerRange LayerRange; // set during registration
@@ -2886,6 +2887,11 @@ public ActionDecl(IToken tok, string name, MoverType moverType,
       this.YieldRequires = yieldRequires;
       this.Asserts = asserts;
       this.PendingAsyncCtorDecl = pendingAsyncCtorDecl;
+      this.IsAnonymous = name == null;
+      if (IsAnonymous)
+      {
+        this.Name = $"AnonymousAction_{this.UniqueId}";
+      }
     }
 
     public override void Register(ResolutionContext rc)
@@ -2949,6 +2955,12 @@ public override void Resolve(ResolutionContext rc)
 
     public override void Typecheck(TypecheckingContext tc)
     {
+      if (IsAnonymous)
+      {
+        var modSetCollector = new ModSetCollector(tc.Options);
+        modSetCollector.DoModSetAnalysis(this.Impl);
+      }
+
       var oldProc = tc.Proc;
       tc.Proc = this;
       base.Typecheck(tc);

Source/Core/Analysis/ModSetCollector.cs

@@ -25,6 +25,17 @@ public ModSetCollector(CoreOptions options)
 
   private bool moreProcessingRequired;
 
+  public void DoModSetAnalysis(Implementation impl)
+  {
+    this.VisitImplementation(impl);
+    var proc = impl.Proc;
+    proc.Modifies = new List<IdentifierExpr>();
+    foreach (Variable v in modSets[proc])
+    {
+      proc.Modifies.Add(new IdentifierExpr(v.tok, v));
+    }
+  }
+
   public void DoModSetAnalysis(Program program)
   {
     Contract.Requires(program != null);

Source/Core/BoogiePL.atg

@@ -701,7 +701,7 @@ ActionDecl<bool isPure, out ActionDecl actionDecl, out Implementation impl, out
     ImplBody<out locals, out stmtList>
     (.
        impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
-                                      locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
+                                      locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone());
     .)
   )
   (.
@@ -742,25 +742,63 @@ SpecCreates<.List<ActionDeclRef> creates.>
   ";"
   .
 
-SpecRefinedAction<ref ActionDeclRef refinedAction>
+SpecRefinedActionForAtomicAction<ref ActionDeclRef refinedAction>
 =
   (. IToken m; QKeyValue kv = null; .) 
   "refines"
-  { Attribute<ref kv> } 
+  { Attribute<ref kv> }
   Ident<out m>
   (.
      if (refinedAction == null) {
-       refinedAction = new ActionDeclRef(m, m.val, kv);
+        refinedAction = new ActionDeclRef(m, m.val, kv);
      } else {
-       this.SemErr("a refines specification already exists");
+        this.SemErr("a refines specification already exists");
      }
   .)
   .
 
+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; .)
+  "refines"
+  { Attribute<ref kv> }
+  (
+    MoverQualifier<ref moverType>
+    "action" (. tok = t; .)
+    { Attribute<ref akv> }
+    Ident<out unused>
+    ImplBody<out locals, out stmtList>
+    (.
+      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);
+        Pgm.AddTopLevelDeclaration(actionDecl);
+        var impl = new Implementation(tok, actionDecl.Name, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
+                                      locals, stmtList, akv == null ? null : (QKeyValue)akv.Clone());
+        Pgm.AddTopLevelDeclaration(impl);
+        refinedAction = new ActionDeclRef(tok, actionDecl.Name);
+      } else {
+        this.SemErr("a refines specification already exists");
+      }
+    .)
+  |
+    Ident<out tok>
+    (.
+     if (refinedAction == null) {
+        refinedAction = new ActionDeclRef(tok, tok.val, kv);
+     } else {
+        this.SemErr("a refines specification already exists");
+     }
+    .)
+    ";"
+  )
+  .
+
 SpecAction<.ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List<IdentifierExpr> mods, List<ActionDeclRef> creates, List<Requires> requires, List<CallCmd> yieldRequires, List<AssertCmd> asserts.>
 =
   (
-    SpecRefinedAction<ref refinedAction>
+    SpecRefinedActionForAtomicAction<ref refinedAction>
     (. IToken m; .)
     ["using" Ident<out m> (. invariantAction = new ActionDeclRef(m, m.val); .)]
     ";"
@@ -803,8 +841,8 @@ YieldProcedureDecl<out YieldProcedureDecl ypDecl, out Implementation impl>
     ProcFormals<true, true, out ins>
       [ "returns" ProcFormals<false, true, out outs> ]
     ( ";"
-      { SpecYieldPrePost<ref refinedAction, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods> }
-    | { SpecYieldPrePost<ref refinedAction, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods> }
+      { SpecYieldPrePost<ref refinedAction, name, ins, outs, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods> }
+    | { SpecYieldPrePost<ref refinedAction, name, ins, outs, pre, post, yieldRequires, yieldEnsures, yieldPreserves, mods> }
       ImplBody<out locals, out stmtList>
       (.
          impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
@@ -855,11 +893,10 @@ SpecYieldPreserves<. List<CallCmd> yieldPreserves .>
   ";"
   .
 
-SpecYieldPrePost<. ref ActionDeclRef refinedAction, List<Requires> pre, List<Ensures> post, List<CallCmd> yieldRequires, List<CallCmd> yieldEnsures, List<CallCmd> yieldPreserves, List<IdentifierExpr> mods.>
+SpecYieldPrePost<. ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs, List<Requires> pre, List<Ensures> post, List<CallCmd> yieldRequires, List<CallCmd> yieldEnsures, List<CallCmd> yieldPreserves, List<IdentifierExpr> mods.>
 =
   (  
-    SpecRefinedAction<ref refinedAction>
-    ";"
+    SpecRefinedActionForYieldProcedure<ref refinedAction, name, ins, outs>
   | SpecYieldRequires<pre, yieldRequires>
   | SpecYieldEnsures<post, yieldEnsures>
   | SpecYieldPreserves<yieldPreserves>