From 99fb25b5bd5fbc4bdc0acb87413021845e8855b2 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Fri, 21 Jan 2011 13:01:38 +0000
Subject: [PATCH] code for "I'm feeling lucky"
---
cav2011-testcases/Debug.scala | 43 +++++
cav2011-testcases/RedBlackTree.scala | 112 +++++++++++
funcheck-etaps | 2 -
src/purescala/FairZ3Solver.scala | 278 ++++++++-------------------
4 files changed, 236 insertions(+), 199 deletions(-)
create mode 100644 cav2011-testcases/Debug.scala
create mode 100644 cav2011-testcases/RedBlackTree.scala
delete mode 100755 funcheck-etaps
diff --git a/cav2011-testcases/Debug.scala b/cav2011-testcases/Debug.scala
new file mode 100644
index 000000000..4fc8c01f5
--- /dev/null
+++ b/cav2011-testcases/Debug.scala
@@ -0,0 +1,43 @@
+import funcheck.Utils._
+import funcheck.Annotations._
+import scala.annotation.tailrec
+
+object Debug {
+ sealed abstract class List
+ case class Nil() extends List
+ case class Cons(head: Int, tail: List) extends List
+
+ def size1(list: List) : Int = {
+ list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size1(xs)
+ }
+ } ensuring(_ >= 0)
+
+ def size2(list: List) : Int = {
+ sizeTailRec(list, 0)
+ }
+
+ def identity(list: List) : List = list
+
+ def zero() : Int = 0
+
+ def sizeTailRec(list: List, acc: Int) : Int = {
+ require(acc >= 0)
+ list match {
+ case Nil() => acc
+ case Cons(_, xs) => sizeTailRec(xs, acc + 1)
+ }
+ } ensuring(_ == acc + size1(list))
+
+ def sizesAreTheSame(list: List) : Boolean = {
+ size1(list) == size2(list)
+ } holds
+
+ def bug(list: List) : Boolean = {
+ list match {
+ case Nil() => true
+ case Cons(_,_) => size1(list) == size2(list) + 1
+ }
+ } holds
+}
diff --git a/cav2011-testcases/RedBlackTree.scala b/cav2011-testcases/RedBlackTree.scala
new file mode 100644
index 000000000..d6d447e65
--- /dev/null
+++ b/cav2011-testcases/RedBlackTree.scala
@@ -0,0 +1,112 @@
+import scala.collection.immutable.Set
+import funcheck.Annotations._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ t match {
+ case Empty() => Node(Red(),Empty(),x,Empty())
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ )
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n))
+ n match {
+ case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+ case _ => n
+ }
+ } ensuring(redNodesHaveBlackChildren(_))
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def buggyAdd(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ //makeBlack(ins(x, t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ //require(
+ // Node(c,a,x,b) match {
+ // case Node(Black(),Node(Red(),Node(Red(),a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black(),Node(Red(),a,_,Node(Red(),b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black(),a,_,Node(Red(),Node(Red(),b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black(),a,_,Node(Red(),b,_,Node(Red(),c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ //)
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)) )//&& redDescHaveBlackChildren(res))
+}
diff --git a/funcheck-etaps b/funcheck-etaps
deleted file mode 100755
index 6e6f2d534..000000000
--- a/funcheck-etaps
+++ /dev/null
@@ -1,2 +0,0 @@
-#!/bin/bash
-./scalac-funcheck -P:funcheck:nodefaults -P:funcheck:extensions=orderedsets.Main "$@"
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 87cd67786..9dbdfd178 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -33,6 +33,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
program = prog
}
+ var partialEvaluator : PartialEvaluator = null
+
private def restartZ3: Unit = {
if (neverInitialized) {
neverInitialized = false
@@ -40,6 +42,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
z3.delete
}
z3 = new Z3Context(z3cfg)
+ partialEvaluator = new PartialEvaluator(program)
// z3.traceToStdout
exprToZ3Id = Map.empty
@@ -278,32 +281,19 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
}
//case (Some(true), m, _) => { // SAT
case (Some(true), m) => { // SAT
- import Evaluator._
-
- val asMap = modelToMap(m, varsInVC)
- lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
- reporter.info("A candidate counter-example was found. It should be valid, but let's check anyway.")
- reporter.info(modelAsString)
- val evalResult = eval(asMap, toCheckAgainstModels)
-
- evalResult match {
- case OK(BooleanLiteral(true)) => {
- reporter.error("Counter-example found and confirmed:")
- reporter.error(modelAsString)
- foundDefinitiveAnswer = true
- definitiveAnswer = Some(false)
- definitiveModel = asMap
- }
- case other => {
- //println(z3)
- reporter.error("Something went wrong. The model should have been valid, yet we got this: " + other)
- reporter.error(m)
- foundDefinitiveAnswer = true
- definitiveAnswer = None
- definitiveModel = asMap
- }
+ val (trueModel, model) = validateAndDeleteModel(m, toCheckAgainstModels, varsInVC)
+
+ if (trueModel) {
+ foundDefinitiveAnswer = true
+ definitiveAnswer = Some(false)
+ definitiveModel = model
+ } else {
+ reporter.error("Something went wrong. The model should have been valid, yet we got this : ")
+ reporter.error(model)
+ foundDefinitiveAnswer = true
+ definitiveAnswer = None
+ definitiveModel = model
}
- m.delete
}
// case (Some(false), m, core) if core.isEmpty => {
// reporter.info("Empty core, definitively valid.")
@@ -324,42 +314,49 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
z3.pop(1)
val (result2,m2) = z3.checkAndGetModel()
- m2.delete
+
if (result2 == Some(false)) {
foundDefinitiveAnswer = true
definitiveAnswer = Some(true)
definitiveModel = Map.empty
} else {
- reporter.info("We need to keep going.")
-
- val toRelease : Set[Expr] = if(USEUNSATCORE) {
- blockingSet//core.map(fromZ3Formula(_)).toSet
+ // we might have been lucky :D
+ val (wereWeLucky, cleanModel) = validateAndDeleteModel(m2, toCheckAgainstModels, varsInVC)
+ if(wereWeLucky) {
+ foundDefinitiveAnswer = true
+ definitiveAnswer = Some(false)
+ definitiveModel = cleanModel
} else {
- blockingSet
- }
+ reporter.info("We need to keep going.")
- // println("Release set : " + toRelease)
+ val toRelease : Set[Expr] = if(USEUNSATCORE) {
+ blockingSet//core.map(fromZ3Formula(_)).toSet
+ } else {
+ blockingSet
+ }
- blockingSet = blockingSet -- toRelease
+ // println("Release set : " + toRelease)
- val toReleaseAsPairs : Set[(Identifier,Boolean)] = toRelease.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)
- })
+ blockingSet = blockingSet -- toRelease
- 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)
- // }
+ val toReleaseAsPairs : Set[(Identifier,Boolean)] = toRelease.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)
+ })
- z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get)
- blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*)
- }
+ 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)
+ // }
+ 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.")
}
}
@@ -367,153 +364,37 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
}
(definitiveAnswer, definitiveModel)
+ }
+
+ private def validateAndDeleteModel(model: Z3Model, formula: Expr, variables: Set[Identifier]) : (Boolean, Map[Identifier,Expr]) = {
+ import Evaluator._
- //var toUnroll : Set[FunctionInvocation] = Set.empty
- //var everythingEverUnrolled : Set[FunctionInvocation] = Set.empty
- //var blockingClause : List[Expr] = Nil
- //val (basis, cls, bools) = clausifyITE(toCheckAgainstModels)
- //var clauses = cls
-
- //toUnroll = toUnroll ++ topLevelFunctionCallsOf(basis)
-
- //println("The basis, with function calls " + topLevelFunctionCallsOf(basis))
- //println(basis)
- //println("The clauses")
- //for (clause <- clauses) {
- // println(clause)
-
- // clause match {
- // case Iff(Variable(switch), cond) => {
- // toUnroll = toUnroll ++ topLevelFunctionCallsOf(cond)
- // }
- // case Implies(v @ Variable(switch), then) => {
- // if(!topLevelFunctionCallsOf(then).isEmpty) {
- // blockingClause = Not(v) :: blockingClause
- // }
- // }
- // case Implies(Not(v @ Variable(switch)), elze) => {
- // if(!topLevelFunctionCallsOf(elze).isEmpty) {
- // blockingClause = v :: blockingClause
- // }
- // }
- // case _ => scala.Predef.error("Something wrong happened. Who added this clause? " + clause)
- // }
- //}
-
- //// I'm conjecturing that this loop terminates :D
- //while(!toUnroll.isEmpty) {
- // println("Still to unroll now:")
- // println(toUnroll)
- // val copy = toUnroll
- // toUnroll = Set.empty
-
- // for(tu <- copy) {
- // val unrolled = unroll(tu) // this is a list of formulas
- // for(formula <- unrolled) {
- // val (basis2, clauses2, _) = clausifyITE(formula)
- // println(tu + " unrolled gives us " + basis2 + "\n" + clauses2.map(_.toString).mkString("\n"))
- // toUnroll = toUnroll ++ topLevelFunctionCallsOf(basis2)
- // clauses = basis2 :: (clauses2 ::: clauses)
- // for (clause <- clauses2) {
- // clause match {
- // case Iff(Variable(switch), cond) => {
- // toUnroll = toUnroll ++ topLevelFunctionCallsOf(cond)
- // }
- // case Implies(v @ Variable(switch), then) => {
- // if(!topLevelFunctionCallsOf(then).isEmpty) {
- // blockingClause = Not(v) :: blockingClause
- // }
- // }
- // case Implies(Not(v @ Variable(switch)), elze) => {
- // if(!topLevelFunctionCallsOf(elze).isEmpty) {
- // blockingClause = v :: blockingClause
- // }
- // }
- // case _ => scala.Predef.error("Something wrong happened. Who added this clause? " + clause)
- // }
- // }
- // }
- // }
- // everythingEverUnrolled = everythingEverUnrolled ++ copy
- // toUnroll = toUnroll -- everythingEverUnrolled
- //}
- //println("The booleans.")
- //println(bools)
-
- //println("The blocking clause.")
- //println(And(blockingClause))
-
-
- //val toConvert = And(basis, And(clauses))
-
- //val result : (Option[Boolean],Map[Identifier,Expr]) = toZ3Formula(z3, toConvert) match {
- // case None => (None, Map.empty) // means it could not be translated
- // case Some(z3f) => {
- // z3.assertCnstr(z3f)
- // //println(z3f)
-
- // //z3.assertCnstr(toZ3Formula(z3, And(blockingClause)).get)
-
- // var foundDefinitiveSolution = false
-
- // val blockingClauseAsZ3 : Seq[Z3AST] = blockingClause.map(toZ3Formula(z3, _).get)
-
- // val actualResult : (Option[Boolean],Map[Identifier,Expr]) = (z3.checkAssumptions(blockingClauseAsZ3 : _*) match {
- // case (Some(true), m, _) => {
- // import Evaluator._
-
- // // WE HAVE TO CHECK THE COUNTER-EXAMPLE.
- // val asMap = modelToMap(m, varsInVC)
- // lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
- // reporter.info(" - A candidate counter-example was found... Examining...")
- // reporter.info(modelAsString)
-
- // val evalResult = eval(asMap, toCheckAgainstModels)
- //
- // evalResult match {
- // case OK(BooleanLiteral(true)) => {
- // reporter.error("Counter-example found and confirmed:")
- // reporter.error(modelAsString)
- // foundDefinitiveSolution = true
- // (Some(false), asMap)
- // }
- // case OK(BooleanLiteral(false)) => {
- // reporter.info("Not a valid counter-example. Must.. keep.. going..")
- // (None, asMap)
- // }
- // case InfiniteComputation() => {
- // reporter.info("Model seems to lead to divergent computation.")
- // reporter.error(modelAsString)
- // foundDefinitiveSolution = true
- // (None, asMap)
- // }
- // case RuntimeError(msg) => {
- // reporter.info("Model leads to runtime error: " + msg)
- // reporter.error(modelAsString)
- // foundDefinitiveSolution = true
- // (Some(false), asMap)
- // }
- // case t @ TypeError(_,_) => {
- // scala.Predef.error("Type error in model evaluation.\n" + t.msg)
- // }
- // case _ => {
- // scala.Predef.error("Why am I here?")
- // }
- // }
- // }
- // case (Some(false), _, core) => {
- // reporter.info("Here is the core : " + core.map(_.toString).mkString(", "))
- // (Some(true), Map.empty)
- // }
- // case (None, m, _) => {
- // reporter.warning("Z3 doesn't know because: " + z3.getSearchFailure.message)
- // (None, Map.empty)
- // }
- // })
- // actualResult
- // }
- //}
- //result
+ val asMap = modelToMap(model, variables)
+ model.delete
+
+ lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
+ val evalResult = eval(asMap, formula)
+
+ evalResult match {
+ case OK(BooleanLiteral(true)) => {
+ reporter.info("Model validated:")
+ reporter.info(modelAsString)
+ (true, asMap)
+ }
+ case RuntimeError(msg) => {
+ reporter.info("Model leads to runtime error: " + msg)
+ reporter.error(modelAsString)
+ (true, asMap)
+ }
+ case OK(BooleanLiteral(false)) => {
+ reporter.info("Invalid model.")
+ (false, Map.empty)
+ }
+ case other => {
+ reporter.error("Something went wrong. While evaluating the model, we got this: " + other)
+ (false, Map.empty)
+ }
+ }
}
// Returns between 0 and 2 tautologies with respect to the interpretation of
@@ -523,14 +404,16 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
val postExpr = if(fd.hasPostcondition) {
val post = expandLets(matchToIfThenElse(fd.postcondition.get))
val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip args) : _*) + (ResultVariable() -> functionInvocation)
- val newBody = /*partialEvaluator(*/replace(substMap, post)/*)*/
+ //val newBody = partialEvaluator(replace(substMap, post))
+ val newBody = replace(substMap, post)
List(newBody)
} else Nil
val bodyExpr = if(fd.hasBody) {
val body = expandLets(matchToIfThenElse(fd.body.get))
val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip args) : _*)
- val newBody = /*partialEvaluator(*/replace(substMap, body)/*)*/
+ //val newBody = partialEvaluator(replace(substMap, body))
+ val newBody = replace(substMap, body)
List(Equals(functionInvocation, newBody))
} else Nil
@@ -855,6 +738,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
stillToUnroll = Set.empty
for(stu <- (copy -- unrolledNow) if !wasUnrolledBefore(stu)) {
+ // println("unrolling " + stu)
val unrolled : Seq[Expr] = unroll(stu) // that's between 0 and two formulas
registerAsUnrolled(stu)
unrolledNow = unrolledNow + stu
--
GitLab