From 5754321484b193cfe42e1e64bd193b30250d4d3d Mon Sep 17 00:00:00 2001 From: Jostar Date: Wed, 4 Sep 2024 10:05:48 +0800 Subject: [PATCH] [feat] add github action build-ubuntu workflow --- .github/workflows/build-ubuntu.yaml | 53 ++ include/dfa/domain/dom_base.hpp | 2 +- include/dfa/domain/map/map_domain.hpp | 2 +- .../domain/map/separate_numerical_domain.hpp | 2 +- include/dfa/domain/num/machine_qnum.hpp | 0 include/dfa/domain/num/qnum.hpp | 583 ++++++++++++++++++ .../dfa/domain/numerical/numerical_base.hpp | 2 +- include/util/log.hpp | 3 +- src/dfa/proc_cfg.cpp | 4 +- src/dfa/program_state.cpp | 12 +- tools/CMakeLists.txt | 3 +- 11 files changed, 652 insertions(+), 14 deletions(-) create mode 100644 .github/workflows/build-ubuntu.yaml delete mode 100644 include/dfa/domain/num/machine_qnum.hpp create mode 100644 include/dfa/domain/num/qnum.hpp diff --git a/.github/workflows/build-ubuntu.yaml b/.github/workflows/build-ubuntu.yaml new file mode 100644 index 0000000..53dec18 --- /dev/null +++ b/.github/workflows/build-ubuntu.yaml @@ -0,0 +1,53 @@ +name: Build on Ubuntu +on: + push: + branches: [ "main" ] + pull_request: + branches: [ "main" ] +jobs: + build-ubuntu: + runs-on: ubuntu-24.04 + steps: + - name: Checkout Repo + uses: actions/checkout@v4 + + - name: Install Dependencies + run: | + echo "deb http://apt.llvm.org/noble/ llvm-toolchain-noble main" | sudo tee /etc/apt/sources.list.d/llvm.list + echo "deb-src http://apt.llvm.org/noble/ llvm-toolchain-noble main" | sudo tee -a /etc/apt/sources.list.d/llvm.list + echo "deb http://apt.llvm.org/noble/ llvm-toolchain-noble-18 main" | sudo tee -a /etc/apt/sources.list.d/llvm.list + echo "deb-src http://apt.llvm.org/noble/ llvm-toolchain-noble-18 main" | sudo tee -a /etc/apt/sources.list.d/llvm.list + echo "deb http://apt.llvm.org/noble/ llvm-toolchain-noble-19 main" | sudo tee -a /etc/apt/sources.list.d/llvm.list + echo "deb-src http://apt.llvm.org/noble/ llvm-toolchain-noble-19 main" | sudo tee -a /etc/apt/sources.list.d/llvm.list + wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | sudo apt-key add - + sudo apt-get update + sudo apt-get install --yes \ + gcc g++ cmake libgmp-dev libedit-dev \ + python3 python3-pip \ + llvm-18 llvm-18-dev llvm-18-tools clang-18 libclang-18-dev + + - name: Spell Check + uses: crate-ci/typos@v1.24.3 + + - name: Clang Format + run: | + chmod +x scripts/run-clang-format + scripts/run-clang-format + + - name: Build Repo + run: | + cmake -DCMAKE_BUILD_TYPE:STRING=Release -DLINK_LLVM_DYLIB=ON -DCMAKE_C_COMPILER:STRING=/usr/bin/gcc -DCMAKE_CXX_COMPILER:STRING=/usr/bin/g++ -DCMAKE_EXPORT_COMPILE_COMMANDS:BOOL=TRUE -DCMAKE_INSTALL_PREFIX="/opt/knight" -DLLVM_BUILD_DIR="/usr/lib/llvm-18" -B build + cmake --build build -j16 + cmake --install build + echo $(pwd)/build/bin >> $GITHUB_PATH + + - name: Test Binary + run: | + knight --help + + - name: Unit Tests + run: | + pwd + chmod +x scripts/unittest + scripts/unittest run test/testcase/ + \ No newline at end of file diff --git a/include/dfa/domain/dom_base.hpp b/include/dfa/domain/dom_base.hpp index 85e5ddd..5f007d2 100644 --- a/include/dfa/domain/dom_base.hpp +++ b/include/dfa/domain/dom_base.hpp @@ -187,7 +187,7 @@ get_domain_bottom_val_fn(DomID id) { template < typename Derived > class AbsDom : public AbsDomBase { public: - AbsDom< Derived >() : AbsDomBase(Derived::get_kind()) {} + AbsDom() : AbsDomBase(Derived::get_kind()) {} void join_with(const AbsDomBase& other) override { static_assert(does_derived_dom_can_join_with< Derived >::value, diff --git a/include/dfa/domain/map/map_domain.hpp b/include/dfa/domain/map/map_domain.hpp index 8e44051..94a125c 100644 --- a/include/dfa/domain/map/map_domain.hpp +++ b/include/dfa/domain/map/map_domain.hpp @@ -75,7 +75,7 @@ class MapDom : public AbsDom< MapDom< Key, SeparateValue, domain_kind > > { } else if (value.is_top()) { this->forget(key); } else { - this->m_table.insert_or_assign(key, value); + this->m_table[key] = value; } } diff --git a/include/dfa/domain/map/separate_numerical_domain.hpp b/include/dfa/domain/map/separate_numerical_domain.hpp index 8fe6128..c597f81 100644 --- a/include/dfa/domain/map/separate_numerical_domain.hpp +++ b/include/dfa/domain/map/separate_numerical_domain.hpp @@ -91,7 +91,7 @@ class SeparateNumericalDom } else if (value.is_top()) { this->forget(key); } else { - this->m_table.insert_or_assign(key, value); + this->m_table[key] = value; } } diff --git a/include/dfa/domain/num/machine_qnum.hpp b/include/dfa/domain/num/machine_qnum.hpp deleted file mode 100644 index e69de29..0000000 diff --git a/include/dfa/domain/num/qnum.hpp b/include/dfa/domain/num/qnum.hpp new file mode 100644 index 0000000..126ef41 --- /dev/null +++ b/include/dfa/domain/num/qnum.hpp @@ -0,0 +1,583 @@ +//===- qnum.hpp -------------------------------------------------------===// +// +// Copyright (c) 2024 Junjie Shen +// +// see https://github.com/shenjunjiekoda/knight/blob/main/LICENSE for +// license information. +// +//===------------------------------------------------------------------===// +// +// This file defines the QNum class, which is a wrapper around GMP's +// mpz_class +// +//===------------------------------------------------------------------===// + +#pragma once + +#include +#include "util/log.hpp" + +#include +#include +#include +#include +#include + +#include + +#include + +#include "util/assert.hpp" +#include "znum.hpp" + +namespace knight::dfa { + +template < typename T > +struct ZNumOrIntegral : public std::is_integral< T > {}; + +template <> +struct ZNumOrIntegral< const ZNum& > : public std::true_type {}; + +namespace internal { + +template < typename T > +struct ZNumTransformer : public MpzTransformer< T > {}; + +template <> +struct ZNumTransformer< const ZNum& > { + const mpz_class& operator()(const ZNum& n) { return n.get_mpz(); } +}; + +} // namespace internal + +/// \brief Class for unlimited precision rationals +class QNum : public llvm::FoldingSetNode { + private: + mpq_class m_mpq; + + public: + [[nodiscard]] static std::optional< QNum > from_string( + const std::string& str, int base = internal::K10Base) { + try { + return QNum(mpq_class(str, base)); + } catch (std::invalid_argument&) { + llvm::WithColor::error() + << "QNum: invalid input string '" << str << "'\n"; + return std::nullopt; + } + } + + [[nodiscard]] const mpq_class& get_mpq() const { return this->m_mpq; } + + QNum() = default; + explicit QNum(const ZNum& n) : m_mpq(n.m_mpz) {} + explicit QNum(ZNum&& n) : m_mpq(std::move(n).m_mpz) {} + + template < typename N, + class = std::enable_if_t< std::is_integral< N >::value > > + explicit QNum(N n) : m_mpq(internal::MpzTransformer< N >()(n)) {} + + explicit QNum(const mpq_class& n) : m_mpq(n) { + knight_assert_msg(this->m_mpq.get_den() != 0, "denominator is zero"); + this->m_mpq.canonicalize(); + } + + explicit QNum(mpq_class&& n) : m_mpq(std::move(n)) { + knight_assert_msg(this->m_mpq.get_den() != 0, "denominator is zero"); + this->m_mpq.canonicalize(); + } + + /// \brief Create a QNum from a numerator and a denominator + template < typename N, + typename D, + class = std::enable_if_t< std::is_integral< N >::value && + std::is_integral< D >::value > > + explicit QNum(N n, D d) + : m_mpq(internal::MpzTransformer< N >()(n), + internal::MpzTransformer< D >()(d)) { + knight_assert_msg(this->m_mpq.get_den() != 0, "denominator is zero"); + this->m_mpq.canonicalize(); + } + + /// \brief Create a QNum from a numerator and a denominator + explicit QNum(const ZNum& n, const ZNum& d) : m_mpq(n.m_mpz, d.m_mpz) { + knight_assert_msg(this->m_mpq.get_den() != 0, "denominator is zero"); + this->m_mpq.canonicalize(); + } + + /// \brief Create a QNum from a numerator and a denominator + explicit QNum(ZNum&& n, ZNum&& d) + : m_mpq(std::move(n).m_mpz, std::move(d).m_mpz) { + knight_assert_msg(this->m_mpq.get_den() != 0, "denominator is zero"); + this->m_mpq.canonicalize(); + } + + /// \brief Create a QNum from a normalized mpq_class + struct NormalizedTag {}; + QNum(const mpq_class& n, NormalizedTag) : m_mpq(n) {} // NOLINT + QNum(mpq_class&& n, NormalizedTag) : m_mpq(std::move(n)) {} // NOLINT + + QNum(const QNum&) = default; + QNum(QNum&&) = default; + QNum& operator=(const QNum&) = default; + QNum& operator=(QNum&&) noexcept = default; + ~QNum() = default; + + QNum& operator=(const ZNum& n) { + this->m_mpq = n.m_mpz; + return *this; + } + + QNum& operator=(ZNum&& n) noexcept { + this->m_mpq = std::move(n.m_mpz); + return *this; + } + + template < typename N, + typename = std::enable_if_t< std::is_integral< N >::value > > + QNum& operator=(N n) { + this->m_mpq = internal::MpzTransformer< N >()(n); + return *this; + } + + /// NOLINTNEXTLINE + void Profile(llvm::FoldingSetNodeID& ID) const { + const mpz_class& num = this->m_mpq.get_num(); + const mpz_class& den = this->m_mpq.get_den(); + + // Add the size of the numerator mpz_t + ID.AddInteger(num.get_mpz_t()[0]._mp_size); + // Add each limb of the numerator mpz_t + for (int i = 0, e = std::abs(num.get_mpz_t()[0]._mp_size); i < e; ++i) { + ID.AddInteger(num.get_mpz_t()[0]._mp_d[i]); // NOLINT + } + + // Add the size of the denominator mpz_t + ID.AddInteger(den.get_mpz_t()[0]._mp_size); + // Add each limb of the denominator mpz_t + for (int i = 0, e = std::abs(den.get_mpz_t()[0]._mp_size); i < e; ++i) { + ID.AddInteger(den.get_mpz_t()[0]._mp_d[i]); // NOLINT + } + } + + QNum& operator+=(const QNum& x) { + this->m_mpq += x.m_mpq; + return *this; + } + + template < typename N, + class = std::enable_if_t< ZNumOrIntegral< N >::value > > + QNum& operator+=(N x) { + this->m_mpq += internal::ZNumTransformer< N >()(x); + return *this; + } + + QNum& operator-=(const QNum& x) { + this->m_mpq -= x.m_mpq; + return *this; + } + + template < typename N, + class = std::enable_if_t< ZNumOrIntegral< N >::value > > + QNum& operator-=(N x) { + this->m_mpq -= internal::ZNumTransformer< N >()(x); + return *this; + } + + QNum& operator*=(const QNum& x) { + this->m_mpq *= x.m_mpq; + return *this; + } + + template < typename N, + class = std::enable_if_t< ZNumOrIntegral< N >::value > > + QNum& operator*=(N x) { + this->m_mpq *= internal::ZNumTransformer< N >()(x); + return *this; + } + + QNum& operator/=(const QNum& x) { + knight_assert_msg(x.m_mpq != 0, "divided by zero"); + this->m_mpq /= x.m_mpq; + return *this; + } + + template < typename N, + class = std::enable_if_t< ZNumOrIntegral< N >::value > > + QNum& operator/=(N x) { + knight_assert_msg(x != 0, "divided by zero"); + this->m_mpq /= internal::ZNumTransformer< N >()(x); + return *this; + } + + /// \brief Unary plus + const QNum& operator+() const { return *this; } + + /// \brief Prefix increment + QNum& operator++() { + ++this->m_mpq; + return *this; + } + + /// \brief Postfix increment + const QNum operator++(int) { // NOLINT + QNum r(*this); + ++this->m_mpq; + return r; + } + + /// \brief Unary minus + const QNum operator-() const { return QNum(-this->m_mpq); } // NOLINT + + /// \brief Prefix decrement + QNum& operator--() { + --this->m_mpq; + return *this; + } + + /// \brief Postfix decrement + const QNum operator--(int) { // NOLINT + QNum r(*this); + --this->m_mpq; + return r; + } + + [[nodiscard]] ZNum numerator() const { return ZNum(this->m_mpq.get_num()); } + [[nodiscard]] ZNum denominator() const { + return ZNum(this->m_mpq.get_den()); + } + + [[nodiscard]] ZNum round_to_upper() const { + const mpz_class& num = this->m_mpq.get_num(); + const mpz_class& den = this->m_mpq.get_den(); + ZNum q(num / den); + ZNum r(num % den); + return (r == 0 || this->m_mpq < 0) ? q : q + 1; + } + + [[nodiscard]] ZNum round_to_lower() const { + const mpz_class& num = this->m_mpq.get_num(); + const mpz_class& den = this->m_mpq.get_den(); + ZNum q(num / den); + ZNum r(num % den); + return (r == 0 || this->m_mpq > 0) ? q : q - 1; + } + + [[nodiscard]] std::string str(int base = internal::K10Base) const { + return this->m_mpq.get_str(base); + } + +}; // end class QNum + +[[nodiscard]] inline QNum operator+(const QNum& lhs, const QNum& rhs) { + return QNum(lhs.get_mpq() + rhs.get_mpq(), QNum::NormalizedTag{}); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline QNum operator+(const QNum& lhs, T rhs) { + return QNum(lhs.get_mpq() + internal::ZNumTransformer< T >()(rhs), + QNum::NormalizedTag{}); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline QNum operator+(T lhs, const QNum& rhs) { + return QNum(internal::ZNumTransformer< T >()(lhs) + rhs.get_mpq(), + QNum::NormalizedTag{}); +} + +[[nodiscard]] inline QNum operator-(const QNum& lhs, const QNum& rhs) { + return QNum(lhs.get_mpq() - rhs.get_mpq(), QNum::NormalizedTag{}); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline QNum operator-(const QNum& lhs, T rhs) { + return QNum(lhs.get_mpq() - internal::ZNumTransformer< T >()(rhs), + QNum::NormalizedTag{}); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline QNum operator-(T lhs, const QNum& rhs) { + return QNum(internal::ZNumTransformer< T >()(lhs) - rhs.get_mpq(), + QNum::NormalizedTag{}); +} + +[[nodiscard]] inline QNum operator*(const QNum& lhs, const QNum& rhs) { + return QNum(lhs.get_mpq() * rhs.get_mpq(), QNum::NormalizedTag{}); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline QNum operator*(const QNum& lhs, T rhs) { + return QNum(lhs.get_mpq() * internal::ZNumTransformer< T >()(rhs), + QNum::NormalizedTag{}); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline QNum operator*(T lhs, const QNum& rhs) { + return QNum(internal::ZNumTransformer< T >()(lhs) * rhs.get_mpq(), + QNum::NormalizedTag{}); +} + +[[nodiscard]] inline QNum operator/(const QNum& lhs, const QNum& rhs) { + knight_assert_msg(rhs.get_mpq() != 0, "divided by zero"); + return QNum(lhs.get_mpq() / rhs.get_mpq(), QNum::NormalizedTag{}); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline QNum operator/(const QNum& lhs, T rhs) { + knight_assert_msg(rhs != 0, "divided by zero"); + return QNum(lhs.get_mpq() / internal::ZNumTransformer< T >()(rhs), + QNum::NormalizedTag{}); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline QNum operator/(T lhs, const QNum& rhs) { + knight_assert_msg(rhs.get_mpq() != 0, "divided by zero"); + return QNum(internal::ZNumTransformer< T >()(lhs) / rhs.get_mpq(), + QNum::NormalizedTag{}); +} + +inline QNum operator%(const QNum& lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator%(const QNum& lhs, T rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator%(T lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +inline QNum operator&(const QNum& lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator&(const QNum& lhs, T rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator&(T lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +inline QNum operator|(const QNum& lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator|(const QNum& lhs, T rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator|(T lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +inline QNum operator^(const QNum& lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator^(const QNum& lhs, T rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator^(T lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +inline QNum operator<<(const QNum& lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator<<(const QNum& lhs, T rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator<<(T lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +inline QNum operator>>(const QNum& lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator>>(const QNum& lhs, T rhs) { + knight_unreachable("unimplemented"); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +inline QNum operator>>(T lhs, const QNum& rhs) { + knight_unreachable("unimplemented"); +} + +[[nodiscard]] inline bool operator==(const QNum& lhs, const QNum& rhs) { + return lhs.get_mpq() == rhs.get_mpq(); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator==(const QNum& lhs, T rhs) { + return lhs.get_mpq() == internal::ZNumTransformer< T >()(rhs); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator==(T lhs, const QNum& rhs) { + return internal::ZNumTransformer< T >()(lhs) == rhs.get_mpq(); +} + +[[nodiscard]] inline bool operator!=(const QNum& lhs, const QNum& rhs) { + return lhs.get_mpq() != rhs.get_mpq(); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator!=(const QNum& lhs, T rhs) { + return lhs.get_mpq() != internal::ZNumTransformer< T >()(rhs); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator!=(T lhs, const QNum& rhs) { + return internal::ZNumTransformer< T >()(lhs) != rhs.get_mpq(); +} + +[[nodiscard]] inline bool operator<(const QNum& lhs, const QNum& rhs) { + return lhs.get_mpq() < rhs.get_mpq(); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator<(const QNum& lhs, T rhs) { + return lhs.get_mpq() < internal::ZNumTransformer< T >()(rhs); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator<(T lhs, const QNum& rhs) { + return internal::ZNumTransformer< T >()(lhs) < rhs.get_mpq(); +} + +[[nodiscard]] inline bool operator<=(const QNum& lhs, const QNum& rhs) { + return lhs.get_mpq() <= rhs.get_mpq(); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator<=(const QNum& lhs, T rhs) { + return lhs.get_mpq() <= internal::ZNumTransformer< T >()(rhs); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator<=(T lhs, const QNum& rhs) { + return internal::ZNumTransformer< T >()(lhs) <= rhs.get_mpq(); +} + +[[nodiscard]] inline bool operator>(const QNum& lhs, const QNum& rhs) { + return lhs.get_mpq() > rhs.get_mpq(); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator>(const QNum& lhs, T rhs) { + return lhs.get_mpq() > internal::ZNumTransformer< T >()(rhs); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator>(T lhs, const QNum& rhs) { + return internal::ZNumTransformer< T >()(lhs) > rhs.get_mpq(); +} + +[[nodiscard]] inline bool operator>=(const QNum& lhs, const QNum& rhs) { + return lhs.get_mpq() >= rhs.get_mpq(); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator>=(const QNum& lhs, T rhs) { + return lhs.get_mpq() >= internal::ZNumTransformer< T >()(rhs); +} + +template < typename T, class = std::enable_if_t< ZNumOrIntegral< T >::value > > +[[nodiscard]] inline bool operator>=(T lhs, const QNum& rhs) { + return internal::ZNumTransformer< T >()(lhs) >= rhs.get_mpq(); +} + +[[nodiscard]] inline const QNum& min(const QNum& a, const QNum& b) { + return (a < b) ? a : b; +} + +[[nodiscard]] inline const QNum& min(const QNum& a, + const QNum& b, + const QNum& c) { + return min(min(a, b), c); +} + +[[nodiscard]] inline const QNum& min(const QNum& a, + const QNum& b, + const QNum& c, + const QNum& d) { + return min(min(min(a, b), c), d); +} + +[[nodiscard]] inline const QNum& max(const QNum& a, const QNum& b) { + return (a < b) ? b : a; +} + +[[nodiscard]] inline const QNum& max(const QNum& a, + const QNum& b, + const QNum& c) { + return max(max(a, b), c); +} + +[[nodiscard]] inline const QNum& max(const QNum& a, + const QNum& b, + const QNum& c, + const QNum& d) { + return max(max(max(a, b), c), d); +} + +[[nodiscard]] inline QNum abs(const QNum& n) { + return QNum(abs(n.get_mpq())); +} + +inline llvm::raw_ostream& operator<<(llvm::raw_ostream& os, const QNum& n) { + return os << n.get_mpq().get_str(); +} + +[[nodiscard]] inline std::size_t hash_value(const QNum& n) { + const mpq_class& m = n.get_mpq(); + std::size_t result = 0; + + // Hash the numerator + hash_combine(result, std::hash< int >()(m.get_num_mpz_t()[0]._mp_size)); + for (int i = 0, e = std::abs(m.get_num_mpz_t()[0]._mp_size); i < e; ++i) { + hash_combine(result, + std::hash< mp_limb_t >()( + m.get_num_mpz_t()[0]._mp_d[i])); // NOLINT + } + + // Hash the denominator + hash_combine(result, std::hash< int >()(m.get_den_mpz_t()[0]._mp_size)); + for (int i = 0, e = std::abs(m.get_den_mpz_t()[0]._mp_size); i < e; ++i) { + hash_combine(result, + std::hash< mp_limb_t >()( + m.get_den_mpz_t()[0]._mp_d[i])); // NOLINT + } + + return result; +} + +} // end namespace knight::dfa + +namespace std { + +template <> +struct hash< knight::dfa::QNum > { + std::size_t operator()(const knight::dfa::QNum& n) const { + return knight::dfa::hash_value(n); + } +}; + +} // end namespace std diff --git a/include/dfa/domain/numerical/numerical_base.hpp b/include/dfa/domain/numerical/numerical_base.hpp index bb245c3..fb9fa9c 100644 --- a/include/dfa/domain/numerical/numerical_base.hpp +++ b/include/dfa/domain/numerical/numerical_base.hpp @@ -183,7 +183,7 @@ class NumericalDom : public NumericalDomBase< Num > { using Var = Variable< Num >; public: - NumericalDom< Derived, Num >() : NumericalDomBase(Derived::get_kind()) {} + NumericalDom() : NumericalDomBase(Derived::get_kind()) {} void join_with(const AbsDomBase& other) override { static_assert(does_derived_dom_can_join_with< Derived >::value, diff --git a/include/util/log.hpp b/include/util/log.hpp index b408287..011edc1 100644 --- a/include/util/log.hpp +++ b/include/util/log.hpp @@ -35,7 +35,8 @@ inline void print_source_location( #define log_with_type(TYPE, PRINT_SRC, NEW_LINE, X) \ do { \ - if (::llvm::DebugFlag && ::llvm::isCurrentDebugType(TYPE)) { \ + using namespace llvm; \ + if (::llvm::DebugFlag && isCurrentDebugType(TYPE)) { \ if (PRINT_SRC) { \ knight::print_source_location(TYPE, __func__, NEW_LINE); \ } \ diff --git a/src/dfa/proc_cfg.cpp b/src/dfa/proc_cfg.cpp index 2988138..f2276a7 100644 --- a/src/dfa/proc_cfg.cpp +++ b/src/dfa/proc_cfg.cpp @@ -59,7 +59,7 @@ void construct_mapping_for_term_condition( } if (const auto* term_cond_stmt = block->getTerminatorCondition()) { // does nothing if the key already exists in the map. - stmtToBlock.insert({term_cond_stmt, block}); + stmtToBlock[term_cond_stmt] = block; } } @@ -69,7 +69,7 @@ void construct_mapping_for_term_stmt(ProcCFG::NodeRef block, return; } if (const auto* term_stmt = block->getTerminatorStmt()) { - stmtToBlock.insert({term_stmt, block}); + stmtToBlock[term_stmt] = block; } } diff --git a/src/dfa/program_state.cpp b/src/dfa/program_state.cpp index f68d925..d30b90d 100644 --- a/src/dfa/program_state.cpp +++ b/src/dfa/program_state.cpp @@ -264,14 +264,14 @@ ProgramStateRef ProgramState::set_to_top() const { const auto& [stmt, sexpr] = pair; \ auto it = other->m_stmt_sexpr.find(stmt); \ if (it == other->m_stmt_sexpr.end() || it->second == sexpr) { \ - stmt_sexpr.insert_or_assign(stmt, sexpr); \ + stmt_sexpr.insert[stmt] = sexpr; \ } \ }); \ \ llvm::for_each(other->m_stmt_sexpr, [&](const auto& pair) { \ const auto& [stmt, sexpr] = pair; \ if (!stmt_sexpr.contains(stmt)) { \ - stmt_sexpr.insert_or_assign(stmt, sexpr); \ + stmt_sexpr.insert[stmt] = sexpr; \ } \ }); \ \ @@ -384,14 +384,14 @@ ProgramStateRef ProgramState::join(const ProgramStateRef& other, const auto& [stmt, sexpr] = pair; auto it = other->m_stmt_sexpr.find(stmt); if (it == other->m_stmt_sexpr.end() || it->second == sexpr) { - stmt_sexpr.insert_or_assign(stmt, sexpr); + stmt_sexpr.insert[stmt] = sexpr; } }); llvm::for_each(other->m_stmt_sexpr, [&](const auto& pair) { const auto& [stmt, sexpr] = pair; if (!stmt_sexpr.contains(stmt)) { - stmt_sexpr.insert_or_assign(stmt, sexpr); + stmt_sexpr.insert[stmt] = sexpr; } }); @@ -530,14 +530,14 @@ ProgramStateRef ProgramState::widen_with_threshold( const auto& [stmt, sexpr] = pair; auto it = other->m_stmt_sexpr.find(stmt); if (it == other->m_stmt_sexpr.end() || it->second == sexpr) { - stmt_sexpr.insert_or_assign(stmt, sexpr); + stmt_sexpr.insert[stmt] = sexpr; } }); llvm::for_each(other->m_stmt_sexpr, [&](const auto& pair) { const auto& [stmt, sexpr] = pair; if (!stmt_sexpr.contains(stmt)) { - stmt_sexpr.insert_or_assign(stmt, sexpr); + stmt_sexpr.insert[stmt] = sexpr; } }); diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index 48501a8..2dd1311 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -1,4 +1,5 @@ set(INCLUDE_DIR_LIST_STR "") + foreach(dir ${LLVM_LIBRARY_DIRS}) set(INCLUDE_DIR_LIST_STR "${INCLUDE_DIR_LIST_STR} -I${dir}/clang/${CLANG_VERSION_MAJOR}/include") endforeach() @@ -8,6 +9,6 @@ add_definitions(-DINCLUDE_DIRS="${INCLUDE_DIR_LIST_STR}") add_executable(knight main.cpp) set_target_properties(knight PROPERTIES RUNTIME_OUTPUT_DIRECTORY - "${CMAKE_BINARY_DIR}/bin") + "${CMAKE_BINARY_DIR}/bin") target_link_libraries(knight PRIVATE knight-lib) \ No newline at end of file