Separate out the concepts of boxing

(i.e., CLR's creating a heap cell and
putting a value into it) from the concept
of the "union" type that all Boogie types
are a subtype of.

5 files changed, 72 insertions, 72 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index aa4141e2..e6e5c414 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -326,7 +326,7 @@ namespace BytecodeTranslator
       var boogieT = this.sink.CciTypeToBoogie(t);

 

       if (t is IGenericParameterReference) {

-        if (boogieT == this.sink.Heap.BoxType) {

+        if (boogieT == this.sink.Heap.UnionType) {

           // then the expression will be represented by something of type Box

           // but the address of it must be a ref, so do the conversion

           this.Traverse(addressOf.Expression);

@@ -481,8 +481,8 @@ namespace BytecodeTranslator
         e = lit;

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

         e = Bpl.Expr.Ident(this.sink.Heap.NullRef);

-      } else if (bplType == this.sink.Heap.BoxType) {

-        e = Bpl.Expr.Ident(this.sink.Heap.DefaultBox);

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

+        e = Bpl.Expr.Ident(this.sink.Heap.DefaultHeapValue);

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

         e = Bpl.Expr.Ident(this.sink.Heap.DefaultReal);

       } else {

@@ -755,7 +755,7 @@ namespace BytecodeTranslator
           e = bplLocal;

         }

 

-        if (currentType is IGenericParameterReference && this.sink.CciTypeToBoogie(currentType) == this.sink.Heap.BoxType)

+        if (currentType is IGenericParameterReference && this.sink.CciTypeToBoogie(currentType) == this.sink.Heap.UnionType)

           inexpr.Add(sink.Heap.Box(token, this.sink.CciTypeToBoogie(expressionToTraverse.Type), e));

         else {

           inexpr.Add(e);

@@ -767,8 +767,8 @@ namespace BytecodeTranslator
           }

           if (penum.Current.Type is IGenericParameterReference) {

             var boogieType = this.sink.CciTypeToBoogie(penum.Current.Type);

-            if (boogieType == this.sink.Heap.BoxType) {

-              Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));

+            if (boogieType == this.sink.Heap.UnionType) {

+              Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.UnionType));

               toBoxed[unboxed] = boxed;

               outvars.Add(boxed);

             } else {

@@ -803,8 +803,8 @@ namespace BytecodeTranslator
           Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(token, v);

           if (resolvedMethod.Type is IGenericParameterReference) {

             var boogieType = this.sink.CciTypeToBoogie(resolvedMethod.Type);

-            if (boogieType == this.sink.Heap.BoxType) {

-              Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));

+            if (boogieType == this.sink.Heap.UnionType) {

+              Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.UnionType));

               toBoxed[unboxed] = boxed;

               outvars.Add(boxed);

             } else {

@@ -1596,8 +1596,8 @@ namespace BytecodeTranslator
           expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Real2Int), new Bpl.ExprSeq(exp));

           expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, expr, Bpl.Expr.Literal(0));

         }

-        else if (boogieTypeOfValue == this.sink.Heap.BoxType) {

-          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Box2Bool), new Bpl.ExprSeq(exp));

+        else if (boogieTypeOfValue == this.sink.Heap.UnionType) {

+          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Union2Bool), new Bpl.ExprSeq(exp));

         }

         else {

           throw new NotImplementedException(msg);

@@ -1617,8 +1617,8 @@ namespace BytecodeTranslator
         else if (boogieTypeOfValue == this.sink.Heap.RealType) {

           expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Real2Int), new Bpl.ExprSeq(exp));

         }

-        else if (boogieTypeOfValue == this.sink.Heap.BoxType) {

-          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Box2Int), new Bpl.ExprSeq(exp));

+        else if (boogieTypeOfValue == this.sink.Heap.UnionType) {

+          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Union2Int), new Bpl.ExprSeq(exp));

         }

         else {

           throw new NotImplementedException(msg);

@@ -1647,8 +1647,8 @@ namespace BytecodeTranslator
         else if (boogieTypeOfValue == this.sink.Heap.RefType) {

           expr = this.sink.Heap.ReadHeap(exp, Bpl.Expr.Ident(this.sink.Heap.BoxField), AccessType.Heap, this.sink.Heap.RealType);

         }

-        else if (boogieTypeOfValue == this.sink.Heap.BoxType) {

-          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Box2Real), new Bpl.ExprSeq(exp));

+        else if (boogieTypeOfValue == this.sink.Heap.UnionType) {

+          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Union2Real), new Bpl.ExprSeq(exp));

         }

         else {

           throw new NotImplementedException(msg);

@@ -1657,19 +1657,19 @@ namespace BytecodeTranslator
         return;

       }

       

-      if (boogieTypeToBeConvertedTo == this.sink.Heap.BoxType) {

+      if (boogieTypeToBeConvertedTo == this.sink.Heap.UnionType) {

         Bpl.Function func;

         if (boogieTypeOfValue == Bpl.Type.Bool) {

-          func = this.sink.Heap.Bool2Box;

+          func = this.sink.Heap.Bool2Union;

         }

         else if (boogieTypeOfValue == Bpl.Type.Int) {

-          func = this.sink.Heap.Int2Box;

+          func = this.sink.Heap.Int2Union;

         }

         else if (boogieTypeOfValue == this.sink.Heap.RefType) {

-          func = this.sink.Heap.Ref2Box;

+          func = this.sink.Heap.Ref2Union;

         }

         else if (boogieTypeOfValue == this.sink.Heap.RealType) {

-          func = this.sink.Heap.Real2Box;

+          func = this.sink.Heap.Real2Union;

         }

         else {

           throw new NotImplementedException(msg);

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 70d30c16..c67c3722 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -52,7 +52,7 @@ namespace BytecodeTranslator {
       string prelude = this.InitialPreludeText + this.CommonText;

       var b = RepresentationFor.ParsePrelude(prelude, this, out program);

       if (b) {

-        this.BoxType = new Bpl.CtorType(this.BoxTypeDecl.tok, this.BoxTypeDecl, new Bpl.TypeSeq());

+        this.UnionType = new Bpl.CtorType(this.UnionTypeDecl.tok, this.UnionTypeDecl, new Bpl.TypeSeq());

         this.DelegateType = new Bpl.CtorType(this.DelegateTypeDecl.tok, this.DelegateTypeDecl, new Bpl.TypeSeq());

         this.DelegateMultisetType = new Bpl.TypeSynonymAnnotation(this.DelegateMultisetTypeDecl.tok, this.DelegateMultisetTypeDecl, new Bpl.TypeSeq());

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

@@ -169,17 +169,17 @@ namespace BytecodeTranslator {
     [RepresentationFor("$Heap", "var $Heap: HeapType;", 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): Union { 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 := H[o][f := v]] }")]

+    [RepresentationFor("Write", "function {:inline true} Write(H:HeapType, o:Ref, f:Field, v:Union): HeapType { H[o := 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 =

-      @"type HeapType = [Ref][Field]Box;

+      @"type HeapType = [Ref][Field]Union;

 

 ";

     private Sink sink;

@@ -193,7 +193,7 @@ namespace BytecodeTranslator {
       string prelude = this.InitialPreludeText + this.CommonText;

       var b = RepresentationFor.ParsePrelude(prelude, this, out program);

       if (b) {

-        this.BoxType = new Bpl.CtorType(this.BoxTypeDecl.tok, this.BoxTypeDecl, new Bpl.TypeSeq());

+        this.UnionType = new Bpl.CtorType(this.UnionTypeDecl.tok, this.UnionTypeDecl, new Bpl.TypeSeq());

         this.DelegateType = new Bpl.CtorType(this.DelegateTypeDecl.tok, this.DelegateTypeDecl, new Bpl.TypeSeq());

         this.DelegateMultisetType = new Bpl.TypeSynonymAnnotation(this.DelegateMultisetTypeDecl.tok, this.DelegateMultisetTypeDecl, new Bpl.TypeSeq());

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

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 6553efba..dc281ad6 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -66,7 +66,7 @@ namespace BytecodeTranslator {
 

   public abstract class Heap : HeapFactory, IHeap

   {

-    [RepresentationFor("$ArrayContents", "var $ArrayContents: [Ref][int]Box;")]

+    [RepresentationFor("$ArrayContents", "var $ArrayContents: [Ref][int]Union;")]

     public Bpl.Variable ArrayContentsVariable = null;

     [RepresentationFor("$ArrayLength", "function $ArrayLength(Ref): int;")]

     public Bpl.Function ArrayLengthFunction = null;

@@ -101,12 +101,12 @@ namespace BytecodeTranslator {
     public Bpl.TypeCtorDecl FieldTypeDecl = null;

     public Bpl.CtorType FieldType;

 

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

-    public Bpl.TypeCtorDecl BoxTypeDecl = null;

-    public Bpl.CtorType BoxType;

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

+    public Bpl.TypeCtorDecl UnionTypeDecl = null;

+    public Bpl.CtorType UnionType;

 

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

-    public Bpl.Constant DefaultBox;

+    [RepresentationFor("$DefaultHeapValue", "const unique $DefaultHeapValue : Union;")]

+    public Bpl.Constant DefaultHeapValue;

 

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

     public Bpl.TypeCtorDecl RefTypeDecl = null;

@@ -130,45 +130,45 @@ namespace BytecodeTranslator {
 

     #region Heap values

 

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

-    public Bpl.Function Box2Bool = null;

+    [RepresentationFor("Union2Bool", "function Union2Bool(Union): bool;")]

+    public Bpl.Function Union2Bool = null;

     

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

-    public Bpl.Function Box2Int = null;

+    [RepresentationFor("Union2Int", "function Union2Int(Union): int;")]

+    public Bpl.Function Union2Int = null;

     

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

-    public Bpl.Function Box2Ref = null;

+    [RepresentationFor("Union2Ref", "function Union2Ref(Union): Ref;")]

+    public Bpl.Function Union2Ref = null;

 

-    [RepresentationFor("Box2Real", "function Box2Real(Box): Real;")]

-    public Bpl.Function Box2Real = null;

+    [RepresentationFor("Union2Real", "function Union2Real(Union): Real;")]

+    public Bpl.Function Union2Real = null;

 

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

-    public Bpl.Function Bool2Box = null;

+    [RepresentationFor("Bool2Union", "function Bool2Union(bool): Union;")]

+    public Bpl.Function Bool2Union = null;

 

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

-    public Bpl.Function Int2Box = null;

+    [RepresentationFor("Int2Union", "function Int2Union(int): Union;")]

+    public Bpl.Function Int2Union = null;

 

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

-    public Bpl.Function Ref2Box = null;

+    [RepresentationFor("Ref2Union", "function Ref2Union(Ref): Union;")]

+    public Bpl.Function Ref2Union = null;

 

-    [RepresentationFor("Real2Box", "function Real2Box(Real): Box;")]

-    public Bpl.Function Real2Box = null;

+    [RepresentationFor("Real2Union", "function Real2Union(Real): Union;")]

+    public Bpl.Function Real2Union = null;

 

-    [RepresentationFor("Box2Box", "function {:inline true} Box2Box(b: Box): Box { b }")]

-    public Bpl.Function Box2Box = null;

+    [RepresentationFor("Union2Union", "function {:inline true} Union2Union(u: Union): Union { u }")]

+    public Bpl.Function Union2Union = null;

 

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

       Bpl.Function conversion;

       if (boogieType == Bpl.Type.Bool)

-        conversion = this.Bool2Box;

+        conversion = this.Bool2Union;

       else if (boogieType == Bpl.Type.Int)

-        conversion = this.Int2Box;

+        conversion = this.Int2Union;

       else if (boogieType == RefType)

-        conversion = this.Ref2Box;

+        conversion = this.Ref2Union;

       else if (boogieType == RealType)

-        conversion = this.Real2Box;

-      else if (boogieType == BoxType)

-        conversion = this.Box2Box;

+        conversion = this.Real2Union;

+      else if (boogieType == UnionType)

+        conversion = this.Union2Union;

       else

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

 

@@ -183,15 +183,15 @@ namespace BytecodeTranslator {
     public Bpl.Expr Unbox(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {

       Bpl.Function conversion = null;

       if (boogieType == Bpl.Type.Bool)

-        conversion = this.Box2Bool;

+        conversion = this.Union2Bool;

       else if (boogieType == Bpl.Type.Int)

-        conversion = this.Box2Int;

+        conversion = this.Union2Int;

       else if (boogieType == RefType)

-        conversion = this.Box2Ref;

+        conversion = this.Union2Ref;

       else if (boogieType == RealType)

-        conversion = this.Box2Real;

-      else if (boogieType == BoxType)

-        conversion = this.Box2Box;

+        conversion = this.Union2Real;

+      else if (boogieType == UnionType)

+        conversion = this.Union2Union;

       else

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

 

@@ -380,13 +380,13 @@ procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
   $result := $TypeOf($DynamicType(this));

 }

 

-axiom Box2Int($DefaultBox) == 0;

-axiom Box2Bool($DefaultBox) == false;

-axiom Box2Ref($DefaultBox) == null;

+axiom Union2Int($DefaultHeapValue) == 0;

+axiom Union2Bool($DefaultHeapValue) == false;

+axiom Union2Ref($DefaultHeapValue) == null;

 

-axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x );

-axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x );

-axiom (forall x: Ref :: { Ref2Box(x) } Box2Ref(Ref2Box(x)) == x );

+axiom (forall x: int :: { Int2Union(x) } Union2Int(Int2Union(x)) == x );

+axiom (forall x: bool :: { Bool2Union(x) } Union2Bool(Bool2Union(x)) == x );

+axiom (forall x: Ref :: { Ref2Union(x) } Union2Ref(Ref2Union(x)) == x );

 

 function $ThreadDelegate(Ref) : Ref;

 

@@ -492,14 +492,14 @@ implementation System.Windows.Controls.Control.get_IsEnabled($this: Ref) returns
   var enabledness: bool;

   $Exception:=null;

   enabledness := isControlEnabled[$this];

-  $result := Box2Ref(Bool2Box(enabledness));

+  $result := Union2Ref(Bool2Union(enabledness));

 }

 

 procedure {:inline 1} System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref);

 implementation System.Windows.Controls.Primitives.ToggleButton.set_IsChecked$System.Nullable$System.Boolean$($this: Ref, value$in: Ref) {

   var check: bool;

   $Exception:=null;

-  check := Box2Bool(Ref2Box(value$in));

+  check := Union2Bool(Ref2Union(value$in));

   isControlChecked[$this] := check;

 }

 

@@ -508,7 +508,7 @@ implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($th
   var isChecked: bool;

   $Exception:=null;

   isChecked := isControlChecked[$this];

-  $result := Box2Ref(Bool2Box(isChecked));

+  $result := Union2Ref(Bool2Union(isChecked));

 }

 

 ";

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 5217df14..abbdcc00 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -565,10 +565,10 @@ namespace BytecodeTranslator {
         Bpl.Expr rexpr = Bpl.Expr.Ident(rvar);

         if (rtype == ltype) {

           // do nothing

-        } else if (ltype == sink.Heap.BoxType) {

+        } else if (ltype == sink.Heap.UnionType) {

           rexpr = sink.Heap.Box(Bpl.Token.NoToken, rtype, rexpr);

         }

-        else if (rtype == sink.Heap.BoxType) {

+        else if (rtype == sink.Heap.UnionType) {

           rexpr = sink.Heap.Unbox(Bpl.Token.NoToken, ltype, rexpr);

         }

         else {

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 4499f11e..bc4e7524 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -144,7 +144,7 @@ namespace BytecodeTranslator {
           if (TypeHelper.TypesAreEquivalent(c, type.PlatformType.SystemValueType)) continue;

           return CciTypeToBoogie(c);

         }

-        return heap.BoxType;

+        return heap.UnionType;

       } else

         return heap.RefType;

     }