aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Solver/CoreSolver.cpp4
-rw-r--r--lib/Solver/Z3Builder.cpp811
-rw-r--r--lib/Solver/Z3Builder.h196
-rw-r--r--lib/Solver/Z3Solver.cpp299
4 files changed, 1307 insertions, 3 deletions
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<bool> 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<char *>(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<Expr> e, int *width_out) {
+ // TODO: We could potentially use Z3_simplify() here
+ // to store simpler expressions.
+ if (!UseConstructHashZ3 || isa<ConstantExpr>(e)) {
+ return constructActual(e, width_out);
+ } else {
+ ExprHashMap<std::pair<Z3ASTHandle, unsigned> >::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<Expr> e, int *width_out) {
+ int width;
+ if (!width_out)
+ width_out = &width;
+
+ ++stats::queryConstructs;
+
+ switch (e->getKind()) {
+ case Expr::Constant: {
+ ConstantExpr *CE = cast<ConstantExpr>(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<ConstantExpr> 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<NotOptimizedExpr>(e);
+ return construct(noe->src, width_out);
+ }
+
+ case Expr::Read: {
+ ReadExpr *re = cast<ReadExpr>(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<SelectExpr>(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<ConcatExpr>(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<ExtractExpr>(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<CastExpr>(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<CastExpr>(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<AddExpr>(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<unsigned>(*width_out) &&
+ "width mismatch");
+ return result;
+ }
+
+ case Expr::Sub: {
+ SubExpr *se = cast<SubExpr>(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<unsigned>(*width_out) &&
+ "width mismatch");
+ return result;
+ }
+
+ case Expr::Mul: {
+ MulExpr *me = cast<MulExpr>(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<unsigned>(*width_out) &&
+ "width mismatch");
+ return result;
+ }
+
+ case Expr::UDiv: {
+ UDivExpr *de = cast<UDivExpr>(e);
+ Z3ASTHandle left = construct(de->left, width_out);
+ assert(*width_out != 1 && "uncanonicalized udiv");
+
+ if (ConstantExpr *CE = dyn_cast<ConstantExpr>(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<unsigned>(*width_out) &&
+ "width mismatch");
+ return result;
+ }
+
+ case Expr::SDiv: {
+ SDivExpr *de = cast<SDivExpr>(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<unsigned>(*width_out) &&
+ "width mismatch");
+ return result;
+ }
+
+ case Expr::URem: {
+ URemExpr *de = cast<URemExpr>(e);
+ Z3ASTHandle left = construct(de->left, width_out);
+ assert(*width_out != 1 && "uncanonicalized urem");
+
+ if (ConstantExpr *CE = dyn_cast<ConstantExpr>(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<unsigned>(*width_out) &&
+ "width mismatch");
+ return result;
+ }
+
+ case Expr::SRem: {
+ SRemExpr *de = cast<SRemExpr>(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<unsigned>(*width_out) &&
+ "width mismatch");
+ return result;
+ }
+
+ // Bitwise
+ case Expr::Not: {
+ NotExpr *ne = cast<NotExpr>(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<AndExpr>(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<OrExpr>(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<XorExpr>(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<ShlExpr>(e);
+ Z3ASTHandle left = construct(se->left, width_out);
+ assert(*width_out != 1 && "uncanonicalized shl");
+
+ if (ConstantExpr *CE = dyn_cast<ConstantExpr>(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<LShrExpr>(e);
+ Z3ASTHandle left = construct(lse->left, width_out);
+ assert(*width_out != 1 && "uncanonicalized lshr");
+
+ if (ConstantExpr *CE = dyn_cast<ConstantExpr>(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<AShrExpr>(e);
+ Z3ASTHandle left = construct(ase->left, width_out);
+ assert(*width_out != 1 && "uncanonicalized ashr");
+
+ if (ConstantExpr *CE = dyn_cast<ConstantExpr>(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<EqExpr>(e);
+ Z3ASTHandle left = construct(ee->left, width_out);
+ Z3ASTHandle right = construct(ee->right, width_out);
+ if (*width_out == 1) {
+ if (ConstantExpr *CE = dyn_cast<ConstantExpr>(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<UltExpr>(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<UleExpr>(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<SltExpr>(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<SleExpr>(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 <z3.h>
+
+namespace klee {
+
+template <typename T> 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<Z3_sort>::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<Z3_sort>::dump() {
+ llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node)
+ << "\n";
+}
+typedef Z3NodeHandle<Z3_sort> Z3SortHandle;
+
+// Specialise for Z3_ast
+template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; }
+template <> inline void Z3NodeHandle<Z3_ast>::dump() {
+ llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast())
+ << "\n";
+}
+typedef Z3NodeHandle<Z3_ast> Z3ASTHandle;
+
+class Z3ArrayExprHash : public ArrayExprHash<Z3ASTHandle> {
+
+ friend class Z3Builder;
+
+public:
+ Z3ArrayExprHash(){};
+ virtual ~Z3ArrayExprHash();
+ void clear();
+};
+
+class Z3Builder {
+ ExprHashMap<std::pair<Z3ASTHandle, unsigned> > 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<Expr> e, int *width_out);
+ Z3ASTHandle construct(ref<Expr> 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<Expr> 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<const Array *> *objects,
+ std::vector<std::vector<unsigned char> > *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<Expr> &result);
+ bool computeInitialValues(const Query &,
+ const std::vector<const Array *> &objects,
+ std::vector<std::vector<unsigned char> > &values,
+ bool &hasSolution);
+ SolverRunStatus
+ handleSolverResponse(::Z3_solver theSolver, ::Z3_lbool satisfiable,
+ const std::vector<const Array *> *objects,
+ std::vector<std::vector<unsigned char> > *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<Z3ASTHandle> assumptions;
+ for (std::vector<ref<Expr> >::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<Expr> &result) {
+ std::vector<const Array *> objects;
+ std::vector<std::vector<unsigned char> > 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<const Array *> &objects,
+ std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
+ return internalRunSolver(query, &objects, &values, hasSolution);
+}
+
+bool Z3SolverImpl::internalRunSolver(
+ const Query &query, const std::vector<const Array *> *objects,
+ std::vector<std::vector<unsigned char> > *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<const Array *> *objects,
+ std::vector<std::vector<unsigned char> > *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 Array *>::const_iterator it = objects->begin(),
+ ie = objects->end();
+ it != ie; ++it) {
+ const Array *array = *it;
+ std::vector<unsigned char> 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-24 19:03:49 +0000