19036509529

Committed 02 Nov 2025 09:22PM UTC coverage: 86.936% (-0.5%) from 87.448%

Build # 19036509529

Build Type

push

github

Committed by

elazarg

Commit Message

Bump external/libbtf from `b674148` to `04281ee`

Bumps [external/libbtf](https://github.com/Alan-Jowett/libbtf) from `b674148` to `04281ee`.
- [Release notes](https://github.com/Alan-Jowett/libbtf/releases)
- [Commits](https://github.com/Alan-Jowett/libbtf/compare/b6741487e...<a class=hub.com/Alan-Jowett/ebpf-verifier/commit/04281ee7a91595911807897b4ca2e7483cf97497">04281ee7a)

---
updated-dependencies:
- dependency-name: external/libbtf
  dependency-version: '04281ee7a91595911807897b4ca2e7483cf97497'
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>

Run Details

9044 of 10403 relevant lines covered (86.94%)

3989157.54 hits per line

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

74.83

/src/crab/interval.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: Apache-2.0
#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;
}

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.
        Number c = *n;
        if (c == 1) {
            return *this;
        } else if (c > 0) {
            return Interval{_lb / c, _ub / c};
        } else if (c < 0) {
            return Interval{_ub / c, _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.
        Interval l{x._lb, -1};
        Interval u{1, x._ub};
        return operator/(l) | operator/(u) | Interval{0};
    } else if (contains(0)) {
        // The dividend contains 0.
        Interval l{_lb, -1};
        Interval u{1, _ub};
        return (l / x) | (u / x) | Interval{0};
    } else {
        // Neither the dividend nor the divisor contains 0
        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.
            Number c{n->cast_to<int64_t>()};
            if (c == 1) {
                return *this;
            } else if (c != 0) {
                return Interval{_lb / c, _ub / c};
            } else {
                // The eBPF ISA defines division by 0 as resulting in 0.
                return Interval{0};
            }
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        Interval l{x._lb, -1};
        Interval u{1, x._ub};
        return sdiv(l) | sdiv(u) | Interval{0};
    } else if (contains(0)) {
        // The dividend contains 0.
        Interval l{_lb, -1};
        Interval u{1, _ub};
        return l.sdiv(x) | u.sdiv(x) | Interval{0};
    } else {
        // Neither the dividend nor the divisor contains 0
        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.
            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.
        Interval l{x._lb, -1};
        Interval u{1, x._ub};
        return udiv(l) | udiv(u) | Interval{0};
    }
    if (contains(0)) {
        // The dividend contains 0.
        Interval l{_lb, -1};
        Interval u{1, _ub};
        return l.udiv(x) | u.udiv(x) | Interval{0};
    }
    // Neither the dividend nor the divisor contains 0
    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.
        Interval l{x._lb, -1};
        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};
                }
                uint64_t dividend_val = dividend->cast_to<uint64_t>();
                uint64_t divisor_val = divisor->cast_to<uint64_t>();
                return Interval{dividend_val % divisor_val};
            }
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        Interval l{x._lb, -1};
        Interval u{1, x._ub};
        return urem(l) | urem(u) | *this;
    } else if (contains(0)) {
        // The dividend contains 0.
        Interval l{_lb, -1};
        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 {
            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();
    }
    assert(is_top() || (lb() >= 0));
    assert(x.is_top() || (x.lb() >= 0));

    if (*this == Interval{0} || x == Interval{0}) {
        return Interval{0};
    }

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

Alan-Jowett / ebpf-verifier / 19036509529

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