diff --git a/src/integration/scala/leon/test/evaluators/EvaluatorSuite.scala b/src/integration/scala/leon/test/evaluators/EvaluatorSuite.scala
index 93f6139d828622bdbdc396e3baa5a2c9bce1c9b3..dfc824f132602c3bd7492fe3c67a26defb3c3a7c 100644
--- a/src/integration/scala/leon/test/evaluators/EvaluatorSuite.scala
+++ b/src/integration/scala/leon/test/evaluators/EvaluatorSuite.scala
@@ -191,6 +191,21 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDS
| }
| def f2 = D().isInstanceOf[B]
| def f3 = C(42).isInstanceOf[A]
+ |}""".stripMargin,
+
+ """object Casts1 {
+ | abstract class Foo
+ | case class Bar1(v: BigInt) extends Foo
+ | case class Bar2(v: BigInt) extends Foo
+ | case class Bar3(v: BigInt) extends Foo
+ |
+ | def test(a: Foo): BigInt = {
+ | if (a.isInstanceOf[Bar1]) {
+ | a.asInstanceOf[Bar1].v
+ | } else {
+ | a.asInstanceOf[Bar2].v
+ | }
+ | }
|}""".stripMargin
)
@@ -363,6 +378,20 @@ class EvaluatorSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDS
}
}
+ test("Casts1") { implicit fix =>
+ def bar1(es: Expr*) = cc("Casts1.Bar1")(es: _*)
+ def bar2(es: Expr*) = cc("Casts1.Bar2")(es: _*)
+ def bar3(es: Expr*) = cc("Casts1.Bar3")(es: _*)
+
+ val b42 = bi(42)
+
+ for(e <- allEvaluators) {
+ eval(e, fcall("Casts1.test")(bar1(b42))) === b42
+ eval(e, fcall("Casts1.test")(bar2(b42))) === b42
+ eval(e, fcall("Casts1.test")(bar3(b42))).failed
+ }
+ }
+
abstract class EvalDSL {
def res: Expr
def ===(res: Expr): Unit
diff --git a/src/integration/scala/leon/test/purescala/ExprOpsSuite.scala b/src/integration/scala/leon/test/purescala/ExprOpsSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..47ac7e4c0299a365028cc71e83f4e18bb585f470
--- /dev/null
+++ b/src/integration/scala/leon/test/purescala/ExprOpsSuite.scala
@@ -0,0 +1,83 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.test.purescala
+
+import leon.test._
+
+import leon._
+import leon.purescala.Constructors._
+import leon.purescala.Definitions._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.DefOps._
+import leon.purescala.Common._
+import leon.utils._
+
+class ExprOpsSuite extends LeonTestSuiteWithProgram with helpers.ExpressionsDSL {
+
+ val sources = List(
+ """object Casts1 {
+ | abstract class Foo
+ | case class Bar1(v: BigInt) extends Foo
+ | case class Bar2(v: BigInt) extends Foo
+ | case class Bar3(v: BigInt) extends Foo
+ | case class Bar4(i: Foo) extends Foo
+ |
+ | def aMatch(a: Foo) = a match {
+ | case b1 @ Bar4(b2: Bar3) => b2
+ | }
+ |}""".stripMargin
+ )
+
+ test("mapForPattern introduces casts"){ implicit fix =>
+ funDef("Casts1.aMatch").body match {
+ case Some(MatchExpr(scrut, Seq(MatchCase(p, None, b)))) =>
+ val m = mapForPattern(scrut, p)
+ val bar4 = caseClassDef("Casts1.Bar4").typed
+ val i = caseClassDef("Casts1.Bar4").fields.head.id
+
+ for ((id, v) <- mapForPattern(scrut, p)) {
+ if (id.name == "b1") {
+ assert(v === AsInstanceOf(scrut, bar4))
+ } else if (id.name == "b2") {
+ assert(v === CaseClassSelector(bar4, AsInstanceOf(scrut, bar4), i))
+ } else {
+ fail("Map contained unknown entry "+id.asString)
+ }
+ }
+
+ case b =>
+ fail("unexpected test shape: "+b)
+ }
+ }
+
+ test("matchToIfThenElse introduces casts"){ implicit fix =>
+ funDef("Casts1.aMatch").body match {
+ case Some(b) =>
+ assert(exists {
+ case AsInstanceOf(_, _) => true
+ case _ => false
+ }(matchToIfThenElse(b)), "Could not find AsInstanceOf in the result of matchToIfThenElse")
+
+ case b =>
+ fail("unexpected test shape: "+b)
+ }
+ }
+
+ test("asInstOf simplifies trivial casts") { implicit fix =>
+ val cct = caseClassDef("Casts1.Bar1").typed
+ val cc = CaseClass(cct, Seq(bi(42)))
+ assert(asInstOf(cc, cct) === cc)
+ }
+
+ test("asInstOf leaves unknown casts") { implicit fix =>
+ val act = classDef("Casts1.Foo").typed
+ val cct = caseClassDef("Casts1.Bar1").typed
+
+ val cc = CaseClass(cct, Seq(bi(42)))
+ val id = FreshIdentifier("tmp", act)
+ val expr = Let(id, cc, id.toVariable)
+
+ assert(asInstOf(expr, cct) === AsInstanceOf(expr, cct))
+ }
+}
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index a3bcb5d1478fbe922b5be02934659ff019dcf2b8..28cbe5f3ef3ca6e2a13eacf4356c17db360f0e2b 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -279,6 +279,13 @@ trait CodeGeneration {
mkExpr(e, ch)
ch << InstanceOf(ccName)
+ case AsInstanceOf(e, cct) =>
+ val (ccName, _) = leonClassToJVMInfo(cct.classDef).getOrElse {
+ throw CompilationException("Unknown class : " + cct.id)
+ }
+ mkExpr(e, ch)
+ ch << CheckCast(ccName)
+
case CaseClassSelector(cct, e, sid) =>
mkExpr(e, ch)
val (ccName, _) = leonClassToJVMInfo(cct.classDef).getOrElse {
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 4c43408486d8af3b2c1b5022c6f3b179276226f2..679da530c486e308c22c77b97efc19ee2d4d6229 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -223,6 +223,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case CaseClass(cd, args) =>
CaseClass(cd, args.map(e))
+ case AsInstanceOf(expr, ct) =>
+ val le = e(expr)
+ if (isSubtypeOf(le.getType, ct)) {
+ le
+ } else {
+ throw RuntimeError("Cast error: cannot cast "+le.asString+" to "+ct.asString)
+ }
+
case IsInstanceOf(ct, expr) =>
val le = e(expr)
BooleanLiteral(isSubtypeOf(le.getType, ct))
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 2d6ec3191621cf54fe251effe8ac1033b6703ff1..a69f2712afce817e4fdb71ad5a839900b6d4f717 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -890,6 +890,13 @@ trait ASTExtractors {
}
}
+ object ExAsInstanceOf {
+ def unapply(tree: TypeApply) : Option[(Tree, Tree)] = tree match {
+ case TypeApply(Select(t, isInstanceOfName), typeTree :: Nil) if isInstanceOfName.toString == "asInstanceOf" => Some((t, typeTree))
+ case _ => None
+ }
+ }
+
object ExIsInstanceOf {
def unapply(tree: TypeApply) : Option[(Tree, Tree)] = tree match {
case TypeApply(Select(t, isInstanceOfName), typeTree :: Nil) if isInstanceOfName.toString == "isInstanceOf" => Some((typeTree, t))
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index e96ad2d5f013dc2737d4d61939aa1075c18e55a5..9663fc89b5781d64594f758f8c90f25fe88efb25 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1392,7 +1392,17 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(tr, "Both branches of ifthenelse have incompatible types ("+r2.getType.asString(ctx)+" and "+r3.getType.asString(ctx)+")")
}
- case ExIsInstanceOf(tt, cc) => {
+ case ExAsInstanceOf(expr, tt) =>
+ val eRec = extractTree(expr)
+ val checkType = extractType(tt)
+ checkType match {
+ case ct: ClassType =>
+ AsInstanceOf(eRec, ct)
+ case _ =>
+ outOfSubsetError(tr, "asInstanceOf can only cast to class types")
+ }
+
+ case ExIsInstanceOf(tt, cc) =>
val ccRec = extractTree(cc)
val checkType = extractType(tt)
checkType match {
@@ -1413,7 +1423,6 @@ trait CodeExtraction extends ASTExtractors {
case _ =>
outOfSubsetError(tr, "isInstanceOf can only be used with a class")
}
- }
case pm @ ExPatternMatching(sel, cses) =>
val rs = extractTree(sel)
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 98379c079f8bc36e6aa8b6f89c1e774995c9cfc2..b69554252f7e6ccbb26e37d2fa9900c7b1c4893f 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -381,4 +381,13 @@ object Constructors {
case (IsTyped(_, RealType), IsTyped(_, RealType)) => RealTimes(lhs, rhs)
}
+ /** $encodingof expr.asInstanceOf[tpe], returns `expr` it it already is of type `tpe`. */
+ def asInstOf(expr: Expr, tpe: ClassType) = {
+ if (isSubtypeOf(expr.getType, tpe)) {
+ expr
+ } else {
+ AsInstanceOf(expr, tpe)
+ }
+ }
+
}
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index eda6e8d9de4d710a1ccb9742d9296229955e5447..0ff696f0a6c28d27767497f04d5dcfaa71c1cadf 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -805,17 +805,17 @@ object ExprOps {
/** Converts the pattern applied to an input to a map between identifiers and expressions */
def mapForPattern(in: Expr, pattern: Pattern) : Map[Identifier,Expr] = {
- def bindIn(id: Option[Identifier]): Map[Identifier,Expr] = id match {
+ def bindIn(id: Option[Identifier], cast: Option[ClassType] = None): Map[Identifier,Expr] = id match {
case None => Map()
- case Some(id) => Map(id -> in)
+ case Some(id) => Map(id -> cast.map(asInstOf(in, _)).getOrElse(in))
}
pattern match {
- case CaseClassPattern(b, ccd, subps) =>
- assert(ccd.fields.size == subps.size)
- val pairs = ccd.fields.map(_.id).toList zip subps.toList
- val subMaps = pairs.map(p => mapForPattern(caseClassSelector(ccd, in, p._1), p._2))
+ case CaseClassPattern(b, cct, subps) =>
+ assert(cct.fields.size == subps.size)
+ val pairs = cct.fields.map(_.id).toList zip subps.toList
+ val subMaps = pairs.map(p => mapForPattern(caseClassSelector(cct, asInstOf(in, cct), p._1), p._2))
val together = subMaps.flatten.toMap
- bindIn(b) ++ together
+ bindIn(b, Some(cct)) ++ together
case TuplePattern(b, subps) =>
val TupleType(tpes) = in.getType
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index a11e542297b0fe6a4745966f41cc755755c966cd..312e9285c08076ab16bbf5c8f18ed3d56741f89f 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -404,6 +404,15 @@ object Expressions {
val getType = BooleanType
}
+ /**
+ * $encodingof `.asInstanceOf[...]`
+ * Introduced by matchToIfThenElse to transform match-cases to type-correct
+ * if bodies.
+ */
+ case class AsInstanceOf(expr: Expr, tpe: ClassType) extends Expr {
+ val getType = tpe
+ }
+
/** $encodingof `value.selector` where value is of a case class type
*
* If you are not sure about the requirement you should use
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index f2c1d1804ceb77306a6b85ee5c27e09e202903ad..7722c4e2aaf0f2228c128b83b7640290082eeea5 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -31,8 +31,10 @@ object Extractors {
Some((Seq(t), (es: Seq[Expr]) => SetCardinality(es.head)))
case CaseClassSelector(cd, e, sel) =>
Some((Seq(e), (es: Seq[Expr]) => caseClassSelector(cd, es.head, sel)))
- case IsInstanceOf(cd, e) =>
- Some((Seq(e), (es: Seq[Expr]) => IsInstanceOf(cd, es.head)))
+ case IsInstanceOf(ct, e) =>
+ Some((Seq(e), (es: Seq[Expr]) => IsInstanceOf(ct, es.head)))
+ case AsInstanceOf(e, ct) =>
+ Some((Seq(e), (es: Seq[Expr]) => asInstOf(es.head, ct)))
case TupleSelect(t, i) =>
Some((Seq(t), (es: Seq[Expr]) => TupleSelect(es.head, i)))
case ArrayLength(a) =>
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b36b2e1cca7dba821975e1ae4dd3e0b9ccef4208..dde462e0cc81518779dc5bb2bfbf893e7489540f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -176,6 +176,7 @@ class PrettyPrinter(opts: PrinterOptions,
case NoTree(tpe) => p"???[$tpe]"
case Choose(pred) => p"choose($pred)"
case e @ Error(tpe, err) => p"""error[$tpe]("$err")"""
+ case AsInstanceOf(e, ct) => p"""$e.asInstanceOf[$ct]"""
case IsInstanceOf(cct, e) =>
if (cct.classDef.isCaseObject) {
p"($e == $cct)"
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 005c877d0e207e503b526ed65166f6f557d68c69..05317ca8ff1dfd9fe985187eaab489694129e3a3 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -295,6 +295,9 @@ object TypeOps {
case cc @ IsInstanceOf(ct, e) =>
IsInstanceOf(tpeSub(ct).asInstanceOf[ClassType], srec(e)).copiedFrom(cc)
+ case cc @ AsInstanceOf(e, ct) =>
+ AsInstanceOf(srec(e), tpeSub(ct).asInstanceOf[ClassType]).copiedFrom(cc)
+
case l @ Let(id, value, body) =>
val newId = freshId(id, tpeSub(id.getType))
Let(newId, srec(value), rec(idsMap + (id -> newId))(body)).copiedFrom(l)
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 4b24f4a6e87fd1092788e7cb782f76c7c032f6d5..5bb65cdb3757eb07ebad63e86162dc492cc8ba70 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -65,7 +65,7 @@ class UnrollingSolver(val context: LeonContext, program: Program, underlying: In
def mkImplies(l: Expr, r: Expr) = implies(l, r)
}, assumePreHolds)
- val unrollingBank = new UnrollingBank(reporter, templateGenerator)
+ val unrollingBank = new UnrollingBank(context, templateGenerator)
val solver = underlying
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 5a4450e58161e91d24f6f6c98ab966274e18cb96..b3365ba2835e0232dcb57545b5ba85b87cdd2d5d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -339,6 +339,9 @@ abstract class SMTLIBSolver(val context: LeonContext,
val selector = selectors.toB((cct, s.selectorIndex))
FunctionApplication(selector, Seq(toSMT(e)))
+ case AsInstanceOf(expr, cct) =>
+ toSMT(expr)
+
case IsInstanceOf(cct, e) =>
declareSort(cct)
val cases = cct match {
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index df1974f715acafe132af48ff8861b31d0dfae79e..95a9e47cec1e606fbd6ca0b399f777779db86cf2 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -9,8 +9,10 @@ import purescala.Expressions._
import purescala.Types._
import utils._
-class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[T]) extends IncrementalState {
+class UnrollingBank[T](ctx: LeonContext, templateGenerator: TemplateGenerator[T]) extends IncrementalState {
implicit val debugSection = utils.DebugSectionSolver
+ implicit val ctx0 = ctx
+ val reporter = ctx.reporter
private val encoder = templateGenerator.encoder
@@ -190,7 +192,7 @@ class UnrollingBank[T](reporter: Reporter, templateGenerator: TemplateGenerator[
// ...so we must force it to true!
val clauses = template.start +: (newClauses ++ blockClauses)
- reporter.debug("Generating clauses for: " + expr)
+ reporter.debug("Generating clauses for: " + expr.asString)
for (cls <- clauses) {
reporter.debug(" . " + cls)
}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 11cf31b270539dddbf6970ce6fd73e9abf5b4c32..550e84f057f6c5d49f139325a5bbdfaf74ac29f4 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -480,6 +480,9 @@ trait AbstractZ3Solver
val selector = selectors.toB(cct, c.selectorIndex)
selector(rec(cc))
+ case AsInstanceOf(expr, ct) =>
+ rec(expr)
+
case IsInstanceOf(act: AbstractClassType, e) =>
act.knownCCDescendants match {
case Seq(cct) =>
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index c88a7677b1b05c2715bbbcd660ce370a0a09f6dc..5a42c60c49629056b65e560e4bffe37be0b3c2f2 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -20,7 +20,7 @@ import evaluators._
import termination._
-class FairZ3Solver(val context : LeonContext, val program: Program)
+class FairZ3Solver(val context: LeonContext, val program: Program)
extends AbstractZ3Solver
with Z3ModelReconstruction
with FairZ3Component {
@@ -154,7 +154,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program)
private var constraints = new IncrementalSeq[Expr]()
- val unrollingBank = new UnrollingBank(reporter, templateGenerator)
+ val unrollingBank = new UnrollingBank(context, templateGenerator)
def push() {
errors.push()
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index e9c3fdcae0714aa79a4b9d7ff0b86b6e6fc3be2e..1d2696772e9cd3dd150f7b933f59c47e55164ec9 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -173,9 +173,9 @@ trait RuleDSL {
}
def solve(sol: Solution)
- (implicit problem: Problem): RuleInstantiation = {
+ (implicit problem: Problem, ctx: LeonContext): RuleInstantiation = {
- new RuleInstantiation(s"Solve: $sol",
+ new RuleInstantiation(s"Solve: ${sol.asString}",
SolutionBuilderCloser(Some(sol))) {
def apply(hctx: SearchContext) = RuleClosed(sol)
}
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 4754f6bc560abf0a05d927e73be7561223ef416d..c4acb572176b2ccc9868013c2aefc4f11cf11703 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -29,6 +29,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
clauses.find {
case Equals(e, CaseClassSelector(`cct`, `s`, `id`)) => true
+ case Equals(e, CaseClassSelector(`cct`, AsInstanceOf(`s`, `cct`), `id`)) => true
case _ => false
} match {
case Some(Equals(e, _)) =>
@@ -39,7 +40,6 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
}).flatten
-
if (fieldsVals.size == cct.fields.size) {
Some((s, CaseClass(cct, fieldsVals)))
} else {
diff --git a/src/main/scala/leon/termination/SelfCallsProcessor.scala b/src/main/scala/leon/termination/SelfCallsProcessor.scala
index 60ebe81babe2a95c2924478ec225acc2d0f699a2..8b53f7cd166c8adeb52e9a2c9f3107cf6fd26936 100644
--- a/src/main/scala/leon/termination/SelfCallsProcessor.scala
+++ b/src/main/scala/leon/termination/SelfCallsProcessor.scala
@@ -54,6 +54,7 @@ class SelfCallsProcessor(val checker: TerminationChecker) extends Processor {
case Equals(lhs: Expr, rhs: Expr) => rec(lhs) || rec(rhs)
case CaseClass(ct, args: Seq[Expr]) => args.exists(arg => rec(arg))
case IsInstanceOf(ct, expr: Expr) => rec(expr)
+ case AsInstanceOf(expr: Expr, ct) => rec(expr)
case CaseClassSelector(ct, caseClassExpr, selector) => rec(caseClassExpr)
case Plus(lhs: Expr, rhs: Expr) => rec(lhs) || rec(rhs)
case Minus(lhs: Expr, rhs: Expr) => rec(lhs) || rec(rhs)
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 11de3159cd10ce55bf2975bab5e425eb0c7bb24f..2bcd2eb0b6aba3f7d8c52fc2999d25b4befd8e19 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -64,6 +64,8 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
VCKinds.ModuloByZero
} else if (err.startsWith("Remainder ")) {
VCKinds.RemainderByZero
+ } else if (err.startsWith("Cast ")) {
+ VCKinds.CastError
} else {
VCKinds.Assert
}
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 2710b399445de20145770a14bfcd47b364143c4b..3c3d89f4859449195584c1bd28460da956ab37fb 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -35,6 +35,12 @@ object InjectAsserts extends LeonPhase[Program, Program] {
case e @ MapGet(m,k) =>
Some(Assert(MapIsDefinedAt(m, k), Some("Map undefined at this index"), e).setPos(e))
+ case e @ AsInstanceOf(expr, ct) =>
+ Some(Assert(IsInstanceOf(ct, expr),
+ Some("Cast error"),
+ e
+ ).setPos(e))
+
case e @ Division(_, d) =>
Some(Assert(Not(Equals(d, InfiniteIntegerLiteral(0))),
Some("Division by zero"),
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index cbec6302779a93f16c7518f3279f1976de83206d..3128567904b2e21165ff6ba8a35759114af5313e 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -37,6 +37,7 @@ object VCKinds {
case object DivisionByZero extends VCKind("division by zero", "div 0")
case object ModuloByZero extends VCKind("modulo by zero", "mod 0")
case object RemainderByZero extends VCKind("remainder by zero", "rem 0")
+ case object CastError extends VCKind("cast correctness", "cast")
}
case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option[Long]) {
diff --git a/src/regression/scala/leon/test/repair/RepairSuite.scala b/src/regression/scala/leon/test/repair/RepairSuite.scala
index a44e1352ca4b5cffc6fc74f285cba991aa11016c..405058dea72e43d63f8e31f8e41d60a972a84108 100644
--- a/src/regression/scala/leon/test/repair/RepairSuite.scala
+++ b/src/regression/scala/leon/test/repair/RepairSuite.scala
@@ -32,14 +32,14 @@ class RepairSuite extends LeonTestSuite {
interruptManager = new InterruptManager(reporter),
options = Seq(
LeonOption(SharedOptions.optFunctions)(Seq(fileToFun(name))),
- LeonOption(SharedOptions.optTimeout)(10L)
+ LeonOption(SharedOptions.optTimeout)(20L)
)
)
test(name) {
pipeline.run(ctx)(List(path))
if(reporter.errorCount > 0) {
- fail("Errors during repair!")
+ fail("Errors during repair:\n"+reporter.lastErrors.mkString("\n"))
}
}
}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorSuite.scala b/src/test/scala/leon/test/evaluators/EvaluatorSuite.scala
index 7a6dce5209f5f98e3c496e4a2c2c497c7767045b..ffbd82e9b716869454456e361a26cc5570bd5b58 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorSuite.scala
@@ -225,7 +225,6 @@ class EvaluatorSuite extends LeonTestSuite with helpers.ExpressionsDSL {
}
}
-
def eqArray(a1: Expr, a2: Expr) = (a1, a2) match {
case (FiniteArray(es1, d1, IntLiteral(l1)), FiniteArray(es2, d2, IntLiteral(l2))) =>
assert(l1 === l2)