18949625295

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

Build # 18949625295

Build Type

push

github

Committed by

elazarg

Commit Message

Bump CLI11 to v2.6.1

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

Run Details

9022 of 10317 relevant lines covered (87.45%)

10783407.68 hits per line

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

75.82

/src/test/ebpf_yaml.cpp

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

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

#include <yaml-cpp/yaml.h>

#include "ebpf_verifier.hpp"
#include "ir/parse.hpp"
#include "ir/syntax.hpp"
#include "string_constraints.hpp"
#include "test/ebpf_yaml.hpp"
#include "verifier.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;

    // 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 {
            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 AnalysisResult result = analyze(prog, test_case.assumed_pre_invariant);
        const StringInvariant actual_last_invariant = result.invariant_at(Label::exit);
        std::set<string> actual_messages;
        if (auto error = result.find_first_error()) {
            actual_messages.insert(to_string(*error));
        }
        for (const auto& [label, msgs] : result.find_unreachable(prog)) {
            for (const auto& msg : msgs) {
                actual_messages.insert(msg);
            }
        }

        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 AnalysisResult result = analyze(prog, pre_invariant);
        return ConformanceTestResult{.success = !result.failed, .r0_value = result.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";
    }
}

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

Alan-Jowett / ebpf-verifier / 18949625295

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

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