From 3ef201af75998c37046ee42e1015c3f870a61fb1 Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <ekneuss@gmail.com> Date: Fri, 29 May 2015 19:25:57 +0200 Subject: [PATCH] Improve model reconstruction by providing target type This is necessary because what was there was invalid: sorts<->types are not a bijection, since several Leon types compile to the same sort (BV32) <-> (CharType, Int32Type). By providing the expected type, we can reconstruct the correct model. If the model uses expressions, we can no longer make sure we get the right thing, and will guess using sorts. --- .../leon/solvers/z3/AbstractZ3Solver.scala | 139 +++++++----------- .../scala/leon/solvers/z3/FairZ3Solver.scala | 11 +- .../solvers/z3/UninterpretedZ3Solver.scala | 2 +- .../solvers/z3/Z3ModelReconstruction.scala | 4 +- 4 files changed, 62 insertions(+), 94 deletions(-) diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala index 42d53fc24..d8ac22b21 100644 --- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala @@ -86,12 +86,6 @@ trait AbstractZ3Solver } } - object LeonType { - def unapply(a: Z3Sort): Option[(TypeTree)] = { - sorts.getLeon(a).map(tt => tt) - } - } - class Bijection[A, B] { var leonToZ3 = Map[A, B]() var z3ToLeon = Map[B, A]() @@ -559,7 +553,7 @@ trait AbstractZ3Solver case Not(e) => z3.mkNot(rec(e)) case IntLiteral(v) => z3.mkInt(v, typeToSort(Int32Type)) case InfiniteIntegerLiteral(v) => z3.mkNumeral(v.toString, typeToSort(IntegerType)) - case CharLiteral(c) => z3.mkInt(c, typeToSort(Int32Type)) + case CharLiteral(c) => z3.mkInt(c, typeToSort(CharType)) case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse() case UnitLiteral() => unitValue case Equals(l, r) => z3.mkEq(rec( l ), rec( r ) ) @@ -728,17 +722,32 @@ trait AbstractZ3Solver } } - protected[leon] def fromZ3Formula(model: Z3Model, tree : Z3AST) : Expr = { - def rec(t: Z3AST): Expr = { + protected[leon] def fromZ3Formula(model: Z3Model, tree: Z3AST, tpe: TypeTree) : Expr = { + + // This is unsafe and should be avoided because sorts<->types are not a bijection + // For instance, both Int32Type and CharType compile to BV32 + + def recGuess(t: Z3AST): Expr = { + val s = z3.getSort(t) + rec(t, sorts.toLeon(s)) + } + + def rec(t: Z3AST, tpe: TypeTree): Expr = { val kind = z3.getASTKind(t) - val sort = z3.getSort(t) kind match { case Z3NumeralIntAST(Some(v)) => { val leading = t.toString.substring(0, 2 min t.toString.length) if(leading == "#x") { _root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match { - case Some(hexa) => IntLiteral(hexa.toInt) + case Some(hexa) => + tpe match { + case Int32Type => IntLiteral(hexa.toInt) + case CharType => CharLiteral(hexa.toInt.toChar) + case _ => + println("Unexpected target type for BV value: " + tpe) + throw new CantTranslateException(t) + } case None => { println("Z3NumeralIntAST with None: " + t) throw new CantTranslateException(t) @@ -750,7 +759,14 @@ trait AbstractZ3Solver } case Z3NumeralIntAST(None) => { _root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match { - case Some(hexa) => IntLiteral(hexa.toInt) + case Some(hexa) => + tpe match { + case Int32Type => IntLiteral(hexa.toInt) + case CharType => CharLiteral(hexa.toInt.toChar) + case _ => + println("Unexpected target type for BV value: " + tpe) + throw new CantTranslateException(t) + } case None => { println("Z3NumeralIntAST with None: " + t) throw new CantTranslateException(t) @@ -764,87 +780,85 @@ trait AbstractZ3Solver } else if(functions containsZ3 decl) { val tfd = functions.toLeon(decl) assert(tfd.params.size == argsSize) - FunctionInvocation(tfd, args.map(rec)) + FunctionInvocation(tfd, args.zip(tfd.params).map{ case (a, p) => rec(a, p.getType) }) } else if(argsSize == 1 && (reverseADTTesters contains decl)) { val cct = reverseADTTesters(decl) - CaseClassInstanceOf(cct, rec(args.head)) + CaseClassInstanceOf(cct, rec(args.head, cct.root)) } else if(argsSize == 1 && (reverseADTFieldSelectors contains decl)) { val (cct, fid) = reverseADTFieldSelectors(decl) - CaseClassSelector(cct, rec(args.head), fid) + CaseClassSelector(cct, rec(args.head, cct), fid) } else if(reverseADTConstructors contains decl) { val cct = reverseADTConstructors(decl) assert(argsSize == cct.fields.size) - CaseClass(cct, args.map(rec)) + CaseClass(cct, args.zip(cct.fieldsTypes).map{ case (a, t) => rec(a, t) }) } else if (generics containsZ3 decl) { generics.toLeon(decl) } else { - sort match { - case LeonType(tp: TypeParameter) => + tpe match { + case tp: TypeParameter => val id = t.toString.split("!").last.toInt GenericValue(tp, id) - case LeonType(tp: TupleType) => - val rargs = args.map(rec) + case TupleType(ts) => + val rargs = args.zip(ts).map{ case (a, t) => rec(a, t) } tupleWrap(rargs) - case LeonType(at @ ArrayType(dt)) => + case at @ ArrayType(dt) => assert(args.size == 2) - val length = rec(args(1)) match { - case InfiniteIntegerLiteral(length) => length.toInt + val length = rec(args(1), Int32Type) match { case IntLiteral(length) => length case _ => throw new CantTranslateException(t) } model.getArrayValue(args(0)) match { case None => throw new CantTranslateException(t) case Some((map, elseZ3Value)) => - val elseValue = rec(elseZ3Value) + val elseValue = rec(elseZ3Value, dt) val valuesMap = map.map { case (k,v) => - val index = rec(k) match { - case InfiniteIntegerLiteral(index) => index.toInt + val index = rec(k, Int32Type) match { case IntLiteral(index) => index case _ => throw new CantTranslateException(t) } - index -> rec(v) + index -> rec(v, dt) } finiteArray(valuesMap, Some(elseValue, IntLiteral(length)), dt) } - case LeonType(tpe @ MapType(kt, vt)) => + case tpe @ MapType(kt, vt) => model.getArrayValue(t) match { case None => throw new CantTranslateException(t) case Some((map, elseZ3Value)) => val values = map.toSeq.map { case (k, v) => (k, z3.getASTKind(v)) }.collect { case (k, Z3AppAST(cons, arg :: Nil)) if cons == mapRangeSomeConstructors(vt) => - (rec(k), rec(arg)) + (rec(k, kt), rec(arg, vt)) } finiteMap(values, kt, vt) } - case LeonType(FunctionType(fts, tt)) => + case FunctionType(fts, tt) => model.getArrayValue(t) match { case None => throw new CantTranslateException(t) case Some((map, elseZ3Value)) => - val leonElseValue = rec(elseZ3Value) - val leonMap = map.toSeq.map(p => rec(p._1) -> rec(p._2)) + val leonElseValue = rec(elseZ3Value, tt) + val leonMap = map.toSeq.map(p => rec(p._1, tupleTypeWrap(fts)) -> rec(p._2, tt)) finiteLambda(leonElseValue, leonMap, fts) } - case LeonType(tpe @ SetType(dt)) => + case tpe @ SetType(dt) => model.getSetValue(t) match { case None => throw new CantTranslateException(t) case Some(set) => - val elems = set.map(e => rec(e)) + val elems = set.map(e => rec(e, dt)) finiteSet(elems, dt) } - case LeonType(UnitType) => + case UnitType => UnitLiteral() case _ => import Z3DeclKind._ - val rargs = args.map(rec) + val rargs = args.map(recGuess) z3.getDeclKind(decl) match { case OpTrue => BooleanLiteral(true) case OpFalse => BooleanLiteral(false) @@ -879,59 +893,12 @@ trait AbstractZ3Solver throw new CantTranslateException(t) } } - rec(tree) - } - - // Tries to convert a Z3AST into a *ground* Expr. Doesn't try very hard, because - // 1) we assume Z3 simplifies ground terms, so why match for +, etc, and - // 2) we use this precisely in one context, where we know function invocations won't show up, etc. - protected[leon] def asGround(tree : Z3AST) : Option[Expr] = { - val e = new Exception("Not ground.") - - def rec(t : Z3AST) : Expr = z3.getASTKind(t) match { - case Z3AppAST(decl, args) => { - val argsSize = args.size - if(functions containsZ3 decl) { - val tfd = functions.toLeon(decl) - FunctionInvocation(tfd, args.map(rec)) - } else if(argsSize == 1 && reverseADTTesters.isDefinedAt(decl)) { - val cct = reverseADTTesters(decl) - CaseClassInstanceOf(cct, rec(args.head)) - } else if(argsSize == 1 && reverseADTFieldSelectors.isDefinedAt(decl)) { - val (cct, fid) = reverseADTFieldSelectors(decl) - CaseClassSelector(cct, rec(args.head), fid) - } else if(reverseADTConstructors.isDefinedAt(decl)) { - val cct = reverseADTConstructors(decl) - CaseClass(cct, args.map(rec)) - } else { - z3.getSort(t) match { - case LeonType(t : TupleType) => - tupleWrap(args.map(rec)) - - case _ => - import Z3DeclKind._ - z3.getDeclKind(decl) match { - case OpTrue => BooleanLiteral(true) - case OpFalse => BooleanLiteral(false) - case _ => throw e - } - } - } - } - case Z3NumeralIntAST(Some(v)) => InfiniteIntegerLiteral(v) - case _ => throw e - } - - try { - Some(rec(tree)) - } catch { - case e : Exception => None - } + rec(tree, tpe) } - protected[leon] def softFromZ3Formula(model: Z3Model, tree : Z3AST) : Option[Expr] = { + protected[leon] def softFromZ3Formula(model: Z3Model, tree: Z3AST, tpe: TypeTree) : Option[Expr] = { try { - Some(fromZ3Formula(model, tree)) + Some(fromZ3Formula(model, tree, tpe)) } catch { case e: CantTranslateException => None } diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala index b13345ae4..ede0429dd 100644 --- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala @@ -11,6 +11,7 @@ import purescala.Definitions._ import purescala.Expressions._ import purescala.Constructors._ import purescala.ExprOps._ +import purescala.Types._ import solvers.templates._ @@ -64,11 +65,11 @@ class FairZ3Solver(val context : LeonContext, val program: Program) val tfd = functions.toLeon(p._1) if (!tfd.hasImplementation) { val (cses, default) = p._2 - val ite = cses.foldLeft(fromZ3Formula(model, default))((expr, q) => IfExpr( + val ite = cses.foldLeft(fromZ3Formula(model, default, tfd.returnType))((expr, q) => IfExpr( andJoin( - q._1.zip(tfd.params).map(a12 => Equals(fromZ3Formula(model, a12._1), Variable(a12._2.id))) + q._1.zip(tfd.params).map(a12 => Equals(fromZ3Formula(model, a12._1, a12._2.getType), Variable(a12._2.id))) ), - fromZ3Formula(model, q._2), + fromZ3Formula(model, q._2, tfd.returnType), expr)) Seq((tfd.id, ite)) } else Seq() @@ -79,7 +80,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program) if(functions containsZ3 p._1) { val tfd = functions.toLeon(p._1) if(!tfd.hasImplementation) { - Seq((tfd.id, fromZ3Formula(model, p._2))) + Seq((tfd.id, fromZ3Formula(model, p._2, tfd.returnType))) } else Seq() } else Seq() }).toMap @@ -223,7 +224,7 @@ class FairZ3Solver(val context : LeonContext, val program: Program) val assumptionsAsZ3Set: Set[Z3AST] = assumptionsAsZ3.toSet def z3CoreToCore(core: Seq[Z3AST]): Set[Expr] = { - core.filter(assumptionsAsZ3Set).map(ast => fromZ3Formula(null, ast) match { + core.filter(assumptionsAsZ3Set).map(ast => fromZ3Formula(null, ast, BooleanType) match { case n @ Not(Variable(_)) => n case v @ Variable(_) => v case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")") diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala index ffc0bdbbc..08589a2e3 100644 --- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala @@ -66,7 +66,7 @@ class UninterpretedZ3Solver(val context : LeonContext, val program: Program) } def getUnsatCore = { - solver.getUnsatCore().map(ast => fromZ3Formula(null, ast) match { + solver.getUnsatCore().map(ast => fromZ3Formula(null, ast, BooleanType) match { case n @ Not(Variable(_)) => n case v @ Variable(_) => v case x => scala.sys.error("Impossible element extracted from core: " + ast + " (as Leon tree : " + x + ")") diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala index be40e8faf..2abe02272 100644 --- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala +++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala @@ -24,12 +24,12 @@ trait Z3ModelReconstruction { case BooleanType => model.evalAs[Boolean](z3ID).map(BooleanLiteral) case Int32Type => model.evalAs[Int](z3ID).map(IntLiteral).orElse{ - model.eval(z3ID).flatMap(t => softFromZ3Formula(model, t)) + model.eval(z3ID).flatMap(t => softFromZ3Formula(model, t, Int32Type)) } case IntegerType => model.evalAs[Int](z3ID).map(InfiniteIntegerLiteral(_)) case other => model.eval(z3ID) match { case None => None - case Some(t) => softFromZ3Formula(model, t) + case Some(t) => softFromZ3Formula(model, t, other) } } } -- GitLab