From 8d7686cd88736d117e37eb9bf9dd17404a294ff4 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 3 Oct 2012 12:32:19 -0700 Subject: bunch of refactorings - moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs --- Source/Predication/BlockPredicator.cs | 373 ++++++++++++++++++ Source/Predication/Predication.csproj | 87 +++++ Source/Predication/SmartBlockPredicator.cs | 528 ++++++++++++++++++++++++++ Source/Predication/UniformityAnalyser.cs | 591 +++++++++++++++++++++++++++++ 4 files changed, 1579 insertions(+) create mode 100644 Source/Predication/BlockPredicator.cs create mode 100644 Source/Predication/Predication.csproj create mode 100644 Source/Predication/SmartBlockPredicator.cs create mode 100644 Source/Predication/UniformityAnalyser.cs (limited to 'Source/Predication') diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs new file mode 100644 index 00000000..8419471e --- /dev/null +++ b/Source/Predication/BlockPredicator.cs @@ -0,0 +1,373 @@ +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 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); + Expr newExpr = new EnabledReplacementVisitor(pExpr).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 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(newCmdSeq, c); + sCmd.Cmds = newCmdSeq; + cmdSeq.Add(sCmd); + } + 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()); + + 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 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; + + internal EnabledReplacementVisitor(Expr pExpr) + { + this.pExpr = pExpr; + } + + 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; + } + } + return base.VisitExpr(node); + } +} + +} diff --git a/Source/Predication/Predication.csproj b/Source/Predication/Predication.csproj new file mode 100644 index 00000000..d5ed2a9e --- /dev/null +++ b/Source/Predication/Predication.csproj @@ -0,0 +1,87 @@ + + + + + Debug + AnyCPU + {AFAA5CE1-C41B-44F0-88F8-FD8A43826D44} + Library + Properties + Predication + Predication + v4.0 + 512 + Client + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + + + true + + + InterimKey.snk + + + + + + + + + + + + + + + + + + + {43dfad18-3e35-4558-9be2-caff6b5ba8a0} + Basetypes + + + {b230a69c-c466-4065-b9c1-84d80e76d802} + Core + + + {69a2b0b8-bcac-4101-ae7a-556fcc58c06e} + Graph + + + {fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5} + ParserHelper + + + {e1f10180-c7b9-4147-b51f-fa1b701966dc} + VCGeneration + + + + + + + + \ No newline at end of file diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs new file mode 100644 index 00000000..9478595b --- /dev/null +++ b/Source/Predication/SmartBlockPredicator.cs @@ -0,0 +1,528 @@ +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 SmartBlockPredicator { + + Program prog; + Implementation impl; + Graph blockGraph; + List> sortedBlocks; + + Func useProcedurePredicates; + + Dictionary predMap, defMap; + Dictionary> ownedMap; + Dictionary parentMap; + Dictionary partInfo; + + IdentifierExpr fp; + Dictionary havocVars = + new Dictionary(); + Dictionary blockIds = new Dictionary(); + HashSet doneBlocks = new HashSet(); + bool myUseProcedurePredicates; + UniformityAnalyser uni; + + SmartBlockPredicator(Program p, Implementation i, Func upp, UniformityAnalyser u) { + prog = p; + impl = i; + useProcedurePredicates = upp; + myUseProcedurePredicates = useProcedurePredicates(i.Proc); + uni = u; + } + + void PredicateCmd(Expr p, List blocks, Block block, Cmd cmd, out Block nextBlock) { + var cCmd = cmd as CallCmd; + if (cCmd != null && !useProcedurePredicates(cCmd.Proc)) { + if (p == null) { + block.Cmds.Add(cmd); + nextBlock = block; + return; + } + + 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 (cmd is CallCmd) { + var cCmd = (CallCmd)cmd; + Debug.Assert(useProcedurePredicates(cCmd.Proc)); + cCmd.Ins.Insert(0, p != null ? p : Expr.True); + cmdSeq.Add(cCmd); + } else if (p == null) { + cmdSeq.Add(cmd); + } else 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 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()); + } + } + + // hasPredicatedRegion is true iff the block or its targets are predicated + // (i.e. we enter, stay within or exit a predicated region). + void PredicateTransferCmd(Expr p, Block src, CmdSeq cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) { + hasPredicatedRegion = predMap.ContainsKey(src); + + if (cmd is GotoCmd) { + var gCmd = (GotoCmd)cmd; + + hasPredicatedRegion = hasPredicatedRegion || + gCmd.labelTargets.Cast().Any(b => predMap.ContainsKey(b)); + + 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 => uni.IsUniform(impl.Name, t) || + partInfo.ContainsKey(t))); + foreach (Block target in gCmd.labelTargets) { + if (!partInfo.ContainsKey(target)) + continue; + + 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) { + var header = i.Current.Item1; + var regionPreds = new List>(); + var ownedPreds = new HashSet(); + ownedMap[header] = ownedPreds; + + if (headPredicate != null) { + predMap[header] = headPredicate; + defMap[header] = headPredicate; + regionPreds.Add(new Tuple(header, headPredicate)); + } + + while (i.MoveNext()) { + var block = i.Current; + if (uni != null && uni.IsUniform(impl.Name, block.Item1)) + continue; + if (block.Item2) { + if (block.Item1 == header) + return; + } else { + if (blockGraph.Headers.Contains(block.Item1)) { + parentMap[block.Item1] = header; + var loopPred = FreshPredicate(ref predCount); + ownedPreds.Add(loopPred); + AssignPredicates(blockGraph, dom, pdom, i, loopPred, ref predCount); + } 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)); + } + } + } + } + } + + void AssignPredicates() { + 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>(); + parentMap = new Dictionary(); + AssignPredicates(blockGraph, dom, pdom, iter, + myUseProcedurePredicates ? impl.InParams[0] : null, + ref predCount); + } + + 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) { + if (uni.IsUniform(impl.Name, block)) + continue; + + 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(); + partInfo = BuildPartitionInfo(); + + if (myUseProcedurePredicates) + fp = Expr.Ident(impl.InParams[0]); + + var newBlocks = new List(); + Block prevBlock = null; + foreach (var n in sortedBlocks) { + if (predMap.ContainsKey(n.Item1)) { + 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 (uni != null && !uni.IsUniform(impl.Name, n.Item1)) { + uni.AddNonUniform(impl.Name, backedgeBlock); + uni.AddNonUniform(impl.Name, tailBlock); + } + + if (prevBlock != null) + prevBlock.TransferCmd = new GotoCmd(Token.NoToken, + new BlockSeq(backedgeBlock, tailBlock)); + prevBlock = tailBlock; + } else { + PredicateBlock(pExpr, n.Item1, newBlocks, ref prevBlock); + } + } else { + if (!n.Item2) { + PredicateBlock(null, n.Item1, newBlocks, ref prevBlock); + } + } + } + + if (prevBlock != null) + prevBlock.TransferCmd = new ReturnCmd(Token.NoToken); + + impl.Blocks = newBlocks; + } + + private void PredicateBlock(Expr pExpr, Block block, List newBlocks, ref Block prevBlock) { + var firstBlock = block; + + var oldCmdSeq = block.Cmds; + block.Cmds = new CmdSeq(); + newBlocks.Add(block); + if (prevBlock != null) { + prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(block)); + } + + if (parentMap.ContainsKey(block)) { + var parent = parentMap[block]; + if (predMap.ContainsKey(parent)) { + var parentPred = predMap[parent]; + if (parentPred != null) { + block.Cmds.Add(new AssertCmd(Token.NoToken, + pExpr != null ? (Expr)Expr.Imp(pExpr, Expr.Ident(parentPred)) + : Expr.Ident(parentPred))); + } + } + } + + var transferCmd = block.TransferCmd; + foreach (Cmd cmd in oldCmdSeq) + PredicateCmd(pExpr, newBlocks, block, cmd, out block); + + if (ownedMap.ContainsKey(firstBlock)) { + var owned = ownedMap[firstBlock]; + foreach (var v in owned) + block.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, Expr.Ident(v), Expr.False)); + } + + bool hasPredicatedRegion; + PredicateTransferCmd(pExpr, block, block.Cmds, transferCmd, out hasPredicatedRegion); + + if (hasPredicatedRegion) + prevBlock = block; + else + prevBlock = null; + + doneBlocks.Add(block); + } + + private Expr CreateIfFPThenElse(Expr then, Expr eElse) { + if (myUseProcedurePredicates) { + return new NAryExpr(Token.NoToken, + new IfThenElse(Token.NoToken), + new ExprSeq(fp, then, eElse)); + } else { + return then; + } + } + + public static void Predicate(Program p, + Func useProcedurePredicates = null, + UniformityAnalyser uni = null) { + useProcedurePredicates = useProcedurePredicates ?? (proc => false); + if (uni != null) { + var oldUPP = useProcedurePredicates; + useProcedurePredicates = proc => oldUPP(proc) && !uni.IsUniform(proc.Name); + } + + foreach (var decl in p.TopLevelDeclarations.ToList()) { + if (decl is Procedure || decl is Implementation) { + var proc = decl as Procedure; + Implementation impl = null; + if (proc == null) { + impl = (Implementation)decl; + proc = impl.Proc; + } + + bool upp = useProcedurePredicates(proc); + if (upp) { + 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 (impl == null) { + 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))); + } + } + } + + if (impl != null) { + try { + new SmartBlockPredicator(p, impl, useProcedurePredicates, uni).PredicateImplementation(); + } catch (Program.IrreducibleLoopException) { } + } + } + } + } + + public static void Predicate(Program p, Implementation impl) { + try { + new SmartBlockPredicator(p, impl, proc => false, null).PredicateImplementation(); + } + catch (Program.IrreducibleLoopException) { } + } + +} + +} diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs new file mode 100644 index 00000000..3408d88b --- /dev/null +++ b/Source/Predication/UniformityAnalyser.cs @@ -0,0 +1,591 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using Microsoft.Boogie; +using System.Diagnostics; +using Microsoft.Boogie.GraphUtil; + +namespace Microsoft.Boogie +{ + + public class UniformityAnalyser + { + private Program prog; + + private bool doAnalysis, unstructured; + + private ISet entryPoints; + + private IEnumerable nonUniformVars; + + private bool ProcedureChanged; + + private Dictionary>> uniformityInfo; + + private Dictionary> nonUniformLoops; + + private Dictionary> nonUniformBlocks; + + private Dictionary> loopsWithNonuniformReturn; + + private Dictionary> inParameters; + + private Dictionary> outParameters; + + private List loopStack; + + private bool hitNonuniformReturn; + + /// + /// Simplifies the CFG of the given implementation impl by merging each + /// basic block with a single predecessor into that predecessor if the + /// predecessor has a single successor. If a uniformity analyser is + /// being used then block will only be merged if they are both uniform + /// or both non-uniform + /// + public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl, UniformityAnalyser uni) + { + var blockGraph = prog.ProcessLoops(impl); + var predMap = new Dictionary(); + foreach (var block in blockGraph.Nodes) + { + try + { + var pred = blockGraph.Predecessors(block).Single(); + if (blockGraph.Successors(pred).Single() == block && + (uni == null || + (uni.IsUniform(impl.Name, pred) && uni.IsUniform(impl.Name, block)) || + (!uni.IsUniform(impl.Name, pred) && !uni.IsUniform(impl.Name, block)))) + { + Block predMapping; + while (predMap.TryGetValue(pred, out predMapping)) + pred = predMapping; + pred.Cmds.AddRange(block.Cmds); + pred.TransferCmd = block.TransferCmd; + impl.Blocks.Remove(block); + predMap[block] = pred; + } + // If Single throws an exception above (i.e. not exactly one pred/succ), skip this block. + } + catch (InvalidOperationException) { } + } + } + + public UniformityAnalyser(Program prog, bool doAnalysis, bool unstructured, ISet entryPoints, IEnumerable nonUniformVars) + { + this.prog = prog; + this.doAnalysis = doAnalysis; + this.unstructured = unstructured; + this.entryPoints = entryPoints; + this.nonUniformVars = nonUniformVars; + uniformityInfo = new Dictionary>>(); + nonUniformLoops = new Dictionary>(); + nonUniformBlocks = new Dictionary>(); + loopsWithNonuniformReturn = new Dictionary>(); + inParameters = new Dictionary>(); + outParameters = new Dictionary>(); + loopStack = new List(); + } + + public void Analyse() + { + var impls = prog.TopLevelDeclarations.OfType(); + + foreach (var Impl in impls) + { + bool uniformProcedure = doAnalysis || entryPoints.Contains(Impl); + + uniformityInfo.Add(Impl.Name, new KeyValuePair> + (uniformProcedure, new Dictionary ())); + + nonUniformLoops.Add(Impl.Name, new HashSet()); + loopsWithNonuniformReturn.Add(Impl.Name, new HashSet()); + + foreach (var v in nonUniformVars) + SetNonUniform(Impl.Name, v.Name); + + foreach (Variable v in Impl.LocVars) + { + if (doAnalysis) + { + SetUniform(Impl.Name, v.Name); + } + else + { + SetNonUniform(Impl.Name, v.Name); + } + } + + inParameters[Impl.Name] = new List(); + + foreach (Variable v in Impl.InParams) + { + inParameters[Impl.Name].Add(v.Name); + if (doAnalysis) + { + SetUniform(Impl.Name, v.Name); + } + else + { + SetNonUniform(Impl.Name, v.Name); + } + } + + outParameters[Impl.Name] = new List(); + foreach (Variable v in Impl.OutParams) + { + outParameters[Impl.Name].Add(v.Name); + if (doAnalysis) + { + SetUniform(Impl.Name, v.Name); + } + else + { + SetNonUniform(Impl.Name, v.Name); + } + } + + ProcedureChanged = true; + } + + if (doAnalysis) + { + while (ProcedureChanged) + { + ProcedureChanged = false; + + foreach (var Impl in impls) + { + hitNonuniformReturn = false; + Analyse(Impl, uniformityInfo[Impl.Name].Key); + } + } + } + + foreach (var Impl in impls) + { + if (!IsUniform (Impl.Name)) + { + List newIns = new List(); + newIns.Add("_P"); + foreach (string s in inParameters[Impl.Name]) + { + newIns.Add(s); + } + inParameters[Impl.Name] = newIns; + } + } + } + + private void Analyse(Implementation Impl, bool ControlFlowIsUniform) + { + if (unstructured) + { + if (!ControlFlowIsUniform) + { + nonUniformBlocks[Impl.Name] = new HashSet(Impl.Blocks); + + foreach (Variable v in Impl.LocVars) { + if (IsUniform(Impl.Name, v.Name)) { + SetNonUniform(Impl.Name, v.Name); + } + } + + foreach (Variable v in Impl.InParams) { + if (IsUniform(Impl.Name, v.Name)) { + SetNonUniform(Impl.Name, v.Name); + } + } + + foreach (Variable v in Impl.OutParams) { + if (IsUniform(Impl.Name, v.Name)) { + SetNonUniform(Impl.Name, v.Name); + } + } + + return; + } + + Graph blockGraph = prog.ProcessLoops(Impl); + var ctrlDep = blockGraph.ControlDependence(); + + // Compute transitive closure of control dependence info. + bool changed; + do + { + changed = false; + foreach (var depEntry in ctrlDep) + { + var newDepSet = new HashSet(depEntry.Value); + foreach (var dep in depEntry.Value) + { + if (ctrlDep.ContainsKey(dep)) + newDepSet.UnionWith(ctrlDep[dep]); + } + if (newDepSet.Count != depEntry.Value.Count) + { + depEntry.Value.UnionWith(newDepSet); + changed = true; + } + } + } while (changed); + + var nonUniformBlockSet = new HashSet(); + nonUniformBlocks[Impl.Name] = nonUniformBlockSet; + + do { + changed = false; + foreach (var block in Impl.Blocks) { + bool uniform = !nonUniformBlockSet.Contains(block); + bool newUniform = Analyse(Impl, block.Cmds, uniform); + if (uniform && !newUniform) { + changed = true; + nonUniformBlockSet.Add(block); + Block pred = blockGraph.Predecessors(block).Single(); + if (ctrlDep.ContainsKey(pred)) + nonUniformBlockSet.UnionWith(ctrlDep[pred]); + } + } + } while (changed); + } + else + { + Analyse(Impl, Impl.StructuredStmts, ControlFlowIsUniform); + } + } + + + private void Analyse(Implementation impl, StmtList stmtList, bool ControlFlowIsUniform) + { + ControlFlowIsUniform &= !hitNonuniformReturn; + foreach (BigBlock bb in stmtList.BigBlocks) + { + Analyse(impl, bb, ControlFlowIsUniform); + } + } + + private Implementation GetImplementation(string procedureName) + { + foreach (Declaration D in prog.TopLevelDeclarations) + { + if (D is Implementation && ((D as Implementation).Name == procedureName)) + { + return D as Implementation; + } + } + return null; + } + + private void Analyse(Implementation impl, BigBlock bb, bool ControlFlowIsUniform) + { + ControlFlowIsUniform &= !hitNonuniformReturn; + Analyse(impl, bb.simpleCmds, ControlFlowIsUniform); + + if (bb.ec is WhileCmd) + { + WhileCmd wc = bb.ec as WhileCmd; + loopStack.Add(wc); + Analyse(impl, wc.Body, ControlFlowIsUniform && IsUniform(impl.Name, wc.Guard) && + !nonUniformLoops[impl.Name].Contains(GetLoopId(wc))); + loopStack.RemoveAt(loopStack.Count - 1); + } + else if (bb.ec is IfCmd) + { + IfCmd ifCmd = bb.ec as IfCmd; + Analyse(impl, ifCmd.thn, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard)); + if (ifCmd.elseBlock != null) + { + Analyse(impl, ifCmd.elseBlock, ControlFlowIsUniform && IsUniform(impl.Name, ifCmd.Guard)); + } + Debug.Assert(ifCmd.elseIf == null); + } + else if (bb.ec is BreakCmd) + { + if (!ControlFlowIsUniform && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[loopStack.Count - 1]))) + { + SetNonUniform(impl.Name, loopStack[loopStack.Count - 1]); + } + } + + if (bb.tc is ReturnCmd && !ControlFlowIsUniform) + { + hitNonuniformReturn = true; + if (loopStack.Count > 0 && !nonUniformLoops[impl.Name].Contains(GetLoopId(loopStack[0]))) + { + SetNonUniform(impl.Name, loopStack[0]); + loopsWithNonuniformReturn[impl.Name].Add(GetLoopId(loopStack[0])); + } + } + + + } + + private bool Analyse(Implementation impl, CmdSeq cmdSeq, bool ControlFlowIsUniform) + { + foreach (Cmd c in cmdSeq) + { + if (c is AssignCmd) + { + AssignCmd assignCmd = c as AssignCmd; + foreach (var a in assignCmd.Lhss.Zip(assignCmd.Rhss)) + { + + if (a.Item1 is SimpleAssignLhs) + { + SimpleAssignLhs lhs = a.Item1 as SimpleAssignLhs; + Expr rhs = a.Item2; + if (IsUniform(impl.Name, lhs.AssignedVariable.Name) && + (!ControlFlowIsUniform || !IsUniform(impl.Name, rhs))) + { + SetNonUniform(impl.Name, lhs.AssignedVariable.Name); + } + + } + } + } + else if (c is HavocCmd) + { + HavocCmd havocCmd = c as HavocCmd; + foreach(IdentifierExpr ie in havocCmd.Vars) + { + if(IsUniform(impl.Name, ie.Decl.Name)) { + SetNonUniform(impl.Name, ie.Decl.Name); + } + } + } + else if (c is CallCmd) + { + CallCmd callCmd = c as CallCmd; + Implementation CalleeImplementation = GetImplementation(callCmd.callee); + + if (CalleeImplementation != null) + { + + if (!ControlFlowIsUniform) + { + if (IsUniform(callCmd.callee)) + { + SetNonUniform(callCmd.callee); + } + } + for (int i = 0; i < CalleeImplementation.InParams.Length; i++) + { + if (IsUniform(callCmd.callee, CalleeImplementation.InParams[i].Name) + && !IsUniform(impl.Name, callCmd.Ins[i])) + { + SetNonUniform(callCmd.callee, CalleeImplementation.InParams[i].Name); + } + } + + for (int i = 0; i < CalleeImplementation.OutParams.Length; i++) + { + if (IsUniform(impl.Name, callCmd.Outs[i].Name) + && !IsUniform(callCmd.callee, CalleeImplementation.OutParams[i].Name)) + { + SetNonUniform(impl.Name, callCmd.Outs[i].Name); + } + } + + } + } + else if (c is AssumeCmd) + { + var ac = (AssumeCmd)c; + if (ControlFlowIsUniform && QKeyValue.FindBoolAttribute(ac.Attributes, "partition") && + !IsUniform(impl.Name, ac.Expr)) + { + ControlFlowIsUniform = false; + } + } + } + + return ControlFlowIsUniform; + } + + private int GetLoopId(WhileCmd wc) + { + AssertCmd inv = wc.Invariants[0] as AssertCmd; + Debug.Assert(inv.Attributes.Key.Contains("loophead_")); + return Convert.ToInt32(inv.Attributes.Key.Substring("loophead_".Length)); + } + + private void SetNonUniform(string procedureName) + { + uniformityInfo[procedureName] = new KeyValuePair> + (false, uniformityInfo[procedureName].Value); + RecordProcedureChanged(); + } + + private void SetNonUniform(string procedureName, WhileCmd wc) + { + nonUniformLoops[procedureName].Add(GetLoopId(wc)); + RecordProcedureChanged(); + } + + public bool IsUniform(string procedureName) + { + if (!uniformityInfo.ContainsKey(procedureName)) + { + return false; + } + return uniformityInfo[procedureName].Key; + } + + public bool IsUniform(string procedureName, Block b) + { + if (!nonUniformBlocks.ContainsKey(procedureName)) + { + return false; + } + return !nonUniformBlocks[procedureName].Contains(b); + } + + class UniformExpressionAnalysisVisitor : StandardVisitor { + + private bool isUniform = true; + private Dictionary uniformityInfo; + + public UniformExpressionAnalysisVisitor(Dictionary uniformityInfo) { + this.uniformityInfo = uniformityInfo; + } + + public override Variable VisitVariable(Variable v) { + if (!uniformityInfo.ContainsKey(v.Name)) { + isUniform = isUniform && (v is Constant); + } else if (!uniformityInfo[v.Name]) { + isUniform = false; + } + + return v; + } + + internal bool IsUniform() { + return isUniform; + } + } + + public bool IsUniform(string procedureName, Expr expr) + { + UniformExpressionAnalysisVisitor visitor = new UniformExpressionAnalysisVisitor(uniformityInfo[procedureName].Value); + visitor.VisitExpr(expr); + return visitor.IsUniform(); + } + + public bool IsUniform(string procedureName, string v) + { + if (!uniformityInfo.ContainsKey(procedureName)) + { + return false; + } + + if (!uniformityInfo[procedureName].Value.ContainsKey(v)) + { + return false; + } + return uniformityInfo[procedureName].Value[v]; + } + + private void SetUniform(string procedureName, string v) + { + uniformityInfo[procedureName].Value[v] = true; + RecordProcedureChanged(); + } + + private void RecordProcedureChanged() + { + ProcedureChanged = true; + } + + private void SetNonUniform(string procedureName, string v) + { + uniformityInfo[procedureName].Value[v] = false; + RecordProcedureChanged(); + } + + public void dump() + { + foreach (string p in uniformityInfo.Keys) + { + Console.WriteLine("Procedure " + p + ": " + + (uniformityInfo[p].Key ? "uniform" : "nonuniform")); + foreach (string v in uniformityInfo[p].Value.Keys) + { + Console.WriteLine(" " + v + ": " + + (uniformityInfo[p].Value[v] ? "uniform" : "nonuniform")); + } + Console.Write("Ins ["); + for (int i = 0; i < inParameters[p].Count; i++) + { + Console.Write((i == 0 ? "" : ", ") + inParameters[p][i]); + } + Console.WriteLine("]"); + Console.Write("Outs ["); + for (int i = 0; i < outParameters[p].Count; i++) + { + Console.Write((i == 0 ? "" : ", ") + outParameters[p][i]); + } + Console.WriteLine("]"); + Console.Write("Non-uniform loops:"); + foreach (int l in nonUniformLoops[p]) + { + Console.Write(" " + l); + } + Console.WriteLine(); + Console.Write("Non-uniform blocks:"); + foreach (Block b in nonUniformBlocks[p]) + { + Console.Write(" " + b.Label); + } + Console.WriteLine(); + } + } + + + public string GetInParameter(string procName, int i) + { + return inParameters[procName][i]; + } + + public string GetOutParameter(string procName, int i) + { + return outParameters[procName][i]; + } + + + public bool knowsOf(string p) + { + return uniformityInfo.ContainsKey(p); + } + + public void AddNonUniform(string proc, string v) + { + if (uniformityInfo.ContainsKey(proc)) + { + Debug.Assert(!uniformityInfo[proc].Value.ContainsKey(v)); + uniformityInfo[proc].Value[v] = false; + } + } + + public void AddNonUniform(string proc, Block b) { + if (nonUniformBlocks.ContainsKey(proc)) { + Debug.Assert(!nonUniformBlocks[proc].Contains(b)); + nonUniformBlocks[proc].Add(b); + } + } + + public bool IsUniform(string proc, WhileCmd wc) + { + if (unstructured) + return false; + + return !nonUniformLoops[proc].Contains(GetLoopId(wc)); + } + + public bool HasNonuniformReturn(string proc, WhileCmd whileCmd) + { + return loopsWithNonuniformReturn[proc].Contains(GetLoopId(whileCmd)); + } + } + +} -- cgit v1.2.3