diff options
-rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 45 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 10 |
2 files changed, 38 insertions, 17 deletions
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 74121074..664db230 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -29,6 +29,15 @@ 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>
@@ -103,10 +112,14 @@ namespace BytecodeTranslator { /// <param name="f">The field that is used to dereference the object <paramref name="o"/>.
/// </param>
public override Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.Expr f, AccessType accessType, Bpl.Type unboxType) {
- if (accessType == AccessType.Struct)
- return Unbox(f.tok, unboxType, Bpl.Expr.Select(o, f));
- else if (accessType == AccessType.Heap)
- return Bpl.Expr.Select(f, o);
+ 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);
+ }
else
return Unbox(f.tok, unboxType, Bpl.Expr.Select(Bpl.Expr.Select(Bpl.Expr.Ident(ArrayContentsVariable), o), f));
}
@@ -117,12 +130,17 @@ namespace BytecodeTranslator { /// </summary>
public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.Expr f, Bpl.Expr value, AccessType accessType, Bpl.Type boxType) {
Debug.Assert(o != null);
- if (accessType == AccessType.Struct)
- return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)o, f, Box(f.tok, boxType, value));
- else if (accessType == AccessType.Heap)
- return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)f, o, value);
- else
+ 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);
+ }
+ 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))));
+ }
}
}
@@ -134,6 +152,15 @@ 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)]
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index 6de7cb95..579ce648 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -73,6 +73,8 @@ namespace BytecodeTranslator { public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);
+ public abstract Bpl.Variable BoxField { get; }
+
#region Boogie Types
[RepresentationFor("Field", "type Field;")]
@@ -184,14 +186,6 @@ namespace BytecodeTranslator { #endregion
- #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;")]
- public Bpl.Constant BoxField = null;
- #endregion
-
#region Real number conversions
[RepresentationFor("Int2Real", "function Int2Real(int): Real;")]
public Bpl.Function Int2Real = null;
|