GPUVerify only generates _READ/WRITE_OFFSET variabls if they do not already exist. Did some tidying up of old source code - removed functions related to Y and Z offsets which we do not use any more.

4 files changed, 43 insertions, 268 deletions

diff --git a/Source/GPUVerify/AccessInvariantProcessor.cs b/Source/GPUVerify/AccessInvariantProcessor.cs
deleted file mode 100644
index 16833b09..00000000
--- a/Source/GPUVerify/AccessInvariantProcessor.cs
+++ /dev/null
@@ -1,103 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using Microsoft.Boogie;

-using System.Diagnostics;

-

-namespace GPUVerify

-{

-    class AccessInvariantProcessor : StandardVisitor

-    {

-

-        private const string NO_READ = "__no_read_";

-        private const string NO_WRITE = "__no_write_";

-        private const string READ = "__read_";

-        private const string WRITE = "__write_";

-        private const string READ_OFFSET = "__read_offset_";

-        private const string WRITE_OFFSET = "__write_offset_";

-        private const string READ_IMPLIES = "__read_implies_";

-        private const string WRITE_IMPLIES = "__write_implies_";

-

-        public override Expr VisitNAryExpr(NAryExpr node)

-        {

-

-            if (node.Fun is FunctionCall)

-            {

-                FunctionCall call = node.Fun as FunctionCall;

-

-                if (MatchesIntrinsic(call.Func, READ_OFFSET))

-                {

-                    return new IdentifierExpr(node.tok, new GlobalVariable(

-                            node.tok, new TypedIdent(node.tok, "_READ_OFFSET_X_" +

-                                call.Func.Name.Substring(READ_OFFSET.Length), Microsoft.Boogie.Type.GetBvType(32)))

-                    );

-                }

-

-                if (MatchesIntrinsic(call.Func, WRITE_OFFSET))

-                {

-                    return new IdentifierExpr(node.tok, new GlobalVariable(

-                            node.tok, new TypedIdent(node.tok, "_WRITE_OFFSET_X_" +

-                                call.Func.Name.Substring(WRITE_OFFSET.Length), Microsoft.Boogie.Type.GetBvType(32)))

-                    );

-                }

-

-                if (MatchesIntrinsic(call.Func, READ_IMPLIES))

-                {

-                    return Expr.Imp(MakeReadHasOccurred(call, READ_IMPLIES), VisitExpr(node.Args[0]));

-                }

-

-                if (MatchesIntrinsic(call.Func, WRITE_IMPLIES))

-                {

-                    return Expr.Imp(MakeWriteHasOccurred(call, WRITE_IMPLIES), VisitExpr(node.Args[0]));

-                }

-

-                if (MatchesIntrinsic(call.Func, NO_READ))

-                {

-                    return Expr.Not(

-                        MakeReadHasOccurred(call, NO_READ)

-                    );

-                }

-

-                if (MatchesIntrinsic(call.Func, NO_WRITE))

-                {

-                    return Expr.Not(

-                        MakeWriteHasOccurred(call, NO_WRITE)

-                    );

-                }

-

-                if (MatchesIntrinsic(call.Func, READ))

-                {

-                    return MakeReadHasOccurred(call, READ);

-                }

-

-                if (MatchesIntrinsic(call.Func, WRITE))

-                {

-                    return MakeWriteHasOccurred(call, WRITE);

-                }

-

-            }

-

-            return base.VisitNAryExpr(node);

-        }

-

-        private static IdentifierExpr MakeReadHasOccurred(FunctionCall call, string intrinsicPrefix)

-        {

-            return GPUVerifier.MakeAccessHasOccurredExpr(call.Func.Name.Substring(intrinsicPrefix.Length), "READ");

-        }

-

-        private static IdentifierExpr MakeWriteHasOccurred(FunctionCall call, string intrinsicPrefix)

-        {

-            return GPUVerifier.MakeAccessHasOccurredExpr(call.Func.Name.Substring(intrinsicPrefix.Length), "WRITE");

-        }

-

-

-        private bool MatchesIntrinsic(Function function, string intrinsicPrefix)

-        {

-            return function.Name.Length > intrinsicPrefix.Length &&

-                function.Name.Substring(0, intrinsicPrefix.Length).Equals(intrinsicPrefix);

-        }

-    

-    

-    }

-}

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 803e30d3..819eece5 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -389,8 +389,6 @@ namespace GPUVerify
                 return;

             }

 

-            ProcessAccessInvariants();

-

             if (CommandLineOptions.ShowStages)

             {

                 emitProgram(outputFilename + "_instrumented");

@@ -535,106 +533,6 @@ namespace GPUVerify
                 .ToDictionary(i => i, i => ReducedStrengthAnalysis.Analyse(this, i));

         }

 

-        private void ProcessAccessInvariants()

-        {

-            foreach (Declaration d in Program.TopLevelDeclarations)

-            {

-                if (d is Procedure)

-                {

-                    Procedure p = d as Procedure;

-                    p.Requires = ProcessAccessInvariants(p.Requires);

-                    p.Ensures = ProcessAccessInvariants(p.Ensures);

-                }

-

-                if (d is Implementation)

-                {

-                    Implementation i = d as Implementation;

-                    ProcessAccessInvariants(i.StructuredStmts);

-                }

-            }

-        }

-

-        private void ProcessAccessInvariants(StmtList stmtList)

-        {

-            

-            foreach (BigBlock bb in stmtList.BigBlocks)

-            {

-                ProcessAccessInvariants(bb);

-            }

-        }

-

-        private void ProcessAccessInvariants(BigBlock bb)

-        {

-            CmdSeq newCommands = new CmdSeq();

-

-            foreach (Cmd c in bb.simpleCmds)

-            {

-                if (c is AssertCmd)

-                {

-                    newCommands.Add(new AssertCmd(c.tok, new AccessInvariantProcessor().VisitExpr((c as AssertCmd).Expr.Clone() as Expr)));

-                }

-                else if (c is AssumeCmd)

-                {

-                    newCommands.Add(new AssumeCmd(c.tok, new AccessInvariantProcessor().VisitExpr((c as AssumeCmd).Expr.Clone() as Expr)));

-                }

-                else

-                {

-                    newCommands.Add(c);

-                }

-            }

-

-            bb.simpleCmds = newCommands;

-

-            if (bb.ec is WhileCmd)

-            {

-                WhileCmd whileCmd = bb.ec as WhileCmd;

-                whileCmd.Invariants = ProcessAccessInvariants(whileCmd.Invariants);

-                ProcessAccessInvariants(whileCmd.Body);

-            }

-            else if (bb.ec is IfCmd)

-            {

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

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

-                {

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

-                }

-            }

-        }

-

-        private List<PredicateCmd> ProcessAccessInvariants(List<PredicateCmd> invariants)

-        {

-            List<PredicateCmd> result = new List<PredicateCmd>();

-

-            foreach (PredicateCmd p in invariants)

-            {

-                PredicateCmd newP = new AssertCmd(p.tok, new AccessInvariantProcessor().VisitExpr(p.Expr.Clone() as Expr));

-                newP.Attributes = p.Attributes;

-                result.Add(newP);

-            }

-

-            return result;

-        }

-

-        private EnsuresSeq ProcessAccessInvariants(EnsuresSeq ensuresSeq)

-        {

-            EnsuresSeq result = new EnsuresSeq();

-            foreach (Ensures e in ensuresSeq)

-            {

-                result.Add(new Ensures(e.Free, new AccessInvariantProcessor().VisitExpr(e.Condition.Clone() as Expr)));

-            }

-            return result;

-        }

-

-        private RequiresSeq ProcessAccessInvariants(RequiresSeq requiresSeq)

-        {

-            RequiresSeq result = new RequiresSeq();

-            foreach (Requires r in requiresSeq)

-            {

-                result.Add(new Requires(r.Free, new AccessInvariantProcessor().VisitExpr(r.Condition.Clone() as Expr)));

-            }

-            return result;

-        }

-

         private void emitProgram(string filename)

         {

             using (TokenTextWriter writer = new TokenTextWriter(filename + ".bpl"))

@@ -1587,16 +1485,6 @@ namespace GPUVerify
             return false;

         }

 

-        public static bool HasYDimension(Variable v)

-        {

-            return v.TypedIdent.Type is MapType && (v.TypedIdent.Type as MapType).Result is MapType;

-        }

-

-        public static bool HasXDimension(Variable v)

-        {

-            return v.TypedIdent.Type is MapType;

-        }

-

         private BigBlock HavocSharedArray(Variable v, int thread)

         {

             IdentifierExpr vForThread = new IdentifierExpr(Token.NoToken, new VariableDualiser(thread, null, null).VisitVariable(v.Clone() as Variable));

@@ -1819,46 +1707,19 @@ namespace GPUVerify
 

         }

 

-

-

-

-

-

-        internal static GlobalVariable MakeOffsetZVariable(Variable v, string ReadOrWrite)

+        internal static string MakeOffsetVariableName(string Name, string AccessType)

         {

-            return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_OFFSET_Z_" + v.Name, IndexTypeOfZDimension(v)));

+            return "_" + AccessType + "_OFFSET_" + Name;

         }

 

-        internal static GlobalVariable MakeOffsetYVariable(Variable v, string ReadOrWrite)

+        internal static GlobalVariable MakeOffsetVariable(Variable v, string ReadOrWrite)

         {

-            return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_OFFSET_Y_" + v.Name, IndexTypeOfYDimension(v)));

+            return new GlobalVariable(v.tok, new TypedIdent(v.tok, MakeOffsetVariableName(v.Name, ReadOrWrite), IndexType(v)));

         }

 

-        internal static GlobalVariable MakeOffsetXVariable(Variable v, string ReadOrWrite)

+        public static Microsoft.Boogie.Type IndexType(Variable v)

         {

-            return new GlobalVariable(v.tok, new TypedIdent(v.tok, "_" + ReadOrWrite + "_OFFSET_X_" + v.Name, IndexTypeOfXDimension(v)));

-        }

-

-        public static Microsoft.Boogie.Type IndexTypeOfZDimension(Variable v)

-        {

-            Contract.Requires(HasZDimension(v));

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

-            MapType mt2 = mt.Result as MapType;

-            MapType mt3 = mt2.Result as MapType;

-            return mt3.Arguments[0];

-        }

-

-        public static Microsoft.Boogie.Type IndexTypeOfYDimension(Variable v)

-        {

-            Contract.Requires(HasYDimension(v));

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

-            MapType mt2 = mt.Result as MapType;

-            return mt2.Arguments[0];

-        }

-

-        public static Microsoft.Boogie.Type IndexTypeOfXDimension(Variable v)

-        {

-            Contract.Requires(HasXDimension(v));

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

             MapType mt = v.TypedIdent.Type as MapType;

             return mt.Arguments[0];

         }

@@ -1882,6 +1743,25 @@ namespace GPUVerify
 

         }

 

+        internal GlobalVariable FindOrCreateOffsetVariable(Variable v, string accessType)

+        {

+            string name = MakeOffsetVariableName(v.Name, accessType) + "$1";

+            foreach (Declaration D in Program.TopLevelDeclarations)

+            {

+                if (D is GlobalVariable && ((GlobalVariable)D).Name.Equals(name))

+                {

+                    return D as GlobalVariable;

+                }

+            }

+

+            GlobalVariable result = new VariableDualiser(1, null, null).VisitVariable(

+                MakeOffsetVariable(v, accessType)) as GlobalVariable;

+

+            Program.TopLevelDeclarations.Add(result);

+            return result;

+

+        }

+

         internal static GlobalVariable MakeAccessHasOccurredVariable(string varName, string accessType)

         {

             return new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, MakeAccessHasOccurredVariableName(varName, accessType), Microsoft.Boogie.Type.Bool));

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 9b3b08cb..d060ad8a 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -104,7 +104,6 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="AccessCollector.cs" />

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

     <Compile Include="AccessRecord.cs" />

     <Compile Include="ArrayControlFlowAnalyser.cs" />

     <Compile Include="AsymmetricExpressionFinder.cs" />

diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs
index 071440e5..b78730aa 100644
--- a/Source/GPUVerify/RaceInstrumenter.cs
+++ b/Source/GPUVerify/RaceInstrumenter.cs
@@ -122,7 +122,7 @@ namespace GPUVerify
 

         private List<Expr> CollectOffsetPredicates(Implementation impl, IRegion region, Variable v, string accessType)

         {

-            var offsetVar = new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, accessType));

+            var offsetVar = new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, accessType));

             var offsetExpr = new IdentifierExpr(Token.NoToken, offsetVar);

             var offsetPreds = new List<Expr>();

 

@@ -704,7 +704,7 @@ namespace GPUVerify
             Procedure LogAccessProcedure = MakeLogAccessProcedureHeader(v, Access);

 

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

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

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

 

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

 

@@ -734,15 +734,15 @@ namespace GPUVerify
             {

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

+                Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(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)), 

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

                                                 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(1, WriteOffsetVariable)), 1, "WRITE"),

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

                         ));

                 }

@@ -761,16 +761,16 @@ namespace GPUVerify
 

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

+                Variable WriteOffsetVariable = GPUVerifier.MakeOffsetVariable(v, "WRITE");

 

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

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

                                                 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(1, WriteOffsetVariable)), 1, "WRITE"),

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

                         ));

                 }

@@ -785,16 +785,16 @@ namespace GPUVerify
 

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

+                Variable ReadOffsetVariable = GPUVerifier.MakeOffsetVariable(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)),

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

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

                 if (!verifier.ArrayModelledAdversarially(v))

                 {

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

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

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

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

                         ));

                 }

@@ -830,14 +830,13 @@ namespace GPUVerify
 

         protected void AddLogRaceDeclarations(Variable v, String ReadOrWrite)

         {

-            Variable AccessHasOccurred = verifier.FindOrCreateAccessHasOccurredVariable(v.Name, ReadOrWrite);

+            verifier.FindOrCreateAccessHasOccurredVariable(v.Name, ReadOrWrite);

 

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

+            verifier.FindOrCreateOffsetVariable(v, ReadOrWrite);

 

         }

         

@@ -900,11 +899,11 @@ namespace GPUVerify
         private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread)

         {

             Expr expr = null;

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

+            if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX()))

             {

                 expr = Expr.Imp(

                         new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),

-                        Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetXVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));

+                        Expr.Eq(new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))), new IdentifierExpr(v.tok, verifier.MakeThreadId(v.tok, "X", Thread))));

             }

             return expr;

         }

@@ -912,12 +911,12 @@ namespace GPUVerify
         private Expr AccessedOffsetIsThreadGlobalIdExpr(Variable v, string ReadOrWrite, int Thread)

         {

             Expr expr = null;

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

+            if (GPUVerifier.IndexType(v).Equals(verifier.GetTypeOfIdX()))

             {

                 expr = Expr.Imp(

                         new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, ReadOrWrite))),

                         Expr.Eq(

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

+                            new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite))),

                             GlobalIdExpr("X", Thread)

                             )

                             );

@@ -961,7 +960,7 @@ namespace GPUVerify
 

         private static IdentifierExpr OffsetXExpr(Variable v, string ReadOrWrite, int Thread)

         {

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

+            return new IdentifierExpr(v.tok, new VariableDualiser(Thread, null, null).VisitVariable(GPUVerifier.MakeOffsetVariable(v, ReadOrWrite)));

         }

 

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