diff options
author | 2012-06-12 21:40:50 +0100 | |
---|---|---|
committer | 2012-06-12 21:40:50 +0100 | |
commit | 7f0d088b487b9f8eb243934c2445b7338ef7bce7 (patch) | |
tree | e930335d6b1e56c30eccf5a30b7b4f1d36128bf0 /Source/GPUVerify/BlockPredicator.cs | |
parent | 6a2d1e99fe29fa6558a5b5186b174c9041069d6c (diff) |
GPUVerify: the non-uniform loop invariant is not a candidate invariant
Thanks to Ally for pointing this out.
Diffstat (limited to 'Source/GPUVerify/BlockPredicator.cs')
-rw-r--r-- | Source/GPUVerify/BlockPredicator.cs | 11 |
1 files changed, 5 insertions, 6 deletions
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<Block>(); 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) { |