diff options
-rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 38 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 10 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 90 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 4 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 2 |
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;
}
|