From ed2c309c94329dabf3f384e445748393af50af12 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Wed, 23 Dec 2015 21:13:16 +0100
Subject: [PATCH] Update GenC regression tests
Tests that couldn't be verified are now in a "unverified" folder: they are not verified with the GenC regression test but they are still converted to C and their execution should yield 0.
At the moment, in ExpressionOrder, test7 fails to verify. However, it should pass because my Scala interpreter successfully return true.
---
.../{valid => unverified}/BinarySearch.scala | 3 +-
.../BinarySearchFun.scala | 24 +++++++++-------
.../genc/{valid => unverified}/MaxSum.scala | 2 +-
.../regression/genc/valid/AbsArray.scala | 22 ++++++++-------
.../regression/genc/valid/CaseClass.scala | 3 +-
.../genc/valid/ExpressionOrder.scala | 28 +++++++++++--------
.../valid/RecursionAndNestedFunctions.scala | 13 +++++----
.../regression/genc/valid/TupleArray.scala | 13 +++++----
src/test/scala/leon/genc/GenCSuite.scala | 12 ++++++--
9 files changed, 72 insertions(+), 48 deletions(-)
rename src/test/resources/regression/genc/{valid => unverified}/BinarySearch.scala (96%)
rename src/test/resources/regression/genc/{valid => unverified}/BinarySearchFun.scala (77%)
rename src/test/resources/regression/genc/{valid => unverified}/MaxSum.scala (98%)
diff --git a/src/test/resources/regression/genc/valid/BinarySearch.scala b/src/test/resources/regression/genc/unverified/BinarySearch.scala
similarity index 96%
rename from src/test/resources/regression/genc/valid/BinarySearch.scala
rename to src/test/resources/regression/genc/unverified/BinarySearch.scala
index 75e1219a0..aec7d2b5d 100644
--- a/src/test/resources/regression/genc/valid/BinarySearch.scala
+++ b/src/test/resources/regression/genc/unverified/BinarySearch.scala
@@ -11,7 +11,8 @@ object BinarySearch {
var res = -1
(while(low <= high && res == -1) {
- val i = (high + low) / 2
+ //val i = (high + low) / 2
+ val i = low + ((high - low) / 2)
val v = a(i)
if(v == key)
diff --git a/src/test/resources/regression/genc/valid/BinarySearchFun.scala b/src/test/resources/regression/genc/unverified/BinarySearchFun.scala
similarity index 77%
rename from src/test/resources/regression/genc/valid/BinarySearchFun.scala
rename to src/test/resources/regression/genc/unverified/BinarySearchFun.scala
index feb7c8cc6..ebc97f6c6 100644
--- a/src/test/resources/regression/genc/valid/BinarySearchFun.scala
+++ b/src/test/resources/regression/genc/unverified/BinarySearchFun.scala
@@ -7,20 +7,24 @@ object BinarySearchFun {
0 <= low && low <= high + 1 && high < a.length
)
- if(low <= high) {
- val i = (high + low) / 2
+ if (low <= high) {
+ //val i = (high + low) / 2
+ val i = low + (high - low) / 2
+
val v = a(i)
- if(v == key) 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)))
+ res < a.length && (
+ if (res >= 0)
+ a(res) == key
+ else
+ (high < 0 || (!occurs(a, low, low + (high - low) / 2, key) &&
+ !occurs(a, low + (high - low) / 2, high, key)))
)
)
@@ -29,13 +33,13 @@ object BinarySearchFun {
require(a.length >= 0 && to <= a.length && from >= 0)
def rec(i: Int): Boolean = {
require(i >= 0)
- if(i >= to)
+ if (i >= to)
false
else {
- if(a(i) == key) true else rec(i+1)
+ if (a(i) == key) true else rec(i+1)
}
}
- if(from >= to)
+ if (from >= to)
false
else
rec(from)
diff --git a/src/test/resources/regression/genc/valid/MaxSum.scala b/src/test/resources/regression/genc/unverified/MaxSum.scala
similarity index 98%
rename from src/test/resources/regression/genc/valid/MaxSum.scala
rename to src/test/resources/regression/genc/unverified/MaxSum.scala
index 1c6fc2432..033dfed30 100644
--- a/src/test/resources/regression/genc/valid/MaxSum.scala
+++ b/src/test/resources/regression/genc/unverified/MaxSum.scala
@@ -65,7 +65,7 @@ object MaxSum {
val max = sm._2
if (sum == 1244 && max == 999) 0
else -1
- }
+ } ensuring { _ == 0 }
}
diff --git a/src/test/resources/regression/genc/valid/AbsArray.scala b/src/test/resources/regression/genc/valid/AbsArray.scala
index b3a592f1a..581684e7c 100644
--- a/src/test/resources/regression/genc/valid/AbsArray.scala
+++ b/src/test/resources/regression/genc/valid/AbsArray.scala
@@ -1,21 +1,23 @@
import leon.lang._
object AbsArray {
- 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)
- abs(a)
+ def abs() {
+ require(a.length < 10000)
+
+ var i = 0;
+ (while (i < a.length && i < 10000) {
+ a(i) = if (a(i) < 0) -a(i) else a(i)
+ i = i + 1
+ }) invariant (i >= 0 && i <= 10000)
+ }
+
+ abs()
a(0) + a(1) - 1 + a(2) - 2 + a(3) - 3 // == 0
- }
+ } ensuring { _ == 0 }
}
diff --git a/src/test/resources/regression/genc/valid/CaseClass.scala b/src/test/resources/regression/genc/valid/CaseClass.scala
index bf104e378..83f598859 100644
--- a/src/test/resources/regression/genc/valid/CaseClass.scala
+++ b/src/test/resources/regression/genc/valid/CaseClass.scala
@@ -14,6 +14,7 @@ object CaseClass {
val d = cyan
val z = sub(c, d).g
z
- }
+ } ensuring { _ == 0 }
}
+
diff --git a/src/test/resources/regression/genc/valid/ExpressionOrder.scala b/src/test/resources/regression/genc/valid/ExpressionOrder.scala
index 5507d8e19..d6620ab35 100644
--- a/src/test/resources/regression/genc/valid/ExpressionOrder.scala
+++ b/src/test/resources/regression/genc/valid/ExpressionOrder.scala
@@ -34,7 +34,7 @@ object ExpressionOrder {
def f4 = (if (i < 0) d else c)._2 // expression result unused
}
- def main =
+ def main = {
bool2int(test0(false), 1) +
bool2int(test1(42), 2) +
bool2int(test2(58), 4) +
@@ -43,6 +43,7 @@ object ExpressionOrder {
bool2int(test6, 32) +
bool2int(test7, 64) +
bool2int(test8, 128)
+ } ensuring { _ == 0 }
def test0(b: Boolean) = {
val f = b && !b // == false
@@ -52,7 +53,7 @@ object ExpressionOrder {
val x = f && { c = 1; true }
c == 0
- }
+ }.holds
def test1(i: Int) = {
require(i > 0)
@@ -63,7 +64,7 @@ object ExpressionOrder {
val x = { c = c + 3; j } + { c = c + 1; j } * { c = c * 2; j }
c == 8 && j == 3 && x == 12
- }
+ }.holds
def test2(i: Int) = {
var c = 0;
@@ -71,7 +72,7 @@ object ExpressionOrder {
if (i < 0) c == 1
else c == 2
- }
+ }.holds
def test3(b: Boolean) = {
val f = b && !b // == false
@@ -80,7 +81,7 @@ object ExpressionOrder {
val x = f || { c = 1; true } || { c = 2; false }
c == 1
- }
+ }.holds
def test4(b: Boolean) = {
var i = 10
@@ -97,7 +98,7 @@ object ExpressionOrder {
}
i == 0 && c == 22
- }
+ }.holds
def test5(b: Boolean) = {
val f = b && !b // == false
@@ -107,17 +108,20 @@ object ExpressionOrder {
c = c + (if (f) 0 else 1)
c == 0
- }
+ }.holds
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)
+ require(i >= 0 && i < 2147483647) // 2^31 - 1
+
+ if (i + 1 < a.length) rec(if (a(i) < a(i + 1)) b else false, i + 1)
+ else b
}
rec(true, 0)
- }
+ }.holds
def test7 = {
var c = 1
@@ -127,7 +131,7 @@ object ExpressionOrder {
a(if(a(0) == 0) { c = c + 1; 0 } else { c = c + 2; 1 }) = { c = c * 2; -1 }
c == 4
- }
+ }.holds
def test8 = {
var x = 0
@@ -139,7 +143,7 @@ object ExpressionOrder {
}
bar(2) == 0
- }
+ }.holds
def bool2int(b: Boolean, f: Int) = if (b) 0 else f;
}
diff --git a/src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala b/src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala
index 70f5c150a..25f69538a 100644
--- a/src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala
+++ b/src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala
@@ -5,14 +5,15 @@ 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
+ if (i - x == j) i
else if (j > i) rec(j - 1)
else rec(j + 1)
- }
+ } ensuring { _ == i }
rec(4)
- }
+ } ensuring { _ == i }
// Complex way to compute 100 + 2 * i
@@ -26,9 +27,11 @@ object RecursionAndNestedFunctions {
baz(42)
}
bar(58) + j - i
- }
+ } ensuring { _ == 100 + 2 * i }
- def main() = foo(2) - zzz(104)
+ def main() = {
+ foo(2) - zzz(104)
+ } ensuring { _ == 0 }
}
diff --git a/src/test/resources/regression/genc/valid/TupleArray.scala b/src/test/resources/regression/genc/valid/TupleArray.scala
index 576ac3d27..1f2354e06 100644
--- a/src/test/resources/regression/genc/valid/TupleArray.scala
+++ b/src/test/resources/regression/genc/valid/TupleArray.scala
@@ -2,12 +2,14 @@ import leon.lang._
object TupleArray {
def exists(av: (Array[Int], Int)): Boolean = {
- var i = 0;
- var found = false;
- while (!found && i < av._1.length) {
+ require(av._1.length < 10000)
+
+ var i = 0
+ var found = false
+ (while (!found && i < av._1.length) {
found = av._1(i) == av._2
i = i + 1
- }
+ }) invariant (i >= 0 && i < 10000)
found
}
@@ -17,6 +19,7 @@ object TupleArray {
val e2 = exists((a, -1))
if (e1 && !e2) 0
else -1
- }
+ } ensuring { _ == 0 }
}
+
diff --git a/src/test/scala/leon/genc/GenCSuite.scala b/src/test/scala/leon/genc/GenCSuite.scala
index a8e0368ee..4292f9583 100644
--- a/src/test/scala/leon/genc/GenCSuite.scala
+++ b/src/test/scala/leon/genc/GenCSuite.scala
@@ -163,7 +163,7 @@ class GenCSuite extends LeonRegressionSuite {
mkTest(files, cat)(block)
}
- protected def testValid(cc: String) = forEachFileIn("valid") { (xCtx, prog) =>
+ protected def testDirectory(cc: String, dir: String) = forEachFileIn(dir) { (xCtx, prog) =>
val converter = convert(xCtx) _
val saver = saveToFile(xCtx) _
val compiler = compile(xCtx, cc) _
@@ -174,6 +174,9 @@ class GenCSuite extends LeonRegressionSuite {
pipeline(prog)
}
+ protected def testValid(cc: String) = testDirectory(cc, "valid")
+ protected def testUnverified(cc: String) = testDirectory(cc, "unverified");
+
protected def testInvalid() = forEachFileIn("invalid") { (xCtx, prog) =>
intercept[LeonFatalError] {
GenerateCPhase(xCtx.leon, prog)
@@ -199,8 +202,11 @@ class GenCSuite extends LeonRegressionSuite {
protected def testAll() = {
// Set C compiler according to the platform we're currently running on
detectCompiler match {
- case Some(cc) => testValid(cc)
- case None => test("dectecting C compiler") { fail("no C compiler found") }
+ case Some(cc) =>
+ testValid(cc)
+ testUnverified(cc)
+ case None =>
+ test("dectecting C compiler") { fail("no C compiler found") }
}
testInvalid()
--
GitLab