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

74.4

/src/crab/ebpf_domain.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT

// This file is eBPF-specific, not derived from CRAB.

#include <optional>
#include <utility>
#include <vector>

#include "boost/endian/conversion.hpp"

#include "arith/dsl_syntax.hpp"
#include "config.hpp"
#include "crab/array_domain.hpp"
#include "crab/ebpf_domain.hpp"
#include "crab/var_registry.hpp"
#include "ir/unmarshal.hpp"

namespace prevail {

StringInvariant EbpfDomain::to_set() const { return rcp.to_set() + stack.to_set(); }

EbpfDomain EbpfDomain::top() {
    EbpfDomain abs;
    abs.set_to_top();
    return abs;
}

EbpfDomain EbpfDomain::bottom() {
    EbpfDomain abs;
    abs.set_to_bottom();
    return abs;
}

EbpfDomain::EbpfDomain() = default;

EbpfDomain::EbpfDomain(TypeToNumDomain rcp, ArrayDomain stack) : rcp(std::move(rcp)), stack(std::move(stack)) {}

void EbpfDomain::set_to_top() {
    rcp.set_to_top();
    stack.set_to_top();
}

void EbpfDomain::set_to_bottom() { rcp.set_to_bottom(); }

bool EbpfDomain::is_bottom() const { return rcp.is_bottom(); }

bool EbpfDomain::is_top() const { return rcp.is_top() && stack.is_top(); }

bool EbpfDomain::operator<=(const EbpfDomain& other) const {
    if (!(stack <= other.stack)) {
        return false;
    }
    return rcp <= other.rcp;
}

bool EbpfDomain::operator<=(EbpfDomain&& other) const {
    if (!(stack <= other.stack)) {
        return false;
    }
    return rcp <= std::move(other.rcp);
}

void EbpfDomain::operator|=(EbpfDomain&& other) {
    if (other.is_bottom()) {
        return;
    }
    if (is_bottom()) {
        *this = std::move(other);
        return;
    }
    stack |= std::move(other.stack);
    rcp |= std::move(other.rcp);
}

void EbpfDomain::operator|=(const EbpfDomain& other) {
    if (other.is_bottom()) {
        return;
    }
    if (is_bottom()) {
        *this = other;
        return;
    }
    stack |= other.stack;
    rcp |= other.rcp;
}

EbpfDomain EbpfDomain::operator|(EbpfDomain&& other) const {
    if (other.is_bottom()) {
        return *this;
    }
    if (is_bottom()) {
        return std::move(other);
    }
    other |= *this;
    return other;
}

EbpfDomain EbpfDomain::operator|(const EbpfDomain& other) const& {
    if (other.is_bottom()) {
        return *this;
    }
    if (is_bottom()) {
        return other;
    }
    EbpfDomain res{other};
    res |= *this;
    return res;
}

EbpfDomain EbpfDomain::operator|(const EbpfDomain& other) && {
    if (other.is_bottom()) {
        return std::move(*this);
    }
    if (is_bottom()) {
        return other;
    }
    *this |= other;
    return std::move(*this);
}

EbpfDomain EbpfDomain::operator&(const EbpfDomain& other) const {
    auto res = rcp & other.rcp;
    if (!res.is_bottom()) {
        return {std::move(res), stack & other.stack};
    }
    return bottom();
}

EbpfDomain EbpfDomain::calculate_constant_limits() {
    EbpfDomain inv;
    using namespace dsl_syntax;
    for (const int i : {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}) {
        const auto r = reg_pack(i);
        inv.add_value_constraint(r.svalue <= std::numeric_limits<int32_t>::max());
        inv.add_value_constraint(r.svalue >= std::numeric_limits<int32_t>::min());
        inv.add_value_constraint(r.uvalue <= std::numeric_limits<uint32_t>::max());
        inv.add_value_constraint(r.uvalue >= 0);
        inv.add_value_constraint(r.stack_offset <= EBPF_TOTAL_STACK_SIZE);
        inv.add_value_constraint(r.stack_offset >= 0);
        inv.add_value_constraint(r.shared_offset <= r.shared_region_size);
        inv.add_value_constraint(r.shared_offset >= 0);
        inv.add_value_constraint(r.packet_offset <= variable_registry->packet_size());
        inv.add_value_constraint(r.packet_offset >= 0);
        if (thread_local_options.cfg_opts.check_for_termination) {
            for (const Variable counter : variable_registry->get_loop_counters()) {
                inv.add_value_constraint(counter <= std::numeric_limits<int32_t>::max());
                inv.add_value_constraint(counter >= 0);
                inv.add_value_constraint(counter <= r.svalue);
            }
        }
    }
    return inv;
}

static const EbpfDomain constant_limits = EbpfDomain::calculate_constant_limits();

EbpfDomain EbpfDomain::widen(const EbpfDomain& other, const bool to_constants) const {
    EbpfDomain res{this->rcp.widen(other.rcp), stack.widen(other.stack)};

    if (to_constants) {
        return res & constant_limits;
    }
    return res;
}

EbpfDomain EbpfDomain::narrow(const EbpfDomain& other) const { return {rcp.narrow(other.rcp), stack & other.stack}; }

void EbpfDomain::add_value_constraint(const LinearConstraint& cst) { rcp.values.add_constraint(cst); }

void EbpfDomain::add_type_constraint(const LinearConstraint& cst) { rcp.types.add_constraint(cst); }

void EbpfDomain::havoc(const Variable var) {
    // TODO: type inv?
    rcp.values.havoc(var);
}

// Get the start and end of the range of possible map fd values.
// In the future, it would be cleaner to use a set rather than an interval
// for map fds.
bool EbpfDomain::get_map_fd_range(const Reg& map_fd_reg, int32_t* start_fd, int32_t* end_fd) const {
    const Interval& map_fd_interval = rcp.values.eval_interval(reg_pack(map_fd_reg).map_fd);
    const auto lb = map_fd_interval.lb().number();
    const auto ub = map_fd_interval.ub().number();
    if (!lb || !lb->fits<int32_t>() || !ub || !ub->fits<int32_t>()) {
        return false;
    }
    *start_fd = lb->narrow<int32_t>();
    *end_fd = ub->narrow<int32_t>();

    // Cap the maximum range we'll check.
    constexpr int max_range = 32;
    return *map_fd_interval.finite_size() < max_range;
}

// All maps in the range must have the same type for us to use it.
std::optional<uint32_t> EbpfDomain::get_map_type(const Reg& map_fd_reg) const {
    int32_t start_fd, end_fd;
    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {
        return {};
    }

    std::optional<uint32_t> type;
    for (int32_t map_fd = start_fd; map_fd <= end_fd; map_fd++) {
        EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd);
        if (map == nullptr) {
            return {};
        }
        if (!type.has_value()) {
            type = map->type;
        } else if (map->type != *type) {
            return {};
        }
    }
    return type;
}

// All maps in the range must have the same inner map fd for us to use it.
std::optional<uint32_t> EbpfDomain::get_map_inner_map_fd(const Reg& map_fd_reg) const {
    int start_fd, end_fd;
    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {
        return {};
    }

    std::optional<uint32_t> inner_map_fd;
    for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
        EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd);
        if (map == nullptr) {
            return {};
        }
        if (!inner_map_fd.has_value()) {
            inner_map_fd = map->inner_map_fd;
        } else if (map->type != *inner_map_fd) {
            return {};
        }
    }
    return inner_map_fd;
}

// We can deal with a range of key sizes.
Interval EbpfDomain::get_map_key_size(const Reg& map_fd_reg) const {
    int start_fd, end_fd;
    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {
        return Interval::top();
    }

    Interval result = Interval::bottom();
    for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
        if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {
            result = result | Interval{map->key_size};
        } else {
            return Interval::top();
        }
    }
    return result;
}

// We can deal with a range of value sizes.
Interval EbpfDomain::get_map_value_size(const Reg& map_fd_reg) const {
    int start_fd, end_fd;
    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {
        return Interval::top();
    }

    Interval result = Interval::bottom();
    for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
        if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {
            result = result | Interval(map->value_size);
        } else {
            return Interval::top();
        }
    }
    return result;
}

// We can deal with a range of max_entries values.
Interval EbpfDomain::get_map_max_entries(const Reg& map_fd_reg) const {
    int start_fd, end_fd;
    if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {
        return Interval::top();
    }

    Interval result = Interval::bottom();
    for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {
        if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {
            result = result | Interval(map->max_entries);
        } else {
            return Interval::top();
        }
    }
    return result;
}

ExtendedNumber EbpfDomain::get_loop_count_upper_bound() const {
    ExtendedNumber ub{0};
    for (const Variable counter : variable_registry->get_loop_counters()) {
        ub = std::max(ub, rcp.values.eval_interval(counter).ub());
    }
    return ub;
}

Interval EbpfDomain::get_r0() const { return rcp.values.eval_interval(reg_pack(R0_RETURN_VALUE).svalue); }

std::ostream& operator<<(std::ostream& o, const TypeDomain& dom) { return o << dom.inv; }

std::ostream& operator<<(std::ostream& o, const TypeToNumDomain& dom) {
    if (dom.is_bottom()) {
        o << "_|_";
    } else {
        o << dom.types << dom.values;
    }
    return o;
}

std::ostream& operator<<(std::ostream& o, const EbpfDomain& dom) {
    if (dom.is_bottom()) {
        o << "_|_";
    } else {
        o << dom.rcp << "\nStack: " << dom.stack;
    }
    return o;
}

void EbpfDomain::initialize_packet() {
    using namespace dsl_syntax;
    EbpfDomain& inv = *this;
    inv.havoc(variable_registry->packet_size());
    inv.havoc(variable_registry->meta_offset());

    inv.add_value_constraint(0 <= variable_registry->packet_size());
    inv.add_value_constraint(variable_registry->packet_size() < MAX_PACKET_SIZE);
    const auto info = *thread_local_program_info;
    if (info.type.context_descriptor->meta >= 0) {
        inv.add_value_constraint(variable_registry->meta_offset() <= 0);
        inv.add_value_constraint(variable_registry->meta_offset() >= -4098);
    } else {
        inv.rcp.values.assign(variable_registry->meta_offset(), 0);
    }
}

EbpfDomain EbpfDomain::from_constraints(const std::vector<LinearConstraint>& type_constraints,
                                        const std::vector<LinearConstraint>& value_constraints) {
    EbpfDomain inv;
    for (const auto& cst : type_constraints) {
        inv.add_type_constraint(cst);
    }
    for (const auto& cst : value_constraints) {
        inv.add_value_constraint(cst);
    }
    return inv;
}

EbpfDomain EbpfDomain::from_constraints(const std::set<std::string>& constraints, const bool setup_constraints) {
    EbpfDomain inv;
    if (setup_constraints) {
        inv = setup_entry(false);
    }
    auto numeric_ranges = std::vector<Interval>();
    auto [type_constraints, value_constraints] = parse_linear_constraints(constraints, numeric_ranges);
    for (const auto& cst : type_constraints) {
        inv.add_type_constraint(cst);
    }
    for (const auto& cst : value_constraints) {
        inv.add_value_constraint(cst);
    }
    for (const Interval& range : numeric_ranges) {
        const auto [start, ub] = range.pair<int64_t>();
        const int width = 1 + (ub - start);
        inv.stack.initialize_numbers(start, width);
    }
    // TODO: handle other stack type constraints
    return inv;
}

EbpfDomain EbpfDomain::setup_entry(const bool init_r1) {
    using namespace dsl_syntax;

    EbpfDomain inv;
    const auto r10 = reg_pack(R10_STACK_POINTER);
    constexpr Reg r10_reg{R10_STACK_POINTER};
    inv.rcp.values.add_constraint(EBPF_TOTAL_STACK_SIZE <= r10.svalue);
    inv.rcp.values.add_constraint(r10.svalue <= PTR_MAX);
    inv.rcp.values.assign(r10.stack_offset, EBPF_TOTAL_STACK_SIZE);
    // stack_numeric_size would be 0, but TOP has the same result
    // so no need to assign it.
    inv.rcp.types.assign_type(r10_reg, T_STACK);

    if (init_r1) {
        const auto r1 = reg_pack(R1_ARG);
        constexpr Reg r1_reg{R1_ARG};
        inv.rcp.values.add_constraint(1 <= r1.svalue);
        inv.rcp.values.add_constraint(r1.svalue <= PTR_MAX);
        inv.rcp.values.assign(r1.ctx_offset, 0);
        inv.rcp.types.assign_type(r1_reg, T_CTX);
    }

    inv.initialize_packet();
    return inv;
}

} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3
4	// This file is eBPF-specific, not derived from CRAB.
5
6	#include <optional>
7	#include <utility>
8	#include <vector>
9
10	#include "boost/endian/conversion.hpp"
11
12	#include "arith/dsl_syntax.hpp"
13	#include "config.hpp"
14	#include "crab/array_domain.hpp"
15	#include "crab/ebpf_domain.hpp"
16	#include "crab/var_registry.hpp"
17	#include "ir/unmarshal.hpp"
18
19	namespace prevail {
20
21	StringInvariant EbpfDomain::to_set() const { return rcp.to_set() + stack.to_set(); }	2,076✔
22
23	EbpfDomain EbpfDomain::top() {	×
24	EbpfDomain abs;	×
25	abs.set_to_top();	×
26	return abs;	×
27	}	×
28
29	EbpfDomain EbpfDomain::bottom() {	1,159,380✔
30	EbpfDomain abs;	1,739,070✔
31	abs.set_to_bottom();	1,739,070✔
32	return abs;	579,690✔
33	}
34
35	EbpfDomain::EbpfDomain() = default;	1,163,182✔
36
37	EbpfDomain::EbpfDomain(TypeToNumDomain rcp, ArrayDomain stack) : rcp(std::move(rcp)), stack(std::move(stack)) {}	122✔
38
39	void EbpfDomain::set_to_top() {	×
40	rcp.set_to_top();	×
41	stack.set_to_top();	×
42	}	×
43
44	void EbpfDomain::set_to_bottom() { rcp.set_to_bottom(); }	1,159,380✔
45
46	bool EbpfDomain::is_bottom() const { return rcp.is_bottom(); }	1,890,944✔
47
48	bool EbpfDomain::is_top() const { return rcp.is_top() && stack.is_top(); }	×
49
50	bool EbpfDomain::operator<=(const EbpfDomain& other) const {	502✔
51	if (!(stack <= other.stack)) {	502✔
52	return false;
53	}
54	return rcp <= other.rcp;	502✔
55	}
56
57	bool EbpfDomain::operator<=(EbpfDomain&& other) const {	×
58	if (!(stack <= other.stack)) {	×
59	return false;
60	}
61	return rcp <= std::move(other.rcp);	×
62	}
63
64	void EbpfDomain::operator\|=(EbpfDomain&& other) {	414,970✔
65	if (other.is_bottom()) {	414,970✔
66	return;	80,430✔
67	}
68	if (is_bottom()) {	254,110✔
69	*this = std::move(other);	237,090✔
70	return;	237,090✔
71	}
72	stack \|= std::move(other.stack);	17,020✔
73	rcp \|= std::move(other.rcp);	17,020✔
74	}
75
76	void EbpfDomain::operator\|=(const EbpfDomain& other) {	120✔
77	if (other.is_bottom()) {	120✔
78	return;
79	}
80	if (is_bottom()) {	120✔
81	*this = other;	×
82	return;	×
83	}
84	stack \|= other.stack;	120✔
85	rcp \|= other.rcp;	120✔
86	}
87
88	EbpfDomain EbpfDomain::operator\|(EbpfDomain&& other) const {	×
89	if (other.is_bottom()) {	×
90	return *this;	×
91	}
92	if (is_bottom()) {	×
93	return std::move(other);	×
94	}
95	other \|= *this;	×
96	return other;	×
97	}
98
99	EbpfDomain EbpfDomain::operator\|(const EbpfDomain& other) const& {	122✔
100	if (other.is_bottom()) {	122✔
101	return *this;	×
102	}
103	if (is_bottom()) {	122✔
104	return other;	2✔
105	}
106	EbpfDomain res{other};	120✔
107	res \|= *this;	120✔
108	return res;	120✔
109	}	120✔
110
111	EbpfDomain EbpfDomain::operator\|(const EbpfDomain& other) && {	×
112	if (other.is_bottom()) {	×
113	return std::move(*this);	×
114	}
115	if (is_bottom()) {	×
116	return other;	×
117	}
118	*this \|= other;	×
119	return std::move(*this);	×
120	}
121
122	EbpfDomain EbpfDomain::operator&(const EbpfDomain& other) const {	38✔
123	auto res = rcp & other.rcp;	38✔
124	if (!res.is_bottom()) {	38✔
125	return {std::move(res), stack & other.stack};	76✔
126	}
127	return bottom();	×
128	}	38✔
129
130	EbpfDomain EbpfDomain::calculate_constant_limits() {	446✔
131	EbpfDomain inv;	446✔
132	using namespace dsl_syntax;	223✔
133	for (const int i : {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}) {	4,906✔
134	const auto r = reg_pack(i);	4,460✔
135	inv.add_value_constraint(r.svalue <= std::numeric_limits<int32_t>::max());	6,690✔
136	inv.add_value_constraint(r.svalue >= std::numeric_limits<int32_t>::min());	6,690✔
137	inv.add_value_constraint(r.uvalue <= std::numeric_limits<uint32_t>::max());	6,690✔
138	inv.add_value_constraint(r.uvalue >= 0);	6,690✔
139	inv.add_value_constraint(r.stack_offset <= EBPF_TOTAL_STACK_SIZE);	6,690✔
140	inv.add_value_constraint(r.stack_offset >= 0);	6,690✔
141	inv.add_value_constraint(r.shared_offset <= r.shared_region_size);	6,690✔
142	inv.add_value_constraint(r.shared_offset >= 0);	6,690✔
143	inv.add_value_constraint(r.packet_offset <= variable_registry->packet_size());	6,690✔
144	inv.add_value_constraint(r.packet_offset >= 0);	6,690✔
145	if (thread_local_options.cfg_opts.check_for_termination) {	4,460✔
146	for (const Variable counter : variable_registry->get_loop_counters()) {	×
147	inv.add_value_constraint(counter <= std::numeric_limits<int32_t>::max());	×
148	inv.add_value_constraint(counter >= 0);	×
149	inv.add_value_constraint(counter <= r.svalue);	×
150	}	×
151	}
152	}
153	return inv;	446✔
154	}	×
155
156	static const EbpfDomain constant_limits = EbpfDomain::calculate_constant_limits();
157
158	EbpfDomain EbpfDomain::widen(const EbpfDomain& other, const bool to_constants) const {	84✔
159	EbpfDomain res{this->rcp.widen(other.rcp), stack.widen(other.stack)};	126✔
160
161	if (to_constants) {	84✔
162	return res & constant_limits;	38✔
163	}
164	return res;	46✔
165	}	84✔
166
167	EbpfDomain EbpfDomain::narrow(const EbpfDomain& other) const { return {rcp.narrow(other.rcp), stack & other.stack}; }	×
168
169	void EbpfDomain::add_value_constraint(const LinearConstraint& cst) { rcp.values.add_constraint(cst); }	51,090✔
170
171	void EbpfDomain::add_type_constraint(const LinearConstraint& cst) { rcp.types.add_constraint(cst); }	2,754✔
172
173	void EbpfDomain::havoc(const Variable var) {	2,424✔
174	// TODO: type inv?
175	rcp.values.havoc(var);	2,424✔
176	}	1,212✔
177
178	// Get the start and end of the range of possible map fd values.
179	// In the future, it would be cleaner to use a set rather than an interval
180	// for map fds.
181	bool EbpfDomain::get_map_fd_range(const Reg& map_fd_reg, int32_t* start_fd, int32_t* end_fd) const {	13,674✔
182	const Interval& map_fd_interval = rcp.values.eval_interval(reg_pack(map_fd_reg).map_fd);	13,674✔
183	const auto lb = map_fd_interval.lb().number();	27,348✔
184	const auto ub = map_fd_interval.ub().number();	27,348✔
185	if (!lb \|\| !lb->fits<int32_t>() \|\| !ub \|\| !ub->fits<int32_t>()) {	13,674✔
186	return false;
187	}
188	*start_fd = lb->narrow<int32_t>();	13,674✔
189	*end_fd = ub->narrow<int32_t>();	13,674✔
190
191	// Cap the maximum range we'll check.
192	constexpr int max_range = 32;	13,674✔
193	return *map_fd_interval.finite_size() < max_range;	13,674✔
194	}	20,511✔
195
196	// All maps in the range must have the same type for us to use it.
197	std::optional<uint32_t> EbpfDomain::get_map_type(const Reg& map_fd_reg) const {	6,836✔
198	int32_t start_fd, end_fd;	3,418✔
199	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	6,836✔
200	return {};	×
201	}
202
203	std::optional<uint32_t> type;	6,836✔
204	for (int32_t map_fd = start_fd; map_fd <= end_fd; map_fd++) {	13,708✔
205	EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd);	6,876✔
206	if (map == nullptr) {	6,876✔
207	return {};	×
208	}
209	if (!type.has_value()) {	6,876✔
210	type = map->type;	6,836✔
211	} else if (map->type != *type) {	40✔
212	return {};	4✔
213	}
214	}
215	return type;	6,832✔
216	}
217
218	// All maps in the range must have the same inner map fd for us to use it.
219	std::optional<uint32_t> EbpfDomain::get_map_inner_map_fd(const Reg& map_fd_reg) const {	32✔
220	int start_fd, end_fd;	16✔
221	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	32✔
222	return {};	×
223	}
224
225	std::optional<uint32_t> inner_map_fd;	32✔
226	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	64✔
227	EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd);	32✔
228	if (map == nullptr) {	32✔
229	return {};	×
230	}
231	if (!inner_map_fd.has_value()) {	32✔
232	inner_map_fd = map->inner_map_fd;	32✔
233	} else if (map->type != *inner_map_fd) {	×
234	return {};	×
235	}
236	}
237	return inner_map_fd;	32✔
238	}
239
240	// We can deal with a range of key sizes.
241	Interval EbpfDomain::get_map_key_size(const Reg& map_fd_reg) const {	3,492✔
242	int start_fd, end_fd;	1,746✔
243	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	3,492✔
244	return Interval::top();	×
245	}
246
247	Interval result = Interval::bottom();	3,492✔
248	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	7,004✔
249	if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {	3,512✔
250	result = result \| Interval{map->key_size};	7,024✔
251	} else {
252	return Interval::top();	×
253	}
254	}
255	return result;	3,492✔
256	}	3,492✔
257
258	// We can deal with a range of value sizes.
259	Interval EbpfDomain::get_map_value_size(const Reg& map_fd_reg) const {	3,310✔
260	int start_fd, end_fd;	1,655✔
261	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	3,310✔
262	return Interval::top();	×
263	}
264
265	Interval result = Interval::bottom();	3,310✔
266	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	6,638✔
267	if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {	3,328✔
268	result = result \| Interval(map->value_size);	6,656✔
269	} else {
270	return Interval::top();	×
271	}
272	}
273	return result;	3,310✔
274	}	3,310✔
275
276	// We can deal with a range of max_entries values.
277	Interval EbpfDomain::get_map_max_entries(const Reg& map_fd_reg) const {	4✔
278	int start_fd, end_fd;	2✔
279	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	4✔
280	return Interval::top();	×
281	}
282
283	Interval result = Interval::bottom();	4✔
284	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	8✔
285	if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {	4✔
286	result = result \| Interval(map->max_entries);	8✔
287	} else {
288	return Interval::top();	×
289	}
290	}
291	return result;	4✔
292	}	4✔
293
294	ExtendedNumber EbpfDomain::get_loop_count_upper_bound() const {	160✔
295	ExtendedNumber ub{0};	160✔
296	for (const Variable counter : variable_registry->get_loop_counters()) {	304✔
297	ub = std::max(ub, rcp.values.eval_interval(counter).ub());	414✔
298	}	80✔
299	return ub;	160✔
300	}	×
301
302	Interval EbpfDomain::get_r0() const { return rcp.values.eval_interval(reg_pack(R0_RETURN_VALUE).svalue); }	2,556✔
303
304	std::ostream& operator<<(std::ostream& o, const TypeDomain& dom) { return o << dom.inv; }	×
305
306	std::ostream& operator<<(std::ostream& o, const TypeToNumDomain& dom) {	×
307	if (dom.is_bottom()) {	×
308	o << "_\|_";	×
309	} else {
310	o << dom.types << dom.values;	×
311	}
312	return o;	×
313	}
314
315	std::ostream& operator<<(std::ostream& o, const EbpfDomain& dom) {	×
316	if (dom.is_bottom()) {	×
317	o << "_\|_";	×
318	} else {
319	o << dom.rcp << "\nStack: " << dom.stack;	×
320	}
321	return o;	×
322	}
323
324	void EbpfDomain::initialize_packet() {	1,212✔
325	using namespace dsl_syntax;	606✔
326	EbpfDomain& inv = *this;	1,212✔
327	inv.havoc(variable_registry->packet_size());	1,212✔
328	inv.havoc(variable_registry->meta_offset());	1,212✔
329
330	inv.add_value_constraint(0 <= variable_registry->packet_size());	2,424✔
331	inv.add_value_constraint(variable_registry->packet_size() < MAX_PACKET_SIZE);	1,818✔
332	const auto info = *thread_local_program_info;	1,212✔
333	if (info.type.context_descriptor->meta >= 0) {	1,212✔
334	inv.add_value_constraint(variable_registry->meta_offset() <= 0);	813✔
335	inv.add_value_constraint(variable_registry->meta_offset() >= -4098);	813✔
336	} else {
337	inv.rcp.values.assign(variable_registry->meta_offset(), 0);	1,005✔
338	}
339	}	1,212✔
340
341	EbpfDomain EbpfDomain::from_constraints(const std::vector<LinearConstraint>& type_constraints,	356✔
342	const std::vector<LinearConstraint>& value_constraints) {
343	EbpfDomain inv;	356✔
344	for (const auto& cst : type_constraints) {	798✔
345	inv.add_type_constraint(cst);	663✔
346	}
347	for (const auto& cst : value_constraints) {	880✔
348	inv.add_value_constraint(cst);	524✔
349	}
350	return inv;	356✔
351	}	×
352
353	EbpfDomain EbpfDomain::from_constraints(const std::set<std::string>& constraints, const bool setup_constraints) {	1,828✔
354	EbpfDomain inv;	1,828✔
355	if (setup_constraints) {	1,828✔
356	inv = setup_entry(false);	666✔
357	}
358	auto numeric_ranges = std::vector<Interval>();	1,828✔
359	auto [type_constraints, value_constraints] = parse_linear_constraints(constraints, numeric_ranges);	1,828✔
360	for (const auto& cst : type_constraints) {	4,140✔
361	inv.add_type_constraint(cst);	3,468✔
362	}
363	for (const auto& cst : value_constraints) {	7,810✔
364	inv.add_value_constraint(cst);	5,982✔
365	}
366	for (const Interval& range : numeric_ranges) {	2,090✔
367	const auto [start, ub] = range.pair<int64_t>();	262✔
368	const int width = 1 + (ub - start);	262✔
369	inv.stack.initialize_numbers(start, width);	262✔
370	}
371	// TODO: handle other stack type constraints
372	return inv;	3,656✔
373	}	1,828✔
374
375	EbpfDomain EbpfDomain::setup_entry(const bool init_r1) {	1,172✔
376	using namespace dsl_syntax;	586✔
377
378	EbpfDomain inv;	1,172✔
379	const auto r10 = reg_pack(R10_STACK_POINTER);	1,172✔
380	constexpr Reg r10_reg{R10_STACK_POINTER};	1,172✔
381	inv.rcp.values.add_constraint(EBPF_TOTAL_STACK_SIZE <= r10.svalue);	2,344✔
382	inv.rcp.values.add_constraint(r10.svalue <= PTR_MAX);	1,758✔
383	inv.rcp.values.assign(r10.stack_offset, EBPF_TOTAL_STACK_SIZE);	1,172✔
384	// stack_numeric_size would be 0, but TOP has the same result
385	// so no need to assign it.
386	inv.rcp.types.assign_type(r10_reg, T_STACK);	1,172✔
387
388	if (init_r1) {	1,172✔
389	const auto r1 = reg_pack(R1_ARG);	728✔
390	constexpr Reg r1_reg{R1_ARG};	728✔
391	inv.rcp.values.add_constraint(1 <= r1.svalue);	1,456✔
392	inv.rcp.values.add_constraint(r1.svalue <= PTR_MAX);	1,092✔
393	inv.rcp.values.assign(r1.ctx_offset, 0);	728✔
394	inv.rcp.types.assign_type(r1_reg, T_CTX);	1,092✔
395	}
396
397	inv.initialize_packet();	1,172✔
398	return inv;	1,758✔
399	}	×
400
401	} // 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