From ce7276db21d005ac11a5dac15488bb79793164a9 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 8 Apr 2014 19:14:19 +0200
Subject: [PATCH] Make vanuatoo more resilient to non-patternable Exprs
---
src/main/scala/leon/datagen/DataGenerator.scala | 2 ++
src/main/scala/leon/datagen/VanuatooDataGen.scala | 7 +++++--
src/main/scala/leon/utils/DebugSections.scala | 4 +++-
.../scala/leon/verification/VerificationCondition.scala | 1 -
src/main/scala/leon/verification/VerificationReport.scala | 8 ++------
5 files changed, 12 insertions(+), 10 deletions(-)
diff --git a/src/main/scala/leon/datagen/DataGenerator.scala b/src/main/scala/leon/datagen/DataGenerator.scala
index 210385cd1..e97321053 100644
--- a/src/main/scala/leon/datagen/DataGenerator.scala
+++ b/src/main/scala/leon/datagen/DataGenerator.scala
@@ -10,6 +10,8 @@ import utils._
import java.util.concurrent.atomic.AtomicBoolean
trait DataGenerator extends Interruptible {
+ implicit val debugSection = DebugSectionDataGen
+
def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]];
protected val interrupted: AtomicBoolean = new AtomicBoolean(false)
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 87e1184bc..284a05009 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -109,6 +109,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
Nil
}
+ // Returns the pattern and whether it is fully precise
private def valueToPattern(v: AnyRef, expType: TypeTree): (VPattern[Expr, TypeTree], Boolean) = (v, expType) match {
case (i: Integer, Int32Type) =>
(cPattern(intConstructor(i), List()), true)
@@ -143,7 +144,8 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
(ConstructorPattern(c, elems.map(_._1)), elems.forall(_._2))
case _ =>
- sys.error("Could not retreive type for :"+cc.getClass.getName)
+ ctx.reporter.error("Could not retreive type for :"+cc.getClass.getName)
+ (AnyPattern[Expr, TypeTree](), false)
}
case (t: codegen.runtime.Tuple, tt @ TupleType(parts)) =>
@@ -165,7 +167,8 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
case (gv: GenericValue, t: TypeParameter) =>
(cPattern(getConstructors(t)(gv.id-1), List()), true)
case (v, t) =>
- sys.error("Unsupported value, can't paternify : "+v+" ("+v.getClass+") : "+t)
+ ctx.reporter.debug("Unsupported value, can't paternify : "+v+" ("+v.getClass+") : "+t)
+ (AnyPattern[Expr, TypeTree](), false)
}
type InstrumentedResult = (EvaluationResults.Result, Option[vanuatoo.Pattern[Expr, TypeTree]])
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index 394df76ca..902d3b4f6 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -16,6 +16,7 @@ case object DebugSectionVerification extends DebugSection("verification", 1 << 4
case object DebugSectionTermination extends DebugSection("termination", 1 << 5)
case object DebugSectionTrees extends DebugSection("trees", 1 << 6)
case object DebugSectionPositions extends DebugSection("positions", 1 << 7)
+case object DebugSectionDataGen extends DebugSection("datagen", 1 << 8)
object DebugSections {
val all = Set[DebugSection](
@@ -26,6 +27,7 @@ object DebugSections {
DebugSectionVerification,
DebugSectionTermination,
DebugSectionTrees,
- DebugSectionPositions
+ DebugSectionPositions,
+ DebugSectionDataGen
)
}
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 204f498b4..4a23e63e1 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -35,7 +35,6 @@ class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: V
case Some(s) => s.name
case None => ""
}
-
}
object VCKind extends Enumeration {
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 9827c72bd..01b129d77 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -6,12 +6,8 @@ package verification
import purescala.Definitions.FunDef
class VerificationReport(val fvcs: Map[FunDef, List[VerificationCondition]]) {
- val conditions : Seq[VerificationCondition] = fvcs.flatMap(_._2).toSeq.sortWith {
- (vc1,vc2) =>
- val id1 = vc1.funDef.id.name
- val id2 = vc2.funDef.id.name
- if(id1 != id2) id1 < id2 else vc1.getPos < vc2.getPos
- }
+ import scala.math.Ordering.Implicits._
+ val conditions : Seq[VerificationCondition] = fvcs.flatMap(_._2).toSeq.sortBy(vc => (vc.funDef.id.name, vc.kind))
lazy val totalConditions : Int = conditions.size
--
GitLab