From d4028d9a8b2e912d4c01f3e4369f92ed94a356de Mon Sep 17 00:00:00 2001
From: ravi <ravi.kandhadai@epfl.ch>
Date: Wed, 23 Mar 2016 19:22:40 +0100
Subject: [PATCH] Minor refactorings in lazy evaluation for leon-web
integration
---
.../invariant/engine/InferenceEngine.scala | 2 +-
.../laziness/LazinessEliminationPhase.scala | 51 ++++++++++---------
.../leon/laziness/LazyVerificationPhase.scala | 28 ++++++++--
3 files changed, 52 insertions(+), 29 deletions(-)
diff --git a/src/main/scala/leon/invariant/engine/InferenceEngine.scala b/src/main/scala/leon/invariant/engine/InferenceEngine.scala
index db4eadea6..4d73ffae3 100644
--- a/src/main/scala/leon/invariant/engine/InferenceEngine.scala
+++ b/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
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 9501f2dc3..2d65f404e 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/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)
}
/**
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index fd063f9d7..a53572667 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/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)
--
GitLab