test suite for Isabelle

build.sbt

@@ -120,10 +120,21 @@ testOptions in IntegrTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWi
 
 
 
-// RegressionTest Tests
+// Regression Tests
 lazy val RegressionTest = config("regression") extend(Test)
 
-testOptions in RegressionTest  := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "leon.regression."))
+testOptions in RegressionTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "leon.regression."))
+
+
+
+// Isabelle Tests
+lazy val IsabelleTest = config("isabelle") extend(Test)
+
+testOptions in IsabelleTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "leon.isabelle."))
+
+parallelExecution in IsabelleTest := false
+
+fork in IsabelleTest := true
 
 
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
@@ -133,9 +144,9 @@ lazy val bonsai      = ghProject("git://github.com/colder/bonsai.git",     "0fec
 lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "8aa4a5588653ce4986e3721115a62cc386714cc2")
 
 lazy val root = (project in file(".")).
-  configs(RegressionTest).
-  configs(IntegrTest).
+  configs(RegressionTest, IsabelleTest, IntegrTest).
   dependsOn(bonsai, scalaSmtLib).
   settings(inConfig(RegressionTest)(Defaults.testTasks ++ testSettings): _*).
   settings(inConfig(IntegrTest)(Defaults.testTasks ++ testSettings): _*).
+  settings(inConfig(IsabelleTest)(Defaults.testTasks ++ testSettings): _*).
   settings(inConfig(Test)(Defaults.testTasks ++ testSettings): _*)

src/test/resources/regression/verification/isabelle/error/FunctionsWrong.scala

+import leon._
+import leon.annotation._
+import leon.collection._
+import leon.lang._
+
+object FunctionsWrong {
+
+  def zero: BigInt = 0
+
+  // unsupported by Isabelle
+  // should report a 'fatal error' (not an 'internal error')
+
+  def length[A]: List[A] => BigInt = {
+    case Nil() => zero
+    case Cons(_, xs) => BigInt(1) + length(xs)
+  }
+
+  def test[A](xs: List[A]) = (length(xs) >= zero) holds
+
+}

src/test/resources/regression/verification/isabelle/error/MutualWrong.scala

+import leon.annotation._
+import leon.lang._
+
+object MutualWrong {
+
+  // unsupported by Isabelle
+  // should report a 'fatal error' (not an 'internal error')
+
+  sealed abstract class List1[A]
+  case class Cons1[A](head: A, tail: List2[A, A]) extends List1[A]
+
+  sealed abstract class List2[A, B]
+  case class Cons2[A, B](head: A, tail: List1[B]) extends List2[A, B]
+  case class Nil2[A, B]() extends List2[A, B]
+
+  def truth = true holds
+
+}

src/test/resources/regression/verification/isabelle/error/TypesWrong.scala

+import leon._
+import leon.collection._
+import leon.lang._
+
+object TypesWrong {
+
+  case class Data(xs: Array[Int])
+
+  def truth = true holds
+
+}

src/test/resources/regression/verification/isabelle/unknown/Casts.scala

+import leon._
+import leon.annotation._
+import leon.collection._
+import leon.lang._
+
+object Casts {
+
+  def check1[A](xs: List[A]) =
+    ((xs.size >= 1) || xs.asInstanceOf[Cons[A]].t == Nil[A]()).holds
+
+  def check2[A](xs: List[A]) =
+    ((xs.size != 1) || xs.asInstanceOf[Cons[A]].t == Nil[A]()).holds
+
+}

src/test/resources/regression/verification/isabelle/unknown/Mutual.scala

+import leon.annotation._
+import leon.lang._
+
+object Mutual {
+
+  sealed abstract class List1[A]
+  case class Cons1[A](head: A, tail: List2[A]) extends List1[A]
+
+  sealed abstract class List2[B]
+  case class Cons2[B](head: B, tail: List1[B]) extends List2[B]
+  case class Nil2[B]() extends List2[B]
+
+  def size1[A](list: List1[A]): BigInt = (list match {
+    case Cons1(_, t) => 1 + size2(t)
+  }) ensuring { _ >= BigInt(0) }
+
+  def size2[A](list: List2[A]): BigInt = (list match {
+    case Nil2() => BigInt(0)
+    case Cons2(_, t) => 1 + size1(t)
+  }) ensuring { _ >= BigInt(0) }
+
+}

src/test/resources/regression/verification/isabelle/valid/Datatypes.scala

+import leon.annotation._
+import leon.lang._
+
+object Datatypes {
+
+  sealed abstract class Foo[A]
+  sealed abstract class Bar[C] extends Foo[C]
+  case class Baz[B](underlying: B, rest: Baz[B]) extends Bar[B]
+  case class FooNil[D]() extends Foo[D]
+
+  def dest[B](baz1: Baz[B], baz2: Baz[B]) = {
+    require(baz1 == baz2)
+    baz1.underlying == baz2.underlying
+  } holds
+
+  def intro_dest[B](baz1: Baz[B], baz2: Baz[B], b1: B, b2: B) = {
+    require(b1 == b2)
+    val x1 = Baz(b1, baz1)
+    val x2 = Baz(b2, baz2)
+    x1.underlying == x2.underlying
+  } holds
+
+  def pm[A](foo: Foo[A]) = (foo match {
+    case Baz(x, y) => true
+    case FooNil() => true
+  }) holds
+
+  def pm2[A](foo: Foo[A]) = (foo match {
+    case Baz(x, y) => true
+    case z: FooNil[A] => true
+  }) holds
+
+  def pm3[A](int: BigInt) = (int match {
+    case BigInt(0) => true
+    case n => true
+  }) holds
+
+  def pm4[A](int: BigInt) = (int match {
+    case BigInt(0) => true
+    case n if false => true
+    case n => true
+  }) holds
+
+}

src/test/resources/regression/verification/isabelle/valid/Lists.scala

+import leon._
+import leon.annotation._
+import leon.collection._
+import leon.lang._
+
+object Lists {
+
+  @isabelle.script(
+    name = "Safe_Head",
+    source = """
+      fun safe_head where
+      "safe_head [] = None" |
+      "safe_head (x # _) = Some x"
+
+      lemma safe_head_eq_head[simp]:
+        assumes "~ List.null xs"
+        shows "safe_head xs = Some (hd xs)"
+      using assms
+      by (cases xs) auto
+    """
+  )
+  @isabelle.function(term = "Safe_Head.safe_head")
+  def safeHead[A](xs: List[A]): Option[A] = xs match {
+    case Nil() => None()
+    case Cons(x, _) => Some(x)
+  }
+
+  def lemma1[A](xs: List[A]) =
+    (xs.isEmpty || safeHead(xs) == Some(xs.asInstanceOf[Cons[A]].h)).holds
+
+  def lemma2[A](xs: List[A]) = {
+    require(!xs.isEmpty)
+    (xs.size > 0)
+  }.holds
+
+  def lemma3[A](xs: List[A], ys: List[A], zs: List[A]) =
+    ((xs ++ ys) ++ zs == xs ++ (ys ++ zs)).holds
+
+  def lemma4[A](xs: List[A], ys: List[A]) =
+    ((xs ++ ys).content == (ys ++ xs).content).holds
+
+  def lemma5[A](x: A, xs: List[A]) =
+    ((x :: xs).content == xs.content ++ Set(x)).holds
+
+  def lemma6[A](xs: List[A]) =
+    (xs.reverse.reverse == xs).holds
+
+  def lemma7[A, B](xs: List[A]) =
+    (xs.zip(Nil[B]()) == Nil[(A, B)]()).holds
+
+  def lemma7_check =
+    (lemma7[Int, Int](Nil())).holds
+
+  def lemma8[A](xs: List[A], x: A) =
+    ((xs - x).content == xs.content -- Set(x)).holds
+
+  def lemma9[A, B, C](xs: List[A], f: A => B, g: B => C) =
+    (xs.map(f).map(g) == xs.map(x => g(f(x)))).holds
+
+  @isabelle.function(term = "Fun.id")
+  def identity[A](x: A) = x
+
+  def lemma10[A](xs: List[A]) =
+    (xs.map(identity) == xs).holds
+
+  @isabelle.proof(method = """(induct "<var xs>", auto)""")
+  def lemma11[A, B, C](xs: List[A], f: A => List[B], g: B => List[C]) =
+    (xs.flatMap(f).flatMap(g) == xs.flatMap(x => f(x).flatMap(g))).holds
+
+  def safeHead2[A](xs: List[A]): A = {
+    require(xs.size > 0)
+    xs.asInstanceOf[Cons[A]].h
+  }
+
+  def lemma12[A](xs: List[A]) =
+    (xs.isEmpty || safeHead2(xs) == xs.asInstanceOf[Cons[A]].h).holds
+
+  def lemma13[A](xs: List[A], x: A) =
+    ((x :: xs).apply(0) == x).holds
+
+  def lenTailrec[T](xs: List[T], n: BigInt): BigInt = xs match {
+    case Nil() => n
+    case Cons(_, xs) => lenTailrec(xs, 1 + n)
+  }
+
+  @isabelle.proof(method = """(induct "<var xs>" "<var n>" rule: [[leon_induct lenTailrec]], auto)""")
+  def lemma14[A](xs: List[A], n: BigInt) =
+    (lenTailrec(xs, n) >= n).holds
+
+}

src/test/resources/regression/verification/isabelle/valid/Overlapping.scala

+import leon.annotation._
+import leon.collection._
+import leon.lang._
+
+object Overlapping {
+
+  def overlapped[A](xs: List[A]) = {
+    require { xs.isInstanceOf[Cons[A]] }
+
+    xs match {
+      case Cons(x1, Cons(x2, xs)) => true
+      case Cons(x1, xs) => true
+      case _ => false
+    }
+  }.holds
+
+}

src/test/resources/regression/verification/isabelle/valid/Reals.scala

+import leon._
+import leon.lang._
+import leon.annotation._
+
+object Reals {
+
+  def comm(x: Real, y: Real) =
+    (x + y == y + x).holds
+
+  def assoc(x: Real, y: Real, z: Real) =
+    ((x * y) * z == x * (y * z)).holds
+
+}

src/test/scala/leon/isabelle/IsabelleLibrarySuite.scala

+package leon.isabelle
+
+import scala.concurrent._
+import scala.concurrent.duration._
+import scala.concurrent.ExecutionContext.Implicits.global
+
+import leon._
+import leon.frontends.scalac.ExtractionPhase
+import leon.purescala.Definitions._
+import leon.utils._
+import leon.solvers.isabelle._
+import leon.test._
+import leon.utils.PreprocessingPhase
+
+class IsabelleLibrarySuite extends LeonRegressionSuite {
+
+  object IsabelleNoopPhase extends LeonPhase[Program, Unit] {
+    val name = "isabelle-noop"
+    val description = "Isabelle definitions"
+
+    implicit val debugSection = DebugSectionIsabelle
+
+    def run(context: LeonContext)(program: Program): Unit =
+      Await.result(IsabelleEnvironment(context, program).map(_ => ()), Duration.Inf)
+  }
+
+  test("Define the library") {
+    val pipeline = ExtractionPhase andThen new PreprocessingPhase andThen IsabelleNoopPhase
+
+    val ctx = Main.processOptions(Seq("--isabelle:download=true", "--functions=_")).copy(reporter = new TestSilentReporter())
+
+    pipeline.run(ctx)(Nil)
+  }
+
+}

src/test/scala/leon/isabelle/IsabelleVerificationSuite.scala

+package leon.isabelle
+
+import leon._
+import leon.regression.verification._
+import leon.solvers.isabelle.AdaptationPhase
+import leon.test._
+import leon.verification.AnalysisPhase
+
+class IsabelleVerificationSuite extends VerificationSuite {
+
+  val testDir = "regression/verification/isabelle/"
+  val pipeFront = xlang.NoXLangFeaturesChecking
+  val pipeBack = AdaptationPhase andThen AnalysisPhase
+  val optionVariants: List[List[String]] = List(List("--isabelle:download=true", "--solvers=isabelle"))
+
+}