Load all assemblies before doing anything else so that the unification for

the Core Assembly identity can happen correctly.
Cache things in the sink based on the mangled name rather than the interned
key: this prevents clashes in the Boogie program, but might mask some errors
due to different types/members with the same full name (minus the assembly name
of course).
Translate generic parameters as Ref instead of Box if they are constrained to
be a reference or struct (since we translate structs as Ref). [Experimental]

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;

     }