diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 863ac8a16905d9e2740430d2990328f7d1a446a9..09ba190b4042dd9f2e932817ace22b501d883042 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -34,7 +34,8 @@ class FunCheckPlugin(val global: Global) extends Plugin {
" -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
" -P:funcheck:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
" -P:funcheck:CAV CAV 2011 settings. In progress." + "\n" +
- " -P:funcheck:prune (with CAV) Use additional SMT queries to rule out some unrollings."
+ " -P:funcheck:prune (with CAV) Use additional SMT queries to rule out some unrollings." + "\n" +
+ " -P:funcheck:cores (with CAV) Use UNSAT cores in the unrolling/refinement step."
)
/** Processes the command-line options. */
@@ -56,6 +57,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
case "PLDI" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = true; purescala.Settings.useFairInstantiator = false; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
case "CAV" => { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = false; purescala.Settings.useFairInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
case "prune" => purescala.Settings.pruneBranches = true
+ case "cores" => purescala.Settings.useCores = true
case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index de6e68676250b2752b0807bd37ca255613882ea5..d11f7f0f99fc973613c02faba1f82911b9f3a7ad 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -43,7 +43,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
}
z3 = new Z3Context(z3cfg)
partialEvaluator = new PartialEvaluator(program)
- // z3.traceToStdout
+ //z3.traceToStdout
exprToZ3Id = Map.empty
z3IdToExpr = Map.empty
@@ -260,18 +260,32 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
var blockingSet : Set[Expr] = Set(guards.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
+ var iterationsLeft : Int = if(Settings.unrollingLevel > 0) Settings.unrollingLevel else 16121984
+
while(!foundDefinitiveAnswer) {
+ iterationsLeft -= 1
+
val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.map(toZ3Formula(z3, _).get).toSeq
// println("Blocking set : " + blockingSet)
- z3.push
- if(!blockingSetAsZ3.isEmpty)
- z3.assertCnstr(z3.mkAnd(blockingSetAsZ3 : _*))
+ if(Settings.useCores) {
+ // NOOP
+ } else {
+ z3.push
+ if(!blockingSetAsZ3.isEmpty)
+ z3.assertCnstr(z3.mkAnd(blockingSetAsZ3 : _*))
+ }
+
+ val (answer, model, core) : (Option[Boolean], Z3Model, Seq[Z3AST]) = if(Settings.useCores) {
+ println(blockingSetAsZ3)
+ z3.checkAssumptions(blockingSetAsZ3 : _*)
+ } else {
+ val (a, m) = z3.checkAndGetModel()
+ (a, m, Seq.empty[Z3AST])
+ }
- //z3.checkAssumptions(blockingSetAsZ3 : _*) match {
reporter.info(" - Running Z3 search...")
- z3.checkAndGetModel() match {
- // case (None, m, _) => { // UNKNOWN
+ (answer, model) match {
case (None, m) => { // UNKNOWN
reporter.warning("Z3 doesn't know because: " + z3.getSearchFailure.message)
foundDefinitiveAnswer = true
@@ -279,7 +293,6 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
definitiveModel = Map.empty
m.delete
}
- //case (Some(true), m, _) => { // SAT
case (Some(true), m) => { // SAT
val (trueModel, model) = validateAndDeleteModel(m, toCheckAgainstModels, varsInVC)
@@ -295,108 +308,127 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
definitiveModel = model
}
}
- // case (Some(false), m, core) if core.isEmpty => {
- // reporter.info("Empty core, definitively valid.")
- // m.delete
- // foundDefinitiveAnswer = true
- // definitiveAnswer = Some(true)
- // definitiveModel = Map.empty
- // }
- case (Some(false), m) if blockingSet.isEmpty => {
+ case (Some(false), m) if Settings.useCores && core.isEmpty => {
+ reporter.info("Empty core, definitively valid.")
+ m.delete
foundDefinitiveAnswer = true
definitiveAnswer = Some(true)
definitiveModel = Map.empty
}
- // case (Some(false), m, core) => {
+ case (Some(false), m) if !Settings.useCores && blockingSet.isEmpty => {
+ foundDefinitiveAnswer = true
+ definitiveAnswer = Some(true)
+ definitiveModel = Map.empty
+ }
+ // This branch is both for with and without unsat cores. The
+ // distinction is made inside.
case (Some(false), m) => {
- m.delete
- val USEUNSATCORE = false
+ //m.delete
- z3.pop(1)
- val (result2,m2) = z3.checkAndGetModel()
+ if(!Settings.useCores) {
+ z3.pop(1)
+
+ val (result2,m2) = z3.checkAndGetModel()
- if (result2 == Some(false)) {
- foundDefinitiveAnswer = true
- definitiveAnswer = Some(true)
- definitiveModel = Map.empty
- } else {
- // we might have been lucky :D
- val (wereWeLucky, cleanModel) = validateAndDeleteModel(m2, toCheckAgainstModels, varsInVC)
- if(wereWeLucky) {
+ if (result2 == Some(false)) {
foundDefinitiveAnswer = true
- definitiveAnswer = Some(false)
- definitiveModel = cleanModel
+ definitiveAnswer = Some(true)
+ definitiveModel = Map.empty
+ } else {
+ // we might have been lucky :D
+ val (wereWeLucky, cleanModel) = validateAndDeleteModel(m2, toCheckAgainstModels, varsInVC)
+ if(wereWeLucky) {
+ foundDefinitiveAnswer = true
+ definitiveAnswer = Some(false)
+ definitiveModel = cleanModel
+ }
+ }
+ }
+
+ if(!foundDefinitiveAnswer) {
+ reporter.info("- We need to keep going.")
+
+ val toRelease : Set[Expr] = if(Settings.useCores) {
+ core.map(ast => fromZ3Formula(ast) match {
+ case n @ Not(Variable(_)) => n
+ case v @ Variable(_) => v
+ case _ => scala.Predef.error("Impossible element extracted from core: " + ast)
+ }).toSet
} else {
- reporter.info("- We need to keep going.")
-
- val toRelease : Set[Expr] = blockingSet
-
- var fixedForEver : Set[Expr] = Set.empty
-
- if(Settings.pruneBranches) {
- for(ex <- blockingSet) ex match {
- case Not(Variable(b)) => {
- z3.push
- z3.assertCnstr(toZ3Formula(z3, Variable(b)).get)
- z3.check match {
- case Some(false) => {
- //println("We had ~" + b + " in the blocking set. We now know it should stay there forever.")
- z3.pop(1)
- z3.assertCnstr(toZ3Formula(z3, Not(Variable(b))).get)
- fixedForEver = fixedForEver + ex
- }
- case _ => z3.pop(1)
+ blockingSet
+ }
+
+ var fixedForEver : Set[Expr] = Set.empty
+
+ if(Settings.pruneBranches) {
+ for(ex <- blockingSet) ex match {
+ case Not(Variable(b)) => {
+ z3.push
+ z3.assertCnstr(toZ3Formula(z3, Variable(b)).get)
+ z3.check match {
+ case Some(false) => {
+ //println("We had ~" + b + " in the blocking set. We now know it should stay there forever.")
+ z3.pop(1)
+ z3.assertCnstr(toZ3Formula(z3, Not(Variable(b))).get)
+ fixedForEver = fixedForEver + ex
}
+ case _ => z3.pop(1)
}
- case Variable(b) => {
- z3.push
- z3.assertCnstr(toZ3Formula(z3, Not(Variable(b))).get)
- z3.check match {
- case Some(false) => {
- //println("We had " + b + " in the blocking set. We now know it should stay there forever.")
- z3.pop(1)
- z3.assertCnstr(toZ3Formula(z3, Variable(b)).get)
- fixedForEver = fixedForEver + ex
- }
- case _ => z3.pop(1)
+ }
+ case Variable(b) => {
+ z3.push
+ z3.assertCnstr(toZ3Formula(z3, Not(Variable(b))).get)
+ z3.check match {
+ case Some(false) => {
+ //println("We had " + b + " in the blocking set. We now know it should stay there forever.")
+ z3.pop(1)
+ z3.assertCnstr(toZ3Formula(z3, Variable(b)).get)
+ fixedForEver = fixedForEver + ex
}
+ case _ => z3.pop(1)
}
- case _ => scala.Predef.error("Should not have happened.")
- }
- if(fixedForEver.size > 0) {
- reporter.info("- Pruned out " + fixedForEver.size + " branches.")
}
+ case _ => scala.Predef.error("Should not have happened.")
}
+ if(fixedForEver.size > 0) {
+ reporter.info("- Pruned out " + fixedForEver.size + " branches.")
+ }
+ }
- // println("Release set : " + toRelease)
+ // println("Release set : " + toRelease)
- blockingSet = blockingSet -- toRelease
+ blockingSet = blockingSet -- toRelease
- val toReleaseAsPairs : Set[(Identifier,Boolean)] = (toRelease -- fixedForEver).map(b => b match {
- case Variable(id) => (id, true)
- case Not(Variable(id)) => (id, false)
- case _ => scala.Predef.error("Impossible value in release set: " + b)
- })
+ val toReleaseAsPairs : Set[(Identifier,Boolean)] = (toRelease -- fixedForEver).map(b => b match {
+ case Variable(id) => (id, true)
+ case Not(Variable(id)) => (id, false)
+ case _ => scala.Predef.error("Impossible value in release set: " + b)
+ })
- reporter.info(" - more unrollings")
- for((id,polarity) <- toReleaseAsPairs) {
- val (newClauses,newBlockers) = unrollingBank.unlock(id, !polarity)
- // for(clause <- newClauses) {
- // println("we're getting a new clause " + clause)
- // z3.assertCnstr(toZ3Formula(z3, clause).get)
- // }
+ reporter.info(" - more unrollings")
+ for((id,polarity) <- toReleaseAsPairs) {
+ val (newClauses,newBlockers) = unrollingBank.unlock(id, !polarity)
+ // for(clause <- newClauses) {
+ // println("we're getting a new clause " + clause)
+ // z3.assertCnstr(toZ3Formula(z3, clause).get)
+ // }
- for(ncl <- newClauses) {
- z3.assertCnstr(toZ3Formula(z3, ncl).get)
- }
- //z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
- blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
+ for(ncl <- newClauses) {
+ z3.assertCnstr(toZ3Formula(z3, ncl).get)
}
+ //z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
+ blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
}
- // scala.Predef.error("...but not quite now.")
}
}
}
+
+ if(iterationsLeft <= 0) {
+ foundDefinitiveAnswer = true
+ definitiveAnswer = None
+ definitiveModel = Map.empty
+ reporter.error("Max. number of iterations reached.")
+ }
}
(definitiveAnswer, definitiveModel)
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 5510626eb068e00bf814f3f07cf7e714f7366e96..869cc02809a52422bb8dc637af3e4ba192307a29 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -19,6 +19,7 @@ object Settings {
var testBounds: (Int, Int) = (0, 3)
var useInstantiator: Boolean = false
var useFairInstantiator: Boolean = false
+ var useCores : Boolean = false
var pruneBranches : Boolean = false
def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator
}
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index 20d2d8f014cfac64424a9f9118ed31946e205afa..8b59d223ff25777940efed271a3544c45f11084b 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -834,6 +834,8 @@ object Trees {
}
object SimplePatternMatching {
+ def isSimple(me: MatchExpr) : Boolean = unapply(me).isDefined
+
// (scrutinee, classtype, list((caseclassdef, variable, list(variable), rhs)))
def unapply(e: MatchExpr) : Option[(Expr,ClassType,Seq[(CaseClassDef,Identifier,Seq[Identifier],Expr)])] = {
val MatchExpr(scrutinee, cases) = e
@@ -953,36 +955,20 @@ object Trees {
})
}
-// def explicitPreconditions(expr: Expr) : Expr = {
-// def rewriteFunctionCall(e: Expr) : Option[Expr] = e match {
-// case fi @ FunctionInvocation(fd, args) if(fd.hasPrecondition && fd.precondition.get != BooleanLiteral(true)) => {
-// val fTpe = fi.getType
-// val prec = matchToIfThenElse(fd.precondition.get)
-// val newLetIDs = fd.args.map(a => FreshIdentifier("precarg_" + a.id.name, true).setType(a.tpe))
-// val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip newLetIDs.map(Variable(_))) : _*)
-// val newPrec = replace(substMap, prec)
-// val newThen = FunctionInvocation(fd, newLetIDs.map(_.toVariable)).setType(fTpe).setPosInfo(fi)
-// val ifExpr: Expr = IfExpr(newPrec, newThen, Error("precondition violated").setType(fTpe).setPosInfo(fi)).setType(fTpe)
-// Some((newLetIDs zip args).foldRight(ifExpr)((iap,e) => Let(iap._1, iap._2, e)))
-// }
-// case _ => None
-// }
-//
-// searchAndReplaceDFS(rewriteFunctionCall)(expr)
-// }
-
private var matchConverterCache = new scala.collection.mutable.HashMap[Expr,Expr]()
/** Rewrites all pattern-matching expressions into if-then-else expressions,
* with additional error conditions. Does not introduce additional variables.
* We use a cache because we can. */
def matchToIfThenElse(expr: Expr) : Expr = {
- if(matchConverterCache.isDefinedAt(expr)) {
+ val toRet = if(matchConverterCache.isDefinedAt(expr)) {
matchConverterCache(expr)
} else {
val converted = convertMatchToIfThenElse(expr)
matchConverterCache(expr) = converted
converted
}
+
+ toRet
}
private def convertMatchToIfThenElse(expr: Expr) : Expr = {
@@ -1030,14 +1016,23 @@ object Trees {
(realCond, newRhs)
}
- val bigIte = condsAndRhs.foldRight[Expr](Error("non-exhaustive match").setType(bestRealType(m.getType)).setPosInfo(m))((p1, ex) => {
+ val optCondsAndRhs = if(SimplePatternMatching.isSimple(m)) {
+ // this is a hackish optimization: because we know all cases are covered, we replace the last condition by true (and that drops the check)
+ val lastExpr = condsAndRhs.last._2
+
+ condsAndRhs.dropRight(1) ++ Seq((BooleanLiteral(true),lastExpr))
+ } else {
+ condsAndRhs
+ }
+
+ val bigIte = optCondsAndRhs.foldRight[Expr](Error("non-exhaustive match").setType(bestRealType(m.getType)).setPosInfo(m))((p1, ex) => {
if(p1._1 == BooleanLiteral(true)) {
p1._2
} else {
IfExpr(p1._1, p1._2, ex).setType(m.getType)
}
})
- //println(condsAndRhs)
+
Some(bigIte)
}
case _ => None