18949625295

Committed 28 Oct 2025 10:33AM UTC coverage: 87.448% (-1.0%) from 88.47%

Build # 18949625295

Build Type

push

github

Committed by

elazarg

Commit Message

Bump CLI11 to v2.6.1

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

Run Details

9022 of 10317 relevant lines covered (87.45%)

10783407.68 hits per line

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

97.5

/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 "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);
        }
    }

    void require_type(const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {
        if (!inv.types.inv.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.rcp, 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.rcp, 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.rcp, lb >= 0, "Lower bound must be at least 0");
    require_value(dom.rcp, 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.rcp, lb >= variable_registry->meta_offset(), "Lower bound must be at least meta_offset");
    if (packet_size) {
        require_value(dom.rcp, ub <= *packet_size, "Upper bound must be at most packet_size");
    } else {
        require_value(dom.rcp, 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.rcp, lb >= 0, "Lower bound must be at least 0");
    require_value(dom.rcp, 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.rcp.types.same_type(s.r1, s.r2)) {
        // Same type. If both are numbers, that's okay. Otherwise:
        TypeDomain non_number_types = dom.rcp.types;
        non_number_types.add_constraint(type_is_not_number(s.r2));
        // We must check that they belong to a singleton region:
        if (!non_number_types.is_in_group(s.r1, TypeGroup::singleton_ptr) &&
            !non_number_types.is_in_group(s.r1, TypeGroup::map_fd)) {
            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.
        require_type(dom.rcp, type_is_number(s.r2), "Cannot subtract pointers to different regions");
    }
}

void EbpfChecker::operator()(const Addable& s) const {
    if (!dom.rcp.types.implies(type_is_pointer(s.ptr), type_is_number(s.num))) {
        throw_fail("Only numbers can be added to pointers");
    }
}

void EbpfChecker::operator()(const ValidDivisor& s) const {
    using namespace dsl_syntax;
    if (!dom.rcp.types.implies(type_is_pointer(s.reg), type_is_number(s.reg))) {
        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.rcp, v != 0, "Possible division by zero");
    }
}

void EbpfChecker::operator()(const ValidStore& s) const {
    if (!dom.rcp.types.implies(type_is_not_stack(s.mem), type_is_number(s.val))) {
        throw_fail("Only numbers can be stored to externally-visible regions");
    }
}

void EbpfChecker::operator()(const TypeConstraint& s) const {
    if (!dom.rcp.types.is_in_group(s.reg, 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.rcp, counter <= BoundedLoopCount::limit, "Loop counter is too large");
}

void EbpfChecker::operator()(const FuncConstraint& s) const {
    // Look up the helper function id.
    if (dom.rcp.is_bottom()) {
        return;
    }
    const auto src_interval = dom.rcp.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.rcp, 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.rcp.enumerate_types(s.access_reg)) {
        if (access_reg_type == T_STACK) {
            Interval offset = dom.rcp.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.rcp, 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.rcp.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.rcp, key_value < *max_entries, "Array index overflow");
                        } else {
                            throw_fail("Max entries is not finite");
                        }
                        require_value(dom.rcp, 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.rcp, 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.rcp.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.rcp.values.eval_interval(lb), dom.rcp.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.rcp, 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.rcp, 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.rcp, 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.rcp.types.get_type(s.reg) == T_NUM && dom.rcp.values.entail(reg.uvalue == 0)) {
        return;
    }
    require_value(dom.rcp, 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
10	#include "arith/dsl_syntax.hpp"
11	#include "config.hpp"
12	#include "crab/array_domain.hpp"
13	#include "crab/ebpf_domain.hpp"
14	#include "crab/var_registry.hpp"
15	#include "ir/program.hpp"
16	#include "ir/syntax.hpp"
17	#include "ir/unmarshal.hpp"
18	#include "platform.hpp"
19
20	namespace prevail {
21
22	class EbpfChecker final {	340✔
23	public:
24	explicit EbpfChecker(const EbpfDomain& dom, Assertion assertion) : assertion{std::move(assertion)}, dom(dom) {}	307,164✔
25
26	void visit() { std::visit(*this, assertion); }	204,776✔
27
28	void operator()(const Addable&) const;
29	void operator()(const BoundedLoopCount&) const;
30	void operator()(const Comparable&) const;
31	void operator()(const FuncConstraint&) const;
32	void operator()(const ValidDivisor&) const;
33	void operator()(const TypeConstraint&) const;
34	void operator()(const ValidAccess&) const;
35	void operator()(const ValidCall&) const;
36	void operator()(const ValidMapKeyValue&) const;
37	void operator()(const ValidSize&) const;
38	void operator()(const ValidStore&) const;
39	void operator()(const ZeroCtxOffset&) const;
40
41	private:
42	void require_value(const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {	86,658✔
43	if (!inv.values.entail(cst)) {	129,987✔
44	throw_fail(msg);	436✔
45	}
46	}	86,222✔
47
48	void require_type(const TypeToNumDomain& inv, const LinearConstraint& cst, const std::string& msg) const {	10✔
49	if (!inv.types.inv.entail(cst)) {	15✔
50	throw_fail(msg);	6✔
51	}
52	}	4✔
53
54	[[noreturn]]
55	void throw_fail(const std::string& msg) const {	660✔
56	throw VerificationError(msg + " (" + to_string(assertion) + ")");	990✔
57	}
58
59	// memory check / load / store
60	void check_access_stack(const LinearExpression& lb, const LinearExpression& ub) const;
61	void check_access_context(const LinearExpression& lb, const LinearExpression& ub) const;
62	void check_access_packet(const LinearExpression& lb, const LinearExpression& ub,
63	std::optional<Variable> packet_size) const;
64	void check_access_shared(const LinearExpression& lb, const LinearExpression& ub, Variable shared_region_size) const;
65
66	private:
67	const Assertion assertion;
68
69	const EbpfDomain& dom;
70	};
71
72	std::optional<VerificationError> ebpf_domain_check(const EbpfDomain& dom, const Assertion& assertion,	342,502✔
73	const Label& where) {
74	if (dom.is_bottom()) {	342,502✔
75	return {};	137,964✔
76	}
77	try {	102,269✔
78	EbpfChecker{dom, assertion}.visit();	308,127✔
79	} catch (VerificationError& error) {	660✔
80	error.where = where;	660✔
81	return {error};	660✔
82	}	660✔
83	return {};	203,878✔
84	}
85
86	void EbpfChecker::check_access_stack(const LinearExpression& lb, const LinearExpression& ub) const {	4,938✔
87	using namespace dsl_syntax;	2,469✔
88	require_value(dom.rcp, reg_pack(R10_STACK_POINTER).stack_offset - EBPF_SUBPROGRAM_STACK_SIZE <= lb,	17,289✔
89	"Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE");
90	require_value(dom.rcp, ub <= EBPF_TOTAL_STACK_SIZE, "Upper bound must be at most EBPF_TOTAL_STACK_SIZE");	9,880✔
91	}	4,932✔
92
93	void EbpfChecker::check_access_context(const LinearExpression& lb, const LinearExpression& ub) const {	5,236✔
94	using namespace dsl_syntax;	2,618✔
95	require_value(dom.rcp, lb >= 0, "Lower bound must be at least 0");	10,480✔
96	require_value(dom.rcp, ub <= thread_local_program_info->type.context_descriptor->size,	10,467✔
97	std::string("Upper bound must be at most ") +	10,467✔
98	std::to_string(thread_local_program_info->type.context_descriptor->size));	13,082✔
99	}	5,230✔
100
101	void EbpfChecker::check_access_packet(const LinearExpression& lb, const LinearExpression& ub,	8,520✔
102	const std::optional<Variable> packet_size) const {
103	using namespace dsl_syntax;	4,260✔
104	require_value(dom.rcp, lb >= variable_registry->meta_offset(), "Lower bound must be at least meta_offset");	17,044✔
105	if (packet_size) {	8,518✔
106	require_value(dom.rcp, ub <= *packet_size, "Upper bound must be at most packet_size");	9,111✔
107	} else {
108	require_value(dom.rcp, ub <= MAX_PACKET_SIZE,	6,234✔
109	std::string{"Upper bound must be at most "} + std::to_string(MAX_PACKET_SIZE));	12,468✔
110	}
111	}	8,260✔
112
113	void EbpfChecker::check_access_shared(const LinearExpression& lb, const LinearExpression& ub,	13,526✔
114	const Variable shared_region_size) const {
115	using namespace dsl_syntax;	6,763✔
116	require_value(dom.rcp, lb >= 0, "Lower bound must be at least 0");	27,052✔
117	require_value(dom.rcp, ub <= shared_region_size,	27,106✔
118	std::string("Upper bound must be at most ") + variable_registry->name(shared_region_size));	40,632✔
119	}	13,490✔
120
121	void EbpfChecker::operator()(const Comparable& s) const {	5,212✔
122	using namespace dsl_syntax;	2,606✔
123	if (dom.rcp.types.same_type(s.r1, s.r2)) {	5,212✔
124	// Same type. If both are numbers, that's okay. Otherwise:
125	TypeDomain non_number_types = dom.rcp.types;	5,202✔
126	non_number_types.add_constraint(type_is_not_number(s.r2));	7,803✔
127	// We must check that they belong to a singleton region:
128	if (!non_number_types.is_in_group(s.r1, TypeGroup::singleton_ptr) &&	5,210✔
129	!non_number_types.is_in_group(s.r1, TypeGroup::map_fd)) {	8✔
130	throw_fail("Cannot subtract pointers to non-singleton regions");	4✔
131	}
132	// And, to avoid wraparound errors, they must be within bounds.
133	this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r1, 0, Imm{0}, false});	5,200✔
134	this->operator()(ValidAccess{MAX_CALL_STACK_FRAMES, s.r2, 0, Imm{0}, false});	5,200✔
135	} else {	5,202✔
136	// _Maybe_ different types, so r2 must be a number.
137	// We checked in a previous assertion that r1 is a pointer or a number.
138	require_type(dom.rcp, type_is_number(s.r2), "Cannot subtract pointers to different regions");	23✔
139	}
140	}	5,202✔
141
142	void EbpfChecker::operator()(const Addable& s) const {	4,090✔
143	if (!dom.rcp.types.implies(type_is_pointer(s.ptr), type_is_number(s.num))) {	4,090✔
144	throw_fail("Only numbers can be added to pointers");	3✔
145	}
146	}	4,088✔
147
148	void EbpfChecker::operator()(const ValidDivisor& s) const {	240✔
149	using namespace dsl_syntax;	120✔
150	if (!dom.rcp.types.implies(type_is_pointer(s.reg), type_is_number(s.reg))) {	240✔
151	throw_fail("Only numbers can be used as divisors");	24✔
152	}
153	if (!thread_local_options.allow_division_by_zero) {	228✔
154	const auto reg = reg_pack(s.reg);	64✔
155	const auto v = s.is_signed ? reg.svalue : reg.uvalue;	64✔
156	require_value(dom.rcp, v != 0, "Possible division by zero");	320✔
157	}
158	}	164✔
159
160	void EbpfChecker::operator()(const ValidStore& s) const {	910✔
161	if (!dom.rcp.types.implies(type_is_not_stack(s.mem), type_is_number(s.val))) {	910✔
162	throw_fail("Only numbers can be stored to externally-visible regions");	3✔
163	}
164	}	908✔
165
166	void EbpfChecker::operator()(const TypeConstraint& s) const {	126,414✔
167	if (!dom.rcp.types.is_in_group(s.reg, s.types)) {	126,414✔
168	throw_fail("Invalid type");	288✔
169	}
170	}	126,222✔
171
172	void EbpfChecker::operator()(const BoundedLoopCount& s) const {	32✔
173	// Enforces an upper bound on loop iterations by checking that the loop counter
174	// does not exceed the specified limit
175	using namespace dsl_syntax;	16✔
176	const auto counter = variable_registry->loop_counter(to_string(s.name));	32✔
177	require_value(dom.rcp, counter <= BoundedLoopCount::limit, "Loop counter is too large");	124✔
178	}	12✔
179
180	void EbpfChecker::operator()(const FuncConstraint& s) const {	48✔
181	// Look up the helper function id.
182	if (dom.rcp.is_bottom()) {	48✔
183	return;
184	}
185	const auto src_interval = dom.rcp.values.eval_interval(reg_pack(s.reg).svalue);	48✔
186	if (const auto sn = src_interval.singleton()) {	48✔
187	if (sn->fits<int32_t>()) {	46✔
188	// We can now process it as if the id was immediate.
189	const int32_t imm = sn->cast_to<int32_t>();	46✔
190	if (!thread_local_program_info->platform->is_helper_usable(imm)) {	46✔
191	throw_fail("invalid helper function id " + std::to_string(imm));	22✔
192	}
193	const Call call = make_call(imm, *thread_local_program_info->platform);	42✔
194	for (const Assertion& sub_assertion : get_assertions(call, *thread_local_program_info, {})) {	260✔
195	// TODO: create explicit sub assertions elsewhere
196	EbpfChecker{dom, sub_assertion}.visit();	397✔
197	}	42✔
198	return;	22✔
199	}	42✔
200	}	47✔
201	throw_fail("callx helper function id is not a valid singleton");	16✔
202	}	35✔
203
204	void EbpfChecker::operator()(const ValidSize& s) const {	4,524✔
205	using namespace dsl_syntax;	2,262✔
206	const auto r = reg_pack(s.reg);	4,524✔
207	require_value(dom.rcp, s.can_be_zero ? r.svalue >= 0 : r.svalue > 0, "Invalid size");	9,058✔
208	}	4,522✔
209
210	void EbpfChecker::operator()(const ValidCall& s) const {	10,474✔
211	if (!s.stack_frame_prefix.empty()) {	10,474✔
212	const EbpfHelperPrototype proto = thread_local_program_info->platform->get_helper_prototype(s.func);	2✔
213	if (proto.return_type == EBPF_RETURN_TYPE_INTEGER_OR_NO_RETURN_IF_SUCCEED) {	2✔
214	throw_fail("tail call not supported in subprogram");	3✔
215	}
216	}
217	}	10,472✔
218
219	void EbpfChecker::operator()(const ValidMapKeyValue& s) const {	4,202✔
220	using namespace dsl_syntax;	2,101✔
221
222	const auto fd_type = dom.get_map_type(s.map_fd_reg);	4,202✔
223
224	const auto access_reg = reg_pack(s.access_reg);	4,202✔
225	int width;	2,101✔
226	if (s.key) {	4,202✔
227	const auto key_size = dom.get_map_key_size(s.map_fd_reg).singleton();	3,492✔
228	if (!key_size.has_value()) {	3,492✔
229	throw_fail("Map key size is not singleton");	×
230	}
231	width = key_size->narrow<int>();	3,492✔
232	} else {	3,492✔
233	const auto value_size = dom.get_map_value_size(s.map_fd_reg).singleton();	710✔
234	if (!value_size.has_value()) {	710✔
235	throw_fail("Map value size is not singleton");	×
236	}
237	width = value_size->narrow<int>();	710✔
238	}	710✔
239
240	for (const auto access_reg_type : dom.rcp.enumerate_types(s.access_reg)) {	8,366✔
241	if (access_reg_type == T_STACK) {	4,202✔
242	Interval offset = dom.rcp.values.eval_interval(access_reg.stack_offset);	4,128✔
243	if (!dom.stack.all_num_width(offset, Interval{width})) {	6,192✔
244	auto lb_is = offset.lb().number();	47✔
245	std::string lb_s = lb_is && lb_is->fits<int32_t>() ? std::to_string(lb_is->narrow<int32_t>()) : "-oo";	29✔
246	Interval ub = offset + Interval{width};	27✔
247	auto ub_is = ub.ub().number();	45✔
248	std::string ub_s = ub_is && ub_is->fits<int32_t>() ? std::to_string(ub_is->narrow<int32_t>()) : "oo";	29✔
249	require_value(dom.rcp, LinearConstraint::false_const(),	36✔
250	"Illegal map update with a non-numerical value [" + lb_s + "-" + ub_s + ")");	117✔
251	} else if (thread_local_options.strict && fd_type.has_value()) {	4,200✔
252	EbpfMapType map_type = thread_local_program_info->platform->get_map_type(*fd_type);	4✔
253	if (map_type.is_array) {	4✔
254	// Get offset value.
255	Variable key_ptr = access_reg.stack_offset;	4✔
256	std::optional<Number> offset_num = dom.rcp.values.eval_interval(key_ptr).singleton();	8✔
257	if (!offset_num.has_value()) {	4✔
258	throw_fail("Pointer must be a singleton");	×
259	} else if (s.key) {	4✔
260	// Look up the value pointed to by the key pointer.
261	Variable key_value =	2✔
262	variable_registry->cell_var(DataKind::svalues, offset_num.value(), sizeof(uint32_t));	4✔
263
264	if (auto max_entries = dom.get_map_max_entries(s.map_fd_reg).lb().number()) {	10✔
265	require_value(dom.rcp, key_value < *max_entries, "Array index overflow");	22✔
266	} else {
267	throw_fail("Max entries is not finite");	2✔
268	}	4✔
269	require_value(dom.rcp, key_value >= 0, "Array index underflow");	2✔
270	}
271	}	4✔
272	}	4✔
273	} else if (access_reg_type == T_PACKET) {	4,202✔
274	Variable lb = access_reg.packet_offset;	44✔
275	LinearExpression ub = lb + width;	66✔
276	check_access_packet(lb, ub, {});	44✔
277	// Packet memory is both readable and writable.
278	} else if (access_reg_type == T_SHARED) {	74✔
279	Variable lb = access_reg.shared_offset;	30✔
280	LinearExpression ub = lb + width;	45✔
281	check_access_shared(lb, ub, access_reg.shared_region_size);	34✔
282	require_value(dom.rcp, access_reg.svalue > 0, "Possible null access");	79✔
283	// Shared memory is zero-initialized when created so is safe to read and write.
284	} else {	30✔
285	throw_fail("Only stack, packet, or shared can be used as a parameter");	19✔
286	}
287	}	4,202✔
288	}	4,164✔
289
290	static std::tuple<LinearExpression, LinearExpression> lb_ub_access_pair(const ValidAccess& s,	32,146✔
291	const Variable offset_var) {
292	using namespace dsl_syntax;	16,073✔
293	LinearExpression lb = offset_var + s.offset;	48,219✔
294	LinearExpression ub = std::holds_alternative<Imm>(s.width) ? lb + std::get<Imm>(s.width).v	46,076✔
295	: lb + reg_pack(std::get<Reg>(s.width)).svalue;	46,076✔
296	return {lb, ub};	64,292✔
297	}	32,146✔
298
299	void EbpfChecker::operator()(const ValidAccess& s) const {	53,176✔
300	using namespace dsl_syntax;	26,588✔
301
302	const bool is_comparison_check = s.width == Value{Imm{0}};	53,176✔
303
304	const auto reg = reg_pack(s.reg);	53,176✔
305	for (const auto type : dom.rcp.enumerate_types(s.reg)) {	106,236✔
306	switch (type) {	53,370✔
307	case T_PACKET: {	8,476✔
308	auto [lb, ub] = lb_ub_access_pair(s, reg.packet_offset);	8,476✔
309	const std::optional<Variable> packet_size =	4,238✔
310	is_comparison_check ? std::optional<Variable>{} : variable_registry->packet_size();	8,606✔
311	check_access_packet(lb, ub, packet_size);	8,476✔
312	// if within bounds, it can never be null
313	// Context memory is both readable and writable.
314	break;	8,216✔
315	}	8,476✔
316	case T_STACK: {	4,938✔
317	auto [lb, ub] = lb_ub_access_pair(s, reg.stack_offset);	4,938✔
318	check_access_stack(lb, ub);	4,938✔
319	// if within bounds, it can never be null
320	if (s.access_type == AccessType::read &&	8,562✔
321	!dom.stack.all_num_lb_ub(dom.rcp.values.eval_interval(lb), dom.rcp.values.eval_interval(ub))) {	12,192✔
322
323	if (s.offset < 0) {	176✔
324	throw_fail("Stack content is not numeric");	×
325	} else {
326	using namespace dsl_syntax;	88✔
327	LinearExpression w = std::holds_alternative<Imm>(s.width)	176✔
328	? LinearExpression{std::get<Imm>(s.width).v}	176✔
329	: reg_pack(std::get<Reg>(s.width)).svalue;	183✔
330
331	require_value(dom.rcp, w <= reg.stack_numeric_size - s.offset, "Stack content is not numeric");	384✔
332	}	176✔
333	}
334	break;	4,924✔
335	}	4,938✔
336	case T_CTX: {	5,236✔
337	auto [lb, ub] = lb_ub_access_pair(s, reg.ctx_offset);	5,236✔
338	check_access_context(lb, ub);	5,236✔
339	// if within bounds, it can never be null
340	// The context is both readable and writable.
341	break;	5,230✔
342	}	5,236✔
343	case T_SHARED: {	13,496✔
344	auto [lb, ub] = lb_ub_access_pair(s, reg.shared_offset);	13,496✔
345	check_access_shared(lb, ub, reg.shared_region_size);	13,496✔
346	if (!is_comparison_check && !s.or_null) {	13,468✔
347	require_value(dom.rcp, reg.svalue > 0, "Possible null access");	34,009✔
348	}
349	// Shared memory is zero-initialized when created so is safe to read and write.
350	break;	13,466✔
351	}	13,496✔
352	case T_NUM:	21,164✔
353	if (!is_comparison_check) {	21,164✔
354	if (s.or_null) {	228✔
355	require_value(dom.rcp, reg.svalue == 0, "Non-null number");	570✔
356	} else {
357	throw_fail("Only pointers can be dereferenced");	×
358	}
359	}
360	break;	10,582✔
361	case T_MAP:	60✔
362	case T_MAP_PROGRAMS:	30✔
363	if (!is_comparison_check) {	60✔
364	throw_fail("FDs cannot be dereferenced directly");	×
365	}
366	break;	30✔
367	default: throw_fail("Invalid type");	155✔
368	}
369	}	53,176✔
370	}	52,866✔
371
372	void EbpfChecker::operator()(const ZeroCtxOffset& s) const {	5,852✔
373	using namespace dsl_syntax;	2,926✔
374	const auto reg = reg_pack(s.reg);	5,852✔
375	// The domain is not expressive enough to handle join of null and non-null ctx,
376	// Since non-null ctx pointers are nonzero numbers.
377	if (s.or_null && dom.rcp.types.get_type(s.reg) == T_NUM && dom.rcp.values.entail(reg.uvalue == 0)) {	8,790✔
378	return;	24✔
379	}
380	require_value(dom.rcp, reg.ctx_offset == 0, "Nonzero context offset");	14,575✔
381	}
382
383	} // namespace prevail

Alan-Jowett / ebpf-verifier / 18949625295

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