Finite domain

src/crab/add_bottom.hpp

@@ -4,15 +4,12 @@
 
 #include <optional>
 
-#include "crab/split_dbm.hpp"
-#include "string_constraints.hpp"
+#include "crab/finite_domain.hpp"
 
-namespace crab {
-
-namespace domains {
+namespace crab::domains {
 
 class AddBottom final {
-    using T = SplitDBM;
+    using T = FiniteDomain;
     std::optional<T> dom{};
     AddBottom() {}
 
@@ -25,6 +22,12 @@ class AddBottom final {
     AddBottom& operator=(const AddBottom& o) = default;
     AddBottom& operator=(AddBottom&& o) = default;
 
+    explicit operator bool() const { return static_cast<bool>(dom); }
+
+    T* operator->() { return &dom.value(); }
+
+    const T* operator->() const { return &dom.value(); }
+
     void set_to_top() {
         if (dom) {
             dom->set_to_top();
@@ -109,7 +112,7 @@ class AddBottom final {
         if (!dom || !o.dom) {
             return bottom();
         }
-        if (auto res = (*dom).meet(*o.dom)) {
+        if (auto res = dom->meet(*o.dom)) {
             return AddBottom(*res);
         }
         return bottom();
@@ -135,35 +138,13 @@ class AddBottom final {
         return bottom();
     }
 
-    void operator-=(variable_t v) {
+    void havoc(variable_t v) {
         if (dom) {
-            (*dom) -= v;
+            dom->havoc(v);
         }
     }
 
-    void assign(std::optional<variable_t> x, const linear_expression_t& e) {
-        if (x) {
-            assign(*x, e);
-        }
-    }
-
-    template <typename V>
-    void assign(variable_t x, const V& value) {
-        if (dom) {
-            // XXX: maybe needs to return false when becomes bottom
-            // is this possible?
-            dom->assign(x, value);
-        }
-    };
-
-    template <typename Op, typename Left, typename Right>
-    void apply(Op op, variable_t x, const Left& left, const Right& right, int finite_width) {
-        if (dom) {
-            dom->apply(op, x, left, right, finite_width);
-        }
-    }
-
-    void operator+=(const linear_constraint_t& cst) {
+    void add_constraint(const linear_constraint_t& cst) {
         if (dom) {
             if (!dom->add_constraint(cst)) {
                 dom = {};
@@ -179,13 +160,6 @@ class AddBottom final {
         return interval_t::bottom();
     }
 
-    interval_t operator[](variable_t x) const {
-        if (dom) {
-            return (*dom)[x];
-        }
-        return interval_t::bottom();
-    }
-
     void set(variable_t x, const interval_t& intv) {
         if (intv.is_bottom()) {
             dom = {};
@@ -194,6 +168,28 @@ class AddBottom final {
         }
     }
 
+    void assign(const std::optional<variable_t> x, const linear_expression_t& e) {
+        if (x) {
+            assign(*x, e);
+        }
+    }
+
+    template <typename V>
+    void assign(variable_t x, const V& value) {
+        if (dom) {
+            // XXX: maybe needs to return false when becomes bottom
+            // is this possible?
+            dom->assign(x, value);
+        }
+    }
+
+    template <typename Op, typename Left, typename Right>
+    void apply(Op op, variable_t x, const Left& left, const Right& right, int finite_width) {
+        if (dom) {
+            dom->apply(op, x, left, right, finite_width);
+        }
+    }
+
     // Return true if inv intersects with cst.
     [[nodiscard]]
     bool intersect(const linear_constraint_t& cst) const {
@@ -228,5 +224,4 @@ class AddBottom final {
     }
 }; // class AddBottom
 
-} // namespace domains
-} // namespace crab
+} // namespace crab::domains

src/crab/array_domain.cpp

@@ -28,8 +28,8 @@ static bool maybe_between(const NumAbsDomain& dom, const extended_number& x, con
     assert(x.is_finite());
     const linear_expression_t num(*x.number());
     NumAbsDomain tmp(dom);
-    tmp += num >= symb_lb;
-    tmp += num <= symb_ub;
+    tmp.add_constraint(num >= symb_lb);
+    tmp.add_constraint(num <= symb_ub);
     return !tmp.is_bottom();
 }
 
@@ -542,13 +542,13 @@ static std::optional<std::pair<offset_t, unsigned>> kill_and_find_var(NumAbsDoma
     if (!cells.empty()) {
         // Forget the scalars from the numerical domain
         for (const auto& c : cells) {
-            inv -= c.get_scalar(kind);
+            inv.havoc(c.get_scalar(kind));
 
             // Forget signed and unsigned values together.
             if (kind == data_kind_t::svalues) {
-                inv -= c.get_scalar(data_kind_t::uvalues);
+                inv.havoc(c.get_scalar(data_kind_t::uvalues));
             } else if (kind == data_kind_t::uvalues) {
-                inv -= c.get_scalar(data_kind_t::svalues);
+                inv.havoc(c.get_scalar(data_kind_t::svalues));
             }
         }
         // Remove the cells. If needed again they will be re-created.
@@ -811,13 +811,13 @@ void array_domain_t::store_numbers(const NumAbsDomain& inv, const variable_t _id
         return;
     }
 
-    const std::optional<number_t> idx_n = inv[_idx].singleton();
+    const std::optional<number_t> idx_n = inv.eval_interval(_idx).singleton();
     if (!idx_n) {
         CRAB_WARN("array expansion store range ignored because ", "lower bound is not constant");
         return;
     }
 
-    const std::optional<number_t> width = inv[_width].singleton();
+    const std::optional<number_t> width = inv.eval_interval(_width).singleton();
     if (!width) {
         CRAB_WARN("array expansion store range ignored because ", "upper bound is not constant");
         return;

src/crab/ebpf_checker.cpp

@@ -12,7 +12,6 @@
 #include "config.hpp"
 #include "crab/array_domain.hpp"
 #include "crab/ebpf_domain.hpp"
-#include "crab_utils/num_safety.hpp"
 #include "dsl_syntax.hpp"
 #include "platform.hpp"
 #include "program.hpp"
@@ -98,7 +97,7 @@ void ebpf_domain_assume(ebpf_domain_t& dom, const Assertion& assertion) {
     ebpf_checker{dom, assertion,
                  [](NumAbsDomain& inv, const linear_constraint_t& cst, const std::string&) {
                      // avoid redundant errors
-                     inv += cst;
+                     inv.add_constraint(cst);
                  }}
         .visit(assertion);
 }
@@ -238,6 +237,9 @@ void ebpf_checker::operator()(const BoundedLoopCount& s) const {
 
 void ebpf_checker::operator()(const FuncConstraint& s) const {
     // Look up the helper function id.
+    if (!m_inv) {
+        return;
+    }
     const reg_pack_t& reg = reg_pack(s.reg);
     const auto src_interval = m_inv.eval_interval(reg.svalue);
     if (const auto sn = src_interval.singleton()) {
@@ -303,7 +305,7 @@ void ebpf_checker::operator()(const ValidMapKeyValue& s) const {
             variable_t lb = access_reg.stack_offset;
             linear_expression_t ub = lb + width;
             if (!stack.all_num(inv, lb, ub)) {
-                auto lb_is = inv[lb].lb().number();
+                auto lb_is = inv.eval_interval(lb).lb().number();
                 std::string lb_s = lb_is && lb_is->fits<int32_t>() ? std::to_string(lb_is->narrow<int32_t>()) : "-oo";
                 auto ub_is = inv.eval_interval(ub).ub().number();
                 std::string ub_s = ub_is && ub_is->fits<int32_t>() ? std::to_string(ub_is->narrow<int32_t>()) : "oo";
@@ -314,7 +316,7 @@ void ebpf_checker::operator()(const ValidMapKeyValue& s) const {
                 if (map_type.is_array) {
                     // Get offset value.
                     variable_t key_ptr = access_reg.stack_offset;
-                    std::optional<number_t> offset = inv[key_ptr].singleton();
+                    std::optional<number_t> offset = inv.eval_interval(key_ptr).singleton();
                     if (!offset.has_value()) {
                         require("Pointer must be a singleton");
                     } else if (s.key) {

src/crab/ebpf_domain.cpp

@@ -40,7 +40,7 @@ std::optional<variable_t> ebpf_domain_t::get_type_offset_variable(const Reg& reg
     return get_type_offset_variable(reg, m_inv);
 }
 
-string_invariant ebpf_domain_t::to_set() const { return this->m_inv.to_set() + this->stack.to_set(); }
+string_invariant ebpf_domain_t::to_set() const { return m_inv.to_set() + stack.to_set(); }
 
 ebpf_domain_t ebpf_domain_t::top() {
     ebpf_domain_t abs;
@@ -118,21 +118,21 @@ ebpf_domain_t ebpf_domain_t::calculate_constant_limits() {
     using namespace crab::dsl_syntax;
     for (const int i : {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}) {
         const auto r = reg_pack(i);
-        inv += r.svalue <= std::numeric_limits<int32_t>::max();
-        inv += r.svalue >= std::numeric_limits<int32_t>::min();
-        inv += r.uvalue <= std::numeric_limits<uint32_t>::max();
-        inv += r.uvalue >= 0;
-        inv += r.stack_offset <= EBPF_TOTAL_STACK_SIZE;
-        inv += r.stack_offset >= 0;
-        inv += r.shared_offset <= r.shared_region_size;
-        inv += r.shared_offset >= 0;
-        inv += r.packet_offset <= variable_t::packet_size();
-        inv += r.packet_offset >= 0;
+        inv.add_constraint(r.svalue <= std::numeric_limits<int32_t>::max());
+        inv.add_constraint(r.svalue >= std::numeric_limits<int32_t>::min());
+        inv.add_constraint(r.uvalue <= std::numeric_limits<uint32_t>::max());
+        inv.add_constraint(r.uvalue >= 0);
+        inv.add_constraint(r.stack_offset <= EBPF_TOTAL_STACK_SIZE);
+        inv.add_constraint(r.stack_offset >= 0);
+        inv.add_constraint(r.shared_offset <= r.shared_region_size);
+        inv.add_constraint(r.shared_offset >= 0);
+        inv.add_constraint(r.packet_offset <= variable_t::packet_size());
+        inv.add_constraint(r.packet_offset >= 0);
         if (thread_local_options.cfg_opts.check_for_termination) {
             for (const variable_t counter : variable_t::get_loop_counters()) {
-                inv += counter <= std::numeric_limits<int32_t>::max();
-                inv += counter >= 0;
-                inv += counter <= r.svalue;
+                inv.add_constraint(counter <= std::numeric_limits<int32_t>::max());
+                inv.add_constraint(counter >= 0);
+                inv.add_constraint(counter <= r.svalue);
             }
         }
     }
@@ -153,15 +153,15 @@ ebpf_domain_t ebpf_domain_t::narrow(const ebpf_domain_t& other) const {
     return ebpf_domain_t(m_inv.narrow(other.m_inv), stack & other.stack);
 }
 
-void ebpf_domain_t::operator+=(const linear_constraint_t& cst) { m_inv += cst; }
+void ebpf_domain_t::add_constraint(const linear_constraint_t& cst) { m_inv.add_constraint(cst); }
 
-void ebpf_domain_t::operator-=(const variable_t var) { m_inv -= var; }
+void ebpf_domain_t::havoc(const variable_t var) { m_inv.havoc(var); }
 
 // Get the start and end of the range of possible map fd values.
 // In the future, it would be cleaner to use a set rather than an interval
 // for map fds.
 bool ebpf_domain_t::get_map_fd_range(const Reg& map_fd_reg, int32_t* start_fd, int32_t* end_fd) const {
-    const interval_t& map_fd_interval = m_inv[reg_pack(map_fd_reg).map_fd];
+    const interval_t& map_fd_interval = m_inv.eval_interval(reg_pack(map_fd_reg).map_fd);
     const auto lb = map_fd_interval.lb().number();
     const auto ub = map_fd_interval.ub().number();
     if (!lb || !lb->fits<int32_t>() || !ub || !ub->fits<int32_t>()) {
@@ -276,12 +276,12 @@ interval_t ebpf_domain_t::get_map_max_entries(const Reg& map_fd_reg) const {
 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());
+        ub = std::max(ub, m_inv.eval_interval(counter).ub());
     }
     return ub;
 }
 
-interval_t ebpf_domain_t::get_r0() const { return m_inv[reg_pack(R0_RETURN_VALUE).svalue]; }
+interval_t ebpf_domain_t::get_r0() const { return m_inv.eval_interval(reg_pack(R0_RETURN_VALUE).svalue); }
 
 std::ostream& operator<<(std::ostream& o, const ebpf_domain_t& dom) {
     if (dom.is_bottom()) {
@@ -295,15 +295,15 @@ std::ostream& operator<<(std::ostream& o, const ebpf_domain_t& dom) {
 void ebpf_domain_t::initialize_packet() {
     using namespace crab::dsl_syntax;
     ebpf_domain_t& inv = *this;
-    inv -= variable_t::packet_size();
-    inv -= variable_t::meta_offset();
+    inv.havoc(variable_t::packet_size());
+    inv.havoc(variable_t::meta_offset());
 
-    inv += 0 <= variable_t::packet_size();
-    inv += variable_t::packet_size() < MAX_PACKET_SIZE;
+    inv.add_constraint(0 <= variable_t::packet_size());
+    inv.add_constraint(variable_t::packet_size() < MAX_PACKET_SIZE);
     const auto info = *thread_local_program_info;
     if (info.type.context_descriptor->meta >= 0) {
-        inv += variable_t::meta_offset() <= 0;
-        inv += variable_t::meta_offset() >= -4098;
+        inv.add_constraint(variable_t::meta_offset() <= 0);
+        inv.add_constraint(variable_t::meta_offset() >= -4098);
     } else {
         inv.m_inv.assign(variable_t::meta_offset(), 0);
     }
@@ -316,7 +316,7 @@ ebpf_domain_t ebpf_domain_t::from_constraints(const std::set<std::string>& const
     }
     auto numeric_ranges = std::vector<interval_t>();
     for (const auto& cst : parse_linear_constraints(constraints, numeric_ranges)) {
-        inv += cst;
+        inv.add_constraint(cst);
     }
     for (const interval_t& range : numeric_ranges) {
         const int start = range.lb().narrow<int>();
@@ -333,8 +333,8 @@ ebpf_domain_t ebpf_domain_t::setup_entry(const bool init_r1) {
     ebpf_domain_t inv;
     const auto r10 = reg_pack(R10_STACK_POINTER);
     constexpr Reg r10_reg{R10_STACK_POINTER};
-    inv.m_inv += EBPF_TOTAL_STACK_SIZE <= r10.svalue;
-    inv.m_inv += r10.svalue <= PTR_MAX;
+    inv.m_inv.add_constraint(EBPF_TOTAL_STACK_SIZE <= r10.svalue);
+    inv.m_inv.add_constraint(r10.svalue <= PTR_MAX);
     inv.m_inv.assign(r10.stack_offset, EBPF_TOTAL_STACK_SIZE);
     // stack_numeric_size would be 0, but TOP has the same result
     // so no need to assign it.
@@ -343,8 +343,8 @@ ebpf_domain_t ebpf_domain_t::setup_entry(const bool init_r1) {
     if (init_r1) {
         const auto r1 = reg_pack(R1_ARG);
         constexpr Reg r1_reg{R1_ARG};
-        inv.m_inv += 1 <= r1.svalue;
-        inv.m_inv += r1.svalue <= PTR_MAX;
+        inv.m_inv.add_constraint(1 <= r1.svalue);
+        inv.m_inv.add_constraint(r1.svalue <= PTR_MAX);
         inv.m_inv.assign(r1.ctx_offset, 0);
         inv.type_inv.assign_type(inv.m_inv, r1_reg, T_CTX);
     }

src/crab/ebpf_domain.hpp

@@ -3,8 +3,6 @@
 #pragma once
 
 // This file is eBPF-specific, not derived from CRAB.
-
-#include <functional>
 #include <optional>
 
 #include "crab/array_domain.hpp"
@@ -76,8 +74,8 @@ class ebpf_domain_t final {
 
   private:
     // private generic domain functions
-    void operator+=(const linear_constraint_t& cst);
-    void operator-=(variable_t var);
+    void add_constraint(const linear_constraint_t& cst);
+    void havoc(variable_t var);
 
     [[nodiscard]]
     std::optional<uint32_t> get_map_type(const Reg& map_fd_reg) const;