using registerAsLatest directly to deal with multiple dll translation

9 files changed, 217 insertions, 84 deletions

diff --git a/.hgtags b/.hgtags
index e69de29b..6e2337a0 100644
--- a/.hgtags
+++ b/.hgtags
@@ -0,0 +1,2 @@
+42ab6e4ab0b1f5e66b0d142df0df98c9495414f5 emicvccbld_build_2.1.30608.0
+7dffe3976b9dcd1153c2b03e5a3d04278eee1633 emicvccbld_build_2.1.30608.1
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 99fbdc28..e2d0d636 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -566,6 +566,9 @@ namespace BytecodeTranslator
         this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));

       }

 

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

+      Bpl.StmtList thenStmt = TranslationHelper.BuildStmtList(this.StmtTraverser.ExceptionJump);

+      this.StmtTraverser.StmtBuilder.Add(new Bpl.IfCmd(methodCall.Token(), expr, thenStmt, null, null));

     }

 

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

@@ -634,9 +637,8 @@ namespace BytecodeTranslator
         }

       }

 

-      var proc = this.sink.FindOrCreateProcedure(resolvedMethod);

-      

-      var translateAsFunctionCall = proc is Bpl.Function;

+      var procInfo = this.sink.FindOrCreateProcedure(resolvedMethod);

+      var translateAsFunctionCall = procInfo.Decl is Bpl.Function;

       if (!translateAsFunctionCall) {

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

           Bpl.Variable v = this.sink.CreateFreshLocal(methodToCall.ResolvedMethod.Type.ResolvedType);

@@ -650,9 +652,10 @@ namespace BytecodeTranslator
           }

           TranslatedExpressions.Push(unboxed);

         }

+        outvars.Add(Bpl.Expr.Ident(procInfo.ExcVariable));

       }

 

-      return proc;

+      return procInfo.Decl;

     }

 

     #endregion

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index b816a439..5b61a6ca 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);

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

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

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

       var stmts = new List<IStatement>();

 

       foreach (var f in typeDefinition.Fields) {

@@ -262,12 +262,12 @@ namespace BytecodeTranslator {
         return;

 

 

-      Sink.ProcedureInfo procAndFormalMap;

+      Sink.ProcedureInfo procInfo;

       IMethodDefinition stubMethod = null;

       if (IsStubMethod(method, out stubMethod)) {

-        procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(stubMethod);

+        procInfo = this.sink.FindOrCreateProcedure(stubMethod);

       } else {

-        procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(method);

+        procInfo = this.sink.FindOrCreateProcedure(method);

       }

 

       if (method.IsAbstract) { // we're done, just define the procedure

@@ -275,14 +275,14 @@ namespace BytecodeTranslator {
       }

 

       this.sink.BeginMethod(method);

-      var decl = procAndFormalMap.Decl;

+      var decl = procInfo.Decl;

       var proc = decl as Bpl.Procedure;

-      var formalMap = procAndFormalMap.FormalMap;

-      this.sink.RetVariable = procAndFormalMap.ReturnVariable;

+      var formalMap = procInfo.FormalMap;

 

       try {

-

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

+        MostNestedTryStatementTraverser tryStatementTraverser = new MostNestedTryStatementTraverser();

+        tryStatementTraverser.Visit(method.Body);

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

 

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

 

@@ -373,7 +373,7 @@ namespace BytecodeTranslator {
         foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {

           vars.Add(v);

         }

-

+        vars.Add(procInfo.LocalExcVariable);

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

         #endregion

 

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index b9f71268..d447874a 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -124,7 +124,7 @@ namespace BytecodeTranslator {
           pdbReader = new PdbReader(pdbStream, host);

         }

         module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;

-        host.HelperRegisterAsLatest(module);

+        host.RegisterAsLatest(module);

         modules.Add(module);

         contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));

         pdbReaders.Add(module, pdbReader);

@@ -241,7 +241,7 @@ namespace BytecodeTranslator {
       }

 

       try {

-        var decl = sink.FindOrCreateProcedure(invokeMethod);

+        var decl = sink.FindOrCreateProcedure(invokeMethod).Decl;

         var proc = decl as Bpl.Procedure;

         var invars = proc.InParams;

         var outvars = proc.OutParams;

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 6e6b7b9b..4476b7f7 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -41,7 +41,7 @@ namespace BytecodeTranslator {
         foreach (var d in this.TranslatedProgram.TopLevelDeclarations) {

           var p = d as Bpl.Procedure;

           if (p != null) {

-            this.initiallyDeclaredProcedures.Add(p.Name, p);

+            this.initiallyDeclaredProcedures.Add(p.Name, new ProcedureInfo(p));

           }

         }

       }

@@ -52,8 +52,10 @@ namespace BytecodeTranslator {
     }

     readonly Heap heap;

 

-    public Bpl.Variable ThisVariable;

-    public Bpl.Variable RetVariable;

+    public Bpl.Formal ThisVariable;

+    public Bpl.Formal RetVariable;

+    public Bpl.Formal ExcVariable;

+    public Bpl.LocalVariable LocalExcVariable;

 

     public readonly string AllocationMethodName = "Alloc";

     public readonly string StaticFieldFunction = "ClassRepr";

@@ -312,49 +314,69 @@ namespace BytecodeTranslator {
     public struct ProcedureInfo {

       private Bpl.DeclWithFormals decl;

       private Dictionary<IParameterDefinition, MethodParameter> formalMap;

-      private Bpl.Variable returnVariable;

+      private Bpl.Formal thisVariable;

+      private Bpl.Formal returnVariable;

+      private Bpl.Formal excVariable;

+      private Bpl.LocalVariable localExcVariable;

       private List<Bpl.Formal> typeParameters;

       private List<Bpl.Formal> methodParameters;

 

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

+      public ProcedureInfo(Bpl.DeclWithFormals decl) {

+        this.decl = decl;

+        this.formalMap = null;

+        this.returnVariable = null;

+        this.thisVariable = null;

+        this.excVariable = null;

+        this.localExcVariable = 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, Bpl.Variable returnVariable, List<Bpl.Formal> typeParameters, List<Bpl.Formal> methodParameters) {

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

         this.returnVariable = returnVariable;

+        this.thisVariable = thisVariable;

+        this.excVariable = excVariable;

+        this.localExcVariable = localExcVariable;

         this.typeParameters = typeParameters;

         this.methodParameters = methodParameters;

       }

 

       public Bpl.DeclWithFormals Decl { get { return decl; } }

       public Dictionary<IParameterDefinition, MethodParameter> FormalMap { get { return formalMap; } }

-      public Bpl.Variable ReturnVariable { get { return returnVariable; } }

+      public Bpl.Formal ThisVariable { get { return thisVariable; } }

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

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

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

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

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

     }

 

-    public Bpl.DeclWithFormals FindOrCreateProcedure(IMethodDefinition method) {

-      ProcedureInfo procAndFormalMap;

-

+    public ProcedureInfo FindOrCreateProcedure(IMethodDefinition method) {

+      ProcedureInfo procInfo;

       var key = method.InternedKey;

 

-      if (!this.declaredMethods.TryGetValue(key, out procAndFormalMap)) {

-

+      if (!this.declaredMethods.TryGetValue(key, out procInfo)) {

         string MethodName = TranslationHelper.CreateUniqueMethodName(method);

+        if (this.initiallyDeclaredProcedures.TryGetValue(MethodName, out procInfo)) return procInfo;

 

-        Bpl.Procedure p;

-        if (this.initiallyDeclaredProcedures.TryGetValue(MethodName, out p)) return p;

-

-        #region Create in- and out-parameters

-

+        Bpl.Formal thisVariable = null;

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

+        

         int in_count = 0;

-        int out_count = 0;

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

         MethodParameter mp;

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

         foreach (IParameterDefinition formal in method.Parameters) {

@@ -365,31 +387,17 @@ namespace BytecodeTranslator {
           formalMap.Add(formal, mp);

         }

 

-        #region Look for Returnvalue

-

-        Bpl.Variable savedRetVariable = this.RetVariable;

-

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

           Bpl.Type rettype = CciTypeToBoogie(method.Type);

           out_count++;

-          this.RetVariable = new Bpl.Formal(method.Token(),

-              new Bpl.TypedIdent(method.Type.Token(),

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

-        } else {

-          this.RetVariable = null;

+          retVariable = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), "$result", rettype), false);

         }

 

-        #endregion

-

-        Bpl.Formal/*?*/ self = null;

-        #region Create 'this' parameter

         if (!method.IsStatic) {

           var selfType = CciTypeToBoogie(method.ContainingType);

           in_count++;

-          var self_name = method.ContainingTypeDefinition.IsStruct ? "this$in" : "this";

-          self = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), self_name, selfType), true);

+          thisVariable = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), "$this", selfType), true);

         }

-        #endregion

 

         List<Bpl.Formal> typeParameters = new List<Bpl.Formal>();

         ITypeDefinition containingType = method.ContainingType.ResolvedType;

@@ -419,10 +427,8 @@ namespace BytecodeTranslator {
         int i = 0;

         int j = 0;

 

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

-        if (self != null)

-          invars[i++] = self;

-        #endregion

+        if (thisVariable != null)

+          invars[i++] = thisVariable;

 

         foreach (MethodParameter mparam in formalMap.Values) {

           if (mparam.inParameterCopy != null) {

@@ -434,10 +440,6 @@ namespace BytecodeTranslator {
           }

         }

 

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

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

-        #endregion

-

         if (method.IsStatic) {

           foreach (Bpl.Formal f in typeParameters) {

             invars[i++] = f;

@@ -446,7 +448,10 @@ namespace BytecodeTranslator {
         foreach (Bpl.Formal f in methodParameters) {

           invars[i++] = f;

         }

-        #endregion

+

+        if (retVariable != null) outvars[j++] = retVariable;

+

+        outvars[j++] = excVariable;

 

         var tok = method.Token();

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

@@ -458,7 +463,7 @@ namespace BytecodeTranslator {
           var func = new Bpl.Function(tok,

             MethodName,

             new Bpl.VariableSeq(invars),

-            this.RetVariable);

+            retVariable);

           decl = func;

         } else {

           var proc = new Bpl.Procedure(tok,

@@ -484,8 +489,8 @@ namespace BytecodeTranslator {
         } else {

           this.TranslatedProgram.TopLevelDeclarations.Add(decl);

         }

-        procAndFormalMap = new ProcedureInfo(decl, formalMap, this.RetVariable, typeParameters, methodParameters);

-        this.declaredMethods.Add(key, procAndFormalMap);

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

+        this.declaredMethods.Add(key, procInfo);

 

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

         // table because information in them might be needed (e.g., if a parameter is mentioned

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

 

             foreach (IPrecondition pre in contract.Preconditions) {

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

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

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

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

               // Todo: Deal with Descriptions

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

 

             foreach (IPostcondition post in contract.Postconditions) {

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

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

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

               exptravers.Visit(post.Condition);

               // Todo: Deal with Descriptions

@@ -554,10 +559,8 @@ namespace BytecodeTranslator {
           }

         }

         #endregion

-

-        this.RetVariable = savedRetVariable;

       }

-      return procAndFormalMap.Decl;

+      return procInfo;

     }

 

     private Dictionary<uint, ProcedureInfo> declaredStructDefaultCtors = new Dictionary<uint, ProcedureInfo>();

@@ -676,11 +679,6 @@ namespace BytecodeTranslator {
       return false;

     }

 

-    public ProcedureInfo FindOrCreateProcedureAndReturnProcAndFormalMap(IMethodDefinition method) {

-      this.FindOrCreateProcedure(method);

-      var key = method.InternedKey;

-      return this.declaredMethods[key];

-    }

     public static IMethodReference Unspecialize(IMethodReference method) {

       IMethodReference result = method;

       var gmir = result as IGenericMethodInstanceReference;

@@ -753,7 +751,7 @@ namespace BytecodeTranslator {
           containingType = containingType.ContainingTypeDefinition as INestedTypeDefinition;

         }

 

-        ProcedureInfo info = FindOrCreateProcedureAndReturnProcAndFormalMap(methodBeingTranslated);

+        ProcedureInfo info = FindOrCreateProcedure(methodBeingTranslated);

         if (methodBeingTranslated.IsStatic) {

           return Bpl.Expr.Ident(info.TypeParameter(index));

         }

@@ -765,7 +763,7 @@ namespace BytecodeTranslator {
 

       IGenericMethodParameter gmp = type as IGenericMethodParameter;

       if (gmp != null) {

-        ProcedureInfo info = FindOrCreateProcedureAndReturnProcAndFormalMap(methodBeingTranslated);

+        ProcedureInfo info = FindOrCreateProcedure(methodBeingTranslated);

         return Bpl.Expr.Ident(info.TypeParameter(gmp.Index));

       }

 

@@ -864,12 +862,15 @@ namespace BytecodeTranslator {
     /// The values in this table are the procedures

     /// defined in the program created by the heap in the Sink's ctor.

     /// </summary>

-    private Dictionary<string, Bpl.Procedure> initiallyDeclaredProcedures = new Dictionary<string, Bpl.Procedure>();

+    private Dictionary<string, ProcedureInfo> initiallyDeclaredProcedures = new Dictionary<string, ProcedureInfo>();

 

     public void BeginMethod(ITypeReference containingType) {

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

       this.localCounter = 0;

-      this.ThisVariable = new Bpl.LocalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "this", this.Heap.RefType));

+      this.ThisVariable = null;

+      this.RetVariable = null;

+      this.ExcVariable = null;

+      this.LocalExcVariable = null;

       this.methodBeingTranslated = null;

     }

 

@@ -877,6 +878,11 @@ namespace BytecodeTranslator {
     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;

     }

 

     public void BeginAssembly(IAssembly assembly) {

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index f03894a2..8310374f 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -20,6 +20,27 @@ using System.Diagnostics.Contracts;
 

 namespace BytecodeTranslator

 {

+  public class MostNestedTryStatementTraverser : BaseCodeTraverser {

+    Dictionary<IName, ITryCatchFinallyStatement> mostNestedTryStatement = new Dictionary<IName, ITryCatchFinallyStatement>();

+    ITryCatchFinallyStatement currStatement = null;

+    public override void Visit(ILabeledStatement labeledStatement) {

+      if (currStatement != null)

+        mostNestedTryStatement.Add(labeledStatement.Label, currStatement);

+      base.Visit(labeledStatement);

+    }

+    public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {

+      ITryCatchFinallyStatement savedStatement = currStatement;

+      currStatement = tryCatchFinallyStatement;

+      base.Visit(tryCatchFinallyStatement);

+      currStatement = savedStatement;

+    }

+    public ITryCatchFinallyStatement MostNestedTryStatement(IName label) {

+      if (!mostNestedTryStatement.ContainsKey(label))

+        return null;

+      return mostNestedTryStatement[label];

+    }

+  }

+

   public class StatementTraverser : BaseCodeTraverser {

 

     public readonly TraverserFactory factory;

@@ -33,11 +54,13 @@ namespace BytecodeTranslator
     internal readonly Stack<IExpression> operandStack = new Stack<IExpression>();

 

     #region Constructors

-    public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {

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

       this.sink = sink;

       this.factory = sink.Factory;

       PdbReader = pdbReader;

       this.contractContext = contractContext;

+      this.exceptionTarget = exceptionTarget;

+      this.mostNestedTryStatement = mostNestedTryStatement;

     }

     #endregion

 

@@ -131,8 +154,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);

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

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

 

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

       condTraverser.Visit(conditionalStatement.Condition);

@@ -277,6 +300,76 @@ 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);

+      }

+

+      string savedExceptionTarget = this.exceptionTarget;

+      string catchLabel = TranslationHelper.GenerateCatchClauseName();

+      this.exceptionTarget = catchLabel;

+      this.Visit(tryCatchFinallyStatement.TryBody);

+      this.exceptionTarget = savedExceptionTarget;

+

+      StmtBuilder.AddLabelCmd(catchLabel);

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

+

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

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

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

+        }

+        catchTraverser.Visit(catchClause.Body);

+        catchStatements.Insert(0, catchTraverser.StmtBuilder.Collect(catchClause.Token()));

+      }

+

+      Bpl.AssignCmd assignCmd = TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.ExcVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable));

+      Bpl.TransferCmd transferCmd = this.ExceptionJump;

+      if (catchStatements.Count == 0) {

+        StmtBuilder.Add(assignCmd);

+        StmtBuilder.Add(transferCmd);

+      }

+      else {

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

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

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

+        }

+        this.StmtBuilder.Add(elseIfCmd);

+      }

+

+      if (finallyLabel != null) {

+        this.StmtBuilder.AddLabelCmd(finallyLabel);

+        Visit(tryCatchFinallyStatement.FinallyBody);

+      }

+    }

+

+    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(this.ExceptionJump);

+    }

+

+    public override void Visit(IRethrowStatement rethrowStatement) {

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

+      StmtBuilder.Add(this.ExceptionJump);

+    }

   }

 

 }

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index cf856024..98337f51 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -61,6 +61,25 @@ namespace BytecodeTranslator {
     /// from Cci to Boogie

     /// </summary>

   static class TranslationHelper {

+    public static Bpl.StmtList BuildStmtList(Bpl.Cmd cmd, Bpl.TransferCmd tcmd) {

+      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

+      builder.Add(cmd);

+      builder.Add(tcmd);

+      return builder.Collect(Bpl.Token.NoToken);

+    }

+

+    public static Bpl.StmtList BuildStmtList(Bpl.TransferCmd tcmd) {

+      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

+      builder.Add(tcmd);

+      return builder.Collect(Bpl.Token.NoToken);

+    }

+

+    public static Bpl.StmtList BuildStmtList(params Bpl.Cmd[] cmds) {

+      Bpl.StmtListBuilder builder = new Bpl.StmtListBuilder();

+      foreach (Bpl.Cmd cmd in cmds)

+        builder.Add(cmd);

+      return builder.Collect(Bpl.Token.NoToken);

+    }

 

     public static Bpl.AssignCmd BuildAssignCmd(Bpl.IdentifierExpr lhs, Bpl.Expr rhs)

     {

@@ -82,6 +101,16 @@ namespace BytecodeTranslator {
       return "$tmp" + (tmpVarCounter++).ToString();

     }

 

+    internal static int catchClauseCounter = 0;

+    public static string GenerateCatchClauseName() {

+      return "catch" + (catchClauseCounter++).ToString();

+    }

+

+    internal static int finallyClauseCounter = 0;

+    public static string GenerateFinallyClauseName() {

+      return "finally" + (finallyClauseCounter++).ToString();

+    }

+

     public static string CreateUniqueMethodName(IMethodReference method) {

       var containingTypeName = TypeHelper.GetTypeName(method.ContainingType, NameFormattingOptions.None);

       var s = MemberHelper.GetMethodSignature(method, NameFormattingOptions.DocumentationId);

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index 78c818bd..71b52864 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) {

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

+    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 ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {

       return new ExpressionTraverser(sink, statementTraverser, contractContext);

diff --git a/BCT/Samples/Exceptions/ExceptionsExample.cs b/BCT/Samples/Exceptions/ExceptionsExample.cs
index 176d0339..5efb69b7 100644
--- a/BCT/Samples/Exceptions/ExceptionsExample.cs
+++ b/BCT/Samples/Exceptions/ExceptionsExample.cs
@@ -27,7 +27,7 @@ class PoirotMain
         {

             x = 34;

         }

-        Contract.Assert(x == 34);

+        Contract.Assert(x == 35);

     }

 }