Reinstate GPUVerify files

author: Peter Collingbourne <peter@pcc.me.uk> 2012-07-02 20:36:17 +0100
committer: Peter Collingbourne <peter@pcc.me.uk> 2012-07-02 20:36:17 +0100
commit: 8505b37ece6701ac653e8fb856a78eaafefce577 (patch)
tree: 7d15426b5f0a74415f6d09318873b900a9afdad9 /Source
parent: a45579e46cf7ac3940f7cf50319c4dfb1231e993 (diff)
3 files changed, 1349 insertions, 0 deletions
diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
new file mode 100644
index 00000000..620f7d1a
--- /dev/null
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -0,0 +1,1042 @@
+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);
+        }
+    }
+
+
+
+}
diff --git a/Source/GPUVerify/ReducedStrengthAnalysis.cs b/Source/GPUVerify/ReducedStrengthAnalysis.cs
new file mode 100644
index 00000000..0e58ff7d
--- /dev/null
+++ b/Source/GPUVerify/ReducedStrengthAnalysis.cs
@@ -0,0 +1,166 @@
+using Microsoft.Boogie;
+using System;
+using System.Collections.Generic;
+using System.Linq;
+
+namespace GPUVerify {
+
+class ReducedStrengthAnalysis {
+
+  GPUVerifier verifier;
+  Implementation impl;
+  VariableDefinitionAnalysis varDefs;
+
+  Dictionary<Variable, List<Tuple<object, Expr>>> multiDefMap = new Dictionary<Variable, List<Tuple<object, Expr>>>();
+  Dictionary<string, ModStrideConstraint> strideConstraintMap = new Dictionary<string, ModStrideConstraint>();
+  Dictionary<object, List<string>> loopCounterMap = new Dictionary<object, List<string>>();
+
+  ReducedStrengthAnalysis(GPUVerifier v, Implementation i) {
+    verifier = v;
+    impl = i;
+    varDefs = verifier.varDefAnalyses[impl];
+  }
+
+  void AddAssignment(object regionId, AssignLhs lhs, Expr rhs) {
+    if (lhs is SimpleAssignLhs) {
+      var sLhs = (SimpleAssignLhs)lhs;
+      var theVar = sLhs.DeepAssignedVariable;
+      List<Tuple<object, Expr>> defs;
+      if (multiDefMap.ContainsKey(theVar))
+        defs = multiDefMap[theVar];
+      else
+        defs = multiDefMap[theVar] = new List<Tuple<object, Expr>>();
+      defs.Add(new Tuple<object, Expr>(regionId, rhs));
+    }
+  }
+
+  void AnalyseRegion(IRegion region) {
+    foreach (var c in region.CmdsChildRegions()) {
+      var ac = c as AssignCmd;
+      if (ac != null) {
+        foreach (var a in ac.Lhss.Zip(ac.Rhss)) {
+          AddAssignment(region.Identifier(), a.Item1, a.Item2);
+        }
+      }
+      var child = c as IRegion;
+      if (child != null)
+        AnalyseRegion(child);
+    }
+  }
+
+  void Analyse() {
+    AnalyseRegion(verifier.RootRegion(impl));
+    foreach (var v in multiDefMap.Keys) {
+      var defs = multiDefMap[v];
+      if (defs.Count != 2)
+        continue;
+      bool def0IsConst, def1IsConst;
+      var def0 = varDefs.SubstDefinitions(defs[0].Item2, impl.Name, out def0IsConst);
+      var def1 = varDefs.SubstDefinitions(defs[1].Item2, impl.Name, out def1IsConst);
+      if (def0IsConst && !def1IsConst) {
+        AddDefinitionPair(v, def0, def1, defs[1].Item1);
+      } else if (!def0IsConst && def1IsConst) {
+        AddDefinitionPair(v, def1, def0, defs[0].Item1);
+      }
+    }
+    multiDefMap = null;
+  }
+
+  private class StrideForm {
+    public StrideForm(Kind kind) { this.kind = kind; this.op = null; }
+    public StrideForm(Kind kind, Expr op) { this.kind = kind; this.op = op; }
+    public enum Kind { Bottom, Identity, Constant, Product, PowerMul, PowerDiv };
+    public Kind kind;
+    public Expr op;
+  }
+
+  private StrideForm ComputeStrideForm(Variable v, Expr e) {
+    Expr lhs, rhs;
+
+    if (e is LiteralExpr)
+      return new StrideForm(StrideForm.Kind.Constant, e);
+
+    var ie = e as IdentifierExpr;
+    if (ie != null) {
+      if (ie.Decl is Constant)
+        return new StrideForm(StrideForm.Kind.Constant, e);
+      if (ie.Decl == v)
+        return new StrideForm(StrideForm.Kind.Identity, e);
+    }
+
+    if (GPUVerifier.IsBVAdd(e, out lhs, out rhs)) {
+      var lhssf = ComputeStrideForm(v, lhs);
+      var rhssf = ComputeStrideForm(v, rhs);
+      if (lhssf.kind == StrideForm.Kind.Constant &&
+          rhssf.kind == StrideForm.Kind.Constant)
+        return new StrideForm(StrideForm.Kind.Constant, e);
+      else if (lhssf.kind == StrideForm.Kind.Constant &&
+               rhssf.kind == StrideForm.Kind.Identity)
+        return new StrideForm(StrideForm.Kind.Product, lhs);
+      else if (lhssf.kind == StrideForm.Kind.Identity &&
+               rhssf.kind == StrideForm.Kind.Constant)
+        return new StrideForm(StrideForm.Kind.Product, rhs);
+      else if (lhssf.kind == StrideForm.Kind.Constant &&
+               rhssf.kind == StrideForm.Kind.Product)
+        return new StrideForm(StrideForm.Kind.Product, verifier.MakeBVAdd(lhs, rhssf.op));
+      else if (lhssf.kind == StrideForm.Kind.Product &&
+               rhssf.kind == StrideForm.Kind.Constant)
+        return new StrideForm(StrideForm.Kind.Product, verifier.MakeBVAdd(lhssf.op, rhs));
+      else
+        return new StrideForm(StrideForm.Kind.Bottom);
+    }
+
+    var ne = e as NAryExpr;
+    if (ne != null) {
+      foreach (Expr op in ne.Args)
+        if (ComputeStrideForm(v, op).kind != StrideForm.Kind.Constant)
+          return new StrideForm(StrideForm.Kind.Bottom);
+      return new StrideForm(StrideForm.Kind.Constant, e);
+    }
+
+    return new StrideForm(StrideForm.Kind.Bottom);
+  }
+
+  private void AddDefinitionPair(Variable v, Expr constDef, Expr nonConstDef, object nonConstId) {
+    var sf = ComputeStrideForm(v, nonConstDef);
+    if (sf.kind == StrideForm.Kind.Product) {
+      var sc = new ModStrideConstraint(sf.op, constDef);
+      if (!sc.IsBottom()) {
+        strideConstraintMap[v.Name] = sc;
+        List<string> lcs;
+        if (loopCounterMap.ContainsKey(nonConstId))
+          lcs = loopCounterMap[nonConstId];
+        else
+          lcs = loopCounterMap[nonConstId] = new List<string>();
+        lcs.Add(v.Name);
+      }
+    }
+  }
+
+  public StrideConstraint GetStrideConstraint(string varName) {
+    int id;
+    var strippedVarName = GPUVerifier.StripThreadIdentifier(varName, out id);
+    if (!strideConstraintMap.ContainsKey(strippedVarName))
+      return null;
+
+    var msc = strideConstraintMap[strippedVarName];
+    if (id == 0)
+      return msc;
+    return new ModStrideConstraint(verifier.MaybeDualise(msc.mod, id, impl.Name),
+                                   verifier.MaybeDualise(msc.modEq, id, impl.Name));
+  }
+
+  public IEnumerable<string> StridedLoopCounters(object loopId) {
+    if (!loopCounterMap.ContainsKey(loopId))
+      return Enumerable.Empty<string>();
+    return loopCounterMap[loopId];
+  }
+
+  public static ReducedStrengthAnalysis Analyse(GPUVerifier verifier, Implementation impl) {
+    var a = new ReducedStrengthAnalysis(verifier, impl);
+    a.Analyse();
+    return a;
+  }
+}
+
+}
diff --git a/Source/GPUVerify/StrideConstraint.cs b/Source/GPUVerify/StrideConstraint.cs
new file mode 100644
index 00000000..948786b7
--- /dev/null
+++ b/Source/GPUVerify/StrideConstraint.cs
@@ -0,0 +1,141 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Basetypes;
+using Microsoft.Boogie;
+
+namespace GPUVerify {
+
+class StrideConstraint {
+
+  public static StrideConstraint Bottom(Expr e) {
+    int width = e.Type.BvBits;
+    return new ModStrideConstraint(new LiteralExpr(Token.NoToken, BigNum.FromInt(1), width),
+                                   new LiteralExpr(Token.NoToken, BigNum.FromInt(0), width));
+  }
+
+  public bool IsBottom() {
+    var msc = this as ModStrideConstraint;
+    if (msc == null)
+        return false;
+
+    var le = msc.mod as LiteralExpr;
+    if (le == null)
+        return false;
+
+    var bvc = le.Val as BvConst;
+    if (bvc == null)
+        return false;
+
+    return bvc.Value.InInt32 && bvc.Value.ToInt == 1;
+  }
+
+  private Expr ExprModPow2(GPUVerifier verifier, Expr expr, Expr powerOfTwoExpr) {
+    Expr Pow2Minus1 = verifier.MakeBVSub(powerOfTwoExpr, 
+                                         new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 32));
+
+    return verifier.MakeBVAnd(Pow2Minus1, expr);
+  }
+
+  public Expr MaybeBuildPredicate(GPUVerifier verifier, Expr e) {
+    var msc = this as ModStrideConstraint;
+    if (msc != null && !msc.IsBottom()) {
+      Expr modEqExpr = Expr.Eq(ExprModPow2(verifier, e, msc.mod), ExprModPow2(verifier, msc.modEq, msc.mod));
+      return modEqExpr;
+    }
+
+    return null;
+  }
+
+  private static StrideConstraint BuildAddStrideConstraint(GPUVerifier verifier, Expr e, StrideConstraint lhsc, StrideConstraint rhsc) {
+    if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint) {
+      return new EqStrideConstraint(e);
+    }
+
+    if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)
+      return BuildAddStrideConstraint(verifier, e, rhsc, lhsc);
+
+    if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint) {
+      var lhsmc = (ModStrideConstraint)lhsc;
+      var rhsec = (EqStrideConstraint)rhsc;
+
+      return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsec.eq));
+    }
+
+    if (lhsc is ModStrideConstraint && rhsc is ModStrideConstraint) {
+      var lhsmc = (ModStrideConstraint)lhsc;
+      var rhsmc = (ModStrideConstraint)rhsc;
+
+      if (lhsmc.mod == rhsmc.mod)
+        return new ModStrideConstraint(lhsmc.mod, verifier.MakeBVAdd(lhsmc.modEq, rhsmc.modEq));
+    }
+
+    return Bottom(e);
+  }
+
+  private static StrideConstraint BuildMulStrideConstraint(GPUVerifier verifier, Expr e, StrideConstraint lhsc, StrideConstraint rhsc) {
+    if (lhsc is EqStrideConstraint && rhsc is EqStrideConstraint) {
+      return new EqStrideConstraint(e);
+    }
+
+    if (lhsc is EqStrideConstraint && rhsc is ModStrideConstraint)
+      return BuildMulStrideConstraint(verifier, e, rhsc, lhsc);
+
+    if (lhsc is ModStrideConstraint && rhsc is EqStrideConstraint) {
+      var lhsmc = (ModStrideConstraint)lhsc;
+      var rhsec = (EqStrideConstraint)rhsc;
+
+      return new ModStrideConstraint(verifier.MakeBVMul(lhsmc.mod, rhsec.eq),
+                                     verifier.MakeBVMul(lhsmc.modEq, rhsec.eq));
+    }
+
+    return Bottom(e);
+  }
+
+  public static StrideConstraint FromExpr(GPUVerifier verifier, Implementation impl, Expr e) {
+    if (e is LiteralExpr)
+      return new EqStrideConstraint(e);
+
+    var ie = e as IdentifierExpr;
+    if (ie != null) {
+      if (ie.Decl is Constant)
+        return new EqStrideConstraint(e);
+
+      var rsa = verifier.reducedStrengthAnalyses[impl];
+      var sc = rsa.GetStrideConstraint(ie.Decl.Name);
+      if (sc == null)
+        return Bottom(e);
+      return sc;
+    }
+
+    Expr lhs, rhs;
+
+    if (GPUVerifier.IsBVAdd(e, out lhs, out rhs)) {
+      var lhsc = FromExpr(verifier, impl, lhs);
+      var rhsc = FromExpr(verifier, impl, rhs);
+      return BuildAddStrideConstraint(verifier, e, lhsc, rhsc);
+    }
+
+    if (GPUVerifier.IsBVMul(e, out lhs, out rhs)) {
+      var lhsc = FromExpr(verifier, impl, lhs);
+      var rhsc = FromExpr(verifier, impl, rhs);
+      return BuildMulStrideConstraint(verifier, e, lhsc, rhsc);
+    }
+
+    return Bottom(e);
+  }
+
+}
+
+class EqStrideConstraint : StrideConstraint {
+  public EqStrideConstraint(Expr eq) { this.eq = eq; }
+  public Expr eq;
+}
+
+class ModStrideConstraint : StrideConstraint {
+  public ModStrideConstraint(Expr mod, Expr modEq) { this.mod = mod; this.modEq = modEq; }
+  public Expr mod, modEq;
+}
+
+}
author	Peter Collingbourne <peter@pcc.me.uk>	2012-07-02 20:36:17 +0100
committer	Peter Collingbourne <peter@pcc.me.uk>	2012-07-02 20:36:17 +0100
commit	8505b37ece6701ac653e8fb856a78eaafefce577 (patch)
tree	7d15426b5f0a74415f6d09318873b900a9afdad9 /Source
parent	a45579e46cf7ac3940f7cf50319c4dfb1231e993 (diff)