From 25a5d2c76c533527244471595b06e6fd08559450 Mon Sep 17 00:00:00 2001
From: ravi <ravi.kandhadai@epfl.ch>
Date: Tue, 19 Apr 2016 17:31:32 +0200
Subject: [PATCH] Fixing extraction of lambda applications with zero arguments
---
.../leon/frontends/scalac/ASTExtractors.scala | 89 +++++++++----------
.../frontends/scalac/CodeExtraction.scala | 32 +++----
2 files changed, 54 insertions(+), 67 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 1d107703b..45ddea6ad 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -53,7 +53,7 @@ trait ASTExtractors {
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)
+ require(0 <= i && i <= 22)
classFromName("scala.Function" + i)
}
@@ -64,7 +64,7 @@ trait ASTExtractors {
def isBigIntSym(sym : Symbol) : Boolean = getResolvedTypeSym(sym) == bigIntSym
- def isStringSym(sym : Symbol) : Boolean = getResolvedTypeSym(sym) match { case `stringSym` => true case _ => false }
+ def isStringSym(sym : Symbol) : Boolean = getResolvedTypeSym(sym) match { case `stringSym` => true case _ => false }
def isByNameSym(sym : Symbol) : Boolean = getResolvedTypeSym(sym) == byNameSym
@@ -101,28 +101,26 @@ trait ASTExtractors {
getResolvedTypeSym(sym) == scalaMapSym
}
-
def isOptionClassSym(sym : Symbol) : Boolean = {
sym == optionClassSym || sym == someClassSym
}
def isFunction(sym : Symbol, i: Int) : Boolean =
- 1 <= i && i <= 22 && sym == functionTraitSym(i)
-
+ 0 <= i && i <= 22 && sym == functionTraitSym(i)
def isArrayClassSym(sym: Symbol): Boolean = sym == arraySym
- def hasIntType(t : Tree) = {
+ def hasIntType(t : Tree) = {
val tpe = t.tpe.widen
tpe =:= IntClass.tpe
}
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?!) */
@@ -215,8 +213,7 @@ trait ASTExtractors {
case _ => None
}
}
-
-
+
/** Matches the `A computes B` expression at the end of any expression A, and returns (A, B).*/
object ExComputesExpression {
def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
@@ -227,7 +224,7 @@ trait ASTExtractors {
case _ => None
}
}
-
+
/** Matches the `O ask I` expression at the end of any expression O, and returns (I, O).*/
object ExAskExpression {
def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
@@ -238,7 +235,7 @@ trait ASTExtractors {
case _ => None
}
}
-
+
object ExByExampleExpression {
def unapply(tree: Apply) : Option[(Tree, Tree)] = tree match {
case Apply(TypeApply(ExSelected("leon", "lang", "package", "byExample"), List(_, _)), input :: res_output :: Nil)
@@ -246,19 +243,19 @@ trait ASTExtractors {
case _ => None
}
}
-
+
/** Extracts the `(input, output) passes { case In => Out ...}` and returns (input, output, list of case classes) */
- object ExPasses {
+ object ExPasses {
def unapply(tree : Apply) : Option[(Tree, Tree, List[CaseDef])] = tree match {
case Apply(
Select(
Apply(
TypeApply(
- ExSelected("leon", "lang", "package", "Passes"),
+ ExSelected("leon", "lang", "package", "Passes"),
List(_, _)
),
List(ExpressionExtractors.ExTuple(_, Seq(in,out)))
- ),
+ ),
ExNamed("passes")
),
List(Function(
@@ -271,11 +268,10 @@ trait ASTExtractors {
}
}
-
/** Returns a string literal from a constant string literal. */
object ExStringLiteral {
def unapply(tree: Tree): Option[String] = tree match {
- case Literal(c @ Constant(i)) if c.tpe == StringClass.tpe =>
+ case Literal(c @ Constant(i)) if c.tpe == StringClass.tpe =>
Some(c.stringValue)
case _ =>
None
@@ -312,7 +308,7 @@ trait ASTExtractors {
None
}
}
-
+
/** Matches Real(x) when n is an integer and returns x */
object ExRealIntLiteral {
def unapply(tree: Tree): Option[Tree] = tree match {
@@ -409,8 +405,8 @@ trait ASTExtractors {
//impl.children foreach println
val symbols = impl.children.collect {
- case df@DefDef(_, name, _, _, _, _) if
- df.symbol.isAccessor && df.symbol.isParamAccessor
+ case df@DefDef(_, name, _, _, _, _) if
+ df.symbol.isAccessor && df.symbol.isParamAccessor
&& !name.endsWith("_$eq") => df.symbol
}
//println("symbols: " + symbols)
@@ -439,16 +435,16 @@ trait ASTExtractors {
}
}
}
-
+
object ExCompanionObjectSynthetic {
def unapply(cd : ClassDef) : Option[(String, Symbol, Template)] = {
- val sym = cd.symbol
+ val sym = cd.symbol
cd match {
case ClassDef(_, name, tparams, impl) if sym.isModule && sym.isSynthetic => //FIXME flags?
Some((name.toString, sym, impl))
case _ => None
}
-
+
}
}
@@ -477,7 +473,7 @@ trait ASTExtractors {
}
object ExFunctionDef {
- /** Matches a function with a single list of arguments,
+ /** Matches a function with a single list of arguments,
* and regardless of its visibility.
*/
def unapply(dd: DefDef): Option[(Symbol, Seq[Symbol], Seq[ValDef], Type, Tree)] = dd match {
@@ -501,7 +497,7 @@ trait ASTExtractors {
object ExLazyAccessorFunction {
def unapply(dd: DefDef): Option[(Symbol, Type, Tree)] = dd match {
case DefDef(_, name, tparams, vparamss, tpt, rhs) if(
- vparamss.size <= 1 && name != nme.CONSTRUCTOR &&
+ vparamss.size <= 1 && name != nme.CONSTRUCTOR &&
!dd.symbol.isSynthetic && dd.symbol.isAccessor && dd.symbol.isLazy
) =>
Some((dd.symbol, tpt.tpe, rhs))
@@ -512,7 +508,7 @@ trait ASTExtractors {
object ExMutatorAccessorFunction {
def unapply(dd: DefDef): Option[(Symbol, Seq[Symbol], Seq[ValDef], Type, Tree)] = dd match {
case DefDef(_, name, tparams, vparamss, tpt, rhs) if(
- vparamss.size <= 1 && name != nme.CONSTRUCTOR &&
+ vparamss.size <= 1 && name != nme.CONSTRUCTOR &&
!dd.symbol.isSynthetic && dd.symbol.isAccessor && name.endsWith("_$eq")
) =>
Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
@@ -527,7 +523,7 @@ trait ASTExtractors {
vd match {
// Implemented fields
case ValDef(mods, name, tpt, rhs) if (
- !sym.isCaseAccessor && !sym.isParamAccessor &&
+ !sym.isCaseAccessor && !sym.isParamAccessor &&
!sym.isLazy && !sym.isSynthetic && !sym.isAccessor && sym.isVar
) =>
println("matched a var accessor field: sym is: " + sym)
@@ -538,7 +534,7 @@ trait ASTExtractors {
}
}
}
-
+
object ExFieldDef {
/** Matches a definition of a strict field inside a class constructor */
def unapply(vd: SymTree) : Option[(Symbol, Type, Tree)] = {
@@ -546,7 +542,7 @@ trait ASTExtractors {
vd match {
// Implemented fields
case ValDef(mods, name, tpt, rhs) if (
- !sym.isCaseAccessor && !sym.isParamAccessor &&
+ !sym.isCaseAccessor && !sym.isParamAccessor &&
!sym.isLazy && !sym.isSynthetic && !sym.isAccessor && !sym.isVar
) =>
// Since scalac uses the accessor symbol all over the place, we pass that instead:
@@ -561,10 +557,10 @@ trait ASTExtractors {
}
}
}
-
+
object ExLazyFieldDef {
/** Matches lazy field definitions.
- * WARNING: Do NOT use this as extractor for lazy fields,
+ * WARNING: Do NOT use this as extractor for lazy fields,
* as it does not contain the body of the lazy definition.
* It is here just to signify a Definition acceptable by Leon
*/
@@ -572,16 +568,16 @@ trait ASTExtractors {
val sym = vd.symbol
vd match {
case ValDef(mods, name, tpt, rhs) if (
- sym.isLazy && !sym.isCaseAccessor && !sym.isParamAccessor &&
- !sym.isSynthetic && !sym.isAccessor
- ) =>
+ sym.isLazy && !sym.isCaseAccessor && !sym.isParamAccessor &&
+ !sym.isSynthetic && !sym.isAccessor
+ ) =>
// Since scalac uses the accessor symbol all over the place, we pass that instead:
true
case _ => false
}
}
}
-
+
object ExFieldAccessorFunction{
/** Matches the accessor function of a field
* WARNING: This is not meant to be used for any useful purpose,
@@ -589,7 +585,7 @@ trait ASTExtractors {
*/
def unapply(dd: DefDef): Boolean = dd match {
case DefDef(_, name, tparams, vparamss, tpt, rhs) if(
- vparamss.size <= 1 && name != nme.CONSTRUCTOR &&
+ vparamss.size <= 1 && name != nme.CONSTRUCTOR &&
dd.symbol.isAccessor && !dd.symbol.isLazy
) =>
true
@@ -603,8 +599,8 @@ trait ASTExtractors {
val sym = dd.symbol
dd match {
case DefDef(_, name, tparams, vparamss, tpt, rhs) if(
- vparamss.size <= 1 && name != nme.CONSTRUCTOR && sym.isSynthetic
- ) =>
+ vparamss.size <= 1 && name != nme.CONSTRUCTOR && sym.isSynthetic
+ ) =>
// Split the name into pieces, to find owner of the parameter + param.index
// Form has to be <owner name>$default$<param index>
@@ -617,13 +613,13 @@ trait ASTExtractors {
Some((sym, tparams.map(_.symbol), vparamss.headOption.getOrElse(Nil), tpt.tpe, ownerString, index, rhs))
} catch {
case _ : NumberFormatException | _ : IllegalArgumentException | _ : ArrayIndexOutOfBoundsException =>
- None
+ None
}
-
+
case _ => None
}
}
- }
+ }
}
@@ -714,7 +710,6 @@ trait ASTExtractors {
}
}
-
object ExValDef {
/** Extracts val's in the head of blocks. */
def unapply(tree: ValDef): Option[(Symbol,Tree,Tree)] = tree match {
@@ -928,7 +923,7 @@ trait ASTExtractors {
case _ => None
}
}
-
+
object ExOr {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
case Apply(s @ Select(lhs, _), List(rhs)) if s.symbol == Boolean_or =>
@@ -936,14 +931,14 @@ trait ASTExtractors {
case _ => None
}
}
-
+
object ExNot {
def unapply(tree: Select): Option[Tree] = tree match {
case Select(t, n) if n == nme.UNARY_! => Some(t)
case _ => None
}
}
-
+
object ExEquals {
def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
case Apply(Select(lhs, n), List(rhs)) if n == nme.EQ => Some((lhs,rhs))
@@ -1079,7 +1074,7 @@ trait ASTExtractors {
}
}
- object ExCall {
+ object ExCall {
def unapply(tree: Tree): Option[(Tree, Symbol, Seq[Tree], Seq[Tree])] = tree match {
// foo / foo[T]
case ExParameterLessCall(t, s, tps) =>
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 4efc43706..dfab2acc8 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -304,7 +304,6 @@ trait CodeExtraction extends ASTExtractors {
case d if d.symbol.isVar =>
None
-
// Everything else is unexpected
case tree =>
println(tree)
@@ -455,10 +454,8 @@ trait CodeExtraction extends ASTExtractors {
}
}
-
private var paramsToDefaultValues = Map[Symbol,FunDef]()
-
def getClassDef(sym: Symbol, pos: Position): LeonClassDef = {
classesToClasses.get(sym) match {
case Some(cd) => cd
@@ -594,7 +591,7 @@ trait CodeExtraction extends ASTExtractors {
def computeChains(tpe: LeonType): Map[TypeParameterDef, Set[LeonClassDef]] = {
var seen: Set[LeonClassDef] = Set.empty
var chains: Map[TypeParameterDef, Set[LeonClassDef]] = Map.empty
-
+
def rec(tpe: LeonType): Set[LeonClassDef] = tpe match {
case ct: ClassType =>
val root = ct.classDef.root
@@ -651,7 +648,6 @@ trait CodeExtraction extends ASTExtractors {
isMethod += fsym
val fd = defineFunDef(fsym, Some(cd))(defCtx)
-
methodToClass += fd -> cd
cd.registerMethod(fd)
@@ -1031,7 +1027,7 @@ trait CodeExtraction extends ASTExtractors {
case ExBooleanLiteral(b) => (LiteralPattern(binder, BooleanLiteral(b)), dctx)
case ExUnitLiteral() => (LiteralPattern(binder, UnitLiteral()), 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)
@@ -1133,27 +1129,27 @@ trait CodeExtraction extends ASTExtractors {
case t @ ExComputesExpression(body, expected) =>
val b = extractTreeOrNoTree(body).setPos(body.pos)
val expected_expr = extractTreeOrNoTree(expected).setPos(expected.pos)
-
+
val resId = FreshIdentifier("res", b.getType).setPos(current.pos)
val post = Lambda(Seq(LeonValDef(resId)), Equals(Variable(resId), expected_expr)).setPos(current.pos)
Ensuring(b, post)
-
+
case t @ ExByExampleExpression(input, output) =>
val input_expr = extractTreeOrNoTree(input).setPos(input.pos)
val output_expr = extractTreeOrNoTree(output).setPos(output.pos)
Passes(input_expr, output_expr, MatchCase(WildcardPattern(None), Some(BooleanLiteral(false)), NoTree(output_expr.getType))::Nil)
-
+
case t @ ExAskExpression(input, output) =>
val input_expr = extractTreeOrNoTree(input).setPos(input.pos)
val output_expr = extractTreeOrNoTree(output).setPos(output.pos)
-
+
val resId = FreshIdentifier("res", output_expr.getType).setPos(current.pos)
val post = Lambda(Seq(LeonValDef(resId)),
Passes(input_expr, Variable(resId), MatchCase(WildcardPattern(None), Some(BooleanLiteral(false)), NoTree(output_expr.getType))::Nil)).setPos(current.pos)
Ensuring(output_expr, post)
-
+
case ExAssertExpression(contract, oerr) =>
val const = extractTree(contract)
val b = rest.map(extractTreeOrNoTree).getOrElse(UnitLiteral())
@@ -1243,7 +1239,6 @@ trait CodeExtraction extends ASTExtractors {
rest = None
Let(newID, valTree, restTree)
-
case d @ ExFunctionDef(sym, tparams, params, ret, b) =>
val fd = defineFunDef(sym)
@@ -1258,13 +1253,13 @@ trait CodeExtraction extends ASTExtractors {
case None => UnitLiteral()
}
rest = None
-
+
val oldCurrentFunDef = currentFunDef
val funDefWithBody = extractFunBody(fd, params, b)(newDctx)
currentFunDef = oldCurrentFunDef
-
+
val (other_fds, block) = restTree match {
case LetDef(fds, block) =>
(fds, block)
@@ -1426,7 +1421,6 @@ trait CodeExtraction extends ASTExtractors {
WithOracle(newOracles, cBody)
-
case chs @ ExChooseExpression(body) =>
val cBody = extractTree(body)
Choose(cBody)
@@ -1630,7 +1624,7 @@ trait CodeExtraction extends ASTExtractors {
case ExImplies(lhs, rhs) =>
Implies(extractTree(lhs), extractTree(rhs)).setPos(current.pos)
-
+
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.
val rrec = rec match {
@@ -1846,7 +1840,6 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, at: ArrayType), "clone", Nil) =>
a1
-
// Map methods
case (IsTyped(a1, MapType(_, vt)), "apply", List(a2)) =>
MapApply(a1, a2)
@@ -1900,7 +1893,6 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, CharType), "<=", List(IsTyped(a2, CharType))) =>
LessEquals(a1, a2)
-
case (a1, name, a2) =>
val typea1 = a1.getType
val typea2 = a2.map(_.getType).mkString(",")
@@ -1951,7 +1943,7 @@ trait CodeExtraction extends ASTExtractors {
case TypeRef(_, sym, _) if isRealSym(sym) =>
RealType
-
+
case TypeRef(_, sym, _) if isStringSym(sym) =>
StringType
@@ -1986,7 +1978,7 @@ trait CodeExtraction extends ASTExtractors {
ArrayType(extractType(btt))
// TODO: What about Function0?
- case TypeRef(_, sym, subs) if subs.size > 1 && isFunction(sym, subs.size - 1) =>
+ case TypeRef(_, sym, subs) if subs.size >= 1 && isFunction(sym, subs.size - 1) =>
val from = subs.init
val to = subs.last
FunctionType(from map extractType, extractType(to))
--
GitLab