diff --git a/src/cp/CPPlugin.scala b/src/cp/CPPlugin.scala
index 1ec9b6a28f2c4b79deec72e90d348fcf3df6a006..4329315f5c6cbaf6b27da02637edcb52934bf5f0 100644
--- a/src/cp/CPPlugin.scala
+++ b/src/cp/CPPlugin.scala
@@ -30,7 +30,6 @@ class CPPlugin(val global: Global) extends PluginBase {
" -P:funcheck:impure Generate testcases only for impure functions" + "\n" +
" -P:funcheck:testcases=[1,2] Number of testcases to generate per function" + "\n" +
" -P:funcheck:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
- " -P:funcheck:quiet No info and warning messages from the extensions" + "\n" +
" -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
" -P:funcheck:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
" -P:funcheck:CAV CAV 2011 settings. In progress." + "\n" +
@@ -47,7 +46,6 @@ class CPPlugin(val global: Global) extends PluginBase {
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 "axioms" => purescala.Settings.noForallAxioms = false
case "nobapa" => purescala.Settings.useBAPA = false
diff --git a/src/funcheck/AnalysisComponent.scala b/src/funcheck/AnalysisComponent.scala
index 7529c3a677af08a14c1891d00d1eefa470e3c912..78dafc2b0e2a3be40d99af3faaf3fdfa4d8549ac 100644
--- a/src/funcheck/AnalysisComponent.scala
+++ b/src/funcheck/AnalysisComponent.scala
@@ -32,16 +32,22 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
println("Extraction complete. Now terminating the compiler process.")
exit(0)
} else {
- println("Extracted program for " + unit + ". Re-run with -P:funcheck:parse to see the output.")
+ if(!pluginInstance.actionAfterExtraction.isDefined) {
+ println("Extracted program for " + unit + ". Re-run with -P:funcheck:parse to see the output.")
+ }
//println(prog)
}
- println("Starting analysis.")
- val analysis = new purescala.Analysis(prog)
- analysis.analyse
- if(pluginInstance.stopAfterAnalysis) {
- println("Analysis complete. Now terminating the compiler process.")
- exit(0)
+ if(!pluginInstance.actionAfterExtraction.isDefined) {
+ println("Starting analysis.")
+ val analysis = new purescala.Analysis(prog)
+ analysis.analyse
+ if(pluginInstance.stopAfterAnalysis) {
+ println("Analysis complete. Now terminating the compiler process.")
+ exit(0)
+ }
+ } else {
+ pluginInstance.actionAfterExtraction.get(prog)
}
}
}
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index c5a70a1ebdd6c74356bac3072d62a6e1d593f7df..4bbc7c3b87e573f32c27631a609decb6094d81ab 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -3,9 +3,10 @@ package funcheck
import scala.tools.nsc
import scala.tools.nsc.{Global,Phase}
import scala.tools.nsc.plugins.{Plugin,PluginComponent}
+import purescala.Definitions.Program
/** This class is the entry point for the plugin. */
-class FunCheckPlugin(val global: Global) extends PluginBase {
+class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Program=>Unit] = None) extends PluginBase {
import global._
val name = "funcheck"
@@ -30,7 +31,6 @@ class FunCheckPlugin(val global: Global) extends PluginBase {
" -P:funcheck:testcases=[1,2] Number of testcases to generate per function" + "\n" +
" -P:funcheck:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
" -P:funcheck:timeout=N Sets a timeout of N seconds (FairZ3 only)" + "\n" +
- " -P:funcheck:quiet No info and warning messages from the extensions" + "\n" +
" -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
" -P:funcheck:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
" -P:funcheck:CAV CAV 2011 settings. In progress." + "\n" +
@@ -47,7 +47,6 @@ class FunCheckPlugin(val global: Global) extends PluginBase {
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 "axioms" => purescala.Settings.noForallAxioms = false
case "nobapa" => purescala.Settings.useBAPA = false
diff --git a/src/funcheck/Main.scala b/src/funcheck/Main.scala
index 330be229ee314fbe2cd29ccea433d970fe4970f3..1b9a703285648bd296fe7a7d550cf3a8abb3dec1 100644
--- a/src/funcheck/Main.scala
+++ b/src/funcheck/Main.scala
@@ -1,14 +1,13 @@
package funcheck
import scala.tools.nsc.{Global,Settings,SubComponent,CompilerCommand}
-import scala.tools.nsc.reporters.{ConsoleReporter,Reporter}
+
+import purescala.Definitions.Program
/** This class is a compiler that will be used for running
* the plugin in standalone mode. Courtesy of D. Zufferey. */
-class PluginRunner(settings : Settings, reporter : Reporter) extends Global(settings, reporter) {
- def this(settings : Settings) = this(settings, new ConsoleReporter(settings))
-
- val funcheckPlugin = new FunCheckPlugin(this)
+class PluginRunner(settings : Settings, reportingFunction : String => Unit, actionOnProgram : Option[Program=>Unit]) extends Global(settings, new SimpleReporter(settings, reportingFunction)) {
+ val funcheckPlugin = new FunCheckPlugin(this, actionOnProgram)
protected def addToPhasesSet(sub : SubComponent, descr : String) : Unit = {
phasesSet += sub
@@ -33,12 +32,24 @@ class PluginRunner(settings : Settings, reporter : Reporter) extends Global(sett
}
object Main {
+ import purescala.{Reporter,DefaultReporter,Definitions,Analysis}
+ import Definitions.Program
+
def main(args: Array[String]): Unit = {
+ main(args, new DefaultReporter)
+ }
+
+ def main(args: Array[String], reporter: Reporter) : Unit = {
val settings = new Settings
- runWithSettings(args, settings)
+ runWithSettings(args, settings, s => reporter.info(s), Some(p => defaultAction(p, reporter)))
+ }
+
+ private def defaultAction(program: Program, reporter: Reporter) : Unit = {
+ val analysis = new Analysis(program, reporter)
+ analysis.analyse
}
- private def runWithSettings(args : Array[String], settings : Settings) : Unit = {
+ private def runWithSettings(args : Array[String], settings : Settings, printerFunction : String=>Unit, actionOnProgram : Option[Program=>Unit] = None) : Unit = {
val (funcheckOptions, nonfuncheckOptions) = args.toList.partition(_.startsWith("--"))
val command = new CompilerCommand(nonfuncheckOptions, settings) {
override val cmdName = "funcheck"
@@ -48,8 +59,10 @@ object Main {
if(settings.version.value) {
println(command.cmdName + " beta.")
} else {
- val runner = new PluginRunner(settings)
+ val runner = new PluginRunner(settings, printerFunction, actionOnProgram)
runner.funcheckPlugin.processOptions(funcheckOptions.map(_.substring(2)), Console.err.println(_))
+ runner.funcheckPlugin.stopAfterExtraction = false
+ runner.funcheckPlugin.stopAfterAnalysis = false
val run = new runner.Run
run.compile(command.files)
}
diff --git a/src/funcheck/SimpleReporter.scala b/src/funcheck/SimpleReporter.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cd20fd8c53a35e7e496a3e6727e95927b505b163
--- /dev/null
+++ b/src/funcheck/SimpleReporter.scala
@@ -0,0 +1,70 @@
+package funcheck
+
+import scala.tools.nsc.Settings
+import scala.tools.nsc.reporters.AbstractReporter
+import scala.tools.nsc.util._
+
+/** This implements a reporter that calls the callback with every line that a
+regular ConsoleReporter would display. */
+class SimpleReporter(val settings: Settings, callback: String => Unit) extends AbstractReporter {
+ final val ERROR_LIMIT = 5
+
+ private def label(severity: Severity): String = severity match {
+ case ERROR => "error"
+ case WARNING => "warning"
+ case INFO => null
+ }
+
+ private def clabel(severity: Severity): String = {
+ val label0 = label(severity)
+ if (label0 eq null) "" else label0 + ": "
+ }
+
+ private def getCountString(severity: Severity): String =
+ countElementsAsString((severity).count, label(severity))
+
+ /** Prints the message. */
+ def printMessage(msg: String) { callback(msg) }
+
+ /** Prints the message with the given position indication. */
+ def printMessage(posIn: Position, msg: String) {
+ val pos = if (posIn eq null) NoPosition
+ else if (posIn.isDefined) posIn.inUltimateSource(posIn.source)
+ else posIn
+ pos match {
+ case FakePos(fmsg) =>
+ printMessage(fmsg+" "+msg)
+ case NoPosition =>
+ printMessage(msg)
+ case _ =>
+ val buf = new StringBuilder(msg)
+ val file = pos.source.file
+ printMessage(pos.line + ": " + msg)
+ printSourceLine(pos)
+ }
+ }
+ def print(pos: Position, msg: String, severity: Severity) {
+ printMessage(pos, clabel(severity) + msg)
+ }
+
+ def printSourceLine(pos: Position) {
+ printMessage(pos.lineContent.stripLineEnd)
+ printColumnMarker(pos)
+ }
+
+ def printColumnMarker(pos: Position) =
+ if (pos.isDefined) { printMessage(" " * (pos.column - 1) + "^") }
+
+ def printSummary() {
+ if (WARNING.count > 0) printMessage(getCountString(WARNING) + " found")
+ if ( ERROR.count > 0) printMessage(getCountString(ERROR ) + " found")
+ }
+
+ def display(pos: Position, msg: String, severity: Severity) {
+ severity.count += 1
+ if (severity != ERROR || severity.count <= ERROR_LIMIT)
+ print(pos, msg, severity)
+ }
+
+ def displayPrompt: Unit = {}
+}
diff --git a/src/purescala/Analysis.scala b/src/purescala/Analysis.scala
index 4abcd0db6f37507add5824458dd76763bb0e0d42..4fb21174dfb2221b780a65d36676d898336e18b9 100644
--- a/src/purescala/Analysis.scala
+++ b/src/purescala/Analysis.scala
@@ -7,12 +7,8 @@ import TypeTrees._
import Extensions._
import scala.collection.mutable.{Set => MutableSet}
-class Analysis(val program: Program) {
- // we always use the global reporter for this class
- val reporter = Settings.reporter
- // ...but not always for the extensions
-
- Extensions.loadAll
+class Analysis(val program: Program, val reporter: Reporter = Settings.reporter) {
+ Extensions.loadAll(reporter)
val analysisExtensions: Seq[Analyser] = loadedAnalysisExtensions
@@ -308,32 +304,4 @@ object Analysis {
val result = searchAndReplaceDFS(applyToCall)(expression)
liftLets(Implies(And(trueThings.reverse), result))
}
-
- // Rewrites pattern matching expressions where the cases simply correspond to
- // the list of constructors
- // def rewriteSimplePatternMatching(expression: Expr) : Expr = {
- // var extras : List[Expr] = Nil
-
- // def rewritePM(e: Expr) : Option[Expr] = e match {
- // // case NotSoSimplePatternMatching(_) => None
- // case SimplePatternMatching(scrutinee, classType, casesInfo) => {
- // val newVar = Variable(FreshIdentifier("pm", true)).setType(e.getType)
- // val scrutAsLetID = FreshIdentifier("scrut", true).setType(scrutinee.getType)
- // val lle : List[(Variable,List[Expr])] = casesInfo.map(cseInfo => {
- // val (ccd, newPID, argIDs, rhs) = cseInfo
- // val newPVar = Variable(newPID)
- // val argVars = argIDs.map(Variable(_))
- // (newPVar, List(Equals(newPVar, CaseClass(ccd, argVars)), Implies(Equals(Variable(scrutAsLetID), newPVar), Equals(newVar, rhs))))
- // }).toList
- // val (newPVars, newExtras) = lle.unzip
- // extras = Let(scrutAsLetID, scrutinee, And(Or(newPVars.map(Equals(Variable(scrutAsLetID), _))), And(newExtras.flatten))) :: extras
- // Some(newVar)
- // }
- // case m @ MatchExpr(s,_) => Settings.reporter.error("Untranslatable PM expression on type " + s.getType + " : " + m); None
- // case _ => None
- // }
-
- // val newExpr = searchAndReplaceDFS(rewritePM)(expression)
- // liftLets(Implies(And(extras), newExpr))
- // }
}
diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala
index 6e50cda68cae1e9427aa34c2b6ac342380997016..ca89dc913820259829df445268cc5dec5592261c 100644
--- a/src/purescala/Extensions.scala
+++ b/src/purescala/Extensions.scala
@@ -44,13 +44,7 @@ object Extensions {
private var solverExtensions : Seq[Solver] = Nil
// Returns the list of the newly loaded.
- def loadAll : Seq[Extension] = {
- val extensionsReporter =
- if(Settings.quietExtensions) {
- Settings.quietReporter
- } else {
- Settings.reporter
- }
+ def loadAll(extensionsReporter : Reporter = Settings.reporter) : Seq[Extension] = {
val allNames: Seq[String] = Settings.extensionNames
val loaded = (if(!allNames.isEmpty) {
val classLoader = Extensions.getClass.getClassLoader
@@ -85,11 +79,13 @@ object Extensions {
}
// these extensions are always loaded, unless specified otherwise
val defaultExtensions: Seq[Extension] = if(Settings.runDefaultExtensions) {
- if(Settings.useFairInstantiator) {
- (new FairZ3Solver(extensionsReporter) :: Nil)
+ //(new TestExtension(extensionsReporter)) ::
+ (if(Settings.useFairInstantiator) {
+ (new FairZ3Solver(extensionsReporter))
} else {
- (new Z3Solver(extensionsReporter)) :: Nil
- }
+ (new Z3Solver(extensionsReporter))
+ }) ::
+ Nil
} else {
Nil
}
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 590f90b3f3d3650772a7c934e1de238d2c17b61b..8926d06ee921575468e52c8b4648d741b32ef137 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -4,11 +4,9 @@ package purescala
object Settings {
var experimental : Boolean = false
var showIDs: Boolean = false
- var quietExtensions: Boolean = false
var functionsToAnalyse: Set[String] = Set.empty
var extensionNames: Seq[String] = Nil
- var reporter: Reporter = new DefaultReporter
- var quietReporter: Reporter = new QuietReporter
+ lazy val reporter: Reporter = new DefaultReporter
var runDefaultExtensions: Boolean = true
var noForallAxioms: Boolean = true
var unrollingLevel: Int = 0
diff --git a/src/purescala/TestExtension.scala b/src/purescala/TestExtension.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f2995d1e1e58ae6a7abea2ea0e3d401dc4eaeff8
--- /dev/null
+++ b/src/purescala/TestExtension.scala
@@ -0,0 +1,107 @@
+package purescala
+
+import purescala.Common._
+import purescala.Trees._
+import purescala.TypeTrees._
+import purescala.Definitions._
+import purescala.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.Predef.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/testcases/PaperDemoExample.scala b/testcases/PaperDemoExample.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a55c26f48814b811bc42c157b1b7a117c9367c7f
--- /dev/null
+++ b/testcases/PaperDemoExample.scala
@@ -0,0 +1,19 @@
+object PaperDemoexample {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ })
+
+ def sizeTailRec(l: List) : Int = sizeAcc(l, 0)
+ def sizeAcc(l: List, acc: Int) : Int = {
+ require(acc >= 0)
+ l match {
+ case Nil() => acc
+ case Cons(_, xs) => sizeAcc(xs, acc+1)
+ }
+ } ensuring(res => res == size(l) + acc)
+}