From 95e3848ecf7d528856f379cd894ddeb272cd25d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Fri, 6 May 2016 11:22:09 +0200
Subject: [PATCH] Fixed code extraction issues for bigLength and bigSubstring
Fixed compilation issue in String.scala Made sure (...).substring(start) is
extracted as a lset in order to not recompute the body twice (and adapted the
pretty-printer)
---
library/lang/package.scala | 10 +++---
library/theories/String.scala | 2 +-
.../leon/frontends/scalac/ASTExtractors.scala | 33 +++++++++++++++++++
.../frontends/scalac/CodeExtraction.scala | 30 ++++++++++++-----
.../scala/leon/purescala/PrettyPrinter.scala | 6 ++++
5 files changed, 68 insertions(+), 13 deletions(-)
diff --git a/library/lang/package.scala b/library/lang/package.scala
index c10c02582..9c3c72d42 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -70,10 +70,12 @@ package object lang {
}
implicit class StringDecorations(val underlying: String) {
- @ignore
- def bigLength = BigInt(underlying.length)
- @ignore
- def bigsubstring(start: BigInt, end: BigInt): String = underlying.substring(start.toInt, end.toInt)
+ @ignore @inline
+ def bigLength() = BigInt(underlying.length)
+ @ignore @inline
+ def bigSubstring(start: BigInt): String = underlying.substring(start.toInt)
+ @ignore @inline
+ def bigSubstring(start: BigInt, end: BigInt): String = underlying.substring(start.toInt, end.toInt)
}
@ignore
diff --git a/library/theories/String.scala b/library/theories/String.scala
index 745501578..8057c2d2a 100644
--- a/library/theories/String.scala
+++ b/library/theories/String.scala
@@ -11,7 +11,7 @@ sealed abstract class String {
}) ensuring (_ >= 0)
def sizeI: Int = this match {
- case StringCons(_, tail) => 1 + tail.length
+ case StringCons(_, tail) => 1 + tail.sizeI
case StringNil() => 0
}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 45ddea6ad..02a58ad29 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -185,6 +185,39 @@ trait ASTExtractors {
case _ => None
}
}
+
+ /** Matches the `bigLength` expression at the end of any string expression, and returns the expression.*/
+ object ExBigLengthExpression {
+ def unapply(tree: Apply) : Option[Tree] = tree match {
+ case Apply(Select(
+ Apply(ExSelected("leon", "lang", "package", "StringDecorations"), stringExpr :: Nil),
+ ExNamed("bigLength")), Nil)
+ => Some(stringExpr)
+ case _ => None
+ }
+ }
+
+ /** Matches the `bigSubstring` method at the end of any string expression, and returns the expression and the start index expression.*/
+ object ExBigSubstringExpression {
+ def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
+ case Apply(Select(
+ Apply(ExSelected("leon", "lang", "package", "StringDecorations"), stringExpr :: Nil),
+ ExNamed("bigSubstring")), startExpr :: Nil)
+ => Some(stringExpr, startExpr)
+ case _ => None
+ }
+ }
+
+ /** Matches the `bigSubstring` expression at the end of any string expression, and returns the expression, the start and end index expressions.*/
+ object ExBigSubstring2Expression {
+ def unapply(tree: Apply) : Option[(Tree, Tree, Tree)] = tree match {
+ case Apply(Select(
+ Apply(ExSelected("leon", "lang", "package", "StringDecorations"), stringExpr :: Nil),
+ ExNamed("bigSubstring")), startExpr :: endExpr :: Nil)
+ => Some(stringExpr, startExpr, endExpr)
+ case _ => None
+ }
+ }
/** Matches an implication `lhs ==> rhs` and returns (lhs, rhs)*/
object ExImplies {
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 9c3e4b393..e37ce4c98 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1195,6 +1195,23 @@ trait CodeExtraction extends ASTExtractors {
Ensuring(output_expr, post)
+ case t @ ExBigLengthExpression(input) =>
+ val input_expr = extractTreeOrNoTree(input).setPos(input.pos)
+ StringBigLength(input_expr)
+ case t @ ExBigSubstringExpression(input, start) =>
+ val input_expr = extractTreeOrNoTree(input).setPos(input.pos)
+ val start_expr = extractTreeOrNoTree(start).setPos(start.pos)
+ val s = FreshIdentifier("s", StringType)
+ let(s, input_expr,
+ BigSubString(Variable(s), start_expr, StringBigLength(Variable(s)))
+ )
+
+ case t @ ExBigSubstring2Expression(input, start, end) =>
+ val input_expr = extractTreeOrNoTree(input).setPos(input.pos)
+ val start_expr = extractTreeOrNoTree(start).setPos(start.pos)
+ val end_expr = extractTreeOrNoTree(end).setPos(end.pos)
+ BigSubString(input_expr, start_expr, end_expr)
+
case ExAssertExpression(contract, oerr) =>
val const = extractTree(contract)
val b = rest.map(extractTreeOrNoTree).getOrElse(UnitLiteral())
@@ -1728,17 +1745,14 @@ trait CodeExtraction extends ASTExtractors {
StringConcat(converter(a1), a2)
case (IsTyped(a1, StringType), "length", List()) =>
StringLength(a1)
- case (IsTyped(a1, StringType), "bigLength", List()) =>
- StringBigLength(a1)
case (IsTyped(a1, StringType), "substring", List(IsTyped(start, Int32Type))) =>
- SubString(a1, start, StringLength(a1))
+ val s = FreshIdentifier("s", StringType)
+ let(s, a1,
+ SubString(Variable(s), start, StringLength(Variable(s)))
+ )
case (IsTyped(a1, StringType), "substring", List(IsTyped(start, Int32Type), IsTyped(end, Int32Type))) =>
SubString(a1, start, end)
- case (IsTyped(a1, StringType), "bigSubstring", List(IsTyped(start, IntegerType))) =>
- BigSubString(a1, start, StringBigLength(a1))
- case (IsTyped(a1, StringType), "bigSubstring", List(IsTyped(start, IntegerType), IsTyped(end, IntegerType))) =>
- BigSubString(a1, start, end)
-
+
//BigInt methods
case (IsTyped(a1, IntegerType), "+", List(IsTyped(a2, IntegerType))) =>
Plus(a1, a2)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index bda0e0612..b812bcf57 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -86,6 +86,12 @@ class PrettyPrinter(opts: PrinterOptions,
case Variable(id) =>
p"$id"
+
+ case Let(id, expr, SubString(Variable(id2), start, StringLength(Variable(id3)))) if id == id2 && id2 == id3 =>
+ p"$expr.substring($start)"
+
+ case Let(id, expr, BigSubString(Variable(id2), start, StringLength(Variable(id3)))) if id == id2 && id2 == id3 =>
+ p"$expr.bigSubstring($start)"
case Let(b,d,e) =>
p"""|val $b = $d
--
GitLab