diff --git a/funcheck b/funcheck deleted file mode 100755 index 3af3d261ad792d2de590eb1651a87397b81aca62..0000000000000000000000000000000000000000 --- a/funcheck +++ /dev/null @@ -1,24 +0,0 @@ -#!/bin/bash - -runner="./scalac-funcheck" -newargs="" - -for arg in $@ -do - if [ -e ${arg} ] - then - newargs="${newargs} ${arg}" - else - newargs="${newargs} -P:funcheck:${arg}" - fi -done - -if [ -e ${runner} ] -then - ${runner} ${newargs} - exit 0 -else - echo "${runner} not found. Have you run 'sbt all' ?" - exit 1 -fi - diff --git a/project/build/funcheck.scala b/project/build/funcheck.scala index 30521628ec2dce3816037e144467e916b3a6cb95..b4e503d0eaa94af58caf64f0f1dd5584dbcec348 100644 --- a/project/build/funcheck.scala +++ b/project/build/funcheck.scala @@ -16,7 +16,7 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT lazy val extensionJars : List[Path] = multisetsLib.jarPath :: multisets.jarPath :: orderedsets.jarPath :: setconstraints.jarPath :: Nil - val scriptPath: Path = "." / "scalac-funcheck" + val scriptPath: Path = "." / "funcheck" lazy val all = task { None } dependsOn(generateScript) describedAs("Compile everything and produce a script file.") @@ -49,14 +49,15 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT fw.write(purescala.jarPath.absolutePath) fw.write("\"" + nl + nl) fw.write("LD_LIBRARY_PATH=" + ("." / "lib-bin").absolutePath + " \\" + nl) - fw.write("java -Xmx1024M \\" + nl) + fw.write("scala -classpath ${FUNCHECKCLASSPATH}:${SCALACCLASSPATH}" + " \\" + nl) + fw.write("funcheck.Main -cp " + plugin.jarPath.absolutePath + " $@" + nl) + // fw.write("java -Xmx1024M \\" + nl) + // // This is a hack :( + // val libStr = (buildLibraryJar.absolutePath).toString + // fw.write(" -Dscala.home=" + libStr.substring(0, libStr.length-21) + " \\" + nl) - // This is a hack :( - val libStr = (buildLibraryJar.absolutePath).toString - fw.write(" -Dscala.home=" + libStr.substring(0, libStr.length-21) + " \\" + nl) - - fw.write(" -classpath ${FUNCHECKCLASSPATH} \\" + nl) - fw.write(" scala.tools.nsc.Main -Xplugin:" + plugin.jarPath.absolutePath + " -classpath ${SCALACCLASSPATH} $@" + nl) + // fw.write(" -classpath ${FUNCHECKCLASSPATH} \\" + nl) + // fw.write(" scala.tools.nsc.Main -Xplugin:" + plugin.jarPath.absolutePath + " -classpath ${SCALACCLASSPATH} $@" + nl) fw.close f.setExecutable(true) None diff --git a/src/funcheck/DefaultMain.scala b/src/funcheck/DefaultMain.scala deleted file mode 100644 index 7a4c7d296ab1c22e04564595629e47eacf2e05db..0000000000000000000000000000000000000000 --- a/src/funcheck/DefaultMain.scala +++ /dev/null @@ -1,8 +0,0 @@ -package funcheck - -object DefaultMain { - def main(args: Array[String]): Unit = { - println("Please use funCheck as a scalac plugin, running:") - println(" scalac -Xplugin:funcheck-plugin.jar ...") - } -} diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala index 09ba190b4042dd9f2e932817ace22b501d883042..ceb7611f15320eb3962806e306336f9a529a0956 100644 --- a/src/funcheck/FunCheckPlugin.scala +++ b/src/funcheck/FunCheckPlugin.scala @@ -68,4 +68,6 @@ class FunCheckPlugin(val global: Global) extends Plugin { } } - val components = List[PluginComponent](new AnalysisComponent(global, this))} + val components = List[PluginComponent](new AnalysisComponent(global, this)) + val descriptions = List[String]("funcheck analyses") +} diff --git a/src/funcheck/Main.scala b/src/funcheck/Main.scala new file mode 100644 index 0000000000000000000000000000000000000000..330be229ee314fbe2cd29ccea433d970fe4970f3 --- /dev/null +++ b/src/funcheck/Main.scala @@ -0,0 +1,58 @@ +package funcheck + +import scala.tools.nsc.{Global,Settings,SubComponent,CompilerCommand} +import scala.tools.nsc.reporters.{ConsoleReporter,Reporter} + +/** 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) + + protected def addToPhasesSet(sub : SubComponent, descr : String) : Unit = { + phasesSet += sub + } + + /** The phases to be run. */ + override protected def computeInternalPhases() : Unit = { + val phs = List( + syntaxAnalyzer -> "parse source into ASTs, perform simple desugaring", + analyzer.namerFactory -> "resolve names, attach symbols to named trees", + analyzer.packageObjects -> "load package objects", + analyzer.typerFactory -> "the meat and potatoes: type the trees", + superAccessors -> "add super accessors in traits and nested classes", + pickler -> "serialize symbol tables", + refchecks -> "reference and override checking, translate nested objects" + ) ::: { + val zipped = funcheckPlugin.components zip funcheckPlugin.descriptions + zipped + } + phs foreach (addToPhasesSet _).tupled + } +} + +object Main { + def main(args: Array[String]): Unit = { + val settings = new Settings + runWithSettings(args, settings) + } + + private def runWithSettings(args : Array[String], settings : Settings) : Unit = { + val (funcheckOptions, nonfuncheckOptions) = args.toList.partition(_.startsWith("--")) + val command = new CompilerCommand(nonfuncheckOptions, settings) { + override val cmdName = "funcheck" + } + + if(command.ok) { + if(settings.version.value) { + println(command.cmdName + " beta.") + } else { + val runner = new PluginRunner(settings) + runner.funcheckPlugin.processOptions(funcheckOptions.map(_.substring(2)), Console.err.println(_)) + val run = new runner.Run + run.compile(command.files) + } + } + } +} diff --git a/vstte10competition/SumAndMax.scala b/vstte10competition/SumAndMax.scala new file mode 100644 index 0000000000000000000000000000000000000000..2410dff5d428a0ef9c12687d0f8ec023a8f682a4 --- /dev/null +++ b/vstte10competition/SumAndMax.scala @@ -0,0 +1,46 @@ +import scala.collection.immutable.Set +import funcheck.Utils._ +import funcheck.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 = { + require(allPos(list)) + sum(list) <= size(list) * (if(list == Nil()) 0 else max(list)) + } holds +}