diff options
| author |  qadeer <unknown> | 2011-02-25 01:42:14 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2011-02-25 01:42:14 +0000 |
| commit | 75e5921cb1cd956d6d317af1957e3e726b1b00fc (patch) | |
| tree | 13874f7ee94ef144ede1ac551b97419101eee7e8 | |
| parent | 52c7b0169c73ff1351582d2b02b2adb52bc0d20c (diff) | |
implemented delegates and events
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 90 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 272 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 154 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 109 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 77 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 9 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 165 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 165 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt | 165 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt | 165 |
10 files changed, 1198 insertions, 173 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 75f376f5..822185aa 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -404,16 +404,18 @@ namespace BytecodeTranslator public override void Visit(IMethodCall methodCall)
{
var resolvedMethod = methodCall.MethodToCall.ResolvedMethod;
-
+
#region Translate In Parameters
var inexpr = new List<Bpl.Expr>();
#region Create the 'this' argument for the function call
+ Bpl.Expr thisExpr = null;
if (!methodCall.IsStaticCall)
{
this.Visit(methodCall.ThisArgument);
- inexpr.Add(this.TranslatedExpressions.Pop());
+ thisExpr = this.TranslatedExpressions.Pop();
+ inexpr.Add(thisExpr);
}
#endregion
@@ -486,12 +488,55 @@ namespace BytecodeTranslator }
Bpl.CallCmd call;
- if (attrib != null)
- call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);
- else
- call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);
- this.StmtTraverser.StmtBuilder.Add(call);
+ bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");
+ bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");
+ if (isEventAdd || isEventRemove)
+ {
+ Bpl.Variable eventVar = null;
+ Bpl.Variable local = null;
+ foreach (var e in resolvedMethod.ContainingTypeDefinition.Events)
+ {
+ if (e.Adder != null && e.Adder.ResolvedMethod == resolvedMethod)
+ {
+ eventVar = this.sink.FindOrCreateEventVariable(e);
+ local = this.sink.CreateFreshLocal(e.Type);
+ break;
+ }
+ }
+ if (methodCall.IsStaticCall)
+ {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));
+ 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))));
+ inexpr[0] = Bpl.Expr.Ident(local);
+ }
+ System.Diagnostics.Debug.Assert(outvars.Count == 0);
+ outvars.Add(Bpl.Expr.Ident(local));
+ string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;
+ call = new Bpl.CallCmd(methodCall.Token(), methodName, inexpr, outvars);
+ this.StmtTraverser.StmtBuilder.Add(call);
+ if (methodCall.IsStaticCall)
+ {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));
+ }
+ else
+ {
+ this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));
+ }
+ }
+ else
+ {
+ string methodName = TranslationHelper.CreateUniqueMethodName(methodCall.MethodToCall);
+ if (attrib != null)
+ call = new Bpl.CallCmd(cloc, methodName, inexpr, outvars, attrib);
+ else
+ call = new Bpl.CallCmd(cloc, methodName, inexpr, outvars);
+ this.StmtTraverser.StmtBuilder.Add(call);
+ }
}
}
@@ -587,8 +632,14 @@ namespace BytecodeTranslator public override void Visit(ICreateDelegateInstance createDelegateInstance)
{
- TranslateDelegateCreation(createDelegateInstance.MethodToCallViaDelegate, createDelegateInstance.Type);
- //base.Visit(createDelegateInstance);
+ if (createDelegateInstance.Instance == null) {
+ TranslatedExpressions.Push(Bpl.Expr.Literal(0));
+ }
+ else {
+ this.Visit(createDelegateInstance.Instance);
+ }
+
+ TranslateDelegateCreation(createDelegateInstance.MethodToCallViaDelegate, createDelegateInstance.Type, createDelegateInstance);
}
private void TranslateArrayCreation(IExpression creationAST)
@@ -603,7 +654,6 @@ namespace BytecodeTranslator TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
-
private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, ITypeReference ctorType, IExpression creationAST)
{
Bpl.IToken token = creationAST.Token();
@@ -655,14 +705,20 @@ namespace BytecodeTranslator TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
- private void TranslateDelegateCreation(IMethodReference methodToCall, ITypeReference type)
+ private void TranslateDelegateCreation(IMethodReference methodToCall, ITypeReference type, IExpression creationAST)
{
- string methodName = TranslationHelper.CreateUniqueMethodName(methodToCall);
- var typedIdent = new Bpl.TypedIdent(Bpl.Token.NoToken, methodName, Bpl.Type.Int);
- var constant = new Bpl.Constant(Bpl.Token.NoToken, typedIdent, true);
- sink.TranslatedProgram.TopLevelDeclarations.Add(constant);
- TranslatedExpressions.Push(Bpl.Expr.Ident(constant));
- sink.AddDelegate(type.ResolvedType, constant);
+ Bpl.IToken cloc = creationAST.Token();
+ var a = this.sink.CreateFreshLocal(creationAST.Type);
+
+ sink.AddDelegate(type.ResolvedType, methodToCall.ResolvedMethod);
+ Bpl.Constant constant = sink.FindOrAddDelegateMethodConstant(methodToCall.ResolvedMethod);
+ Bpl.Expr methodExpr = Bpl.Expr.Ident(constant);
+ Bpl.Expr instanceExpr = TranslatedExpressions.Pop();
+
+ this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, this.sink.DelegateAddHelperName,
+ new Bpl.ExprSeq(Bpl.Expr.Literal(0), Bpl.Expr.Ident(constant), instanceExpr),
+ new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
#endregion
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index 6171c4e9..ee5206db 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -27,7 +27,7 @@ namespace BytecodeTranslator { /// a two-dimensional array indexed by objects and fields, each of which
/// are represented as an integer.
/// </summary>
- public class TwoDIntHeap : HeapFactory, IHeap {
+ public class TwoDIntHeap : Heap {
#region Fields
[RepresentationFor("$Heap", "var $Heap: HeapType where IsGoodHeap($Heap);", true)]
@@ -57,14 +57,16 @@ procedure {:inline 1} Alloc() returns (x: int) assume $Alloc[x] == false;
$Alloc[x] := true;
}
+
";
-
+
#endregion
- public override bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program) {
+ public override bool MakeHeap(Sink sink, out Heap heap, out Bpl.Program/*?*/ program) {
heap = this;
program = null;
- var b = RepresentationFor.ParsePrelude(this.InitialPreludeText, this, out program);
+ string prelude = this.InitialPreludeText + this.DelegateEncodingText;
+ var b = RepresentationFor.ParsePrelude(prelude, this, out program);
return b;
}
@@ -72,7 +74,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
/// on its type based on the heap representation.
/// </summary>
- public Bpl.Variable CreateFieldVariable(IFieldReference field) {
+ public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
Bpl.Variable v;
string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
Bpl.IToken tok = field.Token();
@@ -81,19 +83,37 @@ procedure {:inline 1} Alloc() returns (x: int) if (field.IsStatic) {
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
v = new Bpl.GlobalVariable(tok, tident);
- } else {
+ }
+ 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>
/// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding
/// on its type based on the heap representation. I.e., the value of this
/// variable represents the value of the expression "typeof(type)".
/// </summary>
- public Bpl.Variable CreateTypeVariable(ITypeReference type) {
+ public override Bpl.Variable CreateTypeVariable(ITypeReference type) {
return null;
}
@@ -108,7 +128,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// <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 Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f) {
+ 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 });
}
@@ -118,7 +138,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
/// field.
/// </summary>
- public Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {
+ 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
@@ -131,7 +151,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// Returns the BPL expression that corresponds to the value of the dynamic type
/// of the object represented by the expression <paramref name="o"/>.
/// </summary>
- public Bpl.Expr DynamicType(Bpl.Expr o) {
+ public override Bpl.Expr DynamicType(Bpl.Expr o) {
// $DymamicType(o)
return null;
}
@@ -143,7 +163,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// field. Each global variable is a map from int to T where T is the
/// type of the field.
/// </summary>
- public class SplitFieldsHeap : HeapFactory {
+ public class SplitFieldsHeap : Heap {
/// <summary>
/// Prelude text for which access to the ASTs is not needed
@@ -166,85 +186,98 @@ procedure {:inline 1} Alloc() returns (x: int) }
";
- public override bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program) {
- heap = new HeapRepresentation(sink);
+ public override bool MakeHeap(Sink sink, out Heap heap, out Bpl.Program/*?*/ program) {
+ heap = this;
program = null;
- var b = RepresentationFor.ParsePrelude(this.InitialPreludeText, this, out program);
+ string prelude = this.InitialPreludeText + this.DelegateEncodingText;
+ var b = RepresentationFor.ParsePrelude(prelude, this, out program);
return b;
}
- private class HeapRepresentation : IHeap {
+ /// <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);
- public HeapRepresentation(Sink sink) {
+ if (field.IsStatic) {
+ Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
+ v = new Bpl.GlobalVariable(tok, tident);
+ }
+ else {
+ Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Bpl.Type.Int), t);
+ Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, mt);
+ v = new Bpl.GlobalVariable(tok, tident);
}
+ return v;
+ }
- /// <summary>
- /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
- /// on its type based on the heap representation.
- /// </summary>
- public 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);
+ 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 (field.IsStatic) {
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
- v = new Bpl.GlobalVariable(tok, tident);
- } else {
- Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Bpl.Type.Int), t);
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, mt);
- v = new Bpl.GlobalVariable(tok, tident);
- }
- return v;
+ if (e.Adder.ResolvedMethod.IsStatic) {
+ Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, eventName, t);
+ v = new Bpl.GlobalVariable(tok, tident);
}
-
- /// <summary>
- /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding
- /// on its type based on the heap representation. I.e., the value of this
- /// variable represents the value of the expression "typeof(type)".
- /// </summary>
- public Bpl.Variable CreateTypeVariable(ITypeReference type) {
- return null;
+ else {
+ Bpl.Type mt = new Bpl.MapType(tok, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Bpl.Type.Int), t);
+ Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, eventName, mt);
+ v = new Bpl.GlobalVariable(tok, tident);
}
+ 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 Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f) {
- return Bpl.Expr.Select(f, o);
- }
+ /// <summary>
+ /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding
+ /// on its type based on the heap representation. I.e., the value of this
+ /// variable represents the value of the expression "typeof(type)".
+ /// </summary>
+ public override Bpl.Variable CreateTypeVariable(ITypeReference type) {
+ return null;
+ }
- /// <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 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, f, o, value);
- }
+ /// <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(f, o);
+ }
- /// <summary>
- /// Returns the BPL expression that corresponds to the value of the dynamic type
- /// of the object represented by the expression <paramref name="o"/>.
- /// </summary>
- public Bpl.Expr DynamicType(Bpl.Expr o) {
- // $DymamicType(o)
- return null;
- }
+ /// <summary>
+ /// Returns the BPL expression that corresponds to the value of the dynamic type
+ /// of the object represented by the expression <paramref name="o"/>.
+ /// </summary>
+ public override Bpl.Expr DynamicType(Bpl.Expr o) {
+ // $DymamicType(o)
+ return null;
+ }
+ /// <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, f, o, value);
}
}
@@ -256,7 +289,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// 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 : HeapFactory, IHeap {
+ public class TwoDBoxHeap : Heap {
#region Fields
[RepresentationFor("$Heap", "var $Heap: HeapType where IsGoodHeap($Heap);", true)]
@@ -298,11 +331,12 @@ procedure {:inline 1} Alloc() returns (x: int) #endregion
- public override bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program) {
+ public override bool MakeHeap(Sink sink, out Heap heap, out Bpl.Program/*?*/ program) {
this.sink = sink;
heap = this;
program = null;
- var b = RepresentationFor.ParsePrelude(this.InitialPreludeText, this, out program);
+ string prelude = this.InitialPreludeText + this.DelegateEncodingText;
+ var b = RepresentationFor.ParsePrelude(prelude, this, out program);
return b;
}
@@ -310,7 +344,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
/// on its type based on the heap representation.
/// </summary>
- public Bpl.Variable CreateFieldVariable(IFieldReference field) {
+ public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
Bpl.Variable v;
string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
Bpl.IToken tok = field.Token();
@@ -319,7 +353,25 @@ procedure {:inline 1} Alloc() returns (x: int) if (field.IsStatic) {
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
v = new Bpl.GlobalVariable(tok, tident);
- } else {
+ }
+ 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);
}
@@ -331,7 +383,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// on its type based on the heap representation. I.e., the value of this
/// variable represents the value of the expression "typeof(type)".
/// </summary>
- public Bpl.Variable CreateTypeVariable(ITypeReference type) {
+ public override Bpl.Variable CreateTypeVariable(ITypeReference type) {
return null;
}
@@ -346,7 +398,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// <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 Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f) {
+ 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
@@ -372,10 +424,11 @@ procedure {:inline 1} Alloc() returns (x: int) /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
/// field.
/// </summary>
- public Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {
+ 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 {
+ }
+ else {
// wrap it in the right conversion function
Bpl.Function conversion;
if (f.Type == Bpl.Type.Bool)
@@ -401,7 +454,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// Returns the BPL expression that corresponds to the value of the dynamic type
/// of the object represented by the expression <paramref name="o"/>.
/// </summary>
- public Bpl.Expr DynamicType(Bpl.Expr o) {
+ public override Bpl.Expr DynamicType(Bpl.Expr o) {
// $DymamicType(o)
return null;
}
@@ -413,7 +466,7 @@ procedure {:inline 1} Alloc() returns (x: int) /// for all heap reads and writes. That way the decision about
/// how to exactly represent the heap is made in the Prelude.
/// </summary>
- public class GeneralHeap : HeapFactory, IHeap {
+ public class GeneralHeap : Heap {
#region Fields
@@ -474,11 +527,12 @@ procedure {:inline 1} Alloc() returns (x: ref) #endregion
- public override bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program) {
+ public override bool MakeHeap(Sink sink, out Heap heap, out Bpl.Program/*?*/ program) {
this.sink = sink;
heap = this;
program = null;
- var b = RepresentationFor.ParsePrelude(this.InitialPreludeText, this, out program);
+ string prelude = this.InitialPreludeText + this.DelegateEncodingText;
+ var b = RepresentationFor.ParsePrelude(prelude, this, out program);
if (b) {
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());
@@ -490,7 +544,7 @@ procedure {:inline 1} Alloc() returns (x: ref) /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
/// on its type based on the heap representation.
/// </summary>
- public Bpl.Variable CreateFieldVariable(IFieldReference field) {
+ public override Bpl.Variable CreateFieldVariable(IFieldReference field) {
Bpl.Variable v;
string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
Bpl.IToken tok = field.Token();
@@ -499,7 +553,8 @@ procedure {:inline 1} Alloc() returns (x: ref) Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
v = new Bpl.GlobalVariable(tok, tident);
- } else {
+ }
+ else {
Bpl.Type t = this.FieldType;
Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
v = new Bpl.Constant(tok, tident, true);
@@ -509,12 +564,31 @@ procedure {:inline 1} Alloc() returns (x: ref) }
private Dictionary<Bpl.Variable, ITypeReference> underlyingTypes = new Dictionary<Bpl.Variable, ITypeReference>();
+ public override Bpl.Variable CreateEventVariable(IEventDefinition e) {
+ Bpl.Variable v;
+ string fieldname = TypeHelper.GetTypeName(e.ContainingType) + "." + e.Name.Value;
+ Bpl.IToken tok = e.Token();
+
+ if (e.Adder.ResolvedMethod.IsStatic) {
+ Bpl.Type t = TranslationHelper.CciTypeToBoogie(e.Type.ResolvedType);
+ Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
+ v = new Bpl.GlobalVariable(tok, tident);
+ }
+ else {
+ Bpl.Type t = this.FieldType;
+ Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
+ v = new Bpl.Constant(tok, tident, true);
+ }
+ this.underlyingTypes.Add(v, e.Type);
+ return v;
+ }
+
/// <summary>
/// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding
/// on its type based on the heap representation. I.e., the value of this
/// variable represents the value of the expression "typeof(type)".
/// </summary>
- public Bpl.Variable CreateTypeVariable(ITypeReference type) {
+ public override Bpl.Variable CreateTypeVariable(ITypeReference type) {
Bpl.Variable v;
string typename = TypeHelper.GetTypeName(type);
Bpl.IToken tok = type.Token();
@@ -535,7 +609,7 @@ procedure {:inline 1} Alloc() returns (x: ref) /// <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 Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f) {
+ public override Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f) {
// $Read($Heap, o, f)
var callRead = new Bpl.NAryExpr(
f.tok,
@@ -567,10 +641,11 @@ procedure {:inline 1} Alloc() returns (x: ref) /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
/// field.
/// </summary>
- public Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {
+ 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 {
+ }
+ else {
// wrap it in the right conversion function
Bpl.Function conversion;
if (value.Type == Bpl.Type.Bool)
@@ -600,7 +675,7 @@ procedure {:inline 1} Alloc() returns (x: ref) /// Returns the BPL expression that corresponds to the value of the dynamic type
/// of the object represented by the expression <paramref name="o"/>.
/// </summary>
- public Bpl.Expr DynamicType(Bpl.Expr o) {
+ public override Bpl.Expr DynamicType(Bpl.Expr o) {
// $DymamicType(o)
var callDynamicType = new Bpl.NAryExpr(
o.tok,
@@ -616,7 +691,7 @@ procedure {:inline 1} Alloc() returns (x: ref) internal string name;
internal string declaration;
internal bool required;
- internal RepresentationFor(string name, string declaration) { this.name = name; this.declaration = declaration; this.required = true; }
+ internal RepresentationFor(string name, string declaration) { this.name = name; this.declaration = declaration; this.required = true; }
internal RepresentationFor(string name, string declaration, bool required) { this.name = name; this.declaration = declaration; this.required = required; }
internal static bool ParsePrelude(string initialPreludeText, object instance, out Bpl.Program/*?*/ prelude) {
@@ -632,7 +707,8 @@ procedure {:inline 1} Alloc() returns (x: ref) object[] cas = field.GetCustomAttributes(typeof(RepresentationFor), false);
if (cas == null || cas.Length == 0) { // only look at fields that have the attribute
fields[i] = null;
- } else {
+ }
+ else {
foreach (var a in cas) { // should be exactly one
RepresentationFor rf = a as RepresentationFor;
if (rf != null) {
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index fd1f312e..482058e9 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -30,13 +30,14 @@ namespace BytecodeTranslator { /// </summary>
Bpl.Variable CreateFieldVariable(IFieldReference field);
- /// <summary>
/// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding
/// on its type based on the heap representation. I.e., the value of this
/// variable represents the value of the expression "typeof(type)".
/// </summary>
Bpl.Variable CreateTypeVariable(ITypeReference type);
+ Bpl.Variable CreateEventVariable(IEventDefinition e);
+
/// <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
@@ -66,6 +67,155 @@ namespace BytecodeTranslator { }
+ public abstract class Heap : HeapFactory, IHeap
+ {
+ public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);
+
+ /// Creates a fresh BPL variable to represent <paramref name="type"/>, deciding
+ /// on its type based on the heap representation. I.e., the value of this
+ /// variable represents the value of the expression "typeof(type)".
+ /// </summary>
+ public abstract Bpl.Variable CreateTypeVariable(ITypeReference type);
+
+ public abstract Bpl.Variable CreateEventVariable(IEventDefinition e);
+
+ public abstract Bpl.Expr ReadHeap(Bpl.Expr o, Bpl.IdentifierExpr f);
+
+ public abstract Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr o, Bpl.IdentifierExpr f, Bpl.Expr value);
+
+ /// <summary>
+ /// Returns the BPL expression that corresponds to the value of the dynamic type
+ /// of the object represented by the expression <paramref name="o"/>.
+ /// </summary>
+ public abstract Bpl.Expr DynamicType(Bpl.Expr o);
+
+ protected readonly string DelegateEncodingText =
+ @"procedure 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)
+{
+ 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)
+{
+ 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)
+{
+ 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)
+{
+ 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;
+ }
+}
+
+";
+
+ [RepresentationFor("$Head", "var $Head: [int]int;")]
+ public Bpl.GlobalVariable DelegateHead = null;
+
+ [RepresentationFor("$Next", "var $Next: [int][int]int;")]
+ public Bpl.GlobalVariable DelegateNext = null;
+
+ [RepresentationFor("$Method", "var $Method: [int][int]int;")]
+ public Bpl.GlobalVariable DelegateMethod = null;
+
+ [RepresentationFor("$Receiver", "var $Receiver: [int][int]int;")]
+ public Bpl.GlobalVariable DelegateReceiver = null;
+ }
+
public abstract class HeapFactory {
/// <summary>
@@ -80,7 +230,7 @@ namespace BytecodeTranslator { /// false if and only if an error occurrs and the heap and/or program are not in a
/// good state to be used.
/// </returns>
- public abstract bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program);
+ public abstract bool MakeHeap(Sink sink, out Heap heap, out Bpl.Program/*?*/ program);
}
}
\ No newline at end of file diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 14923bff..8ff1ada2 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -32,9 +32,6 @@ namespace BytecodeTranslator { public readonly PdbReader/*?*/ PdbReader;
- public Bpl.Variable HeapVariable;
-
-
public MetadataTraverser(Sink sink, PdbReader/*?*/ pdbReader)
: base() {
this.sink = sink;
@@ -60,18 +57,33 @@ namespace BytecodeTranslator { }
}
+ private Bpl.IfCmd BuildBreakCmd(Bpl.Expr b) {
+ Bpl.StmtListBuilder ifStmtBuilder = new Bpl.StmtListBuilder();
+ ifStmtBuilder.Add(new Bpl.BreakCmd(b.tok, ""));
+ return new Bpl.IfCmd(b.tok, b, ifStmtBuilder.Collect(b.tok), null, null);
+ }
+
+ private Bpl.IfCmd BuildIfCmd(Bpl.Expr b, Bpl.Cmd cmd, Bpl.IfCmd ifCmd)
+ {
+ Bpl.StmtListBuilder ifStmtBuilder;
+ ifStmtBuilder = new Bpl.StmtListBuilder();
+ ifStmtBuilder.Add(cmd);
+ return new Bpl.IfCmd(b.tok, b, ifStmtBuilder.Collect(b.tok), ifCmd, null);
+ }
+
private void CreateDispatchMethod(ITypeDefinition type)
{
Contract.Assert(type.IsDelegate);
- IMethodDefinition method = null;
+ IMethodDefinition invokeMethod = null;
foreach (IMethodDefinition m in type.Methods)
{
if (m.Name.Value == "Invoke")
{
- method = m;
+ invokeMethod = m;
break;
}
}
+ Bpl.IToken token = invokeMethod.Token();
Dictionary<IParameterDefinition, MethodParameter> formalMap = new Dictionary<IParameterDefinition, MethodParameter>();
this.sink.BeginMethod();
@@ -83,7 +95,7 @@ namespace BytecodeTranslator { int in_count = 0;
int out_count = 0;
MethodParameter mp;
- foreach (IParameterDefinition formal in method.Parameters)
+ foreach (IParameterDefinition formal in invokeMethod.Parameters)
{
mp = new MethodParameter(formal);
if (mp.inParameterCopy != null) in_count++;
@@ -94,13 +106,11 @@ namespace BytecodeTranslator { this.sink.FormalMap = formalMap;
#region Look for Returnvalue
- if (method.Type.TypeCode != PrimitiveTypeCode.Void)
+ if (invokeMethod.Type.TypeCode != PrimitiveTypeCode.Void)
{
- Bpl.Type rettype = TranslationHelper.CciTypeToBoogie(method.Type);
+ Bpl.Type rettype = TranslationHelper.CciTypeToBoogie(invokeMethod.Type);
out_count++;
- this.sink.RetVariable = new Bpl.Formal(method.Token(),
- new Bpl.TypedIdent(method.Token(),
- "$result", rettype), false);
+ this.sink.RetVariable = new Bpl.Formal(token, new Bpl.TypedIdent(token, "$result", rettype), false);
}
else
{
@@ -109,7 +119,7 @@ namespace BytecodeTranslator { #endregion
- in_count++; // for the function pointer parameter
+ in_count++; // for the delegate instance
Bpl.Variable[] invars = new Bpl.Formal[in_count];
Bpl.Variable[] outvars = new Bpl.Formal[out_count];
@@ -117,8 +127,7 @@ namespace BytecodeTranslator { int i = 0;
int j = 0;
- // Create function pointer parameter
- invars[i++] = new Bpl.Formal(method.Token(), new Bpl.TypedIdent(method.Token(), "this", Bpl.Type.Int), true);
+ invars[i++] = new Bpl.Formal(token, new Bpl.TypedIdent(token, "this", Bpl.Type.Int), true);
foreach (MethodParameter mparam in formalMap.Values)
{
@@ -139,10 +148,9 @@ namespace BytecodeTranslator { #endregion
- string MethodName = TranslationHelper.CreateUniqueMethodName(method);
-
- Bpl.Procedure proc = new Bpl.Procedure(method.Token(),
- MethodName, // make it unique!
+ string invokeMethodName = TranslationHelper.CreateUniqueMethodName(invokeMethod);
+ Bpl.Procedure proc = new Bpl.Procedure(token,
+ invokeMethodName, // make it unique!
new Bpl.TypeVariableSeq(),
new Bpl.VariableSeq(invars), // in
new Bpl.VariableSeq(outvars), // out
@@ -152,22 +160,26 @@ namespace BytecodeTranslator { this.sink.TranslatedProgram.TopLevelDeclarations.Add(proc);
- List<Bpl.Block> blocks = new List<Bpl.Block>();
- Bpl.StringSeq labelTargets = new Bpl.StringSeq();
- Bpl.BlockSeq blockTargets = new Bpl.BlockSeq();
- string l = "blocked";
- Bpl.Block b = new Bpl.Block(method.Token(), l,
- new Bpl.CmdSeq(new Bpl.AssumeCmd(method.Token(), Bpl.Expr.False)),
- new Bpl.ReturnCmd(method.Token()));
- labelTargets.Add(l);
- blockTargets.Add(b);
- blocks.Add(b);
- foreach (Bpl.Constant c in sink.delegateTypeToDelegates[type])
+ Bpl.LocalVariable method = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "method", Bpl.Type.Int));
+ Bpl.LocalVariable receiver = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "receiver", Bpl.Type.Int));
+ Bpl.LocalVariable iter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "iter", Bpl.Type.Int));
+ Bpl.LocalVariable niter = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "niter", Bpl.Type.Int));
+
+ Bpl.StmtListBuilder implStmtBuilder = new Bpl.StmtListBuilder();
+ implStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(iter), this.sink.ReadHead(Bpl.Expr.Ident(invars[0]))));
+
+ Bpl.StmtListBuilder whileStmtBuilder = new Bpl.StmtListBuilder();
+ whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(niter), this.sink.ReadNext(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(iter))));
+ whileStmtBuilder.Add(BuildBreakCmd(Bpl.Expr.Eq(Bpl.Expr.Ident(niter), this.sink.ReadHead(Bpl.Expr.Ident(invars[0])))));
+ whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(method), this.sink.ReadMethod(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(niter))));
+ whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(receiver), this.sink.ReadReceiver(Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(niter))));
+ Bpl.IfCmd ifCmd = BuildIfCmd(Bpl.Expr.True, new Bpl.AssumeCmd(token, Bpl.Expr.False), null);
+ foreach (IMethodDefinition defn in sink.delegateTypeToDelegates[type])
{
- Bpl.Expr bexpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(invars[0]), Bpl.Expr.Ident(c));
- Bpl.AssumeCmd assumeCmd = new Bpl.AssumeCmd(method.Token(), bexpr);
Bpl.ExprSeq ins = new Bpl.ExprSeq();
Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();
+ if (!defn.IsStatic)
+ ins.Add(Bpl.Expr.Ident(receiver));
int index;
for (index = 1; index < invars.Length; index++)
{
@@ -177,25 +189,25 @@ namespace BytecodeTranslator { {
outs.Add(Bpl.Expr.Ident(outvars[index]));
}
- Bpl.CallCmd callCmd = new Bpl.CallCmd(method.Token(), c.Name, ins, outs);
- l = "label_" + c.Name;
- b = new Bpl.Block(method.Token(), l, new Bpl.CmdSeq(assumeCmd, callCmd), new Bpl.ReturnCmd(method.Token()));
- labelTargets.Add(l);
- blockTargets.Add(b);
- blocks.Add(b);
+ Bpl.Constant c = sink.FindOrAddDelegateMethodConstant(defn);
+ Bpl.Expr bexpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, Bpl.Expr.Ident(method), Bpl.Expr.Ident(c));
+ Bpl.CallCmd callCmd = new Bpl.CallCmd(token, c.Name, ins, outs);
+ ifCmd = BuildIfCmd(bexpr, callCmd, ifCmd);
}
- Bpl.GotoCmd gotoCmd = new Bpl.GotoCmd(method.Token(), labelTargets, blockTargets);
- Bpl.Block initialBlock = new Bpl.Block(method.Token(), "start", new Bpl.CmdSeq(), gotoCmd);
- blocks.Insert(0, initialBlock);
+ whileStmtBuilder.Add(ifCmd);
+ whileStmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(iter), Bpl.Expr.Ident(niter)));
+ Bpl.WhileCmd whileCmd = new Bpl.WhileCmd(token, Bpl.Expr.True, new List<Bpl.PredicateCmd>(), whileStmtBuilder.Collect(token));
+
+ implStmtBuilder.Add(whileCmd);
Bpl.Implementation impl =
- new Bpl.Implementation(method.Token(),
- MethodName, // make unique
- new Microsoft.Boogie.TypeVariableSeq(),
- new Microsoft.Boogie.VariableSeq(invars),
- new Microsoft.Boogie.VariableSeq(outvars),
- new Bpl.VariableSeq(),
- blocks
+ new Bpl.Implementation(token,
+ invokeMethodName, // make unique
+ new Bpl.TypeVariableSeq(),
+ new Bpl.VariableSeq(invars),
+ new Bpl.VariableSeq(outvars),
+ new Bpl.VariableSeq(iter, niter, method, receiver),
+ implStmtBuilder.Collect(token)
);
impl.Proc = proc;
@@ -242,6 +254,9 @@ namespace BytecodeTranslator { ///
/// </summary>
public override void Visit(IMethodDefinition method) {
+ bool isEventAddOrRemove = method.IsSpecialName && (method.Name.Value.StartsWith("add_") || method.Name.Value.StartsWith("remove_"));
+ if (isEventAddOrRemove)
+ return;
this.sink.BeginMethod();
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 956cb71d..f95675f7 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -13,6 +13,7 @@ using Microsoft.Cci.MetadataReader; using Microsoft.Cci.MutableCodeModel;
using Microsoft.Cci.Contracts;
using Microsoft.Cci.ILToCodeModel;
+using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
@@ -35,10 +36,10 @@ namespace BytecodeTranslator { this.TranslatedProgram = new Bpl.Program();
}
- public IHeap Heap {
+ public Heap Heap {
get { return this.heap; }
}
- readonly IHeap heap;
+ readonly Heap heap;
public Bpl.Variable ArrayContentsVariable
{
@@ -59,6 +60,30 @@ namespace BytecodeTranslator { public readonly string StaticFieldFunction = "ClassRepr";
public readonly string ReferenceTypeName = "Ref";
+ public readonly string DelegateAddHelperName = "DelegateAddHelper";
+ public readonly string DelegateAddName = "DelegateAdd";
+ public readonly string DelegateRemoveName = "DelegateRemove";
+
+ public Bpl.Expr ReadHead(Bpl.Expr delegateReference)
+ {
+ return Bpl.Expr.Select(new Bpl.IdentifierExpr(delegateReference.tok, this.heap.DelegateHead), delegateReference);
+ }
+
+ public Bpl.Expr ReadNext(Bpl.Expr delegateReference, Bpl.Expr listNodeReference)
+ {
+ return Bpl.Expr.Select(Bpl.Expr.Select(new Bpl.IdentifierExpr(delegateReference.tok, this.heap.DelegateNext), delegateReference), listNodeReference);
+ }
+
+ public Bpl.Expr ReadMethod(Bpl.Expr delegateReference, Bpl.Expr listNodeReference)
+ {
+ return Bpl.Expr.Select(Bpl.Expr.Select(new Bpl.IdentifierExpr(delegateReference.tok, this.heap.DelegateMethod), delegateReference), listNodeReference);
+ }
+
+ public Bpl.Expr ReadReceiver(Bpl.Expr delegateReference, Bpl.Expr listNodeReference)
+ {
+ return Bpl.Expr.Select(Bpl.Expr.Select(new Bpl.IdentifierExpr(delegateReference.tok, this.heap.DelegateReceiver), delegateReference), listNodeReference);
+ }
+
public readonly Bpl.Program TranslatedProgram;
/// <summary>
@@ -127,7 +152,28 @@ namespace BytecodeTranslator { /// </summary>
private Dictionary<uint, Bpl.Variable> declaredFields = new Dictionary<uint, Bpl.Variable>();
- public Bpl.Procedure FindOrCreateProcedure(IMethodDefinition method, bool isStatic) {
+ public Bpl.Variable FindOrCreateEventVariable(IEventDefinition e)
+ {
+ Bpl.Variable v;
+ if (!this.declaredEvents.TryGetValue(e, out v))
+ {
+ v = this.Heap.CreateEventVariable(e);
+ this.declaredEvents.Add(e, v);
+ this.TranslatedProgram.TopLevelDeclarations.Add(v);
+ }
+ return v;
+ }
+
+ private Dictionary<IEventDefinition, Bpl.Variable> declaredEvents = new Dictionary<IEventDefinition, Bpl.Variable>();
+
+ public Bpl.Variable FindOrCreatePropertyVariable(IPropertyDefinition p)
+ {
+ return null;
+ }
+
+ private Dictionary<IPropertyDefinition, Bpl.Variable> declaredProperties = new Dictionary<IPropertyDefinition, Bpl.Variable>();
+
+ public Bpl.Procedure FindOrCreateProcedure(IMethodReference method, bool isStatic) {
Bpl.Procedure proc;
var key = method.InternedKey;
if (!this.declaredMethods.TryGetValue(key, out proc)) {
@@ -302,19 +348,32 @@ namespace BytecodeTranslator { this.FormalMap = new Dictionary<IParameterDefinition, MethodParameter>();
}
- public Dictionary<ITypeDefinition, HashSet<Bpl.Constant>> delegateTypeToDelegates =
- new Dictionary<ITypeDefinition, HashSet<Bpl.Constant>>();
+ public Dictionary<ITypeDefinition, HashSet<IMethodDefinition>> delegateTypeToDelegates = new Dictionary<ITypeDefinition, HashSet<IMethodDefinition>>();
- public void AddDelegate(ITypeDefinition type, Bpl.Constant constant)
+ public void AddDelegate(ITypeDefinition type, IMethodDefinition defn)
{
if (!delegateTypeToDelegates.ContainsKey(type))
- delegateTypeToDelegates[type] = new HashSet<Bpl.Constant>();
- delegateTypeToDelegates[type].Add(constant);
+ delegateTypeToDelegates[type] = new HashSet<IMethodDefinition>();
+ delegateTypeToDelegates[type].Add(defn);
}
public void AddDelegateType(ITypeDefinition type) {
if (!delegateTypeToDelegates.ContainsKey(type))
- delegateTypeToDelegates[type] = new HashSet<Bpl.Constant>();
+ delegateTypeToDelegates[type] = new HashSet<IMethodDefinition>();
+ }
+
+ private Dictionary<IMethodDefinition, Bpl.Constant> delegateMethods = new Dictionary<IMethodDefinition, Bpl.Constant>();
+
+ public Bpl.Constant FindOrAddDelegateMethodConstant(IMethodDefinition defn)
+ {
+ if (delegateMethods.ContainsKey(defn))
+ return delegateMethods[defn];
+ string methodName = TranslationHelper.CreateUniqueMethodName(defn);
+ var typedIdent = new Bpl.TypedIdent(Bpl.Token.NoToken, methodName, Bpl.Type.Int);
+ var constant = new Bpl.Constant(Bpl.Token.NoToken, typedIdent, true);
+ this.TranslatedProgram.TopLevelDeclarations.Add(constant);
+ delegateMethods[defn] = constant;
+ return constant;
}
}
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index 8667e1a0..04b95b37 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -68,6 +68,15 @@ namespace BytecodeTranslator { /// </summary>
static class TranslationHelper {
+ public static Bpl.AssignCmd BuildAssignCmd(Bpl.IdentifierExpr lhs, Bpl.Expr rhs)
+ {
+ List<Bpl.AssignLhs> lhss = new List<Bpl.AssignLhs>();
+ lhss.Add(new Bpl.SimpleAssignLhs(lhs.tok, lhs));
+ List<Bpl.Expr> rhss = new List<Bpl.Expr>();
+ rhss.Add(rhs);
+ return new Bpl.AssignCmd(lhs.tok, lhss, rhss);
+ }
+
public static Bpl.IToken Token(this IObjectWithLocations objectWithLocations) {
//TODO: use objectWithLocations.Locations!
Bpl.IToken tok = Bpl.Token.NoToken;
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index d200d8d8..a77683fe 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -31,6 +31,163 @@ implementation Alloc() returns (x: ref) +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;
+ }
+}
+
+
+
type Type;
type Field;
@@ -57,6 +214,14 @@ function {:inline true} Write(H: HeapType, o: ref, f: Field, v: box) : HeapType function $DynamicType(ref) : Type;
+var $Head: [int]int;
+
+var $Next: [int][int]int;
+
+var $Method: [int][int]int;
+
+var $Receiver: [int][int]int;
+
const unique RegressionTestInput.AsyncAttribute: Type;
procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 043ceccf..d0b573a6 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -29,6 +29,171 @@ implementation Alloc() returns (x: int) +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 $Head: [int]int;
+
+var $Next: [int][int]int;
+
+var $Method: [int][int]int;
+
+var $Receiver: [int][int]int;
+
procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt index 98d64ff9..918bf1f7 100644 --- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt @@ -29,6 +29,163 @@ implementation Alloc() returns (x: int) +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;
@@ -39,6 +196,14 @@ function Int2Box(int) : box; function Bool2Box(bool) : box;
+var $Head: [int]int;
+
+var $Next: [int][int]int;
+
+var $Method: [int][int]int;
+
+var $Receiver: [int][int]int;
+
procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt index 56e19305..1b0f35b8 100644 --- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt @@ -27,8 +27,173 @@ implementation Alloc() returns (x: int) +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);
+var $Head: [int]int;
+
+var $Next: [int][int]int;
+
+var $Method: [int][int]int;
+
+var $Receiver: [int][int]int;
+
procedure RegressionTestInput.AsyncAttribute.#ctor(this: int);
|