diff options
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 1994 |
1 files changed, 1040 insertions, 954 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index 7134b023..ba7ea03b 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -7,7 +7,6 @@ // //===----------------------------------------------------------------------===// - /* * MetaSMTBuilder.h * @@ -36,310 +35,353 @@ 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)); +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::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 MetaSMTBuilder; + +template <typename SolverContext> +class MetaSMTArrayExprHash + : public ArrayExprHash<typename SolverContext::result_type> { + + friend class MetaSMTBuilder<SolverContext>; -template<typename SolverContext> -class MetaSMTArrayExprHash : public ArrayExprHash< typename SolverContext::result_type > { - - friend class MetaSMTBuilder<SolverContext>; - public: - MetaSMTArrayExprHash() {}; - virtual ~MetaSMTArrayExprHash() {}; + MetaSMTArrayExprHash(){}; + virtual ~MetaSMTArrayExprHash(){}; }; static const bool mimic_stp = true; - -template<typename SolverContext> -class MetaSMTBuilder { +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); + typename SolverContext::result_type + bvRightShift(typename SolverContext::result_type expr, unsigned width, + unsigned shift); + typename SolverContext::result_type + bvVarLeftShift(typename SolverContext::result_type expr, + typename SolverContext::result_type shift, unsigned width); + typename SolverContext::result_type + bvVarRightShift(typename SolverContext::result_type expr, + typename SolverContext::result_type shift, unsigned width); + typename SolverContext::result_type + bvVarArithRightShift(typename SolverContext::result_type expr, + typename SolverContext::result_type shift, + 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); - 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); - typename SolverContext::result_type bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned shift); - typename SolverContext::result_type bvVarLeftShift(typename SolverContext::result_type expr, typename SolverContext::result_type shift, unsigned width); - typename SolverContext::result_type bvVarRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type shift, unsigned width); - typename SolverContext::result_type bvVarArithRightShift(typename SolverContext::result_type expr, typename SolverContext::result_type shift, 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); - 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); + 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); + 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); }; -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>::getArrayForUpdate(const Array *root, + const UpdateNode *un) { -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 (!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); + } +} - array_expr = evaluate(_solver, buildArray(root->getRange(), root->getDomain())); - - 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); +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(root->getRange(), root->getDomain())); + + 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); + 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> +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>::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) { -template<typename SolverContext> -typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvZExtConst(unsigned width, uint64_t value) { - - typename SolverContext::result_type res; + 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); + 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)); + for (width -= 64; width > 64; width -= 64) { + expr = evaluate(_solver, concat(zero, expr)); } + res = evaluate(_solver, concat(bvConst64(width, 0), expr)); + } - return(res); + return (res); } -template<typename SolverContext> -typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvSExtConst(unsigned width, uint64_t value) { - +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); + 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))); } - 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); + 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>::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>::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>::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 shift, - typename SolverContext::result_type isSigned) { - typename SolverContext::result_type res; - - if (shift == 0) { - res = expr; - } - else if (shift >= width) { - res = bvZero(width); - } - else { - res = evaluate(_solver, metaSMT::logic::Ite(isSigned, - concat(bvMinusOne(shift), bvExtract(expr, width - 1, shift)), - bvRightShift(expr, width, shift))); - } - - return(res); +template <typename SolverContext> +typename SolverContext::result_type +MetaSMTBuilder<SolverContext>::constructAShrByConstant( + typename SolverContext::result_type expr, unsigned width, unsigned shift, + typename SolverContext::result_type isSigned) { + typename SolverContext::result_type res; + + if (shift == 0) { + res = expr; + } else if (shift >= width) { + res = bvZero(width); + } else { + res = evaluate( + _solver, + metaSMT::logic::Ite(isSigned, concat(bvMinusOne(shift), + bvExtract(expr, width - 1, shift)), + bvRightShift(expr, width, shift))); + } + + 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) { - - uint64_t add, sub; - typename SolverContext::result_type res; - bool first = true; +template <typename SolverContext> +typename SolverContext::result_type +MetaSMTBuilder<SolverContext>::constructMulByConstant( + typename SolverContext::result_type expr, unsigned width, uint64_t x) { - // expr*x == expr*(add-sub) == expr*add - expr*sub - ComputeMultConstants64(x, add, sub); + uint64_t add, sub; + typename SolverContext::result_type res; + bool first = true; - // 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; + // expr*x == expr*(add-sub) == expr*add - expr*sub + ComputeMultConstants64(x, add, sub); - if ((add & bit) || (sub & bit)) { - assert(!((add & bit) && (sub & bit)) && "invalid mult constants"); + // legal, these would overflow completely + add = bits64::truncateToNBits(add, width); + sub = bits64::truncateToNBits(sub, width); - typename SolverContext::result_type op = bvLeftShift(expr, width, j); + for (int j = 63; j >= 0; j--) { + uint64_t bit = 1LL << j; - 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 ((add & bit) || (sub & bit)) { + assert(!((add & bit) && (sub & bit)) && "invalid mult constants"); + + typename SolverContext::result_type op = bvLeftShift(expr, width, j); + + 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); -} + if (first) { + res = bvZero(width); + } + return (res); +} -/* - * Compute the 32-bit unsigned integer division of n by a divisor d based on +/* + * 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, + * 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 @@ -348,36 +390,46 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructMulB * * @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); +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 +/* + * 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, + * 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 @@ -386,508 +438,540 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructUDiv * * @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>::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 shift) { - - typename SolverContext::result_type res; +template <typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvLeftShift( + typename SolverContext::result_type expr, unsigned width, unsigned shift) { - 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))); - } + typename SolverContext::result_type res; + + 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); + return (res); } -template<typename SolverContext> -typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift(typename SolverContext::result_type expr, unsigned width, unsigned shift) { - - typename SolverContext::result_type res; +template <typename SolverContext> +typename SolverContext::result_type MetaSMTBuilder<SolverContext>::bvRightShift( + typename SolverContext::result_type expr, unsigned width, unsigned shift) { - if (shift == 0) { - res = expr; - } - else if (shift >= width) { - res = bvZero(width); - } - else { - res = evaluate(_solver, concat(bvZero(shift), - extract(width - 1, shift, expr))); - } + typename SolverContext::result_type res; + + 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); + 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 shift, unsigned width) { - - typename SolverContext::result_type res = bvZero(width); +template <typename SolverContext> +typename SolverContext::result_type +MetaSMTBuilder<SolverContext>::bvVarLeftShift( + typename SolverContext::result_type expr, + typename SolverContext::result_type shift, unsigned width) { + + typename SolverContext::result_type 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 = evaluate(_solver, + metaSMT::logic::Ite(eqExpr(shift, bvConst32(width, i)), + bvLeftShift(expr, width, i), res)); + } - //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(width, i)), - bvLeftShift(expr, width, i), - res)); - } - - // If overshifting, shift to zero - res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), - res, - bvZero(width))); + // If overshifting, shift to zero + res = evaluate(_solver, + metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), res, + bvZero(width))); - return(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 shift, unsigned width) { - - typename SolverContext::result_type 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 = evaluate(_solver, metaSMT::logic::Ite(eqExpr(shift, bvConst32(width, i)), - bvRightShift(expr, width, i), - res)); - // ToDo Reconsider widht to provide to bvRightShift - } - - // If overshifting, shift to zero - res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), - res, - bvZero(width))); - - 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 shift, unsigned width) { + + typename SolverContext::result_type 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 = evaluate(_solver, + metaSMT::logic::Ite(eqExpr(shift, bvConst32(width, i)), + bvRightShift(expr, width, i), res)); + // ToDo Reconsider widht to provide to bvRightShift + } -// 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 shift, unsigned width) { + // If overshifting, shift to zero + res = evaluate(_solver, + metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), res, + bvZero(width))); - //get the sign bit to fill with - typename SolverContext::result_type signedBool = bvBoolExtract(expr, width - 1); + return (res); +} - //start with the result if shifting by width-1 - typename SolverContext::result_type res = constructAShrByConstant(expr, width, width - 1, signedBool); +// 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 shift, unsigned width) { + + // 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); + + // 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(width, i)), + constructAShrByConstant(expr, width, i, signedBool), res)); + } - // 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(width,i)), - constructAShrByConstant(expr, width, i, signedBool), - res)); - } - - // If overshifting, shift to zero - res = evaluate(_solver, metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), - res, - bvZero(width))); + // If overshifting, shift to zero + res = evaluate(_solver, + metaSMT::logic::Ite(bvult(shift, bvConst32(width, width)), res, + bvZero(width))); - return(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; +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)); +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 { - 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; - } + 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) { +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; + typename SolverContext::result_type res; + + int width = 0; + if (!width_out) { + // assert(false); + width_out = &width; + } + + ++stats::queryConstructs; + + // llvm::errs() << "Constructing expression "; + // ExprPPrinter::printSingleExpr(llvm::errs(), e); + // llvm::errs() << "\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)); + } } - - ++stats::queryConstructs; - -// llvm::errs() << "Constructing expression "; -// ExprPPrinter::printSingleExpr(llvm::errs(), e); -// llvm::errs() << "\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; - } + 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::NotOptimized: { + NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e); + assert(noe); + res = construct(noe->src, width_out); + break; + } - case Expr::Read: - { - ReadExpr *re = cast<ReadExpr>(e); - assert(re && re->updates.root); - *width_out = re->updates.root->getRange(); - // FixMe call method of Array - res = evaluate(_solver, - metaSMT::logic::Array::select( - getArrayForUpdate(re->updates.root, re->updates.head), - construct(re->index, 0))); - 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::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::Read: { + ReadExpr *re = cast<ReadExpr>(e); + assert(re && re->updates.root); + *width_out = re->updates.root->getRange(); + // FixMe call method of Array + 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)); + 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; + 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; - } + 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); + 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)); + 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; + 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)); - } + 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)); - } + // 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::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; - } + 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)); - 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; - } - } - } + case Expr::SExt: { + CastExpr *ce = cast<CastExpr>(e); + assert(ce); - if (construct_both) { - res = evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out))); - } - break; - } + int child_width = 0; + typename SolverContext::result_type child = + evaluate(_solver, construct(ce->src, &child_width)); - 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"); - - bool optimized = false; - ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); - if (CE && _optimizeDivides && (*width_out == 32)) { - llvm::APInt divisor = CE->getAPValue(); - if (divisor != llvm::APInt(CE->getWidth(), 1, false /*unsigned*/) && - divisor != llvm::APInt(CE->getWidth(), -1, true /*signed*/)) { - res = constructSDivByConstant(left_expr, *width_out, CE->getZExtValue(32)); - optimized = true; - } - } - if (!optimized) { - res = evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out))); - } - break; + 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)); + 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; } + } + } - case Expr::URem: - { - URemExpr *de = cast<URemExpr>(e); - assert(de); + if (construct_both) { + res = + evaluate(_solver, bvudiv(left_expr, construct(de->right, width_out))); + } + break; + } - 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; - } - } + 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"); + + bool optimized = false; + ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right); + if (CE && _optimizeDivides && (*width_out == 32)) { + llvm::APInt divisor = CE->getAPValue(); + if (divisor != llvm::APInt(CE->getWidth(), 1, false /*unsigned*/) && + divisor != llvm::APInt(CE->getWidth(), -1, true /*signed*/)) { + res = constructSDivByConstant(left_expr, *width_out, + CE->getZExtValue(32)); + optimized = true; + } + } + if (!optimized) { + res = + evaluate(_solver, bvsdiv(left_expr, construct(de->right, width_out))); + } + break; + } - // 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::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; + } + } - 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 (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()) { @@ -902,257 +986,259 @@ typename SolverContext::result_type MetaSMTBuilder<SolverContext>::constructActu } } } - + #endif - if (construct_both) { - res = evaluate(_solver, bvsrem(left_expr, right_expr)); - } - break; - } + 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, bvnot(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()); - } - 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()); - } - 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); - } - 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; + 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, bvnot(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()); + } 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()); + } 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); + } 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)); } - - // unused due to canonicalization + } 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; -} +#endif + default: + assert(false); + break; + }; + return res; +} -} /* end of namespace klee */ +} /* end of namespace klee */ #endif /* ENABLE_METASMT */ |