added an option /doModSetAnalysis specially for Zvonimir

changed liveVarsBefore from Boogie.Set to Generics.Set

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