Added a test for the split fields option.

Refactored some code to make it easier to work with different heap representations.

7 files changed, 876 insertions, 117 deletions

diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs
index 0e82cab4..087f4c69 100644
--- a/BCT/BytecodeTranslator/Heap.cs
+++ b/BCT/BytecodeTranslator/Heap.cs
@@ -42,7 +42,7 @@ namespace BytecodeTranslator {
     /// <summary>

     /// Prelude text for which access to the ASTs is not needed

     /// </summary>

-    private string InitialPreludeText =

+    private readonly string InitialPreludeText =

       @"const null: int;

 type HeapType = [int,int]int;

 function IsGoodHeap(HeapType): bool;

@@ -62,73 +62,11 @@ procedure {:inline 1} Alloc() returns (x: int)
     #endregion

 

     public override bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program) {

-

       heap = this;

       program = null;

-

-      var flags = BindingFlags.NonPublic | BindingFlags.Public | BindingFlags.Instance;

-      FieldInfo/*?*/[] fields = typeof(TwoDIntHeap).GetFields(flags);

-      RepresentationFor[] rfs = new RepresentationFor[fields.Length];

-      for (int i = 0; i < fields.Length; i++) {

-        var field = fields[i];

-        object[] cas = field.GetCustomAttributes(typeof(RepresentationFor), false);

-        if (cas == null || cas.Length == 0) // only look at fields that have the attribute

-          fields[i] = null;

-        else {

-          foreach (var a in cas) { // should be exactly one

-            RepresentationFor rf = a as RepresentationFor;

-            if (rf != null) {

-              rfs[i] = rf;

-              break;

-            }

-          }

-        }

-      }

-

-      #region Gather all of the Boogie declarations from the fields of this class

-      var preludeText = new StringBuilder(InitialPreludeText);

-      for (int i = 0; i < fields.Length; i++) {

-        var field = fields[i];

-        if (field == null) continue;

-        preludeText.AppendLine(rfs[i].declaration);

-      }

-      #endregion

-

-      #region Parse the declarations

-      var ms = new MemoryStream(ASCIIEncoding.UTF8.GetBytes(preludeText.ToString()));

-      Bpl.Program prelude;

-      int errorCount = Bpl.Parser.Parse(ms, "foo", new List<string>(), out prelude);

-      if (prelude == null || errorCount > 0) { // TODO: Signal error

-        prelude = null;

-        return false;

-      }

-      #endregion

-

-      program = prelude;

-

-      #region Use the compiled program to get the ASTs

-      for (int i = 0; i < fields.Length; i++) {

-        var field = fields[i];

-        if (field == null) continue;

-        if (!rfs[i].required) continue;

-        var val = program.TopLevelDeclarations.First(d => { Bpl.NamedDeclaration nd = d as Bpl.NamedDeclaration; return nd != null && nd.Name.Equals(rfs[i].name); });

-        field.SetValue(this, val);

-      }

-      #endregion

-

-      #region Check that every field in this class has been set

-      for (int i = 0; i < fields.Length; i++) {

-        var field = fields[i];

-        if (field == null) continue;

-        if (!rfs[i].required) continue;

-        if (field.GetValue(this) == null) {

-          return false;

-        }

-      }

-      #endregion Check that every field in this class has been set

-

+      var b = RepresentationFor.ParsePrelude(this.InitialPreludeText, this, out program);

+      if (!b) return false;

       heap = this;

-      program = prelude;

       return true;

     }

 

@@ -246,6 +184,9 @@ procedure {:inline 1} Alloc() returns (x: int)
       /// field.

       /// </summary>

       public Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {

+        if (o == null)

+          return Bpl.Cmd.SimpleAssign(tok, f, value);

+        else

           return Bpl.Cmd.MapAssign(tok, f, o, value);

       }

     }

@@ -258,6 +199,72 @@ procedure {:inline 1} Alloc() returns (x: int)
     internal bool required;

     internal RepresentationFor(string name, string declaration) { this.name = name; this.declaration = declaration;  this.required = true; }

     internal RepresentationFor(string name, string declaration, bool required) { this.name = name; this.declaration = declaration; this.required = required; }

+

+    internal static bool ParsePrelude(string initialPreludeText, object instance, out Bpl.Program/*?*/ prelude) {

+

+      prelude = null;

+

+      var flags = BindingFlags.NonPublic | BindingFlags.Public | BindingFlags.Instance;

+      var type = instance.GetType();

+      FieldInfo/*?*/[] fields = type.GetFields(flags);

+      RepresentationFor[] rfs = new RepresentationFor[fields.Length];

+      for (int i = 0; i < fields.Length; i++) {

+        var field = fields[i];

+        object[] cas = field.GetCustomAttributes(typeof(RepresentationFor), false);

+        if (cas == null || cas.Length == 0) { // only look at fields that have the attribute

+          fields[i] = null;

+        } else {

+          foreach (var a in cas) { // should be exactly one

+            RepresentationFor rf = a as RepresentationFor;

+            if (rf != null) {

+              rfs[i] = rf;

+              break;

+            }

+          }

+        }

+      }

+

+      #region Gather all of the Boogie declarations from the fields of this class

+      var preludeText = new StringBuilder(initialPreludeText);

+      for (int i = 0; i < fields.Length; i++) {

+        var field = fields[i];

+        if (field == null) continue;

+        preludeText.AppendLine(rfs[i].declaration);

+      }

+      #endregion

+

+      #region Parse the declarations

+      var ms = new MemoryStream(ASCIIEncoding.UTF8.GetBytes(preludeText.ToString()));

+      int errorCount = Bpl.Parser.Parse(ms, "foo", new List<string>(), out prelude);

+      if (prelude == null || errorCount > 0) {

+        prelude = null;

+        return false;

+      }

+      #endregion

+

+      #region Use the compiled program to get the ASTs

+      for (int i = 0; i < fields.Length; i++) {

+        var field = fields[i];

+        if (field == null) continue;

+        if (!rfs[i].required) continue;

+        var val = prelude.TopLevelDeclarations.First(d => { Bpl.NamedDeclaration nd = d as Bpl.NamedDeclaration; return nd != null && nd.Name.Equals(rfs[i].name); });

+        field.SetValue(instance, val);

+      }

+      #endregion

+

+      #region Check that every field in this class has been set

+      for (int i = 0; i < fields.Length; i++) {

+        var field = fields[i];

+        if (field == null) continue;

+        if (!rfs[i].required) continue;

+        if (field.GetValue(instance) == null) {

+          return false;

+        }

+      }

+      #endregion Check that every field in this class has been set

+

+      return true;

+    }

   }

 

 }
\ No newline at end of file
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index 89ffd3ec..12ed25a0 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -68,7 +68,12 @@ namespace BytecodeTranslator {
       if (!Parse(args, out assemblyName))

           return result;

       try {

-        result = DoRealWork(assemblyName);

+        HeapFactory heap;

+        if (CommandLineOptions.SplitFields)

+          heap = new SplitFieldsHeap();

+        else

+          heap = new TwoDIntHeap();

+        result = TranslateAssembly(assemblyName, heap);

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

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

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

@@ -77,7 +82,7 @@ namespace BytecodeTranslator {
       return result;

     }

 

-    static int DoRealWork(string assemblyName) {

+    public static int TranslateAssembly(string assemblyName, HeapFactory heapFactory) {

 

       var host = new Microsoft.Cci.MutableContracts.CodeContractAwareHostEnvironment();

       Host = host;

@@ -102,12 +107,8 @@ namespace BytecodeTranslator {
       #region Pass 3: Translate the code model to BPL

       //tmp_BPLGenerator translator = new tmp_BPLGenerator(host, acp);

       var factory = new CLRSemantics();

-      HeapFactory heap;

-      if (CommandLineOptions.SplitFields)

-        heap = new SplitFieldsHeap();

-      else

-        heap = new TwoDIntHeap();

-      MetadataTraverser translator = factory.MakeMetadataTraverser(host.GetContractExtractor(module.ModuleIdentity), pdbReader, heap);

+      MetadataTraverser translator = factory.MakeMetadataTraverser(host.GetContractExtractor(module.ModuleIdentity), pdbReader, heapFactory);

+      TranslationHelper.tmpVarCounter = 0;

       assembly = module as IAssembly;

       if (assembly != null)

         translator.Visit(assembly);

@@ -129,7 +130,6 @@ namespace BytecodeTranslator {
         return name.Substring(0, i);

     }

 

-

   }

 

 }

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index d1d08c8b..1a326440 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -74,7 +74,7 @@ namespace BytecodeTranslator {
       return tok;

     }

 

-    private static int tmpVarCounter = 0;

+    internal static int tmpVarCounter = 0;

     public static string GenerateTempVarName() {

       return "$tmp" + (tmpVarCounter++).ToString();

     }

diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
new file mode 100644
index 00000000..aa1f71e0
--- /dev/null
+++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt
@@ -0,0 +1,370 @@
+// Copyright (c) 2010, Microsoft Corp.

+// Bytecode Translator prelude

+

+procedure RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int);

+

+

+

+implementation RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int)

+{

+    return;

+}

+

+

+

+var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

+

+var RegressionTestInput.ClassWithBoolTypes.b: [int]bool;

+

+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int, y$in: int) returns ($result: bool);

+

+

+

+implementation RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int, y$in: int) returns ($result: bool)

+{

+  var x: int;

+  var y: int;

+  var local_0: bool;

+

+    x := x$in;

+    y := y$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 64} true;

+    local_0 := x < y;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 65} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: int, z$in: bool);

+

+

+

+implementation RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: int, z$in: bool)

+{

+  var z: bool;

+

+    z := z$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 67} true;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 68} true;

+    this[RegressionTestInput.ClassWithBoolTypes.b] := z;

+    if (z)

+    {

+        assert {:sourceFile "Class1.cs"} {:sourceLine 69} true;

+        RegressionTestInput.ClassWithBoolTypes.staticB := z;

+    }

+    else

+    {

+    }

+

+    return;

+}

+

+

+

+procedure RegressionTestInput.ClassWithBoolTypes.Main$System.Void();

+

+

+

+implementation RegressionTestInput.ClassWithBoolTypes.Main$System.Void()

+{

+  var $tmp0: bool;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;

+    call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(3, 4);

+    assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

+    return;

+}

+

+

+

+var RegressionTestInput.ClassWithArrayTypes.s: int;

+

+var RegressionTestInput.ClassWithArrayTypes.a: [int]int;

+

+procedure RegressionTestInput.ClassWithArrayTypes.Main1$System.Void();

+

+

+

+implementation RegressionTestInput.ClassWithArrayTypes.Main1$System.Void()

+{

+  var local_0: int;

+  var $tmp1: int;

+  var local_1: int;

+  var $tmp2: int;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 81} true;

+    call $tmp1 := Alloc();

+    local_0 := $tmp1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 82} true;

+    $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 83} true;

+    assert $ArrayContents[local_0][0] == 2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 85} true;

+    call $tmp2 := Alloc();

+    local_1 := $tmp2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;

+    $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 87} true;

+    assert $ArrayContents[local_1][0] == 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 89} true;

+    assert $ArrayContents[local_0][0] == 2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;

+    return;

+}

+

+

+

+procedure RegressionTestInput.ClassWithArrayTypes.Main2$System.Void();

+

+

+

+implementation RegressionTestInput.ClassWithArrayTypes.Main2$System.Void()

+{

+  var $tmp3: int;

+  var local_0: int;

+  var $tmp4: int;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 95} true;

+    call $tmp3 := Alloc();

+    RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 96} true;

+    $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 97} true;

+    assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 99} true;

+    call $tmp4 := Alloc();

+    local_0 := $tmp4;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;

+    $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 101} true;

+    assert $ArrayContents[local_0][0] == 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 103} true;

+    assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;

+    return;

+}

+

+

+

+procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Void(this: int, x$in: int);

+

+

+

+implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Void(this: int, x$in: int)

+{

+  var x: int;

+

+    x := x$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 109} true;

+    $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this] := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x := 42]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 110} true;

+    $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this] := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x + 1 := 43]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 111} true;

+    assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x + 1] == $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x] + 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 112} true;

+    return;

+}

+

+

+

+procedure RegressionTestInput.ClassWithArrayTypes..ctor$System.Void(this: int);

+

+

+

+implementation RegressionTestInput.ClassWithArrayTypes..ctor$System.Void(this: int)

+{

+    return;

+}

+

+

+

+var RegressionTestInput.Class0.StaticInt: int;

+

+procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

+{

+  var x: int;

+  var local_0: int;

+

+    x := x$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 17} true;

+    local_0 := x + 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.M$System.Void(this: int, x$in: int);

+

+

+

+implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int)

+{

+  var x: int;

+  var __temp_1: int;

+  var $tmp5: int;

+  var __temp_2: int;

+  var __temp_3: int;

+  var local_0: int;

+

+    x := x$in;

+    $tmp5 := x;

+    assert $tmp5 != 0;

+    __temp_1 := 5 / $tmp5;

+    __temp_2 := 3;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 21} true;

+    __temp_3 := __temp_2;

+    x := __temp_3;

+    local_0 := __temp_1 + __temp_2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;

+    assert x == 3 && local_0 <= 8;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 23} true;

+    RegressionTestInput.Class0.StaticInt := local_0;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 24} true;

+    assert local_0 == RegressionTestInput.Class0.StaticInt;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 25} true;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int)

+{

+  var local_0: int;

+  var $tmp6: int;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 28} true;

+    call $tmp6 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

+    local_0 := 3 + RegressionTestInput.Class0.StaticInt + $tmp6;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 29} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.OutParam$System.Int32(this: int) returns (x$out: int, $result: int);

+

+

+

+implementation RegressionTestInput.Class0.OutParam$System.Int32(this: int) returns (x$out: int, $result: int)

+{

+  var local_0: int;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 32} true;

+    x$out := 3 + RegressionTestInput.Class0.StaticInt;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 33} true;

+    local_0 := x$out;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 34} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: int) returns (x$out: int, $result: int);

+

+

+

+implementation RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: int) returns (x$out: int, $result: int)

+{

+  var local_0: int;

+

+    x$out := x$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;

+    x$out := x$out + 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 38} true;

+    RegressionTestInput.Class0.StaticInt := x$out;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;

+    local_0 := x$out;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 40} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)

+{

+  var x: int;

+  var local_0: int;

+

+    x := x$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;

+    x := x + 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 44} true;

+    RegressionTestInput.Class0.StaticInt := x;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;

+    local_0 := x;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 46} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

+{

+  var x: int;

+  var local_0: int;

+

+    x := x$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 50} true;

+    local_0 := x;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)

+{

+  var y: int;

+  var local_0: int;

+  var $tmp7: int;

+

+    y := y$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 54} true;

+    call {:async} $tmp7 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);

+    local_0 := $tmp7;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 55} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0..ctor$System.Void(this: int);

+

+

+

+implementation RegressionTestInput.Class0..ctor$System.Void(this: int)

+{

+    return;

+}

+

+

diff --git a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
index 7379389e..6620b0c4 100644
--- a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
+++ b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj
@@ -102,7 +102,10 @@
     </ProjectReference>

   </ItemGroup>

   <ItemGroup>

-    <EmbeddedResource Include="RegressionTestInput.txt" />

+    <EmbeddedResource Include="TwoDIntHeapInput.txt" />

+  </ItemGroup>

+  <ItemGroup>

+    <EmbeddedResource Include="SplitFieldsHeapInput.txt" />

   </ItemGroup>

   <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />

   <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
new file mode 100644
index 00000000..0b5a0c2d
--- /dev/null
+++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt
@@ -0,0 +1,398 @@
+// Copyright (c) 2010, Microsoft Corp.

+// Bytecode Translator prelude

+

+const null: int;

+

+type HeapType = [int,int]int;

+

+function IsGoodHeap(HeapType) : bool;

+

+var $ArrayContents: [int][int]int;

+

+var $ArrayLength: [int]int;

+

+var $Alloc: [int]bool;

+

+procedure {:inline 1} Alloc() returns (x: int);

+  modifies $Alloc;

+  free ensures x != 0;

+

+

+

+implementation Alloc() returns (x: int)

+{

+    assume $Alloc[x] == false;

+    $Alloc[x] := true;

+}

+

+

+

+var $Heap: HeapType where IsGoodHeap($Heap);

+

+procedure RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int);

+

+

+

+implementation RegressionTestInput.AsyncAttribute..ctor$System.Void(this: int)

+{

+    return;

+}

+

+

+

+var RegressionTestInput.ClassWithBoolTypes.staticB: bool;

+

+const unique RegressionTestInput.ClassWithBoolTypes.b: bool;

+

+procedure RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int, y$in: int) returns ($result: bool);

+

+

+

+implementation RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(x$in: int, y$in: int) returns ($result: bool)

+{

+  var x: int;

+  var y: int;

+  var local_0: bool;

+

+    x := x$in;

+    y := y$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 64} true;

+    local_0 := x < y;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 65} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: int, z$in: bool);

+

+

+

+implementation RegressionTestInput.ClassWithBoolTypes..ctor$System.Void(this: int, z$in: bool)

+{

+  var z: bool;

+

+    z := z$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 67} true;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 68} true;

+    $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := z;

+    if (z)

+    {

+        assert {:sourceFile "Class1.cs"} {:sourceLine 69} true;

+        RegressionTestInput.ClassWithBoolTypes.staticB := z;

+    }

+    else

+    {

+    }

+

+    return;

+}

+

+

+

+procedure RegressionTestInput.ClassWithBoolTypes.Main$System.Void();

+

+

+

+implementation RegressionTestInput.ClassWithBoolTypes.Main$System.Void()

+{

+  var $tmp0: bool;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 73} true;

+    call $tmp0 := RegressionTestInput.ClassWithBoolTypes.M$System.Boolean(3, 4);

+    assert {:sourceFile "Class1.cs"} {:sourceLine 74} true;

+    return;

+}

+

+

+

+var RegressionTestInput.ClassWithArrayTypes.s: int;

+

+const unique RegressionTestInput.ClassWithArrayTypes.a: int;

+

+procedure RegressionTestInput.ClassWithArrayTypes.Main1$System.Void();

+

+

+

+implementation RegressionTestInput.ClassWithArrayTypes.Main1$System.Void()

+{

+  var local_0: int;

+  var $tmp1: int;

+  var local_1: int;

+  var $tmp2: int;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 81} true;

+    call $tmp1 := Alloc();

+    local_0 := $tmp1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 82} true;

+    $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 83} true;

+    assert $ArrayContents[local_0][0] == 2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 85} true;

+    call $tmp2 := Alloc();

+    local_1 := $tmp2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 86} true;

+    $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 87} true;

+    assert $ArrayContents[local_1][0] == 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 89} true;

+    assert $ArrayContents[local_0][0] == 2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 90} true;

+    return;

+}

+

+

+

+procedure RegressionTestInput.ClassWithArrayTypes.Main2$System.Void();

+

+

+

+implementation RegressionTestInput.ClassWithArrayTypes.Main2$System.Void()

+{

+  var $tmp3: int;

+  var local_0: int;

+  var $tmp4: int;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 95} true;

+    call $tmp3 := Alloc();

+    RegressionTestInput.ClassWithArrayTypes.s := $tmp3;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 96} true;

+    $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 97} true;

+    assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 99} true;

+    call $tmp4 := Alloc();

+    local_0 := $tmp4;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 100} true;

+    $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 101} true;

+    assert $ArrayContents[local_0][0] == 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 103} true;

+    assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 104} true;

+    return;

+}

+

+

+

+procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Void(this: int, x$in: int);

+

+

+

+implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Void(this: int, x$in: int)

+{

+  var x: int;

+

+    x := x$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 109} true;

+    $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x := 42]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 110} true;

+    $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x + 1 := 43]];

+    assert {:sourceFile "Class1.cs"} {:sourceLine 111} true;

+    assert $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x + 1] == $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x] + 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 112} true;

+    return;

+}

+

+

+

+procedure RegressionTestInput.ClassWithArrayTypes..ctor$System.Void(this: int);

+

+

+

+implementation RegressionTestInput.ClassWithArrayTypes..ctor$System.Void(this: int)

+{

+    return;

+}

+

+

+

+var RegressionTestInput.Class0.StaticInt: int;

+

+procedure RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) returns ($result: int)

+{

+  var x: int;

+  var local_0: int;

+

+    x := x$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 17} true;

+    local_0 := x + 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 18} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.M$System.Void(this: int, x$in: int);

+

+

+

+implementation RegressionTestInput.Class0.M$System.Void(this: int, x$in: int)

+{

+  var x: int;

+  var __temp_1: int;

+  var $tmp5: int;

+  var __temp_2: int;

+  var __temp_3: int;

+  var local_0: int;

+

+    x := x$in;

+    $tmp5 := x;

+    assert $tmp5 != 0;

+    __temp_1 := 5 / $tmp5;

+    __temp_2 := 3;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 21} true;

+    __temp_3 := __temp_2;

+    x := __temp_3;

+    local_0 := __temp_1 + __temp_2;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 22} true;

+    assert x == 3 && local_0 <= 8;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 23} true;

+    RegressionTestInput.Class0.StaticInt := local_0;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 24} true;

+    assert local_0 == RegressionTestInput.Class0.StaticInt;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 25} true;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.NonVoid$System.Int32(this: int) returns ($result: int)

+{

+  var local_0: int;

+  var $tmp6: int;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 28} true;

+    call $tmp6 := RegressionTestInput.Class0.StaticMethod$System.Int32(3);

+    local_0 := 3 + RegressionTestInput.Class0.StaticInt + $tmp6;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 29} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.OutParam$System.Int32(this: int) returns (x$out: int, $result: int);

+

+

+

+implementation RegressionTestInput.Class0.OutParam$System.Int32(this: int) returns (x$out: int, $result: int)

+{

+  var local_0: int;

+

+    assert {:sourceFile "Class1.cs"} {:sourceLine 32} true;

+    x$out := 3 + RegressionTestInput.Class0.StaticInt;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 33} true;

+    local_0 := x$out;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 34} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: int) returns (x$out: int, $result: int);

+

+

+

+implementation RegressionTestInput.Class0.RefParam$System.Int32(this: int, x$in: int) returns (x$out: int, $result: int)

+{

+  var local_0: int;

+

+    x$out := x$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 37} true;

+    x$out := x$out + 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 38} true;

+    RegressionTestInput.Class0.StaticInt := x$out;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 39} true;

+    local_0 := x$out;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 40} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int)

+{

+  var x: int;

+  var local_0: int;

+

+    x := x$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 43} true;

+    x := x + 1;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 44} true;

+    RegressionTestInput.Class0.StaticInt := x;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 45} true;

+    local_0 := x;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 46} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int)

+{

+  var x: int;

+  var local_0: int;

+

+    x := x$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 50} true;

+    local_0 := x;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 51} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int);

+

+

+

+implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int)

+{

+  var y: int;

+  var local_0: int;

+  var $tmp7: int;

+

+    y := y$in;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 54} true;

+    call {:async} $tmp7 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y);

+    local_0 := $tmp7;

+    assert {:sourceFile "Class1.cs"} {:sourceLine 55} true;

+    $result := local_0;

+    return;

+}

+

+

+

+procedure RegressionTestInput.Class0..ctor$System.Void(this: int);

+

+

+

+implementation RegressionTestInput.Class0..ctor$System.Void(this: int)

+{

+    return;

+}

+

+

diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
index 406bfc23..179dbb87 100644
--- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs
+++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs
@@ -60,59 +60,40 @@ namespace TranslationTest {
     //

     #endregion

 

-    private string ExecuteTest(string assemblyName) {

-

-      var host = new Microsoft.Cci.MutableContracts.CodeContractAwareHostEnvironment();

-      BCT.Host = host;

-

-      IModule/*?*/ module = host.LoadUnitFrom(assemblyName) as IModule;

-      if (module == null || module == Dummy.Module || module == Dummy.Assembly) {

-        Console.WriteLine(assemblyName + " is not a PE file containing a CLR module or assembly, or an error occurred when loading it.");

-        Assert.Fail("Failed to read in test assembly for regression test");

-      }

-

-      IAssembly/*?*/ assembly = null;

-

-      PdbReader/*?*/ pdbReader = null;

-      string pdbFile = Path.ChangeExtension(module.Location, "pdb");

-      if (File.Exists(pdbFile)) {

-        Stream pdbStream = File.OpenRead(pdbFile);

-        pdbReader = new PdbReader(pdbStream, host);

-      }

-

-      module = Decompiler.GetCodeModelFromMetadataModel(host, module, pdbReader);

-

-      #region Pass 3: Translate the code model to BPL

-      var factory = new CLRSemantics();

-      var heap = new TwoDIntHeap();

-      MetadataTraverser translator = factory.MakeMetadataTraverser(host.GetContractExtractor(module.ModuleIdentity), pdbReader, heap);

-      assembly = module as IAssembly;

-      if (assembly != null)

-        translator.Visit(assembly);

-      else

-        translator.Visit(module);

-      #endregion Pass 3: Translate the code model to BPL

-      Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(module.Name + ".bpl");

-      Prelude.Emit(writer);

-      translator.TranslatedProgram.Emit(writer);

-      writer.Close();

+    private string ExecuteTest(string assemblyName, HeapFactory heapFactory) {

+      BCT.TranslateAssembly(assemblyName, heapFactory);

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

       var s = File.ReadAllText(fileName);

       return s;

     }

 

     [TestMethod]

-    public void TranslationTest() {

+    public void TwoDIntHeap() {

+      string dir = TestContext.DeploymentDirectory;

+      var fullPath = Path.Combine(dir, "RegressionTestInput.dll");

+      Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.TwoDIntHeapInput.txt");

+      StreamReader reader = new StreamReader(resource);

+      string expected = reader.ReadToEnd();

+      var result = ExecuteTest(fullPath, new TwoDIntHeap());

+      if (result != expected) {

+        string resultFile = Path.GetFullPath("TwoDIntHeapOutput.txt");

+        File.WriteAllText(resultFile, result);

+        Assert.Fail("Output didn't match TwoDIntHeapInput.txt: " + resultFile);

+      }

+    }

+

+    [TestMethod]

+    public void SplitFieldsHeap() {

       string dir = TestContext.DeploymentDirectory;

       var fullPath = Path.Combine(dir, "RegressionTestInput.dll");

-      Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.RegressionTestInput.txt");

+      Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.SplitFieldsHeapInput.txt");

       StreamReader reader = new StreamReader(resource);

       string expected = reader.ReadToEnd();

-      var result = ExecuteTest(fullPath);

+      var result = ExecuteTest(fullPath, new SplitFieldsHeap());

       if (result != expected) {

-        string resultFile = Path.GetFullPath("RegressionTestOutput.txt");

+        string resultFile = Path.GetFullPath("SplitFieldsHeapOutput.txt");

         File.WriteAllText(resultFile, result);

-        Assert.Fail("Output didn't match RegressionTestInput.txt: " + resultFile);

+        Assert.Fail("Output didn't match SplitFieldsHeapInput.txt: " + resultFile);

       }

     }

   }