Generating useful, and guarateed by construction, postconditions and loop invariants for kenrel procedures.

7 files changed, 378 insertions, 472 deletions

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index bef0505e..99cc4b97 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -27,8 +27,6 @@ namespace GPUVerify
         public static bool Symmetry = false;

         public static bool SetEncoding = false;

 

-        public static bool RaceCheckingContract = false;

-

         public static int Parse(string[] args)

         {

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

@@ -113,11 +111,6 @@ namespace GPUVerify
                     Eager = true;

                     break;

 

-                    case "-raceCheckingContract":

-                    case "/raceCheckingContract":

-                    RaceCheckingContract = true;

-                    break;

-

                     case "-inference":

                     case "/inference":

                     Inference = true;

diff --git a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
index b17ca60f..84624e5d 100644
--- a/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/ElementEncodingRaceInstrumenter.cs
@@ -85,6 +85,8 @@ namespace GPUVerify
             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);

         }

@@ -189,9 +191,12 @@ namespace GPUVerify
             bb.simpleCmds.Add(new AssignCmd(tok, lhss, rhss));

         }

 

-        public override void CheckForRaces(IToken tok, BigBlock bb, Variable v)

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

         {

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

+            if (!ReadWriteOnly)

+            {

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

+            }

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

             if (!CommandLineOptions.Symmetry)

             {

@@ -229,9 +234,57 @@ namespace GPUVerify
                     ));

             }

 

+            if (FirstAccessType.Equals("WRITE") && SecondAccessType.Equals("WRITE") && !CommandLineOptions.FullAbstraction)

+            {

+                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).VisitVariable(v.Clone() as Variable));

+

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

+

+                result = Expr.Select(result,

+                    new Expr[] { new IdentifierExpr(v.tok, new VariableDualiser(OneOrTwo).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).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).VisitVariable(GPUVerifier.MakeOffsetZVariable(v, "WRITE"))) });

+

+                    }

+                }

+            }

+

+            return result;

+

+        }

+

         internal static GlobalVariable MakeReadOrWriteHasOccurredVariable(Variable v, string ReadOrWrite)

         {

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

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index c15327ca..5e33e78d 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -398,7 +398,7 @@ namespace GPUVerify
                     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(v.tok, bb, v);

+                        RaceInstrumenter.CheckForRaces(v.tok, 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)

@@ -463,18 +463,11 @@ namespace GPUVerify
                     }

 

                     AddCandidateRequires(Proc);

-                    if (CommandLineOptions.RaceCheckingContract)

-                    {

-                        RaceInstrumenter.AddRaceCheckingCandidateRequires(Proc);

-                    }

-

+                    RaceInstrumenter.AddRaceCheckingCandidateRequires(Proc);

                     AddUserSuppliedCandidateRequires(Proc, UserSuppliedInvariants);

 

                     AddCandidateEnsures(Proc);

-                    if (CommandLineOptions.RaceCheckingContract)

-                    {

-                        RaceInstrumenter.AddRaceCheckingCandidateEnsures(Proc);

-                    }

+                    RaceInstrumenter.AddRaceCheckingCandidateEnsures(Proc);

                     AddUserSuppliedCandidateEnsures(Proc, UserSuppliedInvariants);

 

                 }

@@ -987,35 +980,169 @@ namespace GPUVerify
             {

                 Debug.Assert(AssumeThreadIdsInRange != null);

 

-                KernelProcedure.Requires.Add(new Requires(false, AssumeDistinctThreads));

-                KernelProcedure.Requires.Add(new Requires(false, AssumeThreadIdsInRange));

+                foreach (Declaration D in Program.TopLevelDeclarations)

+                {

+                    if (!(D is Procedure))

+                    {

+                        continue;

+                    }

+                    Procedure Proc = D as Procedure;

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

+                    {

+                        continue;

+                    }

+

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

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

+                }

             }

             else

             {

                 Debug.Assert(AssumeThreadIdsInRange == null);

             }

 

+            foreach (Declaration D in Program.TopLevelDeclarations)

+            {

+                if (!(D is Implementation))

+                {

+                    continue;

+                }

+                Implementation Impl = D as Implementation;

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

+                {

+                    continue;

+                }

+                if (Impl.Proc == KernelProcedure)

+                {

+                    continue;

+                }

+

+                EnsureDisabledThreadHasNoEffect(Impl);

+

+            }

 

         }

 

-        private void GeneratePreconditionsForDimension(ref Expr AssumeDistinctThreads, ref Expr AssumeThreadIdsInRange, IToken tok, String dimension)

+        private void EnsureDisabledThreadHasNoEffect(Implementation Impl)

         {

-            if (KernelHasId(dimension))

+            foreach (IdentifierExpr iex in Impl.Proc.Modifies)

             {

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

+                // For some reason, this does not work well with maps

+                if (iex.Decl.TypedIdent.Type is MapType)

                 {

-                    KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetTileSize(dimension)), ZeroBV(tok))));

-                    KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumTiles(dimension)), ZeroBV(tok))));

-                    KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetTileId(dimension)), ZeroBV(tok))));

-                    KernelProcedure.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));

+                    continue;

                 }

-                else

+

+                Expr NoEffectExpr = Expr.Imp(

+                        Expr.Not(new IdentifierExpr(iex.tok, new LocalVariable(iex.tok, new TypedIdent(iex.tok, "_P$" + GetThreadSuffix(iex.Name), Microsoft.Boogie.Type.Bool)))),

+                        Expr.Eq(iex, new OldExpr(iex.tok, iex))

+                    );

+

+                Impl.Proc.Ensures.Add(new Ensures(false,

+                    NoEffectExpr

+                ));

+

+                AddInvariantToAllLoops(NoEffectExpr, Impl.StructuredStmts);

+

+            }

+

+            AddEnablednessInvariantToAllLoops(Impl.StructuredStmts);

+        }

+

+        private void AddEnablednessInvariantToAllLoops(StmtList stmtList)

+        {

+            foreach (BigBlock bb in stmtList.BigBlocks)

+            {

+                AddEnablednessInvariantToAllLoops(bb);

+            }

+        }

+

+        private void AddEnablednessInvariantToAllLoops(BigBlock bb)

+        {

+            if (bb.ec is WhileCmd)

+            {

+                WhileCmd wc = bb.ec as WhileCmd;

+                Debug.Assert(wc.Guard is NAryExpr);

+                Debug.Assert((wc.Guard as NAryExpr).Fun is BinaryOperator);

+                Debug.Assert((wc.Guard as NAryExpr).Args[0] is IdentifierExpr);

+                string LoopPredicate = ((wc.Guard as NAryExpr).Args[0] as IdentifierExpr).Name;

+                LoopPredicate = StripThreadIdentifier(LoopPredicate);

+

+                wc.Invariants.Add(

+                    new AssertCmd(wc.tok,

+                        Expr.Imp(

+                            Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, "_P$1", Microsoft.Boogie.Type.Bool)))),

+                            Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$1", Microsoft.Boogie.Type.Bool))))

+                    )));

+

+                wc.Invariants.Add(

+                    new AssertCmd(wc.tok,

+                        Expr.Imp(

+                            Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, "_P$2", Microsoft.Boogie.Type.Bool)))),

+                            Expr.Not(new IdentifierExpr(wc.tok, new LocalVariable(wc.tok, new TypedIdent(wc.tok, LoopPredicate + "$2", Microsoft.Boogie.Type.Bool))))

+                    )));

+

+                AddEnablednessInvariantToAllLoops(wc.Body);

+            }

+

+        }

+

+        private void AddInvariantToAllLoops(Expr Invariant, StmtList stmtList)

+        {

+            foreach (BigBlock bb in stmtList.BigBlocks)

+            {

+                AddInvariantToAllLoops(Invariant, bb);

+            }

+        }

+

+        private void AddInvariantToAllLoops(Expr Invariant, BigBlock bb)

+        {

+            if (bb.ec is WhileCmd)

+            {

+                WhileCmd wc = bb.ec as WhileCmd;

+                wc.Invariants.Add(new AssertCmd(wc.tok, Invariant));

+                AddInvariantToAllLoops(Invariant, wc.Body);

+            }

+            Debug.Assert(!(bb.ec is IfCmd));

+        }

+

+        private int GetThreadSuffix(string p)

+        {

+            return Int32.Parse(p.Substring(p.IndexOf("$") + 1, p.Length - (p.IndexOf("$") + 1)));

+        }

+

+        private void GeneratePreconditionsForDimension(ref Expr AssumeDistinctThreads, ref Expr AssumeThreadIdsInRange, IToken tok, String dimension)

+        {

+            if (KernelHasId(dimension))

+            {

+                foreach (Declaration D in Program.TopLevelDeclarations)

                 {

-                    KernelProcedure.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetTileSize(dimension)), Zero(tok))));

-                    KernelProcedure.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetNumTiles(dimension)), Zero(tok))));

-                    KernelProcedure.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, GetTileId(dimension)), Zero(tok))));

-                    KernelProcedure.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));

+                    if (!(D is Procedure))

+                    {

+                        continue;

+                    }

+                    Procedure Proc = D as Procedure;

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

+                    {

+                        continue;

+                    }

+

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

+                    {

+                        Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetTileSize(dimension)), ZeroBV(tok))));

+                        Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumTiles(dimension)), ZeroBV(tok))));

+                        Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetTileId(dimension)), ZeroBV(tok))));

+                        Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));

+                    }

+                    else

+                    {

+                        Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetTileSize(dimension)), Zero(tok))));

+                        Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetNumTiles(dimension)), Zero(tok))));

+                        Proc.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, GetTileId(dimension)), Zero(tok))));

+                        Proc.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, GetTileId(dimension)), new IdentifierExpr(tok, GetNumTiles(dimension)))));

+                    }

                 }

+

                 Expr AssumeThreadsDistinctInDimension =

                         Expr.Neq(

                         new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)),

@@ -1130,7 +1257,10 @@ namespace GPUVerify
                 List<BigBlock> returnbigblocks = new List<BigBlock>();

                 returnbigblocks.Add(new BigBlock(tok, "__Disabled", new CmdSeq(), null, new ReturnCmd(tok)));

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

-                checkNonDivergence.ec = new IfCmd(tok, Expr.And(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);

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

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

+                // fail if divergence has not been proved.

+                checkNonDivergence.ec = new IfCmd(tok, Expr.Or(Expr.Not(P1), Expr.Not(P2)), returnstatement, null, null);

             }

 

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

@@ -1152,6 +1282,8 @@ namespace GPUVerify
             BarrierImplementation.AddAttribute("inline", new object[] { new LiteralExpr(tok, BigNum.FromInt(1)) });

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

 

+            BarrierImplementation.Proc = BarrierProcedure;

+

             Program.TopLevelDeclarations.Add(BarrierImplementation);

         }

 

diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs
index 2540c9d7..9a1c0d8c 100644
--- a/Source/GPUVerify/IRaceInstrumenter.cs
+++ b/Source/GPUVerify/IRaceInstrumenter.cs
@@ -20,7 +20,7 @@ namespace GPUVerify
 

         BigBlock MakeRaceCheckingStatements(IToken tok);

 

-        void CheckForRaces(IToken tok, BigBlock bb, Variable v);

+        void CheckForRaces(IToken tok, BigBlock bb, Variable v, bool ReadWriteOnly);

 

         void AddRaceCheckingCandidateRequires(Procedure Proc);

 

diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs
index 3958a94e..a825a2eb 100644
--- a/Source/GPUVerify/NullRaceInstrumenter.cs
+++ b/Source/GPUVerify/NullRaceInstrumenter.cs
@@ -19,7 +19,7 @@ namespace GPUVerify
             

         }

 

-        public void CheckForRaces(IToken tok, BigBlock bb, Variable v)

+        public void CheckForRaces(IToken tok, BigBlock bb, Variable v, bool ReadWriteOnly)

         {

         }

 

diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 237c155e..4f2f76be 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -244,6 +244,7 @@ namespace GPUVerify
 

             foreach (Cmd c in bb.simpleCmds)

             {

+                result.simpleCmds.Add(c);

                 if (c is AssignCmd)

                 {

                     AssignCmd assign = c as AssignCmd;

@@ -313,7 +314,6 @@ namespace GPUVerify
 

 

                 }

-                result.simpleCmds.Add(c);

             }

 

             if (bb.ec is WhileCmd)

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

                 foreach (Variable v in NonLocalStateToCheck.getAllNonLocalVariables())

                 {

-                    CheckForRaces(tok, checkForRaces, v);

+                    CheckForRaces(tok, checkForRaces, v, false);

                 }

             }

 

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

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

 

-        public abstract void CheckForRaces(IToken tok, BigBlock bb, Variable v);

+        public abstract void CheckForRaces(IToken tok, 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)

         {

diff --git a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
index b3104609..e7e5854e 100644
--- a/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
+++ b/Source/GPUVerify/SetEncodingRaceInstrumenter.cs
@@ -182,6 +182,8 @@ namespace GPUVerify
             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);

         }

@@ -200,301 +202,168 @@ namespace GPUVerify
             }

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

 

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

+            AddAssumeNoAccess(bb, v, AccessType);

 

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

-

-                        Add3DAssumeNoAccess(tok, bb, v, AccessType, mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);

+        }

 

-                    }

-                    else

-                    {

-                        Add2DAssumeNoAccess(tok, bb, v, AccessType, mt.Arguments[0], mt2.Arguments[0]);

-                    }

-                }

-                else

-                {

-                    Add1DAssumeNoAccess(tok, bb, v, AccessType, mt.Arguments[0]);

-                }

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

+        {

+            if (!ReadWriteOnly)

+            {

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

             }

-            else

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

+            if (!CommandLineOptions.Symmetry)

             {

-                Add0DAssumeNoAccess(tok, bb, v, AccessType);

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

             }

-        }

 

-        public override void CheckForRaces(IToken tok, BigBlock bb, Variable v)

-        {

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

 

-                        Add3DRaceCheck(tok, bb, v, "WRITE", "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);

-                        Add3DRaceCheck(tok, bb, v, "READ", "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);

-                        if (!CommandLineOptions.Symmetry)

-                        {

-                            Add3DRaceCheck(tok, bb, v, "WRITE", "READ", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0]);

-                        }

 

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

+        {

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

 

-                    }

-                    else

-                    {

- 

-                        Add2DRaceCheck(tok, bb, v, "WRITE", "WRITE", mt.Arguments[0], mt2.Arguments[0]);

-                        Add2DRaceCheck(tok, bb, v, "READ", "WRITE", mt.Arguments[0], mt2.Arguments[0]);

-                        if (!CommandLineOptions.Symmetry)

-                        {

-                            Add2DRaceCheck(tok, bb, v, "WRITE", "READ", mt.Arguments[0], mt2.Arguments[0]);

-                        }

-                    }

-                }

-                else

-                {

-                    Add1DRaceCheck(tok, bb, v, "WRITE", "WRITE", mt.Arguments[0]);

-                    Add1DRaceCheck(tok, bb, v, "READ", "WRITE", mt.Arguments[0]);

-                    if (!CommandLineOptions.Symmetry)

-                    {

-                        Add1DRaceCheck(tok, bb, v, "WRITE", "READ", mt.Arguments[0]);

-                    }

-                }

-            }

-            else

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

             {

-                Add0DRaceCheck(tok, bb, v, "WRITE", "WRITE");

-                Add0DRaceCheck(tok, bb, v, "READ", "WRITE");

-                if (!CommandLineOptions.Symmetry)

-                {

-                    Add0DRaceCheck(tok, bb, v, "WRITE", "READ");

-                }

+                return mt.Arguments[0];

             }

-        }

 

-        private static void Add0DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2)

-        {

-            bb.simpleCmds.Add(new AssertCmd(tok, Expr.Not(Expr.And(

-                new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))),

-                new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2)))

-                ))));

-        }

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

 

-        private static void Add1DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2, Microsoft.Boogie.Type IndexType)

-        {

-            Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexType));

-            bb.simpleCmds.Add(new AssertCmd(tok,

-                new ForallExpr(tok, new VariableSeq(new Variable[] { DummyX }),

-                    Expr.Not(Expr.And(

-                        Expr.Select(new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))), new Expr[] { new IdentifierExpr(tok, DummyX) }),

-                        Expr.Select(new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2))), new Expr[] { new IdentifierExpr(tok, DummyX) })

-                    ))

-                )

-            ));

-        }

+            if (index == 2)

+            {

+                return mt2.Arguments[0];

+            }

 

-        private static void Add2DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)

-        {

-            Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));

-            Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeX));

-            bb.simpleCmds.Add(new AssertCmd(tok,

-                new ForallExpr(tok, new VariableSeq(new Variable[] { DummyY, DummyX }),

-                    Expr.Not(Expr.And(

-                        Expr.Select(

-                            Expr.Select(new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))), new Expr[] { new IdentifierExpr(tok, DummyY) }),

-                            new Expr[] { new IdentifierExpr(tok, DummyX) }

-                        ),

-                        Expr.Select(

-                            Expr.Select(new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2))), new Expr[] { new IdentifierExpr(tok, DummyY) }),

-                            new Expr[] { new IdentifierExpr(tok, DummyX) }

-                        )

-                    ))

-                )

-            ));

-        }

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

 

-        private static void Add3DRaceCheck(IToken tok, BigBlock bb, Variable v, String Access1, String Access2, Microsoft.Boogie.Type IndexTypeZ, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)

-        {

-            Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));

-            Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeX));

-            Variable DummyZ = new LocalVariable(tok, new TypedIdent(tok, "__z", IndexTypeX));

-            bb.simpleCmds.Add(new AssertCmd(tok,

-                new ForallExpr(tok, new VariableSeq(new Variable[] { DummyZ, DummyY, DummyX }),

-                    Expr.Not(Expr.And(

-                        Expr.Select(

-                            Expr.Select(

-                                Expr.Select(new IdentifierExpr(tok, new VariableDualiser(1).VisitVariable(MakeAccessSetVariable(v, Access1))), new Expr[] { new IdentifierExpr(tok, DummyZ) }),

-                                new Expr[] { new IdentifierExpr(tok, DummyY) }

-                            ),

-                            new Expr[] { new IdentifierExpr(tok, DummyX) }

-                        ),

-                        Expr.Select(

-                            Expr.Select(

-                                Expr.Select(new IdentifierExpr(tok, new VariableDualiser(2).VisitVariable(MakeAccessSetVariable(v, Access2))), new Expr[] { new IdentifierExpr(tok, DummyZ) }),

-                                new Expr[] { new IdentifierExpr(tok, DummyY) }

-                            ),

-                            new Expr[] { new IdentifierExpr(tok, DummyX) }

-                        )

-                    ))

-                )

-            ));

+            Debug.Assert(index == 3);

+            return mt3.Arguments[0];

         }

 

-

-        private static void Add0DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType)

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

         {

-            bb.simpleCmds.Add(new AssumeCmd(tok,

-                NoAccess0DExpr(tok, v, AccessType, 1)

-            ));

-

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

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

             {

-                bb.simpleCmds.Add(new AssumeCmd(tok,

-                    NoAccess0DExpr(tok, v, AccessType, 2)

-                ));

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

             }

-        }

 

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

 

-        private static void Add1DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeX)

-        {

-            Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));

-            bb.simpleCmds.Add(new AssumeCmd(tok,

-                NoAccess1DExpr(tok, v, AccessType, IndexTypeX, 1)

-            ));

+            if (Access1.Equals("WRITE") && Access2.Equals("WRITE") && !CommandLineOptions.FullAbstraction)

+            {

+                VariableSeq DummyVarsAccess1;

+                VariableSeq DummyVarsAccess2;

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

+                Expr IndexExpr2 = QuantifiedIndexExpr(v, new VariableDualiser(2).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));

+            }

 

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

+            AssertExpr = Expr.Not(AssertExpr);

+            if (DummyVars1.Length > 0)

             {

-                bb.simpleCmds.Add(new AssumeCmd(tok,

-                    NoAccess1DExpr(tok, v, AccessType, IndexTypeX, 2)

-                ));

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

             }

-        }

 

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

+        }

 

-        private static void Add2DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)

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

         {

-            Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));

-            Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeX));

-            bb.simpleCmds.Add(new AssumeCmd(tok,

-                NoAccess2DExpr(tok, v, AccessType, IndexTypeY, IndexTypeX, 1)

-            ));

-

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

-            {

-                bb.simpleCmds.Add(new AssumeCmd(tok,

-                    NoAccess2DExpr(tok, v, AccessType, IndexTypeY, IndexTypeX, 2)

-                ));

-            }

+            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 Add3DAssumeNoAccess(IToken tok, BigBlock bb, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeZ, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX)

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

         {

-            bb.simpleCmds.Add(new AssumeCmd(tok,

-                NoAccess3DExpr(tok, v, AccessType, IndexTypeZ, IndexTypeY, IndexTypeX, 1)

-            ));

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

 

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

             {

-                bb.simpleCmds.Add(new AssumeCmd(tok,

-                    NoAccess3DExpr(tok, v, AccessType, IndexTypeZ, IndexTypeY, IndexTypeX, 2)

-                ));

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

             }

         }

 

-        private static Expr NoAccess3DExpr(IToken tok, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeZ, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX, int Thread)

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

         {

-            Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));

-            Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeY));

-            Variable DummyZ = new LocalVariable(tok, new TypedIdent(tok, "__z", IndexTypeZ));

-            return new ForallExpr(tok, new VariableSeq(new Variable[] { DummyZ, DummyY, DummyX }),

-                                Expr.Not(

-                                    Expr.Select(

-                                        Expr.Select(

-                                            Expr.Select(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))), new Expr[] { new IdentifierExpr(tok, DummyZ) }),

-                                            new Expr[] { new IdentifierExpr(tok, DummyY) }

-                                        ),

-                                        new Expr[] { new IdentifierExpr(tok, DummyX) }

-                                    )

-                                )

-                            )

-            ;

-        }

+            VariableSeq DummyVars;

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

 

-        private static Expr NoAccess2DExpr(IToken tok, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeY, Microsoft.Boogie.Type IndexTypeX, int Thread)

-        {

-            Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));

-            Variable DummyY = new LocalVariable(tok, new TypedIdent(tok, "__y", IndexTypeY));

-            return new ForallExpr(tok, new VariableSeq(new Variable[] { DummyY, DummyX }),

-                                Expr.Not(

-                                    Expr.Select(

-                                        Expr.Select(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))), new Expr[] { new IdentifierExpr(tok, DummyY) }),

-                                        new Expr[] { new IdentifierExpr(tok, DummyX) }

-                                    )

-                                )

-                            )

-            ;

-        }

+            result = Expr.Not(result);

+

+            if (DummyVars.Length > 0)

+            {

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

+            }

+            return result;

 

-        private static Expr NoAccess1DExpr(IToken tok, Variable v, String AccessType, Microsoft.Boogie.Type IndexTypeX, int Thread)

-        {

-            Variable DummyX = new LocalVariable(tok, new TypedIdent(tok, "__x", IndexTypeX));

-            return new ForallExpr(tok, new VariableSeq(new Variable[] { DummyX }),

-                                Expr.Not(

-                                    Expr.Select(new IdentifierExpr(tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, AccessType))), new Expr[] { new IdentifierExpr(tok, DummyX) })

-                                )

-                            );

         }

 

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

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

         {

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

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

         }

 

-

-        protected override void AddRequiresNoPendingAccess(Variable v)

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

@@ -502,63 +371,42 @@ namespace GPUVerify
                         Debug.Assert(GPUVerifier.IsIntOrBv32(mt3.Arguments[0]));

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

 

-                        verifier.KernelProcedure.Requires.Add(new Requires(false,

-                            NoAccess3DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 1)));

-                        verifier.KernelProcedure.Requires.Add(new Requires(false,

-                            NoAccess3DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 2)));

-                        verifier.KernelProcedure.Requires.Add(new Requires(false,

-                            NoAccess3DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 1)));

-                        if (!CommandLineOptions.Symmetry)

-                        {

-                            verifier.KernelProcedure.Requires.Add(new Requires(false,

-                                NoAccess3DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], 2)));

-                        }

-

+                        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

                     {

-                        verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                            NoAccess2DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], 1)));

-                        verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                            NoAccess2DExpr(v.tok, v, "WRITE", mt.Arguments[0], mt2.Arguments[0], 2)));

-                        verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                            NoAccess2DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], 1)));

-                        if(!CommandLineOptions.Symmetry)

-                        {

-                            verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                                NoAccess2DExpr(v.tok, v, "READ", mt.Arguments[0], mt2.Arguments[0], 2)));

-                        }

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

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

                     }

                 }

                 else

                 {

-                    verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                        NoAccess1DExpr(v.tok, v, "WRITE", mt.Arguments[0], 1)));

-                    verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                        NoAccess1DExpr(v.tok, v, "WRITE", mt.Arguments[0], 2)));

-                    verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                        NoAccess1DExpr(v.tok, v, "READ", mt.Arguments[0], 1)));

-                    if(!CommandLineOptions.Symmetry)

-                    {

-                        verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                            NoAccess1DExpr(v.tok, v, "READ", mt.Arguments[0], 2)));

-                    }

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

                 }

             }

-            else

+            return result;

+        }

+

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

+        {

+            return Expr.Not(new IdentifierExpr(tok, new VariableDualiser(Thread).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, 

-                    NoAccess0DExpr(v.tok, v, "WRITE", 1)));

-                verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                    NoAccess0DExpr(v.tok, v, "WRITE", 2)));

-                verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                    NoAccess0DExpr(v.tok, v, "READ", 1)));

-                if(!CommandLineOptions.Symmetry)

-                {

-                    verifier.KernelProcedure.Requires.Add(new Requires(false, 

-                        NoAccess0DExpr(v.tok, v, "READ", 2)));

-                }

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

             }

         }

 

@@ -569,44 +417,7 @@ namespace GPUVerify
 

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

         {

-            int OneOrTwo = Int32.Parse(OneOrTwoString);

-            Expr expr = null;

-

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

-                        expr = NoAccess3DExpr(v.tok, v, ReadOrWrite, mt.Arguments[0], mt2.Arguments[0], mt3.Arguments[0], OneOrTwo);

-                    }

-                    else

-                    {

-                        expr = NoAccess2DExpr(v.tok, v, ReadOrWrite, mt.Arguments[0], mt2.Arguments[0], OneOrTwo);

-                    }

-                }

-                else

-                {

-                    expr = NoAccess1DExpr(v.tok, v, ReadOrWrite, mt.Arguments[0], OneOrTwo);

-                }

-            }

-            else

-            {

-                expr = NoAccess0DExpr(v.tok, v, ReadOrWrite, OneOrTwo);

-            }

-            return expr;

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

         }

 

 

@@ -623,131 +434,48 @@ namespace GPUVerify
 

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

         {

-            Expr expr = null;

+            VariableSeq Dummies;

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

 

-            if (v.TypedIdent.Type is MapType)

+            if (Dummies.Length == 0)

             {

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

+                return null;

+            }

 

-                        if (verifier.KernelHasIdZ() && mt.Arguments[0].Equals(verifier.GetTypeOfIdZ()) &&

-                            mt2.Arguments[0].Equals(verifier.GetTypeOfIdY()) &&

-                            mt3.Arguments[0].Equals(verifier.GetTypeOfIdX()))

-                        {

-                            expr = No3DAccessExceptAtThreadId(v, ReadOrWrite, Thread);

-                        }

+            Expr ImplicationLhs;

 

-                    }

-                    else

-                    {

-                        if (verifier.KernelHasIdY() && mt.Arguments[0].Equals(verifier.GetTypeOfIdY()) &&

-                            mt2.Arguments[0].Equals(verifier.GetTypeOfIdX()))

-                        {

-                            expr = No2DAccessExceptAtThreadId(v, ReadOrWrite, Thread);

-                        }

-                    }

-                }

-                else

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

                 {

-                    if (mt.Arguments[0].Equals(verifier.GetTypeOfIdX()))

-                    {

-                        expr = No1DAccessExceptAtThreadId(v, ReadOrWrite, Thread);

-                    }

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

+                    );

             }

-            return expr;

-        }

-

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

-        {

-            Variable DummyX = new LocalVariable(v.tok, new TypedIdent(v.tok, "__x", verifier.GetTypeOfIdX()));

-

-            return new ForallExpr(v.tok,

-                new VariableSeq(new Variable[] { DummyX }),

-                Expr.Imp(

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

-                    Expr.Not(

-                        Expr.Select(

-                            new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, ReadOrWrite))),

-                            new IdentifierExpr(v.tok, DummyX)

-                        )

-                    )

-                )

-            );

-        }

-

-

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

-        {

-            Variable DummyX = new LocalVariable(v.tok, new TypedIdent(v.tok, "__x", verifier.GetTypeOfIdX()));

-            Variable DummyY = new LocalVariable(v.tok, new TypedIdent(v.tok, "__y", verifier.GetTypeOfIdY()));

-

-            return new ForallExpr(v.tok,

-                new VariableSeq(new Variable[] { DummyY, DummyX }),

-                Expr.Imp(

-                    Expr.Or(

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

-                        Expr.Neq(new IdentifierExpr(v.tok, DummyY), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))

-                    ),

-

-                    Expr.Not(

-                        Expr.Select(

-                            Expr.Select(

-                                new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, ReadOrWrite))),

-                                new IdentifierExpr(v.tok, DummyY)

-                            ),

-                            new IdentifierExpr(v.tok, DummyX)

-                        )

-                    )

-                )

-            );

-        }

-

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

-        {

-            Variable DummyX = new LocalVariable(v.tok, new TypedIdent(v.tok, "__x", verifier.GetTypeOfIdX()));

-            Variable DummyY = new LocalVariable(v.tok, new TypedIdent(v.tok, "__y", verifier.GetTypeOfIdY()));

-            Variable DummyZ = new LocalVariable(v.tok, new TypedIdent(v.tok, "__z", verifier.GetTypeOfIdY()));

-

-            return new ForallExpr(v.tok,

-                new VariableSeq(new Variable[] { DummyY, DummyX }),

-                Expr.Imp(

+            else

+            {

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

+                if (!verifier.KernelHasIdZ())

+                {

+                    return null;

+                }

+                ImplicationLhs = Expr.Or(

                     Expr.Or(

-                        Expr.Or(

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

-                            Expr.Neq(new IdentifierExpr(v.tok, DummyY), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Y", Thread)))

-                        ),

-                        Expr.Neq(new IdentifierExpr(v.tok, DummyZ), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "Z", Thread)))

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

+                );

+            }

 

-                    Expr.Not(

-                        Expr.Select(

-                            Expr.Select(

-                                Expr.Select(

-                                    new IdentifierExpr(v.tok, new VariableDualiser(Thread).VisitVariable(MakeAccessSetVariable(v, ReadOrWrite))),

-                                    new IdentifierExpr(v.tok, DummyZ)

-                                ),

-                                new IdentifierExpr(v.tok, DummyY)

-                            ),

-                            new IdentifierExpr(v.tok, DummyX)

-                        )

-                    )

-                )

-            );

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

         }

 

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