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

towards getting enumeration of testcases to work again

parent cdc697d1
No related branches found
No related tags found
No related merge requests found
......@@ -10,7 +10,17 @@ import TypeTrees._
// This is just to factor out the things that are common in "classes that deal
// with a Z3 instance"
trait AbstractZ3Solver {
val reporter : Reporter
self: Solver =>
val reporter: Reporter
protected[purescala] var z3 : Z3Context
protected[purescala] var program : Program
def typeToSort(tt: TypeTree): Z3Sort
protected[purescala] var adtTesters: Map[CaseClassDef, Z3FuncDecl]
protected[purescala] var adtConstructors: Map[CaseClassDef, Z3FuncDecl]
protected[purescala] var adtFieldSelectors: Map[Identifier, Z3FuncDecl]
protected[purescala] var exprToZ3Id : Map[Expr,Z3AST]
protected[purescala] def fromZ3Formula(tree : Z3AST) : Expr
......@@ -22,4 +32,50 @@ trait AbstractZ3Solver {
case _ => None
}
}
protected[purescala] def solveWithBounds(vc: Expr, forValidity: Boolean) : (Option[Boolean], Map[Identifier, Expr])
protected[purescala] def boundValues : Unit = {
val lowerBound: Z3AST = z3.mkInt(Settings.testBounds._1, z3.mkIntSort)
val upperBound: Z3AST = z3.mkInt(Settings.testBounds._2, z3.mkIntSort)
def isUnbounded(field: VarDecl) : Boolean = field.getType match {
case Int32Type => true
case _ => false
}
def boundConstraint(boundVar: Z3AST) : Z3AST = {
lowerBound <= boundVar && boundVar <= upperBound
}
// for all recursive type roots
// for all child ccd of a root
// if ccd contains unbounded types
// create bound vars (mkBound) for each field
// create pattern that says (valueBounds(ccd(f1, ..)))
// create axiom tree that says "values of unbounded types are within bounds"
// assert axiom for the tree above
val roots = program.classHierarchyRoots
for (root <- roots) {
val children: List[CaseClassDef] = (root match {
case c: CaseClassDef => List(c)
case a: AbstractClassDef => a.knownChildren.filter(_.isInstanceOf[CaseClassDef]).map(_.asInstanceOf[CaseClassDef]).toList
})
for (child <- children) child match {
case CaseClassDef(id, parent, fields) =>
val unboundedFields = fields.filter(isUnbounded(_))
if (!unboundedFields.isEmpty) {
val boundVars = fields.zipWithIndex.map{case (f, i) => z3.mkBound(i, typeToSort(f.getType))}
val term = adtConstructors(child)(boundVars : _*)
val pattern = z3.mkPattern(term)
//val constraint = (fields zip boundVars).filter((p: (VarDecl, Z3AST)) => isUnbounded(p._1)).map((p: (VarDecl, Z3AST)) => boundConstraint(p._2)).foldLeft(z3.mkTrue)((a, b) => a && b)
val constraint = (fields zip boundVars).filter((p: (VarDecl, Z3AST)) => isUnbounded(p._1)).map((p: (VarDecl, Z3AST)) => boundConstraint(adtFieldSelectors(p._1.id)(term))).foldLeft(z3.mkTrue)((a, b) => a && b)
val axiom = z3.mkForAll(0, List(pattern), fields.zipWithIndex.map{case (f, i) => (z3.mkIntSymbol(i), typeToSort(f.getType))}, constraint)
println("Asserting: " + axiom)
z3.assertCnstr(axiom)
}
}
}
}
}
......@@ -13,6 +13,8 @@ import scala.collection.mutable.{Set => MutableSet}
class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3Solver with Z3ModelReconstruction {
assert(Settings.useFairInstantiator)
private final val UNKNOWNASSAT : Boolean = true
val description = "Fair Z3 Solver"
override val shortDescription = "Z3-f"
......@@ -70,9 +72,9 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
private var adtSorts: Map[ClassTypeDef, Z3Sort] = Map.empty
private var fallbackSorts: Map[TypeTree, Z3Sort] = Map.empty
private var adtTesters: Map[CaseClassDef, Z3FuncDecl] = Map.empty
private var adtConstructors: Map[CaseClassDef, Z3FuncDecl] = Map.empty
private var adtFieldSelectors: Map[Identifier, Z3FuncDecl] = Map.empty
protected[purescala] var adtTesters: Map[CaseClassDef, Z3FuncDecl] = Map.empty
protected[purescala] var adtConstructors: Map[CaseClassDef, Z3FuncDecl] = Map.empty
protected[purescala] var adtFieldSelectors: Map[Identifier, Z3FuncDecl] = Map.empty
private var reverseADTTesters: Map[Z3FuncDecl, CaseClassDef] = Map.empty
private var reverseADTConstructors: Map[Z3FuncDecl, CaseClassDef] = Map.empty
......@@ -224,10 +226,19 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
def solve(vc: Expr) = decide(vc, true)
def decide(vc: Expr, forValidity: Boolean):Option[Boolean] = decideWithModel(vc, forValidity)._1
def decideWithModel(vc: Expr, forValidity: Boolean): (Option[Boolean], Map[Identifier,Expr]) = {
def solveWithBounds(vc: Expr, fv: Boolean) : (Option[Boolean], Map[Identifier,Expr]) = {
restartZ3
boundValues
println(z3.check)
decideWithModel(vc, fv)
}
def decide(vc: Expr, forValidity: Boolean):Option[Boolean] = {
restartZ3
decideWithModel(vc, forValidity)._1
}
def decideWithModel(vc: Expr, forValidity: Boolean): (Option[Boolean], Map[Identifier,Expr]) = {
val unrollingBank = new UnrollingBank
lazy val varsInVC = variablesOf(vc)
......@@ -276,6 +287,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
z3.assertCnstr(z3.mkAnd(blockingSetAsZ3 : _*))
}
reporter.info(" - Running Z3 search...")
val (answer, model, core) : (Option[Boolean], Z3Model, Seq[Z3AST]) = if(Settings.useCores) {
println(blockingSetAsZ3)
z3.checkAssumptions(blockingSetAsZ3 : _*)
......@@ -284,8 +296,12 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
(a, m, Seq.empty[Z3AST])
}
reporter.info(" - Running Z3 search...")
(answer, model) match {
val reinterpretedAnswer = if(!UNKNOWNASSAT) answer else (answer match {
case None | Some(true) => Some(true)
case Some(false) => Some(false)
})
(reinterpretedAnswer, model) match {
case (None, m) => { // UNKNOWN
reporter.warning("Z3 doesn't know because: " + z3.getSearchFailure.message)
foundDefinitiveAnswer = true
......@@ -428,6 +444,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
definitiveAnswer = None
definitiveModel = Map.empty
reporter.error("Max. number of iterations reached.")
println("Max. number of iterations reached.")
}
}
......
......@@ -83,9 +83,9 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3S
private var adtSorts: Map[ClassTypeDef, Z3Sort] = Map.empty
private var fallbackSorts: Map[TypeTree, Z3Sort] = Map.empty
private var adtTesters: Map[CaseClassDef, Z3FuncDecl] = Map.empty
private var adtConstructors: Map[CaseClassDef, Z3FuncDecl] = Map.empty
private var adtFieldSelectors: Map[Identifier, Z3FuncDecl] = Map.empty
protected[purescala] var adtTesters: Map[CaseClassDef, Z3FuncDecl] = Map.empty
protected[purescala] var adtConstructors: Map[CaseClassDef, Z3FuncDecl] = Map.empty
protected[purescala] var adtFieldSelectors: Map[Identifier, Z3FuncDecl] = Map.empty
private var reverseADTTesters: Map[Z3FuncDecl, CaseClassDef] = Map.empty
private var reverseADTConstructors: Map[Z3FuncDecl, CaseClassDef] = Map.empty
......@@ -175,46 +175,6 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3S
// ...and now everything should be in there...
}
private def boundValues : Unit = {
val lowerBound: Z3AST = z3.mkInt(Settings.testBounds._1, z3.mkIntSort)
val upperBound: Z3AST = z3.mkInt(Settings.testBounds._2, z3.mkIntSort)
def isUnbounded(field: VarDecl) : Boolean = field.getType match {
case Int32Type => true
case _ => false
}
def boundConstraint(boundVar: Z3AST) : Z3AST = {
lowerBound <= boundVar && boundVar <= upperBound
}
// for all recursive type roots
// for all child ccd of a root
// if ccd contains unbounded types
// create bound vars (mkBound) for each field
// create pattern that says (valueBounds(ccd(f1, ..)))
// create axiom tree that says "values of unbounded types are within bounds"
// assert axiom for the tree above
val roots = program.classHierarchyRoots
for (root <- roots) {
val children: List[CaseClassDef] = (root match {
case c: CaseClassDef => List(c)
case a: AbstractClassDef => a.knownChildren.filter(_.isInstanceOf[CaseClassDef]).map(_.asInstanceOf[CaseClassDef]).toList
})
for (child <- children) child match {
case CaseClassDef(id, parent, fields) =>
val unboundedFields = fields.filter(isUnbounded(_))
if (!unboundedFields.isEmpty) {
val boundVars = fields.zipWithIndex.map{case (f, i) => z3.mkBound(i, typeToSort(f.getType))}
val pattern = z3.mkPattern(adtConstructors(child)(boundVars: _*))
val constraint = (fields zip boundVars).filter((p: (VarDecl, Z3AST)) => isUnbounded(p._1)).map((p: (VarDecl, Z3AST)) => boundConstraint(p._2)).foldLeft(z3.mkTrue)((a, b) => a && b)
val axiom = z3.mkForAll(0, List(pattern), fields.zipWithIndex.map{case (f, i) => (z3.mkIntSymbol(i), typeToSort(f.getType))}, constraint)
z3.assertCnstr(axiom)
}
}
}
}
def isKnownDef(funDef: FunDef) : Boolean = if(useAnyInstantiator) {
instantiator.isKnownDef(funDef)
......@@ -456,6 +416,8 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3S
decideIterativeWithModel(vc, forValidity)._1
}
def solveWithBounds(vc: Expr, fv: Boolean) : (Option[Boolean], Map[Identifier,Expr]) = decideIterativeWithBounds(vc, fv)
def decideIterativeWithBounds(vc: Expr, forValidity: Boolean) : (Option[Boolean], Map[Identifier, Expr]) = {
restartZ3
boundValues
......
......@@ -19,7 +19,11 @@ class Main(reporter : Reporter) extends Analyser(reporter) {
reporter.info("Running testcase generation...")
val solver = new purescala.Z3Solver(reporter)
val solver = if(Settings.useFairInstantiator) {
new purescala.FairZ3Solver(reporter)
} else {
new purescala.Z3Solver(reporter)
}
solver.setProgram(program)
def writeToFile(filename: String, content: String) : Unit = {
......@@ -39,7 +43,7 @@ class Main(reporter : Reporter) extends Analyser(reporter) {
var noMoreModels = false
for (i <- 1 to Settings.nbTestcases if !noMoreModels) {
// reporter.info("Current constraints: " + constraints)
val argMap = solver.decideIterativeWithBounds(And(prec, constraints), false)
val argMap = solver.solveWithBounds(And(prec, constraints), false)
argMap match {
case (Some(true), _) => noMoreModels = true
case (_ , map) =>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment