From 31640cd6642e31dd80cff815336a5c4cb79eeefa Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 18 Nov 2010 15:32:44 +0000
Subject: [PATCH] new solver that checks intermediate counter examples
---
src/purescala/Definitions.scala | 18 ++++
src/purescala/Extensions.scala | 6 +-
src/purescala/IterativeZ3Solver.scala | 7 ++
src/purescala/Trees.scala | 48 ++++------
src/purescala/Z3ModelReconstruction.scala | 11 +++
src/purescala/Z3Solver.scala | 93 ++++++++++++++++++-
.../z3plugins/instantiator/Instantiator.scala | 7 +-
7 files changed, 150 insertions(+), 40 deletions(-)
diff --git a/src/purescala/Definitions.scala b/src/purescala/Definitions.scala
index 297d8d025..11e6d35ef 100644
--- a/src/purescala/Definitions.scala
+++ b/src/purescala/Definitions.scala
@@ -201,6 +201,24 @@ object Definitions {
this
}
def parent = parent_
+
+ def selectorID2Index(id: Identifier) : Int = {
+ var i : Int = 0
+ var found = false
+ val fs = fields.size
+ while(!found && i < fs) {
+ if(fields(i).id == id) {
+ found = true
+ } else {
+ i += 1
+ }
+ }
+
+ if(found)
+ i
+ else
+ scala.Predef.error("Asking for index of field that does not belong to the case class.")
+ }
}
/** "Regular" classes */
diff --git a/src/purescala/Extensions.scala b/src/purescala/Extensions.scala
index 7b1331748..f97c25d00 100644
--- a/src/purescala/Extensions.scala
+++ b/src/purescala/Extensions.scala
@@ -85,11 +85,7 @@ object Extensions {
}
// these extensions are always loaded, unless specified otherwise
val defaultExtensions: Seq[Extension] = if(Settings.runDefaultExtensions) {
- if(false && Settings.useInstantiator) {
- (new IterativeZ3Solver(extensionsReporter)) :: Nil
- } else {
- (new Z3Solver(extensionsReporter)) :: Nil
- }
+ (new Z3Solver(extensionsReporter)) :: Nil
} else {
Nil
}
diff --git a/src/purescala/IterativeZ3Solver.scala b/src/purescala/IterativeZ3Solver.scala
index 479ee402e..e142b4fcc 100644
--- a/src/purescala/IterativeZ3Solver.scala
+++ b/src/purescala/IterativeZ3Solver.scala
@@ -1,3 +1,8 @@
+/*
+
+This file is rubbish, I'm sticking with Z3Solver.scala...
+
+
package purescala
import z3.scala._
@@ -15,3 +20,5 @@ class IterativeZ3Solver(reporter: Reporter) extends Z3Solver(reporter) {
Some(false)
}
}
+
+*/
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index 4945b0fda..8be7aaeb8 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -92,22 +92,14 @@ object Trees {
/* Propositional logic */
object And {
- def apply(exprs: Seq[Expr]) : Expr = {
- val newExprs = exprs.filter(_ != BooleanLiteral(true))
- if(newExprs.contains(BooleanLiteral(false))) {
- BooleanLiteral(false)
- } else newExprs.size match {
- case 0 => BooleanLiteral(true)
- case 1 => newExprs.head
- case _ => new And(newExprs)
- }
+ def apply(l: Expr, r: Expr) : Expr = (l,r) match {
+ case (BooleanLiteral(true),_) => r
+ case (_,BooleanLiteral(true)) => l
+ case _ => new And(Seq(l,r))
}
-
- def apply(l: Expr, r: Expr): Expr = (l,r) match {
- case (And(exs1), And(exs2)) => And(exs1 ++ exs2)
- case (And(exs1), ex2) => And(exs1 :+ ex2)
- case (ex1, And(exs2)) => And(exs2 :+ ex1)
- case (ex1, ex2) => And(List(ex1, ex2))
+ def apply(exprs: Seq[Expr]) : Expr = {
+ val simpler = exprs.filter(_ != BooleanLiteral(true))
+ if(simpler.isEmpty) BooleanLiteral(true) else simpler.reduceRight(And(_,_))
}
def unapply(and: And) : Option[Seq[Expr]] =
@@ -119,22 +111,14 @@ object Trees {
}
object Or {
- def apply(exprs: Seq[Expr]) : Expr = {
- val newExprs = exprs.filter(_ != BooleanLiteral(false))
- if(newExprs.contains(BooleanLiteral(true))) {
- BooleanLiteral(true)
- } else newExprs.size match {
- case 0 => BooleanLiteral(false)
- case 1 => newExprs.head
- case _ => new Or(newExprs)
- }
+ def apply(l: Expr, r: Expr) : Expr = (l,r) match {
+ case (BooleanLiteral(false),_) => r
+ case (_,BooleanLiteral(false)) => l
+ case _ => new Or(Seq(l,r))
}
-
- def apply(l: Expr, r: Expr): Expr = (l,r) match {
- case (Or(exs1), Or(exs2)) => Or(exs1 ++ exs2)
- case (Or(exs1), ex2) => Or(exs1 :+ ex2)
- case (ex1, Or(exs2)) => Or(exs2 :+ ex1)
- case (ex1, ex2) => Or(List(ex1, ex2))
+ def apply(exprs: Seq[Expr]) : Expr = {
+ val simpler = exprs.filter(_ != BooleanLiteral(false))
+ if(simpler.isEmpty) BooleanLiteral(false) else simpler.reduceRight(Or(_,_))
}
def unapply(or: Or) : Option[Seq[Expr]] =
@@ -273,8 +257,8 @@ object Trees {
}
/* Option expressions */
- case class OptionSome(value: Expr) extends Expr
- case class OptionNone(baseType: TypeTree) extends Expr with Terminal
+ // case class OptionSome(value: Expr) extends Expr
+ // case class OptionNone(baseType: TypeTree) extends Expr with Terminal
/* Set expressions */
case class EmptySet(baseType: TypeTree) extends Expr with Terminal
diff --git a/src/purescala/Z3ModelReconstruction.scala b/src/purescala/Z3ModelReconstruction.scala
index 6565549cd..c7d94612a 100644
--- a/src/purescala/Z3ModelReconstruction.scala
+++ b/src/purescala/Z3ModelReconstruction.scala
@@ -27,6 +27,17 @@ trait Z3ModelReconstruction {
}
}
+ def modelToMap(model: Z3Model, ids: Iterable[Identifier]) : Map[Identifier,Expr] = {
+ var asMap = Map.empty[Identifier,Expr]
+ for(id <- ids) {
+ modelValue(model, id) match {
+ case None => ; // can't do much here
+ case Some(ex) => asMap = asMap + ((id -> ex))
+ }
+ }
+ asMap
+ }
+
def printExtractedModel(model: Z3Model, ids : Iterable[Identifier]) : Unit = {
reporter.info("Tentative extracted model")
reporter.info("*************************")
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index 24af2daf3..a00212809 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -336,7 +336,13 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
def solve(vc: Expr) = decide(vc, true)
- def decide(vc: Expr, forValidity: Boolean): Option[Boolean] = {
+ def decide(vc: Expr, fv: Boolean) : Option[Boolean] = if(Settings.useInstantiator) {
+ decideIterative(vc, fv)
+ } else {
+ decideStandard(vc, fv)
+ }
+
+ def decideStandard(vc: Expr, forValidity: Boolean): Option[Boolean] = {
restartZ3
abstractedFormula = false
@@ -403,6 +409,91 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
result
}
+ def decideIterative(vc: Expr, forValidity: Boolean) : Option[Boolean] = {
+ restartZ3
+ assert(instantiator != null)
+ assert(!useBAPA)
+
+ lazy val varsInVC = variablesOf(vc)
+
+ if (neverInitialized) {
+ reporter.error("Z3 Solver was not initialized with a PureScala Program.")
+ None
+ }
+ val toConvert = if (forValidity) negate(vc) else vc
+ val toCheckAgainstModels = toConvert
+
+ val result = toZ3Formula(z3, toConvert) match {
+ case None => None // means it could not be translated
+ case Some(z3f) => {
+ z3.assertCnstr(z3f)
+
+ // THE LOOP STARTS HERE.
+ var foundDefinitiveSolution : Boolean = false
+ var finalResult : Option[Boolean] = None
+
+ while(!foundDefinitiveSolution && instantiator.possibleContinuation) {
+ instantiator.increaseSearchDepth()
+ z3.checkAndGetModel() match {
+ case (Some(true), m) => {
+ import Evaluator._
+
+ // WE HAVE TO CHECK THE COUNTER-EXAMPLE.
+ println("A candidate counter-example was found... Examining...")
+ val asMap = modelToMap(m, varsInVC)
+
+ lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
+
+ //println("(I'm going to pretend this never happened...)")
+
+ val evalResult = eval(asMap, toCheckAgainstModels)
+
+
+ evalResult match {
+ case OK(BooleanLiteral(true)) => {
+ reporter.error("Counter-example found and confirmed:")
+ reporter.error(modelAsString)
+ foundDefinitiveSolution = true
+ finalResult = Some(false)
+ }
+ case InfiniteComputation() => {
+ reporter.info("Model seems to lead to divergent computation.")
+ reporter.error(modelAsString)
+ foundDefinitiveSolution = true
+ finalResult = None
+ }
+ case RuntimeError(msg) => {
+ reporter.info("Model leads to runtime error: " + msg)
+ foundDefinitiveSolution = true
+ finalResult = Some(false)
+ }
+ case t @ TypeError(_,_) => {
+ scala.Predef.error("Type error in model evaluation.\n" + t.msg)
+ }
+ case _ => {
+ // false positive. keep searching
+ }
+ }
+ }
+
+ case (Some(false), _) => {
+ // This means a definitive proof of unsatisfiability has been found.
+ foundDefinitiveSolution = true
+ finalResult = Some(true)
+ }
+
+ case (None, m) => {
+ reporter.warning("Iterative Z3 gave up because: " + z3.getSearchFailure.message)
+ foundDefinitiveSolution = true
+ finalResult = None
+ }
+ }
+ }
+ finalResult
+ }
+ }
+ result
+ }
protected[purescala] var exprToZ3Id : Map[Expr,Z3AST] = Map.empty
protected[purescala] var z3IdToExpr : Map[Z3AST,Expr] = Map.empty
diff --git a/src/purescala/z3plugins/instantiator/Instantiator.scala b/src/purescala/z3plugins/instantiator/Instantiator.scala
index b5834f139..f77859c34 100644
--- a/src/purescala/z3plugins/instantiator/Instantiator.scala
+++ b/src/purescala/z3plugins/instantiator/Instantiator.scala
@@ -134,8 +134,7 @@ class Instantiator(val z3Solver: Z3Solver) extends Z3Theory(z3Solver.z3, "Instan
override def finalCheck : Boolean = safeBlockToAssertAxioms {
if(!queue.isEmpty) {
- val smallest = queue.head.depth
- while(!queue.isEmpty) { // && queue.head.depth == smallest) {
+ while(!queue.isEmpty && queue.head.depth <= deepestAuthorized) {
val highest : Unrolling = queue.dequeue()
val toConvertAndAssert = if(highest.isContract) {
highest.body
@@ -249,6 +248,10 @@ class Instantiator(val z3Solver: Z3Solver) extends Z3Theory(z3Solver.z3, "Instan
}
}
+ private var deepestAuthorized : Int = -1
+ def possibleContinuation : Boolean = !queue.isEmpty || deepestAuthorized <= 0
+ def increaseSearchDepth() : Unit = { deepestAuthorized += 1; bodyInlined = 0 }
+
reinit
private def reinit : Unit = {
pushLevel = 0
--
GitLab