More accessed offset inference

9 files changed, 403 insertions, 147 deletions

diff --git a/Source/GPUVerify/AccessInvariantProcessor.cs b/Source/GPUVerify/AccessInvariantProcessor.cs
index 71d3e482..16833b09 100644
--- a/Source/GPUVerify/AccessInvariantProcessor.cs
+++ b/Source/GPUVerify/AccessInvariantProcessor.cs
@@ -44,36 +44,36 @@ namespace GPUVerify
 

                 if (MatchesIntrinsic(call.Func, READ_IMPLIES))

                 {

-                    return Expr.Imp(MakeReadHasOccurred(node, call, READ_IMPLIES), VisitExpr(node.Args[0]));

+                    return Expr.Imp(MakeReadHasOccurred(call, READ_IMPLIES), VisitExpr(node.Args[0]));

                 }

 

                 if (MatchesIntrinsic(call.Func, WRITE_IMPLIES))

                 {

-                    return Expr.Imp(MakeWriteHasOccurred(node, call, WRITE_IMPLIES), VisitExpr(node.Args[0]));

+                    return Expr.Imp(MakeWriteHasOccurred(call, WRITE_IMPLIES), VisitExpr(node.Args[0]));

                 }

 

                 if (MatchesIntrinsic(call.Func, NO_READ))

                 {

                     return Expr.Not(

-                        MakeReadHasOccurred(node, call, NO_READ)

+                        MakeReadHasOccurred(call, NO_READ)

                     );

                 }

 

                 if (MatchesIntrinsic(call.Func, NO_WRITE))

                 {

                     return Expr.Not(

-                        MakeWriteHasOccurred(node, call, NO_WRITE)

+                        MakeWriteHasOccurred(call, NO_WRITE)

                     );

                 }

 

                 if (MatchesIntrinsic(call.Func, READ))

                 {

-                    return MakeReadHasOccurred(node, call, READ);

+                    return MakeReadHasOccurred(call, READ);

                 }

 

                 if (MatchesIntrinsic(call.Func, WRITE))

                 {

-                    return MakeWriteHasOccurred(node, call, WRITE);

+                    return MakeWriteHasOccurred(call, WRITE);

                 }

 

             }

@@ -81,18 +81,14 @@ namespace GPUVerify
             return base.VisitNAryExpr(node);

         }

 

-        private static IdentifierExpr MakeReadHasOccurred(NAryExpr node, FunctionCall call, string intrinsicPrefix)

+        private static IdentifierExpr MakeReadHasOccurred(FunctionCall call, string intrinsicPrefix)

         {

-            return new IdentifierExpr(node.tok, new GlobalVariable(

-                                        node.tok, new TypedIdent(node.tok, "_READ_HAS_OCCURRED_" +

-                                            call.Func.Name.Substring(intrinsicPrefix.Length), Microsoft.Boogie.Type.Bool)));

+            return GPUVerifier.MakeAccessHasOccurredExpr(call.Func.Name.Substring(intrinsicPrefix.Length), "READ");

         }

 

-        private static IdentifierExpr MakeWriteHasOccurred(NAryExpr node, FunctionCall call, string intrinsicPrefix)

+        private static IdentifierExpr MakeWriteHasOccurred(FunctionCall call, string intrinsicPrefix)

         {

-            return new IdentifierExpr(node.tok, new GlobalVariable(

-                                        node.tok, new TypedIdent(node.tok, "_WRITE_HAS_OCCURRED_" +

-                                            call.Func.Name.Substring(intrinsicPrefix.Length), Microsoft.Boogie.Type.Bool)));

+            return GPUVerifier.MakeAccessHasOccurredExpr(call.Func.Name.Substring(intrinsicPrefix.Length), "WRITE");

         }

 

 

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 06acb694..8c090b6a 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -34,6 +34,8 @@ namespace GPUVerify
         public static bool AddDivergenceCandidatesOnlyIfModified = true;

         public static bool AddDivergenceCandidatesOnlyToBarrierLoops = true;

 

+        public static bool AssignAtBarriers = false;

+

         public static bool ShowUniformityAnalysis = false;

         public static bool DoUniformityAnalysis = true;

 

@@ -154,10 +156,16 @@ namespace GPUVerify
                     break;

 

                     case "-alwaysAddDivergenceCandidates":

+                    case "/alwaysAddDivergenceCandidates":

                     AddDivergenceCandidatesOnlyIfModified = false;

                     AddDivergenceCandidatesOnlyToBarrierLoops = false;

                     break;

 

+                    case "-assignAtBarriers":

+                    case "/assignAtBarriers":

+                    AssignAtBarriers = true;

+                    break;

+

                     case "-showUniformityAnalysis":

                     case "/showUniformityAnalysis":

                     ShowUniformityAnalysis = true;

diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
index 7a281da1..4c21765a 100644
--- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
@@ -28,7 +28,7 @@ namespace GPUVerify
             MakeLogAccessProcedureHeader(v, ReadOrWrite, out XParameterVariable, out YParameterVariable, out ZParameterVariable, out LogReadOrWriteProcedure);

 

             IdentifierExprSeq modifies = LogReadOrWriteProcedure.Modifies;

-            Variable ReadOrWriteHasOccurredVariable = MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);

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

             Variable ReadOrWriteOffsetXVariable = null;

             Variable ReadOrWriteOffsetYVariable = null;

             Variable ReadOrWriteOffsetZVariable = null;

@@ -96,7 +96,7 @@ namespace GPUVerify
             ModifiedAtLog = new IdentifierExprSeq();

             ResetAtBarrier = new IdentifierExprSeq();

 

-            Variable AccessHasOccurred = new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));

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

 

             if (CommandLineOptions.Symmetry && ReadOrWrite.Equals("READ"))

             {

@@ -172,24 +172,36 @@ namespace GPUVerify
 

         protected override void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v, string AccessType)

         {

-            IdentifierExpr AccessOccurred1 = new IdentifierExpr(tok, 

-                new VariableDualiser(1, null, null).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));

+            IdentifierExpr AccessOccurred1 = new IdentifierExpr(tok,

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

             IdentifierExpr AccessOccurred2 = new IdentifierExpr(tok,

-                new VariableDualiser(2, null, null).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, AccessType)));

+                new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, AccessType)));

 

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

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

+            if (CommandLineOptions.AssignAtBarriers)

+            {

 

-            lhss.Add(new SimpleAssignLhs(tok, AccessOccurred1));

-            rhss.Add(Expr.False);

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

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

 

-            if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))

-            {

-                lhss.Add(new SimpleAssignLhs(tok, AccessOccurred2));

+                lhss.Add(new SimpleAssignLhs(tok, AccessOccurred1));

                 rhss.Add(Expr.False);

-            }

 

-            bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));

+                if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))

+                {

+                    lhss.Add(new SimpleAssignLhs(tok, AccessOccurred2));

+                    rhss.Add(Expr.False);

+                }

+

+                bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));

+            }

+            else

+            {

+                bb.simpleCmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(AccessOccurred1)));

+                if (!CommandLineOptions.Symmetry || !AccessType.Equals("READ"))

+                {

+                    bb.simpleCmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(AccessOccurred2)));

+                }

+            }

         }

 

         public override void CheckForRaces(BigBlock bb, Variable v, bool ReadWriteOnly)

@@ -208,8 +220,8 @@ namespace GPUVerify
         protected override Expr GenerateRaceCondition(Variable v, string FirstAccessType, string SecondAccessType)

         {

             Expr RaceCondition = Expr.And(

-                new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, FirstAccessType))),

-                new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(MakeReadOrWriteHasOccurredVariable(v, SecondAccessType))));

+                new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, FirstAccessType))),

+                new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, SecondAccessType))));

 

             if (GPUVerifier.HasXDimension(v))

             {

@@ -285,17 +297,12 @@ namespace GPUVerify
 

         }

 

-        internal static GlobalVariable MakeReadOrWriteHasOccurredVariable(Variable v, string ReadOrWrite)

-        {

-            return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_HAS_OCCURRED_" + v.Name, Microsoft.Boogie.Type.Bool));

-        }

-

         protected override void AddRequiresNoPendingAccess(Variable v)

         {

-            IdentifierExpr ReadAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "READ")));

-            IdentifierExpr ReadAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "READ")));

-            IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "WRITE")));

-            IdentifierExpr WriteAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, "WRITE")));

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

+            IdentifierExpr ReadAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2, 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")));

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

 

             if (CommandLineOptions.Symmetry)

             {

@@ -316,7 +323,7 @@ namespace GPUVerify
 

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

         {

-            Variable ReadOrWriteHasOccurred = ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite);

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

@@ -348,7 +355,7 @@ namespace GPUVerify
             if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))

             {

                 expr = Expr.Imp(

-                        new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),

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

@@ -360,7 +367,7 @@ namespace GPUVerify
             if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))

             {

                 expr = Expr.Imp(

-                        new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, ReadOrWrite))),

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

@@ -372,9 +379,7 @@ namespace GPUVerify
 

         private Expr GlobalIdExpr(string dimension, int Thread)

         {

-            return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",

-                            new IdentifierExpr(Token.NoToken, verifier.GetGroupId(dimension)), new IdentifierExpr(Token.NoToken, verifier.GetGroupSize(dimension))),

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

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

         }

 

         private Expr GlobalSizeExpr(string dimension)

@@ -458,7 +463,7 @@ namespace GPUVerify
 

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

         {

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

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

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 26b2759d..581d124e 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -68,7 +68,8 @@ namespace GPUVerify
         public MayBeGidAnalyser mayBeGidAnalyser;

         public MayBeGlobalSizeAnalyser mayBeGlobalSizeAnalyser;

         public MayBeFlattened2DTidOrGidAnalyser mayBeFlattened2DTidOrGidAnalyser;

-        public MayBeTidPlusConstantAnalyser mayBeTidPlusConstantAnalyser;

+        public MayBeLocalIdPlusConstantAnalyser mayBeTidPlusConstantAnalyser;

+        public MayBeGlobalIdPlusConstantAnalyser mayBeGidPlusConstantAnalyser;

         public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;

         public LiveVariableAnalyser liveVariableAnalyser;

         public ArrayControlFlowAnalyser arrayControlFlowAnalyser;

@@ -323,7 +324,7 @@ namespace GPUVerify
 

             DoMayBeTidAnalysis();

 

-            DoMayBeTidPlusConstantAnalysis();

+            DoMayBeIdPlusConstantAnalysis();

 

             DoMayBePowerOfTwoAnalysis();

 

@@ -458,10 +459,12 @@ namespace GPUVerify
             mayBeFlattened2DTidOrGidAnalyser.Analyse();

         }

 

-        private void DoMayBeTidPlusConstantAnalysis()

+        private void DoMayBeIdPlusConstantAnalysis()

         {

-            mayBeTidPlusConstantAnalyser = new MayBeTidPlusConstantAnalyser(this);

+            mayBeTidPlusConstantAnalyser = new MayBeLocalIdPlusConstantAnalyser(this);

             mayBeTidPlusConstantAnalyser.Analyse();

+            mayBeGidPlusConstantAnalyser = new MayBeGlobalIdPlusConstantAnalyser(this);

+            mayBeGidPlusConstantAnalyser.Analyse();

         }

 

         private void DoArrayControlFlowAnalysis()

@@ -1289,7 +1292,7 @@ namespace GPUVerify
             return null;

         }

 

-        internal Constant MakeThreadId(IToken tok, string dimension, int number)

+        internal Constant MakeThreadId(IToken tok, string dimension)

         {

             Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));

             string name = null;

@@ -1297,7 +1300,13 @@ namespace GPUVerify
             if (dimension.Equals("Y")) name = _Y.Name;

             if (dimension.Equals("Z")) name = _Z.Name;

             Debug.Assert(name != null);

-            return new Constant(tok, new TypedIdent(tok, name + "$" + number, GetTypeOfId(dimension)));

+            return new Constant(tok, new TypedIdent(tok, name, GetTypeOfId(dimension)));

+        }

+

+        internal Constant MakeThreadId(IToken tok, string dimension, int number)

+        {

+            Constant resultWithoutThreadId = MakeThreadId(tok, dimension);

+            return new Constant(tok, new TypedIdent(tok, resultWithoutThreadId.Name + "$" + number, GetTypeOfId(dimension)));

         }

 

         internal Constant GetGroupId(string dimension)

@@ -1610,8 +1619,8 @@ namespace GPUVerify
         {

             IdentifierExprSeq newVars = new IdentifierExprSeq();

 

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

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

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

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

 

             newVars.Add(new IdentifierExpr(v.tok, ReadHasOccurred));

             newVars.Add(new IdentifierExpr(v.tok, WriteHasOccurred));

@@ -1669,6 +1678,20 @@ namespace GPUVerify
         }

 

 

+        internal static GlobalVariable MakeAccessHasOccurredVariable(string varName, string accessType)

+        {

+            return new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, MakeAccessHasOccurredVariableName(varName, accessType), Microsoft.Boogie.Type.Bool));

+        }

+

+        internal static string MakeAccessHasOccurredVariableName(string varName, string accessType)

+        {

+            return "_" + accessType + "_HAS_OCCURRED_" + varName;

+        }

+

+        internal static IdentifierExpr MakeAccessHasOccurredExpr(string varName, string accessType)

+        {

+            return new IdentifierExpr(Token.NoToken, MakeAccessHasOccurredVariable(varName, accessType));

+        }

 

         internal static bool IsIntOrBv32(Microsoft.Boogie.Type type)

         {

@@ -2150,10 +2173,7 @@ namespace GPUVerify
 

         public static bool IsThreadLocalIdConstant(Variable variable)

         {

-            return variable is Constant && (

-                QKeyValue.FindBoolAttribute(variable.Attributes, LOCAL_ID_X_STRING) || 

-                QKeyValue.FindBoolAttribute(variable.Attributes, LOCAL_ID_Y_STRING) ||

-                QKeyValue.FindBoolAttribute(variable.Attributes, LOCAL_ID_Z_STRING));

+            return variable.Name.Equals(_X.Name) || variable.Name.Equals(_Y.Name) || variable.Name.Equals(_Z.Name);

         }

 

         internal void AddCandidateInvariant(WhileCmd wc, Expr e)

@@ -2237,6 +2257,13 @@ namespace GPUVerify
         {

             return new ThreadIdentifierStripper().VisitExpr(e.Clone() as Expr);

         }

+

+        internal Expr GlobalIdExpr(string dimension)

+        {

+            return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_ADD", GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",

+                            new IdentifierExpr(Token.NoToken, GetGroupId(dimension)), new IdentifierExpr(Token.NoToken, GetGroupSize(dimension))),

+                                new IdentifierExpr(Token.NoToken, MakeThreadId(Token.NoToken, dimension)));

+        }

     }

 

     class ThreadIdentifierStripper : StandardVisitor

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 39f24d85..b767816c 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -117,7 +117,7 @@
     <Compile Include="LoopInvariantGenerator.cs" />

     <Compile Include="MayBePowerOfTwoAnalyser.cs" />

     <Compile Include="MayBeThreadConfigurationVariableAnalyser.cs" />

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

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

     <Compile Include="StructuredProgramVisitor.cs" />

     <Compile Include="CrossThreadInvariantProcessor.cs" />

     <Compile Include="EnabledToPredicateVisitor.cs" />

diff --git a/Source/GPUVerify/MayBeGidAnalyser.cs b/Source/GPUVerify/MayBeGidAnalyser.cs
index 0d054bc6..bb0f8d22 100644
--- a/Source/GPUVerify/MayBeGidAnalyser.cs
+++ b/Source/GPUVerify/MayBeGidAnalyser.cs
@@ -7,7 +7,7 @@ using Microsoft.Boogie;
 

 namespace GPUVerify

 {

-    class MayBeGidAnalyser

+    class MayBeGidAnalyser : MayBeAnalyser

     {

         private static string[] dimensions = { "x", "y", "z" };

 

@@ -213,7 +213,7 @@ namespace GPUVerify
             mayBeInfo[component][proc][v] = true;

         }

 

-        internal bool MayBe(string component, string proc, string v)

+        override internal bool MayBe(string component, string proc, string v)

         {

             if (!mayBeInfo[component].ContainsKey(proc))

             {

@@ -228,7 +228,7 @@ namespace GPUVerify
             return mayBeInfo[component][proc][v];

         }

 

-        internal bool MayBe(string component, string proc, Expr e)

+        override internal bool MayBe(string component, string proc, Expr e)

         {

             if (e is IdentifierExpr)

             {

diff --git a/Source/GPUVerify/MayBeTidPlusConstantAnalyser.cs b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
index f8b46cf1..f1cf332a 100644
--- a/Source/GPUVerify/MayBeTidPlusConstantAnalyser.cs
+++ b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
@@ -7,25 +7,27 @@ using Microsoft.Boogie;
 

 namespace GPUVerify

 {

-    class MayBeTidPlusConstantAnalyser

+    abstract class MayBeIdPlusConstantAnalyser

     {

-        private GPUVerifier verifier;

+        protected GPUVerifier verifier;

+

+        protected MayBeAnalyser mayBeAnalyser;

 

         // Given a p.v, says whether p.v may be assigned to a tid variable at some point

-        private Dictionary<string, Dictionary<string, bool>> mayBeAssignedTid;

+        protected Dictionary<string, Dictionary<string, bool>> mayBeAssignedId;

 

         // Records the constants that p.v may be incremented by

-        private Dictionary<string, Dictionary<string, HashSet<Expr>>> incrementedBy;

+        protected Dictionary<string, Dictionary<string, HashSet<Expr>>> incrementedBy;

 

         // The final result

-        private Dictionary<string, Dictionary<string, bool>> mayBeTidPlusConstantInfo;

+        protected Dictionary<string, Dictionary<string, bool>> mayBeIdPlusConstantInfo;

 

-        public MayBeTidPlusConstantAnalyser(GPUVerifier verifier)

+        public MayBeIdPlusConstantAnalyser(GPUVerifier verifier)

         {

             this.verifier = verifier;

-            mayBeAssignedTid = new Dictionary<string, Dictionary<string, bool>>();

+            mayBeAssignedId = new Dictionary<string, Dictionary<string, bool>>();

             incrementedBy = new Dictionary<string, Dictionary<string, HashSet<Expr>>>();

-            mayBeTidPlusConstantInfo = new Dictionary<string, Dictionary<string, bool>>();

+            mayBeIdPlusConstantInfo = new Dictionary<string, Dictionary<string, bool>>();

         }

 

         internal void Analyse()

@@ -35,35 +37,35 @@ namespace GPUVerify
                 if (D is Implementation)

                 {

                     Implementation Impl = D as Implementation;

-                    mayBeAssignedTid[Impl.Name] = new Dictionary<string, bool>();

+                    mayBeAssignedId[Impl.Name] = new Dictionary<string, bool>();

                     incrementedBy[Impl.Name] = new Dictionary<string, HashSet<Expr>>();

-                    mayBeTidPlusConstantInfo[Impl.Name] = new Dictionary<string, bool> ();

+                    mayBeIdPlusConstantInfo[Impl.Name] = new Dictionary<string, bool>();

 

                     foreach (Variable v in Impl.LocVars)

                     {

-                        mayBeAssignedTid[Impl.Name][v.Name] = false;

+                        mayBeAssignedId[Impl.Name][v.Name] = false;

                         incrementedBy[Impl.Name][v.Name] = new HashSet<Expr>();

                     }

 

                     foreach (Variable v in Impl.InParams)

                     {

-                        mayBeAssignedTid[Impl.Name][v.Name] = false;

+                        mayBeAssignedId[Impl.Name][v.Name] = false;

                         incrementedBy[Impl.Name][v.Name] = new HashSet<Expr>();

                     }

 

                     foreach (Variable v in Impl.OutParams)

                     {

-                        mayBeAssignedTid[Impl.Name][v.Name] = false;

+                        mayBeAssignedId[Impl.Name][v.Name] = false;

                         incrementedBy[Impl.Name][v.Name] = new HashSet<Expr>();

                     }

 

                     // Fixpoint not required - this is just syntactic

                     Analyse(Impl);

 

-                    foreach (string v in mayBeAssignedTid[Impl.Name].Keys)

+                    foreach (string v in mayBeAssignedId[Impl.Name].Keys)

                     {

-                        mayBeTidPlusConstantInfo[Impl.Name][v] =

-                            mayBeAssignedTid[Impl.Name][v] && incrementedBy[Impl.Name][v].Count == 1;

+                        mayBeIdPlusConstantInfo[Impl.Name][v] =

+                            mayBeAssignedId[Impl.Name][v] && incrementedBy[Impl.Name][v].Count == 1;

                     }

 

                 }

@@ -88,6 +90,7 @@ namespace GPUVerify
             }

         }

 

+

         private void Analyse(Implementation impl, BigBlock bb)

         {

             foreach (Cmd c in bb.simpleCmds)

@@ -103,7 +106,7 @@ namespace GPUVerify
                     {

                         Variable lhsV = (assign.Lhss[0] as SimpleAssignLhs).AssignedVariable.Decl;

 

-                        if (mayBeAssignedTid[impl.Name].ContainsKey(lhsV.Name))

+                        if (mayBeAssignedId[impl.Name].ContainsKey(lhsV.Name))

                         {

 

                             if (assign.Rhss[0] is IdentifierExpr)

@@ -111,9 +114,9 @@ namespace GPUVerify
 

                                 Variable rhsV = (assign.Rhss[0] as IdentifierExpr).Decl;

 

-                                if (verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, rhsV.Name))

+                                if (mayBeAnalyser.MayBe(ComponentString(), impl.Name, rhsV.Name))

                                 {

-                                    mayBeAssignedTid[impl.Name][lhsV.Name] = true;

+                                    mayBeAssignedId[impl.Name][lhsV.Name] = true;

                                 }

 

                             }

@@ -179,7 +182,7 @@ namespace GPUVerify
                 return null;

             }

 

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

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

                 ((nary.Args[0] as IdentifierExpr).Decl.Name.Equals(v.Name))))

             {

                 return null;

@@ -206,12 +209,12 @@ namespace GPUVerify
 

         private void dump()

         {

-            foreach (string p in mayBeTidPlusConstantInfo.Keys)

+            foreach (string p in mayBeIdPlusConstantInfo.Keys)

             {

                 Console.WriteLine("Procedure " + p);

-                foreach (string v in mayBeTidPlusConstantInfo[p].Keys)

+                foreach (string v in mayBeIdPlusConstantInfo[p].Keys)

                 {

-                    Console.WriteLine("  " + v + ": gets assigned tid - " + mayBeAssignedTid[p][v]);

+                    Console.WriteLine("  " + v + ": gets assigned " + idKind() + " - " + mayBeAssignedId[p][v]);

                     Console.Write("  " + v + ": incremented by -");

                     foreach(Expr e in incrementedBy[p][v])

                     {

@@ -221,9 +224,9 @@ namespace GPUVerify
 

                     Console.Write("  " + v + ": ");

                     

-                    if(mayBeTidPlusConstantInfo[p][v])

+                    if(mayBeIdPlusConstantInfo[p][v])

                     {

-                        Console.Write("may be tid + ");

+                        Console.Write("may be " + idKind() + " + ");

                         foreach(Expr e in incrementedBy[p][v])

                         {

                             Console.WriteLine(ConvertToString(e));

@@ -231,33 +234,20 @@ namespace GPUVerify
                     }

                     else

                     {

-                        Console.WriteLine("likely not tid + const");

+                        Console.WriteLine("likely not " + idKind() + " + const");

                     }

                 }

             }

 

         }

 

+        protected abstract string idKind();

 

-        internal bool MayBeTidPlusConstant(string p, string v)

-        {

-            if (!mayBeTidPlusConstantInfo.ContainsKey(p))

-            {

-                return false;

-            }

-

-            if (!mayBeTidPlusConstantInfo[p].ContainsKey(v))

-            {

-                return false;

-            }

-

-            return mayBeTidPlusConstantInfo[p][v];

-        }

-

+        protected abstract string ComponentString();

 

         internal Expr GetIncrement(string p, string v)

         {

-            Debug.Assert(mayBeTidPlusConstantInfo[p][v]);

+            Debug.Assert(mayBeIdPlusConstantInfo[p][v]);

             Debug.Assert(incrementedBy[p][v].Count == 1);

             foreach (Expr e in incrementedBy[p][v])

             {

@@ -267,18 +257,18 @@ namespace GPUVerify
             return null;

         }

 

-        internal HashSet<string> GetMayBeTidPlusConstantVars(string p)

+        internal HashSet<string> GetMayBeIdPlusConstantVars(string p)

         {

             HashSet<string> result = new HashSet<string>();

 

-            if(!mayBeTidPlusConstantInfo.ContainsKey(p))

+            if (!mayBeIdPlusConstantInfo.ContainsKey(p))

             {

                 return result;

             }

 

-            foreach (string v in mayBeTidPlusConstantInfo[p].Keys)

+            foreach (string v in mayBeIdPlusConstantInfo[p].Keys)

             {

-                if (mayBeTidPlusConstantInfo[p][v])

+                if (mayBeIdPlusConstantInfo[p][v])

                 {

                     result.Add(v);

                 }

@@ -286,5 +276,60 @@ namespace GPUVerify
 

             return result;

         }

+

+

+        internal abstract Expr MakeIdExpr();

+    }

+

+    class MayBeLocalIdPlusConstantAnalyser : MayBeIdPlusConstantAnalyser

+    {

+

+        internal MayBeLocalIdPlusConstantAnalyser(GPUVerifier verifier) : base(verifier)

+        {

+            mayBeAnalyser = verifier.mayBeTidAnalyser;

+        }

+

+        override internal Expr MakeIdExpr()

+        {

+            return new IdentifierExpr(Token.NoToken, GPUVerifier._X);

+        }

+

+        protected override string idKind()

+        {

+            return "local id";

+        }

+

+        protected override string ComponentString()

+        {

+            return GPUVerifier.LOCAL_ID_X_STRING;

+        }

     }

+

+    class MayBeGlobalIdPlusConstantAnalyser : MayBeIdPlusConstantAnalyser

+    {

+        internal MayBeGlobalIdPlusConstantAnalyser(GPUVerifier verifier)

+            : base(verifier)

+        {

+            mayBeAnalyser = verifier.mayBeGidAnalyser;

+        }

+

+        protected override string idKind()

+        {

+            return "global id";

+        }

+

+        override internal Expr MakeIdExpr()

+        {

+            return verifier.GlobalIdExpr("X");

+        }

+

+        protected override string ComponentString()

+        {

+            return "x";

+        }

+

+    }

+

+

+

 }

diff --git a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs
index c06edbee..bca71171 100644
--- a/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs
+++ b/Source/GPUVerify/MayBeThreadConfigurationVariableAnalyser.cs
@@ -7,7 +7,13 @@ using Microsoft.Boogie;
 

 namespace GPUVerify

 {

-    class MayBeThreadConfigurationVariableAnalyser

+    abstract class MayBeAnalyser

+    {

+        abstract internal bool MayBe(string component, string proc, string v);

+        abstract internal bool MayBe(string component, string proc, Expr e);

+    }

+

+    class MayBeThreadConfigurationVariableAnalyser : MayBeAnalyser

     {

         private static string[] SpecialNames = { 

             GPUVerifier.LOCAL_ID_X_STRING,

@@ -242,7 +248,7 @@ namespace GPUVerify
             mayBeInfo[component][proc][v] = true;

         }

 

-        internal bool MayBe(string component, string proc, string v)

+        override internal bool MayBe(string component, string proc, string v)

         {

             if (!mayBeInfo[component].ContainsKey(proc))

             {

@@ -257,7 +263,7 @@ namespace GPUVerify
             return mayBeInfo[component][proc][v];

         }

 

-        internal bool MayBe(string component, string proc, Expr e)

+        override internal bool MayBe(string component, string proc, Expr e)

         {

             if (e is IdentifierExpr)

             {

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index b065e9d0..b6136e6b 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -65,13 +65,24 @@ namespace GPUVerify
 

             if (verifier.ContainsBarrierCall(wc.Body))

             {

-                AddNoReadOrWriteCandidateInvariant(wc, v, "READ", "1");

-                AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE", "1");

-                if (!CommandLineOptions.Symmetry)

+                if (verifier.ContainsNamedVariable(

+                    LoopInvariantGenerator.GetModifiedVariables(wc.Body), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "READ")) 

+                    || CommandLineOptions.AssignAtBarriers)

+                {

+                    AddNoReadOrWriteCandidateInvariant(wc, v, "READ", "1");

+                    if (!CommandLineOptions.Symmetry)

+                    {

+                        AddNoReadOrWriteCandidateInvariant(wc, v, "READ", "2");

+                    }

+                }

+

+                if (verifier.ContainsNamedVariable(

+                    LoopInvariantGenerator.GetModifiedVariables(wc.Body), GPUVerifier.MakeAccessHasOccurredVariableName(v.Name, "WRITE"))

+                    || CommandLineOptions.AssignAtBarriers)

                 {

-                    AddNoReadOrWriteCandidateInvariant(wc, v, "READ", "2");

+                    AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE", "1");

+                    AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE", "2");

                 }

-                AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE", "2");

             }

         }

 

@@ -115,23 +126,147 @@ namespace GPUVerify
         {

             foreach (Expr e in GetOffsetsAccessed(wc.Body, v, accessKind))

             {

-                if (!TryGenerateCandidateForStrideVariable(impl, wc, v, e, accessKind))

+                if (TryGenerateCandidateForDirectStridedAccess(impl, wc, v, e, accessKind))

+                {

+                    continue;

+                }

+

+                if (!TryGenerateCandidateForReducedStrengthStrideVariable(impl, wc, v, e, accessKind))

                 {

                     if (e is IdentifierExpr)

                     {

                         foreach(Expr f in GetExpressionsFromWhichVariableIsAssignedInLoop(wc.Body, (e as IdentifierExpr).Decl))

                         {

-                            TryGenerateCandidateForStrideVariable(impl, wc, v, f, accessKind);

+                            TryGenerateCandidateForReducedStrengthStrideVariable(impl, wc, v, f, accessKind);

                         }

                     }

                 }

             }

         }

 

-        private bool TryGenerateCandidateForStrideVariable(Implementation impl, WhileCmd wc, Variable v, Expr e, string accessKind)

+        private bool TryGenerateCandidateForDirectStridedAccess(Implementation impl, WhileCmd wc, Variable v, Expr e, string accessKind)

+        {

+            if (!(e is NAryExpr))

+            {

+                return false;

+            }

+

+            NAryExpr nary = e as NAryExpr;

+

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

+            {

+                return false;

+            }

+

+            {

+                Expr constant = IsIdPlusConstantMultiple(nary.Args[0], nary.Args[1], true, impl);

+                if (constant != null)

+                {

+                    Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));

+                    Expr modPow2Expr = ExprModPow2EqualsId(offsetExpr, constant, new IdentifierExpr(Token.NoToken,

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

+

+                    Expr candidateInvariantExpr = Expr.Imp(

+                            new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),

+                            modPow2Expr);

+

+                    verifier.AddCandidateInvariant(wc, new VariableDualiser(1, verifier.uniformityAnalyser, impl.Name).VisitExpr(candidateInvariantExpr.Clone() as Expr));

+                    if (accessKind.Equals("WRITE") || !CommandLineOptions.Symmetry)

+                    {

+                        verifier.AddCandidateInvariant(wc, new VariableDualiser(2, verifier.uniformityAnalyser, impl.Name).VisitExpr(candidateInvariantExpr.Clone() as Expr));

+                    }

+                    return true;

+                }

+            }

+

+            {

+                Expr constant = IsIdPlusConstantMultiple(nary.Args[0], nary.Args[1], false, impl);

+                if (constant != null)

+                {

+                    Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));

+                    Expr modPow2Expr = ExprModPow2EqualsId(offsetExpr, constant, verifier.GlobalIdExpr("X"));

+

+                    Expr candidateInvariantExpr = Expr.Imp(

+                            new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),

+                            modPow2Expr);

+

+                    verifier.AddCandidateInvariant(wc, new VariableDualiser(1, verifier.uniformityAnalyser, impl.Name).VisitExpr(candidateInvariantExpr.Clone() as Expr));

+                    if (accessKind.Equals("WRITE") || !CommandLineOptions.Symmetry)

+                    {

+                        verifier.AddCandidateInvariant(wc, new VariableDualiser(2, verifier.uniformityAnalyser, impl.Name).VisitExpr(candidateInvariantExpr.Clone() as Expr));

+                    }

+                    return true;

+                }

+            }

+

+            return false;

+

+        }

+

+        private Expr IsIdPlusConstantMultiple(Expr arg1, Expr arg2, bool local, Implementation impl)

+        {

+            {

+                Expr constant = IsConstantMultiple(arg2);

+                if (constant != null && IsId(arg1, local, impl))

+                {

+                    return constant;

+                }

+            }

+

+            {

+                Expr constant = IsConstantMultiple(arg1);

+                if (constant != null && IsId(arg2, local, impl))

+                {

+                    return constant;

+                }

+            }

+

+            return null;

+

+        }

+

+        private Expr IsConstantMultiple(Expr e)

+        {

+            if (!(e is NAryExpr))

+            {

+                return null;

+            }

+

+            NAryExpr nary = e as NAryExpr;

+

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

+            {

+                return null;

+            }

+

+            if (IsConstant(nary.Args[0]))

+            {

+                return nary.Args[0];

+            }

+

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

+            {

+                return nary.Args[1];

+            }

+

+            return null;

+

+        }

+

+        private bool IsId(Expr mayBeId, bool local, Implementation impl)

+        {

+            if (local)

+            {

+                return verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, mayBeId);

+            }

+

+            return verifier.mayBeGidAnalyser.MayBe("x", impl.Name, mayBeId);

+        }

+

+        private bool TryGenerateCandidateForReducedStrengthStrideVariable(Implementation impl, WhileCmd wc, Variable v, Expr e, string accessKind)

         {

             foreach (string w in

-                verifier.mayBeTidPlusConstantAnalyser.GetMayBeTidPlusConstantVars(impl.Name))

+                verifier.mayBeTidPlusConstantAnalyser.GetMayBeIdPlusConstantVars(impl.Name))

             {

                 if (!verifier.ContainsNamedVariable(

                     LoopInvariantGenerator.GetModifiedVariables(wc.Body), w))

@@ -141,45 +276,74 @@ namespace GPUVerify
 

                 // Check also live

 

-                if (!IsLinearFunctionOfVariable(e, w))

+                if (GenerateModIdInvariants(impl, wc, v, e, accessKind, w, verifier.mayBeTidPlusConstantAnalyser))

+                {

+                    return true;

+                }

+

+            }

+

+            foreach (string w in

+                verifier.mayBeGidPlusConstantAnalyser.GetMayBeIdPlusConstantVars(impl.Name))

+            {

+                if (!verifier.ContainsNamedVariable(

+                    LoopInvariantGenerator.GetModifiedVariables(wc.Body), w))

                 {

                     continue;

                 }

 

-                Debug.Assert(!verifier.uniformityAnalyser.IsUniform(impl.Name, w));

+                // Check also live

+

+                if (GenerateModIdInvariants(impl, wc, v, e, accessKind, w, verifier.mayBeGidPlusConstantAnalyser))

+                {

+                    return true;

+                }

+

+            }

+            

+            

+            return false;

+        }

 

-                Variable wVariable = new LocalVariable(wc.tok, new TypedIdent(wc.tok, w,

-                        Microsoft.Boogie.Type.GetBvType(32)));

+        private bool GenerateModIdInvariants(Implementation impl, WhileCmd wc, Variable v, Expr e, string accessKind, 

+            string w, MayBeIdPlusConstantAnalyser mayBeIdPlusConstantAnalyser)

+        {

+            if (!IsLinearFunctionOfVariable(e, w))

+            {

+                return false;

+            }

 

-                Expr indexModPow2EqualsTid = ExprModPow2EqualsTid(

-                    new IdentifierExpr(wc.tok, wVariable),

-                    verifier.mayBeTidPlusConstantAnalyser.GetIncrement(impl.Name, w));

+            Debug.Assert(!verifier.uniformityAnalyser.IsUniform(impl.Name, w));

 

-                verifier.AddCandidateInvariant(wc, new VariableDualiser(1, verifier.uniformityAnalyser, impl.Name).VisitExpr(indexModPow2EqualsTid.Clone() as Expr));

-                verifier.AddCandidateInvariant(wc, new VariableDualiser(2, verifier.uniformityAnalyser, impl.Name).VisitExpr(indexModPow2EqualsTid.Clone() as Expr));

+            Variable wVariable = new LocalVariable(wc.tok, new TypedIdent(wc.tok, w,

+                    Microsoft.Boogie.Type.GetBvType(32)));

 

-                Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));

-                Expr invertedOffset = InverseOfLinearFunctionOfVariable(e, w, offsetExpr);

+            Expr indexModPow2EqualsId = ExprModPow2EqualsId(

+                new IdentifierExpr(wc.tok, wVariable),

+                mayBeIdPlusConstantAnalyser.GetIncrement(impl.Name, w), mayBeIdPlusConstantAnalyser.MakeIdExpr());

 

-                Expr invertedOffsetModPow2EqualsTid = ExprModPow2EqualsTid(

-                    invertedOffset,

-                    verifier.mayBeTidPlusConstantAnalyser.GetIncrement(impl.Name, w));

+            verifier.AddCandidateInvariant(wc, new VariableDualiser(1, verifier.uniformityAnalyser, impl.Name).VisitExpr(indexModPow2EqualsId.Clone() as Expr));

+            verifier.AddCandidateInvariant(wc, new VariableDualiser(2, verifier.uniformityAnalyser, impl.Name).VisitExpr(indexModPow2EqualsId.Clone() as Expr));

 

-                Expr candidateInvariantExpr = Expr.Imp(

-                        new IdentifierExpr(Token.NoToken, ElementEncodingRaceInstrumenter.MakeReadOrWriteHasOccurredVariable(v, accessKind)),

-                        invertedOffsetModPow2EqualsTid);

+            Expr offsetExpr = new IdentifierExpr(Token.NoToken, GPUVerifier.MakeOffsetXVariable(v, accessKind));

+            Expr invertedOffset = InverseOfLinearFunctionOfVariable(e, w, offsetExpr);

 

-                verifier.AddCandidateInvariant(wc, new VariableDualiser(1, verifier.uniformityAnalyser, impl.Name).VisitExpr(candidateInvariantExpr.Clone() as Expr));

+            Expr invertedOffsetModPow2EqualsId = ExprModPow2EqualsId(

+                invertedOffset,

+                mayBeIdPlusConstantAnalyser.GetIncrement(impl.Name, w), mayBeIdPlusConstantAnalyser.MakeIdExpr());

 

-                if (accessKind.Equals("WRITE") || !CommandLineOptions.Symmetry)

-                {

-                    verifier.AddCandidateInvariant(wc, new VariableDualiser(2, verifier.uniformityAnalyser, impl.Name).VisitExpr(candidateInvariantExpr.Clone() as Expr));

-                }

+            Expr candidateInvariantExpr = Expr.Imp(

+                    new IdentifierExpr(Token.NoToken, GPUVerifier.MakeAccessHasOccurredVariable(v.Name, accessKind)),

+                    invertedOffsetModPow2EqualsId);

 

-                return true;

+            verifier.AddCandidateInvariant(wc, new VariableDualiser(1, verifier.uniformityAnalyser, impl.Name).VisitExpr(candidateInvariantExpr.Clone() as Expr));

 

+            if (accessKind.Equals("WRITE") || !CommandLineOptions.Symmetry)

+            {

+                verifier.AddCandidateInvariant(wc, new VariableDualiser(2, verifier.uniformityAnalyser, impl.Name).VisitExpr(candidateInvariantExpr.Clone() as Expr));

             }

-            return false;

+

+            return true;

         }

 

         private HashSet<Expr> GetExpressionsFromWhichVariableIsAssignedInLoop(StmtList stmts, Variable variable)

@@ -290,7 +454,7 @@ namespace GPUVerify
             return null;

         }

 

-        private Expr ExprModPow2EqualsTid(Expr expr, Expr powerOfTwoExpr)

+        private Expr ExprModPow2EqualsId(Expr expr, Expr powerOfTwoExpr, Expr threadIdExpr)

         {

             Expr Pow2Minus1 = GPUVerifier.MakeBitVectorBinaryBitVector("BV32_SUB", powerOfTwoExpr, 

                             new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 32));

@@ -298,7 +462,7 @@ namespace GPUVerify
             Expr Pow2Minus1BitAndExpr =

                 GPUVerifier.MakeBitVectorBinaryBitVector("BV32_AND", Pow2Minus1, expr);

 

-            return Expr.Eq(Pow2Minus1BitAndExpr, new IdentifierExpr(Token.NoToken, GPUVerifier._X));

+            return Expr.Eq(Pow2Minus1BitAndExpr, threadIdExpr);

 

         }

 

@@ -570,7 +734,7 @@ namespace GPUVerify
                 return new KeyValuePair<IdentifierExpr, Expr>(null, null);

             }

 

-            if (!((nary.Args[1] is IdentifierExpr && (nary.Args[1] as IdentifierExpr).Decl is Constant) || nary.Args[1] is LiteralExpr))

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

             {

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

             }

@@ -579,6 +743,11 @@ namespace GPUVerify
 

         }

 

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