From 1f13e9dbf9db2095b6612a47717c2b86e4aaba72 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 26 Jan 2016 17:15:08 +0000 Subject: Add basic implementation of Z3Builder and Z3Solver and Z3SolverImpl which is based on the work of Andrew Santosa (see PR #295) but fixes many bugs in that implementation. The implementation communicates with Z3 via it's C API. This implementation is based of the STPSolver and STPBuilder and so it inherits a lot of its flaws (See TODOs and FIXMEs). I have also ripped out some of the optimisations (constructMulByConstant, constructSDivByConstant and constructUDivByConstant) that were used in the STPBuilder because * I don't trust them * Z3 can probably do these for us in the future if we use the ``Z3_simplify()`` At a glance its performance seems worse than STP but future work can look at improving this. --- include/klee/Solver.h | 19 +- lib/Solver/CoreSolver.cpp | 4 +- lib/Solver/Z3Builder.cpp | 811 ++++++++++++++++++++++++++++++++++++++++++++++ lib/Solver/Z3Builder.h | 196 +++++++++++ lib/Solver/Z3Solver.cpp | 299 +++++++++++++++++ tools/klee/main.cpp | 2 + 6 files changed, 1327 insertions(+), 4 deletions(-) create mode 100644 lib/Solver/Z3Builder.cpp create mode 100644 lib/Solver/Z3Builder.h create mode 100644 lib/Solver/Z3Solver.cpp diff --git a/include/klee/Solver.h b/include/klee/Solver.h index fed6191a..c82ab135 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -225,7 +225,24 @@ namespace klee { }; #endif // ENABLE_STP - +#ifdef ENABLE_Z3 + /// Z3Solver - A solver complete solver based on Z3 + class Z3Solver : public Solver { + public: + /// Z3Solver - Construct a new Z3Solver. + Z3Solver(); + + /// Get the query in SMT-LIBv2 format. + /// \return A C-style string. The caller is responsible for freeing this. + virtual char *getConstraintLog(const Query &); + + /// setCoreSolverTimeout - Set constraint solver timeout delay to the given + /// value; 0 + /// is off. + virtual void setCoreSolverTimeout(double timeout); + }; +#endif // ENABLE_Z3 + #ifdef ENABLE_METASMT template diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 26842d31..94bb3a5e 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -88,9 +88,7 @@ Solver *createCoreSolver(CoreSolverType cst) { return createDummySolver(); case Z3_SOLVER: #ifdef ENABLE_Z3 - // TODO - llvm::report_fatal_error("Z3 support not implemented"); - return NULL; + return new Z3Solver(); #else llvm::errs() << "Not compiled with Z3 support\n"; return NULL; diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp new file mode 100644 index 00000000..f928c927 --- /dev/null +++ b/lib/Solver/Z3Builder.cpp @@ -0,0 +1,811 @@ +//===-- Z3Builder.cpp ------------------------------------------*- C++ -*-====// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#include "klee/Config/config.h" +#ifdef ENABLE_Z3 +#include "Z3Builder.h" + +#include "klee/Expr.h" +#include "klee/Solver.h" +#include "klee/util/Bits.h" +#include "ConstantDivision.h" +#include "klee/SolverStats.h" +#include "llvm/Support/CommandLine.h" + +using namespace klee; + +namespace { +llvm::cl::opt UseConstructHashZ3( + "use-construct-hash-z3", + llvm::cl::desc("Use hash-consing during Z3 query construction."), + llvm::cl::init(true)); +} + +void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) { + ::Z3_string errorMsg = Z3_get_error_msg(ctx, ec); + // FIXME: This is kind of a hack. The value comes from the enum + // Z3_CANCELED_MSG but this isn't currently exposed by Z3's C API + if (strcmp(errorMsg, "canceled") == 0) { + // Solver timeout is not a fatal error + return; + } + llvm::errs() << "Error: Incorrect use of Z3. [" << ec << "] " << errorMsg + << "\n"; + abort(); +} + +Z3ArrayExprHash::~Z3ArrayExprHash() {} + +void Z3ArrayExprHash::clear() { + _update_node_hash.clear(); + _array_hash.clear(); +} + +Z3Builder::Z3Builder(bool autoClearConstructCache) + : autoClearConstructCache(autoClearConstructCache) { + // FIXME: Should probably let the client pass in a Z3_config instead + Z3_config cfg = Z3_mk_config(); + // It is very important that we ask Z3 to let us manage memory so that + // we are able to cache expressions and sorts. + ctx = Z3_mk_context_rc(cfg); + // Make sure we handle any errors reported by Z3. + Z3_set_error_handler(ctx, custom_z3_error_handler); + // When emitting Z3 expressions make them SMT-LIBv2 compliant + Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT); + Z3_del_config(cfg); +} + +Z3Builder::~Z3Builder() { + // Clear caches so exprs/sorts gets freed before the destroying context + // they aren associated with. + clearConstructCache(); + _arr_hash.clear(); + Z3_del_context(ctx); +} + +Z3SortHandle Z3Builder::getBvSort(unsigned width) { + // FIXME: cache these + return Z3SortHandle(Z3_mk_bv_sort(ctx, width), ctx); +} + +Z3SortHandle Z3Builder::getArraySort(Z3SortHandle domainSort, + Z3SortHandle rangeSort) { + // FIXME: cache these + return Z3SortHandle(Z3_mk_array_sort(ctx, domainSort, rangeSort), ctx); +} + +Z3ASTHandle Z3Builder::buildArray(const char *name, unsigned indexWidth, + unsigned valueWidth) { + Z3SortHandle domainSort = getBvSort(indexWidth); + Z3SortHandle rangeSort = getBvSort(valueWidth); + Z3SortHandle t = getArraySort(domainSort, rangeSort); + Z3_symbol s = Z3_mk_string_symbol(ctx, const_cast(name)); + return Z3ASTHandle(Z3_mk_const(ctx, s, t), ctx); +} + +Z3ASTHandle Z3Builder::getTrue() { return Z3ASTHandle(Z3_mk_true(ctx), ctx); } + +Z3ASTHandle Z3Builder::getFalse() { return Z3ASTHandle(Z3_mk_false(ctx), ctx); } + +Z3ASTHandle Z3Builder::bvOne(unsigned width) { return bvZExtConst(width, 1); } + +Z3ASTHandle Z3Builder::bvZero(unsigned width) { return bvZExtConst(width, 0); } + +Z3ASTHandle Z3Builder::bvMinusOne(unsigned width) { + return bvSExtConst(width, (int64_t)-1); +} + +Z3ASTHandle Z3Builder::bvConst32(unsigned width, uint32_t value) { + Z3SortHandle t = getBvSort(width); + return Z3ASTHandle(Z3_mk_unsigned_int(ctx, value, t), ctx); +} + +Z3ASTHandle Z3Builder::bvConst64(unsigned width, uint64_t value) { + Z3SortHandle t = getBvSort(width); + return Z3ASTHandle(Z3_mk_unsigned_int64(ctx, value, t), ctx); +} + +Z3ASTHandle Z3Builder::bvZExtConst(unsigned width, uint64_t value) { + if (width <= 64) + return bvConst64(width, value); + + Z3ASTHandle expr = Z3ASTHandle(bvConst64(64, value), ctx); + Z3ASTHandle zero = Z3ASTHandle(bvConst64(64, 0), ctx); + for (width -= 64; width > 64; width -= 64) + expr = Z3ASTHandle(Z3_mk_concat(ctx, zero, expr), ctx); + return Z3ASTHandle(Z3_mk_concat(ctx, bvConst64(width, 0), expr), ctx); +} + +Z3ASTHandle Z3Builder::bvSExtConst(unsigned width, uint64_t value) { + if (width <= 64) + return bvConst64(width, value); + + Z3SortHandle t = getBvSort(width - 64); + if (value >> 63) { + Z3ASTHandle r = Z3ASTHandle(Z3_mk_int64(ctx, -1, t), ctx); + return Z3ASTHandle(Z3_mk_concat(ctx, r, bvConst64(64, value)), ctx); + } + + Z3ASTHandle r = Z3ASTHandle(Z3_mk_int64(ctx, 0, t), ctx); + return Z3ASTHandle(Z3_mk_concat(ctx, r, bvConst64(64, value)), ctx); +} + +Z3ASTHandle Z3Builder::bvBoolExtract(Z3ASTHandle expr, int bit) { + return Z3ASTHandle(Z3_mk_eq(ctx, bvExtract(expr, bit, bit), bvOne(1)), ctx); +} + +Z3ASTHandle Z3Builder::bvExtract(Z3ASTHandle expr, unsigned top, + unsigned bottom) { + return Z3ASTHandle(Z3_mk_extract(ctx, top, bottom, expr), ctx); +} + +Z3ASTHandle Z3Builder::eqExpr(Z3ASTHandle a, Z3ASTHandle b) { + return Z3ASTHandle(Z3_mk_eq(ctx, a, b), ctx); +} + +// logical right shift +Z3ASTHandle Z3Builder::bvRightShift(Z3ASTHandle expr, unsigned shift) { + unsigned width = getBVLength(expr); + + if (shift == 0) { + return expr; + } else if (shift >= width) { + return bvZero(width); // Overshift to zero + } else { + return Z3ASTHandle( + Z3_mk_concat(ctx, bvZero(shift), bvExtract(expr, width - 1, shift)), + ctx); + } +} + +// logical left shift +Z3ASTHandle Z3Builder::bvLeftShift(Z3ASTHandle expr, unsigned shift) { + unsigned width = getBVLength(expr); + + if (shift == 0) { + return expr; + } else if (shift >= width) { + return bvZero(width); // Overshift to zero + } else { + return Z3ASTHandle( + Z3_mk_concat(ctx, bvExtract(expr, width - shift - 1, 0), bvZero(shift)), + ctx); + } +} + +// left shift by a variable amount on an expression of the specified width +Z3ASTHandle Z3Builder::bvVarLeftShift(Z3ASTHandle expr, Z3ASTHandle shift) { + unsigned width = getBVLength(expr); + Z3ASTHandle res = bvZero(width); + + // construct a big if-then-elif-elif-... with one case per possible shift + // amount + for (int i = width - 1; i >= 0; i--) { + res = + iteExpr(eqExpr(shift, bvConst32(width, i)), bvLeftShift(expr, i), res); + } + + // If overshifting, shift to zero + Z3ASTHandle ex = bvLtExpr(shift, bvConst32(getBVLength(shift), width)); + res = iteExpr(ex, res, bvZero(width)); + return res; +} + +// logical right shift by a variable amount on an expression of the specified +// width +Z3ASTHandle Z3Builder::bvVarRightShift(Z3ASTHandle expr, Z3ASTHandle shift) { + unsigned width = getBVLength(expr); + Z3ASTHandle res = bvZero(width); + + // construct a big if-then-elif-elif-... with one case per possible shift + // amount + for (int i = width - 1; i >= 0; i--) { + res = + iteExpr(eqExpr(shift, bvConst32(width, i)), bvRightShift(expr, i), res); + } + + // If overshifting, shift to zero + Z3ASTHandle ex = bvLtExpr(shift, bvConst32(getBVLength(shift), width)); + res = iteExpr(ex, res, bvZero(width)); + return res; +} + +// arithmetic right shift by a variable amount on an expression of the specified +// width +Z3ASTHandle Z3Builder::bvVarArithRightShift(Z3ASTHandle expr, + Z3ASTHandle shift) { + unsigned width = getBVLength(expr); + + // get the sign bit to fill with + Z3ASTHandle signedBool = bvBoolExtract(expr, width - 1); + + // start with the result if shifting by width-1 + Z3ASTHandle res = constructAShrByConstant(expr, width - 1, signedBool); + + // construct a big if-then-elif-elif-... with one case per possible shift + // amount + // XXX more efficient to move the ite on the sign outside all exprs? + // XXX more efficient to sign extend, right shift, then extract lower bits? + for (int i = width - 2; i >= 0; i--) { + res = iteExpr(eqExpr(shift, bvConst32(width, i)), + constructAShrByConstant(expr, i, signedBool), res); + } + + // If overshifting, shift to zero + Z3ASTHandle ex = bvLtExpr(shift, bvConst32(getBVLength(shift), width)); + res = iteExpr(ex, res, bvZero(width)); + return res; +} + +Z3ASTHandle Z3Builder::notExpr(Z3ASTHandle expr) { + return Z3ASTHandle(Z3_mk_not(ctx, expr), ctx); +} + +Z3ASTHandle Z3Builder::bvNotExpr(Z3ASTHandle expr) { + return Z3ASTHandle(Z3_mk_bvnot(ctx, expr), ctx); +} + +Z3ASTHandle Z3Builder::andExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) { + ::Z3_ast args[2] = {lhs, rhs}; + return Z3ASTHandle(Z3_mk_and(ctx, 2, args), ctx); +} + +Z3ASTHandle Z3Builder::bvAndExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) { + return Z3ASTHandle(Z3_mk_bvand(ctx, lhs, rhs), ctx); +} + +Z3ASTHandle Z3Builder::orExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) { + ::Z3_ast args[2] = {lhs, rhs}; + return Z3ASTHandle(Z3_mk_or(ctx, 2, args), ctx); +} + +Z3ASTHandle Z3Builder::bvOrExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) { + return Z3ASTHandle(Z3_mk_bvor(ctx, lhs, rhs), ctx); +} + +Z3ASTHandle Z3Builder::iffExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) { + Z3SortHandle lhsSort = Z3SortHandle(Z3_get_sort(ctx, lhs), ctx); + Z3SortHandle rhsSort = Z3SortHandle(Z3_get_sort(ctx, rhs), ctx); + assert(Z3_get_sort_kind(ctx, lhsSort) == Z3_get_sort_kind(ctx, rhsSort) && + "lhs and rhs sorts must match"); + assert(Z3_get_sort_kind(ctx, lhsSort) == Z3_BOOL_SORT && "args must have BOOL sort"); + return Z3ASTHandle(Z3_mk_iff(ctx, lhs, rhs), ctx); +} + +Z3ASTHandle Z3Builder::bvXorExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) { + return Z3ASTHandle(Z3_mk_bvxor(ctx, lhs, rhs), ctx); +} + +Z3ASTHandle Z3Builder::bvSignExtend(Z3ASTHandle src, unsigned width) { + unsigned src_width = + Z3_get_bv_sort_size(ctx, Z3SortHandle(Z3_get_sort(ctx, src), ctx)); + assert(src_width <= width && "attempted to extend longer data"); + + return Z3ASTHandle(Z3_mk_sign_ext(ctx, width - src_width, src), ctx); +} + +Z3ASTHandle Z3Builder::writeExpr(Z3ASTHandle array, Z3ASTHandle index, + Z3ASTHandle value) { + return Z3ASTHandle(Z3_mk_store(ctx, array, index, value), ctx); +} + +Z3ASTHandle Z3Builder::readExpr(Z3ASTHandle array, Z3ASTHandle index) { + return Z3ASTHandle(Z3_mk_select(ctx, array, index), ctx); +} + +Z3ASTHandle Z3Builder::iteExpr(Z3ASTHandle condition, Z3ASTHandle whenTrue, + Z3ASTHandle whenFalse) { + return Z3ASTHandle(Z3_mk_ite(ctx, condition, whenTrue, whenFalse), ctx); +} + +unsigned Z3Builder::getBVLength(Z3ASTHandle expr) { + return Z3_get_bv_sort_size(ctx, Z3SortHandle(Z3_get_sort(ctx, expr), ctx)); +} + +Z3ASTHandle Z3Builder::bvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) { + return Z3ASTHandle(Z3_mk_bvult(ctx, lhs, rhs), ctx); +} + +Z3ASTHandle Z3Builder::bvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) { + return Z3ASTHandle(Z3_mk_bvule(ctx, lhs, rhs), ctx); +} + +Z3ASTHandle Z3Builder::sbvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) { + return Z3ASTHandle(Z3_mk_bvslt(ctx, lhs, rhs), ctx); +} + +Z3ASTHandle Z3Builder::sbvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) { + return Z3ASTHandle(Z3_mk_bvsle(ctx, lhs, rhs), ctx); +} + +Z3ASTHandle Z3Builder::constructAShrByConstant(Z3ASTHandle expr, unsigned shift, + Z3ASTHandle isSigned) { + unsigned width = getBVLength(expr); + + if (shift == 0) { + return expr; + } else if (shift >= width) { + return bvZero(width); // Overshift to zero + } else { + // FIXME: Is this really the best way to interact with Z3? + return iteExpr(isSigned, + Z3ASTHandle(Z3_mk_concat(ctx, bvMinusOne(shift), + bvExtract(expr, width - 1, shift)), + ctx), + bvRightShift(expr, shift)); + } +} + +Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { + + assert(root); + Z3ASTHandle array_expr; + bool hashed = _arr_hash.lookupArrayExpr(root, array_expr); + + if (!hashed) { + // Unique arrays by name, so we make sure the name is unique by + // including the address. + char buf[32]; + unsigned const addrlen = + sprintf(buf, "_%p", (const void *)root) + 1; // +1 for null-termination + unsigned const space = (root->name.length() > 32 - addrlen) + ? (32 - addrlen) + : root->name.length(); + memmove(buf + space, buf, addrlen); // moving the address part to the end + memcpy(buf, root->name.c_str(), space); // filling out the name part + + array_expr = buildArray(buf, root->getDomain(), root->getRange()); + + if (root->isConstantArray()) { + // FIXME: Flush the concrete values into Z3. Ideally we would do this + // using assertions, which might be faster, but we need to fix the caching + // to work correctly in that case. + for (unsigned i = 0, e = root->size; i != e; ++i) { + Z3ASTHandle prev = array_expr; + array_expr = writeExpr( + prev, construct(ConstantExpr::alloc(i, root->getDomain()), 0), + construct(root->constantValues[i], 0)); + } + } + + _arr_hash.hashArrayExpr(root, array_expr); + } + + return (array_expr); +} + +Z3ASTHandle Z3Builder::getInitialRead(const Array *root, unsigned index) { + return readExpr(getInitialArray(root), bvConst32(32, index)); +} + +Z3ASTHandle Z3Builder::getArrayForUpdate(const Array *root, + const UpdateNode *un) { + if (!un) { + return (getInitialArray(root)); + } else { + // FIXME: This really needs to be non-recursive. + Z3ASTHandle un_expr; + bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr); + + if (!hashed) { + un_expr = writeExpr(getArrayForUpdate(root, un->next), + construct(un->index, 0), construct(un->value, 0)); + + _arr_hash.hashUpdateNodeExpr(un, un_expr); + } + + return (un_expr); + } +} + +/** if *width_out!=1 then result is a bitvector, + otherwise it is a bool */ +Z3ASTHandle Z3Builder::construct(ref e, int *width_out) { + // TODO: We could potentially use Z3_simplify() here + // to store simpler expressions. + if (!UseConstructHashZ3 || isa(e)) { + return constructActual(e, width_out); + } else { + ExprHashMap >::iterator it = + constructed.find(e); + if (it != constructed.end()) { + if (width_out) + *width_out = it->second.second; + return it->second.first; + } else { + int width; + if (!width_out) + width_out = &width; + Z3ASTHandle res = constructActual(e, width_out); + constructed.insert(std::make_pair(e, std::make_pair(res, *width_out))); + return res; + } + } +} + +/** if *width_out!=1 then result is a bitvector, + otherwise it is a bool */ +Z3ASTHandle Z3Builder::constructActual(ref e, int *width_out) { + int width; + if (!width_out) + width_out = &width; + + ++stats::queryConstructs; + + switch (e->getKind()) { + case Expr::Constant: { + ConstantExpr *CE = cast(e); + *width_out = CE->getWidth(); + + // Coerce to bool if necessary. + if (*width_out == 1) + return CE->isTrue() ? getTrue() : getFalse(); + + // Fast path. + if (*width_out <= 32) + return bvConst32(*width_out, CE->getZExtValue(32)); + if (*width_out <= 64) + return bvConst64(*width_out, CE->getZExtValue()); + + ref Tmp = CE; + Z3ASTHandle Res = bvConst64(64, Tmp->Extract(0, 64)->getZExtValue()); + while (Tmp->getWidth() > 64) { + Tmp = Tmp->Extract(64, Tmp->getWidth() - 64); + unsigned Width = std::min(64U, Tmp->getWidth()); + Res = Z3ASTHandle( + Z3_mk_concat(ctx, + bvConst64(Width, Tmp->Extract(0, Width)->getZExtValue()), + Res), + ctx); + } + return Res; + } + + // Special + case Expr::NotOptimized: { + NotOptimizedExpr *noe = cast(e); + return construct(noe->src, width_out); + } + + case Expr::Read: { + ReadExpr *re = cast(e); + assert(re && re->updates.root); + *width_out = re->updates.root->getRange(); + return readExpr(getArrayForUpdate(re->updates.root, re->updates.head), + construct(re->index, 0)); + } + + case Expr::Select: { + SelectExpr *se = cast(e); + Z3ASTHandle cond = construct(se->cond, 0); + Z3ASTHandle tExpr = construct(se->trueExpr, width_out); + Z3ASTHandle fExpr = construct(se->falseExpr, width_out); + return iteExpr(cond, tExpr, fExpr); + } + + case Expr::Concat: { + ConcatExpr *ce = cast(e); + unsigned numKids = ce->getNumKids(); + Z3ASTHandle res = construct(ce->getKid(numKids - 1), 0); + for (int i = numKids - 2; i >= 0; i--) { + res = + Z3ASTHandle(Z3_mk_concat(ctx, construct(ce->getKid(i), 0), res), ctx); + } + *width_out = ce->getWidth(); + return res; + } + + case Expr::Extract: { + ExtractExpr *ee = cast(e); + Z3ASTHandle src = construct(ee->expr, width_out); + *width_out = ee->getWidth(); + if (*width_out == 1) { + return bvBoolExtract(src, ee->offset); + } else { + return bvExtract(src, ee->offset + *width_out - 1, ee->offset); + } + } + + // Casting + + case Expr::ZExt: { + int srcWidth; + CastExpr *ce = cast(e); + Z3ASTHandle src = construct(ce->src, &srcWidth); + *width_out = ce->getWidth(); + if (srcWidth == 1) { + return iteExpr(src, bvOne(*width_out), bvZero(*width_out)); + } else { + return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - srcWidth), src), + ctx); + } + } + + case Expr::SExt: { + int srcWidth; + CastExpr *ce = cast(e); + Z3ASTHandle src = construct(ce->src, &srcWidth); + *width_out = ce->getWidth(); + if (srcWidth == 1) { + return iteExpr(src, bvMinusOne(*width_out), bvZero(*width_out)); + } else { + return bvSignExtend(src, *width_out); + } + } + + // Arithmetic + case Expr::Add: { + AddExpr *ae = cast(e); + Z3ASTHandle left = construct(ae->left, width_out); + Z3ASTHandle right = construct(ae->right, width_out); + assert(*width_out != 1 && "uncanonicalized add"); + Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvadd(ctx, left, right), ctx); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::Sub: { + SubExpr *se = cast(e); + Z3ASTHandle left = construct(se->left, width_out); + Z3ASTHandle right = construct(se->right, width_out); + assert(*width_out != 1 && "uncanonicalized sub"); + Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvsub(ctx, left, right), ctx); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::Mul: { + MulExpr *me = cast(e); + Z3ASTHandle right = construct(me->right, width_out); + assert(*width_out != 1 && "uncanonicalized mul"); + Z3ASTHandle left = construct(me->left, width_out); + Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvmul(ctx, left, right), ctx); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::UDiv: { + UDivExpr *de = cast(e); + Z3ASTHandle left = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized udiv"); + + if (ConstantExpr *CE = dyn_cast(de->right)) { + if (CE->getWidth() <= 64) { + uint64_t divisor = CE->getZExtValue(); + if (bits64::isPowerOfTwo(divisor)) + return bvRightShift(left, bits64::indexOfSingleBit(divisor)); + } + } + + Z3ASTHandle right = construct(de->right, width_out); + Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvudiv(ctx, left, right), ctx); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::SDiv: { + SDivExpr *de = cast(e); + Z3ASTHandle left = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized sdiv"); + Z3ASTHandle right = construct(de->right, width_out); + Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvsdiv(ctx, left, right), ctx); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::URem: { + URemExpr *de = cast(e); + Z3ASTHandle left = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized urem"); + + if (ConstantExpr *CE = dyn_cast(de->right)) { + if (CE->getWidth() <= 64) { + uint64_t divisor = CE->getZExtValue(); + + if (bits64::isPowerOfTwo(divisor)) { + unsigned bits = bits64::indexOfSingleBit(divisor); + + // special case for modding by 1 or else we bvExtract -1:0 + if (bits == 0) { + return bvZero(*width_out); + } else { + return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - bits), + bvExtract(left, bits - 1, 0)), + ctx); + } + } + } + } + + Z3ASTHandle right = construct(de->right, width_out); + Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvurem(ctx, left, right), ctx); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + case Expr::SRem: { + SRemExpr *de = cast(e); + Z3ASTHandle left = construct(de->left, width_out); + Z3ASTHandle right = construct(de->right, width_out); + assert(*width_out != 1 && "uncanonicalized srem"); + // LLVM's srem instruction says that the sign follows the dividend + // (``left``). + // Z3's C API says ``Z3_mk_bvsrem()`` does this so these seem to match. + Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvsrem(ctx, left, right), ctx); + assert(getBVLength(result) == static_cast(*width_out) && + "width mismatch"); + return result; + } + + // Bitwise + case Expr::Not: { + NotExpr *ne = cast(e); + Z3ASTHandle expr = construct(ne->expr, width_out); + if (*width_out == 1) { + return notExpr(expr); + } else { + return bvNotExpr(expr); + } + } + + case Expr::And: { + AndExpr *ae = cast(e); + Z3ASTHandle left = construct(ae->left, width_out); + Z3ASTHandle right = construct(ae->right, width_out); + if (*width_out == 1) { + return andExpr(left, right); + } else { + return bvAndExpr(left, right); + } + } + + case Expr::Or: { + OrExpr *oe = cast(e); + Z3ASTHandle left = construct(oe->left, width_out); + Z3ASTHandle right = construct(oe->right, width_out); + if (*width_out == 1) { + return orExpr(left, right); + } else { + return bvOrExpr(left, right); + } + } + + case Expr::Xor: { + XorExpr *xe = cast(e); + Z3ASTHandle left = construct(xe->left, width_out); + Z3ASTHandle right = construct(xe->right, width_out); + + if (*width_out == 1) { + // XXX check for most efficient? + return iteExpr(left, Z3ASTHandle(notExpr(right)), right); + } else { + return bvXorExpr(left, right); + } + } + + case Expr::Shl: { + ShlExpr *se = cast(e); + Z3ASTHandle left = construct(se->left, width_out); + assert(*width_out != 1 && "uncanonicalized shl"); + + if (ConstantExpr *CE = dyn_cast(se->right)) { + return bvLeftShift(left, (unsigned)CE->getLimitedValue()); + } else { + int shiftWidth; + Z3ASTHandle amount = construct(se->right, &shiftWidth); + return bvVarLeftShift(left, amount); + } + } + + case Expr::LShr: { + LShrExpr *lse = cast(e); + Z3ASTHandle left = construct(lse->left, width_out); + assert(*width_out != 1 && "uncanonicalized lshr"); + + if (ConstantExpr *CE = dyn_cast(lse->right)) { + return bvRightShift(left, (unsigned)CE->getLimitedValue()); + } else { + int shiftWidth; + Z3ASTHandle amount = construct(lse->right, &shiftWidth); + return bvVarRightShift(left, amount); + } + } + + case Expr::AShr: { + AShrExpr *ase = cast(e); + Z3ASTHandle left = construct(ase->left, width_out); + assert(*width_out != 1 && "uncanonicalized ashr"); + + if (ConstantExpr *CE = dyn_cast(ase->right)) { + unsigned shift = (unsigned)CE->getLimitedValue(); + Z3ASTHandle signedBool = bvBoolExtract(left, *width_out - 1); + return constructAShrByConstant(left, shift, signedBool); + } else { + int shiftWidth; + Z3ASTHandle amount = construct(ase->right, &shiftWidth); + return bvVarArithRightShift(left, amount); + } + } + + // Comparison + + case Expr::Eq: { + EqExpr *ee = cast(e); + Z3ASTHandle left = construct(ee->left, width_out); + Z3ASTHandle right = construct(ee->right, width_out); + if (*width_out == 1) { + if (ConstantExpr *CE = dyn_cast(ee->left)) { + if (CE->isTrue()) + return right; + return notExpr(right); + } else { + return iffExpr(left, right); + } + } else { + *width_out = 1; + return eqExpr(left, right); + } + } + + case Expr::Ult: { + UltExpr *ue = cast(e); + Z3ASTHandle left = construct(ue->left, width_out); + Z3ASTHandle right = construct(ue->right, width_out); + assert(*width_out != 1 && "uncanonicalized ult"); + *width_out = 1; + return bvLtExpr(left, right); + } + + case Expr::Ule: { + UleExpr *ue = cast(e); + Z3ASTHandle left = construct(ue->left, width_out); + Z3ASTHandle right = construct(ue->right, width_out); + assert(*width_out != 1 && "uncanonicalized ule"); + *width_out = 1; + return bvLeExpr(left, right); + } + + case Expr::Slt: { + SltExpr *se = cast(e); + Z3ASTHandle left = construct(se->left, width_out); + Z3ASTHandle right = construct(se->right, width_out); + assert(*width_out != 1 && "uncanonicalized slt"); + *width_out = 1; + return sbvLtExpr(left, right); + } + + case Expr::Sle: { + SleExpr *se = cast(e); + Z3ASTHandle left = construct(se->left, width_out); + Z3ASTHandle right = construct(se->right, width_out); + assert(*width_out != 1 && "uncanonicalized sle"); + *width_out = 1; + return sbvLeExpr(left, right); + } + +// unused due to canonicalization +#if 0 + case Expr::Ne: + case Expr::Ugt: + case Expr::Uge: + case Expr::Sgt: + case Expr::Sge: +#endif + + default: + assert(0 && "unhandled Expr type"); + return getTrue(); + } +} +#endif // ENABLE_Z3 diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h new file mode 100644 index 00000000..f3b2732b --- /dev/null +++ b/lib/Solver/Z3Builder.h @@ -0,0 +1,196 @@ +//===-- Z3Builder.h --------------------------------------------*- C++ -*-====// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef __UTIL_Z3BUILDER_H__ +#define __UTIL_Z3BUILDER_H__ + +#include "klee/util/ExprHashMap.h" +#include "klee/util/ArrayExprHash.h" +#include "klee/Config/config.h" +#include + +namespace klee { + +template class Z3NodeHandle { + // Internally these Z3 types are pointers + // so storing these should be cheap. + // It would be nice if we could infer the Z3_context from the node + // but I can't see a way to do this from Z3's API. +protected: + T node; + ::Z3_context context; + +private: + // To be specialised + inline ::Z3_ast as_ast(); + +public: + Z3NodeHandle() : node(NULL), context(NULL) {} + Z3NodeHandle(const T _node, const ::Z3_context _context) + : node(_node), context(_context) { + if (node && context) { + ::Z3_inc_ref(context, as_ast()); + } + }; + ~Z3NodeHandle() { + if (node && context) { + ::Z3_dec_ref(context, as_ast()); + } + } + Z3NodeHandle(const Z3NodeHandle &b) : node(b.node), context(b.context) { + if (node && context) { + ::Z3_inc_ref(context, as_ast()); + } + } + Z3NodeHandle &operator=(const Z3NodeHandle &b) { + if (node == NULL && context == NULL) { + // Special case for when this object was constructed + // using the default constructor. Try to inherit a non null + // context. + context = b.context; + } + assert(context == b.context && "Mismatched Z3 contexts!"); + // node != nullptr ==> context != NULL + assert((node == NULL || context) && + "Can't have non nullptr node with nullptr context"); + + if (node && context) { + ::Z3_dec_ref(context, as_ast()); + } + node = b.node; + if (node && context) { + ::Z3_inc_ref(context, as_ast()); + } + return *this; + } + // To be specialised + void dump(); + + operator T() { return node; } +}; + +// Specialise for Z3_sort +template <> inline ::Z3_ast Z3NodeHandle::as_ast() { + // In Z3 internally this call is just a cast. We could just do that + // instead to simplify our implementation but this seems cleaner. + return ::Z3_sort_to_ast(context, node); +} +template <> inline void Z3NodeHandle::dump() { + llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node) + << "\n"; +} +typedef Z3NodeHandle Z3SortHandle; + +// Specialise for Z3_ast +template <> inline ::Z3_ast Z3NodeHandle::as_ast() { return node; } +template <> inline void Z3NodeHandle::dump() { + llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast()) + << "\n"; +} +typedef Z3NodeHandle Z3ASTHandle; + +class Z3ArrayExprHash : public ArrayExprHash { + + friend class Z3Builder; + +public: + Z3ArrayExprHash(){}; + virtual ~Z3ArrayExprHash(); + void clear(); +}; + +class Z3Builder { + ExprHashMap > constructed; + Z3ArrayExprHash _arr_hash; + +private: + Z3ASTHandle bvOne(unsigned width); + Z3ASTHandle bvZero(unsigned width); + Z3ASTHandle bvMinusOne(unsigned width); + Z3ASTHandle bvConst32(unsigned width, uint32_t value); + Z3ASTHandle bvConst64(unsigned width, uint64_t value); + Z3ASTHandle bvZExtConst(unsigned width, uint64_t value); + Z3ASTHandle bvSExtConst(unsigned width, uint64_t value); + Z3ASTHandle bvBoolExtract(Z3ASTHandle expr, int bit); + Z3ASTHandle bvExtract(Z3ASTHandle expr, unsigned top, unsigned bottom); + Z3ASTHandle eqExpr(Z3ASTHandle a, Z3ASTHandle b); + + // logical left and right shift (not arithmetic) + Z3ASTHandle bvLeftShift(Z3ASTHandle expr, unsigned shift); + Z3ASTHandle bvRightShift(Z3ASTHandle expr, unsigned shift); + Z3ASTHandle bvVarLeftShift(Z3ASTHandle expr, Z3ASTHandle shift); + Z3ASTHandle bvVarRightShift(Z3ASTHandle expr, Z3ASTHandle shift); + Z3ASTHandle bvVarArithRightShift(Z3ASTHandle expr, Z3ASTHandle shift); + + Z3ASTHandle notExpr(Z3ASTHandle expr); + Z3ASTHandle bvNotExpr(Z3ASTHandle expr); + Z3ASTHandle andExpr(Z3ASTHandle lhs, Z3ASTHandle rhs); + Z3ASTHandle bvAndExpr(Z3ASTHandle lhs, Z3ASTHandle rhs); + Z3ASTHandle orExpr(Z3ASTHandle lhs, Z3ASTHandle rhs); + Z3ASTHandle bvOrExpr(Z3ASTHandle lhs, Z3ASTHandle rhs); + Z3ASTHandle iffExpr(Z3ASTHandle lhs, Z3ASTHandle rhs); + Z3ASTHandle bvXorExpr(Z3ASTHandle lhs, Z3ASTHandle rhs); + Z3ASTHandle bvSignExtend(Z3ASTHandle src, unsigned width); + + // Array operations + Z3ASTHandle writeExpr(Z3ASTHandle array, Z3ASTHandle index, + Z3ASTHandle value); + Z3ASTHandle readExpr(Z3ASTHandle array, Z3ASTHandle index); + + // ITE-expression constructor + Z3ASTHandle iteExpr(Z3ASTHandle condition, Z3ASTHandle whenTrue, + Z3ASTHandle whenFalse); + + // Bitvector length + unsigned getBVLength(Z3ASTHandle expr); + + // Bitvector comparison + Z3ASTHandle bvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs); + Z3ASTHandle bvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs); + Z3ASTHandle sbvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs); + Z3ASTHandle sbvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs); + + Z3ASTHandle constructAShrByConstant(Z3ASTHandle expr, unsigned shift, + Z3ASTHandle isSigned); + + Z3ASTHandle getInitialArray(const Array *os); + Z3ASTHandle getArrayForUpdate(const Array *root, const UpdateNode *un); + + Z3ASTHandle constructActual(ref e, int *width_out); + Z3ASTHandle construct(ref e, int *width_out); + + Z3ASTHandle buildArray(const char *name, unsigned indexWidth, + unsigned valueWidth); + + Z3SortHandle getBvSort(unsigned width); + Z3SortHandle getArraySort(Z3SortHandle domainSort, Z3SortHandle rangeSort); + bool autoClearConstructCache; + +public: + Z3_context ctx; + + Z3Builder(bool autoClearConstructCache = true); + ~Z3Builder(); + + Z3ASTHandle getTrue(); + Z3ASTHandle getFalse(); + Z3ASTHandle getInitialRead(const Array *os, unsigned index); + + Z3ASTHandle construct(ref e) { + Z3ASTHandle res = construct(e, 0); + if (autoClearConstructCache) + clearConstructCache(); + return res; + } + + void clearConstructCache() { constructed.clear(); } +}; +} + +#endif diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp new file mode 100644 index 00000000..994386ab --- /dev/null +++ b/lib/Solver/Z3Solver.cpp @@ -0,0 +1,299 @@ +//===-- Z3Solver.cpp -------------------------------------------*- C++ -*-====// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#include "klee/Config/config.h" +#ifdef ENABLE_Z3 +#include "Z3Builder.h" +#include "klee/Constraints.h" +#include "klee/Solver.h" +#include "klee/SolverImpl.h" +#include "klee/util/Assignment.h" +#include "klee/util/ExprUtil.h" + +namespace klee { + +class Z3SolverImpl : public SolverImpl { +private: + Z3Builder *builder; + double timeout; + SolverRunStatus runStatusCode; + ::Z3_params solverParameters; + // Parameter symbols + ::Z3_symbol timeoutParamStrSymbol; + + bool internalRunSolver(const Query &, + const std::vector *objects, + std::vector > *values, + bool &hasSolution); + +public: + Z3SolverImpl(); + ~Z3SolverImpl(); + + char *getConstraintLog(const Query &); + void setCoreSolverTimeout(double _timeout) { + assert(_timeout >= 0.0 && "timeout must be >= 0"); + timeout = _timeout; + + unsigned int timeoutInMilliSeconds = (unsigned int)((timeout * 1000) + 0.5); + if (timeoutInMilliSeconds == 0) + timeoutInMilliSeconds = UINT_MAX; + Z3_params_set_uint(builder->ctx, solverParameters, timeoutParamStrSymbol, + timeoutInMilliSeconds); + } + + bool computeTruth(const Query &, bool &isValid); + bool computeValue(const Query &, ref &result); + bool computeInitialValues(const Query &, + const std::vector &objects, + std::vector > &values, + bool &hasSolution); + SolverRunStatus + handleSolverResponse(::Z3_solver theSolver, ::Z3_lbool satisfiable, + const std::vector *objects, + std::vector > *values, + bool &hasSolution); + SolverRunStatus getOperationStatusCode(); +}; + +Z3SolverImpl::Z3SolverImpl() + : builder(new Z3Builder(/*autoClearConstructCache=*/false)), timeout(0.0), + runStatusCode(SOLVER_RUN_STATUS_FAILURE) { + assert(builder && "unable to create Z3Builder"); + solverParameters = Z3_mk_params(builder->ctx); + Z3_params_inc_ref(builder->ctx, solverParameters); + timeoutParamStrSymbol = Z3_mk_string_symbol(builder->ctx, "timeout"); + setCoreSolverTimeout(timeout); +} + +Z3SolverImpl::~Z3SolverImpl() { + Z3_params_dec_ref(builder->ctx, solverParameters); + delete builder; +} + +Z3Solver::Z3Solver() : Solver(new Z3SolverImpl()) {} + +char *Z3Solver::getConstraintLog(const Query &query) { + return impl->getConstraintLog(query); +} + +void Z3Solver::setCoreSolverTimeout(double timeout) { + impl->setCoreSolverTimeout(timeout); +} + +char *Z3SolverImpl::getConstraintLog(const Query &query) { + std::vector assumptions; + for (std::vector >::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) { + assumptions.push_back(builder->construct(*it)); + } + ::Z3_ast *assumptionsArray = NULL; + int numAssumptions = query.constraints.size(); + if (numAssumptions) { + assumptionsArray = (::Z3_ast *)malloc(sizeof(::Z3_ast) * numAssumptions); + for (int index = 0; index < numAssumptions; ++index) { + assumptionsArray[index] = (::Z3_ast)assumptions[index]; + } + } + + // KLEE Queries are validity queries i.e. + // ∀ X Constraints(X) → query(X) + // but Z3 works in terms of satisfiability so instead we ask the + // the negation of the equivalent i.e. + // ∃ X Constraints(X) ∧ ¬ query(X) + Z3ASTHandle formula = Z3ASTHandle( + Z3_mk_not(builder->ctx, builder->construct(query.expr)), builder->ctx); + + ::Z3_string result = Z3_benchmark_to_smtlib_string( + builder->ctx, + /*name=*/"Emited by klee::Z3SolverImpl::getConstraintLog()", + /*logic=*/"", + /*status=*/"unknown", + /*attributes=*/"", + /*num_assumptions=*/numAssumptions, + /*assumptions=*/assumptionsArray, + /*formula=*/formula); + + if (numAssumptions) + free(assumptionsArray); + // Client is responsible for freeing the returned C-string + return strdup(result); +} + +bool Z3SolverImpl::computeTruth(const Query &query, bool &isValid) { + bool hasSolution; + bool status = + internalRunSolver(query, /*objects=*/NULL, /*values=*/NULL, hasSolution); + isValid = !hasSolution; + return status; +} + +bool Z3SolverImpl::computeValue(const Query &query, ref &result) { + std::vector objects; + std::vector > values; + bool hasSolution; + + // Find the object used in the expression, and compute an assignment + // for them. + findSymbolicObjects(query.expr, objects); + if (!computeInitialValues(query.withFalse(), objects, values, hasSolution)) + return false; + assert(hasSolution && "state has invalid constraint set"); + + // Evaluate the expression with the computed assignment. + Assignment a(objects, values); + result = a.evaluate(query.expr); + + return true; +} + +bool Z3SolverImpl::computeInitialValues( + const Query &query, const std::vector &objects, + std::vector > &values, bool &hasSolution) { + return internalRunSolver(query, &objects, &values, hasSolution); +} + +bool Z3SolverImpl::internalRunSolver( + const Query &query, const std::vector *objects, + std::vector > *values, bool &hasSolution) { + TimerStatIncrementer t(stats::queryTime); + // TODO: Does making a new solver for each query have a performance + // impact vs making one global solver and using push and pop? + // TODO: is the "simple_solver" the right solver to use for + // best performance? + Z3_solver theSolver = Z3_mk_simple_solver(builder->ctx); + Z3_solver_inc_ref(builder->ctx, theSolver); + Z3_solver_set_params(builder->ctx, theSolver, solverParameters); + + runStatusCode = SOLVER_RUN_STATUS_FAILURE; + + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) { + Z3_solver_assert(builder->ctx, theSolver, builder->construct(*it)); + } + ++stats::queries; + if (objects) + ++stats::queryCounterexamples; + + Z3ASTHandle z3QueryExpr = + Z3ASTHandle(builder->construct(query.expr), builder->ctx); + + // KLEE Queries are validity queries i.e. + // ∀ X Constraints(X) → query(X) + // but Z3 works in terms of satisfiability so instead we ask the + // negation of the equivalent i.e. + // ∃ X Constraints(X) ∧ ¬ query(X) + Z3_solver_assert( + builder->ctx, theSolver, + Z3ASTHandle(Z3_mk_not(builder->ctx, z3QueryExpr), builder->ctx)); + + ::Z3_lbool satisfiable = Z3_solver_check(builder->ctx, theSolver); + runStatusCode = handleSolverResponse(theSolver, satisfiable, objects, values, + hasSolution); + + Z3_solver_dec_ref(builder->ctx, theSolver); + // Clear the builder's cache to prevent memory usage exploding. + // By using ``autoClearConstructCache=false`` and clearning now + // we allow Z3_ast expressions to be shared from an entire + // ``Query`` rather than only sharing within a single call to + // ``builder->construct()``. + builder->clearConstructCache(); + + if (runStatusCode == SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE || + runStatusCode == SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE) { + if (hasSolution) { + ++stats::queriesInvalid; + } else { + ++stats::queriesValid; + } + return true; // success + } + return false; // failed +} + +SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse( + ::Z3_solver theSolver, ::Z3_lbool satisfiable, + const std::vector *objects, + std::vector > *values, bool &hasSolution) { + switch (satisfiable) { + case Z3_L_TRUE: { + hasSolution = true; + if (!objects) { + // No assignment is needed + assert(values == NULL); + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; + } + assert(values && "values cannot be nullptr"); + ::Z3_model theModel = Z3_solver_get_model(builder->ctx, theSolver); + assert(theModel && "Failed to retrieve model"); + Z3_model_inc_ref(builder->ctx, theModel); + values->reserve(objects->size()); + for (std::vector::const_iterator it = objects->begin(), + ie = objects->end(); + it != ie; ++it) { + const Array *array = *it; + std::vector data; + + data.reserve(array->size); + for (unsigned offset = 0; offset < array->size; offset++) { + // We can't use Z3ASTHandle here so have to do ref counting manually + ::Z3_ast arrayElementExpr; + Z3ASTHandle initial_read = builder->getInitialRead(array, offset); + + bool successfulEval = + Z3_model_eval(builder->ctx, theModel, initial_read, + /*model_completion=*/Z3_TRUE, &arrayElementExpr); + assert(successfulEval && "Failed to evaluate model"); + Z3_inc_ref(builder->ctx, arrayElementExpr); + assert(Z3_get_ast_kind(builder->ctx, arrayElementExpr) == + Z3_NUMERAL_AST && + "Evaluated expression has wrong sort"); + + int arrayElementValue = 0; + bool successGet = Z3_get_numeral_int(builder->ctx, arrayElementExpr, + &arrayElementValue); + assert(successGet && "failed to get value back"); + assert(arrayElementValue >= 0 && arrayElementValue <= 255 && + "Integer from model is out of range"); + data.push_back(arrayElementValue); + Z3_dec_ref(builder->ctx, arrayElementExpr); + } + values->push_back(data); + } + + Z3_model_dec_ref(builder->ctx, theModel); + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; + } + case Z3_L_FALSE: + hasSolution = false; + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; + case Z3_L_UNDEF: { + ::Z3_string reason = + ::Z3_solver_get_reason_unknown(builder->ctx, theSolver); + if (strcmp(reason, "timeout") == 0 || strcmp(reason, "canceled") == 0) { + return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; + } + if (strcmp(reason, "unknown") == 0) { + return SolverImpl::SOLVER_RUN_STATUS_FAILURE; + } + llvm::errs() << "Unexpected solver failure. Reason is \"" << reason + << "\"\n"; + abort(); + } + default: + llvm_unreachable("unhandled Z3 result"); + } +} + +SolverImpl::SolverRunStatus Z3SolverImpl::getOperationStatusCode() { + return runStatusCode; +} +} +#endif // ENABLE_Z3 diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index debbe7d2..665cc842 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -480,6 +480,8 @@ void KleeHandler::processTestCase(const ExecutionState &state, } if (WriteCVCs) { + // FIXME: If using Z3 as the core solver the emitted file is actually + // SMT-LIBv2 not CVC which is a bit confusing std::string constraints; m_interpreter->getConstraintLog(state, constraints, Interpreter::STP); llvm::raw_ostream *f = openTestFile("cvc", id); -- cgit 1.4.1