Adding testcases for leon-orb web integeration

src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala

@@ -134,7 +134,7 @@ object InferInvariantsPhase extends LeonPhase[Program, InferenceReport] {
       enumerationRelation = LessEquals, modularlyAnalyze, targettedUnroll, autoInference,
       dumpStats, tightBounds, withmult, usereals, inferTemp, useCegis, timeout, maxCegisBound, statsSuff)
     val report = (new InferenceEngine(inferctx)).run()
-    println("Final Program: \n" +PrettyPrinter.apply(report.finalProgramWoInstrumentation))
+    //println("Final Program: \n" +PrettyPrinter.apply(report.finalProgramWoInstrumentation))
     report
   }
 

src/main/scala/leon/invariant/engine/InferenceReport.scala

@@ -20,13 +20,13 @@ class InferenceCondition(val invariant: Option[Expr], funDef: FunDef)
   extends VC(BooleanLiteral(true), funDef, null) {
 
   var time: Option[Double] = None
+  lazy val prettyInv = invariant.map(inv =>
+    simplifyArithmetic(InstUtil.replaceInstruVars(Util.multToTimes(inv), fd)))
 
-  def status: String = invariant match {
+  def status: String = prettyInv match {
     case None => "unknown"
-    case Some(inv) => {
-      val prettyInv = simplifyArithmetic(InstUtil.replaceInstruVars(Util.multToTimes(inv), fd))
-      PrettyPrinter(prettyInv)
-    }
+    case Some(inv) =>
+      PrettyPrinter(inv)
   }
 }
 
@@ -97,14 +97,13 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]])(implicit ctx: InferenceContex
         val uninstFdOpt =
           if (uninstFunName.isEmpty) None
           else Util.functionByName(uninstFunName, ctx.uninstrumentedProgram)
-        if (uninstFdOpt.isDefined) {          
+        if (uninstFdOpt.isDefined) {
           acc + (fd -> uninstFdOpt.get)
-        }
-        else acc
+        } else acc
     }
     val funToPost = conditions.collect {
       case cd if cd.invariant.isDefined && funToUninstFun.contains(cd.fd) =>
-        funToUninstFun(cd.fd) -> cd.invariant.get
+        funToUninstFun(cd.fd) -> cd.prettyInv.get
     }.toMap
     //println("Function to template: " + funToTmpl.map { case (k, v) => s"${k.id.name} --> $v" }.mkString("\n"))
     Util.assignTemplateAndCojoinPost(Map(), ctx.uninstrumentedProgram, funToPost, uniqueIdDisplay = false)

src/test/scala/leon/regression/orb/OrbRegressionSuite.scala

@@ -24,7 +24,7 @@ class OrbRegressionSuite extends LeonRegressionSuite {
     val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
       new leon.utils.PreprocessingPhase
     val program = beginPipe.run(ctx)(f.getAbsolutePath :: Nil)
-    val processPipe = InstrumentationPhase andThen InferInvariantsPhase
+    val processPipe = InferInvariantsPhase
     val report = processPipe.run(ctx)(program)
     val fails = report.conditions.filterNot(_.invariant.isDefined)
     if (!fails.isEmpty)

testcases/web/invariant/01_Binary_Trie.scala

+import leon.invariant._
+import leon.instrumentation._
+
+object BinaryTrie {
+  sealed abstract class Tree
+  case class Leaf() extends Tree
+  case class Node(nvalue: BigInt, left: Tree, right: Tree) extends Tree
+
+  sealed abstract class IList
+  case class Cons(head: BigInt, tail: IList) extends IList
+  case class Nil() extends IList
+
+  def listSize(l: IList): BigInt = (l match {
+    case Nil() => 0
+    case Cons(x, xs) => 1 + listSize(xs)
+  })
+
+  def height(t: Tree): BigInt = {
+    t match {
+      case Leaf() => 0
+      case Node(x, l, r) => {
+        val hl = height(l)
+        val hr = height(r)
+        if (hl > hr) hl + 1 else hr + 1
+      }
+    }
+  }
+
+  def find(inp: IList, t: Tree): Tree = {
+    inp match {
+      case Nil() => t
+      case Cons(x, Nil()) => t
+      case Cons(x, xs @ Cons(y, _)) => {
+        t match {
+          case Leaf() => t
+          case Node(v, l, r) => {
+            if (y > 0) find(xs, l) else find(xs, r)
+          }
+        }
+      }
+      case _ => t
+    }
+  } ensuring (_ => time <= ? * listSize(inp) + ?)
+
+  def insert(inp: IList, t: Tree): Tree = {
+    t match {
+      case Leaf() => {
+        inp match {
+          case Nil() => t
+          case Cons(x, xs) => {
+            val newch = insert(xs, Leaf())
+            newch match {
+              case Leaf() => Node(x, Leaf(), Leaf())
+              case Node(y, _, _) => if (y > 0) Node(x, newch, Leaf()) else Node(y, Leaf(), newch)
+            }
+          }
+        }
+
+      }
+      case Node(v, l, r) => {
+        inp match {
+          case Nil() => t
+          case Cons(x, Nil()) => t
+          case Cons(x, xs @ Cons(y, _)) => {
+            val ch = if (y > 0) l else r
+            if (y > 0)
+              Node(v, insert(xs, ch), r)
+            else
+              Node(v, l, insert(xs, ch))
+          }
+          case _ => t
+        }
+      }
+    }
+  } ensuring (_ => time <= ? * listSize(inp) + ?)
+
+  def create(inp: IList): Tree = {
+    insert(inp, Leaf())
+  } ensuring (res => time <= ? * listSize(inp) + ?)
+
+  def delete(inp: IList, t: Tree): Tree = {
+    t match {
+        case Leaf() => {
+          inp match {
+            case Nil() => Leaf()
+            case Cons(x ,xs) => {
+              Leaf()
+            }
+          }
+        }
+        case Node(v, l, r) => {
+          inp match {
+            case Nil() => {
+              t
+            }
+            case Cons(x, Nil()) => {
+              if(l == Leaf() && r == Leaf()) Leaf()
+              else t
+            }
+            case Cons(x ,xs@Cons(y, _)) => {
+              val ch = if(y > 0) l else r
+              val newch = delete(xs, ch)
+              if(newch == Leaf() && ((y > 0 && r == Leaf()) || (y <= 0 && l == Leaf()))) Leaf()
+              else {
+                if(y > 0)
+        		  Node(v, newch, r)
+        	    else
+        	      Node(v, l, newch)
+              }
+            }
+            case _ => t
+        }
+      }
+    }
+  } ensuring (_ => time <= ? * listSize(inp) + ?)
+}
\ No newline at end of file

testcases/web/invariant/02_Binomial_Heap.scala

+import leon.invariant._
+import leon.instrumentation._
+
+object BinomialHeap {
+  case class TreeNode(rank: BigInt, elem: Element, children: BinomialHeap)
+  case class Element(n: BigInt)
+
+  sealed abstract class BinomialHeap
+  case class ConsHeap(head: TreeNode, tail: BinomialHeap) extends BinomialHeap
+  case class NilHeap() extends BinomialHeap
+
+  sealed abstract class List
+  case class NodeL(head: BinomialHeap, tail: List) extends List
+  case class NilL() extends List
+
+  sealed abstract class OptionalTree
+  case class Some(t : TreeNode) extends OptionalTree
+  case class None() extends OptionalTree
+ 
+  private def leq(a: Element, b: Element) : Boolean = {
+    a match {
+      case Element(a1) => {
+        b match {
+          case Element(a2) => {
+            if(a1 <= a2) true
+            else false
+          }
+        }
+      }
+    }
+  }
+
+  def isEmpty(t: BinomialHeap) = t match {
+    case ConsHeap(_,_) => false
+    case _ => true
+  }
+
+  def rank(t: TreeNode) : BigInt = t.rank 
+
+  def root(t: TreeNode) : Element = t.elem 
+
+  def link(t1: TreeNode, t2: TreeNode): TreeNode = {
+    if (leq(t1.elem, t2.elem)) {
+      TreeNode(t1.rank + 1, t1.elem, ConsHeap(t2, t1.children))
+    } else {
+      TreeNode(t1.rank + 1, t2.elem, ConsHeap(t1, t2.children))
+    }
+  }
+
+  def treeNum(h: BinomialHeap) : BigInt = {
+    h match {
+      case ConsHeap(head, tail) =>  1 + treeNum(tail)
+      case _ => 0
+    }
+  }
+  
+  def insTree(t: TreeNode, h: BinomialHeap) : BinomialHeap = {
+    h match {
+      case ConsHeap(head, tail) =>  {
+        if (rank(t) < rank(head)) {
+          ConsHeap(t, h)
+        } else if (rank(t) > rank(head)) {
+          ConsHeap(head, insTree(t,tail))
+        } else {
+          insTree(link(t,head), tail)
+        }
+      }
+      case _ => ConsHeap(t, NilHeap())
+    }
+  } ensuring(_ => time <= ? * treeNum(h) + ?)
+
+  def merge(h1: BinomialHeap, h2: BinomialHeap): BinomialHeap = {
+    h1 match {
+      case ConsHeap(head1, tail1) => {
+        h2 match {
+          case ConsHeap(head2, tail2) => {
+            if (rank(head1) < rank(head2)) {
+              ConsHeap(head1, merge(tail1, h2))
+            } else if (rank(head2) < rank(head1)) {
+              ConsHeap(head2, merge(h1, tail2))
+            } else {
+              mergeWithCarry(link(head1, head2), tail1, tail2)
+            }
+          }
+          case _ => h1
+        }
+      }
+      case _ => h2
+    }
+  } ensuring(_ => time <= ? * treeNum(h1) + ? * treeNum(h2) + ?)
+
+  def mergeWithCarry(t: TreeNode, h1: BinomialHeap, h2: BinomialHeap): BinomialHeap = {
+    h1 match {
+      case ConsHeap(head1, tail1) => {
+        h2 match {
+          case ConsHeap(head2, tail2) => {
+            if (rank(head1) < rank(head2)) {
+              if (rank(t) < rank(head1))
+                ConsHeap(t, ConsHeap(head1, merge(tail1, h2)))
+              else
+                mergeWithCarry(link(t, head1), tail1, h2)
+            } else if (rank(head2) < rank(head1)) {
+              if (rank(t) < rank(head2))
+                ConsHeap(t, ConsHeap(head2, merge(h1, tail2)))
+              else
+                mergeWithCarry(link(t, head2), h1, tail2)
+            } else {
+              ConsHeap(t, mergeWithCarry(link(head1, head2), tail1, tail2))
+            }
+          }
+          case _ => {
+            insTree(t, h1)
+          }
+        }
+      }
+      case _ => insTree(t, h2)
+    }
+  } ensuring (_ => time <= ? * treeNum(h1) + ? * treeNum(h2) + ?)
+
+  def removeMinTree(h: BinomialHeap): (OptionalTree, BinomialHeap) = {
+    h match {
+      case ConsHeap(head, NilHeap()) => (Some(head), NilHeap())
+      case ConsHeap(head1, tail1) => {
+        val (opthead2, tail2) = removeMinTree(tail1)
+        opthead2 match {
+          case Some(head2) =>
+            if (leq(root(head1), root(head2))) {
+              (Some(head1), tail1)
+            } else {
+              (Some(head2), ConsHeap(head1, tail2))
+            }
+          case _ => (Some(head1), tail1)
+        }
+      }
+      case _ => (None(), NilHeap())
+    }
+  } ensuring (res => treeNum(res._2) <= treeNum(h) && time <= ? * treeNum(h) + ?)
+
+  def minTreeChildren(h: BinomialHeap) : BigInt = {
+    val (min, _) = removeMinTree(h)
+    min match {
+      case Some(TreeNode(_,_,ch)) => treeNum(ch)
+      case _ => 0
+	  }
+  }
+
+  def deleteMin(h: BinomialHeap) : BinomialHeap = {
+	  val (min, ts2) = removeMinTree(h)
+	  min match {
+		case Some(TreeNode(_,_,ts1)) => merge(ts1, ts2)
+		case _ => h
+	  }
+  } ensuring(_ => time <= ? * minTreeChildren(h) + ? * treeNum(h) + ?)
+}

testcases/web/invariant/03_List_Concat.scala

+import leon.invariant._
+import leon.instrumentation._
+
+object ConcatVariations {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil() => 0
+    case Cons(_, t) => 1 + size(t)
+  })
+
+  def genL(n: BigInt): List = {
+    require(n >= 0)
+    if (n == 0) Nil()
+    else
+      Cons(n, genL(n - 1))
+  } ensuring (res => size(res) == n && time <= ? *n + ?)
+
+  def append(l1: List, l2: List): List = (l1 match {
+    case Nil() => l2
+    case Cons(x, xs) => Cons(x, append(xs, l2))
+
+  }) ensuring (res =>  size(l1) + size(l2) == size(res) && time <= ? *size(l1) + ?)
+
+  def f_good(m: BigInt, n: BigInt): List = {
+    require(0 <= m && 0 <= n)
+    if (m == 0) Nil()
+    else append(genL(n), f_good(m - 1, n))
+
+  } ensuring(res => size(res) == n*m && time <= ? *(n*m) + ? *n + ? *m + ?)
+
+  def f_worst(m: BigInt, n: BigInt): List = {
+    require(0 <= m && 0 <= n)
+
+    if (m == 0) Nil()
+    else append(f_worst(m - 1, n), genL(n))
+
+  } ensuring(res => size(res) == n*m && time <= ? *((n*m)*m)+ ? *(n*m)+ ? *n+ ? *m+ ?)
+}

testcases/web/invariant/04_Red_Black_Tree.scala

+import leon.invariant._
+import leon.instrumentation._
+import scala.collection.immutable.Set
+
+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: BigInt, right: Tree) extends Tree
+
+  def twopower(x: BigInt) : BigInt = {
+    require(x >= 0)
+    if(x < 1) 1
+    else
+      2* twopower(x - 1)
+  }
+
+  def size(t: Tree): BigInt = {
+    require(blackBalanced(t))
+    (t match {
+      case Empty() => BigInt(0)
+      case Node(_, l, v, r) => size(l) + 1 + size(r)
+    })
+  } ensuring (res => twopower(blackHeight(t)) <= ? *res + ?)
+
+  def blackHeight(t : Tree) : BigInt = {
+   t match {
+    case Node(Black(), l, _, _) => blackHeight(l) + 1
+    case Node(Red(), l, _, _) => blackHeight(l)
+    case _ => 0
+   	}
+  }
+
+  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)
+    case _ => false
+  }
+
+  def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+    case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+    case _ => true
+  }
+
+  def blackBalanced(t : Tree) : Boolean = t match {
+    case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+    case _ => true
+  }
+
+  def ins(x: BigInt, 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) {
+        	val t1 = ins(x, a)
+        	balance(c, t1, y, b)
+        }
+        else if (x == y){
+        	Node(c,a,y,b)
+        }
+        else{
+          val t1 = ins(x, b)
+          balance(c,a,y,t1)
+        }
+    }
+  } ensuring(res => time <= ? *blackHeight(t) + ?)
+
+  def makeBlack(n: Tree): Tree = {
+    n match {
+      case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+      case _ => n
+    }
+  }
+
+  def add(x: BigInt, t: Tree): Tree = {
+    require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+    val t1 =  ins(x, t)
+    makeBlack(t1)
+
+  } ensuring(res => time <= ? *blackHeight(t) + ?)
+
+  def balance(co: Color, l: Tree, x: BigInt, r: Tree): Tree = {
+    Node(co,l,x,r)
+     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(co,l,x,r)
+    }
+  }
+}

testcases/web/invariant/05_Leftist_Heap.scala

+import leon.invariant._
+import leon.instrumentation._
+import leon.annotation._
+
+object LeftistHeap {
+  sealed abstract class Heap
+  case class Leaf() extends Heap
+  case class Node(rk : BigInt, value: BigInt, left: Heap, right: Heap) extends Heap
+
+  private def rightHeight(h: Heap) : BigInt = h match {
+    case Leaf() => 0
+    case Node(_,_,_,r) => rightHeight(r) + 1
+  }
+
+  private def rank(h: Heap) : BigInt = h match {
+    case Leaf() => 0
+    case Node(rk,_,_,_) => rk
+  }
+
+  private def hasLeftistProperty(h: Heap) : Boolean = (h match {
+    case Leaf() => true
+    case Node(_,_,l,r) => hasLeftistProperty(l) && hasLeftistProperty(r) && rightHeight(l) >= rightHeight(r) && (rank(h) == rightHeight(h))
+  })
+
+  @monotonic
+  def twopower(x: BigInt) : BigInt = {
+    require(x >= 0)
+    if(x < 1) 1
+    else
+      2* twopower(x - 1)
+  }
+
+  def size(t: Heap): BigInt = {
+    require(hasLeftistProperty(t))
+    (t match {
+      case Leaf() => BigInt(0)
+      case Node(_,v, l, r) => size(l) + 1 + size(r)
+    })
+  } ensuring (res => twopower(rightHeight(t)) <= ? *res + ?)
+
+  def leftRightHeight(h: Heap) : BigInt = {h match {
+    case Leaf() => 0
+    case Node(_,_,l,r) => rightHeight(l)
+  }}
+
+  def removeMax(h: Heap) : Heap = {
+    require(hasLeftistProperty(h))
+    h match {
+      case Node(_,_,l,r) => merge(l, r)
+      case l @ Leaf() => l
+    }
+  } ensuring(res => time <= ? *leftRightHeight(h) + ?)
+
+  private def merge(h1: Heap, h2: Heap) : Heap = {
+    require(hasLeftistProperty(h1) && hasLeftistProperty(h2))
+    h1 match {
+      case Leaf() => h2
+      case Node(_, v1, l1, r1) => h2 match {
+        case Leaf() => h1
+        case Node(_, v2, l2, r2) =>
+          if(v1 > v2)
+            makeT(v1, l1, merge(r1, h2))
+          else
+            makeT(v2, l2, merge(h1, r2))
+      }
+    }
+  } ensuring(res => time <= ? *rightHeight(h1) + ? *rightHeight(h2) + ?)
+
+  private def makeT(value: BigInt, left: Heap, right: Heap) : Heap = {
+    if(rank(left) >= rank(right))
+      Node(rank(right) + 1, value, left, right)
+    else
+      Node(rank(left) + 1, value, right, left)
+  }
+
+  def insert(element: BigInt, heap: Heap) : Heap = {
+   require(hasLeftistProperty(heap))
+
+    merge(Node(1, element, Leaf(), Leaf()), heap)
+
+  } ensuring(res => time <= ? *rightHeight(heap) + ?)
+}

testcases/web/invariant/06_String_Buffer.scala

+import leon.invariant._
+import leon.instrumentation._
+
+object StringBuffer {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil() => 0
+    case Cons(_, t) => 1 + size(t)
+  })
+
+  sealed abstract class StringBuffer
+  case class Chunk(str: List, next: StringBuffer) extends StringBuffer
+  case class Empty() extends StringBuffer
+
+  def length(sb: StringBuffer) : BigInt = sb match {
+    case Chunk(_, next) => 1 + length(next)
+    case _ => 0
+  }
+
+  def sizeBound(sb: StringBuffer, k: BigInt) : Boolean ={
+    sb match {
+      case Chunk(str, next) => size(str) <= k && sizeBound(next, k)
+      case _ => 0 <= k
+    }
+  }
+
+  def Equals(str1: List, str2: List, s1: StringBuffer, s2: StringBuffer, k: BigInt) : Boolean = {
+    require(sizeBound(s1, k) && sizeBound(s2, k) && size(str1) <= k && size(str2) <= k && k >= 0)
+
+    (str1, str2) match {
+      case (Cons(h1,t1), Cons(h2,t2)) => {
+
+        if(h1 != h2) false
+        else Equals(t1,t2, s1,s2, k)
+      }
+      case (Cons(_,_), Nil()) => {
+        s2 match {
+          case Chunk(str, next) => Equals(str1, str, s1, next, k)
+          case Empty() => false
+        }
+      }
+      case (Nil(), Cons(_,_)) => {
+        s1 match {
+          case Chunk(str, next) => Equals(str, str2, next, s2, k)
+          case Empty() => false
+        }
+      }
+      case _ =>{
+        (s1,s2) match {
+          case (Chunk(nstr1, next1),Chunk(nstr2, next2)) => Equals(nstr1, nstr2, next1, next2, k)
+          case (Empty(),Chunk(nstr2, next2)) => Equals(str1, nstr2, s1, next2, k)
+          case (Chunk(nstr1, next1), Empty()) => Equals(nstr1, str2, next1, s2, k)
+          case _ => true
+        }
+      }
+    }
+  } ensuring(res => true && tmpl((a,b,c,d,e) => time <= a*((k+1)*(length(s1) + length(s2))) + b*size(str1) + e))
+
+  def max(x: BigInt, y: BigInt) : BigInt = if(x >= y) x else y
+}