From d823a93f514525f4cd27f0f8ce2f352d3b4d3608 Mon Sep 17 00:00:00 2001 From: allydonaldson Date: Wed, 22 May 2013 14:55:32 +0100 Subject: Fixed bug in staged Houdini. --- Source/Houdini/CandidateDependenceAnalyser.cs | 320 ++++++++++++++++++++++---- 1 file changed, 270 insertions(+), 50 deletions(-) diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index 959eff1e..0a38a674 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -35,53 +35,20 @@ namespace Microsoft.Boogie { candidates = GetCandidates(); - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Candidate dependence analysis: Working out what candidates depend on"); - } - candidateDependsOn = new Dictionary>(); - variableDirectlyReferredToByCandidates = new Dictionary>(); - foreach (var c in candidates) { - candidateDependsOn[c] = new HashSet(); - } + DetermineCandidateVariableDependences(); - // Candidate loop invariants - foreach(var impl in prog.TopLevelDeclarations.OfType()) { - foreach(var b in impl.Blocks) { - foreach (Cmd c in b.Cmds) { - var p = c as PredicateCmd; - if (p != null) { - CheckExpr(impl.Name, p.Expr); - } - } - } - } + //ConstructCandidateReachabilityGraph(); - foreach (var proc in prog.TopLevelDeclarations.OfType()) { - foreach (Requires r in proc.Requires) { - CheckExpr(proc.Name, r.Condition); - } - foreach (Ensures e in proc.Ensures) { - CheckExpr(proc.Name, e.Condition); - } - } - - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Candidate dependence analysis: Building dependence graph"); - } + ConstructCandidateDependenceGraph(); - CandidateDependences = new Graph(); + ConstructStagesDAG(); - foreach (var c in candidates) { - foreach (var vd in candidateDependsOn[c]) { - if (variableDirectlyReferredToByCandidates.ContainsKey(vd)) { - foreach (var d in variableDirectlyReferredToByCandidates[vd]) { - CandidateDependences.AddEdge(c, d); - } - } - } - } + } - if (CommandLineOptions.Clo.Trace) { + private void ConstructStagesDAG() + { + if (CommandLineOptions.Clo.Trace) + { Console.WriteLine("Candidate dependence analysis: Computing SCCs"); } @@ -91,30 +58,271 @@ namespace Microsoft.Boogie { CandidateDependences.Nodes, next, prev); SCCs.Compute(); - if (CommandLineOptions.Clo.Trace) { + if (CommandLineOptions.Clo.Trace) + { Console.WriteLine("Candidate dependence analysis: Building stages DAG"); } Dictionary> rep = new Dictionary>(); - foreach (var scc in SCCs) { - foreach (var s in scc) { + foreach (var scc in SCCs) + { + foreach (var s in scc) + { rep[s] = scc; } } StagesDAG = new Graph>(); - foreach (var edge in CandidateDependences.Edges) { - if (rep[edge.Item1] != rep[edge.Item2]) { + foreach (var edge in CandidateDependences.Edges) + { + if (rep[edge.Item1] != rep[edge.Item2]) + { StagesDAG.AddEdge(rep[edge.Item1], rep[edge.Item2]); } } SCC dummy = new SCC(); - foreach (var scc in SCCs) { + foreach (var scc in SCCs) + { StagesDAG.AddEdge(scc, dummy); } + } + + private void ConstructCandidateDependenceGraph() + { + if (CommandLineOptions.Clo.Trace) + { + Console.WriteLine("Candidate dependence analysis: Building dependence graph"); + } + + CandidateDependences = new Graph(); + foreach (var c in candidates) + { + CandidateDependences.AddEdge(c, c); + foreach (var vd in candidateDependsOn[c]) + { + if (variableDirectlyReferredToByCandidates.ContainsKey(vd)) + { + foreach (var d in variableDirectlyReferredToByCandidates[vd]) + { + if (MayReach(c, d)) + { + CandidateDependences.AddEdge(c, d); + } + } + } + } + } + } + + private void ConstructCandidateReachabilityGraph() + { + Dictionary> procedureCFGs = new Dictionary>(); + Dictionary> candidateToUse = new Dictionary>(); + + #region Prepare implementations + foreach (var impl in prog.TopLevelDeclarations.OfType()) { + procedureCFGs[impl.Name] = PrepareImplementationForCandidateReachability(impl); + } + #endregion + + #region Prepare any procedures that do not have implementations + foreach (var proc in prog.TopLevelDeclarations.OfType()) { + if(!procedureCFGs.ContainsKey(proc.Name)) { + procedureCFGs[proc.Name] = PrepareProcedureForCandidateReachability(proc); + } + } + #endregion + + #region Transform prepared CFGs so that every call is in its own basic block + foreach(var proc in procedureCFGs.Keys) { + List newCFG = new List(); + Dictionary oldToNew = new Dictionary(); + + foreach(var bb in procedureCFGs[proc]) { + List> partition = new List>(); + List current = new List(); + partition.Add(current); + foreach(Cmd cmd in bb.Cmds) { + if(cmd is CallCmd && current.Count > 0) { + current = new List(); + partition.Add(current); + } + current.Add(cmd); + } + + if(partition.Count > 1) { + Block last = null; + int i = 0; + foreach(var cmdList in partition) { + Block newBB = new Block(bb.tok, bb.Label + "_" + i, new CmdSeq(cmdList.ToArray()), null); + newCFG.Add(newBB); + if(last == null) { + oldToNew[bb] = newBB; + } else { + oldToNew[newBB] = newBB; + last.TransferCmd = new GotoCmd(last.tok, new BlockSeq { newBB }); + } + last = newBB; + i++; + } + Debug.Assert(last != null); + Debug.Assert(last.TransferCmd == null); + last.TransferCmd = bb.TransferCmd; + } else { + newCFG.Add(bb); + oldToNew[bb] = bb; + } + + } + + ApplyPatchupMap(newCFG, oldToNew); + procedureCFGs[proc] = newCFG; + + } + #endregion + + #region Replace calls with inter-procedural edges + foreach(var bb in procedureCFGs.Values.SelectMany(Item => Item)) { + if(bb.Cmds.Length == 1 && bb.Cmds[0] is CallCmd) { + Debug.Assert(bb.TransferCmd is GotoCmd); + string proc = (bb.Cmds[0] as CallCmd).callee; + + Block returnBB = procedureCFGs[proc].Last(); + if(returnBB.TransferCmd is ReturnCmd) { + returnBB.TransferCmd = bb.TransferCmd; + } else { + Debug.Assert(returnBB.TransferCmd is GotoCmd); + GotoCmd gotoCmd = returnBB.TransferCmd as GotoCmd; + gotoCmd.labelTargets.AddRange(((GotoCmd)bb.TransferCmd).labelTargets); + } + + Block entryBB = procedureCFGs[proc].First(); + bb.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq { entryBB }); + } + } + #endregion + + throw new NotImplementedException(); + + } + private static List PrepareProcedureForCandidateReachability(Procedure proc) + { + Block ensuresBlock = new Block(proc.tok, "postconditions", + EnsuresToAssertSequence(proc.Ensures), + new ReturnCmd(Token.NoToken)); + Block requiresBlock = new Block(proc.tok, "preconditions", + RequiresToAssertSequence(proc.Requires), + new GotoCmd(Token.NoToken, new BlockSeq { ensuresBlock })); + return new List { requiresBlock, ensuresBlock }; + } + + private static List PrepareImplementationForCandidateReachability(Implementation impl) + { + // Clone the BBs and keep patchup map + List newBBs = new List(); + Dictionary oldToNew = new Dictionary(); + foreach (var bb in impl.Blocks) + { + Block newBB = new Block(bb.tok, bb.Label, bb.Cmds, bb.TransferCmd); + oldToNew[bb] = newBB; + newBBs.Add(newBB); + } + ApplyPatchupMap(newBBs, oldToNew); + Block newEntry = new Block(Token.NoToken, "preconditions", + RequiresToAssertSequence(impl.Proc.Requires), + new GotoCmd(Token.NoToken, new BlockSeq { newBBs[0] })); + + Block newExit = new Block(Token.NoToken, "postconditions", + EnsuresToAssertSequence(impl.Proc.Ensures), + new ReturnCmd(Token.NoToken)); + + foreach (var newBB in newBBs) + { + if (newBB.TransferCmd is ReturnCmd || + (newBB.TransferCmd is GotoCmd && ((GotoCmd)newBB.TransferCmd).labelTargets.Length == 0)) + { + newBB.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq { newExit }); + } + } + + newBBs.Insert(0, newEntry); + newBBs.Add(newExit); + return newBBs; + } + + private static void ApplyPatchupMap(List newBBs, Dictionary oldToNew) + { + foreach (var newBB in newBBs) + { + GotoCmd gotoCmd = newBB.TransferCmd as GotoCmd; + if (gotoCmd != null) + { + gotoCmd.labelTargets = new BlockSeq(((Block[])gotoCmd.labelTargets.ToArray()). + Select(Item => oldToNew[Item]).ToArray()); + } + } + } + + private static CmdSeq RequiresToAssertSequence(RequiresSeq Requires) + { + return new CmdSeq(((Requires[])Requires.ToArray()).Select( + Item => new AssertCmd(Item.tok, Item.Condition)).ToArray()); + } + + private static CmdSeq EnsuresToAssertSequence(EnsuresSeq Ensures) + { + return new CmdSeq(((Ensures[])Ensures.ToArray()).Select( + Item => new AssertCmd(Item.tok, Item.Condition)).ToArray()); + } + + private bool MayReach(string c, string d) + { + return true; + } + + private void DetermineCandidateVariableDependences() + { + if (CommandLineOptions.Clo.Trace) + { + Console.WriteLine("Candidate dependence analysis: Working out what candidates depend on"); + } + candidateDependsOn = new Dictionary>(); + variableDirectlyReferredToByCandidates = new Dictionary>(); + foreach (var c in candidates) + { + candidateDependsOn[c] = new HashSet(); + } + + // Candidate loop invariants + foreach (var impl in prog.TopLevelDeclarations.OfType()) + { + foreach (var b in impl.Blocks) + { + foreach (Cmd c in b.Cmds) + { + var p = c as PredicateCmd; + if (p != null) + { + CheckExpr(impl.Name, p.Expr); + } + } + } + } + + foreach (var proc in prog.TopLevelDeclarations.OfType()) + { + foreach (Requires r in proc.Requires) + { + CheckExpr(proc.Name, r.Condition); + } + foreach (Ensures e in proc.Ensures) + { + CheckExpr(proc.Name, e.Condition); + } + } } private bool FindInDAG(Graph> DAG, SCC toFind, SCC start) { @@ -267,6 +475,10 @@ namespace Microsoft.Boogie { Dictionary candidateToStage = (CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES) ? ComputeCoarseStages() : ComputeFineStages(); + + foreach(var c in candidates) { + Debug.Assert(candidateToStage.ContainsKey(c)); + } #endregion #region Generate boolean variables to control stages @@ -344,16 +556,18 @@ namespace Microsoft.Boogie { foreach(Ensures e in p.Ensures) { string c; if (Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) { + int stage = candidateToStage[c]; + Constant activeBoolean = stageToActiveBoolean[stage]; newEnsures.Add(new Ensures(e.tok, false, Houdini.Houdini.AddConditionToCandidate(e.Condition, - new IdentifierExpr(Token.NoToken, stageToActiveBoolean[candidateToStage[c]]), c), + new IdentifierExpr(Token.NoToken, activeBoolean), c), e.Comment, e.Attributes)); newEnsures.Add(new Ensures(e.tok, true, Houdini.Houdini.AddConditionToCandidate(e.Condition, new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[candidateToStage[c]]), c), e.Comment, e.Attributes)); } else { - newRequires.Add(e); + newEnsures.Add(e); } } p.Ensures = newEnsures; @@ -366,6 +580,7 @@ namespace Microsoft.Boogie { private Dictionary ComputeFineStages() { + var result = new Dictionary(); List> components = StagesDAG.TopologicalSort().ToList(); components.Reverse(); @@ -379,6 +594,11 @@ namespace Microsoft.Boogie { } } + + foreach(var c in candidates) { + Debug.Assert(result.ContainsKey(c)); + } + return result; } -- cgit v1.2.3