From fde61624bc8b47a947d0da8a76632e8b8aeaacb6 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 5 Apr 2015 17:26:44 +0100 Subject: Patch by Jeroen Ketema. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Drop the “basic” block predication algorithm. Block predication is only used by GPUVerify, and then only in the “smart” version as the basic algorithm does not perform very well. As a consequence this code is essentially dead. --- Source/Predication/BlockPredicator.cs | 378 ----------------------------- Source/Predication/Predication.csproj | 3 +- Source/Predication/SmartBlockPredicator.cs | 28 +++ 3 files changed, 29 insertions(+), 380 deletions(-) delete mode 100644 Source/Predication/BlockPredicator.cs (limited to 'Source') diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs deleted file mode 100644 index 82f346c9..00000000 --- a/Source/Predication/BlockPredicator.cs +++ /dev/null @@ -1,378 +0,0 @@ -using Microsoft.Boogie.GraphUtil; -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 List { trueBlock, falseBlock }); - trueBlock.TransferCmd = falseBlock.TransferCmd = - new GotoCmd(Token.NoToken, new List { contBlock }); - nextBlock = contBlock; - } else { - PredicateCmd(block.Cmds, cmd); - nextBlock = block; - } - } - - void PredicateCmd(List 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 List { 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.RemoveAt(cmdSeq.Count-1); - Expr newExpr = new EnabledReplacementVisitor(pExpr, null).VisitExpr(aCmd.Expr); - aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(pExpr, newExpr); - 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 List { havocTempExpr })); - cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v, - new NAryExpr(Token.NoToken, - new IfThenElse(Token.NoToken), - new List { 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) { - var sCmd = (StateCmd)cmd; - var newCmdSeq = new List(); - foreach (Cmd c in sCmd.Cmds) - PredicateCmd(newCmdSeq, c); - sCmd.Cmds = newCmdSeq; - cmdSeq.Add(sCmd); - } - else { - Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString()); - } - } - - void PredicateTransferCmd(List 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 List { 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 List(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 List { 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 List { 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 List { n.Item1 }); - - var tailBlock = new Block(); - newBlocks.Add(tailBlock); - - tailBlock.Label = n.Item1.Label + ".tail"; - tailBlock.Cmds = new List { new AssumeCmd(Token.NoToken, - Expr.Neq(cur, blockIds[n.Item1])) }; - - prevBlock.TransferCmd = new GotoCmd(Token.NoToken, - new List { backedgeBlock, tailBlock }); - prevBlock = tailBlock; - } else { - var runBlock = n.Item1; - var oldCmdSeq = runBlock.Cmds; - runBlock.Cmds = new List(); - newBlocks.Add(runBlock); - prevBlock.TransferCmd = new GotoCmd(Token.NoToken, - new List { 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 List{ fp, then, eElse }); - } else { - return then; - } - } - - private void AddUniformCandidateInvariant(List cs, Block header) { - cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur, - CreateIfFPThenElse(blockIds[header], returnBlockId)), - "uniform loop")); - } - - private void AddNonUniformCandidateInvariant(List 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 List( - (new Variable[] {fpVar}.Concat(dwf.InParams.Cast())) - .ToArray()); - - if (dwf is Procedure) - { - var proc = (Procedure)dwf; - var newRequires = new List(); - foreach (Requires r in proc.Requires) - { - newRequires.Add(new Requires(r.Free, - new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar), Expr.True).VisitExpr(r.Condition))); - } - var newEnsures = new List(); - foreach (Ensures e in proc.Ensures) - { - newEnsures.Add(new Ensures(e.Free, - new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar), Expr.True).VisitExpr(e.Condition))); - } - } - - } - - try { - var impl = decl as Implementation; - if (impl != null) - new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation(); - } - catch (Program.IrreducibleLoopException) { } - } - } - - public static void Predicate(Program p, Implementation impl) { - try { - new BlockPredicator(p, impl, false, false).PredicateImplementation(); - } - catch (Program.IrreducibleLoopException) { } - } - -} - - -class EnabledReplacementVisitor : StandardVisitor -{ - private Expr pExpr; - private Expr pDomExpr; - - internal EnabledReplacementVisitor(Expr pExpr, Expr pDomExpr) - { - this.pExpr = pExpr; - this.pDomExpr = pDomExpr; - } - - public override Expr VisitExpr(Expr node) - { - if (node is IdentifierExpr) - { - IdentifierExpr iExpr = node as IdentifierExpr; - if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__enabled")) - { - return pExpr; - } else if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__dominator_enabled")) - { - return pDomExpr; - } - } - return base.VisitExpr(node); - } -} - -} diff --git a/Source/Predication/Predication.csproj b/Source/Predication/Predication.csproj index 9c32b379..382a8aca 100644 --- a/Source/Predication/Predication.csproj +++ b/Source/Predication/Predication.csproj @@ -135,7 +135,6 @@ - @@ -172,4 +171,4 @@ --> - \ No newline at end of file + diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index 7579158d..739f0e2b 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -606,4 +606,32 @@ public class SmartBlockPredicator { } +class EnabledReplacementVisitor : StandardVisitor +{ + private Expr pExpr; + private Expr pDomExpr; + + internal EnabledReplacementVisitor(Expr pExpr, Expr pDomExpr) + { + this.pExpr = pExpr; + this.pDomExpr = pDomExpr; + } + + public override Expr VisitExpr(Expr node) + { + if (node is IdentifierExpr) + { + IdentifierExpr iExpr = node as IdentifierExpr; + if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__enabled")) + { + return pExpr; + } else if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__dominator_enabled")) + { + return pDomExpr; + } + } + return base.VisitExpr(node); + } +} + } -- cgit v1.2.3