From c6dce4f2c4228a7c8cddba11fa1f991fc7da7089 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Thu, 12 Nov 2015 17:11:45 +0100
Subject: [PATCH] Add regression tests for C code generation
---
build.sbt | 12 +-
.../regression/genc/invalid/AbsFun.scala | 66 ++++++
.../genc/invalid/LinearSearch.scala | 40 ++++
.../regression/genc/valid/BinarySearch.scala | 81 ++++++++
.../genc/valid/BinarySearchFun.scala | 66 ++++++
.../genc/valid/ExpressionOrder.scala | 119 +++++++++++
.../regression/genc/valid/MaxSum.scala | 71 +++++++
.../valid/RecursionAndNestedFunctions.scala | 34 +++
.../regression/genc/valid/TupleArray.scala | 22 ++
src/test/scala/leon/genc/GenCSuite.scala | 194 ++++++++++++++++++
10 files changed, 704 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/regression/genc/invalid/AbsFun.scala
create mode 100644 src/test/resources/regression/genc/invalid/LinearSearch.scala
create mode 100644 src/test/resources/regression/genc/valid/BinarySearch.scala
create mode 100644 src/test/resources/regression/genc/valid/BinarySearchFun.scala
create mode 100644 src/test/resources/regression/genc/valid/ExpressionOrder.scala
create mode 100644 src/test/resources/regression/genc/valid/MaxSum.scala
create mode 100644 src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala
create mode 100644 src/test/resources/regression/genc/valid/TupleArray.scala
create mode 100644 src/test/scala/leon/genc/GenCSuite.scala
diff --git a/build.sbt b/build.sbt
index b825fa5ba..0e3e147a1 100644
--- a/build.sbt
+++ b/build.sbt
@@ -141,6 +141,14 @@ parallelExecution in IsabelleTest := false
fork in IsabelleTest := true
+// GenC Tests
+lazy val GenCTest = config("genc") extend(Test)
+
+testOptions in GenCTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "leon.genc."))
+
+parallelExecution in GenCTest := false
+
+
def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
@@ -148,9 +156,11 @@ lazy val bonsai = ghProject("git://github.com/colder/bonsai.git", "10ea
lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "372bb14d0c84953acc17f9a7e1592087adb0a3e1")
lazy val root = (project in file(".")).
- configs(RegressionTest, IsabelleTest, IntegrTest).
+ configs(RegressionTest, IsabelleTest, GenCTest, IntegrTest).
dependsOn(bonsai, scalaSmtLib).
settings(inConfig(RegressionTest)(Defaults.testTasks ++ testSettings): _*).
settings(inConfig(IntegrTest)(Defaults.testTasks ++ testSettings): _*).
settings(inConfig(IsabelleTest)(Defaults.testTasks ++ testSettings): _*).
+ settings(inConfig(GenCTest)(Defaults.testTasks ++ testSettings): _*).
settings(inConfig(Test)(Defaults.testTasks ++ testSettings): _*)
+
diff --git a/src/test/resources/regression/genc/invalid/AbsFun.scala b/src/test/resources/regression/genc/invalid/AbsFun.scala
new file mode 100644
index 000000000..aff9a2c80
--- /dev/null
+++ b/src/test/resources/regression/genc/invalid/AbsFun.scala
@@ -0,0 +1,66 @@
+import leon.lang._
+
+object AbsFun {
+
+
+ def isPositive(a : Array[Int], size : Int) : Boolean = {
+ require(a.length >= 0 && size <= a.length)
+ rec(0, a, size)
+ }
+
+ def rec(i: Int, a: Array[Int], size: Int) : Boolean = {
+ require(a.length >= 0 && size <= a.length && i >= 0)
+
+ if(i >= size) true
+ else {
+ if (a(i) < 0)
+ false
+ else
+ rec(i + 1, a, size)
+ }
+ }
+
+ // Returning Arrays is not supported by GenC
+ def abs(tab: Array[Int]): Array[Int] = {
+ require(tab.length >= 0)
+ val t = while0(Array.fill(tab.length)(0), 0, tab)
+ t._1
+ } ensuring(res => isPositive(res, res.length))
+
+
+ def while0(t: Array[Int], k: Int, tab: Array[Int]): (Array[Int], Int) = {
+ require(tab.length >= 0 &&
+ t.length == tab.length &&
+ k >= 0 &&
+ k <= tab.length &&
+ isPositive(t, k))
+
+ if(k < tab.length) {
+ val nt = if(tab(k) < 0) {
+ t.updated(k, -tab(k))
+ } else {
+ t.updated(k, tab(k))
+ }
+ while0(nt, k+1, tab)
+ } else {
+ (t, k)
+ }
+ } ensuring(res =>
+ res._2 >= tab.length &&
+ res._1.length == tab.length &&
+ res._2 >= 0 &&
+ res._2 <= tab.length &&
+ isPositive(res._1, res._2))
+
+ def property(t: Array[Int], k: Int): Boolean = {
+ require(isPositive(t, k) && t.length >= 0 && k >= 0)
+ if(k < t.length) {
+ val nt = if(t(k) < 0) {
+ t.updated(k, -t(k))
+ } else {
+ t.updated(k, t(k))
+ }
+ isPositive(nt, k+1)
+ } else true
+ } holds
+}
diff --git a/src/test/resources/regression/genc/invalid/LinearSearch.scala b/src/test/resources/regression/genc/invalid/LinearSearch.scala
new file mode 100644
index 000000000..88cadb0ef
--- /dev/null
+++ b/src/test/resources/regression/genc/invalid/LinearSearch.scala
@@ -0,0 +1,40 @@
+import leon.lang._
+
+/* The calculus of Computation textbook */
+
+object LinearSearch {
+
+ def linearSearch(a: Array[Int], c: Int): Boolean = ({
+ require(a.length >= 0)
+ var i = 0
+ var found = false
+ (while(i < a.length) {
+ if(a(i) == c)
+ found = true
+ i = i + 1
+ }) invariant(
+ i <= a.length &&
+ i >= 0 &&
+ (if(found) contains(a, i, c) else !contains(a, i, c))
+ )
+ found
+ }) ensuring(res => if(res) contains(a, a.length, c) else !contains(a, a.length, c))
+
+ def contains(a: Array[Int], size: Int, c: Int): Boolean = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
+ content(a, size).contains(c)
+ }
+
+ // Set not supported by GenC
+ def content(a: Array[Int], size: Int): Set[Int] = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
+ var set = Set.empty[Int]
+ var i = 0
+ (while(i < size) {
+ set = set ++ Set(a(i))
+ i = i + 1
+ }) invariant(i >= 0 && i <= size)
+ set
+ }
+
+}
diff --git a/src/test/resources/regression/genc/valid/BinarySearch.scala b/src/test/resources/regression/genc/valid/BinarySearch.scala
new file mode 100644
index 000000000..75e1219a0
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/BinarySearch.scala
@@ -0,0 +1,81 @@
+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
+ }
+
+}
+
diff --git a/src/test/resources/regression/genc/valid/BinarySearchFun.scala b/src/test/resources/regression/genc/valid/BinarySearchFun.scala
new file mode 100644
index 000000000..feb7c8cc6
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/BinarySearchFun.scala
@@ -0,0 +1,66 @@
+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
+ }
+}
+
diff --git a/src/test/resources/regression/genc/valid/ExpressionOrder.scala b/src/test/resources/regression/genc/valid/ExpressionOrder.scala
new file mode 100644
index 000000000..f86f3e8d2
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/ExpressionOrder.scala
@@ -0,0 +1,119 @@
+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) +
+ bool2int(test7, 64)
+
+ 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 test7 = {
+ var c = 1
+
+ val a = Array(0, 1, 2, 3, 4)
+
+ a(if(a(0) == 0) { c = c + 1; 0 } else { c = c + 2; 1 }) = { c = c * 2; -1 }
+
+ c == 4
+ }
+
+ def bool2int(b: Boolean, f: Int) = if (b) 0 else f;
+}
+
+
diff --git a/src/test/resources/regression/genc/valid/MaxSum.scala b/src/test/resources/regression/genc/valid/MaxSum.scala
new file mode 100644
index 000000000..1c6fc2432
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/MaxSum.scala
@@ -0,0 +1,71 @@
+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
+ }
+
+}
+
diff --git a/src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala b/src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala
new file mode 100644
index 000000000..70f5c150a
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/RecursionAndNestedFunctions.scala
@@ -0,0 +1,34 @@
+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)
+
+}
+
diff --git a/src/test/resources/regression/genc/valid/TupleArray.scala b/src/test/resources/regression/genc/valid/TupleArray.scala
new file mode 100644
index 000000000..576ac3d27
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/TupleArray.scala
@@ -0,0 +1,22 @@
+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
+ }
+
+}
diff --git a/src/test/scala/leon/genc/GenCSuite.scala b/src/test/scala/leon/genc/GenCSuite.scala
new file mode 100644
index 000000000..c452c948c
--- /dev/null
+++ b/src/test/scala/leon/genc/GenCSuite.scala
@@ -0,0 +1,194 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package genc
+
+import leon.test.LeonRegressionSuite
+
+import leon.frontends.scalac.ExtractionPhase
+import leon.purescala.Definitions.Program
+import leon.utils.{ PreprocessingPhase, UniqueCounter }
+
+import scala.concurrent._
+import ExecutionContext.Implicits.global
+import scala.sys.process._
+
+import org.scalatest.{ Args, Status }
+
+import java.nio.file.{ Files, Path }
+
+class GenCSuite extends LeonRegressionSuite {
+
+ private val testDir = "regression/genc/"
+ private lazy val tmpDir = Files.createTempDirectory("genc")
+ private val ccflags = "-std=c99 -g -O0"
+ private val maxExecutionTime = 2 // seconds
+
+ private val counter = new UniqueCounter[Unit]
+ counter.nextGlobal // Start with 1
+
+ private case class ExtendedContext(leon: LeonContext, tmpDir: Path, progName: String)
+
+ // Tests are run as follows:
+ // - The classic ExtractionPhase & PreprocessingPhase are run on all input files
+ // (this way the libraries are evaluated only once)
+ // - A Program is constructed for each input file
+ // - At this point no error should have occurred or something would be wrong
+ // with the extraction phases
+ // - For each Program P:
+ // + if P is expected to be convertible to C, then we make sure that:
+ // * the GenerateCPhase run without trouble,
+ // * the generated C code compiles using a C99 compiler without error,
+ // * and that, when run, the exit code is 0
+ // + if P is expected to be non-convertible to C, then we make sure that:
+ // * the GenerateCPhase fails
+ private def mkTest(files: List[String], cat: String)(block: (ExtendedContext, Program) => Unit) = {
+ val extraction =
+ ExtractionPhase andThen
+ new PreprocessingPhase(true, true)
+
+ val ctx = createLeonContext(files:_*)
+
+ try {
+ val (_, ast) = extraction.run(ctx, files)
+
+ val programs = {
+ val (user, lib) = ast.units partition { _.isMainUnit }
+ user map ( u => Program(u :: lib) )
+ }
+
+ for { prog <- programs } {
+ val name = prog.units.head.id.name
+ val ctx = createLeonContext(s"--o=$tmpDir/$name.c")
+ val xCtx = ExtendedContext(ctx, tmpDir, name)
+
+ val displayName = s"$cat/$name.scala"
+ val index = counter.nextGlobal
+
+ test(f"$index%3d: $displayName") {
+ block(xCtx, prog)
+ }
+ }
+ } catch {
+ case fe: LeonFatalError =>
+ test("Compilation") {
+ fail(ctx, "Unexpected fatal error while setting up tests", fe)
+ }
+ }
+ }
+
+ // Run a process with a timeout and return the status code
+ private def runProcess(pb: ProcessBuilder): Int = runProcess(pb.run)
+ private def runProcess(p: Process): Int = {
+ val f = Future(blocking(p.exitValue()))
+ try {
+ Await.result(f, duration.Duration(maxExecutionTime, "sec"))
+ } catch {
+ case _: TimeoutException =>
+ p.destroy()
+ p.exitValue()
+ }
+ }
+
+ // Determine which C compiler is available
+ private def detectCompiler: Option[String] = {
+ val testCode = "int main() { return 0; }"
+ val testBinary = s"$tmpDir/test"
+
+ // NOTE this code might print error on stderr when a non-existing compiler
+ // is used. It seems that even with a special ProcessLogger the RuntimeException
+ // is printed for some reason.
+
+ def testCompiler(cc: String): Boolean = try {
+ val process = s"echo $testCode" #| s"$cc $ccflags -o $testBinary -xc -" #&& s"$testBinary"
+ runProcess(process) == 0
+ } catch {
+ case _: java.lang.RuntimeException => false
+ }
+
+ val knownCompiler = "cc" :: "clang" :: "gcc" :: "mingw" :: Nil
+ // Note that VS is not in the list as we cannot specify C99 dialect
+
+ knownCompiler find testCompiler
+ }
+
+ private def convert(xCtx: ExtendedContext)(prog: Program) = {
+ try {
+ GenerateCPhase(xCtx.leon, prog)
+ } catch {
+ case fe: LeonFatalError =>
+ fail(xCtx.leon, "Convertion to C unexpectedly failed", fe)
+ }
+ }
+
+ private def saveToFile(xCtx: ExtendedContext)(cprog: CAST.Prog) = {
+ CFileOutputPhase(xCtx.leon, cprog)
+ }
+
+ private def compile(xCtx: ExtendedContext, cc: String)(unused: Unit) = {
+ val basename = s"${xCtx.tmpDir}/${xCtx.progName}"
+ val sourceFile = s"$basename.c"
+ val compiledProg = basename
+
+ val process = Process(s"$cc $ccflags $sourceFile -o $compiledProg")
+ val status = runProcess(process)
+
+ assert(status == 0, "Compilation of converted program failed")
+ }
+
+ private def evaluate(xCtx: ExtendedContext)(unused: Unit) = {
+ val compiledProg = s"${xCtx.tmpDir}/${xCtx.progName}"
+
+ // TODO memory limit
+ val process = Process(compiledProg)
+
+ val status = runProcess(process)
+ assert(status == 0, s"Evaluation of converted program failed with status [$status]")
+ }
+
+ private def forEachFileIn(cat: String)(block: (ExtendedContext, Program) => Unit) {
+ val fs = filesInResourceDir(testDir + cat, _.endsWith(".scala")).toList
+
+ fs foreach { file =>
+ assert(file.exists && file.isFile && file.canRead,
+ s"Benchmark ${file.getName} is not a readable file")
+ }
+
+ val files = fs map { _.getPath }
+
+ mkTest(files, cat)(block)
+ }
+
+ protected def testValid(cc: String) = forEachFileIn("valid") { (xCtx, prog) =>
+ val converter = convert(xCtx) _
+ val saver = saveToFile(xCtx) _
+ val compiler = compile(xCtx, cc) _
+ val evaluator = evaluate(xCtx) _
+
+ val pipeline = converter andThen saver andThen compiler andThen evaluator
+
+ pipeline(prog)
+ }
+
+ protected def testInvalid() = forEachFileIn("invalid") { (xCtx, prog) =>
+ intercept[LeonFatalError] {
+ GenerateCPhase(xCtx.leon, prog)
+ }
+ }
+
+ 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") }
+ }
+
+ testInvalid()
+ }
+
+ override def run(testName: Option[String], args: Args): Status = {
+ testAll()
+ super.run(testName, args)
+ }
+}
+
--
GitLab