Merge

9 files changed, 541 insertions, 283 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 61943cf0..0911cbd3 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -404,7 +404,7 @@ namespace Microsoft.Boogie {
             inline = true;

           }

         }

-        if (inline && CommandLineOptions.Clo.StratifiedInlining == 0) {

+        if (inline) {

           foreach (var d in TopLevelDeclarations) {

             var impl = d as Implementation;

             if (impl != null) {

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 704c5973..90cfd6d8 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -2482,6 +2482,10 @@ namespace Microsoft.Boogie {
           }

         }

 

+        if (CommandLineOptions.Clo.StratifiedInlining > 0) {

+          return !QKeyValue.FindBoolAttribute(Attributes, "entrypoint");

+        }

+

         return false;

       }

     }

diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs
new file mode 100644
index 00000000..15ad2432
--- /dev/null
+++ b/Source/GPUVerify/BlockPredicator.cs
@@ -0,0 +1,191 @@
+using Microsoft.Boogie;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace GPUVerify {
+
+class BlockPredicator {
+
+  Program prog;
+  Implementation impl;
+
+  Expr returnBlockId;
+
+  LocalVariable curVar, pVar;
+  IdentifierExpr cur, p;
+  Expr pExpr;
+  Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
+    new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
+  Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
+
+  BlockPredicator(Program p, Implementation i) {
+    prog = p;
+    impl = i;
+  }
+
+  void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) {
+    if (cmd is AssignCmd) {
+      var aCmd = (AssignCmd)cmd;
+      cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
+                   new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
+                     new NAryExpr(Token.NoToken,
+                       new IfThenElse(Token.NoToken),
+                       new ExprSeq(p, rhs, lhs.AsExpr))))));
+    } else if (cmd is AssertCmd) {
+      var aCmd = (AssertCmd)cmd;
+      if (cmdSeq.Last() is AssignCmd &&
+          cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) {
+        // This may be a loop invariant.  Make sure it continues to appear as
+        // the first statement in the block.
+        var assign = cmdSeq.Last();
+        cmdSeq.Truncate(cmdSeq.Length-1);
+        cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(pExpr, aCmd.Expr)));
+        cmdSeq.Add(assign);
+      } else {
+        cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+      }
+    } else if (cmd is AssumeCmd) {
+      var aCmd = (AssumeCmd)cmd;
+      cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+    } else if (cmd is HavocCmd) {
+      var hCmd = (HavocCmd)cmd;
+      foreach (IdentifierExpr v in hCmd.Vars) {
+        Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
+        Contract.Assert(type != null);
+
+        IdentifierExpr havocTempExpr;
+        if (havocVars.ContainsKey(type)) {
+          havocTempExpr = havocVars[type];
+        } else {
+          var havocVar = new LocalVariable(Token.NoToken,
+                             new TypedIdent(Token.NoToken,
+                                            "_HAVOC_" + type.ToString(), type));
+          impl.LocVars.Add(havocVar);
+          havocVars[type] = havocTempExpr =
+            new IdentifierExpr(Token.NoToken, havocVar);
+        }
+        cmdSeq.Add(new HavocCmd(Token.NoToken,
+                                new IdentifierExprSeq(havocTempExpr)));
+        cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
+                                    new NAryExpr(Token.NoToken,
+                                      new IfThenElse(Token.NoToken),
+                                      new ExprSeq(p, havocTempExpr, v))));
+      }
+    } else if (cmd is CallCmd) {
+      var cCmd = (CallCmd)cmd;
+      cCmd.Ins.Insert(0, p);
+      cmdSeq.Add(cCmd);
+    } else {
+      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+    }
+  }
+
+  void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) {
+    if (cmd is GotoCmd) {
+      var gCmd = (GotoCmd)cmd;
+      var targets = new List<Expr>(
+        gCmd.labelTargets.Cast<Block>().Select(b => blockIds[b]));
+      if (targets.Count == 1) {
+        PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0]));
+      } else {
+        PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken,
+                                          new IdentifierExprSeq(cur)));
+        PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken,
+               targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or)));
+      }
+    } else if (cmd is ReturnCmd) {
+      PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId));
+    } else {
+      Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+    }
+  }
+
+  void PredicateImplementation() {
+    var g = prog.ProcessLoops(impl);
+    var sortedBlocks = g.LoopyTopSort();
+
+    int blockId = 0;
+    foreach (var block in impl.Blocks)
+      blockIds[block] = Expr.Literal(blockId++);
+    returnBlockId = Expr.Literal(blockId++);
+
+    curVar = new LocalVariable(Token.NoToken,
+                               new TypedIdent(Token.NoToken, "cur",
+                                              Microsoft.Boogie.Type.Int));
+    impl.LocVars.Add(curVar);
+    cur = Expr.Ident(curVar);
+
+    pVar = new LocalVariable(Token.NoToken,
+                             new TypedIdent(Token.NoToken, "p",
+                                            Microsoft.Boogie.Type.Bool));
+    impl.LocVars.Add(pVar);
+    p = Expr.Ident(pVar);
+
+    var newBlocks = new List<Block>();
+
+    var fp = Expr.Ident(impl.InParams[0]);
+    Block entryBlock = new Block();
+    entryBlock.Label = "entry";
+    entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur,
+                        new NAryExpr(Token.NoToken,
+                          new IfThenElse(Token.NoToken),
+                          new ExprSeq(fp, blockIds[sortedBlocks[0].Item1],
+                                      returnBlockId))));
+    newBlocks.Add(entryBlock);
+
+    var prevBlock = entryBlock;
+    foreach (var n in sortedBlocks) {
+      if (n.Item2) {
+        var tailBlock = new Block();
+        newBlocks.Add(tailBlock);
+
+        tailBlock.Label = n.Item1.Label + ".tail";
+        tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
+                                             Expr.Neq(cur, blockIds[n.Item1])));
+
+        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
+                                            new BlockSeq(tailBlock, n.Item1));
+        prevBlock = tailBlock;
+      } else {
+        var runBlock = n.Item1;
+        newBlocks.Add(runBlock);
+
+        pExpr = Expr.Eq(cur, blockIds[runBlock]);
+        CmdSeq newCmdSeq = new CmdSeq();
+        newCmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr));
+        foreach (Cmd cmd in runBlock.Cmds)
+          PredicateCmd(newCmdSeq, cmd);
+        PredicateTransferCmd(newCmdSeq, runBlock.TransferCmd);
+        runBlock.Cmds = newCmdSeq;
+
+        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
+                                            new BlockSeq(runBlock));
+        prevBlock = runBlock;
+      }
+    }
+
+    prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
+    impl.Blocks = newBlocks;
+  }
+
+  public static void Predicate(Program p) {
+    foreach (var decl in p.TopLevelDeclarations) {
+      if (decl is DeclWithFormals && !(decl is Function)) {
+        var dwf = (DeclWithFormals)decl;
+        var fpVar = new LocalVariable(Token.NoToken,
+                                    new TypedIdent(Token.NoToken, "fp",
+                                                   Microsoft.Boogie.Type.Bool));
+        dwf.InParams = new VariableSeq((dwf.InParams + new VariableSeq(fpVar))
+                       .Cast<Variable>().ToArray());
+      }
+      var impl = decl as Implementation;
+      if (impl != null)
+        new BlockPredicator(p, impl).PredicateImplementation();
+    }
+  }
+
+}
+
+}
diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 502844b2..7e6324b2 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -40,6 +40,8 @@ namespace GPUVerify
 

         public static bool NoLoopPredicateInvariants = false;

 

+        public static bool Unstructured = false;

+

         public static int Parse(string[] args)

         {

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

@@ -177,6 +179,11 @@ namespace GPUVerify
                     NoLoopPredicateInvariants = true;

                     break;

 

+                    case "-unstructured":

+                    case "/unstructured":

+                    Unstructured = true;

+                    break;

+

                     default:

                         inputFiles.Add(args[i]);

                         break;

@@ -216,6 +223,7 @@ namespace GPUVerify
   /divided         : check individual pairs of possibly racing statements separately

   /dividedArray    : check races on arrays one at a time

   /dividedElement  : ???

+  /unstructured    : operate on the unstructured form of the program

 

 ");

         }

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index f6ba390b..5d5bd4d6 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -102,19 +102,35 @@ namespace GPUVerify
 

         private Procedure CheckExactlyOneKernelProcedure()

         {

-            return CheckSingleInstanceOfAttributedProcedure(Program, "kernel");

+            var p = CheckSingleInstanceOfAttributedProcedure("kernel");

+            if (p == null)

+            {

+                Error(Program, "\"kernel\" attribute has not been specified for any procedure.  You must mark exactly one procedure with this attribute");

+            }

+

+            return p;

         }

 

-        private Procedure CheckExactlyOneBarrierProcedure()

+        private Procedure FindOrCreateBarrierProcedure()

         {

-            return CheckSingleInstanceOfAttributedProcedure(Program, "barrier");

+            var p = CheckSingleInstanceOfAttributedProcedure("barrier");

+            if (p == null)

+            {

+                p = new Procedure(Token.NoToken, "barrier", new TypeVariableSeq(),

+                                  new VariableSeq(), new VariableSeq(),

+                                  new RequiresSeq(), new IdentifierExprSeq(),

+                                  new EnsuresSeq(),

+                                  new QKeyValue(Token.NoToken, "barrier", new List<object>(), null));

+                Program.TopLevelDeclarations.Add(p);

+            }

+            return p;

         }

 

-        private Procedure CheckSingleInstanceOfAttributedProcedure(Program program, string attribute)

+        private Procedure CheckSingleInstanceOfAttributedProcedure(string attribute)

         {

             Procedure attributedProcedure = null;

 

-            foreach (Declaration decl in program.TopLevelDeclarations)

+            foreach (Declaration decl in Program.TopLevelDeclarations)

             {

                 if (!QKeyValue.FindBoolAttribute(decl.Attributes, attribute))

                 {

@@ -144,11 +160,6 @@ namespace GPUVerify
                 }

             }

 

-            if (attributedProcedure == null)

-            {

-                Error(program, "\"{0}\" attribute has not been specified for any procedure.  You must mark exactly one procedure with this attribute", attribute);

-            }

-

             return attributedProcedure;

         }

 

@@ -189,10 +200,20 @@ namespace GPUVerify
             return true;

         }

 

-        private bool FindNonLocalVariables(Program program)

+        private void MaybeCreateAttributedConst(string attr, ref Constant constFieldRef)

+        {

+            if (constFieldRef == null)

+            {

+                constFieldRef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, attr, Microsoft.Boogie.Type.GetBvType(32)));

+                constFieldRef.AddAttribute(attr);

+                Program.TopLevelDeclarations.Add(constFieldRef);

+            }

+        }

+

+        private bool FindNonLocalVariables()

         {

             bool success = true;

-            foreach (Declaration D in program.TopLevelDeclarations)

+            foreach (Declaration D in Program.TopLevelDeclarations)

             {

                 if (D is Variable && (D as Variable).IsMutable)

                 {

@@ -232,6 +253,22 @@ namespace GPUVerify
                 }

             }

 

+            MaybeCreateAttributedConst(LOCAL_ID_X_STRING, ref _X);

+            MaybeCreateAttributedConst(LOCAL_ID_Y_STRING, ref _Y);

+            MaybeCreateAttributedConst(LOCAL_ID_Z_STRING, ref _Z);

+

+            MaybeCreateAttributedConst(GROUP_SIZE_X_STRING, ref _GROUP_SIZE_X);

+            MaybeCreateAttributedConst(GROUP_SIZE_Y_STRING, ref _GROUP_SIZE_Y);

+            MaybeCreateAttributedConst(GROUP_SIZE_Z_STRING, ref _GROUP_SIZE_Z);

+

+            MaybeCreateAttributedConst(GROUP_ID_X_STRING, ref _GROUP_X);

+            MaybeCreateAttributedConst(GROUP_ID_Y_STRING, ref _GROUP_Y);

+            MaybeCreateAttributedConst(GROUP_ID_Z_STRING, ref _GROUP_Z);

+

+            MaybeCreateAttributedConst(NUM_GROUPS_X_STRING, ref _NUM_GROUPS_X);

+            MaybeCreateAttributedConst(NUM_GROUPS_Y_STRING, ref _NUM_GROUPS_Y);

+            MaybeCreateAttributedConst(NUM_GROUPS_Z_STRING, ref _NUM_GROUPS_Z);

+

             return success;

         }

 

@@ -307,6 +344,10 @@ namespace GPUVerify
 

         internal void doit()

         {

+            if (CommandLineOptions.Unstructured)

+            {

+                Microsoft.Boogie.CommandLineOptions.Clo.PrintUnstructured = 2;

+            }

 

             if (CommandLineOptions.ShowStages)

             {

@@ -1920,7 +1961,7 @@ namespace GPUVerify
                 if (d is Implementation)

                 {

 

-                    new KernelDualiser(this).DualiseImplementation(d as Implementation);

+                    new KernelDualiser(this).DualiseImplementation(d as Implementation, CommandLineOptions.Unstructured);

 

                     NewTopLevelDeclarations.Add(d as Implementation);

 

@@ -1946,6 +1987,12 @@ namespace GPUVerify
 

         private void MakeKernelPredicated()

         {

+            if (CommandLineOptions.Unstructured)

+            {

+                BlockPredicator.Predicate(Program);

+                return;

+            }

+

             foreach (Declaration d in Program.TopLevelDeclarations)

             {

                 if (d is Procedure)

@@ -2007,7 +2054,7 @@ namespace GPUVerify
 

         private int Check()

         {

-            BarrierProcedure = CheckExactlyOneBarrierProcedure();

+            BarrierProcedure = FindOrCreateBarrierProcedure();

             KernelProcedure = CheckExactlyOneKernelProcedure();

 

             if (ErrorCount > 0)

@@ -2025,101 +2072,15 @@ namespace GPUVerify
                 Error(BarrierProcedure, "Barrier procedure must not return any results");

             }

 

-            if (!FindNonLocalVariables(Program))

+            if (!FindNonLocalVariables())

             {

                 return ErrorCount;

             }

 

             CheckKernelImplementation();

-

-            if (!KernelHasIdX())

-            {

-                MissingKernelAttributeError(LOCAL_ID_X_STRING);

-            }

-

-            if (!KernelHasGroupSizeX())

-            {

-                MissingKernelAttributeError(GROUP_SIZE_X_STRING);

-            }

-

-            if (!KernelHasNumGroupsX())

-            {

-                MissingKernelAttributeError(NUM_GROUPS_X_STRING);

-            }

-

-            if (!KernelHasGroupIdX())

-            {

-                MissingKernelAttributeError(GROUP_ID_X_STRING);

-            }

-

-            if (!KernelHasIdY())

-            {

-                MissingKernelAttributeError(LOCAL_ID_Y_STRING);

-            }

-

-            if (!KernelHasGroupSizeY())

-            {

-                MissingKernelAttributeError(GROUP_SIZE_Y_STRING);

-            }

-

-            if (!KernelHasNumGroupsY())

-            {

-                MissingKernelAttributeError(NUM_GROUPS_Y_STRING);

-            }

-

-            if (!KernelHasGroupIdY())

-            {

-                MissingKernelAttributeError(GROUP_ID_Y_STRING);

-            }

-

-            if (!KernelHasIdY())

-            {

-                MissingKernelAttributeError(LOCAL_ID_Y_STRING);

-            }

-

-            if (!KernelHasGroupSizeY())

-            {

-                MissingKernelAttributeError(GROUP_SIZE_Y_STRING);

-            }

-

-            if (!KernelHasNumGroupsY())

-            {

-                MissingKernelAttributeError(NUM_GROUPS_Y_STRING);

-            }

-

-            if (!KernelHasGroupIdY())

-            {

-                MissingKernelAttributeError(GROUP_ID_Y_STRING);

-            }

-

-            if (!KernelHasIdZ())

-            {

-                MissingKernelAttributeError(LOCAL_ID_Z_STRING);

-            }

-

-            if (!KernelHasGroupSizeZ())

-            {

-                MissingKernelAttributeError(GROUP_SIZE_Z_STRING);

-            }

-

-            if (!KernelHasNumGroupsZ())

-            {

-                MissingKernelAttributeError(NUM_GROUPS_Z_STRING);

-            }

-

-            if (!KernelHasGroupIdZ())

-            {

-                MissingKernelAttributeError(GROUP_ID_Z_STRING);

-            }

-

             return ErrorCount;

         }

 

-        private void MissingKernelAttributeError(string attribute)

-        {

-            Error(KernelProcedure.tok, "Kernel must declare global constant marked with attribute ':" + attribute + "'");

-        }

-

         public static bool IsThreadLocalIdConstant(Variable variable)

         {

             return variable.Name.Equals(_X.Name) || variable.Name.Equals(_Y.Name) || variable.Name.Equals(_Z.Name);

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index b375efd9..27b9abe5 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -108,6 +108,8 @@
     <Compile Include="AccessRecord.cs" />

     <Compile Include="ArrayControlFlowAnalyser.cs" />

     <Compile Include="AsymmetricExpressionFinder.cs" />

+    <Compile Include="BlockPredicator.cs" />

+    <Compile Include="GraphAlgorithms.cs" />

     <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />

     <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />

     <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />

@@ -158,6 +160,10 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

+    <ProjectReference Include="..\Graph\Graph.csproj">

+      <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

+      <Name>Graph</Name>

+    </ProjectReference>

     <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

       <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

diff --git a/Source/GPUVerify/GraphAlgorithms.cs b/Source/GPUVerify/GraphAlgorithms.cs
new file mode 100644
index 00000000..3442a64d
--- /dev/null
+++ b/Source/GPUVerify/GraphAlgorithms.cs
@@ -0,0 +1,84 @@
+using Graphing;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace GPUVerify {
+
+public static class GraphAlgorithms {
+
+  public static List<Tuple<Node, bool>> LoopyTopSort<Node>(this Graph<Node> g) {
+    Contract.Assert(g.Reducible);
+
+    int n = g.Nodes.Count;
+    var nodeToNumber = new Dictionary<Node, int>(n);
+    var numberToNode = new Node[n];
+    var allNodes = new List<int>();
+    int counter = 0;
+    foreach (Node node in g.Nodes) {
+      numberToNode[counter] = node;
+      nodeToNumber[node] = counter;
+      allNodes.Add(counter);
+      counter++;
+    }
+
+    var loops = new List<int>[n];
+    foreach (var h in g.Headers) {
+      var loopNodes = new HashSet<Node>();
+      foreach (var b in g.BackEdgeNodes(h))
+        loopNodes.UnionWith(g.NaturalLoops(h, b));
+      loops[nodeToNumber[h]] =
+        new List<int>(loopNodes.Select(node => nodeToNumber[node]));
+    }
+
+    var successors = new List<int>[n];
+    int[] incomingEdges = new int[n];
+
+    foreach (var e in g.Edges) {
+      Contract.Assert(e.Item1 != null);
+      Contract.Assert(e.Item2 != null);
+      int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2];
+      if (loops[target] == null || !loops[target].Contains(source)) {
+        if (successors[source] == null)
+          successors[source] = new List<int>();
+        successors[source].Add(target);
+        incomingEdges[target]++;
+      }
+    }
+
+    var sortedNodes = new List<Tuple<Node, bool>>();
+
+    var regionStack = new Stack<Tuple<Node, List<int>>>();
+    regionStack.Push(new Tuple<Node, List<int>>(default(Node), allNodes));
+
+    while (regionStack.Count != 0) {
+      int rootIndex = -1;
+      foreach (var i in regionStack.Peek().Item2) {
+        if (incomingEdges[i] == 0) {
+          rootIndex = i;
+          break;
+        }
+      }
+      if (rootIndex == -1) {
+        var region = regionStack.Pop();
+        if (regionStack.Count != 0)
+          sortedNodes.Add(new Tuple<Node, bool>(region.Item1, true));
+        continue;
+      }
+      incomingEdges[rootIndex] = -1;
+      sortedNodes.Add(new Tuple<Node, bool>(numberToNode[rootIndex], false));
+      if (successors[rootIndex] != null)
+        foreach (int s in successors[rootIndex])
+          incomingEdges[s]--;
+      if (loops[rootIndex] != null)
+        regionStack.Push(new Tuple<Node, List<int>>(numberToNode[rootIndex],
+                                                    loops[rootIndex]));
+    }
+
+    return sortedNodes;
+  }
+
+}
+
+}
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs
index 0496a4e0..8d51e74e 100644
--- a/Source/GPUVerify/KernelDualiser.cs
+++ b/Source/GPUVerify/KernelDualiser.cs
@@ -82,145 +82,150 @@ namespace GPUVerify
             return result;

         }

 

-        private BigBlock MakeDual(BigBlock bb)

+        private void MakeDual(CmdSeq cs, Cmd c)

         {

-            // Not sure what to do about the transfer command

-

-            BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);

-

-            foreach (Cmd c in bb.simpleCmds)

+            if (c is CallCmd)

             {

-                if (c is CallCmd)

-                {

-                    CallCmd Call = c as CallCmd;

+                CallCmd Call = c as CallCmd;

 

-                    List<Expr> uniformNewIns = new List<Expr>();

-                    List<Expr> nonUniformNewIns = new List<Expr>();

-                    for (int i = 0; i < Call.Ins.Count; i++)

+                List<Expr> uniformNewIns = new List<Expr>();

+                List<Expr> nonUniformNewIns = new List<Expr>();

+                for (int i = 0; i < Call.Ins.Count; i++)

+                {

+                    if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i)))

                     {

-                        if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i)))

-                        {

-                            uniformNewIns.Add(Call.Ins[i]);

-                        }

-                        else

-                        {

-                            nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

-                        }

+                        uniformNewIns.Add(Call.Ins[i]);

                     }

-                    for (int i = 0; i < Call.Ins.Count; i++)

+                    else

                     {

-                        if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))

-                        {

-                            nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

-                        }

+                        nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

                     }

+                }

+                for (int i = 0; i < Call.Ins.Count; i++)

+                {

+                    if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))

+                    {

+                        nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

+                    }

+                }

 

-                    List<Expr> newIns = uniformNewIns;

-                    newIns.AddRange(nonUniformNewIns);

+                List<Expr> newIns = uniformNewIns;

+                newIns.AddRange(nonUniformNewIns);

 

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

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

-                    for (int i = 0; i < Call.Outs.Count; i++)

+                List<IdentifierExpr> uniformNewOuts = new List<IdentifierExpr>();

+                List<IdentifierExpr> nonUniformNewOuts = new List<IdentifierExpr>();

+                for (int i = 0; i < Call.Outs.Count; i++)

+                {

+                    if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i)))

                     {

-                        if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i)))

-                        {

-                            uniformNewOuts.Add(Call.Outs[i]);

-                        }

-                        else

-                        {

-                            nonUniformNewOuts.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);

-                        }

-

+                        uniformNewOuts.Add(Call.Outs[i]);

                     }

-                    for (int i = 0; i < Call.Outs.Count; i++)

+                    else

                     {

-                        if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))

-                        {

-                            nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);

-                        }

+                        nonUniformNewOuts.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);

                     }

 

-                    List<IdentifierExpr> newOuts = uniformNewOuts;

-                    newOuts.AddRange(nonUniformNewOuts);

-

-                    CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);

-

-                    NewCallCmd.Proc = Call.Proc;

-

-                    result.simpleCmds.Add(NewCallCmd);

                 }

-                else if (c is AssignCmd)

+                for (int i = 0; i < Call.Outs.Count; i++)

                 {

-                    AssignCmd assign = c as AssignCmd;

-

-                    Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

-

-                    if (assign.Lhss[0] is SimpleAssignLhs &&

-                        verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))

+                    if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))

                     {

-                        result.simpleCmds.Add(assign);

+                        nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);

                     }

-                    else

-                    {

-                        List<AssignLhs> newLhss = new List<AssignLhs>();

-                        List<Expr> newRhss = new List<Expr>();

+                }

 

-                        newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

-                        newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

+                List<IdentifierExpr> newOuts = uniformNewOuts;

+                newOuts.AddRange(nonUniformNewOuts);

 

-                        newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

-                        newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

+                CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, newIns, newOuts);

 

-                        AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);

+                NewCallCmd.Proc = Call.Proc;

 

-                        result.simpleCmds.Add(newAssign);

-                    }

+                cs.Add(NewCallCmd);

+            }

+            else if (c is AssignCmd)

+            {

+                AssignCmd assign = c as AssignCmd;

+

+                Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

+

+                if (assign.Lhss[0] is SimpleAssignLhs &&

+                    verifier.uniformityAnalyser.IsUniform(procName, (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Name))

+                {

+                    cs.Add(assign);

                 }

-                else if (c is HavocCmd)

+                else

                 {

-                    HavocCmd havoc = c as HavocCmd;

-                    Debug.Assert(havoc.Vars.Length == 1);

+                    List<AssignLhs> newLhss = new List<AssignLhs>();

+                    List<Expr> newRhss = new List<Expr>();

+

+                    newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

+                    newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

+

+                    newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

+                    newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

+

+                    AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);

+

+                    cs.Add(newAssign);

+                }

+            }

+            else if (c is HavocCmd)

+            {

+                HavocCmd havoc = c as HavocCmd;

+                Debug.Assert(havoc.Vars.Length == 1);

 

-                    HavocCmd newHavoc;

+                HavocCmd newHavoc;

 

-                    newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 

-                        (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)), 

-                        (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))

-                    }));

+                newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 

+                    (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)), 

+                    (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))

+                }));

 

-                    result.simpleCmds.Add(newHavoc);

+                cs.Add(newHavoc);

+            }

+            else if (c is AssertCmd)

+            {

+                AssertCmd ass = c as AssertCmd;

+                if (ContainsAsymmetricExpression(ass.Expr))

+                {

+                    cs.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));

                 }

-                else if (c is AssertCmd)

+                else

                 {

-                    AssertCmd ass = c as AssertCmd;

-                    if (ContainsAsymmetricExpression(ass.Expr))

-                    {

-                        result.simpleCmds.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));

-                    }

-                    else

-                    {

-                        result.simpleCmds.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),

-                            new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));

-                    }

+                    cs.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),

+                        new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));

                 }

-                else if (c is AssumeCmd)

+            }

+            else if (c is AssumeCmd)

+            {

+                AssumeCmd ass = c as AssumeCmd;

+                if (ContainsAsymmetricExpression(ass.Expr))

                 {

-                    AssumeCmd ass = c as AssumeCmd;

-                    if (ContainsAsymmetricExpression(ass.Expr))

-                    {

-                        result.simpleCmds.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));

-                    }

-                    else

-                    {

-                        result.simpleCmds.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),

-                            new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));

-                    }

+                    cs.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));

                 }

                 else

                 {

-                    Debug.Assert(false);

+                    cs.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),

+                        new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));

                 }

             }

+            else

+            {

+                Debug.Assert(false);

+            }

+        }

+

+        private BigBlock MakeDual(BigBlock bb)

+        {

+            // Not sure what to do about the transfer command

+

+            BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);

+

+            foreach (Cmd c in bb.simpleCmds)

+            {

+                MakeDual(result.simpleCmds, c);

+            }

 

             if (bb.ec is WhileCmd)

             {

@@ -262,6 +267,16 @@ namespace GPUVerify
 

         }

 

+        private Block MakeDual(Block b)

+        {

+            Block result = new Block(b.tok, b.Label, new CmdSeq(), b.TransferCmd);

+            foreach (Cmd c in b.Cmds)

+            {

+                MakeDual(result.Cmds, c);

+            }

+            return result;

+        }

+

         private List<PredicateCmd> MakeDualInvariants(List<PredicateCmd> originalInvariants)

         {

             List<PredicateCmd> result = new List<PredicateCmd>();

@@ -345,14 +360,17 @@ namespace GPUVerify
         }

 

 

-        internal void DualiseImplementation(Implementation impl)

+        internal void DualiseImplementation(Implementation impl, bool unstructured)

         {

             procName = impl.Name;

 

             impl.InParams = DualiseVariableSequence(impl.InParams);

             impl.OutParams = DualiseVariableSequence(impl.OutParams);

             MakeDualLocalVariables(impl);

-            impl.StructuredStmts = MakeDual(impl.StructuredStmts);

+            if (unstructured)

+                impl.Blocks = new List<Block>(impl.Blocks.Select(MakeDual));

+            else

+                impl.StructuredStmts = MakeDual(impl.StructuredStmts);

 

             procName = null;

         }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 8f9f7498..e69c38b1 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -52,9 +52,7 @@ namespace VC
               Implementation impl = decl as Implementation;

               if (impl == null) continue;

               Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");

-              if (impl.Proc.FindExprAttribute("inline") != null) {

-                implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);

-              }

+              implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);

             }

             this.GenerateRecordFunctions();

             PersistCallTree = false;

@@ -136,58 +134,63 @@ namespace VC
             return node;

           }

         }

-        

-        public class StratifiedVC {

-          private static int newVarCount = 0;

-          private static VCExprVar CreateNewVar(ProverInterface prover, Microsoft.Boogie.Type type) {

-            string newName = "StratifiedInlining@" + newVarCnt.ToString();

-            newVarCount++;

-            Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));

-            prover.Context.DeclareConstant(newVar, false, null);

-            return prover.VCExprGen.Variable(newVar.Name, type);

-          }

-          private static int idCount = 0;

 

+        private int newVarCount = 0;

+        public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {

+          string newName = "StratifiedInlining@" + newVarCnt.ToString();

+          newVarCount++;

+          Constant newVar = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, newName, type));

+          prover.Context.DeclareConstant(newVar, false, null);

+          return prover.VCExprGen.Variable(newVar.Name, type);

+        }

+        private int idCount = 1; // 0 is reserved for the VC of main

+        public int CreateNewId() {

+          return idCount++;

+        }

+

+        public class StratifiedVC {

+          StratifiedInliningInfo info;

           int id;

-          Implementation impl;

           List<VCExprVar> interfaceExprVars;

           List<StratifiedCallSite> callSites;

           VCExpr vcexpr;

           public Dictionary<Block, VCExprVar> reachVars;

 

-          public StratifiedVC(StratifiedInliningInfo info, StratifiedVCGen vcgen) {

+          public StratifiedVC(StratifiedInliningInfo siInfo) {

+            info = siInfo;

             if (!info.initialized) {

-              info.GenerateVC(vcgen);

+              info.GenerateVC();

             }

 

-            impl = info.impl;

-            interfaceExprVars = new List<VCExprVar>();

             VCExpr expansion = info.vcexpr;

+            var vcgen = info.vcgen;

             var prover = vcgen.prover;

             VCExpressionGenerator gen = prover.VCExprGen;

             var bet = prover.Context.BoogieExprTranslator;

             VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);

-            id = idCount++;

+            id = vcgen.CreateNewId();

             VCExpr eqExpr = gen.Eq(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));

             expansion = gen.And(eqExpr, expansion);

 

+            interfaceExprVars = new List<VCExprVar>();

             Dictionary<VCExprVar, VCExpr> substDict = new Dictionary<VCExprVar, VCExpr>();

             foreach (VCExprVar v in info.interfaceExprVars) {

-              VCExprVar newVar = CreateNewVar(prover, v.Type);

+              VCExprVar newVar = vcgen.CreateNewVar(v.Type);

               interfaceExprVars.Add(newVar);

               substDict.Add(v, newVar);

             }

             foreach (VCExprVar v in info.privateExprVars) {

-              substDict.Add(v, CreateNewVar(prover, v.Type));

+              substDict.Add(v, vcgen.CreateNewVar(v.Type));

             }

             VCExprSubstitution subst = new VCExprSubstitution(substDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());

             SubstitutingVCExprVisitor substVisitor = new SubstitutingVCExprVisitor(prover.VCExprGen);

             expansion = substVisitor.Mutate(expansion, subst);

-            

+

+            var impl = info.impl;

             reachVars = new Dictionary<Block, VCExprVar>();

             Dictionary<Block, VCExpr> reachExprs = new Dictionary<Block, VCExpr>();

             foreach (Block b in impl.Blocks) {

-              reachVars[b] = CreateNewVar(prover, Bpl.Type.Bool);

+              reachVars[b] = vcgen.CreateNewVar(Bpl.Type.Bool);

               reachExprs[b] = VCExpressionGenerator.False;

             }

             foreach (Block b in impl.Blocks) {

@@ -209,7 +212,16 @@ namespace VC
             foreach (CallSite cs in info.callSites) {

               callSites.Add(new StratifiedCallSite(cs, substVisitor, subst, reachVars));

             }

+          }

 

+          public VCExpr Attach(StratifiedCallSite stratifiedCallSite) {

+            Contract.Assert(interfaceExprVars.Count == stratifiedCallSite.interfaceExprVars.Count);

+            VCExpressionGenerator gen = info.vcgen.prover.VCExprGen;

+            VCExpr ret = gen.Eq(stratifiedCallSite.reachVar, reachVars[info.impl.Blocks[0]]);

+            for (int i = 0; i < stratifiedCallSite.interfaceExprVars.Count; i++) {

+              ret = gen.And(ret, gen.Eq(stratifiedCallSite.interfaceExprVars[i], interfaceExprVars[i]));

+            }

+            return ret;

           }

         }

 

@@ -225,9 +237,9 @@ namespace VC
         }

 

         public class StratifiedCallSite {

-          CallSite callSite;

-          List<VCExpr> interfaceExprVars;

-          VCExprVar reachVar;

+          public CallSite callSite;

+          public List<VCExpr> interfaceExprVars;

+          public VCExprVar reachVar;

 

           public StratifiedCallSite(CallSite cs, SubstitutingVCExprVisitor substVisitor, VCExprSubstitution subst, Dictionary<Block, VCExprVar> reachVars) {

             callSite = cs;

@@ -240,6 +252,7 @@ namespace VC
         }

 

         public class StratifiedInliningInfo {

+          public StratifiedVCGen vcgen;

           public Implementation impl;

           public Function function;

           public Variable controlFlowVariable;

@@ -252,7 +265,8 @@ namespace VC
           public List<CallSite> callSites;

           public bool initialized;

 

-          public StratifiedInliningInfo(Implementation implementation, StratifiedVCGen vcgen) {

+          public StratifiedInliningInfo(Implementation implementation, StratifiedVCGen stratifiedVcGen) {

+            vcgen = stratifiedVcGen;

             impl = implementation;

 

             VariableSeq functionInterfaceVars = new VariableSeq();

@@ -298,7 +312,7 @@ namespace VC
             initialized = false;

           }

 

-          public void GenerateVC(StratifiedVCGen vcgen) {

+          public void GenerateVC() {

             List<Variable> outputVariables = new List<Variable>();

             assertExpr = new LiteralExpr(Token.NoToken, true);

             foreach (Variable v in impl.OutParams) {

@@ -1054,7 +1068,7 @@ namespace VC
             public ApiChecker checker2;

 

             public VerificationState(VCExpr vcMain, FCallHandler calls, ProverInterface prover, ProverInterface.ErrorHandler reporter) {

-              prover.Assert(vcMain, false); 

+              prover.Assert(vcMain, true); 

               this.calls = calls;

               this.checker = new ApiChecker(prover, reporter);

               vcSize = 0;

@@ -1087,7 +1101,7 @@ namespace VC
             foreach (StratifiedInliningInfo info in implName2StratifiedInliningInfo.Values)

             {

                 Contract.Assert(info != null);

-                info.GenerateVC(this);

+                info.GenerateVC();

             }

 

             // Get the VC of the current procedure

@@ -1285,8 +1299,10 @@ namespace VC
 

         public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback)

         {

-            Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

+            if (!QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint")) 

+              return Outcome.Correct;

             Debug.Assert(this.program == program);

+

             var computeUnderBound = true;

 

             #region stratified inlining options

@@ -1320,11 +1336,12 @@ namespace VC
             }

 

             // Get the VC of the current procedure

-            VCExpr vc;

-            Hashtable/*<int, Absy!>*/ mainLabel2absy;

-            StratifiedInliningErrorReporter reporter;

-            GetVC(impl, program, prover, callback, out vc, out mainLabel2absy, out reporter);

-      

+            StratifiedInliningInfo info = implName2StratifiedInliningInfo[impl.Name];

+            info.GenerateVC();

+            VCExpr vc = info.vcexpr;

+            Hashtable mainLabel2absy = info.label2absy;

+            var reporter = new StratifiedInliningErrorReporter(implName2StratifiedInliningInfo, prover, callback, info.mvInfo, prover.Context, program, impl);

+

             // Find all procedure calls in vc and put labels on them      

             FCallHandler calls = new FCallHandler(prover.VCExprGen, implName2StratifiedInliningInfo, impl.Name, mainLabel2absy);

             calls.setCurrProcAsMain();

@@ -1773,7 +1790,7 @@ namespace VC
                 StratifiedInliningInfo info = implName2StratifiedInliningInfo[procName];

                 if (!info.initialized)

                 {

-                    info.GenerateVC(this);

+                    info.GenerateVC();

                 }

                 //Console.WriteLine("Inlining {0}", procName);

                 VCExpr expansion = cce.NonNull(info.vcexpr);

@@ -1883,7 +1900,7 @@ namespace VC
             }

 

             reporter = new StratifiedInliningErrorReporter(

-               cce.NonNull(implName2StratifiedInliningInfo), prover, callback, mvInfo, prover.Context, gotoCmdOrigins, program, impl);

+               cce.NonNull(implName2StratifiedInliningInfo), prover, callback, mvInfo, prover.Context, program, impl);

         }

 

 

@@ -2467,7 +2484,6 @@ namespace VC
             Program/*!*/ program;

             Implementation/*!*/ mainImpl;

             ProverContext/*!*/ context;

-            Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins;

 

             public bool underapproximationMode;

             public List<int>/*!*/ candidatesToExpand;

@@ -2487,7 +2503,6 @@ namespace VC
 

             public StratifiedInliningErrorReporter(Dictionary<string/*!*/, StratifiedInliningInfo/*!*/>/*!*/ implName2StratifiedInliningInfo,

                                                    ProverInterface/*!*/ theoremProver, VerifierCallback/*!*/ callback, ModelViewInfo mvInfo, ProverContext/*!*/ context,

-                                                   Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins,

                                                    Program/*!*/ program, Implementation/*!*/ mainImpl)

             {

                 Contract.Requires(cce.NonNullDictionaryAndValues(implName2StratifiedInliningInfo));

@@ -2505,7 +2520,6 @@ namespace VC
                 this.underapproximationMode = false;

                 this.calls = null;

                 this.candidatesToExpand = new List<int>();

-                this.gotoCmdOrigins = gotoCmdOrigins;

             }

 

             public void SetCandidateHandler(FCallHandler calls)

@@ -2637,21 +2651,14 @@ namespace VC
               Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || model != null);

 

               candidatesToExpand = new List<int>();

+              var cex = GenerateTraceMain(labels, model, mvInfo);

 

-              if (underapproximationMode) {

-                var cex = GenerateTraceMain(labels, model, mvInfo);

+              if (underapproximationMode && cex != null) {

                 Debug.Assert(candidatesToExpand.All(calls.isSkipped));

-                if (cex != null) {

-                  GetModelWithStates(model);

-                  callback.OnCounterexample(cex, null);

-                  this.PrintModel(model);

-                }

-                return;

+                GetModelWithStates(model);

+                callback.OnCounterexample(cex, null);

+                this.PrintModel(model);

               }

-

-              Contract.Assert(calls != null);

-

-              GenerateTraceMain(labels, model, mvInfo);

             }

 

             // Construct the interprocedural trace

@@ -2663,28 +2670,7 @@ namespace VC
               }

 

               orderedStateIds = new List<Tuple<int, int>>();

-              Counterexample newCounterexample =

-               GenerateTrace(labels, errModel, 0, mainImpl);

-

-              if (newCounterexample == null)

-                return null;

-

-              #region Map passive program errors back to original program errors

-              ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample;

-              if (returnExample != null && gotoCmdOrigins != null) {

-                foreach (Block b in returnExample.Trace) {

-                  Contract.Assert(b != null);

-                  Contract.Assume(b.TransferCmd != null);

-                  ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd];

-                  if (cmd != null) {

-                    returnExample.FailingReturn = cmd;

-                    break;

-                  }

-                }

-              }

-              #endregion

-

-              return newCounterexample;

+              return GenerateTrace(labels, errModel, 0, mainImpl);

             }

 

             private Counterexample GenerateTrace(IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel,