diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 36cffecf044fa4baa5364c46b24248e29c5fc3ab..a94debc9eae65b55aa9e7356dcdcee4d916ac064 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -78,34 +78,40 @@ class Synthesizer(val context : LeonContext,
res match {
case Some((solution, true)) =>
- val ssol = solution.toSimplifiedExpr(context, program)
(solution, true)
case Some((sol, false)) =>
- val ssol = sol.toSimplifiedExpr(context, program)
- reporter.info("Solution requires validation")
-
- val (npr, fds) = solutionToProgram(sol)
-
- val tsolver = new TimeoutSolver(new FairZ3Solver(silentContext), 10000L)
- tsolver.setProgram(npr)
-
- import verification.AnalysisPhase._
- val vcs = generateVerificationConditions(reporter, npr, fds.map(_.id.name))
- val vcreport = checkVerificationConditions(silentReporter, Seq(tsolver), vcs)
-
- if (vcreport.totalValid == vcreport.totalConditions) {
- (sol, true)
- } else {
- reporter.warning("Solution was invalid:")
- reporter.warning(fds.map(ScalaPrinter(_)).mkString("\n\n"))
- reporter.warning(vcreport.summaryString)
- (new AndOrGraphPartialSolution(search.g, (task: TaskRunRule) => Solution.choose(task.problem), false).getSolution, false)
- }
+ validateSolution(search, sol, 5000L)
case None =>
(new AndOrGraphPartialSolution(search.g, (task: TaskRunRule) => Solution.choose(task.problem), true).getSolution, false)
}
}
+ def validateSolution(search: AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution], sol: Solution, timeoutMs: Long): (Solution, Boolean) = {
+ import verification.AnalysisPhase._
+ import verification.VerificationContext
+
+ val ssol = sol.toSimplifiedExpr(context, program)
+ reporter.info("Solution requires validation")
+
+ val (npr, fds) = solutionToProgram(sol)
+
+ val tsolver = new TimeoutSolver(new FairZ3Solver(silentContext), timeoutMs)
+ tsolver.setProgram(npr)
+
+ val vcs = generateVerificationConditions(reporter, npr, fds.map(_.id.name))
+ val vctx = VerificationContext(context, Seq(tsolver), silentReporter)
+ val vcreport = checkVerificationConditions(vctx, vcs)
+
+ if (vcreport.totalValid == vcreport.totalConditions) {
+ (sol, true)
+ } else {
+ reporter.warning("Solution was invalid:")
+ reporter.warning(fds.map(ScalaPrinter(_)).mkString("\n\n"))
+ reporter.warning(vcreport.summaryString)
+ (new AndOrGraphPartialSolution(search.g, (task: TaskRunRule) => Solution.choose(task.problem), false).getSolution, false)
+ }
+ }
+
// Returns the new program and the new functions generated for this
def solutionToProgram(sol: Solution): (Program, Set[FunDef]) = {
import purescala.TypeTrees.TupleType
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 24b154cc1339a92683ad8def03b34231a12c6cc7..3809069403d45e2921a98969604f0d5ff31ef0c0 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -21,17 +21,15 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when trying to prove a verification condition.")
)
- def generateVerificationConditions(reporter: Reporter, program: Program, functionsToAnalyse: Set[String]) : List[VerificationCondition] = {
+ def generateVerificationConditions(reporter: Reporter, program: Program, functionsToAnalyse: Set[String]): Map[FunDef, List[VerificationCondition]] = {
val defaultTactic = new DefaultTactic(reporter)
defaultTactic.setProgram(program)
val inductionTactic = new InductionTactic(reporter)
inductionTactic.setProgram(program)
- var allVCs: Seq[VerificationCondition] = Seq.empty
- val analysedFunctions: MutableSet[String] = MutableSet.empty
+ var allVCs = Map[FunDef, List[VerificationCondition]]()
for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1 < fd2) if (functionsToAnalyse.isEmpty || functionsToAnalyse.contains(funDef.id.name))) {
- analysedFunctions += funDef.id.name
val tactic: Tactic =
if(funDef.annotations.contains("induct")) {
@@ -41,27 +39,27 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}
if(funDef.body.isDefined) {
- allVCs ++= tactic.generatePreconditions(funDef)
- allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
- allVCs ++= tactic.generatePostconditions(funDef)
- allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
- allVCs ++= tactic.generateArrayAccessChecks(funDef)
+ val funVCs = tactic.generatePreconditions(funDef) ++
+ tactic.generatePatternMatchingExhaustivenessChecks(funDef) ++
+ tactic.generatePostconditions(funDef) ++
+ tactic.generateMiscCorrectnessConditions(funDef) ++
+ tactic.generateArrayAccessChecks(funDef)
+
+ allVCs += funDef -> funVCs.toList
}
- allVCs = allVCs.sortWith((vc1, vc2) => {
- val id1 = vc1.funDef.id.name
- val id2 = vc2.funDef.id.name
- if(id1 != id2) id1 < id2 else vc1 < vc2
- })
}
- val notFound = functionsToAnalyse -- analysedFunctions
+ val notFound = functionsToAnalyse -- allVCs.keys.map(_.id.name)
notFound.foreach(fn => reporter.error("Did not find function \"" + fn + "\" though it was marked for analysis."))
- allVCs.toList
+ allVCs
}
- def checkVerificationConditions(reporter: Reporter, solvers: Seq[Solver], vcs: Seq[VerificationCondition]) : VerificationReport = {
- for(vcInfo <- vcs) {
+ def checkVerificationConditions(vctx: VerificationContext, vcs: Map[FunDef, List[VerificationCondition]]) : VerificationReport = {
+ val reporter = vctx.reporter
+ val solvers = vctx.solvers
+
+ for((funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1 < b._1); vcInfo <- vcs if !vctx.shouldStop.get()) {
val funDef = vcInfo.funDef
val vc = vcInfo.condition
@@ -88,37 +86,43 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val dt = ((t2 - t1) / 1000000) / 1000.0
solverResult match {
- case None => false
- case Some(true) => {
+ case _ if vctx.shouldStop.get() =>
+ reporter.info("=== CANCELLED ===")
+ false
+
+ case None =>
+ false
+
+ case Some(true) =>
reporter.info("==== VALID ====")
+ vcInfo.hasValue = true
vcInfo.value = Some(true)
vcInfo.solvedWith = Some(se)
vcInfo.time = Some(dt)
-
true
- }
- case Some(false) => {
+
+ case Some(false) =>
reporter.error("Found counter-example : ")
reporter.error(counterexample.toSeq.sortBy(_._1.name).map(p => p._1 + " -> " + p._2).mkString("\n"))
reporter.error("==== INVALID ====")
+ vcInfo.hasValue = true
vcInfo.value = Some(false)
vcInfo.solvedWith = Some(se)
vcInfo.counterExample = Some(counterexample)
vcInfo.time = Some(dt)
-
true
- }
+
}
}
}) match {
case None => {
+ vcInfo.hasValue = true
reporter.warning("No solver could prove or disprove the verification condition.")
}
- case _ =>
- }
-
- }
+ case _ =>
+ }
+ }
val report = new VerificationReport(vcs)
report
@@ -151,11 +155,12 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
solvers.foreach(_.setProgram(program))
+ val vctx = VerificationContext(ctx, solvers, reporter)
val report = if(solvers.size > 1) {
reporter.info("Running verification condition generation...")
val vcs = generateVerificationConditions(reporter, program, functionsToAnalyse)
- checkVerificationConditions(reporter, solvers, vcs)
+ checkVerificationConditions(vctx, vcs)
} else {
reporter.warning("No solver specified. Cannot test verification conditions.")
VerificationReport.emptyReport
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index a8cbfb51b041a367b2b63c27eba653a34b9f84a1..fee77a683fe344916f5a036cb826a394d16fa96a 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -11,6 +11,7 @@ class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: V
// None = still unknown
// Some(true) = valid
// Some(false) = valid
+ var hasValue = false
var value : Option[Boolean] = None
var solvedWith : Option[Solver] = None
var time : Option[Double] = None
diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala
new file mode 100644
index 0000000000000000000000000000000000000000..87300c40cc8d179ab726de6ce1ad9795e50a4be8
--- /dev/null
+++ b/src/main/scala/leon/verification/VerificationContext.scala
@@ -0,0 +1,13 @@
+package leon
+package verification
+
+import solvers.Solver
+
+import java.util.concurrent.atomic.AtomicBoolean
+
+case class VerificationContext (
+ context: LeonContext,
+ solvers: Seq[Solver],
+ reporter: Reporter,
+ shouldStop: AtomicBoolean = new AtomicBoolean(false)
+)
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index f5c95cbf0447ef362347460f2cec0421acf27aba..e40693199da6951cf4103618bbb342f501a2422f 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -1,6 +1,16 @@
-package leon.verification
+package leon
+package verification
+
+import purescala.Definitions.FunDef
+
+class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
+ val conditions : Seq[VerificationCondition] = fvcs.flatMap(_._2).toSeq.sortWith {
+ (vc1,vc2) =>
+ val id1 = vc1.funDef.id.name
+ val id2 = vc2.funDef.id.name
+ if(id1 != id2) id1 < id2 else vc1 < vc2
+ }
-class VerificationReport(val conditions : Seq[VerificationCondition]) {
lazy val totalConditions : Int = conditions.size
lazy val totalTime : Double = conditions.foldLeft(0.0d)((t,c) => t + c.time.getOrElse(0.0d))
@@ -25,7 +35,7 @@ class VerificationReport(val conditions : Seq[VerificationCondition]) {
}
object VerificationReport {
- def emptyReport : VerificationReport = new VerificationReport(Nil)
+ def emptyReport : VerificationReport = new VerificationReport(Map())
private def fit(str : String, maxLength : Int) : String = {
if(str.length <= maxLength) {
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
index 4f29e272fe66453c8389f5bd8f827238db71bdc1..318e481cdfd698a7c3eb78e1ad5f724efc8af254 100644
--- a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
@@ -44,7 +44,12 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
}
case opt => opt
}
+
val vr = AnalysisPhase.run(ctx.copy(options = newOptions))(pgm4)
+ completeVerificationReport(vr, parents, functionWasLoop _)
+ }
+
+ def completeVerificationReport(vr: VerificationReport, parents: Map[FunDef, FunDef], functionWasLoop: FunDef => Boolean): VerificationReport = {
val vcs = vr.conditions
//this is enough to convert invariant postcondition and inductive conditions. However the initial validity
@@ -52,7 +57,9 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
//To fix this, we need some information in the VCs about which function the precondtion refers to
//although we could arguably say that the term precondition is general enough to refer both to a loop invariant
//precondition and a function invocation precondition
- val freshVcs = vcs.map(vc => {
+ var freshFtoVcs = Map[FunDef, List[VerificationCondition]]()
+
+ for (vc <- vcs) {
val funDef = vc.funDef
if(functionWasLoop(funDef)) {
val freshVc = new VerificationCondition(
@@ -64,17 +71,13 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
freshVc.value = vc.value
freshVc.solvedWith = vc.solvedWith
freshVc.time = vc.time
- freshVc
- } else vc
- })
-
- val sortedFreshVcs = freshVcs.sortWith((vc1, vc2) => {
- val id1 = vc1.funDef.id.name
- val id2 = vc2.funDef.id.name
- if(id1 != id2) id1 < id2 else vc1 < vc2
- })
+ freshFtoVcs += freshVc.funDef -> (freshVc :: freshFtoVcs.getOrElse(freshVc.funDef, List()))
+ } else {
+ freshFtoVcs += vc.funDef -> (vc :: freshFtoVcs.getOrElse(vc.funDef, List()))
+ }
+ }
- new VerificationReport(sortedFreshVcs)
+ new VerificationReport(freshFtoVcs)
}
}