diff options
| author |  mikebarnett <unknown> | 2011-01-20 23:59:09 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2011-01-20 23:59:09 +0000 |
| commit | f44aec83b0569984c76bb8ce9fe90e064ca9dadd (patch) | |
| tree | a23b615073ca0f8b31eb84907d2d246ff0b7b3e3 /BCT/RegressionTests | |
| parent | 9923e90c5980085d12e5185af2be1d4967ad27f9 (diff) | |
Added a test for the split fields option.
Refactored some code to make it easier to work with different heap representations.
Diffstat (limited to 'BCT/RegressionTests')
4 files changed, 794 insertions, 42 deletions
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);
}
}
}
|