diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.ssc | 5 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.ssc | 2 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 6 | ||||
| -rw-r--r-- | Source/Core/DeadVarElim.ssc | 111 |
4 files changed, 114 insertions, 10 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc index 17132062..f68a9bbe 100644 --- a/Source/BoogieDriver/BoogieDriver.ssc +++ b/Source/BoogieDriver/BoogieDriver.ssc @@ -420,6 +420,11 @@ namespace Microsoft.Boogie // Eliminate dead variables
Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+ // Collect mod sets
+ if (CommandLineOptions.Clo.DoModSetAnalysis) {
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
+ }
+
// Coalesce blocks
if (CommandLineOptions.Clo.CoalesceBlocks) {
Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc index da4f4247..926724cb 100644 --- a/Source/Core/AbsyCmd.ssc +++ b/Source/Core/AbsyCmd.ssc @@ -696,7 +696,7 @@ namespace Microsoft.Boogie // VC generation and SCC computation
public BlockSeq! Predecessors;
- public Set liveVarsBefore;
+ public Set<Variable!> liveVarsBefore;
public bool IsLive(Variable! v) {
if (liveVarsBefore == null) return true;
return liveVarsBefore.Contains(v);
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index f9daaaf5..da8ee0fe 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -153,7 +153,8 @@ namespace Microsoft.Boogie public bool UseArrayTheory = false;
public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically
-
+
+ public bool DoModSetAnalysis = false;
public bool UseAbstractInterpretation = true; // true iff the user want to use abstract interpretation
public int /*0..9*/StepsBeforeWidening = 0; // The number of steps that must be done before applying a widen operator
invariant 0 <= StepsBeforeWidening && StepsBeforeWidening <= 9;
@@ -1183,7 +1184,8 @@ namespace Microsoft.Boogie ps.CheckBooleanFlag("z3types", ref Z3types) ||
ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||
ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||
- ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory)
+ ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||
+ ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis)
)
{
// one of the boolean flags matched
diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc index ba7f377b..506739bf 100644 --- a/Source/Core/DeadVarElim.ssc +++ b/Source/Core/DeadVarElim.ssc @@ -31,6 +31,103 @@ namespace Microsoft.Boogie }
}
+ public class ModSetCollector : StandardVisitor {
+ static Procedure proc;
+ static Dictionary<Procedure!, Set<Variable!>!>! modSets;
+ static bool moreProcessingRequired;
+
+ public static void DoModSetAnalysis(Program! program) {
+ int procCount = 0;
+ foreach (Declaration! decl in program.TopLevelDeclarations) {
+ if (decl is Procedure)
+ procCount++;
+ }
+ Console.WriteLine("Number of procedures = {0}", procCount);
+
+ modSets = new Dictionary<Procedure!, Set<Variable!>!>();
+
+ Set<Procedure!> implementedProcs = new Set<Procedure!> ();
+ foreach (Declaration! decl in program.TopLevelDeclarations) {
+ if (decl is Implementation) {
+ Implementation impl = (Implementation) decl;
+ if (impl.Proc != null)
+ implementedProcs.Add(impl.Proc);
+ }
+ }
+ foreach (Declaration! decl in program.TopLevelDeclarations) {
+ if (decl is Procedure && !implementedProcs.Contains((Procedure!) decl)) {
+ proc = (Procedure) decl;
+ foreach (IdentifierExpr! expr in proc.Modifies) {
+ ProcessVariable(expr.Decl);
+ }
+ proc = null;
+ }
+ }
+
+ moreProcessingRequired = true;
+ while (moreProcessingRequired) {
+ moreProcessingRequired = false;
+ ModSetCollector modSetCollector = new ModSetCollector();
+ modSetCollector.Visit(program);
+ }
+
+ procCount = 0;
+ foreach (Procedure! x in modSets.Keys) {
+ procCount++;
+ Console.Write("{0} : ", x.Name);
+ foreach (Variable! y in modSets[x]) {
+ Console.Write("{0}, ", y.Name);
+ }
+ Console.WriteLine("");
+ }
+ Console.WriteLine("Number of procedures with nonempty modsets = {0}", procCount);
+ }
+
+ public override Implementation! VisitImplementation(Implementation! node) {
+ proc = node.Proc;
+ Implementation! ret = base.VisitImplementation(node);
+ proc = null;
+
+ return ret;
+ }
+ public override Cmd! VisitAssignCmd(AssignCmd! assignCmd) {
+ Cmd ret = base.VisitAssignCmd(assignCmd);
+ foreach (AssignLhs! lhs in assignCmd.Lhss) {
+ ProcessVariable(lhs.DeepAssignedVariable);
+ }
+ return ret;
+ }
+ public override Cmd! VisitHavocCmd(HavocCmd! havocCmd) {
+ Cmd ret = base.VisitHavocCmd(havocCmd);
+ foreach (IdentifierExpr! expr in havocCmd.Vars) {
+ ProcessVariable(expr.Decl);
+ }
+ return ret;
+ }
+ public override Cmd! VisitCallCmd(CallCmd! callCmd) {
+ Cmd ret = base.VisitCallCmd(callCmd);
+ Procedure callee = callCmd.Proc;
+ if (callee != null && modSets.ContainsKey(callee)) {
+ foreach (Variable var in modSets[callee]) {
+ ProcessVariable(var);
+ }
+ }
+ return ret;
+ }
+ private static void ProcessVariable(Variable var) {
+ Procedure! localProc = (!)proc;
+ if (var == null) return;
+ if (!(var is GlobalVariable)) return;
+ if (var.Name == "alloc") return;
+ if (!modSets.ContainsKey(localProc)) {
+ modSets[localProc] = new Set<Variable!> ();
+ }
+ if (modSets[localProc].Contains(var)) return;
+ moreProcessingRequired = true;
+ modSets[localProc].Add(var);
+ }
+ }
+
public class VariableCollector : StandardVisitor {
public System.Collections.Generic.Set<Variable!>! usedVars;
public VariableCollector() {
@@ -121,7 +218,7 @@ namespace Microsoft.Boogie }
impl.Blocks = newBlocks;
- //Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count);
+ // Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count);
return impl;
}
}
@@ -152,13 +249,13 @@ namespace Microsoft.Boogie IEnumerable<Block> sortedNodes = dag.TopologicalSort();
foreach (Block! block in sortedNodes) {
- Set! liveVarsAfter = new Set();
+ Set<Variable!>! liveVarsAfter = new Set<Variable!>();
if (block.TransferCmd is GotoCmd) {
GotoCmd gotoCmd = (GotoCmd) block.TransferCmd;
if (gotoCmd.labelTargets != null) {
foreach (Block! succ in gotoCmd.labelTargets) {
assert succ.liveVarsBefore != null;
- liveVarsAfter.AddAll(succ.liveVarsBefore);
+ liveVarsAfter.AddRange(succ.liveVarsBefore);
}
}
}
@@ -174,7 +271,7 @@ namespace Microsoft.Boogie }
// perform in place update of liveSet
- private static void Propagate(Cmd! cmd, Set! liveSet) {
+ private static void Propagate(Cmd! cmd, Set<Variable!>! liveSet) {
if (cmd is AssignCmd) {
AssignCmd! assignCmd = (AssignCmd) cmd;
// I must first iterate over all the targets and remove the live ones.
@@ -199,7 +296,7 @@ namespace Microsoft.Boogie if (indexSet.Contains(index)) {
VariableCollector! collector = new VariableCollector();
collector.Visit(expr);
- liveSet.AddAll(collector.usedVars);
+ liveSet.AddRange(collector.usedVars);
AssignLhs lhs = assignCmd.Lhss[index];
if (lhs is MapAssignLhs) {
// If the target is a map, then all indices are also read
@@ -207,7 +304,7 @@ namespace Microsoft.Boogie foreach (Expr e in malhs.Indexes) {
VariableCollector! c = new VariableCollector();
c.Visit(e);
- liveSet.AddAll(c.usedVars);
+ liveSet.AddRange(c.usedVars);
}
}
}
@@ -231,7 +328,7 @@ namespace Microsoft.Boogie } else {
VariableCollector! collector = new VariableCollector();
collector.Visit(predicateCmd.Expr);
- liveSet.AddAll(collector.usedVars);
+ liveSet.AddRange(collector.usedVars);
}
} else if (cmd is CommentCmd) {
// comments are just for debugging and don't affect verification
|