27778108035

Committed 07 Jun 2026 06:51PM UTC coverage: 86.386% (-2.5%) from 88.93%

Build # 27778108035

Build Type

push

github

Committed by

elazarg

Commit Message

Release v0.2.5

Bump project version to 0.2.5 and add a CHANGELOG entry covering ELF loader hardening, numeric-domain soundness fixes, and the writable helper output initialization documentation update since v0.2.4. Also updates the using_installed_package example version requirement.

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Coverage Stats

9125 of 10563 relevant lines covered (86.39%)

6334294.72 hits per line

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

75.88

/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 {

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

Alan-Jowett / ebpf-verifier / 27778108035

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