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

Alan-Jowett / ebpf-verifier / 18658728485

18 Oct 2025 05:56PM UTC coverage: 88.47% (+0.4%) from 88.11%
18658728485

push

github

elazarg
Bump external/bpf_conformance from `8f3c2fe` to `6fa6a20`

Bumps [external/bpf_conformance](https://github.com/Alan-Jowett/bpf_conformance) from `8f3c2fe` to `6fa6a20`.
- [Release notes](https://github.com/Alan-Jowett/bpf_conformance/releases)
- [Commits](https://github.com/Alan-Jowett/bpf_conformance/compare/8f3c2fe88...<a class=hub.com/Alan-Jowett/ebpf-verifier/commit/6fa6a20ac6fd3612ea9338312a67408687b9f06b">6fa6a20ac)

---
updated-dependencies:
- dependency-name: external/bpf_conformance
  dependency-version: 6fa6a20ac6fd3612ea9338312a67408687b9f06b
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>

8954 of 10121 relevant lines covered (88.47%)

18293099.16 hits per line

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

86.44
/src/crab/type_domain.cpp
1
// Copyright (c) Prevail Verifier contributors.
2
// SPDX-License-Identifier: MIT
3
// ReSharper disable CppMemberFunctionMayBeStatic
4

5
// This file is eBPF-specific, not derived from CRAB.
6
#include <functional>
7
#include <map>
8
#include <optional>
9

10
#include "arith/dsl_syntax.hpp"
11
#include "arith/variable.hpp"
12
#include "crab/array_domain.hpp"
13
#include "crab/interval.hpp"
14
#include "crab/split_dbm.hpp"
15
#include "crab/type_domain.hpp"
16
#include "crab/type_encoding.hpp"
17
#include "crab/var_registry.hpp"
18
#include "crab_utils/debug.hpp"
19

20
namespace prevail {
21

22
template <is_enum T>
23
static void operator++(T& t) {
507,044✔
24
    t = static_cast<T>(1 + static_cast<std::underlying_type_t<T>>(t));
507,044✔
25
}
507,044✔
26

27
std::vector<DataKind> iterate_kinds(const DataKind lb, const DataKind ub) {
32,834✔
28
    if (lb > ub) {
32,834✔
29
        CRAB_ERROR("lower bound ", lb, " is greater than upper bound ", ub);
×
30
    }
31
    if (lb < KIND_MIN || ub > KIND_MAX) {
32,834✔
32
        CRAB_ERROR("bounds ", lb, " and ", ub, " are out of range");
×
33
    }
34
    std::vector<DataKind> res;
32,834✔
35
    for (DataKind i = lb; i <= ub; ++i) {
361,174✔
36
        res.push_back(i);
328,340✔
37
    }
38
    return res;
32,834✔
39
}
×
40

41
std::vector<TypeEncoding> iterate_types(const TypeEncoding lb, const TypeEncoding ub) {
178,204✔
42
    if (lb > ub) {
178,204✔
43
        CRAB_ERROR("lower bound ", lb, " is greater than upper bound ", ub);
×
44
    }
45
    if (lb < T_MIN || ub > T_MAX) {
178,204✔
46
        CRAB_ERROR("bounds ", lb, " and ", ub, " are out of range");
×
47
    }
48
    std::vector<TypeEncoding> res;
178,204✔
49
    for (TypeEncoding i = lb; i <= ub; ++i) {
356,908✔
50
        res.push_back(i);
178,704✔
51
    }
52
    return res;
178,204✔
53
}
×
54

55
std::vector<TypeEncoding> TypeDomain::iterate_types(const Reg& reg) const {
178,174✔
56
    const Interval allowed_types = inv.eval_interval(reg_type(reg));
178,174✔
57
    if (!allowed_types) {
178,174✔
58
        return {};
×
59
    }
60
    if (allowed_types.contains(T_UNINIT)) {
178,174✔
61
        return {T_UNINIT};
×
62
    }
63
    auto [lb, ub] = allowed_types.bound(T_MIN_VALID, T_MAX);
178,174✔
64
    return prevail::iterate_types(lb, ub);
178,174✔
65
}
178,174✔
66

67
static constexpr auto S_UNINIT = "uninit";
68
static constexpr auto S_STACK = "stack";
69
static constexpr auto S_PACKET = "packet";
70
static constexpr auto S_CTX = "ctx";
71
static constexpr auto S_MAP_PROGRAMS = "map_fd_programs";
72
static constexpr auto S_MAP = "map_fd";
73
static constexpr auto S_NUM = "number";
74
static constexpr auto S_SHARED = "shared";
75

76
std::string name_of(const DataKind kind) {
14,351,276✔
77
    switch (kind) {
14,351,276✔
78
    case DataKind::ctx_offsets: return "ctx_offset";
2,586,288✔
79
    case DataKind::map_fds: return "map_fd";
2,523,492✔
80
    case DataKind::map_fd_programs: return "map_fd_programs";
2,520,984✔
81
    case DataKind::packet_offsets: return "packet_offset";
2,544,264✔
82
    case DataKind::shared_offsets: return "shared_offset";
2,545,820✔
83
    case DataKind::shared_region_sizes: return "shared_region_size";
2,545,820✔
84
    case DataKind::stack_numeric_sizes: return "stack_numeric_size";
2,819,984✔
85
    case DataKind::stack_offsets: return "stack_offset";
2,818,660✔
86
    case DataKind::svalues: return "svalue";
2,541,792✔
87
    case DataKind::types: return "type";
2,762,684✔
88
    case DataKind::uvalues: return "uvalue";
3,115,955✔
89
    }
90
    return {};
×
91
}
92

93
DataKind regkind(const std::string& s) {
4,506✔
94
    static const std::map<std::string, DataKind> string_to_kind{
2,253✔
95
        {"type", DataKind::types},
41✔
96
        {"ctx_offset", DataKind::ctx_offsets},
41✔
97
        {"map_fd", DataKind::map_fds},
41✔
98
        {"map_fd_programs", DataKind::map_fd_programs},
41✔
99
        {"packet_offset", DataKind::packet_offsets},
41✔
100
        {"shared_offset", DataKind::shared_offsets},
41✔
101
        {"stack_offset", DataKind::stack_offsets},
41✔
102
        {"shared_region_size", DataKind::shared_region_sizes},
41✔
103
        {"stack_numeric_size", DataKind::stack_numeric_sizes},
41✔
104
        {"svalue", DataKind::svalues},
41✔
105
        {"uvalue", DataKind::uvalues},
41✔
106
    };
5,531✔
107
    if (string_to_kind.contains(s)) {
4,506✔
108
        return string_to_kind.at(s);
4,506✔
109
    }
110
    throw std::runtime_error(std::string() + "Bad kind: " + s);
×
111
}
82✔
112

113
std::ostream& operator<<(std::ostream& os, const TypeEncoding s) {
2,032✔
114
    switch (s) {
2,032✔
115
    case T_SHARED: return os << S_SHARED;
98✔
116
    case T_STACK: return os << S_STACK;
272✔
117
    case T_PACKET: return os << S_PACKET;
116✔
118
    case T_CTX: return os << S_CTX;
102✔
119
    case T_NUM: return os << S_NUM;
1,420✔
120
    case T_MAP: return os << S_MAP;
18✔
121
    case T_MAP_PROGRAMS: return os << S_MAP_PROGRAMS;
6✔
122
    case T_UNINIT: return os << S_UNINIT;
×
123
    default: CRAB_ERROR("Unsupported type encoding", s);
×
124
    }
125
}
126

127
TypeEncoding string_to_type_encoding(const std::string& s) {
2,572✔
128
    static std::map<std::string, TypeEncoding> string_to_type{
1,286✔
129
        {S_UNINIT, T_UNINIT}, {S_MAP_PROGRAMS, T_MAP_PROGRAMS},
41✔
130
        {S_MAP, T_MAP},       {S_NUM, T_NUM},
82✔
131
        {S_CTX, T_CTX},       {S_STACK, T_STACK},
82✔
132
        {S_PACKET, T_PACKET}, {S_SHARED, T_SHARED},
82✔
133
    };
3,351✔
134
    if (string_to_type.contains(s)) {
2,572✔
135
        return string_to_type[s];
2,572✔
136
    }
137
    throw std::runtime_error(std::string("Unsupported type name: ") + s);
×
138
}
82✔
139

140
Variable reg_type(const Reg& lhs) { return variable_registry->type_reg(lhs.v); }
1,331,930✔
141

142
void TypeDomain::assign_type(const Reg& lhs, const Reg& rhs) { inv.assign(reg_type(lhs), reg_type(rhs)); }
46,470✔
143

144
void TypeDomain::assign_type(const std::optional<Variable> lhs, const LinearExpression& t) { inv.assign(lhs, t); }
31,748✔
145

146
void TypeDomain::assign_type(const Reg& lhs, const std::optional<LinearExpression>& rhs) {
108,348✔
147
    inv.assign(reg_type(lhs), rhs);
108,348✔
148
}
108,348✔
149

150
void TypeDomain::havoc_type(const Reg& r) { inv.havoc(reg_type(r)); }
125,468✔
151
void TypeDomain::havoc_type(const Variable& v) { inv.havoc(v); }
1,180✔
152

153
TypeEncoding TypeDomain::get_type(const LinearExpression& v) const {
×
154
    const auto res = inv.eval_interval(v).singleton();
×
155
    if (!res) {
×
156
        return T_UNINIT;
157
    }
158
    return res->narrow<TypeEncoding>();
×
159
}
×
160

161
TypeEncoding TypeDomain::get_type(const Reg& r) const {
26,026✔
162
    const auto res = inv.eval_interval(reg_type(r)).singleton();
39,039✔
163
    if (!res) {
26,026✔
164
        return T_UNINIT;
40✔
165
    }
166
    return res->narrow<TypeEncoding>();
25,946✔
167
}
26,026✔
168

169
[[nodiscard]]
170
bool TypeDomain::is_initialized(const Reg& r) const {
333,968✔
171
    using namespace dsl_syntax;
166,984✔
172
    return inv.entail(reg_type(r) != T_UNINIT);
500,952✔
173
}
174

175
[[nodiscard]]
176
bool TypeDomain::is_initialized(const LinearExpression& v) const {
1,802,372✔
177
    using namespace dsl_syntax;
901,186✔
178
    return inv.entail(v != T_UNINIT);
2,703,558✔
179
}
180

181
// Check whether a given type value is within the range of a given type variable's value.
182
bool TypeDomain::may_have_type(const Reg& r, const TypeEncoding type) const {
4✔
183
    const Interval interval = inv.eval_interval(reg_type(r));
4✔
184
    return interval.contains(type);
6✔
185
}
4✔
186

187
bool TypeDomain::may_have_type(const LinearExpression& v, const TypeEncoding type) const {
282,552,321✔
188
    const Interval interval = inv.eval_interval(v);
282,552,321✔
189
    return interval.contains(type);
423,831,706✔
190
}
282,552,321✔
191

192
static LinearConstraint eq_types(const Reg& a, const Reg& b) {
18,862✔
193
    using namespace dsl_syntax;
9,431✔
194
    return eq(reg_type(a), reg_type(b));
18,862✔
195
}
196

197
bool TypeDomain::same_type(const Reg& a, const Reg& b) const { return inv.entail(eq_types(a, b)); }
28,293✔
198

199
bool TypeDomain::is_in_group(const Reg& r, const TypeGroup group) const {
93,476✔
200
    using namespace dsl_syntax;
46,738✔
201
    const Variable t = reg_type(r);
93,476✔
202
    switch (group) {
93,476✔
203
    case TypeGroup::number: return inv.entail(t == T_NUM);
70,830✔
204
    case TypeGroup::map_fd: return inv.entail(t == T_MAP);
4,476✔
205
    case TypeGroup::map_fd_programs: return inv.entail(t == T_MAP_PROGRAMS);
414✔
206
    case TypeGroup::ctx: return inv.entail(t == T_CTX);
7,854✔
207
    case TypeGroup::packet: return inv.entail(t == T_PACKET);
×
208
    case TypeGroup::stack: return inv.entail(t == T_STACK);
×
209
    case TypeGroup::shared: return inv.entail(t == T_SHARED);
×
210
    case TypeGroup::mem: return inv.entail(t >= T_PACKET);
11,244✔
211
    case TypeGroup::mem_or_num: return inv.entail(t >= T_NUM) && inv.entail(t != T_CTX);
3,332✔
212
    case TypeGroup::pointer: return inv.entail(t >= T_CTX);
28,704✔
213
    case TypeGroup::ptr_or_num: return inv.entail(t >= T_NUM);
26,248✔
214
    case TypeGroup::stack_or_packet: return inv.entail(t >= T_PACKET) && inv.entail(t <= T_STACK);
×
215
    case TypeGroup::singleton_ptr: return inv.entail(t >= T_CTX) && inv.entail(t <= T_STACK);
6,112✔
216
    default: CRAB_ERROR("Unsupported type group", group);
×
217
    }
218
}
219

220
std::string typeset_to_string(const std::vector<TypeEncoding>& items) {
54✔
221
    std::stringstream ss;
54✔
222
    ss << "{";
54✔
223
    for (auto it = items.begin(); it != items.end(); ++it) {
198✔
224
        ss << *it;
144✔
225
        if (std::next(it) != items.end()) {
216✔
226
            ss << ", ";
90✔
227
        }
228
    }
229
    ss << "}";
54✔
230
    return ss.str();
108✔
231
}
54✔
232

233
bool is_singleton_type(const TypeGroup t) {
2,164✔
234
    switch (t) {
2,164✔
235
    case TypeGroup::number:
1,057✔
236
    case TypeGroup::map_fd:
237
    case TypeGroup::map_fd_programs:
238
    case TypeGroup::ctx:
239
    case TypeGroup::packet:
240
    case TypeGroup::stack:
241
    case TypeGroup::shared: return true;
1,057✔
242
    default: return false;
50✔
243
    }
244
}
245

246
std::ostream& operator<<(std::ostream& os, const TypeGroup ts) {
4,376✔
247
    using namespace prevail;
2,188✔
248
    static const std::map<TypeGroup, std::string> string_to_type{
2,188✔
249
        {TypeGroup::number, S_NUM},
2✔
250
        {TypeGroup::map_fd, S_MAP},
2✔
251
        {TypeGroup::map_fd_programs, S_MAP_PROGRAMS},
2✔
252
        {TypeGroup::ctx, S_CTX},
2✔
253
        {TypeGroup::packet, S_PACKET},
2✔
254
        {TypeGroup::stack, S_STACK},
2✔
255
        {TypeGroup::shared, S_SHARED},
2✔
256
        {TypeGroup::mem, typeset_to_string({T_STACK, T_PACKET, T_SHARED})},
8✔
257
        {TypeGroup::pointer, typeset_to_string({T_CTX, T_STACK, T_PACKET, T_SHARED})},
8✔
258
        {TypeGroup::ptr_or_num, typeset_to_string({T_NUM, T_CTX, T_STACK, T_PACKET, T_SHARED})},
8✔
259
        {TypeGroup::stack_or_packet, typeset_to_string({T_STACK, T_PACKET})},
8✔
260
        {TypeGroup::singleton_ptr, typeset_to_string({T_CTX, T_STACK, T_PACKET})},
8✔
261
        {TypeGroup::mem_or_num, typeset_to_string({T_NUM, T_STACK, T_PACKET, T_SHARED})},
8✔
262
    };
4,438✔
263
    if (string_to_type.contains(ts)) {
4,376✔
264
        return os << string_to_type.at(ts);
4,376✔
265
    }
266
    CRAB_ERROR("Unsupported type group", ts);
×
267
}
28✔
268

269
} // namespace prevail
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