From bbf7c241e84fc24d378f598bbdfe2bf4a8f8a805 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 18 Mar 2016 17:39:33 +0100
Subject: [PATCH] Refactor VerificationContext
---
.../leon/laziness/LazyVerificationPhase.scala | 3 +--
src/main/scala/leon/repair/Repairman.scala | 2 +-
src/main/scala/leon/synthesis/Synthesizer.scala | 2 +-
src/main/scala/leon/verification/Tactic.scala | 2 +-
.../verification/VerificationCondition.scala | 3 +--
.../leon/verification/VerificationContext.scala | 16 +++++++++++-----
.../leon/verification/VerificationPhase.scala | 8 ++++----
7 files changed, 20 insertions(+), 16 deletions(-)
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index b41835e1a..864f3ff28 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -199,7 +199,6 @@ object LazyVerificationPhase {
def checkVCs(vcs: List[VC], checkCtx: LeonContext, p: Program) = {
val timeout: Option[Long] = None
- val reporter = checkCtx.reporter
// Solvers selection and validation
val baseSolverF = SolverFactory.getFromSettings(checkCtx, p)
val solverF = timeout match {
@@ -208,7 +207,7 @@ object LazyVerificationPhase {
case None =>
baseSolverF
}
- val vctx = VerificationContext(checkCtx, p, solverF, reporter)
+ val vctx = new VerificationContext(checkCtx, p, solverF)
try {
VerificationPhase.checkVCs(vctx, vcs)
//println("Resource Verification Results: \n" + veriRep.summaryString)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 919a8c458..4b6d0ce83 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -201,7 +201,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
def getVerificationCExs(fd: FunDef): Seq[Example] = {
val timeoutMs = verifTimeoutMs.getOrElse(3000L)
val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(timeoutMs)
- val vctx = VerificationContext(ctx, program, solverf, reporter)
+ val vctx = new VerificationContext(ctx, program, solverf)
val vcs = VerificationPhase.generateVCs(vctx, Seq(fd))
try {
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 0a668a059..3a2a1df7f 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -144,7 +144,7 @@ class Synthesizer(val context : LeonContext,
val solverf = SolverFactory.default(context, npr).withTimeout(timeout)
try {
- val vctx = VerificationContext(context, npr, solverf, context.reporter)
+ val vctx = new VerificationContext(context, npr, solverf)
val vcs = generateVCs(vctx, fds)
val vcreport = checkVCs(vctx, vcs, stopWhen = _.isInvalid)
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 008a03f5a..75910e625 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -9,7 +9,7 @@ import purescala.Expressions._
abstract class Tactic(vctx: VerificationContext) {
val description : String
- implicit protected val ctx = vctx.context
+ implicit val ctx = vctx
def generateVCs(fd: FunDef): Seq[VC] = {
generatePostconditions(fd) ++
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 1cbbf2103..d7850d079 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -49,7 +49,6 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
def report(vctx: VerificationContext) {
import vctx.reporter
- import vctx.context
status match {
case VCStatus.Valid =>
@@ -64,7 +63,7 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
// is free to simplify
val strings = cex.toSeq.sortBy(_._1.name).map {
case (id, v) =>
- (id.asString(context), SelfPrettyPrinter.print(v, PrettyPrinter(v))(vctx.context, vctx.program))
+ (id.asString(vctx), SelfPrettyPrinter.print(v, PrettyPrinter(v))(vctx, vctx.program))
}
if (strings.nonEmpty) {
diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala
index be8f9efe5..87811eb89 100644
--- a/src/main/scala/leon/verification/VerificationContext.scala
+++ b/src/main/scala/leon/verification/VerificationContext.scala
@@ -6,11 +6,17 @@ package verification
import purescala.Definitions.Program
import solvers._
-case class VerificationContext (
+class VerificationContext(
context: LeonContext,
- program: Program,
- solverFactory: SolverFactory[Solver],
- reporter: Reporter
+ val program: Program,
+ val solverFactory: SolverFactory[Solver]
+) extends LeonContext(
+ context.reporter,
+ context.interruptManager,
+ context.options,
+ context.files,
+ context.classDir,
+ context.timers
) {
- val checkInParallel: Boolean = context.findOptionOrDefault(VerificationPhase.optParallelVCs)
+ lazy val checkInParallel: Boolean = context.findOptionOrDefault(VerificationPhase.optParallelVCs)
}
diff --git a/src/main/scala/leon/verification/VerificationPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
index 39ed875a0..01df60771 100644
--- a/src/main/scala/leon/verification/VerificationPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -36,7 +36,7 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
baseSolverF
}
- val vctx = VerificationContext(ctx, program, solverF, reporter)
+ val vctx = new VerificationContext(ctx, program, solverF)
reporter.debug("Generating Verification Conditions...")
@@ -97,7 +97,7 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
vcs: Seq[VC],
stopWhen: VCResult => Boolean = _ => false
): VerificationReport = {
- val interruptManager = vctx.context.interruptManager
+ val interruptManager = vctx.interruptManager
var stop = false
@@ -126,7 +126,7 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
import vctx.reporter
import vctx.solverFactory
- val interruptManager = vctx.context.interruptManager
+ val interruptManager = vctx.interruptManager
val vcCond = vc.condition
@@ -135,7 +135,7 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
try {
reporter.synchronized {
reporter.info(s" - Now considering '${vc.kind}' VC for ${vc.fd.id} @${vc.getPos}...")
- reporter.debug(simplifyLets(vcCond).asString(vctx.context))
+ reporter.debug(simplifyLets(vcCond).asString(vctx))
reporter.debug("Solving with: " + s.name)
}
--
GitLab