bunch of changes related to finally handling

1 files changed, 122 insertions, 34 deletions

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;

     }