From 817dd1030269d8cc0895008e3664ceb562eecdd2 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Fri, 13 Feb 2015 15:53:21 +0100
Subject: [PATCH] Repair regression tests
---
.../regression/repair/Compiler1.scala | 176 ++++++++
.../resources/regression/repair/Heap4.scala | 113 +++++
.../resources/regression/repair/List1.scala | 420 ++++++++++++++++++
.../regression/repair/MergeSort2.scala | 54 +++
.../regression/repair/Numerical1.scala | 53 +++
.../scala/leon/test/repair/RepairSuite.scala | 40 ++
6 files changed, 856 insertions(+)
create mode 100644 src/test/resources/regression/repair/Compiler1.scala
create mode 100644 src/test/resources/regression/repair/Heap4.scala
create mode 100644 src/test/resources/regression/repair/List1.scala
create mode 100644 src/test/resources/regression/repair/MergeSort2.scala
create mode 100644 src/test/resources/regression/repair/Numerical1.scala
create mode 100644 src/test/scala/leon/test/repair/RepairSuite.scala
diff --git a/src/test/resources/regression/repair/Compiler1.scala b/src/test/resources/regression/repair/Compiler1.scala
new file mode 100644
index 000000000..2971855c7
--- /dev/null
+++ b/src/test/resources/regression/repair/Compiler1.scala
@@ -0,0 +1,176 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Neg(desugar(lhs)) // FIXME: Complete nonsense. Leon can't disprove it, uses example...
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ ((e, res) passes {
+ case Trees.Plus(Trees.IntLiteral(i), Trees.Minus(Trees.IntLiteral(j), Trees.IntLiteral(42))) =>
+ Plus(Literal(i), Plus(Literal(j), Neg(Literal(42))))
+ }) &&
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
diff --git a/src/test/resources/regression/repair/Heap4.scala b/src/test/resources/regression/repair/Heap4.scala
new file mode 100644
index 000000000..a19ff6c20
--- /dev/null
+++ b/src/test/resources/regression/repair/Heap4.scala
@@ -0,0 +1,113 @@
+/* Copyright 2009-2013 EPFL, Lausanne
+ *
+ * Author: Ravi
+ * Date: 20.11.2013
+ **/
+
+import leon.collection._
+import leon._
+
+object HeapSort {
+
+ sealed abstract class Heap {
+ val rank : Int = this match {
+ case Leaf() => 0
+ case Node(_, l, r) =>
+ 1 + max(l.rank, r.rank)
+ }
+ def content : Set[Int] = this match {
+ case Leaf() => Set[Int]()
+ case Node(v,l,r) => l.content ++ Set(v) ++ r.content
+ }
+ }
+ case class Leaf() extends Heap
+ case class Node(value:Int, left: Heap, right: Heap) extends Heap
+
+ def max(i1 : Int, i2 : Int) = if (i1 >= i2) i1 else i2
+
+ def hasHeapProperty(h : Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(v, l, r) =>
+ ( l match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ }) &&
+ ( r match {
+ case Leaf() => true
+ case n@Node(v2,_,_) => v >= v2 && hasHeapProperty(n)
+ })
+ }
+
+ def hasLeftistProperty(h: Heap) : Boolean = h match {
+ case Leaf() => true
+ case Node(_,l,r) =>
+ hasLeftistProperty(l) &&
+ hasLeftistProperty(r) &&
+ l.rank >= r.rank
+ }
+
+ def heapSize(t: Heap): Int = { t match {
+ case Leaf() => 0
+ case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
+ }} ensuring(_ >= 0)
+
+ private def merge(h1: Heap, h2: Heap) : Heap = {
+ require(
+ hasLeftistProperty(h1) && hasLeftistProperty(h2) &&
+ hasHeapProperty(h1) && hasHeapProperty(h2)
+ )
+ (h1,h2) match {
+ case (Leaf(), _) => h2
+ case (_, Leaf()) => h2 // FIXME h2 instead of h1
+ case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+ if(v1 >= v2)
+ makeN(v1, l1, merge(r1, h2))
+ else
+ makeN(v2, l2, merge(h1, r2))
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(h1) + heapSize(h2) == heapSize(res) &&
+ h1.content ++ h2.content == res.content
+ }
+
+ private def makeN(value: Int, left: Heap, right: Heap) : Heap = {
+ require(
+ hasLeftistProperty(left) && hasLeftistProperty(right)
+ )
+ if(left.rank >= right.rank)
+ Node(value, left, right)
+ else
+ Node(value, right, left)
+ } ensuring { res =>
+ hasLeftistProperty(res) }
+
+ def insert(element: Int, heap: Heap) : Heap = {
+ require(hasLeftistProperty(heap) && hasHeapProperty(heap))
+
+ merge(Node(element, Leaf(), Leaf()), heap)
+
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res) &&
+ heapSize(res) == heapSize(heap) + 1 &&
+ res.content == heap.content ++ Set(element)
+ }
+
+ def findMax(h: Heap) : Option[Int] = {
+ h match {
+ case Node(m,_,_) => Some(m)
+ case Leaf() => None()
+ }
+ }
+
+ def removeMax(h: Heap) : Heap = {
+ require(hasLeftistProperty(h) && hasHeapProperty(h))
+ h match {
+ case Node(_,l,r) => merge(l, r)
+ case l => l
+ }
+ } ensuring { res =>
+ hasLeftistProperty(res) && hasHeapProperty(res)
+ }
+
+}
diff --git a/src/test/resources/regression/repair/List1.scala b/src/test/resources/regression/repair/List1.scala
new file mode 100644
index 000000000..1e18ca898
--- /dev/null
+++ b/src/test/resources/regression/repair/List1.scala
@@ -0,0 +1,420 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.custom
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List0[T] {
+ def size: Int = (this match {
+ case Nil0() => 0
+ case Cons0(h, t) => 1 + t.size
+ }) ensuring (_ >= 0)
+
+ def content: Set[T] = this match {
+ case Nil0() => Set()
+ case Cons0(h, t) => Set(h) ++ t.content
+ }
+
+ def contains(v: T): Boolean = (this match {
+ case Cons0(h, t) if h == v => true
+ case Cons0(_, t) => t.contains(v)
+ case Nil0() => false
+ }) ensuring { res => res == (content contains v) }
+
+ def ++(that: List0[T]): List0[T] = (this match {
+ case Nil0() => that
+ case Cons0(x, xs) => Cons0(x, xs ++ that)
+ }) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
+
+ def head: T = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => h
+ }
+ }
+
+ def tail: List0[T] = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => t
+ }
+ }
+
+ def apply(index: Int): T = {
+ require(0 <= index && index < size)
+ if (index == 0) {
+ head
+ } else {
+ tail(index-1)
+ }
+ }
+
+ def ::(t:T): List0[T] = Cons0(t, this)
+
+ def :+(t:T): List0[T] = {
+ this match {
+ case Nil0() => Cons0(t, this)
+ case Cons0(x, xs) => Cons0(x, xs :+ (t))
+ }
+ } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+ def reverse: List0[T] = {
+ this match {
+ case Nil0() => this
+ case Cons0(x,xs) => xs.reverse :+ x
+ }
+ } ensuring (res => (res.size == size) && (res.content == content))
+
+ def take(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Nil0()
+ } else {
+ Cons0(h, t.take(i-1))
+ }
+ }
+
+ def drop(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Cons0(h, t)
+ } else {
+ t.drop(i-1)
+ }
+ }
+
+ def slice(from: Int, to: Int): List0[T] = {
+ require(from < to && to < size && from >= 0)
+ drop(from).take(to-from)
+ }
+
+ def replace(from: T, to: T): List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ val r = t.replace(from, to)
+ if (h == from) {
+ Cons0(to, r)
+ } else {
+ Cons0(h, r)
+ }
+ }
+
+ private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+ case Nil0() =>
+ if (acc.size > 0) {
+ res :+ acc
+ } else {
+ res
+ }
+ case Cons0(h, t) =>
+ if (s0 == 0) {
+ chunk0(s, l, Nil0(), res :+ acc, s)
+ } else {
+ chunk0(s, t, acc :+ h, res, s0-1)
+ }
+ }
+
+ def chunks(s: Int): List0[List0[T]] = {
+ require(s > 0)
+
+ chunk0(s, this, Nil0(), Nil0(), s)
+ }
+
+ def zip[B](that: List0[B]): List0[(T, B)] = (this, that) match {
+ case (Cons0(h1, t1), Cons0(h2, t2)) =>
+ Cons0((h1, h2), t1.zip(t2))
+ case (_) =>
+ Nil0()
+ }
+
+ def -(e: T): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (e == h) {
+ t - e
+ } else {
+ Cons0(h, t - e)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def --(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ t -- that
+ } else {
+ Cons0(h, t -- that)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def &(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ Cons0(h, t & that)
+ } else {
+ t & that
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def pad(s: Int, e: T): List0[T] = { (this, s) match {
+ case (_, s) if s <= 0 =>
+ this
+ case (Nil0(), s) =>
+ Cons0(e, Nil0().pad(s-1, e))
+ case (Cons0(h, t), s) =>
+ Cons0(h, t.pad(s-1, e)) // FIXME should be s
+ }} ensuring { res =>
+ ((this,s,e), res) passes {
+ case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+ }
+ }
+
+ def find(e: T): Option[Int] = this match {
+ case Nil0() => None()
+ case Cons0(h, t) =>
+ if (h == e) {
+ Some(0)
+ } else {
+ t.find(e) match {
+ case None() => None()
+ case Some(i) => Some(i+1)
+ }
+ }
+ }
+
+ def init: List0[T] = (this match {
+ case Cons0(h, Nil0()) =>
+ Nil0[T]()
+ case Cons0(h, t) =>
+ Cons0[T](h, t.init)
+ case Nil0() =>
+ Nil0[T]()
+ }) ensuring ( (r: List0[T]) => ((r.size < this.size) || (this.size == 0)) )
+
+ def lastOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ t.lastOption.orElse(Some(h))
+ case Nil0() =>
+ None()
+ }
+
+ def firstOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ Some(h)
+ case Nil0() =>
+ None()
+ }
+
+ def unique: List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ Cons0(h, t.unique - h)
+ }
+
+ def splitAt(e: T): List0[List0[T]] = split(Cons0(e, Nil0()))
+
+ def split(seps: List0[T]): List0[List0[T]] = this match {
+ case Cons0(h, t) =>
+ if (seps.contains(h)) {
+ Cons0(Nil0(), t.split(seps))
+ } else {
+ val r = t.split(seps)
+ Cons0(Cons0(h, r.head), r.tail)
+ }
+ case Nil0() =>
+ Cons0(Nil0(), Nil0())
+ }
+
+ def count(e: T): Int = this match {
+ case Cons0(h, t) =>
+ if (h == e) {
+ 1 + t.count(e)
+ } else {
+ t.count(e)
+ }
+ case Nil0() =>
+ 0
+ }
+
+ def evenSplit: (List0[T], List0[T]) = {
+ val c = size/2
+ (take(c), drop(c))
+ }
+
+ def insertAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ insertAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.insertAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ replaceAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this.drop(l.size)
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.replaceAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def rotate(s: Int): List0[T] = {
+ if (s < 0) {
+ rotate(size+s)
+ } else {
+ val s2 = s % size
+ drop(s2) ++ take(s2)
+ }
+ }
+
+ def isEmpty = this match {
+ case Nil0() => true
+ case _ => false
+ }
+
+}
+
+@ignore
+object List0 {
+ def apply[T](elems: T*): List0[T] = ???
+}
+
+@library
+object List0Ops {
+ def flatten[T](ls: List0[List0[T]]): List0[T] = ls match {
+ case Cons0(h, t) => h ++ flatten(t)
+ case Nil0() => Nil0()
+ }
+
+ def isSorted(ls: List0[Int]): Boolean = ls match {
+ case Nil0() => true
+ case Cons0(_, Nil0()) => true
+ case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
+ case Cons0(_, t) => isSorted(t)
+ }
+
+ def sorted(ls: List0[Int]): List0[Int] = ls match {
+ case Cons0(h, t) => insSort(sorted(t), h)
+ case Nil0() => Nil0()
+ }
+
+ def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+ case Nil0() => Cons0(v, Nil0())
+ case Cons0(h, t) =>
+ if (v <= h) {
+ Cons0(v, t)
+ } else {
+ Cons0(h, insSort(t, v))
+ }
+ }
+}
+
+
+case class Cons0[T](h: T, t: List0[T]) extends List0[T]
+case class Nil0[T]() extends List0[T]
+
+@library
+object List0Specs {
+ def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+ require(0 <= i && i < l.size + 1)
+ // proof:
+ (l match {
+ case Nil0() => true
+ case Cons0(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+ }) &&
+ // claim:
+ ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+ }.holds
+
+ def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l.size)
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+ }) &&
+ (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+ }.holds
+
+ def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l1.size + l2.size)
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+ }) &&
+ ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+ }.holds
+
+ def appendAssoc[T](l1 : List0[T], l2 : List0[T], l3 : List0[T]) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => appendAssoc(xs,l2,l3)
+ }) &&
+ (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+ }.holds
+
+ def snocIsAppend[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIsAppend(xs,t)
+ }) &&
+ ((l :+ t) == l ++ Cons0[T](t, Nil0()))
+ }.holds
+
+ def snocAfterAppend[T](l1 : List0[T], l2 : List0[T], t : T) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocAfterAppend(xs,l2,t)
+ }) &&
+ ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+ }.holds
+
+ def snocReverse[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocReverse(xs,t)
+ }) &&
+ ((l :+ t).reverse == Cons0(t, l.reverse))
+ }.holds
+
+ def reverseReverse[T](l : List0[T]) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+ }) &&
+ (l.reverse.reverse == l)
+ }.holds
+
+ //// my hand calculation shows this should work, but it does not seem to be found
+ //def reverseAppend[T](l1 : List0[T], l2 : List0[T]) : Boolean = {
+ // (l1 match {
+ // case Nil0() => true
+ // case Cons0(x,xs) => {
+ // reverseAppend(xs,l2) &&
+ // snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+ // l1.reverse == (xs.reverse :+ x)
+ // }
+ // }) &&
+ // ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+ //}.holds
+}
diff --git a/src/test/resources/regression/repair/MergeSort2.scala b/src/test/resources/regression/repair/MergeSort2.scala
new file mode 100644
index 000000000..d9966ecdc
--- /dev/null
+++ b/src/test/resources/regression/repair/MergeSort2.scala
@@ -0,0 +1,54 @@
+import leon.collection._
+
+object MergeSort {
+
+ def split(l : List[Int]) : (List[Int],List[Int]) = { l match {
+ case Cons(a, Cons(b, t)) =>
+ val (rec1, rec2) = split(t)
+ (Cons(a, rec1), Cons(b, rec2))
+ case other => (other, Nil())
+ }} ensuring { res =>
+ val (l1, l2) = res
+ l1.size >= l2.size &&
+ l1.size <= l2.size + 1 &&
+ l1.size + l2.size == l.size &&
+ l1.content ++ l2.content == l.content
+ }
+
+ def isSorted(l : List[Int]) : Boolean = l match {
+ case Cons(x, t@Cons(y, _)) => x <= y && isSorted(t)
+ case _ => true
+ }
+
+ def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+ require(isSorted(l1) && isSorted(l2))
+ (l1, l2) match {
+ case (Cons(h1, t1), Cons(h2,t2)) =>
+ if (h1 <= h2)
+ Cons(h1, merge(t1, l2))
+ else
+ Cons(h1, merge(l1, t2)) // FIXME h1 instead of h2
+ case (Nil(), _) => l2
+ case (_, Nil()) => l1
+ }
+ } ensuring { res =>
+ isSorted(res) &&
+ res.size == l1.size + l2.size &&
+ res.content == l1.content ++ l2.content
+ }
+
+ def mergeSort(l : List[Int]) : List[Int] = { l match {
+ case Nil() => l
+ case Cons(_, Nil()) => l
+ case other =>
+ val (l1, l2) = split(other)
+ merge(mergeSort(l1), mergeSort(l2))
+ }} ensuring { res =>
+ isSorted(res) &&
+ res.content == l.content &&
+ res.size == l.size
+ }
+}
+
+
+
diff --git a/src/test/resources/regression/repair/Numerical1.scala b/src/test/resources/regression/repair/Numerical1.scala
new file mode 100644
index 000000000..4f1a32f8b
--- /dev/null
+++ b/src/test/resources/regression/repair/Numerical1.scala
@@ -0,0 +1,53 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+object Numerical {
+ def power(base: Int, p: Int): Int = {
+ require(p >= 0)
+ if (p == 0) {
+ 1
+ } else if (p%2 == 0) {
+ power(base*base, p/2)
+ } else {
+ power(base, p-1) // fixme: Missing base*
+ }
+ } ensuring {
+ res => ((base, p), res) passes {
+ case (_, 0) => 1
+ case (b, 1) => b
+ case (2, 7) => 128
+ case (2, 10) => 1024
+ }
+ }
+
+ def gcd(a: Int, b: Int): Int = {
+ require(a > 0 && b > 0);
+
+ if (a == b) {
+ a
+ } else if (a > b) {
+ gcd(a-b, b)
+ } else {
+ gcd(a, b-a)
+ }
+ } ensuring {
+ res => (a%res == 0) && (b%res == 0) && (((a,b), res) passes {
+ case (468, 24) => 12
+ })
+ }
+
+ def moddiv(a: Int, b: Int): (Int, Int) = {
+ require(a >= 0 && b > 0);
+ if (b > a) {
+ (a, 0)
+ } else {
+ val (r1, r2) = moddiv(a-b, b)
+ (r1, r2+1)
+ }
+ } ensuring {
+ res => b*res._2 + res._1 == a
+ }
+}
diff --git a/src/test/scala/leon/test/repair/RepairSuite.scala b/src/test/scala/leon/test/repair/RepairSuite.scala
new file mode 100644
index 000000000..a68249dcf
--- /dev/null
+++ b/src/test/scala/leon/test/repair/RepairSuite.scala
@@ -0,0 +1,40 @@
+package leon.test.repair
+
+import leon.test._
+import leon._
+import leon.utils._
+import leon.frontends.scalac.ExtractionPhase
+import leon.repair._
+
+class RepairSuite extends LeonTestSuite {
+ val pipeline = ExtractionPhase andThen
+ PreprocessingPhase andThen
+ RepairPhase
+
+ val settings = Settings(verify = false, repair = true)
+ val reporter = new DefaultReporter(settings)
+ val ctx0 = LeonContext(
+ reporter,
+ new InterruptManager(reporter)
+ )
+
+ val fileToFun = Map(
+ "Compiler1.scala" -> "desugar",
+ "Heap4.scala" -> "merge",
+ "List1.scala" -> "_pad",
+ "Numerical1.scala" -> "power",
+ "MergeSort2.scala" -> "merge"
+ )
+
+ for (file <- filesInResourceDir("regression/repair/")) {
+ val path = file.getAbsoluteFile().toString
+ val name = file.getName()
+ val option = LeonValueOption("functions", fileToFun(name))
+ val ctx = ctx0.copy(options = option +: ctx0.options)
+ test(name) {
+ pipeline.run(ctx)(List(path))
+ }
+ }
+
+
+}
\ No newline at end of file
--
GitLab