From c84f20629c861867e75c8b6bc3f67c99ca75da86 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 5 Mar 2012 17:34:31 +0100
Subject: [PATCH] overdue refactoring (funcheck=>leon and single package)
---
src/main/scala/funcheck/FunCheckPlugin.scala | 79 ------------------
.../AbstractZ3Solver.scala | 48 +++++------
.../scala/{purescala => leon}/Analysis.scala | 10 +--
.../{funcheck => leon}/Annotations.scala | 2 +-
.../{purescala => leon}/DefaultTactic.scala | 2 +-
.../scala/{purescala => leon}/Evaluator.scala | 8 +-
.../{purescala => leon}/Extensions.scala | 2 +-
.../{purescala => leon}/FairZ3Solver.scala | 46 +++++------
.../FunctionTemplate.scala | 11 +--
.../{purescala => leon}/InductionTactic.scala | 2 +-
.../{purescala => leon}/ParallelSolver.scala | 10 +--
.../{purescala => leon}/RandomSolver.scala | 10 +--
.../scala/{purescala => leon}/Reporter.scala | 3 +-
.../scala/{purescala => leon}/Settings.scala | 2 +-
.../scala/{purescala => leon}/Stopwatch.scala | 2 +-
.../{purescala => leon}/TestExtension.scala | 4 +-
.../{purescala => leon}/TimeoutSolver.scala | 10 +--
.../scala/{purescala => leon}/Timer.scala | 2 +-
.../{purescala => leon}/TrivialSolver.scala | 10 +--
src/main/scala/{funcheck => leon}/Utils.scala | 2 +-
.../VerificationCondition.scala | 8 +-
.../Z3ModelReconstruction.scala | 10 +--
.../{purescala => leon}/isabelle/Main.scala | 20 ++---
.../scala/{purescala => leon}/isabelle/README | 0
.../isabelle/StrongConnectedComponents.scala | 20 ++---
.../plugin}/AnalysisComponent.scala | 11 +--
.../plugin}/CodeExtraction.scala | 7 +-
.../plugin}/Extractors.scala | 7 +-
src/main/scala/leon/plugin/LeonPlugin.scala | 80 +++++++++++++++++++
.../{funcheck => leon/plugin}/Main.scala | 21 +++--
.../plugin}/SimpleReporter.scala | 3 +-
.../scala/{ => leon}/purescala/Common.scala | 3 +-
.../{ => leon}/purescala/Definitions.scala | 1 +
.../{ => leon}/purescala/PrettyPrinter.scala | 2 +-
.../scala/{ => leon}/purescala/Trees.scala | 1 +
.../{ => leon}/purescala/TypeTrees.scala | 1 +
.../z3plugins/bapa/AST.scala | 0
.../z3plugins/bapa/BAPATheory.scala | 0
.../z3plugins/bapa/BAPATheoryBubbles.scala | 0
.../z3plugins/bapa/BAPATheoryEqc.scala | 0
.../z3plugins/bapa/Bubbles.scala | 0
.../z3plugins/bapa/NormalForms.scala | 0
.../z3plugins/bapa/PrettyPrinter.scala | 0
.../z3plugins/bapa/VennRegions.scala | 0
.../sas2011-testcases/ListOperations.scala | 4 +-
45 files changed, 239 insertions(+), 225 deletions(-)
delete mode 100644 src/main/scala/funcheck/FunCheckPlugin.scala
rename src/main/scala/{purescala => leon}/AbstractZ3Solver.scala (65%)
rename src/main/scala/{purescala => leon}/Analysis.scala (98%)
rename src/main/scala/{funcheck => leon}/Annotations.scala (86%)
rename src/main/scala/{purescala => leon}/DefaultTactic.scala (99%)
rename src/main/scala/{purescala => leon}/Evaluator.scala (99%)
rename src/main/scala/{purescala => leon}/Extensions.scala (99%)
rename src/main/scala/{purescala => leon}/FairZ3Solver.scala (97%)
rename src/main/scala/{purescala => leon}/FunctionTemplate.scala (97%)
rename src/main/scala/{purescala => leon}/InductionTactic.scala (99%)
rename src/main/scala/{purescala => leon}/ParallelSolver.scala (96%)
rename src/main/scala/{purescala => leon}/RandomSolver.scala (97%)
rename src/main/scala/{purescala => leon}/Reporter.scala (98%)
rename src/main/scala/{purescala => leon}/Settings.scala (98%)
rename src/main/scala/{purescala => leon}/Stopwatch.scala (98%)
rename src/main/scala/{purescala => leon}/TestExtension.scala (98%)
rename src/main/scala/{purescala => leon}/TimeoutSolver.scala (83%)
rename src/main/scala/{purescala => leon}/Timer.scala (97%)
rename src/main/scala/{purescala => leon}/TrivialSolver.scala (81%)
rename src/main/scala/{funcheck => leon}/Utils.scala (92%)
rename src/main/scala/{purescala => leon}/VerificationCondition.scala (94%)
rename src/main/scala/{purescala => leon}/Z3ModelReconstruction.scala (95%)
rename src/main/scala/{purescala => leon}/isabelle/Main.scala (99%)
rename src/main/scala/{purescala => leon}/isabelle/README (100%)
rename src/main/scala/{purescala => leon}/isabelle/StrongConnectedComponents.scala (95%)
rename src/main/scala/{funcheck => leon/plugin}/AnalysisComponent.scala (89%)
rename src/main/scala/{funcheck => leon/plugin}/CodeExtraction.scala (99%)
rename src/main/scala/{funcheck => leon/plugin}/Extractors.scala (99%)
create mode 100644 src/main/scala/leon/plugin/LeonPlugin.scala
rename src/main/scala/{funcheck => leon/plugin}/Main.scala (80%)
rename src/main/scala/{funcheck => leon/plugin}/SimpleReporter.scala (98%)
rename src/main/scala/{ => leon}/purescala/Common.scala (98%)
rename src/main/scala/{ => leon}/purescala/Definitions.scala (99%)
rename src/main/scala/{ => leon}/purescala/PrettyPrinter.scala (99%)
rename src/main/scala/{ => leon}/purescala/Trees.scala (99%)
rename src/main/scala/{ => leon}/purescala/TypeTrees.scala (99%)
rename src/main/scala/{purescala => leon}/z3plugins/bapa/AST.scala (100%)
rename src/main/scala/{purescala => leon}/z3plugins/bapa/BAPATheory.scala (100%)
rename src/main/scala/{purescala => leon}/z3plugins/bapa/BAPATheoryBubbles.scala (100%)
rename src/main/scala/{purescala => leon}/z3plugins/bapa/BAPATheoryEqc.scala (100%)
rename src/main/scala/{purescala => leon}/z3plugins/bapa/Bubbles.scala (100%)
rename src/main/scala/{purescala => leon}/z3plugins/bapa/NormalForms.scala (100%)
rename src/main/scala/{purescala => leon}/z3plugins/bapa/PrettyPrinter.scala (100%)
rename src/main/scala/{purescala => leon}/z3plugins/bapa/VennRegions.scala (100%)
diff --git a/src/main/scala/funcheck/FunCheckPlugin.scala b/src/main/scala/funcheck/FunCheckPlugin.scala
deleted file mode 100644
index 8799f320f..000000000
--- a/src/main/scala/funcheck/FunCheckPlugin.scala
+++ /dev/null
@@ -1,79 +0,0 @@
-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, val actionAfterExtraction : Option[Program=>Unit] = None) extends Plugin {
- import global._
-
- val name = "funcheck"
- val description = "Static analysis for Scala by LARA."
-
- var stopAfterAnalysis: Boolean = true
- var stopAfterExtraction: Boolean = false
- var silentlyTolerateNonPureBodies: Boolean = false
-
- /** The help message displaying the options for that plugin. */
- override val optionsHelp: Option[String] = Some(
- " -P:funcheck:uniqid When pretty-printing funcheck trees, show identifiers IDs" + "\n" +
- " -P:funcheck:with-code Allows the compiler to keep running after the static analysis" + "\n" +
- " -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:functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
- " -P:funcheck:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
- " -P:funcheck:axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
- " -P:funcheck:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
- " -P:funcheck:bapa Use BAPA Z3 extension (incompatible with many other things)" + "\n" +
- " -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:timeout=N Sets a timeout of N seconds" + "\n" +
- " -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
- " -P:funcheck:BV Use bit-vectors for integers" + "\n" +
- " -P:funcheck:prune Use additional SMT queries to rule out some unrollings" + "\n" +
- " -P:funcheck:cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
- " -P:funcheck:quickcheck Use QuickCheck-like random search" + "\n" +
- " -P:funcheck:parallel Run all solvers in parallel" + "\n" +
- " -P:funcheck:templates Use new ``FunctionTemplate'' technique" + "\n" +
- " -P:funcheck:noLuckyTests Do not perform additional tests to potentially find models early"
- )
-
- /** Processes the command-line options. */
- private def splitList(lst: String) : Seq[String] = lst.split(':').map(_.trim).filter(!_.isEmpty)
- override def processOptions(options: List[String], error: String => Unit) {
- for(option <- options) {
- option match {
- case "with-code" => stopAfterAnalysis = false
- case "uniqid" => purescala.Settings.showIDs = true
- case "parse" => stopAfterExtraction = true
- case "tolerant" => silentlyTolerateNonPureBodies = true
- case "nodefaults" => purescala.Settings.runDefaultExtensions = false
- case "axioms" => purescala.Settings.noForallAxioms = false
- case "bapa" => purescala.Settings.useBAPA = true
- case "impure" => purescala.Settings.impureTestcases = true
- case "XP" => purescala.Settings.experimental = true
- case "BV" => purescala.Settings.bitvectorBitwidth = Some(32)
- case "prune" => purescala.Settings.pruneBranches = true
- case "cores" => purescala.Settings.useCores = true
- case "quickcheck" => purescala.Settings.useQuickCheck = true
- case "parallel" => purescala.Settings.useParallel = true
- case "templates" => purescala.Settings.useTemplates = true
- case "noLuckyTests" => purescala.Settings.luckyTest = false
- case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
- case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
- case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
- case s if s.startsWith("testbounds=") => purescala.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=") => purescala.Settings.solverTimeout = try { Some(s.substring("timeout=".length, s.length).toInt) } catch { case _ => None }
- case s if s.startsWith("testcases=") => purescala.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
- case _ => error("Invalid option: " + option)
- }
- }
- }
-
- val components = List[PluginComponent](new AnalysisComponent(global, this))
- val descriptions = List[String]("funcheck analyses")
-}
diff --git a/src/main/scala/purescala/AbstractZ3Solver.scala b/src/main/scala/leon/AbstractZ3Solver.scala
similarity index 65%
rename from src/main/scala/purescala/AbstractZ3Solver.scala
rename to src/main/scala/leon/AbstractZ3Solver.scala
index 771dc934d..5c1fc48fa 100644
--- a/src/main/scala/purescala/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/AbstractZ3Solver.scala
@@ -1,11 +1,11 @@
-package purescala
+package leon
import z3.scala._
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
@@ -19,29 +19,29 @@ trait AbstractZ3Solver {
class CantTranslateException(t: Z3AST) extends Exception("Can't translate from Z3 tree: " + t)
- protected[purescala] var z3 : Z3Context
- protected[purescala] var program : Program
+ protected[leon] var z3 : Z3Context
+ protected[leon] var program : Program
def typeToSort(tt: TypeTree): Z3Sort
- protected[purescala] var adtTesters: Map[CaseClassDef, Z3FuncDecl]
- protected[purescala] var adtConstructors: Map[CaseClassDef, Z3FuncDecl]
- protected[purescala] var adtFieldSelectors: Map[Identifier, Z3FuncDecl]
+ protected[leon] var adtTesters: Map[CaseClassDef, Z3FuncDecl]
+ protected[leon] var adtConstructors: Map[CaseClassDef, Z3FuncDecl]
+ protected[leon] var adtFieldSelectors: Map[Identifier, Z3FuncDecl]
- protected[purescala] val mapRangeSorts: MutableMap[TypeTree, Z3Sort]
- protected[purescala] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl]
- protected[purescala] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl]
- protected[purescala] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl]
- protected[purescala] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl]
- protected[purescala] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl]
+ protected[leon] val mapRangeSorts: MutableMap[TypeTree, Z3Sort]
+ protected[leon] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl]
+ protected[leon] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl]
+ protected[leon] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl]
+ protected[leon] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl]
+ protected[leon] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl]
- protected[purescala] var funSorts: Map[TypeTree, Z3Sort]
- protected[purescala] var funDomainConstructors: Map[TypeTree, Z3FuncDecl]
- protected[purescala] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]]
+ protected[leon] var funSorts: Map[TypeTree, Z3Sort]
+ protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl]
+ protected[leon] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]]
- protected[purescala] var exprToZ3Id : Map[Expr,Z3AST]
- protected[purescala] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree]) : Expr
+ protected[leon] var exprToZ3Id : Map[Expr,Z3AST]
+ protected[leon] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree]) : Expr
- protected[purescala] def softFromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: TypeTree) : Option[Expr] = {
+ protected[leon] def softFromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: TypeTree) : Option[Expr] = {
try {
Some(fromZ3Formula(model, tree, Some(expectedType)))
} catch {
@@ -49,9 +49,9 @@ trait AbstractZ3Solver {
}
}
- protected[purescala] def solveWithBounds(vc: Expr, forValidity: Boolean) : (Option[Boolean], Map[Identifier, Expr])
+ protected[leon] def solveWithBounds(vc: Expr, forValidity: Boolean) : (Option[Boolean], Map[Identifier, Expr])
- protected[purescala] def boundValues : Unit = {
+ protected[leon] def boundValues : Unit = {
val lowerBound: Z3AST = z3.mkInt(Settings.testBounds._1, z3.mkIntSort)
val upperBound: Z3AST = z3.mkInt(Settings.testBounds._2, z3.mkIntSort)
diff --git a/src/main/scala/purescala/Analysis.scala b/src/main/scala/leon/Analysis.scala
similarity index 98%
rename from src/main/scala/purescala/Analysis.scala
rename to src/main/scala/leon/Analysis.scala
index cd2a97b46..9849330ce 100644
--- a/src/main/scala/purescala/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -1,9 +1,9 @@
-package purescala
+package leon
-import Common._
-import Definitions._
-import Trees._
-import TypeTrees._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
import scala.collection.mutable.{Set => MutableSet}
diff --git a/src/main/scala/funcheck/Annotations.scala b/src/main/scala/leon/Annotations.scala
similarity index 86%
rename from src/main/scala/funcheck/Annotations.scala
rename to src/main/scala/leon/Annotations.scala
index c90e43247..0831c8ff8 100644
--- a/src/main/scala/funcheck/Annotations.scala
+++ b/src/main/scala/leon/Annotations.scala
@@ -1,4 +1,4 @@
-package funcheck
+package leon
object Annotations {
class induct extends StaticAnnotation
diff --git a/src/main/scala/purescala/DefaultTactic.scala b/src/main/scala/leon/DefaultTactic.scala
similarity index 99%
rename from src/main/scala/purescala/DefaultTactic.scala
rename to src/main/scala/leon/DefaultTactic.scala
index 7a212b667..6f31b9ff5 100644
--- a/src/main/scala/purescala/DefaultTactic.scala
+++ b/src/main/scala/leon/DefaultTactic.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
import purescala.Common._
import purescala.Trees._
diff --git a/src/main/scala/purescala/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
similarity index 99%
rename from src/main/scala/purescala/Evaluator.scala
rename to src/main/scala/leon/Evaluator.scala
index ebaea193e..aec3acfa1 100644
--- a/src/main/scala/purescala/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -1,8 +1,8 @@
-package purescala
+package leon
-import Common._
-import Trees._
-import TypeTrees._
+import purescala.Common._
+import purescala.Trees._
+import purescala.TypeTrees._
object Evaluator {
// Expr should be some ground term. We have call-by-value semantics.
diff --git a/src/main/scala/purescala/Extensions.scala b/src/main/scala/leon/Extensions.scala
similarity index 99%
rename from src/main/scala/purescala/Extensions.scala
rename to src/main/scala/leon/Extensions.scala
index 8bc5a4c46..5905ec998 100644
--- a/src/main/scala/purescala/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
import purescala.Trees._
import purescala.Definitions._
diff --git a/src/main/scala/purescala/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
similarity index 97%
rename from src/main/scala/purescala/FairZ3Solver.scala
rename to src/main/scala/leon/FairZ3Solver.scala
index d4208a8dd..390a72ee9 100644
--- a/src/main/scala/purescala/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -1,11 +1,11 @@
-package purescala
+package leon
import z3.scala._
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
import scala.collection.mutable.{Map => MutableMap}
import scala.collection.mutable.{Set => MutableSet}
@@ -31,8 +31,8 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
)
toggleWarningMessages(true)
- protected[purescala] var z3: Z3Context = null
- protected[purescala] var program: Program = null
+ protected[leon] var z3: Z3Context = null
+ protected[leon] var program: Program = null
private var neverInitialized = true
private var unrollingBank: UnrollingBank = null
@@ -98,9 +98,9 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
private var setSorts: Map[TypeTree, Z3Sort] = Map.empty
private var mapSorts: Map[TypeTree, Z3Sort] = Map.empty
- protected[purescala] var funSorts: Map[TypeTree, Z3Sort] = Map.empty
- protected[purescala] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
- protected[purescala] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
+ protected[leon] var funSorts: Map[TypeTree, Z3Sort] = Map.empty
+ protected[leon] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty
+ protected[leon] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty
private var intSetMinFun: Z3FuncDecl = null
private var intSetMaxFun: Z3FuncDecl = null
@@ -108,20 +108,20 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
private var adtSorts: Map[ClassTypeDef, Z3Sort] = Map.empty
private var fallbackSorts: Map[TypeTree, Z3Sort] = Map.empty
- protected[purescala] var adtTesters: Map[CaseClassDef, Z3FuncDecl] = Map.empty
- protected[purescala] var adtConstructors: Map[CaseClassDef, Z3FuncDecl] = Map.empty
- protected[purescala] var adtFieldSelectors: Map[Identifier, Z3FuncDecl] = Map.empty
+ protected[leon] var adtTesters: Map[CaseClassDef, Z3FuncDecl] = Map.empty
+ protected[leon] var adtConstructors: Map[CaseClassDef, Z3FuncDecl] = Map.empty
+ protected[leon] var adtFieldSelectors: Map[Identifier, Z3FuncDecl] = Map.empty
private var reverseADTTesters: Map[Z3FuncDecl, CaseClassDef] = Map.empty
private var reverseADTConstructors: Map[Z3FuncDecl, CaseClassDef] = Map.empty
private var reverseADTFieldSelectors: Map[Z3FuncDecl, (CaseClassDef,Identifier)] = Map.empty
- protected[purescala] val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
- protected[purescala] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[purescala] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[purescala] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[purescala] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
- protected[purescala] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty
+ protected[leon] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
+ protected[leon] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty
private def mapRangeSort(toType : TypeTree) : Z3Sort = mapRangeSorts.get(toType) match {
case Some(z3sort) => z3sort
@@ -817,9 +817,9 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
(cleanedUp, newClauses.reverse, ite2Bools)
}
- protected[purescala] var exprToZ3Id : Map[Expr,Z3AST] = Map.empty
- protected[purescala] var z3IdToExpr : Map[Z3AST,Expr] = Map.empty
- protected[purescala] def toZ3Formula(z3: Z3Context, expr: Expr, initialMap: Map[Identifier,Z3AST] = Map.empty) : Option[Z3AST] = {
+ protected[leon] var exprToZ3Id : Map[Expr,Z3AST] = Map.empty
+ protected[leon] var z3IdToExpr : Map[Z3AST,Expr] = Map.empty
+ protected[leon] def toZ3Formula(z3: Z3Context, expr: Expr, initialMap: Map[Identifier,Z3AST] = Map.empty) : Option[Z3AST] = {
class CantTranslateException extends Exception
val varsInformula: Set[Identifier] = variablesOf(expr)
@@ -1007,7 +1007,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
}
- protected[purescala] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree] = None) : Expr = {
+ protected[leon] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree] = None) : Expr = {
def rec(t: Z3AST, expType: Option[TypeTree] = None) : Expr = expType match {
case Some(MapType(kt,vt)) =>
model.getArrayValue(t) match {
diff --git a/src/main/scala/purescala/FunctionTemplate.scala b/src/main/scala/leon/FunctionTemplate.scala
similarity index 97%
rename from src/main/scala/purescala/FunctionTemplate.scala
rename to src/main/scala/leon/FunctionTemplate.scala
index e8f1e0667..6a4395f18 100644
--- a/src/main/scala/purescala/FunctionTemplate.scala
+++ b/src/main/scala/leon/FunctionTemplate.scala
@@ -1,12 +1,13 @@
-package purescala
+package leon
-import Common._
-import Trees._
-import TypeTrees._
-import Definitions._
+import purescala.Common._
+import purescala.Trees._
+import purescala.TypeTrees._
+import purescala.Definitions._
import scala.collection.mutable.{Set=>MutableSet,Map=>MutableMap}
+// TODO: maybe a candidate for moving into purescala package?
class FunctionTemplate private(
funDef : FunDef,
activatingBool : Identifier,
diff --git a/src/main/scala/purescala/InductionTactic.scala b/src/main/scala/leon/InductionTactic.scala
similarity index 99%
rename from src/main/scala/purescala/InductionTactic.scala
rename to src/main/scala/leon/InductionTactic.scala
index d93cc5957..5e14f1963 100644
--- a/src/main/scala/purescala/InductionTactic.scala
+++ b/src/main/scala/leon/InductionTactic.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
import purescala.Common._
import purescala.Trees._
diff --git a/src/main/scala/purescala/ParallelSolver.scala b/src/main/scala/leon/ParallelSolver.scala
similarity index 96%
rename from src/main/scala/purescala/ParallelSolver.scala
rename to src/main/scala/leon/ParallelSolver.scala
index 63b04c76c..1a3e1d7c4 100644
--- a/src/main/scala/purescala/ParallelSolver.scala
+++ b/src/main/scala/leon/ParallelSolver.scala
@@ -1,10 +1,10 @@
-package purescala
+package leon
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
import Evaluator._
diff --git a/src/main/scala/purescala/RandomSolver.scala b/src/main/scala/leon/RandomSolver.scala
similarity index 97%
rename from src/main/scala/purescala/RandomSolver.scala
rename to src/main/scala/leon/RandomSolver.scala
index 2b0efd49d..f15381892 100644
--- a/src/main/scala/purescala/RandomSolver.scala
+++ b/src/main/scala/leon/RandomSolver.scala
@@ -1,10 +1,10 @@
-package purescala
+package leon
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
import Evaluator._
diff --git a/src/main/scala/purescala/Reporter.scala b/src/main/scala/leon/Reporter.scala
similarity index 98%
rename from src/main/scala/purescala/Reporter.scala
rename to src/main/scala/leon/Reporter.scala
index ed41c8beb..71f22363a 100644
--- a/src/main/scala/purescala/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -1,7 +1,8 @@
-package purescala
+package leon
import purescala.Definitions.Definition
import purescala.Trees.Expr
+import purescala.PrettyPrinter
abstract class Reporter {
def error(msg: Any) : Unit
diff --git a/src/main/scala/purescala/Settings.scala b/src/main/scala/leon/Settings.scala
similarity index 98%
rename from src/main/scala/purescala/Settings.scala
rename to src/main/scala/leon/Settings.scala
index 914f9c0bd..d62dd80d2 100644
--- a/src/main/scala/purescala/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
// typically these settings can be changed through some command-line switch.
object Settings {
diff --git a/src/main/scala/purescala/Stopwatch.scala b/src/main/scala/leon/Stopwatch.scala
similarity index 98%
rename from src/main/scala/purescala/Stopwatch.scala
rename to src/main/scala/leon/Stopwatch.scala
index c56d17626..842e3fc0a 100644
--- a/src/main/scala/purescala/Stopwatch.scala
+++ b/src/main/scala/leon/Stopwatch.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
/** Implements a stopwatch for profiling purposes */
class Stopwatch(description : String, verbose : Boolean = false) {
diff --git a/src/main/scala/purescala/TestExtension.scala b/src/main/scala/leon/TestExtension.scala
similarity index 98%
rename from src/main/scala/purescala/TestExtension.scala
rename to src/main/scala/leon/TestExtension.scala
index f4244f1a9..c76f81caf 100644
--- a/src/main/scala/purescala/TestExtension.scala
+++ b/src/main/scala/leon/TestExtension.scala
@@ -1,10 +1,10 @@
-package purescala
+package leon
import purescala.Common._
import purescala.Trees._
import purescala.TypeTrees._
import purescala.Definitions._
-import purescala.Extensions._
+import Extensions._
class TestExtension(val reporter: Reporter) extends Analyser(reporter) {
val description : String = "Testing."
diff --git a/src/main/scala/purescala/TimeoutSolver.scala b/src/main/scala/leon/TimeoutSolver.scala
similarity index 83%
rename from src/main/scala/purescala/TimeoutSolver.scala
rename to src/main/scala/leon/TimeoutSolver.scala
index dcd2a95ad..1785aec5e 100644
--- a/src/main/scala/purescala/TimeoutSolver.scala
+++ b/src/main/scala/leon/TimeoutSolver.scala
@@ -1,10 +1,10 @@
-package purescala
+package leon
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
import scala.sys.error
diff --git a/src/main/scala/purescala/Timer.scala b/src/main/scala/leon/Timer.scala
similarity index 97%
rename from src/main/scala/purescala/Timer.scala
rename to src/main/scala/leon/Timer.scala
index b72b12b3e..ffc9d2c5b 100644
--- a/src/main/scala/purescala/Timer.scala
+++ b/src/main/scala/leon/Timer.scala
@@ -1,4 +1,4 @@
-package purescala
+package leon
/** Creates a thread that, when started, counts for maxsecs seconds and then
* calls the callback, unless the timer was halted first. */
diff --git a/src/main/scala/purescala/TrivialSolver.scala b/src/main/scala/leon/TrivialSolver.scala
similarity index 81%
rename from src/main/scala/purescala/TrivialSolver.scala
rename to src/main/scala/leon/TrivialSolver.scala
index 78cf3d0ef..7e08c4832 100644
--- a/src/main/scala/purescala/TrivialSolver.scala
+++ b/src/main/scala/leon/TrivialSolver.scala
@@ -1,11 +1,11 @@
-package purescala
+package leon
import z3.scala._
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
class TrivialSolver(reporter: Reporter) extends Solver(reporter) {
val description = "Solver for syntactically trivial formulas"
diff --git a/src/main/scala/funcheck/Utils.scala b/src/main/scala/leon/Utils.scala
similarity index 92%
rename from src/main/scala/funcheck/Utils.scala
rename to src/main/scala/leon/Utils.scala
index a88bc888a..6d7f019ce 100644
--- a/src/main/scala/funcheck/Utils.scala
+++ b/src/main/scala/leon/Utils.scala
@@ -1,4 +1,4 @@
-package funcheck
+package leon
object Utils {
sealed class IsValid(val property : Boolean) {
diff --git a/src/main/scala/purescala/VerificationCondition.scala b/src/main/scala/leon/VerificationCondition.scala
similarity index 94%
rename from src/main/scala/purescala/VerificationCondition.scala
rename to src/main/scala/leon/VerificationCondition.scala
index 7c6710fa2..4150536fa 100644
--- a/src/main/scala/purescala/VerificationCondition.scala
+++ b/src/main/scala/leon/VerificationCondition.scala
@@ -1,9 +1,9 @@
-package purescala
+package leon
+import purescala.Trees._
+import purescala.Definitions._
+import purescala.Common._
import Extensions._
-import Trees._
-import Definitions._
-import Common._
/** This is just to hold some history information. */
class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: VCKind.Value, val tactic: Tactic, val info: String = "") extends ScalacPositional {
diff --git a/src/main/scala/purescala/Z3ModelReconstruction.scala b/src/main/scala/leon/Z3ModelReconstruction.scala
similarity index 95%
rename from src/main/scala/purescala/Z3ModelReconstruction.scala
rename to src/main/scala/leon/Z3ModelReconstruction.scala
index 59fea83e1..913da2fa3 100644
--- a/src/main/scala/purescala/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/Z3ModelReconstruction.scala
@@ -1,11 +1,11 @@
-package purescala
+package leon
import z3.scala._
-import Common._
-import Definitions._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TypeTrees._
import Extensions._
-import Trees._
-import TypeTrees._
trait Z3ModelReconstruction {
self: AbstractZ3Solver =>
diff --git a/src/main/scala/purescala/isabelle/Main.scala b/src/main/scala/leon/isabelle/Main.scala
similarity index 99%
rename from src/main/scala/purescala/isabelle/Main.scala
rename to src/main/scala/leon/isabelle/Main.scala
index 48ce2afdb..3fd96cff3 100644
--- a/src/main/scala/purescala/isabelle/Main.scala
+++ b/src/main/scala/leon/isabelle/Main.scala
@@ -1,12 +1,14 @@
-package purescala.isabelle
-import purescala.Reporter
-import purescala.Trees._
-import purescala.Definitions._
-import purescala.Extensions._
-import purescala.Settings._
-import purescala.Common.Identifier
-import purescala.TypeTrees._
-import purescala.PrettyPrinter
+package leon.isabelle
+
+import leon.Extensions._
+import leon.Reporter
+import leon.Settings._
+
+import leon.purescala.Common.Identifier
+import leon.purescala.Definitions._
+import leon.purescala.PrettyPrinter
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
import java.lang.StringBuffer
import java.io._
diff --git a/src/main/scala/purescala/isabelle/README b/src/main/scala/leon/isabelle/README
similarity index 100%
rename from src/main/scala/purescala/isabelle/README
rename to src/main/scala/leon/isabelle/README
diff --git a/src/main/scala/purescala/isabelle/StrongConnectedComponents.scala b/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
similarity index 95%
rename from src/main/scala/purescala/isabelle/StrongConnectedComponents.scala
rename to src/main/scala/leon/isabelle/StrongConnectedComponents.scala
index d7a5991da..78eb355ff 100644
--- a/src/main/scala/purescala/isabelle/StrongConnectedComponents.scala
+++ b/src/main/scala/leon/isabelle/StrongConnectedComponents.scala
@@ -1,12 +1,14 @@
-package purescala.isabelle
-import purescala.Reporter
-import purescala.Trees._
-import purescala.Definitions._
-import purescala.Extensions._
-import purescala.Settings._
-import purescala.Common.Identifier
-import purescala.TypeTrees._
-import purescala.PrettyPrinter
+package leon.isabelle
+
+import leon.Extensions._
+import leon.Reporter
+import leon.Settings._
+
+import leon.purescala.Common.Identifier
+import leon.purescala.Definitions._
+import leon.purescala.PrettyPrinter
+import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
import java.lang.StringBuffer
import java.io._
diff --git a/src/main/scala/funcheck/AnalysisComponent.scala b/src/main/scala/leon/plugin/AnalysisComponent.scala
similarity index 89%
rename from src/main/scala/funcheck/AnalysisComponent.scala
rename to src/main/scala/leon/plugin/AnalysisComponent.scala
index 7ca519621..7756946ad 100644
--- a/src/main/scala/funcheck/AnalysisComponent.scala
+++ b/src/main/scala/leon/plugin/AnalysisComponent.scala
@@ -1,9 +1,10 @@
-package funcheck
+package leon
+package plugin
import scala.tools.nsc._
import scala.tools.nsc.plugins._
-class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
+class AnalysisComponent(val global: Global, val pluginInstance: LeonPlugin)
extends PluginComponent
with CodeExtraction
{
@@ -15,7 +16,7 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
val phaseName = pluginInstance.name
- /** this is initialized when the Funcheck phase starts*/
+ /** this is initialized when the Leon phase starts*/
var fresh: scala.tools.nsc.util.FreshNameCreator = null
protected def stopIfErrors: Unit = {
@@ -39,14 +40,14 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
sys.exit(0)
} else {
if(!pluginInstance.actionAfterExtraction.isDefined) {
- println("Extracted program for " + unit + ". Re-run with -P:funcheck:parse to see the output.")
+ println("Extracted program for " + unit + ". Re-run with -P:leon:parse to see the output.")
}
//println(prog)
}
if(!pluginInstance.actionAfterExtraction.isDefined) {
println("Starting analysis.")
- val analysis = new purescala.Analysis(prog)
+ val analysis = new Analysis(prog)
analysis.analyse
if(pluginInstance.stopAfterAnalysis) {
println("Analysis complete. Now terminating the compiler process.")
diff --git a/src/main/scala/funcheck/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
similarity index 99%
rename from src/main/scala/funcheck/CodeExtraction.scala
rename to src/main/scala/leon/plugin/CodeExtraction.scala
index af9756e60..1930fc7a0 100644
--- a/src/main/scala/funcheck/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -1,4 +1,5 @@
-package funcheck
+package leon
+package plugin
import scala.tools.nsc._
import scala.tools.nsc.plugins._
@@ -188,8 +189,8 @@ trait CodeExtraction extends Extractors {
if(mods.isPrivate) funDef.addAnnotation("private")
for(a <- dd.symbol.annotations) {
a.atp.safeToString match {
- case "funcheck.Annotations.induct" => funDef.addAnnotation("induct")
- case "funcheck.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
+ case "leon.Annotations.induct" => funDef.addAnnotation("induct")
+ case "leon.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
case _ => ;
}
}
diff --git a/src/main/scala/funcheck/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
similarity index 99%
rename from src/main/scala/funcheck/Extractors.scala
rename to src/main/scala/leon/plugin/Extractors.scala
index ff7791bae..ee684e97a 100644
--- a/src/main/scala/funcheck/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -1,11 +1,12 @@
-package funcheck
+package leon
+package plugin
import scala.tools.nsc._
/** Contains extractors to pull-out interesting parts of the Scala ASTs. */
trait Extractors {
val global: Global
- val pluginInstance: FunCheckPlugin
+ val pluginInstance: LeonPlugin
import global._
import global.definitions._
@@ -45,7 +46,7 @@ trait Extractors {
object ExHoldsExpression {
def unapply(tree: Select) : Option[Tree] = tree match {
- case Select(Apply(Select(Select(funcheckIdent, utilsName), any2IsValidName), realExpr :: Nil), holdsName) if (
+ case Select(Apply(Select(Select(leonIdent, utilsName), any2IsValidName), realExpr :: Nil), holdsName) if (
utilsName.toString == "Utils" &&
any2IsValidName.toString == "any2IsValid" &&
holdsName.toString == "holds") => Some(realExpr)
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
new file mode 100644
index 000000000..39356927d
--- /dev/null
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -0,0 +1,80 @@
+package leon
+package plugin
+
+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 LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=>Unit] = None) extends Plugin {
+ import global._
+
+ val name = "leon"
+ val description = "The Leon static analyzer"
+
+ var stopAfterAnalysis: Boolean = true
+ var stopAfterExtraction: Boolean = false
+ var silentlyTolerateNonPureBodies: Boolean = false
+
+ /** The help message displaying the options for that plugin. */
+ override val optionsHelp: Option[String] = Some(
+ " -P:leon:uniqid When pretty-printing purescala trees, show identifiers IDs" + "\n" +
+ " -P:leon:with-code Allows the compiler to keep running after the static analysis" + "\n" +
+ " -P:leon:parse Checks only whether the program is valid PureScala" + "\n" +
+ " -P:leon:extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
+ " -P:leon:nodefaults Runs only the analyses provided by the extensions" + "\n" +
+ " -P:leon:functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
+ " -P:leon:unrolling=[0,1,2] Unrolling depth for recursive functions" + "\n" +
+ " -P:leon:axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
+ " -P:leon:tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
+ " -P:leon:bapa Use BAPA Z3 extension (incompatible with many other things)" + "\n" +
+ " -P:leon:impure Generate testcases only for impure functions" + "\n" +
+ " -P:leon:testcases=[1,2] Number of testcases to generate per function" + "\n" +
+ " -P:leon:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
+ " -P:leon:timeout=N Sets a timeout of N seconds" + "\n" +
+ " -P:leon:XP Enable weird transformations and other bug-producing features" + "\n" +
+ " -P:leon:BV Use bit-vectors for integers" + "\n" +
+ " -P:leon:prune Use additional SMT queries to rule out some unrollings" + "\n" +
+ " -P:leon:cores Use UNSAT cores in the unrolling/refinement step" + "\n" +
+ " -P:leon:quickcheck Use QuickCheck-like random search" + "\n" +
+ " -P:leon:parallel Run all solvers in parallel" + "\n" +
+ " -P:leon:templates Use new ``FunctionTemplate'' technique" + "\n" +
+ " -P:leon:noLuckyTests Do not perform additional tests to potentially find models early"
+ )
+
+ /** Processes the command-line options. */
+ private def splitList(lst: String) : Seq[String] = lst.split(':').map(_.trim).filter(!_.isEmpty)
+ override def processOptions(options: List[String], error: String => Unit) {
+ for(option <- options) {
+ option match {
+ case "with-code" => stopAfterAnalysis = false
+ case "uniqid" => leon.Settings.showIDs = true
+ case "parse" => stopAfterExtraction = true
+ case "tolerant" => 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 "templates" => leon.Settings.useTemplates = true
+ case "noLuckyTests" => leon.Settings.luckyTest = false
+ 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 }
+ case _ => error("Invalid option: " + option)
+ }
+ }
+ }
+
+ val components = List[PluginComponent](new AnalysisComponent(global, this))
+ val descriptions = List[String]("leon analyses")
+}
diff --git a/src/main/scala/funcheck/Main.scala b/src/main/scala/leon/plugin/Main.scala
similarity index 80%
rename from src/main/scala/funcheck/Main.scala
rename to src/main/scala/leon/plugin/Main.scala
index 9266ccff2..027b35a70 100644
--- a/src/main/scala/funcheck/Main.scala
+++ b/src/main/scala/leon/plugin/Main.scala
@@ -1,12 +1,12 @@
-package funcheck
+package leon
+package plugin
import scala.tools.nsc.{Global,Settings,SubComponent,CompilerCommand}
import purescala.Definitions.Program
object Main {
- import purescala.{Reporter,DefaultReporter,Definitions,Analysis}
- import Definitions.Program
+ import leon.{Reporter,DefaultReporter,Analysis}
def main(args : Array[String]) : Unit = run(args)
@@ -37,9 +37,9 @@ object Main {
}
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"
+ val (leonOptions, nonLeonOptions) = args.toList.partition(_.startsWith("--"))
+ val command = new CompilerCommand(nonLeonOptions, settings) {
+ override val cmdName = "leon"
}
if(command.ok) {
@@ -47,9 +47,8 @@ object Main {
println(command.cmdName + " beta.")
} else {
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
+ runner.leonPlugin.processOptions(leonOptions.map(_.substring(2)), Console.err.println(_))
+ runner.leonPlugin.stopAfterAnalysis = false
val run = new runner.Run
run.compile(command.files)
}
@@ -60,7 +59,7 @@ object Main {
/** This class is a compiler that will be used for running the plugin in
* standalone mode. Original version courtesy of D. Zufferey. */
class PluginRunner(settings : Settings, reportingFunction : String => Unit, actionOnProgram : Option[Program=>Unit]) extends Global(settings, new SimpleReporter(settings, reportingFunction)) {
- val funcheckPlugin = new FunCheckPlugin(this, actionOnProgram)
+ val leonPlugin = new LeonPlugin(this, actionOnProgram)
protected def myAddToPhasesSet(sub : SubComponent, descr : String) : Unit = {
phasesSet += sub
@@ -77,7 +76,7 @@ class PluginRunner(settings : Settings, reportingFunction : String => Unit, acti
pickler -> "serialize symbol tables",
refchecks -> "reference and override checking, translate nested objects"
) ::: {
- val zipped = funcheckPlugin.components zip funcheckPlugin.descriptions
+ val zipped = leonPlugin.components zip leonPlugin.descriptions
zipped
}
phs foreach (myAddToPhasesSet _).tupled
diff --git a/src/main/scala/funcheck/SimpleReporter.scala b/src/main/scala/leon/plugin/SimpleReporter.scala
similarity index 98%
rename from src/main/scala/funcheck/SimpleReporter.scala
rename to src/main/scala/leon/plugin/SimpleReporter.scala
index cd20fd8c5..0d8e4b0ad 100644
--- a/src/main/scala/funcheck/SimpleReporter.scala
+++ b/src/main/scala/leon/plugin/SimpleReporter.scala
@@ -1,4 +1,5 @@
-package funcheck
+package leon
+package plugin
import scala.tools.nsc.Settings
import scala.tools.nsc.reporters.AbstractReporter
diff --git a/src/main/scala/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
similarity index 98%
rename from src/main/scala/purescala/Common.scala
rename to src/main/scala/leon/purescala/Common.scala
index f3e95df30..6132bd607 100644
--- a/src/main/scala/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -1,3 +1,4 @@
+package leon
package purescala
object Common {
@@ -18,7 +19,7 @@ object Common {
override def hashCode: Int = id
override def toString: String = {
- if(purescala.Settings.showIDs) {
+ if(Settings.showIDs) {
// angle brackets: name + "\u3008" + id + "\u3009"
name + "[" + id + "]"
} else if(alwaysShowUniqueID) {
diff --git a/src/main/scala/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
similarity index 99%
rename from src/main/scala/purescala/Definitions.scala
rename to src/main/scala/leon/purescala/Definitions.scala
index 5aa535395..efd8b52fb 100644
--- a/src/main/scala/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -1,3 +1,4 @@
+package leon
package purescala
object Definitions {
diff --git a/src/main/scala/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
similarity index 99%
rename from src/main/scala/purescala/PrettyPrinter.scala
rename to src/main/scala/leon/purescala/PrettyPrinter.scala
index 16d811e91..c5d2d7158 100644
--- a/src/main/scala/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -1,6 +1,6 @@
+package leon
package purescala
-
/** This pretty-printer uses Unicode for some operators, to make sure we
* distinguish PureScala from "real" Scala (and also because it's cute). */
object PrettyPrinter {
diff --git a/src/main/scala/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
similarity index 99%
rename from src/main/scala/purescala/Trees.scala
rename to src/main/scala/leon/purescala/Trees.scala
index 338b5d24a..7a289934a 100644
--- a/src/main/scala/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -1,3 +1,4 @@
+package leon
package purescala
/** AST definitions for Pure Scala. */
diff --git a/src/main/scala/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
similarity index 99%
rename from src/main/scala/purescala/TypeTrees.scala
rename to src/main/scala/leon/purescala/TypeTrees.scala
index eab21e5cb..e948a433f 100644
--- a/src/main/scala/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -1,3 +1,4 @@
+package leon
package purescala
object TypeTrees {
diff --git a/src/main/scala/purescala/z3plugins/bapa/AST.scala b/src/main/scala/leon/z3plugins/bapa/AST.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/AST.scala
rename to src/main/scala/leon/z3plugins/bapa/AST.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/BAPATheory.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheory.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/BAPATheory.scala
rename to src/main/scala/leon/z3plugins/bapa/BAPATheory.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/BAPATheoryBubbles.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/BAPATheoryBubbles.scala
rename to src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/BAPATheoryEqc.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/BAPATheoryEqc.scala
rename to src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/Bubbles.scala b/src/main/scala/leon/z3plugins/bapa/Bubbles.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/Bubbles.scala
rename to src/main/scala/leon/z3plugins/bapa/Bubbles.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/NormalForms.scala b/src/main/scala/leon/z3plugins/bapa/NormalForms.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/NormalForms.scala
rename to src/main/scala/leon/z3plugins/bapa/NormalForms.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/PrettyPrinter.scala b/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/PrettyPrinter.scala
rename to src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
diff --git a/src/main/scala/purescala/z3plugins/bapa/VennRegions.scala b/src/main/scala/leon/z3plugins/bapa/VennRegions.scala
similarity index 100%
rename from src/main/scala/purescala/z3plugins/bapa/VennRegions.scala
rename to src/main/scala/leon/z3plugins/bapa/VennRegions.scala
diff --git a/testcases/sas2011-testcases/ListOperations.scala b/testcases/sas2011-testcases/ListOperations.scala
index 3a08ac8f9..a4fc4f8dc 100644
--- a/testcases/sas2011-testcases/ListOperations.scala
+++ b/testcases/sas2011-testcases/ListOperations.scala
@@ -1,6 +1,6 @@
import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
object ListOperations {
sealed abstract class List
--
GitLab