diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs | 4 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 33 | ||||
| -rw-r--r-- | Source/GPUVerify/KernelDualiser.cs | 22 | ||||
| -rw-r--r-- | Source/GPUVerify/RaceInstrumenter.cs | 7 | ||||
| -rw-r--r-- | Source/VCGeneration/UniformityAnalyser.cs | 10 |
5 files changed, 50 insertions, 26 deletions
diff --git a/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs b/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs index 8d8f75ec..8be05ecb 100644 --- a/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs +++ b/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs @@ -21,7 +21,7 @@ namespace GPUVerify { }
internal override AssertCmd GetAssertCmd() {
- var vd = new VariableDualiser(1, null, null);
+ var vd = new VariableDualiser(1, Dualiser.verifier.uniformityAnalyser, ProcName);
return new AssertCmd(
Token.NoToken,
Expr.Imp(GPUVerifier.ThreadsInSameGroup(),
@@ -34,7 +34,7 @@ namespace GPUVerify { foreach (var Instantiation in InstantiationExprPairs) {
foreach (var Thread in new int[] { 1, 2 }) {
- var vd = new VariableDualiser(Thread, null, null);
+ var vd = new VariableDualiser(Thread, Dualiser.verifier.uniformityAnalyser, ProcName);
var ThreadInstantiationExpr = vd.VisitExpr(Instantiation.Item1);
var OtherThreadInstantiationExpr = vd.VisitExpr(Instantiation.Item2);
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index f94cf5ef..216954c5 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -1023,17 +1023,17 @@ namespace GPUVerify Expr.Or( Expr.Or( Expr.Neq( - new IdentifierExpr(tok, MakeThreadId(tok, "X", 1)), - new IdentifierExpr(tok, MakeThreadId(tok, "X", 2)) + new IdentifierExpr(tok, MakeThreadId("X", 1)), + new IdentifierExpr(tok, MakeThreadId("X", 2)) ), Expr.Neq( - new IdentifierExpr(tok, MakeThreadId(tok, "Y", 1)), - new IdentifierExpr(tok, MakeThreadId(tok, "Y", 2)) + new IdentifierExpr(tok, MakeThreadId("Y", 1)), + new IdentifierExpr(tok, MakeThreadId("Y", 2)) ) ), Expr.Neq( - new IdentifierExpr(tok, MakeThreadId(tok, "Z", 1)), - new IdentifierExpr(tok, MakeThreadId(tok, "Z", 2)) + new IdentifierExpr(tok, MakeThreadId("Z", 1)), + new IdentifierExpr(tok, MakeThreadId("Z", 2)) ) ); @@ -1196,14 +1196,14 @@ namespace GPUVerify Expr ThreadIdNonNegative = GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)) ? - MakeBVSge(new IdentifierExpr(tok, MakeThreadId(tok, dimension)), ZeroBV()) + MakeBVSge(new IdentifierExpr(tok, MakeThreadId(dimension)), ZeroBV()) : - Expr.Ge(new IdentifierExpr(tok, MakeThreadId(tok, dimension)), Zero()); + Expr.Ge(new IdentifierExpr(tok, MakeThreadId(dimension)), Zero()); Expr ThreadIdLessThanGroupSize = GetTypeOfId(dimension).Equals(Microsoft.Boogie.Type.GetBvType(32)) ? - MakeBVSlt(new IdentifierExpr(tok, MakeThreadId(tok, dimension)), new IdentifierExpr(tok, GetGroupSize(dimension))) + MakeBVSlt(new IdentifierExpr(tok, MakeThreadId(dimension)), new IdentifierExpr(tok, GetGroupSize(dimension))) : - Expr.Lt(new IdentifierExpr(tok, MakeThreadId(tok, dimension)), new IdentifierExpr(tok, GetGroupSize(dimension))); + Expr.Lt(new IdentifierExpr(tok, MakeThreadId(dimension)), new IdentifierExpr(tok, GetGroupSize(dimension))); Proc.Requires.Add(new Requires(false, new VariableDualiser(1, null, null).VisitExpr(ThreadIdNonNegative))); Proc.Requires.Add(new Requires(false, new VariableDualiser(2, null, null).VisitExpr(ThreadIdNonNegative))); @@ -1329,7 +1329,7 @@ namespace GPUVerify return null; } - internal Constant MakeThreadId(IToken tok, string dimension) + internal static Constant MakeThreadId(string dimension) { Contract.Requires(dimension.Equals("X") || dimension.Equals("Y") || dimension.Equals("Z")); string name = null; @@ -1337,13 +1337,14 @@ namespace GPUVerify if (dimension.Equals("Y")) name = _Y.Name; if (dimension.Equals("Z")) name = _Z.Name; Debug.Assert(name != null); - return new Constant(tok, new TypedIdent(tok, name, GetTypeOfId(dimension))); + return new Constant(Token.NoToken, new TypedIdent(Token.NoToken, name, GetTypeOfId(dimension))); } - internal Constant MakeThreadId(IToken tok, string dimension, int number) + internal static Constant MakeThreadId(string dimension, int number) { - Constant resultWithoutThreadId = MakeThreadId(tok, dimension); - return new Constant(tok, new TypedIdent(tok, resultWithoutThreadId.Name + "$" + number, GetTypeOfId(dimension))); + Constant resultWithoutThreadId = MakeThreadId(dimension); + return new Constant(Token.NoToken, new TypedIdent( + Token.NoToken, resultWithoutThreadId.Name + "$" + number, GetTypeOfId(dimension))); } internal static Constant GetGroupId(string dimension) @@ -2142,7 +2143,7 @@ namespace GPUVerify { return MakeBVAdd(MakeBVMul( new IdentifierExpr(Token.NoToken, GetGroupId(dimension)), new IdentifierExpr(Token.NoToken, GetGroupSize(dimension))), - new IdentifierExpr(Token.NoToken, MakeThreadId(Token.NoToken, dimension))); + new IdentifierExpr(Token.NoToken, MakeThreadId(dimension))); } internal IRegion RootRegion(Implementation Impl) diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index d2b921f2..3a2a1776 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -445,12 +445,24 @@ namespace GPUVerify { return InstantiationExpr.Clone() as Expr;
}
- Debug.Assert(node.Decl is Constant ||
- QKeyValue.FindBoolAttribute(node.Decl.Attributes, "global") ||
- QKeyValue.FindBoolAttribute(node.Decl.Attributes, "group_shared") ||
- (Uni != null && Uni.IsUniform(ProcName, node.Decl.Name)));
+ if(node.Decl is Constant ||
+ QKeyValue.FindBoolAttribute(node.Decl.Attributes, "global") ||
+ QKeyValue.FindBoolAttribute(node.Decl.Attributes, "group_shared") ||
+ (Uni != null && Uni.IsUniform(ProcName, node.Decl.Name))) {
+ return base.VisitIdentifierExpr(node);
+ }
- return base.VisitIdentifierExpr(node);
+ if (InstantiationExprIsThreadId()) {
+ return new VariableDualiser(Thread, Uni, ProcName).VisitIdentifierExpr(node);
+ }
+
+ Debug.Assert(false);
+ return null;
+ }
+
+ private bool InstantiationExprIsThreadId() {
+ return (InstantiationExpr is IdentifierExpr) &&
+ ((IdentifierExpr)InstantiationExpr).Decl.Name.Equals(GPUVerifier.MakeThreadId("X", Thread).Name);
}
public override Expr VisitNAryExpr(NAryExpr node) {
diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs index 71214cb3..f3b9194b 100644 --- a/Source/GPUVerify/RaceInstrumenter.cs +++ b/Source/GPUVerify/RaceInstrumenter.cs @@ -1028,7 +1028,8 @@ namespace GPUVerify { private Expr AccessedOffsetIsThreadLocalIdExpr(Variable v, string ReadOrWrite, int Thread) { return 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.MakeOffsetVariable(v.Name, 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.Name, ReadOrWrite))), + new IdentifierExpr(v.tok, GPUVerifier.MakeThreadId("X", Thread)))); } private Expr GlobalIdExpr(string dimension, int Thread) { @@ -1043,10 +1044,10 @@ namespace GPUVerify { private Expr MakeCTimesLocalIdRangeExpression(Variable v, Expr constant, string ReadOrWrite, int Thread) { Expr CTimesLocalId = verifier.MakeBVMul(constant.Clone() as Expr, - new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))); + new IdentifierExpr(Token.NoToken, GPUVerifier.MakeThreadId("X", Thread))); Expr CTimesLocalIdPlusC = verifier.MakeBVAdd(verifier.MakeBVMul(constant.Clone() as Expr, - new IdentifierExpr(Token.NoToken, verifier.MakeThreadId(Token.NoToken, "X", Thread))), constant.Clone() as Expr); + new IdentifierExpr(Token.NoToken, GPUVerifier.MakeThreadId("X", Thread))), constant.Clone() as Expr); Expr CTimesLocalIdLeqAccessedOffset = GPUVerifier.MakeBitVectorBinaryBoolean("BV32_LEQ", CTimesLocalId, OffsetXExpr(v, ReadOrWrite, Thread)); diff --git a/Source/VCGeneration/UniformityAnalyser.cs b/Source/VCGeneration/UniformityAnalyser.cs index 849333b3..802ee2d2 100644 --- a/Source/VCGeneration/UniformityAnalyser.cs +++ b/Source/VCGeneration/UniformityAnalyser.cs @@ -309,6 +309,16 @@ namespace Microsoft.Boogie } } } + else if (c is HavocCmd) + { + HavocCmd havocCmd = c as HavocCmd; + foreach(IdentifierExpr ie in havocCmd.Vars) + { + if(IsUniform(impl.Name, ie.Decl.Name)) { + SetNonUniform(impl.Name, ie.Decl.Name); + } + } + } else if (c is CallCmd) { CallCmd callCmd = c as CallCmd; |