Can now translate multiple assemblies into one Boogie Program.

Support for stub methods.

6 files changed, 124 insertions, 54 deletions

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index ed91f97f..48a57f72 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -39,10 +39,6 @@ namespace BytecodeTranslator {
       this.PdbReader = pdbReader;

     }

 

-    public Bpl.Program TranslatedProgram {

-      get { return this.sink.TranslatedProgram; }

-    }

-

     #region Overrides

 

     public override void Visit(IModule module) {

@@ -86,8 +82,7 @@ namespace BytecodeTranslator {
       

       try

       {

-        var procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(invokeMethod);

-        var proc = procAndFormalMap.Procedure;

+        var proc = this.sink.FindOrCreateProcedure(invokeMethod);

         var invars = proc.InParams;

         var outvars = proc.OutParams;

 

@@ -303,7 +298,13 @@ namespace BytecodeTranslator {
 

       this.sink.BeginMethod();

 

-      var procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(method);

+      Sink.ProcedureInfo procAndFormalMap;

+      IMethodDefinition stubMethod = null;

+      if (IsStubMethod(method, out stubMethod)) {

+        procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(stubMethod);

+      } else {

+        procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(method);

+      }

 

       if (method.IsAbstract) { // we're done, just define the procedure

         return;

@@ -436,6 +437,41 @@ namespace BytecodeTranslator {
       }

       return inits;

     }

+    // TODO: do a type test, not a string test for the attribute

+    private bool IsStubMethod(IMethodDefinition methodDefinition, out IMethodDefinition/*?*/ stubMethod) {

+      stubMethod = null;

+      var td = GetTypeDefinitionFromAttribute(methodDefinition.Attributes, "BytecodeTranslator.StubAttribute");

+      if (td == null)

+        td = GetTypeDefinitionFromAttribute(methodDefinition.ContainingTypeDefinition.Attributes, "BytecodeTranslator.StubAttribute");

+      if (td != null) {

+        foreach (var mem in td.GetMatchingMembersNamed(methodDefinition.Name, false,

+          tdm => {

+            var md = tdm as IMethodDefinition;

+            return md != null && MemberHelper.MethodsAreEquivalent(methodDefinition, md);

+          })) {

+          stubMethod = mem as IMethodDefinition;

+          return true;

+        }

+      }

+      return false;

+    }

+    public static ITypeDefinition/*?*/ GetTypeDefinitionFromAttribute(IEnumerable<ICustomAttribute> attributes, string attributeName) {

+      ICustomAttribute foundAttribute = null;

+      foreach (ICustomAttribute attribute in attributes) {

+        if (TypeHelper.GetTypeName(attribute.Type) == attributeName) {

+          foundAttribute = attribute;

+          break;

+        }

+      }

+      if (foundAttribute == null) return null;

+      List<IMetadataExpression> args = new List<IMetadataExpression>(foundAttribute.Arguments);

+      if (args.Count < 1) return null;

+      IMetadataTypeOf abstractTypeMD = args[0] as IMetadataTypeOf;

+      if (abstractTypeMD == null) return null;

+      ITypeReference referencedTypeReference = Microsoft.Cci.MutableContracts.ContractHelper.Unspecialized(abstractTypeMD.TypeToGet);

+      ITypeDefinition referencedTypeDefinition = referencedTypeReference.ResolvedType;

+      return referencedTypeDefinition;

+    }

 

     public override void Visit(IFieldDefinition fieldDefinition) {

       this.sink.FindOrCreateFieldVariable(fieldDefinition);

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 44a404d0..47700462 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -12,15 +12,17 @@ using Microsoft.Cci.MutableCodeModel;
 using System.Collections.Generic;

 using Microsoft.Cci.Contracts;

 using Microsoft.Cci.ILToCodeModel;

+using Microsoft.Cci.MutableContracts;

 

 using Bpl = Microsoft.Boogie;

+using System.Diagnostics.Contracts;

 

 namespace BytecodeTranslator {

 

   class Options : OptionParsing {

 

-    [OptionDescription("The name of the assembly to use as input", ShortForm = "a")]

-    public string assembly = null;

+    [OptionDescription("The names of the assemblies to use as input", ShortForm = "a")]

+    public List<string> assemblies = null;

 

     [OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]

     public List<string> libpaths = new List<string>();

@@ -52,7 +54,13 @@ namespace BytecodeTranslator {
       }

       #endregion

 

-      var assemblyName = String.IsNullOrEmpty(options.assembly) ? options.GeneralArguments[0] : options.assembly;

+      var assemblyNames = options.assemblies;

+      if (assemblyNames == null || assemblyNames.Count == 0) {

+        assemblyNames = new List<string>();

+        foreach (var g in options.GeneralArguments) {

+          assemblyNames.Add(g);

+        }

+      }

 

       try {

 

@@ -75,7 +83,7 @@ namespace BytecodeTranslator {
             return 1;

         }

 

-        result = TranslateAssembly(assemblyName, heap, options.libpaths, options.wholeProgram);

+        result = TranslateAssembly(assemblyNames, heap, options.libpaths, options.wholeProgram);

 

       } catch (Exception e) { // swallow everything and just return an error code

         Console.WriteLine("The byte-code translator failed with uncaught exception: {0}", e.Message);

@@ -85,46 +93,63 @@ namespace BytecodeTranslator {
       return result;

     }

 

-    public static int TranslateAssembly(string assemblyName, HeapFactory heapFactory, List<string> libPaths, bool wholeProgram) {

+    public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, List<string>/*?*/ libPaths, bool wholeProgram) {

+      Contract.Requires(assemblyNames != null);

+      Contract.Requires(heapFactory != null);

 

-      var host = new Microsoft.Cci.MutableContracts.CodeContractAwareHostEnvironment(libPaths != null ? libPaths : IteratorHelper.GetEmptyEnumerable<string>(), true, true);

+      var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : IteratorHelper.GetEmptyEnumerable<string>(), true, true);

       Host = host;

 

-      IModule/*?*/ module = host.LoadUnitFrom(assemblyName) as IModule;

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

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

-        return 1;

+      var modules = new List<Tuple<IModule,PdbReader/*?*/>>();

+      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");

+        }

+        PdbReader/*?*/ pdbReader = null;

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

+        if (File.Exists(pdbFile)) {

+          Stream pdbStream = File.OpenRead(pdbFile);

+          pdbReader = new PdbReader(pdbStream, host);

+        }

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

+        modules.Add(Tuple.Create(module, pdbReader));

       }

-

-      IAssembly/*?*/ assembly = null;

-

-      PdbReader/*?*/ pdbReader = null;

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

-      if (File.Exists(pdbFile)) {

-        Stream pdbStream = File.OpenRead(pdbFile);

-        pdbReader = new PdbReader(pdbStream, host);

+      if (modules.Count == 0) {

+        Console.WriteLine("No input assemblies to translate.");

+        return -1;

       }

 

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

+      var primaryModule = modules[0].Item1;

 

-      #region Translate the code model to BPL

-      TraverserFactory factory;

+      TraverserFactory traverserFactory;

       if (wholeProgram)

-        factory = new WholeProgram();

+        traverserFactory = new WholeProgram();

       else

-        factory = new CLRSemantics();

-      MetadataTraverser translator = factory.MakeMetadataTraverser(host.GetContractExtractor(module.ModuleIdentity), pdbReader, heapFactory);

+        traverserFactory = new CLRSemantics();

+

+      var sink = new Sink(host, traverserFactory, heapFactory);

       TranslationHelper.tmpVarCounter = 0;

-      assembly = module as IAssembly;

-      if (assembly != null)

-        translator.Visit(assembly);

-      else

-        translator.Visit(module);

-      #endregion

 

-      Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(module.Name + ".bpl");

+      foreach (var tup in modules) {

+

+        var module = tup.Item1;

+        var pdbReader = tup.Item2;

+

+        IAssembly/*?*/ assembly = null;

+        MetadataTraverser translator = traverserFactory.MakeMetadataTraverser(sink, host.GetContractExtractor(module.ModuleIdentity), pdbReader);

+        assembly = module as IAssembly;

+        if (assembly != null)

+          translator.Visit(assembly);

+        else

+          translator.Visit(module);

+

+      }

+

+      Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl");

       Prelude.Emit(writer);

-      translator.TranslatedProgram.Emit(writer);

+      sink.TranslatedProgram.Emit(writer);

       writer.Close();

       return 0; // success

     }

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index c917bd9a..670410f6 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -26,12 +26,15 @@ namespace BytecodeTranslator {
       get { return this.factory; }

     }

     readonly TraverserFactory factory;

-    public readonly IContractProvider ContractProvider;

 

-    public Sink(TraverserFactory factory, HeapFactory heapFactory, IContractProvider contractProvider) {

+    public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory) {

+      Contract.Requires(host != null);

+      Contract.Requires(factory != null);

+      Contract.Requires(heapFactory != null);

+

+      this.host = host;

       this.factory = factory;

       var b = heapFactory.MakeHeap(this, out this.heap, out this.TranslatedProgram); // TODO: what if it returns false?

-      this.ContractProvider = contractProvider;

       if (this.TranslatedProgram == null) {

         this.TranslatedProgram = new Bpl.Program();

       } else {

@@ -139,7 +142,11 @@ namespace BytecodeTranslator {
     public Bpl.Variable FindParameterVariable(IParameterDefinition param, bool contractContext) {

       MethodParameter mp;

       ProcedureInfo procAndFormalMap;

-      this.declaredMethods.TryGetValue(param.ContainingSignature, out procAndFormalMap);

+      var sig = param.ContainingSignature;

+      // BUGBUG: If param's signature is not a method reference, then it doesn't have an interned

+      // key. The declaredMethods table needs to use ISignature for its keys.

+      var key = ((IMethodReference)sig).InternedKey;

+      this.declaredMethods.TryGetValue(key, out procAndFormalMap);

       var formalMap = procAndFormalMap.FormalMap;

       formalMap.TryGetValue(param, out mp);

       return contractContext ? mp.inParameterCopy : mp.outParameterCopy;

@@ -217,7 +224,7 @@ namespace BytecodeTranslator {
     public Bpl.Procedure FindOrCreateProcedure(IMethodDefinition method) {

       ProcedureInfo procAndFormalMap;

 

-      var key = method; //.InternedKey;

+      var key = method.InternedKey;

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

 

         string MethodName = TranslationHelper.CreateUniqueMethodName(method);

@@ -298,7 +305,8 @@ namespace BytecodeTranslator {
         Bpl.IdentifierExprSeq boogieModifies = new Bpl.IdentifierExprSeq();

 

         var possiblyUnspecializedMethod = Unspecialize(method);

-        IMethodContract contract = ContractProvider.GetMethodContractFor(possiblyUnspecializedMethod);

+

+        var contract = Microsoft.Cci.MutableContracts.ContractHelper.GetMethodContractFor(this.host, possiblyUnspecializedMethod.ResolvedMethod);

 

         if (contract != null) {

           try {

@@ -368,7 +376,7 @@ namespace BytecodeTranslator {
 

     // TODO: check method's containing type in case the entire type is a stub type.

     // TODO: do a type test, not a string test for the attribute

-    private bool IsStubMethod(IMethodReference method, out string newName) {

+    private bool IsStubMethod(IMethodReference method, out string/*?*/ newName) {

       newName = null;

       var methodDefinition = method.ResolvedMethod;

       foreach (var a in methodDefinition.Attributes) {

@@ -388,7 +396,7 @@ namespace BytecodeTranslator {
 

     public ProcedureInfo FindOrCreateProcedureAndReturnProcAndFormalMap(IMethodDefinition method) {

       this.FindOrCreateProcedure(method);

-      return this.declaredMethods[method];

+      return this.declaredMethods[method.InternedKey];

     }

     private static IMethodReference Unspecialize(IMethodReference method) {

       IMethodReference result = method;

@@ -433,11 +441,11 @@ namespace BytecodeTranslator {
     private Dictionary<uint, Bpl.Variable> declaredTypes = new Dictionary<uint, Bpl.Variable>();

 

     /// <summary>

-    /// The keys to the table are the signatures of the methods.

+    /// The keys to the table are the interned keys of the methods.

     /// The values are pairs: first element is the procedure,

     /// second element is the formal map for the procedure

     /// </summary>

-    private Dictionary<ISignature, ProcedureInfo> declaredMethods = new Dictionary<ISignature, ProcedureInfo>();

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

     /// <summary>

     /// The values in this table are the procedures

     /// defined in the program created by the heap in the Sink's ctor.

@@ -463,6 +471,7 @@ namespace BytecodeTranslator {
     }

 

     private Dictionary<IMethodDefinition, Bpl.Constant> delegateMethods = new Dictionary<IMethodDefinition, Bpl.Constant>();

+    private IContractAwareHost host;

 

     public Bpl.Constant FindOrAddDelegateMethodConstant(IMethodDefinition defn)

     {

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index ba465067..cdc1c8a3 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -18,9 +18,9 @@ using Bpl = Microsoft.Boogie;
 

 namespace BytecodeTranslator {

   public abstract class TraverserFactory {

-    public virtual MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider, PdbReader/*?*/ pdbReader, HeapFactory heapFactory)

+    public virtual MetadataTraverser MakeMetadataTraverser(Sink sink, IContractProvider contractProvider, PdbReader/*?*/ pdbReader)

     {

-      return new MetadataTraverser(new Sink(this, heapFactory, contractProvider), pdbReader);

+      return new MetadataTraverser(sink, pdbReader);

     }

     public virtual StatementTraverser MakeStatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext) {

       return new StatementTraverser(sink, pdbReader, contractContext);

diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index 290426fc..f4cc59af 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -25,8 +25,8 @@ namespace BytecodeTranslator {
     /// </summary>

     readonly public Dictionary<ITypeReference, List<ITypeReference>> subTypes = new Dictionary<ITypeReference, List<ITypeReference>>();

 

-    public override MetadataTraverser MakeMetadataTraverser(IContractProvider contractProvider, PdbReader pdbReader, HeapFactory heapFactory) {

-      return new WholeProgramMetadataSemantics(this, new Sink(this, heapFactory, contractProvider), pdbReader);

+    public override MetadataTraverser MakeMetadataTraverser(Sink sink, IContractProvider contractProvider, PdbReader pdbReader) {

+      return new WholeProgramMetadataSemantics(this, sink, pdbReader);

     }

 

     public class WholeProgramMetadataSemantics : MetadataTraverser {

diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index 236ec12f..b2ec84b0 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -61,7 +61,7 @@ namespace TranslationTest {
     #endregion

 

     private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {

-      BCT.TranslateAssembly(assemblyName, heapFactory, null, false);

+      BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, null, false);

       var fileName = Path.ChangeExtension(assemblyName, "bpl");

       var s = File.ReadAllText(fileName);

       return s;