From 1f3f0ad4cb1af0a36f2596b31acac0c084b312d7 Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Tue, 1 Mar 2011 19:17:17 +0000 Subject: Fixed many bugs. Ctors now initialize all fields to default (null-equivalent) values. Generate procedures for interface methods. Translate enums just by ignoring them and using the integers that they really are. --- BCT/BytecodeTranslator/ExpressionTraverser.cs | 22 +++--- BCT/BytecodeTranslator/Heap.cs | 2 + BCT/BytecodeTranslator/MetadataTraverser.cs | 78 ++++++++++++++++++---- BCT/BytecodeTranslator/Sink.cs | 33 +++++---- BCT/RegressionTests/RegressionTestInput/Class1.cs | 8 +++ .../TranslationTest/GeneralHeapInput.txt | 64 +++++++++++++++--- .../TranslationTest/SplitFieldsHeapInput.txt | 62 ++++++++++++++--- .../TranslationTest/TwoDBoxHeapInput.txt | 62 ++++++++++++++--- .../TranslationTest/TwoDIntHeapInput.txt | 62 ++++++++++++++--- 9 files changed, 324 insertions(+), 69 deletions(-) diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 1c401873..13cb3552 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -360,7 +360,9 @@ namespace BytecodeTranslator { var bplType = TranslationHelper.CciTypeToBoogie(constant.Type); if (bplType == Bpl.Type.Int) { - TranslatedExpressions.Push(Bpl.Expr.Literal(0)); + var lit = Bpl.Expr.Literal(0); + lit.Type = Bpl.Type.Int; + TranslatedExpressions.Push(lit); } else if (bplType == Bpl.Type.Bool) { TranslatedExpressions.Push(Bpl.Expr.False); } else { @@ -374,20 +376,24 @@ namespace BytecodeTranslator else if (constant.Value is string) { throw new NotImplementedException("Strings are not translated"); - } - else - { + } else { // TODO: (mschaef) hack - TranslatedExpressions.Push(Bpl.Expr.Literal((int)constant.Value)); + var lit = Bpl.Expr.Literal((int)constant.Value); + lit.Type = Bpl.Type.Int; + TranslatedExpressions.Push(lit); } } public override void Visit(IDefaultValue defaultValue) { var bplType = TranslationHelper.CciTypeToBoogie(defaultValue.Type); if (bplType == Bpl.Type.Int) { - TranslatedExpressions.Push(Bpl.Expr.Literal(0)); + var lit = Bpl.Expr.Literal(0); + lit.Type = Bpl.Type.Int; + TranslatedExpressions.Push(lit); } else if (bplType == Bpl.Type.Bool) { - TranslatedExpressions.Push(Bpl.Expr.False); + var lit = Bpl.Expr.False; + lit.Type = Bpl.Type.Bool; + TranslatedExpressions.Push(lit); } else { throw new NotImplementedException("Don't know how to translate type"); } @@ -444,7 +450,7 @@ namespace BytecodeTranslator Bpl.IToken cloc = methodCall.Token(); // meeting a constructor is always something special - if (resolvedMethod.IsConstructor) + if (false && resolvedMethod.IsConstructor) { // Todo: do something with the constructor call } diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index ee5206db..9018884b 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -414,6 +414,7 @@ procedure {:inline 1} Alloc() returns (x: int) new Bpl.FunctionCall(conversion), new Bpl.ExprSeq(selectExpr) ); + callExpr.Type = f.Type; return callExpr; } @@ -631,6 +632,7 @@ procedure {:inline 1} Alloc() returns (x: ref) new Bpl.FunctionCall(conversion), new Bpl.ExprSeq(callRead) ); + callExpr.Type = boogieType; return callExpr; } diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 440e829a..5b05a6bd 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -103,7 +103,7 @@ namespace BytecodeTranslator { out_count++; formalMap.Add(formal, mp); } - this.sink.FormalMap = formalMap; +// this.sink.FormalMap = formalMap; #region Look for Returnvalue if (invokeMethod.Type.TypeCode != PrimitiveTypeCode.Void) @@ -240,9 +240,15 @@ namespace BytecodeTranslator { base.Visit(typeDefinition); } else if (typeDefinition.IsDelegate) { sink.AddDelegateType(typeDefinition); + } else if (typeDefinition.IsInterface) { + sink.FindOrCreateType(typeDefinition); + base.Visit(typeDefinition); + } else if (typeDefinition.IsEnum) { + return; // enums just are translated as ints } else { - Console.WriteLine("Non-Class {0} was found", typeDefinition); - throw new NotImplementedException(String.Format("Non-Class Type {0} is not yet supported.", typeDefinition.ToString())); + Console.WriteLine("Unknown kind of type definition '{0}' was found", + TypeHelper.GetTypeName(typeDefinition)); + throw new NotImplementedException(String.Format("Unknown kind of type definition '{0}'.", TypeHelper.GetTypeName(typeDefinition))); } } @@ -260,19 +266,22 @@ namespace BytecodeTranslator { this.sink.BeginMethod(); - var proc = this.sink.FindOrCreateProcedure(method, method.IsStatic); + var procAndFormalMap = this.sink.FindOrCreateProcedureAndReturnProcAndFormalMap(method, method.IsStatic); - try { + if (method.IsAbstract) { // we're done, just define the procedure + return; + } - if (method.IsAbstract) { - throw new NotImplementedException("abstract methods are not yet implemented"); - } + var proc = procAndFormalMap.Item1; + var formalMap = procAndFormalMap.Item2; + + try { StatementTraverser stmtTraverser = this.factory.MakeStatementTraverser(this.sink, this.PdbReader); - #region Add assignements from In-Params to local-Params + #region Add assignments from In-Params to local-Params - foreach (MethodParameter mparam in this.sink.FormalMap.Values) { + foreach (MethodParameter mparam in formalMap.Values) { if (mparam.inParameterCopy != null) { Bpl.IToken tok = method.Token(); stmtTraverser.StmtBuilder.Add(Bpl.Cmd.SimpleAssign(tok, @@ -283,6 +292,26 @@ namespace BytecodeTranslator { #endregion + #region For non-deferring ctors, initialize all fields to null-equivalent values + if (method.IsConstructor) { + var smb = method.Body as ISourceMethodBody; + if (smb != null && !FindCtorCall.IsDeferringCtor(method, smb.Block)) { + + var inits = new List(); + var thisExp = new ThisReference() { Type = method.ContainingTypeDefinition, }; + foreach (var f in method.ContainingTypeDefinition.Fields) { + var a = new Assignment() { + Source = new DefaultValue() { Type = f.Type, }, + Target = new TargetExpression() { Definition = f, Instance = thisExp, Type = f.Type }, + Type = f.Type, + }; + inits.Add(new ExpressionStatement() { Expression = a, }); + } + new BlockStatement() { Statements = inits, }.Dispatch(stmtTraverser); + } + } + #endregion + try { method.Body.Dispatch(stmtTraverser); } catch (TranslationException te) { @@ -293,7 +322,7 @@ namespace BytecodeTranslator { #region Create Local Vars For Implementation List vars = new List(); - foreach (MethodParameter mparam in this.sink.FormalMap.Values) { + foreach (MethodParameter mparam in formalMap.Values) { if (!(mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut)) vars.Add(mparam.outParameterCopy); } @@ -315,6 +344,7 @@ namespace BytecodeTranslator { impl.Proc = proc; + #region Translate method attributes // Don't need an expression translator because there is a limited set of things // that can appear as arguments to custom attributes foreach (var a in method.Attributes) { @@ -332,7 +362,9 @@ namespace BytecodeTranslator { o = (bool)mdc.Value ? Bpl.Expr.True : Bpl.Expr.False; break; case PrimitiveTypeCode.Int32: - o = Bpl.Expr.Literal((int)mdc.Value); + var lit = Bpl.Expr.Literal((int)mdc.Value); + lit.Type = Bpl.Type.Int; + o = lit; break; case PrimitiveTypeCode.String: o = mdc.Value; @@ -345,6 +377,7 @@ namespace BytecodeTranslator { } impl.AddAttribute(attrName, args); } + #endregion this.sink.TranslatedProgram.TopLevelDeclarations.Add(impl); @@ -363,5 +396,26 @@ namespace BytecodeTranslator { #endregion + private class FindCtorCall : BaseCodeTraverser { + private bool isDeferringCtor = false; + public ITypeReference containingType; + public static bool IsDeferringCtor(IMethodDefinition method, IBlockStatement body) { + var fcc = new FindCtorCall(method.ContainingType); + fcc.Visit(body); + return fcc.isDeferringCtor; + } + private FindCtorCall(ITypeReference containingType) { + this.containingType = containingType; + } + public override void Visit(IMethodCall methodCall) { + var md = methodCall.MethodToCall.ResolvedMethod; + if (md != null && md.IsConstructor && methodCall.ThisArgument is IThisReference) { + this.isDeferringCtor = TypeHelper.TypesAreEquivalent(md.ContainingType, containingType); + this.stopTraversal = true; + return; + } + base.Visit(methodCall); + } + } } } \ No newline at end of file diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index f95675f7..c6fca998 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -130,10 +130,12 @@ namespace BytecodeTranslator { /// public Bpl.Variable FindParameterVariable(IParameterDefinition param) { MethodParameter mp; - this.FormalMap.TryGetValue(param, out mp); + Tuple> procAndFormalMap; + this.declaredMethods.TryGetValue(param.ContainingSignature, out procAndFormalMap); + var formalMap = procAndFormalMap.Item2; + formalMap.TryGetValue(param, out mp); return mp.outParameterCopy; } - public Dictionary FormalMap = null; public Bpl.Variable FindOrCreateFieldVariable(IFieldReference field) { // The Heap has to decide how to represent the field (i.e., its type), @@ -172,11 +174,10 @@ namespace BytecodeTranslator { } private Dictionary declaredProperties = new Dictionary(); - public Bpl.Procedure FindOrCreateProcedure(IMethodReference method, bool isStatic) { - Bpl.Procedure proc; - var key = method.InternedKey; - if (!this.declaredMethods.TryGetValue(key, out proc)) { + Tuple> procAndFormalMap; + var key = method; //.InternedKey; + if (!this.declaredMethods.TryGetValue(key, out procAndFormalMap)) { #region Create in- and out-parameters int in_count = 0; @@ -191,7 +192,6 @@ namespace BytecodeTranslator { out_count++; formalMap.Add(formal, mp); } - this.FormalMap = formalMap; #region Look for Returnvalue @@ -300,7 +300,7 @@ namespace BytecodeTranslator { string MethodName = TranslationHelper.CreateUniqueMethodName(method); - proc = new Bpl.Procedure(method.Token(), + var proc = new Bpl.Procedure(method.Token(), MethodName, new Bpl.TypeVariableSeq(), new Bpl.VariableSeq(invars), // in @@ -311,11 +311,17 @@ namespace BytecodeTranslator { this.TranslatedProgram.TopLevelDeclarations.Add(proc); - this.declaredMethods.Add(key, proc); + procAndFormalMap = Tuple.Create(proc, formalMap); + this.declaredMethods.Add(key, procAndFormalMap); } - return proc; + return procAndFormalMap.Item1; + } + public Tuple> FindOrCreateProcedureAndReturnProcAndFormalMap(IMethodDefinition method, bool isStatic) { + this.FindOrCreateProcedure(method, isStatic); + return this.declaredMethods[method]; } + /// /// Creates a fresh variable that represents the type of /// in the Bpl program. I.e., its @@ -339,13 +345,14 @@ namespace BytecodeTranslator { private Dictionary declaredTypes = new Dictionary(); /// - /// The keys to the table are the interned key of the field. + /// The keys to the table are the signatures of the methods. + /// The values are pairs: first element is the procedure, + /// second element is the formal map for the procedure /// - private Dictionary declaredMethods = new Dictionary(); + private Dictionary>> declaredMethods = new Dictionary>>(); public void BeginMethod() { this.localVarMap = new Dictionary(); - this.FormalMap = new Dictionary(); } public Dictionary> delegateTypeToDelegates = new Dictionary>(); diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs index 9b13508f..f2918aa7 100644 --- a/BCT/RegressionTests/RegressionTestInput/Class1.cs +++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs @@ -122,4 +122,12 @@ namespace RegressionTestInput { } } } + + public class WriteToTheHeapAValueReadFromTheHeap { + int x; + int y; + public void M() { + this.y = this.x; + } + } } diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index a77683fe..00b54a84 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -222,14 +222,57 @@ var $Method: [int][int]int; var $Receiver: [int][int]int; +const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap: Type; + +const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: Field; + +const unique RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: Field; + +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int); + + + +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int) +{ + assert {:sourceFile "Class1.cs"} {:sourceLine 130} true; + $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(Box2Int(Read($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x)))); + assert {:sourceFile "Class1.cs"} {:sourceLine 131} true; + return; +} + + + +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int); + + + +procedure System.Object.#ctor(this: int); + + + +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int) +{ + $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x, Int2Box(0)); + $Heap := Write($Heap, this, RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y, Int2Box(0)); + call System.Object.#ctor(this); + return; +} + + + 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; } @@ -271,7 +314,10 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: var z: bool; z := z$in; + $Heap := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.staticB, Bool2Box(false)); + $Heap := Write($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 := Write($Heap, this, RegressionTestInput.ClassWithBoolTypes.b, Bool2Box(z)); assert {:sourceFile "Class1.cs"} {:sourceLine 74} true; @@ -406,7 +452,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t var xs: int; xs := xs$in; - if (!(!(xs != 0) || $ArrayLength[xs] <= 0)) + if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true)) { assert {:sourceFile "Class1.cs"} {:sourceLine 121} true; $ArrayContents := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a)) := $ArrayContents[Box2Int(Read($Heap, this, RegressionTestInput.ClassWithArrayTypes.a))][0 := $ArrayContents[xs][0]]]; @@ -427,6 +473,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int) { + $Heap := Write($Heap, this, RegressionTestInput.ClassWithArrayTypes.s, Int2Box(0)); + $Heap := Write($Heap, this, RegressionTestInput.ClassWithArrayTypes.a, Int2Box(0)); + call System.Object.#ctor(this); return; } @@ -464,21 +513,16 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) var x: int; var __temp_1: int; var $tmp5: int; - var __temp_2: int; - var __temp_3: int; var local_0: int; x := x$in; $tmp5 := x; assert $tmp5 != 0; __temp_1 := 5 / $tmp5; - __temp_2 := 3; - assert {:sourceFile "Class1.cs"} {:sourceLine 21} true; - __temp_3 := __temp_2; - x := __temp_3; - local_0 := __temp_1 + __temp_2; + x := 3; + local_0 := __temp_1 + 3; assert {:sourceFile "Class1.cs"} {:sourceLine 22} true; - assert x == 3 && local_0 <= 8; + 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; @@ -665,6 +709,8 @@ procedure RegressionTestInput.Class0.#ctor(this: int); implementation RegressionTestInput.Class0.#ctor(this: int) { + $Heap := Write($Heap, this, RegressionTestInput.Class0.StaticInt, Int2Box(0)); + call System.Object.#ctor(this); return; } diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index d0b573a6..f634d13a 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -194,12 +194,53 @@ var $Method: [int][int]int; var $Receiver: [int][int]int; +var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x: [int]int; + +var RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y: [int]int; + +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int); + + + +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.M(this: int) +{ + assert {:sourceFile "Class1.cs"} {:sourceLine 130} true; + RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this]; + assert {:sourceFile "Class1.cs"} {:sourceLine 131} true; + return; +} + + + +procedure RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int); + + + +procedure System.Object.#ctor(this: int); + + + +implementation RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.#ctor(this: int) +{ + RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.x[this] := 0; + RegressionTestInput.WriteToTheHeapAValueReadFromTheHeap.y[this] := 0; + call System.Object.#ctor(this); + return; +} + + + procedure RegressionTestInput.AsyncAttribute.#ctor(this: int); +procedure System.Attribute.#ctor(this: int); + + + implementation RegressionTestInput.AsyncAttribute.#ctor(this: int) { + call System.Attribute.#ctor(this); return; } @@ -239,7 +280,10 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: var z: bool; z := z$in; + RegressionTestInput.ClassWithBoolTypes.staticB[this] := false; + RegressionTestInput.ClassWithBoolTypes.b[this] := false; assert {:sourceFile "Class1.cs"} {:sourceLine 72} true; + call System.Object.#ctor(this); assert {:sourceFile "Class1.cs"} {:sourceLine 73} true; RegressionTestInput.ClassWithBoolTypes.b[this] := z; assert {:sourceFile "Class1.cs"} {:sourceLine 74} true; @@ -372,7 +416,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t var xs: int; xs := xs$in; - if (!(!(xs != 0) || $ArrayLength[xs] <= 0)) + if (!(if xs != 0 then $ArrayLength[xs] <= 0 else true)) { assert {:sourceFile "Class1.cs"} {:sourceLine 121} true; $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this] := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][0 := $ArrayContents[xs][0]]]; @@ -393,6 +437,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int) { + RegressionTestInput.ClassWithArrayTypes.s[this] := 0; + RegressionTestInput.ClassWithArrayTypes.a[this] := 0; + call System.Object.#ctor(this); return; } @@ -428,21 +475,16 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) var x: int; var __temp_1: int; var $tmp5: int; - var __temp_2: int; - var __temp_3: int; var local_0: int; x := x$in; $tmp5 := x; assert $tmp5 != 0; __temp_1 := 5 / $tmp5; - __temp_2 := 3; - assert {:sourceFile "Class1.cs"} {:sourceLine 21} true; - __temp_3 := __temp_2; - x := __temp_3; - local_0 := __temp_1 + __temp_2; + x := 3; + local_0 := __temp_1 + 3; assert {:sourceFile "Class1.cs"} {:sourceLine 22} true; - assert x == 3 && local_0 <= 8; + 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; @@ -629,6 +671,8 @@ procedure RegressionTestInput.Class0.#ctor(this: int); implementation RegressionTestInput.Class0.#ctor(this: int) { + RegressionTestInput.Class0.StaticInt[this] := 0; + call System.Object.#ctor(this); return; } diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt index 918bf1f7..35328269 100644 --- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt @@ -204,12 +204,53 @@ var $Method: [int][int]int; var $Receiver: [int][int]int; +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); + + + +procedure System.Object.#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.AsyncAttribute.#ctor(this: int); +procedure System.Attribute.#ctor(this: int); + + + implementation RegressionTestInput.AsyncAttribute.#ctor(this: int) { + call System.Attribute.#ctor(this); return; } @@ -249,7 +290,10 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: var z: bool; z := z$in; + $Heap[this, RegressionTestInput.ClassWithBoolTypes.staticB] := Bool2Box(false); + $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; @@ -382,7 +426,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t var xs: int; xs := xs$in; - if (!(!(xs != 0) || $ArrayLength[xs] <= 0)) + 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]]]; @@ -403,6 +447,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int) { + $Heap[this, RegressionTestInput.ClassWithArrayTypes.s] := Int2Box(0); + $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := Int2Box(0); + call System.Object.#ctor(this); return; } @@ -438,21 +485,16 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) var x: int; var __temp_1: int; var $tmp5: int; - var __temp_2: int; - var __temp_3: int; var local_0: int; x := x$in; $tmp5 := x; assert $tmp5 != 0; __temp_1 := 5 / $tmp5; - __temp_2 := 3; - assert {:sourceFile "Class1.cs"} {:sourceLine 21} true; - __temp_3 := __temp_2; - x := __temp_3; - local_0 := __temp_1 + __temp_2; + x := 3; + local_0 := __temp_1 + 3; assert {:sourceFile "Class1.cs"} {:sourceLine 22} true; - assert x == 3 && local_0 <= 8; + 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; @@ -639,6 +681,8 @@ procedure RegressionTestInput.Class0.#ctor(this: int); implementation RegressionTestInput.Class0.#ctor(this: int) { + $Heap[this, RegressionTestInput.Class0.StaticInt] := Int2Box(0); + call System.Object.#ctor(this); return; } diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt index 1b0f35b8..e48e4bd1 100644 --- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt @@ -194,12 +194,53 @@ var $Method: [int][int]int; var $Receiver: [int][int]int; +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); + + + +procedure System.Object.#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.AsyncAttribute.#ctor(this: int); +procedure System.Attribute.#ctor(this: int); + + + implementation RegressionTestInput.AsyncAttribute.#ctor(this: int) { + call System.Attribute.#ctor(this); return; } @@ -239,7 +280,10 @@ implementation RegressionTestInput.ClassWithBoolTypes.#ctor$System.Boolean(this: var z: bool; z := z$in; + $Heap[this, RegressionTestInput.ClassWithBoolTypes.staticB] := false; + $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; @@ -372,7 +416,7 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main4$System.Int32array(t var xs: int; xs := xs$in; - if (!(!(xs != 0) || $ArrayLength[xs] <= 0)) + 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]]]; @@ -393,6 +437,9 @@ procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); implementation RegressionTestInput.ClassWithArrayTypes.#ctor(this: int) { + $Heap[this, RegressionTestInput.ClassWithArrayTypes.s] := 0; + $Heap[this, RegressionTestInput.ClassWithArrayTypes.a] := 0; + call System.Object.#ctor(this); return; } @@ -428,21 +475,16 @@ implementation RegressionTestInput.Class0.M$System.Int32(this: int, x$in: int) var x: int; var __temp_1: int; var $tmp5: int; - var __temp_2: int; - var __temp_3: int; var local_0: int; x := x$in; $tmp5 := x; assert $tmp5 != 0; __temp_1 := 5 / $tmp5; - __temp_2 := 3; - assert {:sourceFile "Class1.cs"} {:sourceLine 21} true; - __temp_3 := __temp_2; - x := __temp_3; - local_0 := __temp_1 + __temp_2; + x := 3; + local_0 := __temp_1 + 3; assert {:sourceFile "Class1.cs"} {:sourceLine 22} true; - assert x == 3 && local_0 <= 8; + 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; @@ -629,6 +671,8 @@ procedure RegressionTestInput.Class0.#ctor(this: int); implementation RegressionTestInput.Class0.#ctor(this: int) { + $Heap[this, RegressionTestInput.Class0.StaticInt] := 0; + call System.Object.#ctor(this); return; } -- cgit v1.2.3