Adding some features needed for leon web

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

@@ -45,18 +45,18 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
     ctx.abort = false
   }
 
-  def runWithTimeout() = {
+  def runWithTimeout(progressCallback: Option[InferenceCondition => Unit] = None) = {
     ctx.totalTimeout match {
       case Some(t) => // timeout in secs
         ti.interruptAfter(t * 1000) {
-          run
+          run(progressCallback)
         }
       case None =>
-        run
+        run(progressCallback)
     }
   }
 
-  private def run(): InferenceReport = {
+  private def run(progressCallback: Option[InferenceCondition => Unit] = None): InferenceReport = {
     val reporter = ctx.reporter
     val program = ctx.inferProgram
     reporter.info("Running Inference Engine...")
@@ -80,7 +80,7 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
     //reporter.info("Analysis Order: " + functionsToAnalyze.map(_.id))
     var results: Map[FunDef, InferenceCondition] = null
     if (!ctx.useCegis) {
-      results = analyseProgram(program, functionsToAnalyze)
+      results = analyseProgram(program, functionsToAnalyze, progressCallback)
       //println("Inferrence did not succeeded for functions: "+functionsToAnalyze.filterNot(succeededFuncs.contains _).map(_.id))
     } else {
       var remFuncs = functionsToAnalyze
@@ -89,7 +89,7 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
       breakable {
         while (b <= maxCegisBound) {
           Stats.updateCumStats(1, "CegisBoundsTried")
-          val succeededFuncs = analyseProgram(program, remFuncs)
+          val succeededFuncs = analyseProgram(program, remFuncs, progressCallback)
           remFuncs = remFuncs.filterNot(succeededFuncs.contains _)
           if (remFuncs.isEmpty) break;
           b += 5 //increase bounds in steps of 5
@@ -126,7 +126,8 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
    * TODO: use function names in inference conditions, so that
    * we an get rid of dependence on origFd in many places.
    */
-  def analyseProgram(startProg: Program, functionsToAnalyze: Seq[FunDef]): Map[FunDef, InferenceCondition] = {
+  def analyseProgram(startProg: Program, functionsToAnalyze: Seq[FunDef],
+      progressCallback: Option[InferenceCondition => Unit]): Map[FunDef, InferenceCondition] = {
     val reporter = ctx.reporter
     val funToTmpl =
       if (ctx.autoInference) {
@@ -178,25 +179,28 @@ class InferenceEngine(ctx: InferenceContext) extends Interruptible {
                   val origFd = functionByName(fd.id.name, startProg).get
                   val inv = if (origFd.hasTemplate) {
                     TemplateInstantiator.getAllInvariants(model.get,
-                      Map(origFd -> origFd.getTemplate))(origFd)
+                      Map(origFd -> origFd.getTemplate), prettyInv = true)(origFd)
                   } else {
                     val currentInv = TemplateInstantiator.getAllInvariants(model.get,
-                      Map(fd -> fd.getTemplate))(fd)
+                      Map(fd -> fd.getTemplate), prettyInv = true)(fd)
                     // map result variable  in currentInv
                     val repInv = replace(Map(getResId(fd).get.toVariable -> getResId(origFd).get.toVariable), currentInv)
                     translateExprToProgram(repInv, prog, startProg)
                   }
                   // record the inferred invariants
-                  if (analyzedSet.contains(origFd)) {
+                  val inferCond = if (analyzedSet.contains(origFd)) {
                     val ic = analyzedSet(origFd)
                     ic.addInv(Seq(inv))
+                    ic
                   } else {
                     val ic = new InferenceCondition(Seq(inv), origFd)
                     ic.time = if (first) Some(funcTime) else Some(0.0)
                     // update analyzed set
                     analyzedSet += (origFd -> ic)
                     first = false
+                    ic
                   }
+                  progressCallback.map(cb => cb(inferCond))
                 }
                 val funsWithTemplates = inferredFuns.filter { fd =>
                   val origFd = functionByName(fd.id.name, startProg).get

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

@@ -19,26 +19,27 @@ import Util._
 import PredicateUtil._
 import ProgramUtil._
 import SolverUtil._
+import FunctionUtils._
+import purescala._
 
 class InferenceCondition(invs: Seq[Expr], funDef: FunDef)
-  extends VC(BooleanLiteral(true), funDef, null) {
+    extends VC(BooleanLiteral(true), funDef, null) {
 
   var time: Option[Double] = None
   var invariants = invs
 
-  def addInv(invs : Seq[Expr]) {
+  def addInv(invs: Seq[Expr]) {
     invariants ++= invs
   }
 
   lazy val prettyInv = invariants.map(inv =>
     simplifyArithmetic(InstUtil.replaceInstruVars(multToTimes(inv), fd))) match {
     case Seq() => None
-    case Seq(inv) => Some(inv)
     case invs =>
       invs.map(ExpressionTransformer.simplify _).filter(_ != tru) match {
-        case Seq() => Some(tru)
+        case Seq()     => Some(tru)
         case Seq(ninv) => Some(ninv)
-        case ninvs => Some(And(ninvs))
+        case ninvs     => Some(And(ninvs))
       }
   }
 
@@ -50,7 +51,7 @@ class InferenceCondition(invs: Seq[Expr], funDef: FunDef)
 }
 
 class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ctx: InferenceContext)
-  extends VerificationReport(program, Map()) {
+    extends VerificationReport(program, Map()) {
 
   import scala.math.Ordering.Implicits._
   val conditions: Seq[InferenceCondition] =
@@ -107,10 +108,12 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ct
     }.toMap
     assignTemplateAndCojoinPost(funToTmpl, program)
   }
+}
 
-  def finalProgramWoInstrumentation: Program = {
+object InferenceReportUtil {
 
-    val funToUninstFun = program.definedFunctions.foldLeft(Map[FunDef, FunDef]()) {
+  /*  def programWoInstrumentation(ctx: InferenceContext, p: Program, ics: Seq[InferenceCondition]) = {
+    val funToUninstFun = p.definedFunctions.foldLeft(Map[FunDef, FunDef]()) {
       case (acc, fd) =>
         val uninstFunName = InstUtil.userFunctionName(fd)
         val uninstFdOpt =
@@ -120,11 +123,131 @@ class InferenceReport(fvcs: Map[FunDef, List[VC]], program: Program)(implicit ct
           acc + (fd -> uninstFdOpt.get)
         } else acc
     }
-    val funToPost = conditions.collect {
+    val funToPost = ics.collect {
       case cd if cd.prettyInv.isDefined && funToUninstFun.contains(cd.fd) =>
         funToUninstFun(cd.fd) -> cd.prettyInv.get
     }.toMap
     //println("Function to template: " + funToTmpl.map { case (k, v) => s"${k.id.name} --> $v" }.mkString("\n"))
     assignTemplateAndCojoinPost(Map(), ctx.initProgram, funToPost, uniqueIdDisplay = false)
+  }*/
+
+  def pluginResultInInput(ctx: InferenceContext, ics: Seq[InferenceCondition], p: Program) = {
+
+    val solvedICs = ics.filter { _.prettyInv.isDefined }
+    // mapping from init to output
+    val outputFunMap =
+      functionsWOFields(ctx.initProgram.definedFunctions).map {
+        case fd if fd.isTheoryOperation => (fd -> fd)
+        case fd => {
+          val freshId = FreshIdentifier(fd.id.name, fd.returnType)
+          val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
+          fd -> newfd
+        }
+      }.toMap
+
+    def fullNameWoInst(fd: FunDef) = {
+      val splits = DefOps.fullName(fd)(p).split("-")
+      if (!splits.isEmpty) splits(0)
+      else ""
+    }
+
+    // mapping from p to output
+    val progFunMap = (Map[FunDef, FunDef]() /: functionsWOFields(p.definedFunctions)) {
+      case (acc, fd) =>
+        val inFun = functionByFullName(fullNameWoInst(fd), ctx.initProgram)
+        if (inFun.isDefined)
+          acc + (fd -> outputFunMap(inFun.get))
+        else acc
+    }.toMap
+
+    // mapping from init to ic
+    val initICmap = (Map[FunDef, InferenceCondition]() /: solvedICs) {
+      case (acc, ic) =>
+        val initfd = functionByFullName(fullNameWoInst(ic.fd), ctx.initProgram)
+        if (initfd.isDefined) {
+          acc + (initfd.get -> ic)
+        } else acc
+    }
+
+    def mapProgram(funMap: Map[FunDef, FunDef]) = {
+
+      def mapExpr(ine: Expr): Expr = {
+        val replaced = simplePostTransform((e: Expr) => e match {
+          case FunctionInvocation(tfd, args) if funMap.contains(tfd.fd) =>
+            FunctionInvocation(TypedFunDef(funMap(tfd.fd), tfd.tps), args)
+          case _ => e
+        })(ine)
+        replaced
+      }
+
+      for ((from, to) <- funMap) {
+        to.body = from.body.map(mapExpr)
+        to.precondition = from.precondition.map(mapExpr)
+        if (initICmap.contains(from)) {
+          val ic = initICmap(from)
+          val paramMap = (ic.fd.params zip from.params).map {
+            case (p1, p2) =>
+              (p1.id.toVariable -> p2.id.toVariable)
+          }.toMap
+          val icres = getResId(ic.fd).get
+          val npost =
+            if (from.hasPostcondition) {
+              val resid = getResId(from).get
+              val inv = replace(Map(icres.toVariable -> resid.toVariable) ++ paramMap, ic.prettyInv.get)
+              val postBody = from.postWoTemplate.map(post => createAnd(Seq(post, inv))).getOrElse(inv)
+              Lambda(Seq(ValDef(resid)), postBody)
+            } else {
+              val resid = FreshIdentifier(icres.name, icres.getType)
+              val inv = replace(Map(icres.toVariable -> resid.toVariable) ++ paramMap, ic.prettyInv.get)
+              Lambda(Seq(ValDef(resid)), inv)
+            }
+          to.postcondition = Some(mapExpr(npost))
+        } else
+          to.postcondition = from.postcondition.map(mapExpr)
+        //copy annotations
+        from.flags.foreach(to.addFlag(_))
+      }
+    }
+    mapProgram(outputFunMap ++ progFunMap)
+    copyProgram(ctx.initProgram, (defs: Seq[Definition]) => defs.map {
+      case fd: FunDef if outputFunMap.contains(fd) =>
+        outputFunMap(fd)
+      case d => d
+    })
+    /*if (debugSimplify)
+      println("After Simplifications: \n" + ScalaPrinter.apply(newprog))*/
+    //    /newprog
+    /*if (ic.prettyInv.isDefined) {
+      val uninstFunName = InstUtil.userFunctionName(ic.fd)
+      val inputFdOpt =
+        if (uninstFunName.isEmpty) None
+        else functionByName(uninstFunName, ctx.initProgram)
+      inputFdOpt match {
+        case None => ctx.initProgram
+        case Some(inFd) =>
+          ProgramUtil.copyProgram(ctx.initProgram, defs => defs map {
+            case fd if fd.id == inFd.id =>
+              val newfd = new FunDef(FreshIdentifier(inFd.id.name), inFd.tparams, inFd.params, inFd.returnType)
+              newfd.body = inFd.body
+              newfd.precondition = inFd.precondition
+              val fdres = getResId(ic.fd).get
+              val npost =
+                if (inFd.hasPostcondition) {
+                  val resid = getResId(inFd).get
+                  val inv = replace(Map(fdres.toVariable -> resid.toVariable), ic.prettyInv.get)
+                  // map also functions here.
+                  val postBody = inFd.postWoTemplate.map(post => createAnd(Seq(post, inv))).getOrElse(inv)
+                  Lambda(Seq(ValDef(resid)), postBody)
+                } else {
+                  val resid = FreshIdentifier(fdres.name, fdres.getType)
+                  val inv = replace(Map(fdres.toVariable -> resid.toVariable), ic.prettyInv.get)
+                  Lambda(Seq(ValDef(resid)), inv)
+                }
+              newfd.postcondition = Some(npost)
+              newfd
+            case d => d
+          })
+      }
+    } else ctx.initProgram*/
   }
 }
\ No newline at end of file

src/main/scala/leon/invariant/factories/TemplateInstantiator.scala

@@ -20,12 +20,12 @@ import PredicateUtil._
 import ProgramUtil._
 
 object TemplateInstantiator {
-    /**
+  /**
    * Computes the invariant for all the procedures given a mapping for the
    * template variables.
    * (Undone) If the mapping does not have a value for an id, then the id is bound to the simplest value
    */
-  def getAllInvariants(model: Model, templates :Map[FunDef, Expr]): Map[FunDef, Expr] = {
+  def getAllInvariants(model: Model, templates: Map[FunDef, Expr], prettyInv: Boolean = false): Map[FunDef, Expr] = {
     val invs = templates.map((pair) => {
       val (fd, t) = pair
       //flatten the template
@@ -37,7 +37,7 @@ object TemplateInstantiator {
         (v, model(v.id))
       }).toMap
 
-      val instTemplate = instantiate(template, tempVarMap)
+      val instTemplate = instantiate(template, tempVarMap, prettyInv)
       //now unflatten it
       val comprTemp = ExpressionTransformer.unFlatten(instTemplate, freevars)
       (fd, comprTemp)
@@ -49,7 +49,7 @@ object TemplateInstantiator {
    * Instantiates templated subexpressions of the given expression (expr) using the given mapping for the template variables.
    * The instantiation also takes care of converting the rational coefficients to integer coefficients.
    */
-  def instantiate(expr: Expr, tempVarMap: Map[Expr, Expr]): Expr = {
+  def instantiate(expr: Expr, tempVarMap: Map[Expr, Expr], prettyInv: Boolean = false): Expr = {
     //do a simple post transform and replace the template vars by their values
     val inv = simplePostTransform((tempExpr: Expr) => tempExpr match {
       case e @ Operator(Seq(lhs, rhs), op) if ((e.isInstanceOf[Equals] || e.isInstanceOf[LessThan]
@@ -57,31 +57,28 @@ object TemplateInstantiator {
         || e.isInstanceOf[GreaterEquals])
         &&
         !getTemplateVars(tempExpr).isEmpty) => {
-
-        //println("Template Expression: "+tempExpr)
         val linearTemp = LinearConstraintUtil.exprToTemplate(tempExpr)
-        // println("MODEL\n" + tempVarMap)
-        instantiateTemplate(linearTemp, tempVarMap)
+        instantiateTemplate(linearTemp, tempVarMap, prettyInv)
       }
       case _ => tempExpr
     })(expr)
     inv
   }
 
-  def validateLiteral(e : Expr) = e match {
+  def validateLiteral(e: Expr) = e match {
     case FractionalLiteral(num, denom) => {
       if (denom == 0)
-        throw new IllegalStateException("Denominator is zero !! " +e)
+        throw new IllegalStateException("Denominator is zero !! " + e)
       if (denom < 0)
         throw new IllegalStateException("Denominator is negative: " + denom)
       true
     }
-    case IntLiteral(_) => true
+    case IntLiteral(_)             => true
     case InfiniteIntegerLiteral(_) => true
-    case _ => throw new IllegalStateException("Not a real literal: " + e)
+    case _                         => throw new IllegalStateException("Not a real literal: " + e)
   }
 
-  def instantiateTemplate(linearTemp: LinearTemplate, tempVarMap: Map[Expr, Expr]): Expr = {
+  def instantiateTemplate(linearTemp: LinearTemplate, tempVarMap: Map[Expr, Expr], prettyInv: Boolean = false): Expr = {
     val bigone = BigInt(1)
     val coeffMap = linearTemp.coeffTemplate.map((entry) => {
       val (term, coeffTemp) = entry
@@ -92,20 +89,19 @@ object TemplateInstantiator {
 
       (term -> coeff)
     })
-    val const = if (linearTemp.constTemplate.isDefined){
+    val const = if (linearTemp.constTemplate.isDefined) {
       val constE = replace(tempVarMap, linearTemp.constTemplate.get)
       val constV = RealValuedExprEvaluator.evaluate(constE)
 
       validateLiteral(constV)
       Some(constV)
-    }
-    else None
+    } else None
 
     val realValues: Seq[Expr] = coeffMap.values.toSeq ++ { if (const.isDefined) Seq(const.get) else Seq() }
     //the coefficients could be fractions ,so collect all the denominators
     val getDenom = (t: Expr) => t match {
       case FractionalLiteral(num, denum) => denum
-      case _ => bigone
+      case _                             => bigone
     }
 
     val denoms = realValues.foldLeft(Set[BigInt]())((acc, entry) => { acc + getDenom(entry) })
@@ -114,8 +110,8 @@ object TemplateInstantiator {
     val gcd = denoms.foldLeft(bigone)((acc, d) => acc.gcd(d))
     val lcm = denoms.foldLeft(BigInt(1))((acc, d) => {
       val product = (acc * d)
-      if(product % gcd == 0)
-        product/ gcd
+      if (product % gcd == 0)
+        product / gcd
       else product
     })
 
@@ -131,6 +127,8 @@ object TemplateInstantiator {
     val intConst = if (const.isDefined) Some(scaleNum(const.get)) else None
 
     val linearCtr = new LinearConstraint(linearTemp.op, intCoeffMap, intConst)
-    linearCtr.toExpr
+    if (prettyInv)
+      linearCtr.toPrettyExpr
+    else linearCtr.toExpr
   }
 }
\ No newline at end of file

src/main/scala/leon/invariant/structure/Constraint.scala

@@ -45,10 +45,6 @@ class LinearTemplate(oper: Seq[Expr] => Expr,
     assert(coeffTemp.values.foldLeft(true)((acc, e) => {
       acc && isTemplateExpr(e)
     }))
-
-    //print the template mapping
-    /*println("Coeff Mapping: "+coeffTemp)
-    println("Constant: "+constTemplate)*/
     coeffTemp
   }
 
@@ -72,8 +68,6 @@ class LinearTemplate(oper: Seq[Expr] => Expr,
       else Plus(lhs, constTemp.get)
     } else lhs
     val expr = oper(Seq(lhs, zero))
-    //assert(expr.isInstanceOf[Equals] || expr.isInstanceOf[LessThan] || expr.isInstanceOf[GreaterThan]
-    //  || expr.isInstanceOf[LessEquals] || expr.isInstanceOf[GreaterEquals])
     expr
   }
 
@@ -96,6 +90,45 @@ class LinearTemplate(oper: Seq[Expr] => Expr,
 
   override def toExpr: Expr = template
 
+  /**
+   * Converts the template to a more human readable form
+   * by group positive (and negative) terms together
+   */
+  def toPrettyExpr = {
+    val (lhsCoeff, rhsCoeff) = coeffTemplate.partition {
+      case (term, InfiniteIntegerLiteral(v)) =>
+        v >= 0
+      case _ => true
+    }
+    var lhsExprs: Seq[Expr] = lhsCoeff.map(e => Times(e._2, e._1)).toSeq
+    var rhsExprs: Seq[Expr] = rhsCoeff.map {
+      case (term, InfiniteIntegerLiteral(v)) =>
+        Times(InfiniteIntegerLiteral(-v), term) // make the coeff +ve
+    }.toSeq
+    constTemplate match {
+      case Some(InfiniteIntegerLiteral(v)) if v < 0 =>
+        rhsExprs :+= InfiniteIntegerLiteral(-v)
+      case Some(c) =>
+        lhsExprs :+= c
+      case _ => Nil
+    }
+    val lhsExprOpt = ((None: Option[Expr]) /: lhsExprs) {
+      case (acc, minterm) =>
+        if (acc.isDefined)
+          Some(Plus(acc.get, minterm))
+        else Some(minterm)
+    }
+    val rhsExprOpt = ((None: Option[Expr]) /: rhsExprs) {
+      case (acc, minterm) =>
+        if (acc.isDefined)
+          Some(Plus(acc.get, minterm))
+        else Some(minterm)
+    }
+    val lhs = lhsExprOpt.getOrElse(InfiniteIntegerLiteral(0))
+    val rhs = rhsExprOpt.getOrElse(InfiniteIntegerLiteral(0))
+    oper(Seq(lhs, rhs))
+  }
+
   override def toString(): String = {
 
     val coeffStr = if (coeffTemplate.isEmpty) ""
@@ -145,7 +178,6 @@ class LinearConstraint(opr: Seq[Expr] => Expr, cMap: Map[Expr, Expr], constant:
     assert(cMap.values.foldLeft(true)((acc, e) => {
       acc && variablesOf(e).isEmpty
     }))
-
     //TODO: here we should try to simplify the constant expressions
     cMap
   }

src/main/scala/leon/invariant/util/TreeUtil.scala

@@ -152,6 +152,10 @@ object ProgramUtil {
     prog.definedFunctions.find(fd => fd.id.name == nm)
   }
 
+  def functionByFullName(nm: String, prog: Program) = {
+    prog.definedFunctions.find(fd => fullName(fd)(prog) == nm)
+  }
+
   def functionsWOFields(fds: Seq[FunDef]): Seq[FunDef] = {
     fds.filter(_.isRealFunction)
   }

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

@@ -113,6 +113,8 @@ object InstUtil {
   }
 
   def replaceInstruVars(e: Expr, fd: FunDef): Expr = {
-    replace(getInstVariableMap(fd), e)
+    val resvar = getResId(fd).get.toVariable
+    val newres = FreshIdentifier(resvar.id.name, resvar.getType).toVariable
+    replace(getInstVariableMap(fd) + (TupleSelect(resvar, 1) -> newres), e)
   }
 }