Did some refactoring.

4 files changed, 55 insertions, 72 deletions

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index c73758d8..e268a8d7 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -58,7 +58,7 @@ namespace Microsoft.Boogie.Houdini {
             this.constant2FuncCall = new Dictionary<string, NAryExpr>();

 

             // Find the existential functions

-            foreach (var func in program.TopLevelDeclarations.OfType<Function>()

+            foreach (var func in program.Functions

                 .Where(f => QKeyValue.FindBoolAttribute(f.Attributes, "existential")))

                 existentialFunctions.Add(func.Name, func);

 

@@ -104,7 +104,7 @@ namespace Microsoft.Boogie.Houdini {
             this.proverTime = TimeSpan.Zero;

             this.numProverQueries = 0;

 

-            program.TopLevelDeclarations.OfType<Implementation>()

+            program.Implementations

                 .Where(impl => !impl.SkipVerification)

                 .Iter(impl => name2Impl.Add(impl.Name, impl));

 

@@ -753,23 +753,19 @@ namespace Microsoft.Boogie.Houdini {
         {

             Graph<Implementation> callGraph = new Graph<Implementation>();

             Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();

-            foreach (Declaration decl in program.TopLevelDeclarations)

+            foreach (var proc in program.Procedures)

             {

-                Procedure proc = decl as Procedure;

-                if (proc == null) continue;

                 procToImpls[proc] = new HashSet<Implementation>();

             }

-            foreach (Declaration decl in program.TopLevelDeclarations)

+            foreach (var impl in program.Implementations)

             {

-                Implementation impl = decl as Implementation;

-                if (impl == null || impl.SkipVerification) continue;

+                if (impl.SkipVerification) continue;

                 callGraph.AddSource(impl);

                 procToImpls[impl.Proc].Add(impl);

             }

-            foreach (Declaration decl in program.TopLevelDeclarations)

+            foreach (var impl in program.Implementations)

             {

-                Implementation impl = decl as Implementation;

-                if (impl == null || impl.SkipVerification) continue;

+                if (impl.SkipVerification) continue;

                 foreach (Block b in impl.Blocks)

                 {

                     foreach (Cmd c in b.Cmds)

@@ -2139,8 +2135,7 @@ namespace Microsoft.Boogie.Houdini {
               });

 

             domains.Iter(tup => AbstractDomainFactory.Register(tup.Item1, tup.Item2));

-            program.TopLevelDeclarations.OfType<Function>()

-                .Iter(RegisterFunction);

+            program.Functions.Iter(RegisterFunction);

         }

 

         private static void RegisterFunction(Function func)

@@ -2227,8 +2222,7 @@ namespace Microsoft.Boogie.Houdini {
 

             name2Impl.Values.Iter(attachEnsures);

 

-            program.TopLevelDeclarations

-                .OfType<Implementation>()

+            program.Implementations

                 .Iter(impl => impl2Summary.Add(impl.Name, summaryClass.GetFlaseSummary(program, impl)));

 

             // Build call graph

@@ -2237,7 +2231,7 @@ namespace Microsoft.Boogie.Houdini {
             name2Impl.Values.Iter(impl => Succ.Add(impl, new HashSet<Implementation>()));

             name2Impl.Values.Iter(impl => Pred.Add(impl, new HashSet<Implementation>()));

 

-            foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())

+            foreach (var impl in program.Implementations)

             {

                 foreach (var blk in impl.Blocks)

                 {

@@ -2276,7 +2270,7 @@ namespace Microsoft.Boogie.Houdini {
             var copy = new Dictionary<string, Implementation>();

             if (WitnessFile != null)

             {

-                foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())

+                foreach (var impl in program.Implementations)

                 {

                     var nimpl = new Implementation(Token.NoToken, impl.Name, impl.TypeParameters,

                         impl.InParams, impl.OutParams, new List<Variable>(impl.LocVars), new List<Block>());

@@ -2365,7 +2359,7 @@ namespace Microsoft.Boogie.Houdini {
                 return Expr.True;

 

             var vars = new Dictionary<string, Expr>();

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

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

                 vars.Add(g.Name, Expr.Ident(g));

             foreach (var v in proc.InParams.OfType<Variable>())

                 vars.Add(v.Name, Expr.Ident(v));

@@ -2389,7 +2383,7 @@ namespace Microsoft.Boogie.Houdini {
             if (WitnessFile == null)

                 return;

 

-            foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())

+            foreach (var proc in program.Procedures)

             {

                 var nensures = new List<Ensures>();

                 proc.Ensures.OfType<Ensures>()

@@ -2411,7 +2405,7 @@ namespace Microsoft.Boogie.Houdini {
                 .Iter(decl => decls.Add(decl));

             program.TopLevelDeclarations = decls;

             var name2Proc = new Dictionary<string, Procedure>();

-            foreach (var proc in program.TopLevelDeclarations.OfType<Procedure>())

+            foreach (var proc in program.Procedures)

             {

                 name2Proc.Add(proc.Name, proc);

                 if (impl2Summary.ContainsKey(proc.Name))

@@ -2430,7 +2424,7 @@ namespace Microsoft.Boogie.Houdini {
             }

 

             // Replace SummaryPreds with their definition

-            foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())

+            foreach (var impl in program.Implementations)

             {

                 foreach (var blk in impl.Blocks)

                 {

@@ -2448,7 +2442,7 @@ namespace Microsoft.Boogie.Houdini {
                         var forold = new Dictionary<string, Expr>();

                         var always = new Dictionary<string, Expr>();

                         int i = 0;

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

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

                         {

                             forold.Add(g.Name, expr.Args[i]);

                             always.Add(g.Name, expr.Args[i]);

@@ -2556,23 +2550,19 @@ namespace Microsoft.Boogie.Houdini {
         {

             Graph<Implementation> callGraph = new Graph<Implementation>();

             Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();

-            foreach (Declaration decl in program.TopLevelDeclarations)

+            foreach (var proc in program.Procedures)

             {

-                Procedure proc = decl as Procedure;

-                if (proc == null) continue;

                 procToImpls[proc] = new HashSet<Implementation>();

             }

-            foreach (Declaration decl in program.TopLevelDeclarations)

+            foreach (var impl in program.Implementations)

             {

-                Implementation impl = decl as Implementation;

-                if (impl == null || impl.SkipVerification) continue;

+                if (impl.SkipVerification) continue;

                 callGraph.AddSource(impl);

                 procToImpls[impl.Proc].Add(impl);

             }

-            foreach (Declaration decl in program.TopLevelDeclarations)

+            foreach (var impl in program.Implementations)

             {

-                Implementation impl = decl as Implementation;

-                if (impl == null || impl.SkipVerification) continue;

+                if (impl.SkipVerification) continue;

                 foreach (Block b in impl.Blocks)

                 {

                     foreach (Cmd c in b.Cmds)

@@ -2753,7 +2743,7 @@ namespace Microsoft.Boogie.Houdini {
             var ret = new Dictionary<string, VCExpr>();

 

             var cnt = 0;

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

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

             {

                 ret.Add(string.Format("old({0})", g.Name), summaryPred[cnt]);

                 cnt++;

@@ -2768,7 +2758,7 @@ namespace Microsoft.Boogie.Houdini {
 

             // Fill up values of globals that are not modified

             cnt = 0;

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

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

             {

                 if (ret.ContainsKey(g.Name)) { cnt++; continue; }

 

@@ -2777,7 +2767,7 @@ namespace Microsoft.Boogie.Houdini {
             }

 

             // Constants

-            foreach (var c in program.TopLevelDeclarations.OfType<Constant>())

+            foreach (var c in program.Constants)

             {

                 var value = prover.Context.BoogieExprTranslator.Translate(Expr.Ident(c));

                 ret.Add(string.Format("{0}", c.Name), value);

@@ -2795,7 +2785,7 @@ namespace Microsoft.Boogie.Houdini {
             var implVars = impl2EndStateVars[impl.Name];

 

             var cnt = 0;

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

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

             {

                 ret.Add(string.Format("old({0})", g.Name), getValue(implVars[cnt], model));

                 cnt++;

@@ -2810,7 +2800,7 @@ namespace Microsoft.Boogie.Houdini {
 

             // Fill up values of globals that are not modified

             cnt = 0;

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

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

             {

                 if (ret.ContainsKey(g.Name)) { cnt++; continue; }

 

@@ -2819,7 +2809,7 @@ namespace Microsoft.Boogie.Houdini {
             }

 

             // Constants

-            foreach (var c in program.TopLevelDeclarations.OfType<Constant>())

+            foreach (var c in program.Constants)

             {

                 try

                 {

@@ -3231,7 +3221,7 @@ namespace Microsoft.Boogie.Houdini {
             boolConstants = new HashSet<string>();

             UpperCandidates = new Dictionary<Tuple<string, int>, List<PredicateAbsDisjunct>>();

 

-            program.TopLevelDeclarations.OfType<Constant>()

+            program.Constants

                 .Where(c => c.TypedIdent.Type.IsBool)

                 .Iter(c => boolConstants.Add(c.Name));

 

@@ -3241,7 +3231,7 @@ namespace Microsoft.Boogie.Houdini {
             var posPreT = new HashSet<int>();

             var tempP = new HashSet<Procedure>();

             foreach (var proc in

-                program.TopLevelDeclarations.OfType<Procedure>()

+                program.Procedures

                 .Where(proc => QKeyValue.FindBoolAttribute(proc.Attributes, "template")))

             {

                 tempP.Add(proc);

@@ -3274,7 +3264,7 @@ namespace Microsoft.Boogie.Houdini {
             program.TopLevelDeclarations.RemoveAll(decl => tempP.Contains(decl));

             var upperPreds = new Dictionary<string, List<Expr>>();

 

-            foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())

+            foreach (var impl in program.Implementations)

             {

                 PrePreds.Add(impl.Name, new List<NamedExpr>());

                 PostPreds.Add(impl.Name, new List<NamedExpr>());

@@ -3876,7 +3866,7 @@ namespace Microsoft.Boogie.Houdini {
             Simplify();

 

             // Find the free expressions

-            var proc = program.TopLevelDeclarations.OfType<Procedure>().FirstOrDefault(p => p.Name == procName);

+            var proc = program.Procedures.FirstOrDefault(p => p.Name == procName);

             Contract.Assert(proc != null);

             Expr freeSummary = Expr.True;

             foreach (var req in proc.Requires.OfType<Requires>().Where(req => req.Free))

@@ -4598,13 +4588,9 @@ namespace Microsoft.Boogie.Houdini {
         public static Dictionary<string, Implementation> nameImplMapping(Program p)

         {

             var m = new Dictionary<string, Implementation>();

-            foreach (Declaration d in p.TopLevelDeclarations)

+            foreach (var impl in p.Implementations)

             {

-                if (d is Implementation)

-                {

-                    Implementation impl = d as Implementation;

-                    m.Add(impl.Name, impl);

-                }

+                m.Add(impl.Name, impl);

             }

 

             return m;

diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs
index ea891dd6..9ff333dc 100644
--- a/Source/Houdini/CandidateDependenceAnalyser.cs
+++ b/Source/Houdini/CandidateDependenceAnalyser.cs
@@ -185,7 +185,7 @@ namespace Microsoft.Boogie.Houdini {
 

     private IEnumerable<CandidateInstance> CandidateInstances()

     {

-      foreach (var impl in prog.TopLevelDeclarations.OfType<Implementation>())

+      foreach (var impl in prog.Implementations)

       {

         foreach (var b in impl.Blocks) {

           foreach (Cmd cmd in b.Cmds)

@@ -202,7 +202,7 @@ namespace Microsoft.Boogie.Houdini {
         }

       }

 

-      foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>())

+      foreach (var proc in prog.Procedures)

       {

         foreach (Requires r in proc.Requires)

         {

@@ -351,7 +351,7 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     private IEnumerable<string> GetCandidates() {

-      return prog.TopLevelDeclarations.OfType<Variable>().Where(Item =>

+      return prog.Variables.Where(Item =>

         QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name);

     }

 

@@ -409,7 +409,7 @@ namespace Microsoft.Boogie.Houdini {
         #endregion

 

         #region Adapt candidate assertions to take account of stages

-        foreach (var b in prog.TopLevelDeclarations.OfType<Implementation>().Select(Item => Item.Blocks).SelectMany(Item => Item))

+        foreach (var b in prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item))

         {

             List<Cmd> newCmds = new List<Cmd>();

             foreach (var cmd in b.Cmds)

@@ -433,7 +433,7 @@ namespace Microsoft.Boogie.Houdini {
         #endregion

 

         #region Adapt candidate pre/postconditions to take account of stages

-        foreach (var p in prog.TopLevelDeclarations.OfType<Procedure>())

+        foreach (var p in prog.Procedures)

         {

 

           #region Handle the preconditions

@@ -633,7 +633,7 @@ namespace Microsoft.Boogie.Houdini {
       this.candidateToOccurences = new Dictionary<string,HashSet<object>>();

 

       // Add all candidate occurrences in blocks

-      foreach(Block b in prog.TopLevelDeclarations.OfType<Implementation>().Select(Item => Item.Blocks).SelectMany(Item => Item)) {

+      foreach(Block b in prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item)) {

         foreach(Cmd cmd in b.Cmds) {

           AssertCmd assertCmd = cmd as AssertCmd;

           if(assertCmd != null) {

@@ -646,7 +646,7 @@ namespace Microsoft.Boogie.Houdini {
       }

 

       // Add all candidate occurrences in preconditions

-      foreach(var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {

+      foreach(var proc in prog.Procedures) {

         foreach(Requires r in proc.Requires) {

           string c;

           if(Houdini.MatchCandidate(r.Condition, candidates, out c)) {

@@ -656,7 +656,7 @@ namespace Microsoft.Boogie.Houdini {
       }

 

       // Add all candidate occurrences in preconditions

-      foreach(var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {

+      foreach(var proc in prog.Procedures) {

         foreach(Ensures e in proc.Ensures) {

           string c;

           if(Houdini.MatchCandidate(e.Condition, candidates, out c)) {

diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs
index bfc96258..5c0f217f 100644
--- a/Source/Houdini/ConcurrentHoudini.cs
+++ b/Source/Houdini/ConcurrentHoudini.cs
@@ -46,7 +46,7 @@ namespace Microsoft.Boogie.Houdini
           RefutedAnnotation ra = null;
           Implementation refutationSite = null;
 
-          foreach (var r in program.TopLevelDeclarations.OfType<Implementation>()) {
+          foreach (var r in program.Implementations) {
             if (r.Name.Equals(refutedSharedAnnotations[key].RefutationSite.Name)) {
               refutationSite = r;
               break;
@@ -56,7 +56,7 @@ namespace Microsoft.Boogie.Houdini
 
           if (refutedSharedAnnotations[key].Kind == RefutedAnnotationKind.REQUIRES) {
             Procedure proc = null;
-            foreach (var p in program.TopLevelDeclarations.OfType<Procedure>()) {
+            foreach (var p in program.Procedures) {
               if (p.Name.Equals(refutedSharedAnnotations[key].CalleeProc.Name)) {
                 proc = p;
                 break;
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index e91d0528..6b1f2c39 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -399,14 +399,11 @@ namespace Microsoft.Boogie.Houdini {
 

     protected HashSet<Variable> CollectExistentialConstants() {

       HashSet<Variable> existentialConstants = new HashSet<Variable>();

-      foreach (Declaration decl in program.TopLevelDeclarations) {

-        Constant constant = decl as Constant;

-        if (constant != null) {

-          bool result = false;

-          if (constant.CheckBooleanAttribute("existential", ref result)) {

-            if (result == true)

-              existentialConstants.Add(constant);

-          }

+      foreach (var constant in program.Constants) {

+        bool result = false;

+        if (constant.CheckBooleanAttribute("existential", ref result)) {

+          if (result == true)

+            existentialConstants.Add(constant);

         }

       }

       return existentialConstants;

@@ -898,7 +895,7 @@ namespace Microsoft.Boogie.Houdini {
     private int NumberOfStages()

     {

       int result = 1;

-      foreach(var c in program.TopLevelDeclarations.OfType<Constant>()) {

+      foreach(var c in program.Constants) {

         result = Math.Max(result, 1 + QKeyValue.FindIntAttribute(c.Attributes, "stage_active", -1));

       }

       return result;

@@ -1103,7 +1100,7 @@ namespace Microsoft.Boogie.Houdini {
     protected Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)

     {

       Dictionary<Variable, bool> result = new Dictionary<Variable, bool>(currentHoudiniState.Assignment);

-      foreach (var c in program.TopLevelDeclarations.OfType<Constant>())

+      foreach (var c in program.Constants)

       {

         int stageActive = QKeyValue.FindIntAttribute(c.Attributes, "stage_active", -1);

         if (stageActive != -1)

@@ -1181,7 +1178,7 @@ namespace Microsoft.Boogie.Houdini {
 

       // Treat all assertions

       // TODO: do we need to also consider assumptions?

-      foreach (Block block in prog.TopLevelDeclarations.OfType<Implementation>().Select(item => item.Blocks).SelectMany(item => item)) {

+      foreach (Block block in prog.Implementations.Select(item => item.Blocks).SelectMany(item => item)) {

         List<Cmd> newCmds = new List<Cmd>();

         foreach (Cmd cmd in block.Cmds) {

           string c;

@@ -1190,7 +1187,7 @@ namespace Microsoft.Boogie.Houdini {
             var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];

             if (currentHoudiniState.Assignment[cVar]) {

               Dictionary<Variable, Expr> cToTrue = new Dictionary<Variable, Expr>();

-              Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];

+              Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];

               cToTrue[cVarProg] = Expr.True;

               newCmds.Add(new AssumeCmd(assertCmd.tok,

                 Substituter.Apply(Substituter.SubstitutionFromHashtable(cToTrue), assertCmd.Expr),

@@ -1204,14 +1201,14 @@ namespace Microsoft.Boogie.Houdini {
         block.Cmds = newCmds;

       }

 

-      foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {

+      foreach (var proc in prog.Procedures) {

         List<Requires> newRequires = new List<Requires>();

         foreach (Requires r in proc.Requires) {

           string c;

           if (MatchCandidate(r.Condition, out c)) {

             var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];

             if (currentHoudiniState.Assignment[cVar]) {

-              Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];

+              Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];

               Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

               subst[cVarProg] = Expr.True;

               newRequires.Add(new Requires(Token.NoToken, true,

@@ -1231,7 +1228,7 @@ namespace Microsoft.Boogie.Houdini {
           if (MatchCandidate(e.Condition, out c)) {

             var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];

             if (currentHoudiniState.Assignment[cVar]) {

-              Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];

+              Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];

               Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

               subst[cVarProg] = Expr.True;

               newEnsures.Add(new Ensures(Token.NoToken, true,