From 89c7d4c339f58dc9ec39b14b0b2a4120f2689322 Mon Sep 17 00:00:00 2001 From: allydonaldson Date: Tue, 30 Apr 2013 15:36:09 +0100 Subject: Staged Houdini --- 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 ++++++++++++++++++++++++++++++ 6 files changed, 955 insertions(+), 26 deletions(-) create mode 100644 Source/Core/VariableDependenceAnalyser.cs (limited to 'Source/Core') 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]; + } + + } +} -- cgit v1.2.3