Convert (a subset of) Scala into C99

[mantognini]

List of tasks

:red_circle: indicate limitations in Leon itself.

• [x] Enforce subexpressions execution order: Java vs C
  • [x] Create a value for any function argument / binary operand
  • [x] Except for literals
  • [x] Or variable access
  • [x] But don't break while loops
  • [x] Nor short-circuit
  • [x] Optimize things wherever possible
• [ ] Support for C code injection directly from Scala code
• [ ] Support for function
  • [x] Function invocation
  • [x] Nested functions
  • [x] Recursive functions
  • [ ] Support for methods :question:
• [ ] Support for simple primitive types
  • [x] 32-bit Integer
  • [ ] Other size of integer :question:
  • [x] Boolean
  • [ ] Double :question:
• [ ] Support for non-recusrive algebraic data type
  • [x] Basic case class
  • [x] Access fields
  • [ ] Case class with methods
  • [ ] Regular class
• [x] Support for tuples
  • [x] N-sized tuple
  • [x] Primitive fields
  • [x] Tuples of tuples
  • [x] Array fields
• [ ] Support for array
  • See #2
• [x] Support for values
• [x] Support for variables
• [x] Support for while loops
• [ ] Support for if - else statements
  • [x] Basic support
  • [x] Extended support for foo(if (c) v1 else v2)
  • [ ] Extended support for flatten if - else if - else
• [ ] Support for assertions :question: (disabled for now)
• [ ] Add constraint on main's signature
• [ ] Testcases
  • [ ] Linear algebra operations (e.g. matrix multiplication)
  • [ ] Image processing (e.g. edge detection)
• [x] Add unit/integration/regression tests
• [ ] Explore stacksize with rlimit
• [ ] Improve reporting of unsupported feature by pointing to the specific element position that failed to be accepted.

[mantognini]

Example of nested functions and recursion

:red_circle: Modifying variable from within nested functions is not supported.

import leon.lang._

object RecursionAndNestedFunctions {

  // Complex way to return i
  def zzz(i: Int): Int = {
    val x = 0
    def rec(j: Int): Int = {
      if (i - x == j)     i
      else if (j > i) rec(j - 1)
      else            rec(j + 1)
    }

    rec(4)
  }

  // Complex way to compute 100 + 2 * i
  def foo(i: Int) = {
    var j = i
    def bar(x: Int) = {
      //j = j - 1 <- not supported by leon
      val y = x + i
      def baz(z: Int) = z + y + i
      //j = j + 1 <- not supported by leon
      baz(42)
    }
    bar(58) + j - i
  }

  def main() = foo(2) - zzz(104)

}

[mantognini]

Example of functional binary search on arrays

(based on leon/testcases/verification/xlang)

import leon.lang._

object BinarySearchFun {

  def binarySearch(a: Array[Int], key: Int, low: Int, high: Int): Int = ({
    require(a.length > 0 && sorted(a, low, high) &&
        0 <= low && low <= high + 1 && high < a.length
    )

    if(low <= high) {
      val i = (high + low) / 2
      val v = a(i)

      if(v == key) i
      else if (v > key) binarySearch(a, key, low, i - 1)
      else binarySearch(a, key, i + 1, high)
    } else -1
  }) ensuring(res =>
      res >= -1 &&
      res < a.length &&
      (if (res >= 0)
          a(res) == key else
          (high < 0 || (!occurs(a, low, (high+low)/2, key) && !occurs(a, (high+low)/2, high, key)))
      )
    )

  def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
    require(a.length >= 0 && to <= a.length && from >= 0)
    def rec(i: Int): Boolean = {
      require(i >= 0)
      if(i >= to)
        false
      else {
       if(a(i) == key) true else rec(i+1)
      }
    }
    if(from >= to)
      false
    else
      rec(from)
  }

  def sorted(a: Array[Int], l: Int, u: Int) : Boolean = {
    require(a.length >= 0 && l >= 0 && l <= u + 1 && u < a.length)
    val t = sortedWhile(true, l, l, u, a)
    t._1
  }

  def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Array[Int]): (Boolean, Int) = {
    require(a.length >= 0 && l >= 0 && l <= u+1 && u < a.length && k >= l && k <= u + 1)
    if(k < u) {
      sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a)
    } else (isSorted, k)
  }

  def main = {
    val a = Array(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)
    val i = binarySearch(a, 2, 0, a.length - 1) // should be 2
    val j = binarySearch(a, 11, 0, a.length - 1) // should be -1

    (i - 2) + (j + 1) // == 0
  }
}

[mantognini]

Example of procedural binary search on arrays

(based on leon/testcases/verification/xlang)

import leon.lang._

/* VSTTE 2008 - Dafny paper */

object BinarySearch {

  def binarySearch(a: Array[Int], key: Int): Int = ({
    require(a.length > 0 && sorted(a, 0, a.length - 1))
    var low = 0
    var high = a.length - 1
    var res = -1

    (while(low <= high && res == -1) {
      val i = (high + low) / 2
      val v = a(i)

      if(v == key)
        res = i

      if(v > key)
        high = i - 1
      else if(v < key)
        low = i + 1
    }) invariant(
        res >= -1 &&
        res < a.length &&
        0 <= low && 
        low <= high + 1 && 
        high >= -1 &&
        high < a.length && 
        (if (res >= 0) 
            a(res) == key else 
            (!occurs(a, 0, low, key) && !occurs(a, high + 1, a.length, key))
        )
       )
    res
  }) ensuring(res => 
      res >= -1 && 
      res < a.length && 
      (if(res >= 0) a(res) == key else !occurs(a, 0, a.length, key)))

  def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
    require(a.length >= 0 && to <= a.length && from >= 0)
    def rec(i: Int): Boolean = {
      require(i >= 0)
      if(i >= to) 
        false 
      else {
       if(a(i) == key) true else rec(i+1)
      }
    }
    if(from >= to)
      false
    else
      rec(from)
  }

  def sorted(a: Array[Int], l: Int, u: Int) : Boolean = {
    require(a.length >= 0 && l >= 0 && l <= u && u < a.length)
    val t = sortedWhile(true, l, l, u, a)
    t._1
  }

  def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Array[Int]): (Boolean, Int) = {
    require(a.length >= 0 && l >= 0 && l <= u && u < a.length && k >= l && k <= u)
    if(k < u) {
      sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a)
    } else (isSorted, k)
  }

  def main = {
    val a = Array(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)
    val i = binarySearch(a, 2)
    i - 2 // i should be 2
  }

}

[mantognini]

Example using arrays, tuple, recursion, while loops, variables, if-else, ...

(based on leon/testcases/verification/xlang)

import leon.lang._

/* VSTTE 2010 challenge 1 */

object MaxSum {

  def maxSum(a: Array[Int]): (Int, Int) = ({
    require(a.length >= 0 && isPositive(a))
    var sum = 0
    var max = 0
    var i = 0
    (while(i < a.length) {
      if(max < a(i))
        max = a(i)
      sum = sum + a(i)
      i = i + 1
    }) invariant (sum <= i * max && i >= 0 && i <= a.length)
    (sum, max)
  }) ensuring(res => res._1 <= a.length * res._2)

  def isPositive(a: Array[Int]): Boolean = {
    require(a.length >= 0)
    def rec(i: Int): Boolean = {
      require(i >= 0)
      if(i >= a.length)
        true
      else {
        if(a(i) < 0)
          false
        else
          rec(i+1)
      }
    }
    rec(0)
  }

  def summ(to : Int): Int = ({
    require(to >= 0)
    var i = 0
    var s = 0
    (while (i < to) {
      s = s + i
      i = i + 1
    }) invariant (s >= 0 && i >= 0 && s == i*(i-1)/2 && i <= to)
    s
  }) ensuring(res => res >= 0 && res == to*(to-1)/2)

  def sumsq(to : Int): Int = ({
    require(to >= 0)
    var i = 0
    var s = 0
    (while (i < to) {
      s = s + i*i
      i = i + 1
    }) invariant (s >= 0 && i >= 0 && s == (i-1)*i*(2*i-1)/6 && i <= to)
    s
  }) ensuring(res => res >= 0 && res == (to-1)*to*(2*to-1)/6)

  def main = {
    val a = Array(1, 4, 6, 0, 234, 999)
    val sm = maxSum(a)
    val sum = sm._1
    val max = sm._2
    if (sum == 1244 && max == 999) 0
    else -1
  }

}

[mantognini]

Example of array & tuple

import leon.lang._

object TupleArray {
  def exists(av: (Array[Int], Int)): Boolean = {
    var i = 0;
    var found = false;
    while (!found && i < av._1.length) {
      found = av._1(i) == av._2
      i = i + 1
    }
    found
  }

  def main = {
    val a = Array(0, 1, 5, -5, 9)
    val e1 = exists((a, 0))
    val e2 = exists((a, -1))
    if (e1 && !e2) 0
    else -1
  }
}

[mantognini]

Example of array

import leon.lang._

object ArrayAbs {
  def bar(i: Int) = i * 2

  def foo(i: Int, s: Int) {
    val a = Array.fill(if (s <= 0) 1 else s)(bar(i))
  }

  def dummy = {
    val a = Array.fill(4)(2)

    val b = Array(1, 2, 0)

    b(1) = if (bar(b(1)) % 2 == 0) 42 else 58
    b(if (b(0) < b(1)) bar(0) else 1) = 100

    //val c = Array(true, 2) <- not supported by leon but should NOT be accepted anyway

    a(0) = b(2)
    a(0)
  }

  def abs(a: Array[Int]) {
    var i = 0;
    while (i < a.length) {
      a(i) = if (a(i) < 0) -a(i) else a(i)
      i = i + 1
    }
  }

  def main = {
    val a = Array(0, 1, -2, -3, 4, -5)

    abs(a)

    a(3) - 3 // == 0
  }

}

[mantognini]

Example of sub-expression execution order Scala/C normalisation

import leon.lang._

object ExpressionOrder {
  case class Pixel(rgb: Int)
  case class Matrix(data: Array[Int], w: Int, h: Int)

  def fun = 0xffffff
  def foo = 4
  def bar(i: Int) = i * 2
  def baz(i: Int, j: Int) = bar(i) - bar(j)

  def syntaxCheck {
    val p = Pixel(fun)
    val m = Matrix(Array(0, 1, 2, 3), 2, 2)

    val z = baz(foo, bar(foo))
    val a = Array(0, 1, foo / 2, 3, bar(2), z / 1)

    val t = (true, foo, bar(a(0)))
  }

  def main =
      bool2int(test0(false), 1) +
      bool2int(test1(42),    2) +
      bool2int(test2(58),    4) +
      bool2int(test3(false), 8) +
      bool2int(test4(false), 16) +
      bool2int(test6,        32)

  def test0(b: Boolean) = {
    val f = b && !b // == false

    var c = 0

    val x = f && { c = 1; true }

    c == 0
  }

  def test1(i: Int) = {
    require(i > 0)

    val j = i / i * 3 // == 3

    var c = 0
    val x = { c = c + 3; j } + { c = c + 1; j } * { c = c * 2; j }

    c == 8 && j == 3 && x == 12
  }

  def test2(i: Int) = {
    var c = 0;
    val x = if (i < 0) { c = 1; -i } else { c = 2; i }

    if (i < 0) c == 1
    else c == 2
  }

  def test3(b: Boolean) = {
    val f = b && !b // == false

    var c = 0
    val x = f || { c = 1; true } || { c = 2; false }

    c == 1
  }

  def test4(b: Boolean) = {
    var i = 10
    var c = 0

    val f = b && !b // == false
    val t = b || !b // == true

    // The following condition is executed 11 times,
    // and only during the last execution is the last
    // operand evaluated
    while ({ c = c + 1; t } && i > 0 || { c = c * 2; f }) {
      i = i - 1
    }

    i == 0 && c == 22
  }

  def test5(b: Boolean) = {
    val f = b && !b // == false

    var c = if (f) 0 else -1

    c = c + (if (f) 0 else 1)

    c == 0
  }

  def test6 = {
    val a = Array(0, 1, 2, 3, 4)
    def rec(b: Boolean, i: Int): Boolean = {
      if (a.length <= i + 1) b
      else rec(if (a(i) < a(i + 1)) b else false, i + 1)
    }

    rec(true, 0)
  }

  def bool2int(b: Boolean, f: Int) = if (b) 0 else f;
}