diff --git a/src/main/scala/leon/isabelle/Main.scala b/src/main/scala/leon/isabelle/Main.scala
index 9cf1040b3163d24d7f445023ada714bd00423e0a..abd1f557686213b2a599af1ffb109770834822b6 100644
--- a/src/main/scala/leon/isabelle/Main.scala
+++ b/src/main/scala/leon/isabelle/Main.scala
@@ -4,8 +4,6 @@ package isabelle
import leon.Reporter
import leon.Settings._
-import leon.verification.Analyser
-
import leon.purescala.Common.Identifier
import leon.purescala.Definitions._
import leon.purescala.PrettyPrinter
@@ -18,8 +16,9 @@ import java.lang.StringBuffer
import java.io._
import scala.collection.mutable.ListMap
+// TODO FIXME If this class is to be resurrected, make it a proper phase
@deprecated("Unused, Untested, Unmaintained.", "")
-class Main(context : LeonContext) extends Analyser(context) {
+class Main(context : LeonContext) {
val description = "Generates Isabelle source"
val shortDescription = "isabelle"
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
index 0876e17219def0126a1ac5bc18999b8e0fa06136..6125e6a4d5f71dd4e5c7a5cdc54421baf312a55e 100644
--- a/src/main/scala/leon/testgen/TestGeneration.scala
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -1,8 +1,6 @@
package leon
package testgen
-import leon.verification.Analyser
-
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Trees._
@@ -14,8 +12,9 @@ import leon.Reporter
import scala.collection.mutable.{Set => MutableSet}
+// TODO FIXME if this class is to be resurrected, make it a proper LeonPhase.
@deprecated("Unused, Untested, Unmaintained.", "")
-class TestGeneration(context : LeonContext) extends Analyser(context) {
+class TestGeneration(context : LeonContext) {
def description: String = "Generate random testcases"
def shortDescription: String = "test"
diff --git a/src/main/scala/leon/verification/Analyser.scala b/src/main/scala/leon/verification/Analyser.scala
deleted file mode 100644
index 5885531e8c0c9733c1b6cf8c16667923f1423c29..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/verification/Analyser.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-package leon
-package verification
-
-import purescala.Definitions.Program
-
-// TODO FIXME this class is slowly but surely becoming useless,
-// as we now have a notion of phases.
-abstract class Analyser(context : LeonContext) {
- // 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
deleted file mode 100644
index 2d4b29f7e9e084202196e672fda749b65728aa3e..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/verification/Analysis.scala
+++ /dev/null
@@ -1,157 +0,0 @@
-package leon
-package verification
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-
-import solvers.{Solver,TrivialSolver}
-import solvers.z3.FairZ3Solver
-
-import scala.collection.mutable.{Set => MutableSet}
-
-class Analysis(val program : Program, val context: LeonContext) {
- private val reporter = context.reporter
-
- val trivialSolver = new TrivialSolver(context)
-
- val fairZ3 = new FairZ3Solver(context)
-
- val solvers : Seq[Solver] = trivialSolver :: fairZ3 :: Nil
-
- solvers.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(solvers.size > 1) {
- reporter.info("Running verification condition generation...")
- checkVerificationConditions(generateVerificationConditions)
- } else {
- reporter.warning("No solver specified. Cannot test verification conditions.")
- VerificationReport.emptyReport
- }
-
- // This used to be for additional analyses. They should now just be different phases.
- // 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]
- solvers.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
index 1ec1084e0b978a6b1227595e3a53f223a610953b..cbea0d52431be1e2621075a493e29017c7bff195 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -1,7 +1,16 @@
package leon
package verification
+import purescala.Common._
import purescala.Definitions._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+
+import solvers.{Solver,TrivialSolver}
+import solvers.z3.FairZ3Solver
+
+import scala.collection.mutable.{Set => MutableSet}
object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val name = "Analysis"
@@ -12,6 +21,129 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
)
def run(ctx: LeonContext)(program: Program) : VerificationReport = {
- new Analysis(program, ctx).analyse
+ val reporter = ctx.reporter
+
+ val trivialSolver = new TrivialSolver(ctx)
+ val fairZ3 = new FairZ3Solver(ctx)
+
+ val solvers : Seq[Solver] = trivialSolver :: fairZ3 :: Nil
+
+ solvers.foreach(_.setProgram(program))
+
+ val defaultTactic = new DefaultTactic(reporter)
+ defaultTactic.setProgram(program)
+ val inductionTactic = new InductionTactic(reporter)
+ inductionTactic.setProgram(program)
+
+ 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 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 + " ====")
+ reporter.info(simplifyLets(vc))
+
+ // try all solvers until one returns a meaningful answer
+ var superseeded : Set[String] = Set.empty[String]
+ solvers.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
+ }
+
+ // We generate all function templates in advance.
+ for(funDef <- program.definedFunctions if funDef.hasImplementation) {
+ // this gets cached :D
+ FunctionTemplate.mkTemplate(funDef)
+ }
+
+ val report = if(solvers.size > 1) {
+ reporter.info("Running verification condition generation...")
+ checkVerificationConditions(generateVerificationConditions)
+ } else {
+ reporter.warning("No solver specified. Cannot test verification conditions.")
+ VerificationReport.emptyReport
+ }
+
+ report
}
}