(bct) skeleton of plugin infrastructure. for now the code is essentially the same

I will open a plugin branch to make more deeper changes until everything is stable

18 files changed, 531 insertions, 73 deletions

diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index ff49e4c3..3ddd4e43 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -121,6 +121,8 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

+    <Compile Include="TranslationPlugins\PhoneTranslator\PhoneFeedbackPlugin.cs" />

+    <Compile Include="TranslationPlugins\Translators\BaseTranslator.cs" />

     <Compile Include="CLRSemantics.cs" />

     <Compile Include="Heap.cs" />

     <Compile Include="HeapFactory.cs" />

@@ -139,9 +141,12 @@
     <Compile Include="TranslationException.cs" />

     <Compile Include="TranslationHelper.cs" />

     <Compile Include="TranslationPlugins\BytecodeTranslator\BytecodeTranslatorPlugin.cs" />

-    <Compile Include="TranslationPlugins\IContractAwareTranslator.cs" />

+    <Compile Include="TranslationPlugins\ContractAwareTranslator.cs" />

     <Compile Include="TranslationPlugins\ITranslationPlugin.cs" />

-    <Compile Include="TranslationPlugins\ITranslator.cs" />

+    <Compile Include="TranslationPlugins\PhoneTranslator\PhoneInitializationPlugin.cs" />

+    <Compile Include="TranslationPlugins\Translator.cs" />

+    <Compile Include="TranslationPlugins\Translators\PhoneFeedbackTranslator.cs" />

+    <Compile Include="TranslationPlugins\Translators\PhoneInitializationTranslator.cs" />

     <Compile Include="TraverserFactory.cs" />

     <Compile Include="WholeProgram.cs" />

   </ItemGroup>

diff --git a/BCT/BytecodeTranslator/CLRSemantics.cs b/BCT/BytecodeTranslator/CLRSemantics.cs
index 55f0cd46..ddf85c6f 100644
--- a/BCT/BytecodeTranslator/CLRSemantics.cs
+++ b/BCT/BytecodeTranslator/CLRSemantics.cs
@@ -15,11 +15,17 @@ using Microsoft.Cci.Contracts;
 using Microsoft.Cci.ILToCodeModel;

 

 using Bpl = Microsoft.Boogie;

+using BytecodeTranslator.TranslationPlugins;

 

 namespace BytecodeTranslator {

 

   public class CLRSemantics : TraverserFactory {

 

+    public override Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {

+      Translator translator = new BaseTranslator(this, sink, contractProviders, pdbReaders);

+      return translator;

+    }

+

     public override ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {

       return new CLRExpressionSemantics(sink, statementTraverser, contractContext);

     }

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index ff2c6095..fcbc4e99 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -69,6 +69,7 @@ namespace BytecodeTranslator {
     public override Bpl.Variable CreateFieldVariable(IFieldReference field) {

       Bpl.Variable v;

       string fieldname = MemberHelper.GetMemberSignature(field, NameFormattingOptions.DocumentationId);

+      

       fieldname = TranslationHelper.TurnStringIntoValidIdentifier(fieldname);

       Bpl.IToken tok = field.Token();

       Bpl.Type t = this.sink.CciTypeToBoogie(field.Type.ResolvedType);

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index e4a81eb8..124726e6 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -27,22 +27,65 @@ namespace BytecodeTranslator {
   /// Responsible for traversing all metadata elements (i.e., everything exclusive

   /// of method bodies).

   /// </summary>

-  public class MetadataTraverser : BaseMetadataTraverser, ITranslator {

+  public class MetadataTraverser : BaseMetadataTraverser {

 

     readonly Sink sink;

-

-    public readonly TraverserFactory factory;

+    public readonly TraverserFactory Factory;

 

     public readonly IDictionary<IUnit, PdbReader> PdbReaders;

     public PdbReader/*?*/ PdbReader;

 

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

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

       : base() {

       this.sink = sink;

-      this.factory = sink.Factory;

+      this.Factory = factory;

       this.PdbReaders = pdbReaders;

     }

 

+    public IEnumerable<Bpl.Requires> getPreconditionTranslation(IMethodContract contract) {

+      ICollection<Bpl.Requires> translatedPres = new List<Bpl.Requires>();

+      foreach (IPrecondition pre in contract.Preconditions) {

+        var stmtTraverser = this.Factory.MakeStatementTraverser(sink, null, true);

+        ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, stmtTraverser, true);

+        exptravers.Visit(pre.Condition); // TODO

+        // Todo: Deal with Descriptions

+        var req = new Bpl.Requires(pre.Token(), false, exptravers.TranslatedExpressions.Pop(), "");

+        translatedPres.Add(req);

+      }

+

+      return translatedPres;

+    }

+

+    public IEnumerable<Bpl.Ensures> getPostconditionTranslation(IMethodContract contract) {

+      ICollection<Bpl.Ensures> translatedPosts = new List<Bpl.Ensures>();

+      foreach (IPostcondition post in contract.Postconditions) {

+        var stmtTraverser = this.Factory.MakeStatementTraverser(sink, null, true);

+        ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, stmtTraverser, true);

+        exptravers.Visit(post.Condition);

+        // Todo: Deal with Descriptions

+        var ens = new Bpl.Ensures(post.Token(), false, exptravers.TranslatedExpressions.Pop(), "");

+        translatedPosts.Add(ens);

+      }

+

+      return translatedPosts;

+    }

+

+    public IEnumerable<Bpl.IdentifierExpr> getModifiedIdentifiers(IMethodContract contract) {

+      ICollection<Bpl.IdentifierExpr> modifiedExpr = new List<Bpl.IdentifierExpr>();

+      foreach (IAddressableExpression mod in contract.ModifiedVariables) {

+        ExpressionTraverser exptravers = this.Factory.MakeExpressionTraverser(sink, null, true);

+        exptravers.Visit(mod);

+        Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;

+        if (idexp == null) {

+          throw new TranslationException(String.Format("Cannot create IdentifierExpr for Modifyed Variable {0}", mod.ToString()));

+        }

+        modifiedExpr.Add(idexp);

+      }

+

+      return modifiedExpr;

+    }

+

+

     #region Overrides

 

     public override void Visit(IModule module) {

@@ -136,7 +179,7 @@ namespace BytecodeTranslator {
       if (PhoneCodeHelper.instance().PhonePlugin != null && typeDef.isPhoneApplicationPageClass(sink.host)) {

         IEnumerable<ControlInfoStructure> pageCtrls= PhoneCodeHelper.instance().PhonePlugin.getControlsForPage(typeDef.ToString());

         foreach (ControlInfoStructure ctrlInfo in pageCtrls) {

-          if (ctrlInfo.Name.Contains(PhoneControlsPlugin.BOOGIE_DUMMY_CONTROL)) {

+          if (ctrlInfo.Name.Contains(PhoneControlsPlugin.BOOGIE_DUMMY_CONTROL) || ctrlInfo.Name == Dummy.Name.Value) {

             string anonymousControlName = ctrlInfo.Name;

             IFieldDefinition fieldDef = new FieldDefinition() {

               ContainingTypeDefinition = typeDef,

@@ -152,7 +195,7 @@ namespace BytecodeTranslator {
         }

       }

     }

-     * */

+     */ 

 

     private void CreateDefaultStructConstructor(ITypeDefinition typeDefinition) {

       Contract.Requires(typeDefinition.IsStruct);

@@ -160,7 +203,7 @@ namespace BytecodeTranslator {
       var proc = this.sink.FindOrCreateProcedureForDefaultStructCtor(typeDefinition);

 

       this.sink.BeginMethod(typeDefinition);

-      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

+      var stmtTranslator = this.Factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

       var stmts = new List<IStatement>();

 

       foreach (var f in typeDefinition.Fields) {

@@ -263,7 +306,7 @@ namespace BytecodeTranslator {
 

       this.sink.BeginMethod(typeDefinition);

 

-      var stmtTranslator = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

+      var stmtTranslator = this.Factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

       var stmts = new List<IStatement>();

 

       foreach (var f in typeDefinition.Fields) {

@@ -343,7 +386,7 @@ namespace BytecodeTranslator {
       }

 

       try {

-        StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

+        StatementTraverser stmtTraverser = this.Factory.MakeStatementTraverser(this.sink, this.PdbReader, false);

 

         // FEEDBACK if this is a feedback method it will be plagued with false asserts. They will trigger if $Exception becomes other than null

         // FEEDBACK for modular analysis we need it to be non-null at the start

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index fc48f4c7..3a89a3da 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -23,6 +23,7 @@ using BytecodeTranslator.Phone;
 using System.Text.RegularExpressions;

 using BytecodeTranslator.TranslationPlugins;

 using BytecodeTranslator.TranslationPlugins.BytecodeTranslator;

+using BytecodeTranslator.TranslationPlugins.PhoneTranslator;

 

 namespace BytecodeTranslator {

 

@@ -255,23 +256,52 @@ namespace BytecodeTranslator {
       }

 

       var primaryModule = modules[0];

-      TraverserFactory bctTraverserFactory;

-      if (wholeProgram) {

-        bctTraverserFactory = new WholeProgram();

-      } else {

-        bctTraverserFactory = new CLRSemantics();

-      }

-

-      Sink sink= new Sink(host, bctTraverserFactory, heapFactory, options, exemptionList, whiteList);

+      Sink sink= new Sink(host, heapFactory, options, exemptionList, whiteList);

       TranslationHelper.tmpVarCounter = 0;

 

-      ITranslationPlugin bctPlugin= new BytecodeTranslatorPlugin();

-      ITranslator translator= bctPlugin.getTranslator(sink, contractExtractors, pdbReaders);

+      // TODO move away, get all plugin and translators from a config file or alike

+      #region Plugged translators

+      List<Translator> translatorsPlugged = new List<Translator>();      

+      ITranslationPlugin bctPlugin= new BytecodeTranslatorPlugin(wholeProgram);

+      Translator bcTranslator = bctPlugin.getTranslator(sink, contractExtractors, pdbReaders);

+      translatorsPlugged.Add(bcTranslator);

 

       if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {

+        // TODO this should be part of the translator initialziation

+        PhoneCodeHelper.initialize(host);

+        PhoneCodeHelper.instance().PhonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);

+

+        if (doPhoneNav) {

+          // TODO this should be part of the translator initialziation

+          PhoneCodeHelper.instance().PhoneNavigationToggled = true;

+

+          ITranslationPlugin phoneInitPlugin = new PhoneInitializationPlugin();

+          ITranslationPlugin phoneNavPlugin = new PhoneNavigationPlugin();

+          Translator phInitTranslator = phoneInitPlugin.getTranslator(sink, contractExtractors, pdbReaders);

+          Translator phNavTranslator = phoneNavPlugin.getTranslator(sink, contractExtractors, pdbReaders);

+          translatorsPlugged.Add(phInitTranslator);

+          translatorsPlugged.Add(phNavTranslator);

+        }

+

+        if (doPhoneFeedback) {

+          // TODO this should be part of the translator initialziation

+          PhoneCodeHelper.instance().PhoneFeedbackToggled = true;

+

+          ITranslationPlugin phoneFeedbackPlugin = new PhoneFeedbackPlugin();

+          Translator phFeedbackTranslator = phoneFeedbackPlugin.getTranslator(sink, contractExtractors, pdbReaders);

+          translatorsPlugged.Add(phFeedbackTranslator);

+        }

+      }

+      #endregion

+      sink.TranslationPlugins = translatorsPlugged;

+

+      /*

+      if (phoneControlsConfigFile != null && phoneControlsConfigFile != "") {

+        // TODO send this all way to initialization of phone plugin translator

         PhoneCodeHelper.initialize(host);

         PhoneCodeHelper.instance().PhonePlugin = new PhoneControlsPlugin(phoneControlsConfigFile);

         

+        // TODO these parameters will eventually form part of plugin configuration

         if (doPhoneNav) {

           PhoneCodeHelper.instance().PhoneNavigationToggled = true;

           PhoneInitializationMetadataTraverser initTr = new PhoneInitializationMetadataTraverser(host);

@@ -286,8 +316,17 @@ namespace BytecodeTranslator {
           fbMetaDataTraverser.Visit(modules);

         }

       }

-

-      translator.TranslateAssemblies(modules);

+      */

+

+      // TODO replace the whole translation by a translator initialization and an orchestrator calling back for each element

+      // TODO for the current BC translator it will possibly just implement onMetadataElement(IModule)

+      // TODO refactor this away, handle priorities between plugged translators

+      IOrderedEnumerable<Translator> prioritizedTranslators = translatorsPlugged.OrderBy(t => t.getPriority());

+      foreach (Translator t in prioritizedTranslators) {

+        t.initialize();

+        if (t.isOneShot())

+          t.TranslateAssemblies(modules);

+      }

 

       foreach (var pair in sink.delegateTypeToDelegates.Values) {

         CreateDispatchMethod(sink, pair.Item1, pair.Item2);

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index ea0b22c9..ea6e0878 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -17,27 +17,27 @@ using Microsoft.Cci.ILToCodeModel;
 using System.Diagnostics.Contracts;

 

 using Bpl = Microsoft.Boogie;

+using BytecodeTranslator.TranslationPlugins;

 

 

 namespace BytecodeTranslator {

 

   public class Sink {

 

-    public TraverserFactory Factory {

-      get { return this.factory; }

+    public IEnumerable<Translator> TranslationPlugins {

+      get { return this.translationPlugins; }

+      set { this.translationPlugins= value; }

     }

-    readonly TraverserFactory factory;

+    private IEnumerable<Translator> translationPlugins;

     private readonly Options options;

     readonly bool whiteList;

     readonly List<Regex> exemptionList;

 

-    public Sink(IContractAwareHost host, TraverserFactory factory, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {

+

+    public Sink(IContractAwareHost host, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {

       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.options = options;

       this.exemptionList = exemptionList;

@@ -630,35 +630,24 @@ namespace BytecodeTranslator {
 

         if (contract != null) {

           try {

-

-            foreach (IPrecondition pre in contract.Preconditions) {

-              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true);

-              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, stmtTraverser, true);

-              exptravers.Visit(pre.Condition); // TODO

-              // Todo: Deal with Descriptions

-              var req = new Bpl.Requires(pre.Token(), false, exptravers.TranslatedExpressions.Pop(), "");

-              boogiePrecondition.Add(req);

-            }

-

-            foreach (IPostcondition post in contract.Postconditions) {

-              var stmtTraverser = this.factory.MakeStatementTraverser(this, null, true);

-              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, stmtTraverser, true);

-              exptravers.Visit(post.Condition);

-              // Todo: Deal with Descriptions

-              var ens = new Bpl.Ensures(post.Token(), false, exptravers.TranslatedExpressions.Pop(), "");

-              boogiePostcondition.Add(ens);

-            }

-

-            foreach (IAddressableExpression mod in contract.ModifiedVariables) {

-              ExpressionTraverser exptravers = this.factory.MakeExpressionTraverser(this, null, true);

-              exptravers.Visit(mod);

-

-              Bpl.IdentifierExpr idexp = exptravers.TranslatedExpressions.Pop() as Bpl.IdentifierExpr;

-

-              if (idexp == null) {

-                throw new TranslationException(String.Format("Cannot create IdentifierExpr for Modifyed Variable {0}", mod.ToString()));

+            foreach (Translator translatorPlugin in translationPlugins) {

+              ContractAwareTranslator translator = translatorPlugin as ContractAwareTranslator;

+              if (translator != null) {

+                IEnumerable<Bpl.Requires> preConds = translator.getPreconditionTranslation(contract);

+                foreach (Bpl.Requires preExpr in preConds) {

+                  boogiePrecondition.Add(preExpr);

+                }

+

+                IEnumerable<Bpl.Ensures> ensures = translator.getPostconditionTranslation(contract);

+                foreach (Bpl.Ensures ensuring in ensures) {

+                  boogiePostcondition.Add(ensuring);

+                }

+

+                IEnumerable<Bpl.IdentifierExpr> modifiedExpr = translator.getModifiedIdentifiers(contract);

+                foreach (Bpl.IdentifierExpr ident in modifiedExpr) {

+                  boogieModifies.Add(ident);

+                }

               }

-              boogieModifies.Add(idexp);

             }

           }

           catch (TranslationException te) {

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index b6fc1dfd..40bc14b3 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -58,9 +58,9 @@ namespace BytecodeTranslator
     private static int captureStateCounter = 0;

 

     #region Constructors

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

+    public StatementTraverser(Sink sink, PdbReader/*?*/ pdbReader, bool contractContext, TraverserFactory factory) {

       this.sink = sink;

-      this.factory = sink.Factory;

+      this.factory = factory;

       PdbReader = pdbReader;

       this.contractContext = contractContext;

       this.captureState = sink.Options.captureState;

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs b/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs
index 425a9476..a7b00f63 100644
--- a/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs
+++ b/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs
@@ -6,11 +6,22 @@ using Microsoft.Cci;
 using Microsoft.Cci.Contracts;

 

 namespace BytecodeTranslator.TranslationPlugins.BytecodeTranslator {

-  class BytecodeTranslatorPlugin : ITranslationPlugin {

-    public ITranslator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {

-      // TODO take whole program options into account here

-      return new CLRSemantics().MakeMetadataTraverser(sink, contractProviders, pdbReaders);

-      // return new WholeProgram().MakeMetadataTraverser(sink, contractProviders, pdbReaders);

+  internal class BytecodeTranslatorPlugin : ITranslationPlugin {

+    private bool isWholeProgram = false;

+

+    public BytecodeTranslatorPlugin(Boolean isWholeProgram) {

+      this.isWholeProgram = isWholeProgram;

+    }

+

+    public Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {

+      TraverserFactory factory;

+      if (isWholeProgram)

+        factory= new WholeProgram();

+      else

+        factory= new CLRSemantics();

+      // Translator translator= factory.MakeMetadataTraverser(sink, contractProviders, pdbReaders);

+      Translator translator= factory.getTranslator(sink, contractProviders, pdbReaders);

+      return translator;

     }

   }

 }

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/ContractAwareTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/ContractAwareTranslator.cs
new file mode 100644
index 00000000..ceb8ca0a
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationPlugins/ContractAwareTranslator.cs
@@ -0,0 +1,15 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+using Bpl= Microsoft.Boogie;

+using Microsoft.Cci.Contracts;

+

+namespace BytecodeTranslator.TranslationPlugins {

+  public abstract class ContractAwareTranslator : Translator {

+    public virtual IEnumerable<Bpl.Requires> getPreconditionTranslation(IMethodContract contract) {return new List<Bpl.Requires>(); }

+    public virtual IEnumerable<Bpl.Ensures> getPostconditionTranslation(IMethodContract contract) { return new List<Bpl.Ensures>(); }

+    public virtual IEnumerable<Bpl.IdentifierExpr> getModifiedIdentifiers(IMethodContract contract) { return new List<Bpl.IdentifierExpr>(); }

+  }

+}

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/ITranslationPlugin.cs b/BCT/BytecodeTranslator/TranslationPlugins/ITranslationPlugin.cs
index c6157e49..9cf895fd 100644
--- a/BCT/BytecodeTranslator/TranslationPlugins/ITranslationPlugin.cs
+++ b/BCT/BytecodeTranslator/TranslationPlugins/ITranslationPlugin.cs
@@ -6,7 +6,7 @@ using Microsoft.Cci;
 using Microsoft.Cci.Contracts;

 

 namespace BytecodeTranslator.TranslationPlugins {

-  interface ITranslationPlugin {

-    ITranslator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractExtractors=null, IDictionary<IUnit, PdbReader> pdbReaders=null);

+  public interface ITranslationPlugin {

+    Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractExtractors=null, IDictionary<IUnit, PdbReader> pdbReaders=null);

   }

 }

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneFeedbackPlugin.cs b/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneFeedbackPlugin.cs
new file mode 100644
index 00000000..c6d9b24a
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneFeedbackPlugin.cs
@@ -0,0 +1,15 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Cci;

+using Microsoft.Cci.Contracts;

+using BytecodeTranslator.TranslationPlugins.Translators;

+

+namespace BytecodeTranslator.TranslationPlugins.PhoneTranslator {

+  class PhoneFeedbackPlugin : ITranslationPlugin {

+    public Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {

+      return new PhoneFeedbackTranslator(sink);

+    }

+  }

+}

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneInitializationPlugin.cs b/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneInitializationPlugin.cs
new file mode 100644
index 00000000..98282faa
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationPlugins/PhoneTranslator/PhoneInitializationPlugin.cs
@@ -0,0 +1,21 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Cci;

+using Microsoft.Cci.Contracts;

+using BytecodeTranslator.TranslationPlugins.Translators;

+

+namespace BytecodeTranslator.TranslationPlugins.PhoneTranslator {

+  class PhoneInitializationPlugin : ITranslationPlugin {

+    public Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {

+      return new PhoneInitializationTranslator(sink);

+    }

+  }

+

+  class PhoneNavigationPlugin : ITranslationPlugin {

+    public Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {

+      return new PhoneNavigationTranslator(sink);

+    }

+  }

+}

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translator.cs
new file mode 100644
index 00000000..60d7e2f6
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationPlugins/Translator.cs
@@ -0,0 +1,169 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Cci;

+

+namespace BytecodeTranslator.TranslationPlugins {

+  public abstract class Translator {

+    public abstract void initialize();

+    public abstract bool isOneShot();

+    public abstract int getPriority();

+

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

+

+    // Each plugged translator may choose to implement some action on each metadata / AST element

+    public virtual void onMetadataElement(IArrayTypeReference arrayTypeReference) { }

+    public virtual void onMetadataElement(IAssembly assembly) { }

+    public virtual void onMetadataElement(IAssemblyReference assemblyReference) { }

+    public virtual void onMetadataElement(ICustomAttribute customAttribute) { }

+    public virtual void onMetadataElement(ICustomModifier customModifier) { }

+    public virtual void onMetadataElement(IEventDefinition eventDefinition) { }

+    public virtual void onMetadataElement(IFieldDefinition fieldDefinition) { }

+    public virtual void onMetadataElement(IFieldReference fieldReference) { }

+    public virtual void onMetadataElement(IFileReference fileReference) { }

+    public virtual void onMetadataElement(IFunctionPointerTypeReference functionPointerTypeReference) { }

+    public virtual void onMetadataElement(IGenericMethodInstanceReference genericMethodInstanceReference) { }

+    public virtual void onMetadataElement(IGenericMethodParameter genericMethodParameter) { }

+    public virtual void onMetadataElement(IGenericMethodParameterReference genericMethodParameterReference) { }

+    public virtual void onMetadataElement(IGlobalFieldDefinition globalFieldDefinition) { }

+    public virtual void onMetadataElement(IGlobalMethodDefinition globalMethodDefinition) { }

+    public virtual void onMetadataElement(IGenericTypeInstanceReference genericTypeInstanceReference) { }

+    public virtual void onMetadataElement(IGenericTypeParameter genericTypeParameter) { }

+    public virtual void onMetadataElement(IGenericTypeParameterReference genericTypeParameterReference) { }

+    public virtual void onMetadataElement(ILocalDefinition localDefinition) { }

+    public virtual void onMetadataElement(IManagedPointerTypeReference managedPointerTypeReference) { }

+    public virtual void onMetadataElement(IMarshallingInformation marshallingInformation) { }

+    public virtual void onMetadataElement(IMetadataConstant constant) { }

+    public virtual void onMetadataElement(IMetadataCreateArray createArray) { }

+    public virtual void onMetadataElement(IMetadataExpression expression) { }

+    public virtual void onMetadataElement(IMetadataNamedArgument namedArgument) { }

+    public virtual void onMetadataElement(IMetadataTypeOf typeOf) { }

+    public virtual void onMetadataElement(IMethodBody methodBody) { }

+    public virtual void onMetadataElement(IMethodDefinition method) { }

+    public virtual void onMetadataElement(IMethodImplementation methodImplementation) { }

+    public virtual void onMetadataElement(IMethodReference methodReference) { }

+    public virtual void onMetadataElement(IModifiedTypeReference modifiedTypeReference) { }

+    public virtual void onMetadataElement(IModule module) { }

+    public virtual void onMetadataElement(IModuleReference moduleReference) { }

+    public virtual void onMetadataElement(INamespaceAliasForType namespaceAliasForType) { }

+    public virtual void onMetadataElement(INamespaceTypeDefinition namespaceTypeDefinition) { }

+    public virtual void onMetadataElement(INamespaceTypeReference namespaceTypeReference) { }

+    public virtual void onMetadataElement(INestedAliasForType nestedAliasForType) { }

+    public virtual void onMetadataElement(INestedTypeDefinition nestedTypeDefinition) { }

+    public virtual void onMetadataElement(INestedTypeReference nestedTypeReference) { }

+    public virtual void onMetadataElement(INestedUnitNamespace nestedUnitNamespace) { }

+    public virtual void onMetadataElement(INestedUnitNamespaceReference nestedUnitNamespaceReference) { }

+    public virtual void onMetadataElement(INestedUnitSetNamespace nestedUnitSetNamespace) { }

+    public virtual void onMetadataElement(IOperation operation) { }

+    public virtual void onMetadataElement(IOperationExceptionInformation operationExceptionInformation) { }

+    public virtual void onMetadataElement(IParameterDefinition parameterDefinition) { }

+    public virtual void onMetadataElement(IParameterTypeInformation parameterTypeInformation) { }

+    public virtual void onMetadataElement(IPESection peSection) { }

+    public virtual void onMetadataElement(IPlatformInvokeInformation platformInvokeInformation) { }

+    public virtual void onMetadataElement(IPointerTypeReference pointerTypeReference) { }

+    public virtual void onMetadataElement(IPropertyDefinition propertyDefinition) { }

+    public virtual void onMetadataElement(IResourceReference resourceReference) { }

+    public virtual void onMetadataElement(IRootUnitNamespace rootUnitNamespace) { }

+    public virtual void onMetadataElement(IRootUnitNamespaceReference rootUnitNamespaceReference) { }

+    public virtual void onMetadataElement(IRootUnitSetNamespace rootUnitSetNamespace) { }

+    public virtual void onMetadataElement(ISecurityAttribute securityAttribute) { }

+    public virtual void onMetadataElement(ISpecializedEventDefinition specializedEventDefinition) { }

+    public virtual void onMetadataElement(ISpecializedFieldDefinition specializedFieldDefinition) { }

+    public virtual void onMetadataElement(ISpecializedFieldReference specializedFieldReference) { }

+    public virtual void onMetadataElement(ISpecializedMethodDefinition specializedMethodDefinition) { }

+    public virtual void onMetadataElement(ISpecializedMethodReference specializedMethodReference) { }

+    public virtual void onMetadataElement(ISpecializedPropertyDefinition specializedPropertyDefinition) { }

+    public virtual void onMetadataElement(ISpecializedNestedTypeDefinition specializedNestedTypeDefinition) { }

+    public virtual void onMetadataElement(ISpecializedNestedTypeReference specializedNestedTypeReference) { }

+    public virtual void onMetadataElement(IUnitSet unitSet) { }

+    public virtual void onMetadataElement(IWin32Resource win32Resource) { }

+

+    public virtual void onASTElement(IAddition addition) { }

+    public virtual void onASTElement(IAddressableExpression addressableExpression) { }

+    public virtual void onASTElement(IAddressDereference addressDereference) { }

+    public virtual void onASTElement(IAddressOf addressOf) { }

+    public virtual void onASTElement(IAnonymousDelegate anonymousDelegate) { }

+    public virtual void onASTElement(IArrayIndexer arrayIndexer) { }

+    public virtual void onASTElement(IAssertStatement assertStatement) { }

+    public virtual void onASTElement(IAssignment assignment) { }

+    public virtual void onASTElement(IAssumeStatement assumeStatement) { }

+    public virtual void onASTElement(IBitwiseAnd bitwiseAnd) { }

+    public virtual void onASTElement(IBitwiseOr bitwiseOr) { }

+    public virtual void onASTElement(IBlockExpression blockExpression) { }

+    public virtual void onASTElement(IBlockStatement block) { }

+    public virtual void onASTElement(IBreakStatement breakStatement) { }

+    public virtual void onASTElement(IBoundExpression boundExpression) { }

+    public virtual void onASTElement(ICastIfPossible castIfPossible) { }

+    public virtual void onASTElement(ICatchClause catchClause) { }

+    public virtual void onASTElement(ICheckIfInstance checkIfInstance) { }

+    public virtual void onASTElement(ICompileTimeConstant constant) { }

+    public virtual void onASTElement(IConversion conversion) { }

+    public virtual void onASTElement(IConditional conditional) { }

+    public virtual void onASTElement(IConditionalStatement conditionalStatement) { }

+    public virtual void onASTElement(IContinueStatement continueStatement) { }

+    public virtual void onASTElement(ICreateArray createArray) { }

+    public virtual void onASTElement(ICreateDelegateInstance createDelegateInstance) { }

+    public virtual void onASTElement(ICreateObjectInstance createObjectInstance) { }

+    public virtual void onASTElement(IDebuggerBreakStatement debuggerBreakStatement) { }

+    public virtual void onASTElement(IDefaultValue defaultValue) { }

+    public virtual void onASTElement(IDivision division) { }

+    public virtual void onASTElement(IDoUntilStatement doUntilStatement) { }

+    public virtual void onASTElement(IDupValue dupValue) { }

+    public virtual void onASTElement(IEmptyStatement emptyStatement) { }

+    public virtual void onASTElement(IEquality equality) { }

+    public virtual void onASTElement(IExclusiveOr exclusiveOr) { }

+    public virtual void onASTElement(IExpressionStatement expressionStatement) { }

+    public virtual void onASTElement(IForEachStatement forEachStatement) { }

+    public virtual void onASTElement(IForStatement forStatement) { }

+    public virtual void onASTElement(IGotoStatement gotoStatement) { }

+    public virtual void onASTElement(IGotoSwitchCaseStatement gotoSwitchCaseStatement) { }

+    public virtual void onASTElement(IGetTypeOfTypedReference getTypeOfTypedReference) { }

+    public virtual void onASTElement(IGetValueOfTypedReference getValueOfTypedReference) { }

+    public virtual void onASTElement(IGreaterThan greaterThan) { }

+    public virtual void onASTElement(IGreaterThanOrEqual greaterThanOrEqual) { }

+    public virtual void onASTElement(ILabeledStatement labeledStatement) { }

+    public virtual void onASTElement(ILeftShift leftShift) { }

+    public virtual void onASTElement(ILessThan lessThan) { }

+    public virtual void onASTElement(ILessThanOrEqual lessThanOrEqual) { }

+    public virtual void onASTElement(ILocalDeclarationStatement localDeclarationStatement) { }

+    public virtual void onASTElement(ILockStatement lockStatement) { }

+    public virtual void onASTElement(ILogicalNot logicalNot) { }

+    public virtual void onASTElement(IMakeTypedReference makeTypedReference) { }

+    public virtual void onASTElement(IMethodCall methodCall) { }

+    public virtual void onASTElement(IModulus modulus) { }

+    public virtual void onASTElement(IMultiplication multiplication) { }

+    public virtual void onASTElement(INamedArgument namedArgument) { }

+    public virtual void onASTElement(INotEquality notEquality) { }

+    public virtual void onASTElement(IOldValue oldValue) { }

+    public virtual void onASTElement(IOnesComplement onesComplement) { }

+    public virtual void onASTElement(IOutArgument outArgument) { }

+    public virtual void onASTElement(IPointerCall pointerCall) { }

+    public virtual void onASTElement(IPopValue popValue) { }

+    public virtual void onASTElement(IPushStatement pushStatement) { }

+    public virtual void onASTElement(IRefArgument refArgument) { }

+    public virtual void onASTElement(IResourceUseStatement resourceUseStatement) { }

+    public virtual void onASTElement(IReturnValue returnValue) { }

+    public virtual void onASTElement(IRethrowStatement rethrowStatement) { }

+    public virtual void onASTElement(IReturnStatement returnStatement) { }

+    public virtual void onASTElement(IRightShift rightShift) { }

+    public virtual void onASTElement(IRuntimeArgumentHandleExpression runtimeArgumentHandleExpression) { }

+    public virtual void onASTElement(ISizeOf sizeOf) { }

+    public virtual void onASTElement(IStackArrayCreate stackArrayCreate) { }

+    public virtual void onASTElement(ISubtraction subtraction) { }

+    public virtual void onASTElement(ISwitchCase switchCase) { }

+    public virtual void onASTElement(ISwitchStatement switchStatement) { }

+    public virtual void onASTElement(ITargetExpression targetExpression) { }

+    public virtual void onASTElement(IThisReference thisReference) { }

+    public virtual void onASTElement(IThrowStatement throwStatement) { }

+    public virtual void onASTElement(ITryCatchFinallyStatement tryCatchFilterFinallyStatement) { }

+    public virtual void onASTElement(ITokenOf tokenOf) { }

+    public virtual void onASTElement(ITypeOf typeOf) { }

+    public virtual void onASTElement(IUnaryNegation unaryNegation) { }

+    public virtual void onASTElement(IUnaryPlus unaryPlus) { }

+    public virtual void onASTElement(IVectorLength vectorLength) { }

+    public virtual void onASTElement(IWhileDoStatement whileDoStatement) { }

+    public virtual void onASTElement(IYieldBreakStatement yieldBreakStatement) { }

+    public virtual void onASTElement(IYieldReturnStatement yieldReturnStatement) { }

+  }

+}

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs
new file mode 100644
index 00000000..60f39e03
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationPlugins/Translators/BaseTranslator.cs
@@ -0,0 +1,41 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using BytecodeTranslator.TranslationPlugins;

+using Microsoft.Cci;

+using Microsoft.Cci.Contracts;

+

+namespace BytecodeTranslator {

+  class BaseTranslator : ContractAwareTranslator {

+    public TraverserFactory Factory;

+    private Sink sink;

+    private IDictionary<IUnit, IContractProvider> contractProviders;

+    private IDictionary<IUnit, PdbReader> pdbReaders;

+    private MetadataTraverser traverser;

+

+    public BaseTranslator(TraverserFactory factory, Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {

+      Factory = factory;

+      this.sink = sink;

+      this.contractProviders = contractProviders;

+      this.pdbReaders = pdbReaders;

+    }

+

+    public override void initialize() {

+      traverser = Factory.MakeMetadataTraverser(sink, contractProviders, pdbReaders);

+    }

+

+    public override bool isOneShot() {

+      return true;

+    }

+

+    public override int getPriority() {

+      // TODO make configurable from outside

+      return 10;

+    }

+

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

+      traverser.TranslateAssemblies(assemblies);

+    }

+  }

+}

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs
new file mode 100644
index 00000000..f2932ac0
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneFeedbackTranslator.cs
@@ -0,0 +1,34 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using BytecodeTranslator.Phone;

+using Microsoft.Cci;

+

+namespace BytecodeTranslator.TranslationPlugins.Translators {

+  class PhoneFeedbackTranslator : Translator {

+    private Sink sink;

+    PhoneControlFeedbackMetadataTraverser traverser;

+

+    public PhoneFeedbackTranslator(Sink sink) {

+      this.sink = sink;

+    }

+

+    public override void initialize() {

+      traverser = new PhoneControlFeedbackMetadataTraverser(sink.host as MetadataReaderHost);

+    }

+

+    public override bool isOneShot() {

+      return true;

+    }

+

+    public override int getPriority() {

+      // TODO make configurable from outside

+      return 3;

+    }

+

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

+      traverser.Visit(assemblies);

+    }

+  }

+}

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneInitializationTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneInitializationTranslator.cs
new file mode 100644
index 00000000..7cd35b44
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationPlugins/Translators/PhoneInitializationTranslator.cs
@@ -0,0 +1,61 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+

+using BytecodeTranslator.Phone;

+using Microsoft.Cci;

+

+namespace BytecodeTranslator.TranslationPlugins.Translators {

+  class PhoneInitializationTranslator : Translator {

+    private Sink sink;

+    PhoneInitializationMetadataTraverser traverser;

+

+    public PhoneInitializationTranslator(Sink sink) {

+      this.sink = sink;

+    }

+

+    public override void initialize() {

+      traverser = new PhoneInitializationMetadataTraverser(sink.host as MetadataReaderHost);

+    }

+

+    public override bool isOneShot() {

+      return true;

+    }

+

+    public override int getPriority() {

+      // TODO make configurable from outside

+      return 1;

+    }

+

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

+      traverser.InjectPhoneCodeAssemblies(assemblies);

+    }

+  }

+

+  class PhoneNavigationTranslator : Translator {

+    private Sink sink;

+    PhoneNavigationMetadataTraverser traverser;

+

+    public PhoneNavigationTranslator(Sink sink) {

+      this.sink = sink;

+    }

+

+    public override void initialize() {

+      traverser = new PhoneNavigationMetadataTraverser(sink.host as MetadataReaderHost);

+    }

+

+    public override bool isOneShot() {

+      return true;

+    }

+

+    public override int getPriority() {

+      // TODO make configurable from outside

+      return 2;

+    }

+

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

+      traverser.InjectPhoneCodeAssemblies(assemblies);

+    }

+  }

+}

diff --git a/BCT/BytecodeTranslator/TraverserFactory.cs b/BCT/BytecodeTranslator/TraverserFactory.cs
index fac00e42..472cbb0a 100644
--- a/BCT/BytecodeTranslator/TraverserFactory.cs
+++ b/BCT/BytecodeTranslator/TraverserFactory.cs
@@ -17,19 +17,22 @@ using Microsoft.Cci.ILToCodeModel;
 using TranslationPlugins;

 

 using Bpl = Microsoft.Boogie;

+using BytecodeTranslator.TranslationPlugins;

 

 namespace BytecodeTranslator {

   public abstract class TraverserFactory {

     public int Priority { get; set; }

 

+    public abstract Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> reader);

+

     public virtual MetadataTraverser MakeMetadataTraverser(Sink sink,

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

       IDictionary<IUnit, PdbReader> sourceLocationProviders)

     {

-      return new MetadataTraverser(sink, sourceLocationProviders);

+      return new MetadataTraverser(sink, sourceLocationProviders, this);

     }

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

-      return new StatementTraverser(sink, pdbReader, contractContext);

+      return new StatementTraverser(sink, pdbReader, contractContext, this);

     }

 

     public virtual ExpressionTraverser MakeExpressionTraverser(Sink sink, StatementTraverser/*?*/ statementTraverser, bool contractContext) {

diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs
index fe64ae25..b7611375 100644
--- a/BCT/BytecodeTranslator/WholeProgram.cs
+++ b/BCT/BytecodeTranslator/WholeProgram.cs
@@ -15,6 +15,11 @@ using System.Diagnostics.Contracts;
 namespace BytecodeTranslator {

   class WholeProgram : TraverserFactory {

 

+    public override TranslationPlugins.Translator getTranslator(Sink sink, IDictionary<IUnit, IContractProvider> contractProviders, IDictionary<IUnit, PdbReader> pdbReaders) {

+      BaseTranslator translator = new BaseTranslator(this, sink, contractProviders, pdbReaders);

+      return translator;

+    }

+

     /// <summary>

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

     /// 

@@ -27,7 +32,7 @@ namespace BytecodeTranslator {
     public override MetadataTraverser MakeMetadataTraverser(Sink sink,

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

       IDictionary<IUnit, PdbReader> pdbReaders) {

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

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

     }

 

     public class WholeProgramMetadataSemantics : MetadataTraverser {

@@ -37,8 +42,8 @@ namespace BytecodeTranslator {
 

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

 

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

-        : base(sink, pdbReaders) {

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

+        : base(sink, pdbReaders, factory) {

         this.parent = parent;

         this.sink = sink;

       }