From 60d26eecd28b4785a3e2803d38f231f1c03d6e4f Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Wed, 30 Jun 2010 13:22:32 +0000
Subject: [PATCH] Some new plugin options. Also: now tries all loaded solvers
in order.
---
src/funcheck/FunCheckPlugin.scala | 4 +-
src/purescala/Analysis.scala | 169 ++++++++++++------------------
src/purescala/Extensions.scala | 1 +
src/purescala/Reporter.scala | 21 ++--
src/purescala/Settings.scala | 4 +-
5 files changed, 88 insertions(+), 111 deletions(-)
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index c2bcb978c..934b89b3d 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -22,7 +22,8 @@ class FunCheckPlugin(val global: Global) extends Plugin {
" -P:funcheck:parse Checks only whether the program is valid PureScala" + "\n" +
" -P:funcheck:extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
" -P:funcheck:nodefaults Runs only the analyses provided by the extensions" + "\n" +
- " -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''"
+ " -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
+ " -P:funcheck:quiet No info and warning messages from the extensions"
)
/** Processes the command-line options. */
@@ -33,6 +34,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
case "uniqid" => purescala.Settings.showIDs = true
case "parse" => stopAfterExtraction = true
case "tolerant" => silentlyTolerateNonPureBodies = true
+ case "quiet" => purescala.Settings.quietExtensions = true
case "nodefaults" => purescala.Settings.runDefaultExtensions = false
case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = s.substring("extensions=".length, s.length)
case _ => error("Invalid option: " + option)
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index 7701dca51..a1c312ef9 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -8,15 +8,51 @@ import z3.scala._
import Extensions._
class Analysis(val program: Program) {
+ // we always use the global reporter for this class
val reporter = Settings.reporter
- val extensions: Seq[Extension] = loadAll(reporter)
+ // ...but not always for the extensions
+ val extensionsReporter =
+ if(Settings.quietExtensions) {
+ Settings.quietReporter
+ } else {
+ Settings.reporter
+ }
+
+ // these extensions are always loaded, unless specified otherwise
+ val defaultExtensions: Seq[Extension] =
+ if(Settings.runDefaultExtensions) {
+ (new Z3Solver(extensionsReporter)) :: Nil
+ } else {
+ Nil
+ }
+
+ // we load additional extensions
+ val moreExtensions: Seq[Extension] = loadAll(extensionsReporter)
+ if(!moreExtensions.isEmpty) {
+ reporter.info("The following extensions are loaded:\n" + moreExtensions.toList.map(_.description).mkString(" ", "\n ", ""))
+ }
+ // ...and split the final list between solvers and analysers
+ val extensions: Seq[Extension] = defaultExtensions ++ moreExtensions
val analysisExtensions: Seq[Analyser] = extensions.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser])
val solverExtensions: Seq[Solver] = extensions.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
- if(!extensions.isEmpty) {
- reporter.info("The following extensions are loaded:\n" + extensions.toList.map(_.description).mkString(" ", "\n ", ""))
+ // 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 = {
+ if(solverExtensions.size > 0) {
+ reporter.info("Running verification condition generation...")
+ checkVerificationConditions
+ }
+
+ analysisExtensions.foreach(ae => {
+ reporter.info("Running analysis from extension: " + ae.description)
+ ae.analyse(program)
+ })
}
+ def checkVerificationConditions : Unit = {
// Analysis should check that:
// - all the postconditions are implied by preconds. + body
// - all callsites satisfy the preconditions
@@ -25,57 +61,35 @@ class Analysis(val program: Program) {
// - catamorphisms are catamorphisms (poss. with surjectivity conds.)
// - injective functions are injective
// - all global invariants are satisfied
- def analyse : Unit = {
- if(Settings.runDefaultExtensions || solverExtensions.size > 0) {
- val z3cfg = new Z3Config()
- z3cfg.setParamValue("MODEL", "true")
- val z3 = new Z3Context(z3cfg)
-
- program.mainObject.defs.filter(_.isInstanceOf[FunDef]).foreach(df => {
- val funDef = df.asInstanceOf[FunDef]
-
- if(funDef.body.isDefined) {
- val vc = postconditionVC(funDef)
- if(vc != BooleanLiteral(true)) {
- reporter.info("Verification condition (post) for " + funDef.id + ":")
- reporter.info(vc)
-
- if(Settings.runDefaultExtensions) {
- val z3f = toZ3Formula(z3, vc)
- z3.assertCnstr(z3.mkNot(z3f))
- //z3.print
- z3.checkAndGetModel() match {
- case (Some(true),m) => {
- reporter.error("There's a bug! Here's a model for a counter-example:")
- m.print
- }
- case (Some(false),_) => reporter.info("Contract satisfied!")
- case (None,_) => reporter.error("Z3 couldn't run properly or does not know the answer :(")
- }
- }
-
- solverExtensions.foreach(se => {
- reporter.info("Trying with solver: " + se.description)
- se.solve(vc) match {
- case None => reporter.warning("result unknown")
- case Some(true) => reporter.info("valid!")
- case Some(false) => reporter.error("invalid :(")
- }
- })
- }
- } else {
- if(funDef.postcondition.isDefined) {
- reporter.warning(funDef, "Could not verify postcondition: function implementation is unknown.")
- }
+ program.mainObject.defs.filter(_.isInstanceOf[FunDef]).foreach(df => {
+ val funDef = df.asInstanceOf[FunDef]
+
+ if(funDef.body.isDefined) {
+ val vc = postconditionVC(funDef)
+ if(vc != BooleanLiteral(true)) {
+ reporter.info("Verification condition (post) for " + funDef.id + ":")
+ reporter.info(vc)
+
+ if(Settings.runDefaultExtensions) {
+ }
+
+ // try all solvers until one returns a meaningful answer
+ solverExtensions.find(se => {
+ reporter.info("Trying with solver: " + se.description)
+ se.solve(vc) match {
+ case None => reporter.warning("UNKNOWN"); false
+ case Some(true) => reporter.info("VALID"); true
+ case Some(false) => reporter.error("INVALID"); true
}
- })
+ })
+ }
+ } else {
+ if(funDef.postcondition.isDefined) {
+ reporter.warning(funDef, "Could not verify postcondition: function implementation is unknown.")
+ }
}
-
- analysisExtensions.foreach(ae => {
- reporter.info("Now running analysis from extension: " + ae.description)
- ae.analyse(program)
- })
- }
+ })
+ }
def postconditionVC(functionDefinition: FunDef) : Expr = {
assert(functionDefinition.body.isDefined)
@@ -129,55 +143,4 @@ class Analysis(val program: Program) {
rec(expr)
}
-
- def toZ3Formula(z3: Z3Context, expr: Expr) : (Z3AST) = {
- lazy val intSort = z3.mkIntSort()
- lazy val boolSort = z3.mkBoolSort()
-
- // because we create identifiers the first time we see them, this is
- // convenient.
- var z3Vars: Map[Identifier,Z3AST] = Map.empty
-
- def rec(ex: Expr) : Z3AST = ex match {
- case Let(i,e,b) => {
- z3Vars = z3Vars + (i -> rec(e))
- rec(b)
- }
- case v @ Variable(id) => z3Vars.get(id) match {
- case Some(ast) => ast
- case None => {
- val newAST = if(v.getType == Int32Type) {
- z3.mkConst(z3.mkStringSymbol(id.name), intSort)
- } else if(v.getType == BooleanType) {
- z3.mkConst(z3.mkStringSymbol(id.name), boolSort)
- } else {
- reporter.fatalError("Unsupported type in Z3 transformation: " + v.getType)
- }
- z3Vars = z3Vars + (id -> newAST)
- newAST
- }
- }
- case IfExpr(c,t,e) => z3.mkITE(rec(c), rec(t), rec(e))
- case And(exs) => z3.mkAnd(exs.map(rec(_)) : _*)
- case Or(exs) => z3.mkOr(exs.map(rec(_)) : _*)
- case Not(Equals(l,r)) => z3.mkDistinct(rec(l),rec(r))
- case Not(e) => z3.mkNot(rec(e))
- case Implies(l,r) => z3.mkImplies(rec(l), rec(r))
- case IntLiteral(v) => z3.mkInt(v, intSort)
- case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
- case Equals(l,r) => z3.mkEq(rec(l),rec(r))
- case Plus(l,r) => z3.mkAdd(rec(l), rec(r))
- case Minus(l,r) => z3.mkSub(rec(l), rec(r))
- case Times(l,r) => z3.mkMul(rec(l), rec(r))
- case Division(l,r) => z3.mkDiv(rec(l), rec(r))
- case UMinus(e) => z3.mkUnaryMinus(rec(e))
- case LessThan(l,r) => z3.mkLT(rec(l), rec(r))
- case LessEquals(l,r) => z3.mkLE(rec(l), rec(r))
- case GreaterThan(l,r) => z3.mkGT(rec(l), rec(r))
- case GreaterEquals(l,r) => z3.mkGE(rec(l), rec(r))
- case _ => scala.Predef.error("Can't handle this in translation to Z3: " + ex)
- }
-
- rec(expr)
- }
}
diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala
index 042b3c964..b57f61a7b 100644
--- a/src/purescala/Extensions.scala
+++ b/src/purescala/Extensions.scala
@@ -6,6 +6,7 @@ import purescala.Definitions._
object Extensions {
sealed abstract class Extension(reporter: Reporter) {
val description: String
+ val shortDescription: String = description
}
abstract class Solver(reporter: Reporter) extends Extension(reporter) {
diff --git a/src/purescala/Reporter.scala b/src/purescala/Reporter.scala
index 4c9eaecc0..7261d1121 100644
--- a/src/purescala/Reporter.scala
+++ b/src/purescala/Reporter.scala
@@ -20,17 +20,17 @@ abstract class Reporter {
def fatalError(expr: Expr, msg: Any) : Nothing
}
-object DefaultReporter extends Reporter {
- private val errorPfx = "[ Error ] "
- private val warningPfx = "[Warning] "
- private val infoPfx = "[ Info ] "
- private val fatalPfx = "[ Fatal ] "
+class DefaultReporter extends Reporter {
+ protected val errorPfx = "[ Error ] "
+ protected val warningPfx = "[Warning] "
+ protected val infoPfx = "[ Info ] "
+ protected val fatalPfx = "[ Fatal ] "
def output(msg: String) : Unit = {
Console.err.println(msg)
}
- private def reline(pfx: String, msg: String) : String = {
+ protected def reline(pfx: String, msg: String) : String = {
val color = if(pfx == errorPfx || pfx == warningPfx || pfx == fatalPfx) {
Console.RED
} else {
@@ -53,3 +53,12 @@ object DefaultReporter extends Reporter {
def info(expr: Expr, msg: Any) = output(reline(infoPfx, PrettyPrinter(expr) + "\n" + msg.toString))
def fatalError(expr: Expr, msg: Any) = { output(reline(fatalPfx, PrettyPrinter(expr) + "\n" + msg.toString)); exit(0) }
}
+
+class QuietReporter extends DefaultReporter {
+ override def warning(msg: Any) = {}
+ override def info(msg: Any) = {}
+ override def warning(definition: Definition, msg: Any) = {}
+ override def info(definition: Definition, msg: Any) = {}
+ override def warning(expr: Expr, msg: Any) = {}
+ override def info(expr: Expr, msg: Any) = {}
+}
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 1a0046e62..8e356550e 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -3,7 +3,9 @@ package purescala
// typically these settings can be changed through some command-line switch.
object Settings {
var showIDs: Boolean = false
+ var quietExtensions: Boolean = false
var extensionNames: String = ""
- var reporter: Reporter = DefaultReporter
+ var reporter: Reporter = new DefaultReporter
+ var quietReporter: Reporter = new QuietReporter
var runDefaultExtensions: Boolean = true
}
--
GitLab