diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
deleted file mode 100644
index e1fc9fb1f3fa155bc194433c2948a7fb2b1a34c0..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/Analysis.scala
+++ /dev/null
@@ -1,343 +0,0 @@
-package leon
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-
-import Extensions._
-
-import solvers.TrivialSolver
-
-import scala.collection.mutable.{Set => MutableSet}
-
-class Analysis(val program : Program, val reporter: Reporter = Settings.reporter) {
- Extensions.loadAll(reporter)
-
- val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
-
- val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D
-
- val solverExtensions: Seq[Solver] = trivialSolver +: loadedSolverExtensions
-
- solverExtensions.foreach(_.setProgram(program))
-
- val defaultTactic = new DefaultTactic(reporter)
- defaultTactic.setProgram(program)
- val inductionTactic = new InductionTactic(reporter)
- inductionTactic.setProgram(program)
-
- // 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
- // Analysis extensions are run on the program.
- def analyse : Unit = {
- // We generate all function templates in advance.
- for(funDef <- program.definedFunctions if funDef.hasImplementation) {
- // this gets cached :D
- FunctionTemplate.mkTemplate(funDef)
- }
-
- if(solverExtensions.size > 1) {
- reporter.info("Running verification condition generation...")
-
- val list = generateVerificationConditions
- checkVerificationConditions(list : _*)
- } else {
- reporter.warning("No solver specified. Cannot test verification conditions.")
- }
-
- analysisExtensions.foreach(ae => {
- reporter.info("Running analysis from extension: " + ae.description)
- ae.analyse(program)
- })
- }
-
- private def generateVerificationConditions : List[VerificationCondition] = {
- var allVCs: Seq[VerificationCondition] = Seq.empty
- val analysedFunctions: MutableSet[String] = MutableSet.empty
-
- for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1 < fd2) if (Settings.functionsToAnalyse.isEmpty || Settings.functionsToAnalyse.contains(funDef.id.name))) {
- analysedFunctions += funDef.id.name
-
- val tactic: Tactic =
- if(funDef.annotations.contains("induct")) {
- inductionTactic
- } else {
- defaultTactic
- }
-
- if(funDef.body.isDefined) {
- allVCs ++= tactic.generatePreconditions(funDef)
- allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
- allVCs ++= tactic.generatePostconditions(funDef)
- allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
- allVCs ++= tactic.generateArrayAccessChecks(funDef)
- }
- 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: Set[String] = Settings.functionsToAnalyse -- analysedFunctions
- notFound.foreach(fn => reporter.error("Did not find function \"" + fn + "\" though it was marked for analysis."))
-
- allVCs.toList
- }
-
- def checkVerificationCondition(vc: VerificationCondition) : Unit = checkVerificationConditions(vc)
- def checkVerificationConditions(vcs: VerificationCondition*) : Unit = {
- for(vcInfo <- vcs) {
- val funDef = vcInfo.funDef
- val vc = vcInfo.condition
-
- reporter.info("Now considering '" + vcInfo.kind + "' VC for " + funDef.id + "...")
- reporter.info("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
- // if(Settings.unrollingLevel == 0) {
- reporter.info(simplifyLets(vc))
- // } else {
- // reporter.info("(not showing unrolled VCs)")
- // }
-
- // try all solvers until one returns a meaningful answer
- var superseeded : Set[String] = Set.empty[String]
- solverExtensions.find(se => {
- reporter.info("Trying with solver: " + se.shortDescription)
- if(superseeded(se.shortDescription) || superseeded(se.description)) {
- reporter.info("Solver was superseeded. Skipping.")
- false
- } else {
- superseeded = superseeded ++ Set(se.superseeds: _*)
-
- val t1 = System.nanoTime
- se.init()
- val solverResult = se.solve(vc)
- val t2 = System.nanoTime
- val dt = ((t2 - t1) / 1000000) / 1000.0
-
- solverResult match {
- case None => false
- case Some(true) => {
- reporter.info("==== VALID ====")
-
- vcInfo.value = Some(true)
- vcInfo.solvedWith = Some(se)
- vcInfo.time = Some(dt)
-
- true
- }
- case Some(false) => {
- reporter.error("==== INVALID ====")
-
- vcInfo.value = Some(false)
- vcInfo.solvedWith = Some(se)
- vcInfo.time = Some(dt)
-
- true
- }
- }
- }
- }) match {
- case None => {
- reporter.warning("No solver could prove or disprove the verification condition.")
- }
- case _ =>
- }
-
- }
-
- 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.")
- }
- }
-}
-
-object Analysis {
- private val keepCallWhenInlined: Boolean = true
-
- private def defineOneInlining(f : FunctionInvocation) : (Expr, Expr) = {
- val FunctionInvocation(fd, args) = f
- val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe)).toList
- val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
- val newBody = replace(substMap, freshenLocals(matchToIfThenElse(fd.body.get)))
- val newFunctionCall = FunctionInvocation(fd, newLetIDs.map(Variable(_))).setType(f.getType)
- val callID = FreshIdentifier("call_" + fd.id.name, true).setType(newBody.getType)
- val callTree = Let(callID, (newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e)), Variable(callID))
-
- (Equals(newFunctionCall, Variable(callID)), callTree)
- }
-
- private def inlineFunctionCall(f : FunctionInvocation) : Expr = {
- val FunctionInvocation(fd, args) = f
- val newLetIDs = fd.args.map(a => FreshIdentifier("arg_" + a.id.name, true).setType(a.tpe)).toList
- val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
- val newBody = replace(substMap, freshenLocals(matchToIfThenElse(fd.body.get)))
- simplifyLets((newLetIDs zip args).foldRight(newBody)((iap, e) => Let(iap._1, iap._2, e)))
- }
-
- def inlineNonRecursiveFunctions(program: Program, expression: Expr) : Expr = {
- def applyToCall(e: Expr) : Option[Expr] = e match {
- case f @ FunctionInvocation(fd, args) if fd.hasImplementation && !program.isRecursive(fd) => Some(inlineFunctionCall(f))
- case _ => None
- }
-
- var change: Boolean = true
- var toReturn: Expr = expression
- while(change) {
- val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
- change = c
- toReturn = t
- }
- toReturn
- }
-
- def unrollRecursiveFunctions(program: Program, expression: Expr, times: Int) : Expr = {
- def urf1(expression: Expr, times: Int) : Expr = {
- var newEqs: List[Expr] = Nil
-
- def applyToCall(e: Expr) : Option[Expr] = e match {
- case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => {
- val (newEq, bdy) = defineOneInlining(f)
- newEqs = newEq :: newEqs
- Some(bdy)
- }
- case _ => None
- }
-
- var remaining = if(times < 0) 0 else times
- var change: Boolean = true
- var toReturn: Expr = expression
- while(remaining > 0 && change) {
- val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
- change = c
- toReturn = inlineNonRecursiveFunctions(program, t)
- remaining = remaining - 1
- }
- liftLets(Implies(And(newEqs.reverse), toReturn))
- }
-
- def urf2(expression: Expr, times: Int) : Expr = {
- def applyToCall(e: Expr) : Option[Expr] = e match {
- case f @ FunctionInvocation(fd, args) if fd.hasImplementation && program.isRecursive(fd) => Some(inlineFunctionCall(f))
- case _ => None
- }
-
- var remaining = if(times < 0) 0 else times
- var change: Boolean = true
- var toReturn: Expr = expression
- while(remaining > 0 && change) {
- val (t,c) = searchAndReplaceDFSandTrackChanges(applyToCall)(toReturn)
- change = c
- toReturn = inlineNonRecursiveFunctions(program, t)
- remaining = remaining - 1
- }
- toReturn
- }
-
- if(keepCallWhenInlined)
- urf1(expression, times)
- else
- urf2(expression, times)
- }
-
- def inlineContracts(expression: Expr) : Expr = {
- var trueThings: List[Expr] = Nil
-
- def applyToCall(e: Expr) : Option[Expr] = e match {
- case f @ FunctionInvocation(fd, args) if fd.hasPostcondition => {
- val argsAsLet = fd.args.map(a => FreshIdentifier("parg_" + a.id.name, true).setType(a.tpe)).toList
- val argsAsLetVars = argsAsLet.map(Variable(_))
- val resultAsLet = FreshIdentifier("call_" + fd.id.name, true).setType(f.getType)
- val newFunCall = FunctionInvocation(fd, argsAsLetVars)
- val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip argsAsLetVars) : _*) + (ResultVariable() -> Variable(resultAsLet))
- // this thing is full of let variables! We will need to lift the let
- // defs. later to make sure they capture this
- val trueFact = replace(substMap, freshenLocals(fd.postcondition.get))
- val defList: Seq[(Identifier,Expr)] = ((argsAsLet :+ resultAsLet) zip (args :+ newFunCall))
- trueThings = trueFact :: trueThings
- // again: these let defs. need eventually to capture the "true thing"
- Some(defList.foldRight[Expr](Variable(resultAsLet))((iap, e) => Let(iap._1, iap._2, e)))
- }
- case _ => None
- }
- val result = searchAndReplaceDFS(applyToCall)(expression)
- liftLets(Implies(And(trueThings.reverse), result))
- }
-}
-
-object AnalysisPhase extends UnitPhase[Program] {
- val name = "Analysis"
- val description = "Leon Analyses"
-
- def apply(ctx: LeonContext, program: Program) {
- new Analysis(program).analyse
- }
-}
diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 4b54a38552d3c91dcaea8f6676cf65dfcc882cc6..acc1707eb8e8762c3ef5ad0ca1a3953a8dc4de0b 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -6,53 +6,14 @@ import purescala.TreeOps._
import purescala.Definitions._
object Extensions {
- sealed abstract class Extension(reporter: Reporter) {
+ import leon.verification.{Analyser,Tactic}
+ import leon.solvers.Solver
+
+ abstract class Extension(reporter: Reporter) {
def description: String
def shortDescription: String = description
}
- abstract class Solver(val reporter: Reporter) extends Extension(reporter) {
- // This can be used by solvers to "see" the programs from which the
- // formulas come. (e.g. to set up some datastructures for the defined
- // ADTs, etc.)
- def setProgram(program: Program) : Unit = {}
-
- // Returns Some(true) if valid, Some(false) if invalid,
- // None if unknown.
- // should halt as soon as possible with any result (Unknown is ok) as soon as forceStop is true
- def solve(expression: Expr) : Option[Boolean]
-
- def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = (solve(expression), Map.empty)
-
- def isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
- def superseeds : Seq[String] = Nil
-
- private var _forceStop = false
- def halt() : Unit = {
- _forceStop = true
- }
- def init() : Unit = {
- _forceStop = false
- }
- protected def forceStop = _forceStop
-
- }
-
- abstract class Analyser(reporter: Reporter) extends Extension(reporter) {
- // Does whatever the analysis should. Uses the reporter to
- // signal results and/or errors.
- def analyse(program: Program) : Unit
- }
-
- abstract class Tactic(reporter: Reporter) extends Extension(reporter) {
- def setProgram(program: Program) : Unit = {}
- def generatePostconditions(function: FunDef) : Seq[VerificationCondition]
- def generatePreconditions(function: FunDef) : Seq[VerificationCondition]
- def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition]
- def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition]
- def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition]
- }
-
// The rest of the code is for dynamically loading extensions
private var allLoaded : Seq[Extension] = Nil
diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index d81b8eea718d40639c0ff5edce6bdc57c0837f83..b18f50d2559a196b22163b3c62ed3def2f610ef0 100644
--- a/src/main/scala/leon/LeonPhase.scala
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -2,7 +2,7 @@ package leon
import purescala.Definitions.Program
-abstract class LeonPhase[F, T] {
+abstract class LeonPhase[-F, +T] extends Pipeline[F, T] {
val name: String
val description: String
@@ -34,8 +34,8 @@ case class NoopPhase[T]() extends LeonPhase[T, T] {
override def run(ctx: LeonContext)(v: T) = v
}
-case class ExitPhase[T]() extends LeonPhase[T, Unit] {
+case class ExitPhase() extends LeonPhase[Any, Unit] {
val name = "end";
val description = "end"
- override def run(ctx: LeonContext)(v: T) = ()
+ override def run(ctx: LeonContext)(v: Any) = ()
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index f04a463cfe6dfaf969782c014a9cc344e72e012f..3f6f9e9278a6504a5e465db6870b84b987e67bfa 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -13,7 +13,7 @@ object Main {
/*FunctionHoisting,*/
Simplificator,
synthesis.SynthesisPhase,
- AnalysisPhase
+ verification.AnalysisPhase
)
}
@@ -104,11 +104,11 @@ object Main {
// Process options we understand:
for(opt <- leonOptions) opt match {
case LeonFlagOption("synthesis") =>
- settings = settings.copy(synthesis = true, xlang = false, analyze = false)
+ settings = settings.copy(synthesis = true, xlang = false, verify = false)
case LeonFlagOption("xlang") =>
settings = settings.copy(synthesis = false, xlang = true)
case LeonFlagOption("parse") =>
- settings = settings.copy(synthesis = false, xlang = false, analyze = false)
+ settings = settings.copy(synthesis = false, xlang = false, verify = false)
case LeonFlagOption("help") =>
displayHelp(reporter)
case _ =>
@@ -117,12 +117,10 @@ object Main {
LeonContext(settings = settings, reporter = reporter, files = files, options = leonOptions)
}
- implicit def phaseToPipeline[F, T](phase: LeonPhase[F, T]): Pipeline[F, T] = new PipeCons(phase, new PipeNil())
-
def computePipeline(settings: Settings): Pipeline[List[String], Unit] = {
import purescala.Definitions.Program
- val pipeBegin = phaseToPipeline(plugin.ExtractionPhase)
+ val pipeBegin : Pipeline[List[String],Program] = plugin.ExtractionPhase
val pipeTransforms: Pipeline[Program, Program] =
if (settings.xlang) {
@@ -141,18 +139,18 @@ object Main {
NoopPhase[Program]()
}
- val pipeAnalysis: Pipeline[Program, Program] =
- if (settings.analyze) {
- AnalysisPhase
+ val pipeVerify: Pipeline[Program, Any] =
+ if (settings.verify) {
+ verification.AnalysisPhase
} else {
NoopPhase[Program]()
}
- pipeBegin followedBy
- pipeTransforms followedBy
- pipeSynthesis followedBy
- pipeAnalysis andThen
- ExitPhase[Program]()
+ pipeBegin andThen
+ pipeTransforms andThen
+ pipeSynthesis andThen
+ pipeVerify andThen
+ ExitPhase()
}
def main(args : Array[String]) {
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 477a08c31250ba1996ddccd59262631fe75499c1..cc79495df619d9cb6ed74fb7a8fb03f628e07d6b 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -1,26 +1,11 @@
package leon
-abstract class Pipeline[F, T] {
- def andThen[G](then: LeonPhase[T, G]): Pipeline[F, G];
- def followedBy[G](pipe: Pipeline[T, G]): Pipeline[F, G];
- def run(ctx: LeonContext)(v: F): T;
-}
-
-class PipeCons[F, V, T](phase: LeonPhase[F, V], then: Pipeline[V, T]) extends Pipeline[F, T] {
- def andThen[G](last: LeonPhase[T, G]) = new PipeCons(phase, then andThen last)
- def followedBy[G](pipe: Pipeline[T, G]) = new PipeCons(phase, then followedBy pipe);
- def run(ctx: LeonContext)(v: F): T = then.run(ctx)(phase.run(ctx)(v))
+abstract class Pipeline[-F, +T] {
+ self =>
- override def toString = {
- phase.toString + " -> " + then.toString
+ def andThen[G](then: Pipeline[T, G]): Pipeline[F, G] = new Pipeline[F,G] {
+ def run(ctx : LeonContext)(v : F) : G = then.run(ctx)(self.run(ctx)(v))
}
-}
-class PipeNil[T]() extends Pipeline[T,T] {
- def andThen[G](last: LeonPhase[T, G]) = new PipeCons(last, new PipeNil)
- def run(ctx: LeonContext)(v: T): T = v
- def followedBy[G](pipe: Pipeline[T, G]) = pipe;
- override def toString = {
- "|"
- }
+ def run(ctx: LeonContext)(v: F): T
}
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 03512770fc9c84d9d11a41b2124fafdc6683e506..814c4352a321f41a0f75bac34ad20643d69b6c7b 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 c57a1e4514b00372033c7e19242b7782e40b8c56..04ed6bc41df6aa410879b2492aeb9f5580ab93a9 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -1,6 +1,7 @@
package leon
// typically these settings can be changed through some command-line switch.
+// TODO this global object needs to die (or at least clean out of its var's)
object Settings {
var experimental : Boolean = false
var showIDs: Boolean = false
@@ -10,7 +11,6 @@ object Settings {
var runDefaultExtensions: Boolean = true
var noForallAxioms: Boolean = true
var unrollingLevel: Int = 0
- var zeroInlining : Boolean = true
var useBAPA: Boolean = false
var impureTestcases: Boolean = false
var nbTestcases: Int = 1
@@ -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
@@ -38,5 +37,5 @@ object Settings {
case class Settings(
val synthesis: Boolean = false,
val xlang: Boolean = false,
- val analyze: Boolean = true
+ val verify: Boolean = true
)
diff --git a/src/main/scala/leon/TestExtension.scala b/src/main/scala/leon/TestExtension.scala
deleted file mode 100644
index 5fd517280e6c00eb4939e0615a5b6d41f0822379..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/TestExtension.scala
+++ /dev/null
@@ -1,109 +0,0 @@
-package leon
-
-import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.Extractors._
-import purescala.TypeTrees._
-import purescala.Definitions._
-import Extensions._
-
-class TestExtension(val reporter: Reporter) extends Analyser(reporter) {
- val description : String = "Testing."
- def analyse(program : Program) : Unit = {
- }/*
- for((f: FunDef) <- program.definedFunctions) {
- reporter.info("Got an f ! " + f.id)
- reporter.info("Normal : " + f.body.get)
- val iteized = matchToIfThenElse(expandLets(f.body.get))
- reporter.info("ITEized : " + iteized)
- reporter.info("Leadsto ? : " + (leadsToCall(iteized) : String))
- cleanClausify(iteized, program)
- val (e,l,m) = clausifyITE(iteized)
- reporter.info("As clauses : " + e)
- l.foreach(reporter.info(_))
- reporter.info("***\n")
- }
- reporter.info("Done.")
- }*/
-
- type LiftedBoolean = Option[Boolean]
- val Yes : LiftedBoolean = Some(true)
- val No : LiftedBoolean = Some(false)
- val Maybe : LiftedBoolean = None
- implicit def bool2liftedbool(b : Boolean) : LiftedBoolean = Some(b)
- implicit def liftedbool2String(l : LiftedBoolean) : String = l match {
- case Yes => "Yes"
- case No => "No"
- case Maybe => "Maybe"
- }
-
- // assumes no lets and no match.
- def leadsToCall(e : Expr) : LiftedBoolean = e match {
- case f : FunctionInvocation => true
- case IfExpr(a1, a2, a3) => {
- if(leadsToCall(a1) == Yes) Yes else (leadsToCall(a2),leadsToCall(a3)) match {
- case (Yes,Yes) => Yes
- case (No,No) => No
- case _ => Maybe
- }
- }
- case n @ NAryOperator(args, _) => {
- val ra = args.map(leadsToCall(_))
- if(ra.exists(_ == Yes)) {
- Yes
- } else if(ra.forall(_ == No)) {
- No
- } else {
- Maybe
- }
- }
- case b @ BinaryOperator(a1,a2,_) => (leadsToCall(a1),leadsToCall(a2)) match {
- case (Yes,_) => Yes
- case (_,Yes) => Yes
- case (No,No) => No
- case _ => Maybe
- }
- case u @ UnaryOperator(a,_) => leadsToCall(a)
- case t : Terminal => false
- case unhandled => scala.sys.error("unhandled.")
- }
-
- private def cleanClausify(formula : Expr, program : Program) : Unit = {
- val nonRec = allNonRecursiveFunctionCallsOf(formula, program)
- val allRec = functionCallsOf(formula) -- nonRec
-
- val (e,l,m) = clausifyITE(formula)
- var dangerSet : Set[Expr] = Set.empty[Expr] ++ allRec
- var change : Boolean = true
- var newSet : Set[Expr] = Set.empty
-
- while(change) {
- change = false
- }
- }
-
- private def clausifyITE(formula : Expr) : (Expr, List[Expr], Map[Identifier,Identifier]) = {
- var newClauses : List[Expr] = Nil
- var ite2Bools : Map[Identifier,Identifier] = Map.empty
-
- def clausify(ex : Expr) : Option[Expr] = ex match {
- //case _ if leadsToCall(ex) == No => None
- case ie @ IfExpr(cond, then, elze) => {
- val switch = FreshIdentifier("path", true).setType(BooleanType).toVariable
- val placeHolder = FreshIdentifier("iteval", true).setType(ie.getType).toVariable
- newClauses = Iff(switch, cond) :: newClauses
- newClauses = Implies(switch, Equals(placeHolder, then)) :: newClauses
- newClauses = Implies(Not(switch), Equals(placeHolder, elze)) :: newClauses
- // newBools = newBools + switch.id
- ite2Bools = ite2Bools + (placeHolder.id -> switch.id)
- Some(placeHolder)
- }
- case _ => None
- }
-
- val cleanedUp = searchAndReplaceDFS(clausify)(formula)
-
- (cleanedUp, newClauses.reverse, ite2Bools)
- }
-}
diff --git a/src/main/scala/leon/isabelle/Main.scala b/src/main/scala/leon/isabelle/Main.scala
index ac95c8095ec4a9af8543e8d0cecc795a5f8acd19..3db02146e338b8b6f72c886df9072c5d98f01311 100644
--- a/src/main/scala/leon/isabelle/Main.scala
+++ b/src/main/scala/leon/isabelle/Main.scala
@@ -4,6 +4,8 @@ import leon.Extensions._
import leon.Reporter
import leon.Settings._
+import leon.verification.Analyser
+
import leon.purescala.Common.Identifier
import leon.purescala.Definitions._
import leon.purescala.PrettyPrinter
diff --git a/src/main/scala/leon/plugin/AnalysisComponent.scala b/src/main/scala/leon/plugin/AnalysisComponent.scala
index 77c058a6fa5335cbc5092b545c453d9ef0396cf0..1cc1cde07699255945ffab7a42dba0c52e586a98 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/ExtractorPhase.scala b/src/main/scala/leon/plugin/ExtractorPhase.scala
index ef94d03e53d357b4837173ff49cdf2d082fc3d97..fdc271d53cc641d587dde3fbef7b1520579f28e4 100644
--- a/src/main/scala/leon/plugin/ExtractorPhase.scala
+++ b/src/main/scala/leon/plugin/ExtractorPhase.scala
@@ -12,6 +12,8 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
def run(ctx: LeonContext)(args: List[String]): Program = {
val settings = new NSCSettings
+ settings.usejavacp.value = true
+
val compilerOpts = args.filterNot(_.startsWith("--"))
val command = new CompilerCommand(compilerOpts, settings) {
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index 13542da332745a4db94d34e09bb107a5f4d75e3b..afc5fa35d441c099da969c2e5789ea48ea229643 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/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 4610fb491c1dc139e0c824caf175162cf5308d7c..98551cbc108a6b6f0c4ea74f081584049b65adf4 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1,7 +1,7 @@
package leon
package purescala
-import leon.Extensions.Solver
+import leon.solvers.Solver
object TreeOps {
import Common._
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d998013231be4548a885340fce579e39e09e40e9
--- /dev/null
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -0,0 +1,40 @@
+package leon
+package solvers
+
+import Extensions.Extension
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.TreeOps._
+import purescala.Trees._
+
+abstract class Solver(val reporter: Reporter) extends Extension(reporter) {
+ // This can be used by solvers to "see" the programs from which the
+ // formulas come. (e.g. to set up some datastructures for the defined
+ // ADTs, etc.)
+ // Ideally, we would pass it at construction time and not change it later.
+ def setProgram(program: Program) : Unit = {}
+
+ // Returns Some(true) if valid, Some(false) if invalid,
+ // None if unknown.
+ // should halt as soon as possible with any result (Unknown is ok) as soon as forceStop is true
+ def solve(expression: Expr) : Option[Boolean]
+
+ def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = (solve(expression), Map.empty)
+
+ def isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
+ def superseeds : Seq[String] = Nil
+
+ private var _forceStop = false
+
+ def halt() : Unit = {
+ _forceStop = true
+ }
+
+ def init() : Unit = {
+ _forceStop = false
+ }
+
+ protected def forceStop = _forceStop
+}
+
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 5c31961fb2bc40e0d749e6b44112b74788e22b4a..414e8e1a4941f51659215e545b68095cdf1e30bc 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -15,7 +15,7 @@ import scala.collection.mutable.{Set => MutableSet}
// This is just to factor out the things that are common in "classes that deal
// with a Z3 instance"
trait AbstractZ3Solver {
- self: Solver =>
+ self: leon.solvers.Solver =>
val reporter: Reporter
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 9d654c88fda3821b41765969de134acd28a50bbc..c229d44d3a81e1c4e1bbcf90ee94cc1657f807ba 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -2,6 +2,9 @@ package leon
package solvers.z3
import z3.scala._
+
+import leon.solvers.Solver
+
import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
@@ -247,7 +250,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
reporter.info(" - Running Z3 search...")
- val (answer, model, core) : (Option[Boolean], Z3Model, Seq[Z3AST]) = if(Settings.useCores) {
+ val answerModelCore : (Option[Boolean], Z3Model, Seq[Z3AST]) = if(Settings.useCores) {
// println(blockingSetAsZ3)
z3.checkAssumptions(blockingSetAsZ3 : _*)
} else {
@@ -259,6 +262,8 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
z3SearchStopwatch.stop
(a, m, Seq.empty[Z3AST])
}
+ val (answer, model, core) = answerModelCore // to work around the stupid type inferer
+
reporter.info(" - Finished search with blocked literals")
Logger.debug("The blocking guards are: " + blockingSet.mkString(", "), 4, "z3solver")
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 1ad2ed1fc47f285d0b3ff3101b1c2698291a4958..0100286d6446b96173fa7e2c0b1d7b8d49ceeb9f 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -2,6 +2,9 @@ package leon
package solvers.z3
import z3.scala._
+
+import leon.solvers.Solver
+
import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 0dc4cb283f48c0674b8a3638a1e4f875f7e9affc..91ba9d37f14607bfd2ed867f750791cdbae5260d 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -7,7 +7,7 @@ import purescala.TreeOps._
import purescala.Trees.{Expr, Not}
import purescala.ScalaPrinter
-import Extensions.Solver
+import solvers.Solver
import java.io.File
import collection.mutable.PriorityQueue
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
index 5056ec0e8ead3156847a18a5f358cde951b11d5e..ea6ccabcb826289172607dc94bbf7398e8137716 100644
--- a/src/main/scala/leon/testgen/TestGeneration.scala
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -1,5 +1,7 @@
package leon.testgen
+import leon.verification.Analyser
+
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Trees._
diff --git a/src/main/scala/leon/verification/Analyser.scala b/src/main/scala/leon/verification/Analyser.scala
new file mode 100644
index 0000000000000000000000000000000000000000..84a2d87221bdfeb1d225ec6bb3542c2a5db7f4e4
--- /dev/null
+++ b/src/main/scala/leon/verification/Analyser.scala
@@ -0,0 +1,13 @@
+package leon
+package verification
+
+import Extensions.Extension
+
+import purescala.Definitions.Program
+
+// TODO this class is slowly but surely becoming useless, as we now have a notion of phases.
+abstract class Analyser(reporter: Reporter) extends Extension(reporter) {
+ // Does whatever the analysis should. Uses the reporter to
+ // signal results and/or errors.
+ def analyse(program: Program) : Unit
+}
diff --git a/src/main/scala/leon/verification/Analysis.scala b/src/main/scala/leon/verification/Analysis.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1521ad8e1e3fa4ad42d36664d76d27a5fed4966c
--- /dev/null
+++ b/src/main/scala/leon/verification/Analysis.scala
@@ -0,0 +1,157 @@
+package leon
+package verification
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+
+import Extensions._
+
+import solvers.{Solver,TrivialSolver}
+
+import scala.collection.mutable.{Set => MutableSet}
+
+class Analysis(val program : Program, val reporter: Reporter) {
+ Extensions.loadAll(reporter)
+
+ val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
+
+ val trivialSolver = new TrivialSolver(reporter) // This one you can't disable :D
+
+ val solverExtensions: Seq[Solver] = trivialSolver +: loadedSolverExtensions
+
+ solverExtensions.foreach(_.setProgram(program))
+
+ val defaultTactic = new DefaultTactic(reporter)
+ defaultTactic.setProgram(program)
+ val inductionTactic = new InductionTactic(reporter)
+ inductionTactic.setProgram(program)
+
+ // 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
+ // Analysis extensions are run on the program.
+ def analyse : VerificationReport = {
+ // We generate all function templates in advance.
+ for(funDef <- program.definedFunctions if funDef.hasImplementation) {
+ // this gets cached :D
+ FunctionTemplate.mkTemplate(funDef)
+ }
+
+ val report = if(solverExtensions.size > 1) {
+ reporter.info("Running verification condition generation...")
+ checkVerificationConditions(generateVerificationConditions)
+ } else {
+ reporter.warning("No solver specified. Cannot test verification conditions.")
+ VerificationReport.emptyReport
+ }
+
+ analysisExtensions.foreach(ae => {
+ reporter.info("Running analysis from extension: " + ae.description)
+ ae.analyse(program)
+ })
+
+ report
+ }
+
+ private def generateVerificationConditions : List[VerificationCondition] = {
+ var allVCs: Seq[VerificationCondition] = Seq.empty
+ val analysedFunctions: MutableSet[String] = MutableSet.empty
+
+ for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1 < fd2) if (Settings.functionsToAnalyse.isEmpty || Settings.functionsToAnalyse.contains(funDef.id.name))) {
+ analysedFunctions += funDef.id.name
+
+ val tactic: Tactic =
+ if(funDef.annotations.contains("induct")) {
+ inductionTactic
+ } else {
+ defaultTactic
+ }
+
+ if(funDef.body.isDefined) {
+ allVCs ++= tactic.generatePreconditions(funDef)
+ allVCs ++= tactic.generatePatternMatchingExhaustivenessChecks(funDef)
+ allVCs ++= tactic.generatePostconditions(funDef)
+ allVCs ++= tactic.generateMiscCorrectnessConditions(funDef)
+ allVCs ++= tactic.generateArrayAccessChecks(funDef)
+ }
+ 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: Set[String] = Settings.functionsToAnalyse -- analysedFunctions
+ notFound.foreach(fn => reporter.error("Did not find function \"" + fn + "\" though it was marked for analysis."))
+
+ allVCs.toList
+ }
+
+ private def checkVerificationConditions(vcs: Seq[VerificationCondition]) : VerificationReport = {
+ for(vcInfo <- vcs) {
+ val funDef = vcInfo.funDef
+ val vc = vcInfo.condition
+
+ reporter.info("Now considering '" + vcInfo.kind + "' VC for " + funDef.id + "...")
+ reporter.info("Verification condition (" + vcInfo.kind + ") for ==== " + funDef.id + " ====")
+ // if(Settings.unrollingLevel == 0) {
+ reporter.info(simplifyLets(vc))
+ // } else {
+ // reporter.info("(not showing unrolled VCs)")
+ // }
+
+ // try all solvers until one returns a meaningful answer
+ var superseeded : Set[String] = Set.empty[String]
+ solverExtensions.find(se => {
+ reporter.info("Trying with solver: " + se.shortDescription)
+ if(superseeded(se.shortDescription) || superseeded(se.description)) {
+ reporter.info("Solver was superseeded. Skipping.")
+ false
+ } else {
+ superseeded = superseeded ++ Set(se.superseeds: _*)
+
+ val t1 = System.nanoTime
+ se.init()
+ val solverResult = se.solve(vc)
+ val t2 = System.nanoTime
+ val dt = ((t2 - t1) / 1000000) / 1000.0
+
+ solverResult match {
+ case None => false
+ case Some(true) => {
+ reporter.info("==== VALID ====")
+
+ vcInfo.value = Some(true)
+ vcInfo.solvedWith = Some(se)
+ vcInfo.time = Some(dt)
+
+ true
+ }
+ case Some(false) => {
+ reporter.error("==== INVALID ====")
+
+ vcInfo.value = Some(false)
+ vcInfo.solvedWith = Some(se)
+ vcInfo.time = Some(dt)
+
+ true
+ }
+ }
+ }
+ }) match {
+ case None => {
+ reporter.warning("No solver could prove or disprove the verification condition.")
+ }
+ case _ =>
+ }
+
+ }
+
+ val report = new VerificationReport(vcs)
+ reporter.info(report.summaryString)
+ report
+ }
+}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..726a7922a59de70142369301a5e57917c4b1ad2e
--- /dev/null
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -0,0 +1,13 @@
+package leon
+package verification
+
+import purescala.Definitions._
+
+object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
+ val name = "Analysis"
+ val description = "Leon Verification"
+
+ def run(ctx: LeonContext)(program: Program) : VerificationReport = {
+ new Analysis(program, ctx.reporter).analyse
+ }
+}
diff --git a/src/main/scala/leon/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
similarity index 85%
rename from src/main/scala/leon/DefaultTactic.scala
rename to src/main/scala/leon/verification/DefaultTactic.scala
index 4078e6e490f8a1bbe5adc5a985459d144a13c363..47a2af0d2a098722e36af1c2e829bf31e5734a59 100644
--- a/src/main/scala/leon/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -1,11 +1,11 @@
package leon
+package verification
import purescala.Common._
import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
import purescala.Definitions._
-import Extensions.Tactic
import scala.collection.mutable.{Map => MutableMap}
@@ -42,43 +42,7 @@ class DefaultTactic(reporter: Reporter) extends Tactic(reporter) {
Implies(matchToIfThenElse(prec.get), bodyAndPost)
}
- import Analysis._
-
- if(Settings.zeroInlining) {
- withPrec
- } else {
- if(Settings.experimental) {
- reporter.info("Raw:")
- reporter.info(withPrec)
- reporter.info("Raw, expanded:")
- reporter.info(expandLets(withPrec))
- }
- reporter.info(" - inlining...")
- val expr0 = inlineNonRecursiveFunctions(program, withPrec)
- if(Settings.experimental) {
- reporter.info("Inlined:")
- reporter.info(expr0)
- reporter.info("Inlined, expanded:")
- reporter.info(expandLets(expr0))
- }
- reporter.info(" - unrolling...")
- val expr1 = unrollRecursiveFunctions(program, expr0, Settings.unrollingLevel)
- if(Settings.experimental) {
- reporter.info("Unrolled:")
- reporter.info(expr1)
- reporter.info("Unrolled, expanded:")
- reporter.info(expandLets(expr1))
- }
- reporter.info(" - inlining contracts...")
- val expr2 = inlineContracts(expr1)
- if(Settings.experimental) {
- reporter.info("Contract'ed:")
- reporter.info(expr2)
- reporter.info("Contract'ed, expanded:")
- reporter.info(expandLets(expr2))
- }
- expr2
- }
+ withPrec
}
if(functionDefinition.fromLoop)
Seq(new VerificationCondition(theExpr, functionDefinition.parent.get, VCKind.InvariantPost, this.asInstanceOf[DefaultTactic]).setPosInfo(functionDefinition))
diff --git a/src/main/scala/leon/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
similarity index 99%
rename from src/main/scala/leon/InductionTactic.scala
rename to src/main/scala/leon/verification/InductionTactic.scala
index 4adc158b323678d423ce9c7bb80705ac2512fc25..360f41493440cba920be3a4f21289f33ff3e9f1b 100644
--- a/src/main/scala/leon/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -1,4 +1,5 @@
package leon
+package verification
import purescala.Common._
import purescala.Trees._
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d19752949f393e5bad32f2824b723ea6dfabed91
--- /dev/null
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -0,0 +1,15 @@
+package leon
+package verification
+
+import Extensions.Extension
+
+import purescala.Definitions._
+
+abstract class Tactic(reporter: Reporter) extends Extension(reporter) {
+ def setProgram(program: Program) : Unit = {}
+ def generatePostconditions(function: FunDef) : Seq[VerificationCondition]
+ def generatePreconditions(function: FunDef) : Seq[VerificationCondition]
+ def generatePatternMatchingExhaustivenessChecks(function: FunDef) : Seq[VerificationCondition]
+ def generateMiscCorrectnessConditions(function: FunDef) : Seq[VerificationCondition]
+ def generateArrayAccessChecks(function: FunDef) : Seq[VerificationCondition]
+}
diff --git a/src/main/scala/leon/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
similarity index 56%
rename from src/main/scala/leon/VerificationCondition.scala
rename to src/main/scala/leon/verification/VerificationCondition.scala
index e5556f1acf52fa3f8472556bcc66d3572c032488..217eb94b70287d8f74de5a98a1370c0068c831ac 100644
--- a/src/main/scala/leon/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -1,9 +1,10 @@
-package leon
+package leon.verification
-import purescala.Trees._
-import purescala.Definitions._
-import purescala.Common._
-import Extensions._
+import leon.purescala.Trees._
+import leon.purescala.Definitions._
+import leon.purescala.Common._
+
+import leon.solvers.Solver
/** 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 = "") extends ScalacPositional {
@@ -20,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
new file mode 100644
index 0000000000000000000000000000000000000000..16b6516241c806005605ec8ce0a56cc178eb3035
--- /dev/null
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -0,0 +1,48 @@
+package leon.verification
+
+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/resources/regression/verification/purescala/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dd5a75f89735805a74612665e487aa8fa99ec397
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
@@ -0,0 +1,124 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object AmortizedQueue {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class AbsQueue
+ case class Queue(front : List, rear : List) extends AbsQueue
+
+ def size(list : List) : Int = (list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def asList(queue : AbsQueue) : List = queue match {
+ case Queue(front, rear) => concat(front, reverse(rear))
+ }
+
+ def concat(l1 : List, l2 : List) : List = (l1 match {
+ case Nil() => l2
+ case Cons(x,xs) => Cons(x, concat(xs, l2))
+ }) ensuring (res => size(res) == size(l1) + size(l2) && content(res) == content(l1) ++ content(l2))
+
+ def isAmortized(queue : AbsQueue) : Boolean = queue match {
+ case Queue(front, rear) => size(front) >= size(rear)
+ }
+
+ def isEmpty(queue : AbsQueue) : Boolean = queue match {
+ case Queue(Nil(), Nil()) => true
+ case _ => false
+ }
+
+ def reverse(l : List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil()))
+ }) ensuring (content(_) == content(l))
+
+ def amortizedQueue(front : List, rear : List) : AbsQueue = {
+ if (size(rear) <= size(front))
+ Queue(front, rear)
+ else
+ Queue(concat(front, reverse(rear)), Nil())
+ } ensuring(isAmortized(_))
+
+ def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
+ case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear))
+ }) ensuring(isAmortized(_))
+
+ def tail(queue : AbsQueue) : AbsQueue = {
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
+ }
+ } ensuring (isAmortized(_))
+
+ def front(queue : AbsQueue) : Int = {
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, _), _) => f
+ }
+ }
+
+ // @induct
+ // def propEnqueue(rear : List, front : List, list : List, elem : Int) : Boolean = {
+ // require(isAmortized(Queue(front, rear)))
+ // val queue = Queue(front, rear)
+ // if (asList(queue) == list) {
+ // asList(enqueue(queue, elem)) == concat(list, Cons(elem, Nil()))
+ // } else
+ // true
+ // } holds
+
+ @induct
+ def propFront(queue : AbsQueue, list : List, elem : Int) : Boolean = {
+ require(!isEmpty(queue) && isAmortized(queue))
+ if (asList(queue) == list) {
+ list match {
+ case Cons(x, _) => front(queue) == x
+ }
+ } else
+ true
+ } holds
+
+ @induct
+ def propTail(rear : List, front : List, list : List, elem : Int) : Boolean = {
+ require(!isEmpty(Queue(front, rear)) && isAmortized(Queue(front, rear)))
+ if (asList(Queue(front, rear)) == list) {
+ list match {
+ case Cons(_, xs) => asList(tail(Queue(front, rear))) == xs
+ }
+ } else
+ true
+ } // holds
+
+ def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = {
+ if (isEmpty(queue))
+ front(enqueue(queue, elem)) == elem
+ else
+ true
+ } holds
+
+ def enqueueDequeueThrice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = {
+ if (isEmpty(queue)) {
+ val q1 = enqueue(queue, e1)
+ val q2 = enqueue(q1, e2)
+ val q3 = enqueue(q2, e3)
+ val e1prime = front(q3)
+ val q4 = tail(q3)
+ val e2prime = front(q4)
+ val q5 = tail(q4)
+ val e3prime = front(q5)
+ e1 == e1prime && e2 == e2prime && e3 == e3prime
+ } else
+ true
+ } holds
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f5a2fc0415a2cf6023f9ae1f3620e99f9fdc27cb
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
@@ -0,0 +1,50 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object AssociativeList {
+ sealed abstract class KeyValuePairAbs
+ case class KeyValuePair(key: Int, value: Int) extends KeyValuePairAbs
+
+ sealed abstract class List
+ case class Cons(head: KeyValuePairAbs, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class OptionInt
+ case class Some(i: Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def domain(l: List): Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs)
+ }
+
+ def find(l: List, e: Int): OptionInt = l match {
+ case Nil() => None()
+ case Cons(KeyValuePair(k, v), xs) => if (k == e) Some(v) else find(xs, e)
+ }
+
+ def noDuplicates(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None() && noDuplicates(xs)
+ }
+
+ def update(l1: List, l2: List): List = (l2 match {
+ case Nil() => l1
+ case Cons(x, xs) => update(updateElem(l1, x), xs)
+ }) ensuring(domain(_) == domain(l1) ++ domain(l2))
+
+ def updateElem(l: List, e: KeyValuePairAbs): List = (l match {
+ case Nil() => Cons(e, Nil())
+ case Cons(KeyValuePair(k, v), xs) => e match {
+ case KeyValuePair(ek, ev) => if (ek == k) Cons(KeyValuePair(ek, ev), xs) else Cons(KeyValuePair(k, v), updateElem(xs, e))
+ }
+ }) ensuring(res => e match {
+ case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k)
+ })
+
+ @induct
+ def readOverWrite(l: List, k1: Int, k2: Int, e: Int) : Boolean = {
+ find(updateElem(l, KeyValuePair(k2,e)), k1) == (if (k1 == k2) Some(e) else find(l, k1))
+ } holds
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d2ae67b3bb465f13437a1eb70a57a8e7e613347a
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
@@ -0,0 +1,80 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head:Int,tail:List) extends List
+ case class Nil() extends List
+
+ sealed abstract class OptInt
+ case class Some(value: Int) extends OptInt
+ case class None() extends OptInt
+
+ def size(l : List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def min(l : List) : OptInt = l match {
+ case Nil() => None()
+ case Cons(x, xs) => min(xs) match {
+ case None() => Some(x)
+ case Some(x2) => if(x < x2) Some(x) else Some(x2)
+ }
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, Nil()) => true
+ case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def sortedIns(e: Int, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+ )
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def buggySortedIns(e: Int, l: List): List = {
+ // require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+ )
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = (l match {
+ case Nil() => Nil()
+ case Cons(x,xs) => sortedIns(x, sort(xs))
+ }) ensuring(res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l)
+ )
+
+ def main(args: Array[String]): Unit = {
+ val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
+
+ println(ls)
+ println(sort(ls))
+ }
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a4fc4f8dc44a90f59a772b52b1a05053316e94d2
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
@@ -0,0 +1,107 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class IntPairList
+ case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
+ case class IPNil() extends IntPairList
+
+ sealed abstract class IntPair
+ case class IP(fst: Int, snd: Int) extends IntPair
+
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def iplSize(l: IntPairList) : Int = (l match {
+ case IPNil() => 0
+ case IPCons(_, xs) => 1 + iplSize(xs)
+ }) ensuring(_ >= 0)
+
+ def zip(l1: List, l2: List) : IntPairList = {
+ // try to comment this and see how pattern-matching becomes
+ // non-exhaustive and post-condition fails
+ require(size(l1) == size(l2))
+
+ l1 match {
+ case Nil() => IPNil()
+ case Cons(x, xs) => l2 match {
+ case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
+ }
+ }
+ } ensuring(iplSize(_) == size(l1))
+
+ def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
+ def sizeTailRecAcc(l: List, acc: Int) : Int = {
+ require(acc >= 0)
+ l match {
+ case Nil() => acc
+ case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
+ }
+ } ensuring(res => res == size(l) + acc)
+
+ def sizesAreEquiv(l: List) : Boolean = {
+ size(l) == sizeTailRec(l)
+ } holds
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def sizeAndContent(l: List) : Boolean = {
+ size(l) == 0 || content(l) != Set.empty[Int]
+ } holds
+
+ def drunk(l : List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
+ }) ensuring (size(_) == 2 * size(l))
+
+ def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l))
+ def reverse0(l1: List, l2: List) : List = (l1 match {
+ case Nil() => l2
+ case Cons(x, xs) => reverse0(xs, Cons(x, l2))
+ }) ensuring(content(_) == content(l1) ++ content(l2))
+
+ def append(l1 : List, l2 : List) : List = (l1 match {
+ case Nil() => l2
+ case Cons(x,xs) => Cons(x, append(xs, l2))
+ }) ensuring(content(_) == content(l1) ++ content(l2))
+
+ @induct
+ def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
+
+ @induct
+ def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
+ (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
+
+ def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = {
+ (append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
+ } holds
+
+ @induct
+ def sizeAppend(l1 : List, l2 : List) : Boolean =
+ (size(append(l1, l2)) == size(l1) + size(l2)) holds
+
+ @induct
+ def concat(l1: List, l2: List) : List =
+ concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2))
+
+ @induct
+ def concat0(l1: List, l2: List, l3: List) : List = (l1 match {
+ case Nil() => l2 match {
+ case Nil() => reverse(l3)
+ case Cons(y, ys) => {
+ concat0(Nil(), ys, Cons(y, l3))
+ }
+ }
+ case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
+ }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a35c3ef9be56871900d5e9474b385f0896edccd4
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
@@ -0,0 +1,86 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object PropositionalLogic {
+
+ sealed abstract class Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ case class Or(lhs: Formula, rhs: Formula) extends Formula
+ case class Implies(lhs: Formula, rhs: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Literal(id: Int) extends Formula
+
+ def simplify(f: Formula): Formula = (f match {
+ case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
+ case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
+ case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
+ case Not(f) => Not(simplify(f))
+ case Literal(_) => f
+ }) ensuring(isSimplified(_))
+
+ def isSimplified(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Implies(_,_) => false
+ case Not(f) => isSimplified(f)
+ case Literal(_) => true
+ }
+
+ def nnf(formula: Formula): Formula = (formula match {
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
+ case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
+ case Not(Not(f)) => nnf(f)
+ case Not(Literal(_)) => formula
+ case Literal(_) => formula
+ }) ensuring(isNNF(_))
+
+ def isNNF(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case Literal(_) => true
+ }
+
+ def vars(f: Formula): Set[Int] = {
+ require(isNNF(f))
+ f match {
+ case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Not(Literal(i)) => Set[Int](i)
+ case Literal(i) => Set[Int](i)
+ }
+ }
+
+ def fv(f : Formula) = { vars(nnf(f)) }
+
+ // @induct
+ // def wrongCommutative(f: Formula) : Boolean = {
+ // nnf(simplify(f)) == simplify(nnf(f))
+ // } holds
+
+ @induct
+ def simplifyBreaksNNF(f: Formula) : Boolean = {
+ require(isNNF(f))
+ isNNF(simplify(f))
+ } holds
+
+ @induct
+ def nnfIsStable(f: Formula) : Boolean = {
+ require(isNNF(f))
+ nnf(f) == f
+ } holds
+
+ @induct
+ def simplifyIsStable(f: Formula) : Boolean = {
+ require(isSimplified(f))
+ simplify(f) == f
+ } holds
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/README b/src/test/resources/regression/verification/purescala/valid/README
new file mode 100644
index 0000000000000000000000000000000000000000..2bb01d5fdbd6b59970c0c84f2c10db1ead6097a2
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/README
@@ -0,0 +1,2 @@
+This particular directory contains PureScala programs that can be entirely
+proved correct by Leon.
diff --git a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc2de6ba96ee699736d4558932b752eea9ebba9f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
@@ -0,0 +1,117 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ sealed abstract class OptionInt
+ case class Some(v : Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = (t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }) ensuring(_ >= 0)
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty() => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty() => 1
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty() => Node(Red(),Empty(),x,Empty())
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n))
+ n match {
+ case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def buggyAdd(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+
+ def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ // case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2c137fd4ad6b9d411f7e14b4ada6b834234c9e9e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
@@ -0,0 +1,48 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object SearchLinkedList {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ def size(list : List) : Int = (list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contains(list : List, elem : Int) : Boolean = (list match {
+ case Nil() => false
+ case Cons(x, xs) => x == elem || contains(xs, elem)
+ })
+
+ def firstZero(list : List) : Int = (list match {
+ case Nil() => 0
+ case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
+ }) ensuring (res =>
+ res >= 0 && (if (contains(list, 0)) {
+ firstZeroAtPos(list, res)
+ } else {
+ res == size(list)
+ }))
+
+ def firstZeroAtPos(list : List, pos : Int) : Boolean = {
+ list match {
+ case Nil() => false
+ case Cons(x, xs) => if (pos == 0) x == 0 else x != 0 && firstZeroAtPos(xs, pos - 1)
+ }
+ }
+
+ def goal(list : List, i : Int) : Boolean = {
+ if(firstZero(list) == i) {
+ if(contains(list, 0)) {
+ firstZeroAtPos(list, i)
+ } else {
+ i == size(list)
+ }
+ } else {
+ true
+ }
+ } holds
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0aa4ce7060a391d34dd047338fcd1f638054843f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
@@ -0,0 +1,46 @@
+import leon.Utils._
+import leon.Annotations._
+
+object SumAndMax {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ def max(list : List) : Int = {
+ require(list != Nil())
+ list match {
+ case Cons(x, Nil()) => x
+ case Cons(x, xs) => {
+ val m2 = max(xs)
+ if(m2 > x) m2 else x
+ }
+ }
+ }
+
+ def sum(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x, xs) => x + sum(xs)
+ }
+
+ def size(list : List) : Int = (list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def allPos(list : List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x, xs) => x >= 0 && allPos(xs)
+ }
+
+ def prop0(list : List) : Boolean = {
+ require(list != Nil())
+ !allPos(list) || max(list) >= 0
+ } holds
+
+ @induct
+ def property(list : List) : Boolean = {
+ // This precondition was given in the problem but isn't actually useful :D
+ // require(allPos(list))
+ sum(list) <= size(list) * (if(list == Nil()) 0 else max(list))
+ } holds
+}
diff --git a/src/test/scala/leon/test/Test.scala b/src/test/scala/leon/test/Test.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ed3549395b971f0e12fbdb8a8c7656526fe936e8
--- /dev/null
+++ b/src/test/scala/leon/test/Test.scala
@@ -0,0 +1,9 @@
+package leon.test
+
+import org.scalatest.FunSuite
+
+class Test extends FunSuite {
+ test("Tests work.") {
+ assert(true)
+ }
+}
diff --git a/src/test/scala/leon/test/ValidPrograms.scala b/src/test/scala/leon/test/ValidPrograms.scala
new file mode 100644
index 0000000000000000000000000000000000000000..37df60f224e91b9a23f030b4653ad725db9fad72
--- /dev/null
+++ b/src/test/scala/leon/test/ValidPrograms.scala
@@ -0,0 +1,48 @@
+package leon
+package test
+
+import org.scalatest.FunSuite
+
+import java.io.File
+
+class ValidPrograms extends FunSuite {
+ def runBasicLeonOnFile(filename : String) : Unit = {
+ val file = new File(filename)
+
+ assert(file.exists && file.isFile && file.canRead,
+ "Benchmark [%s] is not a readable file".format(filename))
+
+ val ctx = LeonContext(
+ settings = Settings(
+ synthesis = false,
+ xlang = false,
+ verify = true
+ ),
+ files = List(file),
+ reporter = new SilentReporter
+ )
+
+ val pipeline = Main.computePipeline(ctx.settings)
+ pipeline.run(ctx)("--timeout=2" :: file.getPath :: Nil)
+ }
+
+ def mkTest(filename : String) = {
+ test("Valid PureScala program: [%s]".format(filename)) {
+ runBasicLeonOnFile(filename)
+ assert(true)
+ }
+ }
+
+ test("List files") {
+ import scala.collection.JavaConversions._
+
+ val ress = this.getClass.getClassLoader.getResources("/regression/verification/purescala/valid/")
+
+ for(res <- ress) {
+ println(res)
+ }
+ }
+
+ // Sorry for leaving this there...
+ // mkTest("/home/psuter/Test.scala")
+}
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index 1682054408d45c00a7721bd9a113f61fad4706d9..6b015b9afc8fac4a8fbe51828680920b555a2a40 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -8,7 +8,7 @@ import leon.purescala.TypeTrees._
import leon.SilentReporter
-import leon.Extensions.Solver
+import leon.solvers.Solver
import leon.solvers.z3.UninterpretedZ3Solver
import org.scalatest.FunSuite