diff options
| author |  Peter Collingbourne <peter@pcc.me.uk> | 2012-06-07 20:24:21 +0100 |
|---|---|---|
| committer | Peter Collingbourne <peter@pcc.me.uk> | 2012-06-07 20:24:21 +0100 |
| commit | bcb4b69e529235b16d01c99dacb89f617ba9883f (patch) | |
| tree | c4f78ca2eb6739c16061b28601476d69e9635d94 /Source/GPUVerify/KernelDualiser.cs | |
| parent | 281e96f18dcc95347dd5040fcc7f835975420398 (diff) | |
GPUVerify: emit assumes for backedges
Specifically, have the predicator emit backedge assumes with
a :backedge attribute, and have the dualiser recognise such assumes
and create an OR expression instead of an AND expression.
Diffstat (limited to 'Source/GPUVerify/KernelDualiser.cs')
| -rw-r--r-- | Source/GPUVerify/KernelDualiser.cs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Source/GPUVerify/KernelDualiser.cs b/Source/GPUVerify/KernelDualiser.cs index da9a7a32..5c3f6edc 100644 --- a/Source/GPUVerify/KernelDualiser.cs +++ b/Source/GPUVerify/KernelDualiser.cs @@ -203,6 +203,11 @@ namespace GPUVerify {
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"))
+ {
+ 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),
|