29279923487

Committed 12 Jul 2026 11:38AM UTC coverage: 86.649% (+0.3%) from 86.386%

Build # 29279923487

Build Type

push

github

Committed by

web-flow

Commit Message

Drive sample verification tests from the inventory; parallelize CI (#1195)

Full-program verification of the ebpf-samples corpus was 17 C++ files
generated by scripts/generate_verify_project_tests.py from
test-data/elf_inventory.json, then compiled into the test binary. The
generated files duplicated the inventory and could drift from it (there
was no check keeping them in sync), and the whole corpus ran in one
single-threaded Catch2 process.

Data-driven tests (dedup)
-------------------------
- Add src/test/test_verify_samples.cpp, which reads elf_inventory.json at
  runtime (via yaml-cpp; JSON is a subset of YAML) and registers one
  Catch2 DYNAMIC_SECTION per (object, section[, program]). Adding or
  retagging a sample is now a JSON edit: no code generation, no recompile.
- Delete the 17 generated test_verify_<project>.cpp files and
  scripts/generate_verify_project_tests.py. The inventory is the single
  source of truth. A coverage-guard test asserts the registered projects
  match the inventory exactly, so a new project cannot be left untested.
- Trim test_verify.hpp to the ELF-parse cache and the VerifyIssueKind
  taxonomy the driver and the multithreading test still use.

  Catch2's [!shouldfail] is a compile-time per-TEST_CASE tag and cannot be
  applied per data-driven entry, so an expected_failure (a safe program
  the verifier is currently too imprecise to accept) is asserted as
  *still rejected* -- an xfail/golden marker. A verifier improvement that
  starts accepting it fails the case, prompting an inventory update; a
  regression on a passing program fails it too.

Parallel CI (ctest)
-------------------
- Register ctest entries: one per project (sharded by tag) plus a "unit"
  entry for everything else. The shard list is derived from the inventory
  via string(JSON), so it cannot drift from the corpus.
- CI runs `ctest -j` instead of a single `bin/tests` process. Locally, a
  full run drops from ~104s to ~42s on 16 cores (bounded by t... (continued)

Coverage Stats

9313 of 10748 relevant lines covered (86.65%)

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

Alan-Jowett / ebpf-verifier / 29279923487

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