Did more refactoring and addressed several todos.

4 files changed, 156 insertions, 56 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 38a83b12..30333259 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -295,44 +295,13 @@ namespace Microsoft.Boogie {
   }

 

   public class Program : Absy {

-    [Rep]

-    private List<Declaration/*!*/>/*!*/ topLevelDeclarations;

-

-    public IEnumerable<Declaration> TopLevelDeclarations

-    {

-      get

-      {

-        return topLevelDeclarations;

-      }

-    }

-

-    public void AddTopLevelDeclaration(Declaration decl)

-    {

-      topLevelDeclarations.Add(decl);

-    }

-

-    public void AddTopLevelDeclarations(IEnumerable<Declaration> decls)

-    {

-      topLevelDeclarations.AddRange(decls);

-    }

-

-    public void RemoveTopLevelDeclarations(Predicate<Declaration> match)

-    {

-      topLevelDeclarations.RemoveAll(match);

-    }

-

-    public void ClearTopLevelDeclarations()

-    {

-      topLevelDeclarations.Clear();

-    }

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(TopLevelDeclarations));

-      Contract.Invariant(globals == null || cce.NonNullElements(globals));

+      Contract.Invariant(globalVariablesCache == null || cce.NonNullElements(globalVariablesCache));

     }

-

-

+    

     public Program()

       : base(Token.NoToken) {

       this.topLevelDeclarations = new List<Declaration>();

@@ -472,35 +441,164 @@ namespace Microsoft.Boogie {
       }

     }

 

+    [Rep]

+    private List<Declaration/*!*/>/*!*/ topLevelDeclarations;

+

+    public IEnumerable<Declaration> TopLevelDeclarations

+    {

+      get

+      {

+        return topLevelDeclarations;

+      }

+    }

+

+    public void AddTopLevelDeclaration(Declaration decl)

+    {

+      Contract.Requires(!TopLevelDeclarationsAreFrozen);

+

+      topLevelDeclarations.Add(decl);

+      this.globalVariablesCache = null;

+    }

+

+    public void AddTopLevelDeclarations(IEnumerable<Declaration> decls)

+    {

+      Contract.Requires(!TopLevelDeclarationsAreFrozen);

+

+      topLevelDeclarations.AddRange(decls);

+      this.globalVariablesCache = null;

+    }

+

+    public void RemoveTopLevelDeclarations(Predicate<Declaration> match)

+    {

+      Contract.Requires(!TopLevelDeclarationsAreFrozen);

+

+      topLevelDeclarations.RemoveAll(match);

+      this.globalVariablesCache = null;

+    }

+

+    public void ClearTopLevelDeclarations()

+    {

+      Contract.Requires(!TopLevelDeclarationsAreFrozen);

+

+      topLevelDeclarations.Clear();

+      this.globalVariablesCache = null;

+    }

+

+    bool topLevelDeclarationsAreFrozen;

+    public bool TopLevelDeclarationsAreFrozen { get { return topLevelDeclarationsAreFrozen; } }

+    public void FreezeTopLevelDeclarations()

+    {

+      topLevelDeclarationsAreFrozen = true;

+    }

+

+    Dictionary<string, Implementation> implementationsCache;

     public IEnumerable<Implementation> Implementations

     {

       get

       {

-        return TopLevelDeclarations.OfType<Implementation>();

+        if (implementationsCache != null)

+        {

+          return implementationsCache.Values;

+        }

+        var result = TopLevelDeclarations.OfType<Implementation>();

+        if (topLevelDeclarationsAreFrozen)

+        {

+          implementationsCache = result.ToDictionary(p => p.Id);

+        }

+        return result;

+      }

+    }

+

+    public Implementation FindImplementation(string id)

+    {

+      Implementation result = null;

+      if (implementationsCache != null && implementationsCache.TryGetValue(id, out result))

+      {

+        return result;

+      }

+      else

+      {

+        return Implementations.FirstOrDefault(i => i.Id == id);

       }

     }

 

+    IEnumerable<Axiom> axiomsCache;

     public IEnumerable<Axiom> Axioms

     {

       get

       {

-        return TopLevelDeclarations.OfType<Axiom>();

+        if (axiomsCache != null)

+        {

+          return axiomsCache;

+        }

+        var result = TopLevelDeclarations.OfType<Axiom>();

+        if (topLevelDeclarationsAreFrozen)

+        {

+          axiomsCache = result;

+        }

+        return result;

       }

     }

 

+    Dictionary<string, Procedure> proceduresCache;

     public IEnumerable<Procedure> Procedures

     {

       get

       {

-        return TopLevelDeclarations.OfType<Procedure>();

+        if (proceduresCache != null)

+        {

+          return proceduresCache.Values;

+        }

+        var result = TopLevelDeclarations.OfType<Procedure>();

+        if (topLevelDeclarationsAreFrozen)

+        {

+          proceduresCache = result.ToDictionary(p => p.Name);

+        }

+        return result;

+      }

+    }

+

+    public Procedure FindProcedure(string name)

+    {

+      Procedure result = null;

+      if (proceduresCache != null && proceduresCache.TryGetValue(name, out result))

+      {

+        return result;

+      }

+      else

+      {

+        return Procedures.FirstOrDefault(p => p.Name == name);

       }

     }

 

+    Dictionary<string, Function> functionsCache;

     public IEnumerable<Function> Functions

     {

       get

       {

-        return TopLevelDeclarations.OfType<Function>();

+        if (functionsCache != null)

+        {

+          return functionsCache.Values;

+        }

+        var result = TopLevelDeclarations.OfType<Function>();

+        if (topLevelDeclarationsAreFrozen)

+        {

+          functionsCache = result.ToDictionary(f => f.Name);

+        }

+        return result;

+      }

+    }

+

+    public Function FindFunction(string name)

+    {

+      Function result = null;

+      if (functionsCache != null && functionsCache.TryGetValue(name, out result))

+      {

+        return result;

+      }

+      else

+      {

+        return Functions.FirstOrDefault(f => f.Name == name);

       }

     }

     

@@ -520,6 +618,21 @@ namespace Microsoft.Boogie {
       }

     }

 

+    private List<GlobalVariable/*!*/> globalVariablesCache = null;

+    public IEnumerable<GlobalVariable/*!*/>/*!*/ GlobalVariables

+    {

+      get

+      {

+        Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<GlobalVariable>>()));

+

+        if (globalVariablesCache == null)

+        {

+          globalVariablesCache = TopLevelDeclarations.OfType<GlobalVariable>().ToList();

+        }

+        return globalVariablesCache;

+      }

+    }

+

     public IEnumerable<Block> Blocks()

     {

       return Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item);

@@ -1110,18 +1223,6 @@ namespace Microsoft.Boogie {
       return visitor.VisitProgram(this);

     }

 

-    private List<GlobalVariable/*!*/> globals = null;

-    public IEnumerable<GlobalVariable/*!*/>/*!*/ GlobalVariables() {

-      Contract.Ensures(cce.NonNullElements(Contract.Result<List<GlobalVariable>>()));

-      if (globals != null)

-        return globals;

-      globals = new List<GlobalVariable/*!*/>();

-      foreach (var gvar in TopLevelDeclarations.OfType<GlobalVariable>()) {

-        globals.Add(gvar);

-      }

-      return globals;

-    }

-

     private int invariantGenerationCounter = 0;

 

     public Constant MakeExistentialBoolean(int StageId) {

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index e6cf3e9d..e9975fe5 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -987,7 +987,7 @@ namespace Microsoft.Boogie {
       }

       // Return default: all globals and out params

       HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();

-      foreach (Variable/*!*/ v in prog.GlobalVariables()) {

+      foreach (Variable/*!*/ v in prog.GlobalVariables) {

         Contract.Assert(v != null);

         lv.Add(v);

       }

@@ -1007,7 +1007,7 @@ namespace Microsoft.Boogie {
       }

       // Return default: all globals and in params

       HashSet<Variable/*!*/>/*!*/ lv = new HashSet<Variable/*!*/>();

-      foreach (Variable/*!*/ v in prog.GlobalVariables()) {

+      foreach (Variable/*!*/ v in prog.GlobalVariables) {

         Contract.Assert(v != null);

         lv.Add(v);

       }

@@ -1275,7 +1275,7 @@ Contract.Assert(b != null);
 //Set<Variable!> lv = cfg.weightBefore[b].getLiveVars();

 b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];

 //foreach(GlobalVariable/*!*/

-      /* v in program.GlobalVariables()){Contract.Assert(v != null);

+      /* v in program.GlobalVariables){Contract.Assert(v != null);

 //  b.liveVarsBefore.Add(v);

 //}

 }

@@ -1482,7 +1482,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
         if (predicateCmd.Expr is LiteralExpr && prog != null && impl != null) {

           LiteralExpr le = (LiteralExpr)predicateCmd.Expr;

           if (le.IsFalse) {

-            var globals = prog.GlobalVariables();

+            var globals = prog.GlobalVariables;

             Contract.Assert(cce.NonNullElements(globals));

             foreach (Variable/*!*/ v in globals) {

               Contract.Assert(v != null);

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 6dd030e8..b275288a 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -640,8 +640,7 @@ namespace Microsoft.Boogie {
           var funCall = nAryExpr.Fun as FunctionCall;

           if (funCall != null)

           {

-            // TODO(wuestholz): Maybe we should speed up this lookup.

-            funCall.Func = Program.Functions.FirstOrDefault(f => f.Name == funCall.FunctionName);

+            funCall.Func = Program.FindFunction(funCall.FunctionName);

           }

         }

         return result;

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index fc2608b7..7472ec3d 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -108,7 +108,7 @@ namespace Microsoft.Boogie {
         {

             DistinguishPrefix(v.Name);

         }

-        foreach (var v in program.GlobalVariables())

+        foreach (var v in program.GlobalVariables)

         {

             DistinguishPrefix(v.Name);

         }