From bcb4b69e529235b16d01c99dacb89f617ba9883f Mon Sep 17 00:00:00 2001 From: Peter Collingbourne Date: Thu, 7 Jun 2012 20:24:21 +0100 Subject: 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. --- Source/GPUVerify/KernelDualiser.cs | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'Source/GPUVerify/KernelDualiser.cs') 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), -- cgit v1.2.3