30559636792

Committed 27 Jul 2026 07:29AM UTC coverage: 86.764% (+0.1%) from 86.649%

Build # 30559636792

Build Type

push

github

Committed by

elazarg

Commit Message

Fix 32-bit soundness holes that let unsafe programs pass verification

Two independent classes of ALU32/JMP32 unsoundness allowed a crafted program to
be accepted while performing an out-of-bounds stack access.

MOVSX: the no-op fast path returned early for `wX sN= wX`, skipping the
zero-extension applied at the end of the function. The verifier kept a
sign-extended 64-bit value where the CPU produces a zero-extended 32-bit one, so
`r1 = r10; r2 = -1; w2 s8= r2; r1 += r2` was analyzed as r10 - 1 while the CPU
computes r10 + 0xFFFFFFFF, and the resulting out-of-bounds store was proved
in-bounds. The verifier already contradicted itself here: with r1 = -1,
`w2 s8= r1` yielded 0xFFFFFFFF but `w2 s8= r2` yielded -1 for the same operation
and input. Guard the fast path with bin.is64; the 64-bit form remains a no-op.

32-bit compares: the helpers emitted constraints over the 64-bit svalue/uvalue
variables after testing only the truncated 32-bit views. When a register's
64-bit value falls outside the 32-bit range those views say nothing about how the
64-bit variables are ordered, so branches that concrete executions do take were
proved dead, and unsafe code on them was never checked. Test the 64-bit intervals
instead, falling back to the existing no-constraint case. Precision is unchanged
for registers holding genuine 32-bit values, since the comparison itself pins the
operand's sign in the branches that assert one.

assume_unsigned_32bit_lt already guarded every branch this way, which is why only
the >, >=, s<, s<=, s> and s>= paths were affected.

Also drop the interval parameters these helpers no longer read.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Coverage Stats

19 of 19 new or added lines in 2 files covered. (100.0%)

107 existing lines in 5 files now uncovered.

9328 of 10751 relevant lines covered (86.76%)

6280124.66 hits per line

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

85.16

/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);

    Cell mk_cell(offset_t o, unsigned size);

  public:
    offset_map_t() = default;

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

    [[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 || !n->fits<Index>()) {
        // We can only split a singleton offset. A negative offset is an out-of-bounds
        // access below the stack frame: there is no cell to split and narrowing it to
        // the unsigned cell-offset type would throw, so leave it for the checker.
        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;
    // A strong update requires an offset representable by the unsigned cell-offset
    // type. An out-of-range constant (in particular a negative offset) stays on the
    // weak path below: although the access starts outside the tracked stack, its
    // possible byte range may still overlap a tracked cell.
    if (const auto n = ii.singleton(); n && n->fits<Index>()) {
        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);
            // get_overlap_cells deliberately excludes the exact-match cell (o, size),
            // which is correct for loads (get_cell handles it separately) but wrong for
            // a kill: a pure-havoc caller (e.g. storing an uninitialized register over an
            // exact-match cell) must forget the stale value/type, so include it here.
            if (const auto exact = offset_map.get_cell(o, size)) {
                overlaps.push_back(*exact);
            }
            res = std::make_pair(o, size);
        }
    }
    if (!res) {
        // -- Non-constant index: kill overlapping cells
        // elem_size is a non-negative byte count (ValidSize enforces this for
        // dynamic helper widths), so ii + elem_size is the exclusive end.
        // symbolic_overlap expects an inclusive interval of byte offsets; subtract one
        // to avoid spuriously killing a cell that starts exactly at the end. This also
        // makes a negative constant offset safe without narrowing: [-8, -8] with width
        // 8 touches [-8, -1], while offset -4 with width 8 may touch [0, 3].
        overlaps = offset_map.get_overlap_cells_symbolic_offset(ii | (ii + elem_size - Interval{1}));
    }
    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 / 30559636792

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