diff options
-rw-r--r-- | include/klee/util/ExprRangeEvaluator.h | 2 | ||||
-rw-r--r-- | lib/Expr/Expr.cpp | 17 | ||||
-rw-r--r-- | lib/Solver/FastCexSolver.cpp | 4 |
3 files changed, 13 insertions, 10 deletions
diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h index 61444c76..34b85520 100644 --- a/include/klee/util/ExprRangeEvaluator.h +++ b/include/klee/util/ExprRangeEvaluator.h @@ -93,7 +93,7 @@ template<class T> T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) { switch (e->getKind()) { case Expr::Constant: - return T(cast<ConstantExpr>(e)->getConstantValue()); + return T(cast<ConstantExpr>(e)); case Expr::NotOptimized: break; diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index ae7bc819..e4bde44b 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -164,7 +164,7 @@ unsigned Expr::computeHash() { } unsigned ConstantExpr::computeHash() { - hashValue = getConstantValue() ^ (getWidth() * MAGIC_HASH_CONSTANT); + hashValue = value.getHashValue() ^ (getWidth() * MAGIC_HASH_CONSTANT); return hashValue; } @@ -1001,12 +1001,11 @@ static ref<Expr> TryConstArrayOpt(const ref<ConstantExpr> &cl, } static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) { - uint64_t value = cl->getConstantValue(); Expr::Width width = cl->getWidth(); Expr::Kind rk = r->getKind(); if (width == Expr::Bool) { - if (value) { + if (cl->isTrue()) { return r; } else { // 0 == ... @@ -1033,12 +1032,12 @@ static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) { // (sext(a,T)==c) == (a==c) const SExtExpr *see = cast<SExtExpr>(r); Expr::Width fromBits = see->src->getWidth(); - uint64_t trunc = bits64::truncateToNBits(value, fromBits); + ref<ConstantExpr> trunc = cl->ZExt(fromBits); // pathological check, make sure it is possible to // sext to this value *from any value* - if (value == ints::sext(trunc, width, fromBits)) { - return EqExpr::create(see->src, ConstantExpr::create(trunc, fromBits)); + if (cl == trunc->SExt(width)) { + return EqExpr::create(see->src, trunc); } else { return ConstantExpr::create(0, Expr::Bool); } @@ -1046,12 +1045,12 @@ static ref<Expr> EqExpr_createPartialR(const ref<ConstantExpr> &cl, Expr *r) { // (zext(a,T)==c) == (a==c) const ZExtExpr *zee = cast<ZExtExpr>(r); Expr::Width fromBits = zee->src->getWidth(); - uint64_t trunc = bits64::truncateToNBits(value, fromBits); + ref<ConstantExpr> trunc = cl->ZExt(fromBits); // pathological check, make sure it is possible to // zext to this value *from any value* - if (value == ints::zext(trunc, width, fromBits)) { - return EqExpr::create(zee->src, ConstantExpr::create(trunc, fromBits)); + if (cl == trunc->ZExt(width)) { + return EqExpr::create(zee->src, trunc); } else { return ConstantExpr::create(0, Expr::Bool); } diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 5a2db747..74c068b0 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -101,6 +101,10 @@ private: public: ValueRange() : m_min(1),m_max(0) {} + ValueRange(const ref<ConstantExpr> &ce) { + // FIXME: Support large widths. + m_min = m_max = ce->getLimitedValue(); + } ValueRange(uint64_t value) : m_min(value), m_max(value) {} ValueRange(uint64_t _min, uint64_t _max) : m_min(_min), m_max(_max) {} ValueRange(const ValueRange &b) : m_min(b.m_min), m_max(b.m_max) {} |