From 89c7d4c339f58dc9ec39b14b0b2a4120f2689322 Mon Sep 17 00:00:00 2001 From: allydonaldson Date: Tue, 30 Apr 2013 15:36:09 +0100 Subject: Staged Houdini --- Source/BoogieDriver/BoogieDriver.cs | 12 + Source/Core/Absy.cs | 65 +- Source/Core/CommandLineOptions.cs | 17 + Source/Core/Core.csproj | 1 + Source/Core/DeadVarElim.cs | 24 +- Source/Core/PureCollections.cs | 2 +- Source/Core/VariableDependenceAnalyser.cs | 872 ++++++++++++++++++++++++++ Source/Graph/Graph.cs | 20 + Source/Houdini/CandidateDependenceAnalyser.cs | 346 ++++++++++ Source/Houdini/Houdini.cs | 116 ++-- Source/Houdini/Houdini.csproj | 3 +- Source/Predication/UniformityAnalyser.cs | 179 ++---- 12 files changed, 1422 insertions(+), 235 deletions(-) create mode 100644 Source/Core/VariableDependenceAnalyser.cs create mode 100644 Source/Houdini/CandidateDependenceAnalyser.cs diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 9d1038f5..4531b9bb 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -195,11 +195,23 @@ namespace Microsoft.Boogie { PrintBplFile(CommandLineOptions.Clo.OwickiGriesDesugaredOutputFile, program, false, false); CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured; } + LinearSetTransform linearTransform = new LinearSetTransform(program); linearTransform.Transform(); EliminateDeadVariablesAndInline(program); + if (CommandLineOptions.Clo.StagedHoudini > 0) { + var candidateDependenceAnalyser = new CandidateDependenceAnalyser(program); + candidateDependenceAnalyser.Analyse(); + candidateDependenceAnalyser.ApplyStages(); + if (CommandLineOptions.Clo.Trace) { + candidateDependenceAnalyser.dump(); + } + PrintBplFile("staged.bpl", program, false, false); + Environment.Exit(0); + } + int errorCount, verified, inconclusives, timeOuts, outOfMemories; oc = InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories); switch (oc) { diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 616a0e21..c3a9a164 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -739,6 +739,36 @@ namespace Microsoft.Boogie { fullMap[procName][blockName] = block; } + public static Graph BuildCallGraph(Program program) { + Graph callGraph = new Graph(); + Dictionary> procToImpls = new Dictionary>(); + foreach (Declaration decl in program.TopLevelDeclarations) { + Procedure proc = decl as Procedure; + if (proc == null) continue; + procToImpls[proc] = new HashSet(); + } + foreach (Declaration decl in program.TopLevelDeclarations) { + Implementation impl = decl as Implementation; + if (impl == null || impl.SkipVerification) continue; + callGraph.AddSource(impl); + procToImpls[impl.Proc].Add(impl); + } + foreach (Declaration decl in program.TopLevelDeclarations) { + Implementation impl = decl as Implementation; + if (impl == null || impl.SkipVerification) continue; + foreach (Block b in impl.Blocks) { + foreach (Cmd c in b.Cmds) { + CallCmd cc = c as CallCmd; + if (cc == null) continue; + foreach (Implementation callee in procToImpls[cc.Proc]) { + callGraph.AddEdge(impl, callee); + } + } + } + } + return callGraph; + } + public static Graph/*!*/ GraphFromImpl(Implementation impl) { Contract.Requires(impl != null); Contract.Ensures(cce.NonNullElements(Contract.Result>().TopologicalSort())); @@ -896,16 +926,17 @@ namespace Microsoft.Boogie { private int invariantGenerationCounter = 0; - public Constant MakeExistentialBoolean() { + public Constant MakeExistentialBoolean(int StageId) { Constant ExistentialBooleanConstant = new Constant(Token.NoToken, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false); invariantGenerationCounter++; ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True }); + ExistentialBooleanConstant.AddAttribute("stage_id", new object[] { new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(StageId)) }); TopLevelDeclarations.Add(ExistentialBooleanConstant); return ExistentialBooleanConstant; } - public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null) { - Constant ExistentialBooleanConstant = MakeExistentialBoolean(); + public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null, int StageId = 0) { + Constant ExistentialBooleanConstant = MakeExistentialBoolean(StageId); IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant); PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e)); if (tag != null) @@ -2907,6 +2938,7 @@ namespace Microsoft.Boogie { this.scc = new StronglyConnectedComponents(this.Blocks, next, prev); scc.Compute(); + foreach (Block/*!*/ block in this.Blocks) { Contract.Assert(block != null); block.Predecessors = new BlockSeq(); @@ -2991,15 +3023,17 @@ namespace Microsoft.Boogie { reachableBlocks.Add(b); reachable.Add(b); if (b.TransferCmd is GotoCmd) { - foreach (Cmd/*!*/ s in b.Cmds) { - Contract.Assert(s != null); - if (s is PredicateCmd) { - LiteralExpr e = ((PredicateCmd)s).Expr as LiteralExpr; - if (e != null && e.IsFalse) { - // This statement sequence will never reach the end, because of this "assume false" or "assert false". - // Hence, it does not reach its successors. - b.TransferCmd = new ReturnCmd(b.TransferCmd.tok); - goto NEXT_BLOCK; + if (CommandLineOptions.Clo.PruneInfeasibleEdges) { + foreach (Cmd/*!*/ s in b.Cmds) { + Contract.Assert(s != null); + if (s is PredicateCmd) { + LiteralExpr e = ((PredicateCmd)s).Expr as LiteralExpr; + if (e != null && e.IsFalse) { + // This statement sequence will never reach the end, because of this "assume false" or "assert false". + // Hence, it does not reach its successors. + b.TransferCmd = new ReturnCmd(b.TransferCmd.tok); + goto NEXT_BLOCK; + } } } } @@ -3153,7 +3187,7 @@ namespace Microsoft.Boogie { } } - public sealed class VariableSeq : PureCollections.Sequence { + public sealed class VariableSeq : List { public VariableSeq(params Variable[]/*!*/ args) : base(args) { Contract.Requires(args != null); @@ -3192,6 +3226,11 @@ namespace Microsoft.Boogie { return res; } } + public int Length { + get { + return Count; + } + } } public sealed class TypeSeq : PureCollections.Sequence { diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 46d2c064..e94367ad 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -395,6 +395,7 @@ namespace Microsoft.Boogie { public bool ContractInfer = false; public bool ExplainHoudini = false; public bool HoudiniUseCrossDependencies = false; + public int StagedHoudini = 0; public string AbstractHoudini = null; public bool UseUnsatCoreForContractInfer = false; public bool PrintAssignment = false; @@ -490,6 +491,7 @@ namespace Microsoft.Boogie { public bool RemoveEmptyBlocks = true; public bool CoalesceBlocks = true; + public bool PruneInfeasibleEdges = true; [Rep] public ProverFactory TheProverFactory; @@ -861,6 +863,21 @@ namespace Microsoft.Boogie { return true; } + case "noPruneInfeasibleEdges": { + if (ps.ConfirmArgumentCount(0)) { + PruneInfeasibleEdges = false; + } + return true; + } + + case "stagedHoudini": { + int sh = 0; + if (ps.GetNumericArgument(ref sh, 3)) { + StagedHoudini = sh; + } + return true; + } + case "abstractHoudini": { if (ps.ConfirmArgumentCount(1)) diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index eb581edd..e6db6e9d 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -168,6 +168,7 @@ + diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index d51fcdb3..cb7b01a3 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -55,16 +55,16 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.Trace) { - Console.WriteLine(); - Console.WriteLine("Running modset analysis ..."); - int procCount = 0; - foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) - { - Contract.Assert(decl != null); - if (decl is Procedure) - procCount++; - } - Console.WriteLine("Number of procedures = {0}", procCount); +// Console.WriteLine(); +// Console.WriteLine("Running modset analysis ..."); +// int procCount = 0; +// foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) +// { +// Contract.Assert(decl != null); +// if (decl is Procedure) +// procCount++; +// } +// Console.WriteLine("Number of procedures = {0}", procCount);*/ } modSets = new Dictionary/*!*/>(); @@ -115,8 +115,8 @@ namespace Microsoft.Boogie { } } - if (CommandLineOptions.Clo.Trace) - { + if (false /*CommandLineOptions.Clo.Trace*/) { + Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count); foreach (Procedure/*!*/ x in modSets.Keys) { diff --git a/Source/Core/PureCollections.cs b/Source/Core/PureCollections.cs index 15a6c629..f984ecd4 100644 --- a/Source/Core/PureCollections.cs +++ b/Source/Core/PureCollections.cs @@ -569,7 +569,7 @@ namespace PureCollections { object[] n = new object[card]; int ct = 0; Contract.Assert(this.elems != null); - for (int i = 0; i < elems.Length; i++) + for (int i = 0; i < card; i++) n[ct++] = elems[i]; return n; } diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs new file mode 100644 index 00000000..be9fdcb4 --- /dev/null +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -0,0 +1,872 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics; +using Microsoft.Boogie; +using Microsoft.Boogie.GraphUtil; + + +namespace Microsoft.Boogie { + + public interface IVariableDependenceAnalyser { + + void Analyse(); + VariableDescriptor MakeDescriptor(string proc, Variable v); + HashSet DependsOn(VariableDescriptor v); + void dump(); + + } + + public abstract class VariableDescriptor : IComparable { + internal readonly string Name; + internal VariableDescriptor(string Name) { + this.Name = Name; + } + + public override string ToString() { + return Name; + } + + public override bool Equals(object that) { + + if (object.ReferenceEquals(this, that)) { + return true; + } + + VariableDescriptor thatDescriptor = that as VariableDescriptor; + + if (thatDescriptor == null) { + return false; + } + + return base.Equals(thatDescriptor) && + this.Name.Equals(thatDescriptor.Name); + } + + public override int GetHashCode() { + return Name.GetHashCode(); + } + + public int CompareTo(object that) { + return this.ToString().CompareTo(that.ToString()); + } + + } + + class LocalDescriptor : VariableDescriptor { + internal readonly string Proc; + internal LocalDescriptor(string Proc, string Name) + : base(Name) { + this.Proc = Proc; + } + + public override string ToString() { + return Proc + "." + base.ToString(); + } + + public override bool Equals(object that) { + + if (object.ReferenceEquals(this, that)) { + return true; + } + + LocalDescriptor thatDescriptor = that as LocalDescriptor; + + if (thatDescriptor == null) { + return false; + } + + return base.Equals(thatDescriptor) && + this.Proc.Equals(thatDescriptor.Proc); + + } + + public override int GetHashCode() { + return (33 * base.GetHashCode()) + + this.Proc.GetHashCode(); + } + + } + + class GlobalDescriptor : VariableDescriptor { + internal GlobalDescriptor(string name) : base(name) { } + + public override bool Equals(object that) { + + if (object.ReferenceEquals(this, that)) { + return true; + } + + GlobalDescriptor thatDescriptor = that as GlobalDescriptor; + + if (thatDescriptor == null) { + return false; + } + + return base.Equals(thatDescriptor); + + } + + public override int GetHashCode() { + return base.GetHashCode(); + } + + } + + /// + /// Given a Boogie program, computes a graph that over-approximates dependences + /// between program variables. + /// + public class VariableDependenceAnalyser : IVariableDependenceAnalyser { + + private Graph dependsOnNonTransitive; + private Program prog; + private Dictionary> BlockToControllingBlocks; + private Dictionary> ControllingBlockToVariables; + + public VariableDependenceAnalyser(Program prog) { + this.prog = prog; + dependsOnNonTransitive = new Graph(); + } + + + private void Initialise() { + foreach (var descriptor in + prog.TopLevelDeclarations.OfType().Where(Item => !(Item is Constant)). + Select(Variable => Variable.Name). + Select(Name => new GlobalDescriptor(Name))) { + dependsOnNonTransitive.AddEdge(descriptor, descriptor); + } + + foreach (var Proc in NonInlinedProcedures()) { + + List parameters = new List(); + parameters.AddRange(Proc.InParams); + parameters.AddRange(Proc.OutParams); + foreach (var descriptor in + parameters.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Proc.Name, Name))) { + dependsOnNonTransitive.AddEdge(descriptor, descriptor); + } + } + + foreach (var Impl in NonInlinedImplementations()) { + + List locals = new List(); + locals.AddRange(Impl.LocVars); + foreach (var descriptor in + locals.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Impl.Name, Name))) { + dependsOnNonTransitive.AddEdge(descriptor, descriptor); + } + } + } + + private IEnumerable NonInlinedProcedures() { + return prog.TopLevelDeclarations.OfType(). + Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1); + } + + private IEnumerable NonInlinedImplementations() { + return prog.TopLevelDeclarations.OfType(). + Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1); + } + + public void Analyse() { + + /* The algorithm is as follows: + * + * 1. Build global control dependence graph. First build control dependence graph for each procedure, + * and union them. Then examine each procedure. If block B is control-dependent on block C, make + * every block that can be indirectly reached via a call from B control-dependent on C. + * + * 2. Take transitive closure of global control dependence graph. + * + * 3. For every block B such that some other block is control-dependent on B, determine those variables + * which B tests. If B tests v, and C is control-depdendent on B, we say that v "controls" the + * statements appearing in C. + * + * 4. Consider each statement to work out variable dependences. v may depend on u if: + * - there is a statement v := e where u appears in e + * - there is a statement call ... := foo(..., e, ...) where v is formal in parameter of foo + * corresponding to e and u appears in e + * - there is a statement call ..., v, ... := foo(...) where u is formal out parameter of foo + * correspondnig to v + * - there is a statement v := ... controlled by u + * - there is a statement call ... := foo(...) controlled by u where v is a formal in parameter + * of foo + * - there is a statement call ..., v, ... := foo(...) controlled by u + * + * 5. Finialise variable dependence graph by taking its transitive closure. + * + */ + + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Variable dependence analysis: Initialising"); + } + + Initialise(); + + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Variable dependence analysis: Computing control dependence info"); + } + + BlockToControllingBlocks = ComputeGlobalControlDependences(); + + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Variable dependence analysis: Computing control dependence variables"); + } + + ControllingBlockToVariables = ComputeControllingVariables(BlockToControllingBlocks); + foreach (var Impl in NonInlinedImplementations()) { + + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Variable dependence analysis: Analysing " + Impl.Name); + } + + Analyse(Impl); + } + } + + private void Analyse(Implementation Impl) { + string proc = Impl.Name; + foreach (Block b in Impl.Blocks) { + Analyse(proc, b); + } + } + + private void Analyse(string proc, Block b) { + foreach (Cmd cmd in b.Cmds) { + AssignCmd assign = cmd as AssignCmd; + if (assign != null) { + HandleAssign(proc, b, assign); + } + CallCmd call = cmd as CallCmd; + if (call != null) { + HandleCall(proc, b, call); + } + } + } + + private void HandleCall(string proc, Block b, CallCmd call) { + foreach (var formalActualPair in call.Proc.InParams.Zip(call.Ins)) { + var formalIn = MakeDescriptor(call.callee, formalActualPair.Item1); + AddDependences(formalIn, GetReferencedVariables(formalActualPair.Item2, proc)); + AddControlDependences(b, formalIn); + } + + foreach (var formalActualPair in call.Proc.OutParams.Zip(call.Outs)) { + var actualOut = MakeDescriptor(proc, formalActualPair.Item2.Decl); + AddDependences(actualOut, GetReferencedVariables(new IdentifierExpr(Token.NoToken, formalActualPair.Item1), call.callee)); + AddControlDependences(b, actualOut); + } + + } + + private void HandleAssign(string proc, Block b, AssignCmd assign) { + foreach (var assignPair in assign.Lhss.Zip(assign.Rhss)) { + VariableDescriptor assignedVariable = MakeDescriptor(proc, assignPair.Item1.DeepAssignedVariable); + AddDependences(assignedVariable, GetReferencedVariables(assignPair.Item1, proc)); + AddDependences(assignedVariable, GetReferencedVariables(assignPair.Item2, proc)); + AddControlDependences(b, assignedVariable); + } + } + + private void AddControlDependences(Block b, VariableDescriptor v) { + if (!BlockToControllingBlocks.ContainsKey(b)) { + return; + } + foreach (var controller in BlockToControllingBlocks[b]) { + AddDependences(v, ControllingBlockToVariables[controller]); + } + } + + private IEnumerable GetReferencedVariables(Absy node, string proc) { + var VarCollector = new VariableCollector(); + VarCollector.Visit(node); + return VarCollector.usedVars.Where(Item => !(Item is Constant)).Select(Item => MakeDescriptor(proc, Item)); + } + + void AddDependences(VariableDescriptor v, IEnumerable vs) { + foreach (var n in vs) { + dependsOnNonTransitive.AddEdge(v, n); + } + } + + private Dictionary> ComputeControllingVariables(Dictionary> GlobalCtrlDep) { + Dictionary> result = new Dictionary>(); + foreach (var Impl in NonInlinedImplementations()) { + foreach (var b in Impl.Blocks) { + result[b] = GetControlDependencyVariables(Impl.Name, b); + } + } + return result; + } + + private HashSet GetControlDependencyVariables(string proc, Block b) { + + // This method works under the assumption that assume statements + // relevant to control flow between basic blocks have the "partition" attribute + + HashSet result = new HashSet(); + var gotoCmd = b.TransferCmd as GotoCmd; + if (gotoCmd != null && gotoCmd.labelTargets.Length >= 2) { + foreach (Block succ in gotoCmd.labelTargets) { + foreach (Cmd c in succ.Cmds) { + AssumeCmd a = c as AssumeCmd; + if (a != null && QKeyValue.FindBoolAttribute(a.Attributes, "partition")) { + var VarCollector = new VariableCollector(); + VarCollector.VisitExpr(a.Expr); + result.UnionWith(VarCollector.usedVars.Where(Item => !(Item is Constant)).Select( + Item => MakeDescriptor(proc, Item))); + } + else { + break; + } + } + } + } + return result; + } + + private Dictionary> ComputeGlobalControlDependences() { + + Dictionary> GlobalCtrlDep = new Dictionary>(); + Dictionary>> LocalCtrlDeps = new Dictionary>>(); + + // Work out and union together local control dependences + foreach (var Impl in prog.TopLevelDeclarations.OfType()) { + Graph blockGraph = prog.ProcessLoops(Impl); + LocalCtrlDeps[Impl] = blockGraph.ControlDependence(); + foreach (var KeyValue in LocalCtrlDeps[Impl]) { + GlobalCtrlDep.Add(KeyValue.Key, KeyValue.Value); + } + } + + Graph callGraph = Program.BuildCallGraph(prog); + + // Add inter-procedural control dependence nodes based on calls + foreach (var Impl in prog.TopLevelDeclarations.OfType()) { + foreach (var b in Impl.Blocks) { + foreach (var cmd in b.Cmds.OfType()) { + var DirectCallee = GetImplementation(cmd.callee); + if (DirectCallee != null) { + HashSet IndirectCallees = ComputeIndirectCallees(callGraph, DirectCallee); + foreach (var control in GetControllingBlocks(b, LocalCtrlDeps[Impl])) { + foreach (var c in IndirectCallees.Select(Item => Item.Blocks).SelectMany(Item => Item)) { + GlobalCtrlDep[control].Add(c); + } + } + } + } + } + } + + // Compute transitive closure + GlobalCtrlDep.TransitiveClosure(); + + // Finally reverse the dependences + + Dictionary> result = new Dictionary>(); + + foreach (var KeyValue in GlobalCtrlDep) { + foreach (var v in KeyValue.Value) { + if (!result.ContainsKey(v)) { + result[v] = new HashSet(); + } + result[v].Add(KeyValue.Key); + } + } + + return result; + } + + private HashSet ComputeIndirectCallees(Graph callGraph, Implementation DirectCallee) { + return ComputeIndirectCallees(callGraph, DirectCallee, new HashSet()); + } + + private HashSet ComputeIndirectCallees(Graph callGraph, Implementation DirectCallee, HashSet seen) { + if (seen.Contains(DirectCallee)) { + return new HashSet(); + } + HashSet result = new HashSet(); + result.Add(DirectCallee); + seen.Add(DirectCallee); + foreach (var succ in callGraph.Successors(DirectCallee)) { + result.UnionWith(ComputeIndirectCallees(callGraph, succ, seen)); + } + return result; + } + + private HashSet GetControllingBlocks(Block b, Dictionary> ctrlDep) { + HashSet result = new HashSet(); + foreach (var KeyValue in ctrlDep) { + if (KeyValue.Value.Contains(b)) { + result.Add(KeyValue.Key); + } + } + return result; + } + + private Implementation GetImplementation(string proc) { + foreach (var Impl in prog.TopLevelDeclarations.OfType()) { + if (Impl.Name.Equals(proc)) { + return Impl; + } + } + return null; + } + + public VariableDescriptor MakeDescriptor(string proc, Variable v) { + + // Check whether there is an (Impl, v) match + var MatchingLocals = dependsOnNonTransitive.Nodes.Where(Item => Item is LocalDescriptor).Select( + Item => (LocalDescriptor)Item).Where(Item => Item.Proc.Equals(proc) && + Item.Name.Equals(v.Name)); + if (MatchingLocals.Count() > 0) { + Debug.Assert(MatchingLocals.Count() == 1); + return MatchingLocals.ToArray()[0]; + } + + // It must be a global with same name as v + return dependsOnNonTransitive.Nodes.Where(Item => Item is GlobalDescriptor && + Item.Name.Equals(v.Name)).ToArray()[0]; + } + + private Dictionary, HashSet> DependsOnCache = new Dictionary, HashSet>(); + + private Graph> DependsOnSCCsDAG; + private Dictionary> VariableDescriptorToSCC; + + public HashSet DependsOn(VariableDescriptor v) { + if (DependsOnSCCsDAG == null) { + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Variable dependence: computing SCCs"); + } + Adjacency next = new Adjacency(dependsOnNonTransitive.Successors); + Adjacency prev = new Adjacency(dependsOnNonTransitive.Predecessors); + StronglyConnectedComponents DependsOnSCCs = new StronglyConnectedComponents( + dependsOnNonTransitive.Nodes, next, prev); + DependsOnSCCs.Compute(); + + VariableDescriptorToSCC = new Dictionary>(); + foreach (var scc in DependsOnSCCs) { + foreach (var s in scc) { + VariableDescriptorToSCC[s] = scc; + } + } + + DependsOnSCCsDAG = new Graph>(); + foreach (var edge in dependsOnNonTransitive.Edges) { + if (VariableDescriptorToSCC[edge.Item1] != VariableDescriptorToSCC[edge.Item2]) { + DependsOnSCCsDAG.AddEdge(VariableDescriptorToSCC[edge.Item1], VariableDescriptorToSCC[edge.Item2]); + } + } + + SCC dummy = new SCC(); + foreach (var n in dependsOnNonTransitive.Nodes) { + DependsOnSCCsDAG.AddEdge(VariableDescriptorToSCC[n], dummy); + } + + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Variable dependence: SCCs computed!"); + } + } + return DependsOn(VariableDescriptorToSCC[v]); + } + + public HashSet DependsOn(SCC vSCC) { + + if (!DependsOnCache.ContainsKey(vSCC)) { + HashSet result = new HashSet(); + if (vSCC.Count() > 0) { + result.UnionWith(vSCC); + foreach (var wSCC in DependsOnSCCsDAG.Successors(vSCC)) { + result.UnionWith(DependsOn(wSCC)); + } + } + DependsOnCache[vSCC] = result; + } + return DependsOnCache[vSCC]; + } + + public void dump() { + + Console.WriteLine("Variable dependence information"); + Console.WriteLine("==============================="); + + Console.WriteLine("Global variables"); + Console.WriteLine("================"); + + foreach (var GlobalEntry in dependsOnNonTransitive.Nodes.Where(Item => Item is GlobalDescriptor)) { + dump(GlobalEntry); + } + + foreach (var proc in Procedures()) { + Console.WriteLine("Variables of " + proc); + Console.WriteLine("====================="); + foreach (var LocalEntry in dependsOnNonTransitive.Nodes.Where(Item => Item is LocalDescriptor + && ((LocalDescriptor)Item).Proc.Equals(proc))) { + dump(LocalEntry); + } + } + } + + private void dump(VariableDescriptor vd) { + Console.Write(vd + " <- {"); + bool first = true; + + var SortedDependents = DependsOn(vd).ToList(); + SortedDependents.Sort(); + foreach (var Descriptor in SortedDependents) { + Console.Write((first ? "" : ",") + "\n " + Descriptor); + if (first) { + first = false; + } + } + Debug.Assert(!first); + Console.WriteLine("\n}\n"); + } + + private HashSet Procedures() { + return new HashSet(dependsOnNonTransitive.Nodes.Where(Item => + Item is LocalDescriptor).Select(Item => ((LocalDescriptor)Item).Proc)); + } + + } + + + /// + /// Given a Boogie program, computes a graph that over-approximates dependences + /// between program variables. + /// + public class OldVariableDependenceAnalyser : IVariableDependenceAnalyser { + + private Program prog; + + public Dictionary> dependsOn; + + private Dictionary> callControlDependences; + + private bool ProcedureChanged; + + public OldVariableDependenceAnalyser(Program prog) { + this.prog = prog; + dependsOn = new Dictionary>(); + callControlDependences = new Dictionary>(); + } + + public void Analyse() { + + Initialise(); + + ProcedureChanged = true; + while (ProcedureChanged) { + ProcedureChanged = false; + + foreach (var Impl in NonInlinedImplementations()) { + Analyse(Impl); + } + + } + + } + + private Dictionary temp = new Dictionary(); + + private void Analyse(Implementation Impl) { + + if (!temp.ContainsKey(Impl.Name)) { + temp[Impl.Name] = 0; + } + + temp[Impl.Name]++; + + var ctrlDep = GetControlDependenceTransitiveClosure(Impl); + + var orderedBlocks = GetOrderedBlocks(Impl); + + bool changed; + do { + changed = false; + foreach (Block block in orderedBlocks) { + Analyse(Impl, block, ctrlDep, ref changed); + } + } while (changed); + + } + + private void Analyse(Implementation Impl, Block block, + Dictionary> ctrlDep, ref bool changed) { + + // First, work out the set of all variables that are involved in tests on which + // this block is control-dependent + HashSet ctrlDepVars = GetControlDependencyVariables(block, Impl.Name, ctrlDep); + // Take incoming control dependences for the procedure + ctrlDepVars.UnionWith(callControlDependences[Impl.Name]); + + var ControlInflucencingVariables = GetDependentVariables(ctrlDepVars); + + foreach (var c in block.Cmds) { + + var assign = c as AssignCmd; + if (assign != null) { + + foreach (var assignPair in assign.Lhss.Zip(assign.Rhss)) { + VariableDescriptor assignedVariable = MakeDescriptor(Impl.Name, assignPair.Item1.DeepAssignedVariable); + AddDependences(assignedVariable, GetDependentVariables(GetReferencedVariables(assignPair.Item1, Impl.Name)), ref changed); + AddDependences(assignedVariable, GetDependentVariables(GetReferencedVariables(assignPair.Item2, Impl.Name)), ref changed); + AddDependences(assignedVariable, ControlInflucencingVariables, ref changed); + } + } + + var call = c as CallCmd; + if (call != null) { + AddCallControlDependences(call.callee, ctrlDepVars); + + foreach(var formalActualPair in call.Proc.InParams.Zip(call.Ins)) { + bool unused = false; // When we find that the in parameters of the called procedure have been changed, we do not need to necessarily continue processing this procedure + AddDependences(MakeDescriptor(call.callee, formalActualPair.Item1), + GetDependentVariables(GetReferencedVariables(formalActualPair.Item2, Impl.Name)), ref unused); + AddDependences(MakeDescriptor(call.callee, formalActualPair.Item1), + ControlInflucencingVariables, ref unused); + } + + foreach (var formalActualPair in call.Proc.OutParams.Zip(call.Outs)) { + AddDependences(MakeDescriptor(Impl.Name, formalActualPair.Item2.Decl), + GetDependentVariables(GetReferencedVariables(new IdentifierExpr(Token.NoToken, formalActualPair.Item1), call.callee)), ref changed); + AddDependences(MakeDescriptor(Impl.Name, formalActualPair.Item2.Decl), + ControlInflucencingVariables, ref changed); + } + + } + + } + + } + + private IEnumerable GetDependentVariables(IEnumerable vars) { + HashSet result = new HashSet(); + foreach (var v in vars) { + result.UnionWith(dependsOn[v]); + } + return result; + } + + private IEnumerable GetReferencedVariables(Absy node, string proc) { + var VarCollector = new VariableCollector(); + VarCollector.Visit(node); + IEnumerable result = VarCollector.usedVars.Where(Item => !(Item is Constant)).Select(Item => MakeDescriptor(proc, Item)); + return result; + } + + public VariableDescriptor MakeDescriptor(string proc, Variable v) { + + // Check whether there is an (Impl, v) match + var MatchingLocals = dependsOn.Keys.Where(Item => Item is LocalDescriptor).Select( + Item => (LocalDescriptor)Item).Where(Item => Item.Proc.Equals(proc) && + Item.Name.Equals(v.Name)); + if(MatchingLocals.Count() > 0) { + Debug.Assert(MatchingLocals.Count() == 1); + return MatchingLocals.ToArray()[0]; + } + + // It must be a global with same name as v + return dependsOn.Keys.Where(Item => Item is GlobalDescriptor && + Item.Name.Equals(v.Name)).ToArray()[0]; + } + + private Dictionary> ControlDependencyVariablesCache = new Dictionary>(); + + private HashSet GetControlDependencyVariables(Block b, string proc, Dictionary> ctrlDep) { + + if (!ControlDependencyVariablesCache.ContainsKey(b)) { + HashSet ctrlDepVars = new HashSet(); + foreach (var k in ctrlDep.Keys) { + if (ctrlDep[k].Contains(b)) { + foreach (Variable v in GetControlDependencyVariables(k)) { + ctrlDepVars.Add(MakeDescriptor(proc, v)); + } + } + } + ControlDependencyVariablesCache[b] = ctrlDepVars; + } + + return ControlDependencyVariablesCache[b]; + } + + private static HashSet GetControlDependencyVariables(Block b) { + + // This method works under the assumption that assume statements + // relevant to control flow between basic blocks have the "partition" attribute + + HashSet result = new HashSet(); + if (b.TransferCmd is GotoCmd) { + foreach (Block succ in ((GotoCmd)b.TransferCmd).labelTargets) { + foreach (Cmd c in succ.Cmds) { + AssumeCmd a = c as AssumeCmd; + if (a != null && QKeyValue.FindBoolAttribute(a.Attributes, "partition")) { + var VarCollector = new VariableCollector(); + VarCollector.VisitExpr(a.Expr); + result.UnionWith(VarCollector.usedVars.Where(Item => !(Item is Constant))); + } + else { + break; + } + } + } + } + return result; + } + + private void Initialise() { + foreach (var descriptor in + prog.TopLevelDeclarations.OfType().Where(Item => !(Item is Constant)). + Select(Variable => Variable.Name). + Select(Name => new GlobalDescriptor(Name))) { + dependsOn.Add(descriptor, new HashSet { descriptor }); + } + + foreach (var Proc in NonInlinedProcedures()) { + + callControlDependences[Proc.Name] = new HashSet(); + + List parameters = new List(); + parameters.AddRange(Proc.InParams); + parameters.AddRange(Proc.OutParams); + foreach (var descriptor in + parameters.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Proc.Name, Name))) { + dependsOn.Add(descriptor, new HashSet { descriptor }); + } + } + + foreach (var Impl in NonInlinedImplementations()) { + + List locals = new List(); + locals.AddRange(Impl.LocVars); + foreach (var descriptor in + locals.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Impl.Name, Name))) { + dependsOn.Add(descriptor, new HashSet { descriptor }); + } + } + } + + private IEnumerable NonInlinedProcedures() { + return prog.TopLevelDeclarations.OfType(). + Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1); + } + + private IEnumerable NonInlinedImplementations() { + return prog.TopLevelDeclarations.OfType(). + Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1); + } + + + + public void dump() { + + Console.WriteLine("Variable dependence information"); + Console.WriteLine("==============================="); + + Console.WriteLine("Global variables"); + Console.WriteLine("================"); + + foreach (var GlobalEntry in dependsOn.Where(Item => Item.Key is GlobalDescriptor)) { + dump(GlobalEntry); + } + + foreach (var proc in Procedures()) { + Console.WriteLine("Variables of " + proc); + Console.WriteLine("====================="); + foreach (var LocalEntry in dependsOn.Where(Item => Item.Key is LocalDescriptor + && ((LocalDescriptor)Item.Key).Proc.Equals(proc))) { + dump(LocalEntry); + } + } + } + + private static void dump(KeyValuePair> Entry) + { + Console.Write(Entry.Key + " <- {"); + bool first = true; + + var SortedDependents = Entry.Value.ToList(); + SortedDependents.Sort(); + + foreach(var Descriptor in SortedDependents) { + Console.Write((first ? "" : ",") + "\n " + Descriptor); + if (first) { + first = false; + } + } + Console.WriteLine("\n}\n"); + } + + private HashSet Procedures() { + return new HashSet(dependsOn.Where(Item => + Item.Key is LocalDescriptor).Select(Item => ((LocalDescriptor)Item.Key).Proc)); + } + + void AddDependences(VariableDescriptor v, IEnumerable vs, ref bool Changed) { + foreach (var n in vs) { + if (!dependsOn[v].Contains(n)) { + dependsOn[v].Add(n); + ProcedureChanged = true; + Changed = true; + } + } + } + + private void AddCallControlDependences(string Proc, HashSet ctrlDepVars) { + foreach (var n in ctrlDepVars) { + if (!callControlDependences[Proc].Contains(n)) { + callControlDependences[Proc].Add(n); + ProcedureChanged = true; + } + } + } + + + private Dictionary>> ControlDependenceCache = new Dictionary>>(); + + private Dictionary> GetControlDependenceTransitiveClosure(Implementation Impl) { + if (!ControlDependenceCache.ContainsKey(Impl.Name)) { + Graph blockGraph = prog.ProcessLoops(Impl); + Dictionary> ctrlDep = blockGraph.ControlDependence(); + ctrlDep.TransitiveClosure(); + ControlDependenceCache[Impl.Name] = ctrlDep; + } + return ControlDependenceCache[Impl.Name]; + } + + private Dictionary> OrderedBlocksCache = new Dictionary>(); + + private List GetOrderedBlocks(Implementation Impl) { + if (!OrderedBlocksCache.ContainsKey(Impl.Name)) { + List orderedBlocks = PostOrder(Impl.Blocks[0], new HashSet()); + Debug.Assert(orderedBlocks.Count() == Impl.Blocks.Count()); + orderedBlocks.Reverse(); + OrderedBlocksCache[Impl.Name] = orderedBlocks; + } + return OrderedBlocksCache[Impl.Name]; + } + + private List PostOrder(Block b, HashSet seen) { + seen.Add(b); + List result = new List(); + if(b.TransferCmd is GotoCmd) { + foreach (Block c in ((GotoCmd)b.TransferCmd).labelTargets) { + if (!seen.Contains(c)) { + result.AddRange(PostOrder(c, seen)); + } + } + } + result.Add(b); + return result; + } + + public HashSet DependsOn(VariableDescriptor vd) { + return dependsOn[vd]; + } + + } +} diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index ac406bb6..4d81e741 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -974,6 +974,7 @@ namespace Microsoft.Boogie.GraphUtil { { Graph dual = g.Dual(new Node()); DomRelation pdom = dual.DominatorMap; + var result = new Dictionary>(); var S = g.Edges.Where(e => !pdom.DominatedBy(e.Item1, e.Item2)); @@ -1001,9 +1002,28 @@ namespace Microsoft.Boogie.GraphUtil { result[edge.Item1] = new HashSet(deps); } } + return result; } + public static void TransitiveClosure(this Dictionary> graph) where Node : class { + bool changed; + do { + changed = false; + foreach (var entry in graph) { + var newSuccessors = new HashSet(entry.Value); + foreach (var successor in entry.Value) { + if (graph.ContainsKey(successor)) + newSuccessors.UnionWith(graph[successor]); + } + if (newSuccessors.Count != entry.Value.Count) { + entry.Value.UnionWith(newSuccessors); + changed = true; + } + } + } while (changed); + } + } public delegate System.Collections.IEnumerable/**//*!*/ Adjacency(T/*!*/ node); diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs new file mode 100644 index 00000000..a7083497 --- /dev/null +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -0,0 +1,346 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using Microsoft.Boogie.GraphUtil; +using Microsoft.Basetypes; +using System.Diagnostics; + +namespace Microsoft.Boogie { + + public class CandidateDependenceAnalyser { + + private const int COARSE_STAGES = 1; + private const int FINE_STAGES = 2; + + private Program prog; + private IVariableDependenceAnalyser varDepAnalyser; + private IEnumerable candidates; + private Dictionary> candidateDependsOn; + private Dictionary> variableDirectlyReferredToByCandidates; + private Graph CandidateDependences; + private StronglyConnectedComponents SCCs; + private Graph> StagesDAG; + + public CandidateDependenceAnalyser(Program prog) { + this.prog = prog; + this.varDepAnalyser = new VariableDependenceAnalyser(prog); + varDepAnalyser.Analyse(); + } + + public void Analyse() { + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Candidate dependence analysis: Getting candidates"); + } + + 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(); + } + + // 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); + } + } + + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Candidate dependence analysis: Building dependence graph"); + } + + CandidateDependences = new Graph(); + + 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) { + Console.WriteLine("Candidate dependence analysis: Computing SCCs"); + } + + Adjacency next = new Adjacency(CandidateDependences.Successors); + Adjacency prev = new Adjacency(CandidateDependences.Predecessors); + SCCs = new StronglyConnectedComponents( + CandidateDependences.Nodes, next, prev); + SCCs.Compute(); + + 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) { + rep[s] = scc; + } + } + + StagesDAG = new Graph>(); + + 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) { + StagesDAG.AddEdge(scc, dummy); + } + + } + + private bool FindInDAG(Graph> DAG, SCC toFind, SCC start) { + if (toFind == start) { + return true; + } + foreach (var n in DAG.Successors(start)) { + if (FindInDAG(DAG, toFind, n)) { + return true; + } + } + return false; + } + + private void CheckExpr(string proc, Expr e) { + string candidate; + Houdini.Houdini.MatchCandidate(e, candidates, out candidate); + if (candidate != null) { + VariableCollector vc = new VariableCollector(); + vc.VisitExpr(e); + + foreach (var v in vc.usedVars.Where(Item => !(Item is Constant))) { + VariableDescriptor vd = + varDepAnalyser.MakeDescriptor(proc, v); + if (!variableDirectlyReferredToByCandidates.ContainsKey(vd)) { + variableDirectlyReferredToByCandidates[vd] = new HashSet(); + } + variableDirectlyReferredToByCandidates[vd].Add(candidate); + + foreach (var w in varDepAnalyser.DependsOn(vd)) { + candidateDependsOn[candidate].Add(w); + } + } + } + } + + private bool IsStageDependence(SCC Src, SCC Dst) { + foreach (var c in Src) { + foreach (var d in CandidateDependences.Successors(c)) { + if (Dst.Contains(d)) { + return true; + } + } + } + return false; + } + + + public void dump() { + + varDepAnalyser.dump(); + + /*Console.WriteLine("Candidates and the variables they depend on"); + Console.WriteLine("==========================================="); + foreach (var entry in candidateDependsOn) { + Console.WriteLine(entry.Key + " <- "); + foreach (var vd in entry.Value) { + Console.WriteLine(" " + vd + ", "); + } + } + + Console.WriteLine(""); + + Console.WriteLine("Variables and the candidates that directly refer to them"); + Console.WriteLine("========================================================"); + foreach (var entry in variableDirectlyReferredToByCandidates) { + Console.WriteLine(entry.Key + " <- "); + foreach (var candidate in entry.Value) { + Console.WriteLine(" " + candidate + ", "); + } + } + + Console.WriteLine("");*/ + + /* + Console.WriteLine("Candidate dependence graph"); + Console.WriteLine("=========================="); + foreach (var c in CandidateDependences.Nodes) { + Console.WriteLine(c + " <- "); + foreach (var d in CandidateDependences.Successors(c)) { + Console.WriteLine(" " + d); + } + }*/ + + Console.WriteLine(""); + + Console.WriteLine("Strongly connected components"); + Console.WriteLine("============================="); + + List> Components = StagesDAG.TopologicalSort().ToList(); + + for (int i = 0; i < Components.Count(); i++) { + Console.Write(i + ": "); + DumpSCC(Components[i]); + Console.WriteLine("\n"); + } + + Console.WriteLine("Stages DAG"); + Console.WriteLine("=========="); + for (int i = 0; i < Components.Count(); i++) { + Console.Write(i + " -> { "); + bool first = true; + foreach (var d in StagesDAG.Successors(Components[i])) { + if (first) { + first = false; + } + else { + Console.Write(", "); + } + Console.Write(Components.IndexOf(d)); + } + Console.WriteLine(" }"); + } + + } + + private static void DumpSCC(SCC component) { + var sortedComponent = component.ToList(); + sortedComponent.Sort(); + Console.Write("{ "); + bool first = true; + foreach (var s in sortedComponent) { + if (first) { + first = false; + } + else { + Console.Write(", "); + } + Console.Write(s); + } + Console.Write(" }"); + } + + private IEnumerable GetCandidates() { + return prog.TopLevelDeclarations.OfType().Where(Item => + QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name); + } + + + public void ApplyStages() { + + IEnumerable candidates = prog.TopLevelDeclarations.OfType(). + Where(Item => QKeyValue.FindBoolAttribute(Item.Attributes, "existential")); + + if (candidates.Count() == 0) { + return; + } + + if (StagesDAG.Nodes.Count() == 0) { + return; + } + + + Debug.Assert(CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES || + CommandLineOptions.Clo.StagedHoudini == FINE_STAGES); + + if (CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES) { + SCC start = null; + foreach (var n in StagesDAG.Nodes) { + if (StagesDAG.Successors(n).Count() == 0) { + start = n; + break; + } + } + System.Diagnostics.Debug.Assert(start != null); + + HashSet> done = new HashSet>(); + done.Add(start); + + bool finished = false; + int stageId = 0; + while (!finished) { + finished = true; + HashSet> stage = new HashSet>(); + foreach (var n in StagesDAG.Nodes) { + if (!done.Contains(n)) { + finished = false; + bool ready = true; + foreach (var m in StagesDAG.Successors(n)) { + if (!done.Contains(m)) { + ready = false; + break; + } + } + if (ready) { + stage.Add(n); + done.Add(n); + } + } + } + + foreach (var scc in stage) { + foreach (var candidate in candidates) { + if (scc.Contains(candidate.Name)) { + candidate.Attributes = new QKeyValue(Token.NoToken, "stage_id", new List() { + new LiteralExpr(Token.NoToken, BigNum.FromInt(stageId)) + }, candidate.Attributes); + } + } + } + + stageId++; + } + + } + else { + List> components = StagesDAG.TopologicalSort().ToList(); + components.Reverse(); + + System.Diagnostics.Debug.Assert(components[0].Count() == 0); + for (int i = 1; i < components.Count(); i++) { + foreach (var c in candidates) { + if (components[i].Contains(c.Name)) { + c.Attributes = new QKeyValue(Token.NoToken, "stage_id", new List() { + new LiteralExpr(Token.NoToken, BigNum.FromInt(i - 1)) + }, c.Attributes); + } + } + + } + + } + + + + } + } + +} diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 6d740fdb..a39f4fdb 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -328,7 +328,7 @@ namespace Microsoft.Boogie.Houdini { if (CommandLineOptions.Clo.Trace) Console.WriteLine("Building call graph..."); - this.callGraph = BuildCallGraph(); + this.callGraph = Program.BuildCallGraph(program); if (CommandLineOptions.Clo.Trace) Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count); @@ -493,36 +493,6 @@ namespace Microsoft.Boogie.Houdini { // contant -> set of implementations that have an assume command with that constant public Dictionary> assumedInImpl { get; private set; } } - - private Graph BuildCallGraph() { - Graph callGraph = new Graph(); - Dictionary> procToImpls = new Dictionary>(); - foreach (Declaration decl in program.TopLevelDeclarations) { - Procedure proc = decl as Procedure; - if (proc == null) continue; - procToImpls[proc] = new HashSet(); - } - foreach (Declaration decl in program.TopLevelDeclarations) { - Implementation impl = decl as Implementation; - if (impl == null || impl.SkipVerification) continue; - callGraph.AddSource(impl); - procToImpls[impl.Proc].Add(impl); - } - foreach (Declaration decl in program.TopLevelDeclarations) { - Implementation impl = decl as Implementation; - if (impl == null || impl.SkipVerification) continue; - foreach (Block b in impl.Blocks) { - foreach (Cmd c in b.Cmds) { - CallCmd cc = c as CallCmd; - if (cc == null) continue; - foreach (Implementation callee in procToImpls[cc.Proc]) { - callGraph.AddEdge(impl, callee); - } - } - } - } - return callGraph; - } private WorkQueue BuildWorkList(Program program) { // adding implementations to the workqueue from the bottom of the call graph upwards @@ -1059,9 +1029,10 @@ namespace Microsoft.Boogie.Houdini { /// /// Transforms given program based on Houdini assignment. If a constant is assigned "true", - /// any preconditions or postconditions guarded by the constant are replaced with - /// regular conditions, and any assertions guarded by the constant are replaced with - /// assumptions. If a constant is assigned "false", any preconditions or postconditions + /// any preconditions or postconditions guarded by the constant are made free, and any assertions + /// guarded by the constant are replaced with assumptions. + /// + /// If a constant is assigned "false", any preconditions or postconditions /// guarded by the constant are replaced with "true", and assertions guarded by the constant /// are removed. /// @@ -1094,46 +1065,51 @@ namespace Microsoft.Boogie.Houdini { block.Cmds = newCmds; } - // Treat requires and ensures - new ApplyAssignmentVisitor(this, prog).VisitProgram(prog); - - // Remove the existential constants - prog.TopLevelDeclarations.RemoveAll(item => (item is Variable) && - (houdiniConstants.Select(c => c.Name).Contains((item as Variable).Name))); - } - - class ApplyAssignmentVisitor : StandardVisitor { - - private Houdini houdini; - private Program prog; - - internal ApplyAssignmentVisitor(Houdini houdini, Program prog) { - this.houdini = houdini; - this.prog = prog; - } - - public override Requires VisitRequires(Requires requires) { - requires.Condition = ApplyAssignment(requires.Condition); - return requires; - } - - public override Ensures VisitEnsures(Ensures ensures) { - ensures.Condition = ApplyAssignment(ensures.Condition); - return ensures; - } + foreach (var proc in prog.TopLevelDeclarations.OfType()) { + RequiresSeq newRequires = new RequiresSeq(); + foreach (Requires r in proc.Requires) { + string c; + if (MatchCandidate(r.Condition, out c)) { + var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0]; + if (currentHoudiniState.Assignment[cVar]) { + Variable cVarProg = prog.TopLevelDeclarations.OfType().Where(item => item.Name.Equals(c)).ToList()[0]; + Hashtable subst = new Hashtable(); + subst[cVarProg] = Expr.True; + newRequires.Add(new Requires(Token.NoToken, true, + Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), r.Condition), + r.Comment, r.Attributes)); + } + } + else { + newRequires.Add(r); + } + } + proc.Requires = newRequires; - private Expr ApplyAssignment(Expr e) { - string c; - if (houdini.MatchCandidate(e, out c)) { - var cVar = houdini.currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0]; - Hashtable cToTrue = new Hashtable(); - Variable cVarProg = prog.TopLevelDeclarations.OfType().Where(item => item.Name.Equals(c)).ToList()[0]; - cToTrue[cVarProg] = houdini.currentHoudiniState.Assignment[cVar] ? Expr.True : Expr.False; - return Substituter.Apply(Substituter.SubstitutionFromHashtable(cToTrue), e); + EnsuresSeq newEnsures = new EnsuresSeq(); + foreach (Ensures e in proc.Ensures) { + string c; + if (MatchCandidate(e.Condition, out c)) { + var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0]; + if (currentHoudiniState.Assignment[cVar]) { + Variable cVarProg = prog.TopLevelDeclarations.OfType().Where(item => item.Name.Equals(c)).ToList()[0]; + Hashtable subst = new Hashtable(); + subst[cVarProg] = Expr.True; + newEnsures.Add(new Ensures(Token.NoToken, true, + Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), e.Condition), + e.Comment, e.Attributes)); + } + } + else { + newEnsures.Add(e); + } } - return e; + proc.Ensures = newEnsures; } + // Remove the existential constants + prog.TopLevelDeclarations.RemoveAll(item => (item is Variable) && + (houdiniConstants.Select(c => c.Name).Contains((item as Variable).Name))); } } diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj index 2d2b0373..06d68dba 100644 --- a/Source/Houdini/Houdini.csproj +++ b/Source/Houdini/Houdini.csproj @@ -1,4 +1,4 @@ - + Debug @@ -80,6 +80,7 @@ + diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs index 6365d974..2e0f4074 100644 --- a/Source/Predication/UniformityAnalyser.cs +++ b/Source/Predication/UniformityAnalyser.cs @@ -13,7 +13,7 @@ namespace Microsoft.Boogie { private Program prog; - private bool doAnalysis, unstructured; + private bool doAnalysis; private ISet entryPoints; @@ -33,10 +33,6 @@ namespace Microsoft.Boogie 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 @@ -72,11 +68,10 @@ namespace Microsoft.Boogie } } - public UniformityAnalyser(Program prog, bool doAnalysis, bool unstructured, ISet entryPoints, IEnumerable nonUniformVars) + public UniformityAnalyser(Program prog, bool doAnalysis, ISet entryPoints, IEnumerable nonUniformVars) { this.prog = prog; this.doAnalysis = doAnalysis; - this.unstructured = unstructured; this.entryPoints = entryPoints; this.nonUniformVars = nonUniformVars; uniformityInfo = new Dictionary>>(); @@ -85,7 +80,6 @@ namespace Microsoft.Boogie loopsWithNonuniformReturn = new Dictionary>(); inParameters = new Dictionary>(); outParameters = new Dictionary>(); - loopStack = new List(); } public void Analyse() @@ -195,7 +189,6 @@ namespace Microsoft.Boogie foreach (var Impl in impls) { - hitNonuniformReturn = false; Analyse(Impl, uniformityInfo[Impl.Name].Key); } } @@ -218,89 +211,55 @@ namespace Microsoft.Boogie private void Analyse(Implementation Impl, bool ControlFlowIsUniform) { - if (unstructured) + if (!ControlFlowIsUniform) { - 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); - } - } + nonUniformBlocks[Impl.Name] = new HashSet(Impl.Blocks); - foreach (Variable v in Impl.InParams) { - if (IsUniform(Impl.Name, v.Name)) { - SetNonUniform(Impl.Name, v.Name); - } + foreach (Variable v in Impl.LocVars) { + 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); - } + foreach (Variable v in Impl.InParams) { + 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]); - } + foreach (Variable v in Impl.OutParams) { + if (IsUniform(Impl.Name, v.Name)) { + SetNonUniform(Impl.Name, v.Name); } - } while (changed); - } - else - { - Analyse(Impl, Impl.StructuredStmts, ControlFlowIsUniform); + } + + return; } - } - - private void Analyse(Implementation impl, StmtList stmtList, bool ControlFlowIsUniform) - { - ControlFlowIsUniform &= !hitNonuniformReturn; - foreach (BigBlock bb in stmtList.BigBlocks) - { - Analyse(impl, bb, ControlFlowIsUniform); - } + Graph blockGraph = prog.ProcessLoops(Impl); + var ctrlDep = blockGraph.ControlDependence(); + + // Compute transitive closure of control dependence info. + ctrlDep.TransitiveClosure(); + + var nonUniformBlockSet = new HashSet(); + nonUniformBlocks[Impl.Name] = nonUniformBlockSet; + + bool changed; + 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); } private Procedure GetProcedure(string procedureName) @@ -316,50 +275,6 @@ namespace Microsoft.Boogie 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) @@ -612,18 +527,6 @@ namespace Microsoft.Boogie } } - 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