22160684311

Committed 18 Feb 2026 09:20PM UTC coverage: 88.256% (+1.1%) from 87.142%

Build # 22160684311

Build Type

push

github

Committed by

elazarg

Commit Message

lint

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

Coverage Stats

78 of 82 new or added lines in 6 files covered. (95.12%)

402 existing lines in 18 files now uncovered.

10731 of 12159 relevant lines covered (88.26%)

837642.51 hits per line

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

96.96

/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 ValidCall&) 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 ValidCall& s) const {
    if (!s.stack_frame_prefix.empty()) {
        const EbpfHelperPrototype proto = thread_local_program_info->platform->get_helper_prototype(s.func);
        if (proto.return_type == EBPF_RETURN_TYPE_INTEGER_OR_NO_RETURN_IF_SUCCEED) {
            throw_fail("tail call not supported in subprogram");
        }
    }
}

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");
                } 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;
        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 {	352✔
24	public:
25	explicit EbpfChecker(const EbpfDomain& dom, Assertion assertion) : assertion{std::move(assertion)}, dom(dom) {}	310,020✔
26
27	void visit() { std::visit(*this, assertion); }	206,680✔
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 ValidCall&) 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 {	86,952✔
44	if (!inv.values.entail(cst)) {	130,428✔
45	throw_fail(msg);	448✔
46	}
47	}	86,504✔
48
49	[[noreturn]]
50	void throw_fail(const std::string& msg) const {	684✔
51	throw VerificationError(msg + " (" + to_string(assertion) + ")");	1,026✔
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,	344,530✔
68	const Label& where) {
69	if (dom.is_bottom()) {	344,530✔
70	return {};	138,088✔
71	}
72	try {	103,221✔
73	EbpfChecker{dom, assertion}.visit();	311,031✔
74	} catch (VerificationError& error) {	684✔
75	error.where = where;	684✔
76	return {error};	684✔
77	}	684✔
78	return {};	205,758✔
79	}
80
81	void EbpfChecker::check_access_stack(const LinearExpression& lb, const LinearExpression& ub) const {	4,996✔
82	using namespace dsl_syntax;	2,498✔
83	require_value(dom.state, reg_pack(R10_STACK_POINTER).stack_offset - EBPF_SUBPROGRAM_STACK_SIZE <= lb,	12,496✔
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");	7,499✔
86	}	4,990✔
87
88	void EbpfChecker::check_access_context(const LinearExpression& lb, const LinearExpression& ub) const {	7,860✔
89	using namespace dsl_syntax;	2,620✔
90	require_value(dom.state, lb >= 0, "Lower bound must be at least 0");	7,860✔
91	require_value(dom.state, ub <= thread_local_program_info->type.context_descriptor->size,	10,483✔
92	std::string("Upper bound must be at most ") +	10,483✔
93	std::to_string(thread_local_program_info->type.context_descriptor->size));	7,861✔
94	}	5,238✔
95
96	void EbpfChecker::check_access_packet(const LinearExpression& lb, const LinearExpression& ub,	8,532✔
97	const std::optional<Variable> packet_size) const {
98	using namespace dsl_syntax;	4,266✔
99	require_value(dom.state, lb >= variable_registry->meta_offset(), "Lower bound must be at least meta_offset");	17,068✔
100	if (packet_size) {	8,530✔
101	require_value(dom.state, ub <= *packet_size, "Upper bound must be at most packet_size");	9,125✔
102	} else {
103	require_value(dom.state, ub <= MAX_PACKET_SIZE,	6,246✔
104	std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));	12,492✔
105	}
106	}	8,268✔
107
108	void EbpfChecker::check_access_shared(const LinearExpression& lb, const LinearExpression& ub,	13,574✔
109	const Variable shared_region_size) const {
110	using namespace dsl_syntax;	6,787✔
111	require_value(dom.state, lb >= 0, "Lower bound must be at least 0");	20,361✔
112	require_value(dom.state, ub <= shared_region_size,	27,202✔
113	std::string("Upper bound must be at most ") + variable_registry->name(shared_region_size));	40,776✔
114	}	13,538✔
115
116	void EbpfChecker::operator()(const Comparable& s) const {	5,360✔
117	using namespace dsl_syntax;	2,680✔
118	if (dom.state.same_type(s.r1, s.r2)) {	5,360✔
119	// Same type. If both are numbers, that's okay. Otherwise:
120	TypeDomain non_number_types = dom.state.types;	5,350✔
121	non_number_types.remove_type(reg_type(s.r2), T_NUM);	5,350✔
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)) {	5,350✔
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});	5,348✔
128	this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r2, 0, Imm{0}, false});	5,346✔
129	} else {	5,350✔
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	}	5,350✔
137
138	void EbpfChecker::operator()(const Addable& s) const {	4,122✔
139	if (!dom.state.implies_superset(s.ptr, TS_POINTER, s.num, TS_NUM)) {	4,122✔
140	throw_fail("Only numbers can be added to pointers");	3✔
141	}
142	}	4,120✔
143
144	void EbpfChecker::operator()(const ValidDivisor& s) const {	280✔
145	using namespace dsl_syntax;	140✔
146	if (!dom.state.implies_superset(s.reg, TS_POINTER, s.reg, TS_NUM)) {	280✔
147	throw_fail("Only numbers can be used as divisors");	24✔
148	}
149	if (!thread_local_options.allow_division_by_zero) {	268✔
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	}	204✔
155
156	void EbpfChecker::operator()(const ValidStore& s) const {	914✔
157	if (!dom.state.implies_not_type(s.mem, T_STACK, s.val, TS_NUM)) {	914✔
158	throw_fail("Only numbers can be stored to externally-visible regions");	3✔
159	}
160	}	912✔
161
162	void EbpfChecker::operator()(const TypeConstraint& s) const {	127,586✔
163	if (!dom.state.is_in_group(s.reg, to_typeset(s.types))) {	127,586✔
164	throw_fail("Invalid type");	306✔
165	}
166	}	127,382✔
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, {})) {	260✔
191	// TODO: create explicit sub assertions elsewhere
192	EbpfChecker{dom, sub_assertion}.visit();	397✔
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 {	4,524✔
201	using namespace dsl_syntax;	2,262✔
202	const auto r = reg_pack(s.reg);	4,524✔
203	require_value(dom.state, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size");	11,320✔
204	}	4,522✔
205
206	void EbpfChecker::operator()(const ValidCall& s) const {	10,494✔
207	if (!s.stack_frame_prefix.empty()) {	10,494✔
208	const EbpfHelperPrototype proto = thread_local_program_info->platform->get_helper_prototype(s.func);	2✔
209	if (proto.return_type == EBPF_RETURN_TYPE_INTEGER_OR_NO_RETURN_IF_SUCCEED) {	2✔
210	throw_fail("tail call not supported in subprogram");	3✔
211	}
212	}
213	}	10,492✔
214
215	void EbpfChecker::operator()(const ValidMapKeyValue& s) const {	4,224✔
216	using namespace dsl_syntax;	2,112✔
217
218	const auto fd_type = dom.get_map_type(s.map_fd_reg);	4,224✔
219
220	const auto access_reg = reg_pack(s.access_reg);	4,224✔
221	int width;	2,112✔
222	if (s.key) {	4,224✔
223	const auto key_size = dom.get_map_key_size(s.map_fd_reg).singleton();	3,510✔
224	if (!key_size.has_value()) {	3,510✔
UNCOV 225	throw_fail("Map key size is not singleton");	×
226	}
227	width = key_size->narrow<int>();	3,510✔
228	} else {
229	const auto value_size = dom.get_map_value_size(s.map_fd_reg).singleton();	714✔
230	if (!value_size.has_value()) {	714✔
UNCOV 231	throw_fail("Map value size is not singleton");	×
232	}
233	width = value_size->narrow<int>();	714✔
234	}
235
236	for (const auto access_reg_type : dom.state.enumerate_types(s.access_reg)) {	8,406✔
237	if (access_reg_type == T_STACK) {	4,224✔
238	Interval offset = dom.state.values.eval_interval(access_reg.stack_offset);	4,150✔
239	if (!dom.stack.all_num_width(offset, Interval{width})) {	4,150✔
240	auto lb_is = offset.lb().number();	22✔
241	std::string lb_s = lb_is && lb_is->fits<int32_t>() ? std::to_string(lb_is->narrow<int32_t>()) : "-oo";	24✔
242	Interval ub = offset + Interval{width};	22✔
243	auto ub_is = ub.ub().number();	22✔
244	std::string ub_s = ub_is && ub_is->fits<int32_t>() ? std::to_string(ub_is->narrow<int32_t>()) : "oo";	35✔
245	require_value(dom.state, LinearConstraint::false_const(),	44✔
246	"Illegal map update with a non-numerical value [" + lb_s + "-" + ub_s + ")");	143✔
247	} else if (thread_local_options.strict && fd_type.has_value()) {	4,172✔
248	EbpfMapType map_type = thread_local_program_info->platform->get_map_type(*fd_type);	4✔
249	if (map_type.is_array) {	4✔
250	// Get offset value.
251	Variable key_ptr = access_reg.stack_offset;	4✔
252	std::optional<Number> offset_num = dom.state.values.eval_interval(key_ptr).singleton();	4✔
253	if (!offset_num.has_value()) {	4✔
UNCOV 254	throw_fail("Pointer must be a singleton");	×
255	} else if (s.key) {	4✔
256	// Look up the value pointed to by the key pointer.
257	Variable key_value =	2✔
258	variable_registry->cell_var(DataKind::svalues, offset_num.value(), sizeof(uint32_t));	4✔
259
260	if (auto max_entries = dom.get_map_max_entries(s.map_fd_reg).lb().number()) {	6✔
261	require_value(dom.state, key_value < *max_entries, "Array index overflow");	16✔
262	} else {
UNCOV 263	throw_fail("Max entries is not finite");	×
264	}
265	require_value(dom.state, key_value >= 0, "Array index underflow");	2✔
266	}
267	}
268	}	4✔
269	} else if (access_reg_type == T_PACKET) {	74✔
270	Variable lb = access_reg.packet_offset;	44✔
271	LinearExpression ub = lb + width;	66✔
272	check_access_packet(lb, ub, {});	66✔
273	// Packet memory is both readable and writable.
274	} else if (access_reg_type == T_SHARED) {	74✔
275	Variable lb = access_reg.shared_offset;	30✔
276	LinearExpression ub = lb + width;	45✔
277	check_access_shared(lb, ub, access_reg.shared_region_size);	38✔
278	require_value(dom.state, access_reg.svalue > 0, "Possible null access");	68✔
279	// Shared memory is zero-initialized when created so is safe to read and write.
280	} else {	30✔
281	throw_fail("Only stack, packet, or shared can be used as a parameter");	21✔
282	}
283	}	4,224✔
284	}	4,182✔
285
286	static std::tuple<LinearExpression, LinearExpression> lb_ub_access_pair(const ValidAccess& s,	32,268✔
287	const Variable offset_var) {
288	using namespace dsl_syntax;	16,134✔
289	LinearExpression lb = offset_var + s.offset;	48,402✔
290	LinearExpression ub = std::holds_alternative<Imm>(s.width) ? lb + std::get<Imm>(s.width).v	46,259✔
291	: lb + reg_pack(std::get<Reg>(s.width)).svalue;	60,250✔
292	return {lb, ub};	48,402✔
293	}	32,268✔
294
295	void EbpfChecker::operator()(const ValidAccess& s) const {	53,930✔
296	using namespace dsl_syntax;	26,965✔
297
298	const bool is_comparison_check = s.width == Value{Imm{0}};	53,930✔
299
300	const auto reg = reg_pack(s.reg);	53,930✔
301	for (const auto type : dom.state.enumerate_types(s.reg)) {	107,742✔
302	switch (type) {	54,128✔
303	case T_PACKET: {	8,488✔
304	auto [lb, ub] = lb_ub_access_pair(s, reg.packet_offset);	8,488✔
305	const std::optional<Variable> packet_size =	4,244✔
306	is_comparison_check ? std::optional<Variable>{} : variable_registry->packet_size();	8,620✔
307	check_access_packet(lb, ub, packet_size);	8,488✔
308	// if within bounds, it can never be null
309	// Context memory is both readable and writable.
310	break;	8,224✔
311	}	8,488✔
312	case T_STACK: {	4,996✔
313	auto [lb, ub] = lb_ub_access_pair(s, reg.stack_offset);	4,996✔
314	check_access_stack(lb, ub);	4,996✔
315	// if within bounds, it can never be null
316	if (s.access_type == AccessType::read &&	8,626✔
317	!dom.stack.all_num_lb_ub(dom.state.values.eval_interval(lb), dom.state.values.eval_interval(ub))) {	8,537✔
318
319	if (s.offset < 0) {	178✔
UNCOV 320	throw_fail("Stack content is not numeric");	×
321	} else {
322	using namespace dsl_syntax;	89✔
323	LinearExpression w = std::holds_alternative<Imm>(s.width)	178✔
324	? LinearExpression{std::get<Imm>(s.width).v}	178✔
325	: reg_pack(std::get<Reg>(s.width)).svalue;	186✔
326
327	require_value(dom.state, w <= reg.stack_numeric_size - s.offset, "Stack content is not numeric");	391✔
328	}	178✔
329	}
330	break;	4,980✔
331	}	4,996✔
332	case T_CTX: {	5,240✔
333	auto [lb, ub] = lb_ub_access_pair(s, reg.ctx_offset);	5,240✔
334	check_access_context(lb, ub);	5,240✔
335	// if within bounds, it can never be null
336	// The context is both readable and writable.
337	break;	5,238✔
338	}	5,240✔
339	case T_SHARED: {	13,544✔
340	auto [lb, ub] = lb_ub_access_pair(s, reg.shared_offset);	13,544✔
341	check_access_shared(lb, ub, reg.shared_region_size);	13,544✔
342	if (!is_comparison_check && !s.or_null) {	13,516✔
343	require_value(dom.state, reg.svalue > 0, "Possible null access");	28,431✔
344	}
345	// Shared memory is zero-initialized when created so is safe to read and write.
346	break;	13,510✔
347	}	13,544✔
348	case T_NUM:	21,800✔
349	if (!is_comparison_check) {	21,800✔
350	if (s.or_null) {	228✔
351	require_value(dom.state, reg.svalue == 0, "Non-null number");	456✔
352	} else {
UNCOV 353	throw_fail("Only pointers can be dereferenced");	×
354	}
355	}
356	break;	10,900✔
357	case T_MAP:	60✔
358	case T_MAP_PROGRAMS:	30✔
359	if (!is_comparison_check) {	60✔
UNCOV 360	throw_fail("FDs cannot be dereferenced directly");	×
361	}
362	break;	30✔
363	default: throw_fail("Invalid type");	158✔
364	}
365	}	53,930✔
366	}	53,614✔
367
368	void EbpfChecker::operator()(const ZeroCtxOffset& s) const {	5,852✔
369	using namespace dsl_syntax;	2,926✔
370	const auto reg = reg_pack(s.reg);	5,852✔
371	// The domain is not expressive enough to handle join of null and non-null ctx,
372	// Since non-null ctx pointers are nonzero numbers.
373	if (s.or_null && dom.state.is_in_group(s.reg, TS_NUM) && dom.state.values.entail(reg.uvalue == 0)) {	8,826✔
374	return;	24✔
375	}
376	require_value(dom.state, reg.ctx_offset == 0, "Nonzero context offset");	11,660✔
377	}
378
379	} // namespace prevail

Alan-Jowett / ebpf-verifier / 22160684311

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