diff --git a/src/main/scala/leon/plugin/ExtractorPhase.scala b/src/main/scala/leon/plugin/ExtractorPhase.scala index ef94d03e53d357b4837173ff49cdf2d082fc3d97..fdc271d53cc641d587dde3fbef7b1520579f28e4 100644 --- a/src/main/scala/leon/plugin/ExtractorPhase.scala +++ b/src/main/scala/leon/plugin/ExtractorPhase.scala @@ -12,6 +12,8 @@ object ExtractionPhase extends LeonPhase[List[String], Program] { def run(ctx: LeonContext)(args: List[String]): Program = { val settings = new NSCSettings + settings.usejavacp.value = true + val compilerOpts = args.filterNot(_.startsWith("--")) val command = new CompilerCommand(compilerOpts, settings) { diff --git a/src/main/scala/leon/verification/Analysis.scala b/src/main/scala/leon/verification/Analysis.scala index 94567233d6501e68adc1e0a3317d3aea80c29bcc..500606ac05704ded8282625301e2d9353cb30b02 100644 --- a/src/main/scala/leon/verification/Analysis.scala +++ b/src/main/scala/leon/verification/Analysis.scala @@ -13,7 +13,7 @@ import solvers.{Solver,TrivialSolver} import scala.collection.mutable.{Set => MutableSet} -class Analysis(val program : Program, val reporter: Reporter = Settings.reporter) { +class Analysis(val program : Program, val reporter: Reporter) { Extensions.loadAll(reporter) val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala index 69e35fe0bbab96804fd8703ecab3049bd1db9fad..3a218804c0052a80e442b0fbbfd7cdacfe5a3fe0 100644 --- a/src/main/scala/leon/verification/AnalysisPhase.scala +++ b/src/main/scala/leon/verification/AnalysisPhase.scala @@ -8,6 +8,6 @@ object AnalysisPhase extends UnitPhase[Program] { val description = "Leon Analyses" def apply(ctx: LeonContext, program: Program) { - new Analysis(program).analyse + new Analysis(program, ctx.reporter).analyse } } diff --git a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala new file mode 100644 index 0000000000000000000000000000000000000000..dd5a75f89735805a74612665e487aa8fa99ec397 --- /dev/null +++ b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala @@ -0,0 +1,124 @@ +import scala.collection.immutable.Set +import leon.Utils._ +import leon.Annotations._ + +object AmortizedQueue { + sealed abstract class List + case class Cons(head : Int, tail : List) extends List + case class Nil() extends List + + sealed abstract class AbsQueue + case class Queue(front : List, rear : List) extends AbsQueue + + def size(list : List) : Int = (list match { + case Nil() => 0 + case Cons(_, xs) => 1 + size(xs) + }) ensuring(_ >= 0) + + def content(l: List) : Set[Int] = l match { + case Nil() => Set.empty[Int] + case Cons(x, xs) => Set(x) ++ content(xs) + } + + def asList(queue : AbsQueue) : List = queue match { + case Queue(front, rear) => concat(front, reverse(rear)) + } + + def concat(l1 : List, l2 : List) : List = (l1 match { + case Nil() => l2 + case Cons(x,xs) => Cons(x, concat(xs, l2)) + }) ensuring (res => size(res) == size(l1) + size(l2) && content(res) == content(l1) ++ content(l2)) + + def isAmortized(queue : AbsQueue) : Boolean = queue match { + case Queue(front, rear) => size(front) >= size(rear) + } + + def isEmpty(queue : AbsQueue) : Boolean = queue match { + case Queue(Nil(), Nil()) => true + case _ => false + } + + def reverse(l : List) : List = (l match { + case Nil() => Nil() + case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil())) + }) ensuring (content(_) == content(l)) + + def amortizedQueue(front : List, rear : List) : AbsQueue = { + if (size(rear) <= size(front)) + Queue(front, rear) + else + Queue(concat(front, reverse(rear)), Nil()) + } ensuring(isAmortized(_)) + + def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = (queue match { + case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear)) + }) ensuring(isAmortized(_)) + + def tail(queue : AbsQueue) : AbsQueue = { + require(isAmortized(queue) && !isEmpty(queue)) + queue match { + case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear) + } + } ensuring (isAmortized(_)) + + def front(queue : AbsQueue) : Int = { + require(isAmortized(queue) && !isEmpty(queue)) + queue match { + case Queue(Cons(f, _), _) => f + } + } + + // @induct + // def propEnqueue(rear : List, front : List, list : List, elem : Int) : Boolean = { + // require(isAmortized(Queue(front, rear))) + // val queue = Queue(front, rear) + // if (asList(queue) == list) { + // asList(enqueue(queue, elem)) == concat(list, Cons(elem, Nil())) + // } else + // true + // } holds + + @induct + def propFront(queue : AbsQueue, list : List, elem : Int) : Boolean = { + require(!isEmpty(queue) && isAmortized(queue)) + if (asList(queue) == list) { + list match { + case Cons(x, _) => front(queue) == x + } + } else + true + } holds + + @induct + def propTail(rear : List, front : List, list : List, elem : Int) : Boolean = { + require(!isEmpty(Queue(front, rear)) && isAmortized(Queue(front, rear))) + if (asList(Queue(front, rear)) == list) { + list match { + case Cons(_, xs) => asList(tail(Queue(front, rear))) == xs + } + } else + true + } // holds + + def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = { + if (isEmpty(queue)) + front(enqueue(queue, elem)) == elem + else + true + } holds + + def enqueueDequeueThrice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = { + if (isEmpty(queue)) { + val q1 = enqueue(queue, e1) + val q2 = enqueue(q1, e2) + val q3 = enqueue(q2, e3) + val e1prime = front(q3) + val q4 = tail(q3) + val e2prime = front(q4) + val q5 = tail(q4) + val e3prime = front(q5) + e1 == e1prime && e2 == e2prime && e3 == e3prime + } else + true + } holds +} diff --git a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala new file mode 100644 index 0000000000000000000000000000000000000000..f5a2fc0415a2cf6023f9ae1f3620e99f9fdc27cb --- /dev/null +++ b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala @@ -0,0 +1,50 @@ +import scala.collection.immutable.Set +import leon.Utils._ +import leon.Annotations._ + +object AssociativeList { + sealed abstract class KeyValuePairAbs + case class KeyValuePair(key: Int, value: Int) extends KeyValuePairAbs + + sealed abstract class List + case class Cons(head: KeyValuePairAbs, tail: List) extends List + case class Nil() extends List + + sealed abstract class OptionInt + case class Some(i: Int) extends OptionInt + case class None() extends OptionInt + + def domain(l: List): Set[Int] = l match { + case Nil() => Set.empty[Int] + case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs) + } + + def find(l: List, e: Int): OptionInt = l match { + case Nil() => None() + case Cons(KeyValuePair(k, v), xs) => if (k == e) Some(v) else find(xs, e) + } + + def noDuplicates(l: List): Boolean = l match { + case Nil() => true + case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None() && noDuplicates(xs) + } + + def update(l1: List, l2: List): List = (l2 match { + case Nil() => l1 + case Cons(x, xs) => update(updateElem(l1, x), xs) + }) ensuring(domain(_) == domain(l1) ++ domain(l2)) + + def updateElem(l: List, e: KeyValuePairAbs): List = (l match { + case Nil() => Cons(e, Nil()) + case Cons(KeyValuePair(k, v), xs) => e match { + case KeyValuePair(ek, ev) => if (ek == k) Cons(KeyValuePair(ek, ev), xs) else Cons(KeyValuePair(k, v), updateElem(xs, e)) + } + }) ensuring(res => e match { + case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k) + }) + + @induct + def readOverWrite(l: List, k1: Int, k2: Int, e: Int) : Boolean = { + find(updateElem(l, KeyValuePair(k2,e)), k1) == (if (k1 == k2) Some(e) else find(l, k1)) + } holds +} diff --git a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala new file mode 100644 index 0000000000000000000000000000000000000000..d2ae67b3bb465f13437a1eb70a57a8e7e613347a --- /dev/null +++ b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala @@ -0,0 +1,80 @@ +import scala.collection.immutable.Set +import leon.Annotations._ +import leon.Utils._ + +object InsertionSort { + sealed abstract class List + case class Cons(head:Int,tail:List) extends List + case class Nil() extends List + + sealed abstract class OptInt + case class Some(value: Int) extends OptInt + case class None() extends OptInt + + def size(l : List) : Int = (l match { + case Nil() => 0 + case Cons(_, xs) => 1 + size(xs) + }) ensuring(_ >= 0) + + def contents(l: List): Set[Int] = l match { + case Nil() => Set.empty + case Cons(x,xs) => contents(xs) ++ Set(x) + } + + def min(l : List) : OptInt = l match { + case Nil() => None() + case Cons(x, xs) => min(xs) match { + case None() => Some(x) + case Some(x2) => if(x < x2) Some(x) else Some(x2) + } + } + + def isSorted(l: List): Boolean = l match { + case Nil() => true + case Cons(x, Nil()) => true + case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys)) + } + + /* Inserting element 'e' into a sorted list 'l' produces a sorted list with + * the expected content and size */ + def sortedIns(e: Int, l: List): List = { + require(isSorted(l)) + l match { + case Nil() => Cons(e,Nil()) + case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l) + } + } ensuring(res => contents(res) == contents(l) ++ Set(e) + && isSorted(res) + && size(res) == size(l) + 1 + ) + + /* Inserting element 'e' into a sorted list 'l' produces a sorted list with + * the expected content and size */ + def buggySortedIns(e: Int, l: List): List = { + // require(isSorted(l)) + l match { + case Nil() => Cons(e,Nil()) + case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l) + } + } ensuring(res => contents(res) == contents(l) ++ Set(e) + && isSorted(res) + && size(res) == size(l) + 1 + ) + + /* Insertion sort yields a sorted list of same size and content as the input + * list */ + def sort(l: List): List = (l match { + case Nil() => Nil() + case Cons(x,xs) => sortedIns(x, sort(xs)) + }) ensuring(res => contents(res) == contents(l) + && isSorted(res) + && size(res) == size(l) + ) + + def main(args: Array[String]): Unit = { + val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil())))))) + + println(ls) + println(sort(ls)) + } +} diff --git a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala new file mode 100644 index 0000000000000000000000000000000000000000..a4fc4f8dc44a90f59a772b52b1a05053316e94d2 --- /dev/null +++ b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala @@ -0,0 +1,107 @@ +import scala.collection.immutable.Set +import leon.Annotations._ +import leon.Utils._ + +object ListOperations { + sealed abstract class List + case class Cons(head: Int, tail: List) extends List + case class Nil() extends List + + sealed abstract class IntPairList + case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList + case class IPNil() extends IntPairList + + sealed abstract class IntPair + case class IP(fst: Int, snd: Int) extends IntPair + + def size(l: List) : Int = (l match { + case Nil() => 0 + case Cons(_, t) => 1 + size(t) + }) ensuring(res => res >= 0) + + def iplSize(l: IntPairList) : Int = (l match { + case IPNil() => 0 + case IPCons(_, xs) => 1 + iplSize(xs) + }) ensuring(_ >= 0) + + def zip(l1: List, l2: List) : IntPairList = { + // try to comment this and see how pattern-matching becomes + // non-exhaustive and post-condition fails + require(size(l1) == size(l2)) + + l1 match { + case Nil() => IPNil() + case Cons(x, xs) => l2 match { + case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys)) + } + } + } ensuring(iplSize(_) == size(l1)) + + def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0) + def sizeTailRecAcc(l: List, acc: Int) : Int = { + require(acc >= 0) + l match { + case Nil() => acc + case Cons(_, xs) => sizeTailRecAcc(xs, acc+1) + } + } ensuring(res => res == size(l) + acc) + + def sizesAreEquiv(l: List) : Boolean = { + size(l) == sizeTailRec(l) + } holds + + def content(l: List) : Set[Int] = l match { + case Nil() => Set.empty[Int] + case Cons(x, xs) => Set(x) ++ content(xs) + } + + def sizeAndContent(l: List) : Boolean = { + size(l) == 0 || content(l) != Set.empty[Int] + } holds + + def drunk(l : List) : List = (l match { + case Nil() => Nil() + case Cons(x,l1) => Cons(x,Cons(x,drunk(l1))) + }) ensuring (size(_) == 2 * size(l)) + + def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l)) + def reverse0(l1: List, l2: List) : List = (l1 match { + case Nil() => l2 + case Cons(x, xs) => reverse0(xs, Cons(x, l2)) + }) ensuring(content(_) == content(l1) ++ content(l2)) + + def append(l1 : List, l2 : List) : List = (l1 match { + case Nil() => l2 + case Cons(x,xs) => Cons(x, append(xs, l2)) + }) ensuring(content(_) == content(l1) ++ content(l2)) + + @induct + def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds + + @induct + def appendAssoc(xs : List, ys : List, zs : List) : Boolean = + (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds + + def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = { + (append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2)) + } holds + + @induct + def sizeAppend(l1 : List, l2 : List) : Boolean = + (size(append(l1, l2)) == size(l1) + size(l2)) holds + + @induct + def concat(l1: List, l2: List) : List = + concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2)) + + @induct + def concat0(l1: List, l2: List, l3: List) : List = (l1 match { + case Nil() => l2 match { + case Nil() => reverse(l3) + case Cons(y, ys) => { + concat0(Nil(), ys, Cons(y, l3)) + } + } + case Cons(x, xs) => concat0(xs, l2, Cons(x, l3)) + }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3)) +} diff --git a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala new file mode 100644 index 0000000000000000000000000000000000000000..a35c3ef9be56871900d5e9474b385f0896edccd4 --- /dev/null +++ b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala @@ -0,0 +1,86 @@ +import scala.collection.immutable.Set +import leon.Utils._ +import leon.Annotations._ + +object PropositionalLogic { + + sealed abstract class Formula + case class And(lhs: Formula, rhs: Formula) extends Formula + case class Or(lhs: Formula, rhs: Formula) extends Formula + case class Implies(lhs: Formula, rhs: Formula) extends Formula + case class Not(f: Formula) extends Formula + case class Literal(id: Int) extends Formula + + def simplify(f: Formula): Formula = (f match { + case And(lhs, rhs) => And(simplify(lhs), simplify(rhs)) + case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs)) + case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs)) + case Not(f) => Not(simplify(f)) + case Literal(_) => f + }) ensuring(isSimplified(_)) + + def isSimplified(f: Formula): Boolean = f match { + case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs) + case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs) + case Implies(_,_) => false + case Not(f) => isSimplified(f) + case Literal(_) => true + } + + def nnf(formula: Formula): Formula = (formula match { + case And(lhs, rhs) => And(nnf(lhs), nnf(rhs)) + case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs)) + case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs)) + case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs))) + case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs))) + case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs))) + case Not(Not(f)) => nnf(f) + case Not(Literal(_)) => formula + case Literal(_) => formula + }) ensuring(isNNF(_)) + + def isNNF(f: Formula): Boolean = f match { + case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs) + case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs) + case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs) + case Not(Literal(_)) => true + case Not(_) => false + case Literal(_) => true + } + + def vars(f: Formula): Set[Int] = { + require(isNNF(f)) + f match { + case And(lhs, rhs) => vars(lhs) ++ vars(rhs) + case Or(lhs, rhs) => vars(lhs) ++ vars(rhs) + case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs) + case Not(Literal(i)) => Set[Int](i) + case Literal(i) => Set[Int](i) + } + } + + def fv(f : Formula) = { vars(nnf(f)) } + + // @induct + // def wrongCommutative(f: Formula) : Boolean = { + // nnf(simplify(f)) == simplify(nnf(f)) + // } holds + + @induct + def simplifyBreaksNNF(f: Formula) : Boolean = { + require(isNNF(f)) + isNNF(simplify(f)) + } holds + + @induct + def nnfIsStable(f: Formula) : Boolean = { + require(isNNF(f)) + nnf(f) == f + } holds + + @induct + def simplifyIsStable(f: Formula) : Boolean = { + require(isSimplified(f)) + simplify(f) == f + } holds +} diff --git a/src/test/resources/regression/verification/purescala/valid/README b/src/test/resources/regression/verification/purescala/valid/README new file mode 100644 index 0000000000000000000000000000000000000000..2bb01d5fdbd6b59970c0c84f2c10db1ead6097a2 --- /dev/null +++ b/src/test/resources/regression/verification/purescala/valid/README @@ -0,0 +1,2 @@ +This particular directory contains PureScala programs that can be entirely +proved correct by Leon. diff --git a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala new file mode 100644 index 0000000000000000000000000000000000000000..bc2de6ba96ee699736d4558932b752eea9ebba9f --- /dev/null +++ b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala @@ -0,0 +1,117 @@ +import scala.collection.immutable.Set +import leon.Annotations._ +import leon.Utils._ + +object RedBlackTree { + sealed abstract class Color + case class Red() extends Color + case class Black() extends Color + + sealed abstract class Tree + case class Empty() extends Tree + case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree + + sealed abstract class OptionInt + case class Some(v : Int) extends OptionInt + case class None() extends OptionInt + + def content(t: Tree) : Set[Int] = t match { + case Empty() => Set.empty + case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r) + } + + def size(t: Tree) : Int = (t match { + case Empty() => 0 + case Node(_, l, v, r) => size(l) + 1 + size(r) + }) ensuring(_ >= 0) + + /* We consider leaves to be black by definition */ + def isBlack(t: Tree) : Boolean = t match { + case Empty() => true + case Node(Black(),_,_,_) => true + case _ => false + } + + def redNodesHaveBlackChildren(t: Tree) : Boolean = t match { + case Empty() => true + case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r) + case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r) + } + + def redDescHaveBlackChildren(t: Tree) : Boolean = t match { + case Empty() => true + case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r) + } + + def blackBalanced(t : Tree) : Boolean = t match { + case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r) + case Empty() => true + } + + def blackHeight(t : Tree) : Int = t match { + case Empty() => 1 + case Node(Black(), l, _, _) => blackHeight(l) + 1 + case Node(Red(), l, _, _) => blackHeight(l) + } + + // <<insert element x into the tree t>> + def ins(x: Int, t: Tree): Tree = { + require(redNodesHaveBlackChildren(t) && blackBalanced(t)) + t match { + case Empty() => Node(Red(),Empty(),x,Empty()) + case Node(c,a,y,b) => + if (x < y) balance(c, ins(x, a), y, b) + else if (x == y) Node(c,a,y,b) + else balance(c,a,y,ins(x, b)) + } + } ensuring (res => content(res) == content(t) ++ Set(x) + && size(t) <= size(res) && size(res) <= size(t) + 1 + && redDescHaveBlackChildren(res) + && blackBalanced(res)) + + def makeBlack(n: Tree): Tree = { + require(redDescHaveBlackChildren(n) && blackBalanced(n)) + n match { + case Node(Red(),l,v,r) => Node(Black(),l,v,r) + case _ => n + } + } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res)) + + def add(x: Int, t: Tree): Tree = { + require(redNodesHaveBlackChildren(t) && blackBalanced(t)) + makeBlack(ins(x, t)) + } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res)) + + def buggyAdd(x: Int, t: Tree): Tree = { + require(redNodesHaveBlackChildren(t)) + ins(x, t) + } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res)) + + def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = { + Node(c,a,x,b) match { + case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) => + Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d)) + case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) => + Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d)) + case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) => + Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d)) + case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) => + Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d)) + case Node(c,a,xV,b) => Node(c,a,xV,b) + } + } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res)) + + def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = { + Node(c,a,x,b) match { + case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) => + Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d)) + case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) => + Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d)) + case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) => + Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d)) + case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) => + Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d)) + // case Node(c,a,xV,b) => Node(c,a,xV,b) + } + } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res)) +} diff --git a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala new file mode 100644 index 0000000000000000000000000000000000000000..2c137fd4ad6b9d411f7e14b4ada6b834234c9e9e --- /dev/null +++ b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala @@ -0,0 +1,48 @@ +import scala.collection.immutable.Set +import leon.Utils._ +import leon.Annotations._ + +object SearchLinkedList { + sealed abstract class List + case class Cons(head : Int, tail : List) extends List + case class Nil() extends List + + def size(list : List) : Int = (list match { + case Nil() => 0 + case Cons(_, xs) => 1 + size(xs) + }) ensuring(_ >= 0) + + def contains(list : List, elem : Int) : Boolean = (list match { + case Nil() => false + case Cons(x, xs) => x == elem || contains(xs, elem) + }) + + def firstZero(list : List) : Int = (list match { + case Nil() => 0 + case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1 + }) ensuring (res => + res >= 0 && (if (contains(list, 0)) { + firstZeroAtPos(list, res) + } else { + res == size(list) + })) + + def firstZeroAtPos(list : List, pos : Int) : Boolean = { + list match { + case Nil() => false + case Cons(x, xs) => if (pos == 0) x == 0 else x != 0 && firstZeroAtPos(xs, pos - 1) + } + } + + def goal(list : List, i : Int) : Boolean = { + if(firstZero(list) == i) { + if(contains(list, 0)) { + firstZeroAtPos(list, i) + } else { + i == size(list) + } + } else { + true + } + } holds +} diff --git a/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala new file mode 100644 index 0000000000000000000000000000000000000000..0aa4ce7060a391d34dd047338fcd1f638054843f --- /dev/null +++ b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala @@ -0,0 +1,46 @@ +import leon.Utils._ +import leon.Annotations._ + +object SumAndMax { + sealed abstract class List + case class Cons(head : Int, tail : List) extends List + case class Nil() extends List + + def max(list : List) : Int = { + require(list != Nil()) + list match { + case Cons(x, Nil()) => x + case Cons(x, xs) => { + val m2 = max(xs) + if(m2 > x) m2 else x + } + } + } + + def sum(list : List) : Int = list match { + case Nil() => 0 + case Cons(x, xs) => x + sum(xs) + } + + def size(list : List) : Int = (list match { + case Nil() => 0 + case Cons(_, xs) => 1 + size(xs) + }) ensuring(_ >= 0) + + def allPos(list : List) : Boolean = list match { + case Nil() => true + case Cons(x, xs) => x >= 0 && allPos(xs) + } + + def prop0(list : List) : Boolean = { + require(list != Nil()) + !allPos(list) || max(list) >= 0 + } holds + + @induct + def property(list : List) : Boolean = { + // This precondition was given in the problem but isn't actually useful :D + // require(allPos(list)) + sum(list) <= size(list) * (if(list == Nil()) 0 else max(list)) + } holds +} diff --git a/src/test/scala/leon/test/Test.scala b/src/test/scala/leon/test/Test.scala new file mode 100644 index 0000000000000000000000000000000000000000..ed3549395b971f0e12fbdb8a8c7656526fe936e8 --- /dev/null +++ b/src/test/scala/leon/test/Test.scala @@ -0,0 +1,9 @@ +package leon.test + +import org.scalatest.FunSuite + +class Test extends FunSuite { + test("Tests work.") { + assert(true) + } +} diff --git a/src/test/scala/leon/test/ValidPrograms.scala b/src/test/scala/leon/test/ValidPrograms.scala new file mode 100644 index 0000000000000000000000000000000000000000..82af678129f6f01bd21d6c588b0daea70f4b9545 --- /dev/null +++ b/src/test/scala/leon/test/ValidPrograms.scala @@ -0,0 +1,46 @@ +package leon +package test + +import org.scalatest.FunSuite + +import java.io.File + +class ValidPrograms extends FunSuite { + def runBasicLeonOnFile(filename : String) : Unit = { + val file = new File(filename) + + assert(file.exists && file.isFile && file.canRead, + "Benchmark [%s] is not a readable file".format(filename)) + + val ctx = LeonContext( + Settings( + synthesis = false, + xlang = false, + analyze = true + ), + new SilentReporter + ) + + val pipeline = Main.computePipeline(ctx.settings) + pipeline.run(ctx)("--timeout=2" :: file.getPath :: Nil) + } + + def mkTest(filename : String) = { + test("Valid PureScala program: [%s]".format(filename)) { + runBasicLeonOnFile(filename) + assert(true) + } + } + + test("List files") { + import scala.collection.JavaConversions._ + + val ress = this.getClass.getClassLoader.getResources("/regression/verification/purescala/valid/") + + for(res <- ress) { + println(res) + } + } + + mkTest("/home/psuter/Test.scala") +}