diff options
| author |  Unknown <afd@afd-THINK.home> | 2012-02-28 12:38:38 +0000 |
|---|---|---|
| committer | Unknown <afd@afd-THINK.home> | 2012-02-28 12:38:38 +0000 |
| commit | 91acbf1e099bd3508f99ff5ec1b3bf4f6cd3050f (patch) | |
| tree | 1d91bfb02a521581c8246a51122f79a99aa2a97a /Source/GPUVerify/GPUVerifier.cs | |
| parent | 66829a6c30b0c97d868ce3ce19820c04b1a79c64 (diff) | |
Added support for invariants in GPUVerify input.
Diffstat (limited to 'Source/GPUVerify/GPUVerifier.cs')
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 121 |
1 files changed, 63 insertions, 58 deletions
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 2f9be79b..52d55585 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -2138,7 +2138,11 @@ namespace GPUVerify if (bb.ec is WhileCmd)
{
- result.ec = new WhileCmd(bb.ec.tok, Expr.Or(new VariableDualiser(1).VisitExpr((bb.ec as WhileCmd).Guard), new VariableDualiser(2).VisitExpr((bb.ec as WhileCmd).Guard)), (bb.ec as WhileCmd).Invariants, MakeDual((bb.ec as WhileCmd).Body, HalfDualise));
+ result.ec = new WhileCmd(bb.ec.tok,
+ Expr.Or(new VariableDualiser(1).VisitExpr((bb.ec as WhileCmd).Guard),
+ new VariableDualiser(2).VisitExpr((bb.ec as WhileCmd).Guard)
+ ),
+ MakeDualInvariants((bb.ec as WhileCmd).Invariants), MakeDual((bb.ec as WhileCmd).Body, HalfDualise));
}
else
{
@@ -2149,6 +2153,18 @@ namespace GPUVerify }
+ private List<PredicateCmd> MakeDualInvariants(List<PredicateCmd> originalInvariants)
+ {
+ List<PredicateCmd> result = new List<PredicateCmd>();
+ foreach(PredicateCmd p in originalInvariants)
+ {
+ result.Add(new AssertCmd(p.tok, new VariableDualiser(1).VisitExpr(p.Expr.Clone() as Expr)));
+ result.Add(new AssertCmd(p.tok, new VariableDualiser(2).VisitExpr(p.Expr.Clone() as Expr)));
+ }
+
+ return result;
+ }
+
private void MakeDualLocalVariables(Implementation impl, bool HalfDualise)
{
VariableSeq NewLocalVars = new VariableSeq();
@@ -2222,83 +2238,72 @@ namespace GPUVerify MissingKernelAttributeError("Kernel", GROUP_ID_X_STRING);
}
- if (KernelHasIdY() || KernelHasGroupSizeY() || KernelHasNumGroupsY() || KernelHasGroupIdY())
+ if (!KernelHasIdY())
{
-
- if (!KernelHasIdY())
- {
- MissingKernelAttributeError("2D kernel", LOCAL_ID_Y_STRING);
- }
-
- if (!KernelHasGroupSizeY())
- {
- MissingKernelAttributeError("2D kernel", GROUP_SIZE_Y_STRING);
- }
-
- if (!KernelHasNumGroupsY())
- {
- MissingKernelAttributeError("2D kernel", NUM_GROUPS_Y_STRING);
- }
-
- if (!KernelHasGroupIdY())
- {
- MissingKernelAttributeError("2D kernel", GROUP_ID_Y_STRING);
- }
-
+ MissingKernelAttributeError("Kernel", LOCAL_ID_Y_STRING);
}
- if (KernelHasIdZ() || KernelHasGroupSizeZ() || KernelHasNumGroupsZ() || KernelHasGroupIdZ())
+ if (!KernelHasGroupSizeY())
{
+ MissingKernelAttributeError("2D kernel", GROUP_SIZE_Y_STRING);
+ }
- if (!KernelHasIdY())
- {
- MissingKernelAttributeError("3D kernel", LOCAL_ID_Y_STRING);
- }
+ if (!KernelHasNumGroupsY())
+ {
+ MissingKernelAttributeError("2D kernel", NUM_GROUPS_Y_STRING);
+ }
- if (!KernelHasGroupSizeY())
- {
- MissingKernelAttributeError("3D kernel", GROUP_SIZE_Y_STRING);
- }
+ if (!KernelHasGroupIdY())
+ {
+ MissingKernelAttributeError(GROUP_ID_Y_STRING);
+ }
- if (!KernelHasNumGroupsY())
- {
- MissingKernelAttributeError("3D kernel", NUM_GROUPS_Y_STRING);
- }
+ if (!KernelHasIdY())
+ {
+ MissingKernelAttributeError("3D kernel", LOCAL_ID_Y_STRING);
+ }
- if (!KernelHasGroupIdY())
- {
- MissingKernelAttributeError("3D kernel", GROUP_ID_Y_STRING);
- }
+ if (!KernelHasGroupSizeY())
+ {
+ MissingKernelAttributeError(GROUP_SIZE_Y_STRING);
+ }
- if (!KernelHasIdZ())
- {
- MissingKernelAttributeError("3D kernel", LOCAL_ID_Z_STRING);
- }
+ if (!KernelHasNumGroupsY())
+ {
+ MissingKernelAttributeError(NUM_GROUPS_Y_STRING);
+ }
- if (!KernelHasGroupSizeZ())
- {
- MissingKernelAttributeError("3D kernel", GROUP_SIZE_Z_STRING);
- }
+ if (!KernelHasGroupIdY())
+ {
+ MissingKernelAttributeError(GROUP_ID_Y_STRING);
+ }
- if (!KernelHasNumGroupsZ())
- {
- MissingKernelAttributeError("3D kernel", NUM_GROUPS_Z_STRING);
- }
+ if (!KernelHasIdZ())
+ {
+ MissingKernelAttributeError(LOCAL_ID_Z_STRING);
+ }
- if (!KernelHasGroupIdZ())
- {
- MissingKernelAttributeError("3D kernel", GROUP_ID_Z_STRING);
- }
+ if (!KernelHasGroupSizeZ())
+ {
+ MissingKernelAttributeError(GROUP_SIZE_Z_STRING);
+ }
+ if (!KernelHasNumGroupsZ())
+ {
+ MissingKernelAttributeError(NUM_GROUPS_Z_STRING);
+ }
+ if (!KernelHasGroupIdZ())
+ {
+ MissingKernelAttributeError(GROUP_ID_Z_STRING);
}
return ErrorCount;
}
- private void MissingKernelAttributeError(string kindOfKernel, string attribute)
+ private void MissingKernelAttributeError(string attribute)
{
- Error(KernelProcedure.tok, kindOfKernel + " must declare global constant marked with attribute ':" + attribute + "'");
+ Error(KernelProcedure.tok, "Kernel must declare global constant marked with attribute ':" + attribute + "'");
}
public static bool IsThreadLocalIdConstant(Variable variable)
|