Merge

7 files changed, 781 insertions, 1484 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 75e1f7e3..78943c1b 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -41,53 +41,6 @@ namespace Microsoft.Boogie
             this.gatePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();

             this.failurePreservationCheckerCache = new HashSet<Tuple<ActionInfo, ActionInfo>>();

         }

-        private sealed class MySubstituter : Duplicator

-        {

-            private readonly Substitution outsideOld;

-            private readonly Substitution insideOld;

-            [ContractInvariantMethod]

-            void ObjectInvariant()

-            {

-                Contract.Invariant(insideOld != null);

-            }

-

-            public MySubstituter(Substitution outsideOld, Substitution insideOld)

-                : base()

-            {

-                Contract.Requires(outsideOld != null && insideOld != null);

-                this.outsideOld = outsideOld;

-                this.insideOld = insideOld;

-            }

-

-            private bool insideOldExpr = false;

-

-            public override Expr VisitIdentifierExpr(IdentifierExpr node)

-            {

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

-                Expr e = null;

-

-                if (insideOldExpr)

-                {

-                    e = insideOld(node.Decl);

-                }

-                else

-                {

-                    e = outsideOld(node.Decl);

-                }

-                return e == null ? base.VisitIdentifierExpr(node) : e;

-            }

-

-            public override Expr VisitOldExpr(OldExpr node)

-            {

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

-                bool previouslyInOld = insideOldExpr;

-                insideOldExpr = true;

-                Expr tmp = (Expr)this.Visit(node.Expr);

-                OldExpr e = new OldExpr(node.tok, tmp);

-                insideOldExpr = previouslyInOld;

-                return e;

-            }

-        }

 

         public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

@@ -141,6 +94,20 @@ namespace Microsoft.Boogie
             }

         }

 

+        public sealed class MyDuplicator : Duplicator

+        {

+            public override Expr VisitIdentifierExpr(IdentifierExpr node)

+            {

+                IdentifierExpr ret = (IdentifierExpr) base.VisitIdentifierExpr(node);

+                if (ret.Decl is GlobalVariable)

+                {

+                    return new OldExpr(Token.NoToken, ret);

+                }

+                else

+                    return ret;

+            }

+        }

+

         public class TransitionRelationComputation

         {

             private Program program;

@@ -193,6 +160,21 @@ namespace Microsoft.Boogie
                 }

             }

 

+            struct PathInfo

+            {

+                public HashSet<Variable> existsVars;

+                public Dictionary<Variable, Expr> varToExpr;

+                public Expr pathExpr;

+

+                public PathInfo(HashSet<Variable> existsVars, Dictionary<Variable, Expr> varToExpr, Expr pathExpr)

+                {

+                    this.existsVars = existsVars;

+                    this.varToExpr = varToExpr;

+                    this.pathExpr = pathExpr;

+                }

+            }

+

+            private List<PathInfo> paths = new List<PathInfo>();

             private Expr CalculatePathCondition()

             {

                 HashSet<Variable> existsVars = new HashSet<Variable>();

@@ -212,14 +194,14 @@ namespace Microsoft.Boogie
                 {

                     varToExpr[v] = Expr.Ident(v);

                 }

-                Expr returnExpr = Expr.True;

+                Expr pathExpr = Expr.True;

                 int boundVariableCount = 0;

                 foreach (Cmd cmd in path)

                 {

                     if (cmd is AssumeCmd)

                     {

                         AssumeCmd assumeCmd = cmd as AssumeCmd;

-                        returnExpr = Expr.And(new OldExpr(Token.NoToken, assumeCmd.Expr), returnExpr);

+                        pathExpr = Expr.And(assumeCmd.Expr, pathExpr);

                     }

                     else if (cmd is AssignCmd)

                     {

@@ -229,7 +211,7 @@ namespace Microsoft.Boogie
                         {

                             map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];

                         }

-                        Substitute(map, ref returnExpr, ref varToExpr);

+                        Substitute(map, ref pathExpr, ref varToExpr);

                     }

                     else if (cmd is HavocCmd)

                     {

@@ -241,13 +223,15 @@ namespace Microsoft.Boogie
                             map[ie.Decl] = new IdentifierExpr(Token.NoToken, bv);

                             existsVars.Add(bv);

                         }

-                        Substitute(map, ref returnExpr, ref varToExpr);

+                        Substitute(map, ref pathExpr, ref varToExpr);

                     }

                     else

                     {

                         Debug.Assert(false);

                     }

                 }

+                paths.Add(new PathInfo(existsVars, varToExpr, pathExpr));

+

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

                 foreach (Variable v in varToExpr.Keys)

                 {

@@ -258,21 +242,39 @@ namespace Microsoft.Boogie
                         existsVars.Remove(ie.Decl);

                     }

                 }

-                Substitute(existsMap, ref returnExpr, ref varToExpr);

-                returnExpr = new OldExpr(Token.NoToken, returnExpr);

+                pathExpr = (new MyDuplicator()).VisitExpr(pathExpr);

                 foreach (Variable v in varToExpr.Keys)

                 {

-                    returnExpr = Expr.And(returnExpr, Expr.Eq(Expr.Ident(v), varToExpr[v]));

+                    pathExpr = Expr.And(pathExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v])));

                 }

+                pathExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(existsMap), pathExpr);

                 if (existsVars.Count > 0)

                 {

-                    returnExpr = new ExistsExpr(Token.NoToken, new List<Variable>(existsVars), returnExpr);

+                    pathExpr = new ExistsExpr(Token.NoToken, new List<Variable>(existsVars), pathExpr);

+                }

+                return pathExpr;

+            }

+

+            public Expr LeftMoverCompute(Expr failureExpr)

+            {

+                Expr returnExpr = Expr.False;

+                foreach (PathInfo path in paths)

+                {

+                    Expr expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(path.varToExpr), failureExpr);

+                    expr = Expr.And(path.pathExpr, expr);

+                    expr = new OldExpr(Token.NoToken, expr);

+                    if (path.existsVars.Count > 0)

+                    {

+                        expr = new ExistsExpr(Token.NoToken, new List<Variable>(path.existsVars), expr);

+                    }

+                    returnExpr = Expr.Or(returnExpr, expr);

                 }

                 return returnExpr;

             }

 

             private void Search(Block b, bool inFirst)

             {

+                int pathSizeAtEntry = path.Count;

                 foreach (Cmd cmd in b.Cmds)

                 {

                     path.Push(cmd);

@@ -304,7 +306,8 @@ namespace Microsoft.Boogie
                         Search(target, inFirst);

                     }

                 }

-                foreach (Cmd cmd in b.Cmds)

+                Debug.Assert(path.Count >= pathSizeAtEntry);

+                while (path.Count > pathSizeAtEntry)

                 {

                     path.Pop();

                 }

@@ -379,7 +382,7 @@ namespace Microsoft.Boogie
 

         private void CreateCommutativityChecker(Program program, ActionInfo first, ActionInfo second)

         {

-            if (first == second)

+            if (first == second && first.thatInParams.Count == 0 && first.thatOutParams.Count == 0)

                 return;

             if (first.CommutesWith(second))

                 return;

@@ -416,7 +419,9 @@ namespace Microsoft.Boogie
             List<Requires> requires = DisjointnessRequires(program, first, second);

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

             Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).Compute();

-            ensures.Add(new Ensures(false, transitionRelation));

+            Ensures ensureCheck = new Ensures(false, transitionRelation);

+            ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name);

+            ensures.Add(ensureCheck);

             string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

             program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));

@@ -450,7 +455,9 @@ namespace Microsoft.Boogie
             foreach (AssertCmd assertCmd in first.thatGate)

             {

                 requires.Add(new Requires(false, assertCmd.Expr));

-                ensures.Add(new Ensures(false, assertCmd.Expr));

+                Ensures ensureCheck = new Ensures(assertCmd.tok, false, assertCmd.Expr, null);

+                ensureCheck.ErrorData = string.Format("Gate not preserved by {0}", second.proc.Name);

+                ensures.Add(ensureCheck);

             }

             string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

@@ -464,49 +471,6 @@ namespace Microsoft.Boogie
 

         private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)

         {

-            Debug.Assert(second.isNonBlocking);

-            if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)

-                return;

-            Tuple<ActionInfo, ActionInfo> actionPair = new Tuple<ActionInfo, ActionInfo>(first, second);

-            if (failurePreservationCheckerCache.Contains(actionPair))

-                return;

-            failurePreservationCheckerCache.Add(actionPair);

-

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

-            inputs.AddRange(first.thatInParams);

-            inputs.AddRange(second.thisInParams);

-

-            Expr failureExpr = Expr.True;

-            foreach (AssertCmd assertCmd in first.thatGate)

-            {

-                failureExpr = Expr.And(assertCmd.Expr, failureExpr);

-            }

-            failureExpr = Expr.Not(failureExpr);

-

-            List<Requires> requires = DisjointnessRequires(program, first, second);

-            requires.Add(new Requires(false, failureExpr));

-

-            List<Ensures> ensures = new List<Ensures>();

-            ensures.Add(new Ensures(false, failureExpr));

-

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

-            outputs.AddRange(first.thatOutParams);

-            outputs.AddRange(second.thisOutParams);

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

-            locals.AddRange(second.thisAction.LocVars);

-            List<Block> secondBlocks = CloneBlocks(second.thisAction.Blocks);

-            string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

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

-            program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));

-            Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

-            Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);

-            impl.Proc = proc;

-            this.decls.Add(impl);

-            this.decls.Add(proc);

-        }

-

-        private void CreateFailurePreservationCheckerExists(Program program, ActionInfo first, ActionInfo second)

-        {

             if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0 && second.isNonBlocking)

                 return;

 

@@ -524,48 +488,22 @@ namespace Microsoft.Boogie
             {

                 requiresExpr = Expr.And(assertCmd.Expr, requiresExpr);

             }

-            requiresExpr = Expr.Not(requiresExpr);

+            Expr failureExpr = Expr.Not(requiresExpr);

             List<Requires> requires = DisjointnessRequires(program, first, second);

-            requires.Add(new Requires(false, requiresExpr));

+            requires.Add(new Requires(false, failureExpr));

             foreach (AssertCmd assertCmd in second.thisGate)

             {

                 requires.Add(new Requires(false, assertCmd.Expr));

             }

 

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

-            Dictionary<Variable, Expr> oldMap = new Dictionary<Variable, Expr>();

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

-            foreach (Variable v in program.GlobalVariables())

-            {

-                if (second.modifiedGlobalVars.Contains(v))

-                {

-                    BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));

-                    boundVars.Add(bv);

-                    map[v] = new IdentifierExpr(Token.NoToken, bv);

-                }

-                else

-                {

-                    map[v] = new OldExpr(Token.NoToken, Expr.Ident(v));

-                }

-                oldMap[v] = Expr.Ident(v);

-            }

-            foreach (Variable v in second.thisOutParams)

-            {

-                BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));

-                boundVars.Add(bv);

-                map[v] = new IdentifierExpr(Token.NoToken, bv);

-            }

-

-            Expr ensuresExpr = Expr.And((new TransitionRelationComputation(program, second)).Compute(), requiresExpr);

-            Substitution subst = Substituter.SubstitutionFromHashtable(map);

-            Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap);

-            ensuresExpr = Substituter.Apply(subst, oldSubst, ensuresExpr);

-            if (boundVars.Count > 0)

-            {

-                ensuresExpr = new ExistsExpr(Token.NoToken, boundVars, ensuresExpr);

-            }

+            TransitionRelationComputation transitionRelationComputation = new TransitionRelationComputation(program, second);

+            transitionRelationComputation.Compute();

+            Expr ensuresExpr = transitionRelationComputation.LeftMoverCompute(failureExpr);

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

-            ensures.Add(new Ensures(false, ensuresExpr));

+            Ensures ensureCheck = new Ensures(false, ensuresExpr);

+            ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);

+            ensures.Add(ensureCheck);

+

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

             blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));

             string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 0fdb01e6..85fce9ff 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -266,7 +266,7 @@ namespace Microsoft.Boogie
             return linearTypeChecker.availableLinearVars[absyMap[absy]];

         }

 

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

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

         {

             List<Expr> exprSeq = new List<Expr>();

             foreach (string domainName in linearTypeChecker.linearDomains.Keys)

@@ -302,12 +302,15 @@ namespace Microsoft.Boogie
             {

                 Expr bb = OldEqualityExpr(ogOldGlobalMap);

 

-                // assert pc ==> o_old == o && g_old == g;

-                newCmds.Add(new AssertCmd(Token.NoToken, Expr.Imp(Expr.Ident(pc), bb)));

-

                 // assert (o_old == o && g_old == g) || beta(i, g_old, o, g);

-                AssertCmd betaAssertCmd = new AssertCmd(Token.NoToken, Expr.Or(bb, beta));

-                newCmds.Add(betaAssertCmd);

+                AssertCmd skipOrBetaAssertCmd = new AssertCmd(tok, Expr.Or(bb, beta));

+                skipOrBetaAssertCmd.ErrorData = "Transition invariant in initial state violated";

+                newCmds.Add(skipOrBetaAssertCmd);

+

+                // assert pc ==> o_old == o && g_old == g;

+                AssertCmd skipAssertCmd = new AssertCmd(tok, Expr.Imp(Expr.Ident(pc), bb));

+                skipAssertCmd.ErrorData = "Transition invariant in final state violated"; ;

+                newCmds.Add(skipAssertCmd);

 

                 // pc, ok := ite(o_old == o && g_old == g, pc, true), ok || beta(i, g_old, o, g);

                 List<Expr> iteArgs = new List<Expr>(new Expr[] { bb, Expr.Ident(pc), Expr.True });

@@ -385,7 +388,7 @@ namespace Microsoft.Boogie
 

         private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)

         {

-            AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

+            AddCallToYieldProc(yieldCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

 

             if (globalMods.Count > 0)

             {

@@ -544,9 +547,15 @@ namespace Microsoft.Boogie
             {

                 var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldGlobalSubst, ensures.Condition);

                 if (ensures.Free)

+                {

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

+                }

                 else

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

+                {

+                    AssertCmd assertCmd = new AssertCmd(ensures.tok, newExpr);

+                    assertCmd.ErrorData = "Backwards non-interference check failed";

+                    newCmds.Add(assertCmd);

+                }

             }

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

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

@@ -641,9 +650,15 @@ namespace Microsoft.Boogie
                     PredicateCmd predCmd = (PredicateCmd)cmd;

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

                     if (predCmd is AssertCmd)

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

+                    {

+                        AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes);

+                        assertCmd.ErrorData = "Non-interference check failed";

+                        newCmds.Add(assertCmd);

+                    }

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

@@ -832,7 +847,7 @@ namespace Microsoft.Boogie
                         CallCmd callCmd = cmd as CallCmd; 

                         if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

                         {

-                            AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

+                            AddCallToYieldProc(callCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

                         }

                         if (callCmd.IsAsync)

                         {

@@ -864,8 +879,13 @@ namespace Microsoft.Boogie
                     else if (cmd is ParCallCmd)

                     {

                         ParCallCmd parCallCmd = cmd as ParCallCmd;

-                        AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

+                        AddCallToYieldProc(parCallCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

                         DesugarParallelCallCmd(newCmds, parCallCmd);

+                        if (globalMods.Count > 0 && pc != null)

+                        {

+                            // assume pc || alpha(i, g);

+                            newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Or(Expr.Ident(pc), alpha)));

+                        }

                         HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));

                         foreach (CallCmd callCmd in parCallCmd.CallCmds)

                         {

@@ -894,10 +914,12 @@ namespace Microsoft.Boogie
                 }

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

                 {

-                    AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

+                    AddCallToYieldProc(b.TransferCmd.tok, newCmds, ogOldGlobalMap, domainNameToLocalVar);

                     if (pc != null)

                     {

-                        newCmds.Add(new AssertCmd(Token.NoToken, Expr.Ident(ok)));

+                        AssertCmd assertCmd = new AssertCmd(b.TransferCmd.tok, Expr.Ident(ok));

+                        assertCmd.ErrorData = "Failed to execute atomic action before procedure return";

+                        newCmds.Add(assertCmd);

                     }

                 }

                 b.Cmds = newCmds;

@@ -917,7 +939,7 @@ namespace Microsoft.Boogie
                 Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(AvailableLinearVars(header), domainNameToInputVar);

                 foreach (Block pred in header.Predecessors)

                 {

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

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

                     if (pc != null && !graph.BackEdgeNodes(header).Contains(pred))

                     {

                         pred.Cmds.Add(new AssignCmd(Token.NoToken, new List<AssignLhs>(

@@ -929,8 +951,13 @@ namespace Microsoft.Boogie
                 List<Cmd> newCmds = new List<Cmd>();

                 if (pc != null)

                 {

-                    newCmds.Add(new AssertCmd(Token.NoToken, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc))));

-                    newCmds.Add(new AssertCmd(Token.NoToken, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok))));

+                    AssertCmd assertCmd;

+                    assertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(oldPc), Expr.Ident(pc)));

+                    assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";

+                    newCmds.Add(assertCmd);

+                    assertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(oldOk), Expr.Ident(ok)));

+                    assertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers";

+                    newCmds.Add(assertCmd);

                 } 

                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)

                 {

@@ -1041,7 +1068,9 @@ namespace Microsoft.Boogie
                     }

                     else

                     {

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

+                        AssertCmd assertCmd = new AssertCmd(r.tok, r.Condition, r.Attributes);

+                        assertCmd.ErrorData = "Non-interference check failed";

+                        cmds.Add(assertCmd);

                     }

                 }

                 yields.Add(cmds);

@@ -1080,7 +1109,9 @@ namespace Microsoft.Boogie
                     }

                     else

                     {

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

+                        AssertCmd assertCmd = new AssertCmd(e.tok, e.Condition, e.Attributes);

+                        assertCmd.ErrorData = "Non-interference check failed";

+                        cmds.Add(assertCmd);

                     }

                 }

                 yields.Add(cmds);

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 542f0e4b..2e7881f6 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -171,7 +171,7 @@ namespace Microsoft.Boogie
 

             {

                 VariableCollector collector = new VariableCollector();

-                this.thisGate.ForEach (assertCmd => collector.Visit(assertCmd));

+                this.thisGate.ForEach(assertCmd => collector.Visit(assertCmd));

                 this.gateUsedGlobalVars = new HashSet<Variable>(collector.usedVars.Where(x => x is GlobalVariable));

             }

         }

@@ -223,11 +223,14 @@ namespace Microsoft.Boogie
                         continue;

                     }

                     ActionInfo actionInfo = new ActionInfo(proc, codeExpr, moverType, phaseNum);

+                    /*

+                     * Removing this restriction based on the new failure preservation check

                     if (actionInfo.IsLeftMover && !actionInfo.isNonBlocking)

                     {

                         Error(e, "A left mover must be non blocking");

                         continue;

                     }

+                     */ 

                     procToActionInfo[proc] = actionInfo;

                 }

             }

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index d7c6b5c2..a848ebeb 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -1,9 +1,5 @@
 #if QED

 

-#define DEBUG

-#define OPTIMIZED

-#define NONOPTIMIZED

-

 using System;

 using System.Collections;

 using System.Collections.Generic;

@@ -14,947 +10,328 @@ using Microsoft.Automata;
 using System.Diagnostics.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie.GraphUtil;

+using System.Diagnostics;

 

 namespace Microsoft.Boogie

 {

-    using Set = GSet<object>;

-

     class YieldTypeChecker

     {

-        /*static subfields of yieldtypesafe(YTS) property language*/

-        static CharSetSolver yieldCheckerAutomatonSolver;

-#if OPTIMIZED

-        static string yieldReachabilityOptCheckerRegex = @"^1*([D]+([571])*A?([97])*)*$";

-        static Automaton<BvSet> yieldReachabilityOptCheckerAutomaton;

-        static Automaton<BvSet> minimizedReachabilityOptCheckerAutomaton;

-#endif

-#if !NONOPTIMIZED

-        static string yieldReachabilityCheckerRegex = @"^([1234])*([D]+([56781234])*A?([973])*)*$";// regex of property to build automaton of YTS language   

-        static Automaton<BvSet> yieldReachabilityCheckerAutomaton;

-        static Automaton<BvSet> minimizedReachabilityCheckerAutomaton;

-#endif

-        static Automaton<BvSet> yieldTypeSafeCheckerAutomaton;

-        static Automaton<BvSet> minimizedYieldTypeSafeCheckerAutomaton;

-

+        static CharSetSolver yieldTypeCheckerAutomatonSolver;

+        static Automaton<BvSet> yieldTypeCheckerAutomaton;

         static YieldTypeChecker()

         {

-            yieldCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);

-#if !NONOPTIMIZED

-            yieldReachabilityCheckerAutomaton =

-            Automaton<BvSet>.MkProduct(yieldCheckerAutomatonSolver.Convert(yieldReachabilityCheckerRegex),

-                                           yieldCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$"), // result of product with this Automaton provides us an automaton that has (*) existence alphanum chars in our property automaton 

-                                           yieldCheckerAutomatonSolver);

-            minimizedReachabilityCheckerAutomaton = yieldReachabilityCheckerAutomaton.Determinize(yieldCheckerAutomatonSolver).Minimize(yieldCheckerAutomatonSolver);

-#endif

-

-#if OPTIMIZED

-            yieldReachabilityOptCheckerAutomaton =

-           Automaton<BvSet>.MkProduct(yieldCheckerAutomatonSolver.Convert(yieldReachabilityOptCheckerRegex),

-                                          yieldCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$"), // result of product with this Automaton provides us an automaton that has (*) existence alphanum chars in our property automaton 

-                                          yieldCheckerAutomatonSolver);

-            minimizedReachabilityOptCheckerAutomaton = yieldReachabilityOptCheckerAutomaton.Determinize(yieldCheckerAutomatonSolver).Minimize(yieldCheckerAutomatonSolver);

-

-#endif

-            yieldTypeSafeCheckerAutomaton = yieldCheckerAutomatonSolver.ReadFromRanges(

-                                            0,

-                                           new int[] { 0, 2 },

-                                           new int[][] { 

-                                               // self loop on state 0 transitions

-                                                new int[] {0,51,51,0}, // Q

-                                                new int[] {0,68,68,0},// Y

-                                                new int[] {0,49,49,0},

-                                               //0 to 1 transitions

-                                                new int[] {0,65,65,1},//A

-                                                new int[] {0,55,55,1}, //B

-                                                new int[] {0,57,57,1},//L

-                                                new int[] {0,53,53,1}, //R

-                                               //self loop on state 1 transitions

-                                                new int[] {1,65,65,1},//A 

-                                                new int[] {1,55,55,1},//B

-                                                new int[] {1,57,57,1},//L

-                                                new int[] {1,53,53,1},//R

-                                                new int[] {1,49,49,1},//P

-                                                new int[] {1,51,51,1},//Q

-                                                //1 to 2 transition

-                                                new int[] {1,68,68,2}, //Y

-                                                //self loop on state 2 transitions

-                                                new int[] {2,65,65,2},//A

-                                                new int[] {2,55,55,2},//B

-                                                new int[] {2,57,57,2},//L

-                                                new int[] {2,53,53,2},//R

-                                                new int[] {2,49,49,2},//P

-                                                new int[] {2,68,68,2},//Y 

-                                                new int[] {2,51,51,2},//Q

-                                           });

-            minimizedYieldTypeSafeCheckerAutomaton = yieldTypeSafeCheckerAutomaton.Determinize(yieldCheckerAutomatonSolver).Minimize(yieldCheckerAutomatonSolver);

-

-#if !DEBUG

-            yieldCheckerAutomatonSolver.ShowGraph(minimizedReachabilityOptCheckerAutomaton, "minimizedReachabilityPropertyAutomaton.dgml");

-            yieldCheckerAutomatonSolver.ShowGraph(minimizedYieldTypeSafeCheckerAutomaton, "minimizedTypeSafePropertyAutomaton.dgml");

-#endif

-        }

-

-        private static Tuple<Automaton<BvSet>, bool> IsYieldReachabilitySafe(Automaton<BvSet> implReachabilityCheckAutomaton, Implementation impl, MoverTypeChecker moverTypeChecker, int phaseNum)

-        {

-            List<BvSet> witnessSet;

-#if !NONOPTIMIZED

-            var isNonEmpty = Automaton<BvSet>.CheckDifference(

-                                                           implReachabilityCheckAutomaton,

-                                                           yieldReachabilityCheckerAutomaton,

-                                                           0,

-                                                           yieldCheckerAutomatonSolver,

-                                                           out witnessSet);

-            var diffAutomaton = implReachabilityCheckAutomaton.Minus(yieldReachabilityCheckerAutomaton, yieldCheckerAutomatonSolver);

-#endif

-

-#if OPTIMIZED

-            var isNonEmpty = Automaton<BvSet>.CheckDifference(

-                                                          implReachabilityCheckAutomaton,

-                                                          yieldReachabilityOptCheckerAutomaton,

-                                                          0,

-                                                          yieldCheckerAutomatonSolver,

-                                                          out witnessSet);

-

-            var diffAutomaton = implReachabilityCheckAutomaton.Minus(yieldReachabilityOptCheckerAutomaton, yieldCheckerAutomatonSolver);

-#endif

-

-            if (isNonEmpty)

-            {

-                var witness = new String(Array.ConvertAll(witnessSet.ToArray(), bvset => (char)yieldCheckerAutomatonSolver.Choose(bvset)));

-                Tuple<Automaton<BvSet>, bool> errTraceExists = new Tuple<Automaton<BvSet>, bool>(diffAutomaton, false);

-                return errTraceExists;

-            }

-            Tuple<Automaton<BvSet>, bool> errTraceNotExist = new Tuple<Automaton<BvSet>, bool>(diffAutomaton, true);

-            return errTraceNotExist;

-        }

-

-        private static Tuple<Automaton<BvSet>, bool> IsYieldTypeSafe(Automaton<BvSet> implTypeSafeCheckAutomaton, Implementation impl, MoverTypeChecker moverTypeChecker, int phaseNum)

+            yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);

+            yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.ReadFromRanges(0, new int[] { 0 },

+                new int[][] {

+                    new int[] {0, 'P', 'P', 0 },

+                    new int[] {0, 'Y', 'Y', 0 },

+                    new int[] {0, 'Y', 'Y', 1 },

+                    new int[] {1, 'P', 'P', 1 },

+                    new int[] {1, 'R', 'R', 1 },

+                    new int[] {1, 'B', 'B', 1 },

+                    new int[] {1, 'Y', 'Y', 1 },

+                    new int[] {1, 'Y', 'Y', 0 },

+                    new int[] {1, 'A', 'A', 2 },

+                    new int[] {1, -1, -1, 2 },

+                    new int[] {2, 'L', 'L', 2 },

+                    new int[] {2, 'B', 'B', 2 },

+                    new int[] {2, 'Y', 'Y', 1 },

+                    new int[] {2, 'Y', 'Y', 0 },

+                });

+            // uncomment the following line to visualize the spec automaton

+            // yieldTypeCheckerAutomatonSolver.ShowGraph(yieldTypeCheckerAutomaton, "yieldTypeCheckerAutomaton.dgml");

+        }

+

+        public void IsYieldTypeSafe(Automaton<BvSet> implAutomaton)

         {

             List<BvSet> witnessSet;

             var isNonEmpty = Automaton<BvSet>.CheckDifference(

-                                                           implTypeSafeCheckAutomaton,

-                                                           yieldTypeSafeCheckerAutomaton,

+                                                           implAutomaton,

+                                                           yieldTypeCheckerAutomaton,

                                                            0,

-                                                           yieldCheckerAutomatonSolver,

+                                                           yieldTypeCheckerAutomatonSolver,

                                                            out witnessSet);

-            var diffAutomaton = implTypeSafeCheckAutomaton.Minus(yieldTypeSafeCheckerAutomaton, yieldCheckerAutomatonSolver);

-

+            var diffAutomaton = implAutomaton.Minus(yieldTypeCheckerAutomaton, yieldTypeCheckerAutomatonSolver);

             if (isNonEmpty)

             {

-                var witness = new String(Array.ConvertAll(witnessSet.ToArray(), bvset => (char)yieldCheckerAutomatonSolver.Choose(bvset)));

-                Tuple<Automaton<BvSet>, bool> errTraceExists = new Tuple<Automaton<BvSet>, bool>(diffAutomaton, false);

-                return errTraceExists;

+                moverTypeChecker.Error(impl, PrintErrorTrace(diffAutomaton));

             }

-            Tuple<Automaton<BvSet>, bool> errTraceNotExist = new Tuple<Automaton<BvSet>, bool>(diffAutomaton, true);

-            return errTraceNotExist;

         }

 

-        private static void/*string*/ PrintErrorTrace(Dictionary<int, Absy> cmds, Automaton<BvSet> errorAutomaton, Implementation yTypeChecked)

+        public string PrintErrorTrace(Automaton<BvSet> errorAutomaton)

         {

-            //   var s = new StringBuilder();

-            String s = "";

-

-            s += "\nError Trace " + yTypeChecked.Proc.Name + "{" + "\n";

+            String s = "\nBody of " + impl.Proc.Name + " is not yield_type_safe at phase " + currPhaseNum.ToString() + "\n";

             foreach (var move in errorAutomaton.GetMoves())

             {

-                s += " [Line :" + cmds[move.SourceState].Line.ToString() + "] , [Cmd :" + cmds[move.SourceState].ToString() + " ]" + " \n";

+                IToken tok = nodeToAbsy[move.SourceState].tok;

+                s += string.Format("{0}({1}, {2})\n", tok.filename, tok.line, tok.col);

             }

-            s += "}";

-

-            Console.WriteLine(s);

-            // return s;

+            return s;

         }

+

         public static void PerformYieldSafeCheck(MoverTypeChecker moverTypeChecker)

         {

-            Program yieldTypeCheckedProgram = moverTypeChecker.program;

-            YieldTypeChecker regExprToAuto = new YieldTypeChecker();

-

-            HashSet<int> phases = moverTypeChecker.allPhaseNums;

-            foreach (int yTypeCheckCurrentPhaseNum in phases) // take current phase check num from each interval

+            foreach (int yTypeCheckCurrentPhaseNum in moverTypeChecker.allPhaseNums)

             {

-                foreach (var decl in yieldTypeCheckedProgram.TopLevelDeclarations)

+                foreach (var decl in moverTypeChecker.program.TopLevelDeclarations)

                 {

                     Implementation impl = decl as Implementation;

                     if (impl == null) continue;

                     int phaseNumSpecImpl = moverTypeChecker.FindPhaseNumber(impl.Proc);

                     if (yTypeCheckCurrentPhaseNum > phaseNumSpecImpl) continue;

 

-                    Tuple<Tuple<Dictionary<int, Absy>, Automaton<BvSet>>, Tuple<Dictionary<int, Absy>, Automaton<BvSet>>> yieldCheckAutomatons =

-                             YieldTypeCheckExecutor.YieldTypeCheckAutomaton(impl, phaseNumSpecImpl, yTypeCheckCurrentPhaseNum, moverTypeChecker);

-

-                    Tuple<Automaton<BvSet>, bool> isYieldReachable = IsYieldReachabilitySafe(yieldCheckAutomatons.Item2.Item2, impl, moverTypeChecker, yTypeCheckCurrentPhaseNum);

-                    Tuple<Automaton<BvSet>, bool> isYieldTypeSafe = IsYieldTypeSafe(yieldCheckAutomatons.Item1.Item2, impl, moverTypeChecker, yTypeCheckCurrentPhaseNum);

-                    Automaton<BvSet> isYieldTypeSafeErrorAut = isYieldTypeSafe.Item1;

-                    Automaton<BvSet> isYieldReachableErrorAut = isYieldReachable.Item1;

-

-                    Dictionary<int, Absy> isYieldTypeSafeCmds = yieldCheckAutomatons.Item1.Item1;

-                    Dictionary<int, Absy> isYieldReachableSafeCmds = yieldCheckAutomatons.Item2.Item1;

-

-                    if (!isYieldReachable.Item2 && !isYieldTypeSafe.Item2)

-                    {

-                        moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield_type_safe at phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");

-                        PrintErrorTrace(isYieldTypeSafeCmds, isYieldTypeSafeErrorAut, impl);

-                        moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield_reachable_safe at phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");

-                        PrintErrorTrace(isYieldReachableSafeCmds, isYieldReachableErrorAut, impl);

-                    }

-                    else if (isYieldReachable.Item2 && !isYieldTypeSafe.Item2)

-                    {

-                        moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield_type_safe at phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");

-                        PrintErrorTrace(isYieldTypeSafeCmds, isYieldTypeSafeErrorAut, impl);

-                    }

-                    else if (!isYieldReachable.Item2 && isYieldTypeSafe.Item2)

-                    {

-                        moverTypeChecker.Error(impl, "\n Body of " + impl.Proc.Name + " is not yield_reachable_safe at phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");

-                        PrintErrorTrace(isYieldReachableSafeCmds, isYieldReachableErrorAut, impl);

-                    }

-                    else if (isYieldReachable.Item2 && isYieldTypeSafe.Item2)

-                    {

-

-                    }

+                    YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, yTypeCheckCurrentPhaseNum);

                 }

             }

         }

-    }

 

-    class YieldTypeCheckExecutor

-    {

-        private static YieldTypeCheckExecutor yieldTypeCheckExecutorInstance;

-        static int stateCounter;

-

-        protected YieldTypeCheckExecutor()

+        public MoverType FindMoverType(Procedure proc)

         {

+            if (!moverTypeChecker.procToActionInfo.ContainsKey(proc))

+                return MoverType.Top;

+            ActionInfo actionInfo = moverTypeChecker.procToActionInfo[proc];

+            if (actionInfo.phaseNum >= currPhaseNum)

+                return MoverType.Top;

+            return actionInfo.moverType;

         }

 

-        public static Tuple<Tuple<Dictionary<int, Absy>, Automaton<BvSet>>, Tuple<Dictionary<int, Absy>, Automaton<BvSet>>>

-            YieldTypeCheckAutomaton(Implementation yTypeChecked, int specPhaseNumImpl, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)

-        {

+        int stateCounter;

+        MoverTypeChecker moverTypeChecker;

+        Implementation impl;

+        int currPhaseNum;

+        Dictionary<Absy, int> absyToNode;

+        Dictionary<int, Absy> nodeToAbsy;

+        HashSet<int> initialStates;

+        HashSet<int> finalStates;

+        Dictionary<Tuple<int, int>, int> edgeLabels;

 

-            if (yieldTypeCheckExecutorInstance == null)

+        public YieldTypeChecker(MoverTypeChecker moverTypeChecker, Implementation impl, int currPhaseNum)

+        {

+            this.moverTypeChecker = moverTypeChecker;

+            this.impl = impl;

+            this.currPhaseNum = currPhaseNum;

+            this.stateCounter = 0;

+            this.absyToNode = new Dictionary<Absy, int>();

+            this.initialStates = new HashSet<int>();

+            initialStates.Add(0);

+            this.finalStates = new HashSet<int>();

+            this.edgeLabels = new Dictionary<Tuple<int, int>, int>(); 

+            

+            foreach (Block block in impl.Blocks)

             {

-                yieldTypeCheckExecutorInstance = new YieldTypeCheckExecutor();

+                foreach (Cmd cmd in block.Cmds)

+                {

+                    absyToNode[cmd] = stateCounter;

+                    stateCounter++;

+                }

+                absyToNode[block.TransferCmd] = stateCounter;

+                stateCounter++;

+                if (block.TransferCmd is ReturnCmd)

+                {

+                    finalStates.Add(absyToNode[block.TransferCmd]);

+                }

             }

-

-            CharSetSolver solver = new CharSetSolver(BitWidth.BV7);

-            Dictionary<Tuple<int, int>, string> edgeLabels = new Dictionary<Tuple<int, int>, string>(); // Tuple<int,int> --> "Y" : State(k) --Y--> State(k+1)

-            HashSet<int> finalStates = new HashSet<int>();

-            HashSet<int> initialStates = new HashSet<int>();

-            stateCounter = 0;

-            initialStates.Add(stateCounter); // First state is added to initial states

-            Dictionary<Absy, int> abysToNode = yieldTypeCheckExecutorInstance.CreateStateNumbers(yTypeChecked);

-            Graph<int> graph = yieldTypeCheckExecutorInstance.BuildAutomatonGraph(yTypeChecked, yTypeCheckCurrentPhaseNum, abysToNode, edgeLabels, finalStates, initialStates, moverTypeChecker); // build component of graph for a phase interval            

-

-            //Buradayim

-            Automaton<BvSet> implYieldTypeSafeCheckAut = yieldTypeCheckExecutorInstance.BuildAutomatonYieldSafe(graph, initialStates, finalStates, edgeLabels, solver);

-            Dictionary<int, Absy> nodeToAbysYieldTypeSafe = new Dictionary<int, Absy>();

-            foreach (KeyValuePair<Absy, int> state in abysToNode)

+            foreach (Block block in impl.Blocks)

             {

-                nodeToAbysYieldTypeSafe[state.Value] = state.Key;

+                GotoCmd gotoCmd = block.TransferCmd as GotoCmd;

+                if (gotoCmd == null) continue;

+                foreach (Block successor in gotoCmd.labelTargets)

+                {

+                    Absy successorEntry = successor.Cmds.Count == 0 ? (Absy)successor.TransferCmd : (Absy)successor.Cmds[0];

+                    edgeLabels[new Tuple<int, int>(absyToNode[block.TransferCmd], absyToNode[successorEntry])] = 'Q';

+                }

             }

-            Tuple<Dictionary<int, Absy>, Automaton<BvSet>> implYieldTypeSafeCheckAutomaton = new Tuple<Dictionary<int, Absy>, Automaton<BvSet>>(nodeToAbysYieldTypeSafe, implYieldTypeSafeCheckAut);

-#if !NONOPTIMIZED

-             // Update edges w.r.t yield reaching. VocabX{True,False} 

-            PostProcessGraph(bodyGraphForImplPhaseJ, edgeLabels);

-            Automaton<BvSet> implYieldReachCheckAut = BuildAutomatonYieldReachSafe(bodyGraphForImplPhaseJ, edgeLabels, initialStates, finalStates, ytypeChecked, yTypeCheckCurrentPhaseNum); // Last to arguments are just only for showGraph of automaton lib

-#endif

-#if OPTIMIZED

-            Automaton<BvSet> implYieldReachCheckAut = yieldTypeCheckExecutorInstance.BuildOptAutomatonYieldReachSafe(yTypeChecked, graph, edgeLabels, initialStates, finalStates, moverTypeChecker, solver);

-#endif

-            Dictionary<int, Absy> nodeToAbysYieldReachSafe = new Dictionary<int, Absy>();

-            foreach (KeyValuePair<Absy, int> state in abysToNode)

+

+            this.nodeToAbsy = new Dictionary<int, Absy>();

+            foreach (KeyValuePair<Absy, int> state in absyToNode)

             {

-                nodeToAbysYieldReachSafe[state.Value] = state.Key;

+                this.nodeToAbsy[state.Value] = state.Key;

             }

-            Tuple<Dictionary<int, Absy>, Automaton<BvSet>> implYieldReachCheckAutomaton = new Tuple<Dictionary<int, Absy>, Automaton<BvSet>>(nodeToAbysYieldReachSafe, implYieldReachCheckAut);

-            Tuple<Tuple<Dictionary<int, Absy>, Automaton<BvSet>>, Tuple<Dictionary<int, Absy>, Automaton<BvSet>>> yieldCheckImplAutomaton =

-                new Tuple<Tuple<Dictionary<int, Absy>, Automaton<BvSet>>, Tuple<Dictionary<int, Absy>, Automaton<BvSet>>>(implYieldTypeSafeCheckAutomaton, implYieldReachCheckAutomaton);

-            return yieldCheckImplAutomaton;

-        }

 

-        public Dictionary<Absy, int> CreateStateNumbers(Implementation yTypeChecked)

-        {

-            Dictionary<Absy, int> abysToNodeNo = new Dictionary<Absy, int>();

-            foreach (Block block in yTypeChecked.Blocks)

+            Graph<int> graph = ComputeGraph();

+

+            // Compute all edges that can reach yield or exit

+            HashSet<int> targetStates = new HashSet<int>(finalStates);

+            foreach (Tuple<int, int> edge in edgeLabels.Keys)

             {

-                foreach (Cmd cmd in block.Cmds)

+                if (edgeLabels[edge] == 'Y')

+                {

+                    targetStates.Add(edge.Item1);

+                }

+            }

+            HashSet<Tuple<int, int>> backwardReachableEdges = CollectBackwardReachableEdges(graph, targetStates);

+            HashSet<Tuple<int, int>> edges = new HashSet<Tuple<int, int>>(edgeLabels.Keys);

+            foreach (Tuple<int, int> edge in edges)

+            {

+                int label = edgeLabels[edge];

+                if (label == 'A' || label == 'L')

                 {

-                    if (IsAsyncCallCmd(cmd)) continue;

-                    if (cmd is ParCallCmd)

+                    if (!backwardReachableEdges.Contains(edge))

                     {

-                        ParCallCmd calle = cmd as ParCallCmd;

-                        for (int i = 0; i < calle.CallCmds.Count; i++)

-                        {

-                            abysToNodeNo[calle.CallCmds[i]] = stateCounter;

-                            stateCounter++;

-                        }

+                        moverTypeChecker.Error(impl, "Error message TBD");

+                    }

+                }

+                else if (label == 'B')

+                {

+                    if (!backwardReachableEdges.Contains(edge))

+                    {

+                        edgeLabels[edge] = 'R';

+                    }

+                }

+                else if (label == 'Q')

+                {

+                    if (!backwardReachableEdges.Contains(edge))

+                    {

+                        edgeLabels[edge] = 'P';

                     }

                     else

                     {

-                        abysToNodeNo[cmd] = stateCounter;

-                        stateCounter++;

+                        edgeLabels[edge] = -1;

                     }

                 }

-                abysToNodeNo[block.TransferCmd] = stateCounter;

-                stateCounter++;

             }

-            return abysToNodeNo;

+            Automaton<BvSet> implYieldTypeSafeCheckAut = BuildAutomatonYieldSafe();

+            IsYieldTypeSafe(implYieldTypeSafeCheckAut);

         }

 

-        private Graph<int> BuildAutomatonGraph(Implementation yTypeChecked, int yTypeCheckCurrentPhaseNum, Dictionary<Absy, int> abysToNode, Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<int> finalStates, HashSet<int> initialStates, MoverTypeChecker moverTypeChecker)

+        private Graph<int> ComputeGraph()

         {

-            HashSet<Tuple<int, int>> edges = new HashSet<Tuple<int, int>>();

-            foreach (Block block in yTypeChecked.Blocks)

+            foreach (Block block in impl.Blocks)

             {

-                if (block.Cmds.Count >= 2)

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

                 {

-                    for (int i = 0; i < block.Cmds.Count - 1; i++)

+                    Cmd cmd = block.Cmds[i];

+                    int curr = absyToNode[cmd];

+                    int next = (i + 1 == block.Cmds.Count) ? absyToNode[block.TransferCmd] : absyToNode[block.Cmds[i + 1]];

+                    Tuple<int, int> edge = new Tuple<int, int>(curr, next);

+                    if (cmd is CallCmd)

                     {

-                        //IsProper

-                        if (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))// this is handled in else but keep this branch now

-                        { // proper state transition

-                            int source = abysToNode[block.Cmds[i]];

-                            int dest = abysToNode[block.Cmds[i + 1]];

-                            Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                            edges.Add(edge);

-                            edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));

-

-                        }

-                        else if (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            int source = abysToNode[block.Cmds[i]];

-                            // create artificial final state

-                            int dest = Math.Abs(Guid.NewGuid().GetHashCode()); // Generate unique dummy node ref: http://msdn.microsoft.com/en-us/library/system.guid(v=vs.110).aspx

-                            finalStates.Add(dest);

-                            Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                            edges.Add(edge);

-                            edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));

-

-                        }

-                        else if (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

+                        CallCmd callCmd = cmd as CallCmd;

+                        if (callCmd.IsAsync)

                         {

-                            int source = abysToNode[block.Cmds[i]];

-                            ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;

-                            int dest = abysToNode[nextCmd.CallCmds[0]];

-                            Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                            edges.Add(edge);

-                            edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));

-                        }

-                        else if (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            int source = abysToNode[block.Cmds[i]];

-                            ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;

-                            int dest = abysToNode[nextCmd.CallCmds[0]];

-                            Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                            edges.Add(edge);

-                            edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));

-                        }

-                        // IsCallCmdsExit

-                        else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        { // current cmd exit , next cmd will be put as initial state

-                            initialStates.Add(abysToNode[block.Cmds[i + 1]]);

+                            edgeLabels[edge] = 'Q';

                         }

-                        else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

+                        else

                         {

-                            continue;

-                        }

-                        else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            // Add state number CallCmd of ParallelCmd

-                            ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;

-                            initialStates.Add(abysToNode[nextCmd.CallCmds[0]]);

-                        }

-                        else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            // Add state number CallCmd of ParallelCmd

-                            ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;

-                            initialStates.Add(abysToNode[nextCmd.CallCmds[0]]);

-

-                        }

-                        // ParallelCallCmdYield

-                        else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;

-                            ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;

-

-                            int source = abysToNode[currentCmd.CallCmds[0]];

-                            int dest = abysToNode[nextCmd.CallCmds[0]];

-                            Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                            edges.Add(edge);

-                            edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));

-

-                        }

-                        else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;

-                            ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;

-

-                            int source = abysToNode[currentCmd.CallCmds[0]];

-                            int dest = abysToNode[nextCmd.CallCmds[0]];

-                            Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                            edges.Add(edge);

-                            edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));

-

+                            switch (FindMoverType(callCmd.Proc))

+                            {

+                                case MoverType.Atomic:

+                                    edgeLabels[edge] = 'A';

+                                    break;

+                                case MoverType.Both:

+                                    edgeLabels[edge] = 'B';

+                                    break;

+                                case MoverType.Left:

+                                    edgeLabels[edge] = 'L';

+                                    break;

+                                case MoverType.Right:

+                                    edgeLabels[edge] = 'R';

+                                    break;

+                                case MoverType.Top:

+                                    finalStates.Add(curr);

+                                    initialStates.Add(next);

+                                    break;

+                            }

                         }

-                        else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

+                    }

+                    else if (cmd is ParCallCmd)

+                    {

+                        ParCallCmd parCallCmd = cmd as ParCallCmd;

+                        bool isYield = false;

+                        bool isRightMover = true;

+                        bool isLeftMover = true;

+                        foreach (CallCmd callCmd in parCallCmd.CallCmds)

                         {

-                            //create dummy state as next state

-                            ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;

-                            int source = abysToNode[currentCmd.CallCmds[0]];

-                            int dest = Math.Abs(Guid.NewGuid().GetHashCode()); // Generate unique dummy node 

-                            finalStates.Add(dest);

-                            Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                            edges.Add(edge);

-                            edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));

-

+                            int phaseSpecCallee = moverTypeChecker.FindPhaseNumber(callCmd.Proc);

+                            if (phaseSpecCallee >= currPhaseNum)

+                            {

+                                isYield = true;

+                            }

                         }

-                        else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

+                        if (isYield)

                         {

-                            ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;

-                            int source = abysToNode[currentCmd.CallCmds[0]];

-                            int dest = abysToNode[block.Cmds[i + 1]];

-                            Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                            edges.Add(edge);

-                            edgeLabels.Add(edge, GetEdgeType(block.Cmds[i]));

+                            edgeLabels[edge] = 'Y';

                         }

-                        //SeqComposable Parallel Cmd

-                        else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

+                        else

                         {

-                            ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;

-                            ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;

-

-                            for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)

+                            foreach (CallCmd callCmd in parCallCmd.CallCmds)

                             {

-                                int source = abysToNode[currentCmd.CallCmds[j]];

-                                int dest = abysToNode[currentCmd.CallCmds[j + 1]];

-                                Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                                edges.Add(edge);

-                                edgeLabels.Add(edge, GetEdgeType(block.Cmds[j]));

+                                ActionInfo actionInfo = moverTypeChecker.procToActionInfo[callCmd.Proc];

+                                isRightMover = isRightMover && actionInfo.IsRightMover;

+                                isLeftMover = isLeftMover && actionInfo.IsLeftMover;

                             }

-                            // Peelout last iteration

-                            int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];

-                            int destBtwCalls = abysToNode[nextCmd.CallCmds[0]];

-                            Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);

-                            edges.Add(edgeBtw);

-                            edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));

-                        }

-                        else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;

-                            ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd;

-

-                            for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)

+                            if (isLeftMover && isRightMover)

                             {

-                                int source = abysToNode[currentCmd.CallCmds[j]];

-                                int dest = abysToNode[currentCmd.CallCmds[j + 1]];

-                                Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                                edges.Add(edge);

-                                edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j]));

+                                edgeLabels[edge] = 'B';

                             }

-                            // Peelout last iteration

-                            int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];

-                            int destBtwCalls = abysToNode[nextCmd.CallCmds[0]];

-                            Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);

-                            edges.Add(edgeBtw);

-                            edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));

-                        }

-                        else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;

-                            for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)

+                            else if (isLeftMover)

                             {

-                                int source = abysToNode[currentCmd.CallCmds[j]];

-                                int dest = abysToNode[currentCmd.CallCmds[j + 1]];

-                                Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                                edges.Add(edge);

-                                edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j]));

+                                edgeLabels[edge] = 'L';

                             }

-                            // Peelout last iteration

-                            int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];

-                            int destBtwCalls = Math.Abs(Guid.NewGuid().GetHashCode()); // Generate unique dummy node 

-                            finalStates.Add(destBtwCalls);

-                            Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);

-                            edges.Add(edgeBtw);

-                            edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));

-

-                        }

-                        else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum, moverTypeChecker) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd;

-

-                            for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)

+                            else if (isRightMover)

                             {

-                                int source = abysToNode[currentCmd.CallCmds[j]];

-                                int dest = abysToNode[currentCmd.CallCmds[j + 1]];

-                                Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                                edges.Add(edge);

-                                edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j]));

+                                edgeLabels[edge] = 'R';

+                            }

+                            else

+                            {

+                                Debug.Assert(false);

                             }

-                            // Peelout last iteration

-                            int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];

-                            int destBtwCalls = abysToNode[block.Cmds[i + 1]]; // Generate unique dummy node 

-                            Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);

-                            edges.Add(edgeBtw);

-                            edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));

                         }

                     }

-                    if (IsExitStatement(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                    { // put b.TransferCmd into initial states

-                        initialStates.Add(abysToNode[block.TransferCmd]);

-                    }

-                    else if (IsParallelCallCmdYield(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

+                    else if (cmd is YieldCmd)

                     {

-                        ParCallCmd currentCmd = block.Cmds[block.Cmds.Count - 1] as ParCallCmd;

-                        int source = abysToNode[currentCmd.CallCmds[0]];

-                        int dest = abysToNode[block.TransferCmd];

-                        Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                        edges.Add(edge);

-                        edgeLabels.Add(edge, GetEdgeType(block.Cmds[block.Cmds.Count - 1]));

+                        edgeLabels[edge] = 'Y';

                     }

-                    else if (IsSeqComposableParCallCmd(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

+                    else if (cmd is AssumeCmd)

                     {

-                        ParCallCmd currentCmd = block.Cmds[block.Cmds.Count - 1] as ParCallCmd;

-                        for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)

+                        if (AccessesGlobals(cmd))

                         {

-                            int source = abysToNode[currentCmd.CallCmds[j]];

-                            int dest = abysToNode[currentCmd.CallCmds[j + 1]];

-                            Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                            edges.Add(edge);

-                            edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j]));

+                            finalStates.Add(curr);

+                            initialStates.Add(next);

                         }

-

-                        int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];

-                        int destBtwCalls = abysToNode[block.TransferCmd]; // Generate unique dummy node 

-                        Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);

-                        edges.Add(edgeBtw);

-                        edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));

-

-                    }

-                    else if (IsProperActionCmd(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                    {

-                        // proper transition to state before transfer command

-                        int source = abysToNode[block.Cmds[block.Cmds.Count - 1]];

-                        int dest = abysToNode[block.TransferCmd];

-                        Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                        edges.Add(edge);

-                        edgeLabels.Add(edge, GetEdgeType(block.Cmds[block.Cmds.Count - 1]));

-                    }

-                }

-                else if (block.Cmds.Count == 1)

-                {

-                    if (IsExitStatement(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                    { // put b.TransferCmd into initial states

-                        initialStates.Add(abysToNode[block.TransferCmd]);

-                    }

-                    else if (IsProperActionCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                    { // proper transition to state before transfer command

-                        int source = abysToNode[block.Cmds[0]];

-                        int dest = abysToNode[block.TransferCmd];

-                        Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                        edges.Add(edge);

-                        edgeLabels.Add(edge, GetEdgeType(block.Cmds[0]));

-                    }

-                    else if (IsParallelCallCmdYield(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                    {

-                        ParCallCmd currentCmd = block.Cmds[0] as ParCallCmd;

-                        int source = abysToNode[currentCmd.CallCmds[0]];

-                        int dest = abysToNode[block.TransferCmd];

-                        Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                        edges.Add(edge);

-                        edgeLabels.Add(edge, GetEdgeType(block.Cmds[0]));

-                    }

-                    else if (IsSeqComposableParCallCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                    {

-                        ParCallCmd currentCmd = block.Cmds[0] as ParCallCmd;

-                        for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++)

+                        else

                         {

-                            int source = abysToNode[currentCmd.CallCmds[j]];

-                            int dest = abysToNode[currentCmd.CallCmds[j + 1]];

-                            Tuple<int, int> edge = new Tuple<int, int>(source, dest);

-                            edges.Add(edge);

-                            edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j]));

+                            edgeLabels[edge] = 'P';

                         }

-

-                        int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]];

-                        int destBtwCalls = abysToNode[block.TransferCmd]; // Generate unique dummy node 

-                        Tuple<int, int> edgeBtw = new Tuple<int, int>(sourceBtwCalls, destBtwCalls);

-                        edges.Add(edgeBtw);

-                        edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]));

-

                     }

-                }

-                else if (block.Cmds.Count == 0)

-                {// Target block Entry state will be fetched

-                }

-                // Handle

-                HashSet<int> targetBlockEntryStates = GetStateOfTargetBlock(block.TransferCmd, yTypeCheckCurrentPhaseNum, abysToNode, finalStates, moverTypeChecker);

-                foreach (int entryState in targetBlockEntryStates)

-                {

-                    int source = abysToNode[block.TransferCmd];

-                    Tuple<int, int> transferEdge = new Tuple<int, int>(source, entryState);

-                    edges.Add(transferEdge);

-                    edgeLabels.Add(transferEdge, "E");

-                }

-            }

-            Graph<int> automatonGraphOfImplPerPhase = new Graph<int>(edges);

-            return automatonGraphOfImplPerPhase;

-        }

-

-        private HashSet<int> GetStateOfTargetBlock(TransferCmd tc, int yTypeCheckCurrentPhaseNum, Dictionary<Absy, int> abysToNode, HashSet<int> finalStates, MoverTypeChecker moverTypeChecker)

-        {

-            HashSet<int> targetBlockEntryStates = new HashSet<int>();

-            if (tc is ReturnCmd)

-            {

-                ReturnCmd returnCmd = tc as ReturnCmd;

-                int source = abysToNode[tc];

-                finalStates.Add(source);

-            }

-            else if (tc is GotoCmd)

-            {

-                GotoCmd transferCmd = tc as GotoCmd;

-                foreach (Block block in transferCmd.labelTargets)

-                {

-                    if (block.Cmds.Count == 0)

+                    else if (cmd is AssertCmd)

                     {

-                        targetBlockEntryStates.Add(abysToNode[block.TransferCmd]); //Target block is empty. Add state of target block's transfer command (Goto or Return) 

+                        edgeLabels[edge] = 'Q';

                     }

-                    else if (block.Cmds.Count >= 1)

+                    else if (cmd is AssignCmd || cmd is HavocCmd)

                     {

-                        if (IsExitStatement(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            int targetState = Math.Abs(Guid.NewGuid().GetHashCode());

-                            finalStates.Add(targetState);

-                            targetBlockEntryStates.Add(targetState);

-                        }

-                        else if (IsProperActionCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                        {

-                            targetBlockEntryStates.Add(abysToNode[block.Cmds[0]]);

-                        }

-                        else if (IsParallelCallCmdYield(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))

+                        if (AccessesGlobals(cmd))

                         {

-                            ParCallCmd targetCmd = block.Cmds[0] as ParCallCmd;

-                            targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]);

+                            finalStates.Add(curr);

+                            initialStates.Add(next);

                         }

-                        else if (IsSeqComposableParCallCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum, moverTypeChecker))

+                        else

                         {

-                            ParCallCmd targetCmd = block.Cmds[0] as ParCallCmd;

-                            targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]);

-                        }

-                        else if (IsAsyncCallCmd(block.Cmds[0]))

-                        {

-                            if (block.Cmds.Count == 1)

-                            {

-                                targetBlockEntryStates.Add(abysToNode[block.TransferCmd]);

-                            }

-                            else if (block.Cmds.Count > 1)

-                            {

-                                int existsNonAsync;

-                                for (existsNonAsync = 0; existsNonAsync < block.Cmds.Count; existsNonAsync++)

-                                {

-                                    if (IsAsyncCallCmd(block.Cmds[existsNonAsync])) continue;

-                                    else if (IsParallelCallCmdYield(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                                    {

-                                        ParCallCmd targetCmd = block.Cmds[existsNonAsync] as ParCallCmd;

-                                        targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]);

-                                        break;

-                                    }

-                                    else if (IsSeqComposableParCallCmd(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                                    {

-                                        ParCallCmd targetCmd = block.Cmds[existsNonAsync] as ParCallCmd;

-                                        targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]);

-                                        break;

-

-                                    }

-                                    else if (IsExitStatement(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                                    {

-                                        int targetState = Math.Abs(Guid.NewGuid().GetHashCode());

-                                        finalStates.Add(targetState);

-                                        targetBlockEntryStates.Add(targetState);

-                                        break;

-                                    }

-                                    else if (IsExitStatement(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum, moverTypeChecker))

-                                    {

-                                        targetBlockEntryStates.Add(abysToNode[block.Cmds[existsNonAsync]]);

-                                        break;

-                                    }

-                                }

-                                if (existsNonAsync == block.Cmds.Count)

-                                {

-                                    // put target 

-                                    targetBlockEntryStates.Add(abysToNode[block.TransferCmd]); //Target block is empty. Add state of target block's transfer command (Goto or Return)

-                                }

-                            }

+                            edgeLabels[edge] = 'Q';

                         }

                     }

-                }

-            }

-            return targetBlockEntryStates;

-        }

-

-        private bool IsAccessToNonQedVar(Cmd cmd, MoverTypeChecker moverTypeChecker)

-        {

-            HashSet<Variable> qedGlobalVariables = moverTypeChecker.QedGlobalVariables();

-            Set globalAccesOfCmd = ComputeGlobalAccesses(cmd);

-

-            HashSet<Variable> glbAccessOfCmd = new HashSet<Variable>();

-            foreach (object var in globalAccesOfCmd)

-            {

-                Variable v = (Variable)var;

-                glbAccessOfCmd.Add(v);

-            }

-            if (glbAccessOfCmd.IsSubsetOf(qedGlobalVariables))

-            {

-                return false;

-            }

-            return true;

-        }

-

-        //        

-        private Set FilterGlobalVariables(Set vars)

-        {

-            Set globals = new Set();

-            foreach (object var in vars)

-            {

-                if (var is GlobalVariable)

-                {

-                    globals.Add((GlobalVariable)var);

-                }

-            }

-            return globals;

-        }

-

-        private Set ComputeGlobalAccesses(Cmd cmd)

-        {

-            Set s = ComputeGlobalReads(cmd);

-            s.AddRange(ComputeGlobalWrites(cmd));

-            return s;

-        }

-

-        private Set ComputeGlobalReads(Cmd cmd)

-        {

-            return FilterGlobalVariables(ComputeReads(cmd));

-        }

-

-        private Set ComputeGlobalWrites(Cmd cmd)

-        {

-            return FilterGlobalVariables(ComputeWrites(cmd));

-        }

-

-        private Set ComputeReads(Cmd cmd)

-        {

-            Set vars = new Set();

-

-            if (cmd is AssertCmd)

-            { // noop

-                // AssertCmd assertCmd = cmd as AssertCmd;

-                //assertCmd.Expr.ComputeFreeVariables(vars);  // We can ignore assert cmds

-            }

-            else if (cmd is AssumeCmd)

-            {

-                AssumeCmd assumeCmd = cmd as AssumeCmd;

-                assumeCmd.Expr.ComputeFreeVariables(vars);

-            }

-            else if (cmd is AssignCmd)

-            {

-                AssignCmd assignCmd = cmd as AssignCmd;

-                foreach (AssignLhs assignLhs in assignCmd.Lhss)

-                {

-                    if (assignLhs is MapAssignLhs)

+                    else

                     {

-                        MapAssignLhs mapLhs = assignLhs as MapAssignLhs;

-                        foreach (Expr index in mapLhs.Indexes)

-                        {

-                            index.ComputeFreeVariables(vars);

-                        }

+                        edgeLabels[edge] = 'Q';

                     }

                 }

-                foreach (Expr rhs in assignCmd.Rhss)

-                {

-                    rhs.ComputeFreeVariables(vars);

-                }

-            }

-

-            else if (cmd is HavocCmd)

-            {

-                // noop

-            }

-            // Delegated to Shaz's type checker

-            /*else if (cmd is CallCmd)

-            {

-                CallCmd callCmd = cmd as CallCmd;

-                foreach (Expr var in callCmd.Ins) {var.ComputeFreeVariables(vars); }      

-                

-            }

-            else if(cmd is ParCallCmd){

-                ParCallCmd parCallCmd = cmd as ParCallCmd;

-              

-                foreach (CallCmd parCalle in parCallCmd.CallCmds) {

-                    foreach (Expr var in parCalle.Ins) {

-        //                Console.WriteLine("ParCall rd var " + var.ToString());

-                        var.ComputeFreeVariables(vars);

-                    }

-

-                }            

-            }*/

-            return vars;

-        }

-        // Discuss and remove

-        private Set ComputeWrites(Cmd cmd)

-        {

-            Set vars = new Set();

-            /*

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

-            cmd.AddAssignedVariables(varseq);

-            foreach (Variable var in varseq)

-            {

-                vars.Add(var);

-            }           

-            return vars;

-            */

-            if (cmd is AssertCmd)

-            {

-                // noop

-            }

-            else if (cmd is AssumeCmd)

-            {

-                // noop

-            }

-            else if (cmd is AssignCmd)

-            {

-                AssignCmd assignCmd = cmd as AssignCmd;

-                foreach (AssignLhs assignLhs in assignCmd.Lhss)

-                {

-                    vars.Add(assignLhs.DeepAssignedVariable);

-                }

-            }

-            else if (cmd is HavocCmd)

-            {

-                HavocCmd havocCmd = cmd as HavocCmd;

-                foreach (Expr var in havocCmd.Vars) { var.ComputeFreeVariables(vars); }

-            }

-            // Delegated to Shaz's type checker

-            /*

-          else if (cmd is CallCmd)

-          {

-              CallCmd callCmd = cmd as CallCmd;

-              foreach (Expr var in callCmd.Proc.Modifies) { var.ComputeFreeVariables(vars); }

-              foreach (Expr var in callCmd.Outs) {  var.ComputeFreeVariables(vars); }

-          }

-          else if (cmd is ParCallCmd) {             

-              ParCallCmd parCallCmd = cmd as ParCallCmd;

-              foreach (CallCmd parCalle in parCallCmd.CallCmds) {

-                  foreach (Expr var in parCalle.Proc.Modifies) { var.ComputeFreeVariables(vars); }

-                  foreach (Expr var in parCalle.Outs) { var.ComputeFreeVariables(vars); }

-              }            

-          }*/

-            return vars;

-        }

-

-        //

-        private bool IsProperActionCmd(Cmd cmd, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)

-        {

-            if (!IsExitStatement(cmd, yTypeCheckCurrentPhaseNum, moverTypeChecker) &&

-                !IsParallelCallCmdYield(cmd, yTypeCheckCurrentPhaseNum, moverTypeChecker) &&

-                !IsSeqComposableParCallCmd(cmd, yTypeCheckCurrentPhaseNum, moverTypeChecker) &&

-                !IsAsyncCallCmd(cmd))

-            {

-                return true;

-            }

-            return false;

-

-        }

-        private bool IsExitStatement(Cmd cmd, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)

-        {

-            if (IsCallCmdExitPoint(cmd, yTypeCheckCurrentPhaseNum, moverTypeChecker) || IsAccessToNonQedVar(cmd, moverTypeChecker)) { return true; }

-            return false;

-        }

-

-        private bool IsCallCmdExitPoint(Cmd cmd, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)

-        {

-            if (cmd is CallCmd && !IsAsyncCallCmd(cmd))

-            {

-                CallCmd callee = cmd as CallCmd;

-                int phaseSpecCallee = moverTypeChecker.FindPhaseNumber(callee.Proc);

-                if (phaseSpecCallee >= yTypeCheckCurrentPhaseNum)

-                {

-                    return true;

-                }

             }

-            return false;

-        }

-

-        private bool IsParallelCallCmdYield(Cmd cmd, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)

-        {

-            if (cmd is ParCallCmd)

+            Graph<int> graph = new Graph<int>(new HashSet<Tuple<int, int>>(edgeLabels.Keys));

+            for (int i = 0; i < stateCounter; i++)

             {

-                ParCallCmd callee = cmd as ParCallCmd;

-                foreach (CallCmd parCallee in callee.CallCmds)

-                {

-                    int phaseSpecCallee = moverTypeChecker.FindPhaseNumber(parCallee.Proc);

-                    if (phaseSpecCallee >= yTypeCheckCurrentPhaseNum)

-                    {

-                        return true;

-                    }

-                }

+                graph.AddSource(i);

             }

-            return false;

+            return graph;

         }

 

-        private bool IsSeqComposableParCallCmd(Cmd cmd, int yTypeCheckCurrentPhaseNum, MoverTypeChecker moverTypeChecker)

+        private static bool AccessesGlobals(Cmd cmd)

         {

-            if (cmd is ParCallCmd && !IsParallelCallCmdYield(cmd, yTypeCheckCurrentPhaseNum, moverTypeChecker)) { return true; }

-            return false;

+            VariableCollector collector = new VariableCollector();

+            collector.Visit(cmd);

+            return collector.usedVars.Any(x => x is GlobalVariable);

         }

-        private bool IsAsyncCallCmd(Cmd cmd)

-        {

-            if (cmd is CallCmd)

-            {

-                CallCmd calle = cmd as CallCmd;

-                if (calle.IsAsync) { return true; }

-            }

-            return false;

-        }

-        private string GetEdgeType(Cmd cmd)

-        {

-            if (cmd is YieldCmd)

-            {

-                return "Y";

-            }

-            else if (cmd is HavocCmd)

-            {

-                return "Q";

-            }

-            else if (cmd is AssumeCmd)

-            {

-                return "P";

-            }

-            else if (cmd is AssertCmd)

-            {

-                return "E";

-            }

-

-            else if (cmd is CallCmd)

-            {

-                CallCmd callCmd = cmd as CallCmd;

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

-                {

-                    int pnum;

-                    MoverType actionType = MoverCheck.GetMoverType(e, out pnum);

-                    if (actionType == MoverType.Atomic) return "A";

-                    else if (actionType == MoverType.Both) return "B";

-                    else if (actionType == MoverType.Left) return "L";

-                    else if (actionType == MoverType.Right) return "R";

-                    else if (actionType == MoverType.Top) continue; // Ask this to Shaz                

-                }

-            }

-            else if (cmd is ParCallCmd) // A small trick here : While getting type of SeqCompositional_parCall_commands we pass CallCmd typed parameter

-            {

-                return "Y";

-            }

-            //else if (cmd is AssignCmd)

-            //{  //rest can only be assigncmd                

-            return "Q";

-            //}

-        }

-        private string PrintGraph(Implementation yTypeChecked, Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels)

+        

+        private static string PrintGraph(Implementation yTypeChecked, Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels)

         {

             var s = new StringBuilder();

             s.AppendLine("\nImplementation " + yTypeChecked.Proc.Name + " digraph G {");

@@ -964,494 +341,48 @@ namespace Microsoft.Boogie
             return s.ToString();

         }

 

-#if !NONOPTIMIZED

-        private HashSet<Tuple<int, int>> CollectBackwardEdgesOfYieldEdge(int source)

-        {

-            HashSet<Tuple<int, int>> yieldReachingEdges = new HashSet<Tuple<int, int>>(); // Collect edges that are backward reachable from source vertex of yield a edge,source ---Y---> sink, in backward direction

-            HashSet<int> gray = new HashSet<int>();

-            HashSet<int> black = new HashSet<int>();

-            HashSet<int> white = new HashSet<int>();

-            // Add all vertices except s into 

-            foreach (int v in graph.Nodes)

-            {

-                if (!v.Equals(source))

-                    white.Add(v);

-            }

-

-            Queue<int> frontier = new Queue<int>(); //

-            // n is given as start vertex 

-            gray.Add(source);

-            frontier.Enqueue(source);

-

-            while (frontier.Count > 0)

-            {

-                int u = frontier.Dequeue();

-                foreach (int v in graph.Predecessors(u))

-                {

-

-                    if (white.Contains(v) && !gray.Contains(v) && !black.Contains(v))

-                    {

-

-                        gray.Add(v);

-                        frontier.Enqueue(v);

-                        // Add to yielding edges

-                        yieldReachingEdges.Add(new Tuple<int, int>(v, u));

-                    }

-

-                }

-                black.Add(u);

-            }

-

-            return yieldReachingEdges;

-        }

-

-

-        /*

-         * Calls CollectBackEdges for each Y edge existing in graph

-         */

-        private HashSet<Tuple<int, int>> CollectYieldReachingEdgesOfGraph()

-        {

-            HashSet<Tuple<int, int>> yieldTrueEdges = new HashSet<Tuple<int, int>>(); // Set {forall edges e : e is reaching a Y labeled edge}

-            foreach (var e in graph.Edges) // Visits all edges to and do backward yield reachability analysis starting from source vertex of an "Y" labeled edge

-            {

-                if (edgeLabels[e] == "Y")

-                {

-                    HashSet<Tuple<int, int>> yieldReachingEdges = CollectBackwardEdgesOfYieldEdge(e.Item1);

-                    foreach (Tuple<int, int> yldrch in yieldReachingEdges)

-                    {

-

-                        yieldTrueEdges.Add(yldrch);

-                    }

-                }

-            }

-            return yieldTrueEdges;

-        }

-#endif

-        private HashSet<Tuple<int, int>> CollectEdgesReachableFromAction(Graph<int> graph, int source)

+        private static HashSet<Tuple<int, int>> CollectBackwardReachableEdges(Graph<int> graph, HashSet<int> targets)

         {

-            HashSet<Tuple<int, int>> edgesReachable = new HashSet<Tuple<int, int>>(); // Collect edges that are backward reachable from source vertex of yield a edge,source ---Y---> sink, in backward direction

+            HashSet<Tuple<int, int>> edgesReachable = new HashSet<Tuple<int, int>>(); 

             HashSet<int> gray = new HashSet<int>();

-            HashSet<int> black = new HashSet<int>();

-            HashSet<int> white = new HashSet<int>();

-            // Add all vertices except s into 

-            foreach (int v in graph.Nodes)

+            Queue<int> frontier = new Queue<int>();

+            foreach (int v in targets)

             {

-                if (!v.Equals(source))

-                    white.Add(v);

+                gray.Add(v);

+                frontier.Enqueue(v);

             }

-            Queue<int> frontier = new Queue<int>(); //

-            // n is given as start vertex 

-            gray.Add(source);

-            frontier.Enqueue(source);

-

             while (frontier.Count > 0)

             {

-                int u = frontier.Dequeue();

-                foreach (int v in graph.Successors(u))

+                int v = frontier.Dequeue();

+                foreach (int u in graph.Predecessors(v))

                 {

-                    if (white.Contains(v) && !gray.Contains(v) && !black.Contains(v))

+                    edgesReachable.Add(new Tuple<int, int>(u, v));

+                    if (!gray.Contains(u))

                     {

-                        gray.Add(v);

-                        frontier.Enqueue(v);

-                        // Add to yielding edges

-                        edgesReachable.Add(new Tuple<int, int>(u, v));

+                        gray.Add(u);

+                        frontier.Enqueue(u);

                     }

                 }

-                black.Add(u);

             }

             return edgesReachable;

         }

 

-        private void IsExitOrRetReachableFromAtomicOrLeft(Implementation yTypeChecked, Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<int> finalStates, MoverTypeChecker moverTypeChecker)

-        {

-            foreach (var e in graph.Edges)

-            {

-                if (edgeLabels[e] == "A" || edgeLabels[e] == "L")

-                {

-                    HashSet<Tuple<int, int>> edgesReachable = CollectEdgesReachableFromAction(graph, e.Item1);

-

-                    if (!(ReachesFinalState(finalStates, edgesReachable) || ReachesYieldState(edgeLabels, edgesReachable)))

-                    {

-                        moverTypeChecker.Error(yTypeChecked, "Implementation Yield Reachable " + yTypeChecked.Proc.Name);

-                    }

-                }

-            }

-        }

-        private void IsExitOrReachableFromBoth(Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<int> finalStates)

-        {

-            foreach (var e in graph.Edges)

-            {

-                if (edgeLabels[e] == "B")

-                {

-                    HashSet<Tuple<int, int>> edgesReachable = CollectEdgesReachableFromAction(graph, e.Item1);

-                    if (!(ReachesFinalState(finalStates, edgesReachable) || ReachesYieldState(edgeLabels, edgesReachable)))

-                    {

-                        edgeLabels[e] = "R";

-                    }

-                }

-            }

-

-        }

-        private void IsExitOrReachableFromLocal(Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<int> finalStates)

-        {

-            foreach (var e in graph.Edges)

-            {

-                if (edgeLabels[e] == "Q")

-                {

-                    HashSet<Tuple<int, int>> edgesReachable = CollectEdgesReachableFromAction(graph, e.Item1);

-                    if (!(ReachesFinalState(finalStates, edgesReachable) || ReachesYieldState(edgeLabels, edgesReachable)))

-                    {

-                        edgeLabels[e] = "P";

-                    }

-                    edgeLabels[e] = "E";

-                }

-            }

-        }

-        private bool ReachesFinalState(HashSet<int> finalStates, HashSet<Tuple<int, int>> edges)

-        {

-

-            foreach (Tuple<int, int> e in edges)

-            {

-                if (finalStates.Contains(e.Item1) || finalStates.Contains(e.Item2)) return true;

-            }

-            return false;

-        }

-        private bool ReachesYieldState(Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<Tuple<int, int>> edges)

-        {

-            foreach (var e in edges)

-            {

-

-                if (edgeLabels[e] == "Y") return true;

-            }

-            return false;

-        }

-

-        private Automaton<BvSet> BuildOptAutomatonYieldReachSafe(Implementation yTypeChecked, Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels, HashSet<int> initialStates, HashSet<int> finalStates, MoverTypeChecker moverTypeChecker, CharSetSolver solver)

-        {

-            IsExitOrRetReachableFromAtomicOrLeft(yTypeChecked, graph, edgeLabels, finalStates, moverTypeChecker); ;

-            IsExitOrReachableFromBoth(graph, edgeLabels, finalStates);

-            IsExitOrReachableFromLocal(graph, edgeLabels, finalStates);

-            return BuildAutomatonYieldSafe(graph, initialStates, finalStates, edgeLabels, solver);

-        }

-#if !NONOPTIMIZED

-        /*

-         * Updates vertices map according to according to yieldReaching edges. If an edge in graph is not yield reaching that its vertices map updated.

-         */

-        private void PostProcessGraph()

-        {

-            HashSet<Tuple<int, int>> yieldTrueEdges = CollectYieldReachingEdgesOfGraph();

-

-            foreach (Tuple<int, int> yldrch in yieldTrueEdges)

-            {

-                if (edgeLabels[yldrch] == "Q")

-                {

-                    edgeLabels[yldrch] = "3";

-                }

-                else if (edgeLabels[yldrch] == "P")

-                {

-                    edgeLabels[yldrch] = "1";

-                }

-                else if (edgeLabels[yldrch] == "B")

-                {

-                    edgeLabels[yldrch] = "7";

-                }

-                else if (edgeLabels[yldrch] == "R")

-                {

-                    edgeLabels[yldrch] = "5";

-                }

-                else if (edgeLabels[yldrch] == "L")

-                {

-                    edgeLabels[yldrch] = "9";

-                }

-                else if (edgeLabels[yldrch] == "A")

-                {

-                    edgeLabels[yldrch] = "A";

-                }

-                else if (edgeLabels[yldrch] == "Y")

-                {

-                    edgeLabels[yldrch] = "D";

-                }

-            }

-            foreach (Tuple<int, int> nyldrch in graph.Edges)

-            {

-                if (!yieldTrueEdges.Contains(nyldrch))

-                {

-                    if (edgeLabels[nyldrch] == "Q")

-                    {

-                        edgeLabels[nyldrch] = "4";

-                    }

-                    else if (edgeLabels[nyldrch] == "P")

-                    {

-                        edgeLabels[nyldrch] = "2";

-                    }

-                    else if (edgeLabels[nyldrch] == "B")

-                    {

-                        edgeLabels[nyldrch] = "8";

-                    }

-                    else if (edgeLabels[nyldrch] == "R")

-                    {

-                        edgeLabels[nyldrch] = "6";

-                    }

-                    else if (edgeLabels[nyldrch] == "L")

-                    {

-                        edgeLabels[nyldrch] = "C";

-                    }

-                    else if (edgeLabels[nyldrch] == "A")

-                    {

-                        edgeLabels[nyldrch] = "B";

-                    }

-                    else if (edgeLabels[nyldrch] == "Y")

-                    {

-                        edgeLabels[nyldrch] = "D";

-                    }

-                }

-            }

-        }

-#endif

-        private int[] ComputeFinalStates(HashSet<int> finalStates)

-        {

-            return finalStates.ToArray();

-        }

-        private int[] ComputeInitialStates(HashSet<int> initialStates)

-        {

-            return initialStates.ToArray();

-        }

-

-        private Automaton<BvSet> BuildAutomatonYieldSafe(Graph<int> graph, HashSet<int> initialStates, HashSet<int> finalStates, Dictionary<Tuple<int, int>, string> edgeLabels, CharSetSolver solver)

+        private Automaton<BvSet> BuildAutomatonYieldSafe()

         {

             List<int[]> transitions = new List<int[]>();

-            foreach (Tuple<int, int> e in graph.Edges)

-            {

-                if (edgeLabels[e] == "Q")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 51; // ASCII 3

-                    transition[2] = 51;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "P")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 49; // ASCII 1

-                    transition[2] = 49;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "B")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 55; // ASCII 7

-                    transition[2] = 55;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "R")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 53; // ASCII 5

-                    transition[2] = 53;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "L")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 57; // ASCII 9

-                    transition[2] = 57;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "A")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 65; // ASCII A

-                    transition[2] = 65;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "Y")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 68; // ASCII D

-                    transition[2] = 68;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "E")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = -1;

-                    transition[2] = -1;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-

-            }

-

-            // get final states

-            int[] finalSts = ComputeFinalStates(finalStates);

-            int dummyInitial = Math.Abs(Guid.NewGuid().GetHashCode());

-            foreach (int s in initialStates)

+            foreach (Tuple<int, int> e in edgeLabels.Keys)

             {

+                int label = edgeLabels[e];

+                Debug.Assert(label != 'Q');

                 int[] transition = new int[4];

-                transition[0] = dummyInitial;

-                transition[1] = -1;

-                transition[2] = -1;

-                transition[3] = s;

+                transition[0] = e.Item1;

+                transition[1] = label;

+                transition[2] = label;

+                transition[3] = e.Item2;

                 transitions.Add(transition);

             }

-            // create Automaton

-            Automaton<BvSet> yieldTypeCheckAutomaton = solver.ReadFromRanges(dummyInitial, finalSts, transitions);

-            return yieldTypeCheckAutomaton;

-        }

-#if !NONOPTIMIZED

 

-        private Automaton<BvSet> BuildAutomatonYieldReachSafe()

-        {

-            List<int[]> transitions = new List<int[]>();

-            foreach (Tuple<int, int> e in graph.Edges)

-            {

-                if (edgeLabels[e] == "3")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 51; // ASCII 3

-                    transition[2] = 51;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "1")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 49; // ASCII 1

-                    transition[2] = 49;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "7")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 55; // ASCII 7

-                    transition[2] = 55;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "5")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 53; // ASCII 5

-                    transition[2] = 53;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "9")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 57; // ASCII 9

-                    transition[2] = 57;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "A")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 65; // ASCII A

-                    transition[2] = 65;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "D")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 68; // ASCII D

-                    transition[2] = 68;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "4")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 52; // ASCII 4

-                    transition[2] = 52;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "2")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 50; // ASCII 2

-                    transition[2] = 50;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "8")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 56; // ASCII 8

-                    transition[2] = 56;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "6")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 54; // ASCII 6

-                    transition[2] = 54;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "C")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 67; // ASCII C

-                    transition[2] = 67;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "B")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = 66; // ASCII B

-                    transition[2] = 66;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-                else if (edgeLabels[e] == "E")

-                {

-                    int[] transition = new int[4];

-                    transition[0] = e.Item1;

-                    transition[1] = -1;

-                    transition[2] = -1;

-                    transition[3] = e.Item2;

-                    transitions.Add(transition);

-                }

-

-            }

-

-            // get final states

-            int[] finalSts = ComputeFinalStates();

-            int dummyInitial = Math.Abs(Guid.NewGuid().GetHashCode());

+            int dummyInitial = stateCounter;

             foreach (int s in initialStates)

             {

                 int[] transition = new int[4];

@@ -1462,24 +393,10 @@ namespace Microsoft.Boogie
                 transitions.Add(transition);

             }

 

-            // create Automaton

-            Automaton<BvSet> yieldTypeCheckAutomaton = solver.ReadFromRanges(dummyInitial, finalSts, transitions);

+            Automaton<BvSet> yieldTypeCheckAutomaton = yieldTypeCheckerAutomatonSolver.ReadFromRanges(dummyInitial, finalStates.ToArray(), transitions);

             return yieldTypeCheckAutomaton;

-

-        }

-#endif

-        private string PrintEpsilon(BvSet cond, CharSetSolver slvr)

-        {

-            if (cond == null)

-            {

-                return "E";

-            }

-            else return slvr.PrettyPrint(cond);

-

         }

     }

-

-

 }

 

 #endif
\ No newline at end of file
diff --git a/Test/og/Answer b/Test/og/Answer
index 73ec8537..067a6534 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -1,6 +1,6 @@
 

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

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

+foo.bpl(14,3): Error: Non-interference check failed

 Execution trace:

     foo.bpl(6,5): anon0

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

@@ -8,11 +8,11 @@ Execution trace:
 Boogie program verifier finished with 4 verified, 1 error

 

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

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

+bar.bpl(13,3): Error: Non-interference check failed

 Execution trace:

     bar.bpl(6,5): anon0

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

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

+bar.bpl(13,3): Error: Non-interference check failed

 Execution trace:

     bar.bpl(23,5): anon0

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

@@ -24,11 +24,11 @@ Boogie program verifier finished with 3 verified, 2 errors
 Boogie program verifier finished with 2 verified, 0 errors

 

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

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

+parallel1.bpl(10,1): Error: Non-interference check failed

 Execution trace:

     parallel1.bpl(6,5): anon0

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

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

+parallel1.bpl(14,3): Error: Non-interference check failed

 Execution trace:

     parallel1.bpl(6,5): anon0

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

@@ -72,7 +72,7 @@ Boogie program verifier finished with 4 verified, 0 errors
 Boogie program verifier finished with 3 verified, 0 errors

 

 -------------------- t1.bpl --------------------

-t1.bpl(35,5): Error BP5001: This assertion might not hold.

+t1.bpl(35,5): Error: Non-interference check failed

 Execution trace:

     (0,0): og_init

     (0,0): inline$Impl_YieldChecker_A_2147483647$0$L1

@@ -88,7 +88,7 @@ Boogie program verifier finished with 2 verified, 0 errors
 Boogie program verifier finished with 2 verified, 0 errors

 

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

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

+async.bpl(14,1): Error: Non-interference check failed

 Execution trace:

     async.bpl(7,3): anon0

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

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
new file mode 100644
index 00000000..9da8c125
--- /dev/null
+++ b/Test/og/multiset.bpl
@@ -0,0 +1,322 @@
+type X;

+

+const unique null : int;

+const unique nil: X;

+const unique done: X;

+

+var {:qed} elt : [int]int;

+var {:qed} valid : [int]bool;

+var {:qed} lock : [int]X;

+var {:qed} owner : [int]X;

+const max : int;

+

+axiom (max > 0);

+

+procedure {:yields} acquire(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+ensures {:right 0} |{ A: 

+                      assert 0 <= i && i < max;

+                      assert tidIn != nil && tidIn != done;

+                      assume lock[i] == nil;

+                      tidOut := tidIn;

+	              lock[i] := tidOut;

+                      return true;

+                    }|;

+

+

+procedure {:yields} release(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+ensures {:left 0} |{ A: 

+                     assert 0 <= i && i < max;

+                     assert lock[i] == tidIn;

+                     assert tidIn != nil && tidIn != done; 

+                     tidOut := tidIn;

+	             lock[i] := nil;

+                     return true;

+                    }|;

+

+

+procedure {:yields} getElt(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);

+ensures {:both 0} |{ A: 

+                     assert 0 <= j && j < max;

+                     assert lock[j] == tidIn;

+                     assert tidIn != nil && tidIn != done;

+                     tidOut := tidIn;

+	             elt_j := elt[j];

+                     return true;

+                    }|;

+

+

+procedure {:yields} setElt(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+ensures {:both 0} |{ A: 

+                     assert x != null;

+                     assert owner[j] == nil;

+                     assert 0 <= j && j < max;

+                     assert lock[j] == tidIn;

+                     assert tidIn != nil && tidIn != done;

+                     tidOut := tidIn;

+	             elt[j] := x;

+                     owner[j] := tidIn;

+                     return true;

+                    }|;

+

+

+procedure {:yields} setEltToNull(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+ensures {:left 0} |{ A: 

+                     assert owner[j] == tidIn;

+                     assert 0 <= j && j < max;

+                     assert lock[j] == tidIn;

+                     assert !valid[j];

+                     assert tidIn != nil  && tidIn != done;

+                     tidOut := tidIn;

+	             elt[j] := null;

+                     owner[j] := nil;

+                     return true;

+                    }|;

+

+

+

+

+procedure {:yields} getValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, valid_j:bool);

+ensures {:both 0} |{ A: 

+                     assert 0 <= j && j < max;

+                     assert lock[j] == tidIn;

+                     assert tidIn != nil  && tidIn != done;

+                     tidOut := tidIn;

+	             valid_j := valid[j];

+                     return true;

+                    }|;

+

+

+procedure {:yields} setValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

+ensures {:both 0} |{ A: 

+                     assert 0 <= j && j < max;

+                     assert lock[j] == tidIn;

+                     assert tidIn != nil && tidIn != done;

+                     assert owner[j] == tidIn;

+                     tidOut := tidIn;

+	             valid[j] := true;

+                     owner[j] := done;

+                     return true;

+                    }|;

+

+

+procedure {:yields} FindSlot(x : int, {:linear "tid"} tidIn: X) returns (r : int, {:linear "tid"} tidOut: X)

+requires {:phase 1} Inv(valid, elt, owner);

+ensures {:phase 1} Inv(valid, elt, owner);

+ensures {:right 1}  |{ A: assert tidIn != nil && tidIn != done; 

+                          assert x != null; 

+                          // assert (forall ii:int :: 0 <= ii && ii<max ==> lock[ii] != tidIn);

+                          havoc r; assume (-1 <= r && r < max); goto B, C;

+                       B: assume (r != -1); 

+                                            assume elt[r] == null; 

+                                            assume owner[r] == nil;

+                                            elt[r] := x; 

+                                            owner[r] := tidIn;

+                                            tidOut := tidIn; 

+                                            return true;

+                       C: assume (r == -1); tidOut := tidIn; return true; 

+                   }|;

+{

+	var j : int;

+	var elt_j : int;

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

+        

+        par Yield1();

+

+	j := 0;

+        tidTmp := tidIn;

+

+	

+	while(j < max)

+        invariant {:phase 1} tidTmp != nil && tidTmp != done;

+        invariant {:phase 1} tidTmp == tidIn;

+        invariant {:phase 1} Inv(valid, elt, owner);

+	{

+                par Yield1();

+

+                call tidTmp := acquire(j, tidTmp);

+                call tidTmp, elt_j := getElt(j, tidTmp);

+		if(elt_j == null)

+		{

+                        call tidTmp := setElt(j, x, tidTmp);

+			call tidTmp := release(j, tidTmp);

+			r := j;

+                        tidOut := tidTmp;

+

+                        par Yield1();

+

+			return;		

+		}

+		call tidTmp := release(j,tidTmp);

+

+                par Yield1();

+

+		j := j + 1;	

+	}

+	r := -1;

+        tidOut := tidTmp;

+	return;

+}

+

+procedure {:yields} Insert(x : int, {:linear "tid"} tidIn: X) returns (result : bool, i : int, {:linear "tid"} tidOut: X) 

+requires {:phase 1} Inv(valid, elt, owner);

+requires {:phase 2} Inv(valid, elt, owner);

+ensures {:phase 1} Inv(valid, elt, owner);

+requires {:phase 2} Inv(valid, elt, owner);

+ensures {:atomic 2}  |{ var r:int;

+                        A: assert tidIn != nil && tidIn != done; 

+                           assert x != null;

+                           havoc r; assume (-1 <= r && r < max); goto B, C;

+                        B: assume (r != -1); 

+                           assume valid[r] == false; 

+                           assume elt[r] == null; 

+                           assume owner[r] == nil; 

+                           elt[r] := x; valid[r] := true; owner[r] := done;

+                           tidOut := tidIn; result := true; return true;

+                        C: tidOut := tidIn; result := false; return true; 

+                      }|;

+ {

+

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

+        par Yield12();

+        tidTmp := tidIn;

+        call i, tidTmp := FindSlot(x, tidTmp);

+        

+	if(i == -1)

+	{

+		result := false;

+                tidOut := tidTmp;

+                par YieldInv();

+		return;

+	}

+        par Yield1();

+        assert {:phase 1} i != -1;

+        assert {:phase 2} i != -1;

+	call tidTmp := acquire(i, tidTmp);

+        assert {:phase 2} elt[i] == x;

+	assert {:phase 2}  valid[i] == false;

+        call tidTmp := setValid(i, tidTmp);   

+	call tidTmp := release(i, tidTmp);

+	result := true; 

+        tidOut := tidTmp;

+        par YieldInv();

+	return;

+}

+

+procedure {:yields} InsertPair(x : int, 

+                               y : int, 

+                               {:linear "tid"} tidIn: X) 

+                               returns (result : bool, 

+                                        i : int, 

+                                        j : int,

+                                        {:linear "tid"} tidOut: X) 

+requires {:phase 1} Inv(valid, elt, owner);

+ensures {:phase 1} Inv(valid, elt, owner);

+requires {:phase 2} Inv(valid, elt, owner);

+ensures {:phase 2} Inv(valid, elt, owner);

+ensures {:atomic 2}  |{ var rx:int;

+                        var ry:int;

+                        A: assert tidIn != nil && tidIn != done; 

+                           assert x != null && y != null;

+                           havoc rx; assume (-1 <= rx && rx < max); 

+                           havoc ry; assume (-1 <= ry && ry < max);

+                           assume (rx == ry ==> rx == -1);

+                           goto B, C;

+                        B: assume (rx != -1 && ry != -1); 

+                           assume valid[rx] == false; 

+                           assume valid[ry] == false; 

+                           assume elt[rx] == null; 

+                           assume elt[rx] == null; 

+                           elt[rx] := x; 

+                           elt[ry] := y; 

+                           valid[rx] := true; 

+                           valid[ry] := true;

+                           owner[rx] := done;

+                           owner[ry] := done; 

+                           tidOut := tidIn; 

+                           result := true; return true;

+                        C: tidOut := tidIn; 

+                           result := false; return true; 

+                      }|;

+ {

+

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

+        par Yield12();

+

+        tidTmp := tidIn;

+

+        call i, tidTmp := FindSlot(x, tidTmp);

+        

+	if (i == -1)

+	{

+	 	result := false;

+                tidOut := tidTmp;

+                par Yield12();

+		return;

+	}

+

+        par Yield1();

+        call j, tidTmp := FindSlot(y, tidTmp);

+        

+	if(j == -1)

+	{

+                par Yield1();

+                call tidTmp := acquire(i,tidTmp);  

+                call tidTmp := setEltToNull(i, tidTmp);

+                call tidTmp := release(i,tidTmp);  

+		result := false;

+                tidOut := tidTmp;

+                par Yield12();

+		return;

+	}

+

+        par Yield1();

+        assert {:phase 2} i != -1 && j != -1;

+	call tidTmp := acquire(i, tidTmp);

+	call tidTmp := acquire(j, tidTmp);

+        assert {:phase 2} elt[i] == x;

+        assert {:phase 2} elt[j] == y;

+	assert {:phase 2}  valid[i] == false;

+	assert {:phase 2}  valid[j] == false;

+        call tidTmp := setValid(i, tidTmp);   

+        call tidTmp := setValid(j, tidTmp);   

+	call tidTmp := release(j, tidTmp);

+	call tidTmp := release(i, tidTmp);

+	result := true; 

+        tidOut := tidTmp;

+        par Yield12();

+	return;

+}

+

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

+requires {:phase 1} Inv(valid, elt, owner);

+ensures {:phase 1} Inv(valid, elt, owner);

+ensures {:both 1} |{ A: return true; }|;

+{

+}

+

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

+requires {:phase 2} Inv(valid, elt, owner);

+ensures {:phase 2} Inv(valid, elt, owner);

+{

+        yield;

+        assert {:phase 2} Inv(valid, elt, owner);

+}

+

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

+requires {:phase 1} {:phase 2} Inv(valid, elt, owner);

+ensures {:phase 1} {:phase 2} Inv(valid, elt, owner);

+{

+        yield;

+        assert {:phase 1}  {:phase 2} Inv(valid, elt, owner);

+}

+

+

+

+function {:inline} Inv(valid: [int]bool, elt: [int]int, owner: [int]X): (bool)

+{

+   ( forall i:int :: 0 <= i && i < max ==> 

+                          ( elt[i] == null <==> 

+                            !valid[i] && (owner[i] == nil)

+                          ) 

+   )

+}

diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
new file mode 100644
index 00000000..707688a6
--- /dev/null
+++ b/Test/og/treiber-stack.bpl
@@ -0,0 +1,86 @@
+type Node;

+type lmap;

+function dom(lmap): [Node]bool;

+function map(lmap): [Node]Node;

+

+function {:builtin "MapConst"} MapConst(bool) : [Node]bool;

+function {:builtin "MapOr"} MapOr([Node]bool, [Node]bool) : [Node]bool;

+

+procedure Load(i:Node) returns(v:Node);

+  requires dom(stack)[i];

+  ensures  v == map(stack)[i];

+

+procedure Store({:linear "Node"} l_in:lmap, i:Node, v:Node) returns({:linear "Node"} l_out:lmap);

+  requires dom(l_in)[i];

+  ensures  dom(l_out) == dom(l_in);

+  ensures  map(l_out) == map(l_in)[i := v];

+

+procedure TransferIn({:linear "Node"} l1_in:lmap, d:Node);

+  requires dom(l1_in)[d];

+  modifies stack;

+  ensures  dom(stack) == dom(old(stack))[d := true];

+  ensures  map(stack) == map(old(stack))[d := map(l1_in)[d]];

+

+procedure TransferOut(d:Node);

+  requires dom(stack)[d];

+  modifies stack;

+  ensures  dom(stack) == dom(old(stack))[d := false];

+  ensures  map(stack) == map(old(stack));

+

+procedure New() returns ({:linear "Node"} l: lmap, d: Node);

+ensures dom(l)[d];

+

+const unique null: Node;

+

+var TOP: Node;

+var {:linear "Node"} stack: lmap;

+

+procedure {:yields} CAS(oldVal: Node, newVal: Node)

+returns (r: bool)

+{

+  r := (TOP == oldVal);

+  if (r) {

+    TOP := newVal;

+  }

+}

+

+procedure {:yields} push()

+{

+  var t, x: Node;

+  var g: bool;

+  var {:linear "Node"} x_lmap: lmap;

+

+  call x_lmap, x := New();

+

+  while(true)

+  {

+    t := TOP;		

+    call x_lmap := Store(x_lmap, x, t);

+    call g := CAS(t, x); 

+    if (g) { 

+      call TransferIn(x_lmap, x);

+      break; 

+    }

+  }

+}

+

+procedure {:yields} pop()

+{

+  var t, x: Node;

+  var g: bool;

+

+  while(true)

+  {

+    t := TOP;		

+    if (t == null)

+    {

+      return;

+    }

+    call x := Load(t);

+    call g := CAS(t, x); 

+    if (g) { 

+      call TransferOut(t);

+      break; 

+    }

+  }

+}
\ No newline at end of file