From 6a95ade5ac61a0c08e4370c8af8141e03f30a470 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sun, 20 Jul 2014 03:48:26 -0700
Subject: added support for facoring out calls to yield checkers; this will
 help avoid quadratic space complexity

---
 Source/Concurrency/OwickiGries.cs | 88 ++++++++++++++++++++++++++++-----------
 1 file changed, 64 insertions(+), 24 deletions(-)

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 1147760f..036d2543 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -312,38 +312,44 @@ namespace Microsoft.Boogie
             return linearTypeChecker.AvailableLinearVars(absyMap[absy]);
         }
 
-        private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
+        private CallCmd CallToYieldProc(IToken tok, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
         {
-            if (!CommandLineOptions.Clo.TrustNonInterference)
+            List<Expr> exprSeq = new List<Expr>();
+            foreach (string domainName in linearTypeChecker.linearDomains.Keys)
+            {
+                exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
+            }
+            foreach (IdentifierExpr ie in globalMods)
+            {
+                exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));
+            }
+            if (yieldProc == null)
             {
-                List<Expr> exprSeq = new List<Expr>();
+                List<Variable> inputs = new List<Variable>();
                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)
                 {
-                    exprSeq.Add(Expr.Ident(domainNameToLocalVar[domainName]));
+                    var domain = linearTypeChecker.linearDomains[domainName];
+                    Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + 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)
                 {
-                    exprSeq.Add(Expr.Ident(ogOldGlobalMap[ie.Decl]));
+                    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);
                 }
-                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, "linear_" + 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, string.Format("og_yield_{0}", phaseNum), 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;
+                yieldProc = new Procedure(Token.NoToken, string.Format("og_yield_{0}", phaseNum), 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;
+            return yieldCallCmd;
+        }
+
+        private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
+        {
+            if (!CommandLineOptions.Clo.TrustNonInterference)
+            {
+                CallCmd yieldCallCmd = CallToYieldProc(tok, ogOldGlobalMap, domainNameToLocalVar);
                 newCmds.Add(yieldCallCmd);
             }
 
@@ -831,6 +837,40 @@ namespace Microsoft.Boogie
             impl.LocVars.AddRange(newLocalVars);
             impl.LocVars.AddRange(oldPcs);
             impl.LocVars.AddRange(oldOks);
+
+            //UnifyCallsToYieldProc(impl, ogOldGlobalMap, domainNameToLocalVar);
+        }
+
+        private void UnifyCallsToYieldProc(Implementation impl, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
+        {
+            CallCmd yieldCallCmd = CallToYieldProc(Token.NoToken, ogOldGlobalMap, domainNameToLocalVar);
+            Block yieldCheckBlock = new Block(Token.NoToken, "CallToYieldProc", new List<Cmd>(new Cmd[] { yieldCallCmd, new AssumeCmd(Token.NoToken, Expr.False) }), new ReturnCmd(Token.NoToken));
+            List<Block> newBlocks = new List<Block>();
+            foreach (Block b in impl.Blocks)
+            {
+                TransferCmd transferCmd = b.TransferCmd;
+                List<Cmd> newCmds = new List<Cmd>();
+                for (int i = b.Cmds.Count-1; i >= 0; i--)
+                {
+                    CallCmd callCmd = b.Cmds[i] as CallCmd;
+                    if (callCmd == null || callCmd.Proc != yieldProc)
+                    {
+                        newCmds.Insert(0, b.Cmds[i]);
+                    }
+                    else
+                    {
+                        Block newBlock = new Block(Token.NoToken, b.Label + i, newCmds, transferCmd);
+                        newCmds = new List<Cmd>();
+                        transferCmd = new GotoCmd(Token.NoToken, new List<string>(new string[] { newBlock.Label, yieldCheckBlock.Label }), 
+                                                                 new List<Block>(new Block[] { newBlock, yieldCheckBlock }));
+                        newBlocks.Add(newBlock);
+                    }
+                }
+                b.Cmds = newCmds;
+                b.TransferCmd = transferCmd;
+            }
+            impl.Blocks.AddRange(newBlocks);
+            impl.Blocks.Add(yieldCheckBlock);
         }
 
         private List<List<Cmd>> CollectAndDesugarYields(Implementation impl,
-- 
cgit v1.2.3