From 4fffb5b2570db1c0acacddc6aa6dfd9304ef98ec Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 2 Jul 2012 11:26:47 +0100 Subject: Started adding support for annotation intrinsics for unstructured programs. --- Source/GPUVerify/CrossThreadInvariantProcessor.cs | 44 +- Source/GPUVerify/GPUVerifier.cs | 12 +- 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 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 newInvariants = new List(); + 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 newInvariants = new List(); - 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 blockGraph; - - bool createCandidateInvariants = true; - bool useProcedurePredicates = true; - - Expr returnBlockId; - - LocalVariable curVar, pVar; - IdentifierExpr cur, p, fp; - Expr pExpr; - Dictionary havocVars = - new Dictionary(); - Dictionary blockIds = new Dictionary(); - HashSet doneBlocks = new HashSet(); - - BlockPredicator(Program p, Implementation i, bool cci, bool upp) { - prog = p; - impl = i; - createCandidateInvariants = cci; - useProcedurePredicates = upp; - } - - void PredicateCmd(List 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(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().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 blockGraph; + + bool createCandidateInvariants = true; + bool useProcedurePredicates = true; + + Expr returnBlockId; + + LocalVariable curVar, pVar; + IdentifierExpr cur, p, fp; + Expr pExpr; + Dictionary havocVars = + new Dictionary(); + Dictionary blockIds = new Dictionary(); + HashSet doneBlocks = new HashSet(); + + BlockPredicator(Program p, Implementation i, bool cci, bool upp) { + prog = p; + impl = i; + createCandidateInvariants = cci; + useProcedurePredicates = upp; + } + + void PredicateCmd(List 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(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().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( - gCmd.labelTargets.Cast().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().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().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 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(), 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(); - foreach (var b in blockGraph.BackEdgeNodes(header)) - loopNodes.UnionWith(blockGraph.NaturalLoops(header, b)); - var exits = new HashSet(); - foreach (var ln in loopNodes) { - if (ln.TransferCmd is GotoCmd) { - var gCmd = (GotoCmd) ln.TransferCmd; - foreach (var exit in gCmd.labelTargets.Cast() - .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())) - .ToArray()); + } + } + + void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) { + if (cmd is GotoCmd) { + var gCmd = (GotoCmd)cmd; + var targets = new List( + gCmd.labelTargets.Cast().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().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().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 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(), 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(); + foreach (var b in blockGraph.BackEdgeNodes(header)) + loopNodes.UnionWith(blockGraph.NaturalLoops(header, b)); + var exits = new HashSet(); + foreach (var ln in loopNodes) { + if (ln.TransferCmd is GotoCmd) { + var gCmd = (GotoCmd) ln.TransferCmd; + foreach (var exit in gCmd.labelTargets.Cast() + .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())) + .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) { } + } + +} + +} -- cgit v1.2.3