From 4dd73ec05586f46a9c7a2aa01e0994dbe7ac2620 Mon Sep 17 00:00:00 2001 From: Peter Collingbourne Date: Mon, 30 Jul 2012 21:47:22 +0100 Subject: VCGeneration: implement smart predication This predication algorithm is intended to reduce the complexity of predicated verification conditions by reducing the amount of predicated state and using only boolean algebra, as opposed to the previous algorithm which also uses integers. It assigns a unique predicate to every superblock, which is defined per Agrawal [1] except that superblocks are further partitioned such that either no element of the same superblock may be contained within a natural loop or each element of the superblock has the same innermost natural loop head. Predicates are assigned at the element of the superblock which dominates all others, and are reset to false at a loop head and at the start of a procedure in order to ensure correct execution for future iterations. When exiting a loop, all predicates corresponding to heads of exited loops are reset to false. The algorithm requires that every successor at every divergence point in the CFG contains assumes marked with an attribute (called ':partition') which a frontend uses to certify to the predicator that for each block, if each successor of that block contains an assume statement marked with :partition, exactly one of those assume statement's predicates will hold. The frontend we use for GPUVerify generates such attributes, and as such the new predicator is only used there, and the old predicator has been retained for Corral etc. [1] Hiralal Agrawal. Dominators, super blocks, and program coverage. In POPL '94, p25-34. --- Source/VCGeneration/GraphAlgorithms.cs | 15 + Source/VCGeneration/SmartBlockPredicator.cs | 466 ++++++++++++++++++++++++++++ Source/VCGeneration/VCGeneration.csproj | 3 +- 3 files changed, 483 insertions(+), 1 deletion(-) create mode 100644 Source/VCGeneration/SmartBlockPredicator.cs diff --git a/Source/VCGeneration/GraphAlgorithms.cs b/Source/VCGeneration/GraphAlgorithms.cs index def77485..1a8ab9b1 100644 --- a/Source/VCGeneration/GraphAlgorithms.cs +++ b/Source/VCGeneration/GraphAlgorithms.cs @@ -8,6 +8,21 @@ namespace Microsoft.Boogie { public static class GraphAlgorithms { + public static Graph Dual(this Graph g, Node dummySource) { + var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList(); + if (exits.Count == 0) + return null; + var dual = new Graph(new HashSet>(g.Edges.Select(e => new Tuple(e.Item2, e.Item1)))); + if (exits.Count == 1) + dual.AddSource(exits[0]); + else { + dual.AddSource(dummySource); + foreach (var exit in exits) + dual.AddEdge(dummySource, exit); + } + return dual; + } + public static List> LoopyTopSort(this Graph g) { Contract.Assert(g.Reducible); diff --git a/Source/VCGeneration/SmartBlockPredicator.cs b/Source/VCGeneration/SmartBlockPredicator.cs new file mode 100644 index 00000000..15f19ce5 --- /dev/null +++ b/Source/VCGeneration/SmartBlockPredicator.cs @@ -0,0 +1,466 @@ +using Graphing; +using System; +using System.Collections.Generic; +using System.Diagnostics; +using System.Diagnostics.Contracts; +using System.Linq; + +namespace Microsoft.Boogie { + +public class SmartBlockPredicator { + + Program prog; + Implementation impl; + Graph blockGraph; + List> sortedBlocks; + + bool createCandidateInvariants = true; + bool useProcedurePredicates = true; + + Dictionary predMap, defMap; + Dictionary> ownedMap; + Dictionary partInfo; + + IdentifierExpr fp; + Dictionary havocVars = + new Dictionary(); + Dictionary blockIds = new Dictionary(); + HashSet doneBlocks = new HashSet(); + + SmartBlockPredicator(Program p, Implementation i, bool cci, bool upp) { + prog = p; + impl = i; + createCandidateInvariants = cci; + useProcedurePredicates = upp; + } + + void PredicateCmd(Expr p, 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(p, block.Cmds, cmd); + nextBlock = block; + } + } + + void PredicateCmd(Expr p, CmdSeq cmdSeq, Cmd cmd) { + if (p == null) { + cmdSeq.Add(cmd); + return; + } + + 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; + Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr); + aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(p, newExpr); + cmdSeq.Add(aCmd); + } 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) { + var sCmd = (StateCmd)cmd; + var newCmdSeq = new CmdSeq(); + foreach (Cmd c in sCmd.Cmds) + PredicateCmd(p, newCmdSeq, c); + sCmd.Cmds = newCmdSeq; + cmdSeq.Add(sCmd); + } + else { + Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString()); + } + } + + void PredicateTransferCmd(Expr p, Block src, CmdSeq cmdSeq, TransferCmd cmd) { + if (cmd is GotoCmd) { + var gCmd = (GotoCmd)cmd; + if (gCmd.labelTargets.Length == 1) { + if (defMap.ContainsKey(gCmd.labelTargets[0])) + PredicateCmd(p, cmdSeq, + Cmd.SimpleAssign(Token.NoToken, + Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True)); + } else { + Debug.Assert(gCmd.labelTargets.Length > 1); + Debug.Assert(gCmd.labelTargets.Cast().All(t => partInfo.ContainsKey(t))); + foreach (Block target in gCmd.labelTargets) { + var part = partInfo[target]; + if (defMap.ContainsKey(part.realDest)) + PredicateCmd(p, cmdSeq, + Cmd.SimpleAssign(Token.NoToken, + Expr.Ident(predMap[part.realDest]), part.pred)); + var predsExitingLoop = new Dictionary>(); + foreach (Block exit in LoopsExited(src, target)) { + List predList; + if (!predsExitingLoop.ContainsKey(exit)) + predList = predsExitingLoop[exit] = new List(); + else + predList = predsExitingLoop[exit]; + predList.Add(part.pred); + } + foreach (var pred in predsExitingLoop) { + PredicateCmd(p, cmdSeq, + Cmd.SimpleAssign(Token.NoToken, + Expr.Ident(predMap[pred.Key]), + Expr.Not(pred.Value.Aggregate(Expr.Or)))); + } + } + } + } else if (cmd is ReturnCmd) { + // Blocks which end in a return will never share a predicate with a block + // which appears after it. Furthermore, such a block cannot be part of a + // loop. So it is safe to do nothing here. + } else { + Console.WriteLine("Unsupported cmd: " + cmd.GetType().ToString()); + } + } + + Variable FreshPredicate(ref int predCount) { + var pVar = new LocalVariable(Token.NoToken, + new TypedIdent(Token.NoToken, + "p" + predCount++, + Microsoft.Boogie.Type.Bool)); + impl.LocVars.Add(pVar); + return pVar; + } + + void AssignPredicates(Graph blockGraph, + DomRelation dom, + DomRelation pdom, + IEnumerator> i, + Variable headPredicate, + ref int predCount, + Dictionary predMap, + Dictionary defMap, + Dictionary> ownedMap) { + var header = i.Current.Item1; + var regionPreds = new List>(); + var ownedPreds = new HashSet(); + ownedMap[header] = ownedPreds; + + predMap[header] = headPredicate; + defMap[header] = headPredicate; + regionPreds.Add(new Tuple(header, headPredicate)); + if (!i.MoveNext()) + return; + + do { + var block = i.Current; + if (block.Item2) { + if (block.Item1 == header) + return; + } else { + if (blockGraph.Headers.Contains(block.Item1)) { + var loopPred = FreshPredicate(ref predCount); + ownedPreds.Add(loopPred); + AssignPredicates(blockGraph, dom, pdom, i, loopPred, ref predCount, + predMap, defMap, ownedMap); + } else { + bool foundExisting = false; + foreach (var regionPred in regionPreds) { + if (dom.DominatedBy(block.Item1, regionPred.Item1) && + pdom.DominatedBy(regionPred.Item1, block.Item1)) { + predMap[block.Item1] = regionPred.Item2; + foundExisting = true; + break; + } + } + if (!foundExisting) { + var condPred = FreshPredicate(ref predCount); + predMap[block.Item1] = condPred; + defMap[block.Item1] = condPred; + ownedPreds.Add(condPred); + regionPreds.Add(new Tuple(block.Item1, condPred)); + } + } + } + } while (i.MoveNext()); + } + + void AssignPredicates(out Dictionary predMap, + out Dictionary defMap, + out Dictionary> ownedMap) { + DomRelation dom = blockGraph.DominatorMap; + + Graph dualGraph = blockGraph.Dual(new Block()); + DomRelation pdom = dualGraph.DominatorMap; + + var iter = sortedBlocks.GetEnumerator(); + if (!iter.MoveNext()) { + predMap = defMap = null; + ownedMap = null; + return; + } + + int predCount = 0; + predMap = new Dictionary(); + defMap = new Dictionary(); + ownedMap = new Dictionary>(); + AssignPredicates(blockGraph, dom, pdom, iter, + useProcedurePredicates ? impl.InParams[0] : null, + ref predCount, predMap, defMap, ownedMap); + } + + IEnumerable LoopsExited(Block src, Block dest) { + var i = sortedBlocks.GetEnumerator(); + while (i.MoveNext()) { + var b = i.Current; + if (b.Item1 == src) { + return LoopsExitedForwardEdge(dest, i); + } else if (b.Item1 == dest) { + return LoopsExitedBackEdge(src, i); + } + } + Debug.Assert(false); + return null; + } + + private IEnumerable LoopsExitedBackEdge(Block src, IEnumerator> i) { + var headsSeen = new HashSet(); + while (i.MoveNext()) { + var b = i.Current; + if (!b.Item2 && blockGraph.Headers.Contains(b.Item1)) + headsSeen.Add(b.Item1); + else if (b.Item2) + headsSeen.Remove(b.Item1); + if (b.Item1 == src) + return headsSeen; + } + Debug.Assert(false); + return null; + } + + private IEnumerable LoopsExitedForwardEdge(Block dest, IEnumerator> i) { + var headsSeen = new HashSet(); + while (i.MoveNext()) { + var b = i.Current; + if (b.Item1 == dest) + yield break; + else if (!b.Item2 && blockGraph.Headers.Contains(b.Item1)) + headsSeen.Add(b.Item1); + else if (b.Item2 && !headsSeen.Contains(b.Item1)) + yield return b.Item1; + } + Debug.Assert(false); + } + + class PartInfo { + public PartInfo(Expr p, Block r) { pred = p; realDest = r; } + public Expr pred; + public Block realDest; + } + + Dictionary BuildPartitionInfo() { + var partInfo = new Dictionary(); + foreach (var block in blockGraph.Nodes) { + var parts = block.Cmds.Cast().TakeWhile( + c => c is AssumeCmd && + QKeyValue.FindBoolAttribute(((AssumeCmd)c).Attributes, "partition")); + + Expr pred = null; + if (parts.Count() > 0) { + pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And); + block.Cmds = + new CmdSeq(block.Cmds.Cast().Skip(parts.Count()).ToArray()); + } else { + continue; + } + + Block realDest = block; + if (block.Cmds.Length == 0) { + var gc = block.TransferCmd as GotoCmd; + if (gc != null && gc.labelTargets.Length == 1) + realDest = gc.labelTargets[0]; + } + partInfo[block] = new PartInfo(pred, realDest); + } + + return partInfo; + } + + void PredicateImplementation() { + blockGraph = prog.ProcessLoops(impl); + sortedBlocks = blockGraph.LoopyTopSort(); + + AssignPredicates(out predMap, out defMap, out ownedMap); + partInfo = BuildPartitionInfo(); + + if (useProcedurePredicates) + fp = Expr.Ident(impl.InParams[0]); + + var newBlocks = new List(); + Block prevBlock = null; + foreach (var n in sortedBlocks) { + var p = predMap[n.Item1]; + var pExpr = Expr.Ident(p); + + if (n.Item2) { + var backedgeBlock = new Block(); + newBlocks.Add(backedgeBlock); + + backedgeBlock.Label = n.Item1.Label + ".backedge"; + backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, pExpr, + 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.Not(pExpr))); + + if (prevBlock != null) + 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); + if (prevBlock != null) + prevBlock.TransferCmd = new GotoCmd(Token.NoToken, + new BlockSeq(runBlock)); + + var transferCmd = runBlock.TransferCmd; + foreach (Cmd cmd in oldCmdSeq) + PredicateCmd(pExpr, newBlocks, runBlock, cmd, out runBlock); + + if (ownedMap.ContainsKey(n.Item1)) { + var owned = ownedMap[n.Item1]; + foreach (var v in owned) + runBlock.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, Expr.Ident(v), Expr.False)); + } + + PredicateTransferCmd(pExpr, runBlock, 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; + } + } + + 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()); + + if (dwf is Procedure) + { + var proc = (Procedure)dwf; + var newRequires = new RequiresSeq(); + foreach (Requires r in proc.Requires) + { + newRequires.Add(new Requires(r.Free, + new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition))); + } + var newEnsures = new EnsuresSeq(); + foreach (Ensures e in proc.Ensures) + { + newEnsures.Add(new Ensures(e.Free, + new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition))); + } + } + + } + + try { + var impl = decl as Implementation; + if (impl != null) + new SmartBlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation(); + } + catch (Program.IrreducibleLoopException) { } + } + } + + public static void Predicate(Program p, Implementation impl) { + try { + new SmartBlockPredicator(p, impl, false, false).PredicateImplementation(); + } + catch (Program.IrreducibleLoopException) { } + } + +} + +} diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj index 39da0be6..780e4891 100644 --- a/Source/VCGeneration/VCGeneration.csproj +++ b/Source/VCGeneration/VCGeneration.csproj @@ -155,6 +155,7 @@ + @@ -223,4 +224,4 @@ --> - \ No newline at end of file + -- cgit v1.2.3