Minor refactorings in lazy evaluation for leon-web integration

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

@@ -23,7 +23,7 @@ import Stats._
  * This phase performs automatic invariant inference.
  * TODO: should time be implicitly made positive
  */
-class InferenceEngine(ctx: InferenceContext) extends Interruptible {
+class InferenceEngine(val ctx: InferenceContext) extends Interruptible {
 
   val debugBottomupIterations = false
   val debugAnalysisOrder = false

src/main/scala/leon/laziness/LazinessEliminationPhase.scala

@@ -41,7 +41,33 @@ object LazinessEliminationPhase extends SimpleLeonPhase[Program, LazyVerificatio
    * TODO: add inlining annotations for optimization.
    */
   def apply(ctx: LeonContext, prog: Program): LazyVerificationReport = {
+    val (progWOInstSpecs, instProg) = genVerifiablePrograms(ctx, prog)
+    val checkCtx = contextForChecks(ctx)
+    val stateVeri =
+      if (!skipStateVerification)
+        Some(checkSpecifications(progWOInstSpecs, checkCtx))
+      else None
+
+    val resourceVeri =
+      if (!skipResourceVerification)
+        Some(checkInstrumentationSpecs(instProg, checkCtx,
+          checkCtx.findOption(LazinessEliminationPhase.optUseOrb).getOrElse(false)))
+      else None
+    // dump stats if enabled
+    if (ctx.findOption(GlobalOptions.optBenchmark).getOrElse(false)) {
+      val modid = prog.units.find(_.isMainUnit).get.id
+      val filename = modid + "-stats.txt"
+      val pw = new PrintWriter(filename)
+      Stats.dumpStats(pw)
+      SpecificStats.dumpOutputs(pw)
+      ctx.reporter.info("Stats dumped to file: " + filename)
+      pw.close()
+    }
+    // return a report
+    new LazyVerificationReport(stateVeri, resourceVeri)
+  }
 
+  def genVerifiablePrograms(ctx: LeonContext, prog: Program): (Program, Program) = {
     if (dumpInputProg)
       println("Input prog: \n" + ScalaPrinter.apply(prog))
 
@@ -73,35 +99,12 @@ object LazinessEliminationPhase extends SimpleLeonPhase[Program, LazyVerificatio
     if (dumpProgWOInstSpecs)
       prettyPrintProgramToFile(progWOInstSpecs, ctx, "-woinst")
 
-    val checkCtx = contextForChecks(ctx)
-    val stateVeri =
-      if (!skipStateVerification)
-        Some(checkSpecifications(progWOInstSpecs, checkCtx))
-      else None
-
     // instrument the program for resources (note: we avoid checking preconditions again here)
     val instrumenter = new LazyInstrumenter(InliningPhase.apply(ctx, typeCorrectProg), ctx, closureFactory)
     val instProg = instrumenter.apply
     if (dumpInstrumentedProgram)
       prettyPrintProgramToFile(instProg, ctx, "-withinst", uniqueIds = true)
-
-    val resourceVeri =
-      if (!skipResourceVerification)
-        Some(checkInstrumentationSpecs(instProg, checkCtx,
-          checkCtx.findOption(LazinessEliminationPhase.optUseOrb).getOrElse(false)))
-      else None
-    // dump stats if enabled
-    if (ctx.findOption(GlobalOptions.optBenchmark).getOrElse(false)) {
-      val modid = prog.units.find(_.isMainUnit).get.id
-      val filename = modid + "-stats.txt"
-      val pw = new PrintWriter(filename)
-      Stats.dumpStats(pw)
-      SpecificStats.dumpOutputs(pw)
-      ctx.reporter.info("Stats dumped to file: " + filename)
-      pw.close()
-    }
-    // return a report
-    new LazyVerificationReport(stateVeri, resourceVeri)
+    (progWOInstSpecs, instProg)
   }
 
   /**

src/main/scala/leon/laziness/LazyVerificationPhase.scala

@@ -94,24 +94,25 @@ object LazyVerificationPhase {
       if (fd.annotations.contains("axiom"))
         fd.addFlag(Annotation("library", Seq()))
     }
-    val funsToCheck = p.definedFunctions.filter(shouldGenerateVC)
     val rep =
       if (useOrb) {
-        // create an inference context
+        /*// create an inference context
         val inferOpts = Main.processOptions(Seq("--disableInfer", "--assumepreInf", "--minbounds", "--solvers=smt-cvc4"))
         val ctxForInf = LeonContext(checkCtx.reporter, checkCtx.interruptManager,
           inferOpts.options ++ checkCtx.options)
         val inferctx = new InferenceContext(p, ctxForInf)
         val vcSolver = (funDef: FunDef, prog: Program) => new VCSolver(inferctx, prog, funDef)
-
         if (debugInferProgram){
           prettyPrintProgramToFile(inferctx.inferProgram, checkCtx, "-inferProg", true)
         }
 
         val results = (new InferenceEngine(inferctx)).analyseProgram(inferctx.inferProgram,
             funsToCheck.map(InstUtil.userFunctionName), vcSolver, None)
-        new InferenceReport(results.map { case (fd, ic) => (fd -> List[VC](ic)) }, inferctx.inferProgram)(inferctx)
+        new InferenceReport(results.map { case (fd, ic) => (fd -> List[VC](ic)) }, inferctx.inferProgram)(inferctx)*/
+        val inferctx = getInferenceContext(checkCtx, p)
+        checkUsingOrb(new InferenceEngine(inferctx), inferctx)
       } else {
+        val funsToCheck = p.definedFunctions.filter(shouldGenerateVC)
         val rep = checkVCs(funsToCheck.map(vcForFun), checkCtx, p)
         // record some stats
         collectCumulativeStats(rep)
@@ -122,6 +123,25 @@ object LazyVerificationPhase {
     rep
   }
 
+  def getInferenceContext(checkCtx: LeonContext, p: Program): InferenceContext = {
+    // create an inference context
+    val inferOpts = Main.processOptions(Seq("--disableInfer", "--assumepreInf", "--minbounds", "--solvers=smt-cvc4"))
+    val ctxForInf = LeonContext(checkCtx.reporter, checkCtx.interruptManager,
+      inferOpts.options ++ checkCtx.options)
+    new InferenceContext(p, ctxForInf)
+  }
+
+  def checkUsingOrb(infEngine: InferenceEngine, inferctx: InferenceContext) = {
+    if (debugInferProgram) {
+      prettyPrintProgramToFile(inferctx.inferProgram, inferctx.leonContext, "-inferProg", true)
+    }
+    val funsToCheck = inferctx.initProgram.definedFunctions.filter(shouldGenerateVC)
+    val vcSolver = (funDef: FunDef, prog: Program) => new VCSolver(inferctx, prog, funDef)
+    val results = infEngine.analyseProgram(inferctx.inferProgram,
+      funsToCheck.map(InstUtil.userFunctionName), vcSolver, None)
+    new InferenceReport(results.map { case (fd, ic) => (fd -> List[VC](ic)) }, inferctx.inferProgram)(inferctx)
+  }
+
   def accessesSecondRes(e: Expr, resid: Identifier): Boolean =
       exists(_ == TupleSelect(resid.toVariable, 2))(e)