Merge branch 'master' into exportHiddenFunctions

Source/Concurrency/CivlUtil.cs

@@ -133,7 +133,6 @@ public static int ResolveAndTypecheck(CoreOptions options, Absy absy, Resolution
       }
 
       var tc = new TypecheckingContext(null, options);
-      tc.CheckModifies = false; // to prevent access to tc.Proc which is null
       absy.Typecheck(tc);
       return tc.ErrorCount;
     }

Source/Concurrency/LinearRewriter.cs

@@ -530,10 +530,7 @@ private void ResolveAndTypecheck(CoreOptions options, IEnumerable<Absy> absys)
       return;
     }
     var tc = new TypecheckingContext(null, options);
-    var oldCheckModifies = tc.CheckModifies;
-    tc.CheckModifies = false;
     absys.ForEach(absy => absy.Typecheck(tc));
-    tc.CheckModifies = oldCheckModifies;
   }
 
   private List<Cmd> CreateAccessAsserts(Expr expr, IToken tok, string msg)

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

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 
 namespace Microsoft.Boogie;
 
@@ -25,36 +26,10 @@ 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);
-
-    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)
@@ -63,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))
       {
@@ -100,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;
 
@@ -169,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)
@@ -215,7 +198,7 @@ private void ProcessVariable(Variable var)
       return;
     }
 
-    if (!(var is GlobalVariable))
+    if (var is not GlobalVariable)
     {
       return;
     }

Source/Core/BoogiePL.atg

@@ -759,20 +759,19 @@ SpecRefinedActionForAtomicAction<ref ActionDeclRef refinedAction>
 
 SpecRefinedActionForYieldProcedure<.ref ActionDeclRef refinedAction, IToken name, List<Variable> ins, List<Variable> outs.>
 =
-  (. IToken tok, m; 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.Atomic; List<Variable> locals; StmtList stmtList; .)
   "refines"
   { Attribute<ref kv> }
   (
-    MoverQualifier<ref moverType>
+    [ MoverQualifier<ref moverType> ]
     "action" (. tok = t; .)
     { Attribute<ref akv> }
     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);
@@ -1134,15 +1133,19 @@ WhileCmd<out WhileCmd wcmd>
     "invariant"
     { Attribute<ref kv> }
     (
-      Expression<out e> (. if (isFree) {
-                             invariants.Add(new AssumeCmd(z, e, kv));
-                           } else {
-                             invariants.Add(new AssertCmd(z, e, kv));
-                           }
-						   kv = null;
+      Expression<out e> (.
+                          if (isFree) {
+                            invariants.Add(new AssumeCmd(z, e, kv));
+                          } else {
+                            invariants.Add(new AssertCmd(z, e, kv));
+                          }
+						              kv = null;
                         .)
       |
-      CallCmd<out cmd>  (. yields.Add((CallCmd)cmd); .)
+      CallCmd<out cmd>  (.
+                          yields.Add((CallCmd)cmd);
+                          kv = null;
+                        .)
     )
     ";"
   }

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