Added a new type, Type, that represents runtime types. The Heap interface now provides a way to declare a new user-defined type and to represent the expressions "typeof(T)" or "o.Type" in the BPL program using a new function $DynamicType. Added a method to the Sink so that any of the translation visitors can find or declare a new type. When an object is allocated, an assumption is generated that gives its dynamic type.

Fixed the dynamic dispatch inlining so that the $DynamicType of the object is used to decide which override to call.

7 files changed, 164 insertions, 8 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 82e37212..75f376f5 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -473,7 +473,8 @@ namespace BytecodeTranslator
           outvars.Add(new Bpl.IdentifierExpr(cloc, v));

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

         }

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

+        var proc = this.sink.FindOrCreateProcedure(resolvedMethod, resolvedMethod.IsStatic);

+        string methodname = proc.Name;

 

         Bpl.QKeyValue attrib = null;

         foreach (var a in resolvedMethod.Attributes)

@@ -605,12 +606,12 @@ namespace BytecodeTranslator
 

     private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, ITypeReference ctorType, IExpression creationAST)

     {

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

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

 

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

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

 

       // Second, generate the call to the appropriate ctor

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

@@ -639,7 +640,17 @@ namespace BytecodeTranslator
       Bpl.IdentifierExprSeq outvars = new Bpl.IdentifierExprSeq();

       string methodname = TranslationHelper.CreateUniqueMethodName(ctor);

 

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

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

+

+      // Generate assumption about the dynamic type of the just allocated object

+      this.StmtTraverser.StmtBuilder.Add(

+        new Bpl.AssumeCmd(token, 

+          Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

+          this.sink.Heap.DynamicType(inexpr[0]),

+          Bpl.Expr.Ident(this.sink.FindOrCreateType(creationAST.Type))

+          )

+          )

+        );

 

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

     }

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 133aeed5..6171c4e9 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -89,6 +89,15 @@ procedure {:inline 1} Alloc() returns (x: int)
     }

 

     /// <summary>

+    /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

+    /// on its type based on the heap representation. I.e., the value of this

+    /// variable represents the value of the expression "typeof(type)".

+    /// </summary>

+    public Bpl.Variable CreateTypeVariable(ITypeReference type) {

+      return null;

+    }

+

+    /// <summary>

     /// Returns the (typed) BPL expression that corresponds to the value of the field

     /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when

     /// <paramref name="o"/> is non-null, otherwise the value of the static field.

@@ -118,6 +127,14 @@ procedure {:inline 1} Alloc() returns (x: int)
           new Bpl.IdentifierExpr(tok, this.HeapVariable), new Bpl.ExprSeq(o, f), value);

     }

 

+    /// <summary>

+    /// Returns the BPL expression that corresponds to the value of the dynamic type

+    /// of the object represented by the expression <paramref name="o"/>.

+    /// </summary>

+    public Bpl.Expr DynamicType(Bpl.Expr o) {

+      // $DymamicType(o)

+      return null;

+    }

 

   }

 

@@ -183,6 +200,15 @@ procedure {:inline 1} Alloc() returns (x: int)
       }

 

       /// <summary>

+      /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

+      /// on its type based on the heap representation. I.e., the value of this

+      /// variable represents the value of the expression "typeof(type)".

+      /// </summary>

+      public Bpl.Variable CreateTypeVariable(ITypeReference type) {

+        return null;

+      }

+

+      /// <summary>

       /// Returns the (typed) BPL expression that corresponds to the value of the field

       /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when

       /// <paramref name="o"/> is non-null, otherwise the value of the static field.

@@ -209,6 +235,16 @@ procedure {:inline 1} Alloc() returns (x: int)
         else

           return Bpl.Cmd.MapAssign(tok, f, o, value);

       }

+

+      /// <summary>

+      /// Returns the BPL expression that corresponds to the value of the dynamic type

+      /// of the object represented by the expression <paramref name="o"/>.

+      /// </summary>

+      public Bpl.Expr DynamicType(Bpl.Expr o) {

+        // $DymamicType(o)

+        return null;

+      }

+

     }

 

   }

@@ -291,6 +327,15 @@ procedure {:inline 1} Alloc() returns (x: int)
     }

 

     /// <summary>

+    /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

+    /// on its type based on the heap representation. I.e., the value of this

+    /// variable represents the value of the expression "typeof(type)".

+    /// </summary>

+    public Bpl.Variable CreateTypeVariable(ITypeReference type) {

+      return null;

+    }

+

+    /// <summary>

     /// Returns the (typed) BPL expression that corresponds to the value of the field

     /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when

     /// <paramref name="o"/> is non-null, otherwise the value of the static field.

@@ -352,6 +397,15 @@ procedure {:inline 1} Alloc() returns (x: int)
       }

     }

 

+    /// <summary>

+    /// Returns the BPL expression that corresponds to the value of the dynamic type

+    /// of the object represented by the expression <paramref name="o"/>.

+    /// </summary>

+    public Bpl.Expr DynamicType(Bpl.Expr o) {

+      // $DymamicType(o)

+      return null;

+    }

+

   }

 

   /// <summary>

@@ -363,6 +417,10 @@ procedure {:inline 1} Alloc() returns (x: int)
 

     #region Fields

 

+    [RepresentationFor("Type", "type Type;")]

+    private Bpl.TypeCtorDecl TypeTypeDecl = null;

+    private Bpl.CtorType TypeType;

+

     [RepresentationFor("Field", "type Field;")]

     private Bpl.TypeCtorDecl FieldTypeDecl = null;

     private Bpl.CtorType FieldType;

@@ -386,7 +444,10 @@ procedure {:inline 1} Alloc() returns (x: int)
     private Bpl.Function Read = null;

 

     [RepresentationFor("Write", "function {:inline true} Write(H:HeapType, o:ref, f:Field, v:box): HeapType { H[o,f := v] }")]

-    private Bpl.Function Write = null; 

+    private Bpl.Function Write = null;

+

+    [RepresentationFor("$DynamicType", "function $DynamicType(ref): Type;")]

+    public Bpl.Function DymamicType = null;

 

     /// <summary>

     /// Prelude text for which access to the ASTs is not needed

@@ -420,6 +481,7 @@ procedure {:inline 1} Alloc() returns (x: ref)
       var b = RepresentationFor.ParsePrelude(this.InitialPreludeText, this, out program);

       if (b) {

         this.FieldType = new Bpl.CtorType(this.FieldTypeDecl.tok, this.FieldTypeDecl, new Bpl.TypeSeq());

+        this.TypeType = new Bpl.CtorType(this.TypeTypeDecl.tok, this.TypeTypeDecl, new Bpl.TypeSeq());

       }

       return b;

     }

@@ -448,6 +510,21 @@ procedure {:inline 1} Alloc() returns (x: ref)
     private Dictionary<Bpl.Variable, ITypeReference> underlyingTypes = new Dictionary<Bpl.Variable, ITypeReference>();

 

     /// <summary>

+    /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

+    /// on its type based on the heap representation. I.e., the value of this

+    /// variable represents the value of the expression "typeof(type)".

+    /// </summary>

+    public Bpl.Variable CreateTypeVariable(ITypeReference type) {

+      Bpl.Variable v;

+      string typename = TypeHelper.GetTypeName(type);

+      Bpl.IToken tok = type.Token();

+      Bpl.Type t = this.TypeType;

+      Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, t);

+      v = new Bpl.Constant(tok, tident, true);

+      return v;

+    }

+

+    /// <summary>

     /// Returns the (typed) BPL expression that corresponds to the value of the field

     /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when

     /// <paramref name="o"/> is non-null, otherwise the value of the static field.

@@ -519,6 +596,20 @@ procedure {:inline 1} Alloc() returns (x: ref)
       }

     }

 

+    /// <summary>

+    /// Returns the BPL expression that corresponds to the value of the dynamic type

+    /// of the object represented by the expression <paramref name="o"/>.

+    /// </summary>

+    public Bpl.Expr DynamicType(Bpl.Expr o) {

+      // $DymamicType(o)

+      var callDynamicType = new Bpl.NAryExpr(

+        o.tok,

+        new Bpl.FunctionCall(this.DymamicType),

+        new Bpl.ExprSeq(o)

+        );

+      return callDynamicType;

+    }

+

   }

 

   internal class RepresentationFor : Attribute {

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index d35d12b3..fd1f312e 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -31,6 +31,13 @@ namespace BytecodeTranslator {
     Bpl.Variable CreateFieldVariable(IFieldReference field);

 

     /// <summary>

+    /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding

+    /// on its type based on the heap representation. I.e., the value of this

+    /// variable represents the value of the expression "typeof(type)".

+    /// </summary>

+    Bpl.Variable CreateTypeVariable(ITypeReference type);

+

+    /// <summary>

     /// Returns the (typed) BPL expression that corresponds to the value of the field

     /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when

     /// <paramref name="o"/> is non-null, otherwise the value of the static field.

@@ -51,6 +58,12 @@ namespace BytecodeTranslator {
     /// </summary>

     Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value);

 

+    /// <summary>

+    /// Returns the BPL expression that corresponds to the value of the dynamic type

+    /// of the object represented by the expression <paramref name="o"/>.

+    /// </summary>

+    Bpl.Expr DynamicType(Bpl.Expr o);

+

   }

 

   public abstract class HeapFactory {

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index bb2c08f2..14923bff 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -224,6 +224,7 @@ namespace BytecodeTranslator {
     public override void Visit(ITypeDefinition typeDefinition) {

 

       if (typeDefinition.IsClass) {

+        sink.FindOrCreateType(typeDefinition);

         base.Visit(typeDefinition);

       } else if (typeDefinition.IsDelegate) {

         sink.AddDelegateType(typeDefinition);

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 1fefbe97..956cb71d 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -127,7 +127,7 @@ namespace BytecodeTranslator {
     /// </summary>

     private Dictionary<uint, Bpl.Variable> declaredFields = new Dictionary<uint, Bpl.Variable>();

 

-    public Bpl.Procedure FindOrCreateProcedure(IMethodReference method, bool isStatic) {

+    public Bpl.Procedure FindOrCreateProcedure(IMethodDefinition method, bool isStatic) {

       Bpl.Procedure proc;

       var key = method.InternedKey;

       if (!this.declaredMethods.TryGetValue(key, out proc)) {

@@ -269,6 +269,29 @@ namespace BytecodeTranslator {
       }

       return proc;

     }

+

+    /// <summary>

+    /// Creates a fresh variable that represents the type of

+    /// <paramref name="type"/> in the Bpl program. I.e., its

+    /// value represents the expression "typeof(type)".

+    /// </summary>

+    public Bpl.Variable FindOrCreateType(ITypeReference type) {

+      // The Heap has to decide how to represent the field (i.e., its type),

+      // all the Sink cares about is adding a declaration for it.

+      Bpl.Variable t;

+      var key = type.InternedKey;

+      if (!this.declaredTypes.TryGetValue(key, out t)) {

+        t = this.Heap.CreateTypeVariable(type);

+        this.declaredTypes.Add(key, t);

+        this.TranslatedProgram.TopLevelDeclarations.Add(t);

+      }

+      return t;

+    }

+    /// <summary>

+    /// The keys to the table are the interned key of the type.

+    /// </summary>

+    private Dictionary<uint, Bpl.Variable> declaredTypes = new Dictionary<uint, Bpl.Variable>();

+

     /// <summary>

     /// The keys to the table are the interned key of the field.

     /// </summary>

diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index be3c06a5..29b75d82 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -182,7 +182,9 @@ namespace BytecodeTranslator {
 

         var elseBranch = new Bpl.StmtListBuilder();

 

-        var methodname = TranslationHelper.CreateUniqueMethodName(methodCall.MethodToCall);

+        var proc = this.sink.FindOrCreateProcedure(resolvedMethod, resolvedMethod.IsStatic);

+        var methodname = proc.Name;

+

         Bpl.CallCmd call;

         if (attrib != null)

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

@@ -202,7 +204,10 @@ namespace BytecodeTranslator {
             call = new Bpl.CallCmd(token, methodname, inexpr, outvars);

           thenBranch.Add(call);

           ifcmd = new Bpl.IfCmd(token,

-            Bpl.LiteralExpr.True,

+            Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,

+            this.sink.Heap.DynamicType(inexpr[0]),

+            Bpl.Expr.Ident(this.sink.FindOrCreateType(m.ContainingType))

+            ),

             thenBranch.Collect(token),

             null,

             elseBranch.Collect(token)

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index ea98c61b..d200d8d8 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -31,6 +31,8 @@ implementation Alloc() returns (x: ref)
 

 

 

+type Type;

+

 type Field;

 

 var $Heap: HeapType where IsGoodHeap($Heap);

@@ -53,6 +55,10 @@ function {:inline true} Write(H: HeapType, o: ref, f: Field, v: box) : HeapType
   H[o, f := v]

 }

 

+function $DynamicType(ref) : Type;

+

+const unique RegressionTestInput.AsyncAttribute: Type;

+

 procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);

 

 

@@ -64,6 +70,8 @@ implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
 

 

 

+const unique RegressionTestInput.ClassWithBoolTypes: Type;

+

 var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

 

 const unique RegressionTestInput.ClassWithBoolTypes.b: Field;

@@ -132,6 +140,8 @@ implementation RegressionTestInput.ClassWithBoolTypes.Main()
 

 

 

+const unique RegressionTestInput.ClassWithArrayTypes: Type;

+

 var RegressionTestInput.ClassWithArrayTypes.s: int;

 

 const unique RegressionTestInput.ClassWithArrayTypes.a: Field;

@@ -257,6 +267,8 @@ implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)
 

 

 

+const unique RegressionTestInput.Class0: Type;

+

 var RegressionTestInput.Class0.StaticInt: int;

 

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