Did some refactoring.

5 files changed, 55 insertions, 116 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 9fc301da..bb34c8f8 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -429,12 +429,8 @@ namespace Microsoft.Boogie {
           }

         }

       }

-      foreach (Declaration decl in prog.TopLevelDeclarations) {

-        Contract.Assert(decl != null);

-        Axiom ax = decl as Axiom;

-        if (ax != null) {

-          ctx.AddAxiom(ax, null);

-        }

+      foreach (var ax in prog.Axioms) {

+        ctx.AddAxiom(ax, null);

       }

       foreach (Declaration decl in prog.TopLevelDeclarations) {

         Contract.Assert(decl != null);

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 50a717f9..e74e0bbf 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1831,7 +1831,7 @@ namespace VC {
       // global variables

       lock (program.TopLevelDeclarations)

       {

-        foreach (Variable v in program.TopLevelDeclarations.OfType<Variable>())

+        foreach (var v in program.Variables)

         {

           if (!(v is Constant))

           {

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 9f39e46c..04b976ea 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -392,56 +392,42 @@ namespace Microsoft.Boogie
 

         void MarkAllFunctionImplementationsInline()

         {

-            foreach (var d in program.TopLevelDeclarations)

+            foreach (var func in program.Functions)

             {

-                var impl = d as Function;

-                if (impl != null)

+                if (func.Body == null && func.DefinitionAxiom != null)

                 {

-                    if (impl.Body == null && impl.DefinitionAxiom != null)

-                    {

-                        var def = impl.DefinitionAxiom.Expr as QuantifierExpr;

-                        var bod = def.Body as NAryExpr;

-                        impl.Body = bod.Args[1];

-                        impl.DefinitionAxiom = null;

-                    }

-                    if (impl.Body != null)

-                        if (impl.FindExprAttribute("inline") == null)

-                            impl.AddAttribute("inline", Expr.Literal(100));

+                    var def = func.DefinitionAxiom.Expr as QuantifierExpr;

+                    var bod = def.Body as NAryExpr;

+                    func.Body = bod.Args[1];

+                    func.DefinitionAxiom = null;

                 }

+                if (func.Body != null)

+                    if (func.FindExprAttribute("inline") == null)

+                        func.AddAttribute("inline", Expr.Literal(100));

             }

         }

 

         void InlineAll()

         {

-            foreach (var d in program.TopLevelDeclarations)

+            foreach (var impl in program.Implementations)

             {

-                var impl = d as Implementation;

-                if (impl != null)

-                {

-                    impl.OriginalBlocks = impl.Blocks;

-                    impl.OriginalLocVars = impl.LocVars;

-                    if(impl.Name != main_proc_name)

-                      if(impl.FindExprAttribute("inline") == null)

-                        impl.AddAttribute("inline", Expr.Literal(100));

-                }

+                impl.OriginalBlocks = impl.Blocks;

+                impl.OriginalLocVars = impl.LocVars;

+                if(impl.Name != main_proc_name)

+                  if(impl.FindExprAttribute("inline") == null)

+                    impl.AddAttribute("inline", Expr.Literal(100));

             }

-            var decls = program.TopLevelDeclarations;

-            foreach (var d in decls)

+            foreach (var impl in program.Implementations)

             {

-                var impl = d as Implementation;

-                if (impl != null && !impl.SkipVerification)

+                if (!impl.SkipVerification)

                 {

                     Inliner.ProcessImplementation(program, impl);

                 }

             }

-            foreach (var d in program.TopLevelDeclarations)

+            foreach (var impl in program.Implementations)

             {

-                var impl = d as Implementation;

-                if (impl != null)

-                {

-                    impl.OriginalBlocks = null;

-                    impl.OriginalLocVars = null;

-                }

+                impl.OriginalBlocks = null;

+                impl.OriginalLocVars = null;

             }

         }

 

@@ -650,12 +636,8 @@ namespace Microsoft.Boogie
         public void GenerateVCsForStratifiedInlining()

         {

             Contract.Requires(program != null);

-            foreach (Declaration decl in program.TopLevelDeclarations)

+            foreach (var impl in program.Implementations)

             {

-                Contract.Assert(decl != null);

-                Implementation impl = decl as Implementation;

-                if (impl == null)

-                    continue;

                 Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");

 

                 Procedure proc = cce.NonNull(impl.Proc);

@@ -713,10 +695,8 @@ namespace Microsoft.Boogie
 

             if (mode == Mode.Boogie) return;

 

-            foreach (var decl in program.TopLevelDeclarations)

+            foreach (var proc in program.Procedures)

             {

-                var proc = decl as Procedure;

-                if (proc == null) continue;

                 if (!proc.Name.StartsWith(recordProcName)) continue;

                 Contract.Assert(proc.InParams.Count == 1);

 

@@ -754,12 +734,8 @@ namespace Microsoft.Boogie
 			foreach (var node in rpfp.nodes)

 				pmap.Add ((node.Name as VCExprBoogieFunctionOp).Func.Name, node);

 			

-			foreach (Declaration decl in program.TopLevelDeclarations)

+			foreach (var impl in program.Implementations)

             {

-                Contract.Assert(decl != null);

-                Implementation impl = decl as Implementation;

-                if (impl == null)

-                    continue;

                 Contract.Assert(!impl.Name.StartsWith(recordProcName), "Not allowed to have an implementation for this guy");

 

                 Procedure proc = cce.NonNull(impl.Proc);

@@ -1400,25 +1376,17 @@ namespace Microsoft.Boogie
 

                 // find the name of the main procedure

                 main_proc_name = null; // default in case no entry point defined

-                foreach (var d in program.TopLevelDeclarations)

+                foreach (var impl in program.Implementations)

                 {

-                    var impl = d as Implementation;

-                    if (impl != null)

-                    {

-                        if (QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))

-                            main_proc_name = impl.Proc.Name;

-                    }

+                    if (QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))

+                        main_proc_name = impl.Proc.Name;

                 }

                 if (main_proc_name == null)

                 {

-                    foreach (var d in program.TopLevelDeclarations)

+                    foreach (var impl in program.Implementations)

                     {

-                        var impl = d as Implementation;

-                        if (impl != null)

-                        {

-                            if (impl.Proc.Name == "main" || impl.Proc.Name.EndsWith(".main"))

-                                main_proc_name = impl.Proc.Name;

-                        }

+                        if (impl.Proc.Name == "main" || impl.Proc.Name.EndsWith(".main"))

+                            main_proc_name = impl.Proc.Name;

                     }

                 }

                 if (main_proc_name == null)

@@ -1428,10 +1396,9 @@ namespace Microsoft.Boogie
                 {

                     InlineAll();

                     Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);

-                    foreach (var d in program.TopLevelDeclarations)

+                    foreach (var impl in program.Implementations)

                     {

-                        var impl = d as Implementation;

-                        if (impl != null && main_proc_name == impl.Proc.Name)

+                        if (main_proc_name == impl.Proc.Name)

                         {

                             Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);

                             CyclicLiveVariableAnalysis.ComputeLiveVariables(impl);

@@ -1444,15 +1411,11 @@ namespace Microsoft.Boogie
 

                     if (style == AnnotationStyle.Procedure || style == AnnotationStyle.Call)

                     {

-                        foreach (var proc in program.TopLevelDeclarations)

+                        foreach (var impl in program.Implementations)

                         {

-                            var impl = proc as Implementation;

-                            if (impl != null)

-                            {

-                                if (!QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))

-                                    AnnotateProcRequires(impl.Proc, impl, boogieContext);

-                                AnnotateProcEnsures(impl.Proc, impl, boogieContext);

-                            }

+                            if (!QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))

+                                AnnotateProcRequires(impl.Proc, impl, boogieContext);

+                            AnnotateProcEnsures(impl.Proc, impl, boogieContext);

                         }

                         if (style == AnnotationStyle.Call)

                         {

@@ -1463,40 +1426,30 @@ namespace Microsoft.Boogie
                     // must do this after annotating procedures, else calls

                     // will be prematurely desugared

                     

-                    foreach (var d in program.TopLevelDeclarations)

+                    foreach (var impl in program.Implementations)

                     {

-                        var impl = d as Implementation;

-                        if (impl != null)

-                        {

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

-                            CyclicLiveVariableAnalysis.ComputeLiveVariables(impl);

-                        }

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

+                        CyclicLiveVariableAnalysis.ComputeLiveVariables(impl);

                     }

 

 

                     if (style == AnnotationStyle.Flat || style == AnnotationStyle.Call)

                     {

-                        foreach (var proc in program.TopLevelDeclarations)

+                        foreach (var impl in program.Implementations)

                         {

-                            var impl = proc as Implementation;

-                            if (impl != null)

-                                AnnotateLoops(impl, boogieContext);

+                            AnnotateLoops(impl, boogieContext);

                         }

                     }

                     if (style == AnnotationStyle.Call)

                     {

                         Dictionary<string, bool> impls = new Dictionary<string, bool>();

-                        foreach (var proc in program.TopLevelDeclarations)

+                        foreach (var impl in program.Implementations)

                         {

-                            var impl = proc as Implementation;

-                            if (impl != null)

-                                impls.Add(impl.Proc.Name, true);

+                            impls.Add(impl.Proc.Name, true);

                         }

-                        foreach (var proc in program.TopLevelDeclarations)

+                        foreach (var impl in program.Implementations)

                         {

-                            var impl = proc as Implementation;

-                            if (impl != null)

-                                AnnotateCallSites(impl, boogieContext, impls);

+                            AnnotateCallSites(impl, boogieContext, impls);

                         }

                     }

                     if (style == AnnotationStyle.Flat)

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index fe40618e..5eed14fd 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -333,18 +333,14 @@ namespace VC {
       : base(program, logFilePath, appendLogFile, checkers) {

       implName2StratifiedInliningInfo = new Dictionary<string, StratifiedInliningInfo>();

       prover = ProverInterface.CreateProver(program, logFilePath, appendLogFile, CommandLineOptions.Clo.ProverKillTime);

-      foreach (Declaration decl in program.TopLevelDeclarations) {

-        Implementation impl = decl as Implementation;

-        if (impl == null) continue;

+      foreach (var impl in program.Implementations) {

         implName2StratifiedInliningInfo[impl.Name] = new StratifiedInliningInfo(impl, this);

       }

       GenerateRecordFunctions();

     }

 

     private void GenerateRecordFunctions() {

-      foreach (var decl in program.TopLevelDeclarations) {

-        var proc = decl as Procedure;

-        if (proc == null) continue;

+      foreach (var proc in program.Procedures) {

         if (!proc.Name.StartsWith(recordProcName)) continue;

         Contract.Assert(proc.InParams.Count == 1);

 

@@ -901,9 +897,7 @@ namespace VC {
 

       // Find all the boolean constants

       var allConsts = new HashSet<VCExprVar>();

-      foreach (var decl in program.TopLevelDeclarations) {

-        var constant = decl as Constant;

-        if (constant == null) continue;

+      foreach (var constant in program.Constants) {

         if (!allBoolVars.Contains(constant.Name)) continue;

         var v = prover.Context.BoogieExprTranslator.LookupVariable(constant);

         allConsts.Add(v);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 3735388c..758430bd 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2600,7 +2600,7 @@ namespace VC {
         // where clauses of global variables

         lock (program.TopLevelDeclarations)

         {

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

+          foreach (var gvar in program.GlobalVariables())

           {

             if (gvar != null && gvar.TypedIdent.WhereExpr != null)

             {

@@ -2755,15 +2755,11 @@ namespace VC {
     {

         // Construct the set of inlined procs in the original program

         var inlinedProcs = new HashSet<string>();

-        foreach (var decl in program.TopLevelDeclarations)

+        foreach (var proc in program.Procedures)

         {

-            if (decl is Procedure)

-            {  

-                if (!(decl is LoopProcedure))

-                {

-                    var p = decl as Procedure;

-                    inlinedProcs.Add(p.Name);

-                }

+            if (!(proc is LoopProcedure))

+            {

+                inlinedProcs.Add(proc.Name);

             }

         }