diff options
Diffstat (limited to 'BCT/BytecodeTranslator/HeapFactory.cs')
| -rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 582 |
1 files changed, 0 insertions, 582 deletions
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs deleted file mode 100644 index dd9aa62d..00000000 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ /dev/null @@ -1,582 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-
-using Microsoft.Cci;
-using Microsoft.Cci.MetadataReader;
-using Microsoft.Cci.MutableCodeModel;
-using Microsoft.Cci.Contracts;
-using Microsoft.Cci.ILToCodeModel;
-
-using Bpl = Microsoft.Boogie;
-
-namespace BytecodeTranslator {
-
- /// <summary>
- /// Implementations of this interface determine how the heap is represented in
- /// the translated Boogie program.
- /// </summary>
- public interface IHeap {
-
- /// <summary>
- /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
- /// on its type based on the heap representation.
- /// </summary>
- 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>
- Bpl.Variable CreateTypeVariable(ITypeReference type, List<Bpl.ConstantParent> parents);
-
- 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"/> (which should be non-null).
- /// </summary>
- /// <param name="o">The expression that represents the object to be dereferenced.
- /// </param>
- /// <param name="f">The field that is used to dereference the object <paramref name="o"/>.
- /// </param>
- Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.Expr f, AccessType accessType, Bpl.Type unboxType);
-
- /// <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"/> (which should be non-null).
- /// </summary>
- Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.Expr f, Bpl.Expr value, AccessType accessType, Bpl.Type boxType);
-
- /// <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>
- Bpl.Expr DynamicType(Bpl.Expr o);
-
- }
-
- public enum AccessType { Array, Heap, Struct };
-
- public abstract class Heap : HeapFactory, IHeap
- {
- [RepresentationFor("$ArrayContents", "var $ArrayContents: [Ref][int]Union;")]
- public Bpl.Variable ArrayContentsVariable = null;
- [RepresentationFor("$ArrayLength", "function $ArrayLength(Ref): int;")]
- public Bpl.Function ArrayLengthFunction = null;
-
- public abstract Bpl.Variable CreateFieldVariable(IFieldReference field);
-
- #region Boogie Types
-
- [RepresentationFor("Delegate", "type {:datatype} Delegate;")]
- public Bpl.TypeCtorDecl DelegateTypeDecl = null;
- public Bpl.CtorType DelegateType;
-
- [RepresentationFor("DelegateMultiset", "type DelegateMultiset = [Delegate]int;")]
- public Bpl.TypeSynonymDecl DelegateMultisetTypeDecl = null;
- public Bpl.TypeSynonymAnnotation DelegateMultisetType;
-
- [RepresentationFor("MultisetEmpty", "const unique MultisetEmpty: DelegateMultiset;")]
- public Bpl.Constant MultisetEmpty = null;
-
- [RepresentationFor("MultisetSingleton", "function {:inline true} MultisetSingleton(x: Delegate): DelegateMultiset { MultisetEmpty[x := 1] }")]
- public Bpl.Function MultisetSingleton = null;
-
- [RepresentationFor("MultisetPlus", "function {:inline true} MultisetPlus(x: DelegateMultiset, y: DelegateMultiset): DelegateMultiset { DelegateMapadd(x, y) }")]
- public Bpl.Function MultisetPlus = null;
-
- [RepresentationFor("MultisetMinus", "function {:inline true} MultisetMinus(x: DelegateMultiset, y: DelegateMultiset): DelegateMultiset { DelegateMapiteint(DelegateMapgt(x, y), DelegateMapsub(x, y), DelegateMapconstint(0)) }")]
- public Bpl.Function MultisetMinus = null;
-
- [RepresentationFor("Field", "type Field;")]
- public Bpl.TypeCtorDecl FieldTypeDecl = null;
- public Bpl.CtorType FieldType;
-
- [RepresentationFor("Union", "type Union;")]
- public Bpl.TypeCtorDecl UnionTypeDecl = null;
- public Bpl.CtorType UnionType;
-
- [RepresentationFor("$DefaultHeapValue", "const unique $DefaultHeapValue : Union;")]
- public Bpl.Constant DefaultHeapValue;
-
- [RepresentationFor("Ref", "type Ref;")]
- public Bpl.TypeCtorDecl RefTypeDecl = null;
- public Bpl.CtorType RefType;
- [RepresentationFor("null", "const unique null : Ref;")]
- public Bpl.Constant NullRef;
-
- [RepresentationFor("Type", "type {:datatype} Type;")]
- public Bpl.TypeCtorDecl TypeTypeDecl = null;
- public Bpl.CtorType TypeType;
-
- [RepresentationFor("Real", "type Real;")]
- protected Bpl.TypeCtorDecl RealTypeDecl = null;
- public Bpl.CtorType RealType;
- [RepresentationFor("$DefaultReal", "const unique $DefaultReal : Real;")]
- public Bpl.Constant DefaultReal;
-
- #endregion
-
- #region CLR Boxing
-
- [RepresentationFor("$BoxFromBool", "procedure {:inline 1} $BoxFromBool(b: bool) returns (r: Ref) { call r := Alloc(); assume $BoxedValue(r) == Bool2Union(b); }")]
- public Bpl.Procedure BoxFromBool = null;
-
- [RepresentationFor("$BoxFromInt", "procedure {:inline 1} $BoxFromInt(i: int) returns (r: Ref) { call r := Alloc(); assume $BoxedValue(r) == Int2Union(i); }")]
- public Bpl.Procedure BoxFromInt = null;
-
- [RepresentationFor("$BoxFromReal", "procedure {:inline 1} $BoxFromReal(r: Real) returns (rf: Ref) { call rf := Alloc(); assume $BoxedValue(rf) == Real2Union(r); }")]
- public Bpl.Procedure BoxFromReal = null;
-
- [RepresentationFor("$BoxFromStruct", "procedure {:inline 1} $BoxFromStruct(s: Ref) returns (r: Ref) { call r := Alloc(); assume $BoxedValue(r) == Struct2Union(s); }")]
- public Bpl.Procedure BoxFromStruct = null;
-
- [RepresentationFor("$BoxFromUnion", "procedure {:inline 1} $BoxFromUnion(u: Union) returns (r: Ref) { if (IsRef(u)) { r := Union2Ref(u); } else { call r := Alloc(); assume $BoxedValue(r) == u; } }")]
- public Bpl.Procedure BoxFromUnion = null;
-
- [RepresentationFor("$BoxedValue", "function $BoxedValue(r: Ref): Union;")]
- public Bpl.Function BoxedValue = null;
-
- [RepresentationFor("$Unbox2Bool", "function {:inline true} $Unbox2Bool(r: Ref): (bool) { Union2Bool($BoxedValue(r)) }")]
- public Bpl.Function Unbox2Bool = null;
-
- [RepresentationFor("$Unbox2Int", "function {:inline true} $Unbox2Int(r: Ref): (int) { Union2Int($BoxedValue(r)) }")]
- public Bpl.Function Unbox2Int = null;
-
- [RepresentationFor("$Unbox2Real", "function {:inline true} $Unbox2Real(r: Ref): (Real) { Union2Real($BoxedValue(r)) }")]
- public Bpl.Function Unbox2Real = null;
-
- [RepresentationFor("$Unbox2Struct", "function {:inline true} $Unbox2Struct(r: Ref): (Ref) { Union2Struct($BoxedValue(r)) }")]
- public Bpl.Function Unbox2Struct = null;
-
- [RepresentationFor("$Unbox2Union", "function {:inline true} $Unbox2Union(r: Ref): (Union) { $BoxedValue(r) }")]
- public Bpl.Function Unbox2Union = null;
-
- #endregion
-
- #region Conversions
-
- #region Heap values
-
- [RepresentationFor("Union2Bool", "function Union2Bool(u: Union): (bool);")]
- public Bpl.Function Union2Bool = null;
-
- [RepresentationFor("Union2Int", "function Union2Int(u: Union): (int);")]
- public Bpl.Function Union2Int = null;
-
- [RepresentationFor("Union2Ref", "function Union2Ref(u: Union): (Ref);")]
- public Bpl.Function Union2Ref = null;
-
- [RepresentationFor("Union2Real", "function Union2Real(u: Union): (Real);")]
- public Bpl.Function Union2Real = null;
-
- [RepresentationFor("Union2Struct", "function Union2Struct(u: Union): (Ref);")]
- public Bpl.Function Union2Struct = null;
-
- [RepresentationFor("Bool2Union", "function Bool2Union(boolValue: bool): Union;")]
- public Bpl.Function Bool2Union = null;
-
- [RepresentationFor("Int2Union", "function Int2Union(intValue: int): Union;")]
- public Bpl.Function Int2Union = null;
-
- [RepresentationFor("Ref2Union", "function Ref2Union(refValue: Ref): Union;")]
- public Bpl.Function Ref2Union = null;
-
- [RepresentationFor("Real2Union", "function Real2Union(realValue: Real): Union;")]
- public Bpl.Function Real2Union = null;
-
- [RepresentationFor("Struct2Union", "function Struct2Union(structValue: Ref): Union;")]
- public Bpl.Function Struct2Union = null;
-
- [RepresentationFor("Union2Union", "function {:inline true} Union2Union(u: Union): Union { u }")]
- public Bpl.Function Union2Union = null;
-
- public Bpl.Expr ToUnion(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {
- Bpl.Function conversion;
- if (boogieType == Bpl.Type.Bool)
- conversion = this.Bool2Union;
- else if (boogieType == Bpl.Type.Int)
- conversion = this.Int2Union;
- else if (boogieType == RefType)
- conversion = this.Ref2Union;
- else if (boogieType == RealType)
- conversion = this.Real2Union;
- else if (boogieType == UnionType)
- conversion = this.Union2Union;
- else
- throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));
-
- var callConversion = new Bpl.NAryExpr(
- tok,
- new Bpl.FunctionCall(conversion),
- new Bpl.ExprSeq(expr)
- );
- return callConversion;
- }
-
- public Bpl.Expr FromUnion(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {
- Bpl.Function conversion = null;
- if (boogieType == Bpl.Type.Bool)
- conversion = this.Union2Bool;
- else if (boogieType == Bpl.Type.Int)
- conversion = this.Union2Int;
- else if (boogieType == RefType)
- conversion = this.Union2Ref;
- else if (boogieType == RealType)
- conversion = this.Union2Real;
- else if (boogieType == UnionType)
- conversion = this.Union2Union;
- else
- throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));
-
- var callExpr = new Bpl.NAryExpr(
- tok,
- new Bpl.FunctionCall(conversion),
- new Bpl.ExprSeq(expr)
- );
- callExpr.Type = boogieType;
- return callExpr;
- }
-
- #endregion
-
- #region Real number conversions
- [RepresentationFor("Int2Real", "function Int2Real(int): Real;")]
- public Bpl.Function Int2Real = null;
- [RepresentationFor("Real2Int", "function Real2Int(Real): int;")]
- public Bpl.Function Real2Int = null;
- #endregion
-
- #region Real number operations
- [RepresentationFor("RealPlus", "function RealPlus(Real, Real): Real;")]
- public Bpl.Function RealPlus = null;
- [RepresentationFor("RealMinus", "function RealMinus(Real, Real): Real;")]
- public Bpl.Function RealMinus = null;
- [RepresentationFor("RealTimes", "function RealTimes(Real, Real): Real;")]
- public Bpl.Function RealTimes = null;
- [RepresentationFor("RealDivide", "function RealDivide(Real, Real): Real;")]
- public Bpl.Function RealDivide = null;
- [RepresentationFor("RealModulus", "function RealModulus(Real, Real): Real;")]
- public Bpl.Function RealModulus = null;
- [RepresentationFor("RealLessThan", "function RealLessThan(Real, Real): bool;")]
- public Bpl.Function RealLessThan = null;
- [RepresentationFor("RealLessThanOrEqual", "function RealLessThanOrEqual(Real, Real): bool;")]
- public Bpl.Function RealLessThanOrEqual = null;
- [RepresentationFor("RealGreaterThan", "function RealGreaterThan(Real, Real): bool;")]
- public Bpl.Function RealGreaterThan = null;
- [RepresentationFor("RealGreaterThanOrEqual", "function RealGreaterThanOrEqual(Real, Real): bool;")]
- public Bpl.Function RealGreaterThanOrEqual = null;
- #endregion
-
- #region Bitwise operations
- [RepresentationFor("BitwiseAnd", "function BitwiseAnd(int, int): int;")]
- public Bpl.Function BitwiseAnd = null;
- [RepresentationFor("BitwiseOr", "function BitwiseOr(int, int): int;")]
- public Bpl.Function BitwiseOr = null;
- [RepresentationFor("BitwiseExclusiveOr", "function BitwiseExclusiveOr(int, int): int;")]
- public Bpl.Function BitwiseExclusiveOr = null;
- [RepresentationFor("BitwiseNegation", "function BitwiseNegation(int): int;")]
- public Bpl.Function BitwiseNegation = null;
- [RepresentationFor("RightShift", "function RightShift(int,int): int;")]
- public Bpl.Function RightShift = null;
- [RepresentationFor("LeftShift", "function LeftShift(int,int): int;")]
- public Bpl.Function LeftShift = null;
- #endregion
-
- #endregion
-
- /// <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, List<Bpl.ConstantParent> parents)
- {
- string typename = TypeHelper.GetTypeName(type, NameFormattingOptions.DocumentationId);
- typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
- Bpl.IToken tok = type.Token();
- Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, typename, this.TypeType);
- Bpl.Constant v = new Bpl.Constant(tok, tident, true /*unique*/, parents, false, null);
- return v;
- }
-
- public Bpl.Function CreateTypeFunction(ITypeReference type, int parameterCount) {
- System.Diagnostics.Debug.Assert(parameterCount >= 0);
- string typename = TypeHelper.GetTypeName(type, NameFormattingOptions.DocumentationId);
- typename = TranslationHelper.TurnStringIntoValidIdentifier(typename);
- Bpl.IToken tok = type.Token();
- Bpl.VariableSeq inputs = new Bpl.VariableSeq();
- //for (int i = 0; i < parameterCount; i++) {
- // inputs.Add(new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "arg"+i, this.TypeType), true));
- //}
- foreach (var t in TranslationHelper.ConsolidatedGenericParameters(type)) {
- var n = t.Name.Value;
- var n2 = TranslationHelper.TurnStringIntoValidIdentifier(n);
- inputs.Add(new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, n2, this.TypeType), true));
- }
- Bpl.Variable output = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "result", this.TypeType), false);
- Bpl.Function func = new Bpl.Function(tok, typename, inputs, output);
- var attrib = new Bpl.QKeyValue(Bpl.Token.NoToken, "constructor", new List<object>(1), null);
- func.Attributes = attrib;
- return func;
- }
-
-
- public abstract Bpl.Variable CreateEventVariable(IEventDefinition e);
-
- public abstract Bpl.Expr ReadHeap(Bpl.Expr o, Bpl.Expr f, AccessType accessType, Bpl.Type unboxType);
-
- public abstract Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr o, Bpl.Expr f, Bpl.Expr value, AccessType accessType, Bpl.Type boxType);
-
- [RepresentationFor("$DynamicType", "function $DynamicType(Ref): Type;")]
- protected Bpl.Function DynamicTypeFunction = 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 Bpl.Expr DynamicType(Bpl.Expr o) {
- // $DymamicType(o)
- var callDynamicType = new Bpl.NAryExpr(
- o.tok,
- new Bpl.FunctionCall(this.DynamicTypeFunction),
- new Bpl.ExprSeq(o)
- );
- return callDynamicType;
- }
-
- [RepresentationFor("$TypeOf", "function $TypeOf(Type): Ref;")]
- public Bpl.Function TypeOfFunction = null;
-
- [RepresentationFor("$As", "function $As(Ref, Type): Ref;")]
- public Bpl.Function AsFunction = null;
-
- [RepresentationFor("$Subtype", "function $Subtype(Type, Type): bool;")]
- public Bpl.Function Subtype = null;
-
- [RepresentationFor("$DisjointSubtree", "function $DisjointSubtree(Type, Type): bool;")]
- public Bpl.Function DisjointSubtree = null;
-
- [RepresentationFor("$Alloc", "var $Alloc: [Ref] bool;")]
- public Bpl.Variable AllocVariable = null;
-
- [RepresentationFor("$allocImp", "function {:builtin \"MapImp\"} $allocImp([Ref]bool, [Ref]bool) : [Ref]bool;")]
- public Bpl.Function AllocImplies = null;
- [RepresentationFor("$allocConstBool", "function {:builtin \"MapConst\"} $allocConstBool(bool) : [Ref]bool;")]
- public Bpl.Function AllocConstBool = null;
-
-
-
- protected readonly string CommonText =
- @"//var $Alloc: [Ref] bool;
-
-procedure {:inline 1} Alloc() returns (x: Ref)
- modifies $Alloc;
-{
- assume $Alloc[x] == false && x != null;
- $Alloc[x] := true;
-}
-
-function {:builtin ""MapAdd""} DelegateMapadd([Delegate]int, [Delegate]int) : [Delegate]int;
-function {:builtin ""MapSub""} DelegateMapsub([Delegate]int, [Delegate]int) : [Delegate]int;
-function {:builtin ""MapMul""} DelegateMapmul([Delegate]int, [Delegate]int) : [Delegate]int;
-function {:builtin ""MapDiv""} DelegateMapdiv([Delegate]int, [Delegate]int) : [Delegate]int;
-function {:builtin ""MapMod""} DelegateMapmod([Delegate]int, [Delegate]int) : [Delegate]int;
-function {:builtin ""MapConst""} DelegateMapconstint(int) : [Delegate]int;
-function {:builtin ""MapConst""} DelegateMapconstbool(bool) : [Delegate]bool;
-function {:builtin ""MapAnd""} DelegateMapand([Delegate]bool, [Delegate]bool) : [Delegate]bool;
-function {:builtin ""MapOr""} DelegateMapor([Delegate]bool, [Delegate]bool) : [Delegate]bool;
-function {:builtin ""MapNot""} DelegateMapnot([Delegate]bool) : [Delegate]bool;
-function {:builtin ""MapIte""} DelegateMapiteint([Delegate]bool, [Delegate]int, [Delegate]int) : [Delegate]int;
-function {:builtin ""MapIte""} DelegateMapitebool([Delegate]bool, [Delegate]bool, [Delegate]bool) : [Delegate]bool;
-function {:builtin ""MapLe""} DelegateMaple([Delegate]int, [Delegate]int) : [Delegate]bool;
-function {:builtin ""MapLt""} DelegateMaplt([Delegate]int, [Delegate]int) : [Delegate]bool;
-function {:builtin ""MapGe""} DelegateMapge([Delegate]int, [Delegate]int) : [Delegate]bool;
-function {:builtin ""MapGt""} DelegateMapgt([Delegate]int, [Delegate]int) : [Delegate]bool;
-function {:builtin ""MapEq""} DelegateMapeq([Delegate]int, [Delegate]int) : [Delegate]bool;
-function {:builtin ""MapIff""} DelegateMapiff([Delegate]bool, [Delegate]bool) : [Delegate]bool;
-function {:builtin ""MapImp""} DelegateMapimp([Delegate]bool, [Delegate]bool) : [Delegate]bool;
-axiom MultisetEmpty == DelegateMapconstint(0);
-
-function IsRef(u: Union) : (bool);
-axiom (forall x: bool :: {Bool2Union(x)} Union2Bool(Bool2Union(x)) == x && !IsRef(Bool2Union(x)));
-axiom (forall x: int :: {Int2Union(x)} Union2Int(Int2Union(x)) == x && !IsRef(Int2Union(x)));
-axiom (forall x: Real :: {Real2Union(x)} Union2Real(Real2Union(x)) == x && !IsRef(Real2Union(x)));
-axiom (forall x: Ref :: {Ref2Union(x)} Union2Ref(Ref2Union(x)) == x && IsRef(Ref2Union(x)));
-axiom (forall x: Ref :: {Struct2Union(x)} Union2Struct(Struct2Union(x)) == x && !IsRef(Struct2Union(x)));
-
-
-/*
-// Subtype is reflexive
-axiom (forall t: Type :: $Subtype(t, t) );
-
-// Subtype is anti-symmetric
-axiom (forall t0 : Type, t1 : Type :: { $Subtype(t0, t1), $Subtype(t1, t0) }
- $Subtype(t0, t1) && $Subtype(t1, t0) ==> (t0 == t1) );
-
-// Subtype is transitive
-axiom (forall t0 : Type, t1 : Type, t2 : Type :: { $Subtype(t0, t1), $Subtype(t1, t2) }
- $Subtype(t0, t1) && $Subtype(t1, t2) ==> $Subtype(t0, t2) );
-
-// Incomparable subtypes: the subtrees are disjoint for (some) subtypes (those that imply single inheritance)
-function oneDown(t0 : Type, t1 : Type) : Type; // uninterpreted function with no axioms
-axiom (forall C : Type, D : Type :: { $DisjointSubtree(D, C) }
- $DisjointSubtree(D, C) <==> (forall z : Type :: $Subtype(z, D) ==> oneDown(C,z) == D) );
-*/
-
-function $TypeOfInv(Ref): Type;
-axiom (forall t: Type :: {$TypeOf(t)} $TypeOfInv($TypeOf(t)) == t);
-
-procedure {:inline 1} System.Object.GetType(this: Ref) returns ($result: Ref)
-{
- $result := $TypeOf($DynamicType(this));
-}
-
-axiom Union2Int($DefaultHeapValue) == 0;
-axiom Union2Bool($DefaultHeapValue) == false;
-axiom Union2Ref($DefaultHeapValue) == null;
-
-function $ThreadDelegate(Ref) : Ref;
-
-procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ParameterizedThreadStart(this: Ref, start$in: Ref)
-{
- assume $ThreadDelegate(this) == start$in;
-}
-procedure {:inline 1} System.Threading.Thread.Start$System.Object(this: Ref, parameter$in: Ref)
-{
- call {:async} Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object($ThreadDelegate(this), parameter$in);
-}
-procedure Wrapper_System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref) {
- $Exception := null;
- call System.Threading.ParameterizedThreadStart.Invoke$System.Object(this, obj$in);
-}
-procedure {:extern} System.Threading.ParameterizedThreadStart.Invoke$System.Object(this: Ref, obj$in: Ref);
-
-procedure {:inline 1} System.Threading.Thread.#ctor$System.Threading.ThreadStart(this: Ref, start$in: Ref)
-{
- assume $ThreadDelegate(this) == start$in;
-}
-procedure {:inline 1} System.Threading.Thread.Start(this: Ref)
-{
- call {:async} Wrapper_System.Threading.ThreadStart.Invoke($ThreadDelegate(this));
-}
-procedure Wrapper_System.Threading.ThreadStart.Invoke(this: Ref) {
- $Exception := null;
- call System.Threading.ThreadStart.Invoke(this);
-}
-procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
-
-procedure {:inline 1} DelegateAdd(a: Ref, b: Ref) returns (c: Ref)
-{
- var d: Delegate;
-
- if (a == null)
- {
- c := b;
- }
- else if (b == null)
- {
- c := a;
- }
- else
- {
- call c := Alloc();
- assume $RefToDelegate(c) == $RefToDelegate(a) || $RefToDelegate(c) == $RefToDelegate(b);
- assume $RefToDelegateMultiset(c) == MultisetPlus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b));
- }
-}
-
-procedure {:inline 1} DelegateRemove(a: Ref, b: Ref) returns (c: Ref)
-{
- var d: Delegate;
-
- if (a == null)
- {
- c := null;
- }
- else if (b == null)
- {
- c := a;
- }
- else if (MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b)) == MultisetEmpty)
- {
- c := null;
- }
- else
- {
- call c := Alloc();
- assume $RefToDelegateMultiset(c) == MultisetMinus($RefToDelegateMultiset(a), $RefToDelegateMultiset(b));
- assume $RefToDelegateMultiset(c)[$RefToDelegate(c)] > 0;
- }
-}
-
-procedure {:inline 1} DelegateCreate(d: Delegate) returns (c: Ref)
-{
- call c := Alloc();
- assume $RefToDelegate(c) == d;
- assume $RefToDelegateMultiset(c) == MultisetSingleton(d);
-}
-
-procedure {:inline 1} System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);
-procedure {:inline 1} System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool);
-
-implementation System.String.op_Equality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) {
- $result := (a$in == b$in);
-}
-
-implementation System.String.op_Inequality$System.String$System.String(a$in: Ref, b$in: Ref) returns ($result: bool) {
- $result := (a$in != b$in);
-}
-
-";
-
- [RepresentationFor("$RefToDelegate", "function $RefToDelegate(Ref): Delegate;")]
- public Bpl.Function RefToDelegate = null;
-
- [RepresentationFor("$RefToDelegateMultiset", "function $RefToDelegateMultiset(Ref): DelegateMultiset;")]
- public Bpl.Function RefToDelegateMultiset = null;
-
- [RepresentationFor("$RefToDelegateMultisetCons", "function {:constructor} $RefToDelegateMultisetCons($Method: int, $Receiver: Ref, $TypeParameters: Type): Delegate;")]
- public Bpl.DatatypeConstructor DelegateCons = null;
-
- public Bpl.Function DelegateMethod {
- get { return DelegateCons.selectors[0]; }
- }
-
- public Bpl.Function DelegateReceiver {
- get { return DelegateCons.selectors[1]; }
- }
-
- public Bpl.Function DelegateTypeParameters {
- get { return DelegateCons.selectors[2]; }
- }
-
- [RepresentationFor("$Exception", "var {:thread_local} $Exception: Ref;")]
- public Bpl.GlobalVariable ExceptionVariable = null;
- }
-
- public abstract class HeapFactory {
-
- /// <summary>
- /// Returns two things: an object that determines the heap representation,
- /// and (optionally) an initial program that contains declarations needed
- /// for the heap representation.
- /// </summary>
- /// <param name="sink">
- /// The heap might need to generate declarations so it needs access to the Sink.
- /// </param>
- /// <returns>
- /// 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 Heap heap, out Bpl.Program/*?*/ program);
- }
-
-}
\ No newline at end of file |