From 5b95c6ed4db935a984408aad65e649eb088dbb93 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 19 Aug 2015 15:26:57 +0200
Subject: [PATCH] Use full names to match against --functions. Display
qualified names.
---
doc/options.rst | 6 ++++++
src/main/scala/leon/LeonOption.scala | 10 ++++++----
src/main/scala/leon/evaluators/EvaluationPhase.scala | 2 +-
src/main/scala/leon/purescala/DefOps.scala | 4 ++++
src/main/scala/leon/purescala/Definitions.scala | 4 +++-
src/main/scala/leon/repair/RepairPhase.scala | 2 +-
src/main/scala/leon/synthesis/SynthesisPhase.scala | 2 +-
src/main/scala/leon/termination/TerminationPhase.scala | 2 +-
src/main/scala/leon/verification/AnalysisPhase.scala | 6 +++---
.../scala/leon/verification/VerificationReport.scala | 6 +++---
src/main/scala/leon/xlang/FixReportLabels.scala | 2 +-
11 files changed, 30 insertions(+), 16 deletions(-)
diff --git a/doc/options.rst b/doc/options.rst
index 09f31a1e2..d1e7f3f3f 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -88,6 +88,12 @@ These options are available by all Leon components:
Only consider functions f1, f2, ... . This applies to all functionalities
where Leon manipulates the input in a per-function basis.
+ Leon will match against suffixes of qualified names. For instance:
+ ``--functions=List.size`` will match the method
+ ``leon.collection.List.size`` while ``--functions=size`` will match all ``size``
+ methods and functions. This option supports ``_`` as wildcard: ``--functions=List._`` will
+ match all ``List`` methods.
+
* ``--solvers=s1,s2,...``
Use solvers s1, s2,... . If more than one solver is chosen, all chosen
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 497e729eb..46deafab5 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -4,6 +4,9 @@ package leon
import OptionParsers._
+import purescala.Definitions.Program
+import purescala.DefOps.fullName
+
abstract class LeonOptionDef[+A] {
val name: String
val description: String
@@ -109,8 +112,7 @@ object OptionsHelpers {
val regexPatterns = patterns map { s =>
import java.util.regex.Pattern
- val p0 = scala.reflect.NameTransformer.encode(s)
- val p = p0.replaceAll("\\$","\\\\\\$").replaceAll("\\.", "\\\\.").replaceAll("_", ".+")
+ val p = "(.+\\.)?"+s.replaceAll("\\.", "\\\\.").replaceAll("_", ".+")
Pattern.compile(p)
}
@@ -119,8 +121,8 @@ object OptionsHelpers {
import purescala.Definitions.FunDef
- def fdMatcher(patterns: Traversable[String]): FunDef => Boolean = {
- { (fd: FunDef) => fd.id.name } andThen matcher(patterns)
+ def fdMatcher(pgm: Program)(patterns: Traversable[String]): FunDef => Boolean = {
+ { (fd: FunDef) => fullName(fd)(pgm) } andThen matcher(patterns)
}
def filterInclusive[T](included: Option[T => Boolean], excluded: Option[T => Boolean]): T => Boolean = {
diff --git a/src/main/scala/leon/evaluators/EvaluationPhase.scala b/src/main/scala/leon/evaluators/EvaluationPhase.scala
index 59f82c209..280a68b70 100644
--- a/src/main/scala/leon/evaluators/EvaluationPhase.scala
+++ b/src/main/scala/leon/evaluators/EvaluationPhase.scala
@@ -24,7 +24,7 @@ object EvaluationPhase extends LeonPhase[Program, Unit] {
val fdFilter = {
import OptionsHelpers._
- filterInclusive(evalFuns.map(fdMatcher), None)
+ filterInclusive(evalFuns.map(fdMatcher(program)), None)
}
val toEvaluate = funDefsFromMain(program).toList.filter(_.params.size == 0).filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 0e6150ac1..b8afe6377 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -155,6 +155,10 @@ object DefOps {
pathToString(pathFromRoot(df), useUniqueIds)
}
+ def qualifiedName(fd: FunDef, useUniqueIds: Boolean = false)(implicit pgm: Program): String = {
+ pathToString(pathFromRoot(fd).takeRight(2), useUniqueIds)
+ }
+
private def nameToParts(name: String) = {
name.split("\\.").toList map scala.reflect.NameTransformer.encode
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index fde6f3de7..94c59a85b 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -420,7 +420,9 @@ object Definitions {
def typed = {
TypedFunDef(this, tparams.map(_.tp))
}
-
+
+ def qualifiedName(implicit pgm: Program) = DefOps.qualifiedName(this, false)
+
}
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
index 0f2ed5a9c..342d41ddd 100644
--- a/src/main/scala/leon/repair/RepairPhase.scala
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -21,7 +21,7 @@ object RepairPhase extends UnitPhase[Program]() {
val fdFilter = {
import OptionsHelpers._
- filterInclusive(repairFuns.map(fdMatcher), None)
+ filterInclusive(repairFuns.map(fdMatcher(program)), None)
}
val toRepair = funDefsFromMain(program).toList.filter(fdFilter).filter{ _.hasPostcondition }.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 22ddfa480..2b770e0c5 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -71,7 +71,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
import OptionsHelpers._
val ciTofd = { (ci: ChooseInfo) => ci.fd }
- filterInclusive(options.functions.map(fdMatcher), Some(excludeByDefault _)) compose ciTofd
+ filterInclusive(options.functions.map(fdMatcher(program)), Some(excludeByDefault _)) compose ciTofd
}
val chooses = ChooseInfo.extractFromProgram(ctx, program).filter(fdFilter)
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index a2bd46d90..b13c109ad 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -21,7 +21,7 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
val fdFilter = {
import OptionsHelpers._
- filterInclusive(ctx.findOption(SharedOptions.optFunctions).map(fdMatcher), Some(excludeByDefault _))
+ filterInclusive(ctx.findOption(SharedOptions.optFunctions).map(fdMatcher(program)), Some(excludeByDefault _))
}
val toVerify = tc.program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index e8b3b39f3..c0cc41087 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -41,14 +41,14 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val fdFilter = {
import OptionsHelpers._
- filterInclusive(filterFuns.map(fdMatcher), Some(excludeByDefault _))
+ filterInclusive(filterFuns.map(fdMatcher(program)), Some(excludeByDefault _))
}
val toVerify = program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
for(funDef <- toVerify) {
if (excludeByDefault(funDef)) {
- reporter.warning("Forcing verification of " + funDef.id.name + " which was assumed verified")
+ reporter.warning("Forcing verification of " + funDef.qualifiedName(program) + " which was assumed verified")
}
}
@@ -114,7 +114,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}
}
- VerificationReport(initMap ++ results)
+ VerificationReport(vctx.program, initMap ++ results)
}
def checkVC(vctx: VerificationContext, vc: VC): VCResult = {
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index dd15dda2a..43f6aacb8 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -6,9 +6,9 @@ package verification
import VCKinds._
import VCStatus._
-import purescala.Definitions.FunDef
+import purescala.Definitions.{FunDef, Program}
-case class VerificationReport(val results: Map[VC, Option[VCResult]]) {
+case class VerificationReport(val program: Program, val results: Map[VC, Option[VCResult]]) {
val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {
case (vc, or) => (vc, or.getOrElse(VCResult.unknown))
@@ -30,7 +30,7 @@ case class VerificationReport(val results: Map[VC, Option[VCResult]]) {
t ++= vrs.map { case (vc, vr) =>
val timeStr = vr.timeMs.map(t => f"${t/1000d}%-3.3f").getOrElse("")
Row(Seq(
- Cell(vc.fd.id.toString),
+ Cell(vc.fd.qualifiedName(program)),
Cell(vc.kind.name),
Cell(vc.getPos),
Cell(vr.status),
diff --git a/src/main/scala/leon/xlang/FixReportLabels.scala b/src/main/scala/leon/xlang/FixReportLabels.scala
index 9f18a2646..91eabf9c3 100644
--- a/src/main/scala/leon/xlang/FixReportLabels.scala
+++ b/src/main/scala/leon/xlang/FixReportLabels.scala
@@ -44,7 +44,7 @@ object FixReportLabels extends LeonPhase[VerificationReport, VerificationReport]
}
- VerificationReport(newResults)
+ VerificationReport(vr.program, newResults)
}
--
GitLab