18658728485

Committed 18 Oct 2025 05:56PM UTC coverage: 88.47% (+0.4%) from 88.11%

Build # 18658728485

Build Type

push

github

Committed by

elazarg

Commit Message

Bump external/bpf_conformance from `8f3c2fe` to `6fa6a20`

Bumps [external/bpf_conformance](https://github.com/Alan-Jowett/bpf_conformance) from `8f3c2fe` to `6fa6a20`.
- [Release notes](https://github.com/Alan-Jowett/bpf_conformance/releases)
- [Commits](https://github.com/Alan-Jowett/bpf_conformance/compare/8f3c2fe88...<a class=hub.com/Alan-Jowett/ebpf-verifier/commit/6fa6a20ac6fd3612ea9338312a67408687b9f06b">6fa6a20ac)

---
updated-dependencies:
- dependency-name: external/bpf_conformance
  dependency-version: 6fa6a20ac6fd3612ea9338312a67408687b9f06b
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>

Run Details

8954 of 10121 relevant lines covered (88.47%)

18293099.16 hits per line

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

73.58

/src/test/ebpf_yaml.cpp

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

#include <algorithm>
#include <bit>
#include <iostream>
#include <set>
#include <variant>

#include <yaml-cpp/yaml.h>

#include "asm_parse.hpp"
#include "asm_syntax.hpp"
#include "crab_verifier.hpp"
#include "ebpf_verifier.hpp"
#include "ebpf_yaml.hpp"
#include "string_constraints.hpp"

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

namespace prevail {
// The YAML tests for Call depend on Linux prototypes.
// parse_instruction() in asm_parse.cpp explicitly uses
// g_ebpf_platform_linux when parsing Call instructions
// so we do the same here.

static EbpfProgramType ebpf_get_program_type(const string& section, const string& path) {
    return g_ebpf_platform_linux.get_program_type(section, path);
}

static EbpfMapType ebpf_get_map_type(const uint32_t platform_specific_type) {
    return g_ebpf_platform_linux.get_map_type(platform_specific_type);
}

static EbpfHelperPrototype ebpf_get_helper_prototype(const int32_t n) {
    return g_ebpf_platform_linux.get_helper_prototype(n);
}

static bool ebpf_is_helper_usable(const int32_t n) { return g_ebpf_platform_linux.is_helper_usable(n); }

static void ebpf_parse_maps_section(vector<EbpfMapDescriptor>&, const char*, size_t, int, const ebpf_platform_t*,
                                    ebpf_verifier_options_t) {}

static EbpfMapDescriptor test_map_descriptor = {.original_fd = 0,
                                                .type = 0,
                                                .key_size = sizeof(uint32_t),
                                                .value_size = sizeof(uint32_t),
                                                .max_entries = 4,
                                                .inner_map_fd = 0};

static EbpfMapDescriptor& ebpf_get_map_descriptor(int) { return test_map_descriptor; }

ebpf_platform_t g_platform_test = {.get_program_type = ebpf_get_program_type,
                                   .get_helper_prototype = ebpf_get_helper_prototype,
                                   .is_helper_usable = ebpf_is_helper_usable,
                                   .map_record_size = 0,
                                   .parse_maps_section = ebpf_parse_maps_section,
                                   .get_map_descriptor = ebpf_get_map_descriptor,
                                   .get_map_type = ebpf_get_map_type,
                                   .supported_conformance_groups = bpf_conformance_groups_t::default_groups |
                                                                   bpf_conformance_groups_t::packet |
                                                                   bpf_conformance_groups_t::callx};

static EbpfProgramType make_program_type(const string& name, const ebpf_context_descriptor_t* context_descriptor) {
    return EbpfProgramType{.name = name,
                           .context_descriptor = context_descriptor,
                           .platform_specific_data = 0,
                           .section_prefixes = {},
                           .is_privileged = false};
}

static std::set<string> vector_to_set(const vector<string>& s) {
    std::set<string> res;
    for (const auto& item : s) {
        res.insert(item);
    }
    return res;
}

std::set<string> operator-(const std::set<string>& a, const std::set<string>& b) {
    std::set<string> res;
    std::ranges::set_difference(a, b, std::inserter(res, res.begin()));
    return res;
}

static StringInvariant read_invariant(const vector<string>& raw_invariant) {
    const std::set<string> res = vector_to_set(raw_invariant);
    if (res == std::set<string>{"_|_"}) {
        return StringInvariant{};
    }
    return StringInvariant{res};
}

struct RawTestCase {
    string test_case;
    std::set<string> options;
    vector<string> pre;
    vector<std::tuple<string, vector<string>>> raw_blocks;
    vector<string> post;
    std::set<string> messages;
};

static vector<string> parse_block(const YAML::Node& block_node) {
    vector<string> block;
    std::istringstream is{block_node.as<string>()};
    string line;
    while (std::getline(is, line)) {
        block.emplace_back(line);
    }
    return block;
}

static auto parse_code(const YAML::Node& code_node) {
    vector<std::tuple<string, vector<string>>> res;
    for (const auto& item : code_node) {
        res.emplace_back(item.first.as<string>(), parse_block(item.second));
    }
    return res;
}

static std::set<string> as_set_empty_default(const YAML::Node& optional_node) {
    if (!optional_node.IsDefined() || optional_node.IsNull()) {
        return {};
    }
    return vector_to_set(optional_node.as<vector<string>>());
}

static RawTestCase parse_case(const YAML::Node& case_node) {
    return RawTestCase{
        .test_case = case_node["test-case"].as<string>(),
        .options = as_set_empty_default(case_node["options"]),
        .pre = case_node["pre"].as<vector<string>>(),
        .raw_blocks = parse_code(case_node["code"]),
        .post = case_node["post"].as<vector<string>>(),
        .messages = as_set_empty_default(case_node["messages"]),
    };
}

static InstructionSeq raw_cfg_to_instruction_seq(const vector<std::tuple<string, vector<string>>>& raw_blocks) {
    std::map<string, Label> label_name_to_label;

    int label_index = 0;
    for (const auto& [label_name, raw_block] : raw_blocks) {
        label_name_to_label.emplace(label_name, label_index);
        // don't count large instructions as 2
        label_index += gsl::narrow<int>(raw_block.size());
    }

    InstructionSeq res;
    label_index = 0;
    for (const auto& [label_name, raw_block] : raw_blocks) {
        for (const string& line : raw_block) {
            try {
                const Instruction& ins = parse_instruction(line, label_name_to_label);
                if (std::holds_alternative<Undefined>(ins)) {
                    std::cout << "text:" << line << "; ins: " << ins << "\n";
                }
                res.emplace_back(label_index, ins, std::optional<btf_line_info_t>());
            } catch (const std::exception& e) {
                std::cout << "text:" << line << "; error: " << e.what() << "\n";
                res.emplace_back(label_index, Undefined{0}, std::optional<btf_line_info_t>());
            }
            label_index++;
        }
    }
    return res;
}

static ebpf_verifier_options_t raw_options_to_options(const std::set<string>& raw_options) {
    ebpf_verifier_options_t options{};

    // Use ~simplify for YAML tests unless otherwise specified.
    options.verbosity_opts.simplify = false;

    // All YAML tests use !setup_constraints.
    options.setup_constraints = false;

    // Default to the machine's native endianness.
    options.big_endian = std::endian::native == std::endian::big;

    // Default to not assuming assertions.
    options.assume_assertions = false;

    // Permit test cases to not have an exit instruction.
    options.cfg_opts.must_have_exit = false;

    for (const string& name : raw_options) {
        if (name == "!allow_division_by_zero") {
            options.allow_division_by_zero = false;
        } else if (name == "termination") {
            options.cfg_opts.check_for_termination = true;
        } else if (name == "strict") {
            options.strict = true;
        } else if (name == "simplify") {
            options.verbosity_opts.simplify = true;
        } else if (name == "big_endian") {
            options.big_endian = true;
        } else if (name == "!big_endian") {
            options.big_endian = false;
        } else if (name == "assume_assertions") {
            options.assume_assertions = true;
        } else {
            throw std::runtime_error("Unknown option: " + name);
        }
    }
    return options;
}

static TestCase read_case(const RawTestCase& raw_case) {
    return TestCase{.name = raw_case.test_case,
                    .options = raw_options_to_options(raw_case.options),
                    .assumed_pre_invariant = read_invariant(raw_case.pre),
                    .instruction_seq = raw_cfg_to_instruction_seq(raw_case.raw_blocks),
                    .expected_post_invariant = read_invariant(raw_case.post),
                    .expected_messages = raw_case.messages};
}

static vector<TestCase> read_suite(const string& path) {
    std::ifstream f{path};
    vector<TestCase> res;
    for (const YAML::Node& config : YAML::LoadAll(f)) {
        res.push_back(read_case(parse_case(config)));
    }
    return res;
}

template <typename T>
static Diff<T> make_diff(const T& actual, const T& expected) {
    return Diff<T>{
        .unexpected = actual - expected,
        .unseen = expected - actual,
    };
}

std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {
    thread_local_options = {};
    ThreadLocalGuard clear_thread_local_state;
    test_case.options.verbosity_opts.print_failures = true;
    if (debug) {
        test_case.options.verbosity_opts.print_invariants = true;
    }

    ebpf_context_descriptor_t context_descriptor{64, 0, 4, -1};
    EbpfProgramType program_type = make_program_type(test_case.name, &context_descriptor);

    ProgramInfo info{&g_platform_test, {}, program_type};
    thread_local_options = test_case.options;
    try {
        const Program prog = Program::from_sequence(test_case.instruction_seq, info, test_case.options);
        const Invariants invariants = analyze(prog, test_case.assumed_pre_invariant);
        const StringInvariant actual_last_invariant = invariants.invariant_at(Label::exit);
        const std::set<string> actual_messages = invariants.check_assertions(prog).all_messages();

        if (actual_last_invariant == test_case.expected_post_invariant &&
            actual_messages == test_case.expected_messages) {
            return {};
        }
        return Failure{
            .invariant = make_diff(actual_last_invariant, test_case.expected_post_invariant),
            .messages = make_diff(actual_messages, test_case.expected_messages),
        };
    } catch (InvalidControlFlow& ex) {
        const std::set<string> actual_messages{ex.what()};
        if (test_case.expected_post_invariant == StringInvariant::top() &&
            actual_messages == test_case.expected_messages) {
            return {};
        }
        return Failure{
            .invariant = make_diff(StringInvariant::top(), test_case.expected_post_invariant),
            .messages = make_diff(actual_messages, test_case.expected_messages),
        };
    }
}

template <typename T>
    requires std::is_trivially_copyable_v<T>
static vector<T> vector_of(const std::vector<std::byte>& bytes) {
    auto data = bytes.data();
    const auto size = bytes.size();
    if (size % sizeof(T) != 0 || size > std::numeric_limits<uint32_t>::max() || !data) {
        throw std::runtime_error("Invalid argument to vector_of");
    }
    return {reinterpret_cast<const T*>(data), reinterpret_cast<const T*>(data + size)};
}

template <std::signed_integral TS>
void add_stack_variable(std::set<std::string>& more, int& offset, const std::vector<std::byte>& memory_bytes) {
    using TU = std::make_unsigned_t<TS>;
    constexpr size_t size = sizeof(TS);
    static_assert(sizeof(TU) == size);
    const auto src = memory_bytes.data() + offset + memory_bytes.size() - EBPF_TOTAL_STACK_SIZE;
    TS svalue;
    std::memcpy(&svalue, src, size);
    TU uvalue;
    std::memcpy(&uvalue, src, size);
    const auto range = "s[" + std::to_string(offset) + "..." + std::to_string(offset + size - 1) + "]";
    more.insert(range + ".svalue=" + std::to_string(svalue));
    more.insert(range + ".uvalue=" + std::to_string(uvalue));
    offset += size;
}

StringInvariant stack_contents_invariant(const std::vector<std::byte>& memory_bytes) {
    std::set<std::string> more = {"r1.type=stack",
                                  "r1.stack_offset=" + std::to_string(EBPF_TOTAL_STACK_SIZE - memory_bytes.size()),
                                  "r1.stack_numeric_size=" + std::to_string(memory_bytes.size()),
                                  "r10.type=stack",
                                  "r10.stack_offset=" + std::to_string(EBPF_TOTAL_STACK_SIZE),
                                  "s[" + std::to_string(EBPF_TOTAL_STACK_SIZE - memory_bytes.size()) + "..." +
                                      std::to_string(EBPF_TOTAL_STACK_SIZE - 1) + "].type=number"};

    int offset = EBPF_TOTAL_STACK_SIZE - gsl::narrow<int>(memory_bytes.size());
    if (offset % 2 != 0) {
        add_stack_variable<int8_t>(more, offset, memory_bytes);
    }
    if (offset % 4 != 0) {
        add_stack_variable<int16_t>(more, offset, memory_bytes);
    }
    if (offset % 8 != 0) {
        add_stack_variable<int32_t>(more, offset, memory_bytes);
    }
    while (offset < EBPF_TOTAL_STACK_SIZE) {
        add_stack_variable<int64_t>(more, offset, memory_bytes);
    }

    return StringInvariant(more);
}

ConformanceTestResult run_conformance_test_case(const std::vector<std::byte>& memory_bytes,
                                                const std::vector<std::byte>& program_bytes, bool debug) {
    ebpf_context_descriptor_t context_descriptor{64, -1, -1, -1};
    EbpfProgramType program_type = make_program_type("conformance_check", &context_descriptor);

    ProgramInfo info{&g_platform_test, {}, program_type};

    auto insts = vector_of<EbpfInst>(program_bytes);
    StringInvariant pre_invariant = StringInvariant::top();

    if (!memory_bytes.empty()) {
        if (memory_bytes.size() > EBPF_TOTAL_STACK_SIZE) {
            std::cerr << "memory size overflow\n";
            return {};
        }
        pre_invariant = pre_invariant + stack_contents_invariant(memory_bytes);
    }
    RawProgram raw_prog{.prog = insts};
    ebpf_platform_t platform = g_ebpf_platform_linux;
    platform.supported_conformance_groups |= bpf_conformance_groups_t::callx;
    raw_prog.info.platform = &platform;

    // Convert the raw program section to a set of instructions.
    std::variant<InstructionSeq, std::string> prog_or_error = unmarshal(raw_prog);
    if (auto prog = std::get_if<std::string>(&prog_or_error)) {
        std::cerr << "unmarshaling error at " << *prog << "\n";
        return {};
    }

    const InstructionSeq& inst_seq = std::get<InstructionSeq>(prog_or_error);

    ebpf_verifier_options_t options{};
    if (debug) {
        print(inst_seq, std::cout, {});
        options.verbosity_opts.print_failures = true;
        options.verbosity_opts.print_invariants = true;
        options.verbosity_opts.simplify = false;
    }

    try {
        const Program prog = Program::from_sequence(inst_seq, info, options);
        const Invariants invariants = analyze(prog, pre_invariant);
        return ConformanceTestResult{.success = invariants.verified(prog), .r0_value = invariants.exit_value()};
    } catch (const std::exception&) {
        // Catch exceptions thrown in ebpf_domain.cpp.
        return {};
    }
}

void print_failure(const Failure& failure, std::ostream& os) {
    constexpr auto INDENT = "  ";
    if (!failure.invariant.unexpected.empty()) {
        os << "Unexpected properties:\n" << INDENT << failure.invariant.unexpected << "\n";
    } else {
        os << "Unexpected properties: None\n";
    }
    if (!failure.invariant.unseen.empty()) {
        os << "Unseen properties:\n" << INDENT << failure.invariant.unseen << "\n";
    } else {
        os << "Unseen properties: None\n";
    }

    if (!failure.messages.unexpected.empty()) {
        os << "Unexpected messages:\n";
        for (const auto& item : failure.messages.unexpected) {
            os << INDENT << item << "\n";
        }
    } else {
        os << "Unexpected messages: None\n";
    }

    if (!failure.messages.unseen.empty()) {
        os << "Unseen messages:\n";
        for (const auto& item : failure.messages.unseen) {
            os << INDENT << item << "\n";
        }
    } else {
        os << "Unseen messages: None\n";
    }
}

bool all_suites(const string& path) {
    bool result = true;
    for (const TestCase& test_case : read_suite(path)) {
        result = result && static_cast<bool>(run_yaml_test_case(test_case));
    }
    return result;
}

void foreach_suite(const string& path, const std::function<void(const TestCase&)>& f) {
    for (const TestCase& test_case : read_suite(path)) {
        f(test_case);
    }
}
} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3
4	#include <algorithm>
5	#include <bit>
6	#include <iostream>
7	#include <set>
8	#include <variant>
9
10	#include <yaml-cpp/yaml.h>
11
12	#include "asm_parse.hpp"
13	#include "asm_syntax.hpp"
14	#include "crab_verifier.hpp"
15	#include "ebpf_verifier.hpp"
16	#include "ebpf_yaml.hpp"
17	#include "string_constraints.hpp"
18
19	using std::string;
20	using std::vector;
21
22	namespace prevail {
23	// The YAML tests for Call depend on Linux prototypes.
24	// parse_instruction() in asm_parse.cpp explicitly uses
25	// g_ebpf_platform_linux when parsing Call instructions
26	// so we do the same here.
27
28	static EbpfProgramType ebpf_get_program_type(const string& section, const string& path) {	×
29	return g_ebpf_platform_linux.get_program_type(section, path);	×
30	}
31
32	static EbpfMapType ebpf_get_map_type(const uint32_t platform_specific_type) {	28✔
33	return g_ebpf_platform_linux.get_map_type(platform_specific_type);	28✔
34	}
35
36	static EbpfHelperPrototype ebpf_get_helper_prototype(const int32_t n) {	88✔
37	return g_ebpf_platform_linux.get_helper_prototype(n);	88✔
38	}
39
40	static bool ebpf_is_helper_usable(const int32_t n) { return g_ebpf_platform_linux.is_helper_usable(n); }	92✔
41
42	static void ebpf_parse_maps_section(vector<EbpfMapDescriptor>&, const char, size_t, int, const ebpf_platform_t,	×
43	ebpf_verifier_options_t) {}	×
44
45	static EbpfMapDescriptor test_map_descriptor = {.original_fd = 0,
46	.type = 0,
47	.key_size = sizeof(uint32_t),
48	.value_size = sizeof(uint32_t),
49	.max_entries = 4,
50	.inner_map_fd = 0};
51
52	static EbpfMapDescriptor& ebpf_get_map_descriptor(int) { return test_map_descriptor; }	228✔
53
54	ebpf_platform_t g_platform_test = {.get_program_type = ebpf_get_program_type,
55	.get_helper_prototype = ebpf_get_helper_prototype,
56	.is_helper_usable = ebpf_is_helper_usable,
57	.map_record_size = 0,
58	.parse_maps_section = ebpf_parse_maps_section,
59	.get_map_descriptor = ebpf_get_map_descriptor,
60	.get_map_type = ebpf_get_map_type,
61	.supported_conformance_groups = bpf_conformance_groups_t::default_groups \|
62	bpf_conformance_groups_t::packet \|
63	bpf_conformance_groups_t::callx};
64
65	static EbpfProgramType make_program_type(const string& name, const ebpf_context_descriptor_t* context_descriptor) {	1,836✔
66	return EbpfProgramType{.name = name,	1,140✔
67	.context_descriptor = context_descriptor,
68	.platform_specific_data = 0,
69	.section_prefixes = {},
70	.is_privileged = false};	918✔
71	}
72
73	static std::set<string> vector_to_set(const vector<string>& s) {	206,064✔
74	std::set<string> res;	206,064✔
75	for (const auto& item : s) {	919,544✔
76	res.insert(item);	713,480✔
77	}
78	return res;	206,064✔
79	}	×
80
81	std::set<string> operator-(const std::set<string>& a, const std::set<string>& b) {	×
82	std::set<string> res;	×
83	std::ranges::set_difference(a, b, std::inserter(res, res.begin()));	×
84	return res;	×
85	}	×
86
87	static StringInvariant read_invariant(const vector<string>& raw_invariant) {	168,084✔
88	const std::set<string> res = vector_to_set(raw_invariant);	168,084✔
89	if (res == std::set<string>{"_\|_"}) {	420,210✔
90	return StringInvariant{};	×
91	}
92	return StringInvariant{res};	252,126✔
93	}	588,294✔
94
95	struct RawTestCase {
96	string test_case;
97	std::set<string> options;
98	vector<string> pre;
99	vector<std::tuple<string, vector<string>>> raw_blocks;
100	vector<string> post;
101	std::set<string> messages;
102	};
103
104	static vector<string> parse_block(const YAML::Node& block_node) {	92,112✔
105	vector<string> block;	92,112✔
106	std::istringstream is{block_node.as<string>()};	92,112✔
107	string line;	92,112✔
108	while (std::getline(is, line)) {	206,206✔
109	block.emplace_back(line);	114,094✔
110	}
111	return block;	184,224✔
112	}	92,112✔
113
114	static auto parse_code(const YAML::Node& code_node) {	84,042✔
115	vector<std::tuple<string, vector<string>>> res;	84,042✔
116	for (const auto& item : code_node) {	398,364✔
117	res.emplace_back(item.first.as<string>(), parse_block(item.second));	138,168✔
118	}	176,154✔
119	return res;	84,042✔
120	}	×
121
122	static std::set<string> as_set_empty_default(const YAML::Node& optional_node) {	168,084✔
123	if (!optional_node.IsDefined() \|\| optional_node.IsNull()) {	187,074✔
124	return {};	130,104✔
125	}
126	return vector_to_set(optional_node.as<vector<string>>());	37,980✔
127	}
128
129	static RawTestCase parse_case(const YAML::Node& case_node) {	84,042✔
130	return RawTestCase{	126,063✔
131	.test_case = case_node["test-case"].as<string>(),
132	.options = as_set_empty_default(case_node["options"]),
133	.pre = case_node["pre"].as<vector<string>>(),
134	.raw_blocks = parse_code(case_node["code"]),
135	.post = case_node["post"].as<vector<string>>(),
136	.messages = as_set_empty_default(case_node["messages"]),
137	};	126,063✔
138	}
139
140	static InstructionSeq raw_cfg_to_instruction_seq(const vector<std::tuple<string, vector<string>>>& raw_blocks) {	84,042✔
141	std::map<string, Label> label_name_to_label;	84,042✔
142
143	int label_index = 0;	84,042✔
144	for (const auto& [label_name, raw_block] : raw_blocks) {	176,154✔
145	label_name_to_label.emplace(label_name, label_index);	92,112✔
146	// don't count large instructions as 2
147	label_index += gsl::narrow<int>(raw_block.size());	92,112✔
148	}
149
150	InstructionSeq res;	84,042✔
151	label_index = 0;	84,042✔
152	for (const auto& [label_name, raw_block] : raw_blocks) {	176,154✔
153	for (const string& line : raw_block) {	206,206✔
154	try {	57,047✔
155	const Instruction& ins = parse_instruction(line, label_name_to_label);	114,094✔
156	if (std::holds_alternative<Undefined>(ins)) {	114,094✔
157	std::cout << "text:" << line << "; ins: " << ins << "\n";	×
158	}
159	res.emplace_back(label_index, ins, std::optional<btf_line_info_t>());	171,141✔
160	} catch (const std::exception& e) {	114,094✔
161	std::cout << "text:" << line << "; error: " << e.what() << "\n";	×
162	res.emplace_back(label_index, Undefined{0}, std::optional<btf_line_info_t>());	×
163	}	×
164	label_index++;	114,094✔
165	}
166	}
167	return res;	126,063✔
168	}	84,042✔
169
170	static ebpf_verifier_options_t raw_options_to_options(const std::set<string>& raw_options) {	84,042✔
171	ebpf_verifier_options_t options{};	84,042✔
172
173	// Use ~simplify for YAML tests unless otherwise specified.
174	options.verbosity_opts.simplify = false;	84,042✔
175
176	// All YAML tests use !setup_constraints.
177	options.setup_constraints = false;	84,042✔
178
179	// Default to the machine's native endianness.
180	options.big_endian = std::endian::native == std::endian::big;	84,042✔
181
182	// Default to not assuming assertions.
183	options.assume_assertions = false;	84,042✔
184
185	// Permit test cases to not have an exit instruction.
186	options.cfg_opts.must_have_exit = false;	84,042✔
187
188	for (const string& name : raw_options) {	91,374✔
189	if (name == "!allow_division_by_zero") {	7,332✔
190	options.allow_division_by_zero = false;	1,024✔
191	} else if (name == "termination") {	5,284✔
192	options.cfg_opts.check_for_termination = true;	323✔
193	} else if (name == "strict") {	4,638✔
194	options.strict = true;
195	} else if (name == "simplify") {	4,638✔
196	options.verbosity_opts.simplify = true;	15✔
197	} else if (name == "big_endian") {	4,608✔
198	options.big_endian = true;	500✔
199	} else if (name == "!big_endian") {	3,608✔
200	options.big_endian = false;	556✔
201	} else if (name == "assume_assertions") {	2,496✔
202	options.assume_assertions = true;	1,248✔
203	} else {
204	throw std::runtime_error("Unknown option: " + name);	×
205	}
206	}
207	return options;	84,042✔
208	}
209
210	static TestCase read_case(const RawTestCase& raw_case) {	84,042✔
211	return TestCase{.name = raw_case.test_case,	84,042✔
212	.options = raw_options_to_options(raw_case.options),	84,042✔
213	.assumed_pre_invariant = read_invariant(raw_case.pre),	84,042✔
214	.instruction_seq = raw_cfg_to_instruction_seq(raw_case.raw_blocks),	84,042✔
215	.expected_post_invariant = read_invariant(raw_case.post),	84,042✔
216	.expected_messages = raw_case.messages};	84,042✔
217	}
218
219	static vector<TestCase> read_suite(const string& path) {	1,392✔
220	std::ifstream f{path};	1,392✔
221	vector<TestCase> res;	1,392✔
222	for (const YAML::Node& config : YAML::LoadAll(f)) {	85,434✔
223	res.push_back(read_case(parse_case(config)));	126,063✔
224	}	1,392✔
225	return res;	2,088✔
226	}	1,392✔
227
228	template <typename T>
229	static Diff<T> make_diff(const T& actual, const T& expected) {	×
230	return Diff<T>{
231	.unexpected = actual - expected,
232	.unseen = expected - actual,
233	};	×
234	}	×
235
236	std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {	1,392✔
237	thread_local_options = {};	1,392✔
238	ThreadLocalGuard clear_thread_local_state;	696✔
239	test_case.options.verbosity_opts.print_failures = true;	1,392✔
240	if (debug) {	1,392✔
241	test_case.options.verbosity_opts.print_invariants = true;	×
242	}
243
244	ebpf_context_descriptor_t context_descriptor{64, 0, 4, -1};	1,392✔
245	EbpfProgramType program_type = make_program_type(test_case.name, &context_descriptor);	1,392✔
246
247	ProgramInfo info{&g_platform_test, {}, program_type};	1,392✔
248	thread_local_options = test_case.options;	1,392✔
249	try {	696✔
250	const Program prog = Program::from_sequence(test_case.instruction_seq, info, test_case.options);	1,392✔
251	const Invariants invariants = analyze(prog, test_case.assumed_pre_invariant);	1,384✔
252	const StringInvariant actual_last_invariant = invariants.invariant_at(Label::exit);	1,384✔
253	const std::set<string> actual_messages = invariants.check_assertions(prog).all_messages();	1,384✔
254
255	if (actual_last_invariant == test_case.expected_post_invariant &&	2,768✔
256	actual_messages == test_case.expected_messages) {	1,384✔
257	return {};	1,384✔
258	}
259	return Failure{	×
260	.invariant = make_diff(actual_last_invariant, test_case.expected_post_invariant),	×
261	.messages = make_diff(actual_messages, test_case.expected_messages),	×
262	};	×
263	} catch (InvalidControlFlow& ex) {	2,084✔
264	const std::set<string> actual_messages{ex.what()};	20✔
265	if (test_case.expected_post_invariant == StringInvariant::top() &&	24✔
266	actual_messages == test_case.expected_messages) {	8✔
267	return {};	8✔
268	}
269	return Failure{	×
270	.invariant = make_diff(StringInvariant::top(), test_case.expected_post_invariant),	×
271	.messages = make_diff(actual_messages, test_case.expected_messages),	×
272	};	×
273	}	8✔
274	}	2,108✔
275
276	template <typename T>
277	requires std::is_trivially_copyable_v<T>
278	static vector<T> vector_of(const std::vector<std::byte>& bytes) {	444✔
279	auto data = bytes.data();	444✔
280	const auto size = bytes.size();	444✔
281	if (size % sizeof(T) != 0 \|\| size > std::numeric_limits<uint32_t>::max() \|\| !data) {	444✔
282	throw std::runtime_error("Invalid argument to vector_of");	×
283	}
284	return {reinterpret_cast<const T>(data), reinterpret_cast<const T>(data + size)};	888✔
285	}
286
287	template <std::signed_integral TS>
288	void add_stack_variable(std::set<std::string>& more, int& offset, const std::vector<std::byte>& memory_bytes) {	138✔
289	using TU = std::make_unsigned_t<TS>;
290	constexpr size_t size = sizeof(TS);	138✔
291	static_assert(sizeof(TU) == size);
292	const auto src = memory_bytes.data() + offset + memory_bytes.size() - EBPF_TOTAL_STACK_SIZE;	138✔
293	TS svalue;
294	std::memcpy(&svalue, src, size);	138✔
295	TU uvalue;
296	std::memcpy(&uvalue, src, size);	138✔
297	const auto range = "s[" + std::to_string(offset) + "..." + std::to_string(offset + size - 1) + "]";	345✔
298	more.insert(range + ".svalue=" + std::to_string(svalue));	207✔
299	more.insert(range + ".uvalue=" + std::to_string(uvalue));	207✔
300	offset += size;	138✔
301	}	138✔
302
303	StringInvariant stack_contents_invariant(const std::vector<std::byte>& memory_bytes) {	80✔
304	std::set<std::string> more = {"r1.type=stack",	40✔
305	"r1.stack_offset=" + std::to_string(EBPF_TOTAL_STACK_SIZE - memory_bytes.size()),	120✔
306	"r1.stack_numeric_size=" + std::to_string(memory_bytes.size()),	160✔
307	"r10.type=stack",
308	"r10.stack_offset=" + std::to_string(EBPF_TOTAL_STACK_SIZE),	120✔
309	"s[" + std::to_string(EBPF_TOTAL_STACK_SIZE - memory_bytes.size()) + "..." +	240✔
310	std::to_string(EBPF_TOTAL_STACK_SIZE - 1) + "].type=number"};	760✔
311
312	int offset = EBPF_TOTAL_STACK_SIZE - gsl::narrow<int>(memory_bytes.size());	120✔
313	if (offset % 2 != 0) {	80✔
314	add_stack_variable<int8_t>(more, offset, memory_bytes);	8✔
315	}
316	if (offset % 4 != 0) {	80✔
317	add_stack_variable<int16_t>(more, offset, memory_bytes);	20✔
318	}
319	if (offset % 8 != 0) {	80✔
320	add_stack_variable<int32_t>(more, offset, memory_bytes);	26✔
321	}
322	while (offset < EBPF_TOTAL_STACK_SIZE) {	164✔
323	add_stack_variable<int64_t>(more, offset, memory_bytes);	84✔
324	}
325
326	return StringInvariant(more);	160✔
327	}	560✔
328
329	ConformanceTestResult run_conformance_test_case(const std::vector<std::byte>& memory_bytes,	444✔
330	const std::vector<std::byte>& program_bytes, bool debug) {
331	ebpf_context_descriptor_t context_descriptor{64, -1, -1, -1};	444✔
332	EbpfProgramType program_type = make_program_type("conformance_check", &context_descriptor);	666✔
333
334	ProgramInfo info{&g_platform_test, {}, program_type};	444✔
335
336	auto insts = vector_of<EbpfInst>(program_bytes);	444✔
337	StringInvariant pre_invariant = StringInvariant::top();	444✔
338
339	if (!memory_bytes.empty()) {	444✔
340	if (memory_bytes.size() > EBPF_TOTAL_STACK_SIZE) {	80✔
341	std::cerr << "memory size overflow\n";	×
342	return {};	×
343	}
344	pre_invariant = pre_invariant + stack_contents_invariant(memory_bytes);	200✔
345	}
346	RawProgram raw_prog{.prog = insts};	444✔
347	ebpf_platform_t platform = g_ebpf_platform_linux;	444✔
348	platform.supported_conformance_groups \|= bpf_conformance_groups_t::callx;	444✔
349	raw_prog.info.platform = &platform;	444✔
350
351	// Convert the raw program section to a set of instructions.
352	std::variant<InstructionSeq, std::string> prog_or_error = unmarshal(raw_prog);	444✔
353	if (auto prog = std::get_if<std::string>(&prog_or_error)) {	444✔
354	std::cerr << "unmarshaling error at " << *prog << "\n";	×
355	return {};	×
356	}
357
358	const InstructionSeq& inst_seq = std::get<InstructionSeq>(prog_or_error);	444✔
359
360	ebpf_verifier_options_t options{};	444✔
361	if (debug) {	444✔
362	print(inst_seq, std::cout, {});	×
363	options.verbosity_opts.print_failures = true;	×
364	options.verbosity_opts.print_invariants = true;	×
365	options.verbosity_opts.simplify = false;	×
366	}
367
368	try {	222✔
369	const Program prog = Program::from_sequence(inst_seq, info, options);	444✔
370	const Invariants invariants = analyze(prog, pre_invariant);	444✔
371	return ConformanceTestResult{.success = invariants.verified(prog), .r0_value = invariants.exit_value()};	444✔
372	} catch (const std::exception&) {	444✔
373	// Catch exceptions thrown in ebpf_domain.cpp.
374	return {};	×
375	}	×
376	}	888✔
377
378	void print_failure(const Failure& failure, std::ostream& os) {	×
379	constexpr auto INDENT = " ";	×
380	if (!failure.invariant.unexpected.empty()) {	×
381	os << "Unexpected properties:\n" << INDENT << failure.invariant.unexpected << "\n";	×
382	} else {
383	os << "Unexpected properties: None\n";	×
384	}
385	if (!failure.invariant.unseen.empty()) {	×
386	os << "Unseen properties:\n" << INDENT << failure.invariant.unseen << "\n";	×
387	} else {
388	os << "Unseen properties: None\n";	×
389	}
390
391	if (!failure.messages.unexpected.empty()) {	×
392	os << "Unexpected messages:\n";	×
393	for (const auto& item : failure.messages.unexpected) {	×
394	os << INDENT << item << "\n";	×
395	}
396	} else {
397	os << "Unexpected messages: None\n";	×
398	}
399
400	if (!failure.messages.unseen.empty()) {	×
401	os << "Unseen messages:\n";	×
402	for (const auto& item : failure.messages.unseen) {	×
403	os << INDENT << item << "\n";	×
404	}
405	} else {
406	os << "Unseen messages: None\n";	×
407	}
408	}	×
409
410	bool all_suites(const string& path) {	×
411	bool result = true;	×
412	for (const TestCase& test_case : read_suite(path)) {	×
413	result = result && static_cast<bool>(run_yaml_test_case(test_case));	×
414	}	×
415	return result;	×
416	}
417
418	void foreach_suite(const string& path, const std::function<void(const TestCase&)>& f) {	1,392✔
419	for (const TestCase& test_case : read_suite(path)) {	85,434✔
420	f(test_case);	126,063✔
421	}	1,392✔
422	}	1,392✔
423	} // namespace prevail

Alan-Jowett / ebpf-verifier / 18658728485

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