1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a linear procedure call

2. Inlining requires two fields OriginalBlocks and OriginalLocVars in Implementation.  These are set just before inlining is called and now I reset them to null afterwards to help garbage collection.
3. Clear live variables right after passification again to help garbage collection.

5 files changed, 35 insertions, 4 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc
index 7b22d6fe..f58dbcfd 100644
--- a/Source/BoogieDriver/BoogieDriver.ssc
+++ b/Source/BoogieDriver/BoogieDriver.ssc
@@ -446,6 +446,13 @@ namespace Microsoft.Boogie
               Inliner.ProcessImplementation(program, impl);

             }

           }

+          foreach (Declaration d in TopLevelDeclarations) {

+            Implementation impl = d as Implementation;

+            if (impl != null) {

+              impl.OriginalBlocks = null;

+              impl.OriginalLocVars = null;

+            }

+          }

         }

       }

       return PipelineOutcome.Done;

diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc
index e60a59c3..ba7f377b 100644
--- a/Source/Core/DeadVarElim.ssc
+++ b/Source/Core/DeadVarElim.ssc
@@ -76,6 +76,9 @@ namespace Microsoft.Boogie
     }

     

     public override Implementation! VisitImplementation(Implementation! impl) {

+      //Console.WriteLine("Procedure {0}", impl.Name);

+      //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count);

+      

       Set<Block!> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);

       Set<Block!> visitedBlocks = new Set<Block!>();

       Set<Block!> removedBlocks = new Set<Block!>();

@@ -117,11 +120,19 @@ namespace Microsoft.Boogie
         }

       }

       impl.Blocks = newBlocks;

+      

+      //Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count);

       return impl;

     }

   }

   

   public class LiveVariableAnalysis {

+    public static void ClearLiveVariables(Implementation! impl) {

+      foreach (Block! block in impl.Blocks) {

+        block.liveVarsBefore = null;

+      }

+    }

+    

 	public static void ComputeLiveVariables(Implementation! impl) {

 	  Microsoft.Boogie.Helpers.ExtraTraceInformation("Starting live variable analysis");

 	  Graphing.Graph<Block> dag = new Graph<Block>();

diff --git a/Source/Provers/Z3/ProverInterface.ssc b/Source/Provers/Z3/ProverInterface.ssc
index c3a61fe3..9a28eb42 100644
--- a/Source/Provers/Z3/ProverInterface.ssc
+++ b/Source/Provers/Z3/ProverInterface.ssc
@@ -169,6 +169,13 @@ namespace Microsoft.Boogie.Z3
       allVars.Add(furtherVar);

       return new Z3LineariserOptions(AsTerm, opts, allVars);

     }

+    

+    public override LineariserOptions! AddLetVariables(List<VCExprVar!>! furtherVars) {

+      List<VCExprVar!>! allVars = new List<VCExprVar!> ();

+      allVars.AddRange(LetVariables);

+      allVars.AddRange(furtherVars);

+      return new Z3LineariserOptions(AsTerm, opts, allVars);

+    }

   }

 

   // -----------------------------------------------------------------------------------------------

diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc
index 289dff87..52681162 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.ssc
+++ b/Source/VCExpr/SimplifyLikeLineariser.ssc
@@ -47,6 +47,10 @@ namespace Microsoft.Boogie.VCExprAST
       return this;

     }

 

+	public virtual LineariserOptions! AddLetVariables(List<VCExprVar!>! furtherVars) {

+      return this;

+    }

+    

     private static readonly List<VCExprVar!>! EmptyList = new List<VCExprVar!>();

 

     public bool NativeBv { get {

@@ -477,10 +481,8 @@ namespace Microsoft.Boogie.VCExprAST
 

       wr.Write("(LET (");

 

-      LineariserOptions! optionsWithVars = options;

-      foreach (VCExprVar! var in node.BoundVars)

-        optionsWithVars = optionsWithVars.AddLetVariable(var);

-

+      LineariserOptions! optionsWithVars = options.AddLetVariables(node.BoundVars);

+	  

       string s = "(";

       foreach (VCExprLetBinding! b in node) {

         wr.Write(s);

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index a9b47222..cdc6dde2 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -1759,6 +1759,10 @@ namespace VC
 	  

       Convert2PassiveCmd(impl);

       

+      if (CommandLineOptions.Clo.LiveVariableAnalysis) {

+	    Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);

+	  }

+	  

       #region Peep-hole optimizations

       if (CommandLineOptions.Clo.RemoveEmptyBlocks){

         #region Get rid of empty blocks