From 484aba5e25c9c35eaaa42cb7742591febff9da83 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sat, 23 Apr 2011 23:32:07 -0700 Subject: 0. Deleted other heap representations except SplitField and General 1. first cut at implementing structs --- .../TranslationTest/GeneralHeapInput.txt | 8 +- .../TranslationTest/SplitFieldsHeapInput.txt | 4 + .../TranslationTest/TranslationTest.csproj | 6 - .../TranslationTest/TwoDBoxHeapInput.txt | 729 --------------------- .../TranslationTest/TwoDIntHeapInput.txt | 719 -------------------- BCT/RegressionTests/TranslationTest/UnitTest0.cs | 30 - 6 files changed, 8 insertions(+), 1488 deletions(-) delete mode 100644 BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt delete mode 100644 BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt (limited to 'BCT/RegressionTests') diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 703c908f..87514ae9 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -3,8 +3,6 @@ const null: ref; -type box; - type ref = int; type HeapType = [ref,Field]box; @@ -188,8 +186,6 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) -type Field; - var $Heap: HeapType where IsGoodHeap($Heap); function Box2Int(box) : int; @@ -210,6 +206,10 @@ function {:inline true} Write(H: HeapType, o: ref, f: Field, v: box) : HeapType H[o, f := v] } +type Field; + +type box; + type Type; function $DynamicType(ref) : Type; diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 5245bf3d..e6d6e7fd 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -188,6 +188,10 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) +type Field; + +type box; + type Type; function $DynamicType(ref) : Type; diff --git a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj index cef103b7..b0dd1907 100644 --- a/BCT/RegressionTests/TranslationTest/TranslationTest.csproj +++ b/BCT/RegressionTests/TranslationTest/TranslationTest.csproj @@ -101,15 +101,9 @@ RegressionTestInput - - - - - - diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt deleted file mode 100644 index c23df829..00000000 --- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt +++ /dev/null @@ -1,729 +0,0 @@ -// Copyright (c) 2010, Microsoft Corp. -// Bytecode Translator prelude - -const null: int; - -type box; - -type HeapType = [int,int]box; - -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; -} - - - -procedure DelegateAdd(a: int, b: int) returns (c: int); - - - -implementation DelegateAdd(a: int, b: int) returns (c: int) -{ - var m: int; - var o: int; - - if (a == 0) - { - c := b; - return; - } - else if (b == 0) - { - c := a; - return; - } - - call m, o := GetFirstElement(b); - call c := Alloc(); - $Head[c] := $Head[a]; - $Next[c] := $Next[a]; - $Method[c] := $Method[a]; - $Receiver[c] := $Receiver[a]; - call c := DelegateAddHelper(c, m, o); -} - - - -procedure DelegateRemove(a: int, b: int) returns (c: int); - - - -implementation DelegateRemove(a: int, b: int) returns (c: int) -{ - var m: int; - var o: int; - - if (a == 0) - { - c := 0; - return; - } - else if (b == 0) - { - c := a; - return; - } - - call m, o := GetFirstElement(b); - call c := Alloc(); - $Head[c] := $Head[a]; - $Next[c] := $Next[a]; - $Method[c] := $Method[a]; - $Receiver[c] := $Receiver[a]; - call c := DelegateRemoveHelper(c, m, o); -} - - - -procedure GetFirstElement(i: int) returns (m: int, o: int); - - - -implementation GetFirstElement(i: int) returns (m: int, o: int) -{ - var first: int; - - first := $Next[i][$Head[i]]; - m := $Method[i][first]; - o := $Receiver[i][first]; -} - - - -procedure DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int); - - - -implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int) -{ - var x: int; - var h: int; - - if (oldi == 0) - { - call i := Alloc(); - call x := Alloc(); - $Head[i] := x; - $Next[i] := $Next[i][x := x]; - } - else - { - i := oldi; - } - - h := $Head[i]; - $Method[i] := $Method[i][h := m]; - $Receiver[i] := $Receiver[i][h := o]; - call x := Alloc(); - $Next[i] := $Next[i][x := $Next[i][h]]; - $Next[i] := $Next[i][h := x]; - $Head[i] := x; -} - - - -procedure DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int); - - - -implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) -{ - var prev: int; - var iter: int; - var niter: int; - - i := oldi; - if (i == 0) - { - return; - } - - prev := 0; - iter := $Head[i]; - while (true) - { - niter := $Next[i][iter]; - if (niter == $Head[i]) - { - break; - } - - if ($Method[i][niter] == m && $Receiver[i][niter] == o) - { - prev := iter; - } - - iter := niter; - } - - if (prev == 0) - { - return; - } - - $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]]; - if ($Next[i][$Head[i]] == $Head[i]) - { - i := 0; - } -} - - - -var $Heap: HeapType where IsGoodHeap($Heap); - -function Box2Int(box) : int; - -function Box2Bool(box) : bool; - -function Int2Box(int) : box; - -function Bool2Box(bool) : box; - -type Type; - -function $DynamicType(ref) : Type; - -function $TypeOf(Type) : ref; - -var $Head: [int]int; - -var $Next: [int][int]int; - -var $Method: [int][int]int; - -var $Receiver: [int][int]int; - -const unique RegressionTestInput.ClassWithArrayTypes: Type; - -var RegressionTestInput.ClassWithArrayTypes.s: int; - -const unique RegressionTestInput.ClassWithArrayTypes.a: int; - -procedure RegressionTestInput.ClassWithArrayTypes.Main1(); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main1() -{ - var local_0: int; - var $tmp0: int; - var local_1: int; - var $tmp1: int; - - assert {:sourceFile "Class1.cs"} {:sourceLine 86} true; - call $tmp0 := Alloc(); - local_0 := $tmp0; - assert {:sourceFile "Class1.cs"} {:sourceLine 87} true; - $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 88} true; - assert $ArrayContents[local_0][0] == 2; - assert {:sourceFile "Class1.cs"} {:sourceLine 90} true; - call $tmp1 := Alloc(); - local_1 := $tmp1; - assert {:sourceFile "Class1.cs"} {:sourceLine 91} true; - $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 92} true; - assert $ArrayContents[local_1][0] == 1; - assert {:sourceFile "Class1.cs"} {:sourceLine 94} true; - assert $ArrayContents[local_0][0] == 2; - assert {:sourceFile "Class1.cs"} {:sourceLine 95} true; - return; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main2(); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main2() -{ - var $tmp2: int; - var local_0: int; - var $tmp3: int; - - assert {:sourceFile "Class1.cs"} {:sourceLine 100} true; - call $tmp2 := Alloc(); - RegressionTestInput.ClassWithArrayTypes.s := $tmp2; - assert {:sourceFile "Class1.cs"} {:sourceLine 101} true; - $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 102} true; - assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2; - assert {:sourceFile "Class1.cs"} {:sourceLine 104} true; - call $tmp3 := Alloc(); - local_0 := $tmp3; - assert {:sourceFile "Class1.cs"} {:sourceLine 105} true; - $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 106} true; - assert $ArrayContents[local_0][0] == 1; - assert {:sourceFile "Class1.cs"} {:sourceLine 108} true; - assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2; - assert {:sourceFile "Class1.cs"} {:sourceLine 109} true; - return; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int) -{ - var x: int; - - x := x$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 114} true; - $ArrayContents := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a]) := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x := 42]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 115} true; - $ArrayContents := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a]) := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x + 1 := 43]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 116} true; - assert $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x + 1] == $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][x] + 1; - assert {:sourceFile "Class1.cs"} {:sourceLine 117} true; - return; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int) -{ - var xs: int; - - xs := xs$in; - if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true)) - { - assert {:sourceFile "Class1.cs"} {:sourceLine 121} true; - $ArrayContents := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a]) := $ArrayContents[Box2Int($Heap[this, RegressionTestInput.ClassWithArrayTypes.a])][0 := $ArrayContents[xs][0]]]; - } - else - { - } - - assert {:sourceFile "Class1.cs"} {:sourceLine 123} true; - return; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); - - - -procedure System.Object.#ctor(this: int); - - - -implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int) -{ - $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := Int2Box(0); - call System.Object.#ctor(this); - return; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.#cctor(); - - - -implementation RegressionTestInput.ClassWithArrayTypes.#cctor() -{ - RegressionTestInput.ClassWithArrayTypes.s := 0; -} - - - -const unique RegressionTestInput.Class0: Type; - -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; - - x := x$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 18} true; - $result := x + 1; - return; -} - - - -procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int); - - - -implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) -{ - var x: int; - var __temp_1: int; - var $tmp4: int; - var local_0: int; - - x := x$in; - $tmp4 := x; - assert $tmp4 != 0; - __temp_1 := 5 / $tmp4; - x := 3; - local_0 := __temp_1 + 3; - assert {:sourceFile "Class1.cs"} {:sourceLine 22} true; - assert (if x == 3 then local_0 <= 8 else false); - 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.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int); - - - -implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int) -{ - var x: int; - var y: int; - - x := x$in; - y := y$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 28} true; - return; -} - - - -procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool); - - - -implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool) -{ - var b: bool; - - b := b$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 29} true; - return; -} - - - -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int); - - - -implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int) -{ - var c: int; - - c := c$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 30} true; - return; -} - - - -procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int); - - - -implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int) -{ - var $tmp5: int; - - assert {:sourceFile "Class1.cs"} {:sourceLine 34} true; - call $tmp5 := RegressionTestInput.Class0.StaticMethod$System.Int32(3); - $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5; - 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) -{ - assert {:sourceFile "Class1.cs"} {:sourceLine 37} true; - x$out := 3 + RegressionTestInput.Class0.StaticInt; - assert {:sourceFile "Class1.cs"} {:sourceLine 39} true; - $result := x$out; - 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) -{ - x$out := x$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 42} true; - x$out := x$out + 1; - assert {:sourceFile "Class1.cs"} {:sourceLine 43} true; - RegressionTestInput.Class0.StaticInt := x$out; - assert {:sourceFile "Class1.cs"} {:sourceLine 45} true; - $result := x$out; - 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; - - x := x$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 48} true; - x := x + 1; - assert {:sourceFile "Class1.cs"} {:sourceLine 49} true; - RegressionTestInput.Class0.StaticInt := x; - assert {:sourceFile "Class1.cs"} {:sourceLine 51} true; - $result := x; - return; -} - - - -procedure {:RegressionTestInput.Async} 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; - - x := x$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 56} true; - $result := x; - 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 $tmp6: int; - - y := y$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 60} true; - call {:async} $tmp6 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y); - $result := $tmp6; - return; -} - - - -procedure RegressionTestInput.Class0.#ctor(this: int); - - - -implementation RegressionTestInput.Class0.#ctor(this: int) -{ - call System.Object.#ctor(this); - return; -} - - - -procedure RegressionTestInput.Class0.#cctor(); - - - -implementation RegressionTestInput.Class0.#cctor() -{ - RegressionTestInput.Class0.StaticInt := 0; -} - - - -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type; - -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int; - -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int; - -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int); - - - -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int) -{ - assert {:sourceFile "Class1.cs"} {:sourceLine 130} true; - $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(Box2Int($Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x])); - assert {:sourceFile "Class1.cs"} {:sourceLine 131} true; - return; -} - - - -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int); - - - -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int) -{ - $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := Int2Box(0); - $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := Int2Box(0); - call System.Object.#ctor(this); - return; -} - - - -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor(); - - - -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor() -{ -} - - - -const unique RegressionTestInput.ClassWithBoolTypes: Type; - -var RegressionTestInput.ClassWithBoolTypes.staticB: bool; - -const unique RegressionTestInput.ClassWithBoolTypes.b: bool; - -procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool); - - - -implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool) -{ - var x: int; - var y: int; - - x := x$in; - y := y$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 70} true; - $result := x < y; - return; -} - - - -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool); - - - -implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool) -{ - var z: bool; - - z := z$in; - $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(false); - assert {:sourceFile "Class1.cs"} {:sourceLine 72} true; - call System.Object.#ctor(this); - assert {:sourceFile "Class1.cs"} {:sourceLine 73} true; - $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := Bool2Box(z); - assert {:sourceFile "Class1.cs"} {:sourceLine 74} true; - if (z) - { - assert {:sourceFile "Class1.cs"} {:sourceLine 74} true; - RegressionTestInput.ClassWithBoolTypes.staticB := z; - } - else - { - } - - return; -} - - - -procedure RegressionTestInput.ClassWithBoolTypes.Main(); - - - -implementation RegressionTestInput.ClassWithBoolTypes.Main() -{ - var $tmp7: bool; - - assert {:sourceFile "Class1.cs"} {:sourceLine 78} true; - call $tmp7 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4); - assert {:sourceFile "Class1.cs"} {:sourceLine 79} true; - return; -} - - - -procedure RegressionTestInput.ClassWithBoolTypes.#cctor(); - - - -implementation RegressionTestInput.ClassWithBoolTypes.#cctor() -{ - RegressionTestInput.ClassWithBoolTypes.staticB := false; -} - - - -const unique RegressionTestInput.AsyncAttribute: Type; - -procedure RegressionTestInput.AsyncAttribute.#ctor(this: int); - - - -procedure System.Attribute.#ctor(this: int); - - - -implementation RegressionTestInput.AsyncAttribute.#ctor(this: int) -{ - call System.Attribute.#ctor(this); - return; -} - - - -procedure RegressionTestInput.AsyncAttribute.#cctor(); - - - -implementation RegressionTestInput.AsyncAttribute.#cctor() -{ -} - - diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt deleted file mode 100644 index 262958c0..00000000 --- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt +++ /dev/null @@ -1,719 +0,0 @@ -// 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; -} - - - -procedure DelegateAdd(a: int, b: int) returns (c: int); - - - -implementation DelegateAdd(a: int, b: int) returns (c: int) -{ - var m: int; - var o: int; - - if (a == 0) - { - c := b; - return; - } - else if (b == 0) - { - c := a; - return; - } - - call m, o := GetFirstElement(b); - call c := Alloc(); - $Head[c] := $Head[a]; - $Next[c] := $Next[a]; - $Method[c] := $Method[a]; - $Receiver[c] := $Receiver[a]; - call c := DelegateAddHelper(c, m, o); -} - - - -procedure DelegateRemove(a: int, b: int) returns (c: int); - - - -implementation DelegateRemove(a: int, b: int) returns (c: int) -{ - var m: int; - var o: int; - - if (a == 0) - { - c := 0; - return; - } - else if (b == 0) - { - c := a; - return; - } - - call m, o := GetFirstElement(b); - call c := Alloc(); - $Head[c] := $Head[a]; - $Next[c] := $Next[a]; - $Method[c] := $Method[a]; - $Receiver[c] := $Receiver[a]; - call c := DelegateRemoveHelper(c, m, o); -} - - - -procedure GetFirstElement(i: int) returns (m: int, o: int); - - - -implementation GetFirstElement(i: int) returns (m: int, o: int) -{ - var first: int; - - first := $Next[i][$Head[i]]; - m := $Method[i][first]; - o := $Receiver[i][first]; -} - - - -procedure DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int); - - - -implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int) -{ - var x: int; - var h: int; - - if (oldi == 0) - { - call i := Alloc(); - call x := Alloc(); - $Head[i] := x; - $Next[i] := $Next[i][x := x]; - } - else - { - i := oldi; - } - - h := $Head[i]; - $Method[i] := $Method[i][h := m]; - $Receiver[i] := $Receiver[i][h := o]; - call x := Alloc(); - $Next[i] := $Next[i][x := $Next[i][h]]; - $Next[i] := $Next[i][h := x]; - $Head[i] := x; -} - - - -procedure DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int); - - - -implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) -{ - var prev: int; - var iter: int; - var niter: int; - - i := oldi; - if (i == 0) - { - return; - } - - prev := 0; - iter := $Head[i]; - while (true) - { - niter := $Next[i][iter]; - if (niter == $Head[i]) - { - break; - } - - if ($Method[i][niter] == m && $Receiver[i][niter] == o) - { - prev := iter; - } - - iter := niter; - } - - if (prev == 0) - { - return; - } - - $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]]; - if ($Next[i][$Head[i]] == $Head[i]) - { - i := 0; - } -} - - - -var $Heap: HeapType where IsGoodHeap($Heap); - -type Type; - -function $DynamicType(ref) : Type; - -function $TypeOf(Type) : ref; - -var $Head: [int]int; - -var $Next: [int][int]int; - -var $Method: [int][int]int; - -var $Receiver: [int][int]int; - -const unique RegressionTestInput.ClassWithArrayTypes: Type; - -var RegressionTestInput.ClassWithArrayTypes.s: int; - -const unique RegressionTestInput.ClassWithArrayTypes.a: int; - -procedure RegressionTestInput.ClassWithArrayTypes.Main1(); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main1() -{ - var local_0: int; - var $tmp0: int; - var local_1: int; - var $tmp1: int; - - assert {:sourceFile "Class1.cs"} {:sourceLine 86} true; - call $tmp0 := Alloc(); - local_0 := $tmp0; - assert {:sourceFile "Class1.cs"} {:sourceLine 87} true; - $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 88} true; - assert $ArrayContents[local_0][0] == 2; - assert {:sourceFile "Class1.cs"} {:sourceLine 90} true; - call $tmp1 := Alloc(); - local_1 := $tmp1; - assert {:sourceFile "Class1.cs"} {:sourceLine 91} true; - $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 92} true; - assert $ArrayContents[local_1][0] == 1; - assert {:sourceFile "Class1.cs"} {:sourceLine 94} true; - assert $ArrayContents[local_0][0] == 2; - assert {:sourceFile "Class1.cs"} {:sourceLine 95} true; - return; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main2(); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main2() -{ - var $tmp2: int; - var local_0: int; - var $tmp3: int; - - assert {:sourceFile "Class1.cs"} {:sourceLine 100} true; - call $tmp2 := Alloc(); - RegressionTestInput.ClassWithArrayTypes.s := $tmp2; - assert {:sourceFile "Class1.cs"} {:sourceLine 101} true; - $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 102} true; - assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2; - assert {:sourceFile "Class1.cs"} {:sourceLine 104} true; - call $tmp3 := Alloc(); - local_0 := $tmp3; - assert {:sourceFile "Class1.cs"} {:sourceLine 105} true; - $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 106} true; - assert $ArrayContents[local_0][0] == 1; - assert {:sourceFile "Class1.cs"} {:sourceLine 108} true; - assert $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0] == 2; - assert {:sourceFile "Class1.cs"} {:sourceLine 109} true; - return; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int) -{ - var x: int; - - x := x$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 114} true; - $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x := 42]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 115} true; - $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x + 1 := 43]]; - assert {:sourceFile "Class1.cs"} {:sourceLine 116} true; - assert $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x + 1] == $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][x] + 1; - assert {:sourceFile "Class1.cs"} {:sourceLine 117} true; - return; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int); - - - -implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int) -{ - var xs: int; - - xs := xs$in; - if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true)) - { - assert {:sourceFile "Class1.cs"} {:sourceLine 121} true; - $ArrayContents := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := $ArrayContents[$Heap[this, RegressionTestInput.ClassWithArrayTypes.a]][0 := $ArrayContents[xs][0]]]; - } - else - { - } - - assert {:sourceFile "Class1.cs"} {:sourceLine 123} true; - return; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); - - - -procedure System.Object.#ctor(this: int); - - - -implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int) -{ - $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := 0; - call System.Object.#ctor(this); - return; -} - - - -procedure RegressionTestInput.ClassWithArrayTypes.#cctor(); - - - -implementation RegressionTestInput.ClassWithArrayTypes.#cctor() -{ - RegressionTestInput.ClassWithArrayTypes.s := 0; -} - - - -const unique RegressionTestInput.Class0: Type; - -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; - - x := x$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 18} true; - $result := x + 1; - return; -} - - - -procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int); - - - -implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) -{ - var x: int; - var __temp_1: int; - var $tmp4: int; - var local_0: int; - - x := x$in; - $tmp4 := x; - assert $tmp4 != 0; - __temp_1 := 5 / $tmp4; - x := 3; - local_0 := __temp_1 + 3; - assert {:sourceFile "Class1.cs"} {:sourceLine 22} true; - assert (if x == 3 then local_0 <= 8 else false); - 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.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int); - - - -implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int) -{ - var x: int; - var y: int; - - x := x$in; - y := y$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 28} true; - return; -} - - - -procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool); - - - -implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool) -{ - var b: bool; - - b := b$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 29} true; - return; -} - - - -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int); - - - -implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int) -{ - var c: int; - - c := c$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 30} true; - return; -} - - - -procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int); - - - -implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int) -{ - var $tmp5: int; - - assert {:sourceFile "Class1.cs"} {:sourceLine 34} true; - call $tmp5 := RegressionTestInput.Class0.StaticMethod$System.Int32(3); - $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp5; - 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) -{ - assert {:sourceFile "Class1.cs"} {:sourceLine 37} true; - x$out := 3 + RegressionTestInput.Class0.StaticInt; - assert {:sourceFile "Class1.cs"} {:sourceLine 39} true; - $result := x$out; - 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) -{ - x$out := x$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 42} true; - x$out := x$out + 1; - assert {:sourceFile "Class1.cs"} {:sourceLine 43} true; - RegressionTestInput.Class0.StaticInt := x$out; - assert {:sourceFile "Class1.cs"} {:sourceLine 45} true; - $result := x$out; - 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; - - x := x$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 48} true; - x := x + 1; - assert {:sourceFile "Class1.cs"} {:sourceLine 49} true; - RegressionTestInput.Class0.StaticInt := x; - assert {:sourceFile "Class1.cs"} {:sourceLine 51} true; - $result := x; - return; -} - - - -procedure {:RegressionTestInput.Async} 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; - - x := x$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 56} true; - $result := x; - 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 $tmp6: int; - - y := y$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 60} true; - call {:async} $tmp6 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y); - $result := $tmp6; - return; -} - - - -procedure RegressionTestInput.Class0.#ctor(this: int); - - - -implementation RegressionTestInput.Class0.#ctor(this: int) -{ - call System.Object.#ctor(this); - return; -} - - - -procedure RegressionTestInput.Class0.#cctor(); - - - -implementation RegressionTestInput.Class0.#cctor() -{ - RegressionTestInput.Class0.StaticInt := 0; -} - - - -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type; - -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: int; - -const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: int; - -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int); - - - -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int) -{ - assert {:sourceFile "Class1.cs"} {:sourceLine 130} true; - $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x]; - assert {:sourceFile "Class1.cs"} {:sourceLine 131} true; - return; -} - - - -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int); - - - -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int) -{ - $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x] := 0; - $Heap[this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y] := 0; - call System.Object.#ctor(this); - return; -} - - - -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor(); - - - -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#cctor() -{ -} - - - -const unique RegressionTestInput.ClassWithBoolTypes: Type; - -var RegressionTestInput.ClassWithBoolTypes.staticB: bool; - -const unique RegressionTestInput.ClassWithBoolTypes.b: bool; - -procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool); - - - -implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool) -{ - var x: int; - var y: int; - - x := x$in; - y := y$in; - assert {:sourceFile "Class1.cs"} {:sourceLine 70} true; - $result := x < y; - return; -} - - - -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool); - - - -implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool) -{ - var z: bool; - - z := z$in; - $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := false; - assert {:sourceFile "Class1.cs"} {:sourceLine 72} true; - call System.Object.#ctor(this); - assert {:sourceFile "Class1.cs"} {:sourceLine 73} true; - $Heap[this, RegressionTestInput.ClassWithBoolTypes.b] := z; - assert {:sourceFile "Class1.cs"} {:sourceLine 74} true; - if (z) - { - assert {:sourceFile "Class1.cs"} {:sourceLine 74} true; - RegressionTestInput.ClassWithBoolTypes.staticB := z; - } - else - { - } - - return; -} - - - -procedure RegressionTestInput.ClassWithBoolTypes.Main(); - - - -implementation RegressionTestInput.ClassWithBoolTypes.Main() -{ - var $tmp7: bool; - - assert {:sourceFile "Class1.cs"} {:sourceLine 78} true; - call $tmp7 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4); - assert {:sourceFile "Class1.cs"} {:sourceLine 79} true; - return; -} - - - -procedure RegressionTestInput.ClassWithBoolTypes.#cctor(); - - - -implementation RegressionTestInput.ClassWithBoolTypes.#cctor() -{ - RegressionTestInput.ClassWithBoolTypes.staticB := false; -} - - - -const unique RegressionTestInput.AsyncAttribute: Type; - -procedure RegressionTestInput.AsyncAttribute.#ctor(this: int); - - - -procedure System.Attribute.#ctor(this: int); - - - -implementation RegressionTestInput.AsyncAttribute.#ctor(this: int) -{ - call System.Attribute.#ctor(this); - return; -} - - - -procedure RegressionTestInput.AsyncAttribute.#cctor(); - - - -implementation RegressionTestInput.AsyncAttribute.#cctor() -{ -} - - diff --git a/BCT/RegressionTests/TranslationTest/UnitTest0.cs b/BCT/RegressionTests/TranslationTest/UnitTest0.cs index dadeb4e5..99b6e680 100644 --- a/BCT/RegressionTests/TranslationTest/UnitTest0.cs +++ b/BCT/RegressionTests/TranslationTest/UnitTest0.cs @@ -67,21 +67,6 @@ namespace TranslationTest { return s; } - [TestMethod] - 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; @@ -97,21 +82,6 @@ namespace TranslationTest { } } - [TestMethod] - public void TwoDBoxHeap() { - string dir = TestContext.DeploymentDirectory; - var fullPath = Path.Combine(dir, "RegressionTestInput.dll"); - Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.TwoDBoxHeapInput.txt"); - StreamReader reader = new StreamReader(resource); - string expected = reader.ReadToEnd(); - var result = ExecuteTest(fullPath, new TwoDBoxHeap()); - if (result != expected) { - string resultFile = Path.GetFullPath("TwoDBoxHeapOutput.txt"); - File.WriteAllText(resultFile, result); - Assert.Fail("Output didn't match TwoDBoxHeapInput.txt: " + resultFile); - } - } - [TestMethod] public void GeneralHeap() { string dir = TestContext.DeploymentDirectory; -- cgit v1.2.3