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

namespace GPUVerify
{
    class RaceInstrumenter : IRaceInstrumenter
    {
        protected GPUVerifier verifier;

        public INonLocalState NonLocalStateToCheck;

        public int onlyLog1;
        public int onlyLog2;
        public bool failedToFindSecondAccess;
        public bool addedLogWrite;
        private int logAddCount;

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

        public RaceInstrumenter()
        {
            onlyLog1 = -1;
            onlyLog2 = -1;
            failedToFindSecondAccess = false;
            addedLogWrite = false;
            logAddCount = 0;
        }

        public void setVerifier(GPUVerifier verifier)
        {
            this.verifier = verifier;
            NonLocalStateToCheck = new NonLocalStateLists();
            foreach(Variable v in verifier.NonLocalState.getGlobalVariables())
            {
                NonLocalStateToCheck.getGlobalVariables().Add(v);
            }
            foreach(Variable v in verifier.NonLocalState.getGroupSharedVariables())
            {
                NonLocalStateToCheck.getGroupSharedVariables().Add(v);
            }
        }

        private void AddNoReadOrWriteCandidateInvariants(IRegion region, Variable v)
        {
            // Reasoning: if READ_HAS_OCCURRED_v is not in the modifies set for the
            // loop then there is no point adding an invariant
            //
            // If READ_HAS_OCCURRED_v is in the modifies set, but the loop does not
            // contain a barrier, then it is almost certain that a read CAN be
            // pending at the loop head, so the invariant will not hold
            //
            // If there is a barrier in the loop body then READ_HAS_OCCURRED_v will
            // be in the modifies set, but there may not be a live read at the loop
            // head, so it is worth adding the loop invariant candidate.
            //
            // The same reasoning applies for WRITE

            if (verifier.ContainsBarrierCall(region))
            {
                if (verifier.ContainsNamedVariable(
                    LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ")))
                {
                    AddNoReadOrWriteCandidateInvariant(region, v, "READ");
                }

                if (verifier.ContainsNamedVariable(
                    LoopInvariantGenerator.GetModifiedVariables(region), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE")))
                {
                    AddNoReadOrWriteCandidateInvariant(region, v, "WRITE");
                }
            }
        }

        private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v)
        {
            AddNoReadOrWriteCandidateRequires(Proc, v, "READ", "1");
            AddNoReadOrWriteCandidateRequires(Proc, v, "WRITE", "1");
        }

        private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v)
        {
            AddNoReadOrWriteCandidateEnsures(Proc, v, "READ", "1");
            AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "1");
        }

        private void AddNoReadOrWriteCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)
        {
            Expr candidate = NoReadOrWriteExpr(v, ReadOrWrite, "1");
            verifier.AddCandidateInvariant(region, candidate, "no " + ReadOrWrite.ToLower());
        }

        public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region)
        {
            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
            {
                AddNoReadOrWriteCandidateInvariants(region, v);
                AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "READ");
                AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "WRITE");
                AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "READ", CollectOffsetPredicates(impl, region, v, "READ"));
                AddOffsetsSatisfyPredicatesCandidateInvariant(region, v, "WRITE", CollectOffsetPredicates(impl, region, v, "WRITE"));
            }
        }

        private void AddAccessRelatedCandidateInvariant(IRegion region, string accessKind, Expr candidateInvariantExpr, string procName, string tag)
        {
            Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);
            verifier.AddCandidateInvariant(region, candidate, tag);
        }

        private bool DoesNotReferTo(Expr expr, string v)
        {
            FindReferencesToNamedVariableVisitor visitor = new FindReferencesToNamedVariableVisitor(v);
            visitor.VisitExpr(expr);
            return !visitor.found;
        }

        private List<Expr> CollectOffsetPredicates(Implementation impl, IRegion region, Variable v, string accessType)
        {
            var offsetVar = new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, accessType));
            var offsetExpr = new IdentifierExpr(Token.NoToken, offsetVar);
            var offsetPreds = new List<Expr>();

            foreach (var offset in GetOffsetsAccessed(region, v, accessType))
            {
                bool isConstant;
                var def = verifier.varDefAnalyses[impl].SubstDefinitions(offset, impl.Name, out isConstant);
                if (def == null)
                    continue;

                if (isConstant)
                {
                    offsetPreds.Add(Expr.Eq(offsetExpr, def));
                }
                else
                {
                    var sc = StrideConstraint.FromExpr(verifier, impl, def);
                    var pred = sc.MaybeBuildPredicate(verifier, offsetExpr);
                    if (pred != null)
                        offsetPreds.Add(pred);
                }
            }

            return offsetPreds;
        }

        private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType)
        {
            KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(region.Guard());
            if (iLessThanC.Key != null)
            {
                foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
                {
                    if(HasFormIPlusLocalIdTimesC(e, iLessThanC, impl))
                    {
                        AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(region, v, iLessThanC.Value, accessType);
                        break;
                    }
                }

                foreach (Expr e in GetOffsetsAccessed(region, v, accessType))
                {
                    if (HasFormIPlusGlobalIdTimesC(e, iLessThanC, impl))
                    {
                        AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(region, v, iLessThanC.Value, accessType);
                        break;
                    }
                }
            
            }

        
        }

        private bool HasFormIPlusLocalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl)
        {
            if (!(e is NAryExpr))
            {
                return false;
            }

            NAryExpr nary = e as NAryExpr;

            if (!nary.Fun.FunctionName.Equals("BV32_ADD"))
            {
                return false;
            }

            return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&
                IsLocalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||
                (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&
                IsLocalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));
        }

        private bool IsLocalIdTimesConstant(Expr maybeLocalIdTimesConstant, Expr constant, Implementation impl)
        {
            if (!(maybeLocalIdTimesConstant is NAryExpr))
            {
                return false;
            }
            NAryExpr nary = maybeLocalIdTimesConstant as NAryExpr;
            if(!nary.Fun.FunctionName.Equals("BV32_MUL"))
            {
                return false;
            }

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


        private bool HasFormIPlusGlobalIdTimesC(Expr e, KeyValuePair<IdentifierExpr, Expr> iLessThanC, Implementation impl)
        {
            if (!(e is NAryExpr))
            {
                return false;
            }

            NAryExpr nary = e as NAryExpr;

            if (!nary.Fun.FunctionName.Equals("BV32_ADD"))
            {
                return false;
            }

            return (SameIdentifierExpression(nary.Args[0], iLessThanC.Key) &&
                IsGlobalIdTimesConstant(nary.Args[1], iLessThanC.Value, impl)) ||
                (SameIdentifierExpression(nary.Args[1], iLessThanC.Key) &&
                IsGlobalIdTimesConstant(nary.Args[0], iLessThanC.Value, impl));
        }

        private bool IsGlobalIdTimesConstant(Expr maybeGlobalIdTimesConstant, Expr constant, Implementation impl)
        {
            if (!(maybeGlobalIdTimesConstant is NAryExpr))
            {
                return false;
            }
            NAryExpr nary = maybeGlobalIdTimesConstant as NAryExpr;
            if (!nary.Fun.FunctionName.Equals("BV32_MUL"))
            {
                return false;
            }

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


        private bool SameConstant(Expr expr, Expr constant)
        {
            if (constant is IdentifierExpr)
            {
                IdentifierExpr identifierExpr = constant as IdentifierExpr;
                Debug.Assert(identifierExpr.Decl is Constant);
                return expr is IdentifierExpr && (expr as IdentifierExpr).Decl is Constant && (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Decl.Name);
            }
            else
            {
                Debug.Assert(constant is LiteralExpr);
                LiteralExpr literalExpr = constant as LiteralExpr;
                if (!(expr is LiteralExpr))
                {
                    return false;
                }
                if (!(literalExpr.Val is BvConst) || !((expr as LiteralExpr).Val is BvConst))
                {
                    return false;
                }

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

        private bool SameIdentifierExpression(Expr expr, IdentifierExpr identifierExpr)
        {
            if (!(expr is IdentifierExpr))
            {
                return false;
            }
            return (expr as IdentifierExpr).Decl.Name.Equals(identifierExpr.Name);
        }

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

            if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("bv32_to_bool"))
            {
                expr = (expr as NAryExpr).Args[0];
            }

            if (!(expr is NAryExpr))
            {
                return new KeyValuePair<IdentifierExpr, Expr>(null, null);
            }

            NAryExpr nary = expr as NAryExpr;

            if (!(nary.Fun.FunctionName.Equals("BV32_C_LT") || nary.Fun.FunctionName.Equals("BV32_LT")))
            {
                return new KeyValuePair<IdentifierExpr, Expr>(null, null);
            }

            if (!(nary.Args[0] is IdentifierExpr))
            {
                return new KeyValuePair<IdentifierExpr, Expr>(null, null);
            }

            if (!IsConstant(nary.Args[1]))
            {
                return new KeyValuePair<IdentifierExpr, Expr>(null, null);
            }

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

        }

        private static bool IsConstant(Expr e)
        {
            return ((e is IdentifierExpr && (e as IdentifierExpr).Decl is Constant) || e is LiteralExpr);
        }

        private void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v)
        {
            AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 1);
            AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 1);
        }

        private void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v)
        {
            AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "WRITE", 1);
            AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);
        }

        public void AddKernelPrecondition()
        {
            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
            {
                AddRequiresNoPendingAccess(v);

                if (!verifier.ArrayModelledAdversarially(v))
                {
                    IdentifierExpr v1 = new IdentifierExpr(Token.NoToken, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable));
                    IdentifierExpr v2 = new IdentifierExpr(Token.NoToken, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable));
                    verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.Eq(v1, v2)));
                }
            }
        }

        public bool AddRaceCheckingInstrumentation()
        {

            if (onlyLog1 != -1)
            {
                addedLogWrite = false;
                failedToFindSecondAccess = true;
            }
            else
            {
                addedLogWrite = true;
                failedToFindSecondAccess = false;
            }

            foreach (Declaration d in verifier.Program.TopLevelDeclarations)
            {
                if (d is Implementation)
                {
                    AddRaceCheckCalls(d as Implementation);
                }
            }

            if (failedToFindSecondAccess || !addedLogWrite)
                return false;

            return true;

        }

        private void AddRaceCheckingDecsAndProcsForVar(Variable v)
        {
            AddLogRaceDeclarations(v, "READ");
            AddLogRaceDeclarations(v, "WRITE");
            AddLogAccessProcedure(v, "READ");
            AddLogAccessProcedure(v, "WRITE");

        }
        
        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 Block AddRaceCheckCalls(Block b)
        {
            b.Cmds = AddRaceCheckCalls(b.Cmds);
            return b;
        }

        private void AddRaceCheckCalls(Implementation impl)
        {
            if (CommandLineOptions.Unstructured)
                impl.Blocks = impl.Blocks.Select(AddRaceCheckCalls).ToList();
            else
                impl.StructuredStmts = AddRaceCheckCalls(impl.StructuredStmts);
        }

        private bool shouldAddLogCallAndIncr()
        {
            Contract.Assert(onlyLog1 >= -1);
            int oldLogAddCount = logAddCount;
            ++logAddCount;

            if (onlyLog1 == -1)
            {
                return true;
            }

            if(onlyLog1 + onlyLog2 == oldLogAddCount)
            {
                failedToFindSecondAccess = false;
                return true;
            }

            if (onlyLog1 == oldLogAddCount)
            {
                return true;
            }

            return false;
        }

        private CmdSeq AddRaceCheckCalls(CmdSeq cs)
        {
            var result = new CmdSeq();
            foreach (Cmd c in cs)
            {
                result.Add(c);
                if (c is AssignCmd)
                {
                    AssignCmd assign = c as AssignCmd;

                    ReadCollector rc = new ReadCollector(NonLocalStateToCheck);
                    foreach (var rhs in assign.Rhss)
                        rc.Visit(rhs);
                    if (rc.accesses.Count > 0)
                    {
                        foreach (AccessRecord ar in rc.accesses)
                        {
                            if (shouldAddLogCallAndIncr())
                            {

                                ExprSeq inParams = new ExprSeq();
                                if (ar.IndexZ != null)
                                {
                                    inParams.Add(ar.IndexZ);
                                }
                                if (ar.IndexY != null)
                                {
                                    inParams.Add(ar.IndexY);
                                }
                                if (ar.IndexX != null)
                                {
                                    inParams.Add(ar.IndexX);
                                }

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

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

                                logAccessCallCmd.Proc = logProcedure;

                                result.Add(logAccessCallCmd);

                            }
                        }
                    }

                    foreach (var lhs in assign.Lhss)
                    {
                        WriteCollector wc = new WriteCollector(NonLocalStateToCheck);
                        wc.Visit(lhs);
                        if (wc.GetAccess() != null)
                        {
                            AccessRecord ar = wc.GetAccess();

                            if (shouldAddLogCallAndIncr())
                            {

                                ExprSeq inParams = new ExprSeq();
                                if (ar.IndexZ != null)
                                {
                                    inParams.Add(ar.IndexZ);
                                }
                                if (ar.IndexY != null)
                                {
                                    inParams.Add(ar.IndexY);
                                }
                                if (ar.IndexX != null)
                                {
                                    inParams.Add(ar.IndexX);
                                }

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

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

                                logAccessCallCmd.Proc = logProcedure;

                                result.Add(logAccessCallCmd);

                                addedLogWrite = true;

                            }
                        }
                    }
                }
            }
            return result;
        }

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

            if (bb.ec is WhileCmd)
            {
                WhileCmd WhileCommand = bb.ec as WhileCmd;
                result.ec = new WhileCmd(WhileCommand.tok, WhileCommand.Guard, 
                        WhileCommand.Invariants, AddRaceCheckCalls(WhileCommand.Body));
            }
            else if (bb.ec is IfCmd)
            {
                IfCmd IfCommand = bb.ec as IfCmd;
                Debug.Assert(IfCommand.elseIf == null); // We don't handle else if yet
                result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, AddRaceCheckCalls(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? AddRaceCheckCalls(IfCommand.elseBlock) : null);
            }
            else if (bb.ec is BreakCmd)
            {
                result.ec = bb.ec;
            }
            else
            {
                Debug.Assert(bb.ec == null);
            }

            return result;
        }

        private Procedure GetLogAccessProcedure(IToken tok, string name)
        {
            if (logAccessProcedures.ContainsKey(name))
            {
                return logAccessProcedures[name];
            }
            Procedure newProcedure = new Procedure(tok, name, new TypeVariableSeq(), new VariableSeq(), new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq());
            logAccessProcedures[name] = newProcedure;
            return newProcedure;
        }


        public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread)
        {
            BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null);
            if (Thread == 2)
            {
                return result;
            }

            Expr ResetReadAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
                new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))));
            Expr ResetWriteAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken,
                new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))));

            if (CommandLineOptions.InterGroupRaceChecking && verifier.NonLocalState.getGlobalVariables().Contains(v))
            {
                ResetReadAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetReadAssumeGuard);
                ResetWriteAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);
            }

            result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetReadAssumeGuard));
            result.simpleCmds.Add(new AssumeCmd(Token.NoToken, ResetWriteAssumeGuard));
            return result;
        }

        protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite)
        {
            VariableSeq inParams = new VariableSeq();

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

            Debug.Assert(v.TypedIdent.Type is MapType);
            MapType mt = v.TypedIdent.Type as MapType;
            Debug.Assert(mt.Arguments.Length == 1);
            Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));
            Debug.Assert(!(mt.Result is MapType));

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

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

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

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

            result.InParams = inParams;

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

            return result;
        }

        public void AddRaceCheckingCandidateRequires(Procedure Proc)
        {
            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
            {
                AddNoReadOrWriteCandidateRequires(Proc, v);
                AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);
            }
        }

        public void AddRaceCheckingCandidateEnsures(Procedure Proc)
        {
            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
            {
                AddNoReadOrWriteCandidateEnsures(Proc, v);
                AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);
            }
        }

        private void AddNoReadOrWriteCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
        {
            verifier.AddCandidateRequires(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
        }

        private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, string OneOrTwo)
        {
            verifier.AddCandidateEnsures(Proc, NoReadOrWriteExpr(v, ReadOrWrite, OneOrTwo));
        }

        private HashSet<Expr> GetOffsetsAccessed(IRegion region, Variable v, string AccessType)
        {
            HashSet<Expr> result = new HashSet<Expr>();

            foreach (Cmd c in region.Cmds())
            {
                if (c is CallCmd)
                {
                    CallCmd call = c as CallCmd;

                    if (call.callee == "_LOG_" + AccessType + "_" + v.Name)
                    {
                        // Ins[0] is thread 1's predicate,
                        // Ins[1] is the offset to be read
                        // If Ins[1] has the form BV32_ADD(offset#construct...(P), offset),
                        // we are looking for the second parameter to this BV32_ADD
                        Expr offset = call.Ins[1];
                        if (offset is NAryExpr)
                        {
                            var nExpr = (NAryExpr)offset;
                            if (nExpr.Fun.FunctionName == "BV32_ADD" &&
                                nExpr.Args[0] is NAryExpr)
                            {
                                var n0Expr = (NAryExpr)nExpr.Args[0];
                                if (n0Expr.Fun.FunctionName.StartsWith("offset#"))
                                    offset = nExpr.Args[1];
                            }
                        }
                        result.Add(offset);
                    }

                }

            }

            return result;
        }

        public void AddRaceCheckingDeclarations()
        {
            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())
            {
                AddRaceCheckingDecsAndProcsForVar(v);
            }
        }

        protected void AddLogAccessProcedure(Variable v, string Access)
        {
            Procedure LogAccessProcedure = MakeLogAccessProcedureHeader(v, Access);

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

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

            Debug.Assert(v.TypedIdent.Type is MapType);
            MapType mt = v.TypedIdent.Type as MapType;
            Debug.Assert(mt.Arguments.Length == 1);
            Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));
            Debug.Assert(!(mt.Result is MapType));

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

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

            CmdSeq simpleCmds = new CmdSeq();

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

            simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessHasOccurredVariable), 
                Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), Expr.True));
            simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessOffsetXVariable), 
                Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), 
                new IdentifierExpr(v.tok, VariableForThread(1, OffsetParameter))));

            if (Access.Equals("READ"))
            {
                // Check read by thread 2 does not conflict with write by thread 1
                Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");
                Variable WriteOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "WRITE");
                Expr WriteReadGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
                WriteReadGuard = Expr.And(WriteReadGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));
                WriteReadGuard = Expr.And(WriteReadGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)), 
                                                new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
                if (!verifier.ArrayModelledAdversarially(v))
                {
                    WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(
                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)), 1, "WRITE"),
                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
                        ));
                }

                if (verifier.NonLocalState.getGroupSharedVariables().Contains(v) && CommandLineOptions.InterGroupRaceChecking)
                {
                    WriteReadGuard = Expr.And(WriteReadGuard, verifier.ThreadsInSameGroup());
                }

                WriteReadGuard = Expr.Not(WriteReadGuard);
                simpleCmds.Add(new AssertCmd(Token.NoToken, WriteReadGuard));
            }
            else
            {
                Debug.Assert(Access.Equals("WRITE"));

                // Check write by thread 2 does not conflict with write by thread 1
                Variable WriteHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE");
                Variable WriteOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "WRITE");

                Expr WriteWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
                WriteWriteGuard = Expr.And(WriteWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));
                WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)),
                                                new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
                if (!verifier.ArrayModelledAdversarially(v))
                {
                    WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(
                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)), 1, "WRITE"),
                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")
                        ));
                }

                if (verifier.NonLocalState.getGroupSharedVariables().Contains(v) && CommandLineOptions.InterGroupRaceChecking)
                {
                    WriteWriteGuard = Expr.And(WriteWriteGuard, verifier.ThreadsInSameGroup());
                }

                WriteWriteGuard = Expr.Not(WriteWriteGuard);
                simpleCmds.Add(new AssertCmd(Token.NoToken, WriteWriteGuard));

                // Check write by thread 2 does not conflict with read by thread 1
                Variable ReadHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ");
                Variable ReadOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "READ");

                Expr ReadWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));
                ReadWriteGuard = Expr.And(ReadWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadHasOccurredVariable)));
                ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetXVariable)),
                                                new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));
                if (!verifier.ArrayModelledAdversarially(v))
                {
                    ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(
                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetXVariable)), 1, "WRITE"),
                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")
                        ));
                }

                if (verifier.NonLocalState.getGroupSharedVariables().Contains(v) && CommandLineOptions.InterGroupRaceChecking)
                {
                    ReadWriteGuard = Expr.And(ReadWriteGuard, verifier.ThreadsInSameGroup());
                }

                ReadWriteGuard = Expr.Not(ReadWriteGuard);
                simpleCmds.Add(new AssertCmd(Token.NoToken, ReadWriteGuard));

            }

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

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

            Implementation LogAccessImplementation = new Implementation(v.tok, "_LOG_" + Access + "_" + v.Name, new TypeVariableSeq(), LogAccessProcedure.InParams, new VariableSeq(), locals, new StmtList(bigblocks, v.tok));
            LogAccessImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

            LogAccessImplementation.Proc = LogAccessProcedure;

            verifier.Program.TopLevelDeclarations.Add(LogAccessProcedure);
            verifier.Program.TopLevelDeclarations.Add(LogAccessImplementation);
        }

        private Variable VariableForThread(int thread, Variable v)
        {
            return new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable);
        }

        protected void AddLogRaceDeclarations(Variable v, String ReadOrWrite)
        {
            Variable AccessHasOccurred = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);

            // Assumes full symmetry reduction

            verifier.Program.TopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable(AccessHasOccurred.Clone() as Variable));

            Debug.Assert(v.TypedIdent.Type is MapType);
            MapType mt = v.TypedIdent.Type as MapType;
            Debug.Assert(mt.Arguments.Length == 1);

            Variable AccessOffsetX = GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite);
            verifier.Program.TopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable(AccessOffsetX.Clone() as Variable));

        }
        

        private static AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs)
        {
            List<AssignLhs> lhss = new List<AssignLhs>();
            List<Expr> rhss = new List<Expr>();
            lhss.Add(new SimpleAssignLhs(lhs.tok, new IdentifierExpr(lhs.tok, lhs)));
            rhss.Add(new NAryExpr(rhs.tok, new IfThenElse(rhs.tok), new ExprSeq(new Expr[] { condition, rhs, new IdentifierExpr(lhs.tok, lhs) })));
            return new AssignCmd(lhs.tok, lhss, rhss);
        }

        private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, int Thread, string AccessType)
        {
            Expr result = new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(v.Clone() as Variable));
            Debug.Assert(v.TypedIdent.Type is MapType);
            MapType mt = v.TypedIdent.Type as MapType;
            Debug.Assert(mt.Arguments.Length == 1);

            result = Expr.Select(result,
                new Expr[] { offsetExpr });
            Debug.Assert(!(mt.Result is MapType));
            return result;
        }

        protected void AddRequiresNoPendingAccess(Variable v)
        {
            IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")));
            IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")));

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

        protected Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo)
        {
            Variable ReadOrWriteHasOccurred = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite);
            ReadOrWriteHasOccurred.Name = ReadOrWriteHasOccurred.Name + "$" + OneOrTwo;
            ReadOrWriteHasOccurred.TypedIdent.Name = ReadOrWriteHasOccurred.TypedIdent.Name + "$" + OneOrTwo;
            Expr expr = Expr.Not(new IdentifierExpr(v.tok, ReadOrWriteHasOccurred));
            return expr;
        }


        protected void AddOffsetsSatisfyPredicatesCandidateInvariant(IRegion region, Variable v, string ReadOrWrite, List<Expr> preds)
        {
            if (preds.Count != 0)
            {
                Expr expr = AccessedOffsetsSatisfyPredicatesExpr(v, preds, ReadOrWrite, 1);
                verifier.AddCandidateInvariant(region, expr, "accessed offsets satisfy predicates");
            }
        }

        private Expr AccessedOffsetsSatisfyPredicatesExpr(Variable v, IEnumerable<Expr> offsets, string ReadOrWrite, int Thread) {
            return Expr.Imp(
                    new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
                    offsets.Aggregate(Expr.Or));
        }

        private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread)
        {
            Expr expr = null;
            if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))
            {
                expr = Expr.Imp(
                        new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
                        Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));
            }
            return expr;
        }

        private Expr AccessedOffsetIsThreadGlobalIdExpr(Variable v, string ReadOrWrite, int Thread)
        {
            Expr expr = null;
            if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))
            {
                expr = Expr.Imp(
                        new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),
                        Expr.Eq(
                            new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))),
                            GlobalIdExpr("X", Thread)
                            )
                            );
            }
            return expr;
        }

        private Expr GlobalIdExpr(string dimension, int Thread)
        {
            return new VariableDualiser(Thread, null, null).VisitExpr(verifier.GlobalIdExpr(dimension).Clone() as Expr);
        }

        protected void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)
        {
            Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);
            verifier.AddCandidateInvariant(region,
                expr, "accessed offset in range [ C*local_id, (C+1)*local_id )");
        }

        private Expr MakeCTimesLocalIdRangeExpression(Variable v, Expr constant, string ReadOrWrite, int Thread)
        {
            Expr CTimesLocalId = verifier.MakeBVMul(constant.Clone() as Expr, 
                new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread)));

            Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
                new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr);

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

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

            return Expr.Imp(
                    AccessHasOccurred(v, ReadOrWrite, Thread),
                    Expr.And(CTimesLocalIdLeqAccessedOffset, AccessedOffsetLtCTimesLocalIdPlusC));
        }

        private static IdentifierExpr AccessHasOccurred(Variable v, string ReadOrWrite, int Thread)
        {
            return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite)));
        }

        private static IdentifierExpr OffsetXExpr(Variable v, string ReadOrWrite, int Thread)
        {
            return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite)));
        }

        protected void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)
        {
            Expr expr = MakeCTimesGloalIdRangeExpr(v, constant, ReadOrWrite, 1);
            verifier.AddCandidateInvariant(region,
                expr, "accessed offset in range [ C*global_id, (C+1)*global_id )");
        }

        private Expr MakeCTimesGloalIdRangeExpr(Variable v, Expr constant, string ReadOrWrite, int Thread)
        {
            Expr CTimesGlobalId = verifier.MakeBVMul(constant.Clone() as Expr,
                GlobalIdExpr("X", Thread));

            Expr CTimesGlobalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr,
                GlobalIdExpr("X", Thread)), constant.Clone() as Expr);

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

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

            Expr implication = Expr.Imp(
                    AccessHasOccurred(v, ReadOrWrite, Thread),
                    Expr.And(CTimesGlobalIdLeqAccessedOffset, AccessedOffsetLtCTimesGlobalIdPlusC));
            return implication;
        }

        protected void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
        {
            Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);
            if (expr != null)
            {
                verifier.AddCandidateRequires(Proc, expr);
            }
        }

        protected void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread)
        {
            Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, Thread);
            if (expr != null)
            {
                verifier.AddCandidateEnsures(Proc, expr);
            }
        }



    }



    class FindReferencesToNamedVariableVisitor : StandardVisitor
    {
        internal bool found = false;
        private string name;

        internal FindReferencesToNamedVariableVisitor(string name)
        {
            this.name = name;
        }

        public override Variable VisitVariable(Variable node)
        {
            if (GPUVerifier.StripThreadIdentifier(node.Name).Equals(name))
            {
                found = true;
            }
            return base.VisitVariable(node);
        }
    }



}