more static URI detection

7 files changed, 138 insertions, 145 deletions

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 1bbcc198..d4a125e1 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -355,9 +355,6 @@ namespace BytecodeTranslator {
         if (helperTypes != null) {

           this.privateTypes.AddRange(helperTypes);

         }

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

-        stmtTraverser.StmtBuilder.Add(new Bpl.ReturnCmd(Bpl.Token.NoToken));

-        stmtTraverser.GenerateDispatchContinuation();

         #endregion

 

         #region Create Local Vars For Implementation

@@ -370,7 +367,6 @@ namespace BytecodeTranslator {
           vars.Add(v);

         }

         vars.Add(procInfo.LocalExcVariable);

-        vars.Add(procInfo.FinallyStackVariable);

         vars.Add(procInfo.LabelVariable);

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

         #endregion

diff --git a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
index bf293a51..60bf3360 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneCodeHelper.cs
@@ -44,7 +44,7 @@ namespace BytecodeTranslator.Phone {
       AssemblyIdentity systemAssemblyId = new AssemblyIdentity(host.NameTable.GetNameFor("System"), "", coreRef.Version, coreRef.PublicKeyToken, "");

       IAssemblyReference systemAssembly = host.FindAssembly(systemAssemblyId);

 

-      ITypeReference uriTypeRef= platformType.CreateReference(systemAssembly, "System", "URI");

+      ITypeReference uriTypeRef= platformType.CreateReference(systemAssembly, "System", "Uri");

       return typeRef.isClass(uriTypeRef);

     }

 

@@ -81,5 +81,41 @@ namespace BytecodeTranslator.Phone {
 

       return false;

     }

+

+    /// <summary>

+    /// checks whether a static URI root (a definite page base) can be extracted from the expression 

+    /// </summary>

+    /// <param name="expr"></param>

+    /// <returns></returns>

+    public static bool IsStaticURIRootExtractable(this IExpression expr) {

+      // Pre expr.type == string

+      IMethodCall stringConcatExpr = expr as IMethodCall;

+      if (stringConcatExpr == null)

+        return false;

+

+      if (stringConcatExpr.MethodToCall.Name.Value != "Concat")

+        return false;

+

+      IList<string> constantStrings = new List<string>();

+

+      // TODO this misses so many static strings, but let's start with this for now

+      IExpression leftOp= stringConcatExpr.Arguments.FirstOrDefault();

+      while (leftOp != null && leftOp is ICompileTimeConstant) {

+        ICompileTimeConstant strConst= leftOp as ICompileTimeConstant;

+        constantStrings.Add(strConst.Value as string);

+        if (stringConcatExpr.Arguments.ToList()[1] is IMethodCall) {

+          stringConcatExpr = stringConcatExpr.Arguments.ToList()[1] as IMethodCall;

+          leftOp = stringConcatExpr.Arguments.FirstOrDefault();

+        } else if (stringConcatExpr.Arguments.ToList()[1] is ICompileTimeConstant) {

+          constantStrings.Add((stringConcatExpr.Arguments.ToList()[1] as ICompileTimeConstant).Value as string);

+          break;

+        } else {

+          break;

+        }

+      }

+

+      string constantSubstring= constantStrings.Aggregate((aggr, elem) => aggr + elem);

+      return Uri.IsWellFormedUriString(constantSubstring, UriKind.RelativeOrAbsolute);

+    }

   }

 }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
index ad502911..fd24ff65 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneInitializationTraverser.cs
@@ -236,9 +236,8 @@ namespace BytecodeTranslator.Phone {
       return new List<IStatement>();

     }

 

-    // TODO should stop propagating the string

+    // TODO should stop propagating the string event name

     private IEnumerable<IStatement> getCodeForSettingEventHandlers(ControlInfoStructure controlInfo, string eventName) {

-

       // TODO not implemented yet

       return new List<IStatement>();

     }

diff --git a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
index edefa24d..0cb6d91e 100644
--- a/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
+++ b/BCT/BytecodeTranslator/Phone/PhoneNavigationTraverser.cs
@@ -59,6 +59,7 @@ namespace BytecodeTranslator.Phone {
               Expression= uriInitAssign,

             };

             bodyBlock.Statements.Insert(0, uriInitStmt);

+            bodyBlock.Statements.Insert(0, uriInitStmt);

           }

         }

       }

@@ -100,39 +101,33 @@ namespace BytecodeTranslator.Phone {
         return;

       } else {

         navCallFound = true;

-        bool targetIsStatic=false;

+        bool isStatic=false;

         string notStaticReason = "";

+        StaticURIMode staticMode = StaticURIMode.NOT_STATIC;

+

         if (methodToCallName == "GoBack")

-          targetIsStatic = true;

+          isStatic= true;

         else { // Navigate()

           // check for different static patterns that we may be able to verify

-          bool isStatic = false;

-          StaticURIMode staticMode = StaticURIMode.NOT_STATIC;

-

           IExpression uriArg= methodCall.Arguments.First();

           if (isArgumentURILocallyCreatedStatic(uriArg)) {

             isStatic = true;

             staticMode = StaticURIMode.STATIC_URI_CREATION_ONSITE;

           } else if (isArgumentURILocallyCreatedStaticRoot(uriArg)) {

-            isStatic=true;

-            staticMode=StaticURIMode.STATIC_URI_ROOT_CREATION_ONSITE;

-          }

-

-          ICreateObjectInstance creationSite= methodCall.Arguments.First() as ICreateObjectInstance;

-          if (creationSite != null) {

-            if (creationSite.Arguments.First().Type.ResolvedType.Equals(host.PlatformType.SystemString.ResolvedType) && creationSite.Arguments.First() is ICompileTimeConstant) {

-              targetIsStatic = true;

-            } else {

-              targetIsStatic = false;

-              notStaticReason = "URI not initialized as a static string";

-            }

+            isStatic = true;

+            staticMode = StaticURIMode.STATIC_URI_ROOT_CREATION_ONSITE;

           } else {

-            targetIsStatic = false;

-            notStaticReason = "URI not created at call site";

+            // get reason

+            ICreateObjectInstance creationSite = methodCall.Arguments.First() as ICreateObjectInstance;

+            if (creationSite == null)

+              notStaticReason = "URI not created at call site";

+            else

+              notStaticReason = "URI not initialized as a static string";

           }

         }

-        Console.Write("Page navigation event found. Target is static? " + (targetIsStatic ? "YES" : "NO"));

-        if (!targetIsStatic) {

+

+        Console.Write("Page navigation event found. Target is static? " + (isStatic ? "YES" : "NO"));

+        if (!isStatic) {

           nonStaticNavEvtCount++;

           Console.WriteLine(" -- Reason: " + notStaticReason);

         } else {

@@ -172,8 +167,19 @@ namespace BytecodeTranslator.Phone {
     /// <returns></returns>

     private bool isArgumentURILocallyCreatedStaticRoot(IExpression arg) {

       // Pre: !isArgumentURILocallyCreatedStatic

-      // TODO

-      return false;

+      if (!arg.isCreateObjectInstance())

+        return false;

+

+      if (!arg.Type.isURIClass(host))

+        return false;

+

+      ICreateObjectInstance creationSite = arg as ICreateObjectInstance;

+      IExpression uriTargetArg = creationSite.Arguments.First();

+

+      if (!uriTargetArg.Type.isStringClass(host))

+        return false;

+

+      return uriTargetArg.IsStaticURIRootExtractable();

     }

 

     private void injectNavigationUpdateCode(IBlockStatement block, IEnumerable<IStatement> stmts) {

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index b5c01fc1..c14505ee 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -70,12 +70,6 @@ namespace BytecodeTranslator {
         return info.LocalExcVariable;

       }

     }

-    public Bpl.LocalVariable FinallyStackCounterVariable {

-      get {

-        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

-        return info.FinallyStackVariable;

-      }

-    }

     public Bpl.LocalVariable LabelVariable {

       get {

         ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

@@ -348,7 +342,6 @@ namespace BytecodeTranslator {
       private Bpl.Formal thisVariable;

       private Bpl.Formal returnVariable;

       private Bpl.LocalVariable localExcVariable;

-      private Bpl.LocalVariable finallyStackVariable;

       private Bpl.LocalVariable labelVariable;

       private List<Bpl.Formal> typeParameters;

       private List<Bpl.Formal> methodParameters;

@@ -359,7 +352,6 @@ namespace BytecodeTranslator {
         this.returnVariable = null;

         this.thisVariable = null;

         this.localExcVariable = null;

-        this.finallyStackVariable = null;

         this.labelVariable = null;

         this.typeParameters = null;

         this.methodParameters = null;

@@ -383,14 +375,12 @@ namespace BytecodeTranslator {
         Bpl.Formal returnVariable,

         Bpl.Formal thisVariable,

         Bpl.LocalVariable localExcVariable,

-        Bpl.LocalVariable finallyStackVariable,

         Bpl.LocalVariable labelVariable,

         List<Bpl.Formal> typeParameters,

         List<Bpl.Formal> methodParameters)

         : this(decl, formalMap, returnVariable) {

         this.thisVariable = thisVariable;

         this.localExcVariable = localExcVariable;

-        this.finallyStackVariable = finallyStackVariable;

         this.labelVariable = labelVariable;

         this.typeParameters = typeParameters;

         this.methodParameters = methodParameters;

@@ -401,7 +391,6 @@ namespace BytecodeTranslator {
       public Bpl.Formal ThisVariable { get { return thisVariable; } }

       public Bpl.Formal ReturnVariable { get { return returnVariable; } }

       public Bpl.LocalVariable LocalExcVariable { get { return localExcVariable; } }

-      public Bpl.LocalVariable FinallyStackVariable { get { return finallyStackVariable; } }

       public Bpl.LocalVariable LabelVariable { get { return labelVariable; } }

       public Bpl.Formal TypeParameter(int index) { return typeParameters[index]; }

       public Bpl.Formal MethodParameter(int index) { return methodParameters[index]; } 

@@ -418,7 +407,6 @@ namespace BytecodeTranslator {
         Bpl.Formal thisVariable = null;

         Bpl.Formal retVariable = null;

         Bpl.LocalVariable localExcVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$localExc", this.Heap.RefType));

-        Bpl.LocalVariable finallyStackVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$finallyStackCounter", Bpl.Type.Int));

         Bpl.LocalVariable labelVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$label", Bpl.Type.Int));

         

         int in_count = 0;

@@ -533,7 +521,7 @@ namespace BytecodeTranslator {
         } else {

           this.TranslatedProgram.TopLevelDeclarations.Add(decl);

         }

-        procInfo = new ProcedureInfo(decl, formalMap, retVariable, thisVariable, localExcVariable, finallyStackVariable, labelVariable, typeParameters, methodParameters);

+        procInfo = new ProcedureInfo(decl, formalMap, retVariable, thisVariable, localExcVariable, labelVariable, typeParameters, methodParameters);

         this.declaredMethods.Add(key, procInfo);

 

         // Can't visit the method's contracts until the formalMap and procedure are added to the

@@ -981,18 +969,30 @@ namespace BytecodeTranslator {
       }

       return "continuation" + id;

     }

-    public string FindOrCreateDispatchContinuationLabel(ITryCatchFinallyStatement stmt) {

-      int id;

-      if (!tryCatchFinallyIdentifiers.TryGetValue(stmt, out id)) {

-        id = tryCatchFinallyIdentifiers.Count;

-        tryCatchFinallyIdentifiers[stmt] = id;

-      }

-      return "DispatchContinuation" + id;

-    }

     MostNestedTryStatementTraverser mostNestedTryStatementTraverser;

     public ITryCatchFinallyStatement MostNestedTryStatement(IName label) {

       return mostNestedTryStatementTraverser.MostNestedTryStatement(label);

     }

+    Dictionary<ITryCatchFinallyStatement, List<string>> escapingGotoEdges;

+    public void AddEscapingEdge(ITryCatchFinallyStatement tryCatchFinallyStatement, out int labelId, out string label) {

+      List<string> edges = null;

+      if (!escapingGotoEdges.ContainsKey(tryCatchFinallyStatement)) {

+        escapingGotoEdges[tryCatchFinallyStatement] = new List<string>();

+      }

+      edges = escapingGotoEdges[tryCatchFinallyStatement];

+      label = this.FindOrCreateFinallyLabel(tryCatchFinallyStatement) + "_" + edges.Count;

+      labelId = edges.Count;

+      edges.Add(label);

+    }

+    public List<string> EscapingEdges(ITryCatchFinallyStatement tryCatchFinallyStatement) {

+      if (!escapingGotoEdges.ContainsKey(tryCatchFinallyStatement)) {

+        escapingGotoEdges[tryCatchFinallyStatement] = new List<string>();

+      }

+      return escapingGotoEdges[tryCatchFinallyStatement];

+    }

+    public enum TryCatchFinallyContext { InTry, InCatch, InFinally };

+    public List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>> nestedTryCatchFinallyStatements;

+

     IMethodDefinition methodBeingTranslated;

     public void BeginMethod(IMethodDefinition method) {

       this.BeginMethod(method.ContainingType);

@@ -1000,6 +1000,8 @@ namespace BytecodeTranslator {
       this.cciLabels = new Dictionary<IName, int>();

       this.tryCatchFinallyIdentifiers = new Dictionary<ITryCatchFinallyStatement, int>();

       mostNestedTryStatementTraverser = new MostNestedTryStatementTraverser();

+      escapingGotoEdges = new Dictionary<ITryCatchFinallyStatement, List<string>>();

+      nestedTryCatchFinallyStatements = new List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>>();

       mostNestedTryStatementTraverser.Visit(method.Body);

     }

     

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 6bc399c1..33ecb143 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -59,14 +59,6 @@ namespace BytecodeTranslator
       this.factory = sink.Factory;

       PdbReader = pdbReader;

       this.contractContext = contractContext;

-      this.nestedTryCatchFinallyStatements = new List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>>();

-    }

-    public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, List<Tuple<ITryCatchFinallyStatement,TryCatchFinallyContext>> nestedTryCatchFinallyStatements) {

-      this.sink = sink;

-      this.factory = sink.Factory;

-      PdbReader = pdbReader;

-      this.contractContext = contractContext;

-      this.nestedTryCatchFinallyStatements = nestedTryCatchFinallyStatements;

     }

     #endregion

 

@@ -93,22 +85,6 @@ namespace BytecodeTranslator
       this.Visit(methodBody);

       return newTypes;

     }

-

-    public void GenerateDispatchContinuation() {

-      foreach (ITryCatchFinallyStatement stmt in sink.tryCatchFinallyIdentifiers.Keys) {

-        // Iterate over all labels in sink.cciLabels and generate dispatch based on sink.LabelVariable

-        this.StmtBuilder.AddLabelCmd(sink.FindOrCreateDispatchContinuationLabel(stmt));

-        Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(true), TranslationHelper.BuildStmtList(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false))), null, null);

-        Bpl.IdentifierExpr labelExpr = Bpl.Expr.Ident(this.sink.LabelVariable);

-        foreach (IName name in sink.cciLabels.Keys) {

-          Bpl.GotoCmd gotoCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(name.Value));

-          Bpl.Expr targetExpr = Bpl.Expr.Literal(sink.cciLabels[name]);

-          elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr), TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);

-        }

-        this.StmtBuilder.Add(elseIfCmd);

-        this.StmtBuilder.Add(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false)));

-      }

-    }

     #endregion

 

     //public override void Visit(ISourceMethodBody methodBody) {

@@ -193,8 +169,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.sink, this.PdbReader, this.contractContext, this.nestedTryCatchFinallyStatements);

-      StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext, this.nestedTryCatchFinallyStatements);

+      StatementTraverser thenTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

+      StatementTraverser elseTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

 

       ExpressionTraverser condTraverser = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);

       condTraverser.Visit(conditionalStatement.Condition);

@@ -248,6 +224,10 @@ namespace BytecodeTranslator
       throw new TranslationException("Continue statements are not handled");

     }

 

+    public override void Visit(ISwitchStatement switchStatement) {

+      throw new TranslationException("Switch statements are not handled");

+    }

+

     /// <summary>

     /// If the local declaration has an initial value, then generate the

     /// statement "loc := e" from it. Otherwise ignore it.

@@ -320,33 +300,25 @@ namespace BytecodeTranslator
 

     #region Goto and Labels

 

-    /// <summary>

-    /// 

-    /// </summary>

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

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

     public override void Visit(IGotoStatement gotoStatement) {

       IName target = gotoStatement.TargetStatement.Label;

-      ITryCatchFinallyStatement targetContext = this.sink.MostNestedTryStatement(target);

+      ITryCatchFinallyStatement targetStatement = this.sink.MostNestedTryStatement(target);

       int count = 0;

-      while (count < this.nestedTryCatchFinallyStatements.Count) {

-        int index = this.nestedTryCatchFinallyStatements.Count - count - 1;

-        ITryCatchFinallyStatement nestedContext = this.nestedTryCatchFinallyStatements[index].Item1;

-        if (targetContext == nestedContext)

+      while (count < this.sink.nestedTryCatchFinallyStatements.Count) {

+        int index = this.sink.nestedTryCatchFinallyStatements.Count - count - 1;

+        ITryCatchFinallyStatement nestedStatement = this.sink.nestedTryCatchFinallyStatements[index].Item1;

+        if (targetStatement == nestedStatement)

           break;

-        count++;

-      }

-      System.Diagnostics.Debug.Assert((count == nestedTryCatchFinallyStatements.Count) == (targetContext == null));

-      if (count > 0) {

-        int id = this.sink.FindOrCreateCciLabelIdentifier(target);

-        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(id)));

-        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(count-1)));

-        string finallyLabel = this.sink.FindOrCreateFinallyLabel(this.nestedTryCatchFinallyStatements[this.nestedTryCatchFinallyStatements.Count - 1].Item1);

+        int labelId;

+        string label;

+        this.sink.AddEscapingEdge(nestedStatement, out labelId, out label);

+        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(labelId)));

+        string finallyLabel = this.sink.FindOrCreateFinallyLabel(nestedStatement);

         StmtBuilder.Add(new Bpl.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(finallyLabel)));

+        StmtBuilder.AddLabelCmd(label);

+        count++;

       }

-      else {

-        StmtBuilder.Add(new Bpl.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(target.Value)));

-      }

+      StmtBuilder.Add(new Bpl.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(target.Value)));

     }

 

     /// <summary>

@@ -377,21 +349,34 @@ namespace BytecodeTranslator
 

     #endregion

 

-    public enum TryCatchFinallyContext { InTry, InCatch, InFinally };

-    List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>> nestedTryCatchFinallyStatements;

-    

+    public void GenerateDispatchContinuation(ITryCatchFinallyStatement tryCatchFinallyStatement) {

+      string continuationLabel = this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement);

+      Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(true),

+        TranslationHelper.BuildStmtList(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(continuationLabel))), null, null);

+      List<string> edges = sink.EscapingEdges(tryCatchFinallyStatement);

+      Bpl.IdentifierExpr labelExpr = Bpl.Expr.Ident(this.sink.LabelVariable);

+      for (int i = 0; i < edges.Count; i++) {

+        string label = edges[i];

+        Bpl.GotoCmd gotoCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(label));

+        Bpl.Expr targetExpr = Bpl.Expr.Literal(i);

+        elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr),

+          TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);

+      }

+      this.StmtBuilder.Add(elseIfCmd);

+    }

+

     private void RaiseExceptionHelper(Bpl.StmtListBuilder builder) {

-      int count = nestedTryCatchFinallyStatements.Count;

+      int count = this.sink.nestedTryCatchFinallyStatements.Count;

       if (count == 0) {

         builder.Add(new Bpl.ReturnCmd(Bpl.Token.NoToken));

       }

       else {

-        Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext> topOfStack = nestedTryCatchFinallyStatements[count - 1];

+        Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext> topOfStack = this.sink.nestedTryCatchFinallyStatements[count - 1];

         string exceptionTarget; 

-        if (topOfStack.Item2 == TryCatchFinallyContext.InTry) {

+        if (topOfStack.Item2 == Sink.TryCatchFinallyContext.InTry) {

           exceptionTarget = this.sink.FindOrCreateCatchLabel(topOfStack.Item1);

         }

-        else if (topOfStack.Item2 == TryCatchFinallyContext.InCatch) {

+        else if (topOfStack.Item2 == Sink.TryCatchFinallyContext.InCatch) {

           builder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));

           exceptionTarget = this.sink.FindOrCreateFinallyLabel(topOfStack.Item1);

         }

@@ -414,21 +399,21 @@ namespace BytecodeTranslator
     }

 

     public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {

-      nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InTry));

+      this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InTry));

       this.Visit(tryCatchFinallyStatement.TryBody);

       StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)));

       StmtBuilder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement))));

-      nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);

+      this.sink.nestedTryCatchFinallyStatements.RemoveAt(this.sink.nestedTryCatchFinallyStatements.Count - 1);

 

       StmtBuilder.AddLabelCmd(this.sink.FindOrCreateCatchLabel(tryCatchFinallyStatement));

       StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LocalExcVariable), Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable)));

       StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef)));

       List<Bpl.StmtList> catchStatements = new List<Bpl.StmtList>();

       List<Bpl.Expr> typeReferences = new List<Bpl.Expr>();

-      this.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InCatch));

+      this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InCatch));

       foreach (ICatchClause catchClause in tryCatchFinallyStatement.CatchClauses) {

         typeReferences.Insert(0, this.sink.FindOrCreateType(catchClause.ExceptionType));

-        StatementTraverser catchTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext, this.nestedTryCatchFinallyStatements);

+        StatementTraverser catchTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, this.contractContext);

         if (catchClause.ExceptionContainer != Dummy.LocalVariable) {

           Bpl.Variable catchClauseVariable = this.sink.FindOrCreateLocalVariable(catchClause.ExceptionContainer);

           catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(catchClauseVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));

@@ -447,49 +432,21 @@ namespace BytecodeTranslator
       this.StmtBuilder.Add(elseIfCmd);

       this.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));

       RaiseException();

-      nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);

+      this.sink.nestedTryCatchFinallyStatements.RemoveAt(this.sink.nestedTryCatchFinallyStatements.Count - 1);

 

       this.StmtBuilder.AddLabelCmd(this.sink.FindOrCreateFinallyLabel(tryCatchFinallyStatement));

       if (tryCatchFinallyStatement.FinallyBody != null) {

-        nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>(tryCatchFinallyStatement, TryCatchFinallyContext.InFinally));

+        this.sink.nestedTryCatchFinallyStatements.Add(new Tuple<ITryCatchFinallyStatement, Sink.TryCatchFinallyContext>(tryCatchFinallyStatement, Sink.TryCatchFinallyContext.InFinally));

         Bpl.Variable savedExcVariable = this.sink.CreateFreshLocal(this.sink.Heap.RefType);

         Bpl.Variable savedLabelVariable = this.sink.CreateFreshLocal(Bpl.Type.Int);

-        Bpl.Variable savedFinallyStackCounterVariable = this.sink.CreateFreshLocal(Bpl.Type.Int);

         StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedExcVariable), Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable)));

         StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedLabelVariable), Bpl.Expr.Ident(this.sink.LabelVariable)));

-        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(savedFinallyStackCounterVariable), Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable)));

         Visit(tryCatchFinallyStatement.FinallyBody);

         StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(savedExcVariable)));

         StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Ident(savedLabelVariable)));

-        StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Ident(savedFinallyStackCounterVariable)));

-        nestedTryCatchFinallyStatements.RemoveAt(nestedTryCatchFinallyStatements.Count - 1);

-      }

-      Bpl.GotoCmd dispatchCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateDispatchContinuationLabel(tryCatchFinallyStatement)));

-      Bpl.GotoCmd continuationCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement)));

-      Bpl.IfCmd ifCmd = new Bpl.IfCmd(

-        Bpl.Token.NoToken,

-        Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(this.sink.LabelVariable), Bpl.Expr.Literal(-1)),

-        TranslationHelper.BuildStmtList(continuationCmd),

-        new Bpl.IfCmd(

-          Bpl.Token.NoToken,

-          Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(0)),

-          TranslationHelper.BuildStmtList(dispatchCmd), 

-          null, 

-          null),

-        null);

-      this.StmtBuilder.Add(ifCmd);

-      int count = this.nestedTryCatchFinallyStatements.Count;

-      if (count == 0) {

-        this.StmtBuilder.Add(new Bpl.AssertCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false)));

-      }

-      else {

-        Bpl.IdentifierExpr fsv = Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable);

-        Bpl.AssignCmd decrementCmd = TranslationHelper.BuildAssignCmd(fsv, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, fsv, Bpl.Expr.Literal(1)));

-        this.StmtBuilder.Add(decrementCmd);

-        string parentFinallyLabel = this.sink.FindOrCreateFinallyLabel(this.nestedTryCatchFinallyStatements[count - 1].Item1);

-        Bpl.GotoCmd parentCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(parentFinallyLabel));

-        this.StmtBuilder.Add(parentCmd);

+        this.sink.nestedTryCatchFinallyStatements.RemoveAt(this.sink.nestedTryCatchFinallyStatements.Count - 1);

       }

+      GenerateDispatchContinuation(tryCatchFinallyStatement);

       StmtBuilder.AddLabelCmd(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement));

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

       RaiseException(raiseExpr);

@@ -506,6 +463,7 @@ namespace BytecodeTranslator
       StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));

       RaiseException();

     }

+

   }

 

 }

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index 4685427f..78c818bd 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -27,10 +27,6 @@ namespace BytecodeTranslator {
     public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {

       return new StatementTraverser(sink, pdbReader, contractContext);

     }

-    public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, 

-      List<Tuple<ITryCatchFinallyStatement,StatementTraverser.TryCatchFinallyContext>> nestedTryCatchFinallyStatements) {

-      return new StatementTraverser(sink, pdbReader, contractContext, nestedTryCatchFinallyStatements);

-    }

     public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {

       return new ExpressionTraverser(sink, statementTraverser, contractContext);

     }