From 4553c205f50da90e3fc939d2f7c683f88764d98a Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 10 Feb 2014 11:15:36 +0100
Subject: [PATCH] Fix @induct creating incorrect type-parametric VCs.
Improve debugging capabilities of Pretty/Scala printer w.r.t. types
---
.../scala/leon/purescala/PrettyPrinter.scala | 16 ++++++----
.../scala/leon/purescala/PrinterOptions.scala | 1 +
.../scala/leon/purescala/ScalaPrinter.scala | 3 --
.../scala/leon/solvers/z3/FairZ3Solver.scala | 1 +
.../leon/verification/InductionTactic.scala | 29 +++++++------------
5 files changed, 23 insertions(+), 27 deletions(-)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index a5962a428..98345cba1 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -69,11 +69,15 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
}
case Variable(id) =>
- //sb.append("(")
- pp(id, p)
- //sb.append(": ")
- //pp(id.getType, p)
- //sb.append(")")
+ if (opts.printTypes) {
+ sb.append("(")
+ pp(id, p)
+ sb.append(": ")
+ pp(id.getType, p)
+ sb.append(")")
+ } else {
+ pp(id, p)
+ }
case LetTuple(bs,d,e) =>
sb.append("(let ")
@@ -483,7 +487,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
pp(tp, p)
case TypeParameter(id) =>
- sb.append(id.uniqueName)
+ pp(id, p)
case _ => sb.append("Tree? (" + tree.getClass + ")")
}
diff --git a/src/main/scala/leon/purescala/PrinterOptions.scala b/src/main/scala/leon/purescala/PrinterOptions.scala
index dc7b77aa2..597c15c68 100644
--- a/src/main/scala/leon/purescala/PrinterOptions.scala
+++ b/src/main/scala/leon/purescala/PrinterOptions.scala
@@ -3,5 +3,6 @@ package leon.purescala
case class PrinterOptions (
baseIndent: Int = 0,
printPositions: Boolean = false,
+ printTypes: Boolean = false,
printUniqueIds: Boolean = false
)
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 843e0905b..2347523cb 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -53,9 +53,6 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
var printPos = opts.printPositions
tree match {
- case Variable(id) =>
- pp(id, p)
-
case LetTuple(ids,d,e) =>
optBraces { implicit lvl =>
sb.append("val (" )
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index b3952e4fd..76f52585b 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -225,6 +225,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
// define an activating boolean...
val template = getTemplate(expr)
+
val z3args = for (vd <- template.tfd.args) yield {
variables.getZ3(Variable(vd.id)) match {
case Some(ast) =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 91b92d981..781db8ce1 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -13,16 +13,10 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
override val description = "Induction tactic for suitable functions"
override val shortDescription = "induction"
- private def firstAbsClassDef(args: Seq[VarDecl]) : Option[(AbstractClassDef, VarDecl)] = {
- val filtered = args.filter(arg =>
- arg.getType match {
- case AbstractClassType(_, _) => true
- case _ => false
- })
- if (filtered.size == 0) None else (filtered.head.getType match {
- case AbstractClassType(classDef, _) => Some((classDef, filtered.head))
- case _ => scala.sys.error("This should not happen.")
- })
+ private def firstAbsClassDef(args: Seq[VarDecl]) : Option[(AbstractClassType, VarDecl)] = {
+ args.map(vd => (vd.getType, vd)).collect {
+ case (act: AbstractClassType, vd) => (act, vd)
+ }.headOption
}
private def selectorsOfParentType(parentType: ClassType, cct: CaseClassType, expr: Expr) : Seq[Expr] = {
@@ -34,14 +28,13 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
override def generatePostconditions(funDef: FunDef) : Seq[VerificationCondition] = {
assert(funDef.body.isDefined)
- val defaultPost = super.generatePostconditions(funDef)
firstAbsClassDef(funDef.args) match {
- case Some((classDef, arg)) =>
+ case Some((cct, arg)) =>
val prec = funDef.precondition
val optPost = funDef.postcondition
val body = matchToIfThenElse(funDef.body.get)
val argAsVar = arg.toVariable
- val parentType = classDefToClassType(classDef)
+ val parentType = cct
optPost match {
case None =>
@@ -66,22 +59,22 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
})
Implies(And(inductiveHypothesis), withPrec)
}
- new VerificationCondition(Implies(CaseClassInstanceOf(cct, argAsVar), conditionForChild), funDef, VCKind.Postcondition, this)
+ new VerificationCondition(Implies(CaseClassInstanceOf(cct, argAsVar), conditionForChild), funDef, VCKind.Postcondition, this).setPos(funDef)
}
}
case None =>
- reporter.warning("Induction tactic currently supports exactly one argument of abstract class type")
- defaultPost
+ reporter.warning("Could not find abstract class type argument to induct on")
+ super.generatePostconditions(funDef)
}
}
override def generatePreconditions(function: FunDef) : Seq[VerificationCondition] = {
val defaultPrec = super.generatePreconditions(function)
firstAbsClassDef(function.args) match {
- case Some((classDef, arg)) => {
+ case Some((cct, arg)) => {
val toRet = if(function.hasBody) {
- val parentType = classDefToClassType(classDef)
+ val parentType = cct
val cleanBody = expandLets(matchToIfThenElse(function.body.get))
val allPathConds = collectWithPathCondition((t => t match {
--
GitLab