11758318574

Committed 09 Nov 2024 06:02PM UTC coverage: 90.53% (-0.01%) from 90.54%

Build # 11758318574

Build Type

push

github

Committed by

elazarg

Commit Message

Update notes for Windows to install VS Clang

Signed-off-by: Alan Jowett <alan.jowett@microsoft.com>

Run Details

8565 of 9461 relevant lines covered (90.53%)

9192694.75 hits per line

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

78.76

/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::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 (const auto left = singleton()) {
        if (const auto right = x.singleton()) {
            return interval_t{*left & *right};
        }
    }
    if (x == interval_t{std::numeric_limits<uint32_t>::max()}) {
        // Handle bitwise-AND with std::numeric_limits<uint32_t>::max(), which we do for 32-bit operations.
        if (const auto width = finite_size()) {
            const number_t lb32_n = lb().number()->truncate_to<uint32_t>();
            const number_t ub32_n = ub().number()->truncate_to<uint32_t>();
            if (width->fits<uint32_t>() && lb32_n < ub32_n && lb32_n + width->truncate_to<uint32_t>() == ub32_n) {
                return interval_t{lb32_n, ub32_n};
            }
        }
        return full<uint32_t>();
    }
    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::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::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 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();
}

} // 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) {	162✔
8	if (dividend.ub() >= 0) {	243✔
9	return dividend;	154✔
10	}
11	if (divisor.ub() < 0) {	12✔
12	return dividend + divisor + interval_t{1};	10✔
13	}
14	return dividend + interval_t{1} - divisor;	10✔
15	}
16
17	interval_t interval_t::operator*(const interval_t& x) const {	26,005,872✔
18	if (is_bottom() \|\| x.is_bottom()) {	39,008,809✔
19	return bottom();	×
20	}
21	const auto [clb, cub] = std::minmax({	143,032,281✔
22	_lb * x._lb,	13,002,935✔
23	_lb * x._ub,	13,002,937✔
24	_ub * x._lb,	13,002,937✔
25	_ub * x._ub,	13,002,936✔
26	});	52,011,743✔
27	return interval_t{clb, cub};	26,005,870✔
28	}	26,005,869✔
29
30	// Signed division. eBPF has no instruction for this.
31	interval_t interval_t::operator/(const interval_t& x) const {	7,008✔
32	if (is_bottom() \|\| x.is_bottom()) {	10,512✔
33	return bottom();	×
34	}
35	if (const auto n = x.singleton()) {	7,008✔
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;	7,008✔
40	if (c == 1) {	7,008✔
41	return *this;	5,702✔
42	} else if (c > 0) {	1,306✔
43	return interval_t{_lb / c, _ub / c};	×
44	} else if (c < 0) {	1,306✔
45	return interval_t{_ub / c, _lb / c};	3,918✔
46	} else {
47	// The eBPF ISA defines division by 0 as resulting in 0.
48	return interval_t{0};	3,504✔
49	}
50	}	14,016✔
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 {	212✔
76	if (is_bottom() \|\| x.is_bottom()) {	298✔
77	return bottom();	48✔
78	}
79	if (const auto n = x.singleton()) {	164✔
80	if (n->fits_cast_to<int64_t>()) {	76✔
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>()};	76✔
85	if (c == 1) {	76✔
86	return *this;	8✔
87	} else if (c != 0) {	68✔
88	return interval_t{_lb / c, _ub / c};	96✔
89	} else {
90	// The eBPF ISA defines division by 0 as resulting in 0.
91	return interval_t{0};	56✔
92	}
93	}	76✔
94	}	120✔
95	if (x.contains(0)) {	88✔
96	// The divisor contains 0.
97	interval_t l{x._lb, -1};	28✔
98	interval_t u{1, x._ub};	28✔
99	return SDiv(l) \| SDiv(u) \| interval_t{0};	98✔
100	} else if (contains(0)) {	102✔
101	// The dividend contains 0.
102	interval_t l{_lb, -1};	24✔
103	interval_t u{1, _ub};	24✔
104	return l.SDiv(x) \| u.SDiv(x) \| interval_t{0};	84✔
105	} else {	36✔
106	// Neither the dividend nor the divisor contains 0
107	interval_t a = make_dividend_when_both_nonzero(*this, x);	36✔
108	const auto [clb, cub] = std::minmax({	198✔
109	a._lb / x._lb,	36✔
110	a._lb / x._ub,	36✔
111	a._ub / x._lb,	36✔
112	a._ub / x._ub,	36✔
113	});	72✔
114	return interval_t{clb, cub};	36✔
115	}	54✔
116	}
117
118	// Unsigned division.
119	interval_t interval_t::UDiv(const interval_t& x) const {	2,660✔
120	if (is_bottom() \|\| x.is_bottom()) {	3,934✔
121	return bottom();	132✔
122	}
123	if (const auto n = x.singleton()) {	2,528✔
124	if (n->fits_cast_to<int64_t>()) {	2,258✔
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,258✔
129	if (c == 1) {	2,258✔
130	return *this;	8✔
131	} else if (c > 0) {	2,250✔
132	return interval_t{_lb.UDiv(c), _ub.UDiv(c)};	6,654✔
133	} else {
134	// The eBPF ISA defines division by 0 as resulting in 0.
135	return interval_t{0};	1,145✔
136	}
137	}	2,258✔
138	}	2,393✔
139	if (x.contains(0)) {	270✔
140	// The divisor contains 0.
141	interval_t l{x._lb, -1};	52✔
142	interval_t u{1, x._ub};	52✔
143	return UDiv(l) \| UDiv(u) \| interval_t{0};	182✔
144	}	78✔
145	if (contains(0)) {	218✔
146	// The dividend contains 0.
147	interval_t l{_lb, -1};	92✔
148	interval_t u{1, _ub};	92✔
149	return l.UDiv(x) \| u.UDiv(x) \| interval_t{0};	322✔
150	}	138✔
151	// Neither the dividend nor the divisor contains 0
152	interval_t a = make_dividend_when_both_nonzero(*this, x);	126✔
153	const auto [clb, cub] = std::minmax({	693✔
154	a._lb.UDiv(x._lb),	126✔
155	a._lb.UDiv(x._ub),	126✔
156	a._ub.UDiv(x._lb),	126✔
157	a._ub.UDiv(x._ub),	126✔
158	});	252✔
159	return interval_t{clb, cub};	126✔
160	}	1,456✔
161
162	// Signed remainder (modulo).
163	interval_t interval_t::SRem(const interval_t& x) const {	228✔
164	// note that the sign of the divisor does not matter
165
166	if (is_bottom() \|\| x.is_bottom()) {	342✔
167	return bottom();	16✔
168	}
169	if (const auto dividend = singleton()) {	212✔
170	if (const auto divisor = x.singleton()) {	204✔
171	if (*divisor == 0) {	112✔
172	return interval_t{*dividend};	36✔
173	}
174	return interval_t{dividend % divisor};	152✔
175	}	204✔
176	}	162✔
177	if (x.contains(0)) {	100✔
178	// The divisor contains 0.
179	interval_t l{x._lb, -1};	32✔
180	interval_t u{1, x._ub};	32✔
181	return SRem(l) \| SRem(u) \| *this;	96✔
182	}	48✔
183	if (x.ub().is_finite() && x.lb().is_finite()) {	158✔
184	auto [xlb, xub] = x.pair_number();	44✔
185	const auto [min_divisor, max_divisor] = std::minmax({xlb.abs(), xub.abs()});	176✔
186
187	if (ub() < min_divisor && -lb() < min_divisor) {	118✔
188	// The modulo operation won't change the destination register.
189	return *this;	16✔
190	}
191
192	if (lb() < 0) {	42✔
193	if (ub() > 0) {	6✔
194	return interval_t{-(max_divisor - 1), max_divisor - 1};	×
195	} else {
196	return interval_t{-(max_divisor - 1), 0};	8✔
197	}
198	}
199	return interval_t{0, max_divisor - 1};	48✔
200	}	66✔
201	// Divisor has infinite range, so result can be anything between the dividend and zero.
202	return *this \| interval_t{0};	48✔
203	}
204
205	// Unsigned remainder (modulo).
206	interval_t interval_t::URem(const interval_t& x) const {	232✔
207	if (is_bottom() \|\| x.is_bottom()) {	324✔
208	return bottom();	60✔
209	}
210	if (const auto dividend = singleton()) {	172✔
211	if (const auto divisor = x.singleton()) {	164✔
212	if (dividend->fits_cast_to<uint64_t>() && divisor->fits_cast_to<uint64_t>()) {	68✔
213	// The BPF ISA defines modulo by 0 as resulting in the original value.
214	if (*divisor == 0) {	68✔
215	return interval_t{*dividend};	28✔
216	}
217	uint64_t dividend_val = dividend->cast_to<uint64_t>();	40✔
218	uint64_t divisor_val = divisor->cast_to<uint64_t>();	40✔
219	return interval_t{dividend_val % divisor_val};	54✔
220	}
221	}	164✔
222	}	120✔
223	if (x.contains(0)) {	104✔
224	// The divisor contains 0.
225	interval_t l{x._lb, -1};	32✔
226	interval_t u{1, x._ub};	32✔
227	return URem(l) \| URem(u) \| *this;	96✔
228	} else if (contains(0)) {	120✔
229	// The dividend contains 0.
230	interval_t l{_lb, -1};	24✔
231	interval_t u{1, _ub};	24✔
232	return l.URem(x) \| u.URem(x) \| *this;	72✔
233	} else {	36✔
234	// Neither the dividend nor the divisor contains 0
235	if (x._lb.is_infinite() \|\| x._ub.is_infinite()) {	48✔
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};	72✔
240	} else if (_ub.is_finite() && _ub.number()->cast_to<uint64_t>() < x._lb.number()->cast_to<uint64_t>()) {	66✔
241	// Dividend lower than divisor, so the dividend is the remainder.
242	return *this;	12✔
243	} else {
244	number_t max_divisor{x._ub.number()->cast_to<uint64_t>()};	18✔
245	return interval_t{0, max_divisor - 1};	24✔
246	}	12✔
247	}
248	}
249
250	// Do a bitwise-AND between two uvalue intervals.
251	interval_t interval_t::And(const interval_t& x) const {	73,584✔
252	if (is_bottom() \|\| x.is_bottom()) {	110,376✔
253	return bottom();	×
254	}
255	assert(is_top() \|\| (lb() >= 0));	73,584✔
256	assert(x.is_top() \|\| (x.lb() >= 0));	73,584✔
257
258	if (const auto left = singleton()) {	73,584✔
259	if (const auto right = x.singleton()) {	15,814✔
260	return interval_t{left & right};	31,620✔
261	}	15,814✔
262	}	44,697✔
263	if (x == interval_t{std::numeric_limits<uint32_t>::max()}) {	86,661✔
264	// Handle bitwise-AND with std::numeric_limits<uint32_t>::max(), which we do for 32-bit operations.
265	if (const auto width = finite_size()) {	49,664✔
266	const number_t lb32_n = lb().number()->truncate_to<uint32_t>();	87,144✔
267	const number_t ub32_n = ub().number()->truncate_to<uint32_t>();	87,144✔
268	if (width->fits<uint32_t>() && lb32_n < ub32_n && lb32_n + width->truncate_to<uint32_t>() == ub32_n) {	57,204✔
269	return interval_t{lb32_n, ub32_n};	70,390✔
270	}
271	}	82,036✔
272	return full<uint32_t>();	21,508✔
273	}
274	if (x.contains(std::numeric_limits<uint64_t>::max())) {	8,110✔
275	return truncate_to<uint64_t>();	20✔
276	} else if (!is_top() && !x.is_top()) {	8,090✔
277	return interval_t{0, std::min(ub(), x.ub())};	21,336✔
278	} else if (!x.is_top()) {	1,994✔
279	return interval_t{0, x.ub()};	4,985✔
280	} else if (!is_top()) {	×
281	return interval_t{0, ub()};	×
282	} else {
283	return top();	×
284	}
285	}
286
287	interval_t interval_t::Or(const interval_t& x) const {	11,232✔
288	if (is_bottom() \|\| x.is_bottom()) {	16,848✔
289	return bottom();	×
290	}
291	if (const auto left_op = singleton()) {	11,232✔
292	if (const auto right_op = x.singleton()) {	482✔
293	return interval_t{left_op \| right_op};	920✔
294	}	482✔
295	}	5,846✔
296	if (lb() >= 0 && x.lb() >= 0) {	29,270✔
297	if (const auto left_ub = ub().number()) {	17,312✔
298	if (const auto right_ub = x.ub().number()) {	21,630✔
299	return interval_t{0, std::max(left_ub, right_ub).fill_ones()};	17,304✔
300	}	8,652✔
301	}	8,654✔
302	return interval_t{0, bound_t::plus_infinity()};	8✔
303	}
304	return top();	2,116✔
305	}
306
307	interval_t interval_t::Xor(const interval_t& x) const {	896✔
308	if (is_bottom() \|\| x.is_bottom()) {	1,344✔
309	return bottom();	×
310	}
311	if (const auto left_op = singleton()) {	896✔
312	if (const auto right_op = x.singleton()) {	92✔
313	return interval_t{left_op ^ right_op};	176✔
314	}	92✔
315	}	492✔
316	return Or(x);	808✔
317	}
318
319	interval_t interval_t::Shl(const interval_t& x) const {	3,484✔
320	if (is_bottom() \|\| x.is_bottom()) {	5,226✔
321	return bottom();	×
322	}
323	if (const auto shift = x.singleton()) {	3,484✔
324	const number_t k = *shift;	2,552✔
325	if (k < 0) {	2,552✔
326	return top();	×
327	}
328	// Some crazy linux drivers generate shl instructions with huge shifts.
329	// We limit the number of times the loop is run to avoid wasting too much time on it.
330	if (k <= 128) {	2,552✔
331	number_t factor = 1;	2,552✔
332	for (int i = 0; k > i; i++) {	78,916✔
333	factor *= 2;	114,546✔
334	}
335	return this->operator*(interval_t{factor});	5,104✔
336	}	2,552✔
337	}	5,570✔
338	return top();	932✔
339	}
340
341	interval_t interval_t::AShr(const interval_t& x) const {	×
342	if (is_bottom() \|\| x.is_bottom()) {	×
343	return bottom();	×
344	}
345	if (const auto shift = x.singleton()) {	×
346	const number_t k = *shift;	×
347	if (k < 0) {	×
348	return top();	×
349	}
350	// Some crazy linux drivers generate ashr instructions with huge shifts.
351	// We limit the number of times the loop is run to avoid wasting too much time on it.
352	if (k <= 128) {	×
353	number_t factor = 1;	×
354	for (int i = 0; k > i; i++) {	×
355	factor *= 2;	×
356	}
357	return this->operator/(interval_t{factor});	×
358	}	×
359	}	×
360	return top();	×
361	}
362
363	interval_t interval_t::LShr(const interval_t& x) const {	×
364	if (is_bottom() \|\| x.is_bottom()) {	×
365	return bottom();	×
366	}
367	if (const auto shift = x.singleton()) {	×
368	if (*shift > 0 && lb() >= 0 && ub().is_finite()) {	×
369	const auto [lb, ub] = this->pair_number();	×
370	return interval_t{lb >> shift, ub >> shift};	×
371	}	×
372	}	×
373	return top();	×
374	}
375
376	} // namespace crab

vbpf / ebpf-verifier / 11758318574

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