beginning support for finally clauses

5 files changed, 78 insertions, 23 deletions

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 62d563c2..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, null);

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

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

       var stmts = new List<IStatement>();

 

       foreach (var f in typeDefinition.Fields) {

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

 

       try {

-

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

+        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

 

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 7910604c..b795df27 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -505,7 +505,7 @@ namespace BytecodeTranslator {
           try {

 

             foreach (IPrecondition pre in contract.Preconditions) {

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

+              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

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

 

             foreach (IPostcondition post in contract.Postconditions) {

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

+              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

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 00b2737e..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,12 +54,13 @@ namespace BytecodeTranslator
     internal readonly Stack<IExpression> operandStack = new Stack<IExpression>();

 

     #region Constructors

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

+    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

 

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

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

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

@@ -278,11 +300,18 @@ namespace BytecodeTranslator
 

     #endregion

 

-    string exceptionTarget = null;

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

-      System.Diagnostics.Debug.Assert(tryCatchFinallyStatement.FinallyBody == null);

+      string finallyLabel = null;

+      if (tryCatchFinallyStatement.FinallyBody != null) {

+        finallyLabel = TranslationHelper.GenerateFinallyClauseName();

+        nestedFinallyTargets.Push(finallyLabel);

+      }

+

       string savedExceptionTarget = this.exceptionTarget;

       string catchLabel = TranslationHelper.GenerateCatchClauseName();

       this.exceptionTarget = catchLabel;

@@ -297,7 +326,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);

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

@@ -306,15 +335,28 @@ namespace BytecodeTranslator
         catchStatements.Insert(0, catchTraverser.StmtBuilder.Collect(catchClause.Token()));

       }

 

-      Bpl.StmtList stmtList = TranslationHelper.BuildStmtList(this.ExceptionJump);

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

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

       }

-      this.StmtBuilder.Add(elseIfCmd);

     }

 

     public override void Visit(IThrowStatement throwStatement) {

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

     /// </summary>

   static class TranslationHelper {

-    public static Bpl.StmtList BuildStmtList(Bpl.TransferCmd cmd) {

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

     }

 

@@ -99,6 +106,11 @@ namespace BytecodeTranslator {
       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 23d2aca4..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, string exceptionTarget) {

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

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