refactored og and fixed latest bug reported by chris

5 files changed, 334 insertions, 257 deletions

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index c0dd1164..af5fcb61 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -22,18 +22,12 @@ namespace Microsoft.Boogie
         public bool isAtomic;

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

         public bool inParallelCall;

-        public Procedure yieldCheckerProc;

-        public Implementation yieldCheckerImpl;

-        public Procedure dummyAsyncTargetProc;

         public ProcedureInfo()

         {

             containsYield = false;

             isThreadStart = false;

             isAtomic = true;

             inParallelCall = false;

-            yieldCheckerProc = null;

-            yieldCheckerImpl = null;

-            dummyAsyncTargetProc = null;

         }

     }

 

@@ -80,7 +74,6 @@ namespace Microsoft.Boogie
         {

             procNameToInfo[currentImpl.Name].containsYield = true;

             procNameToInfo[currentImpl.Name].isAtomic = false;

-            CreateYieldCheckerProcedure(currentImpl.Proc);

             return base.VisitYieldCmd(node);

         }

         public override Cmd VisitCallCmd(CallCmd node)

@@ -92,13 +85,6 @@ namespace Microsoft.Boogie
             if (node.IsAsync)

             {

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

-                CreateYieldCheckerProcedure(node.Proc);

-                if (procNameToInfo[node.Proc.Name].dummyAsyncTargetProc == null)

-                {

-                    var dummyAsyncTargetName = string.Format("DummyAsyncTarget_{0}", node.Proc.Name);

-                    var dummyAsyncTargetProc = new Procedure(Token.NoToken, dummyAsyncTargetName, node.Proc.TypeParameters, node.Proc.InParams, node.Proc.OutParams, node.Proc.Requires, new IdentifierExprSeq(), new EnsuresSeq());

-                    procNameToInfo[node.Proc.Name].dummyAsyncTargetProc = dummyAsyncTargetProc;

-                }

             }

             if (node.InParallelWith != null)

             {

@@ -110,21 +96,12 @@ namespace Microsoft.Boogie
                         procNameToInfo[iter.Proc.Name] = new ProcedureInfo();

                     }

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

-                    CreateYieldCheckerProcedure(iter.Proc);

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

                     iter = iter.InParallelWith;

                 }

             }

             return base.VisitCallCmd(node);

         }

-        private void CreateYieldCheckerProcedure(Procedure proc)

-        {

-            if (procNameToInfo[proc.Name].yieldCheckerProc != null) return;

-            var yieldCheckerName = string.Format("YieldChecker_{0}", proc.Name);

-            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, proc.TypeParameters, new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

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

-            procNameToInfo[proc.Name].yieldCheckerProc = yieldCheckerProc;

-        }

     }

 

     class AtomicTraverser : StandardVisitor

@@ -169,7 +146,10 @@ namespace Microsoft.Boogie
         IdentifierExprSeq globalMods;

         Hashtable ogOldGlobalMap;

         Program program;

-        Dictionary<string, Procedure> parallelCallDesugarings; 

+        Dictionary<string, Procedure> asyncAndParallelCallDesugarings;

+        List<Procedure> yieldCheckerProcs;

+        List<Implementation> yieldCheckerImpls;

+        Procedure yieldProc;

 

         public OwickiGriesTransform(Program program)

         {

@@ -184,20 +164,18 @@ namespace Microsoft.Boogie
                 ogOldGlobalMap[g] = new IdentifierExpr(Token.NoToken, oldg);

                 globalMods.Add(new IdentifierExpr(Token.NoToken, g));

             }

-            parallelCallDesugarings = new Dictionary<string, Procedure>();

+            asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();

+            yieldCheckerProcs = new List<Procedure>();

+            yieldCheckerImpls = new List<Implementation>();

+            yieldProc = new Procedure(Token.NoToken, "og@yield", new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

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

         }

 

-        private void AddCallsToYieldCheckers(CmdSeq newCmds)

+        private void AddCallToYieldProc(CmdSeq newCmds)

         {

-            foreach (ProcedureInfo info in procNameToInfo.Values)

-            {

-                if (info.yieldCheckerProc != null)

-                {

-                    CallCmd yieldCallCmd = new CallCmd(Token.NoToken, info.yieldCheckerProc.Name, new ExprSeq(), new IdentifierExprSeq());

-                    yieldCallCmd.Proc = info.yieldCheckerProc;

-                    newCmds.Add(yieldCallCmd);

-                }

-            }

+            CallCmd yieldCallCmd = new CallCmd(Token.NoToken, yieldProc.Name, new ExprSeq(), new IdentifierExprSeq());

+            yieldCallCmd.Proc = yieldProc;

+            newCmds.Add(yieldCallCmd);

         }

 

         private void AddUpdatesToOldGlobalVars(CmdSeq newCmds)

@@ -214,7 +192,7 @@ namespace Microsoft.Boogie
 

         private void DesugarYield(CmdSeq cmds, CmdSeq newCmds)

         {

-            AddCallsToYieldCheckers(newCmds);

+            AddCallToYieldProc(newCmds);

 

             newCmds.Add(new HavocCmd(Token.NoToken, globalMods));

 

@@ -246,8 +224,8 @@ namespace Microsoft.Boogie
             {

                 procName = procName + "@" + calleeName;

             }

-            if (parallelCallDesugarings.ContainsKey(procName))

-                return parallelCallDesugarings[procName];

+            if (asyncAndParallelCallDesugarings.ContainsKey(procName))

+                return asyncAndParallelCallDesugarings[procName];

 

             VariableSeq inParams = new VariableSeq();

             VariableSeq outParams = new VariableSeq();

@@ -289,249 +267,342 @@ namespace Microsoft.Boogie
             }

 

             Procedure proc = new Procedure(Token.NoToken, procName, new TypeVariableSeq(), inParams, outParams, requiresSeq, ieSeq, ensuresSeq);

-            parallelCallDesugarings[procName] = proc;

+            asyncAndParallelCallDesugarings[procName] = proc;

             return proc;

         }

 

-        public void Transform()

+        private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, VariableSeq locals, Hashtable map, Hashtable assumeMap, Hashtable ogOldLocalMap)

         {

-            foreach (var decl in program.TopLevelDeclarations)

-            {

-                Implementation impl = decl as Implementation;

-                if (impl == null) continue;

-                ProcedureInfo info = procNameToInfo[impl.Name];

-

-                // Add free requires

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

-                {

-                    Expr freeRequiresExpr = Expr.True;

-                    foreach (Variable g in ogOldGlobalMap.Keys)

-                    {

-                        freeRequiresExpr = Expr.And(freeRequiresExpr, Expr.Eq(new IdentifierExpr(Token.NoToken, g), (IdentifierExpr)ogOldGlobalMap[g]));

-                    }

-                    impl.Proc.Requires.Add(new Requires(true, freeRequiresExpr));

-                }

+            if (yields.Count == 0) return;

 

-                // Create substitution maps

-                Hashtable map = new Hashtable();

-                VariableSeq locals = new VariableSeq();

-                for (int i = 0; i < impl.Proc.InParams.Length; i++)

-                {

-                    Variable inParam = impl.Proc.InParams[i];

-                    var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));

-                    var ie = new IdentifierExpr(Token.NoToken, copy);

-                    locals.Add(copy);

-                    // substitute for both implementation and procedure parameters because yield predicates can be generated

-                    // either by assertions in the implementation or preconditions and postconditions in the procedure

-                    map[impl.InParams[i]] = ie;

-                    map[impl.Proc.InParams[i]] = ie;

-                }

-                for (int i = 0; i < impl.Proc.OutParams.Length; i++)

-                {

-                    Variable outParam = impl.Proc.OutParams[i];

-                    var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type), outParam.Attributes);

-                    var ie = new IdentifierExpr(Token.NoToken, copy);

-                    locals.Add(copy);

-                    // substitute for both implementation and procedure parameters because yield predicates can be generated

-                    // either by assertions in the implementation or preconditions and postconditions in the procedure

-                    map[impl.OutParams[i]] = ie;

-                    map[impl.Proc.OutParams[i]] = ie;

-                }

-                foreach (Variable local in impl.LocVars)

+            ProcedureInfo info = procNameToInfo[decl.Name];

+            Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);

+            Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);

+            Substitution subst = Substituter.SubstitutionFromHashtable(map);

+            List<Block> yieldCheckerBlocks = new List<Block>();

+            StringSeq labels = new StringSeq();

+            BlockSeq labelTargets = new BlockSeq();

+            Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));

+            labels.Add(yieldCheckerBlock.Label);

+            labelTargets.Add(yieldCheckerBlock);

+            yieldCheckerBlocks.Add(yieldCheckerBlock);

+            int yieldCount = 0;

+            foreach (CmdSeq cs in yields)

+            {

+                CmdSeq newCmds = new CmdSeq();

+                foreach (Cmd cmd in cs)

                 {

-                    var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type), local.Attributes);

-                    locals.Add(copy);

-                    map[local] = new IdentifierExpr(Token.NoToken, copy);

+                    PredicateCmd predCmd = (PredicateCmd)cmd;

+                    newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));

                 }

-                Hashtable assumeMap = new Hashtable(map);

-                foreach (var global in ogOldGlobalMap.Keys)

+                foreach (Cmd cmd in cs)

                 {

-                    assumeMap[global] = ogOldGlobalMap[global];

+                    PredicateCmd predCmd = (PredicateCmd)cmd;

+                    var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);

+                    if (predCmd is AssertCmd)

+                        newCmds.Add(new AssertCmd(predCmd.tok, newExpr));

+                    else

+                        newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));

                 }

+                newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));

+                yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));

+                labels.Add(yieldCheckerBlock.Label);

+                labelTargets.Add(yieldCheckerBlock);

+                yieldCheckerBlocks.Add(yieldCheckerBlock);

+            }

+            yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), new GotoCmd(Token.NoToken, labels, labelTargets)));

 

-                Hashtable ogOldLocalMap = new Hashtable();

-                foreach (var g in program.GlobalVariables())

+            // Create the yield checker procedure

+            var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);

+            var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

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

+            yieldCheckerProcs.Add(yieldCheckerProc);

+

+            // Create the yield checker implementation

+            var yieldCheckerImpl = new Implementation(Token.NoToken, yieldCheckerName, decl.TypeParameters, new VariableSeq(), new VariableSeq(), locals, yieldCheckerBlocks);

+            yieldCheckerImpl.Proc = yieldCheckerProc;

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

+            yieldCheckerImpls.Add(yieldCheckerImpl);

+        }

+

+        private void TransformImpl(Implementation impl)

+        {

+            ProcedureInfo info = procNameToInfo[impl.Name];

+

+            // Add free requires

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

+            {

+                Expr freeRequiresExpr = Expr.True;

+                foreach (Variable g in ogOldGlobalMap.Keys)

                 {

-                    var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og@local_old_{0}", g.Name), g.TypedIdent.Type));

-                    locals.Add(copy);

-                    ogOldLocalMap[g] = new IdentifierExpr(Token.NoToken, copy);

+                    freeRequiresExpr = Expr.And(freeRequiresExpr, Expr.Eq(new IdentifierExpr(Token.NoToken, g), (IdentifierExpr)ogOldGlobalMap[g]));

                 }

+                impl.Proc.Requires.Add(new Requires(true, freeRequiresExpr));

+            }

+

+            // Create substitution maps

+            Hashtable map = new Hashtable();

+            VariableSeq locals = new VariableSeq();

+            for (int i = 0; i < impl.Proc.InParams.Length; i++)

+            {

+                Variable inParam = impl.Proc.InParams[i];

+                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));

+                var ie = new IdentifierExpr(Token.NoToken, copy);

+                locals.Add(copy);

+                map[impl.InParams[i]] = ie;

+            }

+            for (int i = 0; i < impl.Proc.OutParams.Length; i++)

+            {

+                Variable outParam = impl.Proc.OutParams[i];

+                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type), outParam.Attributes);

+                var ie = new IdentifierExpr(Token.NoToken, copy);

+                locals.Add(copy);

+                map[impl.OutParams[i]] = ie;

+            }

+            foreach (Variable local in impl.LocVars)

+            {

+                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type), local.Attributes);

+                locals.Add(copy);

+                map[local] = new IdentifierExpr(Token.NoToken, copy);

+            }

+            Hashtable assumeMap = new Hashtable(map);

+            foreach (var global in ogOldGlobalMap.Keys)

+            {

+                assumeMap[global] = ogOldGlobalMap[global];

+            }

 

-                // Collect the yield predicates and desugar yields

-                HashSet<CmdSeq> yields = new HashSet<CmdSeq>();

-                CmdSeq cmds = new CmdSeq();

-                if (info.isThreadStart && impl.Proc.Requires.Length > 0)

+            Hashtable ogOldLocalMap = new Hashtable();

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

+            {

+                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og@local_old_{0}", g.Name), g.TypedIdent.Type));

+                locals.Add(copy);

+                ogOldLocalMap[g] = new IdentifierExpr(Token.NoToken, copy);

+            }

+

+            // Collect the yield predicates and desugar yields

+            List<CmdSeq> yields = new List<CmdSeq>();

+            CmdSeq cmds = new CmdSeq();

+            foreach (Block b in impl.Blocks)

+            {

+                bool insideYield = false;

+                CmdSeq newCmds = new CmdSeq();

+                for (int i = 0; i < b.Cmds.Length; i++)

                 {

-                    foreach (Requires r in impl.Proc.Requires)

+                    Cmd cmd = b.Cmds[i];

+                    if (cmd is YieldCmd)

                     {

-                        if (r.Free) continue;

-                        cmds.Add(new AssertCmd(r.tok, r.Condition));

+                        insideYield = true;

+                        continue;

                     }

-                    yields.Add(cmds);

-                    cmds = new CmdSeq();

-                }

-                if (info.inParallelCall && impl.Proc.Ensures.Length > 0)

-                {

-                    foreach (Ensures e in impl.Proc.Ensures)

+                    if (insideYield)

                     {

-                        if (e.Free) continue;

-                        cmds.Add(new AssertCmd(e.tok, e.Condition));

+                        PredicateCmd pcmd = cmd as PredicateCmd;

+                        if (pcmd == null)

+                        {

+                            DesugarYield(cmds, newCmds);

+                            if (cmds.Length > 0)

+                            {

+                                yields.Add(cmds);

+                                cmds = new CmdSeq();

+                            }

+                            insideYield = false;

+                        }

+                        else

+                        {

+                            cmds.Add(pcmd);

+                        }

                     }

-                    yields.Add(cmds);

-                    cmds = new CmdSeq();

-                }

-                foreach (Block b in impl.Blocks)

-                {

-                    bool insideYield = false;

-                    CmdSeq newCmds = new CmdSeq();

-                    for (int i = 0; i < b.Cmds.Length; i++)

+                    CallCmd callCmd = cmd as CallCmd;

+                    if (callCmd != null)

                     {

-                        Cmd cmd = b.Cmds[i];

-                        if (cmd is YieldCmd)

+                        if (callCmd.InParallelWith != null)

                         {

-                            insideYield = true;

-                            continue;

+                            List<Expr> ins;

+                            List<IdentifierExpr> outs;

+                            Procedure dummyParallelCallDesugaring = DesugarParallelCallCmd(callCmd, out ins, out outs);

+                            CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyParallelCallDesugaring.Name, ins, outs);

+                            dummyCallCmd.Proc = dummyParallelCallDesugaring;

+                            newCmds.Add(dummyCallCmd);

                         }

-                        if (insideYield)

+                        else if (callCmd.IsAsync)

                         {

-                            PredicateCmd pcmd = cmd as PredicateCmd;

-                            if (pcmd == null)

-                            {

-                                DesugarYield(cmds, newCmds);

-                                if (cmds.Length > 0)

-                                {

-                                    yields.Add(cmds);

-                                    cmds = new CmdSeq();

-                                }

-                                insideYield = false;

-                            }

-                            else

+                            if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name))

                             {

-                                cmds.Add(pcmd);

+                                asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new EnsuresSeq());

                             }

+                            var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name];

+                            CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);

+                            dummyCallCmd.Proc = dummyAsyncTargetProc;

+                            newCmds.Add(dummyCallCmd);

                         }

-                        CallCmd callCmd = cmd as CallCmd;

-                        if (callCmd != null)

+                        else if (procNameToInfo[callCmd.callee].isAtomic)

                         {

-                            if (callCmd.InParallelWith != null)

-                            {

-                                List<Expr> ins;

-                                List<IdentifierExpr> outs;

-                                Procedure dummyParallelCallDesugaring = DesugarParallelCallCmd(callCmd, out ins, out outs);

-                                CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyParallelCallDesugaring.Name, ins, outs);

-                                dummyCallCmd.Proc = dummyParallelCallDesugaring;

-                                newCmds.Add(dummyCallCmd);

-                            }

-                            else if (callCmd.IsAsync)

-                            {

-                                var dummyAsyncTargetProc = procNameToInfo[callCmd.callee].dummyAsyncTargetProc;

-                                CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs);

-                                dummyCallCmd.Proc = dummyAsyncTargetProc;

-                                newCmds.Add(dummyCallCmd);

-                            }

-                            else if (procNameToInfo[callCmd.callee].isAtomic)

-                            {

-                                newCmds.Add(callCmd);

-                            }

-                            else

-                            {

-                                AddCallsToYieldCheckers(newCmds);

-                                newCmds.Add(callCmd);

-                                AddUpdatesToOldGlobalVars(newCmds);

-                            }

+                            newCmds.Add(callCmd);

                         }

                         else

                         {

-                            newCmds.Add(cmd);

+                            AddCallToYieldProc(newCmds);

+                            newCmds.Add(callCmd);

+                            AddUpdatesToOldGlobalVars(newCmds);

                         }

                     }

-                    if (insideYield)

+                    else

                     {

-                        DesugarYield(cmds, newCmds);

-                        if (cmds.Length > 0)

-                        {

-                            yields.Add(cmds);

-                            cmds = new CmdSeq();

-                        }

-                    } 

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

+                        newCmds.Add(cmd);

+                    }

+                }

+                if (insideYield)

+                {

+                    DesugarYield(cmds, newCmds);

+                    if (cmds.Length > 0)

                     {

-                        AddCallsToYieldCheckers(newCmds);

+                        yields.Add(cmds);

+                        cmds = new CmdSeq();

                     }

-                    b.Cmds = newCmds;

                 }

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

+                {

+                    AddCallToYieldProc(newCmds);

+                }

+                b.Cmds = newCmds;

+            }

 

-                if (!info.isAtomic)

+            if (!info.isAtomic)

+            {

+                // Loops

+                impl.PruneUnreachableBlocks();

+                impl.ComputePredecessorsForBlocks();

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

+                g.ComputeLoops();

+                if (g.Reducible)

                 {

-                    // Loops

-                    impl.PruneUnreachableBlocks();

-                    impl.ComputePredecessorsForBlocks();

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

-                    g.ComputeLoops();

-                    if (g.Reducible)

+                    foreach (Block header in g.Headers)

                     {

-                        foreach (Block header in g.Headers)

+                        foreach (Block pred in header.Predecessors)

                         {

-                            foreach (Block pred in header.Predecessors)

-                            {

-                                AddCallsToYieldCheckers(pred.Cmds);

-                                AddUpdatesToOldGlobalVars(pred.Cmds);

-                            }

-                            CmdSeq newCmds = new CmdSeq();

-                            foreach (Variable v in ogOldGlobalMap.Keys)

-                            {

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

-                            }

-                            newCmds.AddRange(header.Cmds);

-                            header.Cmds = newCmds;

+                            AddCallToYieldProc(pred.Cmds);

+                            AddUpdatesToOldGlobalVars(pred.Cmds);

                         }

+                        CmdSeq newCmds = new CmdSeq();

+                        foreach (Variable v in ogOldGlobalMap.Keys)

+                        {

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

+                        }

+                        newCmds.AddRange(header.Cmds);

+                        header.Cmds = newCmds;

                     }

                 }

+            }

+            CreateYieldCheckerImpl(impl, yields, locals, map, assumeMap, ogOldLocalMap);

+        }

 

-                if (!info.containsYield && !info.isThreadStart) continue;

+        public void TransformProc(Procedure proc)

+        {

+            ProcedureInfo info = procNameToInfo[proc.Name];

+            if (!info.isThreadStart) return;

 

-                // Create the body of the yield checker procedure

-                Substitution assumeSubst = Substituter.SubstitutionFromHashtable(assumeMap);

-                Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);

-                Substitution subst = Substituter.SubstitutionFromHashtable(map);

-                List<Block> yieldCheckerBlocks = new List<Block>();

-                StringSeq labels = new StringSeq();

-                BlockSeq labelTargets = new BlockSeq();

-                Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));

-                labels.Add(yieldCheckerBlock.Label);

-                labelTargets.Add(yieldCheckerBlock);

-                yieldCheckerBlocks.Add(yieldCheckerBlock);

-                int yieldCount = 0;

-                foreach (CmdSeq cs in yields)

+            // Create substitution maps

+            Hashtable map = new Hashtable();

+            VariableSeq locals = new VariableSeq();

+            for (int i = 0; i < proc.InParams.Length; i++)

+            {

+                Variable inParam = proc.InParams[i];

+                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));

+                var ie = new IdentifierExpr(Token.NoToken, copy);

+                locals.Add(copy);

+                map[proc.InParams[i]] = ie;

+            }

+            for (int i = 0; i < proc.OutParams.Length; i++)

+            {

+                Variable outParam = proc.OutParams[i];

+                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type), outParam.Attributes);

+                var ie = new IdentifierExpr(Token.NoToken, copy);

+                locals.Add(copy);

+                map[proc.OutParams[i]] = ie;

+            }

+            Hashtable assumeMap = new Hashtable(map);

+            foreach (var global in ogOldGlobalMap.Keys)

+            {

+                assumeMap[global] = ogOldGlobalMap[global];

+            }

+

+            Hashtable ogOldLocalMap = new Hashtable();

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

+            {

+                var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og@local_old_{0}", g.Name), g.TypedIdent.Type));

+                locals.Add(copy);

+                ogOldLocalMap[g] = new IdentifierExpr(Token.NoToken, copy);

+            }

+

+            // Collect the yield predicates and desugar yields

+            List<CmdSeq> yields = new List<CmdSeq>();

+            CmdSeq cmds = new CmdSeq();

+            if (proc.Requires.Length > 0)

+            {

+                foreach (Requires r in proc.Requires)

                 {

-                    CmdSeq newCmds = new CmdSeq();

-                    foreach (Cmd cmd in cs)

-                    {

-                        PredicateCmd predCmd = (PredicateCmd)cmd;

-                        newCmds.Add(new AssumeCmd(Token.NoToken, Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr)));

-                    }

-                    foreach (Cmd cmd in cs)

-                    {

-                        PredicateCmd predCmd = (PredicateCmd)cmd;

-                        var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr);

-                        if (predCmd is AssertCmd)

-                            newCmds.Add(new AssertCmd(predCmd.tok, newExpr));

-                        else

-                            newCmds.Add(new AssumeCmd(Token.NoToken, newExpr));

-                    }

-                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False));

-                    yieldCheckerBlock = new Block(Token.NoToken, "L" + yieldCount++, newCmds, new ReturnCmd(Token.NoToken));

-                    labels.Add(yieldCheckerBlock.Label);

-                    labelTargets.Add(yieldCheckerBlock);

-                    yieldCheckerBlocks.Add(yieldCheckerBlock); 

+                    if (r.Free) continue;

+                    cmds.Add(new AssertCmd(r.tok, r.Condition));

+                }

+                yields.Add(cmds);

+                cmds = new CmdSeq();

+            }

+            if (info.inParallelCall && proc.Ensures.Length > 0)

+            {

+                foreach (Ensures e in proc.Ensures)

+                {

+                    if (e.Free) continue;

+                    cmds.Add(new AssertCmd(e.tok, e.Condition));

+                }

+                yields.Add(cmds);

+                cmds = new CmdSeq();

+            }

+            CreateYieldCheckerImpl(proc, yields, locals, map, assumeMap, ogOldLocalMap);

+        }

+

+        private void AddYieldProcAndImpl() 

+        {

+            List<Block> blocks = new List<Block>();

+            TransferCmd transferCmd = new ReturnCmd(Token.NoToken);

+            if (yieldCheckerProcs.Count > 0)

+            {

+                BlockSeq blockTargets = new BlockSeq();

+                StringSeq labelTargets = new StringSeq();

+                int labelCount = 0;

+                foreach (Procedure proc in yieldCheckerProcs)

+                {

+                    CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, new ExprSeq(), new IdentifierExprSeq());

+                    callCmd.Proc = proc;

+                    string label = string.Format("L_{0}", labelCount++);

+                    Block block = new Block(Token.NoToken, label, new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));

+                    labelTargets.Add(label);

+                    blockTargets.Add(block);

+                    blocks.Add(block);

                 }

-                yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), new GotoCmd(Token.NoToken, labels, labelTargets)));

-                

-                // Create the yield checker implementation

-                var yieldCheckerImpl = new Implementation(Token.NoToken, info.yieldCheckerProc.Name, impl.TypeParameters, new VariableSeq(), new VariableSeq(), locals, yieldCheckerBlocks);

-                yieldCheckerImpl.Proc = info.yieldCheckerProc;

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

-                info.yieldCheckerImpl = yieldCheckerImpl;

+                transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets);

+            }

+            blocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), transferCmd));

+            var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new VariableSeq(), blocks);

+            yieldImpl.Proc = yieldProc;

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

+            program.TopLevelDeclarations.Add(yieldProc);

+            program.TopLevelDeclarations.Add(yieldImpl);

+        }

+

+        public void Transform()

+        {

+            foreach (var decl in program.TopLevelDeclarations)

+            {

+                Procedure proc = decl as Procedure;

+                if (proc == null) continue;

+                TransformProc(proc);

+            }

+

+            foreach (var decl in program.TopLevelDeclarations)

+            {

+                Implementation impl = decl as Implementation;

+                if (impl == null) continue;

+                TransformImpl(impl);

             }

 

             foreach (Variable v in ogOldGlobalMap.Keys)

@@ -539,24 +610,19 @@ namespace Microsoft.Boogie
                 IdentifierExpr ie = (IdentifierExpr) ogOldGlobalMap[v];

                 program.TopLevelDeclarations.Add(ie.Decl);

             }

-            foreach (ProcedureInfo info in procNameToInfo.Values)

+            foreach (Procedure proc in yieldCheckerProcs)

             {

-                if (info.yieldCheckerProc != null)

-                {

-                    Debug.Assert(info.yieldCheckerImpl != null);

-                    program.TopLevelDeclarations.Add(info.yieldCheckerProc);

-                    program.TopLevelDeclarations.Add(info.yieldCheckerImpl);

-                }

-                if (info.dummyAsyncTargetProc != null)

-                {

-                    program.TopLevelDeclarations.Add(info.dummyAsyncTargetProc);

-                }

+                program.TopLevelDeclarations.Add(proc);

+            }

+            foreach (Implementation impl in yieldCheckerImpls)

+            {

+                program.TopLevelDeclarations.Add(impl);

             }

-            foreach (Procedure proc in parallelCallDesugarings.Values)

+            foreach (Procedure proc in asyncAndParallelCallDesugarings.Values)

             {

                 program.TopLevelDeclarations.Add(proc);

             }

-

+            AddYieldProcAndImpl();

             Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);

         }

     }

diff --git a/Test/og/Answer b/Test/og/Answer
index 154b0193..5264da4a 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -3,7 +3,7 @@
 foo.bpl(13,3): Error BP5001: This assertion might not hold.

 Execution trace:

     foo.bpl(5,5): anon0

-    (0,0): inline$YieldChecker_PC$0$L1

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

 

 Boogie program verifier finished with 3 verified, 1 error

 

@@ -11,11 +11,11 @@ Boogie program verifier finished with 3 verified, 1 error
 bar.bpl(12,3): Error BP5001: This assertion might not hold.

 Execution trace:

     bar.bpl(5,5): anon0

-    (0,0): inline$YieldChecker_PC$0$L1

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

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

 Execution trace:

     bar.bpl(17,5): anon0

-    (0,0): inline$YieldChecker_PC$0$L1

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

 

 Boogie program verifier finished with 2 verified, 2 errors

 

@@ -27,11 +27,11 @@ Boogie program verifier finished with 2 verified, 0 errors
 parallel1.bpl(9,3): Error BP5001: This assertion might not hold.

 Execution trace:

     parallel1.bpl(5,5): anon0

-    (0,0): inline$YieldChecker_PC$0$L1

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

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

 Execution trace:

     parallel1.bpl(5,5): anon0

-    (0,0): inline$YieldChecker_PC$0$L2

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

 

 Boogie program verifier finished with 3 verified, 2 errors

 

@@ -63,12 +63,18 @@ Boogie program verifier finished with 4 verified, 0 errors
 parallel4.bpl(14,3): Error BP5001: This assertion might not hold.

 Execution trace:

     parallel4.bpl(12,3): anon0

-    (0,0): inline$YieldChecker_t$0$enter

-    (0,0): inline$YieldChecker_t$0$exit

-    parallel4.bpl(12,3): anon0$2

+    parallel4.bpl(12,3): anon0$1

 

 Boogie program verifier finished with 2 verified, 1 error

 

 -------------------- parallel5.bpl --------------------

 

 Boogie program verifier finished with 4 verified, 0 errors

+

+-------------------- parallel6.bpl --------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

+

+-------------------- parallel7.bpl --------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/og/parallel6.bpl b/Test/og/parallel6.bpl
new file mode 100644
index 00000000..dba3eb2b
--- /dev/null
+++ b/Test/og/parallel6.bpl
@@ -0,0 +1,2 @@
+procedure A();

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

diff --git a/Test/og/parallel7.bpl b/Test/og/parallel7.bpl
new file mode 100644
index 00000000..79c92196
--- /dev/null
+++ b/Test/og/parallel7.bpl
@@ -0,0 +1,3 @@
+procedure A();

+procedure B();

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

diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 64c21618..4009b62f 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl parallel3.bpl) do (
   %BGEXE% %* /nologo /noinfer /doModSetAnalysis /OwickiGries:OwickiGriesDesugared.bpl %%f

 )

 

-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl) do (

+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl parallel6.bpl parallel7.bpl) do (

   echo.

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

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