diff --git a/library/lang/package.scala b/library/lang/package.scala
index 7e40b880e7f89c923a60061774619e5f2d9b4b85..1b26c5006dea499e6d94632be47a20c14c723160 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -26,7 +26,7 @@ package object lang {
implicit def while2Invariant(u: Unit) = InvariantFunction
@ignore
- def error[T](reason: String): T = sys.error(reason)
+ def error[T](reason: java.lang.String): T = sys.error(reason)
@library
def passes[A, B](in: A, out: B)(tests: Map[A,B]): Boolean = {
diff --git a/library/lang/string/String.scala b/library/lang/string/String.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b47fcded3fb24bf362298dba9e4b701f868d79a7
--- /dev/null
+++ b/library/lang/string/String.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+package leon.lang.string
+
+case class String(chars: leon.collection.List[Char]) {
+ def +(that: String): String = {
+ String(this.chars ++ that.chars)
+ }
+
+ def size = chars.size
+
+ def length = size
+}
diff --git a/library/lang/string/package.scala b/library/lang/string/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..01080050cc39baa678b638ba7f0b844cfa88f12a
--- /dev/null
+++ b/library/lang/string/package.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+import scala.language.implicitConversions
+
+package object string {
+ @ignore
+ implicit def strToStr(s: java.lang.String): leon.lang.string.String = {
+ String(leon.collection.Nil())
+ }
+}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index b41389fc2040b4d3785098830d4328c0d7d6d5d2..0ffd0fc708b25016bc8cab85c93d498560b7445b 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -152,6 +152,16 @@ trait ASTExtractors {
}
}
+
+ object ExStringLiteral {
+ def unapply(tree: Apply): Option[String] = tree match {
+ case Apply(ExSelected("leon", "lang", "string", "package", "strToStr"), (str: Literal) :: Nil) =>
+ Some(str.value.stringValue)
+ case _ =>
+ None
+ }
+ }
+
object ExAssertExpression {
/** Extracts the 'assert' contract from an expression (only if it's the
* first call in the block). */
@@ -532,6 +542,13 @@ trait ASTExtractors {
}
}
+ object ExCharLiteral {
+ def unapply(tree: Literal): Option[Char] = tree match {
+ case Literal(c @ Constant(i)) if c.tpe == CharClass.tpe => Some(c.charValue)
+ case _ => None
+ }
+ }
+
object ExInt32Literal {
def unapply(tree: Literal): Option[Int] = tree match {
case Literal(c @ Constant(i)) if c.tpe == IntClass.tpe => Some(c.intValue)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 3c8caa5cc7cbc3cc0f54b2e6a24e215a0769db4a..3f96d94887186aa5a1afdb995ecce21e49a8d5f0 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -367,9 +367,17 @@ trait CodeExtraction extends ASTExtractors {
}
}
- def libraryMethod(classname: String, methodName: String): Option[(LeonClassDef, FunDef)] = {
- classesToClasses.values.find(_.id.name == classname).flatMap { cl =>
- cl.methods.find(_.id.name == methodName).map { fd => (cl, fd) }
+ def libraryClass(pos: Position, className: String): LeonClassDef = {
+ classesToClasses.find{ case (s, c) => s.fullName == className }.map(_._2).getOrElse {
+ outOfSubsetError(pos, "Could not find class "+className)
+ }
+ }
+
+ def libraryCaseClass(pos: Position, className: String): CaseClassDef = {
+ libraryClass(pos, className) match {
+ case ccd: CaseClassDef => ccd
+ case _ =>
+ outOfSubsetError(pos, "Class "+className+" is not a case class")
}
}
@@ -1366,6 +1374,21 @@ trait CodeExtraction extends ASTExtractors {
ArrayUpdated(rar, rk, rv)
+ case chr @ ExCharLiteral(c) =>
+ CharLiteral(c)
+
+ case str @ ExStringLiteral(s) =>
+ val chars = s.toList.map(CharLiteral(_))
+
+ val consChar = CaseClassType(libraryCaseClass(str.pos, "leon.collection.Cons"), Seq(CharType));
+ val nilChar = CaseClassType(libraryCaseClass(str.pos, "leon.collection.Nil"), Seq(CharType));
+
+ val charList = chars.foldRight(CaseClass(nilChar, Seq())) {
+ case (c, s) => CaseClass(consChar, Seq(c, s))
+ }
+
+ CaseClass(CaseClassType(libraryCaseClass(str.pos, "leon.lang.string.String"), Seq()), Seq(charList))
+
case c @ ExCall(rec, sym, tps, args) =>
val rrec = rec match {
case t if (defsToDefs contains sym) && !isMethod(sym) =>
@@ -1536,6 +1559,9 @@ trait CodeExtraction extends ASTExtractors {
}
private def extractType(tpt: Type)(implicit dctx: DefContext, pos: Position): LeonType = tpt match {
+ case tpe if tpe == CharClass.tpe =>
+ CharType
+
case tpe if tpe == IntClass.tpe =>
Int32Type
@@ -1636,7 +1662,7 @@ trait CodeExtraction extends ASTExtractors {
tp
})
} else {
- outOfSubsetError(NoPosition, "Unknown class "+sym.name)
+ outOfSubsetError(NoPosition, "Unknown class "+sym.fullName)
}
}
}
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index b647188e922f592ab0606387ac316fadcb311465..7ab53108831841b671e46a7b12c19ef80f748fa2 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -40,7 +40,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
val injected = if (ctx.settings.injectLibrary) {
libFiles
} else {
- libFiles.filter(f => f.contains("/lang/") || f.contains("/annotation/"))
+ libFiles.filter(f => (f.contains("/lang/") && !f.contains("/lang/string/")) || f.contains("/annotation/"))
}
val compilerOpts = injected ::: args.filterNot(_.startsWith("--"))
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index dd1a6de02e35913f3a2ab11365c49eef3f2597c1..e9501ab8aaa400396c78f9b318837ec25a371c38 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -65,6 +65,8 @@ object Common {
case Some(ow) => ow.id :: ow.id.ownerChain
}
+ def fullName: String = ownerChain.map(_.name).mkString(".")
+
}
private object UniqueCounter {
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 50710f7a123168eb64c642f2202be4c8b42f0720..a8c8dcc59e119dc38423a5529e229b23c13d8238 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -107,6 +107,17 @@ object DefOps {
(pack, finalPath)
}
+ def fullName(df: Definition, fromProgram: Option[Program] = None): String = {
+ val p = fromProgram.getOrElse(inProgram(df))
+
+ val (pr, ds) = pathAsVisibleFrom(p, df)
+
+ (pr ::: ds.flatMap{
+ case _: UnitDef => None
+ case m: ModuleDef if m.isStandalone => None
+ case d => Some(d.id.name)
+ }).mkString(".")
+ }
def searchByFullName (
fullName : String,
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 779aad137c1b18d7d13451b6cd2da3fc1d50275b..86c6cf16fd46cad2b0fe8a4bd52c1398c119c785 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -4,6 +4,7 @@ package leon
package purescala
import scala.collection.generic.CanBuildFrom
+import utils.Library
object Definitions {
import Common._
@@ -82,6 +83,8 @@ object Definitions {
def duplicate = {
copy(units = units.map{_.duplicate})
}
+
+ lazy val library = Library(this)
def writeScalaFile(filename: String) {
import java.io.FileWriter
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 123ab89feda3b57cbeae5988bb2d8130747e3838..a00e2d2450f34e45a6dbc63806eb991144764daa 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -13,6 +13,7 @@ import utils._
import java.lang.StringBuffer
import PrinterHelpers._
+import TreeOps.isStringLiteral
case class PrinterContext(
current: Tree,
@@ -228,14 +229,24 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
} else {
p"""|?($es)"""
}
+ case e @ CaseClass(cct, args) =>
- case CaseClass(cct, args) =>
- if (cct.classDef.isCaseObject) {
- p"$cct"
- } else {
- p"$cct($args)"
+ isStringLiteral(e) match {
+ case Some(str) =>
+ val q = '"';
+ p"$q$str$q"
+
+ case None =>
+ if (cct.classDef.isCaseObject) {
+ p"$cct"
+ } else {
+ p"$cct($args)"
+ }
}
+
+
+
case And(exprs) => optP { p"${nary(exprs, " && ")}" }
case Or(exprs) => optP { p"${nary(exprs, "| || ")}" }
case Not(Equals(l, r)) => optP { p"$l \u2260 $r" }
@@ -244,6 +255,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case UMinus(expr) => p"-$expr"
case Equals(l,r) => optP { p"$l == $r" }
case IntLiteral(v) => p"$v"
+ case CharLiteral(v) => p"$v"
case BooleanLiteral(v) => p"$v"
case StringLiteral(s) => p""""$s""""
case UnitLiteral() => p"()"
@@ -268,8 +280,23 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
if (tfd.fd.isRealFunction) p"($args)"
+ case BinaryMethodCall(a, op, b) =>
+ optP { p"${a} $op ${b}" }
+
+ case FcallMethodInvocation(rec, fd, id, tps, args) =>
+
+ p"${rec}.${id}"
+ if (tps.nonEmpty) {
+ p"[$tps]"
+ }
+
+ if (fd.isRealFunction) {
+ p"($args)"
+ }
+
+
case FunctionInvocation(tfd, args) =>
- printWithPath(tfd.fd)
+ p"${tfd.id}"
if (tfd.tps.nonEmpty) {
p"[${tfd.tps}]"
@@ -380,6 +407,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case Untyped => p"<untyped>"
case UnitType => p"Unit"
case Int32Type => p"Int"
+ case CharType => p"Char"
case BooleanType => p"Boolean"
case ArrayType(bt) => p"Array[$bt]"
case SetType(bt) => p"Set[$bt]"
@@ -526,6 +554,49 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
}
+ object FcallMethodInvocation {
+ def unapply(fi: FunctionInvocation): Option[(Expr, FunDef, String, Seq[TypeTree], Seq[Expr])] = {
+ val FunctionInvocation(tfd, args) = fi
+ tfd.fd.origOwner match {
+ case Some(cd: ClassDef) =>
+ val (rec, rargs) = (args.head, args.tail)
+
+ val fid = tfd.fd.id
+
+ val maybeClassName = fid.name.substring(0, cd.id.name.length)
+
+ val fname = if (maybeClassName == cd.id.name) {
+ fid.name.substring(cd.id.name.length + 1) // +1 to also remove $
+ } else {
+ fid.name
+ }
+
+ val decoded = scala.reflect.NameTransformer.decode(fname)
+
+ val realtps = tfd.tps.drop(cd.tparams.size)
+
+ Some((rec, tfd.fd, decoded, realtps, rargs))
+ case _ =>
+ None
+ }
+ }
+ }
+
+ object BinaryMethodCall {
+ val makeBinary = Set("+", "-", "*", "::", "++", "--", "&&", "||", "/");
+
+ def unapply(fi: FunctionInvocation): Option[(Expr, String, Expr)] = fi match {
+ case FcallMethodInvocation(rec, _, name, Nil, List(a)) =>
+
+ if (makeBinary contains name) {
+ Some((rec, name, a))
+ } else {
+ None
+ }
+ case _ => None
+ }
+ }
+
def requiresBraces(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
case (pa: PrettyPrintable, _) => pa.printRequiresBraces(within)
case (_, None) => false
@@ -541,12 +612,12 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
def precedence(ex: Expr): Int = ex match {
case (pa: PrettyPrintable) => pa.printPrecedence
case (_: ElementOfSet) => 0
- case (_: Or) => 1
- case (_: And) => 3
+ case (_: Or | BinaryMethodCall(_, "||", _)) => 1
+ case (_: And | BinaryMethodCall(_, "&&", _)) => 3
case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan) => 4
case (_: Equals | _: Iff | _: Not) => 5
- case (_: Plus | _: Minus | _: SetUnion| _: SetDifference) => 6
- case (_: Times | _: Division | _: Modulo) => 7
+ case (_: Plus | _: Minus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 6
+ case (_: Times | _: Division | _: Modulo | BinaryMethodCall(_, "*" | "/", _)) => 7
case _ => 7
}
@@ -558,6 +629,8 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case (_, Some(_: Require)) => false
case (_, Some(_: Definition)) => false
case (_, Some(_: MatchExpr | _: MatchCase | _: Let | _: LetTuple | _: LetDef | _: IfExpr)) => false
+ case (b1 @ BinaryMethodCall(_, _, _), Some(b2 @ BinaryMethodCall(_, _, _))) if precedence(b1) > precedence(b2) => false
+ case (BinaryMethodCall(_, _, _), Some(_: FunctionInvocation)) => true
case (_, Some(_: FunctionInvocation)) => false
case (ie: IfExpr, _) => true
case (me: MatchExpr, _ ) => true
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index eece54ca86528b26062fbfd6d42f0a2c2e7a5e2d..7b70def5ddc490c87234e79c73e2edb2627ea512 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -8,6 +8,7 @@ import utils.Simplifiers
import leon.solvers._
import scala.collection.concurrent.TrieMap
+import DefOps._
object TreeOps {
import Common._
@@ -1988,6 +1989,51 @@ object TreeOps {
(fds.values.toSet, res2)
}
+ def isStringLiteral(e: Expr): Option[String] = e match {
+ case CaseClass(cct, args) =>
+ val lib = inProgram(cct.classDef).library
+
+ if (Some(cct.classDef) == lib.String) {
+ listLiteralToList(args(0)) match {
+ case Some(chars) =>
+ val str = chars.map {
+ case CharLiteral(c) => Some(c)
+ case _ => None
+ }
+
+ if (str.forall(_.isDefined)) {
+ Some(str.flatten.mkString)
+ } else {
+ None
+ }
+ case _ =>
+ None
+
+ }
+ } else {
+ None
+ }
+ case _ =>
+ None
+ }
+
+ def listLiteralToList(e: Expr): Option[List[Expr]] = e match {
+ case CaseClass(cct, args) =>
+ val lib = inProgram(cct.classDef).library
+
+ if (Some(cct.classDef) == lib.Nil) {
+ Some(Nil)
+ } else if (Some(cct.classDef) == lib.Cons) {
+ listLiteralToList(args(1)).map { t =>
+ args(0) :: t
+ }
+ } else {
+ None
+ }
+ case _ =>
+ None
+ }
+
/**
* Deprecated API
* ========
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 44b98012a2ef65bf0b5dd570daab9750d4de265f..c5a648cccc458721a464caa2e3a5fba7c5ca16dc 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -434,6 +434,10 @@ object Trees {
val fixedType = tp
}
+ case class CharLiteral(value: Char) extends Literal[Char] with FixedType {
+ val fixedType = CharType
+ }
+
case class IntLiteral(value: Int) extends Literal[Int] with FixedType {
val fixedType = Int32Type
}
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index eb6908420247e0fb0c09efbb862711293423982d..24249ad2aa3e75ae46595bda5efdad8ef86ee616 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -55,6 +55,7 @@ object TypeTrees {
case object BooleanType extends TypeTree
case object Int32Type extends TypeTree
case object UnitType extends TypeTree
+ case object CharType extends TypeTree
case class TypeParameter(id: Identifier) extends TypeTree
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 303276bdfb71ea9927c90858410fa6365c7c72d7..c31506240b3233c981a9fabe570a7d83140993c2 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -90,6 +90,7 @@ trait SMTLIBTarget {
tpe match {
case BooleanType => Core.BoolSort()
case Int32Type => Ints.IntSort()
+ case CharType => FixedSizeBitVectors.BitVectorSort(32)
case RawArrayType(from, to) =>
Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(from), declareSort(to)))
@@ -322,6 +323,7 @@ trait SMTLIBTarget {
declareVariable(FreshIdentifier("Unit").setType(UnitType))
case IntLiteral(i) => if (i > 0) Ints.NumeralLit(i) else Ints.Neg(Ints.NumeralLit(-i))
+ case CharLiteral(c) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt).get)
case BooleanLiteral(v) => Core.BoolConst(v)
case StringLiteral(s) => SString(s)
case Let(b,d,e) =>
@@ -473,6 +475,9 @@ trait SMTLIBTarget {
case (_, UnitType) =>
UnitLiteral()
+ case (SHexadecimal(h), CharType) =>
+ CharLiteral(h.toInt.toChar)
+
case (SNumeral(n), Int32Type) =>
IntLiteral(n.toInt)
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala
index faaa084e57a6f62f1efa68d45a84e12784eccb0a..a556097db125dcf73ca67ca3e1efbd2790d6ed09 100644
--- a/src/main/scala/leon/synthesis/rules/Tegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Tegis.scala
@@ -30,7 +30,6 @@ case object TEGIS extends Rule("TEGIS") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
var tests = p.getTests(sctx).map(_.ins).distinct
-
if (tests.nonEmpty) {
List(new RuleInstantiation(p, this, SolutionBuilder.none, this.name, this.priority) {
def apply(sctx: SynthesisContext): RuleApplicationResult = {
@@ -148,7 +147,6 @@ case object TEGIS extends Rule("TEGIS") {
var candidate: Option[Expr] = None
var enumLimit = 10000;
-
var n = 1;
timers.generating.start()
allExprs.take(enumLimit).takeWhile(e => candidate.isEmpty).foreach { e =>
@@ -188,8 +186,8 @@ case object TEGIS extends Rule("TEGIS") {
}
timers.generating.stop()
- println("Found candidate "+n)
- println("Compiled: "+evaluator.unit.compiledN)
+ //println("Found candidate "+n)
+ //println("Compiled: "+evaluator.unit.compiledN)
if (candidate.isDefined) {
RuleSuccess(Solution(BooleanLiteral(true), Set(), candidate.get), isTrusted = false)
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d80fd76a0a1188423d01763f4392c6e376db9b7a
--- /dev/null
+++ b/src/main/scala/leon/utils/Library.scala
@@ -0,0 +1,19 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package utils
+
+import purescala.Definitions._
+import purescala.DefOps.searchByFullName
+
+case class Library(pgm: Program) {
+ lazy val List = lookup("leon.collection.List")
+ lazy val Cons = lookup("leon.collection.Cons")
+ lazy val Nil = lookup("leon.collection.Nil")
+
+ lazy val String = lookup("leon.lang.string.String")
+
+ def lookup(name: String): Option[Definition] = {
+ searchByFullName(name, pgm)
+ }
+}