(BCT) starting translators-as-plugins impl

7 files changed, 65 insertions, 3 deletions

diff --git a/BCT/BytecodeTranslator/BytecodeTranslator.csproj b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
index 9e5babc1..ff49e4c3 100644
--- a/BCT/BytecodeTranslator/BytecodeTranslator.csproj
+++ b/BCT/BytecodeTranslator/BytecodeTranslator.csproj
@@ -138,6 +138,10 @@
     <Compile Include="Program.cs" />

     <Compile Include="TranslationException.cs" />

     <Compile Include="TranslationHelper.cs" />

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

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

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

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

     <Compile Include="TraverserFactory.cs" />

     <Compile Include="WholeProgram.cs" />

   </ItemGroup>

diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index f1f7e714..e4a81eb8 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -18,6 +18,7 @@ using Bpl = Microsoft.Boogie;
 using System.Diagnostics.Contracts;

 using TranslationPlugins;

 using BytecodeTranslator.Phone;

+using BytecodeTranslator.TranslationPlugins;

 

 

 namespace BytecodeTranslator {

@@ -26,7 +27,7 @@ namespace BytecodeTranslator {
   /// Responsible for traversing all metadata elements (i.e., everything exclusive

   /// of method bodies).

   /// </summary>

-  public class MetadataTraverser : BaseMetadataTraverser {

+  public class MetadataTraverser : BaseMetadataTraverser, ITranslator {

 

     readonly Sink sink;

 

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index da0f401e..fc48f4c7 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -21,6 +21,8 @@ using Microsoft.Cci.MutableCodeModel.Contracts;
 using TranslationPlugins;

 using BytecodeTranslator.Phone;

 using System.Text.RegularExpressions;

+using BytecodeTranslator.TranslationPlugins;

+using BytecodeTranslator.TranslationPlugins.BytecodeTranslator;

 

 namespace BytecodeTranslator {

 

@@ -262,8 +264,9 @@ namespace BytecodeTranslator {
 

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

       TranslationHelper.tmpVarCounter = 0;

-      MetadataTraverser translator;

-      translator= bctTraverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);

+

+      ITranslationPlugin bctPlugin= new BytecodeTranslatorPlugin();

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

 

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

         PhoneCodeHelper.initialize(host);

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs b/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs
new file mode 100644
index 00000000..425a9476
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationPlugins/BytecodeTranslator/BytecodeTranslatorPlugin.cs
@@ -0,0 +1,16 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

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

+    }

+  }

+}

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/IContractAwareTranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/IContractAwareTranslator.cs
new file mode 100644
index 00000000..e1079e5d
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationPlugins/IContractAwareTranslator.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 {

+  interface IContractAwareTranslator : ITranslator {

+    IEnumerable<Bpl.Expr> getPreconditionTranslation(IMethodContract contract);

+    IEnumerable<Bpl.Expr> getPostconditionTranslation(IMethodContract contract);

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

+  }

+}

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

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

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

+  }

+}

diff --git a/BCT/BytecodeTranslator/TranslationPlugins/ITranslator.cs b/BCT/BytecodeTranslator/TranslationPlugins/ITranslator.cs
new file mode 100644
index 00000000..302794b5
--- /dev/null
+++ b/BCT/BytecodeTranslator/TranslationPlugins/ITranslator.cs
@@ -0,0 +1,11 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Cci;

+

+namespace BytecodeTranslator.TranslationPlugins {

+  interface ITranslator {

+    void TranslateAssemblies(IEnumerable<IUnit> assemblies);

+  }

+}