[Civl] Turn modset analysis on (#987)

This PR makes specification of modifies clauses optional on atomic
actions. It also makes it possible to optionally specify a name for an
atomic action defined in a refines specification.

Source/Core/AST/Absy.cs

@@ -2951,12 +2951,6 @@ 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

@@ -26,39 +26,10 @@ public ModSetCollector(CoreOptions options)
 
   private bool moreProcessingRequired;
 
-  public void DoModSetAnalysis(Implementation impl)
-  {
-    this.VisitImplementation(impl);
-    var proc = impl.Proc;
-    if (modSets.ContainsKey(proc))
-    {
-      proc.Modifies = new List<IdentifierExpr>(modSets[proc].Select(v => new IdentifierExpr(v.tok, v)));
-    }
-    else
-    {
-      proc.Modifies = new List<IdentifierExpr>();
-    }
-  }
-
   public void DoModSetAnalysis(Program program)
   {
     Contract.Requires(program != null);
-
-    if (options.Trace)
-    {
-//          Console.WriteLine();
-//          Console.WriteLine("Running modset analysis ...");
-//          int procCount = 0;
-//          foreach (Declaration/*!*/ decl in program.TopLevelDeclarations)
-//          {
-//              Contract.Assert(decl != null);
-//              if (decl is Procedure)
-//                  procCount++;
-//          }
-//          Console.WriteLine("Number of procedures = {0}", procCount);*/
-    }
-
-    HashSet<Procedure /*!*/> implementedProcs = new HashSet<Procedure /*!*/>();
+    var implementedProcs = new HashSet<Procedure>();
     foreach (var impl in program.Implementations)
     {
       if (impl.Proc != null)
@@ -67,7 +38,7 @@ public void DoModSetAnalysis(Program program)
       }
     }
 
-    foreach (var proc in program.Procedures)
+    foreach (var proc in program.Procedures.Where(x => x is not YieldProcedureDecl))
     {
       if (!implementedProcs.Contains(proc))
       {
@@ -104,30 +75,33 @@ public void DoModSetAnalysis(Program program)
 
 #if DEBUG_PRINT
       options.OutputWriter.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count);
-      foreach (Procedure/*!*/ x in modSets.Keys) {
+      foreach (Procedure x in modSets.Keys)
+      {
         Contract.Assert(x != null);
         options.OutputWriter.Write("{0} : ", x.Name);
         bool first = true;
-        foreach (Variable/*!*/ y in modSets[x]) {
-          Contract.Assert(y != null);
+        foreach (var y in modSets[x])
+        {
           if (first)
+          {
             first = false;
+          }
           else
+          {
             options.OutputWriter.Write(", ");
+          }
           options.OutputWriter.Write("{0}", y.Name);
         }
         options.OutputWriter.WriteLine("");
-      options.OutputWriter
+      }
 #endif
   }
 
   public override Implementation VisitImplementation(Implementation node)
   {
-    //Contract.Requires(node != null);
     Contract.Ensures(Contract.Result<Implementation>() != null);
     enclosingProc = node.Proc;
-    Implementation /*!*/
-      ret = base.VisitImplementation(node);
+    Implementation ret = base.VisitImplementation(node);
     Contract.Assert(ret != null);
     enclosingProc = null;
 
@@ -173,9 +147,14 @@ public override Cmd VisitHavocCmd(HavocCmd havocCmd)
 
   public override Cmd VisitCallCmd(CallCmd callCmd)
   {
-    //Contract.Requires(callCmd != null);
     Contract.Ensures(Contract.Result<Cmd>() != null);
     Cmd ret = base.VisitCallCmd(callCmd);
+
+    if (callCmd.IsAsync)
+    {
+      return ret;
+    }
+
     foreach (IdentifierExpr ie in callCmd.Outs)
     {
       if (ie != null)
@@ -219,7 +198,7 @@ private void ProcessVariable(Variable var)
       return;
     }
 
-    if (!(var is GlobalVariable))
+    if (var is not GlobalVariable)
     {
       return;
     }

Source/Core/BoogiePL.atg

@@ -769,10 +769,9 @@ SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name
     Ident<out m>
     ImplBody<out locals, out stmtList>
     (.
-      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),
+      if (refinedAction == null) {
+        var actionName = m.val == "_" ? null : m.val;
+        var actionDecl = new ActionDecl(tok, actionName, 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);

Source/Core/CoreOptions.cs

@@ -55,7 +55,7 @@ public enum VerbosityLevel
     bool OverlookBoogieTypeErrors { get; }
     uint TimeLimit { get; }
     uint ResourceLimit { get; }
-    bool DoModSetAnalysis { get; }
+    bool DoModSetAnalysis { get; set; }
     bool DebugStagedHoudini { get; }
     int LoopUnrollCount { get; }
     bool DeterministicExtractLoops { get; }

Source/Core/Parser.cs

@@ -1235,10 +1235,9 @@ void SpecRefinedActionForYieldProcedure(ref ActionDeclRef refinedAction, IToken
 			}
 			Ident(out m);
 			ImplBody(out locals, out stmtList);
-			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),
+			if (refinedAction == null) {
+			 var actionName = m.val == "_" ? null : m.val;
+			 var actionDecl = new ActionDecl(tok, actionName, 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);

Source/Core/ResolutionContext.cs

@@ -751,7 +751,7 @@ public class TypecheckingContext : CheckingContext
     public LayerRange ExpectedLayerRange;
     public bool GlobalAccessOnlyInOld;
     public int InsideOld;
-    public bool CheckModifies => Proc != null && (Proc.IsPure || (!Options?.DoModSetAnalysis ?? true));
+    public bool CheckModifies => Proc != null && (!Options?.DoModSetAnalysis ?? true);
 
     public TypecheckingContext(IErrorSink errorSink, CoreOptions options)
       : base(errorSink)

Source/ExecutionEngine/ExecutionEngine.cs

@@ -339,6 +339,7 @@ public Program ParseBoogieProgram(IList<string> fileNames, bool suppressTraceOut
         if (program.TopLevelDeclarations.Any(d => d.HasCivlAttribute()))
         {
           Options.Libraries.Add("base");
+          Options.DoModSetAnalysis = true;
         }
 
         foreach (var libraryName in Options.Libraries)

Test/civl/regression-tests/Pure1.bpl

@@ -17,4 +17,14 @@ async atomic action A()
 pure action F()
 creates A;
 {
-}
+}
+
+pure action G(d: int)
+{
+    x := d;
+}
+
+pure action H() returns (d: int)
+{
+    d := x;
+}

Test/civl/regression-tests/Pure1.bpl.expect

@@ -1,4 +1,6 @@
 Pure1.bpl(6,12): Error: unnecessary modifies clause for pure action
 Pure1.bpl(10,9): Error: cannot refer to a global variable in this context: x
 Pure1.bpl(17,12): Error: unnecessary creates clause for pure action
-3 name resolution errors detected in Pure1.bpl
+Pure1.bpl(24,4): Error: cannot refer to a global variable in this context: x
+Pure1.bpl(29,9): Error: cannot refer to a global variable in this context: x
+5 name resolution errors detected in Pure1.bpl

Test/civl/regression-tests/anonymous-action.bpl

@@ -14,4 +14,15 @@ refines both action {:layer 2} _ {
 }
 {
     call j := A(i);
+}
+
+yield procedure {:layer 0} C(i: int) returns (j: int);
+refines both action {:layer 1} AC {
+    call Incr();
+}
+
+action {:layer 1} Incr()
+modifies x;
+{
+    x := x + 1;
 }

Test/civl/regression-tests/anonymous-action.bpl.expect

@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 3 verified, 0 errors
+Boogie program verifier finished with 6 verified, 0 errors