From c185ba7495aee8f4e25a853b2e6ffcca95f52cd6 Mon Sep 17 00:00:00 2001
From: Elazar Gershuni <elazarg@gmail.com>
Date: Thu, 27 Jun 2024 03:11:51 +0300
Subject: [PATCH 1/3] remove radix tree

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>
---
 .gitmodules               |   3 -
 external/radix_tree       |   1 -
 src/crab/array_domain.cpp | 437 +++++---------------------------------
 src/crab/array_domain.hpp | 300 ++++++++++++++++++++++++--
 src/crab/ebpf_domain.cpp  |   7 +-
 src/crab/ebpf_domain.hpp  |   1 +
 src/crab_verifier.cpp     |   3 -
 7 files changed, 339 insertions(+), 413 deletions(-)
 delete mode 160000 external/radix_tree

diff --git a/.gitmodules b/.gitmodules
index f12802369..25d6d4b43 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,9 +1,6 @@
 [submodule "ebpf-samples"]
 	path = ebpf-samples
 	url = https://github.com/vbpf/ebpf-samples.git
-[submodule "external/radix_tree"]
-	path = external/radix_tree
-	url = https://github.com/ytakano/radix_tree
 [submodule "external/bpf_conformance"]
 	path = external/bpf_conformance
 	url = https://github.com/Alan-Jowett/bpf_conformance.git
diff --git a/external/radix_tree b/external/radix_tree
deleted file mode 160000
index f8bc846ef..000000000
--- a/external/radix_tree
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit f8bc846ef1f00ee43af2ddc04af67d2e44d50685
diff --git a/src/crab/array_domain.cpp b/src/crab/array_domain.cpp
index 9a51ba668..992de72f2 100644
--- a/src/crab/array_domain.cpp
+++ b/src/crab/array_domain.cpp
@@ -4,13 +4,11 @@
 #include <algorithm>
 #include <optional>
 #include <set>
-#include <unordered_map>
 #include <utility>
 #include <vector>
 
 #include "boost/endian/conversion.hpp"
 
-#include "radix_tree/radix_tree.hpp"
 #include "crab/array_domain.hpp"
 
 #include "asm_ostream.hpp"
@@ -32,128 +30,6 @@ static bool maybe_between(const NumAbsDomain& dom, const bound_t& x,
     return !tmp.is_bottom();
 }
 
-class offset_t final {
-    index_t _index{};
-    int _prefix_length;
-
-  public:
-    static constexpr int bitsize = 8 * sizeof(index_t);
-    offset_t() : _prefix_length(bitsize) {}
-    offset_t(index_t index) : _index(index), _prefix_length(bitsize) {}
-    offset_t(index_t index, int prefix_length) : _index(index), _prefix_length(prefix_length) {}
-    explicit operator int() const { return static_cast<int>(_index); }
-    operator index_t() const { return _index; }
-    [[nodiscard]] int prefix_length() const { return _prefix_length; }
-
-    index_t operator[](int n) const { return (_index >> (bitsize - 1 - n)) & 1; }
-};
-
-// NOTE: required by radix_tree
-// Get the length of a key, which is the size usable with the [] operator.
-[[maybe_unused]]
-int radix_length(const offset_t& offset) {
-    return offset.prefix_length();
-}
-
-// NOTE: required by radix_tree
-// Get a range of bits out of the middle of a key, starting at [begin] for a given length.
-[[maybe_unused]]
-offset_t radix_substr(const offset_t& key, int begin, int length)
-{
-    uint64_t mask;
-
-    if (length == offset_t::bitsize)
-        mask = 0;
-    else
-        mask = ((index_t)1) << length;
-
-    mask -= 1;
-    mask <<= offset_t::bitsize - length - begin;
-
-    index_t value = (((index_t)key) & mask) << begin;
-    return offset_t{value, length};
-}
-
-// NOTE: required by radix_tree
-// Concatenate two bit patterns.
-[[maybe_unused]]
-offset_t radix_join(const offset_t& entry1, const offset_t& entry2)
-{
-    index_t value1 = (index_t)entry1;
-    index_t value2 = (index_t)entry2;
-    index_t value = value1 | (value2 >> entry1.prefix_length());
-    int prefix_length = entry1.prefix_length() + entry2.prefix_length();
-
-    return offset_t{value, prefix_length};
-}
-
-/***
-   Conceptually, a cell is tuple of an array, offset, size, and
-   scalar variable such that:
-
-_scalar = array[_offset, _offset + 1, ..., _offset + _size - 1]
-
-    For simplicity, we don't carry the array inside the cell class.
-    Only, offset_map objects can create cells. They will consider the
-            array when generating the scalar variable.
-*/
-class cell_t final {
-  private:
-    friend class offset_map_t;
-
-    offset_t _offset{};
-    unsigned _size{};
-
-    // Only offset_map_t can create cells
-    cell_t() = default;
-
-    cell_t(offset_t offset, unsigned size) : _offset(offset), _size(size) {}
-
-    static interval_t to_interval(const offset_t o, unsigned size) {
-        return {number_t{static_cast<int>(o)}, number_t{static_cast<int>(o)} + number_t{static_cast<int>(size - 1)}};
-    }
-
-  public:
-    [[nodiscard]] interval_t to_interval() const { return to_interval(_offset, _size); }
-
-    [[nodiscard]] bool is_null() const { return _offset == 0 && _size == 0; }
-
-    [[nodiscard]] offset_t get_offset() const { return _offset; }
-
-    [[nodiscard]] variable_t get_scalar(data_kind_t kind) const { return variable_t::cell_var(kind, number_t{_offset}, _size); }
-
-    // ignore the scalar variable
-    bool operator==(const cell_t& o) const { return to_interval() == o.to_interval(); }
-
-    // ignore the scalar variable
-    bool operator<(const cell_t& o) const {
-        if (_offset == o._offset)
-            return _size < o._size;
-        return _offset < o._offset;
-    }
-
-    // Return true if [o, o + size) definitely overlaps with the cell,
-    // where o is a constant expression.
-    [[nodiscard]]
-    bool overlap(const offset_t& o, unsigned size) const {
-        interval_t x = to_interval();
-        interval_t y = to_interval(o, size);
-        bool res = (!(x & y).is_bottom());
-        CRAB_LOG("array-expansion-overlap",
-                 std::cout << "**Checking if " << x << " overlaps with " << y << "=" << res << "\n";);
-        return res;
-    }
-
-    // Return true if [symb_lb, symb_ub] may overlap with the cell,
-    // where symb_lb and symb_ub are not constant expressions.
-    [[nodiscard]]
-    bool symbolic_overlap(const linear_expression_t& symb_lb,
-                     const linear_expression_t& symb_ub,
-                     const NumAbsDomain& dom) const;
-
-    friend std::ostream& operator<<(std::ostream& o, const cell_t& c) { return o << "cell(" << c.to_interval() << ")"; }
-};
-
 // Return true if [symb_lb, symb_ub] may overlap with the cell,
 // where symb_lb and symb_ub are not constant expressions.
 bool cell_t::symbolic_overlap(const linear_expression_t& symb_lb, const linear_expression_t& symb_ub,
@@ -163,83 +39,8 @@ bool cell_t::symbolic_overlap(const linear_expression_t& symb_lb, const linear_e
         || maybe_between(dom, x.ub(), symb_lb, symb_ub);
 }
 
-// Map offsets to cells
-class offset_map_t final {
-  private:
-    friend class array_domain_t;
-
-    using cell_set_t = std::set<cell_t>;
-
-    /*
-      The keys in the patricia tree are processing in big-endian
-      order. This means that the keys are sorted. Sortedness is
-      very important to efficiently perform operations such as
-      checking for overlap cells. Since keys are treated as bit
-      patterns, negative offsets can be used but they are treated
-      as large unsigned numbers.
-    */
-    using patricia_tree_t = radix_tree<offset_t, cell_set_t>;
-
-    patricia_tree_t _map;
-
-    // for algorithm::lower_bound and algorithm::upper_bound
-    struct compare_binding_t {
-        bool operator()(const typename patricia_tree_t::value_type& kv, const offset_t& o) const { return kv.first < o; }
-        bool operator()(const offset_t& o, const typename patricia_tree_t::value_type& kv) const { return o < kv.first; }
-        bool operator()(const typename patricia_tree_t::value_type& kv1,
-                        const typename patricia_tree_t::value_type& kv2) const {
-            return kv1.first < kv2.first;
-        }
-    };
-
-    void remove_cell(const cell_t& c);
-
-    void insert_cell(const cell_t& c);
-
-    [[nodiscard]] std::optional<cell_t> get_cell(offset_t o, unsigned size);
-
-    cell_t mk_cell(offset_t o, unsigned size);
-
-  public:
-    offset_map_t() = default;
-
-    [[nodiscard]] bool empty() const { return _map.empty(); }
-
-    [[nodiscard]] std::size_t size() const { return _map.size(); }
-
-    void operator-=(const cell_t& c) { remove_cell(c); }
-
-    void operator-=(const std::vector<cell_t>& cells) {
-        for (auto const& c : cells) {
-            this->operator-=(c);
-        }
-    }
-
-    // Return in out all cells that might overlap with (o, size).
-    std::vector<cell_t> get_overlap_cells(offset_t o, unsigned size);
-
-    [[nodiscard]] std::vector<cell_t> get_overlap_cells_symbolic_offset(const NumAbsDomain& dom,
-                                                                        const linear_expression_t& symb_lb,
-                                                                        const linear_expression_t& symb_ub);
-
-    friend std::ostream& operator<<(std::ostream& o, offset_map_t& m);
-
-    /* Operations needed if used as value in a separate_domain */
-    [[nodiscard]] bool is_top() const { return empty(); }
-    [[nodiscard]] bool is_bottom() const { return false; }
-    /*
-       We don't distinguish between bottom and top.
-       This is fine because separate_domain only calls bottom if
-       operator[] is called over a bottom state. Thus, we will make
-       sure that we don't call operator[] in that case.
-    */
-    static offset_map_t bottom() { return offset_map_t(); }
-    static offset_map_t top() { return offset_map_t(); }
-};
-
 void offset_map_t::remove_cell(const cell_t& c) {
-    offset_t key = c.get_offset();
-    _map[key].erase(c);
+    set.erase(c);
 }
 
 [[nodiscard]]
@@ -247,48 +48,24 @@ std::vector<cell_t> offset_map_t::get_overlap_cells_symbolic_offset(const NumAbs
                                                                     const linear_expression_t& symb_lb,
                                                                     const linear_expression_t& symb_ub) {
     std::vector<cell_t> out;
-    for (const auto& [_offset, o_cells] : _map) {
-        // All cells in o_cells have the same offset. They only differ in the size.
-        // If the largest cell overlaps with [offset, offset + size)
-        // then the rest of cells are considered to overlap.
-        // This is an over-approximation because [offset, offset+size) can overlap
-        // with the largest cell but it doesn't necessarily overlap with smaller cells.
-        // For efficiency, we assume it overlaps with all.
-        cell_t largest_cell;
-        for (const cell_t& c : o_cells) {
-            if (largest_cell.is_null()) {
-                largest_cell = c;
-            } else {
-                assert(c.get_offset() == largest_cell.get_offset());
-                if (largest_cell < c) {
-                    largest_cell = c;
-                }
-            }
-        }
-        if (!largest_cell.is_null()) {
-            if (largest_cell.symbolic_overlap(symb_lb, symb_ub, dom)) {
-                for (auto& c : o_cells) {
-                    out.push_back(c);
-                }
-            }
+    for (const auto& cell : set) {
+        if (cell.symbolic_overlap(symb_lb, symb_ub, dom)) {
+            out.push_back(cell);
         }
     }
     return out;
 }
 
 void offset_map_t::insert_cell(const cell_t& c) {
-    offset_t key = c.get_offset();
-    _map[key].insert(c);
+    set.insert(c);
 }
 
 std::optional<cell_t> offset_map_t::get_cell(offset_t o, unsigned size) {
-    cell_set_t& cells = _map[o];
-    auto it = cells.find(cell_t(o, size));
-    if (it != cells.end()) {
-        return *it;
+    cell_t res{o, size};
+    if (!set.contains(res)) {
+        return {};
     }
-    // not found
-    return {};
+    return res;
 }
 
 cell_t offset_map_t::mk_cell(offset_t o, unsigned size) {
@@ -307,145 +84,33 @@ cell_t offset_map_t::mk_cell(offset_t o, unsigned size) {
 // Return all cells that might overlap with (o, size).
 std::vector<cell_t> offset_map_t::get_overlap_cells(offset_t o, unsigned size) {
     std::vector<cell_t> out;
-    compare_binding_t comp;
-
-    bool added = false;
-    auto maybe_c = get_cell(o, size);
-    if (!maybe_c) {
-        maybe_c = cell_t(o, size);
-        insert_cell(*maybe_c);
-        added = true;
-    }
-
-    auto lb_it = std::lower_bound(_map.begin(), _map.end(), o, comp);
-    if (lb_it != _map.end()) {
-        // Store _map[begin,...,lb_it] into a vector so that we can
-        // go backwards from lb_it.
-        //
-        // TODO: give support for reverse iterator in patricia_tree.
-        std::vector<cell_set_t> upto_lb;
-        upto_lb.reserve(std::distance(_map.begin(), lb_it));
-        for (auto it = _map.begin(), et = lb_it; it != et; ++it) {
-            upto_lb.push_back(it->second);
-        }
-        upto_lb.push_back(lb_it->second);
-
-        for (int i = static_cast<int>(upto_lb.size() - 1); i >= 0; --i) {
-            ///////
-            // All the cells in upto_lb[i] have the same offset. They
-            // just differ in the size.
-            //
-            // If none of the cells in upto_lb[i] overlap with (o, size)
-            // we can stop.
-            ////////
-            bool continue_outer_loop = false;
-            for (const cell_t& x : upto_lb[i]) {
-                if (x.overlap(o, size)) {
-                    if (!(x == *maybe_c)) {
-                        // FIXME: we might have some duplicates. this is a very drastic solution.
-                        if (std::find(out.begin(), out.end(), x) == out.end()) {
-                            out.push_back(x);
-                        }
-                    }
-                    continue_outer_loop = true;
-                }
-            }
-            if (!continue_outer_loop) {
-                break;
-            }
+    for (const cell_t& c : set) {
+        if (c.overlap(o, size)) {
+            out.push_back(c);
         }
     }
-
-    // search for overlapping cells > o
-    auto ub_it = std::upper_bound(_map.begin(), _map.end(), o, comp);
-    for (; ub_it != _map.end(); ++ub_it) {
-        bool continue_outer_loop = false;
-        for (const cell_t& x : ub_it->second) {
-            if (x.overlap(o, size)) {
-                // FIXME: we might have some duplicates. this is a very drastic solution.
-                if (std::find(out.begin(), out.end(), x) == out.end()) {
-                    out.push_back(x);
-                }
-                continue_outer_loop = true;
-            }
-        }
-        if (!continue_outer_loop) {
-            break;
-        }
-    }
-
-    // do not forget the rest of overlapping cells == o
-    for (auto it = ++lb_it, et = ub_it; it != et; ++it) {
-        bool continue_outer_loop = false;
-        for (const cell_t& x : it->second) {
-            if (x == *maybe_c) { // we dont put it in out
-                continue;
-            }
-            if (x.overlap(o, size)) {
-                if (std::find(out.begin(), out.end(), x) == out.end()) {
-                    out.push_back(x);
-                }
-                continue_outer_loop = true;
-            }
-        }
-        if (!continue_outer_loop) {
-            break;
-        }
-    }
-
-    if (added) {
-        remove_cell(*maybe_c);
-    }
     return out;
 }
 
-// We use a global array map
-using array_map_t = std::unordered_map<data_kind_t, offset_map_t>;
-
-static thread_local crab::lazy_allocator<array_map_t> global_array_map;
-
-void clear_thread_local_state()
-{
-    global_array_map.clear();
-}
-
-static offset_map_t& lookup_array_map(data_kind_t kind) {
-    return (*global_array_map)[kind];
-}
-
-/**
-    Ugly this needs to be fixed: needed if multiple analyses are
-    run so we can clear the array map from one run to another.
-**/
-void clear_global_state() {
-    if (!global_array_map->empty()) {
-        if constexpr (crab::CrabSanityCheckFlag) {
-            CRAB_WARN("array_expansion static variable map is being cleared");
-        }
-        global_array_map->clear();
-    }
-}
-
 void array_domain_t::initialize_numbers(int lb, int width) {
     num_bytes.reset(lb, width);
-    lookup_array_map(data_kind_t::svalues).mk_cell(lb, width);
+    array_map[data_kind_t::svalues].mk_cell(lb, width);
 }
 
 std::ostream& operator<<(std::ostream& o, offset_map_t& m) {
-    if (m._map.empty()) {
+    if (m.set.empty()) {
         o << "empty";
     } else {
-        for (const auto& [_offset, cells] : m._map) {
-            o << "{";
-            for (auto cit = cells.begin(), cet = cells.end(); cit != cet;) {
-                o << *cit;
-                ++cit;
-                if (cit != cet) {
+        bool first = true;
+        o << "{";
+        for (const cell_t& cell : m.set) {
+            o << cell;
+            if (!first) {
                     o << ",";
-                }
             }
-            o << "}\n";
+            first = false;
         }
+        o << "}\n";
     }
     return o;
 }
@@ -459,8 +124,7 @@ void array_domain_t::split_cell(NumAbsDomain& inv, data_kind_t kind, int cell_st
     std::optional<linear_expression_t> uvalue = load(inv, data_kind_t::uvalues, number_t(cell_start_index), len);
 
     // Create a new cell for that range.
-    offset_map_t& offset_map = lookup_array_map(kind);
-    cell_t new_cell = offset_map.mk_cell(cell_start_index, len);
+    cell_t new_cell = array_map[kind].mk_cell(cell_start_index, len);
     inv.assign(new_cell.get_scalar(data_kind_t::svalues), svalue);
     inv.assign(new_cell.get_scalar(data_kind_t::uvalues), uvalue);
 }
@@ -470,7 +134,7 @@ void array_domain_t::split_cell(NumAbsDomain& inv, data_kind_t kind, int cell_st
 void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i,
                                       const linear_expression_t& elem_size) {
     assert(kind == data_kind_t::svalues || kind == data_kind_t::uvalues);
-    offset_map_t& offset_map = lookup_array_map(kind);
+    offset_map_t& offset_map = array_map[kind];
     interval_t ii = inv.eval_interval(i);
     std::optional<number_t> n = ii.singleton();
     if (!n) {
@@ -513,11 +177,10 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
 }
 
 // we can only treat this as non-member because we use global state
-static std::optional<std::pair<offset_t, unsigned>>
-kill_and_find_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i, const linear_expression_t& elem_size) {
+std::optional<std::pair<offset_t, unsigned>> array_domain_t::kill_and_find_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i, const linear_expression_t& elem_size) {
     std::optional<std::pair<offset_t, unsigned>> res;
 
-    offset_map_t& offset_map = lookup_array_map(kind);
+    offset_map_t& offset_map = array_map[kind];
     interval_t ii = inv.eval_interval(i);
     std::vector<cell_t> cells;
     if (std::optional<number_t> n = ii.singleton()) {
@@ -526,7 +189,7 @@ kill_and_find_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t
         if (n_bytes) {
             auto size = static_cast<unsigned int>(*n_bytes);
             // -- Constant index: kill overlapping cells
-            offset_t o((uint64_t)*n);
+            auto o((uint64_t)*n);
             cells = offset_map.get_overlap_cells(o, size);
             res = std::make_pair(o, size);
         }
@@ -553,7 +216,7 @@ kill_and_find_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t
     return res;
 }
 
-bool array_domain_t::all_num(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) {
+bool array_domain_t::all_num(const NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) {
     auto min_lb = inv.eval_interval(lb).lb().number();
     auto max_ub = inv.eval_interval(ub).ub().number();
     if (!min_lb || !max_ub || !min_lb->fits_sint32() || !max_ub->fits_sint32())
@@ -580,7 +243,7 @@ int array_domain_t::min_all_num_size(const NumAbsDomain& inv, variable_t offset)
 }
 
 // Get one byte of a value.
-std::optional<uint8_t> get_value_byte(NumAbsDomain& inv, offset_t o, int width) {
+std::optional<uint8_t> get_value_byte(const NumAbsDomain& inv, offset_t o, int width) {
     variable_t v = variable_t::cell_var(data_kind_t::svalues, (o / width) * width, width);
     std::optional<number_t> t = inv.eval_interval(v).singleton();
     if (!t) {
@@ -609,15 +272,15 @@ std::optional<uint8_t> get_value_byte(NumAbsDomain& inv, offset_t o, int width)
             n = boost::endian::native_to_little<uint64_t>(n);
         break;
     }
-    uint8_t* bytes = (uint8_t*)&n;
+    auto* bytes = (uint8_t*)&n;
     return bytes[o % width];
 }
 
 std::optional<linear_expression_t> array_domain_t::load(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i, int width) {
     interval_t ii = inv.eval_interval(i);
     if (std::optional<number_t> n = ii.singleton()) {
-        offset_map_t& offset_map = lookup_array_map(kind);
-        int64_t k = (int64_t)*n;
+        offset_map_t& offset_map = array_map[kind];
+        auto k = (int64_t)*n;
         if (kind == data_kind_t::types) {
             auto [only_num, only_non_num] = num_bytes.uniformity(k, width);
             if (only_num) {
@@ -629,7 +292,7 @@ std::optional<linear_expression_t> array_domain_t::load(NumAbsDomain& inv, data_
         }
         offset_t o(k);
         unsigned size = (long)width;
-        if (auto cell = lookup_array_map(kind).get_cell(o, size)) {
+        if (auto cell = array_map[kind].get_cell(o, size)) {
             return cell->get_scalar(kind);
         }
         if ((kind == data_kind_t::svalues) || (kind == data_kind_t::uvalues)) {
@@ -731,9 +394,9 @@ std::optional<linear_expression_t> array_domain_t::load(NumAbsDomain& inv, data_
 // We are about to write to a given range of bytes on the stack.
 // Any cells covering that range need to be removed, and any cells that only
 // partially cover that range can be split such that any non-covered portions become new cells.
-static std::optional<std::pair<offset_t, unsigned>> split_and_find_var(array_domain_t& array_domain, NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx, const linear_expression_t& elem_size) {
+std::optional<std::pair<offset_t, unsigned>> array_domain_t::split_and_find_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx, const linear_expression_t& elem_size) {
     if (kind == data_kind_t::svalues || kind == data_kind_t::uvalues) {
-        array_domain.split_number_var(inv, kind, idx, elem_size);
+        this->split_number_var(inv, kind, idx, elem_size);
     }
     return kill_and_find_var(inv, kind, idx, elem_size);
 }
@@ -743,7 +406,7 @@ std::optional<variable_t> array_domain_t::store(NumAbsDomain& inv, data_kind_t k
                                                 const linear_expression_t& idx,
                                                 const linear_expression_t& elem_size,
                                                 const linear_expression_t& val) {
-    auto maybe_cell = split_and_find_var(*this, inv, kind, idx, elem_size);
+    auto maybe_cell = split_and_find_var(inv, kind, idx, elem_size);
     if (maybe_cell) {
         // perform strong update
         auto [offset, size] = *maybe_cell;
@@ -754,7 +417,7 @@ std::optional<variable_t> array_domain_t::store(NumAbsDomain& inv, data_kind_t k
             else
                 num_bytes.havoc(offset, size);
         }
-        variable_t v = lookup_array_map(kind).mk_cell(offset, size).get_scalar(kind);
+        variable_t v = array_map[kind].mk_cell(offset, size).get_scalar(kind);
         return v;
     }
     return {};
@@ -765,7 +428,7 @@ std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv,
                                                      const linear_expression_t& elem_size,
                                                      const linear_expression_t& val) {
     auto kind = data_kind_t::types;
-    auto maybe_cell = split_and_find_var(*this, inv, kind, idx, elem_size);
+    auto maybe_cell = split_and_find_var(inv, kind, idx, elem_size);
     if (maybe_cell) {
         // perform strong update
         auto [offset, size] = *maybe_cell;
@@ -774,7 +437,7 @@ std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv,
             num_bytes.reset(offset, size);
         else
             num_bytes.havoc(offset, size);
-        variable_t v = lookup_array_map(kind).mk_cell(offset, size).get_scalar(kind);
+        variable_t v = array_map[kind].mk_cell(offset, size).get_scalar(kind);
         return v;
     }
     return {};
@@ -788,14 +451,14 @@ std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv,
 }
 
 void array_domain_t::havoc(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx, const linear_expression_t& elem_size) {
-    auto maybe_cell = split_and_find_var(*this, inv, kind, idx, elem_size);
+    auto maybe_cell = split_and_find_var(inv, kind, idx, elem_size);
     if (maybe_cell && kind == data_kind_t::types) {
         auto [offset, size] = *maybe_cell;
         num_bytes.havoc(offset, size);
     }
 }
 
-void array_domain_t::store_numbers(NumAbsDomain& inv, variable_t _idx, variable_t _width) {
+void array_domain_t::store_numbers(const NumAbsDomain& inv, variable_t _idx, variable_t _width) {
 
     // TODO: this should be an user parameter.
     const number_t max_num_elems = EBPF_STACK_SIZE;
@@ -827,7 +490,10 @@ void array_domain_t::set_to_top() {
     num_bytes.set_to_top();
 }
 
-void array_domain_t::set_to_bottom() { num_bytes.set_to_bottom(); }
+void array_domain_t::set_to_bottom() {
+    num_bytes.set_to_bottom();
+    array_map.set_to_bottom();
+}
 
 bool array_domain_t::is_bottom() const { return num_bytes.is_bottom(); }
 
@@ -835,10 +501,10 @@ bool array_domain_t::is_top() const { return num_bytes.is_top(); }
 
 string_invariant array_domain_t::to_set() const { return num_bytes.to_set(); }
 
-bool array_domain_t::operator<=(const array_domain_t& other) const { return num_bytes <= other.num_bytes; }
+bool array_domain_t::operator<=(const array_domain_t& other) const { return num_bytes <= other.num_bytes && array_map <= other.array_map; }
 
 bool array_domain_t::operator==(const array_domain_t& other) const {
-    return num_bytes == other.num_bytes;
+    return num_bytes == other.num_bytes && array_map == other.array_map;
 }
 
 void array_domain_t::operator|=(const array_domain_t& other) {
@@ -847,26 +513,27 @@ void array_domain_t::operator|=(const array_domain_t& other) {
         return;
     }
     num_bytes |= other.num_bytes;
+    array_map |= other.array_map;
 }
 
 array_domain_t array_domain_t::operator|(const array_domain_t& other) const {
-    return array_domain_t(num_bytes | other.num_bytes);
+    return array_domain_t(num_bytes | other.num_bytes, array_map | other.array_map);
 }
 
 array_domain_t array_domain_t::operator&(const array_domain_t& other) const {
-    return array_domain_t(num_bytes & other.num_bytes);
+    return array_domain_t(num_bytes & other.num_bytes, array_map & other.array_map);
 }
 
 array_domain_t array_domain_t::widen(const array_domain_t& other) const {
-    return array_domain_t(num_bytes | other.num_bytes);
+    return array_domain_t(num_bytes | other.num_bytes, array_map | other.array_map);
 }
 
 array_domain_t array_domain_t::widening_thresholds(const array_domain_t& other, const iterators::thresholds_t& ts) const {
-    return array_domain_t(num_bytes | other.num_bytes);
+    return array_domain_t(num_bytes | other.num_bytes, array_map | other.array_map);
 }
 
 array_domain_t array_domain_t::narrow(const array_domain_t& other) const {
-    return array_domain_t(num_bytes & other.num_bytes);
+    return array_domain_t(num_bytes & other.num_bytes, array_map & other.array_map);
 }
 
 std::ostream& operator<<(std::ostream& o, const array_domain_t& dom) {
diff --git a/src/crab/array_domain.hpp b/src/crab/array_domain.hpp
index 70525cb90..f15000e5c 100644
--- a/src/crab/array_domain.hpp
+++ b/src/crab/array_domain.hpp
@@ -27,8 +27,10 @@
 #include <optional>
 #include <utility>
 
-#include "crab/variable.hpp"
+#include <boost/container/flat_map.hpp>
+
 #include "crab/add_bottom.hpp"
+#include "crab/variable.hpp"
 
 #include "crab/bitset_domain.hpp"
 
@@ -37,17 +39,272 @@ namespace crab::domains {
 // Numerical abstract domain.
 using NumAbsDomain = AddBottom;
 
-void clear_global_state();
+using offset_t = index_t;
+class offset_map_t;
+
+/***
+   Conceptually, a cell is tuple of an array, offset, size, and
+   scalar variable such that:
+
+_scalar = array[_offset, _offset + 1, ..., _offset + _size - 1]
+
+    For simplicity, we don't carry the array inside the cell class.
+    Only, offset_map objects can create cells. They will consider the
+            array when generating the scalar variable.
+*/
+class cell_t final {
+  private:
+    friend class offset_map_t;
+    friend std::ostream& operator<<(std::ostream& o, offset_map_t& m);
+    offset_t _offset{};
+    unsigned _size{};
+
+    static interval_t to_interval(const offset_t o, unsigned size) {
+        return {number_t{static_cast<int>(o)}, number_t{static_cast<int>(o)} + number_t{static_cast<int>(size - 1)}};
+    }
+    cell_t(offset_t offset, unsigned size) : _offset(offset), _size(size) {}
+
+  public:
+    // Only offset_map_t can create cells
+    cell_t() = delete;
+
+    [[nodiscard]]
+    interval_t to_interval() const {
+        return to_interval(_offset, _size);
+    }
+
+    [[nodiscard]]
+    offset_t get_offset() const {
+        return _offset;
+    }
+
+    [[nodiscard]]
+    variable_t get_scalar(data_kind_t kind) const {
+        return variable_t::cell_var(kind, number_t{_offset}, _size);
+    }
+
+    // ignore the scalar variable
+    bool operator==(const cell_t& o) const { return to_interval() == o.to_interval(); }
+
+    // ignore the scalar variable
+    bool operator<(const cell_t& o) const {
+        if (_offset == o._offset)
+            return _size < o._size;
+        return _offset < o._offset;
+    }
+
+    // Return true if [o, o + size) definitely overlaps with the cell,
+    // where o is a constant expression.
+    [[nodiscard]]
+    bool overlap(const offset_t& o, unsigned size) const {
+        interval_t x = to_interval();
+        interval_t y = to_interval(o, size);
+        bool res = (!(x & y).is_bottom());
+        CRAB_LOG("array-expansion-overlap",
+                 std::cout << "**Checking if " << x << " overlaps with " << y << "=" << res << "\n";);
+        return res;
+    }
+
+    // Return true if [symb_lb, symb_ub] may overlap with the cell,
+    // where symb_lb and symb_ub are not constant expressions.
+    [[nodiscard]]
+    bool symbolic_overlap(const linear_expression_t& symb_lb, const linear_expression_t& symb_ub,
+                          const NumAbsDomain& dom) const;
+
+    friend std::ostream& operator<<(std::ostream& o, const cell_t& c) { return o << "cell(" << c.to_interval() << ")"; }
+};
+
+// Map offsets to cells
+class offset_map_t final {
+  private:
+    friend class array_domain_t;
+
+    std::set<cell_t> set;
+
+    void remove_cell(const cell_t& c);
+
+    void insert_cell(const cell_t& c);
+
+    [[nodiscard]]
+    std::optional<cell_t> get_cell(offset_t o, unsigned size);
+
+    cell_t mk_cell(offset_t o, unsigned size);
+
+  public:
+    offset_map_t() = default;
 
-void clear_thread_local_state();
+    [[nodiscard]]
+    bool empty() const {
+        return set.empty();
+    }
+
+    [[nodiscard]]
+    std::size_t size() const {
+        return set.size();
+    }
+
+    void operator-=(const cell_t& c) { remove_cell(c); }
+
+    void operator-=(const std::vector<cell_t>& cells) {
+        for (auto const& c : cells) {
+            this->operator-=(c);
+        }
+    }
+
+    // Return in out all cells that might overlap with (o, size).
+    std::vector<cell_t> get_overlap_cells(offset_t o, unsigned size);
+
+    [[nodiscard]]
+    std::vector<cell_t> get_overlap_cells_symbolic_offset(const NumAbsDomain& dom, const linear_expression_t& symb_lb,
+                                                          const linear_expression_t& symb_ub);
+
+    friend std::ostream& operator<<(std::ostream& o, offset_map_t& m);
+
+    /* Operations needed if used as value in a separate_domain */
+    [[nodiscard]]
+    bool is_top() const {
+        return empty();
+    }
+    [[nodiscard]]
+    bool is_bottom() const {
+        return false;
+    }
+    /*
+       We don't distinguish between bottom and top.
+       This is fine because separate_domain only calls bottom if
+       operator[] is called over a bottom state. Thus, we will make
+       sure that we don't call operator[] in that case.
+    */
+    static offset_map_t bottom() { return {}; }
+    static offset_map_t top() { return {}; }
+    bool operator<=(const offset_map_t& other) const {
+        return std::includes(set.begin(), set.end(), other.set.begin(), other.set.end());
+    }
+    bool operator==(const offset_map_t& other) const { return set == other.set; }
+    offset_map_t operator|(const offset_map_t& other) const {
+        offset_map_t res;
+        std::set_union(set.begin(), set.end(), other.set.begin(), other.set.end(),
+                       std::inserter(res.set, res.set.begin()));
+        return res;
+    }
+    offset_map_t operator&(const offset_map_t& other) const {
+        offset_map_t res;
+        std::set_intersection(set.begin(), set.end(), other.set.begin(), other.set.end(),
+                              std::inserter(res.set, res.set.begin()));
+        return res;
+    }
+};
+
+// map abstract domain. Lattice operations are memberwise.
+class array_map_t {
+    boost::container::flat_map<data_kind_t, offset_map_t> map;
+
+  public:
+    array_map_t() = default;
+
+    [[nodiscard]]
+    bool empty() const {
+        return map.empty();
+    }
+
+    [[nodiscard]]
+    std::size_t size() const {
+        return map.size();
+    }
+    bool operator==(const array_map_t& other) const = default;
+
+    offset_map_t& operator[](data_kind_t kind) {
+        return map[kind];
+    }
+
+    const offset_map_t& operator[](data_kind_t kind) const {
+        return map.at(kind);
+    }
+
+    void operator-=(const cell_t& c) {
+        for (auto& [_, v] : map) {
+            v -= c;
+        }
+    }
+
+    void operator-=(const std::vector<cell_t>& cells) {
+        for (auto const& c : cells) {
+            this->operator-=(c);
+        }
+    }
+
+    [[nodiscard]]
+    std::vector<cell_t> get_overlap_cells(data_kind_t kind, offset_t o, unsigned size) {
+        auto it = map.find(kind);
+        if (it != map.end()) {
+            return it->second.get_overlap_cells(o, size);
+        }
+        return {};
+    }
+
+    [[nodiscard]]
+    std::vector<cell_t> get_overlap_cells_symbolic_offset(data_kind_t kind, const NumAbsDomain& dom,
+                                                          const linear_expression_t& symb_lb,
+                                                          const linear_expression_t& symb_ub) {
+        auto it = map.find(kind);
+        if (it != map.end()) {
+            return it->second.get_overlap_cells_symbolic_offset(dom, symb_lb, symb_ub);
+        }
+        return {};
+    }
+
+    array_map_t operator|(const array_map_t& other) const {
+        array_map_t res;
+        for (auto& [kind, offset_map] : map) {
+            auto it = other.map.find(kind);
+            if (it != other.map.end()) {
+                res.map[kind] = offset_map | it->second;
+            } else {
+                res.map[kind] = offset_map;
+            }
+        }
+        for (auto& [kind, offset_map] : other.map) {
+            if (res.map.find(kind) == res.map.end()) {
+                res.map[kind] = offset_map;
+            }
+        }
+        return res;
+    }
+
+    array_map_t operator&(const array_map_t& other) const {
+        array_map_t res;
+        for (auto& [kind, offset_map] : map) {
+            auto it = other.map.find(kind);
+            if (it != other.map.end()) {
+                res.map[kind] = offset_map & it->second;
+            }
+        }
+        return res;
+    }
+
+    bool operator<=(const array_map_t& other) const {
+        return std::ranges::all_of(map, [&other](const auto& p) {
+            auto it = other.map.find(p.first);
+            return it != other.map.end() && p.second <= it->second;
+        });
+    }
+
+    array_map_t& operator|=(const array_map_t& other) {
+        *this = *this | other;
+        return *this;
+    }
+    void set_to_bottom() { map.clear(); }
+};
 
 class array_domain_t final {
     bitset_domain_t num_bytes;
+    array_map_t array_map;
 
   public:
     array_domain_t() = default;
 
-    array_domain_t(const bitset_domain_t& num_bytes) : num_bytes(num_bytes) { }
+    array_domain_t(const bitset_domain_t& num_bytes, array_map_t array_map)
+        : num_bytes(num_bytes), array_map(std::move(array_map)) {}
 
     void set_to_top();
     void set_to_bottom();
@@ -68,30 +325,35 @@ class array_domain_t final {
     friend std::ostream& operator<<(std::ostream& o, const array_domain_t& dom);
     [[nodiscard]] string_invariant to_set() const;
 
-    bool all_num(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub);
+    bool all_num(const NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub);
     [[nodiscard]] int min_all_num_size(const NumAbsDomain& inv, variable_t offset) const;
 
-    std::optional<linear_expression_t> load(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i, int width);
-    std::optional<variable_t> store(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx, const linear_expression_t& elem_size,
-                                    const linear_expression_t& val);
-    std::optional<variable_t> store_type(NumAbsDomain& inv,
-                                         const linear_expression_t& idx,
-                                         const linear_expression_t& elem_size,
-                                         const linear_expression_t& val);
-    std::optional<variable_t> store_type(NumAbsDomain& inv,
-                                         const linear_expression_t& idx,
-                                         const linear_expression_t& elem_size,
-                                         const Reg& reg);
-    void havoc(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx, const linear_expression_t& elem_size);
+    std::optional<linear_expression_t> load(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i,
+                                            int width);
+    std::optional<variable_t> store(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx,
+                                    const linear_expression_t& elem_size, const linear_expression_t& val);
+    std::optional<variable_t> store_type(NumAbsDomain& inv, const linear_expression_t& idx,
+                                         const linear_expression_t& elem_size, const linear_expression_t& val);
+    std::optional<variable_t> store_type(NumAbsDomain& inv, const linear_expression_t& idx,
+                                         const linear_expression_t& elem_size, const Reg& reg);
+    void havoc(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx,
+               const linear_expression_t& elem_size);
 
     // Perform array stores over an array segment
-    void store_numbers(NumAbsDomain& inv, variable_t _idx, variable_t _width);
+    void store_numbers(const NumAbsDomain& inv, variable_t _idx, variable_t _width);
 
     void split_number_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i,
                           const linear_expression_t& elem_size);
     void split_cell(NumAbsDomain& inv, data_kind_t kind, int cell_start_index, unsigned int len);
 
     void initialize_numbers(int lb, int width);
+
+    std::optional<std::pair<offset_t, unsigned>> split_and_find_var(NumAbsDomain& inv, data_kind_t kind,
+                                                                        const linear_expression_t& idx,
+                                                                        const linear_expression_t& elem_size);
+    std::optional<std::pair<offset_t, unsigned>> kill_and_find_var(NumAbsDomain& inv, data_kind_t kind,
+                                                                   const linear_expression_t& i,
+                                                                   const linear_expression_t& elem_size);
 };
 
-}
+} // namespace crab::domains
diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
index 200c6b469..8b74978bc 100644
--- a/src/crab/ebpf_domain.cpp
+++ b/src/crab/ebpf_domain.cpp
@@ -1152,6 +1152,7 @@ void ebpf_domain_t::assume(const linear_constraint_t& cst) { crab::assume(m_inv,
 void ebpf_domain_t::require(NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& s) {
     if (check_require)
         check_require(inv, cst, s + " (" + this->current_assertion + ")");
+
     if (thread_local_options.assume_assertions) {
         // avoid redundant errors
         crab::assume(inv, cst);
@@ -2069,8 +2070,10 @@ void ebpf_domain_t::do_store_stack(NumAbsDomain& inv, const number_t& width, con
     std::optional<variable_t> var = stack.store_type(inv, addr, width, val_type);
     type_inv.assign_type(inv, var, val_type);
     if (width == 8) {
-        inv.assign(stack.store(inv, data_kind_t::svalues, addr, width, val_svalue), val_svalue);
-        inv.assign(stack.store(inv, data_kind_t::uvalues, addr, width, val_uvalue), val_uvalue);
+        auto slot_svalue = stack.store(inv, data_kind_t::svalues, addr, width, val_svalue);
+        auto slot_uvalue = stack.store(inv, data_kind_t::uvalues, addr, width, val_uvalue);
+        inv.assign(slot_svalue, val_svalue);
+        inv.assign(slot_uvalue, val_uvalue);
 
         if (opt_val_reg && type_inv.has_type(m_inv, val_type, T_CTX)) {
             inv.assign(stack.store(inv, data_kind_t::ctx_offsets, addr, width, opt_val_reg->ctx_offset),
diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp
index 39f11e73b..98f1b386c 100644
--- a/src/crab/ebpf_domain.hpp
+++ b/src/crab/ebpf_domain.hpp
@@ -214,6 +214,7 @@ class ebpf_domain_t final {
     crab::domains::array_domain_t stack;
 
     std::function<check_require_func_t> check_require{};
+
     bool get_map_fd_range(const Reg& map_fd_reg, int32_t* start_fd, int32_t* end_fd) const;
 
     struct TypeDomain {
diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp
index 81f543e33..1f4ad9a93 100644
--- a/src/crab_verifier.cpp
+++ b/src/crab_verifier.cpp
@@ -145,7 +145,6 @@ static checks_db get_analysis_report(std::ostream& s, cfg_t& cfg, crab::invarian
 static checks_db get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info,
                                  const ebpf_verifier_options_t* options) {
     global_program_info = std::move(info);
-    crab::domains::clear_global_state();
     crab::variable_t::clear_thread_local_state();
     thread_local_options = *options;
 
@@ -188,7 +187,6 @@ std::tuple<string_invariant, bool> ebpf_analyze_program_for_test(std::ostream& o
                                                                  const string_invariant& entry_invariant,
                                                                  const program_info& info,
                                                                  const ebpf_verifier_options_t& options) {
-    crab::domains::clear_global_state();
     crab::variable_t::clear_thread_local_state();
 
     thread_local_options = options;
@@ -233,6 +231,5 @@ void ebpf_verifier_clear_thread_local_state() {
     crab::variable_t::clear_thread_local_state();
     crab::CrabStats::clear_thread_local_state();
     global_program_info.clear();
-    crab::domains::clear_thread_local_state();
     crab::domains::SplitDBM::clear_thread_local_state();
 }

From ed4586f2ed7e1a3a489641843edef626cdb76856 Mon Sep 17 00:00:00 2001
From: Elazar Gershuni <elazarg@gmail.com>
Date: Tue, 3 Sep 2024 18:01:09 +0300
Subject: [PATCH 2/3] clang-format

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>
---
 .clang-format             |   3 +
 src/crab/array_domain.cpp | 123 +++++++++--------
 src/crab/array_domain.hpp |  27 ++--
 src/crab/ebpf_domain.cpp  | 277 ++++++++++++++++++++++++--------------
 src/crab/ebpf_domain.hpp  |  75 +++++++----
 src/crab_verifier.cpp     |  26 ++--
 6 files changed, 322 insertions(+), 209 deletions(-)

diff --git a/.clang-format b/.clang-format
index 09976dd24..dddcb124f 100644
--- a/.clang-format
+++ b/.clang-format
@@ -7,3 +7,6 @@ AlignEscapedNewlines: Left
 BreakAfterAttributes: Always
 PenaltyReturnTypeOnItsOwnLine: 60
 AlwaysBreakAfterReturnType: None
+Cpp11BracedListStyle: true
+BreakBeforeBraces: Attach
+InsertBraces: true
diff --git a/src/crab/array_domain.cpp b/src/crab/array_domain.cpp
index 992de72f2..7990e5da7 100644
--- a/src/crab/array_domain.cpp
+++ b/src/crab/array_domain.cpp
@@ -18,8 +18,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 bound_t& x, const linear_expression_t& symb_lb,
                           const linear_expression_t& symb_ub) {
     using namespace dsl_syntax;
     assert(x.is_finite());
@@ -35,13 +34,10 @@ static bool maybe_between(const NumAbsDomain& dom, const bound_t& x,
 bool cell_t::symbolic_overlap(const linear_expression_t& symb_lb, const linear_expression_t& symb_ub,
                               const NumAbsDomain& dom) const {
     interval_t x = to_interval();
-    return maybe_between(dom, x.lb(), symb_lb, symb_ub)
-        || maybe_between(dom, x.ub(), symb_lb, symb_ub);
+    return maybe_between(dom, x.lb(), symb_lb, symb_ub) || maybe_between(dom, x.ub(), symb_lb, symb_ub);
 }
 
-void offset_map_t::remove_cell(const cell_t& c) {
-    set.erase(c);
-}
+void offset_map_t::remove_cell(const cell_t& c) { set.erase(c); }
 
 [[nodiscard]]
 std::vector<cell_t> offset_map_t::get_overlap_cells_symbolic_offset(const NumAbsDomain& dom,
@@ -56,9 +52,7 @@ std::vector<cell_t> offset_map_t::get_overlap_cells_symbolic_offset(const NumAbs
     return out;
 }
 
-void offset_map_t::insert_cell(const cell_t& c) {
-    set.insert(c);
-}
+void offset_map_t::insert_cell(const cell_t& c) { set.insert(c); }
 
 std::optional<cell_t> offset_map_t::get_cell(offset_t o, unsigned size) {
     cell_t res{o, size};
@@ -72,8 +66,9 @@ cell_t offset_map_t::mk_cell(offset_t o, unsigned size) {
     // TODO: check array is the array associated to this offset map
 
     auto maybe_c = get_cell(o, size);
-    if (maybe_c)
+    if (maybe_c) {
         return *maybe_c;
+    }
     // create a new scalar variable for representing the contents
     // of bytes array[o,o+1,..., o+size-1]
     cell_t c(o, size);
@@ -106,7 +101,7 @@ std::ostream& operator<<(std::ostream& o, offset_map_t& m) {
         for (const cell_t& cell : m.set) {
             o << cell;
             if (!first) {
-                    o << ",";
+                o << ",";
             }
             first = false;
         }
@@ -156,7 +151,8 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
         int cell_start_index = (int)*intv.lb().number();
         int cell_end_index = (int)*intv.ub().number();
 
-        if (!this->num_bytes.all_num(cell_start_index, cell_end_index + 1) || (cell_end_index + 1 < cell_start_index + sizeof(int64_t))) {
+        if (!this->num_bytes.all_num(cell_start_index, cell_end_index + 1) ||
+            (cell_end_index + 1 < cell_start_index + sizeof(int64_t))) {
             // We can only split numeric cells of size 8 or less.
             continue;
         }
@@ -177,7 +173,9 @@ void array_domain_t::split_number_var(NumAbsDomain& inv, data_kind_t kind, const
 }
 
 // we can only treat this as non-member because we use global state
-std::optional<std::pair<offset_t, unsigned>> array_domain_t::kill_and_find_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i, const linear_expression_t& elem_size) {
+std::optional<std::pair<offset_t, unsigned>> array_domain_t::kill_and_find_var(NumAbsDomain& inv, data_kind_t kind,
+                                                                               const linear_expression_t& i,
+                                                                               const linear_expression_t& elem_size) {
     std::optional<std::pair<offset_t, unsigned>> res;
 
     offset_map_t& offset_map = array_map[kind];
@@ -219,14 +217,16 @@ std::optional<std::pair<offset_t, unsigned>> array_domain_t::kill_and_find_var(N
 bool array_domain_t::all_num(const NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) {
     auto min_lb = inv.eval_interval(lb).lb().number();
     auto max_ub = inv.eval_interval(ub).ub().number();
-    if (!min_lb || !max_ub || !min_lb->fits_sint32() || !max_ub->fits_sint32())
+    if (!min_lb || !max_ub || !min_lb->fits_sint32() || !max_ub->fits_sint32()) {
         return false;
+    }
 
     // The all_num() call requires a legal range. If we have an illegal range,
     // we should have already generated an error about the invalid range so just
     // return true now to avoid an extra error about a non-numeric range.
-    if (*min_lb >= *max_ub)
+    if (*min_lb >= *max_ub) {
         return true;
+    }
 
     return this->num_bytes.all_num((int32_t)*min_lb, (int32_t)*max_ub);
 }
@@ -235,8 +235,9 @@ bool array_domain_t::all_num(const NumAbsDomain& inv, const linear_expression_t&
 int array_domain_t::min_all_num_size(const NumAbsDomain& inv, variable_t offset) const {
     auto min_lb = inv.eval_interval(offset).lb().number();
     auto max_ub = inv.eval_interval(offset).ub().number();
-    if (!min_lb || !max_ub || !min_lb->fits_sint32() || !max_ub->fits_sint32())
+    if (!min_lb || !max_ub || !min_lb->fits_sint32() || !max_ub->fits_sint32()) {
         return 0;
+    }
     auto lb = (int)min_lb.value();
     auto ub = (int)max_ub.value();
     return std::max(0, this->num_bytes.all_num_width(lb) - (ub - lb));
@@ -254,29 +255,33 @@ std::optional<uint8_t> get_value_byte(const NumAbsDomain& inv, offset_t o, int w
     // Convert value to bytes of the appropriate endian-ness.
     switch (width) {
     case sizeof(uint16_t):
-        if (thread_local_options.big_endian)
+        if (thread_local_options.big_endian) {
             n = boost::endian::native_to_big<uint16_t>(n);
-        else
+        } else {
             n = boost::endian::native_to_little<uint16_t>(n);
+        }
         break;
     case sizeof(uint32_t):
-        if (thread_local_options.big_endian)
+        if (thread_local_options.big_endian) {
             n = boost::endian::native_to_big<uint32_t>(n);
-        else
+        } else {
             n = boost::endian::native_to_little<uint32_t>(n);
+        }
         break;
     case sizeof(uint64_t):
-        if (thread_local_options.big_endian)
+        if (thread_local_options.big_endian) {
             n = boost::endian::native_to_big<uint64_t>(n);
-        else
+        } else {
             n = boost::endian::native_to_little<uint64_t>(n);
+        }
         break;
     }
     auto* bytes = (uint8_t*)&n;
     return bytes[o % width];
 }
 
-std::optional<linear_expression_t> array_domain_t::load(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i, int width) {
+std::optional<linear_expression_t> array_domain_t::load(NumAbsDomain& inv, data_kind_t kind,
+                                                        const linear_expression_t& i, int width) {
     interval_t ii = inv.eval_interval(i);
     if (std::optional<number_t> n = ii.singleton()) {
         offset_map_t& offset_map = array_map[kind];
@@ -328,26 +333,29 @@ std::optional<linear_expression_t> array_domain_t::load(NumAbsDomain& inv, data_
                 }
                 if (size == 2) {
                     uint16_t b = *(uint16_t*)result_buffer;
-                    if (thread_local_options.big_endian)
+                    if (thread_local_options.big_endian) {
                         b = boost::endian::native_to_big<uint16_t>(b);
-                    else
+                    } else {
                         b = boost::endian::native_to_little<uint16_t>(b);
+                    }
                     return number_t{b};
                 }
                 if (size == 4) {
                     uint32_t b = *(uint32_t*)result_buffer;
-                    if (thread_local_options.big_endian)
+                    if (thread_local_options.big_endian) {
                         b = boost::endian::native_to_big<uint32_t>(b);
-                    else
+                    } else {
                         b = boost::endian::native_to_little<uint32_t>(b);
+                    }
                     return number_t{b};
                 }
                 if (size == 8) {
                     uint64_t b = *(uint64_t*)result_buffer;
-                    if (thread_local_options.big_endian)
+                    if (thread_local_options.big_endian) {
                         b = boost::endian::native_to_big<uint64_t>(b);
-                    else
+                    } else {
                         b = boost::endian::native_to_little<uint64_t>(b);
+                    }
                     return (kind == data_kind_t::uvalues) ? number_t(b) : number_t((int64_t)b);
                 }
             }
@@ -361,8 +369,8 @@ std::optional<linear_expression_t> array_domain_t::load(NumAbsDomain& inv, data_
             // would be unsound.
             return c.get_scalar(kind);
         } else {
-            CRAB_WARN("Ignored read from cell ", kind, "[", o, "...", o + size - 1, "]",
-                      " because it overlaps with ", cells.size(), " cells");
+            CRAB_WARN("Ignored read from cell ", kind, "[", o, "...", o + size - 1, "]", " because it overlaps with ",
+                      cells.size(), " cells");
             /*
                 TODO: we can apply here "Value Recomposition" 'a la'
                 Mine'06 (https://arxiv.org/pdf/cs/0703074.pdf)
@@ -394,28 +402,28 @@ std::optional<linear_expression_t> array_domain_t::load(NumAbsDomain& inv, data_
 // We are about to write to a given range of bytes on the stack.
 // Any cells covering that range need to be removed, and any cells that only
 // partially cover that range can be split such that any non-covered portions become new cells.
-std::optional<std::pair<offset_t, unsigned>> array_domain_t::split_and_find_var(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx, const linear_expression_t& elem_size) {
+std::optional<std::pair<offset_t, unsigned>> array_domain_t::split_and_find_var(NumAbsDomain& inv, data_kind_t kind,
+                                                                                const linear_expression_t& idx,
+                                                                                const linear_expression_t& elem_size) {
     if (kind == data_kind_t::svalues || kind == data_kind_t::uvalues) {
         this->split_number_var(inv, kind, idx, elem_size);
     }
     return kill_and_find_var(inv, kind, idx, elem_size);
 }
 
-
-std::optional<variable_t> array_domain_t::store(NumAbsDomain& inv, data_kind_t kind,
-                                                const linear_expression_t& idx,
-                                                const linear_expression_t& elem_size,
-                                                const linear_expression_t& val) {
+std::optional<variable_t> array_domain_t::store(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx,
+                                                const linear_expression_t& elem_size, const linear_expression_t& val) {
     auto maybe_cell = split_and_find_var(inv, kind, idx, elem_size);
     if (maybe_cell) {
         // perform strong update
         auto [offset, size] = *maybe_cell;
         if (kind == data_kind_t::types) {
             std::optional<number_t> t = inv.eval_interval(val).singleton();
-            if (t && (int64_t)*t == T_NUM)
+            if (t && (int64_t)*t == T_NUM) {
                 num_bytes.reset(offset, size);
-            else
+            } else {
                 num_bytes.havoc(offset, size);
+            }
         }
         variable_t v = array_map[kind].mk_cell(offset, size).get_scalar(kind);
         return v;
@@ -423,8 +431,7 @@ std::optional<variable_t> array_domain_t::store(NumAbsDomain& inv, data_kind_t k
     return {};
 }
 
-std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv,
-                                                     const linear_expression_t& idx,
+std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv, const linear_expression_t& idx,
                                                      const linear_expression_t& elem_size,
                                                      const linear_expression_t& val) {
     auto kind = data_kind_t::types;
@@ -433,24 +440,24 @@ std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv,
         // perform strong update
         auto [offset, size] = *maybe_cell;
         std::optional<number_t> t = inv.eval_interval(val).singleton();
-        if (t && (int64_t)*t == T_NUM)
+        if (t && (int64_t)*t == T_NUM) {
             num_bytes.reset(offset, size);
-        else
+        } else {
             num_bytes.havoc(offset, size);
+        }
         variable_t v = array_map[kind].mk_cell(offset, size).get_scalar(kind);
         return v;
     }
     return {};
 }
 
-std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv,
-                                                     const linear_expression_t& idx,
-                                                     const linear_expression_t& elem_size,
-                                                     const Reg& reg) {
+std::optional<variable_t> array_domain_t::store_type(NumAbsDomain& inv, const linear_expression_t& idx,
+                                                     const linear_expression_t& elem_size, const Reg& reg) {
     return store_type(inv, idx, elem_size, variable_t::reg(data_kind_t::types, reg.v));
 }
 
-void array_domain_t::havoc(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx, const linear_expression_t& elem_size) {
+void array_domain_t::havoc(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& idx,
+                           const linear_expression_t& elem_size) {
     auto maybe_cell = split_and_find_var(inv, kind, idx, elem_size);
     if (maybe_cell && kind == data_kind_t::types) {
         auto [offset, size] = *maybe_cell;
@@ -463,8 +470,9 @@ void array_domain_t::store_numbers(const NumAbsDomain& inv, variable_t _idx, var
     // TODO: this should be an user parameter.
     const number_t max_num_elems = EBPF_STACK_SIZE;
 
-    if (is_bottom())
+    if (is_bottom()) {
         return;
+    }
 
     std::optional<number_t> idx_n = inv[_idx].singleton();
     if (!idx_n) {
@@ -486,9 +494,7 @@ void array_domain_t::store_numbers(const NumAbsDomain& inv, variable_t _idx, var
     num_bytes.reset((int)*idx_n, (int)*width);
 }
 
-void array_domain_t::set_to_top() {
-    num_bytes.set_to_top();
-}
+void array_domain_t::set_to_top() { num_bytes.set_to_top(); }
 
 void array_domain_t::set_to_bottom() {
     num_bytes.set_to_bottom();
@@ -501,7 +507,9 @@ bool array_domain_t::is_top() const { return num_bytes.is_top(); }
 
 string_invariant array_domain_t::to_set() const { return num_bytes.to_set(); }
 
-bool array_domain_t::operator<=(const array_domain_t& other) const { return num_bytes <= other.num_bytes && array_map <= other.array_map; }
+bool array_domain_t::operator<=(const array_domain_t& other) const {
+    return num_bytes <= other.num_bytes && array_map <= other.array_map;
+}
 
 bool array_domain_t::operator==(const array_domain_t& other) const {
     return num_bytes == other.num_bytes && array_map == other.array_map;
@@ -528,7 +536,8 @@ array_domain_t array_domain_t::widen(const array_domain_t& other) const {
     return array_domain_t(num_bytes | other.num_bytes, array_map | other.array_map);
 }
 
-array_domain_t array_domain_t::widening_thresholds(const array_domain_t& other, const iterators::thresholds_t& ts) const {
+array_domain_t array_domain_t::widening_thresholds(const array_domain_t& other,
+                                                   const iterators::thresholds_t& ts) const {
     return array_domain_t(num_bytes | other.num_bytes, array_map | other.array_map);
 }
 
@@ -536,7 +545,5 @@ array_domain_t array_domain_t::narrow(const array_domain_t& other) const {
     return array_domain_t(num_bytes & other.num_bytes, array_map & other.array_map);
 }
 
-std::ostream& operator<<(std::ostream& o, const array_domain_t& dom) {
-    return o << dom.num_bytes;
-}
+std::ostream& operator<<(std::ostream& o, const array_domain_t& dom) { return o << dom.num_bytes; }
 } // namespace crab::domains
diff --git a/src/crab/array_domain.hpp b/src/crab/array_domain.hpp
index f15000e5c..8719e2828 100644
--- a/src/crab/array_domain.hpp
+++ b/src/crab/array_domain.hpp
@@ -88,8 +88,9 @@ class cell_t final {
 
     // ignore the scalar variable
     bool operator<(const cell_t& o) const {
-        if (_offset == o._offset)
+        if (_offset == o._offset) {
             return _size < o._size;
+        }
         return _offset < o._offset;
     }
 
@@ -213,13 +214,9 @@ class array_map_t {
     }
     bool operator==(const array_map_t& other) const = default;
 
-    offset_map_t& operator[](data_kind_t kind) {
-        return map[kind];
-    }
+    offset_map_t& operator[](data_kind_t kind) { return map[kind]; }
 
-    const offset_map_t& operator[](data_kind_t kind) const {
-        return map.at(kind);
-    }
+    const offset_map_t& operator[](data_kind_t kind) const { return map.at(kind); }
 
     void operator-=(const cell_t& c) {
         for (auto& [_, v] : map) {
@@ -308,8 +305,10 @@ class array_domain_t final {
 
     void set_to_top();
     void set_to_bottom();
-    [[nodiscard]] bool is_bottom() const;
-    [[nodiscard]] bool is_top() const;
+    [[nodiscard]]
+    bool is_bottom() const;
+    [[nodiscard]]
+    bool is_top() const;
 
     bool operator<=(const array_domain_t& other) const;
     bool operator==(const array_domain_t& other) const;
@@ -323,10 +322,12 @@ class array_domain_t final {
     array_domain_t narrow(const array_domain_t& other) const;
 
     friend std::ostream& operator<<(std::ostream& o, const array_domain_t& dom);
-    [[nodiscard]] string_invariant to_set() const;
+    [[nodiscard]]
+    string_invariant to_set() const;
 
     bool all_num(const NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub);
-    [[nodiscard]] int min_all_num_size(const NumAbsDomain& inv, variable_t offset) const;
+    [[nodiscard]]
+    int min_all_num_size(const NumAbsDomain& inv, variable_t offset) const;
 
     std::optional<linear_expression_t> load(NumAbsDomain& inv, data_kind_t kind, const linear_expression_t& i,
                                             int width);
@@ -349,8 +350,8 @@ class array_domain_t final {
     void initialize_numbers(int lb, int width);
 
     std::optional<std::pair<offset_t, unsigned>> split_and_find_var(NumAbsDomain& inv, data_kind_t kind,
-                                                                        const linear_expression_t& idx,
-                                                                        const linear_expression_t& elem_size);
+                                                                    const linear_expression_t& idx,
+                                                                    const linear_expression_t& elem_size);
     std::optional<std::pair<offset_t, unsigned>> kill_and_find_var(NumAbsDomain& inv, data_kind_t kind,
                                                                    const linear_expression_t& i,
                                                                    const linear_expression_t& elem_size);
diff --git a/src/crab/ebpf_domain.cpp b/src/crab/ebpf_domain.cpp
index 8b74978bc..6e0246d91 100644
--- a/src/crab/ebpf_domain.cpp
+++ b/src/crab/ebpf_domain.cpp
@@ -103,15 +103,18 @@ static std::vector<linear_constraint_t> assume_bit_cst_interval(const NumAbsDoma
 
     auto dst_interval = inv.eval_interval(dst_uvalue);
     std::optional<number_t> dst_n = dst_interval.singleton();
-    if (!dst_n || !dst_n.value().fits_cast_to_int64())
+    if (!dst_n || !dst_n.value().fits_cast_to_int64()) {
         return {};
+    }
 
     std::optional<number_t> src_n = src_interval.singleton();
-    if (!src_n || !src_n->fits_cast_to_int64())
+    if (!src_n || !src_n->fits_cast_to_int64()) {
         return {};
+    }
     uint64_t src_int_value = src_n.value().cast_to_uint64();
-    if (!is64)
+    if (!is64) {
         src_int_value = (uint32_t)src_int_value;
+    }
 
     bool result;
     switch (op) {
@@ -128,10 +131,11 @@ static std::vector<linear_constraint_t> assume_signed_64bit_eq(const NumAbsDomai
                                                                const linear_expression_t& right_svalue,
                                                                const linear_expression_t& right_uvalue) {
     using namespace crab::dsl_syntax;
-    if (right_interval <= crab::interval_t::nonnegative_int(true) && !right_interval.is_singleton())
+    if (right_interval <= crab::interval_t::nonnegative_int(true) && !right_interval.is_singleton()) {
         return {(left_svalue == right_svalue), (left_uvalue == right_uvalue), eq(left_svalue, left_uvalue)};
-    else
+    } else {
         return {(left_svalue == right_svalue), (left_uvalue == right_uvalue)};
+    }
 }
 
 static std::vector<linear_constraint_t> assume_signed_32bit_eq(const NumAbsDomain& inv, variable_t left_svalue,
@@ -426,10 +430,11 @@ static std::vector<linear_constraint_t> assume_signed_cst_interval(const NumAbsD
 
     if (op == Condition::Op::EQ) {
         // Handle svalue == right.
-        if (is64)
+        if (is64) {
             return assume_signed_64bit_eq(inv, left_svalue, left_uvalue, right_interval, right_svalue, right_uvalue);
-        else
+        } else {
             return assume_signed_32bit_eq(inv, left_svalue, left_uvalue, right_interval);
+        }
     }
 
     const bool is_lt = op == Condition::Op::SLT || op == Condition::Op::SLE;
@@ -455,20 +460,22 @@ static std::vector<linear_constraint_t> assume_signed_cst_interval(const NumAbsD
     }
 
     if (is64) {
-        if (is_lt)
+        if (is_lt) {
             return assume_signed_64bit_lt(inv, strict, left_svalue, left_uvalue, left_interval_positive,
                                           left_interval_negative, right_svalue, right_uvalue, right_interval);
-        else
+        } else {
             return assume_signed_64bit_gt(inv, strict, left_svalue, left_uvalue, left_interval_positive,
                                           left_interval_negative, right_svalue, right_uvalue, right_interval);
+        }
     } else {
         // 32-bit compare.
-        if (is_lt)
+        if (is_lt) {
             return assume_signed_32bit_lt(inv, strict, left_svalue, left_uvalue, left_interval_positive,
                                           left_interval_negative, right_svalue, right_uvalue, right_interval);
-        else
+        } else {
             return assume_signed_32bit_gt(inv, strict, left_svalue, left_uvalue, left_interval_positive,
                                           left_interval_negative, right_svalue, right_uvalue, right_interval);
+        }
     }
     return {};
 }
@@ -485,22 +492,24 @@ assume_unsigned_64bit_lt(const NumAbsDomain& inv, bool strict, variable_t left_s
     auto lllb = left_interval_low.truncate_to_uint(true).lb();
     if ((right_interval <= interval_t::nonnegative_int(true)) && (strict ? (lllb >= rub) : (lllb > rub))) {
         // The high interval is out of range.
-        if (auto lsubn = inv.eval_interval(left_svalue).ub().number())
+        if (auto lsubn = inv.eval_interval(left_svalue).ub().number()) {
             return {left_uvalue >= 0, ((strict) ? left_uvalue < right_uvalue : left_uvalue <= right_uvalue),
                     left_uvalue <= *lsubn, left_svalue >= 0};
-        else
+        } else {
             return {left_uvalue >= 0, ((strict) ? left_uvalue < right_uvalue : left_uvalue <= right_uvalue),
                     left_svalue >= 0};
+        }
     }
     auto lhlb = left_interval_high.truncate_to_uint(true).lb();
     if ((right_interval <= interval_t::unsigned_high(true)) && (strict ? (lhlb >= rub) : (lhlb > rub))) {
         // The high interval is out of range.
-        if (auto lsubn = inv.eval_interval(left_svalue).ub().number())
+        if (auto lsubn = inv.eval_interval(left_svalue).ub().number()) {
             return {left_uvalue >= 0, ((strict) ? left_uvalue < *rub.number() : left_uvalue <= *rub.number()),
                     left_uvalue <= *lsubn, left_svalue >= 0};
-        else
+        } else {
             return {left_uvalue >= 0, ((strict) ? left_uvalue < *rub.number() : left_uvalue <= *rub.number()),
                     left_svalue >= 0};
+        }
     }
     if (right_interval <= interval_t::signed_int(true)) {
         // Interval can be represented as both an svalue and a uvalue since it fits in [0, INT_MAX].
@@ -655,33 +664,37 @@ static std::vector<linear_constraint_t> assume_unsigned_cst_interval(const NumAb
     if (is_lt && (strict ? (lub < rlb) : (lub <= rlb))) {
         // Left unsigned interval is lower than right unsigned interval. We still add a
         // relationship for use when widening, such as is used in the prime conformance test.
-        if (is64)
+        if (is64) {
             return {strict ? left_uvalue < right_uvalue : left_uvalue <= right_uvalue};
-        else
+        } else {
             return {linear_constraint_t::TRUE()};
+        }
     } else if (!is_lt && (strict ? (llb > rub) : (llb >= rub))) {
         // Left unsigned interval is higher than right unsigned interval. We still add a
         // relationship for use when widening, such as is used in the prime conformance test.
-        if (is64)
+        if (is64) {
             return {strict ? left_uvalue > right_uvalue : left_uvalue >= right_uvalue};
-        else
+        } else {
             return {linear_constraint_t::TRUE()};
+        }
     }
 
     if (is64) {
-        if (is_lt)
+        if (is_lt) {
             return assume_unsigned_64bit_lt(inv, strict, left_svalue, left_uvalue, left_interval_low,
                                             left_interval_high, right_svalue, right_uvalue, right_interval);
-        else
+        } else {
             return assume_unsigned_64bit_gt(inv, strict, left_svalue, left_uvalue, left_interval_low,
                                             left_interval_high, right_svalue, right_uvalue, right_interval);
+        }
     } else {
-        if (is_lt)
+        if (is_lt) {
             return assume_unsigned_32bit_lt(inv, strict, left_svalue, left_uvalue, left_interval_low,
                                             left_interval_high, right_svalue, right_uvalue, right_interval);
-        else
+        } else {
             return assume_unsigned_32bit_gt(inv, strict, left_svalue, left_uvalue, left_interval_low,
                                             left_interval_high, right_svalue, right_uvalue, right_interval);
+        }
     }
 }
 
@@ -723,10 +736,11 @@ static std::vector<linear_constraint_t> assume_cst_reg(const NumAbsDomain& inv,
         switch (op) {
         case Op::EQ: {
             crab::interval_t src_interval = inv.eval_interval(src_svalue);
-            if (!src_interval.is_singleton() && (src_interval <= crab::interval_t::nonnegative_int(true)))
+            if (!src_interval.is_singleton() && (src_interval <= crab::interval_t::nonnegative_int(true))) {
                 return {eq(dst_svalue, src_svalue), eq(dst_uvalue, src_uvalue), eq(dst_svalue, dst_uvalue)};
-            else
+            } else {
                 return {eq(dst_svalue, src_svalue), eq(dst_uvalue, src_uvalue)};
+            }
         }
         case Op::NE: return {neq(dst_svalue, src_svalue)};
         case Op::SGE: return {dst_svalue >= src_svalue};
@@ -828,10 +842,11 @@ void ebpf_domain_t::TypeDomain::add_extra_invariant(NumAbsDomain& dst,
 
     // If type is contained in exactly one of dst or src,
     // we need to remember the value.
-    if (dst_has_type && !src_has_type)
+    if (dst_has_type && !src_has_type) {
         extra_invariants.emplace(v, dst.eval_interval(v));
-    else if (!dst_has_type && src_has_type)
+    } else if (!dst_has_type && src_has_type) {
         extra_invariants.emplace(v, src.eval_interval(v));
+    }
 }
 
 void ebpf_domain_t::TypeDomain::selectively_join_based_on_type(NumAbsDomain& dst, NumAbsDomain& src) const {
@@ -947,8 +962,9 @@ static const ebpf_domain_t constant_limits = ebpf_domain_t::calculate_constant_l
 
 ebpf_domain_t ebpf_domain_t::widen(const ebpf_domain_t& other, bool to_constants) {
     ebpf_domain_t res{m_inv.widen(other.m_inv), stack | other.stack};
-    if (to_constants)
+    if (to_constants) {
         return res & constant_limits;
+    }
     return res;
 }
 
@@ -1150,8 +1166,9 @@ static void assume(NumAbsDomain& inv, const linear_constraint_t& cst) { inv += c
 void ebpf_domain_t::assume(const linear_constraint_t& cst) { crab::assume(m_inv, cst); }
 
 void ebpf_domain_t::require(NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& s) {
-    if (check_require)
+    if (check_require) {
         check_require(inv, cst, s + " (" + this->current_assertion + ")");
+    }
 
     if (thread_local_options.assume_assertions) {
         // avoid redundant errors
@@ -1223,15 +1240,17 @@ void ebpf_domain_t::TypeDomain::havoc_type(NumAbsDomain& inv, const Reg& r) { in
 
 int ebpf_domain_t::TypeDomain::get_type(const NumAbsDomain& inv, const Reg& r) const {
     auto res = inv[reg_pack(r).type].singleton();
-    if (!res)
+    if (!res) {
         return T_UNINIT;
+    }
     return (int)*res;
 }
 
 int ebpf_domain_t::TypeDomain::get_type(const NumAbsDomain& inv, variable_t v) const {
     auto res = inv[v].singleton();
-    if (!res)
+    if (!res) {
         return T_UNINIT;
+    }
     return (int)*res;
 }
 
@@ -1240,15 +1259,17 @@ int ebpf_domain_t::TypeDomain::get_type(const NumAbsDomain& inv, const number_t&
 // Check whether a given type value is within the range of a given type variable's value.
 bool ebpf_domain_t::TypeDomain::has_type(const NumAbsDomain& inv, const Reg& r, type_encoding_t type) const {
     crab::interval_t interval = inv[reg_pack(r).type];
-    if (interval.is_top())
+    if (interval.is_top()) {
         return true;
+    }
     return (interval.lb().number().value_or(INT_MIN) <= type) && (interval.ub().number().value_or(INT_MAX) >= type);
 }
 
 bool ebpf_domain_t::TypeDomain::has_type(const NumAbsDomain& inv, variable_t v, type_encoding_t type) const {
     crab::interval_t interval = inv[v];
-    if (interval.is_top())
+    if (interval.is_top()) {
         return true;
+    }
     return (interval.lb().number().value_or(INT_MIN) <= type) && (interval.ub().number().value_or(INT_MAX) >= type);
 }
 
@@ -1260,8 +1281,9 @@ NumAbsDomain ebpf_domain_t::TypeDomain::join_over_types(
     const NumAbsDomain& inv, const Reg& reg,
     const std::function<void(NumAbsDomain&, type_encoding_t)>& transition) const {
     crab::interval_t types = inv.eval_interval(reg_pack(reg).type);
-    if (types.is_bottom())
+    if (types.is_bottom()) {
         return NumAbsDomain::bottom();
+    }
     if (types.is_top()) {
         NumAbsDomain res(inv);
         transition(res, static_cast<type_encoding_t>(T_UNINIT));
@@ -1399,11 +1421,12 @@ void ebpf_domain_t::check_access_packet(NumAbsDomain& inv, const linear_expressi
                                         std::optional<variable_t> packet_size) {
     using namespace crab::dsl_syntax;
     require(inv, lb >= variable_t::meta_offset(), "Lower bound must be at least meta_offset");
-    if (packet_size)
+    if (packet_size) {
         require(inv, ub <= *packet_size, "Upper bound must be at most packet_size");
-    else
+    } else {
         require(inv, ub <= MAX_PACKET_SIZE,
                 std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));
+    }
 }
 
 void ebpf_domain_t::check_access_shared(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
@@ -1423,14 +1446,17 @@ void ebpf_domain_t::operator()(const Assume& s) {
             m_inv = type_inv.join_over_types(m_inv, cond.left, [&](NumAbsDomain& inv, type_encoding_t type) {
                 if (type == T_NUM) {
                     for (const linear_constraint_t& cst :
-                         assume_cst_reg(m_inv, cond.op, cond.is64, dst.svalue, dst.uvalue, src.svalue, src.uvalue))
+                         assume_cst_reg(m_inv, cond.op, cond.is64, dst.svalue, dst.uvalue, src.svalue, src.uvalue)) {
                         inv += cst;
+                    }
                 } else {
                     // Either pointers to a singleton region,
                     // or an equality comparison on map descriptors/pointers to non-singleton locations
-                    if (auto dst_offset = get_type_offset_variable(cond.left, type))
-                        if (auto src_offset = get_type_offset_variable(src_reg, type))
+                    if (auto dst_offset = get_type_offset_variable(cond.left, type)) {
+                        if (auto src_offset = get_type_offset_variable(src_reg, type)) {
                             inv += assume_cst_offsets_reg(cond.op, cond.is64, dst_offset.value(), src_offset.value());
+                        }
+                    }
                 }
             });
         } else {
@@ -1441,8 +1467,9 @@ void ebpf_domain_t::operator()(const Assume& s) {
         }
     } else {
         int64_t imm = static_cast<int64_t>(std::get<Imm>(cond.right).v);
-        for (const linear_constraint_t& cst : assume_cst_imm(m_inv, cond.op, cond.is64, dst.svalue, dst.uvalue, imm))
+        for (const linear_constraint_t& cst : assume_cst_imm(m_inv, cond.op, cond.is64, dst.svalue, dst.uvalue, imm)) {
             assume(cst);
+        }
     }
 }
 
@@ -1568,15 +1595,17 @@ void ebpf_domain_t::operator()(const Comparable& s) {
 }
 
 void ebpf_domain_t::operator()(const Addable& s) {
-    if (!type_inv.implies_type(m_inv, type_is_pointer(reg_pack(s.ptr)), type_is_number(s.num)))
+    if (!type_inv.implies_type(m_inv, type_is_pointer(reg_pack(s.ptr)), type_is_number(s.num))) {
         require(m_inv, linear_constraint_t::FALSE(), "Only numbers can be added to pointers");
+    }
 }
 
 void ebpf_domain_t::operator()(const ValidDivisor& s) {
     using namespace crab::dsl_syntax;
     auto reg = reg_pack(s.reg);
-    if (!type_inv.implies_type(m_inv, type_is_pointer(reg), type_is_number(s.reg)))
+    if (!type_inv.implies_type(m_inv, type_is_pointer(reg), type_is_number(s.reg))) {
         require(m_inv, linear_constraint_t::FALSE(), "Only numbers can be used as divisors");
+    }
     if (!thread_local_options.allow_division_by_zero) {
         auto v = s.is_signed ? reg.svalue : reg.uvalue;
         require(m_inv, v != 0, "Possible division by zero");
@@ -1584,13 +1613,15 @@ void ebpf_domain_t::operator()(const ValidDivisor& s) {
 }
 
 void ebpf_domain_t::operator()(const ValidStore& s) {
-    if (!type_inv.implies_type(m_inv, type_is_not_stack(reg_pack(s.mem)), type_is_number(s.val)))
+    if (!type_inv.implies_type(m_inv, type_is_not_stack(reg_pack(s.mem)), type_is_number(s.val))) {
         require(m_inv, linear_constraint_t::FALSE(), "Only numbers can be stored to externally-visible regions");
+    }
 }
 
 void ebpf_domain_t::operator()(const TypeConstraint& s) {
-    if (!type_inv.is_in_group(m_inv, s.reg, s.types))
+    if (!type_inv.is_in_group(m_inv, s.reg, s.types)) {
         require(m_inv, linear_constraint_t::FALSE(), "Invalid type");
+    }
 }
 
 void ebpf_domain_t::operator()(const FuncConstraint& s) {
@@ -1628,8 +1659,9 @@ bool ebpf_domain_t::get_map_fd_range(const Reg& map_fd_reg, int32_t* start_fd, i
     const crab::interval_t& map_fd_interval = m_inv[reg_pack(map_fd_reg).map_fd];
     auto lb = map_fd_interval.lb().number();
     auto ub = map_fd_interval.ub().number();
-    if (!lb || !lb->fits_sint32() || !ub || !ub->fits_sint32())
+    if (!lb || !lb->fits_sint32() || !ub || !ub->fits_sint32()) {
         return false;
+    }
     *start_fd = (int32_t)lb.value();
     *end_fd = (int32_t)ub.value();
 
@@ -1641,18 +1673,21 @@ bool ebpf_domain_t::get_map_fd_range(const Reg& map_fd_reg, int32_t* start_fd, i
 // All maps in the range must have the same type for us to use it.
 std::optional<uint32_t> ebpf_domain_t::get_map_type(const Reg& map_fd_reg) const {
     int32_t start_fd, end_fd;
-    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd))
+    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {
         return std::optional<uint32_t>();
+    }
 
     std::optional<uint32_t> type;
     for (int32_t map_fd = start_fd; map_fd <= end_fd; map_fd++) {
         EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd);
-        if (map == nullptr)
+        if (map == nullptr) {
             return std::optional<uint32_t>();
-        if (!type.has_value())
+        }
+        if (!type.has_value()) {
             type = map->type;
-        else if (map->type != *type)
+        } else if (map->type != *type) {
             return std::optional<uint32_t>();
+        }
     }
     return type;
 }
@@ -1660,18 +1695,21 @@ std::optional<uint32_t> ebpf_domain_t::get_map_type(const Reg& map_fd_reg) const
 // All maps in the range must have the same inner map fd for us to use it.
 std::optional<uint32_t> ebpf_domain_t::get_map_inner_map_fd(const Reg& map_fd_reg) const {
     int start_fd, end_fd;
-    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd))
+    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {
         return {};
+    }
 
     std::optional<uint32_t> inner_map_fd;
     for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
         EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd);
-        if (map == nullptr)
+        if (map == nullptr) {
             return {};
-        if (!inner_map_fd.has_value())
+        }
+        if (!inner_map_fd.has_value()) {
             inner_map_fd = map->inner_map_fd;
-        else if (map->type != *inner_map_fd)
+        } else if (map->type != *inner_map_fd) {
             return {};
+        }
     }
     return inner_map_fd;
 }
@@ -1679,15 +1717,17 @@ std::optional<uint32_t> ebpf_domain_t::get_map_inner_map_fd(const Reg& map_fd_re
 // We can deal with a range of key sizes.
 crab::interval_t ebpf_domain_t::get_map_key_size(const Reg& map_fd_reg) const {
     int start_fd, end_fd;
-    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd))
+    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {
         return crab::interval_t::top();
+    }
 
     crab::interval_t result = crab::interval_t::bottom();
     for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
-        if (EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd))
+        if (EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd)) {
             result = result | crab::interval_t(number_t(map->key_size));
-        else
+        } else {
             return crab::interval_t::top();
+        }
     }
     return result;
 }
@@ -1695,15 +1735,17 @@ crab::interval_t ebpf_domain_t::get_map_key_size(const Reg& map_fd_reg) const {
 // We can deal with a range of value sizes.
 crab::interval_t ebpf_domain_t::get_map_value_size(const Reg& map_fd_reg) const {
     int start_fd, end_fd;
-    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd))
+    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {
         return crab::interval_t::top();
+    }
 
     crab::interval_t result = crab::interval_t::bottom();
     for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
-        if (EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd))
+        if (EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd)) {
             result = result | crab::interval_t(number_t(map->value_size));
-        else
+        } else {
             return crab::interval_t::top();
+        }
     }
     return result;
 }
@@ -1711,15 +1753,17 @@ crab::interval_t ebpf_domain_t::get_map_value_size(const Reg& map_fd_reg) const
 // We can deal with a range of max_entries values.
 crab::interval_t ebpf_domain_t::get_map_max_entries(const Reg& map_fd_reg) const {
     int start_fd, end_fd;
-    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd))
+    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {
         return crab::interval_t::top();
+    }
 
     crab::interval_t result = crab::interval_t::bottom();
     for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
-        if (EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd))
+        if (EbpfMapDescriptor* map = &global_program_info->platform->get_map_descriptor(map_fd)) {
             result = result | crab::interval_t(number_t(map->max_entries));
-        else
+        } else {
             return crab::interval_t::top();
+        }
     }
     return result;
 }
@@ -1771,10 +1815,11 @@ void ebpf_domain_t::operator()(const ValidMapKeyValue& s) {
                         variable_t key_value =
                             variable_t::cell_var(data_kind_t::svalues, (uint64_t)offset.value(), sizeof(uint32_t));
 
-                        if (auto max_entries = get_map_max_entries(s.map_fd_reg).lb().number())
+                        if (auto max_entries = get_map_max_entries(s.map_fd_reg).lb().number()) {
                             require(inv, key_value < *max_entries, "Array index overflow");
-                        else
+                        } else {
                             require(inv, linear_constraint_t::FALSE(), "Max entries is not finite");
+                        }
                         require(inv, key_value >= 0, "Array index underflow");
                     }
                 }
@@ -1872,8 +1917,9 @@ void ebpf_domain_t::operator()(const ValidAccess& s) {
                                          ? lb + std::get<Imm>(s.width).v
                                          : lb + reg_pack(std::get<Reg>(s.width)).svalue;
             check_access_shared(inv, lb, ub, reg.shared_region_size);
-            if (!is_comparison_check && !s.or_null)
+            if (!is_comparison_check && !s.or_null) {
                 require(inv, reg.svalue > 0, "Possible null access");
+            }
             // Shared memory is zero-initialized when created so is safe to read and write.
             break;
         }
@@ -1910,8 +1956,9 @@ void ebpf_domain_t::do_load_stack(NumAbsDomain& inv, const Reg& target_reg, cons
                                   const Reg& src_reg) {
     type_inv.assign_type(inv, target_reg, stack.load(inv, data_kind_t::types, addr, width));
     using namespace crab::dsl_syntax;
-    if (inv.entail(width <= reg_pack(src_reg).stack_numeric_size))
+    if (inv.entail(width <= reg_pack(src_reg).stack_numeric_size)) {
         type_inv.assign_type(inv, target_reg, T_NUM);
+    }
 
     const reg_pack_t& target = reg_pack(target_reg);
     if (width == 1 || width == 2 || width == 4 || width == 8) {
@@ -1923,12 +1970,15 @@ void ebpf_domain_t::do_load_stack(NumAbsDomain& inv, const Reg& target_reg, cons
         inv.assign(target.svalue, sresult);
         inv.assign(target.uvalue, uresult);
 
-        if (type_inv.has_type(inv, target.type, T_CTX))
+        if (type_inv.has_type(inv, target.type, T_CTX)) {
             inv.assign(target.ctx_offset, stack.load(inv, data_kind_t::ctx_offsets, addr, width));
-        if (type_inv.has_type(inv, target.type, T_MAP) || type_inv.has_type(inv, target.type, T_MAP_PROGRAMS))
+        }
+        if (type_inv.has_type(inv, target.type, T_MAP) || type_inv.has_type(inv, target.type, T_MAP_PROGRAMS)) {
             inv.assign(target.map_fd, stack.load(inv, data_kind_t::map_fds, addr, width));
-        if (type_inv.has_type(inv, target.type, T_PACKET))
+        }
+        if (type_inv.has_type(inv, target.type, T_PACKET)) {
             inv.assign(target.packet_offset, stack.load(inv, data_kind_t::packet_offsets, addr, width));
+        }
         if (type_inv.has_type(inv, target.type, T_SHARED)) {
             inv.assign(target.shared_offset, stack.load(inv, data_kind_t::shared_offsets, addr, width));
             inv.assign(target.shared_region_size, stack.load(inv, data_kind_t::shared_region_sizes, addr, width));
@@ -1937,15 +1987,17 @@ void ebpf_domain_t::do_load_stack(NumAbsDomain& inv, const Reg& target_reg, cons
             inv.assign(target.stack_offset, stack.load(inv, data_kind_t::stack_offsets, addr, width));
             inv.assign(target.stack_numeric_size, stack.load(inv, data_kind_t::stack_numeric_sizes, addr, width));
         }
-    } else
+    } else {
         havoc_register(inv, target_reg);
+    }
 }
 
 void ebpf_domain_t::do_load_ctx(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr_vague,
                                 int width) {
     using namespace crab::dsl_syntax;
-    if (inv.is_bottom())
+    if (inv.is_bottom()) {
         return;
+    }
 
     const ebpf_context_descriptor_t* desc = global_program_info->type.context_descriptor;
 
@@ -1964,10 +2016,11 @@ void ebpf_domain_t::do_load_ctx(NumAbsDomain& inv, const Reg& target_reg, const
     bool may_touch_ptr = interval[desc->data] || interval[desc->meta] || interval[desc->end];
 
     if (!maybe_addr) {
-        if (may_touch_ptr)
+        if (may_touch_ptr) {
             type_inv.havoc_type(inv, target_reg);
-        else
+        } else {
             type_inv.assign_type(inv, target_reg, T_NUM);
+        }
         return;
     }
 
@@ -1979,19 +2032,23 @@ void ebpf_domain_t::do_load_ctx(NumAbsDomain& inv, const Reg& target_reg, const
     // at runtime are actually 64-bit memory pointers.
     int offset_width = desc->end - desc->data;
     if (addr == desc->data) {
-        if (width == offset_width)
+        if (width == offset_width) {
             inv.assign(target.packet_offset, 0);
+        }
     } else if (addr == desc->end) {
-        if (width == offset_width)
+        if (width == offset_width) {
             inv.assign(target.packet_offset, variable_t::packet_size());
+        }
     } else if (addr == desc->meta) {
-        if (width == offset_width)
+        if (width == offset_width) {
             inv.assign(target.packet_offset, variable_t::meta_offset());
+        }
     } else {
-        if (may_touch_ptr)
+        if (may_touch_ptr) {
             type_inv.havoc_type(inv, target_reg);
-        else
+        } else {
             type_inv.assign_type(inv, target_reg, T_NUM);
+        }
         return;
     }
     if (width == offset_width) {
@@ -2003,8 +2060,9 @@ void ebpf_domain_t::do_load_ctx(NumAbsDomain& inv, const Reg& target_reg, const
 
 void ebpf_domain_t::do_load_packet_or_shared(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr,
                                              int width) {
-    if (inv.is_bottom())
+    if (inv.is_bottom()) {
         return;
+    }
     const reg_pack_t& target = reg_pack(target_reg);
 
     type_inv.assign_type(inv, target_reg, T_NUM);
@@ -2138,8 +2196,9 @@ void ebpf_domain_t::do_store_stack(NumAbsDomain& inv, const number_t& width, con
     auto updated_lb = m_inv.eval_interval(addr).lb();
     auto updated_ub = m_inv.eval_interval(addr).ub() + width;
     for (variable_t type_variable : variable_t::get_type_variables()) {
-        if (!type_inv.has_type(inv, type_variable, T_STACK))
+        if (!type_inv.has_type(inv, type_variable, T_STACK)) {
             continue;
+        }
         variable_t stack_offset_variable = variable_t::kind_var(data_kind_t::stack_offsets, type_variable);
         variable_t stack_numeric_size_variable = variable_t::kind_var(data_kind_t::stack_numeric_sizes, type_variable);
 
@@ -2154,8 +2213,9 @@ void ebpf_domain_t::do_store_stack(NumAbsDomain& inv, const number_t& width, con
 }
 
 void ebpf_domain_t::operator()(const Mem& b) {
-    if (m_inv.is_bottom())
+    if (m_inv.is_bottom()) {
         return;
+    }
     if (std::holds_alternative<Reg>(b.value)) {
         if (b.is_load) {
             do_load(b, std::get<Reg>(b.value));
@@ -2173,8 +2233,9 @@ void ebpf_domain_t::operator()(const Mem& b) {
 template <typename Type, typename SValue, typename UValue>
 void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue, UValue val_uvalue,
                                  const std::optional<reg_pack_t>& val_reg) {
-    if (m_inv.is_bottom())
+    if (m_inv.is_bottom()) {
         return;
+    }
     int width = b.access.width;
     number_t offset{b.access.offset};
     if (b.access.basereg.v == R10_STACK_POINTER) {
@@ -2195,8 +2256,7 @@ void ebpf_domain_t::do_mem_store(const Mem& b, Type val_type, SValue val_svalue,
 
 // Construct a Bin operation that does the main operation that a given Atomic operation does atomically.
 static Bin atomic_to_bin(const Atomic& a) {
-    Bin bin{
-        .dst = Reg{R11_ATOMIC_SCRATCH}, .v = a.valreg, .is64 = (a.access.width == sizeof(uint64_t)), .lddw = false};
+    Bin bin{.dst = Reg{R11_ATOMIC_SCRATCH}, .v = a.valreg, .is64 = (a.access.width == sizeof(uint64_t)), .lddw = false};
     switch (a.op) {
     case Atomic::Op::ADD: bin.op = Bin::Op::ADD; break;
     case Atomic::Op::OR: bin.op = Bin::Op::OR; break;
@@ -2210,8 +2270,9 @@ static Bin atomic_to_bin(const Atomic& a) {
 }
 
 void ebpf_domain_t::operator()(const Atomic& a) {
-    if (m_inv.is_bottom())
+    if (m_inv.is_bottom()) {
         return;
+    }
     if (!m_inv.entail(type_is_pointer(reg_pack(a.access.basereg))) ||
         !m_inv.entail(type_is_number(reg_pack(a.valreg)))) {
         return;
@@ -2219,10 +2280,11 @@ void ebpf_domain_t::operator()(const Atomic& a) {
     if (m_inv.entail(type_is_not_stack(reg_pack(a.access.basereg)))) {
         // Shared memory regions are volatile so we can just havoc
         // any register that will be updated.
-        if (a.op == Atomic::Op::CMPXCHG)
+        if (a.op == Atomic::Op::CMPXCHG) {
             havoc_register(m_inv, Reg{R0_RETURN_VALUE});
-        else if (a.fetch)
+        } else if (a.fetch) {
             havoc_register(m_inv, a.valreg);
+        }
         return;
     }
 
@@ -2260,8 +2322,9 @@ void ebpf_domain_t::operator()(const Atomic& a) {
 
 void ebpf_domain_t::operator()(const Call& call) {
     using namespace crab::dsl_syntax;
-    if (m_inv.is_bottom())
+    if (m_inv.is_bottom()) {
         return;
+    }
     std::optional<Reg> maybe_fd_reg{};
     for (ArgSingle param : call.singles) {
         switch (param.kind) {
@@ -2357,8 +2420,9 @@ void ebpf_domain_t::operator()(const Call& call) {
 
 void ebpf_domain_t::operator()(const Callx& callx) {
     using namespace crab::dsl_syntax;
-    if (m_inv.is_bottom())
+    if (m_inv.is_bottom()) {
         return;
+    }
 
     // Look up the helper function id.
     const reg_pack_t& reg = reg_pack(callx.func);
@@ -2411,13 +2475,15 @@ void ebpf_domain_t::assign_valid_ptr(const Reg& dst_reg, bool maybe_null) {
 void ebpf_domain_t::recompute_stack_numeric_size(NumAbsDomain& inv, variable_t type_variable) {
     variable_t stack_numeric_size_variable = variable_t::kind_var(data_kind_t::stack_numeric_sizes, type_variable);
 
-    if (!inv.eval_interval(stack_numeric_size_variable).is_top())
+    if (!inv.eval_interval(stack_numeric_size_variable).is_top()) {
         return;
+    }
 
     if (type_inv.has_type(inv, type_variable, T_STACK)) {
         int numeric_size = stack.min_all_num_size(inv, variable_t::kind_var(data_kind_t::stack_offsets, type_variable));
-        if (numeric_size > 0)
+        if (numeric_size > 0) {
             inv.assign(stack_numeric_size_variable, numeric_size);
+        }
     }
 }
 
@@ -2431,12 +2497,13 @@ void ebpf_domain_t::add(const Reg& reg, int imm, int finite_width) {
     add_overflow(dst.svalue, dst.uvalue, imm, finite_width);
     if (offset.has_value()) {
         add(offset.value(), imm);
-        if (imm > 0)
+        if (imm > 0) {
             // Since the start offset is increasing but
             // the end offset is not, the numeric size decreases.
             sub(dst.stack_numeric_size, imm);
-        else if (imm < 0)
+        } else if (imm < 0) {
             havoc(dst.stack_numeric_size);
+        }
         recompute_stack_numeric_size(m_inv, reg);
     }
 }
@@ -2638,13 +2705,15 @@ void ebpf_domain_t::operator()(const Bin& bin) {
             havoc_offsets(bin.dst);
             break;
         case Bin::Op::ADD:
-            if (imm == 0)
+            if (imm == 0) {
                 return;
+            }
             add(bin.dst, (int)imm, finite_width);
             break;
         case Bin::Op::SUB:
-            if (imm == 0)
+            if (imm == 0) {
                 return;
+            }
             add(bin.dst, (int)-imm, finite_width);
             break;
         case Bin::Op::MUL:
@@ -2708,11 +2777,13 @@ void ebpf_domain_t::operator()(const Bin& bin) {
                         if (dst_type == T_NUM && src_type != T_NUM) {
                             // num += ptr
                             type_inv.assign_type(inv, bin.dst, src_type);
-                            if (auto dst_offset = get_type_offset_variable(bin.dst, src_type))
+                            if (auto dst_offset = get_type_offset_variable(bin.dst, src_type)) {
                                 apply(inv, crab::arith_binop_t::ADD, dst_offset.value(), dst.svalue,
                                       get_type_offset_variable(src_reg, src_type).value());
-                            if (src_type == T_SHARED)
+                            }
+                            if (src_type == T_SHARED) {
                                 inv.assign(dst.shared_region_size, src.shared_region_size);
+                            }
                         } else if (dst_type != T_NUM && src_type == T_NUM) {
                             // ptr += num
                             type_inv.assign_type(inv, bin.dst, dst_type);
@@ -2725,9 +2796,10 @@ void ebpf_domain_t::operator()(const Bin& bin) {
                                     if (m_inv.intersect(src.svalue < 0)) {
                                         inv -= dst.stack_numeric_size;
                                         recompute_stack_numeric_size(inv, dst.type);
-                                    } else
+                                    } else {
                                         apply_signed(inv, crab::arith_binop_t::SUB, dst.stack_numeric_size,
                                                      dst.stack_numeric_size, dst.stack_numeric_size, src.svalue, 0);
+                                    }
                                 }
                             }
                         } else if (dst_type == T_NUM && src_type == T_NUM) {
@@ -2792,9 +2864,10 @@ void ebpf_domain_t::operator()(const Bin& bin) {
                             if (m_inv.intersect(src.svalue > 0)) {
                                 m_inv -= dst.stack_numeric_size;
                                 recompute_stack_numeric_size(m_inv, dst.type);
-                            } else
+                            } else {
                                 apply(m_inv, crab::arith_binop_t::ADD, dst.stack_numeric_size, dst.stack_numeric_size,
                                       src.svalue);
+                            }
                         }
                     }
                 }
@@ -2883,7 +2956,8 @@ void ebpf_domain_t::operator()(const Bin& bin) {
         case Bin::Op::MOVSX16:
         case Bin::Op::MOVSX32:
             // Keep relational information if operation is a no-op.
-            if ((dst.svalue == src.svalue) && (m_inv.eval_interval(dst.svalue) <= interval_t::signed_int(_movsx_bits(bin.op)))) {
+            if ((dst.svalue == src.svalue) &&
+                (m_inv.eval_interval(dst.svalue) <= interval_t::signed_int(_movsx_bits(bin.op)))) {
                 return;
             }
             if (m_inv.entail(type_is_number(src_reg))) {
@@ -3035,8 +3109,9 @@ void ebpf_domain_t::initialize_loop_counter(const label_t label) {
 
 bound_t ebpf_domain_t::get_loop_count_upper_bound() {
     crab::bound_t ub{number_t{0}};
-    for (variable_t counter : variable_t::get_loop_counters())
+    for (variable_t counter : variable_t::get_loop_counters()) {
         ub = std::max(ub, m_inv[counter].ub());
+    }
     return ub;
 }
 
diff --git a/src/crab/ebpf_domain.hpp b/src/crab/ebpf_domain.hpp
index 98f1b386c..be8155288 100644
--- a/src/crab/ebpf_domain.hpp
+++ b/src/crab/ebpf_domain.hpp
@@ -31,8 +31,10 @@ class ebpf_domain_t final {
     static ebpf_domain_t bottom();
     void set_to_top();
     void set_to_bottom();
-    [[nodiscard]] bool is_bottom() const;
-    [[nodiscard]] bool is_top() const;
+    [[nodiscard]]
+    bool is_bottom() const;
+    [[nodiscard]]
+    bool is_top() const;
     bool operator<=(const ebpf_domain_t& other);
     bool operator==(const ebpf_domain_t& other) const;
     void operator|=(ebpf_domain_t&& other);
@@ -83,6 +85,7 @@ class ebpf_domain_t final {
 
     void initialize_loop_counter(label_t label);
     static ebpf_domain_t calculate_constant_limits();
+
   private:
     // private generic domain functions
     void operator+=(const linear_constraint_t& cst);
@@ -153,15 +156,22 @@ class ebpf_domain_t final {
     void havoc_offsets(NumAbsDomain& inv, const Reg& reg);
 
     static std::optional<variable_t> get_type_offset_variable(const Reg& reg, int type);
-    [[nodiscard]] std::optional<variable_t> get_type_offset_variable(const Reg& reg, const NumAbsDomain& inv) const;
-    [[nodiscard]] std::optional<variable_t> get_type_offset_variable(const Reg& reg) const;
+    [[nodiscard]]
+    std::optional<variable_t> get_type_offset_variable(const Reg& reg, const NumAbsDomain& inv) const;
+    [[nodiscard]]
+    std::optional<variable_t> get_type_offset_variable(const Reg& reg) const;
 
     void scratch_caller_saved_registers();
-    [[nodiscard]] std::optional<uint32_t> get_map_type(const Reg& map_fd_reg) const;
-    [[nodiscard]] std::optional<uint32_t> get_map_inner_map_fd(const Reg& map_fd_reg) const;
-    [[nodiscard]] crab::interval_t get_map_key_size(const Reg& map_fd_reg) const;
-    [[nodiscard]] crab::interval_t get_map_value_size(const Reg& map_fd_reg) const;
-    [[nodiscard]] crab::interval_t get_map_max_entries(const Reg& map_fd_reg) const;
+    [[nodiscard]]
+    std::optional<uint32_t> get_map_type(const Reg& map_fd_reg) const;
+    [[nodiscard]]
+    std::optional<uint32_t> get_map_inner_map_fd(const Reg& map_fd_reg) const;
+    [[nodiscard]]
+    crab::interval_t get_map_key_size(const Reg& map_fd_reg) const;
+    [[nodiscard]]
+    crab::interval_t get_map_value_size(const Reg& map_fd_reg) const;
+    [[nodiscard]]
+    crab::interval_t get_map_max_entries(const Reg& map_fd_reg) const;
     void forget_packet_pointers();
     void havoc_register(NumAbsDomain& inv, const Reg& reg);
     void do_load_mapfd(const Reg& dst_reg, int mapfd, bool maybe_null);
@@ -226,30 +236,39 @@ class ebpf_domain_t final {
 
         void havoc_type(NumAbsDomain& inv, const Reg& r);
 
-        [[nodiscard]] int get_type(const NumAbsDomain& inv, variable_t v) const;
-        [[nodiscard]] int get_type(const NumAbsDomain& inv, const Reg& r) const;
-        [[nodiscard]] int get_type(const NumAbsDomain& inv, const number_t& t) const;
-
-        [[nodiscard]] bool has_type(const NumAbsDomain& inv, variable_t v, type_encoding_t type) const;
-        [[nodiscard]] bool has_type(const NumAbsDomain& inv, const Reg& r, type_encoding_t type) const;
-        [[nodiscard]] bool has_type(const NumAbsDomain& inv, const number_t& t, type_encoding_t type) const;
-
-        [[nodiscard]] bool same_type(const NumAbsDomain& inv, const Reg& a, const Reg& b) const;
-        [[nodiscard]] bool implies_type(const NumAbsDomain& inv, const linear_constraint_t& a,
-                                        const linear_constraint_t& b) const;
-
-        [[nodiscard]] NumAbsDomain
-        join_over_types(const NumAbsDomain& inv, const Reg& reg,
-                        const std::function<void(NumAbsDomain&, type_encoding_t)>& transition) const;
-        [[nodiscard]] 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;
+        [[nodiscard]]
+        int get_type(const NumAbsDomain& inv, variable_t v) const;
+        [[nodiscard]]
+        int get_type(const NumAbsDomain& inv, const Reg& r) const;
+        [[nodiscard]]
+        int get_type(const NumAbsDomain& inv, const number_t& t) const;
+
+        [[nodiscard]]
+        bool has_type(const NumAbsDomain& inv, variable_t v, type_encoding_t type) const;
+        [[nodiscard]]
+        bool has_type(const NumAbsDomain& inv, const Reg& r, type_encoding_t type) const;
+        [[nodiscard]]
+        bool has_type(const NumAbsDomain& inv, const number_t& t, type_encoding_t type) const;
+
+        [[nodiscard]]
+        bool same_type(const NumAbsDomain& inv, const Reg& a, const Reg& b) const;
+        [[nodiscard]]
+        bool implies_type(const NumAbsDomain& inv, const linear_constraint_t& a, const linear_constraint_t& b) const;
+
+        [[nodiscard]]
+        NumAbsDomain join_over_types(const NumAbsDomain& inv, const Reg& reg,
+                                     const std::function<void(NumAbsDomain&, type_encoding_t)>& transition) const;
+        [[nodiscard]]
+        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 add_extra_invariant(NumAbsDomain& dst, std::map<crab::variable_t, crab::interval_t>& extra_invariants,
                                  variable_t type_variable, type_encoding_t type, crab::data_kind_t kind,
                                  const NumAbsDomain& other) const;
 
-        [[nodiscard]] bool is_in_group(const NumAbsDomain& inv, const Reg& r, TypeGroup group) const;
+        [[nodiscard]]
+        bool is_in_group(const NumAbsDomain& inv, const Reg& r, TypeGroup group) const;
     };
 
     TypeDomain type_inv;
diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp
index 1f4ad9a93..58b2098a8 100644
--- a/src/crab_verifier.cpp
+++ b/src/crab_verifier.cpp
@@ -45,12 +45,14 @@ struct checks_db final {
         total_unreachable++;
     }
 
-    [[nodiscard]] int get_max_loop_count() const {
+    [[nodiscard]]
+    int get_max_loop_count() const {
         auto m = this->max_loop_count.number();
-        if (m && m->fits_sint32())
+        if (m && m->fits_sint32()) {
             return m->cast_to_sint32();
-        else
+        } else {
             return std::numeric_limits<int>::max();
+        }
     }
     checks_db() = default;
 };
@@ -63,8 +65,9 @@ static checks_db generate_report(cfg_t& cfg, crab::invariant_table_t& pre_invari
         ebpf_domain_t from_inv(pre_invariants.at(label));
         from_inv.set_require_check(
             [&m_db, label](auto& inv, const crab::linear_constraint_t& cst, const std::string& s) {
-                if (inv.is_bottom())
+                if (inv.is_bottom()) {
                     return true;
+                }
                 if (cst.is_contradiction()) {
                     m_db.add_warning(label, s);
                     return false;
@@ -102,8 +105,9 @@ static checks_db generate_report(cfg_t& cfg, crab::invariant_table_t& pre_invari
 static auto get_line_info(const InstructionSeq& insts) {
     std::map<int, btf_line_info_t> label_to_line_info;
     for (auto& [label, inst, line_info] : insts) {
-        if (line_info.has_value())
+        if (line_info.has_value()) {
             label_to_line_info.emplace(label.from, line_info.value());
+        }
     }
     return label_to_line_info;
 }
@@ -115,8 +119,9 @@ static void print_report(std::ostream& os, const checks_db& db, const Instructio
         for (const auto& msg : messages) {
             if (print_line_info) {
                 auto line_info = label_to_line_info.find(label.from);
-                if (line_info != label_to_line_info.end())
+                if (line_info != label_to_line_info.end()) {
                     os << line_info->second;
+                }
             }
             os << label << ": " << msg << "\n";
         }
@@ -164,8 +169,9 @@ static checks_db get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info,
 /// Returned value is true if the program passes verification.
 bool run_ebpf_analysis(std::ostream& s, cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options,
                        ebpf_verifier_stats_t* stats) {
-    if (options == nullptr)
+    if (options == nullptr) {
         options = &ebpf_verifier_default_options;
+    }
     checks_db report = get_ebpf_report(s, cfg, info, options);
     if (stats) {
         stats->total_unreachable = report.total_unreachable;
@@ -193,8 +199,9 @@ std::tuple<string_invariant, bool> ebpf_analyze_program_for_test(std::ostream& o
     global_program_info = info;
     assert(!entry_invariant.is_bottom());
     ebpf_domain_t entry_inv = ebpf_domain_t::from_constraints(entry_invariant.value(), options.setup_constraints);
-    if (entry_inv.is_bottom())
+    if (entry_inv.is_bottom()) {
         throw std::runtime_error("Entry invariant is inconsistent");
+    }
     cfg_t cfg = prepare_cfg(prog, info, options.simplify, false);
     auto [pre_invariants, post_invariants] = crab::run_forward_analyzer(cfg, std::move(entry_inv));
     checks_db report = get_analysis_report(std::cerr, cfg, pre_invariants, post_invariants);
@@ -208,8 +215,9 @@ std::tuple<string_invariant, bool> ebpf_analyze_program_for_test(std::ostream& o
 /// Returned value is true if the program passes verification.
 bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const program_info& info,
                          const ebpf_verifier_options_t* options, ebpf_verifier_stats_t* stats) {
-    if (options == nullptr)
+    if (options == nullptr) {
         options = &ebpf_verifier_default_options;
+    }
 
     // Convert the instruction sequence to a control-flow graph
     // in a "passive", non-deterministic form.

From c26d9a94ab840416f6b1f512ccc26d0bc56e8650 Mon Sep 17 00:00:00 2001
From: Elazar Gershuni <elazarg@gmail.com>
Date: Tue, 3 Sep 2024 18:11:03 +0300
Subject: [PATCH 3/3] remove include

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>
---
 src/crab/array_domain.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/crab/array_domain.cpp b/src/crab/array_domain.cpp
index c63af2422..7990e5da7 100644
--- a/src/crab/array_domain.cpp
+++ b/src/crab/array_domain.cpp
@@ -10,7 +10,6 @@
 #include "boost/endian/conversion.hpp"
 
 #include "crab/array_domain.hpp"
-#include "radix_tree/radix_tree.hpp"
 
 #include "asm_ostream.hpp"
 #include "config.hpp"