From 7f0d088b487b9f8eb243934c2445b7338ef7bce7 Mon Sep 17 00:00:00 2001 From: Peter Collingbourne Date: Tue, 12 Jun 2012 21:40:50 +0100 Subject: GPUVerify: the non-uniform loop invariant is not a candidate invariant Thanks to Ally for pointing this out. --- Source/GPUVerify/BlockPredicator.cs | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'Source/GPUVerify') diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs index a006bde6..5e61734d 100644 --- a/Source/GPUVerify/BlockPredicator.cs +++ b/Source/GPUVerify/BlockPredicator.cs @@ -186,9 +186,9 @@ class BlockPredicator { pExpr = Expr.Eq(cur, blockIds[runBlock]); CmdSeq newCmdSeq = new CmdSeq(); + AddNonUniformInvariant(newCmdSeq, runBlock); if (CommandLineOptions.Inference && blockGraph.Headers.Contains(runBlock)) { AddUniformCandidateInvariant(newCmdSeq, runBlock); - AddNonUniformCandidateInvariant(newCmdSeq, runBlock); } newCmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr)); foreach (Cmd cmd in runBlock.Cmds) @@ -215,7 +215,7 @@ class BlockPredicator { "uniform loop")); } - private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) { + private void AddNonUniformInvariant(CmdSeq cs, Block header) { var loopNodes = new HashSet(); foreach (var b in blockGraph.BackEdgeNodes(header)) loopNodes.UnionWith(blockGraph.NaturalLoops(header, b)); @@ -232,10 +232,9 @@ class BlockPredicator { } var curIsHeaderOrExit = exits.Aggregate((Expr)Expr.Eq(cur, blockIds[header]), (e, exit) => Expr.Or(e, Expr.Eq(cur, exit))); - cs.Add(verifier.CreateCandidateInvariant(new NAryExpr(Token.NoToken, - new IfThenElse(Token.NoToken), - new ExprSeq(fp, curIsHeaderOrExit, Expr.Eq(cur, returnBlockId))), - "non-uniform loop")); + cs.Add(new AssertCmd(Token.NoToken, new NAryExpr(Token.NoToken, + new IfThenElse(Token.NoToken), + new ExprSeq(fp, curIsHeaderOrExit, Expr.Eq(cur, returnBlockId))))); } public static void Predicate(GPUVerifier v, Program p) { -- cgit v1.2.3