From 97d2e06de95247f793f413d2f444ef57eb7886c8 Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Wed, 26 Jan 2011 18:09:43 +0000 Subject: Fix the generation of procedure names so that array types are encoded properly. Translate "default value" expressions. Fix translation of non-trivial conditional expressions and added two more optimizations for trivial ones (trivial ones are where either the true branch or the false branch are constants). Fix translation of array length expressions. Fix translation of logical negation expressions. --- BCT/BytecodeTranslator/ExpressionTraverser.cs | 53 ++++++++++++++++++++-- BCT/BytecodeTranslator/TranslationHelper.cs | 1 + BCT/RegressionTests/RegressionTestInput/Class1.cs | 6 +++ .../TranslationTest/GeneralHeapInput.txt | 24 ++++++++++ .../TranslationTest/SplitFieldsHeapInput.txt | 24 ++++++++++ .../TranslationTest/TwoDBoxHeapInput.txt | 24 ++++++++++ .../TranslationTest/TwoDIntHeapInput.txt | 24 ++++++++++ 7 files changed, 151 insertions(+), 5 deletions(-) (limited to 'BCT') diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index dd6cbb66..5198e908 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -381,6 +381,17 @@ namespace BytecodeTranslator } } + public override void Visit(IDefaultValue defaultValue) { + var bplType = TranslationHelper.CciTypeToBoogie(defaultValue.Type); + if (bplType == Bpl.Type.Int) { + TranslatedExpressions.Push(Bpl.Expr.Literal(0)); + } else if (bplType == Bpl.Type.Bool) { + TranslatedExpressions.Push(Bpl.Expr.False); + } else { + throw new NotImplementedException("Don't know how to translate type"); + } + } + #endregion #region Translate Method Calls @@ -738,8 +749,7 @@ namespace BytecodeTranslator if (ctc != null && ctc.Type == BCT.Host.PlatformType.SystemInt32) { int v = (int)ctc.Value; - if (v == 0) - { + if (v == 0) { // x ? y : 0 == x && y Visit(conditional.Condition); Bpl.Expr x = TranslatedExpressions.Pop(); Visit(conditional.ResultIfTrue); @@ -747,13 +757,21 @@ namespace BytecodeTranslator TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.And, x, y)); return; } + if (v == 1) { // x ? y : 1 == !x || y + Visit(conditional.Condition); + Bpl.Expr x = TranslatedExpressions.Pop(); + Visit(conditional.ResultIfTrue); + Bpl.Expr y = TranslatedExpressions.Pop(); + var notX = Bpl.Expr.Unary(conditional.Token(), Bpl.UnaryOperator.Opcode.Not, x); + TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, notX, y)); + return; + } } ctc = conditional.ResultIfTrue as CompileTimeConstant; if (ctc != null && ctc.Type == BCT.Host.PlatformType.SystemInt32) { int v = (int)ctc.Value; - if (v == 1) - { + if (v == 1) { // x ? 1 : y == x || y Visit(conditional.Condition); Bpl.Expr x = TranslatedExpressions.Pop(); Visit(conditional.ResultIfFalse); @@ -761,8 +779,25 @@ namespace BytecodeTranslator TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, x, y)); return; } + if (v == 0) { // x ? 0 : y == !x && y + Visit(conditional.Condition); + Bpl.Expr x = TranslatedExpressions.Pop(); + Visit(conditional.ResultIfFalse); + Bpl.Expr y = TranslatedExpressions.Pop(); + var notX = Bpl.Expr.Unary(conditional.Token(), Bpl.UnaryOperator.Opcode.Not, x); + TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.And, notX, y)); + return; + } } base.Visit(conditional); + var ifFalse = TranslatedExpressions.Pop(); + var ifTrue = TranslatedExpressions.Pop(); + var c = TranslatedExpressions.Pop(); + var tok = conditional.Token(); + TranslatedExpressions.Push( + new Bpl.NAryExpr(tok, new Bpl.IfThenElse(tok), new Bpl.ExprSeq(c, ifTrue, ifFalse)) + ); + } #endregion @@ -779,13 +814,21 @@ namespace BytecodeTranslator public override void Visit(ILogicalNot logicalNot) { - base.Visit(logicalNot); + base.Visit(logicalNot.Operand); Bpl.Expr exp = TranslatedExpressions.Pop(); TranslatedExpressions.Push(Bpl.Expr.Unary( logicalNot.Token(), Bpl.UnaryOperator.Opcode.Not, exp)); + } + public override void Visit(IVectorLength vectorLength) { + base.Visit(vectorLength.Vector); + var e = TranslatedExpressions.Pop(); + TranslatedExpressions.Push( + Bpl.Expr.Select(new Bpl.IdentifierExpr(vectorLength.Token(), this.sink.ArrayLengthVariable), new Bpl.Expr[] { e }) + ); } + #endregion #region CodeContract Expressions diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index 9f90f94d..707ab4e5 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -98,6 +98,7 @@ namespace BytecodeTranslator { s = s.Replace('(', '$'); s = s.Replace(',', '$'); s = s.TrimEnd(')'); + s = s.Replace("[]", "array"); return s; } diff --git a/BCT/RegressionTests/RegressionTestInput/Class1.cs b/BCT/RegressionTests/RegressionTestInput/Class1.cs index 38d696b7..9b13508f 100644 --- a/BCT/RegressionTests/RegressionTestInput/Class1.cs +++ b/BCT/RegressionTests/RegressionTestInput/Class1.cs @@ -115,5 +115,11 @@ namespace RegressionTestInput { a[x + 1] = 43; Contract.Assert(a[x + 1] == a[x] + 1); } + + public void Main4(int[] xs) { + if (xs != null && xs.Length > 0) { + a[0] = xs[0]; + } + } } } diff --git a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt index de33bdc0..6fc21050 100644 --- a/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/GeneralHeapInput.txt @@ -221,6 +221,30 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: +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 (!(!(xs != 0) || $ArrayLength[xs] <= 0)) + { + 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]]]; + } + else + { + } + + assert {:sourceFile "Class1.cs"} {:sourceLine 123} true; + return; +} + + + procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); diff --git a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt index bcbdb0d5..b8e98a5d 100644 --- a/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/SplitFieldsHeapInput.txt @@ -197,6 +197,30 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: +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 (!(!(xs != 0) || $ArrayLength[xs] <= 0)) + { + assert {:sourceFile "Class1.cs"} {:sourceLine 121} true; + $ArrayContents := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this] := $ArrayContents[RegressionTestInput.ClassWithArrayTypes.a[this]][0 := $ArrayContents[xs][0]]]; + } + else + { + } + + assert {:sourceFile "Class1.cs"} {:sourceLine 123} true; + return; +} + + + procedure RegressionTestInput.ClassWithArrayTypes.#ctor(this: int); diff --git a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt index 3137e894..1088f1f7 100644 --- a/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/TwoDBoxHeapInput.txt @@ -207,6 +207,30 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: +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 (!(!(xs != 0) || $ArrayLength[xs] <= 0)) + { + 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); diff --git a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt index 6d356d4b..1fa0bd18 100644 --- a/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt +++ b/BCT/RegressionTests/TranslationTest/TwoDIntHeapInput.txt @@ -197,6 +197,30 @@ implementation RegressionTestInput.ClassWithArrayTypes.Main3$System.Int32(this: +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 (!(!(xs != 0) || $ArrayLength[xs] <= 0)) + { + 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); -- cgit v1.2.3