fixed a bug on current nav tracking

refactored methodcall visitor a bit

7 files changed, 165 insertions, 106 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index cffbc046..5e195300 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -449,7 +449,6 @@ namespace BytecodeTranslator
     /// <remarks>Stub, This one really needs comments!</remarks>

     public override void Visit(IMethodCall methodCall) {

       var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;

-

       if (resolvedMethod == Dummy.Method) {

         throw new TranslationException(

           ExceptionType.UnresolvedMethod,

@@ -457,108 +456,131 @@ namespace BytecodeTranslator
       }

 

       Bpl.IToken methodCallToken = methodCall.Token();

-

       List<Bpl.Expr> inexpr;

       List<Bpl.IdentifierExpr> outvars;

       Bpl.IdentifierExpr thisExpr;

       Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;

       var proc = TranslateArgumentsAndReturnProcedure(methodCallToken, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed);

-

       string methodname = proc.Name;

       var translateAsFunctionCall = proc is Bpl.Function;

       Bpl.QKeyValue attrib = null;

-      if (!translateAsFunctionCall) {

-        foreach (var a in resolvedMethod.Attributes) {

-          if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {

-            attrib = new Bpl.QKeyValue(methodCallToken, "async", new List<object>(), null);

+

+      // TODO this code structure is quite chaotic, and some code needs to be evaluated regardless, hence the try-finally

+      try {

+        if (!translateAsFunctionCall) {

+          foreach (var a in resolvedMethod.Attributes) {

+            if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {

+              attrib = new Bpl.QKeyValue(methodCallToken, "async", new List<object>(), null);

+            }

           }

         }

-      }

 

-      #region Special case: ctor call for a struct type

-      if (resolvedMethod.IsConstructor && resolvedMethod.ContainingTypeDefinition.IsStruct) {

-        // then the method call looks like "&s.S.ctor(...)" for some variable s of struct type S

-        // treat it as if it was "s := new S(...)"

-        // So this code is the same as Visit(ICreateObjectInstance)

-        // TODO: factor the code into a single method?

-

-        // First generate an Alloc() call

-        this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(thisExpr)));

+        if (resolvedMethod.IsConstructor && resolvedMethod.ContainingTypeDefinition.IsStruct) {

+          handleStructConstructorCall(methodCall, methodCallToken, inexpr, outvars, thisExpr, proc);

+          return;

+        }

 

-        // Second, generate the call to the appropriate ctor

-        this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, proc.Name, inexpr, outvars));

+        Bpl.CallCmd call;

+        bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");

+        bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");

+        if (isEventAdd || isEventRemove) {

+          call = translateAddRemoveCall(methodCall, resolvedMethod, methodCallToken, inexpr, outvars, thisExpr, isEventAdd);

+        } else {

+          if (translateAsFunctionCall) {

+            var func = proc as Bpl.Function;

+            var exprSeq = new Bpl.ExprSeq();

+            foreach (var e in inexpr) {

+              exprSeq.Add(e);

+            }

+            var callFunction = new Bpl.NAryExpr(methodCallToken, new Bpl.FunctionCall(func), exprSeq);

+            this.TranslatedExpressions.Push(callFunction);

+            return;

+          } else {

+            if (attrib != null)

+              call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars, attrib);

+            else

+              call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars);

+            this.StmtTraverser.StmtBuilder.Add(call);

+          }

+        }

 

-        // Generate an assumption about the dynamic type of the just allocated object

-        this.StmtTraverser.StmtBuilder.Add(

-            new Bpl.AssumeCmd(methodCallToken,

-              Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

-              this.sink.Heap.DynamicType(thisExpr),

-              this.sink.FindOrCreateType(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)

-              )

-              )

-            );

+        foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {

+          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));

+        }

 

-        return;

+        Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));

+        this.StmtTraverser.RaiseException(expr);

+      } finally {

+        if (PhoneCodeHelper.PhonePlugin != null) {

+          if (PhoneCodeHelper.isNavigationCall(methodCall, sink.host)) {

+            // the block is a potential page changer

+            List<Bpl.AssignLhs> lhs = new List<Bpl.AssignLhs>();

+            List<Bpl.Expr> rhs = new List<Bpl.Expr>();

+            Bpl.Expr value = new Bpl.LiteralExpr(Bpl.Token.NoToken, false);

+            rhs.Add(value);

+            Bpl.SimpleAssignLhs assignee=

+              new Bpl.SimpleAssignLhs(Bpl.Token.NoToken,

+                                      new Bpl.IdentifierExpr(Bpl.Token.NoToken,

+                                                             sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_CONTINUE_ON_PAGE_VARIABLE, Bpl.Type.Bool)));

+            lhs.Add(assignee);

+            Bpl.AssignCmd assignCmd = new Bpl.AssignCmd(Bpl.Token.NoToken, lhs, rhs);

+            this.StmtTraverser.StmtBuilder.Add(assignCmd);

+          }

+        }

       }

-      #endregion

+    }

 

+    private Bpl.CallCmd translateAddRemoveCall(IMethodCall methodCall, IMethodDefinition resolvedMethod, Bpl.IToken methodCallToken, List<Bpl.Expr> inexpr, List<Bpl.IdentifierExpr> outvars, Bpl.IdentifierExpr thisExpr, bool isEventAdd) {

       Bpl.CallCmd call;

-      bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");

-      bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");

-      if (isEventAdd || isEventRemove) {

-        var mName = resolvedMethod.Name.Value;

-        var eventName = mName.Substring(mName.IndexOf('_') + 1);

-        var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));

-        Contract.Assert(eventDef != Dummy.Event);

-        Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);

-        Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);

-

-        if (methodCall.IsStaticCall) {

-          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));

-          inexpr.Insert(0, Bpl.Expr.Ident(local));

-        }

-        else {

-          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));

-          inexpr[0] = Bpl.Expr.Ident(local);

-        }

-

-        System.Diagnostics.Debug.Assert(outvars.Count == 0);

-        outvars.Insert(0, Bpl.Expr.Ident(local));

-        string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;

-        call = new Bpl.CallCmd(methodCallToken, methodName, inexpr, outvars);

-        this.StmtTraverser.StmtBuilder.Add(call);

-        if (methodCall.IsStaticCall) {

-          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));

-        }

-        else {

-          this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCallToken, thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));

-        }

+      var mName = resolvedMethod.Name.Value;

+      var eventName = mName.Substring(mName.IndexOf('_') + 1);

+      var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));

+      Contract.Assert(eventDef != Dummy.Event);

+      Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);

+      Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);

+

+      if (methodCall.IsStaticCall) {

+        this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));

+        inexpr.Insert(0, Bpl.Expr.Ident(local));

       } else {

-        if (translateAsFunctionCall) {

-          var func = proc as Bpl.Function;

-          var exprSeq = new Bpl.ExprSeq();

-          foreach (var e in inexpr) {

-            exprSeq.Add(e);

-          }

-          var callFunction = new Bpl.NAryExpr(methodCallToken, new Bpl.FunctionCall(func), exprSeq);

-          this.TranslatedExpressions.Push(callFunction);

-          return;

-

-        } else {

-          if (attrib != null)

-            call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars, attrib);

-          else

-            call = new Bpl.CallCmd(methodCallToken, methodname, inexpr, outvars);

-          this.StmtTraverser.StmtBuilder.Add(call);

-        }

+        this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));

+        inexpr[0] = Bpl.Expr.Ident(local);

       }

 

-      foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {

-        this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));

+      System.Diagnostics.Debug.Assert(outvars.Count == 0);

+      outvars.Insert(0, Bpl.Expr.Ident(local));

+      string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;

+      call = new Bpl.CallCmd(methodCallToken, methodName, inexpr, outvars);

+      this.StmtTraverser.StmtBuilder.Add(call);

+      if (methodCall.IsStaticCall) {

+        this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));

+      } else {

+        this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCallToken, thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));

       }

+      return call;

+    }

+

+    private void handleStructConstructorCall(IMethodCall methodCall, Bpl.IToken methodCallToken, List<Bpl.Expr> inexpr, List<Bpl.IdentifierExpr> outvars, Bpl.IdentifierExpr thisExpr, Bpl.DeclWithFormals proc) {

+      // then the method call looks like "&s.S.ctor(...)" for some variable s of struct type S

+      // treat it as if it was "s := new S(...)"

+      // So this code is the same as Visit(ICreateObjectInstance)

+      // TODO: factor the code into a single method?

 

-      Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));

-      this.StmtTraverser.RaiseException(expr);

+      // First generate an Alloc() call

+      this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(thisExpr)));

+

+      // Second, generate the call to the appropriate ctor

+      this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, proc.Name, inexpr, outvars));

+

+      // Generate an assumption about the dynamic type of the just allocated object

+      this.StmtTraverser.StmtBuilder.Add(

+          new Bpl.AssumeCmd(methodCallToken,

+            Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

+            this.sink.Heap.DynamicType(thisExpr),

+            this.sink.FindOrCreateType(methodCall.MethodToCall.ResolvedMethod.ContainingTypeDefinition)

+            )

+            )

+          );

     }

 

     // REVIEW: Does "thisExpr" really need to come back as an identifier? Can't it be a general expression?

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index fef4c944..7abb070c 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -497,7 +497,6 @@ namespace BytecodeTranslator {
     #endregion

 

     private void addPhoneTopLevelDeclarations() {

-      // adding global variable for continue on page

       Bpl.Variable continueOnPageVar = sink.FindOrCreateGlobalVariable(PhoneCodeHelper.BOOGIE_CONTINUE_ON_PAGE_VARIABLE, Bpl.Type.Bool);

       sink.TranslatedProgram.TopLevelDeclarations.Add(continueOnPageVar);

     }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
index 615b5a51..235cdc79 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
@@ -18,6 +18,7 @@ namespace BytecodeTranslator.Phone {
     private const string BOOGIE_VAR_PREFIX= "__BOOGIE_";

     public const string IL_CURRENT_NAVIGATION_URI_VARIABLE = IL_BOOGIE_VAR_PREFIX + "CurrentNavigationURI__";

     public const string BOOGIE_CONTINUE_ON_PAGE_VARIABLE = BOOGIE_VAR_PREFIX + "ContinueOnPage__";

+    public static readonly string[] NAV_CALLS = { /*"GoBack", "GoForward", "Navigate", "StopLoading"*/ "Navigate", "GoBack" };

 

     // awful hack. want to insert a nonexisting method call while traversing CCI AST, deferring it to Boogie translation

     public const string BOOGIE_DO_HAVOC_CURRENTURI = BOOGIE_VAR_PREFIX + "Havoc_CurrentURI__";

@@ -69,12 +70,12 @@ namespace BytecodeTranslator.Phone {
       return false;

     }

 

-    public static bool isStringClass(this ITypeReference typeRef, MetadataReaderHost host) {

+    public static bool isStringClass(this ITypeReference typeRef, IMetadataHost host) {

       ITypeReference targetType = host.PlatformType.SystemString;

       return typeRef.isClass(targetType);

     }

 

-    public static bool isURIClass (this ITypeReference typeRef, MetadataReaderHost host) {

+    public static bool isURIClass (this ITypeReference typeRef, IMetadataHost host) {

       Microsoft.Cci.Immutable.PlatformType platformType = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;

       if (platformType == null)

         return false;

@@ -87,8 +88,27 @@ namespace BytecodeTranslator.Phone {
       return typeRef.isClass(uriTypeRef);

     }

 

+    public static bool isNavigationServiceClass(this ITypeReference typeRef, IMetadataHost host) {

+      Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;

+      AssemblyIdentity MSPhoneAssemblyId =

+          new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),

+                               new byte[] { 0x24, 0xEE, 0xC0, 0xD8, 0xC8, 0x6C, 0xDA, 0x1E }, "");

+

+      IAssemblyReference phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);

+      ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "System", "Windows", "Navigation", "NavigationService");

+

+      ITypeReference baseClass = typeRef.ResolvedType.BaseClasses.FirstOrDefault();

+      while (baseClass != null) {

+        if (baseClass.ResolvedType.Equals(phoneApplicationPageTypeRef.ResolvedType)) {

+          return true;

+        }

+        baseClass = baseClass.ResolvedType.BaseClasses.FirstOrDefault();

+      }

+

+      return false;

+    }

 

-    public static bool isPhoneApplicationClass(this ITypeReference typeRef, MetadataReaderHost host) {

+    public static bool isPhoneApplicationClass(this ITypeReference typeRef, IMetadataHost host) {

       Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;

       IAssemblyReference coreAssemblyRef = platform.CoreAssemblyRef;

       AssemblyIdentity MSPhoneSystemWindowsAssemblyId =

@@ -100,7 +120,7 @@ namespace BytecodeTranslator.Phone {
       return typeRef.isClass(applicationClass);

     }

 

-    public static bool isPhoneApplicationPageClass(ITypeReference typeDefinition, MetadataReaderHost host) {

+    public static bool isPhoneApplicationPageClass(this ITypeReference typeRef, IMetadataHost host) {

       Microsoft.Cci.Immutable.PlatformType platform = host.PlatformType as Microsoft.Cci.Immutable.PlatformType;

       AssemblyIdentity MSPhoneAssemblyId =

           new AssemblyIdentity(host.NameTable.GetNameFor("Microsoft.Phone"), "", new Version("7.0.0.0"),

@@ -109,7 +129,7 @@ namespace BytecodeTranslator.Phone {
       IAssemblyReference phoneAssembly = host.FindAssembly(MSPhoneAssemblyId);

       ITypeReference phoneApplicationPageTypeRef = platform.CreateReference(phoneAssembly, "Microsoft", "Phone", "Controls", "PhoneApplicationPage");

 

-      ITypeReference baseClass = typeDefinition.ResolvedType.BaseClasses.FirstOrDefault();

+      ITypeReference baseClass = typeRef.ResolvedType.BaseClasses.FirstOrDefault();

       while (baseClass != null) {

         if (baseClass.ResolvedType.Equals(phoneApplicationPageTypeRef.ResolvedType)) {

           return true;

@@ -157,6 +177,14 @@ namespace BytecodeTranslator.Phone {
       return Uri.IsWellFormedUriString(uri, UriKind.RelativeOrAbsolute);

     }

 

+    public static bool isNavigationCall(IMethodCall call, IMetadataHost host) {

+      ITypeReference callType = call.MethodToCall.ContainingType;

+      if (!callType.isNavigationServiceClass(host))

+        return false;

+

+      return PhoneCodeHelper.NAV_CALLS.Contains(call.MethodToCall.Name.Value);

+    }

+

     /// <summary>

     /// uri is a valid URI but possibly partial (incomplete ?arg= values) and overspecified (complete ?arg=values)

     /// This method returns a base URI

@@ -172,5 +200,14 @@ namespace BytecodeTranslator.Phone {
       Uri mockStrippedUri = new Uri(str);

       return mockBaseUri.MakeRelativeUri(mockStrippedUri).ToString();

     }

+

+    private static ITypeReference mainAppTypeRef;

+    public static void setMainAppTypeReference(ITypeReference appType) {

+      mainAppTypeRef = appType;

+    }

+

+    public static ITypeReference getMainAppTypeReference() {

+      return mainAppTypeRef;

+    }

   }

 }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs
index 49b43137..3a779dcd 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeWrapperWriter.cs
@@ -8,8 +8,6 @@ using TranslationPlugins;
 namespace BytecodeTranslator.Phone {

   class PhoneCodeWrapperWriter {

     private static Sink sink;

-    private static readonly string BOOGIE_MAIN_PROCEDURE = "$__BOOGIE_MAIN_PROCEDURE__$";

-

     public static void createCodeWrapper(Sink sink) {

       PhoneCodeWrapperWriter.sink = sink;

       /*

diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
index 92090cc1..fec6e870 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
@@ -161,6 +161,7 @@ namespace BytecodeTranslator.Phone {
           IsStatic = false,

         },

         Instance = new ThisReference() { Type = methodBeingTraversed.Container },

+        Type=getTypeForClassname(controlInfo.ClassName),

       };

     }

 

@@ -293,7 +294,9 @@ namespace BytecodeTranslator.Phone {
     /// </summary>

     /// 

     public override void Visit(ITypeDefinition typeDefinition) {

-      if (typeDefinition.IsClass && PhoneCodeHelper.isPhoneApplicationPageClass(typeDefinition, host)) {

+      if (typeDefinition.isPhoneApplicationClass(host)) {

+        PhoneCodeHelper.setMainAppTypeReference(typeDefinition);

+      } else if (typeDefinition.isPhoneApplicationPageClass(host)) {

         base.Visit(typeDefinition);

       }

     }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
index 38fb2b58..ebbf9222 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
@@ -12,8 +12,6 @@ namespace BytecodeTranslator.Phone {
     private ITypeReference navigationSvcType;

     private ITypeReference typeTraversed;

 

-    private static readonly string[] NAV_CALLS = { /*"GoBack", "GoForward", "Navigate", "StopLoading"*/ "Navigate", "GoBack"};

-

     public PhoneNavigationCodeTraverser(MetadataReaderHost host, ITypeReference typeTraversed) : base() {

       this.host = host;

       this.typeTraversed = typeTraversed;

@@ -48,7 +46,8 @@ namespace BytecodeTranslator.Phone {
               Target = new TargetExpression() {

                 Type = host.PlatformType.SystemString,

                 Definition = new FieldReference() {

-                  ContainingType= typeTraversed,

+                  // ContainingType= typeTraversed,

+                  ContainingType= PhoneCodeHelper.getMainAppTypeReference(),

                   IsStatic=true,

                   Type=host.PlatformType.SystemString,

                   Name=host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),

@@ -96,7 +95,7 @@ namespace BytecodeTranslator.Phone {
         return;

 

       string methodToCallName= methodToCall.Name.Value;

-      if (!NAV_CALLS.Contains(methodToCallName))

+      if (!PhoneCodeHelper.NAV_CALLS.Contains(methodToCallName))

         return;

 

       navCallFound = true;

@@ -214,7 +213,7 @@ namespace BytecodeTranslator.Phone {
           Target = new TargetExpression() {

             Type = host.PlatformType.SystemString,

             Definition = new FieldReference() {

-              ContainingType=typeTraversed,

+              ContainingType=PhoneCodeHelper.getMainAppTypeReference(),

               IsStatic= true,

               Type = host.PlatformType.SystemString,

               Name = host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),

@@ -244,7 +243,7 @@ namespace BytecodeTranslator.Phone {
           Target = new TargetExpression() {

             Type = host.PlatformType.SystemString,

             Definition = new FieldReference() {

-              ContainingType=typeTraversed,

+              ContainingType = PhoneCodeHelper.getMainAppTypeReference(),

               IsStatic= true,

               Type = host.PlatformType.SystemString,

               Name = host.NameTable.GetNameFor(PhoneCodeHelper.IL_CURRENT_NAVIGATION_URI_VARIABLE),

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 7dae78e8..8745ee9e 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -176,16 +176,6 @@ namespace BytecodeTranslator {
 

       var primaryModule = modules[0];

 

-      PhoneControlsPlugin phonePlugin = null;

-      if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {

-        phonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);

-        PhoneCodeHelper.PhonePlugin = phonePlugin;

-        PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(host);

-        initTr.InjectPhoneCodeAssemblies(modules);

-        PhoneNavigationMetadataTraverser navTr = new PhoneNavigationMetadataTraverser(host);

-        navTr.InjectPhoneCodeAssemblies(modules);

-      }

-

       TraverserFactory traverserFactory;

       if (wholeProgram)

         traverserFactory = new WholeProgram();

@@ -196,6 +186,17 @@ namespace BytecodeTranslator {
       TranslationHelper.tmpVarCounter = 0;

       MetadataTraverser translator;

       translator= traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);

+

+      PhoneControlsPlugin phonePlugin = null;

+      if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {

+        phonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);

+        PhoneCodeHelper.PhonePlugin = phonePlugin;

+        PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(host);

+        initTr.InjectPhoneCodeAssemblies(modules);

+        PhoneNavigationMetadataTraverser navTr = new PhoneNavigationMetadataTraverser(host);

+        navTr.InjectPhoneCodeAssemblies(modules);

+      }

+

       translator.TranslateAssemblies(modules);

 

       foreach (var pair in sink.delegateTypeToDelegates.Values) {