From fc3d723fa9e843bb30b5702afc5332fed7308451 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 19 Oct 2015 15:56:44 +0200
Subject: [PATCH] Offer command line option to parallelize verification
conditions
---
src/main/scala/leon/repair/Repairman.scala | 1 -
src/main/scala/leon/verification/AnalysisPhase.scala | 11 +++++++++--
.../leon/verification/VerificationCondition.scala | 1 -
.../scala/leon/verification/VerificationContext.scala | 4 +++-
.../scala/leon/regression/repair/RepairSuite.scala | 2 ++
5 files changed, 14 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index e5a1eaafe..aac4a8d4a 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -173,7 +173,6 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val report = AnalysisPhase.checkVCs(
vctx,
vcs,
- checkInParallel = true,
stopAfter = Some({ (vc, vr) => vr.isInvalid })
)
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 8c6c7d0ce..e5edc1308 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -7,6 +7,7 @@ import purescala.Definitions._
import purescala.ExprOps._
import scala.concurrent.duration._
+import java.lang.System
import solvers._
@@ -14,6 +15,10 @@ object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
val name = "Analysis"
val description = "Leon Verification"
+ val optParallelVCs = LeonFlagOptionDef("parallel", "Check verification conditions in parallel", default = false)
+
+ override val definedOptions: Set[LeonOptionDef[Any]] = Set(optParallelVCs)
+
implicit val debugSection = utils.DebugSectionVerification
def apply(ctx: LeonContext, program: Program): VerificationReport = {
@@ -89,7 +94,6 @@ object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
def checkVCs(
vctx: VerificationContext,
vcs: Seq[VC],
- checkInParallel: Boolean = false,
stopAfter: Option[(VC, VCResult) => Boolean] = None
): VerificationReport = {
val interruptManager = vctx.context.interruptManager
@@ -98,7 +102,7 @@ object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
val initMap: Map[VC, Option[VCResult]] = vcs.map(v => v -> None).toMap
- val results = if (checkInParallel) {
+ val results = if (vctx.checkInParallel) {
for (vc <- vcs.par if !stop) yield {
val r = checkVC(vctx, vc)
if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
@@ -168,6 +172,9 @@ object AnalysisPhase extends SimpleLeonPhase[Program,VerificationReport] {
}
reporter.synchronized {
+ if (vctx.checkInParallel) {
+ reporter.info(s" - Result for '${vc.kind}' VC for ${vc.fd.id} @${vc.getPos}:")
+ }
res.report(vctx)
}
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 33511b23c..b138559af 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -5,7 +5,6 @@ package leon.verification
import leon.purescala.Expressions._
import leon.purescala.Definitions._
import leon.purescala.PrettyPrinter
-import leon.purescala.Common._
import leon.utils.Positioned
import leon.solvers._
diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala
index 42d3eba62..ba3b5024e 100644
--- a/src/main/scala/leon/verification/VerificationContext.scala
+++ b/src/main/scala/leon/verification/VerificationContext.scala
@@ -11,4 +11,6 @@ case class VerificationContext (
program: Program,
solverFactory: SolverFactory[Solver],
reporter: Reporter
-)
+) {
+ val checkInParallel: Boolean = context.findOptionOrDefault(AnalysisPhase.optParallelVCs)
+}
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 44659752f..2ac93521b 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -7,6 +7,7 @@ import leon.test._
import leon.utils._
import leon.frontends.scalac.ExtractionPhase
import leon.repair._
+import leon.verification.AnalysisPhase
class RepairSuite extends LeonRegressionSuite {
val pipeline = ExtractionPhase andThen
@@ -34,6 +35,7 @@ class RepairSuite extends LeonRegressionSuite {
interruptManager = new InterruptManager(reporter),
options = Seq(
LeonOption(SharedOptions.optFunctions)(Seq(fileToFun(name))),
+ LeonOption(AnalysisPhase.optParallelVCs)(true),
LeonOption(SharedOptions.optTimeout)(180L)
)
)
--
GitLab