15194704016

Committed 22 May 2025 08:53AM UTC coverage: 88.11% (-0.07%) from 88.177%

Build # 15194704016

Build Type

push

github

Committed by

elazarg

Commit Message

uniform class names and explicit constructors for adapt_sgraph.hpp

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

Run Details

27 of 30 new or added lines in 1 file covered. (90.0%)

481 existing lines in 33 files now uncovered.

8552 of 9706 relevant lines covered (88.11%)

9089054.61 hits per line

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

73.36

/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 <boost/algorithm/string.hpp>

#include <yaml-cpp/yaml.h>

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

Alan-Jowett / ebpf-verifier / 15194704016

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