15194704016

Committed 22 May 2025 08:53AM UTC coverage: 88.11% (-0.07%) from 88.177%

Build # 15194704016

Build Type

push

github

Committed by

elazarg

Commit Message

uniform class names and explicit constructors for adapt_sgraph.hpp

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

Run Details

27 of 30 new or added lines in 1 file covered. (90.0%)

481 existing lines in 33 files now uncovered.

8552 of 9706 relevant lines covered (88.11%)

9089054.61 hits per line

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

75.68

/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 "asm_unmarshal.hpp"
#include "config.hpp"
#include "crab/array_domain.hpp"
#include "crab/dsl_syntax.hpp"
#include "crab/ebpf_domain.hpp"
#include "string_constraints.hpp"

namespace prevail {

std::optional<Variable> EbpfDomain::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:
    case T_MAP_PROGRAMS: return r.map_fd;
    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> EbpfDomain::get_type_offset_variable(const Reg& reg, const NumAbsDomain& inv) const {
    return get_type_offset_variable(reg, type_inv.get_type(inv, reg_pack(reg).type));
}

std::optional<Variable> EbpfDomain::get_type_offset_variable(const Reg& reg) const {
    return get_type_offset_variable(reg, m_inv);
}

StringInvariant EbpfDomain::to_set() const { return m_inv.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() : m_inv(NumAbsDomain::top()) {}

EbpfDomain::EbpfDomain(NumAbsDomain inv, ArrayDomain stack) : m_inv(std::move(inv)), stack(std::move(stack)) {}

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

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

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

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

bool EbpfDomain::operator<=(const EbpfDomain& other) const { return m_inv <= other.m_inv && stack <= other.stack; }

bool EbpfDomain::operator==(const EbpfDomain& other) const {
    return stack == other.stack && m_inv <= other.m_inv && other.m_inv <= m_inv;
}

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

    type_inv.selectively_join_based_on_type(m_inv, std::move(other.m_inv));

    stack |= std::move(other.stack);
}

void EbpfDomain::operator|=(const EbpfDomain& other) {
    EbpfDomain tmp{other};
    operator|=(std::move(tmp));
}

EbpfDomain EbpfDomain::operator|(EbpfDomain&& other) const {
    return EbpfDomain(m_inv | std::move(other.m_inv), stack | other.stack);
}

EbpfDomain EbpfDomain::operator|(const EbpfDomain& other) const& {
    return EbpfDomain(m_inv | other.m_inv, stack | other.stack);
}

EbpfDomain EbpfDomain::operator|(const EbpfDomain& other) && {
    return EbpfDomain(other.m_inv | std::move(m_inv), other.stack | stack);
}

EbpfDomain EbpfDomain::operator&(const EbpfDomain& other) const {
    return EbpfDomain(m_inv & other.m_inv, stack & other.stack);
}

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_constraint(r.svalue <= std::numeric_limits<int32_t>::max());
        inv.add_constraint(r.svalue >= std::numeric_limits<int32_t>::min());
        inv.add_constraint(r.uvalue <= std::numeric_limits<uint32_t>::max());
        inv.add_constraint(r.uvalue >= 0);
        inv.add_constraint(r.stack_offset <= EBPF_TOTAL_STACK_SIZE);
        inv.add_constraint(r.stack_offset >= 0);
        inv.add_constraint(r.shared_offset <= r.shared_region_size);
        inv.add_constraint(r.shared_offset >= 0);
        inv.add_constraint(r.packet_offset <= Variable::packet_size());
        inv.add_constraint(r.packet_offset >= 0);
        if (thread_local_options.cfg_opts.check_for_termination) {
            for (const Variable counter : Variable::get_loop_counters()) {
                inv.add_constraint(counter <= std::numeric_limits<int32_t>::max());
                inv.add_constraint(counter >= 0);
                inv.add_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{m_inv.widen(other.m_inv), stack | other.stack};
    if (to_constants) {
        return res & constant_limits;
    }
    return res;
}

EbpfDomain EbpfDomain::widening_thresholds(const EbpfDomain& other, const Thresholds&) const {
    return widen(other, false);
}

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

void EbpfDomain::add_constraint(const LinearConstraint& cst) { m_inv.add_constraint(cst); }

void EbpfDomain::havoc(const Variable var) { m_inv.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 = m_inv.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>();
    }

    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 std::optional<uint32_t>();
        }
        if (!type.has_value()) {
            type = map->type;
        } else if (map->type != *type) {
            return std::optional<uint32_t>();
        }
    }
    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::get_loop_counters()) {
        ub = std::max(ub, m_inv.eval_interval(counter).ub());
    }
    return ub;
}

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

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

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

    inv.add_constraint(0 <= Variable::packet_size());
    inv.add_constraint(Variable::packet_size() < MAX_PACKET_SIZE);
    const auto info = *thread_local_program_info;
    if (info.type.context_descriptor->meta >= 0) {
        inv.add_constraint(Variable::meta_offset() <= 0);
        inv.add_constraint(Variable::meta_offset() >= -4098);
    } else {
        inv.m_inv.assign(Variable::meta_offset(), 0);
    }
}

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>();
    for (const auto& cst : parse_linear_constraints(constraints, numeric_ranges)) {
        inv.add_constraint(cst);
    }
    for (const Interval& range : numeric_ranges) {
        const int start = range.lb().narrow<int>();
        const int width = 1 + range.finite_size()->narrow<int>();
        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.m_inv.add_constraint(EBPF_TOTAL_STACK_SIZE <= r10.svalue);
    inv.m_inv.add_constraint(r10.svalue <= PTR_MAX);
    inv.m_inv.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.type_inv.assign_type(inv.m_inv, r10_reg, T_STACK);

    if (init_r1) {
        const auto r1 = reg_pack(R1_ARG);
        constexpr Reg r1_reg{R1_ARG};
        inv.m_inv.add_constraint(1 <= r1.svalue);
        inv.m_inv.add_constraint(r1.svalue <= PTR_MAX);
        inv.m_inv.assign(r1.ctx_offset, 0);
        inv.type_inv.assign_type(inv.m_inv, 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 "asm_unmarshal.hpp"
13	#include "config.hpp"
14	#include "crab/array_domain.hpp"
15	#include "crab/dsl_syntax.hpp"
16	#include "crab/ebpf_domain.hpp"
17	#include "string_constraints.hpp"
18
19	namespace prevail {
20
21	std::optional<Variable> EbpfDomain::get_type_offset_variable(const Reg& reg, const int type) {	31,134✔
22	RegPack r = reg_pack(reg);	31,134✔
23	switch (type) {	31,134✔
24	case T_CTX: return r.ctx_offset;	22✔
25	case T_MAP:	22✔
26	case T_MAP_PROGRAMS: return r.map_fd;	22✔
27	case T_PACKET: return r.packet_offset;	5,832✔
28	case T_SHARED: return r.shared_offset;	172✔
29	case T_STACK: return r.stack_offset;	20,182✔
30	default: return {};	4,904✔
31	}
32	}
33
34	std::optional<Variable> EbpfDomain::get_type_offset_variable(const Reg& reg, const NumAbsDomain& inv) const {	25,932✔
35	return get_type_offset_variable(reg, type_inv.get_type(inv, reg_pack(reg).type));	25,932✔
36	}
37
38	std::optional<Variable> EbpfDomain::get_type_offset_variable(const Reg& reg) const {	25,932✔
39	return get_type_offset_variable(reg, m_inv);	25,932✔
40	}
41
42	StringInvariant EbpfDomain::to_set() const { return m_inv.to_set() + stack.to_set(); }	2,094✔
43
UNCOV 44	EbpfDomain EbpfDomain::top() {	×
45	EbpfDomain abs;	×
46	abs.set_to_top();	×
47	return abs;	×
48	}	×
49
50	EbpfDomain EbpfDomain::bottom() {	1,021,632✔
51	EbpfDomain abs;	1,021,632✔
52	abs.set_to_bottom();	1,532,448✔
53	return abs;	1,021,632✔
54	}
55
56	EbpfDomain::EbpfDomain() : m_inv(NumAbsDomain::top()) {}	1,025,012✔
57
58	EbpfDomain::EbpfDomain(NumAbsDomain inv, ArrayDomain stack) : m_inv(std::move(inv)), stack(std::move(stack)) {}	160✔
59
UNCOV 60	void EbpfDomain::set_to_top() {	×
UNCOV 61	m_inv.set_to_top();	×
62	stack.set_to_top();	×
63	}	×
64
65	void EbpfDomain::set_to_bottom() { m_inv.set_to_bottom(); }	1,021,632✔
66
67	bool EbpfDomain::is_bottom() const { return m_inv.is_bottom(); }	1,393,140✔
68
UNCOV 69	bool EbpfDomain::is_top() const { return m_inv.is_top() && stack.is_top(); }	×
70
71	bool EbpfDomain::operator<=(const EbpfDomain& other) const { return m_inv <= other.m_inv && stack <= other.stack; }	198✔
72
UNCOV 73	bool EbpfDomain::operator==(const EbpfDomain& other) const {	×
UNCOV 74	return stack == other.stack && m_inv <= other.m_inv && other.m_inv <= m_inv;	×
75	}
76
77	void EbpfDomain::operator\|=(EbpfDomain&& other) {	364,628✔
78	if (is_bottom()) {	364,628✔
79	*this = std::move(other);	339,706✔
80	return;	339,706✔
81	}
82	if (other.is_bottom()) {	24,922✔
83	return;	345✔
84	}
85
86	type_inv.selectively_join_based_on_type(m_inv, std::move(other.m_inv));	24,232✔
87
88	stack \|= std::move(other.stack);	24,232✔
89	}
90
UNCOV 91	void EbpfDomain::operator\|=(const EbpfDomain& other) {	×
UNCOV 92	EbpfDomain tmp{other};	×
UNCOV 93	operator\|=(std::move(tmp));	×
UNCOV 94	}	×
95
96	EbpfDomain EbpfDomain::operator\|(EbpfDomain&& other) const {	×
97	return EbpfDomain(m_inv \| std::move(other.m_inv), stack \| other.stack);	×
98	}
99
100	EbpfDomain EbpfDomain::operator\|(const EbpfDomain& other) const& {	38✔
101	return EbpfDomain(m_inv \| other.m_inv, stack \| other.stack);	57✔
102	}
103
UNCOV 104	EbpfDomain EbpfDomain::operator\|(const EbpfDomain& other) && {	×
UNCOV 105	return EbpfDomain(other.m_inv \| std::move(m_inv), other.stack \| stack);	×
106	}
107
108	EbpfDomain EbpfDomain::operator&(const EbpfDomain& other) const {	38✔
109	return EbpfDomain(m_inv & other.m_inv, stack & other.stack);	57✔
110	}
111
112	EbpfDomain EbpfDomain::calculate_constant_limits() {	440✔
113	EbpfDomain inv;	440✔
114	using namespace dsl_syntax;	220✔
115	for (const int i : {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}) {	4,840✔
116	const auto r = reg_pack(i);	4,400✔
117	inv.add_constraint(r.svalue <= std::numeric_limits<int32_t>::max());	6,600✔
118	inv.add_constraint(r.svalue >= std::numeric_limits<int32_t>::min());	6,600✔
119	inv.add_constraint(r.uvalue <= std::numeric_limits<uint32_t>::max());	6,600✔
120	inv.add_constraint(r.uvalue >= 0);	6,600✔
121	inv.add_constraint(r.stack_offset <= EBPF_TOTAL_STACK_SIZE);	6,600✔
122	inv.add_constraint(r.stack_offset >= 0);	6,600✔
123	inv.add_constraint(r.shared_offset <= r.shared_region_size);	6,600✔
124	inv.add_constraint(r.shared_offset >= 0);	6,600✔
125	inv.add_constraint(r.packet_offset <= Variable::packet_size());	6,600✔
126	inv.add_constraint(r.packet_offset >= 0);	6,600✔
127	if (thread_local_options.cfg_opts.check_for_termination) {	4,400✔
UNCOV 128	for (const Variable counter : Variable::get_loop_counters()) {	×
UNCOV 129	inv.add_constraint(counter <= std::numeric_limits<int32_t>::max());	×
UNCOV 130	inv.add_constraint(counter >= 0);	×
UNCOV 131	inv.add_constraint(counter <= r.svalue);	×
132	}	×
133	}
134	}
135	return inv;	440✔
136	}	×
137
138	static const EbpfDomain constant_limits = EbpfDomain::calculate_constant_limits();
139
140	EbpfDomain EbpfDomain::widen(const EbpfDomain& other, const bool to_constants) const {	84✔
141	EbpfDomain res{m_inv.widen(other.m_inv), stack \| other.stack};	126✔
142	if (to_constants) {	84✔
143	return res & constant_limits;	38✔
144	}
145	return res;	46✔
146	}	84✔
147
UNCOV 148	EbpfDomain EbpfDomain::widening_thresholds(const EbpfDomain& other, const Thresholds&) const {	×
UNCOV 149	return widen(other, false);	×
150	}
151
152	EbpfDomain EbpfDomain::narrow(const EbpfDomain& other) const {	×
153	return EbpfDomain(m_inv.narrow(other.m_inv), stack & other.stack);	×
154	}
155
156	void EbpfDomain::add_constraint(const LinearConstraint& cst) { m_inv.add_constraint(cst); }	51,193✔
157
158	void EbpfDomain::havoc(const Variable var) { m_inv.havoc(var); }	2,296✔
159
160	// Get the start and end of the range of possible map fd values.
161	// In the future, it would be cleaner to use a set rather than an interval
162	// for map fds.
163	bool EbpfDomain::get_map_fd_range(const Reg& map_fd_reg, int32_t* start_fd, int32_t* end_fd) const {	13,198✔
164	const Interval& map_fd_interval = m_inv.eval_interval(reg_pack(map_fd_reg).map_fd);	13,198✔
165	const auto lb = map_fd_interval.lb().number();	26,396✔
166	const auto ub = map_fd_interval.ub().number();	26,396✔
167	if (!lb \|\| !lb->fits<int32_t>() \|\| !ub \|\| !ub->fits<int32_t>()) {	13,198✔
168	return false;	1✔
169	}
170	*start_fd = lb->narrow<int32_t>();	13,196✔
171	*end_fd = ub->narrow<int32_t>();	13,196✔
172
173	// Cap the maximum range we'll check.
174	constexpr int max_range = 32;	13,196✔
175	return *map_fd_interval.finite_size() < max_range;	13,196✔
176	}	19,797✔
177
178	// All maps in the range must have the same type for us to use it.
179	std::optional<uint32_t> EbpfDomain::get_map_type(const Reg& map_fd_reg) const {	6,600✔
180	int32_t start_fd, end_fd;	3,300✔
181	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	6,600✔
182	return std::optional<uint32_t>();	2✔
183	}
184
185	std::optional<uint32_t> type;	6,598✔
186	for (int32_t map_fd = start_fd; map_fd <= end_fd; map_fd++) {	13,198✔
187	EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd);	6,604✔
188	if (map == nullptr) {	6,602✔
189	return std::optional<uint32_t>();	×
190	}
191	if (!type.has_value()) {	6,602✔
192	type = map->type;	6,596✔
193	} else if (map->type != *type) {	6✔
194	return std::optional<uint32_t>();	2✔
195	}
196	}
197	return type;	6,594✔
198	}
199
200	// All maps in the range must have the same inner map fd for us to use it.
201	std::optional<uint32_t> EbpfDomain::get_map_inner_map_fd(const Reg& map_fd_reg) const {	34✔
202	int start_fd, end_fd;	17✔
203	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	34✔
204	return {};	×
205	}
206
207	std::optional<uint32_t> inner_map_fd;	34✔
208	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	68✔
209	EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd);	34✔
210	if (map == nullptr) {	34✔
211	return {};	×
212	}
213	if (!inner_map_fd.has_value()) {	34✔
214	inner_map_fd = map->inner_map_fd;	34✔
215	} else if (map->type != *inner_map_fd) {	×
216	return {};	×
217	}
218	}
219	return inner_map_fd;	34✔
220	}
221
222	// We can deal with a range of key sizes.
223	Interval EbpfDomain::get_map_key_size(const Reg& map_fd_reg) const {	1,998✔
224	int start_fd, end_fd;	999✔
225	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	1,998✔
226	return Interval::top();	×
227	}
228
229	Interval result = Interval::bottom();	1,998✔
230	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	3,998✔
231	if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {	2,000✔
232	result = result \| Interval{map->key_size};	4,000✔
233	} else {
234	return Interval::top();	×
235	}
236	}
237	return result;	1,998✔
238	}	1,998✔
239
240	// We can deal with a range of value sizes.
241	Interval EbpfDomain::get_map_value_size(const Reg& map_fd_reg) const {	4,562✔
242	int start_fd, end_fd;	2,281✔
243	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	4,562✔
244	return Interval::top();	×
245	}
246
247	Interval result = Interval::bottom();	4,562✔
248	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	9,126✔
249	if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {	4,564✔
250	result = result \| Interval(map->value_size);	9,128✔
251	} else {
252	return Interval::top();	×
253	}
254	}
255	return result;	4,562✔
256	}	4,562✔
257
258	// We can deal with a range of max_entries values.
259	Interval EbpfDomain::get_map_max_entries(const Reg& map_fd_reg) const {	4✔
260	int start_fd, end_fd;	2✔
261	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	4✔
262	return Interval::top();	×
263	}
264
265	Interval result = Interval::bottom();	4✔
266	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	8✔
267	if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {	4✔
268	result = result \| Interval(map->max_entries);	8✔
269	} else {
270	return Interval::top();	×
271	}
272	}
273	return result;	4✔
274	}	4✔
275
276	ExtendedNumber EbpfDomain::get_loop_count_upper_bound() const {	×
277	ExtendedNumber ub{0};	×
278	for (const Variable counter : Variable::get_loop_counters()) {	×
279	ub = std::max(ub, m_inv.eval_interval(counter).ub());	×
280	}	×
281	return ub;	×
282	}	×
283
284	Interval EbpfDomain::get_r0() const { return m_inv.eval_interval(reg_pack(R0_RETURN_VALUE).svalue); }	438✔
285
286	std::ostream& operator<<(std::ostream& o, const EbpfDomain& dom) {	×
287	if (dom.is_bottom()) {	×
288	o << "_\|_";	×
289	} else {
290	o << dom.m_inv << "\nStack: " << dom.stack;	×
291	}
292	return o;	×
293	}
294
295	void EbpfDomain::initialize_packet() {	1,148✔
296	using namespace dsl_syntax;	574✔
297	EbpfDomain& inv = *this;	1,148✔
298	inv.havoc(Variable::packet_size());	1,148✔
299	inv.havoc(Variable::meta_offset());	1,148✔
300
301	inv.add_constraint(0 <= Variable::packet_size());	2,296✔
302	inv.add_constraint(Variable::packet_size() < MAX_PACKET_SIZE);	1,722✔
303	const auto info = *thread_local_program_info;	1,148✔
304	if (info.type.context_descriptor->meta >= 0) {	1,148✔
305	inv.add_constraint(Variable::meta_offset() <= 0);	738✔
306	inv.add_constraint(Variable::meta_offset() >= -4098);	738✔
307	} else {
308	inv.m_inv.assign(Variable::meta_offset(), 0);	984✔
309	}
310	}	1,148✔
311
312	EbpfDomain EbpfDomain::from_constraints(const std::set<std::string>& constraints, const bool setup_constraints) {	1,834✔
313	EbpfDomain inv;	1,834✔
314	if (setup_constraints) {	1,834✔
315	inv = setup_entry(false);	438✔
316	}
317	auto numeric_ranges = std::vector<Interval>();	1,834✔
318	for (const auto& cst : parse_linear_constraints(constraints, numeric_ranges)) {	10,152✔
319	inv.add_constraint(cst);	8,318✔
320	}	1,834✔
321	for (const Interval& range : numeric_ranges) {	2,090✔
322	const int start = range.lb().narrow<int>();	384✔
323	const int width = 1 + range.finite_size()->narrow<int>();	256✔
324	inv.stack.initialize_numbers(start, width);	256✔
325	}
326	// TODO: handle other stack type constraints
327	return inv;	2,751✔
328	}	1,834✔
329
330	EbpfDomain EbpfDomain::setup_entry(const bool init_r1) {	1,106✔
331	using namespace dsl_syntax;	553✔
332
333	EbpfDomain inv;	1,106✔
334	const auto r10 = reg_pack(R10_STACK_POINTER);	1,106✔
335	constexpr Reg r10_reg{R10_STACK_POINTER};	1,106✔
336	inv.m_inv.add_constraint(EBPF_TOTAL_STACK_SIZE <= r10.svalue);	2,212✔
337	inv.m_inv.add_constraint(r10.svalue <= PTR_MAX);	1,659✔
338	inv.m_inv.assign(r10.stack_offset, EBPF_TOTAL_STACK_SIZE);	1,106✔
339	// stack_numeric_size would be 0, but TOP has the same result
340	// so no need to assign it.
341	inv.type_inv.assign_type(inv.m_inv, r10_reg, T_STACK);	1,106✔
342
343	if (init_r1) {	1,106✔
344	const auto r1 = reg_pack(R1_ARG);	667✔
345	constexpr Reg r1_reg{R1_ARG};	667✔
346	inv.m_inv.add_constraint(1 <= r1.svalue);	1,333✔
347	inv.m_inv.add_constraint(r1.svalue <= PTR_MAX);	1,000✔
348	inv.m_inv.assign(r1.ctx_offset, 0);	667✔
349	inv.type_inv.assign_type(inv.m_inv, r1_reg, T_CTX);	1,000✔
350	}
351
352	inv.initialize_packet();	1,106✔
353	return inv;	1,659✔
354	}	×
355
356	} // namespace prevail

Alan-Jowett / ebpf-verifier / 15194704016

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