Merge

3 files changed, 100 insertions, 50 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 47c68419..dd65a1f6 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -54,6 +54,15 @@ namespace BytecodeTranslator
       return this.sink.FindOrCreateTypeReference(typeReference);

     }

 

+    private static IMethodDefinition ResolveUnspecializedMethodOrThrow(IMethodReference methodReference) {

+      var resolvedMethod = Sink.Unspecialize(methodReference).ResolvedMethod;

+      if (resolvedMethod == Dummy.Method) { // avoid downstream errors, fail early

+        throw new TranslationException(ExceptionType.UnresolvedMethod, MemberHelper.GetMethodSignature(methodReference, NameFormattingOptions.None));

+      }

+      return resolvedMethod;

+    }

+

+

     #region Constructors

 

     ///// <summary>

@@ -511,12 +520,7 @@ namespace BytecodeTranslator
     /// <param name="methodCall"></param>

     /// <remarks>Stub, This one really needs comments!</remarks>

     public override void TraverseChildren(IMethodCall methodCall) {

-      var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;

-      if (resolvedMethod == Dummy.Method) {

-        throw new TranslationException(

-          ExceptionType.UnresolvedMethod,

-          MemberHelper.GetMethodSignature(methodCall.MethodToCall, NameFormattingOptions.None));

-      }

+      var resolvedMethod = ResolveUnspecializedMethodOrThrow(methodCall.MethodToCall);

 

       Bpl.IToken methodCallToken = methodCall.Token();

 

@@ -707,10 +711,15 @@ namespace BytecodeTranslator
           if (unboxed == null) {

             throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");

           }

-          if (penum.Current.Type is IGenericTypeParameter || penum.Current.Type is IGenericMethodParameter) {

-            Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));

-            toBoxed[unboxed] = boxed;

-            outvars.Add(boxed);

+          if (penum.Current.Type is IGenericParameter) {

+            var boogieType = this.sink.CciTypeToBoogie(penum.Current.Type);

+            if (boogieType == this.sink.Heap.BoxType) {

+              Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));

+              toBoxed[unboxed] = boxed;

+              outvars.Add(boxed);

+            } else {

+              outvars.Add(unboxed);

+            }

           } else {

             outvars.Add(unboxed);

           }

@@ -738,10 +747,15 @@ namespace BytecodeTranslator
         if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

           Bpl.Variable v = this.sink.CreateFreshLocal(methodToCall.ResolvedMethod.Type.ResolvedType);

           Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(token, v);

-          if (resolvedMethod.Type is IGenericTypeParameter || resolvedMethod.Type is IGenericMethodParameter) {

-            Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));

-            toBoxed[unboxed] = boxed;

-            outvars.Add(boxed);

+          if (resolvedMethod.Type is IGenericParameter) {

+            var boogieType = this.sink.CciTypeToBoogie(methodToCall.Type);

+            if (boogieType == this.sink.Heap.BoxType) {

+              Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));

+              toBoxed[unboxed] = boxed;

+              outvars.Add(boxed);

+            } else {

+              outvars.Add(unboxed);

+            }

           } else {

             outvars.Add(unboxed);

           }

@@ -932,7 +946,8 @@ namespace BytecodeTranslator
     public override void TraverseChildren(ICreateObjectInstance createObjectInstance)

     {

       var ctor = createObjectInstance.MethodToCall;

-      var resolvedMethod = Sink.Unspecialize(ctor).ResolvedMethod;

+      var resolvedMethod = ResolveUnspecializedMethodOrThrow(ctor);

+

       Bpl.IToken token = createObjectInstance.Token();

 

       var a = this.sink.CreateFreshLocal(createObjectInstance.Type);

@@ -974,7 +989,6 @@ namespace BytecodeTranslator
       TranslatedExpressions.Push(Bpl.Expr.Ident(a));

     }

 

-

     public override void TraverseChildren(ICreateArray createArrayInstance)

     {

       Bpl.IToken cloc = createArrayInstance.Token();

@@ -1012,7 +1026,7 @@ namespace BytecodeTranslator
       var a = this.sink.CreateFreshLocal(creationAST.Type);

 

       ITypeDefinition unspecializedType = Microsoft.Cci.MutableContracts.ContractHelper.Unspecialized(type.ResolvedType).ResolvedType;

-      IMethodDefinition unspecializedMethod = Sink.Unspecialize(methodToCall.ResolvedMethod).ResolvedMethod;

+      IMethodDefinition unspecializedMethod = ResolveUnspecializedMethodOrThrow(methodToCall);

       sink.AddDelegate(unspecializedType, unspecializedMethod);

       Bpl.Constant constant = sink.FindOrCreateDelegateMethodConstant(unspecializedMethod);

       Bpl.Expr methodExpr = Bpl.Expr.Ident(constant);

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 4702d5a0..c8300189 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -197,27 +197,35 @@ namespace BytecodeTranslator {
       modules = new List<IModule>();

       var contractExtractors = new Dictionary<IUnit, IContractProvider>();

       var pdbReaders = new Dictionary<IUnit, PdbReader>();

+      #region Load *all* of the assemblies before doing anything else so that they can all vote on unification matters

       foreach (var a in assemblyNames) {

         var module = host.LoadUnitFrom(a) as IModule;

         if (module == null || module == Dummy.Module || module == Dummy.Assembly) {

           Console.WriteLine(a + " is not a PE file containing a CLR module or assembly, or an error occurred when loading it.");

           Console.WriteLine("Skipping it, continuing with other input assemblies");

         }

+        modules.Add(module);

+      }

+      #endregion

+      #region Decompile all of the assemblies

+      var decompiledModules = new List<IModule>();

+      foreach (var m in modules) {

         PdbReader/*?*/ pdbReader = null;

-        string pdbFile = Path.ChangeExtension(module.Location, "pdb");

+        string pdbFile = Path.ChangeExtension(m.Location, "pdb");

         if (File.Exists(pdbFile)) {

           Stream pdbStream = File.OpenRead(pdbFile);

           pdbReader = new PdbReader(pdbStream, host);

         }

-        module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader) as IModule;

+        var m2 = Decompiler.GetCodeModelFromMetadataModel(host, m, 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).Rewrite(module);

-

-        host.RegisterAsLatest(module);

-        modules.Add(module);

-        contractExtractors.Add(module, host.GetContractExtractor(module.UnitIdentity));

-        pdbReaders.Add(module, pdbReader);

+        m2 = new Microsoft.Cci.MutableContracts.ContractExtractor.AssertAssumeExtractor(host, pdbReader).Rewrite(m2);

+        decompiledModules.Add(m2);

+        host.RegisterAsLatest(m2);

+        contractExtractors.Add(m2, host.GetContractExtractor(m2.UnitIdentity));

+        pdbReaders.Add(m2, pdbReader);

       }

+      modules = decompiledModules;

+      #endregion

       #endregion

 

       #region Assemblies to translate (stubs)

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 957b8c38..bcf3ce0b 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -133,9 +133,15 @@ namespace BytecodeTranslator {
         return heap.RefType; // structs are kept on the heap with special rules about assignment

       else if (type.IsEnum)

         return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer

-      else if (type is IGenericTypeParameter || type is IGenericMethodParameter)

+      else if (type is IGenericParameter) {

+        var gp = type as IGenericParameter;

+        if (gp.MustBeReferenceType || gp.MustBeValueType)

+          return heap.RefType;

+        foreach (var c in gp.Constraints){

+          return CciTypeToBoogie(c);

+        }

         return heap.BoxType;

-      else

+      } else

         return heap.RefType;

     }

 

@@ -148,17 +154,19 @@ namespace BytecodeTranslator {
     public Bpl.Variable CreateFreshLocal(ITypeReference typeReference) {

       Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location

       Bpl.Type t = CciTypeToBoogie(typeReference);

-      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));

+      var localName = TranslationHelper.GenerateTempVarName();

+      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, localName, t));

       ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie

-      localVarMap.Add(dummy, v);

+      localVarMap.Add(localName, v);

       return v;

     }

 

     public Bpl.Variable CreateFreshLocal(Bpl.Type t) {

       Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location

-      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));

+      var localName = TranslationHelper.GenerateTempVarName();

+      Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, localName, t));

       ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie

-      localVarMap.Add(dummy, v);

+      localVarMap.Add(localName, v);

       return v;

     }

 

@@ -182,9 +190,10 @@ namespace BytecodeTranslator {
 

     /// <summary>

     /// State that gets re-initialized per method

+    /// Keys are the mangled names to avoid name clashes.

     /// </summary>

-    private Dictionary<ILocalDefinition, Bpl.LocalVariable> localVarMap = null;

-    public Dictionary<ILocalDefinition, Bpl.LocalVariable> LocalVarMap {

+    private Dictionary<string, Bpl.LocalVariable> localVarMap = null;

+    public Dictionary<string, Bpl.LocalVariable> LocalVarMap {

       get { return this.localVarMap; }

     }

     private int localCounter;

@@ -199,11 +208,14 @@ namespace BytecodeTranslator {
       Bpl.LocalVariable v;

       Bpl.IToken tok = local.Token();

       Bpl.Type t = CciTypeToBoogie(local.Type.ResolvedType);

-      if (!localVarMap.TryGetValue(local, out v)) {

-        var name = local.Name.Value;

-        name = TranslationHelper.TurnStringIntoValidIdentifier(name);

+      var name = local.Name.Value;

+      name = TranslationHelper.TurnStringIntoValidIdentifier(name);

+      var typeName = t.ToString();

+      typeName = TranslationHelper.TurnStringIntoValidIdentifier(typeName);

+      var mangledName = String.Format("{0}_{1}", name, typeName);

+      if (!localVarMap.TryGetValue(mangledName, out v)) {

         v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name, t));

-        localVarMap.Add(local, v);

+        localVarMap.Add(mangledName, v);

       }

       return v;

     }

@@ -684,7 +696,15 @@ namespace BytecodeTranslator {
       return procInfo;

     }

 

-    private Dictionary<uint, ProcedureInfo> declaredStructDefaultCtors = new Dictionary<uint, ProcedureInfo>();

+    /// <summary>

+    /// The keys are the mangled names for the ctors. That is avoid generating name conflicts in the translated

+    /// program. This is needed for things like System.Drawing.Rect, which was referenced in both System.Drawing v2

+    /// as well as System.Drawing v4. Since those assemblies are not unified, the two types are distinct, but

+    /// the (generated) name for the default struct ctors clash.

+    /// NB: This means that if there are two different types with the same full name (minus the assembly name),

+    /// then this will implicitly unify them. This could lead to big trouble!

+    /// </summary>

+    private Dictionary<string, ProcedureInfo> declaredStructDefaultCtors = new Dictionary<string, ProcedureInfo>();

     /// <summary>

     /// Struct "creation" (source code that looks like "new S()" for a struct type S) is modeled

     /// by a call to the nullary "ctor" that initializes all of the structs fields to zero-

@@ -699,14 +719,14 @@ namespace BytecodeTranslator {
       Contract.Requires(structType.IsValueType);

 

       ProcedureInfo procAndFormalMap;

-      var key = structType.InternedKey;

-      if (!this.declaredStructDefaultCtors.TryGetValue(key, out procAndFormalMap)) {

-        var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

+      var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

+      var procName = typename + ".#default_ctor";

+      if (!this.declaredStructDefaultCtors.TryGetValue(procName, out procAndFormalMap)) {

         var tok = structType.Token();

         var selfType = this.CciTypeToBoogie(structType); //new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);

         var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), true);

         var invars = new Bpl.Formal[] { selfIn };

-        var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#default_ctor",

+        var proc = new Bpl.Procedure(Bpl.Token.NoToken, procName,

           new Bpl.TypeVariableSeq(),

           new Bpl.VariableSeq(invars),

           new Bpl.VariableSeq(), // out

@@ -716,12 +736,20 @@ namespace BytecodeTranslator {
           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

         procAndFormalMap = new ProcedureInfo(proc, new MethodParameter[0]);

-        this.declaredStructDefaultCtors.Add(key, procAndFormalMap);

+        this.declaredStructDefaultCtors.Add(procName, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

     }

 

-    private Dictionary<uint, ProcedureInfo> declaredStructCopyCtors = new Dictionary<uint, ProcedureInfo>();

+    /// <summary>

+    /// The keys are the mangled names for the ctors. That is avoid generating name conflicts in the translated

+    /// program. This is needed for things like System.Drawing.Rect, which was referenced in both System.Drawing v2

+    /// as well as System.Drawing v4. Since those assemblies are not unified, the two types are distinct, but

+    /// the (generated) name for the default struct ctors clash.

+    /// NB: This means that if there are two different types with the same full name (minus the assembly name),

+    /// then this will implicitly unify them. This could lead to big trouble!

+    /// </summary>

+    private Dictionary<string, ProcedureInfo> declaredStructCopyCtors = new Dictionary<string, ProcedureInfo>();

     private Dictionary<uint, ProcedureInfo> declaredStructEqualityOperators = new Dictionary<uint, ProcedureInfo>();

     /// <summary>

     /// The assignment of one struct value to another is modeled by a method that makes a field-by-field

@@ -736,9 +764,9 @@ namespace BytecodeTranslator {
       Contract.Requires(structType.IsValueType);

 

       ProcedureInfo procAndFormalMap;

-      var key = structType.InternedKey;

-      if (!this.declaredStructCopyCtors.TryGetValue(key, out procAndFormalMap)) {

-        var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

+      var typename = TranslationHelper.TurnStringIntoValidIdentifier(TypeHelper.GetTypeName(structType));

+      var procName = typename + ".#copy_ctor";

+      if (!this.declaredStructCopyCtors.TryGetValue(procName, out procAndFormalMap)) {

         var tok = structType.Token();

         var selfType = this.CciTypeToBoogie(structType); //new Bpl.MapType(Bpl.Token.NoToken, new Bpl.TypeVariableSeq(), new Bpl.TypeSeq(Heap.FieldType), Heap.BoxType);

         var selfIn = new Bpl.Formal(tok, new Bpl.TypedIdent(tok, "this", selfType), true);

@@ -750,7 +778,7 @@ namespace BytecodeTranslator {
         var req = new Bpl.Requires(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, selfInExpr, otherInExpr));

         var ens = new Bpl.Ensures(true, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, selfInExpr, otherInExpr));

 

-        var proc = new Bpl.Procedure(Bpl.Token.NoToken, typename + ".#copy_ctor",

+        var proc = new Bpl.Procedure(Bpl.Token.NoToken, procName,

           new Bpl.TypeVariableSeq(),

           new Bpl.VariableSeq(invars),

           new Bpl.VariableSeq(outvars),

@@ -760,7 +788,7 @@ namespace BytecodeTranslator {
           );

         this.TranslatedProgram.TopLevelDeclarations.Add(proc);

         procAndFormalMap = new ProcedureInfo(proc, new MethodParameter[0]);

-        this.declaredStructCopyCtors.Add(key, procAndFormalMap);

+        this.declaredStructCopyCtors.Add(procName, procAndFormalMap);

       }

       return procAndFormalMap.Decl;

     }

@@ -1124,7 +1152,7 @@ namespace BytecodeTranslator {
     public Dictionary<string, ProcedureInfo> initiallyDeclaredProcedures = new Dictionary<string, ProcedureInfo>();

 

     public void BeginMethod(ITypeReference containingType) {

-      this.localVarMap = new Dictionary<ILocalDefinition, Bpl.LocalVariable>();

+      this.localVarMap = new Dictionary<string, Bpl.LocalVariable>();

       this.localCounter = 0;

       this.methodBeingTranslated = null;

     }