18949625295

Committed 28 Oct 2025 10:33AM UTC coverage: 87.448% (-1.0%) from 88.47%

Build # 18949625295

Build Type

push

github

Committed by

elazarg

Commit Message

Bump CLI11 to v2.6.1

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

Run Details

9022 of 10317 relevant lines covered (87.45%)

10783407.68 hits per line

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

74.47

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

// 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, Bound::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) {	76✔
8	if (dividend.ub() >= 0) {	114✔
9	return dividend;	72✔
10	}
11	if (divisor.ub() < 0) {	6✔
12	return dividend + divisor + Interval{1};	4✔
13	}
14	return dividend + Interval{1} - divisor;	4✔
15	}
16
17	Interval Interval::operator*(const Interval& x) const {	164,591,911✔
18	if (is_bottom() \|\| x.is_bottom()) {	246,882,850✔
19	return bottom();	×
20	}
21	const auto [clb, cub] = std::minmax({	905,260,527✔
22	_lb * x._lb,	82,300,972✔
23	_lb * x._ub,	82,300,972✔
24	_ub * x._lb,	82,300,972✔
25	_ub * x._ub,	82,300,972✔
26	});	905,250,494✔
27	return Interval{clb, cub};	164,591,911✔
28	}	329,183,822✔
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()) {	568✔
121	return bottom();	64✔
122	}
123	if (const auto n = x.singleton()) {	332✔
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	}	261✔
139	if (x.contains(0)) {	142✔
140	// The divisor contains 0.
141	Interval l{x._lb, -1};	16✔
142	Interval u{1, x._ub};	16✔
143	return udiv(l) \| udiv(u) \| Interval{0};	48✔
144	}	24✔
145	if (contains(0)) {	126✔
146	// The dividend contains 0.
147	Interval l{_lb, -1};	54✔
148	Interval u{1, _ub};	54✔
149	return l.udiv(x) \| u.udiv(x) \| Interval{0};	162✔
150	}	81✔
151	// Neither the dividend nor the divisor contains 0
152	Interval a = make_dividend_when_both_nonzero(*this, x);	72✔
153	const auto [clb, cub] = std::minmax({	396✔
154	a._lb.udiv(x._lb),	72✔
155	a._lb.udiv(x._ub),	72✔
156	a._ub.udiv(x._lb),	72✔
157	a._ub.udiv(x._ub),	72✔
158	});	360✔
159	return Interval{clb, cub};	72✔
160	}	180✔
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()) {	150✔
208	return bottom();	12✔
209	}
210	if (const auto dividend = singleton()) {	88✔
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	}	59✔
223	if (x.contains(0)) {	58✔
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)) {	64✔
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()) {	34✔
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>()) {	75✔
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>()};	42✔
245	return Interval{0, max_divisor - 1};	56✔
246	}	28✔
247	}
248	}
249
250	// Do a bitwise-AND between two uvalue intervals.
251	Interval Interval::bitwise_and(const Interval& x) const {	28,938✔
252	if (is_bottom() \|\| x.is_bottom()) {	43,407✔
253	return bottom();	×
254	}
255	assert(is_top() \|\| (lb() >= 0));	28,938✔
256	assert(x.is_top() \|\| (x.lb() >= 0));	28,938✔
257
258	if (*this == Interval{0} \|\| x == Interval{0}) {	55,768✔
259	return Interval{0};	4,218✔
260	}
261
262	if (const auto right = x.singleton()) {	24,720✔
263	if (const auto left = singleton()) {	24,702✔
264	return Interval{left & right};	7,923✔
265	}	14,992✔
266	if (right == Number::max_uint(32)) {	19,420✔
267	return zero_extend(32);	15,248✔
268	}
269	if (right == Number::max_uint(16)) {	4,172✔
270	return zero_extend(16);	650✔
271	}
272	if (right == Number::max_uint(8)) {	3,522✔
273	return zero_extend(8);	500✔
274	}
275	}	23,200✔
276	if (x.contains(std::numeric_limits<uint64_t>::max())) {	3,040✔
277	return truncate_to<uint64_t>();	12✔
278	} else if (!is_top() && !x.is_top()) {	3,028✔
279	return Interval{0, std::min(ub(), x.ub())};	6,454✔
280	} else if (!x.is_top()) {	1,184✔
281	return Interval{0, x.ub()};	2,960✔
282	} else if (!is_top()) {	×
283	return Interval{0, ub()};	×
284	} else {
285	return top();	×
286	}
287	}
288
289	Interval Interval::bitwise_or(const Interval& x) const {	6,866✔
290	if (is_bottom() \|\| x.is_bottom()) {	10,299✔
291	return bottom();	×
292	}
293	if (const auto left_op = singleton()) {	6,866✔
294	if (const auto right_op = x.singleton()) {	250✔
295	return Interval{left_op \| right_op};	363✔
296	}	250✔
297	}	3,554✔
298	if (lb() >= 0 && x.lb() >= 0) {	21,052✔
299	if (const auto left_ub = ub().number()) {	8,190✔
300	if (const auto right_ub = x.ub().number()) {	10,916✔
301	return Interval{0, std::max(left_ub, right_ub).fill_ones()};	10,916✔
302	}	5,458✔
303	}	5,459✔
304	return Interval{0, Bound::plus_infinity()};	4✔
305	}
306	return top();	1,164✔
307	}
308
309	Interval Interval::bitwise_xor(const Interval& x) const {	670✔
310	if (is_bottom() \|\| x.is_bottom()) {	1,005✔
311	return bottom();	×
312	}
313	if (const auto left_op = singleton()) {	670✔
314	if (const auto right_op = x.singleton()) {	108✔
315	return Interval{left_op ^ right_op};	162✔
316	}	108✔
317	}	389✔
318	return bitwise_or(x);	562✔
319	}
320
321	Interval Interval::shl(const Interval& x) const {	2,002✔
322	if (is_bottom() \|\| x.is_bottom()) {	3,003✔
323	return bottom();	×
324	}
325	if (const auto shift = x.singleton()) {	2,002✔
326	const Number k = *shift;	1,520✔
327	if (k < 0) {	1,520✔
328	return top();	×
329	}
330	// Some crazy linux drivers generate shl instructions with huge shifts.
331	// We limit the number of times the loop is run to avoid wasting too much time on it.
332	if (k <= 128) {	1,520✔
333	Number factor = 1;	1,520✔
334	for (int i = 0; k > i; i++) {	48,358✔
335	factor *= 2;	70,257✔
336	}
337	return this->operator*(Interval{factor});	2,280✔
338	}	1,520✔
339	}	2,521✔
340	return top();	482✔
341	}
342
343	Interval Interval::ashr(const Interval& x) const {	×
344	if (is_bottom() \|\| x.is_bottom()) {	×
345	return bottom();	×
346	}
347	if (const auto shift = x.singleton()) {	×
348	const Number k = *shift;	×
349	if (k < 0) {	×
350	return top();	×
351	}
352	// Some crazy linux drivers generate ashr instructions with huge shifts.
353	// We limit the number of times the loop is run to avoid wasting too much time on it.
354	if (k <= 128) {	×
355	Number factor = 1;	×
356	for (int i = 0; k > i; i++) {	×
357	factor *= 2;	×
358	}
359	return this->operator/(Interval{factor});	×
360	}	×
361	}	×
362	return top();	×
363	}
364
365	Interval Interval::lshr(const Interval& x) const {	×
366	if (is_bottom() \|\| x.is_bottom()) {	×
367	return bottom();	×
368	}
369	if (const auto shift = x.singleton()) {	×
370	if (*shift > 0 && lb() >= 0 && ub().is_finite()) {	×
371	const auto [lb, ub] = this->pair_number();	×
372	return Interval{lb >> shift, ub >> shift};	×
373	}	×
374	}	×
375	return top();	×
376	}
377
378	Interval Interval::sign_extend(const int width) const {	40,988✔
379	if (width <= 0) {	40,988✔
380	CRAB_ERROR("Invalid width ", width);	×
381	}
382
383	const Interval full_range = signed_int(width);	40,988✔
384	if (size() < full_range.size()) {	61,482✔
385	if (Interval extended{_lb.sign_extend(width), _ub.sign_extend(width)}) {	87,015✔
386	// If the sign–extended endpoints are in order, no wrap occurred.
387	return extended;	34,528✔
388	}	34,806✔
389	}
390	// [0b0111..., 0b1000...] is in the original range, so the result is [0b1000..., 0b0111...] which is the full range.
391	return full_range;	6,460✔
392	}	40,988✔
393
394	Interval Interval::zero_extend(const int width) const {	79,606✔
395	if (width <= 0) {	79,606✔
396	CRAB_ERROR("Invalid width ", width);	×
397	}
398
399	const Interval full_range = unsigned_int(width);	79,606✔
400	if (size() < full_range.size()) {	119,409✔
401	if (Interval extended{_lb.zero_extend(width), _ub.zero_extend(width)}) {	160,145✔
402	// If the sign–extended endpoints are in order, no wrap occurred.
403	return extended;	64,004✔
404	}	64,058✔
405	}
406	// [0b1111..., 0b0000...] is in the original range, so the result is [0b0000..., 0b1111...] which is the full
407	return full_range;	15,602✔
408	}	79,606✔
409	} // namespace prevail

Alan-Jowett / ebpf-verifier / 18949625295

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