Fix translation of "is" operator.

Fix generation of type constants to avoid infinite loops for recursive type
definitions.

2 files changed, 26 insertions, 7 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index b53eccef..7e7de866 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -1294,7 +1294,10 @@ namespace BytecodeTranslator
       base.Visit(checkIfInstance.Operand);

       var exp = TranslatedExpressions.Pop();

       var dynTypeOfOperand = this.sink.Heap.DynamicType(exp);

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, dynTypeOfOperand, e));

+      var subtype = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Subtype, dynTypeOfOperand, e);

+      var notnull = Bpl.Expr.Neq(exp, Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      var and = Bpl.Expr.And(notnull, subtype);

+      TranslatedExpressions.Push(and);

       return;

     }

 

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 1f57e07d..b5c01fc1 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -880,9 +880,16 @@ namespace BytecodeTranslator {
         Bpl.Variable t;

         var key = type.InternedKey;

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

-          var parents = GetParents(type.ResolvedType);

+          List<ITypeReference> structuralParents;

+          var parents = GetParents(type.ResolvedType, out structuralParents);

           t = this.Heap.CreateTypeVariable(type, parents);

           this.declaredTypeConstants.Add(key, t);

+          foreach (var p in structuralParents) {

+            var p_prime = FindOrCreateType(p);

+            var e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Subtype, Bpl.Expr.Ident(t), p_prime);

+            var a = new Bpl.Axiom(Bpl.Token.NoToken, e);

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

+          }

           this.TranslatedProgram.TopLevelDeclarations.Add(t);

           if (isExtern) {

             var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "extern", new List<object>(1), null);

@@ -893,15 +900,24 @@ namespace BytecodeTranslator {
       }

     }

 

-    private List<Bpl.ConstantParent> GetParents(ITypeDefinition typeDefinition) {

+    private List<Bpl.ConstantParent> GetParents(ITypeDefinition typeDefinition, out List<ITypeReference> structuralParents) {

       var parents = new List<Bpl.ConstantParent>();

+      structuralParents = new List<ITypeReference>();

       foreach (var p in typeDefinition.BaseClasses) {

-        var v = (Bpl.IdentifierExpr) FindOrCreateType(p);

-        parents.Add(new Bpl.ConstantParent(v, true));

+        if (p is IGenericTypeInstanceReference) {

+          structuralParents.Add(p);

+        } else {

+          var v = (Bpl.IdentifierExpr)FindOrCreateType(p);

+          parents.Add(new Bpl.ConstantParent(v, true));

+        }

       }

       foreach (var j in typeDefinition.Interfaces) {

-        var v = (Bpl.IdentifierExpr)FindOrCreateType(j);

-        parents.Add(new Bpl.ConstantParent(v, false));

+        if (j is IGenericTypeInstanceReference) {

+          structuralParents.Add(j);

+        } else {

+          var v = (Bpl.IdentifierExpr)FindOrCreateType(j);

+          parents.Add(new Bpl.ConstantParent(v, false));

+        }

       }

       return parents;

     }