From 4c17827e2d006fde5e289cb031df30d5d240c779 Mon Sep 17 00:00:00 2001 From: Elazar Gershuni Date: Thu, 26 Sep 2024 19:36:04 +0300 Subject: [PATCH] rename bound_t to extended_number everywhere except in interval files Signed-off-by: Elazar Gershuni --- src/crab/array_domain.cpp | 2 +- src/crab/ebpf_domain.cpp | 4 ++-- src/crab/ebpf_domain.hpp | 2 +- src/crab/interval.hpp | 2 ++ src/crab/split_dbm.cpp | 8 ++++---- src/crab/thresholds.cpp | 8 ++++---- src/crab/thresholds.hpp | 8 ++++---- src/crab_utils/num_extended.hpp | 2 -- src/crab_verifier.cpp | 2 +- 9 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/crab/array_domain.cpp b/src/crab/array_domain.cpp index d404223c5..e4768b5e3 100644 --- a/src/crab/array_domain.cpp +++ b/src/crab/array_domain.cpp @@ -20,7 +20,7 @@ namespace crab::domains { -static bool maybe_between(const NumAbsDomain& dom, const bound_t& x, const linear_expression_t& symb_lb, +static bool maybe_between(const NumAbsDomain& dom, const extended_number& x, const linear_expression_t& symb_lb, const linear_expression_t& symb_ub) { using namespace dsl_syntax; assert(x.is_finite()); diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp index 9485f9ba7..ff613cefc 100644 --- a/src/crab/ebpf_domain.cpp +++ b/src/crab/ebpf_domain.cpp @@ -3182,8 +3182,8 @@ void ebpf_domain_t::initialize_loop_counter(const label_t& label) { m_inv.assign(variable_t::loop_counter(to_string(label)), 0); } -bound_t ebpf_domain_t::get_loop_count_upper_bound() const { - bound_t ub{0}; +extended_number ebpf_domain_t::get_loop_count_upper_bound() const { + extended_number ub{0}; for (const variable_t counter : variable_t::get_loop_counters()) { ub = std::max(ub, m_inv[counter].ub()); } diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp index 9a203b9ba..b97d7bb25 100644 --- a/src/crab/ebpf_domain.hpp +++ b/src/crab/ebpf_domain.hpp @@ -49,7 +49,7 @@ class ebpf_domain_t final { typedef bool check_require_func_t(NumAbsDomain&, const linear_constraint_t&, std::string); void set_require_check(std::function f); - bound_t get_loop_count_upper_bound() const; + extended_number get_loop_count_upper_bound() const; static ebpf_domain_t setup_entry(bool init_r1); static ebpf_domain_t from_constraints(const std::set& constraints, bool setup_constraints); diff --git a/src/crab/interval.hpp b/src/crab/interval.hpp index 60328d6fb..1a98ccc99 100644 --- a/src/crab/interval.hpp +++ b/src/crab/interval.hpp @@ -17,6 +17,8 @@ namespace crab { +using bound_t = extended_number; + class interval_t final { bound_t _lb; bound_t _ub; diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp index ca9648872..eefaf0f61 100644 --- a/src/crab/split_dbm.cpp +++ b/src/crab/split_dbm.cpp @@ -1096,8 +1096,8 @@ string_invariant SplitDBM::to_set() const { continue; } interval_t v_out = - interval_t(this->g.elem(v, 0) ? -number_t(this->g.edge_val(v, 0)) : bound_t::minus_infinity(), - this->g.elem(0, v) ? number_t(this->g.edge_val(0, v)) : bound_t::plus_infinity()); + interval_t(this->g.elem(v, 0) ? -number_t(this->g.edge_val(v, 0)) : extended_number::minus_infinity(), + this->g.elem(0, v) ? number_t(this->g.edge_val(0, v)) : extended_number::plus_infinity()); assert(!v_out.is_bottom()); variable_t variable = *(this->rev_map[v]); @@ -1279,8 +1279,8 @@ static interval_t get_interval(const SplitDBM::vert_map_t& m, const SplitDBM::gr return interval_t::top(); } SplitDBM::vert_id v = it->second; - bound_t lb = bound_t::minus_infinity(); - bound_t ub = bound_t::plus_infinity(); + extended_number lb = extended_number::minus_infinity(); + extended_number ub = extended_number::plus_infinity(); if (r.elem(v, 0)) { lb = x.is_unsigned() ? (-number_t(r.edge_val(v, 0))).truncate_to_uint(finite_width) : (-number_t(r.edge_val(v, 0))).truncate_to_sint(finite_width); diff --git a/src/crab/thresholds.cpp b/src/crab/thresholds.cpp index 3fe432794..b460b736e 100644 --- a/src/crab/thresholds.cpp +++ b/src/crab/thresholds.cpp @@ -7,9 +7,9 @@ namespace crab { inline namespace iterators { -void thresholds_t::add(bound_t v1) { +void thresholds_t::add(extended_number v1) { if (m_thresholds.size() < m_size) { - bound_t v = (v1); + extended_number v = (v1); if (std::find(m_thresholds.begin(), m_thresholds.end(), v) == m_thresholds.end()) { auto ub = std::upper_bound(m_thresholds.begin(), m_thresholds.end(), v); @@ -37,9 +37,9 @@ void thresholds_t::add(bound_t v1) { std::ostream& operator<<(std::ostream& o, const thresholds_t& t) { o << "{"; - for (typename std::vector::const_iterator it = t.m_thresholds.begin(), et = t.m_thresholds.end(); + for (typename std::vector::const_iterator it = t.m_thresholds.begin(), et = t.m_thresholds.end(); it != et;) { - bound_t b(*it); + extended_number b(*it); o << b; ++it; if (it != t.m_thresholds.end()) { diff --git a/src/crab/thresholds.hpp b/src/crab/thresholds.hpp index 9d880218c..d1e69de27 100644 --- a/src/crab/thresholds.hpp +++ b/src/crab/thresholds.hpp @@ -24,14 +24,14 @@ inline namespace iterators { class thresholds_t final { private: - std::vector m_thresholds; + std::vector m_thresholds; size_t m_size; public: explicit thresholds_t(size_t size = UINT_MAX) : m_size(size) { - m_thresholds.push_back(bound_t::minus_infinity()); + m_thresholds.push_back(extended_number::minus_infinity()); m_thresholds.emplace_back(number_t{0}); - m_thresholds.push_back(bound_t::plus_infinity()); + m_thresholds.push_back(extended_number::plus_infinity()); } [[nodiscard]] @@ -39,7 +39,7 @@ class thresholds_t final { return m_thresholds.size(); } - void add(bound_t v1); + void add(extended_number v1); friend std::ostream& operator<<(std::ostream& o, const thresholds_t& t); }; diff --git a/src/crab_utils/num_extended.hpp b/src/crab_utils/num_extended.hpp index f397e3578..f072b11e1 100644 --- a/src/crab_utils/num_extended.hpp +++ b/src/crab_utils/num_extended.hpp @@ -223,6 +223,4 @@ class extended_number final { }; // class extended_number -using bound_t = extended_number; - } // namespace crab diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp index a7f2c90d5..d7e720064 100644 --- a/src/crab_verifier.cpp +++ b/src/crab_verifier.cpp @@ -31,7 +31,7 @@ struct checks_db final { std::map> m_db{}; int total_warnings{}; int total_unreachable{}; - crab::bound_t max_loop_count{crab::number_t{0}}; + crab::extended_number max_loop_count{crab::number_t{0}}; void add(const label_t& label, const std::string& msg) { m_db[label].emplace_back(msg); }