diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/GPUVerify/BlockPredicator.cs | 42 |
1 files changed, 35 insertions, 7 deletions
diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs index 26a4f39b..a006bde6 100644 --- a/Source/GPUVerify/BlockPredicator.cs +++ b/Source/GPUVerify/BlockPredicator.cs @@ -17,7 +17,7 @@ class BlockPredicator { Expr returnBlockId; LocalVariable curVar, pVar; - IdentifierExpr cur, p; + IdentifierExpr cur, p, fp; Expr pExpr; Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars = new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>(); @@ -147,7 +147,7 @@ class BlockPredicator { var newBlocks = new List<Block>(); - var fp = Expr.Ident(impl.InParams[0]); + fp = Expr.Ident(impl.InParams[0]); Block entryBlock = new Block(); entryBlock.Label = "entry"; entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur, @@ -187,11 +187,8 @@ class BlockPredicator { pExpr = Expr.Eq(cur, blockIds[runBlock]); CmdSeq newCmdSeq = new CmdSeq(); if (CommandLineOptions.Inference && blockGraph.Headers.Contains(runBlock)) { - newCmdSeq.Add(verifier.CreateCandidateInvariant(Expr.Eq(cur, - new NAryExpr(Token.NoToken, - new IfThenElse(Token.NoToken), - new ExprSeq(fp, blockIds[runBlock], returnBlockId))), - "uniform loop")); + AddUniformCandidateInvariant(newCmdSeq, runBlock); + AddNonUniformCandidateInvariant(newCmdSeq, runBlock); } newCmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr)); foreach (Cmd cmd in runBlock.Cmds) @@ -210,6 +207,37 @@ class BlockPredicator { impl.Blocks = newBlocks; } + private void AddUniformCandidateInvariant(CmdSeq cs, Block header) { + cs.Add(verifier.CreateCandidateInvariant(Expr.Eq(cur, + new NAryExpr(Token.NoToken, + new IfThenElse(Token.NoToken), + new ExprSeq(fp, blockIds[header], returnBlockId))), + "uniform loop")); + } + + private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) { + var loopNodes = new HashSet<Block>(); + foreach (var b in blockGraph.BackEdgeNodes(header)) + loopNodes.UnionWith(blockGraph.NaturalLoops(header, b)); + var exits = new HashSet<Expr>(); + foreach (var ln in loopNodes) { + if (ln.TransferCmd is GotoCmd) { + var gCmd = (GotoCmd) ln.TransferCmd; + foreach (var exit in gCmd.labelTargets.Cast<Block>() + .Where(b => !loopNodes.Contains(b))) + exits.Add(blockIds[exit]); + } + if (ln.TransferCmd is ReturnCmd) + exits.Add(returnBlockId); + } + 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")); + } + public static void Predicate(GPUVerifier v, Program p) { foreach (var decl in p.TopLevelDeclarations.ToList()) { if (decl is DeclWithFormals && !(decl is Function)) { |