Fixed declaration of procedures from static methods so that they don't have the "this" parameter.

If a method definition is marked with an attribute whose name is "AsyncAttribute", then all calls to that method have {: async } added as an attribute on the call.

4 files changed, 107 insertions, 22 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 0f288955..c484d1dd 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -328,10 +328,11 @@ namespace BytecodeTranslator {
     /// <remarks>Stub, This one really needs comments!</remarks>

     public override void Visit(IMethodCall methodCall) {

 

-      #region Translate In Parameters

+      var resolvedMethod = methodCall.MethodToCall.ResolvedMethod;

 

+      #region Translate In Parameters

 

-      Bpl.ExprSeq inexpr = new Bpl.ExprSeq();

+      var inexpr = new List<Bpl.Expr>();

 

       #region Create the 'this' argument for the function call

       if (!methodCall.IsStaticCall) {

@@ -341,7 +342,7 @@ namespace BytecodeTranslator {
       #endregion

 

       Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();

-      IEnumerator<IParameterDefinition> penum = methodCall.MethodToCall.ResolvedMethod.Parameters.GetEnumerator();

+      IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();

       penum.MoveNext();

       foreach (IExpression exp in methodCall.Arguments) {

         if (penum.Current == null) {

@@ -362,13 +363,13 @@ namespace BytecodeTranslator {
       Bpl.IToken cloc = methodCall.Token();

 

       // meeting a constructor is always something special

-      if (methodCall.MethodToCall.ResolvedMethod.IsConstructor) {

+      if (resolvedMethod.IsConstructor) {

         // Todo: do something with the constructor call

       } else {

         // Todo: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!

 

         #region Translate Out vars

-        Bpl.IdentifierExprSeq outvars = new Bpl.IdentifierExprSeq();

+        var outvars = new List<Bpl.IdentifierExpr>();

 

         foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap) {

           if (kvp.Key.IsOut || kvp.Key.IsByReference) {

@@ -386,9 +387,21 @@ namespace BytecodeTranslator {
           outvars.Add(new Bpl.IdentifierExpr(cloc, v));

           TranslatedExpressions.Push(new Bpl.IdentifierExpr(cloc, v));

         }

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

+        string methodname = TranslationHelper.CreateUniqueMethodName(resolvedMethod);

 

-        this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, methodname, inexpr, outvars));

+

+        Bpl.QKeyValue attrib = null;

+        foreach (var a in resolvedMethod.Attributes) {

+          if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {

+            attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);

+          }

+        }

+        Bpl.CallCmd call;

+        if (attrib != null)

+          call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);

+        else

+          call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);

+        this.StmtTraverser.StmtBuilder.Add(call);

 

       }

 

@@ -443,10 +456,18 @@ namespace BytecodeTranslator {
     /// "a" is a fresh local.

     /// </summary>

     public override void Visit(ICreateObjectInstance createObjectInstance) {

+      TranslateCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance.Type, createObjectInstance);

+    }

+

+    public override void Visit(ICreateDelegateInstance createDelegateInstance) {

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

+      base.Visit(createDelegateInstance);

+    }

 

-      Bpl.IToken cloc = createObjectInstance.Token();

+    private void TranslateCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, ITypeReference ctorType, IExpression creationAST) {

+      Bpl.IToken cloc = creationAST.Token();

 

-      var a = this.sink.CreateFreshLocal(createObjectInstance.Type);

+      var a = this.sink.CreateFreshLocal(creationAST.Type);

 

       // First generate an Alloc() call

       this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));

@@ -455,9 +476,9 @@ namespace BytecodeTranslator {
       Bpl.ExprSeq inexpr = new Bpl.ExprSeq();

       Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();

       inexpr.Add(Bpl.Expr.Ident(a));

-      IEnumerator<IParameterDefinition> penum = createObjectInstance.MethodToCall.ResolvedMethod.Parameters.GetEnumerator();

+      IEnumerator<IParameterDefinition> penum = ctor.ResolvedMethod.Parameters.GetEnumerator();

       penum.MoveNext();

-      foreach (IExpression exp in createObjectInstance.Arguments) {

+      foreach (IExpression exp in arguments) {

         if (penum.Current == null) {

           throw new TranslationException("More Arguments than Parameters in functioncall");

         }

@@ -473,13 +494,13 @@ namespace BytecodeTranslator {
       }

 

       Bpl.IdentifierExprSeq outvars = new Bpl.IdentifierExprSeq();

-      string methodname = TranslationHelper.CreateUniqueMethodName(createObjectInstance.MethodToCall.ResolvedMethod);

+      string methodname = TranslationHelper.CreateUniqueMethodName(ctor.ResolvedMethod);

 

       this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, methodname, inexpr, outvars));

 

       TranslatedExpressions.Push(Bpl.Expr.Ident(a));

-

     }

+

     #endregion

     

     #region Translate Binary Operators

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 7f6d95b7..29b11ef4 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -116,13 +116,15 @@ namespace BytecodeTranslator {
 

         #endregion

 

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

         #region Create 'this' parameter

-        in_count++;

-        Bpl.Type selftype = Bpl.Type.Int;

-        Bpl.Formal self = new Bpl.Formal(method.Token(),

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

-                "this", selftype), true);

-

+        if (!method.IsStatic) {

+          in_count++;

+          Bpl.Type selftype = Bpl.Type.Int;

+          self = new Bpl.Formal(method.Token(),

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

+                  "this", selftype), true);

+        }

         #endregion

 

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

@@ -132,7 +134,8 @@ namespace BytecodeTranslator {
         int j = 0;

 

         #region Add 'this' parameter as first in parameter

-        invars[i++] = self;

+        if (!method.IsStatic)

+          invars[i++] = self;

         #endregion

 

         foreach (MethodParameter mparam in formalMap.Values) {

diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs
index 39188b03..7d57a0a9 100644
--- a/BCT/RegressionTests/RegressionTestInput/Class1.cs
+++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs
@@ -5,6 +5,10 @@ using System.Text;
 using System.Diagnostics.Contracts;

 

 namespace RegressionTestInput {

+

+  [AttributeUsage(AttributeTargets.Method)]

+  public class AsyncAttribute : Attribute { }

+

   public class Class0 {

 

     static int StaticInt;

@@ -41,5 +45,15 @@ namespace RegressionTestInput {
       return x;

     }

 

+    [Async]

+    int MethodThatRepresentsAnAynchronousMethod(int x) {

+      return x;

+    }

+

+    int CallAsyncMethod(int y) {

+      return MethodThatRepresentsAnAynchronousMethod(y);

+    }

+

+

   }

 }

diff --git a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
index bc72f5bf..c1258e1d 100644
--- a/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
+++ b/BCT/RegressionTests/TranslationTest/RegressionTestInput.txt
@@ -21,13 +21,24 @@ axiom (forall T: TName :: !($typeof(ClassRepr(T)) <: System.Object));
 axiom (forall T: TName :: ClassRepr(T) != null);

 axiom (forall h: HeapType, c: TName :: { h[ClassRepr(c), $allocated] } IsHeap(h) ==> h[ClassRepr(c), $allocated]);

 

+procedure RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int);

+

+

+

+implementation RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int)

+{

+    return;

+}

+

+

+

 var RegressionTestInput.Class0.StaticInt: int;

 

-procedure RegressionTestInput.Class0.StaticMethod$System.Int32(this: int, x$in: int) returns ($result: int);

+procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);

 

 

 

-implementation RegressionTestInput.Class0.StaticMethod$System.Int32(this: int, x$in: int) returns ($result: int)

+implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

 {

   var x: int;

   var local_0: int;

@@ -139,6 +150,42 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int
 

 

 

+procedure RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

+{

+  var x: int;

+  var local_0: int;

+

+    x := x$in;

+    local_0 := x;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)

+{

+  var y: int;

+  var local_0: int;

+  var $tmp2: int;

+

+    y := y$in;

+    call {:async} $tmp2 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);

+    local_0 := $tmp2;

+    $result := local_0;

+    return;

+}

+

+

+

 procedure RegressionTestInput.Class0..ctor$System.Void(this: int);