Merge

19 files changed, 2000 insertions, 1350 deletions

diff --git a/Source/GPUVerify.sln b/Source/GPUVerify.sln
index 4d515300..7853459f 100644
--- a/Source/GPUVerify.sln
+++ b/Source/GPUVerify.sln
@@ -29,6 +29,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "VCExpr\VCExpr.csp
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Isabelle", "Provers\Isabelle\Isabelle.csproj", "{435D5BD0-6F62-49F8-BB24-33E2257519AD}"

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "GPUVerifyBoogieDriver", "GPUVerifyBoogieDriver\GPUVerifyBoogieDriver.csproj", "{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}"

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Checked|Any CPU = Checked|Any CPU

@@ -327,6 +329,26 @@ Global
 		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Mixed Platforms.ActiveCfg = z3apidebug|Any CPU

 		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|Mixed Platforms.Build.0 = z3apidebug|Any CPU

 		{435D5BD0-6F62-49F8-BB24-33E2257519AD}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Checked|Any CPU.ActiveCfg = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Checked|Mixed Platforms.ActiveCfg = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Checked|Mixed Platforms.Build.0 = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Checked|x86.ActiveCfg = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Checked|x86.Build.0 = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Debug|Any CPU.ActiveCfg = Debug|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Debug|Mixed Platforms.ActiveCfg = Debug|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Debug|Mixed Platforms.Build.0 = Debug|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Debug|x86.ActiveCfg = Debug|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Debug|x86.Build.0 = Debug|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Release|Any CPU.ActiveCfg = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Release|Mixed Platforms.ActiveCfg = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Release|Mixed Platforms.Build.0 = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Release|x86.ActiveCfg = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.Release|x86.Build.0 = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.z3apidebug|Any CPU.ActiveCfg = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.z3apidebug|Mixed Platforms.ActiveCfg = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.z3apidebug|Mixed Platforms.Build.0 = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.z3apidebug|x86.ActiveCfg = Release|x86

+		{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}.z3apidebug|x86.Build.0 = Release|x86

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/GPUVerify/AccessRecord.cs b/Source/GPUVerify/AccessRecord.cs
index fedacde3..343cca8c 100644
--- a/Source/GPUVerify/AccessRecord.cs
+++ b/Source/GPUVerify/AccessRecord.cs
@@ -10,16 +10,12 @@ namespace GPUVerify
     class AccessRecord

     {

         public Variable v;

-        public Expr IndexZ;

-        public Expr IndexY;

-        public Expr IndexX;

+        public Expr Index;

 

-        public AccessRecord(Variable v, Expr IndexZ, Expr IndexY, Expr IndexX)

+        public AccessRecord(Variable v, Expr Index)

         {

             this.v = v;

-            this.IndexZ = IndexZ;

-            this.IndexY = IndexY;

-            this.IndexX = IndexX;

+            this.Index = Index;

         }

 

 

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index f28535c2..2f9ed792 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -21,9 +21,6 @@ namespace GPUVerify
         public static bool Inference = false;

         public static bool ArrayEqualities = false;

         public static string invariantsFile = null;

-        public static bool DividedArray = false;

-        public static string ArrayToCheck = null;

-        public static bool DividedAccesses = false;

 

         public static bool ShowStages = false;

 

@@ -93,28 +90,6 @@ namespace GPUVerify
 

                     break;

 

-                    case "-dividedArray":

-                    case "/dividedArray":

-                    if (hasColonArgument)

-                    {

-                        ArrayToCheck = afterColon;

-                    }

-                    DividedArray = true;

-

-                    break;

-

-                    case "-dividedAccesses":

-                    case "/dividedAccesses":

-                    DividedAccesses = true;

-

-                    break;

-

-                    case "-divided":

-                    case "/divided":

-                    DividedAccesses = true;

-                    DividedArray = true;

-                    break;

-

                     case "-showStages":

                     case "/showStages":

                     ShowStages = true;

@@ -181,11 +156,6 @@ namespace GPUVerify
                         break;

                 }

 

-                if (OnlyDivergence)

-                {

-                    DividedArray = false;

-                    DividedAccesses = false;

-                }

             }

             return 0;

         }

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 68e43242..af7a6cdb 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -24,6 +24,9 @@ namespace GPUVerify
 

         private HashSet<string> ReservedNames = new HashSet<string>();

 

+        internal HashSet<string> OnlyThread1 = new HashSet<string>();

+        internal HashSet<string> OnlyThread2 = new HashSet<string>();

+

         private int TempCounter = 0;

 

         internal const string LOCAL_ID_X_STRING = "local_id_x";

@@ -387,10 +390,7 @@ namespace GPUVerify
                 }

             }

 

-            if (RaceInstrumenter.AddRaceCheckingInstrumentation() == false)

-            {

-                return;

-            }

+            RaceInstrumenter.AddRaceCheckingInstrumentation();

 

             if (CommandLineOptions.ShowStages)

             {

@@ -455,47 +455,6 @@ namespace GPUVerify
 

             emitProgram(outputFilename);

 

-

-            if (CommandLineOptions.DividedAccesses)

-            {

-

-                Program p = GPUVerify.ParseBoogieProgram(new List<string>(new string[] { outputFilename + ".bpl" }), true);

-                ResolutionContext rc = new ResolutionContext(null);

-                p.Resolve(rc);

-                p.Typecheck();

-

-                Contract.Assert(p != null);

-

-                Implementation impl = null;

-

-                {

-                    GPUVerifier tempGPUV = new GPUVerifier("not_used", p, rc, new NullRaceInstrumenter(), true);

-                    tempGPUV.KernelProcedure = tempGPUV.CheckExactlyOneKernelProcedure();

-                    tempGPUV.GetKernelImplementation();

-                    impl = tempGPUV.KernelImplementation;

-                }

-

-                Contract.Assert(impl != null);

-

-                NoConflictingAccessOptimiser opt = new NoConflictingAccessOptimiser(impl);

-                Contract.Assert(opt.NumLogCalls() <= 2);

-                if (opt.NumLogCalls() == 2 && !opt.HasConflicting())

-                {

-                    FileInfo f = new FileInfo(outputFilename);

-                    

-                    string newName = f.Directory.FullName + "\\" + "NO_CONFLICTS_" + f.Name + ".bpl";

-                    //File.Delete(newName);

-                    if (File.Exists(newName))

-                    {

-                        File.Delete(newName);

-                    }

-                    File.Move(outputFilename + ".bpl", newName);

-                    //Console.WriteLine("Renamed " + ouputFilename + "; no conflicting accesses (that are not already tested by other output files).");

-                }

-

-               

-            }

-

         }

 

         private void DoMayBePowerOfTwoAnalysis()

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 4cb24f2c..47965b43 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -126,7 +126,6 @@
     <Compile Include="IKernelArrayInfo.cs" />

     <Compile Include="IRaceInstrumenter.cs" />

     <Compile Include="Main.cs" />

-    <Compile Include="NoConflictingAccessOptimiser.cs" />

     <Compile Include="NonLocalAccessCollector.cs" />

     <Compile Include="NonLocalAccessExtractor.cs" />

     <Compile Include="KernelArrayInfoLists.cs" />

diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs
index 63b1ea1a..5e5cca5c 100644
--- a/Source/GPUVerify/IRaceInstrumenter.cs
+++ b/Source/GPUVerify/IRaceInstrumenter.cs
@@ -11,12 +11,7 @@ namespace GPUVerify
         void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region);

         void AddKernelPrecondition();

 

-        // Summary:

-        // Returns whether we should continue.

-        // E.g. if race checking code could not be added because

-        // the specified accesses to check were read/read or did not exist,

-        // this will return false.

-        bool AddRaceCheckingInstrumentation();

+        void AddRaceCheckingInstrumentation();

 

         void AddRaceCheckingDeclarations();

 

diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs
index fecd26fa..272d0a1b 100644
--- a/Source/GPUVerify/KernelDualiser.cs
+++ b/Source/GPUVerify/KernelDualiser.cs
@@ -106,12 +106,14 @@ namespace GPUVerify {
           if (verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))) {

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

           }

-          else {

+          else if(!verifier.OnlyThread2.Contains(Call.callee)) {

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

+          if (

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

+            && !verifier.OnlyThread1.Contains(Call.callee)) {

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

           }

         }

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index e5a094d5..b11dfc6f 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -88,7 +88,7 @@ namespace GPUVerify
             return null;

         }

 

-        public static bool doit(string filename, Variable v, int a1, int a2)

+/*        public static bool doit(string filename, Variable v, int a1, int a2)

         {

             ResolutionContext rc;

             Program newProgram = parse(out rc);

@@ -121,8 +121,9 @@ namespace GPUVerify
             return !ri.failedToFindSecondAccess;

 

         }

+      */

 

-        public static IList<GPUVerifier> parseProcessOutput()

+        public static void parseProcessOutput()

         {

             string fn = "temp";

             if (CommandLineOptions.outputFile != null)

@@ -137,72 +138,16 @@ namespace GPUVerify
             }

             ResolutionContext rc;

             Program program = parse(out rc);

-            IList<GPUVerifier> result = new List<GPUVerifier>();

             GPUVerifier g = new GPUVerifier(fn, program, rc, new NullRaceInstrumenter());

 

-            if (CommandLineOptions.DividedArray)

+            if (!CommandLineOptions.OnlyDivergence)

             {

-                bool FoundArray = CommandLineOptions.ArrayToCheck == null;

-

-                foreach (Variable v in g.KernelArrayInfo.getAllNonLocalArrays())

-                {

-                    if (CommandLineOptions.DividedAccesses)

-                    {

-                        int i = 0;

-                        int j = 0;

-                        while (true)

-                        {

-                            bool res = doit(fn + "." + v.Name + "." + i + "." + (i + j), v, i, j);

-                            if (!res)

-                            {

-                                if (j == 0)

-                                {

-                                    break;

-                                }

-                                else

-                                {

-                                    i++;

-                                    j = 0;

-                                }

-                            }

-                            else

-                            {

-                                j++;

-                            }

-                        }

-                    }

-                    else

-                    {

-                        if (CommandLineOptions.ArrayToCheck == null || CommandLineOptions.ArrayToCheck.Equals(v.Name))

-                        {

-                            FoundArray = true;

-                            doit("temp_" + v.Name, v, -1, -1);

-                        }

-                    }

-                }

-

-                if (!FoundArray)

-                {

-                    Console.WriteLine("Did not find a non-local array named " + CommandLineOptions.ArrayToCheck);

-                    Environment.Exit(1);

-                }

-

-            }

-            else

-            {

-                if (!CommandLineOptions.OnlyDivergence)

-                {

-                    RaceInstrumenter ri = new RaceInstrumenter();

-                    ri.setVerifier(g);

-                    g.setRaceInstrumenter(ri);

-                }

-

-                g.doit();

-                result.Add(g);

-

+                RaceInstrumenter ri = new RaceInstrumenter();

+                ri.setVerifier(g);

+                g.setRaceInstrumenter(ri);

             }

 

-            return result;

+            g.doit();

             

         }

 

diff --git a/Source/GPUVerify/NoConflictingAccessOptimiser.cs b/Source/GPUVerify/NoConflictingAccessOptimiser.cs
deleted file mode 100644
index f003a3a9..00000000
--- a/Source/GPUVerify/NoConflictingAccessOptimiser.cs
+++ /dev/null
@@ -1,116 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using Microsoft.Boogie;

-using System.Diagnostics.Contracts;

-

-namespace GPUVerify

-{

-    class NoConflictingAccessOptimiser

-    {

-        private Implementation impl;

-        private IList<CallCmdPos> ccs;

-

-        public NoConflictingAccessOptimiser(Implementation impl)

-        {

-            this.impl = impl;

-            ccs = new List<CallCmdPos>();

-            FindCallCmds();

-        }

-

-        private class CallCmdPos

-        {

-            public Block block;

-            public int cmdIndex;

-            public CallCmd cc;

-

-            public CallCmdPos(Block block, int cmdIndex, CallCmd cc)

-            {

-                this.block = block;

-                this.cmdIndex = cmdIndex;

-                this.cc = cc;

-            }

-        }

-

-        public int NumLogCalls()

-        {

-            return ccs.Count;

-        }

-

-        private void FindCallCmds()

-        {

-            foreach (Block b in impl.Blocks)

-            {

-                for(int i=0; i < b.Cmds.Length; i++)

-                {

-                    Cmd c = b.Cmds[i];

-                    CallCmd cc = c as CallCmd;

-                    if (cc != null)

-                    {

-                        if (cc.Proc.Name.Contains("_LOG"))

-                        {

-                            ccs.Add(new CallCmdPos(b, i, cc));

-                        }

-                    }

-                }

-            }

-        }

-

-        public bool HasConflicting()

-        {

-            Contract.Assert(ccs.Count == 2);

-

-            return

-                Reachable(ccs[0].block, ccs[0].cmdIndex, ccs[1].cc, new HashSet<Block>()) ||

-                Reachable(ccs[1].block, ccs[1].cmdIndex, ccs[0].cc, new HashSet<Block>());

-        }

-

-        public bool Reachable(Block startBlock, int cmdStartIndex, CallCmd target, ISet<Block> visited)

-        {

-            Block currBlock = startBlock;

-            int i = cmdStartIndex;

-

-            if(i == 0)

-            {

-                visited.Add(currBlock);

-            }

-

-            while (i < currBlock.Cmds.Length)

-            {

-                CallCmd cc = currBlock.Cmds[i] as CallCmd;

-                if (cc != null)

-                {

-                    if (cc.Proc.Name.Equals("BARRIER"))

-                    {

-                        return false;

-                    }

-

-                    if (target == cc)

-                    {

-                        return true;

-                    }

-                }

-                i++;

-            }

-            

-            

-            //end of block

-                

-            GotoCmd gc = currBlock.TransferCmd as GotoCmd;

-            Contract.Assert(gc != null);

-            foreach (Block t in gc.labelTargets)

-            {

-                if(visited.Contains(t))

-                    continue;

-

-                if (Reachable(t, 0, target, visited))

-                    return true;

-            }

-

-            return false;

-

-        }

-

-    }

-}

diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs
index acba7ca6..458481a0 100644
--- a/Source/GPUVerify/NullRaceInstrumenter.cs
+++ b/Source/GPUVerify/NullRaceInstrumenter.cs
@@ -19,9 +19,9 @@ namespace GPUVerify
             

         }

 

-        public bool AddRaceCheckingInstrumentation()

+        public void AddRaceCheckingInstrumentation()

         {

-            return true;

+

         }

 

         public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)

diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
index 2e7e42d2..3d60b495 100644
--- a/Source/GPUVerify/RaceInstrumenter.cs
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -7,1108 +7,947 @@ using System.Diagnostics.Contracts;
 using Microsoft.Boogie;

 using Microsoft.Basetypes;

 

-namespace GPUVerify

-{

-    class RaceInstrumenter : IRaceInstrumenter

-    {

-        protected GPUVerifier verifier;

-

-        public IKernelArrayInfo NonLocalStateToCheck;

-

-        public int onlyLog1;

-        public int onlyLog2;

-        public bool failedToFindSecondAccess;

-        public bool addedLogWrite;

-        private int logAddCount;

-

-        private Dictionary<string, Procedure> logAccessProcedures = new Dictionary<string, Procedure>();

-

-        public RaceInstrumenter()

-        {

-            onlyLog1 = -1;

-            onlyLog2 = -1;

-            failedToFindSecondAccess = false;

-            addedLogWrite = false;

-            logAddCount = 0;

-        }

+namespace GPUVerify {

+  class RaceInstrumenter : IRaceInstrumenter {

+    protected GPUVerifier verifier;

 

-        public void setVerifier(GPUVerifier verifier)

-        {

-            this.verifier = verifier;

-            NonLocalStateToCheck = new KernelArrayInfoLists();

-            foreach(Variable v in verifier.KernelArrayInfo.getGlobalArrays())

-            {

-                NonLocalStateToCheck.getGlobalArrays().Add(v);

-            }

-            foreach(Variable v in verifier.KernelArrayInfo.getGroupSharedArrays())

-            {

-                NonLocalStateToCheck.getGroupSharedArrays().Add(v);

-            }

-        }

+    private QKeyValue SourceLocationAttributes = null;

 

-        private void AddNoReadOrWriteCandidateInvariants(IRegion region, Variable v)

-        {

-            // Reasoning: if READ_HAS_OCCURRED_v is not in the modifies set for the

-            // loop then there is no point adding an invariant

-            //

-            // If READ_HAS_OCCURRED_v is in the modifies set, but the loop does not

-            // contain a barrier, then it is almost certain that a read CAN be

-            // pending at the loop head, so the invariant will not hold

-            //

-            // If there is a barrier in the loop body then READ_HAS_OCCURRED_v will

-            // be in the modifies set, but there may not be a live read at the loop

-            // head, so it is worth adding the loop invariant candidate.

-            //

-            // The same reasoning applies for WRITE

-

-            if (verifier.ContainsBarrierCall(region))

-            {

-                if (verifier.ContainsNamedVariable(

-                    LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ")))

-                {

-                    AddNoReadOrWriteCandidateInvariant(region, v, "READ");

-                }

+    public IKernelArrayInfo NonLocalStateToCheck;

 

-                if (verifier.ContainsNamedVariable(

-                    LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE")))

-                {

-                    AddNoReadOrWriteCandidateInvariant(region, v, "WRITE");

-                }

-            }

-        }

+    private Dictionary<string, Procedure> RaceCheckingProcedures = new Dictionary<string, Procedure>();

 

-        private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v)

-        {

-            AddNoReadOrWriteCandidateRequires(Proc, v, "READ", "1");

-            AddNoReadOrWriteCandidateRequires(Proc, v, "WRITE", "1");

-        }

+    public void setVerifier(GPUVerifier verifier) {

+      this.verifier = verifier;

+      NonLocalStateToCheck = new KernelArrayInfoLists();

+      foreach (Variable v in verifier.KernelArrayInfo.getGlobalArrays()) {

+        NonLocalStateToCheck.getGlobalArrays().Add(v);

+      }

+      foreach (Variable v in verifier.KernelArrayInfo.getGroupSharedArrays()) {

+        NonLocalStateToCheck.getGroupSharedArrays().Add(v);

+      }

+    }

 

-        private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v)

-        {

-            AddNoReadOrWriteCandidateEnsures(Proc, v, "READ", "1");

-            AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "1");

-        }

+    private void AddNoReadOrWriteCandidateInvariants(IRegion region, Variable v) {

+      // Reasoning: if READ_HAS_OCCURRED_v is not in the modifies set for the

+      // loop then there is no point adding an invariant

+      //

+      // If READ_HAS_OCCURRED_v is in the modifies set, but the loop does not

+      // contain a barrier, then it is almost certain that a read CAN be

+      // pending at the loop head, so the invariant will not hold

+      //

+      // If there is a barrier in the loop body then READ_HAS_OCCURRED_v will

+      // be in the modifies set, but there may not be a live read at the loop

+      // head, so it is worth adding the loop invariant candidate.

+      //

+      // The same reasoning applies for WRITE

+

+      if (verifier.ContainsBarrierCall(region)) {

+        if (verifier.ContainsNamedVariable(

+            LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ"))) {

+          AddNoReadOrWriteCandidateInvariant(region, v, "READ");

+        }

+

+        if (verifier.ContainsNamedVariable(

+            LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE"))) {

+          AddNoReadOrWriteCandidateInvariant(region, v, "WRITE");

+        }

+      }

+    }

 

-        private void AddNoReadOrWriteCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)

-        {

-            Expr candidate = NoReadOrWriteExpr(v, ReadOrWrite, "1");

-            verifier.AddCandidateInvariant(region, candidate, "no " + ReadOrWrite.ToLower());

-        }

+    private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v) {

+      AddNoReadOrWriteCandidateRequires(Proc, v, "READ", "1");

+      AddNoReadOrWriteCandidateRequires(Proc, v, "WRITE", "1");

+    }

 

-        public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region)

-        {

-            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())

-            {

-                AddNoReadOrWriteCandidateInvariants(region, v);

-                AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "READ");

-                AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "WRITE");

-                AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "READ", CollectOffsetPredicates(impl, region, v, "READ"));

-                AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "WRITE", CollectOffsetPredicates(impl, region, v, "WRITE"));

-            }

+    private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v) {

+      AddNoReadOrWriteCandidateEnsures(Proc, v, "READ", "1");

+      AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "1");

+    }

+

+    private void AddNoReadOrWriteCandidateInvariant(IRegion region, Variable v, string ReadOrWrite) {

+      Expr candidate = NoReadOrWriteExpr(v, ReadOrWrite, "1");

+      verifier.AddCandidateInvariant(region, candidate, "no " + ReadOrWrite.ToLower());

+    }

+

+    public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region) {

+      foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {

+        AddNoReadOrWriteCandidateInvariants(region, v);

+        AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "READ");

+        AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "WRITE");

+        AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "READ", CollectOffsetPredicates(impl, region, v, "READ"));

+        AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "WRITE", CollectOffsetPredicates(impl, region, v, "WRITE"));

+      }

+    }

+

+    private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag) {

+      Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);

+      verifier.AddCandidateInvariant(region, candidate, tag);

+    }

+

+    private bool DoesNotReferTo(Expr expr, string v) {

+      FindReferencesToNamedVariableVisitor visitor = new FindReferencesToNamedVariableVisitor(v);

+      visitor.VisitExpr(expr);

+      return !visitor.found;

+    }

+

+    private List<Expr> CollectOffsetPredicates(Implementation impl, IRegion region, Variable v, string accessType) {

+      var offsetVar = new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, accessType));

+      var offsetExpr = new IdentifierExpr(Token.NoToken, offsetVar);

+      var offsetPreds = new List<Expr>();

+

+      foreach (var offset in GetOffsetsAccessed(region, v, accessType)) {

+        bool isConstant;

+        var def = verifier.varDefAnalyses[impl].SubstDefinitions(offset, impl.Name, out isConstant);

+        if (def == null)

+          continue;

+

+        if (isConstant) {

+          offsetPreds.Add(Expr.Eq(offsetExpr, def));

+        }

+        else {

+          var sc = StrideConstraint.FromExpr(verifier, impl, def);

+          var pred = sc.MaybeBuildPredicate(verifier, offsetExpr);

+          if (pred != null)

+            offsetPreds.Add(pred);

         }

+      }

+

+      return offsetPreds;

+    }

 

-        private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag)

-        {

-            Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);

-            verifier.AddCandidateInvariant(region, candidate, tag);

+    private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType) {

+      KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(region.Guard());

+      if (iLessThanC.Key != null) {

+        foreach (Expr e in GetOffsetsAccessed(region, v, accessType)) {

+          if (HasFormIPlusLocalIdTimesC(e, iLessThanC, impl)) {

+            AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(region, v, iLessThanC.Value, accessType);

+            break;

+          }

         }

 

-        private bool DoesNotReferTo(Expr expr, string v)

-        {

-            FindReferencesToNamedVariableVisitor visitor = new FindReferencesToNamedVariableVisitor(v);

-            visitor.VisitExpr(expr);

-            return !visitor.found;

+        foreach (Expr e in GetOffsetsAccessed(region, v, accessType)) {

+          if (HasFormIPlusGlobalIdTimesC(e, iLessThanC, impl)) {

+            AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(region, v, iLessThanC.Value, accessType);

+            break;

+          }

         }

 

-        private List<Expr> CollectOffsetPredicates(Implementation impl, IRegion region, Variable v, string accessType)

-        {

-            var offsetVar = new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, accessType));

-            var offsetExpr = new IdentifierExpr(Token.NoToken, offsetVar);

-            var offsetPreds = new List<Expr>();

-

-            foreach (var offset in GetOffsetsAccessed(region, v, accessType))

-            {

-                bool isConstant;

-                var def = verifier.varDefAnalyses[impl].SubstDefinitions(offset, impl.Name, out isConstant);

-                if (def == null)

-                    continue;

-

-                if (isConstant)

-                {

-                    offsetPreds.Add(Expr.Eq(offsetExpr, def));

-                }

-                else

-                {

-                    var sc = StrideConstraint.FromExpr(verifier, impl, def);

-                    var pred = sc.MaybeBuildPredicate(verifier, offsetExpr);

-                    if (pred != null)

-                        offsetPreds.Add(pred);

-                }

-            }

+      }

 

-            return offsetPreds;

-        }

 

-        private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType)

-        {

-            KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(region.Guard());

-            if (iLessThanC.Key != null)

-            {

-                foreach (Expr e in GetOffsetsAccessed(region, v, accessType))

-                {

-                    if(HasFormIPlusLocalIdTimesC(e, iLessThanC, impl))

-                    {

-                        AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(region, v, iLessThanC.Value, accessType);

-                        break;

-                    }

-                }

+    }

 

-                foreach (Expr e in GetOffsetsAccessed(region, v, accessType))

-                {

-                    if (HasFormIPlusGlobalIdTimesC(e, iLessThanC, impl))

-                    {

-                        AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(region, v, iLessThanC.Value, accessType);

-                        break;

-                    }

-                }

-            

-            }

+    private bool HasFormIPlusLocalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl) {

+      if (!(e is NAryExpr)) {

+        return false;

+      }

 

-        

-        }

+      NAryExpr nary = e as NAryExpr;

 

-        private bool HasFormIPlusLocalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl)

-        {

-            if (!(e is NAryExpr))

-            {

-                return false;

-            }

+      if (!nary.Fun.FunctionName.Equals("BV32_ADD")) {

+        return false;

+      }

 

-            NAryExpr nary = e as NAryExpr;

+      return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&

+          IsLocalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||

+          (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&

+          IsLocalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));

+    }

 

-            if (!nary.Fun.FunctionName.Equals("BV32_ADD"))

-            {

-                return false;

-            }

+    private bool IsLocalIdTimesConstant(Expr maybeLocalIdTimesConstant, Expr constant, Implementation impl) {

+      if (!(maybeLocalIdTimesConstant is NAryExpr)) {

+        return false;

+      }

+      NAryExpr nary = maybeLocalIdTimesConstant as NAryExpr;

+      if (!nary.Fun.FunctionName.Equals("BV32_MUL")) {

+        return false;

+      }

+

+      return

+          (SameConstant(nary.Args[0], constant) && verifier.IsLocalId(nary.Args[1], 0, impl)) ||

+          (SameConstant(nary.Args[1], constant) && verifier.IsLocalId(nary.Args[0], 0, impl));

+    }

 

-            return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&

-                IsLocalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||

-                (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&

-                IsLocalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));

-        }

 

-        private bool IsLocalIdTimesConstant(Expr maybeLocalIdTimesConstant, Expr constant, Implementation impl)

-        {

-            if (!(maybeLocalIdTimesConstant is NAryExpr))

-            {

-                return false;

-            }

-            NAryExpr nary = maybeLocalIdTimesConstant as NAryExpr;

-            if(!nary.Fun.FunctionName.Equals("BV32_MUL"))

-            {

-                return false;

-            }

+    private bool HasFormIPlusGlobalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl) {

+      if (!(e is NAryExpr)) {

+        return false;

+      }

 

-            return

-                (SameConstant(nary.Args[0], constant) && verifier.IsLocalId(nary.Args[1], 0, impl)) ||

-                (SameConstant(nary.Args[1], constant) && verifier.IsLocalId(nary.Args[0], 0, impl));

-        }

+      NAryExpr nary = e as NAryExpr;

 

+      if (!nary.Fun.FunctionName.Equals("BV32_ADD")) {

+        return false;

+      }

 

-        private bool HasFormIPlusGlobalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl)

-        {

-            if (!(e is NAryExpr))

-            {

-                return false;

-            }

+      return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&

+          IsGlobalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||

+          (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&

+          IsGlobalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));

+    }

 

-            NAryExpr nary = e as NAryExpr;

+    private bool IsGlobalIdTimesConstant(Expr maybeGlobalIdTimesConstant, Expr constant, Implementation impl) {

+      if (!(maybeGlobalIdTimesConstant is NAryExpr)) {

+        return false;

+      }

+      NAryExpr nary = maybeGlobalIdTimesConstant as NAryExpr;

+      if (!nary.Fun.FunctionName.Equals("BV32_MUL")) {

+        return false;

+      }

+

+      return

+          (SameConstant(nary.Args[0], constant) && verifier.IsGlobalId(nary.Args[1], 0, impl)) ||

+          (SameConstant(nary.Args[1], constant) && verifier.IsGlobalId(nary.Args[0], 0, impl));

+    }

 

-            if (!nary.Fun.FunctionName.Equals("BV32_ADD"))

-            {

-                return false;

-            }

 

-            return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&

-                IsGlobalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||

-                (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&

-                IsGlobalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));

+    private bool SameConstant(Expr expr, Expr constant) {

+      if (constant is IdentifierExpr) {

+        IdentifierExpr identifierExpr = constant as IdentifierExpr;

+        Debug.Assert(identifierExpr.Decl is Constant);

+        return expr is IdentifierExpr && (expr as IdentifierExpr).Decl is Constant && (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Decl.Name);

+      }

+      else {

+        Debug.Assert(constant is LiteralExpr);

+        LiteralExpr literalExpr = constant as LiteralExpr;

+        if (!(expr is LiteralExpr)) {

+          return false;

+        }

+        if (!(literalExpr.Val is BvConst) || !((expr as LiteralExpr).Val is BvConst)) {

+          return false;

         }

 

-        private bool IsGlobalIdTimesConstant(Expr maybeGlobalIdTimesConstant, Expr constant, Implementation impl)

-        {

-            if (!(maybeGlobalIdTimesConstant is NAryExpr))

-            {

-                return false;

-            }

-            NAryExpr nary = maybeGlobalIdTimesConstant as NAryExpr;

-            if (!nary.Fun.FunctionName.Equals("BV32_MUL"))

-            {

-                return false;

-            }

+        return (literalExpr.Val as BvConst).Value.ToInt == ((expr as LiteralExpr).Val as BvConst).Value.ToInt;

+      }

+    }

 

-            return

-                (SameConstant(nary.Args[0], constant) && verifier.IsGlobalId(nary.Args[1], 0, impl)) ||

-                (SameConstant(nary.Args[1], constant) && verifier.IsGlobalId(nary.Args[0], 0, impl));

-        }

+    private bool SameIdentifierExpression(Expr expr, IdentifierExpr identifierExpr) {

+      if (!(expr is IdentifierExpr)) {

+        return false;

+      }

+      return (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Name);

+    }

 

+    private KeyValuePair<IdentifierExpr, Expr> GetILessThanC(Expr expr) {

 

-        private bool SameConstant(Expr expr, Expr constant)

-        {

-            if (constant is IdentifierExpr)

-            {

-                IdentifierExpr identifierExpr = constant as IdentifierExpr;

-                Debug.Assert(identifierExpr.Decl is Constant);

-                return expr is IdentifierExpr && (expr as IdentifierExpr).Decl is Constant && (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Decl.Name);

-            }

-            else

-            {

-                Debug.Assert(constant is LiteralExpr);

-                LiteralExpr literalExpr = constant as LiteralExpr;

-                if (!(expr is LiteralExpr))

-                {

-                    return false;

-                }

-                if (!(literalExpr.Val is BvConst) || !((expr as LiteralExpr).Val is BvConst))

-                {

-                    return false;

-                }

+      if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("bv32_to_bool")) {

+        expr = (expr as NAryExpr).Args[0];

+      }

 

-                return (literalExpr.Val as BvConst).Value.ToInt == ((expr as LiteralExpr).Val as BvConst).Value.ToInt;

-            }

-        }

+      if (!(expr is NAryExpr)) {

+        return new KeyValuePair<IdentifierExpr, Expr>(null, null);

+      }

 

-        private bool SameIdentifierExpression(Expr expr, IdentifierExpr identifierExpr)

-        {

-            if (!(expr is IdentifierExpr))

-            {

-                return false;

-            }

-            return (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Name);

-        }

+      NAryExpr nary = expr as NAryExpr;

 

-        private KeyValuePair<IdentifierExpr, Expr> GetILessThanC(Expr expr)

-        {

+      if (!(nary.Fun.FunctionName.Equals("BV32_C_LT") || nary.Fun.FunctionName.Equals("BV32_LT"))) {

+        return new KeyValuePair<IdentifierExpr, Expr>(null, null);

+      }

 

-            if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("bv32_to_bool"))

-            {

-                expr = (expr as NAryExpr).Args[0];

-            }

+      if (!(nary.Args[0] is IdentifierExpr)) {

+        return new KeyValuePair<IdentifierExpr, Expr>(null, null);

+      }

 

-            if (!(expr is NAryExpr))

-            {

-                return new KeyValuePair<IdentifierExpr, Expr>(null, null);

-            }

+      if (!IsConstant(nary.Args[1])) {

+        return new KeyValuePair<IdentifierExpr, Expr>(null, null);

+      }

 

-            NAryExpr nary = expr as NAryExpr;

+      return new KeyValuePair<IdentifierExpr, Expr>(nary.Args[0] as IdentifierExpr, nary.Args[1]);

 

-            if (!(nary.Fun.FunctionName.Equals("BV32_C_LT") || nary.Fun.FunctionName.Equals("BV32_LT")))

-            {

-                return new KeyValuePair<IdentifierExpr, Expr>(null, null);

-            }

+    }

 

-            if (!(nary.Args[0] is IdentifierExpr))

-            {

-                return new KeyValuePair<IdentifierExpr, Expr>(null, null);

-            }

+    private static bool IsConstant(Expr e) {

+      return ((e is IdentifierExpr && (e as IdentifierExpr).Decl is Constant) || e is LiteralExpr);

+    }

 

-            if (!IsConstant(nary.Args[1]))

-            {

-                return new KeyValuePair<IdentifierExpr, Expr>(null, null);

-            }

+    private void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v) {

+      AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 1);

+      AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 1);

+    }

 

-            return new KeyValuePair<IdentifierExpr, Expr>(nary.Args[0] as IdentifierExpr, nary.Args[1]);

+    private void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v) {

+      AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "WRITE", 1);

+      AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);

+    }

 

-        }

+    public void AddKernelPrecondition() {

+      foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {

+        AddRequiresNoPendingAccess(v);

 

-        private static bool IsConstant(Expr e)

-        {

-            return ((e is IdentifierExpr && (e as IdentifierExpr).Decl is Constant) || e is LiteralExpr);

+        if (!verifier.ArrayModelledAdversarially(v)) {

+          IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));

+          IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));

+          verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.Eq(v1, v2)));

         }

+      }

+    }

 

-        private void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v)

-        {

-            AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 1);

-            AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 1);

-        }

+    public void AddRaceCheckingInstrumentation() {

 

-        private void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v)

-        {

-            AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "WRITE", 1);

-            AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);

+      foreach (Declaration d in verifier.Program.TopLevelDeclarations) {

+        if (d is Implementation) {

+          AddRaceCheckCalls(d as Implementation);

         }

+      }

 

-        public void AddKernelPrecondition()

-        {

-            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())

-            {

-                AddRequiresNoPendingAccess(v);

-

-                if (!verifier.ArrayModelledAdversarially(v))

-                {

-                    IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));

-                    IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));

-                    verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.Eq(v1, v2)));

-                }

-            }

-        }

+    }

 

-        public bool AddRaceCheckingInstrumentation()

-        {

+    private void AddRaceCheckingDecsAndProcsForVar(Variable v) {

+      AddLogRaceDeclarations(v, "READ");

+      AddLogRaceDeclarations(v, "WRITE");

+      AddLogAccessProcedure(v, "READ");

+      AddCheckAccessProcedure(v, "READ");

+      AddLogAccessProcedure(v, "WRITE");

+      AddCheckAccessProcedure(v, "WRITE");

+    }

 

-            if (onlyLog1 != -1)

-            {

-                addedLogWrite = false;

-                failedToFindSecondAccess = true;

-            }

-            else

-            {

-                addedLogWrite = true;

-                failedToFindSecondAccess = false;

-            }

+    private StmtList AddRaceCheckCalls(StmtList stmtList) {

+      Contract.Requires(stmtList != null);

 

-            foreach (Declaration d in verifier.Program.TopLevelDeclarations)

-            {

-                if (d is Implementation)

-                {

-                    AddRaceCheckCalls(d as Implementation);

-                }

-            }

+      StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);

 

-            if (failedToFindSecondAccess || !addedLogWrite)

-                return false;

+      foreach (BigBlock bodyBlock in stmtList.BigBlocks) {

+        result.BigBlocks.Add(AddRaceCheckCalls(bodyBlock));

+      }

+      return result;

+    }

 

-            return true;

+    private Block AddRaceCheckCalls(Block b) {

+      b.Cmds = AddRaceCheckCalls(b.Cmds);

+      return b;

+    }

 

-        }

+    private void AddRaceCheckCalls(Implementation impl) {

+      if (CommandLineOptions.Unstructured)

+        impl.Blocks = impl.Blocks.Select(AddRaceCheckCalls).ToList();

+      else

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

+    }

 

-        private void AddRaceCheckingDecsAndProcsForVar(Variable v)

-        {

-            AddLogRaceDeclarations(v, "READ");

-            AddLogRaceDeclarations(v, "WRITE");

-            AddLogAccessProcedure(v, "READ");

-            AddLogAccessProcedure(v, "WRITE");

+    private CmdSeq AddRaceCheckCalls(CmdSeq cs) {

+      var result = new CmdSeq();

+      foreach (Cmd c in cs) {

+        result.Add(c);

 

+        if (c is AssertCmd) {

+          AssertCmd assertion = c as AssertCmd;

+          if (QKeyValue.FindBoolAttribute(assertion.Attributes, "sourceloc")) {

+            SourceLocationAttributes = assertion.Attributes;

+          }

         }

-        

-        private StmtList AddRaceCheckCalls(StmtList stmtList)

-        {

-            Contract.Requires(stmtList != null);

 

-            StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);

+        if (c is AssignCmd) {

+          AssignCmd assign = c as AssignCmd;

 

-            foreach (BigBlock bodyBlock in stmtList.BigBlocks)

-            {

-                result.BigBlocks.Add(AddRaceCheckCalls(bodyBlock));

-            }

-            return result;

-        }

+          ReadCollector rc = new ReadCollector(NonLocalStateToCheck);

+          foreach (var rhs in assign.Rhss)

+            rc.Visit(rhs);

+          if (rc.accesses.Count > 0) {

+            foreach (AccessRecord ar in rc.accesses) {

 

-        private Block AddRaceCheckCalls(Block b)

-        {

-            b.Cmds = AddRaceCheckCalls(b.Cmds);

-            return b;

-        }

+              ExprSeq inParams = new ExprSeq();

+              inParams.Add(ar.Index);

 

-        private void AddRaceCheckCalls(Implementation impl)

-        {

-            if (CommandLineOptions.Unstructured)

-                impl.Blocks = impl.Blocks.Select(AddRaceCheckCalls).ToList();

-            else

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

-        }

+              Procedure logProcedure = GetRaceCheckingProcedure(c.tok, "_LOG_READ_" + ar.v.Name);

+              Procedure checkProcedure = GetRaceCheckingProcedure(c.tok, "_CHECK_READ_" + ar.v.Name);

 

-        private bool shouldAddLogCallAndIncr()

-        {

-            Contract.Assert(onlyLog1 >= -1);

-            int oldLogAddCount = logAddCount;

-            ++logAddCount;

+              verifier.OnlyThread1.Add(logProcedure.Name);

+              verifier.OnlyThread2.Add(checkProcedure.Name);

 

-            if (onlyLog1 == -1)

-            {

-                return true;

-            }

+              CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());

+              logAccessCallCmd.Proc = logProcedure;

 

-            if(onlyLog1 + onlyLog2 == oldLogAddCount)

-            {

-                failedToFindSecondAccess = false;

-                return true;

-            }

+              CallCmd checkAccessCallCmd = new CallCmd(c.tok, checkProcedure.Name, inParams, new IdentifierExprSeq());

+              checkAccessCallCmd.Proc = checkProcedure;

+              checkAccessCallCmd.Attributes = SourceLocationAttributes;

+

+              result.Add(logAccessCallCmd);

+              result.Add(checkAccessCallCmd);

 

-            if (onlyLog1 == oldLogAddCount)

-            {

-                return true;

             }

+          }

 

-            return false;

-        }

+          foreach (var lhs in assign.Lhss) {

+            WriteCollector wc = new WriteCollector(NonLocalStateToCheck);

+            wc.Visit(lhs);

+            if (wc.GetAccess() != null) {

+              AccessRecord ar = wc.GetAccess();

 

-        private CmdSeq AddRaceCheckCalls(CmdSeq cs)

-        {

-            var result = new CmdSeq();

-            foreach (Cmd c in cs)

-            {

-                result.Add(c);

-                if (c is AssignCmd)

-                {

-                    AssignCmd assign = c as AssignCmd;

-

-                    ReadCollector rc = new ReadCollector(NonLocalStateToCheck);

-                    foreach (var rhs in assign.Rhss)

-                        rc.Visit(rhs);

-                    if (rc.accesses.Count > 0)

-                    {

-                        foreach (AccessRecord ar in rc.accesses)

-                        {

-                            if (shouldAddLogCallAndIncr())

-                            {

-

-                                ExprSeq inParams = new ExprSeq();

-                                if (ar.IndexZ != null)

-                                {

-                                    inParams.Add(ar.IndexZ);

-                                }

-                                if (ar.IndexY != null)

-                                {

-                                    inParams.Add(ar.IndexY);

-                                }

-                                if (ar.IndexX != null)

-                                {

-                                    inParams.Add(ar.IndexX);

-                                }

-

-                                Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_READ_" + ar.v.Name);

-

-                                CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());

-

-                                logAccessCallCmd.Proc = logProcedure;

-

-                                result.Add(logAccessCallCmd);

-

-                            }

-                        }

-                    }

-

-                    foreach (var lhs in assign.Lhss)

-                    {

-                        WriteCollector wc = new WriteCollector(NonLocalStateToCheck);

-                        wc.Visit(lhs);

-                        if (wc.GetAccess() != null)

-                        {

-                            AccessRecord ar = wc.GetAccess();

-

-                            if (shouldAddLogCallAndIncr())

-                            {

-

-                                ExprSeq inParams = new ExprSeq();

-                                if (ar.IndexZ != null)

-                                {

-                                    inParams.Add(ar.IndexZ);

-                                }

-                                if (ar.IndexY != null)

-                                {

-                                    inParams.Add(ar.IndexY);

-                                }

-                                if (ar.IndexX != null)

-                                {

-                                    inParams.Add(ar.IndexX);

-                                }

-

-                                Procedure logProcedure = GetLogAccessProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);

-

-                                CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());

-

-                                logAccessCallCmd.Proc = logProcedure;

-

-                                result.Add(logAccessCallCmd);

-

-                                addedLogWrite = true;

-

-                            }

-                        }

-                    }

-                }

-            }

-            return result;

-        }

+              ExprSeq inParams = new ExprSeq();

+              inParams.Add(ar.Index);

 

-        private BigBlock AddRaceCheckCalls(BigBlock bb)

-        {

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

+              Procedure logProcedure = GetRaceCheckingProcedure(c.tok, "_LOG_WRITE_" + ar.v.Name);

+              Procedure checkProcedure = GetRaceCheckingProcedure(c.tok, "_CHECK_WRITE_" + ar.v.Name);

 

-            if (bb.ec is WhileCmd)

-            {

-                WhileCmd WhileCommand = bb.ec as WhileCmd;

-                result.ec = new WhileCmd(WhileCommand.tok, WhileCommand.Guard, 

-                        WhileCommand.Invariants, AddRaceCheckCalls(WhileCommand.Body));

-            }

-            else if (bb.ec is IfCmd)

-            {

-                IfCmd IfCommand = bb.ec as IfCmd;

-                Debug.Assert(IfCommand.elseIf == null); // We don't handle else if yet

-                result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, AddRaceCheckCalls(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? AddRaceCheckCalls(IfCommand.elseBlock) : null);

-            }

-            else if (bb.ec is BreakCmd)

-            {

-                result.ec = bb.ec;

-            }

-            else

-            {

-                Debug.Assert(bb.ec == null);

-            }

+              verifier.OnlyThread1.Add(logProcedure.Name);

+              verifier.OnlyThread2.Add(checkProcedure.Name);

 

-            return result;

-        }

+              CallCmd logAccessCallCmd = new CallCmd(c.tok, logProcedure.Name, inParams, new IdentifierExprSeq());

+              CallCmd checkAccessCallCmd = new CallCmd(c.tok, checkProcedure.Name, inParams, new IdentifierExprSeq());

+

+              logAccessCallCmd.Proc = logProcedure;

+              checkAccessCallCmd.Proc = checkProcedure;

+

+              result.Add(logAccessCallCmd);

+              result.Add(checkAccessCallCmd);

 

-        private Procedure GetLogAccessProcedure(IToken tok, string name)

-        {

-            if (logAccessProcedures.ContainsKey(name))

-            {

-                return logAccessProcedures[name];

             }

-            Procedure newProcedure = new Procedure(tok, name, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

-            logAccessProcedures[name] = newProcedure;

-            return newProcedure;

+          }

         }

+      }

+      return result;

+    }

 

+    private BigBlock AddRaceCheckCalls(BigBlock bb) {

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

+

+      if (bb.ec is WhileCmd) {

+        WhileCmd WhileCommand = bb.ec as WhileCmd;

+        result.ec = new WhileCmd(WhileCommand.tok, WhileCommand.Guard,

+                WhileCommand.Invariants, AddRaceCheckCalls(WhileCommand.Body));

+      }

+      else if (bb.ec is IfCmd) {

+        IfCmd IfCommand = bb.ec as IfCmd;

+        Debug.Assert(IfCommand.elseIf == null); // We don't handle else if yet

+        result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, AddRaceCheckCalls(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? AddRaceCheckCalls(IfCommand.elseBlock) : null);

+      }

+      else if (bb.ec is BreakCmd) {

+        result.ec = bb.ec;

+      }

+      else {

+        Debug.Assert(bb.ec == null);

+      }

+

+      return result;

+    }

 

-        public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)

-        {

-            BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);

-            if (Thread == 2)

-            {

-                return result;

-            }

+    private Procedure GetRaceCheckingProcedure(IToken tok, string name) {

+      if (RaceCheckingProcedures.ContainsKey(name)) {

+        return RaceCheckingProcedures[name];

+      }

+      Procedure newProcedure = new Procedure(tok, name, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());

+      RaceCheckingProcedures[name] = newProcedure;

+      return newProcedure;

+    }

 

-            Expr ResetReadAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,

-                new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))));

-            Expr ResetWriteAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,

-                new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));

 

-            if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v))

-            {

-                ResetReadAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetReadAssumeGuard);

-                ResetWriteAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);

-            }

+    public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread) {

+      BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);

+      if (Thread == 2) {

+        return result;

+      }

 

-            result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetReadAssumeGuard));

-            result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetWriteAssumeGuard));

-            return result;

-        }

+      Expr ResetReadAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,

+          new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))));

+      Expr ResetWriteAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,

+          new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));

 

-        protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite)

-        {

-            VariableSeq inParams = new VariableSeq();

+      if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v)) {

+        ResetReadAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetReadAssumeGuard);

+        ResetWriteAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);

+      }

 

-            Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));

+      result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetReadAssumeGuard));

+      result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetWriteAssumeGuard));

+      return result;

+    }

 

-            Debug.Assert(v.TypedIdent.Type is MapType);

-            MapType mt = v.TypedIdent.Type as MapType;

-            Debug.Assert(mt.Arguments.Length == 1);

-            Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));

-            Debug.Assert(!(mt.Result is MapType));

+    protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite) {

+      VariableSeq inParams = new VariableSeq();

 

-            inParams.Add(new VariableDualiser(1, null, null).VisitVariable(PredicateParameter.Clone() as Variable));

-            inParams.Add(new VariableDualiser(1, null, null).VisitVariable(OffsetParameter.Clone() as Variable));

+      Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));

 

-            inParams.Add(new VariableDualiser(2, null, null).VisitVariable(PredicateParameter.Clone() as Variable));

-            inParams.Add(new VariableDualiser(2, null, null).VisitVariable(OffsetParameter.Clone() as Variable));

+      Debug.Assert(v.TypedIdent.Type is MapType);

+      MapType mt = v.TypedIdent.Type as MapType;

+      Debug.Assert(mt.Arguments.Length == 1);

+      Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));

+      Debug.Assert(!(mt.Result is MapType));

 

-            string LogProcedureName = "_LOG_" + ReadOrWrite + "_" + v.Name;

+      inParams.Add(new VariableDualiser(1, null, null).VisitVariable(PredicateParameter.Clone() as Variable));

+      inParams.Add(new VariableDualiser(1, null, null).VisitVariable(OffsetParameter.Clone() as Variable));

 

-            Procedure result = GetLogAccessProcedure(v.tok, LogProcedureName);

+      string LogProcedureName = "_LOG_" + ReadOrWrite + "_" + v.Name;

 

-            result.InParams = inParams;

+      Procedure result = GetRaceCheckingProcedure(v.tok, LogProcedureName);

 

-            result.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

+      result.InParams = inParams;

 

-            return result;

-        }

+      result.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

 

-        public void AddRaceCheckingCandidateRequires(Procedure Proc)

-        {

-            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())

-            {

-                AddNoReadOrWriteCandidateRequires(Proc, v);

-                AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);

-            }

+      return result;

+    }

 

-            DoHoudiniPointerAnalysis(Proc);

+    protected Procedure MakeCheckAccessProcedureHeader(Variable v, string ReadOrWrite) {

+      VariableSeq inParams = new VariableSeq();

 

-        }

+      Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));

 

-        private void DoHoudiniPointerAnalysis(Procedure Proc)

-        {

-            HashSet<string> alreadyConsidered = new HashSet<string>();

+      Debug.Assert(v.TypedIdent.Type is MapType);

+      MapType mt = v.TypedIdent.Type as MapType;

+      Debug.Assert(mt.Arguments.Length == 1);

+      Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));

+      Debug.Assert(!(mt.Result is MapType));

 

-            foreach (Variable v in Proc.InParams)

-            {

-                string strippedVarName = GPUVerifier.StripThreadIdentifier(v.Name);

-                if (alreadyConsidered.Contains(strippedVarName))

-                {

-                    continue;

-                }

-                alreadyConsidered.Add(strippedVarName);

-                if (v.TypedIdent.Type is CtorType)

-                {

-                    CtorType ct = v.TypedIdent.Type as CtorType;

-                    if (ct.Decl.Name.Equals("ptr"))

-                    {

-                        foreach (var arrayCollection in new ICollection<Variable>[] { 

+      inParams.Add(new VariableDualiser(2, null, null).VisitVariable(PredicateParameter.Clone() as Variable));

+      inParams.Add(new VariableDualiser(2, null, null).VisitVariable(OffsetParameter.Clone() as Variable));

+

+      string CheckProcedureName = "_CHECK_" + ReadOrWrite + "_" + v.Name;

+

+      Procedure result = GetRaceCheckingProcedure(v.tok, CheckProcedureName);

+

+      result.InParams = inParams;

+

+      result.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

+

+      return result;

+    }

+

+    public void AddRaceCheckingCandidateRequires(Procedure Proc) {

+      foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {

+        AddNoReadOrWriteCandidateRequires(Proc, v);

+        AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);

+      }

+

+      DoHoudiniPointerAnalysis(Proc);

+

+    }

+

+    private void DoHoudiniPointerAnalysis(Procedure Proc) {

+      HashSet<string> alreadyConsidered = new HashSet<string>();

+

+      foreach (Variable v in Proc.InParams) {

+        string strippedVarName = GPUVerifier.StripThreadIdentifier(v.Name);

+        if (alreadyConsidered.Contains(strippedVarName)) {

+          continue;

+        }

+        alreadyConsidered.Add(strippedVarName);

+        if (v.TypedIdent.Type is CtorType) {

+          CtorType ct = v.TypedIdent.Type as CtorType;

+          if (ct.Decl.Name.Equals("ptr")) {

+            foreach (var arrayCollection in new ICollection<Variable>[] { 

                             verifier.KernelArrayInfo.getGlobalArrays(), verifier.KernelArrayInfo.getGroupSharedArrays(),

-                            verifier.KernelArrayInfo.getPrivateArrays() })

-                        {

-                            if (arrayCollection.Count == 0)

-                            {

-                                continue;

-                            }

-

-                            // This will need to be adapted to work with uniformity analysis

-                            foreach (string thread in new string[] { "1", "2" })

-                            {

-                                Expr DisjunctionOverPointerSet = null;

-                                foreach (var array in arrayCollection)

-                                {

-                                    Expr PointerSetDisjunct = Expr.Eq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array));

-                                    DisjunctionOverPointerSet = (DisjunctionOverPointerSet == null ? PointerSetDisjunct : Expr.Or(DisjunctionOverPointerSet, PointerSetDisjunct));

-                                    verifier.AddCandidateRequires(Proc,

-                                        Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),

-                                            Expr.Neq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array))));

-                                }

-                                Debug.Assert(DisjunctionOverPointerSet != null);

-                                verifier.AddCandidateRequires(Proc,

-                                    Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),

-                                             DisjunctionOverPointerSet));

-                                verifier.AddCandidateRequires(Proc,

-                                    Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),

-                                            Expr.Eq(MakePtrOffsetExpr(v, strippedVarName, thread), GPUVerifier.ZeroBV())));

-                            }

-                        }

-                    }

+                            verifier.KernelArrayInfo.getPrivateArrays() }) {

+              if (arrayCollection.Count == 0) {

+                continue;

+              }

+

+              // This will need to be adapted to work with uniformity analysis

+              foreach (string thread in new string[] { "1", "2" }) {

+                Expr DisjunctionOverPointerSet = null;

+                foreach (var array in arrayCollection) {

+                  Expr PointerSetDisjunct = Expr.Eq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array));

+                  DisjunctionOverPointerSet = (DisjunctionOverPointerSet == null ? PointerSetDisjunct : Expr.Or(DisjunctionOverPointerSet, PointerSetDisjunct));

+                  verifier.AddCandidateRequires(Proc,

+                      Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),

+                          Expr.Neq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array))));

                 }

-            }

-        }

+                Debug.Assert(DisjunctionOverPointerSet != null);

+                verifier.AddCandidateRequires(Proc,

+                    Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),

+                             DisjunctionOverPointerSet));

+                verifier.AddCandidateRequires(Proc,

+                    Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),

+                            Expr.Eq(MakePtrOffsetExpr(v, strippedVarName, thread), GPUVerifier.ZeroBV())));

+              }

+            }

+          }

+        }

+      }

+    }

 

-        private static IdentifierExpr MakeArrayIdExpr(Variable array)

-        {

-            return new IdentifierExpr(Token.NoToken, "$arrayId" + array.Name, null);

-        }

+    private static IdentifierExpr MakeArrayIdExpr(Variable array) {

+      return new IdentifierExpr(Token.NoToken, "$arrayId" + array.Name, null);

+    }

 

-        private static NAryExpr MakePtrBaseExpr(Variable v, string strippedVarName, string thread)

-        {

-            return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "base#MKPTR", v.TypedIdent.Type)),

-                                                        new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));

-        }

+    private static NAryExpr MakePtrBaseExpr(Variable v, string strippedVarName, string thread) {

+      return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "base#MKPTR", v.TypedIdent.Type)),

+                                                  new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));

+    }

 

-        private static NAryExpr MakePtrOffsetExpr(Variable v, string strippedVarName, string thread)

-        {

-            return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "offset#MKPTR", v.TypedIdent.Type)),

-                                                        new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));

-        }

+    private static NAryExpr MakePtrOffsetExpr(Variable v, string strippedVarName, string thread) {

+      return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "offset#MKPTR", v.TypedIdent.Type)),

+                                                  new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));

+    }

 

-        public void AddRaceCheckingCandidateEnsures(Procedure Proc)

-        {

-            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())

-            {

-                AddNoReadOrWriteCandidateEnsures(Proc, v);

-                AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);

-            }

-        }

+    public void AddRaceCheckingCandidateEnsures(Procedure Proc) {

+      foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {

+        AddNoReadOrWriteCandidateEnsures(Proc, v);

+        AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);

+      }

+    }

 

-        private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)

-        {

-            verifier.AddCandidateRequires(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));

-        }

+    private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo) {

+      verifier.AddCandidateRequires(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));

+    }

 

-        private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)

-        {

-            verifier.AddCandidateEnsures(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));

-        }

+    private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo) {

+      verifier.AddCandidateEnsures(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));

+    }

 

-        private HashSet<Expr> GetOffsetsAccessed(IRegion region, Variable v, string AccessType)

-        {

-            HashSet<Expr> result = new HashSet<Expr>();

-

-            foreach (Cmd c in region.Cmds())

-            {

-                if (c is CallCmd)

-                {

-                    CallCmd call = c as CallCmd;

-

-                    if (call.callee == "_LOG_" + AccessType + "_" + v.Name)

-                    {

-                        // Ins[0] is thread 1's predicate,

-                        // Ins[1] is the offset to be read

-                        // If Ins[1] has the form BV32_ADD(offset#construct...(P), offset),

-                        // we are looking for the second parameter to this BV32_ADD

-                        Expr offset = call.Ins[1];

-                        if (offset is NAryExpr)

-                        {

-                            var nExpr = (NAryExpr)offset;

-                            if (nExpr.Fun.FunctionName == "BV32_ADD" &&

-                                nExpr.Args[0] is NAryExpr)

-                            {

-                                var n0Expr = (NAryExpr)nExpr.Args[0];

-                                if (n0Expr.Fun.FunctionName.StartsWith("offset#"))

-                                    offset = nExpr.Args[1];

-                            }

-                        }

-                        result.Add(offset);

-                    }

+    private HashSet<Expr> GetOffsetsAccessed(IRegion region, Variable v, string AccessType) {

+      HashSet<Expr> result = new HashSet<Expr>();

 

-                }

+      foreach (Cmd c in region.Cmds()) {

+        if (c is CallCmd) {

+          CallCmd call = c as CallCmd;

 

+          if (call.callee == "_LOG_" + AccessType + "_" + v.Name) {

+            // Ins[0] is thread 1's predicate,

+            // Ins[1] is the offset to be read

+            // If Ins[1] has the form BV32_ADD(offset#construct...(P), offset),

+            // we are looking for the second parameter to this BV32_ADD

+            Expr offset = call.Ins[1];

+            if (offset is NAryExpr) {

+              var nExpr = (NAryExpr)offset;

+              if (nExpr.Fun.FunctionName == "BV32_ADD" &&

+                  nExpr.Args[0] is NAryExpr) {

+                var n0Expr = (NAryExpr)nExpr.Args[0];

+                if (n0Expr.Fun.FunctionName.StartsWith("offset#"))

+                  offset = nExpr.Args[1];

+              }

             }

+            result.Add(offset);

+          }

 

-            return result;

         }

 

-        public void AddRaceCheckingDeclarations()

-        {

-            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())

-            {

-                AddRaceCheckingDecsAndProcsForVar(v);

-            }

-        }

+      }

 

-        protected void AddLogAccessProcedure(Variable v, string Access)

-        {

-            Procedure LogAccessProcedure = MakeLogAccessProcedureHeader(v, Access);

-

-            Variable AccessHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, Access);

-            Variable AccessOffsetXVariable = GPUVerifier.MakeOffsetVariable(v, Access);

-

-            Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));

-

-            Debug.Assert(v.TypedIdent.Type is MapType);

-            MapType mt = v.TypedIdent.Type as MapType;

-            Debug.Assert(mt.Arguments.Length == 1);

-            Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));

-            Debug.Assert(!(mt.Result is MapType));

-

-            VariableSeq locals = new VariableSeq();

-            Variable TrackVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "track", Microsoft.Boogie.Type.Bool));

-            locals.Add(TrackVariable);

-

-            List<BigBlock> bigblocks = new List<BigBlock>();

-

-            CmdSeq simpleCmds = new CmdSeq();

-

-            simpleCmds.Add(new HavocCmd(v.tok, new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, TrackVariable) })));

-

-            simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessHasOccurredVariable), 

-                Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), Expr.True));

-            simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessOffsetXVariable), 

-                Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), 

-                new IdentifierExpr(v.tok, VariableForThread(1, OffsetParameter))));

-

-            if (Access.Equals("READ"))

-            {

-                // Check read by thread 2 does not conflict with write by thread 1

-                Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");

-                Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");

-                Expr WriteReadGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));

-                WriteReadGuard = Expr.And(WriteReadGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));

-                WriteReadGuard = Expr.And(WriteReadGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 

-                                                new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

-                if (!verifier.ArrayModelledAdversarially(v))

-                {

-                    WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(

-                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),

-                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")

-                        ));

-                }

+      return result;

+    }

 

-                if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v))

-                {

-                    WriteReadGuard = Expr.And(WriteReadGuard, verifier.ThreadsInSameGroup());

-                }

+    public void AddRaceCheckingDeclarations() {

+      foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays()) {

+        AddRaceCheckingDecsAndProcsForVar(v);

+      }

+    }

 

-                WriteReadGuard = Expr.Not(WriteReadGuard);

-                simpleCmds.Add(new AssertCmd(Token.NoToken, WriteReadGuard,

-                  new QKeyValue(Token.NoToken, "write_read_race", new List<object>(new object[] { }), null)

-                  ));

-            }

-            else

-            {

-                Debug.Assert(Access.Equals("WRITE"));

-

-                // Check write by thread 2 does not conflict with write by thread 1

-                Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");

-                Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");

-

-                Expr WriteWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));

-                WriteWriteGuard = Expr.And(WriteWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));

-                WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)),

-                                                new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

-                if (!verifier.ArrayModelledAdversarially(v))

-                {

-                    WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(

-                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),

-                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")

-                        ));

-                }

+    protected void AddLogAccessProcedure(Variable v, string Access) {

+      Procedure LogAccessProcedure = MakeLogAccessProcedureHeader(v, Access);

 

-                if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v))

-                {

-                    WriteWriteGuard = Expr.And(WriteWriteGuard, verifier.ThreadsInSameGroup());

-                }

+      Variable AccessHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, Access);

+      Variable AccessOffsetXVariable = GPUVerifier.MakeOffsetVariable(v, Access);

 

-                WriteWriteGuard = Expr.Not(WriteWriteGuard);

-                simpleCmds.Add(new AssertCmd(Token.NoToken, WriteWriteGuard,

-                   new QKeyValue(Token.NoToken, "write_write_race", new List<object>(new object[] { }), null)

-                  ));

-

-                // Check write by thread 2 does not conflict with read by thread 1

-                Variable ReadHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ");

-                Variable ReadOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "READ");

-

-                Expr ReadWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));

-                ReadWriteGuard = Expr.And(ReadWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadHasOccurredVariable)));

-                ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)),

-                                                new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

-                if (!verifier.ArrayModelledAdversarially(v))

-                {

-                    ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(

-                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)), 1, "WRITE"),

-                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")

-                        ));

-                }

+      Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));

 

-                if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v))

-                {

-                    ReadWriteGuard = Expr.And(ReadWriteGuard, verifier.ThreadsInSameGroup());

-                }

+      Debug.Assert(v.TypedIdent.Type is MapType);

+      MapType mt = v.TypedIdent.Type as MapType;

+      Debug.Assert(mt.Arguments.Length == 1);

+      Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));

+      Debug.Assert(!(mt.Result is MapType));

 

-                ReadWriteGuard = Expr.Not(ReadWriteGuard);

-                simpleCmds.Add(new AssertCmd(Token.NoToken, ReadWriteGuard,

-                  new QKeyValue(Token.NoToken, "read_write_race", new List<object>(new object[] { }), null)

-                  ));

+      VariableSeq locals = new VariableSeq();

+      Variable TrackVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "track", Microsoft.Boogie.Type.Bool));

+      locals.Add(TrackVariable);

 

-            }

+      List<BigBlock> bigblocks = new List<BigBlock>();

 

-            bigblocks.Add(new BigBlock(v.tok, "_LOG_" + Access + "", simpleCmds, null, null));

+      CmdSeq simpleCmds = new CmdSeq();

 

-            LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessHasOccurredVariable)));

-            LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessOffsetXVariable)));

+      simpleCmds.Add(new HavocCmd(v.tok, new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, TrackVariable) })));

 

-            Implementation LogAccessImplementation = new Implementation(v.tok, "_LOG_" + Access + "_" + v.Name, new TypeVariableSeq(), LogAccessProcedure.InParams, new VariableSeq(), locals, new StmtList(bigblocks, v.tok));

-            LogAccessImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

+      simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessHasOccurredVariable),

+          Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), Expr.True));

+      simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessOffsetXVariable),

+          Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)),

+          new IdentifierExpr(v.tok, VariableForThread(1, OffsetParameter))));

 

-            LogAccessImplementation.Proc = LogAccessProcedure;

+      bigblocks.Add(new BigBlock(v.tok, "_LOG_" + Access + "", simpleCmds, null, null));

 

-            verifier.Program.TopLevelDeclarations.Add(LogAccessProcedure);

-            verifier.Program.TopLevelDeclarations.Add(LogAccessImplementation);

-        }

+      LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessHasOccurredVariable)));

+      LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessOffsetXVariable)));

 

-        private Variable VariableForThread(int thread, Variable v)

-        {

-            return new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable);

-        }

+      Implementation LogAccessImplementation = new Implementation(v.tok, "_LOG_" + Access + "_" + v.Name, new TypeVariableSeq(), LogAccessProcedure.InParams, new VariableSeq(), locals, new StmtList(bigblocks, v.tok));

+      LogAccessImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

 

-        protected void AddLogRaceDeclarations(Variable v, String ReadOrWrite)

-        {

-            verifier.FindOrCreateAccessHasOccurredVariable(v.Name, ReadOrWrite);

+      LogAccessImplementation.Proc = LogAccessProcedure;

 

-            Debug.Assert(v.TypedIdent.Type is MapType);

-            MapType mt = v.TypedIdent.Type as MapType;

-            Debug.Assert(mt.Arguments.Length == 1);

+      verifier.Program.TopLevelDeclarations.Add(LogAccessProcedure);

+      verifier.Program.TopLevelDeclarations.Add(LogAccessImplementation);

+    }

 

-            verifier.FindOrCreateOffsetVariable(v, ReadOrWrite);

 

-        }

-        

-

-        private static AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs)

-        {

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

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

-            lhss.Add(new SimpleAssignLhs(lhs.tok, new IdentifierExpr(lhs.tok, lhs)));

-            rhss.Add(new NAryExpr(rhs.tok, new IfThenElse(rhs.tok), new ExprSeq(new Expr[] { condition, rhs, new IdentifierExpr(lhs.tok, lhs) })));

-            return new AssignCmd(lhs.tok, lhss, rhss);

-        }

+    protected void AddCheckAccessProcedure(Variable v, string Access) {

+      Procedure CheckAccessProcedure = MakeCheckAccessProcedureHeader(v, Access);

 

-        private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, int Thread, string AccessType)

-        {

-            Expr result = new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(v.Clone() as Variable));

-            Debug.Assert(v.TypedIdent.Type is MapType);

-            MapType mt = v.TypedIdent.Type as MapType;

-            Debug.Assert(mt.Arguments.Length == 1);

-

-            result = Expr.Select(result,

-                new Expr[] { offsetExpr });

-            Debug.Assert(!(mt.Result is MapType));

-            return result;

-        }

+      Variable AccessHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, Access);

+      Variable AccessOffsetXVariable = GPUVerifier.MakeOffsetVariable(v, Access);

+

+      Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));

 

-        protected void AddRequiresNoPendingAccess(Variable v)

-        {

-            IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")));

-            IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")));

+      Debug.Assert(v.TypedIdent.Type is MapType);

+      MapType mt = v.TypedIdent.Type as MapType;

+      Debug.Assert(mt.Arguments.Length == 1);

+      Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));

+      Debug.Assert(!(mt.Result is MapType));

 

-            verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.Not(WriteAccessOccurred1))));

+      if (Access.Equals("READ")) {

+        // Check read by thread 2 does not conflict with write by thread 1

+        Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");

+        Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");

+        Expr WriteReadGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));

+        WriteReadGuard = Expr.And(WriteReadGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));

+        WriteReadGuard = Expr.And(WriteReadGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)),

+                                        new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

+        if (!verifier.ArrayModelledAdversarially(v)) {

+          WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(

+              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),

+              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")

+              ));

         }

 

-        protected Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)

-        {

-            Variable ReadOrWriteHasOccurred = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);

-            ReadOrWriteHasOccurred.Name = ReadOrWriteHasOccurred.Name + "$" + OneOrTwo;

-            ReadOrWriteHasOccurred.TypedIdent.Name = ReadOrWriteHasOccurred.TypedIdent.Name + "$" + OneOrTwo;

-            Expr expr = Expr.Not(new IdentifierExpr(v.tok, ReadOrWriteHasOccurred));

-            return expr;

+        if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {

+          WriteReadGuard = Expr.And(WriteReadGuard, verifier.ThreadsInSameGroup());

         }

 

+        WriteReadGuard = Expr.Not(WriteReadGuard);

 

-        protected void AddOffsetsSatisfyPredicatesCandidateInvariant(IRegion region, Variable v, string ReadOrWrite, List<Expr> preds)

-        {

-            if (preds.Count != 0)

-            {

-                Expr expr = AccessedOffsetsSatisfyPredicatesExpr(v, preds, ReadOrWrite, 1);

-                verifier.AddCandidateInvariant(region, expr, "accessed offsets satisfy predicates");

-            }

-        }

+        Requires NoWriteReadRaceRequires = new Requires(false, WriteReadGuard);

+        NoWriteReadRaceRequires.Attributes = new QKeyValue(Token.NoToken, "write_read_race",

+          new List<object>(new object[] { }), null);

+        CheckAccessProcedure.Requires.Add(NoWriteReadRaceRequires);

+      }

+      else {

+        Debug.Assert(Access.Equals("WRITE"));

 

-        private Expr AccessedOffsetsSatisfyPredicatesExpr(Variable v, IEnumerable<Expr> offsets, string ReadOrWrite, int Thread) {

-            return Expr.Imp(

-                    new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),

-                    offsets.Aggregate(Expr.Or));

-        }

+        // Check write by thread 2 does not conflict with write by thread 1

+        Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");

+        Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");

 

-        private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread)

-        {

-            Expr expr = null;

-            if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX()))

-            {

-                expr = Expr.Imp(

-                        new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),

-                        Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));

-            }

-            return expr;

+        Expr WriteWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));

+        WriteWriteGuard = Expr.And(WriteWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));

+        WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)),

+                                        new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

+        if (!verifier.ArrayModelledAdversarially(v)) {

+          WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(

+              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetVariable)), 1, "WRITE"),

+              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")

+              ));

         }

 

-        private Expr AccessedOffsetIsThreadGlobalIdExpr(Variable v, string ReadOrWrite, int Thread)

-        {

-            Expr expr = null;

-            if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX()))

-            {

-                expr = Expr.Imp(

-                        new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),

-                        Expr.Eq(

-                            new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))),

-                            GlobalIdExpr("X", Thread)

-                            )

-                            );

-            }

-            return expr;

+        if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {

+          WriteWriteGuard = Expr.And(WriteWriteGuard, verifier.ThreadsInSameGroup());

         }

 

-        private Expr GlobalIdExpr(string dimension, int Thread)

-        {

-            return new VariableDualiser(Thread, null, null).VisitExpr(verifier.GlobalIdExpr(dimension).Clone() as Expr);

+        WriteWriteGuard = Expr.Not(WriteWriteGuard);

+        Requires NoWriteWriteRaceRequires = new Requires(false, WriteWriteGuard);

+        NoWriteWriteRaceRequires.Attributes = new QKeyValue(Token.NoToken, "write_write_race",

+          new List<object>(new object[] { }), null);

+        CheckAccessProcedure.Requires.Add(NoWriteWriteRaceRequires);

+

+        // Check write by thread 2 does not conflict with read by thread 1

+        Variable ReadHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ");

+        Variable ReadOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "READ");

+

+        Expr ReadWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));

+        ReadWriteGuard = Expr.And(ReadWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadHasOccurredVariable)));

+        ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)),

+                                        new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

+        if (!verifier.ArrayModelledAdversarially(v)) {

+          ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(

+              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetVariable)), 1, "WRITE"),

+              MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")

+              ));

         }

 

-        protected void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)

-        {

-            Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);

-            verifier.AddCandidateInvariant(region,

-                expr, "accessed offset in range [ C*local_id, (C+1)*local_id )");

+        if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v)) {

+          ReadWriteGuard = Expr.And(ReadWriteGuard, verifier.ThreadsInSameGroup());

         }

 

-        private Expr MakeCTimesLocalIdRangeExpression(Variable v, Expr constant, string ReadOrWrite, int Thread)

-        {

-            Expr CTimesLocalId = verifier.MakeBVMul(constant.Clone() as Expr, 

-                new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread)));

+        ReadWriteGuard = Expr.Not(ReadWriteGuard);

+        Requires NoReadWriteRaceRequires = new Requires(false, ReadWriteGuard);

+        NoReadWriteRaceRequires.Attributes = new QKeyValue(Token.NoToken, "read_write_race",

+          new List<object>(new object[] { }), null);

+        CheckAccessProcedure.Requires.Add(NoReadWriteRaceRequires);

 

-            Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,

-                new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr);

+      }

+      verifier.Program.TopLevelDeclarations.Add(CheckAccessProcedure);

+    }

 

-            Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread));

 

-            Expr AccessedOffsetLtCTimesLocalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesLocalIdPlusC);

 

-            return Expr.Imp(

-                    AccessHasOccurred(v, ReadOrWrite, Thread),

-                    Expr.And(CTimesLocalIdLeqAccessedOffset, AccessedOffsetLtCTimesLocalIdPlusC));

-        }

+    private Variable VariableForThread(int thread, Variable v) {

+      return new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable);

+    }

 

-        private static IdentifierExpr AccessHasOccurred(Variable v, string ReadOrWrite, int Thread)

-        {

-            return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite)));

-        }

+    protected void AddLogRaceDeclarations(Variable v, String ReadOrWrite) {

+      verifier.FindOrCreateAccessHasOccurredVariable(v.Name, ReadOrWrite);

 

-        private static IdentifierExpr OffsetXExpr(Variable v, string ReadOrWrite, int Thread)

-        {

-            return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite)));

-        }

+      Debug.Assert(v.TypedIdent.Type is MapType);

+      MapType mt = v.TypedIdent.Type as MapType;

+      Debug.Assert(mt.Arguments.Length == 1);

 

-        protected void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)

-        {

-            Expr expr = MakeCTimesGloalIdRangeExpr(v, constant, ReadOrWrite, 1);

-            verifier.AddCandidateInvariant(region,

-                expr, "accessed offset in range [ C*global_id, (C+1)*global_id )");

-        }

+      verifier.FindOrCreateOffsetVariable(v, ReadOrWrite);

 

-        private Expr MakeCTimesGloalIdRangeExpr(Variable v, Expr constant, string ReadOrWrite, int Thread)

-        {

-            Expr CTimesGlobalId = verifier.MakeBVMul(constant.Clone() as Expr,

-                GlobalIdExpr("X", Thread));

+    }

 

-            Expr CTimesGlobalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,

-                GlobalIdExpr("X", Thread)), constant.Clone() as Expr);

 

-            Expr CTimesGlobalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesGlobalId, OffsetXExpr(v, ReadOrWrite, Thread));

+    private static AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs) {

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

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

+      lhss.Add(new SimpleAssignLhs(lhs.tok, new IdentifierExpr(lhs.tok, lhs)));

+      rhss.Add(new NAryExpr(rhs.tok, new IfThenElse(rhs.tok), new ExprSeq(new Expr[] { condition, rhs, new IdentifierExpr(lhs.tok, lhs) })));

+      return new AssignCmd(lhs.tok, lhss, rhss);

+    }

 

-            Expr AccessedOffsetLtCTimesGlobalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesGlobalIdPlusC);

+    private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, int Thread, string AccessType) {

+      Expr result = new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(v.Clone() as Variable));

+      Debug.Assert(v.TypedIdent.Type is MapType);

+      MapType mt = v.TypedIdent.Type as MapType;

+      Debug.Assert(mt.Arguments.Length == 1);

 

-            Expr implication = Expr.Imp(

-                    AccessHasOccurred(v, ReadOrWrite, Thread),

-                    Expr.And(CTimesGlobalIdLeqAccessedOffset, AccessedOffsetLtCTimesGlobalIdPlusC));

-            return implication;

-        }

+      result = Expr.Select(result,

+          new Expr[] { offsetExpr });

+      Debug.Assert(!(mt.Result is MapType));

+      return result;

+    }

 

-        protected void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)

-        {

-            Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);

-            if (expr != null)

-            {

-                verifier.AddCandidateRequires(Proc, expr);

-            }

-        }

+    protected void AddRequiresNoPendingAccess(Variable v) {

+      IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")));

+      IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")));

 

-        protected void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread)

-        {

-            Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);

-            if (expr != null)

-            {

-                verifier.AddCandidateEnsures(Proc, expr);

-            }

-        }

+      verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.Not(WriteAccessOccurred1))));

+    }

 

+    protected Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo) {

+      Variable ReadOrWriteHasOccurred = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);

+      ReadOrWriteHasOccurred.Name = ReadOrWriteHasOccurred.Name + "$" + OneOrTwo;

+      ReadOrWriteHasOccurred.TypedIdent.Name = ReadOrWriteHasOccurred.TypedIdent.Name + "$" + OneOrTwo;

+      Expr expr = Expr.Not(new IdentifierExpr(v.tok, ReadOrWriteHasOccurred));

+      return expr;

+    }

 

 

+    protected void AddOffsetsSatisfyPredicatesCandidateInvariant(IRegion region, Variable v, string ReadOrWrite, List<Expr> preds) {

+      if (preds.Count != 0) {

+        Expr expr = AccessedOffsetsSatisfyPredicatesExpr(v, preds, ReadOrWrite, 1);

+        verifier.AddCandidateInvariant(region, expr, "accessed offsets satisfy predicates");

+      }

     }

 

+    private Expr AccessedOffsetsSatisfyPredicatesExpr(Variable v, IEnumerable<Expr> offsets, string ReadOrWrite, int Thread) {

+      return Expr.Imp(

+              new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),

+              offsets.Aggregate(Expr.Or));

+    }

 

+    private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread) {

+      Expr expr = null;

+      if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX())) {

+        expr = Expr.Imp(

+                new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),

+                Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));

+      }

+      return expr;

+    }

 

-    class FindReferencesToNamedVariableVisitor : StandardVisitor

-    {

-        internal bool found = false;

-        private string name;

+    private Expr AccessedOffsetIsThreadGlobalIdExpr(Variable v, string ReadOrWrite, int Thread) {

+      Expr expr = null;

+      if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX())) {

+        expr = Expr.Imp(

+                new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),

+                Expr.Eq(

+                    new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))),

+                    GlobalIdExpr("X", Thread)

+                    )

+                    );

+      }

+      return expr;

+    }

 

-        internal FindReferencesToNamedVariableVisitor(string name)

-        {

-            this.name = name;

-        }

+    private Expr GlobalIdExpr(string dimension, int Thread) {

+      return new VariableDualiser(Thread, null, null).VisitExpr(verifier.GlobalIdExpr(dimension).Clone() as Expr);

+    }

 

-        public override Variable VisitVariable(Variable node)

-        {

-            if (GPUVerifier.StripThreadIdentifier(node.Name).Equals(name))

-            {

-                found = true;

-            }

-            return base.VisitVariable(node);

-        }

+    protected void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite) {

+      Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);

+      verifier.AddCandidateInvariant(region,

+          expr, "accessed offset in range [ C*local_id, (C+1)*local_id )");

+    }

+

+    private Expr MakeCTimesLocalIdRangeExpression(Variable v, Expr constant, string ReadOrWrite, int Thread) {

+      Expr CTimesLocalId = verifier.MakeBVMul(constant.Clone() as Expr,

+          new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread)));

+

+      Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,

+          new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr);

+

+      Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread));

+

+      Expr AccessedOffsetLtCTimesLocalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesLocalIdPlusC);

+

+      return Expr.Imp(

+              AccessHasOccurred(v, ReadOrWrite, Thread),

+              Expr.And(CTimesLocalIdLeqAccessedOffset, AccessedOffsetLtCTimesLocalIdPlusC));

+    }

+

+    private static IdentifierExpr AccessHasOccurred(Variable v, string ReadOrWrite, int Thread) {

+      return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite)));

+    }

+

+    private static IdentifierExpr OffsetXExpr(Variable v, string ReadOrWrite, int Thread) {

+      return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite)));

+    }

+

+    protected void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite) {

+      Expr expr = MakeCTimesGloalIdRangeExpr(v, constant, ReadOrWrite, 1);

+      verifier.AddCandidateInvariant(region,

+          expr, "accessed offset in range [ C*global_id, (C+1)*global_id )");

+    }

+

+    private Expr MakeCTimesGloalIdRangeExpr(Variable v, Expr constant, string ReadOrWrite, int Thread) {

+      Expr CTimesGlobalId = verifier.MakeBVMul(constant.Clone() as Expr,

+          GlobalIdExpr("X", Thread));

+

+      Expr CTimesGlobalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,

+          GlobalIdExpr("X", Thread)), constant.Clone() as Expr);

+

+      Expr CTimesGlobalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesGlobalId, OffsetXExpr(v, ReadOrWrite, Thread));

+

+      Expr AccessedOffsetLtCTimesGlobalIdPlusC = verifier.MakeBVSlt(OffsetXExpr(v, ReadOrWrite, Thread), CTimesGlobalIdPlusC);

+

+      Expr implication = Expr.Imp(

+              AccessHasOccurred(v, ReadOrWrite, Thread),

+              Expr.And(CTimesGlobalIdLeqAccessedOffset, AccessedOffsetLtCTimesGlobalIdPlusC));

+      return implication;

+    }

+

+    protected void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread) {

+      Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);

+      if (expr != null) {

+        verifier.AddCandidateRequires(Proc, expr);

+      }

+    }

+

+    protected void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread) {

+      Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);

+      if (expr != null) {

+        verifier.AddCandidateEnsures(Proc, expr);

+      }

+    }

+

+

+

+  }

+

+

+

+  class FindReferencesToNamedVariableVisitor : StandardVisitor {

+    internal bool found = false;

+    private string name;

+

+    internal FindReferencesToNamedVariableVisitor(string name) {

+      this.name = name;

+    }

+

+    public override Variable VisitVariable(Variable node) {

+      if (GPUVerifier.StripThreadIdentifier(node.Name).Equals(name)) {

+        found = true;

+      }

+      return base.VisitVariable(node);

     }

+  }

 

 

 

diff --git a/Source/GPUVerify/ReadCollector.cs b/Source/GPUVerify/ReadCollector.cs
index c569b97e..6a94df73 100644
--- a/Source/GPUVerify/ReadCollector.cs
+++ b/Source/GPUVerify/ReadCollector.cs
@@ -36,56 +36,14 @@ namespace GPUVerify
                     MultiDimensionalMapError();

                 }

 

-                Variable ReadVariable = null;

-                Expr IndexX = node.Args[1];

-                Expr IndexY = null;

-                Expr IndexZ = null;

-

-                if (node.Args[0] is NAryExpr)

-                {

-                    NAryExpr nestedMap = node.Args[0] as NAryExpr;

-                    Debug.Assert(nestedMap.Fun is MapSelect);

-                    if ((nestedMap.Fun as MapSelect).Arity > 1)

-                    {

-                        MultiDimensionalMapError();

-                    }

-                    IndexY = nestedMap.Args[1];

-                    if (nestedMap.Args[0] is NAryExpr)

-                    {

-                        NAryExpr nestedNestedMap = nestedMap.Args[0] as NAryExpr;

-                        Debug.Assert(nestedNestedMap.Fun is MapSelect);

-                        if ((nestedNestedMap.Fun as MapSelect).Arity > 1)

-                        {

-                            MultiDimensionalMapError();

-                        }

-                        IndexZ = nestedMap.Args[1];

-                        if (!(nestedNestedMap.Args[0] is IdentifierExpr))

-                        {

-                            Console.WriteLine("*** Error - maps with more than three levels of nesting are not supported");

-                            Environment.Exit(1);

-                        }

-                        ReadVariable = (nestedNestedMap.Args[0] as IdentifierExpr).Decl;

-                        this.VisitExpr(nestedNestedMap.Args[1]);

-                    }

-                    else

-                    {

-                        Debug.Assert(nestedMap.Args[0] is IdentifierExpr);

-                        ReadVariable = (nestedMap.Args[0] as IdentifierExpr).Decl;

-                    }

-                    this.VisitExpr(nestedMap.Args[1]);

-

-                }

-                else

-                {

-                    Debug.Assert(node.Args[0] is IdentifierExpr);

-                    ReadVariable = (node.Args[0] as IdentifierExpr).Decl;

-                }

+                Debug.Assert(node.Args[0] is IdentifierExpr);

+                var ReadVariable = (node.Args[0] as IdentifierExpr).Decl;

+                var Index = node.Args[1];

                 this.VisitExpr(node.Args[1]);

 

-

                 if (NonLocalState.Contains(ReadVariable))

                 {

-                    accesses.Add(new AccessRecord(ReadVariable, IndexZ, IndexY, IndexX));

+                    accesses.Add(new AccessRecord(ReadVariable, Index));

                 }

 

                 return node;

@@ -97,19 +55,5 @@ namespace GPUVerify
         }

 

 

-

-        public override Variable VisitVariable(Variable node)

-        {

-            if (!NonLocalState.Contains(node))

-            {

-                return node;

-            }

-

-            accesses.Add(new AccessRecord(node, null, null, null));

-

-            return node;

-        }

-

-

     }

 }

diff --git a/Source/GPUVerify/WriteCollector.cs b/Source/GPUVerify/WriteCollector.cs
index 00ca63c5..f9633092 100644
--- a/Source/GPUVerify/WriteCollector.cs
+++ b/Source/GPUVerify/WriteCollector.cs
@@ -18,16 +18,6 @@ namespace GPUVerify
         {

         }

 

-        public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)

-        {

-            Debug.Assert(NoWrittenVariable());

-            if (NonLocalState.Contains(node.DeepAssignedVariable))

-            {

-                access = new AccessRecord(node.DeepAssignedVariable, null, null, null);

-            }

-            return node;

-        }

-

         private bool NoWrittenVariable()

         {

             return access == null;

@@ -44,42 +34,12 @@ namespace GPUVerify
 

             Variable WrittenVariable = node.DeepAssignedVariable;

 

-            MapAssignLhs MapAssignX = node;

+            CheckMapIndex(node);

+            Debug.Assert(!(node.Map is MapAssignLhs));

 

-            CheckMapIndex(MapAssignX);

-            Expr IndexX = MapAssignX.Indexes[0];

-            Expr IndexY = null;

-            Expr IndexZ = null;

+            access = new AccessRecord(WrittenVariable, node.Indexes[0]);

 

-            if (MapAssignX.Map is MapAssignLhs)

-            {

-                MapAssignLhs MapAssignY = MapAssignX.Map as MapAssignLhs;

-                CheckMapIndex(MapAssignY);

-                IndexY = MapAssignY.Indexes[0];

-                if (MapAssignY.Map is MapAssignLhs)

-                {

-                    MapAssignLhs MapAssignZ = MapAssignY.Map as MapAssignLhs;

-                    CheckMapIndex(MapAssignZ);

-                    IndexZ = MapAssignZ.Indexes[0];

-                    if (!(MapAssignZ.Map is SimpleAssignLhs))

-                    {

-                        Console.WriteLine("*** Error - maps with more than three levels of nesting are not supported");

-                        Environment.Exit(1);

-                    }

-                }

-                else

-                {

-                    Debug.Assert(MapAssignY.Map is SimpleAssignLhs);

-                }

-            }

-            else

-            {

-                Debug.Assert(MapAssignX.Map is SimpleAssignLhs);

-            }

-

-            access = new AccessRecord(WrittenVariable, IndexZ, IndexY, IndexX);

-

-            return MapAssignX;

+            return node;

         }

 

         private void CheckMapIndex(MapAssignLhs node)

diff --git a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
new file mode 100644
index 00000000..a3423b42
--- /dev/null
+++ b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.cs
@@ -0,0 +1,1008 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+//---------------------------------------------------------------------------------------------

+// OnlyBoogie OnlyBoogie.ssc

+//       - main program for taking a BPL program and verifying it

+//---------------------------------------------------------------------------------------------

+

+namespace Microsoft.Boogie

+{

+  using System;

+  using System.IO;

+  using System.Collections;

+  using System.Collections.Generic;

+  using PureCollections;

+  using Microsoft.Boogie;

+  using Microsoft.Boogie.AbstractInterpretation;

+  using System.Diagnostics.Contracts;

+  using System.Diagnostics;

+  using System.Linq;

+  using VC;

+  using AI = Microsoft.AbstractInterpretationFramework;

+  using BoogiePL = Microsoft.Boogie;

+

+  /* 

+    The following assemblies are referenced because they are needed at runtime, not at compile time:

+      BaseTypes

+      Provers.Z3

+      System.Compiler.Framework

+  */

+

+  public class GPUVerifyBoogieDriver

+  {

+    // ------------------------------------------------------------------------

+    // Main

+

+    public static void Main(string[] args)

+    {

+      Contract.Requires(cce.NonNullElements(args));

+      CommandLineOptions.Install(new CommandLineOptions());

+

+      CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;

+      if (!CommandLineOptions.Clo.Parse(args))

+      {

+        goto END;

+      }

+      if (CommandLineOptions.Clo.Files.Count == 0)

+      {

+        ErrorWriteLine("*** Error: No input files were specified.");

+        goto END;

+      }

+      if (CommandLineOptions.Clo.XmlSink != null)

+      {

+        string errMsg = CommandLineOptions.Clo.XmlSink.Open();

+        if (errMsg != null)

+        {

+          ErrorWriteLine("*** Error: " + errMsg);

+          goto END;

+        }

+      }

+      if (!CommandLineOptions.Clo.DontShowLogo)

+      {

+        Console.WriteLine(CommandLineOptions.Clo.Version);

+      }

+      if (CommandLineOptions.Clo.ShowEnv == CommandLineOptions.ShowEnvironment.Always)

+      {

+        Console.WriteLine("---Command arguments");

+        foreach (string arg in args)

+        {

+          Contract.Assert(arg != null);

+          Console.WriteLine(arg);

+        }

+

+        Console.WriteLine("--------------------");

+      }

+

+      Helpers.ExtraTraceInformation("Becoming sentient");

+

+      List<string> fileList = new List<string>();

+      foreach (string file in CommandLineOptions.Clo.Files)

+      {

+        string extension = Path.GetExtension(file);

+        if (extension != null)

+        {

+          extension = extension.ToLower();

+        }

+        if (extension == ".txt")

+        {

+          StreamReader stream = new StreamReader(file);

+          string s = stream.ReadToEnd();

+          fileList.AddRange(s.Split(new char[3] { ' ', '\n', '\r' }, StringSplitOptions.RemoveEmptyEntries));

+        }

+        else

+        {

+          fileList.Add(file);

+        }

+      }

+      foreach (string file in fileList)

+      {

+        Contract.Assert(file != null);

+        string extension = Path.GetExtension(file);

+        if (extension != null)

+        {

+          extension = extension.ToLower();

+        }

+        if (extension != ".bpl")

+        {

+          ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,

+              extension == null ? "" : extension);

+          goto END;

+        }

+      }

+      ProcessFiles(fileList);

+

+    END:

+      if (CommandLineOptions.Clo.XmlSink != null)

+      {

+        CommandLineOptions.Clo.XmlSink.Close();

+      }

+      if (CommandLineOptions.Clo.Wait)

+      {

+        Console.WriteLine("Press Enter to exit.");

+        Console.ReadLine();

+      }

+    }

+

+    public static void ErrorWriteLine(string s)

+    {

+      Contract.Requires(s != null);

+      if (!s.Contains("Error: ") && !s.Contains("Error BP"))

+      {

+        Console.WriteLine(s);

+        return;

+      }

+

+      // split the string up into its first line and the remaining lines

+      string remaining = null;

+      int i = s.IndexOf('\r');

+      if (0 <= i)

+      {

+        remaining = s.Substring(i + 1);

+        if (remaining.StartsWith("\n"))

+        {

+          remaining = remaining.Substring(1);

+        }

+        s = s.Substring(0, i);

+      }

+

+      ConsoleColor col = Console.ForegroundColor;

+      Console.ForegroundColor = ConsoleColor.Red;

+      Console.WriteLine(s);

+      Console.ForegroundColor = col;

+

+      if (remaining != null)

+      {

+        Console.WriteLine(remaining);

+      }

+    }

+

+    public static void ErrorWriteLine(string format, params object[] args)

+    {

+      Contract.Requires(format != null);

+      string s = string.Format(format, args);

+      ErrorWriteLine(s);

+    }

+

+    public static void AdvisoryWriteLine(string format, params object[] args)

+    {

+      Contract.Requires(format != null);

+      ConsoleColor col = Console.ForegroundColor;

+      Console.ForegroundColor = ConsoleColor.Yellow;

+      Console.WriteLine(format, args);

+      Console.ForegroundColor = col;

+    }

+

+    enum FileType

+    {

+      Unknown,

+      Cil,

+      Bpl,

+      Dafny

+    };

+

+    static void ProcessFiles(List<string> fileNames)

+    {

+      Contract.Requires(cce.NonNullElements(fileNames));

+      using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1]))

+      {

+        //BoogiePL.Errors.count = 0;

+        Program program = ParseBoogieProgram(fileNames, false);

+        if (program == null)

+          return;

+        if (CommandLineOptions.Clo.PrintFile != null)

+        {

+          PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);

+        }

+

+        PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);

+        if (oc != PipelineOutcome.ResolvedAndTypeChecked)

+          return;

+        //BoogiePL.Errors.count = 0;

+

+        // Do bitvector analysis

+        if (CommandLineOptions.Clo.DoBitVectorAnalysis)

+        {

+          Microsoft.Boogie.BitVectorAnalysis.DoBitVectorAnalysis(program);

+          PrintBplFile(CommandLineOptions.Clo.BitVectorAnalysisOutputBplFile, program, false);

+          return;

+        }

+

+        if (CommandLineOptions.Clo.PrintCFGPrefix != null)

+        {

+          foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())

+          {

+            using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot"))

+            {

+              sw.Write(program.ProcessLoops(impl).ToDot());

+            }

+          }

+        }

+

+        EliminateDeadVariablesAndInline(program);

+

+        int errorCount, verified, inconclusives, timeOuts, outOfMemories;

+        oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);

+        switch (oc)

+        {

+          case PipelineOutcome.Done:

+          case PipelineOutcome.VerificationCompleted:

+            WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);

+            break;

+          default:

+            break;

+        }

+      }

+    }

+

+

+    static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring)

+    {

+      Contract.Requires(program != null);

+      Contract.Requires(filename != null);

+      bool oldPrintDesugaring = CommandLineOptions.Clo.PrintDesugarings;

+      if (!allowPrintDesugaring)

+      {

+        CommandLineOptions.Clo.PrintDesugarings = false;

+      }

+      using (TokenTextWriter writer = filename == "-" ?

+                                      new TokenTextWriter("<console>", Console.Out) :

+                                      new TokenTextWriter(filename))

+      {

+        if (CommandLineOptions.Clo.ShowEnv != CommandLineOptions.ShowEnvironment.Never)

+        {

+          writer.WriteLine("// " + CommandLineOptions.Clo.Version);

+          writer.WriteLine("// " + CommandLineOptions.Clo.Environment);

+        }

+        writer.WriteLine();

+        program.Emit(writer);

+      }

+      CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaring;

+    }

+

+

+    static bool ProgramHasDebugInfo(Program program)

+    {

+      Contract.Requires(program != null);

+      // We inspect the last declaration because the first comes from the prelude and therefore always has source context.

+      return program.TopLevelDeclarations.Count > 0 &&

+          ((cce.NonNull(program.TopLevelDeclarations)[program.TopLevelDeclarations.Count - 1]).tok.IsValid);

+    }

+

+

+    /// <summary>

+    /// Inform the user about something and proceed with translation normally.

+    /// Print newline after the message.

+    /// </summary>

+    public static void Inform(string s)

+    {

+      if (!CommandLineOptions.Clo.Trace)

+      {

+        return;

+      }

+      Console.WriteLine(s);

+    }

+

+    static void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories)

+    {

+      Contract.Requires(0 <= errors && 0 <= inconclusives && 0 <= timeOuts && 0 <= outOfMemories);

+      Console.WriteLine();

+      if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

+      {

+        Console.Write("{0} finished with {1} credible, {2} doomed{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");

+      }

+      else

+      {

+        Console.Write("{0} finished with {1} verified, {2} error{3}", CommandLineOptions.Clo.DescriptiveToolName, verified, errors, errors == 1 ? "" : "s");

+      }

+      if (inconclusives != 0)

+      {

+        Console.Write(", {0} inconclusive{1}", inconclusives, inconclusives == 1 ? "" : "s");

+      }

+      if (timeOuts != 0)

+      {

+        Console.Write(", {0} time out{1}", timeOuts, timeOuts == 1 ? "" : "s");

+      }

+      if (outOfMemories != 0)

+      {

+        Console.Write(", {0} out of memory", outOfMemories);

+      }

+      Console.WriteLine();

+      Console.Out.Flush();

+    }

+

+

+

+    static void ReportBplError(Absy node, string message, bool error, bool showBplLocation)

+    {

+      int failLine    = -1;

+      int failCol     = -1;

+      string failFile = null;

+      string locinfo  = null;

+

+      if (node is PredicateCmd)

+      {

+        PredicateCmd c = (PredicateCmd)node;

+        failLine = QKeyValue.FindIntAttribute(c.Attributes, "line", -1);

+        failCol = QKeyValue.FindIntAttribute(c.Attributes, "col", -1);

+        failFile = QKeyValue.FindStringAttribute(c.Attributes, "fname");

+      }

+      else if (node is Requires)

+      {

+        Requires c = (Requires)node;

+        failLine = QKeyValue.FindIntAttribute(c.Attributes, "line", -1);

+        failCol = QKeyValue.FindIntAttribute(c.Attributes, "col", -1);

+        failFile = QKeyValue.FindStringAttribute(c.Attributes, "fname");

+      }

+      else if (node is Ensures)

+      {

+        Ensures c = (Ensures)node;

+        failLine = QKeyValue.FindIntAttribute(c.Attributes, "line", -1);

+        failCol = QKeyValue.FindIntAttribute(c.Attributes, "col", -1);

+        failFile = QKeyValue.FindStringAttribute(c.Attributes, "fname");

+      }

+      else if (node is CallCmd)

+      {

+        CallCmd c = (CallCmd)node;

+        failLine = QKeyValue.FindIntAttribute(c.Attributes, "line", -1);

+        failCol = QKeyValue.FindIntAttribute(c.Attributes, "col", -1);

+        failFile = QKeyValue.FindStringAttribute(c.Attributes, "fname");

+      }

+

+      if (showBplLocation && failLine != -1 && failCol != -1 && failFile != null)

+      {

+        locinfo = "File: \t"  + failFile +

+                  "\nLine:\t" + failLine +

+                  "\nCol:\t"  + failCol  + "\n";

+      }

+      Contract.Requires(message != null);

+      Contract.Requires(node != null);

+      IToken tok = node.tok;

+      if (error)

+      {

+        ErrorWriteLine(message);

+      }

+      else

+      {

+        Console.WriteLine(message);

+      }

+      if (!string.IsNullOrEmpty(locinfo))

+      {

+        ErrorWriteLine(locinfo);

+      }

+      else

+      {

+        ErrorWriteLine("Sourceloc info not found for: {0}({1},{2})\n", tok.filename, tok.line, tok.col);

+      }

+    }

+

+    /// <summary>

+    /// Parse the given files into one Boogie program.  If an I/O or parse error occurs, an error will be printed

+    /// and null will be returned.  On success, a non-null program is returned.

+    /// </summary>

+    static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput)

+    {

+      Contract.Requires(cce.NonNullElements(fileNames));

+      //BoogiePL.Errors.count = 0;

+      Program program = null;

+      bool okay = true;

+      for (int fileId = 0; fileId < fileNames.Count; fileId++)

+      {

+        string bplFileName = fileNames[fileId];

+        if (!suppressTraceOutput)

+        {

+          if (CommandLineOptions.Clo.XmlSink != null)

+          {

+            CommandLineOptions.Clo.XmlSink.WriteFileFragment(bplFileName);

+          }

+          if (CommandLineOptions.Clo.Trace)

+          {

+            Console.WriteLine("Parsing " + bplFileName);

+          }

+        }

+

+        Program programSnippet;

+        int errorCount;

+        try

+        {

+          var defines = new List<string>() { "FILE_" + fileId };

+          errorCount = BoogiePL.Parser.Parse(bplFileName, defines, out programSnippet);

+          if (programSnippet == null || errorCount != 0)

+          {

+            Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);

+            okay = false;

+            continue;

+          }

+        }

+        catch (IOException e)

+        {

+          ErrorWriteLine("Error opening file \"{0}\": {1}", bplFileName, e.Message);

+          okay = false;

+          continue;

+        }

+        if (program == null)

+        {

+          program = programSnippet;

+        }

+        else if (programSnippet != null)

+        {

+          program.TopLevelDeclarations.AddRange(programSnippet.TopLevelDeclarations);

+        }

+      }

+      if (!okay)

+      {

+        return null;

+      }

+      else if (program == null)

+      {

+        return new Program();

+      }

+      else

+      {

+        return program;

+      }

+    }

+

+

+    enum PipelineOutcome

+    {

+      Done,

+      ResolutionError,

+      TypeCheckingError,

+      ResolvedAndTypeChecked,

+      FatalError,

+      VerificationCompleted

+    }

+

+    /// <summary>

+    /// Resolves and type checks the given Boogie program.  Any errors are reported to the

+    /// console.  Returns:

+    ///  - Done if no errors occurred, and command line specified no resolution or no type checking.

+    ///  - ResolutionError if a resolution error occurred

+    ///  - TypeCheckingError if a type checking error occurred

+    ///  - ResolvedAndTypeChecked if both resolution and type checking succeeded

+    /// </summary>

+    static PipelineOutcome ResolveAndTypecheck(Program program, string bplFileName)

+    {

+      Contract.Requires(program != null);

+      Contract.Requires(bplFileName != null);

+      // ---------- Resolve ------------------------------------------------------------

+

+      if (CommandLineOptions.Clo.NoResolve)

+      {

+        return PipelineOutcome.Done;

+      }

+

+      int errorCount = program.Resolve();

+      if (errorCount != 0)

+      {

+        Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, bplFileName);

+        return PipelineOutcome.ResolutionError;

+      }

+

+      // ---------- Type check ------------------------------------------------------------

+

+      if (CommandLineOptions.Clo.NoTypecheck)

+      {

+        return PipelineOutcome.Done;

+      }

+

+      errorCount = program.Typecheck();

+      if (errorCount != 0)

+      {

+        Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName);

+        return PipelineOutcome.TypeCheckingError;

+      }

+

+      if (CommandLineOptions.Clo.PrintFile != null && CommandLineOptions.Clo.PrintDesugarings)

+      {

+        // if PrintDesugaring option is engaged, print the file here, after resolution and type checking

+        PrintBplFile(CommandLineOptions.Clo.PrintFile, program, true);

+      }

+

+      return PipelineOutcome.ResolvedAndTypeChecked;

+    }

+

+    static void EliminateDeadVariablesAndInline(Program program)

+    {

+      Contract.Requires(program != null);

+      // Eliminate dead variables

+      Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);

+

+      // Collect mod sets

+      if (CommandLineOptions.Clo.DoModSetAnalysis)

+      {

+        Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);

+      }

+

+      // Coalesce blocks

+      if (CommandLineOptions.Clo.CoalesceBlocks)

+      {

+        if (CommandLineOptions.Clo.Trace)

+          Console.WriteLine("Coalescing blocks...");

+        Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);

+      }

+

+      // Inline

+      var TopLevelDeclarations = cce.NonNull(program.TopLevelDeclarations);

+

+      if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None)

+      {

+        bool inline = false;

+        foreach (var d in TopLevelDeclarations)

+        {

+          if (d.FindExprAttribute("inline") != null)

+          {

+            inline = true;

+          }

+        }

+        if (inline)

+        {

+          foreach (var d in TopLevelDeclarations)

+          {

+            var impl = d as Implementation;

+            if (impl != null)

+            {

+              impl.OriginalBlocks = impl.Blocks;

+              impl.OriginalLocVars = impl.LocVars;

+            }

+          }

+          foreach (var d in TopLevelDeclarations)

+          {

+            var impl = d as Implementation;

+            if (impl != null && !impl.SkipVerification)

+            {

+              Inliner.ProcessImplementation(program, impl);

+            }

+          }

+          foreach (var d in TopLevelDeclarations)

+          {

+            var impl = d as Implementation;

+            if (impl != null)

+            {

+              impl.OriginalBlocks = null;

+              impl.OriginalLocVars = null;

+            }

+          }

+        }

+      }

+    }

+

+    static QKeyValue extractSourcelocAttrs(BlockSeq s)

+    {

+      foreach (Block b in s)

+      {

+        foreach (Cmd c in b.Cmds)

+        {

+          if (c is AssertCmd)

+          {

+            if (QKeyValue.FindBoolAttribute(((AssertCmd)c).Attributes, "sourceloc"))

+            {

+              return ((AssertCmd)c).Attributes;

+            }

+          }

+        }

+      }

+      return null;

+    }

+

+    static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,

+                       ref int errorCount, ref int verified, ref int inconclusives, ref int timeOuts, ref int outOfMemories)

+    {

+      switch (outcome)

+      {

+        default:

+          Contract.Assert(false);  // unexpected outcome

+          throw new cce.UnreachableException();

+        case VCGen.Outcome.ReachedBound:

+          Inform(String.Format("{0}verified", timeIndication));

+          Console.WriteLine(string.Format("Stratified Inlining: Reached recursion bound of {0}", CommandLineOptions.Clo.RecursionBound));

+          verified++;

+          break;

+        case VCGen.Outcome.Correct:

+          if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

+          {

+            Inform(String.Format("{0}credible", timeIndication));

+            verified++;

+          }

+          else

+          {

+            Inform(String.Format("{0}verified", timeIndication));

+            verified++;

+          }

+          break;

+        case VCGen.Outcome.TimedOut:

+          timeOuts++;

+          Inform(String.Format("{0}timed out", timeIndication));

+          break;

+        case VCGen.Outcome.OutOfMemory:

+          outOfMemories++;

+          Inform(String.Format("{0}out of memory", timeIndication));

+          break;

+        case VCGen.Outcome.Inconclusive:

+          inconclusives++;

+          Inform(String.Format("{0}inconclusive", timeIndication));

+          break;

+        case VCGen.Outcome.Errors:

+          if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

+          {

+            Inform(String.Format("{0}doomed", timeIndication));

+            errorCount++;

+          } //else {

+          Contract.Assert(errors != null);  // guaranteed by postcondition of VerifyImplementation

+          {

+            // BP1xxx: Parsing errors

+            // BP2xxx: Name resolution errors

+            // BP3xxx: Typechecking errors

+            // BP4xxx: Abstract interpretation errors (Is there such a thing?)

+            // BP5xxx: Verification errors

+

+            errors.Sort(new CounterexampleComparer());

+            foreach (Counterexample error in errors)

+            {

+              if (error is CallCounterexample)

+              {

+                CallCounterexample err = (CallCounterexample)error;

+                if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingRequires.ErrorMessage != null)

+                {

+                  ReportBplError(err.FailingRequires, err.FailingRequires.ErrorMessage, true, false);

+                }

+                else if (QKeyValue.FindBoolAttribute(err.FailingRequires.Attributes, "barrier_divergence"))

+                {

+                  ReportBplError(err.FailingCall, "Barrier Divergence Error: \nThe following barrier is reached by non-uniform control flow:", true, true);

+                }

+                else

+                {

+                  ReportBplError(err.FailingCall, "Requires Error: A precondition for this call might not hold.", true, true);

+                  ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false, true);

+                }

+                if (CommandLineOptions.Clo.XmlSink != null)

+                {

+                  CommandLineOptions.Clo.XmlSink.WriteError("precondition violation", err.FailingCall.tok, err.FailingRequires.tok, error.Trace);

+                }

+              }

+              else if (error is ReturnCounterexample)

+              {

+                ReturnCounterexample err = (ReturnCounterexample)error;

+                if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingEnsures.ErrorMessage != null)

+                {

+                  ReportBplError(err.FailingEnsures, err.FailingEnsures.ErrorMessage, true, false);

+                }

+                else

+                {

+                  ReportBplError(err.FailingReturn, "Ensures Error: A postcondition might not hold on this return path.", true, true);

+                  ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false, true);

+                }

+                if (CommandLineOptions.Clo.XmlSink != null)

+                {

+                  CommandLineOptions.Clo.XmlSink.WriteError("postcondition violation", err.FailingReturn.tok, err.FailingEnsures.tok, error.Trace);

+                }

+              }

+              else // error is AssertCounterexample

+              {

+                AssertCounterexample err = (AssertCounterexample)error;

+                if (err.FailingAssert is LoopInitAssertCmd)

+                {

+                  ReportBplError(err.FailingAssert, "Invariant Error: This loop invariant might not hold on entry.", true, true);

+                  if (CommandLineOptions.Clo.XmlSink != null)

+                  {

+                    CommandLineOptions.Clo.XmlSink.WriteError("loop invariant entry violation", err.FailingAssert.tok, null, error.Trace);

+                  }

+                }

+                else if (err.FailingAssert is LoopInvMaintainedAssertCmd)

+                {

+                  // this assertion is a loop invariant which is not maintained

+                  ReportBplError(err.FailingAssert, "Invariant Error: This loop invariant might not be maintained by the loop.", true, true);

+                  if (CommandLineOptions.Clo.XmlSink != null)

+                  {

+                    CommandLineOptions.Clo.XmlSink.WriteError("loop invariant maintenance violation", err.FailingAssert.tok, null, error.Trace);

+                  }

+                }

+                else

+                {

+                  if (!CommandLineOptions.Clo.ForceBplErrors && err.FailingAssert.ErrorMessage != null)

+                  {

+                    ReportBplError(err.FailingAssert, err.FailingAssert.ErrorMessage, true, false);

+                  }

+                  else if (err.FailingAssert.ErrorData is string)

+                  {

+                    ReportBplError(err.FailingAssert, (string)err.FailingAssert.ErrorData, true, true);

+                  }

+                  else if (QKeyValue.FindBoolAttribute(err.FailingAssert.Attributes, "write_read_race")) 

+                  {

+                    err.FailingAssert.Attributes = extractSourcelocAttrs(err.Trace);

+                    ReportBplError(err.FailingAssert, "Race Error: Write-read race caused by statement at:", true, true);

+                  }

+                  else if (QKeyValue.FindBoolAttribute(err.FailingAssert.Attributes, "read_write_race")) 

+                  {

+                    err.FailingAssert.Attributes = extractSourcelocAttrs(err.Trace);

+                    ReportBplError(err.FailingAssert, "Race Error: Read-write race caused by statement at:", true, true);

+                  }

+                  else if (QKeyValue.FindBoolAttribute(err.FailingAssert.Attributes, "write_write_race")) 

+                  {

+                    err.FailingAssert.Attributes = extractSourcelocAttrs(err.Trace);

+                    ReportBplError(err.FailingAssert, "Race Error: Write-write race caused by statement at:", true, true);

+                  }

+                  else

+                  {

+                    ReportBplError(err.FailingAssert, "Assertion Error: This assertion might not hold.", true, true);

+                  }

+                  if (CommandLineOptions.Clo.XmlSink != null)

+                  {

+                    CommandLineOptions.Clo.XmlSink.WriteError("assertion violation", err.FailingAssert.tok, null, error.Trace);

+                  }

+                }

+              }

+              if (CommandLineOptions.Clo.EnhancedErrorMessages == 1)

+              {

+                foreach (string info in error.relatedInformation)

+                {

+                  Contract.Assert(info != null);

+                  Console.WriteLine("       " + info);

+                }

+              }

+              if (CommandLineOptions.Clo.ErrorTrace > 0)

+              {

+                Console.WriteLine("Execution trace:");

+                error.Print(4);

+              }

+              if (CommandLineOptions.Clo.ModelViewFile != null)

+              {

+                error.PrintModel();

+              }

+              errorCount++;

+            }

+            //}

+            Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));

+          }

+          break;

+      }

+    }

+

+    /// <summary>

+    /// Given a resolved and type checked Boogie program, infers invariants for the program

+    /// and then attempts to verify it.  Returns:

+    ///  - Done if command line specified no verification

+    ///  - FatalError if a fatal error occurred, in which case an error has been printed to console

+    ///  - VerificationCompleted if inference and verification completed, in which the out

+    ///    parameters contain meaningful values

+    /// </summary>

+    static PipelineOutcome InferAndVerify(Program program,

+                                           out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

+    {

+      Contract.Requires(program != null);

+      Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));

+

+      errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;

+

+      // ---------- Infer invariants --------------------------------------------------------

+

+      // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)

+      if (CommandLineOptions.Clo.Ai.J_Intervals || CommandLineOptions.Clo.Ai.J_Trivial)

+      {

+        Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);

+      }

+      else

+      {

+        Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);

+      }

+

+      if (CommandLineOptions.Clo.LoopUnrollCount != -1)

+      {

+        program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

+      }

+

+      if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining > 0)

+      {

+        BlockPredicator.Predicate(program, false, false);

+        if (CommandLineOptions.Clo.PrintInstrumented)

+        {

+          using (TokenTextWriter writer = new TokenTextWriter(Console.Out))

+          {

+            program.Emit(writer);

+          }

+        }

+      }

+

+      Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;

+      if (CommandLineOptions.Clo.ExtractLoops)

+      {

+        extractLoopMappingInfo = program.ExtractLoops();

+      }

+

+      if (CommandLineOptions.Clo.PrintInstrumented)

+      {

+        program.Emit(new TokenTextWriter(Console.Out));

+      }

+

+      if (CommandLineOptions.Clo.ExpandLambdas)

+      {

+        LambdaHelper.ExpandLambdas(program);

+        //PrintBplFile ("-", program, true);

+      }

+

+      // ---------- Verify ------------------------------------------------------------

+

+      if (!CommandLineOptions.Clo.Verify)

+      {

+        return PipelineOutcome.Done;

+      }

+

+      #region Run Houdini and verify

+      if (CommandLineOptions.Clo.ContractInfer)

+      {

+        Houdini.Houdini houdini = new Houdini.Houdini(program);

+        Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();

+        if (CommandLineOptions.Clo.PrintAssignment)

+        {

+          Console.WriteLine("Assignment computed by Houdini:");

+          foreach (var x in outcome.assignment)

+          {

+            Console.WriteLine(x.Key + " = " + x.Value);

+          }

+        }

+        if (CommandLineOptions.Clo.Trace)

+        {

+          int numTrueAssigns = 0;

+          foreach (var x in outcome.assignment)

+          {

+            if (x.Value)

+              numTrueAssigns++;

+          }

+          Console.WriteLine("Number of true assignments = " + numTrueAssigns);

+          Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));

+          Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);

+          Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime);

+          Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);

+          Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);

+          Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);

+        }

+

+        foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)

+        {

+          ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);

+        }

+        //errorCount = outcome.ErrorCount;

+        //verified = outcome.Verified;

+        //inconclusives = outcome.Inconclusives;

+        //timeOuts = outcome.TimeOuts;

+        //outOfMemories = 0;

+        return PipelineOutcome.Done;

+      }

+      #endregion

+

+      #region Verify each implementation

+

+      ConditionGeneration vcgen = null;

+      try

+      {

+        if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

+        {

+          vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        }

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

+        {

+          vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        }

+        else

+        {

+          vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        }

+      }

+      catch (ProverException e)

+      {

+        ErrorWriteLine("Fatal Error: ProverException: {0}", e);

+        return PipelineOutcome.FatalError;

+      }

+

+      // operate on a stable copy, in case it gets updated while we're running

+      var decls = program.TopLevelDeclarations.ToArray();

+      foreach (Declaration decl in decls)

+      {

+        Contract.Assert(decl != null);

+        int prevAssertionCount = vcgen.CumulativeAssertionCount;

+        Implementation impl = decl as Implementation;

+        if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification)

+        {

+          List<Counterexample/*!*/>/*?*/ errors;

+

+          DateTime start = new DateTime();  // to please compiler's definite assignment rules

+          if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null)

+          {

+            start = DateTime.UtcNow;

+            if (CommandLineOptions.Clo.Trace)

+            {

+              Console.WriteLine();

+              Console.WriteLine("Verifying {0} ...", impl.Name);

+            }

+            if (CommandLineOptions.Clo.XmlSink != null)

+            {

+              CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);

+            }

+          }

+

+          VCGen.Outcome outcome;

+          try

+          {

+            if (CommandLineOptions.Clo.inferLeastForUnsat != null)

+            {

+              var svcgen = vcgen as VC.StratifiedVCGen;

+              Contract.Assert(svcgen != null);

+              var ss = new HashSet<string>();

+              foreach (var tdecl in program.TopLevelDeclarations)

+              {

+                var c = tdecl as Constant;

+                if (c == null || !c.Name.StartsWith(CommandLineOptions.Clo.inferLeastForUnsat)) continue;

+                ss.Add(c.Name);

+              }

+              outcome = svcgen.FindLeastToVerify(impl, ref ss);

+              errors = new List<Counterexample>();

+              Console.Write("Result: ");

+              foreach (var s in ss)

+              {

+                Console.Write("{0} ", s);

+              }

+              Console.WriteLine();

+            }

+            else

+            {

+              outcome = vcgen.VerifyImplementation(impl, out errors);

+              if (CommandLineOptions.Clo.ExtractLoops && vcgen is VCGen && errors != null)

+              {

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

+                {

+                  errors[i] = (vcgen as VCGen).extractLoopTrace(errors[i], impl.Name, program, extractLoopMappingInfo);

+                }

+              }

+            }

+          }

+          catch (VCGenException e)

+          {

+            ReportBplError(impl, String.Format("Error BP5010: {0}  Encountered in implementation {1}.", e.Message, impl.Name), true, true);

+            errors = null;

+            outcome = VCGen.Outcome.Inconclusive;

+          }

+          catch (UnexpectedProverOutputException upo)

+          {

+            AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);

+            errors = null;

+            outcome = VCGen.Outcome.Inconclusive;

+          }

+

+          string timeIndication = "";

+          DateTime end = DateTime.UtcNow;

+          TimeSpan elapsed = end - start;

+          if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null)

+          {

+            if (CommandLineOptions.Clo.Trace)

+            {

+              int poCount = vcgen.CumulativeAssertionCount - prevAssertionCount;

+              timeIndication = string.Format("  [{0} s, {1} proof obligation{2}]  ", elapsed.ToString("%s\\.fff"), poCount, poCount == 1 ? "" : "s");

+            }

+          }

+

+          ProcessOutcome(outcome, errors, timeIndication, ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);

+

+          if (CommandLineOptions.Clo.XmlSink != null)

+          {

+            CommandLineOptions.Clo.XmlSink.WriteEndMethod(outcome.ToString().ToLowerInvariant(), end, elapsed);

+          }

+          if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace)

+          {

+            Console.Out.Flush();

+          }

+        }

+      }

+

+      vcgen.Close();

+      cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();

+

+

+      #endregion

+

+      return PipelineOutcome.VerificationCompleted;

+    }

+  }

+}

diff --git a/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj
new file mode 100644
index 00000000..c4ab1b6f
--- /dev/null
+++ b/Source/GPUVerifyBoogieDriver/GPUVerifyBoogieDriver.csproj
@@ -0,0 +1,91 @@
+<?xml version="1.0" encoding="utf-8"?>

+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <PropertyGroup>

+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

+    <Platform Condition=" '$(Platform)' == '' ">x86</Platform>

+    <ProductVersion>8.0.30703</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{FD2A2C67-1BD6-4A1A-B65B-B057267E24A3}</ProjectGuid>

+    <OutputType>Exe</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>GPUVerifyBoogieDriver</RootNamespace>

+    <AssemblyName>GPUVerifyBoogieDriver</AssemblyName>

+    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

+    <TargetFrameworkProfile>Client</TargetFrameworkProfile>

+    <FileAlignment>512</FileAlignment>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|x86' ">

+    <PlatformTarget>x86</PlatformTarget>

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>..\..\Binaries\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

+    <PlatformTarget>x86</PlatformTarget>

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="System" />

+    <Reference Include="System.Core" />

+    <Reference Include="System.Xml.Linq" />

+    <Reference Include="System.Data.DataSetExtensions" />

+    <Reference Include="Microsoft.CSharp" />

+    <Reference Include="System.Data" />

+    <Reference Include="System.Xml" />

+  </ItemGroup>

+  <ItemGroup>

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

+    <Compile Include="Properties\AssemblyInfo.cs" />

+  </ItemGroup>

+  <ItemGroup>

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

+      <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project>

+      <Name>AbsInt</Name>

+    </ProjectReference>

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

+      <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>

+      <Name>AIFramework</Name>

+    </ProjectReference>

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

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

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

+      <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="..\Houdini\Houdini.csproj">

+      <Project>{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}</Project>

+      <Name>Houdini</Name>

+    </ProjectReference>

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

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

+      <Name>ParserHelper</Name>

+    </ProjectReference>

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

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

+      <Name>VCGeneration</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+       Other similar extension points exist, see Microsoft.Common.targets.

+  <Target Name="BeforeBuild">

+  </Target>

+  <Target Name="AfterBuild">

+  </Target>

+  -->

+</Project>
\ No newline at end of file
diff --git a/Source/GPUVerifyBoogieDriver/Properties/AssemblyInfo.cs b/Source/GPUVerifyBoogieDriver/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..ef014dd1
--- /dev/null
+++ b/Source/GPUVerifyBoogieDriver/Properties/AssemblyInfo.cs
@@ -0,0 +1,36 @@
+using System.Reflection;

+using System.Runtime.CompilerServices;

+using System.Runtime.InteropServices;

+

+// General Information about an assembly is controlled through the following 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("GPUVerifyBoogieDriver")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("")]

+[assembly: AssemblyProduct("GPUVerifyBoogieDriver")]

+[assembly: AssemblyCopyright("Copyright ©  2012")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]

+

+// Setting ComVisible to false makes the types in this assembly not visible 

+// to COM components.  If you need to access a type in this assembly from 

+// COM, set the ComVisible attribute to true on that type.

+[assembly: ComVisible(false)]

+

+// The following GUID is for the ID of the typelib if this project is exposed to COM

+[assembly: Guid("d7726f3b-aa69-4a39-a821-9503db2ab23b")]

+

+// Version information for an assembly consists of the following four values:

+//

+//      Major Version

+//      Minor Version 

+//      Build Number

+//      Revision

+//

+// You can specify all the values or you can default the Build and Revision Numbers 

+// by using the '*' as shown below:

+// [assembly: AssemblyVersion("1.0.*")]

+[assembly: AssemblyVersion("1.0.0.0")]

+[assembly: AssemblyFileVersion("1.0.0.0")]

diff --git a/Test/inline/Answer b/Test/inline/Answer
index eb409cc2..655143fa 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -306,12 +306,12 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
     goto anon3_Then, anon3_Else;

 

   anon3_Then:

-    assume x == 0;

+    assume {:partition} x == 0;

     y := 1;

     return;

 

   anon3_Else:

-    assume x != 0;

+    assume {:partition} x != 0;

     goto anon2;

 

   anon2:

@@ -350,12 +350,12 @@ implementation recursivetest()
     goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;

 

   inline$recursive$0$anon3_Then:

-    assume inline$recursive$0$x == 0;

+    assume {:partition} inline$recursive$0$x == 0;

     inline$recursive$0$y := 1;

     goto inline$recursive$0$Return;

 

   inline$recursive$0$anon3_Else:

-    assume inline$recursive$0$x != 0;

+    assume {:partition} inline$recursive$0$x != 0;

     goto inline$recursive$1$Entry;

 

   inline$recursive$1$Entry:

@@ -366,12 +366,12 @@ implementation recursivetest()
     goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;

 

   inline$recursive$1$anon3_Then:

-    assume inline$recursive$1$x == 0;

+    assume {:partition} inline$recursive$1$x == 0;

     inline$recursive$1$y := 1;

     goto inline$recursive$1$Return;

 

   inline$recursive$1$anon3_Else:

-    assume inline$recursive$1$x != 0;

+    assume {:partition} inline$recursive$1$x != 0;

     goto inline$recursive$2$Entry;

 

   inline$recursive$2$Entry:

@@ -382,12 +382,12 @@ implementation recursivetest()
     goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;

 

   inline$recursive$2$anon3_Then:

-    assume inline$recursive$2$x == 0;

+    assume {:partition} inline$recursive$2$x == 0;

     inline$recursive$2$y := 1;

     goto inline$recursive$2$Return;

 

   inline$recursive$2$anon3_Else:

-    assume inline$recursive$2$x != 0;

+    assume {:partition} inline$recursive$2$x != 0;

     call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);

     inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;

     goto inline$recursive$2$Return;

@@ -438,12 +438,12 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
     goto anon3_Then, anon3_Else;

 

   anon3_Then:

-    assume x == 0;

+    assume {:partition} x == 0;

     y := 1;

     return;

 

   anon3_Else:

-    assume x != 0;

+    assume {:partition} x != 0;

     goto inline$recursive$0$Entry;

 

   inline$recursive$0$Entry:

@@ -454,12 +454,12 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
     goto inline$recursive$0$anon3_Then, inline$recursive$0$anon3_Else;

 

   inline$recursive$0$anon3_Then:

-    assume inline$recursive$0$x == 0;

+    assume {:partition} inline$recursive$0$x == 0;

     inline$recursive$0$y := 1;

     goto inline$recursive$0$Return;

 

   inline$recursive$0$anon3_Else:

-    assume inline$recursive$0$x != 0;

+    assume {:partition} inline$recursive$0$x != 0;

     goto inline$recursive$1$Entry;

 

   inline$recursive$1$Entry:

@@ -470,12 +470,12 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
     goto inline$recursive$1$anon3_Then, inline$recursive$1$anon3_Else;

 

   inline$recursive$1$anon3_Then:

-    assume inline$recursive$1$x == 0;

+    assume {:partition} inline$recursive$1$x == 0;

     inline$recursive$1$y := 1;

     goto inline$recursive$1$Return;

 

   inline$recursive$1$anon3_Else:

-    assume inline$recursive$1$x != 0;

+    assume {:partition} inline$recursive$1$x != 0;

     goto inline$recursive$2$Entry;

 

   inline$recursive$2$Entry:

@@ -486,12 +486,12 @@ implementation {:inline 3} recursive(x: int) returns (y: int)
     goto inline$recursive$2$anon3_Then, inline$recursive$2$anon3_Else;

 

   inline$recursive$2$anon3_Then:

-    assume inline$recursive$2$x == 0;

+    assume {:partition} inline$recursive$2$x == 0;

     inline$recursive$2$y := 1;

     goto inline$recursive$2$Return;

 

   inline$recursive$2$anon3_Else:

-    assume inline$recursive$2$x != 0;

+    assume {:partition} inline$recursive$2$x != 0;

     call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);

     inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;

     goto inline$recursive$2$Return;

@@ -542,12 +542,12 @@ implementation main(x: int)
     goto anon3_Then, anon3_Else;

 

   anon3_Then:

-    assume b;

+    assume {:partition} b;

     assert i > 0 && A[i] == x;

     goto anon2;

 

   anon3_Else:

-    assume !b;

+    assume {:partition} !b;

     goto anon2;

 

   anon2:

@@ -576,22 +576,22 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
     goto anon4_LoopDone, anon4_LoopBody;

 

   anon4_LoopBody:

-    assume i < size;

+    assume {:partition} i < size;

     call b := check(A, i, x);

     goto anon5_Then, anon5_Else;

 

   anon5_Then:

-    assume b;

+    assume {:partition} b;

     ret := i;

     found := b;

     goto anon3;

 

   anon5_Else:

-    assume !b;

+    assume {:partition} !b;

     goto anon4_LoopHead;

 

   anon4_LoopDone:

-    assume size <= i;

+    assume {:partition} size <= i;

     goto anon3;

 

   anon3:

@@ -613,12 +613,12 @@ implementation {:inline 3} check(A: [int]int, i: int, c: int) returns (ret: bool
     goto anon4_Then, anon4_Else;

 

   anon4_Then:

-    assume A[i] == c;

+    assume {:partition} A[i] == c;

     ret := true;

     goto anon3;

 

   anon4_Else:

-    assume A[i] != c;

+    assume {:partition} A[i] != c;

     ret := false;

     goto anon3;

 

@@ -669,7 +669,7 @@ implementation main(x: int)
     goto inline$find$0$anon4_LoopDone, inline$find$0$anon4_LoopBody;

 

   inline$find$0$anon4_LoopBody:

-    assume inline$find$0$i < inline$find$0$size;

+    assume {:partition} inline$find$0$i < inline$find$0$size;

     goto inline$check$0$Entry;

 

   inline$check$0$Entry:

@@ -683,12 +683,12 @@ implementation main(x: int)
     goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;

 

   inline$check$0$anon4_Then:

-    assume inline$check$0$A[inline$check$0$i] == inline$check$0$c;

+    assume {:partition} inline$check$0$A[inline$check$0$i] == inline$check$0$c;

     inline$check$0$ret := true;

     goto inline$check$0$anon3;

 

   inline$check$0$anon4_Else:

-    assume inline$check$0$A[inline$check$0$i] != inline$check$0$c;

+    assume {:partition} inline$check$0$A[inline$check$0$i] != inline$check$0$c;

     inline$check$0$ret := false;

     goto inline$check$0$anon3;

 

@@ -704,17 +704,17 @@ implementation main(x: int)
     goto inline$find$0$anon5_Then, inline$find$0$anon5_Else;

 

   inline$find$0$anon5_Then:

-    assume inline$find$0$b;

+    assume {:partition} inline$find$0$b;

     inline$find$0$ret := inline$find$0$i;

     inline$find$0$found := inline$find$0$b;

     goto inline$find$0$anon3;

 

   inline$find$0$anon5_Else:

-    assume !inline$find$0$b;

+    assume {:partition} !inline$find$0$b;

     goto inline$find$0$anon4_LoopHead;

 

   inline$find$0$anon4_LoopDone:

-    assume inline$find$0$size <= inline$find$0$i;

+    assume {:partition} inline$find$0$size <= inline$find$0$i;

     goto inline$find$0$anon3;

 

   inline$find$0$anon3:

@@ -729,12 +729,12 @@ implementation main(x: int)
     goto anon3_Then, anon3_Else;

 

   anon3_Then:

-    assume b;

+    assume {:partition} b;

     assert i > 0 && A[i] == x;

     goto anon2;

 

   anon3_Else:

-    assume !b;

+    assume {:partition} !b;

     goto anon2;

 

   anon2:

@@ -766,7 +766,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
     goto anon4_LoopDone, anon4_LoopBody;

 

   anon4_LoopBody:

-    assume i < size;

+    assume {:partition} i < size;

     goto inline$check$0$Entry;

 

   inline$check$0$Entry:

@@ -780,12 +780,12 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
     goto inline$check$0$anon4_Then, inline$check$0$anon4_Else;

 

   inline$check$0$anon4_Then:

-    assume inline$check$0$A[inline$check$0$i] == inline$check$0$c;

+    assume {:partition} inline$check$0$A[inline$check$0$i] == inline$check$0$c;

     inline$check$0$ret := true;

     goto inline$check$0$anon3;

 

   inline$check$0$anon4_Else:

-    assume inline$check$0$A[inline$check$0$i] != inline$check$0$c;

+    assume {:partition} inline$check$0$A[inline$check$0$i] != inline$check$0$c;

     inline$check$0$ret := false;

     goto inline$check$0$anon3;

 

@@ -801,17 +801,17 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in
     goto anon5_Then, anon5_Else;

 

   anon5_Then:

-    assume b;

+    assume {:partition} b;

     ret := i;

     found := b;

     goto anon3;

 

   anon5_Else:

-    assume !b;

+    assume {:partition} !b;

     goto anon4_LoopHead;

 

   anon4_LoopDone:

-    assume size <= i;

+    assume {:partition} size <= i;

     goto anon3;

 

   anon3:

diff --git a/Test/smoke/Answer b/Test/smoke/Answer
index de255422..98cff8d2 100644
--- a/Test/smoke/Answer
+++ b/Test/smoke/Answer
@@ -9,7 +9,7 @@ implementation b(x: int)
     goto anon3_Then;

 

   anon3_Then:

-    assume x < 0;

+    assume {:partition} x < 0;

     y := 1;

     assert false;

     return;

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 473af09b..ae010dc9 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -114,11 +114,11 @@ Execution trace:
     CaptureState.bpl(16,5): anon4_Then

     CaptureState.bpl(24,5): anon3

 *** MODEL

-%lbl%@334 -> false

-%lbl%+110 -> true

+%lbl%@336 -> false

 %lbl%+112 -> true

-%lbl%+116 -> true

-%lbl%+189 -> true

+%lbl%+114 -> true

+%lbl%+118 -> true

+%lbl%+191 -> true

 @MV_state_const -> 6

 boolType -> T@T!val!1

 F -> T@U!val!2