summaryrefslogtreecommitdiff
path: root/Source/GPUVerify
diff options
context:
space:
mode:
Diffstat (limited to 'Source/GPUVerify')
-rw-r--r--Source/GPUVerify/GPUVerifier.cs260
-rw-r--r--Source/GPUVerify/INonLocalState.cs2
-rw-r--r--Source/GPUVerify/Main.cs6
-rw-r--r--Source/GPUVerify/NonLocalStateLists.cs10
-rw-r--r--Source/GPUVerify/RaceInstrumenterBase.cs4
5 files changed, 126 insertions, 156 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 5e33e78d..f1d06590 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -37,29 +37,29 @@ namespace GPUVerify
private const string _Y_name = "_Y";
private const string _Z_name = "_Z";
- private Constant _TILE_SIZE_X = null;
- private Constant _TILE_SIZE_Y = null;
- private Constant _TILE_SIZE_Z = null;
+ private Constant _GROUP_SIZE_X = null;
+ private Constant _GROUP_SIZE_Y = null;
+ private Constant _GROUP_SIZE_Z = null;
- private const string _TILE_SIZE_X_name = "_TILE_SIZE_X";
- private const string _TILE_SIZE_Y_name = "_TILE_SIZE_Y";
- private const string _TILE_SIZE_Z_name = "_TILE_SIZE_Z";
+ private const string _GROUP_SIZE_X_name = "_GROUP_SIZE_X";
+ private const string _GROUP_SIZE_Y_name = "_GROUP_SIZE_Y";
+ private const string _GROUP_SIZE_Z_name = "_GROUP_SIZE_Z";
- private Constant _TILE_X = null;
- private Constant _TILE_Y = null;
- private Constant _TILE_Z = null;
+ private Constant _GROUP_X = null;
+ private Constant _GROUP_Y = null;
+ private Constant _GROUP_Z = null;
- private const string _TILE_X_name = "_TILE_X";
- private const string _TILE_Y_name = "_TILE_Y";
- private const string _TILE_Z_name = "_TILE_Z";
+ private const string _GROUP_X_name = "_GROUP_X";
+ private const string _GROUP_Y_name = "_GROUP_Y";
+ private const string _GROUP_Z_name = "_GROUP_Z";
- private Constant _NUM_TILES_X = null;
- private Constant _NUM_TILES_Y = null;
- private Constant _NUM_TILES_Z = null;
+ private Constant _NUM_GROUPS_X = null;
+ private Constant _NUM_GROUPS_Y = null;
+ private Constant _NUM_GROUPS_Z = null;
- private const string _NUM_TILES_X_name = "_NUM_TILES_X";
- private const string _NUM_TILES_Y_name = "_NUM_TILES_Y";
- private const string _NUM_TILES_Z_name = "_NUM_TILES_Z";
+ private const string _NUM_GROUPS_X_name = "_NUM_GROUPS_X";
+ private const string _NUM_GROUPS_Y_name = "_NUM_GROUPS_Y";
+ private const string _NUM_GROUPS_Z_name = "_NUM_GROUPS_Z";
public IRaceInstrumenter RaceInstrumenter;
@@ -113,6 +113,11 @@ namespace GPUVerify
continue;
}
+ if (decl is Implementation)
+ {
+ continue;
+ }
+
if (decl is Procedure)
{
if (attributedProcedure == null)
@@ -143,9 +148,9 @@ namespace GPUVerify
{
foreach (LocalVariable LV in KernelImplementation.LocVars)
{
- if (QKeyValue.FindBoolAttribute(LV.Attributes, "tile_static"))
+ if (QKeyValue.FindBoolAttribute(LV.Attributes, "group_shared"))
{
- Error(LV.tok, "Local variable must not be marked 'tile_static' -- promote the variable to global scope");
+ Error(LV.tok, "Local variable must not be marked 'group_shared' -- promote the variable to global scope");
}
}
}
@@ -158,11 +163,11 @@ namespace GPUVerify
{
if (!ReservedNames.Contains((D as Variable).Name))
{
- if (QKeyValue.FindBoolAttribute(D.Attributes, "tile_static"))
+ if (QKeyValue.FindBoolAttribute(D.Attributes, "group_shared"))
{
- NonLocalState.getTileStaticVariables().Add(D as Variable);
+ NonLocalState.getGroupSharedVariables().Add(D as Variable);
}
- else
+ else if(QKeyValue.FindBoolAttribute(D.Attributes, "global"))
{
NonLocalState.getGlobalVariables().Add(D as Variable);
}
@@ -186,50 +191,50 @@ namespace GPUVerify
CheckSpecialConstantType(C);
_Z = C;
}
- if (C.Name.Equals(_TILE_SIZE_X_name))
+ if (C.Name.Equals(_GROUP_SIZE_X_name))
{
CheckSpecialConstantType(C);
- _TILE_SIZE_X = C;
+ _GROUP_SIZE_X = C;
}
- if (C.Name.Equals(_TILE_SIZE_Y_name))
+ if (C.Name.Equals(_GROUP_SIZE_Y_name))
{
CheckSpecialConstantType(C);
- _TILE_SIZE_Y = C;
+ _GROUP_SIZE_Y = C;
}
- if (C.Name.Equals(_TILE_SIZE_Z_name))
+ if (C.Name.Equals(_GROUP_SIZE_Z_name))
{
CheckSpecialConstantType(C);
- _TILE_SIZE_Z = C;
+ _GROUP_SIZE_Z = C;
}
- if (C.Name.Equals(_TILE_X_name))
+ if (C.Name.Equals(_GROUP_X_name))
{
CheckSpecialConstantType(C);
- _TILE_X = C;
+ _GROUP_X = C;
}
- if (C.Name.Equals(_TILE_Y_name))
+ if (C.Name.Equals(_GROUP_Y_name))
{
CheckSpecialConstantType(C);
- _TILE_Y = C;
+ _GROUP_Y = C;
}
- if (C.Name.Equals(_TILE_Z_name))
+ if (C.Name.Equals(_GROUP_Z_name))
{
CheckSpecialConstantType(C);
- _TILE_Z = C;
+ _GROUP_Z = C;
}
- if (C.Name.Equals(_NUM_TILES_X_name))
+ if (C.Name.Equals(_NUM_GROUPS_X_name))
{
CheckSpecialConstantType(C);
- _NUM_TILES_X = C;
+ _NUM_GROUPS_X = C;
}
- if (C.Name.Equals(_NUM_TILES_Y_name))
+ if (C.Name.Equals(_NUM_GROUPS_Y_name))
{
CheckSpecialConstantType(C);
- _NUM_TILES_Y = C;
+ _NUM_GROUPS_Y = C;
}
- if (C.Name.Equals(_NUM_TILES_Z_name))
+ if (C.Name.Equals(_NUM_GROUPS_Z_name))
{
CheckSpecialConstantType(C);
- _NUM_TILES_Z = C;
+ _NUM_GROUPS_Z = C;
}
}
@@ -866,49 +871,49 @@ namespace GPUVerify
return _Z != null;
}
- public bool KernelHasTileIdX()
+ public bool KernelHasGroupIdX()
{
- return _TILE_X != null;
+ return _GROUP_X != null;
}
- public bool KernelHasTileIdY()
+ public bool KernelHasGroupIdY()
{
- return _TILE_Y != null;
+ return _GROUP_Y != null;
}
- public bool KernelHasTileIdZ()
+ public bool KernelHasGroupIdZ()
{
- return _TILE_Z != null;
+ return _GROUP_Z != null;
}
- public bool KernelHasNumTilesX()
+ public bool KernelHasNumGroupsX()
{
- return _NUM_TILES_X != null;
+ return _NUM_GROUPS_X != null;
}
- public bool KernelHasNumTilesY()
+ public bool KernelHasNumGroupsY()
{
- return _NUM_TILES_Y != null;
+ return _NUM_GROUPS_Y != null;
}
- public bool KernelHasNumTilesZ()
+ public bool KernelHasNumGroupsZ()
{
- return _NUM_TILES_Z != null;
+ return _NUM_GROUPS_Z != null;
}
- public bool KernelHasTileSizeX()
+ public bool KernelHasGroupSizeX()
{
- return _TILE_SIZE_X != null;
+ return _GROUP_SIZE_X != null;
}
- public bool KernelHasTileSizeY()
+ public bool KernelHasGroupSizeY()
{
- return _TILE_SIZE_Y != null;
+ return _GROUP_SIZE_Y != null;
}
- public bool KernelHasTileSizeZ()
+ public bool KernelHasGroupSizeZ()
{
- return _TILE_SIZE_Z != null;
+ return _GROUP_SIZE_Z != null;
}
public bool KernelHasId(string dimension)
@@ -1129,17 +1134,17 @@ namespace GPUVerify
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)))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetGroupSize(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GT", new IdentifierExpr(tok, GetNumGroups(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, GetGroupId(dimension)), ZeroBV(tok))));
+ Proc.Requires.Add(new Requires(false, MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, GetGroupId(dimension)), new IdentifierExpr(tok, GetNumGroups(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)))));
+ Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetGroupSize(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Gt(new IdentifierExpr(tok, GetNumGroups(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Ge(new IdentifierExpr(tok, GetGroupId(dimension)), Zero(tok))));
+ Proc.Requires.Add(new Requires(false, Expr.Lt(new IdentifierExpr(tok, GetGroupId(dimension)), new IdentifierExpr(tok, GetNumGroups(dimension)))));
}
}
@@ -1159,8 +1164,8 @@ namespace GPUVerify
MakeBitVectorBinaryBoolean("BV32_GEQ", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), ZeroBV(tok))
),
Expr.And(
- MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetTileSize(dimension))),
- MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetTileSize(dimension)))
+ MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetGroupSize(dimension))),
+ MakeBitVectorBinaryBoolean("BV32_LT", new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetGroupSize(dimension)))
))
:
Expr.And(
@@ -1169,8 +1174,8 @@ namespace GPUVerify
Expr.Ge(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), Zero(tok))
),
Expr.And(
- Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetTileSize(dimension))),
- Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetTileSize(dimension)))
+ Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 1)), new IdentifierExpr(tok, GetGroupSize(dimension))),
+ Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension, 2)), new IdentifierExpr(tok, GetGroupSize(dimension)))
));
AssumeThreadIdsInRange = (null == AssumeThreadIdsInRange) ? AssumeThreadIdsInRangeInDimension : Expr.And(AssumeThreadIdsInRange, AssumeThreadIdsInRangeInDimension);
@@ -1185,22 +1190,22 @@ namespace GPUVerify
}), new LocalVariable(lhs.tok, new TypedIdent(lhs.tok, "result", Microsoft.Boogie.Type.Bool)))), new ExprSeq(new Expr[] { lhs, rhs }));
}
- private Constant GetTileSize(string dimension)
+ private Constant GetGroupSize(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
- if (dimension.Equals("X")) return _TILE_SIZE_X;
- if (dimension.Equals("Y")) return _TILE_SIZE_Y;
- if (dimension.Equals("Z")) return _TILE_SIZE_Z;
+ if (dimension.Equals("X")) return _GROUP_SIZE_X;
+ if (dimension.Equals("Y")) return _GROUP_SIZE_Y;
+ if (dimension.Equals("Z")) return _GROUP_SIZE_Z;
Debug.Assert(false);
return null;
}
- private Constant GetNumTiles(string dimension)
+ private Constant GetNumGroups(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
- if (dimension.Equals("X")) return _NUM_TILES_X;
- if (dimension.Equals("Y")) return _NUM_TILES_Y;
- if (dimension.Equals("Z")) return _NUM_TILES_Z;
+ if (dimension.Equals("X")) return _NUM_GROUPS_X;
+ if (dimension.Equals("Y")) return _NUM_GROUPS_Y;
+ if (dimension.Equals("Z")) return _NUM_GROUPS_Z;
Debug.Assert(false);
return null;
}
@@ -1217,12 +1222,12 @@ namespace GPUVerify
return new Constant(tok, new TypedIdent(tok, "_" + dimension + "$" + number, GetTypeOfId(dimension)));
}
- private Constant GetTileId(string dimension)
+ private Constant GetGroupId(string dimension)
{
Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z"));
- if (dimension.Equals("X")) return _TILE_X;
- if (dimension.Equals("Y")) return _TILE_Y;
- if (dimension.Equals("Z")) return _TILE_Z;
+ if (dimension.Equals("X")) return _GROUP_X;
+ if (dimension.Equals("Y")) return _GROUP_Y;
+ if (dimension.Equals("Z")) return _GROUP_Z;
Debug.Assert(false);
return null;
}
@@ -1436,7 +1441,7 @@ namespace GPUVerify
foreach (Variable v in impl.LocVars)
{
- Debug.Assert(!NonLocalState.getTileStaticVariables().Contains(v));
+ Debug.Assert(!NonLocalState.getGroupSharedVariables().Contains(v));
NewLocVars.Add(v);
}
@@ -2184,22 +2189,22 @@ namespace GPUVerify
Error(KernelProcedure.tok, "Kernel must declare global constant '" + _X_name + "'");
}
- if (!KernelHasTileSizeX())
+ if (!KernelHasGroupSizeX())
{
- Error(KernelProcedure.tok, "Kernel must declare global constant '" + _TILE_SIZE_X_name + "'");
+ Error(KernelProcedure.tok, "Kernel must declare global constant '" + _GROUP_SIZE_X_name + "'");
}
- if (!KernelHasNumTilesX())
+ if (!KernelHasNumGroupsX())
{
- Error(KernelProcedure.tok, "Kernel must declare global constant '" + _NUM_TILES_X_name + "'");
+ Error(KernelProcedure.tok, "Kernel must declare global constant '" + _NUM_GROUPS_X_name + "'");
}
- if (!KernelHasTileIdX())
+ if (!KernelHasGroupIdX())
{
- Error(KernelProcedure.tok, "Kernel must declare global constant '" + _TILE_X_name + "'");
+ Error(KernelProcedure.tok, "Kernel must declare global constant '" + _GROUP_X_name + "'");
}
- if (KernelHasIdY() || KernelHasTileSizeY() || KernelHasNumTilesY() || KernelHasTileIdY())
+ if (KernelHasIdY() || KernelHasGroupSizeY() || KernelHasNumGroupsY() || KernelHasGroupIdY())
{
if (!KernelHasIdY())
@@ -2207,24 +2212,24 @@ namespace GPUVerify
Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _Y_name + "'");
}
- if (!KernelHasTileSizeY())
+ if (!KernelHasGroupSizeY())
{
- Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _TILE_SIZE_Y_name + "'");
+ Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _GROUP_SIZE_Y_name + "'");
}
- if (!KernelHasNumTilesY())
+ if (!KernelHasNumGroupsY())
{
- Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _NUM_TILES_Y_name + "'");
+ Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _NUM_GROUPS_Y_name + "'");
}
- if (!KernelHasTileIdY())
+ if (!KernelHasGroupIdY())
{
- Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _TILE_Y_name + "'");
+ Error(KernelProcedure.tok, "2D kernel must declare global constant '" + _GROUP_Y_name + "'");
}
}
- if (KernelHasIdZ() || KernelHasTileSizeZ() || KernelHasNumTilesZ() || KernelHasTileIdZ())
+ if (KernelHasIdZ() || KernelHasGroupSizeZ() || KernelHasNumGroupsZ() || KernelHasGroupIdZ())
{
if (!KernelHasIdY())
@@ -2232,19 +2237,19 @@ namespace GPUVerify
Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _Y_name + "'");
}
- if (!KernelHasTileSizeY())
+ if (!KernelHasGroupSizeY())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_SIZE_Y_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_SIZE_Y_name + "'");
}
- if (!KernelHasNumTilesY())
+ if (!KernelHasNumGroupsY())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_TILES_Y_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_GROUPS_Y_name + "'");
}
- if (!KernelHasTileIdY())
+ if (!KernelHasGroupIdY())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_Y_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_Y_name + "'");
}
if (!KernelHasIdZ())
@@ -2252,19 +2257,19 @@ namespace GPUVerify
Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _Z_name + "'");
}
- if (!KernelHasTileSizeZ())
+ if (!KernelHasGroupSizeZ())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_SIZE_Z_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_SIZE_Z_name + "'");
}
- if (!KernelHasNumTilesZ())
+ if (!KernelHasNumGroupsZ())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_TILES_Z_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _NUM_GROUPS_Z_name + "'");
}
- if (!KernelHasTileIdZ())
+ if (!KernelHasGroupIdZ())
{
- Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _TILE_Z_name + "'");
+ Error(KernelProcedure.tok, "3D kernel must declare global constant '" + _GROUP_Z_name + "'");
}
}
@@ -2272,41 +2277,6 @@ namespace GPUVerify
return ErrorCount;
}
- private bool HasNamedConstant(string dimension, string Name)
- {
- foreach (Declaration d in Program.TopLevelDeclarations)
- {
- if (d is Variable && (d as Variable).Name.Equals(Name + dimension))
- {
- Variable v = d as Variable;
- if (v is Constant && IsIntOrBv32(v.TypedIdent.Type))
- {
- return true;
- }
- else
- {
- Error(v.tok, "Declaration '" + Name + dimension + "' must be a constant integer");
- }
- }
- }
- return false;
- }
-
- private bool HasTileId(string dimension)
- {
- return HasNamedConstant(dimension, "_tile_");
- }
-
- private bool HasNumTiles(string dimension)
- {
- return HasNamedConstant(dimension, "NUM_TILES_");
- }
-
- private bool HasTileSize(string dimension)
- {
- return HasNamedConstant(dimension, "TILE_SIZE_");
- }
-
public static bool IsThreadLocalIdConstant(Variable variable)
{
return variable is Constant && (variable.Name.Equals(_X_name) || variable.Name.Equals(_Y_name) || variable.Name.Equals(_Z_name));
diff --git a/Source/GPUVerify/INonLocalState.cs b/Source/GPUVerify/INonLocalState.cs
index 0e03d685..c6211dab 100644
--- a/Source/GPUVerify/INonLocalState.cs
+++ b/Source/GPUVerify/INonLocalState.cs
@@ -11,7 +11,7 @@ namespace GPUVerify
ICollection<Variable> getGlobalVariables();
- ICollection<Variable> getTileStaticVariables();
+ ICollection<Variable> getGroupSharedVariables();
ICollection<Variable> getAllNonLocalVariables();
diff --git a/Source/GPUVerify/Main.cs b/Source/GPUVerify/Main.cs
index e38aabea..1be30dc9 100644
--- a/Source/GPUVerify/Main.cs
+++ b/Source/GPUVerify/Main.cs
@@ -97,11 +97,11 @@ namespace GPUVerify
Variable newG = findClonedVar(v, newGp.NonLocalState.getGlobalVariables());
- Variable newT = findClonedVar(v, newGp.NonLocalState.getTileStaticVariables());
+ Variable newT = findClonedVar(v, newGp.NonLocalState.getGroupSharedVariables());
Contract.Assert(newG == null || newT == null);
ri.NonLocalStateToCheck.getGlobalVariables().Clear();
- ri.NonLocalStateToCheck.getTileStaticVariables().Clear();
+ ri.NonLocalStateToCheck.getGroupSharedVariables().Clear();
ri.onlyLog1 = a1;
ri.onlyLog2 = a2;
@@ -112,7 +112,7 @@ namespace GPUVerify
if (newT != null)
{
- ri.NonLocalStateToCheck.getTileStaticVariables().Add(newT);
+ ri.NonLocalStateToCheck.getGroupSharedVariables().Add(newT);
}
newGp.doit();
diff --git a/Source/GPUVerify/NonLocalStateLists.cs b/Source/GPUVerify/NonLocalStateLists.cs
index a4b5e154..c47cddd5 100644
--- a/Source/GPUVerify/NonLocalStateLists.cs
+++ b/Source/GPUVerify/NonLocalStateLists.cs
@@ -10,12 +10,12 @@ namespace GPUVerify
class NonLocalStateLists : INonLocalState
{
private List<Variable> GlobalVariables;
- private List<Variable> TileStaticVariables;
+ private List<Variable> GroupSharedVariables;
public NonLocalStateLists()
{
GlobalVariables = new List<Variable>();
- TileStaticVariables = new List<Variable>();
+ GroupSharedVariables = new List<Variable>();
}
public ICollection<Variable> getGlobalVariables()
@@ -23,16 +23,16 @@ namespace GPUVerify
return GlobalVariables;
}
- public ICollection<Variable> getTileStaticVariables()
+ public ICollection<Variable> getGroupSharedVariables()
{
- return TileStaticVariables;
+ return GroupSharedVariables;
}
public ICollection<Variable> getAllNonLocalVariables()
{
List<Variable> all = new List<Variable>();
all.AddRange(GlobalVariables);
- all.AddRange(TileStaticVariables);
+ all.AddRange(GroupSharedVariables);
return all;
}
diff --git a/Source/GPUVerify/RaceInstrumenterBase.cs b/Source/GPUVerify/RaceInstrumenterBase.cs
index 4f2f76be..692f1288 100644
--- a/Source/GPUVerify/RaceInstrumenterBase.cs
+++ b/Source/GPUVerify/RaceInstrumenterBase.cs
@@ -38,9 +38,9 @@ namespace GPUVerify
{
NonLocalStateToCheck.getGlobalVariables().Add(v);
}
- foreach(Variable v in verifier.NonLocalState.getTileStaticVariables())
+ foreach(Variable v in verifier.NonLocalState.getGroupSharedVariables())
{
- NonLocalStateToCheck.getTileStaticVariables().Add(v);
+ NonLocalStateToCheck.getGroupSharedVariables().Add(v);
}
}