diff options
| -rw-r--r-- | Source/GPUVerify/BarrierInvariantDescriptor.cs | 10 | ||||
| -rw-r--r-- | Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs | 10 | ||||
| -rw-r--r-- | Source/GPUVerify/KernelDualiser.cs | 24 | ||||
| -rw-r--r-- | Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs | 16 |
4 files changed, 39 insertions, 21 deletions
diff --git a/Source/GPUVerify/BarrierInvariantDescriptor.cs b/Source/GPUVerify/BarrierInvariantDescriptor.cs index a8320b18..2b7450c9 100644 --- a/Source/GPUVerify/BarrierInvariantDescriptor.cs +++ b/Source/GPUVerify/BarrierInvariantDescriptor.cs @@ -10,15 +10,21 @@ namespace GPUVerify { protected Expr Predicate;
protected Expr BarrierInvariant;
+ protected QKeyValue SourceLocationInfo;
protected KernelDualiser Dualiser;
+ protected string ProcName;
- public BarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant, KernelDualiser Dualiser) {
+ public BarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant,
+ QKeyValue SourceLocationInfo,
+ KernelDualiser Dualiser, string ProcName) {
this.Predicate = Predicate;
this.BarrierInvariant = BarrierInvariant;
+ this.SourceLocationInfo = SourceLocationInfo;
this.Dualiser = Dualiser;
+ this.ProcName = ProcName;
}
- internal abstract AssertCmd GetAssertCmd(QKeyValue Attributes);
+ internal abstract AssertCmd GetAssertCmd();
internal abstract List<AssumeCmd> GetInstantiationCmds();
diff --git a/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs b/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs index df84cae8..8d8f75ec 100644 --- a/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs +++ b/Source/GPUVerify/BinaryBarrierInvariantDescriptor.cs @@ -9,8 +9,10 @@ namespace GPUVerify { private List<Tuple<Expr, Expr>> InstantiationExprPairs;
- public BinaryBarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant, KernelDualiser Dualiser) :
- base(Predicate, BarrierInvariant, Dualiser) {
+ public BinaryBarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant,
+ QKeyValue SourceLocationInfo,
+ KernelDualiser Dualiser, string ProcName) :
+ base(Predicate, BarrierInvariant, SourceLocationInfo, Dualiser, ProcName) {
InstantiationExprPairs = new List<Tuple<Expr, Expr>>();
}
@@ -18,13 +20,13 @@ namespace GPUVerify { InstantiationExprPairs.Add(new Tuple<Expr, Expr>(first, second));
}
- internal override AssertCmd GetAssertCmd(QKeyValue Attributes) {
+ internal override AssertCmd GetAssertCmd() {
var vd = new VariableDualiser(1, null, null);
return new AssertCmd(
Token.NoToken,
Expr.Imp(GPUVerifier.ThreadsInSameGroup(),
vd.VisitExpr(Expr.Imp(Predicate, BarrierInvariant))),
- Dualiser.MakeThreadSpecificAttributes(Attributes, 1));
+ Dualiser.MakeThreadSpecificAttributes(SourceLocationInfo, 1));
}
internal override List<AssumeCmd> GetInstantiationCmds() {
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index 526e39a0..d2b921f2 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -108,7 +108,9 @@ namespace GPUVerify { Debug.Assert(Call.Ins.Count >= 3);
var BIDescriptor = new UnaryBarrierInvariantDescriptor(Call.Ins[0], Expr.Neq(Call.Ins[1], - new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 1)), this);
+ new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 1)),
+ Call.Attributes,
+ this, procName);
for (var i = 2; i < Call.Ins.Count; i++) {
BIDescriptor.AddInstantiationExpr(Call.Ins[i]);
}
@@ -122,7 +124,9 @@ namespace GPUVerify { Debug.Assert(Call.Ins.Count >= 4);
var BIDescriptor = new BinaryBarrierInvariantDescriptor(Call.Ins[0],
Expr.Neq(Call.Ins[1],
- new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 1)), this);
+ new LiteralExpr(Token.NoToken, BigNum.FromInt(0), 1)),
+ Call.Attributes,
+ this, procName);
for (var i = 2; i < Call.Ins.Count; i += 2) {
BIDescriptor.AddInstantiationExprPair(Call.Ins[i], Call.Ins[i + 1]);
}
@@ -134,7 +138,7 @@ namespace GPUVerify { if (Call.callee.Equals(verifier.BarrierProcedure.Name)) {
// Assert barrier invariants
foreach (var BIDescriptor in BarrierInvariantDescriptors) {
- cs.Add(BIDescriptor.GetAssertCmd(Call.Attributes));
+ cs.Add(BIDescriptor.GetAssertCmd());
}
}
@@ -420,14 +424,17 @@ namespace GPUVerify { class ThreadInstantiator : Duplicator {
- private GPUVerifier verifier;
private Expr InstantiationExpr;
private int Thread;
+ private UniformityAnalyser Uni;
+ private string ProcName;
- internal ThreadInstantiator(GPUVerifier verifier, Expr InstantiationExpr, int Thread) {
- this.verifier = verifier;
+ internal ThreadInstantiator(Expr InstantiationExpr, int Thread,
+ UniformityAnalyser Uni, string ProcName) {
this.InstantiationExpr = InstantiationExpr;
this.Thread = Thread;
+ this.Uni = Uni;
+ this.ProcName = ProcName;
}
public override Expr VisitIdentifierExpr(IdentifierExpr node) {
@@ -439,8 +446,9 @@ namespace GPUVerify { }
Debug.Assert(node.Decl is Constant ||
- verifier.KernelArrayInfo.getGroupSharedArrays().Contains(node.Decl) ||
- verifier.KernelArrayInfo.getGlobalArrays().Contains(node.Decl));
+ 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);
}
diff --git a/Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs b/Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs index ef87750e..48e3a2ec 100644 --- a/Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs +++ b/Source/GPUVerify/UnaryBarrierInvariantDescriptor.cs @@ -8,8 +8,9 @@ namespace GPUVerify { class UnaryBarrierInvariantDescriptor : BarrierInvariantDescriptor {
private List<Expr> InstantiationExprs;
- public UnaryBarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant, KernelDualiser Dualiser) :
- base(Predicate, BarrierInvariant, Dualiser) {
+ public UnaryBarrierInvariantDescriptor(Expr Predicate, Expr BarrierInvariant,
+ QKeyValue SourceLocationInfo, KernelDualiser Dualiser, string ProcName) :
+ base(Predicate, BarrierInvariant, SourceLocationInfo, Dualiser, ProcName) {
InstantiationExprs = new List<Expr>();
}
@@ -17,21 +18,22 @@ namespace GPUVerify { InstantiationExprs.Add(InstantiationExpr);
}
- internal override AssertCmd GetAssertCmd(QKeyValue Attributes) {
- var vd = new VariableDualiser(1, null, null);
+ internal override AssertCmd GetAssertCmd() {
+ var vd = new VariableDualiser(1, Dualiser.verifier.uniformityAnalyser, ProcName);
return new AssertCmd(
Token.NoToken,
vd.VisitExpr(Expr.Imp(Predicate, BarrierInvariant)),
- Dualiser.MakeThreadSpecificAttributes(Attributes, 1));
+ Dualiser.MakeThreadSpecificAttributes(SourceLocationInfo, 1));
}
internal override List<AssumeCmd> GetInstantiationCmds() {
var result = new List<AssumeCmd>();
foreach (var Instantiation in InstantiationExprs) {
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);
- var ti = new ThreadInstantiator(Dualiser.verifier, ThreadInstantiationExpr, Thread);
+ var ti = new ThreadInstantiator(ThreadInstantiationExpr, Thread,
+ Dualiser.verifier.uniformityAnalyser, ProcName);
result.Add(new AssumeCmd(
Token.NoToken,
|