1. Fixed bug in StandardVisitor.ssc

2. Hoisted the call to inlining into BoogieDriver.ssc
3. Implemented a simple dead variable elimination
4. Perform inlining only for those procedures whose verification is not skipped

5 files changed, 52 insertions, 32 deletions

diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc
index 0632d83f..18d29c73 100644
--- a/Source/Core/Absy.ssc
+++ b/Source/Core/Absy.ssc
@@ -260,28 +260,6 @@ namespace Microsoft.Boogie
 

       AxiomExpander expander = new AxiomExpander(this, tc);

       expander.CollectExpansions();

-

-      if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {

-        bool inline = false;

-        foreach (Declaration d in TopLevelDeclarations) {

-          if (d.FindExprAttribute("inline") != null) inline = true;

-        }

-        if (inline) {

-          foreach (Declaration d in TopLevelDeclarations) {

-            Implementation impl = d as Implementation;

-            if (impl != null) {

-              impl.OriginalBlocks = impl.Blocks;

-              impl.OriginalLocVars = impl.LocVars;

-            }

-          }

-          foreach (Declaration d in TopLevelDeclarations) {

-            Implementation impl = d as Implementation;

-            if (impl != null) {

-              Inliner.ProcessImplementation(tc, this, impl);

-            }

-          }

-        }

-      }

     }

 

     public void ComputeStronglyConnectedComponents()

diff --git a/Source/Core/Core.sscproj b/Source/Core/Core.sscproj
index ef490ff2..d43dca98 100644
--- a/Source/Core/Core.sscproj
+++ b/Source/Core/Core.sscproj
@@ -210,6 +210,10 @@
                  SubType="Code"

                  RelPath="AssemblyInfo.ssc"

                  />

+        <File BuildAction="Compile"

+                 SubType="Code"

+                 RelPath="DeadVarElim.ssc"

+                 />

       </Include>

     </Files>

   </XEN>

diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc
new file mode 100644
index 00000000..897ca9e8
--- /dev/null
+++ b/Source/Core/DeadVarElim.ssc
@@ -0,0 +1,41 @@
+using System;

+using System.Collections.Generic;

+  

+namespace Microsoft.Boogie

+{

+  public class DeadVarEliminator : StandardVisitor {

+    public static void Eliminate(Program! program) {

+      DeadVarEliminator elim = new DeadVarEliminator();

+      elim.Visit(program);

+    }

+    

+    private System.Collections.Generic.Set<Variable!>! usedVars;

+  

+    private DeadVarEliminator() {

+      usedVars = new System.Collections.Generic.Set<Variable!>();

+    }

+      

+	public override Implementation! VisitImplementation(Implementation! node) {

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

+	  Implementation! impl = base.VisitImplementation(node);

+	  //Console.WriteLine("Old number of local variables = {0}", impl.LocVars.Length);

+	  Microsoft.Boogie.VariableSeq! vars = new Microsoft.Boogie.VariableSeq();

+	  foreach (Variable! var in impl.LocVars) {

+	    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 override Expr! VisitIdentifierExpr(IdentifierExpr! node)

+    {

+      if (node.Decl != null)

+        usedVars.Add(node.Decl);

+      return node;

+    }

+  }

+}
\ No newline at end of file
diff --git a/Source/Core/Inline.ssc b/Source/Core/Inline.ssc
index 13137927..6dff13c3 100644
--- a/Source/Core/Inline.ssc
+++ b/Source/Core/Inline.ssc
@@ -19,7 +19,6 @@ namespace Microsoft.Boogie {
   public class Inliner

   {   

     private InlineCallback inlineCallback;

-    private TypecheckingContext! checkingCtx;

   

     protected CodeCopier! codeCopier;

     

@@ -50,18 +49,17 @@ namespace Microsoft.Boogie {
       return prefix + "$" + formalName;

     }   

     

-    protected Inliner(TypecheckingContext! ctx, InlineCallback cb) {        

+    protected Inliner(InlineCallback cb) {        

       inlinedProcLblMap = new Dictionary<string!,int>();

       recursiveProcUnrollMap = new Dictionary<string!,int>();

       codeCopier = new CodeCopier();

       inlineCallback = cb;

-      checkingCtx = ctx;

     }

     

-    public static void ProcessImplementation(TypecheckingContext! ctx, Program! program, Implementation! impl, InlineCallback cb)

+    public static void ProcessImplementation(Program! program, Implementation! impl, InlineCallback cb)

       requires impl.Proc != null;

     {

-      Inliner inliner = new Inliner(ctx, cb);

+      Inliner inliner = new Inliner(cb);

       

       VariableSeq! newInParams = new VariableSeq(impl.InParams);

       VariableSeq! newOutParams = new VariableSeq(impl.OutParams);

@@ -91,11 +89,10 @@ namespace Microsoft.Boogie {
     }

     

     

-    public static void ProcessImplementation(TypecheckingContext! ctx, Program! program, Implementation! impl)

+    public static void ProcessImplementation(Program! program, Implementation! impl)

       requires impl.Proc != null;

     {

-      

-      ProcessImplementation(ctx, program, impl, null);

+      ProcessImplementation(program, impl, null);

     }

     

     protected void EmitImpl(Implementation! impl)

@@ -162,7 +159,7 @@ namespace Microsoft.Boogie {
             msg = p.Name + " -> " + msg;

           }

           msg += p.Name;

-          checkingCtx.Error(impl, "inlined procedure is recursive, call stack: {0}", msg);

+          //checkingCtx.Error(impl, "inlined procedure is recursive, call stack: {0}", msg);

         }

       }

     }

diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc
index a44290e8..99bac64e 100644
--- a/Source/Core/StandardVisitor.ssc
+++ b/Source/Core/StandardVisitor.ssc
@@ -196,7 +196,7 @@ namespace Microsoft.Boogie
     public virtual List<Declaration!>! VisitDeclarationList(List<Declaration!>! declarationList)

     {

       for (int i = 0, n = declarationList.Count; i < n; i++)

-        declarationList[i] = this.VisitDeclaration(declarationList[i]);

+        declarationList[i] = (Declaration!) this.Visit(declarationList[i]);

       return declarationList; 

     }

     public virtual DeclWithFormals! VisitDeclWithFormals(DeclWithFormals! node)