Merge pull request #2 from Sumith1896/objAlloc

alloc instrumentation phase

library/instrumentation/package.scala

@@ -21,4 +21,7 @@ package object instrumentation {
 
   @library
   def tpr: BigInt = 0
+
+  @library
+  def alloc: BigInt = 0
 }

src/main/scala/leon/transformations/AllocInstPhase.scala

@@ -0,0 +1,60 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package transformations
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Extractors._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
+import leon.utils._
+import invariant.util.Util._
+
+object allocCostModel {
+  def costOf(e: Expr): Int = e match {
+  	case CaseClass(_, _) => 1
+    case t: Terminal => 0
+    case _ => 0
+  }
+
+  def costOfExpr(e: Expr) = InfiniteIntegerLiteral(costOf(e))
+}
+
+class AllocInstrumenter(p: Program, si: SerialInstrumenter) extends Instrumenter(p, si) {
+  import allocCostModel._
+
+  def inst = Alloc
+
+  def functionsToInstrument(): Map[FunDef, List[Instrumentation]] = {
+    //find all functions transitively called from rootFuncs (here ignore functions called via pre/post conditions)
+    val instFunSet = getRootFuncs().foldLeft(Set[FunDef]())((acc, fd) => acc ++ cg.transitiveCallees(fd)).filter(_.hasBody) // ignore uninterpreted functions
+    //println("Root funs: "+getRootFuncs().map(_.id).mkString(",")+" All funcs: "+ instFunSet.map(_.id).mkString(","))
+    instFunSet.map(x => (x, List(Alloc))).toMap
+  }
+
+  def additionalfunctionsToAdd() = Seq()
+
+  def instrumentMatchCase(me: MatchExpr, mc: MatchCase,
+    caseExprCost: Expr, scrutineeCost: Expr): Expr = {
+    val costMatch = costOfExpr(me)
+    def totalCostOfMatchPatterns(me: MatchExpr, mc: MatchCase): BigInt = 0
+    Plus(costMatch, Plus(caseExprCost, scrutineeCost))
+  }
+
+  def instrument(e: Expr, subInsts: Seq[Expr], funInvResVar: Option[Variable] = None)
+  	(implicit fd: FunDef, letIdMap: Map[Identifier,Identifier]): Expr = e match {
+    case t: Terminal => costOfExpr(t)
+    case _ =>
+      subInsts.foldLeft(costOfExpr(e) : Expr)(
+        (acc: Expr, subeObjAlloc: Expr) => Plus(subeObjAlloc, acc))
+  }
+
+  def instrumentIfThenElseExpr(e: IfExpr, condInst: Option[Expr],
+      thenInst: Option[Expr], elzeInst: Option[Expr]): (Expr, Expr) = {    
+  	val costIf = costOfExpr(e)
+    (Plus(costIf, Plus(condInst.get, thenInst.get)),
+      Plus(costIf, Plus(condInst.get, elzeInst.get)))
+  }
+}

src/main/scala/leon/transformations/InstrumentationUtil.scala

@@ -54,11 +54,16 @@ object Stack extends Instrumentation {
   override val getType = IntegerType
   override val name = "stack"
 }
+
+object Alloc extends Instrumentation {
+  override val getType = IntegerType
+  override val name = "alloc"
+}
 //add more instrumentation variables
 
 object InstUtil {
 
-  val InstTypes = Seq(Time, Depth, Rec, TPR, Stack)
+  val InstTypes = Seq(Time, Depth, Rec, TPR, Stack, Alloc)
 
   val maxFun = {
     val xid = FreshIdentifier("x", IntegerType)

src/main/scala/leon/transformations/SerialInstrumentationPhase.scala

@@ -46,7 +46,8 @@ class SerialInstrumenter(program: Program,
       Depth -> new DepthInstrumenter(program, this),
       Rec -> new RecursionCountInstrumenter(program, this),
       Stack -> new StackSpaceInstrumenter(program, this),
-      TPR -> new TPRInstrumenter(program, this))
+      TPR -> new TPRInstrumenter(program, this),
+      Alloc -> new AllocInstrumenter(program, this))
 
   // a map from functions to the list of instrumentations to be performed for the function
   val funcInsts = {

src/main/scala/leon/transformations/TimeStepsPhase.scala

@@ -104,4 +104,4 @@ class TimeInstrumenter(p: Program, si: SerialInstrumenter) extends Instrumenter(
     (Plus(costIf, Plus(condInst.get, thenInst.get)),
       Plus(costIf, Plus(condInst.get, elzeInst.get)))
   }
-}
+}

testcases/orb-testcases/objAlloc/AmortizedQueue.scala

@@ -0,0 +1,90 @@
+package orb
+
+import leon._
+import invariant._
+import instrumentation._
+
+object AmortizedQueue {
+  sealed abstract class List {
+    val size: BigInt = this match {
+      case Nil()       => 0
+      case Cons(_, xs) => 1 + xs.size
+    }
+  }
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  def length(l: List): BigInt = {
+    l match {
+      case Nil()       => BigInt(0)
+      case Cons(_, xs) => 1 + length(xs)
+    }
+  } ensuring(res => res >= 0 && alloc <= ?)
+
+  def concat(l1: List, l2: List): List = (l1 match {
+    case Nil()       => l2
+    case Cons(x, xs) => Cons(x, concat(xs, l2))
+
+  }) ensuring (res => res.size == l1.size + l2.size && alloc <= ? * l1.size + ?)
+
+  def reverseRec(l1: List, l2: List): List = (l1 match {
+    case Nil()       => l2
+    case Cons(x, xs) => reverseRec(xs, Cons(x, l2))
+  }) ensuring (res => l1.size + l2.size == res.size && alloc <= ? * l1.size + ?)
+
+  def listRev(l: List): List = {
+    reverseRec(l, Nil())
+  } ensuring (res => l.size == res.size && alloc <= ? * l.size + ?)
+
+  def removeLast(l: List): List = {
+    require(l != Nil())
+    l match {
+      case Cons(x, Nil()) => Nil()
+      case Cons(x, xs)    => Cons(x, removeLast(xs))
+      case _              => Nil()
+    }
+  } ensuring (res => res.size <= l.size && tmpl((a, b) => alloc <= a * l.size + b))
+
+  case class Queue(front: List, rear: List) {
+    def qsize: BigInt = front.size + rear.size
+
+    def asList: List = concat(front, listRev(rear))
+
+    def isAmortized: Boolean = length(front) >= length(rear)
+
+    def isEmpty: Boolean = this match {
+      case Queue(Nil(), Nil()) => true
+      case _                   => false
+    }
+
+    def amortizedQueue(front: List, rear: List): Queue = {
+      if (length(rear) <= length(front))
+        Queue(front, rear)
+      else
+        Queue(concat(front, listRev(rear)), Nil())
+    }
+
+    def enqueue(elem: BigInt): Queue = ({
+      amortizedQueue(front, Cons(elem, rear))
+    }) ensuring (_ => alloc <= ? * qsize + ?)
+
+    def dequeue: Queue = {
+      require(isAmortized && !isEmpty)
+      front match {
+        case Cons(f, fs) => amortizedQueue(fs, rear)
+        case _           => Queue(Nil(), Nil())
+      }
+    } ensuring (_ => alloc <= ? * qsize + ?)
+
+    def head: BigInt = {
+      require(isAmortized && !isEmpty)
+      front match {
+        case Cons(f, _) => f
+      }
+    }
+
+    def reverse: Queue = { // this lets the queue perform deque operation (but they no longer have efficient constant alloc amortized bounds)
+      amortizedQueue(rear, front)
+    }
+  }
+}

testcases/orb-testcases/objAlloc/BinaryTrie.scala

@@ -0,0 +1,119 @@
+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 (_ => alloc <= ? * 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 (_ => alloc <= ? * listSize(inp) + ?)
+
+  def create(inp: IList): Tree = {
+    insert(inp, Leaf())
+  } ensuring (res => true && tmpl((a, c) => alloc <= a * listSize(inp) + c))
+
+  def delete(inp: IList, t: Tree): Tree = {
+    t match {
+        case Leaf() => {
+          inp match {
+            case Nil() => Leaf()
+            case Cons(x ,xs) => {
+              //the input is not in the tree, so do nothing
+              Leaf()
+            }
+          }
+        }
+        case Node(v, l, r) => {
+          inp match {
+            case Nil() => {
+              //the tree has extensions of the input list so do nothing
+              t
+            }
+            case Cons(x, Nil()) => {
+              //if "l" and "r" are nil, remove the node
+              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 (_ => alloc <= ? * listSize(inp) + ?)
+}