diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 204d9a821041fadba1f575fb3e6c73032dbb08d1..78f887914eb8224b053be19c2481905e32100b25 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -30,6 +30,14 @@ case class LeonValueOption(name: String, value: String) extends LeonOption {
None
}
+ def asLong(ctx : LeonContext) : Option[Long] = try {
+ Some(value.toLong)
+ } catch {
+ case _ : Throwable =>
+ ctx.reporter.error("Option --%s takes a long as value.".format(name))
+ None
+ }
+
override def toString() : String = "--%s=%s".format(name, value)
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index e05adbf6c181c96ad69d4096cd866115b0edb6f8..30e4152c660b1975f5a8f25253514f0454d636c4 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -22,7 +22,7 @@ object Main {
synthesis.SynthesisPhase,
termination.TerminationPhase,
verification.AnalysisPhase,
- refactor.RefactorPhase
+ repair.RepairPhase
)
}
@@ -33,7 +33,7 @@ object Main {
lazy val topLevelOptions : Set[LeonOptionDef] = Set(
LeonFlagOptionDef ("termination", "--termination", "Check program termination"),
- LeonFlagOptionDef ("refactor", "--refactor", "Refactoring/Repair"),
+ LeonFlagOptionDef ("repair", "--repair", "Repair selected functions"),
LeonFlagOptionDef ("synthesis", "--synthesis", "Partial synthesis of choose() constructs"),
LeonFlagOptionDef ("xlang", "--xlang", "Support for extra program constructs (imperative,...)"),
LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum,smt)"),
@@ -142,8 +142,8 @@ object Main {
for(opt <- leonOptions) opt match {
case LeonFlagOption("termination", value) =>
settings = settings.copy(termination = value)
- case LeonFlagOption("refactor", value) =>
- settings = settings.copy(refactor = value)
+ case LeonFlagOption("repair", value) =>
+ settings = settings.copy(repair = value)
case LeonFlagOption("synthesis", value) =>
settings = settings.copy(synthesis = value)
case LeonFlagOption("xlang", value) =>
@@ -209,7 +209,7 @@ object Main {
import termination.TerminationPhase
import xlang.XlangAnalysisPhase
import verification.AnalysisPhase
- import refactor.RefactorPhase
+ import repair.RepairPhase
val pipeBegin : Pipeline[List[String],Program] =
ExtractionPhase andThen
@@ -218,8 +218,8 @@ object Main {
val pipeProcess: Pipeline[Program, Any] = {
if (settings.synthesis) {
SynthesisPhase
- } else if (settings.refactor) {
- RefactorPhase
+ } else if (settings.repair) {
+ RepairPhase
} else if (settings.termination) {
TerminationPhase
} else if (settings.xlang) {
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 31cf87ca4ecb8b93ee4a0da74377f27c8360ed3b..ef9cdf7b032f242f49c2b214412c54ef9a4af72f 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -8,7 +8,7 @@ case class Settings(
val strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
val debugSections: Set[DebugSection] = Set(), // Enables debug message for the following sections
val termination: Boolean = false,
- val refactor: Boolean = false,
+ val repair: Boolean = false,
val synthesis: Boolean = false,
val xlang: Boolean = false,
val verify: Boolean = true,
diff --git a/src/main/scala/leon/refactor/RefactorPhase.scala b/src/main/scala/leon/refactor/RefactorPhase.scala
deleted file mode 100644
index 77e12c2d41f94a5a2bf63c263e3f98cb3694b0bc..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/refactor/RefactorPhase.scala
+++ /dev/null
@@ -1,50 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon
-package refactor
-
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.Constructors._
-import purescala.DefOps._
-
-object RefactorPhase extends LeonPhase[Program, Program] {
- val name = "Refactor"
- val description = "Refactoring/Repairing"
-
- implicit val debugSection = utils.DebugSectionRefactor
-
- override val definedOptions : Set[LeonOptionDef] = Set(
- LeonValueOptionDef("functions", "--functions=f1:f2", "Refactor functions f1,f2,...")
- )
-
- def run(ctx: LeonContext)(program: Program): Program = {
- var refactorFuns: Option[Seq[String]] = None
-
- val reporter = ctx.reporter
-
- for(opt <- ctx.options) opt match {
- case LeonValueOption("functions", ListValue(fs)) =>
- refactorFuns = Some(fs)
- case _ =>
- }
-
-
- val fdFilter = {
- import OptionsHelpers._
-
- filterInclusive(refactorFuns.map(fdMatcher), None)
- }
-
- val toRefactor = funDefsFromMain(program).toList.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos).filter(fdFilter)
-
- for (fd <- toRefactor) {
- new Repairman(ctx, program, fd).repair()
- }
-
- program
- }
-}
diff --git a/src/main/scala/leon/refactor/RepairCostModel.scala b/src/main/scala/leon/repair/RepairCostModel.scala
similarity index 98%
rename from src/main/scala/leon/refactor/RepairCostModel.scala
rename to src/main/scala/leon/repair/RepairCostModel.scala
index 4cb56277ac14b6e7fd1e0d4c37f3232523c385ad..c658b93e1701e3818c932733d3f6b63e25a6e676 100644
--- a/src/main/scala/leon/refactor/RepairCostModel.scala
+++ b/src/main/scala/leon/repair/RepairCostModel.scala
@@ -1,7 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
package leon
-package refactor
+package repair
import synthesis._
import purescala.Definitions._
diff --git a/src/main/scala/leon/repair/RepairPhase.scala b/src/main/scala/leon/repair/RepairPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bdaecde66987bfec2bcdc7d7a8e48009f20dd8c9
--- /dev/null
+++ b/src/main/scala/leon/repair/RepairPhase.scala
@@ -0,0 +1,53 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package repair
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Constructors._
+import purescala.DefOps._
+
+object RepairPhase extends LeonPhase[Program, Program] {
+ val name = "Repair"
+ val description = "Repairing"
+
+ implicit val debugSection = utils.DebugSectionRepair
+
+ override val definedOptions : Set[LeonOptionDef] = Set(
+ LeonValueOptionDef("functions", "--functions=f1:f2", "Repair functions f1,f2,...")
+ )
+
+ def run(ctx: LeonContext)(program: Program): Program = {
+ var repairFuns: Option[Seq[String]] = None
+ var verifTimeout: Option[Long] = None
+
+ val reporter = ctx.reporter
+
+ for(opt <- ctx.options) opt match {
+ case v @ LeonValueOption("timeout", _) =>
+ verifTimeout = v.asLong(ctx)
+ case LeonValueOption("functions", ListValue(fs)) =>
+ repairFuns = Some(fs)
+ case _ =>
+ }
+
+
+ val fdFilter = {
+ import OptionsHelpers._
+
+ filterInclusive(repairFuns.map(fdMatcher), None)
+ }
+
+ val toRepair = funDefsFromMain(program).toList.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos).filter(fdFilter)
+
+ for (fd <- toRepair) {
+ new Repairman(ctx, program, fd, verifTimeout).repair()
+ }
+
+ program
+ }
+}
diff --git a/src/main/scala/leon/refactor/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
similarity index 60%
rename from src/main/scala/leon/refactor/Repairman.scala
rename to src/main/scala/leon/repair/Repairman.scala
index 7e7e6d18e49b1810dd3163ba7c093056187ea8f6..1a86297742074b824ee336e595661758dc0ce741 100644
--- a/src/main/scala/leon/refactor/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -1,7 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
package leon
-package refactor
+package repair
import purescala.Common._
import purescala.Definitions._
@@ -23,16 +23,12 @@ import synthesis.rules._
import synthesis.heuristics._
import graph.DotGenerator
-class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
+class Repairman(ctx: LeonContext, program: Program, fd: FunDef, verifTimeout: Option[Long]) {
val reporter = ctx.reporter
- implicit val debugSection = DebugSectionRefactor
+ implicit val debugSection = DebugSectionRepair
- var testBank = List[Example]()
-
- var solutions: List[(Solution, Expr, List[FunDef])] = Nil
-
- def getSynthesizer(): Synthesizer = {
+ def getSynthesizer(tests: List[Example]): Synthesizer = {
// Gather in/out tests
val pre = fd.precondition.getOrElse(BooleanLiteral(true))
val args = fd.params.map(_.id)
@@ -41,9 +37,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
// Compute tests
val out = fd.postcondition.map(_._1).getOrElse(FreshIdentifier("res", true).setType(fd.returnType))
- val inouts = testBank;
-
- val testsCases = inouts.collect {
+ val testsCases = tests.collect {
case InOutExample(ins, outs) =>
val (patt, optGuard) = expressionToPattern(tupleWrap(ins))
MatchCase(patt, optGuard match {
@@ -58,31 +52,24 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
BooleanLiteral(true)
}
- // Compute guide implementation
- val gexpr = fd.body.get
- val gfd = program.library.guide.get.typed(Seq(gexpr.getType))
- val guide = FunctionInvocation(gfd, Seq(gexpr))
+ // Create a fresh function
+ val nid = FreshIdentifier(fd.id.name+"_repair").copiedFrom(fd.id)
+ val nfd = new FunDef(nid, fd.tparams, fd.returnType, fd.params, fd.defType)
+ nfd.copyContentFrom(fd)
+ nfd.copiedFrom(fd)
- // Compute initial call
- val termfd = program.library.terminating.get
- val withinCall = FunctionInvocation(fd.typedWithDef, fd.params.map(_.id.toVariable))
- val terminating = FunctionInvocation(termfd.typed(Seq(fd.returnType)), Seq(withinCall))
+ nfd.body = nfd.body.map { b => preMap({
+ case fi @ FunctionInvocation(TypedFunDef(`fd`, tps), args) =>
+ Some(FunctionInvocation(TypedFunDef(nfd, tps), args).copiedFrom(fi))
+ case _ => None
+ })(b)}
val spec = and(
- fd.postcondition.map(_._2).getOrElse(BooleanLiteral(true)),
+ nfd.postcondition.map(_._2).getOrElse(BooleanLiteral(true)),
passes
)
- val ws = and(
- guide,
- terminating
- )
-
- // Synthesis from the ground up
- val p = Problem(fd.params.map(_.id).toList, ws, pre, spec, List(out))
- val ch = Choose(List(out), spec)
- // do we really want to do that?
- fd.body = Some(ch)
+ val p = focusRepair(tests, nfd, spec, out)
val soptions0 = SynthesisPhase.processOptions(ctx);
@@ -95,72 +82,45 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
)) diff Seq(ADTInduction)
);
- new Synthesizer(ctx, fd, program, p, soptions)
+ new Synthesizer(ctx, nfd, program, p, soptions)
}
- def repair(): Unit = {
- val synth = getSynthesizer()
- val p = synth.problem
-
-
- synth.synthesize() match {
- case (search, sols) =>
- for (sol <- sols) {
- val expr = sol.toSimplifiedExpr(ctx, program)
+ private def guideOf(expr: Expr): Expr = {
+ val gfd = program.library.guide.get.typed(Seq(expr.getType))
+ FunctionInvocation(gfd, Seq(expr))
+ }
- val (npr, fds) = synth.solutionToProgram(sol)
+ private def focusRepair(tests: List[Example], fd: FunDef, post: Expr, out: Identifier): Problem = {
+ reporter.ifDebug { printer =>
+ printer("Tests failing are: ")
+ tests.collect {
+ case InExample(ins) =>
+ printer(ins.mkString(", "))
+ }
+ }
- if (!sol.isTrusted) {
- getVerificationCounterExamples(fds.head, npr, synth.options.timeoutMs) match {
- case Some(ces) =>
- testBank ++= ces
- reporter.info("Failed :(, but I learned: "+ces.mkString(" | "))
- case None =>
- solutions ::= (sol, expr, fds)
- reporter.info(ASCIIHelpers.title("ZUCCESS!"))
- }
- } else {
- solutions ::= (sol, expr, fds)
- reporter.info(ASCIIHelpers.title("ZUCCESS!"))
- }
- }
+ // Compute initial call for terminating argument
+ val termfd = program.library.terminating.get
+ val withinCall = FunctionInvocation(fd.typedWithDef, fd.params.map(_.id.toVariable))
+ val terminating = FunctionInvocation(termfd.typed(Seq(fd.returnType)), Seq(withinCall))
- if (synth.options.generateDerivationTrees) {
- val dot = new DotGenerator(search.g)
- dot.writeFile("derivation"+DotGenerator.nextId()+".dot")
- }
+ val pre = fd.precondition.getOrElse(BooleanLiteral(true))
- if (solutions.isEmpty) {
- reporter.info(ASCIIHelpers.title("FAILURZ!"))
- } else {
- reporter.info(ASCIIHelpers.title("Solutions"))
- for (((sol, expr, fds), i) <- solutions.zipWithIndex) {
- reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+":"))
- reporter.info(ScalaPrinter(expr));
- }
+ val body = fd.body.get
- if (solutions.size > 1) {
- reporter.info(ASCIIHelpers.title("Disambiguating..."))
- disambiguate(p, solutions(0)._1, solutions(1)._1) match {
- case Some((o1, o2)) =>
- reporter.info("Solutions differ on "+o1.ins.mkString(", "))
- reporter.info("solution A produces: "+o1.outs.mkString(", "))
- reporter.info("solution B produces: "+o2.outs.mkString(", "))
-
- case None =>
- reporter.info("Solutions appear equivalent..")
- }
- }
- }
+ val ws = and(
+ guideOf(body),
+ terminating
+ )
- case _ =>
- reporter.error("I failed you :(")
- }
+ // Synthesis from the ground up
+ val p = Problem(fd.params.map(_.id).toList, ws, pre, post, List(out))
+ p
}
- def getVerificationCounterExamples(fd: FunDef, prog: Program, optTimeout: Option[Long]): Option[Seq[InExample]] = {
- val timeoutMs = optTimeout getOrElse 3000l
+ def getVerificationCounterExamples(fd: FunDef, prog: Program): Option[Seq[InExample]] = {
+ val timeoutMs = verifTimeout.getOrElse(3000L)
val solverf = SolverFactory(() => (new FairZ3Solver(ctx, prog) with TimeoutSolver).setTimeout(timeoutMs))
val vctx = VerificationContext(ctx, prog, solverf, reporter)
val vcs = AnalysisPhase.generateVerificationConditions(vctx, Some(List(fd.id.name)))
@@ -189,7 +149,93 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
}
}
- def disambiguate(p: Problem, sol1: Solution, sol2: Solution): Option[(InOutExample, InOutExample)] = {
+
+ def discoverTests: List[Example] = {
+ val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams(checkContracts = true))
+ val generator= new NaiveDataGen(ctx, program, evaluator)
+
+ val pre = fd.precondition.getOrElse(BooleanLiteral(true))
+
+ val inputs = generator.generateFor(fd.params.map(_.id), pre, 30, 10000).toList
+
+ var tests = List[Example]()
+
+ tests ++= inputs.map { i =>
+ evaluator.eval(FunctionInvocation(fd.typed(fd.tparams.map(_.tp)), i)) match {
+ case EvaluationResults.Successful(res) =>
+ new InOutExample(i, List(res))
+
+ case _ =>
+ new InExample(i)
+ }
+ }
+
+ // Try to verify, if it fails, we have at least one CE
+ getVerificationCounterExamples(fd, program) match {
+ case Some(ces) =>
+ tests ++= ces
+ case _ =>
+ }
+
+ tests
+ }
+
+ def repair() = {
+ reporter.info(ASCIIHelpers.title("1. Discovering tests for "+fd.id))
+ val tests = discoverTests
+
+ reporter.info(ASCIIHelpers.title("2. Creating synthesis Problem"))
+ val synth = getSynthesizer(tests)
+ val p = synth.problem
+
+ var solutions = List[Solution]()
+
+ reporter.info(ASCIIHelpers.title("3. Synthesizing"))
+ reporter.info(p)
+
+ synth.synthesize() match {
+ case (search, sols) =>
+ for (sol <- sols) {
+
+ // Validate solution if not trusted
+ if (!sol.isTrusted) {
+ reporter.info("Found untrusted solution! Verifying...")
+ val (npr, fds) = synth.solutionToProgram(sol)
+
+ getVerificationCounterExamples(fds.head, npr) match {
+ case Some(ces) =>
+ reporter.error("I ended up finding this counter example:\n"+ces.mkString(" | "))
+
+ case None =>
+ solutions ::= sol
+ reporter.info("Solution was not trusted but verification passed!")
+ }
+ } else {
+ reporter.info("Found trusted solution!")
+ solutions ::= sol
+ }
+ }
+
+ if (synth.options.generateDerivationTrees) {
+ val dot = new DotGenerator(search.g)
+ dot.writeFile("derivation"+DotGenerator.nextId()+".dot")
+ }
+
+ if (solutions.isEmpty) {
+ reporter.error(ASCIIHelpers.title("Failed to repair!"))
+ } else {
+ reporter.info(ASCIIHelpers.title("Repair successful:"))
+ for ((sol, i) <- solutions.zipWithIndex) {
+ reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+":"))
+ val expr = sol.toSimplifiedExpr(ctx, program)
+ reporter.info(ScalaPrinter(expr));
+ }
+ }
+ }
+ }
+
+ // ununsed for now, but implementation could be useful later
+ private def disambiguate(p: Problem, sol1: Solution, sol2: Solution): Option[(InOutExample, InOutExample)] = {
val s1 = sol1.toSimplifiedExpr(ctx, program)
val s2 = sol2.toSimplifiedExpr(ctx, program)
@@ -229,44 +275,4 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
}
}
}
-
- def classifier(ok: Seq[Example], notok: Seq[Example]): Option[Expr] = {
- // Obtain expr that returns partitions all examples into ok/notok
-
- None
- }
-
- def discoverTests() = {
- val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams(checkContracts = true))
- val tests = new NaiveDataGen(ctx, program, evaluator)
-
- val pre = fd.precondition.getOrElse(BooleanLiteral(true))
-
- val inputs = tests.generateFor(fd.params.map(_.id), pre, 30, 10000).toList
-
- testBank ++= inputs.map { i =>
- evaluator.eval(FunctionInvocation(fd.typed(fd.tparams.map(_.tp)), i)) match {
- case EvaluationResults.Successful(res) =>
- new InOutExample(i, List(res))
-
- case _ =>
- new InExample(i)
- }
- }
-
- // Try to verify, if it fails, we have at least one CE
- val timeout = ctx.options.flatMap { //FIXME ugly-
- case LeonValueOption("timeout", l) =>
- try {Some(l.toLong * 1000L)} catch { case _: NumberFormatException => None }
- case _ => None
- }.headOption
- getVerificationCounterExamples(fd, program, timeout) match {
- case Some(ces) =>
- testBank ++= ces
- case _ =>
- }
- }
-
- discoverTests()
-
}
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index 0e4d30a4e538e431cb8dc4315defd8c9f459e11e..011e5b3084c4626a627f858ffe351b19fd929279 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -18,7 +18,7 @@ case object DebugSectionTrees extends DebugSection("trees", 1 << 6
case object DebugSectionPositions extends DebugSection("positions", 1 << 7)
case object DebugSectionDataGen extends DebugSection("datagen", 1 << 8)
case object DebugSectionEvaluation extends DebugSection("eval", 1 << 9)
-case object DebugSectionRefactor extends DebugSection("refactor", 1 << 10)
+case object DebugSectionRepair extends DebugSection("repair", 1 << 10)
object DebugSections {
val all = Set[DebugSection](
@@ -32,6 +32,6 @@ object DebugSections {
DebugSectionPositions,
DebugSectionDataGen,
DebugSectionEvaluation,
- DebugSectionRefactor
+ DebugSectionRepair
)
}