Separated the concepts of "boxing" (i.e., CLR boxing of a value type) from

the "union" type that is the supertype of all the translated Boogie types.

7 files changed, 241 insertions, 115 deletions

diff --git a/BCT/BCT.sln b/BCT/BCT.sln
index c8c132bb..cdd22c63 100644
--- a/BCT/BCT.sln
+++ b/BCT/BCT.sln
@@ -54,6 +54,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ILGarbageCollect", "..\..\C
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ControlAndDataFlowGraph", "..\..\ccicodebox\CodeGenerators\ControlAndDataFlowGraph\ControlAndDataFlowGraph.csproj", "{2596EFB0-87AE-42CE-89EB-84F35D6350D2}"

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "NewILToCodeModel", "..\..\CCICodeBox\Converters\NewILToCodeModel\NewILToCodeModel.csproj", "{A555D4CB-F16F-4049-A8CF-180B8A05C755}"

+EndProject

 Global

 	GlobalSection(TeamFoundationVersionControl) = preSolution

 		SccNumberOfProjects = 17

@@ -829,6 +831,36 @@ Global
 		{2596EFB0-87AE-42CE-89EB-84F35D6350D2}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{2596EFB0-87AE-42CE-89EB-84F35D6350D2}.Release|Mixed Platforms.Build.0 = Release|Any CPU

 		{2596EFB0-87AE-42CE-89EB-84F35D6350D2}.Release|x86.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.CompilerOnly|Any CPU.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.CompilerOnly|Any CPU.Build.0 = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.CompilerOnly|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.CompilerOnly|Mixed Platforms.Build.0 = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.CompilerOnly|x86.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.Debug|x86.ActiveCfg = Debug|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.FastpathSim|Any CPU.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.FastpathSim|Any CPU.Build.0 = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.FastpathSim|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.FastpathSim|Mixed Platforms.Build.0 = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.FastpathSim|x86.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyDebug|Any CPU.ActiveCfg = Debug|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyDebug|Any CPU.Build.0 = Debug|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyDebug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyDebug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyDebug|x86.ActiveCfg = Debug|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyRelease|Any CPU.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyRelease|Any CPU.Build.0 = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyRelease|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyRelease|Mixed Platforms.Build.0 = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.NightlyRelease|x86.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.Release|Any CPU.Build.0 = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{A555D4CB-F16F-4049-A8CF-180B8A05C755}.Release|x86.ActiveCfg = Release|Any CPU

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index e6e5c414..a9e1f9b0 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -331,22 +331,13 @@ namespace BytecodeTranslator
           // but the address of it must be a ref, so do the conversion

           this.Traverse(addressOf.Expression);

           var e = this.TranslatedExpressions.Pop();

-          this.TranslatedExpressions.Push(this.sink.Heap.Unbox(addressOf.Token(), this.sink.Heap.RefType, e));

+          this.TranslatedExpressions.Push(this.sink.Heap.FromUnion(addressOf.Token(), this.sink.Heap.RefType, e));

         } else {

           this.Traverse(addressOf.Expression);

         }

       } else {

         this.Traverse(addressOf.Expression);

         return;

-        // TODO: Sometimes the value must still be boxed: for anythign that is not going to be represented as a Ref in Boogie!

-        //this.Traverse(addressOf.Expression);

-        //var e = this.TranslatedExpressions.Pop();

-

-        //Bpl.Variable a = this.sink.CreateFreshLocal(addressOf.Type);

-        //this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));

-        //this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(Bpl.Token.NoToken, Bpl.Expr.Ident(a), Bpl.Expr.Ident(this.sink.Heap.BoxField), e, AccessType.Heap, boogieT));

-        //this.TranslatedExpressions.Push(Bpl.Expr.Ident(a));

-

       }

     }

     #endregion

@@ -554,7 +545,7 @@ namespace BytecodeTranslator
       List<Bpl.Expr> inexpr;

       List<Bpl.IdentifierExpr> outvars;

       Bpl.IdentifierExpr thisExpr;

-      Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;

+      Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> toBoxed;

       var proc = TranslateArgumentsAndReturnProcedure(methodCallToken, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed);

       string methodname = proc.Name;

       var translateAsFunctionCall = proc is Bpl.Function;

@@ -596,6 +587,7 @@ namespace BytecodeTranslator
             this.TranslatedExpressions.Push(callFunction);

             return;

           } else {

+            EmitLineDirective(methodCallToken);

             if (attrib != null)

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

             else

@@ -604,8 +596,20 @@ namespace BytecodeTranslator
           }

         }

 

-        foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {

-          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));

+        foreach (KeyValuePair<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> kv in toBoxed) {

+          var lhs = kv.Key;

+          var tuple = kv.Value;

+          var rhs = tuple.Item1;

+          Bpl.Expr fromUnion;

+          if (tuple.Item2) {

+            // Since both structs and objects are represented by "Ref", need to make a distinction here.

+            // Review: Introduce an explicit type "Struct"?

+            fromUnion = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Union2Struct), new Bpl.ExprSeq(rhs));

+          } else {

+            fromUnion = this.sink.Heap.FromUnion(Bpl.Token.NoToken, lhs.Type, rhs);

+            //this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, this.sink.Heap.FromUnion(Bpl.Token.NoToken, lhs.Type, rhs)));

+          }

+          this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(lhs, fromUnion));

         }

 

         Bpl.Expr expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, Bpl.Expr.Ident(this.sink.Heap.ExceptionVariable), Bpl.Expr.Ident(this.sink.Heap.NullRef));

@@ -630,6 +634,17 @@ namespace BytecodeTranslator
       }

     }

 

+    private void EmitLineDirective(Bpl.IToken methodCallToken) {

+      var sloc = this.StmtTraverser.lastSourceLocation;

+      if (sloc != null) {

+        var fileName = sloc.Document.Location;

+        var lineNumber = sloc.StartLine;

+        var attrib = new Bpl.QKeyValue(methodCallToken, "sourceLine", new List<object> { Bpl.Expr.Literal((int)lineNumber) }, null);

+        attrib = new Bpl.QKeyValue(methodCallToken, "sourceFile", new List<object> { fileName }, attrib);

+        this.StmtTraverser.StmtBuilder.Add(new Bpl.AssertCmd(methodCallToken, Bpl.Expr.True, attrib));

+      }

+    }

+

     private Bpl.CallCmd translateAddRemoveCall(IMethodCall methodCall, IMethodDefinition resolvedMethod, Bpl.IToken methodCallToken, List<Bpl.Expr> inexpr, List<Bpl.IdentifierExpr> outvars, Bpl.IdentifierExpr thisExpr, bool isEventAdd) {

       Bpl.CallCmd call;

       var mName = resolvedMethod.Name.Value;

@@ -670,6 +685,7 @@ namespace BytecodeTranslator
       this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(thisExpr)));

 

       // Second, generate the call to the appropriate ctor

+      EmitLineDirective(methodCallToken);

       this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(methodCallToken, proc.Name, inexpr, outvars));

 

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

@@ -684,7 +700,7 @@ namespace BytecodeTranslator
     }

 

     // REVIEW: Does "thisExpr" really need to come back as an identifier? Can't it be a general expression?

-    protected Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable<IExpression> arguments, out List<Bpl.Expr> inexpr, out List<Bpl.IdentifierExpr> outvars, out Bpl.IdentifierExpr thisExpr, out Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed) {

+    protected Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable<IExpression> arguments, out List<Bpl.Expr> inexpr, out List<Bpl.IdentifierExpr> outvars, out Bpl.IdentifierExpr thisExpr, out Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> toUnioned) {

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

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

 

@@ -718,7 +734,7 @@ namespace BytecodeTranslator
       }

       #endregion

 

-      toBoxed = new Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr>();

+      toUnioned = new Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>>();

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

       penum.MoveNext();

       foreach (IExpression exp in arguments) {

@@ -755,9 +771,16 @@ namespace BytecodeTranslator
           e = bplLocal;

         }

 

-        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 {

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

+          if (TranslationHelper.IsStruct(expressionToTraverse.Type)) {

+            // Since both structs and objects are represented by "Ref", need to make a distinction here.

+            // Review: Introduce an explicit type "Struct"?

+            var toUnion = new Bpl.NAryExpr(token, new Bpl.FunctionCall(this.sink.Heap.Struct2Union), new Bpl.ExprSeq(e));

+            inexpr.Add(toUnion);

+          } else {

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

+          }

+        } else {

           inexpr.Add(e);

         }

         if (penum.Current.IsByReference) {

@@ -769,7 +792,7 @@ namespace BytecodeTranslator
             var boogieType = this.sink.CciTypeToBoogie(penum.Current.Type);

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

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

-              toBoxed[unboxed] = boxed;

+              toUnioned[unboxed] = Tuple.Create(boxed,false);

               outvars.Add(boxed);

             } else {

               outvars.Add(unboxed);

@@ -800,20 +823,20 @@ namespace BytecodeTranslator
       if (!translateAsFunctionCall) {

         if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

           Bpl.Variable v = this.sink.CreateFreshLocal(methodToCall.ResolvedMethod.Type.ResolvedType);

-          Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(token, v);

+          Bpl.IdentifierExpr unUnioned = new Bpl.IdentifierExpr(token, v);

           if (resolvedMethod.Type is IGenericParameterReference) {

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

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

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

+              toUnioned[unUnioned] = Tuple.Create(unioned, TranslationHelper.IsStruct(methodToCall.ResolvedMethod.Type.ResolvedType));

+              outvars.Add(unioned);

             } else {

-              outvars.Add(unboxed);

+              outvars.Add(unUnioned);

             }

           } else {

-            outvars.Add(unboxed);

+            outvars.Add(unUnioned);

           }

-          TranslatedExpressions.Push(unboxed);

+          TranslatedExpressions.Push(unUnioned);

         }

       }

 

@@ -882,6 +905,8 @@ namespace BytecodeTranslator
       }

       Bpl.Cmd cmd;

 

+      EmitLineDirective(tok);

+

       var/*?*/ local = container as ILocalDefinition;

       if (local != null) {

         Contract.Assume(instance == null);

@@ -1025,9 +1050,12 @@ namespace BytecodeTranslator
         List<Bpl.Expr> inexpr;

         List<Bpl.IdentifierExpr> outvars;

         Bpl.IdentifierExpr thisExpr;

-        Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;

+        Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> toBoxed;

         var proc = TranslateArgumentsAndReturnProcedure(token, ctor, resolvedMethod, null, createObjectInstance.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed);

         inexpr.Insert(0, Bpl.Expr.Ident(a));

+

+        EmitLineDirective(token);

+

         this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, proc.Name, inexpr, outvars));

 

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

@@ -1574,7 +1602,8 @@ namespace BytecodeTranslator
       this.Traverse(conversion.ValueToConvert);

       var boogieTypeOfValue = this.sink.CciTypeToBoogie(conversion.ValueToConvert.Type);

       var boogieTypeToBeConvertedTo = this.sink.CciTypeToBoogie(conversion.TypeAfterConversion);

-      if (boogieTypeOfValue == boogieTypeToBeConvertedTo) {

+      if (boogieTypeOfValue == boogieTypeToBeConvertedTo && !TranslationHelper.IsStruct(conversion.ValueToConvert.Type)

+        && !TranslationHelper.IsStruct(conversion.TypeAfterConversion)) {

         // then this conversion is a nop, just ignore it

         return;

       }

@@ -1584,20 +1613,44 @@ namespace BytecodeTranslator
 

       var exp = TranslatedExpressions.Pop();

 

+      if (boogieTypeOfValue == this.sink.Heap.UnionType && boogieTypeToBeConvertedTo != this.sink.Heap.RefType) {

+        var e = this.sink.Heap.FromUnion(tok, boogieTypeToBeConvertedTo, exp);

+        TranslatedExpressions.Push(e);

+        return;

+      }

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

+        Bpl.Expr e;

+        if (boogieTypeOfValue == this.sink.Heap.RefType)

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

+        else

+          e = this.sink.Heap.ToUnion(tok, boogieTypeOfValue, exp);

+        TranslatedExpressions.Push(e);

+        return;

+      }

+

+      if (boogieTypeToBeConvertedTo == this.sink.Heap.RefType &&

+        TranslationHelper.IsStruct(conversion.TypeAfterConversion) &&

+        boogieTypeOfValue == this.sink.Heap.RefType) {

+        // REVIEW: This also applies to conversions from one struct type to another!

+        var e = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Struct), new Bpl.ExprSeq(exp));

+        TranslatedExpressions.Push(e);

+        return;

+      }

+

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

         Bpl.Expr expr;

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

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

         }

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

-          expr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Ident(this.sink.Heap.NullRef));

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

         }

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

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

         }

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

+          expr = this.sink.Heap.FromUnion(tok, Bpl.Type.Bool, exp);

         }

         else {

           throw new NotImplementedException(msg);

@@ -1612,13 +1665,13 @@ namespace BytecodeTranslator
           expr = new Bpl.NAryExpr(tok, new Bpl.IfThenElse(tok), new Bpl.ExprSeq(exp, Bpl.Expr.Literal(1), Bpl.Expr.Literal(0)));

         }

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

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

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

         }

         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.UnionType) {

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

+          expr = this.sink.Heap.FromUnion(Bpl.Token.NoToken, Bpl.Type.Int, exp);

         }

         else {

           throw new NotImplementedException(msg);

@@ -1628,9 +1681,32 @@ namespace BytecodeTranslator
       }

 

       if (boogieTypeToBeConvertedTo == this.sink.Heap.RefType) {

+        // var a = BoxFromXXX(exp);

         Bpl.Variable a = this.sink.CreateFreshLocal(conversion.TypeAfterConversion);

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

-        this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(Bpl.Token.NoToken, Bpl.Expr.Ident(a), Bpl.Expr.Ident(this.sink.Heap.BoxField), exp, AccessType.Heap, boogieTypeOfValue));

+        Bpl.Procedure boxOperator;

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

+          boxOperator = this.sink.Heap.BoxFromBool;

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

+          boxOperator = this.sink.Heap.BoxFromInt;

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

+          boxOperator = this.sink.Heap.BoxFromReal;

+        else if (TranslationHelper.IsStruct(conversion.ValueToConvert.Type)) {

+          // Boxing a struct implicitly makes a copy of the struct

+          var typeOfValue = conversion.ValueToConvert.Type;

+          var proc = this.sink.FindOrCreateProcedureForStructCopy(typeOfValue);

+          var bplLocal = Bpl.Expr.Ident(this.sink.CreateFreshLocal(typeOfValue));

+          var cmd = new Bpl.CallCmd(tok, proc.Name, new List<Bpl.Expr> { exp, }, new List<Bpl.IdentifierExpr> { bplLocal, });

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

+          exp = bplLocal;

+          boxOperator = this.sink.Heap.BoxFromStruct;

+        }  else {

+          if (boogieTypeOfValue != this.sink.Heap.UnionType)

+            throw new NotImplementedException(msg);

+          boxOperator = this.sink.Heap.BoxFromUnion;

+        }

+        var name = boxOperator.Name;

+

+        this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(Bpl.Token.NoToken, name, new Bpl.ExprSeq(exp), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));

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

         return;

       }

@@ -1645,10 +1721,10 @@ namespace BytecodeTranslator
           expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Int2Real), new Bpl.ExprSeq(exp));

         }

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

+          expr = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.sink.Heap.Unbox2Real), 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));

+          expr = this.sink.Heap.FromUnion(tok, this.sink.Heap.RealType, exp);

         }

         else {

           throw new NotImplementedException(msg);

@@ -1657,27 +1733,27 @@ namespace BytecodeTranslator
         return;

       }

       

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

-        Bpl.Function func;

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

-          func = this.sink.Heap.Bool2Union;

-        }

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

-          func = this.sink.Heap.Int2Union;

-        }

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

-          func = this.sink.Heap.Ref2Union;

-        }

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

-          func = this.sink.Heap.Real2Union;

-        }

-        else {

-          throw new NotImplementedException(msg);

-        }

-        var boxExpr = new Bpl.NAryExpr(conversion.Token(), new Bpl.FunctionCall(func), new Bpl.ExprSeq(exp));

-        TranslatedExpressions.Push(boxExpr);

-        return;

-      }

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

+      //  Bpl.Function func;

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

+      //    func = this.sink.Heap.Bool2Union;

+      //  }

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

+      //    func = this.sink.Heap.Int2Union;

+      //  }

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

+      //    func = this.sink.Heap.Ref2Union;

+      //  }

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

+      //    func = this.sink.Heap.Real2Union;

+      //  }

+      //  else {

+      //    throw new NotImplementedException(msg);

+      //  }

+      //  var boxExpr = new Bpl.NAryExpr(conversion.Token(), new Bpl.FunctionCall(func), new Bpl.ExprSeq(exp));

+      //  TranslatedExpressions.Push(boxExpr);

+      //  return;

+      //}

     }

 

     public override void TraverseChildren(IOnesComplement onesComplement) {

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 0c976bcc..aaed79e4 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -29,15 +29,6 @@ namespace BytecodeTranslator {
   /// </summary>

   public class SplitFieldsHeap : Heap {

 

-    #region "Boxing" as done in the CLR

-    /// <summary>

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

-    /// </summary>

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

-    private Bpl.GlobalVariable boxField = null;

-    public override Bpl.Variable BoxField { get { return boxField; } }

-    #endregion

-

     /// <summary>

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

     /// </summary>

@@ -122,13 +113,10 @@ namespace BytecodeTranslator {
       if (accessType == AccessType.Struct || accessType == AccessType.Heap) {

         Bpl.IdentifierExpr field = f as Bpl.IdentifierExpr;

         Debug.Assert(field != null);

-        if (field.Decl == this.BoxField)

-          return Unbox(f.tok, unboxType, Bpl.Expr.Select(field, o));

-        else

-          return Bpl.Expr.Select(field, o);

+        return Bpl.Expr.Select(field, o);

       }

       else

-        return Unbox(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f));

+        return FromUnion(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f));

     }

 

     /// <summary>

@@ -140,13 +128,10 @@ namespace BytecodeTranslator {
       if (accessType == AccessType.Struct || accessType == AccessType.Heap) {

         Bpl.IdentifierExpr field = f as Bpl.IdentifierExpr;

         Debug.Assert(field != null);

-        if (field.Decl == this.BoxField)

-          return Bpl.Cmd.MapAssign(tok, field, o, Box(tok, boxType, value));

-        else

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

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

       }

       else {

-        return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, Box(f.tok, boxType, value))));

+        return TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(ArrayContentsVariable), Bpl.Expr.Store(Bpl.Expr.Ident(ArrayContentsVariable), o, Bpl.Expr.Store(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f, ToUnion(f.tok, boxType, value))));

       }

     }

 

@@ -159,15 +144,6 @@ namespace BytecodeTranslator {
   /// </summary>

   public class GeneralHeap : Heap {

 

-    #region "Boxing" as done in the CLR

-    /// <summary>

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

-    /// </summary>

-    [RepresentationFor("$BoxField", "const unique $BoxField: Field;")]

-    private Bpl.Constant boxField = null;

-    public override Bpl.Variable BoxField { get { return boxField; } }

-    #endregion

-

     #region Fields

 

     [RepresentationFor("$Heap", "var $Heap: HeapType;", true)]

@@ -268,7 +244,7 @@ namespace BytecodeTranslator {
         callRead = Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f);

 

       // wrap it in the right conversion function

-      var callExpr = Unbox(f.tok, unboxType, callRead);

+      var callExpr = FromUnion(f.tok, unboxType, callRead);

       return callExpr;

     }

 

@@ -281,7 +257,7 @@ namespace BytecodeTranslator {
 

       Bpl.IdentifierExpr h;

       Bpl.NAryExpr callWrite;

-      var callConversion = Box(f.tok, boxType, value);

+      var callConversion = ToUnion(f.tok, boxType, value);

 

       if (accessType == AccessType.Struct || accessType == AccessType.Heap) {

         h = Bpl.Expr.Ident(HeapVariable);

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index dc281ad6..f4a04b37 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -73,8 +73,6 @@ namespace BytecodeTranslator {
 

     public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);

 

-    public abstract Bpl.Variable BoxField { get; }

-

     #region Boogie Types

 

     [RepresentationFor("Delegate", "type {:datatype} Delegate;")]

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

     public Bpl.CtorType FieldType;

 

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

+    [RepresentationFor("Union", "type {:datatype} Union;")]

     public Bpl.TypeCtorDecl UnionTypeDecl = null;

     public Bpl.CtorType UnionType;

 

@@ -126,38 +124,81 @@ namespace BytecodeTranslator {
 

     #endregion

 

+    #region CLR Boxing

+

+    [RepresentationFor("$BoxFromBool", "procedure $BoxFromBool(b: bool) returns (r: Ref) free ensures $BoxedValue(r) == Bool2Union(b); { call r := Alloc(); assume $BoxedValue(r) == Bool2Union(b); }")]

+    public Bpl.Procedure BoxFromBool = null;

+

+    [RepresentationFor("$BoxFromInt", "procedure $BoxFromInt(i: int) returns (r: Ref) free ensures $BoxedValue(r) == Int2Union(i); { call r := Alloc(); assume $BoxedValue(r) == Int2Union(i); }")]

+    public Bpl.Procedure BoxFromInt = null;

+

+    [RepresentationFor("$BoxFromReal", "procedure $BoxFromReal(r: Real) returns (rf: Ref) free ensures $BoxedValue(rf) == Real2Union(r); { call rf := Alloc(); assume $BoxedValue(rf) == Real2Union(r); }")]

+    public Bpl.Procedure BoxFromReal = null;

+

+    [RepresentationFor("$BoxFromStruct", "procedure $BoxFromStruct(s: Ref) returns (r: Ref) free ensures $BoxedValue(r) == Struct2Union(s); { call r := Alloc(); assume $BoxedValue(r) == Struct2Union(s); }")]

+    public Bpl.Procedure BoxFromStruct = null;

+

+    [RepresentationFor("$BoxFromUnion", "procedure {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref) { if (is#Ref2Union(u)) { r := refValue#Ref2Union(u); } else { call r := Alloc(); assume $BoxedValue(r) == u; } }")]

+    public Bpl.Procedure BoxFromUnion = null;

+

+    [RepresentationFor("$BoxedValue", "function $BoxedValue(r: Ref): Union;")]

+    public Bpl.Function BoxedValue = null;

+

+    [RepresentationFor("$Unbox2Bool", "function $Unbox2Bool(r: Ref): (bool) { boolValue#Bool2Union($BoxedValue(r)) }")]

+    public Bpl.Function Unbox2Bool = null;

+

+    [RepresentationFor("$Unbox2Int", "function $Unbox2Int(r: Ref): (int) { intValue#Int2Union($BoxedValue(r)) }")]

+    public Bpl.Function Unbox2Int = null;

+

+    [RepresentationFor("$Unbox2Real", "function $Unbox2Real(r: Ref): (Real) { realValue#Real2Union($BoxedValue(r)) }")]

+    public Bpl.Function Unbox2Real = null;

+

+    [RepresentationFor("$Unbox2Struct", "function $Unbox2Struct(r: Ref): (Ref) { structValue#Struct2Union($BoxedValue(r)) }")]

+    public Bpl.Function Unbox2Struct = null;

+

+    [RepresentationFor("$Unbox2Union", "function $Unbox2Union(r: Ref): (Union) { $BoxedValue(r) }")]

+    public Bpl.Function Unbox2Union = null;

+

+    #endregion

+

     #region Conversions

 

     #region Heap values

 

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

+    [RepresentationFor("Union2Bool", "function Union2Bool(u: Union): (bool) { boolValue#Bool2Union(u) }")]

     public Bpl.Function Union2Bool = null;

     

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

+    [RepresentationFor("Union2Int", "function Union2Int(u: Union): (int) { intValue#Int2Union(u) }")]

     public Bpl.Function Union2Int = null;

     

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

+    [RepresentationFor("Union2Ref", "function Union2Ref(u: Union): (Ref) { refValue#Ref2Union(u) }")]

     public Bpl.Function Union2Ref = null;

 

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

+    [RepresentationFor("Union2Real", "function Union2Real(u: Union): (Real) { realValue#Real2Union(u) }")]

     public Bpl.Function Union2Real = null;

 

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

+    [RepresentationFor("Union2Struct", "function Union2Struct(u: Union): (Ref) { structValue#Struct2Union(u) }")]

+    public Bpl.Function Union2Struct = null;

+

+    [RepresentationFor("Bool2Union", "function {:constructor} Bool2Union(boolValue: bool): Union;")]

     public Bpl.Function Bool2Union = null;

 

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

+    [RepresentationFor("Int2Union", "function {:constructor} Int2Union(intValue: int): Union;")]

     public Bpl.Function Int2Union = null;

 

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

+    [RepresentationFor("Ref2Union", "function {:constructor} Ref2Union(refValue: Ref): Union;")]

     public Bpl.Function Ref2Union = null;

 

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

+    [RepresentationFor("Real2Union", "function {:constructor} Real2Union(realValue: Real): Union;")]

     public Bpl.Function Real2Union = null;

 

+    [RepresentationFor("Struct2Union", "function {:constructor} Struct2Union(structValue: Ref): Union;")]

+    public Bpl.Function Struct2Union = 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) {

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

       Bpl.Function conversion;

       if (boogieType == Bpl.Type.Bool)

         conversion = this.Bool2Union;

@@ -180,7 +221,7 @@ namespace BytecodeTranslator {
       return callConversion;

     }

 

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

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

       Bpl.Function conversion = null;

       if (boogieType == Bpl.Type.Bool)

         conversion = this.Union2Bool;

@@ -384,10 +425,6 @@ axiom Union2Int($DefaultHeapValue) == 0;
 axiom Union2Bool($DefaultHeapValue) == false;

 axiom Union2Ref($DefaultHeapValue) == null;

 

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

 

 procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index abbdcc00..8de2f91e 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -566,10 +566,10 @@ namespace BytecodeTranslator {
         if (rtype == ltype) {

           // do nothing

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

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

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

         }

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

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

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

         }

         else {

           System.Diagnostics.Debug.Assert(false);

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index c36608b6..14eee8c6 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -122,6 +122,8 @@ namespace BytecodeTranslator
           foreach (var sloc in slocs) {

             fileName = sloc.Document.Location;

             lineNumber = sloc.StartLine;

+

+            this.parent.lastSourceLocation = sloc;

             break;

           }

           if (fileName != null) {

@@ -237,6 +239,7 @@ namespace BytecodeTranslator
     }

 

     private static int counter = 0;

+    public IPrimarySourceLocation lastSourceLocation;

     internal int NextUniqueNumber() {

       return counter++;

     }

@@ -336,14 +339,16 @@ namespace BytecodeTranslator
       // then a struct value of type S is being assigned: "lhs := s"

       // model this as the statement "call lhs := S..#copy_ctor(s)" that does the bit-wise copying

       if (isStruct) {

-        var defaultValue = new DefaultValue() {

-          DefaultValueType = typ,

-          Locations = new List<ILocation>(localDeclarationStatement.Locations),

-          Type = typ,

-        };

-        var e2 = ExpressionFor(defaultValue);

-        StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, boogieLocalExpr, e2));

-        if (structCopy) {

+        if (!structCopy) {

+          var defaultValue = new DefaultValue() {

+            DefaultValueType = typ,

+            Locations = new List<ILocation>(localDeclarationStatement.Locations),

+            Type = typ,

+          };

+          var e2 = ExpressionFor(defaultValue);

+          StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, boogieLocalExpr, e2));

+        } else 

+        /*if (structCopy) */{

           var proc = this.sink.FindOrCreateProcedureForStructCopy(typ);

           e = ExpressionFor(initVal);

           StmtBuilder.Add(new Bpl.CallCmd(tok, proc.Name, new List<Bpl.Expr> { e, }, new List<Bpl.IdentifierExpr>{ boogieLocalExpr, }));

diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index bd297451..73e882e0 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -140,7 +140,7 @@ namespace BytecodeTranslator {
         List<Bpl.Expr> inexpr;

         List<Bpl.IdentifierExpr> outvars;

         Bpl.IdentifierExpr thisExpr;

-        Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;

+        Dictionary<Bpl.IdentifierExpr, Tuple<Bpl.IdentifierExpr,bool>> toBoxed;

         var proc = TranslateArgumentsAndReturnProcedure(token, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out toBoxed);