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 | |
| 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.
| -rw-r--r-- | Source/GPUVerify/BlockPredicator.cs | 12 | ||||
| -rw-r--r-- | Source/GPUVerify/KernelDualiser.cs | 5 |
2 files changed, 16 insertions, 1 deletions
diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs index 6521960c..29255161 100644 --- a/Source/GPUVerify/BlockPredicator.cs +++ b/Source/GPUVerify/BlockPredicator.cs @@ -158,6 +158,16 @@ class BlockPredicator { var prevBlock = entryBlock; foreach (var n in sortedBlocks) { if (n.Item2) { + var backedgeBlock = new Block();
+ newBlocks.Add(backedgeBlock);
+
+ backedgeBlock.Label = n.Item1.Label + ".backedge"; + backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
+ Expr.Eq(cur, blockIds[n.Item1]),
+ new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));
+ backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
+ new BlockSeq(n.Item1)); + var tailBlock = new Block(); newBlocks.Add(tailBlock); @@ -166,7 +176,7 @@ class BlockPredicator { Expr.Neq(cur, blockIds[n.Item1]))); prevBlock.TransferCmd = new GotoCmd(Token.NoToken, - new BlockSeq(tailBlock, n.Item1)); + new BlockSeq(backedgeBlock, tailBlock)); prevBlock = tailBlock; } else { var runBlock = n.Item1; 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),
|