From e009e46d9b4f534f1a0ede5fd93c39a483470ca9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Fri, 8 Jan 2016 16:55:27 +0100
Subject: [PATCH] Migrated the pretty printing code from
VerificationReport.scala to SelfPrettyPrinter.scala
---
.../leon/purescala/SelfPrettyPrinter.scala | 59 +++++++++++++++++++
.../verification/VerificationCondition.scala | 3 +-
.../verification/VerificationReport.scala | 51 +++-------------
3 files changed, 69 insertions(+), 44 deletions(-)
create mode 100644 src/main/scala/leon/purescala/SelfPrettyPrinter.scala
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
new file mode 100644
index 000000000..35e4d1f61
--- /dev/null
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -0,0 +1,59 @@
+package leon.purescala
+
+import leon.evaluators.StringTracingEvaluator
+import leon.purescala
+import purescala.Definitions.Program
+import leon.evaluators.StringTracingEvaluator
+import purescala.Expressions._
+import purescala.Types.StringType
+import leon.utils.DebugSectionSynthesis
+import leon.utils.DebugSectionVerification
+import leon.purescala.Quantification._
+import purescala.Constructors._
+import purescala.ExprOps._
+import purescala.Expressions.{Pattern, Expr}
+import purescala.Extractors._
+import purescala.TypeOps._
+import purescala.Types._
+import purescala.Common._
+import purescala.Expressions._
+import purescala.Definitions._
+import purescala.SelfPrettyPrinter
+import leon.solvers.{ HenkinModel, Model, SolverFactory }
+import leon.LeonContext
+import leon.evaluators
+
+/** This pretty-printer uses functions defined in Leon itself.
+ * If not pretty printing function is defined, return the default value instead
+ * @param The list of functions which should be excluded from pretty-printing (to avoid rendering counter-examples of toString methods using the method itself)
+ * @return a user defined string for the given typed expression. */
+object SelfPrettyPrinter {
+ def print(v: Expr, orElse: =>String, excluded: FunDef => Boolean = Set())(implicit ctx: LeonContext, program: Program): String = {
+ (program.definedFunctions find {
+ case fd if !excluded(fd) =>
+ fd.returnType == StringType && fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType) && fd.id.name.toLowerCase().endsWith("tostring") &&
+ program.callGraph.transitiveCallees(fd).forall { fde =>
+ !purescala.ExprOps.exists( _.isInstanceOf[Choose])(fde.fullBody)
+ }
+ }) match {
+ case Some(fd) =>
+ //println("Found fd: " + fd.id.name)
+ val ste = new StringTracingEvaluator(ctx, program)
+ try {
+ val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
+
+ result.result match {
+ case Some((StringLiteral(res), _)) if res != "" =>
+ res
+ case _ =>
+ orElse
+ }
+ } catch {
+ case e: evaluators.ContextualEvaluator#EvalError =>
+ orElse
+ }
+ case None =>
+ orElse
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 79fc62b45..e23c6fe92 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -10,6 +10,7 @@ import leon.utils.Positioned
import leon.evaluators.StringTracingEvaluator
import leon.solvers._
import leon.LeonContext
+import leon.purescala.SelfPrettyPrinter
/** This is just to hold some history information. */
case class VC(condition: Expr, fd: FunDef, kind: VCKind) extends Positioned {
@@ -63,7 +64,7 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
// is free to simplify
val strings = cex.toSeq.sortBy(_._1.name).map {
case (id, v) =>
- (id.asString(context), VerificationReport.userDefinedString(v, PrettyPrinter(v))(vctx.context, vctx.program))
+ (id.asString(context), SelfPrettyPrinter.print(v, PrettyPrinter(v))(vctx.context, vctx.program))
}
if (strings.nonEmpty) {
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 9ee17c76e..d695f4ca0 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -3,63 +3,28 @@
package leon
package verification
+import evaluators.StringTracingEvaluator
+import utils.DebugSectionSynthesis
+import utils.DebugSectionVerification
+import leon.purescala
import purescala.Definitions.Program
-import leon.evaluators.StringTracingEvaluator
import purescala.Expressions._
import purescala.Types.StringType
-import leon.utils.DebugSectionSynthesis
-import leon.utils.DebugSectionVerification
-import leon.purescala.TypeOps
-
-import leon.purescala.Quantification._
+import purescala.TypeOps
+import purescala.Quantification._
import purescala.Constructors._
import purescala.ExprOps._
-import purescala.Expressions.Pattern
+import purescala.Expressions.{Pattern, Expr}
import purescala.Extractors._
import purescala.TypeOps._
import purescala.Types._
import purescala.Common._
import purescala.Expressions._
import purescala.Definitions._
+import purescala.SelfPrettyPrinter
import leon.solvers.{ HenkinModel, Model, SolverFactory }
-object VerificationReport {
- /** If it can be computed, returns a user defined string for the given expression
- * @param The list of functions which should be excluded from pretty-printing (to avoid rendering counter-examples of toString methods using the method itself) */
- def userDefinedString(v: Expr, orElse: =>String, excluded: FunDef => Boolean = Set())(ctx: LeonContext, program: Program): String = {
- //println("Functions available:" + program.definedFunctions.map(fd => fd.id.name + "," + (fd.returnType == StringType) + ", " + (fd.params.length == 1) + "," + (fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType)) + ", " + (if(fd.params.length == 1) fd.params.head.getType + " == " + v.getType else "")).mkString("\n"))
- (program.definedFunctions find {
- case fd if !excluded(fd) =>
- fd.returnType == StringType && fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType) && fd.id.name.toLowerCase().endsWith("tostring") &&
- program.callGraph.transitiveCallees(fd).forall { fde =>
- !purescala.ExprOps.exists( _.isInstanceOf[Choose])(fde.fullBody)
- }
- }) match {
- case Some(fd) =>
- //println("Found fd: " + fd.id.name)
- val ste = new StringTracingEvaluator(ctx, program)
- try {
- val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
-
- result.result match {
- case Some((StringLiteral(res), _)) if res != "" =>
- res
- case _ =>
- orElse
- }
- } catch {
- case e: evaluators.ContextualEvaluator#EvalError =>
- orElse
- }
- case None =>
- //println("Function to render " + v + " not found")
- orElse
- }
- }
-}
-
case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) {
-
val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {
case (vc, or) => (vc, or.getOrElse(VCResult.unknown))
}
--
GitLab