• Home
  • Features
  • Pricing
  • Docs
  • Announcements
  • Sign In

vbpf / ebpf-verifier / 12845504567

18 Jan 2025 04:08PM UTC coverage: 88.169% (-1.5%) from 89.646%
12845504567

push

github

web-flow
Handle upgrade from LCOV 1.15 to LCOV 2.0 (#826)

* Testing code coverage with a comment only change
* Workaround for failing code coverage
* Testing code coverage fix

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

8481 of 9619 relevant lines covered (88.17%)

7430805.79 hits per line

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

78.24
/src/crab/interval.cpp
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 {
19,979,462✔
18
    if (is_bottom() || x.is_bottom()) {
29,969,195✔
19
        return bottom();
×
20
    }
21
    const auto [clb, cub] = std::minmax({
109,887,039✔
22
        _lb * x._lb,
9,989,729✔
23
        _lb * x._ub,
9,989,729✔
24
        _ub * x._lb,
9,989,729✔
25
        _ub * x._ub,
9,989,729✔
26
    });
109,887,043✔
27
    return interval_t{clb, cub};
19,979,462✔
28
}
39,958,924✔
29

30
// Signed division. eBPF has no instruction for this.
31
interval_t interval_t::operator/(const interval_t& x) const {
5,480✔
32
    if (is_bottom() || x.is_bottom()) {
8,220✔
33
        return bottom();
×
34
    }
35
    if (const auto n = x.singleton()) {
5,480✔
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;
5,480✔
40
        if (c == 1) {
5,480✔
41
            return *this;
4,652✔
42
        } else if (c > 0) {
828✔
43
            return interval_t{_lb / c, _ub / c};
×
44
        } else if (c < 0) {
828✔
45
            return interval_t{_ub / c, _lb / c};
2,070✔
46
        } else {
47
            // The eBPF ISA defines division by 0 as resulting in 0.
48
            return interval_t{0};
×
49
        }
50
    }
8,220✔
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 {
1,430✔
120
    if (is_bottom() || x.is_bottom()) {
2,107✔
121
        return bottom();
90✔
122
    }
123
    if (const auto n = x.singleton()) {
1,340✔
124
        if (n->fits_cast_to<int64_t>()) {
1,158✔
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>()};
1,158✔
129
            if (c == 1) {
1,158✔
130
                return *this;
4✔
131
            } else if (c > 0) {
1,154✔
132
                return interval_t{_lb.UDiv(c), _ub.UDiv(c)};
2,845✔
133
            } else {
134
                // The eBPF ISA defines division by 0 as resulting in 0.
135
                return interval_t{0};
16✔
136
            }
137
        }
1,158✔
138
    }
1,249✔
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::And(const interval_t& x) const {
38,822✔
252
    if (is_bottom() || x.is_bottom()) {
58,233✔
253
        return bottom();
×
254
    }
255
    assert(is_top() || (lb() >= 0));
38,822✔
256
    assert(x.is_top() || (x.lb() >= 0));
38,822✔
257

258
    if (const auto left = singleton()) {
38,822✔
259
        if (const auto right = x.singleton()) {
8,018✔
260
            return interval_t{*left & *right};
12,024✔
261
        }
8,018✔
262
    }
23,419✔
263
    if (x == interval_t{std::numeric_limits<uint32_t>::max()}) {
46,209✔
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()) {
25,832✔
266
            const number_t lb32_n = lb().number()->truncate_to<uint32_t>();
30,792✔
267
            const number_t ub32_n = ub().number()->truncate_to<uint32_t>();
30,792✔
268
            if (width->fits<uint32_t>() && lb32_n < ub32_n && lb32_n + width->truncate_to<uint32_t>() == ub32_n) {
30,492✔
269
                return interval_t{lb32_n, ub32_n};
36,990✔
270
            }
271
        }
35,710✔
272
        return full<uint32_t>();
11,036✔
273
    }
274
    if (x.contains(std::numeric_limits<uint64_t>::max())) {
4,974✔
275
        return truncate_to<uint64_t>();
10✔
276
    } else if (!is_top() && !x.is_top()) {
4,964✔
277
        return interval_t{0, std::min(ub(), x.ub())};
12,796✔
278
    } else if (!x.is_top()) {
1,308✔
279
        return interval_t{0, x.ub()};
3,270✔
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 {
6,386✔
288
    if (is_bottom() || x.is_bottom()) {
9,579✔
289
        return bottom();
×
290
    }
291
    if (const auto left_op = singleton()) {
6,386✔
292
        if (const auto right_op = x.singleton()) {
236✔
293
            return interval_t{*left_op | *right_op};
330✔
294
        }
236✔
295
    }
3,303✔
296
    if (lb() >= 0 && x.lb() >= 0) {
19,625✔
297
        if (const auto left_ub = ub().number()) {
7,725✔
298
            if (const auto right_ub = x.ub().number()) {
10,296✔
299
                return interval_t{0, std::max(*left_ub, *right_ub).fill_ones()};
10,296✔
300
            }
5,148✔
301
        }
5,149✔
302
        return interval_t{0, bound_t::plus_infinity()};
4✔
303
    }
304
    return top();
1,016✔
305
}
306

307
interval_t interval_t::Xor(const interval_t& x) const {
472✔
308
    if (is_bottom() || x.is_bottom()) {
708✔
309
        return bottom();
×
310
    }
311
    if (const auto left_op = singleton()) {
472✔
312
        if (const auto right_op = x.singleton()) {
70✔
313
            return interval_t{*left_op ^ *right_op};
102✔
314
        }
70✔
315
    }
270✔
316
    return Or(x);
404✔
317
}
318

319
interval_t interval_t::Shl(const interval_t& x) const {
1,938✔
320
    if (is_bottom() || x.is_bottom()) {
2,907✔
321
        return bottom();
×
322
    }
323
    if (const auto shift = x.singleton()) {
1,938✔
324
        const number_t k = *shift;
1,392✔
325
        if (k < 0) {
1,392✔
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) {
1,392✔
331
            number_t factor = 1;
1,392✔
332
            for (int i = 0; k > i; i++) {
44,470✔
333
                factor *= 2;
64,617✔
334
            }
335
            return this->operator*(interval_t{factor});
2,088✔
336
        }
1,392✔
337
    }
2,361✔
338
    return top();
546✔
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
STATUS · Troubleshooting · Open an Issue · Sales · Support · CAREERS · ENTERPRISE · START FREE · SCHEDULE DEMO
ANNOUNCEMENTS · TWITTER · TOS & SLA · Supported CI Services · What's a CI service? · Automated Testing

© 2026 Coveralls, Inc