Merge

15 files changed, 346 insertions, 1252 deletions

diff --git a/Source/GPUVerify/AsymmetricExpressionFinder.cs b/Source/GPUVerify/AsymmetricExpressionFinder.cs
index 40c7eb32..4fb18352 100644
--- a/Source/GPUVerify/AsymmetricExpressionFinder.cs
+++ b/Source/GPUVerify/AsymmetricExpressionFinder.cs
@@ -18,7 +18,9 @@ namespace GPUVerify
         public override Variable VisitVariable(Variable node)

         {

             if (node.TypedIdent.Name.Contains("_READ_HAS_OCCURRED") ||

-                node.TypedIdent.Name.Contains("_READ_OFFSET"))

+                node.TypedIdent.Name.Contains("_READ_OFFSET") ||

+                node.TypedIdent.Name.Contains("_WRITE_HAS_OCCURRED") ||

+                node.TypedIdent.Name.Contains("_WRITE_OFFSET"))

             {

                 found = true;

             }

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index b2e54dbd..502844b2 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -24,18 +24,12 @@ namespace GPUVerify
         public static bool DividedArray = false;

         public static string ArrayToCheck = null;

         public static bool DividedAccesses = false;

-        public static bool Eager = false;

-

-        public static bool Symmetry = false;

-        public static bool SetEncoding = false;

 

         public static bool ShowStages = false;

 

         public static bool AddDivergenceCandidatesOnlyIfModified = true;

         public static bool AddDivergenceCandidatesOnlyToBarrierLoops = true;

 

-        public static bool AssignAtBarriers = false;

-

         public static bool ShowUniformityAnalysis = false;

         public static bool DoUniformityAnalysis = true;

 

@@ -121,21 +115,6 @@ namespace GPUVerify
                     DividedArray = true;

                     break;

 

-                    case "-symmetry":

-                    case "/symmetry":

-                    Symmetry = true;

-                    break;

-

-                    case "-setEncoding":

-                    case "/setEncoding":

-                    SetEncoding = true;

-                    break;

-

-                    case "-eager":

-                    case "/eager":

-                    Eager = true;

-                    break;

-

                     case "-showStages":

                     case "/showStages":

                     ShowStages = true;

@@ -163,11 +142,6 @@ namespace GPUVerify
                     AddDivergenceCandidatesOnlyToBarrierLoops = false;

                     break;

 

-                    case "-assignAtBarriers":

-                    case "/assignAtBarriers":

-                    AssignAtBarriers = true;

-                    break;

-

                     case "-showUniformityAnalysis":

                     case "/showUniformityAnalysis":

                     ShowUniformityAnalysis = true;

diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
index 1763bb58..c249ef0f 100644
--- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
@@ -18,41 +18,20 @@ namespace GPUVerify
 

 

 

-        protected override void AddLogAccessProcedure(Variable v, string ReadOrWrite)

+        protected override void AddLogAccessProcedure(Variable v, string Access)

         {

-            Variable XParameterVariable;

-            Variable YParameterVariable;

-            Variable ZParameterVariable;

-            Procedure LogReadOrWriteProcedure;

+            Procedure LogAccessProcedure = MakeLogAccessProcedureHeader(v, Access);

 

-            MakeLogAccessProcedureHeader(v, ReadOrWrite, out XParameterVariable, out YParameterVariable, out ZParameterVariable, out LogReadOrWriteProcedure);

+            Variable AccessHasOccurredVariable = GPUVerifier.MakeAccessHasOccurredVariable(v.Name, Access);

+            Variable AccessOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, Access);

 

-            IdentifierExprSeq modifies = LogReadOrWriteProcedure.Modifies;

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

-            Variable ReadOrWriteOffsetXVariable = null;

-            Variable ReadOrWriteOffsetYVariable = null;

-            Variable ReadOrWriteOffsetZVariable = null;

+            Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));

 

-            if (XParameterVariable != null)

-            {

-                ReadOrWriteOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite);

-                modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetXVariable));

-            }

-            if (YParameterVariable != null)

-            {

-                Debug.Assert(XParameterVariable != null);

-                ReadOrWriteOffsetYVariable = GPUVerifier.MakeOffsetYVariable(v, ReadOrWrite);

-                modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetYVariable));

-            }

-            if (ZParameterVariable != null)

-            {

-                Debug.Assert(XParameterVariable != null);

-                Debug.Assert(YParameterVariable != null);

-                ReadOrWriteOffsetZVariable = GPUVerifier.MakeOffsetZVariable(v, ReadOrWrite);

-                modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteOffsetZVariable));

-            }

-

-            modifies.Add(new IdentifierExpr(v.tok, ReadOrWriteHasOccurredVariable));

+            Debug.Assert(v.TypedIdent.Type is MapType);

+            MapType mt = v.TypedIdent.Type as MapType;

+            Debug.Assert(mt.Arguments.Length == 1);

+            Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));

+            Debug.Assert(!(mt.Result is MapType));

 

             VariableSeq locals = new VariableSeq();

             Variable TrackVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "track", Microsoft.Boogie.Type.Bool));

@@ -63,103 +42,110 @@ namespace GPUVerify
             CmdSeq simpleCmds = new CmdSeq();

 

             simpleCmds.Add(new HavocCmd(v.tok, new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, TrackVariable) })));

-            simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteHasOccurredVariable, new IdentifierExpr(v.tok, TrackVariable), Expr.True));

-            if (ReadOrWriteOffsetXVariable != null)

-            {

-                simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteOffsetXVariable, new IdentifierExpr(v.tok, TrackVariable), new IdentifierExpr(v.tok, XParameterVariable)));

-            }

-            if (ReadOrWriteOffsetYVariable != null)

-            {

-                simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteOffsetYVariable, new IdentifierExpr(v.tok, TrackVariable), new IdentifierExpr(v.tok, YParameterVariable)));

-            }

-            if (ReadOrWriteOffsetZVariable != null)

-            {

-                simpleCmds.Add(MakeConditionalAssignment(ReadOrWriteOffsetZVariable, new IdentifierExpr(v.tok, TrackVariable), new IdentifierExpr(v.tok, ZParameterVariable)));

-            }

-

-

-            bigblocks.Add(new BigBlock(v.tok, "_LOG_" + ReadOrWrite + "", simpleCmds, null, null));

 

-            StmtList statements = new StmtList(bigblocks, v.tok);

+            simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessHasOccurredVariable), 

+                Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), Expr.True));

+            simpleCmds.Add(MakeConditionalAssignment(VariableForThread(1, AccessOffsetXVariable), 

+                Expr.And(new IdentifierExpr(v.tok, VariableForThread(1, PredicateParameter)), new IdentifierExpr(v.tok, TrackVariable)), 

+                new IdentifierExpr(v.tok, VariableForThread(1, OffsetParameter))));

 

-            Implementation LogReadOrWriteImplementation = new Implementation(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), LogReadOrWriteProcedure.InParams, new VariableSeq(), locals, statements);

-            LogReadOrWriteImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

-

-            LogReadOrWriteImplementation.Proc = LogReadOrWriteProcedure;

-

-            verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteProcedure);

-            verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);

-        }

-

-        protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog)

-        {

-            ModifiedAtLog = new IdentifierExprSeq();

-            ResetAtBarrier = new IdentifierExprSeq();

-

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

-

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

+            if (Access.Equals("READ"))

             {

-                verifier.HalfDualisedVariableNames.Add(AccessHasOccurred.Name);

+                // Check read by thread 2 does not conflict with write by thread 1

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

+                Variable WriteOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "WRITE");

+                Expr WriteReadGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));

+                WriteReadGuard = Expr.And(WriteReadGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));

+                WriteReadGuard = Expr.And(WriteReadGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)), 

+                                                new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

+                if (!verifier.ArrayModelledAdversarially(v))

+                {

+                    WriteReadGuard = Expr.And(WriteReadGuard, Expr.Neq(

+                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)), 1, "WRITE"),

+                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")

+                        ));

+                }

+                WriteReadGuard = Expr.Not(WriteReadGuard);

+                simpleCmds.Add(new AssertCmd(Token.NoToken, WriteReadGuard));

             }

-

-            ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessHasOccurred));

-            ResetAtBarrier.Add(new IdentifierExpr(v.tok, AccessHasOccurred));

-

-            verifier.Program.TopLevelDeclarations.Add(AccessHasOccurred);

-            if (v.TypedIdent.Type is MapType)

+            else

             {

-                MapType mt = v.TypedIdent.Type as MapType;

-                Debug.Assert(mt.Arguments.Length == 1);

+                Debug.Assert(Access.Equals("WRITE"));

 

-                Variable AccessOffsetX = GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite);

+                // Check write by thread 2 does not conflict with write by thread 1

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

+                Variable WriteOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "WRITE");

 

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

+                Expr WriteWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));

+                WriteWriteGuard = Expr.And(WriteWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteHasOccurredVariable)));

+                WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)),

+                                                new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

+                if (!verifier.ArrayModelledAdversarially(v))

+                {

+                    WriteWriteGuard = Expr.And(WriteWriteGuard, Expr.Neq(

+                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, WriteOffsetXVariable)), 1, "WRITE"),

+                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "WRITE")

+                        ));

+                }

+                WriteWriteGuard = Expr.Not(WriteWriteGuard);

+                simpleCmds.Add(new AssertCmd(Token.NoToken, WriteWriteGuard));

+

+                // Check write by thread 2 does not conflict with read by thread 1

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

+                Variable ReadOffsetXVariable = GPUVerifier.MakeOffsetXVariable(v, "READ");

+

+                Expr ReadWriteGuard = new IdentifierExpr(Token.NoToken, VariableForThread(2, PredicateParameter));

+                ReadWriteGuard = Expr.And(ReadWriteGuard, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadHasOccurredVariable)));

+                ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Eq(new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetXVariable)),

+                                                new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter))));

+                if (!verifier.ArrayModelledAdversarially(v))

                 {

-                    verifier.HalfDualisedVariableNames.Add(AccessOffsetX.Name);

+                    ReadWriteGuard = Expr.And(ReadWriteGuard, Expr.Neq(

+                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(1, ReadOffsetXVariable)), 1, "WRITE"),

+                        MakeAccessedIndex(v, new IdentifierExpr(Token.NoToken, VariableForThread(2, OffsetParameter)), 2, "READ")

+                        ));

                 }

+                ReadWriteGuard = Expr.Not(ReadWriteGuard);

+                simpleCmds.Add(new AssertCmd(Token.NoToken, ReadWriteGuard));

 

-                ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetX));

-                verifier.Program.TopLevelDeclarations.Add(AccessOffsetX);

+            }

 

-                if (mt.Result is MapType)

-                {

-                    MapType mt2 = mt.Result as MapType;

-                    Debug.Assert(mt2.Arguments.Length == 1);

-                    Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));

+            bigblocks.Add(new BigBlock(v.tok, "_LOG_" + Access + "", simpleCmds, null, null));

 

-                    Variable AccessOffsetY = GPUVerifier.MakeOffsetYVariable(v, ReadOrWrite);

+            LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessHasOccurredVariable)));

+            LogAccessProcedure.Modifies.Add(new IdentifierExpr(Token.NoToken, VariableForThread(1, AccessOffsetXVariable)));

 

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

-                    {

-                        verifier.HalfDualisedVariableNames.Add(AccessOffsetY.Name);

-                    }

+            Implementation LogAccessImplementation = new Implementation(v.tok, "_LOG_" + Access + "_" + v.Name, new TypeVariableSeq(), LogAccessProcedure.InParams, new VariableSeq(), locals, new StmtList(bigblocks, v.tok));

+            LogAccessImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

 

-                    ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetY));

-                    verifier.Program.TopLevelDeclarations.Add(AccessOffsetY);

+            LogAccessImplementation.Proc = LogAccessProcedure;

 

-                    if (mt2.Result is MapType)

-                    {

-                        MapType mt3 = mt2.Arguments[0] as MapType;

-                        Debug.Assert(mt3.Arguments.Length == 1);

-                        Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));

-                        Debug.Assert(!(mt3.Result is MapType));

+            verifier.Program.TopLevelDeclarations.Add(LogAccessProcedure);

+            verifier.Program.TopLevelDeclarations.Add(LogAccessImplementation);

+        }

 

-                        Variable AccessOffsetZ = GPUVerifier.MakeOffsetZVariable(v, ReadOrWrite);

+        private Variable VariableForThread(int thread, Variable v)

+        {

+            return new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable);

+        }

 

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

-                        {

-                            verifier.HalfDualisedVariableNames.Add(AccessOffsetZ.Name);

-                        }

+        protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite)

+        {

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

 

-                        ModifiedAtLog.Add(new IdentifierExpr(v.tok, AccessOffsetZ));

-                        verifier.Program.TopLevelDeclarations.Add(AccessOffsetZ);

-                    }

-                }

-            }

+            // Assumes full symmetry reduction

 

-        }

+            verifier.Program.TopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable(AccessHasOccurred.Clone() as Variable));

 

+            Debug.Assert(v.TypedIdent.Type is MapType);

+            MapType mt = v.TypedIdent.Type as MapType;

+            Debug.Assert(mt.Arguments.Length == 1);

+

+            Variable AccessOffsetX = GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite);

+            verifier.Program.TopLevelDeclarations.Add(new VariableDualiser(1, null, null).VisitVariable(AccessOffsetX.Clone() as Variable));

+

+        }

+        

 

         private static AssignCmd MakeConditionalAssignment(Variable lhs, Expr condition, Expr rhs)

         {

@@ -174,144 +160,29 @@ namespace GPUVerify
         {

             IdentifierExpr AccessOccurred1 = new IdentifierExpr(tok,

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

-            IdentifierExpr AccessOccurred2 = new IdentifierExpr(tok,

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

-

-            if (CommandLineOptions.AssignAtBarriers)

-            {

 

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

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

-

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

-                rhss.Add(Expr.False);

-

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

-                {

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

-                    rhss.Add(Expr.False);

-                }

-

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

-            }

-            else

-            {

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

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

-                {

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

-                }

-            }

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

         }

 

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

+        private Expr MakeAccessedIndex(Variable v, Expr offsetExpr, int Thread, string AccessType)

         {

-            if (!ReadWriteOnly)

-            {

-                bb.simpleCmds.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "WRITE", "WRITE"))));

-            }

-            bb.simpleCmds.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "READ", "WRITE"))));

-            if (!CommandLineOptions.Symmetry)

-            {

-                bb.simpleCmds.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "WRITE", "READ"))));

-            }

-        }

-

-        protected override Expr GenerateRaceCondition(Variable v, string FirstAccessType, string SecondAccessType)

-        {

-            Expr RaceCondition = Expr.And(

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

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

-

-            if (GPUVerifier.HasXDimension(v))

-            {

-                RaceCondition = Expr.And(RaceCondition, Expr.Eq(

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

-                    new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, SecondAccessType)))

-                ));

-            }

-

-            if (GPUVerifier.HasYDimension(v))

-            {

-                RaceCondition = Expr.And(RaceCondition, Expr.Eq(

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

-                    new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, SecondAccessType)))

-                    ));

-            }

-

-            if (GPUVerifier.HasZDimension(v))

-            {

-                RaceCondition = Expr.And(RaceCondition, Expr.Eq(

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

-                    new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, SecondAccessType)))

-                    ));

-            }

-

-            if (FirstAccessType.Equals("WRITE") && SecondAccessType.Equals("WRITE") && !verifier.ArrayModelledAdversarially(v))

-            {

-                RaceCondition = Expr.And(RaceCondition, Expr.Neq(

-                    MakeWrittenIndex(v, 1),

-                    MakeWrittenIndex(v, 2)

-                    ));

-            }

-

-            return RaceCondition;

-        }

-

-        private static Expr MakeWrittenIndex(Variable v, int OneOrTwo)

-        {

-            Expr result = new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(v.Clone() as Variable));

-

-            if (v.TypedIdent.Type is MapType)

-            {

-                MapType mt = v.TypedIdent.Type as MapType;

-                Debug.Assert(mt.Arguments.Length == 1);

-

-                result = Expr.Select(result,

-                    new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, "WRITE"))) });

-

-                if (mt.Result is MapType)

-                {

-                    MapType mt2 = mt.Result as MapType;

-                    Debug.Assert(mt2.Arguments.Length == 1);

-                    Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));

-

-                    result = Expr.Select(result,

-                        new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(GPUVerifier.MakeOffsetYVariable(v, "WRITE"))) });

-

-                    if (mt2.Result is MapType)

-                    {

-                        MapType mt3 = mt2.Arguments[0] as MapType;

-                        Debug.Assert(mt3.Arguments.Length == 1);

-                        Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));

-                        Debug.Assert(!(mt3.Result is MapType));

-

-                        result = Expr.Select(result,

-                            new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo, null, null).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, "WRITE"))) });

-

-                    }

-                }

-            }

-

+            Expr result = new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(v.Clone() as Variable));

+            Debug.Assert(v.TypedIdent.Type is MapType);

+            MapType mt = v.TypedIdent.Type as MapType;

+            Debug.Assert(mt.Arguments.Length == 1);

+

+            result = Expr.Select(result,

+                new Expr[] { offsetExpr });

+            Debug.Assert(!(mt.Result is MapType));

             return result;

-

         }

 

         protected override void AddRequiresNoPendingAccess(Variable v)

         {

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

-            IdentifierExpr ReadAccessOccurred2 = new IdentifierExpr(v.tok, new VariableDualiser(2, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")));

             IdentifierExpr WriteAccessOccurred1 = new IdentifierExpr(v.tok, new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")));

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

 

-            if (CommandLineOptions.Symmetry)

-            {

-                verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.And(Expr.Not(WriteAccessOccurred1), Expr.Not(WriteAccessOccurred2)))));

-            }

-            else

-            {

-                verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.And(Expr.Not(ReadAccessOccurred2), Expr.And(Expr.Not(WriteAccessOccurred1), Expr.Not(WriteAccessOccurred2))))));

-            }

+            verifier.KernelProcedure.Requires.Add(new Requires(false, Expr.And(Expr.Not(ReadAccessOccurred1), Expr.Not(WriteAccessOccurred1))));

         }

 

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

@@ -327,24 +198,12 @@ namespace GPUVerify
         protected override void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)

         {

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

-

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

-            {

-                expr = Expr.And(expr, AccessedOffsetIsThreadGlobalIdExpr(v, ReadOrWrite, 2));

-            }

-

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

         }

 

         protected override void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)

         {

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

-

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

-            {

-                expr = Expr.And(expr, AccessedOffsetIsThreadLocalIdExpr(v, ReadOrWrite, 2));

-            }

-

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

         }

 

@@ -391,11 +250,6 @@ namespace GPUVerify
         protected override void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)

         {

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

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

-            {

-                expr = Expr.And(expr, AccessedOffsetIsThreadFlattened2DLocalIdExpr(v, ReadOrWrite, 2));

-            }

-            

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

         }

 

@@ -420,11 +274,6 @@ namespace GPUVerify
         protected override void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)

         {

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

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

-            {

-                expr = Expr.And(expr, AccessedOffsetIsThreadFlattened2DGlobalIdExpr(v, ReadOrWrite, 2));

-            }

-

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

         }

 

@@ -448,14 +297,7 @@ namespace GPUVerify
 

         protected override void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite)

         {

-

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

-

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

-            {

-                expr = Expr.And(expr, MakeCTimesLocalIdRangeExpression(v, constant, ReadOrWrite, 2));

-            }

-

             verifier.AddCandidateInvariant(wc,

                 expr, "accessed offset in range [ C*local_id, (C+1)*local_id )");

         }

@@ -490,12 +332,6 @@ namespace GPUVerify
         protected override void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite)

         {

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

-

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

-            {

-                expr = Expr.And(expr, MakeCTimesGloalIdRangeExpr(v, constant, ReadOrWrite, 2));

-            }

-

             verifier.AddCandidateInvariant(wc,

                 expr, "accessed offset in range [ C*global_id, (C+1)*global_id )");

         }

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 9acf7619..f6ba390b 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -23,9 +23,6 @@ namespace GPUVerify
 

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

 

-        internal HashSet<string> HalfDualisedProcedureNames = new HashSet<string>();

-        internal HashSet<string> HalfDualisedVariableNames = new HashSet<string>();

-

         private int TempCounter = 0;

         private int invariantGenerationCounter;

 

@@ -375,10 +372,7 @@ namespace GPUVerify
                 emitProgram(outputFilename + "_cross_thread_invariants");

             }

 

-            if (CommandLineOptions.Eager)

-            {

-                AddEagerRaceChecking();

-            }

+            RaceInstrumenter.AddRaceCheckingDeclarations();

 

             GenerateBarrierImplementation();

 

@@ -614,36 +608,6 @@ namespace GPUVerify
             }

         }

 

-        private void AddEagerRaceChecking()

-        {

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

-            {

-                foreach (Declaration d in Program.TopLevelDeclarations)

-                {

-                    if (!(d is Implementation))

-                    {

-                        continue;

-                    }

-

-                    Implementation impl = d as Implementation;

-

-                    if (impl.Name.Equals("_LOG_READ_" + v.Name) || impl.Name.Equals("_LOG_WRITE_" + v.Name))

-                    {

-                        BigBlock bb = new BigBlock(v.tok, "__CheckForRaces", new CmdSeq(), null, null);

-                        RaceInstrumenter.CheckForRaces(bb, v, impl.Name.Equals("_LOG_READ_" + v.Name));

-                        StmtList newStatements = new StmtList(new List<BigBlock>(), v.tok);

-                        

-                        foreach(BigBlock bb2 in impl.StructuredStmts.BigBlocks)

-                        {

-                            newStatements.BigBlocks.Add(bb2);

-                        }

-                        newStatements.BigBlocks.Add(bb);

-                        impl.StructuredStmts = newStatements;

-                    }

-                }

-            }

-        }

-

         private void ComputeInvariant()

         {

 

@@ -1069,16 +1033,6 @@ namespace GPUVerify
             }

             KernelImplementation.StructuredStmts.BigBlocks[0].simpleCmds = newCommands;

 

-            // Last barrier is needed if we don't use eager race checking

-            if (!CommandLineOptions.Eager)

-            {

-                CmdSeq lastCommand = new CmdSeq();

-                lastCommand.Add(LastBarrier);

-                BigBlock bb = new BigBlock(KernelProcedure.tok, "__lastBarrier", lastCommand, null, null);

-

-                KernelImplementation.StructuredStmts.BigBlocks.Add(bb);

-            }

-

         }

 

         private void GenerateStandardKernelContract()

@@ -1112,11 +1066,7 @@ namespace GPUVerify
                     Proc.Requires.Add(new Requires(false, AssumeDistinctThreads));

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

 

-                    if (Proc != KernelProcedure)

-                    {

-                        RaceInstrumenter.AddNoRaceContract(Proc);

-                    }

-                    else

+                    if (Proc == KernelProcedure)

                     {

                         bool foundNonUniform = false;

                         int indexOfFirstNonUniformParameter;

@@ -1157,8 +1107,6 @@ namespace GPUVerify
                 }

                 Implementation Impl = D as Implementation;

 

-                RaceInstrumenter.AddNoRaceInvariants(Impl);

-

                 if (QKeyValue.FindIntAttribute(Impl.Proc.Attributes, "inline", -1) == 1)

                 {

                     continue;

@@ -1360,7 +1308,7 @@ namespace GPUVerify
                 checkNonDivergence.ec = new IfCmd(tok, Expr.Or(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);

             }

 

-            bigblocks.Add(RaceInstrumenter.MakeRaceCheckingStatements(tok));

+            bigblocks.Add(RaceInstrumenter.MakeResetReadWriteSetsStatements(tok));

 

             BigBlock havocSharedState = new BigBlock(tok, "__HavocSharedState", new CmdSeq(), null, null);

             bigblocks.Add(havocSharedState);

@@ -1983,11 +1931,7 @@ namespace GPUVerify
                 if (d is Variable && ((d as Variable).IsMutable || IsThreadLocalIdConstant(d as Variable)))

                 {

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

-

-                    if (!HalfDualisedVariableNames.Contains((d as Variable).Name))

-                    {

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

-                    }

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

 

                     continue;

                 }

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 9881b0f0..5b0f7e3e 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -108,6 +108,9 @@
     <Compile Include="AccessRecord.cs" />

     <Compile Include="ArrayControlFlowAnalyser.cs" />

     <Compile Include="AsymmetricExpressionFinder.cs" />

+    <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" />

@@ -136,7 +139,6 @@
     <Compile Include="Properties\AssemblyInfo.cs" />

     <Compile Include="RaceInstrumenterBase.cs" />

     <Compile Include="ReadCollector.cs" />

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

     <Compile Include="UniformExpressionAnalysisVisitor.cs" />

     <Compile Include="UniformityAnalyser.cs" />

     <Compile Include="VariableDualiser.cs" />

diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs
index f1b877a5..65d2cc1b 100644
--- a/Source/GPUVerify/IRaceInstrumenter.cs
+++ b/Source/GPUVerify/IRaceInstrumenter.cs
@@ -18,16 +18,13 @@ namespace GPUVerify
         // this will return false.

         bool AddRaceCheckingInstrumentation();

 

-        BigBlock MakeRaceCheckingStatements(IToken tok);

+        void AddRaceCheckingDeclarations();

 

-        void CheckForRaces(BigBlock bb, Variable v, bool ReadWriteOnly);

+        BigBlock MakeResetReadWriteSetsStatements(IToken tok);

 

         void AddRaceCheckingCandidateRequires(Procedure Proc);

 

         void AddRaceCheckingCandidateEnsures(Procedure Proc);

 

-        void AddNoRaceContract(Procedure Proc);

-

-        void AddNoRaceInvariants(Implementation Impl);

     }

 }

diff --git a/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs b/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs
new file mode 100644
index 00000000..1bd66785
--- /dev/null
+++ b/Source/GPUVerify/InvariantGenerationRules/InvariantGenerationRule.cs
@@ -0,0 +1,22 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+

+namespace GPUVerify.InvariantGenerationRules

+{

+    abstract class InvariantGenerationRule

+    {

+        protected GPUVerifier verifier;

+

+        public InvariantGenerationRule(GPUVerifier verifier)

+        {

+            this.verifier = verifier;

+        }

+

+        public abstract void GenerateCandidates(Implementation Impl, WhileCmd wc);

+    }

+

+}

diff --git a/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs b/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs
new file mode 100644
index 00000000..233b3b45
--- /dev/null
+++ b/Source/GPUVerify/InvariantGenerationRules/LoopVariableBoundsInvariantGenerator.cs
@@ -0,0 +1,54 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+using Microsoft.Basetypes;

+

+namespace GPUVerify.InvariantGenerationRules

+{

+    class LoopVariableBoundsInvariantGenerator : InvariantGenerationRule

+    {

+

+        public LoopVariableBoundsInvariantGenerator(GPUVerifier verifier)

+            : base(verifier)

+        {

+

+        }

+

+        public override void GenerateCandidates(Implementation Impl, WhileCmd wc)

+        {

+            if (verifier.uniformityAnalyser.IsUniform(Impl.Name, wc.Guard))

+            {

+                VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();

+                visitor.VisitExpr(wc.Guard);

+                foreach (Variable v in visitor.GetVariables())

+                {

+                    if (!verifier.ContainsNamedVariable(LoopInvariantGenerator.GetModifiedVariables(wc.Body), v.Name))

+                    {

+                        continue;

+                    }

+

+                    if (IsBVType (v.TypedIdent.Type))

+                    {

+                        int BVWidth = (v.TypedIdent.Type as BvType).Bits;

+

+                        verifier.AddCandidateInvariant(wc,

+                                GPUVerifier.MakeBitVectorBinaryBoolean("BV" + BVWidth + "_GEQ",

+                                new IdentifierExpr(v.tok, v),

+                                new LiteralExpr(v.tok, BigNum.FromInt(0), BVWidth)), "loop guard variable non-negative");

+                    }

+                }

+            }

+        }

+

+        private bool IsBVType(Microsoft.Boogie.Type type)

+        {

+            return type.Equals(Microsoft.Boogie.Type.GetBvType(32))

+                || type.Equals(Microsoft.Boogie.Type.GetBvType(16))

+                || type.Equals(Microsoft.Boogie.Type.GetBvType(8));

+        }

+

+    }

+}

diff --git a/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs b/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs
new file mode 100644
index 00000000..6b2bdc56
--- /dev/null
+++ b/Source/GPUVerify/InvariantGenerationRules/PowerOfTwoInvariantGenerator.cs
@@ -0,0 +1,61 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+using Microsoft.Basetypes;

+

+namespace GPUVerify.InvariantGenerationRules

+{

+    class PowerOfTwoInvariantGenerator : InvariantGenerationRule

+    {

+

+        public PowerOfTwoInvariantGenerator(GPUVerifier verifier)

+            : base(verifier)

+        {

+

+        }

+

+        public override void GenerateCandidates(Implementation Impl, WhileCmd wc)

+        {

+            foreach (Variable v in Impl.LocVars)

+            {

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

+                if (verifier.uniformityAnalyser.IsUniform(Impl.Name, basicName))

+                {

+                    if (verifier.mayBePowerOfTwoAnalyser.MayBePowerOfTwo(Impl.Name, basicName))

+                    {

+                        if (verifier.ContainsNamedVariable(LoopInvariantGenerator.GetModifiedVariables(wc.Body), basicName))

+                        {

+                            verifier.AddCandidateInvariant(wc, MakePowerOfTwoExpr(v), "pow2 disjunction");

+                            for (int i = (1 << 15); i > 0; i >>= 1)

+                            {

+                                verifier.AddCandidateInvariant(wc, 

+                                    GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT",

+                                    new IdentifierExpr(v.tok, v),

+                                    new LiteralExpr(v.tok, BigNum.FromInt(i), 32)), "pow2 less than " + i);

+                            }

+                            verifier.AddCandidateInvariant(wc,

+                                Expr.Neq(new IdentifierExpr(v.tok, v),

+                                new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), "pow2 not zero");

+                        }

+                    }

+                }

+            }

+        }

+

+        private Expr MakePowerOfTwoExpr(Variable v)

+        {

+            Expr result = null;

+            for (int i = 1 << 15; i > 0; i >>= 1)

+            {

+                Expr eq = Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(i), 32));

+                result = (result == null ? eq : Expr.Or(eq, result));

+            }

+

+            return Expr.Or(Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), result);

+        }

+

+    }

+}

diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs
index 41546a84..0496a4e0 100644
--- a/Source/GPUVerify/KernelDualiser.cs
+++ b/Source/GPUVerify/KernelDualiser.cs
@@ -23,30 +23,11 @@ namespace GPUVerify
         {

             procName = proc.Name;

 

-            bool HalfDualise = verifier.HalfDualisedProcedureNames.Contains(proc.Name);

-

             proc.Requires = DualiseRequires(proc.Requires);

             proc.Ensures = DualiseEnsures(proc.Ensures);

 

-            proc.InParams = DualiseVariableSequence(proc.InParams, HalfDualise);

-            proc.OutParams = DualiseVariableSequence(proc.OutParams, HalfDualise);

-            IdentifierExprSeq NewModifies = new IdentifierExprSeq();

-            foreach (IdentifierExpr v in proc.Modifies)

-            {

-                NewModifies.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr((IdentifierExpr)v.Clone()));

-            }

-

-            if (!HalfDualise)

-            {

-                foreach (IdentifierExpr v in proc.Modifies)

-                {

-                    if (!CommandLineOptions.Symmetry || !verifier.HalfDualisedVariableNames.Contains(v.Name))

-                    {

-                        NewModifies.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr((IdentifierExpr)v.Clone()));

-                    }

-                }

-            }

-            proc.Modifies = NewModifies;

+            proc.InParams = DualiseVariableSequence(proc.InParams);

+            proc.OutParams = DualiseVariableSequence(proc.OutParams);

 

             procName = null;

         }

@@ -59,7 +40,7 @@ namespace GPUVerify
                 newRequires.Add(new Requires(r.Free, new VariableDualiser(1, verifier.uniformityAnalyser, procName).

                     VisitExpr(r.Condition.Clone() as Expr)));

 

-                if ((!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(r.Condition))

+                if (!ContainsAsymmetricExpression(r.Condition)

                     && !verifier.uniformityAnalyser.IsUniform(procName, r.Condition))

                 {

                     newRequires.Add(new Requires(r.Free, new VariableDualiser(2, verifier.uniformityAnalyser, procName).

@@ -76,7 +57,7 @@ namespace GPUVerify
             {

                 newEnsures.Add(new Ensures(e.Free, new VariableDualiser(1, verifier.uniformityAnalyser, procName).

                     VisitExpr(e.Condition.Clone() as Expr)));

-                if ((!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(e.Condition))

+                if (!ContainsAsymmetricExpression(e.Condition)

                     && !verifier.uniformityAnalyser.IsUniform(procName, e.Condition))

                 {

                     newEnsures.Add(new Ensures(e.Free, new VariableDualiser(2, verifier.uniformityAnalyser, procName).

@@ -87,7 +68,7 @@ namespace GPUVerify
         }

 

 

-        private StmtList MakeDual(StmtList stmtList, bool HalfDualise)

+        private StmtList MakeDual(StmtList stmtList)

         {

             Contract.Requires(stmtList != null);

 

@@ -95,13 +76,13 @@ namespace GPUVerify
 

             foreach (BigBlock bodyBlock in stmtList.BigBlocks)

             {

-                result.BigBlocks.Add(MakeDual(bodyBlock, HalfDualise));

+                result.BigBlocks.Add(MakeDual(bodyBlock));

             }

 

             return result;

         }

 

-        private BigBlock MakeDual(BigBlock bb, bool HalfDualise)

+        private BigBlock MakeDual(BigBlock bb)

         {

             // Not sure what to do about the transfer command

 

@@ -126,14 +107,11 @@ namespace GPUVerify
                             nonUniformNewIns.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

                         }

                     }

-                    if (!HalfDualise && !verifier.HalfDualisedProcedureNames.Contains(Call.callee))

+                    for (int i = 0; i < Call.Ins.Count; i++)

                     {

-                        for (int i = 0; i < Call.Ins.Count; i++)

+                        if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))

                         {

-                            if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetInParameter(Call.callee, i))))

-                            {

-                                nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

-                            }

+                            nonUniformNewIns.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(Call.Ins[i]));

                         }

                     }

 

@@ -154,14 +132,11 @@ namespace GPUVerify
                         }

 

                     }

-                    if (!HalfDualise && !verifier.HalfDualisedProcedureNames.Contains(Call.callee))

+                    for (int i = 0; i < Call.Outs.Count; i++)

                     {

-                        for (int i = 0; i < Call.Outs.Count; i++)

+                        if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))

                         {

-                            if (!(verifier.uniformityAnalyser.knowsOf(Call.callee) && verifier.uniformityAnalyser.IsUniform(Call.callee, verifier.uniformityAnalyser.GetOutParameter(Call.callee, i))))

-                            {

-                                nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);

-                            }

+                            nonUniformNewOuts.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(Call.Outs[i].Clone() as IdentifierExpr) as IdentifierExpr);

                         }

                     }

 

@@ -191,18 +166,10 @@ namespace GPUVerify
                         List<Expr> newRhss = new List<Expr>();

 

                         newLhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

-

-                        if (!HalfDualise)

-                        {

-                            newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

-                        }

+                        newLhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).Visit(assign.Lhss.ElementAt(0).Clone() as AssignLhs) as AssignLhs);

 

                         newRhss.Add(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

-

-                        if (!HalfDualise)

-                        {

-                            newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

-                        }

+                        newRhss.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(assign.Rhss.ElementAt(0).Clone() as Expr));

 

                         AssignCmd newAssign = new AssignCmd(assign.tok, newLhss, newRhss);

 

@@ -216,25 +183,17 @@ namespace GPUVerify
 

                     HavocCmd newHavoc;

 

-                    if (HalfDualise)

-                    {

-                        newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 

-                            (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)) 

-                        }));

-                    }

-                    else

-                    {

-                        newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 

-                            (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)), 

-                            (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))

-                        }));

-                    }

+                    newHavoc = new HavocCmd(havoc.tok, new IdentifierExprSeq(new IdentifierExpr[] { 

+                        (IdentifierExpr)(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr)), 

+                        (IdentifierExpr)(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitIdentifierExpr(havoc.Vars[0].Clone() as IdentifierExpr))

+                    }));

+

                     result.simpleCmds.Add(newHavoc);

                 }

                 else if (c is AssertCmd)

                 {

                     AssertCmd ass = c as AssertCmd;

-                    if (HalfDualise || ContainsAsymmetricExpression(ass.Expr))

+                    if (ContainsAsymmetricExpression(ass.Expr))

                     {

                         result.simpleCmds.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));

                     }

@@ -247,7 +206,7 @@ namespace GPUVerify
                 else if (c is AssumeCmd)

                 {

                     AssumeCmd ass = c as AssumeCmd;

-                    if (HalfDualise || ContainsAsymmetricExpression(ass.Expr))

+                    if (ContainsAsymmetricExpression(ass.Expr))

                     {

                         result.simpleCmds.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));

                     }

@@ -278,16 +237,16 @@ namespace GPUVerify
                 }

                 result.ec = new WhileCmd(bb.ec.tok,

                     NewGuard,

-                    MakeDualInvariants((bb.ec as WhileCmd).Invariants), MakeDual((bb.ec as WhileCmd).Body, HalfDualise));

+                    MakeDualInvariants((bb.ec as WhileCmd).Invariants), MakeDual((bb.ec as WhileCmd).Body));

             }

             else if (bb.ec is IfCmd)

             {

                 Debug.Assert(verifier.uniformityAnalyser.IsUniform(procName, (bb.ec as IfCmd).Guard));

                 result.ec = new IfCmd(bb.ec.tok,

                     (bb.ec as IfCmd).Guard,

-                             MakeDual((bb.ec as IfCmd).thn, HalfDualise),

+                             MakeDual((bb.ec as IfCmd).thn),

                              null,

-                             (bb.ec as IfCmd).elseBlock == null ? null : MakeDual((bb.ec as IfCmd).elseBlock, HalfDualise));

+                             (bb.ec as IfCmd).elseBlock == null ? null : MakeDual((bb.ec as IfCmd).elseBlock));

 

             }

             else if (bb.ec is BreakCmd)

@@ -314,7 +273,7 @@ namespace GPUVerify
                     newP.Attributes = p.Attributes;

                     result.Add(newP);

                 }

-                if ((!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(p.Expr))

+                if (!ContainsAsymmetricExpression(p.Expr)

                     && !verifier.uniformityAnalyser.IsUniform(procName, p.Expr))

                 {

                     PredicateCmd newP = new AssertCmd(p.tok, Dualise(p.Expr, 2));

@@ -326,7 +285,7 @@ namespace GPUVerify
             return result;

         }

 

-        private void MakeDualLocalVariables(Implementation impl, bool HalfDualise)

+        private void MakeDualLocalVariables(Implementation impl)

         {

             VariableSeq NewLocalVars = new VariableSeq();

 

@@ -340,11 +299,8 @@ namespace GPUVerify
                 {

                     NewLocalVars.Add(

                         new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitVariable(v.Clone() as Variable));

-                    if (!HalfDualise)

-                    {

-                        NewLocalVars.Add(

-                            new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitVariable(v.Clone() as Variable));

-                    }

+                    NewLocalVars.Add(

+                        new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitVariable(v.Clone() as Variable));

                 }

             }

 

@@ -358,7 +314,7 @@ namespace GPUVerify
             return finder.foundAsymmetricExpr();

         }

 

-        private VariableSeq DualiseVariableSequence(VariableSeq seq, bool HalfDualise)

+        private VariableSeq DualiseVariableSequence(VariableSeq seq)

         {

             VariableSeq uniform = new VariableSeq();

             VariableSeq nonuniform = new VariableSeq();

@@ -375,14 +331,11 @@ namespace GPUVerify
                 }

             }

 

-             if (!HalfDualise)

+            foreach (Variable v in seq)

             {

-                foreach (Variable v in seq)

+                if (!verifier.uniformityAnalyser.IsUniform(procName, v.Name))

                 {

-                    if (!verifier.uniformityAnalyser.IsUniform(procName, v.Name))

-                    {

-                        nonuniform.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitVariable((Variable)v.Clone()));

-                    }

+                    nonuniform.Add(new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitVariable((Variable)v.Clone()));

                 }

             }

 

@@ -396,12 +349,10 @@ namespace GPUVerify
         {

             procName = impl.Name;

 

-            bool HalfDualise = verifier.HalfDualisedProcedureNames.Contains(impl.Name);

-

-            impl.InParams = DualiseVariableSequence(impl.InParams, HalfDualise);

-            impl.OutParams = DualiseVariableSequence(impl.OutParams, HalfDualise);

-            MakeDualLocalVariables(impl, HalfDualise);

-            impl.StructuredStmts = MakeDual(impl.StructuredStmts, HalfDualise);

+            impl.InParams = DualiseVariableSequence(impl.InParams);

+            impl.OutParams = DualiseVariableSequence(impl.OutParams);

+            MakeDualLocalVariables(impl);

+            impl.StructuredStmts = MakeDual(impl.StructuredStmts);

 

             procName = null;

         }

diff --git a/Source/GPUVerify/LoopInvariantGenerator.cs b/Source/GPUVerify/LoopInvariantGenerator.cs
index 6411025d..ead78917 100644
--- a/Source/GPUVerify/LoopInvariantGenerator.cs
+++ b/Source/GPUVerify/LoopInvariantGenerator.cs
@@ -6,6 +6,8 @@ using Microsoft.Boogie;
 using Microsoft.Basetypes;

 using System.Diagnostics;

 

+using GPUVerify.InvariantGenerationRules;

+

 namespace GPUVerify

 {

     class LoopInvariantGenerator

@@ -13,10 +15,16 @@ namespace GPUVerify
         private GPUVerifier verifier;

         private Implementation Impl;

 

+        private List<InvariantGenerationRule> invariantGenerationRules;

+

         public LoopInvariantGenerator(GPUVerifier verifier, Implementation Impl)

         {

             this.verifier = verifier;

             this.Impl = Impl;

+

+            invariantGenerationRules = new List<InvariantGenerationRule>();

+            invariantGenerationRules.Add(new PowerOfTwoInvariantGenerator(verifier));

+            invariantGenerationRules.Add(new LoopVariableBoundsInvariantGenerator(verifier));

         }

 

         internal void instrument(List<Expr> UserSuppliedInvariants)

@@ -149,11 +157,12 @@ namespace GPUVerify
             {

                 WhileCmd wc = bb.ec as WhileCmd;

 

-                AddBarrierDivergenceCandidates(LocalVars, Impl, wc);

-

-                AddLoopVariableBoundsCandidateInvariants(Impl, wc);

+                foreach (InvariantGenerationRule r in invariantGenerationRules)

+                {

+                    r.GenerateCandidates(Impl, wc);

+                }

 

-                AddPowerOfTwoCandidateInvariants(Impl, wc);

+                AddBarrierDivergenceCandidates(LocalVars, Impl, wc);

 

                 verifier.RaceInstrumenter.AddRaceCheckingCandidateInvariants(Impl, wc);

 

@@ -177,79 +186,6 @@ namespace GPUVerify
             }

         }

 

-        private void AddPowerOfTwoCandidateInvariants(Implementation Impl, WhileCmd wc)

-        {

-            foreach (Variable v in Impl.LocVars)

-            {

-                string basicName = GPUVerifier.StripThreadIdentifier(v.Name);

-                if (verifier.uniformityAnalyser.IsUniform(Impl.Name, basicName))

-                {

-                    if (verifier.mayBePowerOfTwoAnalyser.MayBePowerOfTwo(Impl.Name, basicName))

-                    {

-                        if (verifier.ContainsNamedVariable(GetModifiedVariables(wc.Body), basicName))

-                        {

-                            verifier.AddCandidateInvariant(wc, MakePowerOfTwoExpr(v), "pow2 disjunction");

-                            for (int i = (1 << 15); i > 0; i >>= 1)

-                            {

-                                verifier.AddCandidateInvariant(wc, 

-                                    GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LT",

-                                    new IdentifierExpr(v.tok, v),

-                                    new LiteralExpr(v.tok, BigNum.FromInt(i), 32)), "pow2 less than " + i);

-                            }

-                            verifier.AddCandidateInvariant(wc,

-                                Expr.Neq(new IdentifierExpr(v.tok, v),

-                                new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), "pow2 not zero");

-                        }

-                    }

-                }

-            }

-        }

-

-        private Expr MakePowerOfTwoExpr(Variable v)

-        {

-            Expr result = null;

-            for (int i = 1 << 15; i > 0; i >>= 1)

-            {

-                Expr eq = Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(i), 32));

-                result = (result == null ? eq : Expr.Or(eq, result));

-            }

-

-            return Expr.Or(Expr.Eq(new IdentifierExpr(v.tok, v), new LiteralExpr(v.tok, BigNum.FromInt(0), 32)), result);

-        }

-

-        private void AddLoopVariableBoundsCandidateInvariants(Implementation Impl, WhileCmd wc)

-        {

-            if (verifier.uniformityAnalyser.IsUniform(Impl.Name, wc.Guard))

-            {

-                VariablesOccurringInExpressionVisitor visitor = new VariablesOccurringInExpressionVisitor();

-                visitor.VisitExpr(wc.Guard);

-                foreach (Variable v in visitor.GetVariables())

-                {

-                    if (!verifier.ContainsNamedVariable(GetModifiedVariables(wc.Body), v.Name))

-                    {

-                        continue;

-                    }

-

-                    if (IsBVType (v.TypedIdent.Type))

-                    {

-                        int BVWidth = (v.TypedIdent.Type as BvType).Bits;

-

-                        verifier.AddCandidateInvariant(wc,

-                                GPUVerifier.MakeBitVectorBinaryBoolean("BV" + BVWidth + "_GEQ",

-                                new IdentifierExpr(v.tok, v),

-                                new LiteralExpr(v.tok, BigNum.FromInt(0), BVWidth)), "loop guard variable non-negative");

-                    }

-                }

-            }

-        }

-

-        private bool IsBVType(Microsoft.Boogie.Type type)

-        {

-            return type.Equals(Microsoft.Boogie.Type.GetBvType(32))

-                || type.Equals(Microsoft.Boogie.Type.GetBvType(16))

-                || type.Equals(Microsoft.Boogie.Type.GetBvType(8));

-        }

-

         private void AddUserSuppliedInvariants(WhileCmd wc, List<Expr> UserSuppliedInvariants, Implementation Impl)

         {

             foreach (Expr e in UserSuppliedInvariants)

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index 48cd8a2f..1e0a6b4a 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -91,7 +91,7 @@ namespace GPUVerify
         public static bool doit(string filename, Variable v, int a1, int a2)

         {

             Program newProgram = parse();

-            RaceInstrumenterBase ri = CommandLineOptions.SetEncoding ? (RaceInstrumenterBase)new SetEncodingRaceInstrumenter() : (RaceInstrumenterBase) new ElementEncodingRaceInstrumenter();

+            RaceInstrumenterBase ri = new ElementEncodingRaceInstrumenter();

             GPUVerifier newGp = new GPUVerifier(filename, newProgram, ri);

             ri.setVerifier(newGp);

 

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

                 if (!CommandLineOptions.OnlyDivergence)

                 {

-                    RaceInstrumenterBase ri = CommandLineOptions.SetEncoding ? (RaceInstrumenterBase)new SetEncodingRaceInstrumenter() : (RaceInstrumenterBase)new ElementEncodingRaceInstrumenter();

+                    RaceInstrumenterBase ri = new ElementEncodingRaceInstrumenter();

                     ri.setVerifier(g);

                     g.setRaceInstrumenter(ri);

                 }

diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs
index b2941815..73f038fb 100644
--- a/Source/GPUVerify/NullRaceInstrumenter.cs
+++ b/Source/GPUVerify/NullRaceInstrumenter.cs
@@ -19,18 +19,14 @@ namespace GPUVerify
             

         }

 

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

-        {

-        }

-

         public bool AddRaceCheckingInstrumentation()

         {

             return true;

         }

 

-        public Microsoft.Boogie.BigBlock MakeRaceCheckingStatements(Microsoft.Boogie.IToken tok)

+        public Microsoft.Boogie.BigBlock MakeResetReadWriteSetsStatements(Microsoft.Boogie.IToken tok)

         {

-            return new BigBlock(tok, "__CheckForRaces", new CmdSeq(), null, null);

+            return new BigBlock(tok, "__ResetReadWriteSets", new CmdSeq(), null, null);

         }

 

         public void AddRaceCheckingCandidateRequires(Procedure Proc)

@@ -43,13 +39,7 @@ namespace GPUVerify
 

         }

 

-

-        public void AddNoRaceContract(Procedure proc)

-        {

-

-        }

-

-        public void AddNoRaceInvariants(Implementation impl)

+        public void AddRaceCheckingDeclarations()

         {

 

         }

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 33af1965..7ae7ca44 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -66,15 +66,13 @@ namespace GPUVerify
             if (verifier.ContainsBarrierCall(wc.Body))

             {

                 if (verifier.ContainsNamedVariable(

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

-                    || CommandLineOptions.AssignAtBarriers)

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

                 {

                     AddNoReadOrWriteCandidateInvariant(wc, v, "READ");

                 }

 

                 if (verifier.ContainsNamedVariable(

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

-                    || CommandLineOptions.AssignAtBarriers)

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

                 {

                     AddNoReadOrWriteCandidateInvariant(wc, v, "WRITE");

                 }

@@ -85,31 +83,17 @@ namespace GPUVerify
         {

             AddNoReadOrWriteCandidateRequires(Proc, v, "READ", "1");

             AddNoReadOrWriteCandidateRequires(Proc, v, "WRITE", "1");

-            if (!CommandLineOptions.Symmetry)

-            {

-                AddNoReadOrWriteCandidateRequires(Proc, v, "READ", "2");

-            }

-            AddNoReadOrWriteCandidateRequires(Proc, v, "WRITE", "2");

         }

 

         private void AddNoReadOrWriteCandidateEnsures(Procedure Proc, Variable v)

         {

             AddNoReadOrWriteCandidateEnsures(Proc, v, "READ", "1");

             AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "1");

-            if (!CommandLineOptions.Symmetry)

-            {

-                AddNoReadOrWriteCandidateEnsures(Proc, v, "READ", "2");

-            }

-            AddNoReadOrWriteCandidateEnsures(Proc, v, "WRITE", "2");

         }

 

         private void AddNoReadOrWriteCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)

         {

             Expr candidate = NoReadOrWriteExpr(v, ReadOrWrite, "1");

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

-            {

-                candidate = Expr.And(candidate, NoReadOrWriteExpr(v, ReadOrWrite, "2"));

-            }

             verifier.AddCandidateInvariant(wc, candidate, "no " + ReadOrWrite.ToLower());

         }

 

@@ -201,11 +185,6 @@ namespace GPUVerify
         private void AddAccessRelatedCandidateInvariant(WhileCmd wc, string accessKind, Expr candidateInvariantExpr, string procName, string tag)

         {

             Expr candidate = new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr);

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

-            {

-                candidate = Expr.And(candidate, new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(candidateInvariantExpr.Clone() as Expr));

-            }

-

             verifier.AddCandidateInvariant(wc, candidate, tag);

         }

 

@@ -733,23 +712,13 @@ namespace GPUVerify
         private void AddReadOrWrittenOffsetIsThreadIdCandidateRequires(Procedure Proc, Variable v)

         {

             AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 1);

-            AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "WRITE", 2);

             AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 1);

-            if (!CommandLineOptions.Symmetry)

-            {

-                AddAccessedOffsetIsThreadLocalIdCandidateRequires(Proc, v, "READ", 2);

-            }

         }

 

         private void AddReadOrWrittenOffsetIsThreadIdCandidateEnsures(Procedure Proc, Variable v)

         {

             AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "WRITE", 1);

-            AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "WRITE", 2);

             AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 1);

-            if (!CommandLineOptions.Symmetry)

-            {

-                AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Proc, v, "READ", 2);

-            }

         }

 

         protected abstract void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite);

@@ -777,6 +746,7 @@ namespace GPUVerify
                 AddRequiresNoPendingAccess(v);

             }

         }

+

         public bool AddRaceCheckingInstrumentation()

         {

 

@@ -802,24 +772,14 @@ namespace GPUVerify
             if (failedToFindSecondAccess || !addedLogWrite)

                 return false;

 

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

-            {

-                AddRaceCheckingDecsAndProcsForVar(v);

-            }

-

             return true;

 

         }

 

         private void AddRaceCheckingDecsAndProcsForVar(Variable v)

         {

-            IdentifierExprSeq ReadDeclsResetAtBarrier;

-            IdentifierExprSeq WriteDeclsResetAtBarrier;

-            IdentifierExprSeq ReadDeclsModifiedAtLogRead;

-            IdentifierExprSeq WriteDeclsModifiedAtLogWrite;

-                

-            AddLogRaceDeclarations(v, "READ", out ReadDeclsResetAtBarrier, out ReadDeclsModifiedAtLogRead);

-            AddLogRaceDeclarations(v, "WRITE", out WriteDeclsResetAtBarrier, out WriteDeclsModifiedAtLogWrite);

+            AddLogRaceDeclarations(v, "READ");

+            AddLogRaceDeclarations(v, "WRITE");

             AddLogAccessProcedure(v, "READ");

             AddLogAccessProcedure(v, "WRITE");

 

@@ -996,27 +956,20 @@ namespace GPUVerify
         }

 

 

-        protected abstract void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog);

+        protected abstract void AddLogRaceDeclarations(Variable v, string ReadOrWrite);

 

         protected abstract void AddLogAccessProcedure(Variable v, string ReadOrWrite);

 

 

-        public BigBlock MakeRaceCheckingStatements(IToken tok)

+        public BigBlock MakeResetReadWriteSetsStatements(IToken tok)

         {

-            BigBlock checkForRaces = new BigBlock(tok, "__CheckForRaces", new CmdSeq(), null, null);

-            if (!CommandLineOptions.Eager)

-            {

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

-                {

-                    CheckForRaces(checkForRaces, v, false);

-                }

-            }

+            BigBlock result = new BigBlock(tok, "__ResetReadWriteSets", new CmdSeq(), null, null);

 

             foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

             {

-                SetNoAccessOccurred(tok, checkForRaces, v);

+                SetNoAccessOccurred(tok, result, v);

             }

-            return checkForRaces;

+            return result;

         }

 

         private void SetNoAccessOccurred(IToken tok, BigBlock bb, Variable v)

@@ -1027,66 +980,33 @@ namespace GPUVerify
 

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

 

-        public abstract void CheckForRaces(BigBlock bb, Variable v, bool ReadWriteOnly);

-

-        protected void MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite, out Variable XParameterVariable, out Variable YParameterVariable, out Variable ZParameterVariable, out Procedure LogReadOrWriteProcedure)

+        protected Procedure MakeLogAccessProcedureHeader(Variable v, string ReadOrWrite)

         {

             VariableSeq inParams = new VariableSeq();

-            XParameterVariable = null;

-            YParameterVariable = null;

-            ZParameterVariable = null;

 

-            if (v.TypedIdent.Type is MapType)

-            {

-                MapType mt = v.TypedIdent.Type as MapType;

-                Debug.Assert(mt.Arguments.Length == 1);

+            Variable PredicateParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_P", Microsoft.Boogie.Type.Bool));

 

-                XParameterVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "_X_index", mt.Arguments[0]));

-                if (mt.Result is MapType)

-                {

-                    MapType mt2 = mt.Result as MapType;

-                    Debug.Assert(mt2.Arguments.Length == 1);

-                    Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));

-                    YParameterVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "_Y_index", mt2.Arguments[0]));

-                    if (mt2.Result is MapType)

-                    {

-                        MapType mt3 = mt2.Arguments[0] as MapType;

-                        Debug.Assert(mt3.Arguments.Length == 1);

-                        Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));

-                        Debug.Assert(!(mt3.Result is MapType));

-                        ZParameterVariable = new LocalVariable(v.tok, new TypedIdent(v.tok, "_Z_index", mt3.Arguments[0]));

-                    }

-                }

-            }

+            Debug.Assert(v.TypedIdent.Type is MapType);

+            MapType mt = v.TypedIdent.Type as MapType;

+            Debug.Assert(mt.Arguments.Length == 1);

+            Variable OffsetParameter = new LocalVariable(v.tok, new TypedIdent(v.tok, "_offset", mt.Arguments[0]));

+            Debug.Assert(!(mt.Result is MapType));

 

-            if (ZParameterVariable != null)

-            {

-                inParams.Add(ZParameterVariable);

-            }

-

-            if (YParameterVariable != null)

-            {

-                inParams.Add(YParameterVariable);

-            }

+            inParams.Add(new VariableDualiser(1, null, null).VisitVariable(PredicateParameter.Clone() as Variable));

+            inParams.Add(new VariableDualiser(1, null, null).VisitVariable(OffsetParameter.Clone() as Variable));

 

-            if (XParameterVariable != null)

-            {

-                inParams.Add(XParameterVariable);

-            }

+            inParams.Add(new VariableDualiser(2, null, null).VisitVariable(PredicateParameter.Clone() as Variable));

+            inParams.Add(new VariableDualiser(2, null, null).VisitVariable(OffsetParameter.Clone() as Variable));

 

             string LogProcedureName = "_LOG_" + ReadOrWrite + "_" + v.Name;

 

-            LogReadOrWriteProcedure = GetLogAccessProcedure(v.tok, LogProcedureName);

+            Procedure result = GetLogAccessProcedure(v.tok, LogProcedureName);

 

-            LogReadOrWriteProcedure.InParams = inParams;

+            result.InParams = inParams;

 

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

-            {

-                verifier.HalfDualisedProcedureNames.Add(LogReadOrWriteProcedure.Name);

-            }

-

-            LogReadOrWriteProcedure.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

+            result.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

 

+            return result;

         }

 

         public void AddRaceCheckingCandidateRequires(Procedure Proc)

@@ -1119,81 +1039,6 @@ namespace GPUVerify
 

         protected abstract Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwo);

 

-

-        public void AddNoRaceContract(Procedure proc)

-        {

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

-            {

-                proc.Requires.Add(new Requires(false, Expr.Not(GenerateRaceCondition(v, "WRITE", "WRITE"))));

-                proc.Requires.Add(new Requires(false, Expr.Not(GenerateRaceCondition(v, "READ", "WRITE"))));

-                if (!CommandLineOptions.Symmetry)

-                {

-                    proc.Requires.Add(new Requires(false, Expr.Not(GenerateRaceCondition(v, "WRITE", "READ"))));

-                }

-

-                proc.Ensures.Add(new Ensures(false, Expr.Not(GenerateRaceCondition(v, "WRITE", "WRITE"))));

-                proc.Ensures.Add(new Ensures(false, Expr.Not(GenerateRaceCondition(v, "READ", "WRITE"))));

-                if (!CommandLineOptions.Symmetry)

-                {

-                    proc.Ensures.Add(new Ensures(false, Expr.Not(GenerateRaceCondition(v, "WRITE", "READ"))));

-                }

-            

-            }

-        }

-

-        public void AddNoRaceInvariants(Implementation impl)

-        {

-            AddNoRaceInvariants(impl.StructuredStmts);

-        }

-

-        private void AddNoRaceInvariants(StmtList stmtList)

-        {

-            foreach (BigBlock bb in stmtList.BigBlocks)

-            {

-                AddNoRaceInvariants(bb);

-            }

-        }

-

-        private void AddNoRaceInvariants(BigBlock bb)

-        {

-            if (bb.ec is WhileCmd)

-            {

-                WhileCmd wc = bb.ec as WhileCmd;

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

-                {

-                    wc.Invariants.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "WRITE", "WRITE"))));

-                    wc.Invariants.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "READ", "WRITE"))));

-                    if (!CommandLineOptions.Symmetry)

-                    {

-                        wc.Invariants.Add(new AssertCmd(v.tok, Expr.Not(GenerateRaceCondition(v, "WRITE", "READ"))));

-                    }

-                }

-

-                AddNoRaceInvariants(wc.Body);

-

-            }

-            else if (bb.ec is IfCmd)

-            {

-                AddNoRaceInvariants((bb.ec as IfCmd).thn);

-                if ((bb.ec as IfCmd).elseBlock != null)

-                {

-                    AddNoRaceInvariants((bb.ec as IfCmd).elseBlock);

-                }

-            }

-            else if (bb.ec is BreakCmd)

-            {

-                // Do nothing

-            }

-            else

-            {

-                Debug.Assert(bb.ec == null);

-            }

-        }

-

-

-        protected abstract Expr GenerateRaceCondition(Variable v, string FirstAccessType, string SecondAccessType);

-

-

         private HashSet<Expr> GetOffsetsAccessed(StmtList stmts, Variable v, string AccessType)

         {

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

@@ -1266,9 +1111,19 @@ namespace GPUVerify
             return result;

         }

 

+        public void AddRaceCheckingDeclarations()

+        {

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

+            {

+                AddRaceCheckingDecsAndProcsForVar(v);

+            }

+        }

+

+

     }

 

 

+

     class FindReferencesToNamedVariableVisitor : StandardVisitor

     {

         internal bool found = false;

@@ -1289,4 +1144,6 @@ namespace GPUVerify
         }

     }

 

+

+

 }

diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
deleted file mode 100644
index 2a684c98..00000000
--- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
+++ /dev/null
@@ -1,532 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Diagnostics;

-using Microsoft.Boogie;

-using Microsoft.Basetypes;

-

-namespace GPUVerify

-{

-    class SetEncodingRaceInstrumenter : RaceInstrumenterBase

-    {

-

-        protected override void AddLogRaceDeclarations(Variable v, String ReadOrWrite, out IdentifierExprSeq ResetAtBarrier, out IdentifierExprSeq ModifiedAtLog)

-        {

-            Variable AccessSet = MakeAccessSetVariable(v, ReadOrWrite);

-

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

-            {

-                verifier.HalfDualisedVariableNames.Add(AccessSet.Name);

-            }

-

-            verifier.Program.TopLevelDeclarations.Add(AccessSet);

-

-            ResetAtBarrier = new IdentifierExprSeq(new IdentifierExpr[] { new IdentifierExpr(v.tok, AccessSet) });

-            ModifiedAtLog = ResetAtBarrier;

-

-        }

-

-        private static Variable MakeAccessSetVariable(Variable v, String ReadOrWrite)

-        {

-            Microsoft.Boogie.Type SetType = GetAccessSetType(v);

-

-            Variable AccessSet = new GlobalVariable(v.tok, new TypedIdent(v.tok, MakeAccessSetName(v, ReadOrWrite), SetType));

-            return AccessSet;

-        }

-

-        private static Microsoft.Boogie.Type GetAccessSetType(Variable v)

-        {

-            Microsoft.Boogie.Type SetType;

-

-            if (v.TypedIdent.Type is MapType)

-            {

-                MapType mt = v.TypedIdent.Type as MapType;

-                Debug.Assert(mt.Arguments.Length == 1);

-                Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));

-

-                if (mt.Result is MapType)

-                {

-                    MapType mt2 = mt.Result as MapType;

-                    Debug.Assert(mt2.Arguments.Length == 1);

-                    Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));

-

-                    if (mt2.Result is MapType)

-                    {

-                        MapType mt3 = mt2.Arguments[0] as MapType;

-                        Debug.Assert(mt3.Arguments.Length == 1);

-                        Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));

-                        Debug.Assert(!(mt3.Result is MapType));

-                        SetType = new MapType(mt.tok, new TypeVariableSeq(), mt.Arguments,

-                            new MapType(mt2.tok, new TypeVariableSeq(), mt2.Arguments,

-                                new MapType(mt3.tok, new TypeVariableSeq(), mt3.Arguments,

-                                    Microsoft.Boogie.Type.Bool

-                                )

-                            )

-                        );

-

-                    }

-                    else

-                    {

-                        SetType = new MapType(mt.tok, new TypeVariableSeq(), mt.Arguments,

-                            new MapType(mt2.tok, new TypeVariableSeq(), mt2.Arguments,

-                                Microsoft.Boogie.Type.Bool

-                            )

-                        );

-                    }

-                }

-                else

-                {

-                    SetType = new MapType(mt.tok, new TypeVariableSeq(), mt.Arguments,

-                        Microsoft.Boogie.Type.Bool

-                    );

-                }

-            }

-            else

-            {

-                SetType = Microsoft.Boogie.Type.Bool;

-            }

-            return SetType;

-        }

-

-        private static string MakeAccessSetName(Variable v, String ReadOrWrite)

-        {

-            return "_" + ReadOrWrite + "_SET_" + v.Name;

-        }

-

-        protected override void AddLogAccessProcedure(Variable v, string ReadOrWrite)

-        {

-            Variable XParameterVariable;

-            Variable YParameterVariable;

-            Variable ZParameterVariable;

-            Procedure LogReadOrWriteProcedure;

-

-            MakeLogAccessProcedureHeader(v, ReadOrWrite, out XParameterVariable, out YParameterVariable, out ZParameterVariable, out LogReadOrWriteProcedure);

-

-            LogReadOrWriteProcedure.Modifies.Add(new IdentifierExpr(v.tok, MakeAccessSetVariable(v, ReadOrWrite)));

-

-            List<BigBlock> bigblocks = new List<BigBlock>();

-

-            CmdSeq simpleCmds = new CmdSeq();

-

-            List<Expr> trueExpr = new List<Expr>(new Expr[] { Expr.True });

-

-            if (v.TypedIdent.Type is MapType)

-            {

-                MapType mt = v.TypedIdent.Type as MapType;

-                Debug.Assert(mt.Arguments.Length == 1);

-                Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));

-

-                if (mt.Result is MapType)

-                {

-                    MapType mt2 = mt.Result as MapType;

-                    Debug.Assert(mt2.Arguments.Length == 1);

-                    Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));

-

-                    if (mt2.Result is MapType)

-                    {

-                        MapType mt3 = mt2.Arguments[0] as MapType;

-                        Debug.Assert(mt3.Arguments.Length == 1);

-                        Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));

-                        Debug.Assert(!(mt3.Result is MapType));

-

-                        simpleCmds.Add(

-                            new AssignCmd(v.tok,

-                                 new List<AssignLhs>(new AssignLhs[] {

-                                new MapAssignLhs(v.tok, 

-                                    new MapAssignLhs(v.tok, 

-                                        new MapAssignLhs(v.tok, 

-                                           new SimpleAssignLhs(v.tok, new IdentifierExpr(v.tok, MakeAccessSetVariable(v, ReadOrWrite)))

-                                            , new List<Expr>(new Expr[] {  new IdentifierExpr(v.tok, ZParameterVariable) }))

-                                            , new List<Expr>(new Expr[] {  new IdentifierExpr(v.tok, YParameterVariable) }))

-                                            , new List<Expr>(new Expr[] {  new IdentifierExpr(v.tok, XParameterVariable) }))

-                             }), trueExpr));

-

-                    }

-                    else

-                    {

-                        simpleCmds.Add(

-                            new AssignCmd(v.tok,

-                                 new List<AssignLhs>(new AssignLhs[] {

-                                new MapAssignLhs(v.tok, 

-                                    new MapAssignLhs(v.tok, 

-                                       new SimpleAssignLhs(v.tok, new IdentifierExpr(v.tok, MakeAccessSetVariable(v, ReadOrWrite)))

-                                        , new List<Expr>(new Expr[] {  new IdentifierExpr(v.tok, YParameterVariable) }))

-                                        , new List<Expr>(new Expr[] {  new IdentifierExpr(v.tok, XParameterVariable) }))

-                             }), trueExpr));

-                    }

-                }

-                else

-                {

-                    simpleCmds.Add(

-                        new AssignCmd(v.tok,

-                             new List<AssignLhs>(new AssignLhs[] {

-                                new MapAssignLhs(v.tok, 

-                                    new SimpleAssignLhs(v.tok, new IdentifierExpr(v.tok, MakeAccessSetVariable(v, ReadOrWrite)))

-                                    , new List<Expr>(new Expr[] {  new IdentifierExpr(v.tok, XParameterVariable) }))

-                             }), trueExpr));

-                }

-            }

-            else

-            {

-                simpleCmds.Add(new AssignCmd(v.tok, 

-                    new List<AssignLhs>(new AssignLhs[] { new SimpleAssignLhs(v.tok, new IdentifierExpr(v.tok, MakeAccessSetVariable(v, ReadOrWrite))) }), 

-                    trueExpr));

-            }

-

-

-            bigblocks.Add(new BigBlock(v.tok, "_LOG_" + ReadOrWrite + "", simpleCmds, null, null));

-

-            StmtList statements = new StmtList(bigblocks, v.tok);

-

-            Implementation LogReadOrWriteImplementation = new Implementation(v.tok, "_LOG_" + ReadOrWrite + "_" + v.Name, new TypeVariableSeq(), LogReadOrWriteProcedure.InParams, new VariableSeq(), new VariableSeq(), statements);

-            LogReadOrWriteImplementation.AddAttribute("inline", new object[] { new LiteralExpr(v.tok, BigNum.FromInt(1)) });

-

-            LogReadOrWriteImplementation.Proc = LogReadOrWriteProcedure;

-

-            verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteProcedure);

-            verifier.Program.TopLevelDeclarations.Add(LogReadOrWriteImplementation);

-        }

-

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

-        {

-            IdentifierExpr AccessSet1 = new IdentifierExpr(tok, new VariableDualiser(1, null, null).VisitVariable(

-                            MakeAccessSetVariable(v, AccessType)));

-            IdentifierExprSeq VariablesToHavoc = new IdentifierExprSeq();

-            VariablesToHavoc.Add(AccessSet1);

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

-            {

-                IdentifierExpr AccessSet2 = new IdentifierExpr(tok, new VariableDualiser(2, null, null).VisitVariable(

-                                MakeAccessSetVariable(v, AccessType)));

-                VariablesToHavoc.Add(AccessSet2);

-            }

-            bb.simpleCmds.Add(new HavocCmd(tok, VariablesToHavoc));

-

-            AddAssumeNoAccess(bb, v, AccessType);

-

-        }

-

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

-        {

-            if (!ReadWriteOnly)

-            {

-                AddRaceCheck(bb, v, "WRITE", "WRITE");

-            }

-            AddRaceCheck(bb, v, "READ", "WRITE");

-            if (!CommandLineOptions.Symmetry)

-            {

-                AddRaceCheck(bb, v, "WRITE", "READ");

-            }

-

-

-        }

-

-

-

-        private static Microsoft.Boogie.Type GetIndexType(Variable v, int index)

-        {

-            Debug.Assert(index == 1 || index == 2 || index == 3);

-

-            Debug.Assert(v.TypedIdent.Type is MapType);

-            MapType mt = v.TypedIdent.Type as MapType;

-            Debug.Assert(mt.Arguments.Length == 1);

-            Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));

-

-            if (index == 1)

-            {

-                return mt.Arguments[0];

-            }

-

-            Debug.Assert(mt.Result is MapType);

-            MapType mt2 = mt.Result as MapType;

-            Debug.Assert(mt2.Arguments.Length == 1);

-            Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));

-

-            if (index == 2)

-            {

-                return mt2.Arguments[0];

-            }

-

-            Debug.Assert(mt2.Result is MapType);

-            MapType mt3 = mt2.Arguments[0] as MapType;

-            Debug.Assert(mt3.Arguments.Length == 1);

-            Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));

-            Debug.Assert(!(mt3.Result is MapType));

-

-            Debug.Assert(index == 3);

-            return mt3.Arguments[0];

-        }

-

-        private void AddRaceCheck(BigBlock bb, Variable v, String Access1, String Access2)

-        {

-            Expr AssertExpr = GenerateRaceCondition(v, Access1, Access2);

-

-            bb.simpleCmds.Add(new AssertCmd(v.tok, AssertExpr));

-        }

-

-        protected override Expr GenerateRaceCondition(Variable v, String Access1, String Access2)

-        {

-            VariableSeq DummyVars1;

-            Expr SetExpr1 = AccessExpr(v, Access1, 1, out DummyVars1);

-

-            VariableSeq DummyVars2;

-            Expr SetExpr2 = AccessExpr(v, Access2, 2, out DummyVars2);

-

-            Debug.Assert(DummyVars1.Length == DummyVars2.Length);

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

-            {

-                Debug.Assert(DummyVars1[i].Name.Equals(DummyVars2[i].Name));

-            }

-

-            Expr AssertExpr = Expr.And(SetExpr1, SetExpr2);

-

-            if (Access1.Equals("WRITE") && Access2.Equals("WRITE") && !verifier.ArrayModelledAdversarially(v))

-            {

-                VariableSeq DummyVarsAccess1;

-                VariableSeq DummyVarsAccess2;

-                Expr IndexExpr1 = QuantifiedIndexExpr(v, new VariableDualiser(1, null, null).VisitVariable(v.Clone() as Variable), out DummyVarsAccess1);

-                Expr IndexExpr2 = QuantifiedIndexExpr(v, new VariableDualiser(2, null, null).VisitVariable(v.Clone() as Variable), out DummyVarsAccess2);

-                Debug.Assert(DummyVarsAccess1.Length == DummyVarsAccess2.Length);

-                Debug.Assert(DummyVars1.Length == DummyVarsAccess1.Length);

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

-                {

-                    Debug.Assert(DummyVarsAccess1[i].Name.Equals(DummyVarsAccess2[i].Name));

-                    Debug.Assert(DummyVars1[i].Name.Equals(DummyVarsAccess1[i].Name));

-                }

-                AssertExpr = Expr.And(AssertExpr, Expr.Neq(IndexExpr1, IndexExpr2));

-            }

-

-            AssertExpr = Expr.Not(AssertExpr);

-            if (DummyVars1.Length > 0)

-            {

-                AssertExpr = new ForallExpr(v.tok, DummyVars1, AssertExpr);

-            }

-            return AssertExpr;

-        }

-

-        private static void SetNameDeep(IdentifierExpr e, string name)

-        {

-            e.Name = e.Decl.Name = e.Decl.TypedIdent.Name = name;

-        }

-

-        private static LocalVariable MakeDummy(Variable v, int index)

-        {

-            return new LocalVariable(v.tok, new TypedIdent(v.tok, "__dummy", GetIndexType(v, index)));

-        }

-

-        private static void AddAssumeNoAccess(BigBlock bb, Variable v, String AccessType)

-        {

-            bb.simpleCmds.Add(new AssumeCmd(v.tok, NoAccessExpr(v, AccessType, 1)));

-

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

-            {

-                bb.simpleCmds.Add(new AssumeCmd(v.tok, NoAccessExpr(v, AccessType, 2)));

-            }

-        }

-

-        private static Expr NoAccessExpr(Variable v, String AccessType, int Thread)

-        {

-            VariableSeq DummyVars;

-            Expr result = AccessExpr(v, AccessType, Thread, out DummyVars);

-

-            result = Expr.Not(result);

-

-            if (DummyVars.Length > 0)

-            {

-                result = new ForallExpr(v.tok, DummyVars, result);

-            }

-            return result;

-

-        }

-

-        private static Expr AccessExpr(Variable v, String AccessType, int Thread, out VariableSeq DummyVars)

-        {

-            return QuantifiedIndexExpr(v, new VariableDualiser(Thread, null, null).VisitVariable(MakeAccessSetVariable(v, AccessType)), out DummyVars);

-        }

-

-        private static Expr QuantifiedIndexExpr(Variable v, Variable AccessSetVariable, out VariableSeq DummyVars)

-        {

-            DummyVars = new VariableSeq();

-            Expr result = new IdentifierExpr(v.tok, AccessSetVariable);

-

-            if (v.TypedIdent.Type is MapType)

-            {

-                IdentifierExprSeq DummyIdentifierExprs = new IdentifierExprSeq();

-                MapType mt = v.TypedIdent.Type as MapType;

-                Debug.Assert(mt.Arguments.Length == 1);

-                Debug.Assert(GPUVerifier.IsIntOrBv32(mt.Arguments[0]));

-

-                DummyVars.Add(MakeDummy(v, 1));

-                DummyIdentifierExprs.Add(new IdentifierExpr(v.tok, DummyVars[0]));

-                result = Expr.Select(result, new Expr[] { DummyIdentifierExprs[0] });

-

-                if (mt.Result is MapType)

-                {

-                    MapType mt2 = mt.Result as MapType;

-                    Debug.Assert(mt2.Arguments.Length == 1);

-                    Debug.Assert(GPUVerifier.IsIntOrBv32(mt2.Arguments[0]));

-

-                    DummyVars.Add(MakeDummy(v, 2));

-                    DummyIdentifierExprs.Add(new IdentifierExpr(v.tok, DummyVars[1]));

-                    result = Expr.Select(result, new Expr[] { DummyIdentifierExprs[1] });

-

-                    if (mt2.Result is MapType)

-                    {

-                        MapType mt3 = mt2.Arguments[0] as MapType;

-                        Debug.Assert(mt3.Arguments.Length == 1);

-                        Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));

-                        Debug.Assert(!(mt3.Result is MapType));

-

-                        DummyVars.Add(MakeDummy(v, 3));

-                        DummyIdentifierExprs.Add(new IdentifierExpr(v.tok, DummyVars[2]));

-                        result = Expr.Select(result, new Expr[] { DummyIdentifierExprs[2] });

-

-                        SetNameDeep(DummyIdentifierExprs[0], "__z");

-                        SetNameDeep(DummyIdentifierExprs[1], "__y");

-                        SetNameDeep(DummyIdentifierExprs[2], "__x");

-                    }

-                    else

-                    {

-                        SetNameDeep(DummyIdentifierExprs[0], "__y");

-                        SetNameDeep(DummyIdentifierExprs[1], "__x");

-                    }

-                }

-                else

-                {

-                    SetNameDeep(DummyIdentifierExprs[0], "__x");

-                }

-            }

-            return result;

-        }

-

-        private static Expr NoAccess0DExpr(IToken tok, Variable v, String AccessType, int Thread)

-        {

-            return Expr.Not(new IdentifierExpr(tok, new VariableDualiser(Thread, null, null).VisitVariable(MakeAccessSetVariable(v, AccessType))));

-        }

-

-

-        protected override void AddRequiresNoPendingAccess(Variable v)

-        {

-            verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "WRITE", 1)));

-            verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "WRITE", 2)));

-            verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "READ", 1)));

-            if(!CommandLineOptions.Symmetry)

-            {

-                verifier.KernelProcedure.Requires.Add(new Requires(false, NoAccessExpr(v, "READ", 2)));

-            }

-        }

-

-

-        protected override Expr NoReadOrWriteExpr(Variable v, string ReadOrWrite, string OneOrTwoString)

-        {

-            return NoAccessExpr(v, ReadOrWrite, Int32.Parse(OneOrTwoString));

-        }

-

-

-

-        protected override void AddAccessedOffsetIsThreadLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)

-        {

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

-

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

-            {

-                expr = Expr.And(expr, AccessOnlyAtThreadId(v, ReadOrWrite, 2));

-            }

-

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

-

-        }

-

-        protected override void AddAccessedOffsetIsThreadGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)

-        {

-            throw new NotImplementedException();

-        }

-

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

-        {

-            VariableSeq Dummies;

-            Expr Access = AccessExpr(v, ReadOrWrite, Thread, out Dummies);

-

-            if (Dummies.Length == 0)

-            {

-                return null;

-            }

-

-            Expr ImplicationLhs;

-

-            if (Dummies.Length == 1)

-            {

-                ImplicationLhs = Expr.Neq(new IdentifierExpr(v.tok, Dummies[0]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread)));

-            }

-            else if (Dummies.Length == 2)

-            {

-                if (!verifier.KernelHasIdY())

-                {

-                    return null;

-                }

-                ImplicationLhs = Expr.Or(

-                        Expr.Neq(new IdentifierExpr(v.tok, Dummies[1]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),

-                        Expr.Neq(new IdentifierExpr(v.tok, Dummies[0]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))

-                    );

-            }

-            else

-            {

-                Debug.Assert(Dummies.Length == 3);

-                if (!verifier.KernelHasIdZ())

-                {

-                    return null;

-                }

-                ImplicationLhs = Expr.Or(

-                    Expr.Or(

-                        Expr.Neq(new IdentifierExpr(v.tok, Dummies[2]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))),

-                        Expr.Neq(new IdentifierExpr(v.tok, Dummies[1]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))

-                    ),

-                    Expr.Neq(new IdentifierExpr(v.tok, Dummies[0]), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Z", Thread)))

-                );

-            }

-

-            return new ForallExpr(v.tok, Dummies, Expr.Imp(ImplicationLhs, Expr.Not(Access)));

-        }

-

-        protected override void AddAccessedOffsetIsThreadLocalIdCandidateRequires(Procedure Proc, Variable v, string ReadOrWrite, int Thread)

-        {

-            Expr expr = AccessOnlyAtThreadId(v, ReadOrWrite, Thread);

-

-            if (expr != null)

-            {

-                verifier.AddCandidateRequires(Proc, expr);

-            }

-        }

-

-        protected override void AddAccessedOffsetIsThreadLocalIdCandidateEnsures(Procedure Proc, Variable v, string ReadOrWrite, int Thread)

-        {

-            Expr expr = AccessOnlyAtThreadId(v, ReadOrWrite, Thread);

-

-            if (expr != null)

-            {

-                verifier.AddCandidateEnsures(Proc, expr);

-            }

-        }

-

-        protected override void AddAccessedOffsetIsThreadFlattened2DLocalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)

-        {

-            throw new NotImplementedException();

-        }

-

-        protected override void AddAccessedOffsetIsThreadFlattened2DGlobalIdCandidateInvariant(WhileCmd wc, Variable v, string ReadOrWrite)

-        {

-            throw new NotImplementedException();

-        }

-

-        protected override void AddAccessedOffsetInRangeCTimesLocalIdToCTimesLocalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite)

-        {

-            throw new NotImplementedException();

-        }

-

-        protected override void AddAccessedOffsetInRangeCTimesGlobalIdToCTimesGlobalIdPlusC(WhileCmd wc, Variable v, Expr constant, string ReadOrWrite)

-        {

-            throw new NotImplementedException();

-        }

-

-    }

-}