27778108035

Committed 07 Jun 2026 06:51PM UTC coverage: 86.386% (-2.5%) from 88.93%

Build # 27778108035

Build Type

push

github

Committed by

elazarg

Commit Message

Release v0.2.5

Bump project version to 0.2.5 and add a CHANGELOG entry covering ELF loader hardening, numeric-domain soundness fixes, and the writable helper output initialization documentation update since v0.2.4. Also updates the using_installed_package example version requirement.

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

Coverage Stats

9125 of 10563 relevant lines covered (86.39%)

6334294.72 hits per line

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

90.99

/src/ir/assertions.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#include <cassert>
#include <cinttypes>
#include <utility>
#include <vector>

#include "config.hpp"
#include "ir/call_resolver.hpp"
#include "ir/syntax.hpp"
#include "platform.hpp"

using std::string;
using std::to_string;
using std::vector;

namespace prevail {
class AssertExtractor {
    const ProgramInfo& info;
    const RuntimeConfig& runtime;
    const std::optional<Label>& current_label; ///< Pre-simplification label this assert is part of.

    static Imm imm(const Value& v) { return std::get<Imm>(v); }

    static vector<Assertion> zero_offset_ctx(const Reg reg, const bool or_null) {
        vector<Assertion> res;
        res.emplace_back(TypeConstraint{reg, or_null ? TypeGroup::ctx_or_num : TypeGroup::ctx});
        res.emplace_back(ZeroCtxOffset{reg, or_null});
        return res;
    }

    [[nodiscard]]
    ValidAccess make_valid_access(const Reg reg, const int32_t offset = {}, const Value& width = Imm{0},
                                  const bool or_null = {}, const AccessType access_type = {}) const {
        const int depth = current_label.has_value() ? current_label.value().call_stack_depth() : 1;
        return ValidAccess{depth, reg, offset, width, or_null, access_type};
    }

  public:
    explicit AssertExtractor(const ProgramInfo& info, const RuntimeConfig& runtime, const std::optional<Label>& label)
        : info{info}, runtime{runtime}, current_label{label} {}

    vector<Assertion> operator()(const Undefined&) const { return {}; }

    vector<Assertion> operator()(const IncrementLoopCounter& ipc) const { return {{BoundedLoopCount{ipc.name}}}; }

    vector<Assertion> operator()(const LoadMapFd&) const { return {}; }
    vector<Assertion> operator()(const LoadMapAddress&) const { return {}; }
    vector<Assertion> operator()(const LoadPseudo& pseudo) const {
        switch (pseudo.addr.kind) {
        case PseudoAddress::Kind::CODE_ADDR:
            // Type/offset semantics are handled during abstract transformation.
            return {};
        case PseudoAddress::Kind::VARIABLE_ADDR: [[fallthrough]];
        case PseudoAddress::Kind::MAP_BY_IDX: [[fallthrough]];
        case PseudoAddress::Kind::MAP_VALUE_BY_IDX:
            assert(false && "unexpected LoadPseudo kind after CFG construction");
            return {};
        }
        return {};
    }

    /// Packet access implicitly uses R6, so verify that R6 still has a pointer to the context.
    vector<Assertion> operator()(const Packet&) const { return zero_offset_ctx({6}, false); }

    vector<Assertion> operator()(const Exit&) const {
        vector<Assertion> res;
        if (current_label->stack_frame_prefix.empty()) {
            // Verify that Exit returns a number.
            res.emplace_back(TypeConstraint{Reg{R0_RETURN_VALUE}, TypeGroup::number});
        }
        return res;
    }

    vector<Assertion> operator()(const Call& call) const {
        // Invariant: cfg_builder::check_instruction_feature_support has already
        // rejected unsupported calls, so resolved.contract below is the real
        // contract for this (func, kind) key. An unsupported call would have
        // an empty contract and produce no preconditions here -- sound only
        // because the cfg_builder gate ensures we never reach that state.
        const ResolvedCall resolved = resolve(call, info);
        vector<Assertion> res;
        std::optional<Reg> map_fd_reg;
        for (ArgSingle arg : resolved.contract.singles) {
            switch (arg.kind) {
            case ArgSingle::Kind::ANYTHING:
                // avoid pointer leakage:
                if (!info.type.is_privileged) {
                    res.emplace_back(TypeConstraint{arg.reg, TypeGroup::number});
                }
                break;
            case ArgSingle::Kind::MAP_FD_PROGRAMS:
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd_programs});
                // Do not update map_fd_reg
                break;
            case ArgSingle::Kind::MAP_FD:
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd});
                map_fd_reg = arg.reg;
                break;
            case ArgSingle::Kind::PTR_TO_MAP_KEY: [[fallthrough]];
            case ArgSingle::Kind::PTR_TO_MAP_VALUE:
                assert(map_fd_reg);
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});
                res.emplace_back(ValidMapKeyValue{arg.reg, *map_fd_reg, arg.kind == ArgSingle::Kind::PTR_TO_MAP_KEY});
                break;
            case ArgSingle::Kind::PTR_TO_STACK:
                res.emplace_back(TypeConstraint{arg.reg, arg.or_null ? TypeGroup::stack_or_num : TypeGroup::stack});
                // TODO: check 0 when null
                break;
            case ArgSingle::Kind::PTR_TO_FUNC:
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::func});
                res.emplace_back(ValidCallbackTarget{arg.reg});
                break;
            case ArgSingle::Kind::PTR_TO_CTX:
                for (const Assertion& a : zero_offset_ctx(arg.reg, arg.or_null)) {
                    res.emplace_back(a);
                }
                break;
            case ArgSingle::Kind::PTR_TO_SOCKET: res.emplace_back(TypeConstraint{arg.reg, TypeGroup::socket}); break;
            case ArgSingle::Kind::PTR_TO_BTF_ID: res.emplace_back(TypeConstraint{arg.reg, TypeGroup::btf_id}); break;
            case ArgSingle::Kind::PTR_TO_ALLOC_MEM:
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::alloc_mem});
                break;
            case ArgSingle::Kind::PTR_TO_SPIN_LOCK:
            case ArgSingle::Kind::PTR_TO_TIMER: res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem}); break;
            case ArgSingle::Kind::CONST_SIZE_OR_ZERO:
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::number});
                res.emplace_back(ValidSize{arg.reg, true});
                break;
            case ArgSingle::Kind::PTR_TO_WRITABLE_LONG:
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});
                res.emplace_back(make_valid_access(arg.reg, 0, Imm{8}, false, AccessType::write));
                break;
            case ArgSingle::Kind::PTR_TO_WRITABLE_INT:
                res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});
                res.emplace_back(make_valid_access(arg.reg, 0, Imm{4}, false, AccessType::write));
                break;
            }
        }
        if (map_fd_reg && resolved.contract.allowed_map_types != 0) {
            res.emplace_back(ValidMapType{*map_fd_reg, resolved.contract.allowed_map_types, resolved.name});
        }
        for (ArgPair arg : resolved.contract.pairs) {
            const auto group = arg.or_null ? TypeGroup::mem_or_num : TypeGroup::mem;
            const auto access_type =
                arg.kind == ArgPair::Kind::PTR_TO_READABLE_MEM ? AccessType::read : AccessType::write;
            res.emplace_back(TypeConstraint{arg.size, TypeGroup::number});
            res.emplace_back(ValidSize{arg.size, arg.can_be_zero});
            res.emplace_back(TypeConstraint{arg.mem, group});
            res.emplace_back(make_valid_access(arg.mem, 0, arg.size, arg.or_null, access_type));
            // TODO: reg is constant (or maybe it's not important)
        }
        for (uint8_t i = 0; i < 5; ++i) {
            if (resolved.contract.zero_args_mask & (1 << i)) {
                const Reg arg_reg{static_cast<uint8_t>(i + 1)};
                res.emplace_back(TypeConstraint{arg_reg, TypeGroup::number});
                res.emplace_back(ValidArgZero{arg_reg});
            }
        }
        return res;
    }

    vector<Assertion> operator()(const CallLocal&) const { return {}; }

    vector<Assertion> operator()(const Callx& callx) const {
        vector<Assertion> res;
        res.emplace_back(TypeConstraint{callx.func, TypeGroup::number});
        res.emplace_back(FuncConstraint{callx.func});
        return res;
    }

    // Rejected before assertion extraction by cfg_builder::check_instruction_feature_support.
    vector<Assertion> operator()(const CallBtf&) const {
        assert(false && "CallBtf should be rejected before assertion extraction");
        return {};
    }

    [[nodiscard]]
    vector<Assertion> explicate(const Condition& cond) const {
        vector<Assertion> res;
        if (info.type.is_privileged) {
            return res;
        }
        if (const auto pimm = std::get_if<Imm>(&cond.right)) {
            if (pimm->v != 0) {
                // no need to check for valid access, it must be a number
                res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});
            } else {
                bool allow_pointers = false;

                switch (cond.op) {
                case Condition::Op::EQ: allow_pointers = true; break;
                case Condition::Op::NE: allow_pointers = true; break;
                case Condition::Op::SET: allow_pointers = true; break;
                case Condition::Op::NSET: allow_pointers = true; break;
                case Condition::Op::LT: allow_pointers = true; break;
                case Condition::Op::LE: allow_pointers = true; break;
                case Condition::Op::GT: allow_pointers = true; break;
                case Condition::Op::GE: allow_pointers = true; break;
                case Condition::Op::SLT: allow_pointers = false; break;
                case Condition::Op::SLE: allow_pointers = false; break;
                case Condition::Op::SGT: allow_pointers = false; break;
                case Condition::Op::SGE: allow_pointers = false; break;
                default: std::unreachable();
                }

                // Only permit pointer comparisons if the operation is 64-bit.
                allow_pointers &= cond.is64;

                if (!allow_pointers) {
                    res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});
                }

                res.emplace_back(make_valid_access(cond.left));
                // OK - map_fd is just another pointer
                // Anything can be compared to 0
            }
        } else {
            const auto reg_right = get<Reg>(cond.right);
            res.emplace_back(make_valid_access(cond.left));
            res.emplace_back(make_valid_access(reg_right));
            if (cond.op != Condition::Op::EQ && cond.op != Condition::Op::NE) {
                res.emplace_back(TypeConstraint{cond.left, TypeGroup::ptr_or_num});
            }
            res.emplace_back(Comparable{.r1 = cond.left, .r2 = reg_right, .or_r2_is_number = false});
        }
        return res;
    }

    vector<Assertion> operator()(const Assume& ins) const {
        if (!ins.is_implicit) {
            return explicate(ins.cond);
        }
        return {};
    }

    vector<Assertion> operator()(const Jmp& ins) const {
        if (!ins.cond) {
            return {};
        }
        return explicate(*ins.cond);
    }

    vector<Assertion> operator()(const Mem& ins) const {
        vector<Assertion> res;
        const Reg basereg = ins.access.basereg;
        Imm width{gsl::narrow<uint32_t>(ins.access.width)};
        const int offset = ins.access.offset;
        if (basereg.v == R10_STACK_POINTER) {
            // We know we are accessing the stack.
            if (offset < -runtime.subprogram_stack_size || offset + static_cast<int>(width.v) > 0) {
                // This assertion will fail
                res.emplace_back(make_valid_access(basereg, offset, width, false,
                                                   ins.is_load ? AccessType::read : AccessType::write));
            } else if (ins.is_load) {
                // This assertion is not for bound checks but for reading initialized memory.
                // TODO: avoid load assertions: use post-assertion to check that the loaded value is initialized
                // res.emplace_back(make_valid_access(basereg, offset, width, false, AccessType::read));
            }
        } else {
            res.emplace_back(TypeConstraint{basereg, TypeGroup::pointer});
            res.emplace_back(
                make_valid_access(basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write));
            if (!info.type.is_privileged && !ins.is_load) {
                if (const auto preg = std::get_if<Reg>(&ins.value)) {
                    if (width.v != 8) {
                        res.emplace_back(TypeConstraint{*preg, TypeGroup::number});
                    } else {
                        res.emplace_back(ValidStore{ins.access.basereg, *preg});
                    }
                }
            }
        }
        return res;
    }

    vector<Assertion> operator()(const Atomic& ins) const {

        // An atomic is a read-modify-write: model it as a write so that, like a plain
        // store, it is rejected against read-only context pointer fields (a non-write
        // access_type would let an atomic corrupt e.g. ctx->data unchecked).
        return {
            Assertion{TypeConstraint{ins.valreg, TypeGroup::number}},
            Assertion{TypeConstraint{ins.access.basereg, TypeGroup::pointer}},
            Assertion{make_valid_access(ins.access.basereg, ins.access.offset,
                                        Imm{static_cast<uint32_t>(ins.access.width)}, false, AccessType::write)},
        };
    }

    vector<Assertion> operator()(const Un& ins) const {
        return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};
    }

    vector<Assertion> operator()(const Bin& ins) const {
        switch (ins.op) {
        case Bin::Op::MOV:
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                if (!ins.is64) {
                    return {Assertion{TypeConstraint{*src, TypeGroup::number}}};
                }
            }
            return {};
        case Bin::Op::MOVSX8:
        case Bin::Op::MOVSX16:
        case Bin::Op::MOVSX32:
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                return {Assertion{TypeConstraint{*src, TypeGroup::number}}};
            }
            return {};
        case Bin::Op::ADD: {
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}},
                        Assertion{TypeConstraint{*src, TypeGroup::ptr_or_num}}, Assertion{Addable{*src, ins.dst}},
                        Assertion{Addable{ins.dst, *src}}};
            }
            return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};
        }
        case Bin::Op::SUB: {
            if (const auto reg = std::get_if<Reg>(&ins.v)) {
                // disallow map-map since same type does not mean same offset
                // TODO: map identities
                return {TypeConstraint{ins.dst, TypeGroup::ptr_or_num},
                        Comparable{.r1 = ins.dst, .r2 = *reg, .or_r2_is_number = true}};
            }
            return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};
        }
        case Bin::Op::UDIV:
        case Bin::Op::UMOD:
        case Bin::Op::SDIV:
        case Bin::Op::SMOD: {
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                const bool is_signed = (ins.op == Bin::Op::SDIV || ins.op == Bin::Op::SMOD);
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},
                        Assertion{ValidDivisor{*src, is_signed}}};
            }
            return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};
        }
            // For all other binary operations, the destination register must be a number and the source must either be
            // an immediate or a number.
        default:
            if (const auto src = std::get_if<Reg>(&ins.v)) {
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},
                        Assertion{TypeConstraint{*src, TypeGroup::number}}};
            } else {
                return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};
            }
        }
        std::unreachable();
    }
};

/// Annotate the CFG by adding explicit assertions for all the preconditions
/// of any instruction. For example, jump instructions are asserted not to
/// compare numbers and pointers, or pointers to potentially distinct memory
/// regions. The verifier will use these assertions to treat the program as
/// unsafe unless it can prove that the assertions can never fail.
vector<Assertion> get_assertions(const Instruction& ins, const ProgramInfo& info, const RuntimeConfig& runtime,
                                 const std::optional<Label>& label) {
    return std::visit(AssertExtractor{info, runtime, label}, ins);
}
} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <cassert>
4	#include <cinttypes>
5	#include <utility>
6	#include <vector>
7
8	#include "config.hpp"
9	#include "ir/call_resolver.hpp"
10	#include "ir/syntax.hpp"
11	#include "platform.hpp"
12
13	using std::string;
14	using std::to_string;
15	using std::vector;
16
17	namespace prevail {
18	class AssertExtractor {
19	const ProgramInfo& info;
20	const RuntimeConfig& runtime;
21	const std::optional<Label>& current_label; ///< Pre-simplification label this assert is part of.
22
23	static Imm imm(const Value& v) { return std::get<Imm>(v); }
24
25	static vector<Assertion> zero_offset_ctx(const Reg reg, const bool or_null) {	11,860✔
26	vector<Assertion> res;	11,860✔
27	res.emplace_back(TypeConstraint{reg, or_null ? TypeGroup::ctx_or_num : TypeGroup::ctx});	17,766✔
28	res.emplace_back(ZeroCtxOffset{reg, or_null});	11,860✔
29	return res;	11,860✔
30	}	×
31
32	[[nodiscard]]
33	ValidAccess make_valid_access(const Reg reg, const int32_t offset = {}, const Value& width = Imm{0},	230,400✔
34	const bool or_null = {}, const AccessType access_type = {}) const {
35	const int depth = current_label.has_value() ? current_label.value().call_stack_depth() : 1;	230,400✔
36	return ValidAccess{depth, reg, offset, width, or_null, access_type};	230,400✔
37	}
38
39	public:
40	explicit AssertExtractor(const ProgramInfo& info, const RuntimeConfig& runtime, const std::optional<Label>& label)	1,325,990✔
41	: info{info}, runtime{runtime}, current_label{label} {}	1,325,990✔
42
43	vector<Assertion> operator()(const Undefined&) const { return {}; }	8,268✔
44
45	vector<Assertion> operator()(const IncrementLoopCounter& ipc) const { return {{BoundedLoopCount{ipc.name}}}; }	176✔
46
47	vector<Assertion> operator()(const LoadMapFd&) const { return {}; }	36,312✔
48	vector<Assertion> operator()(const LoadMapAddress&) const { return {}; }	5,898✔
49	vector<Assertion> operator()(const LoadPseudo& pseudo) const {	16✔
50	switch (pseudo.addr.kind) {	16✔
51	case PseudoAddress::Kind::CODE_ADDR:	16✔
52	// Type/offset semantics are handled during abstract transformation.
53	return {};	16✔
54	case PseudoAddress::Kind::VARIABLE_ADDR: [[fallthrough]];	×
55	case PseudoAddress::Kind::MAP_BY_IDX: [[fallthrough]];
56	case PseudoAddress::Kind::MAP_VALUE_BY_IDX:
57	assert(false && "unexpected LoadPseudo kind after CFG construction");	×
58	return {};
59	}
60	return {};	×
61	}
62
63	/// Packet access implicitly uses R6, so verify that R6 still has a pointer to the context.
64	vector<Assertion> operator()(const Packet&) const { return zero_offset_ctx({6}, false); }	344✔
65
66	vector<Assertion> operator()(const Exit&) const {	4,334✔
67	vector<Assertion> res;	4,334✔
68	if (current_label->stack_frame_prefix.empty()) {	4,334✔
69	// Verify that Exit returns a number.
70	res.emplace_back(TypeConstraint{Reg{R0_RETURN_VALUE}, TypeGroup::number});	3,654✔
71	}
72	return res;	4,334✔
73	}	×
74
75	vector<Assertion> operator()(const Call& call) const {	59,866✔
76	// Invariant: cfg_builder::check_instruction_feature_support has already
77	// rejected unsupported calls, so resolved.contract below is the real
78	// contract for this (func, kind) key. An unsupported call would have
79	// an empty contract and produce no preconditions here -- sound only
80	// because the cfg_builder gate ensures we never reach that state.
81	const ResolvedCall resolved = resolve(call, info);	59,866✔
82	vector<Assertion> res;	59,866✔
83	std::optional<Reg> map_fd_reg;	59,866✔
84	for (ArgSingle arg : resolved.contract.singles) {	191,102✔
85	switch (arg.kind) {	131,236✔
86	case ArgSingle::Kind::ANYTHING:	38,362✔
87	// avoid pointer leakage:
88	if (!info.type.is_privileged) {	38,362✔
89	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::number});	31,882✔
90	}
91	break;	19,181✔
92	case ArgSingle::Kind::MAP_FD_PROGRAMS:	1,532✔
93	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd_programs});	1,532✔
94	// Do not update map_fd_reg
95	break;	1,532✔
96	case ArgSingle::Kind::MAP_FD:	33,842✔
97	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::map_fd});	33,842✔
98	map_fd_reg = arg.reg;	99,460✔
99	break;	16,921✔
100	case ArgSingle::Kind::PTR_TO_MAP_KEY: [[fallthrough]];	45,712✔
101	case ArgSingle::Kind::PTR_TO_MAP_VALUE:	22,856✔
102	assert(map_fd_reg);	45,712✔
103	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});	45,712✔
104	res.emplace_back(ValidMapKeyValue{arg.reg, *map_fd_reg, arg.kind == ArgSingle::Kind::PTR_TO_MAP_KEY});	45,712✔
105	break;	45,712✔
106	case ArgSingle::Kind::PTR_TO_STACK:	22✔
107	res.emplace_back(TypeConstraint{arg.reg, arg.or_null ? TypeGroup::stack_or_num : TypeGroup::stack});	22✔
108	// TODO: check 0 when null
109	break;	22✔
110	case ArgSingle::Kind::PTR_TO_FUNC:	22✔
111	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::func});	22✔
112	res.emplace_back(ValidCallbackTarget{arg.reg});	22✔
113	break;	22✔
114	case ArgSingle::Kind::PTR_TO_CTX:	11,516✔
115	for (const Assertion& a : zero_offset_ctx(arg.reg, arg.or_null)) {	34,548✔
116	res.emplace_back(a);	23,032✔
117	}	11,516✔
118	break;	11,516✔
119	case ArgSingle::Kind::PTR_TO_SOCKET: res.emplace_back(TypeConstraint{arg.reg, TypeGroup::socket}); break;	142✔
120	case ArgSingle::Kind::PTR_TO_BTF_ID: res.emplace_back(TypeConstraint{arg.reg, TypeGroup::btf_id}); break;	8✔
121	case ArgSingle::Kind::PTR_TO_ALLOC_MEM:	20✔
122	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::alloc_mem});	20✔
123	break;	20✔
124	case ArgSingle::Kind::PTR_TO_SPIN_LOCK:	38✔
125	case ArgSingle::Kind::PTR_TO_TIMER: res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem}); break;	38✔
126	case ArgSingle::Kind::CONST_SIZE_OR_ZERO:	20✔
127	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::number});	20✔
128	res.emplace_back(ValidSize{arg.reg, true});	20✔
129	break;	20✔
130	case ArgSingle::Kind::PTR_TO_WRITABLE_LONG:	×
131	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});	×
132	res.emplace_back(make_valid_access(arg.reg, 0, Imm{8}, false, AccessType::write));	×
133	break;	×
134	case ArgSingle::Kind::PTR_TO_WRITABLE_INT:	×
135	res.emplace_back(TypeConstraint{arg.reg, TypeGroup::mem});	×
136	res.emplace_back(make_valid_access(arg.reg, 0, Imm{4}, false, AccessType::write));	×
137	break;	×
138	}
139	}
140	if (map_fd_reg && resolved.contract.allowed_map_types != 0) {	59,866✔
141	res.emplace_back(ValidMapType{*map_fd_reg, resolved.contract.allowed_map_types, resolved.name});	2,577✔
142	}
143	for (ArgPair arg : resolved.contract.pairs) {	75,570✔
144	const auto group = arg.or_null ? TypeGroup::mem_or_num : TypeGroup::mem;	15,704✔
145	const auto access_type =	23,556✔
146	arg.kind == ArgPair::Kind::PTR_TO_READABLE_MEM ? AccessType::read : AccessType::write;	15,704✔
147	res.emplace_back(TypeConstraint{arg.size, TypeGroup::number});	15,704✔
148	res.emplace_back(ValidSize{arg.size, arg.can_be_zero});	15,704✔
149	res.emplace_back(TypeConstraint{arg.mem, group});	15,704✔
150	res.emplace_back(make_valid_access(arg.mem, 0, arg.size, arg.or_null, access_type));	23,550✔
151	// TODO: reg is constant (or maybe it's not important)
152	}
153	for (uint8_t i = 0; i < 5; ++i) {	359,196✔
154	if (resolved.contract.zero_args_mask & (1 << i)) {	299,330✔
155	const Reg arg_reg{static_cast<uint8_t>(i + 1)};	2✔
156	res.emplace_back(TypeConstraint{arg_reg, TypeGroup::number});	2✔
157	res.emplace_back(ValidArgZero{arg_reg});	2✔
158	}
159	}
160	return res;	89,799✔
161	}	59,866✔
162
163	vector<Assertion> operator()(const CallLocal&) const { return {}; }	680✔
164
165	vector<Assertion> operator()(const Callx& callx) const {	48✔
166	vector<Assertion> res;	48✔
167	res.emplace_back(TypeConstraint{callx.func, TypeGroup::number});	48✔
168	res.emplace_back(FuncConstraint{callx.func});	48✔
169	return res;	48✔
170	}	×
171
172	// Rejected before assertion extraction by cfg_builder::check_instruction_feature_support.
173	vector<Assertion> operator()(const CallBtf&) const {	×
174	assert(false && "CallBtf should be rejected before assertion extraction");	×
175	return {};
176	}
177
178	[[nodiscard]]
179	vector<Assertion> explicate(const Condition& cond) const {	103,498✔
180	vector<Assertion> res;	103,498✔
181	if (info.type.is_privileged) {	103,498✔
182	return res;	9,489✔
183	}
184	if (const auto pimm = std::get_if<Imm>(&cond.right)) {	84,520✔
185	if (pimm->v != 0) {	68,388✔
186	// no need to check for valid access, it must be a number
187	res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});	21,808✔
188	} else {
189	bool allow_pointers = false;	46,580✔
190
191	switch (cond.op) {	46,580✔
192	case Condition::Op::EQ: allow_pointers = true; break;	10,848✔
193	case Condition::Op::NE: allow_pointers = true; break;	9,196✔
194	case Condition::Op::SET: allow_pointers = true; break;	2✔
195	case Condition::Op::NSET: allow_pointers = true; break;	2✔
196	case Condition::Op::LT: allow_pointers = true; break;	15✔
197	case Condition::Op::LE: allow_pointers = true; break;	2✔
198	case Condition::Op::GT: allow_pointers = true; break;	14✔
199	case Condition::Op::GE: allow_pointers = true; break;	4✔
200	case Condition::Op::SLT: allow_pointers = false; break;	6,388✔
201	case Condition::Op::SLE: allow_pointers = false; break;	3,211✔
202	case Condition::Op::SGT: allow_pointers = false; break;	3,225✔
203	case Condition::Op::SGE: allow_pointers = false; break;	3,211✔
204	default: std::unreachable();	×
205	}
206
207	// Only permit pointer comparisons if the operation is 64-bit.
208	allow_pointers &= cond.is64;	46,580✔
209
210	if (!allow_pointers) {	46,580✔
211	res.emplace_back(TypeConstraint{cond.left, TypeGroup::number});	27,352✔
212	}
213
214	res.emplace_back(make_valid_access(cond.left));	69,870✔
215	// OK - map_fd is just another pointer
216	// Anything can be compared to 0
217	}
218	} else {
219	const auto reg_right = get<Reg>(cond.right);	16,132✔
220	res.emplace_back(make_valid_access(cond.left));	24,198✔
221	res.emplace_back(make_valid_access(reg_right));	24,198✔
222	if (cond.op != Condition::Op::EQ && cond.op != Condition::Op::NE) {	16,132✔
223	res.emplace_back(TypeConstraint{cond.left, TypeGroup::ptr_or_num});	8,822✔
224	}
225	res.emplace_back(Comparable{.r1 = cond.left, .r2 = reg_right, .or_r2_is_number = false});	16,132✔
226	}
227	return res;	42,260✔
228	}	×
229
230	vector<Assertion> operator()(const Assume& ins) const {	206,304✔
231	if (!ins.is_implicit) {	206,304✔
232	return explicate(ins.cond);	348✔
233	}
234	return {};	205,956✔
235	}
236
237	vector<Assertion> operator()(const Jmp& ins) const {	125,364✔
238	if (!ins.cond) {	125,364✔
239	return {};	22,214✔
240	}
241	return explicate(*ins.cond);	103,150✔
242	}
243
244	vector<Assertion> operator()(const Mem& ins) const {	290,142✔
245	vector<Assertion> res;	290,142✔
246	const Reg basereg = ins.access.basereg;	290,142✔
247	Imm width{gsl::narrow<uint32_t>(ins.access.width)};	290,142✔
248	const int offset = ins.access.offset;	290,142✔
249	if (basereg.v == R10_STACK_POINTER) {	290,142✔
250	// We know we are accessing the stack.
251	if (offset < -runtime.subprogram_stack_size \|\| offset + static_cast<int>(width.v) > 0) {	155,598✔
252	// This assertion will fail
253	res.emplace_back(make_valid_access(basereg, offset, width, false,	3✔
254	ins.is_load ? AccessType::read : AccessType::write));	2✔
255	} else if (ins.is_load) {
256	// This assertion is not for bound checks but for reading initialized memory.
257	// TODO: avoid load assertions: use post-assertion to check that the loaded value is initialized
258	// res.emplace_back(make_valid_access(basereg, offset, width, false, AccessType::read));
259	}
260	} else {
261	res.emplace_back(TypeConstraint{basereg, TypeGroup::pointer});	134,544✔
262	res.emplace_back(	201,816✔
263	make_valid_access(basereg, offset, width, false, ins.is_load ? AccessType::read : AccessType::write));	225,992✔
264	if (!info.type.is_privileged && !ins.is_load) {	134,544✔
265	if (const auto preg = std::get_if<Reg>(&ins.value)) {	21,808✔
266	if (width.v != 8) {	21,798✔
267	res.emplace_back(TypeConstraint{*preg, TypeGroup::number});	18,120✔
268	} else {
269	res.emplace_back(ValidStore{ins.access.basereg, *preg});	3,678✔
270	}
271	}
272	}
273	}
274	return res;	435,213✔
275	}	×
276
277	vector<Assertion> operator()(const Atomic& ins) const {	1,306✔
278
279	// An atomic is a read-modify-write: model it as a write so that, like a plain
280	// store, it is rejected against read-only context pointer fields (a non-write
281	// access_type would let an atomic corrupt e.g. ctx->data unchecked).
282	return {	653✔
283	Assertion{TypeConstraint{ins.valreg, TypeGroup::number}},	653✔
284	Assertion{TypeConstraint{ins.access.basereg, TypeGroup::pointer}},	653✔
285	Assertion{make_valid_access(ins.access.basereg, ins.access.offset,	1,959✔
286	Imm{static_cast<uint32_t>(ins.access.width)}, false, AccessType::write)},	653✔
287	};	5,877✔
288	}	2,612✔
289
290	vector<Assertion> operator()(const Un& ins) const {	7,806✔
291	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};	19,515✔
292	}	7,806✔
293
294	vector<Assertion> operator()(const Bin& ins) const {	579,258✔
295	switch (ins.op) {	579,258✔
296	case Bin::Op::MOV:	310,200✔
297	if (const auto src = std::get_if<Reg>(&ins.v)) {	310,200✔
298	if (!ins.is64) {	170,002✔
299	return {Assertion{TypeConstraint{*src, TypeGroup::number}}};	105,120✔
300	}
301	}
302	return {};	268,152✔
303	case Bin::Op::MOVSX8:	3,038✔
304	case Bin::Op::MOVSX16:	1,519✔
305	case Bin::Op::MOVSX32:	1,519✔
306	if (const auto src = std::get_if<Reg>(&ins.v)) {	3,038✔
307	return {Assertion{TypeConstraint{*src, TypeGroup::number}}};	7,595✔
308	}
309	return {};	×
310	case Bin::Op::ADD: {	101,732✔
311	if (const auto src = std::get_if<Reg>(&ins.v)) {	101,732✔
312	return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}},	10,824✔
313	Assertion{TypeConstraint{src, TypeGroup::ptr_or_num}}, Assertion{Addable{src, ins.dst}},	10,824✔
314	Assertion{Addable{ins.dst, *src}}};	119,064✔
315	}
316	return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};	200,210✔
317	}
318	case Bin::Op::SUB: {	2,864✔
319	if (const auto reg = std::get_if<Reg>(&ins.v)) {	2,864✔
320	// disallow map-map since same type does not mean same offset
321	// TODO: map identities
322	return {TypeConstraint{ins.dst, TypeGroup::ptr_or_num},	1,416✔
323	Comparable{.r1 = ins.dst, .r2 = *reg, .or_r2_is_number = true}};	9,912✔
324	}
325	return {Assertion{TypeConstraint{ins.dst, TypeGroup::ptr_or_num}}};	80✔
326	}
327	case Bin::Op::UDIV:	6,642✔
328	case Bin::Op::UMOD:	3,321✔
329	case Bin::Op::SDIV:	3,321✔
330	case Bin::Op::SMOD: {	3,321✔
331	if (const auto src = std::get_if<Reg>(&ins.v)) {	6,642✔
332	const bool is_signed = (ins.op == Bin::Op::SDIV \|\| ins.op == Bin::Op::SMOD);	328✔
333	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},	164✔
334	Assertion{ValidDivisor{*src, is_signed}}};	1,148✔
335	}
336	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};	15,785✔
337	}
338	// For all other binary operations, the destination register must be a number and the source must either be
339	// an immediate or a number.
340	default:	154,782✔
341	if (const auto src = std::get_if<Reg>(&ins.v)) {	154,782✔
342	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}},	23,342✔
343	Assertion{TypeConstraint{*src, TypeGroup::number}}};	163,394✔
344	} else {
345	return {Assertion{TypeConstraint{ins.dst, TypeGroup::number}}};	270,245✔
346	}
347	}
348	std::unreachable();
349	}	311,106✔
350	};
351
352	/// Annotate the CFG by adding explicit assertions for all the preconditions
353	/// of any instruction. For example, jump instructions are asserted not to
354	/// compare numbers and pointers, or pointers to potentially distinct memory
355	/// regions. The verifier will use these assertions to treat the program as
356	/// unsafe unless it can prove that the assertions can never fail.
357	vector<Assertion> get_assertions(const Instruction& ins, const ProgramInfo& info, const RuntimeConfig& runtime,	1,325,990✔
358	const std::optional<Label>& label) {
359	return std::visit(AssertExtractor{info, runtime, label}, ins);	1,325,990✔
360	}
361	} // namespace prevail

Alan-Jowett / ebpf-verifier / 27778108035

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