From 0727d73afd6152410bb8ecc254864fbfdcc94154 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Fri, 14 Nov 2014 16:23:48 +0100
Subject: [PATCH] Deprecate patternMatchReconstruction, minimize use of
matchToIfThenElse
---
.../scala/leon/codegen/CodeGeneration.scala | 26 +-
.../scala/leon/codegen/CompilationUnit.scala | 2 -
src/main/scala/leon/purescala/TreeOps.scala | 485 +++++++++---------
.../scala/leon/synthesis/rules/Cegis.scala | 4 +-
src/main/scala/leon/utils/Simplifiers.scala | 7 -
.../leon/verification/DefaultTactic.scala | 8 +-
.../leon/verification/InductionTactic.scala | 12 +-
src/main/scala/leon/verification/Tactic.scala | 7 +-
.../regression/transformations/Match.scala | 46 --
.../test/purescala/TransformationTests.scala | 5 -
10 files changed, 280 insertions(+), 322 deletions(-)
delete mode 100644 src/test/resources/regression/transformations/Match.scala
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 33c5f9db0..493efc40e 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -6,7 +6,7 @@ package codegen
import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
-import purescala.TreeOps.simplestValue
+import purescala.TreeOps.{simplestValue, matchToIfThenElse}
import purescala.TypeTrees._
import purescala.TypeTreeOps.instantiateType
import utils._
@@ -180,14 +180,12 @@ trait CodeGeneration {
bodyWithPre
}
- val exprToCompile = purescala.TreeOps.matchToIfThenElse(bodyWithPost)
-
if (params.recordInvocations) {
// index of monitor object will be before the first Scala parameter
ch << ALoad(paramsOffset-1) << InvokeVirtual(MonitorClass, "onInvoke", "()V")
}
- mkExpr(exprToCompile, ch)(Locals(newMapping, Map.empty, Map.empty, isStatic))
+ mkExpr(bodyWithPost, ch)(Locals(newMapping, Map.empty, Map.empty, isStatic))
funDef.returnType match {
case Int32Type | BooleanType | UnitType =>
@@ -700,6 +698,9 @@ trait CodeGeneration {
case This(ct) =>
ch << ALoad(0) // FIXME what if doInstrument etc
+ case m : MatchExpr =>
+ mkExpr(matchToIfThenElse(m), ch)
+
case b if b.getType == BooleanType && canDelegateToMkBranch =>
val fl = ch.getFreshLabel("boolfalse")
val al = ch.getFreshLabel("boolafter")
@@ -865,6 +866,19 @@ trait CodeGeneration {
mkExpr(l, ch)
mkExpr(r, ch)
ch << If_ICmpGe(thenn) << Goto(elze)
+
+ case IfExpr(c, t, e) =>
+ val innerThen = ch.getFreshLabel("then")
+ val innerElse = ch.getFreshLabel("else")
+ mkBranch(c, innerThen, innerElse, ch)
+ ch << Label(innerThen)
+ mkBranch(t, thenn, elze, ch)
+ ch << Label(innerElse)
+ mkBranch(e, thenn, elze, ch)
+
+ case cci@CaseClassInstanceOf(cct, e) =>
+ mkExpr(cci, ch)
+ ch << IfEq(elze) << Goto(thenn)
case other if canDelegateToMkExpr =>
mkExpr(other, ch, canDelegateToMkBranch = false)
@@ -943,7 +957,7 @@ trait CodeGeneration {
METHOD_ACC_PUBLIC
})
val ch = accM.codeHandler
- val body = purescala.TreeOps.matchToIfThenElse(lzy.body.getOrElse(throw CompilationException("Lazy field without body?")))
+ val body = lzy.body.getOrElse(throw CompilationException("Lazy field without body?"))
val initLabel = ch.getFreshLabel("isInitialized")
if (params.requireMonitor) {
@@ -1038,7 +1052,7 @@ trait CodeGeneration {
val body = field.body.getOrElse(throw CompilationException("No body for field?"))
val jvmType = typeToJVM(field.returnType)
- mkExpr(purescala.TreeOps.matchToIfThenElse(body), ch)(NoLocals(isStatic)) // FIXME Locals?
+ mkExpr(body, ch)(NoLocals(isStatic)) // FIXME Locals?
if (isStatic){
ch << PutStatic(className, name, jvmType)
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index da2c32b0f..e55f57777 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -280,8 +280,6 @@ class CompilationUnit(val ctx: LeonContext,
args.zipWithIndex.toMap
}
- val exprToCompile = purescala.TreeOps.matchToIfThenElse(e)
-
mkExpr(e, ch)(Locals(newMapping, Map.empty, Map.empty, true))
e.getType match {
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 85c686095..0ba220f7d 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1037,247 +1037,6 @@ object TreeOps {
genericTransform[Unit]((e,c) => (e, None), newPost, noCombiner)(())(expr)._1
}
- /*
- * Transforms complicated Ifs into multiple nested if blocks
- * It will decompose every OR clauses, and it will group AND clauses checking
- * isInstanceOf toghether.
- *
- * if (a.isInstanceof[T1] && a.tail.isInstanceof[T2] && a.head == a2 || C) {
- * T
- * } else {
- * E
- * }
- *
- * Becomes:
- *
- * if (a.isInstanceof[T1] && a.tail.isInstanceof[T2]) {
- * if (a.head == a2) {
- * T
- * } else {
- * if(C) {
- * T
- * } else {
- * E
- * }
- * }
- * } else {
- * if(C) {
- * T
- * } else {
- * E
- * }
- * }
- *
- * This transformation runs immediately before patternMatchReconstruction.
- *
- * Notes: positions are lost.
- */
- def decomposeIfs(e: Expr): Expr = {
- def pre(e: Expr): Expr = e match {
- case IfExpr(cond, thenn, elze) =>
- val TopLevelOrs(orcases) = cond
-
- if (orcases.exists{ case TopLevelAnds(ands) => ands.exists(_.isInstanceOf[CaseClassInstanceOf]) } ) {
- if (!orcases.tail.isEmpty) {
- pre(IfExpr(orcases.head, thenn, IfExpr(Or(orcases.tail), thenn, elze)))
- } else {
- val TopLevelAnds(andcases) = orcases.head
-
- val (andis, andnotis) = andcases.partition(_.isInstanceOf[CaseClassInstanceOf])
-
- if (andis.isEmpty || andnotis.isEmpty) {
- e
- } else {
- IfExpr(And(andis), IfExpr(And(andnotis), thenn, elze), elze)
- }
- }
- } else {
- e
- }
- case _ =>
- e
- }
-
- simplePreTransform(pre)(e)
- }
-
- /**
- * Reconstructs match expressions from if-then-elses.
- *
- * Notes: positions are lost.
- */
- def patternMatchReconstruction(e: Expr): Expr = {
- def post(e: Expr): Expr = e match {
- case IfExpr(cond, thenn, elze) =>
- val TopLevelAnds(cases) = cond
-
- if (cases.forall(_.isInstanceOf[CaseClassInstanceOf])) {
- // matchingOn might initially be: a : T1, a.tail : T2, b: T2
- def selectorDepth(e: Expr): Int = e match {
- case cd: CaseClassSelector =>
- 1+selectorDepth(cd.caseClass)
- case _ =>
- 0
- }
-
- var scrutSet = Set[Expr]()
- var conditions = Map[Expr, CaseClassType]()
-
- var matchingOn = cases.collect { case cc : CaseClassInstanceOf => cc } sortBy(cc => selectorDepth(cc.expr))
- for (CaseClassInstanceOf(cct, expr) <- matchingOn) {
- conditions += expr -> cct
-
- expr match {
- case cd: CaseClassSelector =>
- if (!scrutSet.contains(cd.caseClass)) {
- // we found a test looking like "a.foo.isInstanceof[..]"
- // without a check on "a".
- scrutSet += cd
- }
- case e =>
- scrutSet += e
- }
- }
-
- var substMap = Map[Expr, Expr]()
-
- def computePatternFor(ct: CaseClassType, prefix: Expr): Pattern = {
-
- val name = prefix match {
- case CaseClassSelector(_, _, id) => id.name
- case Variable(id) => id.name
- case _ => "tmp"
- }
-
- val binder = FreshIdentifier(name, true).setType(prefix.getType)
-
- // prefix becomes binder
- substMap += prefix -> Variable(binder)
- substMap += CaseClassInstanceOf(ct, prefix) -> BooleanLiteral(true)
-
- val subconds = for (f <- ct.fields) yield {
- val fieldSel = CaseClassSelector(ct, prefix, f.id)
- if (conditions contains fieldSel) {
- computePatternFor(conditions(fieldSel), fieldSel)
- } else {
- val b = FreshIdentifier(f.id.name, true).setType(f.tpe)
- substMap += fieldSel -> Variable(b)
- WildcardPattern(Some(b))
- }
- }
-
- CaseClassPattern(Some(binder), ct, subconds)
- }
-
- val (scrutinees, patterns) = scrutSet.toSeq.map(s => (s, computePatternFor(conditions(s), s))).unzip
-
- val (scrutinee, pattern) = if (scrutinees.size > 1) {
- (Tuple(scrutinees), TuplePattern(None, patterns))
- } else {
- (scrutinees.head, patterns.head)
- }
-
- // We use searchAndReplace to replace the biggest match first
- // (topdown).
- // So replaceing using Map(a => b, CC(a) => d) will replace
- // "CC(a)" by "d" and not by "CC(b)"
- val newThen = preMap(substMap.lift)(thenn)
-
- // Remove unused binders
- val vars = variablesOf(newThen)
-
- def simplerBinder(oid: Option[Identifier]) = oid.filter(vars(_))
-
- def simplifyPattern(p: Pattern): Pattern = p match {
- case CaseClassPattern(ob, cd, subpatterns) =>
- CaseClassPattern(simplerBinder(ob), cd, subpatterns map simplifyPattern)
- case WildcardPattern(ob) =>
- WildcardPattern(simplerBinder(ob))
- case TuplePattern(ob, patterns) =>
- TuplePattern(simplerBinder(ob), patterns map simplifyPattern)
- case LiteralPattern(ob,lit) => LiteralPattern(simplerBinder(ob), lit)
- case _ =>
- p
- }
-
- val resCases = List(
- SimpleCase(simplifyPattern(pattern), newThen),
- SimpleCase(WildcardPattern(None), elze)
- )
-
- def mergePattern(to: Pattern, anchor: Identifier, pat: Pattern): Pattern = to match {
- case CaseClassPattern(ob, cd, subs) =>
- if (ob == Some(anchor)) {
- sys.error("WOOOT: "+to+" <<= "+pat +" on "+anchor)
- pat
- } else {
- CaseClassPattern(ob, cd, subs.map(mergePattern(_, anchor, pat)))
- }
- case InstanceOfPattern(ob, cd) =>
- if (ob == Some(anchor)) {
- sys.error("WOOOT: "+to+" <<= "+pat +" on "+anchor)
- pat
- } else {
- InstanceOfPattern(ob, cd)
- }
-
- case WildcardPattern(ob) =>
- if (ob == Some(anchor)) {
- pat
- } else {
- WildcardPattern(ob)
- }
- case TuplePattern(ob,subs) =>
- if (ob == Some(anchor)) {
- sys.error("WOOOT: "+to+" <<= "+pat +" on "+anchor)
- pat
- } else {
- TuplePattern(ob, subs)
- }
- case LiteralPattern(ob, lit) => // TODO: is this correct?
- if (ob == Some(anchor)) {
- sys.error("WOOOT: "+to+" <<= "+pat +" on "+anchor)
- pat
- } else {
- LiteralPattern(ob,lit)
- }
-
- }
-
- val newCases = resCases.flatMap { c => c match {
- case SimpleCase(wp: WildcardPattern, m @ MatchExpr(ex, cases)) if ex == scrutinee =>
- cases
-
- case SimpleCase(pattern, m @ MatchExpr(v @ Variable(id), cases)) =>
- if (pattern.binders(id)) {
- cases.map{ nc =>
- SimpleCase(mergePattern(pattern, id, nc.pattern), nc.rhs)
- }
- } else {
- Seq(c)
- }
- case _ =>
- Seq(c)
- }}
-
- var finalMatch = MatchExpr(scrutinee, List(newCases.head)).setType(e.getType)
-
- for (toAdd <- newCases.tail if !isMatchExhaustive(finalMatch)) {
- finalMatch = MatchExpr(scrutinee, finalMatch.cases :+ toAdd).setType(e.getType)
- }
-
- finalMatch
-
- } else {
- e
- }
- case _ =>
- e
- }
-
- simplePostTransform(post)(e)
- }
-
/**
* Simplify If expressions when the branch is predetermined by the path
* condition
@@ -2283,5 +2042,249 @@ object TreeOps {
@deprecated("Use exists instead", "Leon 0.2.1")
def contains(e: Expr, matcher: Expr => Boolean): Boolean = exists(matcher)(e)
+
+ /*
+ * Transforms complicated Ifs into multiple nested if blocks
+ * It will decompose every OR clauses, and it will group AND clauses checking
+ * isInstanceOf toghether.
+ *
+ * if (a.isInstanceof[T1] && a.tail.isInstanceof[T2] && a.head == a2 || C) {
+ * T
+ * } else {
+ * E
+ * }
+ *
+ * Becomes:
+ *
+ * if (a.isInstanceof[T1] && a.tail.isInstanceof[T2]) {
+ * if (a.head == a2) {
+ * T
+ * } else {
+ * if(C) {
+ * T
+ * } else {
+ * E
+ * }
+ * }
+ * } else {
+ * if(C) {
+ * T
+ * } else {
+ * E
+ * }
+ * }
+ *
+ * This transformation runs immediately before patternMatchReconstruction.
+ *
+ * Notes: positions are lost.
+ */
+ @deprecated("Mending an expression after matchToIfThenElse is unsafe", "Leon 0.2.4")
+ def decomposeIfs(e: Expr): Expr = {
+ def pre(e: Expr): Expr = e match {
+ case IfExpr(cond, thenn, elze) =>
+ val TopLevelOrs(orcases) = cond
+
+ if (orcases.exists{ case TopLevelAnds(ands) => ands.exists(_.isInstanceOf[CaseClassInstanceOf]) } ) {
+ if (!orcases.tail.isEmpty) {
+ pre(IfExpr(orcases.head, thenn, IfExpr(Or(orcases.tail), thenn, elze)))
+ } else {
+ val TopLevelAnds(andcases) = orcases.head
+
+ val (andis, andnotis) = andcases.partition(_.isInstanceOf[CaseClassInstanceOf])
+
+ if (andis.isEmpty || andnotis.isEmpty) {
+ e
+ } else {
+ IfExpr(And(andis), IfExpr(And(andnotis), thenn, elze), elze)
+ }
+ }
+ } else {
+ e
+ }
+ case _ =>
+ e
+ }
+
+ simplePreTransform(pre)(e)
+ }
+
+ /**
+ * Reconstructs match expressions from if-then-elses.
+ *
+ * Notes: positions are lost.
+ */
+ @deprecated("Mending an expression after matchToIfThenElse is unsafe", "Leon 0.2.4")
+ def patternMatchReconstruction(e: Expr): Expr = {
+ def post(e: Expr): Expr = e match {
+ case IfExpr(cond, thenn, elze) =>
+ val TopLevelAnds(cases) = cond
+
+ if (cases.forall(_.isInstanceOf[CaseClassInstanceOf])) {
+ // matchingOn might initially be: a : T1, a.tail : T2, b: T2
+ def selectorDepth(e: Expr): Int = e match {
+ case cd: CaseClassSelector =>
+ 1+selectorDepth(cd.caseClass)
+ case _ =>
+ 0
+ }
+
+ var scrutSet = Set[Expr]()
+ var conditions = Map[Expr, CaseClassType]()
+
+ var matchingOn = cases.collect { case cc : CaseClassInstanceOf => cc } sortBy(cc => selectorDepth(cc.expr))
+ for (CaseClassInstanceOf(cct, expr) <- matchingOn) {
+ conditions += expr -> cct
+
+ expr match {
+ case cd: CaseClassSelector =>
+ if (!scrutSet.contains(cd.caseClass)) {
+ // we found a test looking like "a.foo.isInstanceof[..]"
+ // without a check on "a".
+ scrutSet += cd
+ }
+ case e =>
+ scrutSet += e
+ }
+ }
+
+ var substMap = Map[Expr, Expr]()
+
+ def computePatternFor(ct: CaseClassType, prefix: Expr): Pattern = {
+
+ val name = prefix match {
+ case CaseClassSelector(_, _, id) => id.name
+ case Variable(id) => id.name
+ case _ => "tmp"
+ }
+
+ val binder = FreshIdentifier(name, true).setType(prefix.getType)
+
+ // prefix becomes binder
+ substMap += prefix -> Variable(binder)
+ substMap += CaseClassInstanceOf(ct, prefix) -> BooleanLiteral(true)
+
+ val subconds = for (f <- ct.fields) yield {
+ val fieldSel = CaseClassSelector(ct, prefix, f.id)
+ if (conditions contains fieldSel) {
+ computePatternFor(conditions(fieldSel), fieldSel)
+ } else {
+ val b = FreshIdentifier(f.id.name, true).setType(f.tpe)
+ substMap += fieldSel -> Variable(b)
+ WildcardPattern(Some(b))
+ }
+ }
+
+ CaseClassPattern(Some(binder), ct, subconds)
+ }
+
+ val (scrutinees, patterns) = scrutSet.toSeq.map(s => (s, computePatternFor(conditions(s), s))).unzip
+
+ val (scrutinee, pattern) = if (scrutinees.size > 1) {
+ (Tuple(scrutinees), TuplePattern(None, patterns))
+ } else {
+ (scrutinees.head, patterns.head)
+ }
+
+ // We use searchAndReplace to replace the biggest match first
+ // (topdown).
+ // So replaceing using Map(a => b, CC(a) => d) will replace
+ // "CC(a)" by "d" and not by "CC(b)"
+ val newThen = preMap(substMap.lift)(thenn)
+
+ // Remove unused binders
+ val vars = variablesOf(newThen)
+
+ def simplerBinder(oid: Option[Identifier]) = oid.filter(vars(_))
+
+ def simplifyPattern(p: Pattern): Pattern = p match {
+ case CaseClassPattern(ob, cd, subpatterns) =>
+ CaseClassPattern(simplerBinder(ob), cd, subpatterns map simplifyPattern)
+ case WildcardPattern(ob) =>
+ WildcardPattern(simplerBinder(ob))
+ case TuplePattern(ob, patterns) =>
+ TuplePattern(simplerBinder(ob), patterns map simplifyPattern)
+ case LiteralPattern(ob,lit) => LiteralPattern(simplerBinder(ob), lit)
+ case _ =>
+ p
+ }
+
+ val resCases = List(
+ SimpleCase(simplifyPattern(pattern), newThen),
+ SimpleCase(WildcardPattern(None), elze)
+ )
+
+ def mergePattern(to: Pattern, anchor: Identifier, pat: Pattern): Pattern = to match {
+ case CaseClassPattern(ob, cd, subs) =>
+ if (ob == Some(anchor)) {
+ sys.error("WOOOT: "+to+" <<= "+pat +" on "+anchor)
+ pat
+ } else {
+ CaseClassPattern(ob, cd, subs.map(mergePattern(_, anchor, pat)))
+ }
+ case InstanceOfPattern(ob, cd) =>
+ if (ob == Some(anchor)) {
+ sys.error("WOOOT: "+to+" <<= "+pat +" on "+anchor)
+ pat
+ } else {
+ InstanceOfPattern(ob, cd)
+ }
+
+ case WildcardPattern(ob) =>
+ if (ob == Some(anchor)) {
+ pat
+ } else {
+ WildcardPattern(ob)
+ }
+ case TuplePattern(ob,subs) =>
+ if (ob == Some(anchor)) {
+ sys.error("WOOOT: "+to+" <<= "+pat +" on "+anchor)
+ pat
+ } else {
+ TuplePattern(ob, subs)
+ }
+ case LiteralPattern(ob, lit) => // TODO: is this correct?
+ if (ob == Some(anchor)) {
+ sys.error("WOOOT: "+to+" <<= "+pat +" on "+anchor)
+ pat
+ } else {
+ LiteralPattern(ob,lit)
+ }
+
+ }
+
+ val newCases = resCases.flatMap { c => c match {
+ case SimpleCase(wp: WildcardPattern, m @ MatchExpr(ex, cases)) if ex == scrutinee =>
+ cases
+
+ case SimpleCase(pattern, m @ MatchExpr(v @ Variable(id), cases)) =>
+ if (pattern.binders(id)) {
+ cases.map{ nc =>
+ SimpleCase(mergePattern(pattern, id, nc.pattern), nc.rhs)
+ }
+ } else {
+ Seq(c)
+ }
+ case _ =>
+ Seq(c)
+ }}
+
+ var finalMatch = MatchExpr(scrutinee, List(newCases.head)).setType(e.getType)
+
+ for (toAdd <- newCases.tail if !isMatchExhaustive(finalMatch)) {
+ finalMatch = MatchExpr(scrutinee, finalMatch.cases :+ toAdd).setType(e.getType)
+ }
+
+ finalMatch
+
+ } else {
+ e
+ }
+ case _ =>
+ e
+ }
+
+ simplePostTransform(post)(e)
+ }
+
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index c74c52839..17a586dbe 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -240,7 +240,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
val forArray = replace(substMap, simplerRes)
// We trust arrays to be fast...
- val eval = evaluator.compile(matchToIfThenElse(forArray), ba +: p.as)
+ val eval = evaluator.compile(forArray, ba +: p.as)
eval.map{e => { case (bss, ins) =>
e(FiniteArray(bss).setType(ArrayType(BooleanType)) +: ins)
@@ -248,7 +248,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
}
def compileWithArgs(): Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = {
- val eval = evaluator.compile(matchToIfThenElse(simplerRes), bssOrdered ++ p.as)
+ val eval = evaluator.compile(simplerRes, bssOrdered ++ p.as)
eval.map{e => { case (bss, ins) =>
e(bss ++ ins)
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
index 6849a97dc..cb57f3fd1 100644
--- a/src/main/scala/leon/utils/Simplifiers.scala
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -17,10 +17,7 @@ object Simplifiers {
removeWitnesses(p) _,
simplifyTautologies(uninterpretedZ3)(_),
simplifyLets _,
- decomposeIfs _,
- matchToIfThenElse _,
simplifyPaths(uninterpretedZ3)(_),
- patternMatchReconstruction _,
rewriteTuples _,
evalGround(ctx, p),
normalizeExpression _
@@ -46,10 +43,7 @@ object Simplifiers {
val simplifiers = List[Expr => Expr](
simplifyTautologies(uninterpretedZ3)(_),
simplifyLets _,
- decomposeIfs _,
- matchToIfThenElse _,
simplifyPaths(uninterpretedZ3)(_),
- patternMatchReconstruction _,
rewriteTuples _//,
//normalizeExpression _
)
@@ -68,7 +62,6 @@ object Simplifiers {
val simplifiers = List[Expr => Expr](
simplifyTautologies(uninterpretedZ3)(_),
- decomposeIfs _,
rewriteTuples _,
evalGround(ctx, p),
normalizeExpression _
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 71a8b8203..f3c607f6e 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -19,7 +19,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
(fd.postcondition, fd.body) match {
case (Some((id, post)), Some(body)) =>
val res = id.freshen
- val vc = Implies(precOrTrue(fd), Let(res, safe(body), replace(Map(id.toVariable -> res.toVariable), safe(post))))
+ val vc = Implies(precOrTrue(fd), Let(res, body, replace(Map(id.toVariable -> res.toVariable), post)))
Seq(new VerificationCondition(vc, fd, VCPostcondition, this).setPos(post))
case _ =>
@@ -32,11 +32,11 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
case Some(body) =>
val calls = collectWithPC {
case c @ FunctionInvocation(tfd, _) if tfd.hasPrecondition => (c, tfd.precondition.get)
- }(safe(body))
+ }(body)
calls.map {
case ((fi @ FunctionInvocation(tfd, args), pre), path) =>
- val pre2 = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, safe(pre))
+ val pre2 = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, pre)
val vc = Implies(And(precOrTrue(fd), path), pre2)
new VerificationCondition(vc, fd, VCPrecondition, this).setPos(fi)
@@ -70,7 +70,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
case a @ Assert(cond, None, _) => (a, VCAssert, cond)
// Only triggered for inner ensurings, general postconditions are handled by generatePostconditions
case a @ Ensuring(body, id, post) => (a, VCAssert, Let(id, body, post))
- }(safe(body))
+ }(body)
calls.map {
case ((e, kind, errorCond), path) =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 97804cb76..293efa58b 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -27,10 +27,10 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
}
override def generatePostconditions(fd: FunDef): Seq[VerificationCondition] = {
- (fd.body.map(safe), firstAbsClassDef(fd.params), fd.postcondition) match {
+ (fd.body, firstAbsClassDef(fd.params), fd.postcondition) match {
case (Some(b), Some((parentType, arg)), Some((id, p))) =>
- val post = safe(p)
- val body = safe(b)
+ val post = p
+ val body = b
for (cct <- parentType.knownCCDescendents) yield {
val selectors = selectorsOfParentType(parentType, cct, arg.toVariable)
@@ -56,12 +56,12 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
}
override def generatePreconditions(fd: FunDef): Seq[VerificationCondition] = {
- (fd.body.map(safe), firstAbsClassDef(fd.params)) match {
+ (fd.body, firstAbsClassDef(fd.params)) match {
case (Some(b), Some((parentType, arg))) =>
- val body = safe(b)
+ val body = b
val calls = collectWithPC {
- case fi @ FunctionInvocation(tfd, _) if tfd.hasPrecondition => (fi, safe(tfd.precondition.get))
+ case fi @ FunctionInvocation(tfd, _) if tfd.hasPrecondition => (fi, tfd.precondition.get)
}(body)
calls.flatMap {
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 7f4418023..26eef79c1 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -14,7 +14,9 @@ abstract class Tactic(vctx: VerificationContext) {
val program = vctx.program
val reporter = vctx.reporter
- def generateVCs(fd: FunDef): Seq[VerificationCondition] = {
+ def generateVCs(fdUnsafe: FunDef): Seq[VerificationCondition] = {
+ val fd = fdUnsafe.duplicate
+ fd.fullBody = matchToIfThenElse(fd.fullBody)
generatePostconditions(fd) ++
generatePreconditions(fd) ++
generateCorrectnessConditions(fd)
@@ -26,9 +28,8 @@ abstract class Tactic(vctx: VerificationContext) {
// Helper functions
- protected def safe(e: Expr): Expr = matchToIfThenElse(e)
protected def precOrTrue(fd: FunDef): Expr = fd.precondition match {
- case Some(pre) => safe(pre)
+ case Some(pre) => pre
case None => BooleanLiteral(true)
}
diff --git a/src/test/resources/regression/transformations/Match.scala b/src/test/resources/regression/transformations/Match.scala
deleted file mode 100644
index 2567ba2b3..000000000
--- a/src/test/resources/regression/transformations/Match.scala
+++ /dev/null
@@ -1,46 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
-import leon.lang._
-
-object Transform {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case object Nil extends List
-
- def input01(a: List): Int = a match {
- case Cons(h, Cons(th, tt)) =>
- h + th
- case _ =>
- a match {
- case Cons(th, Nil) =>
- th
- case _ =>
- 0
- }
- }
-
- def output01(a: List): Int = a match {
- case Cons(h, Cons(th, _)) =>
- h + th
- case Cons(th, Nil) =>
- th
- case _ =>
- 0
- }
- def input02(a: List): Int = a match {
- case Cons(h, t) =>
- t match {
- case Cons(th, tt) => 1
- case Nil => 2
- }
- case Nil =>
- 3
- }
-
- def output02(a: List): Int = a match {
- case Cons(_, Cons(_, _)) => 1
- case Cons(_, Nil) => 2
- case Nil => 3
- }
-}
diff --git a/src/test/scala/leon/test/purescala/TransformationTests.scala b/src/test/scala/leon/test/purescala/TransformationTests.scala
index 141259f61..7335365aa 100644
--- a/src/test/scala/leon/test/purescala/TransformationTests.scala
+++ b/src/test/scala/leon/test/purescala/TransformationTests.scala
@@ -40,11 +40,6 @@ class TransformationTests extends LeonTestSuite {
"Simplifying paths",
simpPaths
)
- case "Match.scala" =>
- (
- "Match reconstruction/flattening",
- apply (matchToIfThenElse _, patternMatchReconstruction _)
- )
case n =>
fail("Unknown name "+n)
}
--
GitLab