diff --git a/.gitignore b/.gitignore
index 4ef5b5eae48b78d3f7dd97318ed2794a9123564f..cff31570a7dc553b9ffdcd88a0b7ae4afeb0a200 100644
--- a/.gitignore
+++ b/.gitignore
@@ -55,3 +55,12 @@ out-classes
# Isabelle
contrib
/bin/
+/cvc4.exe
+/libz3.dll
+/libz3.lib
+/msvcp100.dll
+/msvcr100.dll
+/scalaz3.dll
+/scalaz3.lib
+/vcomp100.dll
+/z3.exe
diff --git a/library/annotation/package.scala b/library/annotation/package.scala
index 00ae0743c3977c65376ba1d66a9fb476c24b5397..7cf1c7040a98aa2ef8673d41f912c0d4fb2cb38d 100644
--- a/library/annotation/package.scala
+++ b/library/annotation/package.scala
@@ -19,4 +19,6 @@ package object annotation {
class monotonic extends StaticAnnotation
@ignore
class compose extends StaticAnnotation
+ @ignore
+ class internal extends StaticAnnotation
}
\ No newline at end of file
diff --git a/library/collection/package.scala b/library/collection/package.scala
index e163eaf4a70c525be71644ec0e05afeb4f63d87a..8a5ae170763909c20153f373915d6a4e9e726ca0 100644
--- a/library/collection/package.scala
+++ b/library/collection/package.scala
@@ -9,7 +9,7 @@ import leon.lang.synthesis.choose
package object collection {
- @library
+ @internal @library
def setToList[A](set: Set[A]): List[A] = choose {
(x: List[A]) => x.content == set
}
diff --git a/library/lang/StrOps.scala b/library/lang/StrOps.scala
index 3c59590d073de60b109c8d8dc3d48b330749a72c..723ce5be82d7a841c743640ba4f10284076c0dfe 100644
--- a/library/lang/StrOps.scala
+++ b/library/lang/StrOps.scala
@@ -18,6 +18,6 @@ object StrOps {
def substring(a: String, start: BigInt, end: BigInt): String = {
if(start > end || start >= length(a) || end <= 0) "" else a.substring(start.toInt, end.toInt)
}
- @ignore
- def escape(a: String): String = a // Wrong definition, but it will eventually use StringEscapeUtils.escapeJava(s) at parsing and compile time.
+ @internal @library
+ def escape(s: String): String = s // Wrong definition, but it will eventually use StringEscapeUtils.escapeJava(s) at parsing and compile time.
}
\ No newline at end of file
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index f1fced4905e524d9185602756a8971479faca9aa..6d70782ad69c95da4181fd45267b3917a6a0cd04 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -987,7 +987,11 @@ trait CodeGeneration {
mkUnbox(tpe, ch)
case _ =>
}
-
+
+ case FunctionInvocation(TypedFunDef(fd, Nil), Seq(a)) if fd == program.library.escape.get =>
+ mkExpr(a, ch)
+ ch << InvokeStatic(StrOpsClass, "escape", s"(L$JavaStringClass;)L$JavaStringClass;")
+
case FunctionInvocation(TypedFunDef(fd, Seq(tp)), Seq(set)) if fd == program.library.setToList.get =>
val nil = CaseClass(CaseClassType(program.library.Nil.get, Seq(tp)), Seq())
@@ -1199,10 +1203,6 @@ trait CodeGeneration {
mkExpr(end, ch)
ch << InvokeStatic(StrOpsClass, "substring", s"(L$JavaStringClass;L$BigIntClass;L$BigIntClass;)L$JavaStringClass;")
- case StringEscape(a) =>
- mkExpr(a, ch)
- ch << InvokeStatic(StrOpsClass, "escape", s"(L$JavaStringClass;)L$JavaStringClass;")
-
// Arithmetic
case Plus(l, r) =>
mkExpr(l, ch)
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index ceb23eb38c62649e2cb1a1d8f1bbcea10f109100..cf58bf06658c880a4ce84b1a805cc8788f89d1a1 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -14,8 +14,9 @@ import purescala.Common._
import purescala.Expressions._
import purescala.Definitions._
import leon.solvers.{HenkinModel, Model, SolverFactory}
-
import scala.collection.mutable.{Map => MutableMap}
+import leon.purescala.DefOps
+import org.apache.commons.lang3.StringEscapeUtils
abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int)
extends ContextualEvaluator(ctx, prog, maxSteps)
@@ -105,6 +106,13 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
def mkCons(h: Expr, t: Expr) = CaseClass(CaseClassType(cons, Seq(tp)), Seq(h,t))
els.foldRight(nil)(mkCons)
+ case FunctionInvocation(TypedFunDef(fd, Nil), Seq(input)) if fd == program.library.escape.get =>
+ e(input) match {
+ case StringLiteral(s) =>
+ StringLiteral(StringEscapeUtils.escapeJava(s))
+ case _ => throw EvalError(typeErrorMsg(input, StringType))
+ }
+
case FunctionInvocation(tfd, args) =>
if (gctx.stepsLeft < 0) {
throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
@@ -268,11 +276,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case FractionalLiteral(n, d) => StringLiteral(n.toString + "/" + d.toString)
case res => throw EvalError(typeErrorMsg(res, RealType))
}
- case StringEscape(a) => e(a) match {
- case StringLiteral(i) => StringLiteral(codegen.runtime.StrOps.escape(i))
- case res => throw EvalError(typeErrorMsg(res, StringType))
- }
-
+
case BVPlus(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 + i2)
@@ -643,6 +647,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case other =>
context.reporter.error(other.getPos, "Error: don't know how to handle " + other.asString + " in Evaluator ("+other.getClass+").")
+ println("RecursiveEvaluator error:" + other.asString)
throw EvalError("Unhandled case in Evaluator : " + other.asString)
}
diff --git a/src/main/scala/leon/evaluators/StringTracingEvaluator.scala b/src/main/scala/leon/evaluators/StringTracingEvaluator.scala
index 22d4cd8c186235f391c418e0c2b8fe2b649dc302..62cde913fae123ab0fcd8c3d019953af9efb5942 100644
--- a/src/main/scala/leon/evaluators/StringTracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/StringTracingEvaluator.scala
@@ -6,14 +6,24 @@ package evaluators
import purescala.Extractors.Operator
import purescala.Expressions._
import purescala.Types._
-import purescala.Definitions.Program
+import purescala.Definitions.{TypedFunDef, Program}
+import purescala.DefOps
import purescala.Expressions.Expr
import leon.utils.DebugSectionSynthesis
+import org.apache.commons.lang3.StringEscapeUtils
class StringTracingEvaluator(ctx: LeonContext, prog: Program) extends ContextualEvaluator(ctx, prog, 50000) with HasDefaultGlobalContext with HasDefaultRecContext {
val underlying = new DefaultEvaluator(ctx, prog) {
override protected[evaluators] def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
+
+ case FunctionInvocation(TypedFunDef(fd, Nil), Seq(input)) if fd == prog.library.escape.get =>
+ e(input) match {
+ case StringLiteral(s) =>
+ StringLiteral(StringEscapeUtils.escapeJava(s))
+ case _ => throw EvalError(typeErrorMsg(input, StringType))
+ }
+
case FunctionInvocation(tfd, args) =>
if (gctx.stepsLeft < 0) {
throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
@@ -56,12 +66,6 @@ class StringTracingEvaluator(ctx: LeonContext, prog: Program) extends Contextual
case _ =>
StringConcat(es1, es2)
}
- case StringEscape(a) =>
- val ea = e(a)
- ea match {
- case StringLiteral(_) => super.e(StringEscape(a))
- case _ => StringEscape(ea)
- }
case expr =>
super.e(expr)
}
@@ -99,13 +103,6 @@ class StringTracingEvaluator(ctx: LeonContext, prog: Program) extends Contextual
case _ =>
(StringLength(es1), StringLength(t1))
}
-
- case StringEscape(a) =>
- val (ea, ta) = e(a)
- ea match {
- case StringLiteral(_) => (underlying.e(StringEscape(ea)), StringEscape(ta))
- case _ => (StringEscape(ea), StringEscape(ta))
- }
case expr@StringLiteral(s) =>
(expr, expr)
@@ -119,7 +116,7 @@ class StringTracingEvaluator(ctx: LeonContext, prog: Program) extends Contextual
case BooleanLiteral(false) => e(elze)
case _ => throw EvalError(typeErrorMsg(first, BooleanType))
}
-
+
case Operator(es, builder) =>
val (ees, ts) = es.map(e).unzip
(underlying.e(builder(ees)), builder(ts))
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 1016406b2b79e8f116208796e3e0a66cb0b4ec4d..67e5c4502ad1810b323616916e3edfab9c05a8ea 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -200,14 +200,6 @@ trait ASTExtractors {
case _ => None
}
}
-
- /** Matches a call to StrOps.escape */
- object ExStringEscape {
- def unapply(tree: Apply): Option[Tree] = tree match {
- case Apply(ExSelected("leon", "lang", "StrOps", "escape"), List(arg)) => Some(arg)
- case _ => None
- }
- }
/** Extracts the 'require' contract from an expression (only if it's the
* first call in the block). */
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 7a575d8da21e1435b68197da1d14c3bbd1b8f534..54494713006989f356b8174088a79402c5b1e4b0 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1508,9 +1508,6 @@ trait CodeExtraction extends ASTExtractors {
case ExImplies(lhs, rhs) =>
Implies(extractTree(lhs), extractTree(rhs)).setPos(current.pos)
-
- case ExStringEscape(s) =>
- StringEscape(extractTree(s))
case c @ ExCall(rec, sym, tps, args) =>
// The object on which it is called is null if the symbol sym is a valid function in the scope and not a method.
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index a99c1df18b880ea6e7d0f379041deade3172902a..ffb4fa90c3bb15c682f7886f3d3bbf9ee79c508b 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -25,13 +25,16 @@ object ExtractionPhase extends SimpleLeonPhase[List[String], Program] {
val settings = new Settings
+ def getFiles(path: String): Option[Array[String]] =
+ scala.util.Try(new File(path).listFiles().map{ _.getAbsolutePath }).toOption
+
val scalaLib = Option(scala.Predef.getClass.getProtectionDomain.getCodeSource).map{
_.getLocation.getPath
}.orElse( for {
// We are in Eclipse. Look in Eclipse plugins to find scala lib
eclipseHome <- Option(System.getenv("ECLIPSE_HOME"))
pluginsHome = eclipseHome + "/plugins"
- plugins <- scala.util.Try(new File(pluginsHome).listFiles().map{ _.getAbsolutePath }).toOption
+ plugins <- getFiles(pluginsHome)
path <- plugins.find{ _ contains "scala-library"}
} yield path).getOrElse( ctx.reporter.fatalError(
"No Scala library found. If you are working in Eclipse, " +
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index aa216b852507ef66780aa47885c84c87e8e79f7e..ae93221bfe8313cf8cef20ed084d559a2a472133 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -588,13 +588,6 @@ object Expressions {
else Untyped
}
}
- /** $encodingof `StrOps.escape(expr)` for strings */
- case class StringEscape(expr: Expr) extends Expr {
- val getType = {
- if (expr.getType == StringType) StringType
- else Untyped
- }
- }
/* Integer arithmetic */
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 7e8277a4fab21f835eafc85e94d567bc3b7050bc..e2581dd8cdb33e3d025e8206d72dd32fc4ca59f7 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -39,8 +39,6 @@ object Extractors {
Some((Seq(t), (es: Seq[Expr]) => CharToString(es.head)))
case RealToString(t) =>
Some((Seq(t), (es: Seq[Expr]) => RealToString(es.head)))
- case StringEscape(t) =>
- Some((Seq(t), (es: Seq[Expr]) => StringEscape(es.head)))
case SetCardinality(t) =>
Some((Seq(t), (es: Seq[Expr]) => SetCardinality(es.head)))
case CaseClassSelector(cd, e, sel) =>
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 554e70f4343beb38d4ed2773a292cb31476ffe0d..82f41e8764782d78b8fdfef7df5434eaaa96cfd7 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -175,7 +175,6 @@ class PrettyPrinter(opts: PrinterOptions,
case IntegerToString(expr) => p"$expr.toString"
case CharToString(expr) => p"$expr.toString"
case RealToString(expr) => p"$expr.toString"
- case StringEscape(expr) => p"leon.lang.StrOps.escape($expr)"
case StringConcat(lhs, rhs) => optP { p"$lhs + $rhs" }
case SubString(expr, start, end) => p"leon.lang.StrOps.substring($expr, $start, $end)"
diff --git a/src/main/scala/leon/programsets/DirectProgramSet.scala b/src/main/scala/leon/synthesis/programsets/DirectProgramSet.scala
similarity index 91%
rename from src/main/scala/leon/programsets/DirectProgramSet.scala
rename to src/main/scala/leon/synthesis/programsets/DirectProgramSet.scala
index 1a08a98dd68a678c8167945f7f0fa66a56152362..2887c57fcb80b26e40bf07324b8dc8a0bfc5b5eb 100644
--- a/src/main/scala/leon/programsets/DirectProgramSet.scala
+++ b/src/main/scala/leon/synthesis/programsets/DirectProgramSet.scala
@@ -1,4 +1,4 @@
-package leon.programsets
+package leon.synthesis.programsets
import leon.purescala
import purescala.Expressions._
diff --git a/src/main/scala/leon/programsets/JoinProgramSet.scala b/src/main/scala/leon/synthesis/programsets/JoinProgramSet.scala
similarity index 97%
rename from src/main/scala/leon/programsets/JoinProgramSet.scala
rename to src/main/scala/leon/synthesis/programsets/JoinProgramSet.scala
index e12442c9eced94b9d0ff862ef1fbe71333e83973..c0147227a9cacfa0d52b0d94728f1585d3e0cef7 100644
--- a/src/main/scala/leon/programsets/JoinProgramSet.scala
+++ b/src/main/scala/leon/synthesis/programsets/JoinProgramSet.scala
@@ -1,5 +1,5 @@
package leon
-package programsets
+package synthesis.programsets
import leon.purescala
import purescala.Expressions._
diff --git a/src/main/scala/leon/programsets/ProgramSet.scala b/src/main/scala/leon/synthesis/programsets/ProgramSet.scala
similarity index 86%
rename from src/main/scala/leon/programsets/ProgramSet.scala
rename to src/main/scala/leon/synthesis/programsets/ProgramSet.scala
index 04025f01660ef1ae4f2bd603083675d4e684ed9f..ebfcf8fa19de9036c1b6d7e4d2c862038cde8756 100644
--- a/src/main/scala/leon/programsets/ProgramSet.scala
+++ b/src/main/scala/leon/synthesis/programsets/ProgramSet.scala
@@ -1,4 +1,4 @@
-package leon.programsets
+package leon.synthesis.programsets
import leon.purescala
import purescala.Expressions._
diff --git a/src/main/scala/leon/programsets/UnionProgramset.scala b/src/main/scala/leon/synthesis/programsets/UnionProgramset.scala
similarity index 93%
rename from src/main/scala/leon/programsets/UnionProgramset.scala
rename to src/main/scala/leon/synthesis/programsets/UnionProgramset.scala
index 2e089b6bb4d3435fedb556cb13a8785f6ff4c80c..f57c53053fc661c6b0d644d720724fdd7a227bdc 100644
--- a/src/main/scala/leon/programsets/UnionProgramset.scala
+++ b/src/main/scala/leon/synthesis/programsets/UnionProgramset.scala
@@ -1,5 +1,5 @@
package leon
-package programsets
+package synthesis.programsets
import leon.purescala
import purescala.Expressions._
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 81b43f2ec5df8b278bdb4d7e25d20a9298ece61e..f03c54b560e81428851c83b86b9430d4e706e20f 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -10,8 +10,8 @@ import scala.collection.mutable.ListBuffer
import bonsai.enumerators.MemoizedEnumerator
import leon.evaluators.DefaultEvaluator
import leon.evaluators.StringTracingEvaluator
-import leon.programsets.DirectProgramSet
-import leon.programsets.JoinProgramSet
+import leon.synthesis.programsets.DirectProgramSet
+import leon.synthesis.programsets.JoinProgramSet
import leon.purescala.Common.FreshIdentifier
import leon.purescala.Common.Identifier
import leon.purescala.DefOps
@@ -182,7 +182,7 @@ case object StringRender extends Rule("StringRender") {
val tagged_solutions =
for{(funDefs, template) <- wholeTemplates.programs} yield computeSolutions(funDefs, template).map((funDefs, template, _))
- solutionStreamToRuleApplication(p, leon.utils.StreamUtils.interleave(tagged_solutions))
+ solutionStreamToRuleApplication(p, leon.utils.StreamUtils.interleave(tagged_solutions))(hctx.program)
}
/** Find ambiguities not containing _edit_me_ to ask to the user */
@@ -196,7 +196,7 @@ case object StringRender extends Rule("StringRender") {
}
/** Converts the stream of solutions to a RuleApplication */
- def solutionStreamToRuleApplication(p: Problem, solutions: Stream[(Seq[(FunDef, WithIds[Expr])], WithIds[Expr], Assignment)]): RuleApplication = {
+ def solutionStreamToRuleApplication(p: Problem, solutions: Stream[(Seq[(FunDef, WithIds[Expr])], WithIds[Expr], Assignment)])(implicit program: Program): RuleApplication = {
if(solutions.isEmpty) RuleFailed() else {
RuleClosed(
for((funDefsBodies, (singleTemplate, ids), assignment) <- solutions) yield {
@@ -215,11 +215,11 @@ case object StringRender extends Rule("StringRender") {
}
/** Crystallizes a solution so that it will not me modified if the body of fds is modified. */
- def makeFunctionsUnique(term: Expr, fds: Set[FunDef]): (Expr, Set[FunDef]) = {
+ def makeFunctionsUnique(term: Expr, fds: Set[FunDef])(implicit program: Program): (Expr, Set[FunDef]) = {
var transformMap = Map[FunDef, FunDef]()
def mapExpr(body: Expr): Expr = {
ExprOps.preMap((e: Expr) => e match {
- case FunctionInvocation(nfd, args) => Some(FunctionInvocation(getMapping(nfd.fd).typed, args))
+ case FunctionInvocation(TypedFunDef(fd, _), args) if fd != program.library.escape.get => Some(FunctionInvocation(getMapping(fd).typed, args))
case e => None
})(body)
}
@@ -376,10 +376,14 @@ case object StringRender extends Rule("StringRender") {
case None => // No function can render the current type.
input.getType match {
case StringType =>
- gatherInputs(ctx, q, result += Stream((input, Nil)) #::: Stream((StringEscape(input): Expr, Nil)))
+ gatherInputs(ctx, q, result +=
+ (Stream((input, Nil),
+ (FunctionInvocation(
+ hctx.program.library.escape.get.typed,
+ Seq(input)): Expr, Nil))))
case BooleanType =>
val (bTemplate, vs) = booleanTemplate(input).instantiateWithVars
- gatherInputs(ctx, q, result += Stream((BooleanToString(input), Nil)) #::: Stream((bTemplate, vs)))
+ gatherInputs(ctx, q, result += Stream((BooleanToString(input), Nil), (bTemplate, vs)))
case WithStringconverter(converter) => // Base case
gatherInputs(ctx, q, result += Stream((converter(input), Nil)))
case t: ClassType =>
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index b2c382fd80d2a2a63157e1fb41cb804bbab870cf..4d100210911734504a96bd005d0299ae0f1b8906 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -22,6 +22,8 @@ case class Library(pgm: Program) {
lazy val Dummy = lookup("leon.lang.Dummy").collectFirst { case ccd : CaseClassDef => ccd }
lazy val setToList = lookup("leon.collection.setToList").collectFirst { case fd : FunDef => fd }
+
+ lazy val escape = lookup("leon.lang.StrOps.escape").collectFirst { case fd : FunDef => fd }
def lookup(name: String): Seq[Definition] = {
pgm.lookupAll(name)