diff --git a/Source/Core/Analysis/BlockCoalescer.cs b/Source/Core/Analysis/BlockCoalescer.cs
new file mode 100644
index 000000000..959ff9275
--- /dev/null
+++ b/Source/Core/Analysis/BlockCoalescer.cs
@@ -0,0 +1,165 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie;
+
+public class BlockCoalescer : ReadOnlyVisitor
+{
+ public static void CoalesceBlocks(Program program)
+ {
+ Contract.Requires(program != null);
+ BlockCoalescer blockCoalescer = new BlockCoalescer();
+ blockCoalescer.Visit(program);
+ }
+
+ private static HashSet /*!*/ ComputeMultiPredecessorBlocks(Implementation /*!*/ impl)
+ {
+ Contract.Requires(impl != null);
+ Contract.Ensures(cce.NonNullElements(Contract.Result>()));
+ HashSet visitedBlocks = new HashSet();
+ HashSet multiPredBlocks = new HashSet();
+ Stack dfsStack = new Stack();
+ dfsStack.Push(impl.Blocks[0]);
+ while (dfsStack.Count > 0)
+ {
+ Block /*!*/
+ b = dfsStack.Pop();
+ Contract.Assert(b != null);
+ if (visitedBlocks.Contains(b))
+ {
+ multiPredBlocks.Add(b);
+ continue;
+ }
+
+ visitedBlocks.Add(b);
+ if (b.TransferCmd == null)
+ {
+ continue;
+ }
+
+ if (b.TransferCmd is ReturnCmd)
+ {
+ continue;
+ }
+
+ Contract.Assert(b.TransferCmd is GotoCmd);
+ GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
+ if (gotoCmd.labelTargets == null)
+ {
+ continue;
+ }
+
+ foreach (Block /*!*/ succ in gotoCmd.labelTargets)
+ {
+ Contract.Assert(succ != null);
+ dfsStack.Push(succ);
+ }
+ }
+
+ return multiPredBlocks;
+ }
+
+ public override Implementation VisitImplementation(Implementation impl)
+ {
+ //Contract.Requires(impl != null);
+ Contract.Ensures(Contract.Result() != null);
+ //Console.WriteLine("Procedure {0}", impl.Name);
+ //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count);
+
+ HashSet multiPredBlocks = ComputeMultiPredecessorBlocks(impl);
+ Contract.Assert(cce.NonNullElements(multiPredBlocks));
+ HashSet visitedBlocks = new HashSet();
+ HashSet removedBlocks = new HashSet();
+ Stack dfsStack = new Stack();
+ dfsStack.Push(impl.Blocks[0]);
+ while (dfsStack.Count > 0)
+ {
+ Block /*!*/
+ b = dfsStack.Pop();
+ Contract.Assert(b != null);
+ if (visitedBlocks.Contains(b))
+ {
+ continue;
+ }
+
+ visitedBlocks.Add(b);
+ if (b.TransferCmd == null)
+ {
+ continue;
+ }
+
+ if (b.TransferCmd is ReturnCmd)
+ {
+ continue;
+ }
+
+ Contract.Assert(b.TransferCmd is GotoCmd);
+ GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
+ if (gotoCmd.labelTargets == null)
+ {
+ continue;
+ }
+
+ if (gotoCmd.labelTargets.Count == 1)
+ {
+ Block /*!*/
+ succ = cce.NonNull(gotoCmd.labelTargets[0]);
+ if (!multiPredBlocks.Contains(succ))
+ {
+ foreach (Cmd /*!*/ cmd in succ.Cmds)
+ {
+ Contract.Assert(cmd != null);
+ b.Cmds.Add(cmd);
+ }
+
+ b.TransferCmd = succ.TransferCmd;
+ if (!b.tok.IsValid && succ.tok.IsValid)
+ {
+ b.tok = succ.tok;
+ b.Label = succ.Label;
+ }
+
+ removedBlocks.Add(succ);
+ dfsStack.Push(b);
+ visitedBlocks.Remove(b);
+ continue;
+ }
+ }
+
+ foreach (Block /*!*/ succ in gotoCmd.labelTargets)
+ {
+ Contract.Assert(succ != null);
+ dfsStack.Push(succ);
+ }
+ }
+
+ List newBlocks = new List();
+ foreach (Block /*!*/ b in impl.Blocks)
+ {
+ Contract.Assert(b != null);
+ if (visitedBlocks.Contains(b) && !removedBlocks.Contains(b))
+ {
+ newBlocks.Add(b);
+ }
+ }
+
+ impl.Blocks = newBlocks;
+ foreach (Block b in impl.Blocks)
+ {
+ if (b.TransferCmd is ReturnCmd)
+ {
+ continue;
+ }
+
+ GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
+ gotoCmd.labelNames = new List();
+ foreach (Block succ in gotoCmd.labelTargets)
+ {
+ gotoCmd.labelNames.Add(succ.Label);
+ }
+ }
+
+ // Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count);
+ return impl;
+ }
+}
\ No newline at end of file
diff --git a/Source/Core/Analysis/LiveVariableAnalysis/GenKillWeight.cs b/Source/Core/Analysis/LiveVariableAnalysis/GenKillWeight.cs
new file mode 100644
index 000000000..bd4366c01
--- /dev/null
+++ b/Source/Core/Analysis/LiveVariableAnalysis/GenKillWeight.cs
@@ -0,0 +1,189 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie;
+
+/*
+// An idempotent semiring interface
+abstract public class Weight {
+ abstract public Weight! one();
+ abstract public Weight! zero();
+ abstract public Weight! extend(Weight! w1, Weight! w2);
+ abstract public Weight! combine(Weight! w1, Weight! w2);
+ abstract public Weight! isEqual(Weight! w);
+ abstract public Weight! projectLocals()
+}
+*/
+
+// Weight domain for LiveVariableAnalysis (Gen/Kill)
+public class GenKillWeight
+{
+ // lambda S. (S - kill) union gen
+ HashSet /*!*/
+ gen;
+
+ HashSet /*!*/
+ kill;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(cce.NonNullElements(gen));
+ Contract.Invariant(cce.NonNullElements(kill));
+ Contract.Invariant(oneWeight != null);
+ Contract.Invariant(zeroWeight != null);
+ }
+
+ bool isZero;
+
+ public static GenKillWeight /*!*/
+ oneWeight = new GenKillWeight(new HashSet(), new HashSet());
+
+ public static GenKillWeight /*!*/
+ zeroWeight = new GenKillWeight();
+
+ // initializes to zero
+ public GenKillWeight()
+ {
+ this.isZero = true;
+ this.gen = new HashSet();
+ this.kill = new HashSet();
+ }
+
+ public GenKillWeight(HashSet gen, HashSet kill)
+ {
+ Contract.Requires(cce.NonNullElements(gen));
+ Contract.Requires(cce.NonNullElements(kill));
+ Contract.Assert(gen != null);
+ Contract.Assert(kill != null);
+ this.gen = gen;
+ this.kill = kill;
+ this.isZero = false;
+ }
+
+ public static GenKillWeight one()
+ {
+ Contract.Ensures(Contract.Result() != null);
+ return oneWeight;
+ }
+
+ public static GenKillWeight zero()
+ {
+ Contract.Ensures(Contract.Result() != null);
+ return zeroWeight;
+ }
+
+ public static GenKillWeight extend(GenKillWeight w1, GenKillWeight w2)
+ {
+ Contract.Requires(w2 != null);
+ Contract.Requires(w1 != null);
+ Contract.Ensures(Contract.Result() != null);
+ if (w1.isZero || w2.isZero)
+ {
+ return zero();
+ }
+
+ HashSet t = new HashSet(w2.gen);
+ t.ExceptWith(w1.kill);
+ HashSet g = new HashSet(w1.gen);
+ g.UnionWith(t);
+ HashSet k = new HashSet(w1.kill);
+ k.UnionWith(w2.kill);
+ return new GenKillWeight(g, k);
+ //return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill));
+ }
+
+ public static GenKillWeight combine(GenKillWeight w1, GenKillWeight w2)
+ {
+ Contract.Requires(w2 != null);
+ Contract.Requires(w1 != null);
+ Contract.Ensures(Contract.Result() != null);
+ if (w1.isZero)
+ {
+ return w2;
+ }
+
+ if (w2.isZero)
+ {
+ return w1;
+ }
+
+ HashSet g = new HashSet(w1.gen);
+ g.UnionWith(w2.gen);
+ HashSet k = new HashSet(w1.kill);
+ k.IntersectWith(w2.kill);
+ return new GenKillWeight(g, k);
+ //return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill));
+ }
+
+ public static GenKillWeight projectLocals(GenKillWeight w)
+ {
+ Contract.Requires(w != null);
+ Contract.Ensures(Contract.Result() != null);
+ HashSet gen = new HashSet();
+ foreach (Variable v in w.gen)
+ {
+ if (isGlobal(v))
+ {
+ gen.Add(v);
+ }
+ }
+
+ HashSet kill = new HashSet();
+ foreach (Variable v in w.kill)
+ {
+ if (isGlobal(v))
+ {
+ kill.Add(v);
+ }
+ }
+
+ return new GenKillWeight(gen, kill);
+ }
+
+ public static bool isEqual(GenKillWeight w1, GenKillWeight w2)
+ {
+ Contract.Requires(w2 != null);
+ Contract.Requires(w1 != null);
+ if (w1.isZero)
+ {
+ return w2.isZero;
+ }
+
+ if (w2.isZero)
+ {
+ return w1.isZero;
+ }
+
+ return (w1.gen.Equals(w2.gen) && w1.kill.Equals(w2.kill));
+ }
+
+ private static bool isGlobal(Variable v)
+ {
+ Contract.Requires(v != null);
+ return (v is GlobalVariable);
+ }
+
+ [Pure]
+ public override string ToString()
+ {
+ Contract.Ensures(Contract.Result() != null);
+ return string.Format("({0},{1})", gen.ToString(), kill.ToString());
+ }
+
+ public HashSet /*!*/ getLiveVars()
+ {
+ Contract.Ensures(cce.NonNullElements(Contract.Result>()));
+ return gen;
+ }
+
+ public HashSet /*!*/ getLiveVars(HashSet /*!*/ lv)
+ {
+ Contract.Requires(cce.NonNullElements(lv));
+ Contract.Ensures(cce.NonNullElements(Contract.Result>()));
+ HashSet temp = new HashSet(lv);
+ temp.ExceptWith(kill);
+ temp.UnionWith(gen);
+ return temp;
+ }
+}
\ No newline at end of file
diff --git a/Source/Core/Analysis/LiveVariableAnalysis/ImplementationControlFlowGraph.cs b/Source/Core/Analysis/LiveVariableAnalysis/ImplementationControlFlowGraph.cs
new file mode 100644
index 000000000..9845609b0
--- /dev/null
+++ b/Source/Core/Analysis/LiveVariableAnalysis/ImplementationControlFlowGraph.cs
@@ -0,0 +1,219 @@
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie.GraphUtil;
+
+namespace Microsoft.Boogie;
+
+public class ImplementationControlFlowGraph
+{
+ public Graph /*!*/
+ graph;
+
+ // Map from procedure to the list of blocks that call that procedure
+ public Dictionary /*!*/> /*!*/
+ procsCalled;
+
+ public HashSet /*!*/
+ nodes;
+
+ public Dictionary /*!*/> /*!*/
+ succEdges;
+
+ public Dictionary /*!*/> /*!*/
+ predEdges;
+
+ private Dictionary /*!*/
+ priority;
+
+ public HashSet /*!*/
+ srcNodes;
+
+ public HashSet /*!*/
+ exitNodes;
+
+ public Dictionary /*!*/
+ weightBefore;
+
+ public Dictionary /*!*/
+ weightAfter;
+
+ public Dictionary /*!*/> /*!*/
+ liveVarsAfter;
+
+ public Dictionary /*!*/> /*!*/
+ liveVarsBefore;
+
+ public GenKillWeight /*!*/
+ summary;
+
+ private readonly CoreOptions options;
+
+ public Implementation /*!*/
+ impl;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(cce.NonNullElements(graph.Nodes));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(procsCalled));
+ Contract.Invariant(cce.NonNullElements(nodes));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(succEdges));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(predEdges));
+ Contract.Invariant(priority != null);
+ Contract.Invariant(cce.NonNullElements(srcNodes));
+ Contract.Invariant(cce.NonNullElements(exitNodes));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(weightBefore));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(weightAfter));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsAfter));
+ Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsBefore));
+ Contract.Invariant(summary != null);
+ Contract.Invariant(impl != null);
+ }
+
+
+ [NotDelayed]
+ public ImplementationControlFlowGraph(CoreOptions options, Implementation impl)
+ {
+ Contract.Requires(impl != null);
+ this.graph = new Graph();
+ this.procsCalled = new Dictionary /*!*/>();
+ this.nodes = new HashSet();
+ this.succEdges = new Dictionary /*!*/>();
+ this.predEdges = new Dictionary /*!*/>();
+
+ this.priority = new Dictionary();
+
+ this.srcNodes = new HashSet();
+ this.exitNodes = new HashSet();
+
+ this.weightBefore = new Dictionary();
+ this.weightAfter = new Dictionary();
+ this.liveVarsAfter = new Dictionary /*!*/>();
+ this.liveVarsBefore = new Dictionary /*!*/>();
+
+ summary = GenKillWeight.zero();
+ this.options = options;
+ this.impl = impl;
+
+ Initialize(impl);
+ }
+
+ private void Initialize(Implementation impl)
+ {
+ Contract.Requires(impl != null);
+ addSource(impl.Blocks[0]);
+ graph.AddSource(impl.Blocks[0]);
+
+ foreach (Block /*!*/ b in impl.Blocks)
+ {
+ Contract.Assert(b != null);
+ if (b.TransferCmd is ReturnCmd)
+ {
+ exitNodes.Add(b);
+ }
+ else
+ {
+ GotoCmd gc = b.TransferCmd as GotoCmd;
+ Contract.Assert(gc != null);
+ Contract.Assert(gc.labelTargets != null);
+ foreach (Block /*!*/ t in gc.labelTargets)
+ {
+ Contract.Assert(t != null);
+ addEdge(b, t);
+ graph.AddEdge(b, t);
+ }
+ }
+
+ weightBefore[b] = GenKillWeight.zero();
+ weightAfter[b] = GenKillWeight.zero();
+
+ foreach (Cmd /*!*/ c in b.Cmds)
+ {
+ Contract.Assert(c != null);
+ if (c is CallCmd)
+ {
+ CallCmd /*!*/
+ cc = cce.NonNull((CallCmd /*!*/) c);
+ Contract.Assert(cc.Proc != null);
+ string /*!*/
+ procName = cc.Proc.Name;
+ Contract.Assert(procName != null);
+ if (!procsCalled.ContainsKey(procName))
+ {
+ procsCalled.Add(procName, new List());
+ }
+
+ procsCalled[procName].Add(b);
+ }
+ }
+ }
+
+ graph.TarjanTopSort(out var acyclic, out var sortedNodes);
+
+ if (!acyclic)
+ {
+ options.OutputWriter.WriteLine("Warning: graph is not a dag");
+ }
+
+ int num = sortedNodes.Count;
+ foreach (Block /*!*/ b in sortedNodes)
+ {
+ Contract.Assert(b != null);
+ priority.Add(b, num);
+ num--;
+ }
+ }
+
+ public int getPriority(Block b)
+ {
+ Contract.Requires(b != null);
+ if (priority.ContainsKey(b))
+ {
+ return priority[b];
+ }
+
+ return Int32.MaxValue;
+ }
+
+ private void addSource(Block b)
+ {
+ Contract.Requires(b != null);
+ registerNode(b);
+ this.srcNodes.Add(b);
+ }
+
+ private void addExit(Block b)
+ {
+ Contract.Requires(b != null);
+ registerNode(b);
+ this.exitNodes.Add(b);
+ }
+
+ private void registerNode(Block b)
+ {
+ Contract.Requires(b != null);
+ if (!succEdges.ContainsKey(b))
+ {
+ succEdges.Add(b, new HashSet());
+ }
+
+ if (!predEdges.ContainsKey(b))
+ {
+ predEdges.Add(b, new HashSet());
+ }
+
+ nodes.Add(b);
+ }
+
+ private void addEdge(Block src, Block tgt)
+ {
+ Contract.Requires(tgt != null);
+ Contract.Requires(src != null);
+ registerNode(src);
+ registerNode(tgt);
+
+ succEdges[src].Add(tgt);
+ predEdges[tgt].Add(src);
+ }
+}
\ No newline at end of file
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/Analysis/LiveVariableAnalysis/InterProcGenKill.cs
similarity index 50%
rename from Source/Core/DeadVarElim.cs
rename to Source/Core/Analysis/LiveVariableAnalysis/InterProcGenKill.cs
index 65233640b..615bc384b 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/Analysis/LiveVariableAnalysis/InterProcGenKill.cs
@@ -1,1143 +1,9 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
+using System.Collections.Generic;
using Microsoft.Boogie.GraphUtil;
using System.Diagnostics.Contracts;
namespace Microsoft.Boogie
{
- public class UnusedVarEliminator : VariableCollector
- {
- public static void Eliminate(Program program)
- {
- Contract.Requires(program != null);
- UnusedVarEliminator elim = new UnusedVarEliminator();
- elim.Visit(program);
- }
-
- private UnusedVarEliminator()
- : base()
- {
- }
-
- public override Implementation VisitImplementation(Implementation node)
- {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result() != null);
- //Console.WriteLine("Procedure {0}", node.Name);
- Implementation /*!*/
- impl = base.VisitImplementation(node);
- Contract.Assert(impl != null);
- //Console.WriteLine("Old number of local variables = {0}", impl.LocVars.Length);
- List /*!*/
- vars = new List();
- foreach (Variable /*!*/ var in impl.LocVars)
- {
- Contract.Assert(var != null);
- if (_usedVars.Contains(var))
- {
- vars.Add(var);
- }
- }
-
- impl.LocVars = vars;
- //Console.WriteLine("New number of local variables = {0}", impl.LocVars.Length);
- //Console.WriteLine("---------------------------------");
- _usedVars.Clear();
- return impl;
- }
- }
-
- public class ModSetCollector : ReadOnlyVisitor
- {
- private CoreOptions options;
- private Procedure enclosingProc;
-
- private Dictionary> modSets;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(cce.NonNullDictionaryAndValues(modSets));
- Contract.Invariant(Contract.ForAll(modSets.Values, v => cce.NonNullElements(v)));
- }
-
- public ModSetCollector(CoreOptions options)
- {
- this.options = options;
- modSets = new Dictionary>();
- }
-
- private bool moreProcessingRequired;
-
- public void DoModSetAnalysis(Program program)
- {
- Contract.Requires(program != null);
-
- if (options.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);*/
- }
-
- HashSet implementedProcs = new HashSet();
- foreach (var impl in program.Implementations)
- {
- if (impl.Proc != null)
- {
- implementedProcs.Add(impl.Proc);
- }
- }
-
- foreach (var proc in program.Procedures)
- {
- if (!implementedProcs.Contains(proc))
- {
- enclosingProc = proc;
- foreach (var expr in proc.Modifies)
- {
- Contract.Assert(expr != null);
- ProcessVariable(expr.Decl);
- }
-
- enclosingProc = null;
- }
- else
- {
- modSets.Add(proc, new HashSet());
- }
- }
-
- moreProcessingRequired = true;
- while (moreProcessingRequired)
- {
- moreProcessingRequired = false;
- this.Visit(program);
- }
-
- foreach (Procedure x in modSets.Keys)
- {
- x.Modifies = new List();
- foreach (Variable v in modSets[x])
- {
- x.Modifies.Add(new IdentifierExpr(v.tok, v));
- }
- }
-
-#if DEBUG_PRINT
- options.OutputWriter.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count);
- foreach (Procedure/*!*/ x in modSets.Keys) {
- Contract.Assert(x != null);
- options.OutputWriter.Write("{0} : ", x.Name);
- bool first = true;
- foreach (Variable/*!*/ y in modSets[x]) {
- Contract.Assert(y != null);
- if (first)
- first = false;
- else
- options.OutputWriter.Write(", ");
- options.OutputWriter.Write("{0}", y.Name);
- }
- options.OutputWriter.WriteLine("");
- options.OutputWriter
-#endif
- }
-
- public override Implementation VisitImplementation(Implementation node)
- {
- //Contract.Requires(node != null);
- Contract.Ensures(Contract.Result() != null);
- enclosingProc = node.Proc;
- Implementation /*!*/
- ret = base.VisitImplementation(node);
- Contract.Assert(ret != null);
- enclosingProc = null;
-
- return ret;
- }
-
- public override Cmd VisitAssignCmd(AssignCmd assignCmd)
- {
- Contract.Ensures(Contract.Result() != null);
- Cmd ret = base.VisitAssignCmd(assignCmd);
- foreach (AssignLhs lhs in assignCmd.Lhss)
- {
- Contract.Assert(lhs != null);
- ProcessVariable(lhs.DeepAssignedVariable);
- }
-
- return ret;
- }
-
- public override Cmd VisitUnpackCmd(UnpackCmd unpackCmd)
- {
- Contract.Ensures(Contract.Result() != null);
- Cmd ret = base.VisitUnpackCmd(unpackCmd);
- foreach (var expr in unpackCmd.Lhs.Args)
- {
- ProcessVariable(((IdentifierExpr)expr).Decl);
- }
- return ret;
- }
-
- public override Cmd VisitHavocCmd(HavocCmd havocCmd)
- {
- Contract.Ensures(Contract.Result() != null);
- Cmd ret = base.VisitHavocCmd(havocCmd);
- foreach (IdentifierExpr expr in havocCmd.Vars)
- {
- Contract.Assert(expr != null);
- ProcessVariable(expr.Decl);
- }
-
- return ret;
- }
-
- public override Cmd VisitCallCmd(CallCmd callCmd)
- {
- //Contract.Requires(callCmd != null);
- Contract.Ensures(Contract.Result() != null);
- Cmd ret = base.VisitCallCmd(callCmd);
- foreach (IdentifierExpr ie in callCmd.Outs)
- {
- if (ie != null)
- {
- ProcessVariable(ie.Decl);
- }
- }
-
- Procedure callee = callCmd.Proc;
- if (callee == null)
- {
- return ret;
- }
-
- if (modSets.ContainsKey(callee))
- {
- foreach (Variable var in modSets[callee])
- {
- ProcessVariable(var);
- }
- }
-
- return ret;
- }
-
- private void ProcessVariable(Variable var)
- {
- Procedure /*!*/
- localProc = cce.NonNull(enclosingProc);
- if (var == null)
- {
- return;
- }
-
- if (!(var is GlobalVariable))
- {
- return;
- }
-
- if (!modSets.ContainsKey(localProc))
- {
- modSets[localProc] = new HashSet();
- }
-
- if (modSets[localProc].Contains(var))
- {
- return;
- }
-
- moreProcessingRequired = true;
- modSets[localProc].Add(var);
- }
-
- public override Expr VisitCodeExpr(CodeExpr node)
- {
- // don't go into the code expression, since it can only modify variables local to the code expression,
- // and the mod-set analysis is interested in global variables
- return node;
- }
- }
-
- public class MutableVariableCollector : ReadOnlyVisitor
- {
- public HashSet UsedVariables = new HashSet();
-
- public void AddUsedVariables(HashSet usedVariables)
- {
- Contract.Requires(usedVariables != null);
-
- foreach (var v in usedVariables)
- {
- UsedVariables.Add(v);
- }
- }
-
- public override Expr VisitIdentifierExpr(IdentifierExpr node)
- {
- Contract.Ensures(Contract.Result() != null);
-
- if (node.Decl != null && node.Decl.IsMutable)
- {
- UsedVariables.Add(node.Decl);
- }
-
- return base.VisitIdentifierExpr(node);
- }
- }
-
- public class VariableCollector : ReadOnlyVisitor
- {
- private bool _ignoreOld;
-
- protected HashSet _usedVars;
-
- public IEnumerable usedVars
- {
- get { return _usedVars.AsEnumerable(); }
- }
-
- protected HashSet _oldVarsUsed;
-
- public IEnumerable oldVarsUsed
- {
- get { return _oldVarsUsed.AsEnumerable(); }
- }
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(cce.NonNullElements(_usedVars));
- Contract.Invariant(cce.NonNullElements(_oldVarsUsed));
- }
-
- int insideOldExpr;
-
- public VariableCollector(bool ignoreOld = false)
- {
- _ignoreOld = ignoreOld;
- _usedVars = new HashSet();
- _oldVarsUsed = new HashSet();
- insideOldExpr = 0;
- }
-
- public override Expr VisitOldExpr(OldExpr node)
- {
- if (!_ignoreOld)
- {
- insideOldExpr++;
- node.Expr = this.VisitExpr(node.Expr);
- insideOldExpr--;
- }
- return node;
- }
-
- public override Expr VisitIdentifierExpr(IdentifierExpr node)
- {
- if (node.Decl != null)
- {
- _usedVars.Add(node.Decl);
- if (insideOldExpr > 0)
- {
- _oldVarsUsed.Add(node.Decl);
- }
- }
- return node;
- }
-
- public static IEnumerable Collect(Absy node, bool ignoreOld = false)
- {
- var collector = new VariableCollector(ignoreOld);
- collector.Visit(node);
- return collector.usedVars;
- }
-
- public static IEnumerable Collect(IEnumerable nodes, bool ignoreOld = false)
- {
- var collector = new VariableCollector(ignoreOld);
- foreach (var node in nodes)
- {
- collector.Visit(node);
- }
- return collector.usedVars;
- }
- }
-
- public class BlockCoalescer : ReadOnlyVisitor
- {
- public static void CoalesceBlocks(Program program)
- {
- Contract.Requires(program != null);
- BlockCoalescer blockCoalescer = new BlockCoalescer();
- blockCoalescer.Visit(program);
- }
-
- private static HashSet /*!*/ ComputeMultiPredecessorBlocks(Implementation /*!*/ impl)
- {
- Contract.Requires(impl != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result>()));
- HashSet visitedBlocks = new HashSet();
- HashSet multiPredBlocks = new HashSet();
- Stack dfsStack = new Stack();
- dfsStack.Push(impl.Blocks[0]);
- while (dfsStack.Count > 0)
- {
- Block /*!*/
- b = dfsStack.Pop();
- Contract.Assert(b != null);
- if (visitedBlocks.Contains(b))
- {
- multiPredBlocks.Add(b);
- continue;
- }
-
- visitedBlocks.Add(b);
- if (b.TransferCmd == null)
- {
- continue;
- }
-
- if (b.TransferCmd is ReturnCmd)
- {
- continue;
- }
-
- Contract.Assert(b.TransferCmd is GotoCmd);
- GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
- if (gotoCmd.labelTargets == null)
- {
- continue;
- }
-
- foreach (Block /*!*/ succ in gotoCmd.labelTargets)
- {
- Contract.Assert(succ != null);
- dfsStack.Push(succ);
- }
- }
-
- return multiPredBlocks;
- }
-
- public override Implementation VisitImplementation(Implementation impl)
- {
- //Contract.Requires(impl != null);
- Contract.Ensures(Contract.Result() != null);
- //Console.WriteLine("Procedure {0}", impl.Name);
- //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count);
-
- HashSet multiPredBlocks = ComputeMultiPredecessorBlocks(impl);
- Contract.Assert(cce.NonNullElements(multiPredBlocks));
- HashSet visitedBlocks = new HashSet();
- HashSet removedBlocks = new HashSet();
- Stack dfsStack = new Stack();
- dfsStack.Push(impl.Blocks[0]);
- while (dfsStack.Count > 0)
- {
- Block /*!*/
- b = dfsStack.Pop();
- Contract.Assert(b != null);
- if (visitedBlocks.Contains(b))
- {
- continue;
- }
-
- visitedBlocks.Add(b);
- if (b.TransferCmd == null)
- {
- continue;
- }
-
- if (b.TransferCmd is ReturnCmd)
- {
- continue;
- }
-
- Contract.Assert(b.TransferCmd is GotoCmd);
- GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
- if (gotoCmd.labelTargets == null)
- {
- continue;
- }
-
- if (gotoCmd.labelTargets.Count == 1)
- {
- Block /*!*/
- succ = cce.NonNull(gotoCmd.labelTargets[0]);
- if (!multiPredBlocks.Contains(succ))
- {
- foreach (Cmd /*!*/ cmd in succ.Cmds)
- {
- Contract.Assert(cmd != null);
- b.Cmds.Add(cmd);
- }
-
- b.TransferCmd = succ.TransferCmd;
- if (!b.tok.IsValid && succ.tok.IsValid)
- {
- b.tok = succ.tok;
- b.Label = succ.Label;
- }
-
- removedBlocks.Add(succ);
- dfsStack.Push(b);
- visitedBlocks.Remove(b);
- continue;
- }
- }
-
- foreach (Block /*!*/ succ in gotoCmd.labelTargets)
- {
- Contract.Assert(succ != null);
- dfsStack.Push(succ);
- }
- }
-
- List newBlocks = new List();
- foreach (Block /*!*/ b in impl.Blocks)
- {
- Contract.Assert(b != null);
- if (visitedBlocks.Contains(b) && !removedBlocks.Contains(b))
- {
- newBlocks.Add(b);
- }
- }
-
- impl.Blocks = newBlocks;
- foreach (Block b in impl.Blocks)
- {
- if (b.TransferCmd is ReturnCmd)
- {
- continue;
- }
-
- GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
- gotoCmd.labelNames = new List();
- foreach (Block succ in gotoCmd.labelTargets)
- {
- gotoCmd.labelNames.Add(succ.Label);
- }
- }
-
- // Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count);
- return impl;
- }
- }
-
- public class LiveVariableAnalysis
- {
- private CoreOptions options;
-
- public LiveVariableAnalysis(CoreOptions options)
- {
- this.options = options;
- }
-
- public static void ClearLiveVariables(Implementation impl)
- {
- Contract.Requires(impl != null);
- foreach (Block /*!*/ block in impl.Blocks)
- {
- Contract.Assert(block != null);
- block.liveVarsBefore = null;
- }
- }
-
- public void ComputeLiveVariables(Implementation impl)
- {
- Contract.Requires(impl != null);
- Microsoft.Boogie.Helpers.ExtraTraceInformation(options, "Starting live variable analysis");
- Graph dag = Program.GraphFromBlocks(impl.Blocks, false);
- IEnumerable sortedNodes;
- if (options.ModifyTopologicalSorting)
- {
- sortedNodes = dag.TopologicalSort(true);
- }
- else
- {
- sortedNodes = dag.TopologicalSort();
- }
-
- foreach (Block /*!*/ block in sortedNodes)
- {
- Contract.Assert(block != null);
- HashSet /*!*/
- liveVarsAfter = new HashSet();
-
- // The injected assumption variables should always be considered to be live.
- foreach (var v in impl.InjectedAssumptionVariables.Concat(impl.DoomedInjectedAssumptionVariables))
- {
- liveVarsAfter.Add(v);
- }
-
- if (block.TransferCmd is GotoCmd)
- {
- GotoCmd gotoCmd = (GotoCmd) block.TransferCmd;
- if (gotoCmd.labelTargets != null)
- {
- foreach (Block /*!*/ succ in gotoCmd.labelTargets)
- {
- Contract.Assert(succ != null);
- Contract.Assert(succ.liveVarsBefore != null);
- liveVarsAfter.UnionWith(succ.liveVarsBefore);
- }
- }
- }
-
- List cmds = block.Cmds;
- int len = cmds.Count;
- for (int i = len - 1; i >= 0; i--)
- {
- if (cmds[i] is CallCmd)
- {
- Procedure /*!*/
- proc = cce.NonNull(cce.NonNull((CallCmd /*!*/) cmds[i]).Proc);
- if (InterProcGenKill.HasSummary(proc.Name))
- {
- liveVarsAfter =
- InterProcGenKill.PropagateLiveVarsAcrossCall(options, cce.NonNull((CallCmd /*!*/) cmds[i]), liveVarsAfter);
- continue;
- }
- }
-
- Propagate(cmds[i], liveVarsAfter);
- }
-
- block.liveVarsBefore = liveVarsAfter;
- }
- }
-
- // perform in place update of liveSet
- public void Propagate(Cmd cmd, HashSet /*!*/ liveSet)
- {
- Contract.Requires(cmd != null);
- Contract.Requires(cce.NonNullElements(liveSet));
- if (cmd is AssignCmd)
- {
- AssignCmd /*!*/
- assignCmd = (AssignCmd) cce.NonNull(cmd);
- // I must first iterate over all the targets and remove the live ones.
- // After the removals are done, I must add the variables referred on
- // the right side of the removed targets
-
- AssignCmd simpleAssignCmd = assignCmd.AsSimpleAssignCmd;
- HashSet indexSet = new HashSet();
- int index = 0;
- foreach (AssignLhs /*!*/ lhs in simpleAssignCmd.Lhss)
- {
- Contract.Assert(lhs != null);
- SimpleAssignLhs salhs = lhs as SimpleAssignLhs;
- Contract.Assert(salhs != null);
- Variable var = salhs.DeepAssignedVariable;
- if (var != null && liveSet.Contains(var))
- {
- indexSet.Add(index);
- liveSet.Remove(var);
- }
-
- index++;
- }
-
- index = 0;
- foreach (Expr /*!*/ expr in simpleAssignCmd.Rhss)
- {
- Contract.Assert(expr != null);
- if (indexSet.Contains(index))
- {
- VariableCollector /*!*/
- collector = new VariableCollector();
- collector.Visit(expr);
- liveSet.UnionWith(collector.usedVars);
- }
-
- index++;
- }
- }
- else if (cmd is HavocCmd)
- {
- HavocCmd /*!*/
- havocCmd = (HavocCmd) cmd;
- foreach (IdentifierExpr /*!*/ expr in havocCmd.Vars)
- {
- Contract.Assert(expr != null);
- if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") &&
- expr.Decl.Name.StartsWith("a##cached##")))
- {
- liveSet.Remove(expr.Decl);
- }
- }
- }
- else if (cmd is PredicateCmd)
- {
- Contract.Assert((cmd is AssertCmd || cmd is AssumeCmd));
- PredicateCmd /*!*/
- predicateCmd = (PredicateCmd) cce.NonNull(cmd);
- if (predicateCmd.Expr is LiteralExpr)
- {
- LiteralExpr le = (LiteralExpr) predicateCmd.Expr;
- if (le.IsFalse)
- {
- liveSet.Clear();
- }
- }
- else
- {
- VariableCollector /*!*/
- collector = new VariableCollector();
- collector.Visit(predicateCmd.Expr);
- liveSet.UnionWith(collector.usedVars);
- }
- }
- else if (cmd is CommentCmd)
- {
- // comments are just for debugging and don't affect verification
- } else if (cmd is HideRevealCmd)
- {
- // reveal references no variables
- } else if (cmd is ChangeScope)
- {
- }
- else if (cmd is SugaredCmd)
- {
- SugaredCmd /*!*/
- sugCmd = (SugaredCmd) cce.NonNull(cmd);
- Propagate(sugCmd.GetDesugaring(options), liveSet);
- }
- else if (cmd is StateCmd)
- {
- StateCmd /*!*/
- stCmd = (StateCmd) cce.NonNull(cmd);
- List /*!*/
- cmds = cce.NonNull(stCmd.Cmds);
- int len = cmds.Count;
- for (int i = len - 1; i >= 0; i--)
- {
- Propagate(cmds[i], liveSet);
- }
-
- foreach (Variable /*!*/ v in stCmd.Locals)
- {
- Contract.Assert(v != null);
- liveSet.Remove(v);
- }
- }
- else
- {
- {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- }
- }
- }
-
- /*
- // An idempotent semiring interface
- abstract public class Weight {
- abstract public Weight! one();
- abstract public Weight! zero();
- abstract public Weight! extend(Weight! w1, Weight! w2);
- abstract public Weight! combine(Weight! w1, Weight! w2);
- abstract public Weight! isEqual(Weight! w);
- abstract public Weight! projectLocals()
- }
- */
-
- // Weight domain for LiveVariableAnalysis (Gen/Kill)
-
- public class GenKillWeight
- {
- // lambda S. (S - kill) union gen
- HashSet /*!*/
- gen;
-
- HashSet /*!*/
- kill;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(cce.NonNullElements(gen));
- Contract.Invariant(cce.NonNullElements(kill));
- Contract.Invariant(oneWeight != null);
- Contract.Invariant(zeroWeight != null);
- }
-
- bool isZero;
-
- public static GenKillWeight /*!*/
- oneWeight = new GenKillWeight(new HashSet(), new HashSet());
-
- public static GenKillWeight /*!*/
- zeroWeight = new GenKillWeight();
-
- // initializes to zero
- public GenKillWeight()
- {
- this.isZero = true;
- this.gen = new HashSet();
- this.kill = new HashSet();
- }
-
- public GenKillWeight(HashSet gen, HashSet kill)
- {
- Contract.Requires(cce.NonNullElements(gen));
- Contract.Requires(cce.NonNullElements(kill));
- Contract.Assert(gen != null);
- Contract.Assert(kill != null);
- this.gen = gen;
- this.kill = kill;
- this.isZero = false;
- }
-
- public static GenKillWeight one()
- {
- Contract.Ensures(Contract.Result() != null);
- return oneWeight;
- }
-
- public static GenKillWeight zero()
- {
- Contract.Ensures(Contract.Result() != null);
- return zeroWeight;
- }
-
- public static GenKillWeight extend(GenKillWeight w1, GenKillWeight w2)
- {
- Contract.Requires(w2 != null);
- Contract.Requires(w1 != null);
- Contract.Ensures(Contract.Result() != null);
- if (w1.isZero || w2.isZero)
- {
- return zero();
- }
-
- HashSet t = new HashSet(w2.gen);
- t.ExceptWith(w1.kill);
- HashSet g = new HashSet(w1.gen);
- g.UnionWith(t);
- HashSet k = new HashSet(w1.kill);
- k.UnionWith(w2.kill);
- return new GenKillWeight(g, k);
- //return new GenKillWeight(w1.gen.Union(w2.gen.Difference(w1.kill)), w1.kill.Union(w2.kill));
- }
-
- public static GenKillWeight combine(GenKillWeight w1, GenKillWeight w2)
- {
- Contract.Requires(w2 != null);
- Contract.Requires(w1 != null);
- Contract.Ensures(Contract.Result() != null);
- if (w1.isZero)
- {
- return w2;
- }
-
- if (w2.isZero)
- {
- return w1;
- }
-
- HashSet g = new HashSet(w1.gen);
- g.UnionWith(w2.gen);
- HashSet k = new HashSet(w1.kill);
- k.IntersectWith(w2.kill);
- return new GenKillWeight(g, k);
- //return new GenKillWeight(w1.gen.Union(w2.gen), w1.kill.Intersection(w2.kill));
- }
-
- public static GenKillWeight projectLocals(GenKillWeight w)
- {
- Contract.Requires(w != null);
- Contract.Ensures(Contract.Result() != null);
- HashSet gen = new HashSet();
- foreach (Variable v in w.gen)
- {
- if (isGlobal(v))
- {
- gen.Add(v);
- }
- }
-
- HashSet kill = new HashSet();
- foreach (Variable v in w.kill)
- {
- if (isGlobal(v))
- {
- kill.Add(v);
- }
- }
-
- return new GenKillWeight(gen, kill);
- }
-
- public static bool isEqual(GenKillWeight w1, GenKillWeight w2)
- {
- Contract.Requires(w2 != null);
- Contract.Requires(w1 != null);
- if (w1.isZero)
- {
- return w2.isZero;
- }
-
- if (w2.isZero)
- {
- return w1.isZero;
- }
-
- return (w1.gen.Equals(w2.gen) && w1.kill.Equals(w2.kill));
- }
-
- private static bool isGlobal(Variable v)
- {
- Contract.Requires(v != null);
- return (v is GlobalVariable);
- }
-
- [Pure]
- public override string ToString()
- {
- Contract.Ensures(Contract.Result() != null);
- return string.Format("({0},{1})", gen.ToString(), kill.ToString());
- }
-
- public HashSet /*!*/ getLiveVars()
- {
- Contract.Ensures(cce.NonNullElements(Contract.Result>()));
- return gen;
- }
-
- public HashSet /*!*/ getLiveVars(HashSet /*!*/ lv)
- {
- Contract.Requires(cce.NonNullElements(lv));
- Contract.Ensures(cce.NonNullElements(Contract.Result>()));
- HashSet temp = new HashSet(lv);
- temp.ExceptWith(kill);
- temp.UnionWith(gen);
- return temp;
- }
- }
-
- public class ImplementationControlFlowGraph
- {
- public Graph /*!*/
- graph;
-
- // Map from procedure to the list of blocks that call that procedure
- public Dictionary /*!*/> /*!*/
- procsCalled;
-
- public HashSet /*!*/
- nodes;
-
- public Dictionary /*!*/> /*!*/
- succEdges;
-
- public Dictionary /*!*/> /*!*/
- predEdges;
-
- private Dictionary /*!*/
- priority;
-
- public HashSet /*!*/
- srcNodes;
-
- public HashSet /*!*/
- exitNodes;
-
- public Dictionary /*!*/
- weightBefore;
-
- public Dictionary /*!*/
- weightAfter;
-
- public Dictionary /*!*/> /*!*/
- liveVarsAfter;
-
- public Dictionary /*!*/> /*!*/
- liveVarsBefore;
-
- public GenKillWeight /*!*/
- summary;
-
- private readonly CoreOptions options;
-
- public Implementation /*!*/
- impl;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(cce.NonNullElements(graph.Nodes));
- Contract.Invariant(cce.NonNullDictionaryAndValues(procsCalled));
- Contract.Invariant(cce.NonNullElements(nodes));
- Contract.Invariant(cce.NonNullDictionaryAndValues(succEdges));
- Contract.Invariant(cce.NonNullDictionaryAndValues(predEdges));
- Contract.Invariant(priority != null);
- Contract.Invariant(cce.NonNullElements(srcNodes));
- Contract.Invariant(cce.NonNullElements(exitNodes));
- Contract.Invariant(cce.NonNullDictionaryAndValues(weightBefore));
- Contract.Invariant(cce.NonNullDictionaryAndValues(weightAfter));
- Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsAfter));
- Contract.Invariant(cce.NonNullDictionaryAndValues(liveVarsBefore));
- Contract.Invariant(summary != null);
- Contract.Invariant(impl != null);
- }
-
-
- [NotDelayed]
- public ImplementationControlFlowGraph(CoreOptions options, Implementation impl)
- {
- Contract.Requires(impl != null);
- this.graph = new Graph();
- this.procsCalled = new Dictionary /*!*/>();
- this.nodes = new HashSet();
- this.succEdges = new Dictionary /*!*/>();
- this.predEdges = new Dictionary /*!*/>();
-
- this.priority = new Dictionary();
-
- this.srcNodes = new HashSet();
- this.exitNodes = new HashSet();
-
- this.weightBefore = new Dictionary();
- this.weightAfter = new Dictionary();
- this.liveVarsAfter = new Dictionary /*!*/>();
- this.liveVarsBefore = new Dictionary /*!*/>();
-
- summary = GenKillWeight.zero();
- this.options = options;
- this.impl = impl;
-
- Initialize(impl);
- }
-
- private void Initialize(Implementation impl)
- {
- Contract.Requires(impl != null);
- addSource(impl.Blocks[0]);
- graph.AddSource(impl.Blocks[0]);
-
- foreach (Block /*!*/ b in impl.Blocks)
- {
- Contract.Assert(b != null);
- if (b.TransferCmd is ReturnCmd)
- {
- exitNodes.Add(b);
- }
- else
- {
- GotoCmd gc = b.TransferCmd as GotoCmd;
- Contract.Assert(gc != null);
- Contract.Assert(gc.labelTargets != null);
- foreach (Block /*!*/ t in gc.labelTargets)
- {
- Contract.Assert(t != null);
- addEdge(b, t);
- graph.AddEdge(b, t);
- }
- }
-
- weightBefore[b] = GenKillWeight.zero();
- weightAfter[b] = GenKillWeight.zero();
-
- foreach (Cmd /*!*/ c in b.Cmds)
- {
- Contract.Assert(c != null);
- if (c is CallCmd)
- {
- CallCmd /*!*/
- cc = cce.NonNull((CallCmd /*!*/) c);
- Contract.Assert(cc.Proc != null);
- string /*!*/
- procName = cc.Proc.Name;
- Contract.Assert(procName != null);
- if (!procsCalled.ContainsKey(procName))
- {
- procsCalled.Add(procName, new List());
- }
-
- procsCalled[procName].Add(b);
- }
- }
- }
-
- graph.TarjanTopSort(out var acyclic, out var sortedNodes);
-
- if (!acyclic)
- {
- options.OutputWriter.WriteLine("Warning: graph is not a dag");
- }
-
- int num = sortedNodes.Count;
- foreach (Block /*!*/ b in sortedNodes)
- {
- Contract.Assert(b != null);
- priority.Add(b, num);
- num--;
- }
- }
-
- public int getPriority(Block b)
- {
- Contract.Requires(b != null);
- if (priority.ContainsKey(b))
- {
- return priority[b];
- }
-
- return Int32.MaxValue;
- }
-
- private void addSource(Block b)
- {
- Contract.Requires(b != null);
- registerNode(b);
- this.srcNodes.Add(b);
- }
-
- private void addExit(Block b)
- {
- Contract.Requires(b != null);
- registerNode(b);
- this.exitNodes.Add(b);
- }
-
- private void registerNode(Block b)
- {
- Contract.Requires(b != null);
- if (!succEdges.ContainsKey(b))
- {
- succEdges.Add(b, new HashSet());
- }
-
- if (!predEdges.ContainsKey(b))
- {
- predEdges.Add(b, new HashSet());
- }
-
- nodes.Add(b);
- }
-
- private void addEdge(Block src, Block tgt)
- {
- Contract.Requires(tgt != null);
- Contract.Requires(src != null);
- registerNode(src);
- registerNode(tgt);
-
- succEdges[src].Add(tgt);
- predEdges[tgt].Add(src);
- }
- }
-
// Interprocedural Gen/Kill Analysis
public class InterProcGenKill
{
diff --git a/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs b/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs
new file mode 100644
index 000000000..316cd11f2
--- /dev/null
+++ b/Source/Core/Analysis/LiveVariableAnalysis/LiveVariableAnalysis.cs
@@ -0,0 +1,213 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using Microsoft.Boogie.GraphUtil;
+
+namespace Microsoft.Boogie;
+
+public class LiveVariableAnalysis
+{
+ private CoreOptions options;
+
+ public LiveVariableAnalysis(CoreOptions options)
+ {
+ this.options = options;
+ }
+
+ public static void ClearLiveVariables(Implementation impl)
+ {
+ Contract.Requires(impl != null);
+ foreach (Block /*!*/ block in impl.Blocks)
+ {
+ Contract.Assert(block != null);
+ block.liveVarsBefore = null;
+ }
+ }
+
+ public void ComputeLiveVariables(Implementation impl)
+ {
+ Contract.Requires(impl != null);
+ Microsoft.Boogie.Helpers.ExtraTraceInformation(options, "Starting live variable analysis");
+ Graph dag = Program.GraphFromBlocks(impl.Blocks, false);
+ IEnumerable sortedNodes;
+ if (options.ModifyTopologicalSorting)
+ {
+ sortedNodes = dag.TopologicalSort(true);
+ }
+ else
+ {
+ sortedNodes = dag.TopologicalSort();
+ }
+
+ foreach (Block /*!*/ block in sortedNodes)
+ {
+ Contract.Assert(block != null);
+ HashSet /*!*/
+ liveVarsAfter = new HashSet();
+
+ // The injected assumption variables should always be considered to be live.
+ foreach (var v in impl.InjectedAssumptionVariables.Concat(impl.DoomedInjectedAssumptionVariables))
+ {
+ liveVarsAfter.Add(v);
+ }
+
+ if (block.TransferCmd is GotoCmd)
+ {
+ GotoCmd gotoCmd = (GotoCmd) block.TransferCmd;
+ if (gotoCmd.labelTargets != null)
+ {
+ foreach (Block /*!*/ succ in gotoCmd.labelTargets)
+ {
+ Contract.Assert(succ != null);
+ Contract.Assert(succ.liveVarsBefore != null);
+ liveVarsAfter.UnionWith(succ.liveVarsBefore);
+ }
+ }
+ }
+
+ List cmds = block.Cmds;
+ int len = cmds.Count;
+ for (int i = len - 1; i >= 0; i--)
+ {
+ if (cmds[i] is CallCmd)
+ {
+ Procedure /*!*/
+ proc = cce.NonNull(cce.NonNull((CallCmd /*!*/) cmds[i]).Proc);
+ if (InterProcGenKill.HasSummary(proc.Name))
+ {
+ liveVarsAfter =
+ InterProcGenKill.PropagateLiveVarsAcrossCall(options, cce.NonNull((CallCmd /*!*/) cmds[i]), liveVarsAfter);
+ continue;
+ }
+ }
+
+ Propagate(cmds[i], liveVarsAfter);
+ }
+
+ block.liveVarsBefore = liveVarsAfter;
+ }
+ }
+
+ // perform in place update of liveSet
+ public void Propagate(Cmd cmd, HashSet /*!*/ liveSet)
+ {
+ Contract.Requires(cmd != null);
+ Contract.Requires(cce.NonNullElements(liveSet));
+ if (cmd is AssignCmd)
+ {
+ AssignCmd /*!*/
+ assignCmd = (AssignCmd) cce.NonNull(cmd);
+ // I must first iterate over all the targets and remove the live ones.
+ // After the removals are done, I must add the variables referred on
+ // the right side of the removed targets
+
+ AssignCmd simpleAssignCmd = assignCmd.AsSimpleAssignCmd;
+ HashSet indexSet = new HashSet();
+ int index = 0;
+ foreach (AssignLhs /*!*/ lhs in simpleAssignCmd.Lhss)
+ {
+ Contract.Assert(lhs != null);
+ SimpleAssignLhs salhs = lhs as SimpleAssignLhs;
+ Contract.Assert(salhs != null);
+ Variable var = salhs.DeepAssignedVariable;
+ if (var != null && liveSet.Contains(var))
+ {
+ indexSet.Add(index);
+ liveSet.Remove(var);
+ }
+
+ index++;
+ }
+
+ index = 0;
+ foreach (Expr /*!*/ expr in simpleAssignCmd.Rhss)
+ {
+ Contract.Assert(expr != null);
+ if (indexSet.Contains(index))
+ {
+ VariableCollector /*!*/
+ collector = new VariableCollector();
+ collector.Visit(expr);
+ liveSet.UnionWith(collector.usedVars);
+ }
+
+ index++;
+ }
+ }
+ else if (cmd is HavocCmd)
+ {
+ HavocCmd /*!*/
+ havocCmd = (HavocCmd) cmd;
+ foreach (IdentifierExpr /*!*/ expr in havocCmd.Vars)
+ {
+ Contract.Assert(expr != null);
+ if (expr.Decl != null && !(QKeyValue.FindBoolAttribute(expr.Decl.Attributes, "assumption") &&
+ expr.Decl.Name.StartsWith("a##cached##")))
+ {
+ liveSet.Remove(expr.Decl);
+ }
+ }
+ }
+ else if (cmd is PredicateCmd)
+ {
+ Contract.Assert((cmd is AssertCmd || cmd is AssumeCmd));
+ PredicateCmd /*!*/
+ predicateCmd = (PredicateCmd) cce.NonNull(cmd);
+ if (predicateCmd.Expr is LiteralExpr)
+ {
+ LiteralExpr le = (LiteralExpr) predicateCmd.Expr;
+ if (le.IsFalse)
+ {
+ liveSet.Clear();
+ }
+ }
+ else
+ {
+ VariableCollector /*!*/
+ collector = new VariableCollector();
+ collector.Visit(predicateCmd.Expr);
+ liveSet.UnionWith(collector.usedVars);
+ }
+ }
+ else if (cmd is CommentCmd)
+ {
+ // comments are just for debugging and don't affect verification
+ } else if (cmd is HideRevealCmd)
+ {
+ // reveal references no variables
+ } else if (cmd is ChangeScope)
+ {
+ }
+ else if (cmd is SugaredCmd)
+ {
+ SugaredCmd /*!*/
+ sugCmd = (SugaredCmd) cce.NonNull(cmd);
+ Propagate(sugCmd.GetDesugaring(options), liveSet);
+ }
+ else if (cmd is StateCmd)
+ {
+ StateCmd /*!*/
+ stCmd = (StateCmd) cce.NonNull(cmd);
+ List /*!*/
+ cmds = cce.NonNull(stCmd.Cmds);
+ int len = cmds.Count;
+ for (int i = len - 1; i >= 0; i--)
+ {
+ Propagate(cmds[i], liveSet);
+ }
+
+ foreach (Variable /*!*/ v in stCmd.Locals)
+ {
+ Contract.Assert(v != null);
+ liveSet.Remove(v);
+ }
+ }
+ else
+ {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/Source/Core/Analysis/ModSetCollector.cs b/Source/Core/Analysis/ModSetCollector.cs
new file mode 100644
index 000000000..336781057
--- /dev/null
+++ b/Source/Core/Analysis/ModSetCollector.cs
@@ -0,0 +1,223 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie;
+
+public class ModSetCollector : ReadOnlyVisitor
+{
+ private CoreOptions options;
+ private Procedure enclosingProc;
+
+ private Dictionary> modSets;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(cce.NonNullDictionaryAndValues(modSets));
+ Contract.Invariant(Contract.ForAll(modSets.Values, v => cce.NonNullElements(v)));
+ }
+
+ public ModSetCollector(CoreOptions options)
+ {
+ this.options = options;
+ modSets = new Dictionary>();
+ }
+
+ private bool moreProcessingRequired;
+
+ public void DoModSetAnalysis(Program program)
+ {
+ Contract.Requires(program != null);
+
+ if (options.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);*/
+ }
+
+ HashSet implementedProcs = new HashSet();
+ foreach (var impl in program.Implementations)
+ {
+ if (impl.Proc != null)
+ {
+ implementedProcs.Add(impl.Proc);
+ }
+ }
+
+ foreach (var proc in program.Procedures)
+ {
+ if (!implementedProcs.Contains(proc))
+ {
+ enclosingProc = proc;
+ foreach (var expr in proc.Modifies)
+ {
+ Contract.Assert(expr != null);
+ ProcessVariable(expr.Decl);
+ }
+
+ enclosingProc = null;
+ }
+ else
+ {
+ modSets.Add(proc, new HashSet());
+ }
+ }
+
+ moreProcessingRequired = true;
+ while (moreProcessingRequired)
+ {
+ moreProcessingRequired = false;
+ this.Visit(program);
+ }
+
+ foreach (Procedure x in modSets.Keys)
+ {
+ x.Modifies = new List();
+ foreach (Variable v in modSets[x])
+ {
+ x.Modifies.Add(new IdentifierExpr(v.tok, v));
+ }
+ }
+
+#if DEBUG_PRINT
+ options.OutputWriter.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count);
+ foreach (Procedure/*!*/ x in modSets.Keys) {
+ Contract.Assert(x != null);
+ options.OutputWriter.Write("{0} : ", x.Name);
+ bool first = true;
+ foreach (Variable/*!*/ y in modSets[x]) {
+ Contract.Assert(y != null);
+ if (first)
+ first = false;
+ else
+ options.OutputWriter.Write(", ");
+ options.OutputWriter.Write("{0}", y.Name);
+ }
+ options.OutputWriter.WriteLine("");
+ options.OutputWriter
+#endif
+ }
+
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ enclosingProc = node.Proc;
+ Implementation /*!*/
+ ret = base.VisitImplementation(node);
+ Contract.Assert(ret != null);
+ enclosingProc = null;
+
+ return ret;
+ }
+
+ public override Cmd VisitAssignCmd(AssignCmd assignCmd)
+ {
+ Contract.Ensures(Contract.Result() != null);
+ Cmd ret = base.VisitAssignCmd(assignCmd);
+ foreach (AssignLhs lhs in assignCmd.Lhss)
+ {
+ Contract.Assert(lhs != null);
+ ProcessVariable(lhs.DeepAssignedVariable);
+ }
+
+ return ret;
+ }
+
+ public override Cmd VisitUnpackCmd(UnpackCmd unpackCmd)
+ {
+ Contract.Ensures(Contract.Result() != null);
+ Cmd ret = base.VisitUnpackCmd(unpackCmd);
+ foreach (var expr in unpackCmd.Lhs.Args)
+ {
+ ProcessVariable(((IdentifierExpr)expr).Decl);
+ }
+ return ret;
+ }
+
+ public override Cmd VisitHavocCmd(HavocCmd havocCmd)
+ {
+ Contract.Ensures(Contract.Result() != null);
+ Cmd ret = base.VisitHavocCmd(havocCmd);
+ foreach (IdentifierExpr expr in havocCmd.Vars)
+ {
+ Contract.Assert(expr != null);
+ ProcessVariable(expr.Decl);
+ }
+
+ return ret;
+ }
+
+ public override Cmd VisitCallCmd(CallCmd callCmd)
+ {
+ //Contract.Requires(callCmd != null);
+ Contract.Ensures(Contract.Result() != null);
+ Cmd ret = base.VisitCallCmd(callCmd);
+ foreach (IdentifierExpr ie in callCmd.Outs)
+ {
+ if (ie != null)
+ {
+ ProcessVariable(ie.Decl);
+ }
+ }
+
+ Procedure callee = callCmd.Proc;
+ if (callee == null)
+ {
+ return ret;
+ }
+
+ if (modSets.ContainsKey(callee))
+ {
+ foreach (Variable var in modSets[callee])
+ {
+ ProcessVariable(var);
+ }
+ }
+
+ return ret;
+ }
+
+ private void ProcessVariable(Variable var)
+ {
+ Procedure /*!*/
+ localProc = cce.NonNull(enclosingProc);
+ if (var == null)
+ {
+ return;
+ }
+
+ if (!(var is GlobalVariable))
+ {
+ return;
+ }
+
+ if (!modSets.ContainsKey(localProc))
+ {
+ modSets[localProc] = new HashSet();
+ }
+
+ if (modSets[localProc].Contains(var))
+ {
+ return;
+ }
+
+ moreProcessingRequired = true;
+ modSets[localProc].Add(var);
+ }
+
+ public override Expr VisitCodeExpr(CodeExpr node)
+ {
+ // don't go into the code expression, since it can only modify variables local to the code expression,
+ // and the mod-set analysis is interested in global variables
+ return node;
+ }
+}
\ No newline at end of file
diff --git a/Source/Core/Analysis/MutableVariableCollector.cs b/Source/Core/Analysis/MutableVariableCollector.cs
new file mode 100644
index 000000000..baa66a85e
--- /dev/null
+++ b/Source/Core/Analysis/MutableVariableCollector.cs
@@ -0,0 +1,31 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie;
+
+public class MutableVariableCollector : ReadOnlyVisitor
+{
+ public HashSet UsedVariables = new HashSet();
+
+ public void AddUsedVariables(HashSet usedVariables)
+ {
+ Contract.Requires(usedVariables != null);
+
+ foreach (var v in usedVariables)
+ {
+ UsedVariables.Add(v);
+ }
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ Contract.Ensures(Contract.Result() != null);
+
+ if (node.Decl != null && node.Decl.IsMutable)
+ {
+ UsedVariables.Add(node.Decl);
+ }
+
+ return base.VisitIdentifierExpr(node);
+ }
+}
\ No newline at end of file
diff --git a/Source/Core/Analysis/UnusedVarEliminator.cs b/Source/Core/Analysis/UnusedVarEliminator.cs
new file mode 100644
index 000000000..41291120c
--- /dev/null
+++ b/Source/Core/Analysis/UnusedVarEliminator.cs
@@ -0,0 +1,46 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie;
+
+public class UnusedVarEliminator : VariableCollector
+{
+ public static void Eliminate(Program program)
+ {
+ Contract.Requires(program != null);
+ UnusedVarEliminator elim = new UnusedVarEliminator();
+ elim.Visit(program);
+ }
+
+ private UnusedVarEliminator()
+ : base()
+ {
+ }
+
+ public override Implementation VisitImplementation(Implementation node)
+ {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result() != null);
+ //Console.WriteLine("Procedure {0}", node.Name);
+ Implementation /*!*/
+ impl = base.VisitImplementation(node);
+ Contract.Assert(impl != null);
+ //Console.WriteLine("Old number of local variables = {0}", impl.LocVars.Length);
+ List /*!*/
+ vars = new List();
+ foreach (Variable /*!*/ var in impl.LocVars)
+ {
+ Contract.Assert(var != null);
+ if (_usedVars.Contains(var))
+ {
+ vars.Add(var);
+ }
+ }
+
+ impl.LocVars = vars;
+ //Console.WriteLine("New number of local variables = {0}", impl.LocVars.Length);
+ //Console.WriteLine("---------------------------------");
+ _usedVars.Clear();
+ return impl;
+ }
+}
\ No newline at end of file
diff --git a/Source/Core/Analysis/VariableCollector.cs b/Source/Core/Analysis/VariableCollector.cs
new file mode 100644
index 000000000..9e996b71e
--- /dev/null
+++ b/Source/Core/Analysis/VariableCollector.cs
@@ -0,0 +1,82 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+
+namespace Microsoft.Boogie;
+
+public class VariableCollector : ReadOnlyVisitor
+{
+ private bool _ignoreOld;
+
+ protected HashSet _usedVars;
+
+ public IEnumerable usedVars
+ {
+ get { return _usedVars.AsEnumerable(); }
+ }
+
+ protected HashSet _oldVarsUsed;
+
+ public IEnumerable oldVarsUsed
+ {
+ get { return _oldVarsUsed.AsEnumerable(); }
+ }
+
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(cce.NonNullElements(_usedVars));
+ Contract.Invariant(cce.NonNullElements(_oldVarsUsed));
+ }
+
+ int insideOldExpr;
+
+ public VariableCollector(bool ignoreOld = false)
+ {
+ _ignoreOld = ignoreOld;
+ _usedVars = new HashSet();
+ _oldVarsUsed = new HashSet();
+ insideOldExpr = 0;
+ }
+
+ public override Expr VisitOldExpr(OldExpr node)
+ {
+ if (!_ignoreOld)
+ {
+ insideOldExpr++;
+ node.Expr = this.VisitExpr(node.Expr);
+ insideOldExpr--;
+ }
+ return node;
+ }
+
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ if (node.Decl != null)
+ {
+ _usedVars.Add(node.Decl);
+ if (insideOldExpr > 0)
+ {
+ _oldVarsUsed.Add(node.Decl);
+ }
+ }
+ return node;
+ }
+
+ public static IEnumerable Collect(Absy node, bool ignoreOld = false)
+ {
+ var collector = new VariableCollector(ignoreOld);
+ collector.Visit(node);
+ return collector.usedVars;
+ }
+
+ public static IEnumerable Collect(IEnumerable nodes, bool ignoreOld = false)
+ {
+ var collector = new VariableCollector(ignoreOld);
+ foreach (var node in nodes)
+ {
+ collector.Visit(node);
+ }
+ return collector.usedVars;
+ }
+}
\ No newline at end of file