diff options
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 18 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 6 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 21 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 48 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 15 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/WholeProgram.cs | 18 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt | 10 | ||||
| -rw-r--r-- | BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt | 10 | ||||
| -rw-r--r-- | Test/datatypes/t2.bpl | 8 |
9 files changed, 104 insertions, 50 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index dbcc8dad..8e5170b2 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -286,13 +286,23 @@ namespace BytecodeTranslator }
/// <summary>
- /// If the expression is a struct, then this returns a "boxed" struct.
+ /// If the expression's type is a generic parameter (either method or type),
+ /// then this returns a "unboxed" expression, i.e., the value as a ref.
/// Otherwise it just translates the expression and skips the address-of
/// operation.
/// </summary>
public override void TraverseChildren(IAddressOf addressOf)
{
- this.Traverse(addressOf.Expression);
+ var t = addressOf.Expression.Type;
+ if (t is IGenericParameterReference) {
+ // then the expression will be represented by something of type Box
+ // but the address of it must be a ref, so do the conversion
+ this.Traverse(addressOf.Expression);
+ var e = this.TranslatedExpressions.Pop();
+ this.TranslatedExpressions.Push(this.sink.Heap.Unbox(addressOf.Token(), this.sink.Heap.RefType, e));
+ } else {
+ this.Traverse(addressOf.Expression);
+ }
}
#endregion
@@ -646,10 +656,12 @@ namespace BytecodeTranslator var e = this.TranslatedExpressions.Pop();
var identifierExpr = e as Bpl.IdentifierExpr;
if (identifierExpr == null) {
- var newLocal = Bpl.Expr.Ident(this.sink.CreateFreshLocal(thisArg.Type));
+ var newLocal = Bpl.Expr.Ident(this.sink.CreateFreshLocal(methodToCall.ContainingType));
var cmd = Bpl.Cmd.SimpleAssign(token, newLocal, e);
this.StmtTraverser.StmtBuilder.Add(cmd);
e = newLocal;
+ } else {
+
}
inexpr.Add(e);
thisExpr = (Bpl.IdentifierExpr) e;
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index 45adb36e..f5f0bf61 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -275,8 +275,10 @@ namespace BytecodeTranslator { //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 type.ResolvedType.GenericParameters) {
- inputs.Add(new Bpl.Formal(Bpl.Token.NoToken, new Bpl.TypedIdent(Bpl.Token.NoToken, t.Name.Value, 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);
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index f9b0023d..4702d5a0 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -211,7 +211,7 @@ namespace BytecodeTranslator { }
module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;
// The decompiler does not turn calls to Assert/Assume into Code Model nodes
- module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Visit(module);
+ module = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(module);
host.RegisterAsLatest(module);
modules.Add(module);
@@ -632,11 +632,20 @@ namespace BytecodeTranslator { for (int i = 0; i < tempInputs.Count; i++) {
ins.Add(Bpl.Expr.Ident(tempInputs[i]));
}
- int numTypeParameters = Sink.GetNumberTypeParameters(defn);
- for (int i = 0; i < numTypeParameters; i++) {
- ins.Add(new Bpl.NAryExpr(Bpl.Token.NoToken,
- new Bpl.FunctionCall(sink.FindOrCreateTypeParameterFunction(i)),
- new Bpl.ExprSeq(Bpl.Expr.Ident(typeParameter))));
+ if (defn.IsGeneric) {
+ for (int i = 0; i < defn.GenericParameterCount; i++) {
+ ins.Add(new Bpl.NAryExpr(Bpl.Token.NoToken,
+ new Bpl.FunctionCall(sink.FindOrCreateTypeParameterFunction(i)),
+ new Bpl.ExprSeq(Bpl.Expr.Ident(typeParameter))));
+ }
+ }
+ if (defn.IsStatic) {
+ int numTypeParameters = Sink.ConsolidatedGenericParameterCount(defn.ContainingType);
+ for (int i = 0; i < numTypeParameters; i++) {
+ ins.Add(new Bpl.NAryExpr(Bpl.Token.NoToken,
+ new Bpl.FunctionCall(sink.FindOrCreateTypeParameterFunction(i)),
+ new Bpl.ExprSeq(Bpl.Expr.Ident(typeParameter))));
+ }
}
for (int i = 0; i < tempOutputs.Count; i++) {
outs.Add(Bpl.Expr.Ident(tempOutputs[i]));
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index d20671b2..50051b0c 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -820,7 +820,7 @@ namespace BytecodeTranslator { return result;
}
- private static ushort ConsolidatedGenericParameterCount(ITypeReference typeReference) {
+ public static ushort ConsolidatedGenericParameterCount(ITypeReference typeReference) {
Contract.Requires(typeReference != null);
var typeDefinition = typeReference.ResolvedType;
@@ -857,15 +857,9 @@ namespace BytecodeTranslator { if (nestedTypeReference != null) GetConsolidatedTypeArguments(consolidatedTypeArguments, nestedTypeReference.ContainingType);
}
+ [Obsolete]
public static int GetNumberTypeParameters(IMethodDefinition method) {
- int count = 0;
- if (method.IsStatic) {
- List<ITypeReference> consolidatedTypeArguments = new List<ITypeReference>();
- Sink.GetConsolidatedTypeArguments(consolidatedTypeArguments, method.ContainingType);
- count += consolidatedTypeArguments.Count;
- }
- count += method.GenericParameterCount;
- return count;
+ return method.GenericParameterCount + ConsolidatedGenericParameterCount(method.ContainingType);
}
/// <summary>
@@ -888,14 +882,18 @@ namespace BytecodeTranslator { IGenericTypeParameter gtp = type as IGenericTypeParameter;
if (gtp != null) {
- Bpl.Variable v;
- if (!this.declaredTypeVariables.TryGetValue(gtp.InternedKey, out v)) {
- var loc = Bpl.Token.NoToken;
- var t = CciTypeToBoogie(gtp);
- v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, gtp.Name.Value, t));
- this.declaredTypeVariables.Add(gtp.InternedKey, v);
- }
- return Bpl.Expr.Ident(v);
+ var selectorName = gtp.Name.Value;
+ selectorName = TranslationHelper.TurnStringIntoValidIdentifier(selectorName);
+ var typeName = TypeHelper.GetTypeName(gtp.DefiningType, NameFormattingOptions.DocumentationId);
+ typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);
+ var funcName = String.Format("{0}#{1}", selectorName, typeName);
+ Bpl.IToken tok = Bpl.Token.NoToken;
+ var identExpr = Bpl.Expr.Ident(new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, funcName, this.Heap.TypeType)));
+ var funcCall = new Bpl.FunctionCall(identExpr);
+ var thisArg = new Bpl.IdentifierExpr(tok, this.ThisVariable);
+ var dynType = this.Heap.DynamicType(thisArg);
+ var nary = new Bpl.NAryExpr(Bpl.Token.NoToken, funcCall, new Bpl.ExprSeq(dynType));
+ return nary;
}
IGenericMethodParameter gmp = type as IGenericMethodParameter;
@@ -931,7 +929,7 @@ namespace BytecodeTranslator { /// The Heap has to decide how to represent the type.
/// All the Sink cares about is adding a declaration for it.
/// </summary>
- private Bpl.Function FindOrDefineType(ITypeReference type) {
+ public Bpl.Function FindOrDefineType(ITypeReference type) {
Bpl.Function f;
@@ -968,26 +966,31 @@ namespace BytecodeTranslator { return;
}
private void DeclareSuperType(Bpl.Function typeDefinitionAsBplFunction, ITypeReference superType) {
- var superType_prime = FindOrCreateTypeReference(superType);
+ var superTypeFunction = FindOrDefineType(superType);
var numberOfGenericParameters = typeDefinitionAsBplFunction.InParams.Length;
var qvars = new Bpl.VariableSeq();
var exprs = new Bpl.ExprSeq();
+ var superTypeArgs = new Bpl.ExprSeq();
for (int i = 0; i < numberOfGenericParameters; i++) {
var t = typeDefinitionAsBplFunction.InParams[i];
qvars.Add(t);
- exprs.Add(Bpl.Expr.Ident(t));
+ var identForT = Bpl.Expr.Ident(t);
+ exprs.Add(identForT);
+ if (i < superTypeFunction.InParams.Length)
+ superTypeArgs.Add(identForT);
}
// G(t,u)
var callToG = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(typeDefinitionAsBplFunction), exprs);
+ var callToSuperType = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(superTypeFunction), superTypeArgs);
// Subtype(G(t,u), super)
- Bpl.Expr subtype = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(callToG, superType_prime));
+ Bpl.Expr subtype = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.Subtype), new Bpl.ExprSeq(callToG, callToSuperType));
Bpl.Expr disjointSubtree = null;
var isDisjoint = !superType.ResolvedType.IsInterface;
if (isDisjoint) {
// DisjointSubtree(G(t,u), super)
- disjointSubtree = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.DisjointSubtree), new Bpl.ExprSeq(callToG, superType_prime));
+ disjointSubtree = new Bpl.NAryExpr(Bpl.Token.NoToken, new Bpl.FunctionCall(this.Heap.DisjointSubtree), new Bpl.ExprSeq(callToG, callToSuperType));
}
if (0 < numberOfGenericParameters) {
@@ -1037,7 +1040,6 @@ namespace BytecodeTranslator { /// <summary>
/// The keys to the table are the interned key of the type.
/// </summary>
- private Dictionary<uint, Bpl.Variable> declaredTypeVariables = new Dictionary<uint, Bpl.Variable>();
private Dictionary<uint, Bpl.Function> declaredTypeFunctions = new Dictionary<uint, Bpl.Function>();
private List<Bpl.Function> childFunctions = new List<Bpl.Function>();
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index a744f405..98610297 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -16,6 +16,7 @@ using Microsoft.Cci.ILToCodeModel; using Bpl = Microsoft.Boogie;
using System.Text.RegularExpressions;
+using System.Diagnostics.Contracts;
namespace BytecodeTranslator {
@@ -121,6 +122,20 @@ namespace BytecodeTranslator { return "finally" + (finallyClauseCounter++).ToString();
}
+ public static List<IGenericTypeParameter> ConsolidatedGenericParameters(ITypeReference typeReference) {
+ Contract.Requires(typeReference != null);
+
+ var typeDefinition = typeReference.ResolvedType;
+ var totalParameters = new List<IGenericTypeParameter>(typeDefinition.GenericParameters);
+ var nestedTypeDefinition = typeDefinition as INestedTypeDefinition;
+ while (nestedTypeDefinition != null) {
+ var containingType = nestedTypeDefinition.ContainingType.ResolvedType;
+ totalParameters.AddRange(containingType.GenericParameters);
+ nestedTypeDefinition = containingType as INestedTypeDefinition;
+ }
+ return totalParameters;
+ }
+
public static string CreateUniqueMethodName(IMethodReference method) {
var containingTypeName = TypeHelper.GetTypeName(method.ContainingType, NameFormattingOptions.None);
var s = MemberHelper.GetMethodSignature(method, NameFormattingOptions.DocumentationId);
diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs index d90176a8..e1d2d73a 100644 --- a/BCT/BytecodeTranslator/WholeProgram.cs +++ b/BCT/BytecodeTranslator/WholeProgram.cs @@ -163,11 +163,19 @@ namespace BytecodeTranslator { foreach (var typeMethodPair in overrides) {
var t = typeMethodPair.Item1;
var m = typeMethodPair.Item2;
- var typeForT = this.sink.FindOrCreateTypeReference(t);
- if (typeForT == null) {
+
+ // guard: is#T($DynamicType(local_variable))
+ var typeFunction = this.sink.FindOrDefineType(t);
+ if (typeFunction == null) {
// BUGBUG!! This just silently skips the branch that would dispatch to t's implementation of the method!
continue;
}
+ var funcName = String.Format("is#{0}", typeFunction.Name);
+ var identExpr = Bpl.Expr.Ident(new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, funcName, Bpl.Type.Bool)));
+ var funcCall = new Bpl.FunctionCall(identExpr);
+ var exprs = new Bpl.ExprSeq(this.sink.Heap.DynamicType(inexpr[0]));
+ var guard = new Bpl.NAryExpr(token, funcCall, exprs);
+
var thenBranch = new Bpl.StmtListBuilder();
methodname = TranslationHelper.CreateUniqueMethodName(m); // REVIEW: Shouldn't this be call to FindOrCreateProcedure?
if (attrib != null)
@@ -175,11 +183,9 @@ namespace BytecodeTranslator { else
call = new Bpl.CallCmd(token, methodname, inexpr, outvars);
thenBranch.Add(call);
+
ifcmd = new Bpl.IfCmd(token,
- Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq,
- this.sink.Heap.DynamicType(inexpr[0]),
- typeForT
- ),
+ guard,
thenBranch.Collect(token),
null,
elseBranch.Collect(token)
diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 155db7c9..3284f217 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -431,7 +431,7 @@ var {:thread_local} $Exception: Ref; function {:constructor} T$RegressionTestInput.RealNumbers() : Type;
-function {:extern} T$System.Object() : Type;
+function {:constructor} {:extern} T$System.Object() : Type;
axiom $Subtype(T$RegressionTestInput.RealNumbers(), T$System.Object());
@@ -651,7 +651,7 @@ procedure RegressionTestInput.S.#default_ctor(this: Ref); function {:constructor} T$RegressionTestInput.S() : Type;
-function {:extern} T$System.ValueType() : Type;
+function {:constructor} {:extern} T$System.ValueType() : Type;
axiom $Subtype(T$System.ValueType(), T$System.Object());
@@ -1075,13 +1075,13 @@ implementation T$RegressionTestInput.BitwiseOperations.#cctor() function {:constructor} T$RegressionTestInput.AsyncAttribute() : Type;
-function {:extern} T$System.Attribute() : Type;
+function {:constructor} {:extern} T$System.Attribute() : Type;
axiom $Subtype(T$System.Attribute(), T$System.Object());
axiom $DisjointSubtree(T$System.Attribute(), T$System.Object());
-function {:extern} T$System.Runtime.InteropServices._Attribute() : Type;
+function {:constructor} {:extern} T$System.Runtime.InteropServices._Attribute() : Type;
axiom $Subtype(T$System.Attribute(), T$System.Runtime.InteropServices._Attribute());
@@ -1275,7 +1275,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: }
else
{
- call $tmp2 := System.Activator.CreateInstance``1(T);
+ call $tmp2 := System.Activator.CreateInstance``1(T#T$RegressionTestInput.NestedGeneric.C.G`1($DynamicType($this)));
$tmp1 := Box2Box($tmp2);
if ($Exception != null)
{
diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 1a2ff101..83cc1869 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -417,7 +417,7 @@ var {:thread_local} $Exception: Ref; function {:constructor} T$RegressionTestInput.RealNumbers() : Type;
-function {:extern} T$System.Object() : Type;
+function {:constructor} {:extern} T$System.Object() : Type;
axiom $Subtype(T$RegressionTestInput.RealNumbers(), T$System.Object());
@@ -637,7 +637,7 @@ procedure RegressionTestInput.S.#default_ctor(this: Ref); function {:constructor} T$RegressionTestInput.S() : Type;
-function {:extern} T$System.ValueType() : Type;
+function {:constructor} {:extern} T$System.ValueType() : Type;
axiom $Subtype(T$System.ValueType(), T$System.Object());
@@ -1061,13 +1061,13 @@ implementation T$RegressionTestInput.BitwiseOperations.#cctor() function {:constructor} T$RegressionTestInput.AsyncAttribute() : Type;
-function {:extern} T$System.Attribute() : Type;
+function {:constructor} {:extern} T$System.Attribute() : Type;
axiom $Subtype(T$System.Attribute(), T$System.Object());
axiom $DisjointSubtree(T$System.Attribute(), T$System.Object());
-function {:extern} T$System.Runtime.InteropServices._Attribute() : Type;
+function {:constructor} {:extern} T$System.Runtime.InteropServices._Attribute() : Type;
axiom $Subtype(T$System.Attribute(), T$System.Runtime.InteropServices._Attribute());
@@ -1261,7 +1261,7 @@ implementation RegressionTestInput.NestedGeneric.C.G`1.#ctor$System.Int32($this: }
else
{
- call $tmp2 := System.Activator.CreateInstance``1(T);
+ call $tmp2 := System.Activator.CreateInstance``1(T#T$RegressionTestInput.NestedGeneric.C.G`1($DynamicType($this)));
$tmp1 := Box2Box($tmp2);
if ($Exception != null)
{
diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl index 2bca4e83..f794b227 100644 --- a/Test/datatypes/t2.bpl +++ b/Test/datatypes/t2.bpl @@ -38,6 +38,7 @@ axiom (forall u : DotNetType :: $Subtype(D(u), GenericType1(u))); function {:constructor} GenericType2(T:DotNetType, U:DotNetType) : DotNetType;
axiom (forall t : DotNetType, u : DotNetType :: $Subtype(GenericType2(t,u), System.Object()));
+
procedure foo(t : DotNetType)
{
assert System.Object() != GenericType1(t);
@@ -52,3 +53,10 @@ procedure bar(t : DotNetType, u : DotNetType) assert GenericType1(t) != GenericType1(u);
}
+function IntToType(x : int) : DotNetType;
+procedure baz(i : int)
+{
+ var t : DotNetType;
+ t := IntToType(i);
+ assert T#GenericType1(t) == System.Object();
+}
\ No newline at end of file |