Trying to fix "boxing", i.e., value type to ref conversions as done in the CLR.

5 files changed, 163 insertions, 77 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 277374cb..4c287785 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -365,14 +365,23 @@ namespace BytecodeTranslator
     }

 

     /// <summary>

-    /// 

+    /// If the expression is a struct, then this returns a "boxed" struct.

+    /// Otherwise it just translates the expression and skips the address-of

+    /// operation.

     /// </summary>

-    /// <param name="addressOf"></param>

-    /// <remarks>Since we are doing Copy-In,Copy-Out for function calls we can ignore it.

-    /// But will this work for the general case?</remarks>

     public override void Visit(IAddressOf addressOf)

     {

       Visit(addressOf.Expression);

+      if (addressOf.Expression.Type.IsValueType)

+      {

+        var e = this.TranslatedExpressions.Pop();

+        var callBox = new Bpl.NAryExpr(

+          addressOf.Token(),

+        new Bpl.FunctionCall(this.sink.Heap.Struct2Ref),

+        new Bpl.ExprSeq(e)

+        );

+        TranslatedExpressions.Push(callBox);

+      }

     }

     #endregion

 

@@ -389,8 +398,10 @@ namespace BytecodeTranslator
           TranslatedExpressions.Push(lit);

         } else if (bplType == Bpl.Type.Bool) {

           TranslatedExpressions.Push(Bpl.Expr.False);

+        } else if (bplType == this.sink.Heap.RefType) {

+          TranslatedExpressions.Push(Bpl.Expr.Ident(this.sink.Heap.NullRef));

         } else {

-          throw new NotImplementedException("Don't know how to translate type");

+          throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(constant.Type)));

         }

      }

       else if (constant.Value is bool)

@@ -443,19 +454,35 @@ namespace BytecodeTranslator
         args = this.args;

         this.args = savedArgs;

 

-        thisExpr = this.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;

+        var e = this.TranslatedExpressions.Pop();

+        if (methodCall.MethodToCall.ContainingType.IsValueType)

+        {

+          // then the "this arg" was actually an AddressOf the struct

+          // but we are going to ignore that and just get the identifier

+          // that it was the address of

+          var nAry = e as Bpl.NAryExpr;

+          var nAryArgs = nAry.Args;

+          e = nAryArgs[0] as Bpl.IdentifierExpr;

+        }

+        inexpr.Add(e);

+        if (e is Bpl.NAryExpr)

+        {

+          e = ((Bpl.NAryExpr)e).Args[0];

+        }

+        thisExpr = e as Bpl.IdentifierExpr;

         locals = new List<Bpl.Variable>();

         Bpl.Variable x = thisExpr.Decl;

         locals.Add(x);

-        for (int i = 0; i < args.Count; i++) {

+        for (int i = 0; i < args.Count; i++)

+        {

           Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(args[i]));

           Bpl.Variable y = this.sink.CreateFreshLocal(args[i].Type);

           StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(y), this.sink.Heap.ReadHeap(Bpl.Expr.Ident(x), g, args[i].ContainingType.ResolvedType.IsStruct)));

           x = y;

           locals.Add(y);

         }

-        thisExpr = Bpl.Expr.Ident(x);

-        inexpr.Add(thisExpr);

+        //thisExpr = Bpl.Expr.Ident(x);

+        //inexpr.Add(thisExpr);

       }

       #endregion

 

@@ -597,7 +624,8 @@ namespace BytecodeTranslator
           int count = args.Count;

           Bpl.Variable x = locals[count];

           count--;

-          while (0 <= count) {

+          while (0 <= count)

+          {

             IFieldDefinition currField = args[count];

             if (currField.Type.ResolvedType.IsClass) break;

             Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(currField));

@@ -1064,6 +1092,29 @@ namespace BytecodeTranslator
               throw new NotImplementedException();

 

           }

+        case PrimitiveTypeCode.NotPrimitive:

+          Bpl.Function func;

+          switch (conversion.ValueToConvert.Type.TypeCode) {

+            case PrimitiveTypeCode.Boolean:

+              func = this.sink.Heap.Bool2Ref;

+              break;

+            case PrimitiveTypeCode.Char: // chars are represented as ints

+            case PrimitiveTypeCode.Int16:

+            case PrimitiveTypeCode.Int32:

+            case PrimitiveTypeCode.Int64:

+            case PrimitiveTypeCode.Int8:

+              func = this.sink.Heap.Int2Ref;

+              break;

+            default:

+              throw new NotImplementedException();

+          }

+          var boxExpr = new Bpl.NAryExpr(

+            conversion.Token(),

+            new Bpl.FunctionCall(func),

+            new Bpl.ExprSeq(exp)

+            );

+            TranslatedExpressions.Push(boxExpr);

+            return;

         default:

           throw new NotImplementedException();

       }

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 6bd552fa..5426bf00 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -33,18 +33,16 @@ namespace BytecodeTranslator {
     /// Prelude text for which access to the ASTs is not needed

     /// </summary>

     private readonly string InitialPreludeText =

-      @"const null: int;

-type ref = int;

-type struct = [Field]box;

-type HeapType = [int,int]int;

+      @"type Struct = [Field]Box;

+type HeapType = [Ref,Field]Box;

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

 function IsGoodHeap(HeapType): bool;

 var $ArrayContents: [int][int]int;

 var $ArrayLength: [int]int;

 

-var $Alloc: [int] bool;

-procedure {:inline 1} Alloc() returns (x: int)

-  free ensures x != 0;

+var $Alloc: [Ref] bool;

+procedure {:inline 1} Alloc() returns (x: Ref)

+  free ensures x != null;

   modifies $Alloc;

 {

   assume $Alloc[x] == false;

@@ -71,6 +69,7 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
         this.BoxType = new Bpl.CtorType(this.BoxTypeDecl.tok, this.BoxTypeDecl, new Bpl.TypeSeq());

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

+        this.RefType = new Bpl.CtorType(this.RefTypeDecl.tok, this.RefTypeDecl, new Bpl.TypeSeq());

       }

       return b;

     }

@@ -90,7 +89,7 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
         v = new Bpl.GlobalVariable(tok, tident);

       }

       else {

-        Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Bpl.Type.Int), t);

+        Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(this.RefType), t);

         Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, mt);

         v = new Bpl.GlobalVariable(tok, tident);

       }

@@ -156,26 +155,24 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
     [RepresentationFor("$Heap", "var $Heap: HeapType where IsGoodHeap($Heap);", true)]

     private Bpl.Variable HeapVariable = null;

     

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

+    [RepresentationFor("Read", "function {:inline true} Read(H:HeapType, o:Ref, f:Field): Box { H[o, f] }")]

     private Bpl.Function Read = null;

 

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

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

     private Bpl.Function Write = null;

 

     /// <summary>

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

     /// </summary>

     private readonly string InitialPreludeText =

-      @"const null: ref;

-type ref = int;

-type struct = [Field]box;

-type HeapType = [ref,Field]box;

+      @"type Struct = [Field]Box;

+type HeapType = [Ref,Field]Box;

 function IsGoodHeap(HeapType): bool;

-var $ArrayContents: [int][int]int;

-var $ArrayLength: [int]int;

+var $ArrayContents: [Ref][int]Box;

+var $ArrayLength: [Ref]int;

 

-var $Alloc: [ref] bool;

-procedure {:inline 1} Alloc() returns (x: ref)

+var $Alloc: [Ref] bool;

+procedure {:inline 1} Alloc() returns (x: Ref)

   free ensures x != null;

   modifies $Alloc;

 {

@@ -205,6 +202,7 @@ axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );
         this.BoxType = new Bpl.CtorType(this.BoxTypeDecl.tok, this.BoxTypeDecl, new Bpl.TypeSeq());

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

+        this.RefType = new Bpl.CtorType(this.RefTypeDecl.tok, this.RefTypeDecl, new Bpl.TypeSeq());

       }

       return b;

     }

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 9c1870c1..431184b7 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -70,14 +70,18 @@ namespace BytecodeTranslator {
     public Bpl.TypeCtorDecl FieldTypeDecl = null;

     public Bpl.CtorType FieldType;

 

-    [RepresentationFor("box", "type box;")]

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

     public Bpl.TypeCtorDecl BoxTypeDecl = null;

     public Bpl.CtorType BoxType;

 

-    [RepresentationFor("$DefaultBox", "const unique $DefaultBox : box;")]

+    [RepresentationFor("$DefaultBox", "const unique $DefaultBox : Box;")]

     public Bpl.Constant DefaultBox;

-    [RepresentationFor("$DefaultStruct", "const unique $DefaultStruct : struct;")]

-    public Bpl.Constant DefaultStruct;

+

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

+    public Bpl.TypeCtorDecl RefTypeDecl = null;

+    public Bpl.CtorType RefType;

+    [RepresentationFor("null", "const unique null : Ref;")]

+    public Bpl.Constant NullRef;

 

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

     protected Bpl.TypeCtorDecl TypeTypeDecl = null;

@@ -92,25 +96,46 @@ namespace BytecodeTranslator {
         return structType;

       }

     }

+    [RepresentationFor("$DefaultStruct", "const unique $DefaultStruct : Struct;")]

+    public Bpl.Constant DefaultStruct;

 

-    [RepresentationFor("Box2Int", "function Box2Int(box): int;")]

+

+    [RepresentationFor("Box2Int", "function Box2Int(Box): int;")]

     public Bpl.Function Box2Int = null;

 

-    [RepresentationFor("Box2Bool", "function Box2Bool(box): bool;")]

+    [RepresentationFor("Box2Bool", "function Box2Bool(Box): bool;")]

     public Bpl.Function Box2Bool = null;

 

-    [RepresentationFor("Box2Struct", "function Box2Struct(box): struct;")]

+    [RepresentationFor("Box2Struct", "function Box2Struct(Box): Struct;")]

     public Bpl.Function Box2Struct = null;

 

-    [RepresentationFor("Int2Box", "function Int2Box(int): box;")]

+    [RepresentationFor("Box2Ref", "function Box2Ref(Box): Ref;")]

+    public Bpl.Function Box2Ref = null;

+

+    [RepresentationFor("Int2Box", "function Int2Box(int): Box;")]

     public Bpl.Function Int2Box = null;

 

-    [RepresentationFor("Bool2Box", "function Bool2Box(bool): box;")]

+    [RepresentationFor("Bool2Box", "function Bool2Box(bool): Box;")]

     public Bpl.Function Bool2Box = null;

 

-    [RepresentationFor("Struct2Box", "function Struct2Box(struct): box;")]

+    [RepresentationFor("Struct2Box", "function Struct2Box(Struct): Box;")]

     public Bpl.Function Struct2Box = null;

 

+    #region "Boxing" as done in the CLR

+    /// <summary>

+    /// Used to represent "boxing" as it is done in the CLR.

+    /// </summary>

+    [RepresentationFor("Struct2Ref", "function Struct2Ref(Struct): Ref;")]

+    public Bpl.Function Struct2Ref = null;

+    [RepresentationFor("Int2Ref", "function Int2Ref(int): Ref;")]

+    public Bpl.Function Int2Ref = null;

+    [RepresentationFor("Bool2Ref", "function Bool2Ref(bool): Ref;")]

+    public Bpl.Function Bool2Ref = null;

+    #endregion

+

+    [RepresentationFor("Ref2Box", "function Ref2Box(Ref): Box;")]

+    public Bpl.Function Ref2Box = null;

+

     public Bpl.Expr Box(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {

       Bpl.Function conversion;

       if (boogieType == Bpl.Type.Bool)

@@ -119,8 +144,10 @@ namespace BytecodeTranslator {
         conversion = this.Int2Box;

       else if (boogieType == StructType)

         conversion = this.Struct2Box;

+      else if (boogieType == RefType)

+        conversion = this.Ref2Box;

       else

-        throw new InvalidOperationException("Unknown Boogie type");

+        throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));

 

       var callConversion = new Bpl.NAryExpr(

         tok,

@@ -138,8 +165,10 @@ namespace BytecodeTranslator {
         conversion = this.Box2Int;

       else if (boogieType == StructType)

         conversion = this.Box2Struct;

+      else if (boogieType == RefType)

+        conversion = this.Box2Ref;

       else

-        throw new InvalidOperationException("Unknown Boogie type");

+        throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));

 

       var callExpr = new Bpl.NAryExpr(

         tok,

@@ -174,7 +203,7 @@ namespace BytecodeTranslator {
 

     public abstract Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr o, Bpl.IdentifierExpr f, Bpl.Expr value, bool isStruct);

 

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

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

     protected Bpl.Function DynamicTypeFunction = null;

 

     /// <summary>

@@ -191,19 +220,19 @@ namespace BytecodeTranslator {
       return callDynamicType;

     }

 

-    [RepresentationFor("$TypeOf", "function $TypeOf(Type): ref;")]

+    [RepresentationFor("$TypeOf", "function $TypeOf(Type): Ref;")]

     public Bpl.Function TypeOfFunction = null;

 

     protected readonly string DelegateEncodingText =

-      @"procedure DelegateAdd(a: int, b: int) returns (c: int)

+      @"procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref)

 {

-  var m: int;

-  var o: int;

+  var m: Ref;

+  var o: Ref;

 

-  if (a == 0) {

+  if (a == null) {

     c := b;

     return;

-  } else if (b == 0) {

+  } else if (b == null) {

     c := a;

     return;

   }

@@ -218,15 +247,15 @@ namespace BytecodeTranslator {
   call c := DelegateAddHelper(c, m, o);

 }

 

-procedure DelegateRemove(a: int, b: int) returns (c: int)

+procedure DelegateRemove(a: Ref, b: Ref) returns (c: Ref)

 {

-  var m: int;

-  var o: int;

+  var m: Ref;

+  var o: Ref;

 

-  if (a == 0) {

-    c := 0;

+  if (a == null) {

+    c := null;

     return;

-  } else if (b == 0) {

+  } else if (b == null) {

     c := a;

     return;

   }

@@ -241,20 +270,20 @@ procedure DelegateRemove(a: int, b: int) returns (c: int)
   call c := DelegateRemoveHelper(c, m, o);

 }

 

-procedure GetFirstElement(i: int) returns (m: int, o: int)

+procedure GetFirstElement(i: Ref) returns (m: Ref, o: Ref)

 {

-  var first: int;

+  var first: Ref;

   first := $Next[i][$Head[i]];

   m := $Method[i][first];

   o := $Receiver[i][first]; 

 }

 

-procedure DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int)

+procedure DelegateAddHelper(oldi: Ref, m: Ref, o: Ref) returns (i: Ref)

 {

-  var x: int;

-  var h: int;

+  var x: Ref;

+  var h: Ref;

 

-  if (oldi == 0) {

+  if (oldi == null) {

     call i := Alloc();

     call x := Alloc();

     $Head[i] := x;

@@ -273,18 +302,18 @@ procedure DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int)
   $Head[i] := x;

 }

 

-procedure DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)

+procedure DelegateRemoveHelper(oldi: Ref, m: Ref, o: Ref) returns (i: Ref)

 {

-  var prev: int;

-  var iter: int;

-  var niter: int;

+  var prev: Ref;

+  var iter: Ref;

+  var niter: Ref;

 

   i := oldi;

-  if (i == 0) {

+  if (i == null) {

     return;

   }

 

-  prev := 0;

+  prev := null;

   iter := $Head[i];

   while (true) {

     niter := $Next[i][iter];

@@ -296,28 +325,28 @@ procedure DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
     }

     iter := niter;

   }

-  if (prev == 0) {

+  if (prev == null) {

     return;

   }

 

   $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]];

   if ($Next[i][$Head[i]] == $Head[i]) {

-    i := 0;

+    i := null;

   }

 }

 

 ";

 

-    [RepresentationFor("$Head", "var $Head: [int]int;")]

+    [RepresentationFor("$Head", "var $Head: [Ref]Ref;")]

     public Bpl.GlobalVariable DelegateHead = null;

 

-    [RepresentationFor("$Next", "var $Next: [int][int]int;")]

+    [RepresentationFor("$Next", "var $Next: [Ref][Ref]Ref;")]

     public Bpl.GlobalVariable DelegateNext = null;

     

-    [RepresentationFor("$Method", "var $Method: [int][int]int;")]

+    [RepresentationFor("$Method", "var $Method: [Ref][Ref]Ref;")]

     public Bpl.GlobalVariable DelegateMethod = null;

 

-    [RepresentationFor("$Receiver", "var $Receiver: [int][int]int;")]

+    [RepresentationFor("$Receiver", "var $Receiver: [Ref][Ref]Ref;")]

     public Bpl.GlobalVariable DelegateReceiver = null;

   }

 

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index b41e3f4f..eb458845 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -109,8 +109,10 @@ namespace BytecodeTranslator {
         return lit;

       } else if (type.ResolvedType.IsStruct) {

         return Bpl.Expr.Ident(this.Heap.DefaultStruct);

+      } else if (bplType == this.Heap.RefType) {

+        return Bpl.Expr.Ident(this.Heap.NullRef);

       } else {

-        throw new NotImplementedException("Don't know how to translate type");

+        throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(type)));

       }

     }

 

@@ -121,7 +123,13 @@ namespace BytecodeTranslator {
         return Bpl.Type.Int;

       else if (type.ResolvedType.IsStruct)

         return heap.StructType;

-      return Bpl.Type.Int; // BUG! This is where we need to return "ref" for a reference type

+      else if (type.IsEnum)

+      {

+        return CciTypeToBoogie(type.ResolvedType.UnderlyingType);

+      }

+      else

+        return heap.RefType;

+      //return Bpl.Type.Int; // BUG! This is where we need to return "ref" for a reference type

     }

 

     /// <summary>

@@ -219,7 +227,7 @@ namespace BytecodeTranslator {
       Bpl.Constant c;

       if (!this.declaredStringConstants.TryGetValue(str, out c)) {

         var tok = Bpl.Token.NoToken;

-        var t = Bpl.Type.Int;

+        var t = Heap.RefType;

         var name = "$string_literal_" + TranslationHelper.TurnStringIntoValidIdentifier(str);

         var tident = new Bpl.TypedIdent(tok, name, t);

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

@@ -294,9 +302,9 @@ namespace BytecodeTranslator {
         Bpl.Formal selfOut = null;

         #region Create 'this' parameter

         if (!method.IsStatic) {

-          Bpl.Type selfType;

+          Bpl.Type selfType = CciTypeToBoogie(method.ContainingType);

           if (method.ContainingType.ResolvedType.IsStruct) {

-            selfType = Heap.StructType;

+            //selfType = Heap.StructType;

             in_count++;

             self = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), "thisIn", selfType), true);

             out_count++;

@@ -304,7 +312,7 @@ namespace BytecodeTranslator {
           }

           else {

             in_count++;

-            selfType = Bpl.Type.Int;

+            //selfType = Heap.RefType;

             self = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), "this", selfType), true);

           }

         }

diff --git a/BCT/Samples/CodeCounter/codecounter.suo b/BCT/Samples/CodeCounter/codecounter.suo
index 74d31951..84ae5e2a 100644
--- a/BCT/Samples/CodeCounter/codecounter.suo
+++ b/BCT/Samples/CodeCounter/codecounter.suo