Created an API so that a MetadataTraverser is used to translate a set of

assemblies. This enables a translator to do whole-program analyses, such as
recording the subtype relationship across all of the input. (Still need to move
the delegate translation into this method.)
Fixed the existing whole-program translator so it uses the base class functionality
for translating the arguments to a method call.
Updated the regressions.

7 files changed, 84 insertions, 105 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 1dd181ae..08e32248 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -484,21 +484,7 @@ namespace BytecodeTranslator
       string methodname = proc.Name;

       var translateAsFunctionCall = proc is Bpl.Function;

       Bpl.QKeyValue attrib = null;

-

       if (!translateAsFunctionCall) {

-        if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

-          Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);

-          Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(cloc, v);

-          if (resolvedMethod.Type is IGenericTypeParameter) {

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

-            toBoxed[unboxed] = boxed;

-            outvars.Add(boxed);

-          } else {

-            outvars.Add(unboxed);

-          }

-          TranslatedExpressions.Push(unboxed);

-        }

-

         foreach (var a in resolvedMethod.Attributes) {

           if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {

             attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);

@@ -581,7 +567,7 @@ namespace BytecodeTranslator
       }

     }

 

-    private Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable<IExpression> arguments, out List<Bpl.Expr> inexpr, out List<Bpl.IdentifierExpr> outvars, out Bpl.IdentifierExpr thisExpr, out List<Bpl.Variable> locals, out List<IFieldDefinition> args, out Bpl.Expr arrayExpr, out Bpl.Expr indexExpr, out Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed) {

+    protected Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable<IExpression> arguments, out List<Bpl.Expr> inexpr, out List<Bpl.IdentifierExpr> outvars, out Bpl.IdentifierExpr thisExpr, out List<Bpl.Variable> locals, out List<IFieldDefinition> args, out Bpl.Expr arrayExpr, out Bpl.Expr indexExpr, out Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed) {

       inexpr = new List<Bpl.Expr>();

       outvars = new List<Bpl.IdentifierExpr>();

 

@@ -652,7 +638,26 @@ namespace BytecodeTranslator
         }

         penum.MoveNext();

       }

-      return this.sink.FindOrCreateProcedure(resolvedMethod);

+

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

+      

+      var translateAsFunctionCall = proc is Bpl.Function;

+      if (!translateAsFunctionCall) {

+        if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

+          Bpl.Variable v = this.sink.CreateFreshLocal(resolvedMethod.Type.ResolvedType);

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

+          if (resolvedMethod.Type is IGenericTypeParameter) {

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

+            toBoxed[unboxed] = boxed;

+            outvars.Add(boxed);

+          } else {

+            outvars.Add(unboxed);

+          }

+          TranslatedExpressions.Push(unboxed);

+        }

+      }

+

+      return proc;

     }

 

     #endregion

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index e300d3b5..75601140 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -30,22 +30,25 @@ namespace BytecodeTranslator {
 

     public readonly TraverserFactory factory;

 

-    public readonly PdbReader/*?*/ PdbReader;

+    public readonly IDictionary<IUnit, PdbReader> PdbReaders;

+    public PdbReader/*?*/ PdbReader;

 

-    public MetadataTraverser(Sink sink, PdbReader/*?*/ pdbReader)

+    public MetadataTraverser(Sink sink, IDictionary<IUnit, PdbReader> pdbReaders)

       : base() {

       this.sink = sink;

       this.factory = sink.Factory;

-      this.PdbReader = pdbReader;

+      this.PdbReaders = pdbReaders;

     }

 

     #region Overrides

 

     public override void Visit(IModule module) {

+      this.PdbReaders.TryGetValue(module, out this.PdbReader);

       base.Visit(module);

     }

 

     public override void Visit(IAssembly assembly) {

+      this.PdbReaders.TryGetValue(assembly, out this.PdbReader);

       this.sink.BeginAssembly(assembly);

       try {

         base.Visit(assembly);

@@ -386,6 +389,15 @@ namespace BytecodeTranslator {
 

     #endregion

 

+    #region Public API

+    public virtual void TranslateAssemblies(IEnumerable<IUnit> assemblies) {

+      foreach (var a in assemblies) {

+        a.Dispatch(this);

+      }

+    }

+    #endregion

+

+    #region Helpers

     private class FindCtorCall : BaseCodeTraverser {

       private bool isDeferringCtor = false;

       public ITypeReference containingType;

@@ -407,5 +419,7 @@ namespace BytecodeTranslator {
         base.Visit(methodCall);

       }

     }

+    #endregion

+

   }

 }
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index d04a8783..50ac68cf 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -108,7 +108,9 @@ namespace BytecodeTranslator {
       var host = new CodeContractAwareHostEnvironment(libPaths != null ? libPaths : Enumerable<string>.Empty, true, true);

       Host = host;

 

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

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

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

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

       foreach (var a in assemblyNames) {

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

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

@@ -122,7 +124,9 @@ namespace BytecodeTranslator {
           pdbReader = new PdbReader(pdbStream, host);

         }

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

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

+        modules.Add(module);

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

+        pdbReaders.Add(module, pdbReader);

       }

       if (stubAssemblies != null) {

         foreach (var s in stubAssemblies) {

@@ -153,7 +157,9 @@ namespace BytecodeTranslator {
           renamer.targetAssembly = mscorlibAssembly;

           renamer.originalAssemblyIdentity = mscorlibAssembly.AssemblyIdentity;

           renamer.RewriteChildren(mutableModule);

-          modules.Add(Tuple.Create((IModule)mutableModule, pdbReader));

+          modules.Add((IModule)mutableModule);

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

+          pdbReaders.Add(module, pdbReader);

 

         }

       }

@@ -162,7 +168,7 @@ namespace BytecodeTranslator {
         return -1;

       }

 

-      var primaryModule = modules[0].Item1;

+      var primaryModule = modules[0];

 

       TraverserFactory traverserFactory;

       if (wholeProgram)

@@ -173,20 +179,8 @@ namespace BytecodeTranslator {
       var sink = new Sink(host, traverserFactory, heapFactory);

       TranslationHelper.tmpVarCounter = 0;

 

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

-

-      }

+      MetadataTraverser translator = traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);

+      translator.TranslateAssemblies(modules);

 

       foreach (ITypeDefinition type in sink.delegateTypeToDelegates.Keys) {

         CreateDispatchMethod(sink, type);

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

 namespace BytecodeTranslator {

   public abstract class TraverserFactory {

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

+    public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,

+      IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?

+      IDictionary<IUnit, PdbReader> sourceLocationProviders)

     {

-      return new MetadataTraverser(sink, pdbReader);

+      return new MetadataTraverser(sink, sourceLocationProviders);

     }

     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 92154020..dd00768b 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -16,8 +16,7 @@ namespace BytecodeTranslator {
   class WholeProgram : TraverserFactory {

 

     /// <summary>

-    /// Table to be filled by the metadata traverser when it first gets to an assembly.

-    /// [TODO: It should be full set of assemblies that are being translated (CUA).]

+    /// Table to be filled by the metadata traverser before visiting any assemblies.

     /// 

     /// The table lists the direct supertypes of all type definitions that it encounters during the

     /// traversal. (But the table is organized so that subTypes[T] is the list of type definitions

@@ -25,8 +24,10 @@ namespace BytecodeTranslator {
     /// </summary>

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

 

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

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

+    public override MetadataTraverser MakeMetadataTraverser(Sink sink,

+      IDictionary<IUnit, IContractProvider> contractProviders, // TODO: remove this parameter?

+      IDictionary<IUnit, PdbReader> pdbReaders) {

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

     }

 

     public class WholeProgramMetadataSemantics : MetadataTraverser {

@@ -34,27 +35,23 @@ namespace BytecodeTranslator {
       readonly WholeProgram parent;

       readonly Sink sink;

 

-      /// <summary>

-      /// TODO: Need to have this populated before any of the assemblies in the CUA are traversed.

-      /// </summary>

-      readonly Dictionary<IAssembly, bool> codeUnderAnalysis = new Dictionary<IAssembly, bool>();

+      readonly Dictionary<IUnit, bool> codeUnderAnalysis = new Dictionary<IUnit, bool>();

 

-      public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, PdbReader/*?*/ pdbReader)

-        : base(sink, pdbReader) {

+      public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, IDictionary<IUnit, PdbReader> pdbReaders)

+        : base(sink, pdbReaders) {

         this.parent = parent;

         this.sink = sink;

       }

 

-      public override void Visit(IAssembly assembly) {

-

-        #region When doing whole-program analysis, traverse the assembly gathering type information

-        this.codeUnderAnalysis.Add(assembly, true);

+      public override void TranslateAssemblies(IEnumerable<IUnit> assemblies) {

+        #region traverse all of the units gathering type information

         var typeRecorder = new RecordSubtypes(this.parent.subTypes);

-        typeRecorder.Visit(assembly);

+        foreach (var a in assemblies) {

+          this.codeUnderAnalysis.Add(a, true);

+          typeRecorder.Visit(a);

+        }

         #endregion

-

-        base.Visit(assembly);

-

+        base.TranslateAssemblies(assemblies);

       }

       

       class RecordSubtypes : BaseMetadataTraverser {

@@ -120,54 +117,18 @@ namespace BytecodeTranslator {
           return;

         }

 

-        #region Translate In Parameters

-

-        var inexpr = new List<Bpl.Expr>();

-        #region Create the 'this' argument for the function call

-        this.Visit(methodCall.ThisArgument);

-        inexpr.Add(this.TranslatedExpressions.Pop());

-        #endregion

-

-        Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();

-        IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();

-        penum.MoveNext();

-        foreach (IExpression exp in methodCall.Arguments) {

-          if (penum.Current == null) {

-            throw new TranslationException("More Arguments than Parameters in functioncall");

-          }

-          this.Visit(exp);

-          Bpl.Expr e = this.TranslatedExpressions.Pop();

-

-          p2eMap.Add(penum.Current, e);

-          if (!penum.Current.IsOut) {

-            inexpr.Add(e);

-          }

-

-          penum.MoveNext();

-        }

-        #endregion

-

         Bpl.IToken token = methodCall.Token();

 

-        #region Translate Out vars

-        var outvars = new List<Bpl.IdentifierExpr>();

+        List<Bpl.Expr> inexpr;

+        List<Bpl.IdentifierExpr> outvars;

+        Bpl.IdentifierExpr thisExpr;

+        List<Bpl.Variable> locals;

+        List<IFieldDefinition> args;

+        Bpl.Expr arrayExpr;

+        Bpl.Expr indexExpr;

+        Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed;

+        var proc = TranslateArgumentsAndReturnProcedure(token, methodCall.MethodToCall, resolvedMethod, methodCall.IsStaticCall ? null : methodCall.ThisArgument, methodCall.Arguments, out inexpr, out outvars, out thisExpr, out locals, out args, out arrayExpr, out indexExpr, out toBoxed);

 

-        foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap) {

-          if (kvp.Key.IsByReference) {

-            Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;

-            if (iexp == null) {

-              throw new TranslationException("Trying to pass complex expression as out in functioncall");

-            }

-            outvars.Add(iexp);

-          }

-        }

-        #endregion

-

-        if (methodCall.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {

-          Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);

-          outvars.Add(new Bpl.IdentifierExpr(token, v));

-          TranslatedExpressions.Push(new Bpl.IdentifierExpr(token, v));

-        }

 

         Bpl.QKeyValue attrib = null;

         foreach (var a in resolvedMethod.Attributes) {

@@ -179,7 +140,6 @@ namespace BytecodeTranslator {
 

         var elseBranch = new Bpl.StmtListBuilder();

 

-        var proc = this.sink.FindOrCreateProcedure(resolvedMethod);

         var methodname = proc.Name;

 

         Bpl.CallCmd call;

diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
index aac37bf0..295349c9 100644
--- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt
@@ -49,7 +49,9 @@ implementation System.Object.GetType(this: Ref) returns ($result: Ref)
 

 

 

-axiom (forall t: Type :: $DynamicType($TypeOf(t)) == t);

+function $TypeOfInv(Ref) : Type;

+

+axiom (forall t: Type :: { $TypeOf(t) } $TypeOfInv($TypeOf(t)) == t);

 

 function $ThreadDelegate(Ref) : Ref;

 

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
index 73e2000c..a0ba97d5 100644
--- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -51,7 +51,9 @@ implementation System.Object.GetType(this: Ref) returns ($result: Ref)
 

 

 

-axiom (forall t: Type :: $DynamicType($TypeOf(t)) == t);

+function $TypeOfInv(Ref) : Type;

+

+axiom (forall t: Type :: { $TypeOf(t) } $TypeOfInv($TypeOf(t)) == t);

 

 function $ThreadDelegate(Ref) : Ref;