From 356651d4f4e2d9825f18858603f506332d582ad5 Mon Sep 17 00:00:00 2001 From: Mike Barnett Date: Sat, 21 May 2011 18:38:18 -0700 Subject: 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. --- BCT/BytecodeTranslator/ExpressionTraverser.cs | 37 +++++---- BCT/BytecodeTranslator/MetadataTraverser.cs | 20 ++++- BCT/BytecodeTranslator/Program.cs | 30 +++----- BCT/BytecodeTranslator/TraverserFactory.cs | 6 +- BCT/BytecodeTranslator/WholeProgram.cs | 88 ++++++---------------- .../TranslationTest/GeneralHeapInput.txt | 4 +- .../TranslationTest/SplitFieldsHeapInput.txt | 4 +- 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(), null); @@ -581,7 +567,7 @@ namespace BytecodeTranslator } } - private Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable arguments, out List inexpr, out List outvars, out Bpl.IdentifierExpr thisExpr, out List locals, out List args, out Bpl.Expr arrayExpr, out Bpl.Expr indexExpr, out Dictionary toBoxed) { + protected Bpl.DeclWithFormals TranslateArgumentsAndReturnProcedure(Bpl.IToken token, IMethodReference methodToCall, IMethodDefinition resolvedMethod, IExpression/*?*/ thisArg, IEnumerable arguments, out List inexpr, out List outvars, out Bpl.IdentifierExpr thisExpr, out List locals, out List args, out Bpl.Expr arrayExpr, out Bpl.Expr indexExpr, out Dictionary toBoxed) { inexpr = new List(); outvars = new List(); @@ -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 PdbReaders; + public PdbReader/*?*/ PdbReader; - public MetadataTraverser(Sink sink, PdbReader/*?*/ pdbReader) + public MetadataTraverser(Sink sink, IDictionary 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 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.Empty, true, true); Host = host; - var modules = new List>(); + var modules = new List(); + var contractExtractors = new Dictionary(); + var pdbReaders = new Dictionary(); 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 contractProviders, // TODO: remove this parameter? + IDictionary 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 { /// - /// 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 { /// readonly public Dictionary> subTypes = new Dictionary>(); - public override MetadataTraverser MakeMetadataTraverser(Sink sink, IContractProvider contractProvider, PdbReader pdbReader) { - return new WholeProgramMetadataSemantics(this, sink, pdbReader); + public override MetadataTraverser MakeMetadataTraverser(Sink sink, + IDictionary contractProviders, // TODO: remove this parameter? + IDictionary pdbReaders) { + return new WholeProgramMetadataSemantics(this, sink, pdbReaders); } public class WholeProgramMetadataSemantics : MetadataTraverser { @@ -34,27 +35,23 @@ namespace BytecodeTranslator { readonly WholeProgram parent; readonly Sink sink; - /// - /// TODO: Need to have this populated before any of the assemblies in the CUA are traversed. - /// - readonly Dictionary codeUnderAnalysis = new Dictionary(); + readonly Dictionary codeUnderAnalysis = new Dictionary(); - public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, PdbReader/*?*/ pdbReader) - : base(sink, pdbReader) { + public WholeProgramMetadataSemantics(WholeProgram parent, Sink sink, IDictionary 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 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(); - #region Create the 'this' argument for the function call - this.Visit(methodCall.ThisArgument); - inexpr.Add(this.TranslatedExpressions.Pop()); - #endregion - - Dictionary p2eMap = new Dictionary(); - IEnumerator 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(); + List inexpr; + List outvars; + Bpl.IdentifierExpr thisExpr; + List locals; + List args; + Bpl.Expr arrayExpr; + Bpl.Expr indexExpr; + Dictionary 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 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; -- cgit v1.2.3