From c8c066fc6abad3b522862354d6449c9e31ce7601 Mon Sep 17 00:00:00 2001 From: Mike Barnett Date: Fri, 6 May 2011 08:00:25 -0700 Subject: Cleanup of new LHS simplification and replaced the golden output with the new regression output. --- BCT/BytecodeTranslator/ExpressionTraverser.cs | 59 +--- .../TranslationTest/GeneralHeapInput.txt | 387 +++++++++++--------- .../TranslationTest/SplitFieldsHeapInput.txt | 389 ++++++++++++--------- 3 files changed, 441 insertions(+), 394 deletions(-) diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 81c25cf1..d1af8142 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -659,24 +659,19 @@ namespace BytecodeTranslator public override void Visit(IAssignment assignment) { Contract.Assert(TranslatedExpressions.Count == 0); - - //var localDeclaration = AssignmentSimplifier_FirstTry.Simplify(this.sink.host, assignment.Target); - //if (localDeclaration != null) { - // this.StmtTraverser.Visit(localDeclaration); - //} - #region Transform Right Hand Side ... this.Visit(assignment.Source); Bpl.Expr sourceexp = this.TranslatedExpressions.Pop(); #endregion + // Simplify the LHS so that all nested dereferences and method calls are broken + // up into separate assignments to locals. var blockExpression = AssignmentSimplifier.Simplify(this.sink, assignment.Target); foreach (var s in blockExpression.BlockStatement.Statements) { this.StmtTraverser.Visit(s); } var target = blockExpression.Expression as ITargetExpression; - //var target = assignment.Target; var fieldReference = target.Definition as IFieldReference; @@ -1211,56 +1206,6 @@ namespace BytecodeTranslator } #endregion - /// - /// Actually a mutator! It will downcast and whack if/when it finds the right spot in the tree! - /// If found, replaces the "right-most object" on the left-hand side of an asignment with a local. - /// A local declaration statement is created (and stored in a field of this class) that initializes - /// the local to the part of the tree it replaced. - /// - private class AssignmentSimplifier_FirstTry : BaseCodeTraverser { - IMetadataHost host; - private ILocalDeclarationStatement/*?*/ localDeclarationStatement; - private AssignmentSimplifier_FirstTry(IMetadataHost host) - : base() { - this.host = host; - } - public static ILocalDeclarationStatement/*?*/ Simplify(IMetadataHost host, ITargetExpression targetExpression) { - var a = new AssignmentSimplifier_FirstTry(host); - a.Visit(targetExpression); - return a.localDeclarationStatement; - } - public override void Visit(IBoundExpression boundExpression) { - if (boundExpression.Instance == null) { - this.stopTraversal = true; - return; - } - var loc = new LocalDefinition() { - Name = this.host.NameTable.GetNameFor("_loc"), // TODO: should make the name unique within the method containing the assignment - Type = boundExpression.Type, - }; - var mutableBoundExpression = (BoundExpression)boundExpression; - var init = new LocalDeclarationStatement() { - InitialValue = new BoundExpression(){ - Definition = boundExpression.Definition, - Instance = boundExpression.Instance, - Type = boundExpression.Type, - }, - LocalVariable = loc, - Locations = mutableBoundExpression.Locations, - }; - this.localDeclarationStatement = init; - mutableBoundExpression.Instance = null; - mutableBoundExpression.Definition = loc; - this.stopTraversal = true; - return; - } - - public override void Visit(ITargetExpression targetExpression) { - base.Visit(targetExpression); - } - - } - /// /// This is a rewriter so it must be used on a mutable Code Model!!! /// diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index 0ff36879..98d25303 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -1,29 +1,21 @@ // Copyright (c) 2010, Microsoft Corp. // Bytecode Translator prelude -const null: ref; +type Struct = [Field]Box; -type ref = int; - -type struct = [Field]box; - -type HeapType = [ref,Field]box; +type HeapType = [Ref,Field]Box; function IsGoodHeap(HeapType) : bool; -var $ArrayContents: [int][int]int; - -var $ArrayLength: [int]int; +var $Alloc: [Ref]bool; -var $Alloc: [ref]bool; - -procedure {:inline 1} Alloc() returns (x: ref); +procedure {:inline 1} Alloc() returns (x: Ref); modifies $Alloc; free ensures x != null; -implementation Alloc() returns (x: ref) +implementation Alloc() returns (x: Ref) { assume $Alloc[x] == false; $Alloc[x] := true; @@ -41,21 +33,21 @@ axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x); axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x); -procedure DelegateAdd(a: int, b: int) returns (c: int); +procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref); -implementation DelegateAdd(a: int, b: int) returns (c: int) +implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref) { var m: int; - var o: int; + var o: Ref; - if (a == 0) + if (a == null) { c := b; return; } - else if (b == 0) + else if (b == null) { c := a; return; @@ -72,21 +64,21 @@ implementation DelegateAdd(a: int, b: int) returns (c: int) -procedure DelegateRemove(a: int, b: int) returns (c: int); +procedure DelegateRemove(a: Ref, b: Ref) returns (c: Ref); -implementation DelegateRemove(a: int, b: int) returns (c: int) +implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref) { var m: int; - var o: int; + var o: Ref; - if (a == 0) + if (a == null) { - c := 0; + c := null; return; } - else if (b == 0) + else if (b == null) { c := a; return; @@ -103,13 +95,13 @@ implementation DelegateRemove(a: int, b: int) returns (c: int) -procedure GetFirstElement(i: int) returns (m: int, o: int); +procedure GetFirstElement(i: Ref) returns (m: int, o: Ref); -implementation GetFirstElement(i: int) returns (m: int, o: int) +implementation GetFirstElement(i: Ref) returns (m: int, o: Ref) { - var first: int; + var first: Ref; first := $Next[i][$Head[i]]; m := $Method[i][first]; @@ -118,16 +110,16 @@ implementation GetFirstElement(i: int) returns (m: int, o: int) -procedure DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int); +procedure DelegateAddHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref); -implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int) +implementation DelegateAddHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref) { - var x: int; - var h: int; + var x: Ref; + var h: Ref; - if (oldi == 0) + if (oldi == null) { call i := Alloc(); call x := Alloc(); @@ -150,23 +142,23 @@ implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int) -procedure DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int); +procedure DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref); -implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) +implementation DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref) { - var prev: int; - var iter: int; - var niter: int; + var prev: Ref; + var iter: Ref; + var niter: Ref; i := oldi; - if (i == 0) + if (i == null) { return; } - prev := 0; + prev := null; iter := $Head[i]; while (true) { @@ -184,7 +176,7 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) iter := niter; } - if (prev == 0) + if (prev == null) { return; } @@ -192,7 +184,7 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]]; if ($Next[i][$Head[i]] == $Head[i]) { - i := 0; + i := null; } } @@ -200,53 +192,73 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) var $Heap: HeapType where IsGoodHeap($Heap); -function {:inline true} Read(H: HeapType, o: ref, f: Field) : box +function {:inline true} Read(H: HeapType, o: Ref, f: Field) : Box { H[o, f] } -function {:inline true} Write(H: HeapType, o: ref, f: Field, v: box) : HeapType +function {:inline true} Write(H: HeapType, o: Ref, f: Field, v: Box) : HeapType { H[o, f := v] } +var $ArrayContents: [Ref][int]Box; + +var $ArrayLength: [Ref]int; + type Field; -type box; +type Box; -const unique $DefaultBox: box; +const unique $DefaultBox: Box; -const unique $DefaultStruct: struct; +type Ref; + +const unique null: Ref; type Type; -function Box2Int(box) : int; +const unique $DefaultStruct: Struct; + +function Box2Int(Box) : int; -function Box2Bool(box) : bool; +function Box2Bool(Box) : bool; -function Box2Struct(box) : struct; +function Box2Struct(Box) : Struct; -function Int2Box(int) : box; +function Box2Ref(Box) : Ref; -function Bool2Box(bool) : box; +function Int2Box(int) : Box; -function Struct2Box(struct) : box; +function Bool2Box(bool) : Box; -function $DynamicType(ref) : Type; +function Struct2Box(Struct) : Box; -function $TypeOf(Type) : ref; +function Ref2Box(Ref) : Box; -var $Head: [int]int; +function Struct2Ref(Struct) : Ref; -var $Next: [int][int]int; +function Int2Ref(int) : Ref; -var $Method: [int][int]int; +function Bool2Ref(bool) : Ref; -var $Receiver: [int][int]int; +function $DynamicType(Ref) : Type; + +function $TypeOf(Type) : Ref; + +function $As(Ref, Type) : Ref; + +var $Head: [Ref]Ref; + +var $Next: [Ref][Ref]Ref; + +var $Method: [Ref][Ref]int; + +var $Receiver: [Ref][Ref]Ref; const unique RegressionTestInput.ClassWithArrayTypes: Type; -var RegressionTestInput.ClassWithArrayTypes.s: int; +var RegressionTestInput.ClassWithArrayTypes.s: Ref; const unique RegressionTestInput.ClassWithArrayTypes.a: Field; @@ -256,33 +268,37 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1(); implementation RegressionTestInput.ClassWithArrayTypes.Main1() { - var local_0: int; - var $tmp0: int; + var local_0: Ref; + var $tmp0: Ref; var $tmp1: int; - var local_1: int; var $tmp2: int; - var $tmp3: int; + var local_1: Ref; + var $tmp3: Ref; var $tmp4: int; + var $tmp5: int; + var $tmp6: 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]]; + $tmp1 := Box2Int($ArrayContents[local_0][0]); + $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(2)]]; assert {:sourceFile "Class1.cs"} {:sourceLine 88} true; - $tmp1 := $ArrayContents[local_0][0]; - assert $tmp1 == 2; + $tmp2 := Box2Int($ArrayContents[local_0][0]); + assert $tmp2 == 2; assert {:sourceFile "Class1.cs"} {:sourceLine 90} true; - call $tmp2 := Alloc(); - local_1 := $tmp2; + call $tmp3 := Alloc(); + local_1 := $tmp3; assert {:sourceFile "Class1.cs"} {:sourceLine 91} true; - $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]]; + $tmp4 := Box2Int($ArrayContents[local_1][0]); + $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := Int2Box(1)]]; assert {:sourceFile "Class1.cs"} {:sourceLine 92} true; - $tmp3 := $ArrayContents[local_1][0]; - assert $tmp3 == 1; + $tmp5 := Box2Int($ArrayContents[local_1][0]); + assert $tmp5 == 1; assert {:sourceFile "Class1.cs"} {:sourceLine 94} true; - $tmp4 := $ArrayContents[local_0][0]; - assert $tmp4 == 2; + $tmp6 := Box2Int($ArrayContents[local_0][0]); + assert $tmp6 == 2; assert {:sourceFile "Class1.cs"} {:sourceLine 95} true; return; } @@ -295,78 +311,104 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2(); implementation RegressionTestInput.ClassWithArrayTypes.Main2() { - var $tmp5: int; - var $tmp6: int; - var local_0: int; - var $tmp7: int; + var $tmp7: Ref; var $tmp8: int; var $tmp9: int; + var local_0: Ref; + var $tmp10: Ref; + var $tmp11: int; + var $tmp12: int; + var $tmp13: int; assert {:sourceFile "Class1.cs"} {:sourceLine 100} true; - call $tmp5 := Alloc(); - RegressionTestInput.ClassWithArrayTypes.s := $tmp5; + call $tmp7 := Alloc(); + RegressionTestInput.ClassWithArrayTypes.s := $tmp7; assert {:sourceFile "Class1.cs"} {:sourceLine 101} true; - $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]]; + $tmp8 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]); + $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := Int2Box(2)]]; assert {:sourceFile "Class1.cs"} {:sourceLine 102} true; - $tmp6 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]; - assert $tmp6 == 2; + $tmp9 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]); + assert $tmp9 == 2; assert {:sourceFile "Class1.cs"} {:sourceLine 104} true; - call $tmp7 := Alloc(); - local_0 := $tmp7; + call $tmp10 := Alloc(); + local_0 := $tmp10; assert {:sourceFile "Class1.cs"} {:sourceLine 105} true; - $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]]; + $tmp11 := Box2Int($ArrayContents[local_0][0]); + $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := Int2Box(1)]]; assert {:sourceFile "Class1.cs"} {:sourceLine 106} true; - $tmp8 := $ArrayContents[local_0][0]; - assert $tmp8 == 1; + $tmp12 := Box2Int($ArrayContents[local_0][0]); + assert $tmp12 == 1; assert {:sourceFile "Class1.cs"} {:sourceLine 108} true; - $tmp9 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]; - assert $tmp9 == 2; + $tmp13 := Box2Int($ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]); + assert $tmp13 == 2; assert {:sourceFile "Class1.cs"} {:sourceLine 109} true; return; } -procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int); +procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: Ref, x$in: int); -implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int) +implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: Ref, x$in: int) { var x: int; - var $tmp10: int; - var $tmp11: int; + var _loc0: Ref; + var $tmp14: Ref; + var $tmp15: int; + var _loc1: Ref; + var $tmp16: Ref; + var $tmp17: int; + var $tmp18: Ref; + var $tmp19: int; + var $tmp20: Ref; + var $tmp21: int; x := x$in; assert {:sourceFile "Class1.cs"} {:sourceLine 114} true; - $ArrayContents := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x := 42]]; + $tmp14 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)); + _loc0 := $tmp14; + $tmp15 := Box2Int($ArrayContents[_loc0][x]); + $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][x := Int2Box(42)]]; assert {:sourceFile "Class1.cs"} {:sourceLine 115} true; - $ArrayContents := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x + 1 := 43]]; + $tmp16 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)); + _loc1 := $tmp16; + $tmp17 := Box2Int($ArrayContents[_loc1][x + 1]); + $ArrayContents := $ArrayContents[_loc1 := $ArrayContents[_loc1][x + 1 := Int2Box(43)]]; assert {:sourceFile "Class1.cs"} {:sourceLine 116} true; - $tmp10 := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x + 1]; - $tmp11 := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][x]; - assert $tmp10 == $tmp11 + 1; + $tmp18 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)); + $tmp19 := Box2Int($ArrayContents[$tmp18][x + 1]); + $tmp20 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)); + $tmp21 := Box2Int($ArrayContents[$tmp20][x]); + assert $tmp19 == $tmp21 + 1; assert {:sourceFile "Class1.cs"} {:sourceLine 117} true; return; } -procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int); +procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: Ref, xs$in: Ref); -implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int) +implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: Ref, xs$in: Ref) { - var xs: int; - var $tmp12: int; + var xs: Ref; + var $tmp22: int; + var _loc0: Ref; + var $tmp23: Ref; + var $tmp24: int; xs := xs$in; - if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true)) + if (!(if xs != null then $ArrayLength[xs] <= 0 else true)) { assert {:sourceFile "Class1.cs"} {:sourceLine 121} true; - $tmp12 := $ArrayContents[xs][0]; - $ArrayContents := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][0 := $tmp12]]; + $tmp22 := Box2Int($ArrayContents[xs][0]); + $tmp23 := Box2Ref(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)); + _loc0 := $tmp23; + $tmp24 := Box2Int($ArrayContents[_loc0][0]); + $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][0 := Int2Box($tmp22)]]; } else { @@ -378,17 +420,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t -procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); +procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref); -procedure System.Object.#ctor(this: int); +procedure System.Object.#ctor(this: Ref); -implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int) +implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref) { - $Heap := Write($Heap, this, RegressionTestInput.ClassWithArrayTypes.a, Int2Box(0)); + $Heap := Write($Heap, this, RegressionTestInput.ClassWithArrayTypes.a, Ref2Box(null)); call System.Object.#ctor(this); return; } @@ -401,7 +443,7 @@ procedure RegressionTestInput.ClassWithArrayTypes.#cctor(); implementation RegressionTestInput.ClassWithArrayTypes.#cctor() { - RegressionTestInput.ClassWithArrayTypes.s := 0; + RegressionTestInput.ClassWithArrayTypes.s := null; } @@ -423,11 +465,11 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu -procedure RegressionTestInput.RefParameters.#ctor(this: int); +procedure RegressionTestInput.RefParameters.#ctor(this: Ref); -implementation RegressionTestInput.RefParameters.#ctor(this: int) +implementation RegressionTestInput.RefParameters.#ctor(this: Ref) { call System.Object.#ctor(this); return; @@ -465,21 +507,21 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r -procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int); +procedure RegressionTestInput.Class0.M$System.Int32(this: Ref, x$in: int); -implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) +implementation RegressionTestInput.Class0.M$System.Int32(this: Ref, x$in: int) { var x: int; var __temp_1: int; - var $tmp13: int; + var $tmp25: int; var local_0: int; x := x$in; - $tmp13 := x; - assert $tmp13 != 0; - __temp_1 := 5 / $tmp13; + $tmp25 := x; + assert $tmp25 != 0; + __temp_1 := 5 / $tmp25; x := 3; local_0 := __temp_1 + 3; assert {:sourceFile "Class1.cs"} {:sourceLine 22} true; @@ -494,11 +536,11 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) -procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int); +procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int); -implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int) +implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) { var x: int; var y: int; @@ -511,11 +553,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, -procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool); +procedure RegressionTestInput.Class0.M$System.Boolean(this: Ref, b$in: bool); -implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool) +implementation RegressionTestInput.Class0.M$System.Boolean(this: Ref, b$in: bool) { var b: bool; @@ -526,13 +568,13 @@ implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int); +procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: Ref, c$in: Ref); -implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int) +implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: Ref, c$in: Ref) { - var c: int; + var c: Ref; c := c$in; assert {:sourceFile "Class1.cs"} {:sourceLine 30} true; @@ -541,27 +583,27 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int -procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int); +procedure RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int); -implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int) +implementation RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int) { - var $tmp14: int; + var $tmp26: int; assert {:sourceFile "Class1.cs"} {:sourceLine 34} true; - call $tmp14 := RegressionTestInput.Class0.StaticMethod$System.Int32(3); - $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp14; + call $tmp26 := RegressionTestInput.Class0.StaticMethod$System.Int32(3); + $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp26; return; } -procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int); +procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref) returns (x$out: int, $result: int); -implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int) +implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref) returns (x$out: int, $result: int) { assert {:sourceFile "Class1.cs"} {:sourceLine 37} true; x$out := 3 + RegressionTestInput.Class0.StaticInt; @@ -572,11 +614,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) retu -procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int); +procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: Ref, 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) +implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: Ref, x$in: int) returns (x$out: int, $result: int) { x$out := x$in; assert {:sourceFile "Class1.cs"} {:sourceLine 42} true; @@ -590,11 +632,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in -procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int); +procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: Ref, x$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: Ref, x$in: int) returns ($result: int) { var x: int; @@ -610,11 +652,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int -procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int); +procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: Ref, x$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: Ref, x$in: int) returns ($result: int) { var x: int; @@ -626,29 +668,29 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho -procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int); +procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$in: int) returns ($result: int) { var y: int; - var $tmp15: int; + var $tmp27: int; y := y$in; assert {:sourceFile "Class1.cs"} {:sourceLine 60} true; - call {:async} $tmp15 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y); - $result := $tmp15; + call {:async} $tmp27 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y); + $result := $tmp27; return; } -procedure RegressionTestInput.Class0.#ctor(this: int); +procedure RegressionTestInput.Class0.#ctor(this: Ref); -implementation RegressionTestInput.Class0.#ctor(this: int) +implementation RegressionTestInput.Class0.#ctor(this: Ref) { call System.Object.#ctor(this); return; @@ -673,25 +715,28 @@ const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field; const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field; -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int); +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref); -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int) +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref) { + var $tmp28: int; + assert {:sourceFile "Class1.cs"} {:sourceLine 130} true; - $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x)))); + $tmp28 := Box2Int(Read($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x)); + $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box($tmp28)); assert {:sourceFile "Class1.cs"} {:sourceLine 131} true; return; } -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int); +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref); -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int) +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref) { $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0)); $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0)); @@ -735,11 +780,11 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool); +procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: Ref, z$in: bool); -implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool) +implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: Ref, z$in: bool) { var z: bool; @@ -770,10 +815,10 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main(); implementation RegressionTestInput.ClassWithBoolTypes.Main() { - var $tmp16: bool; + var $tmp29: bool; assert {:sourceFile "Class1.cs"} {:sourceLine 78} true; - call $tmp16 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4); + call $tmp29 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4); assert {:sourceFile "Class1.cs"} {:sourceLine 79} true; return; } @@ -799,15 +844,15 @@ const unique RegressionTestInput.S.b: Field; const unique RegressionTestInput.AsyncAttribute: Type; -procedure RegressionTestInput.AsyncAttribute.#ctor(this: int); +procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref); -procedure System.Attribute.#ctor(this: int); +procedure System.Attribute.#ctor(this: Ref); -implementation RegressionTestInput.AsyncAttribute.#ctor(this: int) +implementation RegressionTestInput.AsyncAttribute.#ctor(this: Ref) { call System.Attribute.#ctor(this); return; @@ -827,20 +872,24 @@ implementation RegressionTestInput.AsyncAttribute.#cctor() const unique RegressionTestInput.CreateStruct: Type; -procedure RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box); +procedure RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box); -implementation RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box) +implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box) { - var local_0: [Field]box; + var local_0: [Field]Box; + var $tmp30: int; + var $tmp31: bool; assert {:sourceFile "Class1.cs"} {:sourceLine 141} true; local_0 := $DefaultStruct; assert {:sourceFile "Class1.cs"} {:sourceLine 142} true; - assert Box2Int(local_0[RegressionTestInput.S.x]) == 0; + $tmp30 := Box2Int(local_0[RegressionTestInput.S.x]); + assert $tmp30 == 0; assert {:sourceFile "Class1.cs"} {:sourceLine 143} true; - assert !Box2Bool(local_0[RegressionTestInput.S.b]); + $tmp31 := Box2Bool(local_0[RegressionTestInput.S.b]); + assert !$tmp31; assert {:sourceFile "Class1.cs"} {:sourceLine 145} true; $result := local_0; return; @@ -848,19 +897,21 @@ implementation RegressionTestInput.CreateStruct.Create(this: int) returns ($resu -procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box); +procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box); -implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box) +implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box) { - var s: [Field]box; + var s: [Field]Box; + var $tmp32: int; s := s$in; assert {:sourceFile "Class1.cs"} {:sourceLine 147} true; s := s[RegressionTestInput.S.x := Int2Box(3)]; assert {:sourceFile "Class1.cs"} {:sourceLine 148} true; - assert Box2Int(s[RegressionTestInput.S.x]) == 3; + $tmp32 := Box2Int(s[RegressionTestInput.S.x]); + assert $tmp32 == 3; assert {:sourceFile "Class1.cs"} {:sourceLine 150} true; $result := s; return; @@ -868,11 +919,11 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes -procedure RegressionTestInput.CreateStruct.#ctor(this: int); +procedure RegressionTestInput.CreateStruct.#ctor(this: Ref); -implementation RegressionTestInput.CreateStruct.#ctor(this: int) +implementation RegressionTestInput.CreateStruct.#ctor(this: Ref) { call System.Object.#ctor(this); return; diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index 53e9a8c3..6e450f38 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -1,31 +1,23 @@ // Copyright (c) 2010, Microsoft Corp. // Bytecode Translator prelude -const null: int; +type Struct = [Field]Box; -type ref = int; - -type struct = [Field]box; - -type HeapType = [int,int]int; +type HeapType = [Ref,Field]Box; var $Heap: HeapType where IsGoodHeap($Heap); function IsGoodHeap(HeapType) : bool; -var $ArrayContents: [int][int]int; - -var $ArrayLength: [int]int; +var $Alloc: [Ref]bool; -var $Alloc: [int]bool; - -procedure {:inline 1} Alloc() returns (x: int); +procedure {:inline 1} Alloc() returns (x: Ref); modifies $Alloc; - free ensures x != 0; + free ensures x != null; -implementation Alloc() returns (x: int) +implementation Alloc() returns (x: Ref) { assume $Alloc[x] == false; $Alloc[x] := true; @@ -43,21 +35,21 @@ axiom (forall x: int :: { Int2Box(x) } Box2Int(Int2Box(x)) == x); axiom (forall x: bool :: { Bool2Box(x) } Box2Bool(Bool2Box(x)) == x); -procedure DelegateAdd(a: int, b: int) returns (c: int); +procedure DelegateAdd(a: Ref, b: Ref) returns (c: Ref); -implementation DelegateAdd(a: int, b: int) returns (c: int) +implementation DelegateAdd(a: Ref, b: Ref) returns (c: Ref) { var m: int; - var o: int; + var o: Ref; - if (a == 0) + if (a == null) { c := b; return; } - else if (b == 0) + else if (b == null) { c := a; return; @@ -74,21 +66,21 @@ implementation DelegateAdd(a: int, b: int) returns (c: int) -procedure DelegateRemove(a: int, b: int) returns (c: int); +procedure DelegateRemove(a: Ref, b: Ref) returns (c: Ref); -implementation DelegateRemove(a: int, b: int) returns (c: int) +implementation DelegateRemove(a: Ref, b: Ref) returns (c: Ref) { var m: int; - var o: int; + var o: Ref; - if (a == 0) + if (a == null) { - c := 0; + c := null; return; } - else if (b == 0) + else if (b == null) { c := a; return; @@ -105,13 +97,13 @@ implementation DelegateRemove(a: int, b: int) returns (c: int) -procedure GetFirstElement(i: int) returns (m: int, o: int); +procedure GetFirstElement(i: Ref) returns (m: int, o: Ref); -implementation GetFirstElement(i: int) returns (m: int, o: int) +implementation GetFirstElement(i: Ref) returns (m: int, o: Ref) { - var first: int; + var first: Ref; first := $Next[i][$Head[i]]; m := $Method[i][first]; @@ -120,16 +112,16 @@ implementation GetFirstElement(i: int) returns (m: int, o: int) -procedure DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int); +procedure DelegateAddHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref); -implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int) +implementation DelegateAddHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref) { - var x: int; - var h: int; + var x: Ref; + var h: Ref; - if (oldi == 0) + if (oldi == null) { call i := Alloc(); call x := Alloc(); @@ -152,23 +144,23 @@ implementation DelegateAddHelper(oldi: int, m: int, o: int) returns (i: int) -procedure DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int); +procedure DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref); -implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) +implementation DelegateRemoveHelper(oldi: Ref, m: int, o: Ref) returns (i: Ref) { - var prev: int; - var iter: int; - var niter: int; + var prev: Ref; + var iter: Ref; + var niter: Ref; i := oldi; - if (i == 0) + if (i == null) { return; } - prev := 0; + prev := null; iter := $Head[i]; while (true) { @@ -186,7 +178,7 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) iter := niter; } - if (prev == 0) + if (prev == null) { return; } @@ -194,51 +186,71 @@ implementation DelegateRemoveHelper(oldi: int, m: int, o: int) returns (i: int) $Next[i] := $Next[i][prev := $Next[i][$Next[i][prev]]]; if ($Next[i][$Head[i]] == $Head[i]) { - i := 0; + i := null; } } +var $ArrayContents: [Ref][int]Box; + +var $ArrayLength: [Ref]int; + type Field; -type box; +type Box; + +const unique $DefaultBox: Box; -const unique $DefaultBox: box; +type Ref; -const unique $DefaultStruct: struct; +const unique null: Ref; type Type; -function Box2Int(box) : int; +const unique $DefaultStruct: Struct; + +function Box2Int(Box) : int; + +function Box2Bool(Box) : bool; -function Box2Bool(box) : bool; +function Box2Struct(Box) : Struct; -function Box2Struct(box) : struct; +function Box2Ref(Box) : Ref; -function Int2Box(int) : box; +function Int2Box(int) : Box; -function Bool2Box(bool) : box; +function Bool2Box(bool) : Box; -function Struct2Box(struct) : box; +function Struct2Box(Struct) : Box; -function $DynamicType(ref) : Type; +function Ref2Box(Ref) : Box; -function $TypeOf(Type) : ref; +function Struct2Ref(Struct) : Ref; -var $Head: [int]int; +function Int2Ref(int) : Ref; -var $Next: [int][int]int; +function Bool2Ref(bool) : Ref; -var $Method: [int][int]int; +function $DynamicType(Ref) : Type; -var $Receiver: [int][int]int; +function $TypeOf(Type) : Ref; + +function $As(Ref, Type) : Ref; + +var $Head: [Ref]Ref; + +var $Next: [Ref][Ref]Ref; + +var $Method: [Ref][Ref]int; + +var $Receiver: [Ref][Ref]Ref; const unique RegressionTestInput.ClassWithArrayTypes: Type; -var RegressionTestInput.ClassWithArrayTypes.s: int; +var RegressionTestInput.ClassWithArrayTypes.s: Ref; -var RegressionTestInput.ClassWithArrayTypes.a: [int]int; +var RegressionTestInput.ClassWithArrayTypes.a: [Ref]Ref; procedure RegressionTestInput.ClassWithArrayTypes.Main1(); @@ -246,33 +258,37 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main1(); implementation RegressionTestInput.ClassWithArrayTypes.Main1() { - var local_0: int; - var $tmp0: int; + var local_0: Ref; + var $tmp0: Ref; var $tmp1: int; - var local_1: int; var $tmp2: int; - var $tmp3: int; + var local_1: Ref; + var $tmp3: Ref; var $tmp4: int; + var $tmp5: int; + var $tmp6: int; assert {:sourceFile "Class1.cs"} {:sourceLine 86} true; call $tmp0 := Alloc(); local_0 := $tmp0; assert {:sourceFile "Class1.cs"} {:sourceLine 87} true; + $tmp1 := $ArrayContents[local_0][0]; $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 2]]; assert {:sourceFile "Class1.cs"} {:sourceLine 88} true; - $tmp1 := $ArrayContents[local_0][0]; - assert $tmp1 == 2; + $tmp2 := $ArrayContents[local_0][0]; + assert $tmp2 == 2; assert {:sourceFile "Class1.cs"} {:sourceLine 90} true; - call $tmp2 := Alloc(); - local_1 := $tmp2; + call $tmp3 := Alloc(); + local_1 := $tmp3; assert {:sourceFile "Class1.cs"} {:sourceLine 91} true; + $tmp4 := $ArrayContents[local_1][0]; $ArrayContents := $ArrayContents[local_1 := $ArrayContents[local_1][0 := 1]]; assert {:sourceFile "Class1.cs"} {:sourceLine 92} true; - $tmp3 := $ArrayContents[local_1][0]; - assert $tmp3 == 1; + $tmp5 := $ArrayContents[local_1][0]; + assert $tmp5 == 1; assert {:sourceFile "Class1.cs"} {:sourceLine 94} true; - $tmp4 := $ArrayContents[local_0][0]; - assert $tmp4 == 2; + $tmp6 := $ArrayContents[local_0][0]; + assert $tmp6 == 2; assert {:sourceFile "Class1.cs"} {:sourceLine 95} true; return; } @@ -285,78 +301,104 @@ procedure RegressionTestInput.ClassWithArrayTypes.Main2(); implementation RegressionTestInput.ClassWithArrayTypes.Main2() { - var $tmp5: int; - var $tmp6: int; - var local_0: int; - var $tmp7: int; + var $tmp7: Ref; var $tmp8: int; var $tmp9: int; + var local_0: Ref; + var $tmp10: Ref; + var $tmp11: int; + var $tmp12: int; + var $tmp13: int; assert {:sourceFile "Class1.cs"} {:sourceLine 100} true; - call $tmp5 := Alloc(); - RegressionTestInput.ClassWithArrayTypes.s := $tmp5; + call $tmp7 := Alloc(); + RegressionTestInput.ClassWithArrayTypes.s := $tmp7; assert {:sourceFile "Class1.cs"} {:sourceLine 101} true; + $tmp8 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]; $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0 := 2]]; assert {:sourceFile "Class1.cs"} {:sourceLine 102} true; - $tmp6 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]; - assert $tmp6 == 2; + $tmp9 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]; + assert $tmp9 == 2; assert {:sourceFile "Class1.cs"} {:sourceLine 104} true; - call $tmp7 := Alloc(); - local_0 := $tmp7; + call $tmp10 := Alloc(); + local_0 := $tmp10; assert {:sourceFile "Class1.cs"} {:sourceLine 105} true; + $tmp11 := $ArrayContents[local_0][0]; $ArrayContents := $ArrayContents[local_0 := $ArrayContents[local_0][0 := 1]]; assert {:sourceFile "Class1.cs"} {:sourceLine 106} true; - $tmp8 := $ArrayContents[local_0][0]; - assert $tmp8 == 1; + $tmp12 := $ArrayContents[local_0][0]; + assert $tmp12 == 1; assert {:sourceFile "Class1.cs"} {:sourceLine 108} true; - $tmp9 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]; - assert $tmp9 == 2; + $tmp13 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.s][0]; + assert $tmp13 == 2; assert {:sourceFile "Class1.cs"} {:sourceLine 109} true; return; } -procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int); +procedure RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: Ref, x$in: int); -implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: int, x$in: int) +implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: Ref, x$in: int) { var x: int; - var $tmp10: int; - var $tmp11: int; + var _loc0: Ref; + var $tmp14: Ref; + var $tmp15: int; + var _loc1: Ref; + var $tmp16: Ref; + var $tmp17: int; + var $tmp18: Ref; + var $tmp19: int; + var $tmp20: Ref; + var $tmp21: int; x := x$in; assert {:sourceFile "Class1.cs"} {:sourceLine 114} true; - $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this] := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x := 42]]; + $tmp14 := RegressionTestInput.ClassWithArrayTypes.a[this]; + _loc0 := $tmp14; + $tmp15 := $ArrayContents[_loc0][x]; + $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][x := 42]]; assert {:sourceFile "Class1.cs"} {:sourceLine 115} true; - $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this] := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x + 1 := 43]]; + $tmp16 := RegressionTestInput.ClassWithArrayTypes.a[this]; + _loc1 := $tmp16; + $tmp17 := $ArrayContents[_loc1][x + 1]; + $ArrayContents := $ArrayContents[_loc1 := $ArrayContents[_loc1][x + 1 := 43]]; assert {:sourceFile "Class1.cs"} {:sourceLine 116} true; - $tmp10 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x + 1]; - $tmp11 := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][x]; - assert $tmp10 == $tmp11 + 1; + $tmp18 := RegressionTestInput.ClassWithArrayTypes.a[this]; + $tmp19 := $ArrayContents[$tmp18][x + 1]; + $tmp20 := RegressionTestInput.ClassWithArrayTypes.a[this]; + $tmp21 := $ArrayContents[$tmp20][x]; + assert $tmp19 == $tmp21 + 1; assert {:sourceFile "Class1.cs"} {:sourceLine 117} true; return; } -procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int); +procedure RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: Ref, xs$in: Ref); -implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: int, xs$in: int) +implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(this: Ref, xs$in: Ref) { - var xs: int; - var $tmp12: int; + var xs: Ref; + var $tmp22: int; + var _loc0: Ref; + var $tmp23: Ref; + var $tmp24: int; xs := xs$in; - if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true)) + if (!(if xs != null then $ArrayLength[xs] <= 0 else true)) { assert {:sourceFile "Class1.cs"} {:sourceLine 121} true; - $tmp12 := $ArrayContents[xs][0]; - $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this] := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][0 := $tmp12]]; + $tmp22 := $ArrayContents[xs][0]; + $tmp23 := RegressionTestInput.ClassWithArrayTypes.a[this]; + _loc0 := $tmp23; + $tmp24 := $ArrayContents[_loc0][0]; + $ArrayContents := $ArrayContents[_loc0 := $ArrayContents[_loc0][0 := $tmp22]]; } else { @@ -368,17 +410,17 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t -procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); +procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref); -procedure System.Object.#ctor(this: int); +procedure System.Object.#ctor(this: Ref); -implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int) +implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: Ref) { - RegressionTestInput.ClassWithArrayTypes.a[this] := 0; + RegressionTestInput.ClassWithArrayTypes.a[this] := null; call System.Object.#ctor(this); return; } @@ -391,7 +433,7 @@ procedure RegressionTestInput.ClassWithArrayTypes.#cctor(); implementation RegressionTestInput.ClassWithArrayTypes.#cctor() { - RegressionTestInput.ClassWithArrayTypes.s := 0; + RegressionTestInput.ClassWithArrayTypes.s := null; } @@ -413,11 +455,11 @@ implementation RegressionTestInput.RefParameters.M$System.Int32$(x$in: int) retu -procedure RegressionTestInput.RefParameters.#ctor(this: int); +procedure RegressionTestInput.RefParameters.#ctor(this: Ref); -implementation RegressionTestInput.RefParameters.#ctor(this: int) +implementation RegressionTestInput.RefParameters.#ctor(this: Ref) { call System.Object.#ctor(this); return; @@ -455,21 +497,21 @@ implementation RegressionTestInput.Class0.StaticMethod$System.Int32(x$in: int) r -procedure RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int); +procedure RegressionTestInput.Class0.M$System.Int32(this: Ref, x$in: int); -implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) +implementation RegressionTestInput.Class0.M$System.Int32(this: Ref, x$in: int) { var x: int; var __temp_1: int; - var $tmp13: int; + var $tmp25: int; var local_0: int; x := x$in; - $tmp13 := x; - assert $tmp13 != 0; - __temp_1 := 5 / $tmp13; + $tmp25 := x; + assert $tmp25 != 0; + __temp_1 := 5 / $tmp25; x := 3; local_0 := __temp_1 + 3; assert {:sourceFile "Class1.cs"} {:sourceLine 22} true; @@ -484,11 +526,11 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) -procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int); +procedure RegressionTestInput.Class0.M$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int); -implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, x$in: int, y$in: int) +implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: Ref, x$in: int, y$in: int) { var x: int; var y: int; @@ -501,11 +543,11 @@ implementation RegressionTestInput.Class0.M$System.Int32$System.Int32(this: int, -procedure RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool); +procedure RegressionTestInput.Class0.M$System.Boolean(this: Ref, b$in: bool); -implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool) +implementation RegressionTestInput.Class0.M$System.Boolean(this: Ref, b$in: bool) { var b: bool; @@ -516,13 +558,13 @@ implementation RegressionTestInput.Class0.M$System.Boolean(this: int, b$in: bool -procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int); +procedure RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: Ref, c$in: Ref); -implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int, c$in: int) +implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: Ref, c$in: Ref) { - var c: int; + var c: Ref; c := c$in; assert {:sourceFile "Class1.cs"} {:sourceLine 30} true; @@ -531,27 +573,27 @@ implementation RegressionTestInput.Class0.M$RegressionTestInput.Class0(this: int -procedure RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int); +procedure RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int); -implementation RegressionTestInput.Class0.NonVoid(this: int) returns ($result: int) +implementation RegressionTestInput.Class0.NonVoid(this: Ref) returns ($result: int) { - var $tmp14: int; + var $tmp26: int; assert {:sourceFile "Class1.cs"} {:sourceLine 34} true; - call $tmp14 := RegressionTestInput.Class0.StaticMethod$System.Int32(3); - $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp14; + call $tmp26 := RegressionTestInput.Class0.StaticMethod$System.Int32(3); + $result := 3 + RegressionTestInput.Class0.StaticInt + $tmp26; return; } -procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int); +procedure RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref) returns (x$out: int, $result: int); -implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) returns (x$out: int, $result: int) +implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: Ref) returns (x$out: int, $result: int) { assert {:sourceFile "Class1.cs"} {:sourceLine 37} true; x$out := 3 + RegressionTestInput.Class0.StaticInt; @@ -562,11 +604,11 @@ implementation RegressionTestInput.Class0.OutParam$System.Int32$(this: int) retu -procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in: int) returns (x$out: int, $result: int); +procedure RegressionTestInput.Class0.RefParam$System.Int32$(this: Ref, 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) +implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: Ref, x$in: int) returns (x$out: int, $result: int) { x$out := x$in; assert {:sourceFile "Class1.cs"} {:sourceLine 42} true; @@ -580,11 +622,11 @@ implementation RegressionTestInput.Class0.RefParam$System.Int32$(this: int, x$in -procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int); +procedure RegressionTestInput.Class0.AssignToInParam$System.Int32(this: Ref, x$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int, x$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: Ref, x$in: int) returns ($result: int) { var x: int; @@ -600,11 +642,11 @@ implementation RegressionTestInput.Class0.AssignToInParam$System.Int32(this: int -procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int); +procedure {:RegressionTestInput.Async} RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: Ref, x$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: int, x$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this: Ref, x$in: int) returns ($result: int) { var x: int; @@ -616,29 +658,29 @@ implementation RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMetho -procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int); +procedure RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$in: int) returns ($result: int); -implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: int, y$in: int) returns ($result: int) +implementation RegressionTestInput.Class0.CallAsyncMethod$System.Int32(this: Ref, y$in: int) returns ($result: int) { var y: int; - var $tmp15: int; + var $tmp27: int; y := y$in; assert {:sourceFile "Class1.cs"} {:sourceLine 60} true; - call {:async} $tmp15 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y); - $result := $tmp15; + call {:async} $tmp27 := RegressionTestInput.Class0.MethodThatRepresentsAnAynchronousMethod$System.Int32(this, y); + $result := $tmp27; return; } -procedure RegressionTestInput.Class0.#ctor(this: int); +procedure RegressionTestInput.Class0.#ctor(this: Ref); -implementation RegressionTestInput.Class0.#ctor(this: int) +implementation RegressionTestInput.Class0.#ctor(this: Ref) { call System.Object.#ctor(this); return; @@ -659,29 +701,32 @@ implementation RegressionTestInput.Class0.#cctor() const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type; -var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [int]int; +var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [Ref]int; -var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [int]int; +var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [Ref]int; -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int); +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref); -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int) +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: Ref) { + var $tmp28: int; + assert {:sourceFile "Class1.cs"} {:sourceLine 130} true; - RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this]; + $tmp28 := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this]; + RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := $tmp28; assert {:sourceFile "Class1.cs"} {:sourceLine 131} true; return; } -procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int); +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref); -implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int) +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: Ref) { RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this] := 0; RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := 0; @@ -705,7 +750,7 @@ const unique RegressionTestInput.ClassWithBoolTypes: Type; var RegressionTestInput.ClassWithBoolTypes.staticB: bool; -var RegressionTestInput.ClassWithBoolTypes.b: [int]bool; +var RegressionTestInput.ClassWithBoolTypes.b: [Ref]bool; procedure RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(x$in: int, y$in: int) returns ($result: bool); @@ -725,11 +770,11 @@ implementation RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int3 -procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool); +procedure RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: Ref, z$in: bool); -implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: int, z$in: bool) +implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: Ref, z$in: bool) { var z: bool; @@ -760,10 +805,10 @@ procedure RegressionTestInput.ClassWithBoolTypes.Main(); implementation RegressionTestInput.ClassWithBoolTypes.Main() { - var $tmp16: bool; + var $tmp29: bool; assert {:sourceFile "Class1.cs"} {:sourceLine 78} true; - call $tmp16 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4); + call $tmp29 := RegressionTestInput.ClassWithBoolTypes.M$System.Int32$System.Int32(3, 4); assert {:sourceFile "Class1.cs"} {:sourceLine 79} true; return; } @@ -783,21 +828,21 @@ implementation RegressionTestInput.ClassWithBoolTypes.#cctor() const unique RegressionTestInput.S: Type; -var RegressionTestInput.S.x: [int]int; +var RegressionTestInput.S.x: [Ref]int; -var RegressionTestInput.S.b: [int]bool; +var RegressionTestInput.S.b: [Ref]bool; const unique RegressionTestInput.AsyncAttribute: Type; -procedure RegressionTestInput.AsyncAttribute.#ctor(this: int); +procedure RegressionTestInput.AsyncAttribute.#ctor(this: Ref); -procedure System.Attribute.#ctor(this: int); +procedure System.Attribute.#ctor(this: Ref); -implementation RegressionTestInput.AsyncAttribute.#ctor(this: int) +implementation RegressionTestInput.AsyncAttribute.#ctor(this: Ref) { call System.Attribute.#ctor(this); return; @@ -817,20 +862,24 @@ implementation RegressionTestInput.AsyncAttribute.#cctor() const unique RegressionTestInput.CreateStruct: Type; -procedure RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box); +procedure RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box); -implementation RegressionTestInput.CreateStruct.Create(this: int) returns ($result: [Field]box) +implementation RegressionTestInput.CreateStruct.Create(this: Ref) returns ($result: [Field]Box) { - var local_0: [Field]box; + var local_0: [Field]Box; + var $tmp30: int; + var $tmp31: bool; assert {:sourceFile "Class1.cs"} {:sourceLine 141} true; local_0 := $DefaultStruct; assert {:sourceFile "Class1.cs"} {:sourceLine 142} true; - assert local_0[RegressionTestInput.S.x] == 0; + $tmp30 := local_0[RegressionTestInput.S.x]; + assert $tmp30 == 0; assert {:sourceFile "Class1.cs"} {:sourceLine 143} true; - assert !local_0[RegressionTestInput.S.b]; + $tmp31 := local_0[RegressionTestInput.S.b]; + assert !$tmp31; assert {:sourceFile "Class1.cs"} {:sourceLine 145} true; $result := local_0; return; @@ -838,19 +887,21 @@ implementation RegressionTestInput.CreateStruct.Create(this: int) returns ($resu -procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box); +procedure RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box); -implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: int, s$in: [Field]box) returns ($result: [Field]box) +implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTestInput.S(this: Ref, s$in: [Field]Box) returns ($result: [Field]Box) { - var s: [Field]box; + var s: [Field]Box; + var $tmp32: int; s := s$in; assert {:sourceFile "Class1.cs"} {:sourceLine 147} true; s[RegressionTestInput.S.x] := 3; assert {:sourceFile "Class1.cs"} {:sourceLine 148} true; - assert s[RegressionTestInput.S.x] == 3; + $tmp32 := s[RegressionTestInput.S.x]; + assert $tmp32 == 3; assert {:sourceFile "Class1.cs"} {:sourceLine 150} true; $result := s; return; @@ -858,11 +909,11 @@ implementation RegressionTestInput.CreateStruct.AssignThreeToSDotX$RegressionTes -procedure RegressionTestInput.CreateStruct.#ctor(this: int); +procedure RegressionTestInput.CreateStruct.#ctor(this: Ref); -implementation RegressionTestInput.CreateStruct.#ctor(this: int) +implementation RegressionTestInput.CreateStruct.#ctor(this: Ref) { call System.Object.#ctor(this); return; -- cgit v1.2.3