diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala index a61e24cef6c9f674c6ba0e3c2a25dc7d45f05f7c..7e831fb124b01c2d8fe306dae2ba33f3f7d14778 100644 --- a/src/purescala/Analysis.scala +++ b/src/purescala/Analysis.scala @@ -17,6 +17,14 @@ class Analysis(val program: Program) { val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions val solverExtensions: Seq[Solver] = loadedSolverExtensions + val trivialSolver = new Solver(reporter) { + val description = "Trivial" + override val shortDescription = "trivial" + def solve(e: Expr) = throw new Exception("trivial solver should not be called.") + } + + val defaultTactic = new DefaultTactic(reporter) + // Calling this method will run all analyses on the program passed at // construction time. If at least one solver is loaded, verification // conditions are generated and passed to all solvers. Otherwise, only the @@ -35,7 +43,8 @@ class Analysis(val program: Program) { def checkVerificationConditions : Unit = { // just for the summary: - var verifiedVCs: List[(String,String,String,String,String)] = Nil + var verificationConditionInfos: List[VerificationCondition] = Nil + var analysedFunctions: MutableSet[String] = MutableSet.empty solverExtensions.foreach(_.setProgram(program)) @@ -44,11 +53,18 @@ class Analysis(val program: Program) { analysedFunctions += funDef.id.name if(funDef.body.isDefined) { val vc = postconditionVC(funDef) + val vcInfo = new VerificationCondition(vc, funDef, VCKind.Postcondition, defaultTactic) + verificationConditionInfos = vcInfo :: verificationConditionInfos + if(vc == BooleanLiteral(false)) { - verifiedVCs = (funDef.id.toString, "postcondition", "invalid", "trivial", "--") :: verifiedVCs + vcInfo.value = Some(false) + vcInfo.solvedWith = Some(trivialSolver) + vcInfo.time = Some(0L) } else if(vc == BooleanLiteral(true)) { if(funDef.hasPostcondition) { - verifiedVCs = (funDef.id.toString, "postcondition", "valid", "tautology", "--") :: verifiedVCs + vcInfo.value = Some(true) + vcInfo.solvedWith = Some(trivialSolver) + vcInfo.time = Some(0L) } } else { reporter.info("Verification condition (post) for ==== " + funDef.id + " ====") @@ -57,11 +73,6 @@ class Analysis(val program: Program) { } else { reporter.info("(not showing unrolled VCs)") } - // reporter.info("Negated:") - // reporter.info(negate(vc)) - // reporter.info("Negated, expanded:") - // val exp = expandLets(negate(vc)) - // reporter.info(exp) // try all solvers until one returns a meaningful answer var superseeded : Set[String] = Set.empty[String] @@ -82,12 +93,20 @@ class Analysis(val program: Program) { case None => false case Some(true) => { reporter.info("==== VALID ====") - verifiedVCs = (funDef.id.toString, "postcondition", "valid", se.shortDescription, dt + "s.") :: verifiedVCs + + vcInfo.value = Some(true) + vcInfo.solvedWith = Some(se) + vcInfo.time = Some(dt) + true } case Some(false) => { reporter.error("==== INVALID ====") - verifiedVCs = (funDef.id.toString, "postcondition", "invalid", se.shortDescription, dt + "s.") :: verifiedVCs + + vcInfo.value = Some(false) + vcInfo.solvedWith = Some(se) + vcInfo.time = Some(dt) + true } } @@ -95,7 +114,6 @@ class Analysis(val program: Program) { }) match { case None => { reporter.warning("No solver could prove or disprove the verification condition.") - verifiedVCs = (funDef.id.toString, "postcondition", "unknown", "--", "--") :: verifiedVCs } case _ => } @@ -103,27 +121,18 @@ class Analysis(val program: Program) { } else { if(funDef.postcondition.isDefined) { reporter.warning(funDef, "Could not verify postcondition: function implementation is unknown.") - verifiedVCs = (funDef.id.toString, "postcondition", "unknown", "no body", "--") :: verifiedVCs } } } - if(verifiedVCs.size > 0) { - verifiedVCs = verifiedVCs.reverse - val col1wdth = verifiedVCs.map(_._1).map(_.length).max + 2 - val col2wdth = verifiedVCs.map(_._2).map(_.length).max + 2 - val col3wdth = verifiedVCs.map(_._3).map(_.length).max + 2 - val col4wdth = verifiedVCs.map(_._4).map(_.length).max + 2 - val col5wdth = verifiedVCs.map(_._5).map(_.length).max - def mk1line(line: (String,String,String,String,String)) : String = { - line._1 + (" " * (col1wdth - line._1.length)) + - line._2 + (" " * (col2wdth - line._2.length)) + - line._3 + (" " * (col3wdth - line._3.length)) + - line._4 + (" " * (col4wdth - line._4.length)) + - line._5 - } - val dashes : String = "=" * (col1wdth + col2wdth + col3wdth + col4wdth + col5wdth) - reporter.info("Summary:\n" + dashes + "\n" + verifiedVCs.sortWith(_._1 < _._1).map(mk1line(_)).mkString("\n") + "\n" + dashes) + if(verificationConditionInfos.size > 0) { + verificationConditionInfos = verificationConditionInfos.reverse + val summaryString = ( + VerificationCondition.infoHeader + + verificationConditionInfos.map(_.infoLine).mkString("\n", "\n", "\n") + + VerificationCondition.infoFooter + ) + reporter.info(summaryString) } else { reporter.info("No verification conditions were generated.") } diff --git a/src/purescala/DefaultTactic.scala b/src/purescala/DefaultTactic.scala new file mode 100644 index 0000000000000000000000000000000000000000..da2ca6b950b2253add3ec1d94519f3521445ffd4 --- /dev/null +++ b/src/purescala/DefaultTactic.scala @@ -0,0 +1,26 @@ +package purescala + +import purescala.Trees._ +import purescala.Definitions._ +import Extensions.Tactic + +class DefaultTactic(reporter: Reporter) extends Tactic(reporter) { + val description = "Default verification condition generation approach" + override val shortDescription = "default" + + def generatePostconditions(function: FunDef) : Seq[Expr] = { + Seq.empty + } + + def generatePreconditions(function: FunDef) : Seq[Expr] = { + Seq.empty + } + + def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[Expr] = { + Seq.empty + } + + def generateMiscCorrectnessConditions(function: FunDef) : Seq[Expr] = { + Seq.empty + } +} diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala index 791e0e7d4abb511a87f73a7d860359caf00bbae6..72447b2074f3b01a04ff2756c4cc2a4b2b702f6b 100644 --- a/src/purescala/Extensions.scala +++ b/src/purescala/Extensions.scala @@ -32,6 +32,8 @@ object Extensions { abstract class Tactic(reporter: Reporter) extends Extension(reporter) { def generatePostconditions(function: FunDef) : Seq[Expr] def generatePreconditions(function: FunDef) : Seq[Expr] + def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[Expr] + def generateMiscCorrectnessConditions(function: FunDef) : Seq[Expr] } // The rest of the code is for dynamically loading extensions diff --git a/src/purescala/VerificationCondition.scala b/src/purescala/VerificationCondition.scala new file mode 100644 index 0000000000000000000000000000000000000000..7222e5086cb1e05779f634cc9a4d4c2453141ea8 --- /dev/null +++ b/src/purescala/VerificationCondition.scala @@ -0,0 +1,48 @@ +package purescala + +import purescala.Extensions._ +import purescala.Trees._ +import purescala.Definitions._ + +/** This is just to hold some history information. */ +class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind.Value, val tactic: Tactic, val info: String = "") { + // None = still unknown + // Some(true) = valid + // Some(false) = valid + var value : Option[Boolean] = None + var solvedWith : Option[Solver] = None + var time : Option[Double] = None + + def status : String = value match { + case None => "unknown" + case Some(true) => "valid" + case Some(false) => "invalid" + } + + private def tacticStr = tactic.shortDescription match { + case "default" => "" + case s => s + } + + private 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 = { + "║ %-15s %-10s %-8s %-10s %-10s %7s ║" format (funDef.id.toString, kind, status, tacticStr, solverStr, timeStr) + } +} + +object VerificationCondition { + val infoFooter : String = "╚" + ("═" * 67) + "╝" + val infoHeader : String = "╔══ Summary " + ("═" * 56) + "╗" +} + +object VCKind extends Enumeration { + val Precondition = Value("precond.") + val Postcondition = Value("postcond.") + val ExhaustiveMatch = Value("match.") +}