Cleanup interval bound handling

src/crab/ebpf_domain.hpp

@@ -176,7 +176,7 @@ class ebpf_domain_t final {
     void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const;
     void check_access_context(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const;
     void check_access_packet(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
-                             std::optional<variable_t> shared_region_size) const;
+                             std::optional<variable_t> packet_size) const;
     void check_access_shared(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
                              variable_t shared_region_size) const;
 
@@ -249,7 +249,7 @@ class ebpf_domain_t final {
         NumAbsDomain join_by_if_else(const NumAbsDomain& inv, const linear_constraint_t& condition,
                                      const std::function<void(NumAbsDomain&)>& if_true,
                                      const std::function<void(NumAbsDomain&)>& if_false) const;
-        void selectively_join_based_on_type(NumAbsDomain& dst, NumAbsDomain& src) const;
+        void selectively_join_based_on_type(NumAbsDomain& dst, NumAbsDomain&& src) const;
         void add_extra_invariant(const NumAbsDomain& dst, std::map<variable_t, interval_t>& extra_invariants,
                                  variable_t type_variable, type_encoding_t type, data_kind_t kind,
                                  const NumAbsDomain& other) const;

src/crab/interval.hpp

@@ -54,6 +54,13 @@ class interval_t final {
         }
     }
 
+    template <is_enum T>
+    interval_t(T lb, T ub) : _lb(bound_t{lb}), _ub(bound_t{ub}) {
+        if (lb > ub) {
+            _lb = bound_t{number_t{0}};
+            _ub = bound_t{-1};
+        }
+    }
     explicit interval_t(const bound_t& b)
         : _lb(b.is_infinite() ? bound_t{number_t{0}} : b), _ub(b.is_infinite() ? bound_t{-1} : b) {}
 
@@ -74,6 +81,25 @@ class interval_t final {
         return _ub;
     }
 
+    [[nodiscard]]
+    std::tuple<bound_t, bound_t> pair() const {
+        return {_lb, _ub};
+    }
+
+    template <std::integral T>
+    [[nodiscard]]
+    std::tuple<T, T> bound(T lb, T ub) const {
+        interval_t b = interval_t(lb, ub) & *this;
+        return {static_cast<T>(*b._lb.number()), static_cast<T>(*b._ub.number())};
+    }
+
+    template <is_enum T>
+    [[nodiscard]]
+    std::tuple<T, T> bound(T elb, T eub) const {
+        auto [lb, ub] = bound(static_cast<std::underlying_type_t<T>>(elb), static_cast<std::underlying_type_t<T>>(eub));
+        return {static_cast<T>(lb), static_cast<T>(ub)};
+    }
+
     [[nodiscard]]
     bool is_bottom() const {
         return (_lb > _ub);
@@ -428,19 +454,6 @@ inline interval_t operator-(const interval_t& x, const number_t& c) { return x -
 
 } // namespace interval_operators
 
-inline interval_t trim_interval(const interval_t& i, const interval_t& j) {
-    if (std::optional<number_t> c = j.singleton()) {
-        if (i.lb() == bound_t{*c}) {
-            return interval_t(bound_t{*c + 1}, i.ub());
-        } else if (i.ub() == bound_t{*c}) {
-            return interval_t(i.lb(), bound_t{*c - 1});
-        } else if (i.is_top() && (*c == 0)) {
-            return {number_t{1}, number_t{std::numeric_limits<uint64_t>::max()}};
-        }
-    }
-    return i;
-}
-
 } // namespace crab
 
 std::string to_string(const crab::interval_t& interval) noexcept;

src/crab/split_dbm.cpp

@@ -282,9 +282,22 @@ bool SplitDBM::add_linear_leq(const linear_expression_t& exp) {
     return true;
 }
 
+static interval_t trim_interval(const interval_t& i, const number_t& n) {
+    if (i.lb() == n) {
+        return interval_t{n + 1, i.ub()};
+    }
+    if (i.ub() == n) {
+        return interval_t{i.lb(), n - 1};
+    }
+    if (i.is_top() && n == 0) {
+        return interval_t{1, std::numeric_limits<uint64_t>::max()};
+    }
+    return i;
+}
+
 bool SplitDBM::add_univar_disequation(variable_t x, const number_t& n) {
     interval_t i = get_interval(x, 0);
-    interval_t new_i = trim_interval(i, interval_t(n));
+    interval_t new_i = trim_interval(i, n);
     if (new_i.is_bottom()) {
         return false;
     }

src/crab_utils/debug.hpp

@@ -52,6 +52,11 @@ inline void ___print___(std::ostream& os, ArgTypes... args) {
         throw std::runtime_error(os.str()); \
     } while (0)
 
+#define RAISE_INVALID_WIDTH(width)                                          \
+    do {                                                                    \
+        throw std::runtime_error("Invalid width " + std::to_string(width)); \
+    } while (0)
+
 extern bool CrabWarningFlag;
 void CrabEnableWarningMsg(bool b);
 

src/crab_utils/num_big.hpp

@@ -27,7 +27,7 @@ class number_t final {
     number_t() = default;
     number_t(cpp_int n) : _n(std::move(n)) {}
     number_t(std::integral auto n) : _n{n} {}
-    number_t(is_enum auto n) : _n{static_cast<int64_t>(n)} {}
+    number_t(is_enum auto n) : _n{static_cast<std::underlying_type_t<decltype(n)>>(n)} {}
     explicit number_t(const std::string& s) { _n = cpp_int(s); }
 
     template <std::integral T>
@@ -38,6 +38,11 @@ class number_t final {
         return static_cast<T>(_n);
     }
 
+    template <is_enum T>
+    T cast_to() const {
+        return static_cast<T>(static_cast<std::underlying_type_t<T>>(_n));
+    }
+
     explicit operator cpp_int() const { return _n; }
 
     [[nodiscard]]

src/string_constraints.hpp

@@ -24,13 +24,15 @@ enum type_encoding_t {
     T_STACK = -1,
     T_SHARED = 0
 };
+constexpr type_encoding_t T_MIN = T_MAP_PROGRAMS;
+constexpr type_encoding_t T_MAX = T_SHARED;
 
 struct string_invariant {
     std::optional<std::set<std::string>> maybe_inv{};
 
     string_invariant() = default;
 
-    explicit string_invariant(std::set<std::string> inv) : maybe_inv(std::move(inv)) {};
+    explicit string_invariant(std::set<std::string> inv) : maybe_inv(std::move(inv)){};
 
     string_invariant(const string_invariant& inv) = default;
     string_invariant& operator=(const string_invariant& inv) = default;