From 70971eeb66db0027cc41acbe845114920c0e469a Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 26 Nov 2012 18:05:44 +0100
Subject: [PATCH] Cleaned up many old/useless options.
---
src/main/scala/leon/Logger.scala | 24 ----------
src/main/scala/leon/Settings.scala | 5 --
src/main/scala/leon/plugin/LeonPlugin.scala | 13 -----
.../scala/leon/purescala/Extractors.scala | 47 -------------------
.../scala/leon/solvers/z3/FairZ3Solver.scala | 10 ----
.../leon/verification/AnalysisPhase.scala | 14 ++++--
.../leon/verification/InductionTactic.scala | 4 --
7 files changed, 11 insertions(+), 106 deletions(-)
delete mode 100644 src/main/scala/leon/Logger.scala
diff --git a/src/main/scala/leon/Logger.scala b/src/main/scala/leon/Logger.scala
deleted file mode 100644
index fc4942535..000000000
--- a/src/main/scala/leon/Logger.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-package leon
-
-object Logger {
-
- //the debug level to display, from 0 (no debug information) to 5 (very verbose)
- //var level = 0
-
- //each debug information is tagged by a string, the tag variable only display the message with a tag in this set
- //if the set is empty then all tags are displayed
- //var tags: Set[String] = Set()
-
- val defaultTag = "main"
-
- private def output(msg: String, lvl: Int, tag: String) {
- if(lvl <= Settings.debugLevel) {
- if(Settings.debugTags.isEmpty || Settings.debugTags.contains(tag)) {
- println("DEBUG: [" + tag + "] " + msg)
- }
- }
- }
-
- def debug(msg: String, lvl: Int, tag: String = defaultTag) = output(msg, lvl, tag)
-
-}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 5e2585eb5..5536471de 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -3,12 +3,8 @@ 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
- var functionsToAnalyse: Set[String] = Set.empty
- var extensionNames: Seq[String] = Nil
lazy val reporter: Reporter = new DefaultReporter
- var runDefaultExtensions: Boolean = true
var noForallAxioms: Boolean = true
var unrollingLevel: Int = 0
var useBAPA: Boolean = false
@@ -25,7 +21,6 @@ object Settings {
// When this is None, use real integers
var bitvectorBitwidth : Option[Int] = None
var debugLevel: Int = 0
- var debugTags: Set[String] = Set.empty
var synthesis: Boolean = false
var transformProgram: Boolean = true
var stopAfterExtraction: Boolean = false
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index bdba7fb64..af25f91d3 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -18,9 +18,6 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
" --uniqid When pretty-printing purescala trees, show identifiers IDs" + "\n" +
" --with-code Allows the compiler to keep running after the static analysis" + "\n" +
" --parse Checks only whether the program is valid PureScala" + "\n" +
- " --extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
- " --nodefaults Runs only the analyses provided by the extensions" + "\n" +
- " --functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
" --unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
" --axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
" --tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
@@ -29,17 +26,13 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
" --testcases=[1,2] Number of testcases to generate per function" + "\n" +
" --testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
" --timeout=N Sets a timeout of N seconds" + "\n" +
- " --XP Enable weird transformations and other bug-producing features" + "\n" +
" --BV Use bit-vectors for integers" + "\n" +
" --prune Use additional SMT queries to rule out some unrollings" + "\n" +
" --cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
" --quickcheck Use QuickCheck-like random search" + "\n" +
" --parallel Run all solvers in parallel" + "\n" +
- //" --noLuckyTests Do not perform additional tests to potentially find models early" + "\n" +
" --noverifymodel Do not verify the correctness of models returned by Z3" + "\n" +
" --debug=[1-5] Debug level" + "\n" +
- " --tags=t1:... Filter out debug information that are not of one of the given tags" + "\n" +
- " --oneline Reduce the output to a single line: valid if all properties were valid, invalid if at least one is invalid, unknown else" + "\n" +
" --imperative Preprocessing and transformation from imperative programs" + "\n" +
" --synthesis Magic!"
)
@@ -53,17 +46,14 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
case "uniqid" => leon.Settings.showIDs = true
case "parse" => leon.Settings.stopAfterExtraction = true
case "tolerant" => leon.Settings.silentlyTolerateNonPureBodies = true
- case "nodefaults" => leon.Settings.runDefaultExtensions = false
case "axioms" => leon.Settings.noForallAxioms = false
case "bapa" => leon.Settings.useBAPA = true
case "impure" => leon.Settings.impureTestcases = true
- case "XP" => leon.Settings.experimental = true
case "BV" => leon.Settings.bitvectorBitwidth = Some(32)
case "prune" => leon.Settings.pruneBranches = true
case "cores" => leon.Settings.useCores = true
case "quickcheck" => leon.Settings.useQuickCheck = true
case "parallel" => leon.Settings.useParallel = true
- //case "noLuckyTests" => leon.Settings.luckyTest = false
case "noverifymodel" => leon.Settings.verifyModel = false
case "imperative" => leon.Settings.synthesis = false;
leon.Settings.transformProgram = true;
@@ -72,10 +62,7 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
leon.Settings.stopAfterTransformation = true;
case s if s.startsWith("debug=") => leon.Settings.debugLevel = try { s.substring("debug=".length, s.length).toInt } catch { case _ => 0 }
- case s if s.startsWith("tags=") => leon.Settings.debugTags = Set(splitList(s.substring("tags=".length, s.length)): _*)
case s if s.startsWith("unrolling=") => leon.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
- case s if s.startsWith("functions=") => leon.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
- case s if s.startsWith("extensions=") => leon.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
case s if s.startsWith("testbounds=") => leon.Settings.testBounds = try { val l = splitList(s.substring("testBounds=".length, s.length)).map(_.toInt); if (l.size != 2) (0, 3) else (l(0), l(1)) } catch { case _ => (0, 3) }
case s if s.startsWith("timeout=") => leon.Settings.solverTimeout = try { Some(s.substring("timeout=".length, s.length).toInt) } catch { case _ => None }
case s if s.startsWith("testcases=") => leon.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 4d202f3b5..ff3e92d5d 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -237,53 +237,6 @@ object Extractors {
}
}
- object NotSoSimplePatternMatching {
- def coversType(tpe: ClassTypeDef, patterns: Seq[Pattern]) : Boolean = {
- if(patterns.isEmpty) {
- false
- } else if(patterns.exists(_.isInstanceOf[WildcardPattern])) {
- true
- } else {
- val allSubtypes: Seq[CaseClassDef] = tpe match {
- case acd @ AbstractClassDef(_,_) => acd.knownDescendents.filter(_.isInstanceOf[CaseClassDef]).map(_.asInstanceOf[CaseClassDef])
- case ccd: CaseClassDef => List(ccd)
- }
-
- var seen: Set[CaseClassDef] = Set.empty
- var secondLevel: Map[(CaseClassDef,Int),List[Pattern]] = Map.empty
-
- for(pat <- patterns) if (pat.isInstanceOf[CaseClassPattern]) {
- val pattern: CaseClassPattern = pat.asInstanceOf[CaseClassPattern]
- val ccd: CaseClassDef = pattern.caseClassDef
- seen = seen + ccd
-
- for((subPattern,i) <- (pattern.subPatterns.zipWithIndex)) {
- val seenSoFar = secondLevel.getOrElse((ccd,i), Nil)
- secondLevel = secondLevel + ((ccd,i) -> (subPattern :: seenSoFar))
- }
- }
-
- allSubtypes.forall(ccd => {
- seen(ccd) && ccd.fields.zipWithIndex.forall(p => p._1.tpe match {
- case t: ClassType => coversType(t.classDef, secondLevel.getOrElse((ccd, p._2), Nil))
- case _ => true
- })
- })
- }
- }
-
- def unapply(pm : MatchExpr) : Option[MatchExpr] = if(!Settings.experimental) None else (pm match {
- case MatchExpr(scrutinee, cases) if cases.forall(_.isInstanceOf[SimpleCase]) => {
- val allPatterns = cases.map(_.pattern)
- Settings.reporter.info("This might be a complete pattern-matching expression:")
- Settings.reporter.info(pm)
- Settings.reporter.info("Covered? " + coversType(pm.scrutineeClassType.classDef, allPatterns))
- None
- }
- case _ => None
- })
- }
-
object TopLevelOrs { // expr1 AND (expr2 AND (expr3 AND ..)) => List(expr1, expr2, expr3)
def unapply(e: Expr): Option[Seq[Expr]] = e match {
case Or(exprs) =>
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 9087c942c..a6125b193 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -223,10 +223,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
reporter.info(" - Initial unrolling...")
val (clauses, guards) = unrollingBank.initialUnrolling(expandedVC)
- for(clause <- clauses) {
- Logger.debug("we're getting a new clause " + clause, 4, "z3solver")
- }
-
val cc = toZ3Formula(And(clauses)).get
z3.assertCnstr(cc)
@@ -271,7 +267,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
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")
// if (Settings.useCores)
// reporter.info(" - Core is : " + core)
@@ -289,7 +284,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
}
case (Some(true), m) => { // SAT
validatingStopwatch.start
- Logger.debug("Model Found: " + m, 4, "z3solver")
val (trueModel, model) = if(Settings.verifyModel)
validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator)
else {
@@ -342,7 +336,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
foundAnswer(Some(true), core = core)
} else {
luckyStopwatch.start
- Logger.debug("Model Found: " + m2, 4, "z3solver")
// we might have been lucky :D
val (wereWeLucky, cleanModel) = validateAndDeleteModel(m2, toCheckAgainstModels, varsInVC, evaluator)
if(wereWeLucky) {
@@ -429,9 +422,6 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
reporter.info(" - more unrollings")
for((id,polarity) <- toReleaseAsPairs) {
val (newClauses,newBlockers) = unrollingBank.unlock(id, !polarity)
- for(clause <- newClauses) {
- Logger.debug("we're getting a new clause " + clause, 4, "z3solver")
- }
for(ncl <- newClauses) {
z3.assertCnstr(toZ3Formula(ncl).get)
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index cbea0d524..ce3dc0198 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -17,10 +17,18 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val description = "Leon Verification"
override def definedOptions = Set(
- LeonFlagOptionDef("no-luck", "--no-luck", "Disable early model detection in solving loop.")
+ LeonValueOptionDef("functions", "--functions=f1:f2", "Limit verification to f1,f2,...")
)
def run(ctx: LeonContext)(program: Program) : VerificationReport = {
+ val functionsToAnalyse : MutableSet[String] = MutableSet.empty
+
+ for(opt <- ctx.options) opt match {
+ case LeonValueOption("functions", ListValue(fs)) =>
+ functionsToAnalyse ++= fs
+ case _ =>
+ }
+
val reporter = ctx.reporter
val trivialSolver = new TrivialSolver(ctx)
@@ -39,7 +47,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
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))) {
+ for(funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1 < fd2) if (functionsToAnalyse.isEmpty || functionsToAnalyse.contains(funDef.id.name))) {
analysedFunctions += funDef.id.name
val tactic: Tactic =
@@ -63,7 +71,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
})
}
- val notFound: Set[String] = Settings.functionsToAnalyse -- analysedFunctions
+ val notFound = functionsToAnalyse -- analysedFunctions
notFound.foreach(fn => reporter.error("Did not find function \"" + fn + "\" though it was marked for analysis."))
allVCs.toList
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 360f41493..ba7a210f1 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -67,8 +67,6 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
new VerificationCondition(Implies(CaseClassInstanceOf(ccd, argAsVar), conditionForChild), funDef, VCKind.Postcondition, this)
case _ => scala.sys.error("Abstract class has non-case class subtype.")
}))
- Logger.debug("Induction tactic yields the following VCs:\n" +
- conditionsForEachChild.map(vc => vc.condition).mkString("\n"), 4, "induction")
conditionsForEachChild
}
case None =>
@@ -133,8 +131,6 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
}
case _ => scala.sys.error("Abstract class has non-case class subtype")
}))
- Logger.debug("Induction tactic yields the following VCs:\n" +
- conditionsForEachChild.map(vc => vc.condition).mkString("\n"), 4, "induction")
conditionsForEachChild
}).toSeq
--
GitLab