summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/GPUVerify/BoogieLibrary/GPUVerifyLibrary.bpl100
-rw-r--r--Source/GPUVerify/CommandLineOptions.cs33
-rw-r--r--Source/GPUVerify/GPUVerifier.cs71
-rw-r--r--Source/GPUVerify/LocalVariableAccessReplacer.cs7
-rw-r--r--Source/GPUVerify/Main.cs16
-rw-r--r--Source/GPUVerify/Scripts/GPUVerifyDriver.bat9
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 10:47:36 +0000