Implemented Houdini-based pointer analysis. Made inter-group race checking default.

17 files changed, 275 insertions, 242 deletions

diff --git a/Source/GPUVerify/AccessCollector.cs b/Source/GPUVerify/AccessCollector.cs
index 42ca5cc8..7debe82b 100644
--- a/Source/GPUVerify/AccessCollector.cs
+++ b/Source/GPUVerify/AccessCollector.cs
@@ -8,9 +8,9 @@ namespace GPUVerify
 {

     abstract class AccessCollector : StandardVisitor

     {

-        protected INonLocalState NonLocalState;

+        protected IKernelArrayInfo NonLocalState;

 

-        public AccessCollector(INonLocalState NonLocalState)

+        public AccessCollector(IKernelArrayInfo NonLocalState)

         {

             this.NonLocalState = NonLocalState;

         }

diff --git a/Source/GPUVerify/ArrayControlFlowAnalyser.cs b/Source/GPUVerify/ArrayControlFlowAnalyser.cs
index f1ce9f1e..d7841f0e 100644
--- a/Source/GPUVerify/ArrayControlFlowAnalyser.cs
+++ b/Source/GPUVerify/ArrayControlFlowAnalyser.cs
@@ -37,7 +37,7 @@ namespace GPUVerify
                     SetNotDerivedFromSharedState(Impl.Name, GPUVerifier._Y.Name);

                     SetNotDerivedFromSharedState(Impl.Name, GPUVerifier._Z.Name);

 

-                    foreach (Variable v in verifier.NonLocalState.getAllNonLocalVariables())

+                    foreach (Variable v in verifier.KernelArrayInfo.getAllNonLocalArrays())

                     {

                         SetMayBeDerivedFrom(Impl.Name, v.Name, v.Name);

                     }

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 03ec1728..ed20b08b 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -40,9 +40,7 @@ namespace GPUVerify
 

         public static bool Unstructured = false;

 

-        public static bool InterGroupRaceChecking = false;

-

-        public static bool BarrierParameters = false;

+        public static bool OnlyIntraGroupRaceChecking = false;

 

         public static int Parse(string[] args)

         {

@@ -176,14 +174,9 @@ namespace GPUVerify
                     Unstructured = true;

                     break;

 

-                    case "-interGroupRaceChecking":

-                    case "/interGroupRaceChecking":

-                    InterGroupRaceChecking = true;

-                    break;

-

-                    case "-barrierParameters":

-                    case "/barrierParameters":

-                    BarrierParameters = true;

+                    case "-onlyIntraGroupRaceChecking":

+                    case "/onlyIntraGroupRaceChecking":

+                    OnlyIntraGroupRaceChecking = true;

                     break;

 

                     default:

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 819eece5..56f632f2 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -20,7 +20,7 @@ namespace GPUVerify
         public Implementation KernelImplementation;

         public Procedure BarrierProcedure;

 

-        public INonLocalState NonLocalState = new NonLocalStateLists();

+        public IKernelArrayInfo KernelArrayInfo = new KernelArrayInfoLists();

 

         private HashSet<string> ReservedNames = new HashSet<string>();

 

@@ -117,8 +117,7 @@ namespace GPUVerify
             if (p == null)

             {

                 p = new Procedure(Token.NoToken, "barrier", new TypeVariableSeq(),

-                                  new VariableSeq(CommandLineOptions.BarrierParameters ? 

-                                      new Variable[] { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__flags", new BvType(32)), true) } : new Variable[] { }),

+                                  new VariableSeq(new Variable[] { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__flags", new BvType(32)), true) }),

                                   new VariableSeq(),

                                   new RequiresSeq(), new IdentifierExprSeq(),

                                   new EnsuresSeq(),

@@ -218,18 +217,22 @@ namespace GPUVerify
             bool success = true;

             foreach (Declaration D in Program.TopLevelDeclarations)

             {

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

+                if (D is Variable && 

+                    (D as Variable).IsMutable && 

+                    (D as Variable).TypedIdent.Type is MapType &&

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

                 {

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

+                    if (QKeyValue.FindBoolAttribute(D.Attributes, "group_shared"))

                     {

-                        if (QKeyValue.FindBoolAttribute(D.Attributes, "group_shared"))

-                        {

-                            NonLocalState.getGroupSharedVariables().Add(D as Variable);

-                        }

-                        else if(QKeyValue.FindBoolAttribute(D.Attributes, "global"))

-                        {

-                            NonLocalState.getGlobalVariables().Add(D as Variable);

-                        }

+                        KernelArrayInfo.getGroupSharedArrays().Add(D as Variable);

+                    }

+                    else if (QKeyValue.FindBoolAttribute(D.Attributes, "global"))

+                    {

+                        KernelArrayInfo.getGlobalArrays().Add(D as Variable);

+                    }

+                    else

+                    {

+                        KernelArrayInfo.getPrivateArrays().Add(D as Variable);

                     }

                 }

                 else if (D is Constant)

@@ -991,14 +994,11 @@ namespace GPUVerify
                         )

                     );

 

-                if (CommandLineOptions.InterGroupRaceChecking)

-                {

-                    Proc.Requires.Add(new Requires(false, Expr.Imp(ThreadsInSameGroup(), DistinctLocalIds)));

+                Proc.Requires.Add(new Requires(false, Expr.Imp(ThreadsInSameGroup(), DistinctLocalIds)));

 

-                }

-                else

+                if (CommandLineOptions.OnlyIntraGroupRaceChecking)

                 {

-                    Proc.Requires.Add(new Requires(false, DistinctLocalIds));

+                    Proc.Requires.Add(new Requires(false, ThreadsInSameGroup()));

                 }

 

                 if (Proc == KernelProcedure)

@@ -1117,39 +1117,31 @@ namespace GPUVerify
 

                 if (GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)))

                 {

-                    GroupSizePositive = MakeBVSgt(new IdentifierExpr(tok, GetGroupSize(dimension)), ZeroBV(tok));

-                    NumGroupsPositive = MakeBVSgt(new IdentifierExpr(tok, GetNumGroups(dimension)), ZeroBV(tok));

-                    GroupIdNonNegative = MakeBVSge(new IdentifierExpr(tok, GetGroupId(dimension)), ZeroBV(tok));

+                    GroupSizePositive = MakeBVSgt(new IdentifierExpr(tok, GetGroupSize(dimension)), ZeroBV());

+                    NumGroupsPositive = MakeBVSgt(new IdentifierExpr(tok, GetNumGroups(dimension)), ZeroBV());

+                    GroupIdNonNegative = MakeBVSge(new IdentifierExpr(tok, GetGroupId(dimension)), ZeroBV());

                     GroupIdLessThanNumGroups = MakeBVSlt(new IdentifierExpr(tok, GetGroupId(dimension)), new IdentifierExpr(tok, GetNumGroups(dimension)));

                 }

                 else

                 {

-                    GroupSizePositive = Expr.Gt(new IdentifierExpr(tok, GetGroupSize(dimension)), Zero(tok));

-                    NumGroupsPositive = Expr.Gt(new IdentifierExpr(tok, GetNumGroups(dimension)), Zero(tok));

-                    GroupIdNonNegative = Expr.Ge(new IdentifierExpr(tok, GetGroupId(dimension)), Zero(tok));

+                    GroupSizePositive = Expr.Gt(new IdentifierExpr(tok, GetGroupSize(dimension)), Zero());

+                    NumGroupsPositive = Expr.Gt(new IdentifierExpr(tok, GetNumGroups(dimension)), Zero());

+                    GroupIdNonNegative = Expr.Ge(new IdentifierExpr(tok, GetGroupId(dimension)), Zero());

                     GroupIdLessThanNumGroups = Expr.Lt(new IdentifierExpr(tok, GetGroupId(dimension)), new IdentifierExpr(tok, GetNumGroups(dimension)));

                 }

 

                 Proc.Requires.Add(new Requires(false, GroupSizePositive));

                 Proc.Requires.Add(new Requires(false, NumGroupsPositive));

-                if (CommandLineOptions.InterGroupRaceChecking)

-                {

-                    Proc.Requires.Add(new Requires(false, new VariableDualiser(1, null, null).VisitExpr(GroupIdNonNegative)));

-                    Proc.Requires.Add(new Requires(false, new VariableDualiser(2, null, null).VisitExpr(GroupIdNonNegative)));

-                    Proc.Requires.Add(new Requires(false, new VariableDualiser(1, null, null).VisitExpr(GroupIdLessThanNumGroups)));

-                    Proc.Requires.Add(new Requires(false, new VariableDualiser(2, null, null).VisitExpr(GroupIdLessThanNumGroups)));

-                }

-                else

-                {

-                    Proc.Requires.Add(new Requires(false, GroupIdNonNegative));

-                    Proc.Requires.Add(new Requires(false, GroupIdLessThanNumGroups));

-                }

+                Proc.Requires.Add(new Requires(false, new VariableDualiser(1, null, null).VisitExpr(GroupIdNonNegative)));

+                Proc.Requires.Add(new Requires(false, new VariableDualiser(2, null, null).VisitExpr(GroupIdNonNegative)));

+                Proc.Requires.Add(new Requires(false, new VariableDualiser(1, null, null).VisitExpr(GroupIdLessThanNumGroups)));

+                Proc.Requires.Add(new Requires(false, new VariableDualiser(2, null, null).VisitExpr(GroupIdLessThanNumGroups)));

 

                 Expr ThreadIdNonNegative =

                     GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)) ?

-                            MakeBVSge(new IdentifierExpr(tok, MakeThreadId(tok, dimension)), ZeroBV(tok))

+                            MakeBVSge(new IdentifierExpr(tok, MakeThreadId(tok, dimension)), ZeroBV())

                     :

-                            Expr.Ge(new IdentifierExpr(tok, MakeThreadId(tok, dimension)), Zero(tok));

+                            Expr.Ge(new IdentifierExpr(tok, MakeThreadId(tok, dimension)), Zero());

                 Expr ThreadIdLessThanGroupSize =

                     GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)) ?

                             MakeBVSlt(new IdentifierExpr(tok, MakeThreadId(tok, dimension)), new IdentifierExpr(tok, GetGroupSize(dimension)))

@@ -1313,14 +1305,14 @@ namespace GPUVerify
             return new Constant(Token.NoToken, new TypedIdent(Token.NoToken, resultWithoutThreadId.Name + "$" + number, GetTypeOfId(dimension)));

         }

 

-        private static LiteralExpr Zero(IToken tok)

+        private static LiteralExpr Zero()

         {

-            return new LiteralExpr(tok, BigNum.FromInt(0));

+            return new LiteralExpr(Token.NoToken, BigNum.FromInt(0));

         }

 

-        private static LiteralExpr ZeroBV(IToken tok)

+        internal static LiteralExpr ZeroBV()

         {

-            return new LiteralExpr(tok, BigNum.FromInt(0), 32);

+            return new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 32);

         }

 

         

@@ -1338,14 +1330,10 @@ namespace GPUVerify
             IdentifierExpr P1 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[0].TypedIdent));

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

 

-            IdentifierExpr Flags1 = CommandLineOptions.BarrierParameters ? new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[1].TypedIdent)) : null;

-            IdentifierExpr Flags2 = CommandLineOptions.BarrierParameters ? new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[paramsPerThread + 1].TypedIdent)) : null;

+            IdentifierExpr Flags1 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[1].TypedIdent));

+            IdentifierExpr Flags2 = new IdentifierExpr(tok, new LocalVariable(tok, BarrierProcedure.InParams[paramsPerThread + 1].TypedIdent));

 

-            Expr DivergenceCondition = Expr.Eq(P1, P2);

-            if (CommandLineOptions.InterGroupRaceChecking)

-            {

-                DivergenceCondition = Expr.Imp(ThreadsInSameGroup(), DivergenceCondition);

-            }

+            Expr DivergenceCondition = Expr.Imp(ThreadsInSameGroup(), Expr.Eq(P1, P2));

 

             checkNonDivergence.simpleCmds.Add(new AssertCmd(tok, DivergenceCondition));

 

@@ -1355,60 +1343,37 @@ namespace GPUVerify
                 returnbigblocks.Add(new BigBlock(tok, "__Disabled", new CmdSeq(), null, new ReturnCmd(tok)));

                 StmtList returnstatement = new StmtList(returnbigblocks, BarrierProcedure.tok);

 

-                Expr IfGuard;

-

-                if (CommandLineOptions.InterGroupRaceChecking)

-                {

-                    IfGuard = Expr.Or(Expr.And(Expr.Not(P1), Expr.Not(P2)), Expr.And(ThreadsInSameGroup(), Expr.Or(Expr.Not(P1), Expr.Not(P2))));

-                }

-                else

-                {

-                // We make this an "Or", not an "And", because "And" is implied by the assertion that the variables

-                // are equal, together with the "Or".  The weaker "Or" ensures that many auxiliary assertions will not

-                // fail if divergence has not been proved.

-                    IfGuard = Expr.Or(Expr.Not(P1), Expr.Not(P2));

-            }

+                Expr IfGuard = Expr.Or(Expr.And(Expr.Not(P1), Expr.Not(P2)), Expr.And(ThreadsInSameGroup(), Expr.Or(Expr.Not(P1), Expr.Not(P2))));

                 checkNonDivergence.ec = new IfCmd(tok, IfGuard, returnstatement, null, null);

             }

 

-            if(NonLocalState.getGroupSharedVariables().Count > 0) {

-                Expr IfGuard1 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P1 : (Expr)Expr.True;

-                Expr IfGuard2 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P2 : (Expr)Expr.True;

+            if(KernelArrayInfo.getGroupSharedArrays().Count > 0) {

 

-                if (CommandLineOptions.BarrierParameters)

-            {

-                    IfGuard1 = Expr.And(IfGuard1, CLK_LOCAL_MEM_FENCE_isSet(Flags1));

-                    IfGuard2 = Expr.And(IfGuard2, CLK_LOCAL_MEM_FENCE_isSet(Flags2));

-                }

+                Expr IfGuard1 = Expr.And(P1, CLK_LOCAL_MEM_FENCE_isSet(Flags1));

+                Expr IfGuard2 = Expr.And(P2, CLK_LOCAL_MEM_FENCE_isSet(Flags2));

 

                 bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

-                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, NonLocalState.getGroupSharedVariables()), Token.NoToken), null, null),

+                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),

                     null));

                 bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

-                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, NonLocalState.getGroupSharedVariables()), Token.NoToken), null, null),

+                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null),

                     null));

             }

 

-            if (NonLocalState.getGlobalVariables().Count > 0)

+            if (KernelArrayInfo.getGlobalArrays().Count > 0)

             {

-                Expr IfGuard1 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P1 : (Expr)Expr.True;

-                Expr IfGuard2 = CommandLineOptions.InterGroupRaceChecking ? (Expr)P2 : (Expr)Expr.True;

-

-                if (CommandLineOptions.BarrierParameters)

-                {

-                    IfGuard1 = Expr.And(IfGuard1, CLK_GLOBAL_MEM_FENCE_isSet(Flags1));

-                    IfGuard2 = Expr.And(IfGuard2, CLK_GLOBAL_MEM_FENCE_isSet(Flags2));

-                }

+                Expr IfGuard1 = Expr.And(P1, CLK_GLOBAL_MEM_FENCE_isSet(Flags1));

+                Expr IfGuard2 = Expr.And(P2, CLK_GLOBAL_MEM_FENCE_isSet(Flags2));

 

                 bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

-                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, NonLocalState.getGlobalVariables()), Token.NoToken), null, null),

+                    new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetAndHavocBlocks(1, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),

                     null));

                 bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(),

-                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, NonLocalState.getGlobalVariables()), Token.NoToken), null, null),

+                    new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetAndHavocBlocks(2, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null),

                     null));

             }

 

-            foreach (Variable v in NonLocalState.getAllNonLocalVariables())

+            foreach (Variable v in KernelArrayInfo.getAllNonLocalArrays())

             {

                 if (!ArrayModelledAdversarially(v))

                 {

@@ -1498,25 +1463,17 @@ namespace GPUVerify
 

             Expr AssumeGuard = Expr.Eq(v1, v2);

 

-            Expr EqualityCondition = Expr.True;

+            Expr EqualityCondition = ThreadsInSameGroup();

 

-            if (CommandLineOptions.InterGroupRaceChecking)

+            if (KernelArrayInfo.getGroupSharedArrays().Contains(v))

             {

-                EqualityCondition = ThreadsInSameGroup();

+                EqualityCondition = Expr.And(EqualityCondition,

+                    Expr.And(CLK_LOCAL_MEM_FENCE_isSet(Flags1), CLK_LOCAL_MEM_FENCE_isSet(Flags2)));

             }

-

-            if (CommandLineOptions.BarrierParameters)

+            else if (KernelArrayInfo.getGlobalArrays().Contains(v))

             {

-                if (NonLocalState.getGroupSharedVariables().Contains(v))

-                {

-                    EqualityCondition = Expr.And(EqualityCondition,

-                        Expr.And(CLK_LOCAL_MEM_FENCE_isSet(Flags1), CLK_LOCAL_MEM_FENCE_isSet(Flags2)));

-                }

-                else if (NonLocalState.getGlobalVariables().Contains(v))

-                {

-                    EqualityCondition = Expr.And(EqualityCondition,

-                        Expr.And(CLK_GLOBAL_MEM_FENCE_isSet(Flags1), CLK_GLOBAL_MEM_FENCE_isSet(Flags2)));

-                }

+                EqualityCondition = Expr.And(EqualityCondition,

+                    Expr.And(CLK_GLOBAL_MEM_FENCE_isSet(Flags1), CLK_GLOBAL_MEM_FENCE_isSet(Flags2)));

             }

 

             AssumeGuard = Expr.Imp(EqualityCondition, AssumeGuard);

@@ -1543,7 +1500,7 @@ namespace GPUVerify
 

             foreach (Declaration d in Program.TopLevelDeclarations)

             {

-                if (d is Variable && NonLocalState.Contains(d as Variable) && ArrayModelledAdversarially(d as Variable))

+                if (d is Variable && KernelArrayInfo.Contains(d as Variable) && ArrayModelledAdversarially(d as Variable))

                 {

                     continue;

                 }

@@ -1572,7 +1529,7 @@ namespace GPUVerify
 

             foreach (IdentifierExpr e in proc.Modifies)

             {

-                if (!NonLocalState.Contains(e.Decl) || !ArrayModelledAdversarially(e.Decl))

+                if (!KernelArrayInfo.Contains(e.Decl) || !ArrayModelledAdversarially(e.Decl))

                 {

                     NewModifies.Add(e);

                 }

@@ -1588,7 +1545,7 @@ namespace GPUVerify
 

             foreach (Variable v in impl.LocVars)

             {

-                Debug.Assert(!NonLocalState.getGroupSharedVariables().Contains(v));

+                Debug.Assert(!KernelArrayInfo.getGroupSharedArrays().Contains(v));

                 NewLocVars.Add(v);

             }

 

@@ -1631,7 +1588,7 @@ namespace GPUVerify
                     {

                         AssignLhs lhs = assign.Lhss[i];

                         Expr rhs = assign.Rhss[i];

-                        ReadCollector rc = new ReadCollector(NonLocalState);

+                        ReadCollector rc = new ReadCollector(KernelArrayInfo);

                         rc.Visit(rhs);

 

                         bool foundAdversarial = false;

@@ -1651,7 +1608,7 @@ namespace GPUVerify
                             continue;

                         }

 

-                        WriteCollector wc = new WriteCollector(NonLocalState);

+                        WriteCollector wc = new WriteCollector(KernelArrayInfo);

                         wc.Visit(lhs);

                         if (wc.GetAccess() != null && ArrayModelledAdversarially(wc.GetAccess().v))

                         {

@@ -1905,7 +1862,7 @@ namespace GPUVerify
                     {

                         Expr e = call.Ins[i];

 

-                        while (NonLocalAccessCollector.ContainsNonLocalAccess(e, NonLocalState))

+                        while (NonLocalAccessCollector.ContainsNonLocalAccess(e, KernelArrayInfo))

                         {

                             AssignCmd assignToTemp;

                             LocalVariable tempDecl;

@@ -1927,9 +1884,9 @@ namespace GPUVerify
                     AssignCmd assign = c as AssignCmd;

 

                     if (assign.Lhss.Zip(assign.Rhss, (lhs, rhs) =>

-                            !NonLocalAccessCollector.ContainsNonLocalAccess(rhs, NonLocalState) || 

-                              (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, NonLocalState) && 

-                                NonLocalAccessCollector.IsNonLocalAccess(rhs, NonLocalState))).All(b => b))

+                            !NonLocalAccessCollector.ContainsNonLocalAccess(rhs, KernelArrayInfo) || 

+                              (!NonLocalAccessCollector.ContainsNonLocalAccess(lhs, KernelArrayInfo) && 

+                                NonLocalAccessCollector.IsNonLocalAccess(rhs, KernelArrayInfo))).All(b => b))

                     {

                         result.simpleCmds.Add(c);

                     }

@@ -1969,7 +1926,7 @@ namespace GPUVerify
             if (bb.ec is WhileCmd)

             {

                 WhileCmd WhileCommand = bb.ec as WhileCmd;

-                while (NonLocalAccessCollector.ContainsNonLocalAccess(WhileCommand.Guard, NonLocalState))

+                while (NonLocalAccessCollector.ContainsNonLocalAccess(WhileCommand.Guard, KernelArrayInfo))

                 {

                     AssignCmd assignToTemp;

                     LocalVariable tempDecl;

@@ -1983,7 +1940,7 @@ namespace GPUVerify
             {

                 IfCmd IfCommand = bb.ec as IfCmd;

                 Debug.Assert(IfCommand.elseIf == null); // "else if" must have been eliminated by this phase

-                while (NonLocalAccessCollector.ContainsNonLocalAccess(IfCommand.Guard, NonLocalState))

+                while (NonLocalAccessCollector.ContainsNonLocalAccess(IfCommand.Guard, KernelArrayInfo))

                 {

                     AssignCmd assignToTemp;

                     LocalVariable tempDecl;

@@ -2008,7 +1965,7 @@ namespace GPUVerify
 

         private Expr PullOutNonLocalAccessesIntoTemps(BigBlock result, Expr e, Implementation impl)

         {

-            while (NonLocalAccessCollector.ContainsNonLocalAccess(e, NonLocalState))

+            while (NonLocalAccessCollector.ContainsNonLocalAccess(e, KernelArrayInfo))

             {

                 AssignCmd assignToTemp;

                 LocalVariable tempDecl;

@@ -2021,7 +1978,7 @@ namespace GPUVerify
 

         private Expr ExtractLocalAccessToTemp(Expr rhs, out AssignCmd tempAssignment, out LocalVariable tempDeclaration)

         {

-            NonLocalAccessExtractor extractor = new NonLocalAccessExtractor(TempCounter, NonLocalState);

+            NonLocalAccessExtractor extractor = new NonLocalAccessExtractor(TempCounter, KernelArrayInfo);

             TempCounter++;

             rhs = extractor.VisitExpr(rhs);

             tempAssignment = extractor.Assignment;

@@ -2059,7 +2016,7 @@ namespace GPUVerify
                 }

 

                 if (d is Variable && ((d as Variable).IsMutable || IsThreadLocalIdConstant(d as Variable)

-                    || (CommandLineOptions.InterGroupRaceChecking && IsGroupIdConstant(d as Variable) ) ))

+                    || IsGroupIdConstant(d as Variable) ))

                 {

                     NewTopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable((Variable)d.Clone()));

                     if (!QKeyValue.FindBoolAttribute(d.Attributes, "race_checking"))

@@ -2155,21 +2112,13 @@ namespace GPUVerify
                 return ErrorCount;

             }

 

-            if(!CommandLineOptions.BarrierParameters && BarrierProcedure.InParams.Length != 0)

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

             {

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

+                Error(BarrierProcedure, "Barrier procedure must take exactly one argument");

             }

-

-            if (CommandLineOptions.BarrierParameters)

+            else if (!BarrierProcedure.InParams[0].TypedIdent.Type.Equals(new BvType(32)))

             {

-                if (BarrierProcedure.InParams.Length != 1)

-                {

-                    Error(BarrierProcedure, "Barrier procedure must take exactly one argument");

-                }

-                else if (!BarrierProcedure.InParams[0].TypedIdent.Type.Equals(new BvType(32)))

-                {

-                    Error(BarrierProcedure, "Argument to barrier procedure must have type bv32");

-                }

+                Error(BarrierProcedure, "Argument to barrier procedure must have type bv32");

             }

 

             if (BarrierProcedure.OutParams.Length != 0)

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index d060ad8a..342c0539 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -123,13 +123,13 @@
     <Compile Include="EnabledToPredicateVisitor.cs" />

     <Compile Include="CommandLineOptions.cs" />

     <Compile Include="GPUVerifier.cs" />

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

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

     <Compile Include="IRaceInstrumenter.cs" />

     <Compile Include="Main.cs" />

     <Compile Include="NoConflictingAccessOptimiser.cs" />

     <Compile Include="NonLocalAccessCollector.cs" />

     <Compile Include="NonLocalAccessExtractor.cs" />

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

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

     <Compile Include="NullRaceInstrumenter.cs" />

     <Compile Include="Predicator.cs" />

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

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

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    interface IKernelArrayInfo

+    {

+

+        ICollection<Variable> getGlobalArrays();

+

+        ICollection<Variable> getGroupSharedArrays();

+

+        ICollection<Variable> getPrivateArrays();

+

+        ICollection<Variable> getAllNonLocalArrays();

+

+        ICollection<Variable> getAllArrays();

+

+        bool Contains(Variable v);

+

+    }

+}

diff --git a/Source/GPUVerify/INonLocalState.cs b/Source/GPUVerify/INonLocalState.cs
deleted file mode 100644
index c6211dab..00000000
--- a/Source/GPUVerify/INonLocalState.cs
+++ /dev/null
@@ -1,21 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using Microsoft.Boogie;

-

-namespace GPUVerify

-{

-    interface INonLocalState

-    {

-

-        ICollection<Variable> getGlobalVariables();

-

-        ICollection<Variable> getGroupSharedVariables();

-

-        ICollection<Variable> getAllNonLocalVariables();

-

-        bool Contains(Variable v);

-

-    }

-}

diff --git a/Source/GPUVerify/KernelArrayInfoLists.cs b/Source/GPUVerify/KernelArrayInfoLists.cs
new file mode 100644
index 00000000..7870e031
--- /dev/null
+++ b/Source/GPUVerify/KernelArrayInfoLists.cs
@@ -0,0 +1,60 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Boogie;

+using System.Diagnostics;

+

+namespace GPUVerify

+{

+    class KernelArrayInfoLists : IKernelArrayInfo

+    {

+        private List<Variable> GlobalVariables;

+        private List<Variable> GroupSharedVariables;

+        private List<Variable> PrivateVariables;

+

+        public KernelArrayInfoLists()

+        {

+            GlobalVariables = new List<Variable>();

+            GroupSharedVariables = new List<Variable>();

+            PrivateVariables = new List<Variable>();

+        }

+

+        public ICollection<Variable> getGlobalArrays()

+        {

+            return GlobalVariables;

+        }

+

+        public ICollection<Variable> getGroupSharedArrays()

+        {

+            return GroupSharedVariables;

+        }

+

+        public ICollection<Variable> getAllNonLocalArrays()

+        {

+            List<Variable> all = new List<Variable>();

+            all.AddRange(GlobalVariables);

+            all.AddRange(GroupSharedVariables);

+            return all;

+        }

+

+        public ICollection<Variable> getPrivateArrays()

+        {

+            return PrivateVariables;

+        }

+

+        public ICollection<Variable> getAllArrays()

+        {

+            List<Variable> all = new List<Variable>();

+            all.AddRange(getAllNonLocalArrays());

+            all.AddRange(PrivateVariables);

+            return all;

+        }

+

+        public bool Contains(Variable v)

+        {

+            return getAllNonLocalArrays().Contains(v);

+        }

+

+    }

+}

diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs
index 4bcce722..300089eb 100644
--- a/Source/GPUVerify/LoopInvariantGenerator.cs
+++ b/Source/GPUVerify/LoopInvariantGenerator.cs
@@ -166,7 +166,7 @@ namespace GPUVerify
 

                 if (CommandLineOptions.ArrayEqualities)

                 {

-                    foreach (Variable v in verifier.NonLocalState.getAllNonLocalVariables())

+                    foreach (Variable v in verifier.KernelArrayInfo.getAllNonLocalArrays())

                     {

                         if (!verifier.ArrayModelledAdversarially(v))

                         {

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index 7e64d2e4..e5a094d5 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -97,23 +97,23 @@ namespace GPUVerify
             ri.setVerifier(newGp);

 

             

-            Variable newG = findClonedVar(v, newGp.NonLocalState.getGlobalVariables());

-            Variable newT = findClonedVar(v, newGp.NonLocalState.getGroupSharedVariables());

+            Variable newG = findClonedVar(v, newGp.KernelArrayInfo.getGlobalArrays());

+            Variable newT = findClonedVar(v, newGp.KernelArrayInfo.getGroupSharedArrays());

             Contract.Assert(newG == null || newT == null);

 

-            ri.NonLocalStateToCheck.getGlobalVariables().Clear();

-            ri.NonLocalStateToCheck.getGroupSharedVariables().Clear();

+            ri.NonLocalStateToCheck.getGlobalArrays().Clear();

+            ri.NonLocalStateToCheck.getGroupSharedArrays().Clear();

             ri.onlyLog1 = a1;

             ri.onlyLog2 = a2;

 

             if (newG != null)

             {

-                ri.NonLocalStateToCheck.getGlobalVariables().Add(newG);

+                ri.NonLocalStateToCheck.getGlobalArrays().Add(newG);

             }

 

             if (newT != null)

             {

-                ri.NonLocalStateToCheck.getGroupSharedVariables().Add(newT);

+                ri.NonLocalStateToCheck.getGroupSharedArrays().Add(newT);

             }

             

             newGp.doit();

@@ -144,7 +144,7 @@ namespace GPUVerify
             {

                 bool FoundArray = CommandLineOptions.ArrayToCheck == null;

 

-                foreach (Variable v in g.NonLocalState.getAllNonLocalVariables())

+                foreach (Variable v in g.KernelArrayInfo.getAllNonLocalArrays())

                 {

                     if (CommandLineOptions.DividedAccesses)

                     {

diff --git a/Source/GPUVerify/NonLocalAccessCollector.cs b/Source/GPUVerify/NonLocalAccessCollector.cs
index 13d8f672..6a934899 100644
--- a/Source/GPUVerify/NonLocalAccessCollector.cs
+++ b/Source/GPUVerify/NonLocalAccessCollector.cs
@@ -12,14 +12,14 @@ namespace GPUVerify
     {

         public HashSet<Expr> Accesses = new HashSet<Expr>();

 

-        private INonLocalState NonLocalState;

+        private IKernelArrayInfo NonLocalState;

 

-        public NonLocalAccessCollector(INonLocalState NonLocalState)

+        public NonLocalAccessCollector(IKernelArrayInfo NonLocalState)

         {

             this.NonLocalState = NonLocalState;

         }

 

-        public static bool IsNonLocalAccess(Expr n, INonLocalState NonLocalState)

+        public static bool IsNonLocalAccess(Expr n, IKernelArrayInfo NonLocalState)

         {

             if (n is NAryExpr)

             {

@@ -48,7 +48,7 @@ namespace GPUVerify
             return false;

         }

 

-        public static bool ContainsNonLocalAccess(AssignLhs lhs, INonLocalState NonLocalState)

+        public static bool ContainsNonLocalAccess(AssignLhs lhs, IKernelArrayInfo NonLocalState)

         {

             NonLocalAccessCollector collector = new NonLocalAccessCollector(NonLocalState);

             if (lhs is SimpleAssignLhs)

@@ -63,7 +63,7 @@ namespace GPUVerify
             return collector.Accesses.Count > 0;

         }

 

-        public static bool ContainsNonLocalAccess(Expr rhs, INonLocalState NonLocalState)

+        public static bool ContainsNonLocalAccess(Expr rhs, IKernelArrayInfo NonLocalState)

         {

             NonLocalAccessCollector collector = new NonLocalAccessCollector(NonLocalState);

             collector.VisitExpr(rhs);

diff --git a/Source/GPUVerify/NonLocalAccessExtractor.cs b/Source/GPUVerify/NonLocalAccessExtractor.cs
index 553be683..412998e2 100644
--- a/Source/GPUVerify/NonLocalAccessExtractor.cs
+++ b/Source/GPUVerify/NonLocalAccessExtractor.cs
@@ -14,9 +14,9 @@ namespace GPUVerify
         public LocalVariable Declaration = null;

         public bool done = false;

 

-        private INonLocalState NonLocalState;

+        private IKernelArrayInfo NonLocalState;

 

-        public NonLocalAccessExtractor(int TempId, INonLocalState NonLocalState)

+        public NonLocalAccessExtractor(int TempId, IKernelArrayInfo NonLocalState)

         {

             this.TempId = TempId;

             this.NonLocalState = NonLocalState;

diff --git a/Source/GPUVerify/NonLocalStateLists.cs b/Source/GPUVerify/NonLocalStateLists.cs
deleted file mode 100644
index c47cddd5..00000000
--- a/Source/GPUVerify/NonLocalStateLists.cs
+++ /dev/null
@@ -1,45 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using Microsoft.Boogie;

-using System.Diagnostics;

-

-namespace GPUVerify

-{

-    class NonLocalStateLists : INonLocalState

-    {

-        private List<Variable> GlobalVariables;

-        private List<Variable> GroupSharedVariables;

-

-        public NonLocalStateLists()

-        {

-            GlobalVariables = new List<Variable>();

-            GroupSharedVariables = new List<Variable>();

-        }

-

-        public ICollection<Variable> getGlobalVariables()

-        {

-            return GlobalVariables;

-        }

-

-        public ICollection<Variable> getGroupSharedVariables()

-        {

-            return GroupSharedVariables;

-        }

-

-        public ICollection<Variable> getAllNonLocalVariables()

-        {

-            List<Variable> all = new List<Variable>();

-            all.AddRange(GlobalVariables);

-            all.AddRange(GroupSharedVariables);

-            return all;

-        }

-

-        public bool Contains(Variable v)

-        {

-            return getAllNonLocalVariables().Contains(v);

-        }

-

-    }

-}

diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
index b78730aa..1bf64023 100644
--- a/Source/GPUVerify/RaceInstrumenter.cs
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -13,7 +13,7 @@ namespace GPUVerify
     {

         protected GPUVerifier verifier;

 

-        public INonLocalState NonLocalStateToCheck;

+        public IKernelArrayInfo NonLocalStateToCheck;

 

         public int onlyLog1;

         public int onlyLog2;

@@ -35,14 +35,14 @@ namespace GPUVerify
         public void setVerifier(GPUVerifier verifier)

         {

             this.verifier = verifier;

-            NonLocalStateToCheck = new NonLocalStateLists();

-            foreach(Variable v in verifier.NonLocalState.getGlobalVariables())

+            NonLocalStateToCheck = new KernelArrayInfoLists();

+            foreach(Variable v in verifier.KernelArrayInfo.getGlobalArrays())

             {

-                NonLocalStateToCheck.getGlobalVariables().Add(v);

+                NonLocalStateToCheck.getGlobalArrays().Add(v);

             }

-            foreach(Variable v in verifier.NonLocalState.getGroupSharedVariables())

+            foreach(Variable v in verifier.KernelArrayInfo.getGroupSharedArrays())

             {

-                NonLocalStateToCheck.getGroupSharedVariables().Add(v);

+                NonLocalStateToCheck.getGroupSharedArrays().Add(v);

             }

         }

 

@@ -97,7 +97,7 @@ namespace GPUVerify
 

         public void AddRaceCheckingCandidateInvariants(Implementation impl, IRegion region)

         {

-            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())

             {

                 AddNoReadOrWriteCandidateInvariants(region, v);

                 AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(impl, region, v, "READ");

@@ -340,7 +340,7 @@ namespace GPUVerify
 

         public void AddKernelPrecondition()

         {

-            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())

             {

                 AddRequiresNoPendingAccess(v);

 

@@ -585,7 +585,7 @@ namespace GPUVerify
             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))

+            if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v))

             {

                 ResetReadAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetReadAssumeGuard);

                 ResetWriteAssumeGuard = Expr.Imp(verifier.ThreadsInSameGroup(), ResetWriteAssumeGuard);

@@ -627,16 +627,88 @@ namespace GPUVerify
 

         public void AddRaceCheckingCandidateRequires(Procedure Proc)

         {

-            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())

             {

                 AddNoReadOrWriteCandidateRequires(Proc, v);

                 AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Proc, v);

             }

+

+            DoHoudiniPointerAnalysis(Proc);

+

+        }

+

+        private void DoHoudiniPointerAnalysis(Procedure Proc)

+        {

+            HashSet<string> alreadyConsidered = new HashSet<string>();

+

+            foreach (Variable v in Proc.InParams)

+            {

+                string strippedVarName = GPUVerifier.StripThreadIdentifier(v.Name);

+                if (alreadyConsidered.Contains(strippedVarName))

+                {

+                    continue;

+                }

+                alreadyConsidered.Add(strippedVarName);

+                if (v.TypedIdent.Type is CtorType)

+                {

+                    CtorType ct = v.TypedIdent.Type as CtorType;

+                    if (ct.Decl.Name.Equals("ptr"))

+                    {

+                        foreach (var arrayCollection in new ICollection<Variable>[] { 

+                            verifier.KernelArrayInfo.getGlobalArrays(), verifier.KernelArrayInfo.getGroupSharedArrays(),

+                            verifier.KernelArrayInfo.getPrivateArrays() })

+                        {

+                            if (arrayCollection.Count == 0)

+                            {

+                                continue;

+                            }

+

+                            // This will need to be adapted to work with uniformity analysis

+                            foreach (string thread in new string[] { "1", "2" })

+                            {

+                                Expr DisjunctionOverPointerSet = null;

+                                foreach (var array in arrayCollection)

+                                {

+                                    Expr PointerSetDisjunct = Expr.Eq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array));

+                                    DisjunctionOverPointerSet = (DisjunctionOverPointerSet == null ? PointerSetDisjunct : Expr.Or(DisjunctionOverPointerSet, PointerSetDisjunct));

+                                    verifier.AddCandidateRequires(Proc,

+                                        Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),

+                                            Expr.Neq(MakePtrBaseExpr(v, strippedVarName, thread), MakeArrayIdExpr(array))));

+                                }

+                                Debug.Assert(DisjunctionOverPointerSet != null);

+                                verifier.AddCandidateRequires(Proc,

+                                    Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),

+                                             DisjunctionOverPointerSet));

+                                verifier.AddCandidateRequires(Proc,

+                                    Expr.Imp(new IdentifierExpr(Token.NoToken, "_P$" + thread, Microsoft.Boogie.Type.Bool),

+                                            Expr.Eq(MakePtrOffsetExpr(v, strippedVarName, thread), GPUVerifier.ZeroBV())));

+                            }

+                        }

+                    }

+                }

+            }

+        }

+

+        private static IdentifierExpr MakeArrayIdExpr(Variable array)

+        {

+            return new IdentifierExpr(Token.NoToken, "$arrayId" + array.Name, null);

+        }

+

+        private static NAryExpr MakePtrBaseExpr(Variable v, string strippedVarName, string thread)

+        {

+            return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "base#MKPTR", v.TypedIdent.Type)),

+                                                        new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));

+        }

+

+        private static NAryExpr MakePtrOffsetExpr(Variable v, string strippedVarName, string thread)

+        {

+            return new NAryExpr(Token.NoToken, new FunctionCall(new IdentifierExpr(Token.NoToken, "offset#MKPTR", v.TypedIdent.Type)),

+                                                        new ExprSeq(new Expr[] { new IdentifierExpr(Token.NoToken, strippedVarName + "$" + thread, v.TypedIdent.Type) }));

         }

 

         public void AddRaceCheckingCandidateEnsures(Procedure Proc)

         {

-            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())

             {

                 AddNoReadOrWriteCandidateEnsures(Proc, v);

                 AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Proc, v);

@@ -693,7 +765,7 @@ namespace GPUVerify
 

         public void AddRaceCheckingDeclarations()

         {

-            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

+            foreach (Variable v in NonLocalStateToCheck.getAllNonLocalArrays())

             {

                 AddRaceCheckingDecsAndProcsForVar(v);

             }

@@ -747,7 +819,7 @@ namespace GPUVerify
                         ));

                 }

 

-                if (verifier.NonLocalState.getGroupSharedVariables().Contains(v) && CommandLineOptions.InterGroupRaceChecking)

+                if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v))

                 {

                     WriteReadGuard = Expr.And(WriteReadGuard, verifier.ThreadsInSameGroup());

                 }

@@ -775,7 +847,7 @@ namespace GPUVerify
                         ));

                 }

 

-                if (verifier.NonLocalState.getGroupSharedVariables().Contains(v) && CommandLineOptions.InterGroupRaceChecking)

+                if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v))

                 {

                     WriteWriteGuard = Expr.And(WriteWriteGuard, verifier.ThreadsInSameGroup());

                 }

@@ -799,7 +871,7 @@ namespace GPUVerify
                         ));

                 }

 

-                if (verifier.NonLocalState.getGroupSharedVariables().Contains(v) && CommandLineOptions.InterGroupRaceChecking)

+                if (verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v))

                 {

                     ReadWriteGuard = Expr.And(ReadWriteGuard, verifier.ThreadsInSameGroup());

                 }

diff --git a/Source/GPUVerify/ReadCollector.cs b/Source/GPUVerify/ReadCollector.cs
index 53d9234e..c569b97e 100644
--- a/Source/GPUVerify/ReadCollector.cs
+++ b/Source/GPUVerify/ReadCollector.cs
@@ -17,7 +17,7 @@ namespace GPUVerify
 

         public List<AccessRecord> accesses = new List<AccessRecord>();

 

-        public ReadCollector(INonLocalState NonLocalState)

+        public ReadCollector(IKernelArrayInfo NonLocalState)

             : base(NonLocalState)

         {

         }

diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs
index ddaf2062..6e375945 100644
--- a/Source/GPUVerify/VariableDualiser.cs
+++ b/Source/GPUVerify/VariableDualiser.cs
@@ -36,7 +36,7 @@ namespace GPUVerify
                 return new IdentifierExpr(node.tok, new Constant(node.tok, DualiseTypedIdent(node.Decl)));

             }

 

-            if (CommandLineOptions.InterGroupRaceChecking && GPUVerifier.IsGroupIdConstant(node.Decl))

+            if (GPUVerifier.IsGroupIdConstant(node.Decl))

             {

                 return new IdentifierExpr(node.tok, new Constant(node.tok, DualiseTypedIdent(node.Decl)));

             }

@@ -58,7 +58,7 @@ namespace GPUVerify
         public override Variable VisitVariable(Variable node)

         {

             if (!(node is Constant) || GPUVerifier.IsThreadLocalIdConstant(node) ||

-                (CommandLineOptions.InterGroupRaceChecking && GPUVerifier.IsGroupIdConstant(node)))

+                GPUVerifier.IsGroupIdConstant(node))

             {

                 node.TypedIdent = DualiseTypedIdent(node);

                 node.Name = node.Name + "$" + id;

diff --git a/Source/GPUVerify/WriteCollector.cs b/Source/GPUVerify/WriteCollector.cs
index d55c5d05..00ca63c5 100644
--- a/Source/GPUVerify/WriteCollector.cs
+++ b/Source/GPUVerify/WriteCollector.cs
@@ -13,7 +13,7 @@ namespace GPUVerify
 

         private AccessRecord access = null;

 

-        public WriteCollector(INonLocalState NonLocalState)

+        public WriteCollector(IKernelArrayInfo NonLocalState)

             : base(NonLocalState)

         {

         }