29279923487

Committed 12 Jul 2026 11:38AM UTC coverage: 86.649% (+0.3%) from 86.386%

Build # 29279923487

Build Type

push

github

Committed by

web-flow

Commit Message

Drive sample verification tests from the inventory; parallelize CI (#1195)

Full-program verification of the ebpf-samples corpus was 17 C++ files
generated by scripts/generate_verify_project_tests.py from
test-data/elf_inventory.json, then compiled into the test binary. The
generated files duplicated the inventory and could drift from it (there
was no check keeping them in sync), and the whole corpus ran in one
single-threaded Catch2 process.

Data-driven tests (dedup)
-------------------------
- Add src/test/test_verify_samples.cpp, which reads elf_inventory.json at
  runtime (via yaml-cpp; JSON is a subset of YAML) and registers one
  Catch2 DYNAMIC_SECTION per (object, section[, program]). Adding or
  retagging a sample is now a JSON edit: no code generation, no recompile.
- Delete the 17 generated test_verify_<project>.cpp files and
  scripts/generate_verify_project_tests.py. The inventory is the single
  source of truth. A coverage-guard test asserts the registered projects
  match the inventory exactly, so a new project cannot be left untested.
- Trim test_verify.hpp to the ELF-parse cache and the VerifyIssueKind
  taxonomy the driver and the multithreading test still use.

  Catch2's [!shouldfail] is a compile-time per-TEST_CASE tag and cannot be
  applied per data-driven entry, so an expected_failure (a safe program
  the verifier is currently too imprecise to accept) is asserted as
  *still rejected* -- an xfail/golden marker. A verifier improvement that
  starts accepting it fails the case, prompting an inventory update; a
  regression on a passing program fails it too.

Parallel CI (ctest)
-------------------
- Register ctest entries: one per project (sharded by tag) plus a "unit"
  entry for everything else. The shard list is derived from the inventory
  via string(JSON), so it cannot drift from the corpus.
- CI runs `ctest -j` instead of a single `bin/tests` process. Locally, a
  full run drops from ~104s to ~42s on 16 cores (bounded by t... (continued)

Coverage Stats

9313 of 10748 relevant lines covered (86.65%)

6391896.2 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

85.34

/src/crab/array_domain.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: Apache-2.0

#include <algorithm>
#include <optional>
#include <set>
#include <unordered_map>
#include <utility>
#include <vector>

#include "boost/endian/conversion.hpp"
#include <gsl/narrow>
#include <map>

#include "arith/dsl_syntax.hpp"
#include "config.hpp"
#include "crab/array_domain.hpp"
#include "crab/var_registry.hpp"
#include "crab_utils/num_safety.hpp"

#include <ranges>

namespace prevail {

using Index = uint64_t;

using offset_t = Index;

// 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.
struct Cell final {
    offset_t offset{};
    unsigned size{};

    bool operator==(const Cell&) const = default;
    auto operator<=>(const Cell&) const = default;

    // Return true if [o, o + sz) definitely overlaps with the cell.
    // Offsets are bounded by total_stack_size, so wraparound cannot occur.
    [[nodiscard]]
    bool overlap(const offset_t o, const unsigned sz) const {
        assert(sz > 0 && "overlap query with zero width");
        return offset < o + sz && o < offset + size;
    }
};

static Interval cell_to_interval(const offset_t o, const unsigned size) {
    const Number lb{gsl::narrow<int>(o)};
    return {lb, lb + size - 1};
}

// Return true if [symb_lb, symb_ub] may overlap with the cell,
// where symb_lb and symb_ub are not constant expressions.
static bool symbolic_overlap(const Cell& c, const Interval& range) {
    return !(cell_to_interval(c.offset, c.size) & range).is_bottom();
}

std::ostream& operator<<(std::ostream& o, const Cell& c) { return o << "cell(" << c.offset << "," << c.size << ")"; }

static Variable cell_var(const DataKind kind, const Cell& c) {
    return variable_registry.cell_var(kind, c.offset, c.size);
}

// Map offsets to cells.
// std::map/std::set are used deliberately: empirically, the median collection holds ~3 cells,
// overlap queries hit <5% of the time, and the entire offset map is <1% of verifier runtime.
// At these sizes, specialized data structures (patricia tries, flat sorted vectors) show no
// macro-level improvement while adding complexity or external dependencies.
class offset_map_t final {
    friend class ArrayDomain;
    friend class StackCellRegistry;

    using cell_set_t = std::set<Cell>;

    using map_t = std::map<offset_t, cell_set_t>;

    map_t _map;

    void remove_cell(const Cell& c);

    void insert_cell(const Cell& c);

    [[nodiscard]]
    std::optional<Cell> get_cell(offset_t o, unsigned size);

    Cell mk_cell(offset_t o, unsigned size);

  public:
    offset_map_t() = default;

    [[nodiscard]]
    std::size_t size() const {
        return _map.size();
    }

    void operator-=(const Cell& c) { remove_cell(c); }

    void operator-=(const std::vector<Cell>& cells) {
        for (const auto& c : cells) {
            this->operator-=(c);
        }
    }

    // Return in out all cells that might overlap with (o, size).
    std::vector<Cell> get_overlap_cells(offset_t o, unsigned size);

    [[nodiscard]]
    std::vector<Cell> get_overlap_cells_symbolic_offset(const Interval& range);

    friend std::ostream& operator<<(std::ostream& o, offset_map_t& m);
};

void offset_map_t::remove_cell(const Cell& c) {
    const offset_t key = c.offset;
    if (const auto it = _map.find(key); it != _map.end()) {
        it->second.erase(c);
        if (it->second.empty()) {
            _map.erase(it);
        }
    }
}

[[nodiscard]]
std::vector<Cell> offset_map_t::get_overlap_cells_symbolic_offset(const Interval& range) {
    std::vector<Cell> out;
    for (const auto& o_cells : _map | std::views::values) {
        // 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.
        if (!o_cells.empty()) {
            // Cells are sorted by (offset, size); last element has the largest size.
            const Cell& largest_cell = *o_cells.rbegin();
            if (symbolic_overlap(largest_cell, range)) {
                for (const auto& c : o_cells) {
                    out.push_back(c);
                }
            }
        }
    }
    return out;
}

void offset_map_t::insert_cell(const Cell& c) { _map[c.offset].insert(c); }

std::optional<Cell> offset_map_t::get_cell(const offset_t o, const unsigned size) {
    if (const auto it = _map.find(o); it != _map.end()) {
        if (const auto cit = it->second.find(Cell(o, size)); cit != it->second.end()) {
            return *cit;
        }
    }
    return {};
}

Cell offset_map_t::mk_cell(const offset_t o, const unsigned size) {
    // TODO: check array is the array associated to this offset map

    if (const auto maybe_c = get_cell(o, size)) {
        return *maybe_c;
    }
    // create a new scalar variable for representing the contents
    // of bytes array[o,o+1,..., o+size-1]
    const Cell c(o, size);
    insert_cell(c);
    return c;
}

// Return all cells that might overlap with (o, size).
std::vector<Cell> offset_map_t::get_overlap_cells(const offset_t o, const unsigned size) {
    std::vector<Cell> out;
    const Cell query_cell(o, size);

    // Search backwards: cells at offsets <= o that might extend into [o, o+size).
    // We cannot break early: a bucket with small cells may not overlap while an
    // earlier bucket with larger cells does (e.g., Cell(48,8) overlaps [54,56)
    // but Cell(50,2) does not). The map is tiny (~3 entries) so this is fine.
    for (auto it = _map.upper_bound(o); it != _map.begin();) {
        --it;
        for (const Cell& x : it->second) {
            if (x.overlap(o, size) && x != query_cell) {
                out.push_back(x);
            }
        }
    }

    // Search forwards: cells at offsets > o that start within [o, o+size).
    // Early break is safe here: if no cell at offset k overlaps, then k >= o + size,
    // and all subsequent offsets are even larger, so they cannot overlap either.
    // No duplicates: backward and forward scans visit disjoint key ranges.
    for (auto it = _map.upper_bound(o); it != _map.end(); ++it) {
        bool any_overlap = false;
        for (const Cell& x : it->second) {
            if (x.overlap(o, size)) {
                out.push_back(x);
                any_overlap = true;
            }
        }
        if (!any_overlap) {
            break;
        }
    }

    return out;
}

// Per-domain registry of the stack cells `ArrayDomain` is currently tracking,
// keyed by DataKind. Owned by `ArrayDomain`; copied/merged alongside the domain.
class StackCellRegistry final {
    std::unordered_map<DataKind, offset_map_t> _maps;

  public:
    offset_map_t& get(const DataKind kind) { return _maps[kind]; }

    void merge_from(const StackCellRegistry& other) {
        if (this == &other) {
            return;
        }
        for (const auto& [kind, omap] : other._maps) {
            offset_map_t& dst = _maps[kind];
            for (const auto& [_off, cell_set] : omap._map) {
                for (const Cell& c : cell_set) {
                    dst.insert_cell(c);
                }
            }
        }
    }
};

std::shared_ptr<StackCellRegistry> make_stack_cell_registry() { return std::make_shared<StackCellRegistry>(); }

void ArrayDomain::initialize_numbers(const int lb, const int width) {
    num_bytes.reset(lb, width);
    cells_.get_mutable().get(DataKind::svalues).mk_cell(offset_t{gsl::narrow_cast<Index>(lb)}, width);
}

std::ostream& operator<<(std::ostream& o, offset_map_t& m) {
    if (m._map.empty()) {
        o << "empty";
    } else {
        for (const auto& cells : m._map | std::views::values) {
            o << "{";
            for (auto cit = cells.begin(), cet = cells.end(); cit != cet;) {
                o << *cit;
                ++cit;
                if (cit != cet) {
                    o << ",";
                }
            }
            o << "}\n";
        }
    }
    return o;
}

// Create a new cell that is a subset of an existing cell.
void ArrayDomain::split_cell(NumAbsDomain& inv, const DataKind kind, const int cell_start_index, const unsigned int len,
                             const bool big_endian) {
    assert(kind == DataKind::svalues || kind == DataKind::uvalues);

    // Get the values from the indicated stack range.
    const std::optional<LinearExpression> svalue =
        load(inv, DataKind::svalues, Interval{cell_start_index}, len, big_endian);
    const std::optional<LinearExpression> uvalue =
        load(inv, DataKind::uvalues, Interval{cell_start_index}, len, big_endian);

    // Create a new cell for that range.
    offset_map_t& offset_map = cells_.get_mutable().get(kind);
    const Cell new_cell = offset_map.mk_cell(offset_t{gsl::narrow_cast<Index>(cell_start_index)}, len);
    inv.assign(cell_var(DataKind::svalues, new_cell), svalue);
    inv.assign(cell_var(DataKind::uvalues, new_cell), uvalue);
}

// Prepare to havoc bytes in the middle of a cell by potentially splitting the cell if it is numeric,
// into the part to the left of the havoced portion, and the part to the right of the havoced portion.
void ArrayDomain::split_number_var(NumAbsDomain& inv, const DataKind kind, const Interval& ii,
                                   const Interval& elem_size, const bool big_endian) {
    assert(kind == DataKind::svalues || kind == DataKind::uvalues);
    offset_map_t& offset_map = cells_.get_mutable().get(kind);
    const std::optional<Number> n = ii.singleton();
    if (!n) {
        // We can only split a singleton offset.
        return;
    }
    const std::optional<Number> n_bytes = elem_size.singleton();
    if (!n_bytes) {
        // We can only split a singleton size.
        return;
    }
    const auto size = n_bytes->narrow<unsigned int>();
    const offset_t o(n->narrow<Index>());

    const std::vector<Cell> overlaps = offset_map.get_overlap_cells(o, size);
    for (const Cell& c : overlaps) {
        const auto [cell_start_index, cell_end_index] = cell_to_interval(c.offset, c.size).pair<int>();
        if (!this->num_bytes.all_num(cell_start_index, cell_end_index + 1) ||
            cell_end_index + 1UL < cell_start_index + sizeof(int64_t)) {
            // We can only split numeric cells of size 8 or less.
            continue;
        }

        if (!inv.eval_interval(cell_var(kind, c)).is_singleton()) {
            // We can only split cells with a singleton value.
            continue;
        }
        if (gsl::narrow_cast<Index>(cell_start_index) < o) {
            // Use the bytes to the left of the specified range.
            split_cell(inv, kind, cell_start_index, gsl::narrow<unsigned int>(o - cell_start_index), big_endian);
        }
        if (o + size < cell_end_index + 1UL) {
            // Use the bytes to the right of the specified range.
            split_cell(inv, kind, gsl::narrow<int>(o + size),
                       gsl::narrow<unsigned int>(cell_end_index - (o + size - 1)), big_endian);
        }
    }
}

// Find overlapping cells for the given index range and kill (havoc + remove) them.
// Returns the exact offset and size if the index and element size are both constant.
template <typename HavocFn>
static std::optional<std::pair<offset_t, unsigned>> kill_and_find_var(StackCellRegistry& cells,
                                                                      const HavocFn& havoc_var, const DataKind kind,
                                                                      const Interval& ii, const Interval& elem_size) {
    std::optional<std::pair<offset_t, unsigned>> res;

    offset_map_t& offset_map = cells.get(kind);
    std::vector<Cell> overlaps;
    if (const std::optional<Number> n = ii.singleton()) {
        if (const auto n_bytes = elem_size.singleton()) {
            auto size = n_bytes->narrow<unsigned int>();
            // -- Constant index: kill overlapping cells
            offset_t o(n->narrow<Index>());
            overlaps = offset_map.get_overlap_cells(o, size);
            res = std::make_pair(o, size);
        }
    }
    if (!res) {
        // -- Non-constant index: kill overlapping cells
        overlaps = offset_map.get_overlap_cells_symbolic_offset(ii | (ii + elem_size));
    }
    if (!overlaps.empty()) {
        // Forget the scalars from the relevant domain
        for (const auto& c : overlaps) {
            havoc_var(cell_var(kind, c));

            // Forget signed and unsigned values together.
            if (kind == DataKind::svalues) {
                havoc_var(cell_var(DataKind::uvalues, c));
            } else if (kind == DataKind::uvalues) {
                havoc_var(cell_var(DataKind::svalues, c));
            }
        }
        // Remove the cells. If needed again they will be re-created.
        offset_map -= overlaps;
    }
    return res;
}
static std::optional<std::tuple<int, int>> as_numbytes_range(const Interval& range, const int stack_size) {
    const Interval bounded_range = Interval{0, stack_size} & range;
    if (bounded_range.is_bottom()) {
        return {};
    }
    const auto bounds = bounded_range.pair<int>();
    const auto [lb, ub] = bounds;
    if (lb >= ub) {
        return {};
    }
    return bounds;
}

static std::optional<std::tuple<int, int>> as_numbytes_range(const Interval& index, const Interval& width,
                                                             const int stack_size) {
    const Interval range = index | (index + width);
    return as_numbytes_range(range, stack_size);
}

bool ArrayDomain::all_num_lb_ub(const Interval& lb, const Interval& ub) const {
    const auto range = as_numbytes_range(lb | ub, total_stack_size());
    if (!range.has_value()) {
        return false;
    }
    const auto [min_lb, max_ub] = *range;
    assert(min_lb < max_ub);
    return this->num_bytes.all_num(min_lb, max_ub);
}

bool ArrayDomain::all_num_width(const Interval& index, const Interval& width) const {
    const auto range = as_numbytes_range(index, width, total_stack_size());
    if (!range.has_value()) {
        return false;
    }
    const auto [min_lb, max_ub] = *range;
    assert(min_lb < max_ub);
    return this->num_bytes.all_num(min_lb, max_ub);
}

// Get the number of bytes, starting at offset, that are known to be numbers.
int ArrayDomain::min_all_num_size(const NumAbsDomain& inv, const Variable offset) const {
    const auto min_lb = inv.eval_interval(offset).lb().number();
    const auto max_ub = inv.eval_interval(offset).ub().number();
    if (!min_lb || !max_ub || !min_lb->fits<int32_t>() || !max_ub->fits<int32_t>()) {
        return 0;
    }
    const auto lb = min_lb->narrow<int>();
    const auto ub = max_ub->narrow<int>();
    return std::max(0, this->num_bytes.all_num_width(lb) - (ub - lb));
}

// Get one byte of a value.
std::optional<uint8_t> get_value_byte(const NumAbsDomain& inv, const offset_t o, const int width,
                                      const bool big_endian) {
    const Variable v = variable_registry.cell_var(DataKind::svalues, (o / width) * width, width);
    const std::optional<Number> t = inv.eval_interval(v).singleton();
    if (!t) {
        return {};
    }
    Index n = t->cast_to<Index>();

    // Convert value to bytes of the appropriate endian-ness.
    switch (width) {
    case sizeof(uint8_t): break;
    case sizeof(uint16_t):
        if (big_endian) {
            n = boost::endian::native_to_big<uint16_t>(n);
        } else {
            n = boost::endian::native_to_little<uint16_t>(n);
        }
        break;
    case sizeof(uint32_t):
        if (big_endian) {
            n = boost::endian::native_to_big<uint32_t>(n);
        } else {
            n = boost::endian::native_to_little<uint32_t>(n);
        }
        break;
    case sizeof(Index):
        if (big_endian) {
            n = boost::endian::native_to_big<Index>(n);
        } else {
            n = boost::endian::native_to_little<Index>(n);
        }
        break;
    default: CRAB_ERROR("Unexpected width ", width);
    }
    const auto bytes = reinterpret_cast<uint8_t*>(&n);
    return bytes[o % width];
}

std::optional<LinearExpression> ArrayDomain::load(const NumAbsDomain& inv, const DataKind kind, const Interval& i,
                                                  const int width, const bool big_endian) {
    if (const std::optional<Number> n = i.singleton()) {
        offset_map_t& offset_map = cells_.get_mutable().get(kind);
        const int64_t k = n->narrow<int64_t>();
        const offset_t o(k);
        const unsigned size = to_unsigned(width);
        if (const auto cell = offset_map.get_cell(o, size)) {
            return cell_var(kind, *cell);
        }
        if (kind == DataKind::svalues || kind == DataKind::uvalues) {
            // Copy bytes into result_buffer, taking into account that the
            // bytes might be in different stack variables and might be unaligned.
            uint8_t result_buffer[8];
            bool found = true;
            for (unsigned int index = 0; index < size; index++) {
                const offset_t byte_offset{o + index};
                std::optional<uint8_t> b = get_value_byte(inv, byte_offset, 8, big_endian);
                if (!b) {
                    b = get_value_byte(inv, byte_offset, 4, big_endian);
                    if (!b) {
                        b = get_value_byte(inv, byte_offset, 2, big_endian);
                        if (!b) {
                            b = get_value_byte(inv, byte_offset, 1, big_endian);
                        }
                    }
                }
                if (b) {
                    result_buffer[index] = *b;
                } else {
                    found = false;
                    break;
                }
            }
            if (found) {
                // We have an aligned result in result_buffer so we can now
                // convert to an integer.
                if (size == 1) {
                    return *result_buffer;
                }
                if (size == 2) {
                    uint16_t b = *reinterpret_cast<uint16_t*>(result_buffer);
                    if (big_endian) {
                        b = boost::endian::native_to_big<uint16_t>(b);
                    } else {
                        b = boost::endian::native_to_little<uint16_t>(b);
                    }
                    return b;
                }
                if (size == 4) {
                    uint32_t b = *reinterpret_cast<uint32_t*>(result_buffer);
                    if (big_endian) {
                        b = boost::endian::native_to_big<uint32_t>(b);
                    } else {
                        b = boost::endian::native_to_little<uint32_t>(b);
                    }
                    return b;
                }
                if (size == 8) {
                    Index b = *reinterpret_cast<Index*>(result_buffer);
                    if (big_endian) {
                        b = boost::endian::native_to_big<Index>(b);
                    } else {
                        b = boost::endian::native_to_little<Index>(b);
                    }
                    return kind == DataKind::uvalues ? Number(b) : Number(to_signed(b));
                }
            }
        }

        const std::vector<Cell> overlaps = offset_map.get_overlap_cells(o, size);
        if (overlaps.empty()) {
            const Cell c = offset_map.mk_cell(o, size);
            // Here it's ok to do assignment (instead of expand) because c is not a summarized variable.
            // Otherwise, it would be unsound.
            return cell_var(kind, c);
        }
        CRAB_WARN("Ignored read from cell ", kind, "[", o, "...", o + size - 1, "]", " because it overlaps with ",
                  overlaps.size(), " cells");
        /*
            TODO: we can apply here "Value Recomposition" a la Mine'06 (https://arxiv.org/pdf/cs/0703074.pdf)
                to construct values of some type from a sequence of bytes.
                It can be endian-independent but it would more precise if we choose between little- and big-endian.
        */
    } else {
        // TODO: we can be more precise here
        CRAB_WARN("array expansion: ignored array load because of non-constant array index ", i);
    }
    return {};
}

std::optional<LinearExpression> ArrayDomain::load_type(const Interval& i, const int width) {
    if (const std::optional<Number> n = i.singleton()) {
        offset_map_t& offset_map = cells_.get_mutable().get(DataKind::types);
        const int64_t k = n->narrow<int64_t>();
        auto [only_num, only_non_num] = num_bytes.uniformity(k, width);
        if (only_num) {
            return T_NUM;
        }
        if (!only_non_num || width != 8) {
            return {};
        }
        const offset_t o(k);
        const unsigned size = to_unsigned(width);
        if (const auto cell = offset_map.get_cell(o, size)) {
            return cell_var(DataKind::types, *cell);
        }
        const std::vector<Cell> overlaps = offset_map.get_overlap_cells(o, size);
        if (overlaps.empty()) {
            const Cell c = offset_map.mk_cell(o, size);
            // Here it's ok to do assignment (instead of expand) because c is not a summarized variable.
            // Otherwise, it would be unsound.
            return cell_var(DataKind::types, c);
        }
        CRAB_WARN("Ignored read from cell ", DataKind::types, "[", o, "...", o + size - 1, "]",
                  " because it overlaps with ", overlaps.size(), " cells");
        /*
            TODO: we can apply here "Value Recomposition" a la Mine'06 (https://arxiv.org/pdf/cs/0703074.pdf)
                to construct values of some type from a sequence of bytes.
                It can be endian-independent but it would more precise if we choose between little- and big-endian.
        */
    } else {
        // Check whether the kind is uniform across the entire interval.
        const auto lb = i.lb().number();
        const auto ub = i.ub().number();
        if (lb.has_value() && ub.has_value()) {
            const Number fullwidth = ub.value() - lb.value() + width;
            if (lb->fits<uint32_t>() && fullwidth.fits<uint32_t>()) {
                auto [only_num, only_non_num] =
                    num_bytes.uniformity(lb->narrow<uint32_t>(), fullwidth.narrow<uint32_t>());
                if (only_num) {
                    return T_NUM;
                }
            }
        }
    }
    return {};
}

// 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(ArrayDomain& array_domain, StackCellRegistry& cells, NumAbsDomain& inv, const DataKind kind,
                   const Interval& idx, const Interval& elem_size, const bool big_endian) {
    if (kind == DataKind::svalues || kind == DataKind::uvalues) {
        array_domain.split_number_var(inv, kind, idx, elem_size, big_endian);
    }
    return kill_and_find_var(cells, [&inv](const Variable v) { inv.havoc(v); }, kind, idx, elem_size);
}

std::optional<Variable> ArrayDomain::store(NumAbsDomain& inv, const DataKind kind, const Interval& idx,
                                           const Interval& elem_size, const bool big_endian) {
    if (auto maybe_cell = split_and_find_var(*this, cells_.get_mutable(), inv, kind, idx, elem_size, big_endian)) {
        // perform strong update
        auto [offset, size] = *maybe_cell;
        const Cell c = cells_.get_mutable().get(kind).mk_cell(offset, size);
        Variable v = cell_var(kind, c);
        return v;
    }
    return {};
}

std::optional<Variable> ArrayDomain::store_type(TypeDomain& inv, const Interval& idx, const Interval& width,
                                                const bool is_num) {
    constexpr auto kind = DataKind::types;
    if (auto maybe_cell = kill_and_find_var(
            cells_.get_mutable(), [&inv](const Variable v) { inv.havoc_type(v); }, kind, idx, width)) {
        // perform strong update
        auto [offset, size] = *maybe_cell;
        if (is_num) {
            num_bytes.reset(offset, size);
        } else {
            num_bytes.havoc(offset, size);
        }
        const Cell c = cells_.get_mutable().get(kind).mk_cell(offset, size);
        Variable v = cell_var(kind, c);
        return v;
    } else {
        using namespace dsl_syntax;
        // Weak update: cannot perform a strong update because the index is
        // not a singleton. Havoc the type cells in the range.
        const auto range = as_numbytes_range(idx, width, total_stack_size());
        if (!is_num && range.has_value()) {
            const auto [lb, ub] = *range;
            // A non-numeric value may overwrite previously numeric bytes,
            // so conservatively mark the range [lb, ub) as non-numeric. havoc's
            // second argument is a width, not an upper bound.
            num_bytes.havoc(lb, ub - lb);
        }
        // When is_num is true, the value being stored is numeric. Any byte
        // that gets written will still be numeric, and bytes not written
        // keep their existing status, so num_bytes is left unchanged.
    }
    return {};
}

void ArrayDomain::havoc(NumAbsDomain& inv, const DataKind kind, const Interval& idx, const Interval& elem_size,
                        const bool big_endian) {
    split_and_find_var(*this, cells_.get_mutable(), inv, kind, idx, elem_size, big_endian);
}

void ArrayDomain::havoc_type(TypeDomain& inv, const Interval& idx, const Interval& elem_size) {
    constexpr auto kind = DataKind::types;
    if (auto maybe_cell = kill_and_find_var(
            cells_.get_mutable(), [&inv](const Variable v) { inv.havoc_type(v); }, kind, idx, elem_size)) {
        auto [offset, size] = *maybe_cell;
        num_bytes.havoc(offset, size);
    }
}

void ArrayDomain::store_numbers(const Interval& _idx, const Interval& _width) {
    const std::optional<Number> idx_n = _idx.singleton();
    if (!idx_n) {
        CRAB_WARN("array expansion store range ignored because ", "lower bound is not constant");
        return;
    }

    const std::optional<Number> width = _width.singleton();
    if (!width) {
        CRAB_WARN("array expansion store range ignored because ", "upper bound is not constant");
        return;
    }

    if (*idx_n + *width > total_stack_size()) {
        CRAB_WARN("array expansion store range ignored because ", "the number of elements is larger than limit of ",
                  total_stack_size());
        return;
    }
    num_bytes.reset(idx_n->narrow<int>(), width->narrow<int>());
}

void ArrayDomain::set_to_top() { num_bytes.set_to_top(); }

bool ArrayDomain::is_top() const { return num_bytes.is_top(); }

StringInvariant ArrayDomain::to_set() const { return num_bytes.to_set(); }

bool ArrayDomain::operator<=(const ArrayDomain& other) const { return num_bytes <= other.num_bytes; }

bool ArrayDomain::operator==(const ArrayDomain& other) const { return num_bytes == other.num_bytes; }

void ArrayDomain::operator|=(const ArrayDomain& other) {
    num_bytes |= other.num_bytes;
    cells_.get_mutable().merge_from(*other.cells_);
}

void ArrayDomain::operator|=(ArrayDomain&& other) {
    num_bytes |= std::move(other.num_bytes);
    cells_.get_mutable().merge_from(*other.cells_);
}

// Lattice combinators build a fresh ArrayDomain whose cells map is the union of
// both sides' cells. Cell membership is purely advisory (it enables overlap
// detection and dedup of mk_cell calls); the underlying numeric domain's join
// determines abstract values, and it operates on globally-interned Variable
// names so two domains independently tracking the same cell agree on its name.
ArrayDomain ArrayDomain::operator|(const ArrayDomain& other) const {
    ArrayDomain res{num_bytes | other.num_bytes};
    res.cells_.get_mutable().merge_from(*cells_);
    res.cells_.get_mutable().merge_from(*other.cells_);
    return res;
}

ArrayDomain ArrayDomain::operator&(const ArrayDomain& other) const {
    ArrayDomain res{num_bytes & other.num_bytes};
    res.cells_.get_mutable().merge_from(*cells_);
    res.cells_.get_mutable().merge_from(*other.cells_);
    return res;
}

ArrayDomain ArrayDomain::widen(const ArrayDomain& other) const {
    ArrayDomain res{num_bytes | other.num_bytes};
    res.cells_.get_mutable().merge_from(*cells_);
    res.cells_.get_mutable().merge_from(*other.cells_);
    return res;
}

ArrayDomain ArrayDomain::narrow(const ArrayDomain& other) const {
    ArrayDomain res{num_bytes & other.num_bytes};
    res.cells_.get_mutable().merge_from(*cells_);
    res.cells_.get_mutable().merge_from(*other.cells_);
    return res;
}

std::ostream& operator<<(std::ostream& o, const ArrayDomain& dom) { return o << dom.num_bytes; }
} // namespace prevail

Alan-Jowett / ebpf-verifier / 29279923487

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous