19036509529

Committed 02 Nov 2025 09:22PM UTC coverage: 86.936% (-0.5%) from 87.448%

Build # 19036509529

Build Type

push

github

Committed by

elazarg

Commit Message

Bump external/libbtf from `b674148` to `04281ee`

Bumps [external/libbtf](https://github.com/Alan-Jowett/libbtf) from `b674148` to `04281ee`.
- [Release notes](https://github.com/Alan-Jowett/libbtf/releases)
- [Commits](https://github.com/Alan-Jowett/libbtf/compare/b6741487e...<a class=hub.com/Alan-Jowett/ebpf-verifier/commit/04281ee7a91595911807897b4ca2e7483cf97497">04281ee7a)

---
updated-dependencies:
- dependency-name: external/libbtf
  dependency-version: '04281ee7a91595911807897b4ca2e7483cf97497'
  dependency-type: direct:production
...

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

Run Details

9044 of 10403 relevant lines covered (86.94%)

3989157.54 hits per line

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

86.19

/src/crab/rcp.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#include <ranges>

#include "arith/variable.hpp"
#include "crab/interval.hpp"
#include "crab/rcp.hpp"
#include "crab/type_domain.hpp"
#include "crab/var_registry.hpp"

namespace prevail {

std::optional<Variable> get_type_offset_variable(const Reg& reg, const int type) {
    RegPack r = reg_pack(reg);
    switch (type) {
    case T_CTX: return r.ctx_offset;
    case T_MAP: return r.map_fd;
    case T_MAP_PROGRAMS: return r.map_fd_programs;
    case T_PACKET: return r.packet_offset;
    case T_SHARED: return r.shared_offset;
    case T_STACK: return r.stack_offset;
    default: return {};
    }
}

std::optional<Variable> TypeToNumDomain::get_type_offset_variable(const Reg& reg) const {
    return prevail::get_type_offset_variable(reg, types.get_type(reg));
}

bool TypeToNumDomain::operator<=(const TypeToNumDomain& other) const {
    if (is_bottom()) {
        return true;
    }
    if (other.is_bottom()) {
        return false;
    }
    // First, check the type domain.
    // For example, if r1 in `this` has type {stack} and r1 in `other` has type {stack, packet},
    // then `this` is less than or equal to `other`.
    if (!(types <= other.types)) {
        return false;
    }
    // Then, check the numeric domain with consideration of type-specific variables.
    TypeToNumDomain tmp{other.types, other.values};
    for (const Variable& v : this->get_nonexistent_kind_variables()) {
        tmp.values.havoc(v);
    }
    return values <= tmp.values;
}

void TypeToNumDomain::join_selective(const TypeToNumDomain& right) {
    if (is_bottom()) {
        *this = right;
        return;
    }
    if (right.is_bottom()) {
        return;
    }
    auto extra_invariants = collect_type_dependent_constraints(right);
    this->values |= right.values;
    for (const auto& [variable, interval] : extra_invariants) {
        values.set(variable, interval);
    }
}

void TypeToNumDomain::operator|=(const TypeToNumDomain& other) {
    if (is_bottom()) {
        *this = other;
    }
    if (other.is_bottom()) {
        return;
    }
    this->join_selective(other);
    this->types |= other.types;
}

void TypeToNumDomain::operator|=(TypeToNumDomain&& other) {
    if (is_bottom()) {
        *this = other;
    }
    if (other.is_bottom()) {
        return;
    }
    this->join_selective(other);
    this->types |= std::move(other.types);
}

TypeToNumDomain TypeToNumDomain::operator&(const TypeToNumDomain& other) const {
    if (auto type_inv = types.meet(other.types)) {
        // TODO: remove unuseful variables from the numeric domain
        return TypeToNumDomain{std::move(*type_inv), values & other.values};
    }
    return TypeToNumDomain{TypeDomain::top(), NumAbsDomain::bottom()};
}

TypeToNumDomain TypeToNumDomain::operator&(TypeToNumDomain&& other) const {
    if (auto type_inv = types.meet(std::move(other.types))) {
        // TODO: remove unuseful variables from the numeric domain
        return TypeToNumDomain{std::move(*type_inv), values & std::move(other.values)};
    }
    return {TypeDomain::top(), NumAbsDomain::bottom()};
}

std::vector<Variable> TypeToNumDomain::get_nonexistent_kind_variables() const {
    std::vector<Variable> res;
    for (const Variable v : variable_registry->get_type_variables()) {
        for (const auto& [type, kinds] : type_to_kinds) {
            if (types.may_have_type(v, type)) {
                continue;
            }
            for (const auto kind : kinds) {
                Variable type_offset = variable_registry->kind_var(kind, v);
                res.push_back(type_offset);
            }
        }
    }
    return res;
}

std::vector<std::tuple<Variable, Interval>>
TypeToNumDomain::collect_type_dependent_constraints(const TypeToNumDomain& right) const {
    std::vector<std::tuple<Variable, Interval>> result;

    for (const Variable& type_var : variable_registry->get_type_variables()) {
        for (const auto& [type, kinds] : type_to_kinds) {
            if (kinds.empty()) {
                continue;
            }
            const bool in_left = types.may_have_type(type_var, type);
            const bool in_right = right.types.may_have_type(type_var, type);

            // If a type may be present in one domain but not the other, its
            // dependent constraints must be explicitly preserved.
            if (in_left != in_right) {
                // Identify which domain contains the constraints.
                const NumAbsDomain& source = in_left ? values : right.values;
                for (const DataKind kind : kinds) {
                    Variable var = variable_registry->kind_var(kind, type_var);
                    Interval value = source.eval_interval(var);
                    if (!value.is_top()) {
                        result.emplace_back(var, value);
                    }
                }
            }
        }
    }

    return result;
}

std::vector<TypeEncoding> TypeToNumDomain::enumerate_types(const Reg& reg) const {
    using namespace dsl_syntax;
    if (!types.is_initialized(reg)) {
        return {T_UNINIT};
    }
    return types.iterate_types(reg);
}

TypeToNumDomain
TypeToNumDomain::join_over_types(const Reg& reg,
                                 const std::function<void(TypeToNumDomain&, TypeEncoding)>& transition) const {
    using namespace dsl_syntax;
    if (!types.is_initialized(reg)) {
        TypeToNumDomain res = *this;
        transition(res, T_UNINIT);
        return res;
    }
    TypeToNumDomain res = bottom();
    const std::vector<TypeEncoding> valid_types = types.iterate_types(reg);
    std::map<TypeEncoding, std::vector<DataKind>> valid_type_to_kinds;
    for (const TypeEncoding type : valid_types) {
        valid_type_to_kinds.emplace(type, type_to_kinds.at(type));
    }
    for (const TypeEncoding type : valid_types) {
        TypeToNumDomain tmp(*this);
        tmp.types.add_constraint(reg_type(reg) == type);
        // This might have changed the type variable of reg.
        // It might also have changed the type variable of other registers, but we don't deal with that.
        for (const auto& [other_type, kinds] : valid_type_to_kinds) {
            if (other_type != type) {
                for (const auto kind : kinds) {
                    tmp.values.havoc(variable_registry->kind_var(kind, reg_type(reg)));
                }
            }
        }
        transition(tmp, type);
        res |= tmp;
    }
    return res;
}

void TypeToNumDomain::havoc_all_locations_having_type(const TypeEncoding type) {
    for (const Variable type_variable : variable_registry->get_type_variables()) {
        if (types.may_have_type(type_variable, type)) {
            types.havoc_type(type_variable);
            values.havoc(variable_registry->kind_var(DataKind::svalues, type_variable));
            values.havoc(variable_registry->kind_var(DataKind::uvalues, type_variable));
            for (const DataKind kind : type_to_kinds.at(type)) {
                values.havoc(variable_registry->kind_var(kind, type_variable));
            }
        }
    }
}

void TypeToNumDomain::assume_type(const LinearConstraint& cst) {
    types.add_constraint(cst);
    if (types.inv.is_bottom()) {
        values.set_to_bottom();
    }
}

void TypeToNumDomain::assign(const Reg& lhs, const Reg& rhs) {
    if (lhs == rhs) {
        return;
    }
    types.assign_type(lhs, rhs);

    values.assign(reg_pack(lhs).svalue, reg_pack(rhs).svalue);
    values.assign(reg_pack(lhs).uvalue, reg_pack(rhs).uvalue);

    for (const auto& type : types.iterate_types(lhs)) {
        for (const auto& kind : type_to_kinds.at(type)) {
            values.havoc(variable_registry->kind_var(kind, reg_type(lhs)));
        }
    }
    for (const auto& type : types.iterate_types(rhs)) {
        for (const auto kind : type_to_kinds.at(type)) {
            const auto lhs_var = variable_registry->kind_var(kind, reg_type(lhs));
            values.assign(lhs_var, variable_registry->kind_var(kind, reg_type(rhs)));
        }
    }
}

void TypeToNumDomain::havoc_offsets(const Reg& reg) {
    const RegPack r = reg_pack(reg);
    values.havoc(r.ctx_offset);
    values.havoc(r.map_fd);
    values.havoc(r.map_fd_programs);
    values.havoc(r.packet_offset);
    values.havoc(r.shared_offset);
    values.havoc(r.shared_region_size);
    values.havoc(r.stack_offset);
    values.havoc(r.stack_numeric_size);
}

void TypeToNumDomain::havoc_register_except_type(const Reg& reg) {
    const RegPack r = reg_pack(reg);
    havoc_offsets(reg);
    values.havoc(r.svalue);
    values.havoc(r.uvalue);
}

void TypeToNumDomain::havoc_register(const Reg& reg) {
    types.havoc_type(reg);
    havoc_register_except_type(reg);
}

TypeToNumDomain TypeToNumDomain::widen(const TypeToNumDomain& other) const {
    auto extra_invariants = collect_type_dependent_constraints(other);

    TypeToNumDomain res{types.widen(other.types), values.widen(other.values)};

    // Now add in the extra invariants saved above.
    for (const auto& [variable, interval] : extra_invariants) {
        res.values.set(variable, interval);
    }
    return res;
}

TypeToNumDomain TypeToNumDomain::narrow(const TypeToNumDomain& rcp) const {
    return TypeToNumDomain{types.narrow(rcp.types), values.narrow(rcp.values)};
}

StringInvariant TypeToNumDomain::to_set() const {
    if (is_bottom()) {
        return StringInvariant::bottom();
    }
    return types.to_set() + values.to_set();
}
} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <ranges>
4
5	#include "arith/variable.hpp"
6	#include "crab/interval.hpp"
7	#include "crab/rcp.hpp"
8	#include "crab/type_domain.hpp"
9	#include "crab/var_registry.hpp"
10
11	namespace prevail {
12
13	std::optional<Variable> get_type_offset_variable(const Reg& reg, const int type) {	17,544✔
14	RegPack r = reg_pack(reg);	17,544✔
15	switch (type) {	17,544✔
16	case T_CTX: return r.ctx_offset;	12✔
17	case T_MAP: return r.map_fd;	12✔
18	case T_MAP_PROGRAMS: return r.map_fd_programs;	×
19	case T_PACKET: return r.packet_offset;	5,528✔
20	case T_SHARED: return r.shared_offset;	146✔
21	case T_STACK: return r.stack_offset;	9,030✔
22	default: return {};	2,816✔
23	}
24	}
25
26	std::optional<Variable> TypeToNumDomain::get_type_offset_variable(const Reg& reg) const {	12,792✔
27	return prevail::get_type_offset_variable(reg, types.get_type(reg));	12,792✔
28	}
29
30	bool TypeToNumDomain::operator<=(const TypeToNumDomain& other) const {	502✔
31	if (is_bottom()) {	502✔
32	return true;	3✔
33	}
34	if (other.is_bottom()) {	496✔
35	return false;	1✔
36	}
37	// First, check the type domain.
38	// For example, if r1 in `this` has type {stack} and r1 in `other` has type {stack, packet},
39	// then `this` is less than or equal to `other`.
40	if (!(types <= other.types)) {	494✔
41	return false;	7✔
42	}
43	// Then, check the numeric domain with consideration of type-specific variables.
44	TypeToNumDomain tmp{other.types, other.values};	960✔
45	for (const Variable& v : this->get_nonexistent_kind_variables()) {	4,550✔
46	tmp.values.havoc(v);	4,070✔
47	}	240✔
48	return values <= tmp.values;	480✔
49	}	480✔
50
51	void TypeToNumDomain::join_selective(const TypeToNumDomain& right) {	49,516✔
52	if (is_bottom()) {	49,516✔
53	*this = right;	×
54	return;	×
55	}
56	if (right.is_bottom()) {	49,516✔
57	return;
58	}
59	auto extra_invariants = collect_type_dependent_constraints(right);	49,516✔
60	this->values \|= right.values;	49,516✔
61	for (const auto& [variable, interval] : extra_invariants) {	61,746✔
62	values.set(variable, interval);	12,230✔
63	}
64	}	49,516✔
65
66	void TypeToNumDomain::operator\|=(const TypeToNumDomain& other) {	32,972✔
67	if (is_bottom()) {	32,972✔
68	*this = other;	32,670✔
69	}
70	if (other.is_bottom()) {	32,972✔
71	return;	238✔
72	}
73	this->join_selective(other);	32,496✔
74	this->types \|= other.types;	32,496✔
75	}
76
77	void TypeToNumDomain::operator\|=(TypeToNumDomain&& other) {	17,020✔
78	if (is_bottom()) {	17,020✔
79	*this = other;	×
80	}
81	if (other.is_bottom()) {	17,020✔
82	return;
83	}
84	this->join_selective(other);	17,020✔
85	this->types \|= std::move(other.types);	17,020✔
86	}
87
88	TypeToNumDomain TypeToNumDomain::operator&(const TypeToNumDomain& other) const {	38✔
89	if (auto type_inv = types.meet(other.types)) {	38✔
90	// TODO: remove unuseful variables from the numeric domain
91	return TypeToNumDomain{std::move(*type_inv), values & other.values};	57✔
92	}	38✔
93	return TypeToNumDomain{TypeDomain::top(), NumAbsDomain::bottom()};	×
94	}
95
96	TypeToNumDomain TypeToNumDomain::operator&(TypeToNumDomain&& other) const {	×
97	if (auto type_inv = types.meet(std::move(other.types))) {	×
98	// TODO: remove unuseful variables from the numeric domain
99	return TypeToNumDomain{std::move(*type_inv), values & std::move(other.values)};	×
100	}	×
101	return {TypeDomain::top(), NumAbsDomain::bottom()};	×
102	}
103
104	std::vector<Variable> TypeToNumDomain::get_nonexistent_kind_variables() const {	480✔
105	std::vector<Variable> res;	480✔
106	for (const Variable v : variable_registry->get_type_variables()) {	11,029✔
107	for (const auto& [type, kinds] : type_to_kinds) {	84,392✔
108	if (types.may_have_type(v, type)) {	73,843✔
109	continue;	70,641✔
110	}
111	for (const auto kind : kinds) {	7,272✔
112	Variable type_offset = variable_registry->kind_var(kind, v);	4,070✔
113	res.push_back(type_offset);	4,070✔
114	}
115	}
116	}	240✔
117	return res;	480✔
118	}	×
119
120	std::vector<std::tuple<Variable, Interval>>
121	TypeToNumDomain::collect_type_dependent_constraints(const TypeToNumDomain& right) const {	49,600✔
122	std::vector<std::tuple<Variable, Interval>> result;	49,600✔
123
124	for (const Variable& type_var : variable_registry->get_type_variables()) {	2,271,617✔
125	for (const auto& [type, kinds] : type_to_kinds) {	17,776,136✔
126	if (kinds.empty()) {	15,554,119✔
127	continue;	2,222,017✔
128	}
129	const bool in_left = types.may_have_type(type_var, type);	13,332,102✔
130	const bool in_right = right.types.may_have_type(type_var, type);	13,332,102✔
131
132	// If a type may be present in one domain but not the other, its
133	// dependent constraints must be explicitly preserved.
134	if (in_left != in_right) {	13,332,102✔
135	// Identify which domain contains the constraints.
136	const NumAbsDomain& source = in_left ? values : right.values;	450,544✔
137	for (const DataKind kind : kinds) {	1,051,400✔
138	Variable var = variable_registry->kind_var(kind, type_var);	600,856✔
139	Interval value = source.eval_interval(var);	600,856✔
140	if (!value.is_top()) {	600,856✔
141	result.emplace_back(var, value);	12,230✔
142	}
143	}	600,856✔
144	}
145	}
146	}	24,800✔
147
148	return result;	49,600✔
149	}	×
150
151	std::vector<TypeEncoding> TypeToNumDomain::enumerate_types(const Reg& reg) const {	57,378✔
152	using namespace dsl_syntax;	28,689✔
153	if (!types.is_initialized(reg)) {	57,378✔
154	return {T_UNINIT};	×
155	}
156	return types.iterate_types(reg);	57,378✔
157	}
158
159	TypeToNumDomain
160	TypeToNumDomain::join_over_types(const Reg& reg,	32,668✔
161	const std::function<void(TypeToNumDomain&, TypeEncoding)>& transition) const {
162	using namespace dsl_syntax;	16,334✔
163	if (!types.is_initialized(reg)) {	32,668✔
164	TypeToNumDomain res = *this;	×
165	transition(res, T_UNINIT);	×
166	return res;	×
167	}	×
168	TypeToNumDomain res = bottom();	32,668✔
169	const std::vector<TypeEncoding> valid_types = types.iterate_types(reg);	32,668✔
170	std::map<TypeEncoding, std::vector<DataKind>> valid_type_to_kinds;	32,668✔
171	for (const TypeEncoding type : valid_types) {	65,520✔
172	valid_type_to_kinds.emplace(type, type_to_kinds.at(type));	32,852✔
173	}
174	for (const TypeEncoding type : valid_types) {	65,520✔
175	TypeToNumDomain tmp(*this);	32,852✔
176	tmp.types.add_constraint(reg_type(reg) == type);	49,278✔
177	// This might have changed the type variable of reg.
178	// It might also have changed the type variable of other registers, but we don't deal with that.
179	for (const auto& [other_type, kinds] : valid_type_to_kinds) {	66,072✔
180	if (other_type != type) {	33,220✔
181	for (const auto kind : kinds) {	1,084✔
182	tmp.values.havoc(variable_registry->kind_var(kind, reg_type(reg)));	716✔
183	}
184	}
185	}
186	transition(tmp, type);	32,852✔
187	res \|= tmp;	32,852✔
188	}	32,852✔
189	return res;	32,668✔
190	}	49,002✔
191
192	void TypeToNumDomain::havoc_all_locations_having_type(const TypeEncoding type) {	40✔
193	for (const Variable type_variable : variable_registry->get_type_variables()) {	1,314✔
194	if (types.may_have_type(type_variable, type)) {	1,274✔
195	types.havoc_type(type_variable);	874✔
196	values.havoc(variable_registry->kind_var(DataKind::svalues, type_variable));	874✔
197	values.havoc(variable_registry->kind_var(DataKind::uvalues, type_variable));	874✔
198	for (const DataKind kind : type_to_kinds.at(type)) {	1,748✔
199	values.havoc(variable_registry->kind_var(kind, type_variable));	874✔
200	}
201	}
202	}	40✔
203	}	40✔
204
205	void TypeToNumDomain::assume_type(const LinearConstraint& cst) {	×
206	types.add_constraint(cst);	×
207	if (types.inv.is_bottom()) {	×
208	values.set_to_bottom();	×
209	}
210	}	×
211
212	void TypeToNumDomain::assign(const Reg& lhs, const Reg& rhs) {	26,004✔
213	if (lhs == rhs) {	39,006✔
214	return;
215	}
216	types.assign_type(lhs, rhs);	26,004✔
217
218	values.assign(reg_pack(lhs).svalue, reg_pack(rhs).svalue);	26,004✔
219	values.assign(reg_pack(lhs).uvalue, reg_pack(rhs).uvalue);	26,004✔
220
221	for (const auto& type : types.iterate_types(lhs)) {	52,020✔
222	for (const auto& kind : type_to_kinds.at(type)) {	51,754✔
223	values.havoc(variable_registry->kind_var(kind, reg_type(lhs)));	25,738✔
224	}
225	}	13,002✔
226	for (const auto& type : types.iterate_types(rhs)) {	52,020✔
227	for (const auto kind : type_to_kinds.at(type)) {	51,754✔
228	const auto lhs_var = variable_registry->kind_var(kind, reg_type(lhs));	25,738✔
229	values.assign(lhs_var, variable_registry->kind_var(kind, reg_type(rhs)));	38,607✔
230	}
231	}	26,004✔
232	}
233
234	void TypeToNumDomain::havoc_offsets(const Reg& reg) {	151,528✔
235	const RegPack r = reg_pack(reg);	151,528✔
236	values.havoc(r.ctx_offset);	151,528✔
237	values.havoc(r.map_fd);	151,528✔
238	values.havoc(r.map_fd_programs);	151,528✔
239	values.havoc(r.packet_offset);	151,528✔
240	values.havoc(r.shared_offset);	151,528✔
241	values.havoc(r.shared_region_size);	151,528✔
242	values.havoc(r.stack_offset);	151,528✔
243	values.havoc(r.stack_numeric_size);	151,528✔
244	}	151,528✔
245
246	void TypeToNumDomain::havoc_register_except_type(const Reg& reg) {	91,044✔
247	const RegPack r = reg_pack(reg);	91,044✔
248	havoc_offsets(reg);	91,044✔
249	values.havoc(r.svalue);	91,044✔
250	values.havoc(r.uvalue);	91,044✔
251	}	91,044✔
252
253	void TypeToNumDomain::havoc_register(const Reg& reg) {	70,906✔
254	types.havoc_type(reg);	70,906✔
255	havoc_register_except_type(reg);	70,906✔
256	}	70,906✔
257
258	TypeToNumDomain TypeToNumDomain::widen(const TypeToNumDomain& other) const {	84✔
259	auto extra_invariants = collect_type_dependent_constraints(other);	84✔
260
261	TypeToNumDomain res{types.widen(other.types), values.widen(other.values)};	126✔
262
263	// Now add in the extra invariants saved above.
264	for (const auto& [variable, interval] : extra_invariants) {	84✔
265	res.values.set(variable, interval);	×
266	}
267	return res;	126✔
268	}	84✔
269
270	TypeToNumDomain TypeToNumDomain::narrow(const TypeToNumDomain& rcp) const {	×
271	return TypeToNumDomain{types.narrow(rcp.types), values.narrow(rcp.values)};	×
272	}
273
274	StringInvariant TypeToNumDomain::to_set() const {	1,384✔
275	if (is_bottom()) {	1,384✔
276	return StringInvariant::bottom();	434✔
277	}
278	return types.to_set() + values.to_set();	1,425✔
279	}
280	} // namespace prevail

Alan-Jowett / ebpf-verifier / 19036509529

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