diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 221e8ddcec546ab9cf16e2ff93666cb2c4541a35..8cc1220bb2a7fc85abbf01654e34574e3f53bf78 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -35,7 +35,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
private object VRes {
trait VerificationResult
case object Valid extends VerificationResult
- case class NotValid(passing : List[Example], failing : List[Example]) extends VerificationResult
+ case class NotValid(passing : Seq[Example], failing : Seq[Example]) extends VerificationResult
}
def programSize(pgm: Program): Int = {
@@ -372,25 +372,26 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val timeoutMs = verifTimeoutMs.getOrElse(3000L)
val solver = new TimeoutSolverFactory(SolverFactory.getFromSettings(ctx, prog), timeoutMs)
val vctx = VerificationContext(ctx, prog, solver, reporter)
- val vcs = AnalysisPhase.generateVerificationConditions(vctx, Some(List(fd.id.name)))
+ val vcs = AnalysisPhase.generateVCs(vctx, Some(List(fd.id.name)))
- AnalysisPhase.checkVerificationConditions(
+ val report = AnalysisPhase.checkVCs(
vctx,
vcs,
checkInParallel = true,
- stopAfter = _.counterExample.isDefined
+ stopAfter = Some({ (vc, vr) => vr.isInvalid })
)
- val theVCs = vcs.getOrElse(fd, Nil)
-
- if(theVCs.forall{ _.value == Some(true) } ) {
+ val vrs = report.vrs
+
+ if(vrs.forall{ _._2.isValid }) {
Valid
} else {
NotValid(Nil,
- theVCs.flatMap { _.counterExample map {
- m => InExample(fd.params.map{vd => m(vd.id)})
+ vrs.collect {
+ case (_, VCResult(VCStatus.Invalid(ex), _, _)) =>
+ InExample(fd.params.map{vd => ex(vd.id)})
}
- })
+ )
}
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index bea2751115a30daaa040246047aadfb05a4c5084..47cebfd05e98c368be153873f30f9dde818da1e1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -33,7 +33,7 @@ trait SMTLIBTarget {
var out: java.io.FileWriter = _
reporter.ifDebug { debug =>
- val file = context.files.headOption.map(_.getName).getOrElse("NA")
+ val file = context.files.headOption.map(_.getName).getOrElse("NA")
val n = VCNumbers.getNext(targetName+file)
val dir = new java.io.File("vcs")
@@ -42,7 +42,7 @@ trait SMTLIBTarget {
dir.mkdir
}
- out = new java.io.FileWriter(s"vcs/$targetName-$file-$n.smt2", true)
+ out = new java.io.FileWriter(s"vcs/$targetName-$file-$n.smt2", false)
}
def id2sym(id: Identifier): SSymbol = SSymbol(id.name+"!"+id.globalId)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index f902dbe07663dcb960c52896688e68f69176eaa5..476c7f07ab6907e9636afeeee7d74eb6e7926971 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -77,8 +77,8 @@ class Synthesizer(val context : LeonContext,
val solverf = SolverFactory(() => (new FairZ3Solver(context, npr) with TimeoutSolver).setTimeout(timeoutMs))
val vctx = VerificationContext(context, npr, solverf, context.reporter)
- val vcs = generateVerificationConditions(vctx, Some(fds.map(_.id.name).toSeq))
- val vcreport = checkVerificationConditions(vctx, vcs)
+ val vcs = generateVCs(vctx, Some(fds.map(_.id.name).toSeq))
+ val vcreport = checkVCs(vctx, vcs)
if (vcreport.totalValid == vcreport.totalConditions) {
(sol, true)
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 056858e0da7e002bb0836eaad8df445f09662c51..8fe7ef69e5661c9f2b87c88f12865433c913a01b 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -21,16 +21,52 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when trying to prove a verification condition.")
)
- def generateVerificationConditions(vctx: VerificationContext, filterFuns: Option[Seq[String]]): Map[FunDef, List[VerificationCondition]] = {
+ def run(ctx: LeonContext)(program: Program): VerificationReport = {
+ var filterFuns: Option[Seq[String]] = None
+ var timeout: Option[Int] = None
+
+ val reporter = ctx.reporter
+
+ for(opt <- ctx.options) opt match {
+ case LeonValueOption("functions", ListValue(fs)) =>
+ filterFuns = Some(fs)
+
+
+ case v @ LeonValueOption("timeout", _) =>
+ timeout = v.asInt(ctx)
+
+ case _ =>
+ }
+
+ // Solvers selection and validation
+ val entrySolverFactory = SolverFactory.getFromSettings(ctx, program)
+
+ val mainSolverFactory = timeout match {
+ case Some(sec) =>
+ new TimeoutSolverFactory(entrySolverFactory, sec*1000L)
+ case None =>
+ entrySolverFactory
+ }
+
+ val vctx = VerificationContext(ctx, program, mainSolverFactory, reporter)
+
+ reporter.debug("Generating Verification Conditions...")
+
+ val vcs = generateVCs(vctx, filterFuns)
+
+ reporter.debug("Checking Verification Conditions...")
+
+ checkVCs(vctx, vcs)
+ }
+
+ def generateVCs(vctx: VerificationContext, filterFuns: Option[Seq[String]]): Seq[VC] = {
import vctx.reporter
import vctx.program
- val defaultTactic = new DefaultTactic(vctx)
+ val defaultTactic = new DefaultTactic(vctx)
val inductionTactic = new InductionTactic(vctx)
- var allVCs = Map[FunDef, List[VerificationCondition]]()
-
def excludeByDefault(fd: FunDef): Boolean = {
(fd.annotations contains "verified") || (fd.annotations contains "library")
}
@@ -43,7 +79,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val toVerify = program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
- for(funDef <- toVerify) {
+ val vcs = for(funDef <- toVerify) yield {
if (excludeByDefault(funDef)) {
reporter.warning("Forcing verification of "+funDef.id.name+" which was assumed verified")
}
@@ -56,148 +92,93 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}
if(funDef.body.isDefined) {
- val funVCs = tactic.generateVCs(funDef)
-
- allVCs += funDef -> funVCs.toList
+ tactic.generateVCs(funDef)
+ } else {
+ Nil
}
}
- allVCs
+ vcs.flatten
}
- def checkVerificationConditions(
- vctx: VerificationContext,
- vcs: Map[FunDef, List[VerificationCondition]],
+ def checkVCs(
+ vctx: VerificationContext,
+ vcs: Seq[VC],
checkInParallel: Boolean = false,
- stopAfter : VerificationCondition => Boolean = { _ => false }
- ) : VerificationReport = {
- import vctx.reporter
- import vctx.solverFactory
-
+ stopAfter: Option[(VC, VCResult) => Boolean] = None
+ ): VerificationReport = {
val interruptManager = vctx.context.interruptManager
- def checkVC(vcInfo : VerificationCondition) = {
- val funDef = vcInfo.funDef
- val vc = vcInfo.condition
-
- // Check if vc targets abstract methods
- val targets = functionCallsOf(vc).map(_.tfd.fd)
-
- val s = solverFactory.getNewSolver
- try {
-
- reporter.synchronized {
- reporter.info(s" - Now considering '${vcInfo.kind}' VC for ${funDef.id} @${vcInfo.getPos}...")
- reporter.debug("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
- reporter.debug(simplifyLets(vc).asString(vctx.context))
- reporter.debug("Solving with: " + s.name)
- }
-
- val t1 = System.nanoTime
- s.assertCnstr(Not(vc))
-
- val satResult = s.check
- val counterexample: Map[Identifier, Expr] = if (satResult == Some(true)) s.getModel else Map()
- val solverResult = satResult.map(!_)
-
- val t2 = System.nanoTime
- val dt = ((t2 - t1) / 1000000) / 1000.0
-
- reporter.synchronized {
- def title(s : String) = s" => $s"
- solverResult match {
- case _ if interruptManager.isInterrupted =>
- reporter.warning(title("CANCELLED"))
- vcInfo.time = Some(dt)
- false
-
- case None =>
- vcInfo.hasValue = true
- reporter.warning(title("UNKNOWN"))
- vcInfo.time = Some(dt)
- false
-
- case Some(true) =>
- reporter.info(title("VALID"))
-
- vcInfo.hasValue = true
- vcInfo.value = Some(true)
- vcInfo.solvedWith = Some(s)
- vcInfo.time = Some(dt)
- true
-
- case Some(false) =>
- reporter.error(title("INVALID"))
- reporter.error("Found counter-example : ")
- reporter.error(counterexample.toSeq.sortBy(_._1.name).map(p => p._1 + " -> " + p._2).mkString("\n"))
- vcInfo.hasValue = true
- vcInfo.value = Some(false)
- vcInfo.solvedWith = Some(s)
- vcInfo.counterExample = Some(counterexample)
- vcInfo.time = Some(dt)
- true
- }
- }
- } finally {
- s.free()
- }
- }
-
var stop = false
-
- if (checkInParallel) {
- val allVCsPar = (for {(_, vcs) <- vcs.toSeq; vcInfo <- vcs} yield vcInfo).par
- for (vc <- allVCsPar if !stop) {
- checkVC(vc)
+
+ val initMap: Map[VC, Option[VCResult]] = vcs.map(v => v -> None).toMap
+
+ val results = if (checkInParallel) {
+ for (vc <- vcs.par if !stop) yield {
+ val r = checkVC(vctx, vc)
if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
- stop = stopAfter(vc)
+ stop = stopAfter.map(f => f(vc, r)).getOrElse(false)
+ vc -> Some(r)
}
} else {
- for {
- (funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1.getPos < b._1.getPos)
- vc <- vcs if !interruptManager.isInterrupted && !stop
- } {
- checkVC(vc)
+ for (vc <- vcs.toSeq.sortWith((a,b) => a.fd.getPos < b.fd.getPos) if !interruptManager.isInterrupted && !stop) yield {
+ val r = checkVC(vctx, vc)
if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
- stop = stopAfter(vc)
+ stop = stopAfter.map(f => f(vc, r)).getOrElse(false)
+ vc -> Some(r)
}
}
-
- val report = new VerificationReport(vcs)
- report
+
+ VerificationReport(initMap ++ results)
}
- def run(ctx: LeonContext)(program: Program) : VerificationReport = {
- var filterFuns: Option[Seq[String]] = None
- var timeout: Option[Int] = None
+ def checkVC(vctx: VerificationContext, vc: VC): VCResult = {
+ import vctx.reporter
+ import vctx.solverFactory
- val reporter = ctx.reporter
+ val interruptManager = vctx.context.interruptManager
- for(opt <- ctx.options) opt match {
- case LeonValueOption("functions", ListValue(fs)) =>
- filterFuns = Some(fs)
+ val vcCond = vc.condition
+ val s = solverFactory.getNewSolver
- case v @ LeonValueOption("timeout", _) =>
- timeout = v.asInt(ctx)
+ 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("Solving with: " + s.name)
+ }
- case _ =>
- }
+ val tStart = System.currentTimeMillis
- // Solvers selection and validation
- val entrySolverFactory = SolverFactory.getFromSettings(ctx, program)
+ s.assertCnstr(Not(vcCond))
- val mainSolverFactory = timeout match {
- case Some(sec) =>
- new TimeoutSolverFactory(entrySolverFactory, sec*1000L)
- case None =>
- entrySolverFactory
- }
+ val satResult = s.check
- val vctx = VerificationContext(ctx, program, mainSolverFactory, reporter)
+ val dt = System.currentTimeMillis - tStart
- reporter.debug("Running verification condition generation...")
- val vcs = generateVerificationConditions(vctx, filterFuns)
- checkVerificationConditions(vctx, vcs)
+ val res = satResult match {
+ case _ if interruptManager.isInterrupted =>
+ VCResult(VCStatus.Cancelled, Some(s), Some(dt))
+
+ case None =>
+ VCResult(VCStatus.Unknown, Some(s), Some(dt))
+
+ case Some(false) =>
+ VCResult(VCStatus.Valid, Some(s), Some(dt))
+
+ case Some(true) =>
+ VCResult(VCStatus.Invalid(s.getModel), Some(s), Some(dt))
+ }
+
+ reporter.synchronized {
+ res.report(vctx)
+ }
+
+ res
+
+ } finally {
+ s.free()
+ }
}
}
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 06b35faddb3beb47ca35542a175bb1bfd72a87e1..e58cdc54668f4a367b34895be473f6155d55423c 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -10,20 +10,19 @@ import purescala.Constructors._
class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
val description = "Default verification condition generation approach"
- override val shortDescription = "default"
- def generatePostconditions(fd: FunDef): Seq[VerificationCondition] = {
+ def generatePostconditions(fd: FunDef): Seq[VC] = {
(fd.postcondition, fd.body) match {
case (Some(post), Some(body)) =>
val vc = implies(precOrTrue(fd), application(post, Seq(body)))
- Seq(new VerificationCondition(vc, fd, VCPostcondition, this).setPos(post))
+ Seq(VC(vc, fd, VCKinds.Postcondition, this).setPos(post))
case _ =>
Nil
}
}
- def generatePreconditions(fd: FunDef): Seq[VerificationCondition] = {
+ def generatePreconditions(fd: FunDef): Seq[VC] = {
fd.body match {
case Some(body) =>
val calls = collectWithPC {
@@ -35,7 +34,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
val pre2 = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, pre)
val vc = implies(and(precOrTrue(fd), path), pre2)
- new VerificationCondition(vc, fd, VCPrecondition, this).setPos(fi)
+ VC(vc, fd, VCKinds.Precondition, this).setPos(fi)
}
case None =>
@@ -43,36 +42,36 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
}
}
- def generateCorrectnessConditions(fd: FunDef): Seq[VerificationCondition] = {
+ def generateCorrectnessConditions(fd: FunDef): Seq[VC] = {
fd.body match {
case Some(body) =>
val calls = collectWithPC {
case e @ Error(_, "Match is non-exhaustive") =>
- (e, VCExhaustiveMatch, BooleanLiteral(false))
+ (e, VCKinds.ExhaustiveMatch, BooleanLiteral(false))
case e @ Error(_, _) =>
- (e, VCAssert, BooleanLiteral(false))
+ (e, VCKinds.Assert, BooleanLiteral(false))
case a @ Assert(cond, Some(err), _) =>
val kind = if (err.startsWith("Map ")) {
- VCMapUsage
+ VCKinds.MapUsage
} else if (err.startsWith("Array ")) {
- VCArrayUsage
+ VCKinds.ArrayUsage
} else {
- VCAssert
+ VCKinds.Assert
}
(a, kind, cond)
- case a @ Assert(cond, None, _) => (a, VCAssert, cond)
+ case a @ Assert(cond, None, _) => (a, VCKinds.Assert, cond)
// Only triggered for inner ensurings, general postconditions are handled by generatePostconditions
- case a @ Ensuring(body, post) => (a, VCAssert, application(post, Seq(body)))
+ case a @ Ensuring(body, post) => (a, VCKinds.Assert, application(post, Seq(body)))
}(body)
calls.map {
case ((e, kind, errorCond), path) =>
val vc = implies(and(precOrTrue(fd), path), errorCond)
- new VerificationCondition(vc, fd, kind, this).setPos(e)
+ VC(vc, fd, kind, this).setPos(e)
}
case None =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 4420428a78c00893ba33881ff8f4783bd66e208b..21efc5453e12d4f25465ae2fa1273357321e83d0 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -11,7 +11,6 @@ import purescala.Constructors._
class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
override val description = "Induction tactic for suitable functions"
- override val shortDescription = "induction"
val reporter = vctx.reporter
@@ -28,7 +27,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
}
}
- override def generatePostconditions(fd: FunDef): Seq[VerificationCondition] = {
+ override def generatePostconditions(fd: FunDef): Seq[VC] = {
(fd.body, firstAbsClassDef(fd.params), fd.postcondition) match {
case (Some(body), Some((parentType, arg)), Some(post)) =>
for (cct <- parentType.knownCCDescendents) yield {
@@ -45,7 +44,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
implies(andJoin(subCases), application(post, Seq(body)))
)
- new VerificationCondition(vc, fd, VCPostcondition, this).setPos(fd)
+ VC(vc, fd, VCKinds.Info(VCKinds.Postcondition, s"ind. on ${arg.id} / ${cct.classDef.id}"), this).setPos(fd)
}
case (body, _, post) =>
@@ -56,7 +55,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
}
}
- override def generatePreconditions(fd: FunDef): Seq[VerificationCondition] = {
+ override def generatePreconditions(fd: FunDef): Seq[VC] = {
(fd.body, firstAbsClassDef(fd.params)) match {
case (Some(b), Some((parentType, arg))) =>
val body = b
@@ -78,7 +77,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
val vc = implies(and(CaseClassInstanceOf(cct, arg.toVariable), precOrTrue(fd), path), implies(andJoin(subCases), replace((tfd.params.map(_.toVariable) zip args).toMap, pre)))
- new VerificationCondition(vc, fd, VCPrecondition, this).setPos(fi)
+ VC(vc, fd, VCKinds.Info(VCKinds.Precondition, "ind. on $arg / ${cct.classDef.id}"), this).setPos(fi)
}
}
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 92bf550b4397d08338c1701e50531240e759230e..d6f955257530fd153649ba96862a48553748b186 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -9,9 +9,8 @@ import purescala.ExprOps._
abstract class Tactic(vctx: VerificationContext) {
val description : String
- val shortDescription : String
- def generateVCs(fdUnsafe: FunDef): Seq[VerificationCondition] = {
+ def generateVCs(fdUnsafe: FunDef): Seq[VC] = {
val fd = fdUnsafe.duplicate
fd.fullBody = matchToIfThenElse(fd.fullBody)
generatePostconditions(fd) ++
@@ -19,10 +18,9 @@ abstract class Tactic(vctx: VerificationContext) {
generateCorrectnessConditions(fd)
}
- def generatePostconditions(function: FunDef): Seq[VerificationCondition]
- def generatePreconditions(function: FunDef): Seq[VerificationCondition]
- def generateCorrectnessConditions(function: FunDef): Seq[VerificationCondition]
-
+ def generatePostconditions(function: FunDef): Seq[VC]
+ def generatePreconditions(function: FunDef): Seq[VC]
+ def generateCorrectnessConditions(function: FunDef): Seq[VC]
// Helper functions
protected def precOrTrue(fd: FunDef): Expr = fd.precondition match {
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index e174830946f07b16113f62bb37ac6a6a2872f275..75618fbbaca4ea436d922a966465e243d1f39883 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -10,45 +10,75 @@ import leon.utils.Positioned
import leon.solvers._
/** This is just to hold some history information. */
-class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind, val tactic: Tactic, val info: String = "") extends Positioned {
- // None = still unknown
- // Some(true) = valid
- // Some(false) = invalid
- var hasValue = false
- var value : Option[Boolean] = None
- var solvedWith : Option[Solver] = None
- var time : Option[Double] = None
- var counterExample : Option[Map[Identifier, Expr]] = None
-
- def status : String = value match {
- case None => "unknown"
- case Some(true) => "valid"
- case Some(false) => "invalid"
+case class VC(condition: Expr, fd: FunDef, kind: VCKind, tactic: Tactic) extends Positioned {
+ override def toString = {
+ fd.id.name +" - " +kind.toString
}
+}
- def tacticStr = tactic.shortDescription match {
- case "default" => ""
- case s => s
- }
+abstract class VCKind(val name: String, val abbrv: String) {
+ override def toString = name
- def solverStr = solvedWith match {
- case Some(s) => s.name
- case None => ""
- }
+ def underlying = this
+}
- override def toString = {
- kind.toString + " in function " + funDef.id.name + "\n" +
- condition.toString
+object VCKinds {
+ case class Info(k: VCKind, info: String) extends VCKind(k.abbrv+" ("+info+")", k.abbrv) {
+ override def underlying = k
}
+ case object Precondition extends VCKind("precondition", "precond.")
+ case object Postcondition extends VCKind("postcondition", "postcond.")
+ case object Assert extends VCKind("body assertion", "assert.")
+ case object ExhaustiveMatch extends VCKind("match exhaustiveness", "match.")
+ case object MapUsage extends VCKind("map usage", "map use")
+ case object ArrayUsage extends VCKind("array usage", "arr. use")
}
-abstract class VCKind(val name: String, val abbrv: String) {
+case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option[Long]) {
+ def isValid = status == VCStatus.Valid
+ def isInvalid = status.isInstanceOf[VCStatus.Invalid]
+ def isInconclusive = !isValid && !isInvalid
+
+ def report(vctx: VerificationContext) {
+ import vctx.reporter
+ import vctx.context
+
+ status match {
+ case VCStatus.Valid =>
+ reporter.info(" => VALID")
+
+ case VCStatus.Invalid(cex) =>
+ reporter.error(" => INVALID")
+ reporter.error("Found counter-example:")
+
+ val strings = cex.toSeq.sortBy(_._1.name).map {
+ case (id, v) => (id.asString(context), v.asString(context))
+ }
+
+ if (strings.nonEmpty) {
+ val max = strings.map(_._1.size).max
+
+ for ((id, v) <- strings) {
+ reporter.error((" %-"+max+"s -> %s").format(id, v))
+ }
+ } else {
+ reporter.error(f" (Empty counter-example)")
+ }
+ case _ =>
+ reporter.warning(" => "+status.name.toUpperCase)
+ }
+ }
+}
+
+sealed abstract class VCStatus(val name: String) {
override def toString = name
}
-case object VCPrecondition extends VCKind("precondition", "precond.")
-case object VCPostcondition extends VCKind("postcondition", "postcond.")
-case object VCAssert extends VCKind("body assertion", "assert.")
-case object VCExhaustiveMatch extends VCKind("match exhaustiveness", "match.")
-case object VCMapUsage extends VCKind("map usage", "map use")
-case object VCArrayUsage extends VCKind("array usage", "arr. use")
+
+object VCStatus {
+ case class Invalid(cex: Map[Identifier, Expr]) extends VCStatus("invalid")
+ case object Valid extends VCStatus("valid")
+ case object Unknown extends VCStatus("unknown")
+ case object Timeout extends VCStatus("timeout")
+ case object Cancelled extends VCStatus("cancelled")
+}
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 2683ff2509cd401f3803b12bf628e27f03d3df2e..8db22ff699d58b79fda144303f28761eeda07acb 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -3,36 +3,39 @@
package leon
package verification
+import VCKinds._
+import VCStatus._
+
import purescala.Definitions.FunDef
-class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
+case class VerificationReport(val results: Map[VC, Option[VCResult]]) {
import scala.math.Ordering.Implicits._
- val conditions : Seq[VerificationCondition] = fvcs.flatMap(_._2).toSeq.sortBy(vc => (vc.funDef.id.name, vc.kind.toString))
-
- lazy val totalConditions : Int = conditions.size
- lazy val totalTime : Double = conditions.foldLeft(0.0d)((t,c) => t + c.time.getOrElse(0.0d))
+ val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {
+ case (vc, or) => (vc, or.getOrElse(VCResult(Unknown, None, None)))
+ }
- lazy val totalValid : Int = conditions.count(_.value == Some(true))
+ lazy val totalConditions : Int = vrs.size
- lazy val totalInvalid : Int = conditions.count(_.value == Some(false))
+ lazy val totalTime: Long = vrs.map(_._2.timeMs.getOrElse(0l)).sum
- lazy val totalUnknown : Int = conditions.count(_.value == None)
+ lazy val totalValid: Int = vrs.count(_._2.isValid)
+ lazy val totalInvalid: Int = vrs.count(_._2.isInvalid)
+ lazy val totalUnknown: Int = vrs.count(_._2.isInconclusive)
def summaryString : String = if(totalConditions >= 0) {
import utils.ASCIIHelpers._
var t = Table("Verification Summary")
- t ++= conditions.map { vc =>
- val timeStr = vc.time.map(t => f"$t%-3.3f").getOrElse("")
+ t ++= vrs.map { case (vc, vr) =>
+ val timeStr = vr.timeMs.map(t => f"${t/1000d}%-3.3f").getOrElse("")
Row(Seq(
- Cell(vc.funDef.id.toString),
+ Cell(vc.fd.id.toString),
Cell(vc.kind.name),
Cell(vc.getPos),
- Cell(vc.status),
- Cell(vc.tacticStr),
- Cell(vc.solverStr),
+ Cell(vr.status),
+ Cell(vr.solvedWith.map(_.name).getOrElse("")),
Cell(timeStr, align = Right)
))
}
@@ -40,8 +43,8 @@ class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
t += Separator
t += Row(Seq(
- Cell(f"total: $totalConditions%-4d valid: $totalValid%-4d invalid: $totalInvalid%-4d unknown $totalUnknown%-4d", 6),
- Cell(f"$totalTime%7.3f", align = Right)
+ Cell(f"total: $totalConditions%-4d valid: $totalValid%-4d invalid: $totalInvalid%-4d unknown $totalUnknown%-4d", 5),
+ Cell(f"${totalTime/1000d}%7.3f", align = Right)
))
t.render
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 2198605ee66d800f2b09a3ed5c6acb6992fa5a21..75b16415530a8686c582fa9b08d1ba9b4553a9ad 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -11,8 +11,10 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
val name = "xlang analysis"
val description = "apply analysis on xlang"
- case object VCInvariantPost extends VCKind("invariant postcondition", "inv. post.")
- case object VCInvariantInd extends VCKind("invariant inductive", "inv. ind.")
+ object VCXLangKinds {
+ case object InvariantPost extends VCKind("invariant postcondition", "inv. post.")
+ case object InvariantInd extends VCKind("invariant inductive", "inv. ind.")
+ }
def run(ctx: LeonContext)(pgm: Program): VerificationReport = {
@@ -59,34 +61,34 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
}
def completeVerificationReport(vr: VerificationReport, functionWasLoop: FunDef => Boolean): VerificationReport = {
- val vcs = vr.conditions
//this is enough to convert invariant postcondition and inductive conditions. However the initial validity
//of the invariant (before entering the loop) will still appear as a regular function precondition
//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
- var freshFtoVcs = Map[FunDef, List[VerificationCondition]]()
-
- for (vc <- vcs) {
- val funDef = vc.funDef
- if(functionWasLoop(funDef)) {
- val freshVc = new VerificationCondition(
- vc.condition,
- funDef.owner match { case Some(fd : FunDef) => fd; case _ => funDef },
- if(vc.kind == VCPostcondition) VCInvariantPost else if(vc.kind == VCPrecondition) VCInvariantInd else vc.kind,
- vc.tactic,
- vc.info).setPos(funDef)
- freshVc.value = vc.value
- freshVc.solvedWith = vc.solvedWith
- freshVc.time = vc.time
- freshFtoVcs += freshVc.funDef -> (freshVc :: freshFtoVcs.getOrElse(freshVc.funDef, List()))
+
+ val newResults = for ((vc, ovr) <- vr.results) yield {
+ if(functionWasLoop(vc.fd)) {
+ val nvc = VC(vc.condition,
+ vc.fd.owner match {
+ case Some(fd: FunDef) => fd
+ case _ => vc.fd
+ },
+ vc.kind.underlying match {
+ case VCKinds.Postcondition => VCXLangKinds.InvariantPost
+ case VCKinds.Precondition => VCXLangKinds.InvariantInd
+ case _ => vc.kind
+ },
+ vc.tactic)
+
+ nvc -> ovr
} else {
- freshFtoVcs += vc.funDef -> (vc :: freshFtoVcs.getOrElse(vc.funDef, List()))
+ vc -> ovr
}
}
- new VerificationReport(freshFtoVcs)
+ VerificationReport(newResults)
}
}
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 55902fa9e6e0a863c6fa6ef49443e2b56cd14d84..bc1f0257739b9550dfc50a5eddcb199299bc9f71 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -45,8 +45,8 @@ class PureScalaVerificationRegression extends VerificationRegression {
forEachFileIn("valid") { output =>
val Output(report, reporter) = output
- for (vc <- report.conditions) {
- if (vc.value != Some(true)) {
+ for ((vc, vr) <- report.vrs) {
+ if (!vr.isValid) {
fail("The following verification condition was invalid: " + vc.toString + " @" + vc.getPos)
}
}