From cfe3a050fbb2b56a76f0943d4577779ebf87d656 Mon Sep 17 00:00:00 2001
From: ravi <ravi.kandhadai@epfl.ch>
Date: Fri, 4 Dec 2015 16:54:12 +0100
Subject: [PATCH] (a) Adding a test case to test the laziness of And (b) Adding
an option: unfoldFactor to unfold functions more than once in each iteration
of verification
---
.../solvers/combinators/UnrollingSolver.scala | 16 ++++++++++------
.../scala/leon/solvers/z3/FairZ3Component.scala | 3 ++-
.../leon/verification/VerificationPhase.scala | 1 -
.../purescala/invalid/TestLazinessOfAnd.scala | 16 ++++++++++++++++
4 files changed, 28 insertions(+), 8 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/TestLazinessOfAnd.scala
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index f7d395feb..b9c0dfd94 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -13,7 +13,7 @@ import purescala.ExprOps._
import purescala.Types._
import utils._
-import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre, optNoChecks}
+import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre, optNoChecks, optUnfoldFactor}
import templates._
import evaluators._
@@ -27,6 +27,7 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
val useCodeGen = context.findOptionOrDefault(optUseCodeGen)
val assumePreHolds = context.findOptionOrDefault(optAssumePre)
val disableChecks = context.findOptionOrDefault(optNoChecks)
+ val unfoldFactor = context.findOptionOrDefault(optUnfoldFactor)
protected var lastCheckResult : (Boolean, Option[Boolean], Option[HenkinModel]) = (false, None, None)
@@ -306,14 +307,17 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
if(!hasFoundAnswer) {
reporter.debug("- We need to keep going.")
- val toRelease = unrollingBank.getBlockersToUnlock
+ // unfolling `unfoldFactor` times
+ for (i <- 1 to unfoldFactor.toInt) {
+ val toRelease = unrollingBank.getBlockersToUnlock
- reporter.debug(" - more unrollings")
+ reporter.debug(" - more unrollings")
- val newClauses = unrollingBank.unrollBehind(toRelease)
+ val newClauses = unrollingBank.unrollBehind(toRelease)
- for(ncl <- newClauses) {
- solver.assertCnstr(ncl)
+ for (ncl <- newClauses) {
+ solver.assertCnstr(ncl)
+ }
}
reporter.debug(" - finished unrolling")
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Component.scala b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
index 256dcf38f..70ebd260f 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Component.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
@@ -14,9 +14,10 @@ trait FairZ3Component extends LeonComponent {
val optUnrollCores = LeonFlagOptionDef("unrollcores", "Use unsat-cores to drive unrolling while remaining fair", false)
val optAssumePre = LeonFlagOptionDef("assumepre", "Assume precondition holds (pre && f(x) = body) when unfolding", false)
val optNoChecks = LeonFlagOptionDef("nochecks", "Disable counter-example check in presence of foralls" , false)
+ val optUnfoldFactor = LeonLongOptionDef("unfoldFactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
override val definedOptions: Set[LeonOptionDef[Any]] =
- Set(optEvalGround, optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores, optAssumePre)
+ Set(optEvalGround, optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores, optAssumePre, optUnfoldFactor)
}
object FairZ3Component extends FairZ3Component
diff --git a/src/main/scala/leon/verification/VerificationPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
index 21119c4e2..ea09de821 100644
--- a/src/main/scala/leon/verification/VerificationPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -57,7 +57,6 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
}
}
-
try {
val vcs = generateVCs(vctx, toVerify)
diff --git a/src/test/resources/regression/verification/purescala/invalid/TestLazinessOfAnd.scala b/src/test/resources/regression/verification/purescala/invalid/TestLazinessOfAnd.scala
new file mode 100644
index 000000000..113e7193a
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/TestLazinessOfAnd.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+object AndTest {
+ def nonterm(x: BigInt) : BigInt = {
+ nonterm(x + 1)
+ } ensuring(res => false)
+
+ def precond(y : BigInt) = y < 0
+
+ /**
+ * Leon should find a counter-example here.
+ **/
+ def foo(y: BigInt) : Boolean = {
+ require(precond(y))
+ y >= 0 && (nonterm(0) == 0)
+ } holds
+}
--
GitLab