diff --git a/svf/include/AE/Core/AbstractValue.h b/svf/include/AE/Core/AbstractValue.h index 46f4459d9..0f4a1bf46 100644 --- a/svf/include/AE/Core/AbstractValue.h +++ b/svf/include/AE/Core/AbstractValue.h @@ -213,31 +213,31 @@ class AbstractValue return interval.isBottom(); } - const NumericLiteral& lb() const + const BoundedInt& lb() const { assert(isInterval()); return interval.lb(); } - const NumericLiteral& ub() const + const BoundedInt& ub() const { assert(isInterval()); return interval.ub(); } - void setLb(const NumericLiteral& lb) + void setLb(const BoundedInt& lb) { assert(isInterval()); interval.setLb(lb); } - void setUb(const NumericLiteral& ub) + void setUb(const BoundedInt& ub) { assert(isInterval()); interval.setUb(ub); } - void setValue(const NumericLiteral &lb, const NumericLiteral &ub) + void setValue(const BoundedInt &lb, const BoundedInt &ub) { assert(isInterval()); interval.setValue(lb, ub); diff --git a/svf/include/AE/Core/BoundedZ3Expr.h b/svf/include/AE/Core/BoundedZ3Expr.h deleted file mode 100644 index 20a1f5051..000000000 --- a/svf/include/AE/Core/BoundedZ3Expr.h +++ /dev/null @@ -1,404 +0,0 @@ -//===- BoundedZ3Expr.h ----Address Value Sets-------------------------// -// -// SVF: Static Value-Flow Analysis -// -// Copyright (C) <2013-2022> -// - -// This program is free software: you can redistribute it and/or modify -// it under the terms of the GNU Affero General Public License as published by -// the Free Software Foundation, either version 3 of the License, or -// (at your option) any later version. - -// This program is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU Affero General Public License for more details. - -// You should have received a copy of the GNU Affero General Public License -// along with this program. If not, see . -// -//===----------------------------------------------------------------------===// -/* - * BoundedZ3Expr.h - * - * Created on: Mar 20, 2023 - * Author: Xiao Cheng - * - */ - -#ifndef SVF_BOUNDEDZ3EXPR_H -#define SVF_BOUNDEDZ3EXPR_H -#define MaxBvLen 64 - -#include "Util/Z3Expr.h" - -namespace SVF -{ - -/*! - * Atom Z3 expr for unlimited precision integers - */ -class BoundedZ3Expr : public Z3Expr -{ - -public: - BoundedZ3Expr() = default; - - BoundedZ3Expr(const Z3Expr &z3Expr) : Z3Expr(z3Expr) {} - - BoundedZ3Expr(const z3::expr &e) : Z3Expr(e) {} - - BoundedZ3Expr(s32_t i) : Z3Expr(i) {} - - BoundedZ3Expr(s64_t i) : Z3Expr(getContext().int_val((int64_t)i)) {} - - BoundedZ3Expr(double i) : Z3Expr(getContext().real_val(std::to_string(i).c_str())) {} - - BoundedZ3Expr(const BoundedZ3Expr &z3Expr) : Z3Expr(z3Expr) {} - - inline BoundedZ3Expr &operator=(const BoundedZ3Expr &rhs) - { - Z3Expr::operator=(rhs); - return *this; - } - - BoundedZ3Expr(BoundedZ3Expr &&z3Expr) : Z3Expr(z3Expr) {} - - - inline BoundedZ3Expr &operator=(BoundedZ3Expr &&rhs) - { - Z3Expr::operator=(rhs); - return *this; - } - - bool is_plus_infinite() const - { - return eq(*this, getContext().int_const("+oo")); - } - - bool is_minus_infinite() const - { - return eq(*this, getContext().int_const("-oo")); - } - - bool is_infinite() const - { - return is_plus_infinite() || is_minus_infinite(); - } - - void set_plus_infinite() - { - *this = plus_infinity(); - } - - void set_minus_infinite() - { - *this = minus_infinity(); - } - - static BoundedZ3Expr plus_infinity() - { - return getContext().int_const("+oo"); - } - - static BoundedZ3Expr minus_infinity() - { - return getContext().int_const("-oo"); - } - - static z3::context &getContext() - { - return Z3Expr::getContext(); - } - - bool is_zero() const - { - return getExpr().is_numeral() && eq(getExpr(), Z3Expr(0)); - } - - static bool isZero(const BoundedZ3Expr &expr) - { - return expr.is_numeral() && eq(expr.getExpr(), Z3Expr(0)); - } - - BoundedZ3Expr equal(const BoundedZ3Expr &rhs) const - { - return getExpr() == rhs.getExpr(); - } - - BoundedZ3Expr leq(const BoundedZ3Expr &rhs) const - { - return getExpr() <= rhs.getExpr(); - } - - BoundedZ3Expr geq(const BoundedZ3Expr &rhs) const - { - return getExpr() >= rhs.getExpr(); - } - - /// Reload operator - //{% - friend BoundedZ3Expr operator==(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return lhs.equal(rhs); - } - - friend BoundedZ3Expr operator!=(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return !lhs.equal(rhs); - } - - friend BoundedZ3Expr operator>(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return !lhs.leq(rhs); - } - - friend BoundedZ3Expr operator<(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return !lhs.geq(rhs); - } - - friend BoundedZ3Expr operator<=(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return lhs.leq(rhs); - } - - friend BoundedZ3Expr operator>=(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return lhs.geq(rhs); - } - - friend BoundedZ3Expr operator+(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - if (!lhs.is_infinite() && !rhs.is_infinite()) - return lhs.getExpr() + rhs.getExpr(); - else if (!lhs.is_infinite() && rhs.is_infinite()) - return rhs; - else if (lhs.is_infinite() && !rhs.is_infinite()) - return lhs; - else if (eq(lhs, rhs)) - return lhs; - else - assert(false && "undefined operation +oo + -oo"); - abort(); - } - - friend BoundedZ3Expr operator-(const BoundedZ3Expr &lhs) - { - return -lhs.getExpr(); - } - - friend BoundedZ3Expr operator-(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - if (!lhs.is_infinite() && !rhs.is_infinite()) - return lhs.getExpr() - rhs.getExpr(); - else if (!lhs.is_infinite() && rhs.is_infinite()) - return -rhs; - else if (lhs.is_infinite() && !rhs.is_infinite()) - return lhs; - else if (!eq(lhs, rhs)) - return lhs; - else - assert(false && "undefined operation +oo - +oo"); - abort(); - } - - friend BoundedZ3Expr operator*(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - if (lhs.is_zero() || rhs.is_zero()) return 0; - else if (lhs.is_infinite() && rhs.is_infinite()) - return eq(lhs, rhs) ? plus_infinity() : minus_infinity(); - else if (lhs.is_infinite()) - return ite(rhs.getExpr() > 0, lhs, -lhs); - else if (rhs.is_infinite()) - return ite(lhs.getExpr() > 0, rhs, -rhs); - else - return lhs.getExpr() * rhs.getExpr(); - } - - friend BoundedZ3Expr operator/(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - if (rhs.is_zero()) assert(false && "divide by zero"); - else if (!lhs.is_infinite() && !rhs.is_infinite()) - return lhs.getExpr() / rhs.getExpr(); - else if (!lhs.is_infinite() && rhs.is_infinite()) - return 0; - else if (lhs.is_infinite() && !rhs.is_infinite()) - return ite(rhs.getExpr() > 0, lhs, -lhs); - else - // TODO: +oo/-oo L'Hôpital's rule? - return eq(lhs, rhs) ? plus_infinity() : minus_infinity(); - abort(); - } - - friend BoundedZ3Expr operator%(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - if (rhs.is_zero()) assert(false && "divide by zero"); - else if (!lhs.is_infinite() && !rhs.is_infinite()) - return lhs.getExpr() % rhs.getExpr(); - else if (!lhs.is_infinite() && rhs.is_infinite()) - return 0; - // TODO: not sure - else if (lhs.is_infinite() && !rhs.is_infinite()) - return ite(rhs.getExpr() > 0, lhs, -lhs); - else - // TODO: +oo/-oo L'Hôpital's rule? - return eq(lhs, rhs) ? plus_infinity() : minus_infinity(); - abort(); - } - - friend BoundedZ3Expr operator^(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return bv2int(int2bv(MaxBvLen, lhs.getExpr()) ^ int2bv(MaxBvLen, rhs.getExpr()), true); - } - - friend BoundedZ3Expr operator&(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return bv2int(int2bv(MaxBvLen, lhs.getExpr()) & int2bv(MaxBvLen, rhs.getExpr()), true); - } - - friend BoundedZ3Expr operator|(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return bv2int(int2bv(MaxBvLen, lhs.getExpr()) | int2bv(MaxBvLen, rhs.getExpr()), true); - } - - friend BoundedZ3Expr ashr(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - if (lhs.is_zero()) - return lhs; - else if (lhs.is_infinite()) - return lhs; - else if (rhs.is_infinite()) - return ite(lhs.getExpr() >= 0, BoundedZ3Expr(0), BoundedZ3Expr(-1)); - else - { - return bv2int(ashr(int2bv(MaxBvLen, lhs.getExpr()), int2bv(MaxBvLen, rhs.getExpr())), true); - } - } - - friend BoundedZ3Expr shl(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - if (lhs.is_zero()) - return lhs; - else if (lhs.is_infinite()) - return lhs; - else if (rhs.is_infinite()) - return ite(lhs.getExpr() >= 0, plus_infinity(), minus_infinity()); - else - { - return bv2int(shl(int2bv(MaxBvLen, lhs.getExpr()), int2bv(MaxBvLen, rhs.getExpr())), true); - } - } - - friend BoundedZ3Expr lshr(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return bv2int(lshr(int2bv(MaxBvLen, lhs.getExpr()), int2bv(MaxBvLen, rhs.getExpr())), true); - } - - friend BoundedZ3Expr int2bv(u32_t n, const BoundedZ3Expr &e) - { - return int2bv(n, e.getExpr()); - } - - friend BoundedZ3Expr bv2int(const BoundedZ3Expr &e, bool isSigned) - { - return bv2int(e.getExpr(), isSigned); - } - - friend BoundedZ3Expr operator&&(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return lhs.getExpr() && rhs.getExpr(); - } - - friend BoundedZ3Expr operator||(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return lhs.getExpr() || rhs.getExpr(); - } - - friend BoundedZ3Expr operator!(const BoundedZ3Expr &lhs) - { - return !lhs.getExpr(); - } - - friend BoundedZ3Expr ite(const BoundedZ3Expr &cond, const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return ite(cond.getExpr(), lhs.getExpr(), rhs.getExpr()); - } - - friend std::ostream &operator<<(std::ostream &out, const BoundedZ3Expr &expr) - { - out << expr.getExpr(); - return out; - } - - friend bool eq(const BoundedZ3Expr &lhs, const BoundedZ3Expr &rhs) - { - return eq(lhs.getExpr(), rhs.getExpr()); - } - - inline BoundedZ3Expr simplify() const - { - return getExpr().simplify(); - } - - inline bool is_true() const - { - return getExpr().is_true(); - } - - inline bool is_int() const - { - return getExpr().is_int(); - } - - inline bool is_real() const - { - return getExpr().is_real(); - } - - inline s64_t getIntNumeral() const - { - assert(is_int() && "not an integer"); - int64_t i; - if (getExpr().is_numeral_i64(i)) - return (s64_t)get_numeral_int64(); - else - return (getExpr() < 0).simplify().is_true() ? INT64_MIN : INT64_MAX; - } - - inline double getRealNumeral() const - { - assert(is_real() && "not a real"); - std::string decstr = getExpr().get_decimal_string(10); - return std::stod(decstr); - } - - /// Return Numeral - inline s64_t getNumeral() const - { - int64_t i; - if (getExpr().is_numeral_i64(i)) - return (s64_t)get_numeral_int64(); - else - { - return (getExpr() < 0).simplify().is_true() ? INT64_MIN : INT64_MAX; - } - } - - s64_t bvLen() const; - //%} -}; // end class ConZ3Expr -} // end namespace SVF - -/// Specialise hash for ConZ3Expr -template<> -struct std::hash -{ - size_t operator()(const SVF::BoundedZ3Expr &z3Expr) const - { - return z3Expr.hash(); - } -}; -#endif //SVF_BOUNDEDZ3EXPR_H - diff --git a/svf/include/AE/Core/IntervalValue.h b/svf/include/AE/Core/IntervalValue.h index 7ad7a9b10..b50dd7300 100644 --- a/svf/include/AE/Core/IntervalValue.h +++ b/svf/include/AE/Core/IntervalValue.h @@ -31,8 +31,8 @@ #ifndef Z3_EXAMPLE_IntervalValue_H #define Z3_EXAMPLE_IntervalValue_H -#include "AE/Core/NumericLiteral.h" #include +#include "AE/Core/NumericValue.h" namespace SVF { @@ -44,10 +44,10 @@ class IntervalValue { private: // Lower bound - NumericLiteral _lb; + BoundedInt _lb; // Upper bound - NumericLiteral _ub; + BoundedInt _ub; // Invariant: isBottom() <=> _lb = 1 && _ub = 0 public: @@ -63,18 +63,18 @@ class IntervalValue } /// Get minus infinity -oo - static NumericLiteral minus_infinity() + static BoundedInt minus_infinity() { - return NumericLiteral::minus_infinity(); + return BoundedInt::minus_infinity(); } /// Get plus infinity +oo - static NumericLiteral plus_infinity() + static BoundedInt plus_infinity() { - return NumericLiteral::plus_infinity(); + return BoundedInt::plus_infinity(); } - static bool is_infinite(const NumericLiteral &e) + static bool is_infinite(const BoundedInt &e) { return e.is_infinity(); } @@ -103,16 +103,16 @@ class IntervalValue explicit IntervalValue(double n) : _lb(n), _ub(n) {} - explicit IntervalValue(NumericLiteral n) : IntervalValue(n, n) {} + explicit IntervalValue(BoundedInt n) : IntervalValue(n, n) {} /// Create the IntervalValue [lb, ub] - explicit IntervalValue(NumericLiteral lb, NumericLiteral ub) : _lb(std::move(lb)), _ub(std::move(ub)) {} + explicit IntervalValue(BoundedInt lb, BoundedInt ub) : _lb(std::move(lb)), _ub(std::move(ub)) {} - explicit IntervalValue(s64_t lb, s64_t ub) : IntervalValue(NumericLiteral(lb), NumericLiteral(ub)) {} + explicit IntervalValue(s64_t lb, s64_t ub) : IntervalValue(BoundedInt(lb), BoundedInt(ub)) {} - explicit IntervalValue(double lb, double ub) : IntervalValue(NumericLiteral(lb), NumericLiteral(ub)) {} + explicit IntervalValue(double lb, double ub) : IntervalValue(BoundedInt(lb), BoundedInt(ub)) {} - explicit IntervalValue(float lb, float ub) : IntervalValue(NumericLiteral(lb), NumericLiteral(ub)) {} + explicit IntervalValue(float lb, float ub) : IntervalValue(BoundedInt(lb), BoundedInt(ub)) {} explicit IntervalValue(s32_t lb, s32_t ub) : IntervalValue((s64_t) lb, (s64_t) ub) {} @@ -203,33 +203,33 @@ class IntervalValue ~IntervalValue() = default; /// Return the lower bound - const NumericLiteral &lb() const + const BoundedInt &lb() const { assert(!this->isBottom()); return this->_lb; } /// Return the upper bound - const NumericLiteral &ub() const + const BoundedInt &ub() const { assert(!this->isBottom()); return this->_ub; } /// Set the lower bound - void setLb(const NumericLiteral &lb) + void setLb(const BoundedInt &lb) { this->_lb = lb; } /// Set the upper bound - void setUb(const NumericLiteral &ub) + void setUb(const BoundedInt &ub) { this->_ub = ub; } /// Set the lower bound - void setValue(const NumericLiteral &lb, const NumericLiteral &ub) + void setValue(const BoundedInt &lb, const BoundedInt &ub) { this->_lb = lb; this->_ub = ub; @@ -249,18 +249,14 @@ class IntervalValue bool is_int() const { - bool lb_int = _lb.is_int(); - bool ub_int = _ub.is_int(); - assert (lb_int == ub_int && "lb and ub should be both int or both float"); - return _lb.is_int(); + return !is_real(); } bool is_real() const { bool lb_real = _lb.is_real(); bool ub_real = _ub.is_real(); - assert (lb_real == ub_real && "lb and ub should be both real or both int"); - return _lb.is_real(); + return lb_real || ub_real; } /// Return @@ -539,13 +535,13 @@ inline IntervalValue operator*(const IntervalValue &lhs, } else { - NumericLiteral ll = lhs.lb() * rhs.lb(); - NumericLiteral lu = lhs.lb() * rhs.ub(); - NumericLiteral ul = lhs.ub() * rhs.lb(); - NumericLiteral uu = lhs.ub() * rhs.ub(); - std::vector vec{ll, lu, ul, uu}; - return IntervalValue(NumericLiteral::min(vec), - NumericLiteral::max(vec)); + BoundedInt ll = lhs.lb() * rhs.lb(); + BoundedInt lu = lhs.lb() * rhs.ub(); + BoundedInt ul = lhs.ub() * rhs.lb(); + BoundedInt uu = lhs.ub() * rhs.ub(); + std::vector vec{ll, lu, ul, uu}; + return IntervalValue(BoundedInt::min(vec), + BoundedInt::max(vec)); } } @@ -564,14 +560,14 @@ inline IntervalValue operator/(const IntervalValue &lhs, else { // Neither the dividend nor the divisor contains 0 - NumericLiteral ll = lhs.lb() / rhs.lb(); - NumericLiteral lu = lhs.lb() / rhs.ub(); - NumericLiteral ul = lhs.ub() / rhs.lb(); - NumericLiteral uu = lhs.ub() / rhs.ub(); - std::vector vec{ll, lu, ul, uu}; + BoundedInt ll = lhs.lb() / rhs.lb(); + BoundedInt lu = lhs.lb() / rhs.ub(); + BoundedInt ul = lhs.ub() / rhs.lb(); + BoundedInt uu = lhs.ub() / rhs.ub(); + std::vector vec{ll, lu, ul, uu}; - return IntervalValue(NumericLiteral::min(vec), - NumericLiteral::max(vec)); + return IntervalValue(BoundedInt::min(vec), + BoundedInt::max(vec)); } } @@ -593,9 +589,9 @@ inline IntervalValue operator%(const IntervalValue &lhs, } else { - NumericLiteral n_ub = max(abs(lhs.lb()), abs(lhs.ub())); - NumericLiteral d_ub = max(abs(rhs.lb()), rhs.ub()) - 1; - NumericLiteral ub = min(n_ub, d_ub); + BoundedInt n_ub = max(abs(lhs.lb()), abs(lhs.ub())); + BoundedInt d_ub = max(abs(rhs.lb()), rhs.ub()) - 1; + BoundedInt ub = min(n_ub, d_ub); if (lhs.lb().getNumeral() < 0) { @@ -864,13 +860,13 @@ inline IntervalValue operator>>(const IntervalValue &lhs, const IntervalValue &r } else { - NumericLiteral ll = lhs.lb() >> shift.lb(); - NumericLiteral lu = lhs.lb() >> shift.ub(); - NumericLiteral ul = lhs.ub() >> shift.lb(); - NumericLiteral uu = lhs.ub() >> shift.ub(); - std::vector vec{ll, lu, ul, uu}; - return IntervalValue(NumericLiteral::min(vec), - NumericLiteral::max(vec)); + BoundedInt ll = lhs.lb() >> shift.lb(); + BoundedInt lu = lhs.lb() >> shift.ub(); + BoundedInt ul = lhs.ub() >> shift.lb(); + BoundedInt uu = lhs.ub() >> shift.ub(); + std::vector vec{ll, lu, ul, uu}; + return IntervalValue(BoundedInt::min(vec), + BoundedInt::max(vec)); } } } diff --git a/svf/include/AE/Core/NumericLiteral.h b/svf/include/AE/Core/NumericLiteral.h deleted file mode 100644 index c412be3df..000000000 --- a/svf/include/AE/Core/NumericLiteral.h +++ /dev/null @@ -1,478 +0,0 @@ -//===- NumericLiteral.h ----Number wrapper for domains------------------// -// -// SVF: Static Value-Flow Analysis -// -// Copyright (C) <2013-2022> -// - -// This program is free software: you can redistribute it and/or modify -// it under the terms of the GNU Affero General Public License as published by -// the Free Software Foundation, either version 3 of the License, or -// (at your option) any later version. - -// This program is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU Affero General Public License for more details. - -// You should have received a copy of the GNU Affero General Public License -// along with this program. If not, see . -// -//===----------------------------------------------------------------------===// -/* - * NumericLiteral.h - * - * Created on: Aug 4, 2022 - * Author: Xiao Cheng, Jiawei Wang - * - */ - -#ifndef Z3_EXAMPLE_Number_H -#define Z3_EXAMPLE_Number_H - -#include "Util/GeneralType.h" -#include "AE/Core/BoundedZ3Expr.h" - -namespace SVF -{ -class NumericLiteral -{ -private: - BoundedZ3Expr _n; - -public: - /// Default constructor - NumericLiteral() = delete; - - /// Create a new NumericLiteral from s32_t - - NumericLiteral(const Z3Expr &z3Expr) : _n(z3Expr) {} - - NumericLiteral(const z3::expr &e) : _n(e) {} - - NumericLiteral(float i) : _n(getContext().real_val(std::to_string(i).c_str())) {} - - NumericLiteral(double i) : _n(getContext().real_val(std::to_string(i).c_str())) {} - - NumericLiteral(s32_t i) : _n(i) {} - - NumericLiteral(s64_t i) : _n(i) {} - - NumericLiteral(BoundedZ3Expr z3Expr) : _n(std::move(z3Expr)) {} - - virtual ~NumericLiteral() = default; - - /// Copy Constructor - NumericLiteral(const NumericLiteral &) = default; - - /// Move Constructor - NumericLiteral(NumericLiteral &&) = default; - - /// Operator = , another Copy Constructor - inline NumericLiteral &operator=(const NumericLiteral &) = default; - - /// Operator = , another Move Constructor - inline NumericLiteral &operator=(NumericLiteral &&) = default; - - static NumericLiteral plus_infinity() - { - return BoundedZ3Expr::plus_infinity(); - } - - static NumericLiteral minus_infinity() - { - return BoundedZ3Expr::minus_infinity(); - } - - static z3::context &getContext() - { - return BoundedZ3Expr::getContext(); - } - - const std::string to_string() const - { - return _n.to_string(); - } - - /// Check if this is minus infinity - inline bool is_minus_infinity() const - { - return _n.is_minus_infinite(); - } - - /// Check if this is plus infinity - inline bool is_plus_infinity() const - { - return _n.is_plus_infinite(); - } - - /// Check if this is infinity (either of plus/minus) - inline bool is_infinity() const - { - return is_minus_infinity() || is_plus_infinity(); - } - - /// Check if this is zero - inline bool is_zero() const - { - return _n.is_zero(); - } - - inline bool is_int() const - { - return _n.is_int(); - } - - inline bool is_real() const - { - return _n.is_real(); - } - - /// Return Numeral, default type is double in case to support both int and float - inline s64_t getNumeral() const - { - return _n.getNumeral(); - } - - /// Return Expr - inline Z3Expr getExpr() const - { - return _n.getExpr(); - } - - inline double getRealNumeral() const - { - return _n.getRealNumeral(); - } - - inline s64_t getIntNumeral() const - { - return _n.getIntNumeral(); - } - - /// Check two object is equal - bool equal(const NumericLiteral &rhs) const - { - return eq(*this, rhs); - } - - /// Less then or equal - bool leq(const NumericLiteral &rhs) const - { - if (is_infinity() ^ rhs.is_infinity()) - { - if (is_infinity()) - { - return is_minus_infinity(); - } - else - { - return rhs.is_plus_infinity(); - } - } - if(is_infinity() && rhs.is_infinity()) - { - if(is_minus_infinity()) return true; - else return rhs.is_plus_infinity(); - } - else - return _n.leq(rhs._n).simplify().is_true(); - } - - // Greater than or equal - bool geq(const NumericLiteral &rhs) const - { - if (is_infinity() ^ rhs.is_infinity()) - { - if (is_infinity()) - { - return is_plus_infinity(); - } - else - { - return rhs.is_minus_infinity(); - } - } - if(is_infinity() && rhs.is_infinity()) - { - if(is_plus_infinity()) return true; - else return rhs.is_minus_infinity(); - } - else - return _n.geq(rhs._n).simplify().is_true(); - } - - - /// Reload operator - //{% - friend NumericLiteral operator==(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return eq(lhs, rhs) ? 1 : 0; - } - - friend NumericLiteral operator!=(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return !eq(lhs, rhs) ? 1 : 0; - } - - friend NumericLiteral operator>(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return (!lhs.leq(rhs)) ? 1 : 0; - } - - friend NumericLiteral operator<(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return (!lhs.geq(rhs)) ? 1 : 0; - } - - friend NumericLiteral operator<=(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return lhs.leq(rhs) ? 1 : 0; - } - - friend NumericLiteral operator>=(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return lhs.geq(rhs) ? 1 : 0; - } - - friend NumericLiteral operator+(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - if (!lhs.is_infinity() && !rhs.is_infinity()) - return (lhs._n + rhs._n).simplify(); - else if (!lhs.is_infinity() && rhs.is_infinity()) - return rhs; - else if (lhs.is_infinity() && !rhs.is_infinity()) - return lhs; - else if (eq(lhs, rhs)) - return lhs; - else - { - assert(false && "undefined operation +oo + -oo"); - abort(); - } - } - - friend NumericLiteral operator-(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - if (!lhs.is_infinity() && !rhs.is_infinity()) - return (lhs._n - rhs._n).simplify(); - else if (!lhs.is_infinity() && rhs.is_infinity()) - return -rhs; - else if (lhs.is_infinity() && !rhs.is_infinity()) - return lhs; - else if (!eq(lhs, rhs)) - return lhs; - else - { - assert(false && "undefined operation +oo - +oo"); - abort(); - } - } - - friend NumericLiteral operator*(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - if (lhs.is_zero() || rhs.is_zero()) - return 0; - else if (lhs.is_infinity() && rhs.is_infinity()) - return eq(lhs, rhs) ? plus_infinity() : minus_infinity(); - else if (lhs.is_infinity()) - return !rhs.leq(0) ? lhs : -lhs; - else if (rhs.is_infinity()) - return !lhs.leq(0) ? rhs : -rhs; - else - return (lhs._n * rhs._n).simplify(); - } - - friend NumericLiteral operator/(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - if (rhs.is_zero()) - { - - assert(false && "divide by zero"); - abort(); - } - else if (!lhs.is_infinity() && !rhs.is_infinity()) - return (lhs._n / rhs._n).simplify(); - else if (!lhs.is_infinity() && rhs.is_infinity()) - return 0; - else if (lhs.is_infinity() && !rhs.is_infinity()) - return !rhs.leq(0) ? lhs : -lhs; - else - // TODO: +oo/-oo L'Hôpital's rule? - return eq(lhs, rhs) ? plus_infinity() : minus_infinity(); - } - - friend NumericLiteral operator%(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - if (rhs.is_zero()) - { - assert(false && "divide by zero"); - abort(); - } - else if (!lhs.is_infinity() && !rhs.is_infinity()) - return (lhs._n % rhs._n).simplify(); - else if (!lhs.is_infinity() && rhs.is_infinity()) - return 0; - // TODO: not sure - else if (lhs.is_infinity() && !rhs.is_infinity()) - return !rhs.leq(0) ? lhs : -lhs; - else - // TODO: +oo/-oo L'Hôpital's rule? - return eq(lhs, rhs) ? plus_infinity() : minus_infinity(); - } - - // TODO: logic operation for infinity? - friend NumericLiteral operator^(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return (lhs._n ^ rhs._n).simplify(); - } - - friend NumericLiteral operator&(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return (lhs._n & rhs._n).simplify(); - } - - friend NumericLiteral operator|(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return (lhs._n | rhs._n).simplify(); - } - - friend NumericLiteral operator>>(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - assert(rhs.geq(0) && "rhs should be greater or equal than 0"); - if (lhs.is_zero()) - return lhs; - else if (lhs.is_infinity()) - return lhs; - else if (rhs.is_infinity()) - return lhs.geq(0) ? 0 : -1; - else - return (s32_t) lhs.getNumeral() >> (s32_t) rhs.getNumeral(); - } - - friend NumericLiteral operator<<(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - assert(rhs.geq(0) && "rhs should be greater or equal than 0"); - if (lhs.is_zero()) - return lhs; - else if (lhs.is_infinity()) - return lhs; - else if (rhs.is_infinity()) - return lhs.geq(0) ? plus_infinity() : minus_infinity(); - else - return (s32_t) lhs.getNumeral() << (s32_t) rhs.getNumeral(); - } - - friend NumericLiteral operator&&(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return (lhs._n && rhs._n).simplify(); - } - - friend NumericLiteral operator||(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return (lhs._n || rhs._n).simplify(); - } - - friend NumericLiteral operator!(const NumericLiteral &lhs) - { - return (!lhs._n).simplify(); - } - - friend NumericLiteral operator-(const NumericLiteral &lhs) - { - if (lhs.is_plus_infinity()) - { - return minus_infinity(); - } - else if (lhs.is_minus_infinity()) - { - return plus_infinity(); - } - else - return (-lhs._n).simplify(); - } - - /// Return ite? lhs : rhs - friend NumericLiteral ite(const NumericLiteral &cond, const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return ite(cond._n, lhs._n, rhs._n).simplify(); - } - - friend std::ostream &operator<<(std::ostream &out, const NumericLiteral &expr) - { - if (expr.is_plus_infinity()) - out << "+INF"; - else if (expr.is_minus_infinity()) - out << "-INF"; - else - out << expr._n; - return out; - } - - friend bool eq(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return eq(lhs._n, rhs._n); - } - - friend NumericLiteral min(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return lhs.leq(rhs) ? lhs : rhs; - } - - friend NumericLiteral max(const NumericLiteral &lhs, const NumericLiteral &rhs) - { - return lhs.leq(rhs) ? rhs : lhs; - } - - friend NumericLiteral abs(const NumericLiteral &lhs) - { - return lhs.leq(0) ? -lhs : lhs; - } - - // TODO: how to use initializer_list as argument? - static NumericLiteral min(std::vector& _l) - { - NumericLiteral ret(plus_infinity()); - for (const auto &it: _l) - { - if (it.is_minus_infinity()) - return minus_infinity(); - else if (!it.geq(ret)) - { - ret = it; - } - } - return ret; - } - - static NumericLiteral max(std::vector& _l) - { - NumericLiteral ret(minus_infinity()); - for (const auto &it: _l) - { - if (it.is_plus_infinity()) - return plus_infinity(); - else if (!it.leq(ret)) - { - ret = it; - } - } - return ret; - } - - //%} - - -}; // end class NumericLiteral -} // end namespace SVF - -/// Specialise hash for NumericLiteral -template<> -struct std::hash -{ - size_t operator()(const SVF::NumericLiteral &n) const - { - return n.getNumeral(); - } -}; -#endif //Z3_EXAMPLE_Number_H diff --git a/svf/include/AE/Core/NumericValue.h b/svf/include/AE/Core/NumericValue.h new file mode 100644 index 000000000..3ca170e45 --- /dev/null +++ b/svf/include/AE/Core/NumericValue.h @@ -0,0 +1,641 @@ +//===- NumericValue.h ----Numeric Value-------------------------// +// +// SVF: Static Value-Flow Analysis +// +// Copyright (C) <2013-2022> +// + +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. + +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. + +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . +// +//===----------------------------------------------------------------------===// +/* + * Numeri Value.h + * + * Created on: May 11, 2024 + * Author: Xiao Cheng, Jiawei Ren + * + */ + +#ifndef SVF_NUMERICVALUE_H +#define SVF_NUMERICVALUE_H + +#include "SVFIR/SVFType.h" +#include +#include // For DBL_MAX +#include + + +#define epsilon std::numeric_limits::epsilon(); +namespace SVF +{ + +/*! + * Bounded double numeric value + */ +class BoundedDouble +{ +protected: + + double _fVal; + + BoundedDouble() = default; + +public: + BoundedDouble(double fVal) : _fVal(fVal) {} + + BoundedDouble(const BoundedDouble& rhs) : _fVal(rhs._fVal) {} + + BoundedDouble& operator=(const BoundedDouble& rhs) + { + _fVal = rhs._fVal; + return *this; + } + + BoundedDouble(BoundedDouble &&rhs) : _fVal(std::move(rhs._fVal)) {} + + BoundedDouble& operator=(BoundedDouble&& rhs) { + _fVal = std::move(rhs._fVal); + return *this; + } + + virtual ~BoundedDouble() {} + + + static bool doubleEqual(double a, double b) { + if (std::isinf(a) && std::isinf(b)) + return a == b; + return std::fabs(a - b) < epsilon; + } + + const double getFVal() const { + return _fVal; + } + + bool is_plus_infinity() const + { + return _fVal == std::numeric_limits::infinity(); + } + + bool is_minus_infinity() const + { + return _fVal == -std::numeric_limits::infinity(); + } + + bool is_infinity() const + { + return is_plus_infinity() || is_minus_infinity(); + } + + void set_plus_infinity() + { + *this = plus_infinity(); + } + + void set_minus_infinity() + { + *this = minus_infinity(); + } + + static BoundedDouble plus_infinity() + { + return std::numeric_limits::infinity(); + } + + static BoundedDouble minus_infinity() + { + return -std::numeric_limits::infinity(); + } + + + bool is_zero() const + { + return doubleEqual(_fVal, 0.0f); + } + + static bool isZero(const BoundedDouble &expr) + { + return doubleEqual(expr.getFVal(), 0.0f); + } + + bool equal(const BoundedDouble &rhs) const + { + return doubleEqual(_fVal, rhs._fVal); + } + + bool leq(const BoundedDouble &rhs) const + { + if (is_infinity() ^ rhs.is_infinity()) + { + if (is_infinity()) + { + return is_minus_infinity(); + } + else + { + return rhs.is_plus_infinity(); + } + } + if(is_infinity() && rhs.is_infinity()) + { + if(is_minus_infinity()) return true; + else return rhs.is_plus_infinity(); + } + else + return _fVal <= rhs._fVal; + } + + bool geq(const BoundedDouble &rhs) const + { + if (is_infinity() ^ rhs.is_infinity()) + { + if (is_infinity()) + { + return is_plus_infinity(); + } + else + { + return rhs.is_minus_infinity(); + } + } + if(is_infinity() && rhs.is_infinity()) + { + if(is_plus_infinity()) return true; + else return rhs.is_minus_infinity(); + } + else + return _fVal >= rhs._fVal; + } + + /// Reload operator + //{% + friend BoundedDouble operator==(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return lhs.equal(rhs); + } + + friend BoundedDouble operator!=(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return !lhs.equal(rhs); + } + + friend BoundedDouble operator>(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return !lhs.leq(rhs); + } + + friend BoundedDouble operator<(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return !lhs.geq(rhs); + } + + friend BoundedDouble operator<=(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return lhs.leq(rhs); + } + + friend BoundedDouble operator>=(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return lhs.geq(rhs); + } + + /** + * Adds two floating-point numbers safely, checking for overflow and + * underflow conditions. + * + * @param lhs Left-hand side operand of the addition. + * @param rhs Right-hand side operand of the addition. + * @return The sum of lhs and rhs. If overflow or underflow occurs, returns + * positive or negative infinity. + */ + static double safeAdd(double lhs, double rhs) + { + if ((lhs == std::numeric_limits::infinity() && + rhs == -std::numeric_limits::infinity()) || + (lhs == -std::numeric_limits::infinity() && + rhs == std::numeric_limits::infinity())) { + assert(false && "invalid add"); + } + double res = + lhs + rhs; // Perform the addition and store the result in 'res' + + // Check if the result is positive infinity due to overflow + if (res == std::numeric_limits::infinity()) + { + return res; // Positive overflow has occurred, return positive + // infinity + } + + // Check if the result is negative infinity, which can indicate a large + // negative overflow + if (res == -std::numeric_limits::infinity()) + { + return res; // Negative "overflow", effectively an underflow to + // negative infinity + } + + // Check for positive overflow: verify if both operands are positive and + // their sum exceeds the maximum double value + if (lhs > 0 && rhs > 0 && + (std::numeric_limits::max() - lhs) < rhs) + { + res = + std::numeric_limits::infinity(); // Set result to + // positive infinity to + // indicate overflow + return res; + } + + // Check for an underflow scenario: both numbers are negative and their + // sum is more negative than what double can represent + if (lhs < 0 && rhs < 0 && + (-std::numeric_limits::max() - lhs) > rhs) + { + res = -std::numeric_limits< + double>::infinity(); // Set result to negative infinity to + // clarify extreme negative sum + return res; + } + + // If none of the above conditions are met, return the result of the + // addition + return res; + } + + friend BoundedDouble operator+(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return safeAdd(lhs._fVal, rhs._fVal); + } + + friend BoundedDouble operator-(const BoundedDouble &lhs) + { + return -lhs._fVal; + } + + friend BoundedDouble operator-(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return safeAdd(lhs._fVal, -rhs._fVal); + } + + /** + * Safely multiplies two floating-point numbers, checking for overflow and + * underflow. + * + * @param lhs Left-hand side operand of the multiplication. + * @param rhs Right-hand side operand of the multiplication. + * @return The product of lhs and rhs. If overflow or underflow occurs, + * returns positive or negative infinity accordingly. + */ + static double safeMul(double lhs, double rhs) + { + if (doubleEqual(lhs, 0.0f) || doubleEqual(rhs, 0.0f)) + return 0.0f; + double res = lhs * rhs; + // Check if the result is positive infinity due to overflow + if (res == std::numeric_limits::infinity()) + { + return res; // Positive overflow has occurred, return positive + // infinity + } + + // Check if the result is negative infinity, which can indicate a large + // negative overflow + if (res == -std::numeric_limits::infinity()) + { + return res; // Negative "overflow", effectively an underflow to + // negative infinity + } + // Check for overflow scenarios + if (lhs > 0 && rhs > 0 && lhs > std::numeric_limits::max() / rhs) + { + return std::numeric_limits::infinity(); + } + if (lhs < 0 && rhs < 0 && lhs < std::numeric_limits::max() / rhs) + { + return std::numeric_limits::infinity(); + } + + // Check for "underflow" scenarios (negative overflow) + if (lhs > 0 && rhs < 0 && + rhs < std::numeric_limits::lowest() / lhs) + { + return -std::numeric_limits::infinity(); + } + if (lhs < 0 && rhs > 0 && + lhs < std::numeric_limits::lowest() / rhs) + { + return -std::numeric_limits::infinity(); + } + + return res; // If no overflow or underflow, return the product + } + + friend BoundedDouble operator*(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return safeMul(lhs._fVal, rhs._fVal); + } + + /** + * Safely divides one floating-point number by another, checking for + * division by zero and overflow. + * + * @param lhs Left-hand side operand (numerator). + * @param rhs Right-hand side operand (denominator). + * @return The quotient of lhs and rhs. Returns positive or negative + * infinity for division by zero, or when overflow occurs. + */ + static double safeDiv(double lhs, double rhs) + { + // Check for division by zero + if (doubleEqual(rhs, 0.0f)) + { + return (lhs >= 0.0f) ? std::numeric_limits::infinity() + : -std::numeric_limits::infinity(); + } + double res = lhs / rhs; + // Check if the result is positive infinity due to overflow + if (res == std::numeric_limits::infinity()) + { + return res; // Positive overflow has occurred, return positive + // infinity + } + + // Check if the result is negative infinity, which can indicate a large + // negative overflow + if (res == -std::numeric_limits::infinity()) + { + return res; // Negative "overflow", effectively an underflow to + // negative infinity + } + + // Check for overflow when dividing small numbers + if (rhs > 0 && rhs < std::numeric_limits::min() && + lhs > std::numeric_limits::max() * rhs) + { + return std::numeric_limits::infinity(); + } + if (rhs < 0 && rhs > -std::numeric_limits::min() && + lhs > std::numeric_limits::max() * rhs) + { + return -std::numeric_limits::infinity(); + } + + return res; // If no special cases, return the quotient + } + + friend BoundedDouble operator/(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return safeDiv(lhs._fVal, rhs._fVal); + } + + friend BoundedDouble operator%(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + if (rhs.is_zero()) assert(false && "divide by zero"); + else if (!lhs.is_infinity() && !rhs.is_infinity()) + return std::fmod(lhs._fVal, rhs._fVal); + else if (!lhs.is_infinity() && rhs.is_infinity()) + return 0.0f; + // TODO: not sure + else if (lhs.is_infinity() && !rhs.is_infinity()) + return ite(rhs._fVal > 0.0f, lhs, -lhs); + else + // TODO: +oo/-oo L'Hôpital's rule? + return eq(lhs, rhs) ? plus_infinity() : minus_infinity(); + abort(); + } + + inline bool is_int() const { + return _fVal == std::round(_fVal); + } + inline bool is_real() const { + return !is_int(); + } + + friend BoundedDouble operator^(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + int lInt = std::round(rhs._fVal), rInt = std::round(rhs._fVal); + return lInt ^ rInt; + } + + friend BoundedDouble operator&(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + int lInt = std::round(rhs._fVal), rInt = std::round(rhs._fVal); + return lInt & rInt; + } + + friend BoundedDouble operator|(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + int lInt = std::round(rhs._fVal), rInt = std::round(rhs._fVal); + return lInt | rInt; + } + + + friend BoundedDouble operator&&(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return lhs._fVal && rhs._fVal; + } + + friend BoundedDouble operator||(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return lhs._fVal || rhs._fVal; + } + + friend BoundedDouble operator!(const BoundedDouble &lhs) + { + return !lhs._fVal; + } + + friend BoundedDouble operator>>(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + assert(rhs.geq(0) && "rhs should be greater or equal than 0"); + if (lhs.is_zero()) + return lhs; + else if (lhs.is_infinity()) + return lhs; + else if (rhs.is_infinity()) + return lhs.geq(0) ? 0 : -1; + else + return (s32_t) lhs.getNumeral() >> (s32_t) rhs.getNumeral(); + } + + friend BoundedDouble operator<<(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + assert(rhs.geq(0) && "rhs should be greater or equal than 0"); + if (lhs.is_zero()) + return lhs; + else if (lhs.is_infinity()) + return lhs; + else if (rhs.is_infinity()) + return lhs.geq(0) ? plus_infinity() : minus_infinity(); + else + return (s32_t) lhs.getNumeral() << (s32_t) rhs.getNumeral(); + } + + friend BoundedDouble ite(const BoundedDouble& cond, const BoundedDouble& lhs, + const BoundedDouble& rhs) + { + return cond._fVal != 0.0f ? lhs._fVal : rhs._fVal; + } + + friend std::ostream &operator<<(std::ostream &out, const BoundedDouble &expr) + { + out << expr._fVal; + return out; + } + + friend bool eq(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return doubleEqual(lhs._fVal, rhs._fVal); + } + + friend BoundedDouble min(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return std::min(lhs._fVal, rhs._fVal); + } + + friend BoundedDouble max(const BoundedDouble &lhs, const BoundedDouble &rhs) + { + return std::max(lhs._fVal, rhs._fVal); + } + + static BoundedDouble min(std::vector& _l) + { + BoundedDouble ret(plus_infinity()); + for (const auto &it: _l) + { + if (it.is_minus_infinity()) + return minus_infinity(); + else if (!it.geq(ret)) + { + ret = it; + } + } + return ret; + } + + static BoundedDouble max(std::vector& _l) + { + BoundedDouble ret(minus_infinity()); + for (const auto &it: _l) + { + if (it.is_plus_infinity()) + return plus_infinity(); + else if (!it.leq(ret)) + { + ret = it; + } + } + return ret; + } + + friend BoundedDouble abs(const BoundedDouble &lhs) + { + return lhs.leq(0) ? -lhs : lhs; + } + + inline bool is_true() const + { + return _fVal != 0.0f; + } + + /// Return Numeral + inline s64_t getNumeral() const + { + if (is_minus_infinity()) + { + return INT64_MIN; + } + else if (is_plus_infinity()) + { + return INT64_MAX; + } + else + { + return std::round(_fVal); + } + } + + inline s64_t getIntNumeral() const { + return getNumeral(); + } + + inline double getRealNumeral() const { + return _fVal; + } + + inline virtual const std::string to_string() const { + return std::to_string(_fVal); + } + + //%} +}; // end class BoundedDouble + +class BoundedInt : public BoundedDouble +{ +private: + BoundedInt() = default; + +public: + + BoundedInt(s32_t val) { + _fVal = val; + } + + BoundedInt(s64_t val) { + _fVal = val; + } + + BoundedInt(const BoundedInt& rhs) { + _fVal = rhs._fVal; + } + + BoundedInt& operator=(const BoundedInt& rhs) + { + _fVal = rhs._fVal; + return *this; + } + + BoundedInt(BoundedInt&& rhs) { + _fVal = rhs._fVal; + } + + BoundedInt& operator=(const BoundedInt&& rhs) + { + _fVal = rhs._fVal; + return *this; + } + + BoundedInt(double val) { + _fVal = val; + } + + BoundedInt(const BoundedDouble& f) { + _fVal = f.getFVal(); + } + + virtual ~BoundedInt() {} + + inline const std::string to_string() const override + { + if (is_minus_infinity()) + return "-∞"; + else if (is_plus_infinity()) + return "∞"; + else + return std::to_string(getIntNumeral()); + } +}; + +} // end namespace SVF + +#endif // SVF_NUMERICVALUE_H diff --git a/svf/include/AE/Core/RelationSolver.h b/svf/include/AE/Core/RelationSolver.h index f15fe9fe8..cd1fc7d25 100644 --- a/svf/include/AE/Core/RelationSolver.h +++ b/svf/include/AE/Core/RelationSolver.h @@ -58,24 +58,31 @@ class RelationSolver /// Return Z3 expression lazily based on SVFVar ID - virtual inline Z3Expr toZ3Expr(u32_t varId) const + virtual inline Z3Expr toIntZ3Expr(u32_t varId) const { return Z3Expr::getContext().int_const(std::to_string(varId).c_str()); } + inline Z3Expr toIntVal(s32_t f) const { + return Z3Expr::getContext().int_val(f); + } + inline Z3Expr toRealVal(BoundedDouble f) const { + return Z3Expr::getContext().real_val(std::to_string(f.getFVal()).c_str()); + } + /* two optional solvers: RSY and bilateral */ AbstractState bilateral(const AbstractState& domain, const Z3Expr &phi, u32_t descend_check = 0); AbstractState RSY(const AbstractState& domain, const Z3Expr &phi); - Map BoxedOptSolver(const Z3Expr& phi, Map& ret, Map& low_values, Map& high_values); + Map BoxedOptSolver(const Z3Expr& phi, Map& ret, Map& low_values, Map& high_values); AbstractState BS(const AbstractState& domain, const Z3Expr &phi); - void updateMap(Map& map, u32_t key, const NumericLiteral& value); + void updateMap(Map& map, u32_t key, const s32_t& value); - void decide_cpa_ext(const Z3Expr &phi, Map&, Map&, Map&, Map&, Map&); + void decide_cpa_ext(const Z3Expr &phi, Map&, Map&, Map&, Map&, Map&); }; } diff --git a/svf/lib/AE/Core/BoundedZ3Expr.cpp b/svf/lib/AE/Core/BoundedZ3Expr.cpp deleted file mode 100644 index b1e578ff2..000000000 --- a/svf/lib/AE/Core/BoundedZ3Expr.cpp +++ /dev/null @@ -1,64 +0,0 @@ -//===- BoundedZ3Expr.cpp ----Address Value Sets-------------------------// -// -// SVF: Static Value-Flow Analysis -// -// Copyright (C) <2013-2022> -// - -// This program is free software: you can redistribute it and/or modify -// it under the terms of the GNU Affero General Public License as published by -// the Free Software Foundation, either version 3 of the License, or -// (at your option) any later version. - -// This program is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU Affero General Public License for more details. - -// You should have received a copy of the GNU Affero General Public License -// along with this program. If not, see . -// -//===----------------------------------------------------------------------===// -/* - * BoundedZ3Expr.cpp - * - * Created on: Mar 20, 2023 - * Author: Xiao Cheng - * - */ -#include "AE/Core/BoundedZ3Expr.h" -#include "Util/Options.h" - -using namespace SVF; - -s64_t BoundedZ3Expr::bvLen() const -{ - if(is_infinite()) return (s64_t)Options::MaxBVLen(); - // No overflow - if(getNumeral() != INT64_MIN && getNumeral() != INT64_MAX) return (s64_t)Options::MaxBVLen(); - // Create a symbolic variable - Z3Expr x = getContext().real_const("x"); - Z3Expr y = getContext().real_const("y"); - - // Add constraints and assertions - Z3Expr constraint1 = x > 0; // x > 0 - Z3Expr constraint2 = x == z3::pw(2, y.getExpr()); // x = 2^y, where y is a real variable - Z3Expr assertions = constraint1 && constraint2; - Z3Expr::getSolver().push(); - // Add assertions to the solver - Z3Expr::getSolver().add(assertions.getExpr()); - - // Check for a solution - if (solver->check() == z3::sat) - { - z3::model model = solver->get_model(); - Z3Expr log2_x = model.eval(y.getExpr(), true); - Z3Expr::getSolver().pop(); - return (s64_t)BoundedZ3Expr(log2_x + 1).simplify().getNumeral(); - } - else - { - Z3Expr::getSolver().pop(); - return (s64_t)Options::MaxBVLen(); - } -} \ No newline at end of file diff --git a/svf/lib/AE/Core/RelationSolver.cpp b/svf/lib/AE/Core/RelationSolver.cpp index b3fdf753a..366c3a9d2 100644 --- a/svf/lib/AE/Core/RelationSolver.cpp +++ b/svf/lib/AE/Core/RelationSolver.cpp @@ -205,7 +205,7 @@ Z3Expr RelationSolver::gamma_hat(const AbstractState& exeState) const return Z3Expr::getContext().bool_val(false); if (item.second.isTop()) continue; - Z3Expr v = toZ3Expr(item.first); + Z3Expr v = toIntZ3Expr(item.first); res = (res && v >= (int)item.second.lb().getNumeral() && v <= (int)item.second.ub().getNumeral()).simplify(); } @@ -223,7 +223,7 @@ Z3Expr RelationSolver::gamma_hat(const AbstractState& alpha, return Z3Expr::getContext().bool_val(false); if (interval.isTop()) continue; - Z3Expr v = toZ3Expr(item.first); + Z3Expr v = toIntZ3Expr(item.first); res = (res && v >= (int)interval.lb().getNumeral() && v <= (int)interval.ub().getNumeral()).simplify(); } @@ -234,7 +234,7 @@ Z3Expr RelationSolver::gamma_hat(u32_t id, const AbstractState& exeState) const { auto it = exeState.getVarToVal().find(id); assert(it != exeState.getVarToVal().end() && "id not in varToVal?"); - Z3Expr v = toZ3Expr(id); + Z3Expr v = toIntZ3Expr(id); // Z3Expr v = Z3Expr::getContext().int_const(std::to_string(id).c_str()); Z3Expr res = (v >= (int)it->second.lb().getNumeral() && v <= (int)it->second.ub().getNumeral()); @@ -253,7 +253,7 @@ AbstractState RelationSolver::beta(const Map& sigma, return res; } -void RelationSolver::updateMap(Map& map, u32_t key, const NumericLiteral& value) +void RelationSolver::updateMap(Map& map, u32_t key, const s32_t& value) { auto it = map.find(key); if (it == map.end()) @@ -271,25 +271,25 @@ AbstractState RelationSolver::BS(const AbstractState& domain, const Z3Expr &phi) /// because key of _varToItvVal is u32_t, -key may out of range for int /// so we do key + bias for -key u32_t bias = 0; - s32_t infinity = INT32_MAX - 1; + s32_t infinity = INT32_MAX/2 - 1; // int infinity = (INT32_MAX) - 1; // int infinity = 20; - Map ret; - Map low_values, high_values; + Map ret; + Map low_values, high_values; Z3Expr new_phi = phi; /// init low, ret, high for (const auto& item: domain.getVarToVal()) { - updateMap(ret, item.first, item.second.ub()); + updateMap(ret, item.first, item.second.ub().getFVal()); if (item.second.lb().is_minus_infinity()) updateMap(low_values, item.first, -infinity); else - updateMap(low_values, item.first, item.second.lb()); + updateMap(low_values, item.first, item.second.lb().getFVal()); if (item.second.ub().is_plus_infinity()) updateMap(high_values, item.first, infinity); else - updateMap(high_values, item.first, item.second.ub()); + updateMap(high_values, item.first, item.second.ub().getFVal()); if (item.first > bias) bias = item.first + 1; } @@ -297,17 +297,17 @@ AbstractState RelationSolver::BS(const AbstractState& domain, const Z3Expr &phi) { /// init objects -x u32_t reverse_key = item.first + bias; - updateMap(ret, reverse_key, -item.second.lb()); + updateMap(ret, reverse_key, -item.second.lb().getFVal()); if (item.second.ub().is_plus_infinity()) updateMap(low_values, reverse_key, -infinity); else - updateMap(low_values, reverse_key, -item.second.ub()); + updateMap(low_values, reverse_key, -item.second.ub().getFVal()); if (item.second.lb().is_minus_infinity()) updateMap(high_values, reverse_key, infinity); else - updateMap(high_values, reverse_key, -item.second.lb()); + updateMap(high_values, reverse_key, -item.second.lb().getFVal()); /// add a relation that x == -(x+bias) - new_phi = (new_phi && (toZ3Expr(reverse_key) == -1 * toZ3Expr(item.first))); + new_phi = (new_phi && (toIntZ3Expr(reverse_key) == -1 * toIntZ3Expr(item.first))); } /// optimize each object BoxedOptSolver(new_phi.simplify(), ret, low_values, high_values); @@ -317,38 +317,38 @@ AbstractState RelationSolver::BS(const AbstractState& domain, const Z3Expr &phi) { if (item.first >= bias) { - if (item.second.equal(infinity)) - retInv[item.first - bias].getInterval().setLb(Z3Expr::getContext().int_const("-oo")); + if (item.second == (infinity)) + retInv[item.first - bias].getInterval().setLb(BoundedDouble::minus_infinity()); else - retInv[item.first - bias].getInterval().setLb(-item.second); + retInv[item.first - bias].getInterval().setLb(float(-item.second)); } else { - if (item.second.equal(infinity)) - retInv[item.first].getInterval().setUb(Z3Expr::getContext().int_const("+oo")); + if (item.second == (infinity)) + retInv[item.first].getInterval().setUb(BoundedDouble::plus_infinity()); else - retInv[item.first].getInterval().setUb(item.second); + retInv[item.first].getInterval().setUb(float(item.second)); } } return retInv; } -Map RelationSolver::BoxedOptSolver(const Z3Expr& phi, Map& ret, Map& low_values, Map& high_values) +Map RelationSolver::BoxedOptSolver(const Z3Expr& phi, Map& ret, Map& low_values, Map& high_values) { /// this is the S in the original paper Map L_phi; - Map mid_values; + Map mid_values; while (1) { L_phi.clear(); for (const auto& item : ret) { - Z3Expr v = toZ3Expr(item.first); - if (low_values.at(item.first).leq(high_values.at(item.first))) + Z3Expr v = toIntZ3Expr(item.first); + if (low_values.at(item.first) <= (high_values.at(item.first))) { - NumericLiteral mid = (low_values.at(item.first) + (high_values.at(item.first) - low_values.at(item.first)) / 2); + s32_t mid = (low_values.at(item.first) + (high_values.at(item.first) - low_values.at(item.first)) / 2); updateMap(mid_values, item.first, mid); - Z3Expr expr = (mid.getExpr() <= v && v <= high_values.at(item.first).getExpr()); + Z3Expr expr = (toIntVal(mid) <= v && v <= toIntVal(high_values.at(item.first))); L_phi[item.first] = expr; } } @@ -363,10 +363,10 @@ Map RelationSolver::BoxedOptSolver(const Z3Expr& phi, Map void RelationSolver::decide_cpa_ext(const Z3Expr& phi, Map& L_phi, - Map& mid_values, - Map& ret, - Map& low_values, - Map& high_values) + Map& mid_values, + Map& ret, + Map& low_values, + Map& high_values) { while (1) { @@ -387,24 +387,24 @@ void RelationSolver::decide_cpa_ext(const Z3Expr& phi, for(const auto & item : L_phi) { u32_t id = item.first; - int value = m.eval(toZ3Expr(id).getExpr()).get_numeral_int(); + int value = m.eval(toIntZ3Expr(id).getExpr()).get_numeral_int(); // int value = m.eval(Z3Expr::getContext().int_const(std::to_string(id).c_str())).get_numeral_int(); /// id is the var id, value is the solution found for var_id /// add a relation to check if the solution meets phi_id - Z3Expr expr = (item.second && toZ3Expr(id) == value); + Z3Expr expr = (item.second && toIntZ3Expr(id) == value); solver.push(); solver.add(expr.getExpr()); // solution meets phi_id if (solver.check() == z3::sat) { - updateMap(ret, id, NumericLiteral(value)); + updateMap(ret, id, (value)); updateMap(low_values, id, ret.at(id) + 1); - NumericLiteral mid = (low_values.at(id) + high_values.at(id) + 1) / 2; + s32_t mid = (low_values.at(id) + high_values.at(id) + 1) / 2; updateMap(mid_values, id, mid); - Z3Expr v = toZ3Expr(id); + Z3Expr v = toIntZ3Expr(id); // Z3Expr v = Z3Expr::getContext().int_const(std::to_string(id).c_str()); - Z3Expr expr = (mid_values.at(id).getExpr() <= v && v <= high_values.at(id).getExpr()); + Z3Expr expr = (toIntVal(mid_values.at(id)) <= v && v <= toIntVal(high_values.at(id))); L_phi[id] = expr; } solver.pop(); diff --git a/svf/lib/AE/Svfexe/SVFIR2AbsState.cpp b/svf/lib/AE/Svfexe/SVFIR2AbsState.cpp index 5c2d05cea..88f0b9346 100644 --- a/svf/lib/AE/Svfexe/SVFIR2AbsState.cpp +++ b/svf/lib/AE/Svfexe/SVFIR2AbsState.cpp @@ -150,7 +150,7 @@ AbstractValue SVFIR2AbsState::getZExtValue(const AbstractState& es, const SVFVar return IntervalValue::top(); // TODO: may have better solution } } - assert(false && "cannot support non-integer type"); + return IntervalValue::top(); // TODO: may have better solution } AbstractValue SVFIR2AbsState::getSExtValue(const AbstractState& es, const SVFVar* var)