Decouple the validation, group VCs per functions

Decoupling the validation phase allows the web-interface to interract in
a much easier way.

Grouping VCs per functions makes the verification overview easier.

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

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

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

src/main/scala/leon/verification/VerificationContext.scala

+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)
+)

src/main/scala/leon/verification/VerificationReport.scala

-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) {

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)
   }
 
 }