13955273819

Committed 19 Mar 2025 07:38PM UTC coverage: 88.66% (+0.5%) from 88.134%

Build # 13955273819

Build Type

push

github

Committed by

web-flow

Commit Message

Fix sign extension (#850)

* fix sign extension
* add exhaustive tests for sign extension of <=3 bits
* fix interval::size()
* streamline bit/width operations

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

Run Details

203 of 214 new or added lines in 9 files covered. (94.86%)

9 existing lines in 5 files now uncovered.

8639 of 9744 relevant lines covered (88.66%)

8977818.22 hits per line

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

79.08

/src/crab/interval.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: Apache-2.0
#include "crab/interval.hpp"

namespace crab {

static interval_t make_dividend_when_both_nonzero(const interval_t& dividend, const interval_t& divisor) {
    if (dividend.ub() >= 0) {
        return dividend;
    }
    if (divisor.ub() < 0) {
        return dividend + divisor + interval_t{1};
    }
    return dividend + interval_t{1} - divisor;
}

interval_t interval_t::operator*(const interval_t& 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_t{clb, cub};
}

// Signed division. eBPF has no instruction for this.
interval_t interval_t::operator/(const interval_t& 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_t c = *n;
        if (c == 1) {
            return *this;
        } else if (c > 0) {
            return interval_t{_lb / c, _ub / c};
        } else if (c < 0) {
            return interval_t{_ub / c, _lb / c};
        } else {
            // The eBPF ISA defines division by 0 as resulting in 0.
            return interval_t{0};
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        interval_t l{x._lb, -1};
        interval_t u{1, x._ub};
        return operator/(l) | operator/(u) | interval_t{0};
    } else if (contains(0)) {
        // The dividend contains 0.
        interval_t l{_lb, -1};
        interval_t u{1, _ub};
        return (l / x) | (u / x) | interval_t{0};
    } else {
        // Neither the dividend nor the divisor contains 0
        interval_t 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_t{clb, cub};
    }
}

// Signed division.
interval_t interval_t::sdiv(const interval_t& 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_t c{n->cast_to<int64_t>()};
            if (c == 1) {
                return *this;
            } else if (c != 0) {
                return interval_t{_lb / c, _ub / c};
            } else {
                // The eBPF ISA defines division by 0 as resulting in 0.
                return interval_t{0};
            }
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        interval_t l{x._lb, -1};
        interval_t u{1, x._ub};
        return sdiv(l) | sdiv(u) | interval_t{0};
    } else if (contains(0)) {
        // The dividend contains 0.
        interval_t l{_lb, -1};
        interval_t u{1, _ub};
        return l.sdiv(x) | u.sdiv(x) | interval_t{0};
    } else {
        // Neither the dividend nor the divisor contains 0
        interval_t 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_t{clb, cub};
    }
}

// Unsigned division.
interval_t interval_t::udiv(const interval_t& 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_t c{n->cast_to<uint64_t>()};
            if (c == 1) {
                return *this;
            } else if (c > 0) {
                return interval_t{_lb.udiv(c), _ub.udiv(c)};
            } else {
                // The eBPF ISA defines division by 0 as resulting in 0.
                return interval_t{0};
            }
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        interval_t l{x._lb, -1};
        interval_t u{1, x._ub};
        return udiv(l) | udiv(u) | interval_t{0};
    }
    if (contains(0)) {
        // The dividend contains 0.
        interval_t l{_lb, -1};
        interval_t u{1, _ub};
        return l.udiv(x) | u.udiv(x) | interval_t{0};
    }
    // Neither the dividend nor the divisor contains 0
    interval_t 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_t{clb, cub};
}

// Signed remainder (modulo).
interval_t interval_t::srem(const interval_t& 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_t{*dividend};
            }
            return interval_t{*dividend % *divisor};
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        interval_t l{x._lb, -1};
        interval_t 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_t{-(max_divisor - 1), max_divisor - 1};
            } else {
                return interval_t{-(max_divisor - 1), 0};
            }
        }
        return interval_t{0, max_divisor - 1};
    }
    // Divisor has infinite range, so result can be anything between the dividend and zero.
    return *this | interval_t{0};
}

// Unsigned remainder (modulo).
interval_t interval_t::urem(const interval_t& 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_t{*dividend};
                }
                uint64_t dividend_val = dividend->cast_to<uint64_t>();
                uint64_t divisor_val = divisor->cast_to<uint64_t>();
                return interval_t{dividend_val % divisor_val};
            }
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        interval_t l{x._lb, -1};
        interval_t u{1, x._ub};
        return urem(l) | urem(u) | *this;
    } else if (contains(0)) {
        // The dividend contains 0.
        interval_t l{_lb, -1};
        interval_t 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_t{1}) | interval_t{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_t max_divisor{x._ub.number()->cast_to<uint64_t>()};
            return interval_t{0, max_divisor - 1};
        }
    }
}

// Do a bitwise-AND between two uvalue intervals.
interval_t interval_t::bitwise_and(const interval_t& 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_t{0} || x == interval_t{0}) {
        return interval_t{0};
    }

    if (const auto right = x.singleton()) {
        if (const auto left = singleton()) {
            return interval_t{*left & *right};
        }
        if (right == number_t::max_uint(32)) {
            return zero_extend(32);
        }
        if (right == number_t::max_uint(16)) {
            return zero_extend(16);
        }
        if (right == number_t::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_t{0, std::min(ub(), x.ub())};
    } else if (!x.is_top()) {
        return interval_t{0, x.ub()};
    } else if (!is_top()) {
        return interval_t{0, ub()};
    } else {
        return top();
    }
}

interval_t interval_t::bitwise_or(const interval_t& 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_t{*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_t{0, std::max(*left_ub, *right_ub).fill_ones()};
            }
        }
        return interval_t{0, bound_t::plus_infinity()};
    }
    return top();
}

interval_t interval_t::bitwise_xor(const interval_t& 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_t{*left_op ^ *right_op};
        }
    }
    return bitwise_or(x);
}

interval_t interval_t::shl(const interval_t& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto shift = x.singleton()) {
        const number_t 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_t factor = 1;
            for (int i = 0; k > i; i++) {
                factor *= 2;
            }
            return this->operator*(interval_t{factor});
        }
    }
    return top();
}

interval_t interval_t::ashr(const interval_t& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto shift = x.singleton()) {
        const number_t 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_t factor = 1;
            for (int i = 0; k > i; i++) {
                factor *= 2;
            }
            return this->operator/(interval_t{factor});
        }
    }
    return top();
}

interval_t interval_t::lshr(const interval_t& 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_t{lb >> *shift, ub >> *shift};
        }
    }
    return top();
}

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

    const interval_t full_range = signed_int(width);
    if (size() < full_range.size()) {
        if (interval_t 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_t interval_t::zero_extend(const int width) const {
    if (width <= 0) {
        CRAB_ERROR("Invalid width ", width);
    }

    const interval_t full_range = unsigned_int(width);
    if (size() < full_range.size()) {
        if (interval_t 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 crab

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: Apache-2.0
3	#include "crab/interval.hpp"
4
5	namespace crab {
6
7	static interval_t make_dividend_when_both_nonzero(const interval_t& dividend, const interval_t& divisor) {	104✔
8	if (dividend.ub() >= 0) {	156✔
9	return dividend;	100✔
10	}
11	if (divisor.ub() < 0) {	6✔
12	return dividend + divisor + interval_t{1};	4✔
13	}
14	return dividend + interval_t{1} - divisor;	4✔
15	}
16
17	interval_t interval_t::operator*(const interval_t& x) const {	28,004,616✔
18	if (is_bottom() \|\| x.is_bottom()) {	42,006,926✔
19	return bottom();	×
20	}
21	const auto [clb, cub] = std::minmax({	154,025,386✔
22	_lb * x._lb,	14,002,306✔
23	_lb * x._ub,	14,002,306✔
24	_ub * x._lb,	14,002,306✔
25	_ub * x._ub,	14,002,306✔
26	});	154,025,390✔
27	return interval_t{clb, cub};	28,004,616✔
28	}	56,009,232✔
29
30	// Signed division. eBPF has no instruction for this.
31	interval_t interval_t::operator/(const interval_t& x) const {	6,042✔
32	if (is_bottom() \|\| x.is_bottom()) {	9,063✔
33	return bottom();	×
34	}
35	if (const auto n = x.singleton()) {	6,042✔
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_t c = *n;	6,042✔
40	if (c == 1) {	6,042✔
41	return *this;	5,138✔
42	} else if (c > 0) {	904✔
43	return interval_t{_lb / c, _ub / c};	×
44	} else if (c < 0) {	904✔
45	return interval_t{_ub / c, _lb / c};	2,260✔
46	} else {
47	// The eBPF ISA defines division by 0 as resulting in 0.
48	return interval_t{0};	×
49	}
50	}	9,063✔
51	if (x.contains(0)) {	×
52	// The divisor contains 0.
53	interval_t l{x._lb, -1};	×
54	interval_t u{1, x._ub};	×
55	return operator/(l) \| operator/(u) \| interval_t{0};	×
56	} else if (contains(0)) {	×
57	// The dividend contains 0.
58	interval_t l{_lb, -1};	×
59	interval_t u{1, _ub};	×
60	return (l / x) \| (u / x) \| interval_t{0};	×
61	} else {	×
62	// Neither the dividend nor the divisor contains 0
63	interval_t 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_t{clb, cub};	×
71	}	×
72	}	×
73
74	// Signed division.
75	interval_t interval_t::sdiv(const interval_t& x) const {	106✔
76	if (is_bottom() \|\| x.is_bottom()) {	149✔
77	return bottom();	24✔
78	}
79	if (const auto n = x.singleton()) {	82✔
80	if (n->fits_cast_to<int64_t>()) {	38✔
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_t c{n->cast_to<int64_t>()};	38✔
85	if (c == 1) {	38✔
86	return *this;	4✔
87	} else if (c != 0) {	34✔
88	return interval_t{_lb / c, _ub / c};	40✔
89	} else {
90	// The eBPF ISA defines division by 0 as resulting in 0.
91	return interval_t{0};	18✔
92	}
93	}	38✔
94	}	60✔
95	if (x.contains(0)) {	44✔
96	// The divisor contains 0.
97	interval_t l{x._lb, -1};	14✔
98	interval_t u{1, x._ub};	14✔
99	return sdiv(l) \| sdiv(u) \| interval_t{0};	42✔
100	} else if (contains(0)) {	51✔
101	// The dividend contains 0.
102	interval_t l{_lb, -1};	12✔
103	interval_t u{1, _ub};	12✔
104	return l.sdiv(x) \| u.sdiv(x) \| interval_t{0};	36✔
105	} else {	18✔
106	// Neither the dividend nor the divisor contains 0
107	interval_t a = make_dividend_when_both_nonzero(*this, x);	18✔
108	const auto [clb, cub] = std::minmax({	99✔
109	a._lb / x._lb,	18✔
110	a._lb / x._ub,	18✔
111	a._ub / x._lb,	18✔
112	a._ub / x._ub,	18✔
113	});	90✔
114	return interval_t{clb, cub};	18✔
115	}	27✔
116	}	18✔
117
118	// Unsigned division.
119	interval_t interval_t::udiv(const interval_t& x) const {	2,482✔
120	if (is_bottom() \|\| x.is_bottom()) {	3,685✔
121	return bottom();	90✔
122	}
123	if (const auto n = x.singleton()) {	2,392✔
124	if (n->fits_cast_to<int64_t>()) {	2,210✔
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_t c{n->cast_to<uint64_t>()};	2,210✔
129	if (c == 1) {	2,210✔
130	return *this;	4✔
131	} else if (c > 0) {	2,206✔
132	return interval_t{_lb.udiv(c), _ub.udiv(c)};	5,475✔
133	} else {
134	// The eBPF ISA defines division by 0 as resulting in 0.
135	return interval_t{0};	16✔
136	}
137	}	2,210✔
138	}	2,301✔
139	if (x.contains(0)) {	182✔
140	// The divisor contains 0.
141	interval_t l{x._lb, -1};	30✔
142	interval_t u{1, x._ub};	30✔
143	return udiv(l) \| udiv(u) \| interval_t{0};	90✔
144	}	45✔
145	if (contains(0)) {	152✔
146	// The dividend contains 0.
147	interval_t l{_lb, -1};	66✔
148	interval_t u{1, _ub};	66✔
149	return l.udiv(x) \| u.udiv(x) \| interval_t{0};	198✔
150	}	99✔
151	// Neither the dividend nor the divisor contains 0
152	interval_t a = make_dividend_when_both_nonzero(*this, x);	86✔
153	const auto [clb, cub] = std::minmax({	473✔
154	a._lb.udiv(x._lb),	86✔
155	a._lb.udiv(x._ub),	86✔
156	a._ub.udiv(x._lb),	86✔
157	a._ub.udiv(x._ub),	86✔
158	});	430✔
159	return interval_t{clb, cub};	86✔
160	}	215✔
161
162	// Signed remainder (modulo).
163	interval_t interval_t::srem(const interval_t& x) const {	114✔
164	// note that the sign of the divisor does not matter
165
166	if (is_bottom() \|\| x.is_bottom()) {	171✔
167	return bottom();	8✔
168	}
169	if (const auto dividend = singleton()) {	106✔
170	if (const auto divisor = x.singleton()) {	102✔
171	if (*divisor == 0) {	56✔
172	return interval_t{*dividend};	18✔
173	}
174	return interval_t{dividend % divisor};	57✔
175	}	102✔
176	}	81✔
177	if (x.contains(0)) {	50✔
178	// The divisor contains 0.
179	interval_t l{x._lb, -1};	16✔
180	interval_t u{1, x._ub};	16✔
181	return srem(l) \| srem(u) \| *this;	40✔
182	}	24✔
183	if (x.ub().is_finite() && x.lb().is_finite()) {	79✔
184	auto [xlb, xub] = x.pair_number();	22✔
185	const auto [min_divisor, max_divisor] = std::minmax({xlb.abs(), xub.abs()});	77✔
186
187	if (ub() < min_divisor && -lb() < min_divisor) {	59✔
188	// The modulo operation won't change the destination register.
189	return *this;	8✔
190	}
191
192	if (lb() < 0) {	21✔
193	if (ub() > 0) {	3✔
194	return interval_t{-(max_divisor - 1), max_divisor - 1};	×
195	} else {
196	return interval_t{-(max_divisor - 1), 0};	4✔
197	}
198	}
199	return interval_t{0, max_divisor - 1};	24✔
200	}	33✔
201	// Divisor has infinite range, so result can be anything between the dividend and zero.
202	return *this \| interval_t{0};	18✔
203	}	22✔
204
205	// Unsigned remainder (modulo).
206	interval_t interval_t::urem(const interval_t& x) const {	116✔
207	if (is_bottom() \|\| x.is_bottom()) {	162✔
208	return bottom();	30✔
209	}
210	if (const auto dividend = singleton()) {	86✔
211	if (const auto divisor = x.singleton()) {	82✔
212	if (dividend->fits_cast_to<uint64_t>() && divisor->fits_cast_to<uint64_t>()) {	34✔
213	// The BPF ISA defines modulo by 0 as resulting in the original value.
214	if (*divisor == 0) {	34✔
215	return interval_t{*dividend};	14✔
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_t{dividend_val % divisor_val};	20✔
220	}
221	}	82✔
222	}	60✔
223	if (x.contains(0)) {	52✔
224	// The divisor contains 0.
225	interval_t l{x._lb, -1};	16✔
226	interval_t u{1, x._ub};	16✔
227	return urem(l) \| urem(u) \| *this;	40✔
228	} else if (contains(0)) {	60✔
229	// The dividend contains 0.
230	interval_t l{_lb, -1};	12✔
231	interval_t 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()) {	24✔
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_t{1}) \| interval_t{0};	30✔
240	} else if (_ub.is_finite() && _ub.number()->cast_to<uint64_t>() < x._lb.number()->cast_to<uint64_t>()) {	33✔
241	// Dividend lower than divisor, so the dividend is the remainder.
242	return *this;	6✔
243	} else {
244	number_t max_divisor{x._ub.number()->cast_to<uint64_t>()};	9✔
245	return interval_t{0, max_divisor - 1};	12✔
246	}	6✔
247	}
248	}
249
250	// Do a bitwise-AND between two uvalue intervals.
251	interval_t interval_t::bitwise_and(const interval_t& x) const {	68,052✔
252	if (is_bottom() \|\| x.is_bottom()) {	102,078✔
253	return bottom();	×
254	}
255	assert(is_top() \|\| (lb() >= 0));	68,052✔
256	assert(x.is_top() \|\| (x.lb() >= 0));	68,052✔
257
258	if (*this == interval_t{0} \|\| x == interval_t{0}) {	134,224✔
259	return interval_t{0};	3,762✔
260	}
261
262	if (const auto right = x.singleton()) {	64,290✔
263	if (const auto left = singleton()) {	64,282✔
264	return interval_t{left & right};	13,257✔
265	}	36,560✔
266	if (right == number_t::max_uint(32)) {	55,444✔
267	return zero_extend(32);	48,406✔
268	}
269	if (right == number_t::max_uint(16)) {	7,038✔
270	return zero_extend(16);	2,746✔
271	}
272	if (right == number_t::max_uint(8)) {	4,292✔
273	return zero_extend(8);	854✔
274	}
275	}	62,567✔
276	if (x.contains(std::numeric_limits<uint64_t>::max())) {	3,446✔
277	return truncate_to<uint64_t>();	10✔
278	} else if (!is_top() && !x.is_top()) {	3,436✔
279	return interval_t{0, std::min(ub(), x.ub())};	7,812✔
280	} else if (!x.is_top()) {	1,204✔
281	return interval_t{0, x.ub()};	3,010✔
282	} else if (!is_top()) {	×
283	return interval_t{0, ub()};	×
284	} else {
285	return top();	×
286	}
287	}
288
289	interval_t interval_t::bitwise_or(const interval_t& x) const {	9,050✔
290	if (is_bottom() \|\| x.is_bottom()) {	13,575✔
291	return bottom();	×
292	}
293	if (const auto left_op = singleton()) {	9,050✔
294	if (const auto right_op = x.singleton()) {	256✔
295	return interval_t{left_op \| right_op};	348✔
296	}	256✔
297	}	4,641✔
298	if (lb() >= 0 && x.lb() >= 0) {	28,607✔
299	if (const auto left_ub = ub().number()) {	11,457✔
300	if (const auto right_ub = x.ub().number()) {	15,272✔
301	return interval_t{0, std::max(left_ub, right_ub).fill_ones()};	15,272✔
302	}	7,636✔
303	}	7,637✔
304	return interval_t{0, bound_t::plus_infinity()};	4✔
305	}
306	return top();	1,180✔
307	}
308
309	interval_t interval_t::bitwise_xor(const interval_t& x) const {	828✔
310	if (is_bottom() \|\| x.is_bottom()) {	1,242✔
311	return bottom();	×
312	}
313	if (const auto left_op = singleton()) {	828✔
314	if (const auto right_op = x.singleton()) {	70✔
315	return interval_t{left_op ^ right_op};	102✔
316	}	70✔
317	}	448✔
318	return bitwise_or(x);	760✔
319	}
320
321	interval_t interval_t::shl(const interval_t& x) const {	2,160✔
322	if (is_bottom() \|\| x.is_bottom()) {	3,240✔
323	return bottom();	×
324	}
325	if (const auto shift = x.singleton()) {	2,160✔
326	const number_t k = *shift;	1,614✔
327	if (k < 0) {	1,614✔
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,614✔
333	number_t factor = 1;	1,614✔
334	for (int i = 0; k > i; i++) {	49,572✔
335	factor *= 2;	71,937✔
336	}
337	return this->operator*(interval_t{factor});	2,421✔
338	}	1,614✔
339	}	2,694✔
340	return top();	546✔
341	}
342
NEW 343	interval_t interval_t::ashr(const interval_t& x) const {	×
344	if (is_bottom() \|\| x.is_bottom()) {	×
345	return bottom();	×
346	}
347	if (const auto shift = x.singleton()) {	×
348	const number_t 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_t factor = 1;	×
356	for (int i = 0; k > i; i++) {	×
357	factor *= 2;	×
358	}
359	return this->operator/(interval_t{factor});	×
360	}	×
361	}	×
362	return top();	×
363	}
364
NEW 365	interval_t interval_t::lshr(const interval_t& 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_t{lb >> shift, ub >> shift};	×
373	}	×
374	}	×
375	return top();	×
376	}
377
378	interval_t interval_t::sign_extend(const int width) const {	58,232✔
379	if (width <= 0) {	58,232✔
NEW 380	CRAB_ERROR("Invalid width ", width);	×
381	}
382
383	const interval_t full_range = signed_int(width);	58,232✔
384	if (size() < full_range.size()) {	87,348✔
385	if (interval_t extended{_lb.sign_extend(width), _ub.sign_extend(width)}) {	122,285✔
386	// If the sign–extended endpoints are in order, no wrap occurred.
387	return extended;	48,700✔
388	}	48,914✔
389	}
390	// [0b0111..., 0b1000...] is in the original range, so the result is [0b1000..., 0b0111...] which is the full range.
391	return full_range;	9,532✔
392	}	58,232✔
393
394	interval_t interval_t::zero_extend(const int width) const {	143,156✔
395	if (width <= 0) {	143,156✔
NEW 396	CRAB_ERROR("Invalid width ", width);	×
397	}
398
399	const interval_t full_range = unsigned_int(width);	143,156✔
400	if (size() < full_range.size()) {	214,734✔
401	if (interval_t extended{_lb.zero_extend(width), _ub.zero_extend(width)}) {	232,755✔
402	// If the sign–extended endpoints are in order, no wrap occurred.
403	return extended;	93,048✔
404	}	93,102✔
405	}
406	// [0b1111..., 0b0000...] is in the original range, so the result is [0b0000..., 0b1111...] which is the full
407	return full_range;	50,108✔
408	}	143,156✔
409	} // namespace crab

vbpf / ebpf-verifier / 13955273819

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