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.

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);