diff --git a/src/main/scala/purescala/Extensions.scala b/src/main/scala/purescala/Extensions.scala index 3ae3c0de46cd66efdc0b1c3558274c04cac8edd4..8bc5a4c4673c0688ea9a1364dc02b5af18dddb67 100644 --- a/src/main/scala/purescala/Extensions.scala +++ b/src/main/scala/purescala/Extensions.scala @@ -90,17 +90,12 @@ object Extensions { } // these extensions are always loaded, unless specified otherwise val defaultExtensions: Seq[Extension] = if(Settings.runDefaultExtensions) { - val z3s : Solver = (if(Settings.useFairInstantiator) { - (new FairZ3Solver(extensionsReporter)) - } else { - (new Z3Solver(extensionsReporter)) - }) - z3s :: Nil + val z3 : Solver = new FairZ3Solver(extensionsReporter) + z3 :: Nil } else { Nil } - allLoaded = defaultExtensions ++ loaded analysisExtensions = allLoaded.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser]) diff --git a/src/main/scala/purescala/Settings.scala b/src/main/scala/purescala/Settings.scala index e2be9ef6e4a5fc8ac7763d43b6bc00eb834acea2..914f9c0bd51f61514d49c9ea001f9f6d2ff5f480 100644 --- a/src/main/scala/purescala/Settings.scala +++ b/src/main/scala/purescala/Settings.scala @@ -15,11 +15,8 @@ object Settings { var impureTestcases: Boolean = false var nbTestcases: Int = 1 var testBounds: (Int, Int) = (0, 3) - var useInstantiator: Boolean = false - var useFairInstantiator: Boolean = true var useCores : Boolean = false var pruneBranches : Boolean = false - def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator var solverTimeout : Option[Int] = None var luckyTest : Boolean = true var useQuickCheck : Boolean = false diff --git a/src/main/scala/purescala/Z3Solver.scala b/src/main/scala/purescala/Z3Solver.scala deleted file mode 100644 index 80cf41defa936fcba933fc3e2fed2d95110af9e6..0000000000000000000000000000000000000000 --- a/src/main/scala/purescala/Z3Solver.scala +++ /dev/null @@ -1,795 +0,0 @@ -package purescala - -import z3.scala._ -import Common._ -import Definitions._ -import Extensions._ -import Trees._ -import TypeTrees._ - -import z3plugins.bapa.{BAPATheory, BAPATheoryEqc, BAPATheoryBubbles} -import z3plugins.instantiator.{AbstractInstantiator,Instantiator} - -import scala.collection.mutable.{HashMap => MutableHashMap} -import scala.collection.mutable.{Map => MutableMap} -import scala.collection.mutable.{Set => MutableSet} - -class Z3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3Solver with Z3ModelReconstruction { - import Settings.useBAPA - import Settings.{useInstantiator,useFairInstantiator,useAnyInstantiator} - - val description = "Z3 Solver" - override val shortDescription = "Z3" - - // type BAPATheoryType = BAPATheory - // type BAPATheoryType = BAPATheoryEqc - type BAPATheoryType = BAPATheoryBubbles - - private val reportUnknownAsSat = true - - // this is fixed - private val z3cfg = new Z3Config( - "MODEL" -> true, - "MBQI" -> false, - //"SOFT_TIMEOUT" -> 100, - "TYPE_CHECK" -> true, - "WELL_SORTED_CHECK" -> true - ) - toggleWarningMessages(true) - - protected[purescala] var z3: Z3Context = null - protected[purescala] var program: Program = null - private var bapa: BAPATheoryType = null - private var instantiator: AbstractInstantiator = null - private var neverInitialized = true - - private val IntSetType = SetType(Int32Type) - - override def setProgram(prog: Program): Unit = { - program = prog - } - - private def restartZ3: Unit = { - if (neverInitialized) { - neverInitialized = false - } else { - z3.delete - } - z3 = new Z3Context(z3cfg) - // z3.traceToStdout - if (useBAPA) bapa = new BAPATheoryType(z3) - if (useInstantiator) instantiator = new Instantiator(this) else - if (useFairInstantiator) instantiator = { - scala.sys.error("Z3Solver should not be used with FairInst. FairZ3Solver should be used instead.") - } - - exprToZ3Id = Map.empty - z3IdToExpr = Map.empty - counter = 0 - prepareSorts - prepareFunctions - } - - private var counter = 0 - private object nextIntForSymbol { - def apply(): Int = { - val res = counter - counter = counter + 1 - res - } - } - - private var intSort: Z3Sort = null - private var boolSort: Z3Sort = null - private var setSorts: Map[TypeTree, Z3Sort] = Map.empty - private var intSetMinFun: Z3FuncDecl = null - private var intSetMaxFun: Z3FuncDecl = null - private var setCardFuns: Map[TypeTree, Z3FuncDecl] = Map.empty - private var adtSorts: Map[ClassTypeDef, Z3Sort] = Map.empty - private var fallbackSorts: Map[TypeTree, Z3Sort] = 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 - private var reverseADTFieldSelectors: Map[Z3FuncDecl, (CaseClassDef,Identifier)] = Map.empty - - protected[purescala] val mapRangeSorts: MutableMap[TypeTree, Z3Sort] = MutableMap.empty - protected[purescala] val mapRangeSomeConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty - protected[purescala] val mapRangeNoneConstructors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty - protected[purescala] val mapRangeSomeTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty - protected[purescala] val mapRangeNoneTesters: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty - protected[purescala] val mapRangeValueSelectors: MutableMap[TypeTree, Z3FuncDecl] = MutableMap.empty - - protected[purescala] var funSorts: Map[TypeTree, Z3Sort] = Map.empty - protected[purescala] var funDomainConstructors: Map[TypeTree, Z3FuncDecl] = Map.empty - protected[purescala] var funDomainSelectors: Map[TypeTree, Seq[Z3FuncDecl]] = Map.empty - - case class UntranslatableTypeException(msg: String) extends Exception(msg) - private def prepareSorts: Unit = { - import Z3Context.{ADTSortReference, RecursiveType, RegularSort} - // NOTE THAT abstract classes that extend abstract classes are not - // currently supported in the translation - intSort = z3.mkIntSort - boolSort = z3.mkBoolSort - setSorts = Map.empty - setCardFuns = Map.empty - - val intSetSort = typeToSort(SetType(Int32Type)) - intSetMinFun = z3.mkFreshFuncDecl("setMin", Seq(intSetSort), intSort) - intSetMaxFun = z3.mkFreshFuncDecl("setMax", Seq(intSetSort), intSort) - - val roots = program.classHierarchyRoots - val indexMap: Map[ClassTypeDef, Int] = Map(roots.zipWithIndex: _*) - //println("indexMap: " + indexMap) - - def typeToSortRef(tt: TypeTree): ADTSortReference = tt match { - case BooleanType => RegularSort(boolSort) - case Int32Type => RegularSort(intSort) - case AbstractClassType(d) => RecursiveType(indexMap(d)) - case CaseClassType(d) => indexMap.get(d) match { - case Some(i) => RecursiveType(i) - case None => RecursiveType(indexMap(d.parent.get)) - } - case _ => throw UntranslatableTypeException("Can't handle type " + tt) - } - - val childrenLists: Seq[List[CaseClassDef]] = roots.map(_ match { - case c: CaseClassDef => List(c) - case a: AbstractClassDef => a.knownChildren.filter(_.isInstanceOf[CaseClassDef]).map(_.asInstanceOf[CaseClassDef]).toList - }) - //println("children lists: " + childrenLists.toList.mkString("\n")) - - val rootsAndChildren = (roots zip childrenLists) - - val defs = rootsAndChildren.map(p => { - val (root, childrenList) = p - - root match { - case c: CaseClassDef => { - // we create a recursive type with exactly one constructor - (c.id.uniqueName, List(c.id.uniqueName), List(c.fields.map(f => (f.id.uniqueName, typeToSortRef(f.tpe))))) - } - case a: AbstractClassDef => { - (a.id.uniqueName, childrenList.map(ccd => ccd.id.uniqueName), childrenList.map(ccd => ccd.fields.map(f => (f.id.uniqueName, typeToSortRef(f.tpe))))) - } - } - }) - - //println(defs) - // everything should be alright now... - val resultingZ3Info = z3.mkADTSorts(defs) - - adtSorts = Map.empty - adtTesters = Map.empty - adtConstructors = Map.empty - adtFieldSelectors = Map.empty - reverseADTTesters = Map.empty - reverseADTConstructors = Map.empty - reverseADTFieldSelectors = Map.empty - - for ((z3Inf, (root, childrenList)) <- (resultingZ3Info zip rootsAndChildren)) { - adtSorts += (root -> z3Inf._1) - assert(childrenList.size == z3Inf._2.size) - for ((child, (consFun, testFun)) <- childrenList zip (z3Inf._2 zip z3Inf._3)) { - adtTesters += (child -> testFun) - adtConstructors += (child -> consFun) - } - for ((child, fieldFuns) <- childrenList zip z3Inf._4) { - assert(child.fields.size == fieldFuns.size) - for ((fid, selFun) <- (child.fields.map(_.id) zip fieldFuns)) { - adtFieldSelectors += (fid -> selFun) - reverseADTFieldSelectors += (selFun -> (child, fid)) - } - } - } - - reverseADTTesters = adtTesters.map(_.swap) - reverseADTConstructors = adtConstructors.map(_.swap) - // ...and now everything should be in there... - } - - - def isKnownDef(funDef: FunDef) : Boolean = if(useAnyInstantiator) { - instantiator.isKnownDef(funDef) - } else { - functionMap.isDefinedAt(funDef) - } - def functionDefToDecl(funDef: FunDef) : Z3FuncDecl = { - if(useAnyInstantiator) { - instantiator.functionDefToDecl(funDef) - } else { - functionMap.getOrElse(funDef, scala.sys.error("No Z3 definition found for function symbol " + funDef.id.name + ". (Instantiator is off).")) - } - } - def isKnownDecl(decl: Z3FuncDecl) : Boolean = if(useAnyInstantiator) { - instantiator.isKnownDecl(decl) - } else { - reverseFunctionMap.isDefinedAt(decl) - } - def functionDeclToDef(decl: Z3FuncDecl) : FunDef = { - if(useAnyInstantiator) { - instantiator.functionDeclToDef(decl) - } else { - reverseFunctionMap.getOrElse(decl, scala.sys.error("No FunDef corresponds to Z3 definition " + decl + ". (Instantiator is off).")) - } - } - private var functionMap: Map[FunDef, Z3FuncDecl] = Map.empty - private var reverseFunctionMap: Map[Z3FuncDecl, FunDef] = Map.empty - - def prepareFunctions: Unit = { - for (funDef <- program.definedFunctions) { - val sortSeq = funDef.args.map(vd => typeToSort(vd.tpe)) - val returnSort = typeToSort(funDef.returnType) - - if(useAnyInstantiator) { - instantiator.registerFunction(funDef, sortSeq, returnSort) - } else { - val z3Decl = z3.mkFreshFuncDecl(funDef.id.name, sortSeq, returnSort) - functionMap = functionMap + (funDef -> z3Decl) - reverseFunctionMap = reverseFunctionMap + (z3Decl -> funDef) - } - } - - // Attempts to universally quantify all functions ! - if (!Settings.noForallAxioms && !Settings.useAnyInstantiator) { - for (funDef <- program.definedFunctions) if (funDef.hasImplementation /* && program.isRecursive(funDef) */ && funDef.args.size > 0) { - // println("Generating forall axioms for " + funDef.id.name) - funDef.body.get match { - case SimplePatternMatching(scrutinee, _, infos) if ( - funDef.args.size >= 1 && funDef.args.map(_.toVariable).contains(scrutinee) - ) => { - infos.foreach(i => if (!contains(i._4, _.isInstanceOf[MatchExpr])) { - val argsAsVars: Seq[Option[Variable]] = funDef.args.map(a => { - val v = a.toVariable - if (v == scrutinee) - None - else - Some(v) - }) - val otherFunIDs: Seq[Option[Identifier]] = argsAsVars.map(_.map(_.id)) - val otherFunSorts: Seq[Option[Z3Sort]] = argsAsVars.map(_.map(v => typeToSort(v.getType))) - var c = -1 - val otherFunBounds: Seq[Option[Z3AST]] = for (os <- otherFunSorts) yield { - os match { - case None => None - case Some(s) => { - c = c + 1 - Some(z3.mkBound(c, s)) - } - } - } - val (ccd, pid, subids, dirtyRHS) = i - val cleanRHS = matchToIfThenElse(dirtyRHS) - val argSorts: Seq[Z3Sort] = subids.map(id => typeToSort(id.getType)) - val boundVars = argSorts.zip((c + 1) until (c + 1 + argSorts.size)).map(p => z3.mkBound(p._2, p._1)) - val matcher: Z3AST = adtConstructors(ccd)(boundVars: _*) - val pattern: Z3Pattern = z3.mkPattern(functionDefToDecl(funDef)( - otherFunBounds.map(_ match { - case None => matcher - case Some(b) => b - }): _*)) - - val fOfT: Expr = FunctionInvocation(funDef, - argsAsVars.map(_ match { - case None => CaseClass(ccd, subids.map(Variable(_))) - case Some(v) => v - })) - - val toConvert = Equals(fOfT, cleanRHS) - //println(toConvert) - val initialMap: Map[Identifier,Z3AST] = - Map((funDef.args.map(_.id) zip otherFunBounds).map(_ match { - case (i, Some(b)) => (i -> b) - case (i, None) => (i -> matcher) - }): _*) ++ - Map((subids zip boundVars): _*) + (pid -> matcher) - - toZ3Formula(z3, toConvert, initialMap) match { - case Some(axiomTree) => { - val toAssert = if (boundVars.size == 0 && otherFunBounds.flatten.size == 0) { - axiomTree - } else { - val nameTypePairs = (otherFunSorts.flatten ++ argSorts).map(s => (z3.mkIntSymbol(nextIntForSymbol()), s)) - z3.mkForAll(0, List(pattern), nameTypePairs, axiomTree) - } - //println("Cool axiom: " + toAssert) - z3.assertCnstr(toAssert) - } - case None => { - reporter.warning("Could not convert to axiom:") - reporter.warning(toConvert) - } - } - }) - } - case _ => { - // we don't generate axioms that are not simple. - } - } - } - } - } - - // assumes prepareSorts has been called.... - def typeToSort(tt: TypeTree): Z3Sort = tt match { - case Int32Type => intSort - case BooleanType => boolSort - case AbstractClassType(cd) => adtSorts(cd) - case CaseClassType(cd) => { - if (cd.hasParent) { - adtSorts(cd.parent.get) - } else { - adtSorts(cd) - } - } - case IntSetType if (useBAPA) => bapa.mkSetSort - case SetType(base) => setSorts.get(base) match { - case Some(s) => s - case None => { - val newSetSort = z3.mkSetSort(typeToSort(base)) - setSorts = setSorts + (base -> newSetSort) - val newCardFun = z3.mkFreshFuncDecl("card", Seq(newSetSort), z3.mkIntSort) - setCardFuns = setCardFuns + (base -> newCardFun) - newSetSort - } - } - case other => fallbackSorts.get(other) match { - case Some(s) => s - case None => { - reporter.warning("Resorting to uninterpreted type for : " + other) - val symbol = z3.mkIntSymbol(nextIntForSymbol()) - val newFBSort = z3.mkUninterpretedSort(symbol) - fallbackSorts = fallbackSorts + (other -> newFBSort) - newFBSort - } - } - } - - private var abstractedFormula = false - - override def isUnsat(vc: Expr) = decide(vc, false) - - def solve(vc: Expr) = decide(vc, true) - - def decide(vc: Expr, fv: Boolean) : Option[Boolean] = if(Settings.useAnyInstantiator) { - decideIterative(vc, fv) - } else { - decideStandard(vc, fv) - } - - def decideStandard(vc: Expr, forValidity: Boolean): Option[Boolean] = { - restartZ3 - abstractedFormula = false - - 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 result = toZ3Formula(z3, toConvert) match { - case None => None // means it could not be translated - case Some(z3f) => { - //z3.push - z3.assertCnstr(z3f) - //z3.print - val actualResult = (z3.checkAndGetModel() match { - case (Some(true), m) => { - if (!abstractedFormula) { - reporter.error("There's a bug!") - if(Settings.experimental) { - reporter.error(m) - printExtractedModel(m, varsInVC) - if(useBAPA) { - reporter.error(bapa.toBapaModel(m)) - } - } - Some(false) - } else { - reporter.info("Could or could not be a bug (formula was relaxed).") - if(Settings.experimental) { - reporter.info(m) - printExtractedModel(m, varsInVC) - if(useBAPA) { - reporter.error(bapa.toBapaModel(m)) - } - } - if(reportUnknownAsSat) { - Some(false) - } else { - None - } - } - } - case (Some(false), _) => Some(true) - case (None, m) => { - reporter.warning("Z3 doesn't know because: " + z3.getSearchFailure.message) - if(Settings.experimental) { - reporter.info(m) - } else { - if (useBAPA) reporter.error(bapa.toBapaModel(m)) - } - if(reportUnknownAsSat) { - Some(false) - } else { - None - } - } - }) - //z3.pop(1) - actualResult - } - } - result - } - - def decideIterative(vc: Expr, forValidity: Boolean) : Option[Boolean] = { - restartZ3 - 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 - decideIterativeWithModel(vc, forValidity) - } - - def decideIterativeWithModel(vc: Expr, forValidity: Boolean) : (Option[Boolean], Map[Identifier, Expr]) = { - 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 : (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) - - // THE LOOP STARTS HERE. - var foundDefinitiveSolution : Boolean = false - var finalResult : (Option[Boolean], Map[Identifier, Expr]) = (None, Map.empty) - - while(!foundDefinitiveSolution && instantiator.possibleContinuation) { - instantiator.increaseSearchDepth() - z3.checkAndGetModel() match { - case (Some(false), _) => { - // This means a definitive proof of unsatisfiability has been found. - foundDefinitiveSolution = true - finalResult = (Some(true), Map.empty) - } - - case (outcome, m) if (reportUnknownAsSat || outcome == Some(true)) => { - 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) - - - //println("(I'm going to pretend this never happened...)") - - val evalResult = eval(asMap, toCheckAgainstModels, None) - - - evalResult match { - case OK(BooleanLiteral(true)) => { - reporter.error("Counter-example found and confirmed:") - reporter.error(modelAsString) - foundDefinitiveSolution = true - finalResult = (Some(false), asMap) - } - case InfiniteComputation() => { - reporter.info("Model seems to lead to divergent computation.") - reporter.error(modelAsString) - foundDefinitiveSolution = true - finalResult = (None, asMap) - } - case RuntimeError(msg) => { - reporter.info("Model leads to runtime error: " + msg) - reporter.error(modelAsString) - foundDefinitiveSolution = true - finalResult = (Some(false), asMap) - } - case t @ TypeError(_,_) => { - scala.sys.error("Type error in model evaluation.\n" + t.msg) - } - case _ => { - reporter.info(" -> candidate model discarded.") - } - } - - m.delete - } - - case (None, m) => { - reporter.warning("Iterative Z3 gave up because: " + z3.getSearchFailure.message) - foundDefinitiveSolution = true - finalResult = (None, modelToMap(m, varsInVC)) - m.delete - } - } - } - finalResult - } - } - result - } - - protected[purescala] var exprToZ3Id : Map[Expr,Z3AST] = Map.empty - protected[purescala] var z3IdToExpr : Map[Z3AST,Expr] = Map.empty - protected[purescala] def toZ3Formula(z3: Z3Context, expr: Expr, initialMap: Map[Identifier,Z3AST] = Map.empty): Option[Z3AST] = { - class CantTranslateException extends Exception - - val varsInformula: Set[Identifier] = variablesOf(expr) - - var z3Vars: Map[Identifier,Z3AST] = if(!initialMap.isEmpty) { - initialMap - } else { - // FIXME TODO pleeeeeeeease make this cleaner. Ie. decide what set of - // variable has to remain in a map etc. - exprToZ3Id.filter(p => p._1.isInstanceOf[Variable]).map(p => (p._1.asInstanceOf[Variable].id -> p._2)) - } - // exprToZ3Id = Map.empty - // z3IdToExpr = Map.empty - - for((k, v) <- initialMap) { - exprToZ3Id += (k.toVariable -> v) - z3IdToExpr += (v -> k.toVariable) - } - - def rec(ex: Expr): Z3AST = { - //println("Stacking up call for:") - //println(ex) - val recResult = (ex match { - case Let(i, e, b) => { - val re = rec(e) - z3Vars = z3Vars + (i -> re) - val rb = rec(b) - z3Vars = z3Vars - i - rb - } - case e @ Error(_) => { - val tpe = e.getType - val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe)) - exprToZ3Id += (e -> newAST) - z3IdToExpr += (newAST -> e) - newAST - } - case v@Variable(id) => z3Vars.get(id) match { - case Some(ast) => ast - case None => { - if (id.isLetBinder) { - //scala.sys.error("Error in formula being translated to Z3: identifier " + id + " seems to have escaped its let-definition") - } - val newAST = z3.mkFreshConst(id.name, typeToSort(v.getType)) - z3Vars = z3Vars + (id -> newAST) - exprToZ3Id += (v -> newAST) - z3IdToExpr += (newAST -> v) - newAST - } - } - case IfExpr(c, t, e) => z3.mkITE(rec(c), rec(t), rec(e)) - case And(exs) => z3.mkAnd(exs.map(rec(_)): _*) - case Or(exs) => z3.mkOr(exs.map(rec(_)): _*) - case Implies(l, r) => z3.mkImplies(rec(l), rec(r)) - case Iff(l, r) => { - val rl = rec(l) - val rr = rec(r) - z3.mkAnd(z3.mkImplies(rl, rr), z3.mkImplies(rr, rl)) - } - case Not(Iff(l, r)) => z3.mkXor(rec(l), rec(r)) - case Not(Equals(l, r)) => z3.mkDistinct(rec(l), rec(r)) - case Not(e) => z3.mkNot(rec(e)) - case IntLiteral(v) => z3.mkInt(v, intSort) - case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse() - case Equals(l, r) => z3.mkEq(rec(l), rec(r)) - case Plus(l, r) => z3.mkAdd(rec(l), rec(r)) - case Minus(l, r) => z3.mkSub(rec(l), rec(r)) - case Times(l, r) => z3.mkMul(rec(l), rec(r)) - case Division(l, r) => z3.mkDiv(rec(l), rec(r)) - case UMinus(e) => z3.mkUnaryMinus(rec(e)) - case LessThan(l, r) => z3.mkLT(rec(l), rec(r)) - case LessEquals(l, r) => z3.mkLE(rec(l), rec(r)) - case GreaterThan(l, r) => z3.mkGT(rec(l), rec(r)) - case GreaterEquals(l, r) => z3.mkGE(rec(l), rec(r)) - case c@CaseClass(cd, args) => { - val constructor = adtConstructors(cd) - constructor(args.map(rec(_)): _*) - } - case c@CaseClassSelector(_, cc, sel) => { - val selector = adtFieldSelectors(sel) - selector(rec(cc)) - } - case c@CaseClassInstanceOf(ccd, e) => { - val tester = adtTesters(ccd) - tester(rec(e)) - } - case f@FunctionInvocation(fd, args) => { - z3.mkApp(functionDefToDecl(fd), args.map(rec(_)): _*) - } - case e@EmptySet(_) => if (useBAPA && e.getType == IntSetType) { - bapa.mkEmptySet - } else { - z3.mkEmptySet(typeToSort(e.getType.asInstanceOf[SetType].base)) - } - case SetEquals(s1, s2) => z3.mkEq(rec(s1), rec(s2)) - case ElementOfSet(e, s) => if (useBAPA && s.getType == IntSetType) { - bapa.mkElementOf(rec(e), rec(s)) - } else { - z3.mkSetSubset(z3.mkSetAdd(z3.mkEmptySet(typeToSort(e.getType)), rec(e)), rec(s)) - } - case SubsetOf(s1, s2) => if (useBAPA && s1.getType == IntSetType) { - bapa.mkSubsetEq(rec(s1), rec(s2)) - } else { - z3.mkSetSubset(rec(s1), rec(s2)) - } - case SetIntersection(s1, s2) => if (useBAPA && s1.getType == IntSetType) { - bapa.mkIntersect(rec(s1), rec(s2)) - } else { - z3.mkSetIntersect(rec(s1), rec(s2)) - } - case SetUnion(s1, s2) => if (useBAPA && s1.getType == IntSetType) { - bapa.mkUnion(rec(s1), rec(s2)) - } else { - z3.mkSetUnion(rec(s1), rec(s2)) - } - case SetDifference(s1, s2) => if (useBAPA && s1.getType == IntSetType) { - bapa.mkIntersect(rec(s1), bapa.mkComplement(rec(s2))) - } else { - z3.mkSetDifference(rec(s1), rec(s2)) - } - case f@FiniteSet(elems) => if (useBAPA && f.getType == IntSetType) { - elems.map(e => bapa.mkSingleton(rec(e))).reduceLeft(bapa.mkUnion(_, _)) - } else { - elems.foldLeft(z3.mkEmptySet(typeToSort(f.getType.asInstanceOf[SetType].base)))((ast, el) => z3.mkSetAdd(ast, rec(el))) - } - case SetCardinality(s) => if (useBAPA && s.getType == IntSetType) { - bapa.mkCard(rec(s)) - } else { - val rs = rec(s) - setCardFuns(s.getType.asInstanceOf[SetType].base)(rs) - } - case SetMin(s) => intSetMinFun(rec(s)) - case SetMax(s) => intSetMaxFun(rec(s)) - - case _ => { - reporter.warning("Can't handle this in translation to Z3: " + ex) - throw new CantTranslateException - } - }) - // println("Encoding of:") - // println(ex) - // println("...was encoded as:") - // println(recResult) - recResult - } - - try { - val res = Some(rec(expr)) - // val usedInZ3Form = z3Vars.keys.toSet - // println("Variables in formula: " + varsInformula.map(_.uniqueName)) - // println("Variables passed to Z3: " + usedInZ3Form.map(_.uniqueName)) - res - } catch { - case e: CantTranslateException => None - } - } - - protected[purescala] def fromZ3Formula(model: Z3Model, tree : Z3AST, expectedType: Option[TypeTree] = None) : Expr = { - def rec(t: Z3AST) : Expr = z3.getASTKind(t) match { - case Z3AppAST(decl, args) => { - val argsSize = args.size - if(argsSize == 0 && z3IdToExpr.isDefinedAt(t)) { - val toRet = z3IdToExpr(t) - // println("Map says I should replace " + t + " by " + toRet) - toRet - } else if(isKnownDecl(decl)) { - val fd = functionDeclToDef(decl) - assert(fd.args.size == argsSize) - FunctionInvocation(fd, args.map(rec(_))) - } else if(argsSize == 1 && reverseADTTesters.isDefinedAt(decl)) { - CaseClassInstanceOf(reverseADTTesters(decl), rec(args(0))) - } else if(argsSize == 1 && reverseADTFieldSelectors.isDefinedAt(decl)) { - val (ccd, fid) = reverseADTFieldSelectors(decl) - CaseClassSelector(ccd, rec(args(0)), fid) - } else if(reverseADTConstructors.isDefinedAt(decl)) { - val ccd = reverseADTConstructors(decl) - assert(argsSize == ccd.fields.size) - CaseClass(ccd, args.map(rec(_))) - } else { - import Z3DeclKind._ - val rargs = args.map(rec(_)) - z3.getDeclKind(decl) match { - case OpTrue => BooleanLiteral(true) - case OpFalse => BooleanLiteral(false) - case OpEq => Equals(rargs(0), rargs(1)) - case OpITE => { - assert(argsSize == 3) - val r0 = rargs(0) - val r1 = rargs(1) - val r2 = rargs(2) - try { - IfExpr(r0, r1, r2).setType(leastUpperBound(r1.getType, r2.getType)) - } catch { - case e => { - println("I was asking for lub because of this.") - println(t) - println("which was translated as") - println(IfExpr(r0,r1,r2)) - throw e - } - } - } - case OpAnd => And(rargs) - case OpOr => Or(rargs) - case OpIff => Iff(rargs(0), rargs(1)) - case OpXor => Not(Iff(rargs(0), rargs(1))) - case OpNot => Not(rargs(0)) - case OpImplies => Implies(rargs(0), rargs(1)) - case OpLE => LessEquals(rargs(0), rargs(1)) - case OpGE => GreaterEquals(rargs(0), rargs(1)) - case OpLT => LessThan(rargs(0), rargs(1)) - case OpGT => GreaterThan(rargs(0), rargs(1)) - case OpAdd => { - assert(argsSize == 2) - Plus(rargs(0), rargs(1)) - } - case OpSub => { - assert(argsSize == 2) - Minus(rargs(0), rargs(1)) - } - case OpUMinus => UMinus(rargs(0)) - case OpMul => { - assert(argsSize == 2) - Times(rargs(0), rargs(1)) - } - case OpDiv => { - assert(argsSize == 2) - Division(rargs(0), rargs(1)) - } - case OpIDiv => { - assert(argsSize == 2) - Division(rargs(0), rargs(1)) - } - case other => { - System.err.println("Don't know what to do with this declKind : " + other) - throw new CantTranslateException(t) - } - } - } - } - - case Z3NumeralAST(Some(v)) => IntLiteral(v) - case other @ _ => { - System.err.println("Don't know what this is " + other) - if(useAnyInstantiator) { - instantiator.dumpFunctionMap - } else { - System.err.println("REVERSE FUNCTION MAP:") - System.err.println(reverseFunctionMap.toSeq.mkString("\n")) - } - System.err.println("REVERSE CONS MAP:") - System.err.println(reverseADTConstructors.toSeq.mkString("\n")) - // System.exit(-1) - throw new CantTranslateException(t) - } - } - - rec(tree) - } -} diff --git a/src/main/scala/purescala/testcases/Main.scala b/src/main/scala/purescala/testcases/Main.scala deleted file mode 100644 index b67b26cadf40bb96eb96384024d439746a74a6e3..0000000000000000000000000000000000000000 --- a/src/main/scala/purescala/testcases/Main.scala +++ /dev/null @@ -1,124 +0,0 @@ -package purescala.testcases - -import purescala.Reporter -import purescala.Trees._ -import purescala.Definitions._ -import purescala.Extensions._ -import purescala.Settings -import purescala.Common.Identifier - -class Main(reporter : Reporter) extends Analyser(reporter) { - val description = "Testcase generation from preconditions" - override val shortDescription = "testcases" - - def analyse(program : Program) : Unit = { - // things that we could control with options: - // - generate for all functions or just impure - // - do not generate for private functions (check FunDef.isPrivate) - // - number of cases per function - - reporter.info("Running testcase generation...") - - val solver = if(Settings.useFairInstantiator) { - new purescala.FairZ3Solver(reporter) - } else { - new purescala.Z3Solver(reporter) - } - solver.setProgram(program) - - def writeToFile(filename: String, content: String) : Unit = { - try { - val fw = new java.io.FileWriter(filename) - fw.write(content) - fw.close - } catch { - case e => reporter.error("There was an error while generating the test file" + filename) - } - } - - def generateTestInput(funDef: FunDef) : Seq[Seq[Expr]] = { - var constraints: Expr = BooleanLiteral(true) - val prec = matchToIfThenElse(funDef.precondition.getOrElse(BooleanLiteral(true))) - var inputList: List[Seq[Expr]] = Nil - var noMoreModels = false - for (i <- 1 to Settings.nbTestcases if !noMoreModels) { - // reporter.info("Current constraints: " + constraints) - val argMap = solver.solveWithBounds(And(prec, constraints), false) - argMap match { - case (Some(true), _) => noMoreModels = true - case (_ , map) => - // reporter.info("Solver returned the following assignment: " + map) - val testInput = (for (arg <- funDef.args) yield { - map.get(arg.id) match { - case Some(value) => value - case None => randomValue(arg.toVariable) - } - }) - inputList = testInput :: inputList - val newConstraints = And(funDef.args.map(_.toVariable).zip(testInput).map{ - case (variable, value) => Equals(variable, value) - }) - constraints = And(constraints, negate(newConstraints)) - } - } - - if (inputList.size < Settings.nbTestcases) - reporter.error("Could only generate " + inputList.size + " testcases while " + Settings.nbTestcases + " were requested") - - inputList.reverse - } - - def indent(s: String) : String = " " + s.split("\n").mkString("\n ") - def capitalize(s: String) : String = s.substring(0, 1).toUpperCase + s.substring(1) - - def testFunctionName(id: Identifier) : String = "test" + capitalize(id.toString) - def testFunction(id: Identifier, inputs: Seq[Seq[Expr]]) : String = { - val idString = id.toString - val toReturn = - "def " + testFunctionName(id) + " : Unit = {" + "\n" + - inputs.map(input => indent(idString + input.mkString("(", ", ", ")"))).mkString("\n") + "\n" + - "}" + "\n" - toReturn - } - - def testMainMethod(funcIds: Seq[Identifier]) : String = { - "def main(args: Array[String]) : Unit = {" + "\n" + - indent(funcIds.map(testFunctionName(_)).mkString("\n")) + "\n" + - "}" + "\n" - } - - def testObject(funcInputPairs: Seq[(Identifier, Seq[Seq[Expr]])]) : String = { - val objectName = program.mainObject.id.toString - val toReturn = - "import " + objectName + "._" + "\n" + - "\n" + - "object Test" + capitalize(objectName) + " {" + "\n" + - indent(testMainMethod(funcInputPairs.map(_._1))) + "\n" + - "\n" + - indent(funcInputPairs.map(pair => testFunction(pair._1, pair._2)).mkString("\n")) + "\n" + - "}" - toReturn - } - - val funcInputPairs: Seq[(Identifier, Seq[Seq[Expr]])] = (for (funDef <- program.definedFunctions.toList.sortWith((fd1, fd2) => fd1 < fd2) if (!funDef.isPrivate && (Settings.functionsToAnalyse.isEmpty || Settings.functionsToAnalyse.contains(funDef.id.name)) && (!Settings.impureTestcases || !funDef.hasBody))) yield { - reporter.info("Considering function definition: " + funDef.id) - // funDef.precondition match { - // case Some(p) => reporter.info("The precondition is: " + p) - // case None => reporter.info("Function has no precondition") - // } - - val testInput = generateTestInput(funDef) - // reporter.info("Generated test input is: " + testInput) - (funDef.id, testInput) - }) - - val outputFolderName = "generated-testcases" - val outputFileName = outputFolderName + "/" + "Test" + program.mainObject.id.toString + ".scala" - new java.io.File(outputFolderName).mkdir() - writeToFile(outputFileName, testObject(funcInputPairs)) - reporter.info("Output written into file: " + outputFileName) - - reporter.info("Done.") - } - -} diff --git a/src/main/scala/purescala/z3plugins/instantiator/AbstractInstantiator.scala b/src/main/scala/purescala/z3plugins/instantiator/AbstractInstantiator.scala deleted file mode 100644 index 7d67035a34e7dc9e04eafadb32f92076e0fcc3d5..0000000000000000000000000000000000000000 --- a/src/main/scala/purescala/z3plugins/instantiator/AbstractInstantiator.scala +++ /dev/null @@ -1,19 +0,0 @@ -package purescala.z3plugins.instantiator - -import z3.scala._ -import purescala.Common._ -import purescala.Trees._ -import purescala.Definitions._ -import purescala.Z3Solver - -trait AbstractInstantiator { - val z3Solver : Z3Solver - def isKnownDef(funDef: FunDef) : Boolean - def functionDefToDecl(funDef: FunDef) : Z3FuncDecl - def isKnownDecl(decl: Z3FuncDecl) : Boolean - def functionDeclToDef(decl: Z3FuncDecl) : FunDef - protected[purescala] def registerFunction(funDef: FunDef, sorts: Seq[Z3Sort], returnSort: Z3Sort) : Unit - def possibleContinuation : Boolean - def increaseSearchDepth() : Unit - def dumpFunctionMap : Unit -} diff --git a/src/main/scala/purescala/z3plugins/instantiator/Instantiator.scala b/src/main/scala/purescala/z3plugins/instantiator/Instantiator.scala deleted file mode 100644 index 33641d97cc925c19204da633432d97e26fbae282..0000000000000000000000000000000000000000 --- a/src/main/scala/purescala/z3plugins/instantiator/Instantiator.scala +++ /dev/null @@ -1,306 +0,0 @@ -package purescala.z3plugins.instantiator - -import z3.scala._ - -import purescala.Common._ -import purescala.Trees._ -import purescala.TypeTrees._ -import purescala.Definitions._ -import purescala.Settings - -import purescala.Z3Solver - -import scala.collection.mutable.{Map => MutableMap, Set => MutableSet} -import scala.collection.mutable.PriorityQueue - -class Instantiator(val z3Solver: Z3Solver) extends Z3Theory(z3Solver.z3, "Instantiator") with AbstractInstantiator { - import z3Solver.{z3,program,typeToSort,fromZ3Formula,toZ3Formula} - - setCallbacks( -// reduceApp = true, - finalCheck = true, - push = true, - pop = true, - newApp = true, - newAssignment = true, - //newRelevant = true, - newEq = true, - newDiseq = true, - reset = true, - restart = true - ) - - //showCallbacks(true) - - // Related to creating and recovering Z3 function symbols - private var functionMap : Map[FunDef,Z3FuncDecl] = Map.empty - private var reverseFunctionMap : Map[Z3FuncDecl,FunDef] = Map.empty - - protected[purescala] def registerFunction(funDef: FunDef, sorts: Seq[Z3Sort], returnSort: Z3Sort) : Unit = { - val z3Decl = mkTheoryFuncDecl(z3.mkStringSymbol(funDef.id.uniqueName), sorts, returnSort) - functionMap = functionMap + (funDef -> z3Decl) - reverseFunctionMap = reverseFunctionMap + (z3Decl -> funDef) - } - - def dumpFunctionMap : Unit = { - println("REVERSE FUNCTION MAP:") - println(reverseFunctionMap.toSeq.mkString("\n")) - } - def isKnownDef(funDef: FunDef) : Boolean = functionMap.isDefinedAt(funDef) - def functionDefToDecl(funDef: FunDef) : Z3FuncDecl = { - functionMap.getOrElse(funDef, scala.sys.error("No Z3 definition found for function symbol "+ funDef.id.name + " in Instantiator.")) - } - def isKnownDecl(decl: Z3FuncDecl) : Boolean = reverseFunctionMap.isDefinedAt(decl) - def functionDeclToDef(decl: Z3FuncDecl) : FunDef = { - reverseFunctionMap.getOrElse(decl, scala.sys.error("No FunDef found for Z3 definition " + decl + " in Instantiator.")) - } - - // Related to discovering function calls and adding instantiations - private var queue : PriorityQueue[Unrolling] = new PriorityQueue[Unrolling]()(UnrollingOrdering) -// private var stillToAssert : List[(Int,Expr)] = Nil - - override def newAssignment(ast: Z3AST, polarity: Boolean) : Unit = safeBlockToAssertAxioms { - examineAndUnroll(ast) - } - - // Just using these to assert axioms early when possible... - override def newEq(ast1: Z3AST, ast2: Z3AST) : Unit = safeBlockToAssertAxioms {} - override def newDiseq(ast1: Z3AST, ast2: Z3AST) : Unit = safeBlockToAssertAxioms {} - - override def newApp(ast: Z3AST) : Unit = { - examineAndUnroll(ast) - } - - override def newRelevant(ast: Z3AST) : Unit = { - // WARNING : CURRENTLY NOT CALLED ! - //examineAndUnroll(ast) - } - - private var bodyInlined : Int = 0 - private var seen : Set[Z3AST] = Set.empty - private var seenCount : Int = 0 - def examineAndUnroll(ast: Z3AST, allFunctions: Boolean = false) : Unit = if(bodyInlined < Settings.unrollingLevel) { - if(seen(ast)) { - seenCount += 1 -// println(" HIT ! seenCount now at " + seenCount) - return - } else { - seen += ast - } - - val aps = fromZ3Formula(null,ast) - val fis : Set[FunctionInvocation] = if(allFunctions) { - functionCallsOf(aps) - } else { - aps match { - case f @ FunctionInvocation(_,_) => Set(f) - case _ => Set.empty - } - } - - //println("As Purescala: " + aps) - for(fi <- fis) { - val FunctionInvocation(fd, args) = fi - if(bodyInlined < Settings.unrollingLevel && fd.hasPostcondition) { - bodyInlined += 1 - val post = matchToIfThenElse(fd.postcondition.get) - - val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip args) : _*) + (ResultVariable() -> fi) - val newBody = replace(substMap, post) - - val unrolling = new Unrolling(fi, newBody, true, pushLevel) - queue += unrolling - - //assertIfSafeOrDelay(newBody)//, isSafe) - } - - if(bodyInlined < Settings.unrollingLevel && fd.hasBody) { - bodyInlined += 1 - val body = matchToIfThenElse(fd.body.get) - val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip args) : _*) - val newBody = replace(substMap, body) - // val theEquality = Equals(fi, newBody) - - val unrolling = new Unrolling(fi, newBody, false, pushLevel) - //println("Now enqueuing, for function " + fd.id.name + ", with depth: " + unrolling.depth) - //println(newBody) - - queue += unrolling - - //assertIfSafeOrDelay(theEquality) - } - } - } - - override def finalCheck : Boolean = safeBlockToAssertAxioms { - if(!queue.isEmpty) { - while(!queue.isEmpty && queue.head.depth <= deepestAuthorized) { - val highest : Unrolling = queue.dequeue() - val toConvertAndAssert = if(highest.isContract) { - highest.body - } else { - Equals(highest.invocation, highest.body) - } - // println("Now will be asserting :") - // println(toConvertAndAssert) - assertAxiomASAP(toZ3Formula(z3, toConvertAndAssert).get, 0) - } - } -// stillToAssert = Nil - true -/* - if(stillToAssert.isEmpty) { - true - } else { - for((lvl,ast) <- stillToAssert.reverse) { - assertAxiomASAP(ast, lvl) - //assertPermanently(ast) - } - stillToAssert = Nil - true - } -*/ - } - - // This is concerned with how many new function calls the assertion is going - // to introduce. - // private def assertIfSafeOrDelay(ast: Expr, isSafe: Boolean = false) : Unit = { - // println("I'm going to assert this at the next final check :") - // println(ast) - // println("BTW, I think you should know the depth of this thing is : " + measureADTChildrenDepth(ast)) - // stillToAssert = ((pushLevel, ast)) :: stillToAssert - // } - - // Assert as soon as possible and keep asserting as long as level is >= lvl. - private def assertAxiomASAP(expr: Expr, lvl: Int) : Unit = assertAxiomASAP(toZ3Formula(z3, expr).get, lvl) - private def assertAxiomASAP(ast: Z3AST, lvl: Int) : Unit = { - if(canAssertAxiom) { - assertAxiomNow(ast) - //println("(supposed to be available from level " + lvl + ")") - if(lvl < pushLevel) { - // Remember to reassert when we backtrack. - if(pushLevel > 0) { - rememberToReassertAt(pushLevel - 1, lvl, ast) - } - } - } else { - toAssertASAP = toAssertASAP + ((lvl, ast)) - } - } - - private def assertAxiomFrom(ast: Z3AST, level: Int) : Unit = { - toAssertASAP = toAssertASAP + ((level, ast)) - } - - // private def assertPermanently(expr: Expr) : Unit = { - // val asZ3 = toZ3Formula(z3, expr).get - - // if(canAssertAxiom) { - // assertAxiomNow(asZ3) - // } else { - // toAssertASAP = toAssertASAP + ((0, asZ3)) - // } - // } - - private def assertAxiomNow(ast: Z3AST) : Unit = { - if(!canAssertAxiom) - println("WARNING ! ASSERTING AXIOM WHEN NOT SAFE !") - - //println("Now asserting : " + ast) - assertAxiom(ast) - } - - override def push : Unit = { - pushLevel += 1 - //println("Now at level " + pushLevel) - } - - override def pop : Unit = { - pushLevel -= 1 - //println("Now at level " + pushLevel) - - if(toReassertAt.isDefinedAt(pushLevel)) { - for((lvl,ax) <- toReassertAt(pushLevel)) { - assertAxiomFrom(ax, lvl) - } - toReassertAt(pushLevel).clear - } - - assert(pushLevel >= 0) - } - - override def restart : Unit = { - pushLevel = 0 - } - - override def reset : Unit = reinit - - // Below is all the machinery to be able to assert axioms in safe states. - - private var pushLevel : Int = _ - private var canAssertAxiom : Boolean = _ - private var toAssertASAP : Set[(Int,Z3AST)] = _ - private val toReassertAt : MutableMap[Int,MutableSet[(Int,Z3AST)]] = MutableMap.empty - - private def rememberToReassertAt(lvl: Int, axLvl: Int, ax: Z3AST) : Unit = { - if(toReassertAt.isDefinedAt(lvl)) { - toReassertAt(lvl) += ((axLvl, ax)) - } else { - toReassertAt(lvl) = MutableSet((axLvl, ax)) - } - } - - 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 - canAssertAxiom = false - toAssertASAP = Set.empty - // stillToAssert = Nil - queue.clear - } - - private def safeBlockToAssertAxioms[A](block: => A): A = { - canAssertAxiom = true - - if (toAssertASAP.nonEmpty) { - // println("In a safe block. " + toAssertASAP.size + " axioms to add.") - for ((lvl, ax) <- toAssertASAP) { - if(lvl <= pushLevel) { - assertAxiomNow(ax) - //println("(supposed to be available from level " + lvl + ")") - if(lvl < pushLevel && pushLevel > 0) { - rememberToReassertAt(pushLevel - 1, lvl, ax) - } - } - } - toAssertASAP = Set.empty - } - - val result = block - canAssertAxiom = false - result - } - - private object UnrollingOrdering extends Ordering[Unrolling] { - def compare(u1: Unrolling, u2: Unrolling) : Int = { - u2.depth - u1.depth - } - } - - private class Unrolling(val invocation: FunctionInvocation, val body: Expr, val isContract: Boolean, val fromLevel: Int) { - // the maximal depth of selector calls in arguments of the invocation - val depth : Int = measureADTChildrenDepth(invocation) -// println("unrolling built. It has depth " + depth) - } - private object Unrolling { - def unapply(u: Unrolling) : Option[(FunctionInvocation,Expr)] = if(u != null) { - Some((u.invocation, u.body)) - } else { - None - } - } -}