diff --git a/library/lang/string/package.scala b/library/lang/string/package.scala index e3cd3d7aebda60a240fd47feba7c4e2552b26d64..d931debe7c587f966aadd30b2860b1793c6ad431 100644 --- a/library/lang/string/package.scala +++ b/library/lang/string/package.scala @@ -9,10 +9,10 @@ import scala.language.implicitConversions import scala.collection.immutable.{List => ScalaList} package object string { - @ignore + /*@ignore implicit def strToStr(s: java.lang.String): leon.lang.string.String = { String(listToList(s.toList)) - } + }*/ @ignore def listToList[A](s: ScalaList[A]): List[A] = s match { diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala index db477ec494742b0dc2b0e42e098676c4ab55282d..855efa3360898deb67380c6ea5f3038de6e2dbad 100644 --- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala +++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala @@ -50,6 +50,7 @@ trait ASTExtractors { protected lazy val someClassSym = classFromName("scala.Some") protected lazy val byNameSym = classFromName("scala.<byname>") protected lazy val bigIntSym = classFromName("scala.math.BigInt") + protected lazy val stringSym = classFromName("java.lang.String") protected def functionTraitSym(i:Int) = { require(1 <= i && i <= 22) classFromName("scala.Function" + i) @@ -62,6 +63,8 @@ trait ASTExtractors { def isBigIntSym(sym : Symbol) : Boolean = getResolvedTypeSym(sym) == bigIntSym + def isStringSym(sym : Symbol) : Boolean = getResolvedTypeSym(sym) match { case `stringSym` => true case _ => false } + def isByNameSym(sym : Symbol) : Boolean = getResolvedTypeSym(sym) == byNameSym // Resolve type aliases @@ -110,29 +113,36 @@ trait ASTExtractors { } def hasBigIntType(t : Tree) = isBigIntSym(t.tpe.typeSymbol) + + def hasStringType(t : Tree) = isStringSym(t.tpe.typeSymbol) def hasRealType(t : Tree) = isRealSym(t.tpe.typeSymbol) - + /** A set of helpers for extracting trees.*/ object ExtractorHelpers { + /** Extracts the identifier as `"Ident(name)"` (who needs this?!) */ object ExIdNamed { def unapply(id: Ident): Option[String] = Some(id.toString) } + /** Extracts the tree and its type (who needs this?!) */ object ExHasType { def unapply(tr: Tree): Option[(Tree, Symbol)] = Some((tr, tr.tpe.typeSymbol)) } + /** Extracts the string representation of a name of something having the `Name` trait */ object ExNamed { def unapply(name: Name): Option[String] = Some(name.toString) } + /** Returns the full dot-separated names of the symbol as a list of strings */ object ExSymbol { def unapplySeq(t: Tree): Option[Seq[String]] = { Some(t.symbol.fullName.toString.split('.').toSeq) } } + /** Matches nested `Select(Select(...Select(a, b) ...y) , z)` and returns the list `a,b, ... y,z` */ object ExSelected { def unapplySeq(select: Select): Option[Seq[String]] = select match { case Select(This(scalaName), name) => @@ -153,8 +163,8 @@ trait ASTExtractors { object StructuralExtractors { import ExtractorHelpers._ + /** Extracts the 'ensuring' contract from an expression. */ object ExEnsuredExpression { - /** Extracts the 'ensuring' contract from an expression. */ def unapply(tree: Apply): Option[(Tree,Tree)] = tree match { case Apply(Select(Apply(TypeApply(ExSelected("scala", "Predef", "Ensuring"), _ :: Nil), body :: Nil), ExNamed("ensuring")), contract :: Nil) => Some((body, contract)) @@ -162,6 +172,7 @@ trait ASTExtractors { } } + /** Matches the `holds` expression at the end of any boolean expression, and return the boolean expression.*/ object ExHoldsExpression { def unapply(tree: Select) : Option[Tree] = tree match { case Select( @@ -172,6 +183,7 @@ trait ASTExtractors { } } + /** Matches an implication `lhs ==> rhs` and returns (lhs, rhs)*/ object ExImplies { def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match { case @@ -189,9 +201,9 @@ trait ASTExtractors { } } + /** Extracts the 'require' contract from an expression (only if it's the + * first call in the block). */ object ExRequiredExpression { - /** Extracts the 'require' contract from an expression (only if it's the - * first call in the block). */ def unapply(tree: Apply): Option[Tree] = tree match { case Apply(ExSelected("scala", "Predef", "require"), contractBody :: Nil) => Some(contractBody) @@ -199,6 +211,7 @@ trait ASTExtractors { } } + /** Extracts the `(input, output) passes { case In => Out ...}` and returns (input, output, list of case classes) */ object ExPasses { def unapply(tree : Apply) : Option[(Tree, Tree, List[CaseDef])] = tree match { case Apply( @@ -223,7 +236,7 @@ trait ASTExtractors { } - + /** Returns a string literal either from leon.lang.string.String or from a constant string literal. */ object ExStringLiteral { def unapply(tree: Tree): Option[String] = tree match { case Apply(ExSelected("leon", "lang", "string", "package", "strToStr"), (str: Literal) :: Nil) => @@ -235,6 +248,7 @@ trait ASTExtractors { } } + /** Returns the arguments of an unapply pattern */ object ExUnapplyPattern { def unapply(tree: Tree): Option[(Symbol, Seq[Tree])] = tree match { case UnApply(Apply(s, _), args) => @@ -243,6 +257,7 @@ trait ASTExtractors { } } + /** Returns the argument of a bigint literal, either from scala or leon */ object ExBigIntLiteral { def unapply(tree: Tree): Option[Tree] = tree match { case Apply(ExSelected("scala", "package", "BigInt", "apply"), n :: Nil) => @@ -254,6 +269,7 @@ trait ASTExtractors { } } + /** Returns the two components (n, d) of a real n/d literal */ object ExRealLiteral { def unapply(tree: Tree): Option[(Tree, Tree)] = tree match { case Apply(ExSelected("leon", "lang", "Real", "apply"), n :: d :: Nil) => @@ -262,6 +278,8 @@ trait ASTExtractors { None } } + + /** Matches Real(x) when n is an integer and returns x */ object ExRealIntLiteral { def unapply(tree: Tree): Option[Tree] = tree match { case Apply(ExSelected("leon", "lang", "Real", "apply"), n :: Nil) => @@ -271,7 +289,7 @@ trait ASTExtractors { } } - + /** Matches the construct int2bigInt(a) and returns a */ object ExIntToBigInt { def unapply(tree: Tree): Option[Tree] = tree match { case Apply(ExSelected("math", "BigInt", "int2bigInt"), tree :: Nil) => Some(tree) @@ -279,7 +297,7 @@ trait ASTExtractors { } } - + /** Matches the construct List[tpe](a, b, ...) and returns tpe and arguments */ object ExListLiteral { def unapply(tree: Apply): Option[(Tree, List[Tree])] = tree match { case Apply( @@ -291,9 +309,9 @@ trait ASTExtractors { } } + /** Extracts the 'assert' contract from an expression (only if it's the + * first call in the block). */ object ExAssertExpression { - /** Extracts the 'assert' contract from an expression (only if it's the - * first call in the block). */ def unapply(tree: Apply): Option[(Tree, Option[String])] = tree match { case Apply(ExSelected("scala", "Predef", "assert"), contractBody :: Nil) => Some((contractBody, None)) @@ -304,11 +322,10 @@ trait ASTExtractors { } } - + /** Matches an object with no type parameters, and regardless of its + * visibility. Does not match on case objects or the automatically generated companion + * objects of case classes (or any synthetic class). */ object ExObjectDef { - /** Matches an object with no type parameters, and regardless of its - * visibility. Does not match on case objects or the automatically generated companion - * objects of case classes (or any synthetic class). */ def unapply(cd: ClassDef): Option[(String,Template)] = cd match { case ClassDef(_, name, tparams, impl) if (cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) && @@ -322,10 +339,10 @@ trait ASTExtractors { } } + /** Matches an abstract class or a trait with no type parameters, no + * constructor args (in the case of a class), no implementation details, + * no abstract members. */ object ExAbstractClass { - /** Matches an abstract class or a trait with no type parameters, no - * constrctor args (in the case of a class), no implementation details, - * no abstract members. */ def unapply(cd: ClassDef): Option[(String, Symbol, Template)] = cd match { // abstract class case ClassDef(_, name, tparams, impl) if cd.symbol.isAbstractClass => Some((name.toString, cd.symbol, impl)) @@ -334,10 +351,12 @@ trait ASTExtractors { } } + /** Returns true if the class definition is a case class */ private def isCaseClass(cd: ClassDef): Boolean = { cd.symbol.isCase && !cd.symbol.isAbstractClass && cd.impl.body.size >= 8 } + /** Returns true if the class definition is an implicit class */ private def isImplicitClass(cd: ClassDef): Boolean = { cd.symbol.isImplicit } diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index 299e8995a072084bba0adf0a98603e64b1611aac..a8732f3af9dc9cd849f17f218012bab112a107c4 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -892,16 +892,8 @@ trait CodeExtraction extends ASTExtractors { case ExInt32Literal(i) => (LiteralPattern(binder, IntLiteral(i)), dctx) case ExBooleanLiteral(b) => (LiteralPattern(binder, BooleanLiteral(b)), dctx) case ExUnitLiteral() => (LiteralPattern(binder, UnitLiteral()), dctx) - case sLit@ExStringLiteral(s) => - val consClass = libraryCaseClass(sLit.pos, "leon.collection.Cons") - val nilClass = libraryCaseClass(sLit.pos, "leon.collection.Nil") - val nil = CaseClassPattern(None, CaseClassType(nilClass, Seq(CharType)), Seq()) - val consType = CaseClassType(consClass, Seq(CharType)) - def mkCons(hd: Pattern, tl: Pattern) = CaseClassPattern(None, consType, Seq(hd,tl)) - val chars = s.toCharArray//.asInstanceOf[Seq[Char]] - def charPat(ch : Char) = LiteralPattern(None, CharLiteral(ch)) - (chars.foldRight(nil)( (ch: Char, p : Pattern) => mkCons( charPat(ch), p)), dctx) - + case ExStringLiteral(s) => (LiteralPattern(binder, StringLiteral(s)), dctx) + case up@ExUnapplyPattern(s, args) => implicit val p: Position = NoPosition val fd = getFunDef(s, up.pos) @@ -1485,22 +1477,13 @@ trait CodeExtraction extends ASTExtractors { 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)) - + StringLiteral(s) case ExImplies(lhs, rhs) => Implies(extractTree(lhs), extractTree(rhs)).setPos(current.pos) case c @ ExCall(rec, sym, tps, args) => + println("Parsing call:" + c) val rrec = rec match { case t if (defsToDefs contains sym) && !isMethod(sym) => null @@ -1538,6 +1521,23 @@ trait CodeExtraction extends ASTExtractors { caseClassSelector(cct, rec, fieldID) + //String methods + case (IsTyped(a1, StringType), "toString", List()) => + a1 + case (IsTyped(a1, CanHaveStringType(t)), "toString", List()) => + ToString(a1) + case (IsTyped(a1, StringType), "+", List(IsTyped(a2, StringType))) => + StringConcat(a1, a2) + case (IsTyped(a1, StringType), "+", List(IsTyped(a2, CanHaveStringType(t)))) => + StringConcat(a1, ToString(a2)) + case (IsTyped(a1, CanHaveStringType(t)), "+", List(IsTyped(a2, StringType))) => + StringConcat(ToString(a1), a2) + case (IsTyped(a1, StringType), "length", List()) => + StringLength(a1) + case (IsTyped(a1, StringType), "substring", List(IsTyped(start, IntegerType | Int32Type))) => + SubString(a1, start, StringLength(a1)) + case (IsTyped(a1, StringType), "substring", List(IsTyped(start, IntegerType | Int32Type), IsTyped(end, IntegerType | Int32Type))) => + SubString(a1, start, end) //BigInt methods case (IsTyped(a1, IntegerType), "+", List(IsTyped(a2, IntegerType))) => Plus(a1, a2) @@ -1711,8 +1711,12 @@ trait CodeExtraction extends ASTExtractors { case (IsTyped(a1, CharType), "<=", List(IsTyped(a2, CharType))) => LessEquals(a1, a2) - case (_, name, _) => - outOfSubsetError(tr, "Unknown call to "+name) + case (a1, name, a2) => + val typea1 = a1.getType + val typea2 = a2.map(_.getType).mkString(",") + val sa2 = a2.mkString(",") + println(Thread.currentThread().getStackTrace.take(5).mkString("\n")) + outOfSubsetError(tr, "Unknown call to " + name + s" on $a1 ($typea1) with arguments $sa2 of type $typea2") } // default behaviour is to complain :) @@ -1755,6 +1759,9 @@ trait CodeExtraction extends ASTExtractors { case TypeRef(_, sym, _) if isRealSym(sym) => RealType + + case TypeRef(_, sym, _) if isStringSym(sym) => + StringType case TypeRef(_, sym, btt :: Nil) if isScalaSetSym(sym) => outOfSubsetError(pos, "Scala's Set API is no longer extracted. Make sure you import leon.lang.Set that defines supported Set operations.") @@ -1792,7 +1799,7 @@ trait CodeExtraction extends ASTExtractors { case TypeRef(_, sym, tps) if isByNameSym(sym) => extractType(tps.head) - case TypeRef(_, sym, tps) => + case tr @ TypeRef(_, sym, tps) => val leontps = tps.map(extractType) if (sym.isAbstractType) { diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala index 7216652a427e6784142a17f69c730fa61e2ff0aa..687fbccfd0b659e2b83b4469299617be510c2ded 100644 --- a/src/main/scala/leon/purescala/Expressions.scala +++ b/src/main/scala/leon/purescala/Expressions.scala @@ -416,6 +416,10 @@ object Expressions { val getType = UnitType val value = () } + /** $encodingof a string literal */ + case class StringLiteral(value: String) extends Literal[String] { + val getType = StringType + } /** Generic values. Represent values of the generic type `tp`. @@ -542,7 +546,39 @@ object Expressions { else Untyped } } - + + /** Returns true if the underlined type can be converted to a String */ + object CanHaveStringType { + def apply(t: TypeTree): Boolean = t match { case BooleanType | Int32Type | IntegerType | CharType | RealType | StringType => true case _ => false } + def unapply(t: TypeTree) = if(apply(t)) Some(t) else None + } + + /* String Theory */ + /** $encodingof `expr.toString` for strings */ + case class ToString(expr: Expr) extends Expr { + val getType = if(CanHaveStringType(expr.getType)) StringType else Untyped + } + /** $encodingof `lhs + rhs` for strings */ + case class StringConcat(lhs: Expr, rhs: Expr) extends Expr { + val getType = { + if (CanHaveStringType(lhs.getType) || CanHaveStringType(rhs.getType)) StringType + else Untyped + } + } + /** $encodingof `lhs.subString(start, end)` for strings */ + case class SubString(expr: Expr, start: Expr, end: Expr) extends Expr { + val getType = { + if (expr.getType == StringType && (start == IntegerType || start == Int32Type) && (end == IntegerType || end == Int32Type)) StringType + else Untyped + } + } + /** $encodingof `lhs.length` for strings */ + case class StringLength(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 cd57d2187fe0cd59d45e3d88e17b0926e2279412..abe8dbe1a27c730f8d9ccefd05522bc8a0d9120f 100644 --- a/src/main/scala/leon/purescala/Extractors.scala +++ b/src/main/scala/leon/purescala/Extractors.scala @@ -235,22 +235,6 @@ object Extractors { trait Extractable { def extract: Option[(Seq[Expr], Seq[Expr] => Expr)] } - - object StringLiteral { - def unapply(e: Expr)(implicit pgm: Program): Option[String] = e match { - case CaseClass(cct, args) => - for { - libS <- pgm.library.String - if cct.classDef == libS - (_, chars) <- isListLiteral(args.head) - if chars.forall(_.isInstanceOf[CharLiteral]) - } yield { - chars.collect{ case CharLiteral(c) => c }.mkString - } - case _ => - None - } - } object TopLevelOrs { // expr1 AND (expr2 AND (expr3 AND ..)) => List(expr1, expr2, expr3) def unapply(e: Expr): Option[Seq[Expr]] = e match { diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala index 6b22810e542bdb9af65251da1c9a4d4ab1ab7142..a861a74275f3dcb3f7066d3de9e7b1aae67df575 100644 --- a/src/main/scala/leon/purescala/PrettyPrinter.scala +++ b/src/main/scala/leon/purescala/PrettyPrinter.scala @@ -168,6 +168,7 @@ class PrettyPrinter(opts: PrinterOptions, case CharLiteral(v) => p"$v" case BooleanLiteral(v) => p"$v" case UnitLiteral() => p"()" + case StringLiteral(v) => p""""$v"""" case GenericValue(tp, id) => p"$tp#$id" case Tuple(exprs) => p"($exprs)" case TupleSelect(t, i) => p"$t._$i" @@ -410,6 +411,7 @@ class PrettyPrinter(opts: PrinterOptions, case RealType => p"Real" case CharType => p"Char" case BooleanType => p"Boolean" + case StringType => p"String" case ArrayType(bt) => p"Array[$bt]" case SetType(bt) => p"Set[$bt]" case MapType(ft,tt) => p"Map[$ft, $tt]" diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala index d39fda3338fbeab4dfa9c453a58afa6298bb6ccd..e69678d1f658f8c94033522163f8c332e8025a48 100644 --- a/src/main/scala/leon/purescala/Types.scala +++ b/src/main/scala/leon/purescala/Types.scala @@ -51,6 +51,7 @@ object Types { abstract class BitVectorType(val size: Int) extends TypeTree case object Int32Type extends BitVectorType(32) + case object StringType extends TypeTree class TypeParameter private (name: String) extends TypeTree { val id = FreshIdentifier(name, this) diff --git a/testcases/stringrender/IntWrapperRender.scala b/testcases/stringrender/IntWrapperRender.scala index 5aa2d48c7a00949e0b69c5a6f39b7b962d1e5244..c723e0f5a60172529bf46797ad2f6306c8919010 100644 --- a/testcases/stringrender/IntWrapperRender.scala +++ b/testcases/stringrender/IntWrapperRender.scala @@ -6,7 +6,7 @@ */ import leon.lang._ -import string.String +//import string.String import leon.annotation._ import leon.collection._ import leon.collection.ListOps._ @@ -15,50 +15,50 @@ import leon.lang.synthesis._ object IntWrapperRender { case class IntWrapper(i: Int) - def psStandard(s: IntWrapper)(res: String) = (s, res) passes { + @inline def psStandard(s: IntWrapper) = (res: String) => (s, res) passes { case IntWrapper(0) => "IntWrapper(0)" case IntWrapper(-1) => "IntWrapper(-1)" case IntWrapper(12) => "IntWrapper(12)" } - def psUnwrapped(s: IntWrapper)(res: String) = (s, res) passes { + @inline def psUnwrapped(s: IntWrapper) = (res: String) => (s, res) passes { case IntWrapper(0) => "0" case IntWrapper(-1) => "-1" case IntWrapper(12) => "12" } - def psNameChangedPrefix(s: IntWrapper)(res: String) = (s, res) passes { + @inline def psNameChangedPrefix(s: IntWrapper) = (res: String) => (s, res) passes { case IntWrapper(0) => "number: 0" case IntWrapper(-1) => "number: -1" case IntWrapper(12) => "number: 12" } - def psNameChangedSuffix(s: IntWrapper)(res: String) = (s, res) passes { + @inline def psNameChangedSuffix(s: IntWrapper) = (res: String) => (s, res) passes { case IntWrapper(0) => "0.0" case IntWrapper(-1) => "-1.0" // Here there should be an ambiguity before this line. case IntWrapper(12) => "12.0" } - def psDuplicate(s: IntWrapper)(res: String) = (s, res) passes { + @inline def psDuplicate(s: IntWrapper) = (res: String) => (s, res) passes { case IntWrapper(0) => "0 0" case IntWrapper(-1) => "-1 -1" case IntWrapper(12) => "12 12" } - def repairUnWrapped(s: IntWrapper): String = { - "IntWrapper(" + s.i + ")"" - } ensuring psUnWrapped(s) + def repairUnwrapped(s: IntWrapper): String = { + "IntWrapper(" + s.i + ")" + } ensuring psUnwrapped(s) def repairNameChangedPrefix(s: IntWrapper): String = { - "IntWrapper(" + s.i + ")"" + "IntWrapper(" + s.i + ")" } ensuring psNameChangedPrefix(s) def repairNameChangedSuffix(s: IntWrapper): String = { - "IntWrapper(" + s.i + ")"" + "IntWrapper(" + s.i + ")" } ensuring psNameChangedSuffix(s) def repairDuplicate(s: IntWrapper): String = { - "IntWrapper(" + s.i + ")"" + "IntWrapper(" + s.i + ")" } ensuring psDuplicate(s) def synthesisStandard(s: IntWrapper): String = {