Added driver script and GPUVerify libary. The driver script works around the fact that Boogie does not do deep cloning of expressions when turning a structured program into an unstructured one.

6 files changed, 205 insertions, 31 deletions

diff --git a/Source/GPUVerify/BoogieLibrary/GPUVerifyLibrary.bpl b/Source/GPUVerify/BoogieLibrary/GPUVerifyLibrary.bpl
new file mode 100644
index 00000000..d553689f
--- /dev/null
+++ b/Source/GPUVerify/BoogieLibrary/GPUVerifyLibrary.bpl
@@ -0,0 +1,100 @@
+procedure {:barrier} BARRIER(); // Used to mark out barriers in the code; parameter simply lets us label each barrier

+

+type {:thread_id} ThreadId = Pair;

+

+type Pair;

+

+function constructPair(int, int) returns (Pair);

+function getX(Pair) returns (int);

+function getY(Pair) returns (int);

+

+axiom (forall x, y: int :: {constructPair(y, x)} (getX(constructPair(y, x)) == x) && (getY(constructPair(y, x)) == y));

+axiom (forall p: Pair :: {getX(p)} {getY(p)} constructPair(getY(p), getX(p)) == p);

+

+function {:inline} setX(p: Pair, x: int) returns (Pair)

+{

+    constructPair(getY(p), x)

+}

+

+function {:inline} setY(p: Pair, y: int) returns (Pair)

+{

+    constructPair(y, getX(p))

+}

+

+// Thread ids

+

+axiom BLOCK_X == BLOCK_SIZE;

+axiom BLOCK_Y == BLOCK_SIZE;

+axiom TILE_X == BLOCK_SIZE;

+axiom TILE_Y == BLOCK_SIZE;

+

+const BLOCK_X: int;

+const TILE_X: int;

+const NUM_TILES_X: int;

+axiom TILE_X*NUM_TILES_X == BLOCK_X;

+

+const BLOCK_Y: int;

+const TILE_Y: int;

+const NUM_TILES_Y: int;

+axiom TILE_Y*NUM_TILES_Y == BLOCK_Y;

+

+function {:inline} localId(t: ThreadId) returns (Pair)

+{

+  constructPair( mod(getY(t), TILE_Y ), mod(getX(t), TILE_X) )

+}

+

+function {:inline} tileId(t: ThreadId) returns (Pair)

+{

+  constructPair( div(getY(t), TILE_Y ), div(getX(t), TILE_X) )

+}

+

+function {:inline} distinct_same_tile(i: ThreadId, j: ThreadId) returns (bool)

+{

+  i != j && tileId(i) == tileId(j)

+}

+

+function {:builtin "div"} div(int, int) : int;

+function {:builtin "mod"} mod(int, int) : int;

+

+// These are the declarations that allow race and divergence checking

+

+var AT_BARRIER : [ThreadId]int;

+

+type ArrayBase;

+

+const unique nothing: ArrayBase;

+

+var base     : [ThreadId]ArrayBase;

+var offset_x : [ThreadId]int;

+var offset_y : [ThreadId]int;

+var offset_z : [ThreadId]int;

+var is_write : [ThreadId]bool;

+

+function race(b: [ThreadId]ArrayBase, z: [ThreadId]int, y: [ThreadId]int, x: [ThreadId]int, is_w: [ThreadId]bool, i: ThreadId, j: ThreadId) returns (bool)

+{

+  (is_w[i] || is_w[j]) && (b[i] != nothing && b[j] != nothing) && (b[i] == b[j]) && (z[i] == z[j]) && (y[i] == y[j]) && (x[i] == x[j])

+}

+

+procedure {:inline 1} LOG_READ(b: ArrayBase, z: int, y: int, x: int, i: ThreadId)

+modifies base, offset_z, offset_y, offset_x, is_write;

+{

+  if(*) {

+    base[i] := b;

+    offset_z[i] := z;

+    offset_y[i] := y;

+    offset_x[i] := x;

+    is_write[i] := false;

+  }

+}

+

+procedure {:inline 1} LOG_WRITE(b: ArrayBase, z: int, y: int, x: int, i: ThreadId)

+modifies base, offset_z, offset_y, offset_x, is_write;

+{

+  if(*) {

+    base[i] := b;

+    offset_z[i] := z;

+    offset_y[i] := y;

+    offset_x[i] := x;

+    is_write[i] := true;

+  }

+}

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 80dc18ef..812d9f20 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -3,6 +3,7 @@ using System.Collections.Generic;
 using System.Linq;

 using System.Text;

 using System.IO;

+using System.Diagnostics;

 

 namespace GPUVerify

 {

@@ -12,11 +13,41 @@ namespace GPUVerify
 

         public static List<string> inputFiles = new List<string>();

 

+        public static string outputFile = null;

+

         public static int Parse(string[] args)

         {

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

             {

-                inputFiles.Add(args[i]);

+                bool hasColonArgument = false;

+                string beforeColon;

+                string afterColon = null;

+                int colonIndex = args[i].IndexOf(':');

+                if (colonIndex >= 0 && (args[i].StartsWith("-") || args[i].StartsWith("/"))) {

+                    hasColonArgument = true;

+                    beforeColon = args[i].Substring(0, colonIndex);

+                    afterColon = args[i].Substring(colonIndex + 1);

+                } else {

+                    beforeColon = args[i];

+                }

+

+                switch (beforeColon)

+                {

+                    case "-print":

+                    case "/print":

+                        if (!hasColonArgument)

+                        {

+                            Console.WriteLine("Error: filename expected after " + beforeColon + " argument");

+                            Environment.Exit(1);

+                        }

+                        Debug.Assert(afterColon != null);

+                        outputFile = afterColon;

+                    break;

+

+                    default:

+                        inputFiles.Add(args[i]);

+                        break;

+                }

             }

             return 0;

         }

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 391d7bdf..f90e521e 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -181,16 +181,6 @@ namespace GPUVerify
 

             replacer.VisitImplementation(KernelImplementation);

 

-            Console.WriteLine("After replacement we have ");

-

-            using (TokenTextWriter writer = new TokenTextWriter("<console>", Console.Out))

-            {

-                KernelImplementation.Emit(writer, 1);

-            }

-

-            Environment.Exit(1);

-

-

             // Check that each barrier has a positive integer id

             // Check that these ids are all distinct

             foreach (Block B in KernelImplementation.Blocks)

@@ -527,6 +517,13 @@ namespace GPUVerify
 

             String NewProcedureName = "Barrier_" + GetBarrierId(B) + "_to_next_barriers";

             Procedure NewProcedure = new Procedure(KernelProcedure.tok, NewProcedureName, KernelProcedure.TypeParameters, KernelProcedure.InParams, KernelProcedure.OutParams, KernelProcedure.Requires, KernelProcedure.Modifies, KernelProcedure.Ensures);

+

+            NewProcedure.Modifies.Add(MakeBaseVariable(B.tok));

+            NewProcedure.Modifies.Add(MakeOffsetXVariable(B.tok));

+            NewProcedure.Modifies.Add(MakeOffsetYVariable(B.tok));

+            NewProcedure.Modifies.Add(MakeOffsetZVariable(B.tok));

+            NewProcedure.Modifies.Add(MakeIsWriteVariable(B.tok));

+

             Implementation NewImplementation = ConstructBarrierToNextBarriersImplementation(B, NewProcedureName);

 

             InstrumentWithRaceDetection(NewImplementation);

@@ -536,6 +533,47 @@ namespace GPUVerify
 

         }

 

+        private static CtorType MakeArrayBaseType(IToken tok)

+        {

+            return new CtorType(tok, new TypeCtorDecl(tok, "ArrayBase", 0), new TypeSeq());

+        }

+

+        private IdentifierExpr MakeBaseVariable(IToken tok)

+        {

+            TypeSeq typeSeq = new TypeSeq();

+            typeSeq.Add(ThreadIdType);

+            return new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "base", new MapType(tok, new TypeVariableSeq(), typeSeq, MakeArrayBaseType(tok)))));

+        }

+

+        private IdentifierExpr MakeOffsetVariable(IToken tok, string Dimension)

+        {

+            TypeSeq typeSeq = new TypeSeq();

+            typeSeq.Add(ThreadIdType);

+            return new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "offset_" + Dimension, new MapType(tok, new TypeVariableSeq(), typeSeq, Microsoft.Boogie.Type.Int))));

+        }

+

+        private IdentifierExpr MakeOffsetXVariable(IToken tok)

+        {

+            return MakeOffsetVariable(tok, "x");

+        }

+

+        private IdentifierExpr MakeOffsetYVariable(IToken tok)

+        {

+            return MakeOffsetVariable(tok, "y");

+        }

+

+        private IdentifierExpr MakeOffsetZVariable(IToken tok)

+        {

+            return MakeOffsetVariable(tok, "z");

+        }

+

+        private IdentifierExpr MakeIsWriteVariable(IToken tok)

+        {

+            TypeSeq typeSeq = new TypeSeq();

+            typeSeq.Add(ThreadIdType);

+            return new IdentifierExpr(tok, new GlobalVariable(tok, new TypedIdent(tok, "is_write", new MapType(tok, new TypeVariableSeq(), typeSeq, Microsoft.Boogie.Type.Bool))));

+        }

+

         private void InstrumentWithRaceDetection(Implementation Impl)

         {

             foreach (Block B in Impl.Blocks)

@@ -839,6 +877,19 @@ namespace GPUVerify
         }

 

 

+

+        internal void AddArrayBaseDeclarations()

+        {

+            foreach (Variable V in GetGlobalVariables())

+            {

+                Program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V.tok)), true));

+            }

+

+            foreach (Variable V in GetTileStaticVariables())

+            {

+                Program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V.tok)), true));

+            }

+        }

     }

 

 }

diff --git a/Source/GPUVerify/LocalVariableAccessReplacer.cs b/Source/GPUVerify/LocalVariableAccessReplacer.cs
index 4ec382ad..64dde7dc 100644
--- a/Source/GPUVerify/LocalVariableAccessReplacer.cs
+++ b/Source/GPUVerify/LocalVariableAccessReplacer.cs
@@ -33,16 +33,11 @@ namespace GPUVerify
         {

             if (verifier.GetThreadLocalVariables().Contains(node.Decl))

             {

-                Console.WriteLine("Replacing " + node);

-

                 ExprSeq MapNameAndThreadID = new ExprSeq();

                 MapNameAndThreadID.Add(new IdentifierExpr(node.tok, node.Decl));

                 MapNameAndThreadID.Add(verifier.MakeThreadIdExpr(node.tok));

 

-                Expr result = new NAryExpr(node.tok, new MapSelect(node.tok, 1), MapNameAndThreadID);

-

-                Console.WriteLine("with " + result);

-                return result;

+                return new NAryExpr(node.tok, new MapSelect(node.tok, 1), MapNameAndThreadID);

 

             }

 

diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index 7c72a87c..a0576f45 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -71,17 +71,9 @@ namespace GPUVerify
 

             verifier.ComputeBarrierToBarrierPairs();

 

-            foreach (Variable V in verifier.GetGlobalVariables())

-            {

-                program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V)), true));

-            }

+            verifier.AddArrayBaseDeclarations();

 

-            foreach (Variable V in verifier.GetTileStaticVariables())

-            {

-                program.TopLevelDeclarations.Add(new Constant(V.tok, new TypedIdent(V.tok, V.Name + "_base", MakeArrayBaseType(V)), true));

-            }

-

-            using (TokenTextWriter writer = new TokenTextWriter("<console>", Console.Out))

+            using (TokenTextWriter writer = (CommandLineOptions.outputFile == null ? new TokenTextWriter("<console>", Console.Out) : new TokenTextWriter(CommandLineOptions.outputFile)))

             {

                 program.Emit(writer);

             }

@@ -106,10 +98,6 @@ namespace GPUVerify
 

         }

 

-        private static CtorType MakeArrayBaseType(Variable V)

-        {

-            return new CtorType(V.tok, new TypeCtorDecl(V.tok, "ArrayBase", 0), new TypeSeq());

-        }

 

 

 

diff --git a/Source/GPUVerify/Scripts/GPUVerifyDriver.bat b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat
new file mode 100644
index 00000000..dda5ddcf
--- /dev/null
+++ b/Source/GPUVerify/Scripts/GPUVerifyDriver.bat
@@ -0,0 +1,9 @@
+echo off

+

+Boogie /noVerify /printUnstructured /print:temp_instrumented.bpl %1 %~p0..\BoogieLibrary\GPUVerifyLibrary.bpl

+

+GPUVerify temp_unstructured.bpl /print:temp_ready_to_verify.bpl

+

+Boogie temp_ready_to_verify.bpl /prover:smtlib

+

+del temp_instrumented.bpl