using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics;
using Microsoft.Boogie;
using Microsoft.Basetypes;
using System.Diagnostics.Contracts;

namespace GPUVerify
{
    class GPUVerifierLockStep : GPUVerifier
    {

        private static int WhileLoopCounter;
        private static int IfCounter;
        private static HashSet<Microsoft.Boogie.Type> RequiredHavocVariables;


        private int TempCounter = 0;
        private int invariantGenerationCounter;

        public GPUVerifierLockStep(Program program)
            : base(program)
        {
            CheckWellFormedness();
        }

        override internal void doit()
        {

            PromoteTileStaticToGlobal();

            AddStartAndEndBarriers();

            PullOutNonLocalAccesses();

            if (!CommandLineOptions.OnlyDivergence)
            {
                AddRaceCheckingInstrumentation();
            }

            AbstractSharedState();

            MakeKerenelPredicated();

            MakeKernelDualised();

            GenerateBarrierImplementation();

            GenerateKernelPrecondition();

            if (CommandLineOptions.Inference)
            {
                ComputeInvariant();
            }

            if (CommandLineOptions.outputFile == null)
            {
                CommandLineOptions.outputFile = "temp_ready_to_verify.bpl";
            }

            using (TokenTextWriter writer = new TokenTextWriter(CommandLineOptions.outputFile))
            {
                Program.Emit(writer);
            }



        }

        private void ComputeInvariant()
        {
            invariantGenerationCounter = 0;

            HashSet<string> LocalNames = new HashSet<string>();
            foreach (Variable v in KernelImplementation.LocVars)
            {
                string basicName = StripThreadIdentifier(v.Name);
                LocalNames.Add(basicName);
            }

            AddCandidateInvariants(KernelImplementation.StructuredStmts, LocalNames);
        }

        private void AddCandidateInvariants(StmtList stmtList, HashSet<string> LocalNames)
        {
            foreach (BigBlock bb in stmtList.BigBlocks)
            {
                AddCandidateInvariants(bb, LocalNames);
            }
        }

        private void AddCandidateInvariants(BigBlock bb, HashSet<string> LocalNames)
        {
            if (bb.ec is WhileCmd)
            {
                WhileCmd wc = bb.ec as WhileCmd;

                foreach(string lv in LocalNames)
                {
                    AddCandidateInvariant(wc, Expr.Eq(
                        // Int type used here, but it doesn't matter as we will print and then re-parse the program
                        new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv + "$1", Microsoft.Boogie.Type.Int))),
                        new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, lv + "$2", Microsoft.Boogie.Type.Int)))
                    ));
                }

                if (!CommandLineOptions.OnlyDivergence)
                {
                    AddRaceCheckingCandidateInvariants(wc);
                }

                AddCandidateInvariants(wc.Body, LocalNames);
            }
            else if (bb.ec is IfCmd)
            {
                // We should have done predicated execution by now, so we won't have any if statements
                Debug.Assert(false);
            }
            else
            {
                Debug.Assert(bb.ec == null);
            }
        }

        private void AddRaceCheckingCandidateInvariants(WhileCmd wc)
        {
            foreach (Variable v in GlobalVariables)
            {
                AddNoReadOrWriteCandidateInvariants(wc, v);
                AddReadOrWrittenOffsetIsThreadId(wc, v, "READ");
                AddReadOrWrittenOffsetIsThreadId(wc, v, "WRITE");
            }

            foreach (Variable v in TileStaticVariables)
            {
                AddNoReadOrWriteCandidateInvariants(wc, v);
                AddReadOrWrittenOffsetIsThreadId(wc, v, "READ");
                AddReadOrWrittenOffsetIsThreadId(wc, v, "WRITE");
            }
        }

        private void AddReadOrWrittenOffsetIsThreadId(WhileCmd wc, Variable v, string ReadOrWrite)
        {
            if (HasXDimension(v) && IndexTypeOfXDimension(v).Equals(GetTypeOfId("X")))
            {
                AddCandidateInvariant(wc,
                    Expr.Imp(
                        new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
                        Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeOffsetXVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "X", 1))))
                );
                AddCandidateInvariant(wc,
                    Expr.Imp(
                        new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
                        Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeOffsetXVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "X", 2))))
                );
            }

            if (HasYDimension(v) && HasId("Y") && IndexTypeOfYDimension(v).Equals(GetTypeOfId("Y")))
            {
                AddCandidateInvariant(wc,
                    Expr.Imp(
                        new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
                        Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeOffsetYVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "Y", 1))))
                );
                AddCandidateInvariant(wc,
                    Expr.Imp(
                        new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
                        Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeOffsetYVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "Y", 2))))
                );
            }

            if (HasZDimension(v) && HasId("Z") && IndexTypeOfZDimension(v).Equals(GetTypeOfId("Z")))
            {
                AddCandidateInvariant(wc,
                    Expr.Imp(
                        new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
                        Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(1).VisitVariable(MakeOffsetZVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "Z", 1))))
                );
                AddCandidateInvariant(wc,
                    Expr.Imp(
                        new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),
                        Expr.Eq(new IdentifierExpr(wc.tok, new VariableDualiser(2).VisitVariable(MakeOffsetZVariable(v, ReadOrWrite))), new IdentifierExpr(wc.tok, MakeThreadId(wc.tok, "Z", 2))))
                );
            }
            
        }

        private void AddNoReadOrWriteCandidateInvariants(WhileCmd wc, Variable v)
        {
            AddNoReadOrWriteCandidateInvariant(wc, v, "READ", "1");
            AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE", "1");
            AddNoReadOrWriteCandidateInvariant(wc, v, "READ", "2");
            AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE", "2");
        }

        private void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite, string OneOrTwo)
        {
                            Variable ReadHasOccurred1 = MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);
                            ReadHasOccurred1.Name = ReadHasOccurred1.Name + "$" + OneOrTwo;
                            ReadHasOccurred1.TypedIdent.Name = ReadHasOccurred1.TypedIdent.Name + "$" + OneOrTwo;
                            AddCandidateInvariant(wc, Expr.Not(new IdentifierExpr(wc.tok, ReadHasOccurred1)));
        }

        private void AddCandidateInvariant(WhileCmd wc, Expr e)
        {
            Constant ExistentialBooleanConstant = MakeExistentialBoolean(wc.tok);
            IdentifierExpr ExistentialBoolean = new IdentifierExpr(wc.tok, ExistentialBooleanConstant);
            wc.Invariants.Add(new AssertCmd(wc.tok, Expr.Imp(ExistentialBoolean, e)));
            Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);
        }

        private Constant MakeExistentialBoolean(IToken tok)
        {
            Constant ExistentialBooleanConstant = new Constant(tok, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);
            invariantGenerationCounter++;
            ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });
            return ExistentialBooleanConstant;
        }

        private string StripThreadIdentifier(string p)
        {
            return p.Substring(0, p.IndexOf("$"));
        }

        private void AddStartAndEndBarriers()
        {
            CallCmd FirstBarrier = new CallCmd(KernelImplementation.tok, "BARRIER", new ExprSeq(), new IdentifierExprSeq());
            CallCmd LastBarrier = new CallCmd(KernelImplementation.tok, "BARRIER", new ExprSeq(), new IdentifierExprSeq());

            CmdSeq newCommands = new CmdSeq();
            newCommands.Add(FirstBarrier);
            foreach(Cmd c in KernelImplementation.StructuredStmts.BigBlocks[0].simpleCmds)
            {
                newCommands.Add(c);
            }
            KernelImplementation.StructuredStmts.BigBlocks[0].simpleCmds = newCommands;

            CmdSeq lastCommand = new CmdSeq();
            lastCommand.Add(LastBarrier);
            BigBlock bb = new BigBlock(KernelProcedure.tok, "__lastBarrier", lastCommand, null, null);

            KernelImplementation.StructuredStmts.BigBlocks.Add(bb);
        }

        private void GenerateKernelPrecondition()
        {

            if (!CommandLineOptions.OnlyDivergence)
            {
                foreach (Variable v in GlobalVariables)
                {
                    AddRequiresNoPendingAccess(v);
                }
                foreach (Variable v in TileStaticVariables)
                {
                    AddRequiresNoPendingAccess(v);
                }
            }

            Expr AssumeDistinctThreads = null;
            Expr AssumeThreadIdsInRange = null;
            IToken tok = KernelImplementation.tok;

            GeneratePreconditionsForDimension(ref AssumeDistinctThreads, ref AssumeThreadIdsInRange, tok, "X");
            GeneratePreconditionsForDimension(ref AssumeDistinctThreads, ref AssumeThreadIdsInRange, tok, "Y");
            GeneratePreconditionsForDimension(ref AssumeDistinctThreads, ref AssumeThreadIdsInRange, tok, "Z");

            if (AssumeDistinctThreads != null)
            {
                Debug.Assert(AssumeThreadIdsInRange != null);
                CmdSeq newCmdSeq = new CmdSeq();
                newCmdSeq.Add(new AssumeCmd(KernelProcedure.tok, AssumeDistinctThreads));
                newCmdSeq.Add(new AssumeCmd(KernelProcedure.tok, AssumeThreadIdsInRange));
                foreach (Cmd c in KernelImplementation.StructuredStmts.BigBlocks[0].simpleCmds)
                {
                    newCmdSeq.Add(c);
                }
                KernelImplementation.StructuredStmts.BigBlocks[0].simpleCmds = newCmdSeq;
            }
            else
            {
                Debug.Assert(AssumeThreadIdsInRange == null);
            }


        }

        private void GeneratePreconditionsForDimension(ref Expr AssumeDistinctThreads, ref Expr AssumeThreadIdsInRange, IToken tok, String dimension)
        {
            if (HasId(dimension))
            {
                if (GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)))
                {
                    KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, MakeTileSize(tok, dimension)), ZeroBV(tok))));
                    KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, MakeNumTiles(tok, dimension)), ZeroBV(tok))));
                    KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, MakeTileId(tok, dimension)), ZeroBV(tok))));
                    KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeTileId(tok, dimension)), new IdentifierExpr(tok, MakeNumTiles(tok, dimension)))));
                }
                else
                {
                    KernelProcedure.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, MakeTileSize(tok, dimension)), Zero(tok))));
                    KernelProcedure.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, MakeNumTiles(tok, dimension)), Zero(tok))));
                    KernelProcedure.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, MakeTileId(tok, dimension)), Zero(tok))));
                    KernelProcedure.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, MakeTileId(tok, dimension)), new IdentifierExpr(tok, MakeNumTiles(tok, dimension)))));
                }
                Expr AssumeThreadsDistinctInDimension =
                        Expr.Neq(
                        new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)),
                        new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2))
                        );

                AssumeDistinctThreads = (null == AssumeDistinctThreads) ? AssumeThreadsDistinctInDimension : Expr.Or(AssumeDistinctThreads, AssumeThreadsDistinctInDimension);

                Expr AssumeThreadIdsInRangeInDimension =
                    GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)) ?
                        Expr.And(
                            Expr.And(
                            MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), ZeroBV(tok)),
                            MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), ZeroBV(tok))
                            ),
                            Expr.And(
                            MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, MakeTileSize(tok, dimension))),
                            MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, MakeTileSize(tok, dimension)))
                            ))
                    :
                        Expr.And(
                            Expr.And(
                            Expr.Ge(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), Zero(tok)),
                            Expr.Ge(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), Zero(tok))
                            ),
                            Expr.And(
                            Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, MakeTileSize(tok, dimension))),
                            Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, MakeTileSize(tok, dimension)))
                            ));

                AssumeThreadIdsInRange = (null == AssumeThreadIdsInRange) ? AssumeThreadIdsInRangeInDimension : Expr.And(AssumeThreadIdsInRange, AssumeThreadIdsInRangeInDimension);
            }
        }

        private Expr MakeBitVectorBinaryBoolean(string functionName, Expr lhs, Expr rhs)
        {
            return new NAryExpr(lhs.tok, new FunctionCall(new Function(lhs.tok, functionName, new VariableSeq(new Variable[] { 
                new LocalVariable(lhs.tok, new TypedIdent(lhs.tok, "arg1", Microsoft.Boogie.Type.GetBvType(32))),
                new LocalVariable(lhs.tok, new TypedIdent(lhs.tok, "arg2", Microsoft.Boogie.Type.GetBvType(32)))
            }), new LocalVariable(lhs.tok, new TypedIdent(lhs.tok, "result", Microsoft.Boogie.Type.Bool)))), new ExprSeq(new Expr[] { lhs, rhs }));
        }

        private Constant MakeTileSize(IToken tok, string dimension)
        {
            return new Constant(tok, new TypedIdent(tok, "TILE_SIZE_" + dimension, GetTypeOfId(dimension)));
        }

        private Constant MakeNumTiles(IToken tok, string dimension)
        {
            return new Constant(tok, new TypedIdent(tok, "NUM_TILES_" + dimension, GetTypeOfId(dimension)));
        }

        private LocalVariable MakeThreadId(IToken tok, string dimension, int number)
        {
            return new LocalVariable(tok, new TypedIdent(tok, "_" + dimension + "$" + number, GetTypeOfId(dimension)));
        }

        private Constant MakeTileId(IToken tok, string dimension)
        {
            return new Constant(tok, new TypedIdent(tok, "_tile_" + dimension, GetTypeOfId(dimension)));
        }

        private static LiteralExpr Zero(IToken tok)
        {
            return new LiteralExpr(tok, BigNum.FromInt(0));
        }

        private static LiteralExpr ZeroBV(IToken tok)
        {
            return new LiteralExpr(tok, BigNum.FromInt(0), 32);
        }

        private bool HasId(string idLetter)
        {
            foreach (Variable v in ThreadLocalVariables)
            {
                if (v.Name == "_" + idLetter)
                {
                    return true;
                }
            }
            return false;
        }

        private Microsoft.Boogie.Type GetTypeOfId(string idLetter)
        {
            foreach (Variable v in ThreadLocalVariables)
            {
                if (v.Name == "_" + idLetter)
                {
                    return v.TypedIdent.Type;
                }
            }

            Debug.Assert(false);

            return null;
        }

        private void AddRequiresNoPendingAccess(Variable v)
        {
            IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, "READ")));
            IdentifierExpr ReadAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, "READ")));
            IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, "WRITE")));
            IdentifierExpr WriteAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, "WRITE")));
            KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.And(Expr.Not(ReadAccessOccurred2), Expr.And(Expr.Not(WriteAccessOccurred1), Expr.Not(WriteAccessOccurred2))))));
        }

        private void PromoteTileStaticToGlobal()
        {
            VariableSeq newLocVars = new VariableSeq();

            foreach(Variable v in KernelImplementation.LocVars)
            {
                if (TileStaticVariables.Contains(v))
                {
                    Program.TopLevelDeclarations.Add(v);
                    KernelProcedure.Modifies.Add(new IdentifierExpr(v.tok, v));
                }
                else
                {
                    newLocVars.Add(v);
                }
            }

            KernelImplementation.LocVars = newLocVars;

        }

        private void GenerateBarrierImplementation()
        {
            IToken tok = BarrierProcedure.tok;

            List<BigBlock> bigblocks = new List<BigBlock>();
            BigBlock checkNonDivergence = new BigBlock(tok, "__BarrierImpl", new CmdSeq(), null, null);
            bigblocks.Add(checkNonDivergence);

            IdentifierExpr P1 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[0].TypedIdent));
            IdentifierExpr P2 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[1].TypedIdent));

            checkNonDivergence.simpleCmds.Add(new AssertCmd(tok, Expr.Eq(P1, P2)));

            if (!CommandLineOptions.OnlyDivergence || !CommandLineOptions.FullAbstraction)
            {
                List<BigBlock> returnbigblocks = new List<BigBlock>();
                returnbigblocks.Add(new BigBlock(tok, "__Disabled", new CmdSeq(), null, new ReturnCmd(tok)));
                StmtList returnstatement = new StmtList(returnbigblocks, BarrierProcedure.tok);
                checkNonDivergence.ec = new IfCmd(tok, Expr.And(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);
            }

            if (!CommandLineOptions.OnlyDivergence)
            {
                BigBlock checkForRaces = new BigBlock(tok, "__CheckForRaces", new CmdSeq(), null, null);
                bigblocks.Add(checkForRaces);
                foreach (Variable v in GlobalVariables)
                {
                    CheckForRaces(tok, checkForRaces, v);
                }
                foreach (Variable v in TileStaticVariables)
                {
                    CheckForRaces(tok, checkForRaces, v);
                }

                foreach (Variable v in GlobalVariables)
                {
                    SetNoAccessOccurred(tok, checkForRaces, v);
                }
                foreach (Variable v in TileStaticVariables)
                {
                    SetNoAccessOccurred(tok, checkForRaces, v);
                }

            }

            if (!CommandLineOptions.FullAbstraction)
            {
                BigBlock havocSharedState = new BigBlock(tok, "__HavocSharedState", new CmdSeq(), null, null);
                bigblocks.Add(havocSharedState);
                foreach (Variable v in GlobalVariables)
                {
                    HavocAndAssumeEquality(tok, havocSharedState, v);
                }
                foreach (Variable v in TileStaticVariables)
                {
                    HavocAndAssumeEquality(tok, havocSharedState, v);
                }

            }

            StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok);
            Implementation BarrierImplementation = new Implementation(BarrierProcedure.tok, BarrierProcedure.Name, new TypeVariableSeq(), BarrierProcedure.InParams, BarrierProcedure.OutParams, new VariableSeq(), statements);

            BarrierImplementation.AddAttribute("inline", new object[] { new LiteralExpr(tok, BigNum.FromInt(1)) });
            BarrierProcedure.AddAttribute("inline", new object[] { new LiteralExpr(tok, BigNum.FromInt(1)) });

            Program.TopLevelDeclarations.Add(BarrierImplementation);
        }

        private void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v)
        {
            SetNoAccessOccurred(tok, bb, v, "READ");
            SetNoAccessOccurred(tok, bb, v, "WRITE");
        }

        private void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType)
        {
            IdentifierExpr AccessOccurred1 = new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));
            IdentifierExpr AccessOccurred2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));

            BarrierProcedure.Modifies.Add(AccessOccurred1);
            BarrierProcedure.Modifies.Add(AccessOccurred2);

            List<AssignLhs> lhss = new List<AssignLhs>();
            lhss.Add(new SimpleAssignLhs(tok, AccessOccurred1));
            lhss.Add(new SimpleAssignLhs(tok, AccessOccurred2));
            List<Expr> rhss = new List<Expr>();
            rhss.Add(Expr.False);
            rhss.Add(Expr.False);
            bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));
        }

        private void CheckForRaces(IToken tok, BigBlock bb, Variable v)
        {
            bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(GenerateRaceCondition(tok, v, "WRITE", "WRITE"))));
            bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(GenerateRaceCondition(tok, v, "READ", "WRITE"))));
        }

        private static Expr GenerateRaceCondition(IToken tok, Variable v, string FirstAccessType, string SecondAccessType)
        {
            Expr RaceCondition = Expr.And(
                new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, FirstAccessType))),
                new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, SecondAccessType))));

            if (HasXDimension(v))
            {
                RaceCondition = Expr.And(RaceCondition, Expr.Eq(
                    new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeOffsetXVariable(v, FirstAccessType))),
                    new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeOffsetXVariable(v, SecondAccessType)))
                ));
            }

            if (HasYDimension(v))
            {
                RaceCondition = Expr.And(RaceCondition, Expr.Eq(
                    new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeOffsetYVariable(v, FirstAccessType))),
                    new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeOffsetYVariable(v, SecondAccessType)))
                    ));
            }

            if (HasZDimension(v))
            {
                RaceCondition = Expr.And(RaceCondition, Expr.Eq(
                    new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeOffsetZVariable(v, FirstAccessType))),
                    new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeOffsetZVariable(v, SecondAccessType)))
                    ));
            }

            return RaceCondition;
        }

        private static bool HasZDimension(Variable v)
        {
            if (v.TypedIdent.Type is MapType)
            {
                MapType mt = v.TypedIdent.Type as MapType;

                if (mt.Result is MapType)
                {
                    MapType mt2 = mt.Result as MapType;
                    if (mt2.Result is MapType)
                    {
                        Debug.Assert(!((mt2.Result as MapType).Result is MapType));
                        return true;
                    }
                }
            }
            return false;
        }

        private static bool HasYDimension(Variable v)
        {
            return v.TypedIdent.Type is MapType && (v.TypedIdent.Type as MapType).Result is MapType;
        }

        private static bool HasXDimension(Variable v)
        {
            return v.TypedIdent.Type is MapType;
        }

        private void HavocAndAssumeEquality(IToken tok, BigBlock bb, Variable v)
        {
            IdentifierExpr v1 = new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(v.Clone() as Variable));
            IdentifierExpr v2 = new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(v.Clone() as Variable));

            bb.simpleCmds.Add(new HavocCmd(tok, new IdentifierExprSeq(new IdentifierExpr[] { v1, v2 })));
            bb.simpleCmds.Add(new AssumeCmd(tok, Expr.Eq(v1, v2)));
            BarrierProcedure.Modifies.Add(v1);
            BarrierProcedure.Modifies.Add(v2);

            if (!KernelProcedure.Modifies.Has(v1))
            {
                Debug.Assert(!KernelProcedure.Modifies.Has(v2));
                KernelProcedure.Modifies.Add(v1);
                KernelProcedure.Modifies.Add(v2);
            }

        }

        private void AbstractSharedState()
        {
            if (!CommandLineOptions.FullAbstraction)
            {
                return; // There's actually nothing to do here
            }

            List<Declaration> NewTopLevelDeclarations = new List<Declaration>();

            foreach (Declaration d in Program.TopLevelDeclarations)
            {
                if (d is Variable && GlobalVariables.Contains(d as Variable))
                {
                    continue;
                }

                if (d is Implementation)
                {
                    PerformFullSharedStateAbstraction(d as Implementation);
                }

                if (d is Procedure)
                {
                    PerformFullSharedStateAbstraction(d as Procedure);
                }

                NewTopLevelDeclarations.Add(d);

            }

            Program.TopLevelDeclarations = NewTopLevelDeclarations;

        }

        private void PerformFullSharedStateAbstraction(Procedure proc)
        {
            IdentifierExprSeq NewModifies = new IdentifierExprSeq();

            foreach (IdentifierExpr e in proc.Modifies)
            {
                if (!(GlobalVariables.Contains(e.Decl)))
                {
                    NewModifies.Add(e);
                }
            }

            proc.Modifies = NewModifies;

        }

        private void PerformFullSharedStateAbstraction(Implementation impl)
        {
            VariableSeq NewLocVars = new VariableSeq();

            foreach (Variable v in impl.LocVars)
            {
                if (!TileStaticVariables.Contains(v))
                {
                    NewLocVars.Add(v);
                }
            }

            impl.LocVars = NewLocVars;

            impl.StructuredStmts = PerformFullSharedStateAbstraction(impl.StructuredStmts);

        }


        private StmtList PerformFullSharedStateAbstraction(StmtList stmtList)
        {
            Contract.Requires(stmtList != null);
            
            StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);

            foreach (BigBlock bodyBlock in stmtList.BigBlocks)
            {
                result.BigBlocks.Add(PerformFullSharedStateAbstraction(bodyBlock));
            }
            return result;
        }

        private BigBlock PerformFullSharedStateAbstraction(BigBlock bb)
        {
            BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);

            foreach (Cmd c in bb.simpleCmds)
            {
                if (c is AssignCmd)
                {
                    AssignCmd assign = c as AssignCmd;
                    Debug.Assert(assign.Lhss.Count == 1);
                    Debug.Assert(assign.Rhss.Count == 1);
                    AssignLhs lhs = assign.Lhss[0];
                    Expr rhs = assign.Rhss[0];
                    ReadCollector rc = new ReadCollector(GlobalVariables, TileStaticVariables);
                    rc.Visit(rhs);
                    if (rc.accesses.Count > 0)
                    {
                        Debug.Assert(lhs is SimpleAssignLhs);
                        result.simpleCmds.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));
                        continue;
                    }

                    WriteCollector wc = new WriteCollector(GlobalVariables, TileStaticVariables);
                    wc.Visit(lhs);
                    if (wc.GetAccess() != null)
                    {
                        continue; // Just remove the write
                    }

                }
                result.simpleCmds.Add(c);
            }

            if (bb.ec is WhileCmd)
            {
                WhileCmd WhileCommand = bb.ec as WhileCmd;
                result.ec = new WhileCmd(WhileCommand.tok, WhileCommand.Guard, WhileCommand.Invariants, PerformFullSharedStateAbstraction(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, PerformFullSharedStateAbstraction(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? PerformFullSharedStateAbstraction(IfCommand.elseBlock) : null);
            }
            else
            {
                Debug.Assert(bb.ec == null);
            }

            return result;

        }





        private void AddRaceCheckingInstrumentation()
        {
            foreach(Variable v in GlobalVariables)
            {
                AddRaceCheckingInstrumentation(v);
            }
            foreach (Variable v in TileStaticVariables)
            {
                AddRaceCheckingInstrumentation(v);
            }

            AddRaceCheckCalls(KernelImplementation);

        }

        private void AddRaceCheckingInstrumentation(Variable v)
        {
            IdentifierExprSeq vars = AddRaceCheckingDeclarations(v);
            foreach (IdentifierExpr e in vars)
            {
                KernelProcedure.Modifies.Add(e);
            }
            AddRaceCheckingProcedures(v);
        }

        private void AddRaceCheckCalls(Implementation impl)
        {
            impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
        }

        private StmtList AddRaceCheckCalls(StmtList stmtList)
        {
            Contract.Requires(stmtList != null);
            
            StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);

            foreach (BigBlock bodyBlock in stmtList.BigBlocks)
            {
                result.BigBlocks.Add(AddRaceCheckCalls(bodyBlock));
            }
            return result;
        }

        private BigBlock AddRaceCheckCalls(BigBlock bb)
        {
            BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);

            foreach (Cmd c in bb.simpleCmds)
            {
                if (c is AssignCmd)
                {
                    AssignCmd assign = c as AssignCmd;
                    Debug.Assert(assign.Lhss.Count == 1);
                    Debug.Assert(assign.Rhss.Count == 1);
                    AssignLhs lhs = assign.Lhss[0];
                    Expr rhs = assign.Rhss[0];

                    ReadCollector rc = new ReadCollector(GlobalVariables, TileStaticVariables);
                    rc.Visit(rhs);
                    if (rc.accesses.Count > 0)
                    {
                        Debug.Assert(rc.accesses.Count == 1);
                        AccessRecord ar = rc.accesses.ToList()[0];
                        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);
                        }

                        result.simpleCmds.Add(new CallCmd(c.tok, "_LOG_READ_" + ar.v.Name, inParams, new IdentifierExprSeq()));
                    }

                    WriteCollector wc = new WriteCollector(GlobalVariables, TileStaticVariables);
                    wc.Visit(lhs);
                    if (wc.GetAccess() != null)
                    {
                        AccessRecord ar = wc.GetAccess();
                        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);
                        }

                        result.simpleCmds.Add(new CallCmd(c.tok, "_LOG_WRITE_" + ar.v.Name, inParams, new IdentifierExprSeq()));
                    }



                }
                result.simpleCmds.Add(c);
            }

            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
            {
                Debug.Assert(bb.ec == null);
            }

            return result;

        }

        private void AddRaceCheckingProcedures(Variable v)
        {
            AddLogAccessProcedure(v, "READ");
            AddLogAccessProcedure(v, "WRITE");
        }

        private void AddLogAccessProcedure(Variable v, string ReadOrWrite)
        {
            VariableSeq inParams = new VariableSeq();
            IdentifierExprSeq modifies = new IdentifierExprSeq();
            Variable ReadOrWriteHasOccurredVariable = MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);
            Variable ReadOrWriteOffsetXVariable = null;
            Variable ReadOrWriteOffsetYVariable = null;
            Variable ReadOrWriteOffsetZVariable = null;
            Variable XParameterVariable = null;
            Variable YParameterVariable = null;
            Variable ZParameterVariable = null;

            modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteHasOccurredVariable));

            if (v.TypedIdent.Type is MapType)
            {
                MapType mt = v.TypedIdent.Type as MapType;
                Debug.Assert(mt.Arguments.Length == 1);
                Debug.Assert(IsIntOrBv32(mt.Arguments[0]));

                ReadOrWriteOffsetXVariable = MakeOffsetXVariable(v, ReadOrWrite);
                modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetXVariable));
                XParameterVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "_X", GetTypeOfId("X")));
                if (mt.Result is MapType)
                {
                    MapType mt2 = mt.Result as MapType;
                    Debug.Assert(mt2.Arguments.Length == 1);
                    Debug.Assert(IsIntOrBv32(mt2.Arguments[0]));
                    ReadOrWriteOffsetYVariable = MakeOffsetYVariable(v, ReadOrWrite);
                    modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetYVariable));
                    YParameterVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "_Y", GetTypeOfId("Y")));
                    if (mt2.Result is MapType)
                    {
                        MapType mt3 = mt2.Arguments[0] as MapType;
                        Debug.Assert(mt3.Arguments.Length == 1);
                        Debug.Assert(IsIntOrBv32(mt3.Arguments[0]));
                        Debug.Assert(!(mt3.Result is MapType));
                        ReadOrWriteOffsetZVariable = MakeOffsetZVariable(v, ReadOrWrite);
                        modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetZVariable));
                        ZParameterVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "_Z", GetTypeOfId("Z")));
                    }
                }
            }

            if (ZParameterVariable != null)
            {
                inParams.Add(ZParameterVariable);
            }

            if (YParameterVariable != null)
            {
                inParams.Add(YParameterVariable);
            }

            if (XParameterVariable != null)
            {
                inParams.Add(XParameterVariable);
            }

            Procedure LogReadOrWriteProcedure = new Procedure(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), inParams, new VariableSeq(), new RequiresSeq(), modifies, new EnsuresSeq());
            LogReadOrWriteProcedure.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });


            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(ReadOrWriteHasOccurredVariable, new IdentifierExpr(v.tok, TrackVariable), Expr.True));
            if (ReadOrWriteOffsetXVariable != null)
            {
                simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteOffsetXVariable, new IdentifierExpr(v.tok, TrackVariable), new IdentifierExpr(v.tok, XParameterVariable)));
            }
            if (ReadOrWriteOffsetYVariable != null)
            {
                simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteOffsetYVariable, new IdentifierExpr(v.tok, TrackVariable), new IdentifierExpr(v.tok, YParameterVariable)));
            }
            if (ReadOrWriteOffsetZVariable != null)
            {
                simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteOffsetZVariable, new IdentifierExpr(v.tok, TrackVariable), new IdentifierExpr(v.tok, ZParameterVariable)));
            }


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

            StmtList statements = new StmtList(bigblocks, v.tok);

            Implementation LogReadOrWriteImplementation = new Implementation(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), inParams, new VariableSeq(), locals, statements);
            LogReadOrWriteImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

            Program.TopLevelDeclarations.Add(LogReadOrWriteProcedure);
            Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);
        }

        private static GlobalVariable MakeOffsetZVariable(Variable v, string ReadOrWrite)
        {
            return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_OFFSET_Z_" + v.Name, IndexTypeOfZDimension(v)));
        }

        private static GlobalVariable MakeOffsetYVariable(Variable v, string ReadOrWrite)
        {
            return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_OFFSET_Y_" + v.Name, IndexTypeOfYDimension(v)));
        }

        private static GlobalVariable MakeOffsetXVariable(Variable v, string ReadOrWrite)
        {
            return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_OFFSET_X_" + v.Name, IndexTypeOfXDimension(v)));
        }

        private static GlobalVariable MakeReadOrWriteHasOccurredVariable(Variable v, string ReadOrWrite)
        {
            return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));
        }

        private static Microsoft.Boogie.Type IndexTypeOfZDimension(Variable v)
        {
            Contract.Requires(HasZDimension(v));
            MapType mt = v.TypedIdent.Type as MapType;
            MapType mt2 = mt.Result as MapType;
            MapType mt3 = mt2.Result as MapType;
            return mt3.Arguments[0];
        }

        private static Microsoft.Boogie.Type IndexTypeOfYDimension(Variable v)
        {
            Contract.Requires(HasYDimension(v));
            MapType mt = v.TypedIdent.Type as MapType;
            MapType mt2 = mt.Result as MapType;
            return mt2.Arguments[0];
        }

        private static Microsoft.Boogie.Type IndexTypeOfXDimension(Variable v)
        {
            Contract.Requires(HasXDimension(v));
            MapType mt = v.TypedIdent.Type as MapType;
            return mt.Arguments[0];
        }

        private 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);
        }

        private IdentifierExprSeq AddRaceCheckingDeclarations(Variable v)
        {
            IdentifierExprSeq result = new IdentifierExprSeq();

            Variable ReadHasOccurred = new GlobalVariable(v.tok, new TypedIdent(v.tok, "_READ_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));
            Variable WriteHasOccurred = new GlobalVariable(v.tok, new TypedIdent(v.tok, "_WRITE_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));

            result.Add(new IdentifierExpr(v.tok, ReadHasOccurred));
            result.Add(new IdentifierExpr(v.tok, WriteHasOccurred));

            Program.TopLevelDeclarations.Add(ReadHasOccurred);
            Program.TopLevelDeclarations.Add(WriteHasOccurred);
            if (v.TypedIdent.Type is MapType)
            {
                MapType mt = v.TypedIdent.Type as MapType;
                Debug.Assert(mt.Arguments.Length == 1);
                Debug.Assert(IsIntOrBv32(mt.Arguments[0]));

                Variable ReadOffsetX = MakeOffsetXVariable(v, "READ");
                Variable WriteOffsetX = MakeOffsetXVariable(v, "WRITE");
                result.Add(new IdentifierExpr(v.tok, ReadOffsetX));
                result.Add(new IdentifierExpr(v.tok, WriteOffsetX));
                Program.TopLevelDeclarations.Add(ReadOffsetX);
                Program.TopLevelDeclarations.Add(WriteOffsetX);

                if (mt.Result is MapType)
                {
                    MapType mt2 = mt.Result as MapType;
                    Debug.Assert(mt2.Arguments.Length == 1);
                    Debug.Assert(IsIntOrBv32(mt2.Arguments[0]));

                    Variable ReadOffsetY = MakeOffsetYVariable(v, "READ");
                    Variable WriteOffsetY = MakeOffsetYVariable(v, "WRITE");
                    result.Add(new IdentifierExpr(v.tok, ReadOffsetY));
                    result.Add(new IdentifierExpr(v.tok, WriteOffsetY));
                    Program.TopLevelDeclarations.Add(ReadOffsetY);
                    Program.TopLevelDeclarations.Add(WriteOffsetY);

                    if (mt2.Result is MapType)
                    {
                        MapType mt3 = mt2.Arguments[0] as MapType;
                        Debug.Assert(mt3.Arguments.Length == 1);
                        Debug.Assert(IsIntOrBv32(mt3.Arguments[0]));
                        Debug.Assert(!(mt3.Result is MapType));

                        Variable ReadOffsetZ = MakeOffsetZVariable(v, "READ");
                        Variable WriteOffsetZ = MakeOffsetZVariable(v, "WRITE");
                        result.Add(new IdentifierExpr(v.tok, ReadOffsetZ));
                        result.Add(new IdentifierExpr(v.tok, WriteOffsetZ));
                        Program.TopLevelDeclarations.Add(ReadOffsetZ);
                        Program.TopLevelDeclarations.Add(WriteOffsetZ);

                    }
                }
            }

            return result;
        }

        private bool IsIntOrBv32(Microsoft.Boogie.Type type)
        {
            return type.Equals(Microsoft.Boogie.Type.Int) || type.Equals(Microsoft.Boogie.Type.GetBvType(32));
        }

        private void PullOutNonLocalAccesses()
        {
            KernelImplementation.StructuredStmts = PullOutNonLocalAccesses(KernelImplementation.StructuredStmts);
        }

        private StmtList PullOutNonLocalAccesses(StmtList stmtList)
        {
            Contract.Requires(stmtList != null);            

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

            foreach (BigBlock bodyBlock in stmtList.BigBlocks)
            {
                result.BigBlocks.Add(PullOutNonLocalAccesses(bodyBlock));
            }

            return result;
        }

        private BigBlock PullOutNonLocalAccesses(BigBlock bb)
        {

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

            foreach (Cmd c in bb.simpleCmds)
            {

                if (c is CallCmd)
                {
                    CallCmd call = c as CallCmd;

                    List<Expr> newIns = new List<Expr>();

                    for (int i = 0; i < call.Ins.Count; i++)
                    {
                        Expr e = call.Ins[i];

                        while (NonLocalAccessCollector.ContainsNonLocalAccess(e, GlobalVariables, TileStaticVariables))
                        {
                            AssignCmd assignToTemp;
                            LocalVariable tempDecl;
                            e = ExtractLocalAccessToTemp(e, out assignToTemp, out tempDecl);
                            result.simpleCmds.Add(assignToTemp);
                            KernelImplementation.LocVars.Add(tempDecl);
                        }

                        newIns.Add(e);

                    }

                    result.simpleCmds.Add(new CallCmd(call.tok, call.callee, newIns, call.Outs));
                }
                else if (c is AssignCmd)
                {
                    AssignCmd assign = c as AssignCmd;

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

                    AssignLhs lhs = assign.Lhss.ElementAt(0);
                    Expr rhs = assign.Rhss.ElementAt(0);

                    if (!NonLocalAccessCollector.ContainsNonLocalAccess(rhs, GlobalVariables, TileStaticVariables) || (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, GlobalVariables, TileStaticVariables) && NonLocalAccessCollector.IsNonLocalAccess(rhs, GlobalVariables, TileStaticVariables)))
                    {
                        result.simpleCmds.Add(c);
                    }
                    else
                    {
                        rhs = PullOutNonLocalAccessesIntoTemps(result, rhs);
                        List<AssignLhs> newLhss = new List<AssignLhs>();
                        newLhss.Add(lhs);
                        List<Expr> newRhss = new List<Expr>();
                        newRhss.Add(rhs);
                        result.simpleCmds.Add(new AssignCmd(assign.tok, newLhss, newRhss));
                    }

                }
                else if (c is HavocCmd)
                {
                    result.simpleCmds.Add(c);
                }
                else if (c is AssertCmd)
                {
                    result.simpleCmds.Add(new AssertCmd(c.tok, PullOutNonLocalAccessesIntoTemps(result, (c as AssertCmd).Expr)));
                }
                else if (c is AssumeCmd)
                {
                    result.simpleCmds.Add(new AssumeCmd(c.tok, PullOutNonLocalAccessesIntoTemps(result, (c as AssumeCmd).Expr)));
                }
                else
                {
                    Console.WriteLine(c);
                    Debug.Assert(false);
                }
            }

            if (bb.ec is WhileCmd)
            {
                WhileCmd WhileCommand = bb.ec as WhileCmd;
                while (NonLocalAccessCollector.ContainsNonLocalAccess(WhileCommand.Guard, GlobalVariables, TileStaticVariables))
                {
                    AssignCmd assignToTemp;
                    LocalVariable tempDecl;
                    WhileCommand.Guard = ExtractLocalAccessToTemp(WhileCommand.Guard, out assignToTemp, out tempDecl);
                    result.simpleCmds.Add(assignToTemp);
                    KernelImplementation.LocVars.Add(tempDecl);
                }
                result.ec = new WhileCmd(WhileCommand.tok, WhileCommand.Guard, WhileCommand.Invariants, PullOutNonLocalAccesses(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
                while (NonLocalAccessCollector.ContainsNonLocalAccess(IfCommand.Guard, GlobalVariables, TileStaticVariables))
                {
                    AssignCmd assignToTemp;
                    LocalVariable tempDecl;
                    IfCommand.Guard = ExtractLocalAccessToTemp(IfCommand.Guard, out assignToTemp, out tempDecl);
                    result.simpleCmds.Add(assignToTemp);
                    KernelImplementation.LocVars.Add(tempDecl);
                }
                result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, PullOutNonLocalAccesses(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? PullOutNonLocalAccesses(IfCommand.elseBlock) : null);
            }
            else
            {
                Debug.Assert(bb.ec == null);
            }

            return result;

        }

        private Expr PullOutNonLocalAccessesIntoTemps(BigBlock result, Expr e)
        {
            while (NonLocalAccessCollector.ContainsNonLocalAccess(e, GlobalVariables, TileStaticVariables))
            {
                AssignCmd assignToTemp;
                LocalVariable tempDecl;
                e = ExtractLocalAccessToTemp(e, out assignToTemp, out tempDecl);
                result.simpleCmds.Add(assignToTemp);
                KernelImplementation.LocVars.Add(tempDecl);
            }
            return e;
        }

        private Expr ExtractLocalAccessToTemp(Expr rhs, out AssignCmd tempAssignment, out LocalVariable tempDeclaration)
        {
            NonLocalAccessExtractor extractor = new NonLocalAccessExtractor(TempCounter, GlobalVariables, TileStaticVariables);
            TempCounter++;
            rhs = extractor.VisitExpr(rhs);
            tempAssignment = extractor.Assignment;
            tempDeclaration = extractor.Declaration;
            return rhs;
        }

        private void MakeKernelDualised()
        {

            List<Declaration> NewTopLevelDeclarations = new List<Declaration>();

            foreach (Declaration d in Program.TopLevelDeclarations)
            {
                if (d is Procedure)
                {
                    // DuplicateParameters
                    Procedure proc = d as Procedure;
                    proc.InParams = DualiseVariableSequence(proc.InParams);
                    proc.OutParams = DualiseVariableSequence(proc.OutParams);
                    IdentifierExprSeq NewModifies = new IdentifierExprSeq();
                    foreach (IdentifierExpr v in proc.Modifies)
                    {
                        NewModifies.Add(new VariableDualiser(1).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
                    }
                    foreach (IdentifierExpr v in proc.Modifies)
                    {
                        NewModifies.Add(new VariableDualiser(2).VisitIdentifierExpr((IdentifierExpr)v.Clone()));
                    }
                    proc.Modifies = NewModifies;

                    NewTopLevelDeclarations.Add(proc);

                    continue;

                }

                if (d is Implementation)
                {
                    // DuplicateParameters
                    Implementation impl = d as Implementation;
                    impl.InParams = DualiseVariableSequence(impl.InParams);
                    impl.OutParams = DualiseVariableSequence(impl.OutParams);
                    MakeDualLocalVariables(impl);
                    impl.StructuredStmts = MakeDual(impl.StructuredStmts);

                    NewTopLevelDeclarations.Add(impl);

                    continue;

                }

                if (d is Variable && (d as Variable).IsMutable)
                {
                    NewTopLevelDeclarations.Add(new VariableDualiser(1).VisitVariable((Variable)d.Clone()));
                    NewTopLevelDeclarations.Add(new VariableDualiser(2).VisitVariable((Variable)d.Clone()));

                    continue;
                }

                NewTopLevelDeclarations.Add(d);

            }

            Program.TopLevelDeclarations = NewTopLevelDeclarations;

        }

        private static VariableSeq DualiseVariableSequence(VariableSeq seq)
        {
            VariableSeq result = new VariableSeq();
            foreach (Variable v in seq)
            {
                result.Add(new VariableDualiser(1).VisitVariable((Variable)v.Clone()));
            }
            foreach (Variable v in seq)
            {
                result.Add(new VariableDualiser(2).VisitVariable((Variable)v.Clone()));
            }
            return result;
        }

        private void MakeKerenelPredicated()
        {
            foreach (Declaration d in Program.TopLevelDeclarations)
            {
                if (d is Procedure)
                {
                    if (d != KernelProcedure)
                    {
                        // Add predicate to start of parameter list
                        Procedure proc = d as Procedure;
                        VariableSeq NewIns = new VariableSeq();
                        NewIns.Add(new LocalVariable(proc.tok, new TypedIdent(proc.tok, "_P", Microsoft.Boogie.Type.Bool)));
                        foreach (Variable v in proc.InParams)
                        {
                            NewIns.Add(v);
                        }
                        proc.InParams = NewIns;
                    }

                }
                else if (d is Implementation)
                {
                    MakePredicated(d as Implementation, d != KernelImplementation);
                }
            }

        }

        private void MakePredicated(Implementation impl, bool AddPredicateParameter)
        {
            Expr Predicate;

            if (AddPredicateParameter)
            {
                VariableSeq NewIns = new VariableSeq();
                Variable PredicateVariable = new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P", Microsoft.Boogie.Type.Bool));
                NewIns.Add(PredicateVariable);
                foreach (Variable v in impl.InParams)
                {
                    NewIns.Add(v);
                }
                impl.InParams = NewIns;
                Predicate = new IdentifierExpr(impl.tok, PredicateVariable);
            }
            else
            {
                Predicate = Expr.True;
            }

            WhileLoopCounter = 0;
            IfCounter = 0;
            RequiredHavocVariables = new HashSet<Microsoft.Boogie.Type>();
            impl.StructuredStmts = MakePredicated(impl.StructuredStmts, Predicate);
            AddPredicateLocalVariables(impl);
        }

        private StmtList MakeDual(StmtList stmtList)
        {
            Contract.Requires(stmtList != null);

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

            foreach (BigBlock bodyBlock in stmtList.BigBlocks)
            {
                result.BigBlocks.Add(MakeDual(bodyBlock));
            }

            return result;
        }

        private BigBlock MakeDual(BigBlock bb)
        {
            // Not sure what to do about the transfer command

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

            foreach (Cmd c in bb.simpleCmds)
            {
                if (c is CallCmd)
                {
                    CallCmd Call = c as CallCmd;

                    List<Expr> newIns = new List<Expr>();
                    foreach (Expr e in Call.Ins)
                    {
                        newIns.Add(new VariableDualiser(1).VisitExpr(e));
                    }
                    foreach (Expr e in Call.Ins)
                    {
                        newIns.Add(new VariableDualiser(2).VisitExpr(e));
                    }

                    List<IdentifierExpr> newOuts = new List<IdentifierExpr>();
                    foreach (IdentifierExpr ie in Call.Outs)
                    {
                        newOuts.Add(new VariableDualiser(1).VisitIdentifierExpr(ie.Clone() as IdentifierExpr) as IdentifierExpr);
                    }
                    foreach (IdentifierExpr ie in Call.Outs)
                    {
                        newOuts.Add(new VariableDualiser(2).VisitIdentifierExpr(ie.Clone() as IdentifierExpr) as IdentifierExpr);
                    }

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

                    result.simpleCmds.Add(NewCallCmd);
                }
                else if (c is AssignCmd)
                {
                    AssignCmd assign = c as AssignCmd;

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

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

                    newLhss.Add(new VariableDualiser(1).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);
                    newLhss.Add(new VariableDualiser(2).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

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

                    newRhss.Add(new VariableDualiser(1).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));
                    newRhss.Add(new VariableDualiser(2).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

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

                    result.simpleCmds.Add(newAssign);
                }
                else if (c is HavocCmd)
                {
                    HavocCmd havoc = c as HavocCmd;
                    Debug.Assert(havoc.Vars.Length == 1);
                    HavocCmd newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 
                        (IdentifierExpr)(new VariableDualiser(1).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)), 
                        (IdentifierExpr)(new VariableDualiser(2).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))
                    }));
                    result.simpleCmds.Add(newHavoc);
                }
                else if (c is AssertCmd)
                {
                    AssertCmd ass = c as AssertCmd;
                    result.simpleCmds.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr), new VariableDualiser(2).VisitExpr(ass.Expr.Clone() as Expr))));
                }
                else if (c is AssumeCmd)
                {
                    AssumeCmd ass = c as AssumeCmd;
                    result.simpleCmds.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1).VisitExpr(ass.Expr.Clone() as Expr), new VariableDualiser(2).VisitExpr(ass.Expr.Clone() as Expr))));
                }
                else
                {
                    Debug.Assert(false);
                }
            }

            if (bb.ec is WhileCmd)
            {
                result.ec = new WhileCmd(bb.ec.tok, Expr.Or(new VariableDualiser(1).VisitExpr((bb.ec as WhileCmd).Guard), new VariableDualiser(2).VisitExpr((bb.ec as WhileCmd).Guard)), (bb.ec as WhileCmd).Invariants, MakeDual((bb.ec as WhileCmd).Body));
            }
            else
            {
                Debug.Assert(bb.ec == null);
            }

            return result;

        }

        private void MakeDualLocalVariables(Implementation impl)
        {
            VariableSeq NewLocalVars = new VariableSeq();

            foreach (LocalVariable v in impl.LocVars)
            {
                NewLocalVars.Add(new LocalVariable(v.tok, new TypedIdent(v.tok, v.Name + "$1", v.TypedIdent.Type)));
                NewLocalVars.Add(new LocalVariable(v.tok, new TypedIdent(v.tok, v.Name + "$2", v.TypedIdent.Type)));
            }

            impl.LocVars = NewLocalVars;
        }

        private void AddPredicateLocalVariables(Implementation impl)
        {
            for (int i = 0; i < IfCounter; i++)
            {
                impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_P" + i, Microsoft.Boogie.Type.Bool)));
            }
            for (int i = 0; i < WhileLoopCounter; i++)
            {
                impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_LC" + i, Microsoft.Boogie.Type.Bool)));
            }
            foreach (Microsoft.Boogie.Type t in RequiredHavocVariables)
            {
                impl.LocVars.Add(new LocalVariable(impl.tok, new TypedIdent(impl.tok, "_HAVOC_" + t.ToString(), t)));
            }

        }

        private StmtList MakePredicated(StmtList sl, Expr predicate)
        {
            StmtList result = new StmtList(new List<BigBlock>(), sl.EndCurly);

            foreach (BigBlock bodyBlock in sl.BigBlocks)
            {
                List<BigBlock> newBigBlocks = MakePredicated(bodyBlock, predicate);
                foreach (BigBlock newBigBlock in newBigBlocks)
                {
                    result.BigBlocks.Add(newBigBlock);
                }
            }

            return result;

        }

        private List<BigBlock> MakePredicated(BigBlock b, Expr IncomingPredicate)
        {
            // Not sure what to do about the transfer command

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

            BigBlock firstBigBlock = new BigBlock(b.tok, b.LabelName, new CmdSeq(), null, b.tc);
            result.Add(firstBigBlock);

            foreach (Cmd c in b.simpleCmds)
            {
                if (c is CallCmd)
                {

                    CallCmd Call = c as CallCmd;

                    List<Expr> NewIns = new List<Expr>();
                    NewIns.Add(IncomingPredicate);

                    foreach (Expr e in Call.Ins)
                    {
                        NewIns.Add(e);
                    }

                    CallCmd NewCallCmd = new CallCmd(Call.tok, Call.callee, NewIns, Call.Outs);

                    firstBigBlock.simpleCmds.Add(NewCallCmd);
                } 
                else if (IncomingPredicate.Equals(Expr.True))
                {
                    firstBigBlock.simpleCmds.Add(c);
                }
                else if (c is AssignCmd)
                {
                    AssignCmd assign = c as AssignCmd;
                    Debug.Assert(assign.Lhss.Count == 1 && assign.Rhss.Count == 1);

                    ExprSeq iteArgs = new ExprSeq();
                    iteArgs.Add(IncomingPredicate);
                    iteArgs.Add(assign.Rhss.ElementAt(0));
                    iteArgs.Add(assign.Lhss.ElementAt(0).AsExpr);
                    NAryExpr ite = new NAryExpr(assign.tok, new IfThenElse(assign.tok), iteArgs);

                    List<Expr> newRhs = new List<Expr>();
                    newRhs.Add(ite);

                    AssignCmd newAssign = new AssignCmd(assign.tok, assign.Lhss, newRhs);

                    firstBigBlock.simpleCmds.Add(newAssign);
                }
                else if (c is HavocCmd)
                {
                    HavocCmd havoc = c as HavocCmd;
                    Debug.Assert(havoc.Vars.Length == 1);

                    Microsoft.Boogie.Type type = havoc.Vars[0].Decl.TypedIdent.Type;
                    Debug.Assert(type != null);

                    RequiredHavocVariables.Add(type);

                    IdentifierExpr HavocTempExpr = new IdentifierExpr(havoc.tok, new LocalVariable(havoc.tok, new TypedIdent(havoc.tok, "_HAVOC_" + type.ToString(), type)));
                    firstBigBlock.simpleCmds.Add(new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 
                        HavocTempExpr 
                    })));

                    List<AssignLhs> lhss = new List<AssignLhs>();
                    lhss.Add(new SimpleAssignLhs(havoc.tok, havoc.Vars[0]));

                    List<Expr> rhss = new List<Expr>();
                    rhss.Add(new NAryExpr(havoc.tok, new IfThenElse(havoc.tok), new ExprSeq(new Expr[] { IncomingPredicate, HavocTempExpr, havoc.Vars[0] })));

                    firstBigBlock.simpleCmds.Add(new AssignCmd(havoc.tok, lhss, rhss));

                }
                else
                {
                    Debug.Assert(false);
                }
            }

            if (b.ec is WhileCmd)
            {
                string LoopPredicate = "_LC" + WhileLoopCounter;
                WhileLoopCounter++;

                IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, LoopPredicate, Microsoft.Boogie.Type.Bool)));
                Expr GuardExpr = (b.ec as WhileCmd).Guard;

                List<AssignLhs> WhilePredicateLhss = new List<AssignLhs>();
                WhilePredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));

                List<Expr> WhilePredicateRhss = new List<Expr>();
                WhilePredicateRhss.Add(IncomingPredicate.Equals(Expr.True) ? GuardExpr : Expr.And(IncomingPredicate, GuardExpr));

                firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, WhilePredicateRhss));

                WhileCmd NewWhile = new WhileCmd(b.ec.tok, PredicateExpr, (b.ec as WhileCmd).Invariants, MakePredicated((b.ec as WhileCmd).Body, PredicateExpr));

                List<Expr> UpdatePredicateRhss = new List<Expr>();
                UpdatePredicateRhss.Add(Expr.And(PredicateExpr, GuardExpr));

                CmdSeq updateCmd = new CmdSeq();
                updateCmd.Add(new AssignCmd(b.ec.tok, WhilePredicateLhss, UpdatePredicateRhss));

                NewWhile.Body.BigBlocks.Add(new BigBlock(b.ec.tok, "update_" + LoopPredicate, updateCmd, null, null));

                firstBigBlock.ec = NewWhile;

            }
            else if (b.ec is IfCmd)
            {
                IfCmd IfCommand = b.ec as IfCmd;

                string IfPredicate = "_P" + IfCounter;
                IfCounter++;

                IdentifierExpr PredicateExpr = new IdentifierExpr(b.ec.tok, new LocalVariable(b.ec.tok, new TypedIdent(b.ec.tok, IfPredicate, Microsoft.Boogie.Type.Bool)));
                Expr GuardExpr = IfCommand.Guard;

                List<AssignLhs> IfPredicateLhss = new List<AssignLhs>();
                IfPredicateLhss.Add(new SimpleAssignLhs(b.ec.tok, PredicateExpr));

                List<Expr> IfPredicateRhss = new List<Expr>();
                IfPredicateRhss.Add(GuardExpr);

                firstBigBlock.simpleCmds.Add(new AssignCmd(b.ec.tok, IfPredicateLhss, IfPredicateRhss));

                Debug.Assert(IfCommand.elseIf == null); // We need to preprocess these away

                StmtList PredicatedThen = MakePredicated(IfCommand.thn, Expr.And(IncomingPredicate, PredicateExpr));

                foreach (BigBlock bb in PredicatedThen.BigBlocks)
                {
                    result.Add(bb);
                }

                if (IfCommand.elseBlock != null)
                {
                    StmtList PredicatedElse = MakePredicated(IfCommand.elseBlock, Expr.And(IncomingPredicate, Expr.Not(PredicateExpr)));

                    foreach (BigBlock bb in PredicatedElse.BigBlocks)
                    {
                        result.Add(bb);
                    }
                }




            }
            else
            {
                Debug.Assert(b.ec == null);
            }

            return result;
        }

        override protected void CheckKernelParameters()
        {
            if (KernelProcedure.InParams.Length != 0)
            {
                Error(KernelProcedure.tok, "Kernel should not take any parameters");
            }
            if (KernelProcedure.OutParams.Length != 0)
            {
                Error(KernelProcedure.tok, "Kernel should not take return anything");
            }
        }


        override internal int Check()
        {
            base.Check();

            if (!HasId("X"))
            {
                Error(KernelProcedure.tok, "Kernel must declare local variable '_X'");
            }

            if (!HasTileSize("X"))
            {
                Error(KernelProcedure.tok, "Kernel must declare global constant 'TILE_SIZE_X'");
            }

            if (!HasNumTiles("X"))
            {
                Error(KernelProcedure.tok, "Kernel must declare global constant 'NUM_TILES_X'");
            }

            if (!HasTileId("X"))
            {
                Error(KernelProcedure.tok, "Kernel must declare global constant '_tile_X'");
            }

            if (HasId("Y") || HasTileSize("Y") || HasNumTiles("Y") || HasTileId("Y"))
            {
                if (!HasId("Y"))
                {
                    Error(KernelProcedure.tok, "2D kernel must declare local variable '_Y'");
                }

                if (!HasTileSize("Y"))
                {
                    Error(KernelProcedure.tok, "2D kernel must declare global constant 'TILE_SIZE_Y'");
                }

                if (!HasNumTiles("Y"))
                {
                    Error(KernelProcedure.tok, "2D kernel must declare global constant 'NUM_TILES_Y'");
                }

                if (!HasTileId("Y"))
                {
                    Error(KernelProcedure.tok, "2D kernel must declare global constant '_tile_Y'");
                }
            }

            if (HasId("Z") || HasTileSize("Z") || HasNumTiles("Z") || HasTileId("Z"))
            {
                if (!HasId("Y"))
                {
                    Error(KernelProcedure.tok, "3D kernel must declare local variable '_Y'");
                }

                if (!HasTileSize("Y"))
                {
                    Error(KernelProcedure.tok, "3D kernel must declare global constant 'TILE_SIZE_Y'");
                }

                if (!HasNumTiles("Y"))
                {
                    Error(KernelProcedure.tok, "3D kernel must declare global constant 'NUM_TILES_Y'");
                }

                if (!HasTileId("Y"))
                {
                    Error(KernelProcedure.tok, "3D kernel must declare global constant '_tile_Y'");
                }

                if (!HasId("Z"))
                {
                    Error(KernelProcedure.tok, "3D kernel must declare local variable '_Z'");
                }

                if (!HasTileSize("Z"))
                {
                    Error(KernelProcedure.tok, "3D kernel must declare global constant 'TILE_SIZE_Z'");
                }

                if (!HasNumTiles("Z"))
                {
                    Error(KernelProcedure.tok, "3D kernel must declare global constant 'NUM_TILES_Z'");
                }

                if (!HasTileId("Z"))
                {
                    Error(KernelProcedure.tok, "3D kernel must declare global constant '_tile_Z'");
                }
            }


            if (HasId("Z") && (!HasId("X") || !HasId("Y")))
            {
                Error(KernelProcedure.tok, "Kernel with local variable '_Z' must also have local variables '_X' and '_Y'");
            }

            return ErrorCount;
        }

        private bool HasNamedConstant(string dimension, string Name)
        {
            foreach (Declaration d in Program.TopLevelDeclarations)
            {
                if (d is Variable && (d as Variable).Name.Equals(Name + dimension))
                {
                    Variable v = d as Variable;
                    if (v is Constant && IsIntOrBv32(v.TypedIdent.Type))
                    {
                        return true;
                    }
                    else
                    {
                        Error(v.tok, "Declaration '" + Name + dimension + "' must be a constant integer");
                    }
                }
            }
            return false;
        }

        private bool HasTileId(string dimension)
        {
            return HasNamedConstant(dimension, "_tile_");
        }

        private bool HasNumTiles(string dimension)
        {
            return HasNamedConstant(dimension, "NUM_TILES_");
        }

        private bool HasTileSize(string dimension)
        {
            return HasNamedConstant(dimension, "TILE_SIZE_");
        }

    }



}