Merge

11 files changed, 1520 insertions, 0 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index e91b47c8..ca707746 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -41,6 +41,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TPTP", "Provers\TPTP\TPTP.c
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "Houdini\Houdini.csproj", "{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}"

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "GPUVerify", "GPUVerify\GPUVerify.csproj", "{E5D16606-06D0-434F-A9D7-7D079BC80229}"

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Checked|.NET = Checked|.NET

@@ -521,6 +523,30 @@ Global
 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.z3apidebug|x86.ActiveCfg = Release|Any CPU

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|.NET.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Any CPU.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|Mixed Platforms.Build.0 = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Checked|x86.Build.0 = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|.NET.ActiveCfg = Debug|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Any CPU.ActiveCfg = Debug|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.ActiveCfg = Debug|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|Mixed Platforms.Build.0 = Debug|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.ActiveCfg = Debug|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Debug|x86.Build.0 = Debug|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|.NET.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Any CPU.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|Mixed Platforms.Build.0 = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.Release|x86.Build.0 = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|.NET.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Any CPU.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|Mixed Platforms.Build.0 = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.ActiveCfg = Release|x86

+		{E5D16606-06D0-434F-A9D7-7D079BC80229}.z3apidebug|x86.Build.0 = Release|x86

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/GPUVerify/AccessCollector.cs b/Source/GPUVerify/AccessCollector.cs
new file mode 100644
index 00000000..a3821952
--- /dev/null
+++ b/Source/GPUVerify/AccessCollector.cs
@@ -0,0 +1,25 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    abstract class AccessCollector : StandardVisitor

+    {

+        protected GPUVerifier verifier;

+

+        public AccessCollector(GPUVerifier verifier)

+        {

+            this.verifier = verifier;

+        }

+

+        protected void MultiDimensionalMapError()

+        {

+            Console.WriteLine("*** Error - multidimensional maps not supported in kernels, use nested maps instead");

+            Environment.Exit(1);

+        }

+

+    }

+}

diff --git a/Source/GPUVerify/AccessRecord.cs b/Source/GPUVerify/AccessRecord.cs
new file mode 100644
index 00000000..fedacde3
--- /dev/null
+++ b/Source/GPUVerify/AccessRecord.cs
@@ -0,0 +1,27 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    class AccessRecord

+    {

+        public Variable v;

+        public Expr IndexZ;

+        public Expr IndexY;

+        public Expr IndexX;

+

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

+        {

+            this.v = v;

+            this.IndexZ = IndexZ;

+            this.IndexY = IndexY;

+            this.IndexX = IndexX;

+        }

+

+

+    }

+}

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
new file mode 100644
index 00000000..80dc18ef
--- /dev/null
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -0,0 +1,25 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.IO;

+

+namespace GPUVerify

+{

+

+    class CommandLineOptions

+    {

+

+        public static List<string> inputFiles = new List<string>();

+

+        public static int Parse(string[] args)

+        {

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

+            {

+                inputFiles.Add(args[i]);

+            }

+            return 0;

+        }

+

+    }

+}

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
new file mode 100644
index 00000000..391d7bdf
--- /dev/null
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -0,0 +1,844 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    class GPUVerifier : CheckingContext

+    {

+

+        HashSet<string> ReservedNames;

+

+        private Program Program;

+        private Procedure KernelProcedure;

+        private Implementation KernelImplementation;

+        private Procedure BarrierProcedure;

+        private Microsoft.Boogie.Type ThreadIdType;

+        private String ThreadIdParameterName;

+

+        private HashSet<int> BarrierIds = new HashSet<int>();

+

+        private HashSet<Variable> ThreadLocalVariables = new HashSet<Variable>();

+        private HashSet<Variable> TileStaticVariables = new HashSet<Variable>();

+        private HashSet<Variable> GloalVariables = new HashSet<Variable>();

+

+

+        public GPUVerifier(Program program)

+            : base((IErrorSink)null)

+        {

+            this.Program = program;

+

+            ReservedNames = new HashSet<string>();

+            ReservedNames.Add("base");

+            ReservedNames.Add("offset_x");

+            ReservedNames.Add("offset_y");

+            ReservedNames.Add("offset_z");

+            ReservedNames.Add("AT_BARRIER");

+

+            CheckWellFormedness();

+        }

+

+        private void CheckWellFormedness()

+        {

+            int errorCount = check(Program);

+            if (errorCount != 0)

+            {

+                Console.WriteLine("{0} GPUVerify format errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);

+                Environment.Exit(1);

+            }

+        }

+

+        internal int check(Program program)

+        {

+            BarrierProcedure = CheckExactlyOneBarrierProcedure(program);

+            KernelProcedure = CheckExactlyOneKernelProcedure(program);

+            TypeSynonymDecl ThreadIdDecl = CheckExactlyOneThreadIdType(program);

+            ThreadIdType = new TypeSynonymAnnotation(ThreadIdDecl.tok, ThreadIdDecl, new TypeSeq());

+

+            if (ErrorCount > 0)

+            {

+                return ErrorCount;

+            }

+

+            if (BarrierProcedure.InParams.Length != 0)

+            {

+                Error(BarrierProcedure, "Barrier procedure must not take any arguments");

+            }

+

+            if (BarrierProcedure.OutParams.Length != 0)

+            {

+                Error(BarrierProcedure, "Barrier procedure must not return any results");

+            }

+

+            FindGlobalVariables(program);

+

+            CheckKernelImplementation(program);

+

+            return ErrorCount;

+        }

+

+        private void FindGlobalVariables(Program program)

+        {

+            foreach (Declaration D in program.TopLevelDeclarations)

+            {

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

+                {

+                    if (!ReservedNames.Contains((D as Variable).Name))

+                    {

+                        GloalVariables.Add(D as Variable);

+                    }

+                }

+            }

+        }

+

+

+        private void CheckKernelImplementation(Program Program)

+        {

+            if (KernelProcedure.InParams.Length != 1)

+            {

+                Error(KernelProcedure, "Kernel procedure must take exactly one argument, of type {0}", ThreadIdType.ToString());

+            }

+            else

+            {

+                if (!KernelProcedure.InParams[0].TypedIdent.Type.Equals(ThreadIdType))

+                {

+                    Error(KernelProcedure, "Argument to kernel procedure has wrong type - {0} instead of {1}", KernelProcedure.InParams[0].TypedIdent.Type.ToString(), ThreadIdType.ToString());

+                }

+

+                ThreadIdParameterName = KernelProcedure.InParams[0].TypedIdent.Name;

+

+            }

+

+            if (KernelProcedure.OutParams.Length != 0)

+            {

+                Error(KernelProcedure, "Kernel procedure must not return any results");

+            }

+

+

+            foreach (Declaration decl in Program.TopLevelDeclarations)

+            {

+                if (!(decl is Implementation))

+                {

+                    continue;

+                }

+

+                Implementation Impl = decl as Implementation;

+

+                if (Impl.Proc == KernelProcedure)

+                {

+                    KernelImplementation = Impl;

+                    break;

+                }

+

+            }

+

+            if (KernelImplementation == null)

+            {

+                Error(Token.NoToken, "*** Error: no implementation of kernel procedure");

+                return;

+            }

+

+            // Collect up the local and tile_static variables

+            foreach (LocalVariable LV in KernelImplementation.LocVars)

+            {

+                if (QKeyValue.FindBoolAttribute(LV.Attributes, "tile_static"))

+                {

+                    TileStaticVariables.Add(LV);

+                }

+                else

+                {

+                    ThreadLocalVariables.Add(LV);

+                }

+            }

+

+            // Clear the local variables

+            KernelImplementation.LocVars = new VariableSeq();

+

+            foreach (LocalVariable LV in ThreadLocalVariables)

+            {

+                // Make each local variable a global map from threadid to the usual type

+                GlobalVariable GV = new GlobalVariable(LV.tok, LV.TypedIdent);

+                TypeSeq IndexType = new TypeSeq();

+                IndexType.Add(ThreadIdType);

+                GV.TypedIdent.Type = new MapType(GV.TypedIdent.Type.tok, new TypeVariableSeq(), IndexType, LV.TypedIdent.Type);

+                Program.TopLevelDeclarations.Add(GV);

+                KernelProcedure.Modifies.Add(new IdentifierExpr(GV.tok, GV));

+            }

+

+            foreach (LocalVariable LV in TileStaticVariables)

+            {

+                // Promote each tile-static variable to global

+                GlobalVariable GV = new GlobalVariable(LV.tok, LV.TypedIdent);

+                GV.TypedIdent.Type = LV.TypedIdent.Type;

+                Program.TopLevelDeclarations.Add(GV);

+                KernelProcedure.Modifies.Add(new IdentifierExpr(GV.tok, GV));

+            }

+

+            LocalVariableAccessReplacer replacer = new LocalVariableAccessReplacer(this);

+

+            replacer.VisitImplementation(KernelImplementation);

+

+            Console.WriteLine("After replacement we have ");

+

+            using (TokenTextWriter writer = new TokenTextWriter("<console>", Console.Out))

+            {

+                KernelImplementation.Emit(writer, 1);

+            }

+

+            Environment.Exit(1);

+

+

+            // Check that each barrier has a positive integer id

+            // Check that these ids are all distinct

+            foreach (Block B in KernelImplementation.Blocks)

+            {

+                foreach (Cmd C in B.Cmds)

+                {

+                    if (IsBarrier(C))

+                    {

+                        CallCmd Barrier = C as CallCmd;

+

+                        int BarrierId = QKeyValue.FindIntAttribute(Barrier.Attributes, "barrier_id", -1);

+                        if (BarrierId < 1)

+                        {

+                            Error(Barrier, "Barrier must have positive integer attribute \"barrier_id\"");

+                        }

+                        else if (BarrierIds.Contains(BarrierId))

+                        {

+                            Error(Barrier, "Each barrier call must have a unique integer attribute \"barrier_id\" - duplicate id {0} detected", BarrierId);

+                        }

+                        else

+                        {

+                            BarrierIds.Add(BarrierId);

+                        }

+                    }

+                }

+

+            }

+

+

+        }

+

+

+

+        private Procedure CheckExactlyOneKernelProcedure(Program program)

+        {

+            return CheckSingleInstanceOfAttributedProcedure(program, "kernel");

+        }

+

+        private Procedure CheckExactlyOneBarrierProcedure(Program program)

+        {

+            return CheckSingleInstanceOfAttributedProcedure(program, "barrier");

+        }

+

+        private TypeSynonymDecl CheckExactlyOneThreadIdType(Program program)

+        {

+            return CheckSingleInstanceOfAttributedEntity<TypeSynonymDecl>(program, "thread_id");

+        }

+

+        private T CheckSingleInstanceOfAttributedEntity<T>(Program program, string attribute) where T : Declaration

+        {

+            T attributedEntity = null;

+            foreach (Declaration decl in program.TopLevelDeclarations)

+            {

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

+                {

+                    continue;

+                }

+

+                if (decl is T)

+                {

+                    if (attributedEntity == null)

+                    {

+                        attributedEntity = decl as T;

+                    }

+                    else

+                    {

+                        Error(decl, "\"{0}\" attribute specified for {1}, but it has already been specified for procedure {2}", attribute, decl.ToString(), attributedEntity.ToString());

+                    }

+                }

+                else

+                {

+                    Error(decl, "\"{0}\" attribute applied to wrong sort of declaration {1}", attribute, decl.ToString());

+                }

+            }

+

+            if (attributedEntity == null)

+            {

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

+            }

+

+            return attributedEntity;

+        }

+

+

+        internal void AddBarrierId(int BarrierId)

+        {

+            BarrierIds.Add(BarrierId);

+        }

+

+        internal int MaxBarrierId()

+        {

+            int result = -1;

+            foreach (int i in BarrierIds)

+            {

+                if (i > result)

+                {

+                    result = i;

+                }

+            }

+            return result;

+        }

+

+        internal HashSet<Variable> GetGlobalVariables()

+        {

+            return GloalVariables;

+        }

+

+        internal HashSet<Variable> GetTileStaticVariables()

+        {

+            return TileStaticVariables;

+        }

+

+        internal HashSet<Variable> GetThreadLocalVariables()

+        {

+            return ThreadLocalVariables;

+        }

+

+

+        private Procedure CheckSingleInstanceOfAttributedProcedure(Program program, string attribute)

+        {

+            Procedure attributedProcedure = null;

+

+            foreach (Declaration decl in program.TopLevelDeclarations)

+            {

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

+                {

+                    continue;

+                }

+

+                if (decl is Procedure)

+                {

+                    if (attributedProcedure == null)

+                    {

+                        attributedProcedure = decl as Procedure;

+                    }

+                    else

+                    {

+                        Error(decl, "\"{0}\" attribute specified for procedure {1}, but it has already been specified for procedure {2}", attribute, (decl as Procedure).Name, attributedProcedure.Name);

+                    }

+

+                }

+                else

+                {

+                    Error(decl, "\"{0}\" attribute can only be applied to a procedure", attribute);

+                }

+            }

+

+            if (attributedProcedure == null)

+            {

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

+            }

+

+            return attributedProcedure;

+        }

+

+        public void AddInitialAndFinalBarriers()

+        {

+            // Add barrier to start of first block, if it doesn't already start with a barrier

+            if (!IsBarrier(KernelImplementation.Blocks[0].Cmds[0]))

+            {

+                CmdSeq NewCmds = new CmdSeq();

+                NewCmds.Add(MakeBarrierCmd(0));

+                foreach (Cmd C in KernelImplementation.Blocks[0].Cmds)

+                {

+                    NewCmds.Add(C);

+                }

+                KernelImplementation.Blocks[0].Cmds = NewCmds;

+            }

+

+            CmdSeq FinalBarrierCmdSeq = new CmdSeq();

+

+            int FinalBarrierId = MaxBarrierId() + 1;

+

+            FinalBarrierCmdSeq.Add(MakeBarrierCmd(FinalBarrierId));

+

+            string FinalBarrierLabel = "barrier_label" + FinalBarrierId;

+

+            Block FinalBarrierBlock = new Block(Token.NoToken, FinalBarrierLabel, FinalBarrierCmdSeq, new ReturnCmd(Token.NoToken));

+

+            foreach (Block B in KernelImplementation.Blocks)

+            {

+                if (B.TransferCmd is ReturnCmd)

+                {

+                    BlockSeq BlockSeq = new BlockSeq();

+                    BlockSeq.Add(FinalBarrierBlock);

+                    StringSeq StringSeq = new StringSeq();

+                    StringSeq.Add(FinalBarrierLabel);

+                    B.TransferCmd = new GotoCmd(Token.NoToken, StringSeq, BlockSeq);

+                }

+            }

+

+            KernelImplementation.Blocks.Add(FinalBarrierBlock);

+

+        }

+

+        private Cmd MakeBarrierCmd(int BarrierId)

+        {

+            Debug.Assert(!BarrierIds.Contains(BarrierId));

+            AddBarrierId(BarrierId);

+            CallCmd Result = new CallCmd(Token.NoToken, BarrierProcedure.Name, new ExprSeq(), new IdentifierExprSeq());

+            Result.Attributes = new QKeyValue(Token.NoToken, "barrier_id", new List<object>(new object[] { Expr.Literal(BarrierId) }), null);

+            return Result;

+        }

+

+

+        private static Implementation CloneImplementation(Implementation Impl, string NewName)

+        {

+            Implementation Result = new Implementation(Impl.tok, NewName, Impl.TypeParameters, Impl.InParams, Impl.OutParams, Impl.LocVars, new List<Block>());

+

+            Dictionary<Block, Block> OldToNew = new Dictionary<Block, Block>();

+

+            foreach (Block B in Impl.Blocks)

+            {

+                Block NewB = CloneBlock(B);

+

+                OldToNew.Add(B, NewB);

+

+                Result.Blocks.Add(NewB);

+

+            }

+

+            foreach (Block NewB in Result.Blocks)

+            {

+                if (NewB.TransferCmd is GotoCmd)

+                {

+                    GotoCmd NewGotoCmd = NewB.TransferCmd as GotoCmd;

+

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

+                    {

+                        Block NewSuccessor;

+                        bool found = OldToNew.TryGetValue(NewGotoCmd.labelTargets[i], out NewSuccessor);

+                        Debug.Assert(found);

+

+                        NewGotoCmd.labelTargets[i] = NewSuccessor;

+                    }

+

+                }

+            }

+

+            return Result;

+        }

+

+

+        private static Block CloneBlock(Block B)

+        {

+            Block NewB = new Block(B.tok, B.Label, new CmdSeq(), null);

+

+            foreach (Cmd C in B.Cmds)

+            {

+                NewB.Cmds.Add(C); // The contents of each command is *not* cloned

+            }

+

+            if (B.TransferCmd is ReturnCmd)

+            {

+                NewB.TransferCmd = new ReturnCmd((B.TransferCmd as ReturnCmd).tok);

+            }

+            else

+            {

+                GotoCmd GotoCmd = B.TransferCmd as GotoCmd;

+                NewB.TransferCmd = new GotoCmd(GotoCmd.tok, new StringSeq(), new BlockSeq());

+                GotoCmd NewGotoCmd = NewB.TransferCmd as GotoCmd;

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

+                {

+                    NewGotoCmd.labelNames.Add(GotoCmd.labelNames[i]);

+                    NewGotoCmd.labelTargets.Add(GotoCmd.labelTargets[i]);

+                }

+            }

+            return NewB;

+        }

+

+

+        private static void AppendDuplicateBlockToStartOfImplementation(Implementation Impl, int i)

+        {

+            Block NewBlock = CloneBlock(Impl.Blocks[i]);

+

+            List<Block> NewBlocks = new List<Block>();

+

+            NewBlocks.Add(NewBlock);

+

+            foreach (Block B in Impl.Blocks)

+            {

+                NewBlocks.Add(B);

+            }

+

+            Impl.Blocks = NewBlocks;

+

+        }

+

+        private Implementation ConstructBarrierToNextBarriersImplementation(Block B, String NewProcedureName)

+        {

+            Implementation NewImplementation = CloneImplementation(KernelImplementation, NewProcedureName);

+

+            AppendDuplicateBlockToStartOfImplementation(NewImplementation, KernelImplementation.Blocks.IndexOf(B));

+

+            // Iterate through all blocks except first, immediately following barrier calls with "return"

+

+            for (int i = 1; i < NewImplementation.Blocks.Count; i++)

+            {

+                if (IsBarrier(NewImplementation.Blocks[i]))

+                {

+                    // This is a barrier so we don't want control to get any further.

+                    // To ensure this, we simply remove any commands following the barrier,

+                    // and make the transfer command into a "return".

+                    CmdSeq NewCmdSeq = new CmdSeq();

+                    NewCmdSeq.Add(NewImplementation.Blocks[i].Cmds[0]);

+                    NewImplementation.Blocks[i].Cmds = NewCmdSeq;

+                    NewImplementation.Blocks[i].TransferCmd = new ReturnCmd(Token.NoToken);

+                }

+            }

+

+            NewImplementation.PruneUnreachableBlocks();

+            return NewImplementation;

+        }

+

+        private void SanityCheckKernel()

+        {

+            foreach (Block C in KernelImplementation.Blocks)

+            {

+                if (C.TransferCmd is GotoCmd)

+                {

+                    foreach (Block D in (C.TransferCmd as GotoCmd).labelTargets)

+                    {

+                        Debug.Assert(KernelImplementation.Blocks.Contains(D));

+                    }

+                }

+            }

+        }

+

+

+        private void ComputeBarrierToNextBarriersProcedure(Block B)

+        {

+            SanityCheckKernel();

+            Debug.Assert(IsBarrier(B));

+

+            String NewProcedureName = "Barrier_" + GetBarrierId(B) + "_to_next_barriers";

+            Procedure NewProcedure = new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, KernelProcedure.Requires, KernelProcedure.Modifies, KernelProcedure.Ensures);

+            Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(B, NewProcedureName);

+

+            InstrumentWithRaceDetection(NewImplementation);

+

+            Program.TopLevelDeclarations.Add(NewProcedure);

+            Program.TopLevelDeclarations.Add(NewImplementation);

+

+        }

+

+        private void InstrumentWithRaceDetection(Implementation Impl)

+        {

+            foreach (Block B in Impl.Blocks)

+            {

+                CmdSeq NewCmds = new CmdSeq();

+

+                foreach (Cmd C in B.Cmds)

+                {

+                    ReadCollector rc = new ReadCollector(this);

+                    rc.Visit(C);

+                    WriteCollector wc = new WriteCollector(this);

+                    wc.Visit(C);

+

+                    if (wc.FoundWrite())

+                    {

+                        AccessRecord write = wc.GetAccess();

+                        ExprSeq InParams = ConstructLogAccessParameters(C, write);

+                        NewCmds.Add(new CallCmd(C.tok, "LOG_WRITE", InParams, new IdentifierExprSeq()));

+                    }

+

+                    foreach (AccessRecord read in rc.accesses)

+                    {

+                        ExprSeq InParams = ConstructLogAccessParameters(C, read);

+                        NewCmds.Add(new CallCmd(C.tok, "LOG_READ", InParams, new IdentifierExprSeq()));

+                    }

+

+                    NewCmds.Add(C);

+                }

+                B.Cmds = NewCmds;

+            }

+        }

+

+        private ExprSeq ConstructLogAccessParameters(Cmd C, AccessRecord access)

+        {

+            ExprSeq InParams = new ExprSeq();

+            InParams.Add(new IdentifierExpr(C.tok, new GlobalVariable(C.tok, new TypedIdent(C.tok, access.v.Name + "_base", Microsoft.Boogie.Type.Int))));

+            InParams.Add(access.IndexZ);

+            InParams.Add(access.IndexY);

+            InParams.Add(access.IndexX);

+            InParams.Add(MakeThreadIdExpr(C.tok));

+            return InParams;

+        }

+

+        private void ComputeBarrierAToBarrierBProcedure(Block A, Block B)

+        {

+            Debug.Assert(IsBarrier(A));

+            Debug.Assert(IsBarrier(B));

+

+            String NewProcedureName = "Barrier_" + GetBarrierId(A) + "_to_" + GetBarrierId(B);

+            Procedure NewProcedure = new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, KernelProcedure.Requires, KernelProcedure.Modifies, KernelProcedure.Ensures);

+            Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(A, NewProcedureName);

+

+            Block NewA = NewImplementation.Blocks[0];

+            Block NewB = null;

+            for (int i = 1; i < NewImplementation.Blocks.Count; i++)

+            {

+                if (IsBarrier(NewImplementation.Blocks[i]) && GetBarrierId(B) == GetBarrierId(NewImplementation.Blocks[i]))

+                {

+                    NewB = NewImplementation.Blocks[i];

+                    break;

+                }

+            }

+            if (NewB == null)

+            {

+                // No path between the barriers -- nothing to do

+                return;

+            }

+

+            NewImplementation.ComputePredecessorsForBlocks();

+

+            HashSet<Block> NodesToKeep = BlocksReaching(NewB);

+

+            Debug.Assert(NodesToKeep.Count > 1);

+

+            foreach (Block D in NewImplementation.Blocks)

+            {

+                if (D.TransferCmd is GotoCmd)

+                {

+                    GotoCmd GotoCmd = D.TransferCmd as GotoCmd;

+                    GotoCmd NewGotoCmd = new GotoCmd(GotoCmd.tok, new StringSeq(), new BlockSeq());

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

+                    {

+                        if (NodesToKeep.Contains(GotoCmd.labelTargets[i]))

+                        {

+                            NewGotoCmd.labelNames.Add(GotoCmd.labelNames[i]);

+                            NewGotoCmd.labelTargets.Add(GotoCmd.labelTargets[i]);

+                        }

+                    }

+                    D.TransferCmd = NewGotoCmd;

+                }

+            }

+

+            NewImplementation.PruneUnreachableBlocks();

+

+            Program.TopLevelDeclarations.Add(NewProcedure);

+            Program.TopLevelDeclarations.Add(NewImplementation);

+

+        }

+

+        private static HashSet<Block> BlocksReaching(Block B)

+        {

+            HashSet<Block> Result = new HashSet<Block>();

+            ComputeReachingBlocksRecursive(B, Result);

+            return Result;

+        }

+

+        private static void ComputeReachingBlocksRecursive(Block B, HashSet<Block> Result)

+        {

+            if (Result.Contains(B))

+            {

+                return;

+            }

+

+            Result.Add(B);

+            foreach (Block C in B.Predecessors)

+            {

+                ComputeReachingBlocksRecursive(C, Result);

+            }

+        }

+

+        private static HashSet<Block> BlocksReachableFrom(Block B)

+        {

+            HashSet<Block> Result = new HashSet<Block>();

+            ComputeReachableBlocksRecursive(B, Result);

+            return Result;

+        }

+

+        private static void ComputeReachableBlocksRecursive(Block B, HashSet<Block> Result)

+        {

+            if (Result.Contains(B))

+            {

+                return;

+            }

+            Result.Add(B);

+            if (B.TransferCmd is GotoCmd)

+            {

+                foreach (Block C in (B.TransferCmd as GotoCmd).labelTargets)

+                {

+                    ComputeReachableBlocksRecursive(C, Result);

+                }

+            }

+        }

+

+

+

+

+        private Block FindBarrierBlock(Implementation Impl, int BarrierId)

+        {

+            foreach (Block B in Impl.Blocks)

+            {

+                if (B.Cmds.Length > 0 && IsBarrier(B.Cmds[0]) && GetBarrierId(B) == BarrierId)

+                {

+                    return B;

+                }

+            }

+

+            Debug.Assert(false);

+

+            return null;

+        }

+

+        private int GetBarrierId(Cmd C)

+        {

+            Debug.Assert(IsBarrier(C));

+            return QKeyValue.FindIntAttribute((C as CallCmd).Attributes, "barrier_id", -1);

+        }

+

+        public int GetBarrierId(Block A)

+        {

+            Debug.Assert(A.Cmds.Length > 0);

+            return GetBarrierId(A.Cmds[0]);

+        }

+

+        public bool IsBarrier(Cmd C)

+        {

+            return C is CallCmd && (C as CallCmd).callee == BarrierProcedure.Name;

+        }

+

+        public bool IsBarrier(Block B)

+        {

+            return B.Cmds.Length > 0 && IsBarrier(B.Cmds[0]);

+        }

+

+

+

+

+        public void SplitBlocksAtBarriers()

+        {

+

+            int NumBlocksBeforeSplitting = KernelImplementation.Blocks.Count;

+

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

+            {

+                Block B = KernelImplementation.Blocks[i];

+

+                List<CmdSeq> Segments = new List<CmdSeq>();

+                CmdSeq CurrentSequence = new CmdSeq();

+                foreach (Cmd C in B.Cmds)

+                {

+                    if (IsBarrier(C))

+                    {

+                        if (CurrentSequence.Length > 0)

+                        {

+                            Segments.Add(CurrentSequence);

+                            CurrentSequence = new CmdSeq();

+                        }

+                    }

+

+                    CurrentSequence.Add(C);

+                }

+                if (CurrentSequence.Length > 0)

+                {

+                    Segments.Add(CurrentSequence);

+                }

+

+                if (Segments.Count > 1)

+                {

+                    TransferCmd OriginalTransferCmd = B.TransferCmd;

+

+                    // Set the block's commands to be the first command sequence

+                    B.Cmds = Segments[0];

+                    B.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq());

+                    Block LastBlock = B;

+                    for (int j = 1; j < Segments.Count; j++)

+                    {

+                        Block NewBlock = new Block(Token.NoToken, "barrier_label_" + GetBarrierId(Segments[j][0]), Segments[j], new GotoCmd(Token.NoToken, new BlockSeq()));

+                        KernelImplementation.Blocks.Add(NewBlock);

+                        (LastBlock.TransferCmd as GotoCmd).AddTarget(NewBlock);

+                        LastBlock = NewBlock;

+                    }

+                    LastBlock.TransferCmd = OriginalTransferCmd;

+

+                }

+

+            }

+        }

+

+        private bool ContainsInternalBarrier(Block B)

+        {

+            bool first = true;

+            foreach (Cmd C in B.Cmds)

+            {

+                if (first)

+                {

+                    first = false;

+                    continue;

+                }

+

+                if (C is CallCmd)

+                {

+                    CallCmd Call = C as CallCmd;

+                    if (QKeyValue.FindBoolAttribute(Call.Proc.Attributes, "barrier"))

+                    {

+                        return true;

+                    }

+                }

+

+            }

+

+            return false;

+        }

+

+

+

+        internal Implementation GetKernel()

+        {

+            return KernelImplementation;

+        }

+

+        internal void ComputeBarrierToNextBarriersProcedures()

+        {

+            foreach (Block B in KernelImplementation.Blocks)

+            {

+                if (IsBarrier(B) && (GetBarrierId(B) < MaxBarrierId()))

+                {

+                    ComputeBarrierToNextBarriersProcedure(B);

+                }

+            }

+        }

+

+        internal void ComputeBarrierToBarrierPairs()

+        {

+            foreach (Block A in KernelImplementation.Blocks)

+            {

+                if (IsBarrier(A))

+                {

+                    foreach (Block B in KernelImplementation.Blocks)

+                    {

+                        if (IsBarrier(B))

+                        {

+                            ComputeBarrierAToBarrierBProcedure(A, B);

+                        }

+                    }

+                }

+            }

+        }

+

+        internal IdentifierExpr MakeThreadIdExpr(IToken tok)

+        {

+            return new IdentifierExpr(tok, new LocalVariable(tok, new TypedIdent(tok, ThreadIdParameterName, ThreadIdType)));

+        }

+

+

+    }

+

+}

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
new file mode 100644
index 00000000..407ebe5f
--- /dev/null
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -0,0 +1,86 @@
+<?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>{E5D16606-06D0-434F-A9D7-7D079BC80229}</ProjectGuid>

+    <OutputType>Exe</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>GPUVerify</RootNamespace>

+    <AssemblyName>GPUVerify</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>bin\Debug\</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="AccessCollector.cs" />

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

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

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

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

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

+    <Compile Include="Properties\AssemblyInfo.cs" />

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

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

+  </ItemGroup>

+  <ItemGroup>

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

+      <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>

+      <Name>AIFramework</Name>

+    </ProjectReference>

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

+      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

+      <Name>Basetypes</Name>

+    </ProjectReference>

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

+      <Project>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</Project>

+      <Name>BoogieDriver</Name>

+    </ProjectReference>

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

+      <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

+      <Name>Core</Name>

+    </ProjectReference>

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

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

+      <Name>ParserHelper</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/GPUVerify/LocalVariableAccessReplacer.cs b/Source/GPUVerify/LocalVariableAccessReplacer.cs
new file mode 100644
index 00000000..4ec382ad
--- /dev/null
+++ b/Source/GPUVerify/LocalVariableAccessReplacer.cs
@@ -0,0 +1,54 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    class LocalVariableAccessReplacer : StandardVisitor

+    {

+

+        GPUVerifier verifier;

+

+        public LocalVariableAccessReplacer(GPUVerifier verifier)

+        {

+            this.verifier = verifier;

+        }

+

+

+        public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)

+        {

+            if (verifier.GetThreadLocalVariables().Contains(node.AssignedVariable.Decl))

+            {

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

+                indexes.Add(verifier.MakeThreadIdExpr(node.tok));

+                return new MapAssignLhs(node.tok, node, indexes);

+            }

+            return node;

+        }

+

+        public override Expr VisitIdentifierExpr(IdentifierExpr node)

+        {

+            if (verifier.GetThreadLocalVariables().Contains(node.Decl))

+            {

+                Console.WriteLine("Replacing " + node);

+

+                ExprSeq MapNameAndThreadID = new ExprSeq();

+                MapNameAndThreadID.Add(new IdentifierExpr(node.tok, node.Decl));

+                MapNameAndThreadID.Add(verifier.MakeThreadIdExpr(node.tok));

+

+                Expr result = new NAryExpr(node.tok, new MapSelect(node.tok, 1), MapNameAndThreadID);

+

+                Console.WriteLine("with " + result);

+                return result;

+

+            }

+

+            return node;

+        }

+

+

+    }

+}

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
new file mode 100644
index 00000000..7c72a87c
--- /dev/null
+++ b/Source/GPUVerify/Main.cs
@@ -0,0 +1,175 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.IO;

+using System.Diagnostics;

+

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    class GPUVerify

+    {

+

+

+        public static void Main(string[] args)

+        {

+            CommandLineOptions.Parse(args);

+

+            if (CommandLineOptions.inputFiles.Count < 1)

+            {

+                OnlyBoogie.ErrorWriteLine("*** Error: No input files were specified.");

+                Environment.Exit(1);

+            }

+

+            foreach (string file in CommandLineOptions.inputFiles)

+            {

+                string extension = Path.GetExtension(file);

+                if (extension != null)

+                {

+                    extension = extension.ToLower();

+                }

+                if (extension != ".bpl")

+                {

+                    OnlyBoogie.ErrorWriteLine("*** Error: '{0}': Filename extension '{1}' is not supported. Input files must be BoogiePL programs (.bpl).", file,

+                        extension == null ? "" : extension);

+                    Environment.Exit(1);

+                }

+            }

+

+            Program program = ParseBoogieProgram(CommandLineOptions.inputFiles, false);

+            if (program == null)

+            {

+                Environment.Exit(1);

+            }

+

+            int errorCount = program.Resolve();

+            if (errorCount != 0)

+            {

+                Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);

+                Environment.Exit(1);

+            }

+

+            errorCount = program.Typecheck();

+

+            if (errorCount != 0)

+            {

+                Console.WriteLine("{0} type checking errors detected in {1}", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);

+                Environment.Exit(1);

+            }

+

+            GPUVerifier verifier = new GPUVerifier(program);

+

+            // TODO: check that no non-barrier procedures are called from the kernel

+

+            verifier.AddInitialAndFinalBarriers();

+

+            verifier.SplitBlocksAtBarriers();

+

+            verifier.ComputeBarrierToNextBarriersProcedures();

+

+            verifier.ComputeBarrierToBarrierPairs();

+

+            foreach (Variable V in verifier.GetGlobalVariables())

+            {

+                program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V)), true));

+            }

+

+            foreach (Variable V in verifier.GetTileStaticVariables())

+            {

+                program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V)), true));

+            }

+

+            using (TokenTextWriter writer = new TokenTextWriter("<console>", Console.Out))

+            {

+                program.Emit(writer);

+            }

+

+

+            /*            errorCount = program.Resolve();

+                        if (errorCount != 0)

+                        {

+                            Console.WriteLine("{0} name resolution errors detected in {1} after transformation", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);

+                            Environment.Exit(1);

+                        }

+

+                        errorCount = program.Typecheck();

+

+                        if (errorCount != 0)

+                        {

+                            Console.WriteLine("{0} type checking errors detected in {1} after transformation", errorCount, CommandLineOptions.inputFiles[CommandLineOptions.inputFiles.Count - 1]);

+                            Environment.Exit(1);

+                        }

+            */

+            //Console.ReadLine();

+

+        }

+

+        private static CtorType MakeArrayBaseType(Variable V)

+        {

+            return new CtorType(V.tok, new TypeCtorDecl(V.tok, "ArrayBase", 0), new TypeSeq());

+        }

+

+

+

+

+

+

+        static Program ParseBoogieProgram(List<string> fileNames, bool suppressTraceOutput)

+        {

+            Program program = null;

+            bool okay = true;

+            for (int fileId = 0; fileId < fileNames.Count; fileId++)

+            {

+                string bplFileName = fileNames[fileId];

+

+                Program programSnippet;

+                int errorCount;

+                try

+                {

+                    var defines = new List<string>() { "FILE_" + fileId };

+                    errorCount = Parser.Parse(bplFileName, defines, out programSnippet);

+                    if (programSnippet == null || errorCount != 0)

+                    {

+                        OnlyBoogie.ErrorWriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);

+                        okay = false;

+                        continue;

+                    }

+                }

+                catch (IOException e)

+                {

+                    OnlyBoogie.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;

+            }

+        }

+

+

+    }

+

+

+

+

+}

diff --git a/Source/GPUVerify/Properties/AssemblyInfo.cs b/Source/GPUVerify/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..cff5de61
--- /dev/null
+++ b/Source/GPUVerify/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("GPUVerify")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("Microsoft")]

+[assembly: AssemblyProduct("GPUVerify")]

+[assembly: AssemblyCopyright("Copyright © Microsoft 2011")]

+[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("2cda06c5-da64-412f-9c94-7edc5fd9147f")]

+

+// 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/Source/GPUVerify/ReadCollector.cs b/Source/GPUVerify/ReadCollector.cs
new file mode 100644
index 00000000..e7fd1eee
--- /dev/null
+++ b/Source/GPUVerify/ReadCollector.cs
@@ -0,0 +1,115 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Boogie;

+using Microsoft.Basetypes;

+using System.Diagnostics;

+

+namespace GPUVerify

+{

+

+

+

+

+    class ReadCollector : AccessCollector

+    {

+

+        public HashSet<AccessRecord> accesses = new HashSet<AccessRecord>();

+

+        public ReadCollector(GPUVerifier verifier)

+            : base(verifier)

+        {

+        }

+

+        public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)

+        {

+            return node;

+        }

+

+        public override Expr VisitNAryExpr(NAryExpr node)

+        {

+            if (node.Fun is MapSelect)

+            {

+                if ((node.Fun as MapSelect).Arity > 1)

+                {

+                    MultiDimensionalMapError();

+                }

+

+                Variable ReadVariable = null;

+                Expr IndexX = node.Args[1];

+                Expr IndexY = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));

+                Expr IndexZ = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));

+

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

+                }

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

+

+

+                if (verifier.GetGlobalVariables().Contains(ReadVariable) || verifier.GetTileStaticVariables().Contains(ReadVariable))

+                {

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

+                }

+

+                return node;

+            }

+            else

+            {

+                return base.VisitNAryExpr(node);

+            }

+        }

+

+

+

+        public override Variable VisitVariable(Variable node)

+        {

+            if (!(verifier.GetGlobalVariables().Contains(node) || verifier.GetTileStaticVariables().Contains(node)))

+            {

+                return node;

+            }

+

+            accesses.Add(new AccessRecord(node, new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0))));

+

+            return node;

+        }

+

+

+    }

+}

diff --git a/Source/GPUVerify/WriteCollector.cs b/Source/GPUVerify/WriteCollector.cs
new file mode 100644
index 00000000..e91244cb
--- /dev/null
+++ b/Source/GPUVerify/WriteCollector.cs
@@ -0,0 +1,107 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+using Microsoft.Basetypes;

+

+namespace GPUVerify

+{

+    class WriteCollector : AccessCollector

+    {

+

+        private AccessRecord access = null;

+

+        public WriteCollector(GPUVerifier verifier)

+            : base(verifier)

+        {

+        }

+

+        public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)

+        {

+            Debug.Assert(NoWrittenVariable());

+            if (verifier.GetGlobalVariables().Contains(node.DeepAssignedVariable) || verifier.GetTileStaticVariables().Contains(node.DeepAssignedVariable))

+            {

+                access = new AccessRecord(node.DeepAssignedVariable, new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0)), new LiteralExpr(node.tok, BigNum.FromInt(0)));

+            }

+            return node;

+        }

+

+        private bool NoWrittenVariable()

+        {

+            return access == null;

+        }

+

+        public override AssignLhs VisitMapAssignLhs(MapAssignLhs node)

+        {

+            Debug.Assert(NoWrittenVariable());

+

+            if (!(verifier.GetGlobalVariables().Contains(node.DeepAssignedVariable) || verifier.GetTileStaticVariables().Contains(node.DeepAssignedVariable)))

+            {

+                return node;

+            }

+

+            Variable WrittenVariable = node.DeepAssignedVariable;

+

+            MapAssignLhs MapAssignX = node;

+

+            CheckMapIndex(MapAssignX);

+            Expr IndexX = MapAssignX.Indexes[0];

+            Expr IndexY = new LiteralExpr(Token.NoToken, BigNum.FromInt(0));

+            Expr IndexZ = new LiteralExpr(Token.NoToken, BigNum.FromInt(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;

+        }

+

+        private void CheckMapIndex(MapAssignLhs node)

+        {

+            if (node.Indexes.Count > 1)

+            {

+                MultiDimensionalMapError();

+            }

+        }

+

+

+

+

+        internal bool FoundWrite()

+        {

+            return access != null;

+        }

+

+        internal AccessRecord GetAccess()

+        {

+            return access;

+        }

+

+    }

+}