further changes

2 files changed, 30 insertions, 42 deletions

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 3c5db959..4d13d638 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -913,20 +913,11 @@ namespace BytecodeTranslator {
     public int FindOrCreateCciLabelIdentifier(IName label) {

       int v;

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

-        v = cciLabels.Count + boogieLabels.Count;

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

@@ -961,7 +952,6 @@ namespace BytecodeTranslator {
       this.BeginMethod(method.ContainingType);

       this.methodBeingTranslated = method;

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

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 2e88e72c..c7b94f1a 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -97,11 +97,6 @@ namespace BytecodeTranslator
         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

@@ -298,10 +293,10 @@ namespace BytecodeTranslator
         count++;

       }

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

-      if (count != 0) {

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

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

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

       }

@@ -336,26 +331,22 @@ namespace BytecodeTranslator
     List<Tuple<ITryCatchFinallyStatement, TryCatchFinallyContext>> nestedTryCatchFinallyStatements;

     

     private void RaiseExceptionHelper(Bpl.StmtListBuilder builder) {

-      List<Bpl.Cmd> cmds = new List<Bpl.Cmd>();

       int count = nestedTryCatchFinallyStatements.Count;

       if (count == 0) {

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

       }

       else {

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

-        cmds.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable), Bpl.Expr.Literal(0)));

-        string continuationTarget = this.sink.FindOrCreateContinuationLabel(topOfStack.Item1);

-        string exceptionTarget; // jump target of the exception

+        string exceptionTarget; 

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

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

         }

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

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

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

-          int continuationId = this.sink.FindOrCreateBoogieLabelIdentifier(continuationTarget);

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

         }

         else {

-          exceptionTarget = continuationTarget;

+          exceptionTarget = this.sink.FindOrCreateContinuationLabel(topOfStack.Item1);

         }

         builder.Add(new Bpl.GotoCmd(Bpl.Token.NoToken, new Bpl.StringSeq(exceptionTarget)));

       }

@@ -373,12 +364,9 @@ namespace BytecodeTranslator
     }

 

     public override void Visit(ITryCatchFinallyStatement tryCatchFinallyStatement) {

-      int continuationId = this.sink.FindOrCreateBoogieLabelIdentifier(this.sink.FindOrCreateContinuationLabel(tryCatchFinallyStatement));

-

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

       this.Visit(tryCatchFinallyStatement.TryBody);

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

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

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

 

@@ -396,8 +384,7 @@ namespace BytecodeTranslator
           catchTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(catchClauseVariable), Bpl.Expr.Ident(this.sink.LocalExcVariable)));

         }

         catchTraverser.Visit(catchClause.Body);

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

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

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

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

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

       }

@@ -416,31 +403,42 @@ namespace BytecodeTranslator
       if (tryCatchFinallyStatement.FinallyBody != null) {

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

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

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

         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(savedFinallyStackCounterVariable), Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable)));

         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.FinallyStackCounterVariable), Bpl.Expr.Ident(savedFinallyStackCounterVariable)));

         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.IdentifierExpr fsv = Bpl.Expr.Ident(this.sink.FinallyStackCounterVariable);

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

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

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

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

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

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

-        Bpl.StmtList elseList = TranslationHelper.BuildStmtList(decrementCmd, 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);

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

       }

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