22235569093

Committed 20 Feb 2026 02:12AM UTC coverage: 88.002% (-0.2%) from 88.157%

Build # 22235569093

Build Type

push

github

Committed by

web-flow

Commit Message

Handle Call builtins: fix handling of Falco tests  (#1025)

* falco: fix raw_tracepoint privilege and group expected failures

Mark raw_tracepoint/raw_tracepoint_writable as privileged program types so Falco raw-tracepoint sections are not treated as unprivileged argument checks.

Update Falco sample matrix to move now-passing sections out of TEST_SECTION_FAIL and group the remaining expected failures by root-cause class (offset lower-bound loss vs size lower-bound loss at correlated joins).

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

* elf/unmarshal: gate builtin relocations via platform call model

Add platform hooks to resolve builtin symbols and provide builtin call contracts, thread relocation-gated builtin call offsets through ProgramInfo, and only treat static helper IDs as builtins at gated call sites.

Also extend platform-table, marshal, and YAML-platform tests to cover builtin resolver wiring and call unmarshal behavior.
* crab: canonicalize unsigned intervals in bitwise_and
When uvalue intervals temporarily carry signed lower bounds (e.g. after joins), Interval::bitwise_and asserted in debug builds. Canonicalize both operands via zero_extend(64) before unsigned bitwise reasoning, preserving soundness and avoiding debug aborts.

Validated by reproducing SIGABRT on reverted code in [falco][verify] and confirming the patched build completes with expected 73 pass / 20 failed-as-expected.

* Fix unsound bitwise_and case for non-singleton all-ones rhs

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

Run Details

239 of 252 new or added lines in 9 files covered. (94.84%)

602 existing lines in 16 files now uncovered.

11743 of 13344 relevant lines covered (88.0%)

3262592.78 hits per line

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

75.4

/src/crab/interval.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: Apache-2.0
#include <algorithm>
#include <cassert>

#include "crab/interval.hpp"

namespace prevail {

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

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};
                }
                const uint64_t dividend_val = dividend->cast_to<uint64_t>();
                const uint64_t divisor_val = divisor->cast_to<uint64_t>();
                return Interval{dividend_val % divisor_val};
            }
        }
    }
    if (x.contains(0)) {
        // The divisor contains 0.
        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();
    }

    // Bitwise operations are defined over unsigned machine values.
    // If an interval temporarily carries a signed lower bound (e.g., after
    // relational joins before re-establishing uvalue>=0), convert it to the
    // corresponding 64-bit unsigned range conservatively.
    Interval left = *this;
    Interval right = x;
    if (!left.is_top() && left.lb() < 0) {
        left = left.zero_extend(64);
    }
    if (!right.is_top() && right.lb() < 0) {
        right = right.zero_extend(64);
    }
    assert(left.is_top() || left.lb() >= 0);
    assert(right.is_top() || right.lb() >= 0);

    if (left == Interval{0} || right == Interval{0}) {
        return Interval{0};
    }

    if (const auto right_singleton = right.singleton()) {
        if (const auto left_singleton = left.singleton()) {
            return Interval{*left_singleton & *right_singleton};
        }
        if (right_singleton == Number::max_uint(64)) {
            return left.truncate_to<uint64_t>();
        }
        if (right_singleton == Number::max_uint(32)) {
            return left.zero_extend(32);
        }
        if (right_singleton == Number::max_uint(16)) {
            return left.zero_extend(16);
        }
        if (right_singleton == Number::max_uint(8)) {
            return left.zero_extend(8);
        }
    }
    if (right.contains(std::numeric_limits<uint64_t>::max())) {
        return Interval{0, left.truncate_to<uint64_t>().ub()};
    } else if (!left.is_top() && !right.is_top()) {
        return Interval{0, std::min(left.ub(), right.ub())};
    } else if (!right.is_top()) {
        return Interval{0, right.ub()};
    } else if (!left.is_top()) {
        return Interval{0, left.ub()};
    } else {
        return top();
    }
}

Interval Interval::bitwise_or(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto left_op = singleton()) {
        if (const auto right_op = x.singleton()) {
            return Interval{*left_op | *right_op};
        }
    }
    if (lb() >= 0 && x.lb() >= 0) {
        if (const auto left_ub = ub().number()) {
            if (const auto right_ub = x.ub().number()) {
                return Interval{0, std::max(*left_ub, *right_ub).fill_ones()};
            }
        }
        return Interval{0, PLUS_INFINITY};
    }
    return top();
}

Interval Interval::bitwise_xor(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto left_op = singleton()) {
        if (const auto right_op = x.singleton()) {
            return Interval{*left_op ^ *right_op};
        }
    }
    return bitwise_or(x);
}

Interval Interval::shl(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto shift = x.singleton()) {
        const Number k = *shift;
        if (k < 0) {
            return top();
        }
        // Some crazy linux drivers generate shl instructions with huge shifts.
        // We limit the number of times the loop is run to avoid wasting too much time on it.
        if (k <= 128) {
            Number factor = 1;
            for (int i = 0; k > i; i++) {
                factor *= 2;
            }
            return this->operator*(Interval{factor});
        }
    }
    return top();
}

Interval Interval::ashr(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto shift = x.singleton()) {
        const Number k = *shift;
        if (k < 0) {
            return top();
        }
        // Some crazy linux drivers generate ashr instructions with huge shifts.
        // We limit the number of times the loop is run to avoid wasting too much time on it.
        if (k <= 128) {
            Number factor = 1;
            for (int i = 0; k > i; i++) {
                factor *= 2;
            }
            return this->operator/(Interval{factor});
        }
    }
    return top();
}

Interval Interval::lshr(const Interval& x) const {
    if (is_bottom() || x.is_bottom()) {
        return bottom();
    }
    if (const auto shift = x.singleton()) {
        if (*shift > 0 && lb() >= 0 && ub().is_finite()) {
            const auto [lb, ub] = this->pair_number();
            return Interval{lb >> *shift, ub >> *shift};
        }
    }
    return top();
}

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

    const Interval full_range = signed_int(width);
    if (size() < full_range.size()) {
        if (Interval extended{_lb.sign_extend(width), _ub.sign_extend(width)}) {
            // If the sign–extended endpoints are in order, no wrap occurred.
            return extended;
        }
    }
    // [0b0111..., 0b1000...] is in the original range, so the result is [0b1000..., 0b0111...] which is the full range.
    return full_range;
}

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

    const Interval full_range = unsigned_int(width);
    if (size() < full_range.size()) {
        if (Interval extended{_lb.zero_extend(width), _ub.zero_extend(width)}) {
            // If the sign–extended endpoints are in order, no wrap occurred.
            return extended;
        }
    }
    // [0b1111..., 0b0000...] is in the original range, so the result is [0b0000..., 0b1111...] which is the full
    return full_range;
}

} // namespace prevail

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

Alan-Jowett / ebpf-verifier / 22235569093

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