diff options
| -rw-r--r-- | Source/GPUVerify/CrossThreadInvariantProcessor.cs | 44 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 12 | ||||
| -rw-r--r-- | Source/VCGeneration/BlockPredicator.cs | 614 |
3 files changed, 345 insertions, 325 deletions
diff --git a/Source/GPUVerify/CrossThreadInvariantProcessor.cs b/Source/GPUVerify/CrossThreadInvariantProcessor.cs index 4d215f24..3d64f8dc 100644 --- a/Source/GPUVerify/CrossThreadInvariantProcessor.cs +++ b/Source/GPUVerify/CrossThreadInvariantProcessor.cs @@ -43,7 +43,7 @@ namespace GPUVerify new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
}
- if (call.Func.Name.Equals("__at_most_one"))
+ if (call.Func.Name.Equals("__exclusive"))
{
return Expr.Not(Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
new VariableDualiser(2, verifier.uniformityAnalyser, procName)
@@ -85,11 +85,36 @@ namespace GPUVerify }
}
+ internal void ProcessCrossThreadInvariants(List<Block> blocks)
+ {
+ foreach (Block b in blocks)
+ {
+ b.Cmds = ProcessCrossThreadInvariants(b.Cmds);
+ }
+ }
+
private void ProcessCrossThreadInvariants(BigBlock bb)
{
+ bb.simpleCmds = ProcessCrossThreadInvariants(bb.simpleCmds);
+
+ if (bb.ec is WhileCmd)
+ {
+ WhileCmd whileCmd = bb.ec as WhileCmd;
+ List<PredicateCmd> newInvariants = new List<PredicateCmd>();
+ foreach (PredicateCmd p in whileCmd.Invariants)
+ {
+ newInvariants.Add(new AssertCmd(p.tok, VisitExpr(p.Expr)));
+ }
+ whileCmd.Invariants = newInvariants;
+ ProcessCrossThreadInvariants(whileCmd.Body);
+ }
+ }
+
+ private CmdSeq ProcessCrossThreadInvariants(CmdSeq cmds)
+ {
CmdSeq newCommands = new CmdSeq();
- foreach (Cmd c in bb.simpleCmds)
+ foreach (Cmd c in cmds)
{
if (c is AssertCmd)
{
@@ -104,20 +129,7 @@ namespace GPUVerify newCommands.Add(c);
}
}
-
- bb.simpleCmds = newCommands;
-
- if (bb.ec is WhileCmd)
- {
- WhileCmd whileCmd = bb.ec as WhileCmd;
- List<PredicateCmd> newInvariants = new List<PredicateCmd>();
- foreach (PredicateCmd p in whileCmd.Invariants)
- {
- newInvariants.Add(new AssertCmd(p.tok, VisitExpr(p.Expr)));
- }
- whileCmd.Invariants = newInvariants;
- ProcessCrossThreadInvariants(whileCmd.Body);
- }
+ return newCommands;
}
}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 932b9f1f..79a73a29 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -633,8 +633,16 @@ namespace GPUVerify }
if (d is Implementation)
{
- Implementation i = d as Implementation;
- new CrossThreadInvariantProcessor(this, i.Name).ProcessCrossThreadInvariants(i.StructuredStmts);
+ Implementation impl = d as Implementation;
+
+ if (CommandLineOptions.Unstructured)
+ {
+ new CrossThreadInvariantProcessor(this, impl.Name).ProcessCrossThreadInvariants(impl.Blocks);
+ }
+ else
+ {
+ new CrossThreadInvariantProcessor(this, impl.Name).ProcessCrossThreadInvariants(impl.StructuredStmts);
+ }
}
}
diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs index dcdb087f..226b05e7 100644 --- a/Source/VCGeneration/BlockPredicator.cs +++ b/Source/VCGeneration/BlockPredicator.cs @@ -1,125 +1,125 @@ -using Graphing; -using System; -using System.Collections.Generic; -using System.Diagnostics; -using System.Diagnostics.Contracts; -using System.Linq; - -namespace Microsoft.Boogie { - -public class BlockPredicator { - - Program prog; - Implementation impl; - Graph<Block> blockGraph; - - bool createCandidateInvariants = true; - bool useProcedurePredicates = true; - - Expr returnBlockId; - - LocalVariable curVar, pVar; - IdentifierExpr cur, p, fp; - Expr pExpr; - Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars = - new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>(); - Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>(); - HashSet<Block> doneBlocks = new HashSet<Block>(); - - BlockPredicator(Program p, Implementation i, bool cci, bool upp) { - prog = p; - impl = i; - createCandidateInvariants = cci; - useProcedurePredicates = upp; - } - - void PredicateCmd(List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) { - if (!useProcedurePredicates && cmd is CallCmd) { - var trueBlock = new Block(); - blocks.Add(trueBlock); - trueBlock.Label = block.Label + ".call.true"; - trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p)); - trueBlock.Cmds.Add(cmd); - - var falseBlock = new Block(); - blocks.Add(falseBlock); - falseBlock.Label = block.Label + ".call.false"; - falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p))); - - var contBlock = new Block(); - blocks.Add(contBlock); - contBlock.Label = block.Label + ".call.cont"; - - block.TransferCmd = - new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock)); - trueBlock.TransferCmd = falseBlock.TransferCmd = - new GotoCmd(Token.NoToken, new BlockSeq(contBlock)); - nextBlock = contBlock; - } else { - PredicateCmd(block.Cmds, cmd); - nextBlock = block; - } - } - - void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) { - if (cmd is AssignCmd) { - var aCmd = (AssignCmd)cmd; - cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss, - new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) => - new NAryExpr(Token.NoToken, - new IfThenElse(Token.NoToken), - new ExprSeq(p, rhs, lhs.AsExpr)))))); - } else if (cmd is AssertCmd) { - var aCmd = (AssertCmd)cmd; - if (cmdSeq.Last() is AssignCmd && - cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) { - // This may be a loop invariant. Make sure it continues to appear as - // the first statement in the block. - var assign = cmdSeq.Last(); - cmdSeq.Truncate(cmdSeq.Length-1); - aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr); - cmdSeq.Add(aCmd); - // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr))); - cmdSeq.Add(assign); - } else { - aCmd.Expr = Expr.Imp(p, aCmd.Expr); - cmdSeq.Add(aCmd); - // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr))); - } - } else if (cmd is AssumeCmd) { - var aCmd = (AssumeCmd)cmd; - cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr))); - } else if (cmd is HavocCmd) { - var hCmd = (HavocCmd)cmd; - foreach (IdentifierExpr v in hCmd.Vars) { - Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type; - Contract.Assert(type != null); - - IdentifierExpr havocTempExpr; - if (havocVars.ContainsKey(type)) { - havocTempExpr = havocVars[type]; - } else { - var havocVar = new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, - "_HAVOC_" + type.ToString(), type)); - impl.LocVars.Add(havocVar); - havocVars[type] = havocTempExpr = - new IdentifierExpr(Token.NoToken, havocVar); - } - cmdSeq.Add(new HavocCmd(Token.NoToken, - new IdentifierExprSeq(havocTempExpr))); - cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v, - new NAryExpr(Token.NoToken, - new IfThenElse(Token.NoToken), - new ExprSeq(p, havocTempExpr, v)))); - } - } else if (cmd is CallCmd) { - Debug.Assert(useProcedurePredicates); - var cCmd = (CallCmd)cmd; - cCmd.Ins.Insert(0, p); - cmdSeq.Add(cCmd); - } - else if (cmd is CommentCmd) { +using Graphing;
+using System;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace Microsoft.Boogie {
+
+public class BlockPredicator {
+
+ Program prog;
+ Implementation impl;
+ Graph<Block> blockGraph;
+
+ bool createCandidateInvariants = true;
+ bool useProcedurePredicates = true;
+
+ Expr returnBlockId;
+
+ LocalVariable curVar, pVar;
+ IdentifierExpr cur, p, fp;
+ Expr pExpr;
+ Dictionary<Microsoft.Boogie.Type, IdentifierExpr> havocVars =
+ new Dictionary<Microsoft.Boogie.Type, IdentifierExpr>();
+ Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
+ HashSet<Block> doneBlocks = new HashSet<Block>();
+
+ BlockPredicator(Program p, Implementation i, bool cci, bool upp) {
+ prog = p;
+ impl = i;
+ createCandidateInvariants = cci;
+ useProcedurePredicates = upp;
+ }
+
+ void PredicateCmd(List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {
+ if (!useProcedurePredicates && cmd is CallCmd) {
+ var trueBlock = new Block();
+ blocks.Add(trueBlock);
+ trueBlock.Label = block.Label + ".call.true";
+ trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p));
+ trueBlock.Cmds.Add(cmd);
+
+ var falseBlock = new Block();
+ blocks.Add(falseBlock);
+ falseBlock.Label = block.Label + ".call.false";
+ falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p)));
+
+ var contBlock = new Block();
+ blocks.Add(contBlock);
+ contBlock.Label = block.Label + ".call.cont";
+
+ block.TransferCmd =
+ new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));
+ trueBlock.TransferCmd = falseBlock.TransferCmd =
+ new GotoCmd(Token.NoToken, new BlockSeq(contBlock));
+ nextBlock = contBlock;
+ } else {
+ PredicateCmd(block.Cmds, cmd);
+ nextBlock = block;
+ }
+ }
+
+ void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) {
+ if (cmd is AssignCmd) {
+ var aCmd = (AssignCmd)cmd;
+ cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
+ new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
+ new NAryExpr(Token.NoToken,
+ new IfThenElse(Token.NoToken),
+ new ExprSeq(p, rhs, lhs.AsExpr))))));
+ } else if (cmd is AssertCmd) {
+ var aCmd = (AssertCmd)cmd;
+ if (cmdSeq.Last() is AssignCmd &&
+ cmdSeq.Cast<Cmd>().SkipEnd(1).All(c => c is AssertCmd)) {
+ // This may be a loop invariant. Make sure it continues to appear as
+ // the first statement in the block.
+ var assign = cmdSeq.Last();
+ cmdSeq.Truncate(cmdSeq.Length-1);
+ aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr);
+ cmdSeq.Add(aCmd);
+ // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));
+ cmdSeq.Add(assign);
+ } else {
+ aCmd.Expr = Expr.Imp(p, aCmd.Expr);
+ cmdSeq.Add(aCmd);
+ // cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr)));
+ }
+ } else if (cmd is AssumeCmd) {
+ var aCmd = (AssumeCmd)cmd;
+ cmdSeq.Add(new AssumeCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+ } else if (cmd is HavocCmd) {
+ var hCmd = (HavocCmd)cmd;
+ foreach (IdentifierExpr v in hCmd.Vars) {
+ Microsoft.Boogie.Type type = v.Decl.TypedIdent.Type;
+ Contract.Assert(type != null);
+
+ IdentifierExpr havocTempExpr;
+ if (havocVars.ContainsKey(type)) {
+ havocTempExpr = havocVars[type];
+ } else {
+ var havocVar = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken,
+ "_HAVOC_" + type.ToString(), type));
+ impl.LocVars.Add(havocVar);
+ havocVars[type] = havocTempExpr =
+ new IdentifierExpr(Token.NoToken, havocVar);
+ }
+ cmdSeq.Add(new HavocCmd(Token.NoToken,
+ new IdentifierExprSeq(havocTempExpr)));
+ cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
+ new NAryExpr(Token.NoToken,
+ new IfThenElse(Token.NoToken),
+ new ExprSeq(p, havocTempExpr, v))));
+ }
+ } else if (cmd is CallCmd) {
+ Debug.Assert(useProcedurePredicates);
+ var cCmd = (CallCmd)cmd;
+ cCmd.Ins.Insert(0, p);
+ cmdSeq.Add(cCmd);
+ }
+ else if (cmd is CommentCmd) {
// skip
}
else if (cmd is StateCmd) {
@@ -132,198 +132,198 @@ public class BlockPredicator { }
else {
Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
- } - } - - void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) { - if (cmd is GotoCmd) { - var gCmd = (GotoCmd)cmd; - var targets = new List<Expr>( - gCmd.labelTargets.Cast<Block>().Select(b => blockIds[b])); - if (targets.Count == 1) { - PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0])); - } else { - PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken, - new IdentifierExprSeq(cur))); - PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken, - targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or))); - } - - foreach (Block b in gCmd.labelTargets) { - if (blockGraph.Predecessors(b).Count() == 1) { - if (!doneBlocks.Contains(b)) { - var assumes = b.Cmds.Cast<Cmd>().TakeWhile(c => c is AssumeCmd); - if (assumes.Count() > 0) { - foreach (AssumeCmd aCmd in assumes) { - cmdSeq.Add(new AssumeCmd(Token.NoToken, - Expr.Imp(Expr.Eq(cur, blockIds[b]), - aCmd.Expr))); - } - b.Cmds = - new CmdSeq(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray()); - } - } - } - } - } else if (cmd is ReturnCmd) { - PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId)); - } else { - Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString()); - } - } - - void PredicateImplementation() { - blockGraph = prog.ProcessLoops(impl); - var sortedBlocks = blockGraph.LoopyTopSort(); - - int blockId = 0; - foreach (var block in impl.Blocks) - blockIds[block] = Expr.Literal(blockId++); - returnBlockId = Expr.Literal(blockId++); - - curVar = new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, "cur", - Microsoft.Boogie.Type.Int)); - impl.LocVars.Add(curVar); - cur = Expr.Ident(curVar); - - pVar = new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, "p", - Microsoft.Boogie.Type.Bool)); - impl.LocVars.Add(pVar); - p = Expr.Ident(pVar); - - if (useProcedurePredicates) - fp = Expr.Ident(impl.InParams[0]); - - var newBlocks = new List<Block>(); - - Block entryBlock = new Block(); - entryBlock.Label = "entry"; - entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur, - CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1], - returnBlockId))); - newBlocks.Add(entryBlock); - - 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); - - tailBlock.Label = n.Item1.Label + ".tail"; - tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, - Expr.Neq(cur, blockIds[n.Item1]))); - - prevBlock.TransferCmd = new GotoCmd(Token.NoToken, - new BlockSeq(backedgeBlock, tailBlock)); - prevBlock = tailBlock; - } else { - var runBlock = n.Item1; - var oldCmdSeq = runBlock.Cmds; - runBlock.Cmds = new CmdSeq(); - newBlocks.Add(runBlock); - prevBlock.TransferCmd = new GotoCmd(Token.NoToken, - new BlockSeq(runBlock)); - - pExpr = Expr.Eq(cur, blockIds[runBlock]); - if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) { - AddUniformCandidateInvariant(runBlock.Cmds, runBlock); - AddNonUniformCandidateInvariant(runBlock.Cmds, runBlock); - } - runBlock.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr)); - var transferCmd = runBlock.TransferCmd; - foreach (Cmd cmd in oldCmdSeq) - PredicateCmd(newBlocks, runBlock, cmd, out runBlock); - PredicateTransferCmd(runBlock.Cmds, transferCmd); - - prevBlock = runBlock; - doneBlocks.Add(runBlock); - } - } - - prevBlock.TransferCmd = new ReturnCmd(Token.NoToken); - impl.Blocks = newBlocks; - } - - private Expr CreateIfFPThenElse(Expr then, Expr eElse) { - if (useProcedurePredicates) { - return new NAryExpr(Token.NoToken, - new IfThenElse(Token.NoToken), - new ExprSeq(fp, then, eElse)); - } else { - return then; - } - } - - private void AddUniformCandidateInvariant(CmdSeq cs, Block header) { - cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur, - CreateIfFPThenElse(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(prog.CreateCandidateInvariant( - CreateIfFPThenElse(curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)), - "non-uniform loop")); - } - - public static void Predicate(Program p, - bool createCandidateInvariants = true, - bool useProcedurePredicates = true) { - foreach (var decl in p.TopLevelDeclarations.ToList()) { - if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) { - var dwf = (DeclWithFormals)decl; - var fpVar = new Formal(Token.NoToken, - new TypedIdent(Token.NoToken, "_P", - Microsoft.Boogie.Type.Bool), - /*incoming=*/true); - dwf.InParams = new VariableSeq( - (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>())) - .ToArray()); + }
+ }
+
+ void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) {
+ if (cmd is GotoCmd) {
+ var gCmd = (GotoCmd)cmd;
+ var targets = new List<Expr>(
+ gCmd.labelTargets.Cast<Block>().Select(b => blockIds[b]));
+ if (targets.Count == 1) {
+ PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0]));
+ } else {
+ PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken,
+ new IdentifierExprSeq(cur)));
+ PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken,
+ targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or)));
+ }
+
+ foreach (Block b in gCmd.labelTargets) {
+ if (blockGraph.Predecessors(b).Count() == 1) {
+ if (!doneBlocks.Contains(b)) {
+ var assumes = b.Cmds.Cast<Cmd>().TakeWhile(c => c is AssumeCmd);
+ if (assumes.Count() > 0) {
+ foreach (AssumeCmd aCmd in assumes) {
+ cmdSeq.Add(new AssumeCmd(Token.NoToken,
+ Expr.Imp(Expr.Eq(cur, blockIds[b]),
+ aCmd.Expr)));
+ }
+ b.Cmds =
+ new CmdSeq(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray());
+ }
+ }
+ }
+ }
+ } else if (cmd is ReturnCmd) {
+ PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, returnBlockId));
+ } else {
+ Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString());
+ }
+ }
+
+ void PredicateImplementation() {
+ blockGraph = prog.ProcessLoops(impl);
+ var sortedBlocks = blockGraph.LoopyTopSort();
+
+ int blockId = 0;
+ foreach (var block in impl.Blocks)
+ blockIds[block] = Expr.Literal(blockId++);
+ returnBlockId = Expr.Literal(blockId++);
+
+ curVar = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, "cur",
+ Microsoft.Boogie.Type.Int));
+ impl.LocVars.Add(curVar);
+ cur = Expr.Ident(curVar);
+
+ pVar = new LocalVariable(Token.NoToken,
+ new TypedIdent(Token.NoToken, "p",
+ Microsoft.Boogie.Type.Bool));
+ impl.LocVars.Add(pVar);
+ p = Expr.Ident(pVar);
+
+ if (useProcedurePredicates)
+ fp = Expr.Ident(impl.InParams[0]);
+
+ var newBlocks = new List<Block>();
+
+ Block entryBlock = new Block();
+ entryBlock.Label = "entry";
+ entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur,
+ CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1],
+ returnBlockId)));
+ newBlocks.Add(entryBlock);
+
+ 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);
+
+ tailBlock.Label = n.Item1.Label + ".tail";
+ tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
+ Expr.Neq(cur, blockIds[n.Item1])));
+
+ prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
+ new BlockSeq(backedgeBlock, tailBlock));
+ prevBlock = tailBlock;
+ } else {
+ var runBlock = n.Item1;
+ var oldCmdSeq = runBlock.Cmds;
+ runBlock.Cmds = new CmdSeq();
+ newBlocks.Add(runBlock);
+ prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
+ new BlockSeq(runBlock));
+
+ pExpr = Expr.Eq(cur, blockIds[runBlock]);
+ if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) {
+ AddUniformCandidateInvariant(runBlock.Cmds, runBlock);
+ AddNonUniformCandidateInvariant(runBlock.Cmds, runBlock);
+ }
+ runBlock.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr));
+ var transferCmd = runBlock.TransferCmd;
+ foreach (Cmd cmd in oldCmdSeq)
+ PredicateCmd(newBlocks, runBlock, cmd, out runBlock);
+ PredicateTransferCmd(runBlock.Cmds, transferCmd);
+
+ prevBlock = runBlock;
+ doneBlocks.Add(runBlock);
+ }
+ }
+
+ prevBlock.TransferCmd = new ReturnCmd(Token.NoToken);
+ impl.Blocks = newBlocks;
+ }
+
+ private Expr CreateIfFPThenElse(Expr then, Expr eElse) {
+ if (useProcedurePredicates) {
+ return new NAryExpr(Token.NoToken,
+ new IfThenElse(Token.NoToken),
+ new ExprSeq(fp, then, eElse));
+ } else {
+ return then;
+ }
+ }
+
+ private void AddUniformCandidateInvariant(CmdSeq cs, Block header) {
+ cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur,
+ CreateIfFPThenElse(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(prog.CreateCandidateInvariant(
+ CreateIfFPThenElse(curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)),
+ "non-uniform loop"));
+ }
+
+ public static void Predicate(Program p,
+ bool createCandidateInvariants = true,
+ bool useProcedurePredicates = true) {
+ foreach (var decl in p.TopLevelDeclarations.ToList()) {
+ if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) {
+ var dwf = (DeclWithFormals)decl;
+ var fpVar = new Formal(Token.NoToken,
+ new TypedIdent(Token.NoToken, "_P",
+ Microsoft.Boogie.Type.Bool),
+ /*incoming=*/true);
+ dwf.InParams = new VariableSeq(
+ (new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
+ .ToArray());
}
try {
var impl = decl as Implementation;
if (impl != null)
new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();
}
- catch (Program.IrreducibleLoopException) { } - } - } - + catch (Program.IrreducibleLoopException) { }
+ }
+ }
+
public static void Predicate(Program p, Implementation impl) {
try {
new BlockPredicator(p, impl, false, false).PredicateImplementation();
}
- catch (Program.IrreducibleLoopException) { } - } - -} - -} + catch (Program.IrreducibleLoopException) { }
+ }
+
+}
+
+}
|