From 013b8843d5d46e596bd1b135b4a8c2c9fea84faf Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 26 Oct 2012 22:58:13 +0200
Subject: [PATCH] Analysis/Verification now returns a report.
---
src/main/scala/leon/Reporter.scala | 5 +-
src/main/scala/leon/Settings.scala | 1 -
.../scala/leon/plugin/AnalysisComponent.scala | 3 -
src/main/scala/leon/plugin/LeonPlugin.scala | 1 -
.../scala/leon/verification/Analysis.scala | 83 ++-----------------
.../verification/VerificationCondition.scala | 16 +---
.../verification/VerificationReport.scala | 47 ++++++++++-
src/test/scala/leon/test/ValidPrograms.scala | 3 +-
8 files changed, 59 insertions(+), 100 deletions(-)
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 03512770f..814c4352a 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -27,10 +27,7 @@ class DefaultReporter extends Reporter {
protected val infoPfx = "[ Info ] "
protected val fatalPfx = "[ Fatal ] "
- def output(msg: String) : Unit = {
- if(!Settings.simpleOutput)
- println(msg)
- }
+ def output(msg: String) : Unit = println(msg)
protected def reline(pfx: String, msg: String) : String = {
val color = if(pfx == errorPfx || pfx == warningPfx || pfx == fatalPfx) {
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index f4ff31f49..04ed6bc41 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -26,7 +26,6 @@ object Settings {
var bitvectorBitwidth : Option[Int] = None
var debugLevel: Int = 0
var debugTags: Set[String] = Set.empty
- var simpleOutput: Boolean = false
var synthesis: Boolean = false
var transformProgram: Boolean = true
var stopAfterExtraction: Boolean = false
diff --git a/src/main/scala/leon/plugin/AnalysisComponent.scala b/src/main/scala/leon/plugin/AnalysisComponent.scala
index 77c058a6f..1cc1cde07 100644
--- a/src/main/scala/leon/plugin/AnalysisComponent.scala
+++ b/src/main/scala/leon/plugin/AnalysisComponent.scala
@@ -24,10 +24,7 @@ class AnalysisComponent(val global: Global, val pluginInstance: LeonPlugin)
protected def stopIfErrors: Unit = {
if(reporter.hasErrors) {
- if(Settings.simpleOutput)
- println("error")
sys.exit(1)
- //throw new Exception("There were errors.")
}
}
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index 13542da33..afc5fa35d 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -63,7 +63,6 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
case "cores" => leon.Settings.useCores = true
case "quickcheck" => leon.Settings.useQuickCheck = true
case "parallel" => leon.Settings.useParallel = true
- case "oneline" => leon.Settings.simpleOutput = true
case "noLuckyTests" => leon.Settings.luckyTest = false
case "noverifymodel" => leon.Settings.verifyModel = false
case "imperative" => leon.Settings.synthesis = false;
diff --git a/src/main/scala/leon/verification/Analysis.scala b/src/main/scala/leon/verification/Analysis.scala
index b6786f30c..1521ad8e1 100644
--- a/src/main/scala/leon/verification/Analysis.scala
+++ b/src/main/scala/leon/verification/Analysis.scala
@@ -40,13 +40,12 @@ class Analysis(val program : Program, val reporter: Reporter) {
FunctionTemplate.mkTemplate(funDef)
}
- if(solverExtensions.size > 1) {
+ val report = if(solverExtensions.size > 1) {
reporter.info("Running verification condition generation...")
-
- val list = generateVerificationConditions
- checkVerificationConditions(list : _*)
+ checkVerificationConditions(generateVerificationConditions)
} else {
reporter.warning("No solver specified. Cannot test verification conditions.")
+ VerificationReport.emptyReport
}
analysisExtensions.foreach(ae => {
@@ -54,7 +53,7 @@ class Analysis(val program : Program, val reporter: Reporter) {
ae.analyse(program)
})
- new VerificationReport
+ report
}
private def generateVerificationConditions : List[VerificationCondition] = {
@@ -91,8 +90,7 @@ class Analysis(val program : Program, val reporter: Reporter) {
allVCs.toList
}
- def checkVerificationCondition(vc: VerificationCondition) : Unit = checkVerificationConditions(vc)
- def checkVerificationConditions(vcs: VerificationCondition*) : Unit = {
+ private def checkVerificationConditions(vcs: Seq[VerificationCondition]) : VerificationReport = {
for(vcInfo <- vcs) {
val funDef = vcInfo.funDef
val vc = vcInfo.condition
@@ -152,73 +150,8 @@ class Analysis(val program : Program, val reporter: Reporter) {
}
- if(vcs.size > 0) {
- val summaryString = (
- VerificationCondition.infoHeader +
- vcs.map(_.infoLine).mkString("\n", "\n", "\n") +
- VerificationCondition.infoFooter
- )
- reporter.info(summaryString)
-
- if(Settings.simpleOutput) {
- val outStr =
- if(vcs.forall(_.status == "valid")) "valid"
- else if(vcs.exists(_.status == "invalid")) "invalid"
- else "unknown"
- println(outStr)
- }
-
- // Printing summary for the evaluation section of paper:
- val writeSummary = false
- if (writeSummary) {
- def writeToFile(filename: String, content: String) : Unit = {
- try {
- val fw = new java.io.FileWriter(filename)
- fw.write(content)
- fw.close
- } catch {
- case e => reporter.error("There was an error while generating the test file" + filename)
- }
- }
-
- var toWrite: String = ""
- val functionVCs = vcs groupBy (_.funDef)
- val vcsByPostcond = functionVCs groupBy
- (_._2 exists ((vc: VerificationCondition) => vc.kind == VCKind.Postcondition))
- def functionInfoLine(id: String, funVCs: Traversable[VerificationCondition]) = {
- val vcsByKind = funVCs groupBy (_.kind)
- val nbPrecond = vcsByKind.get(VCKind.Precondition).getOrElse(Nil).size
- val nbMatch = vcsByKind.get(VCKind.ExhaustiveMatch).getOrElse(Nil).size
- val totalTime =
- (funVCs.foldLeft(0.0)((a, b) => a + b.time.getOrElse(0.0)))
- val validStr = "ok"
- val invalidStr = "err"
- val status = if (funVCs.forall(_.status == "valid")) validStr else invalidStr
- val timeStr = if (totalTime < 0.01) "< 0.01" else ("%-3.2f" format totalTime)
-
- val toRet =
- "%-25s %-3s %-3s %-9s %6s" format (id, nbPrecond, nbMatch, status, timeStr)
- toRet
- }
- for ((withPostcond, functionsByPostcond) <- vcsByPostcond) {
- if (withPostcond)
- toWrite += "with postcondition:\n"
- else
- toWrite += "without postcondition:\n"
- for ((funDef, funVCs) <- functionsByPostcond.toList.sortWith((p1, p2) => p1._1 < p2._1)) {
- toWrite += functionInfoLine(funDef.id.toString, funVCs) + "\n"
- }
- }
-
- val fileName = program.mainObject.id.toString + "-evaluation.txt"
- val folderName = "summary"
-
- new java.io.File(folderName).mkdir()
-
- writeToFile(folderName + "/" + fileName, toWrite)
- }
- } else {
- reporter.info("No verification conditions were analyzed.")
- }
+ val report = new VerificationReport(vcs)
+ reporter.info(report.summaryString)
+ report
}
}
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index ac972d50c..217eb94b7 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -21,28 +21,16 @@ class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: V
case Some(false) => "invalid"
}
- private def tacticStr = tactic.shortDescription match {
+ def tacticStr = tactic.shortDescription match {
case "default" => ""
case s => s
}
- private def solverStr = solvedWith match {
+ def solverStr = solvedWith match {
case Some(s) => s.shortDescription
case None => ""
}
- private def timeStr = time.map(t => "%-3.3f".format(t)).getOrElse("")
-
- def infoLine : String = {
- "║ %-25s %-9s %9s %-8s %-10s %-7s %7s ║" format (funDef.id.toString, kind, posInfo, status, tacticStr, solverStr, timeStr)
- }
-}
-
-object VerificationCondition {
- val infoFooter : String = "╚" + ("═" * 83) + "╝"
- val infoHeader : String = ". ┌─────────┐\n" +
- "╔═╡ Summary ╞" + ("═" * 71) + "╗\n" +
- "║ └─────────┘" + (" " * 71) + "║"
}
object VCKind extends Enumeration {
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 2b82dfcee..16b651624 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -1,3 +1,48 @@
package leon.verification
-class VerificationReport
+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))
+
+ lazy val totalValid : Int = conditions.count(_.value == Some(true))
+
+ lazy val totalInvalid : Int = conditions.count(_.value == Some(false))
+
+ lazy val totalUnknown : Int = conditions.count(_.value == None)
+
+ def summaryString : String = if(totalConditions >= 0) {
+ VerificationReport.infoHeader +
+ conditions.map(VerificationReport.infoLine).mkString("\n", "\n", "\n") +
+ VerificationReport.infoSep +
+ ("║ total: %-4d valid: %-4d invalid: %-4d unknown %-4d " +
+ (" " * 18) +
+ " %-3.3f ║\n").format(totalConditions, totalValid, totalInvalid, totalUnknown, totalTime) +
+ VerificationReport.infoFooter
+ } else {
+ "No verification conditions were analyzed."
+ }
+}
+
+object VerificationReport {
+ def emptyReport : VerificationReport = new VerificationReport(Nil)
+
+ private val infoSep : String = "╟" + ("┄" * 83) + "╢\n"
+ private val infoFooter : String = "╚" + ("═" * 83) + "╝"
+ private val infoHeader : String = ". ┌─────────┐\n" +
+ "╔═╡ Summary ╞" + ("═" * 71) + "╗\n" +
+ "║ └─────────┘" + (" " * 71) + "║"
+
+ private def infoLine(vc : VerificationCondition) : String = {
+ val timeStr = vc.time.map(t => "%-3.3f".format(t)).getOrElse("")
+
+ "║ %-25s %-9s %9s %-8s %-10s %-7s %7s ║".format(
+ vc.funDef.id.toString,
+ vc.kind,
+ vc.posInfo,
+ vc.status,
+ vc.tacticStr,
+ vc.solverStr,
+ timeStr)
+ }
+}
diff --git a/src/test/scala/leon/test/ValidPrograms.scala b/src/test/scala/leon/test/ValidPrograms.scala
index 426e78fb2..37df60f22 100644
--- a/src/test/scala/leon/test/ValidPrograms.scala
+++ b/src/test/scala/leon/test/ValidPrograms.scala
@@ -43,5 +43,6 @@ class ValidPrograms extends FunSuite {
}
}
- mkTest("/home/psuter/Test.scala")
+ // Sorry for leaving this there...
+ // mkTest("/home/psuter/Test.scala")
}
--
GitLab