bunch of changes related to finally handling

5 files changed, 219 insertions, 79 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index e2d0d636..69841178 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -1424,12 +1424,12 @@ namespace BytecodeTranslator
 

     public override void Visit(IReturnValue returnValue)

     {

-      if (this.sink.RetVariable == null)

+      if (this.sink.ReturnVariable == null)

       {

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

       }

       TranslatedExpressions.Push(new Bpl.IdentifierExpr(returnValue.Token(),

-        this.sink.RetVariable));

+        this.sink.ReturnVariable));

 

     }

     #endregion

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 5b61a6ca..f133e85c 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -104,7 +104,7 @@ namespace BytecodeTranslator {
       var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(typeDefinition);

 

       this.sink.BeginMethod(typeDefinition);

-      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false, null, null);

+      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false, new List<ITryCatchFinallyStatement>());

       var stmts = new List<IStatement>();

 

       foreach (var f in typeDefinition.Fields) {

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

       this.sink.BeginMethod(typeDefinition);

 

-      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false, null, null);

+      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false, new List<ITryCatchFinallyStatement>());

       var stmts = new List<IStatement>();

 

       foreach (var f in typeDefinition.Fields) {

@@ -280,9 +280,7 @@ namespace BytecodeTranslator {
       var formalMap = procInfo.FormalMap;

 

       try {

-        MostNestedTryStatementTraverser tryStatementTraverser = new MostNestedTryStatementTraverser();

-        tryStatementTraverser.Visit(method.Body);

-        StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false, null, null);

+        StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false, new List<ITryCatchFinallyStatement>());

 

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

 

@@ -359,6 +357,7 @@ namespace BytecodeTranslator {
           this.privateTypes.AddRange(helperTypes);

         }

         //method.Body.Dispatch(stmtTraverser);

+        stmtTraverser.GenerateDispatchContinuation();

         #endregion

 

         #region Create Local Vars For Implementation

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 4476b7f7..951c791a 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -52,10 +52,42 @@ namespace BytecodeTranslator {
     }

     readonly Heap heap;

 

-    public Bpl.Formal ThisVariable;

-    public Bpl.Formal RetVariable;

-    public Bpl.Formal ExcVariable;

-    public Bpl.LocalVariable LocalExcVariable;

+    public Bpl.Formal ThisVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.ThisVariable;

+      }

+    }

+    public Bpl.Formal ReturnVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.ReturnVariable;

+      }

+    }

+    public Bpl.Formal ExcVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.ExcVariable;

+      }

+    }

+    public Bpl.LocalVariable LocalExcVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.LocalExcVariable;

+      }

+    }

+    public Bpl.LocalVariable FinallyStackVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.FinallyStackVariable;

+      }

+    }

+    public Bpl.LocalVariable LabelVariable {

+      get {

+        ProcedureInfo info = FindOrCreateProcedure(this.methodBeingTranslated);

+        return info.LabelVariable;

+      }

+    }

 

     public readonly string AllocationMethodName = "Alloc";

     public readonly string StaticFieldFunction = "ClassRepr";

@@ -318,6 +350,8 @@ namespace BytecodeTranslator {
       private Bpl.Formal returnVariable;

       private Bpl.Formal excVariable;

       private Bpl.LocalVariable localExcVariable;

+      private Bpl.LocalVariable finallyStackVariable;

+      private Bpl.LocalVariable labelVariable;

       private List<Bpl.Formal> typeParameters;

       private List<Bpl.Formal> methodParameters;

 

@@ -328,26 +362,41 @@ namespace BytecodeTranslator {
         this.thisVariable = null;

         this.excVariable = null;

         this.localExcVariable = null;

+        this.finallyStackVariable = null;

+        this.labelVariable = null;

         this.typeParameters = null;

         this.methodParameters = null;

       }

-      public ProcedureInfo(Bpl.DeclWithFormals decl, Dictionary<IParameterDefinition, MethodParameter> formalMap, Bpl.Formal returnVariable) {

-        this.decl = decl;

-        this.formalMap = formalMap;

-        this.returnVariable = returnVariable;

-        this.thisVariable = null;

-        this.excVariable = null;

-        this.localExcVariable = null;

-        this.typeParameters = null;

-        this.methodParameters = null;

+      public ProcedureInfo(

+        Bpl.DeclWithFormals decl,

+        Dictionary<IParameterDefinition, MethodParameter> formalMap)

+        : this(decl) {

+          this.formalMap = formalMap;

       }

-      public ProcedureInfo(Bpl.DeclWithFormals decl, Dictionary<IParameterDefinition, MethodParameter> formalMap, Bpl.Formal returnVariable, Bpl.Formal thisVariable, Bpl.Formal excVariable, Bpl.LocalVariable localExcVariable, List<Bpl.Formal> typeParameters, List<Bpl.Formal> methodParameters) {

-        this.decl = decl;

-        this.formalMap = formalMap;

+      public ProcedureInfo(

+        Bpl.DeclWithFormals decl,

+        Dictionary<IParameterDefinition, MethodParameter> formalMap,

+        Bpl.Formal returnVariable)

+        : this(decl, formalMap) {

         this.returnVariable = returnVariable;

+      }

+      public ProcedureInfo(

+        Bpl.DeclWithFormals decl,

+        Dictionary<IParameterDefinition, MethodParameter> formalMap,

+        Bpl.Formal returnVariable,

+        Bpl.Formal thisVariable,

+        Bpl.Formal excVariable,

+        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.excVariable = excVariable;

         this.localExcVariable = localExcVariable;

+        this.finallyStackVariable = finallyStackVariable;

+        this.labelVariable = labelVariable;

         this.typeParameters = typeParameters;

         this.methodParameters = methodParameters;

       }

@@ -358,6 +407,8 @@ namespace BytecodeTranslator {
       public Bpl.Formal ReturnVariable { get { return returnVariable; } }

       public Bpl.Formal ExcVariable { get { return excVariable; } }

       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]; } 

     }

@@ -374,6 +425,8 @@ namespace BytecodeTranslator {
         Bpl.Formal retVariable = null;

         Bpl.Formal excVariable = new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "$exc", this.Heap.RefType), true);

         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, "$finallyStack", 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;

         int out_count = 1; // every method has the output variable $exc

@@ -489,7 +542,7 @@ namespace BytecodeTranslator {
         } else {

           this.TranslatedProgram.TopLevelDeclarations.Add(decl);

         }

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

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

         this.declaredMethods.Add(key, procInfo);

 

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

@@ -505,7 +558,7 @@ namespace BytecodeTranslator {
           try {

 

             foreach (IPrecondition pre in contract.Preconditions) {

-              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true, null, null);

+              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true, new List<ITryCatchFinallyStatement>());

               ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, stmtTraverser, true);

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

               // Todo: Deal with Descriptions

@@ -514,7 +567,7 @@ namespace BytecodeTranslator {
             }

 

             foreach (IPostcondition post in contract.Postconditions) {

-              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true, null, null);

+              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true, new List<ITryCatchFinallyStatement>());

               ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, stmtTraverser, true);

               exptravers.Visit(post.Condition);

               // Todo: Deal with Descriptions

@@ -583,7 +636,7 @@ namespace BytecodeTranslator {
         var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

         var tok = structType.Token();

         var selfType = this.CciTypeToBoogie(structType); //new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);

-        var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), false);

+        var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), true);

         var invars = new Bpl.Formal[]{ selfIn };

         var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#default_ctor",

           new Bpl.TypeVariableSeq(),

@@ -594,7 +647,7 @@ namespace BytecodeTranslator {
           new Bpl.EnsuresSeq()

           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

-        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>(), this.RetVariable);

+        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>());

         this.declaredStructDefaultCtors.Add(key, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

@@ -620,8 +673,8 @@ namespace BytecodeTranslator {
         var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

         var tok = structType.Token();

         var selfType = this.CciTypeToBoogie(structType); //new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);

-        var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), false);

-        var otherIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "other", selfType), false);

+        var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), true);

+        var otherIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "other", selfType), true);

         var invars = new Bpl.Formal[] { selfIn, otherIn, };

         var outvars = new Bpl.Formal[0];

         var selfInExpr = Bpl.Expr.Ident(selfIn);

@@ -638,7 +691,7 @@ namespace BytecodeTranslator {
           new Bpl.EnsuresSeq(ens)

           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

-        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>(), this.RetVariable);

+        procAndFormalMap = new ProcedureInfo(proc, new Dictionary<IParameterDefinition, MethodParameter>());

         this.declaredStructCopyCtors.Add(key, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

@@ -867,24 +920,59 @@ namespace BytecodeTranslator {
     public void BeginMethod(ITypeReference containingType) {

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

       this.localCounter = 0;

-      this.ThisVariable = null;

-      this.RetVariable = null;

-      this.ExcVariable = null;

-      this.LocalExcVariable = null;

       this.methodBeingTranslated = null;

     }

 

+    public Dictionary<IName, int> cciLabels;

+    public int FindOrCreateCciLabelIdentifier(IName label) {

+      int v;

+      if (!cciLabels.TryGetValue(label, out v)) {

+        v = cciLabels.Count + boogieLabels.Count;

+        cciLabels[label] = v;

+      }

+      return v;

+    }

+    public Dictionary<string, int> boogieLabels;

+    public int FindOrCreateBoogieLabelIdentifier(string label) {

+      int v;

+      if (!boogieLabels.TryGetValue(label, out v)) {

+        v = cciLabels.Count + boogieLabels.Count;

+        boogieLabels[label] = v;

+      }

+      return v;

+    }

+    Dictionary<ITryCatchFinallyStatement, int> tryCatchFinallyIdentifiers;

+    public string FindOrCreateCatchLabel(ITryCatchFinallyStatement stmt) {

+      int id;

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

+        id = tryCatchFinallyIdentifiers.Count;

+        tryCatchFinallyIdentifiers[stmt] = id;

+      }

+      return "catch" + id;

+    }

+    public string FindOrCreateFinallyLabel(ITryCatchFinallyStatement stmt) {

+      int id;

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

+        id = tryCatchFinallyIdentifiers.Count;

+        tryCatchFinallyIdentifiers[stmt] = id;

+      }

+      return "finally" + id;

+    }

+    MostNestedTryStatementTraverser mostNestedTryStatementTraverser;

+    public ITryCatchFinallyStatement MostNestedTryStatement(IName label) {

+      return mostNestedTryStatementTraverser.MostNestedTryStatement(label);

+    }

     IMethodDefinition methodBeingTranslated;

     public void BeginMethod(IMethodDefinition method) {

       this.BeginMethod(method.ContainingType);

       this.methodBeingTranslated = method;

-      ProcedureInfo info = FindOrCreateProcedure(method);

-      this.ThisVariable = info.ThisVariable;

-      this.RetVariable = info.ReturnVariable;

-      this.ExcVariable = info.ExcVariable;

-      this.LocalExcVariable = info.LocalExcVariable;

+      this.cciLabels = new Dictionary<IName, int>();

+      this.boogieLabels = new Dictionary<string, int>();

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

+      mostNestedTryStatementTraverser = new MostNestedTryStatementTraverser();

+      mostNestedTryStatementTraverser.Visit(method.Body);

     }

-

+    

     public void BeginAssembly(IAssembly assembly) {

       this.assemblyBeingTranslated = assembly;

     }

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 8310374f..01a24c17 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -54,13 +54,12 @@ namespace BytecodeTranslator
     internal readonly Stack<IExpression> operandStack = new Stack<IExpression>();

 

     #region Constructors

-    public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, string exceptionTarget, Dictionary<IName, ITryCatchFinallyStatement> mostNestedTryStatement) {

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

       this.sink = sink;

       this.factory = sink.Factory;

       PdbReader = pdbReader;

       this.contractContext = contractContext;

-      this.exceptionTarget = exceptionTarget;

-      this.mostNestedTryStatement = mostNestedTryStatement;

+      this.nestedTryCatchFinallyStatements = nestedTryCatchFinallyStatements;

     }

     #endregion

 

@@ -88,6 +87,23 @@ namespace BytecodeTranslator
       return newTypes;

     }

 

+    public void GenerateDispatchContinuation() {

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

+      this.StmtBuilder.AddLabelCmd("DispatchContinutation");

+      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);

+      }

+      foreach (string name in sink.boogieLabels.Keys) {

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

+        Bpl.Expr targetExpr = Bpl.Expr.Literal(sink.boogieLabels[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);

+    }

     #endregion

 

     //public override void Visit(ISourceMethodBody methodBody) {

@@ -154,8 +170,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.exceptionTarget, this.mostNestedTryStatement);

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

+      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);

 

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

       condTraverser.Visit(conditionalStatement.Condition);

@@ -252,12 +268,12 @@ namespace BytecodeTranslator
         ExpressionTraverser etrav = this.factory.MakeExpressionTraverser(this.sink, this, this.contractContext);

         etrav.Visit(returnStatement.Expression);

 

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

+        if (this.sink.ReturnVariable == 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.sink.RetVariable), etrav.TranslatedExpressions.Pop()));

+            new Bpl.IdentifierExpr(tok, this.sink.ReturnVariable), etrav.TranslatedExpressions.Pop()));

       }

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

     }

@@ -271,11 +287,27 @@ namespace BytecodeTranslator
     /// <remarks> STUB </remarks>

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

     public override void Visit(IGotoStatement gotoStatement) {

-      String[] target = new String[1] { gotoStatement.TargetStatement.Label.Value };

-

-      Bpl.GotoCmd gotocmd = new Microsoft.Boogie.GotoCmd(gotoStatement.Token(), new Bpl.StringSeq(target));

-

-      StmtBuilder.Add(gotocmd);

+      IName target = gotoStatement.TargetStatement.Label;

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

+      int count = 0;

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

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

+        ITryCatchFinallyStatement nestedContext = this.nestedTryCatchFinallyStatements[index];

+        if (targetContext == nestedContext)

+          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.FinallyStackVariable), Bpl.Expr.Literal(count)));

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

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

+      }

+      else {

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

+      }

     }

 

     /// <summary>

@@ -300,25 +332,26 @@ namespace BytecodeTranslator
 

     #endregion

 

-    string exceptionTarget;

-    Dictionary<IName, ITryCatchFinallyStatement> mostNestedTryStatement;

-    public Bpl.TransferCmd ExceptionJump { get { if (exceptionTarget == null) return new Bpl.ReturnCmd(Bpl.Token.NoToken); else return new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(exceptionTarget)); } }

-    Stack<string> nestedFinallyTargets = new Stack<string>();

- 

-    public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {

-      string finallyLabel = null;

-      if (tryCatchFinallyStatement.FinallyBody != null) {

-        finallyLabel = TranslationHelper.GenerateFinallyClauseName();

-        nestedFinallyTargets.Push(finallyLabel);

+    List<ITryCatchFinallyStatement> nestedTryCatchFinallyStatements;

+    public Bpl.TransferCmd ExceptionJump {

+      get {

+        int count = nestedTryCatchFinallyStatements.Count;

+        if (count == 0) {

+          return new Bpl.ReturnCmd(Bpl.Token.NoToken);

+        }

+        else {

+          string exceptionTarget = this.sink.FindOrCreateFinallyLabel(nestedTryCatchFinallyStatements[count - 1]);

+          return new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(exceptionTarget));

+        }

       }

+    }

 

-      string savedExceptionTarget = this.exceptionTarget;

-      string catchLabel = TranslationHelper.GenerateCatchClauseName();

-      this.exceptionTarget = catchLabel;

+    public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {

+      nestedTryCatchFinallyStatements.Add(tryCatchFinallyStatement);

       this.Visit(tryCatchFinallyStatement.TryBody);

-      this.exceptionTarget = savedExceptionTarget;

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

 

-      StmtBuilder.AddLabelCmd(catchLabel);

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

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

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

 

@@ -326,7 +359,7 @@ namespace BytecodeTranslator
       List<Bpl.Expr> typeReferences = new List<Bpl.Expr>();

       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.exceptionTarget, this.mostNestedTryStatement);

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

         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)));

@@ -342,27 +375,47 @@ namespace BytecodeTranslator
         StmtBuilder.Add(transferCmd);

       }

       else {

-        Bpl.StmtList stmtList = TranslationHelper.BuildStmtList(assignCmd, transferCmd);

+        Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(true), TranslationHelper.BuildStmtList(assignCmd, transferCmd), null, null);

         Bpl.Expr dynTypeOfOperand = this.sink.Heap.DynamicType(Bpl.Expr.Ident(this.sink.LocalExcVariable));

-        Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, dynTypeOfOperand, typeReferences[0]);

-        Bpl.IfCmd elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, expr, catchStatements[0], null, stmtList);

-        for (int i = 1; i < catchStatements.Count; i++) {

-          expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, dynTypeOfOperand, typeReferences[i]);

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

+          Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, dynTypeOfOperand, typeReferences[i]);

           elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, expr, catchStatements[i], elseIfCmd, null);

         }

         this.StmtBuilder.Add(elseIfCmd);

       }

 

-      if (finallyLabel != null) {

-        this.StmtBuilder.AddLabelCmd(finallyLabel);

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

+      if (tryCatchFinallyStatement.FinallyBody != null) {

         Visit(tryCatchFinallyStatement.FinallyBody);

       }

+      Bpl.GotoCmd dispatchCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq("DispatchContinuation"));

+      if (this.nestedTryCatchFinallyStatements.Count == 0) {

+        this.StmtBuilder.Add(dispatchCmd);

+      }

+      else {

+        Bpl.IdentifierExpr fsv = Bpl.Expr.Ident(this.sink.FinallyStackVariable);

+        this.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(fsv, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, fsv, Bpl.Expr.Literal(1))));

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

+        Bpl.GotoCmd parentCmd = new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(finallyLabel));

+        Bpl.StmtList thenList = TranslationHelper.BuildStmtList(dispatchCmd);

+        Bpl.StmtList elseList = TranslationHelper.BuildStmtList(parentCmd);

+        Bpl.IfCmd ifCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, fsv, Bpl.Expr.Literal(0)), thenList, null, elseList);

+        this.StmtBuilder.Add(ifCmd);

+      }

     }

 

     public override void Visit(IThrowStatement throwStatement) {

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

       exceptionTraverser.Visit(throwStatement.Exception);

-      StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.ExcVariable), exceptionTraverser.TranslatedExpressions.Pop()));

+      StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.ExcVariable), exceptionTraverser.TranslatedExpressions.Pop())); 

+      if (this.nestedTryCatchFinallyStatements.Count != 0) {

+        ITryCatchFinallyStatement target = this.nestedTryCatchFinallyStatements[this.nestedTryCatchFinallyStatements.Count-1];

+        int id = this.sink.FindOrCreateBoogieLabelIdentifier(this.sink.FindOrCreateCatchLabel(target));

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

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

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

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

+      }

       StmtBuilder.Add(this.ExceptionJump);

     }

 

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index 71b52864..f2b525c2 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -24,8 +24,8 @@ namespace BytecodeTranslator {
     {

       return new MetadataTraverser(sink, sourceLocationProviders);

     }

-    public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, string exceptionTarget, Dictionary<IName, ITryCatchFinallyStatement> mostNestedTryStatement) {

-      return new StatementTraverser(sink, pdbReader, contractContext, exceptionTarget, mostNestedTryStatement);

+    public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, List<ITryCatchFinallyStatement> nestedTryCatchFinallyStatements) {

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

     }

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

       return new ExpressionTraverser(sink, statementTraverser, contractContext);