diff options
| author |  Peter Collingbourne <peter@pcc.me.uk> | 2012-06-15 15:10:41 +0100 |
|---|---|---|
| committer | Peter Collingbourne <peter@pcc.me.uk> | 2012-06-15 15:10:41 +0100 |
| commit | 9b244daef1ff937c4a01974828f1b2216642365a (patch) | |
| tree | c955267195362d6ed1ec10acddcc560d629ea324 /Source/GPUVerify/KernelDualiser.cs | |
| parent | 5994e5ca75b1ba5c93ccfccb20477e1e729616a1 (diff) | |
GPUVerify: when dualising assume and assert statements, emit two statements instead of a conjunction
Diffstat (limited to 'Source/GPUVerify/KernelDualiser.cs')
| -rw-r--r-- | Source/GPUVerify/KernelDualiser.cs | 23 |
1 files changed, 9 insertions, 14 deletions
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index 614659b6..967b69ef 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -186,32 +186,27 @@ namespace GPUVerify else if (c is AssertCmd)
{
AssertCmd ass = c as AssertCmd;
- if (ContainsAsymmetricExpression(ass.Expr))
+ cs.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr), ass.Attributes));
+ if (!ContainsAsymmetricExpression(ass.Expr))
{
- cs.Add(new AssertCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr), ass.Attributes));
- }
- else
- {
- cs.Add(new AssertCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)), ass.Attributes));
+ cs.Add(new AssertCmd(c.tok, new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr), ass.Attributes));
}
}
else if (c is AssumeCmd)
{
AssumeCmd ass = c as AssumeCmd;
- if (ContainsAsymmetricExpression(ass.Expr))
- {
- cs.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
- }
- else if (QKeyValue.FindBoolAttribute(ass.Attributes, "backedge"))
+ if (QKeyValue.FindBoolAttribute(ass.Attributes, "backedge"))
{
cs.Add(new AssumeCmd(c.tok, Expr.Or(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
}
else
{
- cs.Add(new AssumeCmd(c.tok, Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr))));
+ cs.Add(new AssumeCmd(c.tok, new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
+ if (!ContainsAsymmetricExpression(ass.Expr))
+ {
+ cs.Add(new AssumeCmd(c.tok, new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(ass.Expr.Clone() as Expr)));
+ }
}
}
else
|