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

78.43

/src/crab/interval.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: Apache-2.0
#include <algorithm>
#include <cassert>

#include "crab/interval.hpp"

namespace prevail {

// Unsigned division (udiv) operand-box adjustment. Only udiv relies on this;
// signed division (sdiv / operator/) divides the original corners directly,
// because truncated signed division is monotone per argument on a
// sign-consistent box.
static Interval make_dividend_when_both_nonzero(const Interval& dividend, const Interval& divisor) {
    if (dividend.ub() >= 0) {
        return dividend;
    }
    if (divisor.ub() < 0) {
        return dividend + divisor + Interval{1};
    }
    return dividend + Interval{1} - divisor;
}

static ExtendedNumber divide_bound_by_negative_singleton(const ExtendedNumber& bound, const Number& divisor) {
    assert(divisor < 0);
    return bound.is_infinite() ? -bound : bound / divisor;
}

Interval Interval::operator*(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    const auto [clb, cub] = std::minmax({
        _lb * x._lb,
        _lb * x._ub,
        _ub * x._lb,
        _ub * x._ub,
    });
    return Interval{clb, cub};
}

// Signed division. eBPF has no instruction for this.
Interval Interval::operator/(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto n = x.singleton()) {
        // Divisor is a singleton:
        //   the linear interval solver can perform many divisions where
        //   the divisor is a singleton interval. We optimize for this case.
        const Number c = *n;
        if (c == 1) {
            return *this;
        } else if (c > 0) {
            return Interval{_lb / c, _ub / c};
        } else if (c < 0) {
            return Interval{divide_bound_by_negative_singleton(_ub, c), divide_bound_by_negative_singleton(_lb, c)};
        } else {
            // The eBPF ISA defines division by 0 as resulting in 0.
            return Interval{0};
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        const Interval l{x._lb, -1};
        const Interval u{1, x._ub};
        return operator/(l) | operator/(u) | Interval{0};
    } else if (contains(0)) {
        // The dividend contains 0.
        const Interval l{_lb, -1};
        const Interval u{1, _ub};
        return (l / x) | (u / x) | Interval{0};
    } else {
        // Neither the dividend nor the divisor contains 0. eBPF signed division
        // truncates toward zero (matching Number::operator/), and truncated
        // division is monotone in each argument on a sign-consistent box, so the
        // extreme quotients are attained at the corners of the operand box.
        const auto [clb, cub] = std::minmax({
            _lb / x._lb,
            _lb / x._ub,
            _ub / x._lb,
            _ub / x._ub,
        });
        return Interval{clb, cub};
    }
}

// Signed division.
Interval Interval::sdiv(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto n = x.singleton()) {
        if (n->fits_cast_to<int64_t>()) {
            // Divisor is a singleton:
            //   the linear interval solver can perform many divisions where
            //   the divisor is a singleton interval. We optimize for this case.
            const Number c{n->cast_to<int64_t>()};
            if (c == 1) {
                return *this;
            } else if (c > 0) {
                return Interval{_lb / c, _ub / c};
            } else if (c < 0) {
                return Interval{divide_bound_by_negative_singleton(_ub, c), divide_bound_by_negative_singleton(_lb, c)};
            } else {
                // The eBPF ISA defines division by 0 as resulting in 0.
                return Interval{0};
            }
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        const Interval l{x._lb, -1};
        const Interval u{1, x._ub};
        return sdiv(l) | sdiv(u) | Interval{0};
    } else if (contains(0)) {
        // The dividend contains 0.
        const Interval l{_lb, -1};
        const Interval u{1, _ub};
        return l.sdiv(x) | u.sdiv(x) | Interval{0};
    } else {
        // Neither the dividend nor the divisor contains 0. eBPF signed division
        // truncates toward zero (matching Number::operator/), and truncated
        // division is monotone in each argument on a sign-consistent box, so the
        // extreme quotients are attained at the corners of the operand box.
        const auto [clb, cub] = std::minmax({
            _lb / x._lb,
            _lb / x._ub,
            _ub / x._lb,
            _ub / x._ub,
        });
        return Interval{clb, cub};
    }
}

// Unsigned division.
Interval Interval::udiv(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto n = x.singleton()) {
        if (n->fits_cast_to<int64_t>()) {
            // Divisor is a singleton:
            //   the linear interval solver can perform many divisions where
            //   the divisor is a singleton interval. We optimize for this case.
            const Number c{n->cast_to<uint64_t>()};
            if (c == 1) {
                return *this;
            } else if (c > 0) {
                return Interval{_lb.udiv(c), _ub.udiv(c)};
            } else {
                // The eBPF ISA defines division by 0 as resulting in 0.
                return Interval{0};
            }
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        const Interval l{x._lb, -1};
        const Interval u{1, x._ub};
        return udiv(l) | udiv(u) | Interval{0};
    }
    if (contains(0)) {
        // The dividend contains 0.
        const Interval l{_lb, -1};
        const Interval u{1, _ub};
        return l.udiv(x) | u.udiv(x) | Interval{0};
    }
    // Neither the dividend nor the divisor contains 0
    const Interval a = make_dividend_when_both_nonzero(*this, x);
    const auto [clb, cub] = std::minmax({
        a._lb.udiv(x._lb),
        a._lb.udiv(x._ub),
        a._ub.udiv(x._lb),
        a._ub.udiv(x._ub),
    });
    return Interval{clb, cub};
}

// Signed remainder (modulo).
Interval Interval::srem(const Interval& x) const {
    // note that the sign of the divisor does not matter

    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto dividend = singleton()) {
        if (const auto divisor = x.singleton()) {
            if (*divisor == 0) {
                return Interval{*dividend};
            }
            return Interval{*dividend % *divisor};
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        const Interval l{x._lb, -1};
        const Interval u{1, x._ub};
        return srem(l) | srem(u) | *this;
    }
    if (x.ub().is_finite() && x.lb().is_finite()) {
        auto [xlb, xub] = x.pair_number();
        const auto [min_divisor, max_divisor] = std::minmax({xlb.abs(), xub.abs()});

        if (ub() < min_divisor && -lb() < min_divisor) {
            // The modulo operation won't change the destination register.
            return *this;
        }

        if (lb() < 0) {
            if (ub() > 0) {
                return Interval{-(max_divisor - 1), max_divisor - 1};
            } else {
                return Interval{-(max_divisor - 1), 0};
            }
        }
        return Interval{0, max_divisor - 1};
    }
    // Divisor has infinite range, so result can be anything between the dividend and zero.
    return *this | Interval{0};
}

// Unsigned remainder (modulo).
Interval Interval::urem(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto dividend = singleton()) {
        if (const auto divisor = x.singleton()) {
            if (dividend->fits_cast_to<uint64_t>() && divisor->fits_cast_to<uint64_t>()) {
                // The BPF ISA defines modulo by 0 as resulting in the original value.
                if (*divisor == 0) {
                    return Interval{*dividend};
                }
                const uint64_t dividend_val = dividend->cast_to<uint64_t>();
                const uint64_t divisor_val = divisor->cast_to<uint64_t>();
                return Interval{dividend_val % divisor_val};
            }
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        const Interval l{x._lb, -1};
        const Interval u{1, x._ub};
        return urem(l) | urem(u) | *this;
    } else if (contains(0)) {
        // The dividend contains 0.
        const Interval l{_lb, -1};
        const Interval u{1, _ub};
        return l.urem(x) | u.urem(x) | *this;
    } else {
        // Neither the dividend nor the divisor contains 0
        if (x._lb.is_infinite() || x._ub.is_infinite()) {
            // Divisor is infinite. A "negative" dividend could result in anything except
            // a value between the upper bound and 0, so set to top.  A "positive" dividend
            // could result in anything between 0 and the dividend - 1.
            return _ub < 0 ? top() : (*this - Interval{1}) | Interval{0};
        } else if (_ub.is_finite() && _ub.number()->cast_to<uint64_t>() < x._lb.number()->cast_to<uint64_t>()) {
            // Dividend lower than divisor, so the dividend is the remainder.
            return *this;
        } else {
            const Number max_divisor{x._ub.number()->cast_to<uint64_t>()};
            return Interval{0, max_divisor - 1};
        }
    }
}

void Interval::mask_value(const int width) {
    // we assume never to have wider widths than 64
    if (width > 0 && width < 64) {
        *this = bitwise_and(Interval{(1ULL << width) - 1});
    }
}

void Interval::mask_shift_count(const int width) {
    if (width > 0) {
        *this = bitwise_and(Interval{width - 1});
    }
}

// Do a bitwise-AND between two uvalue intervals.
Interval Interval::bitwise_and(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }

    // Bitwise operations are defined over unsigned machine values.
    // If an interval temporarily carries a signed lower bound (e.g., after
    // relational joins before re-establishing uvalue>=0), convert it to the
    // corresponding 64-bit unsigned range conservatively.
    Interval left = *this;
    Interval right = x;
    if (!left.is_top() && left.lb() < 0) {
        left = left.zero_extend(64);
    }
    if (!right.is_top() && right.lb() < 0) {
        right = right.zero_extend(64);
    }
    assert(left.is_top() || left.lb() >= 0);
    assert(right.is_top() || right.lb() >= 0);

    if (left == Interval{0} || right == Interval{0}) {
        return Interval{0};
    }

    if (const auto right_singleton = right.singleton()) {
        if (const auto left_singleton = left.singleton()) {
            return Interval{*left_singleton & *right_singleton};
        }
        if (right_singleton == Number::max_uint(64)) {
            return left.truncate_to<uint64_t>();
        }
        if (right_singleton == Number::max_uint(32)) {
            return left.zero_extend(32);
        }
        if (right_singleton == Number::max_uint(16)) {
            return left.zero_extend(16);
        }
        if (right_singleton == Number::max_uint(8)) {
            return left.zero_extend(8);
        }
    }
    if (right.contains(std::numeric_limits<uint64_t>::max())) {
        return Interval{0, left.truncate_to<uint64_t>().ub()};
    } else if (!left.is_top() && !right.is_top()) {
        return Interval{0, std::min(left.ub(), right.ub())};
    } else if (!right.is_top()) {
        return Interval{0, right.ub()};
    } else if (!left.is_top()) {
        return Interval{0, left.ub()};
    } else {
        return top();
    }
}

Interval Interval::bitwise_or(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto left_op = singleton()) {
        if (const auto right_op = x.singleton()) {
            return Interval{*left_op | *right_op};
        }
    }
    if (lb() >= 0 && x.lb() >= 0) {
        if (const auto left_ub = ub().number()) {
            if (const auto right_ub = x.ub().number()) {
                return Interval{0, std::max(*left_ub, *right_ub).fill_ones()};
            }
        }
        return Interval{0, PLUS_INFINITY};
    }
    return top();
}

Interval Interval::bitwise_xor(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto left_op = singleton()) {
        if (const auto right_op = x.singleton()) {
            return Interval{*left_op ^ *right_op};
        }
    }
    return bitwise_or(x);
}

Interval Interval::shl(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto shift = x.singleton()) {
        const Number k = *shift;
        if (k < 0) {
            return top();
        }
        // Some crazy linux drivers generate shl instructions with huge shifts.
        // We limit the number of times the loop is run to avoid wasting too much time on it.
        if (k <= 128) {
            Number factor = 1;
            for (int i = 0; k > i; i++) {
                factor *= 2;
            }
            return this->operator*(Interval{factor});
        }
    }
    return top();
}

Interval Interval::ashr(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto shift = x.singleton()) {
        const Number k = *shift;
        if (k < 0) {
            return top();
        }
        // Some crazy linux drivers generate ashr instructions with huge shifts.
        // We limit the number of times the loop is run to avoid wasting too much time on it.
        if (k <= 128) {
            Number factor = 1;
            for (int i = 0; k > i; i++) {
                factor *= 2;
            }
            return this->operator/(Interval{factor});
        }
    }
    return top();
}

Interval Interval::lshr(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto shift = x.singleton()) {
        if (*shift > 0 && lb() >= 0 && ub().is_finite()) {
            const auto [lb, ub] = this->pair_number();
            return Interval{lb >> *shift, ub >> *shift};
        }
    }
    return top();
}

Interval Interval::sign_extend(const int width) const {
    if (width <= 0) {
        CRAB_ERROR("Invalid width ", width);
    }

    const Interval full_range = signed_int(width);
    if (size() < full_range.size()) {
        if (Interval extended{_lb.sign_extend(width), _ub.sign_extend(width)}) {
            // If the sign–extended endpoints are in order, no wrap occurred.
            return extended;
        }
    }
    // [0b0111..., 0b1000...] is in the original range, so the result is [0b1000..., 0b0111...] which is the full range.
    return full_range;
}

Interval Interval::zero_extend(const int width) const {
    if (width <= 0) {
        CRAB_ERROR("Invalid width ", width);
    }

    const Interval full_range = unsigned_int(width);
    if (size() < full_range.size()) {
        if (Interval extended{_lb.zero_extend(width), _ub.zero_extend(width)}) {
            // If the sign–extended endpoints are in order, no wrap occurred.
            return extended;
        }
    }
    // [0b1111..., 0b0000...] is in the original range, so the result is [0b0000..., 0b1111...] which is the full
    return full_range;
}

} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: Apache-2.0
3	#include <algorithm>
4	#include <cassert>
5
6	#include "crab/interval.hpp"
7
8	namespace prevail {
9
10	// Unsigned division (udiv) operand-box adjustment. Only udiv relies on this;
11	// signed division (sdiv / operator/) divides the original corners directly,
12	// because truncated signed division is monotone per argument on a
13	// sign-consistent box.
14	static Interval make_dividend_when_both_nonzero(const Interval& dividend, const Interval& divisor) {	78✔
15	if (dividend.ub() >= 0) {	117✔
16	return dividend;	78✔
17	}
18	if (divisor.ub() < 0) {	×
19	return dividend + divisor + Interval{1};	×
20	}
21	return dividend + Interval{1} - divisor;	×
22	}
23
24	static ExtendedNumber divide_bound_by_negative_singleton(const ExtendedNumber& bound, const Number& divisor) {	4,312✔
25	assert(divisor < 0);	4,312✔
26	return bound.is_infinite() ? -bound : bound / divisor;	4,312✔
27	}
28
29	Interval Interval::operator*(const Interval& x) const {	4,770,472✔
30	if (is_bottom() \|\| x.is_bottom()) {	4,770,472✔
31	return bottom();	×
32	}
33	const auto [clb, cub] = std::minmax({	4,770,472✔
34	_lb * x._lb,	4,770,472✔
35	_lb * x._ub,	4,770,472✔
36	_ub * x._lb,	4,770,472✔
37	_ub * x._ub,	4,770,472✔
38	});
39	return Interval{clb, cub};	4,770,472✔
40	}
41
42	// Signed division. eBPF has no instruction for this.
43	Interval Interval::operator/(const Interval& x) const {	4,332✔
44	if (is_bottom() \|\| x.is_bottom()) {	4,332✔
45	return bottom();	×
46	}
47	if (const auto n = x.singleton()) {	4,332✔
48	// Divisor is a singleton:
49	// the linear interval solver can perform many divisions where
50	// the divisor is a singleton interval. We optimize for this case.
51	const Number c = *n;	4,328✔
52	if (c == 1) {	4,328✔
53	return *this;	2,196✔
54	} else if (c > 0) {	2,132✔
55	return Interval{_lb / c, _ub / c};	×
56	} else if (c < 0) {	2,132✔
57	return Interval{divide_bound_by_negative_singleton(_ub, c), divide_bound_by_negative_singleton(_lb, c)};	2,132✔
58	} else {
59	// The eBPF ISA defines division by 0 as resulting in 0.
60	return Interval{0};	×
61	}
62	}
63	if (x.contains(0)) {	4✔
64	// The divisor contains 0.
65	const Interval l{x._lb, -1};	×
66	const Interval u{1, x._ub};	×
67	return operator/(l) \| operator/(u) \| Interval{0};	×
68	} else if (contains(0)) {	4✔
69	// The dividend contains 0.
70	const Interval l{_lb, -1};	×
71	const Interval u{1, _ub};	×
72	return (l / x) \| (u / x) \| Interval{0};	×
73	} else {
74	// Neither the dividend nor the divisor contains 0. eBPF signed division
75	// truncates toward zero (matching Number::operator/), and truncated
76	// division is monotone in each argument on a sign-consistent box, so the
77	// extreme quotients are attained at the corners of the operand box.
78	const auto [clb, cub] = std::minmax({	6✔
79	_lb / x._lb,	4✔
80	_lb / x._ub,	4✔
81	_ub / x._lb,	4✔
82	_ub / x._ub,	4✔
83	});
84	return Interval{clb, cub};	4✔
85	}
86	}	2,164✔
87
88	// Signed division.
89	Interval Interval::sdiv(const Interval& x) const {	62✔
90	if (is_bottom() \|\| x.is_bottom()) {	62✔
91	return bottom();	×
92	}
93	if (const auto n = x.singleton()) {	62✔
94	if (n->fits_cast_to<int64_t>()) {	46✔
95	// Divisor is a singleton:
96	// the linear interval solver can perform many divisions where
97	// the divisor is a singleton interval. We optimize for this case.
98	const Number c{n->cast_to<int64_t>()};	46✔
99	if (c == 1) {	46✔
100	return *this;	×
101	} else if (c > 0) {	46✔
102	return Interval{_lb / c, _ub / c};	8✔
103	} else if (c < 0) {	42✔
104	return Interval{divide_bound_by_negative_singleton(_ub, c), divide_bound_by_negative_singleton(_lb, c)};	24✔
105	} else {
106	// The eBPF ISA defines division by 0 as resulting in 0.
107	return Interval{0};	18✔
108	}
109	}
110	}
111	if (x.contains(0)) {	16✔
112	// The divisor contains 0.
113	const Interval l{x._lb, -1};	×
114	const Interval u{1, x._ub};	×
115	return sdiv(l) \| sdiv(u) \| Interval{0};	×
116	} else if (contains(0)) {	16✔
117	// The dividend contains 0.
118	const Interval l{_lb, -1};	2✔
119	const Interval u{1, _ub};	2✔
120	return l.sdiv(x) \| u.sdiv(x) \| Interval{0};	2✔
121	} else {
122	// Neither the dividend nor the divisor contains 0. eBPF signed division
123	// truncates toward zero (matching Number::operator/), and truncated
124	// division is monotone in each argument on a sign-consistent box, so the
125	// extreme quotients are attained at the corners of the operand box.
126	const auto [clb, cub] = std::minmax({	21✔
127	_lb / x._lb,	14✔
128	_lb / x._ub,	14✔
129	_ub / x._lb,	14✔
130	_ub / x._ub,	14✔
131	});
132	return Interval{clb, cub};	14✔
133	}
134	}
135
136	// Unsigned division.
137	Interval Interval::udiv(const Interval& x) const {	1,266✔
138	if (is_bottom() \|\| x.is_bottom()) {	1,266✔
139	return bottom();	88✔
140	}
141	if (const auto n = x.singleton()) {	1,178✔
142	if (n->fits_cast_to<int64_t>()) {	1,012✔
143	// Divisor is a singleton:
144	// the linear interval solver can perform many divisions where
145	// the divisor is a singleton interval. We optimize for this case.
146	const Number c{n->cast_to<uint64_t>()};	1,012✔
147	if (c == 1) {	1,012✔
148	return *this;	×
149	} else if (c > 0) {	1,012✔
150	return Interval{_lb.udiv(c), _ub.udiv(c)};	1,992✔
151	} else {
152	// The eBPF ISA defines division by 0 as resulting in 0.
153	return Interval{0};	16✔
154	}
155	}
156	}
157	if (x.contains(0)) {	166✔
158	// The divisor contains 0.
159	const Interval l{x._lb, -1};	32✔
160	const Interval u{1, x._ub};	32✔
161	return udiv(l) \| udiv(u) \| Interval{0};	32✔
162	}
163	if (contains(0)) {	134✔
164	// The dividend contains 0.
165	const Interval l{_lb, -1};	56✔
166	const Interval u{1, _ub};	56✔
167	return l.udiv(x) \| u.udiv(x) \| Interval{0};	56✔
168	}
169	// Neither the dividend nor the divisor contains 0
170	const Interval a = make_dividend_when_both_nonzero(*this, x);	78✔
171	const auto [clb, cub] = std::minmax({	117✔
172	a._lb.udiv(x._lb),	78✔
173	a._lb.udiv(x._ub),	78✔
174	a._ub.udiv(x._lb),	78✔
175	a._ub.udiv(x._ub),	78✔
176	});
177	return Interval{clb, cub};	78✔
178	}
179
180	// Signed remainder (modulo).
181	Interval Interval::srem(const Interval& x) const {	70✔
182	// note that the sign of the divisor does not matter
183
184	if (is_bottom() \|\| x.is_bottom()) {	70✔
185	return bottom();	×
186	}
187	if (const auto dividend = singleton()) {	70✔
188	if (const auto divisor = x.singleton()) {	68✔
189	if (*divisor == 0) {	60✔
190	return Interval{*dividend};	60✔
191	}
192	return Interval{dividend % divisor};	42✔
193	}
194	}
195	if (x.contains(0)) {	10✔
196	// The divisor contains 0.
197	const Interval l{x._lb, -1};	×
198	const Interval u{1, x._ub};	×
199	return srem(l) \| srem(u) \| *this;	×
200	}
201	if (x.ub().is_finite() && x.lb().is_finite()) {	10✔
202	auto [xlb, xub] = x.pair_number();	10✔
203	const auto [min_divisor, max_divisor] = std::minmax({xlb.abs(), xub.abs()});	10✔
204
205	if (ub() < min_divisor && -lb() < min_divisor) {	10✔
206	// The modulo operation won't change the destination register.
207	return *this;	2✔
208	}
209
210	if (lb() < 0) {	8✔
211	if (ub() > 0) {	2✔
212	return Interval{-(max_divisor - 1), max_divisor - 1};	×
213	} else {
214	return Interval{-(max_divisor - 1), 0};	2✔
215	}
216	}
217	return Interval{0, max_divisor - 1};	6✔
218	}
219	// Divisor has infinite range, so result can be anything between the dividend and zero.
220	return *this \| Interval{0};	×
221	}
222
223	// Unsigned remainder (modulo).
224	Interval Interval::urem(const Interval& x) const {	312✔
225	if (is_bottom() \|\| x.is_bottom()) {	312✔
226	return bottom();	104✔
227	}
228	if (const auto dividend = singleton()) {	208✔
229	if (const auto divisor = x.singleton()) {	50✔
230	if (dividend->fits_cast_to<uint64_t>() && divisor->fits_cast_to<uint64_t>()) {	46✔
231	// The BPF ISA defines modulo by 0 as resulting in the original value.
232	if (*divisor == 0) {	42✔
233	return Interval{*dividend};	42✔
234	}
235	const uint64_t dividend_val = dividend->cast_to<uint64_t>();	28✔
236	const uint64_t divisor_val = divisor->cast_to<uint64_t>();	28✔
237	return Interval{dividend_val % divisor_val};	28✔
238	}
239	}
240	}
241	if (x.contains(0)) {	166✔
242	// The divisor contains 0.
243	const Interval l{x._lb, -1};	52✔
244	const Interval u{1, x._ub};	52✔
245	return urem(l) \| urem(u) \| *this;	52✔
246	} else if (contains(0)) {	114✔
247	// The dividend contains 0.
248	const Interval l{_lb, -1};	52✔
249	const Interval u{1, _ub};	52✔
250	return l.urem(x) \| u.urem(x) \| *this;	52✔
251	} else {
252	// Neither the dividend nor the divisor contains 0
253	if (x._lb.is_infinite() \|\| x._ub.is_infinite()) {	62✔
254	// Divisor is infinite. A "negative" dividend could result in anything except
255	// a value between the upper bound and 0, so set to top. A "positive" dividend
256	// could result in anything between 0 and the dividend - 1.
257	return _ub < 0 ? top() : (*this - Interval{1}) \| Interval{0};	×
258	} else if (_ub.is_finite() && _ub.number()->cast_to<uint64_t>() < x._lb.number()->cast_to<uint64_t>()) {	93✔
259	// Dividend lower than divisor, so the dividend is the remainder.
260	return *this;	6✔
261	} else {
262	const Number max_divisor{x._ub.number()->cast_to<uint64_t>()};	84✔
263	return Interval{0, max_divisor - 1};	56✔
264	}
265	}
266	}
267
268	void Interval::mask_value(const int width) {	107,258✔
269	// we assume never to have wider widths than 64
270	if (width > 0 && width < 64) {	107,258✔
271	*this = bitwise_and(Interval{(1ULL << width) - 1});	8,724✔
272	}
273	}	107,258✔
274
275	void Interval::mask_shift_count(const int width) {	3,980✔
276	if (width > 0) {	3,980✔
277	*this = bitwise_and(Interval{width - 1});	3,980✔
278	}
279	}	3,980✔
280
281	// Do a bitwise-AND between two uvalue intervals.
282	Interval Interval::bitwise_and(const Interval& x) const {	75,086✔
283	if (is_bottom() \|\| x.is_bottom()) {	75,086✔
284	return bottom();	×
285	}
286
287	// Bitwise operations are defined over unsigned machine values.
288	// If an interval temporarily carries a signed lower bound (e.g., after
289	// relational joins before re-establishing uvalue>=0), convert it to the
290	// corresponding 64-bit unsigned range conservatively.
291	Interval left = *this;	75,086✔
292	Interval right = x;	75,086✔
293	if (!left.is_top() && left.lb() < 0) {	75,086✔
294	left = left.zero_extend(64);	256✔
295	}
296	if (!right.is_top() && right.lb() < 0) {	75,086✔
297	right = right.zero_extend(64);	2✔
298	}
299	assert(left.is_top() \|\| left.lb() >= 0);	75,086✔
300	assert(right.is_top() \|\| right.lb() >= 0);	75,086✔
301
302	if (left == Interval{0} \|\| right == Interval{0}) {	75,086✔
303	return Interval{0};	892✔
304	}
305
306	if (const auto right_singleton = right.singleton()) {	74,194✔
307	if (const auto left_singleton = left.singleton()) {	74,026✔
308	return Interval{left_singleton & right_singleton};	9,582✔
309	}
310	if (right_singleton == Number::max_uint(64)) {	64,444✔
311	return left.truncate_to<uint64_t>();	30,105✔
312	}
313	if (right_singleton == Number::max_uint(32)) {	64,442✔
314	return left.zero_extend(32);	48,558✔
315	}
316	if (right_singleton == Number::max_uint(16)) {	15,884✔
317	return left.zero_extend(16);	784✔
318	}
319	if (right_singleton == Number::max_uint(8)) {	15,100✔
320	return left.zero_extend(8);	1,282✔
321	}
322	}
323	if (right.contains(std::numeric_limits<uint64_t>::max())) {	13,986✔
324	return Interval{0, left.truncate_to<uint64_t>().ub()};	45✔
325	} else if (!left.is_top() && !right.is_top()) {	13,956✔
326	return Interval{0, std::min(left.ub(), right.ub())};	18,973✔
327	} else if (!right.is_top()) {	4,012✔
328	return Interval{0, right.ub()};	6,018✔
329	} else if (!left.is_top()) {	×
330	return Interval{0, left.ub()};	×
331	} else {
332	return top();	×
333	}
334	}
335
336	Interval Interval::bitwise_or(const Interval& x) const {	40,702✔
337	if (is_bottom() \|\| x.is_bottom()) {	40,702✔
338	return bottom();	×
339	}
340	if (const auto left_op = singleton()) {	40,702✔
341	if (const auto right_op = x.singleton()) {	458✔
342	return Interval{left_op \| right_op};	370✔
343	}
344	}
345	if (lb() >= 0 && x.lb() >= 0) {	79,709✔
346	if (const auto left_ub = ub().number()) {	57,087✔
347	if (const auto right_ub = x.ub().number()) {	57,084✔
348	return Interval{0, std::max(left_ub, right_ub).fill_ones()};	39,642✔
349	}
350	}
351	return Interval{0, PLUS_INFINITY};	4✔
352	}
353	return top();	2,274✔
354	}
355
356	Interval Interval::bitwise_xor(const Interval& x) const {	2,474✔
357	if (is_bottom() \|\| x.is_bottom()) {	2,474✔
358	return bottom();	×
359	}
360	if (const auto left_op = singleton()) {	2,474✔
361	if (const auto right_op = x.singleton()) {	198✔
362	return Interval{left_op ^ right_op};	198✔
363	}
364	}
365	return bitwise_or(x);	2,276✔
366	}
367
368	Interval Interval::shl(const Interval& x) const {	3,980✔
369	if (is_bottom() \|\| x.is_bottom()) {	3,980✔
370	return bottom();	×
371	}
372	if (const auto shift = x.singleton()) {	3,980✔
373	const Number k = *shift;	2,416✔
374	if (k < 0) {	2,416✔
375	return top();	2,416✔
376	}
377	// Some crazy linux drivers generate shl instructions with huge shifts.
378	// We limit the number of times the loop is run to avoid wasting too much time on it.
379	if (k <= 128) {	2,416✔
380	Number factor = 1;	1,208✔
381	for (int i = 0; k > i; i++) {	70,122✔
382	factor *= 2;	67,706✔
383	}
384	return this->operator*(Interval{factor});	2,416✔
385	}
386	}
387	return top();	1,564✔
388	}
389
390	Interval Interval::ashr(const Interval& x) const {	×
391	if (is_bottom() \|\| x.is_bottom()) {	×
392	return bottom();	×
393	}
394	if (const auto shift = x.singleton()) {	×
395	const Number k = *shift;	×
396	if (k < 0) {	×
397	return top();	×
398	}
399	// Some crazy linux drivers generate ashr instructions with huge shifts.
400	// We limit the number of times the loop is run to avoid wasting too much time on it.
401	if (k <= 128) {	×
402	Number factor = 1;
403	for (int i = 0; k > i; i++) {	×
404	factor *= 2;	×
405	}
406	return this->operator/(Interval{factor});	×
407	}
408	}
409	return top();	×
410	}
411
412	Interval Interval::lshr(const Interval& x) const {	×
413	if (is_bottom() \|\| x.is_bottom()) {	×
414	return bottom();	×
415	}
416	if (const auto shift = x.singleton()) {	×
417	if (*shift > 0 && lb() >= 0 && ub().is_finite()) {	×
418	const auto [lb, ub] = this->pair_number();	×
419	return Interval{lb >> shift, ub >> shift};	×
420	}
421	}
422	return top();	×
423	}
424
425	Interval Interval::sign_extend(const int width) const {	186,924✔
426	if (width <= 0) {	186,924✔
427	CRAB_ERROR("Invalid width ", width);	×
428	}
429
430	const Interval full_range = signed_int(width);	186,924✔
431	if (size() < full_range.size()) {	186,924✔
432	if (Interval extended{_lb.sign_extend(width), _ub.sign_extend(width)}) {	160,642✔
433	// If the sign–extended endpoints are in order, no wrap occurred.
434	return extended;	159,536✔
435	}
436	}
437	// [0b0111..., 0b1000...] is in the original range, so the result is [0b1000..., 0b0111...] which is the full range.
438	return full_range;	27,388✔
439	}
440
441	Interval Interval::zero_extend(const int width) const {	304,502✔
442	if (width <= 0) {	304,502✔
443	CRAB_ERROR("Invalid width ", width);	×
444	}
445
446	const Interval full_range = unsigned_int(width);	304,502✔
447	if (size() < full_range.size()) {	304,502✔
448	if (Interval extended{_lb.zero_extend(width), _ub.zero_extend(width)}) {	228,404✔
449	// If the sign–extended endpoints are in order, no wrap occurred.
450	return extended;	228,214✔
451	}
452	}
453	// [0b1111..., 0b0000...] is in the original range, so the result is [0b0000..., 0b1111...] which is the full
454	return full_range;	76,288✔
455	}
456
457	} // 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