diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 12 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 63 | ||||
| -rwxr-xr-x | lib/Solver/Makefile | 9 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 1167 | ||||
| -rw-r--r-- | lib/Solver/Solver.cpp | 440 |
5 files changed, 1690 insertions, 1 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index ac0474fb..1201ac29 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -73,5 +73,17 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions( llvm::cl::CommaSeparated ); + +llvm::cl::opt<klee::MetaSMTBackendType> +UseMetaSMT("use-metasmt", + llvm::cl::desc("Use MetaSMT as an underlying SMT solver and specify the solver backend type."), + llvm::cl::values(clEnumValN(METASMT_BACKEND_NONE, "none", "Don't use metaSMT"), + clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"), + clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"), + clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"), + clEnumValEnd), + llvm::cl::init(METASMT_BACKEND_NONE)); + + } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index caf0de36..b2cff8ba 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -105,6 +105,33 @@ using namespace llvm; using namespace klee; + +#ifdef SUPPORT_METASMT + +#include <metaSMT/frontend/Array.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> +#include <metaSMT/backend/MiniSAT.hpp> +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/support/run_algorithm.hpp> +#include <metaSMT/API/Stack.hpp> +#include <metaSMT/API/Group.hpp> + +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + namespace { cl::opt<bool> DumpStatesOnHalt("dump-states-on-halt", @@ -268,7 +295,41 @@ Executor::Executor(const InterpreterOptions &opts, : std::max(MaxCoreSolverTime,MaxInstructionTime)) { if (coreSolverTimeout) UseForkedCoreSolver = true; - Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + + Solver *coreSolver = NULL; + +#ifdef SUPPORT_METASMT + if (UseMetaSMT != METASMT_BACKEND_NONE) { + + std::string backend; + + switch (UseMetaSMT) { + case METASMT_BACKEND_STP: + backend = "STP"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < STP_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_Z3: + backend = "Z3"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Z3_Backend > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_BOOLECTOR: + backend = "Boolector"; + coreSolver = new MetaSMTSolver< DirectSolver_Context < Boolector > >(UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + default: + assert(false); + break; + }; + std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n"; + } + else { + coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + } +#else + coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); +#endif /* SUPPORT_METASMT */ + + Solver *solver = constructSolverChain(coreSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile index 11d3d330..2be74c01 100755 --- a/lib/Solver/Makefile +++ b/lib/Solver/Makefile @@ -14,3 +14,12 @@ DONT_BUILD_RELINKED=1 BUILD_ARCHIVE=1 include $(LEVEL)/Makefile.common + +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + CXX.Flags += -DBOOST_HAS_GCC_TR1 + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags)) + CXX.Flags += $(metaSMT_CXXFLAGS) + CXX.Flags += $(metaSMT_INCLUDES) +endif \ No newline at end of file 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_ */ diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 3414cda2..4df691f2 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -12,6 +12,7 @@ #include "SolverStats.h" #include "STPBuilder.h" +#include "MetaSMTBuilder.h" #include "klee/Constraints.h" #include "klee/Expr.h" @@ -20,6 +21,7 @@ #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprUtil.h" #include "klee/Internal/Support/Timer.h" +#include "klee/CommandLine.h" #define vc_bvBoolExtract IAMTHESPAWNOFSATAN @@ -45,6 +47,24 @@ IgnoreSolverFailures("ignore-solver-failures", using namespace klee; + +#ifdef SUPPORT_METASMT + +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> +#include <metaSMT/backend/MiniSAT.hpp> +#include <metaSMT/support/run_algorithm.hpp> +#include <metaSMT/API/Stack.hpp> +#include <metaSMT/API/Group.hpp> + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + /***/ SolverImpl::~SolverImpl() { @@ -809,3 +829,423 @@ STPSolverImpl::computeInitialValues(const Query &query, SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() { return runStatusCode; } + +#ifdef SUPPORT_METASMT + +// ------------------------------------- MetaSMTSolverImpl class declaration ------------------------------ + +template<typename SolverContext> +class MetaSMTSolverImpl : public SolverImpl { +private: + + SolverContext _meta_solver; + MetaSMTSolver<SolverContext> *_solver; + MetaSMTBuilder<SolverContext> *_builder; + double _timeout; + bool _useForked; + SolverRunStatus _runStatusCode; + +public: + MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides); + virtual ~MetaSMTSolverImpl(); + + char *getConstraintLog(const Query&); + void setCoreSolverTimeout(double timeout) { _timeout = timeout; } + + bool computeTruth(const Query&, bool &isValid); + bool computeValue(const Query&, ref<Expr> &result); + + bool computeInitialValues(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution); + + SolverImpl::SolverRunStatus runAndGetCex(ref<Expr> query_expr, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution); + + SolverImpl::SolverRunStatus runAndGetCexForked(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution, + double timeout); + + SolverRunStatus getOperationStatusCode(); + + SolverContext& get_meta_solver() { return(_meta_solver); }; + +}; + + +// ------------------------------------- MetaSMTSolver methods -------------------------------------------- + + +template<typename SolverContext> +MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides) + : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked, optimizeDivides)) +{ + +} + +template<typename SolverContext> +MetaSMTSolver<SolverContext>::~MetaSMTSolver() +{ + +} + +template<typename SolverContext> +char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query& query) { + return(impl->getConstraintLog(query)); +} + +template<typename SolverContext> +void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) { + impl->setCoreSolverTimeout(timeout); +} + + +// ------------------------------------- MetaSMTSolverImpl methods ---------------------------------------- + + + +template<typename SolverContext> +MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides) + : _solver(solver), + _builder(new MetaSMTBuilder<SolverContext>(_meta_solver, optimizeDivides)), + _timeout(0.0), + _useForked(useForked) +{ + assert(_solver && "unable to create MetaSMTSolver"); + assert(_builder && "unable to create MetaSMTBuilder"); + + if (_useForked) { + shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700); + assert(shared_memory_id >= 0 && "shmget failed"); + shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0); + assert(shared_memory_ptr != (void*) -1 && "shmat failed"); + shmctl(shared_memory_id, IPC_RMID, NULL); + } +} + +template<typename SolverContext> +MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() { + +} + +template<typename SolverContext> +char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query&) { + // ToDo +} + +template<typename SolverContext> +bool MetaSMTSolverImpl<SolverContext>::computeTruth(const Query& query, bool &isValid) { + + bool success = false; + std::vector<const Array*> objects; + std::vector< std::vector<unsigned char> > values; + bool hasSolution; + + if (computeInitialValues(query, objects, values, hasSolution)) { + // query.expr is valid iff !query.expr is not satisfiable + isValid = !hasSolution; + success = true; + } + + return(success); +} + +template<typename SolverContext> +bool MetaSMTSolverImpl<SolverContext>::computeValue(const Query& query, ref<Expr> &result) { + + bool success = false; + std::vector<const Array*> objects; + std::vector< std::vector<unsigned char> > values; + bool hasSolution; + + // Find the object used in the expression, and compute an assignment for them. + findSymbolicObjects(query.expr, objects); + if (computeInitialValues(query.withFalse(), objects, values, hasSolution)) { + assert(hasSolution && "state has invalid constraint set"); + // Evaluate the expression with the computed assignment. + Assignment a(objects, values); + result = a.evaluate(query.expr); + success = true; + } + + return(success); +} + + +template<typename SolverContext> +bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution) { + + _runStatusCode = SOLVER_RUN_STATUS_FAILURE; + + TimerStatIncrementer t(stats::queryTime); + assert(_builder); + + /* + * FIXME push() and pop() work for Z3 but not for Boolector. + * If using Z3, use push() and pop() and assert constraints. + * If using Boolector, assume constrainsts instead of asserting them. + */ + //push(_meta_solver); + + if (!_useForked) { + for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { + //assertion(_meta_solver, _builder->construct(*it)); + assumption(_meta_solver, _builder->construct(*it)); + } + } + + ++stats::queries; + ++stats::queryCounterexamples; + + bool success = true; + if (_useForked) { + _runStatusCode = runAndGetCexForked(query, objects, values, hasSolution, _timeout); + success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) || (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode)); + } + else { + _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution); + success = true; + } + + if (success) { + if (hasSolution) { + ++stats::queriesInvalid; + } + else { + ++stats::queriesValid; + } + } + + //pop(_meta_solver); + + return(success); +} + +template<typename SolverContext> +SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(ref<Expr> query_expr, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution) +{ + + // assume the negation of the query + assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr))); + hasSolution = solve(_meta_solver); + + if (hasSolution) { + values.reserve(objects.size()); + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + + const Array *array = *it; + assert(array); + typename SolverContext::result_type array_exp = _builder->getInitialArray(array); + + std::vector<unsigned char> data; + data.reserve(array->size); + + for (unsigned offset = 0; offset < array->size; offset++) { + typename SolverContext::result_type elem_exp = evaluate( + _meta_solver, + metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain()))); + unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp); + data.push_back(elem_value); + } + + values.push_back(data); + } + } + + if (true == hasSolution) { + return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE); + } + else { + return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE); + } +} + +static void metaSMTTimeoutHandler(int x) { + _exit(52); +} + +template<typename SolverContext> +SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution, + double timeout) +{ + unsigned char *pos = shared_memory_ptr; + unsigned sum = 0; + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + sum += (*it)->size; + } + // sum += sizeof(uint64_t); + sum += sizeof(stats::queryConstructs); + assert(sum < shared_memory_size && "not enough shared memory for counterexample"); + + fflush(stdout); + fflush(stderr); + int pid = fork(); + if (pid == -1) { + fprintf(stderr, "error: fork failed (for metaSMT)"); + return(SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED); + } + + if (pid == 0) { + if (timeout) { + ::alarm(0); /* Turn off alarm so we can safely set signal handler */ + ::signal(SIGALRM, metaSMTTimeoutHandler); + ::alarm(std::max(1, (int) timeout)); + } + + for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) { + assertion(_meta_solver, _builder->construct(*it)); + //assumption(_meta_solver, _builder->construct(*it)); + } + + + std::vector< std::vector<typename SolverContext::result_type> > aux_arr_exprs; + if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) { + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + + std::vector<typename SolverContext::result_type> aux_arr; + const Array *array = *it; + assert(array); + typename SolverContext::result_type array_exp = _builder->getInitialArray(array); + + for (unsigned offset = 0; offset < array->size; offset++) { + typename SolverContext::result_type elem_exp = evaluate( + _meta_solver, + metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain()))); + aux_arr.push_back(elem_exp); + } + aux_arr_exprs.push_back(aux_arr); + } + assert(aux_arr_exprs.size() == objects.size()); + } + + + // assume the negation of the query + // can be also asserted instead of assumed as we are in a child process + assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr))); + unsigned res = solve(_meta_solver); + + if (res) { + + if (UseMetaSMT != METASMT_BACKEND_BOOLECTOR) { + + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + + const Array *array = *it; + assert(array); + typename SolverContext::result_type array_exp = _builder->getInitialArray(array); + + for (unsigned offset = 0; offset < array->size; offset++) { + + typename SolverContext::result_type elem_exp = evaluate( + _meta_solver, + metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain()))); + unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp); + *pos++ = elem_value; + } + } + } + else { + typename std::vector< std::vector<typename SolverContext::result_type> >::const_iterator eit = aux_arr_exprs.begin(), eie = aux_arr_exprs.end(); + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie, eit != eie; ++it, ++eit) { + const Array *array = *it; + const std::vector<typename SolverContext::result_type>& arr_exp = *eit; + assert(array); + assert(array->size == arr_exp.size()); + + for (unsigned offset = 0; offset < array->size; offset++) { + unsigned char elem_value = metaSMT::read_value(_meta_solver, arr_exp[offset]); + *pos++ = elem_value; + } + } + } + } + assert((uint64_t*) pos); + *((uint64_t*) pos) = stats::queryConstructs; + + _exit(!res); + } + else { + int status; + pid_t res; + + do { + res = waitpid(pid, &status, 0); + } + while (res < 0 && errno == EINTR); + + if (res < 0) { + fprintf(stderr, "error: waitpid() for metaSMT failed"); + return(SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED); + } + + // From timed_run.py: It appears that linux at least will on + // "occasion" return a status when the process was terminated by a + // signal, so test signal first. + if (WIFSIGNALED(status) || !WIFEXITED(status)) { + fprintf(stderr, "error: metaSMT did not return successfully (status = %d) \n", WTERMSIG(status)); + return(SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED); + } + + int exitcode = WEXITSTATUS(status); + if (exitcode == 0) { + hasSolution = true; + } + else if (exitcode == 1) { + hasSolution = false; + } + else if (exitcode == 52) { + fprintf(stderr, "error: metaSMT timed out"); + return(SolverImpl::SOLVER_RUN_STATUS_TIMEOUT); + } + else { + fprintf(stderr, "error: metaSMT did not return a recognized code"); + return(SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE); + } + + if (hasSolution) { + values = std::vector< std::vector<unsigned char> >(objects.size()); + unsigned i = 0; + for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + const Array *array = *it; + assert(array); + std::vector<unsigned char> &data = values[i++]; + data.insert(data.begin(), pos, pos + array->size); + pos += array->size; + } + } + stats::queryConstructs += (*((uint64_t*) pos) - stats::queryConstructs); + + if (true == hasSolution) { + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; + } + else { + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; + } + } +} + +template<typename SolverContext> +SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() { + return _runStatusCode; +} + +template class MetaSMTSolver< DirectSolver_Context < Boolector> >; +template class MetaSMTSolver< DirectSolver_Context < Z3_Backend> >; +template class MetaSMTSolver< DirectSolver_Context < STP_Backend> >; + +#endif /* SUPPORT_METASMT */ + |