Added support for translating delegates

3 files changed, 188 insertions, 7 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 5198e908..14ec1da2 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -402,7 +402,6 @@ namespace BytecodeTranslator
     /// <remarks>Stub, This one really needs comments!</remarks>

     public override void Visit(IMethodCall methodCall)

     {

-

       var resolvedMethod = methodCall.MethodToCall.ResolvedMethod;

 

       #region Translate In Parameters

@@ -475,7 +474,6 @@ namespace BytecodeTranslator
         }

         string methodname = TranslationHelper.CreateUniqueMethodName(methodCall.MethodToCall);

 

-

         Bpl.QKeyValue attrib = null;

         foreach (var a in resolvedMethod.Attributes)

         {

@@ -583,11 +581,11 @@ namespace BytecodeTranslator
     {

       TranslateArrayCreation(createArrayInstance);

     }

-

+    

     public override void Visit(ICreateDelegateInstance createDelegateInstance)

     {

-      // TranslateCreation(createDelegateInstance.MethodToCallViaDelegate, createDelegateInstance.Arguments, createDelegateInstance.Type, createDelegateInstance);

-      base.Visit(createDelegateInstance);

+      TranslateDelegateCreation(createDelegateInstance.MethodToCallViaDelegate, createDelegateInstance.Type);

+      //base.Visit(createDelegateInstance);

     }

 

     private void TranslateArrayCreation(IExpression creationAST)

@@ -644,6 +642,16 @@ namespace BytecodeTranslator
       TranslatedExpressions.Push(Bpl.Expr.Ident(a));

     }

 

+    private void TranslateDelegateCreation(IMethodReference methodToCall, ITypeReference type)

+    {

+      string methodName = TranslationHelper.CreateUniqueMethodName(methodToCall);

+      var typedIdent = new Bpl.TypedIdent(Bpl.Token.NoToken, methodName, Bpl.Type.Int);

+      var constant = new Bpl.Constant(Bpl.Token.NoToken, typedIdent, true);

+      sink.TranslatedProgram.TopLevelDeclarations.Add(constant);

+      TranslatedExpressions.Push(Bpl.Expr.Ident(constant));

+      sink.AddDelegate(type.ResolvedType, constant);

+    }

+    

     #endregion

 

     #region Translate Binary Operators

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 05fe0f82..0d0ae65e 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -56,6 +56,165 @@ namespace BytecodeTranslator {
 

     public override void Visit(IAssembly assembly) {

       base.Visit(assembly);

+      foreach (ITypeDefinition type in sink.delegateTypeToDelegates.Keys)

+      {

+        CreateDispatchMethod(type);

+      }

+    }

+

+    private void CreateDispatchMethod(ITypeDefinition type)

+    {

+      System.Diagnostics.Debug.Assert(type.IsDelegate);

+      IMethodDefinition method = null;

+      foreach (IMethodDefinition m in type.Methods)

+      {

+        if (m.Name.Value == "Invoke")

+        {

+          method = m;

+          break;

+        }

+      }

+

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

+      this.sink.BeginMethod();

+

+      try

+      {

+        #region Create in- and out-parameters

+

+        int in_count = 0;

+        int out_count = 0;

+        MethodParameter mp;

+        foreach (IParameterDefinition formal in method.Parameters)

+        {

+          mp = new MethodParameter(formal);

+          if (mp.inParameterCopy != null) in_count++;

+          if (mp.outParameterCopy != null && (formal.IsByReference || formal.IsOut))

+            out_count++;

+          formalMap.Add(formal, mp);

+        }

+        this.sink.FormalMap = formalMap;

+

+        #region Look for Returnvalue

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

+        {

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

+          out_count++;

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

+              new Bpl.TypedIdent(method.Token(),

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

+        }

+        else

+        {

+          this.sink.RetVariable = null;

+        }

+

+        #endregion

+

+        in_count++; // for the function pointer parameter

+

+        Bpl.Variable[] invars = new Bpl.Formal[in_count];

+        Bpl.Variable[] outvars = new Bpl.Formal[out_count];

+

+        int i = 0;

+        int j = 0;

+

+        // Create function pointer parameter

+        invars[i++] = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Token(), "this", Bpl.Type.Int), true);

+

+        foreach (MethodParameter mparam in formalMap.Values)

+        {

+          if (mparam.inParameterCopy != null)

+          {

+            invars[i++] = mparam.inParameterCopy;

+          }

+          if (mparam.outParameterCopy != null)

+          {

+            if (mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut)

+              outvars[j++] = mparam.outParameterCopy;

+          }

+        }

+

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

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

+        #endregion

+

+        #endregion

+

+        string MethodName = TranslationHelper.CreateUniqueMethodName(method);

+

+        Bpl.Procedure proc = new Bpl.Procedure(method.Token(),

+            MethodName, // make it unique!

+            new Bpl.TypeVariableSeq(),

+            new Bpl.VariableSeq(invars), // in

+            new Bpl.VariableSeq(outvars), // out

+            new Bpl.RequiresSeq(),

+            new Bpl.IdentifierExprSeq(),

+            new Bpl.EnsuresSeq());

+

+        this.sink.TranslatedProgram.TopLevelDeclarations.Add(proc);

+

+        List<Bpl.Block> blocks = new List<Bpl.Block>();

+        Bpl.StringSeq labelTargets = new Bpl.StringSeq();

+        Bpl.BlockSeq blockTargets = new Bpl.BlockSeq();

+        string l = "blocked";

+        Bpl.Block b = new Bpl.Block(method.Token(), l, 

+          new Bpl.CmdSeq(new Bpl.AssumeCmd(method.Token(), Bpl.Expr.False)), 

+          new Bpl.ReturnCmd(method.Token()));

+        labelTargets.Add(l);

+        blockTargets.Add(b);

+        blocks.Add(b);

+        foreach (Bpl.Constant c in sink.delegateTypeToDelegates[type])

+        {

+          Bpl.Expr bexpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(c));

+          Bpl.AssumeCmd assumeCmd = new Bpl.AssumeCmd(method.Token(), bexpr);

+          Bpl.ExprSeq ins = new Bpl.ExprSeq();

+          Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();

+          int index;

+          for (index = 1; index < invars.Length; index++)

+          {

+            ins.Add(Bpl.Expr.Ident(invars[index]));

+          }

+          for (index = 0; index < outvars.Length; index++)

+          {

+            outs.Add(Bpl.Expr.Ident(outvars[index]));

+          }

+          Bpl.CallCmd callCmd = new Bpl.CallCmd(method.Token(), c.Name, ins, outs);

+          l = "label_" + c.Name;

+          b = new Bpl.Block(method.Token(), l, new Bpl.CmdSeq(assumeCmd, callCmd), new Bpl.ReturnCmd(method.Token()));

+          labelTargets.Add(l);

+          blockTargets.Add(b);

+          blocks.Add(b);

+        }

+        Bpl.GotoCmd gotoCmd = new Bpl.GotoCmd(method.Token(), labelTargets, blockTargets);

+        Bpl.Block initialBlock = new Bpl.Block(method.Token(), "start", new Bpl.CmdSeq(), gotoCmd);

+        blocks.Insert(0, initialBlock);

+

+        Bpl.Implementation impl =

+            new Bpl.Implementation(method.Token(),

+                MethodName, // make unique

+                new Microsoft.Boogie.TypeVariableSeq(),

+                new Microsoft.Boogie.VariableSeq(invars),

+                new Microsoft.Boogie.VariableSeq(outvars),

+                new Bpl.VariableSeq(),

+                blocks

+                );

+

+        impl.Proc = proc;

+        this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl);

+      }

+      catch (TranslationException te)

+      {

+        throw new NotImplementedException(te.ToString());

+      }

+      catch

+      {

+        throw;

+      }

+      finally

+      {

+        // Maybe this is a good place to add the procedure to the toplevel declarations

+      }

     }

 

     /// <summary>

@@ -67,9 +226,9 @@ namespace BytecodeTranslator {
     public override void Visit(ITypeDefinition typeDefinition) {

 

       if (typeDefinition.IsClass) {

-

         base.Visit(typeDefinition);

-

+      } else if (typeDefinition.IsDelegate) {

+        sink.AddDelegateType(typeDefinition);

       } else {

         Console.WriteLine("Non-Class {0} was found", typeDefinition);

         throw new NotImplementedException(String.Format("Non-Class Type {0} is not yet supported.", typeDefinition.ToString()));

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 04528761..02df9b32 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -130,6 +130,20 @@ namespace BytecodeTranslator {
       this.localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();

     }

 

+    public Dictionary<ITypeDefinition, HashSet<Bpl.Constant>> delegateTypeToDelegates =

+      new Dictionary<ITypeDefinition, HashSet<Bpl.Constant>>();

+

+    public void AddDelegate(ITypeDefinition type, Bpl.Constant constant)

+    {

+      if (!delegateTypeToDelegates.ContainsKey(type))

+        delegateTypeToDelegates[type] = new HashSet<Bpl.Constant>();

+      delegateTypeToDelegates[type].Add(constant);

+    }

+

+    public void AddDelegateType(ITypeDefinition type) {

+      if (!delegateTypeToDelegates.ContainsKey(type))

+        delegateTypeToDelegates[type] = new HashSet<Bpl.Constant>();

+    }

   }

 

 }
\ No newline at end of file