Merge

44 files changed, 719 insertions, 257 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 1dd350de..971e7271 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -30,52 +30,57 @@ namespace Microsoft.Boogie
             if (moverTypeChecker.procToActionInfo.Count == 0)

                 return;

 

+            List<ActionInfo> sortedByCreatedLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo));

+            sortedByCreatedLayerNum.Sort((x, y) => { return (x.createdAtLayerNum == y.createdAtLayerNum) ? 0 : (x.createdAtLayerNum < y.createdAtLayerNum) ? -1 : 1; });

+            List<ActionInfo> sortedByAvailableUptoLayerNum = new List<ActionInfo>(moverTypeChecker.procToActionInfo.Values.Where(x => x is AtomicActionInfo));

+            sortedByAvailableUptoLayerNum.Sort((x, y) => { return (x.availableUptoLayerNum == y.availableUptoLayerNum) ? 0 : (x.availableUptoLayerNum < y.availableUptoLayerNum) ? -1 : 1; });

+

             Dictionary<int, HashSet<AtomicActionInfo>> pools = new Dictionary<int, HashSet<AtomicActionInfo>>();

-            foreach (ActionInfo action in moverTypeChecker.procToActionInfo.Values)

+            int indexIntoSortedByCreatedLayerNum = 0;

+            int indexIntoSortedByAvailableUptoLayerNum = 0;

+            HashSet<AtomicActionInfo> currPool = new HashSet<AtomicActionInfo>();

+            while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)

             {

-                AtomicActionInfo atomicAction = action as AtomicActionInfo;

-                if (atomicAction == null) continue;

-                foreach (int layerNum in moverTypeChecker.AllLayerNums)

+                var currLayerNum = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum].createdAtLayerNum;

+                pools[currLayerNum] = new HashSet<AtomicActionInfo>(currPool);

+                while (indexIntoSortedByCreatedLayerNum < sortedByCreatedLayerNum.Count)

                 {

-                    if (action.createdAtLayerNum < layerNum && layerNum <= action.availableUptoLayerNum)

-                    {

-                        if (!pools.ContainsKey(layerNum))

-                        {

-                            pools[layerNum] = new HashSet<AtomicActionInfo>();

-                        }

-                        pools[layerNum].Add(atomicAction);

-                    }

+                    var actionInfo = sortedByCreatedLayerNum[indexIntoSortedByCreatedLayerNum] as AtomicActionInfo;

+                    if (actionInfo.createdAtLayerNum > currLayerNum) break;

+                    pools[currLayerNum].Add(actionInfo);

+                    indexIntoSortedByCreatedLayerNum++;

                 }

+                while (indexIntoSortedByAvailableUptoLayerNum < sortedByAvailableUptoLayerNum.Count)

+                {

+                    var actionInfo = sortedByAvailableUptoLayerNum[indexIntoSortedByAvailableUptoLayerNum] as AtomicActionInfo;

+                    if (actionInfo.availableUptoLayerNum > currLayerNum) break;

+                    pools[currLayerNum].Remove(actionInfo);

+                    indexIntoSortedByAvailableUptoLayerNum++;

+                }

+                currPool = pools[currLayerNum];

             }

 

             Program program = moverTypeChecker.program;

             MoverCheck moverChecking = new MoverCheck(linearTypeChecker, moverTypeChecker, decls);

-            foreach (int layerNum1 in pools.Keys)

+            foreach (int layerNum in pools.Keys)

             {

-                foreach (AtomicActionInfo first in pools[layerNum1])

+                foreach (AtomicActionInfo first in pools[layerNum])

                 {

                     Debug.Assert(first.moverType != MoverType.Top);

                     if (first.moverType == MoverType.Atomic)

                         continue;

-                    foreach (int layerNum2 in pools.Keys)

+                    foreach (AtomicActionInfo second in pools[layerNum])

                     {

-                        if (layerNum2 < layerNum1) continue;

-                        foreach (AtomicActionInfo second in pools[layerNum2])

+                        if (first.IsRightMover)

+                        {

+                            moverChecking.CreateCommutativityChecker(program, first, second);

+                            moverChecking.CreateGatePreservationChecker(program, second, first);

+                        }

+                        if (first.IsLeftMover)

                         {

-                            if (second.createdAtLayerNum < layerNum1)

-                            {

-                                if (first.IsRightMover)

-                                {

-                                    moverChecking.CreateCommutativityChecker(program, first, second);

-                                    moverChecking.CreateGatePreservationChecker(program, second, first);

-                                }

-                                if (first.IsLeftMover)

-                                {

-                                    moverChecking.CreateCommutativityChecker(program, second, first);

-                                    moverChecking.CreateGatePreservationChecker(program, first, second);

-                                    moverChecking.CreateFailurePreservationChecker(program, second, first);

-                                }

-                            }

+                            moverChecking.CreateCommutativityChecker(program, second, first);

+                            moverChecking.CreateGatePreservationChecker(program, first, second);

+                            moverChecking.CreateFailurePreservationChecker(program, second, first);

                         }

                     }

                 }

@@ -508,7 +513,7 @@ namespace Microsoft.Boogie
             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(Expr.Ident(x)));

+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(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, blocks);

             impl.Proc = proc;

@@ -551,7 +556,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));

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

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

-            program.GlobalVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(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;

@@ -599,7 +604,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));

             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(Expr.Ident(x)));

+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(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;

@@ -633,7 +638,7 @@ namespace Microsoft.Boogie
             blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));

             string checkerName = string.Format("NonBlockingChecker_{0}", second.proc.Name);

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

-            program.GlobalVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

+            moverTypeChecker.SharedVariables.Iter(x => globalVars.Add(Expr.Ident(x)));

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

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);

             impl.Proc = proc;

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index e485e1bc..dbd1dcbd 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -198,7 +198,7 @@ namespace Microsoft.Boogie
                 }

                 procMap[node] = proc;

                 proc.Modifies = new List<IdentifierExpr>();

-                moverTypeChecker.program.GlobalVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));

+                moverTypeChecker.SharedVariables.Iter(x => proc.Modifies.Add(Expr.Ident(x)));

             }

             return procMap[node];

         }

@@ -279,7 +279,7 @@ namespace Microsoft.Boogie
             this.yieldingProcs = duplicator.yieldingProcs;

             Program program = linearTypeChecker.program;

             globalMods = new List<IdentifierExpr>();

-            foreach (Variable g in program.GlobalVariables)

+            foreach (Variable g in moverTypeChecker.SharedVariables)

             {

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

             }

@@ -738,15 +738,16 @@ namespace Microsoft.Boogie
                     foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);

                 }

                 Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);

-                frame = new HashSet<Variable>(program.GlobalVariables);

+                frame = new HashSet<Variable>(moverTypeChecker.SharedVariables);

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

-                foreach (Variable v in program.GlobalVariables)

+                foreach (Variable v in moverTypeChecker.SharedVariables)

                 {

-                    if (moverTypeChecker.hideLayerNums[v] <= actionInfo.createdAtLayerNum || moverTypeChecker.introduceLayerNums[v] > actionInfo.createdAtLayerNum)

+                    if (moverTypeChecker.globalVarToSharedVarInfo[v].hideLayerNum <= actionInfo.createdAtLayerNum || 

+                        moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum > actionInfo.createdAtLayerNum)

                     {

                         frame.Remove(v);

                     }

-                    if (moverTypeChecker.introduceLayerNums[v] == actionInfo.createdAtLayerNum)

+                    if (moverTypeChecker.globalVarToSharedVarInfo[v].introLayerNum == actionInfo.createdAtLayerNum)

                     {

                         introducedVars.Add(v);

                     }

@@ -1159,7 +1160,7 @@ namespace Microsoft.Boogie
         public static void AddCheckers(LinearTypeChecker linearTypeChecker, MoverTypeChecker moverTypeChecker, List<Declaration> decls)

         {

             Program program = linearTypeChecker.program;

-            foreach (int layerNum in moverTypeChecker.AllLayerNums.Except(new int[] { 0 }))

+            foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))

             {

                 if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue;

 

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index d6ccce45..13356aff 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -22,12 +22,14 @@ namespace Microsoft.Boogie
         public Procedure proc;

         public int createdAtLayerNum;

         public int availableUptoLayerNum;

+        public bool hasImplementation;

 

         public ActionInfo(Procedure proc, int createdAtLayerNum, int availableUptoLayerNum)

         {

             this.proc = proc;

             this.createdAtLayerNum = createdAtLayerNum;

             this.availableUptoLayerNum = availableUptoLayerNum;

+            this.hasImplementation = false;

         }

 

         public virtual bool IsRightMover

@@ -199,12 +201,23 @@ namespace Microsoft.Boogie
         }

     }

 

+    public class SharedVariableInfo

+    {

+        public int introLayerNum;

+        public int hideLayerNum;

+

+        public SharedVariableInfo(int introLayerNum, int hideLayerNum)

+        {

+            this.introLayerNum = introLayerNum;

+            this.hideLayerNum = hideLayerNum;

+        }

+    }

+

     public class MoverTypeChecker : ReadOnlyVisitor

     {

         CheckingContext checkingContext;

         public int errorCount;

-        public Dictionary<Variable, int> introduceLayerNums;

-        public Dictionary<Variable, int> hideLayerNums;

+        public Dictionary<Variable, SharedVariableInfo> globalVarToSharedVarInfo;

         Procedure enclosingProc;

         Implementation enclosingImpl;

         public Dictionary<Procedure, ActionInfo> procToActionInfo;

@@ -215,6 +228,7 @@ namespace Microsoft.Boogie
         int maxLayerNum;

         public Dictionary<Absy, HashSet<int>> absyToLayerNums;

         HashSet<Variable> auxVars;

+        public int leastUnimplementedLayerNum;

 

         private static List<int> FindLayers(QKeyValue kv)

         {

@@ -249,20 +263,58 @@ namespace Microsoft.Boogie
             return MoverType.Top;

         }

 

-        private HashSet<int> allLayerNums;

-        public IEnumerable<int> AllLayerNums

+        public MoverTypeChecker(Program program)

+        {

+            this.auxVars = new HashSet<Variable>();

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

+            this.globalVarToSharedVarInfo = new Dictionary<Variable, SharedVariableInfo>();

+            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();

+            this.errorCount = 0;

+            this.checkingContext = new CheckingContext(null);

+            this.program = program;

+            this.enclosingProc = null;

+            this.enclosingImpl = null;

+            this.canAccessSharedVars = false;

+            this.canAccessAuxVars = false;

+            this.minLayerNum = int.MaxValue;

+            this.maxLayerNum = -1;

+            this.leastUnimplementedLayerNum = int.MaxValue;

+            foreach (var g in program.GlobalVariables)

+            {

+                List<int> layerNums = FindLayers(g.Attributes);

+                if (layerNums.Count == 0)

+                {

+                    // Cannot access atomic actions

+                }

+                else if (layerNums.Count == 1)

+                {

+                    this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], int.MaxValue);

+                }

+                else if (layerNums.Count == 2)

+                {

+                    this.globalVarToSharedVarInfo[g] = new SharedVariableInfo(layerNums[0], layerNums[1]);

+                }

+                else

+                {

+                    Error(g, "Too many layer numbers");

+                }

+            }

+        }

+        

+        private HashSet<int> allCreatedLayerNums;

+        public IEnumerable<int> AllCreatedLayerNums

         {

             get

             {

-                if (allLayerNums == null)

+                if (allCreatedLayerNums == null)

                 {

-                    allLayerNums = new HashSet<int>();

+                    allCreatedLayerNums = new HashSet<int>();

                     foreach (ActionInfo actionInfo in procToActionInfo.Values)

                     {

-                        allLayerNums.Add(actionInfo.createdAtLayerNum);

+                        allCreatedLayerNums.Add(actionInfo.createdAtLayerNum);

                     }

                 }

-                return allLayerNums;

+                return allCreatedLayerNums;

             }

         }

 

@@ -289,6 +341,11 @@ namespace Microsoft.Boogie
                     Error(proc, "Incorrect number of layers");

                     continue;

                 }

+                if (availableUptoLayerNum <= createdAtLayerNum)

+                {

+                    Error(proc, "Creation layer number must be less than the available upto layer number");

+                    continue;

+                }

                 foreach (Ensures e in proc.Ensures)

                 {

                     MoverType moverType = GetMoverType(e);

@@ -312,66 +369,69 @@ namespace Microsoft.Boogie
                     enclosingImpl = null;

                     base.VisitEnsures(e);

                     canAccessSharedVars = false;

-                    if (maxLayerNum <= createdAtLayerNum && availableUptoLayerNum <= minLayerNum)

+                    if (maxLayerNum > createdAtLayerNum)

                     {

-                        // ok

+                        Error(e, "A variable being accessed is introduced after this action is created");

                     }

-                    else

+                    else if (availableUptoLayerNum > minLayerNum)

                     {

                         Error(e, "A variable being accessed is hidden before this action becomes unavailable");

                     }

-

-                    procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);

+                    else

+                    {

+                        procToActionInfo[proc] = new AtomicActionInfo(proc, e, moverType, createdAtLayerNum, availableUptoLayerNum);

+                    }

                 }

+                if (errorCount > 0) continue;

                 if (!procToActionInfo.ContainsKey(proc))

                 {

                     procToActionInfo[proc] = new ActionInfo(proc, createdAtLayerNum, availableUptoLayerNum);

                 }

             }

             if (errorCount > 0) return;

-            this.VisitProgram(program);

-            if (errorCount > 0) return;

-            YieldTypeChecker.PerformYieldSafeCheck(this);

-        }

-

-        public MoverTypeChecker(Program program)

-        {

-            this.auxVars = new HashSet<Variable>();

-            this.absyToLayerNums = new Dictionary<Absy, HashSet<int>>();

-            this.introduceLayerNums = new Dictionary<Variable, int>();

-            this.hideLayerNums = new Dictionary<Variable, int>();

-            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();

-            this.errorCount = 0;

-            this.checkingContext = new CheckingContext(null);

-            this.program = program;

-            this.enclosingProc = null;

-            this.enclosingImpl = null;

-            this.canAccessSharedVars = false;

-            this.canAccessAuxVars = false;

-            this.minLayerNum = int.MaxValue;

-            this.maxLayerNum = -1;

-            foreach (var g in program.GlobalVariables)

+            foreach (var impl in program.Implementations)

             {

-                List<int> layerNums = FindLayers(g.Attributes);

-                if (layerNums.Count == 0)

+                if (!procToActionInfo.ContainsKey(impl.Proc)) continue;

+                procToActionInfo[impl.Proc].hasImplementation = true;

+            }

+            foreach (var proc in procToActionInfo.Keys)

+            {

+                ActionInfo actionInfo = procToActionInfo[proc];

+                if (actionInfo.hasImplementation) continue;

+                if (leastUnimplementedLayerNum == int.MaxValue)

                 {

-                    // Cannot access atomic actions

+                    leastUnimplementedLayerNum = actionInfo.createdAtLayerNum;

                 }

-                else if (layerNums.Count == 1)

+                else if (leastUnimplementedLayerNum == actionInfo.createdAtLayerNum)

                 {

-                    this.introduceLayerNums[g] = layerNums[0];

-                    this.hideLayerNums[g] = int.MaxValue;

+                    // do nothing

                 }

-                else if (layerNums.Count == 2)

+                else

                 {

-                    this.introduceLayerNums[g] = layerNums[0];

-                    this.hideLayerNums[g] = layerNums[1];

+                    Error(proc, "All unimplemented atomic actions must be created at the same layer");

                 }

-                else

+            }

+            foreach (var g in this.globalVarToSharedVarInfo.Keys)

+            {

+                var info = globalVarToSharedVarInfo[g];

+                if (!this.AllCreatedLayerNums.Contains(info.introLayerNum))

                 {

-                    Error(g, "Too many layer numbers");

+                    Error(g, "Variable must be introduced with creation of some atomic action");

+                }

+                if (info.hideLayerNum != int.MaxValue && !this.AllCreatedLayerNums.Contains(info.hideLayerNum))

+                {

+                    Error(g, "Variable must be hidden with creation of some atomic action");

                 }

             }

+            if (errorCount > 0) return;

+            this.VisitProgram(program);

+            if (errorCount > 0) return;

+            YieldTypeChecker.PerformYieldSafeCheck(this);

+        }

+

+        public IEnumerable<Variable> SharedVariables

+        {

+            get { return this.globalVarToSharedVarInfo.Keys;  }

         }

         

         public override Implementation VisitImplementation(Implementation node)

@@ -440,6 +500,10 @@ namespace Microsoft.Boogie
                     Error(node, "The callee is not available in the caller procedure");

                 }

             }

+            else

+            {

+                Error(node, "Yielding procedure can call only a yielding procedure");

+            }

             return base.VisitCallCmd(node);

         }

 

@@ -504,17 +568,21 @@ namespace Microsoft.Boogie
                 {

                     Error(node, "Shared variable can be accessed only in atomic actions or specifications");

                 }

-                else

+                else if (this.globalVarToSharedVarInfo.ContainsKey(node.Decl))

                 {

-                    if (hideLayerNums[node.Decl] < minLayerNum)

+                    if (this.globalVarToSharedVarInfo[node.Decl].hideLayerNum < minLayerNum)

                     {

-                        minLayerNum = hideLayerNums[node.Decl];

+                        minLayerNum = this.globalVarToSharedVarInfo[node.Decl].hideLayerNum;

                     }

-                    if (introduceLayerNums[node.Decl] > maxLayerNum)

+                    if (this.globalVarToSharedVarInfo[node.Decl].introLayerNum > maxLayerNum)

                     {

-                        maxLayerNum = introduceLayerNums[node.Decl];

+                        maxLayerNum = this.globalVarToSharedVarInfo[node.Decl].introLayerNum;

                     }

                 }

+                else

+                {

+                    Error(node, "Accessed shared variable must have layer annotation");

+                }

             }

             else if (node.Decl is LocalVariable && auxVars.Contains(node.Decl) && !canAccessAuxVars)

             {

@@ -581,7 +649,11 @@ namespace Microsoft.Boogie
             absyToLayerNums[node] = new HashSet<int>();

             foreach (int layerNum in attrs)

             {

-                if (layerNum > enclosingProcLayerNum)

+                if (layerNum == leastUnimplementedLayerNum || !AllCreatedLayerNums.Contains(layerNum))

+                {

+                    Error(node, "Illegal layer number");

+                }

+                else if (layerNum > enclosingProcLayerNum)

                 {

                     Error(node, "The layer cannot be greater than the layer of enclosing procedure");

                 }

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 8e844ede..95884626 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -136,12 +136,12 @@ namespace Microsoft.Boogie
         {

             foreach (var impl in moverTypeChecker.program.Implementations)

             {

-                if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc) || moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum == 0) continue;

+                if (!moverTypeChecker.procToActionInfo.ContainsKey(impl.Proc)) continue;

                 impl.PruneUnreachableBlocks();

                 Graph<Block> implGraph = Program.GraphFromImpl(impl);

                 implGraph.ComputeLoops();

                 int specLayerNum = moverTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum;

-                foreach (int layerNum in moverTypeChecker.AllLayerNums)

+                foreach (int layerNum in moverTypeChecker.AllCreatedLayerNums.Except(new int[] { moverTypeChecker.leastUnimplementedLayerNum }))

                 {

                     if (layerNum > specLayerNum) continue;

                     YieldTypeChecker executor = new YieldTypeChecker(moverTypeChecker, impl, layerNum, implGraph.Headers);

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 01212da1..682e058c 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1656,6 +1656,11 @@ namespace Microsoft.Boogie {
      {:subsumption n}

        Overrides the /subsumption command-line setting for this assertion.

 

+     {:split_here}

+       Verifies code leading to this point and code leading from this point

+       to the next split_here as separate pieces.  May help with timeouts.

+       May also occasionally double-report errors.

+

   ---- The end ---------------------------------------------------------------

 ");

     }

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 92be2e0a..8187db01 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -536,11 +536,11 @@ namespace Microsoft.Boogie
       }

     }

 

-    public static List<List<string>> LookForSnapshots(List<string> fileNames)

+    public static IList<IList<string>> LookForSnapshots(IList<string> fileNames)

     {

       Contract.Requires(fileNames != null);

 

-      var result = new List<List<string>>();

+      var result = new List<IList<string>>();

       for (int version = 0; true; version++)

       {

         var nextSnapshot = new List<string>();

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 7c6a3a9a..f431c3d5 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -211,28 +211,59 @@ namespace Microsoft.Boogie.SMTLib
 

     public bool Visit(VCExprNAry node, LineariserOptions options)

     {

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

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

-

-      VCExprOp op = node.Op;

-      Contract.Assert(op != null);

-

-      if (op.Equals(VCExpressionGenerator.AndOp) ||

-           op.Equals(VCExpressionGenerator.OrOp)) {

-        // handle these operators without recursion

+        VCExprOp op = node.Op;

+        Contract.Assert(op != null);

 

-        wr.Write("({0}",

-          op.Equals(VCExpressionGenerator.AndOp) ? "and" : "or");

-        foreach (var ch in node.UniformArguments) {

-          wr.Write("\n");

-          Linearise(ch, options);

+        var booleanOps = new HashSet<VCExprOp>();

+        booleanOps.Add(VCExpressionGenerator.NotOp);

+        booleanOps.Add(VCExpressionGenerator.ImpliesOp);

+        booleanOps.Add(VCExpressionGenerator.AndOp);

+        booleanOps.Add(VCExpressionGenerator.OrOp);

+        if (booleanOps.Contains(op))

+        {

+            Stack<VCExpr> exprs = new Stack<VCExpr>();

+            exprs.Push(node);

+            while (exprs.Count > 0)

+            {

+                VCExpr expr = exprs.Pop();

+                if (expr == null)

+                {

+                    wr.Write(")");

+                    continue;

+                }

+                wr.Write(" ");

+                VCExprNAry naryExpr = expr as VCExprNAry;

+                if (naryExpr == null || !booleanOps.Contains(naryExpr.Op))

+                {

+                    Linearise(expr, options);

+                    continue;

+                }

+                else if (naryExpr.Op.Equals(VCExpressionGenerator.NotOp))

+                {

+                    wr.Write("(not");

+                }

+                else if (naryExpr.Op.Equals(VCExpressionGenerator.ImpliesOp))

+                {

+                    wr.Write("(=>");

+                }

+                else if (naryExpr.Op.Equals(VCExpressionGenerator.AndOp))

+                {

+                    wr.Write("(and");

+                }

+                else 

+                {

+                    System.Diagnostics.Debug.Assert(naryExpr.Op.Equals(VCExpressionGenerator.OrOp));

+                    wr.Write("(or");

+                }

+                exprs.Push(null);

+                for (int i = naryExpr.Arity - 1; i >= 0; i--)

+                {

+                    exprs.Push(naryExpr[i]);

+                }

+            }

+            return true;

         }

-        wr.Write(")");

-

-        return true;

-      }

-

-      return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options);

+        return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options);

     }

 

     /////////////////////////////////////////////////////////////////////////////////////

diff --git a/Source/VCExpr/TermFormulaFlattening.cs b/Source/VCExpr/TermFormulaFlattening.cs
index 9198d753..7815413f 100644
--- a/Source/VCExpr/TermFormulaFlattening.cs
+++ b/Source/VCExpr/TermFormulaFlattening.cs
@@ -155,6 +155,12 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()))
 

     ////////////////////////////////////////////////////////////////////////////

 

+    public override bool AvoidVisit(VCExprNAry node, FlattenerState arg)

+    {

+        return node.Op.Equals(VCExpressionGenerator.AndOp) ||

+               node.Op.Equals(VCExpressionGenerator.OrOp);

+    }

+

     public override VCExpr Visit(VCExprNAry node, FlattenerState state){

 Contract.Requires(node != null);

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

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 628ebdf1..2326ba7a 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1087,6 +1087,12 @@ namespace Microsoft.Boogie.TypeErasure {
 

     ////////////////////////////////////////////////////////////////////////////

 

+    public override bool AvoidVisit(VCExprNAry node, VariableBindings arg)

+    {

+        return node.Op.Equals(VCExpressionGenerator.AndOp) ||

+               node.Op.Equals(VCExpressionGenerator.OrOp);

+    }

+

     public override VCExpr Visit(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires(bindings != null);

       Contract.Requires(node != null);

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 02220057..ad0c270d 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -288,14 +288,15 @@ namespace Microsoft.Boogie.VCExprAST {
            node.Op == VCExpressionGenerator.ImpliesOp)) {

         Contract.Assert(node.Op != null);

         VCExprOp op = node.Op;

-

-        IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);

-        enumerator.MoveNext();  // skip the node itself

-

+        HashSet<VCExprOp> ops = new HashSet<VCExprOp>();

+        ops.Add(VCExpressionGenerator.AndOp);

+        ops.Add(VCExpressionGenerator.OrOp);

+        ops.Add(VCExpressionGenerator.ImpliesOp);

+        IEnumerator enumerator = new VCExprNAryMultiUniformOpEnumerator(node, ops);

         while (enumerator.MoveNext()) {

-          VCExpr/*!*/ expr = cce.NonNull((VCExpr/*!*/)enumerator.Current);

+          VCExpr expr = cce.NonNull((VCExpr)enumerator.Current);

           VCExprNAry naryExpr = expr as VCExprNAry;

-          if (naryExpr == null || !naryExpr.Op.Equals(op)) {

+          if (naryExpr == null || !ops.Contains(naryExpr.Op)) {

             expr.Accept(this, arg);

           } else {

             StandardResult(expr, arg);

@@ -433,6 +434,28 @@ namespace Microsoft.Boogie.VCExprAST {
     }

   }

 

+  public class VCExprNAryMultiUniformOpEnumerator : VCExprNAryEnumerator

+  {

+      private readonly HashSet<VCExprOp> Ops;

+      [ContractInvariantMethod]

+      void ObjectInvariant()

+      {

+          Contract.Invariant(Ops != null);

+      }

+

+      public VCExprNAryMultiUniformOpEnumerator(VCExprNAry completeExpr, HashSet<VCExprOp> ops)

+          : base(completeExpr)

+      {

+          Contract.Requires(completeExpr != null);

+

+          this.Ops = ops;

+      }

+      protected override bool Descend(VCExprNAry expr)

+      {

+          return Ops.Contains(expr.Op) && expr.TypeParamArity == 0;

+      }

+  }

+

   //////////////////////////////////////////////////////////////////////////////

   // Visitor that knows about the variables bound at each location in a VCExpr

 

@@ -836,11 +859,14 @@ namespace Microsoft.Boogie.VCExprAST {
         NAryExprTodoStack.Push(exprTodo[i]);

     }

 

+    public virtual bool AvoidVisit(VCExprNAry node, Arg arg)

+    {

+        return true;

+    }

+

     public virtual VCExpr Visit(VCExprNAry node, Arg arg) {

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

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

-      VCExprOp/*!*/ op = node.Op;

-      Contract.Assert(op != null);

       int initialStackSize = NAryExprTodoStack.Count;

       int initialResultStackSize = NAryExprResultStack.Count;

 

@@ -851,10 +877,10 @@ namespace Microsoft.Boogie.VCExprAST {
         Contract.Assert(subExpr != null);

 

         if (Object.ReferenceEquals(subExpr, CombineResultsMarker)) {

-          //

           // assemble a result

           VCExprNAry/*!*/ originalExpr = (VCExprNAry)NAryExprTodoStack.Pop();

           Contract.Assert(originalExpr != null);

+          VCExprOp/*!*/ op = originalExpr.Op;

           bool changed = false;

           List<VCExpr/*!*/>/*!*/ newSubExprs = new List<VCExpr/*!*/>();

 

@@ -870,8 +896,8 @@ namespace Microsoft.Boogie.VCExprAST {
           //

         } else {

           //

-          VCExprNAry narySubExpr = subExpr as VCExprNAry;

-          if (narySubExpr != null && narySubExpr.Op.Equals(op) &&

+            VCExprNAry narySubExpr = subExpr as VCExprNAry;

+          if (narySubExpr != null && this.AvoidVisit(narySubExpr, arg) &&

             // as in VCExprNAryUniformOpEnumerator, all expressions with

             // type parameters are allowed to be inspected more closely

               narySubExpr.TypeParamArity == 0) {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 5e83a337..8a549e9d 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1056,6 +1056,141 @@ namespace VC {
         throw new cce.UnreachableException();

       }

 

+      /// <summary>

+      /// Starting from the 0-index "split_here" annotation in begin, verifies until it reaches a subsequent "split_here" annotation

+      /// Returns a list of blocks where all code not verified has asserts converted into assumes

+      /// </summary>

+      /// <param name="blocks">Implementation's collection of blocks</param>

+      /// <param name="begin">Block containing the first split_here from which to start verifying</param>

+      /// <param name="begin_split_id">0-based ID of the "split_here" annotation within begin at which to start verifying</param>

+      /// <param name="blockInternalSplit">True if the entire split is contained within block begin</param>

+      /// <param name="endPoints">Set of all blocks containing a "split_here" annotation</param>

+      /// <returns></returns>

+      // Note: Current implementation may over report errors.

+      //       For example, if the control flow graph is a diamond (e.g., A -> B, C, B->D, C->D),

+      //       and there is a split in B and an error in D, then D will be verified twice and hence report the error twice.

+      //       Best solution may be to memoize blocks that have been fully verified and be sure not to verify them again

+      private static List<Block> DoManualSplit(List<Block> blocks, Block begin, int begin_split_id, bool blockInternalSplit, IEnumerable<Block> endPoints) {

+        // Compute the set of blocks reachable from begin but not included in endPoints.  These will be verified in their entirety.

+        var blocksToVerifyEntirely = new HashSet<Block>();

+        var reachableEndPoints = new HashSet<Block>();  // Reachable end points will be verified up to their first split point

+        var todo = new Stack<Block>();

+        todo.Push(begin);

+        while (todo.Count > 0) {

+          var currentBlock = todo.Pop();

+          if (blocksToVerifyEntirely.Contains(currentBlock)) continue;

+          blocksToVerifyEntirely.Add(currentBlock);

+          var exit = currentBlock.TransferCmd as GotoCmd;

+          if (exit != null)

+            foreach (Block targetBlock in exit.labelTargets) {

+              if (!endPoints.Contains(targetBlock)) {

+                todo.Push(targetBlock);

+              } else {

+                reachableEndPoints.Add(targetBlock);

+              }

+            }

+              

+        }

+        blocksToVerifyEntirely.Remove(begin);

+

+        // Convert assumes to asserts in "unreachable" blocks, including portions of blocks containing "split_here"

+        var newBlocks = new List<Block>(blocks.Count());  // Copies of the original blocks

+        var duplicator = new Duplicator();

+        var oldToNewBlockMap = new Dictionary<Block, Block>(blocks.Count());  // Maps original blocks to their new copies in newBlocks

+

+        foreach (var currentBlock in blocks) {

+          var newBlock = (Block)duplicator.VisitBlock(currentBlock);

+          oldToNewBlockMap[currentBlock] = newBlock;          

+          newBlocks.Add(newBlock);

+

+          if (!blockInternalSplit && blocksToVerifyEntirely.Contains(currentBlock)) continue;  // All reachable blocks must be checked in their entirety, so don't change anything

+          // Otherwise, we only verify a portion of the current block, so we'll need to look at each of its commands                 

+

+          // !verify -> convert assert to assume

+          var verify = (currentBlock == begin && begin_split_id == -1) // -1 tells us to start verifying from the very beginning (i.e., there is no split in the begin block)

+                      || (reachableEndPoints.Contains(currentBlock)    // This endpoint is reachable from begin, so we verify until we hit the first split point

+                          && !blockInternalSplit);                     // Don't bother verifying if all of the splitting is within the begin block

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

+          var split_here_count = 0;

+

+          foreach (Cmd c in currentBlock.Cmds) {

+            var p = c as PredicateCmd;

+            if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "split_here")) {

+              if (currentBlock == begin) { // Verify everything between the begin_split_id we were given and the next split

+                if (split_here_count == begin_split_id) {

+                  verify = true;

+                } else if (split_here_count == begin_split_id + 1) {

+                  verify = false;

+                }

+              } else {  // We're in an endPoint so we stop verifying as soon as we hit a "split_here"

+                verify = false;

+              }

+              split_here_count++;              

+            }

+              

+            var asrt = c as AssertCmd;

+            if (verify || asrt == null)

+              newCmds.Add(c);

+            else

+              newCmds.Add(AssertTurnedIntoAssume(asrt));

+          }

+

+          newBlock.Cmds = newCmds;

+        }

+

+        // Patch the edges between the new blocks

+        foreach (var oldBlock in blocks) {

+          if (oldBlock.TransferCmd is ReturnCmd) { continue; }

+          var gotoCmd = (GotoCmd)oldBlock.TransferCmd;

+          var newLabelTargets = new List<Block>(gotoCmd.labelTargets.Count());

+          var newLabelNames = new List<string>(gotoCmd.labelTargets.Count());

+          foreach (var target in gotoCmd.labelTargets) {

+            newLabelTargets.Add(oldToNewBlockMap[target]);

+            newLabelNames.Add(oldToNewBlockMap[target].Label);

+          }

+          oldToNewBlockMap[oldBlock].TransferCmd = new GotoCmd(gotoCmd.tok, newLabelNames, newLabelTargets);

+        }

+

+        return newBlocks;

+      }

+

+      public static List<Split/*!*/> FindManualSplits(Implementation/*!*/ impl, Dictionary<TransferCmd, ReturnCmd>/*!*/ gotoCmdOrigins, VCGen/*!*/ par) {

+        Contract.Requires(impl != null);

+        Contract.Ensures(Contract.Result<List<Split>>() == null || cce.NonNullElements(Contract.Result<List<Split>>()));

+

+        var splitPoints = new Dictionary<Block,int>();

+        foreach (var b in impl.Blocks) {

+          foreach (Cmd c in b.Cmds) {

+            var p = c as PredicateCmd;

+            if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "split_here")) {

+              int count;

+              splitPoints.TryGetValue(b, out count);

+              splitPoints[b] = count + 1;

+            }

+          }

+        }

+

+        if (splitPoints.Count() == 0) { // No manual split points here

+          return null;

+        }

+

+        List<Split> splits = new List<Split>();

+        Block entryPoint = impl.Blocks[0];

+        var newEntryBlocks = DoManualSplit(impl.Blocks, entryPoint, -1, splitPoints.Keys.Contains(entryPoint), splitPoints.Keys);

+        splits.Add(new Split(newEntryBlocks, gotoCmdOrigins, par, impl));   // REVIEW: Does gotoCmdOrigins need to be changed at all?        

+

+        foreach (KeyValuePair<Block,int> pair in splitPoints) {

+          for (int i = 0; i < pair.Value; i++) {

+            bool blockInternalSplit = i < pair.Value - 1;   // There's at least one more split, after this one, in the current block

+            var newBlocks = DoManualSplit(impl.Blocks, pair.Key, i, blockInternalSplit, splitPoints.Keys);

+            Split s = new Split(newBlocks, gotoCmdOrigins, par, impl);   // REVIEW: Does gotoCmdOrigins need to be changed at all?

+            splits.Add(s);

+          }

+        }

+

+        return splits;

+      }

+

       public static List<Split/*!*/>/*!*/ DoSplit(Split initial, double max_cost, int max) {

         Contract.Requires(initial != null);

         Contract.Ensures(cce.NonNullElements(Contract.Result<List<Split>>()));

@@ -1639,7 +1774,14 @@ namespace VC {
       Stack<Split> work = new Stack<Split>();

       List<Split> currently_running = new List<Split>();

       ResetPredecessors(impl.Blocks);

-      work.Push(new Split(impl.Blocks, gotoCmdOrigins, this, impl));

+      List<Split> manual_splits = Split.FindManualSplits(impl, gotoCmdOrigins, this);

+      if (manual_splits != null) {

+        foreach (var split in manual_splits) {

+          work.Push(split);

+        }

+      } else {

+        work.Push(new Split(impl.Blocks, gotoCmdOrigins, this, impl));

+      }

 

       bool keep_going = max_kg_splits > 1;

       int total = 0;

@@ -2710,6 +2852,7 @@ namespace VC {
           }

         }

 

+        // Compute the set of blocks reachable from blocks containing "start_checking_here"

         var blocksToCheck = new HashSet<Block>();

         foreach (var b in startPoints) {

           var todo = new Stack<Block>();

@@ -2726,9 +2869,10 @@ namespace VC {
           }

           if (!wasThere) blocksToCheck.Remove(b);

         }

-

+        

+        // Convert asserts to assumes in "unreachable" blocks, as well as in portions of blocks before we reach "start_checking_here"

         foreach (var b in impl.Blocks) {

-          if (blocksToCheck.Contains(b)) continue;

+          if (blocksToCheck.Contains(b)) continue;  // All reachable blocks must be checked in their entirety, so don't change anything

           var newCmds = new List<Cmd>();

           var copyMode = false;

           foreach (Cmd c in b.Cmds) {

diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index 57080cb8..5c936dd0 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -65,9 +65,11 @@ procedure {:yields} {:layer 1} D()
     yield;

 }

 

-procedure E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)

+procedure {:yields} {:layer 1} E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)

 {

+    yield;

     c := a;

+    yield;

 }

 

 procedure {:yields} {:layer 0} F({:linear_in "D"} a: X) returns ({:linear "D"} c: X);

diff --git a/Test/linear/typecheck.bpl.expect b/Test/linear/typecheck.bpl.expect
index dddbd163..5466fe62 100644
--- a/Test/linear/typecheck.bpl.expect
+++ b/Test/linear/typecheck.bpl.expect
@@ -1,16 +1,16 @@
-typecheck.bpl(33,9): Error: Only simple assignment allowed on linear variable b
-typecheck.bpl(35,6): Error: Only variable can be assigned to linear variable a
-typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a
-typecheck.bpl(41,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D
-typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment
-typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter
-typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter b
-typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same
-typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same
-typecheck.bpl(59,4): Error: Only a linear argument can be passed to linear parameter a
-typecheck.bpl(64,4): Error: Linear variable a can occur only once as an input parameter of a parallel call
-typecheck.bpl(71,0): Error: Output variable d must be available at a return
-typecheck.bpl(80,0): Error: Global variable g must be available at a return
-typecheck.bpl(85,7): Error: unavailable source for a linear read
-typecheck.bpl(86,0): Error: Output variable r must be available at a return
-15 type checking errors detected in typecheck.bpl
+typecheck.bpl(33,9): Error: Only simple assignment allowed on linear variable b

+typecheck.bpl(35,6): Error: Only variable can be assigned to linear variable a

+typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a

+typecheck.bpl(41,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D

+typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment

+typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter

+typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter b

+typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same

+typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same

+typecheck.bpl(59,4): Error: Only a linear argument can be passed to linear parameter a

+typecheck.bpl(64,4): Error: Linear variable a can occur only once as an input parameter of a parallel call

+typecheck.bpl(73,0): Error: Output variable d must be available at a return

+typecheck.bpl(82,0): Error: Global variable g must be available at a return

+typecheck.bpl(87,7): Error: unavailable source for a linear read

+typecheck.bpl(88,0): Error: Output variable r must be available at a return

+15 type checking errors detected in typecheck.bpl

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 703456ef..f439b607 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -24,6 +24,14 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
     (ghostLock == nil <==> currsize == newsize)

 }

 

+procedure {:yields} {:layer 1} Yield()

+requires {:layer 1} Inv(ghostLock, currsize, newsize);

+ensures {:layer 1} Inv(ghostLock, currsize, newsize);

+{

+   yield;

+   assert {:layer 1} Inv(ghostLock, currsize, newsize);

+}

+

 procedure {:yields} {:layer 1} YieldToReadCache({:linear "tid"} tid: X)

 requires {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil;

 ensures {:layer 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;

@@ -40,18 +48,21 @@ ensures {:layer 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(
     assert {:layer 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;

 }

 

-procedure Allocate({:linear_in "tid"} xls': [X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X)

 ensures {:layer 1} xl != nil;

+{

+    yield;

+    call xl := AllocateLow();

+    yield;

+}

 

-procedure {:yields} {:layer 1} main({:linear_in "tid"} xls':[X]bool)

-requires {:layer 1} xls' == mapconstbool(true);

+procedure {:yields} {:layer 1} main({:linear_in "tid"} xls: [X]bool)

+requires {:layer 1} xls == mapconstbool(true);

 {

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

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

 

     yield;

 

-    xls := xls';

     call Init(xls);

     

     yield;

@@ -60,7 +71,7 @@ requires {:layer 1} xls' == mapconstbool(true);
     while (*)

     invariant {:layer 1} Inv(ghostLock, currsize, newsize);

     {

-        call xls, tid := Allocate(xls);

+        par tid := Allocate() | Yield();

 	yield;

     	assert {:layer 1} Inv(ghostLock, currsize, newsize);

         async call Thread(tid);

@@ -168,7 +179,7 @@ ensures {:layer 1} Inv(ghostLock, currsize, newsize);
     par YieldToReadCache(tid);

 }

 

-procedure {:yields} {:layer 0,1} Init({:linear "tid"} xls:[X]bool);

+procedure {:yields} {:layer 0,1} Init({:linear_in "tid"} xls:[X]bool);

 ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;

 

 procedure {:yields} {:layer 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int);

@@ -194,3 +205,6 @@ ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; retur
 

 procedure {:yields} {:layer 0,1} release({:linear "tid"} tid: X);

 ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|;

+

+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: X);

+ensures {:atomic} |{ A: assume tid != nil; return true; }|;

diff --git a/Test/og/DeviceCache.bpl.expect b/Test/og/DeviceCache.bpl.expect
index 9e5be400..9ec7a92d 100644
--- a/Test/og/DeviceCache.bpl.expect
+++ b/Test/og/DeviceCache.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 28 verified, 0 errors

+Boogie program verifier finished with 30 verified, 0 errors

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 04255cf2..7345b5b2 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -11,8 +11,13 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
   MapConstBool(false)[x := true]

 }

 

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

-ensures {:layer 1} xls != nil;

+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: X)

+ensures {:layer 1} xl != nil;

+{

+    yield;

+    call xl := AllocateLow();

+    yield;

+}

 

 procedure {:yields} {:layer 1} main()

 {

@@ -38,6 +43,9 @@ ensures {:atomic} |{A: l := nil; return true; }|;
 procedure {:yields} {:layer 0,1} Set(val: int);

 ensures {:atomic} |{A: x := val; return true; }|;

 

+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xl: X);

+ensures {:atomic} |{ A: assume xl != nil; return true; }|;

+

 procedure {:yields} {:layer 1} foo({:linear_in "tid"} tid': X, val: int)

 requires {:layer 1} tid' != nil;

 {

diff --git a/Test/og/FlanaganQadeer.bpl.expect b/Test/og/FlanaganQadeer.bpl.expect
index 5b2909f1..fef5ddc0 100644
--- a/Test/og/FlanaganQadeer.bpl.expect
+++ b/Test/og/FlanaganQadeer.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 3 verified, 0 errors

+Boogie program verifier finished with 4 verified, 0 errors

diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index 0228adc9..7767e179 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -15,7 +15,12 @@ function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
 

 var {:layer 0,1} a:[Tid]int;

 

-procedure Allocate() returns ({:linear "tid"} tid:Tid); 

+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: Tid)

+{

+    yield;

+    call tid := AllocateLow();

+    yield;

+}

 

 procedure {:yields} {:layer 1} main() { 

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

@@ -55,3 +60,6 @@ ensures {:atomic}
 |{A:

   a[tid] := val; return true;

 }|;

+

+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: Tid);

+ensures {:atomic} |{ A: return true; }|;

diff --git a/Test/og/Program4.bpl.expect b/Test/og/Program4.bpl.expect
index 3de74d3e..5b2909f1 100644
--- a/Test/og/Program4.bpl.expect
+++ b/Test/og/Program4.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 3 verified, 0 errors

diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl
index af87eac5..55e4219f 100644
--- a/Test/og/Program5.bpl
+++ b/Test/og/Program5.bpl
@@ -5,8 +5,8 @@ const unique nil: Tid;
 function {:builtin "MapConst"} MapConstBool(bool): [Tid]bool;

 function {:builtin "MapOr"} MapOr([Tid]bool, [Tid]bool) : [Tid]bool;

 

-var {:layer 0,3} Color:int;

-var {:layer 0,3} lock:Tid;

+var {:layer 0} Color:int;

+var {:layer 0} lock:Tid;

 

 function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool

 {

@@ -72,6 +72,6 @@ procedure {:yields} {:layer 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:
 procedure {:yields} {:layer 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int);

   ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|;

 

-procedure {:yields} {:layer 1,2} GetColorNoLock() returns (col:int);

+procedure {:yields} {:layer 0,2} GetColorNoLock() returns (col:int);

   ensures {:atomic} |{A: col := Color; return true;}|;

 

diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index 744029f1..c826b810 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -18,15 +18,6 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
   x

 }

 

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

-ensures {:layer 1} xls != 0;

-

-procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);

-ensures {:layer 1} xls == mapconstbool(true);

-

-procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

-ensures {:layer 1} xls == mapconstbool(true);

-

 var {:layer 0,1} g: int;

 var {:layer 0,1} h: int;

 

@@ -36,14 +27,23 @@ ensures {:atomic} |{A: g := val; return true; }|;
 procedure {:yields} {:layer 0,1} SetH(val:int);

 ensures {:atomic} |{A: h := val; return true; }|;

 

-procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int)

+ensures {:layer 1} xl != 0;

+{

+    yield;

+    call xl := AllocateLow();

+    yield;

+}

+

+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int);

+ensures {:atomic} |{ A: assume xls != 0; return true; }|;

+

+procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int)

+requires {:layer 1} x == mapconstbool(true);

+requires {:layer 1} y == mapconstbool(true);

 {

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

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

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

     tid_out := tid_in;    

-    call x := Allocate_1();

-    call y := Allocate_2();

 

     yield;

     call SetG(0);

diff --git a/Test/og/akash.bpl.expect b/Test/og/akash.bpl.expect
index 5b2909f1..fef5ddc0 100644
--- a/Test/og/akash.bpl.expect
+++ b/Test/og/akash.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 3 verified, 0 errors

+Boogie program verifier finished with 4 verified, 0 errors

diff --git a/Test/og/chris.bpl b/Test/og/chris.bpl
new file mode 100644
index 00000000..b54292ef
--- /dev/null
+++ b/Test/og/chris.bpl
@@ -0,0 +1,28 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+var{:layer 1} x:int;

+

+procedure{:yields}{:layer 2} Havoc()

+  ensures{:atomic} |{ A: return true; }|;

+{

+  yield;

+}

+

+procedure{:yields}{:layer 1} Recover()

+  ensures{:atomic} |{ A: assert x == 5; return true; }|;

+{

+  yield;

+}

+

+procedure{:yields}{:layer 3} P()

+  ensures{:atomic} |{ A: return true; }|;

+  requires{:layer 2,3} x == 5;

+  ensures {:layer 2,3} x == 5;

+{

+

+  yield; assert{:layer 2,3} x == 5;

+  call Havoc();

+  yield; assert{:layer 3} x == 5;

+  call Recover();

+  yield; assert{:layer 2,3} x == 5;

+}

diff --git a/Test/og/chris.bpl.expect b/Test/og/chris.bpl.expect
new file mode 100644
index 00000000..be6b95ba
--- /dev/null
+++ b/Test/og/chris.bpl.expect
@@ -0,0 +1,2 @@
+

+Boogie program verifier finished with 6 verified, 0 errors

diff --git a/Test/og/chris2.bpl b/Test/og/chris2.bpl
new file mode 100644
index 00000000..73f112ed
--- /dev/null
+++ b/Test/og/chris2.bpl
@@ -0,0 +1,34 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+var{:layer 20} x:int;

+

+procedure{:yields}{:layer 20,25} p_gt1_lower();

+  ensures{:both}

+  |{

+    A:

+    x := x + 1;

+    return true;

+  }|;

+

+procedure{:yields}{:layer 25,40} p_gt1()

+  ensures{:both}

+  |{

+    A:

+    x := x + 1;

+    return true;

+  }|;

+{

+  yield;

+  call p_gt1_lower();

+  yield;

+}

+

+procedure{:yields}{:layer 20,40} p_gt2();

+  ensures{:both}

+  |{

+    A:

+    assert x == 0;

+    return true;

+  }|;

+

+

diff --git a/Test/og/chris2.bpl.expect b/Test/og/chris2.bpl.expect
new file mode 100644
index 00000000..2bf339f7
--- /dev/null
+++ b/Test/og/chris2.bpl.expect
@@ -0,0 +1,18 @@
+(0,0): Error BP5003: A postcondition might not hold on this return path.

+chris2.bpl(30,5): Related location: Gate not preserved by p_gt1_lower

+Execution trace:

+    (0,0): this_A

+(0,0): Error BP5003: A postcondition might not hold on this return path.

+(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1_lower

+Execution trace:

+    (0,0): this_A

+(0,0): Error BP5003: A postcondition might not hold on this return path.

+chris2.bpl(30,5): Related location: Gate not preserved by p_gt1

+Execution trace:

+    (0,0): this_A

+(0,0): Error BP5003: A postcondition might not hold on this return path.

+(0,0): Related location: Gate failure of p_gt2 not preserved by p_gt1

+Execution trace:

+    (0,0): this_A

+

+Boogie program verifier finished with 1 verified, 4 errors

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 73849250..e481291a 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -23,10 +23,21 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
 var {:layer 0,1} x: int;

 var {:layer 0,1} l: [X]bool;

 

-procedure Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

-ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

 

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

+procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool)

+ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

+{

+  yield;

+  call xls1, xls2 := SplitLow(xls);

+  yield;

+}

+

+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: [X]bool)

+{

+  yield;

+  call xls := AllocateLow();

+  yield;

+}

 

 procedure {:yields} {:layer 0,1} Set(v: int);

 ensures {:atomic} |{A: x := v; return true; }|;

@@ -37,6 +48,11 @@ ensures {:atomic} |{A: assume l == None(); l := tidls; return true; }|;
 procedure {:yields} {:layer 0,1} Unlock();

 ensures {:atomic} |{A: l := None(); return true; }|;

 

+procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

+ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|;

+

+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: [X]bool);

+ensures {:atomic} |{ A: return true; }|;

 

 procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool) 

 requires {:layer 1} tidls' != None() && xls' == All();

diff --git a/Test/og/linear-set.bpl.expect b/Test/og/linear-set.bpl.expect
index 3de74d3e..fef5ddc0 100644
--- a/Test/og/linear-set.bpl.expect
+++ b/Test/og/linear-set.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 4 verified, 0 errors

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 81d30521..24d8a13a 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -24,11 +24,21 @@ var {:layer 0,1} x: int;
 var {:layer 0,1} l: X;

 const nil: X;

 

-procedure Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

-ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

+procedure {:yields} {:layer 1} Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool)

+ensures {:layer 1} xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();

+{

+  yield;

+  call xls1, xls2 := SplitLow(xls);

+  yield;

+}

 

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

-ensures xls != nil;

+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xls: X)

+ensures {:layer 1} xls != nil;

+{

+  yield;

+  call xls := AllocateLow();

+  yield;

+}

 

 procedure {:yields} {:layer 0,1} Set(v: int);

 ensures {:atomic} |{A: x := v; return true; }|;

@@ -39,6 +49,12 @@ ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|;
 procedure {:yields} {:layer 0,1} Unlock();

 ensures {:atomic} |{A: l := nil; return true; }|;

 

+procedure {:yields} {:layer 0,1} SplitLow({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);

+ensures {:atomic} |{ A: assume xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None(); return true; }|;

+

+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: X);

+ensures {:atomic} |{ A: assume xls != nil; return true; }|;

+

 procedure {:yields} {:layer 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool) 

 requires {:layer 1} tidls' != nil && xls' == All();

 {

diff --git a/Test/og/linear-set2.bpl.expect b/Test/og/linear-set2.bpl.expect
index 3de74d3e..fef5ddc0 100644
--- a/Test/og/linear-set2.bpl.expect
+++ b/Test/og/linear-set2.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 2 verified, 0 errors

+Boogie program verifier finished with 4 verified, 0 errors

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 308e4b8b..7fb0a081 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -63,7 +63,7 @@ ensures {:both} |{ A:
                     }|;

 

 

-procedure {:yields} {:layer 0} setEltToNull(j : int, {:linear "tid"} tid: X);

+procedure {:yields} {:layer 0,2} setEltToNull(j : int, {:linear "tid"} tid: X);

 ensures {:left} |{ A: 

                      assert owner[j] == tid;

                      assert 0 <= j && j < max;

@@ -75,7 +75,7 @@ ensures {:left} |{ A:
                      return true;

                     }|;

 

-procedure {:yields} {:layer 0} setValid(j : int, {:linear "tid"} tid: X);

+procedure {:yields} {:layer 0,2} setValid(j : int, {:linear "tid"} tid: X);

 ensures {:both} |{ A: 

                      assert 0 <= j && j < max;

                      assert lock[j] == tid;

@@ -86,7 +86,7 @@ ensures {:both} |{ A:
                      return true;

                     }|;

 

-procedure {:yields} {:layer 0} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);

+procedure {:yields} {:layer 0,2} isEltThereAndValid(j : int, x : int, {:linear "tid"} tid: X) returns (fnd:bool);

 ensures {:both} |{ A: 

                        assert 0 <= j && j < max;

                        assert lock[j] == tid;

@@ -95,7 +95,7 @@ ensures {:both} |{ A:
                        return true;

                     }|;

 

-procedure {:yields} {:layer 1} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)

+procedure {:yields} {:layer 1,2} FindSlot(x : int, {:linear "tid"} tid: X) returns (r : int)

 requires {:layer 1} Inv(valid, elt, owner) && x != null && tid != nil && tid != done; 

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

 ensures {:right}  |{   A: assert tid != nil && tid != done; 

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index a6b50215..b80b6315 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -9,10 +9,6 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
   x

 }

 

-procedure Allocate_Perm({:linear_in "Perm"} Permissions: [int]bool) returns ({:linear "Perm"} xls: [int]bool);

-requires Permissions == mapconstbool(true);

-ensures xls == mapconstbool(true);

-

 procedure {:yields} {:layer 1} PB({:linear_in "Perm"} permVar_in:[int]bool)

 requires {:layer 1} permVar_in[0] && g == 0;

 {

@@ -31,14 +27,11 @@ requires {:layer 1} permVar_in[0] && g == 0;
 }

 

 procedure {:yields} {:layer 1} Main({:linear_in "Perm"} Permissions: [int]bool)

-requires {:layer 0,1} Permissions == mapconstbool(true);

+requires {:layer 1} Permissions == mapconstbool(true);

 {

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

-

-  call permVar_out := Allocate_Perm(Permissions);

   yield;

   call SetG(0);

-  async call PB(permVar_out);

+  async call PB(Permissions);

   yield;

 }

 

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 4f2cbd5b..c28edf2b 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -8,7 +8,12 @@ function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
   MapConstBool(false)[x := true]

 }

 

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

+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)

+{

+    yield;

+    call tid := AllocateLow();

+    yield;

+}

 

 procedure {:yields} {:layer 0,1} Write(idx: int, val: int);

 ensures {:atomic} |{A: a[idx] := val; return true; }|;

@@ -48,4 +53,7 @@ ensures {:layer 1} old(a)[i] == a[i];
 {

     yield;

     assert {:layer 1} old(a)[i] == a[i];

-}
\ No newline at end of file
+}

+

+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);

+ensures {:atomic} |{ A: return true; }|;

diff --git a/Test/og/parallel2.bpl.expect b/Test/og/parallel2.bpl.expect
index fef5ddc0..05d394c7 100644
--- a/Test/og/parallel2.bpl.expect
+++ b/Test/og/parallel2.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 4 verified, 0 errors

+Boogie program verifier finished with 5 verified, 0 errors

diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index 41d45b79..f06ff4b8 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -2,7 +2,12 @@
 // RUN: %diff "%s.expect" "%t"

 var {:layer 0,1} a:int;

 

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

+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)

+{

+    yield;

+    call tid := AllocateLow();

+    yield;

+}

 

 function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

 function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

@@ -35,3 +40,6 @@ procedure {:yields} {:layer 1} Yield()
 {

   yield;

 }

+

+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);

+ensures {:atomic} |{ A: return true; }|;

diff --git a/Test/og/parallel4.bpl.expect b/Test/og/parallel4.bpl.expect
index 0bef8d9e..eaead450 100644
--- a/Test/og/parallel4.bpl.expect
+++ b/Test/og/parallel4.bpl.expect
@@ -1,6 +1,6 @@
-parallel4.bpl(26,3): Error BP5001: This assertion might not hold.

+parallel4.bpl(31,3): Error BP5001: This assertion might not hold.

 Execution trace:

     (0,0): og_init

     (0,0): anon01

 

-Boogie program verifier finished with 2 verified, 1 error

+Boogie program verifier finished with 3 verified, 1 error

diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index bed51241..87afc888 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -2,7 +2,12 @@
 // RUN: %diff "%s.expect" "%t"

 var {:layer 0,1} a:[int]int;

 

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

+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} tid: int)

+{

+    yield;

+    call tid := AllocateLow();

+    yield;

+}

 

 function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

 function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

@@ -48,4 +53,7 @@ ensures {:layer 1} old(a)[i] == a[i];
 {

     yield;

     assert {:layer 1} old(a)[i] == a[i];

-}
\ No newline at end of file
+}

+

+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} tid: int);

+ensures {:atomic} |{ A: return true; }|;

diff --git a/Test/og/parallel5.bpl.expect b/Test/og/parallel5.bpl.expect
index fef5ddc0..05d394c7 100644
--- a/Test/og/parallel5.bpl.expect
+++ b/Test/og/parallel5.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 4 verified, 0 errors

+Boogie program verifier finished with 5 verified, 0 errors

diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index f0de76d5..5bc75324 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -10,33 +10,25 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
   x

 }

 

-procedure Split({:linear_in "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1: [int]bool, {:linear "Perm"} xls2: [int]bool);

-  ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);

-

-

 procedure {:yields} {:layer 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)

-   free requires {:layer 1} permVar_in == ch_mapconstbool(true);

-   free requires {:layer 1} permVar_in[0];

-   free requires {:layer 1} x == 0;

+   requires {:layer 1} permVar_in == ch_mapconstbool(true);

+   requires {:layer 1} x == 0;

 {

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

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

 

     permVar_out := permVar_in;

 

     yield;

     assert {:layer 1} x == 0;

-    assert {:layer 1} permVar_out[0];

     assert {:layer 1} permVar_out == ch_mapconstbool(true);

 

-    call permVar_out, permVarOut2 := Split(permVar_out);

-    async call foo(permVarOut2);

+    async call foo(permVar_out);

     yield;

 }

 

 procedure {:yields} {:layer 1} foo({:linear_in "Perm"} permVar_in: [int]bool) 

-  free requires {:layer 1} permVar_in != ch_mapconstbool(false);

-  free requires {:layer 1} permVar_in[1];

+  requires {:layer 1} permVar_in != ch_mapconstbool(false);

+  requires {:layer 1} permVar_in[1];

   requires {:layer 1} x == 0;

 {

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

diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index b2f02bda..675b3842 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -18,15 +18,6 @@ function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool
   x

 }

 

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

-ensures {:layer 1} xls != 0;

-

-procedure Allocate_1() returns ({:linear "1"} xls: [int]bool);

-ensures {:layer 1} xls == mapconstbool(true);

-

-procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);

-ensures {:layer 1} xls == mapconstbool(true);

-

 var {:layer 0,1} g: int;

 var {:layer 0,1} h: int;

 

@@ -36,30 +27,43 @@ ensures {:atomic} |{A: g := val; return true; }|;
 procedure {:yields} {:layer 0,1} SetH(val:int);

 ensures {:atomic} |{A: h := val; return true; }|;

 

-procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int) 

+procedure {:yields} {:layer 1} Yield({:linear "1"} x: [int]bool)

+requires {:layer 1} x == mapconstbool(true) && g == 0;    

+ensures {:layer 1} x == mapconstbool(true) && g == 0;    

+{

+    yield;

+    assert {:layer 1} x == mapconstbool(true) && g == 0;    

+}

+

+procedure {:yields} {:layer 1} Allocate() returns ({:linear "tid"} xl: int)

+ensures {:layer 1} xl != 0;

+{

+    yield;

+    call xl := AllocateLow();

+    yield;

+}

+

+procedure {:yields} {:layer 0,1} AllocateLow() returns ({:linear "tid"} xls: int);

+ensures {:atomic} |{ A: assume xls != 0; return true; }|;

+

+procedure {:yields} {:layer 1} A({:linear_in "tid"} tid_in: int, {:linear_in "1"} x: [int]bool, {:linear_in "2"} y: [int]bool) returns ({:linear "tid"} tid_out: int) 

+requires {:layer 1} x == mapconstbool(true);

+requires {:layer 1} y == mapconstbool(true);

 {

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

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

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

     tid_out := tid_in;

-    call x := Allocate_1();

-    call y := Allocate_2();

 

     yield;

     call SetG(0);

-    yield;

-    assert {:layer 1} x == mapconstbool(true);    

-    assert {:layer 1} g == 0;    

+    

+    par tid_child := Allocate() | Yield(x);

 

-    yield;

-    call tid_child := Allocate();

     async call B(tid_child, x);

 

     yield;

     assert {:layer 1} x == mapconstbool(true);    

     assert {:layer 1} g == 0;

 

-    yield;

     call SetH(0);

 

     yield;

diff --git a/Test/og/t1.bpl.expect b/Test/og/t1.bpl.expect
index 7877cfd1..f0195727 100644
--- a/Test/og/t1.bpl.expect
+++ b/Test/og/t1.bpl.expect
@@ -1,10 +1,10 @@
-t1.bpl(60,5): Error: Non-interference check failed

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

 Execution trace:

     (0,0): og_init

-    t1.bpl(80,13): anon0

+    t1.bpl(84,13): anon0

     (0,0): anon05

     (0,0): inline$SetG_1$0$Entry

-    t1.bpl(34,21): inline$SetG_1$0$this_A

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

+    t1.bpl(25,21): inline$SetG_1$0$this_A

+    (0,0): inline$Impl_YieldChecker_A_1$0$L1

 

-Boogie program verifier finished with 2 verified, 1 error

+Boogie program verifier finished with 4 verified, 1 error

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index f875d6e5..91863e1a 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -33,8 +33,13 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
     if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket)

 }

 

-procedure Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

+procedure {:yields} {:layer 2} Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X)

 ensures {:layer 1} {:layer 2} xl != nil;

+{

+    yield;

+    call xls, xl := AllocateLow(xls');

+    yield;

+}

 

 procedure {:yields} {:layer 2} main({:linear_in "tid"} xls':[X]bool)

 requires {:layer 2} xls' == mapconstbool(true);

@@ -53,7 +58,7 @@ requires {:layer 2} xls' == mapconstbool(true);
     invariant {:layer 1} Inv1(T, t);

     invariant {:layer 2} Inv2(T, s, cs);

     {

-        call xls, tid := Allocate(xls);

+        par xls, tid := Allocate(xls) | Yield1() | Yield2();

         async call Customer(tid);

     	par Yield1() | Yield2();

     }

@@ -138,3 +143,5 @@ ensures {:atomic} |{ A: assume m <= s; cs := tid; return true; }|;
 procedure {:yields} {:layer 0,2} Leave({:linear "tid"} tid: X);

 ensures {:atomic} |{ A: s := s + 1; cs := nil; return true; }|;

 

+procedure {:yields} {:layer 0,2} AllocateLow({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);

+ensures {:atomic} |{ A: assume xl != nil; return true; }|;

diff --git a/Test/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect
index f7c1129d..28c26eab 100644
--- a/Test/og/ticket.bpl.expect
+++ b/Test/og/ticket.bpl.expect
@@ -1,2 +1,2 @@
 

-Boogie program verifier finished with 14 verified, 0 errors

+Boogie program verifier finished with 16 verified, 0 errors

diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
index 9a612eb2..8622dd9e 100644
--- a/Test/og/treiber-stack.bpl
+++ b/Test/og/treiber-stack.bpl
@@ -16,24 +16,24 @@ axiom (forall x: lmap, i: Node, v: Node :: dom(Add(x, i, v)) == dom(x)[i:=true]
 function Remove(x: lmap, i: Node): (lmap);

 axiom (forall x: lmap, i: Node :: dom(Remove(x, i)) == dom(x)[i:=false] && map(Remove(x, i)) == map(x));

 

-procedure {:yields} {:layer 0} ReadTopOfStack() returns (v:Node);

+procedure {:yields} {:layer 0,1} ReadTopOfStack() returns (v:Node);

 ensures {:right} |{ A: assume dom(Stack)[v] || dom(Used)[v]; return true; }|;

 

-procedure {:yields} {:layer 0} Load(i:Node) returns (v:Node);

+procedure {:yields} {:layer 0,1} Load(i:Node) returns (v:Node);

 ensures {:right} |{ A: assert dom(Stack)[i] || dom(Used)[i]; goto B,C;

 	            B: assume dom(Stack)[i]; v := map(Stack)[i]; return true; 

 		    C: assume !dom(Stack)[i]; return true; }|;

 

-procedure {:yields} {:layer 0} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);

+procedure {:yields} {:layer 0,1} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);

 ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;

 

-procedure {:yields} {:layer 0} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

+procedure {:yields} {:layer 0,1} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);

 ensures {:atomic} |{ A: assert dom(l_in)[newVal];

 		        goto B,C;

                         B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;

 			C: assume oldVal != TopOfStack; l_out := l_in; r := false; return true; }|;

 

-procedure {:yields} {:layer 0} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);

+procedure {:yields} {:layer 0,1} TransferFromStack(oldVal: Node, newVal: Node) returns (r: bool);

 ensures {:atomic} |{ A: goto B,C;

                         B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;

 		        C: assume oldVal != TopOfStack; r := false; return true; }|;