Simplified the translator by merging the ToplevelTraverser, ClassTraverser, and MethodTraverser into one traverser: MetadataTraverser. It will have to do a little more work to keep its state consistent (like saving any type-related state before traversing a nested type definition), but it seems worth it.

10 files changed, 27 insertions, 541 deletions

diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index e566adff..0a7d6d55 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -109,13 +109,11 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="CLRSemantics.cs" />

+    <Compile Include="MetadataTraverser.cs" />

     <Compile Include="Prelude.cs" />

     <Compile Include="ExpressionTraverser.cs" />

-    <Compile Include="ClassTraverser.cs" />

-    <Compile Include="MethodTraverser.cs" />

     <Compile Include="StatementTraverser.cs" />

     <Compile Include="Program.cs" />

-    <Compile Include="ToplevelTraverser.cs" />

     <Compile Include="TranslationException.cs" />

     <Compile Include="TranslationHelper.cs" />

     <Compile Include="TraverserFactory.cs" />

diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs
index f52b2006..c9f09f5f 100644
--- a/BCT/BytecodeTranslator/CLRSemantics.cs
+++ b/BCT/BytecodeTranslator/CLRSemantics.cs
@@ -37,7 +37,7 @@ namespace BytecodeTranslator {
 

         var tok = TranslationHelper.CciLocationToBoogieToken(division.Locations);

 

-        var loc = this.StmtTraverser.MethodTraverser.CreateFreshLocal(division.RightOperand.Type);

+        var loc = this.StmtTraverser.MetadataTraverser.CreateFreshLocal(division.RightOperand.Type);

         var locExpr = Bpl.Expr.Ident(loc);

         var storeLocal = Bpl.Cmd.SimpleAssign(tok, locExpr, rexp);

         this.StmtTraverser.StmtBuilder.Add(storeLocal);

diff --git a/BCT/BytecodeTranslator/ClassTraverser.cs b/BCT/BytecodeTranslator/ClassTraverser.cs
deleted file mode 100644
index ce72c9ba..00000000
--- a/BCT/BytecodeTranslator/ClassTraverser.cs
+++ /dev/null
@@ -1,85 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

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

-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-

-using Microsoft.Cci;

-using Microsoft.Cci.MetadataReader;

-using Microsoft.Cci.MutableCodeModel;

-using Microsoft.Cci.Contracts;

-using Microsoft.Cci.ILToCodeModel;

-

-using Bpl = Microsoft.Boogie;

-

-namespace BytecodeTranslator {

-  /// <summary>

-  /// 

-  /// </summary>

-  public class ClassTraverser : BaseCodeAndContractTraverser {

-

-    public readonly TraverserFactory factory;

-

-    public readonly ToplevelTraverser ToplevelTraverser;

-

-    private Dictionary<IFieldDefinition, Bpl.GlobalVariable> fieldVarMap = new Dictionary<IFieldDefinition, Microsoft.Boogie.GlobalVariable>();

-

-    private Dictionary<IMethodDefinition, MethodTraverser> methodMap = new Dictionary<IMethodDefinition, MethodTraverser>();

-

-    // TODO: (mschaef) just a stub

-    public readonly Bpl.Variable ThisVariable = TranslationHelper.TempThisVar();

-

-    public readonly Bpl.Variable HeapVariable = TranslationHelper.TempHeapVar();

-

-    public ClassTraverser(TraverserFactory factory, IContractProvider cp, ToplevelTraverser tlTraverser)

-      : base(cp) {

-      this.factory = factory;

-      ToplevelTraverser = tlTraverser;

-    }

-

-    public Bpl.Variable FindOrCreateFieldVariable(IFieldDefinition field) {

-      Bpl.GlobalVariable v;

-      if (!fieldVarMap.TryGetValue(field, out v)) {

-        string fieldname = field.ContainingTypeDefinition.ToString() + "." + field.Name.Value;

-        Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(field.Locations);

-        Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);

-        Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);

-

-        v = new Bpl.GlobalVariable(tok,tident);

-        fieldVarMap.Add(field, v);

-        ToplevelTraverser.TranslatedProgram.TopLevelDeclarations.Add(new Bpl.Constant(tok, tident, true));

-      }

-      return v;

-    }

-

-

-    /// <summary>

-    /// 

-    /// </summary>

-    /// <param name="method"></param>

-    public override void Visit(IMethodDefinition method) {

-      // check if it's static and so on

-      MethodTraverser mt;

-      if (!methodMap.TryGetValue(method, out mt)) {

-        mt = this.factory.MakeMethodTraverser(this, this.contractProvider);

-        this.methodMap.Add(method, mt);

-      }

-      mt.Visit(method);

-    }

-

-    public override void Visit(IFieldDefinition fieldDefinition) {

-      this.FindOrCreateFieldVariable(fieldDefinition);

-    }

-

-    public override void Visit(ITypeInvariant typeInvariant) {

-      // Todo: Not implemented

-      base.Visit(typeInvariant);

-    }

-

-  }

-

-}

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index beeb5cb1..a8f9a758 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -52,12 +52,12 @@ namespace BytecodeTranslator {
     public override void Visit(IAddressableExpression addressableExpression) {

       ILocalDefinition/*?*/ local = addressableExpression.Definition as ILocalDefinition;

       if (local != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindOrCreateLocalVariable(local)));

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindOrCreateLocalVariable(local)));

         return;

       }

       IParameterDefinition/*?*/ param = addressableExpression.Definition as IParameterDefinition;

       if (param != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindParameterVariable(param)));

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindParameterVariable(param)));

         return;

       }

       IFieldReference/*?*/ field = addressableExpression.Definition as IFieldReference;

@@ -125,7 +125,7 @@ namespace BytecodeTranslator {
       #region LocalDefinition

       ILocalDefinition/*?*/ local = targetExpression.Definition as ILocalDefinition;

       if (local != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindOrCreateLocalVariable(local)));

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindOrCreateLocalVariable(local)));

         return;

       }

       #endregion

@@ -133,7 +133,7 @@ namespace BytecodeTranslator {
       #region ParameterDefenition

       IParameterDefinition param = targetExpression.Definition as IParameterDefinition;

       if (param != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindParameterVariable(param)));

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindParameterVariable(param)));

         return;

       }

       #endregion

@@ -156,7 +156,7 @@ namespace BytecodeTranslator {
     

     public override void Visit(IThisReference thisReference) {

       TranslatedExpressions.Push(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(thisReference.Locations),

-        this.StmtTraverser.MethodTraverser.ClassTraverser.ThisVariable));

+        this.StmtTraverser.MetadataTraverser.ThisVariable));

     }

 

     public override void Visit(IBoundExpression boundExpression) {

@@ -168,7 +168,7 @@ namespace BytecodeTranslator {
       #region LocalDefinition

       ILocalDefinition local = boundExpression.Definition as ILocalDefinition;

       if (local != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindOrCreateLocalVariable(local)));

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindOrCreateLocalVariable(local)));

         return;

       }

       #endregion

@@ -176,7 +176,7 @@ namespace BytecodeTranslator {
       #region ParameterDefiniton

       IParameterDefinition param = boundExpression.Definition as IParameterDefinition;

       if (param != null) {

-        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.FindParameterVariable(param)));

+        TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MetadataTraverser.FindParameterVariable(param)));

         return;

       }

       #endregion

@@ -248,9 +248,7 @@ namespace BytecodeTranslator {
 

       //TranslatedExpressions.Push(Bpl.Expr.Ident(this.StmtTraverser.MethodTraverser.ClassTraverser.FindOrCreateFieldVariable(field.ResolvedField))

       TranslatedExpressions.Push( Bpl.Expr.Ident( 

-        this.StmtTraverser.MethodTraverser.ClassTraverser.ToplevelTraverser.FindOrCreateClassField(

-        field.ContainingType.ResolvedType, 

-        field.ResolvedField) ) );

+        this.StmtTraverser.MetadataTraverser.FindOrCreateFieldVariable(field.ResolvedField) ) );

 

       this.Visit(instance);

 

@@ -347,7 +345,7 @@ namespace BytecodeTranslator {
         #endregion

 

         if (methodCall.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

-          Bpl.Variable v = this.StmtTraverser.MethodTraverser.CreateFreshLocal(methodCall.Type.ResolvedType);

+          Bpl.Variable v = this.StmtTraverser.MetadataTraverser.CreateFreshLocal(methodCall.Type.ResolvedType);

           outvars.Add(new Bpl.IdentifierExpr(cloc, v));

           TranslatedExpressions.Push(new Bpl.IdentifierExpr(cloc, v));

         }

@@ -531,11 +529,11 @@ namespace BytecodeTranslator {
     }

     

     public override void Visit(IReturnValue returnValue) {

-      if (this.StmtTraverser.MethodTraverser.RetVariable == null) {

+      if (this.StmtTraverser.MetadataTraverser.RetVariable == null) {

         throw new TranslationException(String.Format("Don't know what to do with return value {0}", returnValue.ToString()));

       }

       TranslatedExpressions.Push(new Bpl.IdentifierExpr(TranslationHelper.CciLocationToBoogieToken(returnValue.Locations),

-        this.StmtTraverser.MethodTraverser.RetVariable));

+        this.StmtTraverser.MetadataTraverser.RetVariable));

 

     }

     #endregion

diff --git a/BCT/BytecodeTranslator/MethodTraverser.cs b/BCT/BytecodeTranslator/MethodTraverser.cs
deleted file mode 100644
index 7a7170e9..00000000
--- a/BCT/BytecodeTranslator/MethodTraverser.cs
+++ /dev/null
@@ -1,341 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

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

-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-

-using Microsoft.Cci;

-using Microsoft.Cci.MetadataReader;

-using Microsoft.Cci.MutableCodeModel;

-using Microsoft.Cci.Contracts;

-using Microsoft.Cci.ILToCodeModel;

-

-using Bpl = Microsoft.Boogie;

-

-namespace BytecodeTranslator {

-  public class MethodTraverser : BaseCodeAndContractTraverser {

-

-    public readonly TraverserFactory factory;

-

-    public readonly ClassTraverser ClassTraverser;

-

-    private Bpl.Procedure procedure;

-

-    public Bpl.Variable RetVariable;

-

-    public List<MethodParameter> OutVars = new List<MethodParameter>();

-

-    public Bpl.Variable HeapVariable;        

-

-    private Dictionary<ILocalDefinition, Bpl.LocalVariable> localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();

-

-    public class MethodParameter {

-      public MethodParameter() {

-        localParameter = null;

-        inParameterCopy = null;

-        outParameterCopy = null;

-      }

-

-      public Bpl.Formal localParameter;

-      public Bpl.Formal inParameterCopy;

-      public Bpl.Formal outParameterCopy;

-    }

-

-    private Dictionary<IParameterDefinition, MethodParameter> formalMap = new Dictionary<IParameterDefinition, MethodParameter>();

-

-    #region Helper Functions

-    /// <summary>

-    /// 

-    /// </summary>

-    /// <param name="local"></param>

-    /// <returns></returns>

-    public Bpl.Variable FindOrCreateLocalVariable(ILocalDefinition local) {

-      Bpl.LocalVariable v;

-      Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(local.Locations);

-      Bpl.Type t = TranslationHelper.CciTypeToBoogie(local.Type.ResolvedType);

-      if (!localVarMap.TryGetValue(local, out v)) {

-        v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, local.Name.Value, t));

-        localVarMap.Add(local, v);

-      }

-      return v;

-    }

-

-    /// <summary>

-    /// Creates a fresh local var of the given Type and adds it to the

-    /// Bpl Implementation

-    /// </summary>

-    /// <param name="typeReference"> The type of the new variable </param>

-    /// <returns> A fresh Variable with automatic generated name and location </returns>

-    public Bpl.Variable CreateFreshLocal(ITypeReference typeReference) {

-      Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location

-      Bpl.Type t = TranslationHelper.CciTypeToBoogie(typeReference);

-      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));

-      ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie

-      localVarMap.Add(dummy, v);

-      return v;

-    }

-

-    /// <summary>

-    /// 

-    /// </summary>

-    /// <param name="param"></param>

-    /// <remarks> (mschaef) only a stub </remarks>

-    private MethodParameter CreateBoogieParameter(IParameterDefinition param) {

-      MethodParameter mparam = new MethodParameter();

-

-      Bpl.Type ptype = Bpl.Type.Int;

-

-      Bpl.Formal v = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),

-          new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(param.Type.Locations),

-              param.Name.Value, ptype), false);

-

-      Bpl.Formal v_in = null;

-      if (!param.IsOut) {

-        v_in = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),

-            new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(param.Type.Locations),

-                param.Name.Value + "$in", ptype), true);

-      }

-      Bpl.Formal v_out = null;

-      if (param.IsByReference || param.IsOut) {

-        v_out = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(param.Locations),

-            new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(param.Type.Locations),

-                param.Name.Value + "$out", ptype), false);

-      }

-      mparam.localParameter = v;

-      mparam.inParameterCopy = v_in;

-      mparam.outParameterCopy = v_out;

-

-      return mparam;

-    }

-

-    /// <summary>

-    /// 

-    /// </summary>

-    /// <param name="param"></param>

-    /// <remarks>STUB</remarks>

-    /// <returns></returns>

-    public Bpl.Variable FindParameterVariable(IParameterDefinition param) {

-      MethodParameter mp;

-      formalMap.TryGetValue(param, out mp);

-      return mp.localParameter;

-    }

-    #endregion

-

-    public MethodTraverser(TraverserFactory factory, IContractProvider cp, ClassTraverser cTraverser)

-      : base(cp) {

-      this.factory = factory;

-      HeapVariable = cTraverser.HeapVariable;

-      procedure = null;

-      ClassTraverser = cTraverser;

-    }

-

-    #region Overrides

-

-    /// <summary>

-    /// 

-    /// </summary>

-    /// <param name="method"></param>

-    public override void Visit(IMethodDefinition method) {

-

-      try {

-        #region Create in- and out-parameters

-

-        int in_count = 0;

-        int out_count = 0;

-        MethodParameter mp;

-        foreach (IParameterDefinition formal in method.ResolvedMethod.Parameters) {

-

-          mp = CreateBoogieParameter(formal);

-          if (mp.inParameterCopy != null) in_count++;

-          if (mp.outParameterCopy != null) out_count++;

-          formalMap.Add(formal, mp);

-        }

-

-        #region Look for Returnvalue

-

-        // This is just a hack, should be replaced with something more robust

-        if (method.Type.TypeCode != PrimitiveTypeCode.Void) {

-          Bpl.Type rettype = Bpl.Type.Int;

-          out_count++;

-          RetVariable = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(method.Locations),

-              new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(method.Type.Locations),

-                  "$result", rettype), false);

-        } else {

-          RetVariable = null;

-        }

-

-        #endregion

-

-        #region Create 'this' parameter

-        in_count++;

-        Bpl.Type selftype = Bpl.Type.Int;

-        Bpl.Formal self = new Bpl.Formal(TranslationHelper.CciLocationToBoogieToken(method.Locations),

-            new Bpl.TypedIdent(TranslationHelper.CciLocationToBoogieToken(method.Type.Locations),

-                "this", selftype), true);

-

-        #endregion

-

-        Bpl.Variable[] invars = new Bpl.Formal[in_count];

-        Bpl.Variable[] outvars = new Bpl.Formal[out_count];

-

-        int i = 0;

-        int j = 0;

-

-        #region Add 'this' parameter as first in parameter

-        invars[i++] = self;

-        #endregion

-

-        foreach (MethodParameter mparam in formalMap.Values) {

-          if (mparam.inParameterCopy != null) {

-            invars[i++] = mparam.inParameterCopy;

-          }

-          if (mparam.outParameterCopy != null) {

-            outvars[j++] = mparam.outParameterCopy;

-            OutVars.Add(mparam);

-          }

-        }

-

-        #region add the returnvalue to out if there is one

-        if (RetVariable != null) outvars[j] = RetVariable;

-        #endregion

-       

-        #endregion

-

-        #region Check The Method Contracts

-        Bpl.RequiresSeq boogiePrecondition = new Bpl.RequiresSeq();

-        Bpl.EnsuresSeq boogiePostcondition = new Bpl.EnsuresSeq();

-        Bpl.IdentifierExprSeq boogieModifies = new Bpl.IdentifierExprSeq();

-

-        IMethodContract contract = contractProvider.GetMethodContractFor(method);

-

-        if (contract != null) {

-          try {

-            foreach (IPrecondition pre in contract.Preconditions) {

-              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);

-              exptravers.Visit(pre.Condition); // TODO

-              // Todo: Deal with Descriptions

-

-

-              Bpl.Requires req

-                  = new Bpl.Requires(TranslationHelper.CciLocationToBoogieToken(pre.Locations),

-                      true, exptravers.TranslatedExpressions.Pop(), "");

-              boogiePrecondition.Add(req);

-            }

-

-            foreach (IPostcondition post in contract.Postconditions) {

-              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);

-

-              exptravers.Visit(post.Condition);

-              // Todo: Deal with Descriptions

-

-              Bpl.Ensures ens =

-                  new Bpl.Ensures(TranslationHelper.CciLocationToBoogieToken(post.Locations),

-                      true, exptravers.TranslatedExpressions.Pop(), "");

-              boogiePostcondition.Add(ens);

-            }

-

-            foreach (IAddressableExpression mod in contract.ModifiedVariables) {

-              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(null, this.HeapVariable);

-              exptravers.Visit(mod);

-

-              Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;

-

-              if (idexp == null) {

-                throw new TranslationException(String.Format("Cannot create IdentifierExpr for Modifyed Variable {0}", mod.ToString()));

-              }

-              boogieModifies.Add(idexp);

-            }

-          } catch (TranslationException te) {

-            throw new NotImplementedException("Cannot Handle Errors in Method Contract: " + te.ToString());

-          } catch {

-            throw;

-          }

-        }

-

-        #endregion

-

-        string MethodName = TranslationHelper.CreateUniqueMethodName(method);

-

-        Bpl.Procedure proc = new Bpl.Procedure(TranslationHelper.CciLocationToBoogieToken(method.Locations),

-            MethodName, // make it unique!

-            new Bpl.TypeVariableSeq(),

-            new Bpl.VariableSeq(invars), // in

-            new Bpl.VariableSeq(outvars), // out

-            boogiePrecondition,

-            boogieModifies,

-            boogiePostcondition);

-

-        ClassTraverser.ToplevelTraverser.TranslatedProgram.TopLevelDeclarations.Add(proc);

-

-        this.procedure = proc;

-

-        if (method.IsAbstract) {

-          throw new NotImplementedException("abstract methods are not yet implemented");

-        }

-

-        StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this, this.HeapVariable);

-

-        #region Add assignements from In-Params to local-Params

-

-        foreach (MethodParameter mparam in formalMap.Values) {

-          if (mparam.inParameterCopy != null) {

-            Bpl.IToken tok = TranslationHelper.CciLocationToBoogieToken(method.Locations);

-            stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

-              new Bpl.IdentifierExpr(tok, mparam.localParameter),

-              new Bpl.IdentifierExpr(tok, mparam.inParameterCopy)));

-          }

-        }

-

-        #endregion

-

-        try {

-          method.ResolvedMethod.Body.Dispatch(stmtTraverser);

-        } catch (TranslationException te) {

-          throw new NotImplementedException("No Errorhandling in Methodvisitor / " + te.ToString());

-        } catch {

-          throw;

-        }

-

-        #region Create Local Vars For Implementation

-        //Todo: (mschaef) hack, there must be a better way to copy this

-        Bpl.Variable[] vars = new Bpl.Variable[localVarMap.Values.Count + formalMap.Values.Count];

-        i = 0;

-        foreach (Bpl.Variable v in localVarMap.Values) {

-          vars[i++] = v;

-        }

-        foreach (MethodParameter mparam in formalMap.Values) {

-          vars[i++] = mparam.localParameter;

-        }

-

-        Bpl.VariableSeq vseq = new Bpl.VariableSeq(vars);

-        #endregion

-

-        Bpl.Implementation impl =

-            new Bpl.Implementation(TranslationHelper.CciLocationToBoogieToken(method.Locations),

-                MethodName, // make unique

-                new Microsoft.Boogie.TypeVariableSeq(),

-                new Microsoft.Boogie.VariableSeq(invars),

-                new Microsoft.Boogie.VariableSeq(outvars),

-                vseq,

-                stmtTraverser.StmtBuilder.Collect(Bpl.Token.NoToken));

-

-        impl.Proc = proc;

-        ClassTraverser.ToplevelTraverser.TranslatedProgram.TopLevelDeclarations.Add(impl);

-      } catch (TranslationException te) {

-        throw new NotImplementedException(te.ToString());

-      } catch {

-        throw;

-      } finally {

-        // Maybe this is a good place to add the procedure to the toplevel declarations

-      }

-    }

-

-    #endregion

-

-  }

-

-}

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 452cc114..14cbfce7 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -62,7 +62,7 @@ namespace BytecodeTranslator {
       #region Pass 3: Translate the code model to BPL

       //tmp_BPLGenerator translator = new tmp_BPLGenerator(host, acp);

       var factory = new CLRSemantics();

-      ToplevelTraverser translator = new ToplevelTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));

+      MetadataTraverser translator = new MetadataTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));

       assembly = module as IAssembly;

       if (assembly != null)

         translator.Visit(assembly);

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 5ebaea37..af053d2d 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -24,20 +24,20 @@ namespace BytecodeTranslator
 

     public readonly TraverserFactory factory;

 

-    public readonly MethodTraverser MethodTraverser;

+    public readonly MetadataTraverser MetadataTraverser;

 

     public readonly Bpl.Variable HeapVariable;

 

     public readonly Bpl.StmtListBuilder StmtBuilder = new Bpl.StmtListBuilder();

 

     #region Constructors

-    public StatementTraverser(TraverserFactory factory, MethodTraverser mt) :

+    public StatementTraverser(TraverserFactory factory, MetadataTraverser mt) :

       this(factory, mt, mt.HeapVariable) { }

 

-    public StatementTraverser(TraverserFactory factory, MethodTraverser mt, Bpl.Variable heapvar) {

+    public StatementTraverser(TraverserFactory factory, MetadataTraverser mt, Bpl.Variable heapvar) {

       this.factory = factory;

       HeapVariable = heapvar;

-      MethodTraverser = mt;

+      MetadataTraverser = mt;

     }

     #endregion

 

@@ -84,8 +84,8 @@ namespace BytecodeTranslator
     /// <remarks>(mschaef) Works, but still a stub</remarks>

     /// <param name="conditionalStatement"></param>

     public override void Visit(IConditionalStatement conditionalStatement) {

-      StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.MethodTraverser, this.HeapVariable);

-      StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.MethodTraverser, this.HeapVariable);

+      StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.MetadataTraverser, this.HeapVariable);

+      StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.MetadataTraverser, this.HeapVariable);

 

       ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this, this.HeapVariable);

       condTraverser.Visit(conditionalStatement.Condition);

@@ -129,7 +129,7 @@ namespace BytecodeTranslator
     /// </summary>

     public override void Visit(ILocalDeclarationStatement localDeclarationStatement) {

       if (localDeclarationStatement.InitialValue == null) return;

-      var loc = this.MethodTraverser.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);

+      var loc = this.MetadataTraverser.FindOrCreateLocalVariable(localDeclarationStatement.LocalVariable);

       var tok = TokenFor(localDeclarationStatement);

       var e = ExpressionFor(localDeclarationStatement.InitialValue);

       StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, loc), e));

@@ -145,7 +145,7 @@ namespace BytecodeTranslator
       Bpl.IToken tok = TokenFor(returnStatement);

 

       #region Copy values of all out parameters to outvariables

-      foreach (MethodTraverser.MethodParameter mp in MethodTraverser.OutVars) {

+      foreach (MetadataTraverser.MethodParameter mp in this.MetadataTraverser.OutVars) {

         StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

           new Bpl.IdentifierExpr(tok, mp.outParameterCopy), new Bpl.IdentifierExpr(tok, mp.localParameter)));

       }

@@ -155,12 +155,12 @@ namespace BytecodeTranslator
         ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this, this.HeapVariable);

         etrav.Visit(returnStatement.Expression);

 

-        if (this.MethodTraverser.RetVariable == null || etrav.TranslatedExpressions.Count < 1) {

+        if (this.MetadataTraverser.RetVariable == null || etrav.TranslatedExpressions.Count < 1) {

           throw new TranslationException(String.Format("{0} returns a value that is not supported by the function", returnStatement.ToString()));

         }

 

         StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,

-            new Bpl.IdentifierExpr(tok, this.MethodTraverser.RetVariable), etrav.TranslatedExpressions.Pop()));

+            new Bpl.IdentifierExpr(tok, this.MetadataTraverser.RetVariable), etrav.TranslatedExpressions.Pop()));

       }

       StmtBuilder.Add(new Bpl.ReturnCmd(TokenFor(returnStatement)));

     }

diff --git a/BCT/BytecodeTranslator/ToplevelTraverser.cs b/BCT/BytecodeTranslator/ToplevelTraverser.cs
deleted file mode 100644
index 0ba7bffa..00000000
--- a/BCT/BytecodeTranslator/ToplevelTraverser.cs
+++ /dev/null
@@ -1,82 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

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

-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-

-using Microsoft.Cci;

-using Microsoft.Cci.MetadataReader;

-using Microsoft.Cci.MutableCodeModel;

-using Microsoft.Cci.Contracts;

-using Microsoft.Cci.ILToCodeModel;

-

-using Bpl = Microsoft.Boogie;

-

-

-namespace BytecodeTranslator {

-    /// <summary>

-    /// 

-    /// </summary>

-  public class ToplevelTraverser : BaseCodeAndContractTraverser {

-

-    public readonly TraverserFactory factory;

-

-    public readonly IContractProvider ContractProvider;

-

-    public readonly Bpl.Program TranslatedProgram;

-

-    private Dictionary<ITypeDefinition, ClassTraverser> classMap = new Dictionary<ITypeDefinition, ClassTraverser>();

-

-    public ToplevelTraverser(TraverserFactory factory, IContractProvider cp)

-      : base(cp) {

-      this.factory = factory;

-      ContractProvider = cp;

-      TranslatedProgram = new Bpl.Program();

-    }

-

-    public Bpl.Variable FindOrCreateClassField(ITypeDefinition classtype, IFieldDefinition field) {

-      ClassTraverser ct;

-      if (!classMap.TryGetValue(classtype, out ct)) {

-        ct = this.factory.MakeClassTraverser(this, this.contractProvider);

-        classMap.Add(classtype, ct);

-        return ct.FindOrCreateFieldVariable(field);

-      } else {

-        return ct.FindOrCreateFieldVariable(field);

-      }

-    }

-

-

-    /// <summary>

-    /// 

-    /// </summary>

-    /// <param name="typeDefinition"></param>

-    public override void Visit(ITypeDefinition typeDefinition) {

-      if (typeDefinition.IsClass) {

-

-        ClassTraverser ct;

-        if (!classMap.TryGetValue(typeDefinition, out ct)) {

-          ct = this.factory.MakeClassTraverser(this, this.contractProvider);

-          classMap.Add(typeDefinition, ct);

-        }

-        ct.Visit(typeDefinition);

-      } else {

-        Console.WriteLine("Non-Class {0} was found", typeDefinition);

-        throw new NotImplementedException(String.Format("Non-Class Type {0} is not yet supported.", typeDefinition.ToString()));

-      }

-    }

-

-    public override void Visit(IModule module) {

-      base.Visit(module);

-    }

-

-    public override void Visit(IAssembly assembly) {

-      base.Visit(assembly);

-    }

-

-  }

-

-}

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index cacc9817..9f79b034 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -18,10 +18,8 @@ using Bpl = Microsoft.Boogie;
 

 namespace BytecodeTranslator {

   public abstract class TraverserFactory {

-    public virtual ToplevelTraverser MakeTopLevelTraverser(IContractProvider contractProvider) { return new ToplevelTraverser(this, contractProvider); }

-    public virtual ClassTraverser MakeClassTraverser(ToplevelTraverser parent, IContractProvider contractProvider) { return new ClassTraverser(this, contractProvider, parent); }

-    public virtual MethodTraverser MakeMethodTraverser(ClassTraverser parent, IContractProvider contractProvider) { return new MethodTraverser(this, contractProvider, parent); }

-    public virtual StatementTraverser MakeStatementTraverser(MethodTraverser parent, Bpl.Variable heapVariable) { return new StatementTraverser(this, parent, heapVariable); }

+    public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider) { return new MetadataTraverser(this, contractProvider); }

+    public virtual StatementTraverser MakeStatementTraverser(MetadataTraverser parent, Bpl.Variable heapVariable) { return new StatementTraverser(this, parent, heapVariable); }

     public virtual ExpressionTraverser MakeExpressionTraverser(StatementTraverser parent, Bpl.Variable heapVariable) { return new ExpressionTraverser(parent, heapVariable); }

   }

 }
\ No newline at end of file
diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index a018797d..ed1be53a 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -84,7 +84,7 @@ namespace TranslationTest {
 

       #region Pass 3: Translate the code model to BPL

       var factory = new CLRSemantics();

-      ToplevelTraverser translator = new ToplevelTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));

+      MetadataTraverser translator = new MetadataTraverser(factory, host.GetContractExtractor(module.ModuleIdentity));

       assembly = module as IAssembly;

       if (assembly != null)

         translator.Visit(assembly);