From 9e63efe639af396be6f6ac6fa925f1414b15a17e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 12 Aug 2015 15:15:10 +0200
Subject: [PATCH] Implement asInstanceOf
---
.../leon/test/evaluators/EvaluatorSuite.scala | 29 +++++++
.../leon/test/purescala/ExprOpsSuite.scala | 83 +++++++++++++++++++
.../scala/leon/codegen/CodeGeneration.scala | 7 ++
.../leon/evaluators/RecursiveEvaluator.scala | 8 ++
.../leon/frontends/scalac/ASTExtractors.scala | 7 ++
.../frontends/scalac/CodeExtraction.scala | 13 ++-
.../scala/leon/purescala/Constructors.scala | 9 ++
src/main/scala/leon/purescala/ExprOps.scala | 14 ++--
.../scala/leon/purescala/Expressions.scala | 9 ++
.../scala/leon/purescala/Extractors.scala | 6 +-
.../scala/leon/purescala/PrettyPrinter.scala | 1 +
src/main/scala/leon/purescala/TypeOps.scala | 3 +
.../solvers/combinators/UnrollingSolver.scala | 2 +-
.../leon/solvers/smtlib/SMTLIBSolver.scala | 3 +
.../solvers/templates/UnrollingBank.scala | 6 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 3 +
.../scala/leon/solvers/z3/FairZ3Solver.scala | 4 +-
src/main/scala/leon/synthesis/Rules.scala | 4 +-
.../synthesis/rules/EquivalentInputs.scala | 2 +-
.../leon/termination/SelfCallsProcessor.scala | 1 +
.../leon/verification/DefaultTactic.scala | 2 +
.../leon/verification/InjectAsserts.scala | 6 ++
.../verification/VerificationCondition.scala | 1 +
.../scala/leon/test/repair/RepairSuite.scala | 4 +-
.../leon/test/evaluators/EvaluatorSuite.scala | 1 -
25 files changed, 206 insertions(+), 22 deletions(-)
create mode 100644 src/integration/scala/leon/test/purescala/ExprOpsSuite.scala
diff --git a/src/integration/scala/leon/test/evaluators/EvaluatorSuite.scala b/src/integration/scala/leon/test/evaluators/EvaluatorSuite.scala
index 93f6139d8..dfc824f13 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 000000000..47ac7e4c0
--- /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 a3bcb5d14..28cbe5f3e 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 4c4340848..679da530c 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 2d6ec3191..a69f2712a 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 e96ad2d5f..9663fc89b 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 98379c079..b69554252 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 eda6e8d9d..0ff696f0a 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 a11e54229..312e9285c 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 f2c1d1804..7722c4e2a 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 b36b2e1cc..dde462e0c 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 005c877d0..05317ca8f 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 4b24f4a6e..5bb65cdb3 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 5a4450e58..b3365ba28 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 df1974f71..95a9e47ce 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 11cf31b27..550e84f05 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 c88a7677b..5a42c60c4 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 e9c3fdcae..1d2696772 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 4754f6bc5..c4acb5721 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 60ebe81ba..8b53f7cd1 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 11de3159c..2bcd2eb0b 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 2710b3994..3c3d89f48 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 cbec63027..312856790 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 a44e1352c..405058dea 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 7a6dce520..ffbd82e9b 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)
--
GitLab