diff options
Diffstat (limited to 'lib/Solver/MetaSMTBuilder.h')
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 1167 |
1 files changed, 1167 insertions, 0 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h new file mode 100644 index 00000000..0e508b46 --- /dev/null +++ b/lib/Solver/MetaSMTBuilder.h @@ -0,0 +1,1167 @@ + /* + * MetaSMTBuilder.h + * + * Created on: 8 Aug 2012 + * Author: hpalikar + */ + +#ifndef METASMTBUILDER_H_ +#define METASMTBUILDER_H_ + +#include "klee/Config/config.h" +#include "klee/Expr.h" +#include "klee/util/ExprPPrinter.h" +#include "klee/util/ArrayExprHash.h" +#include "klee/util/ExprHashMap.h" +#include "ConstantDivision.h" + +#ifdef SUPPORT_METASMT + +#include "llvm/Support/CommandLine.h" + +#include <metaSMT/frontend/Logic.hpp> +#include <metaSMT/frontend/QF_BV.hpp> +#include <metaSMT/frontend/Array.hpp> +#include <metaSMT/support/default_visitation_unrolling_limit.hpp> +#include <metaSMT/support/run_algorithm.hpp> + +#define Expr VCExpr +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef STP + +#include <boost/mpl/vector.hpp> +#include <boost/format.hpp> + +using namespace metaSMT; +using namespace metaSMT::logic::QF_BV; + + +#define DIRECT_CONTEXT + +namespace { + llvm::cl::opt<bool> + UseConstructHashMetaSMT("use-construct-hash-metasmt", + llvm::cl::desc("Use hash-consing during metaSMT query construction."), + llvm::cl::init(true)); +} + + +namespace klee { + +typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::true_tag>::type > const MetaSMTConstTrue; +typedef metaSMT::logic::Predicate<proto::terminal<metaSMT::logic::tag::false_tag>::type > const MetaSMTConstFalse; +typedef metaSMT::logic::Array::array MetaSMTArray; + +template<typename SolverContext> +class MetaSMTBuilder; + +template<typename SolverContext> +class MetaSMTArrayExprHash : public ArrayExprHash< typename SolverContext::result_type > { + + friend class MetaSMTBuilder<SolverContext>; + +public: + MetaSMTArrayExprHash() {}; + virtual ~MetaSMTArrayExprHash() {}; +}; + +static const bool mimic_stp = true; + + +template<typename SolverContext> +class MetaSMTBuilder { +public: + + MetaSMTBuilder(SolverContext& solver, bool optimizeDivides) : _solver(solver), _optimizeDivides(optimizeDivides) { }; + virtual ~MetaSMTBuilder() {}; + + typename SolverContext::result_type construct(ref<Expr> e); + + typename SolverContext::result_type getInitialRead(const Array *root, unsigned index); + + typename SolverContext::result_type getTrue() { + return(evaluate(_solver, metaSMT::logic::True)); + } + + typename SolverContext::result_type getFalse() { + return(evaluate(_solver, metaSMT::logic::False)); + } + + typename SolverContext::result_type bvOne(unsigned width) { + return bvZExtConst(width, 1); + } + + typename SolverContext::result_type bvZero(unsigned width) { + return bvZExtConst(width, 0); + } + + typename SolverContext::result_type bvMinusOne(unsigned width) { + return bvSExtConst(width, (int64_t) -1); + } + + typename SolverContext::result_type bvConst32(unsigned width, uint32_t value) { + return(evaluate(_solver, bvuint(value, width))); + } + + typename SolverContext::result_type bvConst64(unsigned width, uint64_t value) { + return(evaluate(_solver, bvuint(value, width))); + } + + typename SolverContext::result_type bvZExtConst(unsigned width, uint64_t value); + typename SolverContext::result_type bvSExtConst(unsigned width, uint64_t value); + + //logical left and right shift (not arithmetic) + typename SolverContext::result_type bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned shift, unsigned shiftBits); + typename SolverContext::result_type bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits); + typename SolverContext::result_type bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); + typename SolverContext::result_type bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); + typename SolverContext::result_type bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width); + + + typename SolverContext::result_type getArrayForUpdate(const Array *root, const UpdateNode *un); + typename SolverContext::result_type getInitialArray(const Array *root); + MetaSMTArray buildArray(unsigned elem_width, unsigned index_width); + +private: + typedef ExprHashMap< std::pair<typename SolverContext::result_type, unsigned> > MetaSMTExprHashMap; + typedef typename MetaSMTExprHashMap::iterator MetaSMTExprHashMapIter; + typedef typename MetaSMTExprHashMap::const_iterator MetaSMTExprHashMapConstIter; + + SolverContext& _solver; + bool _optimizeDivides; + MetaSMTArrayExprHash<SolverContext> _arr_hash; + MetaSMTExprHashMap _constructed; + + typename SolverContext::result_type constructActual(ref<Expr> e, int *width_out); + typename SolverContext::result_type construct(ref<Expr> e, int *width_out); + + typename SolverContext::result_type bvBoolExtract(typename SolverContext::result_type expr, int bit); + typename SolverContext::result_type bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom); + typename SolverContext::result_type eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b); + + typename SolverContext::result_type constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned shift, + typename SolverContext::result_type isSigned, unsigned shiftBits); + typename SolverContext::result_type constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x); + typename SolverContext::result_type constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d); + typename SolverContext::result_type constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d); + + unsigned getShiftBits(unsigned amount) { + unsigned bits = 1; + amount--; + while (amount >>= 1) { + bits++; + } + return(bits); + } +}; + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getArrayForUpdate(const Array *root, const UpdateNode *un) { + + if (!un) { + return(getInitialArray(root)); + } + else { + typename SolverContext::result_type un_expr; + bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr); + + if (!hashed) { + un_expr = evaluate(_solver, + metaSMT::logic::Array::store(getArrayForUpdate(root, un->next), + construct(un->index, 0), + construct(un->value, 0))); + _arr_hash.hashUpdateNodeExpr(un, un_expr); + } + return(un_expr); + } +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialArray(const Array *root) +{ + assert(root); + typename SolverContext::result_type array_expr; + bool hashed = _arr_hash.lookupArrayExpr(root, array_expr); + + if (!hashed) { + + array_expr = evaluate(_solver, buildArray(8, 32)); + + if (root->isConstantArray()) { + for (unsigned i = 0, e = root->size; i != e; ++i) { + typename SolverContext::result_type tmp = + evaluate(_solver, + metaSMT::logic::Array::store(array_expr, + construct(ConstantExpr::alloc(i, root->getDomain()), 0), + construct(root->constantValues[i], 0))); + array_expr = tmp; + } + } + _arr_hash.hashArrayExpr(root, array_expr); + } + + return(array_expr); +} + +template<typename SolverContext> +MetaSMTArray MetaSMTBuilder<SolverContext>::buildArray(unsigned elem_width, unsigned index_width) { + return(metaSMT::logic::Array::new_array(elem_width, index_width)); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::getInitialRead(const Array *root, unsigned index) { + assert(root); + assert(false); + typename SolverContext::result_type array_exp = getInitialArray(root); + typename SolverContext::result_type res = evaluate( + _solver, + metaSMT::logic::Array::select(array_exp, bvuint(index, root->getDomain()))); + return(res); +} + + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvZExtConst(unsigned width, uint64_t value) { + + typename SolverContext::result_type res; + + if (width <= 64) { + res = bvConst64(width, value); + } + else { + typename SolverContext::result_type expr = bvConst64(64, value); + typename SolverContext::result_type zero = bvConst64(64, 0); + + for (width -= 64; width > 64; width -= 64) { + expr = evaluate(_solver, concat(zero, expr)); + } + res = evaluate(_solver, concat(bvConst64(width, 0), expr)); + } + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvSExtConst(unsigned width, uint64_t value) { + + typename SolverContext::result_type res; + + if (width <= 64) { + res = bvConst64(width, value); + } + else { + // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments + res = evaluate(_solver, sign_extend(width - 64, bvConst64(64, value))); + } + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvBoolExtract(typename SolverContext::result_type expr, int bit) { + return(evaluate(_solver, + metaSMT::logic::equal(extract(bit, bit, expr), + bvOne(1)))); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvExtract(typename SolverContext::result_type expr, unsigned top, unsigned bottom) { + return(evaluate(_solver, extract(top, bottom, expr))); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::eqExpr(typename SolverContext::result_type a, typename SolverContext::result_type b) { + return(evaluate(_solver, metaSMT::logic::equal(a, b))); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructAShrByConstant(typename SolverContext::result_type expr, unsigned width, unsigned amount, + typename SolverContext::result_type isSigned, unsigned shiftBits) { + unsigned shift = amount & ((1 << shiftBits) - 1); + typename SolverContext::result_type res; + + if (shift == 0) { + res = expr; + } + else if (shift >= width - 1) { + res = evaluate(_solver, metaSMT::logic::Ite(isSigned, bvMinusOne(width), bvZero(width))); + } + else { + res = evaluate(_solver, metaSMT::logic::Ite(isSigned, + concat(bvMinusOne(shift), bvExtract(expr, width - 1, shift)), + bvRightShift(expr, width, shift, shiftBits))); + } + + return(res); +} + +// width is the width of expr; x -- number of bits to shift with +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructMulByConstant(typename SolverContext::result_type expr, unsigned width, uint64_t x) { + + unsigned shiftBits = getShiftBits(width); + uint64_t add, sub; + typename SolverContext::result_type res; + bool first = true; + + // expr*x == expr*(add-sub) == expr*add - expr*sub + ComputeMultConstants64(x, add, sub); + + // legal, these would overflow completely + add = bits64::truncateToNBits(add, width); + sub = bits64::truncateToNBits(sub, width); + + for (int j = 63; j >= 0; j--) { + uint64_t bit = 1LL << j; + + if ((add & bit) || (sub & bit)) { + assert(!((add & bit) && (sub & bit)) && "invalid mult constants"); + + typename SolverContext::result_type op = bvLeftShift(expr, width, j, shiftBits); + + if (add & bit) { + if (!first) { + res = evaluate(_solver, bvadd(res, op)); + } else { + res = op; + first = false; + } + } else { + if (!first) { + res = evaluate(_solver, bvsub(res, op)); + } else { + // To reconsider: vc_bvUMinusExpr in STP + res = evaluate(_solver, bvsub(bvZero(width), op)); + first = false; + } + } + } + } + + if (first) { + res = bvZero(width); + } + + return(res); +} + + +/* + * Compute the 32-bit unsigned integer division of n by a divisor d based on + * the constants derived from the constant divisor d. + * + * Returns n/d without doing explicit division. The cost is 2 adds, 3 shifts, + * and a (64-bit) multiply. + * + * @param expr_n numerator (dividend) n as an expression + * @param width number of bits used to represent the value + * @param d the divisor + * + * @return n/d without doing explicit division + */ +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructUDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) { + + assert(width == 32 && "can only compute udiv constants for 32-bit division"); + + // Compute the constants needed to compute n/d for constant d without division by d. + uint32_t mprime, sh1, sh2; + ComputeUDivConstants32(d, mprime, sh1, sh2); + typename SolverContext::result_type expr_sh1 = bvConst32(32, sh1); + typename SolverContext::result_type expr_sh2 = bvConst32(32, sh2); + + // t1 = MULUH(mprime, n) = ( (uint64_t)mprime * (uint64_t)n ) >> 32 + typename SolverContext::result_type expr_n_64 = evaluate(_solver, concat(bvZero(32), expr_n)); //extend to 64 bits + typename SolverContext::result_type t1_64bits = constructMulByConstant(expr_n_64, 64, (uint64_t)mprime); + typename SolverContext::result_type t1 = bvExtract(t1_64bits, 63, 32); //upper 32 bits + + // n/d = (((n - t1) >> sh1) + t1) >> sh2; + typename SolverContext::result_type n_minus_t1 = evaluate(_solver, bvsub(expr_n, t1)); + typename SolverContext::result_type shift_sh1 = bvVarRightShift(n_minus_t1, expr_sh1, 32); + typename SolverContext::result_type plus_t1 = evaluate(_solver, bvadd(shift_sh1, t1)); + typename SolverContext::result_type res = bvVarRightShift(plus_t1, expr_sh2, 32); + + return(res); +} + +/* + * Compute the 32-bitnsigned integer division of n by a divisor d based on + * the constants derived from the constant divisor d. + * + * Returns n/d without doing explicit division. The cost is 3 adds, 3 shifts, + * a (64-bit) multiply, and an XOR. + * + * @param n numerator (dividend) as an expression + * @param width number of bits used to represent the value + * @param d the divisor + * + * @return n/d without doing explicit division + */ +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructSDivByConstant(typename SolverContext::result_type expr_n, unsigned width, uint64_t d) { + + assert(width == 32 && "can only compute udiv constants for 32-bit division"); + + // Compute the constants needed to compute n/d for constant d w/o division by d. + int32_t mprime, dsign, shpost; + ComputeSDivConstants32(d, mprime, dsign, shpost); + typename SolverContext::result_type expr_dsign = bvConst32(32, dsign); + typename SolverContext::result_type expr_shpost = bvConst32(32, shpost); + + // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32) + int64_t mprime_64 = (int64_t)mprime; + + // ToDo Reconsider -- note differences in STP and metaSMT for sign_extend arguments + typename SolverContext::result_type expr_n_64 = evaluate(_solver, sign_extend(64 - width, expr_n)); + typename SolverContext::result_type mult_64 = constructMulByConstant(expr_n_64, 64, mprime_64); + typename SolverContext::result_type mulsh = bvExtract(mult_64, 63, 32); //upper 32-bits + typename SolverContext::result_type n_plus_mulsh = evaluate(_solver, bvadd(expr_n, mulsh)); + + // Improved variable arithmetic right shift: sign extend, shift, extract. + typename SolverContext::result_type extend_npm = evaluate(_solver, sign_extend(64 - width, n_plus_mulsh)); + typename SolverContext::result_type shift_npm = bvVarRightShift(extend_npm, expr_shpost, 64); + typename SolverContext::result_type shift_shpost = bvExtract(shift_npm, 31, 0); //lower 32-bits + + ///////////// + + // XSIGN(n) is -1 if n is negative, positive one otherwise + typename SolverContext::result_type is_signed = bvBoolExtract(expr_n, 31); + typename SolverContext::result_type neg_one = bvMinusOne(32); + typename SolverContext::result_type xsign_of_n = evaluate(_solver, metaSMT::logic::Ite(is_signed, neg_one, bvZero(32))); + + // q0 = (n_plus_mulsh >> shpost) - XSIGN(n) + typename SolverContext::result_type q0 = evaluate(_solver, bvsub(shift_shpost, xsign_of_n)); + + // n/d = (q0 ^ dsign) - dsign + typename SolverContext::result_type q0_xor_dsign = evaluate(_solver, bvxor(q0, expr_dsign)); + typename SolverContext::result_type res = evaluate(_solver, bvsub(q0_xor_dsign, expr_dsign)); + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) { + + typename SolverContext::result_type res; + unsigned shift = amount & ((1 << shiftBits) - 1); + + if (shift == 0) { + res = expr; + } + else if (shift >= width) { + res = bvZero(width); + } + else { + // stp shift does "expr @ [0 x s]" which we then have to extract, + // rolling our own gives slightly smaller exprs + res = evaluate(_solver, concat(extract(width - shift - 1, 0, expr), + bvZero(shift))); + } + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned amount, unsigned shiftBits) { + + typename SolverContext::result_type res; + unsigned shift = amount & ((1 << shiftBits) - 1); + + if (shift == 0) { + res = expr; + } + else if (shift >= width) { + res = bvZero(width); + } + else { + res = evaluate(_solver, concat(bvZero(shift), + extract(width - 1, shift, expr))); + } + + return(res); +} + +// left shift by a variable amount on an expression of the specified width +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) { + + typename SolverContext::result_type res = bvZero(width); + + int shiftBits = getShiftBits(width); + + //get the shift amount (looking only at the bits appropriate for the given width) + typename SolverContext::result_type shift = evaluate(_solver, extract(shiftBits - 1, 0, amount)); + + //construct a big if-then-elif-elif-... with one case per possible shift amount + for(int i = width - 1; i >= 0; i--) { + res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)), + bvLeftShift(expr, width, i, shiftBits), + res)); + } + + return(res); +} + +// logical right shift by a variable amount on an expression of the specified width +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) { + + typename SolverContext::result_type res = bvZero(width); + + int shiftBits = getShiftBits(width); + + //get the shift amount (looking only at the bits appropriate for the given width) + typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0); + + //construct a big if-then-elif-elif-... with one case per possible shift amount + for (int i = width - 1; i >= 0; i--) { + res = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits, i)), + bvRightShift(expr, width, i, shiftBits), + res)); + // ToDo Reconsider widht to provide to bvRightShift + } + + return(res); +} + +// arithmetic right shift by a variable amount on an expression of the specified width +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type amount, unsigned width) { + + int shiftBits = getShiftBits(width); + + //get the shift amount (looking only at the bits appropriate for the given width) + typename SolverContext::result_type shift = bvExtract(amount, shiftBits - 1, 0); + + //get the sign bit to fill with + typename SolverContext::result_type signedBool = bvBoolExtract(expr, width - 1); + + //start with the result if shifting by width-1 + typename SolverContext::result_type res = constructAShrByConstant(expr, width, width - 1, signedBool, shiftBits); + + // 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 = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(shiftBits,i)), + constructAShrByConstant(expr, width, i, signedBool, shiftBits), + res)); + } + + return(res); +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e) { + typename SolverContext::result_type res = construct(e, 0); + _constructed.clear(); + return res; +} + + +/** if *width_out!=1 then result is a bitvector, + otherwise it is a bool */ +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::construct(ref<Expr> e, int *width_out) { + + if (!UseConstructHashMetaSMT || isa<ConstantExpr>(e)) { + return(constructActual(e, width_out)); + } else { + MetaSMTExprHashMapIter it = _constructed.find(e); + if (it != _constructed.end()) { + if (width_out) { + *width_out = it->second.second; + } + return it->second.first; + } else { + int width = 0; + if (!width_out) { + width_out = &width; + } + typename SolverContext::result_type res = constructActual(e, width_out); + _constructed.insert(std::make_pair(e, std::make_pair(res, *width_out))); + return res; + } + } +} + +template<typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActual(ref<Expr> e, int *width_out) { + + typename SolverContext::result_type res; + + int width = 0; + if (!width_out) { + // assert(false); + width_out = &width; + } + + ++stats::queryConstructs; + +// std::cerr << "Constructing expression "; +// ExprPPrinter::printSingleExpr(std::cerr, e); +// std::cerr << "\n"; + + switch (e->getKind()) { + + case Expr::Constant: + { + ConstantExpr *coe = cast<ConstantExpr>(e); + assert(coe); + unsigned coe_width = coe->getWidth(); + *width_out = coe_width; + + // Coerce to bool if necessary. + if (coe_width == 1) { + res = (coe->isTrue()) ? getTrue() : getFalse(); + } + else if (coe_width <= 32) { + res = bvConst32(coe_width, coe->getZExtValue(32)); + } + else if (coe_width <= 64) { + res = bvConst64(coe_width, coe->getZExtValue()); + } + else { + ref<ConstantExpr> tmp = coe; + res = bvConst64(64, tmp->Extract(0, 64)->getZExtValue()); + while (tmp->getWidth() > 64) { + tmp = tmp->Extract(64, tmp->getWidth() - 64); + unsigned min_width = std::min(64U, tmp->getWidth()); + res = evaluate(_solver, + concat(bvConst64(min_width, tmp->Extract(0, min_width)->getZExtValue()), + res)); + } + } + break; + } + + case Expr::NotOptimized: + { + NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e); + assert(noe); + res = construct(noe->src, width_out); + break; + } + + case Expr::Select: + { + SelectExpr *se = cast<SelectExpr>(e); + assert(se); + res = evaluate(_solver, + metaSMT::logic::Ite(construct(se->cond, 0), + construct(se->trueExpr, width_out), + construct(se->falseExpr, width_out))); + break; + } + + case Expr::Read: + { + ReadExpr *re = cast<ReadExpr>(e); + assert(re); + // FixMe call method of Array + *width_out = 8; + res = evaluate(_solver, + metaSMT::logic::Array::select( + getArrayForUpdate(re->updates.root, re->updates.head), + construct(re->index, 0))); + break; + } + + case Expr::Concat: + { + ConcatExpr *ce = cast<ConcatExpr>(e); + assert(ce); + *width_out = ce->getWidth(); + unsigned numKids = ce->getNumKids(); + + if (numKids > 0) { + res = evaluate(_solver, construct(ce->getKid(numKids-1), 0)); + for (int i = numKids - 2; i >= 0; i--) { + res = evaluate(_solver, concat(construct(ce->getKid(i), 0), res)); + } + } + break; + } + + case Expr::Extract: + { + ExtractExpr *ee = cast<ExtractExpr>(e); + assert(ee); + // ToDo spare evaluate? + typename SolverContext::result_type child = evaluate(_solver, construct(ee->expr, width_out)); + + unsigned ee_width = ee->getWidth(); + *width_out = ee_width; + + if (ee_width == 1) { + res = bvBoolExtract(child, ee->offset); + } + else { + res = evaluate(_solver, + extract(ee->offset + ee_width - 1, ee->offset, child)); + } + break; + } + + case Expr::ZExt: + { + CastExpr *ce = cast<CastExpr>(e); + assert(ce); + + int child_width = 0; + typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width)); + + unsigned ce_width = ce->getWidth(); + *width_out = ce_width; + + if (child_width == 1) { + res = evaluate(_solver, + metaSMT::logic::Ite(child, bvOne(ce_width), bvZero(ce_width))); + } + else { + res = evaluate(_solver, zero_extend(ce_width - child_width, child)); + } + + // ToDo calculate how many zeros to add + // Note: STP and metaSMT differ in the prototype arguments; + // STP requires the width of the resulting bv; + // whereas metaSMT (and Z3) require the width of the zero vector that is to be appended + // res = evaluate(_solver, zero_extend(ce_width, construct(ce->src))); + + break; + } + + case Expr::SExt: + { + CastExpr *ce = cast<CastExpr>(e); + assert(ce); + + int child_width = 0; + typename SolverContext::result_type child = evaluate(_solver, construct(ce->src, &child_width)); + + unsigned ce_width = ce->getWidth(); + *width_out = ce_width; + + if (child_width == 1) { + res = evaluate(_solver, + metaSMT::logic::Ite(child, bvMinusOne(ce_width), bvZero(ce_width))); + } + else { + // ToDo ce_width - child_width? It is only ce_width in STPBuilder + res = evaluate(_solver, sign_extend(ce_width - child_width, child)); + } + + break; + } + + case Expr::Add: + { + AddExpr *ae = cast<AddExpr>(e); + assert(ae); + res = evaluate(_solver, bvadd(construct(ae->left, width_out), construct(ae->right, width_out))); + assert(*width_out != 1 && "uncanonicalized add"); + break; + } + + case Expr::Sub: + { + SubExpr *se = cast<SubExpr>(e); + assert(se); + res = evaluate(_solver, bvsub(construct(se->left, width_out), construct(se->right, width_out))); + assert(*width_out != 1 && "uncanonicalized sub"); + break; + } + + case Expr::Mul: + { + MulExpr *me = cast<MulExpr>(e); + assert(me); + + typename SolverContext::result_type right_expr = evaluate(_solver, construct(me->right, width_out)); + assert(*width_out != 1 && "uncanonicalized mul"); + + ConstantExpr *CE = dyn_cast<ConstantExpr>(me->left); + if (CE && (CE->getWidth() <= 64)) { + res = constructMulByConstant(right_expr, *width_out, CE->getZExtValue()); + } + else { + res = evaluate(_solver, bvmul(construct(me->left, width_out), right_expr)); + } + break; + } + + case Expr::UDiv: + { + UDivExpr *de = cast<UDivExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized udiv"); + bool construct_both = true; + + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && (CE->getWidth() <= 64)) { + uint64_t divisor = CE->getZExtValue(); + if (bits64::isPowerOfTwo(divisor)) { + res = bvRightShift(left_expr, *width_out, bits64::indexOfSingleBit(divisor), getShiftBits(*width_out)); + construct_both = false; + } + else if (_optimizeDivides) { + if (*width_out == 32) { //only works for 32-bit division + res = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor); + construct_both = false; + } + } + } + + if (construct_both) { + res = evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out))); + } + break; + } + + case Expr::SDiv: + { + SDivExpr *de = cast<SDivExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized sdiv"); + + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && _optimizeDivides && (*width_out == 32)) { + res = constructSDivByConstant(left_expr, *width_out, CE->getZExtValue(32)); + } + else { + res = evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out))); + } + break; + } + + case Expr::URem: + { + URemExpr *de = cast<URemExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = construct(de->left, width_out); + assert(*width_out != 1 && "uncanonicalized urem"); + + bool construct_both = true; + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && (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) { + res = bvZero(*width_out); + construct_both = false; + } + else { + res = evaluate(_solver, concat(bvZero(*width_out - bits), + bvExtract(left_expr, bits - 1, 0))); + construct_both = false; + } + } + + // Use fast division to compute modulo without explicit division for constant divisor. + + if (_optimizeDivides && *width_out == 32) { //only works for 32-bit division + typename SolverContext::result_type quotient = constructUDivByConstant(left_expr, *width_out, (uint32_t) divisor); + typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor); + res = evaluate(_solver, bvsub(left_expr, quot_times_divisor)); + construct_both = false; + } + } + + if (construct_both) { + res = evaluate(_solver, bvurem(left_expr, construct(de->right, width_out))); + } + break; + } + + case Expr::SRem: + { + SRemExpr *de = cast<SRemExpr>(e); + assert(de); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(de->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(de->right, width_out)); + assert(*width_out != 1 && "uncanonicalized srem"); + + bool construct_both = true; + +#if 0 //not faster per first benchmark + + if (_optimizeDivides) { + if (ConstantExpr *cre = de->right->asConstant()) { + uint64_t divisor = cre->asUInt64; + + //use fast division to compute modulo without explicit division for constant divisor + if( *width_out == 32 ) { //only works for 32-bit division + typename SolverContext::result_type quotient = constructSDivByConstant(left, *width_out, divisor); + typename SolverContext::result_type quot_times_divisor = constructMulByConstant(quotient, *width_out, divisor); + res = vc_bvMinusExpr( vc, *width_out, left, quot_times_divisor ); + construct_both = false; + } + } + } + +#endif + + if (construct_both) { + res = evaluate(_solver, bvsrem(left_expr, right_expr)); + } + break; + } + + case Expr::Not: + { + NotExpr *ne = cast<NotExpr>(e); + assert(ne); + + typename SolverContext::result_type child = evaluate(_solver, construct(ne->expr, width_out)); + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::Not(child)); + } + else { + res = evaluate(_solver, bvneg(child)); + } + break; + } + + case Expr::And: + { + AndExpr *ae = cast<AndExpr>(e); + assert(ae); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ae->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ae->right, width_out)); + + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::And(left_expr, right_expr)); + } + else { + res = evaluate(_solver, bvand(left_expr, right_expr)); + } + + break; + } + + case Expr::Or: + { + OrExpr *oe = cast<OrExpr>(e); + assert(oe); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(oe->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(oe->right, width_out)); + + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::Or(left_expr, right_expr)); + } + else { + res = evaluate(_solver, bvor(left_expr, right_expr)); + } + + break; + } + + case Expr::Xor: + { + XorExpr *xe = cast<XorExpr>(e); + assert(xe); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(xe->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(xe->right, width_out)); + + if (*width_out == 1) { + res = evaluate(_solver, metaSMT::logic::Xor(left_expr, right_expr)); + } + else { + res = evaluate(_solver, bvxor(left_expr, right_expr)); + } + + break; + } + + case Expr::Shl: + { + ShlExpr *se = cast<ShlExpr>(e); + assert(se); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out)); + assert(*width_out != 1 && "uncanonicalized shl"); + + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) { + res = bvLeftShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out)); + } + else { + int shiftWidth = 0; + typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, &shiftWidth)); + res = mimic_stp ? bvVarLeftShift(left_expr, right_expr, *width_out) : + evaluate(_solver, bvshl(left_expr, right_expr)); + } + + break; + } + + case Expr::LShr: + { + LShrExpr *lse = cast<LShrExpr>(e); + assert(lse); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(lse->left, width_out)); + assert(*width_out != 1 && "uncanonicalized lshr"); + + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) { + res = bvRightShift(left_expr, *width_out, (unsigned) CE->getLimitedValue(), getShiftBits(*width_out)); + } + else { + int shiftWidth = 0; + typename SolverContext::result_type right_expr = evaluate(_solver, construct(lse->right, &shiftWidth)); + res = mimic_stp ? bvVarRightShift(left_expr, right_expr, *width_out) : + evaluate(_solver, bvshr(left_expr, right_expr)); + } + + break; + } + + case Expr::AShr: + { + AShrExpr *ase = cast<AShrExpr>(e); + assert(ase); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ase->left, width_out)); + assert(*width_out != 1 && "uncanonicalized ashr"); + + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) { + unsigned shift = (unsigned) CE->getLimitedValue(); + typename SolverContext::result_type signedBool = bvBoolExtract(left_expr, *width_out - 1); + res = constructAShrByConstant(left_expr, *width_out, shift, signedBool, getShiftBits(*width_out)); + } + else { + int shiftWidth = 0; + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ase->right, &shiftWidth)); + res = mimic_stp ? bvVarArithRightShift(left_expr, right_expr, *width_out) : + evaluate(_solver, bvashr(left_expr, right_expr)); + } + + break; + } + + case Expr::Eq: + { + EqExpr *ee = cast<EqExpr>(e); + assert(ee); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ee->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ee->right, width_out)); + + if (*width_out==1) { + if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) { + if (CE->isTrue()) { + res = right_expr; + } + else { + res = evaluate(_solver, metaSMT::logic::Not(right_expr)); + } + } + else { + res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr)); + } + } // end of *width_out == 1 + else { + *width_out = 1; + res = evaluate(_solver, metaSMT::logic::equal(left_expr, right_expr)); + } + + break; + } + + case Expr::Ult: + { + UltExpr *ue = cast<UltExpr>(e); + assert(ue); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized ult"); + *width_out = 1; + + res = evaluate(_solver, bvult(left_expr, right_expr)); + break; + } + + case Expr::Ule: + { + UleExpr *ue = cast<UleExpr>(e); + assert(ue); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(ue->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(ue->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized ule"); + *width_out = 1; + + res = evaluate(_solver, bvule(left_expr, right_expr)); + break; + } + + case Expr::Slt: + { + SltExpr *se = cast<SltExpr>(e); + assert(se); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized slt"); + *width_out = 1; + + res = evaluate(_solver, bvslt(left_expr, right_expr)); + break; + } + + case Expr::Sle: + { + SleExpr *se = cast<SleExpr>(e); + assert(se); + + typename SolverContext::result_type left_expr = evaluate(_solver, construct(se->left, width_out)); + typename SolverContext::result_type right_expr = evaluate(_solver, construct(se->right, width_out)); + + assert(*width_out != 1 && "uncanonicalized sle"); + *width_out = 1; + + res = evaluate(_solver, bvsle(left_expr, right_expr)); + break; + } + + // unused due to canonicalization +#if 0 + case Expr::Ne: + case Expr::Ugt: + case Expr::Uge: + case Expr::Sgt: + case Expr::Sge: +#endif + + default: + assert(false); + break; + + }; + return res; +} + + +} /* end of namespace klee */ + +#endif /* SUPPORT_METASMT */ + +#endif /* METASMTBUILDER_H_ */ |