Merge

6 files changed, 362 insertions, 73 deletions

diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index 86fc4a5d..e4575480 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -32,6 +32,7 @@
     <UseApplicationTrust>false</UseApplicationTrust>

     <BootstrapperEnabled>true</BootstrapperEnabled>

     <TargetFrameworkProfile />

+    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

     <DebugSymbols>true</DebugSymbols>

@@ -41,7 +42,7 @@
     <DefineConstants>DEBUG;TRACE</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

-    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

     <CodeContractsCustomRewriterAssembly>

     </CodeContractsCustomRewriterAssembly>

     <CodeContractsCustomRewriterClass>

@@ -67,6 +68,15 @@
     <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

     <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

     <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

     <DebugType>pdbonly</DebugType>

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 29c0033f..77050c46 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -138,6 +138,16 @@ namespace BytecodeTranslator
     }

 

     public override void Visit(IArrayIndexer arrayIndexer) {

+

+#if EXPERIMENTAL

+      if (!IsAtomicInstance(arrayIndexer.IndexedObject)) {

+        // Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.

+        var se = ExpressionSimplifier.Simplify(this.sink, arrayIndexer);

+        this.Visit(se);

+        return;

+      }

+#endif

+

       this.Visit(arrayIndexer.IndexedObject);

       Bpl.Expr arrayExpr = TranslatedExpressions.Pop();

       this.Visit(arrayIndexer.Indices);

@@ -155,6 +165,9 @@ namespace BytecodeTranslator
         indexExpr = new Bpl.NAryExpr(arrayIndexer.Token(), new Bpl.FunctionCall(f), new Bpl.ExprSeq(indexExprs));

       }

 

+#if EXPERIMENTAL

+      this.TranslatedExpressions.Push(arrayExpr);

+#else

       Bpl.IdentifierExpr temp = Bpl.Expr.Ident(this.sink.CreateFreshLocal(arrayIndexer.Type));

       Bpl.Expr selectExpr = sink.Heap.ReadHeap(arrayExpr, indexExpr, AccessType.Array, temp.Type);

       this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(temp, selectExpr));

@@ -162,10 +175,22 @@ namespace BytecodeTranslator
 

       this.arrayExpr = arrayExpr;

       this.indexExpr = indexExpr;

+#endif

     }

 

     public override void Visit(ITargetExpression targetExpression)

     {

+#if EXPERIMENTAL

+      Contract.Assume(false, "The expression containing this as a subexpression should never allow a call to this routine.");

+

+      if (targetExpression.Instance != null && !IsAtomicInstance(targetExpression.Instance)) {

+        //// Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.

+        var se = ExpressionSimplifier.Simplify(this.sink, targetExpression);

+        this.Visit(se);

+        return;

+      }

+#endif

+

       #region ArrayIndexer

       IArrayIndexer/*?*/ indexer = targetExpression.Definition as IArrayIndexer;

       if (indexer != null)

@@ -252,11 +277,14 @@ namespace BytecodeTranslator
 

     public override void Visit(IBoundExpression boundExpression)

     {

-      //if (boundExpression.Instance != null)

-      //{

-      //    this.Visit(boundExpression.Instance);

-      //    // TODO: (mschaef) look where it's bound and do something

-      //}

+

+      if (boundExpression.Instance != null && !IsAtomicInstance(boundExpression.Instance)) {

+        // Simplify the BE so that all nested dereferences and method calls are broken up into separate assignments to locals.

+        var se = ExpressionSimplifier.Simplify(this.sink, boundExpression);

+        this.Visit(se);

+        return;

+      }

+

       #region Local

       ILocalDefinition local = boundExpression.Definition as ILocalDefinition;

       if (local != null)

@@ -290,9 +318,9 @@ namespace BytecodeTranslator
           }

           else {

             Bpl.Expr instanceExpr = TranslatedExpressions.Pop();

-            Bpl.IdentifierExpr temp = Bpl.Expr.Ident(this.sink.CreateFreshLocal(field.ResolvedField.Type));

-            this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(temp, this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, temp.Type)));

-            TranslatedExpressions.Push(temp);

+            var bplType = this.sink.CciTypeToBoogie(field.Type);

+            var e = this.sink.Heap.ReadHeap(instanceExpr, f, field.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, bplType);

+            this.TranslatedExpressions.Push(e);

           }

         }

         return;

@@ -339,6 +367,14 @@ namespace BytecodeTranslator
       #endregion

     }

 

+    internal static bool IsAtomicInstance(IExpression expression) {

+      var thisInst = expression as IThisReference;

+      if (thisInst != null) return true;

+      var be = expression as IBoundExpression;

+      if (be == null) return false;

+      return be.Instance == null;

+    }

+

     public override void Visit(IPopValue popValue) {

       var locExpr = this.StmtTraverser.operandStack.Pop();

       this.TranslatedExpressions.Push(locExpr);

@@ -604,6 +640,7 @@ namespace BytecodeTranslator
     private Bpl.Expr arrayExpr = null;

     private Bpl.Expr indexExpr = null;

 

+#if EXPERIMENTAL

     /// <summary>

     /// 

     /// </summary>

@@ -612,9 +649,108 @@ namespace BytecodeTranslator
     public override void Visit(IAssignment assignment) {

       Contract.Assert(TranslatedExpressions.Count == 0);

 

+      var tok = assignment.Token();

+

+      object container = assignment.Target.Definition;

+

+      var/*?*/ local = container as ILocalDefinition;

+      if (local != null) {

+        Contract.Assume(assignment.Target.Instance == null);

+        this.Visit(assignment.Source);

+        var e = this.TranslatedExpressions.Pop();

+        var bplLocal = Bpl.Expr.Ident(this.sink.FindOrCreateLocalVariable(local));

+        StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, bplLocal, e));

+        return;

+      }

+

+      var/*?*/ parameter = container as IParameterDefinition;

+      if (parameter != null) {

+        Contract.Assume(assignment.Target.Instance == null);

+        this.Visit(assignment.Source);

+        var e = this.TranslatedExpressions.Pop();

+        var bplParam = Bpl.Expr.Ident(this.sink.FindParameterVariable(parameter, this.contractContext));

+        StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, bplParam, e));

+        return;

+      }

+

+      var/*?*/ field = container as IFieldReference;

+      if (field != null) {

+        this.Visit(assignment.Source);

+        var e = this.TranslatedExpressions.Pop();

+        var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field));

+        if (assignment.Target.Instance == null) {

+          // static fields are not kept in the heap

+          StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, f, e));

+        } else {

+          if (field.ContainingType.ResolvedType.IsStruct) {

+            //var s_prime = this.sink.CreateFreshLocal(this.sink.Heap.StructType);

+            //var s_prime_expr = Bpl.Expr.Ident(s_prime);

+            //var boogieType = sink.CciTypeToBoogie(field.Type);

+            //StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, s_prime_expr, f, e,

+            //  field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,

+            //  boogieType));

+            UpdateStruct(tok, assignment.Target.Instance, field, e);

+          } else {

+            this.Visit(assignment.Target.Instance);

+            var x = this.TranslatedExpressions.Pop();

+            var boogieType = sink.CciTypeToBoogie(field.Type);

+            StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, x, f, e,

+              field.ResolvedField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap,

+              boogieType));

+          }

+        }

+        return;

+      }

+

+      var/*?*/ arrayIndexer = container as IArrayIndexer;

+      if (arrayIndexer != null) {

+        this.Visit(assignment.Target.Instance);

+        var x = this.TranslatedExpressions.Pop();

+        this.Visit(arrayIndexer.Indices);

+        var indices_prime = this.TranslatedExpressions.Pop();

+        this.Visit(assignment.Source);

+        var e = this.TranslatedExpressions.Pop();

+        StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, x, indices_prime, e, AccessType.Array, sink.CciTypeToBoogie(arrayIndexer.Type)));

+        return;

+      }

+

+      Contract.Assume(false);

+    }

+

+    private void UpdateStruct(Bpl.IToken tok, IExpression iExpression, IFieldReference field, Bpl.Expr e) {

+      var addrOf = iExpression as IAddressOf;

+      if (addrOf == null) return;

+      var addressableExpression = addrOf.Expression as IAddressableExpression;

+      if (addressableExpression == null) return;

+

+      var f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(field));

+

+      if (addressableExpression.Instance == null) {

+        var boogieType = sink.CciTypeToBoogie(field.Type);

+        this.Visit(addressableExpression);

+        var def = this.TranslatedExpressions.Pop();

+        StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, def, f, e,

+          AccessType.Struct,

+          boogieType));

+      } else {

+        var s_prime = this.sink.CreateFreshLocal(this.sink.Heap.StructType);

+        var s_prime_expr = Bpl.Expr.Ident(s_prime);

+        var boogieType = sink.CciTypeToBoogie(field.Type);

+        StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(tok, s_prime_expr, f, e,

+          AccessType.Struct,

+          boogieType));

+        UpdateStruct(tok, addressableExpression.Instance, addressableExpression.Definition as IFieldReference, s_prime_expr);

+      }

+    }

+

+#else

+

+    public override void Visit(IAssignment assignment) {

+      Contract.Assert(TranslatedExpressions.Count == 0);

+

       #region Transform Right Hand Side ...

       this.Visit(assignment.Source);

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

+      var sourceexp = this.TranslatedExpressions.Pop();

       #endregion

 

       // Simplify the LHS so that all nested dereferences and method calls are broken

@@ -643,8 +779,7 @@ namespace BytecodeTranslator
         Bpl.IdentifierExpr f = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(fieldReference.ResolvedField));

         if (target.Instance == null) {

           StmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(assignment.Token(), f, sourceexp));

-        }

-        else {

+        } else {

           Debug.Assert(args != null);

           List<Bpl.Variable> locals = new List<Bpl.Variable>();

           Bpl.IdentifierExpr instanceExpr = TranslatedExpressions.Pop() as Bpl.IdentifierExpr;

@@ -715,6 +850,8 @@ namespace BytecodeTranslator
       return;

     }

 

+#endif

+

     #endregion

 

     #region Translate Object Creation

@@ -1161,74 +1298,123 @@ namespace BytecodeTranslator
     }

     #endregion

 

+    public override void Visit(IBlockExpression blockExpression) {

+      this.StmtTraverser.Visit(blockExpression.BlockStatement);

+      this.Visit(blockExpression.Expression);

+    }

+

     /// <summary>

     /// This is a rewriter so it must be used on a mutable Code Model!!!

     /// </summary>

-    private class AssignmentSimplifier : CodeRewriter {

+    private class ExpressionSimplifier : CodeRewriter {

 

       Sink sink;

-      private List<IStatement> localDeclarations = new List<IStatement>();

 

-      private AssignmentSimplifier(Sink sink)

+      private ExpressionSimplifier(Sink sink)

         : base(sink.host) {

         this.sink = sink;

       }

 

-      public static IBlockExpression Simplify(Sink sink, ITargetExpression targetExpression) {

-        var a = new AssignmentSimplifier(sink);

-        var leftOverExpression = a.Rewrite(targetExpression);

-        return new BlockExpression() {

-          BlockStatement = new BlockStatement() { Statements = a.localDeclarations, },

-          Expression = leftOverExpression,

-          Type = targetExpression.Type,

-        };

+      public static IExpression Simplify(Sink sink, IExpression expression) {

+        var a = new ExpressionSimplifier(sink);

+        return a.Rewrite(expression);

       }

 

       public override IExpression Rewrite(IBoundExpression boundExpression) {

-        if (boundExpression.Instance == null)

-          return base.Rewrite(boundExpression); // REVIEW: Maybe just stop the rewriting and return boundExpression?

-        var e = base.Rewrite(boundExpression);

-        boundExpression = e as IBoundExpression;

-        if (boundExpression == null) return e;

+

+        if (ExpressionTraverser.IsAtomicInstance(boundExpression.Instance)) return boundExpression;

+

+        // boundExpression == BE(inst, def), i.e., inst.def

+        // return { loc := e; [assert loc != null;] | BE(BE(null,loc), def) }, i.e., "loc := e; loc.def"

+        //   where e is the rewritten inst

+

+        var e = base.Rewrite(boundExpression.Instance);

+

         var loc = new LocalDefinition() {

-          Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()), // TODO: should make the name unique within the method containing the assignment

+          Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()),

           Type = boundExpression.Type,

         };

-        this.localDeclarations.Add(

-          new LocalDeclarationStatement() {

-            InitialValue = boundExpression,

-            LocalVariable = loc,

-          }

-          );

-        return new BoundExpression() {

-          Definition = loc,

-          Instance = null,

-          Type = boundExpression.Type,

+        var locDecl = new LocalDeclarationStatement() {

+          InitialValue = e,

+          LocalVariable = loc,

         };

+        return new BlockExpression() {

+          BlockStatement = new BlockStatement() {

+            Statements = new List<IStatement> { locDecl },

+          },

+          Expression = new BoundExpression() {

+            Definition = boundExpression.Definition,

+            Instance = new BoundExpression() {

+              Definition = loc,

+              Instance = null,

+              Type = loc.Type,

+            },

+            Type = boundExpression.Type,

+          },

+        };

+

       }

 

-      public override IExpression Rewrite(IMethodCall methodCall) {

+      public override IExpression Rewrite(IArrayIndexer arrayIndexer) {

+        if (ExpressionTraverser.IsAtomicInstance(arrayIndexer.IndexedObject)) return arrayIndexer;

 

-        var e = base.Rewrite(methodCall); // simplify anything deeper in the tree

-        methodCall = e as IMethodCall;

-        if (methodCall == null) return e;

+        // arrayIndexer == AI(inst, [index]), i.e., inst[index0, index1,...]

+        // return { loc := e; [assert loc != null;] | AI(BE(null,loc), [index]) }

+        //   where e is the rewritten array instance

+

+        var e = base.Rewrite(arrayIndexer.IndexedObject);

 

         var loc = new LocalDefinition() {

-          Name = this.host.NameTable.GetNameFor("_loc"), // TODO: should make the name unique within the method containing the assignment

-          Type = methodCall.Type,

+          Name = this.host.NameTable.GetNameFor("_loc" + this.sink.LocalCounter.ToString()),

+          Type = arrayIndexer.Type,

         };

-        this.localDeclarations.Add(

-          new LocalDeclarationStatement() {

-            InitialValue = methodCall,

-            LocalVariable = loc,

-          }

-          );

-        return new BoundExpression() {

-          Definition = loc,

-          Instance = null,

-          Type = methodCall.Type,

+        var locDecl = new LocalDeclarationStatement() {

+          InitialValue = e,

+          LocalVariable = loc,

+        };

+        return new BlockExpression() {

+          BlockStatement = new BlockStatement() {

+            Statements = new List<IStatement> { locDecl },

+          },

+          Expression = new ArrayIndexer() {

+            IndexedObject = new BoundExpression() {

+              Definition = loc,

+              Instance = null,

+              Type = loc.Type,

+            },

+            Indices = new List<IExpression>(arrayIndexer.Indices),

+            Type = arrayIndexer.Type,

+          },

         };

       }

+

+      public override ITargetExpression Rewrite(ITargetExpression targetExpression) {

+        Contract.Assume(false, "The expression containing this as a subexpression should never allow a call to this routine.");

+        return null;

+      }

+

+      //public override IExpression Rewrite(IMethodCall methodCall) {

+

+      //  var e = base.Rewrite(methodCall); // simplify anything deeper in the tree

+      //  methodCall = e as IMethodCall;

+      //  if (methodCall == null) return e;

+

+      //  var loc = new LocalDefinition() {

+      //    Name = this.host.NameTable.GetNameFor("_loc"), // TODO: should make the name unique within the method containing the assignment

+      //    Type = methodCall.Type,

+      //  };

+      //  this.localDeclarations.Add(

+      //    new LocalDeclarationStatement() {

+      //      InitialValue = methodCall,

+      //      LocalVariable = loc,

+      //    }

+      //    );

+      //  return new BoundExpression() {

+      //    Definition = loc,

+      //    Instance = null,

+      //    Type = methodCall.Type,

+      //  };

+      //}

     }

   }

 

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 58bec27f..b1be6294 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -46,7 +46,12 @@ namespace BytecodeTranslator {
     }

 

     public override void Visit(IAssembly assembly) {

-      base.Visit(assembly);

+      this.sink.BeginAssembly(assembly);

+      try {

+        base.Visit(assembly);

+      } finally {

+        this.sink.EndAssembly(assembly);

+      }

     }

 

     /// <summary>

@@ -55,6 +60,9 @@ namespace BytecodeTranslator {
     /// 

     public override void Visit(ITypeDefinition typeDefinition) {

 

+      var savedPrivateTypes = this.privateTypes;

+      this.privateTypes = new List<ITypeDefinition>();

+

       if (typeDefinition.IsClass) {

         bool savedSawCctor = this.sawCctor;

         this.sawCctor = false;

@@ -80,7 +88,12 @@ namespace BytecodeTranslator {
           TypeHelper.GetTypeName(typeDefinition));

         throw new NotImplementedException(String.Format("Unknown kind of type definition '{0}'.", TypeHelper.GetTypeName(typeDefinition)));

       }

+      this.Visit(typeDefinition.PrivateHelperMembers);

+      foreach (var t in this.privateTypes) {

+        this.Visit(t);

+      }

     }

+    List<ITypeDefinition> privateTypes = new List<ITypeDefinition>();

 

     private void CreateDefaultStructConstructor(ITypeDefinition typeDefinition) {

       Contract.Requires(typeDefinition.IsStruct);

@@ -256,7 +269,11 @@ namespace BytecodeTranslator {
         #endregion

 

         #region Translate body

-        method.Body.Dispatch(stmtTraverser);

+        var helperTypes = stmtTraverser.TranslateMethod(method);

+        if (helperTypes != null) {

+          this.privateTypes.AddRange(helperTypes);

+        }

+        //method.Body.Dispatch(stmtTraverser);

         #endregion

 

         #region Create Local Vars For Implementation

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index f42c34d9..471b3431 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -132,12 +132,19 @@ namespace BytecodeTranslator {
           var copier = new CodeDeepCopier(host);

           var mutableModule = copier.Copy(module);

 

-          var mutator = new ReparentModule(host,

-            TypeHelper.GetDefiningUnit(host.PlatformType.SystemObject.ResolvedType),

-            mutableModule);

-          module = mutator.Rewrite(mutableModule);

+          var mscorlib = TypeHelper.GetDefiningUnit(host.PlatformType.SystemObject.ResolvedType);

+

+          //var mutator = new ReparentModule(host, mscorlib, mutableModule);

+          //module = mutator.Rewrite(mutableModule);

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

+

+          RewriteUnitReferences renamer = new RewriteUnitReferences(host, mutableModule);

+          var mscorlibAssembly = (IAssembly)mscorlib;

+          renamer.targetAssembly = mscorlibAssembly;

+          renamer.originalAssemblyIdentity = mscorlibAssembly.AssemblyIdentity;

+          renamer.RewriteChildren(mutableModule);

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

 

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

         }

       }

       if (modules.Count == 0) {

@@ -340,6 +347,34 @@ namespace BytecodeTranslator {
         // Maybe this is a good place to add the procedure to the toplevel declarations

       }

     }

+

+    private class RewriteUnitReferences : MetadataRewriter {

+      private UnitIdentity sourceUnitIdentity = null;

+      internal IAssembly/*?*/ targetAssembly = null;

+      internal AssemblyIdentity/*?*/ originalAssemblyIdentity = null;

+

+      Dictionary<uint, bool> internedKeys = new Dictionary<uint, bool>();

+

+      public RewriteUnitReferences(IMetadataHost host, Module sourceUnit)

+        : base(host) {

+        this.sourceUnitIdentity = sourceUnit.UnitIdentity;

+        }

+

+      public override IModuleReference Rewrite(IModuleReference moduleReference) {

+        if (this.sourceUnitIdentity.Equals(moduleReference.UnitIdentity)) {

+          return this.targetAssembly;

+        }

+        return base.Rewrite(moduleReference);

+      }

+      public override IAssemblyReference Rewrite(IAssemblyReference assemblyReference) {

+        if (this.sourceUnitIdentity.Equals(assemblyReference.UnitIdentity)) {

+          return this.targetAssembly;

+        }

+        return base.Rewrite(assemblyReference);

+      }

+

+    }

+

   }

 

 }

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index b8d8334d..852c3986 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -118,7 +118,7 @@ namespace BytecodeTranslator {
         return heap.StructType;

       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) 

+      else if (type is IGenericTypeParameter)

         return heap.BoxType;

       else

         return heap.RefType;

@@ -167,7 +167,9 @@ namespace BytecodeTranslator {
       Bpl.IToken tok = local.Token();

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

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

-        v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, local.Name.Value, t));

+        var name = local.Name.Value;

+        name = TranslationHelper.TurnStringIntoValidIdentifier(name);

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

         localVarMap.Add(local, v);

       }

       return v;

@@ -334,6 +336,7 @@ namespace BytecodeTranslator {
       ProcedureInfo procAndFormalMap;

 

       var key = method.InternedKey;

+

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

 

         string MethodName = TranslationHelper.CreateUniqueMethodName(method);

@@ -375,7 +378,7 @@ namespace BytecodeTranslator {
         Bpl.Formal selfOut = null;

         #region Create 'this' parameter

         if (!method.IsStatic) {

-          Bpl.Type selfType = CciTypeToBoogie(method.ContainingType);

+          var selfType = CciTypeToBoogie(method.ContainingType);

           if (method.ContainingType.ResolvedType.IsStruct) {

             //selfType = Heap.StructType;

             in_count++;

@@ -470,15 +473,16 @@ namespace BytecodeTranslator {
 

         #endregion

 

+        var tok = method.Token();

         Bpl.DeclWithFormals decl;

         if (IsPure(method)) {

-          var func = new Bpl.Function(method.Token(),

+          var func = new Bpl.Function(tok,

             MethodName,

             new Bpl.VariableSeq(invars),

             this.RetVariable);

           decl = func;

         } else {

-          var proc = new Bpl.Procedure(method.Token(),

+          var proc = new Bpl.Procedure(tok,

               MethodName,

               new Bpl.TypeVariableSeq(),

               new Bpl.VariableSeq(invars),

@@ -488,7 +492,10 @@ namespace BytecodeTranslator {
               boogiePostcondition);

           decl = proc;

         }

-

+        if (!TypeHelper.GetDefiningUnitReference(method.ContainingType).UnitIdentity.Equals(this.assemblyBeingTranslated.UnitIdentity)) {

+          var attrib = new Bpl.QKeyValue(tok, "extern", new List<object>(1), null);

+          decl.Attributes = attrib;

+        }

 

         string newName = null;

         if (IsStubMethod(method, out newName)) {

@@ -573,7 +580,8 @@ namespace BytecodeTranslator {
 

     public ProcedureInfo FindOrCreateProcedureAndReturnProcAndFormalMap(IMethodDefinition method) {

       this.FindOrCreateProcedure(method);

-      return this.declaredMethods[method.InternedKey];

+      var key = method.InternedKey;

+      return this.declaredMethods[key];

     }

     public static IMethodReference Unspecialize(IMethodReference method) {

       IMethodReference result = method;

@@ -634,6 +642,15 @@ namespace BytecodeTranslator {
       this.localCounter = 0;

     }

 

+    public void BeginAssembly(IAssembly assembly) {

+      this.assemblyBeingTranslated = assembly;

+    }

+

+    public void EndAssembly(IAssembly assembly) {

+      this.assemblyBeingTranslated = null;

+    }

+    private IAssembly assemblyBeingTranslated;

+

     public Dictionary<ITypeDefinition, HashSet<IMethodDefinition>> delegateTypeToDelegates = new Dictionary<ITypeDefinition, HashSet<IMethodDefinition>>();

 

     public void AddDelegate(ITypeDefinition type, IMethodDefinition defn)

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 24b4b2ca..0e13c510 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -50,13 +50,37 @@ namespace BytecodeTranslator
       return etrav.TranslatedExpressions.Pop();

     }

 

+    public ICollection<ITypeDefinition>/*?*/ TranslateMethod(IMethodDefinition method) {

+      var methodBody = method.Body as ISourceMethodBody;

+      if (methodBody == null) return null;

+      var block = methodBody.Block as BlockStatement;

+      // TODO: Error if cast fails?

+

+      ICollection<ITypeDefinition> newTypes = null;

+      if (block != null) {

+        var remover = new AnonymousDelegateRemover(this.sink.host, this.PdbReader);

+        newTypes = remover.RemoveAnonymousDelegates(methodBody.MethodDefinition, block);

+      }

+      this.Visit(methodBody);

+      return newTypes;

+    }

+

     #endregion

 

-    public override void Visit(IBlockStatement block) {

-      Bpl.StmtListBuilder slb = new Bpl.StmtListBuilder();

+    //public override void Visit(ISourceMethodBody methodBody) {

+    //  var block = methodBody.Block as BlockStatement;

+    //  // TODO: Error if cast fails?

+

+    //  if (block != null) {

+    //    var remover = new AnonymousDelegateRemover(this.sink.host, this.PdbReader);

+    //    var newTypes = remover.RemoveAnonymousDelegates(methodBody.MethodDefinition, block);

+    //  }

+    //  base.Visit(methodBody);

+    //}

 

-      foreach (IStatement st in block.Statements) {

-        this.Visit(st);

+    public override void Visit(IBlockStatement block) {

+      foreach (var s in block.Statements) {

+        this.Visit(s);

       }

     }