GPUVerify: replace MayBe{ThreadConfigurationVariable,Gid}Analyser with simple functions based on VariableDefinitionAnalysis

This also unbreaks the stride race instrumentation for various subtle
reasons.

7 files changed, 157 insertions, 656 deletions

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 40e27310..5d693fa4 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -61,8 +61,6 @@ namespace GPUVerify
         public IRaceInstrumenter RaceInstrumenter;

 

         public UniformityAnalyser uniformityAnalyser;

-        public MayBeThreadConfigurationVariableAnalyser mayBeTidAnalyser;

-        public MayBeGidAnalyser mayBeGidAnalyser;

         public MayBeLocalIdPlusConstantAnalyser mayBeTidPlusConstantAnalyser;

         public MayBeGlobalIdPlusConstantAnalyser mayBeGidPlusConstantAnalyser;

         public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;

@@ -361,7 +359,7 @@ namespace GPUVerify
 

             DoUniformityAnalysis();

 

-            DoMayBeTidAnalysis();

+            DoVariableDefinitionAnalysis();

 

             DoMayBeIdPlusConstantAnalysis();

 

@@ -369,8 +367,6 @@ namespace GPUVerify
 

             DoArrayControlFlowAnalysis();

 

-            DoVariableDefinitionAnalysis();

-

             if (CommandLineOptions.ShowStages)

             {

                 emitProgram(outputFilename + "_preprocessed");

@@ -483,15 +479,6 @@ namespace GPUVerify
             mayBePowerOfTwoAnalyser.Analyse();

         }

 

-        private void DoMayBeTidAnalysis()

-        {

-            mayBeTidAnalyser = new MayBeThreadConfigurationVariableAnalyser(this);

-            mayBeTidAnalyser.Analyse();

-

-            mayBeGidAnalyser = new MayBeGidAnalyser(this);

-            mayBeGidAnalyser.Analyse();

-        }

-

         private void DoMayBeIdPlusConstantAnalysis()

         {

             mayBeTidPlusConstantAnalyser = new MayBeLocalIdPlusConstantAnalyser(this);

@@ -1040,15 +1027,29 @@ namespace GPUVerify
             return _GROUP_SIZE_Z != null;

         }

 

-        internal static string StripThreadIdentifier(string p)

+        internal static string StripThreadIdentifier(string p, out int id)

         {

-            if (p.Contains("$"))

+            if (p.EndsWith("$1"))

+            {

+                id = 1;

+                return p.Substring(0, p.Length - 2);

+            }

+            if (p.EndsWith("$2"))

             {

-                return p.Substring(0, p.LastIndexOf("$"));

+                id = 2;

+                return p.Substring(0, p.Length - 2);

             }

+

+            id = 0;

             return p;

         }

 

+        internal static string StripThreadIdentifier(string p)

+        {

+            int id;

+            return StripThreadIdentifier(p, out id);

+        }

+

         private void AddStartAndEndBarriers()

         {

             CallCmd FirstBarrier = new CallCmd(KernelImplementation.tok, BarrierProcedure.Name, new ExprSeq(), new IdentifierExprSeq());

@@ -2291,11 +2292,6 @@ namespace GPUVerify
             return !arrayControlFlowAnalyser.MayAffectControlFlow(v.Name);

         }

 

-        internal static Expr StripThreadIdentifiers(Expr e)

-        {

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

-        }

-

         internal Expr GlobalIdExpr(string dimension)

         {

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

@@ -2310,15 +2306,115 @@ namespace GPUVerify
           else

               return new StructuredRegion(Impl);

         }

-    }

 

-    class ThreadIdentifierStripper : StandardVisitor

-    {

-        public override Variable VisitVariable(Variable node)

+

+        public static bool IsGivenConstant(Expr e, Constant c)

+        {

+            if (!(e is IdentifierExpr))

+                return false;

+

+            var varName = ((IdentifierExpr)e).Decl.Name;

+            return (StripThreadIdentifier(varName) == StripThreadIdentifier(c.Name));

+        }

+

+        public bool SubstIsGivenConstant(Implementation impl, Expr e, Constant c)

+        {

+            if (!(e is IdentifierExpr))

+                return false;

+            e = varDefAnalyses[impl].SubstDefinitions(e, impl.Name);

+            return IsGivenConstant(e, c);

+        }

+

+        public Constant GetLocalIdConst(int dim)

+        {

+            switch (dim)

+            {

+                case 0:  return _X;

+                case 1:  return _Y;

+                case 2:  return _Z;

+                default: Debug.Assert(false);

+                         return null;

+            }

+        }

+

+        public Constant GetGroupIdConst(int dim)

+        {

+            switch (dim)

+            {

+                case 0:  return _GROUP_X;

+                case 1:  return _GROUP_Y;

+                case 2:  return _GROUP_Z;

+                default: Debug.Assert(false);

+                         return null;

+            }

+        }

+

+        public Constant GetGroupSizeConst(int dim)

+        {

+            switch (dim)

+            {

+                case 0:  return _GROUP_SIZE_X;

+                case 1:  return _GROUP_SIZE_Y;

+                case 2:  return _GROUP_SIZE_Z;

+                default: Debug.Assert(false);

+                         return null;

+            }

+        }

+

+        public bool IsLocalId(Expr e, int dim, Implementation impl)

         {

-            node.Name = GPUVerifier.StripThreadIdentifier(node.Name);

-            return base.VisitVariable(node);

+            return SubstIsGivenConstant(impl, e, GetLocalIdConst(dim));

+        }

+

+        public bool IsGlobalId(Expr e, int dim, Implementation impl)

+        {

+            e = varDefAnalyses[impl].SubstDefinitions(e, impl.Name);

+

+            if (e is NAryExpr && (e as NAryExpr).Fun.FunctionName.Equals("BV32_ADD"))

+            {

+                NAryExpr nary = e as NAryExpr;

+                Constant localId = GetLocalIdConst(dim);

+

+                if (IsGivenConstant(nary.Args[1], localId))

+                {

+                    return IsGroupIdTimesGroupSize(nary.Args[0], dim);

+                }

+

+                if (IsGivenConstant(nary.Args[0], localId))

+                {

+                    return IsGroupIdTimesGroupSize(nary.Args[1], dim);

+                }

+            }

+

+            return false;

         }

+

+        private bool IsGroupIdTimesGroupSize(Expr expr, int dim)

+        {

+            if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))

+            {

+                NAryExpr innerNary = expr as NAryExpr;

+

+                if (IsGroupIdAndSize(dim, innerNary.Args[0], innerNary.Args[1]))

+                {

+                    return true;

+                }

+

+                if (IsGroupIdAndSize(dim, innerNary.Args[1], innerNary.Args[0]))

+                {

+                    return true;

+                }

+            }

+            return false;

+        }

+

+        private bool IsGroupIdAndSize(int dim, Expr maybeGroupId, Expr maybeGroupSize)

+        {

+            return IsGivenConstant(maybeGroupId, GetGroupIdConst(dim)) &&

+                   IsGivenConstant(maybeGroupSize, GetGroupSizeConst(dim));

+        }

+

+

     }

 

 }

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index eba91cd2..6762e634 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -113,13 +113,11 @@
     <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />

     <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />

     <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />

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

     <Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />

     <Compile Include="KernelDualiser.cs" />

     <Compile Include="LiveVariableAnalyser.cs" />

     <Compile Include="LoopInvariantGenerator.cs" />

     <Compile Include="MayBePowerOfTwoAnalyser.cs" />

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

     <Compile Include="MayBeIdPlusConstantAnalyser.cs" />

     <Compile Include="StructuredProgramVisitor.cs" />

     <Compile Include="CrossThreadInvariantProcessor.cs" />

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

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Diagnostics;

-using Microsoft.Boogie;

-

-namespace GPUVerify

-{

-    class MayBeGidAnalyser : MayBeAnalyser

-    {

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

-

-        private GPUVerifier verifier;

-

-        private bool ProcedureChanged;

-

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

-

-        public MayBeGidAnalyser(GPUVerifier verifier)

-        {

-            this.verifier = verifier;

-

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

-            foreach (string s in dimensions)

-            {

-                mayBeInfo[s] = new Dictionary<string, Dictionary<string, bool>>();

-            }

-        

-        }

-

-        internal void Analyse()

-        {

-            foreach (Declaration D in verifier.Program.TopLevelDeclarations)

-            {

-                if(D is Implementation)

-                {

-                    Implementation Impl = D as Implementation;

-

-                    foreach (string s in dimensions)

-                    {

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

-                    }

-

-                    foreach (Variable v in Impl.LocVars)

-                    {

-                        foreach (string s in dimensions)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    foreach (Variable v in Impl.InParams)

-                    {

-                        foreach (string s in dimensions)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    foreach (Variable v in Impl.OutParams)

-                    {

-                        foreach (string s in dimensions)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    ProcedureChanged = true;

-                }

-            }

-

-            while (ProcedureChanged)

-            {

-                ProcedureChanged = false;

-

-                foreach (Declaration D in verifier.Program.TopLevelDeclarations)

-                {

-                    if (D is Implementation)

-                    {

-                        Implementation Impl = D as Implementation;

-                        Analyse(Impl);

-                    }

-                }

-            }

-

-            if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)

-            {

-                dump();

-            }

-        }

-

-        private void Analyse(Implementation Impl)

-        {

-            Analyse(Impl, verifier.RootRegion(Impl));

-        }

-

-        private void Analyse(Implementation impl, IRegion region)

-        {

-            foreach (Cmd c in region.Cmds())

-            {

-                if (c is AssignCmd)

-                {

-                    foreach (string s in dimensions)

-                    {

-                        TransferAssign(impl, c as AssignCmd, s);

-                    }

-                }

-                else if (c is CallCmd)

-                {

-                    foreach (string s in dimensions)

-                    {

-                        TransferCall(impl, c as CallCmd, s);

-                    }

-                }

-                else if (c is HavocCmd)

-                {

-                    foreach (string s in dimensions)

-                    {

-                        TransferHavoc(impl, c as HavocCmd, s);

-                    }

-                }

-            }

-        }

-

-        private void TransferHavoc(Implementation impl, HavocCmd havoc, string component)

-        {

-            Debug.Assert(havoc.Vars.Length == 1);

-            if (MayBe(component, impl.Name, havoc.Vars[0].Decl.Name))

-            {

-                SetNot(component, impl.Name, havoc.Vars[0].Decl.Name);

-            }

-        }

-

-        private void TransferCall(Implementation impl, CallCmd callCmd, string component)

-        {

-            if (callCmd.callee != verifier.BarrierProcedure.Name)

-            {

-

-                Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);

-                for (int i = 0; i < CalleeImplementation.InParams.Length; i++)

-                {

-                    if (MayBe(component, callCmd.callee, CalleeImplementation.InParams[i].Name)

-                        && !MayBe(component, impl.Name, callCmd.Ins[i]))

-                    {

-                        SetNot(component, callCmd.callee, CalleeImplementation.InParams[i].Name);

-                    }

-                }

-

-                for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)

-                {

-                    if (MayBe(component, impl.Name, callCmd.Outs[i].Name)

-                        && !MayBe(component, callCmd.callee, CalleeImplementation.OutParams[i].Name))

-                    {

-                        SetNot(component, impl.Name, callCmd.Outs[i].Name);

-                    }

-                }

-

-            }

-        }

-

-        private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)

-        {

-            for (int i = 0; i != assignCmd.Lhss.Count; ++i)

-            {

-                if (assignCmd.Lhss[i] is SimpleAssignLhs)

-                {

-                    SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;

-                    Expr rhs = assignCmd.Rhss[i];

-

-                    if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

-                        && !MayBe(component, impl.Name, rhs))

-                    {

-                        SetNot(component, impl.Name, lhs.AssignedVariable.Name);

-                    }

-                }

-            }

-        }

-

-        private void SetNot(string component, string proc, string v)

-        {

-            mayBeInfo[component][proc][v] = false;

-            ProcedureChanged = true;

-        }

-

-        private void SetMayBe(string component, string proc, string v)

-        {

-            mayBeInfo[component][proc][v] = true;

-        }

-

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

-        {

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

-            {

-                return false;

-            }

-

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

-            {

-                return false;

-            }

-

-            return mayBeInfo[component][proc][v];

-        }

-

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

-        {

-            if (e is IdentifierExpr)

-            {

-                return MayBe(component, proc, (e as IdentifierExpr).Decl.Name);

-            }

-

-            if (e is NAryExpr && (e as NAryExpr).Fun.FunctionName.Equals("BV32_ADD"))

-            {

-                NAryExpr nary = e as NAryExpr;

-

-                string localIdString = null;

-

-                if (component.Equals("x"))

-                {

-                    localIdString = GPUVerifier.LOCAL_ID_X_STRING;

-                }

-                else if (component.Equals("y"))

-                {

-                    localIdString = GPUVerifier.LOCAL_ID_Y_STRING;

-                }

-                else if (component.Equals("z"))

-                {

-                    localIdString = GPUVerifier.LOCAL_ID_Z_STRING;

-                }

-                else

-                {

-                    Debug.Assert(false);

-                }

-

-                if(verifier.mayBeTidAnalyser.MayBe(localIdString, proc, nary.Args[1]))

-                {

-                    return IsGroupIdTimesGroupSize(component, proc, nary.Args[0]);

-                }

-

-                if (verifier.mayBeTidAnalyser.MayBe(localIdString, proc, nary.Args[0]))

-                {

-                    return IsGroupIdTimesGroupSize(component, proc, nary.Args[1]);

-                }

-            }

-

-            return false;

-        }

-

-        private bool IsGroupIdTimesGroupSize(string component, string proc, Expr expr)

-        {

-            if (expr is NAryExpr && (expr as NAryExpr).Fun.FunctionName.Equals("BV32_MUL"))

-            {

-                NAryExpr innerNary = expr as NAryExpr;

-

-                if (IsGroupIdAndSize(component, proc, innerNary.Args[0], innerNary.Args[1]))

-                {

-                    return true;

-                }

-

-                if (IsGroupIdAndSize(component, proc, innerNary.Args[1], innerNary.Args[0]))

-                {

-                    return true;

-                }

-            }

-            return false;

-        }

-

-        private bool IsGroupIdAndSize(string component, string proc, Expr maybeGroupId, Expr maybeGroupSize)

-        {

-            string groupIdString = null;

-            string groupSizeString = null;

-            if (component.Equals("x"))

-            {

-                groupIdString = GPUVerifier.GROUP_ID_X_STRING;

-                groupSizeString = GPUVerifier.GROUP_SIZE_X_STRING;

-            }

-            else if (component.Equals("y"))

-            {

-                groupIdString = GPUVerifier.GROUP_ID_Y_STRING;

-                groupSizeString = GPUVerifier.GROUP_SIZE_Y_STRING;

-            }

-            else if (component.Equals("z"))

-            {

-                groupIdString = GPUVerifier.GROUP_ID_Z_STRING;

-                groupSizeString = GPUVerifier.GROUP_SIZE_Z_STRING;

-            }

-            else

-            {

-                Debug.Assert(false);

-            }

-

-            return verifier.mayBeTidAnalyser.MayBe(groupIdString, proc, maybeGroupId) &&

-                                       verifier.mayBeTidAnalyser.MayBe(groupSizeString, proc, maybeGroupSize);

-        }

-

-        private void dump()

-        {

-            foreach (string s in dimensions)

-            {

-                Console.WriteLine("*** global_id_" + s + " ***");

-

-                foreach (string p in mayBeInfo[s].Keys)

-                {

-                    Console.WriteLine("  Procedure " + p);

-

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

-                    {

-                        if (mayBeInfo[s][p][v])

-                        {

-                            Console.WriteLine("    " + v + ": may be global_id_" + s);

-                        }

-                    }

-                }

-            }

-

-        }

-

-    }

-}

diff --git a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
index a57f35ee..3ee8edc8 100644
--- a/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
+++ b/Source/GPUVerify/MayBeIdPlusConstantAnalyser.cs
@@ -11,8 +11,6 @@ namespace GPUVerify
     {

         protected GPUVerifier verifier;

 

-        protected MayBeAnalyser mayBeAnalyser;

-

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

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

 

@@ -104,7 +102,7 @@ namespace GPUVerify
 

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

 

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

+                                    if (IsId(assign.Rhss[i], impl))

                                     {

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

                                     }

@@ -128,6 +126,7 @@ namespace GPUVerify
             }

         }

 

+

         private string ConvertToString(Expr constantIncrement)

         {

             if (constantIncrement is IdentifierExpr)

@@ -217,7 +216,7 @@ namespace GPUVerify
 

         internal abstract string idKind();

 

-        protected abstract string ComponentString();

+        protected abstract bool IsId(Expr expr, Implementation impl);

 

         internal Expr GetIncrement(string p, string v)

         {

@@ -260,7 +259,11 @@ namespace GPUVerify
 

         internal MayBeLocalIdPlusConstantAnalyser(GPUVerifier verifier) : base(verifier)

         {

-            mayBeAnalyser = verifier.mayBeTidAnalyser;

+        }

+

+        protected override bool IsId(Expr expr, Implementation impl)

+        {

+            return verifier.IsLocalId(expr, 0, impl);

         }

 

         override internal Expr MakeIdExpr()

@@ -272,11 +275,6 @@ namespace GPUVerify
         {

             return "local id";

         }

-

-        protected override string ComponentString()

-        {

-            return GPUVerifier.LOCAL_ID_X_STRING;

-        }

     }

 

     class MayBeGlobalIdPlusConstantAnalyser : MayBeIdPlusConstantAnalyser

@@ -284,7 +282,11 @@ namespace GPUVerify
         internal MayBeGlobalIdPlusConstantAnalyser(GPUVerifier verifier)

             : base(verifier)

         {

-            mayBeAnalyser = verifier.mayBeGidAnalyser;

+        }

+

+        protected override bool IsId(Expr expr, Implementation impl)

+        {

+            return verifier.IsGlobalId(expr, 0, impl);

         }

 

         internal override string idKind()

@@ -296,12 +298,6 @@ namespace GPUVerify
         {

             return verifier.GlobalIdExpr("X");

         }

-

-        protected override string ComponentString()

-        {

-            return "x";

-        }

-

     }

 

 

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

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Diagnostics;

-using Microsoft.Boogie;

-

-namespace GPUVerify

-{

-    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,

-            GPUVerifier.LOCAL_ID_Y_STRING,

-            GPUVerifier.LOCAL_ID_Z_STRING,

-            GPUVerifier.GROUP_ID_X_STRING,

-            GPUVerifier.GROUP_ID_Y_STRING,

-            GPUVerifier.GROUP_ID_Z_STRING,

-            GPUVerifier.NUM_GROUPS_X_STRING,

-            GPUVerifier.NUM_GROUPS_Y_STRING,

-            GPUVerifier.NUM_GROUPS_Z_STRING,

-            GPUVerifier.GROUP_SIZE_X_STRING,

-            GPUVerifier.GROUP_SIZE_Y_STRING,

-            GPUVerifier.GROUP_SIZE_Z_STRING

-        };

-

-        private GPUVerifier verifier;

-

-        private bool ProcedureChanged;

-

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

-

-        public MayBeThreadConfigurationVariableAnalyser(GPUVerifier verifier)

-        {

-            this.verifier = verifier;

-

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

-            foreach (string s in SpecialNames)

-            {

-                mayBeInfo[s] = new Dictionary<string, Dictionary<string, bool>>();

-            }

-        

-        }

-

-        internal void Analyse()

-        {

-            foreach (Declaration D in verifier.Program.TopLevelDeclarations)

-            {

-                if(D is Implementation)

-                {

-                    Implementation Impl = D as Implementation;

-

-                    foreach (string s in SpecialNames)

-                    {

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

-                    }

-

-                    SetMayBe(GPUVerifier.LOCAL_ID_X_STRING, Impl.Name, GPUVerifier._X.Name);

-                    SetMayBe(GPUVerifier.LOCAL_ID_Y_STRING, Impl.Name, GPUVerifier._Y.Name);

-                    SetMayBe(GPUVerifier.LOCAL_ID_Z_STRING, Impl.Name, GPUVerifier._Z.Name);

-

-                    SetMayBe(GPUVerifier.GROUP_ID_X_STRING, Impl.Name, GPUVerifier._GROUP_X.Name);

-                    SetMayBe(GPUVerifier.GROUP_ID_Y_STRING, Impl.Name, GPUVerifier._GROUP_Y.Name);

-                    SetMayBe(GPUVerifier.GROUP_ID_Z_STRING, Impl.Name, GPUVerifier._GROUP_Z.Name);

-

-                    SetMayBe(GPUVerifier.GROUP_SIZE_X_STRING, Impl.Name, GPUVerifier._GROUP_SIZE_X.Name);

-                    SetMayBe(GPUVerifier.GROUP_SIZE_Y_STRING, Impl.Name, GPUVerifier._GROUP_SIZE_Y.Name);

-                    SetMayBe(GPUVerifier.GROUP_SIZE_Z_STRING, Impl.Name, GPUVerifier._GROUP_SIZE_Z.Name);

-

-                    SetMayBe(GPUVerifier.NUM_GROUPS_X_STRING, Impl.Name, GPUVerifier._NUM_GROUPS_X.Name);

-                    SetMayBe(GPUVerifier.NUM_GROUPS_Y_STRING, Impl.Name, GPUVerifier._NUM_GROUPS_Y.Name);

-                    SetMayBe(GPUVerifier.NUM_GROUPS_Z_STRING, Impl.Name, GPUVerifier._NUM_GROUPS_Z.Name);

-

-                    foreach (Variable v in Impl.LocVars)

-                    {

-                        foreach (string s in SpecialNames)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    foreach (Variable v in Impl.InParams)

-                    {

-                        foreach (string s in SpecialNames)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    foreach (Variable v in Impl.OutParams)

-                    {

-                        foreach (string s in SpecialNames)

-                        {

-                            SetMayBe(s, Impl.Name, v.Name);

-                        }

-                    }

-

-                    ProcedureChanged = true;

-                }

-            }

-

-            while (ProcedureChanged)

-            {

-                ProcedureChanged = false;

-

-                foreach (Declaration D in verifier.Program.TopLevelDeclarations)

-                {

-                    if (D is Implementation)

-                    {

-                        Implementation Impl = D as Implementation;

-                        Analyse(Impl);

-                    }

-                }

-            }

-

-            if (CommandLineOptions.ShowMayBeThreadConfigurationVariableAnalysis)

-            {

-                dump();

-            }

-        }

-

-        private void Analyse(Implementation Impl)

-        {

-            Analyse(Impl, verifier.RootRegion(Impl));

-        }

-

-        private void Analyse(Implementation impl, IRegion region)

-        {

-            foreach (Cmd c in region.Cmds())

-            {

-                if (c is AssignCmd)

-                {

-                    foreach (string s in SpecialNames)

-                    {

-                        TransferAssign(impl, c as AssignCmd, s);

-                    }

-                }

-                else if (c is CallCmd)

-                {

-                    foreach (string s in SpecialNames)

-                    {

-                        TransferCall(impl, c as CallCmd, s);

-                    }

-                }

-                else if (c is HavocCmd)

-                {

-                    foreach (string s in SpecialNames)

-                    {

-                        TransferHavoc(impl, c as HavocCmd, s);

-                    }

-                }

-            }

-        }

-

-        private void TransferHavoc(Implementation impl, HavocCmd havoc, string component)

-        {

-            Debug.Assert(havoc.Vars.Length == 1);

-            if (MayBe(component, impl.Name, havoc.Vars[0].Decl.Name))

-            {

-                SetNot(component, impl.Name, havoc.Vars[0].Decl.Name);

-            }

-        }

-

-        private void TransferCall(Implementation impl, CallCmd callCmd, string component)

-        {

-            if (callCmd.callee != verifier.BarrierProcedure.Name)

-            {

-

-                Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee);

-                for (int i = 0; i < CalleeImplementation.InParams.Length; i++)

-                {

-                    if (MayBe(component, callCmd.callee, CalleeImplementation.InParams[i].Name)

-                        && !MayBe(component, impl.Name, callCmd.Ins[i]))

-                    {

-                        SetNot(component, callCmd.callee, CalleeImplementation.InParams[i].Name);

-                    }

-                }

-

-                for (int i = 0; i < CalleeImplementation.OutParams.Length; i++)

-                {

-                    if (MayBe(component, impl.Name, callCmd.Outs[i].Name)

-                        && !MayBe(component, callCmd.callee, CalleeImplementation.OutParams[i].Name))

-                    {

-                        SetNot(component, impl.Name, callCmd.Outs[i].Name);

-                    }

-                }

-

-            }

-        }

-

-        private void TransferAssign(Implementation impl, AssignCmd assignCmd, string component)

-        {

-            for (int i = 0; i != assignCmd.Lhss.Count; ++i)

-            {

-                if (assignCmd.Lhss[i] is SimpleAssignLhs)

-                {

-                    SimpleAssignLhs lhs = assignCmd.Lhss[i] as SimpleAssignLhs;

-                    Expr rhs = assignCmd.Rhss[i];

-

-                    if (MayBe(component, impl.Name, lhs.AssignedVariable.Name)

-                        && !MayBe(component, impl.Name, rhs))

-                    {

-                        SetNot(component, impl.Name, lhs.AssignedVariable.Name);

-                    }

-                }

-            }

-        }

-

-        private void SetNot(string component, string proc, string v)

-        {

-            mayBeInfo[component][proc][v] = false;

-            ProcedureChanged = true;

-        }

-

-        private void SetMayBe(string component, string proc, string v)

-        {

-            mayBeInfo[component][proc][v] = true;

-        }

-

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

-        {

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

-            {

-                return false;

-            }

-

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

-            {

-                return false;

-            }

-

-            return mayBeInfo[component][proc][v];

-        }

-

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

-        {

-            if (e is IdentifierExpr)

-            {

-                return MayBe(component, proc, (e as IdentifierExpr).Decl.Name);

-            }

-            return false;

-        }

-

-        private void dump()

-        {

-            foreach (string s in SpecialNames)

-            {

-                Console.WriteLine("*** " + s + " ***");

-

-                foreach (string p in mayBeInfo[s].Keys)

-                {

-                    Console.WriteLine("  Procedure " + p);

-

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

-                    {

-                        if (mayBeInfo[s][p][v])

-                        {

-                            Console.WriteLine("    " + v + ": may be " + s);

-                        }

-                    }

-                }

-            }

-

-        }

-

-    }

-}

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 13a4585b..585ca433 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -242,10 +242,10 @@ namespace GPUVerify
         {

             if (local)

             {

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

+                return verifier.IsLocalId(mayBeId, 0, impl);

             }

 

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

+            return verifier.IsGlobalId(mayBeId, 0, impl);

         }

 

         private bool TryGenerateCandidateForReducedStrengthStrideVariable(Implementation impl, IRegion region, Variable v, Expr e, string accessKind)

@@ -453,7 +453,7 @@ namespace GPUVerify
         private void AddReadOrWrittenOffsetIsThreadIdCandidateInvariants(Implementation impl, IRegion region, Variable v, string accessType)

         {

             var offsets = GetOffsetsAccessed(region, v, accessType)

-               .Select(ofs => verifier.varDefAnalyses[impl].SubstDualisedDefinitions(ofs, 1, impl.Name))

+               .Select(ofs => verifier.varDefAnalyses[impl].SubstDefinitions(ofs, impl.Name))

                .ToList();

 

             if (offsets.Count != 0 && !offsets.Contains(null))

@@ -520,8 +520,8 @@ namespace GPUVerify
             }

 

             return

-                (SameConstant(nary.Args[0], constant) && verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, nary.Args[1])) ||

-                (SameConstant(nary.Args[1], constant) && verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_X_STRING, impl.Name, nary.Args[0]));

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

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

         }

 

 

@@ -558,8 +558,8 @@ namespace GPUVerify
             }

 

             return

-                (SameConstant(nary.Args[0], constant) && verifier.mayBeGidAnalyser.MayBe("x", impl.Name, nary.Args[1])) ||

-                (SameConstant(nary.Args[1], constant) && verifier.mayBeGidAnalyser.MayBe("x", impl.Name, nary.Args[0]));

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

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

         }

 

 

diff --git a/Source/GPUVerify/VariableDefinitionAnalysis.cs b/Source/GPUVerify/VariableDefinitionAnalysis.cs
index 714fcc15..5c04a6f8 100644
--- a/Source/GPUVerify/VariableDefinitionAnalysis.cs
+++ b/Source/GPUVerify/VariableDefinitionAnalysis.cs
@@ -111,31 +111,35 @@ class VariableDefinitionAnalysis {
         BuildNamedDefFor(v);

   }

 

-  private class SubstDualisedDefVisitor : Duplicator {

+  private class SubstDefVisitor : Duplicator {

     private VariableDefinitionAnalysis analysis;

-    private VariableDualiser dualiser;

+    private string procName;

     public bool isSubstitutable = true;

 

-    public SubstDualisedDefVisitor(VariableDefinitionAnalysis a, int id, string procName) {

+    public SubstDefVisitor(VariableDefinitionAnalysis a, string p) {

       analysis = a;

-      dualiser = new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName);

+      procName = p;

     }

 

     public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

       if (expr.Decl is Constant)

-        return dualiser.VisitIdentifierExpr(expr);

-      var varName = GPUVerifier.StripThreadIdentifier(expr.Decl.Name);

+        return expr;

+      int id;

+      var varName = GPUVerifier.StripThreadIdentifier(expr.Decl.Name, out id);

       Expr def;

       if (!analysis.namedDefMap.TryGetValue(varName, out def)) {

         isSubstitutable = false;

         return null;

       }

-      return (Expr)dualiser.Visit(def.Clone());

+      if (id == 0)

+        return def;

+      else

+        return (Expr)new VariableDualiser(id, analysis.verifier.uniformityAnalyser, procName).Visit(def.Clone());

     }

   }

 

-  public Expr SubstDualisedDefinitions(Expr e, int id, string procName) {

-    var v = new SubstDualisedDefVisitor(this, id, procName);

+  public Expr SubstDefinitions(Expr e, string procName) {

+    var v = new SubstDefVisitor(this, procName);

     Expr result = (Expr)v.Visit(e.Clone());

     if (!v.isSubstitutable)

       return null;