Merge

11 files changed, 428 insertions, 132 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) {