diff options
Diffstat (limited to 'BCT')
7 files changed, 151 insertions, 5 deletions
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);
|