cleaned up the OG code

enabled it to be always on

32 files changed, 358 insertions, 356 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 7b3f6fc5..ef2f8ee0 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2863,12 +2863,15 @@ namespace Microsoft.Boogie {
         v.Typecheck(tc);

       }

       List<IdentifierExpr> oldFrame = tc.Frame;

+      bool oldYields = tc.Yields;

       tc.Frame = Proc.Modifies;

+      tc.Yields = QKeyValue.FindBoolAttribute(Proc.Attributes, "yields");

       foreach (Block b in Blocks) {

         b.Typecheck(tc);

       }

       Contract.Assert(tc.Frame == Proc.Modifies);

       tc.Frame = oldFrame;

+      tc.Yields = oldYields;

     }

     void MatchFormals(List<Variable>/*!*/ implFormals, List<Variable>/*!*/ procFormals, string/*!*/ inout, TypecheckingContext/*!*/ tc) {

       Contract.Requires(implFormals != null);

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 57f48f02..2c5e1d89 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -959,7 +959,7 @@ namespace Microsoft.Boogie {
             }

             else if (!CommandLineOptions.Clo.DoModSetAnalysis && v is GlobalVariable && !tc.InFrame(v))

             {

-                tc.Error(this, "command assigns to a global variable that is not in the enclosing method's modifies clause: {0}", v.Name);

+                tc.Error(this, "command assigns to a global variable that is not in the enclosing procedure's modifies clause: {0}", v.Name);

             }

         }

     }

@@ -1084,7 +1084,10 @@ namespace Microsoft.Boogie {
       }

       public override void Typecheck(TypecheckingContext tc)

       {

-          // nothing to typecheck

+          if (!CommandLineOptions.Clo.DoModSetAnalysis && !tc.Yields)

+          {

+              tc.Error(this, "enclosing procedure of a yield command must yield");

+          }

       }

       public override void AddAssignedVariables(List<Variable> vars)

       {

@@ -1942,7 +1945,8 @@ namespace Microsoft.Boogie {
     }

 

     public override void AddAssignedVariables(List<Variable> vars) {

-      //Contract.Requires(vars != null);

+      if (this.IsAsync)

+          return;

       foreach (IdentifierExpr e in Outs) {

         if (e != null) {

           vars.Add(e.Decl);

@@ -1955,54 +1959,81 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public override void Typecheck(TypecheckingContext tc) {

-      //Contract.Requires(tc != null);

-      Contract.Assume(this.Proc != null);  // we assume the CallCmd has been successfully resolved before calling this Typecheck method

-

-      TypecheckAttributes(Attributes, tc);

-

-      // typecheck in-parameters

-      foreach (Expr e in Ins)

-        if (e != null)

-          e.Typecheck(tc);

-      foreach (Expr e in Outs)

-        if (e != null)

-          e.Typecheck(tc);

-      this.CheckAssignments(tc);

-

-      List<Type>/*!*/ formalInTypes = new List<Type>();

-      List<Type>/*!*/ formalOutTypes = new List<Type>();

-      List<Expr>/*!*/ actualIns = new List<Expr>();

-      List<IdentifierExpr>/*!*/ actualOuts = new List<IdentifierExpr>();

-      for (int i = 0; i < Ins.Count; ++i) {

-        if (Ins[i] != null) {

-          formalInTypes.Add(cce.NonNull(Proc.InParams[i]).TypedIdent.Type);

-          actualIns.Add(Ins[i]);

+    public override void Typecheck(TypecheckingContext tc)

+    {

+        //Contract.Requires(tc != null);

+        Contract.Assume(this.Proc != null);  // we assume the CallCmd has been successfully resolved before calling this Typecheck method

+

+        TypecheckAttributes(Attributes, tc);

+

+        // typecheck in-parameters

+        foreach (Expr e in Ins)

+            if (e != null)

+                e.Typecheck(tc);

+        foreach (Expr e in Outs)

+            if (e != null)

+                e.Typecheck(tc);

+        this.CheckAssignments(tc);

+

+        List<Type>/*!*/ formalInTypes = new List<Type>();

+        List<Type>/*!*/ formalOutTypes = new List<Type>();

+        List<Expr>/*!*/ actualIns = new List<Expr>();

+        List<IdentifierExpr>/*!*/ actualOuts = new List<IdentifierExpr>();

+        for (int i = 0; i < Ins.Count; ++i)

+        {

+            if (Ins[i] != null)

+            {

+                formalInTypes.Add(cce.NonNull(Proc.InParams[i]).TypedIdent.Type);

+                actualIns.Add(Ins[i]);

+            }

         }

-      }

-      for (int i = 0; i < Outs.Count; ++i) {

-        if (Outs[i] != null) {

-          formalOutTypes.Add(cce.NonNull(Proc.OutParams[i]).TypedIdent.Type);

-          actualOuts.Add(Outs[i]);

+        for (int i = 0; i < Outs.Count; ++i)

+        {

+            if (Outs[i] != null)

+            {

+                formalOutTypes.Add(cce.NonNull(Proc.OutParams[i]).TypedIdent.Type);

+                actualOuts.Add(Outs[i]);

+            }

         }

-      }

 

-      // match actuals with formals

-      List<Type/*!*/>/*!*/ actualTypeParams;

-      Type.CheckArgumentTypes(Proc.TypeParameters,

-                              out actualTypeParams,

-                              formalInTypes, actualIns,

-                              formalOutTypes, actualOuts,

-                              this.tok,

-                              "call to " + callee,

-                              tc);

-      Contract.Assert(cce.NonNullElements(actualTypeParams));

-      TypeParameters = SimpleTypeParamInstantiation.From(Proc.TypeParameters,

-                                                         actualTypeParams);

-      if (InParallelWith != null)

-      {

-          InParallelWith.Typecheck(tc);

-      }

+        // match actuals with formals

+        List<Type/*!*/>/*!*/ actualTypeParams;

+        Type.CheckArgumentTypes(Proc.TypeParameters,

+                                out actualTypeParams,

+                                formalInTypes, actualIns,

+                                formalOutTypes, actualOuts,

+                                this.tok,

+                                "call to " + callee,

+                                tc);

+        Contract.Assert(cce.NonNullElements(actualTypeParams));

+        TypeParameters = SimpleTypeParamInstantiation.From(Proc.TypeParameters,

+                                                           actualTypeParams);

+

+        if (!CommandLineOptions.Clo.DoModSetAnalysis && (IsAsync || InParallelWith != null))

+        {

+            if (!tc.Yields)

+            {

+                tc.Error(this, "enclosing procedure of a parallel or async call must yield");

+            }

+            var curr = this;

+            while (curr != null)

+            {

+                if (!QKeyValue.FindBoolAttribute(curr.Proc.Attributes, "yields"))

+                {

+                    tc.Error(curr, "target procedure of a parallel or async call must yield");

+                }

+                if (!QKeyValue.FindBoolAttribute(curr.Proc.Attributes, "stable"))

+                {

+                    tc.Error(curr, "target procedure of a parallel or async call must be stable");

+                }

+                curr = curr.InParallelWith;

+            }

+        }

+

+        if (InParallelWith != null)

+        {

+            InParallelWith.Typecheck(tc);

+        }

     }

 

     private IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ TypeParamSubstitution() {

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 9d20c15e..11927293 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -39,8 +39,9 @@ namespace Microsoft.Boogie {
   }

 

   public class ModSetCollector : StandardVisitor {

-    static Procedure proc;

+    static Procedure enclosingProc;

     static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;

+    static HashSet<Procedure> yieldingProcs;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullDictionaryAndValues(modSets));

@@ -67,6 +68,7 @@ namespace Microsoft.Boogie {
       }

 

       modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();

+      yieldingProcs = new HashSet<Procedure>();

 

       HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();

       foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {

@@ -83,13 +85,13 @@ namespace Microsoft.Boogie {
         {

             if (!implementedProcs.Contains(cce.NonNull((Procedure)decl)))

             {

-                proc = (Procedure)decl;

-                foreach (IdentifierExpr/*!*/ expr in proc.Modifies)

+                enclosingProc = (Procedure)decl;

+                foreach (IdentifierExpr/*!*/ expr in enclosingProc.Modifies)

                 {

                     Contract.Assert(expr != null);

                     ProcessVariable(expr.Decl);

                 }

-                proc = null;

+                enclosingProc = null;

             }

             else

             {

@@ -112,6 +114,10 @@ namespace Microsoft.Boogie {
           {

               x.Modifies.Add(new IdentifierExpr(v.tok, v));

           }

+          if (yieldingProcs.Contains(x) && !QKeyValue.FindBoolAttribute(x.Attributes, "yields"))

+          {

+              x.AddAttribute("yields");

+          }

       }

 

       if (false /*CommandLineOptions.Clo.Trace*/)      {

@@ -139,13 +145,22 @@ namespace Microsoft.Boogie {
     public override Implementation VisitImplementation(Implementation node) {

       //Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Implementation>() != null);

-      proc = node.Proc;

+      enclosingProc = node.Proc;

       Implementation/*!*/ ret = base.VisitImplementation(node);

       Contract.Assert(ret != null);

-      proc = null;

+      enclosingProc = null;

 

       return ret;

     }

+    public override YieldCmd VisitYieldCmd(YieldCmd node)

+    {

+        if (!yieldingProcs.Contains(enclosingProc))

+        {

+            yieldingProcs.Add(enclosingProc);

+            moreProcessingRequired = true;

+        }

+        return base.VisitYieldCmd(node);

+    }

     public override Cmd VisitAssignCmd(AssignCmd assignCmd) {

       //Contract.Requires(assignCmd != null);

       Contract.Ensures(Contract.Result<Cmd>() != null);

@@ -183,10 +198,29 @@ namespace Microsoft.Boogie {
           ProcessVariable(var);

         }

       }

+      if (!yieldingProcs.Contains(enclosingProc) && 

+          (yieldingProcs.Contains(callCmd.Proc) || callCmd.IsAsync || callCmd.InParallelWith != null))

+      {

+          yieldingProcs.Add(enclosingProc);

+          moreProcessingRequired = true;

+      }

+      if (callCmd.IsAsync || callCmd.InParallelWith != null)

+      {

+          var curr = callCmd;

+          while (curr != null)

+          {

+              if (!yieldingProcs.Contains(curr.Proc)) 

+              {

+                  yieldingProcs.Add(curr.Proc);

+                  moreProcessingRequired = true;

+              }

+              curr = curr.InParallelWith;

+          }

+      }

       return ret;

     }

     private static void ProcessVariable(Variable var) {

-      Procedure/*!*/ localProc = cce.NonNull(proc);

+      Procedure/*!*/ localProc = cce.NonNull(enclosingProc);

       if (var == null)

         return;

       if (!(var is GlobalVariable))

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index aaee1ff0..26e7edf9 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -10,139 +10,8 @@ using System.Diagnostics.Contracts;
 

 namespace Microsoft.Boogie

 {

-    class ProcedureInfo

-    {

-        // containsYield is true iff there is an implementation that contains a yield statement

-        public bool containsYield;

-        // isThreadStart is true iff there is an async call to the procedure

-        public bool isThreadStart;

-        // isEntrypoint is true iff the procedure is an entrypoint

-        public bool isEntrypoint;

-        // isAtomic is true if there are no yields transitively in any implementation

-        public bool isAtomic;

-        // inParallelCall is true iff this procedure is involved in some parallel call

-        public bool inParallelCall;

-        public ProcedureInfo()

-        {

-            containsYield = false;

-            isThreadStart = false;

-            isAtomic = true;

-            inParallelCall = false;

-        }

-    }

-    

-    class AsyncAndYieldTraverser : StandardVisitor

-    {

-        Dictionary<string, ProcedureInfo> procNameToInfo = new Dictionary<string, ProcedureInfo>();

-        Implementation currentImpl = null;

-        public static Dictionary<string, ProcedureInfo> Traverse(Program program)

-        {

-            AsyncAndYieldTraverser traverser = new AsyncAndYieldTraverser();

-            traverser.VisitProgram(program);

-            return traverser.procNameToInfo;

-        }

-        public override Procedure VisitProcedure(Procedure node)

-        {

-            if (!procNameToInfo.ContainsKey(node.Name))

-            {

-                procNameToInfo[node.Name] = new ProcedureInfo();

-            }

-            if (QKeyValue.FindBoolAttribute(node.Attributes, "entrypoint"))

-            {

-                procNameToInfo[node.Name].isEntrypoint = true;

-            }

-            if (QKeyValue.FindBoolAttribute(node.Attributes, "yields"))

-            {

-                procNameToInfo[node.Name].isAtomic = false;

-            }

-            return base.VisitProcedure(node);

-        }

-        public override Implementation VisitImplementation(Implementation node)

-        {

-            currentImpl = node;

-            if (!procNameToInfo.ContainsKey(node.Name))

-            {

-                procNameToInfo[node.Name] = new ProcedureInfo();

-            }

-            if (QKeyValue.FindBoolAttribute(node.Attributes, "entrypoint"))

-            {

-                procNameToInfo[node.Name].isEntrypoint = true;

-            }

-            return base.VisitImplementation(node);

-        }

-        public override YieldCmd VisitYieldCmd(YieldCmd node)

-        {

-            procNameToInfo[currentImpl.Name].containsYield = true;

-            procNameToInfo[currentImpl.Name].isAtomic = false;

-            return base.VisitYieldCmd(node);

-        }

-        public override Cmd VisitCallCmd(CallCmd node)

-        {

-            if (!procNameToInfo.ContainsKey(node.Proc.Name))

-            {

-                procNameToInfo[node.Proc.Name] = new ProcedureInfo();

-            }

-            if (node.IsAsync)

-            {

-                procNameToInfo[node.Proc.Name].isThreadStart = true;

-            }

-            if (node.InParallelWith != null)

-            {

-                CallCmd iter = node;

-                while (iter != null)

-                {

-                    if (!procNameToInfo.ContainsKey(iter.Proc.Name))

-                    {

-                        procNameToInfo[iter.Proc.Name] = new ProcedureInfo();

-                    }

-                    procNameToInfo[iter.Proc.Name].isThreadStart = true;

-                    procNameToInfo[iter.Proc.Name].inParallelCall = true;

-                    iter = iter.InParallelWith;

-                }

-            }

-            return base.VisitCallCmd(node);

-        }

-    }

-

-    class AtomicTraverser : StandardVisitor

-    {

-        Implementation currentImpl;

-        static Dictionary<string, ProcedureInfo> procNameToInfo;

-        static bool moreProcessingRequired;

-        public static void Traverse(Program program, Dictionary<string, ProcedureInfo> procNameToInfo)

-        {

-            AtomicTraverser.procNameToInfo = procNameToInfo;

-            do

-            {

-                moreProcessingRequired = false;

-                AtomicTraverser traverser = new AtomicTraverser();

-                traverser.VisitProgram(program);

-            } while (moreProcessingRequired);

-        }

-

-        public override Implementation VisitImplementation(Implementation node)

-        {

-            if (!procNameToInfo[node.Name].isAtomic)

-                return node;

-            currentImpl = node;

-            return base.VisitImplementation(node);

-        }

-

-        public override Cmd VisitCallCmd(CallCmd node)

-        {

-            ProcedureInfo info = procNameToInfo[node.callee];

-            if (node.InParallelWith != null || node.IsAsync || !info.isAtomic)

-            {

-                procNameToInfo[currentImpl.Name].isAtomic = false;

-                moreProcessingRequired = true;

-            }

-            return base.VisitCallCmd(node);

-        }

-    }

-

     public class OwickiGriesTransform

     {

-        Dictionary<string, ProcedureInfo> procNameToInfo;

         List<IdentifierExpr> globalMods;

         LinearTypechecker linearTypechecker;

         Dictionary<string, Procedure> asyncAndParallelCallDesugarings;

@@ -154,8 +23,6 @@ namespace Microsoft.Boogie
         {

             this.linearTypechecker = linearTypechecker;

             Program program = linearTypechecker.program;

-            procNameToInfo = AsyncAndYieldTraverser.Traverse(program);

-            AtomicTraverser.Traverse(program, procNameToInfo);

             globalMods = new List<IdentifierExpr>();

             foreach (Variable g in program.GlobalVariables())

             {

@@ -164,20 +31,7 @@ namespace Microsoft.Boogie
             asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();

             yieldCheckerProcs = new List<Procedure>();

             yieldCheckerImpls = new List<Implementation>();

-            List<Variable> inputs = new List<Variable>();

-            foreach (string domainName in linearTypechecker.linearDomains.Keys)

-            {

-                var domain = linearTypechecker.linearDomains[domainName];

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);

-                inputs.Add(f);

-            }

-            foreach (IdentifierExpr ie in globalMods)

-            {

-                Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);

-                inputs.Add(f);

-            }

-            yieldProc = new Procedure(Token.NoToken, "og_yield", new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

-            yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

+            yieldProc = null;

         }

 

         private void AddCallToYieldProc(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)

@@ -190,7 +44,24 @@ namespace Microsoft.Boogie
             foreach (IdentifierExpr ie in globalMods)

             {

                 exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));

-            } 

+            }

+            if (yieldProc == null)

+            {

+                List<Variable> inputs = new List<Variable>();

+                foreach (string domainName in linearTypechecker.linearDomains.Keys)

+                {

+                    var domain = linearTypechecker.linearDomains[domainName];

+                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);

+                    inputs.Add(f);

+                }

+                foreach (IdentifierExpr ie in globalMods)

+                {

+                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true);

+                    inputs.Add(f);

+                }

+                yieldProc = new Procedure(Token.NoToken, "og_yield", new List<TypeVariable>(), inputs, new List<Variable>(), new List<Requires>(), new List<IdentifierExpr>(), new List<Ensures>());

+                yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

+            }

             CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, exprSeq, new List<IdentifierExpr>());

             yieldCallCmd.Proc = yieldProc;

             newCmds.Add(yieldCallCmd);

@@ -283,7 +154,6 @@ namespace Microsoft.Boogie
             List<Variable> outParams = new List<Variable>();

             List<Requires> requiresSeq = new List<Requires>();

             List<Ensures> ensuresSeq = new List<Ensures>();

-            List<IdentifierExpr> ieSeq = new List<IdentifierExpr>();

             int count = 0;

             while (callCmd != null)

             {

@@ -306,10 +176,6 @@ namespace Microsoft.Boogie
                 {

                     requiresSeq.Add(new Requires(req.Free, Substituter.Apply(subst, req.Condition)));

                 }

-                foreach (IdentifierExpr ie in callCmd.Proc.Modifies)

-                {

-                    ieSeq.Add(ie);

-                }

                 foreach (Ensures ens in callCmd.Proc.Ensures)

                 {

                     ensuresSeq.Add(new Ensures(ens.Free, Substituter.Apply(subst, ens.Condition)));

@@ -318,7 +184,8 @@ namespace Microsoft.Boogie
                 callCmd = callCmd.InParallelWith;

             }

 

-            Procedure proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, ieSeq, ensuresSeq);

+            Procedure proc = new Procedure(Token.NoToken, procName, new List<TypeVariable>(), inParams, outParams, requiresSeq, new List<IdentifierExpr>(), ensuresSeq);

+            proc.AddAttribute("yields");

             asyncAndParallelCallDesugarings[procName] = proc;

             return proc;

         }

@@ -328,7 +195,6 @@ namespace Microsoft.Boogie
             if (yields.Count == 0) return;

 

             Program program = linearTypechecker.program;

-            ProcedureInfo info = procNameToInfo[decl.Name];

             List<Variable> locals = new List<Variable>();

             List<Variable> inputs = new List<Variable>();

             foreach (IdentifierExpr ie in map.Values)

@@ -423,11 +289,58 @@ namespace Microsoft.Boogie
             yieldCheckerImpls.Add(yieldCheckerImpl);

         }

 

+        private bool IsYieldingHeader(GraphUtil.Graph<Block> graph, Block header)

+        {

+            foreach (Block backEdgeNode in graph.BackEdgeNodes(header))

+            {

+                foreach (Block x in graph.NaturalLoops(header, backEdgeNode))

+                {

+                    foreach (Cmd cmd in x.Cmds)

+                    {

+                        if (cmd is YieldCmd)

+                            return true;

+                        CallCmd callCmd = cmd as CallCmd;

+                        if (callCmd == null) continue;

+                        if (callCmd.IsAsync || callCmd.InParallelWith != null || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

+                            return true;

+                    }

+                }

+            }

+            return false;

+        }

+

         private void TransformImpl(Implementation impl)

         {

-            Program program = linearTypechecker.program;

-            ProcedureInfo info = procNameToInfo[impl.Name];

+            if (!QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields")) return;

+

+            // Find the yielding loop headers

+            impl.PruneUnreachableBlocks();

+            impl.ComputePredecessorsForBlocks();

+            GraphUtil.Graph<Block> graph = Program.GraphFromImpl(impl);

+            graph.ComputeLoops();

+            if (!graph.Reducible)

+            {

+                throw new Exception("Irreducible flow graphs are unsupported.");

+            }

+            HashSet<Block> yieldingHeaders = new HashSet<Block>();

+            IEnumerable<Block> sortedHeaders = graph.SortHeadersByDominance();

+            foreach (Block header in sortedHeaders)

+            {

+                if (yieldingHeaders.Any(x => graph.DominatorMap.DominatedBy(x, header)))

+                {

+                    yieldingHeaders.Add(header);

+                }

+                else if (IsYieldingHeader(graph, header))

+                {

+                    yieldingHeaders.Add(header);

+                }

+                else

+                {

+                    continue;

+                }

+            }

 

+            Program program = linearTypechecker.program;

             Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

             foreach (Variable local in impl.LocVars)

             {

@@ -493,7 +406,8 @@ namespace Microsoft.Boogie
                     CallCmd callCmd = cmd as CallCmd;

                     if (callCmd != null)

                     {

-                        if (callCmd.InParallelWith != null || callCmd.IsAsync || !procNameToInfo[callCmd.callee].isAtomic)

+                        if (callCmd.InParallelWith != null || callCmd.IsAsync ||

+                            QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

                         {

                             AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

                         }

@@ -521,7 +435,8 @@ namespace Microsoft.Boogie
                         {

                             newCmds.Add(callCmd);

                         }

-                        if (callCmd.InParallelWith != null || callCmd.IsAsync || !procNameToInfo[callCmd.callee].isAtomic)

+                        if (callCmd.InParallelWith != null || callCmd.IsAsync ||

+                            QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

                         {

                             HashSet<Variable> availableLocalLinearVars = new HashSet<Variable>(linearTypechecker.availableLocalLinearVars[callCmd]);

                             foreach (IdentifierExpr ie in callCmd.Outs)

@@ -547,46 +462,34 @@ namespace Microsoft.Boogie
                         cmds = new List<Cmd>();

                     }

                 }

-                if (b.TransferCmd is ReturnCmd && (!info.isAtomic || info.isEntrypoint || info.isThreadStart))

+                if (b.TransferCmd is ReturnCmd && QKeyValue.FindBoolAttribute(impl.Proc.Attributes, "yields"))

                 {

                     AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

                 }

                 b.Cmds = newCmds;

             }

 

-            if (!info.isAtomic)

+            foreach (Block header in yieldingHeaders)

             {

-                // Loops

-                impl.PruneUnreachableBlocks();

-                impl.ComputePredecessorsForBlocks();

-                GraphUtil.Graph<Block> g = Program.GraphFromImpl(impl);

-                g.ComputeLoops();

-                if (g.Reducible)

+                Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[header], domainNameToInputVar);

+                foreach (Block pred in header.Predecessors)

                 {

-                    foreach (Block header in g.Headers)

-                    {

-                        Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[header], domainNameToInputVar);

-                        foreach (Block pred in header.Predecessors)

-                        {

-                            AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);

-                            AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

-                        }

-                        List<Cmd> newCmds = new List<Cmd>();

-                        foreach (string domainName in linearTypechecker.linearDomains.Keys)

-                        {

-                            newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));

-                        }

-                        foreach (Variable v in ogOldGlobalMap.Keys)

-                        {

-                            newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, new IdentifierExpr(Token.NoToken, v), Expr.Ident(ogOldGlobalMap[v]))));

-                        } 

-                        newCmds.AddRange(header.Cmds);

-                        header.Cmds = newCmds;

-                    }

+                    AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);

+                    AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

+                }

+                List<Cmd> newCmds = new List<Cmd>();

+                foreach (string domainName in linearTypechecker.linearDomains.Keys)

+                {

+                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));

                 }

+                foreach (Variable v in ogOldGlobalMap.Keys)

+                {

+                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, new IdentifierExpr(Token.NoToken, v), Expr.Ident(ogOldGlobalMap[v]))));

+                }

+                newCmds.AddRange(header.Cmds);

+                header.Cmds = newCmds;

             }

 

-            if (!info.isAtomic || info.isEntrypoint || info.isThreadStart)

             {

                 // Add initial block

                 List<AssignLhs> lhss = new List<AssignLhs>();

@@ -614,7 +517,7 @@ namespace Microsoft.Boogie
                 {

                     lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));

                     rhss.Add(Expr.Ident(g));

-                } 

+                }

                 if (lhss.Count > 0)

                 {

                     Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] }));

@@ -627,10 +530,9 @@ namespace Microsoft.Boogie
 

         public void TransformProc(Procedure proc)

         {

-            Program program = linearTypechecker.program;

-            ProcedureInfo info = procNameToInfo[proc.Name];

-            if (!info.isThreadStart) return;

+            if (!QKeyValue.FindBoolAttribute(proc.Attributes, "stable")) return;

 

+            Program program = linearTypechecker.program;

             Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();

             {

                 int i = proc.InParams.Count - linearTypechecker.linearDomains.Count;

@@ -684,7 +586,7 @@ namespace Microsoft.Boogie
                 yields.Add(cmds);

                 cmds = new List<Cmd>();

             }

-            if (info.inParallelCall && proc.Ensures.Count > 0)

+            if (proc.Ensures.Count > 0)

             {

                 Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

                 foreach (var domainName in linearTypechecker.linearDomains.Keys)

@@ -728,6 +630,8 @@ namespace Microsoft.Boogie
 

         private void AddYieldProcAndImpl() 

         {

+            if (yieldProc == null) return;

+

             Program program = linearTypechecker.program;

             List<Variable> inputs = new List<Variable>();

             foreach (string domainName in linearTypechecker.linearDomains.Keys)

@@ -804,7 +708,18 @@ namespace Microsoft.Boogie
                 program.TopLevelDeclarations.Add(proc);

             }

             AddYieldProcAndImpl();

-            Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);

+            foreach (var decl in program.TopLevelDeclarations)

+            {

+                Procedure proc = decl as Procedure;

+                if (proc == null) continue;

+                if (QKeyValue.FindBoolAttribute(proc.Attributes, "yields"))

+                {

+                    foreach (GlobalVariable g in program.GlobalVariables())

+                    {

+                        proc.Modifies.Add(new IdentifierExpr(Token.NoToken, g));

+                    }

+                }

+            }

         }

     }

 }

diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 71471413..b86e0a54 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -558,6 +558,7 @@ namespace Microsoft.Boogie {
 

   public class TypecheckingContext : CheckingContext {

     public List<IdentifierExpr> Frame;  // used in checking the assignment targets of implementation bodies

+    public bool Yields;

 

     public TypecheckingContext(IErrorSink errorSink)

       : base(errorSink) {

@@ -566,7 +567,7 @@ namespace Microsoft.Boogie {
     public bool InFrame(Variable v) {

       Contract.Requires(v != null);

       Contract.Requires(Frame != null);

-      return Frame.Any(f => f.Decl == v);

+      return Frame.Any(f => f.Decl == v) || Yields;

     }

   }

 }

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index f81150b1..c6afa0af 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -443,16 +443,18 @@ namespace Microsoft.Boogie
           }

         }

 

-        if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)

         {

           OwickiGriesTransform ogTransform = new OwickiGriesTransform(linearTypechecker);

           ogTransform.Transform();

           var eraser = new LinearEraser();

           eraser.VisitProgram(program);

-          int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;

-          CommandLineOptions.Clo.PrintUnstructured = 1;

-          PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false);

-          CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

+          if (CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile != null)

+          {

+              int oldPrintUnstructured = CommandLineOptions.Clo.PrintUnstructured;

+              CommandLineOptions.Clo.PrintUnstructured = 1;

+              PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false);

+              CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

+          }

         }

 

         EliminateDeadVariablesAndInline(program);

diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index ebd3d07d..973a1c88 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -20,7 +20,7 @@ procedure C()
 

 function f(X): X;

 

-procedure D()

+procedure {:yields} D()

 {

     var {:linear "D"} a: X;

     var {:linear "D"} x: X;

@@ -66,7 +66,7 @@ procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X,
     c := a;

 }

 

-procedure F({:linear "D"} a: X) returns ({:linear "D"} c: X);

+procedure {:yields} {:stable} F({:linear "D"} a: X) returns ({:linear "D"} c: X);

 

 var{:linear "x"} g:int;

 

@@ -81,22 +81,22 @@ modifies g;
   g := r;

 }

 

-procedure I({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} {:stable} I({:linear ""} x:int) returns({:linear ""} x':int)

 {

   x' := x;

 }

 

-procedure J()

+procedure {:yields} {:stable} J()

 {

 }

 

-procedure P1({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} P1({:linear ""} x:int) returns({:linear ""} x':int)

 {

   call x' := I(x) | J();

   call x' := I(x');

 }

 

-procedure P2({:linear ""} x:int) returns({:linear ""} x':int)

+procedure {:yields} P2({:linear ""} x:int) returns({:linear ""} x':int)

 {

   call x' := I(x);

   call x' := I(x') | J();

diff --git a/Test/og/Answer b/Test/og/Answer
index d663de9a..1d516066 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -1,36 +1,36 @@
 

 -------------------- foo.bpl --------------------

-foo.bpl(13,3): Error BP5001: This assertion might not hold.

+foo.bpl(14,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    foo.bpl(5,5): anon0

+    foo.bpl(6,5): anon0

     (0,0): inline$Impl_YieldChecker_PC$0$L0

 

-Boogie program verifier finished with 3 verified, 1 error

+Boogie program verifier finished with 4 verified, 1 error

 

 -------------------- bar.bpl --------------------

-bar.bpl(12,3): Error BP5001: This assertion might not hold.

+bar.bpl(13,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar.bpl(5,5): anon0

+    bar.bpl(6,5): anon0

     (0,0): inline$Impl_YieldChecker_PC$0$L0

-bar.bpl(12,3): Error BP5001: This assertion might not hold.

+bar.bpl(13,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    bar.bpl(17,5): anon0

+    bar.bpl(23,5): anon0

     (0,0): inline$Impl_YieldChecker_PC$0$L0

 

-Boogie program verifier finished with 2 verified, 2 errors

+Boogie program verifier finished with 3 verified, 2 errors

 

 -------------------- one.bpl --------------------

 

 Boogie program verifier finished with 2 verified, 0 errors

 

 -------------------- parallel1.bpl --------------------

-parallel1.bpl(9,3): Error BP5001: This assertion might not hold.

+parallel1.bpl(10,1): Error BP5001: This assertion might not hold.

 Execution trace:

-    parallel1.bpl(5,5): anon0

+    parallel1.bpl(6,5): anon0

     (0,0): inline$Proc_YieldChecker_PC$0$L0

-parallel1.bpl(13,3): Error BP5001: This assertion might not hold.

+parallel1.bpl(14,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    parallel1.bpl(5,5): anon0

+    parallel1.bpl(6,5): anon0

     (0,0): inline$Impl_YieldChecker_PC$0$L0

 

 Boogie program verifier finished with 3 verified, 2 errors

@@ -100,10 +100,10 @@ Boogie program verifier finished with 2 verified, 0 errors
 Boogie program verifier finished with 2 verified, 0 errors

 

 -------------------- async.bpl --------------------

-async.bpl(13,1): Error BP5001: This assertion might not hold.

+async.bpl(14,1): Error BP5001: This assertion might not hold.

 Execution trace:

-    async.bpl(6,3): anon0

-    async.bpl(6,3): anon0$1

+    async.bpl(7,3): anon0

+    async.bpl(7,3): anon0$1

     (0,0): inline$Proc_YieldChecker_P$1$L0

 

 Boogie program verifier finished with 1 verified, 1 error

diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index d231e17c..32fb25b7 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -5,7 +5,7 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     currsize <= newsize && (ghostLock == nil <==> currsize == newsize)

 }

 

-procedure YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} YieldToReadCache({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

 requires tid' != nil;

 requires Inv(ghostLock, currsize, newsize);

 ensures Inv(ghostLock, currsize, newsize);

@@ -19,7 +19,7 @@ ensures tid == tid';
     assert tid != nil;

 }

 

-procedure YieldToUpdateCache({:linear "tid"} tid': X, i: int) returns ({:linear "tid"} tid: X)

+procedure {:yields} YieldToUpdateCache({:linear "tid"} tid': X, i: int) returns ({:linear "tid"} tid: X)

 requires tid' != nil;

 requires Inv(ghostLock, currsize, newsize);

 requires ghostLock == tid';

@@ -56,7 +56,7 @@ modifies lock;
 requires lock == tid;

 ensures lock == nil;

 

-procedure Read ({:linear "tid"} tid': X, start : int, size : int) returns (bytesread : int)

+procedure {:yields} Read ({:linear "tid"} tid': X, start : int, size : int) returns (bytesread : int)

 requires tid' != nil;

 requires 0 <= start && 0 <= size;

 requires Inv(ghostLock, currsize, newsize);

@@ -120,7 +120,7 @@ COPY_TO_BUFFER:
     }

 }

 

-procedure thread({:linear "tid"} tid': X)

+procedure {:yields} {:stable} thread({:linear "tid"} tid': X)

 requires tid' != nil;

 requires Inv(ghostLock, currsize, newsize);

 {

@@ -133,7 +133,7 @@ requires Inv(ghostLock, currsize, newsize);
     call bytesread := Read(tid, start, size);

 }

 

-procedure {:entrypoint} main()

+procedure {:entrypoint} {:yields} main()

 requires currsize == 0 && newsize == 0 && ghostLock == nil && lock == nil;

 {

     var {:linear "tid"} tid: X;

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 434d1f14..5985b6d6 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -7,7 +7,7 @@ var x: int;
 procedure Allocate() returns ({:linear "tid"} xls: X);

 ensures xls != nil;

 

-procedure {:entrypoint} main()

+procedure {:entrypoint} {:yields} main()

 {

     var {:linear "tid"} tid: X;

     var val: int;

@@ -20,7 +20,7 @@ procedure {:entrypoint} main()
     }

 }

 

-procedure foo({:linear "tid"} tid': X, val: int)

+procedure {:yields} {:stable} foo({:linear "tid"} tid': X, val: int)

 requires tid' != nil;

 {

     var {:linear "tid"} tid: X;

@@ -36,7 +36,7 @@ requires tid' != nil;
     l := nil;

 }

 

-procedure Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

+procedure {:yields} Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)

 requires tid' != nil;

 ensures tid == tid';

 ensures old(l) == tid ==> old(l) == l && old(x) == x;

diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index f8c32022..eaa820b9 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -12,7 +12,7 @@ ensures xls == mapconstbool(true);
 var g: int;

 var h: int;

 

-procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -40,7 +40,7 @@ procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
     async call C(tid_child, y);

 }

 

-procedure B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

+procedure {:yields} {:stable} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

 requires x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

@@ -55,7 +55,7 @@ requires x_in != mapconstbool(false);
     g := 2;

 }

 

-procedure C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

+procedure {:yields} {:stable} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

 requires y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

diff --git a/Test/og/async.bpl b/Test/og/async.bpl
index 15f89bae..32f609bc 100644
--- a/Test/og/async.bpl
+++ b/Test/og/async.bpl
@@ -1,7 +1,8 @@
 var x: int;

 var y: int;

 

-procedure {:entrypoint} foo() 

+procedure {:entrypoint} {:yields} foo()

+modifies x, y; 

 {

   assume x == y;

   x := x + 1;

@@ -9,7 +10,7 @@ procedure {:entrypoint} foo()
   y := y + 1;

 }

 

-procedure P()

+procedure {:yields} {:stable} P()

 requires x != y;

 {

   assert x != y;

diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index 8c4586d3..920fc32c 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -1,30 +1,36 @@
 var g:int;

 

-procedure PB()

+procedure {:yields} {:stable} PB()

+modifies g;

 {

   g := g + 1;

 }

 

-procedure PC()

-  ensures g == old(g);

+procedure {:yields} PC()

+ensures g == old(g);

 {

   yield;

   assert g == old(g);

 }

 

-procedure PD()

+procedure {:yields} {:stable} PE()

+{

+  call PC();

+}

+

+procedure {:yields} {:stable} PD()

 {

   g := 3;

   call PC();

   assert g == 3;

 }

 

-procedure{:entrypoint} Main2()

+procedure{:entrypoint} {:yields} Main2()

 {

-  while (true)

+  while (*)

   {

     async call PB();

-    async call PC();

+    async call PE();

     async call PD();

   }

 }

diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index 776a165d..831d2b97 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -1,31 +1,37 @@
 var g:int;

 

-procedure PB()

+procedure {:yields} {:stable} PB()

+modifies g;

 {

   g := g + 1;

 }

 

-procedure PC()

-  ensures g == 3;

+procedure {:yields} PC()

+ensures g == 3;

 {

   g := 3;

   yield;

   assert g == 3;

 }

 

-procedure PD()

+procedure {:yields} {:stable} PE()

+{

+  call PC();

+}

+

+procedure {:yields} {:stable} PD()

 {

   call PC();

   assert g == 3;

   yield;

 }

 

-procedure{:entrypoint} Main()

+procedure {:entrypoint} {:yields} Main()

 {

-  while (true)

+  while (*)

   {

     async call PB();

-    async call PC();

+    async call PE();

     async call PD();

   }

 }

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index c2f792ef..96aca741 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -21,7 +21,7 @@ ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
 

 procedure Allocate() returns ({:linear "tid"} xls: [X]bool);

 

-procedure {:entrypoint} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool) 

+procedure {:entrypoint} {:yields} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool) 

 requires tidls' != None() && xls' == All();

 {

     var {:linear "tid"} tidls: [X]bool;

@@ -46,7 +46,7 @@ requires tidls' != None() && xls' == All();
     async call thread(lsChild, xls2);

 }

 

-procedure thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)

+procedure {:yields} {:stable} thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)

 requires tidls' != None() && xls' != None();

 {

     var {:linear "x"} xls: [X]bool;

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index ac4a2e21..565cc82b 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -23,7 +23,7 @@ ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
 procedure Allocate() returns ({:linear "tid"} xls: X);

 ensures xls != nil;

 

-procedure {:entrypoint} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool) 

+procedure {:entrypoint}  {:yields} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool) 

 requires tidls' != nil && xls' == All();

 {

     var {:linear "tid"} tidls: X;

@@ -46,7 +46,7 @@ requires tidls' != nil && xls' == All();
     async call thread(lsChild, xls2);

 }

 

-procedure thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)

+procedure {:yields} {:stable} thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)

 requires tidls' != nil && xls' != None();

 {

     var {:linear "x"} xls: [X]bool;

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 472e64c6..6ebb9cf1 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -9,7 +9,7 @@ modifies Permissions;
 requires Permissions == mapconstbool(true);

 ensures xls == mapconstbool(true) && Permissions == mapconstbool(false);

 

-procedure PB({:linear "Perm"} permVar_in:[int]bool)

+procedure {:yields} {:stable} PB({:linear "Perm"} permVar_in:[int]bool)

 requires permVar_in[0] && g == 0;

 {

   var {:linear "Perm"} permVar_out: [int]bool;

@@ -26,7 +26,8 @@ requires permVar_in[0] && g == 0;
   assert g == 1;

 }

 

-procedure{:entrypoint} Main()

+procedure{:entrypoint} {:yields} Main()

+modifies g, Permissions;

 requires Permissions == mapconstbool(true);

 {

   var {:linear "Perm"} permVar_out: [int]bool;

diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 806a4178..2a63d60d 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,11 +1,12 @@
 var x:int;

 

 procedure A()

+modifies x;

 {

   x := x;

 }

 

-procedure B()

+procedure {:yields} B()

 {

   x := 5;

   yield;

diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index cb3502b4..ecddc9fc 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -1,26 +1,27 @@
 var g:int;

 

-procedure PB()

+procedure {:yields} {:stable} PB()

+modifies g;

 {

   g := g + 1;

 }

 

-procedure PC()

-  ensures g == 3;

+procedure {:yields} {:stable} PC()

+ensures g == 3;

 {

   g := 3;

   yield;

   assert g == 3;

 }

 

-procedure PD()

+procedure {:yields} {:stable} PD()

 {

   call PC();

   assert g == 3;

   yield;

 }

 

-procedure{:entrypoint} Main()

+procedure {:entrypoint} {:yields} Main()

 {

   while (true)

   {

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 116612cb..b963fe72 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -2,7 +2,7 @@ var a:[int]int;
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

-procedure {:entrypoint} main() 

+procedure {:entrypoint} {:yields} main() 

 {

     var {:linear "tid"} i: int;

     var {:linear "tid"} j: int;

@@ -12,7 +12,7 @@ procedure {:entrypoint} main()
     call i := u(i) | j := u(j);

 }

 

-procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

     i := i';

 

@@ -21,7 +21,7 @@ procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
     assert a[i] == 42;

 }

 

-procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

+procedure {:yields} {:stable} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

 {

     i := i';

 

@@ -30,7 +30,7 @@ procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
     assert a[i] == 42;

 }

 

-procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 ensures i == i';

 ensures old(a)[i] == a[i];

 {

diff --git a/Test/og/parallel3.bpl b/Test/og/parallel3.bpl
index a99a5eb8..f34efc6d 100644
--- a/Test/og/parallel3.bpl
+++ b/Test/og/parallel3.bpl
@@ -1,7 +1,7 @@
-procedure {:entrypoint} main() 

+procedure {:entrypoint} {:yields} main() 

 {

     call A() | B();

 }

 

-procedure A() {}

-procedure B() {}

+procedure {:yields} {:stable} A() {}

+procedure {:yields} {:stable} B() {}

diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index 8f78fdc5..c07975ca 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -2,7 +2,7 @@ var a:int;
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

-procedure {:entrypoint} main() 

+procedure {:entrypoint} {:yields} main() 

 {

   var {:linear "tid"} i: int;

   var {:linear "tid"} j: int;

@@ -11,7 +11,7 @@ procedure {:entrypoint} main()
   call i := t(i) | j := t(j);

 }

 

-procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

   i := i';

   call Yield();

@@ -19,7 +19,7 @@ procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
   a := a + 1;

 }

 

-procedure Yield()

+procedure {:yields} Yield()

 {

   yield;

 }

diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index c583cb3c..eda8ef44 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -2,7 +2,7 @@ var a:[int]int;
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

-procedure {:entrypoint} main() 

+procedure {:entrypoint} {:yields} main() 

 {

     var {:linear "tid"} i: int;

     var {:linear "tid"} j: int;

@@ -12,7 +12,7 @@ procedure {:entrypoint} main()
     call i := u(i) | j := u(j);

 }

 

-procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:stable} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 {

     i := i';

 

@@ -21,7 +21,7 @@ procedure t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
     assert a[i] == 42;

 }

 

-procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

+procedure {:yields} {:stable} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int) 

 {

     i := i';

 

@@ -30,7 +30,7 @@ procedure u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
     assert a[i] == 42;

 }

 

-procedure Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

+procedure {:yields} {:stable} Yield({:linear "tid"} i': int) returns ({:linear "tid"} i: int)

 ensures i == i';

 ensures old(a)[i] == a[i];

 {

diff --git a/Test/og/parallel6.bpl b/Test/og/parallel6.bpl
index dba3eb2b..32f6e4bf 100644
--- a/Test/og/parallel6.bpl
+++ b/Test/og/parallel6.bpl
@@ -1,2 +1,2 @@
-procedure A();

-procedure C() { async call A(); }

+procedure {:yields} {:stable} A();

+procedure {:yields} C() { async call A(); }

diff --git a/Test/og/parallel7.bpl b/Test/og/parallel7.bpl
index 79c92196..7a4018df 100644
--- a/Test/og/parallel7.bpl
+++ b/Test/og/parallel7.bpl
@@ -1,3 +1,3 @@
-procedure A();

-procedure B();

-procedure C() { call A() | B(); }

+procedure {:yields} {:stable} A();

+procedure {:yields} {:stable} B();

+procedure {:yields} C() { call A() | B(); }

diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index 78889868..ad4123f9 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -7,7 +7,7 @@ procedure Split({:linear "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1:
   ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);

 

 

-procedure {:entrypoint} mainE({:linear "Perm"} permVar_in: [int]bool)

+procedure {:entrypoint} {:yields} mainE({:linear "Perm"} permVar_in: [int]bool)

    free requires permVar_in == ch_mapconstbool(true);

    free requires permVar_in[0];

   modifies x;

@@ -28,7 +28,7 @@ procedure {:entrypoint} mainE({:linear "Perm"} permVar_in: [int]bool)
     async call foo(permVarOut2);

 }

 

-procedure foo({:linear "Perm"} permVar_in: [int]bool) 

+procedure {:yields} {:stable} foo({:linear "Perm"} permVar_in: [int]bool) 

   free requires permVar_in != ch_mapconstbool(false);

   free requires permVar_in[1];

   requires x == 0;

diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 5915a206..1325e476 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -6,12 +6,12 @@ set BGEXE=..\..\Binaries\Boogie.exe
 for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do (

   echo.

   echo -------------------- %%f --------------------

-  %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f

+  %BGEXE% %* /nologo /noinfer %%f

 )

 

 for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl) do (

   echo.

   echo -------------------- %%f --------------------

-  %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f

+  %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f

 )

 

diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 28ae5b89..84ed3a35 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -12,7 +12,7 @@ ensures xls == mapconstbool(true);
 var g: int;

 var h: int;

 

-procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

 {

     var {:linear "1"} x: [int]bool;

     var {:linear "2"} y: [int]bool;

@@ -45,7 +45,7 @@ procedure A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
     async call C(tid_child, y);

 }

 

-procedure B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

+procedure {:yields} {:stable} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool) 

 requires x_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

@@ -56,7 +56,7 @@ requires x_in != mapconstbool(false);
     g := 1;

 }

 

-procedure C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

+procedure {:yields} {:stable} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool) 

 requires y_in != mapconstbool(false);

 {

     var {:linear "tid"} tid_out: int;

diff --git a/Test/test0/Answer b/Test/test0/Answer
index 8c7ce4c7..f92dd1dc 100644
--- a/Test/test0/Answer
+++ b/Test/test0/Answer
@@ -123,8 +123,8 @@ axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x
 Boogie program verifier finished with 0 verified, 0 errors

 

 Boogie program verifier finished with 0 verified, 0 errors

-Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q

-Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q

+Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q

+Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q

 2 type checking errors detected in Arrays1.bpl

 Types0.bpl(6,18): error: expected identifier before ':'

 Types0.bpl(6,12): error: expecting an identifier as parameter name

diff --git a/Test/test1/Answer b/Test/test1/Answer
index 70b7ea80..e1a36ad9 100644
--- a/Test/test1/Answer
+++ b/Test/test1/Answer
@@ -1,20 +1,20 @@
 Frame0.bpl(10,11): Error: undeclared identifier: a

 Frame0.bpl(12,11): Error: undeclared identifier: b

 2 name resolution errors detected in Frame0.bpl

-Frame1.bpl(16,7): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

+Frame1.bpl(16,7): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1

 Frame1.bpl(17,6): Error: command assigns to an immutable variable: a

-Frame1.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

+Frame1.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1

 Frame1.bpl(23,4): Error: command assigns to an immutable variable: a

 Frame1.bpl(27,12): Error: command assigns to an immutable variable: hh

-Frame1.bpl(28,12): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(28,12): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

 Frame1.bpl(30,7): Error: command assigns to an immutable variable: hh

-Frame1.bpl(31,7): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(31,7): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

 Frame1.bpl(33,4): Error: command assigns to an immutable variable: hh

-Frame1.bpl(34,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

-Frame1.bpl(55,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g0

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g0

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

-Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(34,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

+Frame1.bpl(55,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g0

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g0

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: g1

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: h0

 Frame1.bpl(84,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x

 Frame1.bpl(89,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x (named y in implementation)

 16 type checking errors detected in Frame1.bpl

@@ -107,7 +107,7 @@ UpdateExprTyping.bpl(36,28): Error: right-hand side in map store with wrong type
 UpdateExprTyping.bpl(38,27): Error: right-hand side in map store with wrong type: ref (expected: int)

 UpdateExprTyping.bpl(39,27): Error: right-hand side in map store with wrong type: int (expected: ref)

 12 type checking errors detected in UpdateExprTyping.bpl

-MapsTypeErrors.bpl(26,6): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: m

+MapsTypeErrors.bpl(26,6): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: m

 MapsTypeErrors.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to []int)

 MapsTypeErrors.bpl(33,3): Error: mismatched types in assignment command (cannot assign []int to int)

 MapsTypeErrors.bpl(39,3): Error: mismatched types in assignment command (cannot assign bool to int)

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 7f20ab7a..502d7db5 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -121,11 +121,11 @@ Execution trace:
     CaptureState.bpl(24,5): anon3

 *** MODEL

 $mv_state_const -> 6

-%lbl%@293 -> false

+%lbl%@294 -> false

 %lbl%+112 -> true

 %lbl%+114 -> true

 %lbl%+118 -> true

-%lbl%+148 -> true

+%lbl%+149 -> true

 boolType -> T@T!val!2

 F -> T@U!val!2

 FieldNameType -> T@T!val!4

diff --git a/Test/test20/Answer b/Test/test20/Answer
index 5e4481ca..4127471b 100644
--- a/Test/test20/Answer
+++ b/Test/test20/Answer
@@ -177,7 +177,7 @@ ProcParamReordering.bpl(15,15): Error: mismatched number of type parameters in p
 2 type checking errors detected in ProcParamReordering.bpl

 ParallelAssignment.bpl(17,2): Error: mismatched types in assignment command (cannot assign bool to int)

 ParallelAssignment.bpl(18,4): Error: invalid type for argument 0 in map assignment: bool (expected: int)

-ParallelAssignment.bpl(20,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: z

+ParallelAssignment.bpl(20,4): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: z

 3 type checking errors detected in ParallelAssignment.bpl

 ParallelAssignment2.bpl(9,7): Error: number of left-hand sides does not match number of right-hand sides

 ParallelAssignment2.bpl(10,9): Error: variable a is assigned more than once in parallel assignment