From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Core/VariableDependenceAnalyser.cs | 1292 ++++++++++++++--------------- 1 file changed, 646 insertions(+), 646 deletions(-) (limited to 'Source/Core/VariableDependenceAnalyser.cs') diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index ab12a47e..30e1dbf3 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -1,646 +1,646 @@ -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(); - void ShowDependencyChain(VariableDescriptor source, VariableDescriptor target); - bool VariableRelevantToAnalysis(Variable v, string proc); - bool Ignoring(Variable v, string proc); - - } - - 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 this.Name.Equals(thatDescriptor.Name); - } - - public override int GetHashCode() { - return Name.GetHashCode(); - } - - public int CompareTo(object that) { - return this.ToString().CompareTo(that.ToString()); - } - - } - - public class LocalDescriptor : VariableDescriptor { - internal readonly string Proc; - public 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(); - } - - } - - public class GlobalDescriptor : VariableDescriptor { - public 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.Variables.Where(Item => VariableRelevantToAnalysis(Item, null)). - Select(Variable => Variable.Name). - Select(Name => new GlobalDescriptor(Name))) { - dependsOnNonTransitive.AddEdge(descriptor, descriptor); - } - - foreach (var Proc in prog.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 prog.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 List ComputeDependencyChain(VariableDescriptor source, VariableDescriptor target, HashSet visited) { - if(source.Equals(target)) { - return new List { target }; - } - - visited.Add(source); - - foreach(var w in dependsOnNonTransitive.Successors(source)) { - if(visited.Contains(w)) { - continue; - } - var result = ComputeDependencyChain(w, target, visited); - if(result != null) { - result.Insert(0, source); - return result; - } - } - - return null; - - } - - public void ShowDependencyChain(VariableDescriptor source, VariableDescriptor target) { - var chain = ComputeDependencyChain(source, target, new HashSet()); - if(chain == null) { - Console.WriteLine("No chain between " + source + " and " + target); - } else { - bool first = true; - foreach(var v in chain) { - if(first) { - first = false; - } else { - Console.Write(" -> "); - } - Console.Write(v); - } - } - Console.WriteLine(); Console.WriteLine(); - } - - 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 prog.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), - "referenced in in-param in call to " + proc, call.tok); - AddControlDependences(b, formalIn, " in param assigned under control dependence in call to " + proc, call.tok); - } - - 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), - "receiving variable for out-param in call to " + proc, call.tok); - AddControlDependences(b, actualOut, " receiving variable assigned under control dependence in call to " + proc, call.tok); - } - - } - - private void HandleAssign(string proc, Block b, AssignCmd assign) { - foreach (var assignPair in assign.Lhss.Zip(assign.Rhss).Where - (Item => VariableRelevantToAnalysis(Item.Item1.DeepAssignedVariable, proc))) { - VariableDescriptor assignedVariable = MakeDescriptor(proc, assignPair.Item1.DeepAssignedVariable); - AddDependences(assignedVariable, GetReferencedVariables(assignPair.Item1, proc), - "LHS of assignment", assign.tok); - AddDependences(assignedVariable, GetReferencedVariables(assignPair.Item2, proc), - "RHS of assignment", assign.tok); - AddControlDependences(b, assignedVariable, "Variable assigned under control dependence", assign.tok); - } - } - - private void AddControlDependences(Block b, VariableDescriptor v, string reason, IToken tok) { - if (!BlockToControllingBlocks.ContainsKey(b)) { - return; - } - foreach (var controller in BlockToControllingBlocks[b]) { - AddDependences(v, ControllingBlockToVariables[controller], reason + " controlling block at (" + controller.tok.line + ":" + controller.tok.col + ")", tok); - } - } - - private IEnumerable GetReferencedVariables(Absy node, string proc) { - var VarCollector = new VariableCollector(); - VarCollector.Visit(node); - return VarCollector.usedVars.Where(Item => VariableRelevantToAnalysis(Item, proc)). - Select(Item => MakeDescriptor(proc, Item)); - } - - void AddDependences(VariableDescriptor v, IEnumerable vs, string reason, IToken tok) { - foreach (var n in vs) { - if(CommandLineOptions.Clo.DebugStagedHoudini) { - Console.WriteLine("Adding dependence " + v + " -> " + n + ", reason: " + reason + "(" + tok.line + ":" + tok.col + ")"); - } - dependsOnNonTransitive.AddEdge(v, n); - } - } - - private Dictionary> ComputeControllingVariables(Dictionary> GlobalCtrlDep) { - Dictionary> result = new Dictionary>(); - foreach (var Impl in prog.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.Count >= 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 => VariableRelevantToAnalysis(Item, proc)). - Select(Item => MakeDescriptor(proc, Item))); - } - else { - break; - } - } - } - } - return result; - } - - private HashSet IgnoredVariables = null; - - public bool Ignoring(Variable v, string proc) { - - if (IgnoredVariables == null) { - MakeIgnoreList(); - } - - if(proc != null && IgnoredVariables.Contains(new LocalDescriptor(proc, v.Name))) { - return true; - } - - if(IgnoredVariables.Contains(new GlobalDescriptor(v.Name))) { - return true; - } - - return false; - - } - - public bool VariableRelevantToAnalysis(Variable v, string proc) { - return !(v is Constant || Ignoring(v, proc)); - } - - private void MakeIgnoreList() - { - IgnoredVariables = new HashSet(); - if(CommandLineOptions.Clo.VariableDependenceIgnore == null) { - return; - } - try { - var file = System.IO.File.OpenText(CommandLineOptions.Clo.VariableDependenceIgnore); - while(!file.EndOfStream) { - string line = file.ReadLine(); - string[] tokens = line.Split(' '); - if(tokens.Count() == 0) { - continue; - } - if(tokens.Count() > 2) { - Console.Error.WriteLine("Ignoring malformed line of ignored variables file: " + line); - continue; - } - if(tokens.Count() == 1) { - IgnoredVariables.Add(new GlobalDescriptor(tokens[0])); - continue; - } - Debug.Assert(tokens.Count() == 2); - IgnoredVariables.Add(new LocalDescriptor(tokens[0], tokens[1])); - } - } catch(System.IO.IOException e) { - Console.Error.WriteLine("Error reading from ignored variables file " + CommandLineOptions.Clo.VariableDependenceIgnore + ": " + e); - } - } - - private Dictionary> ComputeGlobalControlDependences() { - - Dictionary> GlobalCtrlDep = new Dictionary>(); - Dictionary>> LocalCtrlDeps = new Dictionary>>(); - - // Work out and union together local control dependences - foreach (var Impl in prog.NonInlinedImplementations()) { - 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.NonInlinedImplementations()) { - 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.Implementations) { - 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)); - } - - } - - public static class Helper { - - public static IEnumerable NonInlinedProcedures(this Program prog) { - return prog.Procedures. - Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1); - } - - public static IEnumerable NonInlinedImplementations(this Program prog) { - return prog.Implementations. - Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1); - } - - } - -} +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(); + void ShowDependencyChain(VariableDescriptor source, VariableDescriptor target); + bool VariableRelevantToAnalysis(Variable v, string proc); + bool Ignoring(Variable v, string proc); + + } + + 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 this.Name.Equals(thatDescriptor.Name); + } + + public override int GetHashCode() { + return Name.GetHashCode(); + } + + public int CompareTo(object that) { + return this.ToString().CompareTo(that.ToString()); + } + + } + + public class LocalDescriptor : VariableDescriptor { + internal readonly string Proc; + public 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(); + } + + } + + public class GlobalDescriptor : VariableDescriptor { + public 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.Variables.Where(Item => VariableRelevantToAnalysis(Item, null)). + Select(Variable => Variable.Name). + Select(Name => new GlobalDescriptor(Name))) { + dependsOnNonTransitive.AddEdge(descriptor, descriptor); + } + + foreach (var Proc in prog.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 prog.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 List ComputeDependencyChain(VariableDescriptor source, VariableDescriptor target, HashSet visited) { + if(source.Equals(target)) { + return new List { target }; + } + + visited.Add(source); + + foreach(var w in dependsOnNonTransitive.Successors(source)) { + if(visited.Contains(w)) { + continue; + } + var result = ComputeDependencyChain(w, target, visited); + if(result != null) { + result.Insert(0, source); + return result; + } + } + + return null; + + } + + public void ShowDependencyChain(VariableDescriptor source, VariableDescriptor target) { + var chain = ComputeDependencyChain(source, target, new HashSet()); + if(chain == null) { + Console.WriteLine("No chain between " + source + " and " + target); + } else { + bool first = true; + foreach(var v in chain) { + if(first) { + first = false; + } else { + Console.Write(" -> "); + } + Console.Write(v); + } + } + Console.WriteLine(); Console.WriteLine(); + } + + 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 prog.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), + "referenced in in-param in call to " + proc, call.tok); + AddControlDependences(b, formalIn, " in param assigned under control dependence in call to " + proc, call.tok); + } + + 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), + "receiving variable for out-param in call to " + proc, call.tok); + AddControlDependences(b, actualOut, " receiving variable assigned under control dependence in call to " + proc, call.tok); + } + + } + + private void HandleAssign(string proc, Block b, AssignCmd assign) { + foreach (var assignPair in assign.Lhss.Zip(assign.Rhss).Where + (Item => VariableRelevantToAnalysis(Item.Item1.DeepAssignedVariable, proc))) { + VariableDescriptor assignedVariable = MakeDescriptor(proc, assignPair.Item1.DeepAssignedVariable); + AddDependences(assignedVariable, GetReferencedVariables(assignPair.Item1, proc), + "LHS of assignment", assign.tok); + AddDependences(assignedVariable, GetReferencedVariables(assignPair.Item2, proc), + "RHS of assignment", assign.tok); + AddControlDependences(b, assignedVariable, "Variable assigned under control dependence", assign.tok); + } + } + + private void AddControlDependences(Block b, VariableDescriptor v, string reason, IToken tok) { + if (!BlockToControllingBlocks.ContainsKey(b)) { + return; + } + foreach (var controller in BlockToControllingBlocks[b]) { + AddDependences(v, ControllingBlockToVariables[controller], reason + " controlling block at (" + controller.tok.line + ":" + controller.tok.col + ")", tok); + } + } + + private IEnumerable GetReferencedVariables(Absy node, string proc) { + var VarCollector = new VariableCollector(); + VarCollector.Visit(node); + return VarCollector.usedVars.Where(Item => VariableRelevantToAnalysis(Item, proc)). + Select(Item => MakeDescriptor(proc, Item)); + } + + void AddDependences(VariableDescriptor v, IEnumerable vs, string reason, IToken tok) { + foreach (var n in vs) { + if(CommandLineOptions.Clo.DebugStagedHoudini) { + Console.WriteLine("Adding dependence " + v + " -> " + n + ", reason: " + reason + "(" + tok.line + ":" + tok.col + ")"); + } + dependsOnNonTransitive.AddEdge(v, n); + } + } + + private Dictionary> ComputeControllingVariables(Dictionary> GlobalCtrlDep) { + Dictionary> result = new Dictionary>(); + foreach (var Impl in prog.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.Count >= 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 => VariableRelevantToAnalysis(Item, proc)). + Select(Item => MakeDescriptor(proc, Item))); + } + else { + break; + } + } + } + } + return result; + } + + private HashSet IgnoredVariables = null; + + public bool Ignoring(Variable v, string proc) { + + if (IgnoredVariables == null) { + MakeIgnoreList(); + } + + if(proc != null && IgnoredVariables.Contains(new LocalDescriptor(proc, v.Name))) { + return true; + } + + if(IgnoredVariables.Contains(new GlobalDescriptor(v.Name))) { + return true; + } + + return false; + + } + + public bool VariableRelevantToAnalysis(Variable v, string proc) { + return !(v is Constant || Ignoring(v, proc)); + } + + private void MakeIgnoreList() + { + IgnoredVariables = new HashSet(); + if(CommandLineOptions.Clo.VariableDependenceIgnore == null) { + return; + } + try { + var file = System.IO.File.OpenText(CommandLineOptions.Clo.VariableDependenceIgnore); + while(!file.EndOfStream) { + string line = file.ReadLine(); + string[] tokens = line.Split(' '); + if(tokens.Count() == 0) { + continue; + } + if(tokens.Count() > 2) { + Console.Error.WriteLine("Ignoring malformed line of ignored variables file: " + line); + continue; + } + if(tokens.Count() == 1) { + IgnoredVariables.Add(new GlobalDescriptor(tokens[0])); + continue; + } + Debug.Assert(tokens.Count() == 2); + IgnoredVariables.Add(new LocalDescriptor(tokens[0], tokens[1])); + } + } catch(System.IO.IOException e) { + Console.Error.WriteLine("Error reading from ignored variables file " + CommandLineOptions.Clo.VariableDependenceIgnore + ": " + e); + } + } + + private Dictionary> ComputeGlobalControlDependences() { + + Dictionary> GlobalCtrlDep = new Dictionary>(); + Dictionary>> LocalCtrlDeps = new Dictionary>>(); + + // Work out and union together local control dependences + foreach (var Impl in prog.NonInlinedImplementations()) { + 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.NonInlinedImplementations()) { + 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.Implementations) { + 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)); + } + + } + + public static class Helper { + + public static IEnumerable NonInlinedProcedures(this Program prog) { + return prog.Procedures. + Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1); + } + + public static IEnumerable NonInlinedImplementations(this Program prog) { + return prog.Implementations. + Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1); + } + + } + +} -- cgit v1.2.3