From 63477d6cc365eb0b2f6d56970e66841f7ea74152 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Tue, 19 Mar 2013 17:12:17 +0100
Subject: [PATCH] Correct handling of choose in verification.
- Choose expressions becomes uninterpreted functions under the same
constraints.
- Fix bug with variablesOf considering choose binders as free.
- Silence evaluator errors when occuring with tentative lucky models.
Note that choose expressions cannot be evaluated nor compiled.
---
src/main/scala/leon/purescala/TreeOps.scala | 1 +
.../scala/leon/solvers/z3/FairZ3Solver.scala | 12 ++++--
.../leon/solvers/z3/FunctionTemplate.scala | 13 ++++++-
.../purescala/invalid/Choose1.scala | 39 +++++++++++++++++++
.../purescala/valid/Choose1.scala | 39 +++++++++++++++++++
5 files changed, 99 insertions(+), 5 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/Choose1.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/Choose1.scala
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 8ec32c5d8..b70e88998 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -361,6 +361,7 @@ object TreeOps {
def combine(s1: Set[Identifier], s2: Set[Identifier]) = s1 ++ s2
def compute(t: Expr, s: Set[Identifier]) = t match {
case Let(i,_,_) => s -- Set(i)
+ case Choose(is,_) => s -- is
case MatchExpr(_, cses) => s -- (cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b))
case _ => s
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 59da55025..f736bf1fb 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -139,7 +139,7 @@ class FairZ3Solver(context : LeonContext)
(solver.checkAssumptions(assumptions), solver.getModel, solver.getUnsatCore)
}
- private def validateModel(model: Z3Model, formula: Expr, variables: Set[Identifier]) : (Boolean, Map[Identifier,Expr]) = {
+ private def validateModel(model: Z3Model, formula: Expr, variables: Set[Identifier], silenceErrors: Boolean) : (Boolean, Map[Identifier,Expr]) = {
if(!forceStop) {
val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
@@ -185,7 +185,11 @@ class FairZ3Solver(context : LeonContext)
(false, asMap)
case EvaluationResults.EvaluatorError(msg) =>
- reporter.warning("Something went wrong. While evaluating the model, we got this : " + msg)
+ if (silenceErrors) {
+ reporter.info("- Model leads to evaluator error: " + msg)
+ } else {
+ reporter.warning("Something went wrong. While evaluating the model, we got this : " + msg)
+ }
(false, asMap)
}
@@ -502,7 +506,7 @@ class FairZ3Solver(context : LeonContext)
val z3model = solver.getModel
if (this.checkModels) {
- val (isValid, model) = validateModel(z3model, entireFormula, varsInVC)
+ val (isValid, model) = validateModel(z3model, entireFormula, varsInVC, silenceErrors = false)
if (isValid) {
foundAnswer(Some(true), model)
@@ -588,7 +592,7 @@ class FairZ3Solver(context : LeonContext)
if (this.feelingLucky && !forceStop) {
// we might have been lucky :D
luckyTime.start
- val (wereWeLucky, cleanModel) = validateModel(solver.getModel, entireFormula, varsInVC)
+ val (wereWeLucky, cleanModel) = validateModel(solver.getModel, entireFormula, varsInVC, silenceErrors = true)
luckyTime.stop
if(wereWeLucky) {
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index 44963afa4..1c8ca1294 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -272,7 +272,18 @@ object FunctionTemplate {
}
}
- case c @ Choose(_, _) => Variable(FreshIdentifier("choose", true).setType(c.getType))
+ case c @ Choose(ids, cond) =>
+ val cid = FreshIdentifier("choose", true).setType(c.getType)
+ exprVars += cid
+
+ val m: Map[Expr, Expr] = if (ids.size == 1) {
+ Map(Variable(ids.head) -> Variable(cid))
+ } else {
+ ids.zipWithIndex.map{ case (id, i) => Variable(id) -> TupleSelect(Variable(cid), i+1) }.toMap
+ }
+
+ storeGuarded(pathVar, replace(m, cond))
+ Variable(cid)
case n @ NAryOperator(as, r) => r(as.map(a => rec(pathVar, a))).setType(n.getType)
case b @ BinaryOperator(a1, a2, r) => r(rec(pathVar, a1), rec(pathVar, a2)).setType(b.getType)
diff --git a/src/test/resources/regression/verification/purescala/invalid/Choose1.scala b/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
new file mode 100644
index 000000000..a0ac78daf
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
@@ -0,0 +1,39 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Choose1 {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def listOfSize(i: Int): List = {
+ require(i >= 0)
+
+ if (i == 0) {
+ Nil()
+ } else {
+ choose { (res: List) => size(res) == i-1 }
+ }
+ } ensuring ( size(_) == i )
+
+
+ def listOfSize2(i: Int): List = {
+ require(i >= 0)
+
+ if (i > 0) {
+ Cons(0, listOfSize(i-1))
+ } else {
+ Nil()
+ }
+ } ensuring ( size(_) == i )
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Choose1.scala b/src/test/resources/regression/verification/purescala/valid/Choose1.scala
new file mode 100644
index 000000000..620b87811
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Choose1.scala
@@ -0,0 +1,39 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Choose1 {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def listOfSize(i: Int): List = {
+ require(i >= 0)
+
+ if (i == 0) {
+ Nil()
+ } else {
+ choose { (res: List) => size(res) == i }
+ }
+ } ensuring ( size(_) == i )
+
+
+ def listOfSize2(i: Int): List = {
+ require(i >= 0)
+
+ if (i > 0) {
+ Cons(0, listOfSize(i-1))
+ } else {
+ Nil()
+ }
+ } ensuring ( size(_) == i )
+}
--
GitLab