GPUVerify: implement is-a-constant analysis

This analysis is used to generate race checking invariants for
arbitrary (thread-level) constant offsets, in place of invariant
generators for four specific constants (thread-id, global-id, 2D
thread-id and 2D global-id) which are subsumed by the new analysis.
The main motivation is to be able to recognise offsets used by
word level accesses into byte arrays, which are formed from linear
combinations of thread IDs and constants.

This change allows us to remove the 2D and global size analyses,
resulting in a 536-line net reduction in total code size.

10 files changed, 204 insertions, 745 deletions

diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
index 3cd29367..cb880767 100644
--- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
@@ -205,16 +205,16 @@ namespace GPUVerify
         }

 

 

-        protected override void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)

+        protected override void AddAccessedOffsetsAreConstantCandidateInvariant(IRegion region, Variable v, IEnumerable<Expr> offsets, string ReadOrWrite)

         {

-            Expr expr = AccessedOffsetIsThreadGlobalIdExpr(v, ReadOrWrite, 1);

-            verifier.AddCandidateInvariant(region, expr, "accessed offset is global id");

+            Expr expr = AccessedOffsetsAreConstantExpr(v, offsets, ReadOrWrite, 1);

+            verifier.AddCandidateInvariant(region, expr, "accessed offsets are constant");

         }

 

-        protected override void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)

-        {

-            Expr expr = AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, 1);

-            verifier.AddCandidateInvariant(region, expr, "accessed offset is local id");

+        private Expr AccessedOffsetsAreConstantExpr(Variable v, IEnumerable<Expr> offsets, string ReadOrWrite, int Thread) {

+            return Expr.Imp(

+                    new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),

+                    offsets.Select(ofs => (Expr)Expr.Eq(new IdentifierExpr(Token.NoToken, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))), ofs)).Aggregate(Expr.Or));

         }

 

         private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread)

@@ -250,61 +250,6 @@ namespace GPUVerify
             return new VariableDualiser(Thread, null, null).VisitExpr(verifier.GlobalIdExpr(dimension).Clone() as Expr);

         }

 

-        private Expr GlobalSizeExpr(string dimension)

-        {

-            return GPUVerifier.MakeBitVectorBinaryBitVector("BV32_MUL",

-                            new IdentifierExpr(Token.NoToken, verifier.GetNumGroups(dimension)), 

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

-        }

-

-        protected override void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)

-        {

-            Expr expr = AccessedOffsetIsThreadFlattened2DLocalIdExpr(v, ReadOrWrite, 1);

-            verifier.AddCandidateInvariant(region, expr, "accessed offset is flattened 2D local id");

-        }

-

-        private Expr AccessedOffsetIsThreadFlattened2DLocalIdExpr(Variable v, string ReadOrWrite, int Thread)

-        {

-            Expr expr = null;

-            if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))

-            {

-                expr = Expr.Imp(

-                        AccessHasOccurred(v, ReadOrWrite, Thread),

-                        Expr.Eq(

-                            new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))),

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

-                            new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)), new IdentifierExpr(v.tok, verifier.GetGroupSize("X"))),

-                                new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread)))

-                            )

-                            );

-            }

-            return expr;

-        }

-

-        protected override void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite)

-        {

-            Expr expr = AccessedOffsetIsThreadFlattened2DGlobalIdExpr(v, ReadOrWrite, 1);

-            verifier.AddCandidateInvariant(region, expr, "accessed offset is flattened 2D global id");

-        }

-

-        private Expr AccessedOffsetIsThreadFlattened2DGlobalIdExpr(Variable v, string ReadOrWrite, int Thread)

-        {

-            Expr expr = null;

-            if (GPUVerifier.HasXDimension(v) && GPUVerifier.IndexTypeOfXDimension(v).Equals(verifier.GetTypeOfIdX()))

-            {

-                expr = Expr.Imp(

-                        AccessHasOccurred(v, ReadOrWrite, Thread),

-                        Expr.Eq(

-                            new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))),

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

-                            GlobalIdExpr("Y", Thread), GlobalSizeExpr("X")),

-                                GlobalIdExpr("X", Thread))

-                            )

-                            );

-            }

-            return expr;

-        }

-

         protected override void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite)

         {

             Expr expr = MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 1);

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index a49461c7..1839b138 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -64,13 +64,12 @@ namespace GPUVerify
         public UniformityAnalyser uniformityAnalyser;

         public MayBeThreadConfigurationVariableAnalyser mayBeTidAnalyser;

         public MayBeGidAnalyser mayBeGidAnalyser;

-        public MayBeGlobalSizeAnalyser mayBeGlobalSizeAnalyser;

-        public MayBeFlattened2DTidOrGidAnalyser mayBeFlattened2DTidOrGidAnalyser;

         public MayBeLocalIdPlusConstantAnalyser mayBeTidPlusConstantAnalyser;

         public MayBeGlobalIdPlusConstantAnalyser mayBeGidPlusConstantAnalyser;

         public MayBePowerOfTwoAnalyser mayBePowerOfTwoAnalyser;

         public LiveVariableAnalyser liveVariableAnalyser;

         public ArrayControlFlowAnalyser arrayControlFlowAnalyser;

+        public Dictionary<Implementation, VariableDefinitionAnalysis> varDefAnalyses;

 

         public GPUVerifier(string filename, Program program, ResolutionContext rc, IRaceInstrumenter raceInstrumenter) : this(filename, program, rc, raceInstrumenter, false)

         {

@@ -371,6 +370,8 @@ namespace GPUVerify
 

             DoArrayControlFlowAnalysis();

 

+            DoVariableDefinitionAnalysis();

+

             if (CommandLineOptions.ShowStages)

             {

                 emitProgram(outputFilename + "_preprocessed");

@@ -490,12 +491,6 @@ namespace GPUVerify
 

             mayBeGidAnalyser = new MayBeGidAnalyser(this);

             mayBeGidAnalyser.Analyse();

-

-            mayBeGlobalSizeAnalyser = new MayBeGlobalSizeAnalyser(this);

-            mayBeGlobalSizeAnalyser.Analyse();

-

-            mayBeFlattened2DTidOrGidAnalyser = new MayBeFlattened2DTidOrGidAnalyser(this);

-            mayBeFlattened2DTidOrGidAnalyser.Analyse();

         }

 

         private void DoMayBeIdPlusConstantAnalysis()

@@ -524,6 +519,12 @@ namespace GPUVerify
             liveVariableAnalyser.Analyse();

         }

 

+        private void DoVariableDefinitionAnalysis()

+        {

+            varDefAnalyses = Program.TopLevelDeclarations

+                .OfType<Implementation>()

+                .ToDictionary(i => i, i => VariableDefinitionAnalysis.Analyse(this, i));

+        }

 

         private void ProcessAccessInvariants()

         {

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 376d67b5..0c87587f 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -115,8 +115,6 @@
     <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />

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

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

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

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

     <Compile Include="MayBeGidAnalyser.cs" />

     <Compile Include="EnsureDisabledThreadHasNoEffectInstrumenter.cs" />

     <Compile Include="KernelDualiser.cs" />

@@ -147,6 +145,7 @@
     <Compile Include="UniformityAnalyser.cs" />

     <Compile Include="VariableDualiser.cs" />

     <Compile Include="VariablesOccurringInExpressionVisitor.cs" />

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

     <Compile Include="StructuredRegion.cs" />

     <Compile Include="WriteCollector.cs" />

   </ItemGroup>

diff --git a/Source/GPUVerify/IRegion.cs b/Source/GPUVerify/IRegion.cs
index 26adaa4e..c6655b06 100644
--- a/Source/GPUVerify/IRegion.cs
+++ b/Source/GPUVerify/IRegion.cs
@@ -7,6 +7,7 @@ using Microsoft.Boogie;
 namespace GPUVerify {

 

 interface IRegion {

+  object Identifier();

   IEnumerable<Cmd> Cmds();

   IEnumerable<object> CmdsChildRegions();

   IEnumerable<IRegion> SubRegions();

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

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Diagnostics;

-using Microsoft.Boogie;

-

-namespace GPUVerify

-{

-    class MayBeFlattened2DTidOrGidAnalyser

-    {

-        private static string[] cases = { "local", "global" };

-

-        private GPUVerifier verifier;

-

-        private bool ProcedureChanged;

-

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

-

-        public MayBeFlattened2DTidOrGidAnalyser(GPUVerifier verifier)

-        {

-            this.verifier = verifier;

-

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

-            foreach (string s in cases)

-            {

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

-                    {

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

-                    }

-

-                    foreach (Variable v in Impl.LocVars)

-                    {

-                        foreach (string s in cases)

-                        {

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

-                        }

-                    }

-

-                    foreach (Variable v in Impl.InParams)

-                    {

-                        foreach (string s in cases)

-                        {

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

-                        }

-                    }

-

-                    foreach (Variable v in Impl.OutParams)

-                    {

-                        foreach (string s in cases)

-                        {

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

-                    {

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

-                    }

-                }

-                else if (c is CallCmd)

-                {

-                    foreach (string s in cases)

-                    {

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

-                    }

-                }

-                else if (c is HavocCmd)

-                {

-                    foreach (string s in cases)

-                    {

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

-        }

-

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

-        }

-

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

-

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

-                {

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

-                    {

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

-                    }

-

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

-                    {

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

-                    }

-                }

-                else

-                {

-                    Debug.Assert(component.Equals("global"));

-                    if (verifier.mayBeGidAnalyser.MayBe("x", proc, nary.Args[1]))

-                    {

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

-                    }

-

-                    if (verifier.mayBeGidAnalyser.MayBe("x", proc, nary.Args[0]))

-                    {

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

-                    }

-                }

-            }

-

-            return false;

-        }

-

-        private bool IsLocalIdYTimesGroupSizeX(string proc, Expr expr)

-        {

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

-            {

-                NAryExpr innerNary = expr as NAryExpr;

-

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

-                {

-                    return true;

-                }

-

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

-                {

-                    return true;

-                }

-            }

-            return false;

-        }

-

-        private bool IsLocalIdYAndGroupSizeX(string proc, Expr maybeLocalIdY, Expr maybeGroupSizeX)

-        {

-            return verifier.mayBeTidAnalyser.MayBe(GPUVerifier.LOCAL_ID_Y_STRING, proc, maybeLocalIdY) &&

-                                       verifier.mayBeTidAnalyser.MayBe(GPUVerifier.GROUP_SIZE_X_STRING, proc, maybeGroupSizeX);

-        }

-

-

-        private bool IsGlobalIdYTimesGlobalSizeX(string proc, Expr expr)

-        {

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

-            {

-                NAryExpr innerNary = expr as NAryExpr;

-

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

-                {

-                    return true;

-                }

-

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

-                {

-                    return true;

-                }

-            }

-            return false;

-        }

-

-        private bool IsGlobalIdYAndGlobalSizeX(string proc, Expr maybeGlobalIdY, Expr maybeGlobalSizeX)

-        {

-            return verifier.mayBeGidAnalyser.MayBe("y", proc, maybeGlobalIdY) &&

-                                       verifier.mayBeGlobalSizeAnalyser.MayBe("x", proc, maybeGlobalSizeX);

-        }

-

-

-        private void dump()

-        {

-            foreach (string s in cases)

-            {

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

-

-                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 flattened " + s + " id");

-                        }

-                    }

-                }

-            }

-

-        }

-

-    }

-}

diff --git a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs b/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs
deleted file mode 100644
index 98e71179..00000000
--- a/Source/GPUVerify/MayBeGlobalSizeAnalyser.cs
+++ /dev/null
@@ -1,287 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Diagnostics;

-using Microsoft.Boogie;

-

-namespace GPUVerify

-{

-    class MayBeGlobalSizeAnalyser

-    {

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

-

-        private GPUVerifier verifier;

-

-        private bool ProcedureChanged;

-

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

-

-        public MayBeGlobalSizeAnalyser(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;

-        }

-

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

-        }

-

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

-        {

-            if (e is IdentifierExpr)

-            {

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

-            }

-

-            return IsNumGroupsTimesGroupSize(component, proc, e);

-

-        }

-

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

-        {

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

-            {

-                NAryExpr innerNary = expr as NAryExpr;

-

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

-                {

-                    return true;

-                }

-

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

-                {

-                    return true;

-                }

-            }

-            return false;

-        }

-

-        private bool IsNumGroupsAndGroupSize(string component, string proc, Expr maybeNumGroups, Expr maybeGroupSize)

-        {

-            string numGroupsString = null;

-            string groupSizeString = null;

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

-            {

-                numGroupsString = GPUVerifier.NUM_GROUPS_X_STRING;

-                groupSizeString = GPUVerifier.GROUP_SIZE_X_STRING;

-            }

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

-            {

-                numGroupsString = GPUVerifier.NUM_GROUPS_Y_STRING;

-                groupSizeString = GPUVerifier.GROUP_SIZE_Y_STRING;

-            }

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

-            {

-                numGroupsString = GPUVerifier.NUM_GROUPS_Z_STRING;

-                groupSizeString = GPUVerifier.GROUP_SIZE_Z_STRING;

-            }

-            else

-            {

-                Debug.Assert(false);

-            }

-

-            return verifier.mayBeTidAnalyser.MayBe(numGroupsString, proc, maybeNumGroups) &&

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

-        }

-

-        private void dump()

-        {

-            foreach (string s in dimensions)

-            {

-                Console.WriteLine("*** global_size_" + 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_size_" + s);

-                        }

-                    }

-                }

-            }

-

-        }

-

-    }

-}

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 3b307e64..5155b192 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -452,45 +452,13 @@ 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))

+               .ToList();

 

-            foreach (Expr e in GetOffsetsAccessed(region, v, accessType))

+            if (!offsets.Contains(null))

             {

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

-                {

-                    AddAccessedOffsetIsThreadLocalIdCandidateInvariant(region, v, accessType);

-                    // No point adding it multiple times

-                    break;

-                }

-            }

-

-            foreach (Expr e in GetOffsetsAccessed(region, v, accessType))

-            {

-                if (verifier.mayBeGidAnalyser.MayBe("x", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))

-                {

-                    AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(region, v, accessType);

-                    // No point adding it multiple times

-                    break;

-                }

-            }

-

-            foreach (Expr e in GetOffsetsAccessed(region, v, accessType))

-            {

-                if (verifier.mayBeFlattened2DTidOrGidAnalyser.MayBe("local", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))

-                {

-                    AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(region, v, accessType);

-                    // No point adding it multiple times

-                    break;

-                }

-            }

-

-            foreach (Expr e in GetOffsetsAccessed(region, v, accessType))

-            {

-                if (verifier.mayBeFlattened2DTidOrGidAnalyser.MayBe("global", impl.Name, GPUVerifier.StripThreadIdentifiers(e)))

-                {

-                    AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(region, v, accessType);

-                    // No point adding it multiple times

-                    break;

-                }

+                AddAccessedOffsetsAreConstantCandidateInvariant(region, v, offsets, accessType);

             }

 

             KeyValuePair<IdentifierExpr, Expr> iLessThanC = GetILessThanC(region.Guard());

@@ -680,18 +648,12 @@ namespace GPUVerify
             AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);

         }

 

-        protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);

-

-        protected abstract void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);

-

-        protected abstract void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);

-

-        protected abstract void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(IRegion region, Variable v, string ReadOrWrite);

-

         protected abstract void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite);

 

         protected abstract void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(IRegion region, Variable v, Expr constant, string ReadOrWrite);

 

+        protected abstract void AddAccessedOffsetsAreConstantCandidateInvariant(IRegion region, Variable v, IEnumerable<Expr> offsets, string ReadOrWrite);

+

         protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread);

 

         protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread);

diff --git a/Source/GPUVerify/StructuredRegion.cs b/Source/GPUVerify/StructuredRegion.cs
index 815752dd..366682e0 100644
--- a/Source/GPUVerify/StructuredRegion.cs
+++ b/Source/GPUVerify/StructuredRegion.cs
@@ -7,19 +7,29 @@ using Microsoft.Boogie;
 namespace GPUVerify {

 

 class StructuredRegion : IRegion {

+  Implementation impl;

   WhileCmd cmd;

-  StmtList stmts;

+

+  public StructuredRegion(Implementation impl) {

+    this.impl = impl;

+  }

 

   public StructuredRegion(WhileCmd cmd) {

     this.cmd = cmd;

   }

 

-  public StructuredRegion(StmtList stmts) {

-    this.stmts = stmts;

+  public object Identifier() {

+    if (cmd != null)

+      return cmd;

+    else

+      return impl;

   }

 

-  public StructuredRegion(Implementation impl) {

-    this.stmts = impl.StructuredStmts;

+  private StmtList StmtList() {

+    if (cmd != null)

+      return cmd.Body;

+    else

+      return impl.StructuredStmts;

   }

 

   private IEnumerable<Cmd> Cmds(StmtList stmts) {

@@ -84,24 +94,15 @@ class StructuredRegion : IRegion {
   }

 

   public IEnumerable<Cmd> Cmds() {

-    if (cmd != null)

-      return Cmds(cmd.Body);

-    else

-      return Cmds(stmts);

+    return Cmds(StmtList());

   }

 

   public IEnumerable<object> CmdsChildRegions() {

-    if (cmd != null)

-      return CmdsChildRegions(cmd.Body);

-    else

-      return CmdsChildRegions(stmts);

+    return CmdsChildRegions(StmtList());

   }

 

   public IEnumerable<IRegion> SubRegions() {

-    if (cmd != null)

-      return SubRegions(cmd.Body);

-    else

-      return SubRegions(stmts);

+    return SubRegions(StmtList());

   }

 

   public Expr Guard() {

@@ -117,4 +118,4 @@ class StructuredRegion : IRegion {
   }

 }

 

-}
\ No newline at end of file
+}

diff --git a/Source/GPUVerify/UnstructuredRegion.cs b/Source/GPUVerify/UnstructuredRegion.cs
index 607dc6d7..239f7ca0 100644
--- a/Source/GPUVerify/UnstructuredRegion.cs
+++ b/Source/GPUVerify/UnstructuredRegion.cs
@@ -37,6 +37,10 @@ class UnstructuredRegion : IRegion {
     guard = null;

   }

 

+  public object Identifier() {

+    return header;

+  }

+

   private HashSet<Block> SubBlocks() {

     if (header != null) {

       return loopNodes[header];

@@ -90,4 +94,4 @@ class UnstructuredRegion : IRegion {
   }

 }

 

-}
\ No newline at end of file
+}

diff --git a/Source/GPUVerify/VariableDefinitionAnalysis.cs b/Source/GPUVerify/VariableDefinitionAnalysis.cs
new file mode 100644
index 00000000..f55e51e8
--- /dev/null
+++ b/Source/GPUVerify/VariableDefinitionAnalysis.cs
@@ -0,0 +1,155 @@
+using System;

+using Microsoft.Boogie;

+using System.Collections.Generic;

+using System.Linq;

+

+namespace GPUVerify {

+

+class VariableDefinitionAnalysis {

+  GPUVerifier verifier;

+  Implementation impl;

+

+  Dictionary<Variable, Expr> defMap = new Dictionary<Variable, Expr>();

+  Dictionary<string, Expr> namedDefMap = new Dictionary<string, Expr>();

+  bool changed;

+

+  VariableDefinitionAnalysis(GPUVerifier v, Implementation i) {

+    verifier = v;

+    impl = i;

+  }

+

+  private class IsConstantVisitor : StandardVisitor {

+    private VariableDefinitionAnalysis analysis;

+    public bool isConstant = true;

+

+    public IsConstantVisitor(VariableDefinitionAnalysis a) {

+      analysis = a;

+    }

+

+    public override Expr VisitNAryExpr(NAryExpr expr) {

+      if (expr.Fun is MapSelect) {

+        isConstant = false;

+        return expr;

+      } else

+        return base.VisitNAryExpr(expr);

+    }

+

+    public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

+      if (expr.Decl is Constant)

+        return expr;

+      if (!analysis.defMap.ContainsKey(expr.Decl) || analysis.defMap[expr.Decl] == null)

+        isConstant = false;

+      return expr;

+    }

+  };

+

+  bool IsConstant(Expr e) {

+    var v = new IsConstantVisitor(this);

+    v.Visit(e);

+    return v.isConstant;

+  }

+

+  void UpdateDefMap(Variable v, Expr def) {

+    if (!defMap.ContainsKey(v) || defMap[v] != def) {

+      changed = true;

+      defMap[v] = def;

+    }

+  }

+

+  void AddAssignment(AssignLhs lhs, Expr rhs) {

+    if (lhs is SimpleAssignLhs) {

+      var sLhs = (SimpleAssignLhs)lhs;

+      var theVar = sLhs.DeepAssignedVariable;

+      if ((defMap.ContainsKey(theVar) && defMap[theVar] != rhs) || !IsConstant(rhs)) {

+        UpdateDefMap(theVar, null);

+      } else {

+        UpdateDefMap(theVar, rhs);

+      }

+    }

+  }

+

+  void Analyse() {

+    do {

+      changed = false;

+      foreach (var c in verifier.RootRegion(impl).Cmds()) {

+        if (c is AssignCmd) {

+          var aCmd = (AssignCmd)c;

+          foreach (var a in aCmd.Lhss.Zip(aCmd.Rhss)) {

+            AddAssignment(a.Item1, a.Item2);

+          }

+        }

+      }

+    } while (changed);

+  }

+

+  private class BuildNamedDefVisitor : StandardVisitor {

+    private VariableDefinitionAnalysis analysis;

+

+    public BuildNamedDefVisitor(VariableDefinitionAnalysis a) {

+      analysis = a;

+    }

+

+    public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

+      if (expr.Decl is Constant)

+        return expr;

+      return analysis.BuildNamedDefFor(expr.Decl);

+    }

+  }

+

+  Expr BuildNamedDefFor(Variable v) {

+    Expr def;

+    if (namedDefMap.TryGetValue(v.Name, out def))

+      return def;

+    def = (Expr)new BuildNamedDefVisitor(this).Visit(defMap[v].Clone());

+    namedDefMap[v.Name] = def;

+    return def;

+  }

+

+  void BuildNamedDefMap() {

+    foreach (var v in defMap.Keys)

+      if (defMap[v] != null)

+        BuildNamedDefFor(v);

+  }

+

+  private class SubstDualisedDefVisitor : StandardVisitor {

+    private VariableDefinitionAnalysis analysis;

+    private VariableDualiser dualiser;

+    public bool isSubstitutable = true;

+

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

+      analysis = a;

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

+    }

+

+    public override Expr VisitIdentifierExpr(IdentifierExpr expr) {

+      if (expr.Decl is Constant)

+        return dualiser.VisitIdentifierExpr(expr);

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

+      Expr def;

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

+        isSubstitutable = false;

+        return null;

+      }

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

+    }

+  }

+

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

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

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

+    if (!v.isSubstitutable)

+      return null;

+    return result;

+  }

+

+  public static VariableDefinitionAnalysis Analyse(GPUVerifier verifier, Implementation impl) {

+    var a = new VariableDefinitionAnalysis(verifier, impl);

+    a.Analyse();

+    a.BuildNamedDefMap();

+    a.defMap = null;

+    return a;

+  }

+

+}

+

+}