diff options
| author |  allydonaldson <unknown> | 2013-04-30 15:36:09 +0100 |
|---|---|---|
| committer | allydonaldson <unknown> | 2013-04-30 15:36:09 +0100 |
| commit | 89c7d4c339f58dc9ec39b14b0b2a4120f2689322 (patch) | |
| tree | 4a22b414e8a17fa68a34279280142120fc1b203d | |
| parent | 98cab336f54799e105af45d06ec60e29cfca4fd5 (diff) | |
Staged Houdini
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 12 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 65 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 17 | ||||
| -rw-r--r-- | Source/Core/Core.csproj | 1 | ||||
| -rw-r--r-- | Source/Core/DeadVarElim.cs | 24 | ||||
| -rw-r--r-- | Source/Core/PureCollections.cs | 2 | ||||
| -rw-r--r-- | Source/Core/VariableDependenceAnalyser.cs | 872 | ||||
| -rw-r--r-- | Source/Graph/Graph.cs | 20 | ||||
| -rw-r--r-- | Source/Houdini/CandidateDependenceAnalyser.cs | 346 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 116 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.csproj | 3 | ||||
| -rw-r--r-- | Source/Predication/UniformityAnalyser.cs | 179 |
12 files changed, 1422 insertions, 235 deletions
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<Implementation> BuildCallGraph(Program program) {
+ Graph<Implementation> callGraph = new Graph<Implementation>();
+ Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Procedure proc = decl as Procedure;
+ if (proc == null) continue;
+ procToImpls[proc] = new HashSet<Implementation>();
+ }
+ 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<Block/*!*/>/*!*/ GraphFromImpl(Implementation impl) {
Contract.Requires(impl != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().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<Block/*!*/>(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<Variable> {
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 @@ <Compile Include="StandardVisitor.cs" />
<Compile Include="TypeAmbiguitySeeker.cs" />
<Compile Include="Util.cs" />
+ <Compile Include="VariableDependenceAnalyser.cs" />
<Compile Include="VCExp.cs" />
<Compile Include="..\version.cs" />
<Compile Include="Xml.cs" />
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<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();
@@ -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<VariableDescriptor> 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();
+ }
+
+ }
+
+ /// <summary>
+ /// Given a Boogie program, computes a graph that over-approximates dependences
+ /// between program variables.
+ /// </summary>
+ public class VariableDependenceAnalyser : IVariableDependenceAnalyser {
+
+ private Graph<VariableDescriptor> dependsOnNonTransitive;
+ private Program prog;
+ private Dictionary<Block, HashSet<Block>> BlockToControllingBlocks;
+ private Dictionary<Block, HashSet<VariableDescriptor>> ControllingBlockToVariables;
+
+ public VariableDependenceAnalyser(Program prog) {
+ this.prog = prog;
+ dependsOnNonTransitive = new Graph<VariableDescriptor>();
+ }
+
+
+ private void Initialise() {
+ foreach (var descriptor in
+ prog.TopLevelDeclarations.OfType<Variable>().Where(Item => !(Item is Constant)).
+ Select(Variable => Variable.Name).
+ Select(Name => new GlobalDescriptor(Name))) {
+ dependsOnNonTransitive.AddEdge(descriptor, descriptor);
+ }
+
+ foreach (var Proc in NonInlinedProcedures()) {
+
+ List<Variable> parameters = new List<Variable>();
+ 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<Variable> locals = new List<Variable>();
+ 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<Procedure> NonInlinedProcedures() {
+ return prog.TopLevelDeclarations.OfType<Procedure>().
+ Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1);
+ }
+
+ private IEnumerable<Implementation> NonInlinedImplementations() {
+ return prog.TopLevelDeclarations.OfType<Implementation>().
+ 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<VariableDescriptor> 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<VariableDescriptor> vs) {
+ foreach (var n in vs) {
+ dependsOnNonTransitive.AddEdge(v, n);
+ }
+ }
+
+ private Dictionary<Block, HashSet<VariableDescriptor>> ComputeControllingVariables(Dictionary<Block, HashSet<Block>> GlobalCtrlDep) {
+ Dictionary<Block, HashSet<VariableDescriptor>> result = new Dictionary<Block, HashSet<VariableDescriptor>>();
+ foreach (var Impl in NonInlinedImplementations()) {
+ foreach (var b in Impl.Blocks) {
+ result[b] = GetControlDependencyVariables(Impl.Name, b);
+ }
+ }
+ return result;
+ }
+
+ private HashSet<VariableDescriptor> 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<VariableDescriptor> result = new HashSet<VariableDescriptor>();
+ 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<Block, HashSet<Block>> ComputeGlobalControlDependences() {
+
+ Dictionary<Block, HashSet<Block>> GlobalCtrlDep = new Dictionary<Block, HashSet<Block>>();
+ Dictionary<Implementation, Dictionary<Block, HashSet<Block>>> LocalCtrlDeps = new Dictionary<Implementation, Dictionary<Block, HashSet<Block>>>();
+
+ // Work out and union together local control dependences
+ foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {
+ Graph<Block> blockGraph = prog.ProcessLoops(Impl);
+ LocalCtrlDeps[Impl] = blockGraph.ControlDependence();
+ foreach (var KeyValue in LocalCtrlDeps[Impl]) {
+ GlobalCtrlDep.Add(KeyValue.Key, KeyValue.Value);
+ }
+ }
+
+ Graph<Implementation> callGraph = Program.BuildCallGraph(prog);
+
+ // Add inter-procedural control dependence nodes based on calls
+ foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {
+ foreach (var b in Impl.Blocks) {
+ foreach (var cmd in b.Cmds.OfType<CallCmd>()) {
+ var DirectCallee = GetImplementation(cmd.callee);
+ if (DirectCallee != null) {
+ HashSet<Implementation> 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<Block, HashSet<Block>> result = new Dictionary<Block, HashSet<Block>>();
+
+ foreach (var KeyValue in GlobalCtrlDep) {
+ foreach (var v in KeyValue.Value) {
+ if (!result.ContainsKey(v)) {
+ result[v] = new HashSet<Block>();
+ }
+ result[v].Add(KeyValue.Key);
+ }
+ }
+
+ return result;
+ }
+
+ private HashSet<Implementation> ComputeIndirectCallees(Graph<Implementation> callGraph, Implementation DirectCallee) {
+ return ComputeIndirectCallees(callGraph, DirectCallee, new HashSet<Implementation>());
+ }
+
+ private HashSet<Implementation> ComputeIndirectCallees(Graph<Implementation> callGraph, Implementation DirectCallee, HashSet<Implementation> seen) {
+ if (seen.Contains(DirectCallee)) {
+ return new HashSet<Implementation>();
+ }
+ HashSet<Implementation> result = new HashSet<Implementation>();
+ result.Add(DirectCallee);
+ seen.Add(DirectCallee);
+ foreach (var succ in callGraph.Successors(DirectCallee)) {
+ result.UnionWith(ComputeIndirectCallees(callGraph, succ, seen));
+ }
+ return result;
+ }
+
+ private HashSet<Block> GetControllingBlocks(Block b, Dictionary<Block, HashSet<Block>> ctrlDep) {
+ HashSet<Block> result = new HashSet<Block>();
+ 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<Implementation>()) {
+ 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<SCC<VariableDescriptor>, HashSet<VariableDescriptor>> DependsOnCache = new Dictionary<SCC<VariableDescriptor>, HashSet<VariableDescriptor>>();
+
+ private Graph<SCC<VariableDescriptor>> DependsOnSCCsDAG;
+ private Dictionary<VariableDescriptor, SCC<VariableDescriptor>> VariableDescriptorToSCC;
+
+ public HashSet<VariableDescriptor> DependsOn(VariableDescriptor v) {
+ if (DependsOnSCCsDAG == null) {
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Variable dependence: computing SCCs");
+ }
+ Adjacency<VariableDescriptor> next = new Adjacency<VariableDescriptor>(dependsOnNonTransitive.Successors);
+ Adjacency<VariableDescriptor> prev = new Adjacency<VariableDescriptor>(dependsOnNonTransitive.Predecessors);
+ StronglyConnectedComponents<VariableDescriptor> DependsOnSCCs = new StronglyConnectedComponents<VariableDescriptor>(
+ dependsOnNonTransitive.Nodes, next, prev);
+ DependsOnSCCs.Compute();
+
+ VariableDescriptorToSCC = new Dictionary<VariableDescriptor, SCC<VariableDescriptor>>();
+ foreach (var scc in DependsOnSCCs) {
+ foreach (var s in scc) {
+ VariableDescriptorToSCC[s] = scc;
+ }
+ }
+
+ DependsOnSCCsDAG = new Graph<SCC<VariableDescriptor>>();
+ foreach (var edge in dependsOnNonTransitive.Edges) {
+ if (VariableDescriptorToSCC[edge.Item1] != VariableDescriptorToSCC[edge.Item2]) {
+ DependsOnSCCsDAG.AddEdge(VariableDescriptorToSCC[edge.Item1], VariableDescriptorToSCC[edge.Item2]);
+ }
+ }
+
+ SCC<VariableDescriptor> dummy = new SCC<VariableDescriptor>();
+ 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<VariableDescriptor> DependsOn(SCC<VariableDescriptor> vSCC) {
+
+ if (!DependsOnCache.ContainsKey(vSCC)) {
+ HashSet<VariableDescriptor> result = new HashSet<VariableDescriptor>();
+ 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<string> Procedures() {
+ return new HashSet<string>(dependsOnNonTransitive.Nodes.Where(Item =>
+ Item is LocalDescriptor).Select(Item => ((LocalDescriptor)Item).Proc));
+ }
+
+ }
+
+
+ /// <summary>
+ /// Given a Boogie program, computes a graph that over-approximates dependences
+ /// between program variables.
+ /// </summary>
+ public class OldVariableDependenceAnalyser : IVariableDependenceAnalyser {
+
+ private Program prog;
+
+ public Dictionary<VariableDescriptor, HashSet<VariableDescriptor>> dependsOn;
+
+ private Dictionary<string, HashSet<VariableDescriptor>> callControlDependences;
+
+ private bool ProcedureChanged;
+
+ public OldVariableDependenceAnalyser(Program prog) {
+ this.prog = prog;
+ dependsOn = new Dictionary<VariableDescriptor, HashSet<VariableDescriptor>>();
+ callControlDependences = new Dictionary<string, HashSet<VariableDescriptor>>();
+ }
+
+ public void Analyse() {
+
+ Initialise();
+
+ ProcedureChanged = true;
+ while (ProcedureChanged) {
+ ProcedureChanged = false;
+
+ foreach (var Impl in NonInlinedImplementations()) {
+ Analyse(Impl);
+ }
+
+ }
+
+ }
+
+ private Dictionary<string, int> temp = new Dictionary<string,int>();
+
+ 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<Block, HashSet<Block>> 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<VariableDescriptor> 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<VariableDescriptor> GetDependentVariables(IEnumerable<VariableDescriptor> vars) {
+ HashSet<VariableDescriptor> result = new HashSet<VariableDescriptor>();
+ foreach (var v in vars) {
+ result.UnionWith(dependsOn[v]);
+ }
+ return result;
+ }
+
+ private IEnumerable<VariableDescriptor> GetReferencedVariables(Absy node, string proc) {
+ var VarCollector = new VariableCollector();
+ VarCollector.Visit(node);
+ IEnumerable<VariableDescriptor> 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<Block, HashSet<VariableDescriptor>> ControlDependencyVariablesCache = new Dictionary<Block,HashSet<VariableDescriptor>>();
+
+ private HashSet<VariableDescriptor> GetControlDependencyVariables(Block b, string proc, Dictionary<Block, HashSet<Block>> ctrlDep) {
+
+ if (!ControlDependencyVariablesCache.ContainsKey(b)) {
+ HashSet<VariableDescriptor> ctrlDepVars = new HashSet<VariableDescriptor>();
+ 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<Variable> GetControlDependencyVariables(Block b) {
+
+ // This method works under the assumption that assume statements
+ // relevant to control flow between basic blocks have the "partition" attribute
+
+ HashSet<Variable> result = new HashSet<Variable>();
+ 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<Variable>().Where(Item => !(Item is Constant)).
+ Select(Variable => Variable.Name).
+ Select(Name => new GlobalDescriptor(Name))) {
+ dependsOn.Add(descriptor, new HashSet<VariableDescriptor> { descriptor });
+ }
+
+ foreach (var Proc in NonInlinedProcedures()) {
+
+ callControlDependences[Proc.Name] = new HashSet<VariableDescriptor>();
+
+ List<Variable> parameters = new List<Variable>();
+ 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<VariableDescriptor> { descriptor });
+ }
+ }
+
+ foreach (var Impl in NonInlinedImplementations()) {
+
+ List<Variable> locals = new List<Variable>();
+ 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<VariableDescriptor> { descriptor });
+ }
+ }
+ }
+
+ private IEnumerable<Procedure> NonInlinedProcedures() {
+ return prog.TopLevelDeclarations.OfType<Procedure>().
+ Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1);
+ }
+
+ private IEnumerable<Implementation> NonInlinedImplementations() {
+ return prog.TopLevelDeclarations.OfType<Implementation>().
+ 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<VariableDescriptor,HashSet<VariableDescriptor>> 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<string> Procedures() {
+ return new HashSet<string>(dependsOn.Where(Item =>
+ Item.Key is LocalDescriptor).Select(Item => ((LocalDescriptor)Item.Key).Proc));
+ }
+
+ void AddDependences(VariableDescriptor v, IEnumerable<VariableDescriptor> 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<VariableDescriptor> ctrlDepVars) {
+ foreach (var n in ctrlDepVars) {
+ if (!callControlDependences[Proc].Contains(n)) {
+ callControlDependences[Proc].Add(n);
+ ProcedureChanged = true;
+ }
+ }
+ }
+
+
+ private Dictionary<string, Dictionary<Block, HashSet<Block>>> ControlDependenceCache = new Dictionary<string, Dictionary<Block, HashSet<Block>>>();
+
+ private Dictionary<Block, HashSet<Block>> GetControlDependenceTransitiveClosure(Implementation Impl) {
+ if (!ControlDependenceCache.ContainsKey(Impl.Name)) {
+ Graph<Block> blockGraph = prog.ProcessLoops(Impl);
+ Dictionary<Block, HashSet<Block>> ctrlDep = blockGraph.ControlDependence();
+ ctrlDep.TransitiveClosure();
+ ControlDependenceCache[Impl.Name] = ctrlDep;
+ }
+ return ControlDependenceCache[Impl.Name];
+ }
+
+ private Dictionary<string, List<Block>> OrderedBlocksCache = new Dictionary<string,List<Block>>();
+
+ private List<Block> GetOrderedBlocks(Implementation Impl) {
+ if (!OrderedBlocksCache.ContainsKey(Impl.Name)) {
+ List<Block> orderedBlocks = PostOrder(Impl.Blocks[0], new HashSet<Block>());
+ Debug.Assert(orderedBlocks.Count() == Impl.Blocks.Count());
+ orderedBlocks.Reverse();
+ OrderedBlocksCache[Impl.Name] = orderedBlocks;
+ }
+ return OrderedBlocksCache[Impl.Name];
+ }
+
+ private List<Block> PostOrder(Block b, HashSet<Block> seen) {
+ seen.Add(b);
+ List<Block> result = new List<Block>();
+ 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<VariableDescriptor> 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<Node> dual = g.Dual(new Node());
DomRelation<Node> pdom = dual.DominatorMap;
+
var result = new Dictionary<Node, HashSet<Node>>();
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<Node>(deps);
}
}
+
return result;
}
+ public static void TransitiveClosure<Node>(this Dictionary<Node, HashSet<Node>> graph) where Node : class {
+ bool changed;
+ do {
+ changed = false;
+ foreach (var entry in graph) {
+ var newSuccessors = new HashSet<Node>(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/*<Node!>*//*!*/ Adjacency<T>(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<string> candidates;
+ private Dictionary<string, HashSet<VariableDescriptor>> candidateDependsOn;
+ private Dictionary<VariableDescriptor, HashSet<string>> variableDirectlyReferredToByCandidates;
+ private Graph<string> CandidateDependences;
+ private StronglyConnectedComponents<string> SCCs;
+ private Graph<SCC<string>> 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<string, HashSet<VariableDescriptor>>();
+ variableDirectlyReferredToByCandidates = new Dictionary<VariableDescriptor, HashSet<string>>();
+ foreach (var c in candidates) {
+ candidateDependsOn[c] = new HashSet<VariableDescriptor>();
+ }
+
+ // Candidate loop invariants
+ foreach(var impl in prog.TopLevelDeclarations.OfType<Implementation>()) {
+ 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<Procedure>()) {
+ 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<string>();
+
+ 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<string> next = new Adjacency<string>(CandidateDependences.Successors);
+ Adjacency<string> prev = new Adjacency<string>(CandidateDependences.Predecessors);
+ SCCs = new StronglyConnectedComponents<string>(
+ CandidateDependences.Nodes, next, prev);
+ SCCs.Compute();
+
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Candidate dependence analysis: Building stages DAG");
+ }
+
+ Dictionary<string, SCC<string>> rep = new Dictionary<string, SCC<string>>();
+ foreach (var scc in SCCs) {
+ foreach (var s in scc) {
+ rep[s] = scc;
+ }
+ }
+
+ StagesDAG = new Graph<SCC<string>>();
+
+ foreach (var edge in CandidateDependences.Edges) {
+ if (rep[edge.Item1] != rep[edge.Item2]) {
+ StagesDAG.AddEdge(rep[edge.Item1], rep[edge.Item2]);
+ }
+ }
+
+ SCC<string> dummy = new SCC<string>();
+ foreach (var scc in SCCs) {
+ StagesDAG.AddEdge(scc, dummy);
+ }
+
+ }
+
+ private bool FindInDAG(Graph<SCC<string>> DAG, SCC<string> toFind, SCC<string> 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<string>();
+ }
+ variableDirectlyReferredToByCandidates[vd].Add(candidate);
+
+ foreach (var w in varDepAnalyser.DependsOn(vd)) {
+ candidateDependsOn[candidate].Add(w);
+ }
+ }
+ }
+ }
+
+ private bool IsStageDependence(SCC<string> Src, SCC<string> 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<SCC<string>> 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<string> 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<string> GetCandidates() {
+ return prog.TopLevelDeclarations.OfType<Variable>().Where(Item =>
+ QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name);
+ }
+
+
+ public void ApplyStages() {
+
+ IEnumerable<Constant> candidates = prog.TopLevelDeclarations.OfType<Constant>().
+ 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<string> start = null;
+ foreach (var n in StagesDAG.Nodes) {
+ if (StagesDAG.Successors(n).Count() == 0) {
+ start = n;
+ break;
+ }
+ }
+ System.Diagnostics.Debug.Assert(start != null);
+
+ HashSet<SCC<string>> done = new HashSet<SCC<string>>();
+ done.Add(start);
+
+ bool finished = false;
+ int stageId = 0;
+ while (!finished) {
+ finished = true;
+ HashSet<SCC<string>> stage = new HashSet<SCC<string>>();
+ 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<object>() {
+ new LiteralExpr(Token.NoToken, BigNum.FromInt(stageId))
+ }, candidate.Attributes);
+ }
+ }
+ }
+
+ stageId++;
+ }
+
+ }
+ else {
+ List<SCC<string>> 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<object>() {
+ 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<string, HashSet<Implementation>> assumedInImpl { get; private set; }
}
-
- private Graph<Implementation> BuildCallGraph() {
- Graph<Implementation> callGraph = new Graph<Implementation>();
- Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();
- foreach (Declaration decl in program.TopLevelDeclarations) {
- Procedure proc = decl as Procedure;
- if (proc == null) continue;
- procToImpls[proc] = new HashSet<Implementation>();
- }
- 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 { /// <summary>
/// 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<Procedure>()) {
+ 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<Variable>().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<Variable>().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<Variable>().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 @@ -<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -80,6 +80,7 @@ </Compile>
<Compile Include="AbstractHoudini.cs" />
<Compile Include="Checker.cs" />
+ <Compile Include="CandidateDependenceAnalyser.cs" />
<Compile Include="Houdini.cs" />
</ItemGroup>
<ItemGroup>
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<Implementation> entryPoints;
@@ -33,10 +33,6 @@ namespace Microsoft.Boogie private Dictionary<string, List<string>> outParameters;
- private List<WhileCmd> loopStack;
-
- private bool hitNonuniformReturn;
-
/// <summary>
/// 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<Implementation> entryPoints, IEnumerable<Variable> nonUniformVars)
+ public UniformityAnalyser(Program prog, bool doAnalysis, ISet<Implementation> entryPoints, IEnumerable<Variable> nonUniformVars)
{
this.prog = prog;
this.doAnalysis = doAnalysis;
- this.unstructured = unstructured;
this.entryPoints = entryPoints;
this.nonUniformVars = nonUniformVars;
uniformityInfo = new Dictionary<string, KeyValuePair<bool, Dictionary<string, bool>>>();
@@ -85,7 +80,6 @@ namespace Microsoft.Boogie loopsWithNonuniformReturn = new Dictionary<string, HashSet<int>>();
inParameters = new Dictionary<string, List<string>>();
outParameters = new Dictionary<string, List<string>>();
- loopStack = new List<WhileCmd>();
}
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<Block>(Impl.Blocks);
-
- foreach (Variable v in Impl.LocVars) {
- if (IsUniform(Impl.Name, v.Name)) {
- SetNonUniform(Impl.Name, v.Name);
- }
- }
+ nonUniformBlocks[Impl.Name] = new HashSet<Block>(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<Block> 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<Block>(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<Block>();
- 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<Block> blockGraph = prog.ProcessLoops(Impl);
+ var ctrlDep = blockGraph.ControlDependence();
+
+ // Compute transitive closure of control dependence info.
+ ctrlDep.TransitiveClosure();
+
+ var nonUniformBlockSet = new HashSet<Block>();
+ 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));
- }
}
}
|