Refactored translator so it can be called programmatically and return the

translated program in memory without writing it to disk.

2 files changed, 35 insertions, 12 deletions

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 151843d8..c6d8e7a4 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -168,18 +168,46 @@ namespace BytecodeTranslator {
           return 1;

         }

 

-        result = TranslateAssembly(assemblyNames, heap, options, exemptionList, whiteList);

+        var pgm = TranslateAssembly(assemblyNames, heap, options, exemptionList, whiteList);

+        var fileName = assemblyNames[0];

+        fileName = Path.GetFileNameWithoutExtension(fileName);

+        string outputFileName = fileName + ".bpl";

+        Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);

+        Prelude.Emit(writer);

+        pgm.Emit(writer);

+        writer.Close();

+        return 0; // success

 

       } catch (Exception e) { // swallow everything and just return an error code

         Console.WriteLine("The byte-code translator failed: {0}", e.Message);

         // Console.WriteLine("Stack trace: {0}", e.StackTrace);

         return -1;

       }

-      return result;

     }

 

     private static List<IModule> modules;

-    public static int TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {

+

+    public static int TranslateAssemblyAndWriteOutput(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {

+      Contract.Requires(assemblyNames != null);

+      Contract.Requires(heapFactory != null);

+      try {

+        var pgm = TranslateAssembly(assemblyNames, heapFactory, options, exemptionList, whiteList);

+        var fileName = assemblyNames[0];

+        fileName = Path.GetFileNameWithoutExtension(fileName);

+        string outputFileName = fileName + ".bpl";

+        Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);

+        Prelude.Emit(writer);

+        pgm.Emit(writer);

+        writer.Close();

+        return 0; // success

+      } catch (Exception e) { // swallow everything and just return an error code

+        Console.WriteLine("The byte-code translator failed: {0}", e.Message);

+        // Console.WriteLine("Stack trace: {0}", e.StackTrace);

+        return -1;

+      }

+    }

+

+    public static Bpl.Program/*?*/ TranslateAssembly(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {

       Contract.Requires(assemblyNames != null);

       Contract.Requires(heapFactory != null);

 

@@ -268,8 +296,7 @@ namespace BytecodeTranslator {
       #endregion

 

       if (modules.Count == 0) {

-        Console.WriteLine("No input assemblies to translate.");

-        return -1;

+        throw new TranslationException("No input assemblies to translate.");

       }

 

       var primaryModule = modules[0];

@@ -380,14 +407,10 @@ namespace BytecodeTranslator {
       //  }

       //}

       //sink.TranslatedProgram.TopLevelDeclarations = goodDecls;

-

-      Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(outputFileName);

-      Prelude.Emit(writer);

-      sink.TranslatedProgram.Emit(writer);

-      writer.Close();

-      return 0; // success

+      return sink.TranslatedProgram;

     }

 

+

     private static void finalizeNavigationAnalysisAndBoogieCode(string phoneControlsConfigFile, Sink sink, string outputFileName) {

       outputBoogieTrackedControlConfiguration(phoneControlsConfigFile);

       checkTransitivelyCalledBackKeyNavigations(modules);

diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index a8b5fdb2..a48be6af 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -61,7 +61,7 @@ namespace TranslationTest {
     #endregion

 

     private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {

-      BCT.TranslateAssembly(new List<string>{assemblyName}, heapFactory, new Options(), null, false);

+      BCT.TranslateAssemblyAndWriteOutput(new List<string> { assemblyName }, heapFactory, new Options(), null, false);

       var fileName = Path.ChangeExtension(assemblyName, "bpl");

       var s = File.ReadAllText(fileName);

       return s;