summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--BCT/BytecodeTranslator/ExpressionTraverser.cs41
-rw-r--r--BCT/BytecodeTranslator/Heap.cs410
-rw-r--r--BCT/BytecodeTranslator/HeapFactory.cs27
-rw-r--r--BCT/BytecodeTranslator/MetadataTraverser.cs9
-rw-r--r--BCT/BytecodeTranslator/Program.cs6
-rw-r--r--BCT/BytecodeTranslator/Sink.cs52
-rw-r--r--BCT/BytecodeTranslator/TranslationHelper.cs13
-rw-r--r--BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt8
-rw-r--r--BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt4
-rw-r--r--BCT/RegressionTests/TranslationTest/TranslationTest.csproj6
-rw-r--r--BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt729
-rw-r--r--BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt719
-rw-r--r--BCT/RegressionTests/TranslationTest/UnitTest0.cs30
13 files changed, 169 insertions, 1885 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 3db99307..a19bbedc 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -293,10 +293,11 @@ namespace BytecodeTranslator
var instance = boundExpression.Instance;
if (instance == null) {
TranslatedExpressions.Push(f);
- } else {
+ }
+ else {
this.Visit(instance);
Bpl.Expr instanceExpr = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(this.sink.Heap.ReadHeap(instanceExpr, f));
+ TranslatedExpressions.Push(this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct));
}
return;
}
@@ -360,7 +361,7 @@ namespace BytecodeTranslator
{
if (constant.Value == null)
{
- var bplType = TranslationHelper.CciTypeToBoogie(constant.Type);
+ var bplType = sink.CciTypeToBoogie(constant.Type);
if (bplType == Bpl.Type.Int) {
var lit = Bpl.Expr.Literal(0);
lit.Type = Bpl.Type.Int;
@@ -390,7 +391,7 @@ namespace BytecodeTranslator
}
public override void Visit(IDefaultValue defaultValue) {
- var bplType = TranslationHelper.CciTypeToBoogie(defaultValue.Type);
+ var bplType = sink.CciTypeToBoogie(defaultValue.Type);
if (bplType == Bpl.Type.Int) {
var lit = Bpl.Expr.Literal(0);
lit.Type = Bpl.Type.Int;
@@ -464,8 +465,12 @@ namespace BytecodeTranslator
// Todo: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!
#region Translate Out vars
+ Bpl.IdentifierExpr outMap = null;
var outvars = new List<Bpl.IdentifierExpr>();
-
+ if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {
+ outMap = new Bpl.IdentifierExpr(methodCall.Token(), sink.CreateFreshLocal(new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(sink.Heap.FieldType), sink.Heap.BoxType)));
+ outvars.Add(outMap);
+ }
foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap)
{
if (kvp.Key.IsOut || kvp.Key.IsByReference)
@@ -528,8 +533,8 @@ namespace BytecodeTranslator
inexpr.Insert(0, Bpl.Expr.Ident(local));
}
else
- {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar))));
+ {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct)));
inexpr[0] = Bpl.Expr.Ident(local);
}
@@ -544,7 +549,7 @@ namespace BytecodeTranslator
}
else
{
- this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));
+ this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct));
}
}
else
@@ -555,6 +560,16 @@ namespace BytecodeTranslator
call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);
this.StmtTraverser.StmtBuilder.Add(call);
}
+ if (outMap != null) {
+ Debug.Assert(thisExpr != null);
+ Bpl.AssignLhs lhs = new Bpl.SimpleAssignLhs(Bpl.Token.NoToken, (Bpl.IdentifierExpr) thisExpr);
+ List<Bpl.AssignLhs> lhss = new List<Bpl.AssignLhs>();
+ lhss.Add(lhs);
+ List<Bpl.Expr> rhss = new List<Bpl.Expr>();
+ rhss.Add(outMap);
+ Bpl.AssignCmd acmd = new Bpl.AssignCmd(methodCall.Token(), lhss, rhss);
+ this.StmtTraverser.StmtBuilder.Add(acmd);
+ }
}
}
@@ -596,7 +611,15 @@ namespace BytecodeTranslator
if (target.Instance != null)
o = TranslatedExpressions.Pop();
Bpl.IdentifierExpr f = this.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;
- var c = this.sink.Heap.WriteHeap(assignment.Token(), o, f, sourceexp);
+ Bpl.Cmd c;
+ if (target.Instance == null) {
+ c = Bpl.Cmd.SimpleAssign(assignment.Token(), f, sourceexp);
+ }
+ else {
+ c = this.sink.Heap.WriteHeap(assignment.Token(), o, f, sourceexp, fieldReference.ContainingType.ResolvedType.IsStruct);
+ }
+ // In the struct case, I am making the assumption that we only see a single field dereference on the left side of the assignment
+ //var c = (fieldReference.ContainingType.ResolvedType.IsStruct) ? this.sink.WriteStruct((Bpl.IdentifierExpr)o, f, sourceexp) : this.sink.Heap.WriteHeap(assignment.Token(), o, f, sourceexp);
StmtTraverser.StmtBuilder.Add(c);
return;
}
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 8f21d59a..ba06b454 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -23,126 +23,6 @@ using System.Reflection;
namespace BytecodeTranslator {
/// <summary>
- /// A heap representation that uses a global variable, $Heap, which is
- /// a two-dimensional array indexed by objects and fields, each of which
- /// are represented as an integer.
- /// </summary>
- public class TwoDIntHeap : Heap {
-
- #region Fields
- [RepresentationFor("$Heap", "var $Heap: HeapType where IsGoodHeap($Heap);", true)]
- private Bpl.Variable HeapVariable = null;
-
- //[RepresentationFor("HeapType", "type HeapType = [int,int]int;")]
- //private Bpl.TypeSynonymDecl HeapType = null;
-
- //[RepresentationFor("IsGoodHeap", "function IsGoodHeap(HeapType): bool;")]
- //private Bpl.Function IsGoodHeap = null;
-
- /// <summary>
- /// Prelude text for which access to the ASTs is not needed
- /// </summary>
- private readonly string InitialPreludeText =
- @"const null: int;
-type HeapType = [int,int]int;
-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;
- modifies $Alloc;
-{
- assume $Alloc[x] == false;
- $Alloc[x] := true;
-}
-
-";
-
- #endregion
-
- public override bool MakeHeap(Sink sink, out Heap heap, out Bpl.Program/*?*/ program) {
- heap = this;
- program = null;
- string prelude = this.InitialPreludeText + this.DelegateEncodingText;
- var b = RepresentationFor.ParsePrelude(prelude, this, out program);
- if (b) {
- this.TypeType = new Bpl.CtorType(this.TypeTypeDecl.tok, this.TypeTypeDecl, new Bpl.TypeSeq());
- }
- return b;
- }
-
- /// <summary>
- /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
- /// on its type based on the heap representation.
- /// </summary>
- public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
- Bpl.Variable v;
- string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
- Bpl.IToken tok = field.Token();
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);
-
- if (field.IsStatic) {
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
- v = new Bpl.GlobalVariable(tok, tident);
- }
- else {
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
- v = new Bpl.Constant(tok, tident, true);
- }
- return v;
- }
-
- public override Bpl.Variable CreateEventVariable(IEventDefinition e) {
- Bpl.Variable v;
- string eventName = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
- Bpl.IToken tok = e.Token();
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(e.Type.ResolvedType);
-
- if (e.Adder.ResolvedMethod.IsStatic) {
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, eventName, t);
- v = new Bpl.GlobalVariable(tok, tident);
- }
- else {
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, eventName, t);
- v = new Bpl.Constant(tok, tident, true);
- }
- return v;
- }
-
- /// <summary>
- /// Returns the (typed) BPL expression that corresponds to the value of the field
- /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when
- /// <paramref name="o"/> is non-null, otherwise the value of the static field.
- /// </summary>
- /// <param name="o">The expression that represents the object to be dereferenced.
- /// Null if <paramref name="f"/> is a static field.
- /// </param>
- /// <param name="f">The field that is used to dereference the object <paramref name="o"/>, when
- /// it is not null. Otherwise the static field whose value should be read.
- /// </param>
- public override Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f) {
- return Bpl.Expr.Select(new Bpl.IdentifierExpr(f.tok, HeapVariable), new Bpl.Expr[] { o, f });
- }
-
- /// <summary>
- /// Returns the BPL command that corresponds to assigning the value <paramref name="value"/>
- /// to the field <paramref name="f"/> of the object <paramref name="o"/> (when
- /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
- /// field.
- /// </summary>
- public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {
- if (o == null)
- return Bpl.Cmd.SimpleAssign(tok, f, value);
- else
- return
- Bpl.Cmd.MapAssign(tok,
- new Bpl.IdentifierExpr(tok, this.HeapVariable), new Bpl.ExprSeq(o, f), value);
- }
- }
-
- /// <summary>
/// A heap representation that uses a separate global variable for each
/// field. Each global variable is a map from int to T where T is the
/// type of the field.
@@ -171,13 +51,17 @@ procedure {:inline 1} Alloc() returns (x: int)
type ref = int;
";
+ private Sink sink;
public override bool MakeHeap(Sink sink, out Heap heap, out Bpl.Program/*?*/ program) {
heap = this;
program = null;
+ this.sink = sink;
string prelude = this.InitialPreludeText + this.DelegateEncodingText;
var b = RepresentationFor.ParsePrelude(prelude, this, out program);
if (b) {
+ 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());
}
return b;
@@ -191,7 +75,7 @@ type ref = int;
Bpl.Variable v;
string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
Bpl.IToken tok = field.Token();
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);
+ Bpl.Type t = this.sink.CciTypeToBoogie(field.Type.ResolvedType);
if (field.IsStatic) {
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
@@ -209,7 +93,7 @@ type ref = int;
Bpl.Variable v;
string eventName = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
Bpl.IToken tok = e.Token();
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(e.Type.ResolvedType);
+ Bpl.Type t = this.sink.CciTypeToBoogie(e.Type.ResolvedType);
if (e.Adder.ResolvedMethod.IsStatic) {
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, eventName, t);
@@ -225,28 +109,27 @@ type ref = int;
/// <summary>
/// Returns the (typed) BPL expression that corresponds to the value of the field
- /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when
- /// <paramref name="o"/> is non-null, otherwise the value of the static field.
+ /// <paramref name="f"/> belonging to the object <paramref name="o"/> (which must be non-null).
/// </summary>
/// <param name="o">The expression that represents the object to be dereferenced.
- /// Null if <paramref name="f"/> is a static field.
/// </param>
- /// <param name="f">The field that is used to dereference the object <paramref name="o"/>, when
- /// it is not null. Otherwise the static field whose value should be read.
+ /// <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.IdentifierExpr f) {
- return Bpl.Expr.Select(f, o);
+ public override Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, bool isStruct) {
+ if (isStruct)
+ return Bpl.Expr.Select(o, f);
+ else
+ return Bpl.Expr.Select(f, o);
}
/// <summary>
/// Returns the BPL command that corresponds to assigning the value <paramref name="value"/>
- /// to the field <paramref name="f"/> of the object <paramref name="o"/> (when
- /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
- /// field.
+ /// to the field <paramref name="f"/> of the object <paramref name="o"/> (which should be non-null).
/// </summary>
- public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {
- if (o == null)
- return Bpl.Cmd.SimpleAssign(tok, f, value);
+ public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value, bool isStruct) {
+ Debug.Assert(o != null);
+ if (isStruct)
+ return Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr)o, f, value);
else
return Bpl.Cmd.MapAssign(tok, f, o, value);
}
@@ -254,171 +137,6 @@ type ref = int;
}
/// <summary>
- /// A heap representation that uses a global variable, $Heap, which is
- /// a two-dimensional array indexed by objects and fields. Objects
- /// are values of type "int", fields are unique constants, and the
- /// elements of the heap are of type "box". Each value that is read/written
- /// from/to the heap is wrapped in a type conversion function.
- /// </summary>
- public class TwoDBoxHeap : Heap {
-
- #region Fields
- [RepresentationFor("$Heap", "var $Heap: HeapType where IsGoodHeap($Heap);", true)]
- private Bpl.Variable HeapVariable = null;
-
- [RepresentationFor("Box2Int", "function Box2Int(box): int;")]
- private Bpl.Function Box2Int = null;
-
- [RepresentationFor("Box2Bool", "function Box2Bool(box): bool;")]
- private Bpl.Function Box2Bool = null;
-
- [RepresentationFor("Int2Box", "function Int2Box(int): box;")]
- private Bpl.Function Int2Box = null;
-
- [RepresentationFor("Bool2Box", "function Bool2Box(bool): box;")]
- private Bpl.Function Bool2Box = null;
-
- /// <summary>
- /// Prelude text for which access to the ASTs is not needed
- /// </summary>
- private readonly string InitialPreludeText =
- @"const null: int;
-type box;
-type HeapType = [int,int]box;
-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;
- modifies $Alloc;
-{
- assume $Alloc[x] == false;
- $Alloc[x] := true;
-}
-";
- private Sink sink;
-
- #endregion
-
- public override bool MakeHeap(Sink sink, out Heap heap, out Bpl.Program/*?*/ program) {
- this.sink = sink;
- heap = this;
- program = null;
- string prelude = this.InitialPreludeText + this.DelegateEncodingText;
- var b = RepresentationFor.ParsePrelude(prelude, this, out program);
- if (b) {
- this.TypeType = new Bpl.CtorType(this.TypeTypeDecl.tok, this.TypeTypeDecl, new Bpl.TypeSeq());
- }
- return b;
- }
-
- /// <summary>
- /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
- /// on its type based on the heap representation.
- /// </summary>
- public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
- Bpl.Variable v;
- string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
- Bpl.IToken tok = field.Token();
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);
-
- if (field.IsStatic) {
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
- v = new Bpl.GlobalVariable(tok, tident);
- }
- else {
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
- v = new Bpl.Constant(tok, tident, true);
- }
- return v;
- }
-
- public override Bpl.Variable CreateEventVariable(IEventDefinition e) {
- Bpl.Variable v;
- string fieldname = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
- Bpl.IToken tok = e.Token();
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(e.Type.ResolvedType);
-
- if (e.Adder.ResolvedMethod.IsStatic) {
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
- v = new Bpl.GlobalVariable(tok, tident);
- }
- else {
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
- v = new Bpl.Constant(tok, tident, true);
- }
- return v;
- }
-
- /// <summary>
- /// Returns the (typed) BPL expression that corresponds to the value of the field
- /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when
- /// <paramref name="o"/> is non-null, otherwise the value of the static field.
- /// </summary>
- /// <param name="o">The expression that represents the object to be dereferenced.
- /// Null if <paramref name="f"/> is a static field.
- /// </param>
- /// <param name="f">The field that is used to dereference the object <paramref name="o"/>, when
- /// it is not null. Otherwise the static field whose value should be read.
- /// </param>
- public override Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f) {
- // $Heap[o,f]
- var selectExpr = Bpl.Expr.Select(new Bpl.IdentifierExpr(f.tok, HeapVariable), new Bpl.Expr[] { o, f });
- // wrap it in the right conversion function
- Bpl.Function conversion;
- if (f.Type == Bpl.Type.Bool)
- conversion = this.Box2Bool;
- else if (f.Type == Bpl.Type.Int)
- conversion = this.Box2Int;
- else
- throw new InvalidOperationException("Unknown Boogie type");
- var callExpr = new Bpl.NAryExpr(
- f.tok,
- new Bpl.FunctionCall(conversion),
- new Bpl.ExprSeq(selectExpr)
- );
- callExpr.Type = f.Type;
- return callExpr;
-
- }
-
- /// <summary>
- /// Returns the BPL command that corresponds to assigning the value <paramref name="value"/>
- /// to the field <paramref name="f"/> of the object <paramref name="o"/> (when
- /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
- /// field.
- /// </summary>
- public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {
- if (o == null) {
- return Bpl.Cmd.SimpleAssign(tok, f, value);
- }
- else {
- // wrap it in the right conversion function
- Bpl.Function conversion;
- if (f.Type == Bpl.Type.Bool)
- conversion = this.Bool2Box;
- else if (f.Type == Bpl.Type.Int)
- conversion = this.Int2Box;
- else
- throw new InvalidOperationException("Unknown Boogie type");
-
- // $Heap[o,f] := conversion(value)
- var callExpr = new Bpl.NAryExpr(
- f.tok,
- new Bpl.FunctionCall(conversion),
- new Bpl.ExprSeq(value)
- );
- return
- Bpl.Cmd.MapAssign(tok,
- new Bpl.IdentifierExpr(tok, this.HeapVariable), new Bpl.ExprSeq(o, f), callExpr);
- }
- }
-
- }
-
- /// <summary>
/// A heap representation that uses Boogie (in-line) functions
/// for all heap reads and writes. That way the decision about
/// how to exactly represent the heap is made in the Prelude.
@@ -427,10 +145,6 @@ procedure {:inline 1} Alloc() returns (x: int)
#region Fields
- [RepresentationFor("Field", "type Field;")]
- private Bpl.TypeCtorDecl FieldTypeDecl = null;
- private Bpl.CtorType FieldType;
-
[RepresentationFor("$Heap", "var $Heap: HeapType where IsGoodHeap($Heap);", true)]
private Bpl.Variable HeapVariable = null;
@@ -457,7 +171,6 @@ procedure {:inline 1} Alloc() returns (x: int)
/// </summary>
private readonly string InitialPreludeText =
@"const null: ref;
-type box;
type ref = int;
type HeapType = [ref,Field]box;
function IsGoodHeap(HeapType): bool;
@@ -484,6 +197,7 @@ procedure {:inline 1} Alloc() returns (x: ref)
string prelude = this.InitialPreludeText + this.DelegateEncodingText;
var b = RepresentationFor.ParsePrelude(prelude, this, out program);
if (b) {
+ 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());
}
@@ -501,7 +215,7 @@ procedure {:inline 1} Alloc() returns (x: ref)
Bpl.IToken tok = field.Token();
if (field.IsStatic) {
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);
+ Bpl.Type t = this.sink.CciTypeToBoogie(field.Type.ResolvedType);
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
v = new Bpl.GlobalVariable(tok, tident);
}
@@ -521,7 +235,7 @@ procedure {:inline 1} Alloc() returns (x: ref)
Bpl.IToken tok = e.Token();
if (e.Adder.ResolvedMethod.IsStatic) {
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(e.Type.ResolvedType);
+ Bpl.Type t = this.sink.CciTypeToBoogie(e.Type.ResolvedType);
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
v = new Bpl.GlobalVariable(tok, tident);
}
@@ -536,26 +250,28 @@ procedure {:inline 1} Alloc() returns (x: ref)
/// <summary>
/// Returns the (typed) BPL expression that corresponds to the value of the field
- /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when
- /// <paramref name="o"/> is non-null, otherwise the value of the static field.
+ /// <paramref name="f"/> belonging to the object <paramref name="o"/> (which must be non-null).
/// </summary>
/// <param name="o">The expression that represents the object to be dereferenced.
- /// Null if <paramref name="f"/> is a static field.
/// </param>
- /// <param name="f">The field that is used to dereference the object <paramref name="o"/>, when
- /// it is not null. Otherwise the static field whose value should be read.
+ /// <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.IdentifierExpr f) {
- // $Read($Heap, o, f)
- var callRead = new Bpl.NAryExpr(
- f.tok,
- new Bpl.FunctionCall(this.Read),
- new Bpl.ExprSeq(new Bpl.IdentifierExpr(f.tok, this.HeapVariable), o, f)
- );
+ public override Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, bool isStruct) {
+ Debug.Assert(o != null);
+
+ var callRead = isStruct ?
+ Bpl.Expr.Select(o, f) :
+ // $Read($Heap, o, f)
+ new Bpl.NAryExpr(
+ f.tok,
+ new Bpl.FunctionCall(this.Read),
+ new Bpl.ExprSeq(new Bpl.IdentifierExpr(f.tok, this.HeapVariable), o, f)
+ );
+
// wrap it in the right conversion function
Bpl.Function conversion;
var originalType = this.underlyingTypes[f.Decl];
- var boogieType = TranslationHelper.CciTypeToBoogie(originalType);
+ var boogieType = sink.CciTypeToBoogie(originalType);
if (boogieType == Bpl.Type.Bool)
conversion = this.Box2Bool;
else if (boogieType == Bpl.Type.Int)
@@ -574,40 +290,44 @@ procedure {:inline 1} Alloc() returns (x: ref)
/// <summary>
/// Returns the BPL command that corresponds to assigning the value <paramref name="value"/>
- /// to the field <paramref name="f"/> of the object <paramref name="o"/> (when
- /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
- /// field.
+ /// to the field <paramref name="f"/> of the object <paramref name="o"/> (which should be non-null).
/// </summary>
- public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {
- if (o == null) {
- return Bpl.Cmd.SimpleAssign(tok, f, value);
+ public override Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value, bool isStruct) {
+ Debug.Assert(o != null);
+
+ // wrap it in the right conversion function
+ Bpl.Function conversion;
+ var originalType = this.underlyingTypes[f.Decl];
+ var boogieType = sink.CciTypeToBoogie(originalType);
+ if (boogieType == Bpl.Type.Bool)
+ conversion = this.Bool2Box;
+ else if (boogieType == Bpl.Type.Int)
+ conversion = this.Int2Box;
+ else
+ throw new InvalidOperationException("Unknown Boogie type");
+
+ var callConversion = new Bpl.NAryExpr(
+ f.tok,
+ new Bpl.FunctionCall(conversion),
+ new Bpl.ExprSeq(value)
+ );
+
+ Bpl.IdentifierExpr h;
+ Bpl.NAryExpr callWrite;
+ if (isStruct) {
+ h = (Bpl.IdentifierExpr)o;
+ callWrite = Bpl.Expr.Store(h, f, callConversion);
}
else {
- // wrap it in the right conversion function
- Bpl.Function conversion;
- var originalType = this.underlyingTypes[f.Decl];
- var boogieType = TranslationHelper.CciTypeToBoogie(originalType);
- if (boogieType == Bpl.Type.Bool)
- conversion = this.Bool2Box;
- else if (boogieType == Bpl.Type.Int)
- conversion = this.Int2Box;
- else
- throw new InvalidOperationException("Unknown Boogie type");
-
- var callConversion = new Bpl.NAryExpr(
- f.tok,
- new Bpl.FunctionCall(conversion),
- new Bpl.ExprSeq(value)
- );
// $Write($Heap, o, f)
- var h = new Bpl.IdentifierExpr(f.tok, this.HeapVariable);
- var callWrite = new Bpl.NAryExpr(
+ h = new Bpl.IdentifierExpr(f.tok, this.HeapVariable);
+ callWrite = new Bpl.NAryExpr(
f.tok,
new Bpl.FunctionCall(this.Write),
new Bpl.ExprSeq(h, o, f, callConversion)
);
- return Bpl.Cmd.SimpleAssign(f.tok, h, callWrite);
}
+ return Bpl.Cmd.SimpleAssign(f.tok, h, callWrite);
}
}
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 464846d4..23a7de80 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -40,24 +40,19 @@ namespace BytecodeTranslator {
/// <summary>
/// Returns the (typed) BPL expression that corresponds to the value of the field
- /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when
- /// <paramref name="o"/> is non-null, otherwise the value of the static field.
+ /// <paramref name="f"/> belonging to the object <paramref name="o"/> (which should be non-null).
/// </summary>
/// <param name="o">The expression that represents the object to be dereferenced.
- /// Null if <paramref name="f"/> is a static field.
/// </param>
- /// <param name="f">The field that is used to dereference the object <paramref name="o"/>, when
- /// it is not null. Otherwise the static field whose value should be read.
+ /// <param name="f">The field that is used to dereference the object <paramref name="o"/>.
/// </param>
- Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f);
+ Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, bool isStruct);
/// <summary>
/// Returns the BPL command that corresponds to assigning the value <paramref name="value"/>
- /// to the field <paramref name="f"/> of the object <paramref name="o"/> (when
- /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
- /// field.
+ /// to the field <paramref name="f"/> of the object <paramref name="o"/> (which should be non-null).
/// </summary>
- Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value);
+ Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value, bool isStruct);
/// <summary>
/// Returns the BPL expression that corresponds to the value of the dynamic type
@@ -71,6 +66,14 @@ namespace BytecodeTranslator {
{
public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);
+ [RepresentationFor("Field", "type Field;")]
+ public Bpl.TypeCtorDecl FieldTypeDecl = null;
+ public Bpl.CtorType FieldType;
+
+ [RepresentationFor("box", "type box;")]
+ public Bpl.TypeCtorDecl BoxTypeDecl = null;
+ public Bpl.CtorType BoxType;
+
[RepresentationFor("Type", "type Type;")]
protected Bpl.TypeCtorDecl TypeTypeDecl = null;
protected Bpl.CtorType TypeType;
@@ -95,9 +98,9 @@ namespace BytecodeTranslator {
public abstract Bpl.Variable CreateEventVariable(IEventDefinition e);
- public abstract Bpl.Expr ReadHeap(Bpl.Expr o, Bpl.IdentifierExpr f);
+ public abstract Bpl.Expr ReadHeap(Bpl.Expr o, Bpl.IdentifierExpr f, bool isStruct);
- public abstract Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr o, Bpl.IdentifierExpr f, Bpl.Expr value);
+ 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;")]
protected Bpl.Function DynamicTypeFunction = null;
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 71639a5c..bbcc81f5 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -102,7 +102,7 @@ namespace BytecodeTranslator {
if (f.IsStatic) {
Bpl.Expr e;
- var bplType = TranslationHelper.CciTypeToBoogie(f.Type);
+ var bplType = this.sink.CciTypeToBoogie(f.Type);
if (bplType == Bpl.Type.Int) {
e = Bpl.Expr.Literal(0);
e.Type = Bpl.Type.Int;
@@ -181,6 +181,13 @@ namespace BytecodeTranslator {
}
}
+ if (!method.IsStatic && method.ContainingType.ResolvedType.IsStruct) {
+ Bpl.IToken tok = method.Token();
+ stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok,
+ new Bpl.IdentifierExpr(tok, proc.OutParams[0]),
+ new Bpl.IdentifierExpr(tok, proc.InParams[0])));
+ }
+
#endregion
#region For non-deferring ctors and all cctors, initialize all fields to null-equivalent values
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 68107f82..592d9a10 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -73,12 +73,6 @@ namespace BytecodeTranslator {
case Options.HeapRepresentation.splitFields:
heap = new SplitFieldsHeap();
break;
- case Options.HeapRepresentation.twoDInt:
- heap = new TwoDIntHeap();
- break;
- case Options.HeapRepresentation.twoDBox:
- heap = new TwoDBoxHeap();
- break;
case Options.HeapRepresentation.general:
heap = new GeneralHeap();
break;
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index b33edf96..c6fadd5f 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -97,6 +97,16 @@ namespace BytecodeTranslator {
public readonly Bpl.Program TranslatedProgram;
+ public Bpl.Type CciTypeToBoogie(ITypeReference type) {
+ if (TypeHelper.TypesAreEquivalent(type, type.PlatformType.SystemBoolean))
+ return Bpl.Type.Bool;
+ else if (TypeHelper.IsPrimitiveInteger(type))
+ return Bpl.Type.Int;
+ else if (type.ResolvedType.IsStruct)
+ return new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(this.heap.FieldType), this.heap.BoxType);
+ return Bpl.Type.Int; // BUG! This is where we need to return "ref" for a reference type
+ }
+
/// <summary>
/// Creates a fresh local var of the given Type and adds it to the
/// Bpl Implementation
@@ -105,7 +115,15 @@ namespace BytecodeTranslator {
/// <returns> A fresh Variable with automatic generated name and location </returns>
public Bpl.Variable CreateFreshLocal(ITypeReference typeReference) {
Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(typeReference);
+ Bpl.Type t = CciTypeToBoogie(typeReference);
+ Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));
+ ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie
+ localVarMap.Add(dummy, v);
+ return v;
+ }
+
+ public Bpl.Variable CreateFreshLocal(Bpl.Type t) {
+ Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location
Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));
ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie
localVarMap.Add(dummy, v);
@@ -125,7 +143,7 @@ namespace BytecodeTranslator {
public Bpl.Variable FindOrCreateLocalVariable(ILocalDefinition local) {
Bpl.LocalVariable v;
Bpl.IToken tok = local.Token();
- Bpl.Type t = TranslationHelper.CciTypeToBoogie(local.Type.ResolvedType);
+ Bpl.Type t = CciTypeToBoogie(local.Type.ResolvedType);
if (!localVarMap.TryGetValue(local, out v)) {
v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, local.Name.Value, t));
localVarMap.Add(local, v);
@@ -229,7 +247,6 @@ namespace BytecodeTranslator {
string MethodName = TranslationHelper.CreateUniqueMethodName(method);
- Bpl.Function f;
Bpl.Procedure p;
if (this.initiallyDeclaredProcedures.TryGetValue(MethodName, out p)) return p;
@@ -241,7 +258,7 @@ namespace BytecodeTranslator {
var formalMap = new Dictionary<IParameterDefinition, MethodParameter>();
foreach (IParameterDefinition formal in method.Parameters) {
- mp = new MethodParameter(formal);
+ mp = new MethodParameter(formal, this.CciTypeToBoogie(formal.Type));
if (mp.inParameterCopy != null) in_count++;
if (mp.outParameterCopy != null && (formal.IsByReference || formal.IsOut))
out_count++;
@@ -253,7 +270,7 @@ namespace BytecodeTranslator {
Bpl.Variable savedRetVariable = this.RetVariable;
if (method.Type.TypeCode != PrimitiveTypeCode.Void) {
- Bpl.Type rettype = TranslationHelper.CciTypeToBoogie(method.Type);
+ Bpl.Type rettype = CciTypeToBoogie(method.Type);
out_count++;
this.RetVariable = new Bpl.Formal(method.Token(),
new Bpl.TypedIdent(method.Type.Token(),
@@ -265,13 +282,22 @@ namespace BytecodeTranslator {
#endregion
Bpl.Formal/*?*/ self = null;
+ Bpl.Formal selfOut = null;
#region Create 'this' parameter
if (!method.IsStatic) {
- in_count++;
- Bpl.Type selftype = Bpl.Type.Int;
- self = new Bpl.Formal(method.Token(),
- new Bpl.TypedIdent(method.Type.Token(),
- "this", selftype), true);
+ Bpl.Type selfType;
+ if (method.ContainingType.ResolvedType.IsStruct) {
+ selfType = new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);
+ in_count++;
+ self = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), "thisIn", selfType), true);
+ out_count++;
+ selfOut = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), "this", selfType), false);
+ }
+ else {
+ in_count++;
+ selfType = Bpl.Type.Int;
+ self = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Type.Token(), "this", selfType), true);
+ }
}
#endregion
@@ -281,9 +307,11 @@ namespace BytecodeTranslator {
int i = 0;
int j = 0;
- #region Add 'this' parameter as first in parameter
- if (!method.IsStatic)
+ #region Add 'this' parameter as first in parameter and 'thisOut' parameter as first out parameter
+ if (self != null)
invars[i++] = self;
+ if (selfOut != null)
+ outvars[j++] = selfOut;
#endregion
foreach (MethodParameter mparam in formalMap.Values) {
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index f3b7aa58..abc6b9b0 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -36,12 +36,10 @@ namespace BytecodeTranslator {
public IParameterDefinition underlyingParameter;
- public MethodParameter(IParameterDefinition parameterDefinition) {
+ public MethodParameter(IParameterDefinition parameterDefinition, Bpl.Type ptype) {
this.underlyingParameter = parameterDefinition;
- Bpl.Type ptype = TranslationHelper.CciTypeToBoogie(parameterDefinition.Type);
-
var parameterToken = parameterDefinition.Token();
var typeToken = parameterDefinition.Type.Token();
var parameterName = parameterDefinition.Name.Value;
@@ -135,15 +133,6 @@ namespace BytecodeTranslator {
#region Temp Stuff that must be replaced as soon as there is real code to deal with this
- public static Bpl.Type CciTypeToBoogie(ITypeReference type) {
- if (TypeHelper.TypesAreEquivalent(type, type.PlatformType.SystemBoolean))
- return Bpl.Type.Bool;
- else if (TypeHelper.IsPrimitiveInteger(type))
- return Bpl.Type.Int;
- else
- return Bpl.Type.Int; // BUG! This is where we need to return "ref" for a reference type
- }
-
public static Bpl.Variable TempThisVar() {
return new Bpl.GlobalVariable(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, "this", Bpl.Type.Int));
}
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index 703c908f..87514ae9 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -3,8 +3,6 @@
const null: ref;
-type box;
-
type ref = int;
type HeapType = [ref,Field]box;
@@ -188,8 +186,6 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
-type Field;
-
var $Heap: HeapType where IsGoodHeap($Heap);
function Box2Int(box) : int;
@@ -210,6 +206,10 @@ function {:inline true} Write(H: HeapType, o: ref, f: Field, v: box) : HeapType
H[o, f := v]
}
+type Field;
+
+type box;
+
type Type;
function $DynamicType(ref) : Type;
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 5245bf3d..e6d6e7fd 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -188,6 +188,10 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
+type Field;
+
+type box;
+
type Type;
function $DynamicType(ref) : Type;
diff --git a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
index cef103b7..b0dd1907 100644
--- a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
+++ b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
@@ -102,15 +102,9 @@
</ProjectReference>
</ItemGroup>
<ItemGroup>
- <EmbeddedResource Include="TwoDIntHeapInput.txt" />
- </ItemGroup>
- <ItemGroup>
<EmbeddedResource Include="SplitFieldsHeapInput.txt" />
</ItemGroup>
<ItemGroup>
- <EmbeddedResource Include="TwoDBoxHeapInput.txt" />
- </ItemGroup>
- <ItemGroup>
<EmbeddedResource Include="GeneralHeapInput.txt" />
</ItemGroup>
<Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />
diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
deleted file mode 100644
index c23df829..00000000
--- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt
+++ /dev/null
@@ -1,729 +0,0 @@
-// Copyright (c) 2010, Microsoft Corp.
-// Bytecode Translator prelude
-
-const null: int;
-
-type box;
-
-type HeapType = [int,int]box;
-
-function IsGoodHeap(HeapType) : bool;
-
-var $ArrayContents: [int][int]int;
-
-var $ArrayLength: [int]int;
-
-var $Alloc: [int]bool;
-
-procedure {:inline 1} Alloc() returns (x: int);
- modifies $Alloc;
- free ensures x != 0;
-
-
-
-implementation Alloc() returns (x: int)
-{
- assume $Alloc[x] == false;
- $Alloc[x] := true;
-}
-
-
-
-procedure DelegateAdd(a: int, b: int) returns (c: int);
-
-
-
-implementation DelegateAdd(a: int, b: int) returns (c: int)
-{
- var m: int;
- var o: int;
-
- if (a == 0)
- {
- c := b;
- return;
- }
- else if (b == 0)
- {
- c := a;
- return;
- }
-
- call m, o := GetFirstElement(b);
- call c := Alloc();
- $Head[c] := $Head[a];
- $Next[c] := $Next[a];
- $Method[c] := $Method[a];
- $Receiver[c] := $Receiver[a];
- call c := DelegateAddHelper(c, m, o);
-}
-
-
-
-procedure DelegateRemove(a: int, b: int) returns (c: int);
-
-
-
-implementation DelegateRemove(a: int, b: int) returns (c: int)
-{
- var m: int;
- var o: int;
-
- if (a == 0)
- {
- c := 0;
- return;
- }
- else if (b == 0)
- {
- c := a;
- return;
- }
-
- call m, o := GetFirstElement(b);
- call c := Alloc();
- $Head[c] := $Head[a];
- $Next[c] := $Next[a];
- $Method[c] := $Method[a];
- $Receiver[c] := $Receiver[a];
- call c := DelegateRemoveHelper(c, m, o);
-}
-
-
-
-procedure GetFirstElement(i: int) returns (m: int, o: int);
-
-
-
-implementation GetFirstElement(i: int) returns (m: int, o: int)
-{
- var first: int;
-
- first := $Next[i][$Head[i]];
- m := $Method[i][first];
- o := $Receiver[i][first];
-}
-
-
-
-procedure DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int);
-
-
-
-implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int)
-{
- var x: int;
- var h: int;
-
- if (oldi == 0)
- {
- call i := Alloc();
- call x := Alloc();
- $Head[i] := x;
- $Next[i] := $Next[i][x := x];
- }
- else
- {
- i := oldi;
- }
-
- h := $Head[i];
- $Method[i] := $Method[i][h := m];
- $Receiver[i] := $Receiver[i][h := o];
- call x := Alloc();
- $Next[i] := $Next[i][x := $Next[i][h]];
- $Next[i] := $Next[i][h := x];
- $Head[i] := x;
-}
-
-
-
-procedure DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int);
-
-
-
-implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
-{
- var prev: int;
- var iter: int;
- var niter: int;
-
- i := oldi;
- if (i == 0)
- {
- return;
- }
-
- prev := 0;
- iter := $Head[i];
- while (true)
- {
- niter := $Next[i][iter];
- if (niter == $Head[i])
- {
- break;
- }
-
- if ($Method[i][niter] == m && $Receiver[i][niter] == o)
- {
- prev := iter;
- }
-
- iter := niter;
- }
-
- if (prev == 0)
- {
- return;
- }
-
- $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]];
- if ($Next[i][$Head[i]] == $Head[i])
- {
- i := 0;
- }
-}
-
-
-
-var $Heap: HeapType where IsGoodHeap($Heap);
-
-function Box2Int(box) : int;
-
-function Box2Bool(box) : bool;
-
-function Int2Box(int) : box;
-
-function Bool2Box(bool) : box;
-
-type Type;
-
-function $DynamicType(ref) : Type;
-
-function $TypeOf(Type) : ref;
-
-var $Head: [int]int;
-
-var $Next: [int][int]int;
-
-var $Method: [int][int]int;
-
-var $Receiver: [int][int]int;
-
-const unique RegressionTestInput.ClassWithArrayTypes: Type;
-
-var RegressionTestInput.ClassWithArrayTypes.s: int;
-
-const unique RegressionTestInput.ClassWithArrayTypes.a: int;
-
-procedure RegressionTestInput.ClassWithArrayTypes.Main1();
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.Main1()
-{
- var local_0: int;
- var $tmp0: int;
- var local_1: int;
- var $tmp1: int;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;
- call $tmp0 := Alloc();
- local_0 := $tmp0;
- assert {:sourceFile "Class1.cs"} {:sourceLine 87} true;
- $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 88} true;
- assert $ArrayContents[local_0][0] == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;
- call $tmp1 := Alloc();
- local_1 := $tmp1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 91} true;
- $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 92} true;
- assert $ArrayContents[local_1][0] == 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 94} true;
- assert $ArrayContents[local_0][0] == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 95} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithArrayTypes.Main2();
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.Main2()
-{
- var $tmp2: int;
- var local_0: int;
- var $tmp3: int;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;
- call $tmp2 := Alloc();
- RegressionTestInput.ClassWithArrayTypes.s := $tmp2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 101} true;
- $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 102} true;
- assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;
- call $tmp3 := Alloc();
- local_0 := $tmp3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 105} true;
- $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 106} true;
- assert $ArrayContents[local_0][0] == 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 108} true;
- assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 109} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int);
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int)
-{
- var x: int;
-
- x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 114} true;
- $ArrayContents := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a]) := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x := 42]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 115} true;
- $ArrayContents := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a]) := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x + 1 := 43]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 116} true;
- assert $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x + 1] == $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x] + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 117} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int);
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int)
-{
- var xs: int;
-
- xs := xs$in;
- if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true))
- {
- assert {:sourceFile "Class1.cs"} {:sourceLine 121} true;
- $ArrayContents := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a]) := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][0 := $ArrayContents[xs][0]]];
- }
- else
- {
- }
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 123} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
-
-
-
-procedure System.Object.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)
-{
- $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := Int2Box(0);
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithArrayTypes.#cctor();
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.#cctor()
-{
- RegressionTestInput.ClassWithArrayTypes.s := 0;
-}
-
-
-
-const unique RegressionTestInput.Class0: Type;
-
-var RegressionTestInput.Class0.StaticInt: int;
-
-procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);
-
-
-
-implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)
-{
- var x: int;
-
- x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;
- $result := x + 1;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int);
-
-
-
-implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
-{
- var x: int;
- var __temp_1: int;
- var $tmp4: int;
- var local_0: int;
-
- x := x$in;
- $tmp4 := x;
- assert $tmp4 != 0;
- __temp_1 := 5 / $tmp4;
- x := 3;
- local_0 := __temp_1 + 3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;
- assert (if x == 3 then local_0 <= 8 else false);
- assert {:sourceFile "Class1.cs"} {:sourceLine 23} true;
- RegressionTestInput.Class0.StaticInt := local_0;
- assert {:sourceFile "Class1.cs"} {:sourceLine 24} true;
- assert local_0 == RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 25} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int);
-
-
-
-implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int)
-{
- var x: int;
- var y: int;
-
- x := x$in;
- y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 28} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool);
-
-
-
-implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool)
-{
- var b: bool;
-
- b := b$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 29} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int);
-
-
-
-implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int)
-{
- var c: int;
-
- c := c$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 30} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);
-
-
-
-implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int)
-{
- var $tmp5: int;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 34} true;
- call $tmp5 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
- $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);
-
-
-
-implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)
-{
- assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;
- x$out := 3 + RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;
- $result := x$out;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);
-
-
-
-implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)
-{
- x$out := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 42} true;
- x$out := x$out + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;
- RegressionTestInput.Class0.StaticInt := x$out;
- assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;
- $result := x$out;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int);
-
-
-
-implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)
-{
- var x: int;
-
- x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 48} true;
- x := x + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 49} true;
- RegressionTestInput.Class0.StaticInt := x;
- assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;
- $result := x;
- return;
-}
-
-
-
-procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int);
-
-
-
-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)
-{
- var x: int;
-
- x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 56} true;
- $result := x;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int);
-
-
-
-implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)
-{
- var y: int;
- var $tmp6: int;
-
- y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 60} true;
- call {:async} $tmp6 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
- $result := $tmp6;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.Class0.#ctor(this: int)
-{
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.#cctor();
-
-
-
-implementation RegressionTestInput.Class0.#cctor()
-{
- RegressionTestInput.Class0.StaticInt := 0;
-}
-
-
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
-{
- assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(Box2Int($Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x]));
- assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
-{
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := Int2Box(0);
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(0);
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.ClassWithBoolTypes: Type;
-
-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
-
-const unique RegressionTestInput.ClassWithBoolTypes.b: bool;
-
-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool)
-{
- var x: int;
- var y: int;
-
- x := x$in;
- y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
- $result := x < y;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)
-{
- var z: bool;
-
- z := z$in;
- $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(false);
- assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
- call System.Object.#ctor(this);
- assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
- $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(z);
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- if (z)
- {
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- RegressionTestInput.ClassWithBoolTypes.staticB := z;
- }
- else
- {
- }
-
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.Main();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.Main()
-{
- var $tmp7: bool;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 78} true;
- call $tmp7 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
- assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
-{
- RegressionTestInput.ClassWithBoolTypes.staticB := false;
-}
-
-
-
-const unique RegressionTestInput.AsyncAttribute: Type;
-
-procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
-
-
-
-procedure System.Attribute.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
-{
- call System.Attribute.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.AsyncAttribute.#cctor();
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#cctor()
-{
-}
-
-
diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
deleted file mode 100644
index 262958c0..00000000
--- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
+++ /dev/null
@@ -1,719 +0,0 @@
-// Copyright (c) 2010, Microsoft Corp.
-// Bytecode Translator prelude
-
-const null: int;
-
-type HeapType = [int,int]int;
-
-function IsGoodHeap(HeapType) : bool;
-
-var $ArrayContents: [int][int]int;
-
-var $ArrayLength: [int]int;
-
-var $Alloc: [int]bool;
-
-procedure {:inline 1} Alloc() returns (x: int);
- modifies $Alloc;
- free ensures x != 0;
-
-
-
-implementation Alloc() returns (x: int)
-{
- assume $Alloc[x] == false;
- $Alloc[x] := true;
-}
-
-
-
-procedure DelegateAdd(a: int, b: int) returns (c: int);
-
-
-
-implementation DelegateAdd(a: int, b: int) returns (c: int)
-{
- var m: int;
- var o: int;
-
- if (a == 0)
- {
- c := b;
- return;
- }
- else if (b == 0)
- {
- c := a;
- return;
- }
-
- call m, o := GetFirstElement(b);
- call c := Alloc();
- $Head[c] := $Head[a];
- $Next[c] := $Next[a];
- $Method[c] := $Method[a];
- $Receiver[c] := $Receiver[a];
- call c := DelegateAddHelper(c, m, o);
-}
-
-
-
-procedure DelegateRemove(a: int, b: int) returns (c: int);
-
-
-
-implementation DelegateRemove(a: int, b: int) returns (c: int)
-{
- var m: int;
- var o: int;
-
- if (a == 0)
- {
- c := 0;
- return;
- }
- else if (b == 0)
- {
- c := a;
- return;
- }
-
- call m, o := GetFirstElement(b);
- call c := Alloc();
- $Head[c] := $Head[a];
- $Next[c] := $Next[a];
- $Method[c] := $Method[a];
- $Receiver[c] := $Receiver[a];
- call c := DelegateRemoveHelper(c, m, o);
-}
-
-
-
-procedure GetFirstElement(i: int) returns (m: int, o: int);
-
-
-
-implementation GetFirstElement(i: int) returns (m: int, o: int)
-{
- var first: int;
-
- first := $Next[i][$Head[i]];
- m := $Method[i][first];
- o := $Receiver[i][first];
-}
-
-
-
-procedure DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int);
-
-
-
-implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int)
-{
- var x: int;
- var h: int;
-
- if (oldi == 0)
- {
- call i := Alloc();
- call x := Alloc();
- $Head[i] := x;
- $Next[i] := $Next[i][x := x];
- }
- else
- {
- i := oldi;
- }
-
- h := $Head[i];
- $Method[i] := $Method[i][h := m];
- $Receiver[i] := $Receiver[i][h := o];
- call x := Alloc();
- $Next[i] := $Next[i][x := $Next[i][h]];
- $Next[i] := $Next[i][h := x];
- $Head[i] := x;
-}
-
-
-
-procedure DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int);
-
-
-
-implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int)
-{
- var prev: int;
- var iter: int;
- var niter: int;
-
- i := oldi;
- if (i == 0)
- {
- return;
- }
-
- prev := 0;
- iter := $Head[i];
- while (true)
- {
- niter := $Next[i][iter];
- if (niter == $Head[i])
- {
- break;
- }
-
- if ($Method[i][niter] == m && $Receiver[i][niter] == o)
- {
- prev := iter;
- }
-
- iter := niter;
- }
-
- if (prev == 0)
- {
- return;
- }
-
- $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]];
- if ($Next[i][$Head[i]] == $Head[i])
- {
- i := 0;
- }
-}
-
-
-
-var $Heap: HeapType where IsGoodHeap($Heap);
-
-type Type;
-
-function $DynamicType(ref) : Type;
-
-function $TypeOf(Type) : ref;
-
-var $Head: [int]int;
-
-var $Next: [int][int]int;
-
-var $Method: [int][int]int;
-
-var $Receiver: [int][int]int;
-
-const unique RegressionTestInput.ClassWithArrayTypes: Type;
-
-var RegressionTestInput.ClassWithArrayTypes.s: int;
-
-const unique RegressionTestInput.ClassWithArrayTypes.a: int;
-
-procedure RegressionTestInput.ClassWithArrayTypes.Main1();
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.Main1()
-{
- var local_0: int;
- var $tmp0: int;
- var local_1: int;
- var $tmp1: int;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;
- call $tmp0 := Alloc();
- local_0 := $tmp0;
- assert {:sourceFile "Class1.cs"} {:sourceLine 87} true;
- $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 88} true;
- assert $ArrayContents[local_0][0] == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;
- call $tmp1 := Alloc();
- local_1 := $tmp1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 91} true;
- $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 92} true;
- assert $ArrayContents[local_1][0] == 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 94} true;
- assert $ArrayContents[local_0][0] == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 95} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithArrayTypes.Main2();
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.Main2()
-{
- var $tmp2: int;
- var local_0: int;
- var $tmp3: int;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;
- call $tmp2 := Alloc();
- RegressionTestInput.ClassWithArrayTypes.s := $tmp2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 101} true;
- $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 102} true;
- assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;
- call $tmp3 := Alloc();
- local_0 := $tmp3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 105} true;
- $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 106} true;
- assert $ArrayContents[local_0][0] == 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 108} true;
- assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;
- assert {:sourceFile "Class1.cs"} {:sourceLine 109} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int);
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int)
-{
- var x: int;
-
- x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 114} true;
- $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x := 42]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 115} true;
- $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x + 1 := 43]];
- assert {:sourceFile "Class1.cs"} {:sourceLine 116} true;
- assert $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x + 1] == $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x] + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 117} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int);
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int)
-{
- var xs: int;
-
- xs := xs$in;
- if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true))
- {
- assert {:sourceFile "Class1.cs"} {:sourceLine 121} true;
- $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][0 := $ArrayContents[xs][0]]];
- }
- else
- {
- }
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 123} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int);
-
-
-
-procedure System.Object.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int)
-{
- $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := 0;
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithArrayTypes.#cctor();
-
-
-
-implementation RegressionTestInput.ClassWithArrayTypes.#cctor()
-{
- RegressionTestInput.ClassWithArrayTypes.s := 0;
-}
-
-
-
-const unique RegressionTestInput.Class0: Type;
-
-var RegressionTestInput.Class0.StaticInt: int;
-
-procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);
-
-
-
-implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)
-{
- var x: int;
-
- x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;
- $result := x + 1;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int);
-
-
-
-implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int)
-{
- var x: int;
- var __temp_1: int;
- var $tmp4: int;
- var local_0: int;
-
- x := x$in;
- $tmp4 := x;
- assert $tmp4 != 0;
- __temp_1 := 5 / $tmp4;
- x := 3;
- local_0 := __temp_1 + 3;
- assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;
- assert (if x == 3 then local_0 <= 8 else false);
- assert {:sourceFile "Class1.cs"} {:sourceLine 23} true;
- RegressionTestInput.Class0.StaticInt := local_0;
- assert {:sourceFile "Class1.cs"} {:sourceLine 24} true;
- assert local_0 == RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 25} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int);
-
-
-
-implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int)
-{
- var x: int;
- var y: int;
-
- x := x$in;
- y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 28} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool);
-
-
-
-implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool)
-{
- var b: bool;
-
- b := b$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 29} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int);
-
-
-
-implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int)
-{
- var c: int;
-
- c := c$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 30} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int);
-
-
-
-implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int)
-{
- var $tmp5: int;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 34} true;
- call $tmp5 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);
- $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int);
-
-
-
-implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int)
-{
- assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;
- x$out := 3 + RegressionTestInput.Class0.StaticInt;
- assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;
- $result := x$out;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int);
-
-
-
-implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int)
-{
- x$out := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 42} true;
- x$out := x$out + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;
- RegressionTestInput.Class0.StaticInt := x$out;
- assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;
- $result := x$out;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int);
-
-
-
-implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)
-{
- var x: int;
-
- x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 48} true;
- x := x + 1;
- assert {:sourceFile "Class1.cs"} {:sourceLine 49} true;
- RegressionTestInput.Class0.StaticInt := x;
- assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;
- $result := x;
- return;
-}
-
-
-
-procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int);
-
-
-
-implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)
-{
- var x: int;
-
- x := x$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 56} true;
- $result := x;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int);
-
-
-
-implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)
-{
- var y: int;
- var $tmp6: int;
-
- y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 60} true;
- call {:async} $tmp6 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);
- $result := $tmp6;
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.Class0.#ctor(this: int)
-{
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.Class0.#cctor();
-
-
-
-implementation RegressionTestInput.Class0.#cctor()
-{
- RegressionTestInput.Class0.StaticInt := 0;
-}
-
-
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int;
-
-const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int;
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int)
-{
- assert {:sourceFile "Class1.cs"} {:sourceLine 130} true;
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x];
- assert {:sourceFile "Class1.cs"} {:sourceLine 131} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int)
-{
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := 0;
- $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := 0;
- call System.Object.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor();
-
-
-
-implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor()
-{
-}
-
-
-
-const unique RegressionTestInput.ClassWithBoolTypes: Type;
-
-var RegressionTestInput.ClassWithBoolTypes.staticB: bool;
-
-const unique RegressionTestInput.ClassWithBoolTypes.b: bool;
-
-procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool);
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool)
-{
- var x: int;
- var y: int;
-
- x := x$in;
- y := y$in;
- assert {:sourceFile "Class1.cs"} {:sourceLine 70} true;
- $result := x < y;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool);
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool)
-{
- var z: bool;
-
- z := z$in;
- $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := false;
- assert {:sourceFile "Class1.cs"} {:sourceLine 72} true;
- call System.Object.#ctor(this);
- assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;
- $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := z;
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- if (z)
- {
- assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;
- RegressionTestInput.ClassWithBoolTypes.staticB := z;
- }
- else
- {
- }
-
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.Main();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.Main()
-{
- var $tmp7: bool;
-
- assert {:sourceFile "Class1.cs"} {:sourceLine 78} true;
- call $tmp7 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4);
- assert {:sourceFile "Class1.cs"} {:sourceLine 79} true;
- return;
-}
-
-
-
-procedure RegressionTestInput.ClassWithBoolTypes.#cctor();
-
-
-
-implementation RegressionTestInput.ClassWithBoolTypes.#cctor()
-{
- RegressionTestInput.ClassWithBoolTypes.staticB := false;
-}
-
-
-
-const unique RegressionTestInput.AsyncAttribute: Type;
-
-procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
-
-
-
-procedure System.Attribute.#ctor(this: int);
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#ctor(this: int)
-{
- call System.Attribute.#ctor(this);
- return;
-}
-
-
-
-procedure RegressionTestInput.AsyncAttribute.#cctor();
-
-
-
-implementation RegressionTestInput.AsyncAttribute.#cctor()
-{
-}
-
-
diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index dadeb4e5..99b6e680 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -68,21 +68,6 @@ namespace TranslationTest {
}
[TestMethod]
- public void TwoDIntHeap() {
- string dir = TestContext.DeploymentDirectory;
- var fullPath = Path.Combine(dir, "RegressionTestInput.dll");
- Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.TwoDIntHeapInput.txt");
- StreamReader reader = new StreamReader(resource);
- string expected = reader.ReadToEnd();
- var result = ExecuteTest(fullPath, new TwoDIntHeap());
- if (result != expected) {
- string resultFile = Path.GetFullPath("TwoDIntHeapOutput.txt");
- File.WriteAllText(resultFile, result);
- Assert.Fail("Output didn't match TwoDIntHeapInput.txt: " + resultFile);
- }
- }
-
- [TestMethod]
public void SplitFieldsHeap() {
string dir = TestContext.DeploymentDirectory;
var fullPath = Path.Combine(dir, "RegressionTestInput.dll");
@@ -98,21 +83,6 @@ namespace TranslationTest {
}
[TestMethod]
- public void TwoDBoxHeap() {
- string dir = TestContext.DeploymentDirectory;
- var fullPath = Path.Combine(dir, "RegressionTestInput.dll");
- Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.TwoDBoxHeapInput.txt");
- StreamReader reader = new StreamReader(resource);
- string expected = reader.ReadToEnd();
- var result = ExecuteTest(fullPath, new TwoDBoxHeap());
- if (result != expected) {
- string resultFile = Path.GetFullPath("TwoDBoxHeapOutput.txt");
- File.WriteAllText(resultFile, result);
- Assert.Fail("Output didn't match TwoDBoxHeapInput.txt: " + resultFile);
- }
- }
-
- [TestMethod]
public void GeneralHeap() {
string dir = TestContext.DeploymentDirectory;
var fullPath = Path.Combine(dir, "RegressionTestInput.dll");
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 12:23:55 +0000