Skip to content
Snippets Groups Projects
Commit 99fb25b5 authored by Philippe Suter's avatar Philippe Suter
Browse files

code for "I'm feeling lucky"

parent a94c85f3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
cav2011-testcases/Debug.scala 0 → 100644
+ 43
− 0
View file @ 99fb25b5
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
}
cav2011-testcases/RedBlackTree.scala 0 → 100644
+ 112
− 0
View file @ 99fb25b5
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))
}
funcheck-etaps deleted 100755 → 0
+ 0
− 2
View file @ a94c85f3
#!/bin/bash
./scalac-funcheck -P:funcheck:nodefaults -P:funcheck:extensions=orderedsets.Main "$@"
src/purescala/FairZ3Solver.scala
+ 81
− 197
View file @ 99fb25b5
...@@ -33,6 +33,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac ...@@ -33,6 +33,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
program = prog program = prog
} }
var partialEvaluator : PartialEvaluator = null
private def restartZ3: Unit = { private def restartZ3: Unit = {
if (neverInitialized) { if (neverInitialized) {
neverInitialized = false neverInitialized = false
...@@ -40,6 +42,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac ...@@ -40,6 +42,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
z3.delete z3.delete
} }
z3 = new Z3Context(z3cfg) z3 = new Z3Context(z3cfg)
partialEvaluator = new PartialEvaluator(program)
// z3.traceToStdout // z3.traceToStdout
exprToZ3Id = Map.empty exprToZ3Id = Map.empty
...@@ -278,32 +281,19 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac ...@@ -278,32 +281,19 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
} }
//case (Some(true), m, _) => { // SAT //case (Some(true), m, _) => { // SAT
case (Some(true), m) => { // SAT case (Some(true), m) => { // SAT
import Evaluator._ val (trueModel, model) = validateAndDeleteModel(m, toCheckAgainstModels, varsInVC)
val asMap = modelToMap(m, varsInVC) if (trueModel) {
lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n") foundDefinitiveAnswer = true
reporter.info("A candidate counter-example was found. It should be valid, but let's check anyway.") definitiveAnswer = Some(false)
reporter.info(modelAsString) definitiveModel = model
val evalResult = eval(asMap, toCheckAgainstModels) } else {
reporter.error("Something went wrong. The model should have been valid, yet we got this : ")
evalResult match { reporter.error(model)
case OK(BooleanLiteral(true)) => { foundDefinitiveAnswer = true
reporter.error("Counter-example found and confirmed:") definitiveAnswer = None
reporter.error(modelAsString) definitiveModel = model
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
}
} }
m.delete
} }
// case (Some(false), m, core) if core.isEmpty => { // case (Some(false), m, core) if core.isEmpty => {
// reporter.info("Empty core, definitively valid.") // reporter.info("Empty core, definitively valid.")
...@@ -324,42 +314,49 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac ...@@ -324,42 +314,49 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
z3.pop(1) z3.pop(1)
val (result2,m2) = z3.checkAndGetModel() val (result2,m2) = z3.checkAndGetModel()
m2.delete
if (result2 == Some(false)) { if (result2 == Some(false)) {
foundDefinitiveAnswer = true foundDefinitiveAnswer = true
definitiveAnswer = Some(true) definitiveAnswer = Some(true)
definitiveModel = Map.empty definitiveModel = Map.empty
} else { } else {
reporter.info("We need to keep going.") // we might have been lucky :D
val (wereWeLucky, cleanModel) = validateAndDeleteModel(m2, toCheckAgainstModels, varsInVC)
val toRelease : Set[Expr] = if(USEUNSATCORE) { if(wereWeLucky) {
blockingSet//core.map(fromZ3Formula(_)).toSet foundDefinitiveAnswer = true
definitiveAnswer = Some(false)
definitiveModel = cleanModel
} else { } 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 { blockingSet = blockingSet -- toRelease
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") val toReleaseAsPairs : Set[(Identifier,Boolean)] = toRelease.map(b => b match {
for((id,polarity) <- toReleaseAsPairs) { case Variable(id) => (id, true)
val (newClauses,newBlockers) = unrollingBank.unlock(id, !polarity) case Not(Variable(id)) => (id, false)
// for(clause <- newClauses) { case _ => scala.Predef.error("Impossible value in release set: " + b)
// println("we're getting a new clause " + clause) })
// z3.assertCnstr(toZ3Formula(z3, clause).get)
// }
z3.assertCnstr(toZ3Formula(z3, And(newClauses)).get) reporter.info(" - more unrollings")
blockingSet = blockingSet ++ Set(newBlockers.map(p => if(p._2) Not(Variable(p._1)) else Variable(p._1)) : _*) 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.") // scala.Predef.error("...but not quite now.")
} }
} }
...@@ -367,153 +364,37 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac ...@@ -367,153 +364,37 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
} }
(definitiveAnswer, definitiveModel) (definitiveAnswer, definitiveModel)
}
private def validateAndDeleteModel(model: Z3Model, formula: Expr, variables: Set[Identifier]) : (Boolean, Map[Identifier,Expr]) = {
import Evaluator._
//var toUnroll : Set[FunctionInvocation] = Set.empty val asMap = modelToMap(model, variables)
//var everythingEverUnrolled : Set[FunctionInvocation] = Set.empty model.delete
//var blockingClause : List[Expr] = Nil
//val (basis, cls, bools) = clausifyITE(toCheckAgainstModels) lazy val modelAsString = asMap.toList.map(p => p._1 + " -> " + p._2).mkString("\n")
//var clauses = cls val evalResult = eval(asMap, formula)
//toUnroll = toUnroll ++ topLevelFunctionCallsOf(basis) evalResult match {
case OK(BooleanLiteral(true)) => {
//println("The basis, with function calls " + topLevelFunctionCallsOf(basis)) reporter.info("Model validated:")
//println(basis) reporter.info(modelAsString)
//println("The clauses") (true, asMap)
//for (clause <- clauses) { }
// println(clause) case RuntimeError(msg) => {
reporter.info("Model leads to runtime error: " + msg)
// clause match { reporter.error(modelAsString)
// case Iff(Variable(switch), cond) => { (true, asMap)
// toUnroll = toUnroll ++ topLevelFunctionCallsOf(cond) }
// } case OK(BooleanLiteral(false)) => {
// case Implies(v @ Variable(switch), then) => { reporter.info("Invalid model.")
// if(!topLevelFunctionCallsOf(then).isEmpty) { (false, Map.empty)
// blockingClause = Not(v) :: blockingClause }
// } case other => {
// } reporter.error("Something went wrong. While evaluating the model, we got this: " + other)
// case Implies(Not(v @ Variable(switch)), elze) => { (false, Map.empty)
// 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
} }
// Returns between 0 and 2 tautologies with respect to the interpretation of // 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 ...@@ -523,14 +404,16 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
val postExpr = if(fd.hasPostcondition) { val postExpr = if(fd.hasPostcondition) {
val post = expandLets(matchToIfThenElse(fd.postcondition.get)) val post = expandLets(matchToIfThenElse(fd.postcondition.get))
val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip args) : _*) + (ResultVariable() -> functionInvocation) 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) List(newBody)
} else Nil } else Nil
val bodyExpr = if(fd.hasBody) { val bodyExpr = if(fd.hasBody) {
val body = expandLets(matchToIfThenElse(fd.body.get)) val body = expandLets(matchToIfThenElse(fd.body.get))
val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip args) : _*) 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)) List(Equals(functionInvocation, newBody))
} else Nil } else Nil
...@@ -855,6 +738,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac ...@@ -855,6 +738,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
stillToUnroll = Set.empty stillToUnroll = Set.empty
for(stu <- (copy -- unrolledNow) if !wasUnrolledBefore(stu)) { for(stu <- (copy -- unrolledNow) if !wasUnrolledBefore(stu)) {
// println("unrolling " + stu)
val unrolled : Seq[Expr] = unroll(stu) // that's between 0 and two formulas val unrolled : Seq[Expr] = unroll(stu) // that's between 0 and two formulas
registerAsUnrolled(stu) registerAsUnrolled(stu)
unrolledNow = unrolledNow + stu unrolledNow = unrolledNow + stu
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment