22316701280

Committed 22 Feb 2026 08:43PM UTC coverage: 88.93% (+0.9%) from 88.002%

Build # 22316701280

Build Type

push

github

Committed by

web-flow

Commit Message

Human-friendly CLI output for bin/prevail (#1042)

* Replace CSV output with human-friendly PASS/FAIL CLI output

The default output was `{0|1},{seconds},{memory_kb}` — a CSV row for
benchmarking scripts that is unfriendly for humans. Benchmarking is
better done externally (time, /usr/bin/time -v).

New output: `PASS: section/function` or `FAIL: section/function` with
the first error and a hint line pointing to --failure-slice / -v.
Add -q/--quiet (exit code only) and --cfg (replaces --domain cfg).

Remove dead code: --domain option (linux, stats, zoneCrab selectors),
linux_verifier, memsize helpers, collect_stats/stats_headers, fnv1a64,
@headers special filename, bin/check alias, and stale benchmark scripts.

Move src/main/check.cpp → src/main.cpp (simplified, rewritten).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

* Graduate loop3.o from skip to expected failure

The >4x performance improvement means loop3.o no longer hangs.
It now completes quickly but is rejected due to type precision
loss through the loop join (VerifierTypeTracking).

* Remove redundant install exclude, fix doc path

- Remove `PATTERN "main.cpp" EXCLUDE` from install — the glob only
  matches *.hpp/*.h so main.cpp would never be included anyway.
- Fix `./prevail` → `./bin/prevail` in docs/architecture.md for
  consistency with the actual binary location.

---------

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Coverage Stats

1 of 1 new or added line in 1 file covered. (100.0%)

198 existing lines in 11 files now uncovered.

13159 of 14797 relevant lines covered (88.93%)

4658715.43 hits per line

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

80.93

/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 "crab_utils/lazy_allocator.hpp"
#include "ir/unmarshal.hpp"

namespace prevail {

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

std::optional<int64_t> EbpfDomain::get_stack_offset(const Reg& reg) const {
    // Only return an offset when the register is *definitely* a stack pointer,
    // not just possibly one. This ensures we don't misclassify memory deps.
    if (state.get_type(reg) != T_STACK) {
        return std::nullopt;
    }
    const auto offset = state.values.eval_interval(reg_pack(reg).stack_offset);
    if (const auto singleton = offset.singleton()) {
        return singleton->cast_to<int64_t>();
    }
    return std::nullopt;
}

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 state, ArrayDomain stack) : state(std::move(state)), stack(std::move(stack)) {}

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

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

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

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

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

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

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

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

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 = state & other.state;
    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;
}

// Lazy init via LazyAllocator<EbpfDomain, EbpfDomain::calculate_constant_limits> ensures
// thread_local_options and variable_registry are populated before EbpfDomain::calculate_constant_limits
// captures their state. LazyAllocator::get() has no reentrancy guard, but calculate_constant_limits
// does not call get_constant_limits() or widen(to_constants=true), so recursion cannot occur.
// Clamping via intersection (operator&) is sound because it only shrinks the domain by tightening
// constraints element-wise, preserving the over-approximation required for soundness.
static thread_local LazyAllocator<EbpfDomain, EbpfDomain::calculate_constant_limits> constant_limits;

static const EbpfDomain& get_constant_limits() { return constant_limits.get(); }

void EbpfDomain::clear_thread_local_state() { constant_limits.clear(); }

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

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

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

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

void EbpfDomain::havoc(const Variable var) {
    // TODO: type inv?
    state.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 = state.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, state.values.eval_interval(counter).ub());
    }
    return ub;
}

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

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.state << "\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.state.values.assign(variable_registry->meta_offset(), 0);
    }
}

EbpfDomain EbpfDomain::from_constraints(const std::vector<std::pair<Variable, TypeSet>>& type_restrictions,
                                        const std::vector<LinearConstraint>& value_constraints) {
    EbpfDomain inv;

    for (const auto& [var, ts] : type_restrictions) {
        inv.state.types.restrict_to(var, ts);
    }
    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_equalities, type_restrictions, value_constraints] =
        parse_linear_constraints(constraints, numeric_ranges);
    for (const auto& [v1, v2] : type_equalities) {
        inv.state.assume_eq_types(v1, v2);
    }
    for (const auto& [var, ts] : type_restrictions) {
        inv.state.types.restrict_to(var, ts);
    }
    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 = gsl::narrow<int>(1 + (ub - start));
        inv.stack.initialize_numbers(gsl::narrow<int>(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.state.values.add_constraint(EBPF_TOTAL_STACK_SIZE <= r10.svalue);
    inv.state.values.add_constraint(r10.svalue <= PTR_MAX);
    inv.state.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.state.assign_type(r10_reg, T_STACK);

    if (init_r1) {
        const auto r1 = reg_pack(R1_ARG);
        constexpr Reg r1_reg{R1_ARG};
        inv.state.values.add_constraint(1 <= r1.svalue);
        inv.state.values.add_constraint(r1.svalue <= PTR_MAX);
        inv.state.values.assign(r1.ctx_offset, 0);
        inv.state.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 "crab_utils/lazy_allocator.hpp"
18	#include "ir/unmarshal.hpp"
19
20	namespace prevail {
21
22	StringInvariant EbpfDomain::to_set() const { return state.to_set() + stack.to_set(); }	2,148✔
23
24	std::optional<int64_t> EbpfDomain::get_stack_offset(const Reg& reg) const {	34✔
25	// Only return an offset when the register is definitely a stack pointer,
26	// not just possibly one. This ensures we don't misclassify memory deps.
27	if (state.get_type(reg) != T_STACK) {	34✔
28	return std::nullopt;	32✔
29	}
30	const auto offset = state.values.eval_interval(reg_pack(reg).stack_offset);	2✔
31	if (const auto singleton = offset.singleton()) {	2✔
32	return singleton->cast_to<int64_t>();	×
33	}
34	return std::nullopt;	2✔
35	}
36
37	EbpfDomain EbpfDomain::top() {	8✔
38	EbpfDomain abs;	12✔
39	abs.set_to_top();	8✔
40	return abs;	8✔
41	}	×
42
43	EbpfDomain EbpfDomain::bottom() {	4,018,972✔
44	EbpfDomain abs;	6,028,458✔
45	abs.set_to_bottom();	6,028,457✔
46	return abs;	2,009,487✔
47	}
48
49	EbpfDomain::EbpfDomain() = default;	4,024,065✔
50
51	EbpfDomain::EbpfDomain(TypeToNumDomain state, ArrayDomain stack) : state(std::move(state)), stack(std::move(stack)) {}	240✔
52
53	void EbpfDomain::set_to_top() {	8✔
54	state.set_to_top();	8✔
55	stack.set_to_top();	8✔
56	}	8✔
57
58	void EbpfDomain::set_to_bottom() { state.set_to_bottom(); }	4,018,972✔
59
60	bool EbpfDomain::is_bottom() const { return state.is_bottom(); }	6,545,856✔
61
62	bool EbpfDomain::is_top() const { return state.is_top() && stack.is_top(); }	×
63
64	bool EbpfDomain::operator<=(const EbpfDomain& other) const {	710✔
65	if (!(stack <= other.stack)) {	710✔
66	return false;	1✔
67	}
68	return state <= other.state;	708✔
69	}
70
71	bool EbpfDomain::operator<=(EbpfDomain&& other) const {	×
72	if (!(stack <= other.stack)) {	×
73	return false;
74	}
75	return state <= std::move(other.state);	×
76	}
77
78	void EbpfDomain::operator\|=(EbpfDomain&& other) {	1,396,424✔
79	if (other.is_bottom()) {	1,396,424✔
80	return;	223,626✔
81	}
82	if (is_bottom()) {	949,172✔
83	*this = std::move(other);	886,564✔
84	return;	886,564✔
85	}
86	stack \|= std::move(other.stack);	62,608✔
87	state \|= std::move(other.state);	62,608✔
88	}
89
90	void EbpfDomain::operator\|=(const EbpfDomain& other) {	154✔
91	if (other.is_bottom()) {	154✔
92	return;
93	}
94	if (is_bottom()) {	154✔
95	*this = other;	×
96	return;	×
97	}
98	stack \|= other.stack;	154✔
99	state \|= other.state;	154✔
100	}
101
102	EbpfDomain EbpfDomain::operator\|(EbpfDomain&& other) const {	×
103	if (other.is_bottom()) {	×
104	return *this;	×
105	}
106	if (is_bottom()) {	×
107	return std::move(other);	×
108	}
109	other \|= *this;	×
110	return other;	×
111	}
112
113	EbpfDomain EbpfDomain::operator\|(const EbpfDomain& other) const& {	156✔
114	if (other.is_bottom()) {	156✔
115	return *this;	×
116	}
117	if (is_bottom()) {	156✔
118	return other;	2✔
119	}
120	EbpfDomain res{other};	154✔
121	res \|= *this;	154✔
122	return res;	154✔
123	}	154✔
124
125	EbpfDomain EbpfDomain::operator\|(const EbpfDomain& other) && {	×
126	if (other.is_bottom()) {	×
127	return std::move(*this);	×
128	}
129	if (is_bottom()) {	×
130	return other;	×
131	}
132	*this \|= other;	×
133	return std::move(*this);	×
134	}
135
136	EbpfDomain EbpfDomain::operator&(const EbpfDomain& other) const {	80✔
137	auto res = state & other.state;	80✔
138	if (!res.is_bottom()) {	80✔
139	return {std::move(res), stack & other.stack};	156✔
140	}
141	return bottom();	2✔
142	}	80✔
143
144	EbpfDomain EbpfDomain::calculate_constant_limits() {	57✔
145	EbpfDomain inv;	57✔
146	using namespace dsl_syntax;	28✔
147	for (const int i : {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}) {	627✔
148	const auto r = reg_pack(i);	570✔
149	inv.add_value_constraint(r.svalue <= std::numeric_limits<int32_t>::max());	850✔
150	inv.add_value_constraint(r.svalue >= std::numeric_limits<int32_t>::min());	850✔
151	inv.add_value_constraint(r.uvalue <= std::numeric_limits<uint32_t>::max());	850✔
152	inv.add_value_constraint(r.uvalue >= 0);	850✔
153	inv.add_value_constraint(r.stack_offset <= EBPF_TOTAL_STACK_SIZE);	850✔
154	inv.add_value_constraint(r.stack_offset >= 0);	850✔
155	inv.add_value_constraint(r.shared_offset <= r.shared_region_size);	850✔
156	inv.add_value_constraint(r.shared_offset >= 0);	850✔
157	inv.add_value_constraint(r.packet_offset <= variable_registry->packet_size());	850✔
158	inv.add_value_constraint(r.packet_offset >= 0);	850✔
159	if (thread_local_options.cfg_opts.check_for_termination) {	570✔
160	for (const Variable counter : variable_registry->get_loop_counters()) {	780✔
161	inv.add_value_constraint(counter <= std::numeric_limits<int32_t>::max());	580✔
162	inv.add_value_constraint(counter >= 0);	580✔
163	inv.add_value_constraint(counter <= r.svalue);	580✔
164	}	390✔
165	}
166	}
167	return inv;	57✔
168	}	×
169
170	// Lazy init via LazyAllocator<EbpfDomain, EbpfDomain::calculate_constant_limits> ensures
171	// thread_local_options and variable_registry are populated before EbpfDomain::calculate_constant_limits
172	// captures their state. LazyAllocator::get() has no reentrancy guard, but calculate_constant_limits
173	// does not call get_constant_limits() or widen(to_constants=true), so recursion cannot occur.
174	// Clamping via intersection (operator&) is sound because it only shrinks the domain by tightening
175	// constraints element-wise, preserving the over-approximation required for soundness.
176	static thread_local LazyAllocator<EbpfDomain, EbpfDomain::calculate_constant_limits> constant_limits;	757✔
177
178	static const EbpfDomain& get_constant_limits() { return constant_limits.get(); }	72✔
179
180	void EbpfDomain::clear_thread_local_state() { constant_limits.clear(); }	1,442✔
181
182	EbpfDomain EbpfDomain::widen(const EbpfDomain& other, const bool to_constants) const {	162✔
183	EbpfDomain res{this->state.widen(other.state), stack.widen(other.stack)};	243✔
184
185	if (to_constants) {	162✔
186	return res & get_constant_limits();	108✔
187	}
188	return res;	90✔
189	}	162✔
190
191	EbpfDomain EbpfDomain::narrow(const EbpfDomain& other) const {	×
192	return {state.narrow(other.state), stack & other.stack};	×
193	}
194
195	void EbpfDomain::add_value_constraint(const LinearConstraint& cst) { state.values.add_constraint(cst); }	25,669✔
196
197	void EbpfDomain::havoc(const Variable var) {	9,892✔
198	// TODO: type inv?
199	state.values.havoc(var);	9,892✔
200	}	4,946✔
201
202	// Get the start and end of the range of possible map fd values.
203	// In the future, it would be cleaner to use a set rather than an interval
204	// for map fds.
205	bool EbpfDomain::get_map_fd_range(const Reg& map_fd_reg, int32_t* start_fd, int32_t* end_fd) const {	42,386✔
206	const Interval& map_fd_interval = state.values.eval_interval(reg_pack(map_fd_reg).map_fd);	42,386✔
207	const auto lb = map_fd_interval.lb().number();	42,386✔
208	const auto ub = map_fd_interval.ub().number();	42,386✔
209	if (!lb \|\| !lb->fits<int32_t>() \|\| !ub \|\| !ub->fits<int32_t>()) {	42,386✔
210	return false;
211	}
212	*start_fd = lb->narrow<int32_t>();	42,386✔
213	*end_fd = ub->narrow<int32_t>();	42,386✔
214
215	// Cap the maximum range we'll check.
216	constexpr int max_range = 32;	42,386✔
217	return *map_fd_interval.finite_size() < max_range;	42,386✔
218	}
219
220	// All maps in the range must have the same type for us to use it.
221	std::optional<uint32_t> EbpfDomain::get_map_type(const Reg& map_fd_reg) const {	21,194✔
222	int32_t start_fd, end_fd;	10,597✔
223	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	21,194✔
224	return {};	×
225	}
226
227	std::optional<uint32_t> type;	21,194✔
228	for (int32_t map_fd = start_fd; map_fd <= end_fd; map_fd++) {	43,096✔
229	EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd);	21,906✔
230	if (map == nullptr) {	21,906✔
231	return {};	×
232	}
233	if (!type.has_value()) {	21,906✔
234	type = map->type;	21,194✔
235	} else if (map->type != *type) {	712✔
236	return {};	4✔
237	}
238	}
239	return type;	21,190✔
240	}
241
242	// All maps in the range must have the same inner map fd for us to use it.
243	std::optional<uint32_t> EbpfDomain::get_map_inner_map_fd(const Reg& map_fd_reg) const {	98✔
244	int start_fd, end_fd;	49✔
245	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	98✔
246	return {};	×
247	}
248
249	std::optional<uint32_t> inner_map_fd;	98✔
250	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	196✔
251	EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd);	98✔
252	if (map == nullptr) {	98✔
253	return {};	×
254	}
255	if (!inner_map_fd.has_value()) {	98✔
256	inner_map_fd = map->inner_map_fd;	98✔
257	} else if (map->type != *inner_map_fd) {	×
258	return {};	×
259	}
260	}
261	return inner_map_fd;	98✔
262	}
263
264	// We can deal with a range of key sizes.
265	Interval EbpfDomain::get_map_key_size(const Reg& map_fd_reg) const {	10,726✔
266	int start_fd, end_fd;	5,363✔
267	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	10,726✔
268	return Interval::top();	×
269	}
270
271	Interval result = Interval::bottom();	10,726✔
272	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	21,808✔
273	if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {	11,082✔
274	result = result \| Interval{map->key_size};	11,082✔
275	} else {
276	return Interval::top();	×
277	}
278	}
279	return result;	10,726✔
280	}
281
282	// We can deal with a range of value sizes.
283	Interval EbpfDomain::get_map_value_size(const Reg& map_fd_reg) const {	10,368✔
284	int start_fd, end_fd;	5,184✔
285	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	10,368✔
286	return Interval::top();	×
287	}
288
289	Interval result = Interval::bottom();	10,368✔
290	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	21,090✔
291	if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {	10,722✔
292	result = result \| Interval(map->value_size);	10,722✔
293	} else {
294	return Interval::top();	×
295	}
296	}
297	return result;	10,368✔
298	}
299
300	// We can deal with a range of max_entries values.
UNCOV 301	Interval EbpfDomain::get_map_max_entries(const Reg& map_fd_reg) const {	×
302	int start_fd, end_fd;
UNCOV 303	if (!get_map_fd_range(map_fd_reg, &start_fd, &end_fd)) {	×
304	return Interval::top();	×
305	}
306
UNCOV 307	Interval result = Interval::bottom();	×
UNCOV 308	for (int map_fd = start_fd; map_fd <= end_fd; map_fd++) {	×
UNCOV 309	if (const EbpfMapDescriptor* map = &thread_local_program_info->platform->get_map_descriptor(map_fd)) {	×
UNCOV 310	result = result \| Interval(map->max_entries);	×
311	} else {
312	return Interval::top();	×
313	}
314	}
UNCOV 315	return result;	×
316	}
317
318	ExtendedNumber EbpfDomain::get_loop_count_upper_bound() const {	238✔
319	ExtendedNumber ub{0};	238✔
320	for (const Variable counter : variable_registry->get_loop_counters()) {	460✔
321	ub = std::max(ub, state.values.eval_interval(counter).ub());	396✔
322	}	238✔
323	return ub;	238✔
324	}
325
326	Interval EbpfDomain::get_r0() const { return state.values.eval_interval(reg_pack(R0_RETURN_VALUE).svalue); }	6,048✔
327
328	std::ostream& operator<<(std::ostream& o, const TypeToNumDomain& dom) {	6✔
329	if (dom.is_bottom()) {	6✔
330	o << "_\|_";	×
331	} else {
332	o << dom.types << dom.values;	6✔
333	}
334	return o;	6✔
335	}
336
337	std::ostream& operator<<(std::ostream& o, const EbpfDomain& dom) {	6✔
338	if (dom.is_bottom()) {	6✔
339	o << "_\|_";	×
340	} else {
341	o << dom.state << "\nStack: " << dom.stack;	6✔
342	}
343	return o;	6✔
344	}
345
346	void EbpfDomain::initialize_packet() {	4,946✔
347	using namespace dsl_syntax;	2,473✔
348	EbpfDomain& inv = *this;	4,946✔
349	inv.havoc(variable_registry->packet_size());	4,946✔
350	inv.havoc(variable_registry->meta_offset());	4,946✔
351
352	inv.add_value_constraint(0 <= variable_registry->packet_size());	7,419✔
353	inv.add_value_constraint(variable_registry->packet_size() < MAX_PACKET_SIZE);	7,419✔
354	const auto info = *thread_local_program_info;	4,946✔
355	if (info.type.context_descriptor->meta >= 0) {	4,946✔
356	inv.add_value_constraint(variable_registry->meta_offset() <= 0);	5,565✔
357	inv.add_value_constraint(variable_registry->meta_offset() >= -4098);	5,565✔
358	} else {
359	inv.state.values.assign(variable_registry->meta_offset(), 0);	1,854✔
360	}
361	}	4,946✔
362
363	EbpfDomain EbpfDomain::from_constraints(const std::vector<std::pair<Variable, TypeSet>>& type_restrictions,	356✔
364	const std::vector<LinearConstraint>& value_constraints) {
365	EbpfDomain inv;	356✔
366
367	for (const auto& [var, ts] : type_restrictions) {	736✔
368	inv.state.types.restrict_to(var, ts);	380✔
369	}
370	for (const auto& cst : value_constraints) {	880✔
371	inv.add_value_constraint(cst);	524✔
372	}
373	return inv;	356✔
374	}	×
375
376	EbpfDomain EbpfDomain::from_constraints(const std::set<std::string>& constraints, const bool setup_constraints) {	2,072✔
377	EbpfDomain inv;	2,072✔
378	if (setup_constraints) {	2,072✔
379	inv = setup_entry(false);	939✔
380	}
381	auto numeric_ranges = std::vector<Interval>();	2,072✔
382	auto [type_equalities, type_restrictions, value_constraints] =	1,036✔
383	parse_linear_constraints(constraints, numeric_ranges);	2,072✔
384	for (const auto& [v1, v2] : type_equalities) {	2,074✔
385	inv.state.assume_eq_types(v1, v2);	2✔
386	}
387	for (const auto& [var, ts] : type_restrictions) {	4,460✔
388	inv.state.types.restrict_to(var, ts);	2,388✔
389	}
390	for (const auto& cst : value_constraints) {	8,232✔
391	inv.add_value_constraint(cst);	6,160✔
392	}
393	for (const Interval& range : numeric_ranges) {	2,344✔
394	const auto [start, ub] = range.pair<int64_t>();	272✔
395	const int width = gsl::narrow<int>(1 + (ub - start));	272✔
396	inv.stack.initialize_numbers(gsl::narrow<int>(start), width);	272✔
397	}
398	// TODO: handle other stack type constraints
399	return inv;	3,108✔
400	}	2,072✔
401
402	EbpfDomain EbpfDomain::setup_entry(const bool init_r1) {	2,600✔
403	using namespace dsl_syntax;	1,300✔
404
405	EbpfDomain inv;	2,600✔
406
407	const auto r10 = reg_pack(R10_STACK_POINTER);	2,600✔
408	constexpr Reg r10_reg{R10_STACK_POINTER};	2,600✔
409	inv.state.values.add_constraint(EBPF_TOTAL_STACK_SIZE <= r10.svalue);	3,900✔
410	inv.state.values.add_constraint(r10.svalue <= PTR_MAX);	3,900✔
411	inv.state.values.assign(r10.stack_offset, EBPF_TOTAL_STACK_SIZE);	2,600✔
412	// stack_numeric_size would be 0, but TOP has the same result
413	// so no need to assign it.
414	inv.state.assign_type(r10_reg, T_STACK);	2,600✔
415
416	if (init_r1) {	2,600✔
417	const auto r1 = reg_pack(R1_ARG);	1,974✔
418	constexpr Reg r1_reg{R1_ARG};	1,974✔
419	inv.state.values.add_constraint(1 <= r1.svalue);	2,961✔
420	inv.state.values.add_constraint(r1.svalue <= PTR_MAX);	2,961✔
421	inv.state.values.assign(r1.ctx_offset, 0);	1,974✔
422	inv.state.assign_type(r1_reg, T_CTX);	1,974✔
423	}
424
425	inv.initialize_packet();	2,600✔
426	return inv;	3,900✔
427	}	×
428
429	} // namespace prevail

Alan-Jowett / ebpf-verifier / 22316701280

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