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

89.76

/src/crab/ebpf_checker.cpp

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

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

#include <bitset>
#include <optional>
#include <utility>
#include <variant>

#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/program.hpp"
#include "ir/syntax.hpp"
#include "ir/unmarshal.hpp"
#include "platform.hpp"

namespace prevail {

class EbpfChecker final {
  public:
    explicit EbpfChecker(const EbpfDomain& dom, Assertion assertion) : assertion{std::move(assertion)}, dom(dom) {}

    void visit() { std::visit(*this, assertion); }

    void operator()(const Addable&) const;
    void operator()(const BoundedLoopCount&) const;
    void operator()(const Comparable&) const;
    void operator()(const FuncConstraint&) const;
    void operator()(const ValidDivisor&) const;
    void operator()(const TypeConstraint&) const;
    void operator()(const ValidAccess&) const;
    void operator()(const ValidCallbackTarget&) const;
    void operator()(const ValidMapKeyValue&) const;
    void operator()(const ValidSize&) const;
    void operator()(const ValidStore&) const;
    void operator()(const ZeroCtxOffset&) const;

  private:
    void require_value(const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {
        if (!inv.values.entail(cst)) {
            throw_fail(msg);
        }
    }

    [[noreturn]]
    void throw_fail(const std::string& msg) const {
        throw VerificationError(msg + " (" + to_string(assertion) + ")");
    }

    // memory check / load / store
    void check_access_stack(const LinearExpression& lb, const LinearExpression& ub) const;
    void check_access_context(const LinearExpression& lb, const LinearExpression& ub) const;
    void check_access_packet(const LinearExpression& lb, const LinearExpression& ub,
                             std::optional<Variable> packet_size) const;
    void check_access_shared(const LinearExpression& lb, const LinearExpression& ub, Variable shared_region_size) const;

  private:
    const Assertion assertion;

    const EbpfDomain& dom;
};

std::optional<VerificationError> ebpf_domain_check(const EbpfDomain& dom, const Assertion& assertion,
                                                   const Label& where) {
    if (dom.is_bottom()) {
        return {};
    }
    try {
        EbpfChecker{dom, assertion}.visit();
    } catch (VerificationError& error) {
        error.where = where;
        return {error};
    }
    return {};
}

void EbpfChecker::check_access_stack(const LinearExpression& lb, const LinearExpression& ub) const {
    using namespace dsl_syntax;
    require_value(dom.state, reg_pack(R10_STACK_POINTER).stack_offset - EBPF_SUBPROGRAM_STACK_SIZE <= lb,
                  "Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE");
    require_value(dom.state, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE");
}

void EbpfChecker::check_access_context(const LinearExpression& lb, const LinearExpression& ub) const {
    using namespace dsl_syntax;
    require_value(dom.state, lb >= 0, "Lower bound must be at least 0");
    require_value(dom.state, ub <= thread_local_program_info->type.context_descriptor->size,
                  std::string("Upper bound must be at most ") +
                      std::to_string(thread_local_program_info->type.context_descriptor->size));
}

void EbpfChecker::check_access_packet(const LinearExpression& lb, const LinearExpression& ub,
                                      const std::optional<Variable> packet_size) const {
    using namespace dsl_syntax;
    require_value(dom.state, lb >= variable_registry->meta_offset(), "Lower bound must be at least meta_offset");
    if (packet_size) {
        require_value(dom.state, ub <= *packet_size, "Upper bound must be at most packet_size");
    } else {
        require_value(dom.state, ub <= MAX_PACKET_SIZE,
                      std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));
    }
}

void EbpfChecker::check_access_shared(const LinearExpression& lb, const LinearExpression& ub,
                                      const Variable shared_region_size) const {
    using namespace dsl_syntax;
    require_value(dom.state, lb >= 0, "Lower bound must be at least 0");
    require_value(dom.state, ub <= shared_region_size,
                  std::string("Upper bound must be at most ") + variable_registry->name(shared_region_size));
}

void EbpfChecker::operator()(const Comparable& s) const {
    using namespace dsl_syntax;
    if (dom.state.same_type(s.r1, s.r2)) {
        // Same type. If both are numbers, that's okay. Otherwise:
        TypeDomain non_number_types = dom.state.types;
        non_number_types.remove_type(reg_type(s.r2), T_NUM);
        // We must check that they belong to a singleton region:
        if (!non_number_types.is_in_group(s.r1, TS_SINGLETON_PTR) && !non_number_types.is_in_group(s.r1, TS_MAP)) {
            throw_fail("Cannot subtract pointers to non-singleton regions");
        }
        // And, to avoid wraparound errors, they must be within bounds.
        this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r1, 0, Imm{0}, false});
        this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r2, 0, Imm{0}, false});
    } else {
        // _Maybe_ different types, so r2 must be a number.
        // We checked in a previous assertion that r1 is a pointer or a number.
        if (!dom.state.entail_type(reg_type(s.r2), T_NUM)) {
            throw_fail("Cannot subtract pointers to different regions");
        }
    }
}

void EbpfChecker::operator()(const Addable& s) const {
    if (!dom.state.implies_superset(s.ptr, TS_POINTER, s.num, TS_NUM)) {
        throw_fail("Only numbers can be added to pointers");
    }
}

void EbpfChecker::operator()(const ValidDivisor& s) const {
    using namespace dsl_syntax;
    if (!dom.state.implies_superset(s.reg, TS_POINTER, s.reg, TS_NUM)) {
        throw_fail("Only numbers can be used as divisors");
    }
    if (!thread_local_options.allow_division_by_zero) {
        const auto reg = reg_pack(s.reg);
        const auto v = s.is_signed ? reg.svalue : reg.uvalue;
        require_value(dom.state, v != 0, "Possible division by zero");
    }
}

void EbpfChecker::operator()(const ValidStore& s) const {
    if (!dom.state.implies_not_type(s.mem, T_STACK, s.val, TS_NUM)) {
        throw_fail("Only numbers can be stored to externally-visible regions");
    }
}

void EbpfChecker::operator()(const TypeConstraint& s) const {
    if (!dom.state.is_in_group(s.reg, to_typeset(s.types))) {
        throw_fail("Invalid type");
    }
}

void EbpfChecker::operator()(const BoundedLoopCount& s) const {
    // Enforces an upper bound on loop iterations by checking that the loop counter
    // does not exceed the specified limit
    using namespace dsl_syntax;
    const auto counter = variable_registry->loop_counter(to_string(s.name));
    require_value(dom.state, counter <= BoundedLoopCount::limit, "Loop counter is too large");
}

void EbpfChecker::operator()(const FuncConstraint& s) const {
    // Look up the helper function id.
    if (dom.state.is_bottom()) {
        return;
    }
    const auto src_interval = dom.state.values.eval_interval(reg_pack(s.reg).svalue);
    if (const auto sn = src_interval.singleton()) {
        if (sn->fits<int32_t>()) {
            // We can now process it as if the id was immediate.
            const int32_t imm = sn->cast_to<int32_t>();
            if (!thread_local_program_info->platform->is_helper_usable(imm)) {
                throw_fail("invalid helper function id " + std::to_string(imm));
            }
            const Call call = make_call(imm, *thread_local_program_info->platform);
            for (const Assertion& sub_assertion : get_assertions(call, *thread_local_program_info, {})) {
                // TODO: create explicit sub assertions elsewhere
                EbpfChecker{dom, sub_assertion}.visit();
            }
            return;
        }
    }
    throw_fail("callx helper function id is not a valid singleton");
}

void EbpfChecker::operator()(const ValidSize& s) const {
    using namespace dsl_syntax;
    const auto r = reg_pack(s.reg);
    require_value(dom.state, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size");
}

void EbpfChecker::operator()(const ValidCallbackTarget& s) const {
    const auto callback_interval = dom.state.values.eval_interval(reg_pack(s.reg).svalue);
    const auto callback_target = callback_interval.singleton();
    if (!callback_target.has_value() || !callback_target->fits<int32_t>()) {
        throw_fail("callback function pointer must be a singleton code address");
    }

    const int32_t callback_label = callback_target->cast_to<int32_t>();
    if (!thread_local_program_info->callback_target_labels.contains(callback_label)) {
        throw_fail("callback function pointer does not reference a valid callback entry");
    }
    if (!thread_local_program_info->callback_targets_with_exit.contains(callback_label)) {
        throw_fail("callback function does not have a reachable exit");
    }
}

void EbpfChecker::operator()(const ValidMapKeyValue& s) const {
    using namespace dsl_syntax;

    const auto fd_type = dom.get_map_type(s.map_fd_reg);

    const auto access_reg = reg_pack(s.access_reg);
    int width;
    if (s.key) {
        const auto key_size = dom.get_map_key_size(s.map_fd_reg).singleton();
        if (!key_size.has_value()) {
            throw_fail("Map key size is not singleton");
        }
        width = key_size->narrow<int>();
    } else {
        const auto value_size = dom.get_map_value_size(s.map_fd_reg).singleton();
        if (!value_size.has_value()) {
            throw_fail("Map value size is not singleton");
        }
        width = value_size->narrow<int>();
    }

    for (const auto access_reg_type : dom.state.enumerate_types(s.access_reg)) {
        if (access_reg_type == T_STACK) {
            Interval offset = dom.state.values.eval_interval(access_reg.stack_offset);
            if (!dom.stack.all_num_width(offset, Interval{width})) {
                auto lb_is = offset.lb().number();
                std::string lb_s = lb_is && lb_is->fits<int32_t>() ? std::to_string(lb_is->narrow<int32_t>()) : "-oo";
                Interval ub = offset + Interval{width};
                auto ub_is = ub.ub().number();
                std::string ub_s = ub_is && ub_is->fits<int32_t>() ? std::to_string(ub_is->narrow<int32_t>()) : "oo";
                require_value(dom.state, LinearConstraint::false_const(),
                              "Illegal map update with a non-numerical value [" + lb_s + "-" + ub_s + ")");
            } else if (thread_local_options.strict && fd_type.has_value()) {
                EbpfMapType map_type = thread_local_program_info->platform->get_map_type(*fd_type);
                if (map_type.is_array) {
                    // Get offset value.
                    Variable key_ptr = access_reg.stack_offset;
                    std::optional<Number> offset_num = dom.state.values.eval_interval(key_ptr).singleton();
                    if (!offset_num.has_value()) {
                        throw_fail("Pointer must be a singleton");
                    } else if (s.key) {
                        // Look up the value pointed to by the key pointer.
                        Variable key_value =
                            variable_registry->cell_var(DataKind::svalues, offset_num.value(), sizeof(uint32_t));

                        if (auto max_entries = dom.get_map_max_entries(s.map_fd_reg).lb().number()) {
                            require_value(dom.state, key_value < *max_entries, "Array index overflow");
                        } else {
                            throw_fail("Max entries is not finite");
                        }
                        require_value(dom.state, key_value >= 0, "Array index underflow");
                    }
                }
            }
        } else if (access_reg_type == T_PACKET) {
            Variable lb = access_reg.packet_offset;
            LinearExpression ub = lb + width;
            check_access_packet(lb, ub, {});
            // Packet memory is both readable and writable.
        } else if (access_reg_type == T_SHARED) {
            Variable lb = access_reg.shared_offset;
            LinearExpression ub = lb + width;
            check_access_shared(lb, ub, access_reg.shared_region_size);
            require_value(dom.state, access_reg.svalue > 0, "Possible null access");
            // Shared memory is zero-initialized when created so is safe to read and write.
        } else {
            throw_fail("Only stack, packet, or shared can be used as a parameter");
        }
    }
}

static std::tuple<LinearExpression, LinearExpression> lb_ub_access_pair(const ValidAccess& s,
                                                                        const Variable offset_var) {
    using namespace dsl_syntax;
    LinearExpression lb = offset_var + s.offset;
    LinearExpression ub = std::holds_alternative<Imm>(s.width) ? lb + std::get<Imm>(s.width).v
                                                               : lb + reg_pack(std::get<Reg>(s.width)).svalue;
    return {lb, ub};
}

void EbpfChecker::operator()(const ValidAccess& s) const {
    using namespace dsl_syntax;

    const bool is_comparison_check = s.width == Value{Imm{0}};

    const auto reg = reg_pack(s.reg);
    for (const auto type : dom.state.enumerate_types(s.reg)) {
        switch (type) {
        case T_PACKET: {
            auto [lb, ub] = lb_ub_access_pair(s, reg.packet_offset);
            const std::optional<Variable> packet_size =
                is_comparison_check ? std::optional<Variable>{} : variable_registry->packet_size();
            check_access_packet(lb, ub, packet_size);
            // if within bounds, it can never be null
            // Context memory is both readable and writable.
            break;
        }
        case T_STACK: {
            auto [lb, ub] = lb_ub_access_pair(s, reg.stack_offset);
            check_access_stack(lb, ub);
            // if within bounds, it can never be null
            if (s.access_type == AccessType::read &&
                !dom.stack.all_num_lb_ub(dom.state.values.eval_interval(lb), dom.state.values.eval_interval(ub))) {

                if (s.offset < 0) {
                    throw_fail("Stack content is not numeric");
                } else {
                    using namespace dsl_syntax;
                    LinearExpression w = std::holds_alternative<Imm>(s.width)
                                             ? LinearExpression{std::get<Imm>(s.width).v}
                                             : reg_pack(std::get<Reg>(s.width)).svalue;

                    require_value(dom.state, w <= reg.stack_numeric_size - s.offset, "Stack content is not numeric");
                }
            }
            break;
        }
        case T_CTX: {
            auto [lb, ub] = lb_ub_access_pair(s, reg.ctx_offset);
            check_access_context(lb, ub);
            // if within bounds, it can never be null
            // The context is both readable and writable.
            break;
        }
        case T_SHARED: {
            auto [lb, ub] = lb_ub_access_pair(s, reg.shared_offset);
            check_access_shared(lb, ub, reg.shared_region_size);
            if (!is_comparison_check && !s.or_null) {
                require_value(dom.state, reg.svalue > 0, "Possible null access");
            }
            // Shared memory is zero-initialized when created so is safe to read and write.
            break;
        }
        case T_NUM:
            if (!is_comparison_check) {
                if (s.or_null) {
                    require_value(dom.state, reg.svalue == 0, "Non-null number");
                    // A null pointer access is only valid with zero width.
                    if (std::holds_alternative<Imm>(s.width)) {
                        if (std::get<Imm>(s.width).v != 0) {
                            throw_fail("Non-zero access size with null pointer");
                        }
                    } else {
                        const auto width_svalue = reg_pack(std::get<Reg>(s.width)).svalue;
                        require_value(dom.state, width_svalue == 0, "Non-zero access size with null pointer");
                    }
                } else {
                    throw_fail("Only pointers can be dereferenced");
                }
            }
            break;
        case T_MAP:
        case T_MAP_PROGRAMS:
            if (!is_comparison_check) {
                throw_fail("FDs cannot be dereferenced directly");
            }
            break;
        case T_SOCKET:
        case T_BTF_ID:
            // TODO: implement proper access checks for these pointer types.
            if (!is_comparison_check) {
                throw_fail("Unsupported pointer type for memory access");
            }
            break;
        case T_ALLOC_MEM: {
            // Treat like shared: offset-bounded access with null check.
            auto [lb, ub] = lb_ub_access_pair(s, reg.alloc_mem_offset);
            check_access_shared(lb, ub, reg.alloc_mem_size);
            if (!is_comparison_check && !s.or_null) {
                require_value(dom.state, reg.svalue > 0, "Possible null access");
            }
            break;
        }
        case T_FUNC:
            if (!is_comparison_check) {
                throw_fail("Function pointers cannot be dereferenced");
            }
            break;
        default: throw_fail("Invalid type");
        }
    }
}

void EbpfChecker::operator()(const ZeroCtxOffset& s) const {
    using namespace dsl_syntax;
    const auto reg = reg_pack(s.reg);
    // The domain is not expressive enough to handle join of null and non-null ctx,
    // Since non-null ctx pointers are nonzero numbers.
    if (s.or_null && dom.state.is_in_group(s.reg, TS_NUM) && dom.state.values.entail(reg.uvalue == 0)) {
        return;
    }
    require_value(dom.state, reg.ctx_offset == 0, "Nonzero context offset");
}

} // 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 <bitset>
7	#include <optional>
8	#include <utility>
9	#include <variant>
10
11	#include "arith/dsl_syntax.hpp"
12	#include "config.hpp"
13	#include "crab/array_domain.hpp"
14	#include "crab/ebpf_domain.hpp"
15	#include "crab/var_registry.hpp"
16	#include "ir/program.hpp"
17	#include "ir/syntax.hpp"
18	#include "ir/unmarshal.hpp"
19	#include "platform.hpp"
20
21	namespace prevail {
22
23	class EbpfChecker final {	970✔
24	public:
25	explicit EbpfChecker(const EbpfDomain& dom, Assertion assertion) : assertion{std::move(assertion)}, dom(dom) {}	1,130,007✔
26
27	void visit() { std::visit(*this, assertion); }	753,338✔
28
29	void operator()(const Addable&) const;
30	void operator()(const BoundedLoopCount&) const;
31	void operator()(const Comparable&) const;
32	void operator()(const FuncConstraint&) const;
33	void operator()(const ValidDivisor&) const;
34	void operator()(const TypeConstraint&) const;
35	void operator()(const ValidAccess&) const;
36	void operator()(const ValidCallbackTarget&) const;
37	void operator()(const ValidMapKeyValue&) const;
38	void operator()(const ValidSize&) const;
39	void operator()(const ValidStore&) const;
40	void operator()(const ZeroCtxOffset&) const;
41
42	private:
43	void require_value(const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {	395,880✔
44	if (!inv.values.entail(cst)) {	593,820✔
45	throw_fail(msg);	1,128✔
46	}
47	}	394,752✔
48
49	[[noreturn]]
50	void throw_fail(const std::string& msg) const {	1,920✔
51	throw VerificationError(msg + " (" + to_string(assertion) + ")");	2,880✔
52	}
53
54	// memory check / load / store
55	void check_access_stack(const LinearExpression& lb, const LinearExpression& ub) const;
56	void check_access_context(const LinearExpression& lb, const LinearExpression& ub) const;
57	void check_access_packet(const LinearExpression& lb, const LinearExpression& ub,
58	std::optional<Variable> packet_size) const;
59	void check_access_shared(const LinearExpression& lb, const LinearExpression& ub, Variable shared_region_size) const;
60
61	private:
62	const Assertion assertion;
63
64	const EbpfDomain& dom;
65	};
66
67	std::optional<VerificationError> ebpf_domain_check(const EbpfDomain& dom, const Assertion& assertion,	1,099,714✔
68	const Label& where) {
69	if (dom.is_bottom()) {	1,099,714✔
70	return {};	346,572✔
71	}
72	try {	376,571✔
73	EbpfChecker{dom, assertion}.visit();	1,133,553✔
74	} catch (VerificationError& error) {	1,920✔
75	error.where = where;	1,920✔
76	return {error};	1,920✔
77	}	1,920✔
78	return {};	751,222✔
79	}
80
81	void EbpfChecker::check_access_stack(const LinearExpression& lb, const LinearExpression& ub) const {	13,926✔
82	using namespace dsl_syntax;	6,963✔
83	require_value(dom.state, reg_pack(R10_STACK_POINTER).stack_offset - EBPF_SUBPROGRAM_STACK_SIZE <= lb,	34,821✔
84	"Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE");
85	require_value(dom.state, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE");	20,898✔
86	}	13,918✔
87
88	void EbpfChecker::check_access_context(const LinearExpression& lb, const LinearExpression& ub) const {	20,652✔
89	using namespace dsl_syntax;	6,884✔
90	require_value(dom.state, lb >= 0, "Lower bound must be at least 0");	20,652✔
91	require_value(dom.state, ub <= thread_local_program_info->type.context_descriptor->size,	27,539✔
92	std::string("Upper bound must be at most ") +	27,539✔
93	std::to_string(thread_local_program_info->type.context_descriptor->size));	20,653✔
94	}	13,766✔
95
96	void EbpfChecker::check_access_packet(const LinearExpression& lb, const LinearExpression& ub,	22,944✔
97	const std::optional<Variable> packet_size) const {
98	using namespace dsl_syntax;	11,472✔
99	require_value(dom.state, lb >= variable_registry->meta_offset(), "Lower bound must be at least meta_offset");	45,892✔
100	if (packet_size) {	22,942✔
101	require_value(dom.state, ub <= *packet_size, "Upper bound must be at most packet_size");	24,474✔
102	} else {
103	require_value(dom.state, ub <= MAX_PACKET_SIZE,	16,881✔
104	std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));	33,762✔
105	}
106	}	22,210✔
107
108	void EbpfChecker::check_access_shared(const LinearExpression& lb, const LinearExpression& ub,	91,238✔
109	const Variable shared_region_size) const {
110	using namespace dsl_syntax;	45,619✔
111	require_value(dom.state, lb >= 0, "Lower bound must be at least 0");	136,885✔
112	require_value(dom.state, ub <= shared_region_size,	182,574✔
113	std::string("Upper bound must be at most ") + variable_registry->name(shared_region_size));	273,798✔
114	}	91,140✔
115
116	void EbpfChecker::operator()(const Comparable& s) const {	11,510✔
117	using namespace dsl_syntax;	5,755✔
118	if (dom.state.same_type(s.r1, s.r2)) {	11,510✔
119	// Same type. If both are numbers, that's okay. Otherwise:
120	TypeDomain non_number_types = dom.state.types;	11,500✔
121	non_number_types.remove_type(reg_type(s.r2), T_NUM);	11,500✔
122	// We must check that they belong to a singleton region:
123	if (!non_number_types.is_in_group(s.r1, TS_SINGLETON_PTR) && !non_number_types.is_in_group(s.r1, TS_MAP)) {	11,500✔
124	throw_fail("Cannot subtract pointers to non-singleton regions");	4✔
125	}
126	// And, to avoid wraparound errors, they must be within bounds.
127	this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r1, 0, Imm{0}, false});	11,498✔
128	this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r2, 0, Imm{0}, false});	11,496✔
129	} else {	11,500✔
130	// _Maybe_ different types, so r2 must be a number.
131	// We checked in a previous assertion that r1 is a pointer or a number.
132	if (!dom.state.entail_type(reg_type(s.r2), T_NUM)) {	10✔
133	throw_fail("Cannot subtract pointers to different regions");	9✔
134	}
135	}
136	}	11,500✔
137
138	void EbpfChecker::operator()(const Addable& s) const {	24,534✔
139	if (!dom.state.implies_superset(s.ptr, TS_POINTER, s.num, TS_NUM)) {	24,534✔
140	throw_fail("Only numbers can be added to pointers");	21✔
141	}
142	}	24,520✔
143
144	void EbpfChecker::operator()(const ValidDivisor& s) const {	332✔
145	using namespace dsl_syntax;	166✔
146	if (!dom.state.implies_superset(s.reg, TS_POINTER, s.reg, TS_NUM)) {	332✔
147	throw_fail("Only numbers can be used as divisors");	24✔
148	}
149	if (!thread_local_options.allow_division_by_zero) {	320✔
150	const auto reg = reg_pack(s.reg);	64✔
151	const auto v = s.is_signed ? reg.svalue : reg.uvalue;	64✔
152	require_value(dom.state, v != 0, "Possible division by zero");	256✔
153	}
154	}	256✔
155
156	void EbpfChecker::operator()(const ValidStore& s) const {	3,116✔
157	if (!dom.state.implies_not_type(s.mem, T_STACK, s.val, TS_NUM)) {	3,116✔
158	throw_fail("Only numbers can be stored to externally-visible regions");	3✔
159	}
160	}	3,114✔
161
162	void EbpfChecker::operator()(const TypeConstraint& s) const {	506,666✔
163	if (!dom.state.is_in_group(s.reg, to_typeset(s.types))) {	506,666✔
164	throw_fail("Invalid type");	1,098✔
165	}
166	}	505,934✔
167
168	void EbpfChecker::operator()(const BoundedLoopCount& s) const {	40✔
169	// Enforces an upper bound on loop iterations by checking that the loop counter
170	// does not exceed the specified limit
171	using namespace dsl_syntax;	20✔
172	const auto counter = variable_registry->loop_counter(to_string(s.name));	40✔
173	require_value(dom.state, counter <= BoundedLoopCount::limit, "Loop counter is too large");	115✔
174	}	18✔
175
176	void EbpfChecker::operator()(const FuncConstraint& s) const {	48✔
177	// Look up the helper function id.
178	if (dom.state.is_bottom()) {	48✔
179	return;
180	}
181	const auto src_interval = dom.state.values.eval_interval(reg_pack(s.reg).svalue);	48✔
182	if (const auto sn = src_interval.singleton()) {	48✔
183	if (sn->fits<int32_t>()) {	46✔
184	// We can now process it as if the id was immediate.
185	const int32_t imm = sn->cast_to<int32_t>();	46✔
186	if (!thread_local_program_info->platform->is_helper_usable(imm)) {	46✔
187	throw_fail("invalid helper function id " + std::to_string(imm));	12✔
188	}
189	const Call call = make_call(imm, *thread_local_program_info->platform);	42✔
190	for (const Assertion& sub_assertion : get_assertions(call, *thread_local_program_info, {})) {	218✔
191	// TODO: create explicit sub assertions elsewhere
192	EbpfChecker{dom, sub_assertion}.visit();	334✔
193	}	42✔
194	return;	22✔
195	}	42✔
196	}
197	throw_fail("callx helper function id is not a valid singleton");	3✔
198	}
199
200	void EbpfChecker::operator()(const ValidSize& s) const {	14,412✔
201	using namespace dsl_syntax;	7,206✔
202	const auto r = reg_pack(s.reg);	14,412✔
203	require_value(dom.state, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size");	36,520✔
204	}	14,314✔
205
206	void EbpfChecker::operator()(const ValidCallbackTarget& s) const {	8✔
207	const auto callback_interval = dom.state.values.eval_interval(reg_pack(s.reg).svalue);	8✔
208	const auto callback_target = callback_interval.singleton();	8✔
209	if (!callback_target.has_value() \|\| !callback_target->fits<int32_t>()) {	8✔
210	throw_fail("callback function pointer must be a singleton code address");	×
211	}
212
213	const int32_t callback_label = callback_target->cast_to<int32_t>();	8✔
214	if (!thread_local_program_info->callback_target_labels.contains(callback_label)) {	8✔
215	throw_fail("callback function pointer does not reference a valid callback entry");	4✔
216	}
217	if (!thread_local_program_info->callback_targets_with_exit.contains(callback_label)) {	6✔
218	throw_fail("callback function does not have a reachable exit");	3✔
219	}
220	}	4✔
221
222	void EbpfChecker::operator()(const ValidMapKeyValue& s) const {	13,760✔
223	using namespace dsl_syntax;	6,880✔
224
225	const auto fd_type = dom.get_map_type(s.map_fd_reg);	13,760✔
226
227	const auto access_reg = reg_pack(s.access_reg);	13,760✔
228	int width;	6,880✔
229	if (s.key) {	13,760✔
230	const auto key_size = dom.get_map_key_size(s.map_fd_reg).singleton();	10,726✔
231	if (!key_size.has_value()) {	10,726✔
232	throw_fail("Map key size is not singleton");	×
233	}
234	width = key_size->narrow<int>();	10,726✔
235	} else {
236	const auto value_size = dom.get_map_value_size(s.map_fd_reg).singleton();	3,034✔
237	if (!value_size.has_value()) {	3,034✔
238	throw_fail("Map value size is not singleton");	×
239	}
240	width = value_size->narrow<int>();	3,034✔
241	}
242
243	for (const auto access_reg_type : dom.state.enumerate_types(s.access_reg)) {	27,466✔
244	if (access_reg_type == T_STACK) {	13,760✔
245	Interval offset = dom.state.values.eval_interval(access_reg.stack_offset);	13,500✔
246	if (!dom.stack.all_num_width(offset, Interval{width})) {	13,500✔
247	auto lb_is = offset.lb().number();	38✔
248	std::string lb_s = lb_is && lb_is->fits<int32_t>() ? std::to_string(lb_is->narrow<int32_t>()) : "-oo";	40✔
249	Interval ub = offset + Interval{width};	38✔
250	auto ub_is = ub.ub().number();	38✔
251	std::string ub_s = ub_is && ub_is->fits<int32_t>() ? std::to_string(ub_is->narrow<int32_t>()) : "oo";	59✔
252	require_value(dom.state, LinearConstraint::false_const(),	76✔
253	"Illegal map update with a non-numerical value [" + lb_s + "-" + ub_s + ")");	247✔
254	} else if (thread_local_options.strict && fd_type.has_value()) {	13,538✔
UNCOV 255	EbpfMapType map_type = thread_local_program_info->platform->get_map_type(*fd_type);	×
UNCOV 256	if (map_type.is_array) {	×
257	// Get offset value.
UNCOV 258	Variable key_ptr = access_reg.stack_offset;	×
UNCOV 259	std::optional<Number> offset_num = dom.state.values.eval_interval(key_ptr).singleton();	×
UNCOV 260	if (!offset_num.has_value()) {	×
261	throw_fail("Pointer must be a singleton");	×
UNCOV 262	} else if (s.key) {	×
263	// Look up the value pointed to by the key pointer.
264	Variable key_value =
UNCOV 265	variable_registry->cell_var(DataKind::svalues, offset_num.value(), sizeof(uint32_t));	×
266
UNCOV 267	if (auto max_entries = dom.get_map_max_entries(s.map_fd_reg).lb().number()) {	×
UNCOV 268	require_value(dom.state, key_value < *max_entries, "Array index overflow");	×
269	} else {
270	throw_fail("Max entries is not finite");	×
271	}
UNCOV 272	require_value(dom.state, key_value >= 0, "Array index underflow");	×
273	}
274	}
UNCOV 275	}	×
276	} else if (access_reg_type == T_PACKET) {	260✔
277	Variable lb = access_reg.packet_offset;	136✔
278	LinearExpression ub = lb + width;	204✔
279	check_access_packet(lb, ub, {});	204✔
280	// Packet memory is both readable and writable.
281	} else if (access_reg_type == T_SHARED) {	260✔
282	Variable lb = access_reg.shared_offset;	124✔
283	LinearExpression ub = lb + width;	186✔
284	check_access_shared(lb, ub, access_reg.shared_region_size);	132✔
285	require_value(dom.state, access_reg.svalue > 0, "Possible null access");	256✔
286	// Shared memory is zero-initialized when created so is safe to read and write.
287	} else {	124✔
288	throw_fail("Only stack, packet, or shared can be used as a parameter");	27✔
289	}
290	}	13,760✔
291	}	13,706✔
292
293	static std::tuple<LinearExpression, LinearExpression> lb_ub_access_pair(const ValidAccess& s,	141,616✔
294	const Variable offset_var) {
295	using namespace dsl_syntax;	70,808✔
296	LinearExpression lb = offset_var + s.offset;	212,424✔
297	LinearExpression ub = std::holds_alternative<Imm>(s.width) ? lb + std::get<Imm>(s.width).v	205,529✔
298	: lb + reg_pack(std::get<Reg>(s.width)).svalue;	269,442✔
299	return {lb, ub};	212,424✔
300	}	141,616✔
301
302	void EbpfChecker::operator()(const ValidAccess& s) const {	190,976✔
303	using namespace dsl_syntax;	95,488✔
304
305	const bool is_comparison_check = s.width == Value{Imm{0}};	190,976✔
306
307	const auto reg = reg_pack(s.reg);	190,976✔
308	for (const auto type : dom.state.enumerate_types(s.reg)) {	381,306✔
309	switch (type) {	191,232✔
310	case T_PACKET: {	22,808✔
311	auto [lb, ub] = lb_ub_access_pair(s, reg.packet_offset);	22,808✔
312	const std::optional<Variable> packet_size =	11,404✔
313	is_comparison_check ? std::optional<Variable>{} : variable_registry->packet_size();	23,175✔
314	check_access_packet(lb, ub, packet_size);	22,808✔
315	// if within bounds, it can never be null
316	// Context memory is both readable and writable.
317	break;	22,074✔
318	}	22,808✔
319	case T_STACK: {	13,926✔
320	auto [lb, ub] = lb_ub_access_pair(s, reg.stack_offset);	13,926✔
321	check_access_stack(lb, ub);	13,926✔
322	// if within bounds, it can never be null
323	if (s.access_type == AccessType::read &&	20,124✔
324	!dom.stack.all_num_lb_ub(dom.state.values.eval_interval(lb), dom.state.values.eval_interval(ub))) {	20,008✔
325
326	if (s.offset < 0) {	232✔
327	throw_fail("Stack content is not numeric");	×
328	} else {
329	using namespace dsl_syntax;	116✔
330	LinearExpression w = std::holds_alternative<Imm>(s.width)	232✔
331	? LinearExpression{std::get<Imm>(s.width).v}	232✔
332	: reg_pack(std::get<Reg>(s.width)).svalue;	255✔
333
334	require_value(dom.state, w <= reg.stack_numeric_size - s.offset, "Stack content is not numeric");	597✔
335	}	232✔
336	}
337	break;	13,880✔
338	}	13,926✔
339	case T_CTX: {	13,768✔
340	auto [lb, ub] = lb_ub_access_pair(s, reg.ctx_offset);	13,768✔
341	check_access_context(lb, ub);	13,768✔
342	// if within bounds, it can never be null
343	// The context is both readable and writable.
344	break;	13,766✔
345	}	13,768✔
346	case T_SHARED: {	91,104✔
347	auto [lb, ub] = lb_ub_access_pair(s, reg.shared_offset);	91,104✔
348	check_access_shared(lb, ub, reg.shared_region_size);	91,104✔
349	if (!is_comparison_check && !s.or_null) {	91,014✔
350	require_value(dom.state, reg.svalue > 0, "Possible null access");	213,434✔
351	}
352	// Shared memory is zero-initialized when created so is safe to read and write.
353	break;	91,002✔
354	}	91,104✔
355	case T_NUM:	49,416✔
356	if (!is_comparison_check) {	49,416✔
357	if (s.or_null) {	498✔
358	require_value(dom.state, reg.svalue == 0, "Non-null number");	757✔
359	// A null pointer access is only valid with zero width.
360	if (std::holds_alternative<Imm>(s.width)) {	494✔
UNCOV 361	if (std::get<Imm>(s.width).v != 0) {	×
UNCOV 362	throw_fail("Non-zero access size with null pointer");	×
363	}
364	} else {
365	const auto width_svalue = reg_pack(std::get<Reg>(s.width)).svalue;	494✔
366	require_value(dom.state, width_svalue == 0, "Non-zero access size with null pointer");	988✔
367	}
368	} else {
UNCOV 369	throw_fail("Only pointers can be dereferenced");	×
370	}
371	}
372	break;	24,706✔
373	case T_MAP:	126✔
374	case T_MAP_PROGRAMS:	63✔
375	if (!is_comparison_check) {	126✔
UNCOV 376	throw_fail("FDs cannot be dereferenced directly");	×
377	}
378	break;	63✔
379	case T_SOCKET:	60✔
380	case T_BTF_ID:	30✔
381	// TODO: implement proper access checks for these pointer types.
382	if (!is_comparison_check) {	60✔
UNCOV 383	throw_fail("Unsupported pointer type for memory access");	×
384	}
385	break;	30✔
386	case T_ALLOC_MEM: {	10✔
387	// Treat like shared: offset-bounded access with null check.
388	auto [lb, ub] = lb_ub_access_pair(s, reg.alloc_mem_offset);	10✔
389	check_access_shared(lb, ub, reg.alloc_mem_size);	10✔
390	if (!is_comparison_check && !s.or_null) {	10✔
UNCOV 391	require_value(dom.state, reg.svalue > 0, "Possible null access");	×
392	}
393	break;	10✔
394	}	10✔
UNCOV 395	case T_FUNC:	×
UNCOV 396	if (!is_comparison_check) {	×
UNCOV 397	throw_fail("Function pointers cannot be dereferenced");	×
398	}
399	break;
400	default: throw_fail("Invalid type");	479✔
401	}
402	}	190,976✔
403	}	190,074✔
404
405	void EbpfChecker::operator()(const ZeroCtxOffset& s) const {	10,930✔
406	using namespace dsl_syntax;	5,465✔
407	const auto reg = reg_pack(s.reg);	10,930✔
408	// The domain is not expressive enough to handle join of null and non-null ctx,
409	// Since non-null ctx pointers are nonzero numbers.
410	if (s.or_null && dom.state.is_in_group(s.reg, TS_NUM) && dom.state.values.entail(reg.uvalue == 0)) {	16,443✔
411	return;	24✔
412	}
413	require_value(dom.state, reg.ctx_offset == 0, "Nonzero context offset");	21,816✔
414	}
415
416	} // 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